[STATEMENT]
lemma decs_sub_from_counter:
  "evaluate_decs ck mn env s d res \<Longrightarrow>
  \<forall>extra count count' s' r'.
    (clock s) = count + extra \<and> (clock s') = count' + extra \<and>
    res = (s',r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn env (s \<lparr> clock := count \<rparr>) d ((s' \<lparr> clock := count' \<rparr>),r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_decs ck mn env s d res \<Longrightarrow> \<forall>extra count count' s' r'. clock s = count + extra \<and> clock s' = count' + extra \<and> res = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn env (update_clock (\<lambda>_. count) s) d (update_clock (\<lambda>_. count') s', r')
[PROOF STEP]
proof (induction rule:evaluate_decs.inducts)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ck mn env s. \<forall>extra count count' s' r'. clock s = count + extra \<and> clock s' = count' + extra \<and> (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn env (update_clock (\<lambda>_. count) s) [] (update_clock (\<lambda>_. count') s', r')
 2. \<And>ck mn s1 s2 env d ds e. evaluate_dec ck mn env s1 d (s2, Rerr e) \<Longrightarrow> \<forall>extra count count' s' r'. clock s1 = count + extra \<and> clock s' = count' + extra \<and> (s2, Rerr e) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn env (update_clock (\<lambda>_. count) s1) (d # ds) (update_clock (\<lambda>_. count') 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>extra count count' s' r'. clock s2 = count + extra \<and> clock s' = count' + extra \<and> (s3, r) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn (extend_dec_env new_env env) (update_clock (\<lambda>_. count) s2) ds (update_clock (\<lambda>_. count') s', r')) \<Longrightarrow> \<forall>extra count count' s' r'. clock s1 = count + extra \<and> clock s' = count' + extra \<and> (s3, combine_dec_result new_env r) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn env (update_clock (\<lambda>_. count) s1) (d # ds) (update_clock (\<lambda>_. count') s', r')
[PROOF STEP]
case (cons2 ck mn s1 s2 s3 env d ds new_env r)
[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>extra count count' s' r'. clock s2 = count + extra \<and> clock s' = count' + extra \<and> (s3, r) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn (extend_dec_env new_env env) (update_clock (\<lambda>_. count) s2) ds (update_clock (\<lambda>_. count') s', r'))

goal (3 subgoals):
 1. \<And>ck mn env s. \<forall>extra count count' s' r'. clock s = count + extra \<and> clock s' = count' + extra \<and> (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn env (update_clock (\<lambda>_. count) s) [] (update_clock (\<lambda>_. count') s', r')
 2. \<And>ck mn s1 s2 env d ds e. evaluate_dec ck mn env s1 d (s2, Rerr e) \<Longrightarrow> \<forall>extra count count' s' r'. clock s1 = count + extra \<and> clock s' = count' + extra \<and> (s2, Rerr e) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn env (update_clock (\<lambda>_. count) s1) (d # ds) (update_clock (\<lambda>_. count') 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>extra count count' s' r'. clock s2 = count + extra \<and> clock s' = count' + extra \<and> (s3, r) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn (extend_dec_env new_env env) (update_clock (\<lambda>_. count) s2) ds (update_clock (\<lambda>_. count') s', r')) \<Longrightarrow> \<forall>extra count count' s' r'. clock s1 = count + extra \<and> clock s' = count' + extra \<and> (s3, combine_dec_result new_env r) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn env (update_clock (\<lambda>_. count) s1) (d # ds) (update_clock (\<lambda>_. count') s', r')
[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>extra count count' s' r'. clock s2 = count + extra \<and> clock s' = count' + extra \<and> (s3, r) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn (extend_dec_env new_env env) (update_clock (\<lambda>_. count) s2) ds (update_clock (\<lambda>_. count') s', r'))
[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>extra count count' s' r'. clock s2 = count + extra \<and> clock s' = count' + extra \<and> (s3, r) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn (extend_dec_env new_env env) (update_clock (\<lambda>_. count) s2) ds (update_clock (\<lambda>_. count') s', r'))

goal (1 subgoal):
 1. \<forall>extra count count' s' r'. clock s1 = count + extra \<and> clock s' = count' + extra \<and> (s3, combine_dec_result new_env r) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn env (update_clock (\<lambda>_. count) s1) (d # ds) (update_clock (\<lambda>_. count') s', r')
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>extra count count'. \<lbrakk>evaluate_dec True mn env s1 d (s2, Rval new_env); evaluate_decs True mn (extend_dec_env new_env env) s2 ds (s3, r); \<forall>extraa count count'a. clock s2 = count + extraa \<and> count' + extra = count'a + extraa \<longrightarrow> evaluate_decs True mn (extend_dec_env new_env env) (update_clock (\<lambda>_. count) s2) ds (update_clock (\<lambda>_. count'a) s3, r); clock s1 = count + extra; clock s3 = count' + extra; ck\<rbrakk> \<Longrightarrow> evaluate_decs True mn env (update_clock (\<lambda>_. count) s1) (d # ds) (update_clock (\<lambda>_. count') s3, combine_dec_result new_env r)
[PROOF STEP]
subgoal for extra
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate_dec True mn env s1 d (s2, Rval new_env); evaluate_decs True mn (extend_dec_env new_env env) s2 ds (s3, r); \<forall>extraa count count'a. clock s2 = count + extraa \<and> count'_ + extra = count'a + extraa \<longrightarrow> evaluate_decs True mn (extend_dec_env new_env env) (update_clock (\<lambda>_. count) s2) ds (update_clock (\<lambda>_. count'a) s3, r); clock s1 = count_ + extra; clock s3 = count'_ + extra; ck\<rbrakk> \<Longrightarrow> evaluate_decs True mn env (update_clock (\<lambda>_. count_) s1) (d # ds) (update_clock (\<lambda>_. count'_) s3, combine_dec_result new_env r)
[PROOF STEP]
apply (subgoal_tac "clock s2\<ge>extra")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>evaluate_dec True mn env s1 d (s2, Rval new_env); evaluate_decs True mn (extend_dec_env new_env env) s2 ds (s3, r); \<forall>extraa count count'a. clock s2 = count + extraa \<and> count'_ + extra = count'a + extraa \<longrightarrow> evaluate_decs True mn (extend_dec_env new_env env) (update_clock (\<lambda>_. count) s2) ds (update_clock (\<lambda>_. count'a) s3, r); clock s1 = count_ + extra; clock s3 = count'_ + extra; ck; extra \<le> clock s2\<rbrakk> \<Longrightarrow> evaluate_decs True mn env (update_clock (\<lambda>_. count_) s1) (d # ds) (update_clock (\<lambda>_. count'_) s3, combine_dec_result new_env r)
 2. \<lbrakk>evaluate_dec True mn env s1 d (s2, Rval new_env); evaluate_decs True mn (extend_dec_env new_env env) s2 ds (s3, r); \<forall>extraa count count'a. clock s2 = count + extraa \<and> count'_ + extra = count'a + extraa \<longrightarrow> evaluate_decs True mn (extend_dec_env new_env env) (update_clock (\<lambda>_. count) s2) ds (update_clock (\<lambda>_. count'a) s3, r); clock s1 = count_ + extra; clock s3 = count'_ + extra; ck\<rbrakk> \<Longrightarrow> extra \<le> clock s2
