theory IpcCancel_R

lemma valid_queues_not_runnable'_not_ksQ:
  assumes "Invariants_H.valid_queues s" and "st_tcb_at' (Not \<circ> runnable') t s"
  shows   "\<forall>d p. t \<notin> set (ksReadyQueues s (d, p))" using assms apply - apply (clarsimp simp: Invariants_H.valid_queues_def valid_queues_no_bitmap_def pred_tcb_at'_def) apply (erule_tac x=d in allE) apply (erule_tac x=p in allE) apply (clarsimp) apply (drule(1) bspec) apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>d p. t \<notin> set (ksReadyQueues s (d, p)) proof (prove)
using this:
Invariants_H.valid_queues s
st_tcb_at' (Not \<circ> runnable') t s

goal (1 subgoal):
 1. \<forall>d p. t \<notin> set (ksReadyQueues s (d, p)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Invariants_H.valid_queues s; st_tcb_at' (Not \<circ> runnable') t s\<rbrakk> \<Longrightarrow> \<forall>d p. t \<notin> set (ksReadyQueues s (d, p)) proof (prove)
goal (1 subgoal):
 1. \<And>d p. \<lbrakk>obj_at' (\<lambda>ko. \<not> runnable' (tcbState ko)) t s; \<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; t \<in> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>d p. \<lbrakk>obj_at' (\<lambda>ko. \<not> runnable' (tcbState ko)) t s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; t \<in> set (ksReadyQueues s (d, p)); \<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 \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>d p. \<lbrakk>obj_at' (\<lambda>ko. \<not> runnable' (tcbState ko)) t s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; t \<in> set (ksReadyQueues s (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) = [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>d p. \<lbrakk>obj_at' (\<lambda>ko. \<not> runnable' (tcbState ko)) t s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; t \<in> set (ksReadyQueues s (d, p)); \<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> False proof (prove)
goal (1 subgoal):
 1. \<And>d p. \<lbrakk>obj_at' (\<lambda>ko. \<not> runnable' (tcbState ko)) t s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; t \<in> set (ksReadyQueues s (d, p)); 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> False proof (prove)
goal:
No subgoals!