Session Propositional_Proof_Systems

Theory Formulas

section ‹Formulas›

theory Formulas
imports Main "HOL-Library.Countable"
begin

(* unrelated, but I need this in too many places. *)
notation insert ("_  _" [56,55] 55)

datatype (atoms: 'a) formula = 
    Atom 'a
  | Bot                              ("")  
  | Not "'a formula"                 ("¬")
  | And "'a formula" "'a formula"    (infix "" 68)
  | Or "'a formula" "'a formula"     (infix "" 68)
  | Imp "'a formula" "'a formula"    (infixr "" 68)
(* In a standard Isabelle/jEdit config, bold can be done with C-e rightarrow.
   I learned that way too late. *)
(* I'm not sure I'm happy about the definition of what is an atom.
   I'm inclined to treat 'a as our atom type and call an Atom k an "atom formula",
   but this goes against anything the literature does. So, Atom k will be an atom,
   k its index, but there are probably a few cases where I call 'a an atom… *)
(* like here: *)
lemma atoms_finite[simp,intro!]: "finite (atoms F)" by(induction F; simp)

primrec subformulae where
"subformulae  = []" |
"subformulae (Atom k) = [Atom k]" |
"subformulae (Not F) = Not F # subformulae F" |
"subformulae (And F G) = And F G # subformulae F @ subformulae G" |
"subformulae (Imp F G) = Imp F G # subformulae F @ subformulae G" |
"subformulae (Or F G) = Or F G # subformulae F @ subformulae G"

lemma atoms_are_subformulae: "Atom ` atoms F  set (subformulae F)"
  by (induction F) auto
    
lemma subsubformulae: "G  set (subformulae F)  H  set (subformulae G)  H  set (subformulae F)"
  by(induction F; force)
    
lemma subformula_atoms: "G  set (subformulae F)  atoms G  atoms F"
  by(induction F) auto
    
lemma subformulae_self[simp,intro]: "F  set (subformulae F)"
  by(induction F; simp)

lemma subformulas_in_subformulas:
  "G  H  set (subformulae F)  G  set (subformulae F)  H  set (subformulae F)"
  "G  H  set (subformulae F)  G  set (subformulae F)  H  set (subformulae F)"
  "G  H  set (subformulae F)  G  set (subformulae F)  H  set (subformulae F)"
  "¬ G  set (subformulae F)  G  set (subformulae F)"
  by(fastforce elim: subsubformulae)+

lemma length_subformulae: "length (subformulae F) = size F" by(induction F; simp)

subsection‹Derived Connectives›
    
definition Top ("") where
"    "
lemma top_atoms_simp[simp]: "atoms  = {}" unfolding Top_def by simp

primrec BigAnd :: "'a formula list  'a formula" ("_") where
"Nil = (¬)" ― ‹essentially, it doesn't matter what I use here. But since I want to use this in CNFs, implication is not a nice thing to have.› |
"(F#Fs) = F  Fs"

lemma atoms_BigAnd[simp]: "atoms (Fs) = (atoms ` set Fs)"
  by(induction Fs; simp)

primrec BigOr :: "'a formula list  'a formula" ("_") where
"Nil = " |
"(F#Fs) = F  Fs"

text‹Formulas are countable if their atoms are, and @{method countable_datatype} is really helpful with that.› 
instance formula :: (countable) countable by countable_datatype

definition "prod_unions A B  case A of (a,b)  case B of (c,d)  (a  c, b  d)"
primrec pn_atoms where
"pn_atoms (Atom A) = ({A},{})" |
"pn_atoms Bot = ({},{})" |
"pn_atoms (Not F) = prod.swap (pn_atoms F)" |
"pn_atoms (And F G) = prod_unions (pn_atoms F) (pn_atoms G)" |
"pn_atoms (Or F G) = prod_unions (pn_atoms F) (pn_atoms G)" |
"pn_atoms (Imp F G) = prod_unions (prod.swap (pn_atoms F)) (pn_atoms G)"
lemma pn_atoms_atoms: "atoms F = fst (pn_atoms F)  snd (pn_atoms F)"
  by(induction F) (auto simp add: prod_unions_def split: prod.splits)

text‹A very trivial simplifier.
Does wonders as a postprocessor for the Harrison-style Craig interpolations.›
context begin
definition "isstop F  F = ¬  F = "
fun simplify_consts where
"simplify_consts (Atom k) = Atom k" |
"simplify_consts  = " |
"simplify_consts (Not F) = (let S = simplify_consts F in case S of (Not G)  G | _ 
  if isstop S then  else ¬ S)" |
"simplify_consts (And F G) = (let S = simplify_consts F; T = simplify_consts G in (
  if S =  then  else
  if isstop S then T ― ‹not ⊤›, T› else
  if T =  then  else
  if isstop T then S else
  if S = T then S else
  S  T))" |
"simplify_consts (Or F G) = (let S = simplify_consts F; T = simplify_consts G in (
  if S =  then T else
  if isstop S then  else
  if T =  then S else
  if isstop T then  else
  if S = T then S else
  S  T))" |
"simplify_consts (Imp F G) = (let S = simplify_consts F; T = simplify_consts G in (
  if S =  then  else
  if isstop S then T else
  if isstop T then  else
  if T =  then ¬ S else
  if S = T then  else
  case S of Not H  (case T of Not I  
    I  H | _  
    H  T) | _ 
    S  T))"

lemma simplify_consts_size_le: "size (simplify_consts F)  size F"
proof -
  have [simp]: "Suc (Suc 0)  size F + size G" for F G :: "'a formula" by(cases F; cases G; simp)
  show ?thesis by(induction F; fastforce simp add: Let_def isstop_def Top_def split: formula.splits)
qed

lemma simplify_const: "atoms F = {}  isstop (simplify_consts F)  (simplify_consts F) = "
  by(induction F; fastforce simp add: Let_def isstop_def Top_def split: formula.splits)
value "(size , size (¬))" (* this is why I need isstop in this lemma and can't write simplify_consts
  in a way that this lemma can say ∈ {⊤, ⊥} *)

end
  
(*
Here's a useful little function for testing a conjecture on "a few" examples: 
*)
fun all_formulas_of_size where
"all_formulas_of_size K 0 = {}  Atom ` K" |
"all_formulas_of_size K (Suc n) = (
  let af = (set [all_formulas_of_size K m. m  [0..<Suc n]]) in
  (Faf.
    (Gaf. if size F + size G  Suc n then {And F G, Or F G, Imp F G} else {}) 
    (if size F  Suc n then {Not F} else {})) 
   af)"
(* this set obviously grows exponentially (with a base of 5 approximately).
   size 7 produces 26032 formulas, which is probably the last value
   where I can test anything meaningfully with this implementation. *)

lemma all_formulas_of_size: "F  all_formulas_of_size K n  (size F  Suc n  atoms F  K)" (is "?l  ?r")
proof -
  have rl: "?r  ?l"
  proof(induction F arbitrary: n)
    case (Atom x)
    have *: "Atom x  all_formulas_of_size K 0" using Atom by simp
    hence **: "Atom x   (all_formulas_of_size K ` set [0..<Suc m])" for m
      by (simp; metis atLeastLessThan_iff le_zero_eq not_le)
    thus ?case using Atom by(cases n; simp)
  next
    case Bot
    have *: "Bot  all_formulas_of_size K 0" by simp
    hence **: "Bot   (all_formulas_of_size K ` set [0..<Suc m])" for m
      by (simp; metis atLeastLessThan_iff le_zero_eq not_le)
    then show ?case using Bot by(cases n; simp)
  next
    case (Not F)
    have *: "size F  n" using Not by simp
    then obtain m where n[simp]: "n = Suc m" by (metis Suc_diff_1 formula.size_neq leD neq0_conv)
    with Not have IH: "F  all_formulas_of_size K m" by simp
    then show ?case using * by(simp add: bexI[where x=F])
  next
    case (And F G)
    with And have *: "size F + size G  n" by simp
    then obtain m where n[simp]: "n = Suc m"
      by (metis Suc_diff_1 add_is_0 formula.size_neq le_zero_eq neq0_conv)
    then obtain nF nG where nFG[simp]: "size F  nF" "size G  nG" "n = nF + nG"
      by (metis * add.assoc nat_le_iff_add order_refl)
    then obtain mF mG where mFG[simp]: "nF = Suc mF" "nG = Suc mG"
      by (metis Suc_diff_1 formula.size_neq leD neq0_conv)
    with And have IH: "F  all_formulas_of_size K mF" "G  all_formulas_of_size K mG" 
      using nFG by simp+
    let ?af = "(set [all_formulas_of_size K m. m  [0..<Suc m]])"
    have r: "F  all_formulas_of_size K mF  mF  n  F  (set (map (all_formulas_of_size K) [0..<Suc n]))"
      for F mF n by fastforce
    have af: "F  ?af" "G  ?af" using nFG(3) by(intro IH[THEN r]; simp)+
    have m: "F  G  (if size F + size G  Suc m then {F  G, F  G, F  G} else {})" using * by simp
    from IH * show ?case using af by(simp only: n all_formulas_of_size.simps Let_def, insert m) fast
  next
    case (Or F G) case (Imp F G) ― ‹analogous› (*<*)
  next
    case (Or F G)
    with Or have *: "size F + size G  n" by simp
    then obtain m where n[simp]: "n = Suc m"
      by (metis Suc_diff_1 add_is_0 formula.size_neq le_zero_eq neq0_conv)
    then obtain nF nG where nFG[simp]: "size F  nF" "size G  nG" "n = nF + nG"
      by (metis * add.assoc nat_le_iff_add order_refl)
    then obtain mF mG where mFG[simp]: "nF = Suc mF" "nG = Suc mG"
      by (metis Suc_diff_1 formula.size_neq leD neq0_conv)
    with Or have IH: "F  all_formulas_of_size K mF" "G  all_formulas_of_size K mG" 
      using nFG by simp+
    let ?af = "(set [all_formulas_of_size K m. m  [0..<Suc m]])"
    have r: "F  all_formulas_of_size K mF  mF  n  F  (set (map (all_formulas_of_size K) [0..<Suc n]))"
      for F mF n by fastforce
    have af: "F  ?af" "G  ?af" using nFG(3) by(intro IH[THEN r]; simp)+
    have m: "Or F G  (if size F + size G  Suc m then {F  G, F  G, F  G} else {})" using * by simp
    from IH * show ?case using af by(simp only: n all_formulas_of_size.simps Let_def, insert m) fast
  next
    case (Imp F G)
    with Imp have *: "size F + size G  n" by simp
    then obtain m where n[simp]: "n = Suc m"
      by (metis Suc_diff_1 add_is_0 formula.size_neq le_zero_eq neq0_conv)
    then obtain nF nG where nFG[simp]: "size F  nF" "size G  nG" "n = nF + nG"
      by (metis * add.assoc nat_le_iff_add order_refl)
    then obtain mF mG where mFG[simp]: "nF = Suc mF" "nG = Suc mG"
      by (metis Suc_diff_1 formula.size_neq leD neq0_conv)
    with Imp have IH: "F  all_formulas_of_size K mF" "G  all_formulas_of_size K mG" 
      using nFG by simp+
    let ?af = "(set [all_formulas_of_size K m. m  [0..<Suc m]])"
    have r: "F  all_formulas_of_size K mF  mF  n  F  (set (map (all_formulas_of_size K) [0..<Suc n]))"
      for F mF n by fastforce
    have af: "F  ?af" "G  ?af" using nFG(3) by(intro IH[THEN r]; simp)+
    have m: "Imp F G  (if size F + size G  Suc m then {F  G, F  G, F  G} else {})" using * by simp
    from IH * show ?case using af by(simp only: n all_formulas_of_size.simps Let_def, insert m) fast
  (*>*)
  qed
  have lr: ?r if l: ?l 
  proof
    have *: "F  all_formulas_of_size K x  F  all_formulas_of_size K (x + n)" for x n
      by(induction n; simp)
    show "size F  Suc n" using l
      by(induction n; auto split: if_splits) (metis "*" le_SucI le_eq_less_or_eq le_iff_add)
    show "atoms F  K" using l
      proof(induction n arbitrary: F rule: less_induct)
        case (less x)
        then show ?case proof(cases x)
          case 0 with less show ?thesis by force
        next
          case (Suc y) with less show ?thesis 
            by(simp only: all_formulas_of_size.simps Let_def) (fastforce simp add: less_Suc_eq split: if_splits)
        qed
      qed
  qed
  from lr rl show ?thesis proof qed
qed
(* At first I thought: why would I prove anything about all_formulas_of_size, I only want to test a conjecture with it.
   Guess why: it was broken.
   Granted, I spent too much time on this. *)

end

Theory Sema

subsection‹Semantics›
theory Sema
imports Formulas
begin

type_synonym 'a valuation = "'a  bool"
text‹The implicit statement here is that an assignment or valuation is always defined on all atoms (because HOL is a total logic).
Thus, there are no unsuitable assignments.›

primrec formula_semantics :: "'a valuation  'a formula  bool" (infix "" 51) where
"𝒜  Atom k = 𝒜 k" |
"_   = False" |
"𝒜  Not F = (¬ 𝒜  F)" |
"𝒜  And F G = (𝒜  F  𝒜  G)" |
"𝒜  Or F G = (𝒜  F  𝒜  G)" |
"𝒜  Imp F G = (𝒜  F  𝒜  G)"

abbreviation valid (" _" 51) where
" F  A. A  F"

lemma irrelevant_atom[simp]: "A  atoms F  (𝒜(A := V))  F  𝒜  F"
  by (induction F; simp)
lemma relevant_atoms_same_semantics: "k  atoms F. 𝒜1 k = 𝒜2 k  𝒜1  F  𝒜2  F"
  by(induction F; simp)

context begin
text‹Just a definition more similar to~\cite[p. 5]{schoening1987logik}.
Unfortunately, using this as the main definition would get in the way of automated reasoning all the time.›
private primrec formula_semantics_alt where
"formula_semantics_alt 𝒜 (Atom k) = 𝒜 k" |
"formula_semantics_alt 𝒜 (Bot) = False" |
"formula_semantics_alt 𝒜 (Not a) = (if formula_semantics_alt 𝒜 a then False else True)" |
"formula_semantics_alt 𝒜 (And a b) = (if formula_semantics_alt 𝒜 a then formula_semantics_alt 𝒜 b else False)" |
"formula_semantics_alt 𝒜 (Or a b) = (if formula_semantics_alt 𝒜 a then True else formula_semantics_alt 𝒜 b)" |
"formula_semantics_alt 𝒜 (Imp a b) = (if formula_semantics_alt 𝒜 a then formula_semantics_alt 𝒜 b else True)"
private lemma "formula_semantics_alt 𝒜 F  𝒜  F"
  by(induction F; simp)

text‹If you fancy a definition more similar to~\cite[p. 39]{gallier2015logic},
this is probably the closest you can go without going incredibly ugly.›
private primrec formula_semantics_tt where
"formula_semantics_tt 𝒜 (Atom k) = 𝒜 k" |
"formula_semantics_tt 𝒜 (Bot) = False" |
"formula_semantics_tt 𝒜 (Not a) = (case formula_semantics_tt 𝒜 a of True  False | False  True)" |
"formula_semantics_tt 𝒜 (And a b) = (case (formula_semantics_tt 𝒜 a, formula_semantics_tt 𝒜 b) of
  (False, False)  False
| (False, True)  False
| (True, False)  False
| (True, True)  True)" |
"formula_semantics_tt 𝒜 (Or a b) = (case (formula_semantics_tt 𝒜 a, formula_semantics_tt 𝒜 b) of
  (False, False)  False
| (False, True)  True
| (True, False)  True
| (True, True)  True)" |
"formula_semantics_tt 𝒜 (Imp a b) = (case (formula_semantics_tt 𝒜 a, formula_semantics_tt 𝒜 b) of
  (False, False)  True
| (False, True)  True
| (True, False)  False
| (True, True)  True)"
private lemma "A  F  formula_semantics_tt A F"
  by(induction F; simp split: prod.splits bool.splits)
end

definition entailment :: "'a formula set  'a formula  bool" ("(_ / _)" (* \TTurnstile *) [53,53] 53) where
"Γ  F  (𝒜. ((G  Γ. 𝒜  G)  (𝒜  F)))"
text‹We write entailment differently than semantics (⊨› vs. ⊫›).
For humans, it is usually pretty clear what is meant in a specific situation, 
but it often needs to be decided from context that Isabelle/HOL does not have.›
  
text‹Some helpers for the derived connectives›
lemma top_semantics[simp,intro!]: "A  " unfolding Top_def by simp
lemma BigAnd_semantics[simp]: "A  F  (f  set F. A  f)" by(induction F; simp)
lemma BigOr_semantics[simp]: "A  F  (f  set F. A  f)" by(induction F; simp)
    
text‹Definitions for sets of formulae, used for compactness and model existence.›

definition "sat S  𝒜. F  S. 𝒜  F"
definition "fin_sat S  (s  S. finite s  sat s)"
  
lemma entail_sat: "Γ    ¬ sat Γ" (* btw. *)
  unfolding sat_def entailment_def by simp

lemma pn_atoms_updates: "p  snd (pn_atoms F)  n  fst (pn_atoms F) 
  ((M  F  (M(p := True)  F  M(n := False)  F)))  ((¬(M  F))  ¬(M(n := True)  F)  ¬(M(p := False)  F))"
proof(induction F arbitrary: n p)
  case (Imp F G)
  from Imp.prems have prems:
     "p  fst (pn_atoms F)" "p  snd (pn_atoms G)"
     "n  snd (pn_atoms F)" "n  fst (pn_atoms G)"
    by(simp_all add: prod_unions_def split: prod.splits)
  have IH1: "M  F  M(n := True)  F" " M  F  M(p := False)  F" "¬ M  F  ¬ M(p := True)  F" "¬ M  F  ¬ M(n := False)  F"
    using Imp.IH(1)[OF prems(3) prems(1)] by blast+
  have IH2: "M  G  M(p := True)  G" "M  G  M(n := False)  G" "¬ M  G  ¬ M(n := True)  G" "¬ M  G  ¬ M(p := False)  G" 
    using Imp.IH(2)[OF prems(2) prems(4)] by blast+
   show ?case proof(intro conjI; intro impI)
     assume "M  F  G"
     then consider "¬ M  F" | "M G" by auto
     thus "M(p := True)  F  G  M(n := False)  F  G" using IH1(3,4) IH2(1,2) by cases simp_all
   next
     assume "¬(M  F  G)"
     hence "M  F" "¬M  G" by simp_all
     thus "¬ M(n := True)  F  G  ¬ M(p := False)  F  G" using IH1(1,2) IH2(3,4) by simp
   qed
 next
  case (And F G)
  from And.prems have prems:
     "p  snd (pn_atoms F)" "p  snd (pn_atoms G)"
     "n  fst (pn_atoms F)" "n  fst (pn_atoms G)"
    by(simp_all add: prod_unions_def split: prod.splits)
  have IH1: "M  F  M(p := True)  F" " M  F  M(n := False)  F" "¬ M  F  ¬ M(n := True)  F" "¬ M  F  ¬ M(p := False)  F"
    using And.IH(1)[OF prems(1) prems(3)] by blast+
  have IH2: "M  G  M(p := True)  G" "M  G  M(n := False)  G" "¬ M  G  ¬ M(n := True)  G" "¬ M  G  ¬ M(p := False)  G" 
    using And.IH(2)[OF prems(2) prems(4)] by blast+
  show ?case proof(intro conjI; intro impI)
    assume "¬M  F  G"
    then consider "¬ M  F" | "¬ M G" by auto
    thus "¬ M(n := True)  F  G  ¬ M(p := False)  F  G" using IH1 IH2 by cases simp_all
  next
    assume "M  F  G"
    hence "M  F" "M  G" by simp_all
    thus "M(p := True)  F  G  M(n := False)  F  G " using IH1 IH2 by simp
  qed
