diff --git a/thys/Combinable_Wands/CombinableWands.thy b/thys/Combinable_Wands/CombinableWands.thy
--- a/thys/Combinable_Wands/CombinableWands.thy
+++ b/thys/Combinable_Wands/CombinableWands.thy
@@ -1,884 +1,885 @@
 section \<open>Combinable Magic Wands\<close>
 
 text \<open>Note that, in this theory, assertions are represented as semantic assertions, i.e., as the set of states in which they hold.\<close>
 
 theory CombinableWands
   imports PartialHeapSA
 begin             
 
 subsection \<open>Definitions\<close>
 
 type_synonym sem_assertion = "state set"
 
 fun multiply :: "prat \<Rightarrow> state \<Rightarrow> state" where
   "multiply p \<phi> = Abs_state (multiply_mask p (get_m \<phi>), get_h \<phi>)"
 
 text \<open>Because we work in an intuitionistic setting, a fraction of an assertion is defined using the upper-closure operator.\<close>
 
 fun multiply_sem_assertion :: "prat \<Rightarrow> sem_assertion \<Rightarrow> sem_assertion" where
   "multiply_sem_assertion p P = PartialSA.upper_closure (multiply p ` P)"
 
 definition combinable :: "sem_assertion \<Rightarrow> bool" where
   "combinable P \<longleftrightarrow> (\<forall>\<alpha> \<beta>. ppos \<alpha> \<and> ppos \<beta> \<and> pgte pwrite (padd \<alpha> \<beta>) \<longrightarrow> (multiply_sem_assertion \<alpha> P) \<otimes> (multiply_sem_assertion \<beta> P) \<subseteq> multiply_sem_assertion (padd \<alpha> \<beta>) P)"
 
 definition scaled where
   "scaled \<phi> = { multiply p \<phi> |p. ppos p \<and> pgte pwrite p }"
 
 definition comp_min_mask :: "mask \<Rightarrow> (mask \<Rightarrow> mask)" where
   "comp_min_mask b a hl = pmin (a hl) (comp_one (b hl))"
 
 definition scalable where
   "scalable w a \<longleftrightarrow> (\<forall>\<phi> \<in> scaled w. \<not> a |#| \<phi>)"
 
 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. \<forall>a x. a \<in> A \<and> Some x = R a w \<oplus> a \<longrightarrow> x \<in> B }"
 
 definition wand :: "sem_assertion \<Rightarrow> sem_assertion \<Rightarrow> sem_assertion" where
   "wand A B = { w |w. \<forall>a x. a \<in> A \<and> Some x = w \<oplus> a \<longrightarrow> x \<in> B }"
 
 definition intuitionistic where
   "intuitionistic A \<longleftrightarrow> (\<forall>a b. a \<succeq> b \<and> b \<in> A \<longrightarrow> a \<in> A)"
 
 definition binary_mask :: "mask \<Rightarrow> mask" where
   "binary_mask \<pi> l = (if \<pi> l = pwrite then pwrite else pnone)"
 
 definition binary :: "sem_assertion \<Rightarrow> bool" where
   "binary A \<longleftrightarrow> (\<forall>\<phi> \<in> A. Abs_state (binary_mask (get_m \<phi>), get_h \<phi>) \<in> A)"
 
 
 
 
 subsection Lemmas
 
 
 lemma wand_equiv_def:
   "wand A B = { \<phi> |\<phi>. A \<otimes> {\<phi>} \<subseteq> B }"
 proof
   show "wand A B \<subseteq> {\<phi> |\<phi>. A \<otimes> {\<phi>} \<subseteq> B}"
   proof
     fix w assume "w \<in> wand A B"
     have "A \<otimes> {w} \<subseteq> B"
     proof
       fix x assume "x \<in> A \<otimes> {w}"
       then show "x \<in> B"
         using PartialSA.add_set_elem \<open>w \<in> wand A B\<close> commutative wand_def by auto
     qed
     then show "w \<in> {\<phi> |\<phi>. A \<otimes> {\<phi>} \<subseteq> B}"
       by simp
   qed
   show "{\<phi> |\<phi>. A \<otimes> {\<phi>} \<subseteq> B} \<subseteq> wand A B"
   proof
     fix w assume "w \<in> {\<phi> |\<phi>. A \<otimes> {\<phi>} \<subseteq> B}"
     have "\<And>a x. a \<in> A \<and> Some x = w \<oplus> a \<Longrightarrow> x \<in> B"
     proof -
       fix a x assume "a \<in> A \<and> Some x = w \<oplus> a"
       then have "x \<in> A \<otimes> {w}"
         using PartialSA.add_set_elem PartialSA.commutative by auto
       then show "x \<in> B"
         using \<open>w \<in> {\<phi> |\<phi>. A \<otimes> {\<phi>} \<subseteq> B}\<close> by blast
     qed
     then show "w \<in> wand A B"
       using wand_def by force
   qed
 qed
 
 lemma w_in_scaled:
   "w \<in> 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 "\<not> scalable w a"
   shows "\<exists>p. ppos p \<and> pgte pwrite p \<and> 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 \<succeq> 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 "\<not> 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 "\<And>a x. a \<in> A \<and> Some x = R a w \<oplus> a \<Longrightarrow> x \<in> B"
   shows "w \<in> cwand A B"
   using assms cwand_def by force
 
 lemma wandI:
   assumes "\<And>a x. a \<in> A \<and> Some x = a \<oplus> w \<Longrightarrow> x \<in> B"
   shows "w \<in> wand A B"
 proof -
   have "A \<otimes> {w} \<subseteq> B"
   proof (rule subsetI)
     fix x assume "x \<in> A \<otimes> {w}"
     then obtain a where "Some x = a \<oplus> w" "a \<in> A"
       using PartialSA.add_set_elem by auto
     then show "x \<in> B"
       using assms by blast
   qed
   then show ?thesis
     using wand_equiv_def by force
 qed
 
 lemma non_scalable_R_charact:
   assumes "\<not> scalable w a"
   shows "get_m (R a w) = comp_min_mask (get_m a) (get_m w) \<and> 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 "\<And>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 \<noteq> None"
       by (metis Rep_state \<open>ppos (comp_min_mask (get_m a) (get_m w) hl)\<close> 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 "\<And>hl. ppos (binary_mask (get_m a) hl) \<Longrightarrow> get_h a hl \<noteq> 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 \<in> multiply_sem_assertion p A"
   shows "\<exists>a \<in> A. x \<succeq> 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 \<in> A"
   shows "multiply p x \<in> 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 \<succeq> b"
     shows "multiply p a \<succeq> 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 \<and> 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 "\<And>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 \<open>The combinable wand is stronger than the original wand\<close>
 
 lemma cwand_stronger:
   "cwand A B \<subseteq> wand A B"
 proof
   fix w assume asm0: "w \<in> cwand A B"
   then have r: "\<And>a x. a \<in> A \<and> Some x = R a w \<oplus> a \<Longrightarrow> x \<in> B"
     using cwand_def by blast
   show "w \<in> wand A B"
   proof (rule wandI)
     fix a x assume asm1: "a \<in> A \<and> Some x = a \<oplus> w"
     then have "R a w = w"
       by (metis PartialSA.defined_def R_compatible_same option.distinct(1))
     then show "x \<in> B"
       by (metis PartialSA.commutative asm1 r)
   qed
 qed
 
 
 subsection \<open>The combinable wand is the same as the original wand when the left-hand side is binary\<close>
 
 lemma binary_same:
   assumes "binary A"
       and "intuitionistic B"
   shows "wand A B \<subseteq> cwand A B"
 proof (rule subsetI)
   fix w assume "w \<in> wand A B"
   then have asm0: "A \<otimes> {w} \<subseteq> B"
     by (simp add: wand_equiv_def)
   show "w \<in> cwand A B"
   proof (rule in_cwand)
-    fix a x assume "a \<in> A \<and> Some x = R a w \<oplus> a"
+    fix a x assume asm1: "a \<in> A \<and> Some x = R a w \<oplus> a"
     show "x \<in> B"
     proof (cases "scalable w a")
       case True
       then show ?thesis
-        by (metis PartialSA.commutative PartialSA.defined_def R_def \<open>a \<in> A \<and> Some x = R a w \<oplus> a\<close> option.distinct(1) scalable_def w_in_scaled)
+        by (metis PartialSA.commutative PartialSA.defined_def R_def asm1 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) \<and> get_h (R a w) = get_h w"
+      then have r0: "get_m (R a w) = comp_min_mask (get_m a) (get_m w) \<and> 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) \<in> A"
-        using \<open>a \<in> A \<and> Some x = R a w \<oplus> a\<close> assms(1) binary_def by blast
+        using asm1 assms(1) binary_def by blast
       moreover have "greater_mask (add_masks (comp_min_mask (get_m a) (get_m w)) (get_m a))
   (add_masks (binary_mask (get_m a)) (get_m w))"
       proof (rule greater_maskI)
         fix hl show "pgte (add_masks (comp_min_mask (get_m a) (get_m w)) (get_m a) hl) (add_masks (binary_mask (get_m a)) (get_m w) hl)"
         proof (cases "get_m a hl = pwrite")
           case True
           obtain \<phi> where "\<phi> \<in> scaled w" "a |#| \<phi>" 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 \<noteq> 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 \<phi>) = multiply_mask p (get_m \<phi>)"
               using multiply_valid[of p \<phi>] multiply.simps[of p \<phi>]
               by (metis Rep_state_cases Rep_state_inverse \<open>pgte pwrite p\<close> fst_conv get_pre(2) mem_Collect_eq)
             then have "ppos (get_m (multiply p w) hl)" using pmult_ppos
               by (metis Rep_state_cases Rep_state_inverse \<open>pgte pwrite p\<close> \<open>ppos p\<close> calculation fst_conv get_pre(2) mem_Collect_eq multiply.simps multiply_mask_def multiply_valid)
             then have "pgt (padd (get_m (multiply p w) hl) (get_m a hl)) pwrite"
               by (metis True add_le_same_cancel2 leD not_pgte_charact padd.rep_eq pgte.rep_eq ppos.rep_eq)
             then have "\<not> valid_mask (add_masks (get_m (multiply p w)) (get_m a))"
               by (metis add_masks.elims not_pgte_charact valid_mask.elims(1))
             then show False
               using PartialSA.defined_def \<open>multiply p w |#| a\<close> plus_ab_defined by blast
           qed
           then show ?thesis
             by (metis Rep_prat_inverse add.right_neutral add_masks.simps binary_mask_def p_greater_exists padd.rep_eq padd_comm pnone.rep_eq)
         next
           case False
           then have "add_masks (binary_mask (get_m a)) (get_m w) hl = get_m w hl"
             by (metis Rep_prat_inject add.right_neutral add_masks.simps binary_mask_def padd.rep_eq padd_comm pnone.rep_eq)
           then show ?thesis
           proof (cases "pgte (get_m w hl) (comp_one (get_m a hl))")
             case True
             then have "comp_min_mask (get_m a) (get_m w) hl = comp_one (get_m a hl)"
               using comp_min_mask_def pmin_is by presburger
             then have "add_masks (comp_min_mask (get_m a) (get_m w)) (get_m a) hl = pwrite"
               by (metis PartialSA.unit_neutral add_masks.simps add_masks_comm minus_empty option.distinct(1) padd_comp_one plus_ab_defined unit_charact(2) valid_mask.simps)
             then show ?thesis
               by (metis PartialSA.unit_neutral \<open>add_masks (binary_mask (get_m a)) (get_m w) hl = get_m w hl\<close> minus_empty option.distinct(1) plus_ab_defined unit_charact(2) valid_mask.simps)
           next
             case False
             then have "comp_min_mask (get_m a) (get_m w) hl = get_m w hl"
               by (metis comp_min_mask_def not_pgte_charact pgt_implies_pgte pmin_comm pmin_is)
             then show ?thesis
               using \<open>add_masks (binary_mask (get_m a)) (get_m w) hl = get_m w hl\<close> p_greater_exists by auto
           qed
         qed
       qed
       then have "valid_mask (add_masks (binary_mask (get_m a)) (get_m w))"
