theory Schedule_R

lemma ksReadyQueuesL1Bitmap_st_tcb_at':
  "\<lbrakk> ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0 ; valid_queues s \<rbrakk>
   \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s" apply (drule bitmapQ_from_bitmap_lookup; clarsimp simp: valid_queues_def) apply (clarsimp simp add: valid_bitmapQ_bitmapQ_simp) apply (case_tac "ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)") apply simp apply (simp add: valid_queues_no_bitmap_def) apply (erule_tac x="ksCurDomain s" in allE) apply (erule_tac x="lookupBitmapPriority (ksCurDomain s) s" in allE) apply (clarsimp simp: st_tcb_at'_def) apply (erule obj_at'_weaken) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bitmapQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) \<noteq> []; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) \<noteq> []; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = []\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s
 2. \<And>a list. \<lbrakk>ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) \<noteq> []; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = a # list\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) \<noteq> []; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = a # list\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = a # list\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' a s proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = a # list; \<forall>p. (\<forall>t\<in>set (ksReadyQueues s (ksCurDomain s, p)). obj_at' (inQ (ksCurDomain s) p and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (ksCurDomain s, p)) \<and> (maxDomain < ksCurDomain s \<longrightarrow> ksReadyQueues s (ksCurDomain s, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (ksCurDomain s, p) = [])\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' a s proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = a # list; (\<forall>t\<in>set (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)). obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)) \<and> (maxDomain < ksCurDomain s \<longrightarrow> ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = []) \<and> (maxPriority < lookupBitmapPriority (ksCurDomain s) s \<longrightarrow> ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = [])\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' a s proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = a # list; obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState) a s; \<forall>t\<in>set list. obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState) t s; a \<notin> set list; distinct list; \<not> maxDomain < ksCurDomain s; \<not> maxPriority < lookupBitmapPriority (ksCurDomain s) s\<rbrakk> \<Longrightarrow> obj_at' (runnable' \<circ> tcbState) a s proof (prove)
goal (1 subgoal):
 1. \<And>a list obj. \<lbrakk>valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = a # list; \<forall>t\<in>set list. obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState) t s; a \<notin> set list; distinct list; \<not> maxDomain < ksCurDomain s; \<not> maxPriority < lookupBitmapPriority (ksCurDomain s) s; (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState) obj\<rbrakk> \<Longrightarrow> (runnable' \<circ> tcbState) obj proof (prove)
goal:
No subgoals!