(* Author: Asta Halkjær From, DTU Compute, 2019 Contributors: Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen See also the Natural Deduction Assistant: https://nadea.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