theory IpcCancel_C

lemma tcbSchedDequeue_ccorres:
  "ccorres dc xfdc
           (valid_queues and valid_queues' and tcb_at' t and valid_objs')
           (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>)
           []
           (tcbSchedDequeue t)
           (Call tcbSchedDequeue_'proc)" apply (rule ccorres_guard_imp [OF tcbSchedDequeue_ccorres']) apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def) 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. ccorres dc xfdc (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs') (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>) [] (tcbSchedDequeue t) (Call tcbSchedDequeue_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>s. (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs') s \<Longrightarrow> ((\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p))) and valid_queues' and tcb_at' t and valid_objs') s
 2. \<And>s. s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> \<Longrightarrow> s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s d p ta. \<lbrakk>ta \<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; valid_queues' s; tcb_at' t s; valid_objs' s\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) ta s
 2. \<And>s. s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> \<Longrightarrow> s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s d p ta. \<lbrakk>ta \<in> set (ksReadyQueues s (d, p)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; valid_queues' s; tcb_at' t s; valid_objs' 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> obj_at' (inQ d p) ta s
 2. \<And>s. s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> \<Longrightarrow> s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s d p ta. \<lbrakk>ta \<in> set (ksReadyQueues s (d, p)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; valid_queues' s; tcb_at' t s; valid_objs' 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> obj_at' (inQ d p) ta s
 2. \<And>s. s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> \<Longrightarrow> s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s d p ta. \<lbrakk>ta \<in> set (ksReadyQueues s (d, p)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; valid_queues' s; tcb_at' t s; valid_objs' 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) ta s
 2. \<And>s. s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> \<Longrightarrow> s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s d p ta. \<lbrakk>ta \<in> set (ksReadyQueues s (d, p)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; valid_queues' s; tcb_at' t s; valid_objs' 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) ta s\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) ta s
 2. \<And>s. s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> \<Longrightarrow> s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s d p ta k. \<lbrakk>ta \<in> set (ksReadyQueues s (d, p)); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; valid_queues' s; tcb_at' t s; valid_objs' 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
 2. \<And>s. s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> \<Longrightarrow> s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace> proof (prove)
goal:
No subgoals!