next
  case (Or F G)
  from Or.prems have prems:
     "p  snd (pn_atoms F)" "p  snd (pn_atoms G)"
     "n  fst (pn_atoms F)" "n  fst (pn_atoms G)"
    by(simp_all add: prod_unions_def split: prod.splits)
  have IH1: "M  F  M(p := True)  F" " M  F  M(n := False)  F" "¬ M  F  ¬ M(n := True)  F" "¬ M  F  ¬ M(p := False)  F"
    using Or.IH(1)[OF prems(1) prems(3)] by blast+
  have IH2: "M  G  M(p := True)  G" "M  G  M(n := False)  G" "¬ M  G  ¬ M(n := True)  G" "¬ M  G  ¬ M(p := False)  G" 
    using Or.IH(2)[OF prems(2) prems(4)] by blast+
  show ?case proof(intro conjI; intro impI)
    assume "M  F  G"
    then consider "M  F" | "M G" by auto
    thus "M(p := True)  F  G  M(n := False)  F  G" using IH1 IH2 by cases simp_all
  next
    assume "¬M  F  G"
    hence "¬M  F" "¬M  G" by simp_all
    thus "¬M(n := True)  F  G  ¬M(p := False)  F  G " using IH1 IH2 by simp
  qed
qed simp_all
  
lemma const_simplifier_correct: "𝒜  simplify_consts F  𝒜  F"
  by (induction F) (auto simp add: Let_def isstop_def Top_def split: formula.splits) 
 
end

Theory Substitution

subsection‹Substitutions›
theory Substitution
imports Formulas
begin

primrec subst where
"subst A F (Atom B) = (if A = B then F else Atom B)" |
"subst _ _  = " |
"subst A F (G  H) = (subst A F G  subst A F H)" |
"subst A F (G  H) = (subst A F G  subst A F H)" |
"subst A F (G  H) = (subst A F G  subst A F H)" |
"subst A F (¬ H) = (¬ (subst A F H))"
term subst
abbreviation subst_syntax ("(_[/(_/'//_)])" [70,70] 69) where
"A[B / C]  subst C B A"

lemma no_subst[simp]: "k  atoms F  F[G / k] = F" by(induction F; simp)
lemma subst_atoms: "k  atoms F  atoms (F[G / k]) = atoms F - {k}  atoms G" 
proof(induction F)
  case (And F G) thus ?case by(cases "k  atoms F"; force) next
  case (Or F G) thus ?case by(cases "k  atoms F"; force) next
  case (Imp F G) thus ?case by(cases "k  atoms F"; force) next
qed simp_all

lemma subst_atoms_simp: "atoms (F[G / k]) = atoms F - {k}  (if k  atoms F then atoms G else {})"
  by(simp add: subst_atoms)

end

Theory Substitution_Sema

theory Substitution_Sema
imports Substitution Sema
begin

lemma substitution_lemma: "𝒜  F[G / n]  𝒜(n := 𝒜  G)  F" by(induction F; simp)

end

Theory CNF

subsection‹Conjunctive Normal Forms›
theory CNF
imports Main "HOL-Library.Simps_Case_Conv"
begin

datatype 'a literal = Pos 'a ("(_+)" [1000] 999) | Neg 'a ("(_¯)" [1000] 999)

