# 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)"

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"

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
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:
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 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"
then show ?thesis
by (metis assms order_refl p_greater_exists padd_asso pgte.rep_eq)
qed

assumes "a = padd x b"
and "a = padd y b"
shows "x = y"

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

"pnone = padd a b â· a = pnone â§ b = pnone"

assumes "ppos a"
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)"

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)

"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"
proof -
let ?a = "Rep_prat a"
let ?b = "Rep_prat b"
have "(?a / (?a + ?b)) + (?b / (?a + ?b)) = 1"
then show ?thesis
by (metis Rep_prat_inject padd.rep_eq pdiv.rep_eq pwrite.rep_eq)
qed

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


subsection â¹Permission masks: Maps from heap locations to permission amountsâº

imports PosRat
begin

subsubsection â¹Definitionsâº

type_synonym field = string
type_synonym heap_loc = "address Ã field"

type_synonym mask = "heap_loc â prat"
type_synonym bmask = "heap_loc â bool"

definition null where "null = 0"

"full_mask hl = (if fst hl = null then pnone else pwrite)"

"multiply_mask p Ï hl = pmult p (Ï hl)"

inductive rm_acc where
"Ï hl = padd p r â¹ rm_acc Ï hl p (Ï(hl := r))"

"valid_mask Ï â· (âhl. pgte pwrite (Ï hl)) â§ (âf. Ï (null, f) = pnone)"

definition valid_null :: "mask â bool" where
"valid_null Ï â· (âf. Ï (null, f) = pnone)"

"equal_on_mask Ï h h' â· (âhl. ppos (Ï hl) â¶ h hl = h' hl)"

"equal_on_bmask Ï h h' â· (âhl. Ï hl â¶ h hl = h' hl)"

"big_greater_mask Î  Î ' â· (âh. greater_mask (Î  h) (Î ' h))"

"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 Ï)"

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

proof (rule ext)
qed

proof (rule ext)
qed

lemma minus_empty:
proof (rule ext)
qed

proof (rule ext)
qed

assumes "âhl. pgte pwrite (Ï hl)"
and "âf. Ï (null, f) = pnone"

"greater_mask Ï' Ï â· (âhl. pgte (Ï' hl) (Ï hl))"
(is "?A â· ?B")
proof (rule iffI)
show "?A â¹ ?B"
proof (clarify)
fix hl assume "greater_mask Ï' Ï"
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)"
proof (rule ext)
fix hl
have "Ï' hl = padd (Ï hl) (?r hl)"
by (meson â¹âhl. pgte (Ï' hl) (Ï hl)âº p_greater_exists someI_ex)
by auto
qed
then show ?A
qed
qed

assumes "âhl. pgte (Ï' hl) (Ï hl)"

proof (rule ext)
show "Ï x = Ï' x"
qed

lemma valid_empty:

lemma upper_valid_aux:
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"
qed

lemma upper_valid:

assumes "âhl. Ï hl â¹ h hl = h' hl"

lemma big_greater_iff:
proof -
let ?C = "Î»h. SOME r. A h = add_masks (B h) r"
proof (rule ext)
fix x
proof (rule ext)
fix xa
by auto
qed
qed
by fast
qed

proof (rule ext)
qed

proof (rule ext)
qed

proof -
have "âa b. equal_on_mask Ï a b â¹ equal_on_mask Ï b a"
then show ?thesis by blast
qed

assumes "pgte (Ï hl) r"

lemma update_dm_same:
"update_dm dm Ï Ï = dm"
proof (rule ext)
fix x show "update_dm dm Ï Ï x = dm x"
qed

lemma update_trans:
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)"
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

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)"
moreover have "âhl. update_dm dm Ï Ï' hl â· dm hl â¨ pgt (Ï hl) (Ï' hl)"
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'"
then have "âhl. update_dm dm Ï Ï' hl â¹ h' hl = h hl"
then show "âhl. update_dm dm Ï Ï' hl â¶ h' hl = h hl"
by simp
qed
then show ?thesis
qed

proof (rule ccontr)
then obtain hl where "Â¬ pgte (d hl) (b hl)"
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))"
then show "False"
qed

shows "c = d"
proof (rule ext)
fix x show "c x = d x"
qed

assumes "âhl. ppos (Ï hl) â¹ h hl = h' hl"

fix hl assume asm: "ppos (Ï hl)"
then show "h hl = h' hl"
qed

