Session Combinable_Wands

iv class="head">

Theory PosRat

section ‹State Model with Fractional Permissions›

text ‹In this section, we define a concrete state model based on fractional permissions \cite{Boyland03}.
A state is a pair of a permission mask and a partial heap.
A permission mask is a total map from heap locations to a rational between 0 and 1 (included),
while a partial heap is a partial map from heap locations to values.
We also define a partial addition on these states, and show that this state model corresponds to a separation algebra.›

subsection ‹Non-negative rationals (permission amounts)›

theory PosRat
  imports Main HOL.Rat
begin



subsubsection Definitions

typedef prat = "{ r :: rat |r. r ≥ 0}" by fastforce

setup_lifting type_definition_prat

lift_definition pwrite :: "prat" is "1" by simp
lift_definition pnone :: "prat" is "0" by simp
lift_definition half :: "prat" is "1 / 2" by fastforce

lift_definition pgte :: "prat ⇒ prat ⇒ bool" is "(≥)" done
lift_definition pgt :: "prat ⇒ prat ⇒ bool" is "(>)" done
(* lift_definition lte :: "prat ⇒ prat ⇒ bool" is "(≤)" done *)
lift_definition lt :: "prat ⇒ prat ⇒ bool" is "(<)" done
lift_definition ppos :: "prat ⇒ bool" is "λp. p > 0" done

lift_definition pmult :: "prat ⇒ prat ⇒ prat" is "(*)" by simp
lift_definition padd :: "prat ⇒ prat ⇒ prat" is "(+)" by simp

lift_definition pdiv :: "prat ⇒ prat ⇒ prat" is "(/)" by simp

lift_definition pmin :: "prat ⇒ prat ⇒ prat" is "(min)" by simp
lift_definition pmax :: "prat ⇒ prat ⇒ prat" is "(max)" by simp

subsubsection Lemmas

lemma pmin_comm:
  "pmin a b = pmin b a"
  by (metis Rep_prat_inverse min.commute pmin.rep_eq)

lemma pmin_greater:
  "pgte a (pmin a b)"
  by (simp add: pgte.rep_eq pmin.rep_eq)

lemma pmin_is:
  assumes "pgte a b"
  shows "pmin a b = b"
  by (metis Rep_prat_inject assms min_absorb2 pgte.rep_eq pmin.rep_eq)

lemma pmax_comm:
  "pmax a b = pmax b a"
  by (metis Rep_prat_inverse max.commute pmax.rep_eq)

lemma pmax_smaller:
  "pgte (pmax a b) a"
  by (simp add: pgte.rep_eq pmax.rep_eq)

lemma pmax_is:
  assumes "pgte a b"
  shows "pmax a b = a"
  by (metis Rep_prat_inject assms max.absorb_iff1 pgte.rep_eq pmax.rep_eq)


lemma pmax_is_smaller:
  assumes "pgte x a"
      and "pgte x b"
    shows "pgte x (pmax a b)"
proof (cases "pgte a b")
  case True
  then show ?thesis
    by (simp add: assms(1) pmax_is)
next
  case False
  then show ?thesis
    using assms(2) pgte.rep_eq pmax.rep_eq by auto
qed


lemma half_between_0_1:
  "ppos half ∧ pgt pwrite half"
  by (simp add: half.rep_eq pgt.rep_eq ppos.rep_eq pwrite.rep_eq)

lemma pgt_implies_pgte:
  assumes "pgt a b"
  shows "pgte a b"
  by (meson assms less_imp_le pgt.rep_eq pgte.rep_eq)

lemma half_plus_half:
  "padd half half = pwrite"
  by (metis Rep_prat_inject divide_less_eq_numeral1(1) dual_order.irrefl half.rep_eq less_divide_eq_numeral1(1) linorder_neqE_linordered_idom mult.right_neutral one_add_one padd.rep_eq pwrite.rep_eq ring_class.ring_distribs(1))

lemma padd_comm:
  "padd a b = padd b a"
  by (metis Rep_prat_inject add.commute padd.rep_eq)

lemma padd_asso:
  "padd (padd a b) c = padd a (padd b c)"
  by (metis Rep_prat_inverse group_cancel.add1 padd.rep_eq)


lemma p_greater_exists:
  "pgte a b ⟷ (∃r. a = padd b r)"
proof (rule iffI)
  show "pgte a b ⟹ ∃r. a = padd b r"
  proof -
    assume asm: "pgte a b"
    obtain aa bb where "aa = Rep_prat a" "bb = Rep_prat b"
      by simp
    then have "aa ≥ bb" using asm
      using pgte.rep_eq by fastforce
    then obtain rr where "rr = aa - bb"
      by simp
    then have "a = padd b (Abs_prat rr)"
      by (metis Abs_prat_inverse Rep_prat_inject ‹aa = Rep_prat a› ‹bb = Rep_prat b› ‹bb ≤ aa› add.commute diff_add_cancel diff_ge_0_iff_ge mem_Collect_eq padd.rep_eq)
    then show "∃r. a = padd b r" by blast
  qed
  show "∃r. a = padd b r ⟹ pgte a b"
    using Rep_prat padd.rep_eq pgte.rep_eq by force
qed


lemma pgte_antisym:
  assumes "pgte a b"
      and "pgte b a"
    shows "a = b"
  by (metis Rep_prat_inverse assms(1) assms(2) leD le_less pgte.rep_eq)

lemma greater_sum_both:
  assumes "pgte a (padd b c)"
  shows "∃a1 a2. a = padd a1 a2 ∧ pgte a1 b ∧ pgte a2 c"
proof -
  obtain aa bb cc where "aa = Rep_prat a" "bb = Rep_prat b" "cc = Rep_prat c"
    by simp
  then have "aa ≥ bb + cc"
    using assms padd.rep_eq pgte.rep_eq by auto
  then obtain x where "aa = bb + x" "x ≥ cc"
    by (metis add.commute add_le_cancel_left diff_add_cancel)
  then show ?thesis
    by (metis assms order_refl p_greater_exists padd_asso pgte.rep_eq)
qed


lemma padd_cancellative:
  assumes "a = padd x b"
      and "a = padd y b"
    shows "x = y"
  by (metis Rep_prat_inject add_le_cancel_right assms(1) assms(2) leD less_eq_rat_def padd.rep_eq)


lemma not_pgte_charact:
  "¬ pgte a b ⟷ pgt b a"
  by (meson not_less pgt.rep_eq pgte.rep_eq)

lemma pgte_pgt:
  assumes "pgt a b"
      and "pgte c d"
    shows "pgt (padd a c) (padd b d)"
  using assms(1) assms(2) padd.rep_eq pgt.rep_eq pgte.rep_eq by auto

lemma pmult_distr:
  "pmult a (padd b c) = padd (pmult a b) (pmult a c)"
  by (metis Rep_prat_inject distrib_left padd.rep_eq pmult.rep_eq)

lemma pmult_comm:
  "pmult a b = pmult b a"
  by (metis Rep_prat_inject mult.commute pmult.rep_eq)

lemma pmult_special:
  "pmult pwrite x = x"
  "pmult pnone x = pnone"
  apply (metis Rep_prat_inverse comm_monoid_mult_class.mult_1 pmult.rep_eq pwrite.rep_eq)
  by (metis Rep_prat_inverse mult_zero_left pmult.rep_eq pnone.rep_eq)



definition pinv where
  "pinv p = pdiv pwrite p"

lemma pinv_double_half:
  assumes "ppos p"
  shows "pmult half (pinv p) = pinv (padd p p)"
proof -
  have "(Fract 1 2) * ((Fract 1 1) / (Rep_prat p)) = (Fract 1 1) / (Rep_prat p + Rep_prat p)"
    by (metis (no_types, lifting) One_rat_def comm_monoid_mult_class.mult_1 divide_rat mult_2 mult_rat rat_number_expand(3) times_divide_times_eq)
  then show ?thesis
    by (metis Rep_prat_inject half.rep_eq mult_2 mult_numeral_1_right numeral_One padd.rep_eq pdiv.rep_eq pinv_def pmult.rep_eq pwrite.rep_eq times_divide_times_eq)
qed

lemma ppos_mult:
  assumes "ppos a"
      and "ppos b"
    shows "ppos (pmult a b)"
  using assms(1) assms(2) pmult.rep_eq ppos.rep_eq by auto

