theory IpcCancel_R

lemma not_in_epQueue:
  assumes ko_at:  "ko_at' r ep_ptr s" and
          srefs:  "sym_refs (state_refs_of' s)" and
          nidle:  "r \<noteq> IdleEP" and
          st_act: "st_tcb_at' simple' t s"
  shows   "t \<notin> set (epQueue r)" proof assume t_epQ: "t \<in> set (epQueue r)" with ko_at nidle have "(t, EPRecv) \<in> state_refs_of' s ep_ptr
          \<or> (t, EPSend) \<in> state_refs_of' s ep_ptr" by - (drule ko_at_state_refs_ofD', case_tac r, (clarsimp)+) with ko_at srefs have "(ep_ptr, TCBBlockedRecv) \<in> state_refs_of' s t
           \<or> (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t" apply - apply (frule(1) sym_refs_ko_atD') apply (drule ko_at_state_refs_ofD') apply (case_tac r) apply (clarsimp simp: st_tcb_at_refs_of_rev'
               | drule(1) bspec | drule st_tcb_at_state_refs_ofD')+ done with ko_at have "st_tcb_at' (Not \<circ> simple') t s" apply - apply (erule disjE) apply (drule state_refs_of'_elemD) apply (simp add: st_tcb_at_refs_of_rev') apply (erule pred_tcb'_weakenE) apply (clarsimp) apply (drule state_refs_of'_elemD) apply (simp add: st_tcb_at_refs_of_rev') apply (erule pred_tcb'_weakenE) apply (clarsimp) done with st_act show False by (rule pred_tcb'_neq_contra) simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t \<notin> set (epQueue r) proof (state)
goal (1 subgoal):
 1. t \<in> set (epQueue r) \<Longrightarrow> False proof (state)
this:
t \<in> set (epQueue r)

goal (1 subgoal):
 1. t \<in> set (epQueue r) \<Longrightarrow> False proof (chain)
picking this:
ko_at' r ep_ptr s
r \<noteq> Structures_H.endpoint.IdleEP
t \<in> set (epQueue r) proof (prove)
using this:
ko_at' r ep_ptr s
r \<noteq> Structures_H.endpoint.IdleEP
t \<in> set (epQueue r)

goal (1 subgoal):
 1. (t, EPRecv) \<in> state_refs_of' s ep_ptr \<or> (t, EPSend) \<in> state_refs_of' s ep_ptr proof (state)
this:
(t, EPRecv) \<in> state_refs_of' s ep_ptr \<or> (t, EPSend) \<in> state_refs_of' s ep_ptr

goal (1 subgoal):
 1. t \<in> set (epQueue r) \<Longrightarrow> False proof (chain)
picking this:
ko_at' r ep_ptr s
sym_refs (state_refs_of' s)
(t, EPRecv) \<in> state_refs_of' s ep_ptr \<or> (t, EPSend) \<in> state_refs_of' s ep_ptr proof (prove)
using this:
ko_at' r ep_ptr s
sym_refs (state_refs_of' s)
(t, EPRecv) \<in> state_refs_of' s ep_ptr \<or> (t, EPSend) \<in> state_refs_of' s ep_ptr

goal (1 subgoal):
 1. (ep_ptr, TCBBlockedRecv) \<in> state_refs_of' s t \<or> (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' r ep_ptr s; sym_refs (state_refs_of' s); (t, EPRecv) \<in> state_refs_of' s ep_ptr \<or> (t, EPSend) \<in> state_refs_of' s ep_ptr\<rbrakk> \<Longrightarrow> (ep_ptr, TCBBlockedRecv) \<in> state_refs_of' s t \<or> (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' r ep_ptr s; sym_refs (state_refs_of' s); (t, EPRecv) \<in> state_refs_of' s ep_ptr \<or> (t, EPSend) \<in> state_refs_of' s ep_ptr; state_refs_of' s ep_ptr = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (ep_ptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> (ep_ptr, TCBBlockedRecv) \<in> state_refs_of' s t \<or> (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs (state_refs_of' s); (t, EPRecv) \<in> state_refs_of' s ep_ptr \<or> (t, EPSend) \<in> state_refs_of' s ep_ptr; state_refs_of' s ep_ptr = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (ep_ptr, symreftype tp) \<in> refs_of' ko) x s); state_refs_of' s ep_ptr = refs_of' (injectKO r)\<rbrakk> \<Longrightarrow> (ep_ptr, TCBBlockedRecv) \<in> state_refs_of' s t \<or> (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>sym_refs (state_refs_of' s); (t, EPRecv) \<in> state_refs_of' s ep_ptr \<or> (t, EPSend) \<in> state_refs_of' s ep_ptr; state_refs_of' s ep_ptr = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (ep_ptr, symreftype tp) \<in> refs_of' ko) x s); state_refs_of' s ep_ptr = refs_of' (injectKO r); r = Structures_H.endpoint.RecvEP x1\<rbrakk> \<Longrightarrow> (ep_ptr, TCBBlockedRecv) \<in> state_refs_of' s t \<or> (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t
 2. \<lbrakk>sym_refs (state_refs_of' s); (t, EPRecv) \<in> state_refs_of' s ep_ptr \<or> (t, EPSend) \<in> state_refs_of' s ep_ptr; state_refs_of' s ep_ptr = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (ep_ptr, symreftype tp) \<in> refs_of' ko) x s); state_refs_of' s ep_ptr = refs_of' (injectKO r); r = Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> (ep_ptr, TCBBlockedRecv) \<in> state_refs_of' s t \<or> (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t
 3. \<And>x3. \<lbrakk>sym_refs (state_refs_of' s); (t, EPRecv) \<in> state_refs_of' s ep_ptr \<or> (t, EPSend) \<in> state_refs_of' s ep_ptr; state_refs_of' s ep_ptr = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (ep_ptr, symreftype tp) \<in> refs_of' ko) x s); state_refs_of' s ep_ptr = refs_of' (injectKO r); r = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> (ep_ptr, TCBBlockedRecv) \<in> state_refs_of' s t \<or> (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t proof (prove)
goal:
No subgoals! proof (state)
this:
(ep_ptr, TCBBlockedRecv) \<in> state_refs_of' s t \<or> (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t

goal (1 subgoal):
 1. t \<in> set (epQueue r) \<Longrightarrow> False proof (chain)
picking this:
ko_at' r ep_ptr s
(ep_ptr, TCBBlockedRecv) \<in> state_refs_of' s t \<or> (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t proof (prove)
using this:
ko_at' r ep_ptr s
(ep_ptr, TCBBlockedRecv) \<in> state_refs_of' s t \<or> (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t

goal (1 subgoal):
 1. st_tcb_at' (Not \<circ> simple') t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' r ep_ptr s; (ep_ptr, TCBBlockedRecv) \<in> state_refs_of' s t \<or> (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> simple') t s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko_at' r ep_ptr s; (ep_ptr, TCBBlockedRecv) \<in> state_refs_of' s t\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> simple') t s
 2. \<lbrakk>ko_at' r ep_ptr s; (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> simple') t s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko_at' r ep_ptr s; ko_wp_at' (\<lambda>obj. (ep_ptr, TCBBlockedRecv) \<in> refs_of' obj) t s\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> simple') t s
 2. \<lbrakk>ko_at' r ep_ptr s; (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> simple') t s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko_at' r ep_ptr s; st_tcb_at' (\<lambda>ts. \<exists>a. ts = Structures_H.thread_state.BlockedOnReceive ep_ptr a) t s\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> simple') t s
 2. \<lbrakk>ko_at' r ep_ptr s; (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> simple') t s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrakk>ko_at' r ep_ptr s; \<exists>a. st = Structures_H.thread_state.BlockedOnReceive ep_ptr a\<rbrakk> \<Longrightarrow> (Not \<circ> simple') st
 2. \<lbrakk>ko_at' r ep_ptr s; (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> simple') t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' r ep_ptr s; (ep_ptr, TCBBlockedSend) \<in> state_refs_of' s t\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> simple') t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' r ep_ptr s; ko_wp_at' (\<lambda>obj. (ep_ptr, TCBBlockedSend) \<in> refs_of' obj) t s\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> simple') t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' r ep_ptr s; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend ep_ptr a b c d) t s\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> simple') t s proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>ko_at' r ep_ptr s; \<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend ep_ptr a b c d\<rbrakk> \<Longrightarrow> (Not \<circ> simple') st proof (prove)
goal:
No subgoals! proof (state)
this:
st_tcb_at' (Not \<circ> simple') t s

goal (1 subgoal):
 1. t \<in> set (epQueue r) \<Longrightarrow> False proof (chain)
picking this:
st_tcb_at' simple' t s
st_tcb_at' (Not \<circ> simple') t s proof (prove)
using this:
st_tcb_at' simple' t s
st_tcb_at' (Not \<circ> simple') t s

goal (1 subgoal):
 1. False proof (state)
this:
False

goal:
No subgoals!