theory Tcb_R

lemma setThreadState_runnable_simp:
  "runnable' ts \<Longrightarrow> setThreadState ts t =
   threadSet (tcbState_update (\<lambda>x. ts)) t" apply (simp add: setThreadState_def isRunnable_def isStopped_def liftM_def) apply (subst bind_return[symmetric], rule bind_cong[OF refl]) apply (drule use_valid[OF _ threadSet_pred_tcb_at_state[where proj="itcbState" and p=t and P="(=) ts"]]) apply simp apply (subst bind_known_operation_eq) apply wp+ apply clarsimp apply (subst eq_commute, erule conjI[OF _ refl]) apply (rule empty_fail_getThreadState) apply (simp add: getCurThread_def getSchedulerAction_def exec_gets) apply (auto simp: when_def split: Structures_H.thread_state.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. runnable' ts \<Longrightarrow> setThreadState ts t = threadSet (tcbState_update (\<lambda>x. ts)) t proof (prove)
goal (1 subgoal):
 1. runnable' ts \<Longrightarrow> do y <- threadSet (tcbState_update (\<lambda>_. ts)) t;
state <- getThreadState t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od = threadSet (tcbState_update (\<lambda>x. ts)) t proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. \<lbrakk>runnable' ts; (v, s') \<in> fst (threadSet (tcbState_update (\<lambda>_. ts)) t s)\<rbrakk> \<Longrightarrow> (do state <- getThreadState t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od) s' = return v s' proof (prove)
goal (2 subgoals):
 1. \<And>v s s'. runnable' ts \<Longrightarrow> tcb_at' t s \<longrightarrow> (if t = t then obj_at' (\<lambda>tcb. ts = itcbState (tcb_to_itcb' (tcbState_update (\<lambda>_. ts) tcb))) t s else st_tcb_at' ((=) ts) t s)
 2. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> (do state <- getThreadState t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od) s' = return v s' proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> (do state <- getThreadState t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od) s' = return v s' proof (prove)
goal (6 subgoals):
 1. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> no_fail (?P6 v s s') (getThreadState t)
 2. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 v s s'\<rbrace> getThreadState t \<lbrace>\<lambda>rv sa. rv = ?x6 v s s' \<and> sa = ?t6 v s s'\<rbrace>
 3. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> ?P6 v s s' s'
 4. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> ?Q6 v s s' s'
 5. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> empty_fail (getThreadState t)
 6. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> (do curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> (case ?x6 v s s' of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od) (?t6 v s s') = return v s' proof (prove)
goal (4 subgoals):
 1. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> tcb_at' t s'
 2. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>rv. rv = ?x13 v s s') t s' \<and> s' = ?t15 v s s'
 3. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> empty_fail (getThreadState t)
 4. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> (do curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> (case ?x13 v s s' of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od) (?t15 v s s') = return v s' proof (prove)
goal (3 subgoals):
 1. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>rv. rv = ?x13 v s s') t s' \<and> s' = ?t15 v s s'
 2. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> empty_fail (getThreadState t)
 3. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> (do curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> (case ?x13 v s s' of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od) (?t15 v s s') = return v s' proof (prove)
goal (2 subgoals):
 1. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> empty_fail (getThreadState t)
 2. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> (do curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> (case ts of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od) s' = return v s' proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> (do curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> (case ts of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od) s' = return v s' proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>runnable' ts; st_tcb_at' ((=) ts) t s'\<rbrakk> \<Longrightarrow> when (\<not> (case ts of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<and> ksCurThread s' = t \<and> ksSchedulerAction s' = ResumeCurrentThread) rescheduleRequired s' = return () s' proof (prove)
goal:
No subgoals!