theory TcbAcc_R

lemma thread_get_isRunnable_corres: "corres (=) (tcb_at t) (tcb_at' t) (thread_get (\<lambda>tcb. runnable (tcb_state tcb)) t) (isRunnable t)" apply (simp add:  isRunnable_def getThreadState_def threadGet_def
                   thread_get_def) apply (fold liftM_def) apply simp apply (rule corres_rel_imp) apply (rule getObject_TCB_corres) apply (clarsimp simp add: tcb_relation_def thread_state_relation_def) apply (case_tac "tcb_state x",simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t) (thread_get (\<lambda>tcb. runnable (tcb_state tcb)) t) (isRunnable t) proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t) (do tcb <- gets_the (get_tcb t);
return (runnable (tcb_state tcb))
od) (do state <- liftM tcbState (getObject 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 (=) (tcb_at t) (tcb_at' t) (liftM (\<lambda>tcb. runnable (tcb_state tcb)) (gets_the (get_tcb t))) (liftM (\<lambda>state. case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) (liftM tcbState (getObject t))) proof (prove)
goal (1 subgoal):
 1. corres ((\<lambda>x. (=) x \<circ> Structures_H.thread_state.case_thread_state (\<lambda>word bool. False) False (\<lambda>word. False) True False False (\<lambda>word1 word2 bool1 bool2 bool3. False) True \<circ> tcbState) \<circ> (\<lambda>tcb. runnable (tcb_state tcb))) (tcb_at t) (tcb_at' t) (gets_the (get_tcb t)) (getObject t) proof (prove)
goal (2 subgoals):
 1. corres ?r' (tcb_at t) (tcb_at' t) (gets_the (get_tcb t)) (getObject t)
 2. \<And>x y. ?r' x y \<Longrightarrow> ((\<lambda>x. (=) x \<circ> Structures_H.thread_state.case_thread_state (\<lambda>word bool. False) False (\<lambda>word. False) True False False (\<lambda>word1 word2 bool1 bool2 bool3. False) True \<circ> tcbState) \<circ> (\<lambda>tcb. runnable (tcb_state tcb))) x y proof (prove)
goal (1 subgoal):
 1. \<And>x y. tcb_relation x y \<Longrightarrow> ((\<lambda>x. (=) x \<circ> Structures_H.thread_state.case_thread_state (\<lambda>word bool. False) False (\<lambda>word. False) True False False (\<lambda>word1 word2 bool1 bool2 bool3. False) True \<circ> tcbState) \<circ> (\<lambda>tcb. runnable (tcb_state tcb))) x y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>tcb_fault_handler x = to_bl (tcbFaultHandler y); tcb_ipc_buffer x = tcbIPCBuffer y; arch_tcb_relation (tcb_arch x) (tcbArch y); Structures_A.thread_state.rec_thread_state (\<lambda>ts'. ts' = Structures_H.thread_state.Running) (\<lambda>ts'. ts' = Structures_H.thread_state.Inactive) (\<lambda>ts'. ts' = Structures_H.thread_state.Restart) (\<lambda>oref sp ts'. ts' = Structures_H.thread_state.BlockedOnReceive oref (receiver_can_grant sp)) (\<lambda>oref sp ts'. ts' = Structures_H.thread_state.BlockedOnSend oref (sender_badge sp) (sender_can_grant sp) (sender_can_grant_reply sp) (sender_is_call sp)) awaiting_reply' (\<lambda>oref ts'. ts' = Structures_H.thread_state.BlockedOnNotification oref) idle' (tcb_state x) (tcbState y); fault_rel_optionation (tcb_fault x) (tcbFault y); cap_relation (tcb_ctable x) (cteCap (tcbCTable y)); cap_relation (tcb_vtable x) (cteCap (tcbVTable y)); cap_relation (tcb_reply x) (cteCap (tcbReply y)); cap_relation (tcb_caller x) (cteCap (tcbCaller y)); cap_relation (tcb_ipcframe x) (cteCap (tcbIPCBufferFrame y)); tcb_bound_notification x = tcbBoundNotification y; tcb_mcpriority x = tcbMCP y\<rbrakk> \<Longrightarrow> runnable (tcb_state x) = (case tcbState y of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) proof (prove)
goal:
No subgoals!