lemma padd_zero:
  "pnone = padd a b ⟷ a = pnone ∧ b = pnone"
  by (metis Rep_prat Rep_prat_inject add.right_neutral leD le_add_same_cancel2 less_eq_rat_def mem_Collect_eq padd.rep_eq pnone.rep_eq)

lemma ppos_add:
  assumes "ppos a"
  shows "ppos (padd a b)"
  by (metis Rep_prat Rep_prat_inject assms dual_order.strict_iff_order mem_Collect_eq padd_zero pnone.rep_eq ppos.rep_eq)



lemma pinv_inverts:
  assumes "pgte a b"
      and "ppos b"
    shows "pgte (pinv b) (pinv a)"
proof -
  have "Rep_prat a ≥ Rep_prat b"
    using assms(1) pgte.rep_eq by auto
  then have "(Fract 1 1) / Rep_prat b ≥ (Fract 1 1) / Rep_prat a"
    by (metis One_rat_def assms(2) frac_le le_numeral_extra(4) ppos.rep_eq zero_le_one)
  then show ?thesis
    by (simp add: One_rat_def pdiv.rep_eq pgte.rep_eq pinv_def pwrite.rep_eq)
qed



lemma pinv_pmult_ok:
  assumes "ppos p"
  shows "pmult p (pinv p) = pwrite"
proof -
  obtain r where "r = Rep_prat p" by simp
  then have "r * ((Fract 1 1) / r) = Fract 1 1"
    using assms ppos.rep_eq by force
  then show ?thesis
    by (metis One_rat_def Rep_prat_inject ‹r = Rep_prat p› pdiv.rep_eq pinv_def pmult.rep_eq pwrite.rep_eq)
qed


lemma pinv_pwrite:
  "pinv pwrite = pwrite"
  by (metis Rep_prat_inverse div_by_1 pdiv.rep_eq pinv_def pwrite.rep_eq)

lemma pmult_ppos:
  assumes "ppos a"
      and "ppos b"
    shows "ppos (pmult a b)"
  using assms(1) assms(2) pmult.rep_eq ppos.rep_eq by auto


lemma ppos_inv:
  assumes "ppos p"
  shows "ppos (pinv p)"
by (metis Rep_prat Rep_prat_inverse assms less_eq_rat_def mem_Collect_eq not_one_le_zero pinv_pmult_ok pmult_comm pmult_special(2) pnone.rep_eq ppos.rep_eq pwrite.rep_eq)


lemma pmin_pmax:
  assumes "pgte x (pmin a b)"
  shows "x = pmin (pmax x a) (pmax x b)"
proof (cases "pgte x a")
  case True
  then show ?thesis
    by (metis pmax_is pmax_smaller pmin_comm pmin_is)
next
  case False
  then show ?thesis
    by (metis assms not_pgte_charact pgt_implies_pgte pmax_is pmax_smaller pmin_comm pmin_is)
qed

definition comp_one where
  "comp_one p = (SOME r. padd p r = pwrite)"

lemma padd_comp_one:
  assumes "pgte pwrite x"
  shows "padd x (comp_one x) = pwrite"
  by (metis (mono_tags, lifting) assms comp_one_def p_greater_exists someI_ex)

lemma ppos_eq_pnone:
  "ppos p ⟷ p ≠ pnone"
  by (metis Rep_prat Rep_prat_inject dual_order.strict_iff_order mem_Collect_eq pnone.rep_eq ppos.rep_eq)



lemma pmult_order:
  assumes "pgte a b"
  shows "pgte (pmult p a) (pmult b p)"
  using assms p_greater_exists pmult_comm pmult_distr by force

lemma multiply_smaller_pwrite:
  assumes "pgte pwrite a"
      and "pgte pwrite b"
    shows "pgte pwrite (pmult a b)"
  by (metis assms(1) assms(2) p_greater_exists padd_asso pmult_order pmult_special(1))


lemma pmult_pdiv_cancel:
  assumes "ppos a"
  shows "pmult a (pdiv x a) = x"
  by (metis Rep_prat_inject assms divide_cancel_right dual_order.strict_iff_order nonzero_mult_div_cancel_left pdiv.rep_eq pmult.rep_eq ppos.rep_eq)

lemma pmult_padd:
  "pmult a (padd (pmult b x) (pmult c y)) = padd (pmult (pmult a b) x) (pmult (pmult a c) y)"
  by (metis Rep_prat_inject mult.assoc pmult.rep_eq pmult_distr)


lemma pdiv_smaller:
  assumes "pgte a b"
      and "ppos a"
  shows "pgte pwrite (pdiv b a)"
proof -
  let ?a = "Rep_prat a"
  let ?b = "Rep_prat b"
  have "?b / ?a ≤ 1"
    by (meson assms(1) assms(2) divide_le_eq_1_pos pgte.rep_eq ppos.rep_eq)
  then show ?thesis
    by (simp add: pdiv.rep_eq pgte.rep_eq pwrite.rep_eq)
qed


lemma sum_coeff:
  assumes "ppos a"
      and "ppos b"
    shows "padd (pdiv a (padd a b)) (pdiv b (padd a b)) = pwrite"
proof -
  let ?a = "Rep_prat a"
  let ?b = "Rep_prat b"
  have "(?a / (?a + ?b)) + (?b / (?a + ?b)) = 1"
    by (metis add_divide_distrib add_pos_pos assms(1) assms(2) less_irrefl ppos.rep_eq right_inverse_eq)
  then show ?thesis
    by (metis Rep_prat_inject padd.rep_eq pdiv.rep_eq pwrite.rep_eq)
qed

lemma padd_one_ineq_sum:
  assumes "padd a b = pwrite"
      and "pgte x aa"
      and "pgte x bb"
    shows "pgte x (padd (pmult a aa) (pmult b bb))"
  by (metis (mono_tags, lifting) Rep_prat assms(1) assms(2) assms(3) convex_bound_le mem_Collect_eq padd.rep_eq pgte.rep_eq pmult.rep_eq pwrite.rep_eq)


end
class="head">

Theory Mask

subsection ‹Permission masks: Maps from heap locations to permission amounts›

theory Mask
  imports PosRat
begin

subsubsection ‹Definitions›

type_synonym field = string
type_synonym address = nat
type_synonym heap_loc = "address × field"

type_synonym mask = "heap_loc ⇒ prat"
type_synonym bmask = "heap_loc ⇒ bool"

definition null where "null = 0"

definition full_mask :: "mask" where
  "full_mask hl = (if fst hl = null then pnone else pwrite)"


definition multiply_mask :: "prat ⇒ mask ⇒ mask" where
  "multiply_mask p π hl = pmult p (π hl)"

fun empty_mask where
  "empty_mask hl = pnone"

fun empty_bmask where
  "empty_bmask hl = False"

fun add_acc where "add_acc π hl p = π(hl := padd (π hl) p)"

inductive rm_acc where
  "π hl = padd p r ⟹ rm_acc π hl p (π(hl := r))"

fun add_masks where
  "add_masks π' π hl = padd (π' hl) (π hl)"

definition greater_mask where
  "greater_mask π' π ⟷ (∃r. π' = add_masks π r)"

fun uni_mask where
  "uni_mask hl p = empty_mask(hl := p)"

fun valid_mask :: "mask ⇒ bool" where
  "valid_mask π ⟷ (∀hl. pgte pwrite (π hl)) ∧ (∀f. π (null, f) = pnone)"

definition valid_null :: "mask ⇒ bool" where
  "valid_null π ⟷ (∀f. π (null, f) = pnone)"

definition equal_on_mask where
  "equal_on_mask π h h' ⟷ (∀hl. ppos (π hl) ⟶ h hl = h' hl)"

definition equal_on_bmask where
  "equal_on_bmask π h h' ⟷ (∀hl. π hl ⟶ h hl = h' hl)"

definition big_add_masks where
  "big_add_masks Π Π' h = add_masks (Π h) (Π' h)"

definition big_greater_mask where
  "big_greater_mask Π Π' ⟷ (∀h. greater_mask (Π h) (Π' h))"

definition greater_bmask where
  "greater_bmask H H' ⟷ (∀h. H' h ⟶ H h)"

