Theory Examples.IICF_DS_Array_Idxs

theory IICF_DS_Array_Idxs
imports "Isabelle_LLVM.LLVM_DS_NArray" "Isabelle_LLVM.Proto_IICF_EOArray" IICF_Shared_Lists
begin

  (* TODO: Move *)
  lemma entailsD1: "a=b ⟹ a⊢b" by auto
  lemma entailsD2: "a=b ⟹ b⊢a" by auto

    
  (* TODO: Move *)  
  lemma htriple_exI: "⟦⋀x. htriple (P x) c Q⟧ ⟹ htriple (EXS x. P x) c Q"  
    unfolding htriple_def STATE_def by blast
    
  
  
  (* TODO: Move *)  
  lemma mk_assn_dr_prefix_eq[simp]: "mk_assn ↿A = A" unfolding mk_assn_def dr_assn_prefix_def by simp
  lemma dr_prefix_mk_assn_eq[simp]: "↿(mk_assn A) = A" unfolding mk_assn_def dr_assn_prefix_def by simp
    
  
  (* TODO: Move *)  
  lemma sint_in_int_image_cnv: "snat_invar ii ⟹ sint ii ∈ int ` s ⟷ snat ii ∈ s"  
    by (force simp add: cnv_snat_to_uint simp del: nat_uint_eq) 
    
  lemma nat_sint_to_snat: "nat (sint i) = snat i" unfolding snat_def by auto 

  lemma int_eq_sint_snat_eq_conv: "snat_invar ii ⟹ int i = sint ii ⟷ i = snat ii"  
    apply (auto simp: snat_def)
    by (simp add: cnv_snat_to_uint(2))
    
    
  (* TODO: Move *)  
  lemma SOLVE_AUTO_DEFER_FALSE[simp]: "SOLVE_AUTO_DEFER False = False" unfolding SOLVE_AUTO_DEFER_def by simp 
      
    

(* TODO: Move *)    
lemma fri_ll_range_cong: 
  assumes "PRECOND (SOLVE_AUTO (I'=I))"
  assumes "PRECOND (SOLVE_AUTO (∀i∈I. f' i = f i))"
  shows "↿(ll_range I) f p ⊢ ↿(ll_range I') f' p"
  using assms
  by (simp add: PRECOND_def SOLVE_AUTO_def cong: ll_range_cong)


(* TODO: Move *)
lemma entails_pure_triv_simps[simp]: 
  "(□ ⊢ ↑Q) ⟷ Q"  
  "(↑P ⊢ □)"  
  "(↑P ⊢ ↑Q) ⟷ (P ⟶ Q)"  
  by (auto simp: sep_algebra_simps entails_def)

lemma entails_exE: 
  assumes "⋀x. P x ⊢ Q"
  shows "(EXS x. P x) ⊢ Q"  
  using assms by (auto simp: entails_def)

  
  
