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

goal (12 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env'; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty))), snd (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)))
 2. \<And>ck mn env p e v1 s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = No_match; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rerr (Rraise Bindv)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rerr (Rraise Bindv))), snd (s2, Rerr (Rraise Bindv)))
 3. \<And>ck mn env p e v1 s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match_type_error; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rerr (Rabort Rtype_error)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rerr (Rabort Rtype_error))), snd (s2, Rerr (Rabort Rtype_error)))
 4. \<And>ck mn env p e s locs. \<lbrakk>\<not> allDistinct (pat_bindings p []); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 5. \<And>ck mn env p e err s s' locs. \<lbrakk>evaluate ck env s e (s', Rerr err) \<and> allDistinct (pat_bindings p []); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s', Rerr err))) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s', Rerr err)), snd (s', Rerr err))
 6. \<And>ck mn env funs s locs. \<lbrakk>allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)))) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) (fst (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty))), snd (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)))
 7. \<And>ck mn env funs s locs. \<lbrakk>\<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 8. \<And>ck mn env tds s new_tdecs locs. \<lbrakk>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); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))))) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) (fst (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds)))), snd (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))))
 9. \<And>ck mn env tds s locs. \<lbrakk>\<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); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 10. \<And>ck mn env tvs tn t0 s locs. ck = True \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rval (make_sem_env nsEmpty nsEmpty)))) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) (fst (s, Rval (make_sem_env nsEmpty nsEmpty))), snd (s, Rval (make_sem_env nsEmpty nsEmpty)))
A total of 12 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
check_dup_ctors tds_ \<and> new_tdecs_ = type_defs_to_new_tdecs mn_ tds_ \<and> disjnt new_tdecs_ (defined_types s_) \<and> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds_)
ck_ = True
[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_)
ck_ = True

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

goal (1 subgoal):
 1. \<lbrakk>ck_; check_dup_ctors tds_; new_tdecs_ = type_defs_to_new_tdecs mn_ tds_; disjnt (type_defs_to_new_tdecs mn_ tds_) (defined_types s_); allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds_)\<rbrakk> \<Longrightarrow> evaluate_dec True mn_ env_ (update_clock (\<lambda>_. 0) 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
[PROOF STATE]
proof (state)
this:
evaluate_dec ck_ mn_ env_ (update_clock (\<lambda>_. clock s_ - clock (fst (update_defined_types (\<lambda>_. new_tdecs_ \<union> defined_types s_) s_, Rval (make_sem_env nsEmpty (build_tdefs mn_ tds_))))) s_) (Dtype locs_ tds_) (update_clock (\<lambda>_. 0) (fst (update_defined_types (\<lambda>_. new_tdecs_ \<union> defined_types s_) s_, Rval (make_sem_env nsEmpty (build_tdefs mn_ tds_)))), snd (update_defined_types (\<lambda>_. new_tdecs_ \<union> defined_types s_) s_, Rval (make_sem_env nsEmpty (build_tdefs mn_ tds_))))

goal (11 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env'; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty))), snd (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)))
 2. \<And>ck mn env p e v1 s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = No_match; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rerr (Rraise Bindv)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rerr (Rraise Bindv))), snd (s2, Rerr (Rraise Bindv)))
 3. \<And>ck mn env p e v1 s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match_type_error; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rerr (Rabort Rtype_error)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rerr (Rabort Rtype_error))), snd (s2, Rerr (Rabort Rtype_error)))
 4. \<And>ck mn env p e s locs. \<lbrakk>\<not> allDistinct (pat_bindings p []); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 5. \<And>ck mn env p e err s s' locs. \<lbrakk>evaluate ck env s e (s', Rerr err) \<and> allDistinct (pat_bindings p []); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s', Rerr err))) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s', Rerr err)), snd (s', Rerr err))
 6. \<And>ck mn env funs s locs. \<lbrakk>allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)))) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) (fst (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty))), snd (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)))
 7. \<And>ck mn env funs s locs. \<lbrakk>\<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 8. \<And>ck mn env tds s locs. \<lbrakk>\<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); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 9. \<And>ck mn env tvs tn t0 s locs. ck = True \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rval (make_sem_env nsEmpty nsEmpty)))) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) (fst (s, Rval (make_sem_env nsEmpty nsEmpty))), snd (s, Rval (make_sem_env nsEmpty nsEmpty)))
 10. \<And>ck mn env cn ts s locs. \<lbrakk>TypeExn (mk_id mn cn) \<notin> defined_types s; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (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) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) (fst (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)))))), snd (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))))))
A total of 11 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env'; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty))), snd (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)))
 2. \<And>ck mn env p e v1 s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = No_match; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rerr (Rraise Bindv)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rerr (Rraise Bindv))), snd (s2, Rerr (Rraise Bindv)))
 3. \<And>ck mn env p e v1 s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match_type_error; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rerr (Rabort Rtype_error)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rerr (Rabort Rtype_error))), snd (s2, Rerr (Rabort Rtype_error)))
 4. \<And>ck mn env p e s locs. \<lbrakk>\<not> allDistinct (pat_bindings p []); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 5. \<And>ck mn env p e err s s' locs. \<lbrakk>evaluate ck env s e (s', Rerr err) \<and> allDistinct (pat_bindings p []); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s', Rerr err))) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s', Rerr err)), snd (s', Rerr err))
 6. \<And>ck mn env funs s locs. \<lbrakk>allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)))) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) (fst (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty))), snd (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)))
 7. \<And>ck mn env funs s locs. \<lbrakk>\<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 8. \<And>ck mn env tds s locs. \<lbrakk>\<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); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 9. \<And>ck mn env tvs tn t0 s locs. ck = True \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rval (make_sem_env nsEmpty nsEmpty)))) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) (fst (s, Rval (make_sem_env nsEmpty nsEmpty))), snd (s, Rval (make_sem_env nsEmpty nsEmpty)))
 10. \<And>ck mn env cn ts s locs. \<lbrakk>TypeExn (mk_id mn cn) \<notin> defined_types s; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (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) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) (fst (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)))))), snd (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))))))
