theory IpcCancel_R

lemma tcbSchedDequeue_t_notksQ:
  "\<lbrace>\<lambda>s. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow>
           obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t s\<rbrace>
    tcbSchedDequeue t
   \<lbrace>\<lambda>_ s. t \<notin> set (ksReadyQueues s (d, p))\<rbrace>" apply (rule_tac Q="(\<lambda>s. t \<notin> set (ksReadyQueues s (d, p)))
                            or obj_at'(\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t"
               in hoare_pre_imp, clarsimp) apply (rule hoare_pre_disj) apply (wp tcbSchedDequeue_notksQ)[1] apply (simp add: tcbSchedDequeue_def  removeFromBitmap_conceal_def[symmetric]) apply wp apply (rule hoare_pre_post, assumption) apply (clarsimp simp: bitmap_fun_defs removeFromBitmap_conceal_def, wp, clarsimp) apply (wp threadGet_wp)+ apply (auto simp: obj_at'_real_def ko_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t s\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. t \<notin> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. t \<notin> set (ksReadyQueues s (d, p))) or obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. t \<notin> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. t \<notin> set (ksReadyQueues s (d, p))\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. t \<notin> set (ksReadyQueues s (d, p))\<rbrace>
 2. \<lbrace>obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. t \<notin> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. t \<notin> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t\<rbrace> do queued <- threadGet tcbQueued t;
when queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- removeFromBitmap_conceal tdom prio queue t;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
od \<lbrace>\<lambda>_ s. t \<notin> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue y. queued \<Longrightarrow> \<lbrace>?B16 queued tdom prio queue y\<rbrace> removeFromBitmap_conceal tdom prio queue t \<lbrace>\<lambda>ya s. t \<notin> set (ksReadyQueues s (d, p))\<rbrace>
 2. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B15 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>?B16 queued tdom prio queue\<rbrace>
 3. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B14 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B15 queued tdom prio\<rbrace>
 4. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B13 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B14 queued tdom\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q12 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B13 queued\<rbrace>
 6. \<lbrace>?Q10\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q12 queued else (\<lambda>s. t \<notin> set (ksReadyQueues s (d, p)))\<rbrace>
 7. \<And>s. obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t s \<Longrightarrow> ?Q10 s proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue y. queued \<Longrightarrow> \<lbrace>\<lambda>s. t \<notin> set (ksReadyQueues s (d, p))\<rbrace> removeFromBitmap_conceal tdom prio queue t \<lbrace>\<lambda>ya s. t \<notin> set (ksReadyQueues s (d, p))\<rbrace>
 2. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B15 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>\<lambda>y s. t \<notin> set (ksReadyQueues s (d, p))\<rbrace>
 3. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B14 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B15 queued tdom prio\<rbrace>
 4. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B13 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B14 queued tdom\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q12 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B13 queued\<rbrace>
 6. \<lbrace>?Q10\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q12 queued else (\<lambda>s. t \<notin> set (ksReadyQueues s (d, p)))\<rbrace>
 7. \<And>s. obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t s \<Longrightarrow> ?Q10 s proof (prove)
goal (6 subgoals):
 1. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B15 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>\<lambda>y s. t \<notin> set (ksReadyQueues s (d, p))\<rbrace>
 2. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B14 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B15 queued tdom prio\<rbrace>
 3. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B13 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B14 queued tdom\<rbrace>
 4. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q12 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B13 queued\<rbrace>
 5. \<lbrace>?Q10\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q12 queued else (\<lambda>s. t \<notin> set (ksReadyQueues s (d, p)))\<rbrace>
 6. \<And>s. obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t s \<Longrightarrow> ?Q10 s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>tcb. ko_at' tcb t s \<and> (if tcbQueued tcb then \<lambda>s. tcb_at' t s \<longrightarrow> (\<exists>tcb. ko_at' tcb t s \<and> (tcb_at' t s \<longrightarrow> (\<exists>tcba. ko_at' tcba t s \<and> t \<notin> set (((ksReadyQueues s)((tcbDomain tcb, tcbPriority tcba) := filter (\<lambda>x. x \<noteq> t) (ksReadyQueues s (tcbDomain tcb, tcbPriority tcba)))) (d, p))))) else (\<lambda>s. t \<notin> set (ksReadyQueues s (d, p)))) s) proof (prove)
goal:
No subgoals!