theory Tcb_R

lemma activate_invs':
  "\<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace>
     activateThread
   \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace>" apply (simp add: activateThread_def) apply (rule hoare_seq_ext) apply (rule_tac B="\<lambda>state s. invs' s \<and> sch_act_simple s
                              \<and> st_tcb_at' (\<lambda>st. st = state) thread s
                              \<and> thread = ksCurThread s
                              \<and> (runnable' state \<or> idle' state)" in hoare_seq_ext) apply (case_tac x, simp_all add: isTS_defs hoare_pre_cont
                       split del: if_splits cong: if_cong) apply (wp) apply (clarsimp simp: ct_in_state'_def) apply (rule_tac Q="\<lambda>rv. invs' and ct_idle'" in hoare_post_imp, simp) apply (wp activateIdle_invs) apply (clarsimp simp: ct_in_state'_def) apply (rule_tac Q="\<lambda>rv. invs' and ct_running' and sch_act_simple"
                 in hoare_post_imp, simp) apply (rule hoare_weaken_pre) apply (wp ct_in_state'_set asUser_ct sts_invs_minor'
          | wp (once) sch_act_simple_lift)+ apply (rule_tac Q="\<lambda>_. st_tcb_at' runnable' thread
                             and sch_act_simple and invs'
                             and (\<lambda>s. thread = ksCurThread s)"
               in hoare_post_imp, clarsimp) apply (wp sch_act_simple_lift)+ apply (clarsimp simp: valid_idle'_def invs'_def valid_state'_def
                          pred_tcb_at'_def obj_at'_def idle_tcb'_def
                   elim!: pred_tcb'_weakenE) apply (wp gts_st_tcb')+ apply (clarsimp simp: tcb_at_invs' ct_in_state'_def
                         pred_disj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> activateThread \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> 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 \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>thread. \<lbrace>?B 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;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> haskell_fail $ [] @ show state
od \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace>
 2. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread x. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = x) thread s \<and> thread = ksCurThread s \<and> activatable' x\<rbrace> case x 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 x \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace>
 2. \<And>thread. \<lbrace>?B thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = state) thread s \<and> thread = ksCurThread s \<and> activatable' state\<rbrace>
 3. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>thread. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) thread s \<and> thread = ksCurThread s\<rbrace> return () \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace>
 2. \<And>thread. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' idle' thread s \<and> thread = ksCurThread s\<rbrace> activateIdleThread thread \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace>
 3. \<And>thread. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) thread s \<and> thread = ksCurThread s\<rbrace> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace>
 4. \<And>thread. \<lbrace>?B thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = state) thread s \<and> thread = ksCurThread s \<and> activatable' state\<rbrace>
 5. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>thread s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) thread s \<and> thread = ksCurThread s \<Longrightarrow> (invs' and (ct_running' or ct_idle')) s
 2. \<And>thread. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' idle' thread s \<and> thread = ksCurThread s\<rbrace> activateIdleThread thread \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace>
 3. \<And>thread. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) thread s \<and> thread = ksCurThread s\<rbrace> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace>
 4. \<And>thread. \<lbrace>?B thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = state) thread s \<and> thread = ksCurThread s \<and> activatable' state\<rbrace>
 5. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>thread. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' idle' thread s \<and> thread = ksCurThread s\<rbrace> activateIdleThread thread \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace>
 2. \<And>thread. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) thread s \<and> thread = ksCurThread s\<rbrace> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace>
 3. \<And>thread. \<lbrace>?B thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = state) thread s \<and> thread = ksCurThread s \<and> activatable' state\<rbrace>
 4. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>thread. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' idle' thread s \<and> thread = ksCurThread s\<rbrace> activateIdleThread thread \<lbrace>\<lambda>rv. invs' and ct_idle'\<rbrace>
 2. \<And>thread. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) thread s \<and> thread = ksCurThread s\<rbrace> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace>
 3. \<And>thread. \<lbrace>?B thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = state) thread s \<and> thread = ksCurThread s \<and> activatable' state\<rbrace>
 4. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>thread s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' idle' thread s \<and> thread = ksCurThread s \<Longrightarrow> (invs' and ct_idle') s
 2. \<And>thread. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) thread s \<and> thread = ksCurThread s\<rbrace> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace>
 3. \<And>thread. \<lbrace>?B thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = state) thread s \<and> thread = ksCurThread s \<and> activatable' state\<rbrace>
 4. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) thread s \<and> thread = ksCurThread s\<rbrace> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od \<lbrace>\<lambda>rv. invs' and (ct_running' or ct_idle')\<rbrace>
 2. \<And>thread. \<lbrace>?B thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = state) thread s \<and> thread = ksCurThread s \<and> activatable' state\<rbrace>
 3. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) thread s \<and> thread = ksCurThread s\<rbrace> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od \<lbrace>\<lambda>rv. invs' and ct_running' and sch_act_simple\<rbrace>
 2. \<And>thread. \<lbrace>?B thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = state) thread s \<and> thread = ksCurThread s \<and> activatable' state\<rbrace>
 3. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>thread. \<lbrace>?Q17 thread\<rbrace> do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od \<lbrace>\<lambda>rv. invs' and ct_running' and sch_act_simple\<rbrace>
 2. \<And>thread s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) thread s \<and> thread = ksCurThread s \<Longrightarrow> ?Q17 thread s
 3. \<And>thread. \<lbrace>?B thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = state) thread s \<and> thread = ksCurThread s \<and> activatable' state\<rbrace>
 4. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>thread pc. \<lbrace>?P'40 thread pc\<rbrace> asUser thread (setNextPC pc) \<lbrace>\<lambda>rv s. (runnable' Structures_H.thread_state.Running \<and> obj_at' tcbQueued thread s \<longrightarrow> st_tcb_at' runnable' thread s) \<and> sch_act_simple s \<and> invs' s \<and> (tcb_at' thread s \<and> Structures_H.thread_state.Running = Structures_H.thread_state.Running \<and> thread = ksCurThread s) \<and> sch_act_simple s\<rbrace>
 2. \<And>thread. \<lbrace>?Q17 thread\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>pc s. st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Running \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread s \<and> (thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> ((\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Running) \<and> ?P'40 thread pc s\<rbrace>
 3. \<And>thread s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) thread s \<and> thread = ksCurThread s \<Longrightarrow> ?Q17 thread s
 4. \<And>thread. \<lbrace>?B thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = state) thread s \<and> thread = ksCurThread s \<and> activatable' state\<rbrace>
 5. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>thread pc. \<lbrace>?P'40 thread pc\<rbrace> asUser thread (setNextPC pc) \<lbrace>\<lambda>_. st_tcb_at' runnable' thread and sch_act_simple and invs' and (\<lambda>s. thread = ksCurThread s)\<rbrace>
 2. \<And>thread. \<lbrace>?Q17 thread\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>pc s. st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Running \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread s \<and> (thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> ((\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Running) \<and> ?P'40 thread pc s\<rbrace>
 3. \<And>thread s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) thread s \<and> thread = ksCurThread s \<Longrightarrow> ?Q17 thread s
 4. \<And>thread. \<lbrace>?B thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = state) thread s \<and> thread = ksCurThread s \<and> activatable' state\<rbrace>
 5. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) thread s \<and> thread = ksCurThread s \<Longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Running \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread s \<and> (thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> ((\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Running) \<and> st_tcb_at' runnable' thread s \<and> sch_act_simple s \<and> (invs' and tcb_at' thread) s \<and> tcb_at' thread s \<and> thread = ksCurThread s
 2. \<And>thread. \<lbrace>?B thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = state) thread s \<and> thread = ksCurThread s \<and> activatable' state\<rbrace>
 3. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>thread. \<lbrace>?B thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' (\<lambda>st. st = state) thread s \<and> thread = ksCurThread s \<and> activatable' state\<rbrace>
 2. \<lbrace>invs' and sch_act_simple and ct_in_state' activatable'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and sch_act_simple and ct_in_state' activatable') s \<Longrightarrow> invs' s \<and> sch_act_simple s \<and> tcb_at' (ksCurThread s) s \<and> ksCurThread s = ksCurThread s \<and> st_tcb_at' activatable' (ksCurThread s) s proof (prove)
goal:
No subgoals!