[STATEMENT]
lemma consistent_witness:
  fixes p :: \<open>('f, 'p) fm\<close>
  assumes \<open>consistent S\<close> and \<open>p \<in> S\<close> and \<open>vars S \<subseteq> used\<close> and \<open>finite used\<close>
  shows \<open>consistent (witness used p \<union> S)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent (witness used p \<union> S)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
consistent S
p \<in> S
vars S \<subseteq> used
finite used

goal (1 subgoal):
 1. consistent (witness used p \<union> S)
[PROOF STEP]
proof (induct used p rule: witness.induct)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>used p. \<lbrakk>consistent S; \<^bold>\<not> \<^bold>\<forall> p \<in> S; vars S \<subseteq> used; finite used\<rbrakk> \<Longrightarrow> consistent (witness used (\<^bold>\<not> \<^bold>\<forall> p) \<union> S)
 2. \<And>uu_. \<lbrakk>consistent S; \<^bold>\<bottom> \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ \<^bold>\<bottom> \<union> S)
 3. \<And>uu_ v va. \<lbrakk>consistent S; \<^bold>\<ddagger> v va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> v va) \<union> S)
 4. \<And>uu_ va. \<lbrakk>consistent S; \<^bold>\<bottom> \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<bottom> \<^bold>\<longrightarrow> va) \<union> S)
 5. \<And>uu_ vb vc va. \<lbrakk>consistent S; \<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va) \<union> S)
 6. \<And>uu_ vb vc va. \<lbrakk>consistent S; (vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ ((vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va) \<union> S)
 7. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc) \<union> S)
 8. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc) \<union> S)
 9. \<And>uu_ v vb. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<forall> vb \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<forall> vb) \<union> S)
 10. \<And>uu_ v. \<lbrakk>consistent S; \<^bold>\<forall> v \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<forall> v) \<union> S)
[PROOF STEP]
case (1 used p)
[PROOF STATE]
proof (state)
this:
consistent S
\<^bold>\<not> \<^bold>\<forall> p \<in> S
vars S \<subseteq> used
finite used

goal (10 subgoals):
 1. \<And>used p. \<lbrakk>consistent S; \<^bold>\<not> \<^bold>\<forall> p \<in> S; vars S \<subseteq> used; finite used\<rbrakk> \<Longrightarrow> consistent (witness used (\<^bold>\<not> \<^bold>\<forall> p) \<union> S)
 2. \<And>uu_. \<lbrakk>consistent S; \<^bold>\<bottom> \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ \<^bold>\<bottom> \<union> S)
 3. \<And>uu_ v va. \<lbrakk>consistent S; \<^bold>\<ddagger> v va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> v va) \<union> S)
 4. \<And>uu_ va. \<lbrakk>consistent S; \<^bold>\<bottom> \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<bottom> \<^bold>\<longrightarrow> va) \<union> S)
 5. \<And>uu_ vb vc va. \<lbrakk>consistent S; \<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va) \<union> S)
 6. \<And>uu_ vb vc va. \<lbrakk>consistent S; (vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ ((vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va) \<union> S)
 7. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc) \<union> S)
 8. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc) \<union> S)
 9. \<And>uu_ v vb. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<forall> vb \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<forall> vb) \<union> S)
 10. \<And>uu_ v. \<lbrakk>consistent S; \<^bold>\<forall> v \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<forall> v) \<union> S)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
consistent S
\<^bold>\<not> \<^bold>\<forall> p \<in> S
vars S \<subseteq> used
finite used

goal (10 subgoals):
 1. \<And>used p. \<lbrakk>consistent S; \<^bold>\<not> \<^bold>\<forall> p \<in> S; vars S \<subseteq> used; finite used\<rbrakk> \<Longrightarrow> consistent (witness used (\<^bold>\<not> \<^bold>\<forall> p) \<union> S)
 2. \<And>uu_. \<lbrakk>consistent S; \<^bold>\<bottom> \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ \<^bold>\<bottom> \<union> S)
 3. \<And>uu_ v va. \<lbrakk>consistent S; \<^bold>\<ddagger> v va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> v va) \<union> S)
 4. \<And>uu_ va. \<lbrakk>consistent S; \<^bold>\<bottom> \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<bottom> \<^bold>\<longrightarrow> va) \<union> S)
 5. \<And>uu_ vb vc va. \<lbrakk>consistent S; \<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va) \<union> S)
 6. \<And>uu_ vb vc va. \<lbrakk>consistent S; (vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ ((vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va) \<union> S)
 7. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc) \<union> S)
 8. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc) \<union> S)
 9. \<And>uu_ v vb. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<forall> vb \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<forall> vb) \<union> S)
 10. \<And>uu_ v. \<lbrakk>consistent S; \<^bold>\<forall> v \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<forall> v) \<union> S)
[PROOF STEP]
have \<open>\<exists>n. max_set used < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. max_set used < n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. max_set used < n

