[STATEMENT]
theorem tnd: \<open>[] \<turnstile> Or (Pred p []) (Neg (Pred p []))\<close> (is \<open>_ \<turnstile> ?or\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
have \<open>[Neg ?or] \<turnstile> Neg ?or\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Or (Pred p []) (Neg (Pred p [])))
[PROOF STEP]
by (simp add: Assum)
[PROOF STATE]
proof (state)
this:
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Or (Pred p []) (Neg (Pred p [])))

goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Or (Pred p []) (Neg (Pred p [])))

goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Or (Pred p []) (Neg (Pred p [])))

goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
have \<open>[Pred p [], Neg ?or] \<turnstile> Neg ?or\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Or (Pred p []) (Neg (Pred p [])))
[PROOF STEP]
by (simp add: Assum)
[PROOF STATE]
proof (state)
this:
[Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Or (Pred p []) (Neg (Pred p [])))

goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Or (Pred p []) (Neg (Pred p [])))

goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
have \<open>[Pred p [], Neg ?or] \<turnstile> Pred p []\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Pred p []
[PROOF STEP]
by (simp add: Assum)
[PROOF STATE]
proof (state)
this:
[Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Pred p []

goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Pred p []
[PROOF STEP]
have \<open>[Pred p [], Neg ?or] \<turnstile> ?or\<close>
[PROOF STATE]
proof (prove)
using this:
[Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Pred p []

goal (1 subgoal):
 1. [Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
by (rule OrI1)
[PROOF STATE]
proof (state)
this:
[Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Or (Pred p []) (Neg (Pred p []))

goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Or (Pred p []) (Neg (Pred p [])))
[Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
have \<open>[Pred p [], Neg ?or] \<turnstile> FF\<close>
[PROOF STATE]
proof (prove)
using this:
[Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Or (Pred p []) (Neg (Pred p [])))
[Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Or (Pred p []) (Neg (Pred p []))

goal (1 subgoal):
 1. [Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> FF
[PROOF STEP]
by (rule NegE)
[PROOF STATE]
proof (state)
this:
[Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> FF

goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> FF
[PROOF STEP]
have \<open>[Neg ?or] \<turnstile> Neg (Pred p [])\<close>
[PROOF STATE]
proof (prove)
using this:
[Pred p [], Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> FF

goal (1 subgoal):
 1. [Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Pred p [])
[PROOF STEP]
by (rule NegI)
[PROOF STATE]
proof (state)
this:
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Pred p [])

goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Pred p [])
[PROOF STEP]
have \<open>[Neg ?or] \<turnstile> ?or\<close>
[PROOF STATE]
proof (prove)
using this:
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Pred p [])

goal (1 subgoal):
 1. [Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
by (rule OrI2)
[PROOF STATE]
proof (state)
this:
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Or (Pred p []) (Neg (Pred p []))

goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Or (Pred p []) (Neg (Pred p []))

goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Or (Pred p []) (Neg (Pred p [])))
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
have \<open>[Neg ?or] \<turnstile> FF\<close>
[PROOF STATE]
proof (prove)
using this:
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Neg (Or (Pred p []) (Neg (Pred p [])))
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> Or (Pred p []) (Neg (Pred p []))

goal (1 subgoal):
 1. [Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> FF
[PROOF STEP]
by (rule NegE)
[PROOF STATE]
proof (state)
this:
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> FF

goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> FF
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[Neg (Or (Pred p []) (Neg (Pred p [])))] \<turnstile> FF

goal (1 subgoal):
 1. [] \<turnstile> Or (Pred p []) (Neg (Pred p []))
[PROOF STEP]
by (rule Class)
[PROOF STATE]
proof (state)
this:
[] \<turnstile> Or (Pred p []) (Neg (Pred p []))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ex_all_commute:
  \<open>([]::(nat, 'b) form list) \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0])))
     (Forall (Exists (Pred p [Var 0, Var 1])))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
let ?forall = \<open>Forall (Pred p [Var 1, Var 0]) :: (nat, 'b) form\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
have \<open>[Exists ?forall] \<turnstile> Exists ?forall\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Forall (Pred p [Var 1, Var 0]))
[PROOF STEP]
by (simp add: Assum)
[PROOF STATE]
proof (state)
this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Forall (Pred p [Var 1, Var 0]))

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Forall (Pred p [Var 1, Var 0]))

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Forall (Pred p [Var 1, Var 0]))

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
have \<open>[?forall[App 1 []/0], Exists ?forall] \<turnstile> Forall (Pred p [App 1 [], Var 0])\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Forall (Pred p [App 1 [], Var 0])
[PROOF STEP]
by (simp add: Assum)
[PROOF STATE]
proof (state)
this:
[Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Forall (Pred p [App 1 [], Var 0])

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Forall (Pred p [App 1 [], Var 0])

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
have \<open>[Pred p [App 1 [], Var 0][App 0 []/0], ?forall[App 1 []/0],
      Exists ?forall] \<turnstile> Pred p [Var 0, App 0 []][App 1 []/0]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Pred p [App 1 [], Var 0][App 0 []/0], Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Pred p [Var 0, App 0 []][App 1 []/0]
[PROOF STEP]
by (simp add: Assum)
[PROOF STATE]
proof (state)
this:
[Pred p [App 1 [], Var 0][App 0 []/0], Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Pred p [Var 0, App 0 []][App 1 []/0]

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Forall (Pred p [App 1 [], Var 0])
[Pred p [App 1 [], Var 0][App 0 []/0], Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Pred p [Var 0, App 0 []][App 1 []/0]
[PROOF STEP]
have \<open>[?forall[App 1 []/0], Exists ?forall] \<turnstile> (Pred p [Var 0, App 0 []])[App 1 []/0]\<close>
[PROOF STATE]
proof (prove)
using this:
[Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Forall (Pred p [App 1 [], Var 0])
[Pred p [App 1 [], Var 0][App 0 []/0], Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Pred p [Var 0, App 0 []][App 1 []/0]

goal (1 subgoal):
 1. [Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Pred p [Var 0, App 0 []][App 1 []/0]
[PROOF STEP]
by (rule ForallE')
[PROOF STATE]
proof (state)
this:
[Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Pred p [Var 0, App 0 []][App 1 []/0]

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
[Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Pred p [Var 0, App 0 []][App 1 []/0]

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Pred p [Var 0, App 0 []][App 1 []/0]
[PROOF STEP]
have \<open>[?forall[App 1 []/0], Exists ?forall] \<turnstile> Exists (Pred p [Var 0, App 0 []])\<close>
[PROOF STATE]
proof (prove)
using this:
[Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Pred p [Var 0, App 0 []][App 1 []/0]

goal (1 subgoal):
 1. [Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, App 0 []])
[PROOF STEP]
by (rule ExistsI)
[PROOF STATE]
proof (state)
this:
[Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, App 0 []])

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, App 0 []])

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
have \<open>list_all (\<lambda>p. 1 \<notin> params p) [Exists ?forall]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (\<lambda>p. 1 \<notin> params p) [Exists (Forall (Pred p [Var 1, Var 0]))]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list_all (\<lambda>p. 1 \<notin> params p) [Exists (Forall (Pred p [Var 1, Var 0]))]

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_all (\<lambda>p. 1 \<notin> params p) [Exists (Forall (Pred p [Var 1, Var 0]))]

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
have \<open>1 \<notin> params ?forall\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<notin> params (Forall (Pred p [Var 1, Var 0]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<notin> params (Forall (Pred p [Var 1, Var 0]))

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 \<notin> params (Forall (Pred p [Var 1, Var 0]))

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
have \<open>1 \<notin> params (Exists (Pred p [Var 0, App (0 :: nat) []]))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<notin> params (Exists (Pred p [Var 0, App 0 []]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<notin> params (Exists (Pred p [Var 0, App 0 []]))

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Forall (Pred p [Var 1, Var 0]))
[Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, App 0 []])
list_all (\<lambda>p. 1 \<notin> params p) [Exists (Forall (Pred p [Var 1, Var 0]))]
1 \<notin> params (Forall (Pred p [Var 1, Var 0]))
1 \<notin> params (Exists (Pred p [Var 0, App 0 []]))
[PROOF STEP]
have \<open>[Exists ?forall] \<turnstile> Exists (Pred p [Var 0, App 0 []])\<close>
[PROOF STATE]
proof (prove)
using this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Forall (Pred p [Var 1, Var 0]))
[Forall (Pred p [Var 1, Var 0])[App 1 []/0], Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, App 0 []])
list_all (\<lambda>p. 1 \<notin> params p) [Exists (Forall (Pred p [Var 1, Var 0]))]
1 \<notin> params (Forall (Pred p [Var 1, Var 0]))
1 \<notin> params (Exists (Pred p [Var 0, App 0 []]))

goal (1 subgoal):
 1. [Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, App 0 []])
[PROOF STEP]
by (rule ExistsE)
[PROOF STATE]
proof (state)
this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, App 0 []])

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, App 0 []])
[PROOF STEP]
have \<open>[Exists ?forall] \<turnstile> (Exists (Pred p [Var 0, Var 1]))[App 0 []/0]\<close>
[PROOF STATE]
proof (prove)
using this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, App 0 []])

goal (1 subgoal):
 1. [Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, Var 1])[App 0 []/0]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, Var 1])[App 0 []/0]

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, Var 1])[App 0 []/0]

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
have \<open>list_all (\<lambda>p. 0 \<notin> params p) [Exists ?forall]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (\<lambda>p. 0 \<notin> params p) [Exists (Forall (Pred p [Var 1, Var 0]))]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list_all (\<lambda>p. 0 \<notin> params p) [Exists (Forall (Pred p [Var 1, Var 0]))]

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_all (\<lambda>p. 0 \<notin> params p) [Exists (Forall (Pred p [Var 1, Var 0]))]

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
have \<open>0 \<notin> params (Exists (Pred p [Var 0, Var 1]))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<notin> params (Exists (Pred p [Var 0, Var 1]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::?'a1) \<notin> params (Exists (Pred p [Var 0, Var 1]))

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, Var 1])[App 0 []/0]
list_all (\<lambda>p. 0 \<notin> params p) [Exists (Forall (Pred p [Var 1, Var 0]))]
(0::?'a1) \<notin> params (Exists (Pred p [Var 0, Var 1]))
[PROOF STEP]
have \<open>[Exists ?forall] \<turnstile> Forall (Exists (Pred p [Var 0, Var 1]))\<close>
[PROOF STATE]
proof (prove)
using this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Exists (Pred p [Var 0, Var 1])[App 0 []/0]
list_all (\<lambda>p. 0 \<notin> params p) [Exists (Forall (Pred p [Var 1, Var 0]))]
(0::?'a1) \<notin> params (Exists (Pred p [Var 0, Var 1]))

goal (1 subgoal):
 1. [Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Forall (Exists (Pred p [Var 0, Var 1]))
[PROOF STEP]
by (rule ForallI)
[PROOF STATE]
proof (state)
this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Forall (Exists (Pred p [Var 0, Var 1]))

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Forall (Exists (Pred p [Var 0, Var 1]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[Exists (Forall (Pred p [Var 1, Var 0]))] \<turnstile> Forall (Exists (Pred p [Var 0, Var 1]))

goal (1 subgoal):
 1. [] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))
[PROOF STEP]
by (rule ImplI)
[PROOF STATE]
proof (state)
this:
[] \<turnstile> Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1])))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem drinker: \<open>([]::(nat, 'b) form list) \<turnstile>
  Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
let ?impl = \<open>(Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))) :: (nat, 'b) form\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
let ?G' = \<open>[Pred P [Var 0], Neg (Exists ?impl)]\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
let ?G = \<open>Neg (Pred P [App 0 []]) # ?G'\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
have \<open>?G \<turnstile> Neg (Exists ?impl)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))
[PROOF STEP]
by (simp add: Assum)
[PROOF STATE]
proof (state)
this:
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
have \<open>Pred P [App 0 []] # ?G \<turnstile> Neg (Pred P [App 0 []])\<close>
    and \<open>Pred P [App 0 []] # ?G \<turnstile> Pred P [App 0 []]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Neg (Pred P [App 0 []]) &&& [Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Pred P [App 0 []]
