[STATEMENT]
lemma dec_add_clock:
  "evaluate_dec ck mn env s d res \<Longrightarrow>
   \<forall>s' r. res = (s',r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (s (| clock := c |)) d ((s' (| clock := 0 |)),r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_dec ck mn env s d res \<Longrightarrow> \<forall>s' r. res = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) 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. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) 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. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) 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. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) 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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) 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. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) 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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) 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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) 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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 10. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
A total of 12 subgoals...
[PROOF STEP]
case dlet1
[PROOF STATE]
proof (state)
this:
evaluate ck_ env_ s1_ e_ (s2_, Rval v1_) \<and> allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = Match env'_

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. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) 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. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) 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. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) 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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) 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. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) 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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) 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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) 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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 10. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
A total of 12 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate ck_ env_ s1_ e_ (s2_, Rval v1_) \<and> allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = Match env'_
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
evaluate ck_ env_ s1_ e_ (s2_, Rval v1_) \<and> allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = Match env'_

goal (1 subgoal):
 1. \<forall>s' r. (s2_, Rval (make_sem_env (alist_to_ns env'_) nsEmpty)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate ck_ env_ s1_ e_ (s2_, Rval v1_); allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = Match env'_\<rbrakk> \<Longrightarrow> \<forall>s' r. (s2_, Rval (make_sem_env (alist_to_ns env'_) nsEmpty)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply (drule add_clock(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = Match env'_; \<forall>s' r'. (s2_, Rval v1_) = (s', r') \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate True env_ (update_clock (\<lambda>_. c) s1_) e_ (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r. (s2_, Rval (make_sem_env (alist_to_ns env'_) nsEmpty)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
by (auto|rule)+
[PROOF STATE]
proof (state)
this:
\<forall>s' r. (s2_, Rval (make_sem_env (alist_to_ns env'_) nsEmpty)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))

goal (11 subgoals):
 1. \<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. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) 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 [] = Match_type_error \<Longrightarrow> \<forall>s' r. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 4. \<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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s'a, r))
 5. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 6. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 7. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) 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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 9. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) 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 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. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) 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 [] = Match_type_error \<Longrightarrow> \<forall>s' r. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 4. \<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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s'a, r))
 5. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 6. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 7. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) 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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 9. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
A total of 11 subgoals...
[PROOF STEP]
case dlet2
[PROOF STATE]
proof (state)
this:
evaluate ck_ env_ s1_ e_ (s2_, Rval v1_) \<and> allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = No_match

goal (11 subgoals):
 1. \<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. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) 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 [] = Match_type_error \<Longrightarrow> \<forall>s' r. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 4. \<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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s'a, r))
 5. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 6. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 7. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) 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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 9. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate ck_ env_ s1_ e_ (s2_, Rval v1_) \<and> allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = No_match
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
evaluate ck_ env_ s1_ e_ (s2_, Rval v1_) \<and> allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = No_match

