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'  (aS'. 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'  (aS'. 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''  (aS''. 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. (