[STATEMENT]
lemma dec_add_to_counter:
  "evaluate_dec ck mn env s d res \<Longrightarrow>
   \<forall>s' r extra. res = (s',r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow>
     evaluate_dec True mn env (s (| clock := (clock   s) + extra |)) d ((s' (| clock := (clock   s') + extra |)),r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_dec ck mn env s d res \<Longrightarrow> \<forall>s' r extra. res = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) s', r)
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s', Rerr err) = (s'a, r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dlet locs p e) (update_clock (\<lambda>_. clock s'a + extra) 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 extra. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dletrec locs funs) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dletrec locs funs) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtype locs tds) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtype locs tds) (update_clock (\<lambda>_. clock s' + extra) s', r)
 10. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r extra. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. clock s' + extra) s', r)
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. 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 extra. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) s', r)
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s', Rerr err) = (s'a, r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dlet locs p e) (update_clock (\<lambda>_. clock s'a + extra) 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 extra. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dletrec locs funs) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dletrec locs funs) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (update_defined_types (\<lambda>_. new_tdecs \<union> defined_types s) s, Rval (make_sem_env nsEmpty (build_tdefs mn tds))) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtype locs tds) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtype locs tds) (update_clock (\<lambda>_. clock s' + extra) s', r)
 10. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r extra. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. clock s' + extra) s', r)
A total of 12 subgoals...
[PROOF STEP]
case dtype1
[PROOF STATE]
proof (state)
this:
check_dup_ctors tds_ \<and> new_tdecs_ = type_defs_to_new_tdecs mn_ tds_ \<and> disjnt new_tdecs_ (defined_types s_) \<and> allDistinct (map (\<lambda>x. case x of (tvs, tn, ctors) \<Rightarrow> tn) tds_)

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

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

goal (1 subgoal):
 1. \<And>extra. \<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_); ck_\<rbrakk> \<Longrightarrow> evaluate_dec True mn_ env_ (update_clock (\<lambda>_. clock s_ + extra) s_) (Dtype locs_ tds_) (update_defined_types (\<lambda>_. type_defs_to_new_tdecs mn_ tds_ \<union> defined_types s_) (update_clock (\<lambda>_. clock s_ + extra) s_), Rval (make_sem_env nsEmpty (build_tdefs mn_ tds_)))
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
\<forall>s' r extra. (update_defined_types (\<lambda>_. new_tdecs_ \<union> defined_types s_) s_, Rval (make_sem_env nsEmpty (build_tdefs mn_ tds_))) = (s', r) \<and> ck_ = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn_ env_ (update_clock (\<lambda>_. clock s_ + extra) s_) (Dtype locs_ tds_) (update_clock (\<lambda>_. clock s' + extra) s', r)

goal (11 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env' \<Longrightarrow> \<forall>s' r extra. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) s', r)
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s', Rerr err) = (s'a, r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dlet locs p e) (update_clock (\<lambda>_. clock s'a + extra) 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 extra. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dletrec locs funs) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dletrec locs funs) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtype locs tds) (update_clock (\<lambda>_. clock s' + extra) s', r)
 9. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r extra. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. clock s' + extra) s', r)
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r extra. (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 = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dexn locs cn ts) (update_clock (\<lambda>_. clock s' + extra) s', r)
A total of 11 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env' \<Longrightarrow> \<forall>s' r extra. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) s', r)
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s', Rerr err) = (s'a, r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dlet locs p e) (update_clock (\<lambda>_. clock s'a + extra) 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 extra. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dletrec locs funs) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dletrec locs funs) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtype locs tds) (update_clock (\<lambda>_. clock s' + extra) s', r)
 9. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r extra. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. clock s' + extra) s', r)
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r extra. (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 = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dexn locs cn ts) (update_clock (\<lambda>_. clock s' + extra) s', r)
A total of 11 subgoals...
[PROOF STEP]
case dexn1
[PROOF STATE]
proof (state)
this:
TypeExn (mk_id mn_ cn_) \<notin> defined_types s_

goal (11 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env' \<Longrightarrow> \<forall>s' r extra. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) s', r)
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s', Rerr err) = (s'a, r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dlet locs p e) (update_clock (\<lambda>_. clock s'a + extra) 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 extra. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dletrec locs funs) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dletrec locs funs) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtype locs tds) (update_clock (\<lambda>_. clock s' + extra) s', r)
 9. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r extra. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. clock s' + extra) s', r)
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<notin> defined_types s \<Longrightarrow> \<forall>s' r extra. (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 = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dexn locs cn ts) (update_clock (\<lambda>_. clock s' + extra) s', r)
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
TypeExn (mk_id mn_ cn_) \<notin> defined_types s_
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
TypeExn (mk_id mn_ cn_) \<notin> defined_types s_

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

goal (1 subgoal):
 1. \<And>extra. \<lbrakk>TypeExn (mk_id mn_ cn_) \<notin> defined_types s_; ck_\<rbrakk> \<Longrightarrow> evaluate_dec True mn_ env_ (update_clock (\<lambda>_. clock s_ + extra) s_) (Dexn locs_ cn_ ts_) (update_defined_types (\<lambda>_. insert (TypeExn (mk_id mn_ cn_)) (defined_types s_)) (update_clock (\<lambda>_. clock s_ + extra) 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 extra. (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_ = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn_ env_ (update_clock (\<lambda>_. clock s_ + extra) s_) (Dexn locs_ cn_ ts_) (update_clock (\<lambda>_. clock s' + extra) s', r)

goal (10 subgoals):
 1. \<And>ck mn env p e v1 env' s1 s2 locs. evaluate ck env s1 e (s2, Rval v1) \<and> allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s2) p v1 [] = Match env' \<Longrightarrow> \<forall>s' r extra. (s2, Rval (make_sem_env (alist_to_ns env') nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr (Rraise Bindv)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) s', r)
 4. \<And>ck mn env p e s locs. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<forall>s' r extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dlet locs p e) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s', Rerr err) = (s'a, r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dlet locs p e) (update_clock (\<lambda>_. clock s'a + extra) 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 extra. (s, Rval (make_sem_env (build_rec_env funs env nsEmpty) nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dletrec locs funs) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dletrec locs funs) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtype locs tds) (update_clock (\<lambda>_. clock s' + extra) s', r)
 9. \<And>ck mn env tvs tn t0 s locs. \<forall>s' r extra. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dtabbrev locs tvs tn t0) (update_clock (\<lambda>_. clock s' + extra) s', r)
 10. \<And>ck mn env cn ts s locs. TypeExn (mk_id mn cn) \<in> defined_types s \<Longrightarrow> \<forall>s' r extra. (s, Rerr (Rabort Rtype_error)) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec True mn env (update_clock (\<lambda>_. clock s + extra) s) (Dexn locs cn ts) (update_clock (\<lambda>_. clock s' + extra) s', r)
