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"
  by (simp add: assms package_sat_def)


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'"
        by (simp add: fb_def(4) mono_transformer_def)
      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| "
            by (simp add: minus_core succ_refl)
          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)"
      using AddFromOutside.hyps(6) by blast
    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''"
    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: "φ' ⊕ 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''"
      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 "φ ## f"
      by (simp add: AddFromOutside.prems(5))
    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'"
        using AddFromOutside.hyps(6) asm0 by blast

      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"
      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 ∧ φ ## 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'"
    by (simp add: package_rhs.AImp r(1))
  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 )|"
        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| ⊕ 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"
      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 ∧ φ ## 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"
      by (simp add: AStar.prems(4))
    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|"
        by (simp add: a_u_def(4))
      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. (a, u, T) ∈ S ∧ a'' ≽ f2 a u T  ∧ |a''| = |a|"
  proof -
    fix a'' u'' T assume asm0: "(a'', u'', T) ∈ S''"

    
    then obtain a' u' where "(a', u', T) ∈ S' ∧ a'' ≽ ?nf2 a' u' T  ∧ |a''| = |a'| "
      using S''_prop by blast

    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: "a' ≽ nf1 ∧ ?nf2 a' u' T ≽ f2 a u T"
    proof -
      have "nf2 = a' ⊖ nf1" using nf1_def nf2_def by blast
      moreover have "a' ≽ nf1 ∧ a' ⊖ nf1 ≽ f2 a u T"
      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
                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' ≽ nf1" using ‹a' ≽ ?f2 a u T› succ_trans by blast
        then have "Some a' = nf1 ⊕ nf2" using minus_some nf2_def ‹nf2 = a' ⊖ nf1› by presburger
        have r2: "a' ⊖ nf1 ≽ f2 a u T"
          using ‹a' ≽ ?f2 a u T›
        proof (rule prove_last_completeness)

          have "Some (?f2 a u T) = ?fB a u T ⊕ f2 a u T"
            using r ‹(a, u, T) ∈ S› by blast
          moreover have "Some nf1 = |a'| ⊕ ?fB a u T" using rnf1_def by blast

          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 _ "|a|"]
                greater_equiv[of "?f2 a u T" "|a|"]
              by auto
          qed
          ultimately show "Some (?f2 a u T) = nf1 ⊕ 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 ‹a' ≽ ?f2 a u T› succ_trans using r1 by force
      qed
      ultimately show ?thesis  using nf2_def by argo
    qed
    ultimately have "(a, u, T) ∈ S ∧ a' ≽ ?f2 a u T ∧ ?nf2 a' u' T ≽ f2 a u T" using nf1_def nf2_def
        a_u_def by blast
    then have "a'' ≽ f2 a u T ∧  |a''| = |a'| " using ‹(a', u', T) ∈ S' ∧ a'' ≽ ?nf2 a' u' T ∧ |a''| = |a'| ›
      using succ_trans by blast
    then show "∃a u. (a, u, T) ∈ S ∧ a'' ≽ f2 a u T  ∧ |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 φ unit { (a, unit, T) |a T. (a, T) ∈ S } (λ_. True) A φ' f S'"
      and "⋀a T. (a, T) ∈ S ⟹ mono_transformer T"
      and "wf_assertion A"
      and "intuitionistic (sat A) ∨ pure_remains S'"
    shows "Some φ = φ' ⊕ f ∧ stable f ∧ (∀(a, T) ∈ S. a ## T f ⟶ sat A (the (a ⊕ T f)))"
