[STATEMENT]
lemma clocked_min_counter:
  assumes "evaluate True env s e (s',r')"
  shows "evaluate True env (s (| clock := (clock   s) - (clock   s') |)) e ((s' (| clock := 0 |)),r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate True env (update_clock (\<lambda>_. clock s - clock s') s) e (update_clock (\<lambda>_. 0) s', r')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. evaluate True env (update_clock (\<lambda>_. clock s - clock s') s) e (update_clock (\<lambda>_. 0) s', r')
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e (s', r')
[PROOF STEP]
have "(clock   s) \<ge> (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 (fastforce intro:clock_monotone(3)[rule_format])
[PROOF STATE]
proof (state)
this:
clock s' \<le> clock s

goal (1 subgoal):
 1. evaluate True env (update_clock (\<lambda>_. clock s - clock s') s) e (update_clock (\<lambda>_. 0) s', r')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
clock s' \<le> clock s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
clock s' \<le> clock s

goal (1 subgoal):
 1. evaluate True env (update_clock (\<lambda>_. clock s - clock s') s) e (update_clock (\<lambda>_. 0) s', r')
[PROOF STEP]
thm sub_from_counter(3)[rule_format]
[PROOF STATE]
proof (prove)
using this:
clock s' \<le> clock s

goal (1 subgoal):
 1. evaluate True env (update_clock (\<lambda>_. clock s - clock s') s) e (update_clock (\<lambda>_. 0) s', r')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
clock s' \<le> clock s
evaluate True env s e (s', r')

goal (1 subgoal):
 1. evaluate True env (update_clock (\<lambda>_. clock s - clock s') s) e (update_clock (\<lambda>_. 0) s', r')
[PROOF STEP]
by (auto intro!:sub_from_counter(3)[rule_format])
[PROOF STATE]
proof (state)
this:
evaluate True env (update_clock (\<lambda>_. clock s - clock s') s) e (update_clock (\<lambda>_. 0) s', r')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dec_evaluate_not_timeout:
  "evaluate_dec False mn env s d (s',r) \<Longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_dec False mn env s d (s', r) \<Longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
by (ind_cases "evaluate_dec False mn env s d (s', r)", auto dest: big_unclocked_notimeout)


[STATEMENT]
lemma dec_unclocked_ignore:
  "evaluate_dec ck mn env s d res \<Longrightarrow>
   \<forall>s' r count. res = (s',r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow>
    evaluate_dec False mn env (s (| clock := count |)) d (s' (| clock := count |),r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_dec ck mn env s d res \<Longrightarrow> \<forall>s' r count. res = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) d (update_clock (\<lambda>_. count) s', r)
[PROOF STEP]
proof (induction rule:evaluate_dec.inducts)
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env' \<Longrightarrow> \<forall>s' r count. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 2. \<And>ck mn env p e v1 s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = No_match \<Longrightarrow> \<forall>s' r count. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 3. \<And>ck mn env p e v1 s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match_type_error \<Longrightarrow> \<forall>s' r count. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 5. \<And>ck mn env p e err s s' locs. evaluate ck env s e (s', Rerr err) \<and> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s'a r count. (s', Rerr err) = (s'a, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dlet locs p e) (update_clock (\<lambda>_. count) s'a, r)
 6. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r count. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dletrec locs funs) (update_clock (\<lambda>_. count) s', r)
 7. \<And>ck mn env funs s locs. \<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dletrec locs funs) (update_clock (\<lambda>_. count) s', r)
 8. \<And>ck mn env tds s new_tdecs locs. check_dup_ctors tds \<and> new_tdecs = type_defs_to_new_tdecs mn tds \<and> disjnt new_tdecs (defined_types s) \<and> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds) \<Longrightarrow> \<forall>s' r count. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtype locs tds) (update_clock (\<lambda>_. count) s', r)
 9. \<And>ck mn env tds s locs. \<not> check_dup_ctors tds \<or> \<not> disjnt (type_defs_to_new_tdecs mn tds) (defined_types s) \<or> \<not> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtype locs tds) (update_clock (\<lambda>_. count) s', r)
 10. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r count. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. count) s', r)
A total of 12 subgoals...
[PROOF STEP]
case dtype1
[PROOF STATE]
proof (state)
this:
check_dup_ctors tds_ \<and> new_tdecs_ = type_defs_to_new_tdecs mn_ tds_ \<and> disjnt new_tdecs_ (defined_types s_) \<and> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds_)

goal (12 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env' \<Longrightarrow> \<forall>s' r count. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 2. \<And>ck mn env p e v1 s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = No_match \<Longrightarrow> \<forall>s' r count. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 3. \<And>ck mn env p e v1 s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match_type_error \<Longrightarrow> \<forall>s' r count. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 5. \<And>ck mn env p e err s s' locs. evaluate ck env s e (s', Rerr err) \<and> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s'a r count. (s', Rerr err) = (s'a, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dlet locs p e) (update_clock (\<lambda>_. count) s'a, r)
 6. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r count. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dletrec locs funs) (update_clock (\<lambda>_. count) s', r)
 7. \<And>ck mn env funs s locs. \<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dletrec locs funs) (update_clock (\<lambda>_. count) s', r)
 8. \<And>ck mn env tds s new_tdecs locs. check_dup_ctors tds \<and> new_tdecs = type_defs_to_new_tdecs mn tds \<and> disjnt new_tdecs (defined_types s) \<and> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds) \<Longrightarrow> \<forall>s' r count. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtype locs tds) (update_clock (\<lambda>_. count) s', r)
 9. \<And>ck mn env tds s locs. \<not> check_dup_ctors tds \<or> \<not> disjnt (type_defs_to_new_tdecs mn tds) (defined_types s) \<or> \<not> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtype locs tds) (update_clock (\<lambda>_. count) s', r)
 10. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r count. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. count) s', r)
A total of 12 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
check_dup_ctors tds_ \<and> new_tdecs_ = type_defs_to_new_tdecs mn_ tds_ \<and> disjnt new_tdecs_ (defined_types s_) \<and> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
check_dup_ctors tds_ \<and> new_tdecs_ = type_defs_to_new_tdecs mn_ tds_ \<and> disjnt new_tdecs_ (defined_types s_) \<and> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds_)

