[STATEMENT]
theorem finite_char: \<open>finite_char (mk_finite_char C)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_char (mk_finite_char C)
[PROOF STEP]
unfolding finite_char_def mk_finite_char_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S. (S \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C}) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C})
[PROOF STEP]
by blast


[STATEMENT]
theorem finite_char_closed: \<open>finite_char C \<Longrightarrow> subset_closed C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_char C \<Longrightarrow> subset_closed C
[PROOF STEP]
unfolding finite_char_def subset_closed_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S. (S \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C) \<Longrightarrow> \<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
proof (intro ballI allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S' S. \<lbrakk>\<forall>S. (S \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C); S' \<in> C; S \<subseteq> S'\<rbrakk> \<Longrightarrow> S \<in> C
[PROOF STEP]
fix S S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S' S. \<lbrakk>\<forall>S. (S \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C); S' \<in> C; S \<subseteq> S'\<rbrakk> \<Longrightarrow> S \<in> C
[PROOF STEP]
assume *: \<open>\<forall>S. (S \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C)\<close>
    and \<open>S' \<in> C\<close> and \<open>S \<subseteq> S'\<close>
[PROOF STATE]
proof (state)
this:
\<forall>S. (S \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C)
S' \<in> C
S \<subseteq> S'

goal (1 subgoal):
 1. \<And>S' S. \<lbrakk>\<forall>S. (S \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C); S' \<in> C; S \<subseteq> S'\<rbrakk> \<Longrightarrow> S \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. (S \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C)
S' \<in> C
S \<subseteq> S'
[PROOF STEP]
have \<open>\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (S \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C)
S' \<in> C
S \<subseteq> S'

goal (1 subgoal):
 1. \<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. \<And>S' S. \<lbrakk>\<forall>S. (S \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C); S' \<in> C; S \<subseteq> S'\<rbrakk> \<Longrightarrow> S \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C
[PROOF STEP]
show \<open>S \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. S \<in> C
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C
\<forall>S. (S \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem finite_char_subset: \<open>subset_closed C \<Longrightarrow> C \<subseteq> mk_finite_char C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subset_closed C \<Longrightarrow> C \<subseteq> mk_finite_char C
[PROOF STEP]
unfolding mk_finite_char_def subset_closed_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C \<Longrightarrow> C \<subseteq> {S. \<forall>S'\<subseteq>S. finite S' \<longrightarrow> S' \<in> C}
[PROOF STEP]
by blast


[STATEMENT]
theorem is_chainD: \<open>is_chain f \<Longrightarrow> x \<in> f m \<Longrightarrow> x \<in> f (m + n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_chain f; x \<in> f m\<rbrakk> \<Longrightarrow> x \<in> f (m + n)
[PROOF STEP]
by (induct n) (auto simp: is_chain_def)


[STATEMENT]
theorem is_chainD':
  assumes \<open>is_chain f\<close> and \<open>x \<in> f m\<close> and \<open>m \<le> k\<close>
  shows \<open>x \<in> f k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> f k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> f k
[PROOF STEP]
have \<open>\<exists>n. k = m + n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. k = m + n
[PROOF STEP]
using \<open>m \<le> k\<close>
[PROOF STATE]
proof (prove)
using this:
m \<le> k

goal (1 subgoal):
 1. \<exists>n. k = m + n
[PROOF STEP]
by (simp add: le_iff_add)
[PROOF STATE]
proof (state)
this:
\<exists>n. k = m + n

goal (1 subgoal):
 1. x \<in> f k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. k = m + n
[PROOF STEP]
obtain n where \<open>k = m + n\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>n. k = m + n

goal (1 subgoal):
 1. (\<And>n. k = m + n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k = m + n

goal (1 subgoal):
 1. x \<in> f k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k = m + n
[PROOF STEP]
show \<open>x \<in> f k\<close>
[PROOF STATE]
proof (prove)
using this:
k = m + n

goal (1 subgoal):
 1. x \<in> f k
[PROOF STEP]
using \<open>is_chain f\<close> \<open>x \<in> f m\<close>
[PROOF STATE]
proof (prove)
using this:
k = m + n
is_chain f
x \<in> f m

goal (1 subgoal):
 1. x \<in> f k
[PROOF STEP]
by (simp add: is_chainD)
[PROOF STATE]
proof (state)
this:
x \<in> f k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem chain_index:
  assumes ch: \<open>is_chain f\<close> and fin: \<open>finite F\<close>
  shows \<open>F \<subseteq> (\<Union>n. f n) \<Longrightarrow> \<exists>n. F \<subseteq> f n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
finite F

goal (1 subgoal):
 1. F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n
[PROOF STEP]
proof (induct rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {} \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. {} \<subseteq> f n
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n; insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} \<subseteq> \<Union> (range f)

goal (2 subgoals):
 1. {} \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. {} \<subseteq> f n
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n; insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{} \<subseteq> \<Union> (range f)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
{} \<subseteq> \<Union> (range f)

goal (1 subgoal):
 1. \<exists>n. {} \<subseteq> f n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. {} \<subseteq> f n

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n; insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n; insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n
insert x F \<subseteq> \<Union> (range f)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n; insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite F
x \<notin> F
F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n
insert x F \<subseteq> \<Union> (range f)
[PROOF STEP]
have \<open>\<exists>n. F \<subseteq> f n\<close> and \<open>\<exists>m. x \<in> f m\<close> and \<open>F \<subseteq> (\<Union>x. f x)\<close>
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n
insert x F \<subseteq> \<Union> (range f)

goal (1 subgoal):
 1. \<exists>n. F \<subseteq> f n &&& \<exists>m. x \<in> f m &&& F \<subseteq> \<Union> (range f)
[PROOF STEP]
using ch
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n
insert x F \<subseteq> \<Union> (range f)
is_chain f

goal (1 subgoal):
 1. \<exists>n. F \<subseteq> f n &&& \<exists>m. x \<in> f m &&& F \<subseteq> \<Union> (range f)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<exists>n. F \<subseteq> f n
\<exists>m. x \<in> f m
F \<subseteq> \<Union> (range f)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n; insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. F \<subseteq> f n
\<exists>m. x \<in> f m
F \<subseteq> \<Union> (range f)
[PROOF STEP]
obtain n and m where \<open>F \<subseteq> f n\<close> and \<open>x \<in> f m\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>n. F \<subseteq> f n
\<exists>m. x \<in> f m
F \<subseteq> \<Union> (range f)

goal (1 subgoal):
 1. (\<And>n m. \<lbrakk>F \<subseteq> f n; x \<in> f m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
F \<subseteq> f n
x \<in> f m

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n; insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
have \<open>m \<le> max n m\<close> and \<open>n \<le> max n m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> max n m &&& n \<le> max n m
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
m \<le> max n m
n \<le> max n m

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n; insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
have \<open>x \<in> f (max n m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> f (max n m)
[PROOF STEP]
using is_chainD' ch \<open>x \<in> f m\<close> \<open>m \<le> max n m\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_chain ?f; ?x \<in> ?f ?m; ?m \<le> ?k\<rbrakk> \<Longrightarrow> ?x \<in> ?f ?k
is_chain f
x \<in> f m
m \<le> max n m

goal (1 subgoal):
 1. x \<in> f (max n m)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
x \<in> f (max n m)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n; insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> f (max n m)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n; insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
have \<open>F \<subseteq> f (max n m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<subseteq> f (max n m)
[PROOF STEP]
using is_chainD' ch \<open>F \<subseteq> f n\<close> \<open>n \<le> max n m\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_chain ?f; ?x \<in> ?f ?m; ?m \<le> ?k\<rbrakk> \<Longrightarrow> ?x \<in> ?f ?k
is_chain f
F \<subseteq> f n
n \<le> max n m

goal (1 subgoal):
 1. F \<subseteq> f (max n m)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
F \<subseteq> f (max n m)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n; insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
F \<subseteq> f (max n m)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n; insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
have \<open>x \<in> f (max n m) \<and> F \<subseteq> f (max n m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> f (max n m) \<and> F \<subseteq> f (max n m)
[PROOF STEP]
using calculation
[PROOF STATE]
proof (prove)
using this:
x \<in> f (max n m)
F \<subseteq> f (max n m)

goal (1 subgoal):
 1. x \<in> f (max n m) \<and> F \<subseteq> f (max n m)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> f (max n m) \<and> F \<subseteq> f (max n m)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>n. F \<subseteq> f n; insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> f (max n m)
F \<subseteq> f (max n m)
x \<in> f (max n m) \<and> F \<subseteq> f (max n m)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> f (max n m)
F \<subseteq> f (max n m)
x \<in> f (max n m) \<and> F \<subseteq> f (max n m)

goal (1 subgoal):
 1. \<exists>n. insert x F \<subseteq> f n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. insert x F \<subseteq> f n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain_union_closed':
  assumes \<open>is_chain f\<close> and \<open>(\<forall>n. f n \<in> C)\<close> and \<open>\<forall>S' \<in> C. \<forall>S \<subseteq> S'. S \<in> C\<close>
    and \<open>finite S'\<close> and \<open>S' \<subseteq> (\<Union>n. f n)\<close>
  shows \<open>S' \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
note \<open>finite S'\<close> and \<open>S' \<subseteq> (\<Union>n. f n)\<close>
[PROOF STATE]
proof (state)
this:
finite S'
S' \<subseteq> \<Union> (range f)

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite S'
S' \<subseteq> \<Union> (range f)
[PROOF STEP]
obtain n where \<open>S' \<subseteq> f n\<close>
[PROOF STATE]
proof (prove)
using this:
finite S'
S' \<subseteq> \<Union> (range f)

goal (1 subgoal):
 1. (\<And>n. S' \<subseteq> f n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using chain_index \<open>is_chain f\<close>
[PROOF STATE]
proof (prove)
using this:
finite S'
S' \<subseteq> \<Union> (range f)
\<lbrakk>is_chain ?f; finite ?F; ?F \<subseteq> \<Union> (range ?f)\<rbrakk> \<Longrightarrow> \<exists>n. ?F \<subseteq> ?f n
is_chain f

goal (1 subgoal):
 1. (\<And>n. S' \<subseteq> f n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<subseteq> f n

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' \<subseteq> f n

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
have \<open>f n \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n \<in> C
[PROOF STEP]
using \<open>\<forall>n. f n \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n \<in> C

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

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S' \<subseteq> f n
f n \<in> C
[PROOF STEP]
show \<open>S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> f n
f n \<in> C

goal (1 subgoal):
 1. S' \<in> C
[PROOF STEP]
using \<open>\<forall>S' \<in> C. \<forall>S \<subseteq> S'. S \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S' \<subseteq> f n
f n \<in> C
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem chain_union_closed:
  assumes \<open>finite_char C\<close> and \<open>is_chain f\<close> and \<open>\<forall>n. f n \<in> C\<close>
  shows \<open>(\<Union>n. f n) \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (range f) \<in> C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> (range f) \<in> C
[PROOF STEP]
have \<open>subset_closed C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subset_closed C
[PROOF STEP]
using finite_char_closed \<open>finite_char C\<close>
[PROOF STATE]
proof (prove)
using this:
finite_char ?C \<Longrightarrow> subset_closed ?C
finite_char C

goal (1 subgoal):
 1. subset_closed C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
subset_closed C

goal (1 subgoal):
 1. \<Union> (range f) \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subset_closed C
[PROOF STEP]
have \<open>\<forall>S' \<in> C. \<forall>S \<subseteq> S'. S \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
subset_closed C

goal (1 subgoal):
 1. \<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
using subset_closed_def
[PROOF STATE]
proof (prove)
using this:
subset_closed C
subset_closed ?C = (\<forall>S'\<in>?C. \<forall>S\<subseteq>S'. S \<in> ?C)

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

goal (1 subgoal):
 1. \<Union> (range f) \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
have \<open>\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> (\<Union>n. f n) \<longrightarrow> S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C

goal (1 subgoal):
 1. \<forall>S'. finite S' \<longrightarrow> S' \<subseteq> \<Union> (range f) \<longrightarrow> S' \<in> C
[PROOF STEP]
using chain_union_closed' assms
[PROOF STATE]
proof (prove)
using this:
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
\<lbrakk>is_chain ?f; \<forall>n. ?f n \<in> ?C; \<forall>S'\<in>?C. \<forall>S\<subseteq>S'. S \<in> ?C; finite ?S'; ?S' \<subseteq> \<Union> (range ?f)\<rbrakk> \<Longrightarrow> ?S' \<in> ?C
finite_char C
is_chain f
\<forall>n. f n \<in> C

goal (1 subgoal):
 1. \<forall>S'. finite S' \<longrightarrow> S' \<subseteq> \<Union> (range f) \<longrightarrow> S' \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> \<Union> (range f) \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. \<Union> (range f) \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> \<Union> (range f) \<longrightarrow> S' \<in> C

goal (1 subgoal):
 1. \<Union> (range f) \<in> C
[PROOF STEP]
have \<open>((\<Union>n. f n) \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> (\<Union>n. f n) \<longrightarrow> S' \<in> C)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union> (range f) \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> \<Union> (range f) \<longrightarrow> S' \<in> C)
[PROOF STEP]
using \<open>finite_char C\<close>
[PROOF STATE]
proof (prove)
using this:
finite_char C

goal (1 subgoal):
 1. (\<Union> (range f) \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> \<Union> (range f) \<longrightarrow> S' \<in> C)
[PROOF STEP]
unfolding finite_char_def
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (S \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> S \<longrightarrow> S' \<in> C)

goal (1 subgoal):
 1. (\<Union> (range f) \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> \<Union> (range f) \<longrightarrow> S' \<in> C)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Union> (range f) \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> \<Union> (range f) \<longrightarrow> S' \<in> C)

goal (1 subgoal):
 1. \<Union> (range f) \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> \<Union> (range f) \<longrightarrow> S' \<in> C
(\<Union> (range f) \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> \<Union> (range f) \<longrightarrow> S' \<in> C)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> \<Union> (range f) \<longrightarrow> S' \<in> C
(\<Union> (range f) \<in> C) = (\<forall>S'. finite S' \<longrightarrow> S' \<subseteq> \<Union> (range f) \<longrightarrow> S' \<in> C)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem is_chain_extend: \<open>is_chain (extend S C f)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_chain (extend S C f)
[PROOF STEP]
by (simp add: is_chain_def) blast


[STATEMENT]
theorem finite_paramst [simp]: \<open>finite (paramst (t :: 'a term))\<close>
  \<open>finite (paramsts (ts :: 'a term list))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (paramst t) &&& finite (paramsts ts)
[PROOF STEP]
by (induct t and ts rule: paramst.induct paramsts.induct) (simp_all split: sum.split)


[STATEMENT]
theorem finite_params [simp]: \<open>finite (params p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (params p)
[PROOF STEP]
by (induct p) simp_all


[STATEMENT]
theorem finite_params_extend [simp]:
  \<open>infinite (\<Inter>p \<in> S. - params p) \<Longrightarrow> infinite (\<Inter>p \<in> extend S C f n. - params p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (\<Inter>p\<in>S. - params p) \<Longrightarrow> infinite (\<Inter>p\<in>extend S C f n. - params p)
[PROOF STEP]
by (induct n) simp_all


[STATEMENT]
lemma infinite_params_available:
  assumes \<open>infinite (- (\<Union>p \<in> S. params p))\<close>
  shows \<open>\<exists>x. x \<notin> (\<Union>p \<in> extend S C f n \<union> {f n}. params p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
[PROOF STEP]
let ?S' = \<open>extend S C f n \<union> {f n}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
[PROOF STEP]
have \<open>infinite (- (\<Union>x \<in> ?S'. params x))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (- \<Union> (params ` (extend S C f n \<union> {f n})))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
infinite (- \<Union> (params ` S))

goal (1 subgoal):
 1. infinite (- \<Union> (params ` (extend S C f n \<union> {f n})))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
infinite (- \<Union> (params ` (extend S C f n \<union> {f n})))

goal (1 subgoal):
 1. \<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite (- \<Union> (params ` (extend S C f n \<union> {f n})))
[PROOF STEP]
obtain x where \<open>x \<in> - (\<Union>x \<in> ?S'. params x)\<close>
[PROOF STATE]
proof (prove)
using this:
infinite (- \<Union> (params ` (extend S C f n \<union> {f n})))

goal (1 subgoal):
 1. (\<And>x. x \<in> - \<Union> (params ` (extend S C f n \<union> {f n})) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using infinite_imp_nonempty
[PROOF STATE]
proof (prove)
using this:
infinite (- \<Union> (params ` (extend S C f n \<union> {f n})))
infinite ?S \<Longrightarrow> ?S \<noteq> {}

goal (1 subgoal):
 1. (\<And>x. x \<in> - \<Union> (params ` (extend S C f n \<union> {f n})) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> - \<Union> (params ` (extend S C f n \<union> {f n}))

goal (1 subgoal):
 1. \<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> - \<Union> (params ` (extend S C f n \<union> {f n}))
[PROOF STEP]
have \<open>\<forall>a \<in> ?S'. x \<notin> params a\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> - \<Union> (params ` (extend S C f n \<union> {f n}))

goal (1 subgoal):
 1. \<forall>a\<in>extend S C f n \<union> {f n}. x \<notin> params a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>extend S C f n \<union> {f n}. x \<notin> params a

goal (1 subgoal):
 1. \<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>extend S C f n \<union> {f n}. x \<notin> params a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>extend S C f n \<union> {f n}. x \<notin> params a

goal (1 subgoal):
 1. \<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extend_in_C_Exists:
  assumes \<open>alt_consistency C\<close>
    and \<open>infinite (- (\<Union>p \<in> S. params p))\<close>
    and \<open>extend S C f n \<union> {f n} \<in> C\<close> (is \<open>?S' \<in> C\<close>)
    and \<open>\<exists>p. f n = Exists p\<close>
  shows \<open>extend S C f (Suc n) \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
obtain p where *: \<open>f n = Exists p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. f n = Exists p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<exists>p. f n = Exists p\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>p. f n = Exists p

goal (1 subgoal):
 1. (\<And>p. f n = Exists p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f n = Exists p

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
have \<open>\<exists>x. x \<notin> (\<Union>p \<in> ?S'. params p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
[PROOF STEP]
using \<open>infinite (- (\<Union>p \<in> S. params p))\<close> infinite_params_available
[PROOF STATE]
proof (prove)
using this:
infinite (- \<Union> (params ` S))
infinite (- \<Union> (params ` ?S)) \<Longrightarrow> \<exists>x. x \<notin> \<Union> (params ` (extend ?S ?C ?f ?n \<union> {?f ?n}))

goal (1 subgoal):
 1. \<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
have \<open>Exists p \<in> ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Exists p \<in> extend S C f n \<union> {f n}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
f n = Exists p

goal (1 subgoal):
 1. Exists p \<in> extend S C f n \<union> {f n}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Exists p \<in> extend S C f n \<union> {f n}

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Exists p \<in> extend S C f n \<union> {f n}
[PROOF STEP]
have \<open>\<forall>x. x \<notin> (\<Union>p \<in> ?S'. params p) \<longrightarrow> ?S' \<union> {p[App x []/0]} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Exists p \<in> extend S C f n \<union> {f n}

goal (1 subgoal):
 1. \<forall>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n})) \<longrightarrow> extend S C f n \<union> {f n} \<union> {p[App x []/0]} \<in> C
[PROOF STEP]
using \<open>?S' \<in> C\<close> \<open>alt_consistency C\<close>
[PROOF STATE]
proof (prove)
using this:
Exists p \<in> extend S C f n \<union> {f n}
extend S C f n \<union> {f n} \<in> C
alt_consistency C

goal (1 subgoal):
 1. \<forall>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n})) \<longrightarrow> extend S C f n \<union> {f n} \<union> {p[App x []/0]} \<in> C
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
Exists p \<in> extend S C f n \<union> {f n}
extend S C f n \<union> {f n} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)

goal (1 subgoal):
 1. \<forall>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n})) \<longrightarrow> extend S C f n \<union> {f n} \<union> {p[App x []/0]} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n})) \<longrightarrow> extend S C f n \<union> {f n} \<union> {p[App x []/0]} \<in> C

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
\<forall>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n})) \<longrightarrow> extend S C f n \<union> {f n} \<union> {p[App x []/0]} \<in> C
[PROOF STEP]
have \<open>(?S' \<union> {p[App (SOME k. k \<notin> (\<Union>p \<in> ?S'. params p)) []/0]}) \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
\<forall>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n})) \<longrightarrow> extend S C f n \<union> {f n} \<union> {p[App x []/0]} \<in> C

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<union> {p[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]} \<in> C
[PROOF STEP]
by (metis (mono_tags, lifting) someI2)
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<union> {p[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]} \<in> C

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extend S C f n \<union> {f n} \<union> {p[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]} \<in> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<union> {p[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]} \<in> C

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
using assms *
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<union> {p[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]} \<in> C
alt_consistency C
infinite (- \<Union> (params ` S))
extend S C f n \<union> {f n} \<in> C
\<exists>p. f n = Exists p
f n = Exists p

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
extend S C f (Suc n) \<in> C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extend_in_C_Neg_Forall:
  assumes \<open>alt_consistency C\<close>
    and \<open>infinite (- (\<Union>p \<in> S. params p))\<close>
    and \<open>extend S C f n \<union> {f n} \<in> C\<close> (is \<open>?S' \<in> C\<close>)
    and \<open>\<forall>p. f n \<noteq> Exists p\<close>
    and \<open>\<exists>p. f n = Neg (Forall p)\<close>
  shows \<open>extend S C f (Suc n) \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
obtain p where *: \<open>f n = Neg (Forall p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. f n = Neg (Forall p) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<exists>p. f n = Neg (Forall p)\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>p. f n = Neg (Forall p)

goal (1 subgoal):
 1. (\<And>p. f n = Neg (Forall p) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f n = Neg (Forall p)

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
have \<open>\<exists>x. x \<notin> (\<Union>p \<in> ?S'. params p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
[PROOF STEP]
using \<open>infinite (- (\<Union>p \<in> S. params p))\<close> infinite_params_available
[PROOF STATE]
proof (prove)
using this:
infinite (- \<Union> (params ` S))
infinite (- \<Union> (params ` ?S)) \<Longrightarrow> \<exists>x. x \<notin> \<Union> (params ` (extend ?S ?C ?f ?n \<union> {?f ?n}))

goal (1 subgoal):
 1. \<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
have \<open>Neg (Forall p) \<in> ?S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Neg (Forall p) \<in> extend S C f n \<union> {f n}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
f n = Neg (Forall p)

goal (1 subgoal):
 1. Neg (Forall p) \<in> extend S C f n \<union> {f n}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Neg (Forall p) \<in> extend S C f n \<union> {f n}

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Forall p) \<in> extend S C f n \<union> {f n}
[PROOF STEP]
have \<open>\<forall>x. x \<notin> (\<Union>p \<in> ?S'. params p) \<longrightarrow> ?S' \<union> {Neg (p[App x []/0])} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Forall p) \<in> extend S C f n \<union> {f n}

goal (1 subgoal):
 1. \<forall>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n})) \<longrightarrow> extend S C f n \<union> {f n} \<union> {Neg (p[App x []/0])} \<in> C
[PROOF STEP]
using \<open>?S' \<in> C\<close> \<open>alt_consistency C\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Forall p) \<in> extend S C f n \<union> {f n}
extend S C f n \<union> {f n} \<in> C
alt_consistency C

goal (1 subgoal):
 1. \<forall>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n})) \<longrightarrow> extend S C f n \<union> {f n} \<union> {Neg (p[App x []/0])} \<in> C
[PROOF STEP]
unfolding alt_consistency_def
[PROOF STATE]
proof (prove)
using this:
Neg (Forall p) \<in> extend S C f n \<union> {f n}
extend S C f n \<union> {f n} \<in> C
\<forall>S. S \<in> C \<longrightarrow> (\<forall>p ts. \<not> (Pred p ts \<in> S \<and> Neg (Pred p ts) \<in> S)) \<and> FF \<notin> S \<and> Neg TT \<notin> S \<and> (\<forall>Z. Neg (Neg Z) \<in> S \<longrightarrow> S \<union> {Z} \<in> C) \<and> (\<forall>A B. And A B \<in> S \<longrightarrow> S \<union> {A, B} \<in> C) \<and> (\<forall>A B. Neg (Or A B) \<in> S \<longrightarrow> S \<union> {Neg A, Neg B} \<in> C) \<and> (\<forall>A B. Or A B \<in> S \<longrightarrow> S \<union> {A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (And A B) \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {Neg B} \<in> C) \<and> (\<forall>A B. Impl A B \<in> S \<longrightarrow> S \<union> {Neg A} \<in> C \<or> S \<union> {B} \<in> C) \<and> (\<forall>A B. Neg (Impl A B) \<in> S \<longrightarrow> S \<union> {A, Neg B} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> S \<longrightarrow> S \<union> {P[t/0]} \<in> C) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> S \<longrightarrow> S \<union> {Neg (P[t/0])} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Exists P \<in> S \<longrightarrow> S \<union> {P[App x []/0]} \<in> C) \<and> (\<forall>P x. (\<forall>a\<in>S. x \<notin> params a) \<longrightarrow> Neg (Forall P) \<in> S \<longrightarrow> S \<union> {Neg (P[App x []/0])} \<in> C)

goal (1 subgoal):
 1. \<forall>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n})) \<longrightarrow> extend S C f n \<union> {f n} \<union> {Neg (p[App x []/0])} \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n})) \<longrightarrow> extend S C f n \<union> {f n} \<union> {Neg (p[App x []/0])} \<in> C

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
\<forall>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n})) \<longrightarrow> extend S C f n \<union> {f n} \<union> {Neg (p[App x []/0])} \<in> C
[PROOF STEP]
have \<open>(?S' \<union> {Neg (p[App (SOME k. k \<notin> (\<Union>p \<in> ?S'. params p)) []/0])}) \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))
\<forall>x. x \<notin> \<Union> (params ` (extend S C f n \<union> {f n})) \<longrightarrow> extend S C f n \<union> {f n} \<union> {Neg (p[App x []/0])} \<in> C

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<union> {Neg (p[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])} \<in> C
[PROOF STEP]
by (metis (mono_tags, lifting) someI2)
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<union> {Neg (p[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])} \<in> C

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extend S C f n \<union> {f n} \<union> {Neg (p[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])} \<in> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<union> {Neg (p[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])} \<in> C

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
using assms *
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<union> {Neg (p[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])} \<in> C
alt_consistency C
infinite (- \<Union> (params ` S))
extend S C f n \<union> {f n} \<in> C
\<forall>p. f n \<noteq> Exists p
\<exists>p. f n = Neg (Forall p)
f n = Neg (Forall p)

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
extend S C f (Suc n) \<in> C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extend_in_C_no_delta:
  assumes \<open>extend S C f n \<union> {f n} \<in> C\<close>
    and \<open>\<forall>p. f n \<noteq> Exists p\<close>
    and \<open>\<forall>p. f n \<noteq> Neg (Forall p)\<close>
  shows \<open>extend S C f (Suc n) \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<in> C
\<forall>p. f n \<noteq> Exists p
\<forall>p. f n \<noteq> Neg (Forall p)

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
by simp


[STATEMENT]
lemma extend_in_C_stop:
  assumes \<open>extend S C f n \<in> C\<close>
    and \<open>extend S C f n \<union> {f n} \<notin> C\<close>
  shows \<open>extend S C f (Suc n) \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<in> C
extend S C f n \<union> {f n} \<notin> C

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
by simp


[STATEMENT]
theorem extend_in_C: \<open>alt_consistency C \<Longrightarrow>
  S \<in> C \<Longrightarrow> infinite (- (\<Union>p \<in> S. params p)) \<Longrightarrow> extend S C f n \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f n \<in> C
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f 0 \<in> C
 2. \<And>n. \<lbrakk>\<lbrakk>alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f n \<in> C; alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f (Suc n) \<in> C
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
alt_consistency C
S \<in> C
infinite (- \<Union> (params ` S))

goal (2 subgoals):
 1. \<lbrakk>alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f 0 \<in> C
 2. \<And>n. \<lbrakk>\<lbrakk>alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f n \<in> C; alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f (Suc n) \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
alt_consistency C
S \<in> C
infinite (- \<Union> (params ` S))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
alt_consistency C
S \<in> C
infinite (- \<Union> (params ` S))

goal (1 subgoal):
 1. extend S C f 0 \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
extend S C f 0 \<in> C

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f n \<in> C; alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f (Suc n) \<in> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f n \<in> C; alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f (Suc n) \<in> C
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f n \<in> C
alt_consistency C
S \<in> C
infinite (- \<Union> (params ` S))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f n \<in> C; alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f (Suc n) \<in> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f n \<in> C
alt_consistency C
S \<in> C
infinite (- \<Union> (params ` S))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f n \<in> C
alt_consistency C
S \<in> C
infinite (- \<Union> (params ` S))

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
using extend_in_C_Exists extend_in_C_Neg_Forall
      extend_in_C_no_delta extend_in_C_stop
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>alt_consistency C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> extend S C f n \<in> C
alt_consistency C
S \<in> C
infinite (- \<Union> (params ` S))
\<lbrakk>alt_consistency ?C; infinite (- \<Union> (params ` ?S)); extend ?S ?C ?f ?n \<union> {?f ?n} \<in> ?C; \<exists>p. ?f ?n = Exists p\<rbrakk> \<Longrightarrow> extend ?S ?C ?f (Suc ?n) \<in> ?C
\<lbrakk>alt_consistency ?C; infinite (- \<Union> (params ` ?S)); extend ?S ?C ?f ?n \<union> {?f ?n} \<in> ?C; \<forall>p. ?f ?n \<noteq> Exists p; \<exists>p. ?f ?n = Neg (Forall p)\<rbrakk> \<Longrightarrow> extend ?S ?C ?f (Suc ?n) \<in> ?C
\<lbrakk>extend ?S ?C ?f ?n \<union> {?f ?n} \<in> ?C; \<forall>p. ?f ?n \<noteq> Exists p; \<forall>p. ?f ?n \<noteq> Neg (Forall p)\<rbrakk> \<Longrightarrow> extend ?S ?C ?f (Suc ?n) \<in> ?C
\<lbrakk>extend ?S ?C ?f ?n \<in> ?C; extend ?S ?C ?f ?n \<union> {?f ?n} \<notin> ?C\<rbrakk> \<Longrightarrow> extend ?S ?C ?f (Suc ?n) \<in> ?C

goal (1 subgoal):
 1. extend S C f (Suc n) \<in> C
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
extend S C f (Suc n) \<in> C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Extend_in_C: \<open>alt_consistency C \<Longrightarrow> finite_char C \<Longrightarrow>
  S \<in> C \<Longrightarrow> infinite (- (\<Union>p \<in> S. params p)) \<Longrightarrow> Extend S C f \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alt_consistency C; finite_char C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> Extend S C f \<in> C
[PROOF STEP]
unfolding Extend_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alt_consistency C; finite_char C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> \<Union> (range (extend S C f)) \<in> C
[PROOF STEP]
using chain_union_closed is_chain_extend extend_in_C
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite_char ?C; is_chain ?f; \<forall>n. ?f n \<in> ?C\<rbrakk> \<Longrightarrow> \<Union> (range ?f) \<in> ?C
is_chain (extend ?S ?C ?f)
\<lbrakk>alt_consistency ?C; ?S \<in> ?C; infinite (- \<Union> (params ` ?S))\<rbrakk> \<Longrightarrow> extend ?S ?C ?f ?n \<in> ?C

goal (1 subgoal):
 1. \<lbrakk>alt_consistency C; finite_char C; S \<in> C; infinite (- \<Union> (params ` S))\<rbrakk> \<Longrightarrow> \<Union> (range (extend S C f)) \<in> C
[PROOF STEP]
by blast


[STATEMENT]
theorem Extend_subset: \<open>S \<subseteq> Extend S C f\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> Extend S C f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> x \<in> Extend S C f
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> x \<in> Extend S C f
[PROOF STEP]
assume \<open>x \<in> S\<close>
[PROOF STATE]
proof (state)
this:
x \<in> S

goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> x \<in> Extend S C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> S
[PROOF STEP]
have \<open>x \<in> extend S C f 0\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> S

goal (1 subgoal):
 1. x \<in> extend S C f 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> extend S C f 0

goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> x \<in> Extend S C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> extend S C f 0
[PROOF STEP]
have \<open>\<exists>n. x \<in> extend S C f n\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> extend S C f 0

goal (1 subgoal):
 1. \<exists>n. x \<in> extend S C f n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. x \<in> extend S C f n

goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> x \<in> Extend S C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. x \<in> extend S C f n
[PROOF STEP]
show \<open>x \<in> Extend S C f\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>n. x \<in> extend S C f n

goal (1 subgoal):
 1. x \<in> Extend S C f
[PROOF STEP]
by (simp add: Extend_def)
[PROOF STATE]
proof (state)
this:
x \<in> Extend S C f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem extend_maximal:
  assumes \<open>\<forall>y. \<exists>n. y = f n\<close>
    and \<open>finite_char C\<close>
  shows \<open>maximal (Extend S C f) C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal (Extend S C f) C
[PROOF STEP]
unfolding maximal_def Extend_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S'\<in>C. \<Union> (range (extend S C f)) \<subseteq> S' \<longrightarrow> \<Union> (range (extend S C f)) = S'
[PROOF STEP]
proof (intro ballI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<in> C; \<Union> (range (extend S C f)) \<subseteq> S'\<rbrakk> \<Longrightarrow> \<Union> (range (extend S C f)) = S'
[PROOF STEP]
fix S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<in> C; \<Union> (range (extend S C f)) \<subseteq> S'\<rbrakk> \<Longrightarrow> \<Union> (range (extend S C f)) = S'
[PROOF STEP]
assume \<open>S' \<in> C\<close>
    and \<open>(\<Union>x. extend S C f x) \<subseteq> S'\<close>
[PROOF STATE]
proof (state)
this:
S' \<in> C
\<Union> (range (extend S C f)) \<subseteq> S'

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<in> C; \<Union> (range (extend S C f)) \<subseteq> S'\<rbrakk> \<Longrightarrow> \<Union> (range (extend S C f)) = S'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' \<in> C
\<Union> (range (extend S C f)) \<subseteq> S'

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<in> C; \<Union> (range (extend S C f)) \<subseteq> S'\<rbrakk> \<Longrightarrow> \<Union> (range (extend S C f)) = S'
[PROOF STEP]
have \<open>S' \<subseteq> (\<Union>x. extend S C f x)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S' \<subseteq> \<Union> (range (extend S C f))
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> S' \<subseteq> \<Union> (range (extend S C f)) \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> S' \<subseteq> (\<Union>x. extend S C f x)\<close>
[PROOF STATE]
proof (state)
this:
\<not> S' \<subseteq> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. \<not> S' \<subseteq> \<Union> (range (extend S C f)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> S' \<subseteq> \<Union> (range (extend S C f))
[PROOF STEP]
have \<open>\<exists>z. z \<in> S' \<and> z \<notin> (\<Union>x. extend S C f x)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> S' \<subseteq> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. \<exists>z. z \<in> S' \<and> z \<notin> \<Union> (range (extend S C f))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>z. z \<in> S' \<and> z \<notin> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. \<not> S' \<subseteq> \<Union> (range (extend S C f)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>z. z \<in> S' \<and> z \<notin> \<Union> (range (extend S C f))
[PROOF STEP]
obtain z where \<open>z \<in> S'\<close> and *: \<open>z \<notin> (\<Union>x. extend S C f x)\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>z. z \<in> S' \<and> z \<notin> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> S'; z \<notin> \<Union> (range (extend S C f))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z \<in> S'
z \<notin> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. \<not> S' \<subseteq> \<Union> (range (extend S C f)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> S'
z \<notin> \<Union> (range (extend S C f))
[PROOF STEP]
obtain n where \<open>z = f n\<close>
[PROOF STATE]
proof (prove)
using this:
z \<in> S'
z \<notin> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. (\<And>n. z = f n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<forall>y. \<exists>n. y = f n\<close>
[PROOF STATE]
proof (prove)
using this:
z \<in> S'
z \<notin> \<Union> (range (extend S C f))
\<forall>y. \<exists>n. y = f n

goal (1 subgoal):
 1. (\<And>n. z = f n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z = f n

goal (1 subgoal):
 1. \<not> S' \<subseteq> \<Union> (range (extend S C f)) \<Longrightarrow> False
[PROOF STEP]
from \<open>(\<Union>x. extend S C f x) \<subseteq> S'\<close> \<open>z = f n\<close> \<open>z \<in> S'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Union> (range (extend S C f)) \<subseteq> S'
z = f n
z \<in> S'
[PROOF STEP]
have \<open>extend S C f n \<union> {f n} \<subseteq> S'\<close>
[PROOF STATE]
proof (prove)
using this:
\<Union> (range (extend S C f)) \<subseteq> S'
z = f n
z \<in> S'

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<subseteq> S'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<subseteq> S'

goal (1 subgoal):
 1. \<not> S' \<subseteq> \<Union> (range (extend S C f)) \<Longrightarrow> False
[PROOF STEP]
from \<open>finite_char C\<close>
[PROOF STATE]
proof (chain)
picking this:
finite_char C
[PROOF STEP]
have \<open>subset_closed C\<close>
[PROOF STATE]
proof (prove)
using this:
finite_char C

goal (1 subgoal):
 1. subset_closed C
[PROOF STEP]
using finite_char_closed
[PROOF STATE]
proof (prove)
using this:
finite_char C
finite_char ?C \<Longrightarrow> subset_closed ?C

goal (1 subgoal):
 1. subset_closed C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
subset_closed C

goal (1 subgoal):
 1. \<not> S' \<subseteq> \<Union> (range (extend S C f)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subset_closed C
[PROOF STEP]
have \<open>\<forall>S' \<in> C. \<forall>S \<subseteq> S'. S \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
subset_closed C

goal (1 subgoal):
 1. \<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
unfolding subset_closed_def
[PROOF STATE]
proof (prove)
using this:
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C

goal (1 subgoal):
 1. \<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C

goal (1 subgoal):
 1. \<not> S' \<subseteq> \<Union> (range (extend S C f)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
have \<open>\<forall>S \<subseteq> S'. S \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C

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

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

goal (1 subgoal):
 1. \<not> S' \<subseteq> \<Union> (range (extend S C f)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
have \<open>extend S C f n \<union> {f n} \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>S\<subseteq>S'. S \<in> C

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<in> C
[PROOF STEP]
using \<open>extend S C f n \<union> {f n} \<subseteq> S'\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>S\<subseteq>S'. S \<in> C
extend S C f n \<union> {f n} \<subseteq> S'

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<in> C

goal (1 subgoal):
 1. \<not> S' \<subseteq> \<Union> (range (extend S C f)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extend S C f n \<union> {f n} \<in> C
[PROOF STEP]
have \<open>z \<in> extend S C f (Suc n)\<close>
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<in> C

goal (1 subgoal):
 1. z \<in> extend S C f (Suc n)
[PROOF STEP]
using \<open>z \<notin> (\<Union>x. extend S C f x)\<close> \<open>z = f n\<close>
[PROOF STATE]
proof (prove)
using this:
extend S C f n \<union> {f n} \<in> C
z \<notin> \<Union> (range (extend S C f))
z = f n

goal (1 subgoal):
 1. z \<in> extend S C f (Suc n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z \<in> extend S C f (Suc n)

goal (1 subgoal):
 1. \<not> S' \<subseteq> \<Union> (range (extend S C f)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> extend S C f (Suc n)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
z \<in> extend S C f (Suc n)

goal (1 subgoal):
 1. False
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
z \<in> extend S C f (Suc n)
z \<notin> \<Union> (range (extend S C f))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S' \<subseteq> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. \<And>S'. \<lbrakk>S' \<in> C; \<Union> (range (extend S C f)) \<subseteq> S'\<rbrakk> \<Longrightarrow> \<Union> (range (extend S C f)) = S'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S' \<in> C
\<Union> (range (extend S C f)) \<subseteq> S'
S' \<subseteq> \<Union> (range (extend S C f))
[PROOF STEP]
show \<open>(\<Union>x. extend S C f x) = S'\<close>
[PROOF STATE]
proof (prove)
using this:
S' \<in> C
\<Union> (range (extend S C f)) \<subseteq> S'
S' \<subseteq> \<Union> (range (extend S C f))

goal (1 subgoal):
 1. \<Union> (range (extend S C f)) = S'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Union> (range (extend S C f)) = S'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem herbrand_evalt [simp]:
  \<open>closedt 0 t \<Longrightarrow> term_of_hterm (evalt e HApp t) = t\<close>
  \<open>closedts 0 ts \<Longrightarrow> terms_of_hterms (evalts e HApp ts) = ts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (closedt 0 t \<Longrightarrow> term_of_hterm (evalt e HApp t) = t) &&& (closedts 0 ts \<Longrightarrow> terms_of_hterms (evalts e HApp ts) = ts)
[PROOF STEP]
by (induct t and ts rule: closedt.induct closedts.induct) simp_all


[STATEMENT]
theorem herbrand_evalt' [simp]:
  \<open>evalt e HApp (term_of_hterm ht) = ht\<close>
  \<open>evalts e HApp (terms_of_hterms hts) = hts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evalt e HApp (term_of_hterm ht) = ht &&& evalts e HApp (terms_of_hterms hts) = hts
[PROOF STEP]
by (induct ht and hts rule: term_of_hterm.induct terms_of_hterms.induct) simp_all


[STATEMENT]
theorem closed_hterm [simp]:
  \<open>closedt 0 (term_of_hterm (ht::'a hterm))\<close>
  \<open>closedts 0 (terms_of_hterms (hts::'a hterm list))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedt 0 (term_of_hterm ht) &&& closedts 0 (terms_of_hterms hts)
[PROOF STEP]
by (induct ht and hts rule: term_of_hterm.induct terms_of_hterms.induct) simp_all