goal (1 subgoal):
 1. \<forall>s' r. (s2_, Rerr (Rraise Bindv)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate ck_ env_ s1_ e_ (s2_, Rval v1_); allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = No_match\<rbrakk> \<Longrightarrow> \<forall>s' r. (s2_, Rerr (Rraise Bindv)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply (drule add_clock(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = No_match; \<forall>s' r'. (s2_, Rval v1_) = (s', r') \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate True env_ (update_clock (\<lambda>_. c) s1_) e_ (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r. (s2_, Rerr (Rraise Bindv)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ca. \<lbrakk>allDistinct (pat_bindings p_ []); pmatch (c env_) (refs s2_) p_ v1_ [] = No_match; \<not> ck_; evaluate True env_ (update_clock (\<lambda>_. ca) s1_) e_ (update_clock (\<lambda>_. 0) s2_, Rval v1_)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s2_, Rerr (Rraise Bindv))
[PROOF STEP]
by rule+ auto
[PROOF STATE]
proof (state)
this:
\<forall>s' r. (s2_, Rerr (Rraise Bindv)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))

goal (10 subgoals):
 1. \<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. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 3. \<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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s'a, r))
 4. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 5. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 6. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 7. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 8. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 9. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<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. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 3. \<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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s'a, r))
 4. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 5. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 6. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 7. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 8. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 9. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
case dlet3
[PROOF STATE]
proof (state)
this:
evaluate ck_ env_ s1_ e_ (s2_, Rval v1_) \<and> allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = Match_type_error

goal (10 subgoals):
 1. \<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. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 3. \<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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s'a, r))
 4. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 5. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 6. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 7. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 8. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 9. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate ck_ env_ s1_ e_ (s2_, Rval v1_) \<and> allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = Match_type_error
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
evaluate ck_ env_ s1_ e_ (s2_, Rval v1_) \<and> allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = Match_type_error

goal (1 subgoal):
 1. \<forall>s' r. (s2_, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate ck_ env_ s1_ e_ (s2_, Rval v1_); allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = Match_type_error\<rbrakk> \<Longrightarrow> \<forall>s' r. (s2_, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply (drule add_clock(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>allDistinct (pat_bindings p_ []) \<and> pmatch (c env_) (refs s2_) p_ v1_ [] = Match_type_error; \<forall>s' r'. (s2_, Rval v1_) = (s', r') \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate True env_ (update_clock (\<lambda>_. c) s1_) e_ (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r. (s2_, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ca. \<lbrakk>allDistinct (pat_bindings p_ []); pmatch (c env_) (refs s2_) p_ v1_ [] = Match_type_error; \<not> ck_; evaluate True env_ (update_clock (\<lambda>_. ca) s1_) e_ (update_clock (\<lambda>_. 0) s2_, Rval v1_)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s2_, Rerr (Rabort Rtype_error))
[PROOF STEP]
by rule+ auto
[PROOF STATE]
proof (state)
this:
\<forall>s' r. (s2_, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))

goal (9 subgoals):
 1. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 2. \<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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s'a, r))
 3. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 4. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 5. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 6. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 7. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 8. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 9. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 2. \<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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s'a, r))
 3. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 4. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 5. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 6. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 7. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 8. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 9. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
case dlet4
[PROOF STATE]
proof (state)
this:
\<not> allDistinct (pat_bindings p_ [])

goal (9 subgoals):
 1. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s', r))
 2. \<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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s'a, r))
 3. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 4. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 5. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 6. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 7. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 8. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 9. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> allDistinct (pat_bindings p_ [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<not> allDistinct (pat_bindings p_ [])

goal (1 subgoal):
 1. \<forall>s' r. (s_, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
by (auto intro:evaluate_dec.intros)
[PROOF STATE]
proof (state)
this:
\<forall>s' r. (s_, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s', r))

goal (8 subgoals):
 1. \<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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s'a, r))
 2. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 3. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 4. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 5. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 6. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 7. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 8. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s'a, r))
 2. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 3. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 4. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 5. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 6. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 7. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 8. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
case dlet5
[PROOF STATE]
proof (state)
this:
evaluate ck_ env_ s_ e_ (s'_, Rerr err_) \<and> allDistinct (pat_bindings p_ [])

goal (8 subgoals):
 1. \<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. (s', Rerr err) = (s'a, r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) s'a, r))
 2. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 3. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 4. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 5. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 6. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 7. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 8. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate ck_ env_ s_ e_ (s'_, Rerr err_) \<and> allDistinct (pat_bindings p_ [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
evaluate ck_ env_ s_ e_ (s'_, Rerr err_) \<and> allDistinct (pat_bindings p_ [])

goal (1 subgoal):
 1. \<forall>s'a r. (s'_, Rerr err_) = (s'a, r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s'a, r))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate ck_ env_ s_ e_ (s'_, Rerr err_); allDistinct (pat_bindings p_ [])\<rbrakk> \<Longrightarrow> \<forall>s'a r. (s'_, Rerr err_) = (s'a, r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s'a, r))
[PROOF STEP]
apply (drule add_clock(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>allDistinct (pat_bindings p_ []); \<forall>s'a r'. (s'_, Rerr err_) = (s'a, r') \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate True env_ (update_clock (\<lambda>_. c) s_) e_ (update_clock (\<lambda>_. 0) s'a, r'))\<rbrakk> \<Longrightarrow> \<forall>s'a r. (s'_, Rerr err_) = (s'a, r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s'a, r))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>allDistinct (pat_bindings p_ []); \<not> ck_; evaluate True env_ (update_clock (\<lambda>_. c) s_) e_ (update_clock (\<lambda>_. 0) s'_, Rerr err_)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s'_, Rerr err_)
[PROOF STEP]
by rule+ auto
[PROOF STATE]
proof (state)
this:
\<forall>s'a r. (s'_, Rerr err_) = (s'a, r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dlet locs_ p_ e_) (update_clock (\<lambda>_. 0) s'a, r))

goal (7 subgoals):
 1. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 2. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 3. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 4. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 5. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 6. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 7. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 2. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 3. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 4. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 5. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 6. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 7. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
case dletrec1
[PROOF STATE]
proof (state)
this:
allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs_)

goal (7 subgoals):
 1. \<And>ck mn env funs s locs. allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs) \<Longrightarrow> \<forall>s' r. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 2. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 3. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 4. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 5. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 6. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 7. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs_)

goal (1 subgoal):
 1. \<forall>s' r. (s_, Rval (make_sem_env (build_rec_env funs_ env_ nsEmpty) nsEmpty)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dletrec locs_ funs_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>allDistinct (map (\<lambda>x. case x of (x, a) \<Rightarrow> x) funs_); \<not> ck_\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dletrec locs_ funs_) (update_clock (\<lambda>_. 0) s_, Rval (make_sem_env (build_rec_env funs_ env_ nsEmpty) nsEmpty))
[PROOF STEP]
by rule+ auto
[PROOF STATE]
proof (state)
this:
\<forall>s' r. (s_, Rval (make_sem_env (build_rec_env funs_ env_ nsEmpty) nsEmpty)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dletrec locs_ funs_) (update_clock (\<lambda>_. 0) s', r))

goal (6 subgoals):
 1. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 2. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 3. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 4. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 5. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 6. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 2. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 3. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 4. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 5. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 6. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
case dletrec2
[PROOF STATE]
proof (state)
this:
\<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs_)

goal (6 subgoals):
 1. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) s', r))
 2. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 3. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 4. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 5. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 6. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs_)

goal (1 subgoal):
 1. \<forall>s' r. (s_, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dletrec locs_ funs_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> allDistinct (map (\<lambda>x. case x of (x, a) \<Rightarrow> x) funs_); \<not> ck_\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dletrec locs_ funs_) (update_clock (\<lambda>_. 0) s_, Rerr (Rabort Rtype_error))
[PROOF STEP]
by rule+ auto
[PROOF STATE]
proof (state)
this:
\<forall>s' r. (s_, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dletrec locs_ funs_) (update_clock (\<lambda>_. 0) s', r))

goal (5 subgoals):
 1. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 2. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 4. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 5. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 2. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 4. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 5. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[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 (5 subgoals):
 1. \<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. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 2. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 4. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 5. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[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. (update_defined_types (\<lambda>_. new_tdecs_ \<union> defined_types s_) s_, Rval (make_sem_env nsEmpty (build_tdefs mn_ tds_))) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dtype locs_ tds_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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_); \<not> ck_\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dtype locs_ tds_) (update_defined_types (\<lambda>_. type_defs_to_new_tdecs mn_ tds_ \<union> defined_types s_) (update_clock (\<lambda>_. 0) s_), Rval (make_sem_env nsEmpty (build_tdefs mn_ tds_)))
[PROOF STEP]
by (metis (full_types) evaluate_dec.dtype1 state.record_simps(4))
[PROOF STATE]
proof (state)
this:
\<forall>s' r. (update_defined_types (\<lambda>_. new_tdecs_ \<union> defined_types s_) s_, Rval (make_sem_env nsEmpty (build_tdefs mn_ tds_))) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dtype locs_ tds_) (update_clock (\<lambda>_. 0) s', r))

goal (4 subgoals):
 1. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 4. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 4. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
case dtype2
[PROOF STATE]
proof (state)
this:
\<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_)

