[STATEMENT]
theorem natded_complete:
  assumes \<open>closed 0 p\<close>
    and \<open>list_all (closed 0) ps\<close>
    and mod: \<open>\<forall>e f g. e,(f :: nat \<Rightarrow> nat hterm list \<Rightarrow> nat hterm),
              (g :: nat \<Rightarrow> nat hterm list \<Rightarrow> bool),ps \<Turnstile> p\<close>
  shows \<open>ps \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps \<turnstile> p
[PROOF STEP]
proof (rule Class, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
fix e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> Neg p # ps \<turnstile> FF\<close>
[PROOF STATE]
proof (state)
this:
\<not> Neg p # ps \<turnstile> FF

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
let ?S = \<open>set (Neg p # ps)\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
let ?C = \<open>{set (G :: (nat, nat) form list) | G. \<not> G \<turnstile> FF}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
let ?f = HApp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
let ?g = \<open>(\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend ?S
              (mk_finite_char (mk_alt_consistency (close ?C))) from_nat)\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
from \<open>list_all (closed 0) ps\<close>
[PROOF STATE]
proof (chain)
picking this:
list_all (closed 0) ps
[PROOF STEP]
have \<open>\<forall>p \<in> set ps. closed 0 p\<close>
[PROOF STATE]
proof (prove)
using this:
list_all (closed 0) ps

goal (1 subgoal):
 1. \<forall>p\<in>set ps. closed 0 p
[PROOF STEP]
by (simp add: list_all_iff)
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set ps. closed 0 p

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set ps. closed 0 p

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
assume \<open>x \<in> ?S\<close>
[PROOF STATE]
proof (state)
this:
x \<in> set (Neg p # ps)

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> set (Neg p # ps)

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
have \<open>consistency ?C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistency {set G |G. \<not> G \<turnstile> FF}
[PROOF STEP]
using deriv_consistency
[PROOF STATE]
proof (prove)
using this:
infinite UNIV \<Longrightarrow> consistency {set G |G. \<not> G \<turnstile> FF}

goal (1 subgoal):
 1. consistency {set G |G. \<not> G \<turnstile> FF}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
consistency {set G |G. \<not> G \<turnstile> FF}

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
consistency {set G |G. \<not> G \<turnstile> FF}

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
have \<open>?S \<in> ?C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (Neg p # ps) \<in> {set G |G. \<not> G \<turnstile> FF}
[PROOF STEP]
using \<open>\<not> Neg p # ps \<turnstile> FF\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> Neg p # ps \<turnstile> FF

goal (1 subgoal):
 1. set (Neg p # ps) \<in> {set G |G. \<not> G \<turnstile> FF}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set (Neg p # ps) \<in> {set G |G. \<not> G \<turnstile> FF}

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (Neg p # ps) \<in> {set G |G. \<not> G \<turnstile> FF}

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
have \<open>infinite (- (\<Union>p \<in> ?S. params p))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (- \<Union> (params ` set (Neg p # ps)))
[PROOF STEP]
by (simp add: Compl_eq_Diff_UNIV)
[PROOF STATE]
proof (state)
this:
infinite (- \<Union> (params ` set (Neg p # ps)))

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
infinite (- \<Union> (params ` set (Neg p # ps)))

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
note \<open>closed 0 p\<close> \<open>\<forall>p \<in> set ps. closed 0 p\<close> \<open>x \<in> ?S\<close>
[PROOF STATE]
proof (state)
this:
closed 0 p
\<forall>p\<in>set ps. closed 0 p
x \<in> set (Neg p # ps)

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closed 0 p
\<forall>p\<in>set ps. closed 0 p
x \<in> set (Neg p # ps)
[PROOF STEP]
have \<open>closed 0 x\<close>
[PROOF STATE]
proof (prove)
using this:
closed 0 p
\<forall>p\<in>set ps. closed 0 p
x \<in> set (Neg p # ps)

goal (1 subgoal):
 1. closed 0 x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closed 0 x

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (Neg p # ps)
consistency {set G |G. \<not> G \<turnstile> FF}
set (Neg p # ps) \<in> {set G |G. \<not> G \<turnstile> FF}
infinite (- \<Union> (params ` set (Neg p # ps)))
closed 0 x
[PROOF STEP]
have \<open>eval e ?f ?g x\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> set (Neg p # ps)
consistency {set G |G. \<not> G \<turnstile> FF}
set (Neg p # ps) \<in> {set G |G. \<not> G \<turnstile> FF}
infinite (- \<Union> (params ` set (Neg p # ps)))
closed 0 x

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) x
[PROOF STEP]
using model_existence
[PROOF STATE]
proof (prove)
using this:
x \<in> set (Neg p # ps)
consistency {set G |G. \<not> G \<turnstile> FF}
set (Neg p # ps) \<in> {set G |G. \<not> G \<turnstile> FF}
infinite (- \<Union> (params ` set (Neg p # ps)))
closed 0 x
\<lbrakk>consistency ?C; ?S \<in> ?C; infinite (- \<Union> (params ` ?S)); ?p \<in> ?S; closed 0 ?p\<rbrakk> \<Longrightarrow> eval ?e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend ?S (mk_finite_char (mk_alt_consistency (close ?C))) from_nat) ?p

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) x

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x3 \<in> set (Neg p # ps) \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) ?x3

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x3 \<in> set (Neg p # ps) \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) ?x3
[PROOF STEP]
have \<open>list_all (eval e ?f ?g) (Neg p # ps)\<close>
[PROOF STATE]
proof (prove)
using this:
?x3 \<in> set (Neg p # ps) \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) ?x3

goal (1 subgoal):
 1. list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) (Neg p # ps)
[PROOF STEP]
by (simp add: list_all_iff)
[PROOF STATE]
proof (state)
this:
list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) (Neg p # ps)

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) (Neg p # ps)

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
have \<open>eval e ?f ?g (Neg p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) (Neg p)
[PROOF STEP]
using calculation
[PROOF STATE]
proof (prove)
using this:
list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) (Neg p # ps)

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) (Neg p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) (Neg p)

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) (Neg p)

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
have \<open>list_all (eval e ?f ?g) ps\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) ps
[PROOF STEP]
using calculation
[PROOF STATE]
proof (prove)
using this:
list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) (Neg p # ps)
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) (Neg p)

goal (1 subgoal):
 1. list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) ps
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) ps

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) ps
[PROOF STEP]
have \<open>eval e ?f ?g p\<close>
[PROOF STATE]
proof (prove)
using this:
list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) ps

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) p
[PROOF STEP]
using mod
[PROOF STATE]
proof (prove)
using this:
list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) ps
\<forall>e f g. e,f,g,ps \<Turnstile> p

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) p
[PROOF STEP]
unfolding model_def
[PROOF STATE]
proof (prove)
using this:
list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) ps
\<forall>e f g. list_all (eval e f g) ps \<longrightarrow> eval e f g p

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) p

goal (1 subgoal):
 1. \<not> Neg p # ps \<turnstile> FF \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) (Neg p # ps)
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) (Neg p)
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) p
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
list_all (eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat)) (Neg p # ps)
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) (Neg p)
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> Extend (set (Neg p # ps)) (mk_finite_char (mk_alt_consistency (close {set G |G. \<not> G \<turnstile> FF}))) from_nat) p

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed