# Theory Tableau

theory Tableau
imports Common
```(*
Author: Asta Halkjær From, DTU Compute, 2019
Contributors: Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen
*)

section ‹Tableau Calculus›

theory Tableau imports Common begin

inductive TC :: ‹('a, 'b) form list ⇒ bool› (‹⊣ _› 0) where
Basic: ‹⊣ Pred i l # Neg (Pred i l) # G›
| BasicFF: ‹⊣ ⊥ # G›
| BasicNegTT: ‹⊣ Neg ⊤ # G›
| AlphaNegNeg: ‹⊣ A # G ⟹ ⊣ Neg (Neg A) # G›
| AlphaAnd: ‹⊣ A # B # G ⟹ ⊣ And A B # G›
| AlphaNegOr: ‹⊣ Neg A # Neg B # G ⟹ ⊣ Neg (Or A B) # G›
| AlphaNegImpl: ‹⊣ A # Neg B # G ⟹ ⊣ Neg (Impl A B) # G›
| BetaNegAnd: ‹⊣ Neg A # G ⟹ ⊣ Neg B # G ⟹ ⊣ Neg (And A B) # G›
| BetaOr: ‹⊣ A # G ⟹ ⊣ B # G ⟹ ⊣ Or A B # G›
| BetaImpl: ‹⊣ Neg A # G ⟹ ⊣ B # G ⟹ ⊣ Impl A B # G›
| GammaForall: ‹⊣ subst A t 0 # G ⟹ ⊣ Forall A # G›
| GammaNegExists: ‹⊣ Neg (subst A t 0) # G ⟹ ⊣ Neg (Exists A) # G›
| DeltaExists: ‹⊣ subst A (App n []) 0 # G ⟹ news n (A # G) ⟹ ⊣ Exists A # G›
| DeltaNegForall: ‹⊣ Neg (subst A (App n []) 0) # G ⟹ news n (A # G) ⟹ ⊣ Neg (Forall A) # G›
| Order: ‹⊣ G ⟹ set G = set G' ⟹ ⊣ G'›

lemma Shift: ‹⊣ rotate1 G ⟹ ⊣ G›

lemma Swap: ‹⊣ B # A # G ⟹ ⊣ A # B # G›

definition tableauproof :: ‹('a, 'b) form list ⇒ ('a, 'b) form ⇒ bool› where
‹tableauproof ps p ≡ (⊣ Neg p # ps)›

theorem tableauNotAA: ‹⊣ [Neg (Pred ''A'' []), Pred ''A'' []]›
by (rule Shift, simp) (rule Basic)

theorem AndAnd:
‹⊣ [And (Pred ''A'' []) (Pred ''B'' []), Neg (And (Pred ''B'' []) (Pred ''A'' []))]›
apply (rule AlphaAnd)
apply (rule Shift, rule Shift, simp)
apply (rule BetaNegAnd)
apply (rule Shift, rule Shift, simp)
apply (rule Basic)
apply (rule Swap)
apply (rule Basic)
done

subsection ‹Soundness›

lemma TC_soundness:
‹⊣ G ⟹ ∃p ∈ set G. ¬ eval e f g p›
proof (induct G arbitrary: f rule: TC.induct)
case (DeltaExists A n G)
show ?case
proof (rule ccontr)
assume ‹¬ (∃p ∈ set (Exists A # G). ¬ eval e f g p)›
then have *: ‹∀p ∈ set (Exists A # G). eval e f g p›
by simp

then obtain x where ‹eval (shift e 0 x) (f(n := λw. x)) g A›
using ‹news n (A # G)› by auto
then have **: ‹eval e (f(n := λw. x)) g (subst A (App n []) 0)›
by simp

have ‹∃p ∈ set (subst A (App n []) 0 # G). ¬ eval e (f(n := λw. x)) g p›
using DeltaExists by fast
then consider
‹¬ eval e (f(n := λw. x)) g (subst A (App n []) 0)› |
‹∃p ∈ set G. ¬ eval e (f(n := λw. x)) g p›
by auto
then show False
proof cases
case 1
then show ?thesis
using ** ..
next
case 2
then obtain p where ‹¬ eval e (f(n := λw. x)) g p› ‹p ∈ set G›
by blast
then have ‹¬ eval e f g p›
using ‹news n (A # G)› by (metis Ball_set set_subset_Cons subsetCE upd_lemma)
then show ?thesis
using * ‹p ∈ set G› by simp
qed
qed
next
case (DeltaNegForall A n G)
show ?case
proof (rule ccontr)
assume ‹¬ (∃p ∈ set (Neg (Forall A) # G). ¬ eval e f g p)›
then have *: ‹∀p ∈ set (Neg (Forall A) # G). eval e f g p›
by simp

then obtain x where ‹eval (shift e 0 x) (f(n := λw. x)) g (Neg A)›
using ‹news n (A # G)› by auto
then have **: ‹eval e (f(n := λw. x)) g (Neg (subst A (App n []) 0))›
by simp

have ‹∃p ∈ set (Neg (subst A (App n []) 0) # G). ¬ eval e (f(n := λw. x)) g p›
using DeltaNegForall by fast
then consider
‹¬ eval e (f(n := λw. x)) g (Neg (subst A (App n []) 0))› |
‹∃p ∈ set G. ¬ eval e (f(n := λw. x)) g p›
by auto
then show False
proof cases
case 1
then show ?thesis
using ** ..
next
case 2
then obtain p where ‹¬ eval e (f(n := λw. x)) g p› ‹p ∈ set G›
by blast
then have ‹¬ eval e f g p›
using ‹news n (A # G)› by (metis Ball_set set_subset_Cons subsetCE upd_lemma)
then show ?thesis
using * ‹p ∈ set G› by simp
qed
qed
qed auto

theorem tableau_soundness:
‹tableauproof ps p ⟹ list_all (eval e f g) ps ⟹ eval e f g p›
using TC_soundness unfolding tableauproof_def list_all_def by fastforce

subsection ‹Completeness for Closed Formulas›

theorem infinite_nonempty: ‹infinite A ⟹ ∃x. x ∈ A›

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

{ fix p ts
assume ‹Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S›
then show False
using * Basic Order ‹¬ (⊣ G)› by fastforce }

{ assume ‹⊥ ∈ S›
then show False
using * BasicFF Order ‹¬ (⊣ G)› by fastforce }

{ assume ‹Neg ⊤ ∈ S›
then show False
using * BasicNegTT Order ‹¬ (⊣ G)› by fastforce }

{ fix Z
assume ‹Neg (Neg Z) ∈ S›
then have ‹¬ (⊣ Z # G)›
using * AlphaNegNeg Order ‹¬ (⊣ G)›
by (metis insert_absorb list.set(2))
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 ‹¬ (⊣ A # B # G)›
using * AlphaAnd Order ‹¬ (⊣ G)›
by (metis insert_absorb list.set(2))
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 ‹¬ (⊣ Neg A # Neg B # G)›
using * AlphaNegOr Order ‹¬ (⊣ G)›
by (metis insert_absorb list.set(2))
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›
then have ‹¬ (⊣ A # Neg B # G)›
using * AlphaNegImpl Order ‹¬ (⊣ G)›
by (metis insert_absorb list.set(2))
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 ‹¬ (⊣ A # G) ∨ ¬ (⊣ B # G)›
using * BetaOr Order ‹¬ (⊣ G)›
by (metis insert_absorb list.set(2))
then show ‹S ∪ {A} ∈ ?C ∨ S ∪ {B} ∈ ?C›
using * by auto }

{ fix A B
assume ‹Neg (And A B) ∈ S›
then have ‹¬ (⊣ Neg A # G) ∨ ¬ (⊣ Neg B # G)›
using * BetaNegAnd Order ‹¬ (⊣ G)›
by (metis insert_absorb list.set(2))
then show ‹S ∪ {Neg A} ∈ ?C ∨ S ∪ {Neg B} ∈ ?C›
using * by auto }

{ fix A B
assume ‹Impl A B ∈ S›
then have ‹¬ (⊣ Neg A # G) ∨ ¬ (⊣ B # G)›
using * BetaImpl Order ‹¬ (⊣ G)›
by (metis insert_absorb list.set(2))
then show ‹S ∪ {Neg A} ∈ ?C ∨ S ∪ {B} ∈ ?C›
using * by auto }

{ fix P and t :: ‹'a term›
assume ‹Forall P ∈ S›
then have ‹¬ (⊣ subst P t 0 # G)›
using * GammaForall Order‹¬ (⊣ G)›
by (metis insert_absorb list.set(2))
moreover have ‹S ∪ {subst P t 0} = set (subst P t 0 # G)›
using * by simp
ultimately show ‹S ∪ {subst P t 0} ∈ ?C›
by blast }

{ fix P and t :: ‹'a term›
assume ‹Neg (Exists P) ∈ S›
then have ‹¬ (⊣ Neg (subst P t 0) # G)›
using * GammaNegExists Order ‹¬ (⊣ G)›
by (metis insert_absorb list.set(2))
moreover have ‹S ∪ {Neg (subst P t 0)} = set (Neg (subst P t 0) # G)›
using * by simp
ultimately show ‹S ∪ {Neg (subst P t 0)} ∈ ?C›
by blast }

{ fix P
assume ‹Exists P ∈ S›
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 infinite_UNIV_listI by blast
then obtain x where **: ‹x ∈ - ((⋃p ∈ set G. params p) ∪ params P)›
using infinite_imp_nonempty by blast
then have ‹news x (P # G)›
using Ball_set_list_all by auto
then have ‹¬ (⊣ subst P (App x []) 0 # G)›
using * ‹Exists P ∈ S› Order DeltaExists ‹¬ (⊣ G)›
by (metis insert_absorb list.set(2))
moreover have ‹S ∪ {subst P (App x []) 0} = set (subst P (App x []) 0 # G)›
using * by simp
ultimately show ‹∃x. S ∪ {subst P (App x []) 0} ∈ ?C›
by blast }

{ fix P
assume ‹Neg (Forall P) ∈ S›
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 infinite_UNIV_listI by blast
then obtain x where **: ‹x ∈ - ((⋃p ∈ set G. params p) ∪ params P)›
using infinite_imp_nonempty by blast
then have ‹news x (P # G)›
using Ball_set_list_all by auto
then have ‹¬ (⊣ Neg (subst P (App x []) 0) # G)›
using * ‹Neg (Forall P) ∈ S› Order DeltaNegForall ‹¬ (⊣ G)›
by (metis insert_absorb list.set(2))
moreover have ‹S ∪ {Neg (subst P (App x []) 0)} = set (Neg (subst P (App x []) 0) # G)›
using * by simp
ultimately show ‹∃x. S ∪ {Neg (subst P (App x []) 0)} ∈ ?C›
by blast }
qed

theorem tableau_completeness':
fixes p :: ‹(nat, nat) form›
assumes ‹closed 0 p›
and ‹list_all (closed 0) ps›
and mod: ‹∀(e :: nat ⇒ nat hterm) f g. list_all (eval e f g) ps ⟶ eval e f g p›
shows ‹tableauproof ps p›
proof (rule ccontr)
fix e
assume ‹¬ tableauproof ps p›

let ?S = ‹set (Neg p # ps)›
let ?C = ‹{set (G :: (nat, nat) form list) | G. ¬ (⊣ G)}›
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›

{ fix x
assume ‹x ∈ ?S›
moreover have ‹consistency ?C›
using TCd_consistency by blast
moreover have ‹?S ∈ ?C›
using ‹¬ tableauproof ps p› unfolding tableauproof_def by blast
moreover have ‹infinite (- (⋃p ∈ ?S. params p))›
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)›
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 by blast
ultimately show False by simp
qed

subsection ‹Open Formulas›

lemma TC_psubst:
fixes f :: ‹'a ⇒ 'a›
assumes inf_params: ‹infinite (UNIV :: 'a set)›
shows ‹⊣ G ⟹ ⊣ map (psubst f) G›
proof (induct G arbitrary: f rule: TC.induct)
case (DeltaExists A n G)
let ?params = ‹params A ∪ (⋃p ∈ set G. params p)›

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

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

have ‹news n (A # G)›
using DeltaExists by blast
then have ‹new fresh (psubst ?f A)› ‹news fresh (map (psubst ?f) G)›
using * new_psubst_image news_psubst by (fastforce simp add: image_Un)+
then have G: ‹map (psubst ?f) G = map (psubst f) G›
using DeltaExists
by (metis (mono_tags, lifting) Ball_set insertCI list.set(2) map_eq_conv psubst_upd)

have ‹⊣ psubst ?f (subst A (App n []) 0) # map (psubst ?f) G›
using DeltaExists by (metis list.simps(9))
then have ‹⊣ subst (psubst ?f A) (App fresh []) 0 # map (psubst ?f) G›
by simp
moreover have ‹news fresh (map (psubst ?f) (A # G))›
using ‹new fresh (psubst ?f A)› ‹news fresh (map (psubst ?f) G)› by simp
then have ‹news fresh (psubst ?f A # map (psubst ?f) G)›
by simp
ultimately have ‹⊣ map (psubst ?f) (Exists A # G)›
using TC.DeltaExists by fastforce
then show ?case
using DeltaExists G by simp
next
case (DeltaNegForall A n G)
let ?params = ‹params A ∪ (⋃p ∈ set G. params p)›

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

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

have ‹news n (A # G)›
using DeltaNegForall by blast
then have ‹new fresh (psubst ?f A)› ‹news fresh (map (psubst ?f) G)›
using * new_psubst_image news_psubst by (fastforce simp add: image_Un)+
then have G: ‹map (psubst ?f) G = map (psubst f) G›
using DeltaNegForall
by (metis (mono_tags, lifting) Ball_set insertCI list.set(2) map_eq_conv psubst_upd)

have ‹⊣ psubst ?f (Neg (subst A (App n []) 0)) # map (psubst ?f) G›
using DeltaNegForall by (metis list.simps(9))
then have ‹⊣ Neg (subst (psubst ?f A) (App fresh []) 0) # map (psubst ?f) G›
by simp
moreover have ‹news fresh (map (psubst ?f) (A # G))›
using ‹new fresh (psubst ?f A)› ‹news fresh (map (psubst ?f) G)› by simp
then have ‹news fresh (psubst ?f A # map (psubst ?f) G)›
by simp
ultimately have ‹⊣ map (psubst ?f) (Neg (Forall A) # G)›
using TC.DeltaNegForall by fastforce
then show ?case
using DeltaNegForall G by simp
next
case (Order G G')
then show ?case
using Order TC.Order set_map by metis
qed (auto intro: TC.intros)

lemma subcs_map: ‹subcs c s G = map (subc c s) G›
by (induct G) simp_all

lemma TC_subcs:
fixes G :: ‹('a, 'b) form list›
assumes inf_params: ‹infinite (UNIV :: 'a set)›
shows ‹⊣ G ⟹ ⊣ subcs c s G›
proof (induct G arbitrary: c s rule: TC.induct)
case (GammaForall A t G)
let ?params = ‹params A ∪ (⋃p ∈ set G. params p) ∪ paramst s ∪ paramst t ∪ {c}›

have ‹finite ?params›
by simp
then obtain fresh where fresh: ‹fresh ∉ ?params›
using ex_new_if_finite inf_params by metis

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

have s: ‹psubstt ?g ?s = s›
using fresh psubst_new_away' by simp
have ‹subc (?g c) (psubstt ?g ?s) (psubst ?g (Forall A)) = subc c s (Forall A)›
using fresh by simp
then have A: ‹psubst ?g (subc c ?s (Forall A)) = subc c s (Forall A)›
using fun_upd_apply id_def subc_psubst UnCI fresh params.simps(8) by metis
have ‹∀x ∈ (⋃p ∈ set (Forall A # G). params p). x ≠ c ⟶ ?g x ≠ ?g c›
using fresh by auto
moreover have ‹map (psubst ?g) (Forall A # G) = Forall A # G›
using fresh by (induct G) simp_all
ultimately have G: ‹map (psubst ?g) (subcs c ?s (Forall A # G)) = subcs c s (Forall A # G)›
using s A by (simp add: subcs_psubst)

have ‹new_term c ?s›
using fresh psubst_new_free' by fast
then have ‹⊣ subc c ?s (subst A (subc_term c ?s t) 0) # subcs c ?s G›
using GammaForall by (metis new_subc_put subcs.simps(2))
moreover have ‹new_term c (subc_term c ?s t)›
using ‹new_term c ?s› new_subc_same' by simp
ultimately have ‹⊣ subst (subc c (liftt ?s) A) (subc_term c ?s t) 0 # subcs c ?s G›
by simp
moreover have ‹Forall (subc c (liftt ?s) A) ∈ set (subcs c ?s (Forall A # G))›
by simp
ultimately have ‹⊣ subcs c ?s (Forall A # G)›
using TC.GammaForall by simp
then have ‹⊣ map (psubst ?g) (subcs c ?s (Forall A # G))›
using TC_psubst inf_params by blast
then show ‹⊣ subcs c s (Forall A # G)›
using G by simp
next
case (GammaNegExists A t G)
let ?params = ‹params A ∪ (⋃p ∈ set G. params p) ∪ paramst s ∪ paramst t ∪ {c}›

have ‹finite ?params›
by simp
then obtain fresh where fresh: ‹fresh ∉ ?params›
using ex_new_if_finite inf_params by metis

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

have s: ‹psubstt ?g ?s = s›
using fresh psubst_new_away' by simp
have ‹subc (?g c) (psubstt ?g ?s) (psubst ?g (Neg (Exists A))) = subc c s (Neg (Exists A))›
using fresh by simp
then have A: ‹psubst ?g (subc c ?s (Neg (Exists A))) = subc c s (Neg (Exists A))›
using fun_upd_apply id_def subc_psubst UnCI fresh params.simps(7,9) by metis

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

have ‹new_term c ?s›
using fresh psubst_new_free' by fast
then have ‹⊣ Neg (subc c ?s (subst A (subc_term c ?s t) 0)) # subcs c ?s G›
using GammaNegExists by (metis new_subc_put subc.simps(4) subcs.simps(2))
moreover have ‹new_term c (subc_term c ?s t)›
using ‹new_term c ?s› new_subc_same' by simp
ultimately have ‹⊣ Neg (subst (subc c (liftt ?s) A) (subc_term c ?s t) 0) # subcs c ?s G›
by simp
moreover have ‹Neg (Exists (subc c (liftt ?s) A)) ∈ set (subcs c ?s (Neg (Exists A) # G))›
by simp
ultimately have ‹⊣ subcs c ?s (Neg (Exists A) # G)›
using TC.GammaNegExists by simp
then have ‹⊣ map (psubst ?g) (subcs c ?s (Neg (Exists A) # G))›
using TC_psubst inf_params by blast
then show ‹⊣ subcs c s (Neg (Exists A) # G)›
using G by simp
next
case (DeltaExists A n G)
then show ?case
proof (cases ‹c = n›)
case True
then have ‹⊣ Exists A # G›
using DeltaExists TC.DeltaExists by metis
moreover have ‹new c A› and ‹news c G›
using DeltaExists True by simp_all
ultimately show ?thesis
next
case False
let ?params = ‹params A ∪ (⋃p ∈ set G. params p) ∪ paramst s ∪ {c} ∪ {n}›

have ‹finite ?params›
by simp
then obtain fresh where fresh: ‹fresh ∉ ?params›
using ex_new_if_finite inf_params by metis

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

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

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

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

have ‹psubst ?f (subc c ?s (subst A (App n []) 0)) =
subc (?f c) (psubstt ?f ?s) (psubst ?f (subst A (App n []) 0))›
also have ‹… = subc c s (subst (psubst ?f A) (App fresh []) 0)›
using ‹?f c = c› psubst_subst psubst_s by simp
also have ‹… = subc c s (subst A (App fresh []) 0)›
using DeltaExists fresh by simp
finally have psubst_A: ‹psubst ?f (subc c ?s (subst A (App n []) 0)) =
subst (subc c (liftt s) A) (App fresh []) 0›
using ‹new_term c (App fresh [])› by simp

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

have ‹⊣ subc c ?s (subst A (App n []) 0) # subcs c ?s G›
using DeltaExists by simp
then have ‹⊣ psubst ?f (subc c ?s (subst A (App n []) 0)) # map (psubst ?f) (subcs c ?s G)›
using TC_psubst inf_params DeltaExists.hyps(3) by fastforce
then have ‹⊣ psubst ?f (subc c ?s (subst A (App n []) 0)) # subcs c s G›
using psubst_G by simp
then have sub_A: ‹⊣ subst (subc c (liftt s) A) (App fresh []) 0 # subcs c s G›
using psubst_A by simp

have ‹new_term fresh s›
using fresh by simp
then have ‹new_term fresh (liftt s)›
by simp
then have ‹new fresh (subc c (liftt s) A)›
using fresh new_subc by simp
moreover have ‹news fresh (subcs c s G)›
using ‹news fresh G› ‹new_term fresh s› news_subcs by fast
ultimately show ‹⊣ subcs c s (Exists A # G)›
using TC.DeltaExists sub_A by fastforce
qed
next
case (DeltaNegForall A n G)
then show ?case
proof (cases ‹c = n›)
case True
then have ‹⊣ Neg (Forall A) # G›
using DeltaNegForall TC.DeltaNegForall by metis
moreover have ‹new c A› and ‹news c G›
using DeltaNegForall True by simp_all
ultimately show ?thesis
next
case False
let ?params = ‹params A ∪ (⋃p ∈ set G. params p) ∪ paramst s ∪ {c} ∪ {n}›

have ‹finite ?params›
by simp
then obtain fresh where fresh: ‹fresh ∉ ?params›
using ex_new_if_finite inf_params by metis

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

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

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

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

have ‹psubst ?f (subc c ?s (Neg (subst A (App n []) 0))) =
subc (?f c) (psubstt ?f ?s) (psubst ?f (Neg (subst A (App n []) 0)))›
also have ‹… = subc c s (Neg (subst (psubst ?f A)(App fresh []) 0))›
using ‹?f c = c› psubst_subst psubst_s by simp
also have ‹… = subc c s (Neg (subst A (App fresh []) 0))›
using DeltaNegForall fresh by simp
finally have psubst_A: ‹psubst ?f (subc c ?s (Neg (subst A (App n []) 0))) =
Neg (subst (subc c (liftt s) A) (App fresh []) 0)›
using ‹new_term c (App fresh [])› by simp

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

have ‹⊣ subc c ?s (Neg (subst A (App n []) 0)) # subcs c ?s G›
using DeltaNegForall by simp
then have ‹⊣ psubst ?f (subc c ?s (Neg (subst A (App n []) 0)))
# map (psubst ?f) (subcs c ?s G)›
using TC_psubst inf_params DeltaNegForall.hyps(3) by fastforce
then have ‹⊣ psubst ?f (subc c ?s (Neg (subst A (App n []) 0))) # subcs c s G›
using psubst_G by simp
then have sub_A: ‹⊣ Neg (subst (subc c (liftt s) A) (App fresh []) 0) # subcs c s G›
using psubst_A by simp

have ‹new_term fresh s›
using fresh by simp
then have ‹new_term fresh (liftt s)›
by simp
then have ‹new fresh (subc c (liftt s) A)›
using fresh new_subc by simp
moreover have ‹news fresh (subcs c s G)›
using ‹news fresh G› ‹new_term fresh s› news_subcs by fast
ultimately show ‹⊣ subcs c s (Neg (Forall A) # G)›
using TC.DeltaNegForall sub_A by fastforce
qed
next
case (Order G G')
then show ?case
using TC.Order set_map subcs_map by metis
qed (auto intro: TC.intros)

lemma TC_map_subc:
fixes G :: ‹('a, 'b) form list›
assumes inf_params: ‹infinite (UNIV :: 'a set)›
shows ‹⊣ G ⟹ ⊣ map (subc c s) G›
using assms TC_subcs subcs_map by metis

lemma ex_all_closed: ‹∃m. list_all (closed m) G›
proof (induct G)
case Nil
then show ?case
by simp
next
case (Cons a G)
then show ?case
unfolding list_all_def
using ex_closed closed_mono
by (metis Ball_set list_all_simps(1) nat_le_linear)
qed

primrec sub_consts :: ‹'a list ⇒ ('a, 'b) form ⇒ ('a, 'b) form› where
‹sub_consts [] p = p›
| ‹sub_consts (c # cs) p = sub_consts cs (subst p (App c []) (length cs))›

lemma valid_sub_consts:
assumes ‹∀(e :: nat ⇒ 'a) f g. eval e f g p›
shows ‹eval (e :: nat => 'a) f g (sub_consts cs p)›
using assms by (induct cs arbitrary: p) simp_all

lemma closed_sub' [simp]:
assumes ‹k ≤ m› shows
‹closedt (Suc m) t = closedt m (substt t (App c []) k)›
‹closedts (Suc m) l = closedts m (substts l (App c []) k)›
using assms by (induct t and l rule: closedt.induct closedts.induct) auto

lemma closed_sub: ‹k ≤ m ⟹ closed (Suc m) p = closed m (subst p (App c []) k)›
by (induct p arbitrary: m k) simp_all

lemma closed_sub_consts: ‹length cs = k ⟹ closed m (sub_consts cs p) = closed (m + k) p›
proof (induct cs arbitrary: k p)
case Nil
then show ?case
by simp
next
case (Cons c cs)
then show ?case
using closed_sub by fastforce
qed

lemma map_sub_consts_Nil: ‹map (sub_consts []) G = G›
by (induct G) simp_all

primrec conjoin :: ‹('a, 'b) form list ⇒ ('a, 'b) form› where
‹conjoin [] = Neg ⊥›
| ‹conjoin (p # ps) = And p (conjoin ps)›

lemma eval_conjoin: ‹list_all (eval e f g) G = eval e f g (conjoin G)›
by (induct G) simp_all

lemma valid_sub:
fixes e :: ‹nat ⇒ 'a›
assumes ‹∀(e :: nat ⇒ 'a) f g. eval e f g p ⟶ eval e f g q›
shows ‹eval e f g (subst p t m) ⟶ eval e f g (subst q t m)›
using assms by simp

lemma eval_sub_consts:
fixes e :: ‹nat ⇒ 'a›
assumes ‹∀(e :: nat ⇒ 'a) f g. eval e f g p ⟶ eval e f g q›
and ‹eval e f g (sub_consts cs p)›
shows ‹eval e f g (sub_consts cs q)›
using assms
proof (induct cs arbitrary: p q)
case Nil
then show ?case
by simp
next
case (Cons c cs)
then show ?case
by (metis sub_consts.simps(2) subst_lemma)
qed

lemma sub_consts_And [simp]: ‹sub_consts cs (And p q) = And (sub_consts cs p) (sub_consts cs q)›
by (induct cs arbitrary: p q) simp_all

lemma sub_consts_conjoin:
‹eval e f g (sub_consts cs (conjoin G)) = eval e f g (conjoin (map (sub_consts cs) G))›
proof (induct G)
case Nil
then show ?case
by (induct cs) simp_all
next
case (Cons p G)
then show ?case
using sub_consts_And by simp
qed

lemma all_sub_consts_conjoin:
‹list_all (eval e f g) (map (sub_consts cs) G) = eval e f g (sub_consts cs (conjoin G))›
by (induct G) (simp_all add: valid_sub_consts)

lemma valid_all_sub_consts:
fixes e :: ‹nat ⇒ 'a›
assumes ‹∀(e :: nat ⇒ 'a) f g. list_all (eval e f g) G ⟶ eval e f g p›
shows ‹list_all (eval e f g) (map (sub_consts cs) G) ⟶ eval e f g (sub_consts cs p)›
using assms eval_conjoin eval_sub_consts all_sub_consts_conjoin by metis

lemma TC_vars_for_consts:
fixes G :: ‹('a, 'b) form list›
assumes ‹infinite (UNIV :: 'a set)›
shows ‹⊣ G ⟹ ⊣ map (λp. vars_for_consts p cs) G›
proof (induct cs)
case Nil
then show ?case
by simp
next
case (Cons c cs)
have ‹(⊣ map (λp. vars_for_consts p (c # cs)) G) =
(⊣ map (λp. subc c (Var (length cs)) (vars_for_consts p cs)) G)›
by simp
also have ‹… = (⊣ map (subc c (Var (length cs)) o (λp. vars_for_consts p cs)) G)›
unfolding comp_def by simp
also have ‹… = (⊣ map (subc c (Var (length cs))) (map (λp. vars_for_consts p cs) G))›
by simp
finally show ?case
using Cons TC_map_subc assms by metis
qed

lemma vars_for_consts_sub_consts:
‹closed (length cs) p ⟹ list_all (λc. new c p) cs ⟹ distinct cs ⟹
vars_for_consts (sub_consts cs p) cs = p›
proof (induct cs arbitrary: p)
case (Cons c cs)
then show ?case
using subst_new_all closed_sub by force
qed simp

lemma all_vars_for_consts_sub_consts:
‹list_all (closed (length cs)) G ⟹ list_all (λc. list_all (new c) G) cs ⟹ distinct cs ⟹
map (λp. vars_for_consts p cs) (map (sub_consts cs) G) = G›
using vars_for_consts_sub_consts unfolding list_all_def
by (induct G) fastforce+

lemma new_conjoin: ‹new c (conjoin G) ⟹ list_all (new c) G›
by (induct G) simp_all

lemma all_fresh_constants:
fixes G :: ‹('a, 'b) form list›
assumes ‹infinite (UNIV :: 'a set)›
shows ‹∃cs. length cs = m ∧ list_all (λc. list_all (new c) G) cs ∧ distinct cs›
proof -
obtain cs where ‹length cs = m› ‹list_all (λc. new c (conjoin G)) cs› ‹distinct cs›
using assms fresh_constants by blast
then show ?thesis
using new_conjoin unfolding list_all_def by metis
qed

lemma sub_consts_Neg: ‹sub_consts cs (Neg p) = Neg (sub_consts cs p)›
by (induct cs arbitrary: p) simp_all

subsection ‹Completeness›

theorem tableau_completeness:
fixes G :: ‹(nat, nat) form list›
assumes ‹∀(e :: nat ⇒ nat hterm) f g. list_all (eval e f g) G ⟶ eval e f g p›
shows ‹tableauproof G p›
proof -
obtain m where *: ‹list_all (closed m) (p # G)›
using ex_all_closed by blast
moreover obtain cs where **:
‹length cs = m›
‹distinct cs›
‹list_all (λc. list_all (new c) (p # G)) cs›
using all_fresh_constants by blast
ultimately have ‹closed 0 (sub_consts cs p)›
using closed_sub_consts by fastforce
moreover have ‹list_all (closed 0) (map (sub_consts cs) G)›
using closed_sub_consts * ‹length cs = m› by (induct G) fastforce+

moreover have ‹∀(e :: nat ⇒ nat hterm) f g. list_all (eval e f g) (map (sub_consts cs) G) ⟶
eval e f g (sub_consts cs p)›
using assms valid_all_sub_consts by blast
ultimately have ‹⊣ Neg (sub_consts cs p) # map (sub_consts cs) G›
using tableau_completeness' unfolding tableauproof_def by simp
then have ‹⊣ map (sub_consts cs) (Neg p # G)›
then have ‹⊣ map (λp. vars_for_consts p cs) (map (sub_consts cs) (Neg p # G))›
using TC_vars_for_consts by blast
then show ?thesis
unfolding tableauproof_def
using all_vars_for_consts_sub_consts[where G=‹Neg p # G›] * ** by simp
qed

corollary
fixes p :: ‹(nat, nat) form›
assumes ‹∀(e :: nat ⇒ nat hterm) f g. eval e f g p›
shows ‹⊣ [Neg p]›
using assms tableau_completeness unfolding tableauproof_def by simp

end
```