[STATEMENT]
theorem soundness: \<open>\<turnstile> p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
[PROOF STEP]
proof (induct p arbitrary: E F rule: Axiomatic.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>p E F. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
 2. \<And>p t E F. \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>)
 3. \<And>p q E F. \<lbrakk>\<turnstile> p \<^bold>\<longrightarrow> q; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (p \<^bold>\<longrightarrow> q); \<turnstile> p; \<And>E F. \<lbrakk>E, F, G\<rbrakk> p\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> q
 4. \<And>q p n E F. \<lbrakk>\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>); max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> \<^bold>\<forall> p)
[PROOF STEP]
case (GR q p n)
[PROOF STATE]
proof (state)
this:
\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>
\<lbrakk>?E, ?F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>)
max_var p < n
max_var q < n

goal (4 subgoals):
 1. \<And>p E F. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
 2. \<And>p t E F. \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>)
 3. \<And>p q E F. \<lbrakk>\<turnstile> p \<^bold>\<longrightarrow> q; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (p \<^bold>\<longrightarrow> q); \<turnstile> p; \<And>E F. \<lbrakk>E, F, G\<rbrakk> p\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> q
 4. \<And>q p n E F. \<lbrakk>\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>); max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> \<^bold>\<forall> p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>
\<lbrakk>?E, ?F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>)
max_var p < n
max_var q < n
[PROOF STEP]
have \<open>\<lbrakk>E(n := x), F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold>#n/0\<rangle>)\<close> for x
[PROOF STATE]
proof (prove)
using this:
\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>
\<lbrakk>?E, ?F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>)
max_var p < n
max_var q < n

goal (1 subgoal):
 1. \<lbrakk>E(n := x), F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>E(n := ?x), F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>)

goal (4 subgoals):
 1. \<And>p E F. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
 2. \<And>p t E F. \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>)
 3. \<And>p q E F. \<lbrakk>\<turnstile> p \<^bold>\<longrightarrow> q; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (p \<^bold>\<longrightarrow> q); \<turnstile> p; \<And>E F. \<lbrakk>E, F, G\<rbrakk> p\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> q
 4. \<And>q p n E F. \<lbrakk>\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>); max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> \<^bold>\<forall> p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>E(n := ?x), F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>)
[PROOF STEP]
have \<open>\<lbrakk>E(n := x), F, G\<rbrakk> q \<longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p\<langle>\<^bold>#n/0\<rangle>)\<close> for x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>E(n := ?x), F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>)

goal (1 subgoal):
 1. \<lbrakk>E(n := x), F, G\<rbrakk> q \<longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>E(n := ?x), F, G\<rbrakk> q \<longrightarrow> \<lbrakk>E(n := ?x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>)

goal (4 subgoals):
 1. \<And>p E F. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
 2. \<And>p t E F. \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>)
 3. \<And>p q E F. \<lbrakk>\<turnstile> p \<^bold>\<longrightarrow> q; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (p \<^bold>\<longrightarrow> q); \<turnstile> p; \<And>E F. \<lbrakk>E, F, G\<rbrakk> p\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> q
 4. \<And>q p n E F. \<lbrakk>\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>); max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> \<^bold>\<forall> p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>E(n := ?x), F, G\<rbrakk> q \<longrightarrow> \<lbrakk>E(n := ?x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>)
[PROOF STEP]
have \<open>\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p\<langle>\<^bold>#n/0\<rangle>)\<close> for x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>E(n := ?x), F, G\<rbrakk> q \<longrightarrow> \<lbrakk>E(n := ?x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>)

goal (1 subgoal):
 1. \<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>)
[PROOF STEP]
using GR.hyps(3-4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>E(n := ?x), F, G\<rbrakk> q \<longrightarrow> \<lbrakk>E(n := ?x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>)
max_var p < n
max_var q < n

goal (1 subgoal):
 1. \<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> \<lbrakk>E(n := ?x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>)

goal (4 subgoals):
 1. \<And>p E F. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
 2. \<And>p t E F. \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>)
 3. \<And>p q E F. \<lbrakk>\<turnstile> p \<^bold>\<longrightarrow> q; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (p \<^bold>\<longrightarrow> q); \<turnstile> p; \<And>E F. \<lbrakk>E, F, G\<rbrakk> p\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> q
 4. \<And>q p n E F. \<lbrakk>\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>); max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> \<^bold>\<forall> p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> \<lbrakk>E(n := ?x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>)
[PROOF STEP]
have \<open>\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E(n := x), F, G\<rbrakk> (p\<langle>\<^bold>#n/0\<rangle>))\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> \<lbrakk>E(n := ?x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>)

goal (1 subgoal):
 1. \<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E(n := x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E(n := x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>))

goal (4 subgoals):
 1. \<And>p E F. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
 2. \<And>p t E F. \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>)
 3. \<And>p q E F. \<lbrakk>\<turnstile> p \<^bold>\<longrightarrow> q; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (p \<^bold>\<longrightarrow> q); \<turnstile> p; \<And>E F. \<lbrakk>E, F, G\<rbrakk> p\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> q
 4. \<And>q p n E F. \<lbrakk>\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>); max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> \<^bold>\<forall> p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E(n := x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>))
[PROOF STEP]
have \<open>\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E(n := x)\<langle>0:x\<rangle>, F, G\<rbrakk> p)\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E(n := x), F, G\<rbrakk> (p\<langle>\<^bold># n/0\<rangle>))

goal (1 subgoal):
 1. \<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E(n := x)\<langle>0:x\<rangle>, F, G\<rbrakk> p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E(n := x)\<langle>0:x\<rangle>, F, G\<rbrakk> p)

goal (4 subgoals):
 1. \<And>p E F. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
 2. \<And>p t E F. \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>)
 3. \<And>p q E F. \<lbrakk>\<turnstile> p \<^bold>\<longrightarrow> q; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (p \<^bold>\<longrightarrow> q); \<turnstile> p; \<And>E F. \<lbrakk>E, F, G\<rbrakk> p\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> q
 4. \<And>q p n E F. \<lbrakk>\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>); max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> \<^bold>\<forall> p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E(n := x)\<langle>0:x\<rangle>, F, G\<rbrakk> p)
[PROOF STEP]
have \<open>\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>(E\<langle>0:x\<rangle>)(n + 1 := x), F, G\<rbrakk> p)\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E(n := x)\<langle>0:x\<rangle>, F, G\<rbrakk> p)

