[STATEMENT]
lemma prog_unclocked_unchanged:
  "evaluate_prog ck env s prog res \<Longrightarrow> \<not>ck \<Longrightarrow>(snd res) \<noteq> Rerr (Rabort Rtimeout_error) \<and> (clock   (fst res)) = (clock s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate_prog ck env s prog res; \<not> ck\<rbrakk> \<Longrightarrow> snd res \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst res) = clock s
[PROOF STEP]
proof (induction rule:evaluate_prog.inducts)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ck env s. \<not> ck \<Longrightarrow> snd (s, Rval (make_sem_env nsEmpty nsEmpty)) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s, Rval (make_sem_env nsEmpty nsEmpty))) = clock s
 2. \<And>ck s1 s2 s3 env top0 tops new_env r. \<lbrakk>evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<not> ck \<longrightarrow> snd (s3, r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, r)) = clock s2); \<not> ck\<rbrakk> \<Longrightarrow> snd (s3, combine_dec_result new_env r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, combine_dec_result new_env r)) = clock s1
 3. \<And>ck s1 s2 env top0 tops err. \<lbrakk>evaluate_top ck env s1 top0 (s2, Rerr err); \<not> ck\<rbrakk> \<Longrightarrow> snd (s2, Rerr err) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s2, Rerr err)) = clock s1
[PROOF STEP]
case (cons1 ck s1 s2 s3 env top0 tops new_env r)
[PROOF STATE]
proof (state)
this:
evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<not> ck \<longrightarrow> snd (s3, r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, r)) = clock s2)
\<not> ck

goal (3 subgoals):
 1. \<And>ck env s. \<not> ck \<Longrightarrow> snd (s, Rval (make_sem_env nsEmpty nsEmpty)) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s, Rval (make_sem_env nsEmpty nsEmpty))) = clock s
 2. \<And>ck s1 s2 s3 env top0 tops new_env r. \<lbrakk>evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<not> ck \<longrightarrow> snd (s3, r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, r)) = clock s2); \<not> ck\<rbrakk> \<Longrightarrow> snd (s3, combine_dec_result new_env r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, combine_dec_result new_env r)) = clock s1
 3. \<And>ck s1 s2 env top0 tops err. \<lbrakk>evaluate_top ck env s1 top0 (s2, Rerr err); \<not> ck\<rbrakk> \<Longrightarrow> snd (s2, Rerr err) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s2, Rerr err)) = clock s1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<not> ck \<longrightarrow> snd (s3, r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, r)) = clock s2)
\<not> ck
[PROOF STEP]
have "r \<noteq> Rerr (Rabort Rtimeout_error)"
[PROOF STATE]
proof (prove)
using this:
evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<not> ck \<longrightarrow> snd (s3, r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, r)) = clock s2)
\<not> ck

goal (1 subgoal):
 1. r \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r \<noteq> Rerr (Rabort Rtimeout_error)

goal (3 subgoals):
 1. \<And>ck env s. \<not> ck \<Longrightarrow> snd (s, Rval (make_sem_env nsEmpty nsEmpty)) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s, Rval (make_sem_env nsEmpty nsEmpty))) = clock s
 2. \<And>ck s1 s2 s3 env top0 tops new_env r. \<lbrakk>evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<not> ck \<longrightarrow> snd (s3, r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, r)) = clock s2); \<not> ck\<rbrakk> \<Longrightarrow> snd (s3, combine_dec_result new_env r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, combine_dec_result new_env r)) = clock s1
 3. \<And>ck s1 s2 env top0 tops err. \<lbrakk>evaluate_top ck env s1 top0 (s2, Rerr err); \<not> ck\<rbrakk> \<Longrightarrow> snd (s2, Rerr err) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s2, Rerr err)) = clock s1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r \<noteq> Rerr (Rabort Rtimeout_error)

goal (3 subgoals):
 1. \<And>ck env s. \<not> ck \<Longrightarrow> snd (s, Rval (make_sem_env nsEmpty nsEmpty)) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s, Rval (make_sem_env nsEmpty nsEmpty))) = clock s
 2. \<And>ck s1 s2 s3 env top0 tops new_env r. \<lbrakk>evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<not> ck \<longrightarrow> snd (s3, r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, r)) = clock s2); \<not> ck\<rbrakk> \<Longrightarrow> snd (s3, combine_dec_result new_env r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, combine_dec_result new_env r)) = clock s1
 3. \<And>ck s1 s2 env top0 tops err. \<lbrakk>evaluate_top ck env s1 top0 (s2, Rerr err); \<not> ck\<rbrakk> \<Longrightarrow> snd (s2, Rerr err) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s2, Rerr err)) = clock s1
[PROOF STEP]
from cons1
[PROOF STATE]
proof (chain)
picking this:
evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<not> ck \<longrightarrow> snd (s3, r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, r)) = clock s2)
\<not> ck
[PROOF STEP]
have "clock s1 = clock s2"
[PROOF STATE]
proof (prove)
using this:
evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<not> ck \<longrightarrow> snd (s3, r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, r)) = clock s2)
\<not> ck

goal (1 subgoal):
 1. clock s1 = clock s2
[PROOF STEP]
using top_unclocked
[PROOF STATE]
proof (prove)
using this:
evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<not> ck \<longrightarrow> snd (s3, r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, r)) = clock s2)
\<not> ck
(evaluate_top False ?env ?s ?tp (?s', ?r) \<longrightarrow> ?r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock ?s = clock ?s') \<and> evaluate_top False ?env (update_clock (\<lambda>_. ?count1.0) ?s) ?tp (update_clock (\<lambda>_. ?count1.0) ?s', ?r) = evaluate_top False ?env (update_clock (\<lambda>_. ?count2.0) ?s) ?tp (update_clock (\<lambda>_. ?count2.0) ?s', ?r)

goal (1 subgoal):
 1. clock s1 = clock s2
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
clock s1 = clock s2

goal (3 subgoals):
 1. \<And>ck env s. \<not> ck \<Longrightarrow> snd (s, Rval (make_sem_env nsEmpty nsEmpty)) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s, Rval (make_sem_env nsEmpty nsEmpty))) = clock s
 2. \<And>ck s1 s2 s3 env top0 tops new_env r. \<lbrakk>evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<not> ck \<longrightarrow> snd (s3, r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, r)) = clock s2); \<not> ck\<rbrakk> \<Longrightarrow> snd (s3, combine_dec_result new_env r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, combine_dec_result new_env r)) = clock s1
 3. \<And>ck s1 s2 env top0 tops err. \<lbrakk>evaluate_top ck env s1 top0 (s2, Rerr err); \<not> ck\<rbrakk> \<Longrightarrow> snd (s2, Rerr err) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s2, Rerr err)) = clock s1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r \<noteq> Rerr (Rabort Rtimeout_error)
clock s1 = clock s2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
r \<noteq> Rerr (Rabort Rtimeout_error)
clock s1 = clock s2

goal (1 subgoal):
 1. snd (s3, combine_dec_result new_env r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, combine_dec_result new_env r)) = clock s1
[PROOF STEP]
using combine_dec_result.simps cons1
[PROOF STATE]
proof (prove)
using this:
r \<noteq> Rerr (Rabort Rtimeout_error)
clock s1 = clock s2
combine_dec_result ?env (Rerr ?e) = Rerr ?e
combine_dec_result ?env (Rval ?env') = Rval (make_sem_env (nsAppend (sem_env.v ?env') (sem_env.v ?env)) (nsAppend (c ?env') (c ?env)))
evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<not> ck \<longrightarrow> snd (s3, r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, r)) = clock s2)
\<not> ck

goal (1 subgoal):
 1. snd (s3, combine_dec_result new_env r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, combine_dec_result new_env r)) = clock s1
[PROOF STEP]
by (cases r;auto)
[PROOF STATE]
proof (state)
this:
snd (s3, combine_dec_result new_env r) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s3, combine_dec_result new_env r)) = clock s1

goal (2 subgoals):
 1. \<And>ck env s. \<not> ck \<Longrightarrow> snd (s, Rval (make_sem_env nsEmpty nsEmpty)) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s, Rval (make_sem_env nsEmpty nsEmpty))) = clock s
 2. \<And>ck s1 s2 env top0 tops err. \<lbrakk>evaluate_top ck env s1 top0 (s2, Rerr err); \<not> ck\<rbrakk> \<Longrightarrow> snd (s2, Rerr err) \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst (s2, Rerr err)) = clock s1
[PROOF STEP]
qed (auto simp add: top_clocked_unclocked_equiv)


[STATEMENT]
lemma prog_unclocked_1:
  assumes "evaluate_prog False env s prog (s',r)"
  shows "r \<noteq> Rerr (Rabort Rtimeout_error) \<and> (clock s = clock s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