goal (1 subgoal):
 1. \<forall>s' r count. (update_defined_types (\<lambda>_. new_tdecs_ \<union> defined_types s_) s_, Rval (make_sem_env nsEmpty (build_tdefs mn_ tds_))) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn_ env_ (update_clock (\<lambda>_. count) s_) (Dtype locs_ tds_) (update_clock (\<lambda>_. count) s', r)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>count. \<lbrakk>check_dup_ctors tds_; new_tdecs_ = type_defs_to_new_tdecs mn_ tds_; disjnt (type_defs_to_new_tdecs mn_ tds_) (defined_types s_); allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds_)\<rbrakk> \<Longrightarrow> evaluate_dec False mn_ env_ (update_clock (\<lambda>_. count) s_) (Dtype locs_ tds_) (update_defined_types (\<lambda>_. type_defs_to_new_tdecs mn_ tds_ \<union> defined_types s_) (update_clock (\<lambda>_. count) s_), Rval (make_sem_env nsEmpty (build_tdefs mn_ tds_)))
[PROOF STEP]
using evaluate_dec.intros state.record_simps(4)
[PROOF STATE]
proof (prove)
using this:
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = Match ?env' \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rval (make_sem_env (alist_to_ns ?env') nsEmpty))
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = No_match \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rerr (Rraise Bindv))
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = Match_type_error \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rerr (Rabort Rtype_error))
\<not> allDistinct (pat_bindings ?p []) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dlet ?locs ?p ?e) (?s, Rerr (Rabort Rtype_error))
evaluate ?ck ?env ?s ?e (?s', Rerr ?err) \<and> allDistinct (pat_bindings ?p []) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dlet ?locs ?p ?e) (?s', Rerr ?err)
allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) ?funs) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dletrec ?locs ?funs) (?s, Rval (make_sem_env (build_rec_env ?funs ?env nsEmpty) nsEmpty))
\<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) ?funs) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dletrec ?locs ?funs) (?s, Rerr (Rabort Rtype_error))
check_dup_ctors ?tds \<and> ?new_tdecs = type_defs_to_new_tdecs ?mn ?tds \<and> disjnt ?new_tdecs (defined_types ?s) \<and> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) ?tds) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dtype ?locs ?tds) (update_defined_types (\<lambda>_. ?new_tdecs \<union> defined_types ?s) ?s, Rval (make_sem_env nsEmpty (build_tdefs ?mn ?tds)))
\<not> check_dup_ctors ?tds \<or> \<not> disjnt (type_defs_to_new_tdecs ?mn ?tds) (defined_types ?s) \<or> \<not> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) ?tds) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dtype ?locs ?tds) (?s, Rerr (Rabort Rtype_error))
evaluate_dec ?ck ?mn ?env ?s (Dtabbrev ?locs ?tvs ?tn ?t0.0) (?s, Rval (make_sem_env nsEmpty nsEmpty))
TypeExn (mk_id ?mn ?cn) \<notin> defined_types ?s \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dexn ?locs ?cn ?ts) (update_defined_types (\<lambda>_. {TypeExn (mk_id ?mn ?cn)} \<union> defined_types ?s) ?s, Rval (make_sem_env nsEmpty (nsSing ?cn (length ?ts, TypeExn (mk_id ?mn ?cn)))))
TypeExn (mk_id ?mn ?cn) \<in> defined_types ?s \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dexn ?locs ?cn ?ts) (?s, Rerr (Rabort Rtype_error))
defined_types (update_clock ?f ?x) = defined_types ?x