type_synonym 'a clause = "'a literal set"
abbreviation empty_clause ("" (* \box *)) where "  {} :: 'a clause"
(* unfortunately, we'll also have those as lists, occasionally. *)

primrec atoms_of_lit where
"atoms_of_lit (Pos k) = k" |
"atoms_of_lit (Neg k) = k"
case_of_simps lit_atoms_cases: atoms_of_lit.simps

definition "atoms_of_cnf c = atoms_of_lit ` c"
lemma atoms_of_cnf_alt: "atoms_of_cnf c = (((`) atoms_of_lit) ` c)" 
  unfolding atoms_of_cnf_def by blast (* alt as in the German alt *)

lemma atoms_of_cnf_Un: "atoms_of_cnf (S  T) = atoms_of_cnf S  atoms_of_cnf T"
  unfolding atoms_of_cnf_def by auto

(* unbreak set printing *)
term "{0+}::nat clause"
translations
  "{x}" <= "CONST insert x "
term "{0+}::nat clause"
(* hope nobody ever loads this with some other definition for □ *)

end

Theory CNF_Formulas

text‹CNFs alone are nice, but now we want to relate between CNFs and formulas.›
theory CNF_Formulas
imports Formulas CNF
begin
  
context begin

(* attempts to eliminate ⊥ from formulas while converting to nnf have been made.
But that just gives you additional cases. So nnfs and cnfs will contain ⊥ *) 

function (sequential) nnf where
"nnf (Atom k) = (Atom k)" |
"nnf  = " |
"nnf (Not (And F G)) = Or (nnf (Not F)) (nnf (Not G))" |
"nnf (Not (Or F G)) = And (nnf (Not F)) (nnf (Not G))" |
"nnf (Not (Not F)) = nnf F" |
"nnf (Not (Imp F G)) = And (nnf F) (nnf (Not G))" |
"nnf (Not F) = (Not F)" |
"nnf (And F G) = And (nnf F) (nnf G)" |
"nnf (Or F G) = Or (nnf F) (nnf G)" |
"nnf (Imp F G) = Or (nnf (Not F)) (nnf G)"
  by(pat_completeness) auto

private fun nnf_cost where
"nnf_cost (Atom _) = 42" | 
"nnf_cost  = 42" |
"nnf_cost (Not F) = Suc (nnf_cost F)" |
"nnf_cost (And F G) = Suc (nnf_cost F + nnf_cost G)" |
"nnf_cost (Or F G) = Suc (nnf_cost F + nnf_cost G)" |
"nnf_cost (Imp F G) = Suc (Suc (nnf_cost F + nnf_cost G))" (* this is why *)

termination nnf by(relation "measure (λF. nnf_cost F)"; simp)

lemma "nnf ((Atom (k::nat))  (Not ((Atom l)  (Not (Atom m))))) = ¬ (Atom k)  (¬ (Atom l)  Atom m)"
  by code_simp

fun is_lit_plus where
"is_lit_plus  = True" |
"is_lit_plus (Not ) = True" |
"is_lit_plus (Atom _) = True" |
"is_lit_plus (Not (Atom _)) = True" |
"is_lit_plus _ = False"
case_of_simps is_lit_plus_cases: is_lit_plus.simps
fun is_disj where
(* It is crucial for this to be a (right) deep tree for the proof of LSC ⟹ Res
  At some point, we obtain a subset A where A is in a disjunction from (A ∨ B). 
  Now, resolution is at a loss because you can't say anything about the subset.
  If, however, that subset is sandwiched between a literal and the empty clause,
  you can just cover all the cases. *)
"is_disj (Or F G) = (is_lit_plus F  is_disj G)" |
"is_disj F = is_lit_plus F"
fun is_cnf where
(* here, we do want to allow arbitrary trees of ∧.
  If we do not do that, the proofs in LSC_Resolution won't work,
  since it relies on the ∧ case being just
  a simple split in LSC and union in Resolution.
  It is possible that that is fixable, but at what cost? *)
"is_cnf (And F G) = (is_cnf F  is_cnf G)" |
"is_cnf H = is_disj H"
fun is_nnf where
"is_nnf (Imp F G) = False" |
"is_nnf (And F G) = (is_nnf F  is_nnf G)" |
"is_nnf (Or F G) = (is_nnf F  is_nnf G)" |
"is_nnf F = is_lit_plus F"

lemma is_nnf_nnf: "is_nnf (nnf F)"
  by(induction F rule: nnf.induct; simp)
lemma nnf_no_imp: "A  B  set (subformulae (nnf F))"
  by(induction F rule: nnf.induct; simp)
lemma subformulae_nnf: "is_nnf F  G  set (subformulae F)  is_nnf G" (* fun fact *)
  by(induction F rule: is_nnf.induct; simp add: is_lit_plus_cases split: formula.splits; elim disjE conjE; simp)
lemma is_nnf_NotD: "is_nnf (¬ F)  (k. F = Atom k)  F = "
  by(cases F; simp)

fun cnf :: "'a formula  'a clause set" where
"cnf (Atom k) = {{ k+ }}" |
"cnf (Not (Atom k)) = {{ k¯ }}" |
"cnf  = {}" |
"cnf (Not ) = {}"  |
"cnf (And F G) = cnf F  cnf G"  |
"cnf (Or F G) = {C  D| C D. C  (cnf F)  D  (cnf G)}"

lemma cnf_fin:
assumes "is_nnf F"
shows "finite (cnf F)" "C  cnf F  finite C"
proof -
  have "finite (cnf F)  (C  cnf F  finite C)" using assms
    by(induction F arbitrary: C rule: cnf.induct;  clarsimp simp add: finite_image_set2)
  thus "finite (cnf F)" "C  cnf F  finite C" by simp+
qed

(* Sets, as produced by @{const cnf} can be hard to handle.
   Less because of their infinity, more because of their lack of explicit order. *)
fun cnf_lists :: "'a formula  'a literal list list" where
"cnf_lists (Atom k) = [[ k+ ]]" |
"cnf_lists (Not (Atom k)) = [[ k¯ ]]" |
"cnf_lists  = [[]]" |
"cnf_lists (Not ) = []"  |
"cnf_lists (And F G) = cnf_lists F @ cnf_lists G"  |
"cnf_lists (Or F G) = [f @ g. f  (cnf_lists F), g  (cnf_lists G)]"

primrec form_of_lit where
"form_of_lit (Pos k) = Atom k" |
"form_of_lit (Neg k) = ¬(Atom k)"
case_of_simps form_of_lit_cases: form_of_lit.simps

definition "disj_of_clause c  [form_of_lit l. l  c]"
definition "form_of_cnf F  [disj_of_clause c. c  F]"
definition "cnf_form_of  form_of_cnf  cnf_lists"
lemmas cnf_form_of_defs = cnf_form_of_def form_of_cnf_def disj_of_clause_def

lemma disj_of_clause_simps[simp]:
  "disj_of_clause [] = "
  "disj_of_clause (F#FF) = form_of_lit F  disj_of_clause FF"
by(simp_all add: disj_of_clause_def)

lemma is_cnf_BigAnd: "is_cnf (ls)  (l  set ls. is_cnf l)"
  by(induction ls; simp)

private lemma BigOr_is_not_cnf'': "is_cnf (ls)  (l  set ls. is_lit_plus l)" 
proof(induction ls)
  case (Cons l ls)
  from Cons.prems have "is_cnf ( ls)" 
    by (metis BigOr.simps is_cnf.simps(3,5) is_disj.simps(1) list.exhaust)
  thus ?case using Cons by simp
qed simp
private lemma BigOr_is_not_cnf': "(l  set ls. is_lit_plus l)  is_cnf (ls)" 
  by(induction ls; simp) (metis BigOr.simps(1, 2) formula.distinct(25) is_cnf.elims(2) is_cnf.simps(3) list.exhaust)
  (* ugh *)
lemma BigOr_is_not_cnf: "is_cnf (ls)  (l  set ls. is_lit_plus l)"
  using BigOr_is_not_cnf' BigOr_is_not_cnf'' by blast

lemma is_nnf_BigAnd[simp]: "is_nnf (ls)  (l  set ls. is_nnf l)"
  by(induction ls; simp)
lemma is_nnf_BigOr[simp]: "is_nnf (ls)  (l  set ls. is_nnf l)"
  by(induction ls; simp)
lemma form_of_lit_is_nnf[simp,intro!]: "is_nnf (form_of_lit x)"
  by(cases x; simp)
lemma form_of_lit_is_lit[simp,intro!]: "is_lit_plus (form_of_lit x)"
  by(cases x; simp)
lemma disj_of_clause_is_nnf[simp,intro!]: "is_nnf (disj_of_clause F)"
  unfolding disj_of_clause_def by simp

lemma cnf_form_of_is: "is_nnf F  is_cnf (cnf_form_of F)"
  by(cases F) (auto simp: cnf_form_of_defs is_cnf_BigAnd BigOr_is_not_cnf)

lemma nnf_cnf_form: "is_nnf F  is_nnf (cnf_form_of F)"
  by(cases F) (auto simp add: cnf_form_of_defs)

lemma cnf_BigAnd: "cnf (ls) = (x  set ls. cnf x)"
  by(induction ls; simp)

lemma cnf_BigOr: "cnf ( (x @ y)) =  {f  g |f g. f  cnf (x)  g  cnf (y)}"
  by(induction x arbitrary: y; simp) (metis (no_types, hide_lams) sup.assoc)

lemma cnf_cnf: "is_nnf F  cnf (cnf_form_of F) = cnf F"
  by(induction F rule: cnf.induct; 
     fastforce simp add: cnf_form_of_defs cnf_BigAnd cnf_BigOr)
(* this is not an idempotency (is that a word?) lemma, since cnf_form_of is not idempotent. *)

lemma is_nnf_nnf_id: "is_nnf F  nnf F = F"
proof(induction rule: is_nnf.induct)
  fix v assume "is_nnf (¬ v)"
  thus "nnf (¬ v) = ¬ v" by(cases v rule: is_lit_plus.cases; simp)
qed simp_all
  
lemma disj_of_clause_is: "is_disj (disj_of_clause R)"
  by(induction R; simp)
    
lemma form_of_cnf_is_nnf: "is_nnf (form_of_cnf R)"
  unfolding form_of_cnf_def by simp
    
lemma cnf_disj: "cnf (disj_of_clause R) = {set R}"
  by(induction R; simp add: form_of_lit_cases split: literal.splits)
lemma cnf_disj_ex: "is_disj F  R. cnf F = {R}  cnf F = {}"
  by(induction F rule: is_disj.induct; clarsimp simp: is_lit_plus_cases split: formula.splits)
    
    
lemma cnf_form_of_cnf: "cnf (form_of_cnf S) = set (map set S)"
  unfolding form_of_cnf_def by (simp add: cnf_BigAnd cnf_disj) blast
    
lemma disj_is_nnf: "is_disj F  is_nnf F"
  by(induction F rule: is_disj.induct; simp add: is_lit_plus_cases split: formula.splits)
    
lemma nnf_BigAnd: "nnf (F) = (map nnf F)"
  by(induction F; simp)

end

end

Theory CNF_Sema

theory CNF_Sema
imports CNF
begin

(* 'a ⇒ bool is a valuation, but I do not want to include Sema just for that… *)
primrec lit_semantics :: "('a  bool)  'a literal  bool" where
"lit_semantics 𝒜 (k+) = 𝒜 k" |
"lit_semantics 𝒜 (k¯) = (¬𝒜 k)"
case_of_simps lit_semantics_cases: lit_semantics.simps
definition clause_semantics where
  "clause_semantics 𝒜 C  L  C. lit_semantics 𝒜 L"
definition cnf_semantics where
  "cnf_semantics 𝒜 S  C  S. clause_semantics 𝒜 C"


end

Theory CNF_Formulas_Sema

theory CNF_Formulas_Sema
imports CNF_Sema CNF_Formulas Sema
begin

lemma nnf_semantics: "𝒜  nnf F  𝒜  F"
  by(induction F rule: nnf.induct; simp)
  
lemma cnf_semantics: "is_nnf F  cnf_semantics 𝒜 (cnf F)  𝒜  F"
  by(induction F rule: cnf.induct; simp add: cnf_semantics_def clause_semantics_def ball_Un; metis Un_iff)
  (* surprisingly, the solvers are smarter if this one is done on mutlisets.*)

lemma cnf_form_semantics: 
  fixes F :: "'a formula"
  assumes nnf: "is_nnf F"
  shows "𝒜  cnf_form_of F  𝒜  F"
proof -
  define cnf_semantics_list
    where "cnf_semantics_list 𝒜 S  (s  set S. l  set s. lit_semantics 𝒜 (l :: 'a literal))"
    for 𝒜 S
  have tcn: "cnf F = set (map set (cnf_lists F))" using nnf
    by(induction F rule: cnf.induct) (auto simp add: image_UN image_comp comp_def )
  have "𝒜  F  cnf_semantics 𝒜 (cnf F)" using cnf_semantics[OF nnf] by simp
  also have " = cnf_semantics 𝒜 (set (map set (cnf_lists F)))" unfolding tcn ..
  also have " = cnf_semantics_list 𝒜 (cnf_lists F)"
    unfolding cnf_semantics_def clause_semantics_def cnf_semantics_list_def by fastforce
  also have " = 𝒜  (cnf_form_of F)" using nnf
    by(induction F rule: cnf_lists.induct;
       simp add: cnf_semantics_list_def cnf_form_of_defs  ball_Un bex_Un)
  finally show ?thesis by simp
qed
  
corollary "G. 𝒜  F  𝒜  G  is_cnf G"
  using cnf_form_of_is cnf_form_semantics is_nnf_nnf nnf_semantics by blast

end

Theory CNF_To_Formula

subsubsection‹Going back: CNFs to formulas›
theory CNF_To_Formula
imports CNF_Formulas "HOL-Library.List_Lexorder"
begin
  
text‹One downside of CNFs is that they cannot be converted back to formulas 
as-is in full generality.
If we assume an order on the atoms, we can convert finite CNFs.›
(* This theory was written after the theories that use the CNF, so I don't really know,
   but I suspect that you won't gain much from using this for the LSC lemmas… *)

instantiation literal :: (ord) ord
begin

definition
  literal_less_def: "xs < ys  (
    if atoms_of_lit xs = atoms_of_lit ys
    then (case xs of Neg _  (case ys of Pos _  True | _  False) | _  False)
    else atoms_of_lit xs < atoms_of_lit ys)"
  (* the how doesn't /really/ matter, but I still wanted something somewhat pretty. *)

definition
  literal_le_def: "(xs :: _ literal)  ys  xs < ys  xs = ys"

instance ..

end

instance literal :: (linorder) linorder
by standard (auto simp add: literal_less_def literal_le_def split: literal.splits if_splits)

definition formula_of_cnf where
  "formula_of_cnf S  form_of_cnf (sorted_list_of_set (sorted_list_of_set ` S))"
text‹To use the lexicographic order on lists, we first have to convert the clauses to lists,
then the set of lists of literals to a list.›

lemma "simplify_consts (formula_of_cnf ({{Pos 0}} :: nat clause set)) = Atom 0" by code_simp

lemma cnf_formula_of_cnf:
  assumes "finite S" "C  S. finite C"
  shows "cnf (formula_of_cnf S) = S"
  using assms by(simp add: cnf_BigAnd formula_of_cnf_def form_of_cnf_def cnf_disj)
(* again, formula_of_cnf ∘ cnf is not an identity transformation, not even if the formula is_cnf.
   (there may be a much stricter definition of is_cnf for which that is the case) *)
  
end

Theory Tseytin

subsubsection‹Tseytin transformation›

theory Tseytin
imports Formulas CNF_Formulas
begin

text‹The @{const cnf} transformation clearly has exponential complexity.
If the intention is to use Resolution to decide validity of a formula,
that is clearly a deal-breaker for any practical implementation,
since validity can be decided by brute force in exponential time.
This theory pair shows the Tseytin transformation, a way to transform a formula
while preserving validity.
The @{const cnf} of the transformed formula will have clauses with maximally 3 atoms,
and an amount of clauses linear in the size of the formula,
at the cost of introducing one new atom for each subformula of F› (i.e. @{term "size F"} many).
›
  
definition "pair_fun_upd f p  (case p of (k,v)  fun_upd f k v)"

lemma fold_pair_upd_triv: "A  fst ` set U  foldl pair_fun_upd F U A = F A"
  by(induction U arbitrary: F; simp)
    (metis fun_upd_apply pair_fun_upd_def prod.simps(2) surjective_pairing)

lemma distinct_pair_update_one: "(k,v)  set U  distinct (map fst U)  foldl pair_fun_upd F U k = v"
  by(induction U arbitrary: F; clarsimp simp add: pair_fun_upd_def fold_pair_upd_triv split: prod.splits) 
    (insert fold_pair_upd_triv, fastforce)
    
lemma distinct_zipunzip: "distinct xs  distinct (map fst (zip xs ys))" by (simp add: distinct_conv_nth)
    
(* hm, this foldl pair_fun_upd business might have been a bad idea. *)
lemma foldl_pair_fun_upd_map_of: "distinct (map fst U)  foldl pair_fun_upd F U = (λk. case map_of U k of Some v  v | None  F k)"
  by(unfold fun_eq_iff; induction U arbitrary: F; clarsimp split: option.splits simp: pair_fun_upd_def rev_image_eqI)

lemma map_of_map_apsnd: "map_of (map (apsnd t) M) = map_option t  (map_of M)"
  by(unfold fun_eq_iff comp_def; induction M; simp)
    

definition biimp (infix "" 67) where "F  G  (F  G)  (G  F)"
lemma atoms_biimp[simp]: "atoms (F  G) = atoms F  atoms G"
  unfolding biimp_def by auto
lemma biimp_size[simp]: "size (F  G) = (2 * (size F + size G)) + 3"
  by(simp add: biimp_def)
  
locale freshstuff =
  fixes fresh :: "'a set  'a"
  assumes isfresh: "finite S  fresh S  S"
begin
  
primrec nfresh where
"nfresh S 0 = []" |
"nfresh S (Suc n) = (let f = fresh S in f # nfresh (f  S) n)"

lemma length_nfresh: "length (nfresh S n) = n"
  by(induction n arbitrary: S; simp add: Let_def)
    
lemma nfresh_isfresh: "finite S  set (nfresh S n)  S = {}"
  by(induction n arbitrary: S; auto simp add: Let_def isfresh)
    
lemma nfresh_distinct: "finite S  distinct (nfresh S n)"
  by(induction n arbitrary: S; simp add: Let_def; meson disjoint_iff_not_equal finite_insert insertI1 nfresh_isfresh)

definition "tseytin_assmt F  let SF = remdups (subformulae F) in zip (nfresh (atoms F) (length SF)) SF"

lemma tseytin_assmt_distinct: "distinct (map fst (tseytin_assmt F))"
  unfolding tseytin_assmt_def using nfresh_distinct by (simp add: Let_def length_nfresh)
    
lemma tseytin_assmt_has: "G  set (subformulae F)  n. (n,G)  set (tseytin_assmt F)"
proof -
  assume "G  set (subformulae F)"
  then have "n. G = subformulae F ! n  n < length (subformulae F)"
    by (simp add: set_conv_nth)
  then have "a. (a, G)  set (zip (nfresh (atoms F) (length (subformulae F))) (subformulae F))"
    by (metis (no_types) in_set_zip length_nfresh prod.sel(1) prod.sel(2))
  thus ?thesis by(simp add: tseytin_assmt_def Let_def) (metis fst_conv in_set_conv_nth in_set_zip length_nfresh set_remdups snd_conv)
qed

lemma tseytin_assmt_new_atoms: "(k,l)  set (tseytin_assmt F)  k  atoms F"
  unfolding tseytin_assmt_def Let_def using nfresh_isfresh by (fastforce dest: set_zip_leftD)

primrec tseytin_tran1 where
"tseytin_tran1 S (Atom k) = [Atom k  S (Atom k)]" |
"tseytin_tran1 S  = [  S ]" |
"tseytin_tran1 S (Not F) = [S (Not F)  Not (S F)] @ tseytin_tran1 S F" |
"tseytin_tran1 S (And F G) = [S (And F G)  And (S F) (S G)] @ tseytin_tran1 S F @ tseytin_tran1 S G" |
"tseytin_tran1 S (Or F G) = [S (Or F G)  Or (S F) (S G)] @ tseytin_tran1 S F @ tseytin_tran1 S G" |
"tseytin_tran1 S (Imp F G) = [S (Imp F G)  Imp (S F) (S G)] @ tseytin_tran1 S F @ tseytin_tran1 S G"
definition "tseytin_toatom F  Atom  the  map_of (map (λ(a,b). (b,a)) (tseytin_assmt F))"
definition "tseytin_tran F  (let S = tseytin_toatom F in S F # tseytin_tran1 S F)"
  
lemma distinct_snd_tseytin_assmt: "distinct (map snd (tseytin_assmt F))" 
  unfolding tseytin_assmt_def by(simp add: Let_def length_nfresh)

lemma tseytin_assmt_backlookup: assumes "J  set (subformulae F)" 
  shows "(the (map_of (map (λ(a, b). (b, a)) (tseytin_assmt F)) J), J)  set (tseytin_assmt F)"
proof -
  have 1: "distinct (map snd M)  J  snd ` set M  (the (map_of (map (λ(a, b). (b, a)) M) J), J)  set M" for J M
    by(induction M; clarsimp split: prod.splits)
  have 2: "J  set (subformulae F)  J  snd ` set (tseytin_assmt F)" for J using image_iff tseytin_assmt_has by fastforce
  from 1[OF distinct_snd_tseytin_assmt 2, OF assms] show ?thesis .
qed

lemma tseytin_tran_small_clauses: "C  cnf (nnf (tseytin_tran F)). card C  3"
proof -
  have 3: "card S  2  card (a  S)  3" for a S 
    by(cases "finite S"; simp add: card_insert_le_m1)
  have 2: "card S  1  card (a  S)  2" for a S 
    by(cases "finite S"; simp add: card_insert_le_m1)
  have 1: "card S  0  card (a  S)  1" for a S 
    by(cases "finite S"; simp add: card_insert_le_m1)
  have *: "G  set (tseytin_tran1 (Atom  S) F); C  cnf (nnf G)  card C  3" for G C S
    by(induction F arbitrary: G; simp add: biimp_def; (elim disjE exE conjE | intro 1 2 3 | simp)+)
  show ?thesis
    unfolding tseytin_tran_def  tseytin_toatom_def Let_def
    by(clarsimp simp add: cnf_BigAnd nnf_BigAnd comp_assoc *)
qed
  
lemma tseytin_tran_few_clauses: "card (cnf (nnf (tseytin_tran F)))  3 * size F + 1"
proof -
  have "size Bot = 1" by simp  (* just a thing to keep in mind. *)
  have ws: "{c  D |D. D = {c1}  D = {c2}} = {{c,c1},{c,c2}}" for c1 c2 c by auto
  have grr: "Suc (card S)  c  card (a  S)  c" for a S c
    by(cases "finite S"; simp add: card_insert_le_m1)
  have *: "card (aset (tseytin_tran1 (Atom  S) F). cnf (nnf a))  3 * size F" for S
    by(induction F; simp add: biimp_def; ((intro grr card_Un_le[THEN le_trans] | simp add: ws)+)?) 
  show ?thesis
    unfolding tseytin_tran_def tseytin_toatom_def Let_def
    by(clarsimp simp: nnf_BigAnd cnf_BigAnd; intro grr; simp add: comp_assoc *)
qed
  
lemma tseytin_tran_new_atom_count: "card (atoms (tseytin_tran F))  size F + card (atoms F)"
proof -
  have tseytin_tran1_atoms: "H  set (tseytin_tran1 (tseytin_toatom F) G)  G  set (subformulae F) 
    atoms H  atoms F  (I  set (subformulae F). atoms (tseytin_toatom F I))" for G H
  proof(induction G arbitrary: H)
    case (Atom k)
    hence "k  atoms F"
      by simp (meson formula.set_intros(1) rev_subsetD subformula_atoms)
    with Atom show ?case by simp blast
  next
    case Bot then show ?case by simp blast
  next
    case (Not G)
    show ?case by(insert Not.prems(1,2); 
         frule subformulas_in_subformulas; simp; elim disjE; (elim Not.IH | force))
  next
    case (And G1 G2)
    show ?case by(insert And.prems(1,2); 
         frule subformulas_in_subformulas; simp; elim disjE; (elim And.IH; simp | force))
  next
    case (Or G1 G2)
    show ?case by(insert Or.prems(1,2); 
         frule subformulas_in_subformulas; simp; elim disjE; (elim Or.IH; simp | force))
  next
    case (Imp G1 G2)
    show ?case by(insert Imp.prems(1,2); 
         frule subformulas_in_subformulas; simp; elim disjE; (elim Imp.IH; simp | force))
  qed
  have tseytin_tran1_atoms: "(Gset (tseytin_tran1 (tseytin_toatom F) F). atoms G) 
      atoms F  (Iset (subformulae F). atoms (tseytin_toatom F I))"
    using tseytin_tran1_atoms[OF _ subformulae_self] by blast
  have 1: "card (atoms (tseytin_tran F)) 
  card (atoms (tseytin_toatom F F)  (xset (tseytin_tran1 (tseytin_toatom F) F). atoms x))" 
    unfolding tseytin_tran_def by(simp add: Let_def tseytin_tran1_atoms)
  have 2: "atoms (tseytin_toatom F F)  (xset (tseytin_tran1 (tseytin_toatom F) F). atoms x) 
     (atoms F  (Iset (subformulae F). atoms (tseytin_toatom F I)))"
    using tseytin_tran1_atoms by blast
  have twofin: "finite (atoms F  (Iset (subformulae F). atoms (tseytin_toatom F I)))" by simp
  have card_subformulae: "card (set (subformulae F))  size F" using length_subformulae by (metis card_length)
  have card_singleton_union: "finite S  card (xS. {f x})  card S" for f S 
    by(induction S rule: finite_induct; simp add: card_insert_if)
  have 3: "card (Iset (subformulae F). atoms (tseytin_toatom F I))  size F"
    unfolding tseytin_toatom_def using le_trans[OF card_singleton_union card_subformulae]
    by simp fast
  have 4: "card (atoms (tseytin_tran F))  card (atoms F) + card (fset (subformulae F). atoms (tseytin_toatom F f))"
    using le_trans[OF 1 card_mono[OF twofin 2]] card_Un_le le_trans by blast
  show ?thesis using 3 4 by linarith
qed
    
end

definition "freshnat S   Suc (Max (0  S))"
primrec nfresh_natcode where
"nfresh_natcode S 0 = []" |
"nfresh_natcode S (Suc n) = (let f = freshnat S in f # nfresh_natcode (f  S) n)"
interpretation freshnats: freshstuff freshnat unfolding freshnat_def by standard (meson Max_ge Suc_n_not_le_n finite_insert insertCI)
(* interpreting the locale is easy. making it executable… not so. *)
lemma [code_unfold]: "freshnats.nfresh = nfresh_natcode"
proof -
  have "freshnats.nfresh S n  = nfresh_natcode S n" for S n by(induction n arbitrary: S; simp)
  thus ?thesis by auto
qed
lemmas freshnats_code[code_unfold] = freshnats.tseytin_tran_def freshnats.tseytin_toatom_def freshnats.tseytin_assmt_def freshnats.nfresh.simps
  
lemma "freshnats.tseytin_tran (Atom 0  (¬ (Atom 1))) = [
  Atom 2,
  Atom 2  Atom 3  Atom 4,
  Atom 0  Atom 3,
  Atom 4  ¬ (Atom 5),
  Atom 1  Atom 5
]" (is "?l = ?r")
proof -
  have "cnf (nnf ?r) =
    {{Pos 2},
     {Neg 4, Pos 2}, {Pos 3, Pos 2}, {Neg 2, Neg 3, Pos 4},
     {Neg 3, Pos 0}, {Neg 0, Pos 3},
     {Pos 5, Pos 4}, {Neg 4, Neg 5},
     {Neg 5, Pos 1}, {Neg 1, Pos 5}}" by eval
  have ?thesis by eval
  show ?thesis by code_simp
qed
    
end

Theory Tseytin_Sema

theory Tseytin_Sema
imports Sema Tseytin
begin           

lemma biimp_simp[simp]: "𝒜  F  G  (𝒜  F  𝒜  G)"
  unfolding biimp_def by auto
    
locale freshstuff_sema = freshstuff
begin
  
definition "tseytin_update 𝒜 F  (let U = map (apsnd (formula_semantics 𝒜)) (tseytin_assmt F) in foldl pair_fun_upd 𝒜 U)"

lemma tseyting_update_keep_subformula_sema: "G  set (subformulae F)  tseytin_update 𝒜 F  G  𝒜  G"
proof -
  assume "G  set (subformulae F)"
  hence sub: "atoms G  atoms F" by(fact subformula_atoms)
  have natoms: "k  atoms F  k  fst ` set (tseytin_assmt F)" for k l 
    using tseytin_assmt_new_atoms by force
  have "k  atoms F  tseytin_update 𝒜 F k = 𝒜 k" for k
    unfolding tseytin_update_def Let_def 
    by(force intro!: fold_pair_upd_triv dest!: natoms)
  thus ?thesis using relevant_atoms_same_semantics sub by (metis subsetCE)
qed   

lemma "(k,G)  set (tseytin_assmt F)  tseytin_update 𝒜 F k  tseytin_update 𝒜 F  G"
proof(induction F arbitrary: G)
  case (Atom x)
  then show ?case by(simp add: tseytin_update_def tseytin_assmt_def Let_def pair_fun_upd_def)
next
  case Bot
  then show ?case by(simp add: tseytin_update_def tseytin_assmt_def Let_def pair_fun_upd_def)
next
  case (Not F)
  then show ?case
    oops
      
lemma tseytin_updates: "(k,G)  set (tseytin_assmt F)  tseytin_update 𝒜 F k  tseytin_update 𝒜 F  G"
  apply(subst tseytin_update_def)
  apply(simp add: tseytin_assmt_def Let_def foldl_pair_fun_upd_map_of map_of_map_apsnd distinct_zipunzip[OF nfresh_distinct[OF atoms_finite]])
  apply(subst tseyting_update_keep_subformula_sema)
   apply(erule in_set_zipE; simp; fail)
  ..

lemma tseytin_tran1: "G  set (subformulae F)  H  set (tseytin_tran1 S G)  J  set (subformulae F). tseytin_update 𝒜 F  J  tseytin_update 𝒜 F  (S J)  tseytin_update 𝒜 F  H"
proof(induction G arbitrary: H)
  case Bot thus ?case by auto
next
  case (Atom k) thus ?case by fastforce
next
  case (Not G)
  consider "H = S (¬ G)  ¬ (S G)" | " H  set (tseytin_tran1 S G)" using Not.prems(2) by auto
  then show ?case proof cases
    case 1 then show ?thesis using Not.prems(3)
      by (metis Not.prems(1) biimp_simp formula_semantics.simps(3) set_subset_Cons subformulae.simps(3) subformulae_self subsetCE subsubformulae)
  next
    have D: "¬G  set (subformulae F)  G  set (subformulae F)"
      by(elim subsubformulae; simp)
    case 2 then show ?thesis using D Not.IH Not.prems(1,3) by blast
  qed
next
  case (And G1 G2)
  have el: "G1  set (subformulae F)" "G2  set (subformulae F)" using subsubformulae And.prems(1) by fastforce+
  with And.IH And.prems(3) have IH: "H  set (tseytin_tran1 S G1)  tseytin_update 𝒜 F  H"
                                    "H  set (tseytin_tran1 S G2)  tseytin_update 𝒜 F  H" for H
    by blast+
  show ?case using And.prems IH el by(simp; elim disjE; simp; insert And.prems(1) formula_semantics.simps(4), blast)
next
  case (Or G1 G2)
  have el: "G1  set (subformulae F)" "G2  set (subformulae F)" using subsubformulae Or.prems(1) by fastforce+
  with Or.IH Or.prems(3) have IH: "H  set (tseytin_tran1 S G1)  tseytin_update 𝒜 F  H"
                                  "H  set (tseytin_tran1 S G2)  tseytin_update 𝒜 F  H" for H
    by blast+
  show ?case using Or.prems(3,2) IH el by(simp; elim disjE; simp; metis Or.prems(1) formula_semantics.simps(5))
next
  case (Imp G1 G2)
  have el: "G1  set (subformulae F)" "G2  set (subformulae F)" using subsubformulae Imp.prems(1) by fastforce+
  with Imp.IH Imp.prems(3) have IH: "H  set (tseytin_tran1 S G1)  tseytin_update 𝒜 F  H"
                                    "H  set (tseytin_tran1 S G2)  tseytin_update 𝒜 F  H" for H
    by blast+
  show ?case using Imp.prems(3,2) IH el by(simp; elim disjE; simp; metis Imp.prems(1) formula_semantics.simps(6))
qed

lemma all_tran_formulas_validated: "J  set (subformulae F). tseytin_update 𝒜 F  J  tseytin_update 𝒜 F  (tseytin_toatom F J)"
  apply(simp add: tseytin_toatom_def)
  apply(intro ballI)
  apply(subst tseytin_updates)
   apply(erule tseytin_assmt_backlookup)
  ..

lemma tseytin_tran_equisat: "𝒜  F  tseytin_update 𝒜 F  (tseytin_tran F)"
  using all_tran_formulas_validated tseytin_tran1 all_tran_formulas_validated tseyting_update_keep_subformula_sema by(simp add: tseytin_tran_def Let_def) blast
(* unfortunately, that's not enough. *)
    
lemma tseytin_tran1_orig_connection: "G  set (subformulae F)  (Hset (tseytin_tran1 (tseytin_toatom F) G). 𝒜  H) 
  𝒜  G  𝒜  tseytin_toatom F G"
  by(induction G; simp; drule subformulas_in_subformulas; simp)

lemma tseytin_untran: "𝒜  (tseytin_tran F)  𝒜  F" 
proof -
  have 1: "𝒜  tseytin_toatom F F; 𝒜  F  tseytin_update 𝒜 F  tseytin_toatom F F"
    using all_tran_formulas_validated tseyting_update_keep_subformula_sema by blast
  let ?C = "λ𝒜. (H  set (tseytin_tran1 (tseytin_toatom F) F). 𝒜  H)"
  have 2: "?C 𝒜  ?C (tseytin_update 𝒜 F)"
    using all_tran_formulas_validated tseytin_tran1 by blast
  assume "𝒜  tseytin_tran F"
  hence "tseytin_update 𝒜 F  tseytin_tran F" 
    unfolding tseytin_tran_def
    apply(simp add: Let_def)
    apply(intro conjI)
     apply(elim conjE)
     apply(drule tseytin_tran1_orig_connection[OF subformulae_self])
     apply(clarsimp simp add: tseytin_assmt_distinct foldl_pair_fun_upd_map_of 1 2)+
    done
  thus ?thesis using tseytin_tran_equisat by blast
qed
lemma tseytin_tran_equiunsatisfiable: " ¬F   ¬ (tseytin_tran F)"  (is "?l  ?r")
proof(rule iffI; erule contrapos_pp)
  assume "¬?l"
  then obtain 𝒜 where "𝒜  F" by auto
  hence "tseytin_update 𝒜 F  (tseytin_tran F)" using tseytin_tran_equisat by simp
  thus "¬?r" by simp blast
next
  assume "¬?r"
  then obtain 𝒜 where "𝒜  tseytin_tran F" by auto
  thus "~?l" using tseytin_untran by simp blast 
qed
  
end
  
interpretation freshsemanats: freshstuff_sema freshnat
  by (simp add: freshnats.freshstuff_axioms freshstuff_sema_def)
print_theorems
(* Just showing that it is possible. There isn't really anything new that could be executed here. *)
  
end

Theory MiniFormulas

subsection‹Implication-only formulas›

theory MiniFormulas
imports Formulas
begin

fun is_mini_formula where
"is_mini_formula (Atom _) = True" |
"is_mini_formula  = True" |
"is_mini_formula (Imp F G) = (is_mini_formula F  is_mini_formula G)" |
"is_mini_formula _ = False"

text‹
  The similarity between these ``mini'' formulas and Johansson's minimal calculus of implications~\cite{johansson1937minimal} is mostly in name.
  Johansson does replace @{term "¬ F"} by @{term "F  "} in one place, but generally keeps it.
  The main focus of ~\cite{johansson1937minimal} is on removing rules from Calculi anyway, not on removing connectives.
  We are only borrowing the name.›

(*lemma mini_Top[simp,intro!]: "is_mini_formula ⊤" unfolding Top_def by simp *)

primrec to_mini_formula where
"to_mini_formula (Atom k) = Atom k" |
"to_mini_formula  = " |
"to_mini_formula (Imp F G) = to_mini_formula F  to_mini_formula G" |
"to_mini_formula (Not F) = to_mini_formula F  " |
"to_mini_formula (And F G) = (to_mini_formula F  (to_mini_formula G  ))  " |
"to_mini_formula (Or F G) = (to_mini_formula F  )  to_mini_formula G"

lemma to_mini_is_mini[simp,intro!]: "is_mini_formula (to_mini_formula F)"
  by(induction F; simp)
lemma mini_to_mini: "is_mini_formula F  to_mini_formula F = F"
  by(induction F; simp)
corollary mini_mini[simp]: "to_mini_formula (to_mini_formula F) = to_mini_formula F"
  using mini_to_mini[OF to_mini_is_mini] .

text‹We could have used an arbitrary other combination,
  e.g. @{const Atom}, @{const Not}, and @{const And}.
The choice for @{const Atom}, @{term }, and @{const Imp} was made because it is
 (to the best of my knowledge) the only combination that only requires three elements and verifies:›
lemma mini_formula_atoms: "atoms (to_mini_formula F) = atoms F"
 by(induction F; simp)
text‹(The story would be different if we had different junctors, e.g. if we allowed a NAND.)›

end

Theory MiniFormulas_Sema

theory MiniFormulas_Sema
imports MiniFormulas Sema
begin

lemma "A  F  A  to_mini_formula F"
  by(induction F) auto

end

Theory Consistency

subsection‹Consistency›

text‹We follow the proofs by Melvin Fitting~\cite{fitting1990first}.›
theory Consistency
imports Sema
begin

definition "Hintikka S  (
    S
 (k. Atom k  S  ¬ (Atom k)  S  False)
 (F G. F  G  S  F  S  G  S)
 (F G. F  G  S  F  S  G  S)
 (F G. F  G  S  ¬F  S  G  S)
 (F. ¬ (¬F)  S  F  S)
 (F G. ¬(F  G)  S  ¬ F  S  ¬ G  S)
 (F G. ¬(F  G)  S  ¬ F  S  ¬ G  S)
 (F G. ¬(F  G)  S  F  S  ¬ G  S)
)"

lemma "Hintikka {Atom 0  ((¬ (Atom 1))  Atom 2), ((¬ (Atom 1))  Atom 2), Atom 0, ¬(¬ (Atom 1)), Atom 1}"
  unfolding Hintikka_def by simp

theorem Hintikkas_lemma:
  assumes H: "Hintikka S"
  shows "sat S"
proof -
  from H[unfolded Hintikka_def]
  have H': "  S" 
    "Atom k  S  ¬ (Atom k)  S  False"
    "F  G  S  F  S  G  S"
    "F  G  S  F  S  G  S"
    "F  G  S  ¬F  S  G  S"
    "¬ (¬ F)  S  F  S"
    "¬ (F  G)  S  ¬ F  S  ¬ G  S"
    "¬ (F  G)  S  ¬ F  S  ¬ G  S"
    "¬ (F  G)  S  F  S  ¬ G  S"
    for k F G by blast+
  let ?M = "λk. Atom k  S"
  have "(F  S  (?M  F))  (¬ F  S  (¬(?M  F)))" for F
    by(induction F) (auto simp: H'(1) dest!: H'(2-))
  thus ?thesis unfolding sat_def by blast
qed

definition "pcp C  (S  C.
    S
 (k. Atom k  S  ¬ (Atom k)  S  False)
 (F G. F  G  S  F  G  S  C)
 (F G. F  G  S  F  S  C  G  S  C)
 (F G. F  G  S  ¬F  S  C  G  S  C)
 (F. ¬ (¬F)  S  F  S  C)
 (F G. ¬(F  G)  S  ¬ F  S  C  ¬ G  S  C)
 (F G. ¬(F  G)  S  ¬ F  ¬ G  S  C)
 (F G. ¬(F  G)  S  F  ¬ G  S  C)
)"

(* just some examples *)
lemma "pcp {}" "pcp {{}}" "pcp {{Atom 0}}" by (simp add: pcp_def)+
lemma "pcp {{(¬ (Atom 1))  Atom 2},
   {((¬ (Atom 1))  Atom 2), ¬(¬ (Atom 1))},
  {((¬ (Atom 1))  Atom 2), ¬(¬ (Atom 1)),  Atom 1}}" by (auto simp add: pcp_def)

text‹Fitting uses uniform notation~\cite{smullyan1963unifying} for the definition of @{const pcp}. 
We try to mimic this, more to see whether it works than because it is ultimately necessary.›
(* It does help a bit, occasionally. *)
    
inductive Con :: "'a formula => 'a formula => 'a formula => bool" where
"Con (And F G) F G" |
"Con (Not (Or F G)) (Not F) (Not G)" |
"Con (Not (Imp F G)) F (Not G)" |
"Con (Not (Not F)) F F"

inductive Dis :: "'a formula => 'a formula => 'a formula => bool" where
"Dis (Or F G) F G" |
"Dis (Imp F G) (Not F) G" |
"Dis (Not (And F G)) (Not F) (Not G)" |
"Dis (Not (Not F)) F F"

(* note that *)
lemma "Con (Not (Not F)) F F" "Dis (Not (Not F)) F F" by(intro Con.intros Dis.intros)+
(* i.e. ¬¬ is both Conjunctive and Disjunctive. I saw no reason to break this symmetry. *)

lemma con_dis_simps:
  "Con a1 a2 a3 = (a1 = a2  a3  (F G. a1 = ¬ (F  G)  a2 = ¬ F  a3 = ¬ G)  (G. a1 = ¬ (a2  G)  a3 = ¬ G)  a1 = ¬ (¬ a2)  a3 = a2)"
  "Dis a1 a2 a3 = (a1 = a2  a3  (F G. a1 = F  G  a2 = ¬ F  a3 = G)  (F G. a1 = ¬ (F  G)  a2 = ¬ F  a3 = ¬ G)  a1 = ¬ (¬ a2)  a3 = a2)"
  by(simp_all add: Con.simps Dis.simps)

lemma Hintikka_alt: "Hintikka S = (
    S
 (k. Atom k  S  ¬ (Atom k)  S  False)
 (F G H. Con F G H  F  S  G  S  H  S)
 (F G H. Dis F G H  F  S  G  S  H  S)
)"  
  apply(simp add: Hintikka_def con_dis_simps)
  apply(rule iffI)
    (* simp only: ∅ loops. :( *)
   subgoal by blast
  subgoal by safe metis+
done

lemma pcp_alt: "pcp C = (S  C.
    S
 (k. Atom k  S  ¬ (Atom k)  S  False)
 (F G H. Con F G H  F  S  G  H  S  C)
 (F G H. Dis F G H  F  S  G  S  C  H  S  C)
)"
  apply(simp add: pcp_def con_dis_simps)
  apply(rule iffI; unfold Ball_def; elim all_forward)
  by (auto simp add: insert_absorb split: formula.splits)
  