goal (10 subgoals):
 1. \<And>used p. \<lbrakk>consistent S; \<^bold>\<not> \<^bold>\<forall> p \<in> S; vars S \<subseteq> used; finite used\<rbrakk> \<Longrightarrow> consistent (witness used (\<^bold>\<not> \<^bold>\<forall> p) \<union> S)
 2. \<And>uu_. \<lbrakk>consistent S; \<^bold>\<bottom> \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ \<^bold>\<bottom> \<union> S)
 3. \<And>uu_ v va. \<lbrakk>consistent S; \<^bold>\<ddagger> v va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> v va) \<union> S)
 4. \<And>uu_ va. \<lbrakk>consistent S; \<^bold>\<bottom> \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<bottom> \<^bold>\<longrightarrow> va) \<union> S)
 5. \<And>uu_ vb vc va. \<lbrakk>consistent S; \<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va) \<union> S)
 6. \<And>uu_ vb vc va. \<lbrakk>consistent S; (vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ ((vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va) \<union> S)
 7. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc) \<union> S)
 8. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc) \<union> S)
 9. \<And>uu_ v vb. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<forall> vb \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<forall> vb) \<union> S)
 10. \<And>uu_ v. \<lbrakk>consistent S; \<^bold>\<forall> v \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<forall> v) \<union> S)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
consistent S
\<^bold>\<not> \<^bold>\<forall> p \<in> S
vars S \<subseteq> used
finite used
\<exists>n. max_set used < n
[PROOF STEP]
obtain n where n: \<open>witness used (\<^bold>\<not> \<^bold>\<forall>p) = {\<^bold>\<not> p\<langle>\<^bold>#n/0\<rangle>}\<close> and \<open>max_set used < n\<close>
[PROOF STATE]
proof (prove)
using this:
consistent S
\<^bold>\<not> \<^bold>\<forall> p \<in> S
vars S \<subseteq> used
finite used
\<exists>n. max_set used < n

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>witness used (\<^bold>\<not> \<^bold>\<forall> p) = {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>}; max_set used < n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis someI_ex witness.simps(1))
[PROOF STATE]
proof (state)
this:
witness used (\<^bold>\<not> \<^bold>\<forall> p) = {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>}
max_set used < n

goal (10 subgoals):
 1. \<And>used p. \<lbrakk>consistent S; \<^bold>\<not> \<^bold>\<forall> p \<in> S; vars S \<subseteq> used; finite used\<rbrakk> \<Longrightarrow> consistent (witness used (\<^bold>\<not> \<^bold>\<forall> p) \<union> S)
 2. \<And>uu_. \<lbrakk>consistent S; \<^bold>\<bottom> \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ \<^bold>\<bottom> \<union> S)
 3. \<And>uu_ v va. \<lbrakk>consistent S; \<^bold>\<ddagger> v va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> v va) \<union> S)
 4. \<And>uu_ va. \<lbrakk>consistent S; \<^bold>\<bottom> \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<bottom> \<^bold>\<longrightarrow> va) \<union> S)
 5. \<And>uu_ vb vc va. \<lbrakk>consistent S; \<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va) \<union> S)
 6. \<And>uu_ vb vc va. \<lbrakk>consistent S; (vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ ((vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va) \<union> S)
 7. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc) \<union> S)
 8. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc) \<union> S)
 9. \<And>uu_ v vb. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<forall> vb \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<forall> vb) \<union> S)
 10. \<And>uu_ v. \<lbrakk>consistent S; \<^bold>\<forall> v \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<forall> v) \<union> S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
witness used (\<^bold>\<not> \<^bold>\<forall> p) = {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>}
max_set used < n
[PROOF STEP]
have \<open>max_set (vars S) < n\<close>
[PROOF STATE]
proof (prove)
using this:
witness used (\<^bold>\<not> \<^bold>\<forall> p) = {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>}
max_set used < n

goal (1 subgoal):
 1. max_set (vars S) < n
[PROOF STEP]
using 1(3-4) max_list_mono order_le_less_trans
[PROOF STATE]
proof (prove)
using this:
witness used (\<^bold>\<not> \<^bold>\<forall> p) = {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>}
max_set used < n
vars S \<subseteq> used
finite used
set ?xs \<subseteq> set ?ys \<Longrightarrow> max_list ?xs \<le> max_list ?ys
\<lbrakk>?x \<le> ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. max_set (vars S) < n
[PROOF STEP]
by (metis (no_types, lifting) Max.subset_imp bot.extremum_uniqueI less_nat_zero_code linorder_neqE_nat max_set_def)
[PROOF STATE]
proof (state)
this:
max_set (vars S) < n

goal (10 subgoals):
 1. \<And>used p. \<lbrakk>consistent S; \<^bold>\<not> \<^bold>\<forall> p \<in> S; vars S \<subseteq> used; finite used\<rbrakk> \<Longrightarrow> consistent (witness used (\<^bold>\<not> \<^bold>\<forall> p) \<union> S)
 2. \<And>uu_. \<lbrakk>consistent S; \<^bold>\<bottom> \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ \<^bold>\<bottom> \<union> S)
 3. \<And>uu_ v va. \<lbrakk>consistent S; \<^bold>\<ddagger> v va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> v va) \<union> S)
 4. \<And>uu_ va. \<lbrakk>consistent S; \<^bold>\<bottom> \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<bottom> \<^bold>\<longrightarrow> va) \<union> S)
 5. \<And>uu_ vb vc va. \<lbrakk>consistent S; \<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va) \<union> S)
 6. \<And>uu_ vb vc va. \<lbrakk>consistent S; (vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ ((vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va) \<union> S)
 7. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc) \<union> S)
 8. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc) \<union> S)
 9. \<And>uu_ v vb. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<forall> vb \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<forall> vb) \<union> S)
 10. \<And>uu_ v. \<lbrakk>consistent S; \<^bold>\<forall> v \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<forall> v) \<union> S)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
max_set (vars S) < n

