[STATEMENT]
lemma list_eval_Throw: 
assumes eval_e: "P \<turnstile> \<langle>throw x,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
shows "P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
from eval_e
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> \<langle>throw x,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>
[PROOF STEP]
obtain a where e': "e' = Throw a"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>throw x,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>

goal (1 subgoal):
 1. (\<And>a. e' = Throw a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases) (auto dest!: eval_final)
[PROOF STATE]
proof (state)
this:
e' = Throw a

goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
e' = Throw a

goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
fix es
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
have "\<And>vs. es = map Val vs @ throw x # es' 
           \<Longrightarrow> P \<turnstile> \<langle>es,s\<rangle>[\<Rightarrow>]\<langle>map Val vs @ e' # es',s'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>vs. es = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
proof (induct es type: list)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>vs. [] = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>[],s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list vs. \<lbrakk>\<And>vs. list = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>; a # list = map Val vs @ throw x # es'\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>a # list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] = map Val vs @ throw x # es'

goal (2 subgoals):
 1. \<And>vs. [] = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>[],s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list vs. \<lbrakk>\<And>vs. list = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>; a # list = map Val vs @ throw x # es'\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>a # list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
[] = map Val vs @ throw x # es'

goal (1 subgoal):
 1. P \<turnstile> \<langle>[],s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>[],s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. \<And>a list vs. \<lbrakk>\<And>vs. list = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>; a # list = map Val vs @ throw x # es'\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>a # list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list vs. \<lbrakk>\<And>vs. list = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>; a # list = map Val vs @ throw x # es'\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>a # list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
case (Cons e es vs)
[PROOF STATE]
proof (state)
this:
es = map Val ?vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val ?vs @ e' # es',s'\<rangle>
e # es = map Val vs @ throw x # es'

goal (1 subgoal):
 1. \<And>a list vs. \<lbrakk>\<And>vs. list = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>; a # list = map Val vs @ throw x # es'\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>a # list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
have e_es: "e # es = map Val vs @ throw x # es'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e # es = map Val vs @ throw x # es'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
e # es = map Val vs @ throw x # es'

goal (1 subgoal):
 1. \<And>a list vs. \<lbrakk>\<And>vs. list = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>; a # list = map Val vs @ throw x # es'\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>a # list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
show "P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
proof (cases vs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vs = [] \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
vs = []

goal (2 subgoals):
 1. vs = [] \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
with e_es
[PROOF STATE]
proof (chain)
picking this:
e # es = map Val vs @ throw x # es'
vs = []
[PROOF STEP]
obtain "e=throw x" "es=es'"
[PROOF STATE]
proof (prove)
using this:
e # es = map Val vs @ throw x # es'
vs = []

goal (1 subgoal):
 1. (\<lbrakk>e = throw x; es = es'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e = throw x
es = es'

goal (2 subgoals):
 1. vs = [] \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
e = throw x
es = es'

goal (2 subgoals):
 1. vs = [] \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
from eval_e e'
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> \<langle>throw x,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>
e' = Throw a
[PROOF STEP]
have "P \<turnstile> \<langle>throw x # es,s\<rangle> [\<Rightarrow>] \<langle>Throw a # es,s'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>throw x,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>
e' = Throw a

goal (1 subgoal):
 1. P \<turnstile> \<langle>throw x # es,s\<rangle> [\<Rightarrow>] \<langle>Throw a # es,s'\<rangle>
[PROOF STEP]
by (iprover intro: ConsThrow)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>throw x # es,s\<rangle> [\<Rightarrow>] \<langle>Throw a # es,s'\<rangle>

goal (2 subgoals):
 1. vs = [] \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
e = throw x
es = es'
P \<turnstile> \<langle>throw x # es,s\<rangle> [\<Rightarrow>] \<langle>Throw a # es,s'\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e = throw x
es = es'
P \<turnstile> \<langle>throw x # es,s\<rangle> [\<Rightarrow>] \<langle>Throw a # es,s'\<rangle>

goal (1 subgoal):
 1. P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
using Nil e'
[PROOF STATE]
proof (prove)
using this:
e = throw x
es = es'
P \<turnstile> \<langle>throw x # es,s\<rangle> [\<Rightarrow>] \<langle>Throw a # es,s'\<rangle>
vs = []
e' = Throw a

goal (1 subgoal):
 1. P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
case (Cons v vs')
[PROOF STATE]
proof (state)
this:
vs = v # vs'

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
have vs: "vs = v # vs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vs = v # vs'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
vs = v # vs'

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
with e_es
[PROOF STATE]
proof (chain)
picking this:
e # es = map Val vs @ throw x # es'
vs = v # vs'
[PROOF STEP]
obtain 
          e: "e=Val v" and es:"es= map Val vs' @ throw x # es'"
[PROOF STATE]
proof (prove)
using this:
e # es = map Val vs @ throw x # es'
vs = v # vs'

goal (1 subgoal):
 1. (\<lbrakk>e = Val v; es = map Val vs' @ throw x # es'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e = Val v
es = map Val vs' @ throw x # es'

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
from e
[PROOF STATE]
proof (chain)
picking this:
e = Val v
[PROOF STEP]
have "P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>"
[PROOF STATE]
proof (prove)
using this:
e = Val v

goal (1 subgoal):
 1. P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>
[PROOF STEP]
by (iprover intro: eval_evals.Val)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
from es
[PROOF STATE]
proof (chain)
picking this:
es = map Val vs' @ throw x # es'
[PROOF STEP]
have "P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs' @ e' # es',s'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
es = map Val vs' @ throw x # es'

goal (1 subgoal):
 1. P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs' @ e' # es',s'\<rangle>
[PROOF STEP]
by (rule Cons.hyps)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs' @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>
P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs' @ e' # es',s'\<rangle>
[PROOF STEP]
show 
          "P \<turnstile> \<langle>e#es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>
P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs' @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
using vs
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>
P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs' @ e' # es',s'\<rangle>
vs = v # vs'

goal (1 subgoal):
 1. P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
by (auto intro: eval_evals.Cons)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
es = map Val ?vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val ?vs @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?es3 = map Val ?vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>?es3,s\<rangle> [\<Rightarrow>] \<langle>map Val ?vs @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?es3 = map Val ?vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>?es3,s\<rangle> [\<Rightarrow>] \<langle>map Val ?vs @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
(*>*)

\<comment> \<open> separate evaluation of first subexp of a sequence \<close>