theory Tcb_R

lemma activateThread_corres:
 "corres dc (invs and ct_in_state activatable) (invs' and ct_in_state' activatable')
            activate_thread activateThread" supply subst_all [simp del] apply (simp add: activate_thread_def activateThread_def) apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF getCurThread_corres]) apply (rule_tac R="\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts)
                                \<and> invs s \<and> st_tcb_at ((=) ts) thread s"
                  and R'="\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts)
                                \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s"
                  in  corres_split[OF getThreadState_corres]) apply (rule_tac F="idle rv \<or> runnable rv" in corres_req, simp) apply (rule_tac F="idle' rv' \<or> runnable' rv'" in corres_req, simp) apply (case_tac rv, simp_all add:
                  isRunning_def isRestart_def,
                  safe, simp_all)[1] apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF asUser_getRestartPC_corres]) apply (rule corres_split_nor[OF asUser_setNextPC_corres]) apply (rule setThreadState_corres) apply (simp | wp weak_sch_act_wf_lift_linear)+ apply (clarsimp simp: st_tcb_at_tcb_at) apply fastforce apply (rule corres_guard_imp) apply (rule activateIdleThread_corres) apply (clarsimp elim!: st_tcb_weakenE) apply (clarsimp elim!: pred_tcb'_weakenE) apply (wp gts_st_tcb gts_st_tcb' gts_st_tcb_at)+ apply (clarsimp simp: ct_in_state_def tcb_at_invs
                  elim!: st_tcb_weakenE) apply (clarsimp simp: tcb_at_invs' ct_in_state'_def
                 elim!: pred_tcb'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (invs and ct_in_state activatable) (invs' and ct_in_state' activatable') activate_thread activateThread proof (prove)
