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  ab" by auto
  lemma entailsD2: "a=b  ba" 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 (iI. 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 xs2 = length ys2 
   (list_assn A) (xs1@xs2) (ys1@ys2) = ((list_assn A) xs1 ys1 ** (list_assn A) xs2 ys2)"  
  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!iNone}) (λi. the (xs!nat i)) p
  )"
  proof -
    have 1: "int ` sl_indexes' xs = {int i | i. i<length xs  xs!iNone}" 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 xs1) (sl_struct xs2)"
    shows "(array_idxs_dr_assn xs1 p ** array_idxs_dr_assn xs2 p) = array_idxs_dr_assn (sl_join xs1 xs2) p" 
  proof -
  
    have A: "iint`sl_indexes' xs1  sl_get xs1 (nat i) = sl_get (sl_join xs1 xs2) (nat i)" for i
      by (auto simp add: assms sl_get_join1)

    have B: "iint`sl_indexes' xs2  sl_get xs2 (nat i) = sl_get (sl_join xs1 xs2) (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 xs1 p ** array_idxs_dr_assn xs2 p ** (sl_compat (sl_struct xs1) (sl_struct xs2))) 
       array_idxs_dr_assn (sl_join xs1 xs2) 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 "xs1  sl_split ls xs"
    defines "xs2  sl_split (-ls) xs"
    shows "array_idxs_dr_assn xs p = (array_idxs_dr_assn xs1 p ** array_idxs_dr_assn xs2 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(isl_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(isl_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(isl_indexes' xs  jsl_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 xs1) (sl_struct xs2)"
    shows 
      "((list_option_assn A) xs1 xs1' ** (list_option_assn A) xs2 xs2') 
       (list_option_assn A) (sl_join xs1 xs2) (sl_join xs1' xs2')" 
    using assms
  proof (induction xs1 xs2 arbitrary: xs1' xs2' rule: list_induct2')
    case 1
    then show ?case by (auto simp: sep_algebra_simps entails_def)
  next
    case (2 x1 xs1)
    then show ?case by simp
  next
    case (3 x2 xs2)
    then show ?case by simp
  next
    case (4 x1 xs1 x2 xs2)
    hence 
      COMPAT: "x1=None  x2=None" and
      IH: "(list_option_assn A) xs1 xs1' ∧* (list_option_assn A) xs2 xs2' 
           (list_option_assn A) (sl_join xs1 xs2) (sl_join xs1' xs2')" for xs1' xs2'
      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 x1' xs1'' x2' xs2'')
      then show ?case
        apply (sep_drule IH)
        using COMPAT
        apply (cases x1; cases x2; 
          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 xs1) (sl_struct xs2)"
    shows 
      "((list_option_assn A) xs1 xs1' ** (list_option_assn A) xs2 xs2') 
       (list_option_assn A) (sl_join xs1 xs2) (sl_join xs1' xs2') ** (sl_compat (sl_struct xs1') (sl_struct xs2'))" 
    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 "xs1  sl_split ls xs"
    defines "xs2  sl_split (-ls) xs"
    defines "xs1'  sl_split ls xs'"
    defines "xs2'  sl_split (-ls) xs'"
    shows "(list_option_assn A) xs xs'  (list_option_assn A) xs1 xs1' ** (list_option_assn A) xs2 xs2'"
    unfolding assms
  proof (induction xs xs' rule: rev_induct2')
    case empty
    then show ?case by (simp add: sep_algebra_simps)
  next
    case (snocl x1 xs1)
    then show ?case by simp
  next
    case (snocr x1 xs2)
    then show ?case by simp
  next
    case (snoclr x1 xs1 x2 xs2)
    
    show ?case 
      apply (rule entails_pureI)
      apply vcg_prepare_external
    
      apply (sep_drule snoclr.IH)
      apply (simp add: sl_split_snoc)
      apply (cases "length xs2  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 xs1) (sl_struct xs2)"
    shows "((oarray_idxs_dr_assn A) xs1 p ** (oarray_idxs_dr_assn A) xs2 p)  (oarray_idxs_dr_assn A) (sl_join xs1 xs2) 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 "xs1  sl_split ls xs"
    defines "xs2  sl_split (-ls) xs"
    shows "(oarray_idxs_dr_assn A) xs p  ((oarray_idxs_dr_assn A) xs1 p ** (oarray_idxs_dr_assn A) xs2 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(isl_indexes' xs  jsl_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 p1 p2  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) xs1 p1 ** (oarray_idxs_dr_assn A) xs2 p2 ** (p1=p2  sl_compat (sl_struct xs1) (sl_struct xs2)))
    (oidxs_join p1 p2)
    (λ_. (oarray_idxs_dr_assn A) (sl_join xs1 xs2) p2)"    
    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,p1,p2)  m p p;
    oidxs_join p1 p2;
    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 "xs1 xs2. M_mono' (λD. m D xs1 xs2)"
    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 "xs1 xs2. M_mono' (λD. m D xs1 xs2)"
    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: "xs1 xs2. hn_refine 
      (hn_ctxt (oarray_idxs_assn A) xs1 xsi ** hn_ctxt (oarray_idxs_assn A) xs2 xsi ** F) 
      (mi xsi xsi) 
      (F') 
      (R ×a oarray_idxs_assn A ×a oarray_idxs_assn A) 
      (CP' xsi xsi) 
      (m xs1 xs2)"
    assumes CP': "ri xsi1' xsi2'. CP' xsi xsi (ri,xsi1',xsi2')  xsi1'=xsi  xsi2'=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: "xs1 xsi1 xs2 xsi2.  CP_assm (xsi1 = xsi); CP_assm (xsi2 = xsi)   hn_refine 
      (hn_ctxt (oarray_idxs_assn A) xs1 xsi1 ** hn_ctxt (oarray_idxs_assn A) xs2 xsi2 ** Γ1) 
      (mi xsi1 xsi2) 
      (Γ2 xs1 xsi1 xs2 xsi2) (R) (CP xsi1 xsi2) (m xs1 xs2)"
    assumes CP: "ri' xsi1 xsi2 xsi1' xsi2'. CP_assm (CP xsi1 xsi2 (ri',xsi1',xsi2'))  CP_cond (xsi1' = xsi1  xsi2'=xsi2)"  
    assumes FR2: "xs1 xsi1 xs2 xsi2. Γ2 xs1 xsi1 xs2 xsi2 
      hn_invalid (oarray_idxs_assn A) xs1 xsi1 ** hn_invalid (oarray_idxs_assn A) xs2 xsi2 ** Γ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_assnk *a snat_assnk  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