goal (4 subgoals):
 1. \<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. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 4. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<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_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<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_)

goal (1 subgoal):
 1. \<forall>s' r. (s_, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dtype locs_ tds_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>disjnt (type_defs_to_new_tdecs mn_ tds_) (defined_types s_) \<longrightarrow> check_dup_ctors tds_ \<longrightarrow> \<not> allDistinct (map (\<lambda>(tvs, tn, ctors). tn) tds_); \<not> ck_\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dtype locs_ tds_) (update_clock (\<lambda>_. 0) s_, Rerr (Rabort Rtype_error))
[PROOF STEP]
by rule+ auto
[PROOF STATE]
proof (state)
this:
\<forall>s' r. (s_, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dtype locs_ tds_) (update_clock (\<lambda>_. 0) s', r))

goal (3 subgoals):
 1. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
case dtabbrev
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s' r. (s_, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dtabbrev locs_ tvs_ tn_ t0_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> ck_ \<Longrightarrow> \<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dtabbrev locs_ tvs_ tn_ t0_) (update_clock (\<lambda>_. 0) s_, Rval (make_sem_env nsEmpty nsEmpty))
[PROOF STEP]
by rule+
[PROOF STATE]
proof (state)
this:
\<forall>s' r. (s_, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dtabbrev locs_ tvs_ tn_ t0_) (update_clock (\<lambda>_. 0) s', r))

