Theory Probability_Inequality_Completeness

chapter ‹ Introduction ›

theory Probability_Inequality_Completeness
  imports
    "Suppes_Theorem.Probability_Logic"
begin

unbundle no funcset_syntax

text ‹ We introduce a novel logical calculus and prove completeness for
       probability inequalities. This is a vast generalization of ∗‹Suppes' Theorem›
       which lays the foundation for this theory.›

text ‹ We provide two new logical judgements: ∗‹measure deduction› ‹($⊢)› and
       ∗‹counting deduction› ‹(#⊢)›. Both judgements capture a notion of ∗‹measure›
       or quantity. In both cases premises must be partially or completely ∗‹consumed›
       in sense to prove multiple conclusions. That is to say, a portion of the
       premises must be used to prove each conclusion which cannot be reused. Counting
       deduction counts the number of times a particular conclusion can be proved
       (as the name implies), while measure deduction includes multiple, different
       conclusions which must be proven via the premises. ›

text ‹ We also introduce an abstract notion of MaxSAT, which is the
       maximal number of clauses in a list of clauses that can be simultaneously
       satisfied. ›

text ‹ We show the following are equivalent:

  ▪ ‹❙∼ Γ $⊢ ❙∼ Φ›
  ▪ ‹(❙∼ Γ @ Φ) #⊢ (length Φ) ⊥›
  ▪ ‹MaxSAT (❙∼ Γ @ Φ) ≤ length Γ›
  ▪ ‹∀ δ ∈ dirac_measures. (∑φ←Φ. δ φ) ≤ (∑γ←Γ. δ γ)›
  ▪ ‹∀ 𝒫 ∈ probabilities. (∑φ←Φ. 𝒫 φ) ≤ (∑γ←Γ. 𝒫 γ)›
›

text ‹ In the special case of MaxSAT, we show the following are
       equivalent:

  ▪ ‹MaxSAT (❙∼ Γ @ Φ) + c ≤ length Γ›
  ▪ ‹∀ δ ∈ dirac_measures. (∑φ←Φ. δ φ) + c ≤ (∑γ←Γ. δ γ)›
  ▪ ‹∀ 𝒫 ∈ probabilities. (∑φ←Φ. 𝒫 φ) + c ≤ (∑γ←Γ. 𝒫 γ)›
›

chapter ‹ Measure Deduction and Counting Deduction ›

section ‹ Definition of Measure Deduction ›

text ‹ To start, we introduce a common combinator for modifying functions
       that take two arguments. ›

definition uncurry :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a × 'b ⇒ 'c"
  where uncurry_def [simp]: "uncurry f = (λ (x, y). f x y)"

text ‹ Our new logical calculus is a recursively defined relation ‹($⊢)›
       using ∗‹list deduction› \<^term>‹(:⊢)›. ›

text ‹ We call our new logical relation ∗‹measure deduction›: ›

primrec (in classical_logic)
  measure_deduction :: "'a list ⇒ 'a list ⇒ bool" (infix ‹$⊢› 60)
  where
    "Γ $⊢ [] = True"
  | "Γ $⊢ (φ # Φ) =
       (∃ Ψ. mset (map snd Ψ) ⊆# mset Γ
                 ∧ map (uncurry (⊔)) Ψ :⊢ φ
                 ∧ map (uncurry (→)) Ψ @ Γ ⊖ (map snd Ψ) $⊢ Φ)"

text ‹ Let us briefly analyze what the above definition is saying. ›

text ‹ From the above we must find a special list-of-pairs ‹Ψ›,
       which we refer to as a ∗‹witness›, in order to establish
      \<^term>‹Γ $⊢ (φ # Φ)›. ›

text ‹ We may motivate measure deduction as follows. In the simplest case
       we know ‹𝒫 φ ≤ 𝒫 ψ + Σ› if and only if
       ‹𝒫 ( χ ⊔ φ ) + 𝒫 ( ∼ χ ⊔ φ ) ≤ 𝒫 ψ + Σ›, or equivalently
       ‹𝒫 ( χ ⊔ φ ) + 𝒫 ( χ → φ ) ≤ 𝒫 ψ + Σ›. So it suffices to prove
       ‹𝒫 ( χ ⊔ φ ) ≤ 𝒫 ψ› and ‹𝒫 ( χ → φ ) ≤ Σ ›. Here ‹[(χ,φ)]›
       is like the ∗‹witness› in our recursive definition, which reflects the
       ‹∃ Ψ. …› formula is our definition. The fact that measure deduction
       reflects proving theorems in the theory of inequalities of probability
       logic is the elementary intuition behind the soundness theorem we will
       ultimately prove in \S\ref{subsubsec:measure-deduction-soundness}. ›

text ‹ A key difference from the simple motivation above is that, as in the
       case of Suppes' Theorem where we prove ‹ ❙∼ Γ :⊢ ∼ φ › if and only if
       ‹𝒫 φ ≤ (∑ γ ← Γ . 𝒫 γ)› for all ‹𝒫›, soundness in this context means
       ‹ ❙∼ Γ $⊢ ❙∼ Φ › implies ‹∀ 𝒫. (∑γ←Γ. 𝒫 γ) ≥ (∑φ←Φ. 𝒫 φ) ›. ›

text ‹ Another way of thinking about measure deduction is to think of ‹Γ›
       and ‹Σ› as bags of balls of soft clay and \<^term>‹Γ $⊢ Σ› meaning that
       we have shown ‹Γ› is ∗‹heavier than› ‹Σ› (ignoring, for the moment,
       that \<^term>‹($⊢)› is not totally ordered). We have a scale \<^term>‹(:⊢)›
       that lets us weigh several things on the left and one thing on the
       right at a time. We go through each clay ball ‹σ› in ‹Σ› one at a
       time without replacement, putting ‹σ› on the right of the scale. Then,
       we take a bunch of clay balls from ‹Γ›, cut them up as necessary (that
       is the ‹ψ ⊔ γ› trick using the witness ‹Ψ›), and show they are heavier
       using our scale. We take the parts ‹ψ → γ› that we didn't use and put
       them back in our bag ‹Γ›. We will be able to reuse them later. If we
       can do this trick for every element ‹σ› in ‹Σ› successively using
       combinations of split leftovers in ‹Γ›, then we can show ‹Γ› is
       heavier than ‹Σ› (i.e., \<^term>‹Γ $⊢ Σ›). ›

section ‹ Definition of the Stronger Theory Relation ›

text ‹ We next turn to looking at a subrelation of \<^term>‹($⊢)›, which
       we call the ∗‹stronger theory› relation ‹(≼)›. Here we construe a
       ∗‹theory› as a list of propositions. We say theory ‹Γ› is
       ∗‹stronger than› ‹Σ› where, for each element ‹σ› in ‹Σ›, we can take
       an element ‹γ› of ‹Γ› ∗‹without replacement› such that ‹⊢ γ → σ›. ›

text ‹ To motivate this notion, let's reuse the metaphor that ‹Γ› and ‹Σ›
       are bags of balls of clay, and we need to show ‹Γ› is heavier without
       simply weighing the two bags. A sufficient (but incomplete) approach
       is to take each ball of clay ‹σ› in ‹Σ› and find another ball of clay
       ‹γ› in ‹Γ› (without replacement) that is heavier. This simple approach
       avoids the complexity of iteratively cutting up balls of clay. ›

definition (in implication_logic)
  stronger_theory_relation :: "'a list ⇒ 'a list ⇒ bool" (infix ‹≼› 100)
  where
    "Σ ≼ Γ =
       (∃ Φ. map snd Φ = Σ
            ∧ mset (map fst Φ) ⊆# mset Γ
            ∧ (∀ (γ,σ) ∈ set Φ. ⊢ γ → σ))"

abbreviation (in implication_logic)
  stronger_theory_relation_op :: "'a list ⇒ 'a list ⇒ bool" (infix ‹≽› 100)
  where
    "Γ ≽ Σ ≡ Σ ≼ Γ"

section ‹ The Stronger Theory Relation is a Preorder ›

text ‹ Next, we show that \<^term>‹(≼)› is a preorder by establishing reflexivity
       and transitivity. ›

text ‹ We first prove the following lemma with respect to multisets and
       stronger theories. ›

lemma (in implication_logic) msub_stronger_theory_intro:
  assumes "mset Σ ⊆# mset Γ"
  shows "Σ ≼ Γ"
proof -
  let ?ΔΣ = "map (λ x. (x,x)) Σ"
  have "map snd ?ΔΣ = Σ"
    by (induct Σ, simp, simp)
  moreover have "map fst ?ΔΣ = Σ"
    by (induct Σ, simp, simp)
  hence "mset (map fst ?ΔΣ) ⊆# mset Γ"
    using assms by simp
  moreover have "∀ (γ,σ) ∈ set ?ΔΣ. ⊢ γ → σ"
    by (induct Σ, simp, simp,
        metis list_implication.simps(1) list_implication_axiom_k)
  ultimately show ?thesis using stronger_theory_relation_def by (simp, blast)
qed

text ‹ The ∗‹reflexive› property immediately follows: ›

lemma (in implication_logic) stronger_theory_reflexive [simp]: "Γ ≼ Γ"
  using msub_stronger_theory_intro by auto

lemma (in implication_logic) weakest_theory [simp]: "[] ≼ Γ"
  using msub_stronger_theory_intro by auto

lemma (in implication_logic) stronger_theory_empty_list_intro [simp]:
  assumes "Γ ≼ []"
  shows "Γ = []"
  using assms stronger_theory_relation_def by simp

text ‹ Next, we turn to proving transitivity. We first prove two permutation
       theorems. ›

lemma (in implication_logic) stronger_theory_right_permutation:
  assumes "Γ ⇌ Δ"
      and "Σ ≼ Γ"
    shows "Σ ≼ Δ"
proof -
  from assms(1) have "mset Γ = mset Δ"
    by simp
  thus ?thesis
    using assms(2) stronger_theory_relation_def
    by fastforce
qed

lemma (in implication_logic) stronger_theory_left_permutation:
  assumes "Σ ⇌ Δ"
      and "Σ ≼ Γ"
    shows "Δ ≼ Γ"
proof -
  have "∀ Σ Γ. Σ ⇌ Δ ⟶ Σ ≼ Γ ⟶ Δ ≼ Γ"
  proof (induct Δ)
    case Nil
    then show ?case by simp
  next
    case (Cons δ Δ)
    {
      fix Σ Γ
      assume "Σ ⇌ (δ # Δ)" "Σ ≼ Γ"
      from this obtain Φ where Φ:
        "map snd Φ = Σ"
        "mset (map fst Φ) ⊆# mset Γ"
        "∀ (γ,δ) ∈ set Φ. ⊢ γ → δ"
        using stronger_theory_relation_def by fastforce
      with ‹Σ ⇌ (δ # Δ)› have "δ ∈# mset (map snd Φ)"
        by fastforce
      from this obtain γ where γ: "(γ, δ) ∈# mset Φ"
        by (induct Φ, fastforce+)
      let ?Φ⇩0 = "remove1 (γ, δ) Φ"
      let ?Σ⇩0 = "map snd ?Φ⇩0"
      from γ Φ(2) have "mset (map fst ?Φ⇩0) ⊆# mset (remove1 γ Γ)"
        by (metis ex_mset
                  list_subtract_monotonic
                  list_subtract_mset_homomorphism
                  mset_remove1
                  remove1_pairs_list_projections_fst)
      moreover have "mset ?Φ⇩0 ⊆# mset Φ" by simp
      with Φ(3) have "∀ (γ,δ) ∈ set ?Φ⇩0. ⊢ γ → δ" by fastforce
      ultimately have "?Σ⇩0 ≼ remove1 γ Γ"
        unfolding stronger_theory_relation_def by blast
      moreover have "Δ ⇌ (remove1 δ Σ)" using ‹Σ ⇌ (δ # Δ)›
        by (metis perm_remove_perm perm_sym remove_hd)
      moreover from γ Φ(1) have "mset ?Σ⇩0 = mset (remove1 δ Σ)"
        using remove1_pairs_list_projections_snd
        by fastforce
      hence "?Σ⇩0 ⇌ remove1 δ Σ"
        by blast
      ultimately have "Δ ≼ remove1 γ Γ" using Cons
        by presburger
      from this obtain Ψ⇩0 where Ψ⇩0:
        "map snd Ψ⇩0 = Δ"
        "mset (map fst Ψ⇩0) ⊆# mset (remove1 γ Γ)"
        "∀ (γ,δ) ∈ set Ψ⇩0. ⊢ γ → δ"
        using stronger_theory_relation_def by fastforce
      let ?Ψ = "(γ, δ) # Ψ⇩0"
      have "map snd ?Ψ = (δ # Δ)"
        by (simp add: Ψ⇩0(1))
      moreover have "mset (map fst ?Ψ) ⊆# mset (γ # (remove1 γ Γ))"
        using Ψ⇩0(2) by auto
      moreover from γ Φ(3) Ψ⇩0(3) have "∀ (γ,σ) ∈ set ?Ψ. ⊢ γ → σ" by auto
      ultimately have "(δ # Δ) ≼ (γ # (remove1 γ Γ))"
        unfolding stronger_theory_relation_def by metis
      moreover from γ Φ(2) have "γ ∈# mset Γ"
        using mset_subset_eqD by fastforce
      hence "(γ # (remove1 γ Γ)) ⇌ Γ"
        by auto
      ultimately have "(δ # Δ) ≼ Γ"
        using stronger_theory_right_permutation by blast
    }
    then show ?case by blast
  qed
  with assms show ?thesis by blast
qed

lemma (in implication_logic) stronger_theory_transitive:
  assumes "Σ ≼ Δ" and "Δ ≼ Γ"
    shows "Σ ≼ Γ"
proof -
  have "∀ Δ Γ. Σ ≼ Δ ⟶ Δ ≼ Γ ⟶ Σ ≼ Γ"
  proof (induct Σ)
    case Nil
    then show ?case using stronger_theory_relation_def by simp
  next
    case (Cons σ Σ)
    {
      fix Δ Γ
      assume "(σ # Σ) ≼ Δ" "Δ ≼ Γ"
      from this obtain Φ where Φ:
        "map snd Φ = σ # Σ"
        "mset (map fst Φ) ⊆# mset Δ"
        "∀ (δ,σ) ∈ set Φ. ⊢ δ → σ"
        using stronger_theory_relation_def by (simp, metis)
      let ?δ = "fst (hd Φ)"
      from Φ(1) have "Φ ≠ []" by (induct Φ, simp+)
      hence "?δ ∈# mset (map fst Φ)" by (induct Φ, simp+)
      with Φ(2) have "?δ ∈# mset Δ" by (meson mset_subset_eqD)
      hence "mset (map fst (remove1 (hd Φ) Φ)) ⊆# mset (remove1 ?δ Δ)"
        using ‹Φ ≠ []› Φ(2)
        by (simp,
            metis
              diff_single_eq_union
              hd_in_set
              image_mset_add_mset
              insert_subset_eq_iff
              set_mset_mset)
      moreover have "remove1 (hd Φ) Φ = tl Φ"
        using ‹Φ ≠ []›
        by (induct Φ, simp+)
      moreover from Φ(1) have "map snd (tl Φ) = Σ"
        by (simp add: map_tl)
      moreover from Φ(3) have "∀ (δ,σ) ∈ set (tl Φ). ⊢ δ → σ"
        by (simp add: ‹Φ ≠ []› list.set_sel(2))
      ultimately have "Σ ≼ remove1 ?δ Δ"
        using stronger_theory_relation_def by auto
      from ‹?δ ∈# mset Δ› have "?δ # (remove1 ?δ Δ) ⇌ Δ"
        by fastforce
      with ‹Δ ≼ Γ› have "(?δ # (remove1 ?δ Δ)) ≼ Γ"
        using stronger_theory_left_permutation perm_sym by blast
      from this obtain Ψ where Ψ:
        "map snd Ψ = (?δ # (remove1 ?δ Δ))"
        "mset (map fst Ψ) ⊆# mset Γ"
        "∀ (γ,δ) ∈ set Ψ. ⊢ γ → δ"
        using stronger_theory_relation_def by (simp, metis)
      let ?γ = "fst (hd Ψ)"
      from Ψ(1) have "Ψ ≠ []" by (induct Ψ, simp+)
      hence "?γ ∈# mset (map fst Ψ)" by (induct Ψ, simp+)
      with Ψ(2) have "?γ ∈# mset Γ" by (meson mset_subset_eqD)
      hence "mset (map fst (remove1 (hd Ψ) Ψ)) ⊆# mset (remove1 ?γ Γ)"
        using ‹Ψ ≠ []› Ψ(2)
        by (simp,
            metis
              diff_single_eq_union
              hd_in_set
              image_mset_add_mset
              insert_subset_eq_iff
              set_mset_mset)
      moreover from ‹Ψ ≠ []› have "remove1 (hd Ψ) Ψ = tl Ψ"
        by (induct Ψ, simp+)
      moreover from Ψ(1) have "map snd (tl Ψ) = (remove1 ?δ Δ)"
        by (simp add: map_tl)
      moreover from Ψ(3) have "∀ (γ,δ) ∈ set (tl Ψ). ⊢ γ → δ"
        by (simp add: ‹Ψ ≠ []› list.set_sel(2))
      ultimately have "remove1 ?δ Δ ≼ remove1 ?γ Γ"
        using stronger_theory_relation_def by auto
      with ‹Σ ≼ remove1 ?δ Δ› Cons.hyps have "Σ ≼ remove1 ?γ Γ"
        by blast
      from this obtain Ω⇩0 where Ω⇩0:
        "map snd Ω⇩0 = Σ"
        "mset (map fst Ω⇩0) ⊆# mset (remove1 ?γ Γ)"
        "∀ (γ,σ) ∈ set Ω⇩0. ⊢ γ → σ"
        using stronger_theory_relation_def by (simp, metis)
      let ?Ω = "(?γ, σ) # Ω⇩0"
      from Ω⇩0(1) have "map snd ?Ω = σ # Σ" by simp
      moreover from Ω⇩0(2) have "mset (map fst ?Ω) ⊆# mset (?γ # (remove1 ?γ Γ))"
        by simp
      moreover from Φ(1) Ψ(1) have "σ = snd (hd Φ)" "?δ = snd (hd Ψ)" by fastforce+
      with Φ(3) Ψ(3) ‹Φ ≠ []› ‹Ψ ≠ []› hd_in_set have "⊢ ?δ → σ" "⊢ ?γ → ?δ"
        by fastforce+
      hence "⊢ ?γ → σ" using modus_ponens hypothetical_syllogism by blast
      with Ω⇩0(3) have "∀ (γ,σ) ∈ set ?Ω. ⊢ γ → σ"
        by auto
      ultimately have "(σ # Σ) ≼ (?γ # (remove1 ?γ Γ))"
        unfolding stronger_theory_relation_def
        by metis
      moreover from ‹?γ ∈# mset Γ› have "(?γ # (remove1 ?γ Γ)) ⇌ Γ"
        by force
      ultimately have "(σ # Σ) ≼ Γ"
        using stronger_theory_right_permutation
        by blast
    }
    then show ?case by blast
  qed
  thus ?thesis using assms by blast
qed

section ‹ The Stronger Theory Relation is a Subrelation of of Measure Deduction ›

text ‹ Next, we show that ‹ Γ ≽ Σ › implies ‹Γ $⊢ Σ›. Before doing so we
       establish several helpful properties regarding the stronger theory
       relation \<^term>‹(≽)›. ›

lemma (in implication_logic) stronger_theory_witness:
  assumes "σ ∈ set Σ"
    shows "Σ ≼ Γ = (∃ γ ∈ set Γ. ⊢ γ → σ ∧ (remove1 σ Σ) ≼ (remove1 γ Γ))"
proof (rule iffI)
  assume "Σ ≼ Γ"
  from this obtain Φ where Φ:
    "map snd Φ = Σ"
    "mset (map fst Φ) ⊆# mset Γ"
    "∀ (γ,σ) ∈ set Φ. ⊢ γ → σ"
    unfolding stronger_theory_relation_def by blast
  from assms Φ(1) obtain γ where γ: "(γ, σ) ∈# mset Φ"
    by (induct Φ, fastforce+)
  hence "γ ∈# mset (map fst Φ)" by force
  hence "γ ∈# mset Γ" using Φ(2)
    by (meson mset_subset_eqD)
  moreover
  let ?Φ⇩0 = "remove1 (γ, σ) Φ"
  let ?Σ⇩0 = "map snd ?Φ⇩0"
  from γ Φ(2) have "mset (map fst ?Φ⇩0) ⊆# mset (remove1 γ Γ)"
    by (metis
          ex_mset
          list_subtract_monotonic
          list_subtract_mset_homomorphism
          remove1_pairs_list_projections_fst
          mset_remove1)
  moreover have "mset ?Φ⇩0 ⊆# mset Φ" by simp
  with Φ(3) have "∀ (γ,σ) ∈ set ?Φ⇩0. ⊢ γ → σ" by fastforce
  ultimately have "?Σ⇩0 ≼ remove1 γ Γ"
    unfolding stronger_theory_relation_def by blast
  moreover from γ Φ(1) have "mset ?Σ⇩0 = mset (remove1 σ Σ)"
    using remove1_pairs_list_projections_snd
    by fastforce
  hence "?Σ⇩0 ⇌ remove1 σ Σ"
    by linarith
  ultimately have "remove1 σ Σ ≼ remove1 γ Γ"
    using stronger_theory_left_permutation
    by blast
  moreover from γ Φ(3) have "⊢ γ → σ" by (simp, fast)
  moreover from γ Φ(2) have "γ ∈# mset Γ"
    using mset_subset_eqD by fastforce
  ultimately show "∃ γ ∈ set Γ. ⊢ γ → σ ∧ (remove1 σ Σ) ≼ (remove1 γ Γ)" by auto
next
  assume "∃ γ ∈ set Γ. ⊢ γ → σ ∧ (remove1 σ Σ) ≼ (remove1 γ Γ)"
  from this obtain Φ γ where γ: "γ ∈ set Γ" "⊢ γ → σ"
                       and Φ: "map snd Φ = (remove1 σ Σ)"
                              "mset (map fst Φ) ⊆# mset (remove1 γ Γ)"
                              "∀ (γ,σ) ∈ set Φ. ⊢ γ → σ"
    unfolding stronger_theory_relation_def by blast
  let ?Φ = "(γ, σ) # Φ"
  from Φ(1) have "map snd ?Φ = σ # (remove1 σ Σ)" by simp
  moreover from Φ(2) γ(1) have "mset (map fst ?Φ) ⊆# mset Γ"
    by (simp add: insert_subset_eq_iff)
  moreover from Φ(3) γ(2) have "∀ (γ,σ) ∈ set ?Φ. ⊢ γ → σ"
    by auto
  ultimately have "(σ # (remove1 σ Σ)) ≼ Γ"
    unfolding stronger_theory_relation_def by metis
  moreover from assms have "σ # (remove1 σ Σ) ⇌ Σ"
    by force
  ultimately show "Σ ≼ Γ"
    using stronger_theory_left_permutation by blast
qed

lemma (in implication_logic) stronger_theory_cons_witness:
  "(σ # Σ) ≼ Γ = (∃ γ ∈ set Γ. ⊢ γ → σ ∧ Σ ≼ (remove1 γ Γ))"
proof -
  have "σ ∈# mset (σ # Σ)" by simp
  hence "(σ # Σ) ≼ Γ = (∃ γ ∈ set Γ. ⊢ γ → σ ∧ (remove1 σ (σ # Σ)) ≼ (remove1 γ Γ))"
    by (meson list.set_intros(1) stronger_theory_witness)
  thus ?thesis by simp
qed

lemma (in implication_logic) stronger_theory_left_cons:
  assumes "(σ # Σ) ≼ Γ"
  shows "Σ ≼ Γ"
proof -
  from assms obtain Φ where Φ:
    "map snd Φ = σ # Σ"
    "mset (map fst Φ) ⊆# mset Γ"
    "∀ (δ,σ) ∈ set Φ. ⊢ δ → σ"
    using stronger_theory_relation_def by (simp, metis)
  let ?Φ' = "remove1 (hd Φ) Φ"
  from Φ(1) have "map snd ?Φ' = Σ" by (induct Φ, simp+)
  moreover from Φ(2) have "mset (map fst ?Φ') ⊆# mset Γ"
    by (metis diff_subset_eq_self
              list_subtract.simps(1)
              list_subtract.simps(2)
              list_subtract_mset_homomorphism
              map_monotonic
              subset_mset.dual_order.trans)
  moreover from Φ(3) have "∀ (δ,σ) ∈ set ?Φ'. ⊢ δ → σ" by fastforce
  ultimately show ?thesis unfolding stronger_theory_relation_def by blast
qed

lemma (in implication_logic) stronger_theory_right_cons:
  assumes "Σ ≼ Γ"
  shows "Σ ≼ (γ # Γ)"
proof -
  from assms obtain Φ where Φ:
    "map snd Φ = Σ"
    "mset (map fst Φ) ⊆# mset Γ"
    "∀(γ, σ)∈set Φ. ⊢ γ → σ"
    unfolding stronger_theory_relation_def
    by auto
  hence "mset (map fst Φ) ⊆# mset (γ # Γ)"
    by (metis Diff_eq_empty_iff_mset
              list_subtract.simps(2)
              list_subtract_mset_homomorphism
              mset_zero_iff remove1.simps(1))
  with Φ(1) Φ(3) show ?thesis
    unfolding stronger_theory_relation_def
    by auto
qed

lemma (in implication_logic) stronger_theory_left_right_cons:
  assumes "⊢ γ → σ"
      and "Σ ≼ Γ"
    shows "(σ # Σ) ≼ (γ # Γ)"
proof -
  from assms(2) obtain Φ where Φ:
    "map snd Φ = Σ"
    "mset (map fst Φ) ⊆# mset Γ"
    "∀(γ, σ)∈set Φ. ⊢ γ → σ"
    unfolding stronger_theory_relation_def
    by auto
  let ?Φ = "(γ, σ) # Φ"
  from assms(1) Φ have
    "map snd ?Φ = σ # Σ"
    "mset (map fst ?Φ) ⊆# mset (γ # Γ)"
    "∀(γ, σ)∈set ?Φ. ⊢ γ → σ"
    by fastforce+
  thus ?thesis
    unfolding stronger_theory_relation_def
    by metis
qed

lemma (in implication_logic) stronger_theory_relation_alt_def:
  "Σ ≼ Γ = (∃Φ. mset (map snd Φ) = mset Σ ∧
                 mset (map fst Φ) ⊆# mset Γ ∧
                 (∀(γ, σ)∈set Φ. ⊢ γ → σ))"
proof (induct Γ arbitrary: Σ)
  case Nil
    then show ?case
      using stronger_theory_empty_list_intro
            stronger_theory_reflexive
      by (simp, blast)
next
  case (Cons γ Γ)
  have "Σ ≼ (γ # Γ) = (∃Φ. mset (map snd Φ) = mset Σ ∧
                            mset (map fst Φ) ⊆# mset (γ # Γ) ∧
                            (∀(γ, σ) ∈ set Φ. ⊢ γ → σ))"
  proof (rule iffI)
    assume "Σ ≼ (γ # Γ)"
    thus "∃Φ. mset (map snd Φ) = mset Σ ∧
              mset (map fst Φ) ⊆# mset (γ # Γ) ∧
              (∀(γ, σ)∈set Φ. ⊢ γ → σ)"
      unfolding stronger_theory_relation_def
      by metis
  next
    assume "∃Φ. mset (map snd Φ) = mset Σ ∧
                mset (map fst Φ) ⊆# mset (γ # Γ) ∧
                (∀(γ, σ)∈set Φ. ⊢ γ → σ)"
    from this obtain Φ where Φ:
      "mset (map snd Φ) = mset Σ"
      "mset (map fst Φ) ⊆# mset (γ # Γ)"
      "∀(γ, σ)∈set Φ. ⊢ γ → σ"
      by metis
    show "Σ ≼ (γ # Γ)"
    proof (cases "∃ σ. (γ, σ) ∈ set Φ")
      assume "∃ σ. (γ, σ) ∈ set Φ"
      from this obtain σ where σ: "(γ, σ) ∈ set Φ" by auto
      let ?Φ = "remove1 (γ, σ) Φ"
      from σ have "mset (map snd ?Φ) = mset (remove1 σ Σ)"
        using Φ(1) remove1_pairs_list_projections_snd by force+
      moreover
      from σ have "mset (map fst ?Φ) = mset (remove1 γ (map fst Φ))"
        using Φ(1) remove1_pairs_list_projections_fst by force+
      with Φ(2) have "mset (map fst ?Φ) ⊆# mset Γ"
        by (simp add: subset_eq_diff_conv)
      moreover from Φ(3) have "∀(γ, σ)∈set ?Φ. ⊢ γ → σ"
        by fastforce
      ultimately have "remove1 σ Σ ≼ Γ" using Cons by blast
      from this obtain Ψ where Ψ:
        "map snd Ψ = remove1 σ Σ"
        "mset (map fst Ψ) ⊆# mset Γ"
        "∀(γ, σ)∈set Ψ. ⊢ γ → σ"
        unfolding stronger_theory_relation_def
        by blast
      let ?Ψ = "(γ, σ) # Ψ"
      from Ψ have "map snd ?Ψ = σ # (remove1 σ Σ)"
                  "mset (map fst ?Ψ) ⊆# mset (γ # Γ)"
        by simp+
      moreover from Φ(3) σ have "⊢ γ → σ" by auto
      with Ψ(3) have "∀(γ, σ)∈set ?Ψ. ⊢ γ → σ" by auto
      ultimately have "(σ # (remove1 σ Σ)) ≼ (γ # Γ)"
        unfolding stronger_theory_relation_def
        by metis
      moreover
      have "σ ∈ set Σ"
        by (metis Φ(1) σ set_mset_mset set_zip_rightD zip_map_fst_snd)
      hence "Σ ⇌ σ # (remove1 σ Σ)"
        by auto
      hence "Σ ≼ (σ # (remove1 σ Σ))"
        using stronger_theory_reflexive
              stronger_theory_right_permutation
        by blast
      ultimately show ?thesis
        using stronger_theory_transitive
        by blast
    next
      assume "∄σ. (γ, σ) ∈ set Φ"
      hence "γ ∉ set (map fst Φ)" by fastforce
      with Φ(2) have "mset (map fst Φ) ⊆# mset Γ"
        by (metis diff_single_trivial
                  in_multiset_in_set
                  insert_DiffM2
                  mset_remove1
                  remove_hd
                  subset_eq_diff_conv)
      hence "Σ ≼ Γ"
        using Cons Φ(1) Φ(3)
        by blast
      thus ?thesis
        using stronger_theory_right_cons
        by auto
    qed
  qed
  thus ?case by auto
qed

lemma (in implication_logic) stronger_theory_deduction_monotonic:
  assumes "Σ ≼ Γ"
      and "Σ :⊢ φ"
    shows "Γ :⊢ φ"
using assms
proof (induct Σ arbitrary: φ)
  case Nil
  then show ?case
    by (simp add: list_deduction_weaken)
next
  case (Cons σ Σ)
  assume "(σ # Σ) ≼ Γ" "(σ # Σ) :⊢ φ"
  hence "Σ :⊢ σ → φ" "Σ ≼ Γ"
    using
      list_deduction_theorem
      stronger_theory_left_cons
    by (blast, metis)
  with Cons have "Γ :⊢ σ → φ" by blast
  moreover
  have "σ ∈ set (σ # Σ)" by auto
  with ‹(σ # Σ) ≼ Γ› obtain γ where γ: "γ ∈ set Γ" "⊢ γ → σ"
    using stronger_theory_witness by blast
  hence "Γ :⊢ σ"
    using
      list_deduction_modus_ponens
      list_deduction_reflection
      list_deduction_weaken
    by blast
  ultimately have "Γ :⊢ φ"
    using list_deduction_modus_ponens by blast
  then show ?case by blast
qed

lemma (in classical_logic) measure_msub_left_monotonic:
  assumes "mset Σ ⊆# mset Γ"
      and "Σ $⊢ Φ"
    shows "Γ $⊢ Φ"
  using assms
proof (induct Φ arbitrary: Σ Γ)
  case Nil
  then show ?case by simp
next
  case (Cons φ Φ)
  from this obtain Ψ where Ψ:
    "mset (map snd Ψ) ⊆# mset Σ"
    "map (uncurry (⊔)) Ψ :⊢ φ"
    "map (uncurry (→)) Ψ @ Σ ⊖ (map snd Ψ) $⊢ Φ"
    using measure_deduction.simps(2) by blast
  let ?Ψ = "map snd Ψ"
  let ?Ψ' = "map (uncurry (→)) Ψ"
  let ?Σ' = "?Ψ' @ (Σ ⊖ ?Ψ)"
  let ?Γ' = "?Ψ' @ (Γ ⊖ ?Ψ)"
  from Ψ have "mset ?Ψ ⊆# mset Γ"
    using ‹mset Σ ⊆# mset Γ› subset_mset.trans by blast
  moreover have "mset (Σ ⊖ ?Ψ) ⊆# mset (Γ ⊖ ?Ψ)"
    by (metis ‹mset Σ ⊆# mset Γ› list_subtract_monotonic)
  hence "mset ?Σ' ⊆# mset ?Γ'"
    by simp
  with Cons.hyps Ψ(3) have "?Γ' $⊢ Φ" by blast
  ultimately have "Γ $⊢ (φ # Φ)"
    using Ψ(2) by fastforce
  then show ?case
    by simp
qed

lemma (in classical_logic) witness_weaker_theory:
  assumes "mset (map snd Σ) ⊆# mset Γ"
  shows "map (uncurry (⊔)) Σ ≼ Γ"
proof -
  have "∀ Γ. mset (map snd Σ) ⊆# mset Γ ⟶ map (uncurry (⊔)) Σ ≼ Γ"
  proof (induct Σ)
    case Nil
    then show ?case by simp
  next
    case (Cons σ Σ)
    {
      fix Γ
      assume "mset (map snd (σ # Σ)) ⊆# mset Γ"
      hence "mset (map snd Σ) ⊆# mset (remove1 (snd σ) Γ)"
        by (simp add: insert_subset_eq_iff)
      with Cons have "map (uncurry (⊔)) Σ ≼ remove1 (snd σ) Γ" by blast
      moreover have "uncurry (⊔) = (λ σ. fst σ ⊔ snd σ)" by fastforce
      hence "uncurry (⊔) σ = fst σ ⊔ snd σ" by simp
      moreover have "⊢ snd σ → (fst σ ⊔ snd σ)"
        unfolding disjunction_def
        by (simp add: axiom_k)
      ultimately have "map (uncurry (⊔)) (σ # Σ) ≼ (snd σ # (remove1 (snd σ) Γ))"
        by (simp add: stronger_theory_left_right_cons)
      moreover have "mset (snd σ # (remove1 (snd σ) Γ)) = mset Γ"
        using ‹mset (map snd (σ # Σ)) ⊆# mset Γ›
        by (simp, meson insert_DiffM mset_subset_eq_insertD)
      ultimately have "map (uncurry (⊔)) (σ # Σ) ≼ Γ"
        unfolding stronger_theory_relation_alt_def
        by simp
    }
    then show ?case by blast
  qed
  with assms show ?thesis by simp
qed

lemma (in implication_logic) stronger_theory_combine:
  assumes "Φ ≼ Δ"
      and "Ψ ≼ Γ"
    shows "(Φ @ Ψ) ≼ (Δ @ Γ)"
proof -
  have "∀ Φ. Φ ≼ Δ ⟶ (Φ @ Ψ) ≼ (Δ @ Γ)"
  proof (induct Δ)
    case Nil
    then show ?case
      using assms(2) stronger_theory_empty_list_intro by fastforce
  next
    case (Cons δ Δ)
    {
      fix Φ
      assume "Φ ≼ (δ # Δ)"
      from this obtain Σ where Σ:
        "map snd Σ = Φ"
        "mset (map fst Σ) ⊆# mset (δ # Δ)"
        "∀ (δ,φ) ∈ set Σ. ⊢ δ → φ"
        unfolding stronger_theory_relation_def
        by blast
      have "(Φ @ Ψ) ≼ ((δ # Δ) @ Γ)"
      proof (cases "∃ φ . (δ, φ) ∈ set Σ")
        assume "∃ φ . (δ, φ) ∈ set Σ"
        from this obtain φ where φ: "(δ, φ) ∈ set Σ" by auto
        let ?Σ = "remove1 (δ, φ) Σ"
        from φ Σ(1) have "mset (map snd ?Σ) = mset (remove1 φ Φ)"
          using remove1_pairs_list_projections_snd by fastforce
        moreover from φ have "mset (map fst ?Σ) = mset (remove1 δ (map fst Σ))"
          using remove1_pairs_list_projections_fst by fastforce
        hence "mset (map fst ?Σ) ⊆# mset Δ"
          using Σ(2) mset.simps(1) subset_eq_diff_conv by force
        moreover from Σ(3) have "∀ (δ,φ) ∈ set ?Σ. ⊢ δ → φ" by auto
        ultimately have "remove1 φ Φ ≼ Δ"
          unfolding stronger_theory_relation_alt_def by blast
        hence "(remove1 φ Φ @ Ψ) ≼ (Δ @ Γ)" using Cons by auto
        from this obtain Ω where Ω:
          "map snd Ω = (remove1 φ Φ) @ Ψ"
          "mset (map fst Ω) ⊆# mset (Δ @ Γ)"
          "∀ (α,β) ∈ set Ω. ⊢ α → β"
          unfolding stronger_theory_relation_def
          by blast
        let ?Ω = "(δ, φ) # Ω"
        have "map snd ?Ω = φ # remove1 φ Φ @ Ψ"
          using Ω(1) by simp
        moreover have "mset (map fst ?Ω) ⊆# mset ((δ # Δ) @ Γ)"
          using Ω(2) by simp
        moreover have "⊢ δ → φ"
          using Σ(3) φ by blast
        hence "∀ (α,β) ∈ set ?Ω. ⊢ α → β" using Ω(3) by auto
        ultimately have "(φ # remove1 φ Φ @ Ψ) ≼ ((δ # Δ) @ Γ)"
          by (metis stronger_theory_relation_def)
        moreover have "φ ∈ set Φ"
          using Σ(1) φ by force
        hence "(φ # remove1 φ Φ) ⇌ Φ"
          by force
        hence "(φ # remove1 φ Φ @ Ψ) ⇌ Φ @ Ψ"
          by (metis append_Cons perm_append2)
        ultimately show ?thesis
          using stronger_theory_left_permutation by blast
      next
        assume "∄φ. (δ, φ) ∈ set Σ"
        hence "δ ∉ set (map fst Σ)"
              "mset Δ + add_mset δ (mset []) = mset (δ # Δ)"
          by auto
        hence "mset (map fst Σ) ⊆# mset Δ"
          by (metis (no_types) ‹mset (map fst Σ) ⊆# mset (δ # Δ)›
                               diff_single_trivial
                               mset.simps(1)
                               set_mset_mset
                               subset_eq_diff_conv)
        with Σ(1) Σ(3) have "Φ ≼ Δ"
          unfolding stronger_theory_relation_def
          by blast
        hence "(Φ @ Ψ) ≼ (Δ @ Γ)" using Cons by auto
        then show ?thesis
          by (simp add: stronger_theory_right_cons)
      qed
    }
    then show ?case by blast
  qed
  thus ?thesis using assms by blast
qed

text ‹ We now turn to proving that \<^term>‹(≽)› is a subrelation of \<^term>‹(:⊢)›. ›

lemma (in classical_logic) stronger_theory_to_measure_deduction:
  assumes "Γ ≽ Σ"
  shows "Γ $⊢ Σ"
proof -
  have "∀ Γ. Σ ≼ Γ ⟶ Γ $⊢ Σ"
  proof (induct Σ)
    case Nil
    then show ?case by fastforce
  next
    case (Cons σ Σ)
    {
      fix Γ
      assume "(σ # Σ) ≼ Γ"
      from this obtain γ where γ: "γ ∈ set Γ" "⊢ γ → σ" "Σ ≼ (remove1 γ Γ)"
        using stronger_theory_cons_witness by blast
      let ?Φ = "[(γ,γ)]"
      from γ Cons have "(remove1 γ Γ) $⊢ Σ" by blast
      moreover have "mset (remove1 γ Γ) ⊆# mset (map (uncurry (→)) ?Φ @ Γ ⊖ (map snd ?Φ))"
        by simp
      ultimately have "map (uncurry (→)) ?Φ @ Γ ⊖ (map snd ?Φ) $⊢ Σ"
        using measure_msub_left_monotonic by blast
      moreover have "map (uncurry (⊔)) ?Φ :⊢ σ"
        by (simp, metis γ(2)
                        Peirces_law
                        disjunction_def
                        list_deduction_def
                        list_deduction_modus_ponens
                        list_deduction_weaken
                        list_implication.simps(1)
                        list_implication.simps(2))
      moreover from γ(1) have "mset (map snd ?Φ) ⊆# mset Γ" by simp
      ultimately have "Γ $⊢ (σ # Σ)"
        using measure_deduction.simps(2) by blast
    }
    then show ?case by blast
  qed
  thus ?thesis using assms by blast
qed

section ‹ Measure Deduction is a Preorder ›

text ‹ We next show that measure deduction is a preorder. ›

text ‹ Reflexivity follows immediately because \<^term>‹(≼)› is a subrelation
       and is itself reflexive. ›

theorem (in classical_logic) measure_reflexive: "Γ $⊢ Γ"
  by (simp add: stronger_theory_to_measure_deduction)

text ‹ Transitivity is complicated. It requires constructing many witnesses
       and involves a lot of metatheorems. Below we provide various witness
       constructions that allow us to establish \<^term>‹Γ $⊢ Λ ⟹ Λ $⊢ Δ ⟹ Γ $⊢ Δ›. ›

primrec (in implication_logic)
  first_component :: "('a × 'a) list ⇒ ('a × 'a) list ⇒ ('a × 'a) list" (‹𝔄›)
  where
    "𝔄 Ψ [] = []"
  | "𝔄 Ψ (δ # Δ) =
       (case find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ of
             None ⇒ 𝔄 Ψ Δ
           | Some ψ ⇒ ψ # (𝔄 (remove1 ψ Ψ) Δ))"

primrec (in implication_logic)
  second_component :: "('a × 'a) list ⇒ ('a × 'a) list ⇒ ('a × 'a) list" (‹𝔅›)
  where
    "𝔅 Ψ [] = []"
  | "𝔅 Ψ (δ # Δ) =
       (case find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ of
             None ⇒ 𝔅 Ψ Δ
           | Some ψ ⇒ δ # (𝔅 (remove1 ψ Ψ) Δ))"

lemma (in implication_logic) first_component_second_component_mset_connection:
  "mset (map (uncurry (→)) (𝔄 Ψ Δ)) = mset (map snd (𝔅 Ψ Δ))"
proof -
  have "∀ Ψ. mset (map (uncurry (→)) (𝔄 Ψ Δ)) = mset (map snd (𝔅 Ψ Δ))"
  proof (induct Δ)
    case Nil
    then show ?case by simp
  next
    case (Cons δ Δ)
    {
      fix Ψ
      have "mset (map (uncurry (→)) (𝔄 Ψ (δ # Δ))) =
            mset (map snd (𝔅 Ψ (δ # Δ)))"
      proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
        case True
        then show ?thesis using Cons by simp
      next
        case False
        from this obtain ψ where
          "find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
          "uncurry (→) ψ = snd δ"
          using find_Some_predicate
          by fastforce
        then show ?thesis using Cons by simp
      qed
    }
    then show ?case by blast
  qed
  thus ?thesis by blast
qed

lemma (in implication_logic) second_component_right_empty [simp]:
  "𝔅 [] Δ = []"
  by (induct Δ, simp+)

lemma (in implication_logic) first_component_msub:
  "mset (𝔄 Ψ Δ) ⊆# mset Ψ"
proof -
  have "∀ Ψ. mset (𝔄 Ψ Δ) ⊆# mset Ψ"
  proof(induct Δ)
    case Nil
    then show ?case by simp
  next
    case (Cons δ Δ)
    {
      fix Ψ
      have "mset (𝔄 Ψ (δ # Δ)) ⊆# mset Ψ"
      proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
        case True
        then show ?thesis using Cons by simp
      next
        case False
        from this obtain ψ where
          ψ: "find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
             "ψ ∈ set Ψ"
          using find_Some_set_membership
          by fastforce
        have "mset (𝔄 (remove1 ψ Ψ) Δ) ⊆# mset (remove1 ψ Ψ)"
          using Cons by metis
        thus ?thesis using ψ by (simp add: insert_subset_eq_iff)
      qed
    }
    then show ?case by blast
  qed
  thus ?thesis by blast
qed

lemma (in implication_logic) second_component_msub:
  "mset (𝔅 Ψ Δ) ⊆# mset Δ"
proof -
  have "∀Ψ. mset (𝔅 Ψ Δ) ⊆# mset Δ"
  proof (induct Δ)
    case Nil
    then show ?case by simp
  next
    case (Cons δ Δ)
    {
      fix Ψ
      have "mset (𝔅 Ψ (δ # Δ)) ⊆# mset (δ # Δ)"
      using Cons
      by (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None",
           simp,
           metis add_mset_remove_trivial
                 diff_subset_eq_self
                 subset_mset.order_trans,
           auto)
    }
    thus ?case by blast
  qed
  thus ?thesis by blast
qed

lemma (in implication_logic) second_component_snd_projection_msub:
  "mset (map snd (𝔅 Ψ Δ)) ⊆# mset (map (uncurry (→)) Ψ)"
proof -
  have "∀Ψ. mset (map snd (𝔅 Ψ Δ)) ⊆# mset (map (uncurry (→)) Ψ)"
  proof (induct Δ)
    case Nil
    then show ?case by simp
  next
    case (Cons δ Δ)
    {
      fix Ψ
      have "mset (map snd (𝔅 Ψ (δ # Δ))) ⊆# mset (map (uncurry (→)) Ψ)"
      proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
        case True
        then show ?thesis
          using Cons by simp
      next
        case False
        from this obtain ψ where ψ:
          "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = Some ψ"
          by auto
        hence "𝔅 Ψ (δ # Δ) = δ # (𝔅 (remove1 ψ Ψ) Δ)"
          using ψ by fastforce
        with Cons have "mset (map snd (𝔅 Ψ (δ # Δ))) ⊆#
                        mset ((snd δ) # map (uncurry (→)) (remove1 ψ Ψ))"
          by (simp, metis mset_map mset_remove1)
        moreover from ψ have "snd δ = (uncurry (→)) ψ"
          using find_Some_predicate by fastforce
        ultimately have
          "mset (map snd (𝔅 Ψ (δ # Δ))) ⊆#
             mset (map (uncurry (→)) (ψ # (remove1 ψ Ψ)))"
          by simp
        thus ?thesis
          by (metis
                first_component_msub
                first_component_second_component_mset_connection
                map_monotonic)
      qed
    }
    thus ?case by blast
  qed
  thus ?thesis by blast
qed

lemma (in implication_logic) second_component_diff_msub:
  assumes "mset (map snd Δ) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ (map snd Ψ))"
  shows "mset (map snd (Δ ⊖ (𝔅 Ψ Δ))) ⊆# mset (Γ ⊖ (map snd Ψ))"
proof -
  have "∀ Ψ Γ. mset (map snd Δ) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ (map snd Ψ)) ⟶
               mset (map snd (Δ ⊖ (𝔅 Ψ Δ))) ⊆# mset (Γ ⊖ (map snd Ψ))"
  proof (induct Δ)
    case Nil
    then show ?case by simp
  next
    case (Cons δ Δ)
    {
      fix Ψ Γ
      assume ♢: "mset (map snd (δ # Δ)) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ map snd Ψ)"
      have "mset (map snd ((δ # Δ) ⊖ 𝔅 Ψ (δ # Δ))) ⊆# mset (Γ ⊖ map snd Ψ)"
      proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
        case True
        hence A: "snd δ ∉ set (map (uncurry (→)) Ψ)"
        proof (induct Ψ)
          case Nil
          then show ?case by simp
        next
          case (Cons ψ Ψ)
          then show ?case
            by (cases "uncurry (→) ψ = snd δ", simp+)
        qed
        moreover have
          "mset (map snd Δ)
              ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ map snd Ψ) - {#snd δ#}"
          using ♢ insert_subset_eq_iff by fastforce
        ultimately have
          "mset (map snd Δ)
             ⊆# mset (map (uncurry (→)) Ψ @ (remove1 (snd δ) Γ)
                          ⊖ map snd Ψ)"
          by (metis (no_types)
                mset_remove1
                union_code
                list_subtract.simps(2)
                list_subtract_remove1_cons_perm
                remove1_append)
        hence B: "mset (map snd (Δ ⊖ (𝔅 Ψ Δ))) ⊆# mset (remove1 (snd δ) Γ ⊖ (map snd Ψ))"
          using Cons by blast
        have C: "snd δ ∈# mset (snd δ # map snd Δ @
                                  (map (uncurry (→)) Ψ @ Γ ⊖ map snd Ψ) ⊖ (snd δ # map snd Δ))"
          by (meson in_multiset_in_set list.set_intros(1))
        have "mset (map snd (δ # Δ))
           + (mset (map (uncurry (→)) Ψ @ Γ ⊖ map snd Ψ)
              - mset (map snd (δ # Δ)))
         = mset (map (uncurry (→)) Ψ @ Γ ⊖ map snd Ψ)"
          using ♢ subset_mset.add_diff_inverse by blast
        then have "snd δ ∈# mset (map (uncurry (→)) Ψ) + (mset Γ - mset (map snd Ψ))"
          using C by simp
        with A have "snd δ ∈ set Γ"
          by (metis (no_types) diff_subset_eq_self
                               in_multiset_in_set
                               subset_mset.add_diff_inverse
                               union_iff)
        have D: "𝔅 Ψ Δ = 𝔅 Ψ (δ # Δ)"
          using ‹find (λψ. uncurry (→) ψ = snd δ) Ψ = None›
          by simp
        obtain diff :: "'a list ⇒ 'a list ⇒ 'a list" where
          "∀x0 x1. (∃v2. x1 @ v2 ⇌ x0) = (x1 @ diff x0 x1 ⇌ x0)"
          by moura
        then have E:
            "mset (map snd (𝔅 Ψ (δ # Δ))
                  @ diff (map (uncurry (→)) Ψ) (map snd (𝔅 Ψ (δ # Δ))))
             = mset (map (uncurry (→)) Ψ)"
          by (meson second_component_snd_projection_msub mset_le_perm_append)
        have F: "∀a m ma. (add_mset (a::'a) m ⊆# ma) = (a ∈# ma ∧ m ⊆# ma - {#a#})"
          using insert_subset_eq_iff by blast
        then have "snd δ ∈# mset (map snd (𝔅 Ψ (δ # Δ))
                                  @ diff (map (uncurry (→)) Ψ) (map snd (𝔅 Ψ (δ # Δ))))
                          + mset (Γ ⊖ map snd Ψ)"
          using E ♢ by force
        then have "snd δ ∈# mset (Γ ⊖ map snd Ψ)"
          using A E by (metis (no_types) in_multiset_in_set union_iff)
        then have G: "add_mset (snd δ) (mset (map snd (Δ ⊖ 𝔅 Ψ Δ))) ⊆# mset (Γ ⊖ map snd Ψ)"
          using B F by force
        have H: "∀ps psa f. ¬ mset (ps::('a × 'a) list) ⊆# mset psa ∨
                              mset ((map f psa::'a list) ⊖ map f ps) = mset (map f (psa ⊖ ps))"
          using map_list_subtract_mset_equivalence by blast
        have "snd δ ∉# mset (map snd (𝔅 Ψ (δ # Δ)))
                     + mset (diff (map (uncurry (→)) Ψ) (map snd (𝔅 Ψ (δ # Δ))))"
          using A E by auto
        then have "add_mset (snd δ) (mset (map snd (Δ ⊖ 𝔅 Ψ Δ)))
                 = mset (map snd (δ # Δ) ⊖ map snd (𝔅 Ψ (δ # Δ)))"
          using D H second_component_msub by auto
        then show ?thesis
          using G H by (metis (no_types) second_component_msub)
      next
        case False
        from this obtain ψ where ψ: "find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
          by auto
        let ?Ψ' = "remove1 ψ Ψ"
        let ?Γ' = "remove1 (snd ψ) Γ"
        have "snd δ = uncurry (→) ψ"
             "ψ ∈ set Ψ"
             "mset ((δ # Δ) ⊖ 𝔅 Ψ (δ # Δ)) =
              mset (Δ ⊖ 𝔅 ?Ψ' Δ)"
          using ψ find_Some_predicate find_Some_set_membership
          by fastforce+
        moreover
        have "mset (Γ ⊖ map snd Ψ) = mset (?Γ' ⊖ map snd ?Ψ')"
          by (simp, metis ‹ψ ∈ set Ψ› image_mset_add_mset in_multiset_in_set insert_DiffM)
        moreover
        obtain search :: "('a × 'a) list ⇒ ('a × 'a ⇒ bool) ⇒ 'a × 'a" where
          "∀xs P. (∃x. x ∈ set xs ∧ P x) = (search xs P ∈ set xs ∧ P (search xs P))"
          by moura
        then have "∀p ps. (find p ps ≠ None ∨ (∀pa. pa ∉ set ps ∨ ¬ p pa))
                        ∧ (find p ps = None ∨ search ps p ∈ set ps ∧ p (search ps p))"
          by (metis (full_types) find_None_iff)
        then have "(find (λp. uncurry (→) p = snd δ) Ψ ≠ None
                    ∨ (∀p. p ∉ set Ψ ∨ uncurry (→) p ≠ snd δ))
                 ∧ (find (λp. uncurry (→) p = snd δ) Ψ = None
                    ∨ search Ψ (λp. uncurry (→) p = snd δ) ∈ set Ψ
                    ∧ uncurry (→) (search Ψ (λp. uncurry (→) p = snd δ)) = snd δ)"
          by blast
        hence "snd δ ∈ set (map (uncurry (→)) Ψ)"
          by (metis (no_types) False image_eqI image_set)
        moreover
        have A: "add_mset (uncurry (→) ψ) (image_mset snd (mset Δ))
              = image_mset snd (add_mset δ (mset Δ))"
          by (simp add: ‹snd δ = uncurry (→) ψ›)
        have B: "{#snd δ#} ⊆# image_mset (uncurry (→)) (mset Ψ)"
          using ‹snd δ ∈ set (map (uncurry (→)) Ψ)› by force
        have "image_mset (uncurry (→)) (mset Ψ) - {#snd δ#}
            = image_mset (uncurry (→)) (mset (remove1 ψ Ψ))"
          by (simp add: ‹ψ ∈ set Ψ› ‹snd δ = uncurry (→) ψ› image_mset_Diff)
        then have "mset (map snd (Δ ⊖ 𝔅 (remove1 ψ Ψ) Δ))
                ⊆# mset (remove1 (snd ψ) Γ ⊖ map snd (remove1 ψ Ψ))"
          by (metis (no_types)
                    A B ♢ Cons.hyps
                    calculation(1)
                    calculation(4)
                    insert_subset_eq_iff
                    mset.simps(2)
                    mset_map
                    subset_mset.diff_add_assoc2
                    union_code)
        ultimately show ?thesis by fastforce
      qed
    }
    then show ?case by blast
  qed
  thus ?thesis using assms by auto
qed

primrec (in classical_logic)
  merge_witness :: "('a × 'a) list ⇒ ('a × 'a) list ⇒ ('a × 'a) list" (‹𝔍›)
  where
    "𝔍 Ψ [] = Ψ"
  | "𝔍 Ψ (δ # Δ) =
       (case find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ of
             None ⇒ δ # 𝔍 Ψ Δ
           | Some ψ ⇒ (fst δ ⊓ fst ψ, snd ψ) # (𝔍 (remove1 ψ Ψ) Δ))"

lemma (in classical_logic) merge_witness_right_empty [simp]:
  "𝔍 [] Δ = Δ"
  by (induct Δ, simp+)

lemma (in classical_logic) second_component_merge_witness_snd_projection:
  "mset (map snd Ψ @ map snd (Δ ⊖ (𝔅 Ψ Δ))) = mset (map snd (𝔍 Ψ Δ))"
proof -
  have "∀ Ψ. mset (map snd Ψ @ map snd (Δ ⊖ (𝔅 Ψ Δ))) = mset (map snd (𝔍 Ψ Δ))"
  proof (induct Δ)
    case Nil
    then show ?case by simp
  next
    case (Cons δ Δ)
    {
      fix Ψ
      have "mset (map snd Ψ @ map snd ((δ # Δ) ⊖ 𝔅 Ψ (δ # Δ))) =
            mset (map snd (𝔍 Ψ (δ # Δ)))"
      proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
        case True
        then show ?thesis
          using Cons
          by (simp,
              metis (no_types, lifting)
                    ab_semigroup_add_class.add_ac(1)
                    add_mset_add_single
                    image_mset_single
                    image_mset_union
                    second_component_msub
                    subset_mset.add_diff_assoc2)
      next
        case False
        from this obtain ψ where ψ: "find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
          by auto
        moreover have "ψ ∈ set Ψ"
          by (meson ψ find_Some_set_membership)
        moreover
        let ?Ψ' = "remove1 ψ Ψ"
        from Cons have
          "mset (map snd ?Ψ' @ map snd (Δ ⊖ 𝔅 ?Ψ' Δ)) =
            mset (map snd (𝔍 ?Ψ' Δ))"
          by blast
        ultimately show ?thesis
          by (simp,
              metis (no_types, lifting)
                    add_mset_remove_trivial_eq
                    image_mset_add_mset
                    in_multiset_in_set
                    union_mset_add_mset_left)
      qed
    }
    then show ?case by blast
  qed
  thus ?thesis by blast
qed

lemma (in classical_logic) second_component_merge_witness_stronger_theory:
  "(map (uncurry (→)) Δ @ map (uncurry (→)) Ψ ⊖ map snd (𝔅 Ψ Δ)) ≼
    map (uncurry (→)) (𝔍 Ψ Δ)"
proof -
  have "∀ Ψ. (map (uncurry (→)) Δ @
              map (uncurry (→)) Ψ ⊖ map snd (𝔅 Ψ Δ)) ≼
              map (uncurry (→)) (𝔍 Ψ Δ)"
  proof (induct Δ)
    case Nil
    then show ?case
      by simp
  next
    case (Cons δ Δ)
    {
      fix Ψ
      have "⊢ (uncurry (→)) δ → (uncurry (→)) δ"
        using axiom_k modus_ponens implication_absorption by blast
      have
        "(map (uncurry (→)) (δ # Δ) @
          map (uncurry (→)) Ψ ⊖ map snd (𝔅 Ψ (δ # Δ))) ≼
          map (uncurry (→)) (𝔍 Ψ (δ # Δ))"
      proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
        case True
        thus ?thesis
          using Cons
                ‹⊢ (uncurry (→)) δ → (uncurry (→)) δ›
          by (simp, metis stronger_theory_left_right_cons)
      next
        case False
        from this obtain ψ where ψ: "find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
          by auto
        from ψ have "snd δ = uncurry (→) ψ"
          using find_Some_predicate by fastforce
        from ψ ‹snd δ = uncurry (→) ψ› have
          "mset (map (uncurry (→)) (δ # Δ) @
                   map (uncurry (→)) Ψ ⊖ map snd (𝔅 Ψ (δ # Δ))) =
           mset (map (uncurry (→)) (δ # Δ) @
                   map (uncurry (→)) (remove1 ψ Ψ) ⊖
                   map snd (𝔅 (remove1 ψ Ψ) Δ))"
          by (simp add: find_Some_set_membership image_mset_Diff)
        hence
          "(map (uncurry (→)) (δ # Δ) @
              map (uncurry (→)) Ψ ⊖ map snd (𝔅 Ψ (δ # Δ))) ≼
           (map (uncurry (→)) (δ # Δ) @
              map (uncurry (→)) (remove1 ψ Ψ) ⊖ map snd (𝔅 (remove1 ψ Ψ) Δ))"
          by (simp add: msub_stronger_theory_intro)
        with Cons ‹⊢ (uncurry (→)) δ → (uncurry (→)) δ› have
          "(map (uncurry (→)) (δ # Δ) @
            map (uncurry (→)) Ψ ⊖ map snd (𝔅 Ψ (δ # Δ)))
            ≼ ((uncurry (→)) δ # map (uncurry (→)) (𝔍 (remove1 ψ Ψ) Δ))"
          using stronger_theory_left_right_cons
                stronger_theory_transitive
          by fastforce
        moreover
        let ?α = "fst δ"
        let ?β = "fst ψ"
        let ?γ = "snd ψ"
        have "uncurry (→) = (λ δ. fst δ → snd δ)" by fastforce
        with ψ have "(uncurry (→)) δ = ?α → ?β → ?γ"
          using find_Some_predicate by fastforce
        hence "⊢ ((?α ⊓ ?β) → ?γ) → (uncurry (→)) δ"
          using biconditional_def curry_uncurry by auto
        with ψ have
          "((uncurry (→)) δ # map (uncurry (→)) (𝔍 (remove1 ψ Ψ) Δ)) ≼
           map (uncurry (→)) (𝔍 Ψ (δ # Δ))"
          using stronger_theory_left_right_cons by auto
        ultimately show ?thesis
          using stronger_theory_transitive
          by blast
      qed
    }
    then show ?case by simp
  qed
  thus ?thesis by simp
qed

lemma (in classical_logic) merge_witness_msub_intro:
  assumes "mset (map snd Ψ) ⊆# mset Γ"
      and "mset (map snd Δ) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ (map snd Ψ))"
    shows "mset (map snd (𝔍 Ψ Δ)) ⊆# mset Γ"
proof -
  have "∀Ψ Γ. mset (map snd Ψ) ⊆# mset Γ ⟶
               mset (map snd Δ) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ (map snd Ψ)) ⟶
               mset (map snd (𝔍 Ψ Δ)) ⊆# mset Γ"
  proof (induct Δ)
    case Nil
    then show ?case by simp
  next
    case (Cons δ Δ)
    {
      fix Ψ :: "('a × 'a) list"
      fix Γ :: "'a list"
      assume ♢: "mset (map snd Ψ) ⊆# mset Γ"
                "mset (map snd (δ # Δ)) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ (map snd Ψ))"
      have "mset (map snd (𝔍 Ψ (δ # Δ))) ⊆# mset Γ"
      proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
        case True
        hence "snd δ ∉ set (map (uncurry (→)) Ψ)"
        proof (induct Ψ)
          case Nil
          then show ?case by simp
        next
          case (Cons ψ Ψ)
          hence "uncurry (→) ψ ≠ snd δ" by fastforce
          with Cons show ?case by fastforce
        qed
        with ♢(2) have "snd δ ∈# mset (Γ ⊖ map snd Ψ)"
          using mset_subset_eq_insertD by fastforce
        with ♢(1) have "mset (map snd Ψ) ⊆# mset (remove1 (snd δ) Γ)"
          by (metis list_subtract_mset_homomorphism
                    mset_remove1
                    single_subset_iff
                    subset_mset.add_diff_assoc
                    subset_mset.add_diff_inverse
                    subset_mset.le_iff_add)
        moreover
        have "add_mset (snd δ) (mset (Γ ⊖ map snd Ψ) - {#snd δ#}) = mset (Γ ⊖ map snd Ψ)"
          by (meson ‹snd δ ∈# mset (Γ ⊖ map snd Ψ)› insert_DiffM)
        then have "image_mset snd (mset Δ) - (mset Γ - add_mset (snd δ) (image_mset snd (mset Ψ)))
               ⊆# {#x → y. (x, y) ∈# mset Ψ#}"
          using ♢(2) by (simp, metis add_mset_diff_bothsides
                                     list_subtract_mset_homomorphism
                                     mset_map subset_eq_diff_conv)
        hence "mset (map snd Δ)
           ⊆# mset (map (uncurry (→)) Ψ @ (remove1 (snd δ) Γ) ⊖ (map snd Ψ))"
          using subset_eq_diff_conv by (simp, blast)
        ultimately have "mset (map snd (𝔍 Ψ Δ)) ⊆# mset (remove1 (snd δ) Γ)"
          using Cons by blast
        hence "mset (map snd (δ # (𝔍 Ψ Δ))) ⊆# mset Γ"
          by (simp, metis ‹snd δ ∈# mset (Γ ⊖ map snd Ψ)›
                          cancel_ab_semigroup_add_class.diff_right_commute
                          diff_single_trivial
                          insert_subset_eq_iff
                          list_subtract_mset_homomorphism
                          multi_drop_mem_not_eq)
        with ‹find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None›
        show ?thesis
          by simp
      next
        case False
        from this obtain ψ where ψ:
          "find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
          by fastforce
        let ?χ = "fst ψ"
        let ?γ = "snd ψ"
        have "uncurry (→) = (λ ψ. fst ψ → snd ψ)"
          by fastforce
        moreover
        from this have "uncurry (→) ψ = ?χ → ?γ" by fastforce
        with ψ have A: "(?χ, ?γ) ∈ set Ψ"
                and B: "snd δ = ?χ → ?γ"
          using find_Some_predicate
          by (simp add: find_Some_set_membership, fastforce)
        let ?Ψ' = "remove1 (?χ, ?γ) Ψ"
        from B ♢(2) have
          "mset (map snd Δ) ⊆# mset (map (uncurry (→)) Ψ @ Γ ⊖ map snd Ψ) - {# ?χ → ?γ #}"
          by (simp add: insert_subset_eq_iff)
        moreover
        have "mset (map (uncurry (→)) Ψ)
            = add_mset (case (fst ψ, snd ψ) of (x, xa) ⇒ x → xa)
                       (image_mset (uncurry (→)) (mset (remove1 (fst ψ, snd ψ) Ψ)))"
          by (metis (no_types)
                A
                image_mset_add_mset
                in_multiset_in_set
                insert_DiffM
                mset_map
                mset_remove1
                uncurry_def)
        ultimately have
          "mset (map snd Δ) ⊆# mset (map (uncurry (→)) ?Ψ' @ Γ ⊖ map snd Ψ)"
          using
            add_diff_cancel_left'
            add_diff_cancel_right
            diff_diff_add_mset
            diff_subset_eq_self
            mset_append
            subset_eq_diff_conv
            subset_mset.diff_add
          by auto
        moreover from A B ♢
        have "mset (Γ ⊖ map snd Ψ) = mset((remove1 ?γ Γ) ⊖ (remove1 ?γ (map snd Ψ)))"
          using
            image_eqI
            prod.sel(2)
            set_map
          by force
        with A have
          "mset (Γ ⊖ map snd Ψ) = mset((remove1 ?γ Γ) ⊖ (map snd ?Ψ'))"
          by (metis
                remove1_pairs_list_projections_snd
                in_multiset_in_set
                list_subtract_mset_homomorphism
                mset_remove1)
        ultimately have
          "mset (map snd Δ) ⊆# mset (map (uncurry (→)) ?Ψ'
                                        @ (remove1 ?γ Γ)
                                        ⊖ map snd ?Ψ')"
          by simp
        hence "mset (map snd (𝔍 ?Ψ' Δ)) ⊆# mset (remove1 ?γ Γ)"
          using Cons ♢(1) A
          by (metis (no_types, lifting)
                    image_mset_add_mset
                    in_multiset_in_set
                    insert_DiffM
                    insert_subset_eq_iff
                    mset_map mset_remove1
                    prod.collapse)
        with ♢(1) A have "mset (map snd (𝔍 ?Ψ' Δ)) + {# ?γ #} ⊆# mset Γ"
          by (metis add_mset_add_single
                    image_eqI
                    insert_subset_eq_iff
                    mset_remove1
                    mset_subset_eqD
                    set_map
                    set_mset_mset
                    snd_conv)
        hence "mset (map snd ((fst δ ⊓ ?χ, ?γ) # (𝔍 ?Ψ' Δ))) ⊆# mset Γ"
          by simp
        moreover from ψ have
          "𝔍 Ψ (δ # Δ) = (fst δ ⊓ ?χ, ?γ) # (𝔍 ?Ψ' Δ)"
          by simp
        ultimately show ?thesis by simp
      qed
    }
    thus ?case by blast
  qed
  with assms show ?thesis by blast
qed

lemma (in classical_logic) right_merge_witness_stronger_theory:
  "map (uncurry (⊔)) Δ ≼ map (uncurry (⊔)) (𝔍 Ψ Δ)"
proof -
  have "∀ Ψ. map (uncurry (⊔)) Δ ≼ map (uncurry (⊔)) (𝔍 Ψ Δ)"
  proof (induct Δ)
    case Nil
    then show ?case by simp
  next
    case (Cons δ Δ)
    {
      fix Ψ
      have "map (uncurry (⊔)) (δ # Δ) ≼ map (uncurry (⊔)) (𝔍 Ψ (δ # Δ))"
      proof (cases "find (λ ψ. (uncurry (→)) ψ = snd δ) Ψ = None")
        case True
        hence "𝔍 Ψ (δ # Δ) = δ # 𝔍 Ψ Δ"
          by simp
        moreover have "⊢ (uncurry (⊔)) δ → (uncurry (⊔)) δ"
          by (metis axiom_k axiom_s modus_ponens)
        ultimately show ?thesis using Cons
          by (simp add: stronger_theory_left_right_cons)
      next
        case False
        from this obtain ψ where ψ:
          "find (λψ. uncurry (→) ψ = snd δ) Ψ = Some ψ"
          by fastforce
        let ?χ = "fst ψ"
        let ?γ = "snd ψ"
        let ?μ = "fst δ"
        have "uncurry (→) = (λ ψ. fst ψ → snd ψ)"
             "uncurry