Theory CombinableWands
section ‹Combinable Magic Wands›
text ‹Note that, in this theory, assertions are represented as semantic assertions, i.e., as the set of states in which they hold.›
theory CombinableWands
imports PartialHeapSA
begin
subsection ‹Definitions›
type_synonym sem_assertion = "state set"
fun multiply :: "prat ⇒ state ⇒ state" where
"multiply p φ = Abs_state (multiply_mask p (get_m φ), get_h φ)"
text ‹Because we work in an intuitionistic setting, a fraction of an assertion is defined using the upper-closure operator.›
fun multiply_sem_assertion :: "prat ⇒ sem_assertion ⇒ sem_assertion" where
"multiply_sem_assertion p P = PartialSA.upper_closure (multiply p ` P)"
definition combinable :: "sem_assertion ⇒ bool" where
"combinable P ⟷ (∀α β. ppos α ∧ ppos β ∧ pgte pwrite (padd α β) ⟶ (multiply_sem_assertion α P) ⊗ (multiply_sem_assertion β P) ⊆ multiply_sem_assertion (padd α β) P)"
definition scaled where
"scaled φ = { multiply p φ |p. ppos p ∧ pgte pwrite p }"
definition comp_min_mask :: "mask ⇒ (mask ⇒ mask)" where
"comp_min_mask b a hl = pmin (a hl) (comp_one (b hl))"
definition scalable where
"scalable w a ⟷ (∀φ ∈ scaled w. ¬ a |#| φ)"
definition R where
"R a w = (if scalable w a then w else Abs_state (comp_min_mask (get_m a) (get_m w), get_h w))"
definition cwand where
"cwand A B = { w |w. ∀a x. a ∈ A ∧ Some x = R a w ⊕ a ⟶ x ∈ B }"
definition wand :: "sem_assertion ⇒ sem_assertion ⇒ sem_assertion" where
"wand A B = { w |w. ∀a x. a ∈ A ∧ Some x = w ⊕ a ⟶ x ∈ B }"
definition intuitionistic where
"intuitionistic A ⟷ (∀a b. a ≽ b ∧ b ∈ A ⟶ a ∈ A)"
definition binary_mask :: "mask ⇒ mask" where
"binary_mask π l = (if π l = pwrite then pwrite else pnone)"
definition binary :: "sem_assertion ⇒ bool" where
"binary A ⟷ (∀φ ∈ A. Abs_state (binary_mask (get_m φ), get_h φ) ∈ A)"
subsection Lemmas
lemma wand_equiv_def:
"wand A B = { φ |φ. A ⊗ {φ} ⊆ B }"
proof
show "wand A B ⊆ {φ |φ. A ⊗ {φ} ⊆ B}"
proof
fix w assume "w ∈ wand A B"
have "A ⊗ {w} ⊆ B"
proof
fix x assume "x ∈ A ⊗ {w}"
then show "x ∈ B"
using PartialSA.add_set_elem ‹w ∈ wand A B› commutative wand_def by auto
qed
then show "w ∈ {φ |φ. A ⊗ {φ} ⊆ B}"
by simp
qed
show "{φ |φ. A ⊗ {φ} ⊆ B} ⊆ wand A B"
proof
fix w assume "w ∈ {φ |φ. A ⊗ {φ} ⊆ B}"
have "⋀a x. a ∈ A ∧ Some x = w ⊕ a ⟹ x ∈ B"
proof -
fix a x assume "a ∈ A ∧ Some x = w ⊕ a"
then have "x ∈ A ⊗ {w}"
using PartialSA.add_set_elem PartialSA.commutative by auto
then show "x ∈ B"
using ‹w ∈ {φ |φ. A ⊗ {φ} ⊆ B}› by blast
qed
then show "w ∈ wand A B"
using wand_def by force
qed
qed
lemma w_in_scaled:
"w ∈ scaled w"
proof -
have "multiply pwrite w = w"
by (simp add: Rep_state_inverse mult_write_mask)
then show ?thesis
by (metis (mono_tags, lifting) half_between_0_1 half_plus_half mem_Collect_eq not_pgte_charact pgt_implies_pgte ppos_add scaled_def)
qed
lemma non_scalable_instantiate:
assumes "¬ scalable w a"
shows "∃p. ppos p ∧ pgte pwrite p ∧ a |#| multiply p w"
using assms scalable_def scaled_def by auto
lemma compatible_same_mask:
assumes "valid_mask (add_masks a w)"
shows "w = comp_min_mask a w"
proof (rule ext)
fix x
have "pgte pwrite (padd (a x) (w x))"
by (metis add_masks.simps assms valid_mask.elims(1))
moreover have "padd (a x) (comp_one (a x)) = pwrite"
by (meson assms padd_comp_one upper_valid_aux valid_mask.elims(1))
then have "pgte (comp_one (a x)) (w x)"
by (metis add_le_cancel_left calculation padd.rep_eq pgte.rep_eq)
then show "w x = comp_min_mask a w x"
by (metis comp_min_mask_def pmin_comm pmin_is)
qed
lemma R_smaller:
"w ≽ R a w"
proof (cases "scalable w a")
case True
then show ?thesis
by (simp add: PartialSA.succ_refl R_def)
next
case False
then have "R a w = Abs_state (comp_min_mask (get_m a) (get_m w), get_h w)"
by (meson R_def)
moreover have "greater_mask (get_m w) (comp_min_mask (get_m a) (get_m w))"
proof (rule greater_maskI)
fix hl show "pgte (get_m w hl) (comp_min_mask (get_m a) (get_m w) hl)"
by (simp add: comp_min_mask_def pmin_greater)
qed
ultimately show ?thesis
by (metis Abs_state_cases larger_heap_refl Rep_state_cases Rep_state_inverse fst_conv get_h_m greaterI greater_mask_def mem_Collect_eq snd_conv valid_state_decompose)
qed
lemma R_compatible_same:
assumes "a |#| w"
shows "R a w = w"
proof -
have "¬ scalable w a"
using assms scalable_def w_in_scaled by blast
then have "R a w = Abs_state (comp_min_mask (get_m a) (get_m w), get_h w)"
using R_def by auto
then show ?thesis
by (metis PartialSA.defined_def Rep_state_inverse assms compatible_same_mask get_h.simps get_m.simps plus_ab_defined prod.collapse)
qed
lemma in_cwand:
assumes "⋀a x. a ∈ A ∧ Some x = R a w ⊕ a ⟹ x ∈ B"
shows "w ∈ cwand A B"
using assms cwand_def by force
lemma wandI:
assumes "⋀a x. a ∈ A ∧ Some x = a ⊕ w ⟹ x ∈ B"
shows "w ∈ wand A B"
proof -
have "A ⊗ {w} ⊆ B"
proof (rule subsetI)
fix x assume "x ∈ A ⊗ {w}"
then obtain a where "Some x = a ⊕ w" "a ∈ A"
using PartialSA.add_set_elem by auto
then show "x ∈ B"
using assms by blast
qed
then show ?thesis
using wand_equiv_def by force
qed
lemma non_scalable_R_charact:
assumes "¬ scalable w a"
shows "get_m (R a w) = comp_min_mask (get_m a) (get_m w) ∧ get_h (R a w) = get_h w"
proof -
have "R a w = Abs_state (comp_min_mask (get_m a) (get_m w), get_h w)"
using R_def assms by auto
moreover have "valid_state (comp_min_mask (get_m a) (get_m w), get_h w)"
proof (rule valid_stateI)
show "valid_mask (comp_min_mask (get_m a) (get_m w))"
proof (rule valid_maskI)
show "⋀f. comp_min_mask (get_m a) (get_m w) (null, f) = pnone"
by (metis (no_types, opaque_lifting) PartialSA.unit_neutral add_masks.simps comp_min_mask_def option.distinct(1) p_greater_exists padd_zero plus_ab_defined pmin_greater valid_mask.simps)
fix hl show "pgte pwrite (comp_min_mask (get_m a) (get_m w) hl)"
by (metis PartialSA.unit_neutral comp_min_mask_def greater_mask_def greater_mask_equiv_def option.distinct(1) plus_ab_defined pmin_greater upper_valid_aux valid_mask.simps)
qed
fix hl assume "ppos (comp_min_mask (get_m a) (get_m w) hl)"
show "get_h w hl ≠ None"
by (metis Rep_state ‹ppos (comp_min_mask (get_m a) (get_m w) hl)› comp_min_mask_def get_h.simps get_pre(2) mem_Collect_eq p_greater_exists pmin_greater ppos_add prod.collapse valid_heap_def valid_state.simps)
qed
ultimately show ?thesis
by (metis Rep_state_cases Rep_state_inverse fst_conv get_h.simps get_m.simps mem_Collect_eq snd_conv)
qed
lemma valid_bin:
"valid_state (binary_mask (get_m a), get_h a)"
proof (rule valid_stateI)
show "valid_mask (binary_mask (get_m a))"
by (metis PartialSA.unit_neutral binary_mask_def minus_empty option.discI plus_ab_defined unit_charact(2) valid_mask.elims(2) valid_mask.elims(3))
show "⋀hl. ppos (binary_mask (get_m a) hl) ⟹ get_h a hl ≠ None"
by (metis Rep_prat Rep_state binary_mask_def get_h.simps get_pre(2) leD mem_Collect_eq pnone.rep_eq ppos.rep_eq prod.collapse valid_heap_def valid_state.simps)
qed
lemma in_multiply_sem:
assumes "x ∈ multiply_sem_assertion p A"
shows "∃a ∈ A. x ≽ multiply p a"
using PartialSA.sep_algebra_axioms assms greater_def sep_algebra.upper_closure_def by fastforce
lemma get_h_multiply:
assumes "pgte pwrite p"
shows "get_h (multiply p x) = get_h x"
using Abs_state_inverse assms multiply_valid by auto
lemma in_multiply_refl:
assumes "x ∈ A"
shows "multiply p x ∈ multiply_sem_assertion p A"
using PartialSA.succ_refl PartialSA.upper_closure_def assms by fastforce
lemma get_m_smaller:
assumes "pgte pwrite p"
shows "get_m (multiply p a) hl = pmult p (get_m a hl)"
using Abs_state_inverse assms multiply_mask_def multiply_valid by auto
lemma get_m_smaller_mask:
assumes "pgte pwrite p"
shows "get_m (multiply p a) = multiply_mask p (get_m a)"
using Abs_state_inverse assms multiply_mask_def multiply_valid by auto
lemma multiply_order:
assumes "pgte pwrite p"
and "a ≽ b"
shows "multiply p a ≽ multiply p b"
proof (rule greaterI)
show "larger_heap (get_h (multiply p a)) (get_h (multiply p b))"
using assms(1) assms(2) get_h_multiply larger_implies_larger_heap by presburger
show "greater_mask (get_m (multiply p a)) (get_m (multiply p b))"
by (metis assms(1) assms(2) get_m_smaller_mask greater_maskI larger_implies_greater_mask_hl mult_greater)
qed
lemma multiply_twice:
assumes "pgte pwrite a ∧ pgte pwrite b"
shows "multiply a (multiply b x) = multiply (pmult a b) x"
proof -
have "get_h (multiply (pmult a b) x) = get_h x"
by (metis assms get_h_multiply p_greater_exists padd_asso pmult_order pmult_special(1))
moreover have "get_h (multiply a (multiply b x)) = get_h x"
using assms get_h_multiply by presburger
moreover have "get_m (multiply a (multiply b x)) = get_m (multiply (pmult a b) x)"
proof (rule ext)
fix l
have "pgte pwrite (pmult a b)" using multiply_smaller_pwrite assms by simp
then have "get_m (multiply (pmult a b) x) l = pmult (pmult a b) (get_m x l)"
using get_m_smaller by blast
then show "get_m (multiply a (multiply b x)) l = get_m (multiply (pmult a b) x) l"
by (metis Rep_prat_inverse assms get_m_smaller mult.assoc pmult.rep_eq)
qed
ultimately show ?thesis
using state_ext by presburger
qed
lemma valid_mask_add_comp_min:
assumes "valid_mask a"
and "valid_mask b"
shows "valid_mask (add_masks (comp_min_mask b a) b)"
proof (rule valid_maskI)
show "⋀f. add_masks (comp_min_mask b a) b (null, f) = pnone"
proof -
fix f
have "comp_min_mask b a (null, f) = pnone"
by (metis assms(1) comp_min_mask_def p_greater_exists padd_zero pmin_greater valid_mask.simps)
then show "add_masks (comp_min_mask b a) b (null, f) = pnone"
by (metis add_masks.simps assms(2) padd_zero valid_mask.simps)
qed
fix hl show "pgte pwrite (add_masks (comp_min_mask b a) b hl)"
proof (cases "pgte (a hl) (comp_one (b hl))")
case True
then have "add_masks (comp_min_mask b a) b hl = padd (comp_one (b hl)) (b hl)"
by (simp add: comp_min_mask_def pmin_is)
then have "add_masks (comp_min_mask b a) b hl = pwrite"
by (metis assms(2) padd_comm padd_comp_one valid_mask.simps)
then show ?thesis
by (simp add: pgte.rep_eq)
next
case False
then have "comp_min_mask b a hl = a hl"
by (metis comp_min_mask_def not_pgte_charact pgt_implies_pgte pmin_comm pmin_is)
then have "add_masks (comp_min_mask b a) b hl = padd (a hl) (b hl)"
by auto
moreover have "pgte (padd (comp_one (b hl)) (b hl)) (padd (a hl) (b hl))"
using False padd.rep_eq pgte.rep_eq by force
moreover have "padd (comp_one (b hl)) (b hl) = pwrite"
by (metis assms(2) padd_comm padd_comp_one valid_mask.simps)
ultimately show ?thesis by simp
qed
qed
subsection ‹The combinable wand is stronger than the original wand›
lemma cwand_stronger:
"cwand A B ⊆ wand A B"
proof
fix w assume asm0: "w ∈ cwand A B"
then have r: "⋀a x. a ∈ A ∧ Some x = R a w ⊕ a ⟹ x ∈ B"
using cwand_def by blast
show "w ∈ wand A B"
proof (rule wandI)
fix a x assume asm1: "a ∈ A ∧ Some x = a ⊕ w"
then have "R a w = w"
by (metis PartialSA.defined_def R_compatible_same option.distinct(1))
then show "x ∈ B"
by (metis PartialSA.commutative asm1 r)
qed
qed
subsection ‹The combinable wand is the same as the original wand when the left-hand side is binary›
lemma binary_same:
assumes "binary A"
and "intuitionistic B"
shows "wand A B ⊆ cwand A B"
proof (rule subsetI)
fix w assume "w ∈ wand A B"
then have asm0: "A ⊗ {w} ⊆ B"
by (simp add: wand_equiv_def)
show "w ∈ cwand A B"
proof (rule in_cwand)
fix a x assume asm1: "a ∈ A ∧ Some x = R a w ⊕ a"
show "x ∈ B"
proof (cases "scalable w a")
case True
then show ?thesis
by (metis PartialSA.commutative PartialSA.defined_def R_def asm1 option.distinct(1) scalable_def w_in_scaled)
next
case False
then have r0: "get_m (R a w) = comp_min_mask (get_m a) (get_m w) ∧ get_h (R a w) = get_h w"
using non_scalable_R_charact by blast
moreover have "Abs_state (binary_mask (get_m a), get_h a) ∈ A"
using asm1 assms(1) binary_def by blast
moreover have "greater_mask (add_masks (comp_min_mask (get_m a) (get_m w)) (get_m a))
(add_masks (binary_mask (get_m a)) (get_m w))"
proof (rule greater_maskI)
fix hl show "pgte (add_masks (comp_min_mask (get_m a) (get_m w)) (get_m a) hl) (add_masks (binary_mask (get_m a)) (get_m w) hl)"
proof (cases "get_m a hl = pwrite")
case True
obtain φ where "φ ∈ scaled w" "a |#| φ" using False scalable_def[of w a]
by blast
then obtain p where "ppos p" "pgte pwrite p" "multiply p w |#| a"
using PartialSA.commutative PartialSA.defined_def mem_Collect_eq scaled_def by auto
have "get_m w hl = pnone"
proof (rule ccontr)
assume "get_m w hl ≠ pnone"
then have "ppos (get_m w hl)"
by (metis less_add_same_cancel1 not_pgte_charact p_greater_exists padd.rep_eq padd_zero pgt.rep_eq ppos.rep_eq)
moreover have "get_m (multiply p φ) = multiply_mask p (get_m φ)"
using multiply_valid[of p φ] multiply.simps[of p φ]
by (metis Rep_state_cases Rep_state_inverse ‹pgte pwrite p› fst_conv get_pre(2) mem_Collect_eq)
then have "ppos (get_m (multiply p w) hl)" using pmult_ppos
by (metis Rep_state_cases Rep_state_inverse ‹pgte pwrite p› ‹ppos p› calculation fst_conv get_pre(2) mem_Collect_eq multiply.simps multiply_mask_def multiply_valid)
then have "pgt (padd (get_m (multiply p w) hl) (get_m a hl)) pwrite"
by (metis True add_le_same_cancel2 leD not_pgte_charact padd.rep_eq pgte.rep_eq ppos.rep_eq)
then have "¬ valid_mask (add_masks (get_m (multiply p w)) (get_m a))"
by (metis add_masks.elims not_pgte_charact valid_mask.elims(1))
then show False
using PartialSA.defined_def ‹multiply p w |#| a› plus_ab_defined by blast
qed
then show ?thesis
by (metis Rep_prat_inverse add.right_neutral add_masks.simps binary_mask_def p_greater_exists padd.rep_eq padd_comm pnone.rep_eq)
next
case False
then have "add_masks (binary_mask (get_m a)) (get_m w) hl = get_m w hl"
by (metis Rep_prat_inject add.right_neutral add_masks.simps binary_mask_def padd.rep_eq padd_comm pnone.rep_eq)
then show ?thesis
proof (cases "pgte (get_m w hl) (comp_one (get_m a hl))")
case True
then have "comp_min_mask (get_m a) (get_m w) hl = comp_one (get_m a hl)"
using comp_min_mask_def pmin_is by presburger
then have "add_masks (comp_min_mask (get_m a) (get_m w)) (get_m a) hl = pwrite"
by (metis PartialSA.unit_neutral add_masks.simps add_masks_comm minus_empty option.distinct(1) padd_comp_one plus_ab_defined unit_charact(2) valid_mask.simps)
then show ?thesis
by (metis PartialSA.unit_neutral ‹add_masks (binary_mask (get_m a)) (get_m w) hl = get_m w hl› minus_empty option.distinct(1) plus_ab_defined unit_charact(2) valid_mask.simps)
next
case False
then have "comp_min_mask (get_m a) (get_m w) hl = get_m w hl"
by (metis comp_min_mask_def not_pgte_charact pgt_implies_pgte pmin_comm pmin_is)
then show ?thesis
using ‹add_masks (binary_mask (get_m a)) (get_m w) hl = get_m w hl› p_greater_exists by auto
qed
qed
qed
then have "valid_mask (add_masks (binary_mask (get_m a)) (get_m w))"
by (metis asm1 calculation(1) greater_mask_def option.distinct(1) plus_ab_defined upper_valid_aux)
moreover have "compatible_heaps (get_h a) (get_h w)"
by (metis PartialSA.commutative asm1 r0 option.simps(3) plus_ab_defined)
then obtain xx where "Some xx = Abs_state (binary_mask (get_m a), get_h a) ⊕ w"
using Abs_state_inverse calculation compatible_def fst_conv plus_def valid_bin by auto
then have "xx ∈ B" using asm0
by (meson PartialSA.add_set_elem ‹Abs_state (binary_mask (get_m a), get_h a) ∈ A› singletonI subset_iff)
moreover have "x ≽ xx"
proof (rule greaterI)
show "greater_mask (get_m x) (get_m xx)"
using Abs_state_inverse ‹Some xx = Abs_state (binary_mask (get_m a), get_h a) ⊕ w› asm1 ‹greater_mask (add_masks (comp_min_mask (get_m a) (get_m w)) (get_m a)) (add_masks (binary_mask (get_m a)) (get_m w))› calculation(1) plus_charact(1) valid_bin by auto
show "larger_heap (get_h x) (get_h xx)"
proof (rule larger_heapI)
fix hl xa assume "get_h xx hl = Some xa"
then show "get_h x hl = Some xa"
by (metis PartialSA.commutative Rep_state_cases Rep_state_inverse ‹Some xx = Abs_state (binary_mask (get_m a), get_h a) ⊕ w› asm1 calculation(1) get_h.simps mem_Collect_eq plus_charact(2) snd_conv valid_bin)
qed
qed
ultimately show ?thesis
using assms(2) intuitionistic_def by blast
qed
qed
qed
subsection ‹The combinable wand is combinable›
lemma combinableI:
assumes "⋀a b. ppos a ∧ ppos b ∧ padd a b = pwrite ⟹ (multiply_sem_assertion a (cwand A B)) ⊗ (multiply_sem_assertion b (cwand A B)) ⊆ cwand A B"
shows "combinable (cwand A B)"
proof -
have "⋀a b. ppos a ∧ ppos b ∧ pgte pwrite (padd a b) ⟹ (multiply_sem_assertion a (cwand A B)) ⊗ (multiply_sem_assertion b (cwand A B)) ⊆ multiply_sem_assertion (padd a b) (cwand A B)"
proof -
fix a b assume asm0: "ppos a ∧ ppos b ∧ pgte pwrite (padd a b)"
then have "pgte pwrite a ∧ pgte pwrite b"
using padd.rep_eq pgte.rep_eq ppos.rep_eq by auto
show "(multiply_sem_assertion a (cwand A B)) ⊗ (multiply_sem_assertion b (cwand A B)) ⊆ multiply_sem_assertion (padd a b) (cwand A B)"
proof
fix x assume "x ∈ multiply_sem_assertion a (cwand A B) ⊗ multiply_sem_assertion b (cwand A B)"
then obtain xa xb where "Some x = xa ⊕ xb" "xa ∈ multiply_sem_assertion a (cwand A B)" "xb ∈ multiply_sem_assertion b (cwand A B)"
by (meson PartialSA.add_set_elem)
then obtain wa wb where "wa ∈ cwand A B" "wb ∈ cwand A B" "xa ≽ multiply a wa" "xb ≽ multiply b wb"
by (meson in_multiply_sem)
let ?a = "pdiv a (padd a b)"
let ?b = "pdiv b (padd a b)"
have r0: "pgte pwrite ?a ∧ pgte pwrite ?b"
using asm0 p_greater_exists padd_comm pdiv_smaller ppos_add by blast
have "multiply ?a wa |#| multiply ?b wb"
proof (rule compatibleI)
show "compatible_heaps (get_h (multiply (pdiv a (padd a b)) wa)) (get_h (multiply (pdiv b (padd a b)) wb))"
proof -
have "compatible_heaps (get_h (multiply a wa)) (get_h (multiply b wb))"
by (metis PartialSA.asso2 PartialSA.asso3 PartialSA.greater_equiv PartialSA.minus_some ‹Some x = xa ⊕ xb› ‹xa ≽ multiply a wa› ‹xb ≽ multiply b wb› option.simps(3) plus_ab_defined)
moreover have "get_h (multiply (pdiv a (padd a b)) wa) = get_h (multiply a wa) ∧ get_h (multiply (pdiv b (padd a b)) wb) = get_h (multiply b wb)"
proof -
have "pgte pwrite a ∧ pgte pwrite b"
by (metis asm0 p_greater_exists padd_asso padd_comm)
moreover have "pgte pwrite ?a ∧ pgte pwrite ?b"
using asm0 p_greater_exists padd_comm pdiv_smaller ppos_add by blast
ultimately show ?thesis
using get_h_multiply by presburger
qed
then show ?thesis
using calculation by presburger
qed
show "valid_mask (add_masks (get_m (multiply (pdiv a (padd a b)) wa)) (get_m (multiply (pdiv b (padd a b)) wb)))"
proof (rule valid_maskI)
show "⋀f. add_masks (get_m (multiply (pdiv a (padd a b)) wa)) (get_m (multiply (pdiv b (padd a b)) wb)) (null, f) = pnone"
by (metis PartialSA.unit_neutral add_masks_equiv_valid_null option.distinct(1) plus_ab_defined valid_mask.simps valid_null_def)
fix hl have "add_masks (get_m (multiply (pdiv a (padd a b)) wa)) (get_m (multiply (pdiv b (padd a b)) wb)) hl
= padd (pmult ?a (get_m wa hl)) (pmult ?b (get_m wb hl))"
proof -
have "get_m (multiply ?a wa) hl = pmult ?a (get_m wa hl)"
using Abs_state_inverse r0 multiply_mask_def multiply_valid by auto
moreover have "get_m (multiply ?b wb) hl = pmult ?b (get_m wb hl)"
using Abs_state_inverse r0 multiply_mask_def multiply_valid by auto
ultimately show ?thesis by simp
qed
moreover have "pgte pwrite (padd (pmult ?a (get_m wa hl)) (pmult ?b (get_m wb hl)))"
proof (rule padd_one_ineq_sum)
show "pgte pwrite (get_m wa hl)"
by (metis PartialSA.unit_neutral option.discI plus_ab_defined upper_valid_aux valid_mask.simps)
show "pgte pwrite (get_m wb hl)"
by (metis PartialSA.unit_neutral option.discI plus_ab_defined upper_valid_aux valid_mask.simps)
show "padd (pdiv a (padd a b)) (pdiv b (padd a b)) = pwrite"
using asm0 sum_coeff by blast
qed
ultimately show "pgte pwrite (add_masks (get_m (multiply (pdiv a (padd a b)) wa)) (get_m (multiply (pdiv b (padd a b)) wb)) hl)"
by presburger
qed
qed
then obtain xx where xx_def: "Some xx = multiply ?a wa ⊕ multiply ?b wb"
using PartialSA.defined_def by auto
moreover have inclusion: "(multiply_sem_assertion ?a (cwand A B)) ⊗ (multiply_sem_assertion ?b (cwand A B)) ⊆ cwand A B"
proof (rule assms)
show "ppos (pdiv a (padd a b)) ∧ ppos (pdiv b (padd a b)) ∧ padd (pdiv a (padd a b)) (pdiv b (padd a b)) = pwrite"
using asm0 padd.rep_eq pdiv.rep_eq ppos.rep_eq sum_coeff by auto
qed
ultimately have "xx ∈ cwand A B"
proof -
have "multiply ?a wa ∈ multiply_sem_assertion ?a (cwand A B)"
using ‹wa ∈ cwand A B› in_multiply_refl by presburger
moreover have "multiply ?b wb ∈ multiply_sem_assertion ?b (cwand A B)"
by (meson ‹wb ∈ cwand A B› in_multiply_refl)
ultimately show ?thesis
using PartialSA.add_set_def xx_def inclusion by fastforce
qed
moreover have "x ≽ multiply (padd a b) xx"
proof (rule greaterI)
have "valid_state (multiply_mask (padd a b) (get_m xx), get_h xx)"
using asm0 multiply_valid by blast
show "larger_heap (get_h x) (get_h (multiply (padd a b) xx))"
proof -
have "get_h (multiply (padd a b) xx) = get_h xx"
using asm0 get_h_multiply by blast
moreover have "get_h xx = get_h wa ++ get_h wb"
by (metis xx_def asm0 get_h_multiply p_greater_exists padd_comm plus_charact(2) sum_coeff)
moreover have "get_h x = get_h xa ++ get_h xb"
using ‹Some x = xa ⊕ xb› plus_charact(2) by presburger
moreover have "get_h wa = get_h (multiply a wa) ∧ get_h wb = get_h (multiply b wb)"
by (metis asm0 get_h_multiply order_trans p_greater_exists padd_comm pgte.rep_eq)
moreover have "larger_heap (get_h xa) (get_h wa) ∧ larger_heap (get_h xb) (get_h wb)"
using ‹xa ≽ multiply a wa› ‹xb ≽ multiply b wb› calculation(4) larger_implies_larger_heap by presburger
ultimately show ?thesis
by (metis ‹Some x = xa ⊕ xb› larger_heaps_sum_ineq option.simps(3) plus_ab_defined)
qed
show "greater_mask (get_m x) (get_m (multiply (padd a b) xx))"
proof (rule greater_maskI)
fix hl
have "pgte (get_m x hl) (padd (get_m xa hl) (get_m xb hl))"
using ‹Some x = xa ⊕ xb› pgte.rep_eq plus_charact(1) by auto
moreover have "pgte (get_m xa hl) (get_m (multiply a wa) hl) ∧ pgte (get_m xb hl) (get_m (multiply b wb) hl)"
using ‹xa ≽ multiply a wa› ‹xb ≽ multiply b wb› larger_implies_greater_mask_hl by blast
moreover have "get_m (multiply (padd a b) xx) hl = pmult (padd a b) (get_m xx hl)"
by (metis Rep_state_cases Rep_state_inverse ‹valid_state (multiply_mask (padd a b) (get_m xx), get_h xx)› fst_conv get_pre(2) mem_Collect_eq multiply.simps multiply_mask_def)
moreover have "... = padd (pmult (pmult (padd a b) ?a) (get_m wa hl)) (pmult (pmult (padd a b) ?b) (get_m wb hl))"
proof -
have "get_m (multiply ?a wa) hl = pmult ?a (get_m wa hl)"
by (metis Abs_state_inverse asm0 fst_conv get_pre(2) mem_Collect_eq multiply.simps multiply_mask_def multiply_valid p_greater_exists sum_coeff)
moreover have "get_m (multiply ?b wb) hl = pmult ?b (get_m wb hl)"
by (metis Abs_state_inverse asm0 fst_conv get_pre(2) mem_Collect_eq multiply.simps multiply_mask_def multiply_valid p_greater_exists padd_comm pdiv_smaller ppos_add)
ultimately have "get_m xx hl = padd (pmult ?a (get_m wa hl)) (pmult ?b (get_m wb hl))"
using xx_def plus_charact(1) by fastforce
then show ?thesis
by (simp add: pmult_padd)
qed
moreover have "... = padd (pmult a (get_m wa hl)) (pmult b (get_m wb hl))"
using asm0 pmult_pdiv_cancel ppos_add by presburger
moreover have "get_m (multiply a wa) hl = pmult a (get_m wa hl) ∧ get_m (multiply b wb) hl = pmult b (get_m wb hl)"
proof -
have "valid_mask (multiply_mask a (get_m wa))"
using asm0 mult_add_states multiply_valid upper_valid_aux valid_state.simps by blast
moreover have "valid_mask (multiply_mask b (get_m wb))"
using asm0 mult_add_states multiply_valid upper_valid valid_state.simps by blast
ultimately show ?thesis
by (metis (no_types, lifting) Abs_state_inverse asm0 fst_conv get_pre(2) mem_Collect_eq multiply.simps multiply_mask_def multiply_valid order_trans p_greater_exists padd_comm pgte.rep_eq)
qed
ultimately show "pgte (get_m x hl) (get_m (multiply (padd a b) xx) hl)"
by (simp add: padd.rep_eq pgte.rep_eq)
qed
qed
ultimately show "x ∈ multiply_sem_assertion (padd a b) (cwand A B)"
by (metis PartialSA.up_closed_def PartialSA.upper_closure_up_closed in_multiply_refl multiply_sem_assertion.simps)
qed
qed
then show ?thesis
using combinable_def by presburger
qed
lemma combinable_cwand:
assumes "combinable B"
and "intuitionistic B"
shows "combinable (cwand A B)"
proof (rule combinableI)
fix α β assume asm0: "ppos α ∧ ppos β ∧ padd α β = pwrite"
then have "pgte pwrite α ∧ pgte pwrite β"
by (metis p_greater_exists padd_comm)
show "multiply_sem_assertion α (cwand A B) ⊗ multiply_sem_assertion β (cwand A B) ⊆ cwand A B"
proof
fix w assume asm: "w ∈ multiply_sem_assertion α (cwand A B) ⊗ multiply_sem_assertion β (cwand A B)"
then obtain xa xb where "Some w = xa ⊕ xb" "xa ∈ multiply_sem_assertion α (cwand A B)" "xb ∈ multiply_sem_assertion β (cwand A B)"
by (meson PartialSA.add_set_elem)
then obtain wa wb where "wa ∈ cwand A B" "wb ∈ cwand A B" "xa ≽ multiply α wa" "xb ≽ multiply β wb"
by (meson in_multiply_sem)
then obtain r: "⋀a x. a ∈ A ∧ Some x = R a wa ⊕ a ⟹ x ∈ B" "⋀a x. a ∈ A ∧ Some x = R a wb ⊕ a ⟹ x ∈ B"
using cwand_def by blast
show "w ∈ cwand A B"
proof (rule in_cwand)
fix a x assume asm1: "a ∈ A ∧ Some x = R a w ⊕ a"
have "¬ scalable w a"
proof (rule ccontr)
assume "¬ ¬ scalable w a"
then have "R a w = w ∧ ¬ a |#| R a w"
by (simp add: R_def scalable_def w_in_scaled)
then show False
using PartialSA.commutative PartialSA.defined_def asm1 by auto
qed
then have r3: "get_h (R a w) = get_h w ∧ get_m (R a w) = comp_min_mask (get_m a) (get_m w)"
using non_scalable_R_charact by blast
moreover obtain p where "a |#| multiply p w" "ppos p ∧ pgte pwrite p"
using ‹¬ scalable w a› non_scalable_instantiate by blast
moreover have "¬ scalable wa a"
proof -
have "a |#| multiply (pmult α p) wa"
proof -
have "w ≽ xa" using ‹Some w = xa ⊕ xb› using PartialSA.greater_def by blast
then have "multiply p w ≽ multiply p xa"
using calculation(3) multiply_order by blast
then have "multiply p w ≽ multiply (pmult α p) wa"
proof -
have "multiply p w ≽ multiply p (multiply α wa)"
using PartialSA.succ_trans ‹w ≽ xa› ‹xa ≽ multiply α wa› calculation(3) multiply_order by blast
then show ?thesis
using ‹pgte pwrite α ∧ pgte pwrite β› calculation(3) multiply_twice pmult_comm by auto
qed
then show ?thesis
using PartialSA.asso3 PartialSA.defined_def PartialSA.minus_some calculation(2) by fastforce
qed
moreover have "ppos (pmult α p) ∧ pgte pwrite (pmult α p)"
by (metis Rep_prat_inverse ‹ppos p ∧ pgte pwrite p› add.right_neutral asm0 dual_order.strict_iff_order padd.rep_eq pgte.rep_eq pmult_comm pmult_ppos pmult_special(2) pnone.rep_eq ppos.rep_eq ppos_eq_pnone padd_one_ineq_sum)
ultimately show ?thesis
using scalable_def scaled_def by auto
qed
then have r1: "get_h (R a wa) = get_h wa ∧ get_m (R a wa) = comp_min_mask (get_m a) (get_m wa)"
using non_scalable_R_charact by blast
moreover have "R a wa |#| a"
proof (rule compatibleI)
have "larger_heap (get_h w) (get_h xa) ∧ larger_heap (get_h xa) (get_h wa)"
by (metis PartialSA.commutative PartialSA.greater_equiv ‹Some w = xa ⊕ xb› ‹pgte pwrite α ∧ pgte pwrite β› ‹xa ≽ multiply α wa› get_h_multiply larger_implies_larger_heap)
then show "compatible_heaps (get_h (R a wa)) (get_h a)"
by (metis asm1 calculation(1) calculation(4) larger_heap_comp option.distinct(1) plus_ab_defined)
show "valid_mask (add_masks (get_m (R a wa)) (get_m a))"
by (metis PartialSA.unit_neutral calculation(4) minus_empty option.distinct(1) plus_ab_defined unit_charact(2) valid_mask_add_comp_min)
qed
then obtain ba where "Some ba = R a wa ⊕ a"
using PartialSA.defined_def by auto
moreover have "¬ scalable wb a"
proof -
have "a |#| multiply (pmult β p) wb"
proof -
have "w ≽ xb" using ‹Some w = xa ⊕ xb›
using PartialSA.greater_equiv by blast
then have "multiply p w ≽ multiply p xb"
using calculation(3) multiply_order by blast
then have "multiply p w ≽ multiply (pmult β p) wb"
proof -
have "multiply p w ≽ multiply p (multiply β wb)"
using PartialSA.succ_trans ‹w ≽ xb› ‹xb ≽ multiply β wb› calculation(3) multiply_order by blast
then show ?thesis
using ‹pgte pwrite α ∧ pgte pwrite β› calculation(3) multiply_twice pmult_comm by auto
qed
then show ?thesis
using PartialSA.asso3 PartialSA.defined_def PartialSA.minus_some calculation(2) by fastforce
qed
moreover have "ppos (pmult β p) ∧ pgte pwrite (pmult β p)"
by (simp add: ‹pgte pwrite α ∧ pgte pwrite β› ‹ppos p ∧ pgte pwrite p› asm0 multiply_smaller_pwrite pmult_ppos)
ultimately show ?thesis
using scalable_def scaled_def by auto
qed
then have r2: "get_h (R a wb) = get_h wb ∧ get_m (R a wb) = comp_min_mask (get_m a) (get_m wb)"
using non_scalable_R_charact by blast
moreover have "R a wb |#| a"
proof (rule compatibleI)
have "larger_heap (get_h w) (get_h xb) ∧ larger_heap (get_h xb) (get_h wb)"
using ‹Some w = xa ⊕ xb› ‹pgte pwrite α ∧ pgte pwrite β› ‹xb ≽ multiply β wb› get_h_multiply larger_heap_def larger_implies_larger_heap plus_charact(2) by fastforce
then show "compatible_heaps (get_h (R a wb)) (get_h a)"
by (metis asm1 calculation(1) calculation(6) larger_heap_comp option.simps(3) plus_ab_defined)
show "valid_mask (add_masks (get_m (R a wb)) (get_m a))"
by (metis PartialSA.unit_neutral calculation(6) minus_empty option.distinct(1) plus_ab_defined unit_charact(2) valid_mask_add_comp_min)
qed
then obtain bb where "Some bb = R a wb ⊕ a"
using PartialSA.defined_def by auto
moreover obtain ya where "Some ya = R a wa ⊕ a"
using calculation(5) by auto
then have "ya ∈ B"
using asm1 r(1) by blast
then have "multiply α ya ∈ multiply_sem_assertion α B"
using in_multiply_refl by blast
moreover obtain yb where "Some yb = R a wb ⊕ a"
using calculation(7) by auto
then have "yb ∈ B"
using asm1 r(2) by blast
then have "multiply β yb ∈ multiply_sem_assertion β B"
using in_multiply_refl by blast
moreover have "(multiply α ya) |#| (multiply β yb)"
proof (rule compatibleI)
have "get_h ya = get_h wa ++ get_h a"
using ‹Some ya = R a wa ⊕ a› r1 plus_charact(2) by presburger
then have "get_h (multiply α ya) = get_h wa ++ get_h a"
using ‹pgte pwrite α ∧ pgte pwrite β› get_h_multiply by presburger
moreover have "get_h yb = get_h wb ++ get_h a"
using ‹Some yb = R a wb ⊕ a› r2 plus_charact(2) by presburger
then have "get_h (multiply β yb) = get_h wb ++ get_h a"
using ‹pgte pwrite α ∧ pgte pwrite β› get_h_multiply by presburger
moreover have "compatible_heaps (get_h wa) (get_h wb)"
proof (rule compatible_heapsI)
fix hl a b assume "get_h wa hl = Some a" "get_h wb hl = Some b"
then have "get_h xa hl = Some a" "get_h xb hl = Some b"
apply (metis (full_types) ‹pgte pwrite α ∧ pgte pwrite β› ‹xa ≽ multiply α wa› get_h_multiply larger_heap_def larger_implies_larger_heap)
by (metis ‹get_h wb hl = Some b› ‹pgte pwrite α ∧ pgte pwrite β› ‹xb ≽ multiply β wb› get_h_multiply larger_heap_def larger_implies_larger_heap)
moreover have "compatible_heaps (get_h xa) (get_h xb)"
by (metis ‹Some w = xa ⊕ xb› option.simps(3) plus_ab_defined)
ultimately show "a = b"
by (metis compatible_heaps_def compatible_options.simps(1))
qed
ultimately show "compatible_heaps (get_h (multiply α ya)) (get_h (multiply β yb))"
by (metis PartialSA.commutative PartialSA.core_is_smaller ‹Some ya = R a wa ⊕ a› ‹Some yb = R a wb ⊕ a›
r1 r2 compatible_heaps_sum core_defined(1) core_defined(2) option.distinct(1) plus_ab_defined)
show "valid_mask (add_masks (get_m (multiply α ya)) (get_m (multiply β yb)))"
proof (rule valid_maskI)
show "⋀f. add_masks (get_m (multiply α ya)) (get_m (multiply β yb)) (null, f) = pnone"
by (metis (no_types, opaque_lifting) PartialSA.core_is_smaller add_masks.simps core_defined(2) minus_empty not_None_eq plus_ab_defined valid_mask.simps)
fix hl
have "add_masks (get_m (multiply α ya)) (get_m (multiply β yb)) hl = padd (pmult α (get_m ya hl)) (pmult β (get_m yb hl))"
using ‹pgte pwrite α ∧ pgte pwrite β› get_m_smaller by auto
moreover have "get_m ya hl = padd (get_m (R a wa) hl) (get_m a hl) ∧ get_m yb hl = padd (get_m (R a wb) hl) (get_m a hl)"
using ‹Some ya = R a wa ⊕ a› ‹Some yb = R a wb ⊕ a› plus_charact(1) by auto
ultimately show "pgte pwrite (add_masks (get_m (multiply α ya)) (get_m (multiply β yb)) hl)"
by (metis PartialSA.unit_neutral asm0 option.distinct(1) padd_one_ineq_sum plus_ab_defined plus_charact(1) valid_mask.simps)
qed
qed
then obtain y where "Some y = multiply α ya ⊕ multiply β yb"
using PartialSA.defined_def by auto
moreover have "x ≽ y"
proof (rule greaterI)
have "get_h y = get_h ya ++ get_h yb"
using ‹pgte pwrite α ∧ pgte pwrite β› calculation(10) get_h_multiply plus_charact(2) by presburger
moreover have "get_h ya = get_h wa ++ get_h a"
using ‹Some ya = R a wa ⊕ a› r1 plus_charact(2) by presburger
moreover have "get_h yb = get_h wb ++ get_h a"
using ‹Some yb = R a wb ⊕ a› r2 plus_charact(2) by presburger
moreover have "larger_heap (get_h x) (get_h wa)"
proof -
have "larger_heap (get_h x) (get_h xa)"
by (metis PartialSA.greater_def ‹Some w = xa ⊕ xb› r3 asm1 larger_heap_trans larger_implies_larger_heap)
moreover have "larger_heap (get_h xa) (get_h wa)"
by (metis ‹pgte pwrite α ∧ pgte pwrite β› ‹xa ≽ multiply α wa› get_h_multiply larger_implies_larger_heap)
ultimately show ?thesis
using larger_heap_trans by blast
qed
moreover have "larger_heap (get_h x) (get_h wb)"
proof -
have "larger_heap (get_h x) (get_h xb)"
by (metis PartialSA.greater_def PartialSA.greater_equiv ‹Some w = xa ⊕ xb› r3 asm1 larger_heap_trans larger_implies_larger_heap)
moreover have "larger_heap (get_h xb) (get_h wb)"
by (metis ‹pgte pwrite α ∧ pgte pwrite β› ‹xb ≽ multiply β wb› get_h_multiply larger_implies_larger_heap)
ultimately show ?thesis
using larger_heap_trans by blast
qed
moreover have "larger_heap (get_h x) (get_h a)"
using PartialSA.greater_equiv asm1 larger_implies_larger_heap by blast
ultimately show "larger_heap (get_h x) (get_h y)"
by (simp add: larger_heap_plus)
show "greater_mask (get_m x) (get_m y)"
proof (rule greater_maskI)
fix hl
have "get_m x hl = padd (get_m (R a w) hl) (get_m a hl)"
using asm1 plus_charact(1) by auto
moreover have "get_m y hl = padd (pmult α (padd (get_m (R a wa) hl) (get_m a hl))) (pmult β (padd (get_m (R a wb) hl) (get_m a hl)))"
by (metis ‹Some y = multiply α ya ⊕ multiply β yb› ‹Some ya = R a wa ⊕ a› ‹Some yb = R a wb ⊕ a› ‹pgte pwrite α ∧ pgte pwrite β› add_masks.simps get_m_smaller plus_charact(1))
moreover have equ: "padd (pmult α (padd (get_m (R a wa) hl) (get_m a hl))) (pmult β (padd (get_m (R a wb) hl) (get_m a hl)))
= padd (padd (pmult α (get_m a hl)) (pmult β (get_m a hl))) (padd (pmult α (get_m (R a wa) hl)) (pmult β (get_m (R a wb) hl)))"
using padd_asso padd_comm pmult_distr by force
have "pgte (get_m (R a w) hl) (padd (pmult α (get_m (R a wa) hl)) (pmult β (get_m (R a wb) hl)))"
proof (cases "pgte (get_m w hl) (comp_one (get_m a hl))")
case True
then have "get_m (R a w) hl = (comp_one (get_m a hl))"
using r3 comp_min_mask_def pmin_is by presburger
moreover have "pgte (comp_one (get_m a hl)) (get_m (R a wa) hl)"
by (metis r1 comp_min_mask_def pmin_comm pmin_greater)
then have "pgte (pmult α (comp_one (get_m a hl))) (pmult α (get_m (R a wa) hl))"
by (metis pmult_comm pmult_order)
moreover have "pgte (comp_one (get_m a hl)) (get_m (R a wb) hl)"
by (metis r2 comp_min_mask_def pmin_comm pmin_greater)
then have "pgte (pmult β (comp_one (get_m a hl))) (pmult β (get_m (R a wb) hl))"
by (metis pmult_comm pmult_order)
ultimately show ?thesis
using ‹pgte (comp_one (get_m a hl)) (get_m (R a wa) hl)› ‹pgte (comp_one (get_m a hl)) (get_m (R a wb) hl)› asm0 padd_one_ineq_sum by presburger
next
case False
then have "get_m (R a w) hl = get_m w hl"
by (metis r3 comp_min_mask_def not_pgte_charact pgt_implies_pgte pmin_comm pmin_is)
moreover have "pgte (get_m w hl) (padd (pmult α (get_m wa hl)) (pmult β (get_m wb hl)))"
proof -
have "pgte (get_m w hl) (padd (get_m xa hl) (get_m xb hl))"
using ‹Some w = xa ⊕ xb› not_pgte_charact pgt_implies_pgte plus_charact(1) by auto
moreover have "pgte (get_m xa hl) (pmult α (get_m wa hl))"
by (metis ‹pgte pwrite α ∧ pgte pwrite β› ‹xa ≽ multiply α wa› get_m_smaller larger_implies_greater_mask_hl)
moreover have "pgte (get_m xb hl) (pmult β (get_m wb hl))"
by (metis ‹pgte pwrite α ∧ pgte pwrite β› ‹xb ≽ multiply β wb› get_m_smaller larger_implies_greater_mask_hl)
ultimately show ?thesis
by (simp add: padd.rep_eq pgte.rep_eq)
qed
moreover have "pgte (pmult α (get_m wa hl)) (pmult α (get_m (R a wa) hl))"
by (metis R_smaller larger_implies_greater_mask_hl pmult_comm pmult_order)
moreover have "pgte (pmult β (get_m wb hl)) (pmult β (get_m (R a wb) hl))"
by (metis R_smaller larger_implies_greater_mask_hl pmult_comm pmult_order)
ultimately show ?thesis
using padd.rep_eq pgte.rep_eq by force
qed
moreover have "get_m x hl = padd (get_m (R a w) hl) (get_m a hl)"
using calculation(1) by auto
moreover have "get_m y hl = padd (pmult α (get_m ya hl)) (pmult β (get_m yb hl))"
using ‹Some y = multiply α ya ⊕ multiply β yb› ‹pgte pwrite α ∧ pgte pwrite β› get_m_smaller plus_charact(1) by auto
moreover have "padd (pmult α (get_m ya hl)) (pmult β (get_m yb hl)) =
padd (pmult α (padd (get_m (R a wa) hl) (get_m a hl))) (pmult β (padd (get_m (R a wb) hl) (get_m a hl)))"
using calculation(2) calculation(5) by presburger
moreover have "... = padd (pmult (padd α β) (get_m a hl)) (padd (pmult α (get_m (R a wa) hl)) (pmult β (get_m (R a wb) hl)))"
by (metis equ pmult_comm pmult_distr)
ultimately show "pgte (get_m x hl) (get_m y hl)"
using asm0 p_greater_exists padd_asso padd_comm pmult_special(1) by force
qed
qed
ultimately have "y ∈ multiply_sem_assertion α B ⊗ multiply_sem_assertion β B"
using PartialSA.add_set_elem by blast
then have "y ∈ multiply_sem_assertion pwrite B"
by (metis asm0 assms(1) combinable_def not_pgte_charact pgt_implies_pgte subsetD)
then obtain b where "y ≽ multiply pwrite b" "b ∈ B"
using in_multiply_sem by blast
then have "multiply pwrite b = b"
by (metis Rep_state_inverse get_h_m mult_write_mask multiply.simps)
then have "y ∈ B"
by (metis ‹b ∈ B› ‹y ≽ multiply pwrite b› assms(2) intuitionistic_def)
show "x ∈ B"
using ‹x ≽ y› ‹y ∈ B› assms(2) intuitionistic_def by blast
qed
qed
qed
subsection Theorems
text ‹The following theorem is crucial to use the package logic~\<^cite>‹"Dardinier22"› to automatically
compute footprints of combinable wands.›
theorem R_mono_transformer:
"PartialSA.mono_transformer (R a)"
proof -
have "R a unit = unit"
by (simp add: PartialSA.succ_antisym PartialSA.unit_smaller R_smaller)
moreover have "⋀φ φ'. φ' ≽ φ ⟹ R a φ' ≽ R a φ"
proof -
fix φ φ'
assume "φ' ≽ φ"
show "R a φ' ≽ R a φ"
proof (cases "scalable φ' a")
case True
then show ?thesis
by (metis PartialSA.succ_trans R_def R_smaller ‹φ' ≽ φ›)
next
case False
then obtain p where "ppos p" "pgte pwrite p" "multiply p φ' |#| a"
by (metis PartialSA.commutative PartialSA.defined_def non_scalable_instantiate)
then have "multiply p φ |#| a"
using PartialSA.smaller_compatible ‹φ' ≽ φ› multiply_order by blast
then have "¬ scalable φ a"
using PartialSA.commutative PartialSA.defined_def ‹pgte pwrite p› ‹ppos p› scalable_def scaled_def by auto
moreover have "greater_mask (comp_min_mask (get_m a) (get_m φ')) (comp_min_mask (get_m a) (get_m φ))"
proof (rule greater_maskI)
fix hl show "pgte (comp_min_mask (get_m a) (get_m φ') hl) (comp_min_mask (get_m a) (get_m φ) hl)"
proof (cases "pgte (get_m φ' hl) (comp_one (get_m a hl))")
case True
then show ?thesis
by (metis comp_min_mask_def pmin_comm pmin_greater pmin_is)
next
case False
then show ?thesis
by (metis PartialSA.succ_trans R_smaller ‹φ' ≽ φ› calculation comp_min_mask_def larger_implies_greater_mask_hl non_scalable_R_charact not_pgte_charact pgt_implies_pgte pmin_comm pmin_is)
qed
qed
ultimately show ?thesis
using False ‹φ' ≽ φ› greaterI larger_implies_larger_heap non_scalable_R_charact by presburger
qed
qed
ultimately show ?thesis
by (simp add: PartialSA.mono_transformer_def)
qed
theorem properties_of_combinable_wands:
assumes "intuitionistic B"
shows "combinable B ⟹ combinable (cwand A B)"
and "cwand A B ⊆ wand A B"
and "binary A ⟹ cwand A B = wand A B"
by (simp_all add: assms combinable_cwand cwand_stronger binary_same dual_order.eq_iff)
end