goal (2 subgoals):
 1. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
case dexn1
[PROOF STATE]
proof (state)
this:
TypeExn (mk_id mn_ cn_) \<notin> defined_types s_

goal (2 subgoals):
 1. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r. (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> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[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. (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> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dexn locs_ cn_ ts_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>TypeExn (mk_id mn_ cn_) \<notin> defined_types s_; \<not> ck_\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dexn locs_ cn_ ts_) (update_defined_types (\<lambda>_. insert (TypeExn (mk_id mn_ cn_)) (defined_types s_)) (update_clock (\<lambda>_. 0) s_), Rval (make_sem_env nsEmpty (nsSing cn_ (length ts_, TypeExn (mk_id mn_ cn_)))))
[PROOF STEP]
apply (rule exI[where x=0])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>TypeExn (mk_id mn_ cn_) \<notin> defined_types s_; \<not> ck_\<rbrakk> \<Longrightarrow> evaluate_dec True mn_ env_ (update_clock (\<lambda>_. 0) s_) (Dexn locs_ cn_ ts_) (update_defined_types (\<lambda>_. insert (TypeExn (mk_id mn_ cn_)) (defined_types s_)) (update_clock (\<lambda>_. 0) 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. \<lbrakk>TypeExn (mk_id mn_ cn_) \<notin> defined_types s_; \<not> ck_\<rbrakk> \<Longrightarrow> evaluate_dec True mn_ env_ (update_clock (\<lambda>_. 0) s_) (Dexn locs_ cn_ ts_) (update_defined_types (\<lambda>_. insert (TypeExn (mk_id mn_ cn_)) (defined_types s_)) (update_clock (\<lambda>_. 0) 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. (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> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dexn locs_ cn_ ts_) (update_clock (\<lambda>_. 0) s', r))

goal (1 subgoal):
 1. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
case dexn2
[PROOF STATE]
proof (state)
this:
TypeExn (mk_id mn_ cn_) \<in> defined_types s_

goal (1 subgoal):
 1. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
TypeExn (mk_id mn_ cn_) \<in> defined_types s_
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
TypeExn (mk_id mn_ cn_) \<in> defined_types s_

goal (1 subgoal):
 1. \<forall>s' r. (s_, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dexn locs_ cn_ ts_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>TypeExn (mk_id mn_ cn_) \<in> defined_types s_; \<not> ck_\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dexn locs_ cn_ ts_) (update_clock (\<lambda>_. 0) s_, Rerr (Rabort Rtype_error))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>TypeExn (mk_id mn_ cn_) \<in> defined_types s_; \<not> ck_\<rbrakk> \<Longrightarrow> evaluate_dec True mn_ env_ (update_clock (\<lambda>_. ?c4) s_) (Dexn locs_ cn_ ts_) (update_clock (\<lambda>_. 0) s_, Rerr (Rabort Rtype_error))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>TypeExn (mk_id mn_ cn_) \<in> defined_types s_; \<not> ck_\<rbrakk> \<Longrightarrow> TypeExn (mk_id mn_ cn_) \<in> defined_types (update_clock (\<lambda>_. 0) s_)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>s' r. (s_, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s_) (Dexn locs_ cn_ ts_) (update_clock (\<lambda>_. 0) s', r))

goal:
No subgoals!
[PROOF STEP]
qed