Theory MiniSC_Craig

subsubsection‹Craig Interpolation›
theory MiniSC_Craig
imports MiniSC Formulas
begin

abbreviation atoms_mset where "atoms_mset Θ ≡ ⋃F ∈ set_mset Θ. atoms F"
  
(* which version of craig interpolation we show doesn't matter: *)
lemma interpolation_equal_styles: "
(∀Γ Δ Γ' Δ'. Γ + Γ' ⇒ Δ + Δ' ⟶ (∃F :: 'a formula. Γ ⇒ F,Δ ∧ F,Γ' ⇒ Δ' ∧ atoms F ⊆ atoms_mset (Γ + Δ) ∧ atoms F ⊆ atoms_mset (Γ' + Δ')))
  ⟷
(∀Γ Δ. Γ ⇒ Δ ⟶ (∃F :: 'a formula. Γ ⇒ {#F#} ∧ {#F#} ⇒ Δ ∧ atoms F ⊆ atoms_mset Γ ∧ atoms F ⊆ atoms_mset Δ))"
proof(intro iffI allI impI, goal_cases)
  case (1 Γ Δ)
  hence "Γ + {#} ⇒ {#} + Δ ⟶ (∃F. Γ ⇒ F, {#} ∧ F, {#} ⇒ Δ ∧ atoms F ⊆ atoms_mset (Γ + {#}) ∧ atoms F ⊆ atoms_mset ({#} + Δ))"  by presburger
  with 1 show ?case by auto
next
  case (2 Γ Δ Γ' Δ')
  from 2(2) have "Γ ⇒ Δ + image_mset Not Γ' + Δ'" by(induction Γ' arbitrary: Γ; simp add: SCp.NotR)
  hence "Γ + image_mset Not Δ ⇒ image_mset Not Γ' + Δ'" by(induction Δ arbitrary: Δ'; simp add: SCp.NotL) (metis SCp.NotL union_mset_add_mset_right)
  from 2(1)[THEN spec, THEN spec, THEN mp, OF this]
  have "∃F. Γ + image_mset ❙¬ Δ ⇒ {#F#} ∧ {#F#} ⇒ image_mset ❙¬ Γ' + Δ' ∧ atoms F ⊆ atoms_mset (Γ + image_mset ❙¬ Δ) ∧ atoms F ⊆ atoms_mset (image_mset ❙¬ Γ' + Δ')" .
  then obtain F where n: "Γ + image_mset ❙¬ Δ ⇒ {#F#}" and p: "{#F#} ⇒ image_mset ❙¬ Γ' + Δ'" and at: "atoms F ⊆ atoms_mset (Γ + Δ)" "atoms F ⊆ atoms_mset (Γ' + Δ')" by auto
  from n have n: "Γ ⇒ F, Δ" by(induction Δ arbitrary: Γ; simp add: NotL_inv inR1)
  from p have p: "F,Γ' ⇒ Δ'" by(induction Γ' arbitrary: Δ'; simp add: NotR_inv inL1)
  show ?case using p at n by blast
qed
    

text‹The original version of the interpolation theorem is due to Craig~\<^cite>‹"craig1957linear"›.
Our proof partly follows the approach of Troelstra and Schwichtenberg~\<^cite>‹"troelstra2000basic"› but,
especially with the mini formulas, adds its own spin.›

theorem SC_Craig_interpolation:
  assumes "Γ + Γ' ⇒ Δ + Δ'"
  obtains F where 
    "Γ ⇒ F,Δ"
    "F,Γ' ⇒ Δ'"
    "atoms F ⊆ atoms_mset (Γ + Δ)"
    "atoms F ⊆ atoms_mset (Γ' + Δ')"
proof -
  have split_seq: "(∃H'. H = f F J,H') ∨ (∃I'. I = f F J,I')" if "f F J, G = H + I" for f F G H I J
  proof -
    from that have "f F J ∈# H + I" by(metis (mono_tags) add_ac(2) union_single_eq_member)
    thus ?thesis by (meson multi_member_split union_iff)
  qed
  have mini: "∃ F. Γ ⇒ F, Δ ∧ F, Γ' ⇒ Δ' ∧ 
    atoms F ⊆ atoms_mset (Γ + Δ) ∧ atoms F ⊆ atoms_mset (Γ' + Δ') ∧ is_mini_formula F"
    if "Γ + Γ' ⇒ Δ + Δ'" "is_mini_mset (Γ+Γ'+Δ+Δ')" for Γ Γ' Δ Δ'
  using that proof(induction "Γ + Γ'" "Δ + Δ'" arbitrary: Γ Γ' Δ Δ' rule: SCp.induct)
    case BotL thus ?case proof(cases; intro exI)
      assume "⊥ ∈# Γ" with BotL 
      show "Γ ⇒ ⊥, Δ ∧ ⊥, Γ' ⇒ Δ' ∧ atoms ⊥ ⊆ atoms_mset (Γ + Δ) ∧ atoms ⊥ ⊆ atoms_mset (Γ' + Δ') ∧ is_mini_formula ⊥" 
        by(simp add: SCp.BotL)
    next
      assume "¬(⊥ ∈# Γ)" with BotL 
      show "Γ ⇒ ⊤, Δ ∧ ⊤, Γ' ⇒ Δ' ∧ atoms ⊤ ⊆ atoms_mset (Γ + Δ) ∧ atoms ⊤ ⊆ atoms_mset (Γ' + Δ') ∧ is_mini_formula ⊤"
        by(auto simp add: Top_def SCp.ImpR SCp.ImpL SCp.BotL intro!: SCp.intros(3-))
    qed
  next
    case (Ax k)
    let ?ss = "λF. (Γ ⇒ F, Δ ∧ F, Γ' ⇒ Δ' ∧ is_mini_formula F)" (* troelstra calls it a split sequent. *)
    have ff: "?ss ⊥" if "Atom k ∈# Γ" "Atom k ∈# Δ" (* troelstra uses ⊤ in this case. That can't be right. (p. 117, case Ax, right bottom split) *)
      using SCp.BotL SCp.Ax[of k] that by auto
    have fs: "?ss (Atom k)" if "Atom k ∈# Γ" "Atom k ∈# Δ'"
      using that by(auto intro!: SCp.Ax[where k=k])
    have sf: "?ss ((Atom k) ❙→ ⊥)" if "Atom k ∈# Γ'" "Atom k ∈# Δ"
      using that by(auto intro!: SCp.ImpR SCp.ImpL intro: SCp.Ax[where k=k] SCp.BotL)
    have ss: "?ss ⊤" if "Atom k ∈# Γ'" "Atom k ∈# Δ'"
      unfolding Top_def using that SCp.ImpR SCp.Ax BotL_canonical by fastforce
    have in_sumE: "⟦A ∈# (F + G); A ∈# F ⟹ P; A ∈# G ⟹ P⟧ ⟹ P" for A F G P by fastforce
    have trust_firstE: "P F ⟹ Q F ⟹ ∃F. P F ∧ Q F" for P Q F by blast
    from Ax show ?case by(elim in_sumE) (frule (1) ff fs sf ss; elim conjE trust_firstE; force)+
  next
    case (ImpR F G Δ'')
    note split_seq[of Imp, OF ImpR(3)]
    thus ?case proof(elim disjE exE)
      fix H' assume Δ: "Δ = F ❙→ G, H'"
      have "F, Γ + Γ' = (F, Γ) + Γ'" "G, Δ'' = (G, Δ - {#F ❙→ G#}) + Δ'" "is_mini_mset ((F, Γ) + Γ' + (G, Δ - {#F ❙→ G#}) + Δ')"
        using that ImpR(3-) by (simp_all add: union_assoc Δ)
      from  ImpR(2)[OF this] obtain Fa where Fam:
        "F, Γ ⇒ Fa, G, H'" "Fa, Γ' ⇒ Δ'" "is_mini_formula Fa"
        "atoms Fa ⊆ atoms_mset ((F, Γ) + (G, H'))" "atoms Fa ⊆ atoms_mset (Γ' + Δ')" unfolding Δ by auto
      thus ?thesis unfolding Δ proof(intro exI[where x=Fa] conjI ‹is_mini_formula Fa›)
        show "Γ ⇒ Fa, F ❙→ G, H'" using Fam by(intro SCp.ImpR[THEN inR1]; fast)
        show "Fa, Γ' ⇒ Δ'" using Fam by blast
        show "atoms Fa ⊆ atoms_mset (Γ + (F ❙→ G, H'))" "atoms Fa ⊆ atoms_mset (Γ' + Δ')" using Fam by auto
      qed
    next
      fix I' assume Δ': "Δ' = F ❙→ G, I'"
      have "F, Γ + Γ' = Γ + (F,Γ')" "G, Δ'' = Δ + (G, I')" "is_mini_mset (Γ + (F, Γ') + Δ + (G, I'))"
        using ImpR(3-) by (simp_all add: add.left_commute Δ')
      from ImpR(2)[OF this] obtain Fa m where Fam:
        "Γ ⇒ Fa, Δ" "Fa, F, Γ' ⇒ G, I'" "is_mini_formula Fa"
        "atoms Fa ⊆ atoms_mset (Γ + Δ)" "atoms Fa ⊆ atoms_mset ((F, Γ') + (G, I'))" unfolding Δ' by auto
      show ?thesis unfolding Δ' proof(intro exI[where x=Fa] conjI ‹is_mini_formula Fa›)
         show "Γ ⇒ Fa, Δ" using Fam by fast
         show "Fa, Γ' ⇒ F ❙→ G, I'" using Fam by (simp add: SCp.ImpR inL1)
         show "atoms Fa ⊆ atoms_mset (Γ + Δ)" "atoms Fa ⊆ atoms_mset (Γ' + (F ❙→ G, I'))" using Fam by auto
      qed
    qed
  next
    case (ImpL Γ'' F G)
    note split_seq[of Imp, OF ImpL(5)]
    thus ?case proof(elim disjE exE)
      fix H' assume Γ: "Γ = F ❙→ G, H'"
      from Γ have *: "Γ'' = Γ' + H'" "F, Δ + Δ' = Δ' + (F,Δ)"
        using ImpL(5-) by (simp_all add: union_assoc Γ)
      hence  "is_mini_mset (Γ' + H' + Δ' + (F, Δ))" using ImpL(6) by(auto simp add: Γ)
      from ImpL(2)[OF * this] obtain Fa where IH1: "Γ' ⇒ Fa, Δ'" "Fa, H' ⇒ F, Δ" 
        "atoms Fa ⊆ atoms_mset (H' + (F,Δ))" "atoms Fa ⊆ atoms_mset (Γ' + Δ')" "is_mini_formula Fa"  by blast
      from Γ have *: "G, Γ'' = (G, H') + Γ'" "Δ + Δ' = Δ + Δ'"
        using ImpL(5-) by (simp_all add: union_assoc)
      hence "is_mini_mset ((G, H') + Γ' + Δ + Δ')" using ImpL(6) by(simp add: Γ)
      from ImpL(4)[OF * this] obtain Ga where IH2: "G, H' ⇒ Ga, Δ" "Ga, Γ' ⇒ Δ'" 
        "atoms Ga ⊆ atoms_mset ((G, H') + Δ)" "atoms Ga ⊆ atoms_mset (Γ' + Δ')" "is_mini_formula Ga" by blast
      text‹A big part of the difficulty of this proof is finding a way to instantiate the IHs.
        Interestingly, this is not the only way that works. 
        Originally, we used @{term "Γ'' = H' + Γ'"} and @{term "F, Δ + Δ' = (F,Δ) + Δ'"}
        to instantiate the IH (which is in some sense more natural, less use of commutativity).
        This gave us a @{term Fa} that verifies @{term "H' ⇒ Fa, F, Δ"} and @{term "Fa, Γ' ⇒ Δ'"}
         and resulted in the interpolant @{term "to_mini_formula (Fa ❙∨ Ga)"}.›
      let ?w = "Fa ❙→ Ga"
      show ?thesis proof(intro exI[where x="?w"] conjI)  
        from IH1(1) IH2(2) show "?w, Γ' ⇒ Δ'"
          by (simp add: SCp.ImpL)
        from IH1(2) IH2(1) show "Γ ⇒ ?w, Δ" unfolding Γ
          by(intro SCp.ImpL inR1[OF SCp.ImpR] SCp.ImpR) (simp_all add: weakenR weakenL)
        show "atoms ?w ⊆ atoms_mset (Γ + Δ)" "atoms ?w ⊆ atoms_mset (Γ' + Δ')"
          using IH1(3-) IH2(3-) unfolding Γ by auto
        show "is_mini_formula ?w" using ‹is_mini_formula Fa› ‹is_mini_formula Ga› by simp
      qed
    next
      fix I' assume Γ': "Γ' = F ❙→ G, I'" note ImpL(5)[unfolded Γ']
      from Γ' have *: "Γ'' = Γ + I'" "F, Δ + Δ' = Δ + (F,Δ')"
        using ImpL(5-) by(simp_all add: union_assoc add_ac(2,3))
      hence "is_mini_mset (Γ + I' + Δ + (F, Δ'))" using ImpL(6) by(auto simp add: Γ')
      from ImpL(2)[OF * this] obtain Fa
        where IH1: "Γ ⇒ Fa, Δ" "Fa, I' ⇒ F, Δ'" "is_mini_formula Fa"
        "atoms Fa ⊆ atoms_mset (I' + (F,Δ'))" "atoms Fa ⊆ atoms_mset (Γ + Δ)" by blast
      from Γ' have *: "G, Γ'' = Γ + (G, I')" "Δ + Δ' = Δ + Δ'"
        using ImpL(5) by (simp_all add: add_ac ‹Γ'' = Γ + I'›)
      have "is_mini_mset (Γ + (G, I') + Δ + Δ')"  using ImpL(6) by(auto simp add: Γ')
      from ImpL(4)[OF * this] obtain Ga l
        where IH2: "Γ ⇒ Ga, Δ" "Ga, G, I' ⇒ Δ'" "is_mini_formula Ga"
        "atoms Ga ⊆ atoms_mset ((G, I') + Δ')" "atoms Ga ⊆ atoms_mset (Γ + Δ)" by blast
      text‹Same thing as in the other case, just with 
        @{term "G, Γ'' = (G, I') + Γ"}, @{term "Δ + Δ' = Δ' + Δ"},
        @{term "Γ'' = I' + Γ"}, and @{term "F, Δ + Δ' = (F,Δ') + Δ"}
       resulting in @{term "to_mini_formula (❙¬(Fa ❙∨ Ga))"}›
      let ?w = "(Ga ❙→ (Fa ❙→ ⊥)) ❙→ ⊥"
      have "?w = to_mini_formula (Ga ❙∧ Fa)" by (simp add: IH1(3) IH2(3) mini_to_mini)
      show ?thesis proof(intro exI[of _ ?w] conjI)
        from IH1(1) IH2(1) show "Γ ⇒ ?w, Δ"
          by(intro SCp.ImpR SCp.ImpL) (simp_all add: inR1 weakenR BotL_canonical)
        from IH1(2) IH2(2) show "?w, Γ' ⇒ Δ'" unfolding Γ'
          by(blast intro!: SCp.ImpL SCp.ImpR dest: weakenL weakenR)+
        show "atoms ?w ⊆ atoms_mset (Γ + Δ)"
             "atoms ?w ⊆ atoms_mset (Γ' + Δ')" using IH1(3-) IH2(3-) unfolding Γ' by auto
        show "is_mini_formula ?w" using ‹is_mini_formula Fa› ‹is_mini_formula Ga› by simp
      qed
    qed
  next
    text‹The rest is just those cases that can't happen because of the mini formula property.›
  qed (metis add.commute is_mini_formula.simps union_iff union_single_eq_member)+
  define tms :: "'a formula multiset ⇒ 'a formula multiset"
    where "tms = image_mset to_mini_formula"
  have [simp]: "tms (A + B) = tms A + tms B" "tms {#F#} = {#to_mini_formula F#}" for A B F unfolding tms_def by simp_all
  have [simp]: "atoms_mset (tms Γ) = atoms_mset Γ" for Γ unfolding tms_def using mini_formula_atoms by fastforce
  have imm: "is_mini_mset (tms Γ + tms Γ' + tms Δ + tms Δ')" unfolding tms_def by auto
  from assms have "tms Γ + tms Γ' ⇒ tms Δ + tms Δ'" unfolding tms_def using SC_full_to_mini by force
  from mini[OF this imm] obtain F where hp(*habemus papam*):
    "tms Γ ⇒ F, tms Δ" "F, tms Γ' ⇒ tms Δ'"
    and su: "atoms F ⊆ atoms_mset (tms Γ + tms Δ)" "atoms F ⊆ atoms_mset (tms Γ' + tms Δ')"
    and mf: "is_mini_formula F" by blast
  from hp mf have "tms Γ ⇒ tms (F, Δ)" "tms (F, Γ') ⇒ tms Δ'" using mini_to_mini[where 'a='a] unfolding tms_def by simp_all
  hence "Γ ⇒ F, Δ" "F, Γ' ⇒ Δ'" using SC_mini_to_full unfolding tms_def by blast+
  with su show ?thesis using ‹⋀Γ. atoms_mset (tms Γ) = atoms_mset Γ› image_mset_union that by auto
qed
(*
  Gallier:
   - wouldn't hold without bottom. Try interpolating A → A and B → B 
   - is an application of cut elimination? oh well, if you'd have a cut rule in the ⇒ predicate,
      you'd be in trouble, ok.
*)

text‹Note that there is an extension to Craig interpolation:
One can show that atoms that only appear positively/negatively in the original formulas will only appear
positively/negatively in the interpolant. ›

abbreviation "patoms_mset S ≡ ⋃F∈set_mset S. fst (pn_atoms F)"
abbreviation "natoms_mset S ≡ ⋃F∈set_mset S. snd (pn_atoms F)"

theorem SC_Craig_interpolation_pn:
  assumes "Γ + Γ' ⇒ Δ + Δ'"
  obtains F where 
    "Γ ⇒ F,Δ"
    "F,Γ' ⇒ Δ'"
    "fst (pn_atoms F) ⊆ (patoms_mset Γ ∪ natoms_mset Δ) ∩ (natoms_mset Γ' ∪ patoms_mset Δ')"
    "snd (pn_atoms F) ⊆ (natoms_mset Γ ∪ patoms_mset Δ) ∩ (patoms_mset Γ' ∪ natoms_mset Δ')"
proof -
  have split_seq: "(∃H'. H = f F J,H') ∨ (∃I'. I = f F J,I')" if "f F J, G = H + I" for f F G H I J
  proof -
    from that have "f F J ∈# H + I" by(metis (mono_tags) add_ac(2) union_single_eq_member)
    thus ?thesis by (meson multi_member_split union_iff)
  qed
  have mini: "∃ F :: 'a formula. Γ ⇒ F, Δ ∧ F, Γ' ⇒ Δ' ∧ 
    fst (pn_atoms F) ⊆ (patoms_mset Γ ∪ natoms_mset Δ) ∩ (natoms_mset Γ' ∪ patoms_mset Δ') ∧ 
    snd (pn_atoms F) ⊆ (natoms_mset Γ ∪ patoms_mset Δ) ∩ (patoms_mset Γ' ∪ natoms_mset Δ') ∧ is_mini_formula F"
    if "Γ + Γ' ⇒ Δ + Δ'" "is_mini_mset (Γ+Γ'+Δ+Δ')" for Γ Γ' Δ Δ'
  using that proof(induction "Γ + Γ'" "Δ + Δ'" arbitrary: Γ Γ' Δ Δ' rule: SCp.induct)
    case BotL 
    let ?om = "λF. fst (pn_atoms F) ⊆ (patoms_mset Γ ∪ natoms_mset Δ) ∩ (natoms_mset Γ' ∪ patoms_mset Δ') ∧
        snd (pn_atoms F) ⊆ (natoms_mset Γ ∪ patoms_mset Δ) ∩ (patoms_mset Γ' ∪ natoms_mset Δ') ∧ is_mini_formula (F :: 'a formula)"
    show ?case proof(cases; intro exI)
      assume "⊥ ∈# Γ" with BotL 
      show "Γ ⇒ ⊥, Δ ∧ ⊥, Γ' ⇒ Δ' ∧ ?om ⊥" by(simp add: SCp.BotL)
    next
      assume "¬(⊥ ∈# Γ)" with BotL 
      show "Γ ⇒ ⊤, Δ ∧ ⊤, Γ' ⇒ Δ' ∧ ?om ⊤" 
        by(auto simp add: Top_def SCp.ImpR SCp.ImpL SCp.BotL prod_unions_def intro!: SCp.intros(3-))
    qed
  next
    case (Ax k)
    let ?ss = "λF. (Γ ⇒ F, Δ ∧ F, Γ' ⇒ Δ' ∧ fst (pn_atoms F) ⊆ (patoms_mset Γ ∪ natoms_mset Δ) ∩ (natoms_mset Γ' ∪ patoms_mset Δ') ∧
        snd (pn_atoms F) ⊆ (natoms_mset Γ ∪ patoms_mset Δ) ∩ (patoms_mset Γ' ∪ natoms_mset Δ') ∧ is_mini_formula F)" (* troelstra calls it a split sequent. *)
    have ff: "?ss ⊥" if "Atom k ∈# Γ" "Atom k ∈# Δ"
      using SCp.BotL SCp.Ax[of k] that by auto
    have fs: "?ss (Atom k)" if "Atom k ∈# Γ" "Atom k ∈# Δ'"
      using that by(force intro!: SCp.Ax[where k=k])
    have sf: "?ss ((Atom k) ❙→ ⊥)" if "Atom k ∈# Γ'" "Atom k ∈# Δ"
      using that by(auto intro!: SCp.ImpR SCp.ImpL intro: SCp.Ax[where k=k] SCp.BotL exI[where x="Atom k"] simp add: prod_unions_def; force)
    have ss: "?ss ⊤" if "Atom k ∈# Γ'" "Atom k ∈# Δ'"
      unfolding Top_def using that SCp.ImpR by (auto simp add: prod_unions_def SCp.Ax)
    have in_sumE: "⟦A ∈# (F + G); A ∈# F ⟹ P; A ∈# G ⟹ P⟧ ⟹ P" for A F G P by fastforce
    have trust_firstE: "P F ⟹ Q F ⟹ ∃F. P F ∧ Q F" for P Q F by blast
    from Ax show ?case by(elim in_sumE) (frule (1) ff fs sf ss; elim conjE trust_firstE; force)+
  next
  next
    case (ImpR F G Δ'')
    note split_seq[of Imp, OF ImpR(3)]
    thus ?case proof(elim disjE exE)
      fix H' assume Δ: "Δ = F ❙→ G, H'"
      have "F, Γ + Γ' = (F, Γ) + Γ'" "G, Δ'' = (G, Δ - {#F ❙→ G#}) + Δ'" "is_mini_mset ((F, Γ) + Γ' + (G, Δ - {#F ❙→ G#}) + Δ')"
        using that ImpR(3-) by (simp_all add: union_assoc Δ)
      from  ImpR(2)[OF this] obtain Fa where Fam:
        "F, Γ ⇒ Fa, G, H'" "Fa, Γ' ⇒ Δ'" "is_mini_formula Fa"
        "fst (pn_atoms Fa) ⊆ (patoms_mset (F, Γ) ∪ natoms_mset (G, H')) ∩ (natoms_mset Γ' ∪ patoms_mset Δ')"
        "snd (pn_atoms Fa) ⊆ (natoms_mset (F, Γ) ∪ patoms_mset (G, H')) ∩ (patoms_mset Γ' ∪ natoms_mset Δ')" unfolding Δ by auto
      thus ?thesis unfolding Δ proof(intro exI[where x=Fa] conjI ‹is_mini_formula Fa›)
        show "Γ ⇒ Fa, F ❙→ G, H'" using Fam by(intro SCp.ImpR[THEN inR1]; fast)
        show "Fa, Γ' ⇒ Δ'" using Fam by blast
        show "fst (pn_atoms Fa) ⊆ (patoms_mset Γ ∪ natoms_mset (F ❙→ G, H')) ∩ (natoms_mset Γ' ∪ patoms_mset Δ')" 
             "snd (pn_atoms Fa) ⊆ (natoms_mset Γ ∪ patoms_mset (F ❙→ G, H')) ∩ (patoms_mset Γ' ∪ natoms_mset Δ')" 
          using Fam(4-) by (auto simp: prod_unions_def split: prod.splits)
      qed
    next
      fix I' assume Δ': "Δ' = F ❙→ G, I'"
      have "F, Γ + Γ' = Γ + (F,Γ')" "G, Δ'' = Δ + (G, I')" "is_mini_mset (Γ + (F, Γ') + Δ + (G, I'))"
        using ImpR(3-) by (simp_all add: add.left_commute Δ')
      from ImpR(2)[OF this] obtain Fa m where Fam:
        "Γ ⇒ Fa, Δ" "Fa, F, Γ' ⇒ G, I'" "is_mini_formula Fa"
        "fst (pn_atoms Fa) ⊆ (patoms_mset Γ ∪ natoms_mset Δ) ∩ (natoms_mset (F, Γ') ∪ patoms_mset (G, I'))"
        "snd (pn_atoms Fa) ⊆ (natoms_mset Γ ∪ patoms_mset Δ) ∩ (patoms_mset (F, Γ') ∪ natoms_mset (G, I'))" unfolding Δ' by auto
      show ?thesis unfolding Δ' proof(intro exI[where x=Fa] conjI ‹is_mini_formula Fa›)
         show "Γ ⇒ Fa, Δ" using Fam by fast
         show "Fa, Γ' ⇒ F ❙→ G, I'" using Fam by (simp add: SCp.ImpR inL1)
         show "fst (pn_atoms Fa) ⊆ (patoms_mset Γ ∪ natoms_mset Δ) ∩ (natoms_mset Γ' ∪ patoms_mset (F ❙→ G, I'))"
              "snd (pn_atoms Fa) ⊆ (natoms_mset Γ ∪ patoms_mset Δ) ∩ (patoms_mset Γ' ∪ natoms_mset (F ❙→ G, I'))" 
              using Fam by (auto simp: prod_unions_def split: prod.splits)
      qed
    qed
  next
  next
    case (ImpL Γ'' F G)
    note split_seq[of Imp, OF ImpL(5)]
    thus ?case proof(elim disjE exE)
      fix H' assume Γ: "Γ = F ❙→ G, H'"
      from Γ have *: "Γ'' = Γ' + H'" "F, Δ + Δ' = Δ' + (F,Δ)"
        using ImpL(5-) by (simp_all add: union_assoc Γ)
      hence  "is_mini_mset (Γ' + H' + Δ' + (F, Δ))" using ImpL(6) by(auto simp add: Γ)
      from ImpL(2)[OF * this] obtain Fa where IH1: "Γ' ⇒ Fa, Δ'" "Fa, H' ⇒ F, Δ" 
        "fst (pn_atoms Fa) ⊆ (patoms_mset Γ' ∪ natoms_mset Δ') ∩ (natoms_mset H' ∪ patoms_mset (F, Δ))"
        "snd (pn_atoms Fa) ⊆ (natoms_mset Γ' ∪ patoms_mset Δ') ∩ (patoms_mset H' ∪ natoms_mset (F, Δ))" "is_mini_formula Fa"  by blast
      from Γ have *: "G, Γ'' = (G, H') + Γ'" "Δ + Δ' = Δ + Δ'"
        using ImpL(5-) by (simp_all add: union_assoc)
      hence "is_mini_mset ((G, H') + Γ' + Δ + Δ')" using ImpL(6) by(simp add: Γ)
      from ImpL(4)[OF * this] obtain Ga where IH2: "G, H' ⇒ Ga, Δ" "Ga, Γ' ⇒ Δ'" 
        "fst (pn_atoms Ga) ⊆ (patoms_mset (G, H') ∪ natoms_mset Δ) ∩ (natoms_mset Γ' ∪ patoms_mset Δ')"
        "snd (pn_atoms Ga) ⊆ (natoms_mset (G, H') ∪ patoms_mset Δ) ∩ (patoms_mset Γ' ∪ natoms_mset Δ')" "is_mini_formula Ga" by blast
      let ?w = "Fa ❙→ Ga"
      show ?thesis proof(intro exI[where x="?w"] conjI)
        from IH1(1) IH2(2) show "?w, Γ' ⇒ Δ'"
          by (simp add: SCp.ImpL)
        from IH1(2) IH2(1) show "Γ ⇒ ?w, Δ" unfolding Γ
          by(intro SCp.ImpL inR1[OF SCp.ImpR] SCp.ImpR) (simp_all add: weakenR weakenL)
        show "fst (pn_atoms ?w) ⊆ (patoms_mset Γ ∪ natoms_mset Δ) ∩ (natoms_mset Γ' ∪ patoms_mset Δ')" 
             "snd (pn_atoms ?w) ⊆ (natoms_mset Γ ∪ patoms_mset Δ) ∩ (patoms_mset Γ' ∪ natoms_mset Δ')"
          using IH1(3-) IH2(3-) unfolding Γ by (auto simp: prod_unions_def split: prod.splits)
        show "is_mini_formula ?w" using ‹is_mini_formula Fa› ‹is_mini_formula Ga› by simp
      qed
    next
      fix I' assume Γ': "Γ' = F ❙→ G, I'" note ImpL(5)[unfolded Γ']
      from Γ' have *: "Γ'' = Γ + I'" "F, Δ + Δ' = Δ + (F,Δ')"
        using ImpL(5-) by(simp_all add: union_assoc add_ac(2,3))
      hence "is_mini_mset (Γ + I' + Δ + (F, Δ'))" using ImpL(6) by(auto simp add: Γ')
      from ImpL(2)[OF * this] obtain Fa
        where IH1: "Γ ⇒ Fa, Δ" "Fa, I' ⇒ F, Δ'" "is_mini_formula Fa"
        "fst (pn_atoms Fa) ⊆ (patoms_mset Γ ∪ natoms_mset Δ) ∩ (natoms_mset I' ∪ patoms_mset (F, Δ'))"
        " snd (pn_atoms Fa) ⊆ (natoms_mset Γ ∪ patoms_mset Δ) ∩ (patoms_mset I' ∪ natoms_mset (F, Δ'))" by blast
      from Γ' have *: "G, Γ'' = (G, I') + Γ" "Δ + Δ' = Δ' + Δ"
        using ImpL(5) by (simp_all add: add_ac ‹Γ'' = Γ + I'›)
      have "is_mini_mset ((G, I') + Γ + Δ' + Δ)"  using ImpL(6) by(auto simp add: Γ')
      from ImpL(4)[OF * this] obtain Ga
        where IH2: "G, I' ⇒ Ga, Δ'" "Ga, Γ ⇒ Δ" "is_mini_formula Ga"
        "fst (pn_atoms Ga) ⊆ (patoms_mset (G, I') ∪ natoms_mset Δ') ∩ (natoms_mset Γ ∪ patoms_mset Δ)"
        "snd (pn_atoms Ga) ⊆ (natoms_mset (G, I') ∪ patoms_mset Δ') ∩ (patoms_mset Γ ∪ natoms_mset Δ)" by blast
      let ?w = "(Fa ❙→ Ga) ❙→ ⊥"
      have "?w = to_mini_formula (❙¬(Fa ❙→ Ga))" unfolding to_mini_formula.simps mini_to_mini[OF IH1(3)] mini_to_mini[OF IH2(3)] by (simp add: IH1(3) IH2(3) )
      show ?thesis proof(intro exI[of _ ?w] conjI)
        from IH1(1) IH2(2) show "Γ ⇒ ?w, Δ"
          by(intro SCp.ImpR SCp.ImpL) (simp_all add: inR1 weakenR BotL_canonical)
        from IH1(2) IH2(1) show "?w, Γ' ⇒ Δ'" unfolding Γ'
          by(blast intro!: SCp.ImpL SCp.ImpR dest: weakenL weakenR)+
        show "fst (pn_atoms ?w) ⊆ (patoms_mset Γ ∪ natoms_mset Δ) ∩ (natoms_mset Γ' ∪ patoms_mset Δ')"
             "snd (pn_atoms ?w) ⊆ (natoms_mset Γ ∪ patoms_mset Δ) ∩ (patoms_mset Γ' ∪ natoms_mset Δ')"
          using IH1(4-) IH2(4-) unfolding Γ' by (auto simp: prod_unions_def split: prod.splits)
        show "is_mini_formula ?w" using ‹is_mini_formula Fa› ‹is_mini_formula Ga› by simp
      qed
    qed
  next
  qed (metis add.commute is_mini_formula.simps union_iff union_single_eq_member)+
  define tms :: "'a formula multiset ⇒ 'a formula multiset"
    where "tms = image_mset to_mini_formula"
  have [simp]: "tms (A + B) = tms A + tms B" "tms {#F#} = {#to_mini_formula F#}" for A B F unfolding tms_def by simp_all
  have imm: "is_mini_mset (tms Γ + tms Γ' + tms Δ + tms Δ')" unfolding tms_def by auto
  from assms have "tms Γ + tms Γ' ⇒ tms Δ + tms Δ'" unfolding tms_def using SC_full_to_mini by force
  from mini[OF this imm] obtain F where hp:
    "tms Γ ⇒ F, tms Δ" "F, tms Γ' ⇒ tms Δ'"
    and su: " fst (pn_atoms F) ⊆ (patoms_mset (tms Γ) ∪ natoms_mset (tms Δ)) ∩ (natoms_mset (tms Γ') ∪ patoms_mset (tms Δ'))"
      "snd (pn_atoms F) ⊆ (natoms_mset (tms Γ) ∪ patoms_mset (tms Δ)) ∩ (patoms_mset (tms Γ') ∪ natoms_mset (tms Δ'))"
    and mf: "is_mini_formula F" by blast
  from hp mf have "tms Γ ⇒ tms (F, Δ)" "tms (F, Γ') ⇒ tms Δ'" using mini_to_mini[where 'a='a] unfolding tms_def by simp_all
  hence *: "Γ ⇒ F, Δ" "F, Γ' ⇒ Δ'" using SC_mini_to_full unfolding tms_def by blast+
  have "pn_atoms (to_mini_formula F) = pn_atoms F" for F :: "'a formula" by(induction F; simp add: prod_unions_def split: prod.splits)
  hence pn_tms: "patoms_mset (tms Γ) = patoms_mset Γ" "natoms_mset (tms Γ) = natoms_mset Γ" for Γ unfolding tms_def by simp_all
  from su[unfolded pn_tms] show ?thesis using that[of F, OF * _ _] by auto
qed
(* why this proof, again? Troelstra, somewhat unintuitively uses Fa ❙→ Ga and Fa ❙∧ Ga as interpolants in the
   ImpL cases. The asymmetry seems weird, at least. This shows: at least, they are correct. *)

end