Theory FOL_Fitting

(*  Author:     Stefan Berghofer, TU Muenchen, 2003
    Author: Asta Halkjær From, DTU Compute, 2019
    Thanks to John Bruntse Larsen, Anders Schlichtkrull & Jørgen Villadsen
    See also the Natural Deduction Assistant: https://nadea.compute.dtu.dk/
*)

section ‹First-Order Logic According to Fitting›

theory FOL_Fitting
  imports "HOL-Library.Countable"
begin

section ‹Miscellaneous Utilities›

text ‹Some facts about (in)finite sets›

theorem set_inter_compl_diff [simp]: ‹- A ∩ B = B - A› by blast

section ‹Terms and formulae›

text ‹
\label{sec:terms}
The datatypes of terms and formulae in {\em de Bruijn notation}
are defined as follows:
›

datatype 'a "term"
  = Var nat
  | App 'a ‹'a term list›

datatype ('a, 'b) form
  = FF
  | TT
  | Pred 'b ‹'a term list›
  | And ‹('a, 'b) form› ‹('a, 'b) form›
  | Or ‹('a, 'b) form› ‹('a, 'b) form›
  | Impl ‹('a, 'b) form› ‹('a, 'b) form›
  | Neg ‹('a, 'b) form›
  | Forall ‹('a, 'b) form›
  | Exists ‹('a, 'b) form›

text ‹
We use ‹'a› and ‹'b› to denote the type of
{\em function symbols} and {\em predicate symbols}, respectively.
In applications ‹App a ts› and predicates
‹Pred a ts›, the length of ‹ts› is considered
to be a part of the function or predicate name, so ‹App a [t]›
and ‹App a [t,u]› refer to different functions.

The size of a formula is used later for wellfounded induction. The
default implementation provided by the datatype package is not quite
what we need, so here is an alternative version:
›

primrec size_form :: ‹('a, 'b) form ⇒ nat› where
  ‹size_form FF = 0›
| ‹size_form TT = 0›
| ‹size_form (Pred _ _) = 0›
| ‹size_form (And p q) = size_form p + size_form q + 1›
| ‹size_form (Or p q) = size_form p + size_form q + 1›
| ‹size_form (Impl p q) = size_form p + size_form q + 1›
| ‹size_form (Neg p) = size_form p + 1›
| ‹size_form (Forall p) = size_form p + 1›
| ‹size_form (Exists p) = size_form p + 1›

subsection ‹Closed terms and formulae›

text ‹
Many of the results proved in the following sections are restricted
to closed terms and formulae. We call a term or formula {\em closed at
level ‹i›}, if it only contains ``loose'' bound variables with
indices smaller than ‹i›.
›

primrec
  closedt :: ‹nat ⇒ 'a term ⇒ bool› and
  closedts :: ‹nat ⇒ 'a term list ⇒ bool› where
  ‹closedt m (Var n) = (n < m)›
| ‹closedt m (App a ts) = closedts m ts›
| ‹closedts m [] = True›
| ‹closedts m (t # ts) = (closedt m t ∧ closedts m ts)›

primrec closed :: ‹nat ⇒ ('a, 'b) form ⇒ bool› where
  ‹closed m FF = True›
| ‹closed m TT = True›
| ‹closed m (Pred b ts) = closedts m ts›
| ‹closed m (And p q) = (closed m p ∧ closed m q)›
| ‹closed m (Or p q) = (closed m p ∧ closed m q)›
| ‹closed m (Impl p q) = (closed m p ∧ closed m q)›
| ‹closed m (Neg p) = closed m p›
| ‹closed m (Forall p) = closed (Suc m) p›
| ‹closed m (Exists p) = closed (Suc m) p›

theorem closedt_mono: assumes le: ‹i ≤ j›
  shows ‹closedt i (t::'a term) ⟹ closedt j t›
    and ‹closedts i (ts::'a term list) ⟹ closedts j ts›
  using le by (induct t and ts rule: closedt.induct closedts.induct) simp_all

theorem closed_mono: assumes le: ‹i ≤ j›
  shows ‹closed i p ⟹ closed j p›
  using le
proof (induct p arbitrary: i j)
  case (Pred i l)
  then show ?case
    using closedt_mono by simp
qed auto

subsection ‹Substitution›

text ‹
We now define substitution functions for terms and formulae. When performing
substitutions under quantifiers, we need to {\em lift} the terms to be substituted
for variables, in order for the ``loose'' bound variables to point to the right
position.
›

primrec
  substt :: ‹'a term ⇒ 'a term ⇒ nat ⇒ 'a term› (‹_[_'/_]› [300, 0, 0] 300) and
  substts :: ‹'a term list ⇒ 'a term ⇒ nat ⇒ 'a term list› (‹_[_'/_]› [300, 0, 0] 300) where
  ‹(Var i)[s/k] = (if k < i then Var (i - 1) else if i = k then s else Var i)›