[PROOF STEP]
by (simp_all add: Assum)
[PROOF STATE]
proof (state)
this:
[Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Neg (Pred P [App 0 []])
[Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Pred P [App 0 []]

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Neg (Pred P [App 0 []])
[Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Pred P [App 0 []]
[PROOF STEP]
have \<open>Pred P [App 0 []] # ?G \<turnstile> FF\<close>
[PROOF STATE]
proof (prove)
using this:
[Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Neg (Pred P [App 0 []])
[Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Pred P [App 0 []]

goal (1 subgoal):
 1. [Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> FF
[PROOF STEP]
by (rule NegE)
[PROOF STATE]
proof (state)
this:
[Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> FF

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> FF
[PROOF STEP]
have \<open>Pred P [App 0 []] # ?G \<turnstile> Forall (Pred P [Var 0])\<close>
[PROOF STATE]
proof (prove)
using this:
[Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> FF

goal (1 subgoal):
 1. [Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Forall (Pred P [Var 0])
[PROOF STEP]
by (rule FFE)
[PROOF STATE]
proof (state)
this:
[Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Forall (Pred P [Var 0])

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Forall (Pred P [Var 0])
[PROOF STEP]
have \<open>?G \<turnstile> ?impl[App 0 []/0]\<close>
[PROOF STATE]
proof (prove)
using this:
[Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Forall (Pred P [Var 0])

goal (1 subgoal):
 1. [Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))[App 0 []/0]
[PROOF STEP]
using ImplI
[PROOF STATE]
proof (prove)
using this:
[Pred P [App 0 []], Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Forall (Pred P [Var 0])
?a # ?G \<turnstile> ?b \<Longrightarrow> ?G \<turnstile> Impl ?a ?b

goal (1 subgoal):
 1. [Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))[App 0 []/0]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))[App 0 []/0]

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))[App 0 []/0]
[PROOF STEP]
have \<open>?G \<turnstile> Exists ?impl\<close>
[PROOF STATE]
proof (prove)
using this:
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))[App 0 []/0]

goal (1 subgoal):
 1. [Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
by (rule ExistsI)
[PROOF STATE]
proof (state)
this:
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
have \<open>?G \<turnstile> FF\<close>
[PROOF STATE]
proof (prove)
using this:
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))

goal (1 subgoal):
 1. [Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> FF
[PROOF STEP]
by (rule NegE)
[PROOF STATE]
proof (state)
this:
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> FF

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> FF
[PROOF STEP]
have \<open>?G' \<turnstile> Pred P [Var 0][App 0 []/0]\<close>
[PROOF STATE]
proof (prove)
using this:
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> FF

goal (1 subgoal):
 1. [Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Pred P [Var 0][App 0 []/0]
[PROOF STEP]
using Class
[PROOF STATE]
proof (prove)
using this:
[Neg (Pred P [App 0 []]), Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> FF
Neg ?a # ?G \<turnstile> FF \<Longrightarrow> ?G \<turnstile> ?a

goal (1 subgoal):
 1. [Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Pred P [Var 0][App 0 []/0]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Pred P [Var 0][App 0 []/0]

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Pred P [Var 0][App 0 []/0]

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
have \<open>list_all (\<lambda>p. (0 :: nat) \<notin> params p) ?G'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (\<lambda>p. 0 \<notin> params p) [Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list_all (\<lambda>p. 0 \<notin> params p) [Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))]

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_all (\<lambda>p. 0 \<notin> params p) [Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))]

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
have \<open>(0 :: nat) \<notin> params (Pred P [Var 0])\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> params (Pred P [Var 0])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<notin> params (Pred P [Var 0])

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Pred P [Var 0][App 0 []/0]
list_all (\<lambda>p. 0 \<notin> params p) [Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))]
0 \<notin> params (Pred P [Var 0])
[PROOF STEP]
have \<open>?G' \<turnstile> Forall (Pred P [Var 0])\<close>
[PROOF STATE]
proof (prove)
using this:
[Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Pred P [Var 0][App 0 []/0]
list_all (\<lambda>p. 0 \<notin> params p) [Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))]
0 \<notin> params (Pred P [Var 0])

goal (1 subgoal):
 1. [Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Forall (Pred P [Var 0])
[PROOF STEP]
by (rule ForallI)
[PROOF STATE]
proof (state)
this:
[Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Forall (Pred P [Var 0])

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Forall (Pred P [Var 0])
[PROOF STEP]
have \<open>[Neg (Exists ?impl)] \<turnstile> ?impl[Var 0/0]\<close>
[PROOF STATE]
proof (prove)
using this:
[Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Forall (Pred P [Var 0])

goal (1 subgoal):
 1. [Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))[Var 0/0]
[PROOF STEP]
using ImplI
[PROOF STATE]
proof (prove)
using this:
[Pred P [Var 0], Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Forall (Pred P [Var 0])
?a # ?G \<turnstile> ?b \<Longrightarrow> ?G \<turnstile> Impl ?a ?b

goal (1 subgoal):
 1. [Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))[Var 0/0]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))[Var 0/0]

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))[Var 0/0]
[PROOF STEP]
have \<open>[Neg (Exists ?impl)] \<turnstile> Exists ?impl\<close>
[PROOF STATE]
proof (prove)
using this:
[Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))[Var 0/0]