goal (1 subgoal):
 1. \<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>(E\<langle>0:x\<rangle>)(n + 1 := x), F, G\<rbrakk> p)
[PROOF STEP]
using shift_upd_commute
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E(n := x)\<langle>0:x\<rangle>, F, G\<rbrakk> p)
?m \<le> ?n \<Longrightarrow> ?E(?n := ?x)\<langle>?m:?y\<rangle> = (?E\<langle>?m:?y\<rangle>)(?n + 1 := ?x)

goal (1 subgoal):
 1. \<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>(E\<langle>0:x\<rangle>)(n + 1 := x), F, G\<rbrakk> p)
[PROOF STEP]
by (metis zero_le)
[PROOF STATE]
proof (state)
this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>(E\<langle>0:x\<rangle>)(n + 1 := x), F, G\<rbrakk> p)

goal (4 subgoals):
 1. \<And>p E F. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
 2. \<And>p t E F. \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>)
 3. \<And>p q E F. \<lbrakk>\<turnstile> p \<^bold>\<longrightarrow> q; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (p \<^bold>\<longrightarrow> q); \<turnstile> p; \<And>E F. \<lbrakk>E, F, G\<rbrakk> p\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> q
 4. \<And>q p n E F. \<lbrakk>\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>); max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> \<^bold>\<forall> p)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>(E\<langle>0:x\<rangle>)(n + 1 := x), F, G\<rbrakk> p)

goal (4 subgoals):
 1. \<And>p E F. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
 2. \<And>p t E F. \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>)
 3. \<And>p q E F. \<lbrakk>\<turnstile> p \<^bold>\<longrightarrow> q; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (p \<^bold>\<longrightarrow> q); \<turnstile> p; \<And>E F. \<lbrakk>E, F, G\<rbrakk> p\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> q
 4. \<And>q p n E F. \<lbrakk>\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>); max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> \<^bold>\<forall> p)
[PROOF STEP]
have \<open>max_list (vars_fm p) < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_var p < n
[PROOF STEP]
using GR.hyps(3)
[PROOF STATE]
proof (prove)
using this:
max_var p < n

goal (1 subgoal):
 1. max_var p < n
[PROOF STEP]
by (simp add: max_list_append)
[PROOF STATE]
proof (state)
this:
max_var p < n

goal (4 subgoals):
 1. \<And>p E F. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
 2. \<And>p t E F. \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>)
 3. \<And>p q E F. \<lbrakk>\<turnstile> p \<^bold>\<longrightarrow> q; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (p \<^bold>\<longrightarrow> q); \<turnstile> p; \<And>E F. \<lbrakk>E, F, G\<rbrakk> p\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> q
 4. \<And>q p n E F. \<lbrakk>\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>); max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> \<^bold>\<forall> p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>(E\<langle>0:x\<rangle>)(n + 1 := x), F, G\<rbrakk> p)
max_var p < n
[PROOF STEP]
have \<open>\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E\<langle>0:x\<rangle>, F, G\<rbrakk> p)\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>(E\<langle>0:x\<rangle>)(n + 1 := x), F, G\<rbrakk> p)
max_var p < n

goal (1 subgoal):
 1. \<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E\<langle>0:x\<rangle>, F, G\<rbrakk> p)
[PROOF STEP]
using upd_vars_fm
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>(E\<langle>0:x\<rangle>)(n + 1 := x), F, G\<rbrakk> p)
max_var p < n
max_var ?p < ?n \<Longrightarrow> \<lbrakk>?E(?n := ?x), ?F, ?G\<rbrakk> ?p = \<lbrakk>?E, ?F, ?G\<rbrakk> ?p

goal (1 subgoal):
 1. \<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E\<langle>0:x\<rangle>, F, G\<rbrakk> p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E\<langle>0:x\<rangle>, F, G\<rbrakk> p)

goal (4 subgoals):
 1. \<And>p E F. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
 2. \<And>p t E F. \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>)
 3. \<And>p q E F. \<lbrakk>\<turnstile> p \<^bold>\<longrightarrow> q; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (p \<^bold>\<longrightarrow> q); \<turnstile> p; \<And>E F. \<lbrakk>E, F, G\<rbrakk> p\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> q
 4. \<And>q p n E F. \<lbrakk>\<turnstile> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>); max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> \<^bold>\<forall> p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E\<langle>0:x\<rangle>, F, G\<rbrakk> p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>E, F, G\<rbrakk> q \<longrightarrow> (\<forall>x. \<lbrakk>E\<langle>0:x\<rangle>, F, G\<rbrakk> p)

goal (1 subgoal):
 1. \<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> \<^bold>\<forall> p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>E, F, G\<rbrakk> (q \<^bold>\<longrightarrow> \<^bold>\<forall> p)

goal (3 subgoals):
 1. \<And>p E F. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
 2. \<And>p t E F. \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>)
 3. \<And>p q E F. \<lbrakk>\<turnstile> p \<^bold>\<longrightarrow> q; \<And>E F. \<lbrakk>E, F, G\<rbrakk> (p \<^bold>\<longrightarrow> q); \<turnstile> p; \<And>E F. \<lbrakk>E, F, G\<rbrakk> p\<rbrakk> \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> q
[PROOF STEP]
qed (auto simp: tautology)


