theory IpcCancel_R

lemma setThreadState_oa_queued:
  "\<lbrace>\<lambda>s. P' (obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s) \<rbrace>
    setThreadState st t
   \<lbrace>\<lambda>_ s. P' (obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s) \<rbrace>"
  (is "\<lbrace>\<lambda>s. P' (?Q P s)\<rbrace> _ \<lbrace>\<lambda>_ s. P' (?Q P s)\<rbrace>") proof (rule P_bool_lift [where P=P']) show pos:
      "\<And>R. \<lbrace> ?Q R \<rbrace> setThreadState st t \<lbrace>\<lambda>_. ?Q R \<rbrace>" apply (simp add: setThreadState_def) apply (wp rescheduleRequired_oa_queued) apply (simp add: sch_act_simple_def) apply (rule_tac Q="\<lambda>_. ?Q R" in hoare_post_imp, clarsimp) apply (wp threadSet_obj_at'_strongish) apply (clarsimp) done show "\<lbrace>\<lambda>s. \<not> ?Q P s\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. \<not> ?Q P s\<rbrace>" by (simp add: not_obj_at' comp_def, wp hoare_convert_imp pos) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s)\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. P' (obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s)\<rbrace> proof (state)
goal (2 subgoals):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t'\<rbrace> setThreadState st t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t'\<rbrace>
 2. \<lbrace>\<lambda>s. \<not> obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. \<not> obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>R. \<lbrace>obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t'\<rbrace> setThreadState st t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>R. \<lbrace>obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t'\<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>_. obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>R. \<lbrace>?Q R\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>y s. (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' and sch_act_simple else obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t') s\<rbrace>
 2. \<And>R s. obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s \<Longrightarrow> ?Q R s proof (prove)
goal (2 subgoals):
 1. \<And>R. \<lbrace>?Q R\<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> obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s) \<and> ((ksCurThread s = t \<longrightarrow> st_tcb_at' runnable' t s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s)\<rbrace>
 2. \<And>R s. obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s \<Longrightarrow> ?Q R s proof (prove)
goal (2 subgoals):
 1. \<And>R. \<lbrace>?Q R\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t'\<rbrace>
 2. \<And>R s. obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s \<Longrightarrow> ?Q R s proof (prove)
goal (1 subgoal):
 1. \<And>R s. obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s \<Longrightarrow> obj_at' (\<lambda>obj. if t = t' then R (tcbQueued (tcbState_update (\<lambda>_. st) obj)) (tcbDomain (tcbState_update (\<lambda>_. st) obj)) (tcbPriority (tcbState_update (\<lambda>_. st) obj)) else R (tcbQueued obj) (tcbDomain obj) (tcbPriority obj)) t' s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>obj_at' (\<lambda>tcb. ?R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t'\<rbrace> setThreadState st t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. ?R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t'\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. \<not> obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. \<not> obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s\<rbrace> proof (state)
this:
\<lbrace>\<lambda>s. \<not> obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. \<not> obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s\<rbrace>

goal:
No subgoals!