theory IsolatedThreadAction

lemma activateThread_simple_rewrite:
  "monadic_rewrite True True (ct_in_state' ((=) Running))
       (activateThread) (return ())" apply (simp add: activateThread_def) apply wp_pre apply (monadic_rewrite_symb_exec_l) apply (monadic_rewrite_symb_exec_l_known Running, simp) apply (rule monadic_rewrite_refl) apply wpsimp+ apply (clarsimp simp: ct_in_state'_def elim!: pred_tcb'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (ct_in_state' ((=) Structures_H.thread_state.Running)) activateThread (return ()) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (ct_in_state' ((=) Structures_H.thread_state.Running)) (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) (return ()) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (ct_in_state' ((=) Structures_H.thread_state.Running)) (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) (return ()) proof (prove)
goal (3 subgoals):
 1. \<And>thread. monadic_rewrite True True (?Q2 thread) (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) (return ())
 2. \<lbrace>?Q1\<rbrace> getCurThread \<lbrace>?Q2\<rbrace>
 3. \<And>s. ct_in_state' ((=) Structures_H.thread_state.Running) s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>thread. monadic_rewrite True True (?Q30 thread) (return ()) (return ())
 2. \<And>thread. \<lbrace>?P30 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv' _. rv' = Structures_H.thread_state.Running\<rbrace>
 3. \<lbrace>?Q1\<rbrace> getCurThread \<lbrace>\<lambda>thread. ?P30 thread and ?Q30 thread\<rbrace>
 4. \<And>s. ct_in_state' ((=) Structures_H.thread_state.Running) s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?P30 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv' _. rv' = Structures_H.thread_state.Running\<rbrace>
 2. \<lbrace>?Q1\<rbrace> getCurThread \<lbrace>\<lambda>thread. ?P30 thread and (\<lambda>_. True)\<rbrace>
 3. \<And>s. ct_in_state' ((=) Structures_H.thread_state.Running) s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_in_state' ((=) Structures_H.thread_state.Running) s \<Longrightarrow> st_tcb_at' (\<lambda>rv. rv = Structures_H.thread_state.Running) (ksCurThread s) s proof (prove)
goal:
No subgoals!