theory FinalCaps

lemma weak_derived_overlaps':
  "\<lbrakk> weak_derived cap cap'; obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {} \<rbrakk>
     \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<or>
         cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}" apply (simp add: weak_derived_def) apply (erule disjE) prefer 2 apply simp apply (simp add: copy_of_def split: if_split_asm add: same_object_as_def split: cap.splits) apply ((case_tac cap; simp)+)[5] apply (clarsimp simp: aobj_ref_same_aobject) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>weak_derived cap cap'; obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<or> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>copy_of cap cap' \<and> cap_asid cap = cap_asid cap' \<and> cap_asid_base cap = cap_asid_base cap' \<and> cap_vptr cap = cap_vptr cap' \<or> cap' = cap; obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; copy_of cap cap' \<and> cap_asid cap = cap_asid cap' \<and> cap_asid_base cap = cap_asid_base cap' \<and> cap_vptr cap = cap_vptr cap'\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}
 2. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; cap' = cap\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; cap' = cap\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}
 2. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; copy_of cap cap' \<and> cap_asid cap = cap_asid cap' \<and> cap_asid_base cap = cap_asid_base cap' \<and> cap_vptr cap = cap_vptr cap'\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; copy_of cap cap' \<and> cap_asid cap = cap_asid cap' \<and> cap_asid_base cap = cap_asid_base cap' \<and> cap_vptr cap = cap_vptr cap'\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {} proof (prove)
goal (6 subgoals):
 1. \<And>x32 x33. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; cap' = EndpointCap (obj_ref_of cap) x32 x33; is_ep_cap cap \<and> is_reply_cap (EndpointCap (obj_ref_of cap) x32 x33) = is_reply_cap cap \<and> is_master_reply_cap (EndpointCap (obj_ref_of cap) x32 x33) = is_master_reply_cap cap \<and> cap_asid cap = cap_asid (EndpointCap (obj_ref_of cap) x32 x33) \<and> cap_asid_base cap = cap_asid_base (EndpointCap (obj_ref_of cap) x32 x33) \<and> cap_vptr cap = cap_vptr (EndpointCap (obj_ref_of cap) x32 x33)\<rbrakk> \<Longrightarrow> obj_ref_of cap \<in> obj_refs cap
 2. \<And>x42 x43. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; cap' = NotificationCap (obj_ref_of cap) x42 x43; is_ntfn_cap cap \<and> is_reply_cap (NotificationCap (obj_ref_of cap) x42 x43) = is_reply_cap cap \<and> is_master_reply_cap (NotificationCap (obj_ref_of cap) x42 x43) = is_master_reply_cap cap \<and> cap_asid cap = cap_asid (NotificationCap (obj_ref_of cap) x42 x43) \<and> cap_asid_base cap = cap_asid_base (NotificationCap (obj_ref_of cap) x42 x43) \<and> cap_vptr cap = cap_vptr (NotificationCap (obj_ref_of cap) x42 x43)\<rbrakk> \<Longrightarrow> obj_ref_of cap \<in> obj_refs cap
 3. \<And>x51 x52 x53. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; cap' = ReplyCap x51 x52 x53; (\<exists>m' cr. cap = ReplyCap x51 m' cr) \<and> is_reply_cap (ReplyCap x51 x52 x53) = is_reply_cap cap \<and> is_master_reply_cap (ReplyCap x51 x52 x53) = is_master_reply_cap cap \<and> cap_asid cap = cap_asid (ReplyCap x51 x52 x53) \<and> cap_asid_base cap = cap_asid_base (ReplyCap x51 x52 x53) \<and> cap_vptr cap = cap_vptr (ReplyCap x51 x52 x53)\<rbrakk> \<Longrightarrow> False
 4. \<And>x63. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; cap' = CNodeCap (obj_ref_of cap) (bits_of cap) x63; is_cnode_cap cap \<and> is_reply_cap (CNodeCap (obj_ref_of cap) (bits_of cap) x63) = is_reply_cap cap \<and> is_master_reply_cap (CNodeCap (obj_ref_of cap) (bits_of cap) x63) = is_master_reply_cap cap \<and> cap_asid cap = cap_asid (CNodeCap (obj_ref_of cap) (bits_of cap) x63) \<and> cap_asid_base cap = cap_asid_base (CNodeCap (obj_ref_of cap) (bits_of cap) x63) \<and> cap_vptr cap = cap_vptr (CNodeCap (obj_ref_of cap) (bits_of cap) x63)\<rbrakk> \<Longrightarrow> obj_ref_of cap \<in> obj_refs cap
 5. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; cap' = ThreadCap (obj_ref_of cap); is_thread_cap cap \<and> is_reply_cap (ThreadCap (obj_ref_of cap)) = is_reply_cap cap \<and> is_master_reply_cap (ThreadCap (obj_ref_of cap)) = is_master_reply_cap cap \<and> cap_asid cap = cap_asid (ThreadCap (obj_ref_of cap)) \<and> cap_asid_base cap = cap_asid_base (ThreadCap (obj_ref_of cap)) \<and> cap_vptr cap = cap_vptr (ThreadCap (obj_ref_of cap))\<rbrakk> \<Longrightarrow> obj_ref_of cap \<in> obj_refs cap
 6. \<And>x12 x12a. \<lbrakk>\<exists>y. aobj_ref x12a = Some y; cap' = ArchObjectCap x12; cap = ArchObjectCap x12a; same_aobject_as x12 x12a \<and> is_reply_cap (ArchObjectCap x12) = is_reply_cap (ArchObjectCap x12a) \<and> is_master_reply_cap (ArchObjectCap x12) = is_master_reply_cap (ArchObjectCap x12a) \<and> cap_asid (ArchObjectCap x12a) = cap_asid (ArchObjectCap x12) \<and> cap_asid_base (ArchObjectCap x12a) = cap_asid_base (ArchObjectCap x12) \<and> cap_vptr (ArchObjectCap x12a) = cap_vptr (ArchObjectCap x12)\<rbrakk> \<Longrightarrow> set_option (aobj_ref x12a) \<inter> set_option (aobj_ref x12) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x12 x12a. \<lbrakk>\<exists>y. aobj_ref x12a = Some y; cap' = ArchObjectCap x12; cap = ArchObjectCap x12a; same_aobject_as x12 x12a \<and> is_reply_cap (ArchObjectCap x12) = is_reply_cap (ArchObjectCap x12a) \<and> is_master_reply_cap (ArchObjectCap x12) = is_master_reply_cap (ArchObjectCap x12a) \<and> cap_asid (ArchObjectCap x12a) = cap_asid (ArchObjectCap x12) \<and> cap_asid_base (ArchObjectCap x12a) = cap_asid_base (ArchObjectCap x12) \<and> cap_vptr (ArchObjectCap x12a) = cap_vptr (ArchObjectCap x12)\<rbrakk> \<Longrightarrow> set_option (aobj_ref x12a) \<inter> set_option (aobj_ref x12) \<noteq> {} proof (prove)
goal:
No subgoals!