goal (1 subgoal):
 1. \<And>count. \<lbrakk>check_dup_ctors tds_; new_tdecs_ = type_defs_to_new_tdecs mn_ tds_; disjnt (type_defs_to_new_tdecs mn_ tds_) (defined_types s_); allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds_)\<rbrakk> \<Longrightarrow> evaluate_dec False mn_ env_ (update_clock (\<lambda>_. count) s_) (Dtype locs_ tds_) (update_defined_types (\<lambda>_. type_defs_to_new_tdecs mn_ tds_ \<union> defined_types s_) (update_clock (\<lambda>_. count) s_), Rval (make_sem_env nsEmpty (build_tdefs mn_ tds_)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>s' r count. (update_defined_types (\<lambda>_. new_tdecs_ \<union> defined_types s_) s_, Rval (make_sem_env nsEmpty (build_tdefs mn_ tds_))) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn_ env_ (update_clock (\<lambda>_. count) s_) (Dtype locs_ tds_) (update_clock (\<lambda>_. count) s', r)

goal (11 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env' \<Longrightarrow> \<forall>s' r count. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 2. \<And>ck mn env p e v1 s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = No_match \<Longrightarrow> \<forall>s' r count. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 3. \<And>ck mn env p e v1 s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match_type_error \<Longrightarrow> \<forall>s' r count. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 5. \<And>ck mn env p e err s s' locs. evaluate ck env s e (s', Rerr err) \<and> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s'a r count. (s', Rerr err) = (s'a, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dlet locs p e) (update_clock (\<lambda>_. count) s'a, r)
 6. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r count. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dletrec locs funs) (update_clock (\<lambda>_. count) s', r)
 7. \<And>ck mn env funs s locs. \<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dletrec locs funs) (update_clock (\<lambda>_. count) s', r)
 8. \<And>ck mn env tds s locs. \<not> check_dup_ctors tds \<or> \<not> disjnt (type_defs_to_new_tdecs mn tds) (defined_types s) \<or> \<not> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtype locs tds) (update_clock (\<lambda>_. count) s', r)
 9. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r count. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. count) s', r)
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r count. (update_defined_types (\<lambda>_. {TypeExn (mk_id mn cn)} \<union> defined_types s) s, Rval (make_sem_env nsEmpty (nsSing cn (length ts, TypeExn (mk_id mn cn))))) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dexn locs cn ts) (update_clock (\<lambda>_. count) s', r)
A total of 11 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env' \<Longrightarrow> \<forall>s' r count. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 2. \<And>ck mn env p e v1 s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = No_match \<Longrightarrow> \<forall>s' r count. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 3. \<And>ck mn env p e v1 s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match_type_error \<Longrightarrow> \<forall>s' r count. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 5. \<And>ck mn env p e err s s' locs. evaluate ck env s e (s', Rerr err) \<and> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s'a r count. (s', Rerr err) = (s'a, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dlet locs p e) (update_clock (\<lambda>_. count) s'a, r)
 6. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r count. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dletrec locs funs) (update_clock (\<lambda>_. count) s', r)
 7. \<And>ck mn env funs s locs. \<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dletrec locs funs) (update_clock (\<lambda>_. count) s', r)
 8. \<And>ck mn env tds s locs. \<not> check_dup_ctors tds \<or> \<not> disjnt (type_defs_to_new_tdecs mn tds) (defined_types s) \<or> \<not> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtype locs tds) (update_clock (\<lambda>_. count) s', r)
 9. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r count. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. count) s', r)
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r count. (update_defined_types (\<lambda>_. {TypeExn (mk_id mn cn)} \<union> defined_types s) s, Rval (make_sem_env nsEmpty (nsSing cn (length ts, TypeExn (mk_id mn cn))))) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dexn locs cn ts) (update_clock (\<lambda>_. count) s', r)
A total of 11 subgoals...
[PROOF STEP]
case dexn1
[PROOF STATE]
proof (state)
this:
TypeExn (mk_id mn_ cn_) \<notin> defined_types s_

goal (11 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env' \<Longrightarrow> \<forall>s' r count. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 2. \<And>ck mn env p e v1 s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = No_match \<Longrightarrow> \<forall>s' r count. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 3. \<And>ck mn env p e v1 s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match_type_error \<Longrightarrow> \<forall>s' r count. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 5. \<And>ck mn env p e err s s' locs. evaluate ck env s e (s', Rerr err) \<and> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s'a r count. (s', Rerr err) = (s'a, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dlet locs p e) (update_clock (\<lambda>_. count) s'a, r)
 6. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r count. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dletrec locs funs) (update_clock (\<lambda>_. count) s', r)
 7. \<And>ck mn env funs s locs. \<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dletrec locs funs) (update_clock (\<lambda>_. count) s', r)
 8. \<And>ck mn env tds s locs. \<not> check_dup_ctors tds \<or> \<not> disjnt (type_defs_to_new_tdecs mn tds) (defined_types s) \<or> \<not> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtype locs tds) (update_clock (\<lambda>_. count) s', r)
 9. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r count. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. count) s', r)
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r count. (update_defined_types (\<lambda>_. {TypeExn (mk_id mn cn)} \<union> defined_types s) s, Rval (make_sem_env nsEmpty (nsSing cn (length ts, TypeExn (mk_id mn cn))))) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dexn locs cn ts) (update_clock (\<lambda>_. count) s', r)
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
TypeExn (mk_id mn_ cn_) \<notin> defined_types s_
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
TypeExn (mk_id mn_ cn_) \<notin> defined_types s_

goal (1 subgoal):
 1. \<forall>s' r count. (update_defined_types (\<lambda>_. {TypeExn (mk_id mn_ cn_)} \<union> defined_types s_) s_, Rval (make_sem_env nsEmpty (nsSing cn_ (length ts_, TypeExn (mk_id mn_ cn_))))) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn_ env_ (update_clock (\<lambda>_. count) s_) (Dexn locs_ cn_ ts_) (update_clock (\<lambda>_. count) s', r)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>count. TypeExn (mk_id mn_ cn_) \<notin> defined_types s_ \<Longrightarrow> evaluate_dec False mn_ env_ (update_clock (\<lambda>_. count) s_) (Dexn locs_ cn_ ts_) (update_defined_types (\<lambda>_. insert (TypeExn (mk_id mn_ cn_)) (defined_types s_)) (update_clock (\<lambda>_. count) s_), Rval (make_sem_env nsEmpty (nsSing cn_ (length ts_, TypeExn (mk_id mn_ cn_)))))
[PROOF STEP]
using evaluate_dec.intros state.record_simps(4)
[PROOF STATE]
proof (prove)
using this:
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = Match ?env' \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rval (make_sem_env (alist_to_ns ?env') nsEmpty))
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = No_match \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rerr (Rraise Bindv))
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = Match_type_error \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rerr (Rabort Rtype_error))
\<not> allDistinct (pat_bindings ?p []) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dlet ?locs ?p ?e) (?s, Rerr (Rabort Rtype_error))
evaluate ?ck ?env ?s ?e (?s', Rerr ?err) \<and> allDistinct (pat_bindings ?p []) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dlet ?locs ?p ?e) (?s', Rerr ?err)
allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) ?funs) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dletrec ?locs ?funs) (?s, Rval (make_sem_env (build_rec_env ?funs ?env nsEmpty) nsEmpty))
\<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) ?funs) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dletrec ?locs ?funs) (?s, Rerr (Rabort Rtype_error))
check_dup_ctors ?tds \<and> ?new_tdecs = type_defs_to_new_tdecs ?mn ?tds \<and> disjnt ?new_tdecs (defined_types ?s) \<and> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) ?tds) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dtype ?locs ?tds) (update_defined_types (\<lambda>_. ?new_tdecs \<union> defined_types ?s) ?s, Rval (make_sem_env nsEmpty (build_tdefs ?mn ?tds)))
\<not> check_dup_ctors ?tds \<or> \<not> disjnt (type_defs_to_new_tdecs ?mn ?tds) (defined_types ?s) \<or> \<not> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) ?tds) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dtype ?locs ?tds) (?s, Rerr (Rabort Rtype_error))
evaluate_dec ?ck ?mn ?env ?s (Dtabbrev ?locs ?tvs ?tn ?t0.0) (?s, Rval (make_sem_env nsEmpty nsEmpty))
TypeExn (mk_id ?mn ?cn) \<notin> defined_types ?s \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dexn ?locs ?cn ?ts) (update_defined_types (\<lambda>_. {TypeExn (mk_id ?mn ?cn)} \<union> defined_types ?s) ?s, Rval (make_sem_env nsEmpty (nsSing ?cn (length ?ts, TypeExn (mk_id ?mn ?cn)))))
TypeExn (mk_id ?mn ?cn) \<in> defined_types ?s \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dexn ?locs ?cn ?ts) (?s, Rerr (Rabort Rtype_error))
defined_types (update_clock ?f ?x) = defined_types ?x

