[STATEMENT]
lemma evaluate_total: "\<exists>s' r. evaluate True env s e (s', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
have "wf (less_than <*lex*> measure (size::exp \<Rightarrow> nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (less_than <*lex*> measure size)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf (less_than <*lex*> measure size)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf (less_than <*lex*> measure size)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf (less_than <*lex*> measure size)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (induction "(clock s, e)" arbitrary: env s e)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s e env. (\<And>sa ea env. ((clock sa, ea), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True env sa ea (s', r)) \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)

goal (1 subgoal):
 1. \<And>s e env. (\<And>sa ea env. ((clock sa, ea), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True env sa ea (s', r)) \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases e)
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>x1. e = Raise x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x41 x42. e = Con x41 x42 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x5. e = Var x5 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 14 subgoals...
[PROOF STEP]
case (Raise e')
[PROOF STATE]
proof (state)
this:
e = Raise e'

goal (14 subgoals):
 1. \<And>x1. e = Raise x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x41 x42. e = Con x41 x42 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x5. e = Var x5 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 14 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = Raise e'
[PROOF STEP]
have "\<exists>s' r. evaluate True env s e' (s', r)"
[PROOF STATE]
proof (prove)
using this:
e = Raise e'

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e' (s', r)
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
e = Raise e'
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e' (s', r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e' (s', r)

goal (14 subgoals):
 1. \<And>x1. e = Raise x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x41 x42. e = Con x41 x42 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x5. e = Var x5 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 14 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' r. evaluate True env s e' (s', r)
[PROOF STEP]
obtain s' r where "evaluate True env s e' (s', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True env s e' (s', r)

goal (1 subgoal):
 1. (\<And>s' r. evaluate True env s e' (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate True env s e' (s', r)

goal (14 subgoals):
 1. \<And>x1. e = Raise x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x41 x42. e = Con x41 x42 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x5. e = Var x5 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 14 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e' (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Raise
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Raise e') (s', r)
[PROOF STEP]
by (cases r) (metis raise1 raise2)+
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (13 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x41 x42. e = Con x41 x42 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x5. e = Var x5 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 13 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x41 x42. e = Con x41 x42 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x5. e = Var x5 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 13 subgoals...
[PROOF STEP]
case (Con cn es)
[PROOF STATE]
proof (state)
this:
e = Con cn es

goal (13 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x41 x42. e = Con x41 x42 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x5. e = Var x5 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 13 subgoals...
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases "do_con_check (c env) cn (length es)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. do_con_check (c env) cn (length es) \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<not> do_con_check (c env) cn (length es) \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
do_con_check (c env) cn (length es)

goal (2 subgoals):
 1. do_con_check (c env) cn (length es) \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<not> do_con_check (c env) cn (length es) \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
have "\<exists>s' vs. evaluate_list True env s (rev es) (s', vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' vs. evaluate_list True env s (rev es) (s', vs)
[PROOF STEP]
apply (rule evaluate_list_total0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e env s'. \<lbrakk>e \<in> set (rev es); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' vs. evaluate True env s' e (s'', vs)
[PROOF STEP]
apply (rule less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e env s'. \<lbrakk>e \<in> set (rev es); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> ((clock s', e), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
unfolding Con
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e env s'. \<lbrakk>e \<in> set (rev es); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> ((clock s', e), clock s, Con cn es) \<in> less_than <*lex*> measure size
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e s'. \<lbrakk>e \<in> set es; clock s' = clock s\<rbrakk> \<Longrightarrow> size e < Suc (size_list size es)
[PROOF STEP]
using Con
[PROOF STATE]
proof (prove)
using this:
e = Con cn es

goal (1 subgoal):
 1. \<And>e s'. \<lbrakk>e \<in> set es; clock s' = clock s\<rbrakk> \<Longrightarrow> size e < Suc (size_list size es)
[PROOF STEP]
apply (auto simp: less_eq_Suc_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e s'. \<lbrakk>e \<in> set es; clock s' = clock s; e = Con cn es\<rbrakk> \<Longrightarrow> size e \<le> size_list size es
[PROOF STEP]
apply (rule size_list_estimation')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>e s'. \<lbrakk>e \<in> set es; clock s' = clock s; e = Con cn es\<rbrakk> \<Longrightarrow> ?x10 e s' \<in> set es
 2. \<And>e s'. \<lbrakk>e \<in> set es; clock s' = clock s; e = Con cn es\<rbrakk> \<Longrightarrow> size e \<le> size (?x10 e s')
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e s'. \<lbrakk>e \<in> set es; clock s' = clock s; e = Con cn es\<rbrakk> \<Longrightarrow> size e \<le> size e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>s' vs. evaluate_list True env s (rev es) (s', vs)

goal (2 subgoals):
 1. do_con_check (c env) cn (length es) \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<not> do_con_check (c env) cn (length es) \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' vs. evaluate_list True env s (rev es) (s', vs)
[PROOF STEP]
obtain r s' where es: "evaluate_list True env s (rev es) (s', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' vs. evaluate_list True env s (rev es) (s', vs)

goal (1 subgoal):
 1. (\<And>s' r. evaluate_list True env s (rev es) (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate_list True env s (rev es) (s', r)

goal (2 subgoals):
 1. do_con_check (c env) cn (length es) \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<not> do_con_check (c env) cn (length es) \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Rval vs)
[PROOF STATE]
proof (state)
this:
r = Rval vs

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r = Rval vs

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
obtain v where "build_conv (c env) cn (rev vs) = Some v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v. build_conv (c env) cn (rev vs) = Some v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
do_con_check (c env) cn (length es)

goal (1 subgoal):
 1. (\<And>v. build_conv (c env) cn (rev vs) = Some v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases cn) (auto split: option.splits)
[PROOF STATE]
proof (state)
this:
build_conv (c env) cn (rev vs) = Some v

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r = Rval vs
build_conv (c env) cn (rev vs) = Some v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r = Rval vs
build_conv (c env) cn (rev vs) = Some v

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
using True es
[PROOF STATE]
proof (prove)
using this:
r = Rval vs
build_conv (c env) cn (rev vs) = Some v
do_con_check (c env) cn (length es)
evaluate_list True env s (rev es) (s', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Con
[PROOF STATE]
proof (prove)
using this:
r = Rval vs
build_conv (c env) cn (rev vs) = Some v
do_con_check (c env) cn (length es)
evaluate_list True env s (rev es) (s', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Con cn es) (s', r)
[PROOF STEP]
by (metis con1)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case Rerr
[PROOF STATE]
proof (state)
this:
r = Rerr x2_

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with True es
[PROOF STATE]
proof (chain)
picking this:
do_con_check (c env) cn (length es)
evaluate_list True env s (rev es) (s', r)
r = Rerr x2_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
do_con_check (c env) cn (length es)
evaluate_list True env s (rev es) (s', r)
r = Rerr x2_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Con
[PROOF STATE]
proof (prove)
using this:
do_con_check (c env) cn (length es)
evaluate_list True env s (rev es) (s', r)
r = Rerr x2_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Con cn es) (s', r)
[PROOF STEP]
by (metis con3)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. \<not> do_con_check (c env) cn (length es) \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> do_con_check (c env) cn (length es) \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> do_con_check (c env) cn (length es)

goal (1 subgoal):
 1. \<not> do_con_check (c env) cn (length es) \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with Con
[PROOF STATE]
proof (chain)
picking this:
e = Con cn es
\<not> do_con_check (c env) cn (length es)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e = Con cn es
\<not> do_con_check (c env) cn (length es)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
by (metis con2)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (12 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x5. e = Var x5 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 12 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x5. e = Var x5 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 12 subgoals...
[PROOF STEP]
case (Var n)
[PROOF STATE]
proof (state)
this:
e = Var n

goal (12 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x5. e = Var x5 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 12 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = Var n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e = Var n

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
by (cases "nsLookup (sem_env.v env) n") (metis var1 var2)+
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (11 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 11 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 11 subgoals...
[PROOF STEP]
case (App op es)
[PROOF STATE]
proof (state)
this:
e = App op es

goal (11 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 11 subgoals...
[PROOF STEP]
have "\<exists>s' vs. evaluate_list True env s (rev es) (s', vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' vs. evaluate_list True env s (rev es) (s', vs)
[PROOF STEP]
apply (rule evaluate_list_total0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e env s'. \<lbrakk>e \<in> set (rev es); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' vs. evaluate True env s' e (s'', vs)
[PROOF STEP]
apply (rule less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e env s'. \<lbrakk>e \<in> set (rev es); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> ((clock s', e), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
unfolding App
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e env s'. \<lbrakk>e \<in> set (rev es); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> ((clock s', e), clock s, App op es) \<in> less_than <*lex*> measure size
[PROOF STEP]
apply (auto simp: less_eq_Suc_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e s'. \<lbrakk>e \<in> set es; clock s' \<le> clock s; \<not> Suc (clock s') \<le> clock s\<rbrakk> \<Longrightarrow> size e \<le> size_list size es
[PROOF STEP]
apply (rule size_list_estimation')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>e s'. \<lbrakk>e \<in> set es; clock s' \<le> clock s; \<not> Suc (clock s') \<le> clock s\<rbrakk> \<Longrightarrow> ?x11 e s' \<in> set es
 2. \<And>e s'. \<lbrakk>e \<in> set es; clock s' \<le> clock s; \<not> Suc (clock s') \<le> clock s\<rbrakk> \<Longrightarrow> size e \<le> size (?x11 e s')
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e s'. \<lbrakk>e \<in> set es; clock s' \<le> clock s; \<not> Suc (clock s') \<le> clock s\<rbrakk> \<Longrightarrow> size e \<le> size e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>s' vs. evaluate_list True env s (rev es) (s', vs)

goal (11 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' vs. evaluate_list True env s (rev es) (s', vs)
[PROOF STEP]
obtain r s2 where es: "evaluate_list True env s (rev es) (s2, r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' vs. evaluate_list True env s (rev es) (s', vs)

goal (1 subgoal):
 1. (\<And>s2 r. evaluate_list True env s (rev es) (s2, r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate_list True env s (rev es) (s2, r)

goal (11 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_list True env s (rev es) (s2, r)
[PROOF STEP]
have clock: "clock s2 \<le> clock s"
[PROOF STATE]
proof (prove)
using this:
evaluate_list True env s (rev es) (s2, r)

goal (1 subgoal):
 1. clock s2 \<le> clock s
[PROOF STEP]
by (metis evaluate_clock_mono)
[PROOF STATE]
proof (state)
this:
clock s2 \<le> clock s

goal (11 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x71 x72. e = App x71 x72 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
A total of 11 subgoals...
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Rval vs)
[PROOF STATE]
proof (state)
this:
r = Rval vs

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases "op = Opapp")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. op = Opapp \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. op \<noteq> Opapp \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case opapp: True
[PROOF STATE]
proof (state)
this:
op = Opapp

goal (2 subgoals):
 1. op = Opapp \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. op \<noteq> Opapp \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases "do_opapp (rev vs)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. do_opapp (rev vs) = None \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>a. do_opapp (rev vs) = Some a \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
do_opapp (rev vs) = None

goal (2 subgoals):
 1. do_opapp (rev vs) = None \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>a. do_opapp (rev vs) = Some a \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with App opapp Rval es
[PROOF STATE]
proof (chain)
picking this:
e = App op es
op = Opapp
r = Rval vs
evaluate_list True env s (rev es) (s2, r)
do_opapp (rev vs) = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e = App op es
op = Opapp
r = Rval vs
evaluate_list True env s (rev es) (s2, r)
do_opapp (rev vs) = None

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
by (metis app3)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. \<And>a. do_opapp (rev vs) = Some a \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. do_opapp (rev vs) = Some a \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Some r)
[PROOF STATE]
proof (state)
this:
do_opapp (rev vs) = Some r

goal (1 subgoal):
 1. \<And>a. do_opapp (rev vs) = Some a \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
obtain env' e' where "r = (env', e')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>env' e'. r = (env', e') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis surj_pair)
[PROOF STATE]
proof (state)
this:
r = (env', e')

goal (1 subgoal):
 1. \<And>a. do_opapp (rev vs) = Some a \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases "clock s2 = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. clock s2 = 0 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. clock s2 \<noteq> 0 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
clock s2 = 0

goal (2 subgoals):
 1. clock s2 = 0 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. clock s2 \<noteq> 0 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding \<open>op = _\<close> App
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (App Opapp es) (s', r)
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s (App Opapp es) (?s', ?r1)
[PROOF STEP]
apply (rule app2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_list True env s (rev es) (?s', Rval ?vs2) \<and> do_opapp (rev ?vs2) = Some (?env'2, ?e2) \<and> clock ?s' = 0 \<and> True
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. evaluate_list True env s (rev es) (?s', Rval ?vs2)
 2. do_opapp (rev ?vs2) = Some (?env'2, ?e2)
 3. clock ?s' = 0
 4. True
[PROOF STEP]
using es
[PROOF STATE]
proof (prove)
using this:
evaluate_list True env s (rev es) (s2, r__)

goal (4 subgoals):
 1. evaluate_list True env s (rev es) (?s', Rval ?vs2)
 2. do_opapp (rev ?vs2) = Some (?env'2, ?e2)
 3. clock ?s' = 0
 4. True
[PROOF STEP]
unfolding Rval
[PROOF STATE]
proof (prove)
using this:
evaluate_list True env s (rev es) (s2, Rval vs)

goal (4 subgoals):
 1. evaluate_list True env s (rev es) (?s', Rval ?vs2)
 2. do_opapp (rev ?vs2) = Some (?env'2, ?e2)
 3. clock ?s' = 0
 4. True
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. do_opapp (rev vs) = Some (?env'2, ?e2)
 2. clock s2 = 0
 3. True
[PROOF STEP]
using Some
[PROOF STATE]
proof (prove)
using this:
do_opapp (rev vs) = Some r

goal (3 subgoals):
 1. do_opapp (rev vs) = Some (?env'2, ?e2)
 2. clock s2 = 0
 3. True
[PROOF STEP]
unfolding \<open>r = _\<close>
[PROOF STATE]
proof (prove)
using this:
do_opapp (rev vs) = Some (env', e')

goal (3 subgoals):
 1. do_opapp (rev vs) = Some (?env'2, ?e2)
 2. clock s2 = 0
 3. True
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. clock s2 = 0
 2. True
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. clock s2 \<noteq> 0 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. clock s2 \<noteq> 0 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
clock s2 \<noteq> 0

goal (1 subgoal):
 1. clock s2 \<noteq> 0 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
have "\<exists>s' r. evaluate True env' (s2 \<lparr> clock := clock s2 - Suc 0 \<rparr>) e' (s', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env' (update_clock (\<lambda>_. clock s2 - Suc 0) s2) e' (s', r)
[PROOF STEP]
apply (rule less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((clock (update_clock (\<lambda>_. clock s2 - Suc 0) s2), e'), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
using False clock
[PROOF STATE]
proof (prove)
using this:
clock s2 \<noteq> 0
clock s2 \<le> clock s

goal (1 subgoal):
 1. ((clock (update_clock (\<lambda>_. clock s2 - Suc 0) s2), e'), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
by (auto simp: datatype_record_update split: state.splits)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env' (update_clock (\<lambda>_. clock s2 - Suc 0) s2) e' (s', r)

goal (1 subgoal):
 1. clock s2 \<noteq> 0 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' r. evaluate True env' (update_clock (\<lambda>_. clock s2 - Suc 0) s2) e' (s', r)
[PROOF STEP]
obtain s' r' where "evaluate True env' (s2 \<lparr> clock := clock s2 - Suc 0 \<rparr>) e' (s', r')"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True env' (update_clock (\<lambda>_. clock s2 - Suc 0) s2) e' (s', r)

goal (1 subgoal):
 1. (\<And>s' r'. evaluate True env' (update_clock (\<lambda>_. clock s2 - Suc 0) s2) e' (s', r') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate True env' (update_clock (\<lambda>_. clock s2 - Suc 0) s2) e' (s', r')

goal (1 subgoal):
 1. clock s2 \<noteq> 0 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding \<open>op = _\<close> App
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (App Opapp es) (s', r)
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s (App Opapp es) (?s', ?r1)
[PROOF STEP]
apply (rule app1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_list True env s (rev es) (?s2.2, Rval ?vs2) \<and> do_opapp (rev ?vs2) = Some (?env'2, ?e2) \<and> (True \<longrightarrow> clock ?s2.2 \<noteq> 0) \<and> evaluate True ?env'2 (if True then update_clock (\<lambda>_. clock ?s2.2 - 1) ?s2.2 else ?s2.2) ?e2 (?s', ?r1)
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. evaluate_list True env s (rev es) (?s2.2, Rval ?vs2)
 2. do_opapp (rev ?vs2) = Some (?env'2, ?e2)
 3. True \<longrightarrow> clock ?s2.2 \<noteq> 0
 4. evaluate True ?env'2 (if True then update_clock (\<lambda>_. clock ?s2.2 - 1) ?s2.2 else ?s2.2) ?e2 (?s', ?r1)
[PROOF STEP]
using es
[PROOF STATE]
proof (prove)
using this:
evaluate_list True env s (rev es) (s2, r__)

goal (4 subgoals):
 1. evaluate_list True env s (rev es) (?s2.2, Rval ?vs2)
 2. do_opapp (rev ?vs2) = Some (?env'2, ?e2)
 3. True \<longrightarrow> clock ?s2.2 \<noteq> 0
 4. evaluate True ?env'2 (if True then update_clock (\<lambda>_. clock ?s2.2 - 1) ?s2.2 else ?s2.2) ?e2 (?s', ?r1)
[PROOF STEP]
unfolding Rval
[PROOF STATE]
proof (prove)
using this:
evaluate_list True env s (rev es) (s2, Rval vs)

goal (4 subgoals):
 1. evaluate_list True env s (rev es) (?s2.2, Rval ?vs2)
 2. do_opapp (rev ?vs2) = Some (?env'2, ?e2)
 3. True \<longrightarrow> clock ?s2.2 \<noteq> 0
 4. evaluate True ?env'2 (if True then update_clock (\<lambda>_. clock ?s2.2 - 1) ?s2.2 else ?s2.2) ?e2 (?s', ?r1)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. do_opapp (rev vs) = Some (?env'2, ?e2)
 2. True \<longrightarrow> clock s2 \<noteq> 0
 3. evaluate True ?env'2 (if True then update_clock (\<lambda>_. clock s2 - 1) s2 else s2) ?e2 (?s', ?r1)
[PROOF STEP]
using Some
[PROOF STATE]
proof (prove)
using this:
do_opapp (rev vs) = Some r

goal (3 subgoals):
 1. do_opapp (rev vs) = Some (?env'2, ?e2)
 2. True \<longrightarrow> clock s2 \<noteq> 0
 3. evaluate True ?env'2 (if True then update_clock (\<lambda>_. clock s2 - 1) s2 else s2) ?e2 (?s', ?r1)
[PROOF STEP]
unfolding \<open>r = _\<close>
[PROOF STATE]
proof (prove)
using this:
do_opapp (rev vs) = Some (env', e')

goal (3 subgoals):
 1. do_opapp (rev vs) = Some (?env'2, ?e2)
 2. True \<longrightarrow> clock s2 \<noteq> 0
 3. evaluate True ?env'2 (if True then update_clock (\<lambda>_. clock s2 - 1) s2 else s2) ?e2 (?s', ?r1)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. True \<longrightarrow> clock s2 \<noteq> 0
 2. evaluate True env' (if True then update_clock (\<lambda>_. clock s2 - 1) s2 else s2) e' (?s', ?r1)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
clock s2 \<noteq> 0

goal (2 subgoals):
 1. True \<longrightarrow> clock s2 \<noteq> 0
 2. evaluate True env' (if True then update_clock (\<lambda>_. clock s2 - 1) s2 else s2) e' (?s', ?r1)
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env' (if True then update_clock (\<lambda>_. clock s2 - 1) s2 else s2) e' (?s', ?r1)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env' (update_clock (\<lambda>_. clock s2 - Suc 0) s2) e' (?s', ?r1)
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. op \<noteq> Opapp \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op \<noteq> Opapp \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
op \<noteq> Opapp

goal (1 subgoal):
 1. op \<noteq> Opapp \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases "do_app ((refs   s2),(ffi   s2)) op (rev vs)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. do_app (refs s2, ffi s2) op (rev vs) = None \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>a. do_app (refs s2, ffi s2) op (rev vs) = Some a \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
do_app (refs s2, ffi s2) op (rev vs) = None

goal (2 subgoals):
 1. do_app (refs s2, ffi s2) op (rev vs) = None \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>a. do_app (refs s2, ffi s2) op (rev vs) = Some a \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding App
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (App op es) (s', r)
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s (App op es) (?s', ?r1)
[PROOF STEP]
apply (rule app5)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_list True env s (rev es) (?s', Rval ?vs2) \<and> do_app (refs ?s', ffi ?s') op (rev ?vs2) = None \<and> op \<noteq> Opapp
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. evaluate_list True env s (rev es) (?s', Rval ?vs2)
 2. do_app (refs ?s', ffi ?s') op (rev ?vs2) = None
 3. op \<noteq> Opapp
[PROOF STEP]
using es
[PROOF STATE]
proof (prove)
using this:
evaluate_list True env s (rev es) (s2, r)

goal (3 subgoals):
 1. evaluate_list True env s (rev es) (?s', Rval ?vs2)
 2. do_app (refs ?s', ffi ?s') op (rev ?vs2) = None
 3. op \<noteq> Opapp
[PROOF STEP]
unfolding Rval
[PROOF STATE]
proof (prove)
using this:
evaluate_list True env s (rev es) (s2, Rval vs)

goal (3 subgoals):
 1. evaluate_list True env s (rev es) (?s', Rval ?vs2)
 2. do_app (refs ?s', ffi ?s') op (rev ?vs2) = None
 3. op \<noteq> Opapp
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. do_app (refs s2, ffi s2) op (rev vs) = None
 2. op \<noteq> Opapp
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. \<And>a. do_app (refs s2, ffi s2) op (rev vs) = Some a \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. do_app (refs s2, ffi s2) op (rev vs) = Some a \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Some r)
[PROOF STATE]
proof (state)
this:
do_app (refs s2, ffi s2) op (rev vs) = Some r

goal (1 subgoal):
 1. \<And>a. do_app (refs s2, ffi s2) op (rev vs) = Some a \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
obtain refs' ffi' res where "r = ((refs', ffi'), res)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>refs' ffi' res. r = ((refs', ffi'), res) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis surj_pair)
[PROOF STATE]
proof (state)
this:
r = ((refs', ffi'), res)

goal (1 subgoal):
 1. \<And>a. do_app (refs s2, ffi s2) op (rev vs) = Some a \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding App
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (App op es) (s', r)
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s (App op es) (?s', ?r1)
[PROOF STEP]
apply (rule app4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_list True env s (rev es) (?s2.2, Rval ?vs2) \<and> do_app (refs ?s2.2, ffi ?s2.2) op (rev ?vs2) = Some ((?refs'2, ?ffi'2), ?r1) \<and> op \<noteq> Opapp
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. evaluate_list True env s (rev es) (?s2.2, Rval ?vs2)
 2. do_app (refs ?s2.2, ffi ?s2.2) op (rev ?vs2) = Some ((?refs'2, ?ffi'2), ?r1)
 3. op \<noteq> Opapp
[PROOF STEP]
using es
[PROOF STATE]
proof (prove)
using this:
evaluate_list True env s (rev es) (s2, r__)

goal (3 subgoals):
 1. evaluate_list True env s (rev es) (?s2.2, Rval ?vs2)
 2. do_app (refs ?s2.2, ffi ?s2.2) op (rev ?vs2) = Some ((?refs'2, ?ffi'2), ?r1)
 3. op \<noteq> Opapp
[PROOF STEP]
unfolding Rval
[PROOF STATE]
proof (prove)
using this:
evaluate_list True env s (rev es) (s2, Rval vs)

goal (3 subgoals):
 1. evaluate_list True env s (rev es) (?s2.2, Rval ?vs2)
 2. do_app (refs ?s2.2, ffi ?s2.2) op (rev ?vs2) = Some ((?refs'2, ?ffi'2), ?r1)
 3. op \<noteq> Opapp
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. do_app (refs s2, ffi s2) op (rev vs) = Some ((?refs'2, ?ffi'2), ?r1)
 2. op \<noteq> Opapp
[PROOF STEP]
using Some
[PROOF STATE]
proof (prove)
using this:
do_app (refs s2, ffi s2) op (rev vs) = Some r

goal (2 subgoals):
 1. do_app (refs s2, ffi s2) op (rev vs) = Some ((?refs'2, ?ffi'2), ?r1)
 2. op \<noteq> Opapp
[PROOF STEP]
unfolding \<open>r = _\<close>
[PROOF STATE]
proof (prove)
using this:
do_app (refs s2, ffi s2) op (rev vs) = Some ((refs', ffi'), res)

goal (2 subgoals):
 1. do_app (refs s2, ffi s2) op (rev vs) = Some ((?refs'2, ?ffi'2), ?r1)
 2. op \<noteq> Opapp
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op \<noteq> Opapp
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case Rerr
[PROOF STATE]
proof (state)
this:
r = Rerr x2_

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with es App
[PROOF STATE]
proof (chain)
picking this:
evaluate_list True env s (rev es) (s2, r)
e = App op es
r = Rerr x2_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate_list True env s (rev es) (s2, r)
e = App op es
r = Rerr x2_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
by (metis app6)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (10 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Log op e1 e2)
[PROOF STATE]
proof (state)
this:
e = Log op e1 e2

goal (10 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with less
[PROOF STATE]
proof (chain)
picking this:
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)
e = Log op e1 e2
[PROOF STEP]
have "\<exists>s' r. evaluate True env s e1 (s', r)"
[PROOF STATE]
proof (prove)
using this:
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)
e = Log op e1 e2

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e1 (s', r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e1 (s', r)

goal (10 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' r. evaluate True env s e1 (s', r)
[PROOF STEP]
obtain s' r where e1: "evaluate True env s e1 (s', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True env s e1 (s', r)

goal (1 subgoal):
 1. (\<And>s' r. evaluate True env s e1 (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
evaluate True env s e1 (s', r)

goal (10 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e1 (s', r)
[PROOF STEP]
have clock: "clock s' \<le> clock s"
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e1 (s', r)

goal (1 subgoal):
 1. clock s' \<le> clock s
[PROOF STEP]
by (metis evaluate_clock_mono)
[PROOF STATE]
proof (state)
this:
clock s' \<le> clock s

goal (10 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x81 x82 x83. e = Log x81 x82 x83 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 10. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Rval v)
[PROOF STATE]
proof (state)
this:
r = Rval v

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with e1 Log
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e1 (s', r)
e = Log op e1 e2
r = Rval v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e1 (s', r)
e = Log op e1 e2
r = Rval v

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases op v e2 rule: do_log_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = None\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>v'. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Val v')\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Exp e2)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case none
[PROOF STATE]
proof (state)
this:
do_log op v e2 = None

goal (3 subgoals):
 1. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = None\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>v'. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Val v')\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Exp e2)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
do_log op v e2 = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
do_log op v e2 = None

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Log
[PROOF STATE]
proof (prove)
using this:
do_log op v e2 = None

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Log op e1 e2) (s', r)
[PROOF STEP]
using e1 Rval
[PROOF STATE]
proof (prove)
using this:
do_log op v e2 = None
evaluate True env s e1 (s', r)
r = Rval v

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Log op e1 e2) (s', r)
[PROOF STEP]
by (metis log3)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (2 subgoals):
 1. \<And>v'. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Val v')\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Exp e2)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v'. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Val v')\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Exp e2)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case val
[PROOF STATE]
proof (state)
this:
do_log op v e2 = Some (Val v'_)

goal (2 subgoals):
 1. \<And>v'. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Val v')\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Exp e2)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
do_log op v e2 = Some (Val v'_)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
do_log op v e2 = Some (Val v'_)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Log
[PROOF STATE]
proof (prove)
using this:
do_log op v e2 = Some (Val v'_)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Log op e1 e2) (s', r)
[PROOF STEP]
using e1 Rval
[PROOF STATE]
proof (prove)
using this:
do_log op v e2 = Some (Val v'_)
evaluate True env s e1 (s', r)
r = Rval v

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Log op e1 e2) (s', r)
[PROOF STEP]
by (metis log2)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Exp e2)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Exp e2)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case exp
[PROOF STATE]
proof (state)
this:
do_log op v e2 = Some (Exp e2)

goal (1 subgoal):
 1. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Exp e2)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
have "\<exists>s'' r. evaluate True env s' e2 (s'', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s'' r. evaluate True env s' e2 (s'', r)
[PROOF STEP]
apply (rule less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((clock s', e2), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
using clock Log
[PROOF STATE]
proof (prove)
using this:
clock s' \<le> clock s
e = Log op e1 e2

goal (1 subgoal):
 1. ((clock s', e2), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s'' r. evaluate True env s' e2 (s'', r)

goal (1 subgoal):
 1. \<lbrakk>evaluate True env s e1 (s', r); e = Log op e1 e2; r = Rval v; do_log op v e2 = Some (Exp e2)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s'' r. evaluate True env s' e2 (s'', r)
[PROOF STEP]
obtain s'' r where "evaluate True env s' e2 (s'', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s'' r. evaluate True env s' e2 (s'', r)

goal (1 subgoal):
 1. (\<And>s'' r. evaluate True env s' e2 (s'', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate True env s' e2 (s'', r)

goal (1 subgoal):
 1. \<lbrakk>evaluate True env s e1 (s', r__); e = Log op e1 e2; r__ = Rval v; do_log op v e2 = Some (Exp e2)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Log
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Log op e1 e2) (s', r)
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s (Log op e1 e2) (?s', ?r1)
[PROOF STEP]
apply (rule log1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s e1 (?s2.2, Rval ?v1.2) \<and> do_log op ?v1.2 e2 = Some (Exp ?e'2) \<and> evaluate True env ?s2.2 ?e'2 (?s', ?r1)
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. evaluate True env s e1 (?s2.2, Rval ?v1.2)
 2. do_log op ?v1.2 e2 = Some (Exp ?e'2)
 3. evaluate True env ?s2.2 ?e'2 (?s', ?r1)
[PROOF STEP]
using Rval e1
[PROOF STATE]
proof (prove)
using this:
r__ = Rval v
evaluate True env s e1 (s', r__)

goal (3 subgoals):
 1. evaluate True env s e1 (?s2.2, Rval ?v1.2)
 2. do_log op ?v1.2 e2 = Some (Exp ?e'2)
 3. evaluate True env ?s2.2 ?e'2 (?s', ?r1)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. do_log op v e2 = Some (Exp ?e'2)
 2. evaluate True env s' ?e'2 (?s', ?r1)
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case Rerr
[PROOF STATE]
proof (state)
this:
r = Rerr x2_

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with e1
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e1 (s', r)
r = Rerr x2_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e1 (s', r)
r = Rerr x2_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Log
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e1 (s', r)
r = Rerr x2_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Log op e1 e2) (s', r)
[PROOF STEP]
by (metis log4)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (9 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (If e1 e2 e3)
[PROOF STATE]
proof (state)
this:
e = exp0.If e1 e2 e3

goal (9 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with less
[PROOF STATE]
proof (chain)
picking this:
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)
e = exp0.If e1 e2 e3
[PROOF STEP]
have "\<exists>s' r. evaluate True env s e1 (s', r)"
[PROOF STATE]
proof (prove)
using this:
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)
e = exp0.If e1 e2 e3

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e1 (s', r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e1 (s', r)

goal (9 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' r. evaluate True env s e1 (s', r)
[PROOF STEP]
obtain s' r where e1: "evaluate True env s e1 (s', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True env s e1 (s', r)

goal (1 subgoal):
 1. (\<And>s' r. evaluate True env s e1 (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate True env s e1 (s', r)

goal (9 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e1 (s', r)
[PROOF STEP]
have clock: "clock s' \<le> clock s"
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e1 (s', r)

goal (1 subgoal):
 1. clock s' \<le> clock s
[PROOF STEP]
by (metis evaluate_clock_mono)
[PROOF STATE]
proof (state)
this:
clock s' \<le> clock s

goal (9 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x91 x92 x93. e = exp0.If x91 x92 x93 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 9. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Rval v1)
[PROOF STATE]
proof (state)
this:
r = Rval v1

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases v1 e2 e3 rule: do_if_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. do_if v1 e2 e3 = None \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. do_if v1 e2 e3 = Some e2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. do_if v1 e2 e3 = Some e3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case none
[PROOF STATE]
proof (state)
this:
do_if v1 e2 e3 = None

goal (3 subgoals):
 1. do_if v1 e2 e3 = None \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. do_if v1 e2 e3 = Some e2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. do_if v1 e2 e3 = Some e3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding If
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (exp0.If e1 e2 e3) (s', r)
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s (exp0.If e1 e2 e3) (?s', ?r1)
[PROOF STEP]
apply (rule if2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s e1 (?s', Rval ?v1.2) \<and> do_if ?v1.2 e2 e3 = None
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. evaluate True env s e1 (?s', Rval ?v1.2)
 2. do_if ?v1.2 e2 e3 = None
[PROOF STEP]
using Rval e1
[PROOF STATE]
proof (prove)
using this:
r = Rval v1
evaluate True env s e1 (s', r)

goal (2 subgoals):
 1. evaluate True env s e1 (?s', Rval ?v1.2)
 2. do_if ?v1.2 e2 e3 = None
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. do_if v1 e2 e3 = None
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (2 subgoals):
 1. do_if v1 e2 e3 = Some e2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. do_if v1 e2 e3 = Some e3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. do_if v1 e2 e3 = Some e2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. do_if v1 e2 e3 = Some e3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case true
[PROOF STATE]
proof (state)
this:
do_if v1 e2 e3 = Some e2

goal (2 subgoals):
 1. do_if v1 e2 e3 = Some e2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. do_if v1 e2 e3 = Some e3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
have "\<exists>s'' r. evaluate True env s' e2 (s'', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s'' r. evaluate True env s' e2 (s'', r)
[PROOF STEP]
apply (rule less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((clock s', e2), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
using clock If
[PROOF STATE]
proof (prove)
using this:
clock s' \<le> clock s
e = exp0.If e1 e2 e3

goal (1 subgoal):
 1. ((clock s', e2), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s'' r. evaluate True env s' e2 (s'', r)

goal (2 subgoals):
 1. do_if v1 e2 e3 = Some e2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. do_if v1 e2 e3 = Some e3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s'' r. evaluate True env s' e2 (s'', r)
[PROOF STEP]
obtain s'' r where "evaluate True env s' e2 (s'', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s'' r. evaluate True env s' e2 (s'', r)

goal (1 subgoal):
 1. (\<And>s'' r. evaluate True env s' e2 (s'', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate True env s' e2 (s'', r)

goal (2 subgoals):
 1. do_if v1 e2 e3 = Some e2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. do_if v1 e2 e3 = Some e3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding If
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (exp0.If e1 e2 e3) (s', r)
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s (exp0.If e1 e2 e3) (?s', ?r1)
[PROOF STEP]
apply (rule if1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s e1 (?s2.2, Rval ?v1.2) \<and> do_if ?v1.2 e2 e3 = Some ?e'2 \<and> evaluate True env ?s2.2 ?e'2 (?s', ?r1)
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. evaluate True env s e1 (?s2.2, Rval ?v1.2)
 2. do_if ?v1.2 e2 e3 = Some ?e'2
 3. evaluate True env ?s2.2 ?e'2 (?s', ?r1)
[PROOF STEP]
using Rval e1
[PROOF STATE]
proof (prove)
using this:
r__ = Rval v1
evaluate True env s e1 (s', r__)

goal (3 subgoals):
 1. evaluate True env s e1 (?s2.2, Rval ?v1.2)
 2. do_if ?v1.2 e2 e3 = Some ?e'2
 3. evaluate True env ?s2.2 ?e'2 (?s', ?r1)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. do_if v1 e2 e3 = Some ?e'2
 2. evaluate True env s' ?e'2 (?s', ?r1)
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. do_if v1 e2 e3 = Some e3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. do_if v1 e2 e3 = Some e3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case false
[PROOF STATE]
proof (state)
this:
do_if v1 e2 e3 = Some e3

goal (1 subgoal):
 1. do_if v1 e2 e3 = Some e3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
have "\<exists>s'' r. evaluate True env s' e3 (s'', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s'' r. evaluate True env s' e3 (s'', r)
[PROOF STEP]
apply (rule less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((clock s', e3), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
using clock If
[PROOF STATE]
proof (prove)
using this:
clock s' \<le> clock s
e = exp0.If e1 e2 e3

goal (1 subgoal):
 1. ((clock s', e3), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s'' r. evaluate True env s' e3 (s'', r)

goal (1 subgoal):
 1. do_if v1 e2 e3 = Some e3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s'' r. evaluate True env s' e3 (s'', r)
[PROOF STEP]
obtain s'' r where "evaluate True env s' e3 (s'', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s'' r. evaluate True env s' e3 (s'', r)

goal (1 subgoal):
 1. (\<And>s'' r. evaluate True env s' e3 (s'', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate True env s' e3 (s'', r)

goal (1 subgoal):
 1. do_if v1 e2 e3 = Some e3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding If
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (exp0.If e1 e2 e3) (s', r)
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s (exp0.If e1 e2 e3) (?s', ?r1)
[PROOF STEP]
apply (rule if1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s e1 (?s2.2, Rval ?v1.2) \<and> do_if ?v1.2 e2 e3 = Some ?e'2 \<and> evaluate True env ?s2.2 ?e'2 (?s', ?r1)
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. evaluate True env s e1 (?s2.2, Rval ?v1.2)
 2. do_if ?v1.2 e2 e3 = Some ?e'2
 3. evaluate True env ?s2.2 ?e'2 (?s', ?r1)
[PROOF STEP]
using Rval e1
[PROOF STATE]
proof (prove)
using this:
r__ = Rval v1
evaluate True env s e1 (s', r__)

goal (3 subgoals):
 1. evaluate True env s e1 (?s2.2, Rval ?v1.2)
 2. do_if ?v1.2 e2 e3 = Some ?e'2
 3. evaluate True env ?s2.2 ?e'2 (?s', ?r1)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. do_if v1 e2 e3 = Some ?e'2
 2. evaluate True env s' ?e'2 (?s', ?r1)
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case Rerr
[PROOF STATE]
proof (state)
this:
r = Rerr x2_

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with e1
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e1 (s', r)
r = Rerr x2_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e1 (s', r)
r = Rerr x2_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding If
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e1 (s', r)
r = Rerr x2_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (exp0.If e1 e2 e3) (s', r)
[PROOF STEP]
by (metis if3)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (8 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Handle e' pes)
[PROOF STATE]
proof (state)
this:
e = Handle e' pes

goal (8 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with less
[PROOF STATE]
proof (chain)
picking this:
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)
e = Handle e' pes
[PROOF STEP]
have "\<exists>s' r. evaluate True env s e' (s', r)"
[PROOF STATE]
proof (prove)
using this:
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)
e = Handle e' pes

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e' (s', r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e' (s', r)

goal (8 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' r. evaluate True env s e' (s', r)
[PROOF STEP]
obtain s' r where e': "evaluate True env s e' (s', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True env s e' (s', r)

goal (1 subgoal):
 1. (\<And>s' r. evaluate True env s e' (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate True env s e' (s', r)

goal (8 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e' (s', r)
[PROOF STEP]
have clock: "clock s' \<le> clock s"
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', r)

goal (1 subgoal):
 1. clock s' \<le> clock s
[PROOF STEP]
by (metis evaluate_clock_mono)
[PROOF STATE]
proof (state)
this:
clock s' \<le> clock s

goal (8 subgoals):
 1. \<And>x21 x22. e = Handle x21 x22 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 8. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case Rval
[PROOF STATE]
proof (state)
this:
r = Rval x1_

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with e'
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e' (s', r)
r = Rval x1_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', r)
r = Rval x1_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Handle
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', r)
r = Rval x1_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Handle e' pes) (s', r)
[PROOF STEP]
by (metis handle1)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Rerr err)
[PROOF STATE]
proof (state)
this:
r = Rerr err

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases err)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. err = Rraise x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. err = Rabort x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Rraise exn)
[PROOF STATE]
proof (state)
this:
err = Rraise exn

goal (2 subgoals):
 1. \<And>x1. err = Rraise x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. err = Rabort x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
have "\<exists>s'' r. evaluate_match True env s' exn pes exn (s'', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s'' r. evaluate_match True env s' exn pes exn (s'', r)
[PROOF STEP]
apply (rule evaluate_match_total0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p e env s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'\<rbrakk> \<Longrightarrow> \<exists>s''a r. evaluate True env s'' e (s''a, r)
[PROOF STEP]
apply (rule less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p e env s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'\<rbrakk> \<Longrightarrow> ((clock s'', e), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
using Handle clock
[PROOF STATE]
proof (prove)
using this:
e = Handle e' pes
clock s' \<le> clock s

goal (1 subgoal):
 1. \<And>p e env s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'\<rbrakk> \<Longrightarrow> ((clock s'', e), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
apply (auto simp: less_eq_Suc_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p e s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'; e = Handle e' pes; clock s' \<le> clock s; \<not> Suc (clock s'') \<le> clock s\<rbrakk> \<Longrightarrow> size e \<le> size_list (size_prod (\<lambda>x. 0) size) pes + size e'
[PROOF STEP]
apply (rule trans_le_add1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p e s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'; e = Handle e' pes; clock s' \<le> clock s; \<not> Suc (clock s'') \<le> clock s\<rbrakk> \<Longrightarrow> size e \<le> size_list (size_prod (\<lambda>x. 0) size) pes
[PROOF STEP]
apply (rule size_list_estimation')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p e s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'; e = Handle e' pes; clock s' \<le> clock s; \<not> Suc (clock s'') \<le> clock s\<rbrakk> \<Longrightarrow> ?x13 p e s'' \<in> set pes
 2. \<And>p e s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'; e = Handle e' pes; clock s' \<le> clock s; \<not> Suc (clock s'') \<le> clock s\<rbrakk> \<Longrightarrow> size e \<le> size_prod (\<lambda>x. 0) size (?x13 p e s'')
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p e s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'; e = Handle e' pes; clock s' \<le> clock s; \<not> Suc (clock s'') \<le> clock s\<rbrakk> \<Longrightarrow> size e \<le> size_prod (\<lambda>x. 0) size (p, e)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s'' r. evaluate_match True env s' exn pes exn (s'', r)

goal (2 subgoals):
 1. \<And>x1. err = Rraise x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. err = Rabort x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s'' r. evaluate_match True env s' exn pes exn (s'', r)
[PROOF STEP]
obtain s'' r where "evaluate_match True env s' exn pes exn (s'', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s'' r. evaluate_match True env s' exn pes exn (s'', r)

goal (1 subgoal):
 1. (\<And>s'' r. evaluate_match True env s' exn pes exn (s'', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate_match True env s' exn pes exn (s'', r)

goal (2 subgoals):
 1. \<And>x1. err = Rraise x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. err = Rabort x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Handle
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Handle e' pes) (s', r)
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s (Handle e' pes) (?s', ?r1)
[PROOF STEP]
apply (rule handle2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s e' (?s2.2, Rerr (Rraise ?v1.2)) \<and> evaluate_match True env ?s2.2 ?v1.2 pes ?v1.2 (?s', ?r1)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. evaluate True env s e' (?s2.2, Rerr (Rraise ?v1.2))
 2. evaluate_match True env ?s2.2 ?v1.2 pes ?v1.2 (?s', ?r1)
[PROOF STEP]
using e'
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', r__)

goal (2 subgoals):
 1. evaluate True env s e' (?s2.2, Rerr (Rraise ?v1.2))
 2. evaluate_match True env ?s2.2 ?v1.2 pes ?v1.2 (?s', ?r1)
[PROOF STEP]
unfolding Rerr Rraise
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', Rerr (Rraise exn))

goal (2 subgoals):
 1. evaluate True env s e' (?s2.2, Rerr (Rraise ?v1.2))
 2. evaluate_match True env ?s2.2 ?v1.2 pes ?v1.2 (?s', ?r1)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_match True env s' exn pes exn (?s', ?r1)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. \<And>x2. err = Rabort x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. err = Rabort x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Rabort x2)
[PROOF STATE]
proof (state)
this:
err = Rabort x2

goal (1 subgoal):
 1. \<And>x2. err = Rabort x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with e' Rerr
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e' (s', r)
r = Rerr err
err = Rabort x2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', r)
r = Rerr err
err = Rabort x2

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Handle
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', r)
r = Rerr err
err = Rabort x2

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Handle e' pes) (s', r)
[PROOF STEP]
by (metis handle3)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (7 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Mat e' pes)
[PROOF STATE]
proof (state)
this:
e = Mat e' pes

goal (7 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with less
[PROOF STATE]
proof (chain)
picking this:
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)
e = Mat e' pes
[PROOF STEP]
have "\<exists>s' r. evaluate True env s e' (s', r)"
[PROOF STATE]
proof (prove)
using this:
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)
e = Mat e' pes

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e' (s', r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e' (s', r)

goal (7 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' r. evaluate True env s e' (s', r)
[PROOF STEP]
obtain s' r where e': "evaluate True env s e' (s', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True env s e' (s', r)

goal (1 subgoal):
 1. (\<And>s' r. evaluate True env s e' (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate True env s e' (s', r)

goal (7 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e' (s', r)
[PROOF STEP]
have clock: "clock s' \<le> clock s"
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', r)

goal (1 subgoal):
 1. clock s' \<le> clock s
[PROOF STEP]
by (metis evaluate_clock_mono)
[PROOF STATE]
proof (state)
this:
clock s' \<le> clock s

goal (7 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x101 x102. e = Mat x101 x102 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 7. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Rval v)
[PROOF STATE]
proof (state)
this:
r = Rval v

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
have "\<exists>s'' r. evaluate_match True env s' v pes (Conv (Some (''Bind'', TypeExn (Short ''Bind''))) []) (s'', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s'' r. evaluate_match True env s' v pes (Conv (Some (''Bind'', TypeExn (Short ''Bind''))) []) (s'', r)
[PROOF STEP]
apply (rule evaluate_match_total0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p e env s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'\<rbrakk> \<Longrightarrow> \<exists>s''a r. evaluate True env s'' e (s''a, r)
[PROOF STEP]
apply (rule less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p e env s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'\<rbrakk> \<Longrightarrow> ((clock s'', e), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
unfolding Mat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p e env s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'\<rbrakk> \<Longrightarrow> ((clock s'', e), clock s, Mat e' pes) \<in> less_than <*lex*> measure size
[PROOF STEP]
using clock
[PROOF STATE]
proof (prove)
using this:
clock s' \<le> clock s

goal (1 subgoal):
 1. \<And>p e env s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'\<rbrakk> \<Longrightarrow> ((clock s'', e), clock s, Mat e' pes) \<in> less_than <*lex*> measure size
[PROOF STEP]
apply (auto simp: less_eq_Suc_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p e s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'; clock s' \<le> clock s; \<not> Suc (clock s'') \<le> clock s\<rbrakk> \<Longrightarrow> size e \<le> size_list (size_prod (\<lambda>x. 0) size) pes + size e'
[PROOF STEP]
apply (rule trans_le_add1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p e s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'; clock s' \<le> clock s; \<not> Suc (clock s'') \<le> clock s\<rbrakk> \<Longrightarrow> size e \<le> size_list (size_prod (\<lambda>x. 0) size) pes
[PROOF STEP]
apply (rule size_list_estimation')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p e s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'; clock s' \<le> clock s; \<not> Suc (clock s'') \<le> clock s\<rbrakk> \<Longrightarrow> ?x13 p e s'' \<in> set pes
 2. \<And>p e s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'; clock s' \<le> clock s; \<not> Suc (clock s'') \<le> clock s\<rbrakk> \<Longrightarrow> size e \<le> size_prod (\<lambda>x. 0) size (?x13 p e s'')
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p e s''. \<lbrakk>(p, e) \<in> set pes; clock s'' \<le> clock s'; clock s' \<le> clock s; \<not> Suc (clock s'') \<le> clock s\<rbrakk> \<Longrightarrow> size e \<le> size_prod (\<lambda>x. 0) size (p, e)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s'' r. evaluate_match True env s' v pes (Conv (Some (''Bind'', TypeExn (Short ''Bind''))) []) (s'', r)

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s'' r. evaluate_match True env s' v pes (Conv (Some (''Bind'', TypeExn (Short ''Bind''))) []) (s'', r)
[PROOF STEP]
obtain s'' r where "evaluate_match True env s' v pes (Conv (Some (''Bind'', TypeExn (Short ''Bind''))) []) (s'', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s'' r. evaluate_match True env s' v pes (Conv (Some (''Bind'', TypeExn (Short ''Bind''))) []) (s'', r)

goal (1 subgoal):
 1. (\<And>s'' r. evaluate_match True env s' v pes (Conv (Some (''Bind'', TypeExn (Short ''Bind''))) []) (s'', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate_match True env s' v pes (Conv (Some (''Bind'', TypeExn (Short ''Bind''))) []) (s'', r)

goal (2 subgoals):
 1. \<And>x1. r__ = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r__ = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Mat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Mat e' pes) (s', r)
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s (Mat e' pes) (?s', ?r1)
[PROOF STEP]
apply (rule mat1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env s e' (?s2.2, Rval ?v1.2) \<and> evaluate_match True env ?s2.2 ?v1.2 pes (Conv (Some (''Bind'', TypeExn (Short ''Bind''))) []) (?s', ?r1)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. evaluate True env s e' (?s2.2, Rval ?v1.2)
 2. evaluate_match True env ?s2.2 ?v1.2 pes (Conv (Some (''Bind'', TypeExn (Short ''Bind''))) []) (?s', ?r1)
[PROOF STEP]
using e'
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', r__)

goal (2 subgoals):
 1. evaluate True env s e' (?s2.2, Rval ?v1.2)
 2. evaluate_match True env ?s2.2 ?v1.2 pes (Conv (Some (''Bind'', TypeExn (Short ''Bind''))) []) (?s', ?r1)
[PROOF STEP]
unfolding Rval
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', Rval v)

goal (2 subgoals):
 1. evaluate True env s e' (?s2.2, Rval ?v1.2)
 2. evaluate_match True env ?s2.2 ?v1.2 pes (Conv (Some (''Bind'', TypeExn (Short ''Bind''))) []) (?s', ?r1)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_match True env s' v pes (Conv (Some (''Bind'', TypeExn (Short ''Bind''))) []) (?s', ?r1)
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. \<And>x2. r__ = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case Rerr
[PROOF STATE]
proof (state)
this:
r = Rerr x2_

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with e'
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e' (s', r)
r = Rerr x2_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', r)
r = Rerr x2_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Mat
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e' (s', r)
r = Rerr x2_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Mat e' pes) (s', r)
[PROOF STEP]
by (metis mat2)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (6 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Let n e1 e2)
[PROOF STATE]
proof (state)
this:
e = exp0.Let n e1 e2

goal (6 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = exp0.Let n e1 e2
[PROOF STEP]
have "\<exists>s' r. evaluate True env s e1 (s', r)"
[PROOF STATE]
proof (prove)
using this:
e = exp0.Let n e1 e2

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e1 (s', r)
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
e = exp0.Let n e1 e2
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e1 (s', r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e1 (s', r)

goal (6 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' r. evaluate True env s e1 (s', r)
[PROOF STEP]
obtain s' r where e1: "evaluate True env s e1 (s', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True env s e1 (s', r)

goal (1 subgoal):
 1. (\<And>s' r. evaluate True env s e1 (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate True env s e1 (s', r)

goal (6 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e1 (s', r)
[PROOF STEP]
have clock: "clock s' \<le> clock s"
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e1 (s', r)

goal (1 subgoal):
 1. clock s' \<le> clock s
[PROOF STEP]
by (metis evaluate_clock_mono)
[PROOF STATE]
proof (state)
this:
clock s' \<le> clock s

goal (6 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x111 x112 x113. e = exp0.Let x111 x112 x113 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 6. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Rval v)
[PROOF STATE]
proof (state)
this:
r = Rval v

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
have "\<exists>s'' r. evaluate True (env \<lparr> sem_env.v := nsOptBind n v (sem_env.v env) \<rparr>) s' e2 (s'', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s'' r. evaluate True (update_v (\<lambda>_. nsOptBind n v (sem_env.v env)) env) s' e2 (s'', r)
[PROOF STEP]
apply (rule less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((clock s', e2), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
using Let clock
[PROOF STATE]
proof (prove)
using this:
e = exp0.Let n e1 e2
clock s' \<le> clock s

goal (1 subgoal):
 1. ((clock s', e2), clock s, e) \<in> less_than <*lex*> measure size
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s'' r. evaluate True (update_v (\<lambda>_. nsOptBind n v (sem_env.v env)) env) s' e2 (s'', r)

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s'' r. evaluate True (update_v (\<lambda>_. nsOptBind n v (sem_env.v env)) env) s' e2 (s'', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s'' r. evaluate True (update_v (\<lambda>_. nsOptBind n v (sem_env.v env)) env) s' e2 (s'', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Let
[PROOF STATE]
proof (prove)
using this:
\<exists>s'' r. evaluate True (update_v (\<lambda>_. nsOptBind n v (sem_env.v env)) env) s' e2 (s'', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (exp0.Let n e1 e2) (s', r)
[PROOF STEP]
using e1 Rval
[PROOF STATE]
proof (prove)
using this:
\<exists>s'' r. evaluate True (update_v (\<lambda>_. nsOptBind n v (sem_env.v env)) env) s' e2 (s'', r)
evaluate True env s e1 (s', r)
r = Rval v

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (exp0.Let n e1 e2) (s', r)
[PROOF STEP]
by (metis let1)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case Rerr
[PROOF STATE]
proof (state)
this:
r = Rerr x2_

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with e1
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e1 (s', r)
r = Rerr x2_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e1 (s', r)
r = Rerr x2_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Let
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e1 (s', r)
r = Rerr x2_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (exp0.Let n e1 e2) (s', r)
[PROOF STEP]
by (metis let2)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (5 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Letrec funs e')
[PROOF STATE]
proof (state)
this:
e = Letrec funs e'

goal (5 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = Letrec funs e'
[PROOF STEP]
have "\<exists>s' r. evaluate True (env \<lparr> sem_env.v := build_rec_env funs env (sem_env.v env) \<rparr>) s e' (s', r)"
[PROOF STATE]
proof (prove)
using this:
e = Letrec funs e'

goal (1 subgoal):
 1. \<exists>s' r. evaluate True (update_v (\<lambda>_. build_rec_env funs env (sem_env.v env)) env) s e' (s', r)
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
e = Letrec funs e'
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True (update_v (\<lambda>_. build_rec_env funs env (sem_env.v env)) env) s e' (s', r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True (update_v (\<lambda>_. build_rec_env funs env (sem_env.v env)) env) s e' (s', r)

goal (5 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x121 x122. e = Letrec x121 x122 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 5. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' r. evaluate True (update_v (\<lambda>_. build_rec_env funs env (sem_env.v env)) env) s e' (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True (update_v (\<lambda>_. build_rec_env funs env (sem_env.v env)) env) s e' (s', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding Letrec
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True (update_v (\<lambda>_. build_rec_env funs env (sem_env.v env)) env) s e' (s', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Letrec funs e') (s', r)
[PROOF STEP]
by (cases "allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs)")
               (metis letrec1 letrec2)+
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (4 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Tannot e')
[PROOF STATE]
proof (state)
this:
e = Tannot e' x132_

goal (4 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with less
[PROOF STATE]
proof (chain)
picking this:
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)
e = Tannot e' x132_
[PROOF STEP]
have "\<exists>s' r. evaluate True env s e' (s', r)"
[PROOF STATE]
proof (prove)
using this:
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)
e = Tannot e' x132_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e' (s', r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e' (s', r)

goal (4 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x131 x132. e = Tannot x131 x132 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 4. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' r. evaluate True env s e' (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True env s e' (s', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding \<open>e = _\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True env s e' (s', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Tannot e' x132_) (s', r)
[PROOF STEP]
by (fastforce intro: evaluate_match_evaluate_list_evaluate.intros)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (3 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
case (Lannot e')
[PROOF STATE]
proof (state)
this:
e = Lannot e' x142_

goal (3 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
with less
[PROOF STATE]
proof (chain)
picking this:
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)
e = Lannot e' x142_
[PROOF STEP]
have "\<exists>s' r. evaluate True env s e' (s', r)"
[PROOF STATE]
proof (prove)
using this:
((clock ?s, ?e), clock s, e) \<in> less_than <*lex*> measure size \<Longrightarrow> \<exists>s' r. evaluate True ?env ?s ?e (s', r)
e = Lannot e' x142_

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e' (s', r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e' (s', r)

goal (3 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 3. \<And>x141 x142. e = Lannot x141 x142 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' r. evaluate True env s e' (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True env s e' (s', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
unfolding \<open>e = _\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True env s e' (s', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate True env s (Lannot e' x142_) (s', r)
[PROOF STEP]
by (fastforce intro: evaluate_match_evaluate_list_evaluate.intros)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal (2 subgoals):
 1. \<And>x3. e = Lit x3 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
 2. \<And>x61 x62. e = Fun x61 x62 \<Longrightarrow> \<exists>s' r. evaluate True env s e (s', r)
[PROOF STEP]
qed (fastforce intro: evaluate_match_evaluate_list_evaluate.intros)+
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True env s e (s', r)

goal:
No subgoals!
[PROOF STEP]
qed