theory TcbQueue_C

lemma ntfn_ntfn_disjoint:
  assumes  srs: "sym_refs (state_refs_of' s)"
  and    ntfnat: "ko_at' ntfn ntfnptr s"
  and   ntfnat': "ko_at' ntfn' ntfnptr' s"
  and     ntfnq: "isWaitingNtfn (ntfnObj ntfn)"
  and    ntfnq': "isWaitingNtfn (ntfnObj ntfn')"
  and      neq: "ntfnptr' \<noteq> ntfnptr"
  shows  "set (ntfnQueue (ntfnObj ntfn)) \<inter> set (ntfnQueue (ntfnObj ntfn')) = {}" using srs ntfnat ntfnat' ntfnq ntfnq' neq 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 split: ntfn.splits) apply (drule bspec, fastforce simp: ko_wp_at'_def)+ apply (clarsimp simp: ko_wp_at'_def refs_of_rev') done

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

goal (1 subgoal):
 1. set (ntfnQueue (ntfnObj ntfn)) \<inter> set (ntfnQueue (ntfnObj ntfn')) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs (state_refs_of' s); ko_at' ntfn ntfnptr s; ko_at' ntfn' ntfnptr' s; isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn'); ntfnptr' \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> set (ntfnQueue (ntfnObj ntfn)) \<inter> set (ntfnQueue (ntfnObj ntfn')) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>sym_refs (state_refs_of' s); ko_at' ntfn ntfnptr s; ko_at' ntfn' ntfnptr' s; isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn'); ntfnptr' \<noteq> ntfnptr; x \<in> set (ntfnQueue (ntfnObj ntfn)); 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); isWaitingNtfn (ntfnObj ntfn'); ntfnptr' \<noteq> ntfnptr; x \<in> set (ntfnQueue (ntfnObj ntfn)); y \<in> set (ntfnQueue (ntfnObj ntfn')); x = y; 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); 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); isWaitingNtfn (ntfnObj ntfn'); ntfnptr' \<noteq> ntfnptr; y \<in> set (ntfnQueue (ntfnObj ntfn)); y \<in> set (ntfnQueue (ntfnObj ntfn')); 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; 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 (1 subgoal):
 1. \<And>y x3 x3a. \<lbrakk>ntfnptr' \<noteq> ntfnptr; y \<in> set x3; y \<in> set x3a; 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; state_refs_of' s ntfnptr' = set x3a \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn'); \<forall>x\<in>set x3a \<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; ntfnObj ntfn' = Structures_H.ntfn.WaitingNtfn x3a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y x3 x3a. \<lbrakk>ntfnptr' \<noteq> ntfnptr; y \<in> set x3; y \<in> set x3a; state_refs_of' s ntfnptr = set x3 \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn); state_refs_of' s ntfnptr' = set x3a \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn'); sym_refs (state_refs_of' s); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3; ntfnObj ntfn' = Structures_H.ntfn.WaitingNtfn x3a; case (y, NTFNSignal) of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x 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!