theory IpcCancel_C

lemma ep_ep_disjoint:
  assumes srs: "sym_refs (state_refs_of' s)"
  and    epat: "ko_at' ep epptr s"
  and   epat': "ko_at' ep' epptr' s"
  and     epq: "(isSendEP ep \<or> isRecvEP ep)"
  and    epq': "(isSendEP ep' \<or> isRecvEP ep')"
  and      neq: "epptr' \<noteq> epptr"
  shows  "set (epQueue ep) \<inter> set (epQueue ep') = {}" using srs epat epat' epq epq' neq apply - apply (subst disjoint_iff_not_equal, intro ballI, rule notI) apply (drule sym_refs_ko_atD', clarsimp)+ apply clarsimp apply (clarsimp simp: isSendEP_def isRecvEP_def split: endpoint.splits) apply (simp_all add: st_tcb_at_refs_of_rev') apply (fastforce simp: st_tcb_at'_def obj_at'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (epQueue ep) \<inter> set (epQueue ep') = {} proof (prove)
using this:
sym_refs (state_refs_of' s)
ko_at' ep epptr s
ko_at' ep' epptr' s
isSendEP ep \<or> isRecvEP ep
isSendEP ep' \<or> isRecvEP ep'
epptr' \<noteq> epptr

goal (1 subgoal):
 1. set (epQueue ep) \<inter> set (epQueue ep') = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs (state_refs_of' s); ko_at' ep epptr s; ko_at' ep' epptr' s; isSendEP ep \<or> isRecvEP ep; isSendEP ep' \<or> isRecvEP ep'; epptr' \<noteq> epptr\<rbrakk> \<Longrightarrow> set (epQueue ep) \<inter> set (epQueue ep') = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>sym_refs (state_refs_of' s); ko_at' ep epptr s; ko_at' ep' epptr' s; isSendEP ep \<or> isRecvEP ep; isSendEP ep' \<or> isRecvEP ep'; epptr' \<noteq> epptr; x \<in> set (epQueue ep); y \<in> set (epQueue ep'); x = y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>sym_refs (state_refs_of' s); isSendEP ep \<or> isRecvEP ep; isSendEP ep' \<or> isRecvEP ep'; epptr' \<noteq> epptr; x \<in> set (epQueue ep); y \<in> set (epQueue ep'); x = y; state_refs_of' s epptr = refs_of' (injectKOS ep) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ep). ko_wp_at' (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of' ko) x s); state_refs_of' s epptr' = refs_of' (injectKOS ep') \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ep'). ko_wp_at' (\<lambda>ko. (epptr', symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>sym_refs (state_refs_of' s); isSendEP ep \<or> isRecvEP ep; isSendEP ep' \<or> isRecvEP ep'; epptr' \<noteq> epptr; y \<in> set (epQueue ep); y \<in> set (epQueue ep'); state_refs_of' s epptr = ep_q_refs_of' ep; \<forall>x\<in>ep_q_refs_of' ep. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of' ko) x s; state_refs_of' s epptr' = ep_q_refs_of' ep'; \<forall>x\<in>ep_q_refs_of' ep'. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (epptr', symreftype tp) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>y x1 x1a. \<lbrakk>epptr' \<noteq> epptr; y \<in> set x1; y \<in> set x1a; state_refs_of' s epptr = set x1 \<times> {EPRecv}; \<forall>x\<in>set x1. ko_wp_at' (\<lambda>ko. (epptr, TCBBlockedRecv) \<in> refs_of' ko) x s; state_refs_of' s epptr' = set x1a \<times> {EPRecv}; \<forall>x\<in>set x1a. ko_wp_at' (\<lambda>ko. (epptr', TCBBlockedRecv) \<in> refs_of' ko) x s; sym_refs (state_refs_of' s); ep = Structures_H.endpoint.RecvEP x1; ep' = Structures_H.endpoint.RecvEP x1a\<rbrakk> \<Longrightarrow> False
 2. \<And>y x1 x3. \<lbrakk>epptr' \<noteq> epptr; y \<in> set x1; y \<in> set x3; state_refs_of' s epptr = set x1 \<times> {EPRecv}; \<forall>x\<in>set x1. ko_wp_at' (\<lambda>ko. (epptr, TCBBlockedRecv) \<in> refs_of' ko) x s; state_refs_of' s epptr' = set x3 \<times> {EPSend}; \<forall>x\<in>set x3. ko_wp_at' (\<lambda>ko. (epptr', TCBBlockedSend) \<in> refs_of' ko) x s; sym_refs (state_refs_of' s); ep = Structures_H.endpoint.RecvEP x1; ep' = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> False
 3. \<And>y x3 x1. \<lbrakk>epptr' \<noteq> epptr; y \<in> set x3; y \<in> set x1; state_refs_of' s epptr = set x3 \<times> {EPSend}; \<forall>x\<in>set x3. ko_wp_at' (\<lambda>ko. (epptr, TCBBlockedSend) \<in> refs_of' ko) x s; state_refs_of' s epptr' = set x1 \<times> {EPRecv}; \<forall>x\<in>set x1. ko_wp_at' (\<lambda>ko. (epptr', TCBBlockedRecv) \<in> refs_of' ko) x s; sym_refs (state_refs_of' s); ep = Structures_H.endpoint.SendEP x3; ep' = Structures_H.endpoint.RecvEP x1\<rbrakk> \<Longrightarrow> False
 4. \<And>y x3 x3a. \<lbrakk>epptr' \<noteq> epptr; y \<in> set x3; y \<in> set x3a; state_refs_of' s epptr = set x3 \<times> {EPSend}; \<forall>x\<in>set x3. ko_wp_at' (\<lambda>ko. (epptr, TCBBlockedSend) \<in> refs_of' ko) x s; state_refs_of' s epptr' = set x3a \<times> {EPSend}; \<forall>x\<in>set x3a. ko_wp_at' (\<lambda>ko. (epptr', TCBBlockedSend) \<in> refs_of' ko) x s; sym_refs (state_refs_of' s); ep = Structures_H.endpoint.SendEP x3; ep' = Structures_H.endpoint.SendEP x3a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>y x1 x1a. \<lbrakk>epptr' \<noteq> epptr; y \<in> set x1; y \<in> set x1a; state_refs_of' s epptr = set x1 \<times> {EPRecv}; \<forall>x\<in>set x1. st_tcb_at' (\<lambda>ts. \<exists>a. ts = Structures_H.thread_state.BlockedOnReceive epptr a) x s; state_refs_of' s epptr' = set x1a \<times> {EPRecv}; \<forall>x\<in>set x1a. st_tcb_at' (\<lambda>ts. \<exists>a. ts = Structures_H.thread_state.BlockedOnReceive epptr' a) x s; sym_refs (state_refs_of' s); ep = Structures_H.endpoint.RecvEP x1; ep' = Structures_H.endpoint.RecvEP x1a\<rbrakk> \<Longrightarrow> False
 2. \<And>y x1 x3. \<lbrakk>epptr' \<noteq> epptr; y \<in> set x1; y \<in> set x3; state_refs_of' s epptr = set x1 \<times> {EPRecv}; \<forall>x\<in>set x1. st_tcb_at' (\<lambda>ts. \<exists>a. ts = Structures_H.thread_state.BlockedOnReceive epptr a) x s; state_refs_of' s epptr' = set x3 \<times> {EPSend}; \<forall>x\<in>set x3. st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr' a b c d) x s; sym_refs (state_refs_of' s); ep = Structures_H.endpoint.RecvEP x1; ep' = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> False
 3. \<And>y x3 x1. \<lbrakk>epptr' \<noteq> epptr; y \<in> set x3; y \<in> set x1; state_refs_of' s epptr = set x3 \<times> {EPSend}; \<forall>x\<in>set x3. st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; state_refs_of' s epptr' = set x1 \<times> {EPRecv}; \<forall>x\<in>set x1. st_tcb_at' (\<lambda>ts. \<exists>a. ts = Structures_H.thread_state.BlockedOnReceive epptr' a) x s; sym_refs (state_refs_of' s); ep = Structures_H.endpoint.SendEP x3; ep' = Structures_H.endpoint.RecvEP x1\<rbrakk> \<Longrightarrow> False
 4. \<And>y x3 x3a. \<lbrakk>epptr' \<noteq> epptr; y \<in> set x3; y \<in> set x3a; state_refs_of' s epptr = set x3 \<times> {EPSend}; \<forall>x\<in>set x3. st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; state_refs_of' s epptr' = set x3a \<times> {EPSend}; \<forall>x\<in>set x3a. st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr' a b c d) x s; sym_refs (state_refs_of' s); ep = Structures_H.endpoint.SendEP x3; ep' = Structures_H.endpoint.SendEP x3a\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!