theory Orphanage

lemma tcbSchedDequeue_all_queued_tcb_ptrs:
  "\<lbrace>\<lambda>s. x \<in> all_queued_tcb_ptrs s \<and> x \<noteq> t \<rbrace>
   tcbSchedDequeue t \<lbrace>\<lambda>_ s. x \<in> all_queued_tcb_ptrs s\<rbrace>" apply (rule_tac Q="(\<lambda>s. x \<in> all_queued_tcb_ptrs s) and K (x \<noteq> t)"
           in hoare_pre_imp, clarsimp) apply (rule hoare_gen_asm) apply (clarsimp simp: tcbSchedDequeue_def all_queued_tcb_ptrs_def) apply (rule hoare_pre) apply (wp, clarsimp) apply (wp hoare_vcg_ex_lift)+ apply (rename_tac d p) apply (rule_tac Q="\<lambda>_ s. x \<in> set (ksReadyQueues s (d, p))"
                     in hoare_post_imp, clarsimp) apply (wp hoare_vcg_all_lift | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. x \<in> all_queued_tcb_ptrs s \<and> x \<noteq> t\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. x \<in> all_queued_tcb_ptrs s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. x \<in> all_queued_tcb_ptrs s) and K (x \<noteq> t)\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. x \<in> all_queued_tcb_ptrs s\<rbrace> proof (prove)
goal (1 subgoal):
 1. x \<noteq> t \<Longrightarrow> \<lbrace>\<lambda>s. x \<in> all_queued_tcb_ptrs s\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_ s. x \<in> all_queued_tcb_ptrs s\<rbrace> proof (prove)
goal (1 subgoal):
 1. x \<noteq> t \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>a b. x \<in> set (ksReadyQueues s (a, b))\<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 <- when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
od \<lbrace>\<lambda>_ s. \<exists>a b. x \<in> set (ksReadyQueues s (a, b))\<rbrace> proof (prove)
goal (2 subgoals):
 1. x \<noteq> t \<Longrightarrow> \<lbrace>?Q4\<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 <- when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
od \<lbrace>\<lambda>_ s. \<exists>a b. x \<in> set (ksReadyQueues s (a, b))\<rbrace>
 2. \<And>s. \<lbrakk>x \<noteq> t; \<exists>a b. x \<in> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (6 subgoals):
 1. \<And>queued tdom prio queue. \<lbrakk>x \<noteq> t; queued\<rbrakk> \<Longrightarrow> \<lbrace>?B12 True tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>\<lambda>y s. \<exists>a b. x \<in> set (ksReadyQueues s (a, b))\<rbrace>
 2. \<And>queued tdom prio. \<lbrakk>x \<noteq> t; queued\<rbrakk> \<Longrightarrow> \<lbrace>?B11 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B12 queued tdom prio\<rbrace>
 3. \<And>queued tdom. \<lbrakk>x \<noteq> t; queued\<rbrakk> \<Longrightarrow> \<lbrace>?B10 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B11 queued tdom\<rbrace>
 4. \<And>queued. \<lbrakk>x \<noteq> t; queued\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B10 queued\<rbrace>
 5. x \<noteq> t \<Longrightarrow> \<lbrace>?Q4\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q9 queued else (\<lambda>s. \<exists>a b. x \<in> set (ksReadyQueues s (a, b)))\<rbrace>
 6. \<And>s. \<lbrakk>x \<noteq> t; \<exists>a b. x \<in> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom xa xaa. \<lbrakk>x \<noteq> t; queued\<rbrakk> \<Longrightarrow> \<lbrace>?P45 queued tdom xa xaa\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>rv s. x \<in> set (((ksReadyQueues s)((tdom, rv) := filter (\<lambda>x. x \<noteq> t) (ksReadyQueues s (tdom, rv)))) (xa, xaa))\<rbrace>
 2. \<And>queued. \<lbrakk>x \<noteq> t; queued\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom s. \<exists>x xa. ?P45 queued tdom x xa s\<rbrace>
 3. x \<noteq> t \<Longrightarrow> \<lbrace>?Q4\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q9 queued else (\<lambda>s. \<exists>a b. x \<in> set (ksReadyQueues s (a, b)))\<rbrace>
 4. \<And>s. \<lbrakk>x \<noteq> t; \<exists>a b. x \<in> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom d p. \<lbrakk>x \<noteq> t; queued\<rbrakk> \<Longrightarrow> \<lbrace>?P45 queued tdom d p\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>rv s. x \<in> set (((ksReadyQueues s)((tdom, rv) := filter (\<lambda>x. x \<noteq> t) (ksReadyQueues s (tdom, rv)))) (d, p))\<rbrace>
 2. \<And>queued. \<lbrakk>x \<noteq> t; queued\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom s. \<exists>x xa. ?P45 queued tdom x xa s\<rbrace>
 3. x \<noteq> t \<Longrightarrow> \<lbrace>?Q4\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q9 queued else (\<lambda>s. \<exists>a b. x \<in> set (ksReadyQueues s (a, b)))\<rbrace>
 4. \<And>s. \<lbrakk>x \<noteq> t; \<exists>a b. x \<in> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom d p. \<lbrakk>x \<noteq> t; queued\<rbrakk> \<Longrightarrow> \<lbrace>?P45 queued tdom d p\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>_ s. x \<in> set (ksReadyQueues s (d, p))\<rbrace>
 2. \<And>queued. \<lbrakk>x \<noteq> t; queued\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom s. \<exists>x xa. ?P45 queued tdom x xa s\<rbrace>
 3. x \<noteq> t \<Longrightarrow> \<lbrace>?Q4\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q9 queued else (\<lambda>s. \<exists>a b. x \<in> set (ksReadyQueues s (a, b)))\<rbrace>
 4. \<And>s. \<lbrakk>x \<noteq> t; \<exists>a b. x \<in> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal:
No subgoals!