theory Schedule_DR

lemma schedule_choose_new_thread_dcorres_fragment:
  "\<And>cur_ts cur. dcorres dc \<top>
        (\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = choose_new_thread)
        Schedule_D.schedule
        (do y \<leftarrow> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
            schedule_choose_new_thread
         od)" apply (rule dcorres_symb_exec_r) apply (rule corres_guard_imp) apply (rule schedule_choose_new_thread_dcorres) apply (wp tcb_sched_action_transform| simp add: valid_sched_def st_tcb_at_def obj_at_def not_cur_thread_def| clarsimp simp: transform_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cur_ts cur. dcorres dc (\<lambda>_. True) (\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = choose_new_thread) Schedule_D.schedule (do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od) proof (prove)
goal (3 subgoals):
 1. \<And>cur_ts cur rv. dcorres dc (\<lambda>_. True) (?Q' cur_ts cur rv) Schedule_D.schedule schedule_choose_new_thread
 2. \<And>cur_ts cur. \<lbrace>\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>?Q' cur_ts cur\<rbrace>
 3. \<And>cur_ts cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cur_ts cur rv. dcorres dc (?Q4 cur_ts cur rv) (?Q'4 cur_ts cur rv) Schedule_D.schedule schedule_choose_new_thread
 2. \<And>cur_ts cur rv s. True \<Longrightarrow> ?Q4 cur_ts cur rv s
 3. \<And>cur_ts cur rv s. ?Q' cur_ts cur rv s \<Longrightarrow> ?Q'4 cur_ts cur rv s
 4. \<And>cur_ts cur. \<lbrace>\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>?Q' cur_ts cur\<rbrace>
 5. \<And>cur_ts cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cur_ts cur rv s. True \<Longrightarrow> True
 2. \<And>cur_ts cur rv s. ?Q' cur_ts cur rv s \<Longrightarrow> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread
 3. \<And>cur_ts cur. \<lbrace>\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = choose_new_thread\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>?Q' cur_ts cur\<rbrace>
 4. \<And>cur_ts cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!