[PROOF STEP]
apply (metis dec_sub_from_counter diff_add_inverse2 eq_diff_iff evaluate_decs.cons2 le_add2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate_dec True mn env s1 d (s2, Rval new_env); evaluate_decs True mn (extend_dec_env new_env env) s2 ds (s3, r); \<forall>extraa count count'a. clock s2 = count + extraa \<and> count'_ + extra = count'a + extraa \<longrightarrow> evaluate_decs True mn (extend_dec_env new_env env) (update_clock (\<lambda>_. count) s2) ds (update_clock (\<lambda>_. count'a) s3, r); clock s1 = count_ + extra; clock s3 = count'_ + extra; ck\<rbrakk> \<Longrightarrow> extra \<le> clock s2
[PROOF STEP]
using decs_clock_monotone
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>evaluate_decs ?ck ?mn ?env ?s ?d ?res; ?ck = True\<rbrakk> \<Longrightarrow> clock (fst ?res) \<le> clock ?s

goal (1 subgoal):
 1. \<lbrakk>evaluate_dec True mn env s1 d (s2, Rval new_env); evaluate_decs True mn (extend_dec_env new_env env) s2 ds (s3, r); \<forall>extraa count count'a. clock s2 = count + extraa \<and> count'_ + extra = count'a + extraa \<longrightarrow> evaluate_decs True mn (extend_dec_env new_env env) (update_clock (\<lambda>_. count) s2) ds (update_clock (\<lambda>_. count'a) s3, r); clock s1 = count_ + extra; clock s3 = count'_ + extra; ck\<rbrakk> \<Longrightarrow> extra \<le> clock s2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>extra count count' s' r'. clock s1 = count + extra \<and> clock s' = count' + extra \<and> (s3, combine_dec_result new_env r) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn env (update_clock (\<lambda>_. count) s1) (d # ds) (update_clock (\<lambda>_. count') s', r')

goal (2 subgoals):
 1. \<And>ck mn env s. \<forall>extra count count' s' r'. clock s = count + extra \<and> clock s' = count' + extra \<and> (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn env (update_clock (\<lambda>_. count) s) [] (update_clock (\<lambda>_. count') s', r')
 2. \<And>ck mn s1 s2 env d ds e. evaluate_dec ck mn env s1 d (s2, Rerr e) \<Longrightarrow> \<forall>extra count count' s' r'. clock s1 = count + extra \<and> clock s' = count' + extra \<and> (s2, Rerr e) = (s', r') \<and> ck = True \<longrightarrow> evaluate_decs ck mn env (update_clock (\<lambda>_. count) s1) (d # ds) (update_clock (\<lambda>_. count') s', r')
[PROOF STEP]
qed (auto intro!:evaluate_decs.intros simp add:dec_sub_from_counter)


[STATEMENT]
lemma decs_clocked_min_counter:
  assumes "evaluate_decs ck mn env s ds res" "ck = True"
  shows "evaluate_decs ck mn env (s \<lparr> clock := clock s - (clock (fst res))\<rparr>) ds (((fst res) \<lparr> clock := 0 \<rparr>),(snd res))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_decs ck mn env (update_clock (\<lambda>_. clock s - clock (fst res)) s) ds (update_clock (\<lambda>_. 0) (fst res), snd res)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. evaluate_decs ck mn env (update_clock (\<lambda>_. clock s - clock (fst res)) s) ds (update_clock (\<lambda>_. 0) (fst res), snd res)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
evaluate_decs ck mn env s ds res
ck = True
[PROOF STEP]
have "clock (fst res) \<le> clock s"
[PROOF STATE]
proof (prove)
using this:
evaluate_decs ck mn env s ds res
ck = True

goal (1 subgoal):
 1. clock (fst res) \<le> clock s
[PROOF STEP]
using decs_clock_monotone
[PROOF STATE]
proof (prove)
using this:
evaluate_decs ck mn env s ds res
ck = True
\<lbrakk>evaluate_decs ?ck ?mn ?env ?s ?d ?res; ?ck = True\<rbrakk> \<Longrightarrow> clock (fst ?res) \<le> clock ?s

goal (1 subgoal):
 1. clock (fst res) \<le> clock s
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
clock (fst res) \<le> clock s

goal (1 subgoal):
 1. evaluate_decs ck mn env (update_clock (\<lambda>_. clock s - clock (fst res)) s) ds (update_clock (\<lambda>_. 0) (fst res), snd res)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
evaluate_decs ck mn env s ds res
ck = True
clock (fst res) \<le> clock s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate_decs ck mn env s ds res
ck = True
clock (fst res) \<le> clock s

goal (1 subgoal):
 1. evaluate_decs ck mn env (update_clock (\<lambda>_. clock s - clock (fst res)) s) ds (update_clock (\<lambda>_. 0) (fst res), snd res)
[PROOF STEP]
by (auto elim!: decs_sub_from_counter[rule_format])
[PROOF STATE]
proof (state)
this:
evaluate_decs ck mn env (update_clock (\<lambda>_. clock s - clock (fst res)) s) ds (update_clock (\<lambda>_. 0) (fst res), snd res)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma decs_add_to_counter:
  "evaluate_decs 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_decs True mn env (s \<lparr> clock := clock s + extra \<rparr>) d ((s' \<lparr> clock := clock s' + extra \<rparr>),r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_decs 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_decs 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_decs.inducts)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ck mn env s. \<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_decs True mn env (update_clock (\<lambda>_. clock s + extra) s) [] (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr e) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (d # ds) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s3, r) = (s', ra) \<and> ck = True \<and> ra \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn (extend_dec_env new_env env) (update_clock (\<lambda>_. clock s2 + extra) s2) ds (update_clock (\<lambda>_. clock s' + extra) s', ra)) \<Longrightarrow> \<forall>s' ra extra. (s3, combine_dec_result new_env r) = (s', ra) \<and> ck = True \<and> ra \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (d # ds) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s3_, r_) = (s', ra) \<and> ck_ = True \<and> ra \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn_ (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. clock s2_ + extra) s2_) ds_ (update_clock (\<lambda>_. clock s' + extra) s', ra))

