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