goal (1 subgoal):
 1. \<And>count. TypeExn (mk_id mn_ cn_) \<notin> defined_types s_ \<Longrightarrow> evaluate_dec False mn_ env_ (update_clock (\<lambda>_. count) s_) (Dexn locs_ cn_ ts_) (update_defined_types (\<lambda>_. insert (TypeExn (mk_id mn_ cn_)) (defined_types s_)) (update_clock (\<lambda>_. count) s_), Rval (make_sem_env nsEmpty (nsSing cn_ (length ts_, TypeExn (mk_id mn_ cn_)))))
[PROOF STEP]
by (metis Un_insert_left sup_bot.left_neutral)
[PROOF STATE]
proof (state)
this:
\<forall>s' r count. (update_defined_types (\<lambda>_. {TypeExn (mk_id mn_ cn_)} \<union> defined_types s_) s_, Rval (make_sem_env nsEmpty (nsSing cn_ (length ts_, TypeExn (mk_id mn_ cn_))))) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn_ env_ (update_clock (\<lambda>_. count) s_) (Dexn locs_ cn_ ts_) (update_clock (\<lambda>_. count) s', r)

goal (10 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env' \<Longrightarrow> \<forall>s' r count. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 2. \<And>ck mn env p e v1 s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = No_match \<Longrightarrow> \<forall>s' r count. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 3. \<And>ck mn env p e v1 s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match_type_error \<Longrightarrow> \<forall>s' r count. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s1) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dlet locs p e) (update_clock (\<lambda>_. count) s', r)
 5. \<And>ck mn env p e err s s' locs. evaluate ck env s e (s', Rerr err) \<and> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s'a r count. (s', Rerr err) = (s'a, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dlet locs p e) (update_clock (\<lambda>_. count) s'a, r)
 6. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r count. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dletrec locs funs) (update_clock (\<lambda>_. count) s', r)
 7. \<And>ck mn env funs s locs. \<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dletrec locs funs) (update_clock (\<lambda>_. count) s', r)
 8. \<And>ck mn env tds s locs. \<not> check_dup_ctors tds \<or> \<not> disjnt (type_defs_to_new_tdecs mn tds) (defined_types s) \<or> \<not> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds) \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtype locs tds) (update_clock (\<lambda>_. count) s', r)
 9. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r count. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. count) s', r)
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r count. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) (Dexn locs cn ts) (update_clock (\<lambda>_. count) s', r)
[PROOF STEP]
qed (force intro:evaluate_dec.intros simp add:big_unclocked_ignore(3))+


[STATEMENT]
lemma dec_unclocked_1:
  assumes "evaluate_dec False mn env s d (s',r)"
  shows "(r \<noteq> Rerr (Rabort Rtimeout_error)) \<and> (clock   s) = (clock   s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
evaluate_dec False mn env s d (s', r)

goal (1 subgoal):
 1. r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
by cases (auto dest: big_unclocked_notimeout big_unclocked_unchanged)


[STATEMENT]
lemma dec_unclocked_2:
  assumes "evaluate_dec False mn env (s \<lparr> clock := count1 \<rparr>) d ((s' \<lparr> clock := count1 \<rparr>),r)"
  shows "evaluate_dec False mn env (s \<lparr> clock := count2 \<rparr>) d ((s' \<lparr> clock := count2 \<rparr>),r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_dec False mn env (update_clock (\<lambda>_. count2) s) d (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. evaluate_dec False mn env (update_clock (\<lambda>_. count2) s) d (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
evaluate_dec False mn env (update_clock (\<lambda>_. count1) s) d (update_clock (\<lambda>_. count1) s', r)
[PROOF STEP]
have "r \<noteq> Rerr (Rabort Rtimeout_error)"
[PROOF STATE]
proof (prove)
using this:
evaluate_dec False mn env (update_clock (\<lambda>_. count1) s) d (update_clock (\<lambda>_. count1) s', r)

goal (1 subgoal):
 1. r \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
using dec_evaluate_not_timeout
[PROOF STATE]
proof (prove)
using this:
evaluate_dec False mn env (update_clock (\<lambda>_. count1) s) d (update_clock (\<lambda>_. count1) s', r)
evaluate_dec False ?mn ?env ?s ?d (?s', ?r) \<Longrightarrow> ?r \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. r \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. evaluate_dec False mn env (update_clock (\<lambda>_. count2) s) d (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. evaluate_dec False mn env (update_clock (\<lambda>_. count2) s) d (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
using assms dec_unclocked_ignore[rule_format]
[PROOF STATE]
proof (prove)
using this:
r \<noteq> Rerr (Rabort Rtimeout_error)
evaluate_dec False mn env (update_clock (\<lambda>_. count1) s) d (update_clock (\<lambda>_. count1) s', r)
\<lbrakk>evaluate_dec ?ck ?mn ?env ?s ?d ?res; ?res = (?s', ?r) \<and> ?r \<noteq> Rerr (Rabort Rtimeout_error)\<rbrakk> \<Longrightarrow> evaluate_dec False ?mn ?env (update_clock (\<lambda>_. ?count) ?s) ?d (update_clock (\<lambda>_. ?count) ?s', ?r)

goal (1 subgoal):
 1. evaluate_dec False mn env (update_clock (\<lambda>_. count2) s) d (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
evaluate_dec False mn env (update_clock (\<lambda>_. count2) s) d (update_clock (\<lambda>_. count2) s', r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dec_unclocked:
  "(evaluate_dec False mn env s d (s',r) \<longrightarrow> (r \<noteq> Rerr (Rabort Rtimeout_error)) \<and> (clock   s) = (clock   s')) \<and>
   (evaluate_dec False mn env (s (| clock := count1 |)) d ((s' (| clock := count1 |)),r) \<longrightarrow>
   evaluate_dec False mn env (s (| clock := count2 |)) d ((s' (| clock := count2 |)),r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (evaluate_dec False mn env s d (s', r) \<longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s') \<and> (evaluate_dec False mn env (update_clock (\<lambda>_. count1) s) d (update_clock (\<lambda>_. count1) s', r) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count2) s) d (update_clock (\<lambda>_. count2) s', r))
[PROOF STEP]
using dec_unclocked_1 dec_unclocked_2
[PROOF STATE]
proof (prove)
using this:
evaluate_dec False ?mn ?env ?s ?d (?s', ?r) \<Longrightarrow> ?r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock ?s = clock ?s'
evaluate_dec False ?mn ?env (update_clock (\<lambda>_. ?count1.0) ?s) ?d (update_clock (\<lambda>_. ?count1.0) ?s', ?r) \<Longrightarrow> evaluate_dec False ?mn ?env (update_clock (\<lambda>_. ?count2.0) ?s) ?d (update_clock (\<lambda>_. ?count2.0) ?s', ?r)

goal (1 subgoal):
 1. (evaluate_dec False mn env s d (s', r) \<longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s') \<and> (evaluate_dec False mn env (update_clock (\<lambda>_. count1) s) d (update_clock (\<lambda>_. count1) s', r) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count2) s) d (update_clock (\<lambda>_. count2) s', r))
[PROOF STEP]
by blast


[STATEMENT]
lemma not_evaluate_dec_timeout:
  assumes "\<forall>r. \<not>evaluate_dec False mn env s d r"
  shows "\<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
proof (cases d)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x11 x12 x13. d = Dlet x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x21 x22. d = Dletrec x21 x22 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 3. \<And>x31 x32. d = Dtype x31 x32 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 4. \<And>x41 x42 x43 x44. d = Dtabbrev x41 x42 x43 x44 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 5. \<And>x51 x52 x53. d = Dexn x51 x52 x53 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
case (Dlet locs p e)
[PROOF STATE]
proof (state)
this:
d = Dlet locs p e

goal (5 subgoals):
 1. \<And>x11 x12 x13. d = Dlet x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x21 x22. d = Dletrec x21 x22 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 3. \<And>x31 x32. d = Dtype x31 x32 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 4. \<And>x41 x42 x43 x44. d = Dtabbrev x41 x42 x43 x44 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 5. \<And>x51 x52 x53. d = Dexn x51 x52 x53 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
have "\<not> evaluate False env s e r" for r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> evaluate False env s e r
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate False env s e r \<Longrightarrow> False
[PROOF STEP]
apply (cases "Lem_list.allDistinct (pat_bindings p [])")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>evaluate False env s e r; allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>evaluate False env s e r; \<not> allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate False env s e r; allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cases r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>evaluate False env s e r; allDistinct (pat_bindings p []); r = (a, b)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply hypsubst_thin
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>evaluate False env s e (a, b); allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for s' r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate False env s e (s', r); allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cases r; hypsubst_thin)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>evaluate False env s e (s', Rval x1); allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>evaluate False env s e (s', Rerr x2); allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate False env s e (s', Rval v); allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cases "pmatch(c   env)(refs   s') p v []")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>evaluate False env s e (s', Rval v); allDistinct (pat_bindings p []); pmatch (c env) (refs s') p v [] = No_match\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>evaluate False env s e (s', Rval v); allDistinct (pat_bindings p []); pmatch (c env) (refs s') p v [] = Match_type_error\<rbrakk> \<Longrightarrow> False
 3. \<And>x3. \<lbrakk>evaluate False env s e (s', Rval v); allDistinct (pat_bindings p []); pmatch (c env) (refs s') p v [] = Match x3\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>r. \<not> evaluate_dec False mn env s d r

goal (3 subgoals):
 1. \<lbrakk>evaluate False env s e (s', Rval v); allDistinct (pat_bindings p []); pmatch (c env) (refs s') p v [] = No_match\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>evaluate False env s e (s', Rval v); allDistinct (pat_bindings p []); pmatch (c env) (refs s') p v [] = Match_type_error\<rbrakk> \<Longrightarrow> False
 3. \<And>x3. \<lbrakk>evaluate False env s e (s', Rval v); allDistinct (pat_bindings p []); pmatch (c env) (refs s') p v [] = Match x3\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding Dlet
[PROOF STATE]
proof (prove)
using this:
\<forall>r. \<not> evaluate_dec False mn env s (Dlet locs p e) r

goal (3 subgoals):
 1. \<lbrakk>evaluate False env s e (s', Rval v); allDistinct (pat_bindings p []); pmatch (c env) (refs s') p v [] = No_match\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>evaluate False env s e (s', Rval v); allDistinct (pat_bindings p []); pmatch (c env) (refs s') p v [] = Match_type_error\<rbrakk> \<Longrightarrow> False
 3. \<And>x3. \<lbrakk>evaluate False env s e (s', Rval v); allDistinct (pat_bindings p []); pmatch (c env) (refs s') p v [] = Match x3\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis evaluate_dec.intros)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evaluate False env s e (s', Rerr x2); allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate False env s e (s', Rerr x2_); allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>r. \<not> evaluate_dec False mn env s d r

goal (1 subgoal):
 1. \<lbrakk>evaluate False env s e (s', Rerr x2_); allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding Dlet
[PROOF STATE]
proof (prove)
using this:
\<forall>r. \<not> evaluate_dec False mn env s (Dlet locs p e) r

goal (1 subgoal):
 1. \<lbrakk>evaluate False env s e (s', Rerr x2_); allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis dlet5)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate False env s e r; \<not> allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate False env s e r; \<not> allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>r. \<not> evaluate_dec False mn env s d r

goal (1 subgoal):
 1. \<lbrakk>evaluate False env s e r; \<not> allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding Dlet
[PROOF STATE]
proof (prove)
using this:
\<forall>r. \<not> evaluate_dec False mn env s (Dlet locs p e) r

goal (1 subgoal):
 1. \<lbrakk>evaluate False env s e r; \<not> allDistinct (pat_bindings p [])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis dlet4)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<not> evaluate False env s e ?r

goal (5 subgoals):
 1. \<And>x11 x12 x13. d = Dlet x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x21 x22. d = Dletrec x21 x22 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 3. \<And>x31 x32. d = Dtype x31 x32 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 4. \<And>x41 x42 x43 x44. d = Dtabbrev x41 x42 x43 x44 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 5. \<And>x51 x52 x53. d = Dexn x51 x52 x53 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
note big_clocked_unclocked_equiv_timeout_1[rule_format, OF this]
[PROOF STATE]
proof (state)
this:
\<exists>s'. evaluate True env (update_clock (\<lambda>_. ?c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0

goal (5 subgoals):
 1. \<And>x11 x12 x13. d = Dlet x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x21 x22. d = Dletrec x21 x22 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 3. \<And>x31 x32. d = Dtype x31 x32 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 4. \<And>x41 x42 x43 x44. d = Dtabbrev x41 x42 x43 x44 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 5. \<And>x51 x52 x53. d = Dexn x51 x52 x53 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s'. evaluate True env (update_clock (\<lambda>_. ?c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0
[PROOF STEP]
obtain s' where "evaluate True env (update_clock (\<lambda>_. clock s) s) e (s', Rerr (Rabort Rtimeout_error))"
[PROOF STATE]
proof (prove)
using this:
\<exists>s'. evaluate True env (update_clock (\<lambda>_. ?c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0

goal (1 subgoal):
 1. (\<And>s'. evaluate True env (update_clock (\<lambda>_. clock s) s) e (s', Rerr (Rabort Rtimeout_error)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
evaluate True env (update_clock (\<lambda>_. clock s) s) e (s', Rerr (Rabort Rtimeout_error))

goal (5 subgoals):
 1. \<And>x11 x12 x13. d = Dlet x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x21 x22. d = Dletrec x21 x22 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 3. \<And>x31 x32. d = Dtype x31 x32 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 4. \<And>x41 x42 x43 x44. d = Dtabbrev x41 x42 x43 x44 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 5. \<And>x51 x52 x53. d = Dexn x51 x52 x53 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate True env (update_clock (\<lambda>_. clock s) s) e (s', Rerr (Rabort Rtimeout_error))
[PROOF STEP]
have "evaluate True env s e (s', Rerr (Rabort Rtimeout_error))"
[PROOF STATE]
proof (prove)
using this:
evaluate True env (update_clock (\<lambda>_. clock s) s) e (s', Rerr (Rabort Rtimeout_error))

goal (1 subgoal):
 1. evaluate True env s e (s', Rerr (Rabort Rtimeout_error))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
evaluate True env s e (s', Rerr (Rabort Rtimeout_error))

goal (5 subgoals):
 1. \<And>x11 x12 x13. d = Dlet x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x21 x22. d = Dletrec x21 x22 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 3. \<And>x31 x32. d = Dtype x31 x32 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 4. \<And>x41 x42 x43 x44. d = Dtabbrev x41 x42 x43 x44 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 5. \<And>x51 x52 x53. d = Dexn x51 x52 x53 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
have "Lem_list.allDistinct (pat_bindings p [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. allDistinct (pat_bindings p [])
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> False
[PROOF STEP]
apply (drule dlet4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_dec ?ck2 ?mn2 ?env2 ?s2 (Dlet ?locs2 p ?e2) (?s2, Rerr (Rabort Rtype_error)) \<Longrightarrow> False
[PROOF STEP]
using assms Dlet
[PROOF STATE]
proof (prove)
using this:
\<forall>r. \<not> evaluate_dec False mn env s d r
d = Dlet locs p e

goal (1 subgoal):
 1. evaluate_dec ?ck2 ?mn2 ?env2 ?s2 (Dlet ?locs2 p ?e2) (?s2, Rerr (Rabort Rtype_error)) \<Longrightarrow> False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
allDistinct (pat_bindings p [])

goal (5 subgoals):
 1. \<And>x11 x12 x13. d = Dlet x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x21 x22. d = Dletrec x21 x22 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 3. \<And>x31 x32. d = Dtype x31 x32 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 4. \<And>x41 x42 x43 x44. d = Dtabbrev x41 x42 x43 x44 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 5. \<And>x51 x52 x53. d = Dexn x51 x52 x53 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
unfolding Dlet
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_dec True mn env s (Dlet locs p e) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply (intro exI conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. evaluate_dec True mn env s (Dlet locs p e) ?r
 2. snd ?r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply (rule dlet5)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. evaluate True env s e (?s'2, Rerr ?err2) \<and> allDistinct (pat_bindings p [])
 2. snd (?s'2, Rerr ?err2) = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. evaluate True env s e (?s'2, Rerr ?err2)
 2. allDistinct (pat_bindings p [])
 3. snd (?s'2, Rerr ?err2) = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply fact+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (s', Rerr (Rabort Rtimeout_error)) = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)

goal (4 subgoals):
 1. \<And>x21 x22. d = Dletrec x21 x22 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x31 x32. d = Dtype x31 x32 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 3. \<And>x41 x42 x43 x44. d = Dtabbrev x41 x42 x43 x44 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
 4. \<And>x51 x52 x53. d = Dexn x51 x52 x53 \<Longrightarrow> \<exists>r. evaluate_dec True mn env s d r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
qed (metis evaluate_dec.intros assms)+


[STATEMENT]
lemma dec_clocked_total: "\<exists>res. evaluate_dec True mn env s d res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>res. evaluate_dec True mn env s d res
[PROOF STEP]
proof (cases d)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x11 x12 x13. d = Dlet x11 x12 x13 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 2. \<And>x21 x22. d = Dletrec x21 x22 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 3. \<And>x31 x32. d = Dtype x31 x32 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 4. \<And>x41 x42 x43 x44. d = Dtabbrev x41 x42 x43 x44 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 5. \<And>x51 x52 x53. d = Dexn x51 x52 x53 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
[PROOF STEP]
case (Dlet locs p e)
[PROOF STATE]
proof (state)
this:
d = Dlet locs p e

goal (5 subgoals):
 1. \<And>x11 x12 x13. d = Dlet x11 x12 x13 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 2. \<And>x21 x22. d = Dletrec x21 x22 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 3. \<And>x31 x32. d = Dtype x31 x32 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 4. \<And>x41 x42 x43 x44. d = Dtabbrev x41 x42 x43 x44 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 5. \<And>x51 x52 x53. d = Dexn x51 x52 x53 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
[PROOF STEP]
obtain s' r where e:"evaluate True env s e (s', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s' r. evaluate True env s e (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis evaluate_total)
[PROOF STATE]
proof (state)
this:
evaluate True env s e (s', r)

goal (5 subgoals):
 1. \<And>x11 x12 x13. d = Dlet x11 x12 x13 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 2. \<And>x21 x22. d = Dletrec x21 x22 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 3. \<And>x31 x32. d = Dtype x31 x32 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 4. \<And>x41 x42 x43 x44. d = Dtabbrev x41 x42 x43 x44 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 5. \<And>x51 x52 x53. d = Dexn x51 x52 x53 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>res. evaluate_dec True mn env s d res
[PROOF STEP]
unfolding Dlet
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
[PROOF STEP]
apply (cases "Lem_list.allDistinct (pat_bindings p [])")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. allDistinct (pat_bindings p []) \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
 2. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. allDistinct (pat_bindings p []) \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e (s', r)

goal (1 subgoal):
 1. allDistinct (pat_bindings p []) \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
[PROOF STEP]
apply (cases r)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>allDistinct (pat_bindings p []); evaluate True env s e (s', r); r = Rval x1\<rbrakk> \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
 2. \<And>x2. \<lbrakk>allDistinct (pat_bindings p []); evaluate True env s e (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
[PROOF STEP]
subgoal for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>allDistinct (pat_bindings p []); evaluate True env s e (s', r); r = Rval v\<rbrakk> \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
[PROOF STEP]
apply hypsubst_thin
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>allDistinct (pat_bindings p []); evaluate True env s e (s', Rval v)\<rbrakk> \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
[PROOF STEP]
apply (cases "pmatch(c   env)(refs   s') p v []")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>allDistinct (pat_bindings p []); evaluate True env s e (s', Rval v); pmatch (c env) (refs s') p v [] = No_match\<rbrakk> \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
 2. \<lbrakk>allDistinct (pat_bindings p []); evaluate True env s e (s', Rval v); pmatch (c env) (refs s') p v [] = Match_type_error\<rbrakk> \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
 3. \<And>x3. \<lbrakk>allDistinct (pat_bindings p []); evaluate True env s e (s', Rval v); pmatch (c env) (refs s') p v [] = Match x3\<rbrakk> \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
[PROOF STEP]
using evaluate_dec.intros
[PROOF STATE]
proof (prove)
using this:
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = Match ?env' \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rval (make_sem_env (alist_to_ns ?env') nsEmpty))
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = No_match \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rerr (Rraise Bindv))
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = Match_type_error \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rerr (Rabort Rtype_error))
\<not> allDistinct (pat_bindings ?p []) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dlet ?locs ?p ?e) (?s, Rerr (Rabort Rtype_error))
evaluate ?ck ?env ?s ?e (?s', Rerr ?err) \<and> allDistinct (pat_bindings ?p []) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dlet ?locs ?p ?e) (?s', Rerr ?err)
allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) ?funs) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dletrec ?locs ?funs) (?s, Rval (make_sem_env (build_rec_env ?funs ?env nsEmpty) nsEmpty))
\<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) ?funs) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dletrec ?locs ?funs) (?s, Rerr (Rabort Rtype_error))
check_dup_ctors ?tds \<and> ?new_tdecs = type_defs_to_new_tdecs ?mn ?tds \<and> disjnt ?new_tdecs (defined_types ?s) \<and> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) ?tds) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dtype ?locs ?tds) (update_defined_types (\<lambda>_. ?new_tdecs \<union> defined_types ?s) ?s, Rval (make_sem_env nsEmpty (build_tdefs ?mn ?tds)))
\<not> check_dup_ctors ?tds \<or> \<not> disjnt (type_defs_to_new_tdecs ?mn ?tds) (defined_types ?s) \<or> \<not> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) ?tds) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dtype ?locs ?tds) (?s, Rerr (Rabort Rtype_error))
evaluate_dec ?ck ?mn ?env ?s (Dtabbrev ?locs ?tvs ?tn ?t0.0) (?s, Rval (make_sem_env nsEmpty nsEmpty))
TypeExn (mk_id ?mn ?cn) \<notin> defined_types ?s \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dexn ?locs ?cn ?ts) (update_defined_types (\<lambda>_. {TypeExn (mk_id ?mn ?cn)} \<union> defined_types ?s) ?s, Rval (make_sem_env nsEmpty (nsSing ?cn (length ?ts, TypeExn (mk_id ?mn ?cn)))))
TypeExn (mk_id ?mn ?cn) \<in> defined_types ?s \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dexn ?locs ?cn ?ts) (?s, Rerr (Rabort Rtype_error))

goal (3 subgoals):
 1. \<lbrakk>allDistinct (pat_bindings p []); evaluate True env s e (s', Rval v); pmatch (c env) (refs s') p v [] = No_match\<rbrakk> \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
 2. \<lbrakk>allDistinct (pat_bindings p []); evaluate True env s e (s', Rval v); pmatch (c env) (refs s') p v [] = Match_type_error\<rbrakk> \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
 3. \<And>x3. \<lbrakk>allDistinct (pat_bindings p []); evaluate True env s e (s', Rval v); pmatch (c env) (refs s') p v [] = Match x3\<rbrakk> \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
[PROOF STEP]
by metis+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>allDistinct (pat_bindings p []); evaluate True env s e (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
[PROOF STEP]
using evaluate_dec.intros
[PROOF STATE]
proof (prove)
using this:
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = Match ?env' \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rval (make_sem_env (alist_to_ns ?env') nsEmpty))
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = No_match \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rerr (Rraise Bindv))
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = Match_type_error \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rerr (Rabort Rtype_error))
\<not> allDistinct (pat_bindings ?p []) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dlet ?locs ?p ?e) (?s, Rerr (Rabort Rtype_error))
evaluate ?ck ?env ?s ?e (?s', Rerr ?err) \<and> allDistinct (pat_bindings ?p []) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dlet ?locs ?p ?e) (?s', Rerr ?err)
allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) ?funs) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dletrec ?locs ?funs) (?s, Rval (make_sem_env (build_rec_env ?funs ?env nsEmpty) nsEmpty))
\<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) ?funs) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dletrec ?locs ?funs) (?s, Rerr (Rabort Rtype_error))
check_dup_ctors ?tds \<and> ?new_tdecs = type_defs_to_new_tdecs ?mn ?tds \<and> disjnt ?new_tdecs (defined_types ?s) \<and> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) ?tds) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dtype ?locs ?tds) (update_defined_types (\<lambda>_. ?new_tdecs \<union> defined_types ?s) ?s, Rval (make_sem_env nsEmpty (build_tdefs ?mn ?tds)))
\<not> check_dup_ctors ?tds \<or> \<not> disjnt (type_defs_to_new_tdecs ?mn ?tds) (defined_types ?s) \<or> \<not> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) ?tds) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dtype ?locs ?tds) (?s, Rerr (Rabort Rtype_error))
evaluate_dec ?ck ?mn ?env ?s (Dtabbrev ?locs ?tvs ?tn ?t0.0) (?s, Rval (make_sem_env nsEmpty nsEmpty))
TypeExn (mk_id ?mn ?cn) \<notin> defined_types ?s \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dexn ?locs ?cn ?ts) (update_defined_types (\<lambda>_. {TypeExn (mk_id ?mn ?cn)} \<union> defined_types ?s) ?s, Rval (make_sem_env nsEmpty (nsSing ?cn (length ?ts, TypeExn (mk_id ?mn ?cn)))))
TypeExn (mk_id ?mn ?cn) \<in> defined_types ?s \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dexn ?locs ?cn ?ts) (?s, Rerr (Rabort Rtype_error))