proof -
  let ?S = "{ (a, unit, p) |a p. (a, p) ∈ S }"
  let ?pc = "λ_. True"
  have "package_rhs_connection φ unit ?S ?pc A φ' f S' ∧ valid_package_set S' f"
  proof (rule package_rhs_proof)
    show "package_rhs φ unit {(a, unit, p) |a p. (a, p) ∈ S} (λ_. True) A φ' f S'"
      using assms(1) by auto
    show "valid_package_set {(a, unit, p) |a p. (a, p) ∈ S} unit"
    proof (rule valid_package_setI)
      fix a u T
      assume "(a, u, T) ∈ {(a, unit, p) |a p. (a, p) ∈ S}"
      then have "u = unit" by blast
      moreover have "|T unit| = unit"
        using ‹(a, u, T) ∈ {(a, unit, p) |a p. (a, p) ∈ S}› assms(2) mono_transformer_def unit_core by fastforce
      then show "a ## u ∧ |a| ≽ |u| ∧ mono_transformer T ∧ a ≽  |T unit|"
        using ‹(a, u, T) ∈ {(a, unit, p) |a p. (a, p) ∈ S}› 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 (λ_. True)"
      using mono_pure_cond_def by auto
    show "stable unit" by (simp add: stable_unit)
    show "φ ## unit"
      using defined_def unit_neutral by auto
  qed

  then obtain r: "φ ⊕ unit = φ' ⊕ f" "stable f"
    "⋀a u T. (a, u, T) ∈ ?S ⟹ (∃au. Some au = a ⊕ u ∧ (au ## (T f ⊖ T unit) ⟶
      (∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ (T f ⊖ T unit) = a' ⊕ u' ∧ u' ≽ u ∧ package_sat ?pc A a' u' u)))"
    using package_rhs_connection_def by force

  moreover have "⋀a T x. (a, T) ∈ S ∧ Some x = a ⊕ T f ⟹ sat A x"
  proof -
    fix a T x assume asm0: "(a, T) ∈ S ∧ Some x = a ⊕ T f"
    then have "T f ⊖ 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 au_def: "Some au = a ⊕ unit ∧ (au ## T f ⟶
      (∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ au ⊕ T f = a' ⊕ u' ∧ u' ≽ unit ∧ package_sat ?pc A a' u' unit))"
      using r asm0 by fastforce
    then have "au = a" by (metis option.inject unit_neutral)
    then have "(∃a' u'. (a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ a ⊕ T f = a' ⊕ u' ∧ package_sat ?pc A a' u' unit)"
      using au_def asm0 defined_def       
      by auto
    then obtain a' u' where r0: "(a', u', T) ∈ S' ∧ |a'| ≽ |a| ∧ a ⊕ T f = a' ⊕ u' ∧ package_sat ?pc A a' u' unit"
      by presburger
    then obtain y where "Some y = |a'| ⊕ (u' ⊖ unit)" "sat A y"
      using package_sat_def by auto
    then have "Some y =  |a'| ⊕ u'"
      by (metis commutative minus_equiv_def splus.simps(3) unit_neutral unit_smaller)
    then have "x ≽ y"
      by (metis r0 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 ‹Some y = |a'| ⊕ (u' ⊖ unit)› ‹sat A y› ‹x ≽ y› intuitionistic_def)
    next
      case False
      then have "pure_remains S'" using assms(4) by auto
      then have "pure a'" using pure_remains_def r0
        by fast
      then show ?thesis using r0 ‹Some y = |a'| ⊕ (u' ⊖ unit)› ‹sat A y› ‹Some y = |a'| ⊕ u'› asm0 core_is_smaller
          core_max option.sel pure_def asso1[of a'] by metis
    qed
  qed
  then have "(∀(a, T) ∈ S. a ## T f ⟶ sat A (the (a ⊕ T f)))"
    using sep_algebra.defined_def sep_algebra_axioms by fastforce
  moreover have "Some φ = φ' ⊕ f ∧ stable f"
    using r(1) r(2) unit_neutral by auto
  ultimately show ?thesis by blast
qed

theorem soundness:
  assumes "wf_assertion B"
      and "⋀a. sat A a ⟹ a ∈ S"
      and "⋀a. a ∈ S ⟹ mono_transformer (R a)"
      and "package_rhs σ unit { (a, unit, R a) |a. a ∈ S } (λ_. True) B σ' w S'"
      and "intuitionistic (sat B) ∨ pure_remains S'"
    shows "stable w ∧ Some σ = σ' ⊕ w ∧ is_footprint_general w R A B"
proof -
  let ?S = "{ (a, R a) |a. a ∈ S} "
  have r: "Some σ = σ' ⊕ w ∧ stable w ∧ (∀(a, T)∈{(a, R a) |a. a ∈ S}. a ## T w ⟶ sat B (the (a ⊕ T w)))"
  proof (rule general_soundness)
    show "package_rhs σ unit {(a, unit, T) |a T. (a, T) ∈ {(a, R a) |a. a ∈ S}} (λ_. True) B σ' w S'"
      using assms(4) by auto
    show "⋀a T. (a, T) ∈ {(a, R a) |a. a ∈ S} ⟹ mono_transformer T" using assms(3) by blast
    show "wf_assertion B" by (simp add: assms(1))
    show "intuitionistic (sat B) ∨ 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 ∧ Some b = a ⊕ R a w"
    then have "(a, R a) ∈ ?S"
      using assms(2) by blast
    then have "sat B (the (a ⊕ 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 "⋀a. sat A a ⟹ a ∈ S"
      and "package_rhs σ unit { (a, unit, id) |a. a ∈ S } (λ_. True) B σ' w S'"
      and "intuitionistic (sat B) ∨ pure_remains S'"
    shows "stable w ∧ Some σ = σ' ⊕ w ∧ is_footprint_standard w A B"
proof -
  have "stable w ∧ Some σ = σ' ⊕ w ∧ is_footprint_general w (λ_. id) A B"
    using assms soundness[of B A S "λ_. id" σ σ' 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 "⋀a u T x. (a, u, T) ∈ S ⟹ Some x = a ⊕ T f ⟹ sat A x"
      and "Some φ = φ' ⊕ f"
      and "stable f"
      and "valid_package_set S unit"
      and "wf_assertion A"
    shows "∃S'. package_rhs φ unit S (λ_. True) A φ' f S'"
proof -
  define S' where "S' = { (r, u, T) |a u T r. (a, u, T) ∈ S ∧ Some r = a ⊕ (T f ⊖ T unit) ∧ r ## u }"
  let ?pc = "λ_. True"
  have "∃S''. package_rhs φ' f S' ?pc A φ' f S''"
  proof -
    let ?f2 = "λa u T. unit"
    let ?f1 = "λa u T. a"
    have "∃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| )"
    proof (rule completeness_aux)
      show "mono_pure_cond (λ_. 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) ∈ S'"
        then obtain a where asm: "(a, u', T) ∈ S ∧ Some a' = a ⊕ (T f ⊖ T unit) ∧ a' ## u'"
          using S'_def by blast
        then have "a ## u' ∧  |a|  ≽  |u'|  ∧ mono_transformer T "
          using assms(4) valid_package_set_def by fastforce
        moreover have "|T f ⊖ T unit| = |T f|"
          by (simp add: minus_core)
        ultimately show "a' ## u' ∧  |a'|  ≽  |u'|  ∧ mono_transformer T ∧ a' ≽  |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 ∧ φ' ## f"
        by (metis assms(2) assms(3) defined_def domI domIff)
      fix a u T
      assume "(a, u, T) ∈ S'"
      then obtain a' u' where "(a', u', T) ∈ S" "Some a = a' ⊕ (T f ⊖ T unit)" using S'_def by blast
      moreover have "T f ⊖ T unit = T f"
      proof -
        have "mono_transformer T" using ‹valid_package_set S unit› valid_package_set_def ‹(a', u', T) ∈ S› 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|  ⊕ a))"
        by (metis assms(1) calculation(1) calculation(2) commutative core_is_smaller option.sel)
      then show "|a|  ≽  |a|  ∧ Some a = a ⊕ unit ∧ (True ⟶ sat A (the ( |a|  ⊕ a)))"
        by (simp add: succ_refl unit_neutral)
    qed
    then show ?thesis by auto
  qed
  then obtain S'' where "package_rhs φ' f S' ?pc A φ' f S''" by blast
  have "package_rhs φ unit S ?pc A φ' f S''"
    using assms(2)
  proof (rule package_rhs.AddFromOutside)
    show "package_rhs φ' f S' ?pc A φ' f S''"
      by (simp add: ‹package_rhs φ' f S' ?pc A φ' f S''›)
    show "stable f" using assms(3) by simp
    show "Some f = unit ⊕ f"
      by (simp add: commutative unit_neutral)
    show "S' = { (r, u, T) |a u T r. (a, u, T) ∈ S ∧ Some r = a ⊕ (T f ⊖ T unit) ∧ r ## u }"
      using S'_def by blast
  qed
  then show ?thesis
    by blast
qed

theorem completeness:
  assumes "wf_assertion B"
      and "stable w ∧ is_footprint_general w R A B"
      and "Some σ = σ' ⊕ w"
      and "⋀a. sat A a ⟹ mono_transformer (R a)"
    shows "∃S'. package_rhs σ unit {(a, unit, R a) |a. sat A a} (λ_. True) B σ' w S'"
proof -
  let ?S = "{(a, unit, R a) |a. sat A a}"
  have "∃S'. package_rhs σ unit {(a, unit, R a) |a. sat A a} (λ_. True) B σ' w S'"
  proof (rule general_completeness[of ?S w B σ σ'])
    show "⋀a u T x. (a, u, T) ∈ {(a, unit, R a) |a. sat A a} ⟹ Some x = a ⊕ T w ⟹ sat B x"
      using assms(2) is_footprint_general_def by blast
    show "Some σ = σ' ⊕ 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) ∈ {(a, unit, R a) |a. sat A a}"
      then have "u = unit ∧ T = R a ∧ sat A a" by fastforce
      then show "a ## u ∧  |a|  ≽  |u|  ∧ mono_transformer T ∧ a ≽  |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 ∧ is_footprint_standard w A B"
      and "Some σ = σ' ⊕ w"
    shows "∃S'. package_rhs σ unit {(a, unit, id) |a. sat A a} (λ_. True) B σ' w S'"
proof -
  have "∃S'. package_rhs σ unit {(a, unit, (λ_. id) a) |a. sat A a} (λ_. True) B σ' w S'"
    using assms(1)
  proof (rule completeness)
    show "stable w ∧ is_footprint_general w (λa. id) A B"
      using assms(2) is_footprint_general_def is_footprint_standard_def by force
    show "Some σ = σ' ⊕ w" by (simp add: assms(3))
    show "⋀a. sat A a ⟹ mono_transformer id" using mono_transformer_def by auto
  qed
  then show ?thesis by meson
qed


end

end