| ‹(App a ts)[s/k] = App a (ts[s/k])›
| ‹[][s/k] = []›
| ‹(t # ts)[s/k] = t[s/k] # ts[s/k]›

primrec
  liftt :: ‹'a term ⇒ 'a term› and
  liftts :: ‹'a term list ⇒ 'a term list› where
  ‹liftt (Var i) = Var (Suc i)›
| ‹liftt (App a ts) = App a (liftts ts)›
| ‹liftts [] = []›
| ‹liftts (t # ts) = liftt t # liftts ts›

primrec subst :: ‹('a, 'b) form ⇒ 'a term ⇒ nat ⇒ ('a, 'b) form›
  (‹_[_'/_]› [300, 0, 0] 300) where
  ‹FF[s/k] = FF›
| ‹TT[s/k] = TT›
| ‹(Pred b ts)[s/k] = Pred b (ts[s/k])›
| ‹(And p q)[s/k] = And (p[s/k]) (q[s/k])›
| ‹(Or p q)[s/k] = Or (p[s/k]) (q[s/k])›
| ‹(Impl p q)[s/k] = Impl (p[s/k]) (q[s/k])›
| ‹(Neg p)[s/k] = Neg (p[s/k])›
| ‹(Forall p)[s/k] = Forall (p[liftt s/Suc k])›
| ‹(Exists p)[s/k] = Exists (p[liftt s/Suc k])›

theorem lift_closed [simp]:
  ‹closedt 0 (t::'a term) ⟹ closedt 0 (liftt t)›
  ‹closedts 0 (ts::'a term list) ⟹ closedts 0 (liftts ts)›
  by (induct t and ts rule: closedt.induct closedts.induct) simp_all

theorem subst_closedt [simp]:
  assumes u: ‹closedt 0 u›
  shows ‹closedt (Suc i) t ⟹ closedt i (t[u/i])›
    and ‹closedts (Suc i) ts ⟹ closedts i (ts[u/i])›
  using u closedt_mono(1)
  by (induct t and ts rule: closedt.induct closedts.induct) auto

theorem subst_closed [simp]:
  ‹closedt 0 t ⟹ closed (Suc i) p ⟹ closed i (p[t/i])›
  by (induct p arbitrary: i t) simp_all

theorem subst_size_form [simp]: ‹size_form (subst p t i) = size_form p›
  by (induct p arbitrary: i t) simp_all

subsection ‹Parameters›

text ‹
The introduction rule ‹ForallI› for the universal quantifier,
as well as the elimination rule ‹ExistsE› for the existential
quantifier introduced in \secref{sec:proof-calculus} require the
quantified variable to be replaced by a ``fresh'' parameter. Fitting's
solution is to use a new nullary function symbol for this purpose.
To express that a function symbol is ``fresh'', we introduce functions
for collecting all function symbols occurring in a term or formula.
›

primrec
  paramst :: ‹'a term ⇒ 'a set› and
  paramsts :: ‹'a term list ⇒ 'a set› where
  ‹paramst (Var n) = {}›
| ‹paramst (App a ts) = {a} ∪ paramsts ts›
| ‹paramsts [] = {}›
| ‹paramsts (t # ts) = (paramst t ∪ paramsts ts)›

primrec params :: ‹('a, 'b) form ⇒ 'a set› where
  ‹params FF = {}›
| ‹params TT = {}›
| ‹params (Pred b ts) = paramsts ts›
| ‹params (And p q) = params p ∪ params q›
| ‹params (Or p q) = params p ∪ params q›
| ‹params (Impl p q) = params p ∪ params q›
| ‹params (Neg p) = params p›
| ‹params (Forall p) = params p›
| ‹params (Exists p) = params p›

text‹
We also define parameter substitution functions on terms and formulae
that apply a function ‹f› to all function symbols.
›

primrec
  psubstt :: ‹('a ⇒ 'c) ⇒ 'a term ⇒ 'c term› and
  psubstts :: ‹('a ⇒ 'c) ⇒ 'a term list ⇒ 'c term list› where
  ‹psubstt f (Var i) = Var i›
| ‹psubstt f (App x ts) = App (f x) (psubstts f ts)›
| ‹psubstts f [] = []›
| ‹psubstts f (t # ts) = psubstt f t # psubstts f ts›

primrec psubst :: ‹('a ⇒ 'c) ⇒ ('a, 'b) form ⇒ ('c, 'b) form› where
  ‹psubst f FF = FF›
| ‹psubst f TT = TT›
| ‹psubst f (Pred b ts) = Pred b (psubstts f ts)›
| ‹psubst f (And p q) = And (psubst f p) (psubst f q)›
| ‹psubst f (Or p q) = Or (psubst f p) (psubst f q)›
| ‹psubst f (Impl p q) = Impl (psubst f p) (psubst f q)›
| ‹psubst f (Neg p) = Neg (psubst f p)›
| ‹psubst f (Forall p) = Forall (psubst f p)›
| ‹psubst f (Exists p) = Exists (psubst f p)›

theorem psubstt_closed [simp]:
  ‹closedt i (psubstt f t) = closedt i t›
  ‹closedts i (psubstts f ts) = closedts i ts›
  by (induct t and ts rule: closedt.induct closedts.induct) simp_all

theorem psubst_closed [simp]:
  ‹closed i (psubst f p) = closed i p›
  by (induct p arbitrary: i) simp_all

theorem psubstt_subst [simp]:
  ‹psubstt f (substt t u i) = substt (psubstt f t) (psubstt f u) i›
  ‹psubstts f (substts ts u i) = substts (psubstts f ts) (psubstt f u) i›
  by (induct t and ts rule: psubstt.induct psubstts.induct) simp_all

theorem psubstt_lift [simp]:
  ‹psubstt f (liftt t) = liftt (psubstt f t)›
  ‹psubstts f (liftts ts) = liftts (psubstts f ts)›
  by (induct t and ts rule: psubstt.induct psubstts.induct) simp_all

theorem psubst_subst [simp]:
  ‹psubst f (subst P t i) = subst (psubst f P) (psubstt f t) i›
  by (induct P arbitrary: i t) simp_all

theorem psubstt_upd [simp]:
  ‹x ∉ paramst (t::'a term) ⟹ psubstt (f(x := y)) t = psubstt f t›
  ‹x ∉ paramsts (ts::'a term list) ⟹ psubstts (f(x := y)) ts = psubstts f ts›
  by (induct t and ts rule: psubstt.induct psubstts.induct) (auto split: sum.split)

theorem psubst_upd [simp]: ‹x ∉ params P ⟹ psubst (f(x := y)) P = psubst f P›
  by (induct P) (simp_all del: fun_upd_apply)

theorem psubstt_id:
  fixes t :: ‹'a term› and ts :: ‹'a term list›
  shows ‹psubstt id t = t› and ‹psubstts (λx. x) ts = ts›
  by (induct t and ts rule: psubstt.induct psubstts.induct) simp_all

theorem psubst_id [simp]: ‹psubst id = id›
proof
  fix p :: ‹('a, 'b) form›
  show ‹psubst id p = id p›
    by (induct p) (simp_all add: psubstt_id)
qed

theorem psubstt_image [simp]:
  ‹paramst (psubstt f t) = f ` paramst t›
  ‹paramsts (psubstts f ts) = f ` paramsts ts›
  by (induct t and ts rule: paramst.induct paramsts.induct) (simp_all add: image_Un)

theorem psubst_image [simp]: ‹params (psubst f p) = f ` params p›
  by (induct p) (simp_all add: image_Un)

section ‹Semantics›

text ‹
\label{sec:semantics}
In this section, we define evaluation functions for terms and formulae.
Evaluation is performed relative to an environment mapping indices of variables
to values. We also introduce a function, denoted by ‹e⟨i:a⟩›, for inserting
a value ‹a› at position ‹i› into the environment. All values of variables
with indices less than ‹i› are left untouched by this operation, whereas the
values of variables with indices greater or equal than ‹i› are shifted one
position up.
›

definition shift :: ‹(nat ⇒ 'a) ⇒ nat ⇒ 'a ⇒ nat ⇒ 'a› (‹_⟨_:_⟩› [90, 0, 0] 91) where
  ‹e⟨i:a⟩ = (λj. if j < i then e j else if j = i then a else e (j - 1))›

lemma shift_eq [simp]: ‹i = j ⟹ (e⟨i:T⟩) j = T›
  by (simp add: shift_def)

lemma shift_gt [simp]: ‹j < i ⟹ (e⟨i:T⟩) j = e j›
  by (simp add: shift_def)

lemma shift_lt [simp]: ‹i < j ⟹ (e⟨i:T⟩) j = e (j - 1)›
  by (simp add: shift_def)

lemma shift_commute [simp]: ‹e⟨i:U⟩⟨0:T⟩ = e⟨0:T⟩⟨Suc i:U⟩›
proof
  fix x
  show ‹(e⟨i:U⟩⟨0:T⟩) x = (e⟨0:T⟩⟨Suc i:U⟩) x›
    by (cases x) (simp_all add: shift_def)
qed

primrec
  evalt :: ‹(nat ⇒ 'c) ⇒ ('a ⇒ 'c list ⇒ 'c) ⇒ 'a term ⇒ 'c› and
  evalts :: ‹(nat ⇒ 'c) ⇒ ('a ⇒ 'c list ⇒ 'c) ⇒ 'a term list ⇒ 'c list› where
  ‹evalt e f (Var n) = e n›
| ‹evalt e f (App a ts) = f a (evalts e f ts)›
| ‹evalts e f [] = []›
| ‹evalts e f (t # ts) = evalt e f t # evalts e f ts›

primrec eval :: ‹(nat ⇒ 'c) ⇒ ('a ⇒ 'c list ⇒ 'c) ⇒
  ('b ⇒ 'c list ⇒ bool) ⇒ ('a, 'b) form ⇒ bool› where
  ‹eval e f g FF = False›
| ‹eval e f g TT = True›
| ‹eval e f g (Pred a ts) = g a (evalts e f ts)›
| ‹eval e f g (And p q) = ((eval e f g p) ∧ (eval e f g q))›
| ‹eval e f g (Or p q) = ((eval e f g p) ∨ (eval e f g q))›
| ‹eval e f g (Impl p q) = ((eval e f g p) ⟶ (eval e f g q))›
| ‹eval e f g (Neg p) = (¬ (eval e f g p))›
| ‹eval e f g (Forall p) = (∀z. eval (e⟨0:z⟩) f g p)›
| ‹eval e f g (Exists p) = (∃z. eval (e⟨0:z⟩) f g p)›

text ‹
We write ‹e,f,g,ps ⊨ p› to mean that the formula ‹p› is a
semantic consequence of the list of formulae ‹ps› with respect to an
environment ‹e› and interpretations ‹f› and ‹g› for
function and predicate symbols, respectively.
›

definition model :: ‹(nat ⇒ 'c) ⇒ ('a ⇒ 'c list ⇒ 'c) ⇒ ('b ⇒ 'c list ⇒ bool) ⇒
    ('a, 'b) form list ⇒ ('a, 'b) form ⇒ bool› (‹_,_,_,_ ⊨ _› [50,50] 50) where
  ‹(e,f,g,ps ⊨ p) = (list_all (eval e f g) ps ⟶ eval e f g p)›

text ‹
The following substitution lemmas relate substitution and evaluation functions:
›

theorem subst_lemma' [simp]:
  ‹evalt e f (substt t u i) = evalt (e⟨i:evalt e f u⟩) f t›
  ‹evalts e f (substts ts u i) = evalts (e⟨i:evalt e f u⟩) f ts›
  by (induct t and ts rule: substt.induct substts.induct) simp_all

theorem lift_lemma [simp]:
  ‹evalt (e⟨0:z⟩) f (liftt t) = evalt e f t›
  ‹evalts (e⟨0:z⟩) f (liftts ts) = evalts e f ts›
  by (induct t and ts rule: liftt.induct liftts.induct) simp_all

theorem subst_lemma [simp]:
  ‹eval e f g (subst a t i) = eval (e⟨i:evalt e f t⟩) f g a›
  by (induct a arbitrary: e i t) simp_all

theorem upd_lemma' [simp]:
  ‹n ∉ paramst t ⟹ evalt e (f(n := x)) t = evalt e f t›
  ‹n ∉ paramsts ts ⟹ evalts e (f(n := x)) ts = evalts e f ts›
  by (induct t and ts rule: paramst.induct paramsts.induct) auto

theorem upd_lemma [simp]:
  ‹n ∉ params p ⟹ eval e (f(n := x)) g p = eval e f g p›
  by (induct p arbitrary: e) simp_all

theorem list_upd_lemma [simp]: ‹list_all (λp. n ∉ params p) G ⟹
  list_all (eval e (f(n := x)) g) G = list_all (eval e f g) G›
  by (induct G) simp_all

theorem psubst_eval' [simp]:
  ‹evalt e f (psubstt h t) = evalt e (λp. f (h p)) t›
  ‹evalts e f (psubstts h ts) = evalts e (λp. f (h p)) ts›
  by (induct t and ts rule: psubstt.induct psubstts.induct) simp_all

theorem psubst_eval:
  ‹eval e f g (psubst h p) = eval e (λp. f (h p)) g p›
  by (induct p arbitrary: e) simp_all

text ‹
In order to test the evaluation function defined above, we apply it
to an example:
›

theorem ex_all_commute_eval:
  ‹eval e f g (Impl (Exists (Forall (Pred p [Var 1, Var 0])))
    (Forall (Exists (Pred p [Var 0, Var 1]))))›
  apply simp
  txt ‹
Simplification yields the following proof state:
@{subgoals [display]}
This is easily proved using intuitionistic logic:
›
  by iprover

section ‹Proof calculus›

text ‹
\label{sec:proof-calculus}
We now introduce a natural deduction proof calculus for first order logic.
The derivability judgement ‹G ⊢ a› is defined as an inductive predicate.
›

inductive deriv :: ‹('a, 'b) form list ⇒ ('a, 'b) form ⇒ bool› (‹_ ⊢ _› [50,50] 50) where
  Assum: ‹a ∈ set G ⟹ G ⊢ a›
| TTI: ‹G ⊢ TT›
| FFE: ‹G ⊢ FF ⟹ G ⊢ a›
| NegI: ‹a # G ⊢ FF ⟹ G ⊢ Neg a›
| NegE: ‹G ⊢ Neg a ⟹ G ⊢ a ⟹ G ⊢ FF›
| Class: ‹Neg a # G ⊢ FF ⟹ G ⊢ a›
| AndI: ‹G ⊢ a ⟹ G ⊢ b ⟹ G ⊢ And a b›
| AndE1: ‹G ⊢ And a b ⟹ G ⊢ a›
| AndE2: ‹G ⊢ And a b ⟹ G ⊢ b›
| OrI1: ‹G ⊢ a ⟹ G ⊢ Or a b›
| OrI2: ‹G ⊢ b ⟹ G ⊢ Or a b›
| OrE: ‹G ⊢ Or a b ⟹ a # G ⊢ c ⟹ b # G ⊢ c ⟹ G ⊢ c›
| ImplI: ‹a # G ⊢ b ⟹ G ⊢ Impl a b›
| ImplE: ‹G ⊢ Impl a b ⟹ G ⊢ a ⟹ G ⊢ b›
| ForallI: ‹G ⊢ a[App n []/0] ⟹ list_all (λp. n ∉ params p) G ⟹
    n ∉ params a ⟹ G ⊢ Forall a›
| ForallE: ‹G ⊢ Forall a ⟹ G ⊢ a[t/0]›
| ExistsI: ‹G ⊢ a[t/0] ⟹ G ⊢ Exists a›
| ExistsE: ‹G ⊢ Exists a ⟹ a[App n []/0] # G ⊢ b ⟹
    list_all (λp. n ∉ params p) G ⟹ n ∉ params a ⟹ n ∉ params b ⟹ G ⊢ b›

text ‹
The following derived inference rules are sometimes useful in applications.
›

theorem Class': ‹Neg A # G ⊢ A ⟹ G ⊢ A›
  by (rule Class, rule NegE, rule Assum) (simp, iprover)

theorem cut: ‹G ⊢ A ⟹ A # G ⊢ B ⟹ G ⊢ B›
  by (rule ImplE, rule ImplI)

theorem ForallE': ‹G ⊢ Forall a ⟹ subst a t 0 # G ⊢ B ⟹ G ⊢ B›
  by (rule cut, rule ForallE)

text ‹
As an example, we show that the excluded middle, a commutation property
for existential and universal quantifiers, the drinker principle, as well
as Peirce's law are derivable in the calculus given above.
›

theorem tnd: ‹[] ⊢ Or (Pred p []) (Neg (Pred p []))› (is ‹_ ⊢ ?or›)
proof -
  have ‹[Neg ?or] ⊢ Neg ?or›
    by (simp add: Assum)
  moreover { have ‹[Pred p [], Neg ?or] ⊢ Neg ?or›
      by (simp add: Assum)
    moreover have ‹[Pred p [], Neg ?or] ⊢ Pred p []›
      by (simp add: Assum)
    then have ‹[Pred p [], Neg ?or] ⊢ ?or›
      by (rule OrI1)
    ultimately have ‹[Pred p [], Neg ?or] ⊢ FF›
      by (rule NegE)
    then have ‹[Neg ?or] ⊢ Neg (Pred p [])›
      by (rule NegI)
    then have ‹[Neg ?or] ⊢ ?or›
      by (rule OrI2) }
  ultimately have ‹[Neg ?or] ⊢ FF›
    by (rule NegE)
  then show ?thesis
    by (rule Class)
qed

theorem ex_all_commute:
  ‹([]::(nat, 'b) form list) ⊢ Impl (Exists (Forall (Pred p [Var 1, Var 0])))
     (Forall (Exists (Pred p [Var 0, Var 1])))›
proof -
  let ?forall = ‹Forall (Pred p [Var 1, Var 0]) :: (nat, 'b) form›

  have ‹[Exists ?forall] ⊢ Exists ?forall›
    by (simp add: Assum)
  moreover { have ‹[?forall[App 1 []/0], Exists ?forall] ⊢ Forall (Pred p [App 1 [], Var 0])›
      by (simp add: Assum)
    moreover have ‹[Pred p [App 1 [], Var 0][App 0 []/0], ?forall[App 1 []/0],
      Exists ?forall] ⊢ Pred p [Var 0, App 0 []][App 1 []/0]›
      by (simp add: Assum)
    ultimately have ‹[?forall[App 1 []/0], Exists ?forall] ⊢ (Pred p [Var 0, App 0 []])[App 1 []/0]›
      by (rule ForallE') }
  then have ‹[?forall[App 1 []/0], Exists ?forall] ⊢ Exists (Pred p [Var 0, App 0 []])›
    by (rule ExistsI)
  moreover have ‹list_all (λp. 1 ∉ params p) [Exists ?forall]›
    by simp
  moreover have ‹1 ∉ params ?forall›
    by simp
  moreover have ‹1 ∉ params (Exists (Pred p [Var 0, App (0 :: nat) []]))›
    by simp
  ultimately have ‹[Exists ?forall] ⊢ Exists (Pred p [Var 0, App 0 []])›
    by (rule ExistsE)
  then have ‹[Exists ?forall] ⊢ (Exists (Pred p [Var 0, Var 1]))[App 0 []/0]›
    by simp
  moreover have ‹list_all (λp. 0 ∉ params p) [Exists ?forall]›
    by simp
  moreover have ‹0 ∉ params (Exists (Pred p [Var 0, Var 1]))›
    by simp
  ultimately have ‹[Exists ?forall] ⊢ Forall (Exists (Pred p [Var 0, Var 1]))›
    by (rule ForallI)
  then show ?thesis
    by (rule ImplI)
qed

theorem drinker: ‹([]::(nat, 'b) form list) ⊢
  Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))›
proof -
  let ?impl = ‹(Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))) :: (nat, 'b) form›
  let ?G' = ‹[Pred P [Var 0], Neg (Exists ?impl)]›
  let ?G = ‹Neg (Pred P [App 0 []]) # ?G'›

  have ‹?G ⊢ Neg (Exists ?impl)›
    by (simp add: Assum)
  moreover have ‹Pred P [App 0 []] # ?G ⊢ Neg (Pred P [App 0 []])›
    and ‹Pred P [App 0 []] # ?G ⊢ Pred P [App 0 []]›
    by (simp_all add: Assum)
  then have ‹Pred P [App 0 []] # ?G ⊢ FF›
    by (rule NegE)
  then have ‹Pred P [App 0 []] # ?G ⊢ Forall (Pred P [Var 0])›
    by (rule FFE)
  then have ‹?G ⊢ ?impl[App 0 []/0]›
    using ImplI by simp
  then have ‹?G ⊢ Exists ?impl›
    by (rule ExistsI)
  ultimately have ‹?G ⊢ FF›
    by (rule NegE)
  then have ‹?G' ⊢ Pred P [Var 0][App 0 []/0]›
    using Class by simp
  moreover have ‹list_all (λp. (0 :: nat) ∉ params p) ?G'›
    by simp
  moreover have ‹(0 :: nat) ∉ params (Pred P [Var 0])›
    by simp
  ultimately have ‹?G' ⊢ Forall (Pred P [Var 0])›
    by (rule ForallI)
  then have ‹[Neg (Exists ?impl)] ⊢ ?impl[Var 0/0]›
    using ImplI by simp
  then have ‹[Neg (Exists ?impl)] ⊢ Exists ?impl›
    by (rule ExistsI)
  then show ?thesis
    by (rule Class')
qed

theorem peirce:
  ‹[] ⊢ Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])›
  (is ‹[] ⊢ Impl ?PQP (Pred P [])›)
proof -
  let ?PQPP = ‹Impl ?PQP (Pred P [])›

  have ‹[?PQP, Neg ?PQPP] ⊢ ?PQP›
    by (simp add: Assum)
  moreover { have ‹[Pred P [], ?PQP, Neg ?PQPP] ⊢ Neg ?PQPP›
      by (simp add: Assum)
    moreover have ‹[?PQP, Pred P [], ?PQP, Neg ?PQPP] ⊢ Pred P []›
      by (simp add: Assum)
    then have ‹[Pred P [], ?PQP, Neg ?PQPP] ⊢ ?PQPP›
      by (rule ImplI)
    ultimately have ‹[Pred P [], ?PQP, Neg ?PQPP] ⊢ FF›
      by (rule NegE) }
  then have ‹[Pred P [], ?PQP, Neg ?PQPP] ⊢ Pred Q []›
    by (rule FFE)
  then have ‹[?PQP, Neg ?PQPP] ⊢ Impl (Pred P []) (Pred Q [])›
    by (rule ImplI)
  ultimately have ‹[?PQP, Neg ?PQPP] ⊢ Pred P []›
    by (rule ImplE)
  then have ‹[Neg ?PQPP] ⊢ ?PQPP›
    by (rule ImplI)
  then show ‹[] ⊢ ?PQPP›
    by (rule Class')
qed

section ‹Correctness›

text ‹
The correctness of the proof calculus introduced in \secref{sec:proof-calculus}
can now be proved by induction on the derivation of @{term ‹G ⊢ p›}, using the
substitution rules proved in \secref{sec:semantics}.
›

theorem correctness: ‹G ⊢ p ⟹ ∀e f g. e,f,g,G ⊨ p›
proof (induct p rule: deriv.induct)
  case (Assum a G)
  then show ?case by (simp add: model_def list_all_iff)
next
  case (ForallI G a n)
  show ?case
  proof (intro allI)
    fix f g and e :: ‹nat ⇒ 'c›
    have ‹∀z. e, (f(n := λx. z)), g, G ⊨ (a[App n []/0])›
      using ForallI by blast
    then have ‹∀z. list_all (eval e f g) G ⟶ eval (e⟨0:z⟩) f g a›
      using ForallI unfolding model_def by simp
    then show ‹e,f,g,G ⊨ Forall a› unfolding model_def by simp
  qed
next
  case (ExistsE G a n b)
  show ?case
  proof (intro allI)
    fix f g and e :: ‹nat ⇒ 'c›
    obtain z where ‹list_all (eval e f g) G ⟶ eval (e⟨0:z⟩) f g a›
      using ExistsE unfolding model_def by simp blast
    then have ‹e, (f(n := λx. z)), g, G ⊨ b›
      using ExistsE unfolding model_def by simp
    then show ‹e,f,g,G ⊨ b›
      using ExistsE unfolding model_def by simp
  qed
qed (simp_all add: model_def, blast+)

section ‹Completeness›

text ‹
The goal of this section is to prove completeness of the natural deduction
calculus introduced in \secref{sec:proof-calculus}. Before we start with the
actual proof, it is useful to note that the following two formulations of
completeness are equivalent:
\begin{enumerate}
\item All valid formulae are derivable, i.e.
  ‹ps ⊨ p ⟹ ps ⊢ p›
\item All consistent sets are satisfiable
\end{enumerate}
The latter property is called the {\em model existence theorem}. To see why 2
implies 1, observe that ‹Neg p, ps \<notturnstile> FF› implies
that ‹Neg p, ps› is consistent, which, by the model existence theorem,
implies that ‹Neg p, ps› has a model, which in turn implies that
‹ps \<notTurnstile> p›. By contraposition, it therefore follows
from ‹ps ⊨ p› that ‹Neg p, ps ⊢ FF›, which allows us to
deduce ‹ps ⊢ p› using rule ‹Class›.

In most textbooks on logic, a set ‹S› of formulae is called {\em consistent},
if no contradiction can be derived from ‹S› using a {\em specific proof calculus},
i.e.\ ‹S \<notturnstile> FF›. Rather than defining consistency relative to
a {\em specific} calculus, Fitting uses the more general approach of describing
properties that all consistent sets must have (see \secref{sec:consistent-sets}).

The key idea behind the proof of the model existence theorem is to
extend a consistent set to one that is {\em maximal} (see \secref{sec:extend}).
In order to do this, we use the fact that the set of formulae is enumerable
(see \secref{sec:enumeration}), which allows us to form a sequence
$\phi_0$, $\phi_1$, $\phi_2$, $\ldots$ containing all formulae.
We can then construct a sequence $S_i$ of consistent sets as follows:
\[
\begin{array}{l}
  S_0 = S \\
  S_{i+1} = \left\{\begin{array}{ll}
    S_i \cup \{\phi_i\} & \hbox{if } S_i \cup \{\phi_i\} \hbox{ consistent} \\
    S_i & \hbox{otherwise}
  \end{array}\right.
\end{array}
\]
To obtain a maximal consistent set, we form the union $\bigcup_i S_i$ of these
sets. To ensure that this union is still consistent, additional closure
(see \secref{sec:closure}) and finiteness (see \secref{sec:finiteness})
properties are needed.
It can be shown that a maximal consistent set is a {\em Hintikka set}
(see \secref{sec:hintikka}). Hintikka sets are satisfiable in {\em Herbrand}
models, where closed terms coincide with their interpretation.
›

subsection ‹Consistent sets›

text ‹
\label{sec:consistent-sets}
In this section, we describe an abstract criterion for consistent sets.
A set of sets of formulae is called a {\em consistency property}, if the
following holds:
›

definition consistency :: ‹('a, 'b) form set set ⇒ bool› where
  ‹consistency C = (∀S. S ∈ C ⟶
     (∀p ts. ¬ (Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S)) ∧
     FF ∉ S ∧ Neg TT ∉ S ∧
     (∀Z. Neg (Neg Z) ∈ S ⟶ S ∪ {Z} ∈ C) ∧
     (∀A B. And A B ∈ S ⟶ S ∪ {A, B} ∈ C) ∧
     (∀A B. Neg (Or A B) ∈ S ⟶ S ∪ {Neg A, Neg B} ∈ C) ∧
     (∀A B. Or A B ∈ S ⟶ S ∪ {A} ∈ C ∨ S ∪ {B} ∈ C) ∧
     (∀A B. Neg (And A B) ∈ S ⟶ S ∪ {Neg A} ∈ C ∨ S ∪ {Neg B} ∈ C) ∧
     (∀A B. Impl A B ∈ S ⟶ S ∪ {Neg A} ∈ C ∨ S ∪ {B} ∈ C) ∧
     (∀A B. Neg (Impl A B) ∈ S ⟶ S ∪ {A, Neg B} ∈ C) ∧
     (∀P t. closedt 0 t ⟶ Forall P ∈ S ⟶ S ∪ {P[t/0]} ∈ C) ∧
     (∀P t. closedt 0 t ⟶ Neg (Exists P) ∈ S ⟶ S ∪ {Neg (P[t/0])} ∈ C) ∧
     (∀P. Exists P ∈ S ⟶ (∃x. S ∪ {P[App x []/0]} ∈ C)) ∧
     (∀P. Neg (Forall P) ∈ S ⟶ (∃x. S ∪ {Neg (P[App x []/0])} ∈ C)))›

text ‹
In \secref{sec:finiteness}, we will show how to extend a consistency property
to one that is of {\em finite character}. However, the above
definition of a consistency property cannot be used for this, since there is
a problem with the treatment of formulae of the form ‹Exists P› and
‹Neg (Forall P)›. Fitting therefore suggests to define an {\em alternative
consistency property} as follows:
›

definition alt_consistency :: ‹('a, 'b) form set set ⇒ bool› where
  ‹alt_consistency C = (∀S. S ∈ C ⟶
     (∀p ts. ¬ (Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S)) ∧
     FF ∉ S ∧ Neg TT ∉ S ∧
     (∀Z. Neg (Neg Z) ∈ S ⟶ S ∪ {Z} ∈ C) ∧
     (∀A B. And A B ∈ S ⟶ S ∪ {A, B} ∈ C) ∧
     (∀A B. Neg (Or A B) ∈ S ⟶ S ∪ {Neg A, Neg B} ∈ C) ∧
     (∀A B. Or A B ∈ S ⟶ S ∪ {A} ∈ C ∨ S ∪ {B} ∈ C) ∧
     (∀A B. Neg (And A B) ∈ S ⟶ S ∪ {Neg A} ∈ C ∨ S ∪ {Neg B} ∈ C) ∧
     (∀A B. Impl A B ∈ S ⟶ S ∪ {Neg A} ∈ C ∨ S ∪ {B} ∈ C) ∧
     (∀A B. Neg (Impl A B) ∈ S ⟶ S ∪ {A, Neg B} ∈ C) ∧
     (∀P t. closedt 0 t ⟶ Forall P ∈ S ⟶ S ∪ {P[t/0]} ∈ C) ∧
     (∀P t. closedt 0 t ⟶ Neg (Exists P) ∈ S ⟶ S ∪ {Neg (P[t/0])} ∈ C) ∧
     (∀P x. (∀a ∈ S. x ∉ params a) ⟶ Exists P ∈ S ⟶
       S ∪ {P[App x []/0]} ∈ C) ∧
     (∀P x. (∀a ∈ S. x ∉ params a) ⟶ Neg (Forall P) ∈ S ⟶
       S ∪ {Neg (P[App x []/0])} ∈ C))›

text ‹
Note that in the clauses for ‹Exists P› and ‹Neg (Forall P)›,
the first definition requires the existence of a parameter ‹x› with a certain
property, whereas the second definition requires that all parameters ‹x› that
are new for ‹S› have a certain property. A consistency property can easily be
turned into an alternative consistency property by applying a suitable parameter
substitution:
›

definition mk_alt_consistency :: ‹('a, 'b) form set set ⇒ ('a, 'b) form set set› where
  ‹mk_alt_consistency C = {S. ∃f. psubst f ` S ∈ C}›

theorem alt_consistency:
  assumes conc: ‹consistency C›
  shows ‹alt_consistency (mk_alt_consistency C)› (is ‹alt_consistency ?C'›)
  unfolding alt_consistency_def
proof (intro allI impI conjI)
  fix f :: ‹'a ⇒ 'a› and S :: ‹('a, 'b) form set›

  assume ‹S ∈ mk_alt_consistency C›
  then obtain f where sc: ‹psubst f ` S ∈ C› (is ‹?S' ∈ C›)
    unfolding mk_alt_consistency_def by blast

  fix p ts
  show ‹¬ (Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S)›
  proof
    assume *: ‹Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S›
    then have ‹psubst f (Pred p ts) ∈ ?S'›
      by blast
    then have ‹Pred p (psubstts f ts) ∈ ?S'›
      by simp
    then have ‹Neg (Pred p (psubstts f ts)) ∉ ?S'›
      using conc sc by (simp add: consistency_def)
    then have ‹Neg (Pred p ts) ∉ S›
      by force
    then show False
      using * by blast
  qed

  have ‹FF ∉ ?S'› and ‹Neg TT ∉ ?S'›
    using conc sc unfolding consistency_def by simp_all
  then show ‹FF ∉ S› and ‹Neg TT ∉ S›
    by (force, force)

  { fix Z
    assume ‹Neg (Neg Z) ∈ S›
    then have ‹psubst f (Neg (Neg Z)) ∈ ?S'›
      by blast
    then have ‹?S' ∪ {psubst f Z} ∈ C›
      using conc sc by (simp add: consistency_def)
    then show ‹S ∪ {Z} ∈ ?C'›
      unfolding mk_alt_consistency_def by auto }

  { fix A B
    assume ‹And A B ∈ S›
    then have ‹psubst f (And A B) ∈ ?S'›
      by blast
    then have ‹?S' ∪ {psubst f A, psubst f B} ∈ C›
      using conc sc by (simp add: consistency_def)
    then show ‹S ∪ {A, B} ∈ ?C'›
      unfolding mk_alt_consistency_def by auto }

  { fix A B
    assume ‹Neg (Or A B) ∈ S›
    then have ‹psubst f (Neg (Or A B)) ∈ ?S'›
      by blast
    then have ‹?S' ∪ {Neg (psubst f A), Neg (psubst f B)} ∈ C›
      using conc sc by (simp add: consistency_def)
    then show ‹S ∪ {Neg A, Neg B} ∈ ?C'›
      unfolding mk_alt_consistency_def by auto }

  { fix A B
    assume ‹Neg (Impl A B) ∈ S›
    then have ‹psubst f (Neg (Impl A B)) ∈ ?S'›
      by blast
    then have ‹?S' ∪ {psubst f A, Neg (psubst f B)} ∈ C›
      using conc sc by (simp add: consistency_def)
    then show ‹S ∪ {A, Neg B} ∈ ?C'›
      unfolding mk_alt_consistency_def by auto }

  { fix A B
    assume ‹Or A B ∈ S›
    then have ‹psubst f (Or A B) ∈ ?S'›
      by blast
    then have ‹?S' ∪ {psubst f A} ∈ C ∨ ?S' ∪ {psubst f B} ∈ C›
      using conc sc by (simp add: consistency_def)
    then show ‹S ∪ {A} ∈ ?C' ∨ S ∪ {B} ∈ ?C'›
      unfolding mk_alt_consistency_def by auto }

  { fix A B
    assume ‹Neg (And A B) ∈ S›
    then have ‹psubst f (Neg (And A B)) ∈ ?S'›
      by blast
    then have ‹?S' ∪ {Neg (psubst f A)} ∈ C ∨ ?S' ∪ {Neg (psubst f B)} ∈ C›
      using conc sc by (simp add: consistency_def)
    then show ‹S ∪ {Neg A} ∈ ?C' ∨ S ∪ {Neg B} ∈ ?C'›
      unfolding mk_alt_consistency_def by auto }

  { fix A B
    assume ‹Impl A B ∈ S›
    then have ‹psubst f (Impl A B) ∈ ?S'›
      by blast
    then have ‹?S' ∪ {Neg (psubst f A)} ∈ C ∨ ?S' ∪ {psubst f B} ∈ C›
      using conc sc by (simp add: consistency_def)
    then show ‹S ∪ {Neg A} ∈ ?C' ∨ S ∪ {B} ∈ ?C'›
      unfolding mk_alt_consistency_def by auto }

  { fix P and t :: ‹'a term›
    assume ‹closedt 0 t› and ‹Forall P ∈ S›
    then have ‹psubst f (Forall P) ∈ ?S'›
      by blast
    then have ‹?S' ∪ {psubst f P[psubstt f t/0]} ∈ C›
      using ‹closedt 0 t› conc sc by (simp add: consistency_def)
    then show ‹S ∪ {P[t/0]} ∈ ?C'›
      unfolding mk_alt_consistency_def by auto }

  { fix P and t :: ‹'a term›
    assume ‹closedt 0 t› and ‹Neg (Exists P) ∈ S›
    then have ‹psubst f (Neg (Exists P)) ∈ ?S'›
      by blast
    then have ‹?S' ∪ {Neg (psubst f P[psubstt f t/0])} ∈ C›
      using ‹closedt 0 t› conc sc by (simp add: consistency_def)
    then show ‹S ∪ {Neg (P[t/0])} ∈ ?C'›
      unfolding mk_alt_consistency_def by auto }

  { fix P :: ‹('a, 'b) form› and x f'
    assume ‹∀a ∈ S. x ∉ params a› and ‹Exists P ∈ S›
    moreover have ‹psubst f (Exists P) ∈ ?S'›
      using calculation by blast
    then have ‹∃y. ?S' ∪ {psubst f P[App y []/0]} ∈ C›
      using conc sc by (simp add: consistency_def)
    then obtain y where ‹?S' ∪ {psubst f P[App y []/0]} ∈ C›
      by blast

    moreover have ‹psubst (f(x := y)) ` S = ?S'›
      using calculation by (simp cong add: image_cong)
    moreover have ‹psubst (f(x := y)) `
        S ∪ {psubst (f(x := y)) P[App ((f(x := y)) x) []/0]} ∈ C›
      using calculation by auto
    ultimately have ‹∃f. psubst f ` S ∪ {psubst f P[App (f x) []/0]} ∈ C›
      by blast
    then show ‹S ∪ {P[App x []/0]} ∈ ?C'›
      unfolding mk_alt_consistency_def by simp }

  { fix P :: ‹('a, 'b) form› and x
    assume ‹∀a ∈ S. x ∉ params a› and ‹Neg (Forall P) ∈ S›
    moreover have ‹psubst f (Neg (Forall P)) ∈ ?S'›
      using calculation by blast
    then have ‹∃y. ?S' ∪ {Neg (psubst f P[App y []/0])} ∈ C›
      using conc sc by (simp add: consistency_def)
    then obtain y where ‹?S' ∪ {Neg (psubst f P[App y []/0])} ∈ C›
      by blast

    moreover have ‹psubst (f(x := y)) ` S = ?S'›
      using calculation by (simp cong add: image_cong)
    moreover have ‹psubst (f(x := y)) `
    S ∪ {Neg (psubst (f(x := y)) P[App ((f(x := y)) x) []/0])} ∈ C›
      using calculation by auto
    ultimately have ‹∃f. psubst f ` S ∪ {Neg (psubst f P[App (f x) []/0])} ∈ C›
      by blast
    then show ‹S ∪ {Neg (P[App x []/0])} ∈ ?C'›
      unfolding mk_alt_consistency_def by simp }
qed

theorem mk_alt_consistency_subset: ‹C ⊆ mk_alt_consistency C›
  unfolding mk_alt_consistency_def
proof
  fix x assume ‹x ∈ C›
  then have ‹psubst id ` x ∈ C›
    by simp
  then have ‹(∃f. psubst f ` x ∈ C)›
    by blast
  then show ‹x ∈ {S. ∃f. psubst f ` S ∈ C}›
    by simp
qed

subsection ‹Closure under subsets›

text ‹
\label{sec:closure}
We now show that a consistency property can be extended to one
that is closed under subsets.
›

definition close :: ‹('a, 'b) form set set ⇒ ('a, 'b) form set set› where
  ‹close C = {S. ∃S' ∈ C. S ⊆ S'}›

definition subset_closed :: ‹'a set set ⇒ bool› where
  ‹subset_closed C = (∀S' ∈ C. ∀S. S ⊆ S' ⟶ S ∈ C)›

lemma subset_in_close:
  assumes ‹S ⊆ S'›
  shows ‹S' ∪ x ∈ C ⟶ S ∪ x ∈ close C›
proof -
  have ‹S' ∪ x ∈ close C ⟶ S ∪ x ∈ close C›
    unfolding close_def using ‹S ⊆ S'› by blast
  then show ?thesis unfolding close_def by blast
qed

theorem close_consistency:
  assumes conc: ‹consistency C›
  shows ‹consistency (close C)›
  unfolding consistency_def
proof (intro allI impI conjI)
  fix S
  assume ‹S ∈ close C›
  then obtain x where ‹x ∈ C› and ‹S ⊆ x›
    unfolding close_def by blast

  { fix p ts
    have ‹¬ (Pred p ts ∈ x ∧ Neg (Pred p ts) ∈ x)›
      using ‹x ∈ C› conc unfolding consistency_def by simp
    then show ‹¬ (Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S)›
      using ‹S ⊆ x› by blast }

  { have ‹FF ∉ x›
      using ‹x ∈ C› conc unfolding consistency_def by blast
    then show ‹FF ∉ S›
      using ‹S ⊆ x› by blast }

  { have ‹Neg TT ∉ x›
      using ‹x ∈ C› conc unfolding consistency_def by blast
    then show ‹Neg TT ∉ S›
      using ‹S ⊆ x› by blast }

  { fix Z
    assume ‹Neg (Neg Z) ∈ S›
    then have ‹Neg (Neg Z) ∈ x›
      using ‹S ⊆ x› by blast
    then have ‹x ∪ {Z} ∈ C›
      using ‹x ∈ C› conc unfolding consistency_def by simp
    then show ‹S ∪ {Z} ∈ close C›
      using ‹S ⊆ x› subset_in_close by blast }

  { fix A B
    assume ‹And A B ∈ S›
    then have ‹And A B ∈ x›
      using ‹S ⊆ x› by blast
    then have ‹x ∪ {A, B} ∈ C›
      using ‹x ∈ C› conc unfolding consistency_def by simp
    then show ‹S ∪ {A, B} ∈ close C›
      using ‹S ⊆ x› subset_in_close by blast }

  { fix A B
    assume ‹Neg (Or A B) ∈ S›
    then have ‹Neg (Or A B) ∈ x›
      using ‹S ⊆ x› by blast
    then have ‹x ∪ {Neg A, Neg B} ∈ C›
      using ‹x ∈ C› conc unfolding consistency_def by simp
    then show ‹S ∪ {Neg A, Neg B} ∈ close C›
      using ‹S ⊆ x› subset_in_close by blast }

  { fix A B
    assume ‹Or A B ∈ S›
    then have ‹Or A B ∈ x›
      using ‹S ⊆ x› by blast
    then have ‹x ∪ {A} ∈ C ∨ x ∪ {B} ∈ C›
      using ‹x ∈ C› conc unfolding consistency_def by simp
    then show ‹S ∪ {A} ∈ close C ∨ S ∪ {B} ∈ close C›
      using ‹S ⊆ x› subset_in_close by blast }

  { fix A B
    assume ‹Neg (And A B) ∈ S›
    then have ‹Neg (And A B) ∈ x›
      using ‹S ⊆ x› by blast
    then have ‹x ∪ {Neg A} ∈ C ∨ x ∪ {Neg B} ∈ C›
      using ‹x ∈ C› conc unfolding consistency_def by simp
    then show ‹S ∪ {Neg A} ∈ close C ∨ S ∪ {Neg B} ∈ close C›
      using ‹S ⊆ x› subset_in_close by blast }

  { fix A B
    assume ‹Impl A B ∈ S›
    then have ‹Impl A B ∈ x›
      using ‹S ⊆ x› by blast
    then have ‹x ∪ {Neg A} ∈ C ∨ x ∪ {B} ∈ C›
      using ‹x ∈ C› conc unfolding consistency_def by simp
    then show ‹S ∪ {Neg A} ∈ close C ∨ S ∪ {B} ∈ close C›
      using ‹S ⊆ x› subset_in_close by blast }

  { fix A B
    assume ‹Neg (Impl A B) ∈ S›
    then have ‹Neg (Impl A B) ∈ x›
      using ‹S ⊆ x› by blast
    then have ‹x ∪ {A, Neg B} ∈ C›
      using ‹x ∈ C› conc unfolding consistency_def by blast
    then show ‹S ∪ {A, Neg B} ∈ close C›
      using ‹S ⊆ x› subset_in_close by blast }

  { fix P and t :: ‹'a term›
    assume ‹closedt 0 t› and ‹Forall P ∈ S›
    then have ‹Forall P ∈ x›
      using ‹S ⊆ x› by blast
    then have ‹x ∪ {P[t/0]} ∈ C›
      using ‹closedt 0 t› ‹x ∈ C› conc unfolding consistency_def by blast
    then show ‹S ∪ {P[t/0]} ∈ close C›
      using ‹S ⊆ x› subset_in_close by blast }

  { fix P and t :: ‹'a term›
    assume ‹closedt 0 t› and ‹Neg (Exists P) ∈ S›
    then have ‹Neg (Exists P) ∈ x›
      using ‹S ⊆ x› by blast
    then have ‹x ∪ {Neg (P[t/0])} ∈ C›
      using ‹closedt 0 t› ‹x ∈ C› conc unfolding consistency_def by blast
    then show ‹S ∪ {Neg (P[t/0])} ∈ close C›
      using ‹S ⊆ x› subset_in_close by blast }

  { fix P
    assume ‹Exists P ∈ S›
    then have ‹Exists P ∈ x›
      using ‹S ⊆ x› by blast
    then have ‹∃c. x ∪ {P[App c []/0]} ∈ C›
      using ‹x ∈ C› conc unfolding consistency_def by blast
    then show ‹∃c. S ∪ {P[App c []/0]} ∈ close C›
      using ‹S ⊆ x› subset_in_close by blast }

  { fix P
    assume ‹Neg (Forall P) ∈ S›
    then have ‹Neg (Forall P) ∈ x›
      using ‹S ⊆ x› by blast
    then have ‹∃c. x ∪ {Neg (P[App c []/0])} ∈ C›
      using ‹x ∈ C› conc unfolding consistency_def by simp
    then show ‹∃c. S ∪ {Neg (P[App c []/0])} ∈ close C›
      using ‹S ⊆ x› subset_in_close by blast }
qed

theorem close_closed: ‹subset_closed (close C)›
  unfolding close_def subset_closed_def by blast

theorem close_subset: ‹C ⊆ close C›
  unfolding close_def by blast

text ‹
If a consistency property ‹C› is closed under subsets, so is the
corresponding alternative consistency property:
›

theorem mk_alt_consistency_closed:
  assumes ‹subset_closed C›
  shows ‹subset_closed (mk_alt_consistency C)›
  unfolding subset_closed_def mk_alt_consistency_def
proof (intro ballI allI impI)
  fix S S' :: ‹('a, 'b) form set›
  assume ‹S ⊆ S'› and ‹S' ∈ {S. ∃f. psubst f ` S ∈ C}›
  then obtain f where *: ‹psubst f ` S' ∈ C›
    by blast
  moreover have ‹psubst f ` S ⊆ psubst f ` S'›
    using ‹S ⊆ S'› by blast
  moreover have ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
    using ‹subset_closed C› unfolding subset_closed_def by blast
  ultimately have ‹psubst f ` S ∈ C›
    by blast
  then show ‹S ∈ {S. ∃f. psubst f ` S ∈ C}›
    by blast
qed

subsection ‹Finite character›

text ‹
\label{sec:finiteness}
In this section, we show that an alternative consistency property can
be extended to one of finite character. A set of sets ‹C› is said
to be of finite character, provided that ‹S› is a member of ‹C›
if and only if every subset of ‹S› is.
›

definition finite_char :: ‹'a set set ⇒ bool› where
  ‹finite_char C = (∀S. S ∈ C = (∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ C))›

definition mk_finite_char :: ‹'a set set ⇒ 'a set set› where
  ‹mk_finite_char C = {S. ∀S'. S' ⊆ S ⟶ finite S' ⟶ S' ∈ C}›

theorem finite_alt_consistency:
  assumes altconc: ‹alt_consistency C›
    and ‹subset_closed C›
  shows ‹alt_consistency (mk_finite_char C)›
  unfolding alt_consistency_def
proof (intro allI impI conjI)
  fix S
  assume ‹S ∈ mk_finite_char C›
  then have finc: ‹∀S' ⊆ S. finite S' ⟶ S' ∈ C›
    unfolding mk_finite_char_def by blast

  have ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
    using ‹subset_closed C› unfolding subset_closed_def by blast
  then have sc: ‹∀S' x. S' ∪ x ∈ C ⟶ (∀S ⊆ S' ∪ x. S ∈ C)›
    by blast

  { fix p ts
    show ‹¬ (Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S)›
    proof
      assume ‹Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S›
      then have ‹{Pred p ts, Neg (Pred p ts)} ∈ C›
        using finc by simp
      then show False
        using altconc unfolding alt_consistency_def by fast
    qed }

  show ‹FF ∉ S›
  proof
    assume ‹FF ∈ S›
    then have ‹{FF} ∈ C›
      using finc by simp
    then show False
      using altconc unfolding alt_consistency_def by fast
  qed

  show ‹Neg TT ∉ S›
  proof
    assume ‹Neg TT ∈ S›
    then have ‹{Neg TT} ∈ C›
      using finc by simp
    then show False
      using altconc unfolding alt_consistency_def by fast
  qed

  { fix Z
    assume *: ‹Neg (Neg Z) ∈ S›
    show ‹S ∪ {Z} ∈ mk_finite_char C›
      unfolding mk_finite_char_def
    proof (intro allI impI CollectI)
      fix S'
      let ?S' = ‹S' - {Z} ∪ {Neg (Neg Z)}›

      assume ‹S' ⊆ S ∪ {Z}› and ‹finite S'›
      then have ‹?S' ⊆ S›
        using * by blast
      moreover have ‹finite ?S'›
        using ‹finite S'› by blast
      ultimately have ‹?S' ∈ C›
        using finc by blast
      then have ‹?S' ∪ {Z} ∈ C›
        using altconc unfolding alt_consistency_def by simp
      then show ‹S' ∈ C›
        using sc by blast
    qed }

  { fix A B
    assume *: ‹And A B ∈ S›
    show ‹S ∪ {A, B} ∈ mk_finite_char C›
      unfolding mk_finite_char_def
    proof (intro allI impI CollectI)
      fix S'
      let ?S' = ‹S' - {A, B} ∪ {And A B}›

      assume ‹S' ⊆ S ∪ {A, B}› and ‹finite S'›
      then have ‹?S' ⊆ S›
        using * by blast
      moreover have ‹finite ?S'›
        using ‹finite S'› by blast
      ultimately have ‹?S' ∈ C›
        using finc by blast
      then have ‹?S' ∪ {A, B} ∈ C›
        using altconc unfolding alt_consistency_def by simp
      then show ‹S' ∈ C›
        using sc by blast
    qed }

  { fix A B
    assume *: ‹Neg (Or A B) ∈ S›
    show ‹S ∪ {Neg A, Neg B} ∈ mk_finite_char C›
      unfolding mk_finite_char_def
    proof (intro allI impI CollectI)
      fix S'
      let ?S' = ‹S' - {Neg A, Neg B} ∪ {Neg (Or A B)}›

      assume ‹S' ⊆ S ∪ {Neg A, Neg B}› and ‹finite S'›
      then have ‹?S' ⊆ S›
        using * by blast
      moreover have ‹finite ?S'›
        using ‹finite S'› by blast
      ultimately have ‹?S' ∈ C›
        using finc by blast
      then have ‹?S' ∪ {Neg A, Neg B} ∈ C›
        using altconc unfolding alt_consistency_def by simp
      then show ‹S' ∈ C›
        using sc by blast
    qed }

  { fix A B
    assume *: ‹Neg (Impl A B) ∈ S›
    show ‹S ∪ {A, Neg B} ∈ mk_finite_char C›
      unfolding mk_finite_char_def
    proof (intro allI impI CollectI)
      fix S'
      let ?S' = ‹S' - {A, Neg B} ∪ {Neg (Impl A B)}›

      assume ‹S' ⊆ S ∪ {A, Neg B}› and ‹finite S'›
      then have ‹?S' ⊆ S›
        using * by blast
      moreover have ‹finite ?S'›
        using ‹finite S'› by blast
      ultimately have ‹?S' ∈ C›
        using finc by blast
      then have ‹?S' ∪ {A, Neg B} ∈ C›
        using altconc unfolding alt_consistency_def by simp
      then show ‹S' ∈ C›
        using sc by blast
    qed }

  { fix A B
    assume *: ‹Or A B ∈ S›
    show ‹S ∪ {A} ∈ mk_finite_char C ∨ S ∪ {B} ∈ mk_finite_char C›
    proof (rule ccontr)
      assume ‹¬ ?thesis›
      then obtain Sa and Sb
        where ‹Sa ⊆ S ∪ {A}› and ‹finite Sa› and ‹Sa ∉ C›
          and ‹Sb ⊆ S ∪ {B}› and ‹finite Sb› and ‹Sb ∉ C›
        unfolding mk_finite_char_def by blast

      let ?S' = ‹(Sa - {A}) ∪ (Sb - {B}) ∪ {Or A B}›

      have ‹?S' ⊆ S›
        using ‹Sa ⊆ S ∪ {A}› ‹Sb ⊆ S ∪ {B}› * by blast
      moreover have ‹finite ?S'›
        using ‹finite Sa› ‹finite Sb› by blast
      ultimately have ‹?S' ∈ C›
        using finc by blast
      then have ‹?S' ∪ {A} ∈ C ∨ ?S' ∪ {B} ∈ C›
        using altconc unfolding alt_consistency_def by simp
      then have ‹Sa ∈ C ∨ Sb ∈ C›
        using sc by blast
      then show False
        using ‹Sa ∉ C› ‹Sb ∉ C› by blast
    qed }

  { fix A B
    assume *: ‹Neg (And A B) ∈ S›
    show ‹S ∪ {Neg A} ∈ mk_finite_char C ∨ S ∪ {Neg B} ∈ mk_finite_char C›
    proof (rule ccontr)
      assume ‹¬ ?thesis›
      then obtain Sa and Sb
        where ‹Sa ⊆ S ∪ {Neg A}› and ‹finite Sa› and ‹Sa ∉ C›
          and ‹Sb ⊆ S ∪ {Neg B}› and ‹finite Sb› and ‹Sb ∉ C›
        unfolding mk_finite_char_def by blast

      let ?S' = ‹(Sa - {Neg A}) ∪ (Sb - {Neg B}) ∪ {Neg (And A B)}›

      have ‹?S' ⊆ S›
        using ‹Sa ⊆ S ∪ {Neg A}› ‹Sb ⊆ S ∪ {Neg B}› * by blast
      moreover have ‹finite ?S'›
        using ‹finite Sa› ‹finite Sb› by blast
      ultimately have ‹?S' ∈ C›
        using finc by blast
      then have ‹?S' ∪ {Neg A} ∈ C ∨ ?S' ∪ {Neg B} ∈ C›
        using altconc unfolding alt_consistency_def by simp
      then have ‹Sa ∈ C ∨ Sb ∈ C›
        using sc by blast
      then show False
        using ‹Sa ∉ C› ‹Sb ∉ C› by blast
    qed }

  { fix A B
    assume *: ‹Impl A B ∈ S›
    show ‹S ∪ {Neg A} ∈ mk_finite_char C ∨ S ∪ {B} ∈ mk_finite_char C›
    proof (rule ccontr)
      assume ‹¬ ?thesis›
      then obtain Sa and Sb
        where ‹Sa ⊆ S ∪ {Neg A}› and ‹finite Sa› and ‹Sa ∉ C›
          and ‹Sb ⊆ S ∪ {B}› and ‹finite Sb› and ‹Sb ∉ C›
        unfolding mk_finite_char_def by blast

      let ?S' = ‹(Sa - {Neg A}) ∪ (Sb - {B}) ∪ {Impl A B}›

      have ‹?S' ⊆ S›
        using ‹Sa ⊆ S ∪ {Neg A}› ‹Sb ⊆ S ∪ {B}› * by blast
      moreover have ‹finite ?S'›
        using ‹finite Sa› ‹finite Sb› by blast
      ultimately have ‹?S' ∈ C›
        using finc by blast
      then have ‹?S' ∪ {Neg A} ∈ C ∨ ?S' ∪ {B} ∈ C›
        using altconc unfolding alt_consistency_def by simp
      then have ‹Sa ∈ C ∨ Sb ∈ C›
        using sc by blast
      then show False
        using ‹Sa ∉ C› ‹Sb ∉ C› by blast
    qed }

  { fix P and t :: ‹'a term›
    assume *: ‹Forall P ∈ S› and ‹closedt 0 t›
    show ‹S ∪ {P[t/0]} ∈ mk_finite_char C›
      unfolding mk_finite_char_def
    proof (intro allI impI CollectI)
      fix S'
      let ?S' = ‹S' - {P[t/0]} ∪ {Forall P}›

      assume ‹S' ⊆ S ∪ {P[t/0]}› and ‹finite S'›
      then have ‹?S' ⊆ S›
        using * by blast
      moreover have ‹finite ?S'›
        using ‹finite S'› by blast
      ultimately have ‹?S' ∈ C›
        using finc by blast
      then have ‹?S' ∪ {P[t/0]} ∈ C›
        using altconc ‹closedt 0 t› unfolding alt_consistency_def by simp
      then show ‹S' ∈ C›
        using sc by blast
    qed }

  { fix P and t :: ‹'a term›
    assume *: ‹Neg (Exists P) ∈ S› and ‹closedt 0 t›
    show ‹S ∪ {Neg (P[t/0])} ∈ mk_finite_char C›
      unfolding mk_finite_char_def
    proof (intro allI impI CollectI)
      fix S'
      let ?S' = ‹S' - {Neg (P[t/0])} ∪ {Neg (Exists P)}›

      assume ‹S' ⊆ S ∪ {Neg (P[t/0])}› and ‹finite S'›
      then have ‹?S' ⊆ S›
        using * by blast
      moreover have ‹finite ?S'›
        using ‹finite S'› by blast
      ultimately have ‹?S' ∈ C›
        using finc by blast
      then have ‹?S' ∪ {Neg (P[t/0])} ∈ C›
        using altconc ‹closedt 0 t› unfolding alt_consistency_def by simp
      then show ‹S' ∈ C›
        using sc by blast
    qed }

  { fix P x
    assume *: ‹Exists P ∈ S› and ‹∀a ∈ S. x ∉ params a›
    show ‹S ∪ {P[App x []/0]} ∈ mk_finite_char C›
      unfolding mk_finite_char_def
    proof (intro allI impI CollectI)
      fix S'
      let ?S' = ‹S' - {P[App x []/0]} ∪ {Exists P}›

      assume ‹S' ⊆ S ∪ {P[App x []/0]}› and ‹finite S'›
      then have ‹?S' ⊆ S›
        using * by blast
      moreover have ‹finite ?S'›
        using ‹finite S'› by blast
      ultimately have ‹?S' ∈ C›
        using finc by blast
      moreover have ‹∀a ∈ ?S'. x ∉ params a›
        using ‹∀a ∈ S. x ∉ params a› ‹?S' ⊆ S› by blast
      ultimately have ‹?S' ∪ {P[App x []/0]} ∈ C›
        using altconc ‹∀a ∈ S. x ∉ params a› unfolding alt_consistency_def by blast
      then show ‹S' ∈ C›
        using sc by blast
    qed }

  { fix P x
    assume *: ‹Neg (Forall P) ∈ S› and ‹∀a ∈ S. x ∉ params a›
    show ‹S ∪ {Neg (P[App x []/0])} ∈ mk_finite_char C›
      unfolding mk_finite_char_def
    proof (intro allI impI CollectI)
      fix S'
      let ?S' = ‹S' - {Neg (P[App x []/0])} ∪ {Neg (Forall P)}›

      assume ‹S' ⊆ S ∪ {Neg (P[App x []/0])}› and ‹finite S'›
      then have ‹?S' ⊆ S›
        using * by blast
      moreover have ‹finite ?S'›
        using ‹finite S'› by blast
      ultimately have ‹?S' ∈ C›
        using finc by blast
      moreover have ‹∀a ∈ ?S'. x ∉ params a›
        using ‹∀a ∈ S. x ∉ params a› ‹?S' ⊆ S› by blast
      ultimately have ‹?S' ∪ {Neg (P[App x []/0])} ∈ C›
        using altconc ‹∀a ∈ S. x ∉ params a› unfolding alt_consistency_def by simp
      then show ‹S' ∈ C›
        using sc by blast
    qed }
qed

theorem finite_char: ‹finite_char (mk_finite_char C)›
  unfolding finite_char_def mk_finite_char_def by blast

theorem finite_char_closed: ‹finite_char C ⟹ subset_closed C›
  unfolding finite_char_def subset_closed_def
proof (intro ballI allI impI)
  fix S S'
  assume *: ‹∀S. (S ∈ C) = (∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ C)›
    and ‹S' ∈ C› and ‹S ⊆ S'›
  then have ‹∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ C› by blast
  then show ‹S ∈ C› using * by blast
qed

theorem finite_char_subset: ‹subset_closed C ⟹ C ⊆ mk_finite_char C›
  unfolding mk_finite_char_def subset_closed_def by blast

subsection ‹Enumerating datatypes›

text ‹
\label{sec:enumeration}
As has already been mentioned earlier, the proof of the model existence theorem
relies on the fact that the set of formulae is enumerable. Using the infrastructure
for datatypes, the types @{type term} and @{type form} can automatically be shown to
be a member of the @{class countable} type class:
›

instance ‹term› :: (countable) countable
  by countable_datatype

instance form :: (countable, countable) countable
  by countable_datatype

subsection ‹Extension to maximal consistent sets›

text ‹
\label{sec:extend}
Given a set ‹C› of finite character, we show that
the least upper bound of a chain of sets that are elements
of ‹C› is again an element of ‹C›.
›

definition is_chain :: ‹(nat ⇒ 'a set) ⇒ bool› where
  ‹is_chain f = (∀n. f n ⊆ f (Suc n))›

theorem is_chainD: ‹is_chain f ⟹ x ∈ f m ⟹ x ∈ f (m + n)›
  by (induct n) (auto simp: is_chain_def)

theorem is_chainD':
  assumes ‹is_chain f› and ‹x ∈ f m› and ‹m ≤ k›
  shows ‹x ∈ f k›
proof -
  have ‹∃n. k = m + n›
    using ‹m ≤ k› by (simp add: le_iff_add)
  then obtain n where ‹k = m + n›
    by blast
  then show ‹x ∈ f k›
    using ‹is_chain f› ‹x ∈ f m›
    by (simp add: is_chainD)
qed

theorem chain_index:
  assumes ch: ‹is_chain f› and fin: ‹finite F›
  shows ‹F ⊆ (⋃n. f n) ⟹ ∃n. F ⊆ f n›
  using fin
proof (induct rule: finite_induct)
  case empty
  then show ?case by blast
next
  case (insert x F)
  then have ‹∃n. F ⊆ f n› and ‹∃m. x ∈ f m› and ‹F ⊆ (⋃x. f x)›
    using ch by simp_all
  then obtain n and m where ‹F ⊆ f n› and ‹x ∈ f m›
    by blast
  have ‹m ≤ max n m› and ‹n ≤ max n m›
    by simp_all
  have ‹x ∈ f (max n m)›
    using is_chainD' ch ‹x ∈ f m› ‹m ≤ max n m› by fast
  moreover have ‹F ⊆ f (max n m)›
    using is_chainD' ch ‹F ⊆ f n› ‹n ≤ max n m› by fast
  moreover have ‹x ∈ f (max n m) ∧ F ⊆ f (max n m)›
    using calculation by blast
  ultimately show ?case by blast
qed

lemma chain_union_closed':
  assumes ‹is_chain f› and ‹(∀n. f n ∈ C)› and ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
    and ‹finite S'› and ‹S' ⊆ (⋃n. f n)›
  shows ‹S' ∈ C›
proof -
  note ‹finite S'› and ‹S' ⊆ (⋃n. f n)›
  then obtain n where ‹S' ⊆ f n›
    using chain_index ‹is_chain f› by blast
  moreover have ‹f n ∈ C›
    using ‹∀n. f n ∈ C› by blast
  ultimately show ‹S' ∈ C›
    using ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C› by blast
qed

theorem chain_union_closed:
  assumes ‹finite_char C› and ‹is_chain f› and ‹∀n. f n ∈ C›
  shows ‹(⋃n. f n) ∈ C›
proof -
  have ‹subset_closed C›
    using finite_char_closed ‹finite_char C› by blast
  then have ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
    using subset_closed_def by blast
  then have ‹∀S'. finite S' ⟶ S' ⊆ (⋃n. f n) ⟶ S' ∈ C›
    using chain_union_closed' assms by blast
  moreover have ‹((⋃n. f n) ∈ C) = (∀S'. finite S' ⟶ S' ⊆ (⋃n. f n) ⟶ S' ∈ C)›
    using ‹finite_char C› unfolding finite_char_def by blast
  ultimately show ?thesis by blast
qed

text ‹
We can now define a function ‹Extend› that extends a consistent
set to a maximal consistent set. To this end, we first define an auxiliary
function ‹extend› that produces the elements of an ascending chain of
consistent sets.
›

primrec (nonexhaustive) dest_Neg :: ‹('a, 'b) form ⇒ ('a, 'b) form› where
  ‹dest_Neg (Neg p) = p›

primrec (nonexhaustive) dest_Forall :: ‹('a, 'b) form ⇒ ('a, 'b) form› where
  ‹dest_Forall (Forall p) = p›

primrec (nonexhaustive) dest_Exists :: ‹('a, 'b) form ⇒ ('a, 'b) form› where
  ‹dest_Exists (Exists p) = p›

primrec extend :: ‹(nat, 'b) form set ⇒ (nat, 'b) form set set ⇒
    (nat ⇒ (nat, 'b) form) ⇒ nat ⇒ (nat, 'b) form set› where
  ‹extend S C f 0 = S›
| ‹extend S C f (Suc n) = (if extend S C f n ∪ {f n} ∈ C
     then
       (if (∃p. f n = Exists p)
        then extend S C f n ∪ {f n} ∪ {subst (dest_Exists (f n))
          (App (SOME k. k ∉ (⋃p ∈ extend S C f n ∪ {f n}. params p)) []) 0}
        else if (∃p. f n = Neg (Forall p))
        then extend S C f n ∪ {f n} ∪ {Neg (subst (dest_Forall (dest_Neg (f n)))
          (App (SOME k. k ∉ (⋃p ∈ extend S C f n ∪ {f n}. params p)) []) 0)}
        else extend S C f n ∪ {f n})
     else extend S C f n)›

definition Extend :: ‹(nat, 'b) form set ⇒ (nat, 'b) form set set ⇒
    (nat ⇒ (nat, 'b) form) ⇒ (nat, 'b) form set› where
  ‹Extend S C f = (⋃n. extend S C f n)›

theorem is_chain_extend: ‹is_chain (extend S C f)›
  by (simp add: is_chain_def) blast

theorem finite_paramst [simp]: ‹finite (paramst (t :: 'a term))›
  ‹finite (paramsts (ts :: 'a term list))›
  by (induct t and ts rule: paramst.induct paramsts.induct) (simp_all split: sum.split)

theorem finite_params [simp]: ‹finite (params p)›
  by (induct p) simp_all

theorem finite_params_extend [simp]:
  ‹infinite (⋂p ∈ S. - params p) ⟹ infinite (⋂p ∈ extend S C f n. - params p)›
  by (induct n) simp_all

lemma infinite_params_available:
  assumes ‹infinite (- (⋃p ∈ S. params p))›
  shows ‹∃x. x ∉ (⋃p ∈ extend S C f n ∪ {f n}. params p)›
proof -
  let ?S' = ‹extend S C f n ∪ {f n}›

  have ‹infinite (- (⋃x ∈ ?S'. params x))›
    using assms by simp
  then obtain x where ‹x ∈ - (⋃x ∈ ?S'. params x)›
    using infinite_imp_nonempty by blast
  then have ‹∀a ∈ ?S'. x ∉ params a›
    by blast
  then show ?thesis
    by blast
qed

lemma extend_in_C_Exists:
  assumes ‹alt_consistency C›
    and ‹infinite (- (⋃p ∈ S. params p))›
    and ‹extend S C f n ∪ {f n} ∈ C› (is ‹?S' ∈ C›)
    and ‹∃p. f n = Exists p›
  shows ‹extend S C f (Suc n) ∈ C›
proof -
  obtain p where *: ‹f n = Exists p›
    using ‹∃p. f n = Exists p› by blast
  have ‹∃x. x ∉ (⋃p ∈ ?S'. params p)›
    using ‹infinite (- (⋃p ∈ S. params p))› infinite_params_available
    by blast
  moreover have ‹Exists p ∈ ?S'›
    using * by simp
  then have ‹∀x. x ∉ (⋃p ∈ ?S'. params p) ⟶ ?S' ∪ {p[App x []/0]} ∈ C›
    using ‹?S' ∈ C› ‹alt_consistency C›
    unfolding alt_consistency_def by simp
  ultimately have ‹(?S' ∪ {p[App (SOME k. k ∉ (⋃p ∈ ?S'. params p)) []/0]}) ∈ C›
    by (metis (mono_tags, lifting) someI2)
  then show ?thesis
    using assms * by simp
qed

lemma extend_in_C_Neg_Forall:
  assumes ‹alt_consistency C›
    and ‹infinite (- (⋃p ∈ S. params p))›
    and ‹extend S C f n ∪ {f n} ∈ C› (is ‹?S' ∈ C›)
    and ‹∀p. f n ≠ Exists p›
    and ‹∃p. f n = Neg (Forall p)›
  shows ‹extend S C f (Suc n) ∈ C›
proof -
  obtain p where *: ‹f n = Neg (Forall p)›
    using ‹∃p. f n = Neg (Forall p)› by blast
  have ‹∃x. x ∉ (⋃p ∈ ?S'. params p)›
    using ‹infinite (- (⋃p ∈ S. params p))› infinite_params_available
    by blast
  moreover have ‹Neg (Forall p) ∈ ?S'›
    using * by simp
  then have ‹∀x. x ∉ (⋃p ∈ ?S'. params p) ⟶ ?S' ∪ {Neg (p[App x []/0])} ∈ C›
    using ‹?S' ∈ C› ‹alt_consistency C›
    unfolding alt_consistency_def by simp
  ultimately have ‹(?S' ∪ {Neg (p[App (SOME k. k ∉ (⋃p ∈ ?S'. params p)) []/0])}) ∈ C›
    by (metis (mono_tags, lifting) someI2)
  then show ?thesis
    using assms * by simp
qed

lemma extend_in_C_no_delta:
  assumes ‹extend S C f n ∪ {f n} ∈ C›
    and ‹∀p. f n ≠ Exists p›
    and ‹∀p. f n ≠ Neg (Forall p)›
  shows ‹extend S C f (Suc n) ∈ C›
  using assms by simp

lemma extend_in_C_stop:
  assumes ‹extend S C f n ∈ C›
    and ‹extend S C f n ∪ {f n} ∉ C›
  shows ‹extend S C f (Suc n) ∈ C›
  using assms by simp

theorem extend_in_C: ‹alt_consistency C ⟹
  S ∈ C ⟹ infinite (- (⋃p ∈ S. params p)) ⟹ extend S C f n ∈ C›
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case
    using extend_in_C_Exists extend_in_C_Neg_Forall
      extend_in_C_no_delta extend_in_C_stop
    by metis
qed

text ‹
The main theorem about ‹Extend› says that if ‹C› is an
alternative consistency property that is of finite character,
‹S› is consistent and ‹S› uses only finitely many
parameters, then ‹Extend S C f› is again consistent.
›

theorem Extend_in_C: ‹alt_consistency C ⟹ finite_char C ⟹
  S ∈ C ⟹ infinite (- (⋃p ∈ S. params p)) ⟹ Extend S C f ∈ C›
  unfolding Extend_def
  using chain_union_closed is_chain_extend extend_in_C
  by blast

theorem Extend_subset: ‹S ⊆ Extend S C f›
proof
  fix x
  assume ‹x ∈ S›
  then have ‹x ∈ extend S C f 0› by simp
  then have ‹∃n. x ∈ extend S C f n› by blast
  then show ‹x ∈ Extend S C f› by (simp add: Extend_def)
qed

text ‹
The ‹Extend› function yields a maximal set:
›

definition maximal :: ‹'a set ⇒ 'a set set ⇒ bool› where
  ‹maximal S C = (∀S' ∈ C. S ⊆ S' ⟶ S = S')›

theorem extend_maximal:
  assumes ‹∀y. ∃n. y = f n›
    and ‹finite_char C›
  shows ‹maximal (Extend S C f) C›
  unfolding maximal_def Extend_def
proof (intro ballI impI)
  fix S'
  assume ‹S' ∈ C›
    and ‹(⋃x. extend S C f x) ⊆ S'›
  moreover have ‹S' ⊆ (⋃x. extend S C f x)›
  proof (rule ccontr)
    assume ‹¬ S' ⊆ (⋃x. extend S C f x)›
    then have ‹∃z. z ∈ S' ∧ z ∉ (⋃x. extend S C f x)›
      by blast
    then obtain z where ‹z ∈ S'› and *: ‹z ∉ (⋃x. extend S C f x)›
      by blast
    then obtain n where ‹z = f n›
      using ‹∀y. ∃n. y = f n› by blast

    from ‹(⋃x. extend S C f x) ⊆ S'› ‹z = f n› ‹z ∈ S'›
    have ‹extend S C f n ∪ {f n} ⊆ S'› by blast

    from ‹finite_char C›
    have ‹subset_closed C› using finite_char_closed by blast
    then have ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
      unfolding subset_closed_def by simp
    then have ‹∀S ⊆ S'. S ∈ C›
      using ‹S' ∈ C› by blast
    then have ‹extend S C f n ∪ {f n} ∈ C›
      using ‹extend S C f n ∪ {f n} ⊆ S'›
      by blast
    then have ‹z ∈ extend S C f (Suc n)›
      using ‹z ∉ (⋃x. extend S C f x)› ‹z = f n›
      by simp
    then show False using * by blast
  qed
  ultimately show ‹(⋃x. extend S C f x) = S'›
    by simp
qed

subsection ‹Hintikka sets and Herbrand models›

text ‹
\label{sec:hintikka}
A Hintikka set is defined as follows:
›

definition hintikka :: ‹('a, 'b) form set ⇒ bool› where
  ‹hintikka H =
     ((∀p ts. ¬ (Pred p ts ∈ H ∧ Neg (Pred p ts) ∈ H)) ∧
     FF ∉ H ∧ Neg TT ∉ H ∧
     (∀Z. Neg (Neg Z) ∈ H ⟶ Z ∈ H) ∧
     (∀A B. And A B ∈ H ⟶ A ∈ H ∧ B ∈ H) ∧
     (∀A B. Neg (Or A B) ∈ H ⟶ Neg A ∈ H ∧ Neg B ∈ H) ∧
     (∀A B. Or A B ∈ H ⟶ A ∈ H ∨ B ∈ H) ∧
     (∀A B. Neg (And A B) ∈ H ⟶ Neg A ∈ H ∨ Neg B ∈ H) ∧
     (∀A B. Impl A B ∈ H ⟶ Neg A ∈ H ∨ B ∈ H) ∧
     (∀A B. Neg (Impl A B) ∈ H ⟶ A ∈ H ∧ Neg B ∈ H) ∧
     (∀P t. closedt 0 t ⟶ Forall P ∈ H ⟶ subst P t 0 ∈ H) ∧
     (∀P t. closedt 0 t ⟶ Neg (Exists P) ∈ H ⟶ Neg (subst P t 0) ∈ H) ∧
     (∀P. Exists P ∈ H ⟶ (∃t. closedt 0 t ∧ subst P t 0 ∈ H)) ∧
     (∀P. Neg (Forall P) ∈ H ⟶ (∃t. closedt 0 t ∧ Neg (subst P t 0) ∈ H)))›

text ‹
In Herbrand models, each {\em closed} term is interpreted by itself.
We introduce a new datatype ‹hterm› (``Herbrand terms''), which
is similar to the datatype ‹term› introduced in \secref{sec:terms},
but without variables. We also define functions for converting between
closed terms and Herbrand terms.
›

datatype 'a hterm = HApp 'a ‹'a hterm list›

primrec
  term_of_hterm :: ‹'a hterm ⇒ 'a term› and
  terms_of_hterms :: ‹'a hterm list ⇒ 'a term list› where
  ‹term_of_hterm (HApp a hts) = App a (terms_of_hterms hts)›
| ‹terms_of_hterms [] = []›
| ‹terms_of_hterms (ht # hts) = term_of_hterm ht # terms_of_hterms hts›

theorem herbrand_evalt [simp]:
  ‹closedt 0 t ⟹ term_of_hterm (evalt e HApp t) = t›
  ‹closedts 0 ts ⟹ terms_of_hterms (evalts e HApp ts) = ts›
  by (induct t and ts rule: closedt.induct closedts.induct) simp_all

theorem herbrand_evalt' [simp]:
  ‹evalt e HApp (term_of_hterm ht) = ht›
  ‹evalts e HApp (terms_of_hterms hts) = hts›
  by (induct ht and hts rule: term_of_hterm.induct terms_of_hterms.induct) simp_all

theorem closed_hterm [simp]:
  ‹closedt 0 (term_of_hterm (ht::'a hterm))›
  ‹closedts 0 (terms_of_hterms (hts::'a hterm list))›
  by (induct ht and hts rule: term_of_hterm.induct terms_of_hterms.induct) simp_all

text ‹
We can prove that Hintikka sets are satisfiable in Herbrand models.
Note that this theorem cannot be proved by a simple structural induction
(as claimed in Fitting's book), since a parameter substitution has
to be applied in the cases for quantifiers. However, since parameter
substitution does not change the size of formulae, the theorem can
be proved by well-founded induction on the size of the formula ‹p›.
›

theorem hintikka_model:
  assumes hin: ‹hintikka H›
  shows ‹(p ∈ H ⟶ closed 0 p ⟶
    eval e HApp (λa ts. Pred a (terms_of_hterms ts) ∈ H) p) ∧
  (Neg p ∈ H ⟶ closed 0 p ⟶
    eval e HApp (λa ts. Pred a (terms_of_hterms ts) ∈ H) (Neg p))›
proof (induct p rule: wf_induct [where r=‹measure size_form›])
  show ‹wf (measure size_form)›
    by blast
next
  let ?eval = ‹eval e HApp (λa ts. Pred a (terms_of_hterms ts) ∈ H)›

  fix x
  assume wf: ‹∀y. (y, x) ∈ measure size_form ⟶
                  (y ∈ H ⟶ closed 0 y ⟶ ?eval y) ∧
              (Neg y ∈ H ⟶ closed 0 y ⟶ ?eval (Neg y))›

  show ‹(x ∈ H ⟶ closed 0 x ⟶ ?eval x) ∧ (Neg x ∈ H ⟶ closed 0 x ⟶ ?eval (Neg x))›
  proof (cases x)
    case FF
    show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ H›
      then show ‹?eval x›
        using FF hin by (simp add: hintikka_def)
    next
      assume ‹Neg x ∈ H›
      then show ‹?eval (Neg x)› using FF by simp
    qed
  next
    case TT
    show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ H›
      then show ‹?eval x›
        using TT by simp
    next
      assume ‹Neg x ∈ H›
      then show ‹?eval (Neg x)›
        using TT hin by (simp add: hintikka_def)
    qed
  next
    case (Pred p ts)
    show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ H› and ‹closed 0 x›
      then show ‹?eval x› using Pred by simp
    next
      assume ‹Neg x ∈ H› and ‹closed 0 x›
      then have ‹Neg (Pred p ts) ∈ H›
        using Pred by simp
      then have ‹Pred p ts ∉ H›
        using hin unfolding hintikka_def by fast
      then show ‹?eval (Neg x)›
        using Pred ‹closed 0 x› by simp
    qed
  next
    case (Neg Z)
    then show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ H› and ‹closed 0 x›
      then show ‹?eval x›
        using Neg wf by simp
    next
      assume ‹Neg x ∈ H›
      then have ‹Z ∈ H›
        using Neg hin unfolding hintikka_def by blast
      moreover assume ‹closed 0 x›
      then have ‹closed 0 Z›
        using Neg by simp
      ultimately have ‹?eval Z›
        using Neg wf by simp
      then show ‹?eval (Neg x)›
        using Neg by simp
    qed
  next
    case (And A B)
    then show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ H› and ‹closed 0 x›
      then have ‹And A B ∈ H› and ‹closed 0 (And A B)›
        using And by simp_all
      then have ‹A ∈ H ∧ B ∈ H›
        using And hin unfolding hintikka_def by blast
      then show ‹?eval x›
        using And wf ‹closed 0 (And A B)› by simp
    next
      assume ‹Neg x ∈ H› and ‹closed 0 x›
      then have ‹Neg (And A B) ∈ H› and ‹closed 0 (And A B)›
        using And by simp_all
      then have ‹Neg A ∈ H ∨ Neg B ∈ H›
        using hin unfolding hintikka_def by blast
      then show ‹?eval (Neg x)›
        using And wf ‹closed 0 (And A B)› by fastforce
    qed
  next
    case (Or A B)
    then show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ H› and ‹closed 0 x›
      then have ‹Or A B ∈ H› and ‹closed 0 (Or A B)›
        using Or by simp_all
      then have ‹A ∈ H ∨ B ∈ H›
        using hin unfolding hintikka_def by blast
      then show ‹?eval x›
        using Or wf ‹closed 0 (Or A B)› by fastforce
    next
      assume ‹Neg x ∈ H› and ‹closed 0 x›
      then have ‹Neg (Or A B) ∈ H› and ‹closed 0 (Or A B)›
        using Or by simp_all
      then have ‹Neg A ∈ H ∧ Neg B ∈ H›
        using hin unfolding hintikka_def by blast
      then show ‹?eval (Neg x)›
        using Or wf ‹closed 0 (Or A B)› by simp
    qed
  next
    case (Impl A B)
    then show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ H› and ‹closed 0 x›
      then have ‹Impl A B ∈ H› and ‹closed 0 (Impl A B)›
        using Impl by simp_all
      then have ‹Neg A ∈ H ∨ B ∈ H›
        using hin unfolding hintikka_def by blast
      then show ‹?eval x›
        using Impl wf ‹closed 0 (Impl A B)› by fastforce
    next
      assume ‹Neg x ∈ H› and ‹closed 0 x›
      then have ‹Neg (Impl A B) ∈ H› and ‹closed 0 (Impl A B)›
        using Impl by simp_all
      then have ‹A ∈ H ∧ Neg B ∈ H›
        using hin unfolding hintikka_def by blast
      then show ‹?eval (Neg x)›
        using Impl wf ‹closed 0 (Impl A B)› by simp
    qed
  next
    case (Forall P)
    then show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ H› and ‹closed 0 x›
      have ‹∀z. eval (e⟨0:z⟩) HApp (λa ts. Pred a (terms_of_hterms ts) ∈ H) P›
      proof (rule allI)
        fix z
        from ‹x ∈ H› and ‹closed 0 x›
        have ‹Forall P ∈ H› and ‹closed 0 (Forall P)›
          using Forall by simp_all
        then have *: ‹∀P t. closedt 0 t ⟶ Forall P ∈ H ⟶ P[t/0] ∈ H›
          using hin unfolding hintikka_def by blast
        from ‹closed 0 (Forall P)›
        have ‹closed (Suc 0) P› by simp

        have ‹(P[term_of_hterm z/0], Forall P) ∈ measure size_form ⟶
              (P[term_of_hterm z/0] ∈ H ⟶ closed 0 (P[term_of_hterm z/0]) ⟶
              ?eval (P[term_of_hterm z/0]))›
          using Forall wf by blast
        then show ‹eval (e⟨0:z⟩) HApp (λa ts. Pred a (terms_of_hterms ts) ∈ H) P›
          using * ‹Forall P ∈ H› ‹closed (Suc 0) P› by simp
      qed
      then show ‹?eval x›
        using Forall by simp
    next
      assume ‹Neg x ∈ H› and ‹closed 0 x›
      then have ‹Neg (Forall P) ∈ H›
        using Forall by simp
      then have ‹∃t. closedt 0 t ∧ Neg (P[t/0]) ∈ H›
        using Forall hin unfolding hintikka_def by blast
      then obtain t where *: ‹closedt 0 t ∧ Neg (P[t/0]) ∈ H›
        by blast
      then have ‹closed 0 (P[t/0])›
        using Forall ‹closed 0 x› by simp

      have ‹(subst P t 0, Forall P) ∈ measure size_form ⟶
              (Neg (subst P t 0) ∈ H ⟶ closed 0 (subst P t 0) ⟶
              ?eval (Neg (subst P t 0)))›
        using Forall wf by blast
      then have ‹?eval (Neg (P[t/0]))›
        using Forall * ‹closed 0 (P[t/0])› by simp
      then have ‹∃z. ¬ eval (e⟨0:z⟩) HApp (λa ts. Pred a (terms_of_hterms ts) ∈ H) P›
        by auto
      then show ‹?eval (Neg x)›
        using Forall by simp
    qed
  next
    case (Exists P)
    then show ?thesis
    proof (intro conjI impI allI)
      assume ‹x ∈ H› and ‹closed 0 x›
      then have ‹∃t. closedt 0 t ∧ (P[t/0]) ∈ H›
        using Exists hin unfolding hintikka_def by blast
      then obtain t where *: ‹closedt 0 t ∧ (P[t/0]) ∈ H›
        by blast
      then have ‹closed 0 (P[t/0])›
        using Exists ‹closed 0 x› by simp

      have ‹(subst P t 0, Exists P) ∈ measure size_form ⟶
              ((subst P t 0) ∈ H ⟶ closed 0 (subst P t 0) ⟶
              ?eval (subst P t 0))›
        using Exists wf by blast
      then have ‹?eval (P[t/0])›
        using Exists * ‹closed 0 (P[t/0])› by simp
      then have ‹∃z. eval (e⟨0:z⟩) HApp (λa ts. Pred a (terms_of_hterms ts) ∈ H) P›
        by auto
      then show ‹?eval x›
        using Exists by simp
    next
      assume ‹Neg x ∈ H› and ‹closed 0 x›
      have ‹∀z. ¬ eval (e⟨0:z⟩) HApp (λa ts. Pred a (terms_of_hterms ts) ∈ H) P›
      proof (rule allI)
        fix z
        from ‹Neg x ∈ H› and ‹closed 0 x›
        have ‹Neg (Exists P) ∈ H› and ‹closed 0 (Neg (Exists P))›
          using Exists by simp_all
        then have *: ‹∀P t. closedt 0 t ⟶ Neg (Exists P) ∈ H ⟶ Neg (P[t/0]) ∈ H›
          using hin unfolding hintikka_def by blast
        from ‹closed 0 (Neg (Exists P))›
        have ‹closed (Suc 0) P› by simp

        have ‹(P[term_of_hterm z/0], Exists P) ∈ measure size_form ⟶
              (Neg (P[term_of_hterm z/0]) ∈ H ⟶ closed 0 (P[term_of_hterm z/0]) ⟶
              ?eval (Neg (P[term_of_hterm z/0])))›
          using Exists wf by blast
        then show ‹¬ eval (e⟨0:z⟩) HApp (λa ts. Pred a (terms_of_hterms ts) ∈ H) P›
          using * ‹Neg (Exists P) ∈ H› ‹closed (Suc 0) P› by simp
      qed
      then show ‹?eval (Neg x)›
        using Exists by simp
    qed
  qed
qed

text ‹
Using the maximality of @{term ‹Extend S C f›}, we can show
that @{term ‹Extend S C f›} yields Hintikka sets:
›

lemma Exists_in_extend:
  assumes ‹extend S C f n ∪ {f n} ∈ C› (is ‹?S' ∈ C›)
    and ‹Exists P = f n›
  shows ‹P[(App (SOME k. k ∉ (⋃p ∈ extend S C f n ∪ {f n}. params p)) [])/0] ∈
          extend S C f (Suc n)›
    (is ‹subst P ?t 0 ∈ extend S C f (Suc n)›)
proof -
  have ‹∃p. f n = Exists p›
    using ‹Exists P = f n› by metis
  then have ‹extend S C f (Suc n) = (?S' ∪ {(dest_Exists (f n))[?t/0]})›
    using ‹?S' ∈ C› by simp
  also have ‹… = (?S' ∪ {(dest_Exists (Exists P))[?t/0]})›
    using ‹Exists P = f n› by simp
  also have ‹… = (?S' ∪ {P[?t/0]})›
    by simp
  finally show ?thesis
    by blast
qed

lemma Neg_Forall_in_extend:
  assumes ‹extend S C f n ∪ {f n} ∈ C› (is ‹?S' ∈ C›)
    and ‹Neg (Forall P) = f n›
  shows ‹Neg (P[(App (SOME k. k ∉ (⋃p ∈ extend S C f n ∪ {f n}. params p)) [])/0])  ∈
          extend S C f (Suc n)›
    (is ‹Neg (subst P ?t 0) ∈ extend S C f (Suc n)›)
proof -
  have ‹f n ≠ Exists P›
    using ‹Neg (Forall P) = f n› by auto

  have ‹∃p. f n = Neg (Forall p)›
    using ‹Neg (Forall P) = f n› by metis
  then have ‹extend S C f (Suc n) = (?S' ∪ {Neg (dest_Forall (dest_Neg (f n))[?t/0])})›
    using ‹?S' ∈ C› ‹f n ≠ Exists P› by auto
  also have ‹… = (?S' ∪ {Neg (dest_Forall (dest_Neg (Neg (Forall P)))[?t/0])})›
    using ‹Neg (Forall P) = f n› by simp
  also have ‹… = (?S' ∪ {Neg (P[?t/0])})›
    by simp
  finally show ?thesis
    by blast
qed

theorem extend_hintikka:
  assumes fin_ch: ‹finite_char C›
    and infin_p: ‹infinite (- (⋃p ∈ S. params p))›
    and surj: ‹∀y. ∃n. y = f n›
    and altc: ‹alt_consistency C›
    and ‹S ∈ C›
  shows ‹hintikka (Extend S C f)› (is ‹hintikka ?H›)
  unfolding hintikka_def
proof (intro allI impI conjI)
  have ‹maximal ?H C›
    by (simp add: extend_maximal fin_ch surj)

  have ‹?H ∈ C›
    using Extend_in_C assms by blast

  have ‹∀S' ∈ C. ?H ⊆ S' ⟶ ?H = S'›
    using ‹maximal ?H C›
    unfolding maximal_def by blast

  { fix p ts
    show ‹¬ (Pred p ts ∈ ?H ∧ Neg (Pred p ts) ∈ ?H)›
      using ‹?H ∈ C› altc unfolding alt_consistency_def by fast }

  show ‹FF ∉ ?H›
    using ‹?H ∈ C› altc unfolding alt_consistency_def by blast

  show ‹Neg TT ∉ ?H›
    using ‹?H ∈ C› altc unfolding alt_consistency_def by blast

  { fix Z
    assume ‹Neg (Neg Z) ∈ ?H›
    then have ‹?H ∪ {Z} ∈ C›
      using ‹?H ∈ C› altc unfolding alt_consistency_def by fast
    then show ‹Z ∈ ?H›
      using ‹maximal ?H C› unfolding maximal_def by fast }

  { fix A B
    assume ‹And A B ∈ ?H›
    then have ‹?H ∪ {A, B} ∈ C›
      using ‹?H ∈ C› altc unfolding alt_consistency_def by fast
    then show ‹A ∈ ?H› and ‹B ∈ ?H›
      using ‹maximal ?H C› unfolding maximal_def by fast+ }

  { fix A B
    assume ‹Neg (Or A B) ∈ ?H›
    then have ‹?H ∪ {Neg A, Neg B} ∈ C›
      using ‹?H ∈ C› altc unfolding alt_consistency_def by fast
    then show ‹Neg A ∈ ?H› and ‹Neg B ∈ ?H›
      using ‹maximal ?H C› unfolding maximal_def by fast+ }

  { fix A B
    assume ‹Neg (Impl A B) ∈ ?H›
    then have ‹?H ∪ {A, Neg B} ∈ C›
      using ‹?H ∈ C› altc unfolding alt_consistency_def by blast
    then show ‹A ∈ ?H› and ‹Neg B ∈ ?H›
      using ‹maximal ?H C› unfolding maximal_def by fast+ }

  { fix A B
    assume ‹Or A B ∈ ?H›
    then have ‹?H ∪ {A} ∈ C ∨ ?H ∪ {B} ∈ C›
      using ‹?H ∈ C› altc unfolding alt_consistency_def by fast
    then show ‹A ∈ ?H ∨ B ∈ ?H›
      using ‹maximal ?H C› unfolding maximal_def by fast }

  { fix A B
    assume ‹Neg (And A B) ∈ ?H›
    then have ‹?H ∪ {Neg A} ∈ C ∨ ?H ∪ {Neg B} ∈ C›
      using ‹?H ∈ C› altc unfolding alt_consistency_def by simp
    then show ‹Neg A ∈ ?H ∨ Neg B ∈ ?H›
      using ‹maximal ?H C› unfolding maximal_def by fast }

  { fix A B
    assume ‹Impl A B ∈ ?H›
    then have ‹?H ∪ {Neg A} ∈ C ∨ ?H ∪ {B} ∈ C›
      using ‹?H ∈ C› altc unfolding alt_consistency_def by simp
    then show ‹Neg A ∈ ?H ∨ B ∈ ?H›
      using ‹maximal ?H C› unfolding maximal_def by fast }

  { fix P and t :: ‹nat term›
    assume ‹Forall P ∈ ?H› and ‹closedt 0 t›
    then have ‹?H ∪ {P[t/0]} ∈ C›
      using ‹?H ∈ C› altc unfolding alt_consistency_def by blast
    then show ‹P[t/0] ∈ ?H›
      using ‹maximal ?H C› unfolding maximal_def by fast }

  { fix P and t :: ‹nat term›
    assume ‹Neg (Exists P) ∈ ?H› and ‹closedt 0 t›
    then have ‹?H ∪ {Neg (P[t/0])} ∈ C›
      using ‹?H ∈ C› altc unfolding alt_consistency_def by blast
    then show ‹Neg (P[t/0]) ∈ ?H›
      using ‹maximal ?H C› unfolding maximal_def by fast }

  { fix P
    assume ‹Exists P ∈ ?H›
    obtain n where *: ‹Exists P = f n›
      using surj by blast

    let ?t = ‹App (SOME k. k ∉ (⋃p ∈ extend S C f n ∪ {f n}. params p)) []›
    have ‹closedt 0 ?t› by simp

    have ‹Exists P ∈ (⋃n. extend S C f n)›
      using ‹Exists P ∈ ?H› Extend_def by blast
    then have ‹extend S C f n ∪ {f n} ⊆ (⋃n. extend S C f n)›
      using * by (simp add: UN_upper)
    then have ‹extend S C f n ∪ {f n} ∈ C›
      using Extend_def ‹Extend S C f ∈ C› fin_ch finite_char_closed
      unfolding subset_closed_def by metis
    then have ‹P[?t/0] ∈ extend S C f (Suc n)›
      using * Exists_in_extend by blast
    then have ‹P[?t/0] ∈ ?H›
      using Extend_def by blast
    then show ‹∃t. closedt 0 t ∧ P[t/0] ∈ ?H›
      using ‹closedt 0 ?t› by blast }

  { fix P
    assume ‹Neg (Forall P) ∈ ?H›
    obtain n where *: ‹Neg (Forall P) = f n›
      using surj by blast

    let ?t = ‹App (SOME k. k ∉ (⋃p ∈ extend S C f n ∪ {f n}. params p)) []›
    have ‹closedt 0 ?t› by simp

    have ‹Neg (Forall P) ∈ (⋃n. extend S C f n)›
      using ‹Neg (Forall P) ∈ ?H› Extend_def by blast
    then have ‹extend S C f n ∪ {f n} ⊆ (⋃n. extend S C f n)›
      using * by (simp add: UN_upper)
    then have ‹extend S C f n ∪ {f n} ∈ C›
      using Extend_def ‹Extend S C f ∈ C› fin_ch finite_char_closed
      unfolding subset_closed_def by metis
    then have ‹Neg (P[?t/0]) ∈ extend S C f (Suc n)›
      using * Neg_Forall_in_extend by blast
    then have ‹Neg (P[?t/0]) ∈ ?H›
      using Extend_def by blast
    then show ‹∃t. closedt 0 t ∧ Neg (P[t/0]) ∈ ?H›
      using ‹closedt 0 ?t› by blast }
qed

subsection ‹Model existence theorem›

text ‹
\label{sec:model-existence}
Since the result of extending ‹S› is a superset of ‹S›,
it follows that each consistent set ‹S› has a Herbrand model:
›

lemma hintikka_Extend_S:
  assumes ‹consistency C› and ‹S ∈ C›
    and ‹infinite (- (⋃p ∈ S. params p))›
  shows ‹hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)›
    (is ‹hintikka (Extend S ?C' from_nat)›)
proof -
  have ‹finite_char ?C'›
    using finite_char by blast
  moreover have ‹∀y. y = from_nat (to_nat y)›
    by simp
  then have ‹∀y. ∃n. y = from_nat n›
    by blast
  moreover have ‹alt_consistency ?C'›
    using alt_consistency close_closed close_consistency ‹consistency C›
      finite_alt_consistency mk_alt_consistency_closed
    by blast
  moreover have ‹S ∈ close C›
    using close_subset ‹S ∈ C› by blast
  then have ‹S ∈ mk_alt_consistency (close C)›
    using mk_alt_consistency_subset by blast
  then have ‹S ∈ ?C'›
    using close_closed finite_char_subset mk_alt_consistency_closed by blast
  ultimately show ?thesis
    using extend_hintikka ‹infinite (- (⋃p ∈ S. params p))›
    by metis
qed

theorem model_existence:
  assumes ‹consistency C›
    and ‹S ∈ C›
    and ‹infinite (- (⋃p ∈ S. params p))›
    and ‹p ∈ S›
    and ‹closed 0 p›
  shows ‹eval e HApp (λa ts. Pred a (terms_of_hterms ts) ∈ Extend S
        (mk_finite_char (mk_alt_consistency (close C))) from_nat) p›
  using assms hintikka_model hintikka_Extend_S Extend_subset
  by blast

subsection ‹Completeness for Natural Deduction›

text ‹
Thanks to the model existence theorem, we can now show the completeness
of the natural deduction calculus introduced in \secref{sec:proof-calculus}.
In order for the model existence theorem to be applicable, we have to prove
that the set of sets that are consistent with respect to ‹⊢› is a
consistency property:
›

theorem deriv_consistency:
  assumes inf_param: ‹infinite (UNIV :: 'a set)›
  shows ‹consistency {S::('a, 'b) form set. ∃G. S = set G ∧ ¬ G ⊢ FF}›
  unfolding consistency_def
proof (intro conjI allI impI notI)
  fix S :: ‹('a, 'b) form set›
  assume ‹S ∈ {set G | G. ¬ G ⊢ FF}› (is ‹S ∈ ?C›)
  then obtain G :: ‹('a, 'b) form list›
    where *: ‹S = set G› and ‹¬ G ⊢ FF›
    by blast

  { fix p ts
    assume ‹Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S›
    then have ‹G ⊢ Pred p ts› and ‹G ⊢ Neg (Pred p ts)›
      using Assum * by blast+
    then have ‹G ⊢ FF›
      using NegE by blast
    then show False
      using ‹¬ G ⊢ FF› by blast }

  { assume ‹FF ∈ S›
    then have ‹G ⊢ FF›
      using Assum * by blast
    then show False
      using ‹¬ G ⊢ FF› by blast }

  { assume ‹Neg TT ∈ S›
    then have ‹G ⊢ Neg TT›
      using Assum * by blast
    moreover have ‹G ⊢ TT›
      using TTI by blast
    ultimately have ‹G ⊢ FF›
      using NegE by blast
    then show False
      using ‹¬ G ⊢ FF› by blast }

  { fix Z
    assume ‹Neg (Neg Z) ∈ S›
    then have ‹G ⊢ Neg (Neg Z)›
      using Assum * by blast

    { assume ‹Z # G ⊢ FF›
      then have ‹G ⊢ Neg Z›
        using NegI by blast
      then have ‹G ⊢ FF›
        using NegE ‹G ⊢ Neg (Neg Z)› by blast
      then have False
        using ‹¬ G ⊢ FF› by blast }
    then have ‹¬ Z # G ⊢ FF›
      by blast
    moreover have ‹S ∪ {Z} = set (Z # G)›
      using * by simp
    ultimately show ‹S ∪ {Z} ∈ ?C›
      by blast }

  { fix A B
    assume ‹And A B ∈ S›
    then have ‹G ⊢ And A B›
      using Assum * by blast
    then have ‹G ⊢ A› and ‹G ⊢ B›
      using AndE1 AndE2 by blast+

    { assume ‹A # B # G ⊢ FF›
      then have ‹B # G ⊢ Neg A›
        using NegI by blast
      then have ‹G ⊢ Neg A›
        using cut ‹G ⊢ B› by blast
      then have ‹G ⊢ FF›
        using NegE ‹G ⊢ A› by blast
      then have False
        using ‹¬ G ⊢ FF› by blast }
    then have ‹¬ A # B # G ⊢ FF›
      by blast
    moreover have ‹S ∪ {A, B} = set (A # B # G)›
      using * by simp
    ultimately show ‹S ∪ {A, B} ∈ ?C›
      by blast }

  { fix A B
    assume ‹Neg (Or A B) ∈ S›
    then have ‹G ⊢ Neg (Or A B)›
      using Assum * by blast

    have ‹A # Neg B # G ⊢ A›
      by (simp add: Assum)
    then have ‹A # Neg B # G ⊢ Or A B›
      using OrI1 by blast
    moreover have ‹A # Neg B # G ⊢ Neg (Or A B)›
      using * ‹Neg (Or A B) ∈ S› by (simp add: Assum)
    ultimately have ‹A # Neg B # G ⊢ FF›
      using NegE ‹A # Neg B # G ⊢ Neg (Or A B)› by blast
    then have ‹Neg B # G ⊢ Neg A›
      using NegI by blast

    have ‹B # G ⊢ B›
      by (simp add: Assum)
    then have ‹B # G ⊢ Or A B›
      using OrI2 by blast
    moreover have ‹B # G ⊢ Neg (Or A B)›
      using * ‹Neg (Or A B) ∈ S› by (simp add: Assum)
    ultimately have ‹B # G ⊢ FF›
      using NegE ‹B # G ⊢ Neg (Or A B)› by blast
    then have ‹G ⊢ Neg B›
      using NegI by blast

    { assume ‹Neg A # Neg B # G ⊢ FF›
      then have ‹Neg B # G ⊢ Neg (Neg A)›
        using NegI by blast
      then have ‹Neg B # G ⊢ FF›
        using NegE ‹Neg B # G ⊢ Neg A› by blast
      then have ‹G ⊢ FF›
        using cut ‹G ⊢ Neg B› by blast
      then have False
        using ‹¬ G ⊢ FF› by blast }
    then have ‹¬ Neg A # Neg B # G ⊢ FF›
      by blast
    moreover have ‹S ∪ {Neg A, Neg B} = set (Neg A # Neg B # G)›
      using * by simp
    ultimately show ‹S ∪ {Neg A, Neg B} ∈ ?C›
      by blast }

  { fix A B
    assume ‹Neg (Impl A B) ∈ S›

    have ‹A # Neg A # Neg B # G ⊢ A›
      by (simp add: Assum)
    moreover have ‹A # Neg A # Neg B # G ⊢ Neg A›
      by (simp add: Assum)
    ultimately have ‹A # Neg A # Neg B # G ⊢ FF›
      using NegE by blast
    then have ‹A # Neg A # Neg B # G ⊢ B›
      using FFE by blast
    then have ‹Neg A # Neg B # G ⊢ Impl A B›
      using ImplI by blast
    moreover have ‹Neg A # Neg B # G ⊢ Neg (Impl A B)›
      using * ‹Neg (Impl A B) ∈ S› by (simp add: Assum)
    ultimately have ‹Neg A # Neg B # G ⊢ FF›
      using NegE by blast
    then have ‹Neg B # G ⊢ A›
      using Class by blast

    have ‹A # B # G ⊢ B›
      by (simp add: Assum)
    then have ‹B # G ⊢ Impl A B›
      using ImplI by blast
    moreover have ‹B # G ⊢ Neg (Impl A B)›
      using * ‹Neg (Impl A B) ∈ S› by (simp add: Assum)
    ultimately have ‹B # G ⊢ FF›
      using NegE by blast
    then have ‹G ⊢ Neg B›
      using NegI by blast

    { assume ‹A # Neg B # G ⊢ FF›
      then have ‹Neg B # G ⊢ Neg A›
        using NegI by blast
      then have ‹Neg B # G ⊢ FF›
        using NegE ‹Neg B # G ⊢ A› by blast
      then have ‹G ⊢ FF›
        using cut ‹G ⊢ Neg B› by blast
      then have False
        using ‹¬ G ⊢ FF›
        by blast }
    then have ‹¬ A # Neg B # G ⊢ FF›
      by blast
    moreover have ‹{A, Neg B} ∪ S = set (A # Neg B # G)›
      using * by simp
    ultimately show ‹S ∪ {A, Neg B} ∈ ?C›
      by blast }

  { fix A B
    assume ‹Or A B ∈ S›
    then have ‹G ⊢ Or A B›
      using * Assum by blast

    { assume ‹(∀G'. set G' = S ∪ {A} ⟶ G' ⊢ FF)›
        and ‹(∀G'. set G' = S ∪ {B} ⟶ G' ⊢ FF)›
      then have ‹A # G ⊢ FF› and ‹B # G ⊢ FF›
        using * by simp_all
      then have ‹G ⊢ FF›
        using OrE ‹G ⊢ Or A B› by blast
      then have False
        using ‹¬ G ⊢ FF› by blast }
    then show ‹S ∪ {A} ∈ ?C ∨ S ∪ {B} ∈ ?C›
      by blast }

  { fix A B
    assume ‹Neg (And A B) ∈ S›

    let ?x = ‹Or (Neg A) (Neg B)›

    have ‹B # A # Neg ?x # G ⊢ A› and ‹B # A # Neg ?x # G ⊢ B›
      by (simp_all add: Assum)
    then have ‹B # A # Neg ?x # G ⊢ And A B›
      using AndI by blast
    moreover have ‹B # A # Neg ?x # G ⊢ Neg (And A B)›
      using * ‹Neg (And A B) ∈ S› by (simp add: Assum)
    ultimately have ‹B # A # Neg ?x # G ⊢ FF›
      using NegE by blast
    then have ‹A # Neg ?x # G ⊢ Neg B›
      using NegI by blast
    then have ‹A # Neg ?x # G ⊢ ?x›
      using OrI2 by blast
    moreover have ‹A # Neg ?x # G ⊢ Neg ?x›
      by (simp add: Assum)
    ultimately have ‹A # Neg ?x # G ⊢ FF›
      using NegE by blast
    then have ‹Neg ?x # G ⊢ Neg A›
      using NegI by blast
    then have ‹Neg ?x # G ⊢ ?x›
      using OrI1 by blast
    then have ‹G ⊢ Or (Neg A) (Neg B)›
      using Class' by blast

    { assume ‹(∀G'. set G' = S ∪ {Neg A} ⟶ G' ⊢ FF)›
        and ‹(∀G'. set G' = S ∪ {Neg B} ⟶ G' ⊢ FF)›
      then have ‹Neg A # G ⊢ FF› and ‹Neg B # G ⊢ FF›
        using * by simp_all
      then have ‹G ⊢ FF›
        using OrE ‹G ⊢ Or (Neg A) (Neg B)› by blast
      then have False
        using ‹¬ G ⊢ FF› by blast }
    then show ‹S ∪ {Neg A} ∈ ?C ∨ S ∪ {Neg B} ∈ ?C›
      by blast }

  { fix A B
    assume ‹Impl A B ∈ S›

    let ?x = ‹Or (Neg A) B›

    have ‹A # Neg ?x # G ⊢ A›
      by (simp add: Assum)
    moreover have ‹A # Neg ?x # G ⊢ Impl A B›
      using * ‹Impl A B ∈ S› by (simp add: Assum)
    ultimately have ‹A # Neg ?x # G ⊢ B›
      using ImplE by blast
    then have ‹A # Neg ?x # G ⊢ ?x›
      using OrI2 by blast
    moreover have ‹A # Neg ?x # G ⊢ Neg ?x›
      by (simp add: Assum)
    ultimately have ‹A # Neg ?x # G ⊢ FF›
      using NegE by blast
    then have ‹Neg ?x # G ⊢ Neg A›
      using NegI by blast
    then have ‹Neg ?x # G ⊢ ?x›
      using OrI1 by blast
    then have ‹G ⊢ Or (Neg A) B›
      using Class' by blast

    { assume ‹(∀G'. set G' = S ∪ {Neg A} ⟶ G' ⊢ FF)›
        and ‹(∀G'. set G' = S ∪ {B} ⟶ G' ⊢ FF)›
      then have ‹Neg A # G ⊢ FF› and ‹B # G ⊢ FF›
        using * by simp_all
      then have ‹G ⊢ FF›
        using OrE ‹G ⊢ Or (Neg A) B› by blast
      then have False
        using ‹¬ G ⊢ FF› by blast }
    then show ‹S ∪ {Neg A} ∈ ?C ∨ S ∪ {B} ∈ ?C›
      by blast }

  { fix P and t :: ‹'a term›
    assume ‹closedt 0 t› and ‹Forall P ∈ S›
    then have ‹G ⊢ Forall P›
      using Assum * by blast
    then have ‹G ⊢ P[t/0]›
      using ForallE by blast

    { assume ‹P[t/0] # G ⊢ FF›
      then have ‹G ⊢ FF›
        using cut ‹G ⊢ P[t/0]› by blast
      then have False
        using ‹¬ G ⊢ FF› by blast }
    then have ‹¬ P[t/0] # G ⊢ FF›
      by blast
    moreover have ‹S ∪ {P[t/0]} = set (P[t/0] # G)›
      using * by simp
    ultimately show ‹S ∪ {P[t/0]} ∈ ?C›
      by blast }

  { fix P and t :: ‹'a term›
    assume ‹closedt 0 t› and ‹Neg (Exists P) ∈ S›
    then have ‹G ⊢ Neg (Exists P)›
      using Assum * by blast
    then have ‹P[t/0] ∈ set (P[t/0] # G)›
      by (simp add: Assum)
    then have ‹P[t/0] # G ⊢ P[t/0]›
      using Assum by blast
    then have ‹P[t/0] # G ⊢ Exists P›
      using ExistsI by blast
    moreover have ‹P[t/0] # G ⊢ Neg (Exists P)›
      using * ‹Neg (Exists P) ∈ S› by (simp add: Assum)
    ultimately have ‹P[t/0] # G ⊢ FF›
      using NegE by blast
    then have ‹G ⊢ Neg (P[t/0])›
      using NegI by blast

    { assume ‹Neg (P[t/0]) # G ⊢ FF›
      then have ‹G ⊢ FF›
        using cut ‹G ⊢ Neg (P[t/0])› by blast
      then have False
        using ‹¬ G ⊢ FF› by blast }
    then have ‹¬ Neg (P[t/0]) # G ⊢ FF›
      by blast
    moreover have ‹S ∪ {Neg (P[t/0])} = set (Neg (P[t/0]) # G)›
      using * by simp
    ultimately show ‹S ∪ {Neg (P[t/0])} ∈ ?C›
      by blast }

  { fix P
    assume ‹Exists P ∈ S›
    then have ‹G ⊢ Exists P›
      using * Assum by blast

    have ‹finite ((⋃p ∈ set G. params p) ∪ params P)›
      by simp
    then have ‹infinite (- ((⋃p ∈ set G. params p) ∪ params P))›
      using inf_param Diff_infinite_finite finite_compl by blast
    then have ‹infinite (- ((⋃p ∈ set G. params p) ∪ params P))›
      by (simp add: Compl_eq_Diff_UNIV)
    then obtain x where **: ‹x ∈ - ((⋃p ∈ set G. params p) ∪ params P)›
      using infinite_imp_nonempty by blast

    { assume ‹P[App x []/0] # G ⊢ FF›
      moreover have ‹list_all (λp. x ∉ params p) G›
        using ** by (simp add: list_all_iff)
      moreover have ‹x ∉ params P›
        using ** by simp
      moreover have ‹x ∉ params FF›
        by simp
      ultimately have ‹G ⊢ FF›
        using ExistsE ‹G ⊢ Exists P› by fast
      then have False
        using ‹¬ G ⊢ FF›
        by blast}
    then have ‹¬ P[App x []/0] # G ⊢ FF›
      by blast
    moreover have ‹S ∪ {P[App x []/0]} = set (P[App x []/0] # G)›
      using * by simp
    ultimately show ‹∃x. S ∪ {P[App x []/0]} ∈ ?C›
      by blast }

  { fix P
    assume ‹Neg (Forall P) ∈ S›
    then have ‹G ⊢ Neg (Forall P)›
      using * Assum by blast

    have ‹finite ((⋃p ∈ set G. params p) ∪ params P)›
      by simp
    then have ‹infinite (- ((⋃p ∈ set G. params p) ∪ params P))›
      using inf_param Diff_infinite_finite finite_compl by blast
    then have ‹infinite (- ((⋃p ∈ set G. params p) ∪ params P))›
      by (simp add: Compl_eq_Diff_UNIV)
    then obtain x where **: ‹x ∈ - ((⋃p ∈ set G. params p) ∪ params P)›
      using infinite_imp_nonempty by blast

    let ?x = ‹Neg (Exists (Neg P))›

    have ‹Neg (P[App x []/0]) # ?x # G ⊢ Neg P[App x []/0]›
      by (simp add: Assum)
    then have ‹Neg (P[App x []/0]) # ?x # G ⊢ Exists (Neg P)›
      using ExistsI by blast
    moreover have ‹Neg (P[App x []/0]) # ?x # G ⊢ ?x›
      by (simp add: Assum)
    ultimately have ‹Neg (P[App x []/0]) # ?x # G ⊢ FF›
      using NegE by blast
    then have ‹?x # G ⊢ P[App x []/0]›
      using Class by blast
    moreover have ‹list_all (λp. x ∉ params p) (?x # G)›
      using ** by (simp add: list_all_iff)
    moreover have ‹x ∉ params P›
      using ** by simp
    ultimately have ‹?x # G ⊢ Forall P›
      using ForallI by fast
    moreover have ‹?x # G ⊢ Neg (Forall P)›
      using * ‹Neg (Forall P) ∈ S› by (simp add: Assum)
    ultimately have ‹?x # G ⊢ FF›
      using NegE by blast
    then have ‹G ⊢ Exists (Neg P)›
      using Class by blast

    { assume ‹Neg (P[App x []/0]) # G ⊢ FF›
      moreover have ‹list_all (λp. x ∉ params p) G›
        using ** by (simp add: list_all_iff)
      moreover have ‹x ∉ params P›
        using ** by simp
      moreover have ‹x ∉ params FF›
        by simp
      ultimately have ‹G ⊢ FF›
        using ExistsE ‹G ⊢ Exists (Neg P)› by fastforce
      then have False
        using ‹¬ G ⊢ FF›
        by blast}
    then have ‹¬ Neg (P[App x []/0]) # G ⊢ FF›
      by blast
    moreover have ‹S ∪ {Neg (P[App x []/0])} = set (Neg (P[App x []/0]) # G)›
      using * by simp
    ultimately show ‹∃x. S ∪ {Neg (P[App x []/0])} ∈ ?C›
      by blast }
qed

text ‹
Hence, by contradiction, we have completeness of natural deduction:
›

theorem natded_complete:
  assumes ‹closed 0 p›
    and ‹list_all (closed 0) ps›
    and mod: ‹∀e f g. e,(f :: nat ⇒ nat hterm list ⇒ nat hterm),
              (g :: nat ⇒ nat hterm list ⇒ bool),ps ⊨ p›
  shows ‹ps ⊢ p›
proof (rule Class, rule ccontr)
  fix e
  assume ‹¬ Neg p # ps ⊢ FF›

  let ?S = ‹set (Neg p # ps)›
  let ?C = ‹{set (G :: (nat, nat) form list) | G. ¬ G ⊢ FF}›
  let ?f = HApp
  let ?g = ‹(λa ts. Pred a (terms_of_hterms ts) ∈ Extend ?S
              (mk_finite_char (mk_alt_consistency (close ?C))) from_nat)›

  from ‹list_all (closed 0) ps›
  have ‹∀p ∈ set ps. closed 0 p›
    by (simp add: list_all_iff)

  { fix x
    assume ‹x ∈ ?S›
    moreover have ‹consistency ?C›
      using deriv_consistency by blast
    moreover have ‹?S ∈ ?C›
      using ‹¬ Neg p # ps ⊢ FF› by blast
    moreover have ‹infinite (- (⋃p ∈ ?S. params p))›
      by (simp add: Compl_eq_Diff_UNIV)
    moreover note ‹closed 0 p› ‹∀p ∈ set ps. closed 0 p› ‹x ∈ ?S›
    then have ‹closed 0 x› by auto
    ultimately have ‹eval e ?f ?g x›
      using model_existence by blast }
  then have ‹list_all (eval e ?f ?g) (Neg p # ps)›
    by (simp add: list_all_iff)
  moreover have ‹eval e ?f ?g (Neg p)›
    using calculation by simp
  moreover have ‹list_all (eval e ?f ?g) ps›
    using calculation by simp
  then have ‹eval e ?f ?g p›
    using mod unfolding model_def by blast
  ultimately show False by simp
qed

section ‹L\"owenheim-Skolem theorem›

text ‹
Another application of the model existence theorem presented in \secref{sec:model-existence}
is the L\"owenheim-Skolem theorem. It says that a set of formulae that is satisfiable in an
{\em arbitrary model} is also satisfiable in a {\em Herbrand model}. The main idea behind the
proof is to show that satisfiable sets are consistent, hence they must be satisfiable in a
Herbrand model.
›

theorem sat_consistency:
  ‹consistency {S. infinite (- (⋃p ∈ S. params p)) ∧ (∃f. ∀(p::('a, 'b)form) ∈ S. eval e f g p)}›
  unfolding consistency_def
proof (intro allI impI conjI)
  let ?C = ‹{S. infinite (- (⋃p ∈ S. params p)) ∧ (∃f. ∀p ∈ S. eval e f g p)}›

  fix S :: ‹('a, 'b) form set›
  assume ‹S ∈ ?C›
  then have inf_params: ‹infinite (- (⋃p ∈ S. params p))›
    and ‹∃f. ∀p ∈ S. eval e f g p›
    by blast+
  then obtain f where *: ‹∀x ∈ S. eval e f g x› by blast

  { fix p ts
    show ‹¬ (Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S)›
    proof
      assume ‹Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S›
      then have ‹eval e f g (Pred p ts) ∧ eval e f g (Neg (Pred p ts))›
        using * by blast
      then show False by simp
    qed }

  show ‹FF ∉ S›
    using * by fastforce

  show ‹Neg TT ∉ S›
    using * by fastforce

  { fix Z
    assume ‹Neg (Neg Z) ∈ S›
    then have ‹∀x ∈ S ∪ {Neg (Neg Z)}. eval e f g x›
      using * by blast
    then have ‹∀x ∈ S ∪ {Z}. eval e f g x›
      by simp
    moreover have ‹infinite (- (⋃p ∈ S ∪ {Z}. params p))›
      using inf_params by simp
    ultimately show ‹S ∪ {Z} ∈ ?C›
      by blast }

  { fix A B
    assume ‹And A B ∈ S›
    then have ‹∀x ∈ S ∪ {And A B}. eval e f g x›
      using * by blast
    then have ‹∀x ∈ S ∪ {A, B}. eval e f g x›
      by simp
    moreover have ‹infinite (- (⋃p ∈ S ∪ {A, B}. params p))›
      using inf_params by simp
    ultimately show ‹S ∪ {A, B} ∈ ?C›
      by blast }

  { fix A B
    assume ‹Neg (Or A B) ∈ S›
    then have ‹∀x ∈ S ∪ {Neg (Or A B)}. eval e f g x›
      using * by blast
    then have ‹∀x ∈ S ∪ {Neg A, Neg B}. eval e f g x›
      by simp
    moreover have ‹infinite (- (⋃p ∈ S ∪ {Neg A, Neg B}. params p))›
      using inf_params by simp
    ultimately show ‹S ∪ {Neg A, Neg B} ∈ ?C›
      by blast }

  { fix A B
    assume ‹Neg (Impl A B) ∈ S›
    then have ‹∀x ∈ S ∪ {Neg (Impl A B)}. eval e f g x›
      using * by blast
    then have ‹∀x ∈ S ∪ {A, Neg B}. eval e f g x›
      by simp
    moreover have ‹infinite (- (⋃p ∈ S ∪ {A, Neg B}. params p))›
      using inf_params by simp
    ultimately show ‹S ∪ {A, Neg B} ∈ ?C›
      by blast }

  { fix A B
    assume ‹Or A B ∈ S›
    then have ‹∀x ∈ S ∪ {Or A B}. eval e f g x›
      using * by blast
    then have ‹(∀x ∈ S ∪ {A}. eval e f g x) ∨
               (∀x ∈ S ∪ {B}. eval e f g x)›
      by simp
    moreover have ‹infinite (- (⋃p ∈ S ∪ {A}. params p))›
      and ‹infinite (- (⋃p ∈ S ∪ {B}. params p))›
      using inf_params by simp_all
    ultimately show ‹S ∪ {A} ∈ ?C ∨ S ∪ {B} ∈ ?C›
      by blast }

  { fix A B
    assume ‹Neg (And A B) ∈ S›
    then have ‹∀x ∈ S ∪ {Neg (And A B)}. eval e f g x›
      using * by blast
    then have ‹(∀x ∈ S ∪ {Neg A}. eval e f g x) ∨
               (∀x ∈ S ∪ {Neg B}. eval e f g x)›
      by simp
    moreover have ‹infinite (- (⋃p ∈ S ∪ {Neg A}. params p))›
      and ‹infinite (- (⋃p ∈ S ∪ {Neg B}. params p))›
      using inf_params by simp_all
    ultimately show ‹S ∪ {Neg A} ∈ ?C ∨ S ∪ {Neg B} ∈ ?C›
      by blast }

  { fix A B
    assume ‹Impl A B ∈ S›
    then have ‹∀x ∈ S ∪ {Impl A B}. eval e f g x›
      using * by blast
    then have ‹(∀x ∈ S ∪ {Neg A}. eval e f g x) ∨
               (∀x ∈ S ∪ {B}. eval e f g x)›
      by simp
    moreover have ‹infinite (- (⋃p ∈ S ∪ {Neg A}. params p))›
      and ‹infinite (- (⋃p ∈ S ∪ {B}. params p))›
      using inf_params by simp_all
    ultimately show ‹S ∪ {Neg A} ∈ ?C ∨ S ∪ {B} ∈ ?C›
      by blast }

  { fix P and t :: ‹'a term›
    assume ‹Forall P ∈ S›
    then have ‹∀x ∈ S ∪ {Forall P}. eval e f g x›
      using * by blast
    then have ‹∀x ∈ S ∪ {P[t/0]}. eval e f g x›
      by simp
    moreover have ‹infinite (- (⋃p ∈ S ∪ {P[t/0]}. params p))›
      using inf_params by simp
    ultimately show ‹S ∪ {P[t/0]} ∈ ?C›
      by blast }

  { fix P and t :: ‹'a term›
    assume ‹Neg (Exists P) ∈ S›
    then have ‹∀x ∈ S ∪ {Neg (Exists P)}. eval e f g x›
      using * by blast
    then have ‹∀x ∈ S ∪ {Neg (P[t/0])}. eval e f g x›
      by simp
    moreover have ‹infinite (- (⋃p ∈ S ∪ {Neg (P[t/0])}. params p))›
      using inf_params by simp
    ultimately show ‹S ∪ {Neg (P[t/0])} ∈ ?C›
      by blast }

  { fix P
    assume ‹Exists P ∈ S›
    then have ‹∀x ∈ S ∪ {Exists P}. eval e f g x›
      using * by blast
    then have ‹eval e f g (Exists P)›
      by blast
    then obtain z where ‹eval (e⟨0:z⟩) f g P›
      by auto
    moreover obtain x where **: ‹x ∈ - (⋃p ∈ S. params p)›
      using inf_params infinite_imp_nonempty by blast
    then have ‹x ∉ params P›
      using ‹Exists P ∈ S› by auto
    ultimately have ‹eval (e⟨0:(f(x := λy. z)) x []⟩) (f(x := λy. z)) g P›
      by simp
    moreover have ‹∀p ∈ S. eval e (f(x := λy. z)) g p›
      using * ** by simp
    moreover have ‹infinite (- (⋃p ∈ S ∪ {P[App x []/0]}. params p))›
      using inf_params by simp
    ultimately have ‹S ∪ {P[App x []/0]}  ∈
                      {S. infinite (- (⋃p ∈ S. params p)) ∧ (∀p ∈ S. eval e (f(x := λy. z)) g p)}›
      by simp
    then show ‹∃x. S ∪ {P[App x []/0]} ∈ ?C›
      by blast }

  { fix P
    assume ‹Neg (Forall P) ∈ S›
    then have ‹∀x ∈ S ∪ {Neg (Forall P)}. eval e f g x›
      using * by blast
    then have ‹eval e f g (Neg (Forall P))›
      by blast
    then obtain z where ‹¬ eval (e⟨0:z⟩) f g P›
      by auto
    moreover obtain x where **: ‹x ∈ - (⋃p ∈ S. params p)›
      using inf_params infinite_imp_nonempty by blast
    then have ‹x ∉ params P›
      using ‹Neg (Forall P) ∈ S› by auto
    ultimately have ‹¬ eval (e⟨0:(f(x := λy. z)) x []⟩) (f(x := λy. z)) g P›
      by simp
    moreover have ‹∀p ∈ S. eval e (f(x := λy. z)) g p›
      using * ** by simp
    moreover have ‹infinite (- (⋃p ∈ S ∪ {P[App x []/0]}. params p))›
      using inf_params by simp
    ultimately have ‹S ∪ {Neg (P[App x []/0])}  ∈
                      {S. infinite (- (⋃p ∈ S. params p)) ∧ (∀p ∈ S. eval e (f(x := λy. z)) g p)}›
      by simp
    then show ‹∃x. S ∪ {Neg (P[App x []/0])} ∈ ?C›
      by blast }
qed

theorem doublep_infinite_params:
  ‹infinite (- (⋃p ∈ psubst (λn::nat. 2 * n) ` S. params p))›
proof (rule infinite_super)
  show ‹infinite (range (λn::nat. 2 * n + 1))›
    using inj_onI Suc_1 Suc_mult_cancel1 add_right_imp_eq finite_imageD infinite_UNIV_char_0
    by (metis (no_types, lifting))
next
  have ‹⋀m n. Suc (2 * m) ≠ 2 * n› by arith
  then show ‹range (λn. 2 * n + 1)
    ⊆ - (⋃p::(nat, 'a) form ∈ psubst (λn . 2 * n) ` S. params p)›
    by auto
qed

text ‹
When applying the model existence theorem, there is a technical
complication. We must make sure that there are infinitely many
unused parameters. In order to achieve this, we encode parameters
as natural numbers and multiply each parameter occurring in the
set ‹S› by ‹2›.
›

theorem loewenheim_skolem:
  assumes evalS: ‹∀p ∈ S. eval e f g p›
  shows ‹∀p ∈ S. closed 0 p ⟶ eval e' (λn. HApp (2*n)) (λa ts.
      Pred a (terms_of_hterms ts) ∈ Extend (psubst (λn. 2 * n) ` S)
        (mk_finite_char (mk_alt_consistency (close
          {S. infinite (- (⋃p ∈ S. params p)) ∧ (∃f. ∀p ∈ S. eval e f g p)}))) from_nat) p›
    (is ‹∀_ ∈ _. _ _ _ ⟶ eval _ _ ?g _›)
  using evalS
proof (intro ballI impI)
  fix p

  let ?C = ‹{S. infinite (- (⋃p ∈ S. params p)) ∧ (∃f. ∀x ∈ S. eval e f g x)}›

  assume ‹p ∈ S›
    and ‹closed 0 p›
  then have ‹eval e f g p›
    using evalS by blast
  then have ‹∀x ∈ S. eval e f g x›
    using evalS by blast
  then have ‹∀p ∈ psubst (λn. 2 * n) ` S. eval e (λn. f (n div 2)) g p›
    by (simp add: psubst_eval)
  then have ‹psubst (λn. 2 * n) ` S ∈ ?C›
    using doublep_infinite_params by blast
  moreover have ‹psubst (λn. 2 * n) p ∈ psubst (λn. 2 * n) ` S›
    using ‹p ∈ S› by blast
  moreover have ‹closed 0 (psubst (λn. 2 * n) p)›
    using ‹closed 0 p› by simp
  moreover have ‹consistency ?C›
    using sat_consistency by blast
  ultimately have ‹eval e' HApp ?g (psubst (λn. 2 * n) p)›
    using model_existence by blast
  then show ‹eval e' (λn. HApp (2 * n)) ?g p›
    using psubst_eval by blast
qed

section ‹Completeness for open formulas›

abbreviation ‹new_term c t ≡ c ∉ paramst t›
abbreviation ‹new_list c ts ≡ c ∉ paramsts ts›

abbreviation ‹new c p ≡ c ∉ params p›

abbreviation ‹news c z ≡ list_all (new c) z›

subsection ‹Renaming›

lemma new_psubst_image':
  ‹new_term c t ⟹ d ∉ image f (paramst t) ⟹ new_term d (psubstt (f(c := d)) t)›
  ‹new_list c l ⟹ d ∉ image f (paramsts l) ⟹ new_list d (psubstts (f(c := d)) l)›
  by (induct t and l rule: paramst.induct paramsts.induct) auto

lemma new_psubst_image: ‹new c p ⟹ d ∉ image f (params p) ⟹ new d (psubst (f(c := d)) p)›
  using new_psubst_image' by (induct p) auto

lemma news_psubst: ‹news c z ⟹ d ∉ image f (⋃p ∈ set z. params p) ⟹
    news d (map (psubst (f(c := d))) z)›
  using new_psubst_image by (induct z) auto

lemma member_psubst: ‹p ∈ set z ⟹ psubst f p ∈ set (map (psubst f) z)›
  by (induct z) auto

lemma deriv_psubst:
  fixes f :: ‹'a ⇒ 'a›
  assumes inf_params: ‹infinite (UNIV :: 'a set)›
  shows ‹z ⊢ p ⟹ map (psubst f) z ⊢ psubst f p›
proof (induct z p arbitrary: f rule: deriv.induct)
  case (Assum a G)
  then show ?case
    using deriv.Assum member_psubst by blast
next
  case (TTI G)
  then show ?case
    using deriv.TTI by auto
next
  case (FFE G a)
  then show ?case
    using deriv.FFE by auto
next
  case (NegI a G)
  then show ?case
    using deriv.NegI by auto
next
  case (NegE G a)
  then show ?case
    using deriv.NegE by auto
next
  case (Class a G)
  then show ?case
    using deriv.Class by auto
next
  case (ImplE G a b)
  then have ‹map (psubst f) G ⊢ Impl (psubst f a) (psubst f b)›
    and ‹map (psubst f) G ⊢ psubst f a›
    by simp_all
  then show ?case
    using deriv.ImplE by blast
next
  case (ImplI G a b)
  then show ?case
    using deriv.ImplI by auto
next
  case (OrE G a b c)
  then have ‹map (psubst f) G ⊢ Or (psubst f a) (psubst f b)›
    and ‹psubst f a # map (psubst f) G ⊢ psubst f c›
    and ‹psubst f b # map (psubst f) G ⊢ psubst f c›
    by simp_all
  then show ?case
    using deriv.OrE by blast
next
  case (OrI1 G a b)
  then show ?case
    using deriv.OrI1 by auto
next
  case (OrI2 G a b)
  then show ?case
    using deriv.OrI2 by auto
next
  case (AndE1 G a b)
  then show ?case
    using deriv.AndE1 by auto
next
  case (AndE2 p q z)
  then show ?case
    using deriv.AndE2 by auto
next
  case (AndI G a b)
  then show ?case
    using deriv.AndI by fastforce
next
  case (ExistsE z p c q)
  let ?params = ‹params p ∪ params q ∪ (⋃p ∈ set z. params p)›

  have ‹finite ?params›
    by simp
  then obtain fresh where *: ‹fresh ∉ ?params ∪ {c} ∪ image f ?params›
    using ex_new_if_finite inf_params
    by (metis finite.emptyI finite.insertI finite_UnI finite_imageI)

  let ?f = ‹f(c := fresh)›

  have ‹news c (p # q # z)›
    using ExistsE by simp
  then have ‹new fresh (psubst ?f p)› ‹new fresh (psubst ?f q)› ‹news fresh (map (psubst ?f) z)›
    using * new_psubst_image news_psubst by (fastforce simp add: image_Un)+
  then have ‹map (psubst ?f) z = map (psubst f) z›
    using ExistsE by (metis (mono_tags, lifting) Ball_set map_eq_conv psubst_upd)

  have ‹map (psubst ?f) z ⊢ psubst ?f (Exists p)›
    using ExistsE by blast
  then have ‹map (psubst ?f) z ⊢ Exists (psubst ?f p)›
    by simp
  moreover have ‹map (psubst ?f) (subst p (App c []) 0 # z) ⊢ psubst ?f q›
    using ExistsE by blast
  then have ‹subst (psubst ?f p) (App fresh []) 0 # map (psubst ?f) z ⊢ psubst ?f q›
    by simp
  moreover have ‹news fresh (map (psubst ?f) (p # q # z))›
    using ‹new fresh (psubst ?f p)› ‹new fresh (psubst ?f q)› ‹news fresh (map (psubst ?f) z)›
    by simp
  then have ‹new fresh (psubst ?f p)› ‹new fresh (psubst ?f q)› ‹news fresh (map (psubst ?f) z)›
    by simp_all
  ultimately have ‹map (psubst ?f) z ⊢ psubst ?f q›
    using deriv.ExistsE by metis
  then show ?case
    using ExistsE ‹map (psubst ?f) z = map (psubst f) z› by simp
next
  case (ExistsI z p t)
  then show ?case
    using deriv.ExistsI by auto
next
  case (ForallE z p t)
  then show ?case
    using deriv.ForallE by auto
next
  case (ForallI z p c)
  let ?params = ‹params p ∪(⋃p ∈ set z. params p)›

  have ‹finite ?params›
    by simp
  then obtain fresh where *: ‹fresh ∉ ?params ∪ {c} ∪ image f ?params›
    using ex_new_if_finite inf_params
    by (metis finite.emptyI finite.insertI finite_UnI finite_imageI)

  let ?f = ‹f(c := fresh)›

  have ‹news c (p # z)›
    using ForallI by simp
  then have ‹new fresh (psubst ?f p)› ‹news fresh (map (psubst ?f) z)›
    using * new_psubst_image news_psubst by (fastforce simp add: image_Un)+
  then have ‹map (psubst ?f) z = map (psubst f) z›
    using ForallI by (metis (mono_tags, lifting) Ball_set map_eq_conv psubst_upd)

  have ‹map (psubst ?f) z ⊢ psubst ?f (subst p (App c []) 0)›
    using ForallI by blast
  then have ‹map (psubst ?f) z ⊢ subst (psubst ?f p) (App fresh []) 0›
    by simp
  moreover have ‹news fresh (map (psubst ?f) (p # z))›
    using ‹new fresh (psubst ?f p)› ‹news fresh (map (psubst ?f) z)›
    by simp
  then have ‹new fresh (psubst ?f p)› ‹news fresh (map (psubst ?f) z)›
    by simp_all
  ultimately have ‹map (psubst ?f) z ⊢ Forall (psubst ?f p)›
    using deriv.ForallI by metis
  then show ?case
    using ForallI ‹map (psubst ?f) z = map (psubst f) z› by simp
qed

subsection ‹Substitution for constants›

primrec
  subc_term :: ‹'a ⇒ 'a term ⇒ 'a term ⇒ 'a term› and
  subc_list :: ‹'a ⇒ 'a term ⇒ 'a term list ⇒ 'a term list› where
  ‹subc_term c s (Var n) = Var n› |
  ‹subc_term c s (App i l) = (if i = c then s else App i (subc_list c s l))› |
  ‹subc_list c s [] = []› |
  ‹subc_list c s (t # l) = subc_term c s t # subc_list c s l›

primrec subc :: ‹'a ⇒ 'a term ⇒ ('a, 'b) form ⇒ ('a, 'b) form› where
  ‹subc c s FF = FF› |
  ‹subc c s TT = TT› |
  ‹subc c s (Pred i l) = Pred i (subc_list c s l)› |
  ‹subc c s (Neg p) = Neg (subc c s p)› |
  ‹subc c s (Impl p q) = Impl (subc c s p) (subc c s q)› |
  ‹subc c s (Or p q) = Or (subc c s p) (subc c s q)› |
  ‹subc c s (And p q) = And (subc c s p) (subc c s q)› |
  ‹subc c s (Exists p) = Exists (subc c (liftt s) p)› |
  ‹subc c s (Forall p) = Forall (subc c (liftt s) p)›

primrec subcs :: ‹'a ⇒ 'a term ⇒ ('a, 'b) form list ⇒ ('a, 'b) form list› where
  ‹subcs c s [] = []› |
  ‹subcs c s (p # z) = subc c s p # subcs c s z›

lemma subst_0_lift:
  ‹substt (liftt t) s 0 = t›
  ‹substts (liftts l) s 0 = l›
  by (induct t and l rule: substt.induct substts.induct) simp_all

lemma params_lift [simp]:
  fixes t :: ‹'a term› and ts :: ‹'a term list›
  shows
    ‹paramst (liftt t) = paramst t›
    ‹paramsts (liftts ts) = paramsts ts›
  by (induct t and ts rule: paramst.induct paramsts.induct) simp_all

lemma subst_new' [simp]:
  ‹new_term c s ⟹ new_term c t ⟹ new_term c (substt t s m)›
  ‹new_term c s ⟹ new_list c l ⟹ new_list c (substts l s m)›
  by (induct t and l rule: substt.induct substts.induct) simp_all

lemma subst_new [simp]: ‹new_term c s ⟹ new c p ⟹ new c (subst p s m)›
  by (induct p arbitrary: m s) simp_all

lemma subst_new_all:
  assumes ‹a ∉ set cs› ‹list_all (λc. new c p) cs›
  shows ‹list_all (λc. new c (subst p (App a []) m)) cs›
  using assms by (induct cs) auto

lemma subc_new' [simp]:
  ‹new_term c t ⟹ subc_term c s t = t›
  ‹new_list c l ⟹ subc_list c s l = l›
  by (induct t and l rule: subc_term.induct subc_list.induct) auto

lemma subc_new [simp]: ‹new c p ⟹ subc c s p = p›
  by (induct p arbitrary: s) simp_all

lemma subcs_news: ‹news c z ⟹ subcs c s z = z›
  by (induct z) simp_all

lemma subc_psubst' [simp]:
  ‹(∀x ∈ paramst t. x ≠ c ⟶ f x ≠ f c) ⟹
    psubstt f (subc_term c s t) = subc_term (f c) (psubstt f s) (psubstt f t)›
  ‹(∀x ∈ paramsts l. x ≠ c ⟶ f x ≠ f c) ⟹
    psubstts f (subc_list c s l) = subc_list (f c) (psubstt f s) (psubstts f l)›
  by (induct t and l rule: psubstt.induct psubstts.induct) simp_all

lemma subc_psubst: ‹(∀x ∈ params p. x ≠ c ⟶ f x ≠ f c) ⟹
    psubst f (subc c s p) = subc (f c) (psubstt f s) (psubst f p)›
  by (induct p arbitrary: s) simp_all

lemma subcs_psubst: ‹(∀x ∈ (⋃p ∈ set z. params p). x ≠ c ⟶ f x ≠ f c) ⟹
    map (psubst f) (subcs c s z) = subcs (f c) (psubstt f s) (map (psubst f) z)›
  by (induct z) (simp_all add: subc_psubst)

lemma new_lift:
  ‹new_term c t ⟹ new_term c (liftt t)›
  ‹new_list c l ⟹ new_list c (liftts l)›
  by (induct t and l rule: liftt.induct liftts.induct) simp_all

lemma new_subc' [simp]:
  ‹new_term d s ⟹ new_term d t ⟹ new_term d (subc_term c s t)›
  ‹new_term d s ⟹ new_list d l ⟹ new_list d (subc_list c s l)›
  by (induct t and l rule: substt.induct substts.induct) simp_all

lemma new_subc [simp]: ‹new_term d s ⟹ new d p ⟹ new d (subc c s p)›
  by (induct p arbitrary: s) simp_all

lemma news_subcs: ‹new_term d s ⟹ news d z ⟹ news d (subcs c s z)›
  by (induct z) simp_all

lemma psubst_new_free':
  ‹c ≠ n ⟹ new_term n (psubstt (id(n := c)) t)›
  ‹c ≠ n ⟹ new_list n (psubstts (id(n := c)) l)›
  by (induct t and l rule: paramst.induct paramsts.induct) simp_all

lemma psubst_new_free: ‹c ≠ n ⟹ new n (psubst (id(n := c)) p)›
  using psubst_new_free' by (induct p) fastforce+

lemma map_psubst_new_free: ‹c ≠ n ⟹ news n (map (psubst (id(n := c))) z)›
  using psubst_new_free by (induct z) fastforce+

lemma psubst_new_away' [simp]:
  ‹new_term fresh t ⟹ psubstt (id(fresh := c)) (psubstt (id(c := fresh)) t) = t›
  ‹new_list fresh l ⟹ psubstts (id(fresh := c)) (psubstts (id(c := fresh)) l) = l›
  by (induct t and l rule: psubstt.induct psubstts.induct) auto

lemma psubst_new_away [simp]: ‹new fresh p ⟹ psubst (id(fresh := c)) (psubst (id(c := fresh)) p) = p›
  by (induct p) simp_all

lemma map_psubst_new_away:
  ‹news fresh z ⟹ map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z) = z›
  by (induct z) simp_all

lemma psubst_new':
  ‹new_term c t ⟹ psubstt (id(c := x)) t = t›
  ‹new_list c l ⟹ psubstts (id(c := x)) l = l›
  by (induct t and l rule: psubstt.induct psubstts.induct) auto

lemma psubst_new: ‹new c p ⟹ psubst (id(c := x)) p = p›
  using psubst_new' by (induct p) fastforce+

lemma map_psubst_new: ‹news c z ⟹ map (psubst (id(c := x))) z = z›
  using psubst_new by (induct z) auto

lemma lift_subst [simp]:
  ‹liftt (substt t u m) = substt (liftt t) (liftt u) (m + 1)›
  ‹liftts (substts l u m) = substts (liftts l) (liftt u) (m + 1)›
  by (induct t and l rule: substt.induct substts.induct) simp_all

lemma new_subc_same' [simp]:
  ‹new_term c s ⟹ new_term c (subc_term c s t)›
  ‹new_term c s ⟹ new_list c (subc_list c s l)›
  by (induct t and l rule: subc_term.induct subc_list.induct) simp_all

lemma new_subc_same: ‹new_term c s ⟹ new c (subc c s p)›
  by (induct p arbitrary: s) simp_all

lemma lift_subc:
  ‹liftt (subc_term c s t) = subc_term c (liftt s) (liftt t)›
  ‹liftts (subc_list c s l) = subc_list c (liftt s) (liftts l)›
  by (induct t and l rule: liftt.induct liftts.induct) simp_all

lemma new_subc_put':
  ‹new_term c s ⟹ subc_term c s (substt t u m) = subc_term c s (substt t (subc_term c s u) m)›
  ‹new_term c s ⟹ subc_list c s (substts l u m) = subc_list c s (substts l (subc_term c s u) m)›
  by (induct t and l rule: subc_term.induct subc_list.induct) simp_all

lemma new_subc_put:
  ‹new_term c s ⟹ subc c s (subst p t m) = subc c s (subst p (subc_term c s t) m)›
proof (induct p arbitrary: s m t)
  case FF
  then show ?case
    by simp
next
  case TT
  then show ?case
    by simp
next
  case (Pred i l)
  then show ?case
    using new_subc_put' by fastforce
next
  case (Neg p)
  then show ?case
    by (metis subc.simps(4) subst.simps(7))
next
  case (Impl p q)
  then show ?case
    by (metis subc.simps(5) subst.simps(6))
next
  case (Or p q)
  then show ?case
    by (metis subc.simps(6) subst.simps(5))
next
  case (And p q)
  then show ?case
    by (metis subc.simps(7) subst.simps(4))
next
  case (Exists p)
  have ‹subc c s (subst (Exists p) (subc_term c s t) m) =
      Exists (subc c (liftt s) (subst p (subc_term c (liftt s) (liftt t)) (Suc m)))›
    by (simp add: lift_subc)
  also have ‹… = Exists (subc c (liftt s) (subst p (liftt t) (Suc m)))›
    using Exists new_lift(1) by metis
  finally show ?case
    by simp
next
  case (Forall p)
  have ‹subc c s (subst (Forall p) (subc_term c s t) m) =
      Forall (subc c (liftt s) (subst p (subc_term c (liftt s) (liftt t)) (Suc m)))›
    by (simp add: lift_subc)
  also have ‹… = Forall (subc c (liftt s) (subst p (liftt t) (Suc m)))›
    using Forall new_lift(1) by metis
  finally show ?case
    by simp
qed

lemma subc_subst_new':
  ‹new_term c u ⟹ subc_term c (substt s u m) (substt t u m) = substt (subc_term c s t) u m›
  ‹new_term c u ⟹ subc_list c (substt s u m) (substts l u m) = substts (subc_list c s l) u m›
  by (induct t and l rule: subc_term.induct subc_list.induct) simp_all

lemma subc_subst_new:
  ‹new_term c t ⟹ subc c (substt s t m) (subst p t m) = subst (subc c s p) t m›
  using subc_subst_new' by (induct p arbitrary: m t s) fastforce+

lemma subc_sub_0_new [simp]:
  ‹new_term c t ⟹ subc c s (subst p t 0) = subst (subc c (liftt s) p) t 0›
  using subc_subst_new subst_0_lift(1) by metis

lemma member_subc: ‹p ∈ set z ⟹ subc c s p ∈ set (subcs c s z)›
  by (induct z) auto

lemma deriv_subc:
  fixes p :: ‹('a, 'b) form›
  assumes inf_params: ‹infinite (UNIV :: 'a set)›
  shows ‹z ⊢ p ⟹ subcs c s z ⊢ subc c s p›
proof (induct z p arbitrary: c s rule: deriv.induct)
  case (Assum p z)
  then show ?case
    using member_subc deriv.Assum by fast
next
  case TTI
  then show ?case
    using deriv.TTI by simp
  case FFE
  then show ?case
    using deriv.FFE by auto
next
  case (NegI z p)
  then show ?case
    using deriv.NegI by auto
next
  case (NegE z p)
  then show ?case
    using deriv.NegE by fastforce
next
  case (Class p z)
  then show ?case
    using deriv.Class by auto
next
  case (ImplE z p q)
  then show ?case
    using deriv.ImplE by fastforce
next
  case (ImplI z q p)
  then show ?case
    using deriv.ImplI by fastforce
next
  case (OrE z p q r)
  then show ?case
    using deriv.OrE by fastforce
next
  case (OrI1 z p q)
  then show ?case
    using deriv.OrI1 by fastforce
next
  case (OrI2 z q p)
  then show ?case
    using deriv.OrI2 by fastforce
next
  case (AndE1 z p q)
  then show ?case
    using deriv.AndE1 by fastforce
next
  case (AndE2 z p q)
  then show ?case
    using deriv.AndE2 by fastforce
next
  case (AndI p z q)
  then show ?case
    using deriv.AndI by fastforce
next
  case (ExistsE z p d q)
  then show ?case
  proof (cases ‹c = d›)
    case True
    then have ‹z ⊢ q›
      using ExistsE deriv.ExistsE by fast
    moreover have ‹new c q› and ‹news c z›
      using ExistsE True by simp_all
    ultimately show ?thesis
      using subc_new subcs_news by metis
  next
    case False
    let ?params = ‹params p ∪ params q ∪ (⋃p ∈ set z. params p) ∪ paramst s ∪ {c} ∪ {d}›

    have ‹finite ?params›
      by simp
    then obtain fresh where fresh: ‹fresh ∉ ?params›
      using inf_params by (meson ex_new_if_finite infinite_UNIV_listI)

    let ?s = ‹psubstt (id(d := fresh)) s›
    let ?f = ‹id(d := fresh, fresh := d)›

    have f: ‹∀x ∈ ?params. x ≠ c ⟶ ?f x ≠ ?f c›
      using fresh by simp

    have ‹new_term d ?s›
      using fresh psubst_new_free'(1) by fast
    then have ‹psubstt ?f ?s = psubstt (id(fresh := d)) ?s›
      by (metis fun_upd_twist psubstt_upd(1))
    then have psubst_s: ‹psubstt ?f ?s = s›
      using fresh by simp

    have ‹?f c = c› and ‹new_term (?f c) (App fresh [])›
      using False fresh by auto

    have ‹subcs c (psubstt ?f ?s) z ⊢ subc c (psubstt ?f ?s) (Exists p)›
      using ExistsE by blast
    then have exi_p:
      ‹subcs c s z ⊢ Exists (subc c (liftt (psubstt ?f ?s)) p)›
      using psubst_s by simp

    have ‹news d z›
      using ExistsE by simp
    moreover have ‹news fresh z›
      using fresh by (induct z) simp_all
    ultimately have ‹map (psubst ?f) z = z›
      by (induct z) simp_all
    moreover have ‹∀x ∈ ⋃p ∈ set z. params p. x ≠ c ⟶ ?f x ≠ ?f c›
      by auto
    ultimately have psubst_z: ‹map (psubst ?f) (subcs c ?s z) = subcs c s z›
      using ‹?f c = c› psubst_s by (simp add: subcs_psubst)

    have ‹psubst ?f (subc c ?s (subst p (App d []) 0)) =
        subc (?f c) (psubstt ?f ?s) (psubst ?f (subst p (App d []) 0))›
      using fresh by (simp add: subc_psubst)
    also have ‹… = subc c s (subst (psubst ?f p) (App fresh []) 0)›
      using psubst_subst psubst_s ‹?f c = c› by simp
    also have ‹… = subc c s (subst p (App fresh []) 0)›
      using ExistsE fresh by simp
    finally have psubst_p: ‹psubst ?f (subc c ?s (subst p (App d []) 0)) =
        subst (subc c (liftt s) p) (App fresh []) 0›
      using subc_sub_0_new ‹new_term (?f c) (App fresh [])› ‹?f c = c› by metis

    have ‹∀x ∈ params q. x ≠ c ⟶ ?f x ≠ ?f c›
      using f by blast
    then have psubst_q: ‹psubst ?f (subc c ?s q) = subc c s q›
      using ExistsE fresh ‹?f c = c› psubst_s f by (simp add: subc_psubst)

    have ‹subcs c ?s (subst p (App d []) 0 # z) ⊢ subc c ?s q›
      using ExistsE by blast
    then have ‹subc c ?s (subst p (App d []) 0) # subcs c ?s z ⊢ subc c ?s q›
      by simp
    then have ‹psubst ?f (subc c ?s (subst p (App d []) 0)) # map (psubst ?f) (subcs c ?s z)
        ⊢ psubst ?f (subc c ?s q)›
      using deriv_psubst inf_params by fastforce
    then have q: ‹subst (subc c (liftt s) p) (App fresh []) 0 # subcs c s z ⊢ subc c s q›
      using psubst_q psubst_z psubst_p by simp

    have ‹new fresh (subc c (liftt s) p)›
      using fresh new_subc new_lift by simp
    moreover have ‹new fresh (subc c s q)›
      using fresh new_subc by simp
    moreover have ‹news fresh (subcs c s z)›
      using fresh ‹news fresh z› by (simp add: news_subcs)
    ultimately show ‹subcs c s z ⊢ subc c s q›
      using deriv.ExistsE exi_p q psubst_s by metis
  qed
next
  case (ExistsI z p t)
  let ?params = ‹params p ∪ (⋃p ∈ set z. params p) ∪ paramst s ∪ paramst t ∪ {c}›

  have ‹finite ?params›
    by simp
  then obtain fresh where fresh: ‹fresh ∉ ?params›
    using inf_params by (meson ex_new_if_finite infinite_UNIV_listI)

  let ?f = ‹id(c := fresh)›
  let ?g = ‹id(fresh := c)›
  let ?s = ‹psubstt ?f s›

  have c: ‹?g c = c›
    using fresh by simp
  have s: ‹psubstt ?g ?s = s›
    using fresh by simp
  have p: ‹psubst ?g (Exists p) = Exists p›
    using fresh by simp

  have ‹∀x ∈ (⋃p ∈ set z. params p). x ≠ c ⟶ ?g x ≠ ?g c›
    using fresh by auto
  moreover have ‹map (psubst ?g) z = z›
    using fresh by (induct z) simp_all
  ultimately have z: ‹map (psubst ?g) (subcs c ?s z) = subcs c s z›
    using s by (simp add: subcs_psubst)

  have ‹new_term c ?s›
    using fresh psubst_new_free' by fast
  then have ‹subcs c ?s z ⊢ subc c ?s (subst p (subc_term c ?s t) 0)›
    using ExistsI new_subc_put by metis
  moreover have ‹new_term c (subc_term c ?s t)›
    using ‹new_term c ?s› new_subc_same' by fast
  ultimately have ‹subcs c ?s z ⊢ subst (subc c (liftt ?s) p) (subc_term c ?s t) 0›
    using subc_sub_0_new by metis

  then have ‹subcs c ?s z ⊢ subc c ?s (Exists p)›
    using deriv.ExistsI by simp
  then have ‹map (psubst ?g) (subcs c ?s z) ⊢ psubst ?g (subc c ?s (Exists p))›
    using deriv_psubst inf_params by blast
  moreover have ‹∀x ∈ params (Exists p). x ≠ c ⟶ ?g x ≠ ?g c›
    using fresh by auto
  ultimately show ‹subcs c s z ⊢ subc c s (Exists p)›
    using c s p z by (simp add: subc_psubst)
next
  case (ForallE z p t)
  let ?params = ‹params p ∪ (⋃p ∈ set z. params p) ∪ paramst s ∪ paramst t ∪ {c}›

  have ‹finite ?params›
    by simp
  then obtain fresh where fresh: ‹fresh ∉ ?params›
    using inf_params by (meson ex_new_if_finite infinite_UNIV_listI)

  let ?f = ‹id(c := fresh)›
  let ?g = ‹id(fresh := c)›
  let ?s = ‹psubstt ?f s›

  have c: ‹?g c = c›
    using fresh by simp
  have s: ‹psubstt ?g ?s = s›
    using fresh by simp
  have p: ‹psubst ?g (subst p t 0) = subst p t 0›
    using fresh psubst_new psubst_subst subst_new psubst_new'(1) by fastforce

  have ‹∀x ∈ (⋃p ∈ set z. params p). x ≠ c ⟶ ?g x ≠ ?g c›
    using fresh by auto
  moreover have ‹map (psubst ?g) z = z›
    using fresh by (induct z) simp_all
  ultimately have z: ‹map (psubst ?g) (subcs c ?s z) = subcs c s z›
    using s by (simp add: subcs_psubst)

  have ‹new_term c ?s›
    using fresh psubst_new_free' by fastforce

  have ‹subcs c ?s z ⊢ Forall (subc c (liftt ?s) p)›
    using ForallE by simp
  then have ‹subcs c ?s z ⊢ subst (subc c (liftt ?s) p) (subc_term c ?s t) 0›
    using deriv.ForallE by blast
  moreover have ‹new_term c (subc_term c ?s t)›
    using ‹new_term c ?s› new_subc_same' by fast
  ultimately have ‹subcs c ?s z ⊢ subc c ?s (subst p (subc_term c ?s t) 0)›
    by simp
  then have ‹subcs c ?s z ⊢ subc c ?s (subst p t 0)›
    using new_subc_put ‹new_term c ?s› by metis
  then have ‹map (psubst ?g) (subcs c ?s z) ⊢ psubst ?g (subc c ?s (subst p t 0))›
    using deriv_psubst inf_params by blast
  moreover have ‹∀x ∈ params (subst p t 0). x ≠ c ⟶ ?g x ≠ ?g c›
    using fresh p psubst_new_free by (metis fun_upd_apply id_apply)
  ultimately show ‹subcs c s z ⊢ subc c s (subst p t 0)›
    using c s p z by (simp add: subc_psubst)
next
  case (ForallI z p d)
  then show ?case
  proof (cases ‹c = d›)
    case True
    then have ‹z ⊢ Forall p›
      using ForallI deriv.ForallI by fast
    moreover have ‹new c p› and ‹news c z›
      using ForallI True by simp_all
    ultimately show ?thesis
      by (simp add: subcs_news)
  next
    case False
    let ?params = ‹params p ∪ (⋃p ∈ set z. params p) ∪ paramst s ∪ {c} ∪ {d}›

    have ‹finite ?params›
      by simp
    then obtain fresh where fresh: ‹fresh ∉ ?params›
      using inf_params by (meson ex_new_if_finite infinite_UNIV_listI)

    let ?s = ‹psubstt (id(d := fresh)) s›
    let ?f = ‹id(d := fresh, fresh := d)›

    have f: ‹∀x ∈ ?params. x ≠ c ⟶ ?f x ≠ ?f c›
      using fresh by simp

    have ‹new_term d ?s›
      using fresh psubst_new_free' by fastforce
    then have ‹psubstt ?f ?s = psubstt (id(fresh := d)) ?s›
      by (metis fun_upd_twist psubstt_upd(1))
    then have psubst_s: ‹psubstt ?f ?s = s›
      using fresh by simp

    have ‹?f c = c› and ‹new_term c (App fresh [])›
      using False fresh by auto

    have ‹psubst ?f (subc c ?s (subst p (App d []) 0)) =
      subc (?f c) (psubstt ?f ?s) (psubst ?f (subst p (App d []) 0))›
      by (simp add: subc_psubst)
    also have ‹… = subc c s (subst (psubst ?f p) (App fresh []) 0)›
      using ‹?f c = c› psubst_subst psubst_s by simp
    also have ‹… = subc c s (subst p (App fresh []) 0)›
      using ForallI fresh by simp
    finally have psubst_p: ‹psubst ?f (subc c ?s (subst p (App d []) 0)) =
        subst (subc c (liftt s) p) (App fresh []) 0›
      using subc_sub_0_new ‹new_term c (App fresh [])› by simp

    have ‹news d z›
      using ForallI by simp
    moreover have ‹news fresh z›
      using fresh by (induct z) simp_all
    ultimately have ‹map (psubst ?f) z = z›
      by (induct z) simp_all
    moreover have ‹∀x ∈ ⋃p ∈ set z. params p. x ≠ c ⟶ ?f x ≠ ?f c›
      by auto
    ultimately have psubst_z: ‹map (psubst ?f) (subcs c ?s z) = subcs c s z›
      using ‹?f c = c› psubst_s by (simp add: subcs_psubst)

    have ‹subcs c ?s z ⊢ subc c ?s (subst p (App d []) 0)›
      using ForallI by blast
    then have ‹map (psubst ?f) (subcs c ?s z) ⊢ psubst ?f (subc c ?s (subst p (App d []) 0))›
      using deriv_psubst inf_params by blast
    then have ‹subcs c s z ⊢ psubst ?f (subc c ?s (subst p (App d []) 0))›
      using psubst_z by simp
    then have sub_p: ‹subcs c s z ⊢ subst (subc c (liftt s) p) (App fresh []) 0›
      using psubst_p by simp

    have ‹new_term fresh s›
      using fresh by simp
    then have ‹new_term fresh (liftt s)›
      using new_lift by simp
    then have ‹new fresh (subc c (liftt s) p)›
      using fresh new_subc by simp
    moreover have ‹news fresh (subcs c s z)›
      using ‹news fresh z› ‹new_term fresh s› news_subcs by fast
    ultimately show ‹subcs c s z ⊢ subc c s (Forall p)›
      using deriv.ForallI sub_p by simp
  qed
qed

subsection ‹Weakening assumptions›

lemma psubst_new_subset:
  assumes ‹set z ⊆ set z'› ‹c ∉ (⋃p ∈ set z. params p)›
  shows ‹set z ⊆ set (map (psubst (id(c := n))) z')›
  using assms by force

lemma subset_cons: ‹set z ⊆ set z' ⟹ set (p # z) ⊆ set (p # z')›
  by auto

lemma weaken_assumptions:
  fixes p :: ‹('a, 'b) form›
  assumes inf_params: ‹infinite (UNIV :: 'a set)›
  shows ‹z ⊢ p ⟹ set z ⊆ set z' ⟹ z' ⊢ p›
proof (induct z p arbitrary: z' rule: deriv.induct)
  case (Assum p z)
  then show ?case
    using deriv.Assum by auto
next
  case TTI
  then show ?case
    using deriv.TTI by auto
next
  case FFE
  then show ?case
    using deriv.FFE by auto
next
  case (NegI p z)
  then show ?case
    using deriv.NegI subset_cons by metis
next
  case (NegE p z)
  then show ?case
    using deriv.NegE by metis
next
  case (Class z p)
  then show ?case
    using deriv.Class subset_cons by metis
next
  case (ImplE z p q)
  then show ?case
    using deriv.ImplE by blast
next
  case (ImplI z q p)
  then show ?case
    using deriv.ImplI subset_cons by metis
next
  case (OrE z p q z )
  then show ?case
    using deriv.OrE subset_cons by metis
next
  case (OrI1 z p q)
  then show ?case
    using deriv.OrI1 by blast
next
  case (OrI2 z q p)
  then show ?case
    using deriv.OrI2 by blast
next
  case (AndE1 z p q)
  then show ?case
    using deriv.AndE1 by blast
next
  case (AndE2 z p q)
  then show ?case
    using deriv.AndE2 by blast
next
  case (AndI z p q)
  then show ?case
    using deriv.AndI by blast
next
  case (ExistsE z p c q)
  let ?params = ‹params p ∪ params q ∪ (⋃p ∈ set z'. params p) ∪ {c}›

  have ‹finite ?params›
    by simp
  then obtain fresh where fresh: ‹fresh ∉ ?params›
    using inf_params by (meson ex_new_if_finite List.finite_set infinite_UNIV_listI)

  let ?z' = ‹map (psubst (id(c := fresh))) z'›

  have ‹news c z›
    using ExistsE by simp
  then have ‹set z ⊆ set ?z'›
    using ExistsE psubst_new_subset by (simp add: Ball_set)
  then have ‹?z' ⊢ Exists p›
    using ExistsE by blast

  moreover have ‹set (subst p (App c []) 0 # z) ⊆ set (subst p (App c []) 0 # ?z')›
    using ‹set z ⊆ set ?z'› by auto
  then have ‹subst p (App c []) 0 # ?z' ⊢ q›
    using ExistsE by blast

  moreover have ‹news c ?z'›
    using fresh by (simp add: map_psubst_new_free)
  then have ‹new c p› ‹new c q› ‹news c ?z'›
    using ExistsE by simp_all

  ultimately have ‹?z' ⊢ q›
    using ExistsE deriv.ExistsE by metis

  then have ‹map (psubst (id(fresh := c))) ?z' ⊢ psubst (id(fresh := c)) q›
    using deriv_psubst inf_params by blast
  moreover have ‹map (psubst (id(fresh := c))) ?z' = z'›
    using fresh map_psubst_new_away Ball_set by fastforce
  moreover have ‹psubst (id(fresh := c)) q = q›
    using fresh by simp
  ultimately show ‹z' ⊢ q›
    by simp
next
  case (ExistsI z p t)
  then show ?case
    using deriv.ExistsI by blast
next
  case (ForallE p z t)
  then show ?case
    using deriv.ForallE by blast
next
  case (ForallI z p c)
  let ?params = ‹params p ∪ (⋃p ∈ set z'. params p) ∪ {c}›

  have ‹finite ?params›
    by simp
  then obtain fresh where fresh: ‹fresh ∉ ?params›
    using inf_params by (meson ex_new_if_finite List.finite_set infinite_UNIV_listI)

  let ?z' = ‹map (psubst (id(c := fresh))) z'›

  have ‹news c z›
    using ForallI by simp
  then have ‹set z ⊆ set ?z'›
    using ForallI psubst_new_subset by (metis (no_types, lifting) Ball_set UN_iff)
  then have ‹?z' ⊢ subst p (App c []) 0›
    using ForallI by blast

  moreover have ‹∀p ∈ set ?z'. c ∉ params p›
    using fresh psubst_new_free by fastforce
  then have ‹list_all (λp. c ∉ params p) (p # ?z')›
    using ForallI by (simp add: list_all_iff)
  then have ‹new c p› ‹news c ?z'›
    by simp_all

  ultimately have ‹?z' ⊢ Forall p›
    using ForallI deriv.ForallI by fast

  then have ‹map (psubst (id(fresh := c))) ?z' ⊢ psubst (id(fresh := c)) (Forall p)›
    using deriv_psubst inf_params by blast
  moreover have ‹map (psubst (id(fresh := c))) ?z' = z'›
    using fresh map_psubst_new_away Ball_set by fastforce
  moreover have ‹psubst (id(fresh := c)) (Forall p) = Forall p›
    using fresh ForallI by simp
  ultimately show ‹z' ⊢ Forall p›
    by simp
qed

subsection ‹Implications and assumptions›

primrec put_imps :: ‹('a, 'b) form ⇒ ('a, 'b) form list ⇒ ('a, 'b) form› where
  ‹put_imps p [] = p› |
  ‹put_imps p (q # z) = Impl q (put_imps p z)›

lemma semantics_put_imps:
  ‹(e,f,g,z ⊨ p) = eval e f g (put_imps p z)›
  unfolding model_def by (induct z) auto

lemma shift_imp_assum:
  fixes p :: ‹('a, 'b) form›
  assumes inf_params: ‹infinite (UNIV :: 'a set)›
    and ‹z ⊢ Impl p q›
  shows ‹p # z ⊢ q›
proof -
  have ‹set z ⊆ set (p # z)›
    by auto
  then have ‹p # z ⊢ Impl p q›
    using assms weaken_assumptions inf_params by blast
  moreover have ‹p # z ⊢ p›
    by (simp add: Assum)
  ultimately show ‹p # z ⊢ q›
    using ImplE by blast
qed

lemma remove_imps:
  assumes ‹infinite (- params p)›
  shows ‹z' ⊢ put_imps p z ⟹ rev z @ z' ⊢ p›
  using assms shift_imp_assum by (induct z arbitrary: z') auto

subsection ‹Closure elimination›

lemma subc_sub_closed_var' [simp]:
  ‹new_term c t ⟹ closedt (Suc m) t ⟹ subc_term c (Var m) (substt t (App c []) m) = t›
  ‹new_list c l ⟹ closedts (Suc m) l ⟹ subc_list c (Var m) (substts l (App c []) m) = l›
  by (induct t and l rule: substt.induct substts.induct) auto

lemma subc_sub_closed_var [simp]: ‹new c p ⟹ closed (Suc m) p ⟹
    subc c (Var m) (subst p (App c []) m) = p›
  by (induct p arbitrary: m) simp_all

primrec put_unis :: ‹nat ⇒ ('a, 'b) form ⇒ ('a, 'b) form› where
  ‹put_unis 0 p = p› |
  ‹put_unis (Suc m) p = Forall (put_unis m p)›

lemma sub_put_unis [simp]:
  ‹subst (put_unis k p) (App c []) i = put_unis k (subst p (App c []) (i + k))›
  by (induct k arbitrary: i) simp_all

lemma closed_put_unis [simp]: ‹closed m (put_unis k p) = closed (m + k) p›
  by (induct k arbitrary: m) simp_all

lemma valid_put_unis: ‹∀(e :: nat ⇒ 'a) f g. eval e f g p ⟹
    eval (e :: nat ⇒ 'a) f g (put_unis m p)›
  by (induct m arbitrary: e) simp_all

lemma put_unis_collapse: ‹put_unis m (put_unis n p) = put_unis (m + n) p›
  by (induct m) simp_all

fun consts_for_unis :: ‹('a, 'b) form ⇒ 'a list ⇒ ('a, 'b) form› where
  ‹consts_for_unis (Forall p) (c#cs) = consts_for_unis (subst p (App c []) 0) cs› |
  ‹consts_for_unis p _ = p›

lemma consts_for_unis: ‹[] ⊢ put_unis (length cs) p ⟹
  [] ⊢ consts_for_unis (put_unis (length cs) p) cs›
proof (induct cs arbitrary: p)
  case (Cons c cs)
  then have ‹[] ⊢ Forall (put_unis (length cs) p)›
    by simp
  then have ‹[] ⊢ subst (put_unis (length cs) p) (App c []) 0›
    using ForallE by blast
  then show ?case
    using Cons by simp
qed simp

primrec vars_for_consts :: ‹('a, 'b) form ⇒ 'a list ⇒ ('a, 'b) form› where
  ‹vars_for_consts p [] = p› |
  ‹vars_for_consts p (c # cs) = subc c (Var (length cs)) (vars_for_consts p cs)›

lemma vars_for_consts:
  assumes ‹infinite (- params p)›
  shows ‹[] ⊢ p ⟹ [] ⊢ vars_for_consts p xs›
  using assms deriv_subc by (induct xs arbitrary: p) fastforce+

lemma vars_for_consts_for_unis:
  ‹closed (length cs) p ⟹ list_all (λc. new c p) cs ⟹ distinct cs ⟹
   vars_for_consts (consts_for_unis (put_unis (length cs) p) cs) cs = p›
  by (induct cs arbitrary: p) (simp_all add: subst_new_all)

lemma fresh_constant:
  fixes p :: ‹('a, 'b) form›
  assumes ‹infinite (UNIV :: 'a set)›
  shows ‹∃c. c ∉ set cs ∧ new c p›
proof -
  have ‹finite (set cs ∪ params p)›
    by simp
  then show ?thesis
    using assms ex_new_if_finite UnI1 UnI2 by metis
qed

lemma fresh_constants:
  fixes p :: ‹('a, 'b) form›
  assumes ‹infinite (UNIV :: 'a set)›
  shows ‹∃cs. length cs = m ∧ list_all (λc. new c p) cs ∧ distinct cs›
proof (induct m)
  case (Suc m)
  then obtain cs where ‹length cs = m ∧ list_all (λc. new c p) cs ∧ distinct cs›
    by blast
  moreover obtain c where ‹c ∉ set cs ∧ new c p›
    using Suc assms fresh_constant by blast
  ultimately have ‹length (c # cs) = Suc m ∧ list_all (λc. new c p) (c # cs) ∧ distinct (c # cs)›
    by simp
  then show ?case
    by blast
qed simp

lemma closed_max:
  assumes ‹closed m p› ‹closed n q›
  shows ‹closed (max m n) p ∧ closed (max m n) q›
proof -
  have ‹m ≤ max m n› and ‹n ≤ max m n›
    by simp_all
  then show ?thesis
    using assms closed_mono by metis
qed

lemma ex_closed' [simp]:
  fixes t :: ‹'a term› and l :: ‹'a term list›
  shows ‹∃m. closedt m t› ‹∃n. closedts n l›
proof (induct t and l rule: closedt.induct closedts.induct)
  case (Cons_term t l)
  then obtain m and n where ‹closedt m t› and ‹closedts n l›
    by blast
  moreover have ‹m ≤ max m n› and ‹n ≤ max m n›
    by simp_all
  ultimately have ‹closedt (max m n) t› and ‹closedts (max m n) l›
    using closedt_mono by blast+
  then show ?case
    by auto
qed auto

lemma ex_closed [simp]: ‹∃m. closed m p›
proof (induct p)
  case FF
  then show ?case
    by simp
next
  case TT
  then show ?case
    by simp
next
  case (Neg p)
  then show ?case
    by simp
next
  case (Impl p q)
  then show ?case
    using closed_max by fastforce
next
  case (Or p q)
  then show ?case
    using closed_max by fastforce
next
  case (And p q)
  then show ?case
    using closed_max by fastforce
next
  case (Exists p)
  then obtain m where ‹closed m p›
    by blast
  then have ‹closed (Suc m) p›
    using closed_mono Suc_n_not_le_n nat_le_linear by blast
  then show ?case
    by auto
next
  case (Forall p)
  then obtain m where ‹closed m p›
    by blast
  then have ‹closed (Suc m) p›
    using closed_mono Suc_n_not_le_n nat_le_linear by blast
  then show ?case
    by auto
qed simp_all

lemma ex_closure: ‹∃m. closed 0 (put_unis m p)›
  by simp

lemma remove_unis_sentence:
  assumes inf_params: ‹infinite (- params p)›
    and ‹closed 0 (put_unis m p)› ‹[] ⊢ put_unis m p›
  shows ‹[] ⊢ p›
proof -
  obtain cs :: ‹'a list› where ‹length cs = m›
    and *: ‹distinct cs› and **: ‹list_all (λc. new c p) cs›
    using assms finite_compl finite_params fresh_constants inf_params by metis
  then have ‹[] ⊢ consts_for_unis (put_unis (length cs) p) cs›
    using assms consts_for_unis by blast
  then have ‹[] ⊢ vars_for_consts (consts_for_unis (put_unis (length cs) p) cs) cs›
    using vars_for_consts inf_params by fastforce
  moreover have ‹closed (length cs) p›
    using assms ‹length cs = m› by simp
  ultimately show ‹[] ⊢ p›
    using vars_for_consts_for_unis * ** by metis
qed

subsection ‹Completeness›

theorem completeness:
  fixes p :: ‹(nat, nat) form›
  assumes ‹∀(e :: nat ⇒ nat hterm) f g. e, f, g, z ⊨ p›
  shows ‹z ⊢ p›
proof -
  let ?p = ‹put_imps p (rev z)›

  have *: ‹∀(e :: nat ⇒ nat hterm) f g. eval e f g ?p›
    using assms semantics_put_imps unfolding model_def by fastforce
  obtain m where **: ‹closed 0 (put_unis m ?p)›
    using ex_closure by blast
  moreover have ‹list_all (closed 0) []›
    by simp
  moreover have ‹∀(e :: nat ⇒ nat hterm) f g. e, f, g, [] ⊨ put_unis m ?p›
    using * valid_put_unis unfolding model_def by blast
  ultimately have ‹[] ⊢ put_unis m ?p›
    using natded_complete by blast
  then have ‹[] ⊢ ?p›
    using ** remove_unis_sentence by fastforce
  then show ‹z ⊢ p›
    using remove_imps by fastforce
qed

abbreviation ‹valid p ≡ ∀(e :: nat ⇒ nat hterm) f g. eval e f g p›

proposition
  fixes p :: ‹(nat, nat) form›
  shows ‹valid p ⟹ eval e f g p›
  using completeness correctness
  unfolding model_def by (metis list.pred_inject(1))

proposition
  fixes p :: ‹(nat, nat) form›
  shows ‹([] ⊢ p) = valid p›
  using completeness correctness
  unfolding model_def by fastforce

corollary ‹∀e (f::nat ⇒ nat hterm list ⇒ nat hterm) (g::nat ⇒ nat hterm list ⇒ bool).
    e,f,g,ps ⊨ p ⟹ ps ⊢ p›
  by (rule completeness)

end