goal (1 subgoal):
 1. \<And>x2. \<lbrakk>allDistinct (pat_bindings p []); evaluate True env s e (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
[PROOF STEP]
by metis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
[PROOF STEP]
using evaluate_dec.intros
[PROOF STATE]
proof (prove)
using this:
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = Match ?env' \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rval (make_sem_env (alist_to_ns ?env') nsEmpty))
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = No_match \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rerr (Rraise Bindv))
evaluate ?ck ?env ?s1.0 ?e (?s2.0, Rval ?v1.0) \<and> allDistinct (pat_bindings ?p []) \<and> pmatch (c ?env) (refs ?s2.0) ?p ?v1.0 [] = Match_type_error \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s1.0 (Dlet ?locs ?p ?e) (?s2.0, Rerr (Rabort Rtype_error))
\<not> allDistinct (pat_bindings ?p []) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dlet ?locs ?p ?e) (?s, Rerr (Rabort Rtype_error))
evaluate ?ck ?env ?s ?e (?s', Rerr ?err) \<and> allDistinct (pat_bindings ?p []) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dlet ?locs ?p ?e) (?s', Rerr ?err)
allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) ?funs) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dletrec ?locs ?funs) (?s, Rval (make_sem_env (build_rec_env ?funs ?env nsEmpty) nsEmpty))
\<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) ?funs) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dletrec ?locs ?funs) (?s, Rerr (Rabort Rtype_error))
check_dup_ctors ?tds \<and> ?new_tdecs = type_defs_to_new_tdecs ?mn ?tds \<and> disjnt ?new_tdecs (defined_types ?s) \<and> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) ?tds) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dtype ?locs ?tds) (update_defined_types (\<lambda>_. ?new_tdecs \<union> defined_types ?s) ?s, Rval (make_sem_env nsEmpty (build_tdefs ?mn ?tds)))
\<not> check_dup_ctors ?tds \<or> \<not> disjnt (type_defs_to_new_tdecs ?mn ?tds) (defined_types ?s) \<or> \<not> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) ?tds) \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dtype ?locs ?tds) (?s, Rerr (Rabort Rtype_error))
evaluate_dec ?ck ?mn ?env ?s (Dtabbrev ?locs ?tvs ?tn ?t0.0) (?s, Rval (make_sem_env nsEmpty nsEmpty))
TypeExn (mk_id ?mn ?cn) \<notin> defined_types ?s \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dexn ?locs ?cn ?ts) (update_defined_types (\<lambda>_. {TypeExn (mk_id ?mn ?cn)} \<union> defined_types ?s) ?s, Rval (make_sem_env nsEmpty (nsSing ?cn (length ?ts, TypeExn (mk_id ?mn ?cn)))))
TypeExn (mk_id ?mn ?cn) \<in> defined_types ?s \<Longrightarrow> evaluate_dec ?ck ?mn ?env ?s (Dexn ?locs ?cn ?ts) (?s, Rerr (Rabort Rtype_error))

goal (1 subgoal):
 1. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<exists>res. evaluate_dec True mn env s (Dlet locs p e) res
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>res. evaluate_dec True mn env s d res

goal (4 subgoals):
 1. \<And>x21 x22. d = Dletrec x21 x22 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 2. \<And>x31 x32. d = Dtype x31 x32 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 3. \<And>x41 x42 x43 x44. d = Dtabbrev x41 x42 x43 x44 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
 4. \<And>x51 x52 x53. d = Dexn x51 x52 x53 \<Longrightarrow> \<exists>res. evaluate_dec True mn env s d res
[PROOF STEP]
qed (blast intro: evaluate_dec.intros)+