goal (1 subgoal):
 1. corres dc (invs and ct_in_state activatable) (invs' and ct_in_state' activatable') activate_thread activateThread proof (prove)
goal (1 subgoal):
 1. corres dc (invs and ct_in_state activatable) (invs' and ct_in_state' activatable') (do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Structures_A.thread_state.Running \<Rightarrow> return () | Structures_A.thread_state.Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Structures_A.thread_state.Running
od | Structures_A.thread_state.IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od) (do thread <- getCurThread;
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;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> haskell_fail $ [] @ show state
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Structures_A.thread_state.Running \<Rightarrow> return () | Structures_A.thread_state.Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Structures_A.thread_state.Running
od | Structures_A.thread_state.IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od) (do thread <- getCurThread;
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;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> haskell_fail $ [] @ show state
od)
 2. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>thread. corres dc (?R4 thread) (?R'4 thread) (do state <- get_thread_state thread;
case state of Structures_A.thread_state.Running \<Rightarrow> return () | Structures_A.thread_state.Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Structures_A.thread_state.Running
od | Structures_A.thread_state.IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od) (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;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> haskell_fail $ [] @ show state
od)
 2. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>?R'4\<rbrace>
 4. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread rv rv'. thread_state_relation rv rv' \<Longrightarrow> corres dc (\<lambda>s. valid_tcb_state rv s \<and> (idle rv \<or> runnable rv) \<and> invs s \<and> st_tcb_at ((=) rv) thread s) (\<lambda>s. valid_tcb_state' rv' s \<and> (idle' rv' \<or> runnable' rv') \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = rv') thread s) (case rv of Structures_A.thread_state.Running \<Rightarrow> return () | Structures_A.thread_state.Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Structures_A.thread_state.Running
od | Structures_A.thread_state.IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail) (case rv' 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;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> haskell_fail $ [] @ show rv')
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. tcb_at thread and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and ?Q'8 thread\<rbrace>
 6. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread rv rv'. \<lbrakk>thread_state_relation rv rv'; idle rv \<or> runnable rv\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. valid_tcb_state rv s \<and> (idle rv \<or> runnable rv) \<and> invs s \<and> st_tcb_at ((=) rv) thread s) (\<lambda>s. valid_tcb_state' rv' s \<and> (idle' rv' \<or> runnable' rv') \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = rv') thread s) (case rv of Structures_A.thread_state.Running \<Rightarrow> return () | Structures_A.thread_state.Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Structures_A.thread_state.Running
od | Structures_A.thread_state.IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail) (case rv' 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;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> haskell_fail $ [] @ show rv')
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. tcb_at thread and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and ?Q'8 thread\<rbrace>
 6. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread rv rv'. \<lbrakk>thread_state_relation rv rv'; idle rv \<or> runnable rv; idle' rv' \<or> runnable' rv'\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. valid_tcb_state rv s \<and> (idle rv \<or> runnable rv) \<and> invs s \<and> st_tcb_at ((=) rv) thread s) (\<lambda>s. valid_tcb_state' rv' s \<and> (idle' rv' \<or> runnable' rv') \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = rv') thread s) (case rv of Structures_A.thread_state.Running \<Rightarrow> return () | Structures_A.thread_state.Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Structures_A.thread_state.Running
od | Structures_A.thread_state.IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail) (case rv' 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;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> haskell_fail $ [] @ show rv')
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. tcb_at thread and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and ?Q'8 thread\<rbrace>
 6. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>thread. corres dc (\<lambda>s. valid_tcb_state Structures_A.thread_state.Restart s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.Restart) thread s) (\<lambda>s. valid_tcb_state' Structures_H.thread_state.Restart s \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = Structures_H.thread_state.Restart) thread s) (do pc <- as_user thread getRestartPC;
y <- as_user thread (setNextPC pc);
set_thread_state thread Structures_A.thread_state.Running
od) (do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od)
 2. \<And>thread. corres dc (\<lambda>s. valid_tcb_state Structures_A.thread_state.IdleThreadState s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.IdleThreadState) thread s) (\<lambda>s. valid_tcb_state' Structures_H.thread_state.IdleThreadState s \<and> invs' s \<and> st_tcb_at' idle' thread s) (arch_activate_idle_thread thread) (activateIdleThread thread)
 3. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 4. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. tcb_at thread and ?Q8 thread\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and ?Q'8 thread\<rbrace>
 7. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>thread. corres dc (?Q19 thread) (?Q'19 thread) (do pc <- as_user thread getRestartPC;
y <- as_user thread (setNextPC pc);
set_thread_state thread Structures_A.thread_state.Running
od) (do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od)
 2. \<And>thread s. valid_tcb_state Structures_A.thread_state.Restart s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.Restart) thread s \<Longrightarrow> ?Q19 thread s
 3. \<And>thread s. valid_tcb_state' Structures_H.thread_state.Restart s \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = Structures_H.thread_state.Restart) thread s \<Longrightarrow> ?Q'19 thread s
 4. \<And>thread. corres dc (\<lambda>s. valid_tcb_state Structures_A.thread_state.IdleThreadState s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.IdleThreadState) thread s) (\<lambda>s. valid_tcb_state' Structures_H.thread_state.IdleThreadState s \<and> invs' s \<and> st_tcb_at' idle' thread s) (arch_activate_idle_thread thread) (activateIdleThread thread)
 5. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 6. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
 7. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. tcb_at thread and ?Q8 thread\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and ?Q'8 thread\<rbrace>
 9. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 10. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (12 subgoals):
 1. \<And>thread pc. corres dc (?R23 thread pc) (?R'23 thread pc) (do y <- as_user thread (setNextPC pc);
set_thread_state thread Structures_A.thread_state.Running
od) (do y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od)
 2. \<And>thread. \<lbrace>?Q23 thread\<rbrace> as_user thread getRestartPC \<lbrace>?R23 thread\<rbrace>
 3. \<And>thread. \<lbrace>?Q'23 thread\<rbrace> asUser thread getRestartPC \<lbrace>?R'23 thread\<rbrace>
 4. \<And>thread s. valid_tcb_state Structures_A.thread_state.Restart s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.Restart) thread s \<Longrightarrow> (tcb_at thread and ?Q23 thread) s
 5. \<And>thread s. valid_tcb_state' Structures_H.thread_state.Restart s \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = Structures_H.thread_state.Restart) thread s \<Longrightarrow> (tcb_at' thread and ?Q'23 thread) s
 6. \<And>thread. corres dc (\<lambda>s. valid_tcb_state Structures_A.thread_state.IdleThreadState s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.IdleThreadState) thread s) (\<lambda>s. valid_tcb_state' Structures_H.thread_state.IdleThreadState s \<and> invs' s \<and> st_tcb_at' idle' thread s) (arch_activate_idle_thread thread) (activateIdleThread thread)
 7. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 8. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
 9. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. tcb_at thread and ?Q8 thread\<rbrace>
 10. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and ?Q'8 thread\<rbrace>