goal (3 subgoals):
 1. \<And>ck mn env s. \<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_decs True mn env (update_clock (\<lambda>_. clock s + extra) s) [] (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr e) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (d # ds) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s3, r) = (s', ra) \<and> ck = True \<and> ra \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn (extend_dec_env new_env env) (update_clock (\<lambda>_. clock s2 + extra) s2) ds (update_clock (\<lambda>_. clock s' + extra) s', ra)) \<Longrightarrow> \<forall>s' ra extra. (s3, combine_dec_result new_env r) = (s', ra) \<and> ck = True \<and> ra \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (d # ds) (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s3_, r_) = (s', ra) \<and> ck_ = True \<and> ra \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn_ (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. clock s2_ + extra) s2_) ds_ (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s3_, r_) = (s', ra) \<and> ck_ = True \<and> ra \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn_ (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. clock s2_ + extra) s2_) ds_ (update_clock (\<lambda>_. clock s' + extra) s', ra))

goal (1 subgoal):
 1. \<forall>s' ra extra. (s3_, combine_dec_result new_env_ r_) = (s', ra) \<and> ck_ = True \<and> ra \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn_ env_ (update_clock (\<lambda>_. clock s1_ + extra) s1_) (d_ # ds_) (update_clock (\<lambda>_. clock s' + extra) s', ra)
[PROOF STEP]
using dec_add_to_counter evaluate_decs.cons2
[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 extra. (s3_, r_) = (s', ra) \<and> ck_ = True \<and> ra \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn_ (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. clock s2_ + extra) s2_) ds_ (update_clock (\<lambda>_. clock s' + extra) s', ra))
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)
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. \<forall>s' ra extra. (s3_, combine_dec_result new_env_ r_) = (s', ra) \<and> ck_ = True \<and> ra \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn_ env_ (update_clock (\<lambda>_. clock s1_ + extra) s1_) (d_ # ds_) (update_clock (\<lambda>_. clock s' + extra) s', ra)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>s' ra extra. (s3_, combine_dec_result new_env_ r_) = (s', ra) \<and> ck_ = True \<and> ra \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn_ env_ (update_clock (\<lambda>_. clock s1_ + extra) s1_) (d_ # ds_) (update_clock (\<lambda>_. clock s' + extra) s', ra)

goal (2 subgoals):
 1. \<And>ck mn env s. \<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_decs True mn env (update_clock (\<lambda>_. clock s + extra) s) [] (update_clock (\<lambda>_. clock s' + extra) 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 extra. (s2, Rerr e) = (s', r) \<and> ck = True \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_decs True mn env (update_clock (\<lambda>_. clock s1 + extra) s1) (d # ds) (update_clock (\<lambda>_. clock s' + extra) s', r)
[PROOF STEP]
qed (auto intro!:evaluate_decs.intros simp add:dec_add_to_counter)


[STATEMENT]
lemma top_evaluate_not_timeout:
  "evaluate_top False env s tp (s',r) \<Longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_top False env s tp (s', r) \<Longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
by (ind_cases "evaluate_top False env s tp (s',r)") (fastforce dest:dec_evaluate_not_timeout decs_evaluate_not_timeout)+


[STATEMENT]
lemma top_unclocked_ignore:
  assumes "evaluate_top ck env s tp (s',r)" "r \<noteq> Rerr (Rabort Rtimeout_error)"
  shows "evaluate_top False env (s \<lparr> clock := cnt \<rparr>) tp ((s' \<lparr> clock := cnt \<rparr>),r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
evaluate_top ck env s tp (s', r)
r \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>d new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 2. \<And>d err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 3. \<And>s2 ds mn specs new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env))); [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 4. \<And>s2 ds mn specs err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rerr err; [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 5. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 6. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
case (tmod1 s2 ds mn specs new_env)
[PROOF STATE]
proof (state)
this:
tp = Tmod mn specs ds
s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2
r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env)))
[mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)

goal (6 subgoals):
 1. \<And>d new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 2. \<And>d err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 3. \<And>s2 ds mn specs new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env))); [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 4. \<And>s2 ds mn specs err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rerr err; [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 5. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 6. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tp = Tmod mn specs ds
s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2
r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env)))
[mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn specs ds
s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2
r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env)))
[mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)

goal (1 subgoal):
 1. evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env))); [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
from tmod1
[PROOF STATE]
proof (chain)
picking this:
tp = Tmod mn specs ds
s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2
r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env)))
[mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)
[PROOF STEP]
have "[mn] \<notin> defined_mods (update_clock (\<lambda>_. cnt) s)"
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn specs ds
s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2
r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env)))
[mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)

goal (1 subgoal):
 1. [mn] \<notin> defined_mods (update_clock (\<lambda>_. cnt) s)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
[mn] \<notin> defined_mods (update_clock (\<lambda>_. cnt) s)

goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env))); [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[mn] \<notin> defined_mods (update_clock (\<lambda>_. cnt) s)

goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env))); [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
from tmod1
[PROOF STATE]
proof (chain)
picking this:
tp = Tmod mn specs ds
s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2
r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env)))
[mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)
[PROOF STEP]
have "evaluate_decs False [mn] env (update_clock (\<lambda>_. cnt) s) ds (update_clock (\<lambda>_. cnt) s2, Rval new_env)"
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn specs ds
s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2
r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env)))
[mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)

goal (1 subgoal):
 1. evaluate_decs False [mn] env (update_clock (\<lambda>_. cnt) s) ds (update_clock (\<lambda>_. cnt) s2, Rval new_env)
[PROOF STEP]
using decs_unclocked_ignore
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn specs ds
s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2
r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env)))
[mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)
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] env (update_clock (\<lambda>_. cnt) s) ds (update_clock (\<lambda>_. cnt) s2, Rval new_env)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
evaluate_decs False [mn] env (update_clock (\<lambda>_. cnt) s) ds (update_clock (\<lambda>_. cnt) s2, Rval new_env)

goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env))); [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[mn] \<notin> defined_mods (update_clock (\<lambda>_. cnt) s)
evaluate_decs False [mn] env (update_clock (\<lambda>_. cnt) s) ds (update_clock (\<lambda>_. cnt) s2, Rval new_env)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[mn] \<notin> defined_mods (update_clock (\<lambda>_. cnt) s)
evaluate_decs False [mn] env (update_clock (\<lambda>_. cnt) s) ds (update_clock (\<lambda>_. cnt) s2, Rval new_env)

goal (1 subgoal):
 1. evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
unfolding tmod1
[PROOF STATE]
proof (prove)
using this:
[mn] \<notin> defined_mods (update_clock (\<lambda>_. cnt) s)
evaluate_decs False [mn] env (update_clock (\<lambda>_. cnt) s) ds (update_clock (\<lambda>_. cnt) s2, Rval new_env)

goal (1 subgoal):
 1. evaluate_top False env (update_clock (\<lambda>_. cnt) s) (Tmod mn specs ds) (update_clock (\<lambda>_. cnt) (update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2), Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env))))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>[mn] \<notin> defined_mods (update_clock (\<lambda>_. cnt) s); evaluate_decs False [mn] env (update_clock (\<lambda>_. cnt) s) ds (update_clock (\<lambda>_. cnt) s2, Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) (Tmod mn specs ds) (update_clock (\<lambda>_. cnt) (update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2), Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env))))
[PROOF STEP]
apply (drule evaluate_top.tmod1[OF conjI])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. evaluate_decs False [mn] env (update_clock (\<lambda>_. cnt) s) ds (update_clock (\<lambda>_. cnt) s2, Rval new_env) \<Longrightarrow> no_dup_types ?ds2 \<and> evaluate_decs ?ck2 [mn] ?env2 (update_clock (\<lambda>_. cnt) s) ?ds2 (?s2.2, Rval ?new_env2)
 2. \<lbrakk>evaluate_decs False [mn] env (update_clock (\<lambda>_. cnt) s) ds (update_clock (\<lambda>_. cnt) s2, Rval new_env); evaluate_top ?ck2 ?env2 (update_clock (\<lambda>_. cnt) s) (Tmod mn ?specs2 ?ds2) (update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods ?s2.2) ?s2.2, Rval (make_sem_env (nsLift mn (sem_env.v ?new_env2)) (nsLift mn (c ?new_env2))))\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) (Tmod mn specs ds) (update_clock (\<lambda>_. cnt) (update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2), Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env))))
[PROOF STEP]
using tmod1
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn specs ds
s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2
r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env)))
[mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)

goal (2 subgoals):
 1. evaluate_decs False [mn] env (update_clock (\<lambda>_. cnt) s) ds (update_clock (\<lambda>_. cnt) s2, Rval new_env) \<Longrightarrow> no_dup_types ?ds2 \<and> evaluate_decs ?ck2 [mn] ?env2 (update_clock (\<lambda>_. cnt) s) ?ds2 (?s2.2, Rval ?new_env2)
 2. \<lbrakk>evaluate_decs False [mn] env (update_clock (\<lambda>_. cnt) s) ds (update_clock (\<lambda>_. cnt) s2, Rval new_env); evaluate_top ?ck2 ?env2 (update_clock (\<lambda>_. cnt) s) (Tmod mn ?specs2 ?ds2) (update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods ?s2.2) ?s2.2, Rval (make_sem_env (nsLift mn (sem_env.v ?new_env2)) (nsLift mn (c ?new_env2))))\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) (Tmod mn specs ds) (update_clock (\<lambda>_. cnt) (update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2), Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)