proof
then show "h hl = h' hl"
proof (cases "ppos (Ï1 hl)")
case True
then show ?thesis
next
case False
then show ?thesis
qed
qed
qed

lemma mult_greater:

proof (rule ext)
fix x show "multiply_mask pwrite Ï x = Ï x"
qed

proof (rule ext)
qed

proof (rule ext)
qed

lemma upper_boundedI:
assumes "âhl. pgte p (Ï hl)"
shows "upper_bounded Ï p"

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:
and "pgte pwrite p"
have "upper_bounded Ï pwrite"
using assms(1) upper_bounded_def by auto
then have "upper_bounded (multiply_mask p Ï) (pmult p pwrite)"
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"
qed

lemma valid_sum:
and "upper_bounded a ma"
and "upper_bounded b mb"
and "pgte pwrite (padd ma mb)"
proof -
fix hl
by (meson assms(5) dual_order.trans pgte.rep_eq)
qed
qed

lemma valid_multiply:
and "upper_bounded a ma"
and "pgte pwrite (pmult ma p)"
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:

end

ody>

# Theory PartialHeapSA

subsection â¹Partial heaps: Partial maps from heap location to valuesâº

theory PartialHeapSA
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:
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:
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

fun add_states :: "pre_state â pre_state â pre_state" where

definition larger_heap where
"larger_heap h' h â· (âhl x. h hl = Some x â¶ h' hl = Some x)"

definition unit :: "state" where

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:
shows "valid_state (a, h)"
proof (rule valid_stateI)
using assms upper_valid_aux valid_state.simps by blast
fix hl assume "ppos (a hl)" then show "h hl â  None"
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"
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"

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
next
case (Some a)
then show ?thesis
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)"

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"
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)
using calculation(2) compatible_def by fastforce
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)"
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
qed
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"
case True
then have "(get_h a) ++ (get_h b) = (get_h b) ++ (get_h a)"
then show ?thesis
next
case False
then show ?thesis
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
by (metis None assms plus_ab_defined plus_charact(1))
then show ?thesis
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)
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
qed

lemma asso2:
assumes "a â b = Some ab â§ b â c = None"
shows " ab â c = None"
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"
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))"
proof -
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
qed

lemma core_defined:
"get_h |Ï| = get_h Ï"
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"
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"
ultimately show ?thesis by blast
qed

lemma cancellative:
assumes "Some a = b â x"
and "Some a = b â y"
and "|x| = |y|"
shows "x = y"

lemma unit_charact:
"get_h unit = empty_heap"
proof -
using valid_pre_unit by auto
then show "get_h unit = empty_heap" using unit_def
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"
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"
show "?B â¹ ?A"
qed
qed

lemma multiply_valid:
assumes "pgte pwrite p"
shows "valid_state (multiply_mask p (get_m Ï), get_h Ï)"
proof (rule valid_stateI)
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 defined (infixl "|#|" 60) = "PartialSA.defined"
and greater_set (infixl "|â«|" 50) = "PartialSA.greater_set"
and minus (infixl "|â|" 60) = "PartialSA.minus"
apply standard
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"
proof (rule ext)
fix l
have "pgte (get_m a l) (get_m b l)"
then have "get_m a l = padd (get_m b l) (SOME p. get_m a l = padd (get_m b l) p)"
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)"
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"
qed
then show ?thesis
qed
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

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)"
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 }"

"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)"

"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}"
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"
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

shows "w = comp_min_mask a w"
proof (rule ext)
fix x
have "pgte pwrite (padd (a x) (w x))"
moreover have "padd (a x) (comp_one (a x)) = pwrite"
then have "pgte (comp_one (a x)) (w x)"
then show "w x = comp_min_mask a w x"
qed

lemma R_smaller:
"w â½ R a w"
proof (cases "scalable w a")
case True
then show ?thesis
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)
fix hl show "pgte (get_m w hl) (comp_min_mask (get_m a) (get_m w) hl)"
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"
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 "âf. comp_min_mask (get_m a) (get_m w) (null, f) = pnone"
fix hl show "pgte pwrite (comp_min_mask (get_m a) (get_m w) hl)"
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 "â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

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))"
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

proof -
fix f
have "comp_min_mask b a (null, f) = pnone"
qed
proof (cases "pgte (a hl) (comp_one (b hl))")
case True
then show ?thesis
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)
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"
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"
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
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 Rep_state_cases Rep_state_inverse â¹`