theory Schedule_R

lemma scheduleChooseNewThread_fragment_corres:
  "corres dc (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread))
     (do _ \<leftarrow> when (domainTime = 0) next_domain;
         choose_thread
      od)
     (do _ \<leftarrow> when (domainTime = 0) nextDomain;
          chooseThread
      od)" apply (subst bind_dummy_ret_val) apply (subst bind_dummy_ret_val) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule corres_when, simp) apply (rule nextDomain_corres) apply simp apply (rule chooseThread_corres) apply (wp nextDomain_invs_no_cicd')+ apply (clarsimp simp: valid_sched_def invs'_def valid_state'_def all_invs_but_ct_idle_or_in_cur_domain'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) (do _ <- when (domainTime = (0::'a)) next_domain;
choose_thread
od) (do _ <- when (domainTime = (0::'a)) nextDomain;
chooseThread
od) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) (do when (domainTime = (0::'a)) next_domain;
choose_thread
od) (do _ <- when (domainTime = (0::'a)) nextDomain;
chooseThread
od) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) (do when (domainTime = (0::'a)) next_domain;
choose_thread
od) (do when (domainTime = (0::'a)) nextDomain;
chooseThread
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do when (domainTime = (0::'a)) next_domain;
choose_thread
od) (do when (domainTime = (0::'a)) nextDomain;
chooseThread
od)
 2. \<And>s. (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres ?r'4 ?P4 ?P'4 (when (domainTime = (0::'a)) next_domain) (when (domainTime = (0::'a)) nextDomain)
 2. \<And>rv rv'. ?r'4 rv rv' \<Longrightarrow> corres dc (?R4 rv) (?R'4 rv') (K_bind choose_thread rv) (K_bind chooseThread rv')
 3. \<lbrace>?Q4\<rbrace> when (domainTime = (0::'a)) next_domain \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> when (domainTime = (0::'a)) nextDomain \<lbrace>?R'4\<rbrace>
 5. \<And>s. (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) s \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. corres dc ?P9 ?P'9 next_domain nextDomain
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (?R4 rv) (?R'4 rv') (K_bind choose_thread rv) (K_bind chooseThread rv')
 3. \<lbrace>?Q4\<rbrace> when (domainTime = (0::'a)) next_domain \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> when (domainTime = (0::'a)) nextDomain \<lbrace>?R'4\<rbrace>
 5. \<And>s. (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) s \<Longrightarrow> ((\<lambda>x. domainTime = (0::'a) \<longrightarrow> ?P9 x) and ?Q4) s
 6. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>x. domainTime = (0::'a) \<longrightarrow> ?P'9 x) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (?R4 rv) (?R'4 rv') (K_bind choose_thread rv) (K_bind chooseThread rv')
 2. \<lbrace>?Q4\<rbrace> when (domainTime = (0::'a)) next_domain \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> when (domainTime = (0::'a)) nextDomain \<lbrace>?R'4\<rbrace>
 4. \<And>s. (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) s \<Longrightarrow> ((\<lambda>x. domainTime = (0::'a) \<longrightarrow> True) and ?Q4) s
 5. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>x. domainTime = (0::'a) \<longrightarrow> True) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. corres dc (?R4 ()) (?R'4 ()) choose_thread chooseThread
 2. \<lbrace>?Q4\<rbrace> when (domainTime = (0::'a)) next_domain \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> when (domainTime = (0::'a)) nextDomain \<lbrace>?R'4\<rbrace>
 4. \<And>s. (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) s \<Longrightarrow> ((\<lambda>x. domainTime = (0::'a) \<longrightarrow> True) and ?Q4) s
 5. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>x. domainTime = (0::'a) \<longrightarrow> True) and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> when (domainTime = (0::'a)) next_domain \<lbrace>\<lambda>a. invs and valid_sched\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> when (domainTime = (0::'a)) nextDomain \<lbrace>\<lambda>a. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace>
 3. \<And>s. (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) s \<Longrightarrow> ((\<lambda>x. domainTime = (0::'a) \<longrightarrow> True) and ?Q4) s
 4. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>x. domainTime = (0::'a) \<longrightarrow> True) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) s \<Longrightarrow> ((\<lambda>x. domainTime = (0::'a) \<longrightarrow> True) and (if domainTime = (0::'a) then \<lambda>s. invs s \<and> (valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) s else (\<lambda>s. invs s \<and> valid_sched s))) s
 2. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>x. domainTime = (0::'a) \<longrightarrow> True) and (if domainTime = (0::'a) then invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread) else all_invs_but_ct_idle_or_in_cur_domain')) s proof (prove)
goal:
No subgoals!