# 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
(⋃F∈af.
(⋃G∈af. 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"
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"
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"
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)"
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)"
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)"
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 {})"

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"

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"

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)"
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 (⋃a∈set (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: "(⋃G∈set (tseytin_tran1 (tseytin_toatom F) F). atoms G) ⊆
atoms F ∪ (⋃I∈set (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) ∪ (⋃x∈set (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) ∪ (⋃x∈set (tseytin_tran1 (tseytin_toatom F) F). atoms x) ⊆
(atoms F ∪ (⋃I∈set (subformulae F). atoms (tseytin_toatom F I)))"
using tseytin_tran1_atoms by blast
have twofin: "finite (atoms F ∪ (⋃I∈set (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 (⋃x∈S. {f x}) ≤ card S" for f S
by(induction S rule: finite_induct; simp add: card_insert_if)
have 3: "card (⋃I∈set (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 (⋃f∈set (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(intro ballI)
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) ⟹ (∀H∈set (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(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
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)"

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(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(rule iffI; unfold Ball_def; elim all_forward)
by (auto simp add: insert_absorb split: formula.splits)

definition "subset_closed C ≡ (∀S ∈ C. ∀s⊆S. 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. ∃S∈C. 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. ∀s⊆S. finite s ⟶ s ∈ C}" if si: "⋀s. ⟦s⊆S; 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. ∀s⊆S. finite s ⟶ s ∈ C} ∨ H ▹ S ∈ C ∪ {S. ∀s⊆S. finite s ⟶ s ∈ C}"
if si: "⋀s. s⊆S ⟹ 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;
∀s⊆S2. finite s ⟶ s ∈ C; h2 F2 G2 ∈ S2; False⟧
⟹ f2 F2 ▹ S2 ∈ C ∪ {S. ∀s⊆S. finite s ⟶ s ∈ C} ∨ g2 G2 ▹ S2 ∈ C ∪ {S. ∀s⊆S. 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
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
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: "∀x∈s. 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 "∃x∈s. ¬ 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
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
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
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 "∀F∈S. (λ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: "∀s⊆S. finite s ⟶ (∃𝒜. ∀F∈s. 𝒜 ⊨ 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⟧ ⟹ ∃𝒜. ∀F∈s. 𝒜 ⊨ 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: "∀H∈h 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 "∀H∈h 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; ∀𝒜. ∃x∈s1. ¬ 𝒜 ⊨ x; finite s2; ∀𝒜. ∃x∈s2. ¬ 𝒜 ⊨ 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(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#})"

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 (I❙→J) H ⟹ H,F❙→G,S = F❙→G,H,S"
"NO_MATCH (I❙→J) H ⟹ NO_MATCH (I❙∨J) H ⟹ H,F❙∨G,S = F❙∨G,H,S"
"NO_MATCH (I❙→J) H ⟹ NO_MATCH (I❙∨J) H ⟹ NO_MATCH (I❙∧J) H ⟹ H,F❙∧G,S = F❙∧G,H,S"
"NO_MATCH (I❙→J) H ⟹ NO_MATCH (I❙∨J) H ⟹ NO_MATCH (I❙∧J) H ⟹ NO_MATCH (❙¬J) H ⟹ H,❙¬G,S = ❙¬G,H,S"
"NO_MATCH (I❙→J) H ⟹ NO_MATCH (I❙∨J) H ⟹ NO_MATCH (I❙∧J) H ⟹ NO_MATCH (❙¬J) H ⟹ NO_MATCH (⊥) H ⟹ H,⊥,S = ⊥,H,S"
"NO_MATCH (I❙→J) H ⟹ NO_MATCH (I❙∨J) H ⟹ NO_MATCH (I❙∧J) 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;
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;
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;
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 + Γ ⇒ Δ"
lemma weakenR_set: "Γ ⇒ Δ ⟹ Γ ⇒ F + Δ"

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
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
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 "Δ + Δ'"])
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
then obtain Γ'' where Γ[simp]: "Γ = x,Γ''" by (meson multi_member_split)
from add.prems(1) have "x,x,Γ'' + Γ' ⇒ Δ" by simp
with contractL have "x, Γ'' + Γ' ⇒ Δ" .
qed
have contractΔΔ: "Γ ⇒ Δ+Δ' ⟹ Δ' ⊆# Δ ⟹ Γ ⇒ Δ" for Γ Δ Δ'
proof(induction "Δ'" arbitrary: Δ)
case empty thus ?case using weakenL_set by force
next
then obtain Δ'' where Δ[simp]: "Δ = x,Δ''" by (metis multi_member_split)
from add.prems(1) have "Γ ⇒ x,x,Δ'' + Δ'" by simp
with contractR have "Γ ⇒ x, Δ'' + Δ'" .
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)
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))

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;
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;
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;
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 Γ'
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
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
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(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(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(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(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'<