[PROOF STEP]
qed (force intro:evaluate_dec.intros simp add:add_to_counter(3))+


[STATEMENT]
lemma dec_unclocked_unchanged:
  "evaluate_dec ck mn env s d r \<Longrightarrow> ck = False \<Longrightarrow> (snd r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> (clock   s) = (clock   (fst r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate_dec ck mn env s d r; ck = False\<rbrakk> \<Longrightarrow> snd r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock (fst r)
[PROOF STEP]
by (induction rule: evaluate_dec.inducts)
     (auto simp: big_unclocked_notimeout big_clocked_unclocked_equiv)


[STATEMENT]
lemma dec_clocked_unclocked_equiv:
  "evaluate_dec False mn env s1 d (s2,r) =
  (\<exists>c. evaluate_dec True mn env (s1 (| clock := c |)) d ((s2 (| clock := 0 |)),r) \<and>
       r \<noteq> Rerr (Rabort Rtimeout_error) \<and> (clock   s1) = (clock   s2))" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_dec False mn env s1 d (s2, r) = (\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. evaluate_dec False mn env s1 d (s2, r) \<Longrightarrow> \<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2
 2. \<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2 \<Longrightarrow> evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
evaluate_dec False mn env s1 d (s2, r)

goal (2 subgoals):
 1. evaluate_dec False mn env s1 d (s2, r) \<Longrightarrow> \<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2
 2. \<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2 \<Longrightarrow> evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
evaluate_dec False mn env s1 d (s2, r)

goal (1 subgoal):
 1. \<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2
[PROOF STEP]
by (auto dest:dec_unclocked_unchanged dec_add_clock)
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2

goal (1 subgoal):
 1. \<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2 \<Longrightarrow> evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2 \<Longrightarrow> evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2

goal (1 subgoal):
 1. \<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2 \<Longrightarrow> evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2

goal (1 subgoal):
 1. evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
using dec_unclocked_ignore
[PROOF STATE]
proof (prove)
using this:
\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2
evaluate_dec ?ck ?mn ?env ?s ?d ?res \<Longrightarrow> \<forall>s' r count. ?res = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False ?mn ?env (update_clock (\<lambda>_. count) ?s) ?d (update_clock (\<lambda>_. count) s', r)

goal (1 subgoal):
 1. evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2; \<And>ck mn env s d res. evaluate_dec ck mn env s d res \<Longrightarrow> \<forall>s' r count. res = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) d (update_clock (\<lambda>_. count) s', r)\<rbrakk> \<Longrightarrow> evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
(* sledgehammer proof *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2; \<And>ck mn env s d res. evaluate_dec ck mn env s d res \<Longrightarrow> \<forall>s' r count. res = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) d (update_clock (\<lambda>_. count) s', r)\<rbrakk> \<Longrightarrow> evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
obtain nn :: nat where
      f1: "evaluate_dec True mn env (update_clock (\<lambda>n. nn) s1) d (update_clock (\<lambda>n. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>nn. evaluate_dec True mn env (update_clock (\<lambda>n. nn) s1) d (update_clock (\<lambda>n. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2

