Theory Sep_Value_RS
section ‹Reasoning about Values›
theory Sep_Value_RS
imports Sep_Lift "../basic/LLVM_Basic_Main"
begin
subsection ‹Lifting Scheme on Maps›
definition "prefix_map1 i m ≡ λ[] ⇒ None | i'#as ⇒ if i=i' then m as else None"
definition "project_map1 i m ≡ λa. m (i#a)"
definition "carve_map1 i m ≡ λ[] ⇒ m [] | i'#a ⇒ if i=i' then None else m (i'#a)"
definition "prefix_adom1 va d = (#)va`d"
lemma prefix_map1_apply: "prefix_map1 i m xs = (case xs of [] ⇒ None | j#as ⇒ if i=j then m as else None)"
by (auto simp: prefix_map1_def)
lemma project_map1_apply: "project_map1 i m xs = m (i#xs)"
by (auto simp: project_map1_def)
lemmas lift_map_apply = prefix_map1_apply project_map1_apply
lemma prefix_map1_empty[simp]:
"prefix_map1 i Map.empty = Map.empty"
"prefix_map1 i m = Map.empty ⟷ m=Map.empty"
by (auto simp: prefix_map1_def fun_eq_iff split: if_splits list.splits)
lemma prefix_map1_add_distrib[simp]: "prefix_map1 i (a⇩1 ++ a⇩2) = prefix_map1 i a⇩1 ++ prefix_map1 i a⇩2"
apply (rule ext)
by (auto simp: prefix_map1_def map_add_def split: list.splits option.splits)
lemma prefix_map_complete_eq_iff[simp]:
"prefix_map1 PFST a ++ prefix_map1 PSND b = prefix_map1 PFST a' ++ prefix_map1 PSND b'
⟷ a=a' ∧ b=b'"
apply (auto simp: fun_eq_iff map_add_def prefix_map1_def split: option.split list.split)
by (metis option.exhaust va_item.distinct(1))
lemma project_map1_empty[simp]: "project_map1 i Map.empty = Map.empty"
by (auto simp: project_map1_def)
lemma dom_project_map1_iff[simp]: "dom (project_map1 i b) = { a. i#a ∈ dom b}"
by (auto simp: project_map1_def)
lemma project_map_add_distrib[simp]: "project_map1 i (b⇩1 ++ b⇩2) = project_map1 i b⇩1 ++ project_map1 i b⇩2"
apply (rule ext)
by (auto simp: project_map1_def map_add_def)
lemma project_map_prefix_id[simp]: "project_map1 i (prefix_map1 i a) = a"
apply (rule ext)
by (auto simp: project_map1_def prefix_map1_def)
lemma carve_map1_empty[simp]:
"carve_map1 i Map.empty = Map.empty"
by (rule ext) (auto simp: carve_map1_def split: list.splits)
lemma carve_map1_dom[simp]: "dom (carve_map1 i v) = dom v - {i # as |as. True}"
by (auto simp: carve_map1_def split: list.splits if_splits)
lemma carve_map_add_distrib[simp]: "carve_map1 i (b⇩1 ++ b⇩2) = carve_map1 i b⇩1 ++ carve_map1 i b⇩2"
apply (rule ext)
by (auto simp: carve_map1_def map_add_def split: list.splits if_splits)
lemma project_carve_empty[simp]: "project_map1 i (carve_map1 i b) = Map.empty"
apply (rule ext)
by (auto simp: carve_map1_def project_map1_def split: list.splits if_splits)
lemma carve_prefix_empty[simp]: "carve_map1 i (prefix_map1 i a) = Map.empty"
apply (rule ext)
by (auto simp: carve_map1_def prefix_map1_def split: list.splits if_splits)
lemma prefix_adom_empty[simp]:
"prefix_adom1 i {} = {}"
by (auto simp: prefix_adom1_def)
lemma prefix_adom_empty_iff[simp]:
"prefix_adom1 i d = {} ⟷ d={}"
by (auto simp: prefix_adom1_def)
lemma prefix_adom_insert[simp]:
"prefix_adom1 i (insert d e) = insert (i#d) (prefix_adom1 i e)"
by (auto simp: prefix_adom1_def)
lemma prefix_adom_union[simp]:
"prefix_adom1 i (d∪e) = prefix_adom1 i d ∪ prefix_adom1 i e"
by (auto simp: prefix_adom1_def)
lemma in_prefix_adom_conv[simp]:
"x∈prefix_adom1 i d ⟷ (∃va'∈d. x=i#va')"
by (auto simp: prefix_adom1_def)
lemma prefix_map1_dom[simp]: "dom (prefix_map1 i m) = prefix_adom1 i (dom m)"
by (auto simp: prefix_map1_def split: list.splits if_splits)
lemma map1_split_complete: "prefix_map1 i (project_map1 i b) ++ carve_map1 i b = b"
apply (rule ext)
apply (auto simp: prefix_map1_def project_map1_def carve_map1_def map_add_def split: list.splits option.splits)
done
lemma project_map1_prefix_diff[simp]: "i≠j ⟹ project_map1 i (prefix_map1 j a) = Map.empty"
apply (rule ext)
apply (auto simp: project_map1_def prefix_map1_def)
done
lemma carve_map1_prefix_diff[simp]: "i≠j ⟹ carve_map1 i (prefix_map1 j a) = prefix_map1 j a"
apply (rule ext)
apply (auto simp: prefix_map1_def carve_map1_def split: list.splits)
done
subsection ‹Independence of Addresses›
lemma lens_of_item_indepI: "i≠i' ⟹ lens_of_item i ⨝ lens_of_item i'"
apply (cases i; cases i')
apply (simp_all add: lens_indep_sym)
done
lemma lens_of_item_indepD: "lens_of_item i ⨝ lens_of_item i' ⟹ i≠i'"
apply (cases i; cases i')
apply (simp_all add: lens_indep_sym)
apply (meson hlens_def lens.pre_get_imp_putI rnl_indep_not_refl rnlensI val.discI(1) val.distinct(1) val.fst⇩L_lens val.fst⇩L_pre_disc)
by (meson hlens_def lens.pre_get_imp_putI rnl_indep_not_refl rnlensI val.discI(1) val.distinct(1) val.snd⇩L_lens val.snd⇩L_pre_disc)
lemma lens_of_item_indep_eq[simp]: "lens_of_item i ⨝ lens_of_item i' ⟷ i≠i'"
using lens_of_item_indepI lens_of_item_indepD by blast
definition "vaddr_indep va va' ⟷ (lens_of_vaddr va :: unit val ⟹ _) ⨝ lens_of_vaddr va'"
lemma "¬(lens_of_vaddr [] ⨝ lens_of_vaddr va)" by simp
lemma "¬(lens_of_vaddr va ⨝ lens_of_vaddr [])" by simp
lemma lens_of_vaddr_indep_Cons: "(lens_of_vaddr (i#is) :: 'a val ⟹ _) ⨝ lens_of_vaddr (j#js)
⟷ i≠j ∨ (lens_of_vaddr is :: 'a val ⟹ _) ⨝ lens_of_vaddr js"
apply (cases "i=j")
by (auto simp: lens_indep_extend2)
lemma lens_of_vaddr_indep_normalize:
assumes "NO_MATCH TYPE(unit) TYPE('a)"
shows "lens_of_vaddr va ⨝ (lens_of_vaddr va' :: 'a val ⟹ _) ⟷ lens_of_vaddr va ⨝ (lens_of_vaddr va' :: unit val ⟹ _)"
proof (induction va arbitrary: va')
case Nil
then show ?case by auto
next
case (Cons a va)
then show ?case
apply (cases va')
apply simp
apply (simp only: lens_of_vaddr_indep_Cons)
done
qed
lemma vaddr_indep_alt: "vaddr_indep a b ⟷ lens_of_vaddr a ⨝ lens_of_vaddr b"
using lens_of_vaddr_indep_normalize vaddr_indep_def by auto
lemma vaddr_indep_irrefl[simp, intro!]: "¬vaddr_indep a a"
unfolding vaddr_indep_def by auto
lemma vaddr_indep_sym: "vaddr_indep a b ⟹ vaddr_indep b a"
unfolding vaddr_indep_def
using lens_indep_sym by auto
lemma vaddr_indep_Nil:
"¬vaddr_indep [] va"
"¬vaddr_indep va []"
by (simp_all add: vaddr_indep_def)
lemma vaddr_indep_Cons:
"vaddr_indep (a#va⇩1) (b#va⇩2) ⟷ (a≠b ∨ vaddr_indep va⇩1 va⇩2)"
using lens_of_vaddr_indep_Cons vaddr_indep_def by auto
lemmas vaddr_indep_simps[simp] = vaddr_indep_Nil vaddr_indep_Cons
lemma vaddr_indep_prefix[simp]: "vaddr_indep (va@va⇩1) (va@va⇩2) ⟷ vaddr_indep va⇩1 va⇩2"
by (induction va) auto
definition "s_indep s1 s2 ≡ ∀x∈s1. ∀y∈s2. vaddr_indep x y"
lemma s_indep_irrefl[simp]: "s_indep m m ⟷ m={}"
by (force simp: s_indep_def)
lemma s_indep_sym: "s_indep s1 s2 ⟹ s_indep s2 s1"
by (auto simp: s_indep_def vaddr_indep_sym)
lemma s_indep_imp_disj: "s_indep s1 s2 ⟹ s1 ∩ s2 = {}"
by (force simp: s_indep_def)
lemma s_indep_simps[simp]:
"s_indep {} s"
"s_indep s {}"
"s_indep (insert x s) r ⟷ (∀y∈r. vaddr_indep x y) ∧ s_indep s r"
"s_indep r (insert x s) ⟷ (∀y∈r. vaddr_indep y x) ∧ s_indep r s"
by (auto simp: s_indep_def)
lemma s_indep_union[simp]:
"s_indep (a∪b) c ⟷ s_indep a c ∧ s_indep b c"
"s_indep a (b∪c) ⟷ s_indep a b ∧ s_indep a c"
by (auto simp: s_indep_def)
lemma s_indep_ne[simp, intro]:
"[]∈s⇩1 ⟹ s_indep s⇩1 s⇩2 ⟷ s⇩2={}"
"[]∈s⇩2 ⟹ s_indep s⇩1 s⇩2 ⟷ s⇩1={}"
by (all ‹force simp: s_indep_def›)
lemma s_indep_projectI: "s_indep s⇩1 s⇩2 ⟹ s_indep {a. i # a ∈ s⇩1} {a. i # a ∈ s⇩2}"
apply (auto simp: s_indep_def)
using vaddr_indep_Cons by blast
lemma s_indep_mono: "s_indep s⇩1 s⇩2 ⟹ s⇩1'⊆s⇩1 ⟹ s⇩2'⊆s⇩2 ⟹ s_indep s⇩1' s⇩2'"
by (auto simp: s_indep_def)
lemma s_indep_Cons[simp]: "s_indep (prefix_adom1 a s⇩1) (prefix_adom1 b s⇩2) ⟷ a≠b ∨ s_indep s⇩1 s⇩2"
by (auto simp: s_indep_def prefix_adom1_def)
lemma s_indep_project_shift_prefix:
"⟦[] ∉ dom b; s_indep (dom a) (dom (project_map1 i b))⟧
⟹ s_indep (dom (prefix_map1 i a)) (dom b)"
apply (clarsimp simp: s_indep_def)
by (metis domI neq_Nil_conv option.distinct(1) vaddr_indep_Cons vaddr_indep_sym)
lemma s_indep_carve_prefix:
"[] ∉ dom b ⟹ s_indep (dom (carve_map1 i b)) (dom (prefix_map1 i a))"
apply (clarsimp simp: s_indep_def)
by (metis neq_Nil_conv option.distinct(1) vaddr_indep_Cons)
subsection ‹Separation Algebra for Values›
typedef 'a aval = "{ m :: vaddr ⇀ 'a. ∀va∈dom m. ∀va'∈dom m. va≠va' ⟶ vaddr_indep va va' }" by auto
setup_lifting type_definition_aval
instantiation aval :: (type) unique_zero_sep_algebra
begin
lift_definition sep_disj_aval :: "'a aval ⇒ 'a aval ⇒ bool" is "λx y. s_indep (dom x) (dom y)" .
lift_definition plus_aval :: "'a aval ⇒ 'a aval ⇒ 'a aval" is "λm1 m2. if s_indep (dom m1) (dom m2) then m1 ++ m2 else Map.empty"
apply (auto split: if_splits simp: s_indep_def) apply blast apply blast
by (meson domI vaddr_indep_sym)
lift_definition zero_aval :: "'a aval" is "Map.empty" by simp
instance
apply standard
apply (determ transfer; auto simp: s_indep_def)
apply (determ transfer; auto simp: s_indep_def dom_def; metis vaddr_indep_sym)
apply (determ transfer; auto simp: s_indep_def)
apply (determ transfer; auto simp: s_indep_imp_disj simp: map_add_comm s_indep_sym)
apply (determ transfer; clarsimp; meson UnE s_indep_def)
apply (determ transfer; unfold s_indep_def; auto simp: domI)
apply (determ transfer; simp)
done
end
subsection ‹Lifting Scheme on ‹aval››
lift_definition prefix_aval1 :: "va_item ⇒ 'a aval ⇒ 'a aval" is prefix_map1 by auto auto
lift_definition prim_aval :: "'a ⇒ 'a aval" is "λx. [[] ↦ x]" by simp
lift_definition adom :: "'a aval ⇒ vaddr set" is "dom" .
lift_definition project_aval1 :: "va_item ⇒ 'a aval ⇒ 'a aval" is project_map1
apply (auto simp: project_map1_def)
by (meson domI list.inject vaddr_indep_Cons)
lift_definition carve_aval1 :: "va_item ⇒ 'a aval ⇒ 'a aval" is carve_map1
by (fastforce simp: carve_map1_def split: list.splits if_splits)
lemma indep_prefix_aux1: "[]∉dom b ⟹ s_indep (prefix_adom1 i {a. i # a ∈ dom b}) (dom b - {as'. ∃as. as' = i # as})"
apply (auto simp: prefix_adom1_def s_indep_def)
by (metis neq_Nil_conv option.distinct(1) vaddr_indep_Cons)
lemma carve_indep_id_aux1: "⟦∀va∈dom i. ∀va'∈dom i. va ≠ va' ⟶ vaddr_indep va va'; ¬ [] ∉ dom i⟧ ⟹ carve_map1 b i = i"
apply (rule ext)
apply (auto simp: carve_map1_def split: list.split)
by (metis domIff list.distinct(1) option.distinct(1) vaddr_indep_simps(1))
interpretation aval_lifting_scheme: sep_lifting_scheme "prefix_aval1 i" "project_aval1 i" "carve_aval1 i" "λx. []∉adom x"
apply unfold_locales
apply (all ‹determ transfer›)
apply (all ‹(simp;fail)?›)
subgoal by (auto simp: domI) []
subgoal by (auto ) []
subgoal by (auto simp: domI s_indep_projectI) []
subgoal by (auto simp: domI s_indep_projectI) []
subgoal by (auto intro: s_indep_mono)
subgoal by (auto intro: s_indep_mono)
subgoal by (rule s_indep_project_shift_prefix)
subgoal by (rule s_indep_carve_prefix)
subgoal by (auto simp: map1_split_complete indep_prefix_aux1) []
subgoal by (auto simp: carve_indep_id_aux1)
done
subsubsection ‹Additional Lemmas›
lemma adomZ[simp]: "adom 0 = {}"
apply transfer by auto
lemma adom_Z_iff[simp]: "adom v = {} ⟹ v = 0"
by (determ transfer) auto
lemma disj_eq_adom: "a##b ⟷ s_indep (adom a) (adom b)"
apply transfer by (auto simp: s_indep_def)
lemma adom_plus[simp]: "a##b ⟹ adom (a+b) = adom a ∪ adom b"
apply transfer by auto
lemma adom_primval[simp]: "adom (prim_aval x) = {[]}"
apply transfer by auto
lemma adom_prefix[simp]: "adom (prefix_aval1 i v) = (prefix_adom1 i (adom v))"
by (determ transfer) auto
lemma aval_project_prefix_diff[simp]: "i≠j ⟹ project_aval1 i (prefix_aval1 j a) = 0"
apply transfer by auto
lemma carve_aval_prefix_diff[simp]: "i≠j ⟹ carve_aval1 i (prefix_aval1 j a) = prefix_aval1 j a"
apply transfer by auto
lemma adom_cases: obtains (primitive) "adom a = {[]}" | (compound) "[]∉adom a"
by transfer force
lemma va_item_complete:
"i≠PFST ⟹ i=PSND"
"i≠PSND ⟹ i=PFST"
"PFST≠i ⟹ i=PSND"
"PSND≠i ⟹ i=PFST"
by (all ‹cases i; auto›)
lemma aval_cases:
obtains (primitive) x where "v = prim_aval x"
| (compound) v⇩1 v⇩2 where "v = prefix_aval1 PFST v⇩1 + prefix_aval1 PSND v⇩2"
proof -
have "(∃x. v = prim_aval x) ∨ (∃v⇩1 v⇩2. v = prefix_aval1 PFST v⇩1 + prefix_aval1 PSND v⇩2)"
proof (transfer, goal_cases)
case (1 v)
assume INDEP: "∀vaa∈dom v. ∀va'∈dom v. vaa ≠ va' ⟶ vaddr_indep vaa va'"
then consider (primitive) "dom v = {[]}" | (compound) "[]∉dom v" by force
then show ?case proof cases
case primitive
then show ?thesis
apply (rule_tac disjI1)
by (simp add: dom_eq_singleton_conv)
next
case compound
then show ?thesis
apply (rule_tac disjI2)
apply (rule bexI[where x="project_map1 PFST v"])
apply (rule bexI[where x="project_map1 PSND v"])
subgoal
apply (rule ext)
subgoal for x
apply (cases x)
apply (auto simp add: map_add_def lift_map_apply dest: va_item_complete split: option.splits)
done
done
using INDEP
apply clarsimp_all
apply (meson domI list.inject vaddr_indep_Cons)+
done
qed
qed
thus ?thesis using that by blast
qed
lemma prim_aval_complete[simp]:
"prim_aval x ## v ⟷ v=0"
"v ## prim_aval x ⟷ v=0"
by (auto simp: disj_eq_adom)
lemma prim_aval_neqZ[simp]: "prim_aval x ≠ 0"
by (metis adomZ adom_primval empty_iff insert_iff)
lemma prefix_aval_complete_eq_iff[simp]:
"prefix_aval1 PFST a + prefix_aval1 PSND b = prefix_aval1 PFST a' + prefix_aval1 PSND b'
⟷ a=a' ∧ b=b'"
apply transfer
apply auto
done
lemma prefix_aval_split_ne_prim: "prefix_aval1 PFST a + prefix_aval1 PSND b ≠ prim_aval x"
proof -
have "adom (prefix_aval1 PFST a + prefix_aval1 PSND b) ≠ {[]}"
by (metis aval_lifting_scheme.carve_disj_lift(2) aval_lifting_scheme.splittable_add_distrib aval_lifting_scheme.splittable_lift carve_aval_prefix_diff insertI1 va_item.distinct(1))
then show ?thesis
by (rule_tac ccontr; simp)
qed
lemma prim_aval_inj[simp]: "prim_aval x = prim_aval y ⟷ x = y"
apply transfer
apply (auto simp: fun_eq_iff split: if_splits)
done
subsection ‹Lifter for Value Address Items›
fun val_dom where
"val_dom (PRIMITIVE x) = {[]}"
| "val_dom (PAIR x y) = prefix_adom1 PFST (val_dom x) ∪ prefix_adom1 PSND (val_dom y)"
fun val_α where
"val_α (PRIMITIVE x) = prim_aval x"
| "val_α (PAIR x y) = prefix_aval1 PFST (val_α x) + prefix_aval1 PSND (val_α y)"
lemma ne_prefix_disjI[simp, intro]: "i≠j ⟹ prefix_aval1 i v⇩1 ## prefix_aval1 j v⇩2"
by (auto simp add: disj_eq_adom)
lemma adom_val_α[simp]: "adom (val_α x) = val_dom x"
by (induction x) (auto)
definition "val_item_lifter i ≡ ⦇
sep_lifter.lift = prefix_aval1 i,
sep_lifter.project = project_aval1 i,
sep_lifter.carve = carve_aval1 i,
sep_lifter.splittable = λa. [] ∉ adom a,
sep_lifter.L = lens_of_item i,
sep_lifter.αb = val_α,
sep_lifter.αs = val_α,
sep_lifter.tyb = λ_. (),
sep_lifter.tys = λ_. ()
⦈"
lemma val_item_lifter_simps[simp]:
"sep_lifter.lift (val_item_lifter i) = prefix_aval1 i"
"sep_lifter.project (val_item_lifter i) = project_aval1 i"
"sep_lifter.carve (val_item_lifter i) = carve_aval1 i"
"sep_lifter.splittable (val_item_lifter i) = (λa. [] ∉ adom a)"
"sep_lifter.L (val_item_lifter i) = lens_of_item i"
"sep_lifter.αb (val_item_lifter i) = val_α"
"sep_lifter.αs (val_item_lifter i) = val_α"
"sep_lifter.tyb (val_item_lifter i) = (λ_. ())"
"sep_lifter.tys (val_item_lifter i) = (λ_. ())"
by (auto simp: val_item_lifter_def)
lemma val_item_lifter[simp, intro!]: "sep_lifter (val_item_lifter i)"
apply intro_locales
subgoal by (simp add: val_item_lifter_def) unfold_locales
subgoal
apply (rule sep_lifter_axioms.intro)
apply (clarsimp_all simp: val_item_lifter_def)
subgoal for cb by (cases cb; cases i) auto
subgoal for cb
apply (cases cb; cases i)
apply (auto simp: )
done
subgoal for cb x
apply (cases cb; cases i)
apply (auto simp: sep_algebra_simps)
done
done
done
lemma val_α_neqZ[simp]: "val_α x ≠ 0"
by (induction x) auto
lemma val_α_complete[simp]: "val_α v ## x ⟷ x=0"
proof (induction v arbitrary: x)
case (PAIR v1 v2)
show ?case
apply (cases x rule: aval_cases)
apply (auto simp: PAIR.IH)
done
next
case (PRIMITIVE y)
then show ?case
by (cases x rule: aval_cases) auto
qed
lemma val_α_inj[simp]: "val_α v = val_α v' ⟷ v=v'"
proof (induction v arbitrary: v')
case (PAIR v1 v2)
then show ?case
by (cases v') (auto simp: prefix_aval_split_ne_prim)
next
case (PRIMITIVE x)
then show ?case
apply (cases v')
apply auto
by (metis prefix_aval_split_ne_prim)
qed
subsection ‹Lifter for Value Addresses›
definition "vaddr_lifter addr = foldr (λi l. l ∙⇩l⇩f⇩t val_item_lifter i) addr (id_lifter (λ_. ()) val_α)"
lemma vaddr_lifter_rec_simps:
"vaddr_lifter [] = id_lifter (λ_. ()) val_α"
"vaddr_lifter (i#a) = vaddr_lifter a ∙⇩l⇩f⇩t val_item_lifter i"
unfolding vaddr_lifter_def by auto
lemma vaddr_lifter_αs_simp: "sep_lifter.αs (vaddr_lifter addr) = val_α"
apply (induction addr) apply (auto simp: vaddr_lifter_rec_simps compose_lifter_simps) done
lemma vaddr_lifter_αb_simp: "sep_lifter.αb (vaddr_lifter addr) = val_α"
apply (induction addr) apply (auto simp: vaddr_lifter_rec_simps compose_lifter_simps) done
lemma vaddr_lifter_L_simp: "sep_lifter.L (vaddr_lifter addr) = lens_of_vaddr addr"
apply (induction addr)
apply (auto simp: vaddr_lifter_rec_simps compose_lifter_simps)
done
lemmas vaddr_lifter_simps[simp] = vaddr_lifter_αs_simp vaddr_lifter_αb_simp vaddr_lifter_L_simp
lemma vaddr_lifter[simp, intro!]: "sep_lifter (vaddr_lifter addr)"
apply (induction addr) apply (auto simp: vaddr_lifter_rec_simps compose_lifter_simps) done
interpretation val_item_lifter: sep_lifter "val_item_lifter i" for i by simp
interpretation vaddr_lifter: sep_lifter "vaddr_lifter addr" for addr by simp
lemma vaddr_lift_Nil[simp]: "vaddr_lifter.lift [] = id"
by (auto simp: vaddr_lifter_def id_lifter_def)
lemma vaddr_lift_Cons[simp]: "vaddr_lifter.lift (i#as) = prefix_aval1 i o vaddr_lifter.lift as"
apply (rule ext)
apply (auto simp: vaddr_lifter_rec_simps compose_lifter_simps)
done
lemma vaddr_lift_append[simp]: "vaddr_lifter.lift (as⇩1@as⇩2) = vaddr_lifter.lift as⇩1 o vaddr_lifter.lift as⇩2"
by (induction as⇩1) auto
subsection ‹Points-To Assertion for Values›
definition "vpto_assn v addr ≡ vaddr_lifter.lift_assn addr (EXACT (val_α v))"
lemma vpto_assn_split: "vpto_assn (PAIR a b) addr = (vpto_assn a (addr@[PFST]) ** vpto_assn b (addr@[PSND]))"
by (auto simp: vpto_assn_def EXACT_split)
lemma vpto_assn_notZ[simp]: "¬ vpto_assn x a 0"
by (auto simp: vpto_assn_def)
lemma vpto_assn_this[simp]: "vpto_assn v [] av = (av = val_α v)"
by (auto simp: vpto_assn_def)
subsection ‹Hoare-Triples for Load and Store›
lemma get_aval_rule: "notime.htriple val_α (EXACT (val_α v)) Monad.get (λr. ↑(r=v) ** EXACT (val_α v))"
apply (rule notime.htripleI')
apply (auto simp: wpn_def run_simps)
apply (auto simp: sep_algebra_simps)
done
lemma set_aval_rule: "notime.htriple val_α (EXACT (val_α v)) (Monad.set v') (λ_. EXACT (val_α v'))"
apply (rule notime.htripleI')
apply (auto simp: wpn_def run_simps)
done
lemma vload_rule: "notime.htriple val_α (vpto_assn v a) (vload err a) (λr. ↑(r=v) ** vpto_assn v a)"
unfolding vload_def vpto_assn_def
apply (rule notime.cons_post_rule)
apply (rule vaddr_lifter.lift_operation[simplified])
apply simp
apply (rule get_aval_rule)
by auto
lemma vstore_rule: "notime.htriple val_α (vpto_assn v a) (vstore err v' a) (λ_. vpto_assn v' a)"
unfolding vstore_def vpto_assn_def
apply (rule notime.cons_post_rule)
apply (rule vaddr_lifter.lift_operation[simplified])
apply simp
apply (rule set_aval_rule)
by auto
lifting_forget aval.lifting
end