theory TcbAcc_R

lemma setThreadState_corres:
  "thread_state_relation ts ts' \<Longrightarrow>
   corres dc
          (tcb_at t)
          (tcb_at' t)
          (set_thread_state t ts) (setThreadState ts' t)"
  (is "?tsr \<Longrightarrow> corres dc ?Pre ?Pre' ?sts ?sts'") apply (simp add: set_thread_state_def setThreadState_def) apply (simp add: set_thread_state_ext_def[abs_def]) apply (subst bind_assoc[symmetric], subst thread_set_def[simplified, symmetric]) apply (rule corres_guard_imp) apply (rule corres_split[where r'=dc]) apply (rule threadset_corres, (simp add: tcb_relation_def exst_same_def)+) apply (subst thread_get_test[where test="runnable"]) apply (rule corres_split[OF thread_get_isRunnable_corres]) apply (rule corres_split[OF getCurThread_corres]) apply (rule corres_split[OF getSchedulerAction_corres]) apply (simp only: when_def) apply (rule corres_if[where Q=\<top> and Q'=\<top>]) apply (rule iffI) apply clarsimp+ apply (case_tac rva,simp_all)[1] apply (wp rescheduleRequired_corres_simple corres_return_trivial | simp)+ apply (wp hoare_vcg_conj_lift[where Q'="\<top>\<top>"] | simp add: sch_act_simple_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_state_relation ts ts' \<Longrightarrow> corres dc (tcb_at t) (tcb_at' t) (set_thread_state t ts) (setThreadState ts' t) proof (prove)
goal (1 subgoal):
 1. thread_state_relation ts ts' \<Longrightarrow> corres dc (tcb_at t) (tcb_at' t) (do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext t
od) (do y <- threadSet (tcbState_update (\<lambda>_. ts')) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od) proof (prove)
goal (1 subgoal):
 1. thread_state_relation ts ts' \<Longrightarrow> corres dc (tcb_at t) (tcb_at' t) (do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
ts <- get_thread_state t;
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = t \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od) (do y <- threadSet (tcbState_update (\<lambda>_. ts')) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od) proof (prove)
goal (1 subgoal):
 1. thread_state_relation ts ts' \<Longrightarrow> corres dc (tcb_at t) (tcb_at' t) (do y <- thread_set (tcb_state_update (\<lambda>_. ts)) t;
ts <- get_thread_state t;
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = t \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od) (do y <- threadSet (tcbState_update (\<lambda>_. ts')) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od) proof (prove)
goal (3 subgoals):
 1. thread_state_relation ts ts' \<Longrightarrow> corres dc ?Q1 ?Q'1 (do y <- thread_set (tcb_state_update (\<lambda>_. ts)) t;
ts <- get_thread_state t;
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = t \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od) (do y <- threadSet (tcbState_update (\<lambda>_. ts')) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od)
 2. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at t s\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q'1 s proof (prove)
goal (6 subgoals):
 1. thread_state_relation ts ts' \<Longrightarrow> corres dc ?P5 ?P'5 (thread_set (tcb_state_update (\<lambda>_. ts)) t) (threadSet (tcbState_update (\<lambda>_. ts')) t)
 2. \<And>y ya. \<lbrakk>thread_state_relation ts ts'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R5 y) (?R'5 ya) (do ts <- get_thread_state t;
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = t \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od) (do runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od)
 3. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_set (tcb_state_update (\<lambda>_. ts)) t \<lbrace>?R5\<rbrace>
 4. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadSet (tcbState_update (\<lambda>_. ts')) t \<lbrace>?R'5\<rbrace>
 5. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at t s\<rbrakk> \<Longrightarrow> (?P5 and ?Q5) s
 6. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at' t s\<rbrakk> \<Longrightarrow> (?P'5 and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. thread_state_relation ts ts' \<Longrightarrow> corres dc (?R5 ()) (?R'5 ()) (do ts <- get_thread_state t;
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = t \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od) (do runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od)
 2. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_set (tcb_state_update (\<lambda>_. ts)) t \<lbrace>?R5\<rbrace>
 3. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadSet (tcbState_update (\<lambda>_. ts')) t \<lbrace>?R'5\<rbrace>
 4. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q5) s
 5. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. thread_state_relation ts ts' \<Longrightarrow> corres dc (?R24 ()) (?R'24 ()) (do ta <- thread_get (\<lambda>tcb. runnable (tcb_state tcb)) t;
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> ta \<and> cur = t \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od) (do runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od)
 2. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_set (tcb_state_update (\<lambda>_. ts)) t \<lbrace>?R5\<rbrace>
 3. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadSet (tcbState_update (\<lambda>_. ts')) t \<lbrace>?R'5\<rbrace>
 4. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q5) s
 5. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'5) s
flex-flex pairs:
?R'24 () \<equiv>\<^sup>? ?R'5 ()
?R24 () \<equiv>\<^sup>? ?R5 () proof (prove)
goal (7 subgoals):
 1. \<And>ta runnable. \<lbrakk>thread_state_relation ts ts'; ta = runnable\<rbrakk> \<Longrightarrow> corres dc (?R26 ta) (?R'26 runnable) (do cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> ta \<and> cur = t \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od) (do curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od)
 2. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q34 ()\<rbrace> thread_get (\<lambda>tcb. runnable (tcb_state tcb)) t \<lbrace>?R26\<rbrace>
 3. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'32 ()\<rbrace> isRunnable t \<lbrace>?R'26\<rbrace>
 4. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_set (tcb_state_update (\<lambda>_. ts)) t \<lbrace>\<lambda>a. tcb_at t and ?Q35 a\<rbrace>
 5. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadSet (tcbState_update (\<lambda>_. ts')) t \<lbrace>\<lambda>a. tcb_at' t and ?Q'33 a\<rbrace>
 6. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q5) s
 7. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'5) s
flex-flex pairs:
?Q35 () \<equiv>\<^sup>? ?Q34 ()
?Q'33 () \<equiv>\<^sup>? ?Q'32 () proof (prove)
goal (9 subgoals):
 1. \<And>ta runnable rv rv'. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'\<rbrakk> \<Longrightarrow> corres dc (?R39 ta runnable rv) (?R'39 ta runnable rv') (do action <- gets scheduler_action;
when (\<not> ta \<and> rv = t \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od) (do action <- getSchedulerAction;
when (\<not> runnable \<and> rv' = t \<and> action = ResumeCurrentThread) rescheduleRequired
od)
 2. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 t\<rbrace> gets cur_thread \<lbrace>?R39 t runnable\<rbrace>
 3. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 runnable\<rbrace> getCurThread \<lbrace>?R'39 t runnable\<rbrace>
 4. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q34 ()\<rbrace> thread_get (\<lambda>tcb. runnable (tcb_state tcb)) t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q45 a\<rbrace>
 5. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'32 ()\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'43 a\<rbrace>
 6. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_set (tcb_state_update (\<lambda>_. ts)) t \<lbrace>\<lambda>a. tcb_at t and ?Q35 a\<rbrace>
 7. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadSet (tcbState_update (\<lambda>_. ts')) t \<lbrace>\<lambda>a. tcb_at' t and ?Q'33 a\<rbrace>
 8. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q5) s
 9. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'5) s
flex-flex pairs:
?Q35 () \<equiv>\<^sup>? ?Q34 ()
?Q'33 () \<equiv>\<^sup>? ?Q'32 () proof (prove)
goal (11 subgoals):
 1. \<And>ta runnable rv rv' rva rv'a. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'; sched_act_relation rva rv'a\<rbrakk> \<Longrightarrow> corres dc (?R49 ta runnable rv rv' rva) (?R'49 ta runnable rv rv' rv'a) (when (\<not> ta \<and> rv = t \<and> rva = resume_cur_thread) (set_scheduler_action choose_new_thread)) (when (\<not> runnable \<and> rv' = t \<and> rv'a = ResumeCurrentThread) rescheduleRequired)
 2. \<And>t runnable rv rv'. \<lbrakk>thread_state_relation ts ts'; t = runnable; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q55 t runnable rv\<rbrace> gets scheduler_action \<lbrace>?R49 t runnable rv rv'\<rbrace>
 3. \<And>t runnable rv rv'. \<lbrakk>thread_state_relation ts ts'; t = runnable; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 t runnable rv'\<rbrace> getSchedulerAction \<lbrace>?R'49 t runnable rv rv'\<rbrace>
 4. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 t\<rbrace> gets cur_thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q55 t runnable a\<rbrace>
 5. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 runnable\<rbrace> getCurThread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'53 t runnable a\<rbrace>
 6. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q34 ()\<rbrace> thread_get (\<lambda>tcb. runnable (tcb_state tcb)) t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q45 a\<rbrace>
 7. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'32 ()\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'43 a\<rbrace>
 8. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_set (tcb_state_update (\<lambda>_. ts)) t \<lbrace>\<lambda>a. tcb_at t and ?Q35 a\<rbrace>
 9. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadSet (tcbState_update (\<lambda>_. ts')) t \<lbrace>\<lambda>a. tcb_at' t and ?Q'33 a\<rbrace>
 10. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q5) s
A total of 11 subgoals...
flex-flex pairs:
?Q35 () \<equiv>\<^sup>? ?Q34 ()
?Q'33 () \<equiv>\<^sup>? ?Q'32 () proof (prove)
goal (11 subgoals):
 1. \<And>ta runnable rv rv' rva rv'a. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'; sched_act_relation rva rv'a\<rbrakk> \<Longrightarrow> corres dc (?R49 runnable runnable rv' rv' rva) (?R'49 runnable runnable rv' rv' rv'a) (if \<not> runnable \<and> rv' = t \<and> rva = resume_cur_thread then set_scheduler_action choose_new_thread else return ()) (if \<not> runnable \<and> rv' = t \<and> rv'a = ResumeCurrentThread then rescheduleRequired else return ())
 2. \<And>t runnable rv rv'. \<lbrakk>thread_state_relation ts ts'; t = runnable; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q55 t runnable rv\<rbrace> gets scheduler_action \<lbrace>?R49 t runnable rv rv'\<rbrace>
 3. \<And>t runnable rv rv'. \<lbrakk>thread_state_relation ts ts'; t = runnable; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 t runnable rv'\<rbrace> getSchedulerAction \<lbrace>?R'49 t runnable rv rv'\<rbrace>
 4. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 t\<rbrace> gets cur_thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q55 t runnable a\<rbrace>
 5. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 runnable\<rbrace> getCurThread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'53 t runnable a\<rbrace>
 6. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q34 ()\<rbrace> thread_get (\<lambda>tcb. runnable (tcb_state tcb)) t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q45 a\<rbrace>
 7. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'32 ()\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'43 a\<rbrace>
 8. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_set (tcb_state_update (\<lambda>_. ts)) t \<lbrace>\<lambda>a. tcb_at t and ?Q35 a\<rbrace>
 9. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadSet (tcbState_update (\<lambda>_. ts')) t \<lbrace>\<lambda>a. tcb_at' t and ?Q'33 a\<rbrace>
 10. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q5) s
A total of 11 subgoals...
flex-flex pairs:
?Q35 () \<equiv>\<^sup>? ?Q34 ()
?Q'33 () \<equiv>\<^sup>? ?Q'32 () proof (prove)
goal (13 subgoals):
 1. \<And>ta runnable rv rv' rva rv'a. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'; sched_act_relation rva rv'a\<rbrakk> \<Longrightarrow> (\<not> runnable \<and> rv' = t \<and> rva = resume_cur_thread) = (\<not> runnable \<and> rv' = t \<and> rv'a = ResumeCurrentThread)
 2. \<And>t runnable rv rv' rva rv'a. \<lbrakk>thread_state_relation ts ts'; t = runnable; rv = rv'; sched_act_relation rva rv'a\<rbrakk> \<Longrightarrow> corres dc (?P64 runnable runnable rv' rv' rva) (?P'62 runnable runnable rv' rv' rv'a) (set_scheduler_action choose_new_thread) rescheduleRequired
 3. \<And>t runnable rv rv' rva rv'a. \<lbrakk>thread_state_relation ts ts'; t = runnable; rv = rv'; sched_act_relation rva rv'a\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 4. \<And>ta runnable rv rv'. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q55 ta runnable rv\<rbrace> gets scheduler_action \<lbrace>\<lambda>a. if \<not> runnable \<and> rv' = t \<and> a = resume_cur_thread then ?P64 ta runnable rv rv' a else (\<lambda>_. True)\<rbrace>
 5. \<And>ta runnable rv rv'. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 ta runnable rv'\<rbrace> getSchedulerAction \<lbrace>\<lambda>a. if \<not> runnable \<and> rv' = t \<and> a = ResumeCurrentThread then ?P'62 ta runnable rv rv' a else (\<lambda>_. True)\<rbrace>
 6. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 t\<rbrace> gets cur_thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q55 t runnable a\<rbrace>
 7. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 runnable\<rbrace> getCurThread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'53 t runnable a\<rbrace>
 8. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q34 ()\<rbrace> thread_get (\<lambda>tcb. runnable (tcb_state tcb)) t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q45 a\<rbrace>
 9. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'32 ()\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'43 a\<rbrace>
 10. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_set (tcb_state_update (\<lambda>_. ts)) t \<lbrace>\<lambda>a. tcb_at t and ?Q35 a\<rbrace>
A total of 13 subgoals...
flex-flex pairs:
?Q35 () \<equiv>\<^sup>? ?Q34 ()
?Q'33 () \<equiv>\<^sup>? ?Q'32 () proof (prove)
goal (14 subgoals):
 1. \<And>ta runnable rv rv' rva rv'a. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'; sched_act_relation rva rv'a; \<not> runnable \<and> rv' = t \<and> rva = resume_cur_thread\<rbrakk> \<Longrightarrow> \<not> runnable \<and> rv' = t \<and> rv'a = ResumeCurrentThread
 2. \<And>ta runnable rv rv' rva rv'a. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'; sched_act_relation rva rv'a; \<not> runnable \<and> rv' = t \<and> rv'a = ResumeCurrentThread\<rbrakk> \<Longrightarrow> \<not> runnable \<and> rv' = t \<and> rva = resume_cur_thread
 3. \<And>t runnable rv rv' rva rv'a. \<lbrakk>thread_state_relation ts ts'; t = runnable; rv = rv'; sched_act_relation rva rv'a\<rbrakk> \<Longrightarrow> corres dc (?P64 runnable runnable rv' rv' rva) (?P'62 runnable runnable rv' rv' rv'a) (set_scheduler_action choose_new_thread) rescheduleRequired
 4. \<And>t runnable rv rv' rva rv'a. \<lbrakk>thread_state_relation ts ts'; t = runnable; rv = rv'; sched_act_relation rva rv'a\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 5. \<And>ta runnable rv rv'. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q55 ta runnable rv\<rbrace> gets scheduler_action \<lbrace>\<lambda>a. if \<not> runnable \<and> rv' = t \<and> a = resume_cur_thread then ?P64 ta runnable rv rv' a else (\<lambda>_. True)\<rbrace>
 6. \<And>ta runnable rv rv'. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 ta runnable rv'\<rbrace> getSchedulerAction \<lbrace>\<lambda>a. if \<not> runnable \<and> rv' = t \<and> a = ResumeCurrentThread then ?P'62 ta runnable rv rv' a else (\<lambda>_. True)\<rbrace>
 7. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 t\<rbrace> gets cur_thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q55 t runnable a\<rbrace>
 8. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 runnable\<rbrace> getCurThread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'53 t runnable a\<rbrace>
 9. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q34 ()\<rbrace> thread_get (\<lambda>tcb. runnable (tcb_state tcb)) t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q45 a\<rbrace>
 10. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'32 ()\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'43 a\<rbrace>
A total of 14 subgoals...
flex-flex pairs:
?Q35 () \<equiv>\<^sup>? ?Q34 ()
?Q'33 () \<equiv>\<^sup>? ?Q'32 () proof (prove)
goal (13 subgoals):
 1. \<And>t runnable rva. \<lbrakk>thread_state_relation ts ts'; \<not> t; sched_act_relation rva ResumeCurrentThread; \<not> runnable\<rbrakk> \<Longrightarrow> rva = resume_cur_thread
 2. \<And>t runnable rv rv' rva rv'a. \<lbrakk>thread_state_relation ts ts'; t = runnable; rv = rv'; sched_act_relation rva rv'a\<rbrakk> \<Longrightarrow> corres dc (?P64 runnable runnable rv' rv' rva) (?P'62 runnable runnable rv' rv' rv'a) (set_scheduler_action choose_new_thread) rescheduleRequired
 3. \<And>t runnable rv rv' rva rv'a. \<lbrakk>thread_state_relation ts ts'; t = runnable; rv = rv'; sched_act_relation rva rv'a\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 4. \<And>ta runnable rv rv'. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q55 ta runnable rv\<rbrace> gets scheduler_action \<lbrace>\<lambda>a. if \<not> runnable \<and> rv' = t \<and> a = resume_cur_thread then ?P64 ta runnable rv rv' a else (\<lambda>_. True)\<rbrace>
 5. \<And>ta runnable rv rv'. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 ta runnable rv'\<rbrace> getSchedulerAction \<lbrace>\<lambda>a. if \<not> runnable \<and> rv' = t \<and> a = ResumeCurrentThread then ?P'62 ta runnable rv rv' a else (\<lambda>_. True)\<rbrace>
 6. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 t\<rbrace> gets cur_thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q55 t runnable a\<rbrace>
 7. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 runnable\<rbrace> getCurThread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'53 t runnable a\<rbrace>
 8. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q34 ()\<rbrace> thread_get (\<lambda>tcb. runnable (tcb_state tcb)) t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q45 a\<rbrace>
 9. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'32 ()\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'43 a\<rbrace>
 10. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_set (tcb_state_update (\<lambda>_. ts)) t \<lbrace>\<lambda>a. tcb_at t and ?Q35 a\<rbrace>
A total of 13 subgoals...
flex-flex pairs:
?Q35 () \<equiv>\<^sup>? ?Q34 ()
?Q'33 () \<equiv>\<^sup>? ?Q'32 () proof (prove)
goal (12 subgoals):
 1. \<And>t runnable rv rv' rva rv'a. \<lbrakk>thread_state_relation ts ts'; t = runnable; rv = rv'; sched_act_relation rva rv'a\<rbrakk> \<Longrightarrow> corres dc (?P64 runnable runnable rv' rv' rva) (?P'62 runnable runnable rv' rv' rv'a) (set_scheduler_action choose_new_thread) rescheduleRequired
 2. \<And>t runnable rv rv' rva rv'a. \<lbrakk>thread_state_relation ts ts'; t = runnable; rv = rv'; sched_act_relation rva rv'a\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 3. \<And>ta runnable rv rv'. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q55 ta runnable rv\<rbrace> gets scheduler_action \<lbrace>\<lambda>a. if \<not> runnable \<and> rv' = t \<and> a = resume_cur_thread then ?P64 ta runnable rv rv' a else (\<lambda>_. True)\<rbrace>
 4. \<And>ta runnable rv rv'. \<lbrakk>thread_state_relation ts ts'; ta = runnable; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 ta runnable rv'\<rbrace> getSchedulerAction \<lbrace>\<lambda>a. if \<not> runnable \<and> rv' = t \<and> a = ResumeCurrentThread then ?P'62 ta runnable rv rv' a else (\<lambda>_. True)\<rbrace>
 5. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q45 t\<rbrace> gets cur_thread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q55 t runnable a\<rbrace>
 6. \<And>t runnable. \<lbrakk>thread_state_relation ts ts'; t = runnable\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 runnable\<rbrace> getCurThread \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'53 t runnable a\<rbrace>
 7. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q34 ()\<rbrace> thread_get (\<lambda>tcb. runnable (tcb_state tcb)) t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q45 a\<rbrace>
 8. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'32 ()\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and ?Q'43 a\<rbrace>
 9. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_set (tcb_state_update (\<lambda>_. ts)) t \<lbrace>\<lambda>a. tcb_at t and ?Q35 a\<rbrace>
 10. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadSet (tcbState_update (\<lambda>_. ts')) t \<lbrace>\<lambda>a. tcb_at' t and ?Q'33 a\<rbrace>
A total of 12 subgoals...
flex-flex pairs:
?Q35 () \<equiv>\<^sup>? ?Q34 ()
?Q'33 () \<equiv>\<^sup>? ?Q'32 () proof (prove)
goal (3 subgoals):
 1. thread_state_relation ts ts' \<Longrightarrow> \<lbrace>?P'132\<rbrace> threadSet (tcbState_update (\<lambda>_. ts')) t \<lbrace>\<lambda>rv s. \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> sch_act_simple s\<rbrace>
 2. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and (\<lambda>s. tcb_at t s \<and> True \<and> True \<and> ?Q125 (exst s))) s
 3. \<And>s. \<lbrakk>thread_state_relation ts ts'; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>s. obj_at' (\<lambda>obj. if t = t then True else True) t s \<and> ?P'132 s)) s
flex-flex pairs:
?Q126 () \<equiv>\<^sup>? \<lambda>a. ?Q125 (exst a) proof (prove)
goal:
No subgoals!