Theory Proto_EOArray

theory Proto_EOArray
imports LLVM_DS_NArray
begin
  
  subsection List Assertion

  definition "list_assn A  mk_assn (λxs xsi. (length xs = length xsi) ** (⋃*i{0..<length xs}. A (xs!i) (xsi!i)))"

  text Inductive characterization
  lemma list_assn_ee_simp:
    "(list_assn A) [] [] = "
    unfolding list_assn_def
    by (auto simp: sep_algebra_simps)
  
  lemma list_assn_nm_simp:
    "(list_assn A) [] (xi#xsi) = sep_false"
    "(list_assn A) (x#xs) [] = sep_false"
    unfolding list_assn_def
    by (auto simp: sep_algebra_simps)


  lemma list_assn_cc_simp:
    shows "(list_assn A) (x#xs) (xi#xsi) = (A x xi ** (list_assn A) xs xsi)"
  proof -
    have intv_conv1: "{0..<Suc n} = insert 0 (Suc`{0..<n})" for n by auto
    have 1: "(⋃*i{0..<Suc n}. A i) = (A 0 ** (⋃*i{0..<n}. A (Suc i)))" for A :: "nat  ll_assn" and n
      by (simp del: image_Suc_atLeastLessThan add: intv_conv1 sep_set_img_map)
  
    show ?thesis
      unfolding list_assn_def
      by (auto simp: sep_algebra_simps entails_lift_extract_simps entails_eq_iff 1)
      
  qed    
  

  lemmas list_assn_simps[simp] = list_assn_ee_simp list_assn_nm_simp list_assn_cc_simp
  
  lemma list_assn_empty1_conv[simp]: "(list_assn A) [] ys = (ys=[])"
    by (cases ys) (auto simp: sep_algebra_simps)

  lemma list_assn_empty2_conv[simp]: "(list_assn A) xs [] = (xs=[])"
    by (cases xs) (auto simp: sep_algebra_simps)
    
    
  lemma list_assn_cons1_conv: "(list_assn A) (x#xs) yys = (EXS y ys. (yys=y#ys) ** A x y ** (list_assn A) xs ys)"
    apply (cases yys)
    by (auto simp: entails_eq_iff sep_algebra_simps)
  
  lemma list_assn_cons2_conv: "(list_assn A) xxs (y#ys) = (EXS x xs. (xxs=x#xs) ** A x y ** (list_assn A) xs ys)"
    apply (cases xxs)
    by (auto simp: entails_eq_iff sep_algebra_simps)
  
  lemma list_assn_append1_conv: "(list_assn A) (xs1@xs2) yys = (EXS ys1 ys2. (yys=ys1@ys2) ** (list_assn A) xs1 ys1 ** (list_assn A) xs2 ys2)"
    apply (induction xs1 arbitrary: yys)
    by (auto simp: sep_algebra_simps list_assn_cons1_conv)
  
  lemma list_assn_append2_conv: "(list_assn A) xxs (ys1@ys2) = (EXS xs1 xs2. (xxs=xs1@xs2) ** (list_assn A) xs1 ys1 ** (list_assn A) xs2 ys2)"
    apply (induction ys1 arbitrary: xxs)
    by (auto simp: sep_algebra_simps list_assn_cons2_conv)

  lemma list_assn_neq_len[simp]: 
    "length xs  length xsi  (list_assn A) xs xsi = sep_false"  
    "length xsi  length xs  (list_assn A) xs xsi = sep_false"  
    by (auto simp: list_assn_def)
    
  lemma list_assn_append[simp]: "length xs1 = length ys1 
     (list_assn A) (xs1@xs2) (ys1@ys2) = ((list_assn A) xs1 ys1 ** (list_assn A) xs2 ys2)"  
    apply (induction rule: list_induct2)
    by (auto simp: sep_algebra_simps)
    
    
  lemma list_assn_pure_part[vcg_prep_ext_rules]: 
    "pure_part ((list_assn A) xs ys)  length xs = length ys" (* TODO: Extraction should also go to elements! *)  
    unfolding list_assn_def
    apply (vcg_prepare_external)
    by (auto)
    

  definition "oelem_assn A  mk_assn (λNone  λ_.  | Some x  λxi. A x xi)"

  lemma oelem_assn_simps[simp]:
    "(oelem_assn A) None xi = "
    "(oelem_assn A) (Some x) xi = A x xi"  
    unfolding oelem_assn_def by auto


  lemma split_list_according:
    assumes "xs = xs1@x#xs2"
    assumes "length ys = length xs"
    obtains ys1 y ys2 where "ys = ys1@y#ys2" "length ys1 = length xs1" "length ys2 = length xs2"
      using assms
      apply (subst (asm) id_take_nth_drop[of "length xs1" ys])
      by auto
  

  lemma lo_focus_elem_gen:
    assumes "i<length xs" "xs!i = Some x"  
    shows "(list_assn (oelem_assn A)) xs ys = ((A x (ys!i)) ** (list_assn (oelem_assn A)) (xs[i:=None]) (ys[i:=anything]))"
  proof (cases "length ys = length xs")
    case [simp]: True
    
    obtain xs1 xs2 where XSF[simp]: "xs = xs1@Some x#xs2" and [simp]: "i = length xs1" 
      using id_take_nth_drop[OF assms(1)] assms(2) by fastforce
    obtain ys1 y ys2 where [simp]: "ys = ys1@y#ys2" "length ys1 = length xs1" "length ys2 = length xs2"
      using split_list_according[OF XSF True] .
      
    show ?thesis
      by (simp add: nth_append list_update_append sep_algebra_simps sep_conj_c)
      
  qed simp
      
  text Extract element from list assertion
  lemma lo_extract_elem:
    assumes "i<length xs" "xs!i = Some x"  
    shows "(list_assn (oelem_assn A)) xs ys = ((A x (ys!i)) ** (list_assn (oelem_assn A)) (xs[i:=None]) ys)"
    by (metis list_update_id lo_focus_elem_gen[OF assms])
    
  
  text Insert element into list assertion  
  lemma lo_insert_elem:
    assumes "i<length xs" "xs!i = None"
    shows "(list_assn (oelem_assn A)) (xs[i:=Some x]) (ys[i:=y]) = (A x y ** (list_assn (oelem_assn A)) xs ys)"
    apply (cases "length ys = length xs")
    using lo_focus_elem_gen[of i "xs[i:=Some x]" x A "ys[i:=y]" "ys!i"] using assms
    apply simp_all
    by (metis list_update_id)
    
  
  definition "nao_assn A  mk_assn (λxs p. EXS xsi. narray_assn xsi p ** (list_assn (oelem_assn A)) xs xsi)"

  
  lemma nao_nth_rule[vcg_rules]: "llvm_htriple 
    ((nao_assn A) xs p ∧* snat.assn i ii ∧* d(i < length xs  xs!iNone)) 
    (array_nth p ii)
    (λri. A (the (xs!i)) ri ∧* (nao_assn A) (xs[i:=None]) p)"  
    unfolding nao_assn_def
    supply [simp] = lo_extract_elem
    apply vcg'
    done
  
  
  lemma nao_upd_rule_snat[vcg_rules]: "llvm_htriple 
    ((nao_assn A) xs p ∧* A x xi ∧* snat.assn i ii ∧* d(i < length xs  xs!i=None)) 
    (array_upd p ii xi)
    (λr. (r = p) ∧* (nao_assn A) (xs[i := Some x]) p)"
    unfolding nao_assn_def 
    supply [simp] = lo_insert_elem
    apply vcg'
    done

    
    
  definition "sao_assn A  mk_assn (λxs p. EXS xsi. array_slice_assn xsi p ** (list_assn (oelem_assn A)) xs xsi)"

  
  lemma sao_nth_rule[vcg_rules]: "llvm_htriple 
    ((sao_assn A) xs p ∧* snat.assn i ii ∧* d(i < length xs  xs!iNone)) 
    (array_nth p ii)
    (λri. A (the (xs!i)) ri ∧* (sao_assn A) (xs[i:=None]) p)"  
    unfolding sao_assn_def
    supply [simp] = lo_extract_elem
    apply vcg'
    done
  
  
  lemma sao_upd_rule_snat[vcg_rules]: "llvm_htriple 
    ((sao_assn A) xs p ∧* A x xi ∧* snat.assn i ii ∧* d(i < length xs  xs!i=None)) 
    (array_upd p ii xi)
    (λr. (r = p) ∧* (sao_assn A) (xs[i := Some x]) p)"
    unfolding sao_assn_def 
    supply [simp] = lo_insert_elem
    apply vcg'
    done
    
    
        
(*
  xxx, ctd here: new, free, then integrate into sepref!   
    XXX: First integrate into sepref, than care about new and free.
      for sorting algos, we only need get and set!
        
*)    
    
    
    
        
  
end