[STATEMENT]
lemma hintikka_Extend_S:
  assumes \<open>consistency C\<close> and \<open>S \<in> C\<close>
    and \<open>infinite (- (\<Union>p \<in> S. params p))\<close>
  shows \<open>hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)\<close>
    (is \<open>hintikka (Extend S ?C' from_nat)\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
have \<open>finite_char ?C'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_char (mk_finite_char (mk_alt_consistency (close C)))
[PROOF STEP]
using finite_char
[PROOF STATE]
proof (prove)
using this:
finite_char (mk_finite_char ?C)

goal (1 subgoal):
 1. finite_char (mk_finite_char (mk_alt_consistency (close C)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite_char (mk_finite_char (mk_alt_consistency (close C)))

goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite_char (mk_finite_char (mk_alt_consistency (close C)))

goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
have \<open>\<forall>y. y = from_nat (to_nat y)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. y = from_nat (to_nat y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>y. y = from_nat (to_nat y)

goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. y = from_nat (to_nat y)
[PROOF STEP]
have \<open>\<forall>y. \<exists>n. y = from_nat n\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>y. y = from_nat (to_nat y)

goal (1 subgoal):
 1. \<forall>y. \<exists>n. y = from_nat n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>y. \<exists>n. y = from_nat n

goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>y. \<exists>n. y = from_nat n

goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
have \<open>alt_consistency ?C'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alt_consistency (mk_finite_char (mk_alt_consistency (close C)))
[PROOF STEP]
using alt_consistency close_closed close_consistency \<open>consistency C\<close>
      finite_alt_consistency mk_alt_consistency_closed
[PROOF STATE]
proof (prove)
using this:
consistency ?C \<Longrightarrow> alt_consistency (mk_alt_consistency ?C)
subset_closed (close ?C)
consistency ?C \<Longrightarrow> consistency (close ?C)
consistency C
\<lbrakk>alt_consistency ?C; subset_closed ?C\<rbrakk> \<Longrightarrow> alt_consistency (mk_finite_char ?C)
subset_closed ?C \<Longrightarrow> subset_closed (mk_alt_consistency ?C)

goal (1 subgoal):
 1. alt_consistency (mk_finite_char (mk_alt_consistency (close C)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
alt_consistency (mk_finite_char (mk_alt_consistency (close C)))

goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
alt_consistency (mk_finite_char (mk_alt_consistency (close C)))

goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
have \<open>S \<in> close C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<in> close C
[PROOF STEP]
using close_subset \<open>S \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
?C \<subseteq> close ?C
S \<in> C

goal (1 subgoal):
 1. S \<in> close C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S \<in> close C

goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S \<in> close C
[PROOF STEP]
have \<open>S \<in> mk_alt_consistency (close C)\<close>
[PROOF STATE]
proof (prove)
using this:
S \<in> close C

goal (1 subgoal):
 1. S \<in> mk_alt_consistency (close C)
[PROOF STEP]
using mk_alt_consistency_subset
[PROOF STATE]
proof (prove)
using this:
S \<in> close C
?C \<subseteq> mk_alt_consistency ?C

goal (1 subgoal):
 1. S \<in> mk_alt_consistency (close C)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S \<in> mk_alt_consistency (close C)

goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S \<in> mk_alt_consistency (close C)
[PROOF STEP]
have \<open>S \<in> ?C'\<close>
[PROOF STATE]
proof (prove)
using this:
S \<in> mk_alt_consistency (close C)

goal (1 subgoal):
 1. S \<in> mk_finite_char (mk_alt_consistency (close C))
[PROOF STEP]
using close_closed finite_char_subset mk_alt_consistency_closed
[PROOF STATE]
proof (prove)
using this:
S \<in> mk_alt_consistency (close C)
subset_closed (close ?C)
subset_closed ?C \<Longrightarrow> ?C \<subseteq> mk_finite_char ?C
subset_closed ?C \<Longrightarrow> subset_closed (mk_alt_consistency ?C)

goal (1 subgoal):
 1. S \<in> mk_finite_char (mk_alt_consistency (close C))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S \<in> mk_finite_char (mk_alt_consistency (close C))

goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite_char (mk_finite_char (mk_alt_consistency (close C)))
\<forall>y. \<exists>n. y = from_nat n
alt_consistency (mk_finite_char (mk_alt_consistency (close C)))
S \<in> mk_finite_char (mk_alt_consistency (close C))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite_char (mk_finite_char (mk_alt_consistency (close C)))
\<forall>y. \<exists>n. y = from_nat n
alt_consistency (mk_finite_char (mk_alt_consistency (close C)))
S \<in> mk_finite_char (mk_alt_consistency (close C))

goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
using extend_hintikka \<open>infinite (- (\<Union>p \<in> S. params p))\<close>
[PROOF STATE]
proof (prove)
using this:
finite_char (mk_finite_char (mk_alt_consistency (close C)))
\<forall>y. \<exists>n. y = from_nat n
alt_consistency (mk_finite_char (mk_alt_consistency (close C)))
S \<in> mk_finite_char (mk_alt_consistency (close C))
\<lbrakk>finite_char ?C; infinite (- \<Union> (params ` ?S)); \<forall>y. \<exists>n. y = ?f n; alt_consistency ?C; ?S \<in> ?C\<rbrakk> \<Longrightarrow> hintikka (Extend ?S ?C ?f)
infinite (- \<Union> (params ` S))

goal (1 subgoal):
 1. hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
hintikka (Extend S (mk_finite_char (mk_alt_consistency (close C))) from_nat)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem model_existence:
  assumes \<open>consistency C\<close>
    and \<open>S \<in> C\<close>
    and \<open>infinite (- (\<Union>p \<in> S. params p))\<close>
    and \<open>p \<in> S\<close>
    and \<open>closed 0 p\<close>
  shows \<open>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\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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
[PROOF STEP]
using assms hintikka_model hintikka_Extend_S Extend_subset
[PROOF STATE]
proof (prove)
using this:
consistency C
S \<in> C
infinite (- \<Union> (params ` S))
p \<in> S
closed 0 p
hintikka ?H \<Longrightarrow> (?p \<in> ?H \<longrightarrow> closed 0 ?p \<longrightarrow> eval ?e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> ?H) ?p) \<and> (Neg ?p \<in> ?H \<longrightarrow> closed 0 ?p \<longrightarrow> eval ?e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> ?H) (Neg ?p))
\<lbrakk>consistency ?C; ?S \<in> ?C; infinite (- \<Union> (params ` ?S))\<rbrakk> \<Longrightarrow> hintikka (Extend ?S (mk_finite_char (mk_alt_consistency (close ?C))) from_nat)
?S \<subseteq> Extend ?S ?C ?f

goal (1 subgoal):
 1. 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
[PROOF STEP]
by blast