theory Orphanage

lemma tcbSchedEnqueue_in_ksQ'':
  "\<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and>
    (t' \<noteq> t \<longrightarrow> (\<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority)))) \<rbrace>
   tcbSchedEnqueue t
   \<lbrace>\<lambda>r s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))\<rbrace>" apply (case_tac "t'=t", wpsimp wp: tcbSchedEnqueue_in_ksQ) apply clarsimp apply (wpsimp simp:  tcbSchedEnqueue_def unless_def) apply (rule_tac Q="\<lambda>_ s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))"
              in hoare_post_imp) apply metis apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and> (t' \<noteq> t \<longrightarrow> (\<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))))\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>r s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))\<rbrace> proof (prove)
goal (1 subgoal):
 1. t' \<noteq> t \<Longrightarrow> \<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and> (t' \<noteq> t \<longrightarrow> (\<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))))\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>r s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))\<rbrace> proof (prove)
goal (1 subgoal):
 1. t' \<noteq> t \<Longrightarrow> \<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and> (\<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority)))\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>r s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom. \<lbrakk>t' \<noteq> t; \<not> queued\<rbrakk> \<Longrightarrow> \<lbrace>?B10 (ds_id False) tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prio s. \<exists>domain priority. (domain = tdom \<and> priority = prio \<longrightarrow> t' \<in> set (ksReadyQueues s (tdom, prio))) \<and> ((domain = tdom \<longrightarrow> priority \<noteq> prio) \<longrightarrow> t' \<in> set (ksReadyQueues s (domain, priority)))\<rbrace>
 2. \<And>queued. \<lbrakk>t' \<noteq> t; \<not> queued\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B10 queued\<rbrace>
 3. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q7\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if \<not> queued then ?Q9 queued else (\<lambda>s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority)))\<rbrace>
 4. \<And>s. \<lbrakk>t' \<noteq> t; valid_queues' s \<and> tcb_at' t s \<and> (\<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority)))\<rbrakk> \<Longrightarrow> ?Q7 s proof (prove)
goal (5 subgoals):
 1. \<And>queued tdom rv s. \<lbrakk>t' \<noteq> t; \<not> queued; \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))\<rbrakk> \<Longrightarrow> \<exists>domain priority. (domain = tdom \<and> priority = rv \<longrightarrow> t' \<in> set (ksReadyQueues s (tdom, rv))) \<and> ((domain = tdom \<longrightarrow> priority \<noteq> rv) \<longrightarrow> t' \<in> set (ksReadyQueues s (domain, priority)))
 2. \<And>queued tdom. \<lbrakk>t' \<noteq> t; \<not> queued\<rbrakk> \<Longrightarrow> \<lbrace>?B10 (ds_id False) tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>_ s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))\<rbrace>
 3. \<And>queued. \<lbrakk>t' \<noteq> t; \<not> queued\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B10 queued\<rbrace>
 4. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q7\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if \<not> queued then ?Q9 queued else (\<lambda>s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority)))\<rbrace>
 5. \<And>s. \<lbrakk>t' \<noteq> t; valid_queues' s \<and> tcb_at' t s \<and> (\<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority)))\<rbrakk> \<Longrightarrow> ?Q7 s proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom. \<lbrakk>t' \<noteq> t; \<not> queued\<rbrakk> \<Longrightarrow> \<lbrace>?B10 (ds_id False) tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>_ s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))\<rbrace>
 2. \<And>queued. \<lbrakk>t' \<noteq> t; \<not> queued\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B10 queued\<rbrace>
 3. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q7\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if \<not> queued then ?Q9 queued else (\<lambda>s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority)))\<rbrace>
 4. \<And>s. \<lbrakk>t' \<noteq> t; valid_queues' s \<and> tcb_at' t s \<and> (\<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority)))\<rbrakk> \<Longrightarrow> ?Q7 s proof (prove)
goal:
No subgoals!