A total of 11 subgoals...
[PROOF STEP]
case dexn1
[PROOF STATE]
proof (state)
this:
TypeExn (mk_id mn_ cn_) \<notin> defined_types s_
ck_ = True

goal (11 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env'; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty))), snd (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)))
 2. \<And>ck mn env p e v1 s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = No_match; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rerr (Rraise Bindv)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rerr (Rraise Bindv))), snd (s2, Rerr (Rraise Bindv)))
 3. \<And>ck mn env p e v1 s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match_type_error; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rerr (Rabort Rtype_error)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rerr (Rabort Rtype_error))), snd (s2, Rerr (Rabort Rtype_error)))
 4. \<And>ck mn env p e s locs. \<lbrakk>\<not> allDistinct (pat_bindings p []); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 5. \<And>ck mn env p e err s s' locs. \<lbrakk>evaluate ck env s e (s', Rerr err) \<and> allDistinct (pat_bindings p []); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s', Rerr err))) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s', Rerr err)), snd (s', Rerr err))
 6. \<And>ck mn env funs s locs. \<lbrakk>allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)))) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) (fst (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty))), snd (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)))
 7. \<And>ck mn env funs s locs. \<lbrakk>\<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 8. \<And>ck mn env tds s locs. \<lbrakk>\<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); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 9. \<And>ck mn env tvs tn t0 s locs. ck = True \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rval (make_sem_env nsEmpty nsEmpty)))) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) (fst (s, Rval (make_sem_env nsEmpty nsEmpty))), snd (s, Rval (make_sem_env nsEmpty nsEmpty)))
 10. \<And>ck mn env cn ts s locs. \<lbrakk>TypeExn (mk_id mn cn) \<notin> defined_types s; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (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) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) (fst (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)))))), snd (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))))))
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
TypeExn (mk_id mn_ cn_) \<notin> defined_types s_
ck_ = True
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
TypeExn (mk_id mn_ cn_) \<notin> defined_types s_
ck_ = True

goal (1 subgoal):
 1. evaluate_dec ck_ mn_ env_ (update_clock (\<lambda>_. clock s_ - clock (fst (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_) (Dexn locs_ cn_ ts_) (update_clock (\<lambda>_. 0) (fst (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_)))))), snd (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_))))))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>TypeExn (mk_id mn_ cn_) \<notin> defined_types s_; 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_; 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:
evaluate_dec ck_ mn_ env_ (update_clock (\<lambda>_. clock s_ - clock (fst (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_) (Dexn locs_ cn_ ts_) (update_clock (\<lambda>_. 0) (fst (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_)))))), snd (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_))))))

goal (10 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env'; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty))), snd (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)))
 2. \<And>ck mn env p e v1 s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = No_match; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rerr (Rraise Bindv)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rerr (Rraise Bindv))), snd (s2, Rerr (Rraise Bindv)))
 3. \<And>ck mn env p e v1 s1 s2 locs. \<lbrakk>evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match_type_error; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s1 - clock (fst (s2, Rerr (Rabort Rtype_error)))) s1) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s2, Rerr (Rabort Rtype_error))), snd (s2, Rerr (Rabort Rtype_error)))
 4. \<And>ck mn env p e s locs. \<lbrakk>\<not> allDistinct (pat_bindings p []); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 5. \<And>ck mn env p e err s s' locs. \<lbrakk>evaluate ck env s e (s', Rerr err) \<and> allDistinct (pat_bindings p []); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s', Rerr err))) s) (Dlet locs p e) (update_clock (\<lambda>_. 0) (fst (s', Rerr err)), snd (s', Rerr err))
 6. \<And>ck mn env funs s locs. \<lbrakk>allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)))) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) (fst (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty))), snd (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)))
 7. \<And>ck mn env funs s locs. \<lbrakk>\<not> allDistinct (map (\<lambda>x. case x of (x, y, z) \<Rightarrow> x) funs); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dletrec locs funs) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 8. \<And>ck mn env tds s locs. \<lbrakk>\<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); ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dtype locs tds) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
 9. \<And>ck mn env tvs tn t0 s locs. ck = True \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rval (make_sem_env nsEmpty nsEmpty)))) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. 0) (fst (s, Rval (make_sem_env nsEmpty nsEmpty))), snd (s, Rval (make_sem_env nsEmpty nsEmpty)))
 10. \<And>ck mn env cn ts s locs. \<lbrakk>TypeExn (mk_id mn cn) \<in> defined_types s; ck = True\<rbrakk> \<Longrightarrow> evaluate_dec ck mn env (update_clock (\<lambda>_. clock s - clock (fst (s, Rerr (Rabort Rtype_error)))) s) (Dexn locs cn ts) (update_clock (\<lambda>_. 0) (fst (s, Rerr (Rabort Rtype_error))), snd (s, Rerr (Rabort Rtype_error)))
[PROOF STEP]
qed (force intro:evaluate_dec.intros simp add:clocked_min_counter)+