theory TcbQueue_C

lemma ntfn_ep_disjoint:
  assumes  srs: "sym_refs (state_refs_of' s)"
  and     epat: "ko_at' ep epptr s"
  and    ntfnat: "ko_at' ntfn ntfnptr s"
  and  ntfnq: "isWaitingNtfn (ntfnObj ntfn)"
  and   epq: "isSendEP ep \<or> isRecvEP ep"
  shows  "set (epQueue ep) \<inter> set (ntfnQueue (ntfnObj ntfn)) = {}" using srs epat ntfnat ntfnq epq apply - apply (subst disjoint_iff_not_equal, intro ballI, rule notI) apply (drule sym_refs_ko_atD', clarsimp)+ apply clarsimp apply (clarsimp simp: isWaitingNtfn_def isSendEP_def isRecvEP_def
                 split: ntfn.splits endpoint.splits) apply (drule bspec, fastforce simp: ko_wp_at'_def)+ apply (fastforce simp: ko_wp_at'_def refs_of_rev') apply (drule bspec, fastforce simp: ko_wp_at'_def)+ apply (fastforce simp: ko_wp_at'_def refs_of_rev') done

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

goal (1 subgoal):
 1. set (epQueue ep) \<inter> set (ntfnQueue (ntfnObj ntfn)) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs (state_refs_of' s); ko_at' ep epptr s; ko_at' ntfn ntfnptr s; isWaitingNtfn (ntfnObj ntfn); isSendEP ep \<or> isRecvEP ep\<rbrakk> \<Longrightarrow> set (epQueue ep) \<inter> set (ntfnQueue (ntfnObj ntfn)) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>sym_refs (state_refs_of' s); ko_at' ep epptr s; ko_at' ntfn ntfnptr s; isWaitingNtfn (ntfnObj ntfn); isSendEP ep \<or> isRecvEP ep; x \<in> set (epQueue ep); y \<in> set (ntfnQueue (ntfnObj ntfn)); x = y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>sym_refs (state_refs_of' s); isWaitingNtfn (ntfnObj ntfn); isSendEP ep \<or> isRecvEP ep; x \<in> set (epQueue ep); y \<in> set (ntfnQueue (ntfnObj ntfn)); 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 ntfnptr = refs_of' (injectKOS ntfn) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ntfn). ko_wp_at' (\<lambda>ko. (ntfnptr, 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); isWaitingNtfn (ntfnObj ntfn); isSendEP ep \<or> isRecvEP ep; y \<in> set (epQueue ep); y \<in> set (ntfnQueue (ntfnObj ntfn)); 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 ntfnptr = ntfn_q_refs_of' (ntfnObj ntfn) \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn); \<forall>x\<in>ntfn_q_refs_of' (ntfnObj ntfn) \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y x3 x1. \<lbrakk>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 ntfnptr = set x3 \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn); \<forall>x\<in>set x3 \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s; sym_refs (state_refs_of' s); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; ep = Structures_H.endpoint.RecvEP x1\<rbrakk> \<Longrightarrow> False
 2. \<And>y x3 x3a. \<lbrakk>y \<in> set x3a; y \<in> set x3; 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; state_refs_of' s ntfnptr = set x3 \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn); \<forall>x\<in>set x3 \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s; sym_refs (state_refs_of' s); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; ep = Structures_H.endpoint.SendEP x3a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y x3 x1. \<lbrakk>y \<in> set x1; y \<in> set x3; state_refs_of' s epptr = set x1 \<times> {EPRecv}; state_refs_of' s ntfnptr = set x3 \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn); sym_refs (state_refs_of' s); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; ep = Structures_H.endpoint.RecvEP x1; ko_wp_at' (\<lambda>ko. (epptr, TCBBlockedRecv) \<in> refs_of' ko) y s; case (y, NTFNSignal) of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> False
 2. \<And>y x3 x3a. \<lbrakk>y \<in> set x3a; y \<in> set x3; 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; state_refs_of' s ntfnptr = set x3 \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn); \<forall>x\<in>set x3 \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s; sym_refs (state_refs_of' s); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; ep = Structures_H.endpoint.SendEP x3a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y x3 x3a. \<lbrakk>y \<in> set x3a; y \<in> set x3; 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; state_refs_of' s ntfnptr = set x3 \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn); \<forall>x\<in>set x3 \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s; sym_refs (state_refs_of' s); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; ep = Structures_H.endpoint.SendEP x3a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y x3 x3a. \<lbrakk>y \<in> set x3a; y \<in> set x3; state_refs_of' s epptr = set x3a \<times> {EPSend}; state_refs_of' s ntfnptr = set x3 \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn); sym_refs (state_refs_of' s); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; ep = Structures_H.endpoint.SendEP x3a; ko_wp_at' (\<lambda>ko. (epptr, TCBBlockedSend) \<in> refs_of' ko) y s; case (y, NTFNSignal) of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!