theory IpcCancel_R

lemma tcbSchedDequeue_notksQ:
  "\<lbrace>\<lambda>s. t' \<notin> set(ksReadyQueues s p)\<rbrace>
    tcbSchedDequeue t
   \<lbrace>\<lambda>_ s. t' \<notin> set(ksReadyQueues s p)\<rbrace>" 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+ apply clarsimp apply (rule_tac Q="\<lambda>_ s. t' \<notin> set(ksReadyQueues s p)" in hoare_post_imp) apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t' \<notin> set (ksReadyQueues s p)\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. t' \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t' \<notin> set (ksReadyQueues s p)\<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 p)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue y. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue y\<rbrace> removeFromBitmap_conceal tdom prio queue t \<lbrace>\<lambda>ya s. t' \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>?B6 queued tdom prio queue\<rbrace>
 3. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B4 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B5 queued tdom prio\<rbrace>
 4. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B3 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B4 queued tdom\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q2 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B3 queued\<rbrace>
 6. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q2 queued else (\<lambda>s. t' \<notin> set (ksReadyQueues s p))\<rbrace>
 7. \<And>s. t' \<notin> set (ksReadyQueues s p) \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue y. queued \<Longrightarrow> \<lbrace>\<lambda>s. t' \<notin> set (ksReadyQueues s p)\<rbrace> removeFromBitmap_conceal tdom prio queue t \<lbrace>\<lambda>ya s. t' \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>\<lambda>y s. t' \<notin> set (ksReadyQueues s p)\<rbrace>
 3. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B4 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B5 queued tdom prio\<rbrace>
 4. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B3 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B4 queued tdom\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q2 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B3 queued\<rbrace>
 6. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q2 queued else (\<lambda>s. t' \<notin> set (ksReadyQueues s p))\<rbrace>
 7. \<And>s. t' \<notin> set (ksReadyQueues s p) \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>\<lambda>y s. t' \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B4 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B5 queued tdom prio\<rbrace>
 3. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B3 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B4 queued tdom\<rbrace>
 4. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q2 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B3 queued\<rbrace>
 5. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q2 queued else (\<lambda>s. t' \<notin> set (ksReadyQueues s p))\<rbrace>
 6. \<And>s. t' \<notin> set (ksReadyQueues s p) \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B3 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prio s. t' \<notin> set (((ksReadyQueues s)((tdom, prio) := filter (\<lambda>x. x \<noteq> t) (ksReadyQueues s (tdom, prio)))) p)\<rbrace>
 2. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q2 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B3 queued\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q2 queued else (\<lambda>s. t' \<notin> set (ksReadyQueues s p))\<rbrace>
 4. \<And>s. t' \<notin> set (ksReadyQueues s p) \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B3 True tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prio s. (p = (tdom, prio) \<longrightarrow> t' \<in> set (ksReadyQueues s (tdom, prio)) \<longrightarrow> t' = t) \<and> (p \<noteq> (tdom, prio) \<longrightarrow> t' \<notin> set (ksReadyQueues s p))\<rbrace>
 2. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q2 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B3 queued\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q2 queued else (\<lambda>s. t' \<notin> set (ksReadyQueues s p))\<rbrace>
 4. \<And>s. t' \<notin> set (ksReadyQueues s p) \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>queued tdom rv s. \<lbrakk>queued; t' \<notin> set (ksReadyQueues s p)\<rbrakk> \<Longrightarrow> (p = (tdom, rv) \<longrightarrow> t' \<in> set (ksReadyQueues s (tdom, rv)) \<longrightarrow> t' = t) \<and> (p \<noteq> (tdom, rv) \<longrightarrow> t' \<notin> set (ksReadyQueues s p))
 2. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B3 True tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>_ s. t' \<notin> set (ksReadyQueues s p)\<rbrace>
 3. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q2 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B3 queued\<rbrace>
 4. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q2 queued else (\<lambda>s. t' \<notin> set (ksReadyQueues s p))\<rbrace>
 5. \<And>s. t' \<notin> set (ksReadyQueues s p) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!