theory IpcCancel_R

lemma setBoundNotification_oa_queued:
  "\<lbrace>\<lambda>s. P' (obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s) \<rbrace>
    setBoundNotification ntfn 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> setBoundNotification ntfn t \<lbrace>\<lambda>_. ?Q R \<rbrace>" apply (simp add: setBoundNotification_def) apply (wp threadSet_obj_at'_strongish) apply (clarsimp) done show "\<lbrace>\<lambda>s. \<not> ?Q P s\<rbrace> setBoundNotification ntfn 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> setBoundNotification ntfn 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> setBoundNotification ntfn 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> setBoundNotification ntfn 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> setBoundNotification ntfn 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> threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. R (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t'\<rbrace> 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 (tcbBoundNotification_update (\<lambda>_. ntfn) obj)) (tcbDomain (tcbBoundNotification_update (\<lambda>_. ntfn) obj)) (tcbPriority (tcbBoundNotification_update (\<lambda>_. ntfn) 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> setBoundNotification ntfn 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> setBoundNotification ntfn 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> setBoundNotification ntfn 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> setBoundNotification ntfn t \<lbrace>\<lambda>_ s. \<not> obj_at' (\<lambda>tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s\<rbrace>

goal:
No subgoals!