definition "subset_closed C  (S  C. sS. s  C)"
definition "finite_character C  (S. S  C  (s  S. finite s  s  C))"

lemma ex1: "pcp C  C'. C  C'  pcp C'  subset_closed C'"
proof(intro exI[of _ "{s . S  C. s  S}"] conjI)
  let ?E = "{s. SC. s  S}"
  show "C  ?E" by blast
  show "subset_closed ?E" unfolding subset_closed_def by blast
  assume C: ‹pcp C
  show "pcp ?E" using C unfolding pcp_alt
    by (intro ballI conjI; simp; meson insertI1 rev_subsetD subset_insertI subset_insertI2)
qed

lemma sallI: "(s. s  S  P s)  s  S. P s" by simp 

lemma ex2: 
  assumes fc: "finite_character C"
  shows "subset_closed C"
  unfolding subset_closed_def
proof (intro ballI sallI)
  fix s S
  assume e: S  C and s: s  S
  hence *: "t  s  t  S" for t by simp
  from fc have "t  S  finite t  t  C" for t unfolding finite_character_def using e by blast
  hence "t  s  finite t  t  C" for t using * by simp
  with fc show s  C unfolding finite_character_def by blast
qed

lemma
  assumes C: "pcp C"
  assumes S: "subset_closed C"
  shows ex3: "C'. C  C'  pcp C'  finite_character C'"
proof(intro exI[of _ "C  {S. s  S. finite s  s  C}"] conjI)
  let ?E = " {S. s  S. finite s  s  C}"
  show "C  C  ?E" by blast
  from S show "finite_character (C  ?E)" unfolding finite_character_def subset_closed_def by blast
  note C'' = C[unfolded pcp_alt, THEN bspec]
    
  (* uniform notation. what did I learn? only slightly more elegant… *)
  have CON: "G  H  S  C  {S. sS. finite s  s  C}" if si: "s. sS; finite s  s  C" and
    un: "Con F G H" and el: " F  S" for F G H S proof -
    have k: "s  S. finite s  F  s  G  H  s  C"
      using si un C'' by simp
    have "G  H  S  ?E"
      unfolding mem_Collect_eq Un_iff proof safe
      fix s
      assume "s  G  H  S" and f: "finite s"
      hence "F  (s - {G,H})  S" using el by blast
      with k f have "G  H  F  (s - {G,H})  C" by simp
      hence "F  G  H  s  C" using insert_absorb by fastforce
      thus "s  C" using S unfolding subset_closed_def by fast  
    qed
    thus "G  H  S  C  ?E" by simp
  qed
  have DIS: "G  S  C  {S. sS. finite s  s  C}  H  S  C  {S. sS. finite s  s  C}" 
    if si: "s. sS  finite s  s  C" and un: "Dis F G H" and el: "F  S"
    for F G H S proof -
    have l: "I{G, H}. I  s1  C  I  s2  C" 
      if "s1  S" "finite s1" "F  s1" 
         "s2  S" "finite s2" "F  s2" for s1 s2
    proof -
      let ?s = "s1  s2"
      have "?s  S" "finite ?s" using that by simp_all 
      with si have "?s  C" by simp
      moreover have "F  ?s" using that by simp
      ultimately have "I{G,H}. I  ?s  C"
        using C'' un by simp
      thus "I{G,H}. I  s1  C  I  s2  C"
        by (meson S[unfolded subset_closed_def, THEN bspec] insert_mono sup.cobounded2 sup_ge1)
    qed
    have m: "s1  S; finite s1; F  s1; G  s1  C; s2  S; finite s2; F  s2; H  s2  C  False" for s1 s2
      using l by blast
    have "False" if "s1  S" "finite s1" "G  s1  C" "s2  S" "finite s2" "H  s2  C" for s1 s2
    proof -
      have *: "F  s1  S" "finite (F  s1)" "F  F  s1" if  "s1  S" "finite s1" for s1
        using that el by simp_all
      have  "G  F  s1  C" "H  F  s2  C" 
        by (meson S insert_mono subset_closed_def subset_insertI that(3,6))+
      from m[OF *[OF that(1-2)] this(1) *[OF that(4-5)] this(2)]
      show False .
    qed
    hence "G  S  ?E  H  S  ?E"
      unfolding mem_Collect_eq Un_iff
      by (metis (no_types, lifting) finite_Diff insert_Diff si subset_insert_iff)
    thus "G  S  C  ?E  H  S  C  ?E" by blast
  qed
    
  (* this proof does benefit from uniform notation a bit. Before it was introduced,
     the subclaims CON, DIS had to be stated as *)  
  have CON': "f2 g2 h2 F2 G2 S2. s. s  C; h2 F2 G2  s  f2 F2  s  C  g2 G2  s  C; 
                                   sS2. finite s  s  C; h2 F2 G2  S2; False
       f2 F2  S2  C  {S. sS. finite s  s  C}  g2 G2  S2  C  {S. sS. finite s  s  C}" 
    by fast
  (* (without the False, obviously). The proof of the subclaim does not change gravely, 
      but the f2 g2 h2 have to be instantiated manually upon use (with, e.g., id Not (λF G. ¬(F  G))),
      and there were multiple working instantiations. Generally not as beautiful. *)

  show "pcp (C  ?E)" unfolding pcp_alt
    apply(intro ballI conjI; elim UnE; (unfold mem_Collect_eq)?)
           subgoal using C'' by blast
          subgoal using C'' by blast
         subgoal using C'' by (simp;fail)
        subgoal by (meson C'' empty_subsetI finite.emptyI finite_insert insert_subset subset_insertI)
       subgoal using C'' by simp
      subgoal using CON by simp
     subgoal using C'' by blast
    subgoal using DIS by simp
  done
qed

primrec pcp_seq where
"pcp_seq C S 0 = S" |
"pcp_seq C S (Suc n) = (
  let Sn = pcp_seq C S n; Sn1 = from_nat n  Sn in
  if Sn1  C then Sn1 else Sn
)"

lemma pcp_seq_in: "pcp C  S  C  pcp_seq C S n  C"
proof(induction n)
  case (Suc n)
  hence "pcp_seq C S n  C" by simp
  thus ?case by(simp add: Let_def)
qed simp
  
lemma pcp_seq_mono: "n  m  pcp_seq C S n  pcp_seq C S m"
proof(induction m)
  case (Suc m)
  thus ?case by(cases "n = Suc m"; simp add: Let_def; blast)
qed simp

lemma pcp_seq_UN: "{pcp_seq C S n|n. n  m} = pcp_seq C S m"
proof(induction m)
  case (Suc m)
  have "{f n |n. n  Suc m} = f (Suc m)  {f n |n. n  m}" for f using le_Suc_eq by auto
  hence "{pcp_seq C S n |n. n  Suc m} = pcp_seq C S (Suc m)  {pcp_seq C S n |n. n  m}" .
  hence "{pcp_seq C S n |n. n  Suc m} = {pcp_seq C S n |n. n  m}  pcp_seq C S (Suc m)" by auto
  thus ?case using Suc pcp_seq_mono by blast
qed simp
  
lemma wont_get_added: "(F :: ('a :: countable) formula)  pcp_seq C S (Suc (to_nat F))  F  pcp_seq C S (Suc (to_nat F) + n)"
text‹We don't necessarily have @{term "n = to_nat (from_nat n)"}, so this doesn't hold.›
oops

definition "pcp_lim C S  {pcp_seq C S n|n. True}"
  
lemma pcp_seq_sub: "pcp_seq C S n  pcp_lim C S"
  unfolding pcp_lim_def by(induction n; blast)
    
lemma pcp_lim_inserted_at_ex: "x  pcp_lim C S  k. x  pcp_seq C S k"
  unfolding pcp_lim_def by blast

lemma pcp_lim_in:
  assumes c: "pcp C"
  and el: "S  C"
  and sc: "subset_closed C"
  and fc: "finite_character C"
  shows "pcp_lim C S  C" (is "?cl  C")
proof -
  from pcp_seq_in[OF c el, THEN allI] have "n. pcp_seq C S n  C" .
  hence "m. {pcp_seq C S n|n. n  m}  C" unfolding pcp_seq_UN .
  
  have "s  ?cl. finite s  s  C"
  proof safe
    fix s :: "'a formula set"
    have "pcp_seq C S (Suc (Max (to_nat ` s)))  pcp_lim C S" using pcp_seq_sub by blast
    assume ‹finite s s  pcp_lim C S
    hence "k. s  pcp_seq C S k" 
    proof(induction s rule: finite_induct) 
      case (insert x s)
      hence "k. s  pcp_seq C S k" by fast
      then guess k1 ..
      moreover obtain k2 where "x  pcp_seq C S k2"
        by (meson pcp_lim_inserted_at_ex insert.prems insert_subset)
      ultimately have "x  s  pcp_seq C S (max k1 k2)"
        by (meson pcp_seq_mono dual_order.trans insert_subset max.bounded_iff order_refl subsetCE)
      thus ?case by blast
    qed simp
    with pcp_seq_in[OF c el] sc
    show "s  C" unfolding subset_closed_def by blast
  qed
  thus "?cl  C" using fc unfolding finite_character_def by blast
qed
  
lemma cl_max:
  assumes c: "pcp C"
  assumes sc: "subset_closed C"
  assumes el: "K  C"
  assumes su: "pcp_lim C S  K"
  shows "pcp_lim C S = K" (is ?e)
proof (rule ccontr)
  assume ¬?e
  with su have "pcp_lim C S  K" by simp
  then obtain F where e: "F  K" and ne: "F  pcp_lim C S" by blast
  from ne have "F  pcp_seq C S (Suc (to_nat F))" using pcp_seq_sub by fast
  hence 1: "F  pcp_seq C S (to_nat F)  C" by (simp add: Let_def split: if_splits)
  have "F  pcp_seq C S (to_nat F)  K" using pcp_seq_sub e su by blast
  hence "F  pcp_seq C S (to_nat F)  C" using sc unfolding subset_closed_def using el by blast
  with 1 show False ..
qed

lemma cl_max':
  assumes c: "pcp C"
  assumes sc: "subset_closed C"
  shows "F  pcp_lim C S  C  F  pcp_lim C S"
    "F  G  pcp_lim C S  C  F  pcp_lim C S  G  pcp_lim C S"