goal (10 subgoals):
 1. \<And>used p. \<lbrakk>consistent S; \<^bold>\<not> \<^bold>\<forall> p \<in> S; vars S \<subseteq> used; finite used\<rbrakk> \<Longrightarrow> consistent (witness used (\<^bold>\<not> \<^bold>\<forall> p) \<union> S)
 2. \<And>uu_. \<lbrakk>consistent S; \<^bold>\<bottom> \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ \<^bold>\<bottom> \<union> S)
 3. \<And>uu_ v va. \<lbrakk>consistent S; \<^bold>\<ddagger> v va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> v va) \<union> S)
 4. \<And>uu_ va. \<lbrakk>consistent S; \<^bold>\<bottom> \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<bottom> \<^bold>\<longrightarrow> va) \<union> S)
 5. \<And>uu_ vb vc va. \<lbrakk>consistent S; \<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va) \<union> S)
 6. \<And>uu_ vb vc va. \<lbrakk>consistent S; (vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ ((vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va) \<union> S)
 7. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc) \<union> S)
 8. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc) \<union> S)
 9. \<And>uu_ v vb. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<forall> vb \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<forall> vb) \<union> S)
 10. \<And>uu_ v. \<lbrakk>consistent S; \<^bold>\<forall> v \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<forall> v) \<union> S)
[PROOF STEP]
have \<open>finite (vars S)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (vars S)
[PROOF STEP]
using 1(3-4) infinite_super
[PROOF STATE]
proof (prove)
using this:
vars S \<subseteq> used
finite used
\<lbrakk>?S \<subseteq> ?T; infinite ?S\<rbrakk> \<Longrightarrow> infinite ?T

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

goal (10 subgoals):
 1. \<And>used p. \<lbrakk>consistent S; \<^bold>\<not> \<^bold>\<forall> p \<in> S; vars S \<subseteq> used; finite used\<rbrakk> \<Longrightarrow> consistent (witness used (\<^bold>\<not> \<^bold>\<forall> p) \<union> S)
 2. \<And>uu_. \<lbrakk>consistent S; \<^bold>\<bottom> \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ \<^bold>\<bottom> \<union> S)
 3. \<And>uu_ v va. \<lbrakk>consistent S; \<^bold>\<ddagger> v va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> v va) \<union> S)
 4. \<And>uu_ va. \<lbrakk>consistent S; \<^bold>\<bottom> \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<bottom> \<^bold>\<longrightarrow> va) \<union> S)
 5. \<And>uu_ vb vc va. \<lbrakk>consistent S; \<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va) \<union> S)
 6. \<And>uu_ vb vc va. \<lbrakk>consistent S; (vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ ((vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va) \<union> S)
 7. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc) \<union> S)
 8. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc) \<union> S)
 9. \<And>uu_ v vb. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<forall> vb \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<forall> vb) \<union> S)
 10. \<And>uu_ v. \<lbrakk>consistent S; \<^bold>\<forall> v \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<forall> v) \<union> S)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
max_set (vars S) < n
finite (vars S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
max_set (vars S) < n
finite (vars S)

goal (1 subgoal):
 1. consistent (witness used (\<^bold>\<not> \<^bold>\<forall> p) \<union> S)
[PROOF STEP]
using 1 n(1) consistent_add_witness
[PROOF STATE]
proof (prove)
using this:
max_set (vars S) < n
finite (vars S)
consistent S
\<^bold>\<not> \<^bold>\<forall> p \<in> S
vars S \<subseteq> used
finite used
witness used (\<^bold>\<not> \<^bold>\<forall> p) = {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>}
\<lbrakk>consistent ?S; \<^bold>\<not> \<^bold>\<forall> ?p \<in> ?S; finite (vars ?S); max_set (vars ?S) < ?n\<rbrakk> \<Longrightarrow> consistent ({\<^bold>\<not> ?p\<langle>\<^bold># ?n/0\<rangle>} \<union> ?S)

goal (1 subgoal):
 1. consistent (witness used (\<^bold>\<not> \<^bold>\<forall> p) \<union> S)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
consistent (witness used (\<^bold>\<not> \<^bold>\<forall> p) \<union> S)

goal (9 subgoals):
 1. \<And>uu_. \<lbrakk>consistent S; \<^bold>\<bottom> \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ \<^bold>\<bottom> \<union> S)
 2. \<And>uu_ v va. \<lbrakk>consistent S; \<^bold>\<ddagger> v va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> v va) \<union> S)
 3. \<And>uu_ va. \<lbrakk>consistent S; \<^bold>\<bottom> \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<bottom> \<^bold>\<longrightarrow> va) \<union> S)
 4. \<And>uu_ vb vc va. \<lbrakk>consistent S; \<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<ddagger> vb vc \<^bold>\<longrightarrow> va) \<union> S)
 5. \<And>uu_ vb vc va. \<lbrakk>consistent S; (vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ ((vb \<^bold>\<longrightarrow> vc) \<^bold>\<longrightarrow> va) \<union> S)
 6. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<ddagger> vb vc) \<union> S)
 7. \<And>uu_ v vb vc. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> vb \<^bold>\<longrightarrow> vc) \<union> S)
 8. \<And>uu_ v vb. \<lbrakk>consistent S; v \<^bold>\<longrightarrow> \<^bold>\<forall> vb \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (v \<^bold>\<longrightarrow> \<^bold>\<forall> vb) \<union> S)
 9. \<And>uu_ v. \<lbrakk>consistent S; \<^bold>\<forall> v \<in> S; vars S \<subseteq> uu_; finite uu_\<rbrakk> \<Longrightarrow> consistent (witness uu_ (\<^bold>\<forall> v) \<union> S)