goal (5 subgoals):
 1. \<And>d new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 2. \<And>d err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rerr err; [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 4. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 5. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>d new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 2. \<And>d err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rerr err; [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 4. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 5. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
case tmod2
[PROOF STATE]
proof (state)
this:
tp = Tmod mn_ specs_ ds_
s' = update_defined_mods (\<lambda>_. {[mn_]} \<union> defined_mods s2_) s2_
r = Rerr err_
[mn_] \<notin> defined_mods s \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)

goal (5 subgoals):
 1. \<And>d new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 2. \<And>d err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rerr err; [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 4. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 5. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
(* this is the same as tmod1 *)
[PROOF STATE]
proof (state)
this:
tp = Tmod mn_ specs_ ds_
s' = update_defined_mods (\<lambda>_. {[mn_]} \<union> defined_mods s2_) s2_
r = Rerr err_
[mn_] \<notin> defined_mods s \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)

goal (5 subgoals):
 1. \<And>d new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 2. \<And>d err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rerr err; [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 4. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 5. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tp = Tmod mn_ specs_ ds_
s' = update_defined_mods (\<lambda>_. {[mn_]} \<union> defined_mods s2_) s2_
r = Rerr err_
[mn_] \<notin> defined_mods s \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn_ specs_ ds_
s' = update_defined_mods (\<lambda>_. {[mn_]} \<union> defined_mods s2_) s2_
r = Rerr err_
[mn_] \<notin> defined_mods s \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)

goal (1 subgoal):
 1. evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn_ specs_ ds_
s' = update_defined_mods (\<lambda>_. {[mn_]} \<union> defined_mods s2_) s2_
r = Rerr err_
[mn_] \<notin> defined_mods s \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)
evaluate_top ck env s tp (s', r)
r \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn_ specs_ ds_; s' = update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_; r = Rerr err_; evaluate_top ck env s (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_, Rerr err_); err_ \<noteq> Rabort Rtimeout_error; [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) (update_clock (\<lambda>_. cnt) s2_), Rerr err_)
[PROOF STEP]
apply (subst state.record_simps(5)[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn_ specs_ ds_; s' = update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_; r = Rerr err_; evaluate_top ck env s (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_, Rerr err_); err_ \<noteq> Rabort Rtimeout_error; [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods (update_clock ?f8 s2_))) (update_clock (\<lambda>_. cnt) s2_), Rerr err_)
[PROOF STEP]
by (fastforce simp add:decs_unclocked_ignore intro:evaluate_top.tmod2[simplified])
[PROOF STATE]
proof (state)
this:
evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)

goal (4 subgoals):
 1. \<And>d new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 2. \<And>d err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 3. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 4. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>d new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 2. \<And>d err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 3. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 4. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
case (tmod3 ds mn specs)
[PROOF STATE]
proof (state)
this:
tp = Tmod mn specs ds
s' = s
r = Rerr (Rabort Rtype_error)
\<not> no_dup_types ds

goal (4 subgoals):
 1. \<And>d new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 2. \<And>d err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 3. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 4. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tp = Tmod mn specs ds
s' = s
r = Rerr (Rabort Rtype_error)
\<not> no_dup_types ds
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn specs ds
s' = s
r = Rerr (Rabort Rtype_error)
\<not> no_dup_types ds

goal (1 subgoal):
 1. evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
by (auto intro:evaluate_top.intros)
[PROOF STATE]
proof (state)
this:
evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)

goal (3 subgoals):
 1. \<And>d new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 2. \<And>d err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
 3. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top False env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
qed(auto intro!:evaluate_top.intros simp add:dec_unclocked_ignore)


[STATEMENT]
lemma top_unclocked:
  "(evaluate_top False env s tp (s',r) \<longrightarrow> (r \<noteq> Rerr (Rabort Rtimeout_error)) \<and> (clock   s) = (clock   s')) \<and>
   (evaluate_top False env (s (| clock := count1 |)) tp ((s' (| clock := count1 |)),r) =
    evaluate_top False env (s (| clock := count2 |)) tp ((s' (| clock := count2 |)),r))" (is "?P \<and> ?Q")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (evaluate_top False env s tp (s', r) \<longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s') \<and> evaluate_top False env (update_clock (\<lambda>_. count1) s) tp (update_clock (\<lambda>_. count1) s', r) = evaluate_top False env (update_clock (\<lambda>_. count2) s) tp (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. evaluate_top False env s tp (s', r) \<longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
 2. evaluate_top False env (update_clock (\<lambda>_. count1) s) tp (update_clock (\<lambda>_. count1) s', r) = evaluate_top False env (update_clock (\<lambda>_. count2) s) tp (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
show ?P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_top False env s tp (s', r) \<longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
apply (auto simp add:top_evaluate_not_timeout)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_top False env s tp (s', r) \<Longrightarrow> clock s = clock s'
[PROOF STEP]
by (ind_cases "evaluate_top False env s tp (s',r)")
    (auto simp add:dec_unclocked decs_unclocked top_evaluate_not_timeout)
[PROOF STATE]
proof (state)
this:
evaluate_top False env s tp (s', r) \<longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'

goal (1 subgoal):
 1. evaluate_top False env (update_clock (\<lambda>_. count1) s) tp (update_clock (\<lambda>_. count1) s', r) = evaluate_top False env (update_clock (\<lambda>_. count2) s) tp (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. evaluate_top False env (update_clock (\<lambda>_. count1) s) tp (update_clock (\<lambda>_. count1) s', r) = evaluate_top False env (update_clock (\<lambda>_. count2) s) tp (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
show ?Q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_top False env (update_clock (\<lambda>_. count1) s) tp (update_clock (\<lambda>_. count1) s', r) = evaluate_top False env (update_clock (\<lambda>_. count2) s) tp (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
using top_unclocked_ignore[rule_format] top_evaluate_not_timeout
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>evaluate_top ?ck ?env ?s ?tp (?s', ?r); ?r \<noteq> Rerr (Rabort Rtimeout_error)\<rbrakk> \<Longrightarrow> evaluate_top False ?env (update_clock (\<lambda>_. ?cnt) ?s) ?tp (update_clock (\<lambda>_. ?cnt) ?s', ?r)
evaluate_top False ?env ?s ?tp (?s', ?r) \<Longrightarrow> ?r \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. evaluate_top False env (update_clock (\<lambda>_. count1) s) tp (update_clock (\<lambda>_. count1) s', r) = evaluate_top False env (update_clock (\<lambda>_. count2) s) tp (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
evaluate_top False env (update_clock (\<lambda>_. count1) s) tp (update_clock (\<lambda>_. count1) s', r) = evaluate_top False env (update_clock (\<lambda>_. count2) s) tp (update_clock (\<lambda>_. count2) s', r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_evaluate_top_timeout:
  assumes "\<forall>r. \<not>evaluate_top False env s tp r"
  shows " \<exists>r. evaluate_top True env s tp r \<and> (snd r) = Rerr (Rabort Rtimeout_error)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
proof (cases tp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12 x13. tp = Tmod x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
case (Tmod mn specs ds)
[PROOF STATE]
proof (state)
this:
tp = Tmod mn specs ds

goal (2 subgoals):
 1. \<And>x11 x12 x13. tp = Tmod x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
have ds:"no_dup_types ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_dup_types ds
[PROOF STEP]
using Tmod assms tmod3
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn specs ds
\<forall>r. \<not> evaluate_top False env s tp r
\<not> no_dup_types ?ds \<Longrightarrow> evaluate_top ?ck ?env ?s1.0 (Tmod ?mn ?specs ?ds) (?s1.0, Rerr (Rabort Rtype_error))

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

goal (2 subgoals):
 1. \<And>x11 x12 x13. tp = Tmod x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
have mn:"[mn] \<notin> defined_mods s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [mn] \<notin> defined_mods s
[PROOF STEP]
using Tmod assms tmod4
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn specs ds
\<forall>r. \<not> evaluate_top False env s tp r
[?mn] \<in> defined_mods ?s \<Longrightarrow> evaluate_top ?ck ?env ?s (Tmod ?mn ?specs ?ds) (?s, Rerr (Rabort Rtype_error))

goal (1 subgoal):
 1. [mn] \<notin> defined_mods s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[mn] \<notin> defined_mods s

goal (2 subgoals):
 1. \<And>x11 x12 x13. tp = Tmod x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
have "\<not> evaluate_decs False [mn] env s ds (s', r)" for s' r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> evaluate_decs False [mn] env s ds (s', r)
[PROOF STEP]
apply (cases r)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<not> evaluate_decs False [mn] env s ds (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<not> evaluate_decs False [mn] env s ds (s', r)
[PROOF STEP]
using ds mn Tmod assms tmod1 tmod2
[PROOF STATE]
proof (prove)
using this:
no_dup_types ds
[mn] \<notin> defined_mods s
tp = Tmod mn specs ds
\<forall>r. \<not> evaluate_top False env s tp r
[?mn] \<notin> defined_mods ?s1.0 \<and> no_dup_types ?ds \<and> evaluate_decs ?ck [?mn] ?env ?s1.0 ?ds (?s2.0, Rval ?new_env) \<Longrightarrow> evaluate_top ?ck ?env ?s1.0 (Tmod ?mn ?specs ?ds) (update_defined_mods (\<lambda>_. {[?mn]} \<union> defined_mods ?s2.0) ?s2.0, Rval (make_sem_env (nsLift ?mn (sem_env.v ?new_env)) (nsLift ?mn (c ?new_env))))
[?mn] \<notin> defined_mods ?s1.0 \<and> no_dup_types ?ds \<and> evaluate_decs ?ck [?mn] ?env ?s1.0 ?ds (?s2.0, Rerr ?err) \<Longrightarrow> evaluate_top ?ck ?env ?s1.0 (Tmod ?mn ?specs ?ds) (update_defined_mods (\<lambda>_. {[?mn]} \<union> defined_mods ?s2.0) ?s2.0, Rerr ?err)

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<not> evaluate_decs False [mn] env s ds (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<not> evaluate_decs False [mn] env s ds (s', r)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
\<not> evaluate_decs False [mn] env s ds (?s', ?r)

goal (2 subgoals):
 1. \<And>x11 x12 x13. tp = Tmod x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> evaluate_decs False [mn] env s ds (?s', ?r)
[PROOF STEP]
obtain s' where " evaluate_decs True [mn] env s ds (s', Rerr (Rabort Rtimeout_error))"
[PROOF STATE]
proof (prove)
using this:
\<not> evaluate_decs False [mn] env s ds (?s', ?r)

goal (1 subgoal):
 1. (\<And>s'. evaluate_decs True [mn] env s ds (s', Rerr (Rabort Rtimeout_error)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (full_types) not_evaluate_decs_timeout[simplified])
[PROOF STATE]
proof (state)
this:
evaluate_decs True [mn] env s ds (s', Rerr (Rabort Rtimeout_error))

goal (2 subgoals):
 1. \<And>x11 x12 x13. tp = Tmod x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
unfolding Tmod
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_top True env s (Tmod mn specs ds) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply (intro exI conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. evaluate_top True env s (Tmod mn specs ds) ?r
 2. snd ?r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply (rule tmod2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs True [mn] env s ds (?s2.2, Rerr ?err2)
 2. snd (update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods ?s2.2) ?s2.2, Rerr ?err2) = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. [mn] \<notin> defined_mods s
 2. no_dup_types ds
 3. evaluate_decs True [mn] env s ds (?s2.2, Rerr ?err2)
 4. snd (update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods ?s2.2) ?s2.2, Rerr ?err2) = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply fact+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s') s', Rerr (Rabort Rtimeout_error)) = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
case (Tdec d)
[PROOF STATE]
proof (state)
this:
tp = Tdec d

goal (1 subgoal):
 1. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
have "\<not> evaluate_dec False [] env s d (s', r)" for s' r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> evaluate_dec False [] env s d (s', r)
[PROOF STEP]
apply (cases r)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<not> evaluate_dec False [] env s d (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<not> evaluate_dec False [] env s d (s', r)
[PROOF STEP]
using tdec1 tdec2 assms Tdec
[PROOF STATE]
proof (prove)
using this:
evaluate_dec ?ck [] ?env ?s1.0 ?d (?s2.0, Rval ?new_env) \<Longrightarrow> evaluate_top ?ck ?env ?s1.0 (Tdec ?d) (?s2.0, Rval ?new_env)
evaluate_dec ?ck [] ?env ?s1.0 ?d (?s2.0, Rerr ?err) \<Longrightarrow> evaluate_top ?ck ?env ?s1.0 (Tdec ?d) (?s2.0, Rerr ?err)
\<forall>r. \<not> evaluate_top False env s tp r
tp = Tdec d

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<not> evaluate_dec False [] env s d (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<not> evaluate_dec False [] env s d (s', r)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
\<not> evaluate_dec False [] env s d (?s', ?r)

goal (1 subgoal):
 1. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> evaluate_dec False [] env s d (?s', ?r)
[PROOF STEP]
obtain s' where  " evaluate_dec True [] env s d (s', Rerr (Rabort Rtimeout_error))"
[PROOF STATE]
proof (prove)
using this:
\<not> evaluate_dec False [] env s d (?s', ?r)

goal (1 subgoal):
 1. (\<And>s'. evaluate_dec True [] env s d (s', Rerr (Rabort Rtimeout_error)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using not_evaluate_dec_timeout[simplified]
[PROOF STATE]
proof (prove)
using this:
\<not> evaluate_dec False [] env s d (?s', ?r)
\<forall>a b. \<not> evaluate_dec False ?mn ?env ?s ?d (a, b) \<Longrightarrow> \<exists>a b. evaluate_dec True ?mn ?env ?s ?d (a, b) \<and> b = Rerr (Rabort Rtimeout_error)

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

goal (1 subgoal):
 1. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
unfolding Tdec
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_top True env s (Tdec d) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply (intro exI conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. evaluate_top True env s (Tdec d) ?r
 2. snd ?r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. evaluate_dec True [] env s d (?s2.2, Rerr ?err2)
 2. snd (?s2.2, Rerr ?err2) = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (s', Rerr (Rabort Rtimeout_error)) = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>r. evaluate_top True env s tp r \<and> snd r = Rerr (Rabort Rtimeout_error)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma top_clocked_total:
  "\<exists>r. evaluate_top True env s tp r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
proof (cases tp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12 x13. tp = Tmod x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
 2. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
case (Tmod mn specs ds)
[PROOF STATE]
proof (state)
this:
tp = Tmod mn specs ds

goal (2 subgoals):
 1. \<And>x11 x12 x13. tp = Tmod x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
 2. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
have ds:"\<exists>s' r. evaluate_decs True [mn] env s ds (s',r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_decs True [mn] env s ds (s', r)
[PROOF STEP]
using decs_clocked_total[simplified]
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. evaluate_decs True ?mn ?env ?s ?ds (a, b)

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

goal (2 subgoals):
 1. \<And>x11 x12 x13. tp = Tmod x11 x12 x13 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
 2. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
from Tmod
[PROOF STATE]
proof (chain)
picking this:
tp = Tmod mn specs ds
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn specs ds

goal (1 subgoal):
 1. \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
apply (cases "no_dup_types ds")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
 2. \<lbrakk>tp = Tmod mn specs ds; \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tp = Tmod mn specs ds; \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
 2. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
using tmod3
[PROOF STATE]
proof (prove)
using this:
\<not> no_dup_types ?ds \<Longrightarrow> evaluate_top ?ck ?env ?s1.0 (Tmod ?mn ?specs ?ds) (?s1.0, Rerr (Rabort Rtype_error))

goal (2 subgoals):
 1. \<lbrakk>tp = Tmod mn specs ds; \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
 2. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
apply (cases "[mn] \<in>(defined_mods s)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds; [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
 2. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds; [mn] \<notin> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
using tmod4
[PROOF STATE]
proof (prove)
using this:
[?mn] \<in> defined_mods ?s \<Longrightarrow> evaluate_top ?ck ?env ?s (Tmod ?mn ?specs ?ds) (?s, Rerr (Rabort Rtype_error))

goal (2 subgoals):
 1. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds; [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
 2. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds; [mn] \<notin> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds; [mn] \<notin> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
using ds
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate_decs True [mn] env s ds (s', r)

goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds; [mn] \<notin> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s' r. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds; [mn] \<notin> defined_mods s; evaluate_decs True [mn] env s ds (s', r)\<rbrakk> \<Longrightarrow> \<exists>a b. evaluate_top True env s (Tmod mn specs ds) (a, b)
[PROOF STEP]
subgoal for s' r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds; [mn] \<notin> defined_mods s; evaluate_decs True [mn] env s ds (s', r)\<rbrakk> \<Longrightarrow> \<exists>a b. evaluate_top True env s (Tmod mn specs ds) (a, b)
[PROOF STEP]
apply (cases r)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds; [mn] \<notin> defined_mods s; evaluate_decs True [mn] env s ds (s', r); r = Rval x1\<rbrakk> \<Longrightarrow> \<exists>a b. evaluate_top True env s (Tmod mn specs ds) (a, b)
 2. \<And>x2. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds; [mn] \<notin> defined_mods s; evaluate_decs True [mn] env s ds (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>a b. evaluate_top True env s (Tmod mn specs ds) (a, b)
[PROOF STEP]
using evaluate_top.tmod1 evaluate_top.tmod2
[PROOF STATE]
proof (prove)
using this:
[?mn] \<notin> defined_mods ?s1.0 \<and> no_dup_types ?ds \<and> evaluate_decs ?ck [?mn] ?env ?s1.0 ?ds (?s2.0, Rval ?new_env) \<Longrightarrow> evaluate_top ?ck ?env ?s1.0 (Tmod ?mn ?specs ?ds) (update_defined_mods (\<lambda>_. {[?mn]} \<union> defined_mods ?s2.0) ?s2.0, Rval (make_sem_env (nsLift ?mn (sem_env.v ?new_env)) (nsLift ?mn (c ?new_env))))
[?mn] \<notin> defined_mods ?s1.0 \<and> no_dup_types ?ds \<and> evaluate_decs ?ck [?mn] ?env ?s1.0 ?ds (?s2.0, Rerr ?err) \<Longrightarrow> evaluate_top ?ck ?env ?s1.0 (Tmod ?mn ?specs ?ds) (update_defined_mods (\<lambda>_. {[?mn]} \<union> defined_mods ?s2.0) ?s2.0, Rerr ?err)

goal (2 subgoals):
 1. \<And>x1. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds; [mn] \<notin> defined_mods s; evaluate_decs True [mn] env s ds (s', r); r = Rval x1\<rbrakk> \<Longrightarrow> \<exists>a b. evaluate_top True env s (Tmod mn specs ds) (a, b)
 2. \<And>x2. \<lbrakk>tp = Tmod mn specs ds; no_dup_types ds; [mn] \<notin> defined_mods s; evaluate_decs True [mn] env s ds (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>a b. evaluate_top True env s (Tmod mn specs ds) (a, b)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>r. evaluate_top True env s tp r

goal (1 subgoal):
 1. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
case (Tdec d)
[PROOF STATE]
proof (state)
this:
tp = Tdec d

goal (1 subgoal):
 1. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
have d:"\<exists>s' r. evaluate_dec True [] env s d (s',r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_dec True [] env s d (s', r)
[PROOF STEP]
using dec_clocked_total[simplified]
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. evaluate_dec True ?mn ?env ?s ?d (a, b)

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

goal (1 subgoal):
 1. \<And>x2. tp = Tdec x2 \<Longrightarrow> \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_top True env s tp r
[PROOF STEP]
unfolding Tdec
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_top True env s (Tdec d) r
[PROOF STEP]
using d
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate_dec True [] env s d (s', r)

goal (1 subgoal):
 1. \<exists>r. evaluate_top True env s (Tdec d) r
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s' r. evaluate_dec True [] env s d (s', r) \<Longrightarrow> \<exists>a b. evaluate_top True env s (Tdec d) (a, b)
[PROOF STEP]
subgoal for s' r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_dec True [] env s d (s', r) \<Longrightarrow> \<exists>a b. evaluate_top True env s (Tdec d) (a, b)
[PROOF STEP]
apply (cases r)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>evaluate_dec True [] env s d (s', r); r = Rval x1\<rbrakk> \<Longrightarrow> \<exists>a b. evaluate_top True env s (Tdec d) (a, b)
 2. \<And>x2. \<lbrakk>evaluate_dec True [] env s d (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>a b. evaluate_top True env s (Tdec d) (a, b)
[PROOF STEP]
using evaluate_top.tdec1 evaluate_top.tdec2
[PROOF STATE]
proof (prove)
using this:
evaluate_dec ?ck [] ?env ?s1.0 ?d (?s2.0, Rval ?new_env) \<Longrightarrow> evaluate_top ?ck ?env ?s1.0 (Tdec ?d) (?s2.0, Rval ?new_env)
evaluate_dec ?ck [] ?env ?s1.0 ?d (?s2.0, Rerr ?err) \<Longrightarrow> evaluate_top ?ck ?env ?s1.0 (Tdec ?d) (?s2.0, Rerr ?err)

goal (2 subgoals):
 1. \<And>x1. \<lbrakk>evaluate_dec True [] env s d (s', r); r = Rval x1\<rbrakk> \<Longrightarrow> \<exists>a b. evaluate_top True env s (Tdec d) (a, b)
 2. \<And>x2. \<lbrakk>evaluate_dec True [] env s d (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>a b. evaluate_top True env s (Tdec d) (a, b)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>r. evaluate_top True env s tp r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma top_clocked_min_counter:
  assumes "evaluate_top ck env s tp (s',r)" "ck"
  shows "evaluate_top ck env (s \<lparr> clock := clock s - clock s' \<rparr>) tp (s' \<lparr> clock := 0 \<rparr>,r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
evaluate_top ck env s tp (s', r)
ck

goal (1 subgoal):
 1. evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>d new_env. \<lbrakk>ck; tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>d err. \<lbrakk>ck; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>s2 ds mn specs new_env. \<lbrakk>ck; tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env))); [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>s2 ds mn specs err. \<lbrakk>ck; tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rerr err; [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 5. \<And>ds mn specs. \<lbrakk>ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 6. \<And>mn specs ds. \<lbrakk>ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
case tmod1
[PROOF STATE]
proof (state)
this:
tp = Tmod mn_ specs_ ds_
s' = update_defined_mods (\<lambda>_. {[mn_]} \<union> defined_mods s2_) s2_
r = Rval (make_sem_env (nsLift mn_ (sem_env.v new_env_)) (nsLift mn_ (c new_env_)))
[mn_] \<notin> defined_mods s \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env s ds_ (s2_, Rval new_env_)

goal (6 subgoals):
 1. \<And>d new_env. \<lbrakk>ck; tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>d err. \<lbrakk>ck; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>s2 ds mn specs new_env. \<lbrakk>ck; tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rval (make_sem_env (nsLift mn (sem_env.v new_env)) (nsLift mn (c new_env))); [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>s2 ds mn specs err. \<lbrakk>ck; tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rerr err; [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 5. \<And>ds mn specs. \<lbrakk>ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 6. \<And>mn specs ds. \<lbrakk>ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tp = Tmod mn_ specs_ ds_
s' = update_defined_mods (\<lambda>_. {[mn_]} \<union> defined_mods s2_) s2_
r = Rval (make_sem_env (nsLift mn_ (sem_env.v new_env_)) (nsLift mn_ (c new_env_)))
[mn_] \<notin> defined_mods s \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env s ds_ (s2_, Rval new_env_)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn_ specs_ ds_
s' = update_defined_mods (\<lambda>_. {[mn_]} \<union> defined_mods s2_) s2_
r = Rval (make_sem_env (nsLift mn_ (sem_env.v new_env_)) (nsLift mn_ (c new_env_)))
[mn_] \<notin> defined_mods s \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env s ds_ (s2_, Rval new_env_)

goal (1 subgoal):
 1. evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn_ specs_ ds_; s' = update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_; r = Rval (make_sem_env (nsLift mn_ (sem_env.v new_env_)) (nsLift mn_ (c new_env_))); [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs ck [mn_] env s ds_ (s2_, Rval new_env_)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s2_) s) (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) (update_clock (\<lambda>_. 0) s2_), Rval (make_sem_env (nsLift mn_ (sem_env.v new_env_)) (nsLift mn_ (c new_env_))))
[PROOF STEP]
apply (subst state.record_simps(5)[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn_ specs_ ds_; s' = update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_; r = Rval (make_sem_env (nsLift mn_ (sem_env.v new_env_)) (nsLift mn_ (c new_env_))); [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs ck [mn_] env s ds_ (s2_, Rval new_env_)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s2_) s) (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods (update_clock ?f6 s2_))) (update_clock (\<lambda>_. 0) s2_), Rval (make_sem_env (nsLift mn_ (sem_env.v new_env_)) (nsLift mn_ (c new_env_))))
[PROOF STEP]
apply (rule evaluate_top.tmod1[simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn_ specs_ ds_; s' = update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_; r = Rval (make_sem_env (nsLift mn_ (sem_env.v new_env_)) (nsLift mn_ (c new_env_))); [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs ck [mn_] env s ds_ (s2_, Rval new_env_)\<rbrakk> \<Longrightarrow> [mn_] \<notin> defined_mods (update_clock (\<lambda>_. clock s - clock s2_) s) \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env (update_clock (\<lambda>_. clock s - clock s2_) s) ds_ (update_clock (\<lambda>_. 0) s2_, Rval new_env_)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
evaluate_top ck env s tp (s', r)
ck

goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn_ specs_ ds_; s' = update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_; r = Rval (make_sem_env (nsLift mn_ (sem_env.v new_env_)) (nsLift mn_ (c new_env_))); [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs ck [mn_] env s ds_ (s2_, Rval new_env_)\<rbrakk> \<Longrightarrow> [mn_] \<notin> defined_mods (update_clock (\<lambda>_. clock s - clock s2_) s) \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env (update_clock (\<lambda>_. clock s - clock s2_) s) ds_ (update_clock (\<lambda>_. 0) s2_, Rval new_env_)
[PROOF STEP]
by (auto dest:decs_clocked_min_counter)
[PROOF STATE]
proof (state)
this:
evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)

goal (5 subgoals):
 1. \<And>d new_env. \<lbrakk>ck; tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>d err. \<lbrakk>ck; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>ck; tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rerr err; [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>ds mn specs. \<lbrakk>ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 5. \<And>mn specs ds. \<lbrakk>ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>d new_env. \<lbrakk>ck; tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>d err. \<lbrakk>ck; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>ck; tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rerr err; [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>ds mn specs. \<lbrakk>ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 5. \<And>mn specs ds. \<lbrakk>ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
case tmod2
[PROOF STATE]
proof (state)
this:
tp = Tmod mn_ specs_ ds_
s' = update_defined_mods (\<lambda>_. {[mn_]} \<union> defined_mods s2_) s2_
r = Rerr err_
[mn_] \<notin> defined_mods s \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)

goal (5 subgoals):
 1. \<And>d new_env. \<lbrakk>ck; tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>d err. \<lbrakk>ck; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>ck; tp = Tmod mn specs ds; s' = update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2; r = Rerr err; [mn] \<notin> defined_mods s \<and> no_dup_types ds \<and> evaluate_decs ck [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>ds mn specs. \<lbrakk>ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 5. \<And>mn specs ds. \<lbrakk>ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tp = Tmod mn_ specs_ ds_
s' = update_defined_mods (\<lambda>_. {[mn_]} \<union> defined_mods s2_) s2_
r = Rerr err_
[mn_] \<notin> defined_mods s \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn_ specs_ ds_
s' = update_defined_mods (\<lambda>_. {[mn_]} \<union> defined_mods s2_) s2_
r = Rerr err_
[mn_] \<notin> defined_mods s \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)

goal (1 subgoal):
 1. evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn_ specs_ ds_; s' = update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_; r = Rerr err_; [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s2_) s) (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) (update_clock (\<lambda>_. 0) s2_), Rerr err_)
[PROOF STEP]
apply (subst state.record_simps(5)[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn_ specs_ ds_; s' = update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_; r = Rerr err_; [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s2_) s) (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods (update_clock ?f6 s2_))) (update_clock (\<lambda>_. 0) s2_), Rerr err_)
[PROOF STEP]
apply (rule evaluate_top.tmod2[simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn_ specs_ ds_; s' = update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_; r = Rerr err_; [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)\<rbrakk> \<Longrightarrow> [mn_] \<notin> defined_mods (update_clock (\<lambda>_. clock s - clock s2_) s) \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env (update_clock (\<lambda>_. clock s - clock s2_) s) ds_ (update_clock (\<lambda>_. 0) s2_, Rerr err_)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
evaluate_top ck env s tp (s', r)
ck

goal (1 subgoal):
 1. \<lbrakk>tp = Tmod mn_ specs_ ds_; s' = update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_; r = Rerr err_; [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs ck [mn_] env s ds_ (s2_, Rerr err_)\<rbrakk> \<Longrightarrow> [mn_] \<notin> defined_mods (update_clock (\<lambda>_. clock s - clock s2_) s) \<and> no_dup_types ds_ \<and> evaluate_decs ck [mn_] env (update_clock (\<lambda>_. clock s - clock s2_) s) ds_ (update_clock (\<lambda>_. 0) s2_, Rerr err_)
[PROOF STEP]
by (auto dest:decs_clocked_min_counter)
[PROOF STATE]
proof (state)
this:
evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)

goal (4 subgoals):
 1. \<And>d new_env. \<lbrakk>ck; tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>d err. \<lbrakk>ck; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>ds mn specs. \<lbrakk>ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>mn specs ds. \<lbrakk>ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. clock s - clock s') s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
qed (fastforce intro:evaluate_top.intros dest:dec_clocked_min_counter)+