diff --git a/thys/Package_logic/PackageLogic.thy b/thys/Package_logic/PackageLogic.thy
new file mode 100755
--- /dev/null
+++ b/thys/Package_logic/PackageLogic.thy
@@ -0,0 +1,1420 @@
+section \<open>Package Logic\<close>
+
+text \<open>In this section, we define our package logic, as described in \cite{Dardinier22},
+and then prove that this logic is sound and complete for packaging magic wands.\<close>
+
+theory PackageLogic
+  imports Main SepAlgebra
+begin
+
+subsection Definitions
+
+type_synonym 'a abool = "'a \<Rightarrow> bool"
+
+datatype 'a aassertion =
+  AStar "'a aassertion" "'a aassertion"
+| AImp "'a abool" "'a aassertion"
+| ASem "'a abool"
+
+locale package_logic = sep_algebra +
+
+  fixes unit :: "'a"
+  fixes stable :: "'a \<Rightarrow> bool"
+
+  assumes unit_neutral: "Some a = a \<oplus> unit"
+      and stable_sum: "stable a \<Longrightarrow> stable b \<Longrightarrow> Some x = a \<oplus> b \<Longrightarrow> stable x"
+      and stable_unit: "stable unit"
+
+begin
+
+fun sat :: "'a aassertion \<Rightarrow> 'a \<Rightarrow> bool" where
+  "sat (AStar A B) \<phi> \<longleftrightarrow> (\<exists>a b. Some \<phi> = a \<oplus> b \<and> sat A a \<and> sat B b)"
+| "sat (AImp b A) \<phi> \<longleftrightarrow> (b \<phi> \<longrightarrow> sat A \<phi>)"
+| "sat (ASem A) \<phi> \<longleftrightarrow> A \<phi>"
+
+definition mono_pure_cond where
+  "mono_pure_cond b \<longleftrightarrow> (\<forall>\<phi>. b \<phi> \<longleftrightarrow> b |\<phi>| ) \<and> (\<forall>\<phi>' \<phi> r. pure r \<and> Some \<phi>' = \<phi> \<oplus> r \<and> \<not> b \<phi> \<longrightarrow> \<not> b \<phi>')"
+
+definition bool_conj where
+  "bool_conj a b x \<longleftrightarrow> a x \<and> b x"
+
+type_synonym 'c pruner = "'c \<Rightarrow> bool"
+
+(* Only positively, so not-well defined = false *)
+definition mono_pruner :: "'a pruner \<Rightarrow> bool" where
+  "mono_pruner p \<longleftrightarrow> (\<forall>\<phi>' \<phi> r. pure r \<and> p \<phi> \<and> Some \<phi>' = \<phi> \<oplus> r \<longrightarrow> p \<phi>')"
+(* opposite of mono_cond *)
+
+fun wf_assertion where
+  "wf_assertion (AStar A B) \<longleftrightarrow> wf_assertion A \<and> wf_assertion B"
+| "wf_assertion (AImp b A) \<longleftrightarrow> mono_pure_cond b \<and> wf_assertion A"
+| "wf_assertion (ASem A) \<longleftrightarrow> mono_pruner A"
+
+type_synonym 'c transformer = "'c \<Rightarrow> 'c"
+
+type_synonym 'c ext_state = "'c \<times> 'c \<times> 'c transformer"
+
+inductive package_rhs ::
+  "'a \<Rightarrow> 'a \<Rightarrow> 'a ext_state set \<Rightarrow> 'a abool \<Rightarrow> 'a aassertion \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a ext_state set \<Rightarrow> bool" where 
+
+  AStar: "\<lbrakk> package_rhs \<phi> f S pc A \<phi>' f' S' ; package_rhs \<phi>' f' S' pc B \<phi>'' f'' S'' \<rbrakk> \<Longrightarrow> package_rhs \<phi> f S pc (AStar A B) \<phi>'' f'' S''"
+| AImp: "package_rhs \<phi> f S (bool_conj pc b) A \<phi>' f' S' \<Longrightarrow> package_rhs \<phi> f S pc (AImp b A) \<phi>' f' S'"
+(* witness means we *choose* how we satisfy B *)
+| ASem: "\<lbrakk> \<And>a u T b. (a, u, T) \<in> S \<Longrightarrow> pc a \<Longrightarrow> b = witness (a, u, T) \<Longrightarrow> a \<succeq> b \<and> B b ;
+  S' = { (a, u, T) |a u T. (a, u, T) \<in> S \<and> \<not> pc a }
+  \<union> { (a \<ominus> b, the (u \<oplus> b), T) |a u T b. (a, u, T) \<in> S \<and> pc a \<and> b = witness (a, u, T) } \<rbrakk>
+  \<Longrightarrow> package_rhs \<phi> f S pc (ASem B) \<phi> f S'"
+
+| AddFromOutside: "\<lbrakk> Some \<phi> = \<phi>' \<oplus> m ; package_rhs \<phi>' f' S' pc A \<phi>'' f'' S'' ; stable m ; Some f' = f \<oplus> m ;
+  S' = { (r, u, T) |a u T r. (a, u, T) \<in> S \<and> Some r = a \<oplus> (T f' \<ominus> T f)  \<and> r ## u } \<rbrakk>
+  \<Longrightarrow> package_rhs \<phi> f S pc A \<phi>'' f'' S''"
+
+
+definition package_sat where
+  "package_sat pc A a' u' u \<longleftrightarrow> (pc |a'| \<longrightarrow> (\<exists>x. Some x = |a'| \<oplus> (u' \<ominus> u ) \<and> sat A x))"
+
+definition package_rhs_connection :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ext_state set \<Rightarrow> 'a abool \<Rightarrow> 'a aassertion \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a ext_state set \<Rightarrow> bool" where
+  "package_rhs_connection \<phi> f S pc A \<phi>' f' S' \<longleftrightarrow> f' \<succeq> f \<and> \<phi> ## f \<and> \<phi> \<oplus> f = \<phi>' \<oplus> f' \<and> stable f' \<and>
+    (\<forall>(a, u, T) \<in> S. \<exists>au. Some au = a \<oplus> u \<and> (au ## (T f' \<ominus> T f) \<longrightarrow>
+      (\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u)))"
+
+definition mono_transformer :: "'a transformer \<Rightarrow> bool" where
+  "mono_transformer T \<longleftrightarrow> (\<forall>\<phi> \<phi>'. \<phi>' \<succeq> \<phi> \<longrightarrow> T \<phi>' \<succeq> T \<phi>) \<and> T unit = unit"
+
+definition valid_package_set where
+  "valid_package_set S f \<longleftrightarrow> (\<forall>(a, u, T) \<in> S. a ## u \<and> |a| \<succeq> |u| \<and> mono_transformer T \<and> a \<succeq> |T f| )"
+
+definition intuitionistic where
+  "intuitionistic A \<longleftrightarrow> (\<forall>\<phi>' \<phi>. \<phi>' \<succeq> \<phi> \<and> A \<phi> \<longrightarrow> A \<phi>')"
+
+definition pure_remains where
+  "pure_remains S \<longleftrightarrow> (\<forall>(a, u, p) \<in> S. pure a)"
+
+definition is_footprint_general :: "'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a aassertion \<Rightarrow> 'a aassertion \<Rightarrow> bool" where
+  "is_footprint_general w R A B \<longleftrightarrow> (\<forall>a b. sat A a \<and> Some b = a \<oplus> R a w \<longrightarrow> sat B b)"
+
+definition is_footprint_standard :: "'a \<Rightarrow> 'a aassertion \<Rightarrow> 'a aassertion \<Rightarrow> bool" where
+  "is_footprint_standard w A B \<longleftrightarrow> (\<forall>a b. sat A a \<and> Some b = a \<oplus> w \<longrightarrow> sat B b)"
+
+
+
+subsection Lemmas
+
+lemma is_footprint_generalI:
+  assumes "\<And>a b. sat A a \<and> Some b = a \<oplus> R a w \<Longrightarrow> sat B b"
+  shows "is_footprint_general w R A B"
+  using assms is_footprint_general_def by blast
+
+lemma is_footprint_standardI:
+  assumes "\<And>a b. sat A a \<and> Some b = a \<oplus> w \<Longrightarrow> sat B b"
+  shows "is_footprint_standard w A B"
+  using assms is_footprint_standard_def by blast
+
+
+lemma mono_pure_condI:
+  assumes "\<And>\<phi>. b \<phi> \<longleftrightarrow> b |\<phi>|"
+      and "\<And>\<phi> \<phi>' r. pure r \<and> Some \<phi>' = \<phi> \<oplus> r \<and> \<not> b \<phi> \<Longrightarrow> \<not> b \<phi>'"
+    shows "mono_pure_cond b"
+  using assms(1) assms(2) mono_pure_cond_def by blast
+
+lemma mono_pure_cond_conj:
+  assumes "mono_pure_cond pc"
+      and "mono_pure_cond b"
+    shows "mono_pure_cond (bool_conj pc b)"
+proof (rule mono_pure_condI)
+  show "\<And>\<phi>. bool_conj pc b \<phi> = bool_conj pc b  |\<phi>|"
+    by (metis assms(1) assms(2) bool_conj_def mono_pure_cond_def)
+  show "\<And>\<phi> \<phi>' r. pure r \<and> Some \<phi>' = \<phi> \<oplus> r \<and> \<not> bool_conj pc b \<phi> \<Longrightarrow> \<not> bool_conj pc b \<phi>'"
+    by (metis assms(1) assms(2) bool_conj_def mono_pure_cond_def)
+qed
+
+lemma bigger_sum:
+  assumes "Some \<phi> = a \<oplus> b"
+      and "\<phi>' \<succeq> \<phi>"
+    shows "\<exists>b'. b' \<succeq> b \<and> Some \<phi>' = a \<oplus> b'"
+proof -
+  obtain r where "Some \<phi>' = \<phi> \<oplus> r"
+    using assms(2) greater_def by blast
+  then obtain b' where "Some b' = b \<oplus> r"
+    by (metis assms(1) asso2 domD domI domIff)
+  then show ?thesis
+    by (metis \<open>Some \<phi>' = \<phi> \<oplus> r\<close> assms(1) asso1 commutative sep_algebra.greater_equiv sep_algebra_axioms)
+qed
+
+lemma wf_assertion_sat_larger_pure:
+  assumes "wf_assertion A"
+      and "sat A \<phi>"
+      and "Some \<phi>' = \<phi> \<oplus> r"
+      and "pure r"
+    shows "sat A \<phi>'"
+  using assms
+proof (induct arbitrary: \<phi> \<phi>' r rule: wf_assertion.induct)
+  case (1 A B)
+  then obtain a b where "Some \<phi> = a \<oplus> b" "sat A a" "sat B b" by (meson sat.simps(1))
+  then obtain b' where "Some b' = b \<oplus> r"
+    by (metis "1.prems"(3) asso2 option.collapse)
+  moreover obtain a' where "Some a' = a \<oplus> r"
+    by (metis "1.prems"(3) \<open>Some \<phi> = a \<oplus> b\<close> asso2 commutative option.collapse)
+  ultimately show ?case
+    using 1
+    by (metis \<open>Some \<phi> = a \<oplus> b\<close> \<open>sat A a\<close> \<open>sat B b\<close> asso1 sat.simps(1) wf_assertion.simps(1))
+next
+  case (2 b A)
+  then show ?case
+    by (metis mono_pure_cond_def sat.simps(2) wf_assertion.simps(2))
+next
+  case (3 A)
+  then show ?case
+    by (metis mono_pruner_def sat.simps(3) wf_assertion.simps(3))
+qed
+
+
+lemma package_satI:
+  assumes "pc |a'| \<Longrightarrow> (\<exists>x. Some x = |a'| \<oplus> (u' \<ominus> u ) \<and> sat A x)"
+  shows "package_sat pc A a' u' u"
+  by (simp add: assms package_sat_def)
+
+
+lemma package_rhs_connection_instantiate:
+  assumes "package_rhs_connection \<phi> f S pc A \<phi>' f' S'"
+      and "(a, u, T) \<in> S"
+  obtains au where "Some au = a \<oplus> u"
+      and "au ## (T f' \<ominus> T f) \<Longrightarrow> \<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u"
+  using assms(1) assms(2) package_rhs_connection_def by fastforce
+
+lemma package_rhs_connectionI:
+  assumes "\<phi> \<oplus> f = \<phi>' \<oplus> f'"
+    and "stable f'"
+    and "\<phi> ## f"
+    and "f' \<succeq> f"
+      and "\<And>a u T. (a, u, T) \<in> S \<Longrightarrow> (\<exists>au. Some au = a \<oplus> u \<and> (au ## (T f' \<ominus> T f) \<longrightarrow>
+      (\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u'\<and> u' \<succeq> u \<and> package_sat pc A a' u' u)))"
+    shows "package_rhs_connection \<phi> f S pc A \<phi>' f' S'"
+  using package_rhs_connection_def assms by auto
+
+lemma valid_package_setI:
+  assumes "\<And>a u T. (a, u, T) \<in> S \<Longrightarrow> a ## u \<and> |a| \<succeq> |u| \<and> mono_transformer T \<and> a \<succeq> |T f| "
+  shows "valid_package_set S f"
+  using assms valid_package_set_def by auto
+
+lemma defined_sum_move:
+  assumes "a ## b"
+      and "Some b = x \<oplus> y"
+      and "Some a' = a \<oplus> x"
+    shows "a' ## y"
+  by (metis assms defined_def sep_algebra.asso1 sep_algebra_axioms)
+
+lemma bigger_core_sum_defined:
+  assumes "|a| \<succeq> b"
+  shows "Some a = a \<oplus> b"
+  by (metis (no_types, lifting) assms asso1 core_is_smaller greater_equiv max_projection_prop_pure_core mpp_prop pure_def pure_smaller)
+
+
+lemma package_rhs_proof:
+  assumes "package_rhs \<phi> f S pc A \<phi>' f' S'"
+      and "valid_package_set S f"
+      and "wf_assertion A"
+      and "mono_pure_cond pc"
+      and "stable f"
+      and "\<phi> ## f"
+    shows "package_rhs_connection \<phi> f S pc A \<phi>' f' S' \<and> valid_package_set S' f'"
+  using assms
+proof (induct rule: package_rhs.induct)
+  case (AImp \<phi> f S pc b A \<phi>' f' S')
+  then have asm0: "package_rhs_connection \<phi> f S (bool_conj pc b) A \<phi>' f' S' \<and> valid_package_set S' f'"
+    using mono_pure_cond_conj wf_assertion.simps(2) by blast
+  let ?pc = "bool_conj pc b"
+  obtain "\<phi> \<oplus> f = \<phi>' \<oplus> f'" "stable f'" "\<phi> ## f" "f' \<succeq> f"
+    and \<section>: "\<And>a u T. (a, u, T) \<in> S \<Longrightarrow> (\<exists>au. Some au = a \<oplus> u \<and> (au ## (T f' \<ominus> T f) \<longrightarrow>
+      (\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat ?pc A a' u' u)))"
+  using asm0 package_rhs_connection_def by force
+
+
+  have "package_rhs_connection \<phi> f S pc (AImp b A) \<phi>' f' S'"
+  proof (rule package_rhs_connectionI)
+    show "\<phi> ## f"
+      by (simp add: \<open>\<phi> ## f\<close>)
+    show "\<phi> \<oplus> f = \<phi>' \<oplus> f'" by (simp add: \<open>\<phi> \<oplus> f = \<phi>' \<oplus> f'\<close>)
+    show "stable f'" using \<open>stable f'\<close> by simp
+    show "f' \<succeq> f" by (simp add: \<open>f' \<succeq> f\<close>)
+    fix a u T assume asm1: "(a, u, T) \<in> S"
+    then obtain au where asm2: "Some au = a \<oplus> u \<and> (au ## (T f' \<ominus> T f) \<longrightarrow>
+      (\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat ?pc A a' u' u))"
+      using \<section> by presburger
+
+    then have "au ## (T f' \<ominus> T f) \<Longrightarrow>
+      (\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc (AImp b A) a' u' u)"
+    proof -
+      assume asm3: "au ## (T f' \<ominus> T f)"
+      then obtain a' u' where au': "(a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat ?pc A a' u' u"
+        using asm2 by blast
+      have "(the ( |a'| \<oplus> (u' \<ominus> u))) \<succeq> |a'|"
+      proof -
+        have "u' \<succeq> u' \<ominus> u"
+          by (metis minus_default minus_smaller succ_refl)
+        then have "a' ## (u' \<ominus> u)"
+          by (metis au' asm3 asso3 defined_def minus_exists)
+        then show ?thesis
+          by (metis core_is_smaller defined_def greater_def option.exhaust_sel sep_algebra.asso2 sep_algebra_axioms)
+      qed
+      have "package_sat pc (AImp b A) a' u' u"
+      proof (rule package_satI)
+        assume "pc |a'|"
+        then show "\<exists>x. Some x = |a'| \<oplus> (u' \<ominus> u) \<and> sat (AImp b A) x"
+        proof (cases "b |a'|")
+          case True
+          then have "?pc |a'|"
+            by (simp add: \<open>pc |a'|\<close> bool_conj_def)
+          then show ?thesis
+            by (metis au' package_logic.package_sat_def package_logic_axioms sat.simps(2))
+        next
+          case False
+          then have "\<not> b (the ( |a'| \<oplus> (u' \<ominus> u)))"
+            using AImp.prems(2) \<open>the ( |a'| \<oplus> (u' \<ominus> u)) \<succeq> |a'|\<close> core_sum max_projection_prop_def max_projection_prop_pure_core minus_exists mono_pure_cond_def wf_assertion.simps(2)
+            by metis
+          moreover obtain x where "Some x = |a'| \<oplus> (u' \<ominus> u)"
+            by (metis au' asm3 asso2 commutative core_is_smaller defined_def minus_and_plus option.collapse)
+          ultimately show ?thesis by (metis option.sel sat.simps(2))
+        qed
+      qed
+      then show "\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc (AImp b A) a' u' u"
+        using au' by blast
+    qed
+    then show "\<exists>au. Some au = a \<oplus> u \<and> (au ## (T f' \<ominus> T f) \<longrightarrow> (\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc (AImp b A) a' u' u))"
+      using asm2 by auto
+  qed
+  then show ?case
+    using \<open>package_rhs_connection \<phi> f S (bool_conj pc b) A \<phi>' f' S' \<and> valid_package_set S' f'\<close> by blast
+next
+  case (AStar \<phi> f S pc A \<phi>' f' S' B \<phi>'' f'' S'')
+  then have r1: "package_rhs_connection \<phi> f S pc A \<phi>' f' S' \<and> valid_package_set S' f'"
+    using wf_assertion.simps(1) by blast
+  moreover have "\<phi>' ## f'" using r1 package_rhs_connection_def[of \<phi> f S pc A \<phi>' f' S'] defined_def
+    by fastforce
+  ultimately have r2: "package_rhs_connection \<phi>' f' S' pc B \<phi>'' f'' S'' \<and> valid_package_set S'' f''"
+    using AStar.hyps(4) AStar.prems(2) AStar.prems(3) package_rhs_connection_def by force
+
+  moreover obtain fa_def: "\<phi> \<oplus> f = \<phi>' \<oplus> f'" "stable f'" "\<phi> ## f" "f' \<succeq> f"
+    and **: "\<And>a u T. (a, u, T) \<in> S \<Longrightarrow> (\<exists>au. Some au = a \<oplus> u \<and> (au ## (T f' \<ominus> T f) \<longrightarrow>
+      (\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u)))"
+  using r1 package_rhs_connection_def by fastforce
+  then obtain fb_def: "\<phi>' \<oplus> f' = \<phi>'' \<oplus> f''" "stable f''" "\<phi>' ## f'" "f'' \<succeq> f'"
+    and "\<And>a u T. (a, u, T) \<in> S' \<Longrightarrow> (\<exists>au. Some au = a \<oplus> u \<and> (au ## (T f'' \<ominus> T f') \<longrightarrow>
+      (\<exists>a' u'. (a', u', T) \<in> S'' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f'' \<ominus> T f') = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc B a' u' u)))"
+    using r2 package_rhs_connection_def by fastforce
+
+
+  moreover have "package_rhs_connection \<phi> f S pc (AStar A B) \<phi>'' f'' S''"
+  proof (rule package_rhs_connectionI)
+    show "\<phi> \<oplus> f = \<phi>'' \<oplus> f''" by (simp add: fa_def(1) fb_def(1))
+    show "stable f''" by (simp add: fb_def(2))
+    show "\<phi> ## f" using fa_def(3) by auto
+    show "f'' \<succeq> f" using fa_def(4) fb_def(4) succ_trans by blast
+
+
+    fix a u T assume asm0: "(a, u, T) \<in> S"
+    then have f_def: "Some (T f'' \<ominus> T f) = (T f'' \<ominus> T f') \<oplus> (T f' \<ominus> T f)"
+    proof -
+      have "mono_transformer T" using valid_package_set_def asm0 \<open>valid_package_set S f\<close> by fastforce
+      then have "T f'' \<succeq> T f'"
+        by (simp add: fb_def(4) mono_transformer_def)
+      moreover have "T f' \<succeq> T f"
+        using \<open>mono_transformer T\<close> fa_def(4) mono_transformer_def by blast
+      ultimately show ?thesis
+        using commutative minus_and_plus minus_equiv_def by presburger
+    qed
+
+    then obtain au where au_def: "Some au = a \<oplus> u"
+      "au ## (T f' \<ominus> T f) \<Longrightarrow> (\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u)"
+      using \<open>\<And>u a T. (a, u, T) \<in> S \<Longrightarrow> \<exists>au. Some au = a \<oplus> u \<and> (au ## T f' \<ominus> T f \<longrightarrow> (\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u))\<close> asm0 by blast
+    then show "\<exists>au. Some au = a \<oplus> u \<and> (au ## (T f'' \<ominus> T f) \<longrightarrow> (\<exists>a' u'. (a', u', T) \<in> S'' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f'' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc (AStar A B) a' u' u))"
+    proof (cases "au ## (T f'' \<ominus> T f)")
+      case True
+      moreover have "mono_transformer T" using \<open>valid_package_set S f\<close> valid_package_set_def asm0 by fastforce
+      ultimately have "au ## (T f'' \<ominus> T f') \<and> au ## (T f' \<ominus> T f)" using asso3 commutative defined_def f_def
+        by metis
+      then obtain a' u' where "(a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u"
+        using au_def(2) by blast
+
+      then obtain au' where au'_def: "Some au' = a' \<oplus> u'"
+        "au' ## (T f'' \<ominus> T f') \<Longrightarrow> (\<exists>a'' u''. (a'', u'', T) \<in> S'' \<and> |a''| \<succeq> |a'| \<and> au' \<oplus> (T f'' \<ominus> T f') = a'' \<oplus> u'' \<and> u'' \<succeq> u' \<and> package_sat pc B a'' u'' u')"
+        using \<open>\<And>u a T. (a, u, T) \<in> S' \<Longrightarrow> \<exists>au. Some au = a \<oplus> u \<and> (au ## T f'' \<ominus> T f' \<longrightarrow> (\<exists>a' u'. (a', u', T) \<in> S'' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f'' \<ominus> T f') = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc B a' u' u))\<close> by blast
+      moreover have "au' ## T f'' \<ominus> T f'"
+        using True \<open>(a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u\<close> calculation(1) commutative defined_sum_move f_def by fastforce
+      ultimately obtain a'' u'' where "(a'', u'', T) \<in> S'' \<and> |a''| \<succeq> |a'| \<and> au' \<oplus> (T f'' \<ominus> T f') = a'' \<oplus> u'' \<and> u'' \<succeq> u' \<and> package_sat pc B a'' u'' u'"
+        by blast
+
+      then have "au \<oplus> (T f'' \<ominus> T f) = a'' \<oplus> u''"
+      proof -
+        have "au \<oplus> (T f'' \<ominus> T f) = splus (Some au) (Some (T f'' \<ominus> T f))"
+          by simp
+        also have "... = splus (Some au) (splus (Some (T f'' \<ominus> T f')) (Some (T f' \<ominus> T f)))"
+          using f_def by auto
+        finally show ?thesis 
+          by (metis (full_types) \<open>(a'', u'', T) \<in> S'' \<and> |a''| \<succeq> |a'| \<and> au' \<oplus> (T f'' \<ominus> T f') = a'' \<oplus> u'' \<and> u'' \<succeq> u' \<and> package_sat pc B a'' u'' u'\<close> \<open>(a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u\<close> au'_def(1) splus.simps(3) splus_asso splus_comm)
+      qed
+      moreover have "package_sat pc (AStar A B) a'' u'' u"
+      proof (rule package_satI)
+        assume "pc |a''|"
+        then have "pc |a'|"
+          by (metis AStar.prems(3) \<open>(a'', u'', T) \<in> S'' \<and> |a''| \<succeq> |a'| \<and> au' \<oplus> (T f'' \<ominus> T f') = a'' \<oplus> u'' \<and> u'' \<succeq> u' \<and> package_sat pc B a'' u'' u'\<close> greater_equiv minus_core minus_core_weaker minus_equiv_def mono_pure_cond_def pure_def)
+        then obtain x where "Some x = |a'| \<oplus> (u' \<ominus> u) \<and> sat A x"
+          using \<open>(a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u\<close> package_sat_def by fastforce
+        then obtain x' where "Some x' = |a''| \<oplus> (u'' \<ominus> u') \<and> sat B x'"
+          using \<open>(a'', u'', T) \<in> S'' \<and> |a''| \<succeq> |a'| \<and> au' \<oplus> (T f'' \<ominus> T f') = a'' \<oplus> u'' \<and> u'' \<succeq> u' \<and> package_sat pc B a'' u'' u'\<close> \<open>pc |a''|\<close> package_sat_def by auto
+        have "u'' \<succeq> u'' \<ominus> u"
+          by (metis minus_default minus_smaller succ_refl)
+        moreover have "a'' ## u''"
+          using True \<open>au \<oplus> (T f'' \<ominus> T f) = a'' \<oplus> u''\<close> defined_def by auto
+        ultimately obtain x'' where "Some x'' = |a''| \<oplus> (u'' \<ominus> u)"
+          by (metis commutative defined_def max_projection_prop_pure_core mpp_smaller not_None_eq smaller_compatible)
+        moreover have "Some (u'' \<ominus> u) = (u'' \<ominus> u') \<oplus> (u' \<ominus> u)"
+          using \<open>(a'', u'', T) \<in> S'' \<and> |a''| \<succeq> |a'| \<and> au' \<oplus> (T f'' \<ominus> T f') = a'' \<oplus> u'' \<and> u'' \<succeq> u' \<and> package_sat pc B a'' u'' u'\<close> \<open>(a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u\<close> commutative minus_and_plus minus_equiv_def by presburger
+        moreover have "|a''| \<succeq> |a'|"
+          using \<open>(a'', u'', T) \<in> S'' \<and> |a''| \<succeq> |a'| \<and> au' \<oplus> (T f'' \<ominus> T f') = a'' \<oplus> u'' \<and> u'' \<succeq> u' \<and> package_sat pc B a'' u'' u'\<close> by blast
+        moreover have "Some |a''| = |a'| \<oplus> |a''|"
+          by (metis (no_types, lifting) calculation(3) core_is_pure sep_algebra.asso1 sep_algebra.minus_exists sep_algebra_axioms)
+        ultimately have "Some x'' = x' \<oplus> x"
+          using asso1[of _ _ x'] \<open>Some x = |a'| \<oplus> (u' \<ominus> u) \<and> sat A x\<close> \<open>Some x' = |a''| \<oplus> (u'' \<ominus> u') \<and> sat B x'\<close>  commutative
+          by metis
+        then show "\<exists>x. Some x = |a''| \<oplus> (u'' \<ominus> u) \<and> sat (AStar A B) x"
+          using \<open>Some x = |a'| \<oplus> (u' \<ominus> u) \<and> sat A x\<close> \<open>Some x' = |a''| \<oplus> (u'' \<ominus> u') \<and> sat B x'\<close> \<open>Some x'' = |a''| \<oplus> (u'' \<ominus> u)\<close> commutative by fastforce
+      qed
+      ultimately show ?thesis
+        using \<open>(a'', u'', T) \<in> S'' \<and> |a''| \<succeq> |a'| \<and> au' \<oplus> (T f'' \<ominus> T f') = a'' \<oplus> u'' \<and> u'' \<succeq> u' \<and> package_sat pc B a'' u'' u'\<close> \<open>(a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u\<close> au_def(1) succ_trans by blast
+    next
+      case False
+      then show ?thesis
+        using au_def(1) by blast
+    qed
+  qed
+  ultimately show ?case by blast
+next
+  case (ASem S pc witness B S' \<phi> f)
+  have "valid_package_set S' f"
+  proof (rule valid_package_setI)
+    fix a' u' T assume asm0: "(a', u', T) \<in> S'"
+    then show "a' ## u' \<and> |a'| \<succeq> |u'| \<and> mono_transformer T \<and> a' \<succeq> |T f|"
+    proof (cases "(a', u', T) \<in> S")
+      case True
+      then show ?thesis
+        using ASem.prems(1) valid_package_set_def by auto
+    next
+      case False
+      then have "(a', u', T) \<in> {(a \<ominus> b, the (u \<oplus> b), T) |a u T b. (a, u, T) \<in> S \<and> pc a \<and> b = witness (a, u, T)}"
+        using ASem.hyps(2) asm0 by blast
+      then obtain a u b where "(a, u, T) \<in> S" "pc a" "b = witness (a, u, T)" "a' = a \<ominus> b" "u' = the (u \<oplus> b)" by blast
+      then have "a \<succeq> b \<and> B b"
+        using ASem.hyps(1) by presburger
+      have "a ## u"
+        using ASem.prems(1) \<open>(a, u, T) \<in> S\<close> valid_package_set_def by fastforce
+      then have "Some u' = u \<oplus> b"
+        by (metis \<open>a \<succeq> b \<and> B b\<close> \<open>u' = the (u \<oplus> b)\<close> commutative defined_def option.exhaust_sel smaller_compatible)
+      moreover have "Some a = a' \<oplus> b"
+        using \<open>a \<succeq> b \<and> B b\<close> \<open>a' = a \<ominus> b\<close> commutative minus_equiv_def by presburger
+
+      ultimately have "a' ## u'"
+        by (metis \<open>a ## u\<close> asso1 commutative defined_def)
+      moreover have "|a'| \<succeq> |u'|"
+      proof -
+        have "|a| \<succeq> |u|"
+          using ASem.prems(1) \<open>(a, u, T) \<in> S\<close> valid_package_set_def by fastforce
+        moreover have "|a'| \<succeq> |a|"
+          by (simp add: \<open>a' = a \<ominus> b\<close> minus_core succ_refl)
+        moreover have "|a'| \<succeq> |b|"
+          using \<open>a \<succeq> b \<and> B b\<close> \<open>a' = a \<ominus> b\<close> max_projection_prop_pure_core minus_core mpp_mono by presburger
+        ultimately show ?thesis
+          by (metis \<open>Some u' = u \<oplus> b\<close> \<open>a' = a \<ominus> b\<close> core_is_pure core_sum minus_core pure_def smaller_pure_sum_smaller)
+      qed
+      moreover have "a' \<succeq> |T f|"
+      proof -
+        have "a \<succeq> |T f|" using \<open>(a, u, T) \<in> S\<close> \<open>valid_package_set S f\<close> valid_package_set_def
+          by fastforce
+        then show ?thesis
+          by (metis \<open>a' = a \<ominus> b\<close> max_projection_prop_pure_core minus_core mpp_mono mpp_smaller sep_algebra.mpp_invo sep_algebra.succ_trans sep_algebra_axioms)
+      qed
+      ultimately show ?thesis using \<open>(a, u, T) \<in> S\<close> \<open>valid_package_set S f\<close> valid_package_set_def 
+        by fastforce
+    qed
+  qed
+  moreover have "package_rhs_connection \<phi> f S pc (ASem B) \<phi> f S'"
+  proof (rule package_rhs_connectionI)
+    show "\<phi> \<oplus> f = \<phi> \<oplus> f"
+      by simp
+    show "stable f" by (simp add: ASem.prems(4))
+    show "\<phi> ## f" by (simp add: ASem.prems(5))
+    show "f \<succeq> f" by (simp add: succ_refl)
+            
+    fix a u T assume asm0: "(a, u, T) \<in> S"
+
+    then obtain au where "Some au = a \<oplus> u" using \<open>valid_package_set S f\<close> valid_package_set_def defined_def by auto
+    then have "(\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> Some au = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc (ASem B) a' u' u)"
+    proof -
+      let ?b = "witness (a, u, T)"
+      let ?a = "a \<ominus> ?b"
+      let ?u = "the (u \<oplus> ?b)"
+      show "\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> Some au = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc (ASem B) a' u' u"
+      proof (cases "pc a")
+        case True
+        then have "(?a, ?u, T) \<in> S'" using ASem.hyps(2) asm0 by blast
+        then have "a \<succeq> ?b \<and> B ?b" using ASem.hyps(1) True asm0 by blast
+        moreover have "(?a, ?u, T) \<in> S' \<and> |?a| \<succeq> |a| \<and> Some au = ?a \<oplus> ?u \<and> ?u \<succeq> u"
+        proof
+          show "(a \<ominus> witness (a, u, T), the (u \<oplus> witness (a, u, T)), T) \<in> S'"
+            by (simp add: \<open>(a \<ominus> witness (a, u, T), the (u \<oplus> witness (a, u, T)), T) \<in> S'\<close>)
+          have "|a \<ominus> witness (a, u, T)|  \<succeq>  |a| "
+            by (simp add: minus_core succ_refl)
+          moreover have "Some au = a \<ominus> witness (a, u, T) \<oplus> the (u \<oplus> witness (a, u, T))"
+            using \<open>Some au = a \<oplus> u\<close> \<open>a \<succeq> witness (a, u, T) \<and> B (witness (a, u, T))\<close>
+              asso1[of "a \<ominus> witness (a, u, T)" "witness (a, u, T)" a u "the (u \<oplus> witness (a, u, T))"]
+              commutative option.distinct(1) option.exhaust_sel asso3 minus_equiv_def
+            by metis
+          moreover have "the (u \<oplus> witness (a, u, T)) \<succeq> u"
+            using \<open>Some au = a \<oplus> u\<close> \<open>a \<succeq> witness (a, u, T) \<and> B (witness (a, u, T))\<close> commutative
+              greater_def option.distinct(1) option.exhaust_sel asso3[of u "witness (a, u, T)" ]
+            by metis
+          ultimately show "|a \<ominus> witness (a, u, T)|  \<succeq>  |a|  \<and> Some au = a \<ominus> witness (a, u, T) \<oplus> the (u \<oplus> witness (a, u, T)) \<and> the (u \<oplus> witness (a, u, T)) \<succeq> u"
+            by blast
+        qed
+        moreover have "package_sat pc (ASem B) ?a ?u u"
+        proof (rule package_satI)
+          assume "pc |a \<ominus> witness (a, u, T)|"
+          have "Some ?u = u \<oplus> ?b"
+            by (metis (no_types, lifting) \<open>Some au = a \<oplus> u\<close> calculation(1) commutative minus_equiv_def option.distinct(1) option.exhaust_sel sep_algebra.asso3 sep_algebra_axioms)
+          moreover have "?a ## ?u"
+            by (metis \<open>(a \<ominus> witness (a, u, T), the (u \<oplus> witness (a, u, T)), T) \<in> S' \<and> |a \<ominus> witness (a, u, T)| \<succeq> |a| \<and> Some au = a \<ominus> witness (a, u, T) \<oplus> the (u \<oplus> witness (a, u, T)) \<and> the (u \<oplus> witness (a, u, T)) \<succeq> u\<close> defined_def option.distinct(1))
+          moreover have "?u \<succeq> ?u \<ominus> u"
+            using \<open>(a \<ominus> witness (a, u, T), the (u \<oplus> witness (a, u, T)), T) \<in> S' \<and> |a \<ominus> witness (a, u, T)| \<succeq> |a| \<and> Some au = a \<ominus> witness (a, u, T) \<oplus> the (u \<oplus> witness (a, u, T)) \<and> the (u \<oplus> witness (a, u, T)) \<succeq> u\<close> minus_smaller by blast
+          ultimately obtain x where "Some x = |a \<ominus> ?b| \<oplus> (?u \<ominus> u)"
+            by (metis (no_types, opaque_lifting) \<open>a \<succeq> witness (a, u, T) \<and> B (witness (a, u, T))\<close> commutative defined_def minus_core minus_equiv_def option.exhaust smaller_compatible)
+          moreover have "x \<succeq> ?b"
+          proof -
+            have "?u \<ominus> u \<succeq> ?b"
+              using \<open>Some (the (u \<oplus> witness (a, u, T))) = u \<oplus> witness (a, u, T)\<close> minus_bigger by blast
+            then show ?thesis
+              using calculation greater_equiv succ_trans by blast
+          qed
+          ultimately show "\<exists>x. Some x = |a \<ominus> witness (a, u, T)| \<oplus> (the (u \<oplus> witness (a, u, T)) \<ominus> u) \<and> sat (ASem B) x"
+            using ASem.prems(2) \<open>Some (the (u \<oplus> witness (a, u, T))) = u \<oplus> witness (a, u, T)\<close>
+              \<open>a \<succeq> witness (a, u, T) \<and> B (witness (a, u, T))\<close> commutative max_projection_prop_def[of pure core]
+              max_projection_prop_pure_core minus_equiv_def_any_elem mono_pruner_def[of B]
+              sat.simps(3)[of B] wf_assertion.simps(3)[of B]
+            by metis
+        qed
+        ultimately show ?thesis by blast
+      next
+        case False
+        then have "package_sat pc (ASem B) a u u"
+          by (metis ASem.prems(3) mono_pure_cond_def package_sat_def)
+        moreover have "(a, u, T) \<in> S'" 
+          using False ASem.hyps(2) asm0 by blast
+        ultimately show ?thesis
+          using \<open>Some au = a \<oplus> u\<close> succ_refl by blast
+      qed
+    qed
+    moreover have "au \<oplus> (T f \<ominus> T f) = Some au"
+    proof -
+      have "a \<succeq> |T f|" using \<open>(a, u, T) \<in> S\<close> \<open>valid_package_set S f\<close> valid_package_set_def by fastforce
+      then have "|a| \<succeq> T f \<ominus> T f"
+        using core_is_smaller max_projection_prop_def max_projection_prop_pure_core minusI by presburger
+      then have "|au| \<succeq> T f \<ominus> T f"
+        using \<open>Some au = a \<oplus> u\<close> core_sum greater_def succ_trans by blast
+      then show ?thesis using bigger_core_sum_defined by force
+    qed
+    ultimately show "\<exists>au. Some au = a \<oplus> u \<and> (au ## (T f \<ominus> T f) \<longrightarrow> (\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc (ASem B) a' u' u))"
+      using \<open>Some au = a \<oplus> u\<close> by fastforce
+  qed
+  ultimately show ?case by blast
+next
+  case (AddFromOutside \<phi> \<phi>' m f' S' pc A \<phi>'' f'' S'' f S)
+  have "valid_package_set S' f'"
+  proof (rule valid_package_setI)
+    fix a' u T assume asm0: "(a', u, T) \<in> S'"
+    then obtain a where "(a, u, T) \<in> S" "a' ## u" "Some a' = a \<oplus> (T f' \<ominus> T f)"
+      using AddFromOutside.hyps(6) by blast
+    then have "|a| \<succeq> |u| \<and> mono_transformer T \<and> a \<succeq> |T f|" using \<open>valid_package_set S f\<close> valid_package_set_def 
+      by fastforce
+    moreover have "a' \<succeq> |T f'|"
+      by (metis (no_types, opaque_lifting) \<open>Some a' = a \<oplus> (T f' \<ominus> T f)\<close> commutative greater_equiv minus_core minus_equiv_def minus_smaller succ_trans unit_neutral)
+    ultimately show "a' ## u \<and> |a'| \<succeq> |u| \<and> mono_transformer T \<and> a' \<succeq> |T f'|"
+      using \<open>Some a' = a \<oplus> (T f' \<ominus> T f)\<close> \<open>a' ## u\<close> greater_def max_projection_prop_pure_core mpp_mono succ_trans by blast
+  qed
+  then have r: "package_rhs_connection \<phi>' f' S' pc A \<phi>'' f'' S'' \<and> valid_package_set S'' f''"
+    by (metis AddFromOutside.hyps(1) AddFromOutside.hyps(3) AddFromOutside.hyps(4) AddFromOutside.hyps(5) AddFromOutside.prems(2) AddFromOutside.prems(3) AddFromOutside.prems(4) AddFromOutside.prems(5) asso1 commutative defined_def stable_sum)
+  then obtain r2: "\<phi>' \<oplus> f' = \<phi>'' \<oplus> f''" "stable f''" "\<phi>' ## f'" "f'' \<succeq> f'"
+    "\<And>a u T. (a, u, T) \<in> S' \<Longrightarrow> (\<exists>au. Some au = a \<oplus> u \<and> (au ## (T f'' \<ominus> T f') \<longrightarrow>
+      (\<exists>a' u'. (a', u', T) \<in> S'' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f'' \<ominus> T f') = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u)))"
+    using package_rhs_connection_def by fastforce
+
+  moreover have "package_rhs_connection \<phi> f S pc A \<phi>'' f'' S''"
+  proof (rule package_rhs_connectionI)
+    show "\<phi> \<oplus> f = \<phi>'' \<oplus> f''"
+      by (metis AddFromOutside.hyps(1) AddFromOutside.hyps(5) asso1 commutative r2(1))
+    show "stable f''"
+      using AddFromOutside.hyps(4) calculation(4) r2(2) stable_sum by blast
+    show "\<phi> ## f"
+      by (simp add: AddFromOutside.prems(5))
+    show "f'' \<succeq> f"
+      using AddFromOutside.hyps(5) bigger_sum greater_def r2(4) by blast
+
+    fix a u T
+    assume asm0: "(a, u, T) \<in> S"
+    then obtain au where "Some au = a \<oplus> u" using \<open>valid_package_set S f\<close> valid_package_set_def defined_def
+      by fastforce
+    moreover have "au ## (T f'' \<ominus> T f) \<Longrightarrow> (\<exists>a' u'. (a', u', T) \<in> S'' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f'' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u)"
+    proof -
+      assume asm1: "au ## (T f'' \<ominus> T f)"
+      moreover have "mono_transformer T" using \<open>valid_package_set S f\<close> valid_package_set_def asm0
+        by fastforce
+      then have "Some (T f'' \<ominus> T f) = (T f'' \<ominus> T f') \<oplus> (T f' \<ominus> T f)"
+        by (metis AddFromOutside.hyps(5) commutative greater_equiv minus_and_plus minus_equiv_def mono_transformer_def r2(4))
+      ultimately have "a ## (T f' \<ominus> T f)"
+        using \<open>Some au = a \<oplus> u\<close> asso2 commutative defined_def minus_exists
+        by metis
+      then obtain a' where "Some a' = a \<oplus> (T f' \<ominus> T f)"
+        by (meson defined_def option.collapse)
+      moreover have "a' ## u"
+      proof -
+        have "T f'' \<ominus> T f \<succeq> T f' \<ominus> T f"
+          using \<open>Some (T f'' \<ominus> T f) = T f'' \<ominus> T f' \<oplus> (T f' \<ominus> T f)\<close> greater_equiv by blast
+        then show ?thesis
+          using \<open>Some au = a \<oplus> u\<close> asm1 asso1[of u a au "T f' \<ominus> T f" a'] asso2[of ] calculation commutative
+            defined_def[of ] greater_equiv[of "T f'' \<ominus> T f" "T f' \<ominus> T f"]
+          by metis
+      qed
+
+      ultimately have "(a', u, T) \<in> S'"
+        using AddFromOutside.hyps(6) asm0 by blast
+
+      moreover have "au ## (T f'' \<ominus> T f')"
+        by (metis \<open>Some (T f'' \<ominus> T f) = T f'' \<ominus> T f' \<oplus> (T f' \<ominus> T f)\<close> asm1 asso3 defined_def)
+
+      then have "\<exists>au. Some au = a' \<oplus> u \<and> (au ## (T f'' \<ominus> T f') \<longrightarrow> (\<exists>a'a u'. (a'a, u', T) \<in> S'' \<and> |a'a| \<succeq> |a'| \<and> au \<oplus> (T f'' \<ominus> T f') = a'a \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a'a u' u))"
+        using r2(5) calculation by blast
+
+      then obtain au' a'' u' where r3: "Some au' = a' \<oplus> u" "au' ## (T f'' \<ominus> T f') \<Longrightarrow> (a'', u', T) \<in> S'' \<and> |a''| \<succeq> |a'| \<and> au' \<oplus> (T f'' \<ominus> T f') = a'' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a'' u' u"
+        using \<open>au ## (T f'' \<ominus> T f')\<close> by blast
+      moreover have "au' ## (T f'' \<ominus> T f')" using \<open>au ## (T f'' \<ominus> T f)\<close> \<open>Some au = a \<oplus> u\<close> r3(1)
+      \<open>Some (T f'' \<ominus> T f) = (T f'' \<ominus> T f') \<oplus> (T f' \<ominus> T f)\<close>
+        \<open>Some a' = a \<oplus> (T f' \<ominus> T f)\<close> asso1[of u a au "T f' \<ominus> T f" a'] commutative defined_sum_move[of au "T f'' \<ominus> T f"]
+        by metis
+      ultimately have r4: "(a'', u', T) \<in> S'' \<and> |a''| \<succeq> |a'| \<and> au' \<oplus> (T f'' \<ominus> T f') = a'' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a'' u' u"
+        by blast
+      moreover have "|a''| \<succeq> |a|"
+      proof -
+        have "|a'| \<succeq> |a|"
+          using \<open>Some a' = a \<oplus> (T f' \<ominus> T f)\<close> core_sum greater_def by blast
+        then show ?thesis
+          using r4 succ_trans by blast
+      qed
+      ultimately show "\<exists>a' u'. (a', u', T) \<in> S'' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f'' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u"        
+        using \<open>Some (T f'' \<ominus> T f) = T f'' \<ominus> T f' \<oplus> (T f' \<ominus> T f)\<close> \<open>Some a' = a \<oplus> (T f' \<ominus> T f)\<close> \<open>Some au = a \<oplus> u\<close>
+          commutative r3(1) asso1 splus.simps(3) splus_asso by metis
+    qed
+    ultimately show "\<exists>au. Some au = a \<oplus> u \<and> (au ## (T f'' \<ominus> T f) \<longrightarrow> (\<exists>a' u'. (a', u', T) \<in> S'' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f'' \<ominus> T f) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat pc A a' u' u))"
+      by blast
+  qed
+  ultimately show ?case using r by blast
+qed
+
+lemma unit_core:
+  "|unit| = unit"
+  by (meson core_is_pure max_projection_prop_pure_core sep_algebra.cancellative sep_algebra.mpp_invo sep_algebra_axioms unit_neutral)
+
+lemma unit_smaller:
+  "\<phi> \<succeq> unit"
+  using greater_equiv unit_neutral by auto
+
+
+subsection \<open>Lemmas for completeness\<close>
+
+lemma sat_star_exists_bigger:
+  assumes "sat (AStar A B) \<phi>"
+      and "wf_assertion A"
+      and "wf_assertion B"
+  shows "\<exists>a b. |a| \<succeq> |\<phi>| \<and> |b| \<succeq> |\<phi>| \<and> Some \<phi> = a \<oplus> b \<and> sat A a \<and> sat B b"
+proof -
+  obtain a b where "Some \<phi> = a \<oplus> b \<and> sat A a \<and> sat B b"
+    using assms sat.simps(1) by blast
+  then obtain a' b' where "Some a' = a \<oplus> |\<phi>|" "Some b' = b \<oplus> |\<phi>|"
+    by (meson defined_def greater_def greater_equiv option.collapse smaller_compatible_core)
+  then have "a' \<succeq> a \<and> b' \<succeq> b"
+    using greater_def by blast
+  then have "sat A a' \<and> sat B b'"
+    using \<open>Some \<phi> = a \<oplus> b \<and> sat A a \<and> sat B b\<close> \<open>Some a' = a \<oplus> |\<phi>|\<close> \<open>Some b' = b \<oplus> |\<phi>|\<close> assms(2) assms(3) core_is_pure pure_def wf_assertion_sat_larger_pure by blast
+  moreover have "Some \<phi> = a' \<oplus> b'"
+    by (metis (no_types, lifting) \<open>Some \<phi> = a \<oplus> b \<and> sat A a \<and> sat B b\<close> \<open>Some a' = a \<oplus> |\<phi>|\<close> \<open>Some b' = b \<oplus> |\<phi>|\<close> asso1 commutative core_is_smaller)
+  ultimately show ?thesis
+    by (metis \<open>Some \<phi> = a \<oplus> b \<and> sat A a \<and> sat B b\<close> \<open>Some a' = a \<oplus> |\<phi>|\<close> \<open>Some b' = b \<oplus> |\<phi>|\<close> commutative greater_def smaller_than_core succ_refl)
+qed
+
+lemma let_pair_instantiate:
+  assumes "(a, b) = f x y"
+  shows "(let (a, b) = f x y in g a b) = g a b"
+  by (metis assms case_prod_conv)
+
+
+lemma greater_than_sum_exists:
+  assumes "a \<succeq> b"
+      and "Some b = b1 \<oplus> b2"
+    shows "\<exists>r. Some a = r \<oplus> b2 \<and> |r| \<succeq> |a| \<and> r \<succeq> b1"
+proof -
+  obtain r where "Some a = r \<oplus> b2 \<and> r \<succeq> b1"
+    by (metis assms(1) assms(2) bigger_sum commutative)
+  then obtain r' where "Some r' = r \<oplus> |a|"
+    by (metis defined_def greater_def option.exhaust smaller_compatible_core)
+  then have "Some a = r' \<oplus> b2"
+    by (metis \<open>Some a = r \<oplus> b2 \<and> r \<succeq> b1\<close> commutative core_is_smaller sep_algebra.asso1 sep_algebra_axioms)
+  then show ?thesis
+    by (metis \<open>Some a = r \<oplus> b2 \<and> r \<succeq> b1\<close> \<open>Some r' = r \<oplus> |a|\<close> core_is_pure greater_def smaller_than_core succ_trans)
+qed
+
+lemma bigger_the:
+  assumes "Some a = x' \<oplus> y"
+      and "x' \<succeq> x"
+    shows "the (   |a|  \<oplus>  x') \<succeq> the (   |a|  \<oplus> x)"
+proof -
+  have "a \<succeq> x'"
+    using assms(1) greater_def by blast
+  then have "|a|  ##  x'"
+    using commutative defined_def smaller_compatible_core by auto
+  moreover have "|a|  ## x"
+    by (metis assms(2) calculation defined_def sep_algebra.asso3 sep_algebra.minus_exists sep_algebra_axioms)
+  ultimately show ?thesis
+    using addition_bigger assms(2) commutative defined_def by force
+qed
+
+lemma wf_assertion_and_the:
+  assumes "|a| ## b"
+      and "sat A b"
+      and "wf_assertion A"
+    shows "sat A (the ( |a| \<oplus> b))"
+  by (metis assms(1) assms(2) assms(3) commutative defined_def max_projection_prop_pure_core option.collapse sep_algebra.mpp_prop sep_algebra_axioms wf_assertion_sat_larger_pure)
+
+lemma minus_some:
+  assumes "a \<succeq> b"
+  shows "Some a = b \<oplus> (a \<ominus> b)"
+  using assms commutative minus_equiv_def by force
+
+lemma core_mono:
+  assumes "a \<succeq> b"
+  shows "|a| \<succeq> |b|"
+  using assms max_projection_prop_pure_core mpp_mono by auto
+
+lemma prove_last_completeness:
+  assumes "a' \<succeq> a"
+      and "Some a = nf1 \<oplus> f2"
+    shows "a' \<ominus> nf1 \<succeq> f2"
+  by (meson assms(1) assms(2) greater_def greater_minus_trans minus_bigger succ_trans)
+
+lemma completeness_aux:
+  assumes "\<And>a u T. (a, u, T) \<in> S \<Longrightarrow> |f1 a u T| \<succeq> |a| \<and> Some a = f1 a u T \<oplus> f2 a u T \<and> (pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> (f1 a u T))))"
+      and "valid_package_set S f"
+      and "wf_assertion A"
+      and "mono_pure_cond pc"
+      and "stable f \<and> \<phi> ## f"
+    shows "\<exists>S'. package_rhs \<phi> f S pc A \<phi> f S' \<and> (\<forall>(a', u', T) \<in> S'. \<exists>a u. (a, u, T) \<in> S \<and> a' \<succeq> f2 a u T \<and> |a'| = |a| )"
+  using assms
+proof (induct A arbitrary: S pc f1 f2)
+  case (AImp b A)
+  let ?pc = "bool_conj pc b"
+
+  have "\<exists>S'. package_rhs \<phi> f S (bool_conj pc b) A \<phi> f S' \<and> (\<forall>a\<in>S'. case a of (a', u', T) \<Rightarrow> \<exists>a u. (a, u, T) \<in> S \<and> a' \<succeq> f2 a u T \<and> |a'| = |a| )"
+  proof (rule AImp(1))
+    show "valid_package_set S f"
+      by (simp add: AImp.prems(2))
+    show "wf_assertion A" using AImp.prems(3) by auto
+    show "mono_pure_cond (bool_conj pc b)"
+      by (meson AImp.prems(3) AImp.prems(4) mono_pure_cond_conj wf_assertion.simps(2))
+    show "stable f \<and> \<phi> ## f" using \<open>stable f \<and> \<phi> ## f\<close> by simp
+
+    fix a u T
+    assume asm0: "(a, u, T) \<in> S" 
+    then have "Some a = f1 a u T \<oplus> f2 a u T"
+      using AImp.prems(1) by blast
+    moreover have "bool_conj pc b |a| \<Longrightarrow> sat A (the ( |a| \<oplus> f1 a u T))"
+    proof -
+      assume "bool_conj pc b |a|"
+      then have "pc |a|"
+        by (meson bool_conj_def)
+      then have "|f1 a u T| \<succeq> |a| \<and> Some a = f1 a u T \<oplus> f2 a u T \<and> sat (AImp b A) (the ( |a| \<oplus> f1 a u T))"
+        using AImp.prems(1) asm0(1) by blast
+      moreover have "b (the ( |a| \<oplus> f1 a u T))"
+      proof -
+        have "|a| ## f1 a u T \<and> |a| \<succeq> |f1 a u T|"
+          by (metis calculation commutative core_is_smaller defined_def greater_def max_projection_prop_pure_core mpp_mono option.discI succ_antisym)
+        then obtain x where "Some x = |a| \<oplus> f1 a u T"
+          by (meson defined_def option.collapse)
+        then have "|x| = |a|"
+          by (metis \<open>Some x = |a| \<oplus> f1 a u T\<close> \<open>|a| ## f1 a u T \<and> |a| \<succeq> |f1 a u T|\<close> commutative core_is_pure core_sum max_projection_prop_pure_core mpp_smaller smaller_than_core)
+        then show ?thesis
+          by (metis AImp.prems(3) \<open>Some x = |a| \<oplus> f1 a u T\<close> \<open>bool_conj pc b |a|\<close> bool_conj_def mono_pure_cond_def option.sel wf_assertion.simps(2))
+      qed
+      ultimately show "sat A (the ( |a| \<oplus> f1 a u T))" by (metis sat.simps(2))
+    qed
+    ultimately show "|f1 a u T| \<succeq> |a| \<and> Some a = f1 a u T \<oplus> f2 a u T \<and> (bool_conj pc b |a| \<longrightarrow> sat A (the ( |a| \<oplus> f1 a u T)))" 
+      by (metis AImp.prems(1) asm0)
+  qed
+  then obtain S' where r: "package_rhs \<phi> f S (bool_conj pc b) A \<phi> f S'" "\<And>a' u' T. (a', u', T) \<in> S' \<Longrightarrow> (\<exists>a u. (a, u, T) \<in> S \<and> a' \<succeq> f2 a u T)"
+    by fast
+  moreover have "package_rhs \<phi> f S pc (AImp b A) \<phi> f S'"
+    by (simp add: package_rhs.AImp r(1))
+  ultimately show ?case
+    using \<open>\<exists>S'. package_rhs \<phi> f S (bool_conj pc b) A \<phi> f S' \<and> (\<forall>a\<in>S'. case a of (a', u', T) \<Rightarrow> \<exists>a u. (a, u, T) \<in> S \<and> a' \<succeq> f2 a u T \<and> |a'| = |a| )\<close> package_rhs.AImp by blast
+next
+  case (ASem A)
+  let ?witness = "\<lambda>(a, u, T). the ( |a| \<oplus> f1 a u T)"
+
+  obtain S' where S'_def: "S' = { (a, u, T) |a u T. (a, u, T) \<in> S \<and> \<not> pc a }
+  \<union> { (a \<ominus> b, the (u \<oplus> b), T) |a u T b. (a, u, T) \<in> S \<and> pc a \<and> b = ?witness (a, u, T) }"
+    by blast
+
+  have "package_rhs \<phi> f S pc (ASem A) \<phi> f S'"
+  proof (rule package_rhs.ASem)
+    show "S' = {(a, u, T) |a u T. (a, u, T) \<in> S \<and> \<not> pc a} \<union> {(a \<ominus> b, the (u \<oplus> b), T) |a u T b. (a, u, T) \<in> S \<and> pc a \<and> b = ?witness (a, u, T)}"
+      using S'_def by blast
+    fix a u T b
+    assume asm0: "(a, u, T) \<in> S" "pc a" "b = (case (a, u, T) of (a, u, T) \<Rightarrow> the ( |a| \<oplus> f1 a u T))"
+    then have "b = the ( |a| \<oplus> f1 a u T)" by fastforce
+    moreover have "pc |a|"
+      by (meson ASem.prems(4) asm0(2) mono_pure_cond_def)
+    then have "|f1 a u T| \<succeq> |a| \<and> Some a = f1 a u T \<oplus> f2 a u T \<and> sat (ASem A) (the ( |a| \<oplus> f1 a u T))"
+      using ASem.prems(1) asm0(1) by blast
+    then have "Some b = |a| \<oplus> f1 a u T" by (metis calculation commutative defined_def minus_bigger minus_core option.exhaust_sel smaller_compatible_core)
+    moreover have "a \<succeq> b"
+    proof -
+      have "a \<succeq> f1 a u T"
+        using \<open>|f1 a u T| \<succeq> |a| \<and> Some a = f1 a u T \<oplus> f2 a u T \<and> sat (ASem A) (the ( |a| \<oplus> f1 a u T))\<close> asso1 calculation(2) commutative core_is_smaller greater_def by metis
+      then show ?thesis
+        by (metis calculation(2) commutative max_projection_prop_pure_core mpp_smaller sep_algebra.mpp_prop sep_algebra_axioms smaller_pure_sum_smaller)
+    qed
+    ultimately show "a \<succeq> b \<and> A b"
+      using \<open>|f1 a u T| \<succeq> |a| \<and> Some a = f1 a u T \<oplus> f2 a u T \<and> sat (ASem A) (the ( |a| \<oplus> f1 a u T))\<close> commutative greater_def max_projection_prop_def max_projection_prop_pure_core sat.simps(3) smaller_pure_sum_smaller
+      by metis
+  qed
+
+  moreover have "\<And>a' u' T. (a', u', T) \<in> S' \<Longrightarrow> (\<exists>a u. (a, u, T) \<in> S \<and> a' \<succeq> f2 a u T \<and> |a'| = |a| )"
+  proof -
+    fix a' u' T assume asm0: "(a', u', T) \<in> S'"
+    then show "\<exists>a u. (a, u, T) \<in> S \<and> a' \<succeq> f2 a u T \<and> |a'| = |a| "
+    proof (cases "(a', u', T) \<in> {(a, u, T) |a u T. (a, u, T) \<in> S \<and> \<not> pc a}")
+      case True
+      then show ?thesis using ASem.prems(1) greater_equiv by fastforce
+    next
+      case False
+      then have "(a', u', T) \<in> { (a \<ominus> b, the (u \<oplus> b), T) |a u T b. (a, u, T) \<in> S \<and> pc a \<and> b = ?witness (a, u, T) }"
+        using S'_def asm0 by blast
+      then obtain a u b where "a' = a \<ominus> b" "u' = the (u \<oplus> b)" "(a, u, T) \<in> S" "pc a" "b = ?witness (a, u, T)"
+        by blast
+      then have "a' \<succeq> f2 a u T"
+      proof -
+        have "a \<succeq> b"
+        proof -
+          have "a \<succeq> f1 a u T"
+            using ASem.prems(1) \<open>(a, u, T) \<in> S\<close> greater_def by blast
+          moreover have "Some b = |a| \<oplus> f1 a u T"
+            by (metis \<open>b = (case (a, u, T) of (a, u, T) \<Rightarrow> the ( |a| \<oplus> f1 a u T))\<close> calculation case_prod_conv commutative defined_def option.exhaust_sel smaller_compatible_core)
+          ultimately show ?thesis
+            by (metis commutative max_projection_prop_pure_core mpp_smaller sep_algebra.mpp_prop sep_algebra_axioms smaller_pure_sum_smaller)
+        qed
+        then show ?thesis
+          using ASem.prems(1)[of a u T]
+            \<open>(a, u, T) \<in> S\<close> \<open>a' = a \<ominus> b\<close> \<open>b = (case (a, u, T) of (a, u, T) \<Rightarrow> the ( |a| \<oplus> f1 a u T))\<close>
+            commutative core_is_smaller minus_bigger option.exhaust_sel option.simps(3)
+            asso1[of "f2 a u T" "f1 a u T" a "|a|" "the ( |a|  \<oplus> f1 a u T)"] asso2[of "f2 a u T" "f1 a u T"]
+            split_conv
+          by metis
+      qed
+      then show ?thesis
+        using \<open>(a, u, T) \<in> S\<close> \<open>a' = a \<ominus> b\<close> minus_core by blast
+    qed
+  qed
+
+  ultimately show ?case by blast
+next
+  case (AStar A B)
+
+  let ?fA = "\<lambda>a u T. SOME x. \<exists>y. Some (f1 a u T) = x \<oplus> y \<and> |x| \<succeq> |f1 a u T| \<and> |y| \<succeq> |a| \<and> (pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> x)) \<and> sat B (the ( |a| \<oplus> y)))"
+  let ?fB = "\<lambda>a u T. SOME y. Some (f1 a u T) = ?fA a u T \<oplus> y \<and> |y| \<succeq> |a| \<and> (pc |a| \<longrightarrow> sat B (the ( |a| \<oplus> y)))"
+  let ?f2 = "\<lambda>a u T. the (?fB a u T \<oplus> f2 a u T)"
+
+  have r: "\<And>a u T. (a, u, T) \<in> S \<Longrightarrow> Some (f1 a u T) = ?fA a u T \<oplus> ?fB a u T \<and> |?fA a u T| \<succeq> |f1 a u T| \<and> |?fB a u T| \<succeq> |a| \<and> (pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> ?fA a u T)) \<and> sat B (the ( |a| \<oplus> ?fB a u T)))
+  \<and> Some (?f2 a u T) = ?fB a u T \<oplus> f2 a u T"
+  proof -
+    fix a u T assume asm0: "(a, u, T) \<in> S"
+    then have "Some a = f1 a u T \<oplus> f2 a u T \<and> (pc |a| \<longrightarrow> sat (AStar A B) (the ( |a| \<oplus> f1 a u T)))"
+      using AStar.prems(1) by blast
+    then have "\<exists>x y. Some (the ( |a| \<oplus> f1 a u T )) = x \<oplus> y \<and> (pc |a| \<longrightarrow> sat A x) \<and> (pc |a| \<longrightarrow> sat B y) \<and>
+      x \<succeq> |(the ( |a| \<oplus> f1 a u T))| \<and> y \<succeq> |(the ( |a| \<oplus> f1 a u T))|"
+    proof (cases "pc |a|")
+      case True
+      then show ?thesis
+        using AStar.prems(3) \<open>Some a = f1 a u T \<oplus> f2 a u T \<and> (pc |a| \<longrightarrow> sat (AStar A B) (the ( |a| \<oplus> f1 a u T)))\<close>
+          max_projection_prop_def[of pure core] max_projection_prop_pure_core
+          sat_star_exists_bigger[of A B "(the ( |a|  \<oplus> f1 a u T))"]
+          succ_trans[of ] wf_assertion.simps(1)[of A B]
+        by blast
+    next
+      case False
+      then have "Some (the ( |a| \<oplus> f1 a u T )) = the ( |a| \<oplus> f1 a u T) \<oplus> |the ( |a| \<oplus> f1 a u T )|"
+        by (simp add: core_is_smaller)
+      then show ?thesis by (metis False max_projection_prop_pure_core mpp_smaller succ_refl)
+    qed
+    then obtain x y where "Some (the ( |a| \<oplus> f1 a u T)) = x \<oplus> y" "pc |a| \<longrightarrow> sat A x" "pc |a| \<longrightarrow> sat B y"
+      "x \<succeq> |(the ( |a| \<oplus> f1 a u T))|" "y \<succeq> |(the ( |a| \<oplus> f1 a u T))|" by blast
+    moreover obtain af where "Some af = |a| \<oplus> f1 a u T"
+      by (metis \<open>Some a = f1 a u T \<oplus> f2 a u T \<and> (pc |a| \<longrightarrow> sat (AStar A B) (the ( |a| \<oplus> f1 a u T)))\<close> commutative defined_def minus_bigger minus_core option.exhaust_sel smaller_compatible_core)
+    ultimately have "Some (f1 a u T) = x \<oplus> y"
+      by (metis AStar.prems(1) \<open>Some a = f1 a u T \<oplus> f2 a u T \<and> (pc |a| \<longrightarrow> sat (AStar A B) (the ( |a| \<oplus> f1 a u T)))\<close> asm0 commutative core_is_smaller greater_def max_projection_prop_pure_core mpp_mono option.sel succ_antisym)
+    moreover have "|a| ## x \<and> |a| ## y"
+      by (metis \<open>Some af = |a| \<oplus> f1 a u T\<close> calculation commutative defined_def option.discI sep_algebra.asso3 sep_algebra_axioms)
+    then have "the ( |a| \<oplus> x) \<succeq> x \<and> the ( |a| \<oplus> y) \<succeq> y"
+      using commutative defined_def greater_def by auto
+
+    ultimately have "pc |a| \<Longrightarrow> sat A (the ( |a| \<oplus> x)) \<and> sat B (the ( |a| \<oplus> y))"
+      by (metis AStar.prems(3) \<open>pc |a| \<longrightarrow> sat A x\<close> \<open>pc |a| \<longrightarrow> sat B y\<close> \<open>|a| ## x \<and> |a| ## y\<close> commutative defined_def max_projection_prop_pure_core option.exhaust_sel package_logic.wf_assertion.simps(1) package_logic_axioms sep_algebra.mpp_prop sep_algebra_axioms wf_assertion_sat_larger_pure)
+
+    have "\<exists>y. Some (f1 a u T) = ?fA a u T \<oplus> y \<and> |?fA a u T| \<succeq> |f1 a u T| \<and> |y| \<succeq> |a| \<and> (pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> ?fA a u T)) \<and> sat B (the ( |a| \<oplus> y)))"
+    proof (rule someI_ex)
+      show "\<exists>x y. Some (f1 a u T) = x \<oplus> y \<and> |x| \<succeq> |f1 a u T| \<and> |y| \<succeq> |a| \<and> (pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> x)) \<and> sat B (the ( |a| \<oplus> y)))"
+        using \<open>Some (f1 a u T) = x \<oplus> y\<close> \<open>Some (the ( |a| \<oplus> f1 a u T)) = x \<oplus> y\<close> \<open>pc |a| \<Longrightarrow> sat A (the ( |a| \<oplus> x)) \<and> sat B (the ( |a| \<oplus> y))\<close> \<open>x \<succeq> |the ( |a| \<oplus> f1 a u T)|\<close> \<open>y \<succeq> |the ( |a| \<oplus> f1 a u T)|\<close> core_is_pure max_projection_propE(3) max_projection_prop_pure_core option.sel pure_def
+        by (metis AStar.prems(1) asm0 minusI minus_core)
+    qed
+    then obtain yy where "Some (f1 a u T) = ?fA a u T \<oplus> yy \<and> |?fA a u T| \<succeq> |f1 a u T| \<and> |yy| \<succeq> |a| \<and> (pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> ?fA a u T)) \<and> sat B (the ( |a| \<oplus> yy)))"
+      by blast
+    moreover have "Some (f1 a u T) = ?fA a u T \<oplus> ?fB a u T \<and> |?fB a u T| \<succeq> |a| \<and> (pc |a| \<longrightarrow> sat B (the ( |a| \<oplus> ?fB a u T)))"
+    proof (rule someI_ex)
+      show "\<exists>y. Some (f1 a u T) = ?fA a u T \<oplus> y \<and> |y| \<succeq> |a| \<and> (pc |a| \<longrightarrow> sat B (the ( |a| \<oplus> y)))"
+        using \<open>\<exists>y. Some (f1 a u T) = ?fA a u T \<oplus> y \<and> |?fA a u T| \<succeq> |f1 a u T| \<and> |y| \<succeq> |a| \<and> (pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> ?fA a u T)) \<and> sat B (the ( |a| \<oplus> y)))\<close>
+        by blast
+    qed
+    ultimately have "?fB a u T \<oplus> f2 a u T \<noteq> None"
+      using \<open>Some a = f1 a u T \<oplus> f2 a u T \<and> (pc |a| \<longrightarrow> sat (AStar A B) (the ( |a| \<oplus> f1 a u T)))\<close>
+        option.distinct(1) [of ] option.exhaust_sel[of "?fB a u T \<oplus> f2 a u T"] asso2[of "?fA a u T" "?fB a u T" "f1 a u T" "f2 a u T"]
+      by metis
+    then show "Some (f1 a u T) = ?fA a u T \<oplus> ?fB a u T \<and> |?fA a u T| \<succeq> |f1 a u T| \<and> |?fB a u T| \<succeq> |a| \<and> (pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> ?fA a u T)) \<and> sat B (the ( |a| \<oplus> ?fB a u T)))
+\<and> Some (?f2 a u T) = ?fB a u T \<oplus> f2 a u T"
+      using \<open>Some a = f1 a u T \<oplus> f2 a u T \<and> (pc |a| \<longrightarrow> sat (AStar A B) (the ( |a| \<oplus> f1 a u T)))\<close>
+ option.distinct(1) option.exhaust_sel[of "?fB a u T \<oplus> f2 a u T"] asso2[of "?fA a u T" "?fB a u T" "f1 a u T" "f2 a u T"]
+\<open>Some (f1 a u T) = ?fA a u T \<oplus> ?fB a u T \<and> |?fB a u T| \<succeq> |a| \<and> (pc |a| \<longrightarrow> sat B (the ( |a| \<oplus> ?fB a u T)))\<close>
+\<open>Some (f1 a u T) = ?fA a u T \<oplus> yy \<and> |?fA a u T| \<succeq> |f1 a u T| \<and> |yy| \<succeq> |a| \<and> (pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> ?fA a u T)) \<and> sat B (the ( |a| \<oplus> yy)))\<close>
+      by simp
+  qed
+  have ih1: "\<exists>S'. package_rhs \<phi> f S pc A \<phi> f S' \<and> (\<forall>a\<in>S'. case a of (a', u', T) \<Rightarrow> \<exists>a u. (a, u, T) \<in> S \<and> a' \<succeq> ?f2 a u T \<and> |a'| = |a| )"
+  proof (rule AStar(1))
+    show "valid_package_set S f"
+      by (simp add: AStar.prems(2))
+    show "wf_assertion A"
+      using AStar.prems(3) by auto
+    show "mono_pure_cond pc"
+      by (simp add: AStar.prems(4))
+    show "stable f \<and> \<phi> ## f" using \<open>stable f \<and> \<phi> ## f\<close> by simp
+
+    fix a u T
+    assume asm0: "(a, u, T) \<in> S"
+    then have b: "Some (f1 a u T) = ?fA a u T \<oplus> ?fB a u T \<and> |?fA a u T| \<succeq> |f1 a u T| \<and> |?fB a u T| \<succeq> |a| \<and> (pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> ?fA a u T)) \<and> sat B (the ( |a| \<oplus> ?fB a u T)))"
+      using r by fast
+    show "|?fA a u T| \<succeq> |a| \<and> Some a = ?fA a u T \<oplus> ?f2 a u T \<and> (pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> ?fA a u T)))"
+    proof -
+      have "|?fA a u T| \<succeq> |a|"
+      using AStar.prems(1)[of a u T] asm0 b asso1[of "?fA a u T" "?fB a u T" "f1 a u T" ]
+        asso2[of "?fA a u T" "?fB a u T" ] option.sel succ_trans[of "|?fA a u T|" _ "|a|"]
+        by blast
+      moreover have "Some a = ?fA a u T \<oplus> ?f2 a u T"
+        using AStar.prems(1)[of a u T] asm0 b asso1[of "?fA a u T" "?fB a u T" "f1 a u T" "f2 a u T" "?f2 a u T"]
+          asso2[of "?fA a u T" "?fB a u T" "f1 a u T" "f2 a u T"] option.sel
+  option.exhaust_sel[of "?fB a u T \<oplus> f2 a u T" "Some a = ?fA a u T \<oplus> ?f2 a u T"]
+        by force
+      moreover have "pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> ?fA a u T))"
+        using AStar.prems(1)[of a u T] asm0 b
+          asso2[of "?fA a u T" "?fB a u T" ] option.sel succ_trans[of "|?fA a u T|" _ "|a|"]
+        by blast
+      ultimately show ?thesis
+        by blast
+    qed
+  qed
+  then obtain S' where r': "package_rhs \<phi> f S pc A \<phi> f S'" "\<And>a' u' T. (a', u', T) \<in> S' \<Longrightarrow> \<exists>a u. (a, u, T) \<in> S \<and> a' \<succeq> ?f2 a u T  \<and> |a'| = |a| "
+    by fast
+
+  let ?project = "\<lambda>a' T. (SOME r. \<exists>a u. r = (a, u) \<and> (a, u, T) \<in> S \<and> a' \<succeq> ?f2 a u T \<and> |a'| = |a| )"
+  have project_prop: "\<And>a' u' T. (a', u', T) \<in> S' \<Longrightarrow> \<exists>a u. ?project a' T = (a, u) \<and> (a, u, T) \<in> S \<and> a' \<succeq> ?f2 a u T  \<and> |a'| = |a| "
+  proof -
+    fix a' u' T assume "(a', u', T) \<in> S'"
+    then obtain a u where "(a, u, T) \<in> S \<and> a' \<succeq> ?f2 a u T  \<and> |a'| = |a| "
+      using \<open>\<And>a' u' p. (a', u', T) \<in> S' \<Longrightarrow> \<exists>a u. (a, u, T) \<in> S \<and> a' \<succeq> ?f2 a u T \<and> |a'| = |a| \<close> by blast
+    show "\<exists>a u. ?project a' T = (a, u) \<and> (a, u, T) \<in> S \<and> a' \<succeq> ?f2 a u T \<and> |a'| = |a| "
+    proof (rule someI_ex)
+      show "\<exists>r a u. r = (a, u) \<and> (a, u, T) \<in> S \<and> a' \<succeq> ?f2 a u T \<and> |a'| = |a| " using \<open>(a, u, T) \<in> S \<and> a' \<succeq> ?f2 a u T \<and> |a'| = |a| \<close> by blast
+    qed
+  qed
+
+  let ?nf1 = "\<lambda>a' u' T. let (a, u) = ?project a' T in (SOME r. Some r = |a'| \<oplus> ?fB a u T)"
+  let ?nf2 = "\<lambda>a' u' T. a' \<ominus> ?nf1 a' u' T"
+
+  have "\<exists>S''. package_rhs \<phi> f S' pc B \<phi> f S'' \<and> (\<forall>a\<in>S''. case a of (a', u', T) \<Rightarrow> \<exists>a u. (a, u, T) \<in> S' \<and> a' \<succeq> ?nf2 a u T \<and> |a'| = |a| )"
+  proof (rule AStar(2))
+    show "stable f \<and> \<phi> ## f" using \<open>stable f \<and> \<phi> ## f\<close> by simp
+
+    then show "valid_package_set S' f"
+      using AStar.prems \<open>package_rhs \<phi> f S pc A \<phi> f S'\<close> package_logic.package_rhs_proof package_logic.wf_assertion.simps(1) package_logic_axioms
+      by metis
+    show "wf_assertion B"
+      using AStar.prems(3) by auto
+    show "mono_pure_cond pc"
+      by (simp add: AStar.prems(4))
+    fix a' u' T assume "(a', u', T) \<in> S'"
+    then obtain a u where a_u_def: "(a, u) = ?project a' T" "(a, u, T) \<in> S" "a' \<succeq> ?f2 a u T" "|a'| = |a|"
+      using project_prop by force
+    define nf1 where "nf1 = ?nf1 a' u' T"
+    define nf2 where "nf2 = ?nf2 a' u' T"
+    moreover have rnf1_def: "Some nf1 = |a'| \<oplus> ?fB a u T"
+    proof -
+      let ?x = "(SOME r. Some r = |a'| \<oplus> ?fB a u T )"
+      have "Some ?x = |a'| \<oplus> ?fB a u T"
+      proof (rule someI_ex)
+        have "Some (f1 a u T) = ?fA a u T \<oplus> ?fB a u T \<and> |?fA a u T| \<succeq> |f1 a u T| \<and> |?fB a u T| \<succeq> |a|
+          \<and> (pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> ?fA a u T)) \<and> sat B (the ( |a| \<oplus> ?fB a u T)))"
+          using r a_u_def by blast
+        then have "Some (?f2 a u T) = ?fB a u T \<oplus> f2 a u T"
+          by (metis (no_types, lifting) AStar.prems(1) a_u_def(2) asso2 option.distinct(1) option.exhaust_sel)
+        moreover have "a' \<succeq> (?f2 a u T)" using \<open>a' \<succeq> ?f2 a u T\<close> by blast
+        ultimately have "a' \<succeq> ?fB a u T" using succ_trans greater_def
+          by blast
+        then obtain r where "Some r = |a'| \<oplus> ?fB a u T"
+          using
+           commutative
+           greater_equiv[of a' "?fB a u T"]
+           minus_equiv_def_any_elem[of a']
+          by fastforce
+        then show "\<exists>r. Some r = |a'| \<oplus> ?fB a u T" by blast
+      qed
+      moreover have "?nf1 a' u' T = ?x"
+        using let_pair_instantiate[of a u _ a' T "\<lambda>a u. (SOME r. Some r = |a'| \<oplus> ?fB a u T )"] a_u_def
+        by fast
+      ultimately show ?thesis using nf1_def by argo
+    qed
+
+    moreover have rnf2_def: "Some a' = nf1 \<oplus> nf2"
+    proof -
+      have "nf2 = a' \<ominus> nf1" using nf1_def nf2_def by blast
+      moreover have "a' \<succeq> nf1"
+      proof -
+        have "?f2 a u T \<succeq> nf1"
+        proof -
+          have "Some (?f2 a u T) = ?fB a u T \<oplus> f2 a u T" using r \<open>(a, u, T) \<in> S\<close> by blast
+          then have "?f2 a u T \<succeq> ?fB a u T"
+            using greater_def by blast
+          moreover have "?f2 a u T \<succeq> |a'|"
+          proof -
+            have "|?f2 a u T| \<succeq> |a|"
+            proof -
+              have "|?f2 a u T| \<succeq> |?fB a u T|" using \<open>?f2 a u T \<succeq> ?fB a u T\<close> core_mono by blast
+              moreover have "|?fB a u T| \<succeq> |a|" using r \<open>(a, u, T) \<in> S\<close> by blast
+              ultimately show ?thesis using succ_trans \<open>|a'| = |a|\<close> by blast
+            qed
+            then show ?thesis
+              using a_u_def(4)
+                bigger_core_sum_defined[of "?f2 a u T"]
+                greater_equiv[of _ "|a|"]
+              by auto
+          qed
+          ultimately show ?thesis using
+              core_is_pure[of a'] commutative pure_def[of "|a'|"] smaller_pure_sum_smaller[of _ _ "|a'|"] rnf1_def
+            by (metis (no_types, lifting))
+        qed
+        then show ?thesis using \<open>a' \<succeq> ?f2 a u T\<close> succ_trans by blast
+      qed
+      ultimately show ?thesis using minus_some nf2_def by blast
+    qed
+
+    moreover have "pc  |a'| \<Longrightarrow> sat B (the ( |a'|  \<oplus> ?nf1 a' u' T))"
+    proof -
+      assume "pc  |a'|"
+      moreover have "|a'| = |a|"
+        by (simp add: a_u_def(4))
+      then have "pc |a|" using \<open>pc  |a'|\<close> by simp
+      ultimately have "sat B (the ( |a| \<oplus> ?fB a u T))"
+        using r a_u_def by blast
+      then have "sat B (the ( |a'| \<oplus> ?fB a u T))" using \<open>|a'| = |a|\<close> by simp
+
+      then show "sat B (the ( |a'|  \<oplus> ?nf1 a' u' T))"
+      proof -
+        have "nf1 \<succeq> |a'|" using rnf1_def
+          using greater_def by blast
+        then have "Some nf1 = |a'| \<oplus> nf1"
+          by (metis bigger_core_sum_defined commutative core_mono max_projection_prop_pure_core mpp_invo)
+        then show ?thesis using nf1_def rnf1_def \<open>sat B (the ( |a'| \<oplus> ?fB a u T))\<close> by argo
+      qed
+    qed
+    moreover have "|?nf1 a' u' T|  \<succeq>  |a'|"
+    proof -
+      have "?nf1 a' u' T \<succeq> |a'|" using nf1_def greater_def rnf1_def by blast
+      then show ?thesis
+        using max_projection_propE(3) max_projection_prop_pure_core sep_algebra.mpp_prop sep_algebra_axioms by fastforce
+    qed
+    ultimately show "|?nf1 a' u' T|  \<succeq>  |a'|  \<and> Some a' = ?nf1 a' u' T \<oplus> ?nf2 a' u' T \<and> (pc  |a'|  \<longrightarrow> sat B (the ( |a'|  \<oplus> ?nf1 a' u' T)))"
+      using nf1_def
+      by blast
+  qed
+
+  then obtain S'' where "package_rhs \<phi> f S' pc B \<phi> f S''" "\<And>a' u' T. (a', u', T) \<in> S'' \<Longrightarrow> \<exists>a u. (a, u, T) \<in> S' \<and> a' \<succeq> ?nf2 a u T  \<and> |a'| = |a| "
+    by fast
+
+  then have "package_rhs \<phi> f S pc (AStar A B) \<phi> f S''"
+    using \<open>package_rhs \<phi> f S pc A \<phi> f S'\<close> package_rhs.AStar by presburger
+  moreover have "\<And>a'' u'' T. (a'', u'', T) \<in> S'' \<Longrightarrow> \<exists>a u. (a, u, T) \<in> S \<and> a'' \<succeq> f2 a u T  \<and> |a''| = |a|"
+  proof -
+    fix a'' u'' T assume asm0: "(a'', u'', T) \<in> S''"
+
+    
+    then obtain a' u' where "(a', u', T) \<in> S' \<and> a'' \<succeq> ?nf2 a' u' T  \<and> |a''| = |a'| "
+      using \<open>\<And>a' u' p. (a', u', T) \<in> S'' \<Longrightarrow> \<exists>a u. (a, u, T) \<in> S' \<and> a' \<succeq> ?nf2 a u T \<and> |a'| = |a| \<close> by blast
+
+    then obtain a u where a_u_def: "(a, u) = ?project a' T" "(a, u, T) \<in> S" "a' \<succeq> ?f2 a u T" "|a'| = |a|"
+      using project_prop by force
+
+    define nf1 where "nf1 = ?nf1 a' u' T"
+    define nf2 where "nf2 = ?nf2 a' u' T"
+
+    moreover have rnf1_def: "Some nf1 = |a'| \<oplus> ?fB a u T"
+    proof -
+      let ?x = "(SOME r. Some r = |a'| \<oplus> ?fB a u T )"
+      have "Some ?x = |a'| \<oplus> ?fB a u T"
+      proof (rule someI_ex)
+        have "Some (f1 a u T) = ?fA a u T \<oplus> ?fB a u T \<and> |?fA a u T| \<succeq> |f1 a u T| \<and> |?fB a u T| \<succeq> |a|
+          \<and> (pc |a| \<longrightarrow> sat A (the ( |a| \<oplus> ?fA a u T)) \<and> sat B (the ( |a| \<oplus> ?fB a u T)))"
+          using r a_u_def by blast
+        then have "Some (?f2 a u T) = ?fB a u T \<oplus> f2 a u T"
+          by (metis (no_types, lifting) AStar.prems(1) a_u_def(2) asso2 option.distinct(1) option.exhaust_sel)
+        moreover have "a' \<succeq> (?f2 a u T)" using \<open>a' \<succeq> ?f2 a u T\<close> by blast
+        ultimately have "a' \<succeq> ?fB a u T" using succ_trans greater_def
+          by blast
+        then obtain r where "Some r = |a'| \<oplus> ?fB a u T"
+          using commutative greater_equiv[of a' "?fB a u T"] minus_equiv_def_any_elem[of a' ] by fastforce
+        then show "\<exists>r. Some r = |a'| \<oplus> ?fB a u T" by blast
+      qed
+      moreover have "?nf1 a' u' T = ?x"
+        using let_pair_instantiate[of a u _ a' T "\<lambda>a u. (SOME r. Some r = |a'| \<oplus> ?fB a u T )"] a_u_def
+        by fast
+      ultimately show ?thesis using nf1_def by argo
+    qed
+
+    moreover have rnf2_def: "a' \<succeq> nf1 \<and> ?nf2 a' u' T \<succeq> f2 a u T"
+    proof -
+      have "nf2 = a' \<ominus> nf1" using nf1_def nf2_def by blast
+      moreover have "a' \<succeq> nf1 \<and> a' \<ominus> nf1 \<succeq> f2 a u T"
+      proof -
+        have "?f2 a u T \<succeq> nf1"
+        proof -
+          have "Some (?f2 a u T) = ?fB a u T \<oplus> f2 a u T" using r \<open>(a, u, T) \<in> S\<close> by blast
+          then have "?f2 a u T \<succeq> ?fB a u T"
+            using greater_def by blast
+          moreover have "?f2 a u T \<succeq> |a'|"
+          proof -
+            have "|?f2 a u T| \<succeq> |a|"
+            proof -
+              have "|?f2 a u T| \<succeq> |?fB a u T|" using \<open>?f2 a u T \<succeq> ?fB a u T\<close> core_mono by blast
+              moreover have "|?fB a u T| \<succeq> |a|" using r \<open>(a, u, T) \<in> S\<close> by blast
+              ultimately show ?thesis using succ_trans \<open>|a'| = |a|\<close> by blast
+            qed
+            then show ?thesis
+              using a_u_def(4)
+                bigger_core_sum_defined
+                greater_equiv[of "?f2 a u T" "|a'|"]
+              by auto
+          qed
+          ultimately show ?thesis using 
+              core_is_pure[of "a'"] commutative pure_def[of "|a'|"] smaller_pure_sum_smaller[of "?f2 a u T" _ "|a'|"] rnf1_def
+            by simp
+        qed
+        then have r1: "a' \<succeq> nf1" using \<open>a' \<succeq> ?f2 a u T\<close> succ_trans by blast
+        then have "Some a' = nf1 \<oplus> nf2" using minus_some nf2_def \<open>nf2 = a' \<ominus> nf1\<close> by presburger
+        have r2: "a' \<ominus> nf1 \<succeq> f2 a u T"
+          using \<open>a' \<succeq> ?f2 a u T\<close>
+        proof (rule prove_last_completeness)
+
+          have "Some (?f2 a u T) = ?fB a u T \<oplus> f2 a u T"
+            using r \<open>(a, u, T) \<in> S\<close> by blast
+          moreover have "Some nf1 = |a'| \<oplus> ?fB a u T" using rnf1_def by blast
+
+          have "Some (?f2 a u T) = ?fB a u T \<oplus> f2 a u T" using r \<open>(a, u, T) \<in> S\<close> by blast
+          then have "?f2 a u T \<succeq> ?fB a u T"
+            using greater_def by blast
+          moreover have "?f2 a u T \<succeq> |a'|"
+          proof -
+            have "|?f2 a u T| \<succeq> |a|"
+            proof -
+              have "|?f2 a u T| \<succeq> |?fB a u T|" using \<open>?f2 a u T \<succeq> ?fB a u T\<close> core_mono by blast
+              moreover have "|?fB a u T| \<succeq> |a|" using r \<open>(a, u, T) \<in> S\<close> by blast
+              ultimately show ?thesis using succ_trans \<open>|a'| = |a|\<close> by blast
+            qed
+            then show ?thesis
+              using a_u_def(4)
+                bigger_core_sum_defined[of _ "|a|"]
+                greater_equiv[of "?f2 a u T" "|a|"]
+              by auto
+          qed
+          ultimately show "Some (?f2 a u T) = nf1 \<oplus> f2 a u T"
+            using asso1[of "|a'|" "?fB a u T" nf1 "f2 a u T" "?f2 a u T"]
+            asso1[of "|a'|" "|a'|" "|a'|" ] core_is_pure[of "a'"] greater_def[of "?f2 a u T" "|a'|"] rnf1_def
+            by (metis (no_types, lifting))
+        qed
+        then show ?thesis using \<open>a' \<succeq> ?f2 a u T\<close> succ_trans using r1 by force
+      qed
+      ultimately show ?thesis  using nf2_def by argo
+    qed
+    ultimately have "(a, u, T) \<in> S \<and> a' \<succeq> ?f2 a u T \<and> ?nf2 a' u' T \<succeq> f2 a u T" using nf1_def nf2_def
+        a_u_def by blast
+    then have "a'' \<succeq> f2 a u T \<and>  |a''| = |a'| " using \<open>(a', u', T) \<in> S' \<and> a'' \<succeq> ?nf2 a' u' T \<and> |a''| = |a'| \<close>
+      using succ_trans by blast
+    then show "\<exists>a u. (a, u, T) \<in> S \<and> a'' \<succeq> f2 a u T  \<and> |a''| = |a| " using r'
+      using a_u_def(2) a_u_def(4) by auto
+  qed
+  ultimately show ?case by blast
+qed
+
+
+
+
+
+
+subsection Soundness
+
+theorem general_soundness:
+  assumes "package_rhs \<phi> unit { (a, unit, T) |a T. (a, T) \<in> S } (\<lambda>_. True) A \<phi>' f S'"
+      and "\<And>a T. (a, T) \<in> S \<Longrightarrow> mono_transformer T"
+      and "wf_assertion A"
+      and "intuitionistic (sat A) \<or> pure_remains S'"
+    shows "Some \<phi> = \<phi>' \<oplus> f \<and> stable f \<and> (\<forall>(a, T) \<in> S. a ## T f \<longrightarrow> sat A (the (a \<oplus> T f)))"
+proof -
+  let ?S = "{ (a, unit, p) |a p. (a, p) \<in> S }"
+  let ?pc = "\<lambda>_. True"
+  have "package_rhs_connection \<phi> unit ?S ?pc A \<phi>' f S' \<and> valid_package_set S' f"
+  proof (rule package_rhs_proof)
+    show "package_rhs \<phi> unit {(a, unit, p) |a p. (a, p) \<in> S} (\<lambda>_. True) A \<phi>' f S'"
+      using assms(1) by auto
+    show "valid_package_set {(a, unit, p) |a p. (a, p) \<in> S} unit"
+    proof (rule valid_package_setI)
+      fix a u T
+      assume "(a, u, T) \<in> {(a, unit, p) |a p. (a, p) \<in> S}"
+      then have "u = unit" by blast
+      moreover have "|T unit| = unit"
+        using \<open>(a, u, T) \<in> {(a, unit, p) |a p. (a, p) \<in> S}\<close> assms(2) mono_transformer_def unit_core by fastforce
+      then show "a ## u \<and> |a| \<succeq> |u| \<and> mono_transformer T \<and> a \<succeq>  |T unit|"
+        using \<open>(a, u, T) \<in> {(a, unit, p) |a p. (a, p) \<in> S}\<close> assms(2) defined_def unit_core unit_neutral unit_smaller by auto
+    qed
+    show "wf_assertion A" by (simp add: assms(3))
+    show "mono_pure_cond (\<lambda>_. True)"
+      using mono_pure_cond_def by auto
+    show "stable unit" by (simp add: stable_unit)
+    show "\<phi> ## unit"
+      using defined_def unit_neutral by auto
+  qed
+
+  then obtain r: "\<phi> \<oplus> unit = \<phi>' \<oplus> f" "stable f"
+    "\<And>a u T. (a, u, T) \<in> ?S \<Longrightarrow> (\<exists>au. Some au = a \<oplus> u \<and> (au ## (T f \<ominus> T unit) \<longrightarrow>
+      (\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> (T f \<ominus> T unit) = a' \<oplus> u' \<and> u' \<succeq> u \<and> package_sat ?pc A a' u' u)))"
+    using package_rhs_connection_def by force
+
+  moreover have "\<And>a T x. (a, T) \<in> S \<and> Some x = a \<oplus> T f \<Longrightarrow> sat A x"
+  proof -
+    fix a T x assume asm0: "(a, T) \<in> S \<and> Some x = a \<oplus> T f"
+    then have "T f \<ominus> T unit = T f"
+      by (metis assms(2) commutative minus_equiv_def mono_transformer_def option.sel unit_neutral unit_smaller)
+    then obtain au where "Some au = a \<oplus> unit \<and> (au ## T f \<longrightarrow>
+      (\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> T f = a' \<oplus> u' \<and> u' \<succeq> unit \<and> package_sat ?pc A a' u' unit))"
+      using r asm0 by fastforce
+    then have "au = a" by (metis option.inject unit_neutral)
+    then have "(\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> a \<oplus> T f = a' \<oplus> u' \<and> package_sat ?pc A a' u' unit)"
+      using \<open>Some au = a \<oplus> unit \<and> (au ## T f \<longrightarrow> (\<exists>a' u'. (a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> au \<oplus> T f = a' \<oplus> u' \<and> u' \<succeq> unit \<and> package_sat (\<lambda>_. True) A a' u' unit))\<close> asm0 defined_def       
+      by auto
+    then obtain a' u' where "(a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> a \<oplus> T f = a' \<oplus> u' \<and> package_sat ?pc A a' u' unit"
+      by presburger
+    then obtain y where "Some y = |a'| \<oplus> (u' \<ominus> unit) \<and> sat A y"
+      using package_sat_def by auto
+    then have "Some y =  |a'| \<oplus> u'"
+      by (metis commutative minus_equiv_def splus.simps(3) unit_neutral unit_smaller)
+    then have "x \<succeq> y"
+      by (metis \<open>(a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> a \<oplus> T f = a' \<oplus> u' \<and> package_sat (\<lambda>_. True) A a' u' unit\<close> addition_bigger asm0 max_projection_prop_pure_core mpp_smaller)
+    then show "sat A x"
+    proof (cases "intuitionistic (sat A)")
+      case True
+      then show ?thesis by (meson \<open>Some y = |a'| \<oplus> (u' \<ominus> unit) \<and> sat A y\<close> \<open>x \<succeq> y\<close> intuitionistic_def)
+    next
+      case False
+      then have "pure_remains S'" using assms(4) by auto
+      then have "pure a'" using pure_remains_def \<open>(a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> a \<oplus> T f = a' \<oplus> u' \<and> package_sat (\<lambda>_. True) A a' u' unit\<close>
+        by fast
+      then show ?thesis using \<open>(a', u', T) \<in> S' \<and> |a'| \<succeq> |a| \<and> a \<oplus> T f = a' \<oplus> u' \<and> package_sat (\<lambda>_. True) A a' u' unit\<close>
+          \<open>Some y = |a'| \<oplus> (u' \<ominus> unit) \<and> sat A y\<close> \<open>Some y = |a'| \<oplus> u'\<close> asm0 core_is_smaller
+          core_max option.sel pure_def asso1[of a']
+        by metis
+    qed
+  qed
+  then have "(\<forall>(a, T) \<in> S. a ## T f \<longrightarrow> sat A (the (a \<oplus> T f)))"
+    using sep_algebra.defined_def sep_algebra_axioms by fastforce
+  moreover have "Some \<phi> = \<phi>' \<oplus> f \<and> stable f"
+    using r(1) r(2) unit_neutral by auto
+  ultimately show ?thesis by blast
+qed
+
+theorem soundness:
+  assumes "wf_assertion B"
+      and "\<And>a. sat A a \<Longrightarrow> a \<in> S"
+      and "\<And>a. a \<in> S \<Longrightarrow> mono_transformer (R a)"
+      and "package_rhs \<sigma> unit { (a, unit, R a) |a. a \<in> S } (\<lambda>_. True) B \<sigma>' w S'"
+      and "intuitionistic (sat B) \<or> pure_remains S'"
+    shows "stable w \<and> Some \<sigma> = \<sigma>' \<oplus> w \<and> is_footprint_general w R A B"
+proof -
+  let ?S = "{ (a, R a) |a. a \<in> S} "
+  have r: "Some \<sigma> = \<sigma>' \<oplus> w \<and> stable w \<and> (\<forall>(a, T)\<in>{(a, R a) |a. a \<in> S}. a ## T w \<longrightarrow> sat B (the (a \<oplus> T w)))"
+  proof (rule general_soundness)
+    show "package_rhs \<sigma> unit {(a, unit, T) |a T. (a, T) \<in> {(a, R a) |a. a \<in> S}} (\<lambda>_. True) B \<sigma>' w S'"
+      using assms(4) by auto
+    show "\<And>a T. (a, T) \<in> {(a, R a) |a. a \<in> S} \<Longrightarrow> mono_transformer T" using assms(3) by blast
+    show "wf_assertion B" by (simp add: assms(1))
+    show "intuitionistic (sat B) \<or> pure_remains S'" by (simp add: assms(5))
+  qed
+  moreover have "is_footprint_general w R A B"
+  proof (rule is_footprint_generalI)
+    fix a b assume asm: "sat A a \<and> Some b = a \<oplus> R a w"
+    then have "(a, R a) \<in> ?S"
+      using assms(2) by blast
+    then have "sat B (the (a \<oplus> R a w))" using r using asm defined_def by fastforce
+    then show "sat B b" by (metis asm option.sel)
+  qed
+  ultimately show ?thesis by blast
+qed
+
+corollary soundness_paper:
+  assumes "wf_assertion B"
+      and "\<And>a. sat A a \<Longrightarrow> a \<in> S"
+      and "package_rhs \<sigma> unit { (a, unit, id) |a. a \<in> S } (\<lambda>_. True) B \<sigma>' w S'"
+      and "intuitionistic (sat B) \<or> pure_remains S'"
+    shows "stable w \<and> Some \<sigma> = \<sigma>' \<oplus> w \<and> is_footprint_standard w A B"
+proof -
+  have "stable w \<and> Some \<sigma> = \<sigma>' \<oplus> w \<and> is_footprint_general w (\<lambda>_. id) A B"
+    using assms soundness[of B A S "\<lambda>_. id" \<sigma> \<sigma>' w S']
+    by (simp add: mono_transformer_def)
+  then show ?thesis
+    using is_footprint_general_def is_footprint_standardI by fastforce
+qed
+
+
+
+subsection Completeness
+
+theorem general_completeness:
+  assumes "\<And>a u T x. (a, u, T) \<in> S \<Longrightarrow> Some x = a \<oplus> T f \<Longrightarrow> sat A x"
+      and "Some \<phi> = \<phi>' \<oplus> f"
+      and "stable f"
+      and "valid_package_set S unit"
+      and "wf_assertion A"
+    shows "\<exists>S'. package_rhs \<phi> unit S (\<lambda>_. True) A \<phi>' f S'"
+proof -
+  define S' where "S' = { (r, u, T) |a u T r. (a, u, T) \<in> S \<and> Some r = a \<oplus> (T f \<ominus> T unit) \<and> r ## u }"
+  let ?pc = "\<lambda>_. True"
+  have "\<exists>S''. package_rhs \<phi>' f S' ?pc A \<phi>' f S''"
+  proof -
+    let ?f2 = "\<lambda>a u T. unit"
+    let ?f1 = "\<lambda>a u T. a"
+    have "\<exists>S''. package_rhs \<phi>' f S' ?pc A \<phi>' f S'' \<and> (\<forall>(a', u', T) \<in> S''. \<exists>a u. (a, u, T) \<in> S' \<and> a' \<succeq> ?f2 a u T \<and> |a'| = |a| )"
+    proof (rule completeness_aux)
+      show "mono_pure_cond (\<lambda>_. True)" by (simp add: mono_pure_cond_def)
+      show "wf_assertion A" by (simp add: assms(5))
+      show "valid_package_set S' f"
+      proof (rule valid_package_setI)
+        fix a' u' T
+        assume "(a', u', T) \<in> S'"
+        then obtain a where asm: "(a, u', T) \<in> S \<and> Some a' = a \<oplus> (T f \<ominus> T unit) \<and> a' ## u'"
+          using S'_def by blast
+        then have "a ## u' \<and>  |a|  \<succeq>  |u'|  \<and> mono_transformer T "
+          using assms(4) valid_package_set_def by fastforce
+        moreover have "|T f \<ominus> T unit| = |T f|"
+          by (simp add: minus_core)
+        ultimately show "a' ## u' \<and>  |a'|  \<succeq>  |u'|  \<and> mono_transformer T \<and> a' \<succeq>  |T f| "
+          by (meson asm core_sum greater_def greater_equiv minus_equiv_def mono_transformer_def succ_trans unit_neutral)
+      qed
+      show "stable f \<and> \<phi>' ## f"
+        by (metis assms(2) assms(3) defined_def domI domIff)
+      fix a u T
+      assume "(a, u, T) \<in> S'"
+      then obtain a' u' where "(a', u', T) \<in> S" "Some a = a' \<oplus> (T f \<ominus> T unit)" using S'_def by blast
+      moreover have "T f \<ominus> T unit = T f"
+      proof -
+        have "mono_transformer T" using \<open>valid_package_set S unit\<close> valid_package_set_def \<open>(a', u', T) \<in> S\<close> by auto
+        then show ?thesis
+          by (metis commutative minus_default minus_equiv_def mono_transformer_def option.sel unit_neutral)
+      qed
+
+      then have "sat A (the ( |a|  \<oplus> a))"
+        by (metis assms(1) calculation(1) calculation(2) commutative core_is_smaller option.sel)
+      then show "|a|  \<succeq>  |a|  \<and> Some a = a \<oplus> unit \<and> (True \<longrightarrow> sat A (the ( |a|  \<oplus> a)))"
+        by (simp add: succ_refl unit_neutral)
+    qed
+    then show ?thesis by auto
+  qed
+  then obtain S'' where "package_rhs \<phi>' f S' ?pc A \<phi>' f S''" by blast
+  have "package_rhs \<phi> unit S ?pc A \<phi>' f S''"
+    using assms(2)
+  proof (rule package_rhs.AddFromOutside)
+    show "package_rhs \<phi>' f S' ?pc A \<phi>' f S''"
+      by (simp add: \<open>package_rhs \<phi>' f S' ?pc A \<phi>' f S''\<close>)
+    show "stable f" using assms(3) by simp
+    show "Some f = unit \<oplus> f"
+      by (simp add: commutative unit_neutral)
+    show "S' = { (r, u, T) |a u T r. (a, u, T) \<in> S \<and> Some r = a \<oplus> (T f \<ominus> T unit) \<and> r ## u }"
+      using S'_def by blast
+  qed
+  then show ?thesis
+    by blast
+qed
+
+theorem completeness:
+  assumes "wf_assertion B"
+      and "stable w \<and> is_footprint_general w R A B"
+      and "Some \<sigma> = \<sigma>' \<oplus> w"
+      and "\<And>a. sat A a \<Longrightarrow> mono_transformer (R a)"
+    shows "\<exists>S'. package_rhs \<sigma> unit {(a, unit, R a) |a. sat A a} (\<lambda>_. True) B \<sigma>' w S'"
+proof -
+  let ?S = "{(a, unit, R a) |a. sat A a}"
+  have "\<exists>S'. package_rhs \<sigma> unit {(a, unit, R a) |a. sat A a} (\<lambda>_. True) B \<sigma>' w S'"
+  proof (rule general_completeness[of ?S w B \<sigma> \<sigma>'])
+    show "\<And>a u T x. (a, u, T) \<in> {(a, unit, R a) |a. sat A a} \<Longrightarrow> Some x = a \<oplus> T w \<Longrightarrow> sat B x"
+      using assms(2) is_footprint_general_def by blast
+    show "Some \<sigma> = \<sigma>' \<oplus> w" by (simp add: assms(3))
+    show "stable w" by (simp add: assms(2))
+    show "wf_assertion B" by (simp add: assms(1))
+
+    show "valid_package_set {(a, unit, R a) |a. sat A a} unit"
+    proof (rule valid_package_setI)
+      fix a u T assume asm0: "(a, u, T) \<in> {(a, unit, R a) |a. sat A a}"
+      then have "u = unit \<and> T = R a \<and> sat A a" by fastforce
+      then show "a ## u \<and>  |a|  \<succeq>  |u|  \<and> mono_transformer T \<and> a \<succeq>  |T unit|"
+        using assms(4) defined_def mono_transformer_def unit_core unit_neutral unit_smaller by auto
+    qed
+  qed
+  then show ?thesis by meson
+qed
+
+corollary completeness_paper:
+  assumes "wf_assertion B"
+      and "stable w \<and> is_footprint_standard w A B"
+      and "Some \<sigma> = \<sigma>' \<oplus> w"
+    shows "\<exists>S'. package_rhs \<sigma> unit {(a, unit, id) |a. sat A a} (\<lambda>_. True) B \<sigma>' w S'"
+proof -
+  have "\<exists>S'. package_rhs \<sigma> unit {(a, unit, (\<lambda>_. id) a) |a. sat A a} (\<lambda>_. True) B \<sigma>' w S'"
+    using assms(1)
+  proof (rule completeness)
+    show "stable w \<and> is_footprint_general w (\<lambda>a. id) A B"
+      using assms(2) is_footprint_general_def is_footprint_standard_def by force
+    show "Some \<sigma> = \<sigma>' \<oplus> w" by (simp add: assms(3))
+    show "\<And>a. sat A a \<Longrightarrow> mono_transformer id" using mono_transformer_def by auto
+  qed
+  then show ?thesis by meson
+qed
+
+
+end
+
+end
diff --git a/thys/Package_logic/ROOT b/thys/Package_logic/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Package_logic/ROOT
@@ -0,0 +1,10 @@
+chapter AFP
+
+session Package_logic (AFP) = HOL +
+  options [timeout=300]
+  theories
+  	SepAlgebra
+  	PackageLogic
+  document_files
+	"root.bib"
+    	"root.tex"
diff --git a/thys/Package_logic/SepAlgebra.thy b/thys/Package_logic/SepAlgebra.thy
new file mode 100755
--- /dev/null
+++ b/thys/Package_logic/SepAlgebra.thy
@@ -0,0 +1,1042 @@
+section \<open>Separation Algebra\<close>
+
+text \<open>In this section, we formalize the concept of a separation algebra~\cite{Calcagno2007, Dockins2009}, on which our package logic is based.\<close>
+
+theory SepAlgebra
+  imports Main
+begin
+
+type_synonym 'a property = "'a \<Rightarrow> bool"
+
+locale sep_algebra =
+
+  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a option" (infixl "\<oplus>" 63)
+
+  fixes core :: "'a \<Rightarrow> 'a" (" |_| ")
+  (* Largest duplicable part of a state *)
+
+  assumes commutative: "a \<oplus> b = b \<oplus> a"
+      and asso1: "a \<oplus> b = Some ab \<and> b \<oplus> c = Some bc \<Longrightarrow> ab \<oplus> c = a \<oplus> bc"
+      and asso2: "a \<oplus> b = Some ab \<and> b \<oplus> c = None \<Longrightarrow> ab \<oplus> c = None"
+
+(* The core of x is the max of { p | pure p \<and> x \<ge> p} *)
+      and core_is_smaller: "Some x = x \<oplus> |x|"
+      and core_is_pure: "Some |x| = |x| \<oplus> |x|"
+      and core_max: "Some x = x \<oplus> c \<Longrightarrow> (\<exists>r. Some |x| = c \<oplus> r)"
+      and core_sum: "Some c = a \<oplus> b \<Longrightarrow> Some |c| = |a| \<oplus> |b|"
+
+      and positivity: "a \<oplus> b = Some c \<Longrightarrow> Some c = c \<oplus> c \<Longrightarrow> Some a = a \<oplus> a"
+      and cancellative: "Some a = b \<oplus> x \<Longrightarrow> Some a = b \<oplus> y \<Longrightarrow> |x| = |y| \<Longrightarrow> x = y"
+
+begin
+
+lemma asso3:
+  assumes "a \<oplus> b = None"
+      and "b \<oplus> c = Some bc"
+    shows "a \<oplus> bc = None"
+  by (metis assms(1) assms(2) sep_algebra.asso2 sep_algebra.commutative sep_algebra_axioms)
+
+subsection  \<open>Definitions\<close>
+
+definition defined :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "##" 62) where
+  "a ## b \<longleftrightarrow> a \<oplus> b \<noteq> None"
+
+definition greater :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<succeq>" 50) where
+  "a \<succeq> b \<longleftrightarrow> (\<exists>c. Some a = b \<oplus> c)"
+
+definition pure :: "'a \<Rightarrow> bool" where
+  "pure a \<longleftrightarrow> Some a = a \<oplus> a"
+
+definition minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<ominus>" 63)
+  where "b \<ominus> a = (THE_default b (\<lambda>x. Some b = a \<oplus> x \<and> x \<succeq> |b| ))"
+
+definition add_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<otimes>" 60) where
+  "A \<otimes> B = { \<phi> | \<phi> a b. a \<in> A \<and> b \<in> B \<and> Some \<phi> = a \<oplus> b }"
+
+definition greater_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "\<ggreater>" 50) where
+  "A \<ggreater> B \<longleftrightarrow> (\<forall>a \<in> A. \<exists>b \<in> B. a \<succeq> b)"
+
+definition up_closed :: "'a set \<Rightarrow> bool" where
+  "up_closed A \<longleftrightarrow> (\<forall>\<phi>'. (\<exists>\<phi> \<in> A. \<phi>' \<succeq> \<phi>) \<longrightarrow> \<phi>' \<in> A)"
+
+definition equiv :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "\<sim>" 40) where
+  "A \<sim> B \<longleftrightarrow> A \<ggreater> B \<and> B \<ggreater> A"
+
+definition setify :: "'a property \<Rightarrow> ('a set \<Rightarrow> bool)" where
+  "setify P A \<longleftrightarrow> (\<forall>x \<in> A. P x)"
+
+definition mono_prop :: "'a property \<Rightarrow> bool" where
+  "mono_prop P \<longleftrightarrow> (\<forall>x y. y \<succeq> x \<and> P x \<longrightarrow> P y)"
+
+definition under :: "'a set \<Rightarrow> 'a \<Rightarrow> 'a set" where
+  "under A \<omega> = { \<omega>' | \<omega>'. \<omega>' \<in> A \<and> \<omega> \<succeq> \<omega>'}"
+
+definition max_projection_prop :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where
+  "max_projection_prop P f \<longleftrightarrow> (\<forall>x. x \<succeq> f x \<and> P (f x) \<and>
+  (\<forall>p. P p \<and> x \<succeq> p \<longrightarrow> f x \<succeq> p))"
+
+inductive multi_plus :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
+  MPSingle: "multi_plus [a] a"
+| MPConcat: "\<lbrakk> length la > 0 ; length lb > 0 ; multi_plus la a ; multi_plus lb b ; Some \<omega> = a \<oplus> b \<rbrakk> \<Longrightarrow> multi_plus (la @ lb)  \<omega>"
+
+fun splus :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option" where
+  "splus None _ = None"
+| "splus _ None = None"
+| "splus (Some a) (Some b) = a \<oplus> b"
+
+
+
+subsection \<open>First lemmata\<close>
+
+lemma greater_equiv:
+  "a \<succeq> b \<longleftrightarrow> (\<exists>c. Some a = c \<oplus> b)"
+  using commutative greater_def by auto
+
+lemma smaller_compatible:
+  assumes "a' ## b"
+      and "a' \<succeq> a"
+    shows "a ## b"
+  by (metis (full_types) assms(1) assms(2) asso3 commutative defined_def greater_def)
+
+lemma bigger_sum_smaller:
+  assumes "Some c = a \<oplus> b"
+      and "a \<succeq> a'"
+    shows "\<exists>b'. b' \<succeq> b \<and> Some c = a' \<oplus> b'"
+proof -
+  obtain r where "Some a = a' \<oplus> r" 
+    using assms(2) greater_def by auto
+  then obtain br where "Some br = r \<oplus> b"
+    by (metis assms(1) asso2 domD domIff option.discI)
+  then have "Some c = a' \<oplus> br" 
+    by (metis \<open>Some a = a' \<oplus> r\<close> assms(1) asso1)
+  then show ?thesis 
+    using \<open>Some br = r \<oplus> b\<close> commutative greater_def by force
+qed
+
+subsubsection \<open>splus\<close>
+
+lemma splus_develop:
+  assumes "Some a = b \<oplus> c"
+  shows "a \<oplus> d = splus (splus (Some b) (Some c)) (Some d)"
+  by (metis assms splus.simps(3))
+
+lemma splus_comm:
+  "splus a b = splus b a"
+  apply (cases a)
+   apply (cases b)
+    apply simp_all
+  apply (cases b)
+  by (simp_all add: commutative)
+
+lemma splus_asso:
+  "splus (splus a b) c = splus a (splus b c)"
+proof (cases a)
+  case None
+  then show ?thesis 
+    by simp
+next
+  case (Some a')
+  then have "a = Some a'" by simp
+  then show ?thesis
+  proof (cases b)
+    case None
+    then show ?thesis by (simp add: Some)
+  next
+    case (Some b')
+    then have "b = Some b'" by simp
+    then show ?thesis
+    proof (cases c)
+      case None
+      then show ?thesis by (simp add: splus_comm)
+    next
+      case (Some c')
+      then have "c = Some c'" by simp
+      then show ?thesis
+      proof (cases "a' \<oplus> b'")
+        case None
+        then have "a' \<oplus> b' = None" by simp
+        then show ?thesis
+        proof (cases "b' \<oplus> c'")
+          case None
+          then show ?thesis 
+            by (simp add: Some \<open>a = Some a'\<close> \<open>a' \<oplus> b' = None\<close> \<open>b = Some b'\<close>)
+        next
+          case (Some bc)
+          then show ?thesis
+            by (metis (full_types) None \<open>a = Some a'\<close> \<open>b = Some b'\<close> \<open>c = Some c'\<close> sep_algebra.asso2 sep_algebra_axioms splus.simps(2) splus.simps(3) splus_comm)
+        qed
+      next
+        case (Some ab)
+        then have "Some ab = a' \<oplus> b'" by simp
+        then show ?thesis
+        proof (cases "b' \<oplus> c'")
+          case None
+          then show ?thesis 
+            by (metis Some \<open>a = Some a'\<close> \<open>b = Some b'\<close> \<open>c = Some c'\<close> asso2 splus.simps(2) splus.simps(3))
+        next
+          case (Some bc)
+          then show ?thesis
+            by (metis \<open>Some ab = a' \<oplus> b'\<close> \<open>a = Some a'\<close> \<open>b = Some b'\<close> \<open>c = Some c'\<close> sep_algebra.asso1 sep_algebra_axioms splus.simps(3))
+        qed
+      qed
+    qed
+  qed
+qed
+
+
+
+
+
+
+
+subsubsection \<open>Pure\<close>
+
+(* Maybe need more *)
+lemma pure_stable:
+  assumes "pure a"
+      and "pure b"
+      and "Some c = a \<oplus> b"
+    shows "pure c"
+  by (metis assms asso1 commutative pure_def)
+
+(* Specific to pure *)
+lemma pure_smaller:
+  assumes "pure a"
+      and "a \<succeq> b"
+    shows "pure b"
+  by (metis assms greater_def positivity pure_def)
+
+
+subsection \<open>Succ is an order\<close>
+
+lemma succ_antisym:
+  assumes "a \<succeq> b"
+      and "b \<succeq> a"
+    shows "a = b"
+proof -
+  obtain ra where "Some a = b \<oplus> ra" 
+    using assms(1) greater_def by auto
+  obtain rb where "Some b = a \<oplus> rb" 
+    using assms(2) greater_def by auto
+  then have "Some a = splus (Some a) (splus (Some ra) (Some rb))"
+  proof -
+    have "Some b = splus (Some a) (Some rb)"
+      by (simp add: \<open>Some b = a \<oplus> rb\<close>)
+    then show ?thesis
+      by (metis (full_types) \<open>Some a = b \<oplus> ra\<close> sep_algebra.splus.simps(3) sep_algebra_axioms splus_asso splus_comm)
+  qed
+  moreover have "Some b = splus (Some b) (splus (Some ra) (Some rb))"
+    by (metis \<open>Some a = b \<oplus> ra\<close> \<open>Some b = a \<oplus> rb\<close> sep_algebra.splus.simps(3) sep_algebra_axioms splus_asso)
+  moreover have "pure ra \<and> pure rb"
+  proof -
+    obtain rab where "Some rab = ra \<oplus> rb" 
+      by (metis calculation(2) splus.elims splus.simps(3))
+    then have "|a| \<succeq> rab" 
+      by (metis calculation(1) core_max greater_def splus.simps(3))
+    then have "pure rab" 
+      using core_is_pure pure_def pure_smaller by blast
+    moreover have "rab \<succeq> ra \<and> rab \<succeq> rb" 
+      using \<open>Some rab = ra \<oplus> rb\<close> greater_def greater_equiv by blast
+    ultimately have "pure ra" using pure_smaller 
+      by blast
+    moreover have "pure rb" 
+      using \<open>pure rab\<close> \<open>rab \<succeq> ra \<and> rab \<succeq> rb\<close> pure_smaller by blast
+    ultimately show ?thesis 
+      by blast
+  qed
+  ultimately show ?thesis 
+    by (metis \<open>Some b = a \<oplus> rb\<close> option.inject pure_def sep_algebra.splus.simps(3) sep_algebra_axioms splus_asso)
+qed
+
+lemma succ_trans:
+  assumes "a \<succeq> b"
+      and "b \<succeq> c"
+    shows "a \<succeq> c"
+  using assms(1) assms(2) bigger_sum_smaller greater_def by blast
+
+lemma succ_refl:
+  "a \<succeq> a" 
+  using core_is_smaller greater_def by blast
+
+
+
+
+
+
+
+
+subsection \<open>Core (pure) and stabilize (stable)\<close>
+
+lemma max_projection_propI:
+  assumes "\<And>x. x \<succeq> f x"
+      and "\<And>x. P (f x)"
+      and "\<And>x p. P p \<and> x \<succeq> p \<Longrightarrow> f x \<succeq> p"
+    shows "max_projection_prop P f"
+  by (simp add: assms(1) assms(2) assms(3) max_projection_prop_def)
+
+lemma max_projection_propE:
+  assumes "max_projection_prop P f"
+    shows "\<And>x. x \<succeq> f x"
+      and "\<And>x. P (f x)"
+      and "\<And>x p. P p \<and> x \<succeq> p \<Longrightarrow> f x \<succeq> p"
+  using assms max_projection_prop_def by auto
+
+lemma max_projection_prop_pure_core:
+  "max_projection_prop pure core"
+proof (rule max_projection_propI)
+  fix x
+  show "x \<succeq> |x|" 
+    using core_is_smaller greater_equiv by blast
+  show "pure |x|" 
+    by (simp add: core_is_pure pure_def)
+  show "\<And>p. pure p \<and> x \<succeq> p \<Longrightarrow> |x| \<succeq> p"
+  proof -
+    fix p assume "pure p \<and> x \<succeq> p"
+    then obtain r where "Some x = p \<oplus> r" 
+      using greater_def by blast
+    then show "|x| \<succeq> p"
+      by (metis \<open>pure p \<and> x \<succeq> p\<close> asso1 commutative core_max greater_equiv pure_def)
+  qed
+qed
+
+lemma mpp_smaller:
+  assumes "max_projection_prop P f"
+  shows "x \<succeq> f x"
+  using assms max_projection_propE(1) by auto
+
+lemma mpp_compatible:
+  assumes "max_projection_prop P f"
+      and "a ## b"
+    shows "f a ## f b"
+  by (metis (mono_tags, opaque_lifting) assms(1) assms(2) commutative defined_def max_projection_prop_def smaller_compatible)
+
+
+
+lemma mpp_prop:
+  assumes "max_projection_prop P f"
+  shows "P (f x)"
+  by (simp add: assms max_projection_propE(2))
+
+
+lemma mppI:
+  assumes "max_projection_prop P f"
+      and "a \<succeq> x"
+      and "P x"
+      and "x \<succeq> f a"
+    shows "x = f a"
+proof -
+  have "f a \<succeq> x" 
+    using assms max_projection_propE(3) by auto
+  then show ?thesis 
+    by (simp add: assms(4) succ_antisym)
+qed
+
+lemma mpp_invo:
+  assumes "max_projection_prop P f"
+  shows "f (f x) = f x"
+  using assms max_projection_prop_def succ_antisym by auto
+
+lemma mpp_mono:
+  assumes "max_projection_prop P f"
+      and "a \<succeq> b"
+    shows "f a \<succeq> f b"
+  by (metis assms max_projection_prop_def succ_trans)
+
+
+subsection \<open>Subtraction\<close>
+
+lemma addition_bigger:
+  assumes "a' \<succeq> a"
+      and "Some x' = a' \<oplus> b"
+      and "Some x = a \<oplus> b"
+    shows "x' \<succeq> x"
+  by (metis assms asso1 bigger_sum_smaller greater_def)
+
+
+lemma smaller_than_core:
+  assumes "y \<succeq> x"
+      and "Some z = x \<oplus> |y|"
+    shows "|z| = |y|"
+proof -
+  have "Some |z| = |x| \<oplus> |y|"
+    using assms(2) core_sum max_projection_prop_pure_core mpp_invo by fastforce
+  then have "Some |z| = |x| \<oplus> |y|"
+    by simp
+  moreover have "|z| \<succeq> |y|" 
+    using calculation greater_equiv by blast
+  ultimately show ?thesis 
+    by (meson addition_bigger assms(1) assms(2) core_is_smaller core_sum greater_def succ_antisym)
+qed
+
+lemma extract_core:
+  assumes "Some b = a \<oplus> x \<and> x \<succeq> |b|"
+  shows "|x| = |b|"
+proof -
+  obtain r where "Some x = r \<oplus> |b|"
+    using assms greater_equiv by auto
+  show ?thesis
+  proof (rule smaller_than_core)
+    show "Some x = r \<oplus> |b|"
+      using \<open>Some x = r \<oplus> |b|\<close> by auto
+    show "b \<succeq> r"
+      by (metis \<open>Some x = r \<oplus> |b|\<close> assms commutative greater_def succ_trans)
+  qed
+qed
+
+
+lemma minus_unique:
+  assumes "Some b = a \<oplus> x \<and> x \<succeq> |b|"
+      and "Some b = a \<oplus> y \<and> y \<succeq> |b|"
+    shows "x = y"
+proof -
+  have "|x| = |b|"
+    using assms(1) extract_core by blast
+  moreover have "|y| = |b|"
+    using assms(2) extract_core by blast
+  ultimately show ?thesis
+    using assms(1) assms(2) cancellative by auto
+qed
+
+lemma minus_exists:
+  assumes "b \<succeq> a"
+  shows "\<exists>x. Some b = a \<oplus> x \<and> x \<succeq> |b|"
+  using assms bigger_sum_smaller core_is_smaller by blast
+
+lemma minus_equiv_def:
+  assumes "b \<succeq> a"
+    shows "Some b = a \<oplus> (b \<ominus> a) \<and> (b \<ominus> a) \<succeq> |b|"
+proof -
+  let ?x = "THE_default b (\<lambda>x. Some b = a \<oplus> x \<and> x \<succeq> |b| )"
+  have "(\<lambda>x. Some b = a \<oplus> x \<and> x \<succeq> |b| ) ?x"
+  proof (rule THE_defaultI')
+    show "\<exists>!x. Some b = a \<oplus> x \<and> x \<succeq> |b|"
+      using assms local.minus_unique minus_exists by blast
+  qed
+  then show ?thesis by (metis minus_def)
+qed
+
+lemma minus_default:
+  assumes "\<not> b \<succeq> a"
+  shows "b \<ominus> a = b"
+  using THE_default_none assms greater_def minus_def by fastforce
+
+lemma minusI:
+  assumes "Some b = a \<oplus> x"
+      and "x \<succeq> |b|"
+    shows "x = b \<ominus> a"  
+  using assms(1) assms(2) greater_def local.minus_unique minus_equiv_def by blast
+
+lemma minus_core:
+  "|a \<ominus> b| = |a|"
+proof (cases "a \<succeq> b")
+  case True
+  then have "Some a = b \<oplus> (a \<ominus> b) \<and> a \<ominus> b \<succeq> |a|"
+    using minus_equiv_def by auto
+  then show ?thesis
+    using extract_core by blast
+next
+  case False
+  then show ?thesis by (simp add: minus_default)
+qed
+
+
+lemma minus_core_weaker:
+  "|a \<ominus> b| = |a| \<ominus> |b|"
+proof (cases "a \<succeq> b")
+  case True
+  then show ?thesis 
+    by (metis greater_equiv max_projection_prop_pure_core minus_core minus_default minus_equiv_def mpp_invo succ_antisym)
+next
+  case False
+  then show ?thesis
+    by (metis greater_equiv max_projection_prop_pure_core minus_default minus_equiv_def mpp_invo succ_antisym)
+qed
+
+lemma minus_equiv_def_any_elem:
+  assumes "Some x = a \<oplus> b"
+  shows "Some (x \<ominus> a) = b \<oplus> |x|"
+proof -
+  obtain r where "Some r = b \<oplus> |x|" 
+    by (metis assms core_is_smaller domD domIff option.simps(3) sep_algebra.asso2 sep_algebra_axioms)
+  have "r = x \<ominus> a"
+  proof (rule minusI)
+    show "Some x = a \<oplus> r" 
+      by (metis \<open>Some r = b \<oplus> |x|\<close> assms asso1 core_is_smaller)
+    moreover show "r \<succeq> |x|"
+      using \<open>Some r = b \<oplus> |x|\<close> greater_equiv by blast
+  qed
+  then show ?thesis 
+    using \<open>Some r = b \<oplus> |x|\<close> by blast
+qed
+
+lemma minus_bigger:
+  assumes "Some x = a \<oplus> b"
+  shows "x \<ominus> a \<succeq> b"
+  using assms greater_def minus_equiv_def_any_elem by blast
+
+lemma minus_smaller:
+  assumes "x \<succeq> a"
+  shows "x \<succeq> x \<ominus> a"
+  using assms greater_equiv minus_equiv_def by blast
+
+lemma minus_sum:
+  assumes "Some a = b \<oplus> c"
+      and "x \<succeq> a"
+    shows "x \<ominus> a = (x \<ominus> b) \<ominus> c"
+proof (rule minusI)
+  obtain r where "Some r = c \<oplus> (x \<ominus> a)"
+    by (metis assms(1) assms(2) asso2 minus_equiv_def option.exhaust_sel)
+  have "r = (x \<ominus> b)"
+  proof (rule minusI)
+    show "Some x = b \<oplus> r" 
+      by (metis \<open>Some r = c \<oplus> (x \<ominus> a)\<close> assms(1) assms(2) asso1 minus_equiv_def)
+    moreover show "r \<succeq> |x|" 
+      by (meson \<open>Some r = c \<oplus> (x \<ominus> a)\<close> assms(2) greater_equiv sep_algebra.minus_equiv_def sep_algebra_axioms succ_trans)
+  qed
+  then show "Some (x \<ominus> b) = c \<oplus> (x \<ominus> a)" 
+    using \<open>Some r = c \<oplus> (x \<ominus> a)\<close> by blast
+  moreover show "x \<ominus> a \<succeq> |x \<ominus> b|"
+    by (simp add: assms(2) minus_core minus_equiv_def)
+qed
+
+lemma smaller_compatible_core:
+  assumes "y \<succeq> x"
+  shows "x ## |y|"
+  by (metis assms asso2 core_is_smaller defined_def greater_equiv option.discI)
+
+lemma smaller_pure_sum_smaller:
+  assumes "y \<succeq> a"
+      and "y \<succeq> b"
+      and "Some x = a \<oplus> b"
+      and "pure b"
+    shows "y \<succeq> x"
+proof -
+  obtain r where "Some y = r \<oplus> b" "r \<succeq> a"
+    by (metis assms(1) assms(2) assms(4) asso1 greater_equiv pure_def)
+  then show ?thesis
+    using addition_bigger assms(3) by blast
+qed
+
+lemma greater_minus_trans:
+  assumes "y \<succeq> x"
+      and "x \<succeq> a"
+    shows "y \<ominus> a \<succeq> x \<ominus> a"
+proof -
+  obtain r where "Some y = x \<oplus> r" 
+    using assms(1) greater_def by blast
+  then obtain ra where "Some x = a \<oplus> ra" 
+    using assms(2) greater_def by blast
+  then have "Some (x \<ominus> a) = ra \<oplus> |x|"
+    by (simp add: minus_equiv_def_any_elem)
+  then obtain yy where "Some yy = (x \<ominus> a) \<oplus> r" 
+    by (metis (full_types) \<open>Some y = x \<oplus> r\<close> assms(2) asso3 commutative minus_equiv_def not_Some_eq)
+  then have "Some x = a \<oplus> (x \<ominus> a) \<and> x \<ominus> a \<succeq>  |x|"
+    by (simp add: assms(2) sep_algebra.minus_equiv_def sep_algebra_axioms)
+  then obtain y' where "Some y' = a \<oplus> yy"
+    using \<open>Some y = x \<oplus> r\<close> \<open>Some yy = x \<ominus> a \<oplus> r\<close> asso1
+    by metis
+  moreover have "y \<succeq> y'"
+    by (metis \<open>Some x = a \<oplus> (x \<ominus> a) \<and> x \<ominus> a \<succeq> |x|\<close> \<open>Some y = x \<oplus> r\<close> \<open>Some yy = x \<ominus> a \<oplus> r\<close> asso1 calculation option.inject succ_refl)
+  moreover obtain x' where "Some x' = (x \<ominus> a) \<oplus> a" 
+    using assms(2) commutative minus_equiv_def by fastforce
+  then have "y \<succeq> x'" 
+    by (metis assms(1) assms(2) commutative minus_equiv_def option.sel)
+  moreover have "x' \<succeq> x \<ominus> a" 
+    using \<open>Some x' = x \<ominus> a \<oplus> a\<close> greater_def by auto
+  ultimately show ?thesis 
+    using \<open>Some x' = x \<ominus> a \<oplus> a\<close> \<open>Some y = x \<oplus> r\<close> assms(2) asso1 commutative greater_equiv minus_bigger minus_equiv_def option.sel sep_algebra.succ_trans sep_algebra_axioms
+  proof -
+    have f1: "Some y' = a \<oplus> yy"
+      by (simp add: \<open>Some y' = a \<oplus> yy\<close> commutative)
+    then have "y = y'"
+      by (metis \<open>Some y = x \<oplus> r\<close> \<open>Some yy = x \<ominus> a \<oplus> r\<close> \<open>x \<succeq> a\<close> asso1 minus_equiv_def option.sel)
+    then show ?thesis
+      using f1 by (metis (no_types) \<open>Some yy = x \<ominus> a \<oplus> r\<close> commutative greater_equiv minus_bigger sep_algebra.succ_trans sep_algebra_axioms)
+  qed
+qed
+
+
+
+
+lemma minus_and_plus:
+  assumes "Some \<omega>' = \<omega> \<oplus> r"
+      and "\<omega> \<succeq> a"
+    shows "Some (\<omega>' \<ominus> a) = (\<omega> \<ominus> a) \<oplus> r"
+proof -
+  have "\<omega> \<succeq> \<omega> \<ominus> a" 
+    by (simp add: assms(2) minus_smaller)
+  then have "(\<omega> \<ominus> a) ## r" 
+    by (metis (full_types) assms(1) defined_def option.discI sep_algebra.smaller_compatible sep_algebra_axioms)
+  then obtain x where "Some x = (\<omega> \<ominus> a) \<oplus> r"
+    using defined_def by auto
+  then have "Some \<omega>' = a \<oplus> x \<and> x \<succeq> |\<omega>'|"
+    by (metis (no_types, lifting) assms asso1 core_sum max_projection_prop_pure_core minus_core minus_equiv_def mpp_smaller option.inject)
+  then have "x = \<omega>' \<ominus> a" 
+    by (simp add: minusI)
+  then show ?thesis 
+    using \<open>Some x = \<omega> \<ominus> a \<oplus> r\<close> by blast
+qed
+
+
+
+
+
+
+
+
+
+subsection \<open>Lifting the algebra to sets of states\<close>
+
+lemma add_set_commm:
+  "A \<otimes> B = B \<otimes> A"
+proof
+  show "A \<otimes> B \<subseteq> B \<otimes> A"
+    using add_set_def sep_algebra.commutative sep_algebra_axioms by fastforce
+  show "B \<otimes> A \<subseteq> A \<otimes> B"
+    using add_set_def commutative by fastforce
+qed
+
+lemma x_elem_set_product:
+  "x \<in> A \<otimes> B \<longleftrightarrow> (\<exists>a b. a \<in> A \<and> b \<in> B \<and> Some x = a \<oplus> b)"
+  using sep_algebra.add_set_def sep_algebra_axioms by fastforce
+
+lemma x_elem_set_product_splus:
+  "x \<in> A \<otimes> B \<longleftrightarrow> (\<exists>a b. a \<in> A \<and> b \<in> B \<and> Some x = splus (Some a) (Some b))"
+  using sep_algebra.add_set_def sep_algebra_axioms by fastforce
+
+lemma add_set_asso:
+  "(A \<otimes> B) \<otimes> C = A \<otimes> (B \<otimes> C)" (is "?A = ?B")
+proof -
+  have "?A \<subseteq> ?B"
+  proof (rule subsetI)
+    fix x assume "x \<in> ?A"
+    then obtain ab c where "Some x = ab \<oplus> c" "ab \<in> A \<otimes> B" "c \<in> C"
+      using x_elem_set_product by auto
+    then obtain a b where "Some ab = a \<oplus> b" "a \<in> A" "b \<in> B"
+      using x_elem_set_product by auto
+    then obtain bc where "Some bc = b \<oplus> c" 
+      by (metis \<open>Some x = ab \<oplus> c\<close> asso2 option.exhaust)
+    then show "x \<in> ?B" 
+      by (metis \<open>Some ab = a \<oplus> b\<close> \<open>Some x = ab \<oplus> c\<close> \<open>a \<in> A\<close> \<open>b \<in> B\<close> \<open>c \<in> C\<close> asso1 x_elem_set_product)
+  qed
+  moreover have "?B \<subseteq> ?A"
+  proof (rule subsetI)
+    fix x assume "x \<in> ?B"
+    then obtain a bc where "Some x = a \<oplus> bc" "a \<in> A" "bc \<in> B \<otimes> C"
+      using x_elem_set_product by auto
+    then obtain b c where "Some bc = b \<oplus> c" "c \<in> C" "b \<in> B"
+      using x_elem_set_product by auto
+    then obtain ab where "Some ab = a \<oplus> b"
+      by (metis \<open>Some x = a \<oplus> bc\<close> asso3 option.collapse)
+    then show "x \<in> ?A"
+      by (metis \<open>Some bc = b \<oplus> c\<close> \<open>Some x = a \<oplus> bc\<close> \<open>a \<in> A\<close> \<open>b \<in> B\<close> \<open>c \<in> C\<close> asso1 x_elem_set_product)
+  qed
+  ultimately show ?thesis by blast
+qed
+
+lemma up_closedI:
+  assumes "\<And>\<phi>' \<phi>. (\<phi>' :: 'a) \<succeq> \<phi> \<and> \<phi> \<in> A \<Longrightarrow> \<phi>' \<in> A"
+  shows "up_closed A"
+  using assms up_closed_def by blast
+
+lemma up_closed_plus_UNIV:
+  "up_closed (A \<otimes> UNIV)"
+proof (rule up_closedI)
+  fix \<phi> \<phi>'
+  assume asm: "\<phi>' \<succeq> \<phi> \<and> \<phi> \<in> A \<otimes> UNIV"
+  then obtain r a b where "Some \<phi>' = \<phi> \<oplus> r" "Some \<phi> = a \<oplus> b" "a \<in> A"
+    using greater_def x_elem_set_product by auto
+  then obtain br where "Some br = b \<oplus> r" 
+    by (metis asso2 option.exhaust_sel)
+  then have "Some \<phi>' = a \<oplus> br" 
+    by (metis \<open>Some \<phi> = a \<oplus> b\<close> \<open>Some \<phi>' = \<phi> \<oplus> r\<close> splus.simps(3) splus_asso)
+  then show "\<phi>' \<in> A \<otimes> UNIV" 
+    using \<open>a \<in> A\<close> x_elem_set_product by auto
+qed
+
+
+lemma succ_set_trans:
+  assumes "A \<ggreater> B"
+      and "B \<ggreater> C"
+    shows "A \<ggreater> C"
+  by (meson assms(1) assms(2) greater_set_def succ_trans)
+
+lemma greater_setI:
+  assumes "\<And>a. a \<in> A \<Longrightarrow> (\<exists>b \<in> B. a \<succeq> b)"
+    shows "A \<ggreater> B"
+  by (simp add: assms greater_set_def)  
+
+lemma bigger_set:
+  assumes "A' \<ggreater> A"
+  shows "A' \<otimes> B \<ggreater> A \<otimes> B"
+proof (rule greater_setI)
+  fix x assume "x \<in> A' \<otimes> B"
+  then obtain a' b where "Some x = a' \<oplus> b" "a' \<in> A'" "b \<in> B"
+    using x_elem_set_product by auto
+  then obtain a where "a' \<succeq> a" "a \<in> A"
+    using assms greater_set_def by blast
+  then obtain ab where "Some ab = a \<oplus> b"
+    by (metis \<open>Some x = a' \<oplus> b\<close> asso2 domD domIff greater_equiv)
+  then show "\<exists>ab\<in>A \<otimes> B. x \<succeq> ab"
+    using \<open>Some x = a' \<oplus> b\<close> \<open>a \<in> A\<close> \<open>a' \<succeq> a\<close> \<open>b \<in> B\<close> addition_bigger x_elem_set_product by blast
+qed
+
+lemma bigger_singleton:
+  assumes "\<phi>' \<succeq> \<phi>"
+  shows "{\<phi>'} \<ggreater> {\<phi>}"
+  by (simp add: assms greater_set_def)
+
+lemma add_set_elem:
+  "\<phi> \<in> A \<otimes> B \<longleftrightarrow> (\<exists>a b. Some \<phi> = a \<oplus> b \<and> a \<in> A \<and> b \<in> B)"
+  using add_set_def by auto
+
+lemma up_closed_sum:
+  assumes "up_closed A"
+    shows "up_closed (A \<otimes> B)"
+proof (rule up_closedI)
+  fix \<phi>' \<phi> assume asm: "\<phi>' \<succeq> \<phi> \<and> \<phi> \<in> A \<otimes> B"
+  then obtain a b where "a \<in> A" "b \<in> B" "Some \<phi> = a \<oplus> b" 
+    using add_set_elem by auto
+  moreover obtain r where "Some \<phi>' = \<phi> \<oplus> r" 
+    using asm greater_def by blast
+  then obtain ar where "Some ar = a \<oplus> r" 
+    by (metis asso2 calculation(3) commutative option.exhaust_sel option.simps(3))
+  then have "ar \<in> A" 
+    by (meson assms calculation(1) greater_def sep_algebra.up_closed_def sep_algebra_axioms)
+  then show "\<phi>' \<in> A \<otimes> B" 
+    by (metis \<open>Some \<phi>' = \<phi> \<oplus> r\<close> \<open>Some ar = a \<oplus> r\<close> add_set_elem asso1 calculation(2) calculation(3) commutative)
+qed
+
+lemma up_closed_bigger_subset:
+  assumes "up_closed B"
+      and "A \<ggreater> B"
+    shows "A \<subseteq> B"
+  by (meson assms(1) assms(2) greater_set_def sep_algebra.up_closed_def sep_algebra_axioms subsetI)
+
+lemma up_close_equiv:
+  assumes "up_closed A"
+      and "up_closed B"
+    shows "A \<sim> B \<longleftrightarrow> A = B"
+proof -
+  have "A \<sim> B \<longleftrightarrow> A \<ggreater> B \<and> B \<ggreater> A" 
+    using local.equiv_def by auto
+  also have "... \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" 
+    by (metis assms(1) assms(2) greater_set_def set_eq_subset succ_refl up_closed_bigger_subset)
+  ultimately show ?thesis 
+    by blast
+qed
+
+lemma equiv_stable_sum:
+  assumes "A \<sim> B"
+  shows "A \<otimes> C \<sim> B \<otimes> C"
+  using assms bigger_set local.equiv_def by auto
+
+lemma equiv_up_closed_subset:
+  assumes "up_closed A"
+      and "equiv B C"
+    shows "B \<subseteq> A \<longleftrightarrow> C \<subseteq> A" (is "?B \<longleftrightarrow> ?C")
+proof -
+  have "?B \<Longrightarrow> ?C"
+    by (meson greater_set_def up_closed_def equiv_def assms(1) assms(2) subsetD subsetI)
+  moreover have "?C \<Longrightarrow> ?B"
+    by (meson greater_set_def up_closed_def equiv_def assms(1) assms(2) subsetD subsetI)
+  ultimately show ?thesis by blast
+qed
+
+lemma mono_propI:
+  assumes "\<And>x y. y \<succeq> x \<and> P x \<Longrightarrow> P y"
+  shows "mono_prop P"
+  using assms mono_prop_def by blast
+
+lemma mono_prop_set:
+  assumes "A \<ggreater> B"
+      and "setify P B"
+      and "mono_prop P"
+    shows "setify P A"
+  using assms(1) assms(2) assms(3) greater_set_def local.setify_def mono_prop_def by auto
+
+lemma mono_prop_set_equiv:
+  assumes "mono_prop P"
+      and "equiv A B"
+    shows "setify P A \<longleftrightarrow> setify P B"
+  by (meson assms(1) assms(2) local.equiv_def sep_algebra.mono_prop_set sep_algebra_axioms)
+
+lemma setify_sum:
+  "setify P (A \<otimes> B) \<longleftrightarrow> (\<forall>x \<in> A. setify P ({x} \<otimes> B))" (is "?A \<longleftrightarrow> ?B")
+proof -
+  have "?A \<Longrightarrow> ?B" 
+    using local.setify_def sep_algebra.add_set_elem sep_algebra_axioms singletonD by fastforce
+  moreover have "?B \<Longrightarrow> ?A" 
+    using add_set_elem local.setify_def by fastforce
+  ultimately show ?thesis by blast
+qed
+
+lemma setify_sum_image:
+  "setify P ((Set.image f A) \<otimes> B) \<longleftrightarrow> (\<forall>x \<in> A. setify P ({f x} \<otimes> B))"
+proof
+  show "setify P (f ` A \<otimes> B) \<Longrightarrow> \<forall>x\<in>A. setify P ({f x} \<otimes> B)"
+    by (meson rev_image_eqI sep_algebra.setify_sum sep_algebra_axioms)
+  show "\<forall>x\<in>A. setify P ({f x} \<otimes> B) \<Longrightarrow> setify P (f ` A \<otimes> B)"
+    by (metis (mono_tags, lifting) image_iff sep_algebra.setify_sum sep_algebra_axioms)
+qed
+
+lemma equivI:
+  assumes "A \<ggreater> B"
+    and "B \<ggreater> A"
+    shows "equiv A B"
+  by (simp add: assms(1) assms(2) local.equiv_def)
+
+lemma sub_bigger:
+  assumes "A \<subseteq> B"
+  shows "A \<ggreater> B" 
+  by (meson assms greater_set_def in_mono succ_refl)
+
+lemma larger_set_refl:
+  "A \<ggreater> A"
+  by (simp add: sub_bigger)
+
+
+definition upper_closure where
+  "upper_closure A = { \<phi>' |\<phi>' \<phi>. \<phi>' \<succeq> \<phi> \<and> \<phi> \<in> A }"
+
+
+
+lemma upper_closure_up_closed:
+  "up_closed (upper_closure A)"
+proof (rule up_closedI)
+  fix \<phi>' \<phi>
+  assume asm0: "\<phi>' \<succeq> \<phi> \<and> \<phi> \<in> upper_closure A"
+  then obtain a where "a \<in> A \<and> \<phi> \<succeq> a"
+    using sep_algebra.upper_closure_def sep_algebra_axioms by fastforce
+  then have "\<phi>' \<succeq> a"
+    using asm0 succ_trans by blast
+  then show "\<phi>' \<in> upper_closure A"
+    using \<open>a \<in> A \<and> \<phi> \<succeq> a\<close> upper_closure_def by auto
+qed
+
+
+subsection \<open>Addition of more than two states\<close>
+
+lemma multi_decompose:
+  assumes "multi_plus l \<omega>"
+    shows "length l \<ge> 2 \<Longrightarrow> (\<exists>a b la lb. l = la @ lb \<and> length la > 0 \<and> length lb > 0 \<and> multi_plus la a \<and> multi_plus lb b \<and> Some \<omega> = a \<oplus> b)"
+  using assms
+  apply (rule multi_plus.cases)
+  by auto[2]
+
+
+
+lemma multi_take_drop:
+  assumes "multi_plus l \<omega>"
+      and "length l \<ge> 2"
+    shows "\<exists>n a b. n > 0 \<and> n < length l \<and> multi_plus (take n l) a \<and> multi_plus (drop n l) b \<and> Some \<omega> = a \<oplus> b"
+proof -
+  obtain a b la lb where "l = la @ lb \<and> length la > 0 \<and> length lb > 0 \<and> multi_plus la a \<and> multi_plus lb b \<and> Some \<omega> = a \<oplus> b"
+    using assms(1) assms(2) multi_decompose by blast
+  let ?n = "length la"
+  have "la = take ?n l" 
+    by (simp add: \<open>l = la @ lb \<and> 0 < length la \<and> 0 < length lb \<and> multi_plus la a \<and> multi_plus lb b \<and> Some \<omega> = a \<oplus> b\<close>)
+  moreover have "lb = drop ?n l" 
+    by (simp add: \<open>l = la @ lb \<and> 0 < length la \<and> 0 < length lb \<and> multi_plus la a \<and> multi_plus lb b \<and> Some \<omega> = a \<oplus> b\<close>)
+  ultimately show ?thesis 
+    by (metis \<open>l = la @ lb \<and> 0 < length la \<and> 0 < length lb \<and> multi_plus la a \<and> multi_plus lb b \<and> Some \<omega> = a \<oplus> b\<close> length_drop zero_less_diff)
+qed
+
+lemma multi_plus_single:
+  assumes "multi_plus [v] a"
+  shows "a = v"
+  using assms
+  apply (cases)
+  apply simp
+  by (metis (no_types, lifting) Nil_is_append_conv butlast.simps(2) butlast_append length_greater_0_conv)
+
+lemma multi_plus_two:
+  assumes "length l \<ge> 2"
+  shows "multi_plus l \<omega> \<longleftrightarrow> (\<exists>a b la lb. l = (la @ lb) \<and> length la > 0 \<and> length lb > 0 \<and> multi_plus la a \<and> multi_plus lb b \<and> Some \<omega> = a \<oplus> b)" (is "?A \<longleftrightarrow> ?B")
+  by (meson MPConcat assms multi_decompose)
+
+lemma multi_plus_head_tail:
+  "length l \<le> n \<and> length l \<ge> 2 \<longrightarrow> (multi_plus l \<omega> \<longleftrightarrow> (\<exists>r. Some \<omega> = (List.hd l) \<oplus> r \<and> multi_plus (List.tl l) r))"
+proof (induction n arbitrary: l \<omega>)
+  case 0
+  then show ?case by auto
+next
+  case (Suc n)
+  then have IH: "\<And>(l :: 'a list) \<omega>. length l \<le> n \<and> length l \<ge> 2 \<longrightarrow> multi_plus l \<omega> = (\<exists>r. Some \<omega> = hd l \<oplus> r \<and> multi_plus (tl l) r)"
+    by blast
+  then show ?case
+  proof (cases "n = 0")
+    case True
+    then have "n = 0" by simp
+    then show ?thesis by linarith
+  next
+    case False
+    then have "length (l :: 'a list) \<ge> 2 \<and> length l \<le> n + 1 \<Longrightarrow> multi_plus l \<omega> \<longleftrightarrow> (\<exists>r. Some \<omega> = hd l \<oplus> r \<and> multi_plus (tl l) r)" (is "length l \<ge> 2  \<and> length l \<le> n + 1 \<Longrightarrow> ?A \<longleftrightarrow> ?B")
+    proof -
+      assume asm: "length (l :: 'a list) \<ge> 2 \<and> length l \<le> n + 1"
+      have "?B \<Longrightarrow> ?A"
+      proof -
+        assume "?B"
+        then obtain r where "Some \<omega> = hd l \<oplus> r \<and> multi_plus (tl l) r" by blast
+        then have "multi_plus [hd l] (hd l)" 
+          using MPSingle by blast
+        moreover have "[hd l] @ (tl l) = l" 
+          by (metis Suc_le_length_iff asm append_Cons list.collapse list.simps(3) numeral_2_eq_2 self_append_conv2)
+        ultimately show ?A 
+          by (metis (no_types, lifting) MPConcat Suc_1 Suc_le_mono asm \<open>Some \<omega> = hd l \<oplus> r \<and> multi_plus (tl l) r\<close> append_Nil2 length_Cons length_greater_0_conv list.size(3) not_one_le_zero zero_less_Suc)
+      qed
+      moreover have "?A \<Longrightarrow> ?B"
+      proof -
+        assume ?A
+        then obtain la lb a b where "l = la @ lb" "length la > 0" "length lb > 0" "multi_plus la a" "multi_plus lb b" "Some \<omega> = a \<oplus> b"
+          using asm multi_decompose by blast
+        then have "length la \<le> n \<and> length la \<ge> 2 \<longrightarrow> multi_plus la a = (\<exists>r. Some a = hd la \<oplus> r \<and> multi_plus (tl la) r)"
+          using IH by blast
+        then show ?B
+        proof (cases "length la \<ge> 2")
+          case True
+          then obtain ra where "Some a = (hd la) \<oplus> ra" "multi_plus (tl la) ra"
+            by (metis Suc_eq_plus1 \<open>0 < length lb\<close> \<open>l = la @ lb\<close> \<open>length la \<le> n \<and> 2 \<le> length la \<longrightarrow> multi_plus la a = (\<exists>r. Some a = hd la \<oplus> r \<and> multi_plus (tl la) r)\<close> \<open>multi_plus la a\<close> append_eq_conv_conj asm drop_eq_Nil le_add1 le_less_trans length_append length_greater_0_conv less_Suc_eq_le order.not_eq_order_implies_strict)
+          moreover obtain rab where "Some rab = ra \<oplus> b"
+            by (metis \<open>Some \<omega> = a \<oplus> b\<close> calculation(1) asso2 option.exhaust_sel)
+          then have "multi_plus ((tl la) @ lb) rab" 
+            by (metis (no_types, lifting) Nil_is_append_conv \<open>multi_plus lb b\<close> calculation(2) length_greater_0_conv list.simps(3) multi_plus.cases sep_algebra.MPConcat sep_algebra_axioms)
+          moreover have "Some \<omega> = hd la \<oplus> rab" 
+            by (metis \<open>Some \<omega> = a \<oplus> b\<close> \<open>Some rab = ra \<oplus> b\<close> asso1 calculation(1))
+          ultimately show ?B 
+            using \<open>0 < length la\<close> \<open>l = la @ lb\<close> by auto
+        next
+          case False
+          then have "length la = 1" 
+            using \<open>0 < length la\<close> by linarith
+          then have "la = [a]"
+            by (metis Nitpick.size_list_simp(2) One_nat_def Suc_le_length_iff \<open>multi_plus la a\<close> diff_Suc_1 le_numeral_extra(4) length_0_conv list.sel(3) sep_algebra.multi_plus_single sep_algebra_axioms)
+          then show ?thesis 
+            using \<open>Some \<omega> = a \<oplus> b\<close> \<open>l = la @ lb\<close> \<open>multi_plus lb b\<close> by auto
+        qed
+      qed
+      then show ?thesis using calculation by blast
+    qed
+    then show ?thesis by (metis (no_types, lifting) Suc_eq_plus1)
+  qed
+qed
+
+lemma not_multi_plus_empty:
+  "\<not> multi_plus [] \<omega>"
+  by (metis Nil_is_append_conv length_greater_0_conv list.simps(3) sep_algebra.multi_plus.simps sep_algebra_axioms)
+
+lemma multi_plus_deter:
+  "length l \<le> n \<Longrightarrow> multi_plus l \<omega> \<Longrightarrow> multi_plus l \<omega>' \<Longrightarrow> \<omega> = \<omega>'"
+proof (induction n arbitrary: l \<omega> \<omega>')
+  case 0
+  then show ?case 
+    using multi_plus.cases by auto
+next
+  case (Suc n)
+  then show ?case
+  proof (cases "length l \<ge> 2")
+    case True
+    then obtain r where "Some \<omega> = (List.hd l) \<oplus> r \<and> multi_plus (List.tl l) r"
+      using Suc.prems(2) multi_plus_head_tail by blast
+    moreover obtain r' where "Some \<omega>' = (List.hd l) \<oplus> r' \<and> multi_plus (List.tl l) r'"
+      using Suc.prems(3) True multi_plus_head_tail by blast
+    ultimately have "r = r'" 
+      by (metis Suc.IH Suc.prems(1) drop_Suc drop_eq_Nil)
+    then show ?thesis 
+      by (metis \<open>Some \<omega> = hd l \<oplus> r \<and> multi_plus (tl l) r\<close> \<open>Some \<omega>' = hd l \<oplus> r' \<and> multi_plus (tl l) r'\<close> option.inject)
+  next
+    case False
+    then have "length l \<le> 1" 
+      by simp
+    then show ?thesis
+    proof (cases "length l = 0")
+      case True
+      then show ?thesis
+        using Suc.prems(2) sep_algebra.not_multi_plus_empty sep_algebra_axioms by fastforce
+    next
+      case False
+      then show ?thesis 
+        by (metis One_nat_def Suc.prems(2) Suc.prems(3) Suc_length_conv \<open>length l \<le> 1\<close> le_SucE le_zero_eq length_greater_0_conv less_numeral_extra(3) sep_algebra.multi_plus_single sep_algebra_axioms)
+    qed      
+  qed
+qed
+
+lemma multi_plus_implies_multi_plus_of_drop:
+  assumes "multi_plus l \<omega>"
+      and "n < length l"
+    shows "\<exists>a. multi_plus (drop n l) a \<and> \<omega> \<succeq> a"
+  using assms
+proof (induction n arbitrary: l \<omega>)
+  case 0
+  then show ?case using succ_refl by fastforce
+next
+  case (Suc n)
+  then have "length l \<ge> 2" 
+    by linarith
+  then obtain r where "Some \<omega> = (List.hd l) \<oplus> r \<and> multi_plus (List.tl l) r" 
+    using Suc.prems(1) multi_plus_head_tail by blast
+  then obtain a where "multi_plus (drop n (List.tl l)) a \<and> r \<succeq> a" 
+    using Suc.IH Suc.prems(2) by fastforce
+  then show ?case 
+    by (metis \<open>Some \<omega> = hd l \<oplus> r \<and> multi_plus (tl l) r\<close> bigger_sum_smaller commutative drop_Suc greater_def)
+qed
+
+lemma multi_plus_bigger_than_head:
+  assumes "length l > 0"
+      and "multi_plus l \<omega>"
+    shows "\<omega> \<succeq> List.hd l"
+proof (cases "length l \<ge> 2")
+  case True
+  then obtain r where "Some \<omega> = (List.hd l) \<oplus> r \<and> multi_plus (List.tl l) r" 
+    using assms(1) assms(2) multi_plus_head_tail by blast
+  then show ?thesis 
+    using greater_def by blast
+next
+  case False
+  then show ?thesis
+    by (metis Cons_nth_drop_Suc MPSingle assms(1) assms(2) drop_0 drop_eq_Nil hd_conv_nth length_greater_0_conv not_less_eq_eq numeral_2_eq_2 sep_algebra.multi_plus_deter sep_algebra_axioms succ_refl)
+qed
+
+lemma multi_plus_bigger:
+  assumes "i < length l"
+      and "multi_plus l \<omega>"
+    shows "\<omega> \<succeq> (l ! i)"
+proof -
+  obtain a where "multi_plus (drop i l) a \<and> \<omega> \<succeq> a"
+    using assms(1) assms(2) multi_plus_implies_multi_plus_of_drop order.strict_trans by blast
+  moreover have "List.hd (drop i l) = l ! i" 
+    by (simp add: assms(1) hd_drop_conv_nth)
+  then show ?thesis
+    by (metis (no_types, lifting) succ_trans assms(1) assms(2) drop_eq_Nil leD length_greater_0_conv multi_plus_bigger_than_head multi_plus_implies_multi_plus_of_drop)
+qed
+
+
+lemma sum_then_singleton:
+  "Some a = b \<oplus> c \<longleftrightarrow> {a} = {b} \<otimes> {c}" (is "?A \<longleftrightarrow> ?B")
+proof -
+  have "?A \<Longrightarrow> ?B"
+  proof -
+    assume ?A
+    then have "{a} \<subseteq> {b} \<otimes> {c}"
+      using add_set_elem by auto
+    moreover have "{b} \<otimes> {c} \<subseteq> {a}"
+    proof (rule subsetI)
+      fix x assume "x \<in> {b} \<otimes> {c}"
+      then show "x \<in> {a}"
+        by (metis \<open>Some a = b \<oplus> c\<close> option.sel sep_algebra.add_set_elem sep_algebra_axioms singleton_iff)
+    qed
+    ultimately show ?thesis by blast
+  qed
+  moreover have "?B \<Longrightarrow> ?A" 
+    using add_set_elem by auto
+  ultimately show ?thesis by blast
+qed
+
+lemma empty_set_sum:
+  "{} \<otimes> A = {}" 
+  by (simp add: add_set_def)
+
+
+end
+
+end
diff --git a/thys/Package_logic/document/root.bib b/thys/Package_logic/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Package_logic/document/root.bib
@@ -0,0 +1,47 @@
+
+
+@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}
+}
diff --git a/thys/Package_logic/document/root.tex b/thys/Package_logic/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Package_logic/document/root.tex
@@ -0,0 +1,78 @@
+\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{-\!\!*}}}
+\newcommand{\cwand}{\ensuremath{\mathbin{-\!\!*}_c}}
+\newcommand{\twand}{\ensuremath{\mathbin{-\!\!*}_{\mathcal{T}}}}
+
+\begin{document}
+
+\title{Formalization of a Framework for the Sound Automation of Magic Wands}
+\author{Thibault Dardinier}
+\maketitle
+
+\begin{abstract}
+The magic wand $\wand$ (also called separating implication) is a separation logic~\cite{Reynolds02a} connective % I find it a bit tricky that we talk about the connective and a formula built from it as if these were the same thing
+commonly used to specify properties of partial data structures,
+for instance during iterative traversals.
+A \emph{footprint} of a magic wand formula $A \wand B$ is a state that, combined with any state in which $A$ holds, yields a state in which $B$ holds.
+The key challenge of proving a magic wand (also called \emph{packaging} a wand) is to find such a footprint.
+Existing package algorithms either have a high annotation overhead or are unsound.
+
+In this entry, we formally define a framework for the sound automation of magic wands, described in a paper at CAV~2022~\cite{Dardinier22},
+and prove that it is sound and complete.
+This framework, called the \emph{package logic}, precisely characterises a wide design space of possible package algorithms applicable to a large class of separation logics.
+%Moreover, we define a novel, restricted definition of wands, called \emph{combinable wands}, and prove that it is possible to soundly combine fractions of such wands, which is not the case for arbitrary wands.
+%Finally, we instantiate the package logic to show our framework can also be used with combinable wands.
+\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,680 +1,681 @@
 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
 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
 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