kings-crown/FVELER_Isabelle huggingface dataset:
theory Tcb_R

lemma restart_tcb'[wp]:
  "\<lbrace>tcb_at' t'\<rbrace> ThreadDecls_H.restart t \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace>" apply (simp add: restart_def isStopped_def2) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t'\<rbrace> ThreadDecls_H.restart t \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t'\<rbrace> do blocked <- liftM (Not \<circ> activatable') (getThreadState t);
when blocked (do y <- cancelIPC t;
y <- setupReplyMaster t;
y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
possibleSwitchTo t
od)
od \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma no_fail_setRegister: "no_fail \<top> (setRegister r v)" by (simp add: setRegister_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (setRegister r v)
theory Tcb_R

lemma updateRestartPC_ex_nonz_cap_to'[wp]:
  "\<lbrace>ex_nonz_cap_to' p\<rbrace> updateRestartPC t \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" unfolding updateRestartPC_def apply (rule asUser_cap_to') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p\<rbrace> updateRestartPC t \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p\<rbrace> asUser t (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister) \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma invs_valid_queues':
  "invs' s \<longrightarrow> valid_queues' s" by (clarsimp simp:invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<longrightarrow> valid_queues' s
theory Tcb_R

lemma einvs_valid_etcbs: "einvs s \<longrightarrow> valid_etcbs s" by (clarsimp simp: valid_sched_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. einvs s \<longrightarrow> valid_etcbs s
theory Tcb_R

lemma asUser_postModifyRegisters_corres:
  "corres dc \<top> (tcb_at' t)
     (arch_post_modify_registers ct t)
     (asUser t $ postModifyRegisters ct t)" apply (simp add: arch_post_modify_registers_def postModifyRegisters_def) apply (subst submonad_asUser.return) apply (rule corres_stateAssert_assume) by simp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (tcb_at' t) (arch_post_modify_registers ct t) (asUser t $ postModifyRegisters ct t) proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (tcb_at' t) (return ()) (asUser t (return ())) proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (tcb_at' t) (return ()) (do u <- stateAssert (tcb_at' t) [];
return ()
od) proof (prove)
goal (2 subgoals):
 1. corres dc (\<lambda>_. True) (tcb_at' t) (return ()) (return ())
 2. \<And>s. tcb_at' t s \<Longrightarrow> tcb_at' t s
theory Tcb_R

lemma tcbSchedDequeue_ResumeCurrentThread_imp_notct[wp]:
  "\<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
   tcbSchedDequeue t
   \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>" by (wp hoare_convert_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
theory Tcb_R

lemma updateRestartPC_ResumeCurrentThread_imp_notct[wp]:
  "\<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
   updateRestartPC t
   \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>" unfolding updateRestartPC_def apply (wp hoare_convert_imp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> updateRestartPC t \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> asUser t (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister) \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma suspend_ResumeCurrentThread_imp_notct[wp]:
  "\<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
   suspend t
   \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>" by (wpsimp simp: suspend_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t'\<rbrace>
theory Tcb_R

lemma readreg_invs':
  "\<lbrace>invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src\<rbrace>
     invokeTCB (tcbinvocation.ReadRegisters src susp n arch)
   \<lbrace>\<lambda>rv. invs'\<rbrace>" by (simp add: invokeTCB_def performTransfer_def | wp
       | clarsimp simp: invs'_def valid_state'_def
                 dest!: global'_no_ex_cap)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src\<rbrace> invokeTCB (tcbinvocation.ReadRegisters src susp n arch) \<lbrace>\<lambda>rv. invs'\<rbrace>
theory Tcb_R

lemma writereg_invs':
  "\<lbrace>invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest\<rbrace>
     invokeTCB (tcbinvocation.WriteRegisters dest resume values arch)
   \<lbrace>\<lambda>rv. invs'\<rbrace>" by (simp add: invokeTCB_def performTransfer_def  | wp restart_invs' | rule conjI
       | clarsimp
       | clarsimp simp: invs'_def valid_state'_def
                 dest!: global'_no_ex_cap)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest\<rbrace> invokeTCB (tcbinvocation.WriteRegisters dest resume values arch) \<lbrace>\<lambda>rv. invs'\<rbrace>
theory Tcb_R

lemma isRunnable_corres:
  "corres (\<lambda>ts runn. runnable ts = runn) (tcb_at t) (tcb_at' t)
     (get_thread_state t) (isRunnable t)" apply (simp add: isRunnable_def) apply (subst bind_return[symmetric]) apply (rule corres_guard_imp) apply (rule corres_split[OF getThreadState_corres]) apply (case_tac rv, clarsimp+) apply (wp hoare_TrueI)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>ts. (=) (runnable ts)) (tcb_at t) (tcb_at' t) (get_thread_state t) (isRunnable t) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>ts. (=) (runnable ts)) (tcb_at t) (tcb_at' t) (get_thread_state t) (do state <- getThreadState t;
return (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)
od) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>ts. (=) (runnable ts)) (tcb_at t) (tcb_at' t) (get_thread_state t >>= return) (do state <- getThreadState t;
return (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)
od) proof (prove)
goal (3 subgoals):
 1. corres (\<lambda>ts. (=) (runnable ts)) ?Q ?Q' (get_thread_state t >>= return) (do state <- getThreadState t;
return (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)
od)
 2. \<And>s. tcb_at t s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>rv state. thread_state_relation rv state \<Longrightarrow> corres (\<lambda>ts. (=) (runnable ts)) (?R4 rv) (?R'4 state) (return rv) (return (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False))
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>?R'4\<rbrace>
 4. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?R4\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>?R'4\<rbrace>
 3. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q4) s
 4. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q4) s
 2. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma tcbSchedDequeue_not_queued:
  "\<lbrace>\<top>\<rbrace> tcbSchedDequeue t
   \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace>" apply (simp add: tcbSchedDequeue_def) apply (wp | simp)+ apply (rule_tac Q="\<lambda>rv. obj_at' (\<lambda>obj. tcbQueued obj = rv) t"
               in hoare_post_imp) apply (clarsimp simp: obj_at'_def) apply (wp tg_sp' [where P=\<top>, simplified] | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do queued <- threadGet tcbQueued t;
when queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
od \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then tcb_at' t else obj_at' (Not \<circ> tcbQueued) t\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. obj_at' (\<lambda>obj. tcbQueued obj = rv) t s \<Longrightarrow> (if rv then tcb_at' t else obj_at' (Not \<circ> tcbQueued) t) s
 2. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 3. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma tcbSchedDequeue_not_in_queue:
  "\<And>p. \<lbrace>Invariants_H.valid_queues and tcb_at' t and valid_objs'\<rbrace> tcbSchedDequeue t
   \<lbrace>\<lambda>rv s. t \<notin> set (ksReadyQueues s p)\<rbrace>" apply (rule_tac Q="\<lambda>rv. Invariants_H.valid_queues and obj_at' (Not \<circ> tcbQueued) t"
               in hoare_post_imp) apply (fastforce simp: valid_queues_def valid_queues_no_bitmap_def obj_at'_def projectKOs inQ_def ) apply (wp tcbSchedDequeue_not_queued tcbSchedDequeue_valid_queues |
         simp add: valid_objs'_maxDomain valid_objs'_maxPriority)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrace>Invariants_H.valid_queues and tcb_at' t and valid_objs'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv s. t \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>p rv s. (Invariants_H.valid_queues and obj_at' (Not \<circ> tcbQueued) t) s \<Longrightarrow> t \<notin> set (ksReadyQueues s p)
 2. \<And>p. \<lbrace>Invariants_H.valid_queues and tcb_at' t and valid_objs'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. Invariants_H.valid_queues and obj_at' (Not \<circ> tcbQueued) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrace>Invariants_H.valid_queues and tcb_at' t and valid_objs'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. Invariants_H.valid_queues and obj_at' (Not \<circ> tcbQueued) t\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma threadSet_ct_in_state':
  "(\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow>
  \<lbrace>ct_in_state' test\<rbrace> threadSet f t \<lbrace>\<lambda>rv. ct_in_state' test\<rbrace>" apply (simp add: ct_in_state'_def) apply (rule hoare_lift_Pf [where f=ksCurThread]) apply (wp threadSet_pred_tcb_no_state)+ apply simp+ apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>ct_in_state' test\<rbrace> threadSet f t \<lbrace>\<lambda>rv. ct_in_state' test\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>\<lambda>s. st_tcb_at' test (ksCurThread s) s\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. st_tcb_at' test (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. (\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>st_tcb_at' test x\<rbrace> threadSet f t \<lbrace>\<lambda>_. st_tcb_at' test x\<rbrace>
 2. \<And>P. (\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x tcb. (\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow> itcbState (tcb_to_itcb' (f tcb)) = itcbState (tcb_to_itcb' tcb)
 2. \<And>x s. \<lbrakk>\<And>tcb. tcbState (f tcb) = tcbState tcb; st_tcb_at' test x s\<rbrakk> \<Longrightarrow> st_tcb_at' test x s
 3. \<And>P. (\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. (\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma tcbSchedDequeue_ct_in_state'[wp]:
  "\<lbrace>ct_in_state' test\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. ct_in_state' test\<rbrace>" apply (simp add: ct_in_state'_def) apply (rule hoare_lift_Pf [where f=ksCurThread]; wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' test\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. ct_in_state' test\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. st_tcb_at' test (ksCurThread s) s\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv s. st_tcb_at' test (ksCurThread s) s\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma valid_tcb'_tcbPriority_update: "\<lbrakk>valid_tcb' tcb s; f (tcbPriority tcb) \<le> maxPriority \<rbrakk> \<Longrightarrow> valid_tcb' (tcbPriority_update f tcb) s" apply (simp add: valid_tcb'_def tcb_cte_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_tcb' tcb s; f (tcbPriority tcb) \<le> maxPriority\<rbrakk> \<Longrightarrow> valid_tcb' (tcbPriority_update f tcb) s proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma setPriority_corres: "corres dc (einvs and tcb_at t) (invs' and tcb_at' t and valid_objs' and (\<lambda>_. x \<le> maxPriority))
                     (set_priority t x) (setPriority t x)" apply (rule corres_guard_imp) apply (rule sp_corres2) apply (clarsimp simp: valid_sched_def valid_sched_action_def) apply (clarsimp simp: invs'_def valid_state'_def sch_act_wf_weak) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t and valid_objs' and (\<lambda>_. x \<le> maxPriority)) (set_priority t x) (setPriority t x) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (set_priority t x) (setPriority t x)
 2. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and tcb_at' t and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s \<Longrightarrow> ?Q' s proof (prove)
goal (2 subgoals):
 1. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (valid_etcbs and weak_valid_sched_action and cur_tcb) s
 2. \<And>s. (invs' and tcb_at' t and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and tcb_at' t and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma setMCPriority_corres: "corres dc (tcb_at t) (tcb_at' t)
                     (set_mcpriority t x) (setMCPriority t x)" apply (rule corres_guard_imp) apply (clarsimp simp: setMCPriority_def set_mcpriority_def) apply (rule threadset_corresT) by (clarsimp simp: tcb_relation_def tcb_cap_cases_tcb_mcpriority
                          tcb_cte_cases_def exst_same_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t) (tcb_at' t) (set_mcpriority t x) (setMCPriority t x) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (set_mcpriority t x) (setMCPriority t x)
 2. \<And>s. tcb_at t s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (thread_set (tcb_mcpriority_update (\<lambda>_. x)) t) (threadSet (tcbMCP_update (\<lambda>_. x)) t)
 2. \<And>s. tcb_at t s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> tcb_relation (tcb\<lparr>tcb_mcpriority := x\<rparr>) (tcbMCP_update (\<lambda>_. x) tcb')
 2. \<And>tcb. \<forall>(getF, setF)\<in>ran tcb_cap_cases. getF (tcb\<lparr>tcb_mcpriority := x\<rparr>) = getF tcb
 3. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbMCP_update (\<lambda>_. x) tcb) = getF tcb
 4. \<And>tcb'. exst_same tcb' (tcbMCP_update (\<lambda>_. x) tcb')
 5. \<And>s. tcb_at t s \<Longrightarrow> tcb_at t s
 6. \<And>s. tcb_at' t s \<Longrightarrow> tcb_at' t s
theory Tcb_R

lemma out_corresT:
  assumes x: "\<And>tcb v. \<forall>(getF, setF)\<in>ran tcb_cap_cases. getF (fn v tcb) = getF tcb"
  assumes y: "\<And>v. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (fn' v tcb) = getF tcb"
  assumes e: "\<And>tcb v. exst_same tcb (fn' v tcb)"
  shows
  "out_rel fn fn' v v' \<Longrightarrow>
     corres dc (tcb_at t)
               (tcb_at' t)
       (option_update_thread t fn v)
       (case_option (return ()) (\<lambda>x. threadSet (fn' x) t) v')" apply (case_tac v, simp_all add: out_rel_def
                       option_update_thread_def) apply clarsimp apply (clarsimp simp add: threadset_corresT [OF _ x y e]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. out_rel fn fn' v v' \<Longrightarrow> corres dc (tcb_at t) (tcb_at' t) (option_update_thread t fn v) (case v' of None \<Rightarrow> return () | Some x \<Rightarrow> threadSet (fn' x) t) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>(\<exists>y. v' = Some y) \<and> (\<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> tcb_relation (fn a tcb) ((case v' of None \<Rightarrow> id | Some x2 \<Rightarrow> fn' x2) tcb')); v = Some a\<rbrakk> \<Longrightarrow> corres dc (tcb_at t) (tcb_at' t) (thread_set (fn a) t) (case v' of None \<Rightarrow> return () | Some x \<Rightarrow> threadSet (fn' x) t) proof (prove)
goal (1 subgoal):
 1. \<And>a y. \<lbrakk>v = Some a; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> tcb_relation (fn a tcb) (fn' y tcb'); v' = Some y\<rbrakk> \<Longrightarrow> corres dc (tcb_at t) (tcb_at' t) (thread_set (fn a) t) (threadSet (fn' y) t) proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma tcbSchedDequeue_sch_act_simple[wp]:
  "tcbSchedDequeue t \<lbrace>sch_act_simple\<rbrace>" by (wpsimp simp: sch_act_simple_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. sch_act_simple\<rbrace>
theory Tcb_R

lemma valid_queues_subsetE':
  "\<lbrakk> valid_queues' s; ksPSpace s = ksPSpace s';
     \<forall>x. set (ksReadyQueues s x) \<subseteq> set (ksReadyQueues s' x) \<rbrakk>
   \<Longrightarrow> valid_queues' s'" by (simp add: valid_queues'_def obj_at'_def
                ps_clear_def subset_iff projectKOs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_queues' s; ksPSpace s = ksPSpace s'; \<forall>x. set (ksReadyQueues s x) \<subseteq> set (ksReadyQueues s' x)\<rbrakk> \<Longrightarrow> valid_queues' s'
theory Tcb_R

lemma setQueue_invs_bits[wp]:
  "\<lbrace>valid_pspace'\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>"
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> setQueue d p q \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
  "\<lbrace>\<lambda>s. sym_refs (state_refs_of' s)\<rbrace> setQueue d p q \<lbrace>\<lambda>rv s. sym_refs (state_refs_of' s)\<rbrace>"
  "\<lbrace>if_live_then_nonz_cap'\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>"
  "\<lbrace>if_unsafe_then_cap'\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>"
  "\<lbrace>cur_tcb'\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>"
  "\<lbrace>valid_global_refs'\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>"
  "\<lbrace>valid_irq_handlers'\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" by (simp add: setQueue_def tcb_in_cur_domain'_def
         | wp sch_act_wf_lift cur_tcb_lift
         | fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lbrace>valid_pspace'\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> &&& \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> setQueue d p q \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>) &&& \<lbrace>\<lambda>s. sym_refs (state_refs_of' s)\<rbrace> setQueue d p q \<lbrace>\<lambda>rv s. sym_refs (state_refs_of' s)\<rbrace> &&& \<lbrace>if_live_then_nonz_cap'\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>) &&& (\<lbrace>if_unsafe_then_cap'\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> &&& \<lbrace>cur_tcb'\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>) &&& \<lbrace>valid_global_refs'\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> &&& \<lbrace>valid_irq_handlers'\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>
theory Tcb_R

lemma setQueue_ex_idle_cap[wp]:
  "\<lbrace>\<lambda>s. ex_nonz_cap_to' (ksIdleThread s) s\<rbrace>
   setQueue d p q
   \<lbrace>\<lambda>rv s. ex_nonz_cap_to' (ksIdleThread s) s\<rbrace>" by (simp add: setQueue_def, wp,
      simp add: ex_nonz_cap_to'_def cte_wp_at_pspaceI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ex_nonz_cap_to' (ksIdleThread s) s\<rbrace> setQueue d p q \<lbrace>\<lambda>rv s. ex_nonz_cap_to' (ksIdleThread s) s\<rbrace>
theory Tcb_R

lemma tcbPriority_caps_safe:
  "\<forall>tcb. \<forall>x\<in>ran tcb_cte_cases. (\<lambda>(getF, setF). getF (tcbPriority_update f tcb) = getF tcb) x" by (rule all_tcbI, rule ball_tcb_cte_casesI, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>tcb. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbPriority_update f tcb) = getF tcb