Theory FOL_Seq_Calc1.Tableau

(*
    Author: Asta Halkjær From, DTU Compute, 2019-2021
    Contributors: Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen

    See also the Natural Deduction Assistant (NaDeA) and the Sequent Calculus Verifier (SeCaV):

      https://nadea.compute.dtu.dk/
      https://secav.compute.dtu.dk/
*)

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
  by (simp add: Order)

lemma Swap:  B # A # G   A # B # G
  by (simp add: Order insert_commute)

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
  by (simp add: ex_in_conv infinite_imp_nonempty)

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
    by (simp add: list_all_iff)

  { 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))
      by (simp add: Compl_eq_Diff_UNIV infinite_UNIV_listI)
    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 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
      by (simp add: subcs_news)
  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))
      by (simp add: subc_psubst)
    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
      by (simp add: subcs_news)
  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)))
      by (simp add: subc_psubst)
    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)
    by (simp add: sub_consts_Neg)
  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