using cl_max[OF assms] by blast+

lemma pcp_lim_Hintikka:
  assumes c: "pcp C"
  assumes sc: "subset_closed C"
  assumes fc: "finite_character C"
  assumes el: "S  C"
  shows "Hintikka (pcp_lim C S)"
proof -
  let ?cl = "pcp_lim C S"
  have "?cl  C" using pcp_lim_in[OF c el sc fc] .
  from c[unfolded pcp_alt, THEN bspec, OF this]
  have d: "  ?cl"
    "Atom k  ?cl  ¬ (Atom k)  ?cl  False"
    "Con F G H  F  ?cl  G  H  ?cl  C"
    "Dis F G H  F  ?cl  G  ?cl  C  H  ?cl  C"
  for k F G H by blast+
  have
    "Con F G H  F  ?cl  G  ?cl  H  ?cl"
    "Dis F G H  F  ?cl  G  ?cl  H  ?cl"
    for F G H
    by(auto dest: d(3-) cl_max'[OF c sc])
  with d(1,2) show ?thesis unfolding Hintikka_alt by fast
qed
  
theorem pcp_sat: ― ‹model existence theorem›
  fixes S :: "'a :: countable formula set"
  assumes c: "pcp C"
  assumes el: "S  C"
  shows "sat S"
proof -
  note [[show_types]]
  from c obtain Ce where "C  Ce" "pcp Ce" "subset_closed Ce" "finite_character Ce" using ex1[where 'a='a] ex2[where 'a='a] ex3[where 'a='a]
    by (meson dual_order.trans ex2)
  have "S  Ce" using C  Ce el ..
  with pcp_lim_Hintikka ‹pcp Ce ‹subset_closed Ce ‹finite_character Ce
  have  "Hintikka (pcp_lim Ce S)" .
  with Hintikkas_lemma have "sat (pcp_lim Ce S)" .
  moreover have "S  pcp_lim Ce S" using pcp_seq.simps(1) pcp_seq_sub by fast
  ultimately show ?thesis unfolding sat_def by fast
qed
(* This and Hintikka's lemma are the only two where we need semantics. 
   Still, I don't think it's meaningful to separate those two into an extra theory. *)

end

Theory Compactness

subsection‹Compactness›

theory Compactness
imports Sema
begin

lemma fin_sat_extend: "fin_sat S  fin_sat (insert F S)  fin_sat (insert (¬F) S)"
proof (rule ccontr)
  assume fs: "fin_sat S"
  assume nfs: "¬ (fin_sat (insert F S)  fin_sat (insert (¬ F) S))"
  from nfs obtain s1 where s1: "s1  insert F S"       "finite s1" "¬sat s1" unfolding fin_sat_def by blast
  from nfs obtain s2 where s2: "s2  insert (Not F) S" "finite s2" "¬sat s2" unfolding fin_sat_def by blast
  let ?u = "(s1 - {F})  (s2 - {Not F})"
  have "?u  S" "finite ?u" using s1 s2 by auto
  hence "sat ?u" using fs unfolding fin_sat_def by blast
  then obtain A where A: "F  ?u. A  F" unfolding sat_def by blast
  have "A  F  A  ¬F" by simp
  hence "sat s1  sat s2" using A unfolding sat_def by(fastforce intro!: exI[where x=A])
  thus False using s1(3) s2(3) by simp
qed

context
begin

lemma fin_sat_antimono: "fin_sat F  G  F  fin_sat G" unfolding fin_sat_def by simp
lemmas fin_sat_insert = fin_sat_antimono[OF _ subset_insertI]

primrec extender :: "nat  ('a :: countable) formula set  'a formula set" where
"extender 0 S = S" |
"extender (Suc n) S = (
  let r = extender n S; 
  rt = insert (from_nat n) r;
  rf = insert (¬(from_nat n)) r
  in if fin_sat rf then rf else rt
)"

private lemma extender_fin_sat: "fin_sat S  fin_sat (extender n S)"
proof(induction n arbitrary: S)
  case (Suc n)
  note mIH = Suc.IH[OF Suc.prems]
  show ?case proof(cases "fin_sat (insert (Not (from_nat n)) (extender n S))")
    case True thus ?thesis by simp
  next
    case False
    hence "fin_sat (insert ((from_nat n)) (extender n S))" using mIH fin_sat_extend by auto
    thus ?thesis by(simp add: Let_def)
  qed
qed simp

definition "extended S = {extender n S|n. True}"

lemma extended_max: "F  extended S  Not F  extended S"
proof -
  obtain n where [simp]: "F = from_nat n" by (metis from_nat_to_nat)
  have "F  extender (Suc n) S  Not F  extender (Suc n) S" by(simp add: Let_def)
  thus ?thesis unfolding extended_def by blast
qed

private lemma extender_Sucset: "extender k S  extender (Suc k) S" by(force simp add: Let_def)
private lemma extender_deeper: "F  extender k S  k  l  F  extender l S" using extender_Sucset le_Suc_eq
  by(induction l) (auto simp del: extender.simps)
private lemma extender_subset: "S  extender k S"
proof -
  from extender_deeper[OF _ le0] have "F  extender 0 Sa  F  extender l Sa" for Sa l F .
  thus ?thesis by auto
qed

lemma extended_fin_sat: 
  assumes "fin_sat S"
  shows  "fin_sat (extended S)"
proof -
  have assm: "s  extender n S; finite s  sat s" for s n
    using extender_fin_sat[OF assms] unfolding fin_sat_def by presburger
  hence "sat s" if su: "s  {extender n S |n. True}" and fin: "finite s" for s proof -
    { fix x assume e: "x  s"
      with su have "x  {extender n S |n. True}" by blast
      hence "n. x  extender n S" unfolding Union_eq by blast }
    hence "x  s. n. x  extender n S" by blast
    from finite_set_choice[OF fin this] obtain f where cf: "xs. x  extender (f x) S" ..
    have "k. s  {extender n S |n. n  k}" proof(intro exI subsetI)
      fix x assume e: "x  s"
      with cf have "x  extender (f x) S" ..
      hence "x  extender (Max (f ` s)) S" by(elim extender_deeper; simp add: e fin)
      thus "x  {extender n S |n. n  Max (f ` s)}" by blast
    qed
    moreover have "{extender n S |n. n  k} = extender k S" for k proof(induction k) 
      case (Suc k)
      moreover have "{extender n S |n. n  Suc k} = {extender n S |n. n  k}  extender (Suc k) S" 
        unfolding Union_eq le_Suc_eq
        using le_Suc_eq by(auto simp del: extender.simps)
      ultimately show ?case using extender_Sucset by(force simp del: extender.simps)
    qed simp
    ultimately show "sat s" using assm fin by auto
  qed
  thus ?thesis unfolding extended_def fin_sat_def by presburger
qed

lemma extended_superset: "S  extended S" unfolding extended_def using extender.simps(1) by blast

lemma extended_complem:
  assumes fs: "fin_sat S"
  shows "(F  extended S)  (Not F  extended S)"
proof -
  note fs = fs[THEN extended_fin_sat]
  show ?thesis proof(cases "F  extended S")
    case False with extended_max show ?thesis by blast
  next
    case True have "Not F  extended S" proof 
      assume False: "Not F  extended S"
      with True have "{F, Not F}  extended S" by blast
      moreover have "finite {F, Not F}" by simp
      ultimately have "sat {F, Not F}" using fs unfolding fin_sat_def by blast
      thus False unfolding sat_def by simp
    qed
    with True show ?thesis by blast
  qed
qed

lemma not_fin_sat_extended_UNIV: fixes S :: "'a :: countable formula set" assumes "¬fin_sat S" shows "extended S = UNIV" 
text‹Note that this crucially depends on the fact that we check \emph{first} whether adding @{term "¬F"} makes the set not satisfiable, 
  and add @{term F} otherwise \emph{without any further checks}.
  The proof of compactness does (to the best of my knowledge) depend on neither of these two facts.›
proof -
  from assms[unfolded fin_sat_def, simplified] obtain s :: "'a :: countable formula set"
    where "finite s" "¬ sat s" by clarify
  from this(2)[unfolded sat_def, simplified] have "xs. ¬ A  x" for A ..
  have nfs: "¬fin_sat (insert x (extender n S))" for n x 
    apply(rule notI)
    apply(drule fin_sat_insert)
    apply(drule fin_sat_antimono)
     apply(rule extender_subset)
    apply(erule notE[rotated])
    apply(fact assms)
  done
  have "x  {extender n S |n. True}" for x proof cases
    assume "x  S" thus ?thesis by (metis extended_def extended_superset insert_absorb insert_subset)
  next
    assume "x  S"
    have "x  extender (Suc (to_nat x)) S" 
      unfolding extender.simps Let_def
      unfolding if_not_P[OF nfs] by simp
    thus ?thesis by blast
  qed
  thus ?thesis unfolding extended_def by auto
qed

lemma extended_tran: "S  T  extended S  extended T"
text‹This lemma doesn't hold: think of making S empty and inserting a formula into T s.t. it can never be satisfied simultaneously with the first 
non-tautological formula in the extension S. Showing that this is possible is not worth the effort, since we can't influence the ordering of formulae.
But we showed it anyway.›
oops
lemma extended_not_increasing: "S T. fin_sat S  fin_sat T  ¬ (S  T  extended S  extended (T :: 'a :: countable formula set))"
proof -
  have ex_then_min: "x :: nat. P x  P (LEAST x. P x)" for P using LeastI2_wellorder by auto
  define P where "P x = (let F = (from_nat x :: 'a formula) in (A. ¬ A  F)  ( A. A  F))" for x
  define x where "x = (LEAST n. P n)"
  hence "n. P n" unfolding P_def Let_def by(auto intro!: exI[where x="to_nat (Atom undefined :: 'a formula)"])
  from ex_then_min[OF this] have Px: "P x" unfolding x_def .
  have lessx: "n < x  ¬ P n" for n unfolding x_def using not_less_Least by blast
  let ?S = "{} :: 'a formula set" let ?T = "{from_nat x :: 'a formula}"
  have s: "fin_sat ?S" "fin_sat ?T" using Px unfolding P_def fin_sat_def sat_def Let_def by fastforce+
  have reject: "Q A  A. ¬ Q A  False" for A Q by simp
  have "y  x  F  extender y ?S   F" for F y
  proof(induction y arbitrary: F)
    case (Suc y)
    have *: "F  extender y {}   F" for F :: "'a formula" using Suc.IH Suc.prems(1) by auto
    let ?Y = "from_nat y :: 'a formula"
    have ex: "(A. ¬ A  ?Y)   ?Y" unfolding formula_semantics.simps by (meson P_def Suc.prems(1) Suc_le_lessD lessx)
    have 1: "A. ¬ A  ?Y" if "fin_sat (Not ?Y  extender y ?S)"
    proof -
      note[[show_types]]
      from that have "A. A  Not ?Y" unfolding fin_sat_def sat_def  by(elim allE[where x="{Not ?Y}"]) simp
      hence "¬ ?Y" by simp
      hence "A. ¬ A  ?Y" using ex by argo
      thus ?thesis by simp
    qed
    have 2: "¬ fin_sat (Not ?Y  extender y ?S)   ?Y"
    proof(erule contrapos_np)
      assume "¬  ?Y"
      hence "A. ¬ A  ?Y" using ex by argo
      hence " ¬ ?Y" by simp
      thus "fin_sat (¬ ?Y  extender y ?S)" unfolding fin_sat_def sat_def
        by(auto intro!: exI[where x="λ_ :: 'a. False"] dest!: rev_subsetD[rotated] *)
    qed
    show ?case using Suc.prems(2) by(simp add: Let_def split: if_splits; elim disjE; simp add: * 1 2)
  qed simp
  hence "fin_sat (¬ (from_nat x)  extender x ?S)" using Px unfolding P_def Let_def
    by (clarsimp simp: fin_sat_def sat_def) (insert formula_semantics.simps(3), blast)
  hence "Not (from_nat x)  extender (Suc x) ?S" by(simp)
  hence "Not (from_nat x)  extended ?S" unfolding extended_def by blast
  moreover have "Not (from_nat x)  extended ?T" using extended_complem extended_superset s(2) by blast
  ultimately show ?thesis using s by blast
qed

private lemma not_in_extended_FE: "fin_sat S  (¬sat (insert (Not F) G))  F  extended S  G  extended S  finite G  False"
proof(goal_cases)
  case 1
  hence "Not F  extended S" using extended_max by blast
  thus False using 1 extended_fin_sat fin_sat_def
    by (metis Diff_eq_empty_iff finite.insertI insert_Diff_if)
qed
  
lemma extended_id: "extended (extended S) = extended S" 
  using extended_complem extended_fin_sat extended_max extended_superset not_fin_sat_extended_UNIV 
  by(intro equalityI[rotated] extended_superset) blast
  