-        by (metis \<open>a \<in> A \<and> Some x = R a w \<oplus> a\<close> calculation(1) greater_mask_def option.distinct(1) plus_ab_defined upper_valid_aux)
+        by (metis asm1 calculation(1) greater_mask_def option.distinct(1) plus_ab_defined upper_valid_aux)
       moreover have "compatible_heaps (get_h a) (get_h w)"
-        by (metis PartialSA.commutative \<open>a \<in> A \<and> Some x = R a w \<oplus> a\<close> \<open>get_m (R a w) = comp_min_mask (get_m a) (get_m w) \<and> get_h (R a w) = get_h w\<close> option.simps(3) plus_ab_defined)
+        by (metis PartialSA.commutative asm1 r0 option.simps(3) plus_ab_defined)
       then obtain xx where "Some xx = Abs_state (binary_mask (get_m a), get_h a) \<oplus> w"
         using Abs_state_inverse calculation compatible_def fst_conv plus_def valid_bin by auto
       then have "xx \<in> B" using asm0
         by (meson PartialSA.add_set_elem \<open>Abs_state (binary_mask (get_m a), get_h a) \<in> A\<close> singletonI subset_iff)
       moreover have "x \<succeq> xx"
       proof (rule greaterI)
         show "greater_mask (get_m x) (get_m xx)"
-          using Abs_state_inverse \<open>Some xx = Abs_state (binary_mask (get_m a), get_h a) \<oplus> w\<close> \<open>a \<in> A \<and> Some x = R a w \<oplus> a\<close> \<open>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))\<close> calculation(1) plus_charact(1) valid_bin by auto
+          using Abs_state_inverse \<open>Some xx = Abs_state (binary_mask (get_m a), get_h a) \<oplus> w\<close> asm1 \<open>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))\<close> calculation(1) plus_charact(1) valid_bin by auto
         show "larger_heap (get_h x) (get_h xx)"
         proof (rule larger_heapI)
           fix hl xa assume "get_h xx hl = Some xa"
           then show "get_h x hl = Some xa"
-            by (metis PartialSA.commutative Rep_state_cases Rep_state_inverse \<open>Some xx = Abs_state (binary_mask (get_m a), get_h a) \<oplus> w\<close> \<open>a \<in> A \<and> Some x = R a w \<oplus> a\<close> calculation(1) get_h.simps mem_Collect_eq plus_charact(2) snd_conv valid_bin)
+            by (metis PartialSA.commutative Rep_state_cases Rep_state_inverse \<open>Some xx = Abs_state (binary_mask (get_m a), get_h a) \<oplus> w\<close> asm1 calculation(1) get_h.simps mem_Collect_eq plus_charact(2) snd_conv valid_bin)
         qed
       qed
       ultimately show ?thesis
         using assms(2) intuitionistic_def by blast
     qed
   qed
 qed
 
 
 subsection \<open>The combinable wand is combinable\<close>
 
 lemma combinableI:
   assumes "\<And>a b. ppos a \<and> ppos b \<and> padd a b = pwrite \<Longrightarrow> (multiply_sem_assertion a (cwand A B)) \<otimes> (multiply_sem_assertion b (cwand A B)) \<subseteq> cwand A B"
   shows "combinable (cwand A B)"
 proof -
   have "\<And>a b. ppos a \<and> ppos b \<and> pgte pwrite (padd a b) \<Longrightarrow> (multiply_sem_assertion a (cwand A B)) \<otimes> (multiply_sem_assertion b (cwand A B)) \<subseteq> multiply_sem_assertion (padd a b) (cwand A B)"
   proof -    
     fix a b assume asm0: "ppos a \<and> ppos b \<and> pgte pwrite (padd a b)"
     then have "pgte pwrite a \<and> pgte pwrite b"
       using padd.rep_eq pgte.rep_eq ppos.rep_eq by auto
     show "(multiply_sem_assertion a (cwand A B)) \<otimes> (multiply_sem_assertion b (cwand A B)) \<subseteq> multiply_sem_assertion (padd a b) (cwand A B)"
     proof
       fix x assume "x \<in> multiply_sem_assertion a (cwand A B) \<otimes> multiply_sem_assertion b (cwand A B)"
       then obtain xa xb where "Some x = xa \<oplus> xb" "xa \<in> multiply_sem_assertion a (cwand A B)" "xb \<in> multiply_sem_assertion b (cwand A B)"
         by (meson PartialSA.add_set_elem)
       then obtain wa wb where "wa \<in> cwand A B" "wb \<in> cwand A B" "xa \<succeq> multiply a wa" "xb \<succeq> multiply b wb"
         by (meson in_multiply_sem)
       let ?a = "pdiv a (padd a b)"
       let ?b = "pdiv b (padd a b)"
-      have "pgte pwrite ?a \<and> pgte pwrite ?b"
+      have r0: "pgte pwrite ?a \<and> pgte pwrite ?b"
         using asm0 p_greater_exists padd_comm pdiv_smaller ppos_add by blast
       have "multiply ?a wa |#| multiply ?b wb"
       proof (rule compatibleI)
         show "compatible_heaps (get_h (multiply (pdiv a (padd a b)) wa)) (get_h (multiply (pdiv b (padd a b)) wb))"
         proof -
           have "compatible_heaps (get_h (multiply a wa)) (get_h (multiply b wb))"
             by (metis PartialSA.asso2 PartialSA.asso3 PartialSA.greater_equiv PartialSA.minus_some \<open>Some x = xa \<oplus> xb\<close> \<open>xa \<succeq> multiply a wa\<close> \<open>xb \<succeq> multiply b wb\<close> option.simps(3) plus_ab_defined)
           moreover have "get_h (multiply (pdiv a (padd a b)) wa) = get_h (multiply a wa) \<and> get_h (multiply (pdiv b (padd a b)) wb) = get_h (multiply b wb)"
           proof -
             have "pgte pwrite a \<and> pgte pwrite b"
               by (metis asm0 p_greater_exists padd_asso padd_comm)
             moreover have "pgte pwrite ?a \<and> pgte pwrite ?b"
               using asm0 p_greater_exists padd_comm pdiv_smaller ppos_add by blast
             ultimately show ?thesis
               using get_h_multiply by presburger
           qed
           then show ?thesis
             using calculation by presburger
         qed
         show "valid_mask (add_masks (get_m (multiply (pdiv a (padd a b)) wa)) (get_m (multiply (pdiv b (padd a b)) wb)))"
         proof (rule valid_maskI)
           show "\<And>f. add_masks (get_m (multiply (pdiv a (padd a b)) wa)) (get_m (multiply (pdiv b (padd a b)) wb)) (null, f) = pnone"
             by (metis PartialSA.unit_neutral add_masks_equiv_valid_null option.distinct(1) plus_ab_defined valid_mask.simps valid_null_def)
           fix hl have "add_masks (get_m (multiply (pdiv a (padd a b)) wa)) (get_m (multiply (pdiv b (padd a b)) wb)) hl
                       = padd (pmult ?a (get_m wa hl)) (pmult ?b (get_m wb hl))"
           proof -
             have "get_m (multiply ?a wa) hl = pmult ?a (get_m wa hl)"
-              using Abs_state_inverse \<open>pgte pwrite (pdiv a (padd a b)) \<and> pgte pwrite (pdiv b (padd a b))\<close> multiply_mask_def multiply_valid by auto
+              using Abs_state_inverse r0 multiply_mask_def multiply_valid by auto
             moreover have "get_m (multiply ?b wb) hl = pmult ?b (get_m wb hl)"
-              using Abs_state_inverse \<open>pgte pwrite (pdiv a (padd a b)) \<and> pgte pwrite (pdiv b (padd a b))\<close> multiply_mask_def multiply_valid by auto
+              using Abs_state_inverse r0 multiply_mask_def multiply_valid by auto
             ultimately show ?thesis by simp
           qed
           moreover have "pgte pwrite (padd (pmult ?a (get_m wa hl)) (pmult ?b (get_m wb hl)))"
           proof (rule padd_one_ineq_sum)
             show "pgte pwrite (get_m wa hl)"
               by (metis PartialSA.unit_neutral option.discI plus_ab_defined upper_valid_aux valid_mask.simps)
             show "pgte pwrite (get_m wb hl)"
               by (metis PartialSA.unit_neutral option.discI plus_ab_defined upper_valid_aux valid_mask.simps)
             show "padd (pdiv a (padd a b)) (pdiv b (padd a b)) = pwrite"
               using asm0 sum_coeff by blast
           qed
           ultimately show "pgte pwrite (add_masks (get_m (multiply (pdiv a (padd a b)) wa)) (get_m (multiply (pdiv b (padd a b)) wb)) hl)"
             by presburger
         qed
       qed
-      then obtain xx where "Some xx = multiply ?a wa \<oplus> multiply ?b wb"        
+      then obtain xx where xx_def: "Some xx = multiply ?a wa \<oplus> multiply ?b wb"        
         using PartialSA.defined_def by auto