goal (1 subgoal):
 1. [Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
by (rule ExistsI)
[PROOF STATE]
proof (state)
this:
[Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[Neg (Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))))] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))

goal (1 subgoal):
 1. [] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))
[PROOF STEP]
by (rule Class')
[PROOF STATE]
proof (state)
this:
[] \<turnstile> Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem peirce:
  \<open>[] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])\<close>
  (is \<open>[] \<turnstile> Impl ?PQP (Pred P [])\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
let ?PQPP = \<open>Impl ?PQP (Pred P [])\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
have \<open>[?PQP, Neg ?PQPP] \<turnstile> ?PQP\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])
[PROOF STEP]
by (simp add: Assum)
[PROOF STATE]
proof (state)
this:
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
have \<open>[Pred P [], ?PQP, Neg ?PQPP] \<turnstile> Neg ?PQPP\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))
[PROOF STEP]
by (simp add: Assum)
[PROOF STATE]
proof (state)
this:
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
have \<open>[?PQP, Pred P [], ?PQP, Neg ?PQPP] \<turnstile> Pred P []\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Pred P []
[PROOF STEP]
by (simp add: Assum)
[PROOF STATE]
proof (state)
this:
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Pred P []

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Pred P []
[PROOF STEP]
have \<open>[Pred P [], ?PQP, Neg ?PQPP] \<turnstile> ?PQPP\<close>
[PROOF STATE]
proof (prove)
using this:
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Pred P []

