theory IpcCancel_R

lemma ep_q_refs_max:
  "\<lbrakk> ko_at' r p s; sym_refs (state_refs_of' s); r \<noteq> IdleEP \<rbrakk>
      \<Longrightarrow> (state_refs_of' s p \<subseteq> (set (epQueue r) \<times> {EPSend, EPRecv}))
       \<and> (\<forall>x\<in>set (epQueue r). \<exists>ntfnptr. state_refs_of' s x \<subseteq>
                                  {(p, TCBBlockedSend), (p, TCBBlockedRecv), (ntfnptr, TCBBound)})" 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' tcb_bound_refs'_def
             | rule conjI | drule(1) bspec | drule st_tcb_at_state_refs_ofD'
             | case_tac ntfnptr)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' r p s; sym_refs (state_refs_of' s); r \<noteq> Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> state_refs_of' s p \<subseteq> set (epQueue r) \<times> {EPSend, EPRecv} \<and> (\<forall>x\<in>set (epQueue r). \<exists>ntfnptr. state_refs_of' s x \<subseteq> {(p, TCBBlockedSend), (p, TCBBlockedRecv), (ntfnptr, TCBBound)}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' r p s; sym_refs (state_refs_of' s); r \<noteq> Structures_H.endpoint.IdleEP; state_refs_of' s p = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> state_refs_of' s p \<subseteq> set (epQueue r) \<times> {EPSend, EPRecv} \<and> (\<forall>x\<in>set (epQueue r). \<exists>ntfnptr. state_refs_of' s x \<subseteq> {(p, TCBBlockedSend), (p, TCBBlockedRecv), (ntfnptr, TCBBound)}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs (state_refs_of' s); r \<noteq> Structures_H.endpoint.IdleEP; state_refs_of' s p = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s); state_refs_of' s p = refs_of' (injectKO r)\<rbrakk> \<Longrightarrow> state_refs_of' s p \<subseteq> set (epQueue r) \<times> {EPSend, EPRecv} \<and> (\<forall>x\<in>set (epQueue r). \<exists>ntfnptr. state_refs_of' s x \<subseteq> {(p, TCBBlockedSend), (p, TCBBlockedRecv), (ntfnptr, TCBBound)}) proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>sym_refs (state_refs_of' s); r \<noteq> Structures_H.endpoint.IdleEP; state_refs_of' s p = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s); state_refs_of' s p = refs_of' (injectKO r); r = Structures_H.endpoint.RecvEP x1\<rbrakk> \<Longrightarrow> state_refs_of' s p \<subseteq> set (epQueue r) \<times> {EPSend, EPRecv} \<and> (\<forall>x\<in>set (epQueue r). \<exists>ntfnptr. state_refs_of' s x \<subseteq> {(p, TCBBlockedSend), (p, TCBBlockedRecv), (ntfnptr, TCBBound)})
 2. \<lbrakk>sym_refs (state_refs_of' s); r \<noteq> Structures_H.endpoint.IdleEP; state_refs_of' s p = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s); state_refs_of' s p = refs_of' (injectKO r); r = Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> state_refs_of' s p \<subseteq> set (epQueue r) \<times> {EPSend, EPRecv} \<and> (\<forall>x\<in>set (epQueue r). \<exists>ntfnptr. state_refs_of' s x \<subseteq> {(p, TCBBlockedSend), (p, TCBBlockedRecv), (ntfnptr, TCBBound)})
 3. \<And>x3. \<lbrakk>sym_refs (state_refs_of' s); r \<noteq> Structures_H.endpoint.IdleEP; state_refs_of' s p = refs_of' (injectKO r) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO r). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s); state_refs_of' s p = refs_of' (injectKO r); r = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> state_refs_of' s p \<subseteq> set (epQueue r) \<times> {EPSend, EPRecv} \<and> (\<forall>x\<in>set (epQueue r). \<exists>ntfnptr. state_refs_of' s x \<subseteq> {(p, TCBBlockedSend), (p, TCBBlockedRecv), (ntfnptr, TCBBound)}) proof (prove)
goal:
No subgoals!