# Theory PackageLogic

```section ‹Package Logic›

text ‹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.›

theory PackageLogic
imports Main SepAlgebra
begin

subsection Definitions

type_synonym 'a abool = "'a ⇒ 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 ⇒ bool"

assumes unit_neutral: "Some a = a ⊕ unit"
and stable_sum: "stable a ⟹ stable b ⟹ Some x = a ⊕ b ⟹ stable x"
and stable_unit: "stable unit"

begin

fun sat :: "'a aassertion ⇒ 'a ⇒ bool" where
"sat (AStar A B) φ ⟷ (∃a b. Some φ = a ⊕ b ∧ sat A a ∧ sat B b)"
| "sat (AImp b A) φ ⟷ (b φ ⟶ sat A φ)"
| "sat (ASem A) φ ⟷ A φ"

definition mono_pure_cond where
"mono_pure_cond b ⟷ (∀φ. b φ ⟷ b |φ| ) ∧ (∀φ' φ r. pure r ∧ Some φ' = φ ⊕ r ∧ ¬ b φ ⟶ ¬ b φ')"

definition bool_conj where
"bool_conj a b x ⟷ a x ∧ b x"

type_synonym 'c pruner = "'c ⇒ bool"

(* Only positively, so not-well defined = false *)
definition mono_pruner :: "'a pruner ⇒ bool" where
"mono_pruner p ⟷ (∀φ' φ r. pure r ∧ p φ ∧ Some φ' = φ ⊕ r ⟶ p φ')"
(* opposite of mono_cond *)

fun wf_assertion where
"wf_assertion (AStar A B) ⟷ wf_assertion A ∧ wf_assertion B"
| "wf_assertion (AImp b A) ⟷ mono_pure_cond b ∧ wf_assertion A"
| "wf_assertion (ASem A) ⟷ mono_pruner A"

type_synonym 'c transformer = "'c ⇒ 'c"

type_synonym 'c ext_state = "'c × 'c × 'c transformer"

inductive package_rhs ::
"'a ⇒ 'a ⇒ 'a ext_state set ⇒ 'a abool ⇒ 'a aassertion ⇒ 'a ⇒ 'a ⇒ 'a ext_state set ⇒ bool" where

AStar: "⟦ package_rhs φ f S pc A φ' f' S' ; package_rhs φ' f' S' pc B φ'' f'' S'' ⟧ ⟹ package_rhs φ f S pc (AStar A B) φ'' f'' S''"
| AImp: "package_rhs φ f S (bool_conj pc b) A φ' f' S' ⟹ package_rhs φ f S pc (AImp b A) φ' f' S'"
(* witness means we *choose* how we satisfy B *)
| ASem: "⟦ ⋀a u T b. (a, u, T) ∈ S ⟹ pc a ⟹ b = witness (a, u, T) ⟹ a ≽ b ∧ B b ;
S' = { (a, u, T) |a u T. (a, u, T) ∈ S ∧ ¬ pc a }
∪ { (a ⊖ b, the (u ⊕ b), T) |a u T b. (a, u, T) ∈ S ∧ pc a ∧ b = witness (a, u, T) } ⟧
⟹ package_rhs φ f S pc (ASem B) φ f S'"

| AddFromOutside: "⟦ Some φ = φ' ⊕ m ; package_rhs φ' f' S' pc A φ'' f'' S'' ; stable m ; Some f' = f ⊕ m ;
S' = { (r, u, T) |a u T r. (a, u, T) ∈ S ∧ Some r = a ⊕ (T f' ⊖ T f)  ∧ r ## u } ⟧
⟹ package_rhs φ f S pc A φ'' f'' S''"

definition package_sat where
"package_sat pc A a' u' u ⟷ (pc |a'| ⟶ (∃x. Some x = |a'| ⊕ (u' ⊖ u ) ∧ sat A x))"

definition package_rhs_connection :: "'a ⇒ 'a ⇒ 'a ext_state set ⇒ 'a abool ⇒ 'a aassertion ⇒ 'a ⇒ 'a ⇒ 'a ext_state set ⇒ bool" where
"package_rhs_connection φ f S pc A φ' f' S' ⟷ f' ≽ f ∧ φ ## f ∧ φ ⊕ f = φ' ⊕ f' ∧ stable f' ∧
(∀(a, u, T) ∈ S. ∃au. Some au = a ⊕ u ∧ (au ## (T f' ⊖ T f) ⟶
(∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc A a' u' u)))"

definition mono_transformer :: "'a transformer ⇒ bool" where
"mono_transformer T ⟷ (∀φ φ'. φ' ≽ φ ⟶ T φ' ≽ T φ) ∧ T unit = unit"

definition valid_package_set where
"valid_package_set S f ⟷ (∀(a, u, T) ∈ S. a ## u ∧ |a| ≽ |u| ∧ mono_transformer T ∧ a ≽ |T f| )"

definition intuitionistic where
"intuitionistic A ⟷ (∀φ' φ. φ' ≽ φ ∧ A φ ⟶ A φ')"

definition pure_remains where
"pure_remains S ⟷ (∀(a, u, p) ∈ S. pure a)"

definition is_footprint_general :: "'a ⇒ ('a ⇒ 'a ⇒ 'a) ⇒ 'a aassertion ⇒ 'a aassertion ⇒ bool" where
"is_footprint_general w R A B ⟷ (∀a b. sat A a ∧ Some b = a ⊕ R a w ⟶ sat B b)"

definition is_footprint_standard :: "'a ⇒ 'a aassertion ⇒ 'a aassertion ⇒ bool" where
"is_footprint_standard w A B ⟷ (∀a b. sat A a ∧ Some b = a ⊕ w ⟶ sat B b)"

subsection Lemmas

lemma is_footprint_generalI:
assumes "⋀a b. sat A a ∧ Some b = a ⊕ R a w ⟹ sat B b"
shows "is_footprint_general w R A B"
using assms is_footprint_general_def by blast

lemma is_footprint_standardI:
assumes "⋀a b. sat A a ∧ Some b = a ⊕ w ⟹ sat B b"
shows "is_footprint_standard w A B"
using assms is_footprint_standard_def by blast

lemma mono_pure_condI:
assumes "⋀φ. b φ ⟷ b |φ|"
and "⋀φ φ' r. pure r ∧ Some φ' = φ ⊕ r ∧ ¬ b φ ⟹ ¬ b φ'"
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 "⋀φ. bool_conj pc b φ = bool_conj pc b  |φ|"
by (metis assms(1) assms(2) bool_conj_def mono_pure_cond_def)
show "⋀φ φ' r. pure r ∧ Some φ' = φ ⊕ r ∧ ¬ bool_conj pc b φ ⟹ ¬ bool_conj pc b φ'"
by (metis assms(1) assms(2) bool_conj_def mono_pure_cond_def)
qed

lemma bigger_sum:
assumes "Some φ = a ⊕ b"
and "φ' ≽ φ"
shows "∃b'. b' ≽ b ∧ Some φ' = a ⊕ b'"
proof -
obtain r where "Some φ' = φ ⊕ r"
using assms(2) greater_def by blast
then obtain b' where "Some b' = b ⊕ r"
by (metis assms(1) asso2 domD domI domIff)
then show ?thesis
by (metis ‹Some φ' = φ ⊕ r› 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 φ"
and "Some φ' = φ ⊕ r"
and "pure r"
shows "sat A φ'"
using assms
proof (induct arbitrary: φ φ' r rule: wf_assertion.induct)
case (1 A B)
then obtain a b where "Some φ = a ⊕ b" "sat A a" "sat B b" by (meson sat.simps(1))
then obtain b' where "Some b' = b ⊕ r"
by (metis "1.prems"(3) asso2 option.collapse)
moreover obtain a' where "Some a' = a ⊕ r"
by (metis "1.prems"(3) ‹Some φ = a ⊕ b› asso2 commutative option.collapse)
ultimately show ?case
using 1
by (metis ‹Some φ = a ⊕ b› ‹sat A a› ‹sat B b› 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'| ⟹ (∃x. Some x = |a'| ⊕ (u' ⊖ u ) ∧ sat A x)"
shows "package_sat pc A a' u' u"

lemma package_rhs_connection_instantiate:
assumes "package_rhs_connection φ f S pc A φ' f' S'"
and "(a, u, T) ∈ S"
obtains au where "Some au = a ⊕ u"
and "au ## (T f' ⊖ T f) ⟹ ∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc A a' u' u"
using assms(1) assms(2) package_rhs_connection_def by fastforce

lemma package_rhs_connectionI:
assumes "φ ⊕ f = φ' ⊕ f'"
and "stable f'"
and "φ ## f"
and "f' ≽ f"
and "⋀a u T. (a, u, T) ∈ S ⟹ (∃au. Some au = a ⊕ u ∧ (au ## (T f' ⊖ T f) ⟶
(∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f' ⊖ T f) = a' ⊕ u'∧ u' ≽ u ∧ package_sat pc A a' u' u)))"
shows "package_rhs_connection φ f S pc A φ' f' S'"
using package_rhs_connection_def assms by auto

lemma valid_package_setI:
assumes "⋀a u T. (a, u, T) ∈ S ⟹ a ## u ∧ |a| ≽ |u| ∧ mono_transformer T ∧ a ≽ |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 ⊕ y"
and "Some a' = a ⊕ x"
shows "a' ## y"
by (metis assms defined_def sep_algebra.asso1 sep_algebra_axioms)

lemma bigger_core_sum_defined:
assumes "|a| ≽ b"
shows "Some a = a ⊕ 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 φ f S pc A φ' f' S'"
and "valid_package_set S f"
and "wf_assertion A"
and "mono_pure_cond pc"
and "stable f"
and "φ ## f"
shows "package_rhs_connection φ f S pc A φ' f' S' ∧ valid_package_set S' f'"
using assms
proof (induct rule: package_rhs.induct)
case (AImp φ f S pc b A φ' f' S')
then have asm0: "package_rhs_connection φ f S (bool_conj pc b) A φ' f' S' ∧ valid_package_set S' f'"
using mono_pure_cond_conj wf_assertion.simps(2) by blast
let ?pc = "bool_conj pc b"
obtain "φ ⊕ f = φ' ⊕ f'" "stable f'" "φ ## f" "f' ≽ f"
and §: "⋀a u T. (a, u, T) ∈ S ⟹ (∃au. Some au = a ⊕ u ∧ (au ## (T f' ⊖ T f) ⟶
(∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat ?pc A a' u' u)))"
using asm0 package_rhs_connection_def by force

have "package_rhs_connection φ f S pc (AImp b A) φ' f' S'"
proof (rule package_rhs_connectionI)
show "φ ## f"
by (simp add: ‹φ ## f›)
show "φ ⊕ f = φ' ⊕ f'" by (simp add: ‹φ ⊕ f = φ' ⊕ f'›)
show "stable f'" using ‹stable f'› by simp
show "f' ≽ f" by (simp add: ‹f' ≽ f›)
fix a u T assume asm1: "(a, u, T) ∈ S"
then obtain au where asm2: "Some au = a ⊕ u ∧ (au ## (T f' ⊖ T f) ⟶
(∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat ?pc A a' u' u))"
using § by presburger

then have "au ## (T f' ⊖ T f) ⟹
(∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc (AImp b A) a' u' u)"
proof -
assume asm3: "au ## (T f' ⊖ T f)"
then obtain a' u' where au': "(a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat ?pc A a' u' u"
using asm2 by blast
have "(the ( |a'| ⊕ (u' ⊖ u))) ≽ |a'|"
proof -
have "u' ≽ u' ⊖ u"
by (metis minus_default minus_smaller succ_refl)
then have "a' ## (u' ⊖ 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 "∃x. Some x = |a'| ⊕ (u' ⊖ u) ∧ sat (AImp b A) x"
proof (cases "b |a'|")
case True
then have "?pc |a'|"
by (simp add: ‹pc |a'|› 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 "¬ b (the ( |a'| ⊕ (u' ⊖ u)))"
using AImp.prems(2) ‹the ( |a'| ⊕ (u' ⊖ u)) ≽ |a'|› 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'| ⊕ (u' ⊖ 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 "∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc (AImp b A) a' u' u"
using au' by blast
qed
then show "∃au. Some au = a ⊕ u ∧ (au ## (T f' ⊖ T f) ⟶ (∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc (AImp b A) a' u' u))"
using asm2 by auto
qed
then show ?case
using ‹package_rhs_connection φ f S (bool_conj pc b) A φ' f' S' ∧ valid_package_set S' f'› by blast
next
case (AStar φ f S pc A φ' f' S' B φ'' f'' S'')
then have r1: "package_rhs_connection φ f S pc A φ' f' S' ∧ valid_package_set S' f'"
using wf_assertion.simps(1) by blast
moreover have "φ' ## f'" using r1 package_rhs_connection_def[of φ f S pc A φ' f' S'] defined_def
by fastforce
ultimately have r2: "package_rhs_connection φ' f' S' pc B φ'' f'' S'' ∧ 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: "φ ⊕ f = φ' ⊕ f'" "stable f'" "φ ## f" "f' ≽ f"
and **: "⋀a u T. (a, u, T) ∈ S ⟹ (∃au. Some au = a ⊕ u ∧ (au ## (T f' ⊖ T f) ⟶
(∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc A a' u' u)))"
using r1 package_rhs_connection_def by fastforce
then obtain fb_def: "φ' ⊕ f' = φ'' ⊕ f''" "stable f''" "φ' ## f'" "f'' ≽ f'"
and "⋀a u T. (a, u, T) ∈ S' ⟹ (∃au. Some au = a ⊕ u ∧ (au ## (T f'' ⊖ T f') ⟶
(∃a' u'. (a', u', T) ∈ S'' ∧ |a'| ≽ |a| ∧ au ⊕ (T f'' ⊖ T f') = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc B a' u' u)))"
using r2 package_rhs_connection_def by fastforce

moreover have "package_rhs_connection φ f S pc (AStar A B) φ'' f'' S''"
proof (rule package_rhs_connectionI)
show "φ ⊕ f = φ'' ⊕ f''" by (simp add: fa_def(1) fb_def(1))
show "stable f''" by (simp add: fb_def(2))
show "φ ## f" using fa_def(3) by auto
show "f'' ≽ f" using fa_def(4) fb_def(4) succ_trans by blast

fix a u T assume asm0: "(a, u, T) ∈ S"
then have f_def: "Some (T f'' ⊖ T f) = (T f'' ⊖ T f') ⊕ (T f' ⊖ T f)"
proof -
have "mono_transformer T" using valid_package_set_def asm0 ‹valid_package_set S f› by fastforce
then have "T f'' ≽ T f'"
moreover have "T f' ≽ T f"
using ‹mono_transformer T› 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 ⊕ u"
"au ## (T f' ⊖ T f) ⟹ (∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc A a' u' u)"
using ** asm0 by blast
then show "∃au. Some au = a ⊕ u ∧ (au ## (T f'' ⊖ T f) ⟶ (∃a' u'. (a', u', T) ∈ S'' ∧ |a'| ≽ |a| ∧ au ⊕ (T f'' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc (AStar A B) a' u' u))"
proof (cases "au ## (T f'' ⊖ T f)")
case True
moreover have "mono_transformer T" using ‹valid_package_set S f› valid_package_set_def asm0 by fastforce
ultimately have "au ## (T f'' ⊖ T f') ∧ au ## (T f' ⊖ T f)" using asso3 commutative defined_def f_def
by metis
then obtain a' u' where r3: "(a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc A a' u' u"
using au_def(2) by blast

then obtain au' where au'_def: "Some au' = a' ⊕ u'"
"au' ## (T f'' ⊖ T f') ⟹ (∃a'' u''. (a'', u'', T) ∈ S'' ∧ |a''| ≽ |a'| ∧ au' ⊕ (T f'' ⊖ T f') = a'' ⊕ u'' ∧ u'' ≽ u' ∧ package_sat pc B a'' u'' u')"
by (meson package_logic.package_rhs_connection_instantiate package_logic_axioms r2)
moreover have "au' ## T f'' ⊖ T f'"
using True r3 calculation(1) commutative defined_sum_move f_def by fastforce
ultimately obtain a'' u'' where r4: "(a'', u'', T) ∈ S'' ∧ |a''| ≽ |a'| ∧ au' ⊕ (T f'' ⊖ T f') = a'' ⊕ u'' ∧ u'' ≽ u' ∧ package_sat pc B a'' u'' u'"
by blast

then have "au ⊕ (T f'' ⊖ T f) = a'' ⊕ u''"
proof -
have "au ⊕ (T f'' ⊖ T f) = splus (Some au) (Some (T f'' ⊖ T f))"
by simp
also have "... = splus (Some au) (splus (Some (T f'' ⊖ T f')) (Some (T f' ⊖ T f)))"
using f_def by auto
finally show ?thesis
by (metis (full_types) r3 r4 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) r4 greater_equiv minus_core minus_core_weaker minus_equiv_def mono_pure_cond_def pure_def)
then obtain x where "Some x = |a'| ⊕ (u' ⊖ u) ∧ sat A x"
using r3 package_sat_def by fastforce
then obtain x' where "Some x' = |a''| ⊕ (u'' ⊖ u') ∧ sat B x'"
using ‹pc |a''|› package_sat_def r4 by presburger

have "u'' ≽ u'' ⊖ u"
by (metis minus_default minus_smaller succ_refl)
moreover have "a'' ## u''"
using True ‹au ⊕ (T f'' ⊖ T f) = a'' ⊕ u''› defined_def by auto
ultimately obtain x'' where "Some x'' = |a''| ⊕ (u'' ⊖ u)"
by (metis commutative defined_def max_projection_prop_pure_core mpp_smaller not_None_eq smaller_compatible)
moreover have "Some (u'' ⊖ u) = (u'' ⊖ u') ⊕ (u' ⊖ u)"
using r4 ‹(a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc A a' u' u› commutative minus_and_plus minus_equiv_def by presburger
moreover have "|a''| ≽ |a'|"
using r4 by blast
moreover have "Some |a''| = |a'| ⊕ |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' ⊕ x"
using asso1[of _ _ x'] ‹Some x = |a'| ⊕ (u' ⊖ u) ∧ sat A x› ‹Some x' = |a''| ⊕ (u'' ⊖ u') ∧ sat B x'›  commutative
by metis
then show "∃x. Some x = |a''| ⊕ (u'' ⊖ u) ∧ sat (AStar A B) x"
using ‹Some x = |a'| ⊕ (u' ⊖ u) ∧ sat A x› ‹Some x' = |a''| ⊕ (u'' ⊖ u') ∧ sat B x'› ‹Some x'' = |a''| ⊕ (u'' ⊖ u)› commutative by fastforce
qed
ultimately show ?thesis
using r3 r4 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' φ f)
have "valid_package_set S' f"
proof (rule valid_package_setI)
fix a' u' T assume asm0: "(a', u', T) ∈ S'"
then show "a' ## u' ∧ |a'| ≽ |u'| ∧ mono_transformer T ∧ a' ≽ |T f|"
proof (cases "(a', u', T) ∈ S")
case True
then show ?thesis
using ASem.prems(1) valid_package_set_def by auto
next
case False
then have "(a', u', T) ∈ {(a ⊖ b, the (u ⊕ b), T) |a u T b. (a, u, T) ∈ S ∧ pc a ∧ b = witness (a, u, T)}"
using ASem.hyps(2) asm0 by blast
then obtain a u b where "(a, u, T) ∈ S" "pc a" "b = witness (a, u, T)" "a' = a ⊖ b" "u' = the (u ⊕ b)" by blast
then have "a ≽ b ∧ B b"
using ASem.hyps(1) by presburger
have "a ## u"
using ASem.prems(1) ‹(a, u, T) ∈ S› valid_package_set_def by fastforce
then have "Some u' = u ⊕ b"
by (metis ‹a ≽ b ∧ B b› ‹u' = the (u ⊕ b)› commutative defined_def option.exhaust_sel smaller_compatible)
moreover have "Some a = a' ⊕ b"
using ‹a ≽ b ∧ B b› ‹a' = a ⊖ b› commutative minus_equiv_def by presburger

ultimately have "a' ## u'"
by (metis ‹a ## u› asso1 commutative defined_def)
moreover have "|a'| ≽ |u'|"
proof -
have "|a| ≽ |u|"
using ASem.prems(1) ‹(a, u, T) ∈ S› valid_package_set_def by fastforce
moreover have "|a'| ≽ |a|"
by (simp add: ‹a' = a ⊖ b› minus_core succ_refl)
moreover have "|a'| ≽ |b|"
using ‹a ≽ b ∧ B b› ‹a' = a ⊖ b› max_projection_prop_pure_core minus_core mpp_mono by presburger
ultimately show ?thesis
by (metis ‹Some u' = u ⊕ b› ‹a' = a ⊖ b› core_is_pure core_sum minus_core pure_def smaller_pure_sum_smaller)
qed
moreover have "a' ≽ |T f|"
proof -
have "a ≽ |T f|" using ‹(a, u, T) ∈ S› ‹valid_package_set S f› valid_package_set_def
by fastforce
then show ?thesis
by (metis ‹a' = a ⊖ b› 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 ‹(a, u, T) ∈ S› ‹valid_package_set S f› valid_package_set_def
by fastforce
qed
qed
moreover have "package_rhs_connection φ f S pc (ASem B) φ f S'"
proof (rule package_rhs_connectionI)
show "φ ⊕ f = φ ⊕ f"
by simp
show "stable f" by (simp add: ASem.prems(4))
show "φ ## f" by (simp add: ASem.prems(5))
show "f ≽ f" by (simp add: succ_refl)

fix a u T assume asm0: "(a, u, T) ∈ S"

then obtain au where "Some au = a ⊕ u" using ‹valid_package_set S f› valid_package_set_def defined_def by auto
then have r0: "(∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ Some au = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc (ASem B) a' u' u)"
proof -
let ?b = "witness (a, u, T)"
let ?a = "a ⊖ ?b"
let ?u = "the (u ⊕ ?b)"
show "∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ Some au = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc (ASem B) a' u' u"
proof (cases "pc a")
case True
then have "(?a, ?u, T) ∈ S'" using ASem.hyps(2) asm0 by blast
then have "a ≽ ?b ∧ B ?b" using ASem.hyps(1) True asm0 by blast
moreover have r1: "(?a, ?u, T) ∈ S' ∧ |?a| ≽ |a| ∧ Some au = ?a ⊕ ?u ∧ ?u ≽ u"
proof
show "(a ⊖ witness (a, u, T), the (u ⊕ witness (a, u, T)), T) ∈ S'"
by (simp add: ‹(a ⊖ witness (a, u, T), the (u ⊕ witness (a, u, T)), T) ∈ S'›)
have "|a ⊖ witness (a, u, T)|  ≽  |a| "
moreover have "Some au = a ⊖ witness (a, u, T) ⊕ the (u ⊕ witness (a, u, T))"
using ‹Some au = a ⊕ u› ‹a ≽ witness (a, u, T) ∧ B (witness (a, u, T))›
asso1[of "a ⊖ witness (a, u, T)" "witness (a, u, T)" a u "the (u ⊕ witness (a, u, T))"]
commutative option.distinct(1) option.exhaust_sel asso3 minus_equiv_def
by metis
moreover have "the (u ⊕ witness (a, u, T)) ≽ u"
using ‹Some au = a ⊕ u› ‹a ≽ witness (a, u, T) ∧ B (witness (a, u, T))› commutative
greater_def option.distinct(1) option.exhaust_sel asso3[of u "witness (a, u, T)" ]
by metis
ultimately show "|a ⊖ witness (a, u, T)|  ≽  |a|  ∧ Some au = a ⊖ witness (a, u, T) ⊕ the (u ⊕ witness (a, u, T)) ∧ the (u ⊕ witness (a, u, T)) ≽ u"
by blast
qed
moreover have "package_sat pc (ASem B) ?a ?u u"
proof (rule package_satI)
assume "pc |a ⊖ witness (a, u, T)|"
have "Some ?u = u ⊕ ?b"
by (metis (no_types, lifting) ‹Some au = a ⊕ u› calculation(1) commutative minus_equiv_def option.distinct(1) option.exhaust_sel sep_algebra.asso3 sep_algebra_axioms)
moreover have "?a ## ?u"
by (metis r1 defined_def option.distinct(1))
moreover have "?u ≽ ?u ⊖ u"
using r1 minus_smaller by blast
ultimately obtain x where "Some x = |a ⊖ ?b| ⊕ (?u ⊖ u)"
by (metis (no_types, opaque_lifting) ‹a ≽ witness (a, u, T) ∧ B (witness (a, u, T))› commutative defined_def minus_core minus_equiv_def option.exhaust smaller_compatible)
moreover have "x ≽ ?b"
proof -
have "?u ⊖ u ≽ ?b"
using ‹Some (the (u ⊕ witness (a, u, T))) = u ⊕ witness (a, u, T)› minus_bigger by blast
then show ?thesis
using calculation greater_equiv succ_trans by blast
qed
ultimately show "∃x. Some x = |a ⊖ witness (a, u, T)| ⊕ (the (u ⊕ witness (a, u, T)) ⊖ u) ∧ sat (ASem B) x"
using ASem.prems(2) ‹Some (the (u ⊕ witness (a, u, T))) = u ⊕ witness (a, u, T)›
‹a ≽ witness (a, u, T) ∧ B (witness (a, u, T))› 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) ∈ S'"
using False ASem.hyps(2) asm0 by blast
ultimately show ?thesis
using ‹Some au = a ⊕ u› succ_refl by blast
qed
qed
moreover have "au ⊕ (T f ⊖ T f) = Some au"
proof -
have "a ≽ |T f|" using ‹(a, u, T) ∈ S› ‹valid_package_set S f› valid_package_set_def by fastforce
then have "|a| ≽ T f ⊖ T f"
using core_is_smaller max_projection_prop_def max_projection_prop_pure_core minusI by presburger
then have "|au| ≽ T f ⊖ T f"
using ‹Some au = a ⊕ u› core_sum greater_def succ_trans by blast
then show ?thesis using bigger_core_sum_defined by force
qed
ultimately show "∃au. Some au = a ⊕ u ∧ (au ## (T f ⊖ T f) ⟶ (∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc (ASem B) a' u' u))"
using ‹Some au = a ⊕ u› by fastforce
qed
ultimately show ?case by blast
next
case (AddFromOutside φ φ' m f' S' pc A φ'' f'' S'' f S)
have "valid_package_set S' f'"
proof (rule valid_package_setI)
fix a' u T assume asm0: "(a', u, T) ∈ S'"
then obtain a where "(a, u, T) ∈ S" "a' ## u" "Some a' = a ⊕ (T f' ⊖ T f)"
then have "|a| ≽ |u| ∧ mono_transformer T ∧ a ≽ |T f|" using ‹valid_package_set S f› valid_package_set_def
by fastforce
moreover have "a' ≽ |T f'|"
by (metis (no_types, opaque_lifting) ‹Some a' = a ⊕ (T f' ⊖ T f)› commutative greater_equiv minus_core minus_equiv_def minus_smaller succ_trans unit_neutral)
ultimately show "a' ## u ∧ |a'| ≽ |u| ∧ mono_transformer T ∧ a' ≽ |T f'|"
using ‹Some a' = a ⊕ (T f' ⊖ T f)› ‹a' ## u› greater_def max_projection_prop_pure_core mpp_mono succ_trans by blast
qed
then have r: "package_rhs_connection φ' f' S' pc A φ'' f'' S'' ∧ valid_package_set S'' f''"
then obtain r2: "φ' ⊕ f' = φ'' ⊕ f''" "stable f''" "φ' ## f'" "f'' ≽ f'"
"⋀a u T. (a, u, T) ∈ S' ⟹ (∃au. Some au = a ⊕ u ∧ (au ## (T f'' ⊖ T f') ⟶
(∃a' u'. (a', u', T) ∈ S'' ∧ |a'| ≽ |a| ∧ au ⊕ (T f'' ⊖ T f') = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc A a' u' u)))"
using package_rhs_connection_def by fastforce

moreover have "package_rhs_connection φ f S pc A φ'' f'' S''"
proof (rule package_rhs_connectionI)
show "φ ⊕ f = φ'' ⊕ f''"
show "stable f''"
using AddFromOutside.hyps(4) calculation(4) r2(2) stable_sum by blast
show "φ ## f"
show "f'' ≽ f"
using AddFromOutside.hyps(5) bigger_sum greater_def r2(4) by blast

fix a u T
assume asm0: "(a, u, T) ∈ S"
then obtain au where "Some au = a ⊕ u" using ‹valid_package_set S f› valid_package_set_def defined_def
by fastforce
moreover have "au ## (T f'' ⊖ T f) ⟹ (∃a' u'. (a', u', T) ∈ S'' ∧ |a'| ≽ |a| ∧ au ⊕ (T f'' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc A a' u' u)"
proof -
assume asm1: "au ## (T f'' ⊖ T f)"
moreover have "mono_transformer T" using ‹valid_package_set S f› valid_package_set_def asm0
by fastforce
then have "Some (T f'' ⊖ T f) = (T f'' ⊖ T f') ⊕ (T f' ⊖ 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' ⊖ T f)"
using ‹Some au = a ⊕ u› asso2 commutative defined_def minus_exists
by metis
then obtain a' where "Some a' = a ⊕ (T f' ⊖ T f)"
by (meson defined_def option.collapse)
moreover have "a' ## u"
proof -
have "T f'' ⊖ T f ≽ T f' ⊖ T f"
using ‹Some (T f'' ⊖ T f) = T f'' ⊖ T f' ⊕ (T f' ⊖ T f)› greater_equiv by blast
then show ?thesis
using ‹Some au = a ⊕ u› asm1 asso1[of u a au "T f' ⊖ T f" a'] asso2[of ] calculation commutative
defined_def[of ] greater_equiv[of "T f'' ⊖ T f" "T f' ⊖ T f"]
by metis
qed

ultimately have "(a', u, T) ∈ S'"

moreover have "au ## (T f'' ⊖ T f')"
by (metis ‹Some (T f'' ⊖ T f) = T f'' ⊖ T f' ⊕ (T f' ⊖ T f)› asm1 asso3 defined_def)

then have "∃au. Some au = a' ⊕ u ∧ (au ## (T f'' ⊖ T f') ⟶ (∃a'a u'. (a'a, u', T) ∈ S'' ∧ |a'a| ≽ |a'| ∧ au ⊕ (T f'' ⊖ T f') = a'a ⊕ u' ∧ u' ≽ u ∧ package_sat pc A a'a u' u))"
using r2(5) calculation by blast

then obtain au' a'' u' where r3: "Some au' = a' ⊕ u" "au' ## (T f'' ⊖ T f') ⟹ (a'', u', T) ∈ S'' ∧ |a''| ≽ |a'| ∧ au' ⊕ (T f'' ⊖ T f') = a'' ⊕ u' ∧ u' ≽ u ∧ package_sat pc A a'' u' u"
using ‹au ## (T f'' ⊖ T f')› by blast
moreover have "au' ## (T f'' ⊖ T f')" using ‹au ## (T f'' ⊖ T f)› ‹Some au = a ⊕ u› r3(1)
‹Some (T f'' ⊖ T f) = (T f'' ⊖ T f') ⊕ (T f' ⊖ T f)›
‹Some a' = a ⊕ (T f' ⊖ T f)› asso1[of u a au "T f' ⊖ T f" a'] commutative defined_sum_move[of au "T f'' ⊖ T f"]
by metis
ultimately have r4: "(a'', u', T) ∈ S'' ∧ |a''| ≽ |a'| ∧ au' ⊕ (T f'' ⊖ T f') = a'' ⊕ u' ∧ u' ≽ u ∧ package_sat pc A a'' u' u"
by blast
moreover have "|a''| ≽ |a|"
proof -
have "|a'| ≽ |a|"
using ‹Some a' = a ⊕ (T f' ⊖ T f)› core_sum greater_def by blast
then show ?thesis
using r4 succ_trans by blast
qed
ultimately show "∃a' u'. (a', u', T) ∈ S'' ∧ |a'| ≽ |a| ∧ au ⊕ (T f'' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat pc A a' u' u"
using ‹Some (T f'' ⊖ T f) = T f'' ⊖ T f' ⊕ (T f' ⊖ T f)› ‹Some a' = a ⊕ (T f' ⊖ T f)› ‹Some au = a ⊕ u›
commutative r3(1) asso1 splus.simps(3) splus_asso by metis
qed
ultimately show "∃au. Some au = a ⊕ u ∧ (au ## (T f'' ⊖ T f) ⟶ (∃a' u'. (a', u', T) ∈ S'' ∧ |a'| ≽ |a| ∧ au ⊕ (T f'' ⊖ T f) = a' ⊕ u' ∧ u' ≽ u ∧ 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:
"φ ≽ unit"
using greater_equiv unit_neutral by auto

subsection ‹Lemmas for completeness›

lemma sat_star_exists_bigger:
assumes "sat (AStar A B) φ"
and "wf_assertion A"
and "wf_assertion B"
shows "∃a b. |a| ≽ |φ| ∧ |b| ≽ |φ| ∧ Some φ = a ⊕ b ∧ sat A a ∧ sat B b"
proof -
obtain a b where "Some φ = a ⊕ b" "sat A a" "sat B b"
using assms sat.simps(1) by blast
then obtain a' b' where "Some a' = a ⊕ |φ|" "Some b' = b ⊕ |φ|"
by (meson defined_def greater_def greater_equiv option.collapse smaller_compatible_core)
then have "a' ≽ a ∧ b' ≽ b"
using greater_def by blast
then have "sat A a' ∧ sat B b'"
by (metis ‹Some a' = a ⊕ |φ|› ‹Some b' = b ⊕ |φ|› ‹sat A a› ‹sat B b› assms(2) assms(3) max_projection_prop_pure_core mpp_prop package_logic.wf_assertion_sat_larger_pure package_logic_axioms)
moreover have "Some φ = a' ⊕ b'"
by (metis (no_types, lifting) ‹Some φ = a ⊕ b› ‹Some a' = a ⊕ |φ|› ‹Some b' = b ⊕ |φ|› asso1 commutative core_is_smaller)
ultimately show ?thesis
by (metis ‹Some a' = a ⊕ |φ|› ‹Some b' = b ⊕ |φ|› commutative extract_core greater_equiv max_projection_prop_pure_core mpp_mono)
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 ≽ b"
and "Some b = b1 ⊕ b2"
shows "∃r. Some a = r ⊕ b2 ∧ |r| ≽ |a| ∧ r ≽ b1"
proof -
obtain r where "Some a = r ⊕ b2 ∧ r ≽ b1"
by (metis assms(1) assms(2) bigger_sum commutative)
then obtain r' where "Some r' = r ⊕ |a|"
by (metis defined_def greater_def option.exhaust smaller_compatible_core)
then have "Some a = r' ⊕ b2"
by (metis ‹Some a = r ⊕ b2 ∧ r ≽ b1› commutative core_is_smaller sep_algebra.asso1 sep_algebra_axioms)
then show ?thesis
by (metis ‹Some a = r ⊕ b2 ∧ r ≽ b1› ‹Some r' = r ⊕ |a|› core_is_pure greater_def smaller_than_core succ_trans)
qed

lemma bigger_the:
assumes "Some a = x' ⊕ y"
and "x' ≽ x"
shows "the (   |a|  ⊕  x') ≽ the (   |a|  ⊕ x)"
proof -
have "a ≽ 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| ⊕ 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 ≽ b"
shows "Some a = b ⊕ (a ⊖ b)"
using assms commutative minus_equiv_def by force

lemma core_mono:
assumes "a ≽ b"
shows "|a| ≽ |b|"
using assms max_projection_prop_pure_core mpp_mono by auto

lemma prove_last_completeness:
assumes "a' ≽ a"
and "Some a = nf1 ⊕ f2"
shows "a' ⊖ nf1 ≽ f2"
by (meson assms(1) assms(2) greater_def greater_minus_trans minus_bigger succ_trans)

lemma completeness_aux:
assumes "⋀a u T. (a, u, T) ∈ S ⟹ |f1 a u T| ≽ |a| ∧ Some a = f1 a u T ⊕ f2 a u T ∧ (pc |a| ⟶ sat A (the ( |a| ⊕ (f1 a u T))))"
and "valid_package_set S f"
and "wf_assertion A"
and "mono_pure_cond pc"
and "stable f ∧ φ ## f"
shows "∃S'. package_rhs φ f S pc A φ f S' ∧ (∀(a', u', T) ∈ S'. ∃a u. (a, u, T) ∈ S ∧ a' ≽ f2 a u T ∧ |a'| = |a| )"
using assms
proof (induct A arbitrary: S pc f1 f2)
case (AImp b A)
let ?pc = "bool_conj pc b"

have r0: "∃S'. package_rhs φ f S (bool_conj pc b) A φ f S' ∧ (∀a∈S'. case a of (a', u', T) ⇒ ∃a u. (a, u, T) ∈ S ∧ a' ≽ f2 a u T ∧ |a'| = |a| )"
proof (rule AImp(1))
show "valid_package_set S f"
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 ∧ φ ## f" using ‹stable f ∧ φ ## f› by simp

fix a u T
assume asm0: "(a, u, T) ∈ S"
then have "Some a = f1 a u T ⊕ f2 a u T"
using AImp.prems(1) by blast
moreover have "bool_conj pc b |a| ⟹ sat A (the ( |a| ⊕ 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| ≽ |a| ∧ Some a = f1 a u T ⊕ f2 a u T ∧ sat (AImp b A) (the ( |a| ⊕ f1 a u T))"
using AImp.prems(1) asm0(1) by blast
moreover have "b (the ( |a| ⊕ f1 a u T))"
proof -
have "|a| ## f1 a u T ∧ |a| ≽ |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| ⊕ f1 a u T"
by (meson defined_def option.collapse)
then have "|x| = |a|"
by (metis ‹Some x = |a| ⊕ f1 a u T› ‹|a| ## f1 a u T ∧ |a| ≽ |f1 a u T|› commutative core_is_pure core_sum max_projection_prop_pure_core mpp_smaller smaller_than_core)
then show ?thesis
by (metis AImp.prems(3) ‹Some x = |a| ⊕ f1 a u T› ‹bool_conj pc b |a|› bool_conj_def mono_pure_cond_def option.sel wf_assertion.simps(2))
qed
ultimately show "sat A (the ( |a| ⊕ f1 a u T))" by (metis sat.simps(2))
qed
ultimately show "|f1 a u T| ≽ |a| ∧ Some a = f1 a u T ⊕ f2 a u T ∧ (bool_conj pc b |a| ⟶ sat A (the ( |a| ⊕ f1 a u T)))"
by (metis AImp.prems(1) asm0)
qed
then obtain S' where r: "package_rhs φ f S (bool_conj pc b) A φ f S'" "⋀a' u' T. (a', u', T) ∈ S' ⟹ (∃a u. (a, u, T) ∈ S ∧ a' ≽ f2 a u T)"
by fast
moreover have "package_rhs φ f S pc (AImp b A) φ f S'"
ultimately show ?case
using r0 package_rhs.AImp by blast
next
case (ASem A)
let ?witness = "λ(a, u, T). the ( |a| ⊕ f1 a u T)"

obtain S' where S'_def: "S' = { (a, u, T) |a u T. (a, u, T) ∈ S ∧ ¬ pc a }
∪ { (a ⊖ b, the (u ⊕ b), T) |a u T b. (a, u, T) ∈ S ∧ pc a ∧ b = ?witness (a, u, T) }"
by blast

have "package_rhs φ f S pc (ASem A) φ f S'"
proof (rule package_rhs.ASem)
show "S' = {(a, u, T) |a u T. (a, u, T) ∈ S ∧ ¬ pc a} ∪ {(a ⊖ b, the (u ⊕ b), T) |a u T b. (a, u, T) ∈ S ∧ pc a ∧ b = ?witness (a, u, T)}"
using S'_def by blast
fix a u T b
assume asm0: "(a, u, T) ∈ S" "pc a" "b = (case (a, u, T) of (a, u, T) ⇒ the ( |a| ⊕ f1 a u T))"
then have "b = the ( |a| ⊕ f1 a u T)" by fastforce
moreover have "pc |a|"
by (meson ASem.prems(4) asm0(2) mono_pure_cond_def)
then obtain "|f1 a u T| ≽ |a|" "Some a = f1 a u T ⊕ f2 a u T" "sat (ASem A) (the ( |a| ⊕ f1 a u T))"
using ASem.prems(1) asm0(1) by blast
then have "Some b = |a| ⊕ f1 a u T" by (metis calculation commutative defined_def minus_bigger minus_core option.exhaust_sel smaller_compatible_core)
moreover have "a ≽ b"
proof -
have "a ≽ f1 a u T"
using ‹Some a = f1 a u T ⊕ f2 a u T› greater_def by blast
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 ≽ b ∧ A b"
using ‹sat (ASem A) (the ( |a| ⊕ f1 a u T))› sat.simps(3) by blast
qed

moreover have r0: "⋀a' u' T. (a', u', T) ∈ S' ⟹ (∃a u. (a, u, T) ∈ S ∧ a' ≽ f2 a u T ∧ |a'| = |a| )"
proof -
fix a' u' T assume asm0: "(a', u', T) ∈ S'"
then show "∃a u. (a, u, T) ∈ S ∧ a' ≽ f2 a u T ∧ |a'| = |a| "
proof (cases "(a', u', T) ∈ {(a, u, T) |a u T. (a, u, T) ∈ S ∧ ¬ pc a}")
case True
then show ?thesis using ASem.prems(1) greater_equiv by fastforce
next
case False
then have "(a', u', T) ∈ { (a ⊖ b, the (u ⊕ b), T) |a u T b. (a, u, T) ∈ S ∧ pc a ∧ b = ?witness (a, u, T) }"
using S'_def asm0 by blast
then obtain a u b where "a' = a ⊖ b" "u' = the (u ⊕ b)" "(a, u, T) ∈ S" "pc a" "b = ?witness (a, u, T)"
by blast
then have "a' ≽ f2 a u T"
proof -
have "a ≽ b"
proof -
have "a ≽ f1 a u T"
using ASem.prems(1) ‹(a, u, T) ∈ S› greater_def by blast
moreover have "Some b = |a| ⊕ f1 a u T"
by (metis ‹b = (case (a, u, T) of (a, u, T) ⇒ the ( |a| ⊕ f1 a u T))› 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]
‹(a, u, T) ∈ S› ‹a' = a ⊖ b› ‹b = (case (a, u, T) of (a, u, T) ⇒ the ( |a| ⊕ f1 a u T))›
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|  ⊕ f1 a u T)"] asso2[of "f2 a u T" "f1 a u T"]
split_conv
by metis
qed
then show ?thesis
using ‹(a, u, T) ∈ S› ‹a' = a ⊖ b› minus_core by blast
qed
qed

ultimately show ?case by blast
next
case (AStar A B)

let ?fA = "λa u T. SOME x. ∃y. Some (f1 a u T) = x ⊕ y ∧ |x| ≽ |f1 a u T| ∧ |y| ≽ |a| ∧ (pc |a| ⟶ sat A (the ( |a| ⊕ x)) ∧ sat B (the ( |a| ⊕ y)))"
let ?fB = "λa u T. SOME y. Some (f1 a u T) = ?fA a u T ⊕ y ∧ |y| ≽ |a| ∧ (pc |a| ⟶ sat B (the ( |a| ⊕ y)))"
let ?f2 = "λa u T. the (?fB a u T ⊕ f2 a u T)"

have r: "⋀a u T. (a, u, T) ∈ S ⟹ Some (f1 a u T) = ?fA a u T ⊕ ?fB a u T ∧ |?fA a u T| ≽ |f1 a u T| ∧ |?fB a u T| ≽ |a| ∧ (pc |a| ⟶ sat A (the ( |a| ⊕ ?fA a u T)) ∧ sat B (the ( |a| ⊕ ?fB a u T)))
∧ Some (?f2 a u T) = ?fB a u T ⊕ f2 a u T"
proof -
fix a u T assume asm0: "(a, u, T) ∈ S"
then have r0: "Some a = f1 a u T ⊕ f2 a u T ∧ (pc |a| ⟶ sat (AStar A B) (the ( |a| ⊕ f1 a u T)))"
using AStar.prems(1) by blast
then have "∃x y. Some (the ( |a| ⊕ f1 a u T )) = x ⊕ y ∧ (pc |a| ⟶ sat A x) ∧ (pc |a| ⟶ sat B y) ∧
x ≽ |(the ( |a| ⊕ f1 a u T))| ∧ y ≽ |(the ( |a| ⊕ f1 a u T))|"
proof (cases "pc |a|")
case True
then show ?thesis
using AStar.prems(3) r0
max_projection_prop_def[of pure core] max_projection_prop_pure_core
sat_star_exists_bigger[of A B "(the ( |a|  ⊕ f1 a u T))"]
succ_trans[of ] wf_assertion.simps(1)[of A B]
by blast
next
case False
then have "Some (the ( |a| ⊕ f1 a u T )) = the ( |a| ⊕ f1 a u T) ⊕ |the ( |a| ⊕ f1 a u T )|"
then show ?thesis by (metis False max_projection_prop_pure_core mpp_smaller succ_refl)
qed
then obtain x y where "Some (the ( |a| ⊕ f1 a u T)) = x ⊕ y" "pc |a| ⟶ sat A x" "pc |a| ⟶ sat B y"
"x ≽ |(the ( |a| ⊕ f1 a u T))|" "y ≽ |(the ( |a| ⊕ f1 a u T))|" by blast
moreover obtain af where "Some af = |a| ⊕ f1 a u T"
by (metis r0 commutative defined_def minus_bigger minus_core option.exhaust_sel smaller_compatible_core)
ultimately have "Some (f1 a u T) = x ⊕ y"
by (metis AStar.prems(1) r0 asm0 commutative core_is_smaller greater_def max_projection_prop_pure_core mpp_mono option.sel succ_antisym)
moreover have "|a| ## x ∧ |a| ## y"
by (metis ‹Some af = |a| ⊕ f1 a u T› calculation commutative defined_def option.discI sep_algebra.asso3 sep_algebra_axioms)
then have "the ( |a| ⊕ x) ≽ x ∧ the ( |a| ⊕ y) ≽ y"
using commutative defined_def greater_def by auto

ultimately have pc_implies_sat: "pc |a| ⟹ sat A (the ( |a| ⊕ x)) ∧ sat B (the ( |a| ⊕ y))"
by (metis AStar.prems(3) ‹pc |a| ⟶ sat A x› ‹pc |a| ⟶ sat B y› ‹|a| ## x ∧ |a| ## y› 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 r1: "∃y. Some (f1 a u T) = ?fA a u T ⊕ y ∧ |?fA a u T| ≽ |f1 a u T| ∧ |y| ≽ |a| ∧ (pc |a| ⟶ sat A (the ( |a| ⊕ ?fA a u T)) ∧ sat B (the ( |a| ⊕ y)))"
proof (rule someI_ex)
show "∃x y. Some (f1 a u T) = x ⊕ y ∧ |x| ≽ |f1 a u T| ∧ |y| ≽ |a| ∧ (pc |a| ⟶ sat A (the ( |a| ⊕ x)) ∧ sat B (the ( |a| ⊕ y)))"
using ‹Some (f1 a u T) = x ⊕ y› ‹Some (the ( |a| ⊕ f1 a u T)) = x ⊕ y› pc_implies_sat ‹x ≽ |the ( |a| ⊕ f1 a u T)|› ‹y ≽ |the ( |a| ⊕ f1 a u T)|› 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 yy_prop: "Some (f1 a u T) = ?fA a u T ⊕ yy ∧ |?fA a u T| ≽ |f1 a u T| ∧ |yy| ≽ |a| ∧ (pc |a| ⟶ sat A (the ( |a| ⊕ ?fA a u T)) ∧ sat B (the ( |a| ⊕ yy)))"
by blast
moreover have r2: "Some (f1 a u T) = ?fA a u T ⊕ ?fB a u T ∧ |?fB a u T| ≽ |a| ∧ (pc |a| ⟶ sat B (the ( |a| ⊕ ?fB a u T)))"
proof (rule someI_ex)
show "∃y. Some (f1 a u T) = ?fA a u T ⊕ y ∧ |y| ≽ |a| ∧ (pc |a| ⟶ sat B (the ( |a| ⊕ y)))"
using r1 by blast
qed
ultimately have "?fB a u T ⊕ f2 a u T ≠ None"
using r0
option.distinct(1) [of ] option.exhaust_sel[of "?fB 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"]
by metis
then show "Some (f1 a u T) = ?fA a u T ⊕ ?fB a u T ∧ |?fA a u T| ≽ |f1 a u T| ∧ |?fB a u T| ≽ |a|
∧ (pc |a| ⟶ sat A (the ( |a| ⊕ ?fA a u T)) ∧ sat B (the ( |a| ⊕ ?fB a u T))) ∧ Some (?f2 a u T) = ?fB a u T ⊕ f2 a u T"
using r0 r2 yy_prop
option.distinct(1) option.exhaust_sel[of "?fB 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"]
by simp
qed
have ih1: "∃S'. package_rhs φ f S pc A φ f S' ∧ (∀a∈S'. case a of (a', u', T) ⇒ ∃a u. (a, u, T) ∈ S ∧ a' ≽ ?f2 a u T ∧ |a'| = |a| )"
proof (rule AStar(1))
show "valid_package_set S f"
show "wf_assertion A"
using AStar.prems(3) by auto
show "mono_pure_cond pc"
show "stable f ∧ φ ## f" using ‹stable f ∧ φ ## f› by simp

fix a u T
assume asm0: "(a, u, T) ∈ S"
then have b: "Some (f1 a u T) = ?fA a u T ⊕ ?fB a u T ∧ |?fA a u T| ≽ |f1 a u T| ∧ |?fB a u T| ≽ |a| ∧ (pc |a| ⟶ sat A (the ( |a| ⊕ ?fA a u T)) ∧ sat B (the ( |a| ⊕ ?fB a u T)))"
using r by fast
show "|?fA a u T| ≽ |a| ∧ Some a = ?fA a u T ⊕ ?f2 a u T ∧ (pc |a| ⟶ sat A (the ( |a| ⊕ ?fA a u T)))"
proof -
have "|?fA a u T| ≽ |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 ⊕ ?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 ⊕ f2 a u T" "Some a = ?fA a u T ⊕ ?f2 a u T"]
by force
moreover have "pc |a| ⟶ sat A (the ( |a| ⊕ ?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 φ f S pc A φ f S'" "⋀a' u' T. (a', u', T) ∈ S' ⟹ ∃a u. (a, u, T) ∈ S ∧ a' ≽ ?f2 a u T  ∧ |a'| = |a| "
by fast

let ?project = "λa' T. (SOME r. ∃a u. r = (a, u) ∧ (a, u, T) ∈ S ∧ a' ≽ ?f2 a u T ∧ |a'| = |a| )"
have project_prop: "⋀a' u' T. (a', u', T) ∈ S' ⟹ ∃a u. ?project a' T = (a, u) ∧ (a, u, T) ∈ S ∧ a' ≽ ?f2 a u T  ∧ |a'| = |a| "
proof -
fix a' u' T assume "(a', u', T) ∈ S'"
then obtain a u where "(a, u, T) ∈ S ∧ a' ≽ ?f2 a u T  ∧ |a'| = |a| "
using r' by blast
moreover show "∃a u. ?project a' T = (a, u) ∧ (a, u, T) ∈ S ∧ a' ≽ ?f2 a u T ∧ |a'| = |a| "
proof (rule someI_ex)
show "∃r a u. r = (a, u) ∧ (a, u, T) ∈ S ∧ a' ≽ ?f2 a u T ∧ |a'| = |a| " using calculation by blast
qed
qed

let ?nf1 = "λa' u' T. let (a, u) = ?project a' T in (SOME r. Some r = |a'| ⊕ ?fB a u T)"
let ?nf2 = "λa' u' T. a' ⊖ ?nf1 a' u' T"

have "∃S''. package_rhs φ f S' pc B φ f S'' ∧ (∀a∈S''. case a of (a', u', T) ⇒ ∃a u. (a, u, T) ∈ S' ∧ a' ≽ ?nf2 a u T ∧ |a'| = |a| )"
proof (rule AStar(2))
show "stable f ∧ φ ## f" using ‹stable f ∧ φ ## f› by simp

then show "valid_package_set S' f"
using AStar.prems ‹package_rhs φ f S pc A φ f S'› 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"
fix a' u' T assume "(a', u', T) ∈ S'"
then obtain a u where a_u_def: "(a, u) = ?project a' T" "(a, u, T) ∈ S" "a' ≽ ?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'| ⊕ ?fB a u T"
proof -
let ?x = "(SOME r. Some r = |a'| ⊕ ?fB a u T )"
have "Some ?x = |a'| ⊕ ?fB a u T"
proof (rule someI_ex)
have "Some (f1 a u T) = ?fA a u T ⊕ ?fB a u T ∧ |?fA a u T| ≽ |f1 a u T| ∧ |?fB a u T| ≽ |a|
∧ (pc |a| ⟶ sat A (the ( |a| ⊕ ?fA a u T)) ∧ sat B (the ( |a| ⊕ ?fB a u T)))"
using r a_u_def by blast
then have "Some (?f2 a u T) = ?fB a u T ⊕ 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' ≽ (?f2 a u T)" using ‹a' ≽ ?f2 a u T› by blast
ultimately have "a' ≽ ?fB a u T" using succ_trans greater_def
by blast
then obtain r where "Some r = |a'| ⊕ ?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 "∃r. Some r = |a'| ⊕ ?fB a u T" by blast
qed
moreover have "?nf1 a' u' T = ?x"
using let_pair_instantiate[of a u _ a' T "λa u. (SOME r. Some r = |a'| ⊕ ?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 ⊕ nf2"
proof -
have "nf2 = a' ⊖ nf1" using nf1_def nf2_def by blast
moreover have "a' ≽ nf1"
proof -
have "?f2 a u T ≽ nf1"
proof -
have "Some (?f2 a u T) = ?fB a u T ⊕ f2 a u T" using r ‹(a, u, T) ∈ S› by blast
then have "?f2 a u T ≽ ?fB a u T"
using greater_def by blast
moreover have "?f2 a u T ≽ |a'|"
proof -
have "|?f2 a u T| ≽ |a|"
proof -
have "|?f2 a u T| ≽ |?fB a u T|" using ‹?f2 a u T ≽ ?fB a u T› core_mono by blast
moreover have "|?fB a u T| ≽ |a|" using r ‹(a, u, T) ∈ S› by blast
ultimately show ?thesis using succ_trans ‹|a'| = |a|› 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 ‹a' ≽ ?f2 a u T› succ_trans by blast
qed
ultimately show ?thesis using minus_some nf2_def by blast
qed

moreover have "pc  |a'| ⟹ sat B (the ( |a'|  ⊕ ?nf1 a' u' T))"
proof -
assume "pc  |a'|"
moreover have "|a'| = |a|"
then have "pc |a|" using ‹pc  |a'|› by simp
ultimately have "sat B (the ( |a| ⊕ ?fB a u T))"
using r a_u_def by blast
then have "sat B (the ( |a'| ⊕ ?fB a u T))" using ‹|a'| = |a|› by simp

then show "sat B (the ( |a'|  ⊕ ?nf1 a' u' T))"
proof -
have "nf1 ≽ |a'|" using rnf1_def
using greater_def by blast
then have "Some nf1 = |a'| ⊕ 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 ‹sat B (the ( |a'| ⊕ ?fB a u T))› by argo
qed
qed
moreover have "|?nf1 a' u' T|  ≽  |a'|"
proof -
have "?nf1 a' u' T ≽ |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|  ≽  |a'|  ∧ Some a' = ?nf1 a' u' T ⊕ ?nf2 a' u' T ∧ (pc  |a'|  ⟶ sat B (the ( |a'|  ⊕ ?nf1 a' u' T)))"
using nf1_def
by blast
qed

then obtain S'' where S''_prop: "package_rhs φ f S' pc B φ f S''" "⋀a' u' T. (a', u', T) ∈ S'' ⟹ ∃a u. (a, u, T) ∈ S' ∧ a' ≽ ?nf2 a u T  ∧ |a'| = |a| "
by fast

then have "package_rhs φ f S pc (AStar A B) φ f S''"
using ‹package_rhs φ f S pc A φ f S'› package_rhs.AStar by presburger
moreover have "⋀a'' u'' T. (a'', u'', T) ∈ S'' ⟹ ∃a u. (```