definition update_dm where
  "update_dm dm π π' hl ⟷ (dm hl ∨ pgt (π hl) (π' hl))"

fun pre_get_m where "pre_get_m φ = fst φ"
fun pre_get_h where "pre_get_h φ = snd φ"
fun srm_acc where "srm_acc φ hl p = (rm_acc (pre_get_m φ) hl p, pre_get_h φ)"


datatype val = Bool (the_bool: bool) | Address (the_address: address) | Rat (the_rat: prat)

definition upper_bounded :: "mask ⇒ prat ⇒ bool" where
  "upper_bounded π p ⟷ (∀hl. pgte p (π hl))"




subsubsection ‹Lemmas›

lemma ssubsetI:
  assumes "⋀π h. (π, h) ∈ A ⟹ (π, h) ∈ B"
  shows "A ⊆ B"
  using assms by auto

lemma double_inclusion:
  assumes "A ⊆ B"
      and "B ⊆ A"
    shows "A = B"
  using assms by blast

lemma add_masks_comm:
  "add_masks a b = add_masks b a"
proof (rule ext)
  fix x show "add_masks a b x = add_masks b a x"
    by (metis Rep_prat_inverse add.commute add_masks.simps padd.rep_eq)
qed

lemma add_masks_asso:
  "add_masks (add_masks a b) c = add_masks a (add_masks b c)"
proof (rule ext)
  fix x show "add_masks (add_masks a b) c x = add_masks a (add_masks b c) x"
    by (metis Rep_prat_inverse add.assoc add_masks.simps padd.rep_eq)
qed

lemma minus_empty:
  "π = add_masks π empty_mask"
proof (rule ext)
  fix x show "π x = add_masks π empty_mask x"
    by (metis Rep_prat_inverse add.right_neutral add_masks.simps empty_mask.simps padd.rep_eq pnone.rep_eq)
qed

lemma add_acc_uni_mask:
  "add_acc π hl p = add_masks π (uni_mask hl p)"
proof (rule ext)
  fix x show "add_acc π hl p x = add_masks π (uni_mask hl p) x"
    by (metis (no_types, opaque_lifting) add_acc.simps add_masks.simps fun_upd_apply minus_empty uni_mask.simps)
qed

lemma add_masks_equiv_valid_null:
  "valid_null (add_masks a b) ⟷ valid_null a ∧ valid_null b"
  by (metis (mono_tags, lifting) add_masks.simps padd_zero valid_null_def)

lemma valid_maskI:
  assumes "⋀hl. pgte pwrite (π hl)"
      and "⋀f. π (null, f) = pnone"
    shows "valid_mask π"
  by (simp add: assms(1) assms(2))

lemma greater_mask_equiv_def:
  "greater_mask π' π ⟷ (∀hl. pgte (π' hl) (π hl))"
  (is "?A ⟷ ?B")
