theory Schedule_R

lemma valid_queues_not_runnable_not_queued:
  fixes s
  assumes vq:  "Invariants_H.valid_queues s"
      and vq': "valid_queues' s"
      and st: "st_tcb_at' (Not \<circ> runnable') t s"
  shows "obj_at' (Not \<circ> tcbQueued) t s" proof (rule ccontr) assume "\<not> obj_at' (Not \<circ> tcbQueued) t s" moreover from st have "typ_at' TCBT t s" by (rule pred_tcb_at' [THEN tcb_at_typ_at' [THEN iffD1]]) ultimately have "obj_at' tcbQueued t s" by (clarsimp simp: not_obj_at' comp_def) moreover from st [THEN pred_tcb_at', THEN tcb_at'_has_tcbPriority] obtain p where tp: "obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s" by clarsimp moreover from st [THEN pred_tcb_at', THEN tcb_at'_has_tcbDomain] obtain d where td: "obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s" by clarsimp ultimately have "t \<in> set (ksReadyQueues s (d, p))" using vq' unfolding valid_queues'_def apply - apply (drule_tac x=d in spec) apply (drule_tac x=p in spec) apply (drule_tac x=t in spec) apply (erule impE) apply (fastforce simp add: inQ_def obj_at'_def) apply (assumption) done with vq have "st_tcb_at' runnable' t s" unfolding Invariants_H.valid_queues_def valid_queues_no_bitmap_def apply - apply clarsimp apply (drule_tac x=d in spec) apply (drule_tac x=p in spec) apply (clarsimp simp add: st_tcb_at'_def) apply (drule(1) bspec) apply (erule obj_at'_weakenE) apply (clarsimp) done with st show False apply - apply (drule(1) pred_tcb_at_conj') apply (clarsimp) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' (Not \<circ> tcbQueued) t s proof (state)
goal (1 subgoal):
 1. \<not> obj_at' (Not \<circ> tcbQueued) t s \<Longrightarrow> False proof (state)
this:
\<not> obj_at' (Not \<circ> tcbQueued) t s

goal (1 subgoal):
 1. \<not> obj_at' (Not \<circ> tcbQueued) t s \<Longrightarrow> False proof (state)
this:
\<not> obj_at' (Not \<circ> tcbQueued) t s

goal (1 subgoal):
 1. \<not> obj_at' (Not \<circ> tcbQueued) t s \<Longrightarrow> False proof (chain)
picking this:
st_tcb_at' (Not \<circ> runnable') t s proof (prove)
using this:
st_tcb_at' (Not \<circ> runnable') t s

goal (1 subgoal):
 1. typ_at' TCBT t s proof (state)
this:
typ_at' TCBT t s

goal (1 subgoal):
 1. \<not> obj_at' (Not \<circ> tcbQueued) t s \<Longrightarrow> False proof (chain)
picking this:
\<not> obj_at' (Not \<circ> tcbQueued) t s
typ_at' TCBT t s proof (prove)
using this:
\<not> obj_at' (Not \<circ> tcbQueued) t s
typ_at' TCBT t s

goal (1 subgoal):
 1. obj_at' tcbQueued t s proof (state)
this:
obj_at' tcbQueued t s

goal (1 subgoal):
 1. \<not> obj_at' (Not \<circ> tcbQueued) t s \<Longrightarrow> False proof (state)
this:
obj_at' tcbQueued t s

goal (1 subgoal):
 1. \<not> obj_at' (Not \<circ> tcbQueued) t s \<Longrightarrow> False proof (chain)
picking this:
\<exists>p. obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s proof (prove)
using this:
\<exists>p. obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s

goal (1 subgoal):
 1. (\<And>p. obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s

goal (1 subgoal):
 1. \<not> obj_at' (Not \<circ> tcbQueued) t s \<Longrightarrow> False proof (state)
this:
obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s

goal (1 subgoal):
 1. \<not> obj_at' (Not \<circ> tcbQueued) t s \<Longrightarrow> False proof (chain)
picking this:
\<exists>p. obj_at' (\<lambda>tcb. tcbDomain tcb = p) t s proof (prove)
using this:
\<exists>p. obj_at' (\<lambda>tcb. tcbDomain tcb = p) t s

goal (1 subgoal):
 1. (\<And>d. obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s

goal (1 subgoal):
 1. \<not> obj_at' (Not \<circ> tcbQueued) t s \<Longrightarrow> False proof (chain)
picking this:
obj_at' tcbQueued t s
obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s
obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s proof (prove)
using this:
obj_at' tcbQueued t s
obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s
obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s

goal (1 subgoal):
 1. t \<in> set (ksReadyQueues s (d, p)) proof (prove)
using this:
obj_at' tcbQueued t s
obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s
obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s
valid_queues' s

goal (1 subgoal):
 1. t \<in> set (ksReadyQueues s (d, p)) proof (prove)
using this:
obj_at' tcbQueued t s
obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s
obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s
\<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p))

goal (1 subgoal):
 1. t \<in> set (ksReadyQueues s (d, p)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' tcbQueued t s; obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s; obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s; \<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues s (d, p)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' tcbQueued t s; obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s; obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s; \<forall>p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues s (d, p)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' tcbQueued t s; obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s; obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s; \<forall>t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues s (d, p)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' tcbQueued t s; obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s; obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s; obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues s (d, p)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>obj_at' tcbQueued t s; obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s; obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) t s
 2. \<lbrakk>obj_at' tcbQueued t s; obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s; obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s; t \<in> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues s (d, p)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' tcbQueued t s; obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s; obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s; t \<in> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues s (d, p)) proof (prove)
goal:
No subgoals! proof (state)
this:
t \<in> set (ksReadyQueues s (d, p))

goal (1 subgoal):
 1. \<not> obj_at' (Not \<circ> tcbQueued) t s \<Longrightarrow> False proof (chain)
picking this:
Invariants_H.valid_queues s
t \<in> set (ksReadyQueues s (d, p)) proof (prove)
using this:
Invariants_H.valid_queues s
t \<in> set (ksReadyQueues s (d, p))

goal (1 subgoal):
 1. st_tcb_at' runnable' t s proof (prove)
using this:
(\<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
t \<in> set (ksReadyQueues s (d, p))

goal (1 subgoal):
 1. st_tcb_at' runnable' t s proof (prove)
goal (1 subgoal):
 1. \<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 \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s; t \<in> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' 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 \<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\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' 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 \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' 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 \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' 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' (runnable' \<circ> tcbState) 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' (runnable' \<circ> tcbState) 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> (runnable' \<circ> tcbState) k proof (prove)
goal:
No subgoals! proof (state)
this:
st_tcb_at' runnable' t s

goal (1 subgoal):
 1. \<not> obj_at' (Not \<circ> tcbQueued) t s \<Longrightarrow> False proof (chain)
picking this:
st_tcb_at' (Not \<circ> runnable') t s
st_tcb_at' runnable' t s proof (prove)
using this:
st_tcb_at' (Not \<circ> runnable') t s
st_tcb_at' runnable' t s

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' (Not \<circ> runnable') t s; st_tcb_at' runnable' t s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' runnable' t s; st_tcb_at' (\<lambda>a. (Not \<circ> runnable') a \<and> runnable' a) t s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
False

goal:
No subgoals!