Theory IICF_Shared_Lists

theory IICF_Shared_Lists
imports "Isabelle_LLVM.IICF"
begin

(* TODO: Move *)  
lemma list_all2_append2: "length xs' = length ys' ⟹ list_all2 P (xs@xs') (ys@ys') ⟷ list_all2 P xs ys ∧ list_all2 P xs' ys'"  
  by (auto simp: list_all2_append list_all2_iff)

(* TODO: Move *)  
lemma rev_induct2 [consumes 1, case_names Nil snoc]:
  "length xs = length ys ⟹ P [] [] ⟹
   (⋀x xs y ys. length xs = length ys ⟹ P xs ys ⟹ P (xs@[x]) (ys@[y]))
   ⟹ P xs ys"
proof (induct xs arbitrary: ys rule: rev_induct)
  case (snoc x xs ys) then show ?case by (cases ys rule: rev_cases) simp_all
qed simp

lemma map_by_map_idx: "map f xs = map (f o nth xs) [0..<length xs]"  
  apply (induction xs rule: rev_induct)
  by auto
  
lemma map2_map_conv: "map2 f (map g xs) (map h ys) = map2 (λx y. f (g x) (h y)) xs ys"
  apply(induction xs ys rule: list_induct2')
  by auto
  
lemma map2_same[simp]: "map2 f xs xs = map (λx. f x x) xs"
  apply (induction xs) by auto
  

lemma nth_map2: "⟦ i<length xs; i<length ys ⟧ ⟹ map2 f xs ys ! i = f (xs!i) (ys!i)" by simp

lemma map2_update1: "map2 f (xs[i:=x]) ys = (map2 f xs ys)[i := f x (ys!i)]"
  by (metis list_update_id map_update old.prod.case zip_update)

lemma map2_update2: "map2 f xs (ys[i:=y]) = (map2 f xs ys)[i := f (xs!i) y]"
  by (metis list_update_id map_update old.prod.case zip_update)
    
lemma list_all2_map_map_conv: "list_all2 P (map f xs) (map g ys) = list_all2 (λx y. P (f x) (g y)) xs ys"
  by (auto simp: list.rel_map)
  


section ‹Lists with Element-wise Ownership›


  
subsection ‹Abstract Operations›
(* Split *)
definition "sl_split s xs = map (λi. if i∈s ∧ i<length xs then xs!i else None) [0..<length xs]"

(* Join *)
fun join_option where
  "join_option None y = y"
| "join_option x None = x"  
| "join_option _ _ = None"  (* Corner case mapped symmetrically to None *)

lemma join_option_add_simp[simp]: "join_option x None = x" by (cases x) auto

definition "sl_join = map2 join_option"

(* Conversion from/to plain list *)
definition "sl_of_list = map Some"
definition "list_of_sl = map the"

(* Structure *)
definition "sl_struct xs = map ((=)None) xs"
definition "sl_compat s⇩1 s⇩2 = list_all2 (∨) s⇩1 s⇩2"
definition "sl_complete s ⟷ set s ⊆ {False}"
definition "sl_indexes s = {i . i<length s ∧ ¬s!i}"

abbreviation "sl_indexes' xs ≡ sl_indexes (sl_struct xs)"

definition "sl_struct_join s⇩1 s⇩2 = map2 (=) s⇩1 s⇩2"
definition "sl_struct_split I s = map (λi. if i∈I then s!i else True) [0..<length s]"

(* Operations *)
definition "sl_get xs i = (if i<length xs then the (xs!i) else undefined (i-length xs))"
definition "sl_put xs i x = xs[i:=Some x]"


subsection ‹Lemmas for Abstract Operations›

lemma sl_indexes_alt: "sl_indexes' xs = {i . i<length xs ∧ xs!i ≠ None}"
  unfolding sl_indexes_def sl_struct_def
  by auto

lemma sl_of_list_empty[simp]: "sl_of_list [] = []"
  by (auto simp: sl_of_list_def)

lemma sl_of_list_eq_empty_conv[simp]: "sl_of_list xs = [] ⟷ xs=[]"
  by (auto simp: sl_of_list_def)

lemma sl_split_empty[simp]: "sl_split s [] = []" by (auto simp: sl_split_def) 
  
lemma sl_split_eq_empty_conv[simp]: "sl_split s xs = [] ⟷ xs=[]"  by (auto simp: sl_split_def)

lemma sl_struct_empty[simp]: "sl_struct [] = []" by (auto simp: sl_struct_def)
lemma sl_struct_eq_empty_conv[simp]: "sl_struct xs = [] ⟷ xs=[]" by (auto simp: sl_struct_def)

lemma sl_compat_empty[simp]: "sl_compat [] []" unfolding sl_compat_def by auto
lemma sl_compat_empty_conv[simp]: 
  "sl_compat [] xs⇩2 ⟷ xs⇩2 = []" 
  "sl_compat xs⇩1 [] ⟷ xs⇩1 = []" 
  unfolding sl_compat_def by auto


lemma sl_join_empty[simp]: 
  "sl_join [] xs = []"
  "sl_join xs [] = []"
  unfolding sl_join_def by auto

lemma sl_join_eq_empty_conv[simp]: "sl_compat (sl_struct xs⇩1) (sl_struct xs⇩2) ⟹ sl_join xs⇩1 xs⇩2 = [] ⟷ xs⇩1=[] ∧ xs⇩2=[]"  
  unfolding sl_join_def
  by auto
  
lemma sl_indexes_empty[simp]: "sl_indexes [] = {}"
  unfolding sl_indexes_def by auto
  
  
  
lemma sl_indexes_of_list[simp]: "sl_indexes' (sl_of_list xs) = {0..<length xs}"
  unfolding sl_indexes_def sl_struct_def sl_of_list_def by auto

lemma sl_struct_put[simp]: "i∈sl_indexes' xs ⟹ sl_struct (sl_put xs i x) = sl_struct xs"
  unfolding sl_indexes_def sl_struct_def sl_put_def 
  by (auto simp: map_update list_update_same_conv)

lemma sl_get_of_list[simp]: "i<length xs ⟹ sl_get (sl_of_list xs) i = xs!i"  
  unfolding sl_get_def sl_of_list_def by simp
  
lemma sl_put_of_list[simp]: "sl_put (sl_of_list xs) i x = sl_of_list (xs[i:=x])"
  unfolding sl_put_def sl_of_list_def 
  by (simp add: map_update)
  
lemma sl_list_of_list[simp]: "list_of_sl (sl_of_list xs) = xs"
  unfolding list_of_sl_def sl_of_list_def by auto

lemma sl_of_list_length[simp]: "length (sl_of_list xs) = length xs"  
  unfolding sl_of_list_def by auto
    
lemma sl_split_length[simp]: "length (sl_split s xs) = length xs"    
  unfolding sl_split_def by auto

lemma sl_struct_length[simp]: "length (sl_struct xs) = length xs"  
  unfolding sl_struct_def by auto
  
lemma sl_join_length_nopre: "length (sl_join xs ys) = min (length xs) (length ys)"  
  unfolding sl_join_def by simp

lemma sl_struct_join_length_nopre: "length (sl_struct_join s⇩1 s⇩2) = min (length s⇩1) (length s⇩2)"  
  unfolding sl_struct_join_def by auto

lemma sl_compat_lengthD: "sl_compat s⇩1 s⇩2 ⟹ length s⇩1 = length s⇩2"  
  unfolding sl_compat_def by (auto simp: list_all2_lengthD)
  
lemma sl_join_struct_length[simp]: "sl_compat s⇩1 s⇩2 ⟹ length (sl_struct_join s⇩1 s⇩2) = length s⇩2"  
  by (auto dest: sl_compat_lengthD simp: sl_struct_join_length_nopre)
  
lemma sl_join_length[simp]: "sl_compat (sl_struct xs) (sl_struct ys) ⟹ length (sl_join xs ys) = length ys"  
  by (auto dest: sl_compat_lengthD simp: sl_join_length_nopre)
  
lemma sl_struct_join[simp]: "sl_struct (sl_join xs ys) = sl_struct_join (sl_struct xs) (sl_struct ys)"
  unfolding sl_compat_def sl_join_def sl_struct_join_def sl_struct_def
  by (auto simp add: map2_map_conv)
  
lemma sl_join_indexes_nopre: "sl_indexes (sl_struct_join s⇩1 s⇩2) = ((sl_indexes s⇩1 ∪ sl_indexes s⇩2) - (sl_indexes s⇩1 ∩ sl_indexes s⇩2)) ∩ ({0..<min (length s⇩1) (length s⇩2)})"  
  unfolding sl_indexes_def
  apply (simp add: sl_struct_join_def)
  by auto
  
lemma sl_compat_idx_djD: "sl_compat s⇩1 s⇩2 ⟹ sl_indexes s⇩1 ∩ sl_indexes s⇩2 = {}"  
  unfolding sl_compat_def sl_indexes_def
  by (auto simp: sl_struct_def dest: list_all2_nthD) 
  
lemma sl_indexes_lengthD: "i∈sl_indexes s ⟹ i<length s"  
  unfolding sl_indexes_def by auto
  
lemma sl_join_indexes[simp]: "sl_compat s⇩1 s⇩2 ⟹ sl_indexes (sl_struct_join s⇩1 s⇩2) = sl_indexes s⇩1 ∪ sl_indexes s⇩2"  
  by (auto 0 3 simp: sl_join_indexes_nopre dest: sl_compat_idx_djD sl_compat_lengthD sl_indexes_lengthD)


lemma sl_get_split: "i∈s ⟹ sl_get (sl_split s xs) i = sl_get xs i"
  unfolding sl_get_def sl_split_def 
  apply (cases "i<length xs")
  by (auto simp: nth_undefined)
  
lemma sl_put_split: "i∈s ⟹ sl_put (sl_split s xs) i x = sl_split s (sl_put xs i x)"  
  unfolding sl_put_def sl_split_def 
  apply (cases "i<length xs")
  by (auto simp: nth_list_update intro: nth_equalityI)
  

    
  
lemma sl_get_join: "sl_compat (sl_struct xs) (sl_struct ys) ⟹ i<length ys ⟹ sl_get (sl_join xs ys) i = (if i∈sl_indexes' xs then sl_get xs i else sl_get ys i)"
  unfolding sl_indexes_def sl_compat_def sl_get_def sl_join_def sl_struct_def
  by (auto simp add: list.rel_map nth_map2 list_all2_lengthD dest: list_all2_nthD2)

lemma sl_get_join1: "sl_compat (sl_struct xs) (sl_struct ys) ⟹ i∈sl_indexes' xs ⟹ sl_get (sl_join xs ys) i = sl_get xs i"
  apply (subst sl_get_join)
  by (auto 0 3 simp: sl_get_join dest: sl_indexes_lengthD sl_compat_lengthD)
            
lemma sl_get_join2: "sl_compat (sl_struct xs) (sl_struct ys) ⟹ i∈sl_indexes' ys ⟹ sl_get (sl_join xs ys) i = sl_get ys i"
  apply (subst sl_get_join)
  by (auto 0 3 simp: sl_get_join dest: sl_indexes_lengthD sl_compat_lengthD sl_compat_idx_djD)

lemma sl_put_join1: "sl_compat (sl_struct xs) (sl_struct ys) ⟹ i∈sl_indexes' xs ⟹ sl_put (sl_join xs ys) i x = sl_join (sl_put xs i x) ys"
  unfolding sl_indexes_def sl_compat_def sl_put_def sl_join_def sl_struct_def
  by (auto 0 3 simp add: list.rel_map nth_map2 list_all2_lengthD map2_update1 dest: list_all2_nthD2)
  
lemma sl_put_join2: "sl_compat (sl_struct xs) (sl_struct ys) ⟹ i∈sl_indexes' ys ⟹ sl_put (sl_join xs ys) i x = sl_join xs (sl_put ys i x)"
  unfolding sl_indexes_def sl_compat_def sl_put_def sl_join_def sl_struct_def
  by (auto 0 3 simp add: list.rel_map nth_map2 list_all2_lengthD map2_update2 dest: list_all2_nthD2)

lemma sl_struct_split[simp]: "sl_struct (sl_split s xs) = sl_struct_split s (sl_struct xs)"
  unfolding sl_struct_def sl_split_def sl_struct_split_def
  by auto
  
lemma sl_compat_splitI: "s∩s'={} ⟹ sl_compat (sl_struct_split s (sl_struct xs)) (sl_struct_split s' (sl_struct xs))"
  by (auto simp: sl_compat_def sl_struct_split_def list.rel_map intro!: list.rel_refl)
  
  
lemma sl_indexes_split: "sl_indexes (sl_struct_split I s) = I ∩ sl_indexes s"
  unfolding sl_indexes_def sl_struct_split_def
  by auto
  
  
lemma sl_of_list_complete[simp]: "sl_complete (sl_struct (sl_of_list xs))"  
  unfolding sl_complete_def sl_struct_def sl_of_list_def by auto
  
lemma sl_get_complete[simp]: "sl_complete (sl_struct xs) ⟹ sl_get xs i = list_of_sl xs!i"  
  unfolding sl_complete_def sl_struct_def sl_of_list_def sl_get_def list_of_sl_def
  apply (cases "i<length xs")  
  by (simp_all add: nth_undefined)

lemma list_eq_iff_sl_eq: "xs=xs' 
  ⟷ (length xs = length xs' ∧ sl_indexes' xs = sl_indexes' xs' ∧ (∀i∈sl_indexes' xs'. sl_get xs i = sl_get xs' i))"
  apply (rule iffI)
  apply (auto; fail)
  apply (clarsimp simp: sl_indexes_alt sl_get_def list_eq_iff_nth_eq)
  by (smt (verit) mem_Collect_eq option.exhaust_sel option.sel)
  
  
lemma sl_join_split_eq: "sl_join (sl_split ls xs) (sl_split (-ls) xs) = xs"  
  apply (auto simp: list_eq_iff_sl_eq sl_compat_splitI sl_indexes_split )
  apply (subst sl_get_join)
  apply (simp add: sl_compat_splitI; fail)
  apply (auto dest: sl_indexes_lengthD; fail) []
  apply (auto simp: sl_get_split sl_indexes_split)
  done
  
lemma sl_put_empty_iff[simp]: "sl_put xs i x = [] ⟷ xs=[]"  
  unfolding sl_put_def by auto


lemma sl_get_put[simp]: "i∈sl_indexes' xs ⟹ sl_get (sl_put xs i x) i = x"  
  unfolding sl_get_def sl_put_def
  by (auto dest: sl_indexes_lengthD)

lemma sl_get_put_indep[simp]: "i≠j ⟹ sl_get (sl_put xs i x) j = sl_get xs j"  
  unfolding sl_get_def sl_put_def
  by (auto)

lemma sl_put_get[simp]: "i∈sl_indexes' xs ⟹ sl_put xs i (sl_get xs i) = xs"  
  unfolding sl_get_def sl_put_def sl_indexes_alt
  by auto
    
definition "sl_split1' b x ≡ if b then x else None"  
lemma sl_split1'_simp[simp]:
  "sl_split1' True x = x"
  "sl_split1' False x = None"
  "sl_split1' b None = None"
  unfolding sl_split1'_def by auto

      
lemma sl_split_snoc: "sl_split ls (xs@[x]) = sl_split ls xs @ [ sl_split1' (length xs ∈ ls) x]"  
  unfolding sl_split_def
  by auto
  
lemma sl_struct_Cons[simp]: "sl_struct (x#xs) = (x=None)#sl_struct xs"
  by (auto simp: sl_struct_def)


lemma sl_compat_Cons[simp]: "sl_compat (x#xs) (y#ys) ⟷ (x∨y) ∧ sl_compat xs ys"  
  unfolding sl_compat_def
  by simp
      
lemma sl_join_Cons[simp]: "sl_join (x#xs) (y#ys) = join_option x y # sl_join xs ys"  
  unfolding sl_join_def by simp
  
lemma sl_indexes_finite[simp, intro!]: "finite (sl_indexes s)" by (auto simp: sl_indexes_def)

lemma sl_struct_join_split: "sl_struct_join (sl_struct_split I s) (sl_struct_split (-I) s) = s"
  unfolding sl_struct_join_def sl_struct_split_def
  by (auto simp: map2_map_conv map_nth) 

(*
lemma sl_join_split_eq: "sl_join (sl_split s xs) (sl_split (-s) xs) = xs"  
  unfolding sl_join_def sl_split_def 
  apply (rewrite at "_ = ⌑" map_nth[symmetric])
  by (auto simp: map2_map_conv)
*)  
  
lemma mset_of_list_permut: "mset xs = mset (sl_of_list xs⇩0) ⟹ mset (list_of_sl xs) = mset xs⇩0" 
  unfolding sl_of_list_def list_of_sl_def
  by (simp add: mset_map_id)

lemma length_sl_put[simp]: "length (sl_put xs i x) = length xs" unfolding sl_put_def by auto


lemma sl_swap_aux: "⟦i ∈ sl_indexes' xs; j ∈ sl_indexes' xs⟧ 
  ⟹ sl_put (sl_put xs i (sl_get xs j)) j (sl_get xs i) = swap xs i j"
  by (auto simp add: list_eq_iff_nth_eq sl_put_def sl_get_def sl_indexes_alt swap_def)
  
  
  
(* TODO: Move *)  
lemma sl_struct_swap[simp]: "⟦ i∈sl_indexes' xs; j∈sl_indexes' xs ⟧ ⟹ sl_struct (swap xs i j) = sl_struct xs"
  by (simp flip: sl_swap_aux)
  
  
lemma sl_get_swap_iff: "⟦ i∈sl_indexes' xs; j∈sl_indexes' xs ⟧ ⟹ sl_get (swap xs i j) k = (if k=i then sl_get xs j else if k=j then sl_get xs i else sl_get xs k)"  
  by (auto simp add: sl_get_def swap_nth dest!: sl_indexes_lengthD)
  
lemma sl_get_swap_other: "⟦k≠i; k≠j⟧ ⟹ sl_get (swap xs i j) k = sl_get xs k"  
  by (simp add: sl_get_def swap_def)

  


lemma slcompat_None_lower_bound:
  assumes "sl_compat (sl_struct xs⇩1) (sl_struct xs⇩2)"  
  shows "replicate_mset (length xs⇩1) None ⊆# mset xs⇩1 + mset xs⇩2"  
proof -
  from assms show ?thesis
    unfolding sl_compat_def sl_struct_def
    apply (simp add: list.rel_map)
    apply (induction xs⇩1 xs⇩2 rule: list_all2_induct)
    apply (auto)
    subgoal by (metis add_mset_add_single mset_le_incr_right1)
    subgoal by (meson mset_le_add_mset_decr_left1 subset_mset.dual_order.refl subset_mset.dual_order.trans)
    done
    
qed      
  

lemma mset_join_idxs_eq:
  assumes "sl_compat (sl_struct xs⇩1) (sl_struct xs⇩2)"  
  shows "mset (sl_join xs⇩1 xs⇩2) = mset xs⇩1 + mset xs⇩2 - replicate_mset (length xs⇩1) None"
  using sl_compat_lengthD[OF assms] assms
  apply simp
  apply (induction xs⇩1 xs⇩2 rule: list_induct2)
  subgoal by (auto simp: sl_join_def)
  subgoal for x xs y ys
    using slcompat_None_lower_bound[of xs ys]
    unfolding sl_compat_def sl_struct_def
    apply (auto simp: sl_join_def)
    subgoal by (metis add_mset_add_single subset_mset.add_diff_assoc2)
    subgoal by (metis add_mset_add_single subset_mset.add_diff_assoc2)
    done
  done

  
(* TODO: Move *)
lemma fold_is_None': "(=)None = is_None" by auto

lemma sl_struct_param[param]: "(sl_struct,sl_struct) ∈ ⟨⟨A⟩option_rel⟩list_rel → ⟨bool_rel⟩list_rel"  
  unfolding sl_struct_def fold_is_None'
  by parametricity
  
lemma sl_indexes_param[param]: "(sl_indexes, sl_indexes) ∈ ⟨bool_rel⟩list_rel → ⟨nat_rel⟩set_rel" by simp

lemma sl_split_param[param]: "(sl_split,sl_split) ∈ ⟨nat_rel⟩set_rel → ⟨⟨A⟩option_rel⟩list_rel → ⟨⟨A⟩option_rel⟩list_rel"
  unfolding sl_split_def
  apply parametricity
  by auto

lemma join_option_param[param]: "(join_option, join_option) ∈ ⟨A⟩option_rel → ⟨A⟩option_rel → ⟨A⟩option_rel"
  by (auto simp: option_rel_def)

lemma sl_join_param[param]: "(sl_join, sl_join) ∈ ⟨⟨A⟩option_rel⟩list_rel → ⟨⟨A⟩option_rel⟩list_rel → ⟨⟨A⟩option_rel⟩list_rel"  
  unfolding sl_join_def
  by parametricity
  
lemma sl_complete_sl_of_list_of_sl[simp]: "sl_complete (sl_struct xs) ⟹ sl_of_list (list_of_sl xs) = xs"
  unfolding sl_of_list_def list_of_sl_def sl_complete_def
  apply (induction xs)
  by auto
  
  
  
subsection ‹Sepref ADT Setup›  
sepref_decl_op slist_swap: "swap:: _ option list ⇒ _ "
  :: "[λ((l,i),j). i∈sl_indexes' l ∧ j∈sl_indexes' l]⇩f (⟨⟨A⟩option_rel⟩list_rel ×⇩r nat_rel) ×⇩r nat_rel → ⟨⟨A⟩option_rel⟩list_rel" 
  apply rule
  apply (clarsimp dest!: sl_indexes_lengthD)
  apply parametricity
  by auto

sepref_decl_op sl_of_list :: "⟨Id::'a rel⟩list_rel → ⟨⟨Id::'a rel⟩option_rel⟩list_rel" . 
  
sepref_decl_op list_of_sl :: "[λxs. sl_complete (sl_struct xs) ]⇩f ⟨⟨Id::'a rel⟩option_rel⟩list_rel → ⟨Id::'a rel⟩list_rel" by auto 
  
  
    
subsection ‹With-Idxs Combinator›  
  
definition "WITH_IDXS ls xs m ≡ do {
  ASSERT (ls⊆sl_indexes' xs);

  let xs⇩1 = sl_split ls xs;
  let xs⇩2 = sl_split (-ls) xs;
  
  (r,xs⇩1',xs⇩2') ← m xs⇩1 xs⇩2;
  
  ASSERT (sl_struct xs⇩1' = sl_struct xs⇩1);
  ASSERT (sl_struct xs⇩2' = sl_struct xs⇩2);

  RETURN (r,sl_join xs⇩1' xs⇩2')
}"

lemma WITH_IDXS_rule[refine_vcg]:
  assumes "ls ⊆ sl_indexes' xs"
  assumes "⋀xs⇩1 xs⇩2. ⟦ 
    xs⇩1 = sl_split ls xs; 
    xs⇩2 = sl_split (-ls) xs;
    sl_compat (sl_struct xs⇩1) (sl_struct xs⇩2)
  ⟧ ⟹ m xs⇩1 xs⇩2 ≤ SPEC (λ(r,xs⇩1',xs⇩2'). 
            sl_struct xs⇩1' = sl_struct xs⇩1 
          ∧ sl_struct xs⇩2' = sl_struct xs⇩2   
          ∧ P (r, sl_join xs⇩1' xs⇩2')
        )
        "
  shows "WITH_IDXS ls xs m ≤ SPEC P"
  unfolding WITH_IDXS_def
  apply refine_vcg
  apply fact
  apply (refine_vcg assms(2))
  apply (auto simp: sl_compat_splitI)
  done

  
lemma WITH_IDXS_mono[refine_mono]: 
  "⟦⋀a b. f a b ≤ f' a b⟧ ⟹ WITH_IDXS ls xs f ≤ WITH_IDXS ls xs f'"
  unfolding WITH_IDXS_def
  by refine_mono

lemma WITH_IDXS_mono_flat[refine_mono]: 
  "⟦⋀a b. flat_ge (f a b) (f' a b)⟧ ⟹ flat_ge (WITH_IDXS ls xs f) (WITH_IDXS ls xs f')"
  unfolding WITH_IDXS_def
  by refine_mono
  
  
(* Monadifier setup *)

lemma WITH_IDXS_pat[def_pat_rules]:
  "WITH_IDXS$ls ≡ UNPROTECT (WITH_IDXS ls)"
  by (simp)

term WITH_IDXS  
  
lemma id_WITH_IDXS[id_rules]: 
  "PR_CONST (WITH_IDXS ls) ::⇩i TYPE('a option list ⇒ ('a option list ⇒ 'a option list ⇒ ('b × 'c option list × 'c option list) nres) ⇒ ('b × 'c option list) nres)"
  by simp

lemma WITH_IDXS_arity[sepref_monadify_arity]: "PR_CONST (WITH_IDXS ls) ≡ λ⇩2xs f. SP (PR_CONST (WITH_IDXS ls))$xs$(λ⇩2a b. f$a$b)"
  by simp

lemma WITH_IDXS_comb[sepref_monadify_comb]:  
  "PR_CONST (WITH_IDXS ls)$xs$f = Refine_Basic.bind$(EVAL$xs)$(λ⇩2xs. SP (PR_CONST (WITH_IDXS ls))$xs$f)"
  by simp

  
  
  
  
lemma WITH_IDXS_refine[refine]:
  assumes "(ls',ls)∈Id"
  assumes "(xs',xs) ∈ ⟨⟨A⟩option_rel⟩list_rel"
  assumes [refine]: "⟦ls ⊆ sl_indexes' xs; ls' ⊆ sl_indexes' xs'⟧ 
    ⟹ m' (sl_split ls' xs') (sl_split (-ls') xs') ≤ ⇓(R×⇩r⟨⟨A⟩option_rel⟩list_rel×⇩r⟨⟨A⟩option_rel⟩list_rel) (m (sl_split ls xs) (sl_split (-ls) xs))"
  shows "WITH_IDXS ls' xs' m' ≤⇓(R ×⇩r ⟨⟨A⟩option_rel⟩list_rel) (WITH_IDXS ls xs m)"
  unfolding WITH_IDXS_def
  apply (rule nres_relD)
  using assms(1,2)
  apply refine_rcg
  subgoal
    apply (subgoal_tac "(sl_indexes' xs', sl_indexes' xs)∈⟨nat_rel⟩set_rel")
    apply simp
    by parametricity
  apply clarsimp  
  subgoal for _ xx1s xx2s _ xx1s' xx2s'
    apply (subgoal_tac "(sl_struct xx1s',sl_struct xx1s) ∈ ⟨bool_rel⟩list_rel")
    apply (subgoal_tac "(sl_struct xs',sl_struct xs) ∈ ⟨bool_rel⟩list_rel")
    apply auto []
    apply parametricity
    apply parametricity
    done
  apply clarsimp  
  subgoal for _ xx1s xx2s _ xx1s' xx2s'
    apply (subgoal_tac "(sl_struct xx2s',sl_struct xx2s) ∈ ⟨bool_rel⟩list_rel")
    apply (subgoal_tac "(sl_struct xs',sl_struct xs) ∈ ⟨bool_rel⟩list_rel")
    apply auto []
    apply parametricity
    apply parametricity
    done
  subgoal  
    apply parametricity
    by simp_all  
  done  

end