goal (1 subgoal):
 1. [Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
by (rule ImplI)
[PROOF STATE]
proof (state)
this:
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
have \<open>[Pred P [], ?PQP, Neg ?PQPP] \<turnstile> FF\<close>
[PROOF STATE]
proof (prove)
using this:
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])

goal (1 subgoal):
 1. [Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> FF
[PROOF STEP]
by (rule NegE)
[PROOF STATE]
proof (state)
this:
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> FF

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> FF

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> FF
[PROOF STEP]
have \<open>[Pred P [], ?PQP, Neg ?PQPP] \<turnstile> Pred Q []\<close>
[PROOF STATE]
proof (prove)
using this:
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> FF

goal (1 subgoal):
 1. [Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Pred Q []
[PROOF STEP]
by (rule FFE)
[PROOF STATE]
proof (state)
this:
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Pred Q []

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Pred Q []
[PROOF STEP]
have \<open>[?PQP, Neg ?PQPP] \<turnstile> Impl (Pred P []) (Pred Q [])\<close>
[PROOF STATE]
proof (prove)
using this:
[Pred P [], Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Pred Q []

goal (1 subgoal):
 1. [Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Pred P []) (Pred Q [])
[PROOF STEP]
by (rule ImplI)
[PROOF STATE]
proof (state)
this:
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Pred P []) (Pred Q [])

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Pred P []) (Pred Q [])
[PROOF STEP]
have \<open>[?PQP, Neg ?PQPP] \<turnstile> Pred P []\<close>
[PROOF STATE]
proof (prove)
using this:
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Pred P []) (Pred Q [])