-      moreover have "(multiply_sem_assertion ?a (cwand A B)) \<otimes> (multiply_sem_assertion ?b (cwand A B)) \<subseteq> cwand A B"
+      moreover have inclusion: "(multiply_sem_assertion ?a (cwand A B)) \<otimes> (multiply_sem_assertion ?b (cwand A B)) \<subseteq> cwand A B"
       proof (rule assms)
         show "ppos (pdiv a (padd a b)) \<and> ppos (pdiv b (padd a b)) \<and> padd (pdiv a (padd a b)) (pdiv b (padd a b)) = pwrite"
           using asm0 padd.rep_eq pdiv.rep_eq ppos.rep_eq sum_coeff by auto
       qed
       ultimately have "xx \<in> cwand A B"
       proof -
         have "multiply ?a wa \<in> multiply_sem_assertion ?a (cwand A B)"
           using \<open>wa \<in> cwand A B\<close> in_multiply_refl by presburger
         moreover have "multiply ?b wb \<in> multiply_sem_assertion ?b (cwand A B)"
           by (meson \<open>wb \<in> cwand A B\<close> in_multiply_refl)
         ultimately show ?thesis
-          using PartialSA.add_set_def \<open>Some xx = multiply (pdiv a (padd a b)) wa \<oplus> multiply (pdiv b (padd a b)) wb\<close> \<open>multiply_sem_assertion (pdiv a (padd a b)) (cwand A B) \<otimes> multiply_sem_assertion (pdiv b (padd a b)) (cwand A B) \<subseteq> cwand A B\<close> by fastforce
+          using PartialSA.add_set_def xx_def inclusion by fastforce
       qed
       moreover have "x \<succeq> multiply (padd a b) xx"
       proof (rule greaterI)
         have "valid_state (multiply_mask (padd a b) (get_m xx), get_h xx)"
           using asm0 multiply_valid by blast
         show "larger_heap (get_h x) (get_h (multiply (padd a b) xx))"
         proof -
           have "get_h (multiply (padd a b) xx) = get_h xx"
             using asm0 get_h_multiply by blast
           moreover have "get_h xx = get_h wa ++ get_h wb"
-            by (metis \<open>Some xx = multiply (pdiv a (padd a b)) wa \<oplus> multiply (pdiv b (padd a b)) wb\<close> asm0 get_h_multiply p_greater_exists padd_comm plus_charact(2) sum_coeff)
+            by (metis xx_def asm0 get_h_multiply p_greater_exists padd_comm plus_charact(2) sum_coeff)
           moreover have "get_h x = get_h xa ++ get_h xb"
             using \<open>Some x = xa \<oplus> xb\<close> plus_charact(2) by presburger
           moreover have "get_h wa = get_h (multiply a wa) \<and> get_h wb = get_h (multiply b wb)"
             by (metis asm0 get_h_multiply order_trans p_greater_exists padd_comm pgte.rep_eq)
           moreover have "larger_heap (get_h xa) (get_h wa) \<and> larger_heap (get_h xb) (get_h wb)"
             using \<open>xa \<succeq> multiply a wa\<close> \<open>xb \<succeq> multiply b wb\<close> calculation(4) larger_implies_larger_heap by presburger
           ultimately show ?thesis
             by (metis \<open>Some x = xa \<oplus> xb\<close> larger_heaps_sum_ineq option.simps(3) plus_ab_defined)
         qed
         show "greater_mask (get_m x) (get_m (multiply (padd a b) xx))"
         proof (rule greater_maskI)
           fix hl
           have "pgte (get_m x hl) (padd (get_m xa hl) (get_m xb hl))"
             using \<open>Some x = xa \<oplus> xb\<close> pgte.rep_eq plus_charact(1) by auto
           moreover have "pgte (get_m xa hl) (get_m (multiply a wa) hl) \<and> pgte (get_m xb hl) (get_m (multiply b wb) hl)"
             using \<open>xa \<succeq> multiply a wa\<close> \<open>xb \<succeq> multiply b wb\<close> larger_implies_greater_mask_hl by blast
           moreover have "get_m (multiply (padd a b) xx) hl = pmult (padd a b) (get_m xx hl)"
             by (metis Rep_state_cases Rep_state_inverse \<open>valid_state (multiply_mask (padd a b) (get_m xx), get_h xx)\<close> fst_conv get_pre(2) mem_Collect_eq multiply.simps multiply_mask_def)
           moreover have "... = padd (pmult (pmult (padd a b) ?a) (get_m wa hl)) (pmult (pmult (padd a b) ?b) (get_m wb hl))"
           proof -
             have "get_m (multiply ?a wa) hl = pmult ?a (get_m wa hl)"
               by (metis Abs_state_inverse asm0 fst_conv get_pre(2) mem_Collect_eq multiply.simps multiply_mask_def multiply_valid p_greater_exists sum_coeff)
             moreover have "get_m (multiply ?b wb) hl = pmult ?b (get_m wb hl)"
               by (metis Abs_state_inverse asm0 fst_conv get_pre(2) mem_Collect_eq multiply.simps multiply_mask_def multiply_valid p_greater_exists padd_comm pdiv_smaller ppos_add)
             ultimately have "get_m xx hl = padd (pmult ?a (get_m wa hl)) (pmult ?b (get_m wb hl))"
-              using \<open>Some xx = multiply (pdiv a (padd a b)) wa \<oplus> multiply (pdiv b (padd a b)) wb\<close> plus_charact(1) by fastforce
+              using xx_def plus_charact(1) by fastforce
             then show ?thesis
               by (simp add: pmult_padd)
           qed
           moreover have "... = padd (pmult a (get_m wa hl)) (pmult b (get_m wb hl))"
             using asm0 pmult_pdiv_cancel ppos_add by presburger
           moreover have "get_m (multiply a wa) hl = pmult a (get_m wa hl) \<and> get_m (multiply b wb) hl = pmult b (get_m wb hl)"
           proof -
             have "valid_mask (multiply_mask a (get_m wa))"
               using asm0 mult_add_states multiply_valid upper_valid_aux valid_state.simps by blast
             moreover have "valid_mask (multiply_mask b (get_m wb))"
               using asm0 mult_add_states multiply_valid upper_valid valid_state.simps by blast
             ultimately show ?thesis
               by (metis (no_types, lifting) Abs_state_inverse asm0 fst_conv get_pre(2) mem_Collect_eq multiply.simps multiply_mask_def multiply_valid order_trans p_greater_exists padd_comm pgte.rep_eq)
           qed
           ultimately show "pgte (get_m x hl) (get_m (multiply (padd a b) xx) hl)"
             by (simp add: padd.rep_eq pgte.rep_eq)
         qed
       qed
       ultimately show "x \<in> multiply_sem_assertion (padd a b) (cwand A B)"
         by (metis PartialSA.up_closed_def PartialSA.upper_closure_up_closed in_multiply_refl multiply_sem_assertion.simps)
     qed
   qed
   then show ?thesis
     using combinable_def by presburger
 qed
 
 lemma combinable_cwand:
   assumes "combinable B"
       and "intuitionistic B"
     shows "combinable (cwand A B)"
 proof (rule combinableI)
   fix \<alpha> \<beta> assume asm0: "ppos \<alpha> \<and> ppos \<beta> \<and> padd \<alpha> \<beta> = pwrite"
   then have "pgte pwrite \<alpha> \<and> pgte pwrite \<beta>"
     by (metis p_greater_exists padd_comm)
   show "multiply_sem_assertion \<alpha> (cwand A B) \<otimes> multiply_sem_assertion \<beta> (cwand A B) \<subseteq> cwand A B"
   proof
-    fix w assume "w \<in> multiply_sem_assertion \<alpha> (cwand A B) \<otimes> multiply_sem_assertion \<beta> (cwand A B)"
+    fix w assume asm: "w \<in> multiply_sem_assertion \<alpha> (cwand A B) \<otimes> multiply_sem_assertion \<beta> (cwand A B)"
     then obtain xa xb where "Some w = xa \<oplus> xb" "xa \<in> multiply_sem_assertion \<alpha> (cwand A B)" "xb \<in> multiply_sem_assertion \<beta> (cwand A B)"
       by (meson PartialSA.add_set_elem)
     then obtain wa wb where "wa \<in> cwand A B" "wb \<in> cwand A B" "xa \<succeq> multiply \<alpha> wa" "xb \<succeq> multiply \<beta> wb"
       by (meson in_multiply_sem)
     then obtain r: "\<And>a x. a \<in> A \<and> Some x = R a wa \<oplus> a \<Longrightarrow> x \<in> B" "\<And>a x. a \<in> A \<and> Some x = R a wb \<oplus> a \<Longrightarrow> x \<in> B"
       using cwand_def by blast
     show "w \<in> cwand A B"
     proof (rule in_cwand)
       fix a x assume asm1: "a \<in> A \<and> Some x = R a w \<oplus> a"
       have "\<not> scalable w a"
       proof (rule ccontr)
         assume "\<not> \<not> scalable w a"
         then have "R a w = w \<and> \<not> a |#| R a w"
           by (simp add: R_def scalable_def w_in_scaled)
         then show False
           using PartialSA.commutative PartialSA.defined_def asm1 by auto
       qed
-      then have "get_h (R a w) = get_h w \<and> get_m (R a w) = comp_min_mask (get_m a) (get_m w)"
+      then have r3: "get_h (R a w) = get_h w \<and> get_m (R a w) = comp_min_mask (get_m a) (get_m w)"
         using non_scalable_R_charact by blast
       moreover obtain p where "a |#| multiply p w" "ppos p \<and> pgte pwrite p"
         using \<open>\<not> scalable w a\<close> non_scalable_instantiate by blast
       moreover have "\<not> scalable wa a"
       proof -
         have "a |#| multiply (pmult \<alpha> p) wa"
         proof -
           have "w \<succeq> xa" using \<open>Some w = xa \<oplus> xb\<close> using PartialSA.greater_def by blast
           then have "multiply p w \<succeq> multiply p xa"
             using calculation(3) multiply_order by blast
           then have "multiply p w \<succeq> multiply (pmult \<alpha> p) wa"
           proof -
             have "multiply p w \<succeq> multiply p (multiply \<alpha> wa)"
               using PartialSA.succ_trans \<open>w \<succeq> xa\<close> \<open>xa \<succeq> multiply \<alpha> wa\<close> calculation(3) multiply_order by blast
             then show ?thesis
               using \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> calculation(3) multiply_twice pmult_comm by auto
           qed
           then show ?thesis
             using PartialSA.asso3 PartialSA.defined_def PartialSA.minus_some calculation(2) by fastforce
         qed
         moreover have "ppos (pmult \<alpha> p) \<and> pgte pwrite (pmult \<alpha> p)"
           by (metis Rep_prat_inverse \<open>ppos p \<and> pgte pwrite p\<close> add.right_neutral asm0 dual_order.strict_iff_order padd.rep_eq pgte.rep_eq pmult_comm pmult_ppos pmult_special(2) pnone.rep_eq ppos.rep_eq ppos_eq_pnone padd_one_ineq_sum)
         ultimately show ?thesis
           using scalable_def scaled_def by auto
       qed