(* TODO: Move *)    
lemma list_assn_append2[simp]: "length xs⇩2 = length ys⇩2 
  ⟹ ↿(list_assn A) (xs⇩1@xs⇩2) (ys⇩1@ys⇩2) = (↿(list_assn A) xs⇩1 ys⇩1 ** ↿(list_assn A) xs⇩2 ys⇩2)"  
  by (smt (verit, del_insts) add.commute add_diff_cancel_right' length_append list_assn_append list_assn_neq_len(2) sep_conj_commute)
    

    
section ‹Arrays with Partial Index Ownership›  

context begin

  interpretation llvm_prim_mem_setup .

  definition "array_idxs_dr_assn ≡ mk_assn (λxs p. 
    if xs=[] then □
    else ↿(ll_range (int ` sl_indexes' xs)) (sl_get xs o nat) p
  )"


  context
    notes [[coercion_enabled]]
  begin  
  (* For paper *)
  lemma "array_idxs_dr_assn = mk_assn (λxs p. 
    if xs=[] then □
    else ↿(ll_range {i | i. i<length xs ∧ xs!i≠None}) (λi. the (xs!nat i)) p
  )"
  proof -
    have 1: "int ` sl_indexes' xs = {int i | i. i<length xs ∧ xs!i≠None}" for xs :: "'a option list"
      unfolding sl_indexes_alt by auto
    thus ?thesis
      unfolding array_idxs_dr_assn_def sl_get_def
      apply (fo_rule cong refl)+
      apply (intro ext)
      apply (fo_rule ll_range_cong cong refl 1)+
      by auto
  
  qed
  end
  
  
  lemma array_idxs_empty[sep_algebra_simps]:
    "↿array_idxs_dr_assn [] p = □"  
    unfolding array_idxs_dr_assn_def
    by auto
      
  lemma narray_assn_to_idxs: "↿narray_assn xs p = (↿array_idxs_dr_assn (sl_of_list xs) p ** ↿array_base_assn (length xs) p)"  
    unfolding narray_assn_def LLVM_DS_Array.array_assn_def array_base_assn_def array_idxs_dr_assn_def
    apply (simp add: cong: ll_range_cong)
    apply (simp add: image_int_atLeastLessThan)
    by (auto simp: sep_algebra_simps comp_def split: list.splits)

  lemma array_slice_to_idxs: "↿LLVM_DS_NArray.array_slice_assn xs p = ↿array_idxs_dr_assn (sl_of_list xs) p"
    unfolding LLVM_DS_NArray.array_slice_assn_def array_idxs_dr_assn_def
    by (simp add: image_int_atLeastLessThan cong: ll_range_cong)
    
    
  lemma array_idxs_join_eq:
    assumes "sl_compat (sl_struct xs⇩1) (sl_struct xs⇩2)"
    shows "(↿array_idxs_dr_assn xs⇩1 p ** ↿array_idxs_dr_assn xs⇩2 p) = ↿array_idxs_dr_assn (sl_join xs⇩1 xs⇩2) p" 
  proof -
  
    have A: "i∈int`sl_indexes' xs⇩1 ⟹ sl_get xs⇩1 (nat i) = sl_get (sl_join xs⇩1 xs⇩2) (nat i)" for i
      by (auto simp add: assms sl_get_join1)

    have B: "i∈int`sl_indexes' xs⇩2 ⟹ sl_get xs⇩2 (nat i) = sl_get (sl_join xs⇩1 xs⇩2) (nat i)" for i
      by (auto simp add: assms sl_get_join2)
        
    show ?thesis  
      unfolding array_idxs_dr_assn_def
      using assms
      apply (clarsimp simp: sep_algebra_simps)
      apply (auto simp: sep_algebra_simps A B cong: ll_range_cong)
      
      apply (subst ll_range_merge)
      apply (auto dest!: sl_compat_idx_djD) []
      
      apply (fo_rule fun_cong arg_cong)+
      by auto
  qed  

  
  lemma array_idxs_join:
    "(↿array_idxs_dr_assn xs⇩1 p ** ↿array_idxs_dr_assn xs⇩2 p ** ↑(sl_compat (sl_struct xs⇩1) (sl_struct xs⇩2))) 
      ⊢ ↿array_idxs_dr_assn (sl_join xs⇩1 xs⇩2) p" 
    apply (clarsimp simp: pred_lift_move_front_simps entails_lift_extract_simps)  
    by (simp add: array_idxs_join_eq)
      

  lemma array_idxs_split_eq: 
    fixes ls xs
    defines "xs⇩1 ≡ sl_split ls xs"
    defines "xs⇩2 ≡ sl_split (-ls) xs"
    shows "↿array_idxs_dr_assn xs p = (↿array_idxs_dr_assn xs⇩1 p ** ↿array_idxs_dr_assn xs⇩2 p)"
    apply (subst array_idxs_join_eq)
    unfolding assms
    by (auto simp: sl_compat_splitI sl_join_split_eq)
    
    
  lemma array_idxs_nth_rule[vcg_rules]: "llvm_htriple
    (↿array_idxs_dr_assn xs p ** ↿snat.assn i ii ** ↑⇩d(i∈sl_indexes' xs))
    (array_nth p ii)
    (λr. ↑(r=sl_get xs i) ** ↿array_idxs_dr_assn xs p)
  "
    apply (cases "xs=[]"; (simp add: array_idxs_empty)?)
    unfolding array_nth_def array_idxs_dr_assn_def snat.assn_def
    supply [simp] = sint_in_int_image_cnv nat_sint_to_snat
    by vcg

  lemma array_idxs_upd_rule[vcg_rules]: "llvm_htriple
    (↿array_idxs_dr_assn xs p ** ↿snat.assn i ii ** ↑⇩d(i∈sl_indexes' xs))
    (array_upd p ii x)
    (λr. ↑(r=p) ** ↿array_idxs_dr_assn (sl_put xs i x) p)
  "
    apply (cases "xs=[]"; (simp add: array_idxs_empty)?)
    unfolding array_upd_def array_idxs_dr_assn_def snat.assn_def
    supply [simp] = sint_in_int_image_cnv nat_sint_to_snat int_eq_sint_snat_eq_conv
    supply [fri_rules] = fri_ll_range_cong
    by vcg

    
    
  definition [llvm_inline]: "raw_array_swap p i j ≡ doM {
    vi ← array_nth p i;
    vj ← array_nth p j;
    p ← array_upd p i vj;
    p ← array_upd p j vi;
    Mreturn p
  }"  
  
  
  (* TODO: raw_array_swap should be implemented for more arrays. *)
  lemma raw_array_swap_idxs_rule[vcg_rules]: "llvm_htriple 
    (↿array_idxs_dr_assn xs p ** ↿snat.assn i ii ** ↿snat.assn j ji ** ↑⇩d(i∈sl_indexes' xs ∧ j∈sl_indexes' xs))
    (raw_array_swap p ii ji)
    (λr. ↑(r=p) ** ↿array_idxs_dr_assn (swap xs i j) p)"
    unfolding raw_array_swap_def
    supply [simp] = sl_swap_aux
    by vcg
    
    
    
    
    
    
  subsection ‹Composition with Assertion for Elements›    
    
  context
    fixes A :: "('a,'c) dr_assn"
  begin  
  
    definition "option_assn ≡ mk_assn (λa c. case (a,c) of
        (None,None) ⇒ □
      | (Some a, Some c) ⇒ ↿A a c
      | _ ⇒ sep_false)
    "

    lemma option_assn_simps[simp]:  
      "↿option_assn None None = □"  
      "↿option_assn (Some a) (Some c) = ↿A a c"  
      "↿option_assn None (Some c) = sep_false"
      "↿option_assn (Some a) None = sep_false"
      
      "↿option_assn (Some a) bb = (EXS b. ↑(bb=Some b) ** ↿A a b)"
      "↿option_assn aa (Some b) = (EXS a. ↑(aa=Some a) ** ↿A a b)"
      "↿option_assn None bb = ↑(bb=None)"
      "↿option_assn aa None = ↑(aa=None)"
      
      unfolding option_assn_def 
      apply (auto split: option.splits simp: sep_algebra_simps)
      done
          
  end  

  definition "list_option_assn A ≡ list_assn (option_assn A)"
  
  lemma list_option_assn_imp_struct_eq: "pure_part (↿(list_option_assn A) xs xs') ⟹ sl_struct xs = sl_struct xs'"
    apply (induction xs xs' rule: list_induct2')
    by (auto simp: list_option_assn_def sep_algebra_simps dest!: pure_part_split_conj)
    
  lemma list_option_assn_empty[simp]: 
    "↿(list_option_assn A) [] [] = □"  
    "↿(list_option_assn A) [] (y#ys) = sep_false"  
    "↿(list_option_assn A) (x#xs) [] = sep_false"  
    unfolding list_option_assn_def
    by (auto simp: sep_algebra_simps)
    
    
  lemma list_option_assn_cons[simp]: "↿(list_option_assn A) (x#xs) (y#ys) 
    = (↿(option_assn A) x y ** ↿(list_option_assn A) xs ys)"  
    unfolding list_option_assn_def
    by simp
    
  lemma list_option_assn_cons1_conv:
    "↿(list_option_assn A) (x#xs') ys 
      = (EXS y ys'. ↑(ys=y#ys') ** ↿(option_assn A) x y ** ↿(list_option_assn A) xs' ys')"  
    unfolding list_option_assn_def
    by (auto simp: list_assn_cons1_conv)
    
  lemma list_option_assn_cons2_conv:
    "↿(list_option_assn A) xs (y#ys') 
      = (EXS x xs'. ↑(xs=x#xs') ** ↿(option_assn A) x y ** ↿(list_option_assn A) xs' ys')"  
    unfolding list_option_assn_def
    by (auto simp: list_assn_cons2_conv)

    
  (* TODO: append is more general! *)    
  lemma list_option_assn_snoc[simp]: "↿(list_option_assn A) (xs@[x]) (ys@[y]) = ( ↿(list_option_assn A) xs ys ** ↿(option_assn A) x y)"  
    unfolding list_option_assn_def
    by (auto simp: sep_algebra_simps)

  lemma list_option_assn_empty_conv[simp]:
    "↿(list_option_assn A) xs [] = (↑(xs=[]))"
    "↿(list_option_assn A) [] ys = (↑(ys=[]))"
    unfolding list_option_assn_def by auto
    
    
  lemma list_option_assn_pure_part[vcg_prep_ext_rules]: 
    "pure_part (↿(list_option_assn A) xs ys) ⟹ length xs = length ys" (* TODO: Extraction should also go to elements! *)  
    unfolding list_option_assn_def
    apply (vcg_prepare_external)
    by (auto)
    
        
  lemmas list_option_assn_cons_conv = list_option_assn_cons1_conv list_option_assn_cons2_conv
    
    
  lemma list_option_join_aux:
    assumes "sl_compat (sl_struct xs⇩1) (sl_struct xs⇩2)"
    shows 
      "(↿(list_option_assn A) xs⇩1 xs⇩1' ** ↿(list_option_assn A) xs⇩2 xs⇩2') 
      ⊢ ↿(list_option_assn A) (sl_join xs⇩1 xs⇩2) (sl_join xs⇩1' xs⇩2')" 
    using assms
  proof (induction xs⇩1 xs⇩2 arbitrary: xs⇩1' xs⇩2' rule: list_induct2')
    case 1
    then show ?case by (auto simp: sep_algebra_simps entails_def)
  next
    case (2 x⇩1 xs⇩1)
    then show ?case by simp
  next
    case (3 x⇩2 xs⇩2)
    then show ?case by simp
  next
    case (4 x⇩1 xs⇩1 x⇩2 xs⇩2)
    hence 
      COMPAT: "x⇩1=None ∨ x⇩2=None" and
      IH: "↿(list_option_assn A) xs⇩1 xs⇩1' ∧* ↿(list_option_assn A) xs⇩2 xs⇩2' 
          ⊢ ↿(list_option_assn A) (sl_join xs⇩1 xs⇩2) (sl_join xs⇩1' xs⇩2')" for xs⇩1' xs⇩2'
      by auto    
    
    show ?case
      apply (rewrite in "⌑⊢_" list_option_assn_cons1_conv)+
      apply (clarsimp 
            simp: pred_lift_move_front_simps entails_lift_extract_simps sep_conj_exists
            intro!: entails_exE)
    proof goal_cases
      case (1 x⇩1' xs⇩1'' x⇩2' xs⇩2'')
      then show ?case
        apply (sep_drule IH)
        using COMPAT
        apply (cases x⇩1; cases x⇩2; 
          clarsimp 
            simp: pred_lift_move_front_simps entails_lift_extract_simps sep_conj_exists
            intro!: entails_exE
        )
        apply fri
        apply fri
        done
        
    qed  
  qed
    
  lemma list_option_join:
    assumes "sl_compat (sl_struct xs⇩1) (sl_struct xs⇩2)"
    shows 
      "(↿(list_option_assn A) xs⇩1 xs⇩1' ** ↿(list_option_assn A) xs⇩2 xs⇩2') 
      ⊢ ↿(list_option_assn A) (sl_join xs⇩1 xs⇩2) (sl_join xs⇩1' xs⇩2') ** ↑(sl_compat (sl_struct xs⇩1') (sl_struct xs⇩2'))" 
    apply (rule entails_pureI)
    using assms
    apply (clarsimp dest!: pure_part_split_conj list_option_assn_imp_struct_eq simp: sep_algebra_simps)
    apply (rule list_option_join_aux) 
    by simp

        
  lemma list_option_split:
    fixes ls xs xs'
    defines "xs⇩1 ≡ sl_split ls xs"
    defines "xs⇩2 ≡ sl_split (-ls) xs"
    defines "xs⇩1' ≡ sl_split ls xs'"
    defines "xs⇩2' ≡ sl_split (-ls) xs'"
    shows "↿(list_option_assn A) xs xs' ⊢ ↿(list_option_assn A) xs⇩1 xs⇩1' ** ↿(list_option_assn A) xs⇩2 xs⇩2'"
    unfolding assms
  proof (induction xs xs' rule: rev_induct2')
    case empty
    then show ?case by (simp add: sep_algebra_simps)
  next
    case (snocl x⇩1 xs⇩1)
    then show ?case by simp
  next
    case (snocr x⇩1 xs⇩2)
    then show ?case by simp
  next
    case (snoclr x⇩1 xs⇩1 x⇩2 xs⇩2)
    
    show ?case 
      apply (rule entails_pureI)
      apply vcg_prepare_external
    
      apply (sep_drule snoclr.IH)
      apply (simp add: sl_split_snoc)
      apply (cases "length xs⇩2 ∈ ls"; simp)
      apply fri
      apply fri
      done
  qed    
      
  
  definition "oarray_idxs_dr_assn A ≡ mk_assn (assn_comp (↿(list_option_assn A)) (↿array_idxs_dr_assn))"
  
  lemma oarray_idxs_join:
    assumes COMPAT: "sl_compat (sl_struct xs⇩1) (sl_struct xs⇩2)"
    shows "(↿(oarray_idxs_dr_assn A) xs⇩1 p ** ↿(oarray_idxs_dr_assn A) xs⇩2 p) ⊢ ↿(oarray_idxs_dr_assn A) (sl_join xs⇩1 xs⇩2) p" 
    
    unfolding oarray_idxs_dr_assn_def assn_comp_def
    apply (clarsimp 
          simp: pred_lift_move_front_simps entails_lift_extract_simps sep_conj_exists
          intro!: entails_exE)
    apply (sep_drule list_option_join[OF COMPAT])      
    apply (sep_drule array_idxs_join)
    by fri

    
  lemma oarray_idxs_split: 
    fixes ls xs
    defines "xs⇩1 ≡ sl_split ls xs"
    defines "xs⇩2 ≡ sl_split (-ls) xs"
    shows "↿(oarray_idxs_dr_assn A) xs p ⊢ (↿(oarray_idxs_dr_assn A) xs⇩1 p ** ↿(oarray_idxs_dr_assn A) xs⇩2 p)"
    unfolding oarray_idxs_dr_assn_def assn_comp_def
    apply (clarsimp 
          simp: pred_lift_move_front_simps entails_lift_extract_simps sep_conj_exists assms
          intro!: entails_exE)
    apply (subst array_idxs_split_eq[where ls=ls])
    apply (sep_drule list_option_split[where ls=ls])
    apply fri
    done
    
  
  (* TODO: There's a simproc for that in HOL. And there was one in Sep_Logic_Imp_HOL. *)
  lemma EXS_det_simple: 
    "(EXS x. ↑(x=a) ** P x) = (P a)"
    "(EXS x x'. ↑(x=f x') ** Q x x') = (EXS x'. Q (f x') x')"
    by (auto simp: sep_algebra_simps)
    
    
  
  lemma list_option_map_Some1_conv:"↿(list_option_assn A) (map Some xs) yss = (EXS ys. ↑(yss = map Some ys) ** ↿(list_assn A) xs ys)"  
    apply (induction xs yss rule: list_induct2') 
    apply (simp_all add: sep_algebra_simps) [3]
    apply simp
    apply (thin_tac _)
    apply (simp add: list_assn_cons1_conv)
    apply (rule entails_eqI)
    
    apply (rule entails_pureI)
    apply (clarsimp 
      dest!: pure_part_split_conj
      simp: pred_lift_move_front_simps entails_lift_extract_simps sep_conj_exists
      intro!: entails_exE
      )
    subgoal for x xs y ys
      apply (rule entails_exI[where x="y#ys"])
      by fri
    
    apply (clarsimp 
      dest!: pure_part_split_conj
      simp: pred_lift_move_front_simps entails_lift_extract_simps sep_conj_exists
      intro!: entails_exE
      )
    apply fri  
    done
      
  lemma list_option_map_Some2_conv:
    "↿(list_option_assn A) xss (map Some ys) 
    = (EXS xs. ↑(xss = map Some xs) ** ↿(list_assn A) xs ys)"  
    apply (induction xss ys rule: list_induct2') 
    apply (simp_all add: sep_algebra_simps) [3]
    apply simp
    apply (thin_tac _)
    apply (simp add: list_assn_cons2_conv)
    apply (rule entails_eqI)
    
    apply (rule entails_pureI)
    apply (clarsimp 
      dest!: pure_part_split_conj
      simp: pred_lift_move_front_simps entails_lift_extract_simps sep_conj_exists
      intro!: entails_exE
      )
    subgoal for x xs y ys
      apply (rule entails_exI[where x="y#ys"])
      by fri
    
    apply (clarsimp 
      dest!: pure_part_split_conj
      simp: pred_lift_move_front_simps entails_lift_extract_simps sep_conj_exists
      intro!: entails_exE
      )
    apply fri  
    done
    
    
  lemma list_oelem_assn_map_Some_conv: "↿(list_assn (oelem_assn A)) (map Some xs) ys = ↿(list_assn A) xs ys"  
    apply (induction xs ys rule: list_induct2')
    by auto
    
  lemma sao_assn_map_Some_conv: "↿(sao_assn A) (map Some xs) p = (EXS xsh. (↿(list_assn A) xs xsh) ** raw_array_slice_assn xsh p)"  
    unfolding sao_assn_def
    by (simp add: list_oelem_assn_map_Some_conv sep_conj_commute)
    
  lemma woarray_slice_to_idxs: "woarray_slice_assn A xs p = ↿(oarray_idxs_dr_assn (mk_assn A)) (sl_of_list xs) p"
    unfolding woarray_slice_assn_def hr_comp_def
    apply (clarsimp 
      simp: some_list_rel_conv EXS_det_simple sl_of_list_def
      simp: pred_lift_move_front_simps entails_lift_extract_simps sep_conj_exists
    )
    unfolding oarray_idxs_dr_assn_def assn_comp_def
    apply (clarsimp simp: list_option_map_Some1_conv EXS_det_simple sep_conj_exists)
    unfolding eoarray_slice_assn_def
    by (simp add: sao_assn_map_Some_conv array_slice_to_idxs sl_of_list_def)

  lemma idxs_to_woarray_slice: "sl_complete (sl_struct xs) ⟹ ↿(oarray_idxs_dr_assn A) xs p = woarray_slice_assn (↿A) (list_of_sl xs) p"
    apply (subst woarray_slice_to_idxs)
    by simp
    
    
  lemma list_option_assn_swap: 
    "⟦i<length xs; j<length xs⟧ ⟹ ↿(list_option_assn A) (swap xs i j) (swap xs' i j) = ↿(list_option_assn A) xs xs'"  
    unfolding list_option_assn_def list_assn_def
    apply (cases "length xs = length xs'"; simp add: sep_algebra_simps)
    apply (cases "i=j"; simp?)
    apply (rewrite in "⌑=_" sep_set_img_remove[of i], simp)
    apply (rewrite in "⌑=_" sep_set_img_remove[of j], simp)
    apply (rewrite in "_=⌑" sep_set_img_remove[of i], simp)
    apply (rewrite in "_=⌑" sep_set_img_remove[of j], simp)
    apply (simp add: swap_def)
    apply (rule entails_eqI)
    apply fri+
    done
    
  lemma list_option_assn_swap_fri_rl: 
    "PRECOND (SOLVE_DEFAULT_AUTO (i<length xs ∧ j<length xs)) ⟹ ↿(list_option_assn A) xs xs' ⊢ ↿(list_option_assn A) (swap xs i j) (swap xs' i j)"  
    by (simp add: PRECOND_def SOLVE_DEFAULT_AUTO_def list_option_assn_swap)
    
  lemma sl_struct_eq_imp_length_eq: "sl_struct xs = sl_struct ys ⟹ length xs = length ys"  
    unfolding sl_struct_def by (rule map_eq_imp_length_eq)
  
  lemma raw_array_swap_oidxs_rule[vcg_rules]: "llvm_htriple 
    (↿(oarray_idxs_dr_assn A) xs p ** ↿snat.assn i ii ** ↿snat.assn j ji ** ↑⇩d(i∈sl_indexes' xs ∧ j∈sl_indexes' xs))
    (raw_array_swap p ii ji)
    (λr. ↑(r=p) ** ↿(oarray_idxs_dr_assn A) (swap xs i j) p)"
    unfolding oarray_idxs_dr_assn_def assn_comp_def
    apply (clarsimp simp: sep_conj_exists intro!: htriple_exI)
    apply (rule htriple_pure_preI)
    apply (clarsimp dest!: pure_part_split_conj list_option_assn_imp_struct_eq)
    apply (frule sl_struct_eq_imp_length_eq)

    supply [fri_rules] = list_option_assn_swap_fri_rl
    supply [dest] = sl_indexes_lengthD
    by vcg

    
  definition [llvm_inline]: "oidxs_split ls p ≡ Mreturn ()"  
  definition [llvm_inline]: "oidxs_join p⇩1 p⇩2 ≡ Mreturn ()"
  
  lemma oidxs_split_rule[vcg_rules]: "llvm_htriple 
    (↿(oarray_idxs_dr_assn A) xs p)
    (oidxs_split ls p)
    (λ_. ↿(oarray_idxs_dr_assn A) (sl_split ls xs) p ** ↿(oarray_idxs_dr_assn A) (sl_split (-ls) xs) p)"
    unfolding oidxs_split_def
    apply (rule htriple_ent_pre)
    apply (sep_drule oarray_idxs_split[where ls=ls], rule entails_refl)
    by vcg
  
  lemma oidxs_join_rule[vcg_rules]: "llvm_htriple
    (↿(oarray_idxs_dr_assn A) xs⇩1 p⇩1 ** ↿(oarray_idxs_dr_assn A) xs⇩2 p⇩2 ** ↑(p⇩1=p⇩2 ∧ sl_compat (sl_struct xs⇩1) (sl_struct xs⇩2)))
    (oidxs_join p⇩1 p⇩2)
    (λ_. ↿(oarray_idxs_dr_assn A) (sl_join xs⇩1 xs⇩2) p⇩2)"    
    unfolding oidxs_join_def
    apply (rule htriple_ent_pre)
    apply (clarsimp simp: pred_lift_move_front_simps entails_lift_extract_simps sep_conj_exists)
    apply (sep_drule oarray_idxs_join, simp)
    apply (rule entails_refl)
    by vcg

    
  definition "oarray_idxs_assn A ≡ ↿(oarray_idxs_dr_assn (mk_assn A))"
        
    
  definition "oidxs_with_idxs ls p m ≡ doM {
    oidxs_split ls p;
    (r,p⇩1,p⇩2) ← m p p;
    oidxs_join p⇩1 p⇩2;
    Mreturn (r,p)
  }"
  
  definition [llvm_inline]: "oidxs_with_idxs' p m ≡ doM { (r,_,_) ← m p p; Mreturn (r,p) }"
  
  lemma oidxs_with_idxs_elim_ghost[llvm_inline]: "oidxs_with_idxs ls p m = oidxs_with_idxs' p m"
    unfolding oidxs_with_idxs_def oidxs_split_def oidxs_join_def oidxs_with_idxs'_def
    by simp
  
  (* Monotonicity setup *)
  lemma oidxs_with_idxs_mono[partial_function_mono]:
    assumes "⋀xs⇩1 xs⇩2. M_mono' (λD. m D xs⇩1 xs⇩2)"
    shows "M_mono' (λD. oidxs_with_idxs ls a (m D))"
    unfolding oidxs_with_idxs_def using assms
    by pf_mono_prover

  lemma oidxs_with_idxs'_mono[partial_function_mono]:
    assumes "⋀xs⇩1 xs⇩2. M_mono' (λD. m D xs⇩1 xs⇩2)"
    shows "M_mono' (λD. oidxs_with_idxs' a (m D))"
    unfolding oidxs_with_idxs'_def using assms
    by pf_mono_prover
    
        
  lemma hn_WITH_IDXS_aux:
    assumes MHN: "⋀xs⇩1 xs⇩2. hn_refine 
      (hn_ctxt (oarray_idxs_assn A) xs⇩1 xsi ** hn_ctxt (oarray_idxs_assn A) xs⇩2 xsi ** F) 
      (mi xsi xsi) 
      (F') 
      (R ×⇩a oarray_idxs_assn A ×⇩a oarray_idxs_assn A) 
      (CP' xsi xsi) 
      (m xs⇩1 xs⇩2)"
    assumes CP': "⋀ri xsi⇩1' xsi⇩2'. CP' xsi xsi (ri,xsi⇩1',xsi⇩2') ⟹ xsi⇩1'=xsi ∧ xsi⇩2'=xsi ∧ CP ri"
    shows "hn_refine 
      (hn_ctxt (oarray_idxs_assn A) xs xsi ** F) 
      (oidxs_with_idxs' xsi mi) 
      (F') 
      (R ×⇩a oarray_idxs_assn A) 
      (λ(ri,xsi'). xsi'=xsi ∧ CP ri) 
      (WITH_IDXS ls xs m)"  
      
    apply (rewrite oidxs_with_idxs_elim_ghost[symmetric, where ls=ls])  
      
    apply (sepref_to_hoare)
    unfolding oidxs_with_idxs_def WITH_IDXS_def oarray_idxs_assn_def hn_ctxt_def
    
    supply [simp] = pure_def refine_pw_simps pw_le_iff sl_compat_splitI
    supply [dest] = CP'
    
    apply (clarsimp simp: )
    
    supply [vcg_rules] = hn_refineD[OF MHN, unfolded oarray_idxs_assn_def hn_ctxt_def]
    
    apply vcg
    apply (drule CP')
    apply vcg
    done
        
  lemma hn_WITH_IDXS_oarray_idxs[sepref_comb_rules]: 
    assumes FR: "Γ ⊢ hn_ctxt (oarray_idxs_assn A) xs xsi ** Γ⇩1"
    assumes HN: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2. ⟦ CP_assm (xsi⇩1 = xsi); CP_assm (xsi⇩2 = xsi) ⟧ ⟹ hn_refine 
      (hn_ctxt (oarray_idxs_assn A) xs⇩1 xsi⇩1 ** hn_ctxt (oarray_idxs_assn A) xs⇩2 xsi⇩2 ** Γ⇩1) 
      (mi xsi⇩1 xsi⇩2) 
      (Γ⇩2 xs⇩1 xsi⇩1 xs⇩2 xsi⇩2) (R) (CP xsi⇩1 xsi⇩2) (m xs⇩1 xs⇩2)"
    assumes CP: "⋀ri' xsi⇩1 xsi⇩2 xsi⇩1' xsi⇩2'. CP_assm (CP xsi⇩1 xsi⇩2 (ri',xsi⇩1',xsi⇩2')) ⟹ CP_cond (xsi⇩1' = xsi⇩1 ∧ xsi⇩2'=xsi⇩2)"  
    assumes FR2: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2. Γ⇩2 xs⇩1 xsi⇩1 xs⇩2 xsi⇩2 ⊢
      hn_invalid (oarray_idxs_assn A) xs⇩1 xsi⇩1 ** hn_invalid (oarray_idxs_assn A) xs⇩2 xsi⇩2 ** Γ⇩1'"
    assumes FR3: "⋀x xi. hn_ctxt R x xi ⊢ hn_ctxt (R' ×⇩a oarray_idxs_assn A ×⇩a oarray_idxs_assn A) x xi"  
    assumes CP2: "CP_simplify (CP_EX32 (CP xsi xsi)) (CP')"  
    shows "hn_refine 
      (Γ) 
      (oidxs_with_idxs' xsi mi) 
      (hn_invalid (oarray_idxs_assn A) xs xsi ** Γ⇩1') 
      (R' ×⇩a oarray_idxs_assn A) 
      (CP') 
      (PR_CONST (WITH_IDXS ls)$xs$(λ⇩2a b. m a b))"  
      unfolding autoref_tag_defs PROTECT2_def
      apply (rule hn_refine_cons_pre)
      applyS (rule FR)
      apply1 extract_hnr_invalids
      supply R = hn_WITH_IDXS_aux[where CP="λri. CP xsi xsi (ri,xsi,xsi)"]
      thm hn_refine_cons_cp[OF _ R[where CP'=CP]]
      apply (rule hn_refine_cons_cp[OF _ R])
      
      applyS (fri)
      apply1 extract_hnr_invalids
      
      supply R = hn_refine_cons[OF _ HN, of _ _ xsi _ xsi]
      thm R
      
      apply (rule R)
      applyS (fri)
      applyS (simp add: CP_defs)
      applyS (simp add: CP_defs)
      applyS (sep_drule FR2; simp; rule entails_refl)
      focus
        apply clarsimp
        apply (sep_drule FR3[unfolded hn_ctxt_def])
        apply simp
        apply (rule entails_refl)
        solved
      subgoal 
        using CP unfolding CP_defs by blast 
      applyS simp  
      applyS simp  
      subgoal
        using CP2 unfolding CP_defs by blast 
      done  
      
        
      
  lemma slist_swap_oidxs_hnr: "(uncurry2 raw_array_swap,uncurry2 mop_slist_swap) 
    ∈ [λ_. True]⇩c (oarray_idxs_assn A)⇧d *⇩a snat_assn⇧k *⇩a snat_assn⇧k → oarray_idxs_assn A [λ((xsi,_),_) ri. ri=xsi]⇩c"
    unfolding snat_rel_def snat.assn_is_rel[symmetric]
    apply sepref_to_hoare
    apply (simp add: refine_pw_simps)
    unfolding oarray_idxs_assn_def
    by vcg

  thm woarray_slice_to_idxs
  
  lemma oidxs_of_woarray_slice_hnr: "(Mreturn,mop_sl_of_list) ∈ [λ_. True]⇩c (woarray_slice_assn A)⇧d → oarray_idxs_assn A [λxsi ri. ri=xsi]⇩c"  
    apply sepref_to_hoare
    apply (simp add: woarray_slice_to_idxs oarray_idxs_assn_def)
    by vcg
    
  lemma woarray_slice_of_oidxs_hnr: "(Mreturn,mop_list_of_sl) ∈ [λ_. True]⇩c (oarray_idxs_assn A)⇧d → woarray_slice_assn A [λxsi ri. ri=xsi]⇩c"  
    apply sepref_to_hoare
    apply (simp add: refine_pw_simps)
    apply (simp add: idxs_to_woarray_slice oarray_idxs_assn_def)
    apply vcg
    done
    
              
  context
    notes [fcomp_norm_simps] = option_rel_id_simp list_rel_id_simp
  begin  
    sepref_decl_impl (ismop) slist_swap_oidxs_hnr uses mop_slist_swap.fref[of Id] .
    sepref_decl_impl (ismop) oidxs_of_woarray_slice_hnr .
    sepref_decl_impl (ismop) woarray_slice_of_oidxs_hnr .
  end


end

end