A total of 12 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>thread pc. corres dc (?R28 thread pc) (?R'28 thread pc) (set_thread_state thread Structures_A.thread_state.Running) (setThreadState Structures_H.thread_state.Running thread)
 2. \<And>thread pc. \<lbrace>?Q28 thread pc\<rbrace> as_user thread (setNextPC pc) \<lbrace>\<lambda>x. ?R28 thread pc\<rbrace>
 3. \<And>thread pc. \<lbrace>?Q'28 thread pc\<rbrace> asUser thread (setNextPC pc) \<lbrace>\<lambda>x. ?R'28 thread pc\<rbrace>
 4. \<And>thread. \<lbrace>?Q23 thread\<rbrace> as_user thread getRestartPC \<lbrace>\<lambda>pc. tcb_at thread and invs and ?Q28 thread pc\<rbrace>
 5. \<And>thread. \<lbrace>?Q'23 thread\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>pc. tcb_at' thread and invs' and ?Q'28 thread pc\<rbrace>
 6. \<And>thread s. valid_tcb_state Structures_A.thread_state.Restart s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.Restart) thread s \<Longrightarrow> (tcb_at thread and ?Q23 thread) s
 7. \<And>thread s. valid_tcb_state' Structures_H.thread_state.Restart s \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = Structures_H.thread_state.Restart) thread s \<Longrightarrow> (tcb_at' thread and ?Q'23 thread) s
 8. \<And>thread. corres dc (\<lambda>s. valid_tcb_state Structures_A.thread_state.IdleThreadState s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.IdleThreadState) thread s) (\<lambda>s. valid_tcb_state' Structures_H.thread_state.IdleThreadState s \<and> invs' s \<and> st_tcb_at' idle' thread s) (arch_activate_idle_thread thread) (activateIdleThread thread)
 9. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 10. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>thread pc. thread_state_relation Structures_A.thread_state.Running Structures_H.thread_state.Running
 2. \<And>thread pc. \<lbrace>?Q28 thread pc\<rbrace> as_user thread (setNextPC pc) \<lbrace>\<lambda>x. tcb_at thread\<rbrace>
 3. \<And>thread pc. \<lbrace>?Q'28 thread pc\<rbrace> asUser thread (setNextPC pc) \<lbrace>\<lambda>x. tcb_at' thread\<rbrace>
 4. \<And>thread. \<lbrace>?Q23 thread\<rbrace> as_user thread getRestartPC \<lbrace>\<lambda>pc. tcb_at thread and invs and ?Q28 thread pc\<rbrace>
 5. \<And>thread. \<lbrace>?Q'23 thread\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>pc. tcb_at' thread and invs' and ?Q'28 thread pc\<rbrace>
 6. \<And>thread s. valid_tcb_state Structures_A.thread_state.Restart s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.Restart) thread s \<Longrightarrow> (tcb_at thread and ?Q23 thread) s
 7. \<And>thread s. valid_tcb_state' Structures_H.thread_state.Restart s \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = Structures_H.thread_state.Restart) thread s \<Longrightarrow> (tcb_at' thread and ?Q'23 thread) s
 8. \<And>thread. corres dc (\<lambda>s. valid_tcb_state Structures_A.thread_state.IdleThreadState s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.IdleThreadState) thread s) (\<lambda>s. valid_tcb_state' Structures_H.thread_state.IdleThreadState s \<and> invs' s \<and> st_tcb_at' idle' thread s) (arch_activate_idle_thread thread) (activateIdleThread thread)
 9. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 10. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
