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) (xs⇩1@xs⇩2) yys = (EXS ys⇩1 ys⇩2. ↑(yys=ys⇩1@ys⇩2) ** ↿(list_assn A) xs⇩1 ys⇩1 ** ↿(list_assn A) xs⇩2 ys⇩2)"
    apply (induction xs⇩1 arbitrary: yys)
    by (auto simp: sep_algebra_simps list_assn_cons1_conv)
  
  lemma list_assn_append2_conv: "↿(list_assn A) xxs (ys⇩1@ys⇩2) = (EXS xs⇩1 xs⇩2. ↑(xxs=xs⇩1@xs⇩2) ** ↿(list_assn A) xs⇩1 ys⇩1 ** ↿(list_assn A) xs⇩2 ys⇩2)"
    apply (induction ys⇩1 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 xs⇩1 = length ys⇩1 
    ⟹ ↿(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)"  
    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 = xs⇩1@x#xs⇩2"
    assumes "length ys = length xs"
    obtains ys⇩1 y ys⇩2 where "ys = ys⇩1@y#ys⇩2" "length ys⇩1 = length xs⇩1" "length ys⇩2 = length xs⇩2"
      using assms
      apply (subst (asm) id_take_nth_drop[of "length xs⇩1" 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 xs⇩1 xs⇩2 where XSF[simp]: "xs = xs⇩1@Some x#xs⇩2" and [simp]: "i = length xs⇩1" 
      using id_take_nth_drop[OF assms(1)] assms(2) by fastforce
    obtain ys⇩1 y ys⇩2 where [simp]: "ys = ys⇩1@y#ys⇩2" "length ys⇩1 = length xs⇩1" "length ys⇩2 = length xs⇩2"
      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!i≠None)) 
    (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!i≠None)) 
    (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