theory KHeap_DR

lemma reschedule_required_dcorres: "dcorres dc P P' (return ()) reschedule_required" apply (clarsimp simp: reschedule_required_def) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply (clarsimp simp: set_scheduler_action_def (*switch_thread_def*) modify_def bind_def return_def get_def put_def corres_underlying_def) apply (case_tac "\<exists>t. rv = switch_thread t") apply (clarsimp | wp)+ apply (clarsimp split: Deterministic_A.scheduler_action.splits | rule tcb_sched_action_transform | wp )+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (return ()) reschedule_required proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (return ()) (do action <- gets scheduler_action;
y <- case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ();
set_scheduler_action choose_new_thread
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv. dcorres dc P (?Q' rv) (return ()) (do y <- case rv of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ();
set_scheduler_action choose_new_thread
od)
 2. \<lbrace>P'\<rbrace> gets scheduler_action \<lbrace>?Q'\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rva. dcorres dc P (?Q'4 rv rva) (return ()) (set_scheduler_action choose_new_thread)
 2. \<And>rv. \<lbrace>?Q' rv\<rbrace> case rv of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>?Q'4 rv\<rbrace>
 3. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> case rv of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>P'\<rbrace> gets scheduler_action \<lbrace>?Q'\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrace>?Q' rv\<rbrace> case rv of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>?Q'4 rv\<rbrace>
 2. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> case rv of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<lbrace>P'\<rbrace> gets scheduler_action \<lbrace>?Q'\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv. \<exists>t. rv = switch_thread t \<Longrightarrow> \<lbrace>?Q' rv\<rbrace> case rv of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>?Q'4 rv\<rbrace>
 2. \<And>rv. \<nexists>t. rv = switch_thread t \<Longrightarrow> \<lbrace>?Q' rv\<rbrace> case rv of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>?Q'4 rv\<rbrace>
 3. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> case rv of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>P'\<rbrace> gets scheduler_action \<lbrace>?Q'\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> case rv of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<lbrace>P'\<rbrace> gets scheduler_action \<lbrace>\<lambda>r a. True\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!