kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_R

lemma asUser_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t'\<rbrace> asUser t m \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace>" apply (simp add: asUser_def tcb_in_cur_domain'_def threadGet_def) apply (wp | wpc | simp)+ apply (rule_tac f="ksCurDomain" in hoare_lift_Pf) apply (wp threadSet_obj_at'_strongish getObject_tcb_wp | simp)+ apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t'\<rbrace> asUser t m \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> do uc <- liftM (atcbContextGet \<circ> tcbArch) (getObject t);
(a, uc') <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) t;
return a
od \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>uc x x1 x2. x = (x1, x2) \<Longrightarrow> \<lbrace>?R10 uc (x1, x2) x1 x2\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet x2 (tcbArch tcb)) tcb) t \<lbrace>\<lambda>y a. obj_at' (\<lambda>tcb. ksCurDomain a = tcbDomain tcb) t' a\<rbrace>
 2. \<And>uc. \<lbrace>?B1 uc\<rbrace> select_f (m uc) \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> ?R10 uc x xa xb s\<rbrace>
 3. \<lbrace>?Q\<rbrace> liftM (atcbContextGet \<circ> tcbArch) (getObject t) \<lbrace>?B1\<rbrace>
 4. \<And>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>uc x x1 x2 xa. x = (x1, x2) \<Longrightarrow> \<lbrace>obj_at' (\<lambda>tcb. xa = tcbDomain tcb) t'\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet x2 (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. xa = tcbDomain tcb) t'\<rbrace>
 2. \<And>uc x x1 x2 P. x = (x1, x2) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet x2 (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 3. \<And>uc. \<lbrace>?B1 uc\<rbrace> select_f (m uc) \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace>
 4. \<lbrace>?Q\<rbrace> liftM (atcbContextGet \<circ> tcbArch) (getObject t) \<lbrace>?B1\<rbrace>
 5. \<And>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_tcbDomain_inv[wp]:
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> asUser t m \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" apply (simp add: asUser_def tcb_in_cur_domain'_def threadGet_def) apply (wp threadSet_obj_at'_strongish getObject_tcb_wp | wpc | simp | clarsimp simp: obj_at'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> asUser t m \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> do uc <- liftM (atcbContextGet \<circ> tcbArch) (getObject t);
(a, uc') <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) t;
return a
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_tcbPriority_inv[wp]:
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> asUser t m \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace>" apply (simp add: asUser_def tcb_in_cur_domain'_def threadGet_def) apply (wp threadSet_obj_at'_strongish getObject_tcb_wp | wpc | simp | clarsimp simp: obj_at'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> asUser t m \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> do uc <- liftM (atcbContextGet \<circ> tcbArch) (getObject t);
(a, uc') <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) t;
return a
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
    asUser t m \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" by (wp sch_act_wf_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> asUser t m \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
theory TcbAcc_R

lemma asUser_idle'[wp]:
  "\<lbrace>valid_idle'\<rbrace> asUser t m \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" apply (simp add: asUser_def split_def) apply (wpsimp wp: threadSet_idle' select_f_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> asUser t m \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_setRegister_corres:
  "corres dc (tcb_at t)
             (tcb_at' t)
             (as_user t (setRegister r v))
             (asUser t (setRegister r v))" apply (simp add: setRegister_def) apply (rule asUser_corres') apply (rule corres_modify'; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t) (tcb_at' t) (as_user t (setRegister r v)) (asUser t (setRegister r v)) proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t) (tcb_at' t) (as_user t (modify (\<lambda>uc. uc(r := v)))) (asUser t (modify (\<lambda>uc. uc(r := v)))) proof (prove)
goal (1 subgoal):
 1. corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (modify (\<lambda>uc. uc(r := v))) (modify (\<lambda>uc. uc(r := v))) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma getThreadState_corres:
  "corres thread_state_relation (tcb_at t) (tcb_at' t)
          (get_thread_state t) (getThreadState t)" apply (simp add: get_thread_state_def getThreadState_def) apply (rule threadGet_corres) apply (simp add: tcb_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres thread_state_relation (tcb_at t) (tcb_at' t) (get_thread_state t) (getThreadState t) proof (prove)
goal (1 subgoal):
 1. corres thread_state_relation (tcb_at t) (tcb_at' t) (thread_get tcb_state t) (threadGet tcbState t) proof (prove)
goal (1 subgoal):
 1. \<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> thread_state_relation (tcb_state tcb) (tcbState tcb') proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma gts_wf'[wp]: "\<lbrace>tcb_at' t and invs'\<rbrace> getThreadState t \<lbrace>valid_tcb_state'\<rbrace>" apply (simp add: getThreadState_def threadGet_def liftM_def) apply (wp getObject_tcb_wp) apply clarsimp apply (drule obj_at_ko_at', clarsimp) apply (frule ko_at_valid_objs', fastforce, simp add: projectKOs) apply (fastforce simp: valid_obj'_def valid_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t and invs'\<rbrace> getThreadState t \<lbrace>valid_tcb_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t and invs'\<rbrace> do x <- getObject t;
return (tcbState x)
od \<lbrace>valid_tcb_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at' t and invs') s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> valid_tcb_state' (tcbState ta) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>tcb_at' t s; invs' s\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s \<and> valid_tcb_state' (tcbState ta) s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>invs' s; ko_at' ko t s\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s \<and> valid_tcb_state' (tcbState ta) s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>invs' s; ko_at' ko t s; valid_obj' (injectKO ko) s\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s \<and> valid_tcb_state' (tcbState ta) s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma gts_st_tcb_at'[wp]: "\<lbrace>st_tcb_at' P t\<rbrace> getThreadState t \<lbrace>\<lambda>rv s. P rv\<rbrace>" apply (simp add: getThreadState_def threadGet_def liftM_def) apply wp apply (rule hoare_chain) apply (rule obj_at_getObject) apply (clarsimp simp: loadObject_default_def projectKOs in_monad) apply assumption apply simp apply (simp add: pred_tcb_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> getThreadState t \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> do x <- getObject t;
return (tcbState x)
od \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getObject t \<lbrace>\<lambda>x a. P (tcbState x)\<rbrace>
 2. \<And>s. st_tcb_at' P t s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P3\<rbrace> getObject t \<lbrace>?Q3\<rbrace>
 2. \<And>s. ?Q s \<Longrightarrow> ?P3 s
 3. \<And>rv s. ?Q3 rv s \<Longrightarrow> P (tcbState rv)
 4. \<And>s. st_tcb_at' P t s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>a b n ko s obj. \<lbrakk>(a, b) \<in> fst (loadObject t t n ko s); projectKO_opt ko = Some obj\<rbrakk> \<Longrightarrow> a = obj
 2. \<And>s. ?Q s \<Longrightarrow> obj_at' ?Q8 t s
 3. \<And>rv s. ?Q8 rv \<Longrightarrow> P (tcbState rv)
 4. \<And>s. st_tcb_at' P t s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>s. ?Q s \<Longrightarrow> obj_at' ?Q8 t s
 2. \<And>rv s. ?Q8 rv \<Longrightarrow> P (tcbState rv)
 3. \<And>s. st_tcb_at' P t s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ?Q8 rv \<Longrightarrow> P (tcbState rv)
 2. \<And>s. st_tcb_at' P t s \<Longrightarrow> obj_at' ?Q8 t s proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at' P t s \<Longrightarrow> obj_at' (\<lambda>rv. P (tcbState rv)) t s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma gts_inv'[wp]: "\<lbrace>P\<rbrace> getThreadState t \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: getThreadState_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getThreadState t \<lbrace>\<lambda>rv. P\<rbrace>
theory TcbAcc_R

lemma getBoundNotification_corres:
  "corres (=) (tcb_at t) (tcb_at' t)
          (get_bound_notification t) (getBoundNotification t)" apply (simp add: get_bound_notification_def getBoundNotification_def) apply (rule threadGet_corres) apply (simp add: tcb_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t) (get_bound_notification t) (getBoundNotification t) proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t) (thread_get tcb_bound_notification t) (threadGet tcbBoundNotification t) proof (prove)
goal (1 subgoal):
 1. \<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> tcb_bound_notification tcb = tcbBoundNotification tcb' proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma gbn_bound_tcb_at'[wp]: "\<lbrace>bound_tcb_at' P t\<rbrace> getBoundNotification t \<lbrace>\<lambda>rv s. P rv\<rbrace>" apply (simp add: getBoundNotification_def threadGet_def liftM_def) apply wp apply (rule hoare_strengthen_post) apply (rule obj_at_getObject) apply (clarsimp simp: loadObject_default_def projectKOs in_monad) apply simp apply (simp add: pred_tcb_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at' P t\<rbrace> getBoundNotification t \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at' P t\<rbrace> do x <- getObject t;
return (tcbBoundNotification x)
od \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getObject t \<lbrace>\<lambda>x a. P (tcbBoundNotification x)\<rbrace>
 2. \<And>s. bound_tcb_at' P t s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> getObject t \<lbrace>?Q3\<rbrace>
 2. \<And>rv s. ?Q3 rv s \<Longrightarrow> P (tcbBoundNotification rv)
 3. \<And>s. bound_tcb_at' P t s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>a b n ko s obj. \<lbrakk>(a, b) \<in> fst (loadObject t t n ko s); projectKO_opt ko = Some obj\<rbrakk> \<Longrightarrow> a = obj
 2. \<And>rv s. ?Q7 rv \<Longrightarrow> P (tcbBoundNotification rv)
 3. \<And>s. bound_tcb_at' P t s \<Longrightarrow> obj_at' ?Q7 t s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ?Q7 rv \<Longrightarrow> P (tcbBoundNotification rv)
 2. \<And>s. bound_tcb_at' P t s \<Longrightarrow> obj_at' ?Q7 t s proof (prove)
goal (1 subgoal):
 1. \<And>s. bound_tcb_at' P t s \<Longrightarrow> obj_at' (\<lambda>rv. P (tcbBoundNotification rv)) t s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma gbn_inv'[wp]: "\<lbrace>P\<rbrace> getBoundNotification t \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: getBoundNotification_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getBoundNotification t \<lbrace>\<lambda>rv. P\<rbrace>
theory TcbAcc_R

lemma isStopped_def2:
  "isStopped t = liftM (Not \<circ> activatable') (getThreadState t)" apply (unfold isStopped_def fun_app_def) apply (fold liftM_def) apply (rule arg_cong [where f="\<lambda>f. liftM f (getThreadState t)"]) apply (rule ext) apply (simp split: Structures_H.thread_state.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isStopped t = liftM (Not \<circ> activatable') (getThreadState t) proof (prove)
goal (1 subgoal):
 1. do state <- getThreadState t;
return (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True)
od = liftM (Not \<circ> activatable') (getThreadState t) proof (prove)
goal (1 subgoal):
 1. liftM (\<lambda>state. case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) (getThreadState t) = liftM (Not \<circ> activatable') (getThreadState t) proof (prove)
goal (1 subgoal):
 1. (\<lambda>state. case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = Not \<circ> activatable' proof (prove)
goal (1 subgoal):
 1. \<And>state. (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = (Not \<circ> activatable') state proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma isStopped_inv[wp]:
  "\<lbrace>P\<rbrace> isStopped t \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: isStopped_def2 | wp gts_inv')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> isStopped t \<lbrace>\<lambda>rv. P\<rbrace>
theory TcbAcc_R

lemma isRunnable_inv[wp]:
  "\<lbrace>P\<rbrace> isRunnable t \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: isRunnable_def2 | wp gts_inv')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> isRunnable t \<lbrace>\<lambda>rv. P\<rbrace>
theory TcbAcc_R

lemma setQueue_obj_at[wp]:
  "\<lbrace>obj_at' P t\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. obj_at' P t\<rbrace>" apply (simp add: setQueue_def) apply wp apply (fastforce intro: obj_at'_pspaceI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>) \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' P t s \<Longrightarrow> obj_at' P t (s\<lparr>ksReadyQueues := (ksReadyQueues s)((d, p) := q)\<rparr>) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setQueue_nosch[wp]:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
    setQueue d p ts
   \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" apply (simp add: setQueue_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setQueue d p ts \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := ts)\<rparr>) \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ksSchedulerAction s) \<Longrightarrow> P (ksSchedulerAction (s\<lparr>ksReadyQueues := (ksReadyQueues s)((d, p) := ts)\<rparr>)) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma gq_wp[wp]: "\<lbrace>\<lambda>s. Q (ksReadyQueues s (d, p)) s\<rbrace> getQueue d p \<lbrace>Q\<rbrace>" by (simp add: getQueue_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (ksReadyQueues s (d, p)) s\<rbrace> getQueue d p \<lbrace>Q\<rbrace>
theory TcbAcc_R

lemma no_fail_getQueue [wp]:
  "no_fail \<top> (getQueue d p)" by (simp add: getQueue_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (getQueue d p)
theory TcbAcc_R

lemma no_fail_setQueue [wp]:
  "no_fail \<top> (setQueue d p xs)" by (simp add: setQueue_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (setQueue d p xs)
theory TcbAcc_R

lemma in_magnitude_check':
  "\<lbrakk> is_aligned x n; (1 :: word32) < 2 ^ n; ksPSpace s x = Some y; ps = ksPSpace s \<rbrakk>
     \<Longrightarrow> ((v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x ps)) n s)) =
        (s' = s \<and> ps_clear x n s)" by (simp add: in_magnitude_check)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; ps = ksPSpace s\<rbrakk> \<Longrightarrow> ((v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x ps)) n s)) = (s' = s \<and> ps_clear x n s)
theory TcbAcc_R

lemma cdt_relation_trans_state[simp]:
  "cdt_relation (swp cte_at (trans_state f s)) m m' = cdt_relation (swp cte_at s) m m'" by (simp add: cdt_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt_relation (swp (cte_wp_at (\<lambda>_. True)) (trans_state f s)) m m' = cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) m m'
theory TcbAcc_R

lemma getObject_obj_at_tcb:
  "\<lbrace>obj_at' (\<lambda>t. P t t) p\<rbrace> getObject p \<lbrace>\<lambda>t::tcb. obj_at' (P t) p\<rbrace>" apply (wp getObject_tcb_wp) apply (drule obj_at_ko_at') apply clarsimp apply (rule exI, rule conjI, assumption) apply (erule obj_at'_weakenE) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>t. P t t) p\<rbrace> getObject p \<lbrace>\<lambda>t. obj_at' (P t) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (\<lambda>t. P t t) p s \<Longrightarrow> tcb_at' p s \<longrightarrow> (\<exists>t. ko_at' t p s \<and> obj_at' (P t) p s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>ko. ko_at' ko p s \<and> P ko ko \<Longrightarrow> tcb_at' p s \<longrightarrow> (\<exists>t. ko_at' t p s \<and> obj_at' (P t) p s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>ko_at' ko p s; P ko ko; tcb_at' p s\<rbrakk> \<Longrightarrow> \<exists>t. ko_at' t p s \<and> obj_at' (P t) p s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>ko_at' ko p s; P ko ko; tcb_at' p s\<rbrakk> \<Longrightarrow> obj_at' (P ko) p s proof (prove)
goal (1 subgoal):
 1. \<And>s ko k. \<lbrakk>P ko ko; tcb_at' p s; k = ko\<rbrakk> \<Longrightarrow> P ko k proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadGet_obj_at':
  "\<lbrace>obj_at' (\<lambda>t. P (f t) t) t\<rbrace> threadGet f t \<lbrace>\<lambda>rv. obj_at' (P rv) t\<rbrace>" by (simp add: threadGet_def o_def | wp getObject_obj_at_tcb)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>t. P (f t) t) t\<rbrace> threadGet f t \<lbrace>\<lambda>rv. obj_at' (P rv) t\<rbrace>
theory TcbAcc_R

lemma ethreadget_corres:
  assumes x: "\<And>etcb tcb'. etcb_relation etcb tcb' \<Longrightarrow> r (f etcb) (f' tcb')"
  shows      "corres r (is_etcb_at t) (tcb_at' t) (ethread_get f t) (threadGet f' t)" apply (simp add: ethread_get_def threadGet_def) apply (fold liftM_def) apply simp apply (rule corres_rel_imp) apply (rule corres_get_etcb) apply (simp add: x) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r (is_etcb_at t) (tcb_at' t) (ethread_get f t) (threadGet f' t) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>x. r x \<circ> f') (is_etcb_at t) (tcb_at' t) (do tcb <- gets_the (get_etcb t);
return (f tcb)
od) (getObject t) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>x. r x \<circ> f') (is_etcb_at t) (tcb_at' t) (liftM f (gets_the (get_etcb t))) (getObject t) proof (prove)
goal (1 subgoal):
 1. corres ((\<lambda>x. r x \<circ> f') \<circ> f) (is_etcb_at t) (tcb_at' t) (gets_the (get_etcb t)) (getObject t) proof (prove)
goal (2 subgoals):
 1. corres ?r' (is_etcb_at t) (tcb_at' t) (gets_the (get_etcb t)) (getObject t)
 2. \<And>x y. ?r' x y \<Longrightarrow> ((\<lambda>x. r x \<circ> f') \<circ> f) x y proof (prove)
goal (1 subgoal):
 1. \<And>x y. etcb_relation x y \<Longrightarrow> ((\<lambda>x. r x \<circ> f') \<circ> f) x y proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setQueue_corres:
  "corres dc \<top> \<top> (set_tcb_queue d p q) (setQueue d p q)" apply (rule corres_no_failI) apply wp apply (clarsimp simp: setQueue_def in_monad set_tcb_queue_def return_def simpler_modify_def) apply (fastforce simp: state_relation_def ready_queues_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (set_tcb_queue d p q) (setQueue d p q) proof (prove)
goal (2 subgoals):
 1. True \<Longrightarrow> no_fail (\<lambda>_. True) (setQueue d p q)
 2. \<forall>(s, s')\<in>state_relation. True \<and> True \<longrightarrow> (\<forall>(r', t')\<in>fst (setQueue d p q s'). \<exists>(r, t)\<in>fst (set_tcb_queue d p q s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. \<forall>(s, s')\<in>state_relation. True \<and> True \<longrightarrow> (\<forall>(r', t')\<in>fst (setQueue d p q s'). \<exists>(r, t)\<in>fst (set_tcb_queue d p q s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> state_relation \<Longrightarrow> (ready_queues_update (\<lambda>_ d' pa. if d' = d \<and> pa = p then q else ready_queues a d' pa) a, b\<lparr>ksReadyQueues := (ksReadyQueues b)((d, p) := q)\<rparr>) \<in> state_relation proof (prove)
goal:
No subgoals!