-      then have "get_h (R a wa) = get_h wa \<and> get_m (R a wa) = comp_min_mask (get_m a) (get_m wa)"
+      then have r1: "get_h (R a wa) = get_h wa \<and> get_m (R a wa) = comp_min_mask (get_m a) (get_m wa)"
         using non_scalable_R_charact by blast
       moreover have "R a wa |#| a"
       proof (rule compatibleI)
         have "larger_heap (get_h w) (get_h xa) \<and> larger_heap (get_h xa) (get_h wa)"
           by (metis PartialSA.commutative PartialSA.greater_equiv \<open>Some w = xa \<oplus> xb\<close> \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> \<open>xa \<succeq> multiply \<alpha> wa\<close> get_h_multiply larger_implies_larger_heap)
         then show "compatible_heaps (get_h (R a wa)) (get_h a)"
           by (metis asm1 calculation(1) calculation(4) larger_heap_comp option.distinct(1) plus_ab_defined)
         show "valid_mask (add_masks (get_m (R a wa)) (get_m a))"
           by (metis PartialSA.unit_neutral calculation(4) minus_empty option.distinct(1) plus_ab_defined unit_charact(2) valid_mask_add_comp_min)
       qed
       then obtain ba where "Some ba = R a wa \<oplus> a"
         using PartialSA.defined_def by auto
 
       moreover have "\<not> scalable wb a"
       proof -
         have "a |#| multiply (pmult \<beta> p) wb"
         proof -
           have "w \<succeq> xb" using \<open>Some w = xa \<oplus> xb\<close>
             using PartialSA.greater_equiv by blast
           then have "multiply p w \<succeq> multiply p xb"
             using calculation(3) multiply_order by blast
           then have "multiply p w \<succeq> multiply (pmult \<beta> p) wb"
           proof -
             have "multiply p w \<succeq> multiply p (multiply \<beta> wb)"
               using PartialSA.succ_trans \<open>w \<succeq> xb\<close> \<open>xb \<succeq> multiply \<beta> wb\<close> calculation(3) multiply_order by blast
             then show ?thesis
               using \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> calculation(3) multiply_twice pmult_comm by auto
           qed
           then show ?thesis
             using PartialSA.asso3 PartialSA.defined_def PartialSA.minus_some calculation(2) by fastforce
         qed
         moreover have "ppos (pmult \<beta> p) \<and> pgte pwrite (pmult \<beta> p)"
           by (simp add: \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> \<open>ppos p \<and> pgte pwrite p\<close> asm0 multiply_smaller_pwrite pmult_ppos)
         ultimately show ?thesis
           using scalable_def scaled_def by auto
       qed
-      then have "get_h (R a wb) = get_h wb \<and> get_m (R a wb) = comp_min_mask (get_m a) (get_m wb)"
+      then have r2: "get_h (R a wb) = get_h wb \<and> get_m (R a wb) = comp_min_mask (get_m a) (get_m wb)"
         using non_scalable_R_charact by blast
       moreover have "R a wb |#| a"
       proof (rule compatibleI)
         have "larger_heap (get_h w) (get_h xb) \<and> larger_heap (get_h xb) (get_h wb)"
           using \<open>Some w = xa \<oplus> xb\<close> \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> \<open>xb \<succeq> multiply \<beta> wb\<close> get_h_multiply larger_heap_def larger_implies_larger_heap plus_charact(2) by fastforce
         then show "compatible_heaps (get_h (R a wb)) (get_h a)"
           by (metis asm1 calculation(1) calculation(6) larger_heap_comp option.simps(3) plus_ab_defined)
         show "valid_mask (add_masks (get_m (R a wb)) (get_m a))"
           by (metis PartialSA.unit_neutral calculation(6) minus_empty option.distinct(1) plus_ab_defined unit_charact(2) valid_mask_add_comp_min)
       qed
       then obtain bb where "Some bb = R a wb \<oplus> a"
         using PartialSA.defined_def by auto
 
       moreover obtain ya where "Some ya = R a wa \<oplus> a"
         using calculation(5) by auto
       then have "ya \<in> B"
         using asm1 r(1) by blast
       then have "multiply \<alpha> ya \<in> multiply_sem_assertion \<alpha> B"
         using in_multiply_refl by blast
       moreover obtain yb where "Some yb = R a wb \<oplus> a"
         using calculation(7) by auto
       then have "yb \<in> B"
         using asm1 r(2) by blast
       then have "multiply \<beta> yb \<in> multiply_sem_assertion \<beta> B"
         using in_multiply_refl by blast
       moreover have "(multiply \<alpha> ya) |#| (multiply \<beta> yb)"
       proof (rule compatibleI)
         have "get_h ya = get_h wa ++ get_h a"
-          using \<open>Some ya = R a wa \<oplus> a\<close> \<open>get_h (R a wa) = get_h wa \<and> get_m (R a wa) = comp_min_mask (get_m a) (get_m wa)\<close> plus_charact(2) by presburger
+          using \<open>Some ya = R a wa \<oplus> a\<close> r1 plus_charact(2) by presburger
         then have "get_h (multiply \<alpha> ya) = get_h wa ++ get_h a"
           using \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> get_h_multiply by presburger
         moreover have "get_h yb = get_h wb ++ get_h a"
-          using \<open>Some yb = R a wb \<oplus> a\<close> \<open>get_h (R a wb) = get_h wb \<and> get_m (R a wb) = comp_min_mask (get_m a) (get_m wb)\<close> plus_charact(2) by presburger
+          using \<open>Some yb = R a wb \<oplus> a\<close> r2 plus_charact(2) by presburger
         then have "get_h (multiply \<beta> yb) = get_h wb ++ get_h a"
           using \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> get_h_multiply by presburger
         moreover have "compatible_heaps (get_h wa) (get_h wb)"
         proof (rule compatible_heapsI)
           fix hl a b assume "get_h wa hl = Some a" "get_h wb hl = Some b"
           then have "get_h xa hl = Some a" "get_h xb hl = Some b"
            apply (metis (full_types) \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> \<open>xa \<succeq> multiply \<alpha> wa\<close> get_h_multiply larger_heap_def larger_implies_larger_heap)
             by (metis \<open>get_h wb hl = Some b\<close> \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> \<open>xb \<succeq> multiply \<beta> wb\<close> get_h_multiply larger_heap_def larger_implies_larger_heap)
           moreover have "compatible_heaps (get_h xa) (get_h xb)"
             by (metis \<open>Some w = xa \<oplus> xb\<close> option.simps(3) plus_ab_defined)
           ultimately show "a = b"
             by (metis compatible_heaps_def compatible_options.simps(1))
         qed
         ultimately show "compatible_heaps (get_h (multiply \<alpha> ya)) (get_h (multiply \<beta> yb))"
-          by (metis PartialSA.commutative PartialSA.core_is_smaller \<open>Some ya = R a wa \<oplus> a\<close> \<open>Some yb = R a wb \<oplus> a\<close> \<open>get_h (R a wa) = get_h wa \<and> get_m (R a wa) = comp_min_mask (get_m a) (get_m wa)\<close> \<open>get_h (R a wb) = get_h wb \<and> get_m (R a wb) = comp_min_mask (get_m a) (get_m wb)\<close> compatible_heaps_sum core_defined(1) core_defined(2) option.distinct(1) plus_ab_defined)
+          by (metis PartialSA.commutative PartialSA.core_is_smaller \<open>Some ya = R a wa \<oplus> a\<close> \<open>Some yb = R a wb \<oplus> a\<close>
+              r1 r2 compatible_heaps_sum core_defined(1) core_defined(2) option.distinct(1) plus_ab_defined)
         show "valid_mask (add_masks (get_m (multiply \<alpha> ya)) (get_m (multiply \<beta> yb)))"
         proof (rule valid_maskI)
           show "\<And>f. add_masks (get_m (multiply \<alpha> ya)) (get_m (multiply \<beta> yb)) (null, f) = pnone"
             by (metis (no_types, opaque_lifting) PartialSA.core_is_smaller add_masks.simps core_defined(2) minus_empty not_None_eq plus_ab_defined valid_mask.simps)
           fix hl 
           have "add_masks (get_m (multiply \<alpha> ya)) (get_m (multiply \<beta> yb)) hl = padd (pmult \<alpha> (get_m ya hl)) (pmult \<beta> (get_m yb hl))"
             using \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> get_m_smaller by auto
           moreover have "get_m ya hl = padd (get_m (R a wa) hl) (get_m a hl) \<and> get_m yb hl = padd (get_m (R a wb) hl) (get_m a hl)"
             using \<open>Some ya = R a wa \<oplus> a\<close> \<open>Some yb = R a wb \<oplus> a\<close> plus_charact(1) by auto          
           ultimately show "pgte pwrite (add_masks (get_m (multiply \<alpha> ya)) (get_m (multiply \<beta> yb)) hl)"
             by (metis PartialSA.unit_neutral asm0 option.distinct(1) padd_one_ineq_sum plus_ab_defined plus_charact(1) valid_mask.simps)
         qed
       qed
       then obtain y where "Some y = multiply \<alpha> ya \<oplus> multiply \<beta> yb"
         using PartialSA.defined_def by auto
       moreover have "x \<succeq> y"
       proof (rule greaterI)
         have "get_h y = get_h ya ++ get_h yb"
           using \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> calculation(10) get_h_multiply plus_charact(2) by presburger
         moreover have "get_h ya = get_h wa ++ get_h a"
-          using \<open>Some ya = R a wa \<oplus> a\<close> \<open>get_h (R a wa) = get_h wa \<and> get_m (R a wa) = comp_min_mask (get_m a) (get_m wa)\<close> plus_charact(2) by presburger
+          using \<open>Some ya = R a wa \<oplus> a\<close> r1 plus_charact(2) by presburger
         moreover have "get_h yb = get_h wb ++ get_h a"
-          using \<open>Some yb = R a wb \<oplus> a\<close> \<open>get_h (R a wb) = get_h wb \<and> get_m (R a wb) = comp_min_mask (get_m a) (get_m wb)\<close> plus_charact(2) by presburger
+          using \<open>Some yb = R a wb \<oplus> a\<close> r2 plus_charact(2) by presburger
         moreover have "larger_heap (get_h x) (get_h wa)"
         proof -
           have "larger_heap (get_h x) (get_h xa)"