proof (rule iffI)
  show "?A ⟹ ?B"
  proof (clarify)
    fix hl assume "greater_mask π' π"
    then obtain r where "π' = add_masks π r"
      using greater_mask_def by blast
    then show "pgte (π' hl) (π hl)"
      using Rep_prat padd.rep_eq pgte.rep_eq by auto
  qed
  show "?B ⟹ ?A"
  proof -
    assume ?B
    let ?r = "λhl. (SOME p. π' hl = padd (π hl) p)"
    have "π' = add_masks π ?r"
    proof (rule ext)
      fix hl
      have "π' hl = padd (π hl) (?r hl)"
        by (meson ‹∀hl. pgte (π' hl) (π hl)› p_greater_exists someI_ex)
      then show "π' hl = add_masks π ?r hl"
        by auto
    qed
    then show ?A
      using greater_mask_def by blast
  qed
qed

lemma greater_maskI:
  assumes "⋀hl. pgte (π' hl) (π hl)"
  shows "greater_mask π' π"
  by (simp add: assms greater_mask_equiv_def)

lemma greater_mask_properties:
  "greater_mask π π"
  "greater_mask a b ∧ greater_mask b c ⟹ greater_mask a c"
  "greater_mask π' π ∧ greater_mask π π' ⟹ π = π'"
  apply (simp add: greater_maskI pgte.rep_eq)
  apply (metis add_masks_asso greater_mask_def)
proof (rule ext)
  fix x assume "greater_mask π' π ∧ greater_mask π π'"
  show "π x = π' x"
    by (meson ‹greater_mask π' π ∧ greater_mask π π'› greater_mask_equiv_def pgte_antisym)
qed

lemma greater_mask_decomp:
  assumes "greater_mask a (add_masks b c)"
  shows "∃a1 a2. a = add_masks a1 a2 ∧ greater_mask a1 b ∧ greater_mask a2 c"
  by (metis add_masks_asso assms greater_mask_def greater_mask_properties(1))

lemma valid_empty:
  "valid_mask empty_mask"
  by (metis empty_mask.simps le_add_same_cancel1 p_greater_exists padd.rep_eq pgte.rep_eq pnone.rep_eq valid_mask.simps)

lemma upper_valid_aux:
  assumes "valid_mask a"
      and "a = add_masks b c"
    shows "valid_mask b"
proof (rule valid_maskI)
  show "⋀hl. pgte pwrite (b hl)"
    using assms(1) assms(2) p_greater_exists padd_asso by fastforce
  fix f show " b (null, f) = pnone"
    by (metis add_masks_comm assms(1) assms(2) empty_mask.simps greater_mask_def greater_mask_equiv_def minus_empty pgte_antisym valid_mask.simps)
qed

lemma upper_valid:
  assumes "valid_mask a"
      and "a = add_masks b c"
    shows "valid_mask b ∧ valid_mask c"
  using add_masks_comm assms(1) assms(2) upper_valid_aux by blast

lemma equal_on_bmaskI:
  assumes "⋀hl. π hl ⟹ h hl = h' hl"
  shows "equal_on_bmask π h h'"
  using assms equal_on_bmask_def by blast

lemma big_add_greater:
  "big_greater_mask (big_add_masks A B) B"
  by (metis add_masks_comm big_add_masks_def big_greater_mask_def greater_mask_def)

lemma big_greater_iff:
  "big_greater_mask A B ⟹ (∃C. A = big_add_masks B C)"
proof -
  assume "big_greater_mask A B"
  let ?C = "λh. SOME r. A h = add_masks (B h) r"
  have "A = big_add_masks B ?C"
  proof (rule ext)
    fix x
    have "A x = add_masks (B x) (?C x)"
    proof (rule ext)
      fix xa 
      have "A x = add_masks (B x) (SOME r. A x = add_masks (B x) r)"
        by (metis (mono_tags, lifting) ‹big_greater_mask A B› big_greater_mask_def greater_mask_def someI_ex)
      then show "A x xa = add_masks (B x) (SOME r. A x = add_masks (B x) r) xa"
        by auto
    qed
    then show "A x = big_add_masks B (λh. SOME r. A h = add_masks (B h) r) x"
      by (metis (no_types, lifting) big_add_masks_def)
  qed
  then show "∃C. A = big_add_masks B C"
    by fast
qed

lemma big_add_masks_asso:
  "big_add_masks A (big_add_masks B C) = big_add_masks (big_add_masks A B) C"
proof (rule ext)
  fix x show "big_add_masks A (big_add_masks B C) x = big_add_masks (big_add_masks A B) C x"
    by (simp add: add_masks_asso big_add_masks_def)
qed

lemma big_add_mask_neutral:
  "big_add_masks Π (λ_. empty_mask) = Π"
proof (rule ext)
  fix x show "big_add_masks Π (λ_. empty_mask) x = Π x"
    by (metis big_add_masks_def minus_empty)
qed

lemma sym_equal_on_mask:
  "equal_on_mask π a b ⟷ equal_on_mask π b a"
proof -
  have "⋀a b. equal_on_mask π a b ⟹ equal_on_mask π b a"
    by (simp add: equal_on_mask_def)
  then show ?thesis by blast
qed

lemma greater_mask_uni_equiv:
  "greater_mask π (uni_mask hl r) ⟷ pgte (π hl) r"
  by (metis add_masks_comm fun_upd_apply greater_mask_def greater_mask_equiv_def minus_empty uni_mask.simps)

lemma greater_mask_uniI:
  assumes "pgte (π hl) r"
  shows "greater_mask π (uni_mask hl r)"
  using greater_mask_uni_equiv assms by metis

lemma greater_bmask_refl:
  "greater_bmask H H"
  by (simp add: greater_bmask_def)

lemma greater_bmask_trans:
  assumes "greater_bmask A B"
      and "greater_bmask B C"
    shows "greater_bmask A C"
  by (metis assms(1) assms(2) greater_bmask_def)

lemma update_dm_same:
  "update_dm dm π π = dm"
proof (rule ext)
  fix x show "update_dm dm π π x = dm x"
    by (simp add: pgt.rep_eq update_dm_def)
qed

lemma update_trans:
  assumes "greater_mask π π'"
      and "greater_mask π' π''"
  shows "update_dm (update_dm dm π π') π' π'' = update_dm dm π π''"
proof (rule ext)
  fix hl show "update_dm (update_dm dm π π') π' π'' hl = update_dm dm π π'' hl"
  proof -
    have "update_dm (update_dm dm π π') π' π'' hl ⟷ (update_dm dm π π') hl ∨ pgt (π' hl) (π'' hl)"
      using update_dm_def by metis
    also have "... ⟷ dm hl ∨ pgt (π hl) (π' hl) ∨ pgt (π' hl) (π'' hl)"
      using update_dm_def by metis
    moreover have "update_dm dm π π'' hl ⟷ dm hl ∨ pgt (π hl) (π'' hl)"
      using update_dm_def by metis
    moreover have "pgt (π hl) (π' hl) ∨ pgt (π' hl) (π'' hl) ⟷ pgt (π hl) (π'' hl)"
    proof
      show "pgt (π hl) (π' hl) ∨ pgt (π' hl) (π'' hl) ⟹ pgt (π hl) (π'' hl)"
        by (metis assms(1) assms(2) greater_mask_equiv_def greater_mask_properties(2) not_pgte_charact pgte_antisym)
      show "pgt (π hl) (π'' hl) ⟹ pgt (π hl) (π' hl) ∨ pgt (π' hl) (π'' hl)"
        by (metis assms(1) greater_mask_equiv_def not_pgte_charact pgte_antisym)
    qed
    ultimately show ?thesis by blast
  qed
qed

lemma equal_on_bmask_greater:
  assumes "equal_on_bmask π' h h'"
      and "greater_bmask π' π"
    shows "equal_on_bmask π h h'"
  by (metis (mono_tags, lifting) assms(1) assms(2) equal_on_bmask_def greater_bmask_def)

lemma update_dm_equal_bmask:
  assumes "π = add_masks π' m"   
  shows "equal_on_bmask (update_dm dm π π') h' h ⟷ equal_on_mask m h h' ∧ equal_on_bmask dm h h'"
proof -
  have "equal_on_bmask (update_dm dm π π') h' h ⟷ (∀hl. update_dm dm π π' hl ⟶ h' hl = h hl)"
    by (simp add: equal_on_bmask_def)
  moreover have "⋀hl. update_dm dm π π' hl ⟷ dm hl ∨ pgt (π hl) (π' hl)"
    by (simp add: update_dm_def)
  moreover have "(∀hl. update_dm dm π π' hl ⟶ h' hl = h hl) ⟷ equal_on_mask m h h' ∧ equal_on_bmask dm h h'"
  proof
    show "∀hl. update_dm dm π π' hl ⟶ h' hl = h hl ⟹ equal_on_mask m h h' ∧ equal_on_bmask dm h h'"
      by (simp add: assms equal_on_bmask_def equal_on_mask_def padd.rep_eq pgt.rep_eq ppos.rep_eq update_dm_def)
    assume "equal_on_mask m h h' ∧ equal_on_bmask dm h h'"
    then have "⋀hl. update_dm dm π π' hl ⟹ h' hl = h hl"
      by (metis (full_types) add.right_neutral add_masks.simps assms dual_order.strict_iff_order equal_on_bmask_def equal_on_mask_def padd.rep_eq pgt.rep_eq pnone.rep_eq ppos_eq_pnone update_dm_def)
    then show "∀hl. update_dm dm π π' hl ⟶ h' hl = h hl"
      by simp
  qed
  then show ?thesis
    by (simp add: calculation)
qed

lemma const_sum_mask_greater:
  assumes "add_masks a b = add_masks c d"
      and "greater_mask a c"
    shows "greater_mask d b"
proof (rule ccontr)
  assume "¬ greater_mask d b"
  then obtain hl where "¬ pgte (d hl) (b hl)"
    using greater_mask_equiv_def by blast
  then have "pgt (b hl) (d hl)"
    using not_pgte_charact by auto
  then have "pgt (padd (a hl) (b hl)) (padd (c hl) (d hl))"
    by (metis assms(2) greater_mask_equiv_def padd_comm pgte_pgt)
  then show "False"
    by (metis add_masks.simps assms(1) not_pgte_charact order_refl pgte.rep_eq)
qed

lemma add_masks_cancellative:
  assumes "add_masks b c = add_masks b d"
    shows "c = d"
proof (rule ext)
  fix x show "c x = d x"
    by (metis assms(1) const_sum_mask_greater greater_mask_properties(1) greater_mask_properties(3))
qed

lemma equal_on_maskI:
  assumes "⋀hl. ppos (π hl) ⟹ h hl = h' hl"
  shows "equal_on_mask π h h'"
  by (simp add: assms equal_on_mask_def)

lemma greater_equal_on_mask:
  assumes "equal_on_mask π' h h'"
      and "greater_mask π' π"
    shows "equal_on_mask π h h'"
proof (rule equal_on_maskI)
  fix hl assume asm: "ppos (π hl)"
  then show "h hl = h' hl"
    by (metis assms(1) assms(2) equal_on_mask_def greater_mask_equiv_def less_le_trans pgte.rep_eq ppos.rep_eq)
qed

lemma equal_on_mask_sum:
  "equal_on_mask π1 h h' ∧ equal_on_mask π2 h h' ⟷ equal_on_mask (add_masks π1 π2) h h'"
proof
  show "equal_on_mask (add_masks π1 π2) h h' ⟹ equal_on_mask π1 h h' ∧ equal_on_mask π2 h h'"
    using add_masks_comm greater_equal_on_mask greater_mask_def by blast
  assume "equal_on_mask π1 h h' ∧ equal_on_mask π2 h h'"
  show "equal_on_mask (add_masks π1 π2) h h'"
  proof (rule equal_on_maskI)
    fix hl assume "ppos (add_masks π1 π2 hl)"
    then show "h hl = h' hl"
    proof (cases "ppos (π1 hl)")
      case True
      then show ?thesis
        by (meson ‹equal_on_mask π1 h h' ∧ equal_on_mask π2 h h'› equal_on_mask_def)
    next
      case False
      then show ?thesis
        by (metis ‹equal_on_mask π1 h h' ∧ equal_on_mask π2 h h'› ‹ppos (add_masks π1 π2 hl)› add_masks.simps equal_on_mask_def padd_zero ppos_eq_pnone)
    qed
  qed
qed

lemma valid_larger_mask:
  "valid_mask π ⟷ greater_mask full_mask π "
  by (metis fst_eqD full_mask_def greater_maskI greater_mask_def not_one_le_zero not_pgte_charact pgt_implies_pgte pgte.rep_eq pnone.rep_eq pwrite.rep_eq surjective_pairing upper_valid_aux valid_mask.elims(1))

lemma valid_mask_full_mask:
  "valid_mask full_mask"
  using greater_mask_properties(1) valid_larger_mask by blast

lemma mult_greater:
  assumes "greater_mask a b"
  shows "greater_mask (multiply_mask p a) (multiply_mask p b)"
  by (metis (full_types) assms greater_mask_equiv_def multiply_mask_def p_greater_exists pmult_distr)

lemma mult_write_mask:
  "multiply_mask pwrite π = π"
proof (rule ext)
  fix x show "multiply_mask pwrite π x = π x"
    by (simp add: multiply_mask_def pmult_special(1))
qed

lemma mult_distr_masks:
  "multiply_mask a (add_masks b c) = add_masks (multiply_mask a b) (multiply_mask a c)"
proof (rule ext)
  fix x show "multiply_mask a (add_masks b c) x = add_masks (multiply_mask a b) (multiply_mask a c) x"
    by (simp add: multiply_mask_def pmult_distr)
qed

lemma mult_add_states:
  "multiply_mask (padd a b) π = add_masks (multiply_mask a π) (multiply_mask b π)"
proof (rule ext)
  fix x show "multiply_mask (padd a b) π x = add_masks (multiply_mask a π) (multiply_mask b π) x"    
    by (simp add: multiply_mask_def pmult_comm pmult_distr)
qed

lemma upper_boundedI:
  assumes "⋀hl. pgte p (π hl)"
  shows "upper_bounded π p"
  by (simp add: assms upper_bounded_def)

lemma upper_bounded_smaller:
  assumes "upper_bounded π a"
  shows "upper_bounded (multiply_mask p π) (pmult p a)"  
  by (metis assms multiply_mask_def p_greater_exists pmult_distr upper_bounded_def)

lemma upper_bounded_bigger:
  assumes "upper_bounded π a"
      and "pgte b a"
    shows "upper_bounded π b"
  by (meson assms(1) assms(2) order_trans pgte.rep_eq upper_bounded_def)


lemma valid_mult:
  assumes "valid_mask π"
      and "pgte pwrite p"
    shows "valid_mask (multiply_mask p π)"
proof (rule valid_maskI)
  have "upper_bounded π pwrite"
    using assms(1) upper_bounded_def by auto
  then have "upper_bounded (multiply_mask p π) (pmult p pwrite)"
    by (simp add: upper_bounded_smaller)
  then show "⋀hl. pgte pwrite (multiply_mask p π hl)"
    by (metis assms(2) pmult_comm pmult_special(1) upper_bounded_bigger upper_bounded_def)
  show "⋀f. multiply_mask p π (null, f) = pnone"
    by (metis Rep_prat_inverse add_0_left assms(1) multiply_mask_def padd.rep_eq padd_cancellative pmult_distr pnone.rep_eq valid_mask.elims(1))
qed

lemma valid_sum:
  assumes "valid_mask a"
      and "valid_mask b"
      and "upper_bounded a ma"
      and "upper_bounded b mb"
      and "pgte pwrite (padd ma mb)"
    shows "valid_mask (add_masks a b)"
      and "upper_bounded (add_masks a b) (padd ma mb)"
proof (rule valid_maskI)
  show "⋀hl. pgte pwrite (add_masks a b hl)"
  proof -
    fix hl 
    have "pgte (padd ma mb) (add_masks a b hl)"
      by (metis (mono_tags, lifting) add_masks.simps add_mono_thms_linordered_semiring(1) assms(3) assms(4) padd.rep_eq pgte.rep_eq upper_bounded_def)
    then show "pgte pwrite (add_masks a b hl)"
      by (meson assms(5) dual_order.trans pgte.rep_eq)
  qed
  show "⋀f. add_masks a b (null, f) = pnone"
    by (metis Rep_prat_inverse add_0_left add_masks.simps assms(1) assms(2) padd.rep_eq pnone.rep_eq valid_mask.simps)
  show "upper_bounded (add_masks a b) (padd ma mb)"
    using add_mono_thms_linordered_semiring(1) assms(3) assms(4) padd.rep_eq pgte.rep_eq upper_bounded_def by fastforce
qed

lemma valid_multiply:
  assumes "valid_mask a"
      and "upper_bounded a ma"
      and "pgte pwrite (pmult ma p)"
    shows "valid_mask (multiply_mask p a)"
  by (metis (no_types, opaque_lifting) assms(1) assms(2) assms(3) multiply_mask_def pmult_comm pmult_special(2) upper_bounded_bigger upper_bounded_def upper_bounded_smaller valid_mask.elims(1))

lemma greater_mult:
  assumes "greater_mask a b"
  shows "greater_mask (multiply_mask p a) (multiply_mask p b)"
  by (metis Rep_prat assms greater_mask_equiv_def mem_Collect_eq mult_left_mono multiply_mask_def pgte.rep_eq pmult.rep_eq)

end
ody>

Theory PartialHeapSA

subsection ‹Partial heaps: Partial maps from heap location to values›

theory PartialHeapSA
  imports Mask "Package_logic.PackageLogic"
begin

subsubsection ‹Definitions›

type_synonym heap = "heap_loc ⇀ val"
type_synonym pre_state = "mask × heap"

definition valid_heap :: "mask ⇒ heap ⇒ bool" where
  "valid_heap π h ⟷ (∀hl. ppos (π hl) ⟶ h hl ≠ None)"

fun valid_state :: "pre_state ⇒ bool" where
  "valid_state (π, h) ⟷ valid_mask π ∧ valid_heap π h"

lemma valid_stateI:
  assumes "valid_mask π"
      and "⋀hl. ppos (π hl) ⟹ h hl ≠ None"
    shows "valid_state (π, h)"
  using assms(1) assms(2) valid_heap_def valid_state.simps by blast

definition empty_heap where "empty_heap hl = None"

lemma valid_pre_unit:
  "valid_state (empty_mask, empty_heap)"
  using pnone.rep_eq ppos.rep_eq valid_empty valid_stateI by fastforce

typedef state = "{ φ |φ. valid_state φ }"
  using valid_pre_unit by blast

fun get_m :: "state ⇒ mask" where "get_m a = fst (Rep_state a)"
fun get_h :: "state ⇒ heap" where "get_h a = snd (Rep_state a)"

fun compatible_options where
  "compatible_options (Some a) (Some b) ⟷ a = b"
| "compatible_options _ _ ⟷ True"

definition compatible_heaps :: "heap ⇒ heap ⇒ bool" where
  "compatible_heaps h h' ⟷ (∀hl. compatible_options (h hl) (h' hl))"

definition compatible :: "pre_state ⇒ pre_state ⇒ bool" where
  "compatible φ φ' ⟷ compatible_heaps (snd φ) (snd φ') ∧ valid_mask (add_masks (fst φ) (fst φ'))"

fun add_states :: "pre_state ⇒ pre_state ⇒ pre_state" where
  "add_states (π, h) (π', h') = (add_masks π π', h ++ h')"

definition larger_heap where
  "larger_heap h' h ⟷ (∀hl x. h hl = Some x ⟶ h' hl = Some x)"

definition unit :: "state" where
  "unit = Abs_state (empty_mask, empty_heap)"

definition plus :: "state ⇒ state ⇀ state" (infixl "⊕" 63) where
  "a ⊕ b = (if compatible (Rep_state a) (Rep_state b) then Some (Abs_state (add_states (Rep_state a) (Rep_state b))) else None)"

definition core :: "state ⇒ state" (" |_| ") where
  "core φ = Abs_state (empty_mask, get_h φ)"

definition stable :: "state ⇒ bool" where
  "stable φ ⟷ (∀hl. ppos (get_m φ hl) ⟷ get_h φ hl ≠ None)"








subsubsection Lemmas

lemma valid_heapI:
  assumes "⋀hl. ppos (π hl) ⟹ h hl ≠ None"
  shows "valid_heap π h"
  using assms valid_heap_def by presburger

lemma valid_state_decompose:
  assumes "valid_state (add_masks a b, h)"
  shows "valid_state (a, h)"
proof (rule valid_stateI)
  show "valid_mask a"
    using assms upper_valid_aux valid_state.simps by blast
  fix hl assume "ppos (a hl)" then show "h hl ≠ None"
    by (metis add_masks.simps assms ppos_add valid_heap_def valid_state.simps)
qed

lemma compatible_heapsI:
  assumes "⋀hl a b. h hl = Some a ⟹ h' hl = Some b ⟹ a = b"
  shows "compatible_heaps h h'"
  by (metis assms compatible_heaps_def compatible_options.elims(3))

lemma compatibleI_old:
  assumes "⋀hl x y. snd φ hl = Some x ∧ snd φ' hl = Some y ⟹ x = y"
      and "valid_mask (add_masks (fst φ) (fst φ'))"
    shows "compatible φ φ'"
  using assms(1) assms(2) compatible_def compatible_heapsI by presburger

lemma larger_heap_anti:
  assumes "larger_heap a b"
      and "larger_heap b a"
    shows "a = b"
proof (rule ext)
  fix x show "a x = b x"
  proof (cases "a x")
    case None
    then show ?thesis
      by (metis assms(1) larger_heap_def not_None_eq)
  next
    case (Some a)
    then show ?thesis
      by (metis assms(2) larger_heap_def)
  qed
qed

lemma larger_heapI:
  assumes "⋀hl x. h hl = Some x ⟹ h' hl = Some x"
  shows "larger_heap h' h"
  by (simp add: assms larger_heap_def)

lemma larger_heap_refl:
  "larger_heap h h"
  using larger_heap_def by blast

lemma compatible_heaps_comm:
  assumes "compatible_heaps a b"
  shows "a ++ b = b ++ a"
proof (rule ext)
  fix x show "(a ++ b) x = (b ++ a) x"
  proof (cases "a x")
    case None
    then show ?thesis
      by (simp add: domIff map_add_dom_app_simps(2) map_add_dom_app_simps(3))
  next
    case (Some a)
    then show ?thesis
      by (metis (no_types, lifting) assms compatible_heaps_def compatible_options.elims(2) map_add_None map_add_dom_app_simps(1) map_add_dom_app_simps(3))
  qed
qed

lemma larger_heaps_sum_ineq:
  assumes "larger_heap a' a"
      and "larger_heap b' b"
      and "compatible_heaps a' b'"
    shows "larger_heap (a' ++ b') (a ++ b)"
proof (rule larger_heapI)
  fix hl x assume "(a ++ b) hl = Some x"
  show "(a' ++ b') hl = Some x"
  proof (cases "a hl")
    case None
    then show ?thesis
      by (metis ‹(a ++ b) hl = Some x› assms(2) larger_heap_def map_add_SomeD map_add_find_right)
  next
    case (Some aa)
    then show ?thesis
      by (metis (mono_tags, lifting) ‹(a ++ b) hl = Some x› assms(1) assms(2) assms(3) compatible_heaps_comm larger_heap_def map_add_Some_iff)
  qed
qed

lemma larger_heap_trans:
  assumes "larger_heap a b"
      and "larger_heap b c"
    shows "larger_heap a c"
  by (metis (no_types, opaque_lifting) assms(1) assms(2) larger_heap_def)

lemma larger_heap_comp:
  assumes "larger_heap a b"
      and "compatible_heaps a c"
    shows "compatible_heaps b c"
proof (rule compatible_heapsI)
  fix hl a ba
  assume "b hl = Some a" "c hl = Some ba"
  then show "a = ba"
    by (metis assms(1) assms(2) compatible_heaps_def compatible_options.simps(1) larger_heap_def)
qed

lemma larger_heap_plus:
  assumes "larger_heap a b"
      and "larger_heap a c"
    shows "larger_heap a (b ++ c)"
proof (rule larger_heapI)
  fix hl x assume "(b ++ c) hl = Some x"
  then show "a hl = Some x"
  proof (cases "b hl")
    case None
    then show ?thesis
      by (metis ‹(b ++ c) hl = Some x› assms(2) larger_heap_def map_add_SomeD)
  next
    case (Some bb)
    then show ?thesis
      by (metis ‹(b ++ c) hl = Some x› assms(1) assms(2) larger_heap_def map_add_SomeD)
  qed
qed

lemma compatible_heaps_sum:
  assumes "compatible_heaps a b"
      and "compatible_heaps a c"
    shows "compatible_heaps a (b ++ c)"
  by (metis (no_types, opaque_lifting) assms(1) assms(2) compatible_heaps_def map_add_dom_app_simps(1) map_add_dom_app_simps(3))

lemma larger_compatible_sum_heaps:
  assumes "larger_heap a x"
      and "larger_heap b y"
      and "compatible_heaps a b"
    shows "compatible_heaps x y"
proof (rule compatible_heapsI)
  fix hl a b assume "x hl = Some a" "y hl = Some b"
  then show "a = b"
    by (metis assms(1) assms(2) assms(3) compatible_heaps_def compatible_options.simps(1) larger_heap_def)
qed

lemma get_h_m:
  "Rep_state x = (get_m x, get_h x)" by simp

lemma get_pre:
  "get_h x = snd (Rep_state x)"
  "get_m x = fst (Rep_state x)"
  by simp_all

lemma plus_ab_defined:
  "φ ⊕ φ' ≠ None ⟷ compatible_heaps (get_h φ) (get_h φ') ∧ valid_mask (add_masks (get_m φ) (get_m φ'))"
  (is "?A ⟷ ?B")
proof
  show "?A ⟹ ?B"
    by (metis compatible_def get_pre(1) get_pre(2) plus_def)
  show "?B ⟹ ?A"
    using compatible_def plus_def by auto
qed

lemma plus_charact:
  assumes "a ⊕ b = Some x"
    shows "get_m x = add_masks (get_m a) (get_m b)"
      and "get_h x = (get_h a) ++ (get_h b)"
proof -
  have "x = (Abs_state (add_states (Rep_state a) (Rep_state b)))"
    by (metis assms option.discI option.inject plus_def)
  moreover have "compatible (Rep_state a) (Rep_state b)"
    using assms(1) plus_def by (metis option.discI)

  moreover have "valid_state (add_states (Rep_state a) (Rep_state b))"
  proof -
    have "valid_state (add_masks (get_m a) (get_m b), (get_h a) ++ (get_h b))"
    proof (rule valid_stateI)
      show "valid_mask (add_masks (get_m a) (get_m b))"
        using calculation(2) compatible_def by fastforce
      fix hl assume "ppos (add_masks (get_m a) (get_m b) hl)"
      then show "(get_h a ++ get_h b) hl ≠ None"
      proof (cases "ppos (get_m a hl)")
        case True
        then show ?thesis
          by (metis Rep_state get_h_m map_add_None mem_Collect_eq valid_heap_def valid_state.simps)
      next
        case False
        then have "ppos (get_m b hl)"
          using ‹ppos (add_masks (get_m a) (get_m b) hl)› padd.rep_eq ppos.rep_eq by auto
        then show ?thesis
          by (metis Rep_state get_h_m map_add_None mem_Collect_eq valid_heap_def valid_state.simps)
      qed
    qed
    then show ?thesis
      using add_states.simps get_h_m by presburger
  qed
  ultimately show "get_m x = add_masks (get_m a) (get_m b)"
    by (metis Abs_state_inverse add_states.simps fst_conv get_h_m mem_Collect_eq)

  show "get_h x = (get_h a) ++ (get_h b)"
    by (metis Abs_state_inject CollectI Rep_state Rep_state_inverse ‹valid_state (add_states (Rep_state a) (Rep_state b))› ‹x = Abs_state (add_states (Rep_state a) (Rep_state b))› add_states.simps eq_snd_iff get_h.simps)
qed

lemma commutative:
  "a ⊕ b = b ⊕ a"
proof (cases "compatible_heaps (get_h a) (get_h b) ∧ valid_mask (add_masks (get_m a) (get_m b))")
  case True
  then have "compatible_heaps (get_h b) (get_h a) ∧ add_masks (get_m a) (get_m b) = add_masks (get_m b) (get_m a)"
    by (metis add_masks_comm compatible_heapsI compatible_heaps_def compatible_options.simps(1))
  then have "(get_h a) ++ (get_h b) = (get_h b) ++ (get_h a)"
    by (simp add: compatible_heaps_comm)
  then show ?thesis
    by (metis True ‹compatible_heaps (get_h b) (get_h a) ∧ add_masks (get_m a) (get_m b) = add_masks (get_m b) (get_m a)› add_states.simps get_h_m plus_ab_defined plus_def)
next
  case False
  then show ?thesis
    by (metis add_masks_comm compatible_heapsI compatible_heaps_def compatible_options.simps(1) plus_ab_defined)
qed

lemma asso1:
  assumes "a ⊕ b = Some ab ∧ b ⊕ c = Some bc"
  shows "ab ⊕ c = a ⊕ bc"
proof (cases "ab ⊕ c")
  case None
  then show ?thesis
  proof (cases "compatible_heaps (get_h ab) (get_h c)")
    case True
    then have "¬ valid_mask (add_masks (add_masks (get_m a) (get_m b)) (get_m c))"
      by (metis None assms plus_ab_defined plus_charact(1))
    then show ?thesis
      by (metis add_masks_asso assms plus_ab_defined plus_charact(1))
  next
    case False
    then have "¬ compatible_heaps (get_h a ++ get_h b) (get_h c)"
      using assms plus_charact(2) by force
    then obtain l x y where "(get_h a ++ get_h b) l = Some x" "get_h c l = Some y" "x ≠ y"
      using compatible_heapsI by blast
    then have "¬ compatible_heaps (get_h a) (get_h b ++ get_h c)"
    proof (cases "get_h a l")
      case None
      then show ?thesis
        by (metis ‹(get_h a ++ get_h b) l = Some x› ‹get_h c l = Some y› ‹x ≠ y› assms compatible_heaps_comm map_add_dom_app_simps(1) map_add_dom_app_simps(3) map_add_find_right option.inject option.simps(3) plus_ab_defined)
    next
      case (Some aa)
      then show ?thesis
        by (metis ‹(get_h a ++ get_h b) l = Some x› ‹get_h c l = Some y› ‹x ≠ y› assms commutative compatible_heaps_def compatible_options.elims(2) map_add_find_right option.inject option.simps(3) plus_charact(2))
    qed
    then show ?thesis
      by (metis None assms plus_ab_defined plus_charact(2))
  qed
next
  case (Some x)
  then have "compatible_heaps (get_h a ++ get_h b) (get_h c)"
    by (metis assms option.simps(3) plus_ab_defined plus_charact(2))
  then have "compatible_heaps (get_h a) (get_h b ++ get_h c)"
    by (metis (full_types) assms compatible_heaps_comm compatible_heaps_def compatible_heaps_sum compatible_options.simps(2) domIff map_add_dom_app_simps(1) option.distinct(1) plus_ab_defined)
  moreover have "valid_mask (add_masks (get_m a) (add_masks (get_m b) (get_m c)))"
    by (metis Some add_masks_asso assms option.distinct(1) plus_ab_defined plus_charact(1))
  ultimately obtain y where "Some y = a ⊕ bc"
    by (metis assms plus_ab_defined plus_charact(1) plus_charact(2) plus_def)
  then show ?thesis
    by (metis (mono_tags, lifting) Some add_masks_asso add_states.simps assms get_h_m map_add_assoc option.distinct(1) plus_charact(1) plus_charact(2) plus_def)
qed

lemma asso2:
  assumes "a ⊕ b = Some ab ∧ b ⊕ c = None"
  shows " ab ⊕ c = None"
proof (cases "valid_mask (add_masks (get_m b) (get_m c))")
  case True
  then have "¬ compatible_heaps (get_h b) (get_h c)"
    using assms plus_ab_defined by blast
  then obtain l x y where "get_h b l = Some x" "get_h c l = Some y" "x ≠ y"
    using compatible_heapsI by blast
  then have "get_h ab l = Some x"
    by (metis assms map_add_find_right plus_charact(2))
  then show ?thesis
    by (metis ‹get_h c l = Some y› ‹x ≠ y› compatible_heaps_def compatible_options.simps(1) plus_ab_defined)
next
  case False
  then obtain l where "¬ (pgte pwrite (add_masks (get_m b) (get_m c) l))"
    by (metis Abs_state_cases Rep_state_cases Rep_state_inverse add_masks_equiv_valid_null get_h_m mem_Collect_eq valid_mask.simps valid_null_def valid_state.simps)
  then have "¬ (pgte pwrite (add_masks (get_m ab) (get_m c) l))"
  proof -
    have "pgte (add_masks (get_m ab) (get_m c) l) (add_masks (get_m b) (get_m c) l)"
      using assms p_greater_exists padd_asso padd_comm plus_charact(1) by auto
    then show ?thesis
      by (meson ‹¬ pgte pwrite (add_masks (get_m b) (get_m c) l)› order_trans pgte.rep_eq)
  qed
  then show ?thesis
    using plus_ab_defined valid_mask.simps by blast
qed

lemma core_defined:
  "get_h |φ| = get_h φ"
  "get_m |φ| = empty_mask"
  using Abs_state_inverse core_def pnone.rep_eq ppos.rep_eq valid_empty valid_stateI apply force
  by (metis Abs_state_inverse CollectI core_def empty_mask.simps fst_conv get_pre(2) less_irrefl pnone.rep_eq ppos.rep_eq valid_empty valid_stateI)

lemma state_ext:
  assumes "get_h a = get_h b"
      and "get_m a = get_m b"
    shows "a = b"
  by (metis Rep_state_inverse assms(1) assms(2) get_h_m)

lemma core_is_smaller:
  "Some x = x ⊕ |x|"
proof -
  obtain y where "Some y = x ⊕ |x|"
    by (metis Rep_state compatible_heapsI core_defined(1) core_defined(2) get_h_m mem_Collect_eq minus_empty option.collapse option.sel plus_ab_defined valid_state.simps)
  moreover have "y = x"
  proof (rule state_ext)
    have "get_h x = get_h x ++ get_h x"
      by (simp add: map_add_subsumed1)
    then show "get_h y = get_h x"
      using calculation core_defined(1) plus_charact(2) by presburger
    show "get_m y = get_m x"
      by (metis calculation core_defined(2) minus_empty plus_charact(1))
  qed
  ultimately show ?thesis by blast
qed

lemma core_is_pure:
  "Some |x| = |x| ⊕ |x|"
proof -
  obtain y where "Some y = |x| ⊕ |x|"
    by (metis core_def core_defined(1) core_is_smaller)
  moreover have "y = |x|"
    by (metis calculation core_def core_defined(1) core_is_smaller option.sel)
  ultimately show ?thesis by blast
qed

lemma core_sum:
  assumes "Some c = a ⊕ b"
  shows "Some |c| = |a| ⊕ |b|"
proof -
  obtain x where "Some x = |a| ⊕ |b|"
    by (metis assms core_defined(1) core_defined(2) minus_empty option.exhaust_sel plus_ab_defined valid_empty)
  moreover have "x = |c|"
    by (metis assms calculation core_defined(1) core_defined(2) minus_empty plus_charact(1) plus_charact(2) state_ext)
  ultimately show ?thesis by blast
qed

lemma core_max:
  assumes "Some x = x ⊕ c"
  shows "∃r. Some |x| = c ⊕ r"
proof -
  obtain y where "Some y = c ⊕ |x|"
    by (metis assms asso2 core_is_smaller plus_def)
  moreover have "|x| = y"
    by (metis (mono_tags, opaque_lifting) Rep_state_inverse add_masks_cancellative assms calculation commutative core_defined(1) core_sum get_h_m minus_empty option.inject plus_charact(1))
  ultimately show ?thesis by blast
qed

lemma positivity:
  assumes "a ⊕ b = Some c"
      and "Some c = c ⊕ c"
    shows "Some a = a ⊕ a"
proof -
  obtain x where "Some x = a ⊕ a"
    by (metis assms(1) assms(2) asso2 commutative option.exhaust_sel)
  moreover have "x = a"
    by (metis Rep_state_inverse add_masks_cancellative add_masks_comm assms(1) assms(2) calculation core_defined(1) core_defined(2) core_is_smaller get_h_m greater_mask_def greater_mask_properties(3) option.sel plus_charact(1))
  ultimately show ?thesis by blast
qed

lemma cancellative:
  assumes "Some a = b ⊕ x"
      and "Some a = b ⊕ y"
      and "|x| = |y|"
    shows "x = y"
  by (metis add_masks_cancellative assms(1) assms(2) assms(3) core_defined(1) plus_charact(1) state_ext)

lemma unit_charact:
  "get_h unit = empty_heap"
  "get_m unit = empty_mask"
proof -
  have "valid_state (empty_mask, empty_heap)"
    using valid_pre_unit by auto
  then show "get_h unit = empty_heap" using unit_def
    by (simp add: ‹unit = Abs_state (empty_mask, empty_heap)› Abs_state_inverse)
  show "get_m unit = empty_mask"
    using ‹valid_state (empty_mask, empty_heap)› unit_def Abs_state_inverse
    by fastforce
qed

lemma empty_heap_neutral:
  "a ++ empty_heap = a"
proof (rule ext)
  fix x show "(a ++ empty_heap) x = a x"
    by (simp add: domIff empty_heap_def map_add_dom_app_simps(3))
qed

lemma unit_neutral:
  "Some a = a ⊕ unit"
proof -
  obtain x where "Some x = a ⊕ unit"
    by (metis Abs_state_cases Rep_state_cases Rep_state_inverse compatible_heapsI empty_heap_def fst_conv get_h_m mem_Collect_eq minus_empty option.distinct(1) option.exhaust_sel plus_ab_defined snd_conv unit_def valid_pre_unit valid_state.simps)
  moreover have "x = a"
  proof (rule state_ext)
    show "get_h x = get_h a"
      using calculation empty_heap_neutral plus_charact(2) unit_charact(1) by auto
    show "get_m x = get_m a"
      by (metis calculation minus_empty plus_charact(1) unit_charact(2))
  qed
  ultimately show ?thesis by blast
qed

lemma stableI:
  assumes "⋀hl. ppos (get_m φ hl) ⟷ get_h φ hl ≠ None"
  shows "stable φ"
  using assms stable_def by blast

lemma stable_unit:
  "stable unit"
  by (metis empty_heap_def stable_def unit_charact(1) unit_charact(2) valid_heap_def valid_pre_unit valid_state.simps)

lemma stable_sum:
  assumes "stable a"
      and "stable b"
      and "Some x = a ⊕ b"
    shows "stable x"
proof (rule stableI)
  fix hl
  show "ppos (get_m x hl) = (get_h x hl ≠ None)" (is "?A ⟷ ?B")
  proof
    show "?A ⟹ ?B"
      by (metis add_le_same_cancel2 add_masks.simps assms(1) assms(2) assms(3) leI less_le_trans map_add_None padd.rep_eq plus_charact(1) plus_charact(2) ppos.rep_eq stable_def)
    show "?B ⟹ ?A"
      by (metis add_masks.simps assms(1) assms(2) assms(3) map_add_None padd_comm plus_charact(1) plus_charact(2) ppos_add stable_def)
  qed
qed

lemma multiply_valid:
  assumes "pgte pwrite p"
  shows "valid_state (multiply_mask p (get_m φ), get_h φ)"
proof (rule valid_stateI)
  show "valid_mask (multiply_mask p (get_m φ))"
    by (metis Rep_state assms(1) get_h_m mem_Collect_eq valid_mult valid_state.simps)
  fix hl show "ppos (multiply_mask p (get_m φ) hl) ⟹ get_h φ hl ≠ None"
    by (metis Abs_state_cases Rep_state_cases Rep_state_inverse get_h_m mem_Collect_eq multiply_mask_def pmult_comm pmult_special(2) ppos_eq_pnone valid_heap_def valid_state.simps)
qed

subsection ‹This state model corresponds to a separation algebra›

global_interpretation PartialSA: package_logic plus core unit stable
  defines greater (infixl "≽" 50) = "PartialSA.greater"
      and add_set (infixl "⊗" 60) = "PartialSA.add_set"
      and defined (infixl "|#|" 60) = "PartialSA.defined"
      and greater_set (infixl "|≫|" 50) = "PartialSA.greater_set"
      and minus (infixl "|⊖|" 60) = "PartialSA.minus"
  apply standard
  apply (simp add: commutative)
  using asso1 apply blast
  using asso2 apply blast
  using core_is_smaller apply blast
  using core_is_pure apply blast
  using core_max apply blast
  using core_sum apply blast
  using positivity apply blast
  using cancellative apply blast
  using unit_neutral apply blast
  using stable_sum apply blast
  using stable_unit by blast


lemma greaterI:
  assumes "larger_heap (get_h a) (get_h b)"
      and "greater_mask (get_m a) (get_m b)"
    shows "a ≽ b"
proof -
  let ?m = "λl. SOME p. get_m a l = padd (get_m b l) p"
  have "get_m a = add_masks (get_m b) ?m"
  proof (rule ext)
    fix l
    have "pgte (get_m a l) (get_m b l)"
      by (meson assms(2) greater_mask_equiv_def)
    then have "get_m a l = padd (get_m b l) (SOME p. get_m a l = padd (get_m b l) p)"
      by (simp add: p_greater_exists verit_sko_ex')
    then show "get_m a l = add_masks (get_m b) (λl. SOME p. get_m a l = padd (get_m b l) p) l"
      by simp
  qed
  moreover have "valid_state (?m, get_h a)"
  proof (rule valid_stateI)
    show "valid_mask (λl. SOME p. get_m a l = padd (get_m b l) p)"
      by (metis (no_types, lifting) Rep_state calculation get_h_m mem_Collect_eq upper_valid valid_state.simps)
    fix hl
    assume asm0: "ppos (SOME p. get_m a hl = padd (get_m b hl) p)"
    then have "ppos (get_m a hl)"
      by (metis (no_types, lifting) add_masks.elims add_masks_comm calculation greater_mask_def ppos_add)
    then show "get_h a hl ≠ None"
      by (metis Rep_state get_h.simps get_pre(2) mem_Collect_eq prod.collapse valid_heap_def valid_state.simps)
  qed
  moreover have "compatible_heaps (get_h b) (get_h a)"
    by (metis (mono_tags, lifting) assms(1) compatible_heapsI larger_heap_def option.inject)
  ultimately have "(get_m a, get_h a) = add_states (get_m b, get_h b) (?m, get_h a)"
  proof -
    have "get_h b ++ get_h a = get_h a"
    proof (rule ext)
      fix x show "(get_h b ++ get_h a) x = get_h a x"
        by (metis assms(1) domIff larger_heap_def map_add_dom_app_simps(1) map_add_dom_app_simps(3) not_Some_eq)
    qed
    then show ?thesis
      by (metis ‹get_m a = add_masks (get_m b) (λl. SOME p. get_m a l = padd (get_m b l) p)› add_states.simps)
  qed
  moreover have "compatible_heaps (get_h b) (get_h a) ∧ valid_mask (add_masks (get_m b) ?m)"
    by (metis Rep_state ‹compatible_heaps (get_h b) (get_h a)› ‹get_m a = add_masks (get_m b) (λl. SOME p. get_m a l = padd (get_m b l) p)› get_h_m mem_Collect_eq valid_state.simps)
  ultimately have "Some a = b ⊕ Abs_state (?m, get_h a)"
  proof -
    have "Rep_state (Abs_state (?m, get_h a)) = (?m, get_h a)"
      using Abs_state_inverse ‹valid_state (λl. SOME p. get_m a l = padd (get_m b l) p, get_h a)› by blast
    moreover have "compatible (Rep_state b) (?m, get_h a)"
      using ‹compatible_heaps (get_h b) (get_h a) ∧ valid_mask (add_masks (get_m b) (λl. SOME p. get_m a l = padd (get_m b l) p))› compatible_def by auto
    moreover have "valid_state (add_states (Rep_state b) (?m, get_h a))"
      by (metis Rep_state ‹(get_m a, get_h a) = add_states (get_m b, get_h b) (λl. SOME p. get_m a l = padd (get_m b l) p, get_h a)› get_h_m mem_Collect_eq)
    ultimately show ?thesis
      by (metis (no_types, lifting) Rep_state_inverse ‹(get_m a, get_h a) = add_states (get_m b, get_h b) (λl. SOME p. get_m a l = padd (get_m b l) p, get_h a)› get_h_m plus_def)
  qed
  then show ?thesis
    by (meson PartialSA.greater_def)
qed

lemma larger_implies_greater_mask_hl:
  assumes "a ≽ b"
  shows "pgte (get_m a hl) (get_m b hl)"
  using PartialSA.greater_def assms p_greater_exists plus_charact(1) by auto

lemma larger_implies_larger_heap:
  assumes "a ≽ b"
  shows "larger_heap (get_h a) (get_h b)"
  by (metis (full_types) PartialSA.greater_equiv assms larger_heapI map_add_find_right plus_charact(2))

lemma compatibleI:
  assumes "compatible_heaps (get_h a) (get_h b)"
      and "valid_mask (add_masks (get_m a) (get_m b))"
    shows "a |#| b"
  using PartialSA.defined_def assms(1) assms(2) plus_ab_defined by presburger

end

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 "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 ‹a ∈ A ∧ Some x = R a w ⊕ a› option.distinct(1) scalable_def w_in_scaled)
    next
      case False
      then have "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 ‹a ∈ A ∧ Some x = R a w ⊕ a› 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 ‹