theory Invariants_H

lemma valid_queues_obj_at'D:
   "\<lbrakk> t \<in> set (ksReadyQueues s (d, p)); valid_queues s \<rbrakk>
        \<Longrightarrow> obj_at' (inQ d p) t s" apply (unfold valid_queues_def valid_queues_no_bitmap_def) apply (elim conjE) apply (drule_tac x=d in spec) apply (drule_tac x=p in spec) apply (clarsimp) apply (drule(1) bspec) apply (erule obj_at'_weakenE) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set (ksReadyQueues s (d, p)); valid_queues s\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set (ksReadyQueues s (d, p)); (\<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 \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set (ksReadyQueues s (d, p)); \<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 \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set (ksReadyQueues s (d, p)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; \<forall>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 \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set (ksReadyQueues s (d, p)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; (\<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 \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set (ksReadyQueues s (d, p)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; \<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s; distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set (ksReadyQueues s (d, p)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []; obj_at' (inQ d p and runnable' \<circ> tcbState) t s\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) t s proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>t \<in> set (ksReadyQueues s (d, p)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []; (inQ d p and runnable' \<circ> tcbState) k\<rbrakk> \<Longrightarrow> inQ d p k proof (prove)
goal:
No subgoals!