theory Schedule_R

lemma switchToThread_lookupBitmapPriority_wp:
  "\<lbrace>\<lambda>s. invs_no_cicd' s \<and> bitmapQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) s \<and>
        t = hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)) \<rbrace>
   ThreadDecls_H.switchToThread t
   \<lbrace>\<lambda>rv. invs'\<rbrace>" proof - have switchToThread_pre:
    "\<And>s p t.\<lbrakk> valid_queues s ; bitmapQ (ksCurDomain s) p s ; t = hd (ksReadyQueues s (ksCurDomain s,p)) \<rbrakk>
            \<Longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s" unfolding valid_queues_def apply (clarsimp dest!: bitmapQ_ksReadyQueuesI) apply (case_tac "ksReadyQueues s (ksCurDomain s, p)", simp) apply (rename_tac t ts) apply (drule_tac t=t and p=p and d="ksCurDomain s" in valid_queues_no_bitmap_objD) apply simp apply (fastforce elim: obj_at'_weaken simp: inQ_def tcb_in_cur_domain'_def st_tcb_at'_def) done thus ?thesis by (wp switchToThread_invs_no_cicd') (fastforce dest: invs_no_cicd'_queues) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> bitmapQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) s \<and> t = hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))\<rbrace> global.switchToThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> bitmapQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) s \<and> t = hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))\<rbrace> global.switchToThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s p t. \<lbrakk>Invariants_H.valid_queues s; bitmapQ (ksCurDomain s) p s; t = hd (ksReadyQueues s (ksCurDomain s, p))\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s proof (prove)
goal (1 subgoal):
 1. \<And>s p t. \<lbrakk>valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s; bitmapQ (ksCurDomain s) p s; t = hd (ksReadyQueues s (ksCurDomain s, p))\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s proof (prove)
goal (1 subgoal):
 1. \<And>s p. \<lbrakk>valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, p) \<noteq> []\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, p))) s \<and> tcb_in_cur_domain' (hd (ksReadyQueues s (ksCurDomain s, p))) s proof (prove)
goal (1 subgoal):
 1. \<And>s p a list. \<lbrakk>valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, p) \<noteq> []; ksReadyQueues s (ksCurDomain s, p) = a # list\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, p))) s \<and> tcb_in_cur_domain' (hd (ksReadyQueues s (ksCurDomain s, p))) s proof (prove)
goal (1 subgoal):
 1. \<And>s p t ts. \<lbrakk>valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, p) \<noteq> []; ksReadyQueues s (ksCurDomain s, p) = t # ts\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, p))) s \<and> tcb_in_cur_domain' (hd (ksReadyQueues s (ksCurDomain s, p))) s proof (prove)
goal (2 subgoals):
 1. \<And>s p t ts. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, p) \<noteq> []; ksReadyQueues s (ksCurDomain s, p) = t # ts\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues s (ksCurDomain s, p))
 2. \<And>s p t ts. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, p) \<noteq> []; ksReadyQueues s (ksCurDomain s, p) = t # ts; obj_at' (inQ (ksCurDomain s) p and runnable' \<circ> tcbState) t s\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, p))) s \<and> tcb_in_cur_domain' (hd (ksReadyQueues s (ksCurDomain s, p))) s proof (prove)
goal (1 subgoal):
 1. \<And>s p t ts. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, p) \<noteq> []; ksReadyQueues s (ksCurDomain s, p) = t # ts; obj_at' (inQ (ksCurDomain s) p and runnable' \<circ> tcbState) t s\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, p))) s \<and> tcb_in_cur_domain' (hd (ksReadyQueues s (ksCurDomain s, p))) s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>Invariants_H.valid_queues ?s; bitmapQ (ksCurDomain ?s) ?p ?s; ?t = hd (ksReadyQueues ?s (ksCurDomain ?s, ?p))\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' ?t ?s \<and> tcb_in_cur_domain' ?t ?s

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> bitmapQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) s \<and> t = hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))\<rbrace> global.switchToThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
using this:
\<lbrakk>Invariants_H.valid_queues ?s; bitmapQ (ksCurDomain ?s) ?p ?s; ?t = hd (ksReadyQueues ?s (ksCurDomain ?s, ?p))\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' ?t ?s \<and> tcb_in_cur_domain' ?t ?s

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> bitmapQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) s \<and> t = hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))\<rbrace> global.switchToThread t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (state)
this:
\<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> bitmapQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) s \<and> t = hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))\<rbrace> global.switchToThread t \<lbrace>\<lambda>rv. invs'\<rbrace>

goal:
No subgoals!