[STATEMENT]
lemma AS: \<open>\<turnstile> (p \<^bold>\<longrightarrow> q \<^bold>\<longrightarrow> r) \<^bold>\<longrightarrow> (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> p \<^bold>\<longrightarrow> r\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> (p \<^bold>\<longrightarrow> q \<^bold>\<longrightarrow> r) \<^bold>\<longrightarrow> (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> p \<^bold>\<longrightarrow> r
[PROOF STEP]
by auto


[STATEMENT]
lemma AK: \<open>\<turnstile> q \<^bold>\<longrightarrow> p \<^bold>\<longrightarrow> q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> q \<^bold>\<longrightarrow> p \<^bold>\<longrightarrow> q
[PROOF STEP]
by auto


[STATEMENT]
lemma Neg: \<open>\<turnstile> \<^bold>\<not> \<^bold>\<not> p \<^bold>\<longrightarrow> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<^bold>\<not> \<^bold>\<not> p \<^bold>\<longrightarrow> p
[PROOF STEP]
by auto


[STATEMENT]
lemma contraposition:
  \<open>\<turnstile> (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<not> p\<close>
  \<open>\<turnstile> (\<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<not> p) \<^bold>\<longrightarrow> p \<^bold>\<longrightarrow> q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<not> p &&& \<turnstile> (\<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<not> p) \<^bold>\<longrightarrow> p \<^bold>\<longrightarrow> q
[PROOF STEP]
by (auto intro: TA)


[STATEMENT]
lemma GR': \<open>\<turnstile> \<^bold>\<not> p\<langle>\<^bold>#n/0\<rangle> \<^bold>\<longrightarrow> q \<Longrightarrow> max_var p < n \<Longrightarrow> max_var q < n \<Longrightarrow> \<turnstile> \<^bold>\<not> \<^bold>\<forall>p \<^bold>\<longrightarrow> q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> q; max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> q; max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> q
[PROOF STEP]
assume *: \<open>\<turnstile> \<^bold>\<not> p\<langle>\<^bold>#n/0\<rangle> \<^bold>\<longrightarrow> q\<close> and n: \<open>max_var p < n\<close> \<open>max_var q < n\<close>
[PROOF STATE]
proof (state)
this:
\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> q
max_var p < n
max_var q < n

goal (1 subgoal):
 1. \<lbrakk>\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> q; max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> q
[PROOF STEP]
have \<open>\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> p\<langle>\<^bold>#n/0\<rangle>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>
[PROOF STEP]
using * contraposition(1)
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> q
\<turnstile> (?p \<^bold>\<longrightarrow> ?q) \<^bold>\<longrightarrow> \<^bold>\<not> ?q \<^bold>\<longrightarrow> \<^bold>\<not> ?p

goal (1 subgoal):
 1. \<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>

goal (1 subgoal):
 1. \<lbrakk>\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> q; max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>
[PROOF STEP]
have \<open>\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> p\<langle>\<^bold>#n/0\<rangle>\<close>
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>

goal (1 subgoal):
 1. \<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>
[PROOF STEP]
by (meson AK AS MP Neg)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>

goal (1 subgoal):
 1. \<lbrakk>\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> q; max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>
[PROOF STEP]
have \<open>\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<forall>p\<close>
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>

goal (1 subgoal):
 1. \<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<forall> p
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> p\<langle>\<^bold># n/0\<rangle>
max_var p < n
max_var q < n

goal (1 subgoal):
 1. \<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<forall> p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<forall> p

goal (1 subgoal):
 1. \<lbrakk>\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> q; max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<forall> p
[PROOF STEP]
have \<open>\<turnstile> \<^bold>\<not> \<^bold>\<forall>p \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> q\<close>
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<forall> p

goal (1 subgoal):
 1. \<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> q
[PROOF STEP]
using contraposition(1)
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<^bold>\<not> q \<^bold>\<longrightarrow> \<^bold>\<forall> p
\<turnstile> (?p \<^bold>\<longrightarrow> ?q) \<^bold>\<longrightarrow> \<^bold>\<not> ?q \<^bold>\<longrightarrow> \<^bold>\<not> ?p

goal (1 subgoal):
 1. \<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> q
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> q

goal (1 subgoal):
 1. \<lbrakk>\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> q; max_var p < n; max_var q < n\<rbrakk> \<Longrightarrow> \<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> q

goal (1 subgoal):
 1. \<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> q
[PROOF STEP]
by (meson AK AS MP Neg)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Imp3: \<open>\<turnstile> (p \<^bold>\<longrightarrow> q \<^bold>\<longrightarrow> r) \<^bold>\<longrightarrow> ((s \<^bold>\<longrightarrow> p) \<^bold>\<longrightarrow> (s \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> s \<^bold>\<longrightarrow> r)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> (p \<^bold>\<longrightarrow> q \<^bold>\<longrightarrow> r) \<^bold>\<longrightarrow> (s \<^bold>\<longrightarrow> p) \<^bold>\<longrightarrow> (s \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> s \<^bold>\<longrightarrow> r
[PROOF STEP]
by auto


[STATEMENT]
lemma imply_ImpE: \<open>\<turnstile> ps \<^bold>\<leadsto> p \<^bold>\<longrightarrow> ps \<^bold>\<leadsto> (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> ps \<^bold>\<leadsto> q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> ps \<^bold>\<leadsto> p \<^bold>\<longrightarrow> ps \<^bold>\<leadsto> (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> ps \<^bold>\<leadsto> q
[PROOF STEP]
by (induct ps) (auto intro: Imp3 MP)


[STATEMENT]
lemma MP' [trans, dest]: \<open>ps \<turnstile> p \<^bold>\<longrightarrow> q \<Longrightarrow> ps \<turnstile> p \<Longrightarrow> ps \<turnstile> q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps \<turnstile> p \<^bold>\<longrightarrow> q; ps \<turnstile> p\<rbrakk> \<Longrightarrow> ps \<turnstile> q
[PROOF STEP]
using imply_ImpE
[PROOF STATE]
proof (prove)
using this:
\<turnstile> ?ps \<^bold>\<leadsto> ?p \<^bold>\<longrightarrow> ?ps \<^bold>\<leadsto> (?p \<^bold>\<longrightarrow> ?q) \<^bold>\<longrightarrow> ?ps \<^bold>\<leadsto> ?q

goal (1 subgoal):
 1. \<lbrakk>ps \<turnstile> p \<^bold>\<longrightarrow> q; ps \<turnstile> p\<rbrakk> \<Longrightarrow> ps \<turnstile> q
[PROOF STEP]
by fast


[STATEMENT]
lemma imply_Cons [intro]: \<open>ps \<turnstile> q \<Longrightarrow> p # ps \<turnstile> q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps \<turnstile> q \<Longrightarrow> p # ps \<turnstile> q
[PROOF STEP]
by (auto intro: MP AK)


[STATEMENT]
lemma imply_head [intro]: \<open>p # ps \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p # ps \<turnstile> p
[PROOF STEP]
proof (induct ps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [p] \<turnstile> p
 2. \<And>a ps. p # ps \<turnstile> p \<Longrightarrow> p # a # ps \<turnstile> p
[PROOF STEP]
case (Cons q ps)
[PROOF STATE]
proof (state)
this:
p # ps \<turnstile> p

goal (2 subgoals):
 1. [p] \<turnstile> p
 2. \<And>a ps. p # ps \<turnstile> p \<Longrightarrow> p # a # ps \<turnstile> p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p # ps \<turnstile> p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p # ps \<turnstile> p

goal (1 subgoal):
 1. p # q # ps \<turnstile> p
[PROOF STEP]
by (metis AK MP' imply.simps(1-2))
[PROOF STATE]
proof (state)
this:
p # q # ps \<turnstile> p

goal (1 subgoal):
 1. [p] \<turnstile> p
[PROOF STEP]
qed auto


[STATEMENT]
lemma imply_lift_Imp [simp]:
  assumes \<open>\<turnstile> p \<^bold>\<longrightarrow> q\<close>
  shows \<open>\<turnstile> p \<^bold>\<longrightarrow> ps \<^bold>\<leadsto> q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> p \<^bold>\<longrightarrow> ps \<^bold>\<leadsto> q
[PROOF STEP]
using assms MP MP' imply_head
[PROOF STATE]
proof (prove)
using this:
\<turnstile> p \<^bold>\<longrightarrow> q
\<lbrakk>\<turnstile> ?p \<^bold>\<longrightarrow> ?q; \<turnstile> ?p\<rbrakk> \<Longrightarrow> \<turnstile> ?q
\<lbrakk>?ps \<turnstile> ?p \<^bold>\<longrightarrow> ?q; ?ps \<turnstile> ?p\<rbrakk> \<Longrightarrow> ?ps \<turnstile> ?q
?p # ?ps \<turnstile> ?p

goal (1 subgoal):
 1. \<turnstile> p \<^bold>\<longrightarrow> ps \<^bold>\<leadsto> q
[PROOF STEP]
by (metis imply.simps(2))


[STATEMENT]
lemma add_imply [simp]: \<open>\<turnstile> q \<Longrightarrow> ps \<turnstile> q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> q \<Longrightarrow> ps \<turnstile> q
[PROOF STEP]
using MP imply_head
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<turnstile> ?p \<^bold>\<longrightarrow> ?q; \<turnstile> ?p\<rbrakk> \<Longrightarrow> \<turnstile> ?q
?p # ?ps \<turnstile> ?p

goal (1 subgoal):
 1. \<turnstile> q \<Longrightarrow> ps \<turnstile> q
[PROOF STEP]
by (auto simp del: TA)


[STATEMENT]
lemma imply_mem [simp]: \<open>p \<in> set ps \<Longrightarrow> ps \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> set ps \<Longrightarrow> ps \<turnstile> p
[PROOF STEP]
proof (induct ps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> set [] \<Longrightarrow> [] \<turnstile> p
 2. \<And>a ps. \<lbrakk>p \<in> set ps \<Longrightarrow> ps \<turnstile> p; p \<in> set (a # ps)\<rbrakk> \<Longrightarrow> a # ps \<turnstile> p
[PROOF STEP]
case (Cons q ps)
[PROOF STATE]
proof (state)
this:
p \<in> set ps \<Longrightarrow> ps \<turnstile> p
p \<in> set (q # ps)

goal (2 subgoals):
 1. p \<in> set [] \<Longrightarrow> [] \<turnstile> p
 2. \<And>a ps. \<lbrakk>p \<in> set ps \<Longrightarrow> ps \<turnstile> p; p \<in> set (a # ps)\<rbrakk> \<Longrightarrow> a # ps \<turnstile> p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> set ps \<Longrightarrow> ps \<turnstile> p
p \<in> set (q # ps)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> set ps \<Longrightarrow> ps \<turnstile> p
p \<in> set (q # ps)

goal (1 subgoal):
 1. q # ps \<turnstile> p
[PROOF STEP]
by (metis imply_Cons imply_head set_ConsD)
[PROOF STATE]
proof (state)
this:
q # ps \<turnstile> p

goal (1 subgoal):
 1. p \<in> set [] \<Longrightarrow> [] \<turnstile> p
[PROOF STEP]
qed simp


[STATEMENT]
lemma deduct1: \<open>ps \<turnstile> p \<^bold>\<longrightarrow> q \<Longrightarrow> p # ps \<turnstile> q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps \<turnstile> p \<^bold>\<longrightarrow> q \<Longrightarrow> p # ps \<turnstile> q
[PROOF STEP]
by (meson MP' imply_Cons imply_head)


[STATEMENT]
lemma imply_append [iff]: \<open>(ps @ qs \<^bold>\<leadsto> r) = (ps \<^bold>\<leadsto> qs \<^bold>\<leadsto> r)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps @ qs \<^bold>\<leadsto> r = ps \<^bold>\<leadsto> qs \<^bold>\<leadsto> r
[PROOF STEP]
by (induct ps) simp_all


[STATEMENT]
lemma imply_swap_append: \<open>ps @ qs \<turnstile> r \<Longrightarrow> qs @ ps \<turnstile> r\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps @ qs \<turnstile> r \<Longrightarrow> qs @ ps \<turnstile> r
[PROOF STEP]
proof (induct qs arbitrary: ps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ps. ps @ [] \<turnstile> r \<Longrightarrow> [] @ ps \<turnstile> r
 2. \<And>a qs ps. \<lbrakk>\<And>ps. ps @ qs \<turnstile> r \<Longrightarrow> qs @ ps \<turnstile> r; ps @ a # qs \<turnstile> r\<rbrakk> \<Longrightarrow> (a # qs) @ ps \<turnstile> r
[PROOF STEP]
case (Cons q qs)
[PROOF STATE]
proof (state)
this:
?ps @ qs \<turnstile> r \<Longrightarrow> qs @ ?ps \<turnstile> r
ps @ q # qs \<turnstile> r

goal (2 subgoals):
 1. \<And>ps. ps @ [] \<turnstile> r \<Longrightarrow> [] @ ps \<turnstile> r
 2. \<And>a qs ps. \<lbrakk>\<And>ps. ps @ qs \<turnstile> r \<Longrightarrow> qs @ ps \<turnstile> r; ps @ a # qs \<turnstile> r\<rbrakk> \<Longrightarrow> (a # qs) @ ps \<turnstile> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?ps @ qs \<turnstile> r \<Longrightarrow> qs @ ?ps \<turnstile> r
ps @ q # qs \<turnstile> r
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?ps @ qs \<turnstile> r \<Longrightarrow> qs @ ?ps \<turnstile> r
ps @ q # qs \<turnstile> r

goal (1 subgoal):
 1. (q # qs) @ ps \<turnstile> r
[PROOF STEP]
by (metis deduct1 imply.simps(2) imply_append)
[PROOF STATE]
proof (state)
this:
(q # qs) @ ps \<turnstile> r

goal (1 subgoal):
 1. \<And>ps. ps @ [] \<turnstile> r \<Longrightarrow> [] @ ps \<turnstile> r
[PROOF STEP]
qed simp


[STATEMENT]
lemma deduct2: \<open>p # ps \<turnstile> q \<Longrightarrow> ps \<turnstile> p \<^bold>\<longrightarrow> q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p # ps \<turnstile> q \<Longrightarrow> ps \<turnstile> p \<^bold>\<longrightarrow> q
[PROOF STEP]
by (metis imply.simps(1-2) imply_append imply_swap_append)


[STATEMENT]
lemma cut [trans, dest]: \<open>p # ps \<turnstile> r \<Longrightarrow> q # ps \<turnstile> p \<Longrightarrow> q # ps \<turnstile> r\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p # ps \<turnstile> r; q # ps \<turnstile> p\<rbrakk> \<Longrightarrow> q # ps \<turnstile> r
[PROOF STEP]
by (meson MP' deduct(2) imply_Cons)


[STATEMENT]
lemma Boole: \<open>(\<^bold>\<not> p) # ps \<turnstile> \<^bold>\<bottom> \<Longrightarrow> ps \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<not> p # ps \<turnstile> \<^bold>\<bottom> \<Longrightarrow> ps \<turnstile> p
[PROOF STEP]
by (meson MP' Neg add_imply deduct(2))


[STATEMENT]
lemma imply_weaken: \<open>ps \<turnstile> q \<Longrightarrow> set ps \<subseteq> set ps' \<Longrightarrow> ps' \<turnstile> q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps \<turnstile> q; set ps \<subseteq> set ps'\<rbrakk> \<Longrightarrow> ps' \<turnstile> q
[PROOF STEP]
proof (induct ps arbitrary: q)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>[] \<turnstile> q; set [] \<subseteq> set ps'\<rbrakk> \<Longrightarrow> ps' \<turnstile> q
 2. \<And>a ps q. \<lbrakk>\<And>q. \<lbrakk>ps \<turnstile> q; set ps \<subseteq> set ps'\<rbrakk> \<Longrightarrow> ps' \<turnstile> q; a # ps \<turnstile> q; set (a # ps) \<subseteq> set ps'\<rbrakk> \<Longrightarrow> ps' \<turnstile> q
[PROOF STEP]
case (Cons p ps)
[PROOF STATE]
proof (state)
this:
\<lbrakk>ps \<turnstile> ?q; set ps \<subseteq> set ps'\<rbrakk> \<Longrightarrow> ps' \<turnstile> ?q
p # ps \<turnstile> q
set (p # ps) \<subseteq> set ps'

goal (2 subgoals):
 1. \<And>q. \<lbrakk>[] \<turnstile> q; set [] \<subseteq> set ps'\<rbrakk> \<Longrightarrow> ps' \<turnstile> q
 2. \<And>a ps q. \<lbrakk>\<And>q. \<lbrakk>ps \<turnstile> q; set ps \<subseteq> set ps'\<rbrakk> \<Longrightarrow> ps' \<turnstile> q; a # ps \<turnstile> q; set (a # ps) \<subseteq> set ps'\<rbrakk> \<Longrightarrow> ps' \<turnstile> q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>ps \<turnstile> ?q; set ps \<subseteq> set ps'\<rbrakk> \<Longrightarrow> ps' \<turnstile> ?q
p # ps \<turnstile> q
set (p # ps) \<subseteq> set ps'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ps \<turnstile> ?q; set ps \<subseteq> set ps'\<rbrakk> \<Longrightarrow> ps' \<turnstile> ?q
p # ps \<turnstile> q
set (p # ps) \<subseteq> set ps'

goal (1 subgoal):
 1. ps' \<turnstile> q
[PROOF STEP]
by (metis MP' deduct(2) imply_mem insert_subset list.simps(15))
[PROOF STATE]
proof (state)
this:
ps' \<turnstile> q

goal (1 subgoal):
 1. \<And>q. \<lbrakk>[] \<turnstile> q; set [] \<subseteq> set ps'\<rbrakk> \<Longrightarrow> ps' \<turnstile> q
[PROOF STEP]
qed simp


[STATEMENT]
lemma UN_finite_bound:
  assumes \<open>finite A\<close> and \<open>A \<subseteq> (\<Union>n. f n)\<close>
  shows \<open>\<exists>m :: nat. A \<subseteq> (\<Union>n \<le> m. f n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. A \<subseteq> \<Union> (f ` {..m})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
A \<subseteq> \<Union> (range f)

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

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

goal (1 subgoal):
 1. (\<And>m. A \<subseteq> \<Union> (f ` {..m}) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
A \<subseteq> \<Union> (f ` {..m})

goal (2 subgoals):
 1. {} \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>m. {} \<subseteq> \<Union> (f ` {..m})
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>m. F \<subseteq> \<Union> (f ` {..m}); insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>m. insert x F \<subseteq> \<Union> (f ` {..m})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<subseteq> \<Union> (f ` {..m})
[PROOF STEP]
have \<open>A \<subseteq> (\<Union>n \<le> (m + k). f n)\<close> for k
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> \<Union> (f ` {..m})

goal (1 subgoal):
 1. A \<subseteq> \<Union> (f ` {..m + k})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A \<subseteq> \<Union> (f ` {..m + ?k})

goal (2 subgoals):
 1. {} \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>m. {} \<subseteq> \<Union> (f ` {..m})
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>m. F \<subseteq> \<Union> (f ` {..m}); insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>m. insert x F \<subseteq> \<Union> (f ` {..m})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A \<subseteq> \<Union> (f ` {..m + ?k})

goal (2 subgoals):
 1. {} \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>m. {} \<subseteq> \<Union> (f ` {..m})
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>m. F \<subseteq> \<Union> (f ` {..m}); insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>m. insert x F \<subseteq> \<Union> (f ` {..m})
[PROOF STEP]
obtain m' where \<open>x \<in> f m'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m'. x \<in> f m' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insert(4)
[PROOF STATE]
proof (prove)
using this:
insert x A \<subseteq> \<Union> (range f)

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

goal (2 subgoals):
 1. {} \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>m. {} \<subseteq> \<Union> (f ` {..m})
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>m. F \<subseteq> \<Union> (f ` {..m}); insert x F \<subseteq> \<Union> (range f)\<rbrakk> \<Longrightarrow> \<exists>m. insert x F \<subseteq> \<Union> (f ` {..m})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A \<subseteq> \<Union> (f ` {..m + ?k})
x \<in> f m'
[PROOF STEP]
have \<open>{x} \<union> A \<subseteq> (\<Union>n \<le> m + m'. f n)\<close>
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> \<Union> (f ` {..m + ?k})
x \<in> f m'

goal (1 subgoal):
 1. {x} \<union> A \<subseteq> \<Union> (f ` {..m + m'})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x} \<union> A \<subseteq> \<Union> (f ` {..m + m'})

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

goal (1 subgoal):
 1. \<exists>m. insert x A \<subseteq> \<Union> (f ` {..m})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m. insert x A \<subseteq> \<Union> (f ` {..m})

goal (1 subgoal):
 1. {} \<subseteq> \<Union> (range f) \<Longrightarrow> \<exists>m. {} \<subseteq> \<Union> (f ` {..m})
[PROOF STEP]
qed simp


[STATEMENT]
lemma split_list:
  assumes \<open>x \<in> set A\<close>
  shows \<open>set (x # removeAll x A) = set A \<and> x \<notin> set (removeAll x A)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (x # removeAll x A) = set A \<and> x \<notin> set (removeAll x A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> set A

goal (1 subgoal):
 1. set (x # removeAll x A) = set A \<and> x \<notin> set (removeAll x A)
[PROOF STEP]
by auto


[STATEMENT]
lemma imply_vars_fm: \<open>vars_fm (ps \<^bold>\<leadsto> q) = concat (map vars_fm ps) @ vars_fm q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_fm (ps \<^bold>\<leadsto> q) = concat (map vars_fm ps) @ vars_fm q
[PROOF STEP]
by (induct ps) auto


[STATEMENT]
lemma inconsistent_fm:
  assumes \<open>consistent S\<close> and \<open>\<not> consistent ({p} \<union> S)\<close>
  obtains S' where \<open>set S' \<subseteq> S\<close> and \<open>p # S' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>set S' \<subseteq> S; p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>set S' \<subseteq> S; p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain S' where S': \<open>set S' \<subseteq> {p} \<union> S\<close> \<open>p \<in> set S'\<close> \<open>S' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>set S' \<subseteq> {p} \<union> S; p \<in> set S'; S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
consistent S
\<not> consistent ({p} \<union> S)

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>set S' \<subseteq> {p} \<union> S; p \<in> set S'; S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
\<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>)

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>set S' \<subseteq> {p} \<union> S; p \<in> set S'; S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set S' \<subseteq> {p} \<union> S
p \<in> set S'
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]
then
[PROOF STATE]
proof (chain)
picking this:
set S' \<subseteq> {p} \<union> S
p \<in> set S'
S' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
obtain S'' where S'': \<open>set (p # S'') = set S'\<close> \<open>p \<notin> set S''\<close>
[PROOF STATE]
proof (prove)
using this:
set S' \<subseteq> {p} \<union> S
p \<in> set S'
S' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. (\<And>S''. \<lbrakk>set (p # S'') = set S'; p \<notin> set S''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using split_list
[PROOF STATE]
proof (prove)
using this:
set S' \<subseteq> {p} \<union> S
p \<in> set S'
S' \<turnstile> \<^bold>\<bottom>
?x \<in> set ?A \<Longrightarrow> set (?x # removeAll ?x ?A) = set ?A \<and> ?x \<notin> set (removeAll ?x ?A)

goal (1 subgoal):
 1. (\<And>S''. \<lbrakk>set (p # S'') = set S'; p \<notin> set S''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
set (p # S'') = set S'
p \<notin> set S''

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

goal (1 subgoal):
 1. p # S'' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
using \<open>S' \<turnstile> \<^bold>\<bottom>\<close> imply_weaken
[PROOF STATE]
proof (prove)
using this:
set (p # S'') = set S'
p \<notin> set S''
S' \<turnstile> \<^bold>\<bottom>
\<lbrakk>?ps \<turnstile> ?q; set ?ps \<subseteq> set ?ps'\<rbrakk> \<Longrightarrow> ?ps' \<turnstile> ?q

goal (1 subgoal):
 1. p # S'' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p # 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]
then
[PROOF STATE]
proof (chain)
picking this:
p # S'' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p # S'' \<turnstile> \<^bold>\<bottom>

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

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (metis Diff_insert_absorb Diff_subset_conv list.simps(15))
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma max_list_in_Cons: \<open>xs \<noteq> [] \<Longrightarrow> max_list xs \<in> set xs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> max_list xs \<in> set xs
[PROOF STEP]
proof (induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> max_list [] \<in> set []
 2. \<And>a xs. \<lbrakk>xs \<noteq> [] \<Longrightarrow> max_list xs \<in> set xs; a # xs \<noteq> []\<rbrakk> \<Longrightarrow> max_list (a # xs) \<in> set (a # xs)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] \<noteq> []

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> max_list [] \<in> set []
 2. \<And>a xs. \<lbrakk>xs \<noteq> [] \<Longrightarrow> max_list xs \<in> set xs; a # xs \<noteq> []\<rbrakk> \<Longrightarrow> max_list (a # xs) \<in> set (a # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] \<noteq> []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[] \<noteq> []

goal (1 subgoal):
 1. max_list [] \<in> set []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
max_list [] \<in> set []

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>xs \<noteq> [] \<Longrightarrow> max_list xs \<in> set xs; a # xs \<noteq> []\<rbrakk> \<Longrightarrow> max_list (a # xs) \<in> set (a # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>xs \<noteq> [] \<Longrightarrow> max_list xs \<in> set xs; a # xs \<noteq> []\<rbrakk> \<Longrightarrow> max_list (a # xs) \<in> set (a # xs)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
xs \<noteq> [] \<Longrightarrow> max_list xs \<in> set xs
x # xs \<noteq> []

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>xs \<noteq> [] \<Longrightarrow> max_list xs \<in> set xs; a # xs \<noteq> []\<rbrakk> \<Longrightarrow> max_list (a # xs) \<in> set (a # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> [] \<Longrightarrow> max_list xs \<in> set xs
x # xs \<noteq> []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> [] \<Longrightarrow> max_list xs \<in> set xs
x # xs \<noteq> []

goal (1 subgoal):
 1. max_list (x # xs) \<in> set (x # xs)
[PROOF STEP]
by (metis linorder_not_less list.set_intros(1-2) max.absorb2 max.absorb3
        max_list.simps(1-2) max_nat.right_neutral)
[PROOF STATE]
proof (state)
this:
max_list (x # xs) \<in> set (x # xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma max_list_max: \<open>\<forall>x \<in> set xs. x \<le> max_list xs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. x \<le> max_list xs
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma max_list_in_set: \<open>finite S \<Longrightarrow> set xs \<subseteq> S \<Longrightarrow> max_list xs \<le> max_set S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> max_list xs \<le> max_set S
[PROOF STEP]
unfolding max_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> max_list xs \<le> (if S = {} then 0 else Max S)
[PROOF STEP]
using max_list_in_Cons
[PROOF STATE]
proof (prove)
using this:
?xs \<noteq> [] \<Longrightarrow> max_list ?xs \<in> set ?xs

goal (1 subgoal):
 1. \<lbrakk>finite S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> max_list xs \<le> (if S = {} then 0 else Max S)
[PROOF STEP]
by (metis (mono_tags, lifting) Max_ge bot.extremum_uniqueI bot_nat_0.extremum max_list.simps(1)
      set_empty subsetD)


[STATEMENT]
lemma consistent_add_witness:
  assumes \<open>consistent S\<close> and \<open>(\<^bold>\<not> \<^bold>\<forall>p) \<in> S\<close>
    and \<open>finite (vars S)\<close> and \<open>max_set (vars S) < n\<close>
  shows \<open>consistent ({\<^bold>\<not> p\<langle>\<^bold>#n/0\<rangle>} \<union> S)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent ({\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S)
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>S'. set S' \<subseteq> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<exists>S'. set S' \<subseteq> {\<^bold>\<not> p\<langle>\<^bold>#n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (state)
this:
\<exists>S'. set S' \<subseteq> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>

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

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>set S' \<subseteq> S; \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> # 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> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>
consistent S
\<^bold>\<not> \<^bold>\<forall> p \<in> S
finite (vars S)
max_set (vars S) < n
\<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\<langle>\<^bold># n/0\<rangle> # 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> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>
\<nexists>S'. set S' \<subseteq> S \<and> S' \<turnstile> \<^bold>\<bottom>
\<^bold>\<not> \<^bold>\<forall> p \<in> S
finite (vars S)
max_set (vars S) < n
\<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; \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
set S' \<subseteq> S
\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> # S' \<turnstile> \<^bold>\<bottom>

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

goal (1 subgoal):
 1. \<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> S' \<^bold>\<leadsto> \<^bold>\<bottom>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> S' \<^bold>\<leadsto> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> S' \<^bold>\<leadsto> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
have \<open>max_list (vars_fm p) < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_var p < n
[PROOF STEP]
using assms(2-4) max_list_in_set
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> \<^bold>\<forall> p \<in> S
finite (vars S)
max_set (vars S) < n
\<lbrakk>finite ?S; set ?xs \<subseteq> ?S\<rbrakk> \<Longrightarrow> max_list ?xs \<le> max_set ?S

goal (1 subgoal):
 1. max_var p < n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
max_var p < n

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
max_var p < n

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
have \<open>\<forall>p \<in> set S'. max_list (vars_fm p) < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>set S'. max_var p < n
[PROOF STEP]
using \<open>set S' \<subseteq> S\<close> assms(3-4) max_list_in_set
[PROOF STATE]
proof (prove)
using this:
set S' \<subseteq> S
finite (vars S)
max_set (vars S) < n
\<lbrakk>finite ?S; set ?xs \<subseteq> ?S\<rbrakk> \<Longrightarrow> max_list ?xs \<le> max_set ?S

goal (1 subgoal):
 1. \<forall>p\<in>set S'. max_var p < n
[PROOF STEP]
by (meson Union_upper image_eqI order_le_less_trans subsetD)
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set S'. max_var p < n

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set S'. max_var p < n
[PROOF STEP]
have \<open>max_list (concat (map vars_fm S')) < n\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set S'. max_var p < n

goal (1 subgoal):
 1. max_list (concat (map vars_fm S')) < n
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set S'. max_var p < n
max_set (vars S) < n

goal (1 subgoal):
 1. max_list (concat (map vars_fm S')) < n
[PROOF STEP]
by (induct S') (auto simp: max_list_append)
[PROOF STATE]
proof (state)
this:
max_list (concat (map vars_fm S')) < n

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max_list (concat (map vars_fm S')) < n
[PROOF STEP]
have \<open>max_list (vars_fm (S' \<^bold>\<leadsto> \<^bold>\<bottom>)) < n\<close>
[PROOF STATE]
proof (prove)
using this:
max_list (concat (map vars_fm S')) < n

goal (1 subgoal):
 1. max_var (S' \<^bold>\<leadsto> \<^bold>\<bottom>) < n
[PROOF STEP]
unfolding imply_vars_fm max_list_append
[PROOF STATE]
proof (prove)
using this:
max_list (concat (map vars_fm S')) < n

goal (1 subgoal):
 1. max (max_list (concat (map vars_fm S'))) (max_var \<^bold>\<bottom>) < n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
max_var (S' \<^bold>\<leadsto> \<^bold>\<bottom>) < n

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> S' \<^bold>\<leadsto> \<^bold>\<bottom>
max_var p < n
max_var (S' \<^bold>\<leadsto> \<^bold>\<bottom>) < n
[PROOF STEP]
have \<open>\<turnstile> \<^bold>\<not> \<^bold>\<forall>p \<^bold>\<longrightarrow> S' \<^bold>\<leadsto> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> S' \<^bold>\<leadsto> \<^bold>\<bottom>
max_var p < n
max_var (S' \<^bold>\<leadsto> \<^bold>\<bottom>) < n

goal (1 subgoal):
 1. \<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> S' \<^bold>\<leadsto> \<^bold>\<bottom>
[PROOF STEP]
using GR'
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> S' \<^bold>\<leadsto> \<^bold>\<bottom>
max_var p < n
max_var (S' \<^bold>\<leadsto> \<^bold>\<bottom>) < n
\<lbrakk>\<turnstile> \<^bold>\<not> ?p\<langle>\<^bold># ?n/0\<rangle> \<^bold>\<longrightarrow> ?q; max_var ?p < ?n; max_var ?q < ?n\<rbrakk> \<Longrightarrow> \<turnstile> \<^bold>\<not> \<^bold>\<forall> ?p \<^bold>\<longrightarrow> ?q

goal (1 subgoal):
 1. \<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> S' \<^bold>\<leadsto> \<^bold>\<bottom>
[PROOF STEP]
unfolding max_list_append
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<^bold>\<longrightarrow> S' \<^bold>\<leadsto> \<^bold>\<bottom>
max_var p < n
max_var (S' \<^bold>\<leadsto> \<^bold>\<bottom>) < n
\<lbrakk>\<turnstile> \<^bold>\<not> ?p\<langle>\<^bold># ?n/0\<rangle> \<^bold>\<longrightarrow> ?q; max_var ?p < ?n; max_var ?q < ?n\<rbrakk> \<Longrightarrow> \<turnstile> \<^bold>\<not> \<^bold>\<forall> ?p \<^bold>\<longrightarrow> ?q

goal (1 subgoal):
 1. \<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> S' \<^bold>\<leadsto> \<^bold>\<bottom>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<turnstile> \<^bold>\<not> \<^bold>\<forall> p \<^bold>\<longrightarrow> S' \<^bold>\<leadsto> \<^bold>\<bottom>

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

goal (1 subgoal):
 1. \<^bold>\<not> \<^bold>\<forall> p # S' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> \<^bold>\<forall> p # S' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> \<^bold>\<forall> p # S' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {\<^bold>\<not> p\<langle>\<^bold># n/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
have \<open>set ((\<^bold>\<not> \<^bold>\<forall>p) # S') \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (\<^bold>\<not> \<^bold>\<forall> p # S') \<subseteq> S
[PROOF STEP]
using \<open>set S' \<subseteq> S\<close> assms(2)
[PROOF STATE]
proof (prove)
using this:
set S' \<subseteq> S
\<^bold>\<not> \<^bold>\<forall> p \<in> S

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

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> \<^bold>\<forall> p # S' \<turnstile> \<^bold>\<bottom>
set (\<^bold>\<not> \<^bold>\<forall> p # 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


[STATEMENT]
lemma consistent_add_instance:
  assumes \<open>consistent S\<close> and \<open>\<^bold>\<forall>p \<in> S\<close>
  shows \<open>consistent ({p\<langle>t/0\<rangle>} \<union> S)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent ({p\<langle>t/0\<rangle>} \<union> S)
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>S'. set S' \<subseteq> {p\<langle>t/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {p\<langle>t/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<exists>S'. set S' \<subseteq> {p\<langle>t/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (state)
this:
\<exists>S'. set S' \<subseteq> {p\<langle>t/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>

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

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>set S' \<subseteq> S; p\<langle>t/0\<rangle> # 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\<langle>t/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>
consistent S
\<^bold>\<forall> p \<in> 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\<langle>t/0\<rangle> # 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\<langle>t/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>
\<nexists>S'. set S' \<subseteq> S \<and> S' \<turnstile> \<^bold>\<bottom>
\<^bold>\<forall> p \<in> 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\<langle>t/0\<rangle> # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set S' \<subseteq> S
p\<langle>t/0\<rangle> # S' \<turnstile> \<^bold>\<bottom>

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

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {p\<langle>t/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
have \<open>\<turnstile> \<^bold>\<forall>p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>
[PROOF STEP]
using IA
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<^bold>\<forall> ?p \<^bold>\<longrightarrow> ?p\<langle>?t/0\<rangle>

goal (1 subgoal):
 1. \<turnstile> \<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<turnstile> \<^bold>\<forall> p \<^bold>\<longrightarrow> p\<langle>t/0\<rangle>

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

goal (1 subgoal):
 1. \<^bold>\<forall> p # S' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
by (meson add_imply cut deduct(1))
[PROOF STATE]
proof (state)
this:
\<^bold>\<forall> p # S' \<turnstile> \<^bold>\<bottom>

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

goal (1 subgoal):
 1. \<exists>S'. set S' \<subseteq> {p\<langle>t/0\<rangle>} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom> \<Longrightarrow> False
[PROOF STEP]
have \<open>set ((\<^bold>\<forall>p) # S') \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (\<^bold>\<forall> p # S') \<subseteq> S
[PROOF STEP]
using \<open>set S' \<subseteq> S\<close> assms(2)
[PROOF STATE]
proof (prove)
using this:
set S' \<subseteq> S
\<^bold>\<forall> p \<in> S

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

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<forall> p # S' \<turnstile> \<^bold>\<bottom>
set (\<^bold>\<forall> p # 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


[STATEMENT]
lemma Extend_subset: \<open>S \<subseteq> Extend S f\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> Extend S f
[PROOF STEP]
unfolding Extend_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> \<Union> (range (extend S f))
[PROOF STEP]
by (metis Union_upper extend.simps(1) range_eqI)


[STATEMENT]
lemma extend_bound: \<open>(\<Union>n \<le> m. extend S f n) = extend S f m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (extend S f ` {..m}) = extend S f m
[PROOF STEP]
by (induct m) (simp_all add: atMost_Suc Let_def)


[STATEMENT]
lemma finite_vars_witness [simp]: \<open>finite (vars (witness used p))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (vars (witness used p))
[PROOF STEP]
by (induct used p rule: witness.induct) simp_all


[STATEMENT]
lemma finite_vars_extend [simp]: \<open>finite (vars S) \<Longrightarrow> finite (vars (extend S f n))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (vars S) \<Longrightarrow> finite (vars (extend S f n))
[PROOF STEP]
by (induct n) (simp_all add: Let_def)


[STATEMENT]
lemma max_list_mono: \<open>set xs \<subseteq> set ys \<Longrightarrow> max_list xs \<le> max_list ys\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> set ys \<Longrightarrow> max_list xs \<le> max_list ys
[PROOF STEP]
using max_list_max max_list_in_Cons
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set ?xs. x \<le> max_list ?xs
?xs \<noteq> [] \<Longrightarrow> max_list ?xs \<in> set ?xs

goal (1 subgoal):
 1. set xs \<subseteq> set ys \<Longrightarrow> max_list xs \<le> max_list ys
[PROOF STEP]
by (metis less_nat_zero_code linorder_not_le max_list.simps(1) subset_code(1))