theory Schedule_R

lemma tcbSchedEnqueue_in_ksQ:
  "\<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedEnqueue t
   \<lbrace>\<lambda>r s. \<exists>domain priority. t \<in> set (ksReadyQueues s (domain, priority))\<rbrace>" apply (rule_tac Q="\<lambda>s. \<exists>d p. valid_queues' s \<and>
                             obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and>
                             obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s"
           in hoare_pre_imp) apply (clarsimp simp: tcb_at'_has_tcbPriority tcb_at'_has_tcbDomain) apply (rule hoare_vcg_ex_lift)+ apply (simp add: tcbSchedEnqueue_def unless_def) apply (wpsimp simp: if_apply_def2) apply (rule_tac Q="\<lambda>rv s. tdom = d \<and> rv = p \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s
                             \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s"
              in hoare_post_imp, clarsimp) apply (wp, (wp threadGet_const)+) apply (rule_tac Q="\<lambda>rv s.
              obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and>
              obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<and>
              obj_at' (\<lambda>tcb. tcbQueued tcb = rv) t s \<and>
              (rv \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)))" in hoare_post_imp) apply (clarsimp simp: o_def elim!: obj_at'_weakenE) apply (wp threadGet_obj_at' hoare_vcg_imp_lift threadGet_const) apply clarsimp apply normalise_obj_at' apply (frule(1) valid_queues'_ko_atD, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>r s. \<exists>domain priority. t \<in> set (ksReadyQueues s (domain, priority))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> \<exists>d p. valid_queues' s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s
 2. \<lbrace>\<lambda>s. \<exists>d p. valid_queues' s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>r s. \<exists>domain priority. t \<in> set (ksReadyQueues s (domain, priority))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>d p. valid_queues' s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>r s. \<exists>domain priority. t \<in> set (ksReadyQueues s (domain, priority))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p. \<lbrace>\<lambda>s. valid_queues' s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>rv s. t \<in> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p. \<lbrace>\<lambda>s. valid_queues' s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s\<rbrace> do queued <- threadGet tcbQueued t;
when (\<not> queued) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
od \<lbrace>\<lambda>rv s. t \<in> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>d p queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B10 d p (ds_id False) tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>prio s. (d = tdom \<longrightarrow> p \<noteq> prio) \<longrightarrow> t \<in> set (ksReadyQueues s (d, p))\<rbrace>
 2. \<And>d p queued. \<not> queued \<Longrightarrow> \<lbrace>?Q9 d p queued\<rbrace> threadGet tcbDomain t \<lbrace>?B10 d p queued\<rbrace>
 3. \<And>d p. \<lbrace>?Q7 d p\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if \<not> queued then ?Q9 d p queued else (\<lambda>s. t \<in> set (ksReadyQueues s (d, p)))\<rbrace>
 4. \<And>d p s. valid_queues' s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<Longrightarrow> ?Q7 d p s proof (prove)
goal (4 subgoals):
 1. \<And>d p queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B10 d p (ds_id False) tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>rv s. tdom = d \<and> rv = p \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s\<rbrace>
 2. \<And>d p queued. \<not> queued \<Longrightarrow> \<lbrace>?Q9 d p queued\<rbrace> threadGet tcbDomain t \<lbrace>?B10 d p queued\<rbrace>
 3. \<And>d p. \<lbrace>?Q7 d p\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if \<not> queued then ?Q9 d p queued else (\<lambda>s. t \<in> set (ksReadyQueues s (d, p)))\<rbrace>
 4. \<And>d p s. valid_queues' s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<Longrightarrow> ?Q7 d p s proof (prove)
goal (2 subgoals):
 1. \<And>d p. \<lbrace>?Q7 d p\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if \<not> queued then \<lambda>s. (tcb_at' t s \<longrightarrow> obj_at' ((\<lambda>rv. rv = d) \<circ> tcbDomain) t s) \<and> (tcb_at' t s \<longrightarrow> obj_at' ((\<lambda>a. a = p) \<circ> tcbPriority) t s) \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s else (\<lambda>s. t \<in> set (ksReadyQueues s (d, p)))\<rbrace>
 2. \<And>d p s. valid_queues' s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<Longrightarrow> ?Q7 d p s proof (prove)
goal (3 subgoals):
 1. \<And>d p rv s. obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<and> obj_at' (\<lambda>tcb. tcbQueued tcb = rv) t s \<and> (rv \<longrightarrow> t \<in> set (ksReadyQueues s (d, p))) \<Longrightarrow> (if \<not> rv then \<lambda>s. (tcb_at' t s \<longrightarrow> obj_at' ((\<lambda>rv. rv = d) \<circ> tcbDomain) t s) \<and> (tcb_at' t s \<longrightarrow> obj_at' ((\<lambda>a. a = p) \<circ> tcbPriority) t s) \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s else (\<lambda>s. t \<in> set (ksReadyQueues s (d, p)))) s
 2. \<And>d p. \<lbrace>?Q7 d p\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<and> obj_at' (\<lambda>tcb. tcbQueued tcb = rv) t s \<and> (rv \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)))\<rbrace>
 3. \<And>d p s. valid_queues' s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<Longrightarrow> ?Q7 d p s proof (prove)
goal (2 subgoals):
 1. \<And>d p. \<lbrace>?Q7 d p\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<and> obj_at' (\<lambda>tcb. tcbQueued tcb = rv) t s \<and> (rv \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)))\<rbrace>
 2. \<And>d p s. valid_queues' s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<Longrightarrow> ?Q7 d p s proof (prove)
goal (1 subgoal):
 1. \<And>d p s. valid_queues' s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<Longrightarrow> obj_at' (\<lambda>t. tcbPriority t = p) t s \<and> obj_at' (\<lambda>t. tcbDomain t = d) t s \<and> obj_at' (\<lambda>t. tcbQueued t = tcbQueued t) t s \<and> ((tcb_at' t s \<longrightarrow> obj_at' (Not \<circ> tcbQueued) t s) \<or> t \<in> set (ksReadyQueues s (d, p))) proof (prove)
goal (1 subgoal):
 1. \<And>d p s. \<lbrakk>valid_queues' s; obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s; obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s\<rbrakk> \<Longrightarrow> tcb_at' t s \<and> (tcb_at' t s \<longrightarrow> obj_at' (Not \<circ> tcbQueued) t s \<or> t \<in> set (ksReadyQueues s (d, p))) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_queues' s; ko_at' ko t s; tcbQueued ko\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues s (tcbDomain ko, tcbPriority ko)) proof (prove)
goal:
No subgoals!