[PROOF STEP]
qed (auto simp: assms)


[STATEMENT]
lemma consistent_extend:
  fixes f :: \<open>nat \<Rightarrow> ('f, 'p) fm\<close>
  assumes \<open>consistent S\<close> \<open>finite (vars S)\<close>
  shows \<open>consistent (extend S f n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent (extend S f n)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
consistent S
finite (vars S)

goal (1 subgoal):
 1. consistent (extend S f n)
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>consistent S; finite (vars S)\<rbrakk> \<Longrightarrow> consistent (extend S f 0)
 2. \<And>n. \<lbrakk>\<lbrakk>consistent S; finite (vars S)\<rbrakk> \<Longrightarrow> consistent (extend S f n); consistent S; finite (vars S)\<rbrakk> \<Longrightarrow> consistent (extend S f (Suc n))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>consistent S; finite (vars S)\<rbrakk> \<Longrightarrow> consistent (extend S f n)
consistent S
finite (vars S)

goal (2 subgoals):
 1. \<lbrakk>consistent S; finite (vars S)\<rbrakk> \<Longrightarrow> consistent (extend S f 0)
 2. \<And>n. \<lbrakk>\<lbrakk>consistent S; finite (vars S)\<rbrakk> \<Longrightarrow> consistent (extend S f n); consistent S; finite (vars S)\<rbrakk> \<Longrightarrow> consistent (extend S f (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>consistent S; finite (vars S)\<rbrakk> \<Longrightarrow> consistent (extend S f n)
consistent S
finite (vars S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>consistent S; finite (vars S)\<rbrakk> \<Longrightarrow> consistent (extend S f n)
consistent S
finite (vars S)

goal (1 subgoal):
 1. consistent (extend S f (Suc n))
[PROOF STEP]
using consistent_witness[where S=\<open>{f n} \<union> _\<close>]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>consistent S; finite (vars S)\<rbrakk> \<Longrightarrow> consistent (extend S f n)
consistent S
finite (vars S)
\<lbrakk>consistent ({f n} \<union> ?uu4); ?p \<in> {f n} \<union> ?uu4; vars ({f n} \<union> ?uu4) \<subseteq> ?used; finite ?used\<rbrakk> \<Longrightarrow> consistent (witness ?used ?p \<union> ({f n} \<union> ?uu4))

goal (1 subgoal):
 1. consistent (extend S f (Suc n))
[PROOF STEP]
by (auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
consistent (extend S f (Suc n))

goal (1 subgoal):
 1. \<lbrakk>consistent S; finite (vars S)\<rbrakk> \<Longrightarrow> consistent (extend S f 0)
[PROOF STEP]
qed simp


[STATEMENT]
lemma consistent_Extend:
  fixes f :: \<open>nat \<Rightarrow> ('f, 'p) fm\<close>
  assumes \<open>consistent S\<close> \<open>finite (vars S)\<close>
  shows \<open>consistent (Extend S f)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent (Extend S f)
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<exists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (state)
this:
\<exists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
obtain S' where \<open>S' \<turnstile> \<^bold>\<bottom>\<close> and \<open>set S' \<subseteq> Extend S f\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>S' \<turnstile> \<^bold>\<bottom>; set S' \<subseteq> Extend S f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
\<exists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>S' \<turnstile> \<^bold>\<bottom>; set S' \<subseteq> Extend S f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<turnstile> \<^bold>\<bottom>
set S' \<subseteq> Extend S f

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' \<turnstile> \<^bold>\<bottom>
set S' \<subseteq> Extend S f
[PROOF STEP]
obtain m where \<open>set S' \<subseteq> (\<Union>n \<le> m. extend S f n)\<close>
[PROOF STATE]
proof (prove)
using this:
S' \<turnstile> \<^bold>\<bottom>
set S' \<subseteq> Extend S f

goal (1 subgoal):
 1. (\<And>m. set S' \<subseteq> \<Union> (extend S f ` {..m}) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Extend_def
[PROOF STATE]
proof (prove)
using this:
S' \<turnstile> \<^bold>\<bottom>
set S' \<subseteq> \<Union> (range (extend S f))

goal (1 subgoal):
 1. (\<And>m. set S' \<subseteq> \<Union> (extend S f ` {..m}) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using UN_finite_bound
[PROOF STATE]
proof (prove)
using this:
S' \<turnstile> \<^bold>\<bottom>
set S' \<subseteq> \<Union> (range (extend S f))
\<lbrakk>finite ?A; ?A \<subseteq> \<Union> (range ?f)\<rbrakk> \<Longrightarrow> \<exists>m. ?A \<subseteq> \<Union> (?f ` {..m})

goal (1 subgoal):
 1. (\<And>m. set S' \<subseteq> \<Union> (extend S f ` {..m}) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis List.finite_set)
[PROOF STATE]
proof (state)
this:
set S' \<subseteq> \<Union> (extend S f ` {..m})

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set S' \<subseteq> \<Union> (extend S f ` {..m})
[PROOF STEP]
have \<open>set S' \<subseteq> extend S f m\<close>
[PROOF STATE]
proof (prove)
using this:
set S' \<subseteq> \<Union> (extend S f ` {..m})

goal (1 subgoal):
 1. set S' \<subseteq> extend S f m
[PROOF STEP]
using extend_bound
[PROOF STATE]
proof (prove)
using this:
set S' \<subseteq> \<Union> (extend S f ` {..m})
\<Union> (extend ?S ?f ` {..?m}) = extend ?S ?f ?m

goal (1 subgoal):
 1. set S' \<subseteq> extend S f m
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set S' \<subseteq> extend S f m

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set S' \<subseteq> extend S f m

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
have \<open>consistent (extend S f m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent (extend S f m)
[PROOF STEP]
using assms consistent_extend
[PROOF STATE]
proof (prove)
using this:
consistent S
finite (vars S)
\<lbrakk>consistent ?S; finite (vars ?S)\<rbrakk> \<Longrightarrow> consistent (extend ?S ?f ?n)

goal (1 subgoal):
 1. consistent (extend S f m)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
consistent (extend S f m)

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set S' \<subseteq> extend S f m
consistent (extend S f m)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
set S' \<subseteq> extend S f m
consistent (extend S f m)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
set S' \<subseteq> extend S f m
\<nexists>S'. set S' \<subseteq> extend S f m \<and> S' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>S' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
using this:
set S' \<subseteq> extend S f m
\<nexists>S'. set S' \<subseteq> extend S f m \<and> S' \<turnstile> \<^bold>\<bottom>
S' \<turnstile> \<^bold>\<bottom>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma maximal_exactly_one:
  assumes \<open>consistent S\<close> and \<open>maximal S\<close>
  shows \<open>p \<in> S \<longleftrightarrow> (\<^bold>\<not> p) \<notin> S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<in> S) = (\<^bold>\<not> p \<notin> S)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> S \<Longrightarrow> \<^bold>\<not> p \<notin> S
 2. \<^bold>\<not> p \<notin> S \<Longrightarrow> p \<in> S
[PROOF STEP]
assume \<open>p \<in> S\<close>
[PROOF STATE]
proof (state)
this:
p \<in> S

goal (2 subgoals):
 1. p \<in> S \<Longrightarrow> \<^bold>\<not> p \<notin> S
 2. \<^bold>\<not> p \<notin> S \<Longrightarrow> p \<in> S
[PROOF STEP]
show \<open>(\<^bold>\<not> p) \<notin> S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<not> p \<notin> S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<^bold>\<not> p \<in> S \<Longrightarrow> False
[PROOF STEP]
assume \<open>(\<^bold>\<not> p) \<in> S\<close>
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> p \<in> S

goal (1 subgoal):
 1. \<^bold>\<not> p \<in> S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<not> p \<in> S
[PROOF STEP]
have \<open>set [p, \<^bold>\<not> p] \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> p \<in> S

goal (1 subgoal):
 1. set [p, \<^bold>\<not> p] \<subseteq> S
[PROOF STEP]
using \<open>p \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> p \<in> S
p \<in> S

goal (1 subgoal):
 1. set [p, \<^bold>\<not> p] \<subseteq> S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set [p, \<^bold>\<not> p] \<subseteq> S

goal (1 subgoal):
 1. \<^bold>\<not> p \<in> S \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set [p, \<^bold>\<not> p] \<subseteq> S

goal (1 subgoal):
 1. \<^bold>\<not> p \<in> S \<Longrightarrow> False
[PROOF STEP]
have \<open>[p, \<^bold>\<not> p] \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [p, \<^bold>\<not> p] \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[p, \<^bold>\<not> p] \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<^bold>\<not> p \<in> S \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set [p, \<^bold>\<not> p] \<subseteq> S
[p, \<^bold>\<not> p] \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
set [p, \<^bold>\<not> p] \<subseteq> S
[p, \<^bold>\<not> p] \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>consistent S\<close>
[PROOF STATE]
proof (prove)
using this:
set [p, \<^bold>\<not> p] \<subseteq> S
[p, \<^bold>\<not> p] \<turnstile> \<^bold>\<bottom>
consistent S

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
set [p, \<^bold>\<not> p] \<subseteq> S
[p, \<^bold>\<not> p] \<turnstile> \<^bold>\<bottom>
\<nexists>S'. set S' \<subseteq> S \<and> S' \<turnstile> \<^bold>\<bottom>

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:
\<^bold>\<not> p \<notin> S

goal (1 subgoal):
 1. \<^bold>\<not> p \<notin> S \<Longrightarrow> p \<in> S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<^bold>\<not> p \<notin> S \<Longrightarrow> p \<in> S
[PROOF STEP]
assume \<open>(\<^bold>\<not> p) \<notin> S\<close>
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> p \<notin> S

goal (1 subgoal):
 1. \<^bold>\<not> p \<notin> S \<Longrightarrow> p \<in> S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<not> p \<notin> S
[PROOF STEP]
have \<open>\<not> consistent ({\<^bold>\<not> p} \<union> S)\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> p \<notin> S

goal (1 subgoal):
 1. \<not> consistent ({\<^bold>\<not> p} \<union> S)
[PROOF STEP]
using \<open>maximal S\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> p \<notin> S
maximal S

goal (1 subgoal):
 1. \<not> consistent ({\<^bold>\<not> p} \<union> S)
[PROOF STEP]
unfolding maximal_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> p \<notin> S
\<forall>p. p \<notin> S \<longrightarrow> \<not> consistent ({p} \<union> S)

goal (1 subgoal):
 1. \<not> consistent ({\<^bold>\<not> p} \<union> S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> consistent ({\<^bold>\<not> p} \<union> S)

goal (1 subgoal):
 1. \<^bold>\<not> p \<notin> S \<Longrightarrow> p \<in> S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> consistent ({\<^bold>\<not> p} \<union> S)
[PROOF STEP]
obtain S' where \<open>set S' \<subseteq> S\<close> \<open>(\<^bold>\<not> p) # S' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> consistent ({\<^bold>\<not> p} \<union> S)

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>set S' \<subseteq> S; \<^bold>\<not> p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>consistent S\<close> inconsistent_fm
[PROOF STATE]
proof (prove)
using this:
\<not> consistent ({\<^bold>\<not> p} \<union> S)
consistent S
\<lbrakk>consistent ?S; \<not> consistent ({?p} \<union> ?S); \<And>S'. \<lbrakk>set S' \<subseteq> ?S; ?p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>set S' \<subseteq> S; \<^bold>\<not> p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set S' \<subseteq> S
\<^bold>\<not> p # S' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<^bold>\<not> p \<notin> S \<Longrightarrow> p \<in> S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set S' \<subseteq> S
\<^bold>\<not> p # S' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
have \<open>S' \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
using this:
set S' \<subseteq> S
\<^bold>\<not> p # S' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. S' \<turnstile> p
[PROOF STEP]
using Boole
[PROOF STATE]
proof (prove)
using this:
set S' \<subseteq> S
\<^bold>\<not> p # S' \<turnstile> \<^bold>\<bottom>
\<^bold>\<not> ?p # ?ps \<turnstile> \<^bold>\<bottom> \<Longrightarrow> ?ps \<turnstile> ?p

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

goal (1 subgoal):
 1. \<^bold>\<not> p \<notin> S \<Longrightarrow> p \<in> S
[PROOF STEP]
have \<open>consistent ({p} \<union> S)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent ({p} \<union> S)
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<exists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (state)
this:
\<exists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
obtain S'' where \<open>set S'' \<subseteq> S\<close> and \<open>p # S'' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. (\<And>S''. \<lbrakk>set S'' \<subseteq> S; p # S'' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms inconsistent_fm
[PROOF STATE]
proof (prove)
using this:
\<exists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>
consistent S
maximal S
\<lbrakk>consistent ?S; \<not> consistent ({?p} \<union> ?S); \<And>S'. \<lbrakk>set S' \<subseteq> ?S; ?p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>S''. \<lbrakk>set S'' \<subseteq> S; p # S'' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
\<exists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>
\<nexists>S'. set S' \<subseteq> S \<and> S' \<turnstile> \<^bold>\<bottom>
maximal S
\<lbrakk>\<nexists>S'. set S' \<subseteq> ?S \<and> S' \<turnstile> \<^bold>\<bottom>; \<not> (\<nexists>S'. set S' \<subseteq> {?p} \<union> ?S \<and> S' \<turnstile> \<^bold>\<bottom>); \<And>S'. \<lbrakk>set S' \<subseteq> ?S; ?p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>S''. \<lbrakk>set S'' \<subseteq> S; p # S'' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set S'' \<subseteq> S
p # S'' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set S'' \<subseteq> S
p # S'' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
have \<open>S' @ S'' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
using this:
set S'' \<subseteq> S
p # S'' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. S' @ S'' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
using \<open>S' \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
using this:
set S'' \<subseteq> S
p # S'' \<turnstile> \<^bold>\<bottom>
S' \<turnstile> p

goal (1 subgoal):
 1. S' @ S'' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
by (metis MP' add_imply imply.simps(2) imply_append)
[PROOF STATE]
proof (state)
this:
S' @ S'' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' @ S'' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
have \<open>set (S' @ S'') \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (S' @ S'') \<subseteq> S
[PROOF STEP]
using \<open>set S' \<subseteq> S\<close> \<open>set S'' \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
set S' \<subseteq> S
set S'' \<subseteq> S

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

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S' @ S'' \<turnstile> \<^bold>\<bottom>
set (S' @ S'') \<subseteq> S
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
S' @ S'' \<turnstile> \<^bold>\<bottom>
set (S' @ S'') \<subseteq> S

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>consistent S\<close>
[PROOF STATE]
proof (prove)
using this:
S' @ S'' \<turnstile> \<^bold>\<bottom>
set (S' @ S'') \<subseteq> S
consistent S

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
S' @ S'' \<turnstile> \<^bold>\<bottom>
set (S' @ S'') \<subseteq> S
\<nexists>S'. set S' \<subseteq> S \<and> S' \<turnstile> \<^bold>\<bottom>

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:
consistent ({p} \<union> S)

goal (1 subgoal):
 1. \<^bold>\<not> p \<notin> S \<Longrightarrow> p \<in> S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
consistent ({p} \<union> S)
[PROOF STEP]
show \<open>p \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
consistent ({p} \<union> S)

goal (1 subgoal):
 1. p \<in> S
[PROOF STEP]
using \<open>maximal S\<close>
[PROOF STATE]
proof (prove)
using this:
consistent ({p} \<union> S)
maximal S

goal (1 subgoal):
 1. p \<in> S
[PROOF STEP]
unfolding maximal_def
[PROOF STATE]
proof (prove)
using this:
consistent ({p} \<union> S)
\<forall>p. p \<notin> S \<longrightarrow> \<not> consistent ({p} \<union> S)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma maximal_Extend:
  assumes \<open>surj f\<close>
  shows \<open>maximal (Extend S f)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal (Extend S f)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> maximal (Extend S f) \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> maximal (Extend S f)\<close>
[PROOF STATE]
proof (state)
this:
\<not> maximal (Extend S f)

goal (1 subgoal):
 1. \<not> maximal (Extend S f) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> maximal (Extend S f)
[PROOF STEP]
obtain p where
    \<open>p \<notin> Extend S f\<close> and \<open>consistent ({p} \<union> Extend S f)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> maximal (Extend S f)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<notin> Extend S f; consistent ({p} \<union> Extend S f)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding maximal_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>p. p \<notin> Extend S f \<longrightarrow> \<not> consistent ({p} \<union> Extend S f))

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<notin> Extend S f; consistent ({p} \<union> Extend S f)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms consistent_Extend
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>p. p \<notin> Extend S f \<longrightarrow> \<not> consistent ({p} \<union> Extend S f))
surj f
\<lbrakk>consistent ?S; finite (vars ?S)\<rbrakk> \<Longrightarrow> consistent (Extend ?S ?f)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<notin> Extend S f; consistent ({p} \<union> Extend S f)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<notin> Extend S f
consistent ({p} \<union> Extend S f)

goal (1 subgoal):
 1. \<not> maximal (Extend S f) \<Longrightarrow> False
[PROOF STEP]
obtain k where k: \<open>f k = p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. f k = p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>surj f\<close>
[PROOF STATE]
proof (prove)
using this:
surj f

goal (1 subgoal):
 1. (\<And>k. f k = p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding surj_def
[PROOF STATE]
proof (prove)
using this:
\<forall>y. \<exists>x. y = f x

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

goal (1 subgoal):
 1. \<not> maximal (Extend S f) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f k = p
[PROOF STEP]
have \<open>p \<notin> extend S f (Suc k)\<close>
[PROOF STATE]
proof (prove)
using this:
f k = p

goal (1 subgoal):
 1. p \<notin> extend S f (Suc k)
[PROOF STEP]
using \<open>p \<notin> Extend S f\<close>
[PROOF STATE]
proof (prove)
using this:
f k = p
p \<notin> Extend S f

goal (1 subgoal):
 1. p \<notin> extend S f (Suc k)
[PROOF STEP]
unfolding Extend_def
[PROOF STATE]
proof (prove)
using this:
f k = p
p \<notin> \<Union> (range (extend S f))

goal (1 subgoal):
 1. p \<notin> extend S f (Suc k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<notin> extend S f (Suc k)

goal (1 subgoal):
 1. \<not> maximal (Extend S f) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<notin> extend S f (Suc k)
[PROOF STEP]
have \<open>\<not> consistent ({p} \<union> extend S f k)\<close>
[PROOF STATE]
proof (prove)
using this:
p \<notin> extend S f (Suc k)

goal (1 subgoal):
 1. \<not> consistent ({p} \<union> extend S f k)
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
p \<notin> extend S f (Suc k)
f k = p

goal (1 subgoal):
 1. \<not> consistent ({p} \<union> extend S f k)
[PROOF STEP]
by (auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
\<not> consistent ({p} \<union> extend S f k)

goal (1 subgoal):
 1. \<not> maximal (Extend S f) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> consistent ({p} \<union> extend S f k)

goal (1 subgoal):
 1. \<not> maximal (Extend S f) \<Longrightarrow> False
[PROOF STEP]
have \<open>{p} \<union> extend S f k \<subseteq> {p} \<union> Extend S f\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p} \<union> extend S f k \<subseteq> {p} \<union> Extend S f
[PROOF STEP]
unfolding Extend_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p} \<union> extend S f k \<subseteq> {p} \<union> \<Union> (range (extend S f))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{p} \<union> extend S f k \<subseteq> {p} \<union> Extend S f

goal (1 subgoal):
 1. \<not> maximal (Extend S f) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> consistent ({p} \<union> extend S f k)
{p} \<union> extend S f k \<subseteq> {p} \<union> Extend S f
[PROOF STEP]
have \<open>\<not> consistent ({p} \<union> Extend S f)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> consistent ({p} \<union> extend S f k)
{p} \<union> extend S f k \<subseteq> {p} \<union> Extend S f

goal (1 subgoal):
 1. \<not> consistent ({p} \<union> Extend S f)
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<nexists>S'. set S' \<subseteq> {p} \<union> extend S f k \<and> S' \<turnstile> \<^bold>\<bottom>)
{p} \<union> extend S f k \<subseteq> {p} \<union> Extend S f

goal (1 subgoal):
 1. \<not> (\<nexists>S'. set S' \<subseteq> {p} \<union> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> consistent ({p} \<union> Extend S f)

goal (1 subgoal):
 1. \<not> maximal (Extend S f) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> consistent ({p} \<union> Extend S f)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> consistent ({p} \<union> Extend S f)

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>consistent ({p} \<union> Extend S f)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> consistent ({p} \<union> Extend S f)
consistent ({p} \<union> Extend S f)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma saturated_Extend:
  assumes \<open>consistent (Extend S f)\<close> and \<open>surj f\<close>
  shows \<open>saturated (Extend S f)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. saturated (Extend S f)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> saturated (Extend S f) \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> saturated (Extend S f)\<close>
[PROOF STATE]
proof (state)
this:
\<not> saturated (Extend S f)

goal (1 subgoal):
 1. \<not> saturated (Extend S f) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> saturated (Extend S f)
[PROOF STEP]
obtain p where p: \<open>(\<^bold>\<not> \<^bold>\<forall>p) \<in> Extend S f\<close> \<open>\<nexists>n. (\<^bold>\<not> p\<langle>\<^bold>#n/0\<rangle>) \<in> Extend S f\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> saturated (Extend S f)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>\<^bold>\<not> \<^bold>\<forall> p \<in> Extend S f; \<nexists>n. \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<in> Extend S f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding saturated_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>p. \<^bold>\<not> \<^bold>\<forall> p \<in> Extend S f \<longrightarrow> (\<exists>n. \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<in> Extend S f))

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>\<^bold>\<not> \<^bold>\<forall> p \<in> Extend S f; \<nexists>n. \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<in> Extend S f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> \<^bold>\<forall> p \<in> Extend S f
\<nexists>n. \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<in> Extend S f

goal (1 subgoal):
 1. \<not> saturated (Extend S f) \<Longrightarrow> False
[PROOF STEP]
obtain k where k: \<open>f k = (\<^bold>\<not> \<^bold>\<forall>p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. f k = \<^bold>\<not> \<^bold>\<forall> p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>surj f\<close>
[PROOF STATE]
proof (prove)
using this:
surj f

goal (1 subgoal):
 1. (\<And>k. f k = \<^bold>\<not> \<^bold>\<forall> p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding surj_def
[PROOF STATE]
proof (prove)
using this:
\<forall>y. \<exists>x. y = f x

goal (1 subgoal):
 1. (\<And>k. f k = \<^bold>\<not> \<^bold>\<forall> p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
f k = \<^bold>\<not> \<^bold>\<forall> p

goal (1 subgoal):
 1. \<not> saturated (Extend S f) \<Longrightarrow> False
[PROOF STEP]
have \<open>extend S f k \<subseteq> Extend S f\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend S f k \<subseteq> Extend S f
[PROOF STEP]
unfolding Extend_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend S f k \<subseteq> \<Union> (range (extend S f))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extend S f k \<subseteq> Extend S f

goal (1 subgoal):
 1. \<not> saturated (Extend S f) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extend S f k \<subseteq> Extend S f
[PROOF STEP]
have \<open>consistent ({\<^bold>\<not> \<^bold>\<forall>p} \<union> extend S f k)\<close>
[PROOF STATE]
proof (prove)
using this:
extend S f k \<subseteq> Extend S f

goal (1 subgoal):
 1. consistent ({\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k)
[PROOF STEP]
using assms(1) p(1)
[PROOF STATE]
proof (prove)
using this:
extend S f k \<subseteq> Extend S f
consistent (Extend S f)
\<^bold>\<not> \<^bold>\<forall> p \<in> Extend S f

goal (1 subgoal):
 1. consistent ({\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k)
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
extend S f k \<subseteq> Extend S f
\<nexists>S'. set S' \<subseteq> Extend S f \<and> S' \<turnstile> \<^bold>\<bottom>
\<^bold>\<not> \<^bold>\<forall> p \<in> Extend S f

goal (1 subgoal):
 1. \<nexists>S'. set S' \<subseteq> {\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k \<and> S' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
consistent ({\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k)

goal (1 subgoal):
 1. \<not> saturated (Extend S f) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
consistent ({\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k)
[PROOF STEP]
have \<open>\<exists>n. extend S f (Suc k) = {\<^bold>\<not> p\<langle>\<^bold>#n/0\<rangle>} \<union> {\<^bold>\<not> \<^bold>\<forall>p} \<union> extend S f k\<close>
[PROOF STATE]
proof (prove)
using this:
consistent ({\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k)

goal (1 subgoal):
 1. \<exists>n. extend S f (Suc k) = {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> {\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
consistent ({\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k)
f k = \<^bold>\<not> \<^bold>\<forall> p

goal (1 subgoal):
 1. \<exists>n. extend S f (Suc k) = {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> {\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k
[PROOF STEP]
by (auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
\<exists>n. extend S f (Suc k) = {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> {\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k

goal (1 subgoal):
 1. \<not> saturated (Extend S f) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>n. extend S f (Suc k) = {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> {\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k

goal (1 subgoal):
 1. \<not> saturated (Extend S f) \<Longrightarrow> False
[PROOF STEP]
have \<open>extend S f (Suc k) \<subseteq> Extend S f\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend S f (Suc k) \<subseteq> Extend S f
[PROOF STEP]
unfolding Extend_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend S f (Suc k) \<subseteq> \<Union> (range (extend S f))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
extend S f (Suc k) \<subseteq> Extend S f

goal (1 subgoal):
 1. \<not> saturated (Extend S f) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. extend S f (Suc k) = {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> {\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k
extend S f (Suc k) \<subseteq> Extend S f
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<exists>n. extend S f (Suc k) = {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> {\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k
extend S f (Suc k) \<subseteq> Extend S f

goal (1 subgoal):
 1. False
[PROOF STEP]
using p(2)
[PROOF STATE]
proof (prove)
using this:
\<exists>n. extend S f (Suc k) = {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> {\<^bold>\<not> \<^bold>\<forall> p} \<union> extend S f k
extend S f (Suc k) \<subseteq> Extend S f
\<nexists>n. \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<in> Extend S f

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma semantics_tm_id [simp]:
  \<open>\<lparr>\<^bold>#, \<^bold>\<dagger>\<rparr> t = t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<^bold>#, \<^bold>\<dagger>\<rparr> t = t
[PROOF STEP]
by (induct t) (auto cong: map_cong)


[STATEMENT]
lemma semantics_tm_id_map [simp]: \<open>map \<lparr>\<^bold>#, \<^bold>\<dagger>\<rparr> ts = ts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<lparr>\<^bold>#, \<^bold>\<dagger>\<rparr> ts = ts
[PROOF STEP]
by (auto cong: map_cong)