A total of 14 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>thread s. valid_tcb_state Structures_A.thread_state.Restart s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.Restart) thread s \<Longrightarrow> tcb_at thread s
 2. \<And>thread s. valid_tcb_state' Structures_H.thread_state.Restart s \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = Structures_H.thread_state.Restart) thread s \<Longrightarrow> (tcb_at' thread and (\<lambda>s. tcb_at' thread s \<and> (invs' and tcb_at' thread) s \<and> tcb_at' thread s)) s
 3. \<And>thread. corres dc (\<lambda>s. valid_tcb_state Structures_A.thread_state.IdleThreadState s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.IdleThreadState) thread s) (\<lambda>s. valid_tcb_state' Structures_H.thread_state.IdleThreadState s \<and> invs' s \<and> st_tcb_at' idle' thread s) (arch_activate_idle_thread thread) (activateIdleThread thread)
 4. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 5. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. tcb_at thread and ?Q8 thread\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and ?Q'8 thread\<rbrace>
 8. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>thread s. valid_tcb_state' Structures_H.thread_state.Restart s \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = Structures_H.thread_state.Restart) thread s \<Longrightarrow> (tcb_at' thread and (\<lambda>s. tcb_at' thread s \<and> (invs' and tcb_at' thread) s \<and> tcb_at' thread s)) s
 2. \<And>thread. corres dc (\<lambda>s. valid_tcb_state Structures_A.thread_state.IdleThreadState s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.IdleThreadState) thread s) (\<lambda>s. valid_tcb_state' Structures_H.thread_state.IdleThreadState s \<and> invs' s \<and> st_tcb_at' idle' thread s) (arch_activate_idle_thread thread) (activateIdleThread thread)
 3. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 4. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. tcb_at thread and ?Q8 thread\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and ?Q'8 thread\<rbrace>
 7. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread. corres dc (\<lambda>s. valid_tcb_state Structures_A.thread_state.IdleThreadState s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.IdleThreadState) thread s) (\<lambda>s. valid_tcb_state' Structures_H.thread_state.IdleThreadState s \<and> invs' s \<and> st_tcb_at' idle' thread s) (arch_activate_idle_thread thread) (activateIdleThread thread)
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. tcb_at thread and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and ?Q'8 thread\<rbrace>
 6. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>thread. corres dc (?Q72 thread) (?Q'72 thread) (arch_activate_idle_thread thread) (activateIdleThread thread)
 2. \<And>thread s. valid_tcb_state Structures_A.thread_state.IdleThreadState s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.IdleThreadState) thread s \<Longrightarrow> ?Q72 thread s
 3. \<And>thread s. valid_tcb_state' Structures_H.thread_state.IdleThreadState s \<and> invs' s \<and> st_tcb_at' idle' thread s \<Longrightarrow> ?Q'72 thread s
 4. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 5. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. tcb_at thread and ?Q8 thread\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and ?Q'8 thread\<rbrace>
 8. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>thread s. valid_tcb_state Structures_A.thread_state.IdleThreadState s \<and> invs s \<and> st_tcb_at ((=) Structures_A.thread_state.IdleThreadState) thread s \<Longrightarrow> (invs and st_tcb_at idle thread) s
 2. \<And>thread s. valid_tcb_state' Structures_H.thread_state.IdleThreadState s \<and> invs' s \<and> st_tcb_at' idle' thread s \<Longrightarrow> (invs' and st_tcb_at' idle' thread) s
 3. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 4. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. tcb_at thread and ?Q8 thread\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and ?Q'8 thread\<rbrace>
 7. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread s. valid_tcb_state' Structures_H.thread_state.IdleThreadState s \<and> invs' s \<and> st_tcb_at' idle' thread s \<Longrightarrow> (invs' and st_tcb_at' idle' thread) s
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. tcb_at thread and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and ?Q'8 thread\<rbrace>
 6. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>thread. \<lbrace>?Q8 thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>ts s. valid_tcb_state ts s \<and> (idle ts \<or> runnable ts) \<and> invs s \<and> st_tcb_at ((=) ts) thread s\<rbrace>
 2. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>ts s. valid_tcb_state' ts s \<and> (idle' ts \<or> runnable' ts) \<and> invs' s \<and> st_tcb_at' (\<lambda>ts'. ts' = ts) thread s\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. tcb_at thread and ?Q8 thread\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>thread. tcb_at' thread and ?Q'8 thread\<rbrace>
 5. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs and ct_in_state activatable) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at (cur_thread s) and (\<lambda>sa. (tcb_at (cur_thread s) and invs) sa \<and> st_tcb_at (\<lambda>rv. idle rv \<or> runnable rv) (cur_thread s) sa \<and> invs sa \<and> True)) s)) s
 2. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at' (ksCurThread s) and (\<lambda>sa. (tcb_at' (ksCurThread s) and invs') sa \<and> st_tcb_at' (\<lambda>rv. idle' rv \<or> runnable' rv) (ksCurThread s) sa \<and> invs' sa \<and> True)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and ct_in_state' activatable') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at' (ksCurThread s) and (\<lambda>sa. (tcb_at' (ksCurThread s) and invs') sa \<and> st_tcb_at' (\<lambda>rv. idle' rv \<or> runnable' rv) (ksCurThread s) sa \<and> invs' sa \<and> True)) s)) s proof (prove)
goal:
No subgoals!