theory IpcCancel_R

lemma tcbSchedEnqueue_valid_inQ_queues[wp]:
  "\<lbrace>valid_inQ_queues\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>" apply (simp add: tcbSchedEnqueue_def setQueue_after_addToBitmap) apply (rule hoare_pre) apply (rule_tac B="\<lambda>rv. valid_inQ_queues and obj_at' (\<lambda>obj. tcbQueued obj = rv) t"
                in hoare_seq_ext) apply (rename_tac queued) apply (case_tac queued, simp_all add: unless_def)[1] apply (wp setQueue_valid_inQ_queues threadSet_valid_inQ_queues threadGet_wp
               hoare_vcg_const_Ball_lift
          | simp add: inQ_def bitmap_fun_defs
          | fastforce simp: valid_inQ_queues_def inQ_def obj_at'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> do queued <- threadGet tcbQueued t;
unless queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- when (null queue) (addToBitmap tdom prio);
y <- threadSet (tcbQueued_update (\<lambda>_. True)) t;
setQueue tdom prio (t # queue)
od)
od \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do queued <- threadGet tcbQueued t;
unless queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- when (null queue) (addToBitmap tdom prio);
y <- threadSet (tcbQueued_update (\<lambda>_. True)) t;
setQueue tdom prio (t # queue)
od)
od \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>
 2. \<And>s. valid_inQ_queues s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>valid_inQ_queues and obj_at' (\<lambda>obj. tcbQueued obj = x) t\<rbrace> unless x (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- when (null queue) (addToBitmap tdom prio);
y <- threadSet (tcbQueued_update (\<lambda>_. True)) t;
setQueue tdom prio (t # queue)
od) \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>
 2. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_inQ_queues and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 3. \<And>s. valid_inQ_queues s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>queued. \<lbrace>valid_inQ_queues and obj_at' (\<lambda>obj. tcbQueued obj = queued) t\<rbrace> unless queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- when (null queue) (addToBitmap tdom prio);
y <- threadSet (tcbQueued_update (\<lambda>_. True)) t;
setQueue tdom prio (t # queue)
od) \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>
 2. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_inQ_queues and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 3. \<And>s. valid_inQ_queues s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>queued. queued \<Longrightarrow> \<lbrace>valid_inQ_queues and obj_at' tcbQueued t\<rbrace> return () \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>valid_inQ_queues and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t\<rbrace> do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- when (null queue) (addToBitmap tdom prio);
y <- threadSet (tcbQueued_update (\<lambda>_. True)) t;
setQueue tdom prio (t # queue)
od \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_inQ_queues and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 4. \<And>s. valid_inQ_queues s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!