goal (1 subgoal):
 1. [Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Pred P []
[PROOF STEP]
by (rule ImplE)
[PROOF STATE]
proof (state)
this:
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Pred P []

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Pred P []
[PROOF STEP]
have \<open>[Neg ?PQPP] \<turnstile> ?PQPP\<close>
[PROOF STATE]
proof (prove)
using this:
[Impl (Impl (Pred P []) (Pred Q [])) (Pred P []), Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Pred P []

goal (1 subgoal):
 1. [Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
by (rule ImplI)
[PROOF STATE]
proof (state)
this:
[Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
show \<open>[] \<turnstile> ?PQPP\<close>
[PROOF STATE]
proof (prove)
using this:
[Neg (Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P []))] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])

goal (1 subgoal):
 1. [] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])
[PROOF STEP]
by (rule Class')
[PROOF STATE]
proof (state)
this:
[] \<turnstile> Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem correctness: \<open>G \<turnstile> p \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<turnstile> p \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> p
[PROOF STEP]
proof (induct p rule: deriv.induct)
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>a G. a \<in> set G \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 2. \<And>G. \<forall>e f g. e,f,g,G \<Turnstile> TT
 3. \<And>G a. \<lbrakk>G \<turnstile> FF; \<forall>e f g. e,f,g,G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 4. \<And>a G. \<lbrakk>a # G \<turnstile> FF; \<forall>e f g. e,f,g,a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Neg a
 5. \<And>G a. \<lbrakk>G \<turnstile> Neg a; \<forall>e f g. e,f,g,G \<Turnstile> Neg a; G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> FF
 6. \<And>a G. \<lbrakk>Neg a # G \<turnstile> FF; \<forall>e f g. e,f,g,Neg a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 7. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a; G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> And a b
 8. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 9. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> b
 10. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
A total of 18 subgoals...
[PROOF STEP]
case (Assum a G)
[PROOF STATE]
proof (state)
this:
a \<in> set G

goal (18 subgoals):
 1. \<And>a G. a \<in> set G \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 2. \<And>G. \<forall>e f g. e,f,g,G \<Turnstile> TT
 3. \<And>G a. \<lbrakk>G \<turnstile> FF; \<forall>e f g. e,f,g,G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 4. \<And>a G. \<lbrakk>a # G \<turnstile> FF; \<forall>e f g. e,f,g,a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Neg a
 5. \<And>G a. \<lbrakk>G \<turnstile> Neg a; \<forall>e f g. e,f,g,G \<Turnstile> Neg a; G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> FF
 6. \<And>a G. \<lbrakk>Neg a # G \<turnstile> FF; \<forall>e f g. e,f,g,Neg a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 7. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a; G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> And a b
 8. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 9. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> b
 10. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
A total of 18 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> set G
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<in> set G

goal (1 subgoal):
 1. \<forall>e f g. e,f,g,G \<Turnstile> a
[PROOF STEP]
by (simp add: model_def list_all_iff)
[PROOF STATE]
proof (state)
this:
\<forall>e f g. e,f,g,G \<Turnstile> a

goal (17 subgoals):
 1. \<And>G. \<forall>e f g. e,f,g,G \<Turnstile> TT
 2. \<And>G a. \<lbrakk>G \<turnstile> FF; \<forall>e f g. e,f,g,G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 3. \<And>a G. \<lbrakk>a # G \<turnstile> FF; \<forall>e f g. e,f,g,a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Neg a
 4. \<And>G a. \<lbrakk>G \<turnstile> Neg a; \<forall>e f g. e,f,g,G \<Turnstile> Neg a; G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> FF
 5. \<And>a G. \<lbrakk>Neg a # G \<turnstile> FF; \<forall>e f g. e,f,g,Neg a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 6. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a; G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> And a b
 7. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 8. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> b
 9. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
 10. \<And>G b a. \<lbrakk>G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
A total of 17 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>G. \<forall>e f g. e,f,g,G \<Turnstile> TT
 2. \<And>G a. \<lbrakk>G \<turnstile> FF; \<forall>e f g. e,f,g,G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 3. \<And>a G. \<lbrakk>a # G \<turnstile> FF; \<forall>e f g. e,f,g,a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Neg a
 4. \<And>G a. \<lbrakk>G \<turnstile> Neg a; \<forall>e f g. e,f,g,G \<Turnstile> Neg a; G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> FF
 5. \<And>a G. \<lbrakk>Neg a # G \<turnstile> FF; \<forall>e f g. e,f,g,Neg a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 6. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a; G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> And a b
 7. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 8. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> b
 9. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
 10. \<And>G b a. \<lbrakk>G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
A total of 17 subgoals...
[PROOF STEP]
case (ForallI G a n)
[PROOF STATE]
proof (state)
this:
G \<turnstile> a[App n []/0]
\<forall>e f g. e,f,g,G \<Turnstile> a[App n []/0]
list_all (\<lambda>p. n \<notin> params p) G
n \<notin> params a

goal (17 subgoals):
 1. \<And>G. \<forall>e f g. e,f,g,G \<Turnstile> TT
 2. \<And>G a. \<lbrakk>G \<turnstile> FF; \<forall>e f g. e,f,g,G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 3. \<And>a G. \<lbrakk>a # G \<turnstile> FF; \<forall>e f g. e,f,g,a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Neg a
 4. \<And>G a. \<lbrakk>G \<turnstile> Neg a; \<forall>e f g. e,f,g,G \<Turnstile> Neg a; G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> FF
 5. \<And>a G. \<lbrakk>Neg a # G \<turnstile> FF; \<forall>e f g. e,f,g,Neg a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 6. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a; G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> And a b
 7. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 8. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> b
 9. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
 10. \<And>G b a. \<lbrakk>G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
A total of 17 subgoals...
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e f g. e,f,g,G \<Turnstile> Forall a
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e f g. e,f,g,G \<Turnstile> Forall a
[PROOF STEP]
fix f g and e :: \<open>nat \<Rightarrow> 'c\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e f g. e,f,g,G \<Turnstile> Forall a
[PROOF STEP]
have \<open>\<forall>z. e, (f(n := \<lambda>x. z)), g, G \<Turnstile> (a[App n []/0])\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. e,f(n := \<lambda>x. z),g,G \<Turnstile> a[App n []/0]
[PROOF STEP]
using ForallI
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> a[App n []/0]
\<forall>e f g. e,f,g,G \<Turnstile> a[App n []/0]
list_all (\<lambda>p. n \<notin> params p) G
n \<notin> params a

goal (1 subgoal):
 1. \<forall>z. e,f(n := \<lambda>x. z),g,G \<Turnstile> a[App n []/0]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>z. e,f(n := \<lambda>x. z),g,G \<Turnstile> a[App n []/0]

goal (1 subgoal):
 1. \<And>e f g. e,f,g,G \<Turnstile> Forall a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>z. e,f(n := \<lambda>x. z),g,G \<Turnstile> a[App n []/0]
[PROOF STEP]
have \<open>\<forall>z. list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>z. e,f(n := \<lambda>x. z),g,G \<Turnstile> a[App n []/0]

goal (1 subgoal):
 1. \<forall>z. list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a
[PROOF STEP]
using ForallI
[PROOF STATE]
proof (prove)
using this:
\<forall>z. e,f(n := \<lambda>x. z),g,G \<Turnstile> a[App n []/0]
G \<turnstile> a[App n []/0]
\<forall>e f g. e,f,g,G \<Turnstile> a[App n []/0]
list_all (\<lambda>p. n \<notin> params p) G
n \<notin> params a

goal (1 subgoal):
 1. \<forall>z. list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a
[PROOF STEP]
unfolding model_def
[PROOF STATE]
proof (prove)
using this:
\<forall>z. list_all (eval e (f(n := \<lambda>x. z)) g) G \<longrightarrow> eval e (f(n := \<lambda>x. z)) g (a[App n []/0])
G \<turnstile> a[App n []/0]
\<forall>e f g. list_all (eval e f g) G \<longrightarrow> eval e f g (a[App n []/0])
list_all (\<lambda>p. n \<notin> params p) G
n \<notin> params a

goal (1 subgoal):
 1. \<forall>z. list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>z. list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a

goal (1 subgoal):
 1. \<And>e f g. e,f,g,G \<Turnstile> Forall a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>z. list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a
[PROOF STEP]
show \<open>e,f,g,G \<Turnstile> Forall a\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>z. list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a

goal (1 subgoal):
 1. e,f,g,G \<Turnstile> Forall a
[PROOF STEP]
unfolding model_def
[PROOF STATE]
proof (prove)
using this:
\<forall>z. list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a

goal (1 subgoal):
 1. list_all (eval e f g) G \<longrightarrow> eval e f g (Forall a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e,f,g,G \<Turnstile> Forall a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>e f g. e,f,g,G \<Turnstile> Forall a

goal (16 subgoals):
 1. \<And>G. \<forall>e f g. e,f,g,G \<Turnstile> TT
 2. \<And>G a. \<lbrakk>G \<turnstile> FF; \<forall>e f g. e,f,g,G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 3. \<And>a G. \<lbrakk>a # G \<turnstile> FF; \<forall>e f g. e,f,g,a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Neg a
 4. \<And>G a. \<lbrakk>G \<turnstile> Neg a; \<forall>e f g. e,f,g,G \<Turnstile> Neg a; G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> FF
 5. \<And>a G. \<lbrakk>Neg a # G \<turnstile> FF; \<forall>e f g. e,f,g,Neg a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 6. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a; G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> And a b
 7. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 8. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> b
 9. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
 10. \<And>G b a. \<lbrakk>G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
A total of 16 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (16 subgoals):
 1. \<And>G. \<forall>e f g. e,f,g,G \<Turnstile> TT
 2. \<And>G a. \<lbrakk>G \<turnstile> FF; \<forall>e f g. e,f,g,G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 3. \<And>a G. \<lbrakk>a # G \<turnstile> FF; \<forall>e f g. e,f,g,a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Neg a
 4. \<And>G a. \<lbrakk>G \<turnstile> Neg a; \<forall>e f g. e,f,g,G \<Turnstile> Neg a; G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> FF
 5. \<And>a G. \<lbrakk>Neg a # G \<turnstile> FF; \<forall>e f g. e,f,g,Neg a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 6. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a; G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> And a b
 7. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 8. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> b
 9. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
 10. \<And>G b a. \<lbrakk>G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
A total of 16 subgoals...
[PROOF STEP]
case (ExistsE G a n b)
[PROOF STATE]
proof (state)
this:
G \<turnstile> Exists a
\<forall>e f g. e,f,g,G \<Turnstile> Exists a
a[App n []/0] # G \<turnstile> b
\<forall>e f g. e,f,g,a[App n []/0] # G \<Turnstile> b
list_all (\<lambda>p. n \<notin> params p) G
n \<notin> params a
n \<notin> params b

goal (16 subgoals):
 1. \<And>G. \<forall>e f g. e,f,g,G \<Turnstile> TT
 2. \<And>G a. \<lbrakk>G \<turnstile> FF; \<forall>e f g. e,f,g,G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 3. \<And>a G. \<lbrakk>a # G \<turnstile> FF; \<forall>e f g. e,f,g,a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Neg a
 4. \<And>G a. \<lbrakk>G \<turnstile> Neg a; \<forall>e f g. e,f,g,G \<Turnstile> Neg a; G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> FF
 5. \<And>a G. \<lbrakk>Neg a # G \<turnstile> FF; \<forall>e f g. e,f,g,Neg a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 6. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a; G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> And a b
 7. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 8. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> b
 9. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
 10. \<And>G b a. \<lbrakk>G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
A total of 16 subgoals...
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e f g. e,f,g,G \<Turnstile> b
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e f g. e,f,g,G \<Turnstile> b
[PROOF STEP]
fix f g and e :: \<open>nat \<Rightarrow> 'c\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e f g. e,f,g,G \<Turnstile> b
[PROOF STEP]
obtain z where \<open>list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z. list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ExistsE
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> Exists a
\<forall>e f g. e,f,g,G \<Turnstile> Exists a
a[App n []/0] # G \<turnstile> b
\<forall>e f g. e,f,g,a[App n []/0] # G \<Turnstile> b
list_all (\<lambda>p. n \<notin> params p) G
n \<notin> params a
n \<notin> params b

goal (1 subgoal):
 1. (\<And>z. list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding model_def
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> Exists a
\<forall>e f g. list_all (eval e f g) G \<longrightarrow> eval e f g (Exists a)
a[App n []/0] # G \<turnstile> b
\<forall>e f g. list_all (eval e f g) (a[App n []/0] # G) \<longrightarrow> eval e f g b
list_all (\<lambda>p. n \<notin> params p) G
n \<notin> params a
n \<notin> params b

goal (1 subgoal):
 1. (\<And>z. list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a

goal (1 subgoal):
 1. \<And>e f g. e,f,g,G \<Turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a
[PROOF STEP]
have \<open>e, (f(n := \<lambda>x. z)), g, G \<Turnstile> b\<close>
[PROOF STATE]
proof (prove)
using this:
list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a

goal (1 subgoal):
 1. e,f(n := \<lambda>x. z),g,G \<Turnstile> b
[PROOF STEP]
using ExistsE
[PROOF STATE]
proof (prove)
using this:
list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a
G \<turnstile> Exists a
\<forall>e f g. e,f,g,G \<Turnstile> Exists a
a[App n []/0] # G \<turnstile> b
\<forall>e f g. e,f,g,a[App n []/0] # G \<Turnstile> b
list_all (\<lambda>p. n \<notin> params p) G
n \<notin> params a
n \<notin> params b

goal (1 subgoal):
 1. e,f(n := \<lambda>x. z),g,G \<Turnstile> b
[PROOF STEP]
unfolding model_def
[PROOF STATE]
proof (prove)
using this:
list_all (eval e f g) G \<longrightarrow> eval (e\<langle>0:z\<rangle>) f g a
G \<turnstile> Exists a
\<forall>e f g. list_all (eval e f g) G \<longrightarrow> eval e f g (Exists a)
a[App n []/0] # G \<turnstile> b
\<forall>e f g. list_all (eval e f g) (a[App n []/0] # G) \<longrightarrow> eval e f g b
list_all (\<lambda>p. n \<notin> params p) G
n \<notin> params a
n \<notin> params b

goal (1 subgoal):
 1. list_all (eval e (f(n := \<lambda>x. z)) g) G \<longrightarrow> eval e (f(n := \<lambda>x. z)) g b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e,f(n := \<lambda>x. z),g,G \<Turnstile> b

goal (1 subgoal):
 1. \<And>e f g. e,f,g,G \<Turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e,f(n := \<lambda>x. z),g,G \<Turnstile> b
[PROOF STEP]
show \<open>e,f,g,G \<Turnstile> b\<close>
[PROOF STATE]
proof (prove)
using this:
e,f(n := \<lambda>x. z),g,G \<Turnstile> b

goal (1 subgoal):
 1. e,f,g,G \<Turnstile> b
[PROOF STEP]
using ExistsE
[PROOF STATE]
proof (prove)
using this:
e,f(n := \<lambda>x. z),g,G \<Turnstile> b
G \<turnstile> Exists a
\<forall>e f g. e,f,g,G \<Turnstile> Exists a
a[App n []/0] # G \<turnstile> b
\<forall>e f g. e,f,g,a[App n []/0] # G \<Turnstile> b
list_all (\<lambda>p. n \<notin> params p) G
n \<notin> params a
n \<notin> params b

goal (1 subgoal):
 1. e,f,g,G \<Turnstile> b
[PROOF STEP]
unfolding model_def
[PROOF STATE]
proof (prove)
using this:
list_all (eval e (f(n := \<lambda>x. z)) g) G \<longrightarrow> eval e (f(n := \<lambda>x. z)) g b
G \<turnstile> Exists a
\<forall>e f g. list_all (eval e f g) G \<longrightarrow> eval e f g (Exists a)
a[App n []/0] # G \<turnstile> b
\<forall>e f g. list_all (eval e f g) (a[App n []/0] # G) \<longrightarrow> eval e f g b
list_all (\<lambda>p. n \<notin> params p) G
n \<notin> params a
n \<notin> params b

goal (1 subgoal):
 1. list_all (eval e f g) G \<longrightarrow> eval e f g b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e,f,g,G \<Turnstile> b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>e f g. e,f,g,G \<Turnstile> b

goal (15 subgoals):
 1. \<And>G. \<forall>e f g. e,f,g,G \<Turnstile> TT
 2. \<And>G a. \<lbrakk>G \<turnstile> FF; \<forall>e f g. e,f,g,G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 3. \<And>a G. \<lbrakk>a # G \<turnstile> FF; \<forall>e f g. e,f,g,a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Neg a
 4. \<And>G a. \<lbrakk>G \<turnstile> Neg a; \<forall>e f g. e,f,g,G \<Turnstile> Neg a; G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> FF
 5. \<And>a G. \<lbrakk>Neg a # G \<turnstile> FF; \<forall>e f g. e,f,g,Neg a # G \<Turnstile> FF\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 6. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a; G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> And a b
 7. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> a
 8. \<And>G a b. \<lbrakk>G \<turnstile> And a b; \<forall>e f g. e,f,g,G \<Turnstile> And a b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> b
 9. \<And>G a b. \<lbrakk>G \<turnstile> a; \<forall>e f g. e,f,g,G \<Turnstile> a\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
 10. \<And>G b a. \<lbrakk>G \<turnstile> b; \<forall>e f g. e,f,g,G \<Turnstile> b\<rbrakk> \<Longrightarrow> \<forall>e f g. e,f,g,G \<Turnstile> Or a b
A total of 15 subgoals...
[PROOF STEP]
qed (simp_all add: model_def, blast+)