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"
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 :
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
end