(* This would be nicer, though… 
inductive_set extended_set :: "form set ⇒ form set" for S where
"F ∈ S ⟹ F ∈ extended_set S" |
"fin_sat (insert F (extended_set S)) ∨ F ∈ extended_set S ⟹ F ∈ extended_set S"
but it can't work, as extended is not increasing (?) *)
  
lemma ext_model:
  assumes r: "fin_sat S"
  shows "(λk. Atom k  extended S)  F  F  extended S"
proof -
  note fs = r[THEN extended_fin_sat]
  have Elim: "F  S  G  S  {F,G}  S" "F  S  {F}  S" for F G S by simp+
  show ?thesis
  proof(induction F)
    case Atom thus ?case by(simp)
  next
    case Bot
    have False if "  extended S" proof -
      have "finite {}" by simp
      moreover from that have "{}  extended S" by simp
      ultimately have "A. A  " using fs unfolding fin_sat_def sat_def
        by(elim allE[of _ "{}"]) simp
      thus False by simp
    qed
    thus ?case by auto
  next
    case (Not F)
    moreover have "A  F  A  ¬F" for A F by simp
    ultimately show ?case using extended_complem[OF r] by blast
  next
    case (And F G)
    have "(F  extended S  G  extended S) = (F  G  extended S)" proof -
      have *: "¬sat {¬ (F  G), F, G}" "¬sat {¬ F, (F  G)}" "¬sat {¬ G, (F  G)}" unfolding sat_def by auto
      show ?thesis by(intro iffI; rule ccontr) (auto intro: *[THEN not_in_extended_FE[OF r]])
    qed
    thus ?case by(simp add: And) 
  next
    case (Or F G)
    have "(F  extended S  G  extended S) = (F  G  extended S)" proof -
      have "¬sat {¬(F  G), F}" "¬sat {¬(F  G), G}" unfolding sat_def by auto
      from this[THEN not_in_extended_FE[OF r]] have 1: "F  extended S  G  extended S; F  G  extended S  False" by auto
      have "¬sat {¬F, ¬G, F  G}" unfolding sat_def by auto
      hence 2: "F  G  extended S; F  extended S; G  extended S  False" using extended_max not_in_extended_FE[OF r] by fastforce
      show ?thesis by(intro iffI; rule ccontr) (auto intro: 1 2)
    qed
    thus ?case by(simp add: Or)
  next
    case (Imp F G)
    have "(F  extended S  G  extended S) = (F  G  extended S)" proof -
      have "¬sat {¬G, F, F  G}" unfolding sat_def by auto
      hence 1: "F  G  extended S; F  extended S; G  extended S  False" using extended_max not_in_extended_FE[OF r] by blast
      have "¬sat {¬F,¬(F  G)}" unfolding sat_def by auto
      hence 2: "F  G  extended S; F  extended S  False" using extended_max not_in_extended_FE[OF r] by blast
      have "¬sat {¬(F  G),G}" unfolding sat_def by auto
      hence 3: "F  G  extended S; G  extended S  False" using extended_max not_in_extended_FE[OF r] by blast
      show ?thesis by(intro iffI; rule ccontr) (auto intro: 1 2 3)
    qed
    thus ?case by(simp add: Imp)
  qed
qed

theorem compactness:
  fixes S :: "'a :: countable formula set"
  shows "sat S  fin_sat S" (is "?l = ?r")
proof
  assume ?l thus ?r unfolding sat_def fin_sat_def by blast
next
  assume r: ?r
  note ext_model[OF r, THEN iffD2]
  hence "FS. (λk. Atom k  extended S)  F" using extended_superset by blast
  thus ?l unfolding sat_def by blast
qed

corollary compact_entailment:
  fixes F :: "'a :: countable formula"
  assumes fent: "Γ  F"
  shows "Γ'. finite Γ'  Γ'  Γ  Γ'  F"
proof -
  have ND_sem:  "Γ  F  ¬sat (insert (¬F) Γ)" 
    for Γ F unfolding sat_def entailment_def by auto
  obtain Γ' where 0: "finite Γ'" "Γ'  F" "Γ'  Γ" proof(goal_cases)
    from fent[unfolded ND_sem compactness] have "¬ fin_sat (insert (¬ F) Γ)" .
    from this[unfolded fin_sat_def] obtain s where s: "s  insert(¬F) Γ" "finite s" "¬sat s" by blast
    have 2: "finite (s - {¬ F})" using s by simp
    have 3: "s - {¬ F}  F" unfolding ND_sem using s(3) unfolding sat_def by blast
    have 4: "s - {¬ F}  Γ" using s by blast
    case 1 from 2 3 4 show ?case by(intro 1[of "s - {Not F}"])
  qed
  thus ?thesis by blast
qed
  
corollary compact_to_formula:
  fixes F :: "'a :: countable formula"
  assumes fent: "Γ  F"
  obtains Γ' where "set Γ'  Γ" " (Γ')  F"
proof goal_cases
  case 1
  note compact_entailment[OF assms]
  then guess Γ' ..
  moreover then obtain Γ'' where "Γ' = set Γ''" using finite_list by auto
  ultimately show thesis by(intro 1)  (blast, simp add: entailment_def)
qed

end
    
end

Theory Compactness_Consistency

theory Compactness_Consistency
imports Consistency
begin
  
theorem "sat S  fin_sat (S :: 'a :: countable formula set)" (is "?l = ?r")
proof
  assume 0: ?r
  let ?C = "{W :: 'a formula set. fin_sat W}"
  have 1: "S  ?C" using 0 unfolding mem_Collect_eq .
  have 2: "pcp ?C" proof -
    { fix S :: "'a formula set"
      assume "S  ?C"
      hence a: "sS. finite s  (𝒜. Fs. 𝒜  F)" by (simp add: fin_sat_def sat_def)
      have conj: "h F G  S; s  f F  g G  S; finite s;
        A. A  h F G  A  f F  A  g G  𝒜. Fs. 𝒜  F" 
        for F G s and f g :: "'a formula  'a formula" and h :: "'a formula  'a formula  'a formula"
      proof goal_cases
        case 1
        have "h F G  s - {f F,g G}S" "finite (h F G  s-{f F,g G})" using 1 by auto
        then obtain A where 2: "Hh F G  s-{f F,g G}. A  H" using a by presburger
        hence "A  f F" "A  g G" using 1(4) by simp_all
        with 2 have "Hh F G  s. A  H" by blast
        thus ?case by blast
      qed
      have disj: "h F G  S; s1  f F  S; s2  g G  S; finite s1; 𝒜. xs1. ¬ 𝒜  x; finite s2; 𝒜. xs2. ¬ 𝒜  x;
        A. A  h F G  A  f F  A  g G  False"
        for F G s1 s2 and f g :: "'a formula  'a formula" and h :: "'a formula  'a formula  'a formula" 
      proof goal_cases
        case 1
        let ?U = "h F G  (s1 - {f F})  (s2 - {g G})"
        have "?U  S" "finite ?U" using 1 by auto
        with a obtain A where 2: "H  ?U  A  H" for H by meson
        with 1(1) 1(8)  have "A  f F  A  g G" by force
        hence "(H  s1. A  H)  (H  s1. A  H)" using 1(7) 2
          by (metis DiffI Diff_empty Diff_iff UnCI insert_iff)
        thus ?case using 1 by fast
      qed
      have 1: "  S" using a by (meson empty_subsetI finite.emptyI finite.insertI formula_semantics.simps(2) insertI1 insert_subset)
      have 2: "Atom k  S  ¬ (Atom k)  S  False" for k using a[THEN spec[of _ "{Atom k, ¬(Atom k)}"]] by auto
      have 3: "F  G  S  F  G  S  Collect fin_sat" for F G unfolding fin_sat_def sat_def mem_Collect_eq using conj[] by fastforce
      have 4: "F  G  S  F  S  Collect fin_sat  G  S  Collect fin_sat" for F G
        unfolding fin_sat_def sat_def mem_Collect_eq using disj[of Or F G _ "λk. k" _ "λk. k"] by (metis formula_semantics.simps(5))
      have 5: "F  G  S  ¬ F  S  Collect fin_sat  G  S  Collect fin_sat" for F G
        unfolding fin_sat_def sat_def mem_Collect_eq using disj[of Imp F G _ Not _ "λk. k"] by (metis formula_semantics.simps(3,6))
      have 6: "¬ (¬ F)  S  F  S  Collect fin_sat" for F unfolding fin_sat_def sat_def mem_Collect_eq using conj[of "λF G. Not (Not F)" F F _ "λk. k" "λk. k"] by simp
      have 7: "¬ (F  G)  S  ¬ F  S  Collect fin_sat  ¬ G  S  Collect fin_sat" for F G
        unfolding fin_sat_def sat_def mem_Collect_eq using disj[of "λF G. Not (And F G)" F G _ Not _ Not] by (metis formula_semantics.simps(3,4))
      have 8: "F G. ¬ (F  G)  S  ¬ F  ¬ G  S  Collect fin_sat" unfolding fin_sat_def sat_def mem_Collect_eq using conj[] by fastforce
      have 9: "F G. ¬ (F  G)  S  F  ¬ G  S  Collect fin_sat" unfolding fin_sat_def sat_def mem_Collect_eq using conj[] by fastforce
      note 1 2 3 4 5 6 7 8 9
    }
    thus "pcp ?C" unfolding pcp_def by auto
  qed
  from pcp_sat 2 1 show ?l .
next
  assume ?l thus ?r unfolding sat_def fin_sat_def by blast
qed

end

Theory Sema_Craig

subsection‹Craig Interpolation using Semantics›

theory Sema_Craig
imports Substitution_Sema
begin

text‹Semantic proof of Craig interpolation following Harrison~\cite{harrison2009handbook}.›
  
(* we don't really need this lemma, sledgehammer would find a proof anyway. But it would be massively ugly. *)
lemma subst_true_false:
  assumes "𝒜  F"
  shows "𝒜  ((F[ / n])  (F[ / n]))"
using assms by(cases "𝒜 n"; simp add: substitution_lemma fun_upd_idem)

theorem interpolation:
  assumes " Γ  Δ"
  obtains ρ where
    " Γ  ρ" " ρ  Δ"
    "atoms ρ  atoms Γ"
    "atoms ρ  atoms Δ"
proof(goal_cases)
  let ?as = "atoms Γ - atoms Δ"
  have fas: "finite ?as" by simp
  from fas assms have "ρ. (( Γ  ρ)  ( ρ  Δ)  (atoms ρ  atoms Γ)  (atoms ρ  atoms Δ))"
  proof(induction ?as arbitrary: Γ rule: finite_induct)
    case empty
    from {} = atoms Γ - atoms Δ have "atoms Γ  atoms Δ" by blast
    with  Γ  Δ show ?case by(intro exI[where x=Γ]) simp
  next
    case (insert a A)
    hence e: "a  atoms Γ" "a  atoms Δ" by auto
    define Γ' where "Γ' = (Γ[ / a])  (Γ[ / a])"
    have su: "atoms Γ'  atoms Γ" unfolding Γ'_def by(cases "a  atoms Γ"; simp add: subst_atoms)
    from  Γ  Δ e have " Γ'  Δ" by (auto simp add: substitution_lemma Γ'_def)
    from a  A = atoms Γ - atoms Δ a  A e have "A = atoms Γ' - atoms Δ" by(simp add: subst_atoms Γ'_def) blast
    from insert.hyps(3)[OF this  Γ'  Δ] obtain ρ where ρ: " Γ'  ρ" " ρ  Δ" "atoms ρ  atoms Γ'" "atoms ρ  atoms Δ" by clarify
    have " Γ  ρ" using ρ(1) subst_true_false unfolding Γ'_def by fastforce
    with ρ su show ?case by(intro exI[where x=ρ]) simp
  qed
  moreover case 1
  ultimately show thesis by blast
qed
  
text‹The above proof is constructive, and it is actually very easy to write a procedure down.›
function interpolate where
"interpolate F H = (
let K = atoms F - atoms H in
  if K = {}
  then F
  else (
    let k = Min K
    in interpolate ((F[ / k])  (F[ / k])) H
  )
)" by pat_completeness simp
(* I tried Inf instead of Min first. Only has downsides. *)

text‹Showing termination is slightly technical\dots›
termination interpolate
  apply(relation "measure (λ(F,H). card (atoms F - atoms H))") 
              (* "measure (λ(F,H). card (atoms F))" also works, but doesn't make things more beautiful *)
   subgoal by simp
  apply (simp add: subst_atoms_simp)
  apply(intro conjI impI)
   apply(intro psubset_card_mono)
    subgoal by simp
   apply(subgoal_tac "Min (atoms F - atoms H)  atoms H")
    subgoal by blast
   apply (meson atoms_finite Diff_eq_empty_iff Diff_iff Min_in finite_Diff)+
done

text‹Surprisingly, @{const interpolate} is even executable,
  despite all the set operations involving @{const atoms}
lemma "interpolate (And (Atom (0::nat)) (Atom 1)) (Or (Atom 1) (Atom 2)) = 
  (  Atom 1)  (  Atom 1)" by simp
value[code] "simplify_consts (interpolate (And (Atom (0::nat)) (Atom 1)) (Or (Atom 1) (Atom 2)))"
(* and the wikipedia example: *)
lemma "let P = Atom (0 :: nat); Q = Atom 1; R = Atom 2; T = Atom 3;
φ = (¬(P  Q))  (¬R  Q);
ψ = (T  P)  (T  (¬R));
I = interpolate φ ψ in
(size I) = 23  simplify_consts I = Atom 2  Atom 0"
  by code_simp

theorem nonexistential_interpolation:
  assumes " F  H"
  shows
    " F  interpolate F H" (is "?t1") " interpolate F H  H" (is "?t2")
    "atoms (interpolate F H)  atoms F  atoms H" (is "?s")
proof -
  let ?as = "atoms F - atoms H"
  have fas: "finite ?as" by simp
  hence "?t1  ?t2  ?s" using assms
  proof(induction "card ?as" arbitrary: F H)
    case (Suc n)
    let ?inf = "Min (atoms F - atoms H)"
    define G where "G = (F[ / ?inf])  (F[ / ?inf])"
    have e: "Min (atoms F - atoms H)  atoms F - atoms H" by (metis Min_in Suc.hyps(2) Suc.prems(1) card.empty nat.simps(3))
    with Suc(2) have "n = card (atoms G - atoms H)" unfolding G_def subst_atoms_simp
    proof -
      assume a1: "Suc n = card (atoms F - atoms H)"
      assume "Min (atoms F - atoms H)  atoms F - atoms H"
      hence a2: "Min (atoms F - atoms H)  atoms F  Min (atoms F - atoms H)  atoms H" by simp
      have "n = card (atoms F - atoms H) - 1"
        using a1 by presburger
      hence "n = card (atoms (F[ / Min (atoms F - atoms H)])  atoms (F[ / Min (atoms F - atoms H)]) - atoms H)"
        using a2 by (metis (full_types) formula.set(2) Diff_insert Diff_insert2 Suc.prems(1) Un_absorb Un_empty_right card_Diff_singleton e subst_atoms top_atoms_simp)
        (* you need to tell sledgehammer about formula.set if you want it to find a proof here… *)
      thus "n = card (atoms ((F[ / Min (atoms F - atoms H)])  (F[ / Min (atoms F - atoms H)])) - atoms H)" by simp
    qed
    moreover have "finite (atoms G - atoms H)" " G  H" using Suc(3-) e
      by(auto simp: G_def substitution_lemma)
    ultimately have IH: " G  interpolate G H" " interpolate G H  H" 
        "atoms (interpolate G H)  atoms G  atoms H" using Suc by blast+
    moreover have " F  G" unfolding G_def 
      using subst_true_false by fastforce
    moreover { (* sledgehammer… *)
        assume a1: "atoms (interpolate ((F[/Min (atoms F - atoms H)])  (F[/Min (atoms F - atoms H)])) H)  atoms (F[/Min (atoms F - atoms H)])  atoms (F[/Min (atoms F - atoms H)])  atoms (interpolate ((F[/Min (atoms F - atoms H)])  (F[/Min (atoms F - atoms H)])) H)  atoms H"
        have f2: "atoms ((::'a formula)  ) = atoms "
          by simp
        then have f3: "atoms F - {Min (atoms F - atoms H)} = atoms (F[/Min (atoms F - atoms H)])"
          by (metis (no_types) DiffD1 Top_def Un_empty_right e formula.simps(91) subst_atoms)
        have "atoms (F[/Min (atoms F - atoms H)]) = atoms (F[/Min (atoms F - atoms H)])"
          using f2 by (metis (no_types) DiffD1 Top_def e subst_atoms)
        then have "¬ atoms F  atoms H  atoms (interpolate ((F[/Min (atoms F - atoms H)])  (F[/Min (atoms F - atoms H)])) H)  atoms F"
          using f3 a1 by blast
    } ultimately show ?case
      by (intro conjI; subst interpolate.simps; simp del: interpolate.simps add: Let_def G_def; blast?)
  qed auto
  thus "?t1" "?t2" "?s" by simp_all
qed
text‹So no, the proof is by no means easier this way.
  Admittedly, part of the fuzz is due to @{const Min},
  but replacing atoms with something that returns lists doesn't make it better.›
    

end

Theory SC

section‹Proof Systems›
subsection‹Sequent Calculus›

theory SC
imports Formulas "HOL-Library.Multiset"
begin

abbreviation msins ("_, _" [56,56] 56) where "x,M == add_mset x M"  

text‹We do not formalize the concept of sequents, only that of sequent calculus derivations.›
inductive SCp :: "'a formula multiset  'a formula multiset  bool" ("(_ / _)" [53] 53) where
BotL: " ∈# Γ  ΓΔ" |
Ax: "Atom k ∈# Γ  Atom k ∈# Δ  ΓΔ" |
NotL: "Γ  F,Δ  Not F, Γ  Δ" |
NotR: "F,Γ  Δ  Γ  Not F, Δ" |
AndL: "F,G,Γ  Δ  And F G, Γ  Δ" |
AndR: " Γ  F,Δ; Γ  G,Δ   Γ  And F G, Δ" |
OrL: " F,Γ  Δ; G,Γ  Δ   Or F G, Γ  Δ" |
OrR: "Γ  F,G,Δ  Γ  Or F G, Δ" |
ImpL: " Γ  F,Δ; G,Γ  Δ   Imp F G, Γ  Δ" |
ImpR: "F,Γ  G,Δ  Γ  Imp F G, Δ"

text‹Many of the proofs here are inspired Troelstra and Schwichtenberg~\cite{troelstra2000basic}.›

lemma
  shows BotL_canonical[intro!]: ",ΓΔ"
    and Ax_canonical[intro!]: "Atom k,Γ  Atom k,Δ"
  by (meson SCp.intros union_single_eq_member)+
    

lemma lem1: "x  y  x, M = y,N  x ∈# N  M = y,(N - {#x#})"
  by (metis (no_types, lifting) add_eq_conv_ex add_mset_remove_trivial add_mset_remove_trivial_eq)

lemma lem2: "x  y  x, M = y, N  y ∈# M  N = x, (M - {#y#})"
  using lem1 by fastforce

text‹This is here to deal with a technical problem: the way the simplifier uses @{thm add_mset_commute} is really suboptimal for the unification of SC rules.›
  
lemma sc_insertion_ordering[simp]:
  "NO_MATCH (IJ) H  H,FG,S = FG,H,S"
  "NO_MATCH (IJ) H  NO_MATCH (IJ) H  H,FG,S = FG,H,S"
  "NO_MATCH (IJ) H  NO_MATCH (IJ) H  NO_MATCH (IJ) H  H,FG,S = FG,H,S"
  "NO_MATCH (IJ) H  NO_MATCH (IJ) H  NO_MATCH (IJ) H  NO_MATCH (¬J) H  H,¬G,S = ¬G,H,S"
  "NO_MATCH (IJ) H  NO_MATCH (IJ) H  NO_MATCH (IJ) H  NO_MATCH (¬J) H  NO_MATCH () H  H,,S = ,H,S"
  "NO_MATCH (IJ) H  NO_MATCH (IJ) H  NO_MATCH (IJ) H  NO_MATCH (¬J) H  NO_MATCH () H  NO_MATCH (Atom k) H  H,Atom l,S = Atom l,H,S"
  (* I have decided that ⊥ and atoms should be pulled outwards with the lowest priorities. this may not always be smart. *)
  by simp_all
    
lemma shows
     inR1: "Γ  G, H, Δ  Γ  H, G, Δ"
 and inL1: "G, H, Γ  Δ  H, G, Γ  Δ"
 and inR2: "Γ  F, G, H, Δ  Γ  G, H, F, Δ"
 and inL2: "F, G, H, Γ  Δ  G, H, F, Γ  Δ" by(simp_all add: add_mset_commute)
lemmas SCp_swap_applies[elim!,intro] = inL1 inL2 inR1 inR2

lemma NotL_inv: "Not F, Γ  Δ  Γ  F,Δ"
proof(induction "Not F, Γ" Δ arbitrary: Γ rule: SCp.induct)
  case (NotL Γ' G Δ) thus ?case by(cases "Not F = Not G") (auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2)
qed (auto intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)

lemma AndL_inv: "And F G, Γ  Δ  F,G,Γ  Δ"
proof(induction "And F G, Γ" Δ arbitrary: Γ rule: SCp.induct)
  case (AndL F' G' Γ' Δ) thus ?case 
    by(cases "And F G = And F' G'"; 
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       metis add_mset_commute)
qed (auto intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2 inL2)

lemma OrL_inv: 
  assumes "Or F G, Γ  Δ"
  shows "F,Γ  Δ  G,Γ  Δ"
proof(insert assms, induction "Or F G, Γ" Δ arbitrary: Γ rule: SCp.induct)
  case (OrL F' Γ' Δ G') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       blast)
qed (fastforce intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)+

lemma ImpL_inv: 
  assumes "Imp F G, Γ  Δ"
  shows "Γ  F,Δ  G,Γ  Δ"
proof(insert assms, induction "Imp F G, Γ" Δ arbitrary: Γ rule: SCp.induct)
  case (ImpL Γ' F' Δ G') thus ?case 
    by(cases "Or F G = Or F' G'"; (* oops, I didn't pay attention and used the wrong constructor… doesn't matter! *)
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       blast)
qed (fastforce intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)+
  
lemma ImpR_inv:
  assumes "Γ  Imp F G,Δ"
  shows "F,Γ  G,Δ"
proof(insert assms, induction Γ "Imp F G, Δ" arbitrary: Δ rule: SCp.induct)
  case (ImpR  F' Γ G' Δ') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       blast)
qed (fastforce intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)+

lemma AndR_inv:
shows "Γ  And F G, Δ  Γ  F, Δ  Γ  G, Δ"
proof(induction Γ "And F G, Δ" arbitrary: Δ rule: SCp.induct)
  case (AndR  Γ F' Δ' G') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       blast)
qed (fastforce intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)+

lemma OrR_inv: "Γ  Or F G, Δ  Γ  F,G,Δ"
proof(induction Γ "Or F G, Δ" arbitrary: Δ rule: SCp.induct)
  case (OrR  Γ F' G' Δ') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       metis add_mset_commute)
qed (fastforce intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)+

lemma NotR_inv: "Γ  Not F, Δ  F,Γ  Δ"
proof(induction Γ "Not F, Δ" arbitrary: Δ rule: SCp.induct)
  case (NotR  G Γ Δ') thus ?case 
    by(cases "Not F = Not G"; 
       auto intro!: SCp.intros(3-) dest!: multi_member_split simp: lem1 lem2;
       metis add_mset_commute)
qed (fastforce intro!: SCp.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)+

lemma weakenL: "Γ  Δ  F,Γ  Δ"
  by(induction rule: SCp.induct) 
    (auto intro!: SCp.intros(3-) intro: SCp.intros(1,2))

lemma weakenR: "Γ  Δ  Γ  F,Δ "
  by(induction rule: SCp.induct)
    (auto intro!: SCp.intros(3-) intro: SCp.intros(1,2))

lemma weakenL_set: "Γ  Δ  F + Γ  Δ"
  by(induction F; simp add: weakenL) 
lemma weakenR_set: "Γ  Δ  Γ  F + Δ"
  by(induction F; simp add: weakenR)

lemma extended_Ax: "Γ ∩# Δ  {#}  Γ  Δ"
proof -
  assume "Γ ∩# Δ  {#}"
  then obtain W where "W ∈# Γ" "W ∈# Δ" by force
  then show ?thesis proof(induction W arbitrary: Γ Δ)
    case (Not W)
    from Not.prems obtain Γ' Δ' where [simp]: "Γ = Not W,Γ'" "Δ = Not W,Δ'" by (metis insert_DiffM)
    have "W ∈# W,Γ'" "W ∈# W,Δ'" by simp_all
    from Not.IH[OF this] obtain n where "W, Γ'  W, Δ'" by presburger
    hence "Not W, Γ'  Not W, Δ'" using SCp.intros(3,4) add_mset_commute by metis
    thus "Γ  Δ" by auto
  next
    case (And G H)
    from And.prems obtain Γ' Δ' where [simp]: "Γ = And G H,Γ'" "Δ = And G H,Δ'" by (metis insert_DiffM)
    have "G ∈# G, H, Γ'" "G ∈# G, Δ'" by simp_all
    with And.IH(1) have IH1: "G, H, Γ'  G, Δ'" .
    have "H ∈# G, H, Γ'" "H ∈# H, Δ'" by simp_all
    with And.IH(2) have IH2: "G, H, Γ'  H, Δ'" .
    from IH1 IH2 have "G, H, Γ'  G, Δ'" "G, H, Γ'  H, Δ'" by fast+
    thus "Γ  Δ" using SCp.intros(5,6) by fastforce
  next
    case (Or G H)
    case (Imp G H)
    text‹analogously› (*<*)
  next
    case (Or G H)
    from Or.prems obtain Γ' Δ' where [simp]: "Γ = Or G H,Γ'" "Δ = Or G H,Δ'" by (metis insert_DiffM)
    with Or.IH show ?case using SCp.intros(7,8)[where 'a='a] by fastforce
  next
    case (Imp G H)
    from Imp.prems obtain Γ' Δ' where [simp]: "Γ = Imp G H,Γ'" "Δ = Imp G H,Δ'" by (metis insert_DiffM)
    from Imp.IH have "G, Γ'  G, H, Δ'" "H, G, Γ'  H, Δ'" by simp_all
    thus ?case by(auto intro!: SCp.intros(3-))
  (*>*)
  qed (auto intro: SCp.intros)
qed

lemma Bot_delR: "Γ  Δ  Γ  Δ-{##}"
proof(induction rule: SCp.induct)
  case BotL
  thus ?case by (simp add: SCp.BotL)
next
  case Ax
  thus ?case
    by (metis SCp.Ax diff_union_swap formula.distinct(1) insert_DiffM union_single_eq_member)
next
  case NotL
  thus ?case
    by (metis SCp.NotL diff_single_trivial diff_union_swap2)
next
  case NotR
  thus ?case by(simp add: SCp.NotR)
next
  case AndL
  thus ?case by (simp add: SCp.AndL)
next
  case AndR
  thus ?case
    by (metis SCp.AndR diff_single_trivial diff_union_swap diff_union_swap2 formula.distinct(13))
next
  case OrL
  thus ?case by(simp add: SCp.OrL)
next
  case OrR
  thus ?case
    by (metis SCp.OrR diff_single_trivial diff_union_swap2 formula.distinct(15) insert_iff set_mset_add_mset_insert)
next
  case ImpL
  thus ?case by (metis SCp.ImpL diff_single_trivial diff_union_swap2)
next
  case ImpR
  thus ?case
    by (metis SCp.ImpR diff_single_trivial diff_union_swap diff_union_swap2 formula.distinct(17))
qed
corollary Bot_delR_simp: "Γ  ,Δ = Γ  Δ"
  using Bot_delR weakenR by fastforce

end

Theory SC_Cut

theory SC_Cut
imports SC
begin
  
subsubsection‹Contraction›
  
text‹First, we need contraction:›
lemma contract:
  "(F,F,Γ  Δ  F,Γ  Δ)  (Γ  F,F,Δ  Γ  F,Δ)"
proof(induction F arbitrary: Γ Δ)
  case (Atom k)
  have "Atom k, Atom k, Γ  Δ  Atom k, Γ  Δ"
    by(induction "Atom k, Atom k, Γ" Δ arbitrary: Γ rule: SCp.induct)
      (auto dest!: multi_member_split intro!: SCp.intros(3-) simp add: lem2 lem1 SCp.intros)  
  moreover have "Γ  Atom k, Atom k, Δ  Γ  Atom k, Δ"
    by(induction "Γ" "Atom k, Atom k, Δ" arbitrary: Δ rule: SCp.induct)
      (auto dest!: multi_member_split intro!: SCp.intros(3-) simp add: lem2 lem1 SCp.intros)
  ultimately show ?case by blast
next
  case Bot
  have ", , Γ  Δ  , Γ  Δ" by(blast)
  moreover have "(Γ  , , Δ  Γ  , Δ)"    
    using Bot_delR by fastforce
  ultimately show ?case by blast
next
  case (Not F)
  then show ?case by (meson NotL_inv NotR_inv SCp.NotL SCp.NotR)
next
  case (And F1 F2) then show ?case by(auto intro!: SCp.intros(3-) dest!: AndR_inv AndL_inv) (metis add_mset_commute)
next
  case (Or F1 F2) then show ?case by(auto intro!: SCp.intros(3-) dest!: OrR_inv OrL_inv) (metis add_mset_commute)
next
  (* Okay, so the induction hypothesis is poison for the simplifier. 
     For some reason, this didn't cause trouble for the other two cases, but here, it does. *)
  case (Imp F1 F2) show ?case by(auto dest!: ImpR_inv ImpL_inv intro!: SCp.intros(3-)) (insert Imp.IH; blast)+
qed
corollary
  shows contractL: "F, F, Γ  Δ  F, Γ  Δ"
  and contractR:   "Γ  F, F, Δ  Γ  F, Δ"
  using contract by blast+
    
subsubsection‹Cut›
  
text‹Which cut rule we show is up to us:›
lemma cut_cs_cf:
  assumes context_sharing_Cut: "(A::'a formula) Γ Δ. Γ  A,Δ  A,Γ  Δ  Γ  Δ"
  shows context_free_Cut: "Γ  (A::'a formula),Δ  A,Γ'  Δ'  Γ + Γ'  Δ + Δ'"
  by(intro context_sharing_Cut[of "Γ + Γ'" A "Δ + Δ'"])
    (metis add.commute union_mset_add_mset_left weakenL_set weakenR_set)+
lemma cut_cf_cs:
  assumes context_free_Cut: "(A::'a formula) Γ Γ' Δ Δ'. Γ  A,Δ  A,Γ'  Δ'  Γ + Γ'  Δ + Δ'"
  shows context_sharing_Cut: "Γ  (A::'a formula),Δ  A,Γ  Δ  Γ  Δ"
proof - 
  have contractΓΓ: "Γ+Γ'  Δ  Γ' ⊆# Γ  Γ  Δ" for Γ Γ' Δ
  proof(induction "Γ'" arbitrary: Γ)
    case empty thus ?case using weakenL_set by force
  next
    case (add x Γ' Γ)
    from add.prems(2) have "x ∈# Γ" by (simp add: insert_subset_eq_iff)
    then obtain Γ'' where Γ[simp]: "Γ = x,Γ''" by (meson multi_member_split)
    from add.prems(1) have "x,x,Γ'' + Γ'  Δ" by simp
    with contractL have "x, Γ'' + Γ'  Δ" .
    with add.IH[of Γ] show ?case using Γ  add.prems(2) subset_mset.trans by force
  qed
  have contractΔΔ: "Γ  Δ+Δ'  Δ' ⊆# Δ  Γ  Δ" for Γ Δ Δ'
  proof(induction "Δ'" arbitrary: Δ)
    case empty thus ?case using weakenL_set by force
  next
    case (add x Δ' Δ)
    from add.prems(2) have "x ∈# Δ" by (simp add: insert_subset_eq_iff)
    then obtain Δ'' where Δ[simp]: "Δ = x,Δ''" by (metis multi_member_split)
    from add.prems(1) have "Γ  x,x,Δ'' + Δ'" by simp
    with contractR have "Γ  x, Δ'' + Δ'" .
    with add.IH[of Δ] show ?case using Δ add.prems(2) subset_mset.trans by force
  qed
  show "Γ  A,Δ  A,Γ  Δ  Γ  Δ"
    using context_free_Cut[of Γ A Δ Γ Δ] contractΓΓ contractΔΔ
    by blast
qed
(* since these are the only lemmas that need contraction on sets, I've decided to transfer those in place *)
text‹According to Troelstra and Schwichtenberg~\cite{troelstra2000basic}, the sharing variant is the one we want to prove.›
  
lemma Cut_Atom_pre: "Atom k,Γ  Δ  Γ  Atom k,Δ  Γ  Δ"
proof(induction "Atom k,Γ" "Δ" arbitrary: Γ rule: SCp.induct)
  case BotL
  hence " ∈# Γ" by simp
  thus ?case using SCp.BotL by blast
next
  case (Ax l Δ)
  show ?case proof cases
    assume "l = k"
    with ‹Atom l ∈# Δ obtain Δ' where "Δ = Atom k, Δ'" by (meson multi_member_split)
    with Γ  Atom k, Δ have "Γ  Δ" using contractR by blast
    thus ?thesis by auto
  next
    assume "l  k"
    with ‹Atom l ∈# Atom k, Γ have "Atom l ∈# Γ" by simp
    with ‹Atom l ∈# Δ show ?thesis using SCp.Ax[of l] by blast
  qed
next
  case NotL
  thus ?case by(auto simp: add_eq_conv_ex intro!: SCp.NotL dest!: NotL_inv)
next
  case NotR
  then show ?case by(auto intro!: SCp.NotR dest!: NotR_inv)
next
  case AndL
  thus ?case by(auto simp: add_eq_conv_ex intro!: SCp.AndL dest!: AndL_inv)
next
  case AndR
  then show ?case by(auto intro!: SCp.AndR dest!: AndR_inv)
next
  case OrL
  thus ?case by(auto simp: add_eq_conv_ex intro!: SCp.OrL dest!: OrL_inv)
next
  case OrR
  thus ?case by(auto intro!: SCp.OrR dest!: OrR_inv)
next
  case ImpL
  thus ?case by(auto simp: add_eq_conv_ex intro!: SCp.ImpL dest!: ImpL_inv)
next
  case ImpR
  then show ?case by (auto dest!: ImpR_inv intro!: SCp.ImpR)
qed
  
text‹We can show the admissibility of the cut rule by induction on the cut formula 
(or, if you will, as a procedure that splits the cut into smaller formulas that get cut).
The only mildly complicated case is that of cutting in an @{term "Atom k"}.
It is, contrary to the general case, only mildly complicated, since the cut formula can only appear principal in the axiom rules.›

theorem cut: "Γ  F,Δ  F,Γ  Δ  Γ  Δ"
proof(induction F arbitrary: Γ Δ)
  case Atom thus ?case using Cut_Atom_pre by metis
next
  case Bot thus ?case using Bot_delR by fastforce 
next
  case Not with  NotL_inv NotR_inv show ?case by blast
next
  case And thus ?case by (meson AndL_inv AndR_inv weakenL)
next
  case Or thus ?case by (metis OrL_inv OrR_inv weakenR)
next
  case (Imp F G)
(* an automatic proof:
  thus ?case by (meson ImpL_inv ImpR_inv weakenR)
   a readable one: *)
  from ImpR_inv Γ  F  G, Δ have R: "F, Γ  G, Δ" by blast
  from ImpL_inv F  G, Γ  Δ have L: "Γ  F, Δ" "G, Γ  Δ" by blast+
  from L(1) have "Γ  F, G, Δ" using weakenR add_ac(3) by blast
  with R have "Γ  G, Δ" using Imp.IH(1) by simp
  with L(2) show "Γ  Δ" using Imp.IH(2) by clarsimp
qed
  (* For this proof to work with FOL, I think we would need very special inversion rules.
  For example, for ∀R, we would need that there's a (finite!) multiset of substitutions S, such that
  instead of having ∀x.F,Δ, having {F[s/x] | s ∈ S} + Δ is enough. I don't think that holds,
  but we may be able to cheat ourselves around it… *)
  
corollary cut_cf: " Γ  A, Δ; A, Γ'  Δ'  Γ + Γ'  Δ + Δ'"
  using cut_cs_cf cut by metis

lemma assumes cut: " Γ' Δ' (A::'a formula). Γ'  A, Δ'; A, Γ'  Δ'  Γ'  Δ'"
  shows contraction_admissibility: "F,F,Γ  Δ  (F::'a formula),Γ  Δ"
  by(rule cut[of "F,Γ" F Δ, OF extended_Ax]) simp_all
(* yes, unpublished Chapman p 2/5, second to last paragraph. that's right. we can prove contraction with cut. but what's that good for? *)
  
end

Theory SC_Depth

theory SC_Depth
imports SC
begin
  
text‹
Many textbook arguments about SC use the depth of the derivation tree as basis for inductions.
We had originally thought that this is mandatory for the proof of contraction,
but found out it is not.
It remains unclear to us whether there is any proof on SC that requires an argument using depth.
›
text‹
We keep our formalization of SC with depth for didactic reasons:
we think that arguments about depth do not need much meta-explanation,
but structural induction and rule induction usually need extra explanation
for students unfamiliar with Isabelle/HOL.
They are also a lot harder to execute.
We dare the reader to write down (a few of) the cases for, e.g. AndL_inv'›, by hand.
›

(* Warning: This theory may have name collisions with SC.thy… *)

inductive SCc :: "'a formula multiset  'a formula multiset  nat  bool" ("((_ / _)  _)" [53,53] 53) where
BotL: " ∈# Γ  ΓΔ  Suc n" |
Ax: "Atom k ∈# Γ  Atom k ∈# Δ  ΓΔ  Suc n" |
NotL: "Γ  F,Δ  n  Not F, Γ  Δ  Suc n" |
NotR: "F,Γ  Δ  n  Γ  Not F, Δ  Suc n" |
AndL: "F,G,Γ  Δ  n  And F G, Γ  Δ  Suc n" |
AndR: " Γ  F,Δ  n; Γ  G,Δ  n   Γ  And F G, Δ  Suc n" |
OrL: " F,Γ  Δ  n; G,Γ  Δ  n   Or F G, Γ  Δ  Suc n" |
OrR: "Γ  F,G,Δ  n  Γ  Or F G, Δ  Suc n" |
ImpL: " Γ  F,Δ  n; G,Γ  Δ  n   Imp F G, Γ  Δ  Suc n" |
ImpR: "F,Γ  G,Δ  n  Γ  Imp F G, Δ  Suc n"

lemma
  shows BotL_canonical'[intro!]: ",ΓΔ  Suc n"
    and Ax_canonical'[intro!]: "Atom k,Γ  Atom k,Δ  Suc n"
  by (meson SCc.intros union_single_eq_member)+
    
lemma deeper: "Γ  Δ  n  Γ  Δ  n + m"
  by(induction rule: SCc.induct; insert SCc.intros; auto) 
lemma deeper_suc: "Γ  Δ  n  Γ  Δ  Suc n"
  (* this version is actually required more often. It can be declared as an elim!, but I want to make its usage explicit *)
  thm deeper[unfolded Suc_eq_plus1[symmetric]]
  by(drule deeper[where m=1]) simp
    
text‹The equivalence is obvious.›
theorem SC_SCp_eq:
  fixes Γ Δ :: "'a formula multiset"
  shows "(n. Γ  Δ  n)  Γ  Δ" (is "?c  ?p")
proof
  assume ?c then guess n ..
  thus ?p by(induction rule: SCc.induct; simp add: SCp.intros)
next
  have deeper_max: "Γ  Δ  max m n" "Γ  Δ  max n m" if "Γ  Δ  n" for n m and Γ Δ :: "'a formula multiset"
  proof -
    have "n  m  k. m = n + k" by presburger
    with that[THEN deeper] that
    show "Γ  Δ  max n m" unfolding max_def by clarsimp
    thus "Γ  Δ  max m n" by (simp add: max.commute)
  qed
  assume ?p thus ?c by(induction rule: SCp.induct)
    (insert SCc.intros[where 'a='a] deeper_max; metis)+
qed

(* it makes a difference whether we say Ax is 0 or any: with Ax ↓ 0 we could not prove the deepening rules.
   Also, it is important to allow only atoms in Ax, otherwise the inv-rules are not depth preserving.
  Making Ax/BotL start from ≥1 saves proving the base-cases twice
 *)
lemma no_0_SC[dest!]: "Γ  Δ  0  False"
  by(cases rule: SCc.cases[of Γ Δ 0]) assumption
    

lemma inR1': "Γ  G, H, Δ  n  Γ  H, G, Δ  n" by(simp add: add_mset_commute)
lemma inL1': "G, H, Γ  Δ  n  H, G, Γ  Δ  n" by(simp add: add_mset_commute)
lemma inR2': "Γ  F, G, H, Δ  n  Γ  G, H, F, Δ  n" by(simp add: add_mset_commute)
lemma inL2': "F, G, H, Γ  Δ  n  G, H, F, Γ  Δ  n" by(simp add: add_mset_commute)
lemma inR3': "Γ  F, G, H, Δ  n  Γ  H, F, G, Δ  n" by(simp add: add_mset_commute)
lemma inR4': "Γ  F, G, H, I, Δ  n  Γ  H, I, F, G, Δ  n" by(simp add: add_mset_commute)
lemma inL3': "F, G, H, Γ  Δ  n  H, F, G, Γ  Δ  n" by(simp add: add_mset_commute)
lemma inL4': "F, G, H, I, Γ  Δ  n  H, I, F, G, Γ  Δ  n" by(simp add: add_mset_commute)
lemmas SC_swap_applies[intro,elim!] = inL1' inL2' inL3' inL4' inR1' inR2' inR3' inR4'
  (* these are here because they can be used for more careful reasoning with intro *)

lemma "Atom C  Atom D  Atom E,
       Atom k  Atom C  Atom D, 
       Atom k, {#} 
 {# Atom E #}  Suc (Suc (Suc (Suc (Suc 0))))"
  by(auto intro!: SCc.intros(3-) intro: SCc.intros(1,2))

lemma Bot_delR': "Γ  Δ  n  Γ  Δ-{##}  n"
proof(induction rule: SCc.induct) 
  case BotL thus ?case by(rule SCc.BotL; simp) (* SC.BotL refers to SC.SCp.BotL. Even more interestingly, there used to be a SCc.SC.BotL (which was not reffered to). I'll just leave this here and see how long till someone breaks it. *)
next case (Ax k) thus ?case by(intro SCc.Ax[of k]; simp; metis diff_single_trivial formula.distinct(1) insert_DiffM lem1)
next case NotL thus ?case using SCc.NotL by (metis add_mset_remove_trivial diff_single_trivial diff_union_swap insert_DiffM)
next case NotR thus ?case using SCc.NotR by (metis diff_union_swap formula.distinct(11))
next case AndR thus ?case using SCc.AndR by (metis diff_single_trivial diff_union_swap diff_union_swap2 formula.distinct(13))
next case OrR thus ?case using SCc.OrR by (metis diff_single_trivial diff_union_swap2 formula.distinct(15) insert_iff set_mset_add_mset_insert)
next case ImpL thus ?case using SCc.ImpL by (metis diff_single_trivial diff_union_swap2)
next case ImpR thus ?case using SCc.ImpR by (metis diff_single_trivial diff_union_swap diff_union_swap2 formula.distinct(17))
qed (simp_all add: SCc.intros)
  
lemma NotL_inv': "Not F, Γ  Δ  n  Γ  F,Δ   n"
proof(induction "Not F, Γ" Δ n arbitrary: Γ rule: SCc.induct)
  case (NotL Γ' G Δ n) thus ?case by(cases "Not F = Not G")
    (auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc)
qed (auto intro!: SCc.intros(3-) dest!: multi_member_split simp: SCp.intros lem1 lem2)

lemma AndL_inv': "And F G, Γ  Δ  n  F,G,Γ  Δ  n"
proof(induction "And F G, Γ" Δ n arbitrary: Γ rule: SCc.induct)
  case (AndL F' G' Γ' Δ) thus ?case 
    by(cases "And F G = And F' G'"; 
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       metis add_mset_commute)
qed (auto intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2 inL2')

lemma OrL_inv': 
  assumes "Or F G, Γ  Δ  n"
  shows "F,Γ  Δ  n  G,Γ  Δ  n"
proof(insert assms, induction "Or F G, Γ" Δ n arbitrary: Γ rule: SCc.induct)
  case (OrL F' Γ' Δ n G') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       blast)
qed (fastforce intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2)+

lemma ImpL_inv': 
  assumes "Imp F G, Γ  Δ  n"
  shows "Γ  F,Δ  n  G,Γ  Δ  n"
proof(insert assms, induction "Imp F G, Γ" Δ n arbitrary: Γ rule: SCc.induct)
  case (ImpL Γ' F' Δ n G') thus ?case 
    by(cases "Or F G = Or F' G'"; (* oops, I didn't pay attention and used the wrong constructor… doesn't matter! *)
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       blast)
qed (fastforce intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2)+
  
lemma ImpR_inv':
  assumes "Γ  Imp F G,Δ  n"
  shows "F,Γ  G,Δ  n"
proof(insert assms, induction Γ "Imp F G, Δ" n arbitrary: Δ rule: SCc.induct)
  case (ImpR  F' Γ G' Δ') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       blast)
qed (fastforce intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2)+

lemma AndR_inv':
shows "Γ  And F G, Δ  n  Γ  F, Δ  n  Γ  G, Δ  n"
proof(induction Γ "And F G, Δ" n arbitrary: Δ rule: SCc.induct)
  case (AndR  Γ F' Δ' n G') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       blast)
qed (fastforce intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2)+

lemma OrR_inv': "Γ  Or F G, Δ  n  Γ  F,G,Δ  n"
proof(induction Γ "Or F G, Δ" n arbitrary: Δ rule: SCc.induct)
  case (OrR  Γ F' G' Δ') thus ?case 
    by(cases "Or F G = Or F' G'"; 
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       metis add_mset_commute)
qed (fastforce intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2)+

lemma NotR_inv': "Γ  Not F, Δ  n  F,Γ  Δ  n"
proof(induction Γ "Not F, Δ" n arbitrary: Δ rule: SCc.induct)
  case (NotR  G Γ Δ') thus ?case 
    by(cases "Not F = Not G"; 
       auto intro!: SCc.intros(3-) dest!: multi_member_split simp: lem1 lem2 deeper_suc;
       metis add_mset_commute)
qed (fastforce intro!: SCc.intros(3-) dest!: multi_member_split simp: SCc.intros lem1 lem2)+

lemma weakenL': "Γ  Δ  n  F,Γ  Δ   n"
  by(induction rule: SCc.induct) 
    (auto intro!: SCc.intros(3-) intro: SCc.intros(1,2))

lemma weakenR': "Γ  Δ   n  Γ  F,Δ   n"
  by(induction rule: SCc.induct)
    (auto intro!: SCc.intros(3-) intro: SCc.intros(1,2))

lemma contract':
  "(F,F,Γ  Δ  n  F,Γ  Δ  n)  (Γ  F,F,Δ  n  Γ  F,Δ  n)"
proof(induction n arbitrary: F Γ Δ)
  case (Suc n)
  hence IH: "F, F, Γ  Δ  n  F, Γ  Δ  n" "Γ  F, F, Δ  n  Γ  F, Δ  n" for F :: "'a formula" and Γ Δ by blast+
  show ?case proof(intro conjI allI impI, goal_cases)
    case 1
    let ?ffs = "λΓ. Γ - {# F #} - {# F #}"
    from 1 show ?case proof(insert 1; cases rule: SCc.cases[of "F,F,Γ" Δ "Suc n"])
      case (NotL  Γ' G)
      show ?thesis
      proof(cases)
        assume e: "F = ¬G"
        with NotL have Γ': "Γ' = ¬G, Γ" by simp
        from NotL_inv' NotL(2) have "Γ  G, G, Δ  n" unfolding Γ' .
        with IH(2) have "Γ  G, Δ  n" .
        with SCc.NotL show ?thesis unfolding e .
      next
        assume e: "F  ¬G"
        have ?thesis
          using NotL(2) IH(1)[of F "?ffs Γ'" "G, Δ"] SCc.NotL[of "F, Γ' - {# F #} - {# F #}" G Δ n]
          using e NotL(1) by (metis (no_types, lifting) insert_DiffM lem2)
        from e NotL(1) have Γ: "Γ = ¬ G, ?ffs Γ'" by (meson lem1)
        with NotL(1) have Γ': "F,F,?ffs Γ' = Γ'" by simp
        show ?thesis using NotL(2) IH(1)[of F "?ffs Γ'" "G, Δ"] SCc.NotL[of "F, ?ffs Γ'" G Δ n] F, Γ  Δ  Suc n by blast
      qed
    next
      case (AndL G H Γ') show ?thesis proof cases
        assume e: "F = And G H"
        with AndL(1) have Γ': "Γ' = And G H, Γ" by simp
        have "G  H, G, H, Γ  Δ  n" using AndL(2) unfolding Γ' by auto
        hence "G, H, G, H, Γ  Δ  n" by(rule AndL_inv')
        hence "G, H, Γ  Δ  n" using IH(1) by (metis inL1' inL3')
        thus "F, Γ  Δ  Suc n" using e SCc.AndL by simp
      next
        assume ne: "F  And G H"
        with AndL(1) have Γ: "Γ = And G H, ?ffs Γ'" by (metis (no_types, lifting) diff_diff_add lem2)
        have "F, F, G, H, ?ffs Γ'  Δ  n" using AndL(2) using Γ inL4' local.AndL(1) by auto
        hence "G, H, F, ?ffs Γ'  Δ  n" using IH(1) inL2 by blast
        thus ?thesis using SCc.AndL unfolding Γ using inL1 by blast
      qed
    next
      case (OrL G Γ' H) show ?thesis proof cases
        assume e: "F = Or G H"
        with OrL(1) have Γ': "Γ' = Or G H, Γ" by simp
        have "Or G H, G, Γ  Δ  n" "Or G H, H, Γ  Δ  n" using OrL(2,3) unfolding Γ' by simp_all
        hence "G, G, Γ  Δ  n" "H, H, Γ  Δ  n" using OrL_inv' by blast+
        hence "G, Γ  Δ  n" "H, Γ  Δ  n" using IH(1) by presburger+
        thus "F, Γ  Δ  Suc n" unfolding e using SCc.OrL by blast
      next
        assume ne: "F  Or G H"
        with OrL(1) have Γ: "Γ = Or G H, ?ffs Γ'" by (metis (no_types, lifting) diff_diff_add lem2)
        have "F, F, G, ?ffs Γ'  Δ  n" "F, F, H,?ffs Γ'  Δ  n" using OrL Γ by auto
        hence "G, F, ?ffs Γ'  Δ  n" "H, F, ?ffs Γ'  Δ  n" using IH(1) by(metis add_mset_commute)+
        thus ?thesis using SCc.OrL unfolding Γ by auto
      qed
    next
      case (ImpL Γ' G H) show ?thesis proof cases
        assume e: "F = Imp G H"
        with ImpL(1) have Γ': "Γ' = Imp G H, Γ" by simp
        have "H, Γ  Δ  n" "Γ  G,Δ  n" using IH ImpL_inv' ImpL(2,3) unfolding Γ'
          by (metis add_mset_commute)+
        thus ?thesis unfolding e using SCc.ImpL[where 'a='a] by simp
      next
        assume ne: "F  Imp G H"
        with ImpL(1) have Γ: "Γ = Imp G H, ?ffs Γ'" by (metis (no_types, lifting) diff_diff_add lem2)
        have "F, F, ?ffs Γ'  G, Δ  n" "F, F, H, ?ffs Γ'  Δ  n" using ImpL Γ by auto
        thus ?thesis using SCc.ImpL IH unfolding Γ by (metis inL1')
      qed
    next
      case ImpR thus ?thesis by (simp add: IH(1) SCc.intros(10) add_mset_commute)
    next
      case (NotR G Δ') thus ?thesis using IH(1) by (simp add: SCc.NotR add_mset_commute)
    qed (auto intro: IH SCc.intros(1,2) intro!: SCc.intros(3-10))
  next
    case 2
    let ?ffs = "λΓ. Γ - {# F #} - {# F #}"
    have not_principal[dest]:
      "F  f G H; F, F, Δ = f G H, Δ'  Δ = f G H, ?ffs Δ'  F, F, ?ffs Δ' = Δ'" for f G H Δ' proof(intro conjI, goal_cases)
        case 2
        from 2 have "F ∈# Δ'" by(blast dest: lem1[THEN iffD1])
        then obtain Δ'' where Δ': "Δ' = F,Δ''"  by (metis insert_DiffM)
        with 2(2) have "F, Δ = f G H, Δ''" by(simp add: add_mset_commute)
        hence "F ∈# Δ''" using 2(1) by(blast dest: lem1[THEN iffD1])
        then obtain Δ''' where Δ'': "Δ'' = F,Δ'''" by (metis insert_DiffM)
        show ?case unfolding Δ' Δ'' by simp
        case 1 show ?case using 1(2) unfolding Δ' Δ'' by(simp add: add_mset_commute)
      qed
    have principal[dest]: "F, F, Δ = f G H, Δ'  F = f G H  Δ' = f G H, Δ" for f G H Δ' by simp
    from 2 show ?case proof(cases rule: SCc.cases[of Γ "F,F,Δ" "Suc n"])
      case (ImpR G H Δ') thus ?thesis proof cases
        assume e[simp]: "F = Imp G H"
        with ImpR(1) have Δ'[simp]: "Δ' = Imp G H, Δ" by simp
        have "G, Γ  Imp G H, H, Δ  n" using ImpR(2) by simp
        hence "G, G, Γ  H, H, Δ  n" by(rule ImpR_inv')
        hence "G, Γ  H, Δ  n" using IH by fast
        thus "Γ  F, Δ  Suc n" using SCc.ImpR by simp
      next
        assume a: "F  Imp G H"
        with ImpR(1) have Δ: "Δ = Imp G H, ?ffs Δ'" by (metis (no_types, lifting) diff_diff_add lem2)
        have "G,Γ  F, F, H, ?ffs Δ'  n" using ImpR Δ by fastforce
        thus ?thesis using SCc.ImpR IH unfolding Δ by (metis inR1')
      qed
    next
      case (AndR G Δ' H) thus ?thesis proof(cases "F = And G H")
        case True thus ?thesis using AndR by(auto intro!: SCc.intros(3-) dest!: AndR_inv' intro: IH)
      next
        case False 
        hence e: "Δ = And G H, ?ffs Δ'" using AndR(1) using diff_diff_add lem2 by blast
        hence "G  H, F, F, ?ffs Δ' = G  H, Δ'" using AndR(1) by simp
        hence "Γ  F, F, G, ?ffs Δ'  n" "Γ  F, F, H, ?ffs Δ'  n" using AndR(2,3) using add_left_imp_eq inR2 by fastforce+
        hence "Γ  G, F, ?ffs Δ'  n" "Γ  H, F, ?ffs Δ'  n" using IH(2) by blast+
        thus ?thesis unfolding e by(intro SCc.AndR[THEN inR1'])
      qed
    next
    case (OrR G H Δ') thus ?thesis proof cases
      assume a: "F = Or G H" 
      hence Δ': "Δ' = G  H, Δ" using OrR(1) by(intro principal)
      hence "Γ  G, H, G, H, Δ  n" using inR3'[THEN OrR_inv'] OrR(2) by auto
      hence "Γ  H, G, Δ  n" using IH(2)[of Γ G "H,H,Δ"] IH(2)[of Γ H "G,Δ"]
        unfolding add_ac(3)[of "{#H#}" "{#G#}"] using inR2  by blast
      hence "Γ  G, H, Δ  n" by(elim SC_swap_applies)
    thus ?thesis unfolding a by (simp add: SCc.OrR)
    next
      assume a: "F  Or G H"
      with not_principal have np: "Δ = G  H, ?ffs Δ'  F, F, ?ffs Δ' = Δ'" using OrR(1) .
      with OrR(2) have "Γ  G, H, F, ?ffs Δ'  n" using IH(2) by (metis inR2' inR4')
      hence "Γ  F, G  H, ?ffs Δ'  Suc n" by(intro SCc.OrR[THEN inR1'])
      thus ?thesis using np by simp
    qed
    next
      case (NotR G Δ') thus ?thesis proof(cases "F = Not G") 
        case True 
        with principal NotR(1) have "Δ' = ¬ G, Δ" .
        with NotR_inv' NotR(2) have "G, G, Γ  Δ  n" by blast
        with IH(1) have "G, Γ  Δ  n" .
        thus "Γ  F, Δ  Suc n" unfolding True by(intro SCc.NotR)
      next
        case False 
        with not_principal have np: "Δ = ¬ G, Δ' - (F, {#F#})  F, F, Δ' - (F, {#F#}) = Δ'" using NotR(1) by auto
        hence "G, Γ  F, F, ?ffs Δ'  n" using NotR(2) by simp
        hence "G, Γ  F, ?ffs Δ'  n" by(elim IH(2))
        thus ?thesis using np SCc.NotR inR1 by auto
      qed
    next
      case BotL thus ?thesis by(elim SCc.BotL)
    next
      case (Ax k) thus ?thesis by(intro SCc.Ax[where k=k]) simp_all
    next
      case NotL thus ?thesis by (simp add: SCc.NotL Suc.IH add_mset_commute)
    next
      case AndL thus ?thesis using SCc.AndL Suc.IH by blast
    next
      case OrL thus ?thesis using SCc.OrL Suc.IH by blast
    next
      case ImpL thus ?thesis by (metis SCc.ImpL Suc.IH add_mset_commute)
    qed
  qed
qed blast

(* depth for cut? *)
lemma Cut_Atom_depth: "Atom k,Γ  Δ  n  Γ  Atom k,Δ  m  Γ  Δ  n + m"
proof(induction "Atom k,Γ" "Δ" n arbitrary: Γ m rule: SCc.induct)
  case (BotL Δ)
  hence " ∈# Γ" by simp
  thus ?case using SCc.BotL  by auto
next
  case (Ax l Δ)
  show ?case proof cases
    assume "l = k"
    with ‹Atom l ∈# Δ obtain Δ' where "Δ = Atom k, Δ'" by (meson multi_member_split)
    with Γ  Atom k, Δ  m have "Γ  Δ  m" using contract' by blast
    thus ?thesis by (metis add.commute deeper)
  next
    assume "l  k"
    with ‹Atom l ∈# Atom k, Γ have "Atom l ∈# Γ" by simp
    with ‹Atom l ∈# Δ show ?thesis using SCc.Ax[of l] by simp
  qed
next
  case (NotL Γ F Δ)
  obtain Γ' where Γ: "Γ = Not F, Γ'" by (meson NotL.hyps(3) add_eq_conv_ex formula.simps(9))
  show ?case unfolding Γ
    apply(unfold plus_nat.add_Suc)
    apply(intro SCc.NotL)
    apply(intro NotL.hyps (* IH *))
     subgoal using NotL Γ by (simp add: lem2)
    subgoal using Γ NotL.prems NotL_inv' by blast
  done
next
  case (NotR F Δ)
  then show ?case by(auto intro!: SCc.NotR dest!: NotR_inv')
next
  case (AndL F G Γ Δ)
  obtain Γ' where Γ: "Γ = And F G, Γ'" by (metis AndL.hyps(3) add_eq_conv_diff formula.distinct(5))
  show ?case unfolding Γ
    apply(unfold plus_nat.add_Suc)
    apply(intro SCc.AndL)
    apply(intro AndL.hyps (* IH *))
     subgoal using AndL Γ by (simp add: lem2)
    subgoal using Γ AndL.prems AndL_inv' by blast
  done
next
  case (AndR F Δ G)
  then show ?case
    using AndR_inv' SCc.AndR by (metis add_Suc inR1')
next
  case (OrL F Γ' Δ n G)
  obtain Γ'' where Γ: "Γ = Or F G, Γ''" by (meson OrL.hyps(5) add_eq_conv_ex formula.simps(13))
  have ihm: "F, Γ' = Atom k, F, Γ''" "G, Γ' = Atom k, G, Γ''" using OrL Γ  by (simp_all add: lem2)
  show ?case unfolding Γ
    apply(unfold plus_nat.add_Suc)
    apply(intro SCc.OrL OrL.hyps(2)[OF ihm(1)] OrL.hyps(4)[OF ihm(2)])
     subgoal using Γ OrL.prems OrL_inv' by blast
    subgoal using Γ OrL.prems OrL_inv' by blast
  done
next
  case (OrR F G Δ)
  then show ?case by(auto intro!: SCc.intros(3-) dest!: OrR_inv')
next
  case (ImpL Γ' F Δ n G)
  obtain Γ'' where Γ: "Γ = Imp F G, Γ''" by (metis ImpL.hyps(5) add_eq_conv_ex formula.simps)
  show ?case unfolding Γ
    apply(unfold plus_nat.add_Suc)
    apply(intro SCc.ImpL ImpL.hyps(2) ImpL.hyps(4))
       subgoal using ImpL Γ by (simp add: lem2)
      subgoal using Γ ImpL.prems by(auto dest!: ImpL_inv')
     subgoal using ImpL Γ by (simp add: lem2)
    subgoal using Γ ImpL.prems ImpL_inv' by blast
  done
next
  case (ImpR F G Δ)
  then show ?case by (auto dest!: ImpR_inv' intro!: SCc.ImpR)
qed
primrec cut_bound :: "nat  nat  'a formula  nat" where
  "cut_bound n m (Atom _) = m + n" |
  "cut_bound n m Bot = n" |
  "cut_bound n m (Not F) = cut_bound m n F" |
  "cut_bound n m (And F G) = cut_bound n (cut_bound n m F) G" |
  "cut_bound n m (Or F G) = cut_bound (cut_bound n m F) m G" |
  "cut_bound n m (Imp F G) = cut_bound (cut_bound m n F) m G"
theorem cut_bound: "Γ  F,Δ  n  F,Γ  Δ   m  Γ  Δ  cut_bound n m F"
proof(induction F arbitrary: Γ Δ n m)
  case (Atom k) thus ?case using Cut_Atom_depth by simp fast
next
  case Bot thus ?case using Bot_delR' by fastforce 
next
  case Not from Not.prems show ?case by(auto dest!: NotL_inv' NotR_inv' intro!: Not.IH elim!: weakenL)
next
  case (And F G) from And.prems show ?case by(auto dest!: AndL_inv' AndR_inv' intro!: And.IH elim!: weakenR' weakenL')
next
  case (Or F G) from Or.prems show ?case by(auto dest: OrL_inv' OrR_inv' intro!: Or.IH elim!:  weakenR' weakenL')
next
  case (Imp F G)
  from ImpR_inv' Γ  F  G, Δ  n have R: "F, Γ  G, Δ  n" by blast
  from ImpL_inv' F  G, Γ  Δ  m have L: "Γ  F, Δ  m" "G, Γ  Δ  m" by blast+
  from L(1) have "Γ  F, G, Δ  m" using weakenR' by blast
  from Imp.IH(1)[OF this R] have "Γ  G, Δ  cut_bound m n F" .
  from Imp.IH(2)[OF this L(2)] have "Γ  Δ  cut_bound (cut_bound m n F) m G" .
  thus "Γ  Δ  cut_bound n m (F  G)" by simp
qed
  
context begin
private primrec cut_bound' :: "nat  'a formula  nat" where
  "cut_bound' n (Atom _) = 2*n" |
  "cut_bound' n Bot = n" |
  "cut_bound' n (Not F) = cut_bound' n F" |
  "cut_bound'<