-            by (metis PartialSA.greater_def \<open>Some w = xa \<oplus> xb\<close> \<open>get_h (R a w) = get_h w \<and> get_m (R a w) = comp_min_mask (get_m a) (get_m w)\<close> asm1 larger_heap_trans larger_implies_larger_heap)
+            by (metis PartialSA.greater_def \<open>Some w = xa \<oplus> xb\<close> r3 asm1 larger_heap_trans larger_implies_larger_heap)
           moreover have "larger_heap (get_h xa) (get_h wa)"
             by (metis \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> \<open>xa \<succeq> multiply \<alpha> wa\<close> get_h_multiply larger_implies_larger_heap)
           ultimately show ?thesis
             using larger_heap_trans by blast
         qed
         moreover have "larger_heap (get_h x) (get_h wb)"
         proof -
           have "larger_heap (get_h x) (get_h xb)"
-            by (metis PartialSA.greater_def PartialSA.greater_equiv \<open>Some w = xa \<oplus> xb\<close> \<open>get_h (R a w) = get_h w \<and> get_m (R a w) = comp_min_mask (get_m a) (get_m w)\<close> asm1 larger_heap_trans larger_implies_larger_heap)
+            by (metis PartialSA.greater_def PartialSA.greater_equiv \<open>Some w = xa \<oplus> xb\<close> r3 asm1 larger_heap_trans larger_implies_larger_heap)
           moreover have "larger_heap (get_h xb) (get_h wb)"
             by (metis \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> \<open>xb \<succeq> multiply \<beta> wb\<close> get_h_multiply larger_implies_larger_heap)
           ultimately show ?thesis
             using larger_heap_trans by blast
         qed
         moreover have "larger_heap (get_h x) (get_h a)"
           using PartialSA.greater_equiv asm1 larger_implies_larger_heap by blast
         ultimately show "larger_heap (get_h x) (get_h y)"          
           by (simp add: larger_heap_plus)
         show "greater_mask (get_m x) (get_m y)"
         proof (rule greater_maskI)
           fix hl 
           have "get_m x hl = padd (get_m (R a w) hl) (get_m a hl)"
             using asm1 plus_charact(1) by auto
           moreover have "get_m y hl = padd (pmult \<alpha> (padd (get_m (R a wa) hl) (get_m a hl))) (pmult \<beta> (padd (get_m (R a wb) hl) (get_m a hl)))"
             by (metis \<open>Some y = multiply \<alpha> ya \<oplus> multiply \<beta> yb\<close> \<open>Some ya = R a wa \<oplus> a\<close> \<open>Some yb = R a wb \<oplus> a\<close> \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> add_masks.simps get_m_smaller plus_charact(1))
 
-          moreover have "padd (pmult \<alpha> (padd (get_m (R a wa) hl) (get_m a hl))) (pmult \<beta> (padd (get_m (R a wb) hl) (get_m a hl)))
+          moreover have equ: "padd (pmult \<alpha> (padd (get_m (R a wa) hl) (get_m a hl))) (pmult \<beta> (padd (get_m (R a wb) hl) (get_m a hl)))
 = padd (padd (pmult \<alpha> (get_m a hl)) (pmult \<beta> (get_m a hl))) (padd (pmult \<alpha> (get_m (R a wa) hl)) (pmult \<beta> (get_m (R a wb) hl)))"
             using padd_asso padd_comm pmult_distr by force
 
           have "pgte (get_m (R a w) hl) (padd (pmult \<alpha> (get_m (R a wa) hl)) (pmult \<beta> (get_m (R a wb) hl)))"
           proof (cases "pgte (get_m w hl) (comp_one (get_m a hl))")
             case True
             then have "get_m (R a w) hl = (comp_one (get_m a hl))"
-              using \<open>get_h (R a w) = get_h w \<and> get_m (R a w) = comp_min_mask (get_m a) (get_m w)\<close> comp_min_mask_def pmin_is by presburger
+              using r3 comp_min_mask_def pmin_is by presburger
             moreover have "pgte (comp_one (get_m a hl)) (get_m (R a wa) hl)"
-              by (metis \<open>get_h (R a wa) = get_h wa \<and> get_m (R a wa) = comp_min_mask (get_m a) (get_m wa)\<close> comp_min_mask_def pmin_comm pmin_greater)
+              by (metis r1 comp_min_mask_def pmin_comm pmin_greater)
             then have "pgte (pmult \<alpha> (comp_one (get_m a hl))) (pmult \<alpha> (get_m (R a wa) hl))"
               by (metis pmult_comm pmult_order)
             moreover have "pgte (comp_one (get_m a hl)) (get_m (R a wb) hl)"
-              by (metis \<open>get_h (R a wb) = get_h wb \<and> get_m (R a wb) = comp_min_mask (get_m a) (get_m wb)\<close> comp_min_mask_def pmin_comm pmin_greater)
+              by (metis r2 comp_min_mask_def pmin_comm pmin_greater)
             then have "pgte (pmult \<beta> (comp_one (get_m a hl))) (pmult \<beta> (get_m (R a wb) hl))"
               by (metis pmult_comm pmult_order)
             ultimately show ?thesis
               using \<open>pgte (comp_one (get_m a hl)) (get_m (R a wa) hl)\<close> \<open>pgte (comp_one (get_m a hl)) (get_m (R a wb) hl)\<close> asm0 padd_one_ineq_sum by presburger
           next
             case False
             then have "get_m (R a w) hl = get_m w hl"
-              by (metis \<open>get_h (R a w) = get_h w \<and> get_m (R a w) = comp_min_mask (get_m a) (get_m w)\<close> comp_min_mask_def not_pgte_charact pgt_implies_pgte pmin_comm pmin_is)
+              by (metis r3 comp_min_mask_def not_pgte_charact pgt_implies_pgte pmin_comm pmin_is)
             moreover have "pgte (get_m w hl) (padd (pmult \<alpha> (get_m wa hl)) (pmult \<beta> (get_m wb hl)))"
             proof -
               have "pgte (get_m w hl) (padd (get_m xa hl) (get_m xb hl))"
                 using \<open>Some w = xa \<oplus> xb\<close> not_pgte_charact pgt_implies_pgte plus_charact(1) by auto
               moreover have "pgte (get_m xa hl) (pmult \<alpha> (get_m wa hl))"
                 by (metis \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> \<open>xa \<succeq> multiply \<alpha> wa\<close> get_m_smaller larger_implies_greater_mask_hl)
               moreover have "pgte (get_m xb hl) (pmult \<beta> (get_m wb hl))"
                 by (metis \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> \<open>xb \<succeq> multiply \<beta> wb\<close> get_m_smaller larger_implies_greater_mask_hl)
               ultimately show ?thesis
                 by (simp add: padd.rep_eq pgte.rep_eq)
             qed
             moreover have "pgte (pmult \<alpha> (get_m wa hl)) (pmult \<alpha> (get_m (R a wa) hl))"
               by (metis R_smaller larger_implies_greater_mask_hl pmult_comm pmult_order)
             moreover have "pgte (pmult \<beta> (get_m wb hl)) (pmult \<beta> (get_m (R a wb) hl))"
               by (metis R_smaller larger_implies_greater_mask_hl pmult_comm pmult_order)
             ultimately show ?thesis
               using padd.rep_eq pgte.rep_eq by force
           qed
           moreover have "get_m x hl = padd (get_m (R a w) hl) (get_m a hl)"
             using calculation(1) by auto
           moreover have "get_m y hl = padd (pmult \<alpha> (get_m ya hl)) (pmult \<beta> (get_m yb hl))"
             using \<open>Some y = multiply \<alpha> ya \<oplus> multiply \<beta> yb\<close> \<open>pgte pwrite \<alpha> \<and> pgte pwrite \<beta>\<close> get_m_smaller plus_charact(1) by auto
           moreover have "padd (pmult \<alpha> (get_m ya hl)) (pmult \<beta> (get_m yb hl)) = 
 padd (pmult \<alpha> (padd (get_m (R a wa) hl) (get_m a hl))) (pmult \<beta> (padd (get_m (R a wb) hl) (get_m a hl)))"
             using calculation(2) calculation(5) by presburger
           moreover have "... = padd (pmult (padd \<alpha> \<beta>) (get_m a hl)) (padd (pmult \<alpha> (get_m (R a wa) hl)) (pmult \<beta> (get_m (R a wb) hl)))"
