theory Schedule_R

lemma scheduleChooseNewThread_corres:
  "corres dc
    (\<lambda>s. invs s \<and> valid_sched s \<and> scheduler_action s = choose_new_thread)
    (\<lambda>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread)
           schedule_choose_new_thread scheduleChooseNewThread" unfolding schedule_choose_new_thread_def scheduleChooseNewThread_def apply (rule corres_guard_imp) apply (rule corres_split[OF getDomainTime_corres], clarsimp) apply (rule corres_split[OF scheduleChooseNewThread_fragment_corres, simplified bind_assoc]) apply (rule setSchedulerAction_corres) apply (wp | simp)+ apply (wp | simp add: getDomainTime_def)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> scheduler_action s = choose_new_thread) (\<lambda>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread) schedule_choose_new_thread scheduleChooseNewThread proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> scheduler_action s = choose_new_thread) (\<lambda>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread) (do dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
choose_thread;
set_scheduler_action resume_cur_thread
od) (do domainTime <- getDomainTime;
when (domainTime = 0) $ nextDomain;
chooseThread;
setSchedulerAction ResumeCurrentThread
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
choose_thread;
set_scheduler_action resume_cur_thread
od) (do domainTime <- getDomainTime;
when (domainTime = 0) $ nextDomain;
chooseThread;
setSchedulerAction ResumeCurrentThread
od)
 2. \<And>s. invs s \<and> valid_sched s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ?Q s
 3. \<And>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>dom_time. corres dc (?R4 dom_time) (?R'4 dom_time) (do y <- when (dom_time = 0) next_domain;
y <- choose_thread;
set_scheduler_action resume_cur_thread
od) (do y <- when (dom_time = 0) nextDomain;
y <- chooseThread;
setSchedulerAction ResumeCurrentThread
od)
 2. \<lbrace>?Q4\<rbrace> gets domain_time \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getDomainTime \<lbrace>?R'4\<rbrace>
 4. \<And>s. invs s \<and> valid_sched s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>dom_time rv rv'. dc rv rv' \<Longrightarrow> corres dc (?R10 dom_time rv) (?R'10 dom_time rv') (set_scheduler_action resume_cur_thread) (setSchedulerAction ResumeCurrentThread)
 2. \<And>dom_time. \<lbrace>?Q10 dom_time\<rbrace> do _ <- when (dom_time = 0) next_domain;
choose_thread
od \<lbrace>?R10 dom_time\<rbrace>
 3. \<And>dom_time. \<lbrace>?Q'10 dom_time\<rbrace> do _ <- when (dom_time = 0) nextDomain;
chooseThread
od \<lbrace>?R'10 dom_time\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets domain_time \<lbrace>\<lambda>dom_time. invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread) and ?Q10 dom_time\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getDomainTime \<lbrace>\<lambda>dom_time. invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread) and ?Q'10 dom_time\<rbrace>
 6. \<And>s. invs s \<and> valid_sched s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>dom_time rv rv'. dc rv rv' \<Longrightarrow> sched_act_relation resume_cur_thread ResumeCurrentThread
 2. \<And>dom_time. \<lbrace>?Q10 dom_time\<rbrace> do _ <- when (dom_time = 0) next_domain;
choose_thread
od \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>dom_time. \<lbrace>?Q'10 dom_time\<rbrace> do _ <- when (dom_time = 0) nextDomain;
chooseThread
od \<lbrace>\<lambda>rv' _. True\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets domain_time \<lbrace>\<lambda>dom_time. invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread) and ?Q10 dom_time\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getDomainTime \<lbrace>\<lambda>dom_time. invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread) and ?Q'10 dom_time\<rbrace>
 6. \<And>s. invs s \<and> valid_sched s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'4\<rbrace> getDomainTime \<lbrace>\<lambda>dom_time s. invs' s \<and> ksSchedulerAction s = ChooseNewThread\<rbrace>
 2. \<And>s. invs s \<and> valid_sched s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> ((\<lambda>_. True) and (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread) and (\<lambda>_. True))) s
 3. \<And>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs s \<and> valid_sched s \<and> scheduler_action s = choose_new_thread \<Longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)
 2. \<And>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread)) s proof (prove)
goal:
No subgoals!