goal (1 subgoal):
 1. (\<And>nn. evaluate_dec True mn env (update_clock (\<lambda>n. nn) s1) d (update_clock (\<lambda>n. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
evaluate_dec True mn env (update_clock (\<lambda>n. nn) s1) d (update_clock (\<lambda>n. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2

goal (1 subgoal):
 1. \<lbrakk>\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2; \<And>ck mn env s d res. evaluate_dec ck mn env s d res \<Longrightarrow> \<forall>s' r count. res = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) d (update_clock (\<lambda>_. count) s', r)\<rbrakk> \<Longrightarrow> evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_dec True mn env (update_clock (\<lambda>n. nn) s1) d (update_clock (\<lambda>n. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2
[PROOF STEP]
have "\<forall>n. evaluate_dec False mn env (update_clock (\<lambda>na. n) s1) d (update_clock (\<lambda>na. n) s2, r)"
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True mn env (update_clock (\<lambda>n. nn) s1) d (update_clock (\<lambda>n. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2

goal (1 subgoal):
 1. \<forall>n. evaluate_dec False mn env (update_clock (\<lambda>na. n) s1) d (update_clock (\<lambda>na. n) s2, r)
[PROOF STEP]
using dec_unclocked_ignore
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True mn env (update_clock (\<lambda>n. nn) s1) d (update_clock (\<lambda>n. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2
evaluate_dec ?ck ?mn ?env ?s ?d ?res \<Longrightarrow> \<forall>s' r count. ?res = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False ?mn ?env (update_clock (\<lambda>_. count) ?s) ?d (update_clock (\<lambda>_. count) s', r)

goal (1 subgoal):
 1. \<forall>n. evaluate_dec False mn env (update_clock (\<lambda>na. n) s1) d (update_clock (\<lambda>na. n) s2, r)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>n. evaluate_dec False mn env (update_clock (\<lambda>na. n) s1) d (update_clock (\<lambda>na. n) s2, r)

goal (1 subgoal):
 1. \<lbrakk>\<exists>c. evaluate_dec True mn env (update_clock (\<lambda>_. c) s1) d (update_clock (\<lambda>_. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2; \<And>ck mn env s d res. evaluate_dec ck mn env s d res \<Longrightarrow> \<forall>s' r count. res = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False mn env (update_clock (\<lambda>_. count) s) d (update_clock (\<lambda>_. count) s', r)\<rbrakk> \<Longrightarrow> evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. evaluate_dec False mn env (update_clock (\<lambda>na. n) s1) d (update_clock (\<lambda>na. n) s2, r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n. evaluate_dec False mn env (update_clock (\<lambda>na. n) s1) d (update_clock (\<lambda>na. n) s2, r)

goal (1 subgoal):
 1. evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
\<forall>n. evaluate_dec False mn env (update_clock (\<lambda>na. n) s1) d (update_clock (\<lambda>na. n) s2, r)
evaluate_dec True mn env (update_clock (\<lambda>n. nn) s1) d (update_clock (\<lambda>n. 0) s2, r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s1 = clock s2

goal (1 subgoal):
 1. evaluate_dec False mn env s1 d (s2, r)
[PROOF STEP]
by (metis (full_types) state.record_simps(7))
[PROOF STATE]
proof (state)
this:
evaluate_dec False mn env s1 d (s2, r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
evaluate_dec False mn env s1 d (s2, r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma decs_add_clock:
  "evaluate_decs ck mn env s ds res \<Longrightarrow>
   \<forall>s' r. res = (s',r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (s (| clock := c |)) ds (s' (| clock := 0 |),r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_decs ck mn env s ds res \<Longrightarrow> \<forall>s' r. res = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
proof (induction rule:evaluate_decs.inducts)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ck mn env s. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s) [] (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn s1 s2 env d ds e. evaluate_dec ck mn env s1 d (s2, Rerr e) \<Longrightarrow> \<forall>s' r. (s2, Rerr e) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s1) (d # ds) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn s1 s2 s3 env d ds new_env r. evaluate_dec ck mn env s1 d (s2, Rval new_env) \<and> evaluate_decs ck mn (extend_dec_env new_env env) s2 ds (s3, r) \<and> (\<forall>s' ra. (s3, r) = (s', ra) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn (extend_dec_env new_env env) (update_clock (\<lambda>_. c) s2) ds (update_clock (\<lambda>_. 0) s', ra))) \<Longrightarrow> \<forall>s' ra. (s3, combine_dec_result new_env r) = (s', ra) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s1) (d # ds) (update_clock (\<lambda>_. 0) s', ra))
[PROOF STEP]
case cons1
[PROOF STATE]
proof (state)
this:
evaluate_dec ck_ mn_ env_ s1_ d_ (s2_, Rerr e_)

goal (3 subgoals):
 1. \<And>ck mn env s. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s) [] (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn s1 s2 env d ds e. evaluate_dec ck mn env s1 d (s2, Rerr e) \<Longrightarrow> \<forall>s' r. (s2, Rerr e) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s1) (d # ds) (update_clock (\<lambda>_. 0) s', r))
 3. \<And>ck mn s1 s2 s3 env d ds new_env r. evaluate_dec ck mn env s1 d (s2, Rval new_env) \<and> evaluate_decs ck mn (extend_dec_env new_env env) s2 ds (s3, r) \<and> (\<forall>s' ra. (s3, r) = (s', ra) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn (extend_dec_env new_env env) (update_clock (\<lambda>_. c) s2) ds (update_clock (\<lambda>_. 0) s', ra))) \<Longrightarrow> \<forall>s' ra. (s3, combine_dec_result new_env r) = (s', ra) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s1) (d # ds) (update_clock (\<lambda>_. 0) s', ra))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_dec ck_ mn_ env_ s1_ d_ (s2_, Rerr e_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
evaluate_dec ck_ mn_ env_ s1_ d_ (s2_, Rerr e_)

goal (1 subgoal):
 1. \<forall>s' r. (s2_, Rerr e_) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_decs True mn_ env_ (update_clock (\<lambda>_. c) s1_) (d_ # ds_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
using dec_add_clock evaluate_decs.cons1
[PROOF STATE]
proof (prove)
using this:
evaluate_dec ck_ mn_ env_ s1_ d_ (s2_, Rerr e_)
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))
evaluate_dec ?ck ?mn ?env ?s1.0 ?d (?s2.0, Rerr ?e) \<Longrightarrow> evaluate_decs ?ck ?mn ?env ?s1.0 (?d # ?ds) (?s2.0, Rerr ?e)

goal (1 subgoal):
 1. \<forall>s' r. (s2_, Rerr e_) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_decs True mn_ env_ (update_clock (\<lambda>_. c) s1_) (d_ # ds_) (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>s' r. (s2_, Rerr e_) = (s', r) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_decs True mn_ env_ (update_clock (\<lambda>_. c) s1_) (d_ # ds_) (update_clock (\<lambda>_. 0) s', r))

goal (2 subgoals):
 1. \<And>ck mn env s. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s) [] (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn s1 s2 s3 env d ds new_env r. evaluate_dec ck mn env s1 d (s2, Rval new_env) \<and> evaluate_decs ck mn (extend_dec_env new_env env) s2 ds (s3, r) \<and> (\<forall>s' ra. (s3, r) = (s', ra) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn (extend_dec_env new_env env) (update_clock (\<lambda>_. c) s2) ds (update_clock (\<lambda>_. 0) s', ra))) \<Longrightarrow> \<forall>s' ra. (s3, combine_dec_result new_env r) = (s', ra) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s1) (d # ds) (update_clock (\<lambda>_. 0) s', ra))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ck mn env s. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s) [] (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn s1 s2 s3 env d ds new_env r. evaluate_dec ck mn env s1 d (s2, Rval new_env) \<and> evaluate_decs ck mn (extend_dec_env new_env env) s2 ds (s3, r) \<and> (\<forall>s' ra. (s3, r) = (s', ra) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn (extend_dec_env new_env env) (update_clock (\<lambda>_. c) s2) ds (update_clock (\<lambda>_. 0) s', ra))) \<Longrightarrow> \<forall>s' ra. (s3, combine_dec_result new_env r) = (s', ra) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s1) (d # ds) (update_clock (\<lambda>_. 0) s', ra))
[PROOF STEP]
case cons2
[PROOF STATE]
proof (state)
this:
evaluate_dec ck_ mn_ env_ s1_ d_ (s2_, Rval new_env_) \<and> evaluate_decs ck_ mn_ (extend_dec_env new_env_ env_) s2_ ds_ (s3_, r_) \<and> (\<forall>s' ra. (s3_, r_) = (s', ra) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_decs True mn_ (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) ds_ (update_clock (\<lambda>_. 0) s', ra)))

goal (2 subgoals):
 1. \<And>ck mn env s. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s) [] (update_clock (\<lambda>_. 0) s', r))
 2. \<And>ck mn s1 s2 s3 env d ds new_env r. evaluate_dec ck mn env s1 d (s2, Rval new_env) \<and> evaluate_decs ck mn (extend_dec_env new_env env) s2 ds (s3, r) \<and> (\<forall>s' ra. (s3, r) = (s', ra) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn (extend_dec_env new_env env) (update_clock (\<lambda>_. c) s2) ds (update_clock (\<lambda>_. 0) s', ra))) \<Longrightarrow> \<forall>s' ra. (s3, combine_dec_result new_env r) = (s', ra) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s1) (d # ds) (update_clock (\<lambda>_. 0) s', ra))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_dec ck_ mn_ env_ s1_ d_ (s2_, Rval new_env_) \<and> evaluate_decs ck_ mn_ (extend_dec_env new_env_ env_) s2_ ds_ (s3_, r_) \<and> (\<forall>s' ra. (s3_, r_) = (s', ra) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_decs True mn_ (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) ds_ (update_clock (\<lambda>_. 0) s', ra)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
evaluate_dec ck_ mn_ env_ s1_ d_ (s2_, Rval new_env_) \<and> evaluate_decs ck_ mn_ (extend_dec_env new_env_ env_) s2_ ds_ (s3_, r_) \<and> (\<forall>s' ra. (s3_, r_) = (s', ra) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_decs True mn_ (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) ds_ (update_clock (\<lambda>_. 0) s', ra)))

goal (1 subgoal):
 1. \<forall>s' ra. (s3_, combine_dec_result new_env_ r_) = (s', ra) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_decs True mn_ env_ (update_clock (\<lambda>_. c) s1_) (d_ # ds_) (update_clock (\<lambda>_. 0) s', ra))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>evaluate_dec False mn_ env_ s1_ d_ (s2_, Rval new_env_); evaluate_decs False mn_ (extend_dec_env new_env_ env_) s2_ ds_ (s3_, r_); \<not> ck_; evaluate_decs True mn_ (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) ds_ (update_clock (\<lambda>_. 0) s3_, r_)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_decs True mn_ env_ (update_clock (\<lambda>_. c) s1_) (d_ # ds_) (update_clock (\<lambda>_. 0) s3_, combine_dec_result new_env_ r_)
[PROOF STEP]
apply (drule dec_add_clock)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>evaluate_decs False mn_ (extend_dec_env new_env_ env_) s2_ ds_ (s3_, r_); \<not> ck_; evaluate_decs True mn_ (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) ds_ (update_clock (\<lambda>_. 0) s3_, r_); \<forall>s' r. (s2_, Rval new_env_) = (s', r) \<and> False = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) d_ (update_clock (\<lambda>_. 0) s', r))\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_decs True mn_ env_ (update_clock (\<lambda>_. c) s1_) (d_ # ds_) (update_clock (\<lambda>_. 0) s3_, combine_dec_result new_env_ r_)
[PROOF STEP]
using dec_add_to_counter[rule_format] evaluate_decs.cons2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>evaluate_dec ?ck ?mn ?env ?s ?d ?res; ?res = (?s', ?r) \<and> ?ck = True \<and> ?r \<noteq> Rerr (Rabort Rtimeout_error)\<rbrakk> \<Longrightarrow> evaluate_dec True ?mn ?env (update_clock (\<lambda>_. clock ?s + ?extra) ?s) ?d (update_clock (\<lambda>_. clock ?s' + ?extra) ?s', ?r)
evaluate_dec ?ck ?mn ?env ?s1.0 ?d (?s2.0, Rval ?new_env) \<and> evaluate_decs ?ck ?mn (extend_dec_env ?new_env ?env) ?s2.0 ?ds (?s3.0, ?r) \<Longrightarrow> evaluate_decs ?ck ?mn ?env ?s1.0 (?d # ?ds) (?s3.0, combine_dec_result ?new_env ?r)

goal (1 subgoal):
 1. \<And>c. \<lbrakk>evaluate_decs False mn_ (extend_dec_env new_env_ env_) s2_ ds_ (s3_, r_); \<not> ck_; evaluate_decs True mn_ (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) ds_ (update_clock (\<lambda>_. 0) s3_, r_); \<forall>s' r. (s2_, Rval new_env_) = (s', r) \<and> False = False \<longrightarrow> (\<exists>c. evaluate_dec True mn_ env_ (update_clock (\<lambda>_. c) s1_) d_ (update_clock (\<lambda>_. 0) s', r))\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_decs True mn_ env_ (update_clock (\<lambda>_. c) s1_) (d_ # ds_) (update_clock (\<lambda>_. 0) s3_, combine_dec_result new_env_ r_)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>s' ra. (s3_, combine_dec_result new_env_ r_) = (s', ra) \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_decs True mn_ env_ (update_clock (\<lambda>_. c) s1_) (d_ # ds_) (update_clock (\<lambda>_. 0) s', ra))

goal (1 subgoal):
 1. \<And>ck mn env s. \<forall>s' r. (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_decs True mn env (update_clock (\<lambda>_. c) s) [] (update_clock (\<lambda>_. 0) s', r))
[PROOF STEP]
qed (auto intro:evaluate_decs.intros)


[STATEMENT]
lemma decs_evaluate_not_timeout:
  "evaluate_decs ck mn env s ds r \<Longrightarrow>
   \<forall>s' r'. ck = False \<and> r = (s',r') \<longrightarrow> r' \<noteq> Rerr (Rabort Rtimeout_error)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_decs ck mn env s ds r \<Longrightarrow> \<forall>s' r'. ck = False \<and> r = (s', r') \<longrightarrow> r' \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
by (induction rule:evaluate_decs.inducts)
     (case_tac r;fastforce dest:dec_evaluate_not_timeout)+


[STATEMENT]
lemma decs_unclocked_unchanged:
  "evaluate_decs ck mn env s ds r \<Longrightarrow>
   \<forall>s' r'. ck = False \<and> r = (s',r') \<longrightarrow> r' \<noteq> Rerr (Rabort Rtimeout_error) \<and> (clock   s) = (clock   s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_decs ck mn env s ds r \<Longrightarrow> \<forall>s' r'. ck = False \<and> r = (s', r') \<longrightarrow> r' \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
by (induction rule:evaluate_decs.inducts)
     (case_tac r;fastforce simp add:dec_unclocked_unchanged dest:dec_evaluate_not_timeout)+


[STATEMENT]
lemma decs_unclocked_ignore:
  "evaluate_decs ck mn env s d res \<Longrightarrow> \<forall>s' r count. res = (s',r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow>
    evaluate_decs False mn env (s (| clock := count |)) d ((s' (| clock := count |)),r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_decs ck mn env s d res \<Longrightarrow> \<forall>s' r count. res = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs False mn env (update_clock (\<lambda>_. count) s) d (update_clock (\<lambda>_. count) s', r)
[PROOF STEP]
by (induction rule:evaluate_decs.inducts)
     (auto intro!:evaluate_decs.intros simp add:dec_unclocked_ignore)


[STATEMENT]
lemma decs_unclocked_2:
  assumes "evaluate_decs False mn env (s (| clock := count1 |)) ds ((s' (| clock := count1 |)),r)"
  shows "evaluate_decs False mn env (s (| clock := count2 |)) ds ((s' (| clock := count2 |)),r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_decs False mn env (update_clock (\<lambda>_. count2) s) ds (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
using decs_unclocked_ignore[rule_format] assms decs_evaluate_not_timeout
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>evaluate_decs ?ck ?mn ?env ?s ?d ?res; ?res = (?s', ?r) \<and> ?r \<noteq> Rerr (Rabort Rtimeout_error)\<rbrakk> \<Longrightarrow> evaluate_decs False ?mn ?env (update_clock (\<lambda>_. ?count) ?s) ?d (update_clock (\<lambda>_. ?count) ?s', ?r)
evaluate_decs False mn env (update_clock (\<lambda>_. count1) s) ds (update_clock (\<lambda>_. count1) s', r)
evaluate_decs ?ck ?mn ?env ?s ?ds ?r \<Longrightarrow> \<forall>s' r'. ?ck = False \<and> ?r = (s', r') \<longrightarrow> r' \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. evaluate_decs False mn env (update_clock (\<lambda>_. count2) s) ds (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma decs_unclocked:
  "(evaluate_decs False mn env s ds (s',r) \<longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> (clock   s) = (clock   s')) \<and>
   (evaluate_decs False mn env (s (| clock := count1 |)) ds ((s' (| clock := count1 |)),r) =
   evaluate_decs False mn env (s (| clock := count2 |)) ds ((s' (| clock := count2 |)),r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (evaluate_decs False mn env s ds (s', r) \<longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s') \<and> evaluate_decs False mn env (update_clock (\<lambda>_. count1) s) ds (update_clock (\<lambda>_. count1) s', r) = evaluate_decs False mn env (update_clock (\<lambda>_. count2) s) ds (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
by (auto simp add:decs_unclocked_unchanged decs_unclocked_2)


[STATEMENT]
lemma not_evaluate_decs_timeout:
  assumes "\<forall>r. \<not>evaluate_decs False mn env s ds r"
  shows "\<exists>r. evaluate_decs True mn env s ds r \<and> (snd r) = Rerr (Rabort Rtimeout_error)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_decs True mn env s ds r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>r. \<not> evaluate_decs False mn env s ds r

goal (1 subgoal):
 1. \<exists>r. evaluate_decs True mn env s ds r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
proof (induction ds arbitrary:mn env s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>mn env s. \<forall>r. \<not> evaluate_decs False mn env s [] r \<Longrightarrow> \<exists>r. evaluate_decs True mn env s [] r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>a ds mn env s. \<lbrakk>\<And>mn env s. \<forall>r. \<not> evaluate_decs False mn env s ds r \<Longrightarrow> \<exists>r. evaluate_decs True mn env s ds r \<and> snd r = Rerr (Rabort Rtimeout_error); \<forall>r. \<not> evaluate_decs False mn env s (a # ds) r\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (a # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>r. \<not> evaluate_decs False mn env s [] r

goal (2 subgoals):
 1. \<And>mn env s. \<forall>r. \<not> evaluate_decs False mn env s [] r \<Longrightarrow> \<exists>r. evaluate_decs True mn env s [] r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>a ds mn env s. \<lbrakk>\<And>mn env s. \<forall>r. \<not> evaluate_decs False mn env s ds r \<Longrightarrow> \<exists>r. evaluate_decs True mn env s ds r \<and> snd r = Rerr (Rabort Rtimeout_error); \<forall>r. \<not> evaluate_decs False mn env s (a # ds) r\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (a # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>r. \<not> evaluate_decs False mn env s [] r
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>r. \<not> evaluate_decs False mn env s [] r

goal (1 subgoal):
 1. \<exists>r. evaluate_decs True mn env s [] r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
using assms evaluate_decs.intros
[PROOF STATE]
proof (prove)
using this:
\<forall>r. \<not> evaluate_decs False mn env s [] r
\<forall>r. \<not> evaluate_decs False mn env s ds r
evaluate_decs ?ck ?mn ?env ?s [] (?s, Rval (make_sem_env nsEmpty nsEmpty))
evaluate_dec ?ck ?mn ?env ?s1.0 ?d (?s2.0, Rerr ?e) \<Longrightarrow> evaluate_decs ?ck ?mn ?env ?s1.0 (?d # ?ds) (?s2.0, Rerr ?e)
evaluate_dec ?ck ?mn ?env ?s1.0 ?d (?s2.0, Rval ?new_env) \<and> evaluate_decs ?ck ?mn (extend_dec_env ?new_env ?env) ?s2.0 ?ds (?s3.0, ?r) \<Longrightarrow> evaluate_decs ?ck ?mn ?env ?s1.0 (?d # ?ds) (?s3.0, combine_dec_result ?new_env ?r)

goal (1 subgoal):
 1. \<exists>r. evaluate_decs True mn env s [] r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>r. evaluate_decs True mn env s [] r \<and> snd r = Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. \<And>a ds mn env s. \<lbrakk>\<And>mn env s. \<forall>r. \<not> evaluate_decs False mn env s ds r \<Longrightarrow> \<exists>r. evaluate_decs True mn env s ds r \<and> snd r = Rerr (Rabort Rtimeout_error); \<forall>r. \<not> evaluate_decs False mn env s (a # ds) r\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (a # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ds mn env s. \<lbrakk>\<And>mn env s. \<forall>r. \<not> evaluate_decs False mn env s ds r \<Longrightarrow> \<exists>r. evaluate_decs True mn env s ds r \<and> snd r = Rerr (Rabort Rtimeout_error); \<forall>r. \<not> evaluate_decs False mn env s (a # ds) r\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (a # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
case (Cons d ds)
[PROOF STATE]
proof (state)
this:
\<forall>r. \<not> evaluate_decs False ?mn ?env ?s ds r \<Longrightarrow> \<exists>r. evaluate_decs True ?mn ?env ?s ds r \<and> snd r = Rerr (Rabort Rtimeout_error)
\<forall>r. \<not> evaluate_decs False mn env s (d # ds) r

goal (1 subgoal):
 1. \<And>a ds mn env s. \<lbrakk>\<And>mn env s. \<forall>r. \<not> evaluate_decs False mn env s ds r \<Longrightarrow> \<exists>r. evaluate_decs True mn env s ds r \<and> snd r = Rerr (Rabort Rtimeout_error); \<forall>r. \<not> evaluate_decs False mn env s (a # ds) r\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (a # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
obtain s' r where d:"evaluate_dec True mn env s d (s',r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s' r. evaluate_dec True mn env s d (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dec_clocked_total
[PROOF STATE]
proof (prove)
using this:
\<exists>res. evaluate_dec True ?mn ?env ?s ?d res

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

goal (1 subgoal):
 1. \<And>a ds mn env s. \<lbrakk>\<And>mn env s. \<forall>r. \<not> evaluate_decs False mn env s ds r \<Longrightarrow> \<exists>r. evaluate_decs True mn env s ds r \<and> snd r = Rerr (Rabort Rtimeout_error); \<forall>r. \<not> evaluate_decs False mn env s (a # ds) r\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (a # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_dec True mn env s d (s', r)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True mn env s d (s', r)

goal (1 subgoal):
 1. \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>evaluate_dec True mn env s d (s', r); r = Rval x1\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x2. \<lbrakk>evaluate_dec True mn env s d (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
case (Rval new_env)
[PROOF STATE]
proof (state)
this:
r = Rval new_env

goal (2 subgoals):
 1. \<And>x1. \<lbrakk>evaluate_dec True mn env s d (s', r); r = Rval x1\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x2. \<lbrakk>evaluate_dec True mn env s d (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
have "\<not> evaluate_decs False mn (extend_dec_env new_env env) s' ds (s3, r)" for s3 r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> evaluate_decs False mn (extend_dec_env new_env env) s' ds (s3, r)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. evaluate_decs False mn (extend_dec_env new_env env) s' ds (s3, r) \<Longrightarrow> False
[PROOF STEP]
assume "evaluate_decs False mn (extend_dec_env new_env env) s' ds (s3, r)"
[PROOF STATE]
proof (state)
this:
evaluate_decs False mn (extend_dec_env new_env env) s' ds (s3, r)

goal (1 subgoal):
 1. evaluate_decs False mn (extend_dec_env new_env env) s' ds (s3, r) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_decs False mn (extend_dec_env new_env env) s' ds (s3, r)
[PROOF STEP]
have "evaluate_decs False mn (extend_dec_env new_env env) (s' \<lparr>clock := (clock s)\<rparr>) ds ((s3 \<lparr>clock := (clock s)\<rparr>), r)"
[PROOF STATE]
proof (prove)
using this:
evaluate_decs False mn (extend_dec_env new_env env) s' ds (s3, r)

goal (1 subgoal):
 1. evaluate_decs False mn (extend_dec_env new_env env) (update_clock (\<lambda>_. clock s) s') ds (update_clock (\<lambda>_. clock s) s3, r)
[PROOF STEP]
using decs_unclocked decs_unclocked_ignore
[PROOF STATE]
proof (prove)
using this:
evaluate_decs False mn (extend_dec_env new_env env) s' ds (s3, r)
(evaluate_decs False ?mn ?env ?s ?ds (?s', ?r) \<longrightarrow> ?r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock ?s = clock ?s') \<and> evaluate_decs False ?mn ?env (update_clock (\<lambda>_. ?count1.0) ?s) ?ds (update_clock (\<lambda>_. ?count1.0) ?s', ?r) = evaluate_decs False ?mn ?env (update_clock (\<lambda>_. ?count2.0) ?s) ?ds (update_clock (\<lambda>_. ?count2.0) ?s', ?r)
evaluate_decs ?ck ?mn ?env ?s ?d ?res \<Longrightarrow> \<forall>s' r count. ?res = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs False ?mn ?env (update_clock (\<lambda>_. count) ?s) ?d (update_clock (\<lambda>_. count) s', r)

goal (1 subgoal):
 1. evaluate_decs False mn (extend_dec_env new_env env) (update_clock (\<lambda>_. clock s) s') ds (update_clock (\<lambda>_. clock s) s3, r)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
evaluate_decs False mn (extend_dec_env new_env env) (update_clock (\<lambda>_. clock s) s') ds (update_clock (\<lambda>_. clock s) s3, r)

goal (1 subgoal):
 1. evaluate_decs False mn (extend_dec_env new_env env) s' ds (s3, r) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
evaluate_decs False mn (extend_dec_env new_env env) (update_clock (\<lambda>_. clock s) s') ds (update_clock (\<lambda>_. clock s) s3, r)

goal (1 subgoal):
 1. evaluate_decs False mn (extend_dec_env new_env env) s' ds (s3, r) \<Longrightarrow> False
[PROOF STEP]
from d
[PROOF STATE]
proof (chain)
picking this:
evaluate_dec True mn env s d (s', r__)
[PROOF STEP]
have "evaluate_dec False mn env s d ((s' \<lparr>clock := (clock s)\<rparr>), Rval new_env)"
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True mn env s d (s', r__)

goal (1 subgoal):
 1. evaluate_dec False mn env s d (update_clock (\<lambda>_. clock s) s', Rval new_env)
[PROOF STEP]
using dec_unclocked_ignore
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True mn env s d (s', r__)
evaluate_dec ?ck ?mn ?env ?s ?d ?res \<Longrightarrow> \<forall>s' r count. ?res = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False ?mn ?env (update_clock (\<lambda>_. count) ?s) ?d (update_clock (\<lambda>_. count) s', r)

goal (1 subgoal):
 1. evaluate_dec False mn env s d (update_clock (\<lambda>_. clock s) s', Rval new_env)
[PROOF STEP]
unfolding Rval
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True mn env s d (s', Rval new_env)
evaluate_dec ?ck ?mn ?env ?s ?d ?res \<Longrightarrow> \<forall>s' r count. ?res = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_dec False ?mn ?env (update_clock (\<lambda>_. count) ?s) ?d (update_clock (\<lambda>_. count) s', r)

goal (1 subgoal):
 1. evaluate_dec False mn env s d (update_clock (\<lambda>_. clock s) s', Rval new_env)
[PROOF STEP]
by (metis (full_types) result.distinct(1) state.record_simps(7))
[PROOF STATE]
proof (state)
this:
evaluate_dec False mn env s d (update_clock (\<lambda>_. clock s) s', Rval new_env)

goal (1 subgoal):
 1. evaluate_decs False mn (extend_dec_env new_env env) s' ds (s3, r) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
evaluate_decs False mn (extend_dec_env new_env env) (update_clock (\<lambda>_. clock s) s') ds (update_clock (\<lambda>_. clock s) s3, r)
evaluate_dec False mn env s d (update_clock (\<lambda>_. clock s) s', Rval new_env)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
evaluate_decs False mn (extend_dec_env new_env env) (update_clock (\<lambda>_. clock s) s') ds (update_clock (\<lambda>_. clock s) s3, r)
evaluate_dec False mn env s d (update_clock (\<lambda>_. clock s) s', Rval new_env)

goal (1 subgoal):
 1. False
[PROOF STEP]
using evaluate_decs.cons2 Cons
[PROOF STATE]
proof (prove)
using this:
evaluate_decs False mn (extend_dec_env new_env env) (update_clock (\<lambda>_. clock s) s') ds (update_clock (\<lambda>_. clock s) s3, r)
evaluate_dec False mn env s d (update_clock (\<lambda>_. clock s) s', Rval new_env)
evaluate_dec ?ck ?mn ?env ?s1.0 ?d (?s2.0, Rval ?new_env) \<and> evaluate_decs ?ck ?mn (extend_dec_env ?new_env ?env) ?s2.0 ?ds (?s3.0, ?r) \<Longrightarrow> evaluate_decs ?ck ?mn ?env ?s1.0 (?d # ?ds) (?s3.0, combine_dec_result ?new_env ?r)
\<forall>r. \<not> evaluate_decs False ?mn ?env ?s ds r \<Longrightarrow> \<exists>r. evaluate_decs True ?mn ?env ?s ds r \<and> snd r = Rerr (Rabort Rtimeout_error)
\<forall>r. \<not> evaluate_decs False mn env s (d # ds) r

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> evaluate_decs False mn (extend_dec_env new_env env) s' ds (?s3.0, ?r)

goal (2 subgoals):
 1. \<And>x1. \<lbrakk>evaluate_dec True mn env s d (s', r); r = Rval x1\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x2. \<lbrakk>evaluate_dec True mn env s d (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> evaluate_decs False mn (extend_dec_env new_env env) s' ds (?s3.0, ?r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> evaluate_decs False mn (extend_dec_env new_env env) s' ds (?s3.0, ?r)

goal (1 subgoal):
 1. \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
using Cons.IH[simplified] evaluate_decs.cons2 d
[PROOF STATE]
proof (prove)
using this:
\<not> evaluate_decs False mn (extend_dec_env new_env env) s' ds (?s3.0, ?r)
\<forall>a b. \<not> evaluate_decs False ?mn ?env ?s ds (a, b) \<Longrightarrow> \<exists>a. evaluate_decs True ?mn ?env ?s ds (a, Rerr (Rabort Rtimeout_error))
evaluate_dec ?ck ?mn ?env ?s1.0 ?d (?s2.0, Rval ?new_env) \<and> evaluate_decs ?ck ?mn (extend_dec_env ?new_env ?env) ?s2.0 ?ds (?s3.0, ?r) \<Longrightarrow> evaluate_decs ?ck ?mn ?env ?s1.0 (?d # ?ds) (?s3.0, combine_dec_result ?new_env ?r)
evaluate_dec True mn env s d (s', r)

goal (1 subgoal):
 1. \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
unfolding Rval
[PROOF STATE]
proof (prove)
using this:
\<not> evaluate_decs False mn (extend_dec_env new_env env) s' ds (?s3.0, ?r)
\<forall>a b. \<not> evaluate_decs False ?mn ?env ?s ds (a, b) \<Longrightarrow> \<exists>a. evaluate_decs True ?mn ?env ?s ds (a, Rerr (Rabort Rtimeout_error))
evaluate_dec ?ck ?mn ?env ?s1.0 ?d (?s2.0, Rval ?new_env) \<and> evaluate_decs ?ck ?mn (extend_dec_env ?new_env ?env) ?s2.0 ?ds (?s3.0, ?r) \<Longrightarrow> evaluate_decs ?ck ?mn ?env ?s1.0 (?d # ?ds) (?s3.0, combine_dec_result ?new_env ?r)
evaluate_dec True mn env s d (s', Rval new_env)

goal (1 subgoal):
 1. \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
by (metis combine_dec_result.simps(1) snd_conv)
[PROOF STATE]
proof (state)
this:
\<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evaluate_dec True mn env s d (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evaluate_dec True mn env s d (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
case (Rerr e)
[PROOF STATE]
proof (state)
this:
r = Rerr e

goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evaluate_dec True mn env s d (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
have "e = Rabort Rtimeout_error"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e = Rabort Rtimeout_error
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e \<noteq> Rabort Rtimeout_error \<Longrightarrow> False
[PROOF STEP]
assume "e \<noteq> Rabort Rtimeout_error"
[PROOF STATE]
proof (state)
this:
e \<noteq> Rabort Rtimeout_error

goal (1 subgoal):
 1. e \<noteq> Rabort Rtimeout_error \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e \<noteq> Rabort Rtimeout_error
[PROOF STEP]
obtain s' where "evaluate_dec False mn env s d (s',r)"
[PROOF STATE]
proof (prove)
using this:
e \<noteq> Rabort Rtimeout_error

goal (1 subgoal):
 1. (\<And>s'. evaluate_dec False mn env s d (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dec_unclocked_ignore[rule_format, where count="clock s"] d Rerr state.simps
[PROOF STATE]
proof (prove)
using this:
e \<noteq> Rabort Rtimeout_error
\<lbrakk>evaluate_dec ?ck ?mn ?env ?s ?d ?res; ?res = (?s', ?r) \<and> ?r \<noteq> Rerr (Rabort Rtimeout_error)\<rbrakk> \<Longrightarrow> evaluate_dec False ?mn ?env (update_clock (\<lambda>_. clock s) ?s) ?d (update_clock (\<lambda>_. clock s) ?s', ?r)
evaluate_dec True mn env s d (s', r)
r = Rerr e
(make_state ?x1.0 ?x2.0 ?x3.0 ?x4.0 ?x5.0 = make_state ?y1.0 ?y2.0 ?y3.0 ?y4.0 ?y5.0) = (?x1.0 = ?y1.0 \<and> ?x2.0 = ?y2.0 \<and> ?x3.0 = ?y3.0 \<and> ?x4.0 = ?y4.0 \<and> ?x5.0 = ?y5.0)
(case make_state ?x1.0 ?x2.0 ?x3.0 ?x4.0 ?x5.0 of make_state x xa xb xc xd \<Rightarrow> ?f x xa xb xc xd) = ?f ?x1.0 ?x2.0 ?x3.0 ?x4.0 ?x5.0
rec_state ?f (make_state ?x1.0 ?x2.0 ?x3.0 ?x4.0 ?x5.0) = ?f ?x1.0 ?x2.0 ?x3.0 ?x4.0 ?x5.0

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

goal (1 subgoal):
 1. e \<noteq> Rabort Rtimeout_error \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
evaluate_dec False mn env s d (s', r)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding Rerr
[PROOF STATE]
proof (prove)
using this:
evaluate_dec False mn env s d (s', Rerr e)

goal (1 subgoal):
 1. False
[PROOF STEP]
using Cons evaluate_decs.cons1
[PROOF STATE]
proof (prove)
using this:
evaluate_dec False mn env s d (s', Rerr e)
\<forall>r. \<not> evaluate_decs False ?mn ?env ?s ds r \<Longrightarrow> \<exists>r. evaluate_decs True ?mn ?env ?s ds r \<and> snd r = Rerr (Rabort Rtimeout_error)
\<forall>r. \<not> evaluate_decs False mn env s (d # ds) r
evaluate_dec ?ck ?mn ?env ?s1.0 ?d (?s2.0, Rerr ?e) \<Longrightarrow> evaluate_decs ?ck ?mn ?env ?s1.0 (?d # ?ds) (?s2.0, Rerr ?e)

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
e = Rabort Rtimeout_error

goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evaluate_dec True mn env s d (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = Rabort Rtimeout_error
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e = Rabort Rtimeout_error

goal (1 subgoal):
 1. \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
using d evaluate_decs.cons1 Rerr
[PROOF STATE]
proof (prove)
using this:
e = Rabort Rtimeout_error
evaluate_dec True mn env s d (s', r)
evaluate_dec ?ck ?mn ?env ?s1.0 ?d (?s2.0, Rerr ?e) \<Longrightarrow> evaluate_decs ?ck ?mn ?env ?s1.0 (?d # ?ds) (?s2.0, Rerr ?e)
r = Rerr e

goal (1 subgoal):
 1. \<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>r. evaluate_decs True mn env s (d # ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma decs_clocked_total: "\<exists>res. evaluate_decs True mn env s ds res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>res. evaluate_decs True mn env s ds res
[PROOF STEP]
proof (induction ds arbitrary:mn env s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>mn env s. Ex (evaluate_decs True mn env s [])
 2. \<And>a ds mn env s. (\<And>mn env s. Ex (evaluate_decs True mn env s ds)) \<Longrightarrow> Ex (evaluate_decs True mn env s (a # ds))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>mn env s. Ex (evaluate_decs True mn env s [])
 2. \<And>a ds mn env s. (\<And>mn env s. Ex (evaluate_decs True mn env s ds)) \<Longrightarrow> Ex (evaluate_decs True mn env s (a # ds))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. evaluate_decs True mn env s [] a
[PROOF STEP]
by (auto intro:evaluate_decs.intros)
[PROOF STATE]
proof (state)
this:
\<exists>a. evaluate_decs True mn env s [] a

goal (1 subgoal):
 1. \<And>a ds mn env s. (\<And>mn env s. Ex (evaluate_decs True mn env s ds)) \<Longrightarrow> Ex (evaluate_decs True mn env s (a # ds))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ds mn env s. (\<And>mn env s. Ex (evaluate_decs True mn env s ds)) \<Longrightarrow> Ex (evaluate_decs True mn env s (a # ds))
[PROOF STEP]
case (Cons d ds)
[PROOF STATE]
proof (state)
this:
\<exists>a. evaluate_decs True ?mn ?env ?s ds a

goal (1 subgoal):
 1. \<And>a ds mn env s. (\<And>mn env s. Ex (evaluate_decs True mn env s ds)) \<Longrightarrow> Ex (evaluate_decs True mn env s (a # ds))
[PROOF STEP]
obtain s' r where d:"evaluate_dec True mn env s d (s',r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s' r. evaluate_dec True mn env s d (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dec_clocked_total
[PROOF STATE]
proof (prove)
using this:
\<exists>res. evaluate_dec True ?mn ?env ?s ?d res

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

goal (1 subgoal):
 1. \<And>a ds mn env s. (\<And>mn env s. Ex (evaluate_decs True mn env s ds)) \<Longrightarrow> Ex (evaluate_decs True mn env s (a # ds))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_dec True mn env s d (s', r)
[PROOF STEP]
obtain s'' r' where ds:"evaluate_decs True mn env s' ds (s'',r')"
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True mn env s d (s', r)

goal (1 subgoal):
 1. (\<And>s'' r'. evaluate_decs True mn env s' ds (s'', r') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True mn env s d (s', r)
\<exists>a. evaluate_decs True ?mn ?env ?s ds a

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

goal (1 subgoal):
 1. \<And>a ds mn env s. (\<And>mn env s. Ex (evaluate_decs True mn env s ds)) \<Longrightarrow> Ex (evaluate_decs True mn env s (a # ds))
[PROOF STEP]
from d ds
[PROOF STATE]
proof (chain)
picking this:
evaluate_dec True mn env s d (s', r)
evaluate_decs True mn env s' ds (s'', r')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True mn env s d (s', r)
evaluate_decs True mn env s' ds (s'', r')

goal (1 subgoal):
 1. \<exists>a. evaluate_decs True mn env s (d # ds) a
[PROOF STEP]
using evaluate_decs.intros Cons
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True mn env s d (s', r)
evaluate_decs True mn env s' ds (s'', r')
evaluate_decs ?ck ?mn ?env ?s [] (?s, Rval (make_sem_env nsEmpty nsEmpty))
evaluate_dec ?ck ?mn ?env ?s1.0 ?d (?s2.0, Rerr ?e) \<Longrightarrow> evaluate_decs ?ck ?mn ?env ?s1.0 (?d # ?ds) (?s2.0, Rerr ?e)
evaluate_dec ?ck ?mn ?env ?s1.0 ?d (?s2.0, Rval ?new_env) \<and> evaluate_decs ?ck ?mn (extend_dec_env ?new_env ?env) ?s2.0 ?ds (?s3.0, ?r) \<Longrightarrow> evaluate_decs ?ck ?mn ?env ?s1.0 (?d # ?ds) (?s3.0, combine_dec_result ?new_env ?r)
\<exists>a. evaluate_decs True ?mn ?env ?s ds a

goal (1 subgoal):
 1. \<exists>a. evaluate_decs True mn env s (d # ds) a
[PROOF STEP]
by (cases r;fastforce)+
[PROOF STATE]
proof (state)
this:
\<exists>a. evaluate_decs True mn env s (d # ds) a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma decs_clock_monotone:
  "evaluate_decs ck mn env s d res \<Longrightarrow> ck = True \<Longrightarrow> (clock (fst res)) \<le> (clock s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate_decs ck mn env s d res; ck = True\<rbrakk> \<Longrightarrow> clock (fst res) \<le> clock s
[PROOF STEP]
by (induction rule:evaluate_decs.inducts) (fastforce dest:dec_clock_monotone)+