diff --git a/thys/Combinable_Wands/CombinableWands.thy b/thys/Combinable_Wands/CombinableWands.thy
new file mode 100755
--- /dev/null
+++ b/thys/Combinable_Wands/CombinableWands.thy
@@ -0,0 +1,884 @@
+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"
+    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)
+    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"
+        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
+      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)
+      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)
+      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
+        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)
+        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"
+        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
+            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
+            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"        
+        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"
+      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
+      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)
+          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
+            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)"
+    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)"
+        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)"
+        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)"
+        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
+        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
+        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)
+        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
+        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
+        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)
+          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)
+          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)))
+= 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
+            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)
+            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)
+            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)
+            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)
+          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
new file mode 100755
--- /dev/null
+++ b/thys/Combinable_Wands/Mask.thy
@@ -0,0 +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)
+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'"
+  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)
+    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)
+    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
diff --git a/thys/Combinable_Wands/PartialHeapSA.thy b/thys/Combinable_Wands/PartialHeapSA.thy
new file mode 100755
--- /dev/null
+++ b/thys/Combinable_Wands/PartialHeapSA.thy
@@ -0,0 +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)"
+    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)
+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"
+  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)"
+  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)
+  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)
+  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
+    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)
+    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)
+  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
diff --git a/thys/Combinable_Wands/PosRat.thy b/thys/Combinable_Wands/PosRat.thy
new file mode 100755
--- /dev/null
+++ b/thys/Combinable_Wands/PosRat.thy
@@ -0,0 +1,340 @@
+section \<open>State Model with Fractional Permissions\<close>
+
+text \<open>In this section, we define a concrete state model based on fractional permissions \cite{Boyland03}.
+A state is a pair of a permission mask and a partial heap.
+A permission mask is a total map from heap locations to a rational between 0 and 1 (included),
+while a partial heap is a partial map from heap locations to values.
+We also define a partial addition on these states, and show that this state model corresponds to a separation algebra.\<close>
+
+subsection \<open>Non-negative rationals (permission amounts)\<close>
+
+theory PosRat
+  imports Main HOL.Rat
+begin
+
+
+
+subsubsection Definitions
+
+typedef prat = "{ r :: rat |r. r \<ge> 0}" by fastforce
+
+setup_lifting type_definition_prat
+
+lift_definition pwrite :: "prat" is "1" by simp
+lift_definition pnone :: "prat" is "0" by simp
+lift_definition half :: "prat" is "1 / 2" by fastforce
+
+lift_definition pgte :: "prat \<Rightarrow> prat \<Rightarrow> bool" is "(\<ge>)" done
+lift_definition pgt :: "prat \<Rightarrow> prat \<Rightarrow> bool" is "(>)" done
+(* lift_definition lte :: "prat \<Rightarrow> prat \<Rightarrow> bool" is "(\<le>)" done *)
+lift_definition lt :: "prat \<Rightarrow> prat \<Rightarrow> bool" is "(<)" done
+lift_definition ppos :: "prat \<Rightarrow> bool" is "\<lambda>p. p > 0" done
+
+lift_definition pmult :: "prat \<Rightarrow> prat \<Rightarrow> prat" is "(*)" by simp
+lift_definition padd :: "prat \<Rightarrow> prat \<Rightarrow> prat" is "(+)" by simp
+
+lift_definition pdiv :: "prat \<Rightarrow> prat \<Rightarrow> prat" is "(/)" by simp
+
+lift_definition pmin :: "prat \<Rightarrow> prat \<Rightarrow> prat" is "(min)" by simp
+lift_definition pmax :: "prat \<Rightarrow> prat \<Rightarrow> prat" is "(max)" by simp
+
+subsubsection Lemmas
+
+lemma pmin_comm:
+  "pmin a b = pmin b a"
+  by (metis Rep_prat_inverse min.commute pmin.rep_eq)
+
+lemma pmin_greater:
+  "pgte a (pmin a b)"
+  by (simp add: pgte.rep_eq pmin.rep_eq)
+
+lemma pmin_is:
+  assumes "pgte a b"
+  shows "pmin a b = b"
+  by (metis Rep_prat_inject assms min_absorb2 pgte.rep_eq pmin.rep_eq)
+
+lemma pmax_comm:
+  "pmax a b = pmax b a"
+  by (metis Rep_prat_inverse max.commute pmax.rep_eq)
+
+lemma pmax_smaller:
+  "pgte (pmax a b) a"
+  by (simp add: pgte.rep_eq pmax.rep_eq)
+
+lemma pmax_is:
+  assumes "pgte a b"
+  shows "pmax a b = a"
+  by (metis Rep_prat_inject assms max.absorb_iff1 pgte.rep_eq pmax.rep_eq)
+
+
+lemma pmax_is_smaller:
+  assumes "pgte x a"
+      and "pgte x b"
+    shows "pgte x (pmax a b)"
+proof (cases "pgte a b")
+  case True
+  then show ?thesis
+    by (simp add: assms(1) pmax_is)
+next
+  case False
+  then show ?thesis
+    using assms(2) pgte.rep_eq pmax.rep_eq by auto
+qed
+
+
+lemma half_between_0_1:
+  "ppos half \<and> pgt pwrite half"
+  by (simp add: half.rep_eq pgt.rep_eq ppos.rep_eq pwrite.rep_eq)
+
+lemma pgt_implies_pgte:
+  assumes "pgt a b"
+  shows "pgte a b"
+  by (meson assms less_imp_le pgt.rep_eq pgte.rep_eq)
+
+lemma half_plus_half:
+  "padd half half = pwrite"
+  by (metis Rep_prat_inject divide_less_eq_numeral1(1) dual_order.irrefl half.rep_eq less_divide_eq_numeral1(1) linorder_neqE_linordered_idom mult.right_neutral one_add_one padd.rep_eq pwrite.rep_eq ring_class.ring_distribs(1))
+
+lemma padd_comm:
+  "padd a b = padd b a"
+  by (metis Rep_prat_inject add.commute padd.rep_eq)
+
+lemma padd_asso:
+  "padd (padd a b) c = padd a (padd b c)"
+  by (metis Rep_prat_inverse group_cancel.add1 padd.rep_eq)
+
+
+lemma p_greater_exists:
+  "pgte a b \<longleftrightarrow> (\<exists>r. a = padd b r)"
+proof (rule iffI)
+  show "pgte a b \<Longrightarrow> \<exists>r. a = padd b r"
+  proof -
+    assume asm: "pgte a b"
+    obtain aa bb where "aa = Rep_prat a" "bb = Rep_prat b"
+      by simp
+    then have "aa \<ge> bb" using asm
+      using pgte.rep_eq by fastforce
+    then obtain rr where "rr = aa - bb"
+      by simp
+    then have "a = padd b (Abs_prat rr)"
+      by (metis Abs_prat_inverse Rep_prat_inject \<open>aa = Rep_prat a\<close> \<open>bb = Rep_prat b\<close> \<open>bb \<le> aa\<close> add.commute diff_add_cancel diff_ge_0_iff_ge mem_Collect_eq padd.rep_eq)
+    then show "\<exists>r. a = padd b r" by blast
+  qed
+  show "\<exists>r. a = padd b r \<Longrightarrow> pgte a b"
+    using Rep_prat padd.rep_eq pgte.rep_eq by force
+qed
+
+
+lemma pgte_antisym:
+  assumes "pgte a b"
+      and "pgte b a"
+    shows "a = b"
+  by (metis Rep_prat_inverse assms(1) assms(2) leD le_less pgte.rep_eq)
+
+lemma greater_sum_both:
+  assumes "pgte a (padd b c)"
+  shows "\<exists>a1 a2. a = padd a1 a2 \<and> pgte a1 b \<and> pgte a2 c"
+proof -
+  obtain aa bb cc where "aa = Rep_prat a" "bb = Rep_prat b" "cc = Rep_prat c"
+    by simp
+  then have "aa \<ge> bb + cc"
+    using assms padd.rep_eq pgte.rep_eq by auto
+  then obtain x where "aa = bb + x" "x \<ge> cc"
+    by (metis add.commute add_le_cancel_left diff_add_cancel)
+  then show ?thesis
+    by (metis assms order_refl p_greater_exists padd_asso pgte.rep_eq)
+qed
+
+
+lemma padd_cancellative:
+  assumes "a = padd x b"
+      and "a = padd y b"
+    shows "x = y"
+  by (metis Rep_prat_inject add_le_cancel_right assms(1) assms(2) leD less_eq_rat_def padd.rep_eq)
+
+
+lemma not_pgte_charact:
+  "\<not> pgte a b \<longleftrightarrow> pgt b a"
+  by (meson not_less pgt.rep_eq pgte.rep_eq)
+
+lemma pgte_pgt:
+  assumes "pgt a b"
+      and "pgte c d"
+    shows "pgt (padd a c) (padd b d)"
+  using assms(1) assms(2) padd.rep_eq pgt.rep_eq pgte.rep_eq by auto
+
+lemma pmult_distr:
+  "pmult a (padd b c) = padd (pmult a b) (pmult a c)"
+  by (metis Rep_prat_inject distrib_left padd.rep_eq pmult.rep_eq)
+
+lemma pmult_comm:
+  "pmult a b = pmult b a"
+  by (metis Rep_prat_inject mult.commute pmult.rep_eq)
+
+lemma pmult_special:
+  "pmult pwrite x = x"
+  "pmult pnone x = pnone"
+  apply (metis Rep_prat_inverse comm_monoid_mult_class.mult_1 pmult.rep_eq pwrite.rep_eq)
+  by (metis Rep_prat_inverse mult_zero_left pmult.rep_eq pnone.rep_eq)
+
+
+
+definition pinv where
+  "pinv p = pdiv pwrite p"
+
+lemma pinv_double_half:
+  assumes "ppos p"
+  shows "pmult half (pinv p) = pinv (padd p p)"
+proof -
+  have "(Fract 1 2) * ((Fract 1 1) / (Rep_prat p)) = (Fract 1 1) / (Rep_prat p + Rep_prat p)"
+    by (metis (no_types, lifting) One_rat_def comm_monoid_mult_class.mult_1 divide_rat mult_2 mult_rat rat_number_expand(3) times_divide_times_eq)
+  then show ?thesis
+    by (metis Rep_prat_inject half.rep_eq mult_2 mult_numeral_1_right numeral_One padd.rep_eq pdiv.rep_eq pinv_def pmult.rep_eq pwrite.rep_eq times_divide_times_eq)
+qed
+
+lemma ppos_mult:
+  assumes "ppos a"
+      and "ppos b"
+    shows "ppos (pmult a b)"
+  using assms(1) assms(2) pmult.rep_eq ppos.rep_eq by auto
+
+lemma padd_zero:
+  "pnone = padd a b \<longleftrightarrow> a = pnone \<and> b = pnone"
+  by (metis Rep_prat Rep_prat_inject add.right_neutral leD le_add_same_cancel2 less_eq_rat_def mem_Collect_eq padd.rep_eq pnone.rep_eq)
+
+lemma ppos_add:
+  assumes "ppos a"
+  shows "ppos (padd a b)"
+  by (metis Rep_prat Rep_prat_inject assms dual_order.strict_iff_order mem_Collect_eq padd_zero pnone.rep_eq ppos.rep_eq)
+
+
+
+lemma pinv_inverts:
+  assumes "pgte a b"
+      and "ppos b"
+    shows "pgte (pinv b) (pinv a)"
+proof -
+  have "Rep_prat a \<ge> Rep_prat b"
+    using assms(1) pgte.rep_eq by auto
+  then have "(Fract 1 1) / Rep_prat b \<ge> (Fract 1 1) / Rep_prat a"
+    by (metis One_rat_def assms(2) frac_le le_numeral_extra(4) ppos.rep_eq zero_le_one)
+  then show ?thesis
+    by (simp add: One_rat_def pdiv.rep_eq pgte.rep_eq pinv_def pwrite.rep_eq)
+qed
+
+
+
+lemma pinv_pmult_ok:
+  assumes "ppos p"
+  shows "pmult p (pinv p) = pwrite"
+proof -
+  obtain r where "r = Rep_prat p" by simp
+  then have "r * ((Fract 1 1) / r) = Fract 1 1"
+    using assms ppos.rep_eq by force
+  then show ?thesis
+    by (metis One_rat_def Rep_prat_inject \<open>r = Rep_prat p\<close> pdiv.rep_eq pinv_def pmult.rep_eq pwrite.rep_eq)
+qed
+
+
+lemma pinv_pwrite:
+  "pinv pwrite = pwrite"
+  by (metis Rep_prat_inverse div_by_1 pdiv.rep_eq pinv_def pwrite.rep_eq)
+
+lemma pmult_ppos:
+  assumes "ppos a"
+      and "ppos b"
+    shows "ppos (pmult a b)"
+  using assms(1) assms(2) pmult.rep_eq ppos.rep_eq by auto
+
+
+lemma ppos_inv:
+  assumes "ppos p"
+  shows "ppos (pinv p)"
+by (metis Rep_prat Rep_prat_inverse assms less_eq_rat_def mem_Collect_eq not_one_le_zero pinv_pmult_ok pmult_comm pmult_special(2) pnone.rep_eq ppos.rep_eq pwrite.rep_eq)
+
+
+lemma pmin_pmax:
+  assumes "pgte x (pmin a b)"
+  shows "x = pmin (pmax x a) (pmax x b)"
+proof (cases "pgte x a")
+  case True
+  then show ?thesis
+    by (metis pmax_is pmax_smaller pmin_comm pmin_is)
+next
+  case False
+  then show ?thesis
+    by (metis assms not_pgte_charact pgt_implies_pgte pmax_is pmax_smaller pmin_comm pmin_is)
+qed
+
+definition comp_one where
+  "comp_one p = (SOME r. padd p r = pwrite)"
+
+lemma padd_comp_one:
+  assumes "pgte pwrite x"
+  shows "padd x (comp_one x) = pwrite"
+  by (metis (mono_tags, lifting) assms comp_one_def p_greater_exists someI_ex)
+
+lemma ppos_eq_pnone:
+  "ppos p \<longleftrightarrow> p \<noteq> pnone"
+  by (metis Rep_prat Rep_prat_inject dual_order.strict_iff_order mem_Collect_eq pnone.rep_eq ppos.rep_eq)
+
+
+
+lemma pmult_order:
+  assumes "pgte a b"
+  shows "pgte (pmult p a) (pmult b p)"
+  using assms p_greater_exists pmult_comm pmult_distr by force
+
+lemma multiply_smaller_pwrite:
+  assumes "pgte pwrite a"
+      and "pgte pwrite b"
+    shows "pgte pwrite (pmult a b)"
+  by (metis assms(1) assms(2) p_greater_exists padd_asso pmult_order pmult_special(1))
+
+
+lemma pmult_pdiv_cancel:
+  assumes "ppos a"
+  shows "pmult a (pdiv x a) = x"
+  by (metis Rep_prat_inject assms divide_cancel_right dual_order.strict_iff_order nonzero_mult_div_cancel_left pdiv.rep_eq pmult.rep_eq ppos.rep_eq)
+
+lemma pmult_padd:
+  "pmult a (padd (pmult b x) (pmult c y)) = padd (pmult (pmult a b) x) (pmult (pmult a c) y)"
+  by (metis Rep_prat_inject mult.assoc pmult.rep_eq pmult_distr)
+
+
+lemma pdiv_smaller:
+  assumes "pgte a b"
+      and "ppos a"
+  shows "pgte pwrite (pdiv b a)"
+proof -
+  let ?a = "Rep_prat a"
+  let ?b = "Rep_prat b"
+  have "?b / ?a \<le> 1"
+    by (meson assms(1) assms(2) divide_le_eq_1_pos pgte.rep_eq ppos.rep_eq)
+  then show ?thesis
+    by (simp add: pdiv.rep_eq pgte.rep_eq pwrite.rep_eq)
+qed
+
+
+lemma sum_coeff:
+  assumes "ppos a"
+      and "ppos b"
+    shows "padd (pdiv a (padd a b)) (pdiv b (padd a b)) = pwrite"
+proof -
+  let ?a = "Rep_prat a"
+  let ?b = "Rep_prat b"
+  have "(?a / (?a + ?b)) + (?b / (?a + ?b)) = 1"
+    by (metis add_divide_distrib add_pos_pos assms(1) assms(2) less_irrefl ppos.rep_eq right_inverse_eq)
+  then show ?thesis
+    by (metis Rep_prat_inject padd.rep_eq pdiv.rep_eq pwrite.rep_eq)
+qed
+
+lemma padd_one_ineq_sum:
+  assumes "padd a b = pwrite"
+      and "pgte x aa"
+      and "pgte x bb"
+    shows "pgte x (padd (pmult a aa) (pmult b bb))"
+  by (metis (mono_tags, lifting) Rep_prat assms(1) assms(2) assms(3) convex_bound_le mem_Collect_eq padd.rep_eq pgte.rep_eq pmult.rep_eq pwrite.rep_eq)
+
+
+end
diff --git a/thys/Combinable_Wands/ROOT b/thys/Combinable_Wands/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Combinable_Wands/ROOT
@@ -0,0 +1,12 @@
+chapter AFP
+
+session Combinable_Wands (AFP) = Package_logic +
+  options [timeout = 300]
+  theories
+    PosRat
+    Mask
+    PartialHeapSA
+    CombinableWands
+  document_files
+    "root.bib"
+    "root.tex"
diff --git a/thys/Combinable_Wands/document/root.bib b/thys/Combinable_Wands/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Combinable_Wands/document/root.bib
@@ -0,0 +1,100 @@
+
+
+@inproceedings{Dockins2009,
+author = {Dockins, Robert and Hobor, Aquinas and Appel, Andrew W.},
+pages = {161--177},
+title = {{A Fresh Look at Separation Algebras and Share Accounting}},
+booktitle = {Asian Symposium on Programming Languages and Systems (APLAS)},
+editor    = {Zhenjiang Hu},
+year = {2009}
+}
+
+@inproceedings{Calcagno2007,
+author = {Calcagno, Cristiano and O'Hearn, Peter W. and Yang, Hongseok},
+pages = {366--375},
+title = {{Local Action and Abstract Separation Logic}},
+booktitle = {Logic in Computer Science (LICS)},
+year = {2007}
+}
+
+@inproceedings{SchwerhoffSummers15,
+ author = {M. Schwerhoff and A. J. Summers},
+ title = {{Lightweight Support for Magic Wands in an Automatic Verifier}},
+ booktitle = {European Conference on Object-Oriented Programming (ECOOP)},
+ pages = {614--638},
+ series = {LIPIcs},
+ year = {2015},
+ volume = {37},
+ editor = {J. T. Boyland},
+ publisher = {Schloss Dagstuhl},
+}
+
+@inproceedings{Dardinier22,
+  author = {Dardinier, Thibault and Parthasarathy, Gaurav and Weeks, No\'e and M\"uller, Peter and Summers, Alexander J.},
+  title = {{Sound Automation of Magic Wands}},
+  booktitle = {Computer Aided Verification (CAV)},
+  year = {2022},
+  note = {To appear}
+}
+
+@inproceedings{Reynolds02a,
+	author = {J. C. Reynolds},
+	title = {{Separation Logic: A Logic for Shared Mutable Data Structures}},
+	booktitle = {Logic in Computer Science (LICS)},
+	Publisher = {IEEE},
+	pages     = {55--74},
+	year = {2002}
+}
+
+@inproceedings{Boyland03,
+author="Boyland, John",
+editor="Cousot, Radhia",
+title="Checking Interference with Fractional Permissions",
+booktitle="Static Analysis (SAS)",
+year="2003",
+pages="55--72",
+}
+
+@article{Boyland10,
+  author    = {John Tang Boyland},
+  title     = {Semantics of fractional permissions with nesting},
+  journal   = {Transactions on Programming Languages and Systems (TOPLAS)},
+  volume    = {32},
+  number    = {6},
+  pages     = {22:1--22:33},
+  year      = {2010},
+  doi       = {10.1145/1749608.1749611},
+  biburl    = {https://dblp.org/rec/journals/toplas/Boyland10.bib}
+}
+
+@inproceedings{JacobsPiessens11,
+  author    = {Bart Jacobs and Frank Piessens},
+  title     = {Expressive modular fine-grained concurrency specification},
+  booktitle = {Principles of Programming Languages (POPL)},
+  pages     = {271--282},
+  year      = {2011},
+  doi       = {10.1145/1926385.1926417},
+  biburl    = {https://dblp.org/rec/conf/popl/JacobsP11.bib}
+}
+
+@inproceedings{LeHobor18,
+author="Le, Xuan-Bach
+and Hobor, Aquinas",
+editor="Ahmed, Amal",
+title="Logical Reasoning for Disjoint Permissions",
+booktitle="European Symposium on Programming (ESOP)",
+year="2018"
+}
+
+@inproceedings{Brotherston20,
+author="Brotherston, James
+and Costa, Diana
+and Hobor, Aquinas
+and Wickerson, John",
+editor="Lahiri, Shuvendu K.
+and Wang, Chao",
+title="Reasoning over Permissions Regions in Concurrent Separation Logic",
+booktitle="Computer Aided Verification (CAV)",
+year="2020"
+}
+
diff --git a/thys/Combinable_Wands/document/root.tex b/thys/Combinable_Wands/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Combinable_Wands/document/root.tex
@@ -0,0 +1,76 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage{eurosym}
+  %for \<euro>
+
+%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
+  %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>
+
+%\usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+  %\<currency>
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+\newcommand{\wand}{\ensuremath{\mathbin{-\!\!*}}}
+
+\begin{document}
+
+\title{A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand}
+  
+\author{Thibault Dardinier}
+\maketitle
+
+\begin{abstract}
+Many separation logics support \emph{fractional permissions}~\cite{Boyland03} to distinguish between read and write access to a heap location, for instance, to allow concurrent reads while enforcing exclusive writes.
+The concept has been generalized to fractional assertions~\cite{Boyland10,JacobsPiessens11,LeHobor18,Brotherston20}. $A^p$ (where $A$ is a separation logic assertion and $p$ a fraction between $0$ and $1$) represents a fraction $p$ of $A$.
+$A^p$ holds in a state $\sigma$ iff there exists a state $\sigma_A$ in which $A$ holds and $\sigma$ is obtained from $\sigma_A$ by multiplying all permission amounts held by $p$.
+
+While $A^{p + q}$ can always be split into $A^p * A^q$, recombining $A^p * A^q$ into $A^{p+q}$ is not always sound.
+We say that $A$ is \emph{combinable} iff the entailment $A^p * A^q \models A^{p+q}$ holds for any two positive fractions $p$ and $q$ such that $p + q \le 1$.
+Combinable assertions are particularly useful to reason about concurrent programs, for instance, to combine the postconditions of parallel branches when they terminate.
+Unfortunately, the magic wand assertion $A \wand B$, commonly used to specify properties of partial data structures, is typically \emph{not} combinable.
+
+In this entry, we formalize a novel, restricted definition of the magic wand, described in a paper at CAV 22~\cite{Dardinier22}, which we call the \emph{combinable wand}.
+We prove some key properties of the combinable wand; in particular, a combinable wand is combinable if its right-hand side is combinable.
+\end{abstract}
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,682 +1,683 @@
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Ackermanns_not_PR
 Actuarial_Mathematics
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BD_Security_Compositional
 BNF_CC
 BNF_Operations
 BTree
 Banach_Steinhaus
 Belief_Revision
 Bell_Numbers_Spivey
 BenOr_Kozen_Reif
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
 CSP_RefTK
 CYK
 CZH_Elementary_Categories
 CZH_Foundations
 CZH_Universal_Constructions
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 Clique_and_Monotone_Circuits
 ClockSynchInst
 Closest_Pair_Points
 CoCon
 CoSMeDis
 CoSMed
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
+Combinable_Wands
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Bounded_Operators
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Conditional_Simplification
 Conditional_Transfer_Rule
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Core_SC_DOM
 Correctness_Algebras
 Cotangent_PFD_Formula
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 Cubic_Quartic_Equations
 DFS_Framework
 DOM_Components
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Dedekind_Real
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Design_Theory
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Digit_Expansions
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 Dominance_CHK
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Equivalence_Relation_Enumeration
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Eval_FO
 Example-Submission
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Axiomatic
 FOL_Harrison
 FOL_Seq_Calc1
 FOL_Seq_Calc2
 FOL_Seq_Calc3
 Factor_Algebraic_Polynomial
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 Finitely_Generated_Abelian_Groups
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Fishers_Inequality
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Foundation_of_geometry
 Fourier
 FO_Theory_Rewriting
 Free-Boolean-Algebra
 Free-Groups
 Frequency_Moments
 Fresh_Identifiers
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 GaleStewart_Games
 Gale_Shapley
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Grothendieck_Schemes
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Hahn_Jordan_Decomposition
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 Hyperdual
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IMP_Compiler
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Independence_CH
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpolation_Polynomials_HOL_Algebra
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Intro_Dest_Elim
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Irrationals_From_THEBOOK
 IsaGeoCoq
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
 Knights_Tour
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 Lifting_the_Exponent
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Logging_Independent_Anonymity
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 LP_Duality
 Lucas_Theorem
 MDP-Algorithms
 MDP-Rewards
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Method
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MiniML
 MiniSail
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multiset_Ordering_NPC
 Multi_Party_Computation
 Multirelations
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 Package_logic
 PAL
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Padic_Ints
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Pluennecke_Ruzsa_Inequality
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Prefix_Free_Code_Combinators
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Program-Conflict-Analysis
 Progress_Tracking
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 Public_Announcement_Logic
 QHLProver
 QR_Decomposition
 Quantales
 Quasi_Borel_Spaces
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Real_Power
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Registers
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Regular_Tree_Relations
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rep_Fin_Groups
 ResiduatedTransitionSystem
 Residuated_Lattices
 Resolution_FOL
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Roth_Arithmetic_Progressions
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Saturation_Framework
 Saturation_Framework_Extensions
 Schutz_Spacetime
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Simplicial_complexes_and_boolean_functions
 SimplifiedOntologicalArgument
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Sophomores_Dream
 Sort_Encodings
 Source_Coding_Theorem
 SpecCheck
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Szemeredi_Regularity
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Three_Circles
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Transitive_Models
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 Types_To_Sets_Extension
 UPF
 UPF_Firewall
 UTP
 Universal_Hash_Families
 Universal_Turing_Machine
 UpDown_Scheme
 Valuation
 Van_Emde_Boas_Trees
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 Virtual_Substitution
 VolpanoSmith
 VYDRA_MDL
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Weighted_Path_Order
 Well_Quasi_Orders
 Wetzels_Problem
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 X86_Semantics
 XML
 Youngs_Inequality
 ZFC_in_HOL
 Zeta_3_Irrational
 Zeta_Function
 pGCL