theory Tcb_R

lemma activate_sch_act:
  "\<lbrace>ct_in_state' activatable' and (\<lambda>s. P (ksSchedulerAction s))\<rbrace>
     activateThread \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" apply (simp add: activateThread_def getCurThread_def
             cong: if_cong Structures_H.thread_state.case_cong) apply (rule hoare_seq_ext [OF _ gets_sp]) apply (rule hoare_seq_ext[where B="\<lambda>st s. (runnable' or idle') st
                                          \<and> P (ksSchedulerAction s)"]) apply (rule hoare_pre) apply (wp | wpc | simp add: setThreadState_runnable_simp)+ apply (clarsimp simp: ct_in_state'_def cur_tcb'_def pred_tcb_at'
                 elim!: pred_tcb'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' activatable' and (\<lambda>s. P (ksSchedulerAction s))\<rbrace> activateThread \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' activatable' and (\<lambda>s. P (ksSchedulerAction s))\<rbrace> do thread <- gets ksCurThread;
state <- getThreadState thread;
case state of Structures_H.thread_state.Running \<Rightarrow> return () | Structures_H.thread_state.IdleThreadState \<Rightarrow> activateIdleThread thread | Structures_H.thread_state.Restart \<Rightarrow> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>thread. \<lbrace>ct_in_state' activatable' and (\<lambda>s. P (ksSchedulerAction s)) and (\<lambda>s. ksCurThread s = thread)\<rbrace> do state <- getThreadState thread;
case state of Structures_H.thread_state.Running \<Rightarrow> return () | Structures_H.thread_state.IdleThreadState \<Rightarrow> activateIdleThread thread | Structures_H.thread_state.Restart \<Rightarrow> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>thread state. \<lbrace>\<lambda>s. (runnable' or idle') state \<and> P (ksSchedulerAction s)\<rbrace> case state of Structures_H.thread_state.Running \<Rightarrow> return () | Structures_H.thread_state.IdleThreadState \<Rightarrow> activateIdleThread thread | Structures_H.thread_state.Restart \<Rightarrow> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> fail \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>
 2. \<And>thread. \<lbrace>ct_in_state' activatable' and (\<lambda>s. P (ksSchedulerAction s)) and (\<lambda>s. ksCurThread s = thread)\<rbrace> getThreadState thread \<lbrace>\<lambda>st s. (runnable' or idle') st \<and> P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread state. \<lbrace>?Q18 thread state\<rbrace> case state of Structures_H.thread_state.Running \<Rightarrow> return () | Structures_H.thread_state.IdleThreadState \<Rightarrow> activateIdleThread thread | Structures_H.thread_state.Restart \<Rightarrow> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> fail \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>
 2. \<And>thread state s. (runnable' or idle') state \<and> P (ksSchedulerAction s) \<Longrightarrow> ?Q18 thread state s
 3. \<And>thread. \<lbrace>ct_in_state' activatable' and (\<lambda>s. P (ksSchedulerAction s)) and (\<lambda>s. ksCurThread s = thread)\<rbrace> getThreadState thread \<lbrace>\<lambda>st s. (runnable' or idle') st \<and> P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_in_state' activatable' s \<and> P (ksSchedulerAction s) \<Longrightarrow> st_tcb_at' activatable' (ksCurThread s) s proof (prove)
goal:
No subgoals!