theory IpcCancel_R

lemma not_in_ntfnQueue:
  assumes ko_at:  "ko_at' r ntfn_ptr s" and
          srefs:  "sym_refs (state_refs_of' s)" and
          nidle:  "ntfnObj r \<noteq> IdleNtfn \<and> (\<forall>b m. ntfnObj r \<noteq> ActiveNtfn b)" and
          st_act: "st_tcb_at' simple' t s"
  shows   "t \<notin> set (ntfnQueue (ntfnObj r))" proof assume t_epQ: "t \<in> set (ntfnQueue (ntfnObj r))" with ko_at nidle have "(t, NTFNSignal) \<in> state_refs_of' s ntfn_ptr" by - (drule ko_at_state_refs_ofD', case_tac "ntfnObj r", (clarsimp)+) with ko_at srefs have "(ntfn_ptr, TCBSignal) \<in> state_refs_of' s t" apply - apply (frule(1) sym_refs_ko_atD') apply (drule ko_at_state_refs_ofD') apply (case_tac "ntfnObj r") apply (clarsimp simp: st_tcb_at_refs_of_rev' ntfn_bound_refs'_def
             | drule st_tcb_at_state_refs_ofD')+ apply (drule_tac x="(t, NTFNSignal)" in bspec, clarsimp) apply (clarsimp simp: st_tcb_at_refs_of_rev' dest!: st_tcb_at_state_refs_ofD') done with ko_at have "st_tcb_at' (Not \<circ> simple') t s" apply - 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 (ntfnQueue (ntfnObj r)) proof (state)
goal (1 subgoal):
 1. t \<in> set (ntfnQueue (ntfnObj r)) \<Longrightarrow> False proof (state)
this:
t \<in> set (ntfnQueue (ntfnObj r))

goal (1 subgoal):
 1. t \<in> set (ntfnQueue (ntfnObj r)) \<Longrightarrow> False proof (chain)
picking this:
ko_at' r ntfn_ptr s
ntfnObj r \<noteq> Structures_H.ntfn.IdleNtfn \<and> (\<forall>b m. ntfnObj r \<noteq> Structures_H.ntfn.ActiveNtfn b)
t \<in> set (ntfnQueue (ntfnObj r)) proof (prove)
using this:
ko_at' r ntfn_ptr s
ntfnObj r \<noteq> Structures_H.ntfn.IdleNtfn \<and> (\<forall>b m. ntfnObj r \<noteq> Structures_H.ntfn.ActiveNtfn b)
t \<in> set (ntfnQueue (ntfnObj r))

goal (1 subgoal):
 1. (t, NTFNSignal) \<in> state_refs_of' s ntfn_ptr proof (state)
this:
(t, NTFNSignal) \<in> state_refs_of' s ntfn_ptr

goal (1 subgoal):
 1. t \<in> set (ntfnQueue (ntfnObj r)) \<Longrightarrow> False proof (chain)
picking this:
ko_at' r ntfn_ptr s
sym_refs (state_refs_of' s)
(t, NTFNSignal) \<in> state_refs_of' s ntfn_ptr proof (prove)
using this:
ko_at' r ntfn_ptr s
sym_refs (state_refs_of' s)
(t, NTFNSignal) \<in> state_refs_of' s ntfn_ptr

goal (1 subgoal):
 1. (ntfn_ptr, TCBSignal) \<in> state_refs_of' s t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' r ntfn_ptr s; sym_refs (state_refs_of' s); (t, NTFNSignal) \<in> state_refs_of' s ntfn_ptr\<rbrakk> \<Longrightarrow> (ntfn_ptr, TCBSignal) \<in> state_refs_of' s t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' r ntfn_ptr s; sym_refs (state_refs_of' s); (t, NTFNSignal) \<in> state_refs_of' s ntfn_ptr; state_refs_of' s ntfn_ptr = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (ntfn_ptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> (ntfn_ptr, TCBSignal) \<in> state_refs_of' s t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs (state_refs_of' s); (t, NTFNSignal) \<in> state_refs_of' s ntfn_ptr; state_refs_of' s ntfn_ptr = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (ntfn_ptr, symreftype tp) \<in> refs_of' ko) x s); state_refs_of' s ntfn_ptr = refs_of' (injectKO r)\<rbrakk> \<Longrightarrow> (ntfn_ptr, TCBSignal) \<in> state_refs_of' s t proof (prove)
goal (3 subgoals):
 1. \<lbrakk>sym_refs (state_refs_of' s); (t, NTFNSignal) \<in> state_refs_of' s ntfn_ptr; state_refs_of' s ntfn_ptr = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (ntfn_ptr, symreftype tp) \<in> refs_of' ko) x s); state_refs_of' s ntfn_ptr = refs_of' (injectKO r); ntfnObj r = Structures_H.ntfn.IdleNtfn\<rbrakk> \<Longrightarrow> (ntfn_ptr, TCBSignal) \<in> state_refs_of' s t
 2. \<And>x2. \<lbrakk>sym_refs (state_refs_of' s); (t, NTFNSignal) \<in> state_refs_of' s ntfn_ptr; state_refs_of' s ntfn_ptr = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (ntfn_ptr, symreftype tp) \<in> refs_of' ko) x s); state_refs_of' s ntfn_ptr = refs_of' (injectKO r); ntfnObj r = Structures_H.ntfn.ActiveNtfn x2\<rbrakk> \<Longrightarrow> (ntfn_ptr, TCBSignal) \<in> state_refs_of' s t
 3. \<And>x3. \<lbrakk>sym_refs (state_refs_of' s); (t, NTFNSignal) \<in> state_refs_of' s ntfn_ptr; state_refs_of' s ntfn_ptr = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (ntfn_ptr, symreftype tp) \<in> refs_of' ko) x s); state_refs_of' s ntfn_ptr = refs_of' (injectKO r); ntfnObj r = Structures_H.ntfn.WaitingNtfn x3\<rbrakk> \<Longrightarrow> (ntfn_ptr, TCBSignal) \<in> state_refs_of' s t proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>sym_refs (state_refs_of' s); t \<in> set x3; \<forall>x\<in>set x3 \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB r) \<times> {NTFNBound}. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfn_ptr, symreftype tp) \<in> refs_of' ko) x s; state_refs_of' s ntfn_ptr = set x3 \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB r) \<times> {NTFNBound}; ntfnObj r = Structures_H.ntfn.WaitingNtfn x3\<rbrakk> \<Longrightarrow> (ntfn_ptr, TCBSignal) \<in> state_refs_of' s t proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>sym_refs (state_refs_of' s); t \<in> set x3; state_refs_of' s ntfn_ptr = set x3 \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB r) \<times> {NTFNBound}; ntfnObj r = Structures_H.ntfn.WaitingNtfn x3; case (t, NTFNSignal) of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfn_ptr, symreftype tp) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> (ntfn_ptr, TCBSignal) \<in> state_refs_of' s t proof (prove)
goal:
No subgoals! proof (state)
this:
(ntfn_ptr, TCBSignal) \<in> state_refs_of' s t

goal (1 subgoal):
 1. t \<in> set (ntfnQueue (ntfnObj r)) \<Longrightarrow> False proof (chain)
picking this:
ko_at' r ntfn_ptr s
(ntfn_ptr, TCBSignal) \<in> state_refs_of' s t proof (prove)
using this:
ko_at' r ntfn_ptr s
(ntfn_ptr, TCBSignal) \<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 ntfn_ptr s; (ntfn_ptr, TCBSignal) \<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 ntfn_ptr s; ko_wp_at' (\<lambda>obj. (ntfn_ptr, TCBSignal) \<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 ntfn_ptr s; st_tcb_at' (\<lambda>ts. ts = Structures_H.thread_state.BlockedOnNotification ntfn_ptr) t s\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> simple') t s proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>ko_at' r ntfn_ptr s; st = Structures_H.thread_state.BlockedOnNotification ntfn_ptr\<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 (ntfnQueue (ntfnObj 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!