-            by (metis \<open>padd (pmult \<alpha> (padd (get_m (R a wa) hl) (get_m a hl))) (pmult \<beta> (padd (get_m (R a wb) hl) (get_m a hl))) = padd (padd (pmult \<alpha> (get_m a hl)) (pmult \<beta> (get_m a hl))) (padd (pmult \<alpha> (get_m (R a wa) hl)) (pmult \<beta> (get_m (R a wb) hl)))\<close> pmult_comm pmult_distr)
+            by (metis equ pmult_comm pmult_distr)
           ultimately show "pgte (get_m x hl) (get_m y hl)"
             using asm0 p_greater_exists padd_asso padd_comm pmult_special(1) by force
         qed
       qed
       ultimately have "y \<in> multiply_sem_assertion \<alpha> B \<otimes> multiply_sem_assertion \<beta> B"
         using PartialSA.add_set_elem by blast
       then have "y \<in> multiply_sem_assertion pwrite B"
         by (metis asm0 assms(1) combinable_def not_pgte_charact pgt_implies_pgte subsetD)
       then obtain b where "y \<succeq> multiply pwrite b" "b \<in> B"
         using in_multiply_sem by blast
       then have "multiply pwrite b = b"
         by (metis Rep_state_inverse get_h_m mult_write_mask multiply.simps)
       then have "y \<in> B"
         by (metis \<open>b \<in> B\<close> \<open>y \<succeq> multiply pwrite b\<close> assms(2) intuitionistic_def)
       show "x \<in> B"
         using \<open>x \<succeq> y\<close> \<open>y \<in> B\<close> assms(2) intuitionistic_def by blast
     qed
   qed
 qed
 
 
 
 
 
 subsection Theorems
 
 text \<open>The following theorem is crucial to use the package logic~\cite{Dardinier22} to automatically
 compute footprints of combinable wands.\<close>
 
 theorem R_mono_transformer:
   "PartialSA.mono_transformer (R a)"
 proof -
   have "R a unit = unit"
     by (simp add: PartialSA.succ_antisym PartialSA.unit_smaller R_smaller)
   moreover have "\<And>\<phi> \<phi>'. \<phi>' \<succeq> \<phi> \<Longrightarrow> R a \<phi>' \<succeq> R a \<phi>"
   proof -
     fix \<phi> \<phi>'
     assume "\<phi>' \<succeq> \<phi>"
     show "R a \<phi>' \<succeq> R a \<phi>"
     proof (cases "scalable \<phi>' a")
       case True
       then show ?thesis
         by (metis PartialSA.succ_trans R_def R_smaller \<open>\<phi>' \<succeq> \<phi>\<close>)
     next
       case False
       then obtain p where "ppos p" "pgte pwrite p" "multiply p \<phi>' |#| a"
         by (metis PartialSA.commutative PartialSA.defined_def non_scalable_instantiate)
       then have "multiply p \<phi> |#| a"
         using PartialSA.smaller_compatible \<open>\<phi>' \<succeq> \<phi>\<close> multiply_order by blast
       then have "\<not> scalable \<phi> a"
         using PartialSA.commutative PartialSA.defined_def \<open>pgte pwrite p\<close> \<open>ppos p\<close> scalable_def scaled_def by auto
 
       moreover have "greater_mask (comp_min_mask (get_m a) (get_m \<phi>')) (comp_min_mask (get_m a) (get_m  \<phi>))"
       proof (rule greater_maskI)
         fix hl show "pgte (comp_min_mask (get_m a) (get_m \<phi>') hl) (comp_min_mask (get_m a) (get_m \<phi>) hl)"
         proof (cases "pgte (get_m \<phi>' hl) (comp_one (get_m a hl))")
           case True
           then show ?thesis
             by (metis comp_min_mask_def pmin_comm pmin_greater pmin_is)
         next
           case False
           then show ?thesis
             by (metis PartialSA.succ_trans R_smaller \<open>\<phi>' \<succeq> \<phi>\<close> calculation comp_min_mask_def larger_implies_greater_mask_hl non_scalable_R_charact not_pgte_charact pgt_implies_pgte pmin_comm pmin_is)
         qed
       qed
       ultimately show ?thesis
         using False \<open>\<phi>' \<succeq> \<phi>\<close> greaterI larger_implies_larger_heap non_scalable_R_charact by presburger
     qed
   qed
   ultimately show ?thesis
     by (simp add: PartialSA.mono_transformer_def)
 qed
 
 theorem properties_of_combinable_wands:
   assumes "intuitionistic B"
     shows "combinable B \<Longrightarrow> combinable (cwand A B)"
       and "cwand A B \<subseteq> wand A B"
       and "binary A \<Longrightarrow> cwand A B = wand A B"
   by (simp_all add: assms combinable_cwand cwand_stronger binary_same dual_order.eq_iff)
 
 
 end
diff --git a/thys/Combinable_Wands/Mask.thy b/thys/Combinable_Wands/Mask.thy
--- a/thys/Combinable_Wands/Mask.thy
+++ b/thys/Combinable_Wands/Mask.thy
@@ -1,499 +1,499 @@
 subsection \<open>Permission masks: Maps from heap locations to permission amounts\<close>
 
 theory Mask
   imports PosRat
 begin
 
 subsubsection \<open>Definitions\<close>
 
 type_synonym field = string
 type_synonym address = nat
 type_synonym heap_loc = "address \<times> field"
 
 type_synonym mask = "heap_loc \<Rightarrow> prat"
 type_synonym bmask = "heap_loc \<Rightarrow> 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 \<Rightarrow> mask \<Rightarrow> mask" where
   "multiply_mask p \<pi> hl = pmult p (\<pi> hl)"
 
 fun empty_mask where
   "empty_mask hl = pnone"
 
 fun empty_bmask where
   "empty_bmask hl = False"
 
 fun add_acc where "add_acc \<pi> hl p = \<pi>(hl := padd (\<pi> hl) p)"
 
 inductive rm_acc where
   "\<pi> hl = padd p r \<Longrightarrow> rm_acc \<pi> hl p (\<pi>(hl := r))"
 
 fun add_masks where
   "add_masks \<pi>' \<pi> hl = padd (\<pi>' hl) (\<pi> hl)"
 
 definition greater_mask where
   "greater_mask \<pi>' \<pi> \<longleftrightarrow> (\<exists>r. \<pi>' = add_masks \<pi> r)"
 
 fun uni_mask where
   "uni_mask hl p = empty_mask(hl := p)"
 
 fun valid_mask :: "mask \<Rightarrow> bool" where
   "valid_mask \<pi> \<longleftrightarrow> (\<forall>hl. pgte pwrite (\<pi> hl)) \<and> (\<forall>f. \<pi> (null, f) = pnone)"
 
 definition valid_null :: "mask \<Rightarrow> bool" where
   "valid_null \<pi> \<longleftrightarrow> (\<forall>f. \<pi> (null, f) = pnone)"
 
 definition equal_on_mask where
   "equal_on_mask \<pi> h h' \<longleftrightarrow> (\<forall>hl. ppos (\<pi> hl) \<longrightarrow> h hl = h' hl)"
 
 definition equal_on_bmask where
   "equal_on_bmask \<pi> h h' \<longleftrightarrow> (\<forall>hl. \<pi> hl \<longrightarrow> h hl = h' hl)"
 
 definition big_add_masks where
   "big_add_masks \<Pi> \<Pi>' h = add_masks (\<Pi> h) (\<Pi>' h)"
 
 definition big_greater_mask where
   "big_greater_mask \<Pi> \<Pi>' \<longleftrightarrow> (\<forall>h. greater_mask (\<Pi> h) (\<Pi>' h))"
 
 definition greater_bmask where
   "greater_bmask H H' \<longleftrightarrow> (\<forall>h. H' h \<longrightarrow> H h)"
 
 definition update_dm where
   "update_dm dm \<pi> \<pi>' hl \<longleftrightarrow> (dm hl \<or> pgt (\<pi> hl) (\<pi>' hl))"
 
 fun pre_get_m where "pre_get_m \<phi> = fst \<phi>"
 fun pre_get_h where "pre_get_h \<phi> = snd \<phi>"
 fun srm_acc where "srm_acc \<phi> hl p = (rm_acc (pre_get_m \<phi>) hl p, pre_get_h \<phi>)"
 
 
 datatype val = Bool (the_bool: bool) | Address (the_address: address) | Rat (the_rat: prat)
 
 definition upper_bounded :: "mask \<Rightarrow> prat \<Rightarrow> bool" where
   "upper_bounded \<pi> p \<longleftrightarrow> (\<forall>hl. pgte p (\<pi> hl))"
 
 
 
 
 subsubsection \<open>Lemmas\<close>
 
 lemma ssubsetI:
   assumes "\<And>\<pi> h. (\<pi>, h) \<in> A \<Longrightarrow> (\<pi>, h) \<in> B"
   shows "A \<subseteq> B"
   using assms by auto
 
 lemma double_inclusion:
   assumes "A \<subseteq> B"
       and "B \<subseteq> 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:
   "\<pi> = add_masks \<pi> empty_mask"
 proof (rule ext)
   fix x show "\<pi> x = add_masks \<pi> 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 \<pi> hl p = add_masks \<pi> (uni_mask hl p)"
 proof (rule ext)
   fix x show "add_acc \<pi> hl p x = add_masks \<pi> (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) \<longleftrightarrow> valid_null a \<and> valid_null b"
   by (metis (mono_tags, lifting) add_masks.simps padd_zero valid_null_def)
 
 lemma valid_maskI:
   assumes "\<And>hl. pgte pwrite (\<pi> hl)"
       and "\<And>f. \<pi> (null, f) = pnone"
     shows "valid_mask \<pi>"
   by (simp add: assms(1) assms(2))
 
 lemma greater_mask_equiv_def:
   "greater_mask \<pi>' \<pi> \<longleftrightarrow> (\<forall>hl. pgte (\<pi>' hl) (\<pi> hl))"
   (is "?A \<longleftrightarrow> ?B")
 proof (rule iffI)
   show "?A \<Longrightarrow> ?B"
   proof (clarify)
     fix hl assume "greater_mask \<pi>' \<pi>"
     then obtain r where "\<pi>' = add_masks \<pi> r"
       using greater_mask_def by blast
     then show "pgte (\<pi>' hl) (\<pi> hl)"
       using Rep_prat padd.rep_eq pgte.rep_eq by auto
   qed
   show "?B \<Longrightarrow> ?A"
   proof -
     assume ?B
     let ?r = "\<lambda>hl. (SOME p. \<pi>' hl = padd (\<pi> hl) p)"
     have "\<pi>' = add_masks \<pi> ?r"
     proof (rule ext)
       fix hl
       have "\<pi>' hl = padd (\<pi> hl) (?r hl)"
         by (meson \<open>\<forall>hl. pgte (\<pi>' hl) (\<pi> hl)\<close> p_greater_exists someI_ex)
       then show "\<pi>' hl = add_masks \<pi> ?r hl"
         by auto
     qed
     then show ?A
       using greater_mask_def by blast
   qed
 qed
 
 lemma greater_maskI:
   assumes "\<And>hl. pgte (\<pi>' hl) (\<pi> hl)"
   shows "greater_mask \<pi>' \<pi>"
   by (simp add: assms greater_mask_equiv_def)
 
 lemma greater_mask_properties:
   "greater_mask \<pi> \<pi>"
   "greater_mask a b \<and> greater_mask b c \<Longrightarrow> greater_mask a c"
   "greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>' \<Longrightarrow> \<pi> = \<pi>'"
   apply (simp add: greater_maskI pgte.rep_eq)
   apply (metis add_masks_asso greater_mask_def)
 proof (rule ext)
   fix x assume "greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>'"
-  show "\<pi> x = \<pi>' x"
-    by (meson \<open>greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>'\<close> greater_mask_equiv_def pgte_antisym)
+  then show "\<pi> x = \<pi>' x"
+    by (meson greater_mask_equiv_def pgte_antisym)
 qed
 
 lemma greater_mask_decomp:
   assumes "greater_mask a (add_masks b c)"
   shows "\<exists>a1 a2. a = add_masks a1 a2 \<and> greater_mask a1 b \<and> 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 "\<And>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 \<and> valid_mask c"
   using add_masks_comm assms(1) assms(2) upper_valid_aux by blast
 
 lemma equal_on_bmaskI:
   assumes "\<And>hl. \<pi> hl \<Longrightarrow> h hl = h' hl"
   shows "equal_on_bmask \<pi> 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 \<Longrightarrow> (\<exists>C. A = big_add_masks B C)"
 proof -
   assume "big_greater_mask A B"
   let ?C = "\<lambda>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) \<open>big_greater_mask A B\<close> 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 (\<lambda>h. SOME r. A h = add_masks (B h) r) x"
       by (metis (no_types, lifting) big_add_masks_def)
   qed
   then show "\<exists>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 \<Pi> (\<lambda>_. empty_mask) = \<Pi>"
 proof (rule ext)
   fix x show "big_add_masks \<Pi> (\<lambda>_. empty_mask) x = \<Pi> x"
     by (metis big_add_masks_def minus_empty)
 qed
 
 lemma sym_equal_on_mask:
   "equal_on_mask \<pi> a b \<longleftrightarrow> equal_on_mask \<pi> b a"
 proof -
   have "\<And>a b. equal_on_mask \<pi> a b \<Longrightarrow> equal_on_mask \<pi> b a"
     by (simp add: equal_on_mask_def)
   then show ?thesis by blast
 qed
 
 lemma greater_mask_uni_equiv:
   "greater_mask \<pi> (uni_mask hl r) \<longleftrightarrow> pgte (\<pi> 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 (\<pi> hl) r"
   shows "greater_mask \<pi> (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 \<pi> \<pi> = dm"
 proof (rule ext)
   fix x show "update_dm dm \<pi> \<pi> x = dm x"
     by (simp add: pgt.rep_eq update_dm_def)
 qed
 
 lemma update_trans:
   assumes "greater_mask \<pi> \<pi>'"
       and "greater_mask \<pi>' \<pi>''"
   shows "update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' = update_dm dm \<pi> \<pi>''"
 proof (rule ext)
   fix hl show "update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl"
   proof -
     have "update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl \<longleftrightarrow> (update_dm dm \<pi> \<pi>') hl \<or> pgt (\<pi>' hl) (\<pi>'' hl)"
       using update_dm_def by metis
     also have "... \<longleftrightarrow> dm hl \<or> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl)"
       using update_dm_def by metis
     moreover have "update_dm dm \<pi> \<pi>'' hl \<longleftrightarrow> dm hl \<or> pgt (\<pi> hl) (\<pi>'' hl)"
       using update_dm_def by metis
     moreover have "pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl) \<longleftrightarrow> pgt (\<pi> hl) (\<pi>'' hl)"
     proof
       show "pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl) \<Longrightarrow> pgt (\<pi> hl) (\<pi>'' hl)"
         by (metis assms(1) assms(2) greater_mask_equiv_def greater_mask_properties(2) not_pgte_charact pgte_antisym)
       show "pgt (\<pi> hl) (\<pi>'' hl) \<Longrightarrow> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' 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 \<pi>' h h'"
       and "greater_bmask \<pi>' \<pi>"
     shows "equal_on_bmask \<pi> h h'"
   by (metis (mono_tags, lifting) assms(1) assms(2) equal_on_bmask_def greater_bmask_def)
 
 lemma update_dm_equal_bmask:
   assumes "\<pi> = add_masks \<pi>' m"   
   shows "equal_on_bmask (update_dm dm \<pi> \<pi>') h' h \<longleftrightarrow> equal_on_mask m h h' \<and> equal_on_bmask dm h h'"
 proof -
   have "equal_on_bmask (update_dm dm \<pi> \<pi>') h' h \<longleftrightarrow> (\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl)"
     by (simp add: equal_on_bmask_def)
   moreover have "\<And>hl. update_dm dm \<pi> \<pi>' hl \<longleftrightarrow> dm hl \<or> pgt (\<pi> hl) (\<pi>' hl)"
     by (simp add: update_dm_def)
   moreover have "(\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl) \<longleftrightarrow> equal_on_mask m h h' \<and> equal_on_bmask dm h h'"
   proof
     show "\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl \<Longrightarrow> equal_on_mask m h h' \<and> 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' \<and> equal_on_bmask dm h h'"
     then have "\<And>hl. update_dm dm \<pi> \<pi>' hl \<Longrightarrow> 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 "\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> 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 "\<not> greater_mask d b"
   then obtain hl where "\<not> 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 "\<And>hl. ppos (\<pi> hl) \<Longrightarrow> h hl = h' hl"
   shows "equal_on_mask \<pi> h h'"
   by (simp add: assms equal_on_mask_def)
 
 lemma greater_equal_on_mask:
   assumes "equal_on_mask \<pi>' h h'"
       and "greater_mask \<pi>' \<pi>"
     shows "equal_on_mask \<pi> h h'"
 proof (rule equal_on_maskI)
   fix hl assume asm: "ppos (\<pi> 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 \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h' \<longleftrightarrow> equal_on_mask (add_masks \<pi>1 \<pi>2) h h'"
 proof
   show "equal_on_mask (add_masks \<pi>1 \<pi>2) h h' \<Longrightarrow> equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h'"
     using add_masks_comm greater_equal_on_mask greater_mask_def by blast
-  assume "equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h'"
+  assume asm0: "equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h'"
   show "equal_on_mask (add_masks \<pi>1 \<pi>2) h h'"
   proof (rule equal_on_maskI)
     fix hl assume "ppos (add_masks \<pi>1 \<pi>2 hl)"
     then show "h hl = h' hl"
     proof (cases "ppos (\<pi>1 hl)")
       case True
       then show ?thesis
-        by (meson \<open>equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h'\<close> equal_on_mask_def)
+        by (meson asm0 equal_on_mask_def)
     next
       case False
       then show ?thesis
-        by (metis \<open>equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h'\<close> \<open>ppos (add_masks \<pi>1 \<pi>2 hl)\<close> add_masks.simps equal_on_mask_def padd_zero ppos_eq_pnone)
+        by (metis asm0 \<open>ppos (add_masks \<pi>1 \<pi>2 hl)\<close> add_masks.simps equal_on_mask_def padd_zero ppos_eq_pnone)
     qed
   qed
 qed
 
 lemma valid_larger_mask:
   "valid_mask \<pi> \<longleftrightarrow> greater_mask full_mask \<pi> "
   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 \<pi> = \<pi>"
 proof (rule ext)
   fix x show "multiply_mask pwrite \<pi> x = \<pi> 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) \<pi> = add_masks (multiply_mask a \<pi>) (multiply_mask b \<pi>)"
 proof (rule ext)
   fix x show "multiply_mask (padd a b) \<pi> x = add_masks (multiply_mask a \<pi>) (multiply_mask b \<pi>) x"    
     by (simp add: multiply_mask_def pmult_comm pmult_distr)
 qed
 
 lemma upper_boundedI:
   assumes "\<And>hl. pgte p (\<pi> hl)"
   shows "upper_bounded \<pi> p"
   by (simp add: assms upper_bounded_def)
 
 lemma upper_bounded_smaller:
   assumes "upper_bounded \<pi> a"
   shows "upper_bounded (multiply_mask p \<pi>) (pmult p a)"  
   by (metis assms multiply_mask_def p_greater_exists pmult_distr upper_bounded_def)
 
 lemma upper_bounded_bigger:
   assumes "upper_bounded \<pi> a"
       and "pgte b a"
     shows "upper_bounded \<pi> b"
   by (meson assms(1) assms(2) order_trans pgte.rep_eq upper_bounded_def)
 
 
 lemma valid_mult:
   assumes "valid_mask \<pi>"
       and "pgte pwrite p"
     shows "valid_mask (multiply_mask p \<pi>)"
 proof (rule valid_maskI)
   have "upper_bounded \<pi> pwrite"
     using assms(1) upper_bounded_def by auto
   then have "upper_bounded (multiply_mask p \<pi>) (pmult p pwrite)"
     by (simp add: upper_bounded_smaller)
   then show "\<And>hl. pgte pwrite (multiply_mask p \<pi> hl)"
     by (metis assms(2) pmult_comm pmult_special(1) upper_bounded_bigger upper_bounded_def)
   show "\<And>f. multiply_mask p \<pi> (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 "\<And>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 "\<And>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
+end
\ No newline at end of file
diff --git a/thys/Combinable_Wands/PartialHeapSA.thy b/thys/Combinable_Wands/PartialHeapSA.thy
--- a/thys/Combinable_Wands/PartialHeapSA.thy
+++ b/thys/Combinable_Wands/PartialHeapSA.thy
@@ -1,604 +1,604 @@
 subsection \<open>Partial heaps: Partial maps from heap location to values\<close>
 
 theory PartialHeapSA
   imports Mask "Package_logic.PackageLogic"
 begin
 
 subsubsection \<open>Definitions\<close>
 
 type_synonym heap = "heap_loc \<rightharpoonup> val"
 type_synonym pre_state = "mask \<times> heap"
 
 definition valid_heap :: "mask \<Rightarrow> heap \<Rightarrow> bool" where
   "valid_heap \<pi> h \<longleftrightarrow> (\<forall>hl. ppos (\<pi> hl) \<longrightarrow> h hl \<noteq> None)"
 
 fun valid_state :: "pre_state \<Rightarrow> bool" where
   "valid_state (\<pi>, h) \<longleftrightarrow> valid_mask \<pi> \<and> valid_heap \<pi> h"
 
 lemma valid_stateI:
   assumes "valid_mask \<pi>"
       and "\<And>hl. ppos (\<pi> hl) \<Longrightarrow> h hl \<noteq> None"
     shows "valid_state (\<pi>, 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 = "{ \<phi> |\<phi>. valid_state \<phi> }"
   using valid_pre_unit by blast
 
 fun get_m :: "state \<Rightarrow> mask" where "get_m a = fst (Rep_state a)"
 fun get_h :: "state \<Rightarrow> heap" where "get_h a = snd (Rep_state a)"
 
 fun compatible_options where
   "compatible_options (Some a) (Some b) \<longleftrightarrow> a = b"
 | "compatible_options _ _ \<longleftrightarrow> True"
 
 definition compatible_heaps :: "heap \<Rightarrow> heap \<Rightarrow> bool" where
   "compatible_heaps h h' \<longleftrightarrow> (\<forall>hl. compatible_options (h hl) (h' hl))"
 
 definition compatible :: "pre_state \<Rightarrow> pre_state \<Rightarrow> bool" where
   "compatible \<phi> \<phi>' \<longleftrightarrow> compatible_heaps (snd \<phi>) (snd \<phi>') \<and> valid_mask (add_masks (fst \<phi>) (fst \<phi>'))"
 
 fun add_states :: "pre_state \<Rightarrow> pre_state \<Rightarrow> pre_state" where
   "add_states (\<pi>, h) (\<pi>', h') = (add_masks \<pi> \<pi>', h ++ h')"
 
 definition larger_heap where
   "larger_heap h' h \<longleftrightarrow> (\<forall>hl x. h hl = Some x \<longrightarrow> h' hl = Some x)"
 
 definition unit :: "state" where
   "unit = Abs_state (empty_mask, empty_heap)"
 
 definition plus :: "state \<Rightarrow> state \<rightharpoonup> state" (infixl "\<oplus>" 63) where
   "a \<oplus> 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 \<Rightarrow> state" (" |_| ") where
   "core \<phi> = Abs_state (empty_mask, get_h \<phi>)"
 
 definition stable :: "state \<Rightarrow> bool" where
   "stable \<phi> \<longleftrightarrow> (\<forall>hl. ppos (get_m \<phi> hl) \<longleftrightarrow> get_h \<phi> hl \<noteq> None)"
 
 
 
 
 
 
 
 
 subsubsection Lemmas
 
 lemma valid_heapI:
   assumes "\<And>hl. ppos (\<pi> hl) \<Longrightarrow> h hl \<noteq> None"
   shows "valid_heap \<pi> 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 \<noteq> None"
     by (metis add_masks.simps assms ppos_add valid_heap_def valid_state.simps)
 qed
 
 lemma compatible_heapsI:
   assumes "\<And>hl a b. h hl = Some a \<Longrightarrow> h' hl = Some b \<Longrightarrow> a = b"
   shows "compatible_heaps h h'"
   by (metis assms compatible_heaps_def compatible_options.elims(3))
 
 lemma compatibleI_old:
   assumes "\<And>hl x y. snd \<phi> hl = Some x \<and> snd \<phi>' hl = Some y \<Longrightarrow> x = y"
       and "valid_mask (add_masks (fst \<phi>) (fst \<phi>'))"
     shows "compatible \<phi> \<phi>'"
   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 "\<And>hl x. h hl = Some x \<Longrightarrow> 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 \<open>(a ++ b) hl = Some x\<close> assms(2) larger_heap_def map_add_SomeD map_add_find_right)
   next
     case (Some aa)
     then show ?thesis
       by (metis (mono_tags, lifting) \<open>(a ++ b) hl = Some x\<close> 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 \<open>(b ++ c) hl = Some x\<close> assms(2) larger_heap_def map_add_SomeD)
   next
     case (Some bb)
     then show ?thesis
       by (metis \<open>(b ++ c) hl = Some x\<close> 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:
   "\<phi> \<oplus> \<phi>' \<noteq> None \<longleftrightarrow> compatible_heaps (get_h \<phi>) (get_h \<phi>') \<and> valid_mask (add_masks (get_m \<phi>) (get_m \<phi>'))"
   (is "?A \<longleftrightarrow> ?B")
 proof
   show "?A \<Longrightarrow> ?B"
     by (metis compatible_def get_pre(1) get_pre(2) plus_def)
   show "?B \<Longrightarrow> ?A"
     using compatible_def plus_def by auto
 qed
 
 lemma plus_charact:
   assumes "a \<oplus> 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 \<noteq> 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 \<open>ppos (add_masks (get_m a) (get_m b) hl)\<close> 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 \<open>valid_state (add_states (Rep_state a) (Rep_state b))\<close> \<open>x = Abs_state (add_states (Rep_state a) (Rep_state b))\<close> add_states.simps eq_snd_iff get_h.simps)
 qed
 
 lemma commutative:
   "a \<oplus> b = b \<oplus> a"
 proof (cases "compatible_heaps (get_h a) (get_h b) \<and> valid_mask (add_masks (get_m a) (get_m b))")
   case True
-  then have "compatible_heaps (get_h b) (get_h a) \<and> add_masks (get_m a) (get_m b) = add_masks (get_m b) (get_m a)"
+  then have r0: "compatible_heaps (get_h b) (get_h a) \<and> 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 \<open>compatible_heaps (get_h b) (get_h a) \<and> add_masks (get_m a) (get_m b) = add_masks (get_m b) (get_m a)\<close> add_states.simps get_h_m plus_ab_defined plus_def)
+    by (metis True r0 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 \<oplus> b = Some ab \<and> b \<oplus> c = Some bc"
   shows "ab \<oplus> c = a \<oplus> bc"
 proof (cases "ab \<oplus> c")
   case None
   then show ?thesis
   proof (cases "compatible_heaps (get_h ab) (get_h c)")
     case True
     then have "\<not> 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 "\<not> 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 \<noteq> y"
       using compatible_heapsI by blast
     then have "\<not> compatible_heaps (get_h a) (get_h b ++ get_h c)"
     proof (cases "get_h a l")
       case None
       then show ?thesis
         by (metis \<open>(get_h a ++ get_h b) l = Some x\<close> \<open>get_h c l = Some y\<close> \<open>x \<noteq> y\<close> 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 \<open>(get_h a ++ get_h b) l = Some x\<close> \<open>get_h c l = Some y\<close> \<open>x \<noteq> y\<close> 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 \<oplus> 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 \<oplus> b = Some ab \<and> b \<oplus> c = None"
   shows " ab \<oplus> c = None"
 proof (cases "valid_mask (add_masks (get_m b) (get_m c))")
   case True
   then have "\<not> 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 \<noteq> 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 \<open>get_h c l = Some y\<close> \<open>x \<noteq> y\<close> compatible_heaps_def compatible_options.simps(1) plus_ab_defined)
 next
   case False
   then obtain l where "\<not> (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 "\<not> (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 \<open>\<not> pgte pwrite (add_masks (get_m b) (get_m c) l)\<close> order_trans pgte.rep_eq)
   qed
   then show ?thesis
     using plus_ab_defined valid_mask.simps by blast
 qed
 
 lemma core_defined:
   "get_h |\<phi>| = get_h \<phi>"
   "get_m |\<phi>| = 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 \<oplus> |x|"
 proof -
   obtain y where "Some y = x \<oplus> |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| \<oplus> |x|"
 proof -
   obtain y where "Some y = |x| \<oplus> |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 \<oplus> b"
   shows "Some |c| = |a| \<oplus> |b|"
 proof -
   obtain x where "Some x = |a| \<oplus> |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 \<oplus> c"
   shows "\<exists>r. Some |x| = c \<oplus> r"
 proof -
   obtain y where "Some y = c \<oplus> |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 \<oplus> b = Some c"
       and "Some c = c \<oplus> c"
     shows "Some a = a \<oplus> a"
 proof -
   obtain x where "Some x = a \<oplus> 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 \<oplus> x"
       and "Some a = b \<oplus> 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: \<open>unit = Abs_state (empty_mask, empty_heap)\<close> Abs_state_inverse)
   show "get_m unit = empty_mask"
     using \<open>valid_state (empty_mask, empty_heap)\<close> 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 \<oplus> unit"
 proof -
   obtain x where "Some x = a \<oplus> 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 "\<And>hl. ppos (get_m \<phi> hl) \<longleftrightarrow> get_h \<phi> hl \<noteq> None"
   shows "stable \<phi>"
   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 \<oplus> b"
     shows "stable x"
 proof (rule stableI)
   fix hl
   show "ppos (get_m x hl) = (get_h x hl \<noteq> None)" (is "?A \<longleftrightarrow> ?B")
   proof
     show "?A \<Longrightarrow> ?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 \<Longrightarrow> ?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 \<phi>), get_h \<phi>)"
 proof (rule valid_stateI)
   show "valid_mask (multiply_mask p (get_m \<phi>))"
     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 \<phi>) hl) \<Longrightarrow> get_h \<phi> hl \<noteq> 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 \<open>This state model corresponds to a separation algebra\<close>
 
 global_interpretation PartialSA: package_logic plus core unit stable
   defines greater (infixl "\<succeq>" 50) = "PartialSA.greater"
       and add_set (infixl "\<otimes>" 60) = "PartialSA.add_set"
       and defined (infixl "|#|" 60) = "PartialSA.defined"
       and greater_set (infixl "|\<ggreater>|" 50) = "PartialSA.greater_set"
       and minus (infixl "|\<ominus>|" 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 \<succeq> b"
 proof -
   let ?m = "\<lambda>l. SOME p. get_m a l = padd (get_m b l) p"
-  have "get_m a = add_masks (get_m b) ?m"
+  have r0: "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) (\<lambda>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 (\<lambda>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 \<noteq> 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)"
+  ultimately have r2: "(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 \<open>get_m a = add_masks (get_m b) (\<lambda>l. SOME p. get_m a l = padd (get_m b l) p)\<close> add_states.simps)
+      by (metis r0 add_states.simps)
   qed
-  moreover have "compatible_heaps (get_h b) (get_h a) \<and> valid_mask (add_masks (get_m b) ?m)"
-    by (metis Rep_state \<open>compatible_heaps (get_h b) (get_h a)\<close> \<open>get_m a = add_masks (get_m b) (\<lambda>l. SOME p. get_m a l = padd (get_m b l) p)\<close> get_h_m mem_Collect_eq valid_state.simps)
+  moreover have r1: "compatible_heaps (get_h b) (get_h a) \<and> valid_mask (add_masks (get_m b) ?m)"
+    by (metis Rep_state \<open>compatible_heaps (get_h b) (get_h a)\<close> r0 get_h_m mem_Collect_eq valid_state.simps)
   ultimately have "Some a = b \<oplus> Abs_state (?m, get_h a)"
   proof -
     have "Rep_state (Abs_state (?m, get_h a)) = (?m, get_h a)"
       using Abs_state_inverse \<open>valid_state (\<lambda>l. SOME p. get_m a l = padd (get_m b l) p, get_h a)\<close> by blast
     moreover have "compatible (Rep_state b) (?m, get_h a)"
-      using \<open>compatible_heaps (get_h b) (get_h a) \<and> valid_mask (add_masks (get_m b) (\<lambda>l. SOME p. get_m a l = padd (get_m b l) p))\<close> compatible_def by auto
+      using r1 compatible_def by auto
     moreover have "valid_state (add_states (Rep_state b) (?m, get_h a))"
-      by (metis Rep_state \<open>(get_m a, get_h a) = add_states (get_m b, get_h b) (\<lambda>l. SOME p. get_m a l = padd (get_m b l) p, get_h a)\<close> get_h_m mem_Collect_eq)
+      by (metis Rep_state r2 get_h_m mem_Collect_eq)
     ultimately show ?thesis
-      by (metis (no_types, lifting) Rep_state_inverse \<open>(get_m a, get_h a) = add_states (get_m b, get_h b) (\<lambda>l. SOME p. get_m a l = padd (get_m b l) p, get_h a)\<close> get_h_m plus_def)
+      by (metis (no_types, lifting) Rep_state_inverse r2 get_h_m plus_def)
   qed
   then show ?thesis
     by (meson PartialSA.greater_def)
 qed
 
 lemma larger_implies_greater_mask_hl:
   assumes "a \<succeq> 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 \<succeq> 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