evaluate_prog False env s prog (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate_prog False env s prog (s', r)

goal (1 subgoal):
 1. r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
using prog_unclocked_unchanged
[PROOF STATE]
proof (prove)
using this:
evaluate_prog False env s prog (s', r)
\<lbrakk>evaluate_prog ?ck ?env ?s ?prog ?res; \<not> ?ck\<rbrakk> \<Longrightarrow> snd ?res \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock (fst ?res) = clock ?s

goal (1 subgoal):
 1. r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prog_unclocked_2:
  assumes "evaluate_prog False env (s \<lparr> clock := cnt1 \<rparr>) prog (s' \<lparr> clock := cnt1 \<rparr>,r)"
  shows "evaluate_prog False env (s \<lparr> clock := cnt2 \<rparr>) prog (s' \<lparr> clock := cnt2 \<rparr>,r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_prog False env (update_clock (\<lambda>_. cnt2) s) prog (update_clock (\<lambda>_. cnt2) s', r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. evaluate_prog False env (update_clock (\<lambda>_. cnt2) s) prog (update_clock (\<lambda>_. cnt2) s', r)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
evaluate_prog False env (update_clock (\<lambda>_. cnt1) s) prog (update_clock (\<lambda>_. cnt1) s', r)
[PROOF STEP]
have "r \<noteq> Rerr (Rabort Rtimeout_error)"
[PROOF STATE]
proof (prove)
using this:
evaluate_prog False env (update_clock (\<lambda>_. cnt1) s) prog (update_clock (\<lambda>_. cnt1) s', r)

goal (1 subgoal):
 1. r \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
using prog_unclocked_1
[PROOF STATE]
proof (prove)
using this:
evaluate_prog False env (update_clock (\<lambda>_. cnt1) s) prog (update_clock (\<lambda>_. cnt1) s', r)
evaluate_prog False ?env ?s ?prog (?s', ?r) \<Longrightarrow> ?r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock ?s = clock ?s'

goal (1 subgoal):
 1. r \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. evaluate_prog False env (update_clock (\<lambda>_. cnt2) s) prog (update_clock (\<lambda>_. cnt2) s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. evaluate_prog False env (update_clock (\<lambda>_. cnt2) s) prog (update_clock (\<lambda>_. cnt2) s', r)
[PROOF STEP]
using prog_unclocked_ignore assms
[PROOF STATE]
proof (prove)
using this:
r \<noteq> Rerr (Rabort Rtimeout_error)
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)
evaluate_prog False env (update_clock (\<lambda>_. cnt1) s) prog (update_clock (\<lambda>_. cnt1) s', r)

goal (1 subgoal):
 1. evaluate_prog False env (update_clock (\<lambda>_. cnt2) s) prog (update_clock (\<lambda>_. cnt2) s', r)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
evaluate_prog False env (update_clock (\<lambda>_. cnt2) s) prog (update_clock (\<lambda>_. cnt2) s', r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prog_unclocked:
  "(evaluate_prog False env s prog (s',r) \<longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> (clock s = clock s')) \<and>
   (evaluate_prog False env (s \<lparr> clock := cnt1 \<rparr>) prog (s' \<lparr> clock := cnt1 \<rparr>,r) =
   evaluate_prog False env (s \<lparr> clock := cnt2 \<rparr>) prog (s' \<lparr> clock := cnt2 \<rparr>,r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (evaluate_prog False env s prog (s', r) \<longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s') \<and> evaluate_prog False env (update_clock (\<lambda>_. cnt1) s) prog (update_clock (\<lambda>_. cnt1) s', r) = evaluate_prog False env (update_clock (\<lambda>_. cnt2) s) prog (update_clock (\<lambda>_. cnt2) s', r)
[PROOF STEP]
using prog_unclocked_1 prog_unclocked_2
[PROOF STATE]
proof (prove)
using this:
evaluate_prog False ?env ?s ?prog (?s', ?r) \<Longrightarrow> ?r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock ?s = clock ?s'
evaluate_prog False ?env (update_clock (\<lambda>_. ?cnt1.0) ?s) ?prog (update_clock (\<lambda>_. ?cnt1.0) ?s', ?r) \<Longrightarrow> evaluate_prog False ?env (update_clock (\<lambda>_. ?cnt2.0) ?s) ?prog (update_clock (\<lambda>_. ?cnt2.0) ?s', ?r)

goal (1 subgoal):
 1. (evaluate_prog False env s prog (s', r) \<longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s') \<and> evaluate_prog False env (update_clock (\<lambda>_. cnt1) s) prog (update_clock (\<lambda>_. cnt1) s', r) = evaluate_prog False env (update_clock (\<lambda>_. cnt2) s) prog (update_clock (\<lambda>_. cnt2) s', r)
[PROOF STEP]
by blast


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

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

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

goal (1 subgoal):
 1. \<exists>r. evaluate_prog True env s [] r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
using evaluate_prog.intros(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>res. \<not> evaluate_prog False env s [] res
evaluate_prog ?ck ?env ?s [] (?s, Rval (make_sem_env nsEmpty nsEmpty))

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

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

goal (1 subgoal):
 1. \<And>a prog env s. \<lbrakk>\<And>env s. \<forall>res. \<not> evaluate_prog False env s prog res \<Longrightarrow> \<exists>r. evaluate_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error); \<forall>res. \<not> evaluate_prog False env s (a # prog) res\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_prog True env s (a # prog) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
obtain s' r where top0:"evaluate_top True env s top0 (s',r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s' r. evaluate_top True env s top0 (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using top_clocked_total[simplified]
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. evaluate_top True ?env ?s ?tp (a, b)

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

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

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

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

goal (1 subgoal):
 1. evaluate_prog False (extend_dec_env new_env env) s' tops (s3, r) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_prog False (extend_dec_env new_env env) s' tops (s3, r)
[PROOF STEP]
have "r \<noteq> Rerr (Rabort Rtimeout_error)"
[PROOF STATE]
proof (prove)
using this:
evaluate_prog False (extend_dec_env new_env env) s' tops (s3, r)

goal (1 subgoal):
 1. r \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
using prog_unclocked
[PROOF STATE]
proof (prove)
using this:
evaluate_prog False (extend_dec_env new_env env) s' tops (s3, r)
(evaluate_prog False ?env ?s ?prog (?s', ?r) \<longrightarrow> ?r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock ?s = clock ?s') \<and> evaluate_prog False ?env (update_clock (\<lambda>_. ?cnt1.0) ?s) ?prog (update_clock (\<lambda>_. ?cnt1.0) ?s', ?r) = evaluate_prog False ?env (update_clock (\<lambda>_. ?cnt2.0) ?s) ?prog (update_clock (\<lambda>_. ?cnt2.0) ?s', ?r)

goal (1 subgoal):
 1. r \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
r \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. evaluate_prog False (extend_dec_env new_env env) s' tops (s3, r) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. evaluate_prog False (extend_dec_env new_env env) s' tops (s3, r) \<Longrightarrow> False
[PROOF STEP]
from top0
[PROOF STATE]
proof (chain)
picking this:
evaluate_top True env s top0 (s', r__)
[PROOF STEP]
have "evaluate_top False env s top0 (update_clock (\<lambda>_. clock s) s', Rval new_env)"
[PROOF STATE]
proof (prove)
using this:
evaluate_top True env s top0 (s', r__)

goal (1 subgoal):
 1. evaluate_top False env s top0 (update_clock (\<lambda>_. clock s) s', Rval new_env)
[PROOF STEP]
unfolding Rval
[PROOF STATE]
proof (prove)
using this:
evaluate_top True env s top0 (s', Rval new_env)

goal (1 subgoal):
 1. evaluate_top False env s top0 (update_clock (\<lambda>_. clock s) s', Rval new_env)
[PROOF STEP]
using top_unclocked_ignore
[PROOF STATE]
proof (prove)
using this:
evaluate_top True env s top0 (s', Rval new_env)
\<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 top0 (update_clock (\<lambda>_. clock s) s', Rval new_env)
[PROOF STEP]
by (metis (full_types) result.distinct(1) state.record_simps(7))
[PROOF STATE]
proof (state)
this:
evaluate_top False env s top0 (update_clock (\<lambda>_. clock s) s', Rval new_env)

goal (1 subgoal):
 1. evaluate_prog False (extend_dec_env new_env env) s' tops (s3, r) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r \<noteq> Rerr (Rabort Rtimeout_error)
evaluate_top False env s top0 (update_clock (\<lambda>_. clock s) s', Rval new_env)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
r \<noteq> Rerr (Rabort Rtimeout_error)
evaluate_top False env s top0 (update_clock (\<lambda>_. clock s) s', Rval new_env)

goal (1 subgoal):
 1. False
[PROOF STEP]
using prog_unclocked_ignore[rule_format] Cons.prems evaluate_prog.cons1 tops
[PROOF STATE]
proof (prove)
using this:
r \<noteq> Rerr (Rabort Rtimeout_error)
evaluate_top False env s top0 (update_clock (\<lambda>_. clock s) s', Rval new_env)
\<lbrakk>evaluate_prog ?ck ?env ?s ?prog ?res; ?res = (?s', ?r) \<and> ?r \<noteq> Rerr (Rabort Rtimeout_error)\<rbrakk> \<Longrightarrow> evaluate_prog False ?env (update_clock (\<lambda>_. ?cnt) ?s) ?prog (update_clock (\<lambda>_. ?cnt) ?s', ?r)
\<forall>res. \<not> evaluate_prog False env s (top0 # tops) res
evaluate_top ?ck ?env ?s1.0 ?top0.0 (?s2.0, Rval ?new_env) \<and> evaluate_prog ?ck (extend_dec_env ?new_env ?env) ?s2.0 ?tops (?s3.0, ?r) \<Longrightarrow> evaluate_prog ?ck ?env ?s1.0 (?top0.0 # ?tops) (?s3.0, combine_dec_result ?new_env ?r)
evaluate_prog False (extend_dec_env new_env env) s' tops (s3, r)

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evaluate_top True env s top0 (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_prog True env s (top0 # tops) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evaluate_top True env s top0 (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_prog True env s (top0 # tops) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
case (Rerr err)
[PROOF STATE]
proof (state)
this:
r = Rerr err

goal (1 subgoal):
 1. \<And>x2. \<lbrakk>evaluate_top True env s top0 (s', r); r = Rerr x2\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_prog True env s (top0 # tops) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
have "err = Rabort Rtimeout_error"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. err = Rabort Rtimeout_error
[PROOF STEP]
using Cons top0 top_unclocked_ignore
[PROOF STATE]
proof (prove)
using this:
\<forall>res. \<not> evaluate_prog False ?env ?s tops res \<Longrightarrow> \<exists>r. evaluate_prog True ?env ?s tops r \<and> snd r = Rerr (Rabort Rtimeout_error)
\<forall>res. \<not> evaluate_prog False env s (top0 # tops) res
evaluate_top True env s top0 (s', r)
\<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. err = Rabort Rtimeout_error
[PROOF STEP]
unfolding Rerr
[PROOF STATE]
proof (prove)
using this:
\<forall>res. \<not> evaluate_prog False ?env ?s tops res \<Longrightarrow> \<exists>r. evaluate_prog True ?env ?s tops r \<and> snd r = Rerr (Rabort Rtimeout_error)
\<forall>res. \<not> evaluate_prog False env s (top0 # tops) res
evaluate_top True env s top0 (s', Rerr err)
\<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. err = Rabort Rtimeout_error
[PROOF STEP]
by (metis evaluate_prog.cons2 result.inject(2) state.record_simps(7))
[PROOF STATE]
proof (state)
this:
err = Rabort Rtimeout_error

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

goal (1 subgoal):
 1. \<exists>r. evaluate_prog True env s (top0 # tops) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
using top0
[PROOF STATE]
proof (prove)
using this:
err = Rabort Rtimeout_error
evaluate_top True env s top0 (s', r)

goal (1 subgoal):
 1. \<exists>r. evaluate_prog True env s (top0 # tops) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
unfolding Rerr
[PROOF STATE]
proof (prove)
using this:
err = Rabort Rtimeout_error
evaluate_top True env s top0 (s', Rerr err)

goal (1 subgoal):
 1. \<exists>r. evaluate_prog True env s (top0 # tops) r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
by (meson evaluate_prog.cons2 snd_conv)
[PROOF STATE]
proof (state)
this:
\<exists>r. evaluate_prog True env s (top0 # tops) r \<and> snd r = Rerr (Rabort Rtimeout_error)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_evaluate_whole_prog_timeout:
  assumes "\<forall>res. \<not>evaluate_whole_prog False env s prog res"
  shows "\<exists>r. evaluate_whole_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error)" (is ?P)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_whole_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r. evaluate_whole_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
show ?P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. evaluate_whole_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply (cases "no_dup_mods prog (defined_mods s)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. no_dup_mods prog (defined_mods s) \<Longrightarrow> \<exists>r. evaluate_whole_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<not> no_dup_mods prog (defined_mods s) \<Longrightarrow> \<exists>r. evaluate_whole_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply (cases "no_dup_top_types prog (defined_types s)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>no_dup_mods prog (defined_mods s); no_dup_top_types prog (defined_types s)\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_whole_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<lbrakk>no_dup_mods prog (defined_mods s); \<not> no_dup_top_types prog (defined_types s)\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_whole_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error)
 3. \<not> no_dup_mods prog (defined_mods s) \<Longrightarrow> \<exists>r. evaluate_whole_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
using not_evaluate_prog_timeout assms
[PROOF STATE]
proof (prove)
using this:
\<forall>res. \<not> evaluate_prog False ?env ?s ?prog res \<Longrightarrow> \<exists>r. evaluate_prog True ?env ?s ?prog r \<and> snd r = Rerr (Rabort Rtimeout_error)
\<forall>res. \<not> evaluate_whole_prog False env s prog res

goal (3 subgoals):
 1. \<lbrakk>no_dup_mods prog (defined_mods s); no_dup_top_types prog (defined_types s)\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_whole_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error)
 2. \<lbrakk>no_dup_mods prog (defined_mods s); \<not> no_dup_top_types prog (defined_types s)\<rbrakk> \<Longrightarrow> \<exists>r. evaluate_whole_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error)
 3. \<not> no_dup_mods prog (defined_mods s) \<Longrightarrow> \<exists>r. evaluate_whole_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
\<exists>r. evaluate_whole_prog True env s prog r \<and> snd r = Rerr (Rabort Rtimeout_error)

goal:
No subgoals!
[PROOF STEP]
qed


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


[STATEMENT]
lemma prog_sub_from_counter:
  "evaluate_prog ck env s prog res \<Longrightarrow>
   \<forall>extra cnt cnt' s' r.
     (clock   s) = extra + cnt \<and> (clock   s') = extra + cnt' \<and> res = (s',r) \<and> ck = True \<longrightarrow>
     evaluate_prog ck 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>extra cnt cnt' s' r. clock s = extra + cnt \<and> clock s' = extra + cnt' \<and> res = (s', r) \<and> ck = True \<longrightarrow> evaluate_prog ck env (update_clock (\<lambda>_. cnt) s) prog (update_clock (\<lambda>_. cnt') s', r)
[PROOF STEP]
proof (induction rule:evaluate_prog.inducts)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ck env s. \<forall>extra cnt cnt' s' r. clock s = extra + cnt \<and> clock s' = extra + cnt' \<and> (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = True \<longrightarrow> evaluate_prog ck env (update_clock (\<lambda>_. cnt) s) [] (update_clock (\<lambda>_. cnt') s', r)
 2. \<And>ck s1 s2 s3 env top0 tops new_env r. evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<forall>extra cnt cnt' s' ra. clock s2 = extra + cnt \<and> clock s' = extra + cnt' \<and> (s3, r) = (s', ra) \<and> ck = True \<longrightarrow> evaluate_prog ck (extend_dec_env new_env env) (update_clock (\<lambda>_. cnt) s2) tops (update_clock (\<lambda>_. cnt') s', ra)) \<Longrightarrow> \<forall>extra cnt cnt' s' ra. clock s1 = extra + cnt \<and> clock s' = extra + cnt' \<and> (s3, combine_dec_result new_env r) = (s', ra) \<and> ck = True \<longrightarrow> evaluate_prog ck env (update_clock (\<lambda>_. cnt) s1) (top0 # tops) (update_clock (\<lambda>_. cnt') s', ra)
 3. \<And>ck s1 s2 env top0 tops err. evaluate_top ck env s1 top0 (s2, Rerr err) \<Longrightarrow> \<forall>extra cnt cnt' s' r. clock s1 = extra + cnt \<and> clock s' = extra + cnt' \<and> (s2, Rerr err) = (s', r) \<and> ck = True \<longrightarrow> evaluate_prog ck env (update_clock (\<lambda>_. cnt) s1) (top0 # tops) (update_clock (\<lambda>_. cnt') s', r)
[PROOF STEP]
case (cons1 ck s1 s2 s3 env top0 tops new_env r)
[PROOF STATE]
proof (state)
this:
evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<forall>extra cnt cnt' s' ra. clock s2 = extra + cnt \<and> clock s' = extra + cnt' \<and> (s3, r) = (s', ra) \<and> ck = True \<longrightarrow> evaluate_prog ck (extend_dec_env new_env env) (update_clock (\<lambda>_. cnt) s2) tops (update_clock (\<lambda>_. cnt') s', ra))

goal (3 subgoals):
 1. \<And>ck env s. \<forall>extra cnt cnt' s' r. clock s = extra + cnt \<and> clock s' = extra + cnt' \<and> (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = True \<longrightarrow> evaluate_prog ck env (update_clock (\<lambda>_. cnt) s) [] (update_clock (\<lambda>_. cnt') s', r)
 2. \<And>ck s1 s2 s3 env top0 tops new_env r. evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<forall>extra cnt cnt' s' ra. clock s2 = extra + cnt \<and> clock s' = extra + cnt' \<and> (s3, r) = (s', ra) \<and> ck = True \<longrightarrow> evaluate_prog ck (extend_dec_env new_env env) (update_clock (\<lambda>_. cnt) s2) tops (update_clock (\<lambda>_. cnt') s', ra)) \<Longrightarrow> \<forall>extra cnt cnt' s' ra. clock s1 = extra + cnt \<and> clock s' = extra + cnt' \<and> (s3, combine_dec_result new_env r) = (s', ra) \<and> ck = True \<longrightarrow> evaluate_prog ck env (update_clock (\<lambda>_. cnt) s1) (top0 # tops) (update_clock (\<lambda>_. cnt') s', ra)
 3. \<And>ck s1 s2 env top0 tops err. evaluate_top ck env s1 top0 (s2, Rerr err) \<Longrightarrow> \<forall>extra cnt cnt' s' r. clock s1 = extra + cnt \<and> clock s' = extra + cnt' \<and> (s2, Rerr err) = (s', r) \<and> ck = True \<longrightarrow> evaluate_prog ck env (update_clock (\<lambda>_. cnt) s1) (top0 # tops) (update_clock (\<lambda>_. cnt') s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<forall>extra cnt cnt' s' ra. clock s2 = extra + cnt \<and> clock s' = extra + cnt' \<and> (s3, r) = (s', ra) \<and> ck = True \<longrightarrow> evaluate_prog ck (extend_dec_env new_env env) (update_clock (\<lambda>_. cnt) s2) tops (update_clock (\<lambda>_. cnt') s', ra))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
evaluate_top ck env s1 top0 (s2, Rval new_env) \<and> evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<forall>extra cnt cnt' s' ra. clock s2 = extra + cnt \<and> clock s' = extra + cnt' \<and> (s3, r) = (s', ra) \<and> ck = True \<longrightarrow> evaluate_prog ck (extend_dec_env new_env env) (update_clock (\<lambda>_. cnt) s2) tops (update_clock (\<lambda>_. cnt') s', ra))

goal (1 subgoal):
 1. \<forall>extra cnt cnt' s' ra. clock s1 = extra + cnt \<and> clock s' = extra + cnt' \<and> (s3, combine_dec_result new_env r) = (s', ra) \<and> ck = True \<longrightarrow> evaluate_prog ck env (update_clock (\<lambda>_. cnt) s1) (top0 # tops) (update_clock (\<lambda>_. cnt') s', ra)
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>extra cnt cnt'. \<lbrakk>evaluate_top True env s1 top0 (s2, Rval new_env); evaluate_prog True (extend_dec_env new_env env) s2 tops (s3, r); \<forall>extraa cnt cnt'a. clock s2 = extraa + cnt \<and> extra + cnt' = extraa + cnt'a \<longrightarrow> evaluate_prog True (extend_dec_env new_env env) (update_clock (\<lambda>_. cnt) s2) tops (update_clock (\<lambda>_. cnt'a) s3, r); clock s1 = extra + cnt; clock s3 = extra + cnt'; ck\<rbrakk> \<Longrightarrow> evaluate_prog True env (update_clock (\<lambda>_. cnt) s1) (top0 # tops) (update_clock (\<lambda>_. cnt') s3, combine_dec_result new_env r)
[PROOF STEP]
subgoal for extra
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate_top True env s1 top0 (s2, Rval new_env); evaluate_prog True (extend_dec_env new_env env) s2 tops (s3, r); \<forall>extraa cnt cnt'a. clock s2 = extraa + cnt \<and> extra + cnt'_ = extraa + cnt'a \<longrightarrow> evaluate_prog True (extend_dec_env new_env env) (update_clock (\<lambda>_. cnt) s2) tops (update_clock (\<lambda>_. cnt'a) s3, r); clock s1 = extra + cnt_; clock s3 = extra + cnt'_; ck\<rbrakk> \<Longrightarrow> evaluate_prog True env (update_clock (\<lambda>_. cnt_) s1) (top0 # tops) (update_clock (\<lambda>_. cnt'_) s3, combine_dec_result new_env r)
[PROOF STEP]
apply (subgoal_tac "clock   s2 \<ge> extra")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>evaluate_top True env s1 top0 (s2, Rval new_env); evaluate_prog True (extend_dec_env new_env env) s2 tops (s3, r); \<forall>extraa cnt cnt'a. clock s2 = extraa + cnt \<and> extra + cnt'_ = extraa + cnt'a \<longrightarrow> evaluate_prog True (extend_dec_env new_env env) (update_clock (\<lambda>_. cnt) s2) tops (update_clock (\<lambda>_. cnt'a) s3, r); clock s1 = extra + cnt_; clock s3 = extra + cnt'_; ck; extra \<le> clock s2\<rbrakk> \<Longrightarrow> evaluate_prog True env (update_clock (\<lambda>_. cnt_) s1) (top0 # tops) (update_clock (\<lambda>_. cnt'_) s3, combine_dec_result new_env r)
 2. \<lbrakk>evaluate_top True env s1 top0 (s2, Rval new_env); evaluate_prog True (extend_dec_env new_env env) s2 tops (s3, r); \<forall>extraa cnt cnt'a. clock s2 = extraa + cnt \<and> extra + cnt'_ = extraa + cnt'a \<longrightarrow> evaluate_prog True (extend_dec_env new_env env) (update_clock (\<lambda>_. cnt) s2) tops (update_clock (\<lambda>_. cnt'a) s3, r); clock s1 = extra + cnt_; clock s3 = extra + cnt'_; ck\<rbrakk> \<Longrightarrow> extra \<le> clock s2
[PROOF STEP]
apply (drule_tac x="extra" in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>evaluate_top True env s1 top0 (s2, Rval new_env); evaluate_prog True (extend_dec_env new_env env) s2 tops (s3, r); clock s1 = extra + cnt_; clock s3 = extra + cnt'_; ck; extra \<le> clock s2; \<forall>cnt cnt'a. clock s2 = extra + cnt \<and> extra + cnt'_ = extra + cnt'a \<longrightarrow> evaluate_prog True (extend_dec_env new_env env) (update_clock (\<lambda>_. cnt) s2) tops (update_clock (\<lambda>_. cnt'a) s3, r)\<rbrakk> \<Longrightarrow> evaluate_prog True env (update_clock (\<lambda>_. cnt_) s1) (top0 # tops) (update_clock (\<lambda>_. cnt'_) s3, combine_dec_result new_env r)
 2. \<lbrakk>evaluate_top True env s1 top0 (s2, Rval new_env); evaluate_prog True (extend_dec_env new_env env) s2 tops (s3, r); \<forall>extraa cnt cnt'a. clock s2 = extraa + cnt \<and> extra + cnt'_ = extraa + cnt'a \<longrightarrow> evaluate_prog True (extend_dec_env new_env env) (update_clock (\<lambda>_. cnt) s2) tops (update_clock (\<lambda>_. cnt'a) s3, r); clock s1 = extra + cnt_; clock s3 = extra + cnt'_; ck\<rbrakk> \<Longrightarrow> extra \<le> clock s2
[PROOF STEP]
apply (drule_tac x="(clock s2) - extra" in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>evaluate_top True env s1 top0 (s2, Rval new_env); evaluate_prog True (extend_dec_env new_env env) s2 tops (s3, r); clock s1 = extra + cnt_; clock s3 = extra + cnt'_; ck; extra \<le> clock s2; \<forall>cnt'a. clock s2 = extra + (clock s2 - extra) \<and> extra + cnt'_ = extra + cnt'a \<longrightarrow> evaluate_prog True (extend_dec_env new_env env) (update_clock (\<lambda>_. clock s2 - extra) s2) tops (update_clock (\<lambda>_. cnt'a) s3, r)\<rbrakk> \<Longrightarrow> evaluate_prog True env (update_clock (\<lambda>_. cnt_) s1) (top0 # tops) (update_clock (\<lambda>_. cnt'_) s3, combine_dec_result new_env r)
 2. \<lbrakk>evaluate_top True env s1 top0 (s2, Rval new_env); evaluate_prog True (extend_dec_env new_env env) s2 tops (s3, r); \<forall>extraa cnt cnt'a. clock s2 = extraa + cnt \<and> extra + cnt'_ = extraa + cnt'a \<longrightarrow> evaluate_prog True (extend_dec_env new_env env) (update_clock (\<lambda>_. cnt) s2) tops (update_clock (\<lambda>_. cnt'a) s3, r); clock s1 = extra + cnt_; clock s3 = extra + cnt'_; ck\<rbrakk> \<Longrightarrow> extra \<le> clock s2
[PROOF STEP]
apply rule+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>evaluate_top True env s1 top0 (s2, Rval new_env); evaluate_prog True (extend_dec_env new_env env) s2 tops (s3, r); clock s1 = extra + cnt_; clock s3 = extra + cnt'_; ck; extra \<le> clock s2; \<forall>cnt'a. clock s2 = extra + (clock s2 - extra) \<and> extra + cnt'_ = extra + cnt'a \<longrightarrow> evaluate_prog True (extend_dec_env new_env env) (update_clock (\<lambda>_. clock s2 - extra) s2) tops (update_clock (\<lambda>_. cnt'a) s3, r)\<rbrakk> \<Longrightarrow> evaluate_top True env (update_clock (\<lambda>_. cnt_) s1) top0 (?s2.5, Rval new_env)
 2. \<lbrakk>evaluate_top True env s1 top0 (s2, Rval new_env); evaluate_prog True (extend_dec_env new_env env) s2 tops (s3, r); clock s1 = extra + cnt_; clock s3 = extra + cnt'_; ck; extra \<le> clock s2; \<forall>cnt'a. clock s2 = extra + (clock s2 - extra) \<and> extra + cnt'_ = extra + cnt'a \<longrightarrow> evaluate_prog True (extend_dec_env new_env env) (update_clock (\<lambda>_. clock s2 - extra) s2) tops (update_clock (\<lambda>_. cnt'a) s3, r)\<rbrakk> \<Longrightarrow> evaluate_prog True (extend_dec_env new_env env) ?s2.5 tops (update_clock (\<lambda>_. cnt'_) s3, r)
 3. \<lbrakk>evaluate_top True env s1 top0 (s2, Rval new_env); evaluate_prog True (extend_dec_env new_env env) s2 tops (s3, r); \<forall>extraa cnt cnt'a. clock s2 = extraa + cnt \<and> extra + cnt'_ = extraa + cnt'a \<longrightarrow> evaluate_prog True (extend_dec_env new_env env) (update_clock (\<lambda>_. cnt) s2) tops (update_clock (\<lambda>_. cnt'a) s3, r); clock s1 = extra + cnt_; clock s3 = extra + cnt'_; ck\<rbrakk> \<Longrightarrow> extra \<le> clock s2
[PROOF STEP]
by (auto simp add:top_sub_from_counter dest:prog_clock_monotone)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>extra cnt cnt' s' ra. clock s1 = extra + cnt \<and> clock s' = extra + cnt' \<and> (s3, combine_dec_result new_env r) = (s', ra) \<and> ck = True \<longrightarrow> evaluate_prog ck env (update_clock (\<lambda>_. cnt) s1) (top0 # tops) (update_clock (\<lambda>_. cnt') s', ra)

goal (2 subgoals):
 1. \<And>ck env s. \<forall>extra cnt cnt' s' r. clock s = extra + cnt \<and> clock s' = extra + cnt' \<and> (s, Rval (make_sem_env nsEmpty nsEmpty)) = (s', r) \<and> ck = True \<longrightarrow> evaluate_prog ck env (update_clock (\<lambda>_. cnt) s) [] (update_clock (\<lambda>_. cnt') s', r)
 2. \<And>ck s1 s2 env top0 tops err. evaluate_top ck env s1 top0 (s2, Rerr err) \<Longrightarrow> \<forall>extra cnt cnt' s' r. clock s1 = extra + cnt \<and> clock s' = extra + cnt' \<and> (s2, Rerr err) = (s', r) \<and> ck = True \<longrightarrow> evaluate_prog ck env (update_clock (\<lambda>_. cnt) s1) (top0 # tops) (update_clock (\<lambda>_. cnt') s', r)
[PROOF STEP]
qed (auto intro!:evaluate_prog.intros simp add:top_sub_from_counter)


[STATEMENT]
lemma prog_clocked_min_counter:
  assumes "evaluate_prog True env s prog (s', r)"
  shows "evaluate_prog True env (s (| clock := (clock   s) - (clock  s') |)) prog (((s') (| clock := 0 |)), r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_prog True env (update_clock (\<lambda>_. clock s - clock s') s) prog (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
evaluate_prog True env s prog (s', r)

goal (1 subgoal):
 1. evaluate_prog True env (update_clock (\<lambda>_. clock s - clock s') s) prog (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_prog True env s prog (s', r) \<Longrightarrow> evaluate_prog True env (update_clock (\<lambda>_. clock s - clock s') s) prog (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
apply (frule prog_clock_monotone)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. evaluate_prog True env s prog (s', r) \<Longrightarrow> True
 2. \<lbrakk>evaluate_prog True env s prog (s', r); clock (fst (s', r)) \<le> clock s\<rbrakk> \<Longrightarrow> evaluate_prog True env (update_clock (\<lambda>_. clock s - clock s') s) prog (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
using prog_sub_from_counter
[PROOF STATE]
proof (prove)
using this:
evaluate_prog ?ck ?env ?s ?prog ?res \<Longrightarrow> \<forall>extra cnt cnt' s' r. clock ?s = extra + cnt \<and> clock s' = extra + cnt' \<and> ?res = (s', r) \<and> ?ck = True \<longrightarrow> evaluate_prog ?ck ?env (update_clock (\<lambda>_. cnt) ?s) ?prog (update_clock (\<lambda>_. cnt') s', r)

goal (2 subgoals):
 1. evaluate_prog True env s prog (s', r) \<Longrightarrow> True
 2. \<lbrakk>evaluate_prog True env s prog (s', r); clock (fst (s', r)) \<le> clock s\<rbrakk> \<Longrightarrow> evaluate_prog True env (update_clock (\<lambda>_. clock s - clock s') s) prog (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
by force+


[STATEMENT]
lemma prog_add_clock:
  "evaluate_prog False env s prog (s', res) \<Longrightarrow> \<exists>c. evaluate_prog True env (s (| clock := c |)) prog ((s' (| clock := 0 |)),res)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_prog False env s prog (s', res) \<Longrightarrow> \<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', res)
[PROOF STEP]
proof (induction False env s prog s' res rule: evaluate_prog.induct[split_format(complete)])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>env s. \<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s) [] (update_clock (\<lambda>_. 0) s, Rval (make_sem_env nsEmpty nsEmpty))
 2. \<And>s1 s2 s3 env top0 tops new_env r. evaluate_top False env s1 top0 (s2, Rval new_env) \<and> evaluate_prog False (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<exists>c. evaluate_prog True (extend_dec_env new_env env) (update_clock (\<lambda>_. c) s2) tops (update_clock (\<lambda>_. 0) s3, r)) \<Longrightarrow> \<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s1) (top0 # tops) (update_clock (\<lambda>_. 0) s3, combine_dec_result new_env r)
 3. \<And>s1 s2 env top0 tops err. evaluate_top False env s1 top0 (s2, Rerr err) \<Longrightarrow> \<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s1) (top0 # tops) (update_clock (\<lambda>_. 0) s2, Rerr err)
[PROOF STEP]
case cons1
[PROOF STATE]
proof (state)
this:
evaluate_top False env_ s1_ top0_ (s2_, Rval new_env_) \<and> evaluate_prog False (extend_dec_env new_env_ env_) s2_ tops_ (s3_, r_) \<and> (\<exists>c. evaluate_prog True (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) tops_ (update_clock (\<lambda>_. 0) s3_, r_))

goal (3 subgoals):
 1. \<And>env s. \<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s) [] (update_clock (\<lambda>_. 0) s, Rval (make_sem_env nsEmpty nsEmpty))
 2. \<And>s1 s2 s3 env top0 tops new_env r. evaluate_top False env s1 top0 (s2, Rval new_env) \<and> evaluate_prog False (extend_dec_env new_env env) s2 tops (s3, r) \<and> (\<exists>c. evaluate_prog True (extend_dec_env new_env env) (update_clock (\<lambda>_. c) s2) tops (update_clock (\<lambda>_. 0) s3, r)) \<Longrightarrow> \<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s1) (top0 # tops) (update_clock (\<lambda>_. 0) s3, combine_dec_result new_env r)
 3. \<And>s1 s2 env top0 tops err. evaluate_top False env s1 top0 (s2, Rerr err) \<Longrightarrow> \<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s1) (top0 # tops) (update_clock (\<lambda>_. 0) s2, Rerr err)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate_top False env_ s1_ top0_ (s2_, Rval new_env_) \<and> evaluate_prog False (extend_dec_env new_env_ env_) s2_ tops_ (s3_, r_) \<and> (\<exists>c. evaluate_prog True (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) tops_ (update_clock (\<lambda>_. 0) s3_, r_))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
evaluate_top False env_ s1_ top0_ (s2_, Rval new_env_) \<and> evaluate_prog False (extend_dec_env new_env_ env_) s2_ tops_ (s3_, r_) \<and> (\<exists>c. evaluate_prog True (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) tops_ (update_clock (\<lambda>_. 0) s3_, r_))

goal (1 subgoal):
 1. \<exists>c. evaluate_prog True env_ (update_clock (\<lambda>_. c) s1_) (top0_ # tops_) (update_clock (\<lambda>_. 0) s3_, combine_dec_result new_env_ r_)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>evaluate_top False env_ s1_ top0_ (s2_, Rval new_env_); evaluate_prog False (extend_dec_env new_env_ env_) s2_ tops_ (s3_, r_); evaluate_prog True (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) tops_ (update_clock (\<lambda>_. 0) s3_, r_)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_prog True env_ (update_clock (\<lambda>_. c) s1_) (top0_ # tops_) (update_clock (\<lambda>_. 0) s3_, combine_dec_result new_env_ r_)
[PROOF STEP]
apply (drule top_add_clock)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>evaluate_prog False (extend_dec_env new_env_ env_) s2_ tops_ (s3_, r_); evaluate_prog True (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) tops_ (update_clock (\<lambda>_. 0) s3_, r_)\<rbrakk> \<Longrightarrow> \<not> False
 2. \<And>c. \<lbrakk>evaluate_prog False (extend_dec_env new_env_ env_) s2_ tops_ (s3_, r_); evaluate_prog True (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) tops_ (update_clock (\<lambda>_. 0) s3_, r_); \<exists>c. evaluate_top True env_ (update_clock (\<lambda>_. c) s1_) top0_ (update_clock (\<lambda>_. 0) s2_, Rval new_env_)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_prog True env_ (update_clock (\<lambda>_. c) s1_) (top0_ # tops_) (update_clock (\<lambda>_. 0) s3_, combine_dec_result new_env_ r_)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c ca. \<lbrakk>evaluate_prog False (extend_dec_env new_env_ env_) s2_ tops_ (s3_, r_); evaluate_prog True (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) tops_ (update_clock (\<lambda>_. 0) s3_, r_); evaluate_top True env_ (update_clock (\<lambda>_. ca) s1_) top0_ (update_clock (\<lambda>_. 0) s2_, Rval new_env_)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_prog True env_ (update_clock (\<lambda>_. c) s1_) (top0_ # tops_) (update_clock (\<lambda>_. 0) s3_, combine_dec_result new_env_ r_)
[PROOF STEP]
subgoal for c c'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate_prog False (extend_dec_env new_env_ env_) s2_ tops_ (s3_, r_); evaluate_prog True (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) tops_ (update_clock (\<lambda>_. 0) s3_, r_); evaluate_top True env_ (update_clock (\<lambda>_. c') s1_) top0_ (update_clock (\<lambda>_. 0) s2_, Rval new_env_)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_prog True env_ (update_clock (\<lambda>_. c) s1_) (top0_ # tops_) (update_clock (\<lambda>_. 0) s3_, combine_dec_result new_env_ r_)
[PROOF STEP]
apply (drule top_add_to_counter[where extra = c])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>evaluate_prog False (extend_dec_env new_env_ env_) s2_ tops_ (s3_, r_); evaluate_prog True (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) tops_ (update_clock (\<lambda>_. 0) s3_, r_)\<rbrakk> \<Longrightarrow> Rval new_env_ \<noteq> Rerr (Rabort Rtimeout_error)
 2. \<lbrakk>evaluate_prog False (extend_dec_env new_env_ env_) s2_ tops_ (s3_, r_); evaluate_prog True (extend_dec_env new_env_ env_) (update_clock (\<lambda>_. c) s2_) tops_ (update_clock (\<lambda>_. 0) s3_, r_); evaluate_top True env_ (update_clock (\<lambda>_. clock (update_clock (\<lambda>_. c') s1_) + c) (update_clock (\<lambda>_. c') s1_)) top0_ (update_clock (\<lambda>_. clock (update_clock (\<lambda>_. 0) s2_) + c) (update_clock (\<lambda>_. 0) s2_), Rval new_env_)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate_prog True env_ (update_clock (\<lambda>_. c) s1_) (top0_ # tops_) (update_clock (\<lambda>_. 0) s3_, combine_dec_result new_env_ r_)
[PROOF STEP]
by (auto simp add:add.commute intro: evaluate_prog.intros)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate_prog True env_ (update_clock (\<lambda>_. c) s1_) (top0_ # tops_) (update_clock (\<lambda>_. 0) s3_, combine_dec_result new_env_ r_)

goal (2 subgoals):
 1. \<And>env s. \<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s) [] (update_clock (\<lambda>_. 0) s, Rval (make_sem_env nsEmpty nsEmpty))
 2. \<And>s1 s2 env top0 tops err. evaluate_top False env s1 top0 (s2, Rerr err) \<Longrightarrow> \<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s1) (top0 # tops) (update_clock (\<lambda>_. 0) s2, Rerr err)
[PROOF STEP]
qed (auto intro: evaluate_prog.intros dest: top_add_clock)


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

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

goal (1 subgoal):
 1. \<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
using prog_add_clock
[PROOF STATE]
proof (prove)
using this:
evaluate_prog False env s prog (s', r)
evaluate_prog False ?env ?s ?prog (?s', ?res) \<Longrightarrow> \<exists>c. evaluate_prog True ?env (update_clock (\<lambda>_. c) ?s) ?prog (update_clock (\<lambda>_. 0) ?s', ?res)

goal (1 subgoal):
 1. \<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
by (fastforce simp: prog_unclocked)
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (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_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> evaluate_prog False env s prog (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> evaluate_prog False env s prog (s', r)
[PROOF STEP]
assume "?rhs"
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (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_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> evaluate_prog False env s prog (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
show "?lhs"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'

goal (1 subgoal):
 1. evaluate_prog False env s prog (s', r)
[PROOF STEP]
apply (auto simp: prog_unclocked)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r); r \<noteq> Rerr (Rabort Rtimeout_error); clock s = clock s'\<rbrakk> \<Longrightarrow> evaluate_prog False env s prog (s', r)
[PROOF STEP]
(* sledgehammer proof *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r); r \<noteq> Rerr (Rabort Rtimeout_error); clock s = clock s'\<rbrakk> \<Longrightarrow> evaluate_prog False env s prog (s', r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r); r \<noteq> Rerr (Rabort Rtimeout_error); clock s = clock s'\<rbrakk> \<Longrightarrow> evaluate_prog False env s prog (s', r)
[PROOF STEP]
fix c :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r); r \<noteq> Rerr (Rabort Rtimeout_error); clock s = clock s'\<rbrakk> \<Longrightarrow> evaluate_prog False env s prog (s', r)
[PROOF STEP]
assume a1: "evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r)"
[PROOF STATE]
proof (state)
this:
evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r)

goal (1 subgoal):
 1. \<And>c. \<lbrakk>evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r); r \<noteq> Rerr (Rabort Rtimeout_error); clock s = clock s'\<rbrakk> \<Longrightarrow> evaluate_prog False env s prog (s', r)
[PROOF STEP]
assume a2: "r \<noteq> Rerr (Rabort Rtimeout_error)"
[PROOF STATE]
proof (state)
this:
r \<noteq> Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. \<And>c. \<lbrakk>evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r); r \<noteq> Rerr (Rabort Rtimeout_error); clock s = clock s'\<rbrakk> \<Longrightarrow> evaluate_prog False env s prog (s', r)
[PROOF STEP]
assume a3: "clock s = clock s'"
[PROOF STATE]
proof (state)
this:
clock s = clock s'

goal (1 subgoal):
 1. \<And>c. \<lbrakk>evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r); r \<noteq> Rerr (Rabort Rtimeout_error); clock s = clock s'\<rbrakk> \<Longrightarrow> evaluate_prog False env s prog (s', r)
[PROOF STEP]
have "\<forall>n. evaluate_prog False env (update_clock (\<lambda>na. n) s) prog (update_clock (\<lambda>na. n) s', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. evaluate_prog False env (update_clock (\<lambda>na. n) s) prog (update_clock (\<lambda>na. n) s', r)
[PROOF STEP]
using a2 a1 prog_unclocked_ignore
[PROOF STATE]
proof (prove)
using this:
r \<noteq> Rerr (Rabort Rtimeout_error)
evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r)
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)

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

goal (1 subgoal):
 1. \<And>c. \<lbrakk>evaluate_prog True env (update_clock (\<lambda>_. c) s) prog (update_clock (\<lambda>_. 0) s', r); r \<noteq> Rerr (Rabort Rtimeout_error); clock s = clock s'\<rbrakk> \<Longrightarrow> evaluate_prog False env s prog (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. evaluate_prog False env (update_clock (\<lambda>na. n) s) prog (update_clock (\<lambda>na. n) s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n. evaluate_prog False env (update_clock (\<lambda>na. n) s) prog (update_clock (\<lambda>na. n) s', r)

goal (1 subgoal):
 1. evaluate_prog False env s prog (s', r)
[PROOF STEP]
using a3
[PROOF STATE]
proof (prove)
using this:
\<forall>n. evaluate_prog False env (update_clock (\<lambda>na. n) s) prog (update_clock (\<lambda>na. n) s', r)
clock s = clock s'

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clocked_evaluate:
  "(\<exists>k. BigStep.evaluate True env (update_clock (\<lambda>_. k) s) e (s', r) \<and> r \<noteq>  Rerr (Rabort Rtimeout_error)) =
   (\<exists>k. BigStep.evaluate True env (update_clock (\<lambda>_. k) s) e ((update_clock (\<lambda>_. 0) s'), r) \<and> r \<noteq>  Rerr (Rabort Rtimeout_error))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>k. evaluate True env (update_clock (\<lambda>_. k) s) e (s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error)) = (\<exists>k. evaluate True env (update_clock (\<lambda>_. k) s) e (update_clock (\<lambda>_. 0) s', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); evaluate True env (update_clock (\<lambda>_. k) s) e (s', r)\<rbrakk> \<Longrightarrow> \<exists>k. evaluate True env (update_clock (\<lambda>_. k) s) e (update_clock (\<lambda>_. 0) s', r)
 2. \<And>k. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); evaluate True env (update_clock (\<lambda>_. k) s) e (update_clock (\<lambda>_. 0) s', r)\<rbrakk> \<Longrightarrow> \<exists>k. evaluate True env (update_clock (\<lambda>_. k) s) e (s', r)
[PROOF STEP]
apply (frule clock_monotone)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); evaluate True env (update_clock (\<lambda>_. k) s) e (s', r); \<forall>s'a r'. (s', r) = (s'a, r') \<and> True = True \<longrightarrow> clock s'a \<le> clock (update_clock (\<lambda>_. k) s)\<rbrakk> \<Longrightarrow> \<exists>k. evaluate True env (update_clock (\<lambda>_. k) s) e (update_clock (\<lambda>_. 0) s', r)
 2. \<And>k. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); evaluate True env (update_clock (\<lambda>_. k) s) e (update_clock (\<lambda>_. 0) s', r)\<rbrakk> \<Longrightarrow> \<exists>k. evaluate True env (update_clock (\<lambda>_. k) s) e (s', r)
[PROOF STEP]
subgoal for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); evaluate True env (update_clock (\<lambda>_. k) s) e (s', r); \<forall>s'a r'. (s', r) = (s'a, r') \<and> True = True \<longrightarrow> clock s'a \<le> clock (update_clock (\<lambda>_. k) s)\<rbrakk> \<Longrightarrow> \<exists>k. evaluate True env (update_clock (\<lambda>_. k) s) e (update_clock (\<lambda>_. 0) s', r)
[PROOF STEP]
by (force dest: sub_from_counter(3)[rule_format, where count' = 0 and count = "k - (clock s')"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>r \<noteq> Rerr (Rabort Rtimeout_error); evaluate True env (update_clock (\<lambda>_. k) s) e (update_clock (\<lambda>_. 0) s', r)\<rbrakk> \<Longrightarrow> \<exists>k. evaluate True env (update_clock (\<lambda>_. k) s) e (s', r)
[PROOF STEP]
by (force dest: add_to_counter[where extra = "clock s'"])


[STATEMENT]
lemma lim_Ref_alloc[simp]: "lim (snd (Ref.alloc x h)) = Suc (lim h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim (snd (Ref.alloc x h)) = Suc (lim h)
[PROOF STEP]
unfolding Ref.alloc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim (snd (let l = lim h; r = Ref l in (r, Ref.set r x (h\<lparr>lim := l + 1\<rparr>)))) = Suc (lim h)
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma lim_Array_alloc[simp]: "lim (snd (Array.alloc x h)) = Suc (lim h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim (snd (Array.alloc x h)) = Suc (lim h)
[PROOF STEP]
unfolding Array.alloc_def Array.set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim (snd (let l = lim h; r = Array l in Let (arrays_update (\<lambda>h. h(TYPEREP('a) := (h TYPEREP('a))(addr_of_array r := map to_nat x))) (h\<lparr>lim := l + 1\<rparr>)) (Pair r))) = Suc (lim h)
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma lim_Array_set[simp]: "lim (Array.set a xs h) = lim h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim (Array.set a xs h) = lim h
[PROOF STEP]
unfolding Array.set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim (arrays_update (\<lambda>h. h(TYPEREP('a) := (h TYPEREP('a))(addr_of_array a := map to_nat xs))) h) = lim h
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma lim_Array_update[simp]: "lim (Array.update a i x h) = lim h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim (Array.update a i x h) = lim h
[PROOF STEP]
unfolding Array.update_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim (Array.set a ((Array.get h a)[i := x]) h) = lim h
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma addr_of_ref_alloc[simp]:
  "addr_of_ref (fst (Ref.alloc x h)) = lim h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_of_ref (fst (Ref.alloc x h)) = lim h
[PROOF STEP]
unfolding Ref.alloc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_of_ref (fst (let l = lim h; r = Ref l in (r, Ref.set r x (h\<lparr>lim := l + 1\<rparr>)))) = lim h
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma addr_of_array_alloc[simp]:
  "addr_of_array (fst (Array.alloc x h)) = lim h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_of_array (fst (Array.alloc x h)) = lim h
[PROOF STEP]
unfolding Array.alloc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_of_array (fst (let l = lim h; r = Array l in Let (Array.set r x (h\<lparr>lim := l + 1\<rparr>)) (Pair r))) = lim h
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma "vec_index (vec (5::nat) (\<lambda>i. False)) 2 = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec 5 (\<lambda>i. False) $ 2 = False
[PROOF STEP]
by simp


[STATEMENT]
lemma "vec_index (vec (5::nat) (\<lambda>i. True)) 3 = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec 5 (\<lambda>i. True) $ 3 = True
[PROOF STEP]
by simp


[STATEMENT]
lemma "count_true (vec (1::nat) (\<lambda>i. True)) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_true (vec 1 (\<lambda>i. True)) = 1
[PROOF STEP]
unfolding count_true_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<dim_vec (vec 1 (\<lambda>i. True)). if vec 1 (\<lambda>i. True) $ i then 1 else 0) = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma "count_true (vec (2::nat) (\<lambda>i. True)) = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_true (vec 2 (\<lambda>i. True)) = 2
[PROOF STEP]
unfolding count_true_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<dim_vec (vec 2 (\<lambda>i. True)). if vec 2 (\<lambda>i. True) $ i then 1 else 0) = 2
[PROOF STEP]
by simp


[STATEMENT]
lemma "count_true (vec (5::nat) (\<lambda>i. True)) = 5"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_true (vec 5 (\<lambda>i. True)) = 5
[PROOF STEP]
unfolding count_true_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<dim_vec (vec 5 (\<lambda>i. True)). if vec 5 (\<lambda>i. True) $ i then 1 else 0) = 5
[PROOF STEP]
by simp


[STATEMENT]
lemma "mono_on UNIV bool_fun_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono bool_fun_top
[PROOF STEP]
by (simp add: bool_fun_top_def mono_onI monotone_bool_fun_def)


[STATEMENT]
lemma "monotone_bool_fun bool_fun_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone_bool_fun bool_fun_top
[PROOF STEP]
by (simp add: bool_fun_top_def mono_onI monotone_bool_fun_def)


[STATEMENT]
lemma "mono_on UNIV bool_fun_bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono bool_fun_bot
[PROOF STEP]
by (simp add: bool_fun_bot_def mono_onI monotone_bool_fun_def)


[STATEMENT]
lemma "monotone_bool_fun bool_fun_bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone_bool_fun bool_fun_bot
[PROOF STEP]
by (simp add: bool_fun_bot_def mono_onI monotone_bool_fun_def)


[STATEMENT]
lemma "mono_on UNIV (bool_fun_threshold n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (bool_fun_threshold n)
[PROOF STEP]
by (meson mono_onI monotone_bool_fun_def monotone_threshold)


[STATEMENT]
lemma "monotone_bool_fun (bool_fun_threshold n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone_bool_fun (bool_fun_threshold n)
[PROOF STEP]
unfolding monotone_bool_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono_on (carrier_vec n) (bool_fun_threshold n)
[PROOF STEP]
by (meson boolean_functions.monotone_threshold mono_onI)


[STATEMENT]
lemma Example1:
 "\<Gamma>, \<Theta>|\<tturnstile>\<^bsub>/F\<^esub>\<lbrace>True\<rbrace>
   COBEGIN SCHEME [0\<le>i<n] \<lbrace>True\<rbrace> \<acute>ex1_a:=\<acute>ex1_a (i:=0) \<lbrace>\<acute>ex1_a i=0\<rbrace>, \<lbrace>False\<rbrace> COEND
  \<lbrace>\<forall>i < n. \<acute>ex1_a i = 0\<rbrace>, X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>, \<Theta> |\<tturnstile>\<^bsub>/F\<^esub> \<lbrace>True\<rbrace>
COBEGIN
  SCHEME [0 \<le> i < n]
\<lbrace>True\<rbrace>
\<acute>ex1_a := \<acute>ex1_a(i := 0)
\<lbrace>\<acute>ex1_a i = 0\<rbrace>, \<lbrace>False\<rbrace>
COEND
\<lbrace>\<forall>i<n. \<acute>ex1_a i = 0\<rbrace>, X
[PROOF STEP]
apply oghoare
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrace>True\<rbrace> \<subseteq> pre (AnnPar (map (\<lambda>i. (AnnExpr \<lbrace>True\<rbrace>, \<lbrace>\<acute>ex1_a i = 0\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n]))
 2. \<And>i. 0 \<le> i \<and> i < n \<Longrightarrow> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(i := 0))) \<in> \<lbrace>\<acute>ex1_a i = 0\<rbrace>\<rbrace>
 3. \<And>i j. 0 \<le> i \<and> i < n \<and> 0 \<le> j \<and> j < n \<and> i \<noteq> j \<Longrightarrow> \<lbrace>\<acute>ex1_a i = 0\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(j := 0))) \<in> \<lbrace>\<acute>ex1_a i = 0\<rbrace>\<rbrace>
 4. \<And>i j. 0 \<le> i \<and> i < n \<and> 0 \<le> j \<and> j < n \<and> i \<noteq> j \<Longrightarrow> \<lbrace>False\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(j := 0))) \<in> \<lbrace>False\<rbrace>\<rbrace>
 5. \<And>i j. 0 \<le> i \<and> i < n \<and> 0 \<le> j \<and> j < n \<and> i \<noteq> j \<Longrightarrow> \<lbrace>True\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(j := 0))) \<in> \<lbrace>True\<rbrace>\<rbrace>
 6. \<And>x i. \<lbrakk>x \<in> snd (snd (map (\<lambda>i. (AnnExpr \<lbrace>True\<rbrace>, \<lbrace>\<acute>ex1_a i = 0\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n] ! i)); i < n - 0\<rbrakk> \<Longrightarrow> x \<in> X
 7. \<And>x i. \<lbrakk>\<forall>i<n - 0. x \<in> fst (snd (map (\<lambda>i. (AnnExpr \<lbrace>True\<rbrace>, \<lbrace>\<acute>ex1_a i = 0\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n] ! i)); i < n\<rbrakk> \<Longrightarrow> ex1_a x i = 0
[PROOF STEP]
(* 7 subgoals *)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrace>True\<rbrace> \<subseteq> pre (AnnPar (map (\<lambda>i. (AnnExpr \<lbrace>True\<rbrace>, \<lbrace>\<acute>ex1_a i = 0\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n]))
 2. \<And>i. 0 \<le> i \<and> i < n \<Longrightarrow> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(i := 0))) \<in> \<lbrace>\<acute>ex1_a i = 0\<rbrace>\<rbrace>
 3. \<And>i j. 0 \<le> i \<and> i < n \<and> 0 \<le> j \<and> j < n \<and> i \<noteq> j \<Longrightarrow> \<lbrace>\<acute>ex1_a i = 0\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(j := 0))) \<in> \<lbrace>\<acute>ex1_a i = 0\<rbrace>\<rbrace>
 4. \<And>i j. 0 \<le> i \<and> i < n \<and> 0 \<le> j \<and> j < n \<and> i \<noteq> j \<Longrightarrow> \<lbrace>False\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(j := 0))) \<in> \<lbrace>False\<rbrace>\<rbrace>
 5. \<And>i j. 0 \<le> i \<and> i < n \<and> 0 \<le> j \<and> j < n \<and> i \<noteq> j \<Longrightarrow> \<lbrace>True\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(j := 0))) \<in> \<lbrace>True\<rbrace>\<rbrace>
 6. \<And>x i. \<lbrakk>x \<in> snd (snd (map (\<lambda>i. (AnnExpr \<lbrace>True\<rbrace>, \<lbrace>\<acute>ex1_a i = 0\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n] ! i)); i < n - 0\<rbrakk> \<Longrightarrow> x \<in> X
 7. \<And>x i. \<lbrakk>\<forall>i<n - 0. x \<in> fst (snd (map (\<lambda>i. (AnnExpr \<lbrace>True\<rbrace>, \<lbrace>\<acute>ex1_a i = 0\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n] ! i)); i < n\<rbrakk> \<Longrightarrow> ex1_a x i = 0
[PROOF STEP]
apply (simp ; fail)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Example1_proc_simp[unfolded Example1'b_def oghoare_simps]:
 "\<Gamma>' 0 = Some (com (Example1'b))"
 "\<Theta>' 0 = Some ([ ann(Example1'b)])"
 "[ ann(Example1'b)]!0 = ann(Example1'b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>' (0::'d) = Some (com Example1'b) &&& \<Theta>' 0 = Some [ann Example1'b] &&& [ann Example1'b] ! 0 = ann Example1'b
[PROOF STEP]
by (simp add: \<Gamma>'_def \<Theta>'_def)+


[STATEMENT]
lemma Example1':
notes Example1_proc_simp[proc_simp]
shows
 "\<Gamma>', \<Theta>' |\<turnstile>\<^bsub>/F\<^esub> Example1' \<lbrace>\<forall>i < 2. \<acute>ex1_a i = 0\<rbrace>, \<lbrace>False\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>', \<Theta>' |\<turnstile>\<^bsub>/F\<^esub> Example1'
\<lbrace>\<forall>i<2. \<acute>ex1_a i = 0\<rbrace>, \<lbrace>False\<rbrace>
[PROOF STEP]
unfolding Example1'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>', \<Theta>' |\<turnstile>\<^bsub>/F\<^esub> COBEGIN
  Example1'a
\<lbrace>\<acute>ex1_a 0 = 0\<rbrace>, \<lbrace>False\<rbrace>
\<parallel>
  \<lbrace>True\<rbrace>
SCALL 0 0
\<lbrace>\<acute>ex1_a 1 = 0\<rbrace>, \<lbrace>False\<rbrace>
COEND
\<lbrace>\<forall>i<2. \<acute>ex1_a i = 0\<rbrace>, \<lbrace>False\<rbrace>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>', \<Theta>' |\<turnstile>\<^bsub>/F\<^esub> COBEGIN
  Example1'a
\<lbrace>\<acute>ex1_a 0 = 0\<rbrace>, {}
\<parallel>
  UNIV
SCALL 0 0
\<lbrace>\<acute>ex1_a (Suc 0) = 0\<rbrace>, {}
COEND
\<lbrace>\<forall>i<2. \<acute>ex1_a i = 0\<rbrace>, {}
[PROOF STEP]
unfolding Example1'a_def Example1'b_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>', \<Theta>' |\<turnstile>\<^bsub>/F\<^esub> COBEGIN
  \<lbrace>True\<rbrace>
\<acute>ex1_a := \<acute>ex1_a(0 := 0)
\<lbrace>\<acute>ex1_a 0 = 0\<rbrace>, {}
\<parallel>
  UNIV
SCALL 0 0
\<lbrace>\<acute>ex1_a (Suc 0) = 0\<rbrace>, {}
COEND
\<lbrace>\<forall>i<2. \<acute>ex1_a i = 0\<rbrace>, {}
[PROOF STEP]
apply oghoare
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<lbrace>\<acute>ex1_a (Suc 0) = 0\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(0 := 0))) \<in> \<lbrace>\<acute>ex1_a (Suc 0) = 0\<rbrace>\<rbrace>
 2. \<lbrace>\<acute>ex1_a 0 = 0\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(1 := 0))) \<in> \<lbrace>\<acute>ex1_a 0 = 0\<rbrace>\<rbrace>
 3. \<lbrace>True\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(0 := 0))) \<in> \<lbrace>True\<rbrace>\<rbrace>
 4. \<lbrace>True\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(1 := 0))) \<in> \<lbrace>True\<rbrace>\<rbrace>
 5. UNIV \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(0 := 0))) \<in> UNIV\<rbrace>
 6. {} \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(0 := 0))) \<in> {}\<rbrace>
 7. {} \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(1 := 0))) \<in> {}\<rbrace>
 8. \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(1 := 0))) \<in> \<lbrace>\<acute>ex1_a (Suc 0) = 0\<rbrace>\<rbrace>
 9. \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(0 := 0))) \<in> \<lbrace>\<acute>ex1_a 0 = 0\<rbrace>\<rbrace>
 10. UNIV \<subseteq> pre (AnnExpr \<lbrace>True\<rbrace>)
A total of 12 subgoals...
[PROOF STEP]
(*12 subgoals*)
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<lbrace>\<acute>ex1_a (Suc 0) = 0\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(0 := 0))) \<in> \<lbrace>\<acute>ex1_a (Suc 0) = 0\<rbrace>\<rbrace>
 2. \<lbrace>\<acute>ex1_a 0 = 0\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(1 := 0))) \<in> \<lbrace>\<acute>ex1_a 0 = 0\<rbrace>\<rbrace>
 3. \<lbrace>True\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(0 := 0))) \<in> \<lbrace>True\<rbrace>\<rbrace>
 4. \<lbrace>True\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(1 := 0))) \<in> \<lbrace>True\<rbrace>\<rbrace>
 5. UNIV \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(0 := 0))) \<in> UNIV\<rbrace>
 6. {} \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(0 := 0))) \<in> {}\<rbrace>
 7. {} \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(1 := 0))) \<in> {}\<rbrace>
 8. \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(1 := 0))) \<in> \<lbrace>\<acute>ex1_a (Suc 0) = 0\<rbrace>\<rbrace>
 9. \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex1_a_update (\<lambda>_. \<acute>ex1_a(0 := 0))) \<in> \<lbrace>\<acute>ex1_a 0 = 0\<rbrace>\<rbrace>
 10. UNIV \<subseteq> pre (AnnExpr \<lbrace>True\<rbrace>)
