[STATEMENT]
lemma top_add_clock:
  assumes "evaluate_top ck env s tp (s',r)" "\<not>ck"
  shows "\<exists>c. evaluate_top True env (s (| clock := c |)) tp ((s' (| clock := 0 |)),r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) 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)
\<not> ck

goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) 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>\<not> ck; tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>d err. \<lbrakk>\<not> ck; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>s2 ds mn specs new_env. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 5. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 6. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
case (tdec1 d)
[PROOF STATE]
proof (state)
this:
tp = Tdec d
r = Rval new_env_
evaluate_dec ck [] env s d (s', Rval new_env_)

goal (6 subgoals):
 1. \<And>d new_env. \<lbrakk>\<not> ck; tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>d err. \<lbrakk>\<not> ck; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>s2 ds mn specs new_env. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 5. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 6. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tp = Tdec d
r = Rval new_env_
evaluate_dec ck [] env s d (s', Rval new_env_)
[PROOF STEP]
obtain c where "evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', r)"
[PROOF STATE]
proof (prove)
using this:
tp = Tdec d
r = Rval new_env_
evaluate_dec ck [] env s d (s', Rval new_env_)

goal (1 subgoal):
 1. (\<And>c. evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dec_add_clock assms
[PROOF STATE]
proof (prove)
using this:
tp = Tdec d
r = Rval new_env_
evaluate_dec ck [] env s d (s', Rval new_env_)
evaluate_dec ?ck ?mn ?env ?s ?d ?res \<Longrightarrow> \<forall>s' r. ?res = (s', r) \<and> ?ck = False \<longrightarrow> (\<exists>c. evaluate_dec True ?mn ?env (update_clock (\<lambda>_. c) ?s) ?d (update_clock (\<lambda>_. 0) s', r))
evaluate_top ck env s tp (s', r)
\<not> ck

goal (1 subgoal):
 1. (\<And>c. evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', r)

goal (6 subgoals):
 1. \<And>d new_env. \<lbrakk>\<not> ck; tp = Tdec d; r = Rval new_env; evaluate_dec ck [] env s d (s', Rval new_env)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>d err. \<lbrakk>\<not> ck; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>s2 ds mn specs new_env. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 5. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 6. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', r)

goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
unfolding tdec1
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', Rval new_env_)

goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) (Tdec d) (update_clock (\<lambda>_. 0) s', Rval new_env_)
[PROOF STEP]
by - rule+
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)

goal (5 subgoals):
 1. \<And>d err. \<lbrakk>\<not> ck; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>s2 ds mn specs new_env. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 5. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>d err. \<lbrakk>\<not> ck; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>s2 ds mn specs new_env. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 5. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
case (tdec2 d)
[PROOF STATE]
proof (state)
this:
tp = Tdec d
r = Rerr err_
evaluate_dec ck [] env s d (s', Rerr err_)

goal (5 subgoals):
 1. \<And>d err. \<lbrakk>\<not> ck; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>s2 ds mn specs new_env. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 5. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tp = Tdec d
r = Rerr err_
evaluate_dec ck [] env s d (s', Rerr err_)
[PROOF STEP]
obtain c where "evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', r)"
[PROOF STATE]
proof (prove)
using this:
tp = Tdec d
r = Rerr err_
evaluate_dec ck [] env s d (s', Rerr err_)

goal (1 subgoal):
 1. (\<And>c. evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dec_add_clock assms
[PROOF STATE]
proof (prove)
using this:
tp = Tdec d
r = Rerr err_
evaluate_dec ck [] env s d (s', Rerr err_)
evaluate_dec ?ck ?mn ?env ?s ?d ?res \<Longrightarrow> \<forall>s' r. ?res = (s', r) \<and> ?ck = False \<longrightarrow> (\<exists>c. evaluate_dec True ?mn ?env (update_clock (\<lambda>_. c) ?s) ?d (update_clock (\<lambda>_. 0) s', r))
evaluate_top ck env s tp (s', r)
\<not> ck

goal (1 subgoal):
 1. (\<And>c. evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', r)

goal (5 subgoals):
 1. \<And>d err. \<lbrakk>\<not> ck; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>s2 ds mn specs new_env. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 5. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', r)

goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
unfolding tdec2
[PROOF STATE]
proof (prove)
using this:
evaluate_dec True [] env (update_clock (\<lambda>_. c) s) d (update_clock (\<lambda>_. 0) s', Rerr err_)

goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) (Tdec d) (update_clock (\<lambda>_. 0) s', Rerr err_)
[PROOF STEP]
by - rule+
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)

goal (4 subgoals):
 1. \<And>s2 ds mn specs new_env. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>s2 ds mn specs new_env. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) 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 (4 subgoals):
 1. \<And>s2 ds mn specs new_env. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) 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]
obtain c where "evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) 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. (\<And>c. evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rval new_env) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using decs_add_clock assms
[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 ?ds ?res \<Longrightarrow> \<forall>s' r. ?res = (s', r) \<and> ?ck = False \<longrightarrow> (\<exists>c. evaluate_decs True ?mn ?env (update_clock (\<lambda>_. c) ?s) ?ds (update_clock (\<lambda>_. 0) s', r))
evaluate_top ck env s tp (s', r)
\<not> ck

goal (1 subgoal):
 1. (\<And>c. evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rval new_env) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rval new_env)

goal (4 subgoals):
 1. \<And>s2 ds mn specs new_env. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 4. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rval new_env)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rval new_env)

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

goal (1 subgoal):
 1. \<exists>ca. evaluate_top True env (update_clock (\<lambda>_. ca) s) (Tmod mn specs ds) (update_clock (\<lambda>_. 0) (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 auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rval new_env) \<Longrightarrow> \<exists>ca. evaluate_top True env (update_clock (\<lambda>_. ca) 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. evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rval new_env) \<Longrightarrow> \<exists>ca. evaluate_top True env (update_clock (\<lambda>_. ca) s) (Tmod mn specs ds) (update_defined_mods (\<lambda>_. insert [mn] (defined_mods (update_clock ?f1 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+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rval new_env) \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. ?c2) s) (Tmod mn specs ds) (update_defined_mods (\<lambda>_. insert [mn] (defined_mods (update_clock ?f1 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. evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rval new_env) \<Longrightarrow> [mn] \<notin> defined_mods (update_clock (\<lambda>_. ?c2) s) \<and> no_dup_types ds \<and> evaluate_decs True [mn] env (update_clock (\<lambda>_. ?c2) s) ds (update_clock (\<lambda>_. 0) s2, Rval 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 (1 subgoal):
 1. evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rval new_env) \<Longrightarrow> [mn] \<notin> defined_mods (update_clock (\<lambda>_. ?c2) s) \<and> no_dup_types ds \<and> evaluate_decs True [mn] env (update_clock (\<lambda>_. ?c2) s) ds (update_clock (\<lambda>_. 0) s2, Rval new_env)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)

goal (3 subgoals):
 1. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
case (tmod2 s2 ds mn specs err)
[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 (3 subgoals):
 1. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) 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]
obtain c where "evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err)"
[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. (\<And>c. evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using decs_add_clock 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_decs ?ck ?mn ?env ?s ?ds ?res \<Longrightarrow> \<forall>s' r. ?res = (s', r) \<and> ?ck = False \<longrightarrow> (\<exists>c. evaluate_decs True ?mn ?env (update_clock (\<lambda>_. c) ?s) ?ds (update_clock (\<lambda>_. 0) s', r))
evaluate_top ck env s tp (s', r)
\<not> ck

goal (1 subgoal):
 1. (\<And>c. evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err)

goal (3 subgoals):
 1. \<And>s2 ds mn specs err. \<lbrakk>\<not> 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> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 3. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err)

goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
unfolding tmod2
[PROOF STATE]
proof (prove)
using this:
evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err)

goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) (Tmod mn specs ds) (update_clock (\<lambda>_. 0) (update_defined_mods (\<lambda>_. {[mn]} \<union> defined_mods s2) s2), Rerr err)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err) \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) 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. evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err) \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) (Tmod mn specs ds) (update_defined_mods (\<lambda>_. insert [mn] (defined_mods (update_clock ?f1 s2))) (update_clock (\<lambda>_. 0) s2), Rerr err)
[PROOF STEP]
apply rule+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err) \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. ?c2) s) (Tmod mn specs ds) (update_defined_mods (\<lambda>_. insert [mn] (defined_mods (update_clock ?f1 s2))) (update_clock (\<lambda>_. 0) s2), Rerr err)
[PROOF STEP]
apply (rule evaluate_top.tmod2[simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err) \<Longrightarrow> [mn] \<notin> defined_mods (update_clock (\<lambda>_. ?c2) s) \<and> no_dup_types ds \<and> evaluate_decs True [mn] env (update_clock (\<lambda>_. ?c2) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err)
[PROOF STEP]
using tmod2
[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_decs True [mn] env (update_clock (\<lambda>_. c) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err) \<Longrightarrow> [mn] \<notin> defined_mods (update_clock (\<lambda>_. ?c2) s) \<and> no_dup_types ds \<and> evaluate_decs True [mn] env (update_clock (\<lambda>_. ?c2) s) ds (update_clock (\<lambda>_. 0) s2, Rerr err)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)

goal (2 subgoals):
 1. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
case tmod3
[PROOF STATE]
proof (state)
this:
tp = Tmod mn_ specs_ ds_
s' = s
r = Rerr (Rabort Rtype_error)
\<not> no_dup_types ds_

goal (2 subgoals):
 1. \<And>ds mn specs. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
 2. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) 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. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
by (auto intro:evaluate_top.intros)
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)

goal (1 subgoal):
 1. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
case tmod4
[PROOF STATE]
proof (state)
this:
tp = Tmod mn_ specs_ ds_
s' = s
r = Rerr (Rabort Rtype_error)
[mn_] \<in> defined_mods s

goal (1 subgoal):
 1. \<And>mn specs ds. \<lbrakk>\<not> ck; tp = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tp = Tmod mn_ specs_ ds_
s' = s
r = Rerr (Rabort Rtype_error)
[mn_] \<in> defined_mods s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
tp = Tmod mn_ specs_ ds_
s' = s
r = Rerr (Rabort Rtype_error)
[mn_] \<in> defined_mods s

goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
unfolding tmod4
[PROOF STATE]
proof (prove)
using this:
Tmod mn_ specs_ ds_ = Tmod mn_ specs_ ds_
s = s
Rerr (Rabort Rtype_error) = Rerr (Rabort Rtype_error)
[mn_] \<in> defined_mods s

goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) (Tmod mn_ specs_ ds_) (update_clock (\<lambda>_. 0) s, Rerr (Rabort Rtype_error))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Tmod mn_ specs_ ds_ = Tmod mn_ specs_ ds_; s = s; Rerr (Rabort Rtype_error) = Rerr (Rabort Rtype_error); [mn_] \<in> defined_mods s\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) (Tmod mn_ specs_ ds_) (update_clock (\<lambda>_. 0) s, Rerr (Rabort Rtype_error))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Tmod mn_ specs_ ds_ = Tmod mn_ specs_ ds_; s = s; Rerr (Rabort Rtype_error) = Rerr (Rabort Rtype_error); [mn_] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. ?c4) s) (Tmod mn_ specs_ ds_) (update_clock (\<lambda>_. 0) s, Rerr (Rabort Rtype_error))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Tmod mn_ specs_ ds_ = Tmod mn_ specs_ ds_; s = s; Rerr (Rabort Rtype_error) = Rerr (Rabort Rtype_error); [mn_] \<in> defined_mods s\<rbrakk> \<Longrightarrow> [mn_] \<in> defined_mods (update_clock (\<lambda>_. 0) s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma top_clocked_unclocked_equiv:
  "evaluate_top False env s tp (s',r) =
  (\<exists>c. evaluate_top True env (s \<lparr> clock := c \<rparr>) tp ((s' \<lparr> clock := 0 \<rparr>),r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and>
       (clock s) = (clock s'))" (is "?P = ?Q")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_top False env s tp (s', r) = (\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. evaluate_top False env s tp (s', r) \<Longrightarrow> \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
 2. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> evaluate_top False env s tp (s', r)
[PROOF STEP]
assume ?P
[PROOF STATE]
proof (state)
this:
evaluate_top False env s tp (s', r)

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

goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
by (auto simp add:top_add_clock top_unclocked dest:top_evaluate_not_timeout)
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'

goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> evaluate_top False env s tp (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> evaluate_top False env s tp (s', r)
[PROOF STEP]
assume ?Q
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'

goal (1 subgoal):
 1. \<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> evaluate_top False env s tp (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
show ?P
[PROOF STATE]
proof (prove)
using this:
\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'

goal (1 subgoal):
 1. evaluate_top False env s tp (s', r)
[PROOF STEP]
using top_unclocked_ignore
[PROOF STATE]
proof (prove)
using this:
\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
\<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)

goal (1 subgoal):
 1. evaluate_top False env s tp (s', r)
[PROOF STEP]
(* sledgehammer proof *)
[PROOF STATE]
proof (prove)
using this:
\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
\<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)

goal (1 subgoal):
 1. evaluate_top False env s tp (s', r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'; \<And>ck env s tp s' r cnt. \<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)\<rbrakk> \<Longrightarrow> evaluate_top False env s tp (s', r)
[PROOF STEP]
obtain nn :: nat where
      f1: "evaluate_top True env (update_clock (\<lambda>n. nn) s) tp (update_clock (\<lambda>n. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>nn. evaluate_top True env (update_clock (\<lambda>n. nn) s) tp (update_clock (\<lambda>n. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'

goal (1 subgoal):
 1. (\<And>nn. evaluate_top True env (update_clock (\<lambda>n. nn) s) tp (update_clock (\<lambda>n. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
evaluate_top True env (update_clock (\<lambda>n. nn) s) tp (update_clock (\<lambda>n. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'

goal (1 subgoal):
 1. \<lbrakk>\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'; \<And>ck env s tp s' r cnt. \<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)\<rbrakk> \<Longrightarrow> evaluate_top False env s tp (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_top True env (update_clock (\<lambda>n. nn) s) tp (update_clock (\<lambda>n. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
have "\<forall>n. evaluate_top False env (update_clock (\<lambda>na. n) s) tp (update_clock (\<lambda>na. n) s', r)"
[PROOF STATE]
proof (prove)
using this:
evaluate_top True env (update_clock (\<lambda>n. nn) s) tp (update_clock (\<lambda>n. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'

goal (1 subgoal):
 1. \<forall>n. evaluate_top False env (update_clock (\<lambda>na. n) s) tp (update_clock (\<lambda>na. n) s', r)
[PROOF STEP]
using top_unclocked_ignore
[PROOF STATE]
proof (prove)
using this:
evaluate_top True env (update_clock (\<lambda>n. nn) s) tp (update_clock (\<lambda>n. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
\<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)

goal (1 subgoal):
 1. \<forall>n. evaluate_top False env (update_clock (\<lambda>na. n) s) tp (update_clock (\<lambda>na. n) s', r)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>n. evaluate_top False env (update_clock (\<lambda>na. n) s) tp (update_clock (\<lambda>na. n) s', r)

goal (1 subgoal):
 1. \<lbrakk>\<exists>c. evaluate_top True env (update_clock (\<lambda>_. c) s) tp (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'; \<And>ck env s tp s' r cnt. \<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)\<rbrakk> \<Longrightarrow> evaluate_top False env s tp (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. evaluate_top False env (update_clock (\<lambda>na. n) s) tp (update_clock (\<lambda>na. n) s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n. evaluate_top False env (update_clock (\<lambda>na. n) s) tp (update_clock (\<lambda>na. n) s', r)

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

goal (1 subgoal):
 1. evaluate_top False env s tp (s', r)
[PROOF STEP]
by (metis state.record_simps(7))
[PROOF STATE]
proof (state)
this:
evaluate_top False env s tp (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
evaluate_top False env s tp (s', r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma top_clock_monotone:
  "evaluate_top ck env s tp (s',r) \<Longrightarrow> ck = True \<Longrightarrow> (clock   s') \<le> (clock   s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate_top ck env s tp (s', r); ck = True\<rbrakk> \<Longrightarrow> clock s' \<le> clock s
[PROOF STEP]
by (ind_cases "evaluate_top ck env s tp (s',r)") (fastforce dest:dec_clock_monotone decs_clock_monotone)+


[STATEMENT]
lemma top_sub_from_counter:
  assumes "evaluate_top ck env s tp (s',r)" "ck = True" "(clock   s) = cnt + extra" "(clock   s') = cnt' + extra"
  shows "evaluate_top ck env (s (| clock := cnt |)) tp ((s' (| clock := cnt' |)),r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_top ck 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)
ck = True
clock s = cnt + extra
clock s' = cnt' + extra

goal (1 subgoal):
 1. evaluate_top ck 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>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 2. \<And>d err. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 3. \<And>s2 ds mn specs new_env. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 4. \<And>s2 ds mn specs err. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 5. \<And>ds mn specs. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 6. \<And>mn specs ds. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') 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 = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 2. \<And>d err. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 3. \<And>s2 ds mn specs new_env. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 4. \<And>s2 ds mn specs err. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 5. \<And>ds mn specs. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 6. \<And>mn specs ds. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. 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 ck 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 = 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_top ck env s tp (s', r)
ck = True
clock s = cnt + extra
clock s' = cnt' + extra

goal (1 subgoal):
 1. evaluate_top ck 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 = Rval (make_sem_env (nsLift mn_ (sem_env.v new_env_)) (nsLift mn_ (c new_env_))); evaluate_top True env s (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_, Rval (make_sem_env (nsLift mn_ (sem_env.v new_env_)) (nsLift mn_ (c new_env_)))); ck; clock s = cnt + extra; clock s2_ = cnt' + extra; [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs True [mn_] env s ds_ (s2_, Rval new_env_)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. cnt) s) (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) (update_clock (\<lambda>_. cnt') 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_))); evaluate_top True env s (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_, Rval (make_sem_env (nsLift mn_ (sem_env.v new_env_)) (nsLift mn_ (c new_env_)))); ck; clock s = cnt + extra; clock s2_ = cnt' + extra; [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs True [mn_] env s ds_ (s2_, Rval new_env_)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. cnt) s) (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods (update_clock ?f10 s2_))) (update_clock (\<lambda>_. cnt') 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_))); evaluate_top True env s (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_, Rval (make_sem_env (nsLift mn_ (sem_env.v new_env_)) (nsLift mn_ (c new_env_)))); ck; clock s = cnt + extra; clock s2_ = cnt' + extra; [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs True [mn_] env s ds_ (s2_, Rval new_env_)\<rbrakk> \<Longrightarrow> [mn_] \<notin> defined_mods (update_clock (\<lambda>_. cnt) s) \<and> no_dup_types ds_ \<and> evaluate_decs True [mn_] env (update_clock (\<lambda>_. cnt) s) ds_ (update_clock (\<lambda>_. cnt') s2_, Rval new_env_)
[PROOF STEP]
by (auto dest:decs_sub_from_counter)
[PROOF STATE]
proof (state)
this:
evaluate_top ck env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)

goal (5 subgoals):
 1. \<And>d new_env. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 2. \<And>d err. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 4. \<And>ds mn specs. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 5. \<And>mn specs ds. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. 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>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 2. \<And>d err. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 4. \<And>ds mn specs. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 5. \<And>mn specs ds. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. 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>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 2. \<And>d err. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 4. \<And>ds mn specs. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 5. \<And>mn specs ds. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. 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 ck 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)
ck = True
clock s = cnt + extra
clock s' = cnt' + extra

goal (1 subgoal):
 1. evaluate_top ck 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 True env s (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_, Rerr err_); ck; clock s = cnt + extra; clock s2_ = cnt' + extra; [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs True [mn_] env s ds_ (s2_, Rerr err_)\<rbrakk> \<Longrightarrow> evaluate_top True 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 True env s (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_, Rerr err_); ck; clock s = cnt + extra; clock s2_ = cnt' + extra; [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs True [mn_] env s ds_ (s2_, Rerr err_)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. cnt) s) (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods (update_clock ?f10 s2_))) (update_clock (\<lambda>_. cnt') 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_; evaluate_top True env s (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_, Rerr err_); ck; clock s = cnt + extra; clock s2_ = cnt' + extra; [mn_] \<notin> defined_mods s; no_dup_types ds_; evaluate_decs True [mn_] env s ds_ (s2_, Rerr err_)\<rbrakk> \<Longrightarrow> [mn_] \<notin> defined_mods (update_clock (\<lambda>_. cnt) s) \<and> no_dup_types ds_ \<and> evaluate_decs True [mn_] env (update_clock (\<lambda>_. cnt) s) ds_ (update_clock (\<lambda>_. cnt') s2_, Rerr err_)
[PROOF STEP]
by (auto dest:decs_sub_from_counter)
[PROOF STATE]
proof (state)
this:
evaluate_top ck env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)

goal (4 subgoals):
 1. \<And>d new_env. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 2. \<And>d err. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; tp = Tdec d; r = Rerr err; evaluate_dec ck [] env s d (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top ck env (update_clock (\<lambda>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 3. \<And>ds mn specs. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
 4. \<And>mn specs ds. \<lbrakk>ck = True; clock s = cnt + extra; clock s' = cnt' + extra; 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>_. cnt) s) tp (update_clock (\<lambda>_. cnt') s', r)
[PROOF STEP]
qed (fastforce intro:evaluate_top.intros simp add:dec_sub_from_counter)+


[STATEMENT]
lemma top_add_to_counter:
  assumes "evaluate_top True env s d (s',r)" "r \<noteq> Rerr (Rabort Rtimeout_error)"
  shows "evaluate_top True env (s (| clock := (clock   s) + extra |)) d ((s' (| clock := (clock   s') + extra |)),r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
evaluate_top True env s d (s', r)
r \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>da new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tdec da; r = Rval new_env; evaluate_dec True [] env s da (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 2. \<And>da err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tdec da; r = Rerr err; evaluate_dec True [] env s da (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 3. \<And>s2 ds mn specs new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = 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 True [mn] env s ds (s2, Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 4. \<And>s2 ds mn specs err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = 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 True [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 5. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 6. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
[PROOF STEP]
case tmod1
[PROOF STATE]
proof (state)
this:
d = 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 True [mn_] env s ds_ (s2_, Rval new_env_)

goal (6 subgoals):
 1. \<And>da new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tdec da; r = Rval new_env; evaluate_dec True [] env s da (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 2. \<And>da err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tdec da; r = Rerr err; evaluate_dec True [] env s da (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 3. \<And>s2 ds mn specs new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = 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 True [mn] env s ds (s2, Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 4. \<And>s2 ds mn specs err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = 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 True [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 5. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 6. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d = 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 True [mn_] env s ds_ (s2_, Rval new_env_)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d = 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 True [mn_] env s ds_ (s2_, Rval new_env_)

goal (1 subgoal):
 1. evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d = 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 True [mn_] env s ds_ (s2_, Rval new_env_)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) (update_clock (\<lambda>_. clock s2_ + extra) 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>d = 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 True [mn_] env s ds_ (s2_, Rval new_env_)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods (update_clock ?f6 s2_))) (update_clock (\<lambda>_. clock s2_ + extra) 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>d = 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 True [mn_] env s ds_ (s2_, Rval new_env_)\<rbrakk> \<Longrightarrow> [mn_] \<notin> defined_mods (update_clock (\<lambda>_. clock s + extra) s) \<and> no_dup_types ds_ \<and> evaluate_decs True [mn_] env (update_clock (\<lambda>_. clock s + extra) s) ds_ (update_clock (\<lambda>_. clock s2_ + extra) s2_, Rval new_env_)
[PROOF STEP]
by (auto dest:decs_add_to_counter)
[PROOF STATE]
proof (state)
this:
evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)

goal (5 subgoals):
 1. \<And>da new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tdec da; r = Rval new_env; evaluate_dec True [] env s da (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 2. \<And>da err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tdec da; r = Rerr err; evaluate_dec True [] env s da (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = 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 True [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 4. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 5. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>da new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tdec da; r = Rval new_env; evaluate_dec True [] env s da (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 2. \<And>da err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tdec da; r = Rerr err; evaluate_dec True [] env s da (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = 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 True [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 4. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 5. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
[PROOF STEP]
case tmod2
[PROOF STATE]
proof (state)
this:
d = 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 True [mn_] env s ds_ (s2_, Rerr err_)

goal (5 subgoals):
 1. \<And>da new_env. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tdec da; r = Rval new_env; evaluate_dec True [] env s da (s', Rval new_env)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 2. \<And>da err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tdec da; r = Rerr err; evaluate_dec True [] env s da (s', Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 3. \<And>s2 ds mn specs err. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = 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 True [mn] env s ds (s2, Rerr err)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 4. \<And>ds mn specs. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); \<not> no_dup_types ds\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
 5. \<And>mn specs ds. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); d = Tmod mn specs ds; s' = s; r = Rerr (Rabort Rtype_error); [mn] \<in> defined_mods s\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d = 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 True [mn_] env s ds_ (s2_, Rerr err_)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d = 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 True [mn_] env s ds_ (s2_, Rerr err_)

goal (1 subgoal):
 1. evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
d = 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 True [mn_] env s ds_ (s2_, Rerr err_)
evaluate_top True env s d (s', r)
r \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d = Tmod mn_ specs_ ds_; s' = update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_; r = Rerr err_; evaluate_top True 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 True [mn_] env s ds_ (s2_, Rerr err_)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) (update_clock (\<lambda>_. clock s2_ + extra) s2_), Rerr err_)
[PROOF STEP]
apply (subst state.record_simps(5)[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d = Tmod mn_ specs_ ds_; s' = update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_; r = Rerr err_; evaluate_top True 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 True [mn_] env s ds_ (s2_, Rerr err_)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) (Tmod mn_ specs_ ds_) (update_defined_mods (\<lambda>_. insert [mn_] (defined_mods (update_clock ?f8 s2_))) (update_clock (\<lambda>_. clock s2_ + extra) s2_), Rerr err_)
[PROOF STEP]
apply (rule evaluate_top.tmod2[simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d = Tmod mn_ specs_ ds_; s' = update_defined_mods (\<lambda>_. insert [mn_] (defined_mods s2_)) s2_; r = Rerr err_; evaluate_top True 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 True [mn_] env s ds_ (s2_, Rerr err_)\<rbrakk> \<Longrightarrow> [mn_] \<notin> defined_mods (update_clock (\<lambda>_. clock s + extra) s) \<and> no_dup_types ds_ \<and> evaluate_decs True [mn_] env (update_clock (\<lambda>_. clock s + extra) s) ds_ (update_clock (\<lambda>_. clock s2_ + extra) s2_, Rerr err_)
[PROOF STEP]
by (auto dest:decs_add_to_counter)
[PROOF STATE]
proof (state)
this:
evaluate_top True env (update_clock (\<lambda>_. clock s + extra) s) d (update_clock (\<lambda>_. clock s' + extra) s', r)

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


[STATEMENT]
lemma prog_clock_monotone:
  "evaluate_prog ck env s prog res \<Longrightarrow> ck \<Longrightarrow> (clock (fst res)) \<le> (clock s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate_prog ck env s prog res; ck\<rbrakk> \<Longrightarrow> clock (fst res) \<le> clock s
[PROOF STEP]
by (induction rule:evaluate_prog.inducts) (auto dest:top_clock_monotone)


[STATEMENT]
lemma prog_unclocked_ignore:
  "evaluate_prog ck env s prog res \<Longrightarrow> \<forall>cnt s' r. res = (s',r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error)
    \<longrightarrow> evaluate_prog False env (s (| clock := cnt |)) prog ((s' (| clock := cnt |)),r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_prog ck env s prog res \<Longrightarrow> \<forall>cnt s' r. res = (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_prog False env (update_clock (\<lambda>_. cnt) s) prog (update_clock (\<lambda>_. cnt) s', r)
[PROOF STEP]
by (induction rule:evaluate_prog.inducts) (auto intro!:evaluate_prog.intros dest:top_unclocked_ignore)