theory TcbAcc_R

lemma sts_iflive'[wp]:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s
      \<and> (st \<noteq> Inactive \<and> \<not> idle' st \<longrightarrow> ex_nonz_cap_to' t s)\<rbrace>
     setThreadState st t
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (simp add: setThreadState_def setQueue_def) apply (rule hoare_pre) apply (wp | simp)+ apply (rule_tac Q="\<lambda>rv. if_live_then_nonz_cap'" in hoare_post_imp) apply clarsimp apply (wp threadSet_iflive' | simp)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s)\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>
 2. \<And>s. if_live_then_nonz_cap' s \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>y s. (\<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> if_live_then_nonz_cap' s) \<and> ((ksCurThread s = t \<longrightarrow> st_tcb_at' runnable' t s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> if_live_then_nonz_cap' s)\<rbrace>
 2. \<And>s. if_live_then_nonz_cap' s \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. if_live_then_nonz_cap' s \<Longrightarrow> (\<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> if_live_then_nonz_cap' s) \<and> ((ksCurThread s = t \<longrightarrow> st_tcb_at' runnable' t s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> if_live_then_nonz_cap' s)
 2. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>
 3. \<And>s. if_live_then_nonz_cap' s \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>
 2. \<And>s. if_live_then_nonz_cap' s \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. if_live_then_nonz_cap' s \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s) \<Longrightarrow> ((\<exists>tcb. tcbBoundNotification tcb = None \<and> (\<exists>y. tcbBoundNotification tcb = Some y) \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. (tcbState tcb = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcb)) \<and> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued tcb \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) proof (prove)
goal:
No subgoals!