A total of 12 subgoals...
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i. \<lbrakk>ex1_a x (Suc 0) = 0; ex1_a x 0 = 0; i < 2\<rbrakk> \<Longrightarrow> ex1_a x i = 0
 2. \<And>x i. \<lbrakk>i \<in> insert (Suc 0) (insert 0 \<lbrace>False\<rbrace>); x \<in> snd (snd ([(AnnExpr \<lbrace>True\<rbrace>, \<lbrace>\<acute>ex1_a 0 = 0\<rbrace>, {}), (AnnCall UNIV 0, \<lbrace>\<acute>ex1_a (Suc 0) = 0\<rbrace>, {})] ! i))\<rbrakk> \<Longrightarrow> x \<in> {}
[PROOF STEP]
using less_2_cases
[PROOF STATE]
proof (prove)
using this:
?n < 2 \<Longrightarrow> ?n = 0 \<or> ?n = Suc 0

goal (2 subgoals):
 1. \<And>x i. \<lbrakk>ex1_a x (Suc 0) = 0; ex1_a x 0 = 0; i < 2\<rbrakk> \<Longrightarrow> ex1_a x i = 0
 2. \<And>x i. \<lbrakk>i \<in> insert (Suc 0) (insert 0 \<lbrace>False\<rbrace>); x \<in> snd (snd ([(AnnExpr \<lbrace>True\<rbrace>, \<lbrace>\<acute>ex1_a 0 = 0\<rbrace>, {}), (AnnCall UNIV 0, \<lbrace>\<acute>ex1_a (Suc 0) = 0\<rbrace>, {})] ! i))\<rbrakk> \<Longrightarrow> x \<in> {}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>i \<in> insert (Suc 0) (insert 0 \<lbrace>False\<rbrace>); x \<in> snd (snd ([(AnnExpr \<lbrace>True\<rbrace>, \<lbrace>\<acute>ex1_a 0 = 0\<rbrace>, {}), (AnnCall UNIV 0, \<lbrace>\<acute>ex1_a (Suc 0) = 0\<rbrace>, {})] ! i))\<rbrakk> \<Longrightarrow> x \<in> {}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>i = Suc 0 \<or> i = 0; x \<in> snd (snd ([(AnnExpr UNIV, \<lbrace>\<acute>ex1_a 0 = 0\<rbrace>, {}), (AnnCall UNIV 0, \<lbrace>\<acute>ex1_a (Suc 0) = 0\<rbrace>, {})] ! i))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule disjE ; clarsimp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Example2'n_map_of_simps[simp]:
  "i < n \<Longrightarrow>
    map_of (map (\<lambda>i. ((p, i), g i)) [0..<n])
       (p, i) = Some (g i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> map_of (map (\<lambda>i. ((p, i), g i)) [0..<n]) (p, i) = Some (g i)
[PROOF STEP]
apply (rule map_of_is_SomeI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i < n \<Longrightarrow> distinct (map fst (map (\<lambda>i. ((p, i), g i)) [0..<n]))
 2. i < n \<Longrightarrow> ((p, i), g i) \<in> set (map (\<lambda>i. ((p, i), g i)) [0..<n])
[PROOF STEP]
apply (clarsimp simp: distinct_map o_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i < n \<Longrightarrow> inj_on (Pair p) {0..<n}
 2. i < n \<Longrightarrow> ((p, i), g i) \<in> set (map (\<lambda>i. ((p, i), g i)) [0..<n])
[PROOF STEP]
apply (meson inj_onI prod.inject)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> ((p, i), g i) \<in> set (map (\<lambda>i. ((p, i), g i)) [0..<n])
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma  Example2'n_proc_simp[unfolded Example2'n_def oghoare_simps]:
 "i<n \<Longrightarrow> \<Gamma>'' n (''f'',i) = Some ( com(Example2'n i))"
 "i<n \<Longrightarrow> \<Theta>'' n (''f'',i) = Some ([ ann(Example2'n i)])"
 "[ ann(Example2'n i)]!0 = ann(Example2'n i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < n \<Longrightarrow> \<Gamma>'' n (''f'', i) = Some (com (Example2'n i))) &&& (i < n \<Longrightarrow> \<Theta>'' n (''f'', i) = Some [ann (Example2'n i)]) &&& [ann (Example2'n i)] ! 0 = ann (Example2'n i)
[PROOF STEP]
by (simp add: \<Gamma>''_def \<Theta>''_def)+