theory FinalCaps

lemma same_object_as_slots_holding_overlapping_caps:
  "\<lbrakk> same_object_as a cap; \<not> cap_points_to_label aag a (pasSubject aag) \<rbrakk>
     \<Longrightarrow> slots_holding_overlapping_caps cap s = slots_holding_overlapping_caps a s" apply (simp add: same_object_as_def slots_holding_overlapping_caps_def2 ctes_wp_at_def
           split: cap.splits) apply (case_tac cap, simp_all) apply (case_tac cap, simp_all) apply (case_tac cap, simp_all) apply (case_tac cap, simp_all) apply (case_tac cap, simp_all) apply (fastforce dest: aobj_ref_same_aobject) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>same_object_as a cap; \<not> cap_points_to_label aag a (pasSubject aag)\<rbrakk> \<Longrightarrow> slots_holding_overlapping_caps cap s = slots_holding_overlapping_caps a s proof (prove)
goal (6 subgoals):
 1. \<And>x32 x33. \<lbrakk>\<not> cap_points_to_label aag (EndpointCap (obj_ref_of cap) x32 x33) (pasSubject aag); a = EndpointCap (obj_ref_of cap) x32 x33; is_ep_cap cap\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. obj_ref_of cap \<in> obj_refs c) ptr s}
 2. \<And>x42 x43. \<lbrakk>\<not> cap_points_to_label aag (NotificationCap (obj_ref_of cap) x42 x43) (pasSubject aag); a = NotificationCap (obj_ref_of cap) x42 x43; is_ntfn_cap cap\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. obj_ref_of cap \<in> obj_refs c) ptr s}
 3. \<And>x51 x52 x53. \<lbrakk>\<not> cap_points_to_label aag (ReplyCap x51 x52 x53) (pasSubject aag); a = ReplyCap x51 x52 x53; \<exists>m' cr. cap = ReplyCap x51 m' cr\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. False) ptr s}
 4. \<And>x63. \<lbrakk>\<not> cap_points_to_label aag (CNodeCap (obj_ref_of cap) (bits_of cap) x63) (pasSubject aag); a = CNodeCap (obj_ref_of cap) (bits_of cap) x63; is_cnode_cap cap\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. obj_ref_of cap \<in> obj_refs c) ptr s}
 5. \<lbrakk>\<not> cap_points_to_label aag (ThreadCap (obj_ref_of cap)) (pasSubject aag); a = ThreadCap (obj_ref_of cap); is_thread_cap cap\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. obj_ref_of cap \<in> obj_refs c) ptr s}
 6. \<And>x12 x12a. \<lbrakk>\<not> cap_points_to_label aag (ArchObjectCap x12) (pasSubject aag); a = ArchObjectCap x12; cap = ArchObjectCap x12a; same_aobject_as x12 x12a\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. set_option (aobj_ref x12a) \<inter> obj_refs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. set_option (aobj_ref x12) \<inter> obj_refs c \<noteq> {}) ptr s} proof (prove)
goal (5 subgoals):
 1. \<And>x42 x43. \<lbrakk>\<not> cap_points_to_label aag (NotificationCap (obj_ref_of cap) x42 x43) (pasSubject aag); a = NotificationCap (obj_ref_of cap) x42 x43; is_ntfn_cap cap\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. obj_ref_of cap \<in> obj_refs c) ptr s}
 2. \<And>x51 x52 x53. \<lbrakk>\<not> cap_points_to_label aag (ReplyCap x51 x52 x53) (pasSubject aag); a = ReplyCap x51 x52 x53; \<exists>m' cr. cap = ReplyCap x51 m' cr\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. False) ptr s}
 3. \<And>x63. \<lbrakk>\<not> cap_points_to_label aag (CNodeCap (obj_ref_of cap) (bits_of cap) x63) (pasSubject aag); a = CNodeCap (obj_ref_of cap) (bits_of cap) x63; is_cnode_cap cap\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. obj_ref_of cap \<in> obj_refs c) ptr s}
 4. \<lbrakk>\<not> cap_points_to_label aag (ThreadCap (obj_ref_of cap)) (pasSubject aag); a = ThreadCap (obj_ref_of cap); is_thread_cap cap\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. obj_ref_of cap \<in> obj_refs c) ptr s}
 5. \<And>x12 x12a. \<lbrakk>\<not> cap_points_to_label aag (ArchObjectCap x12) (pasSubject aag); a = ArchObjectCap x12; cap = ArchObjectCap x12a; same_aobject_as x12 x12a\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. set_option (aobj_ref x12a) \<inter> obj_refs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. set_option (aobj_ref x12) \<inter> obj_refs c \<noteq> {}) ptr s} proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53. \<lbrakk>\<not> cap_points_to_label aag (ReplyCap x51 x52 x53) (pasSubject aag); a = ReplyCap x51 x52 x53; \<exists>m' cr. cap = ReplyCap x51 m' cr\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. False) ptr s}
 2. \<And>x63. \<lbrakk>\<not> cap_points_to_label aag (CNodeCap (obj_ref_of cap) (bits_of cap) x63) (pasSubject aag); a = CNodeCap (obj_ref_of cap) (bits_of cap) x63; is_cnode_cap cap\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. obj_ref_of cap \<in> obj_refs c) ptr s}
 3. \<lbrakk>\<not> cap_points_to_label aag (ThreadCap (obj_ref_of cap)) (pasSubject aag); a = ThreadCap (obj_ref_of cap); is_thread_cap cap\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. obj_ref_of cap \<in> obj_refs c) ptr s}
 4. \<And>x12 x12a. \<lbrakk>\<not> cap_points_to_label aag (ArchObjectCap x12) (pasSubject aag); a = ArchObjectCap x12; cap = ArchObjectCap x12a; same_aobject_as x12 x12a\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. set_option (aobj_ref x12a) \<inter> obj_refs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. set_option (aobj_ref x12) \<inter> obj_refs c \<noteq> {}) ptr s} proof (prove)
goal (3 subgoals):
 1. \<And>x63. \<lbrakk>\<not> cap_points_to_label aag (CNodeCap (obj_ref_of cap) (bits_of cap) x63) (pasSubject aag); a = CNodeCap (obj_ref_of cap) (bits_of cap) x63; is_cnode_cap cap\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. obj_ref_of cap \<in> obj_refs c) ptr s}
 2. \<lbrakk>\<not> cap_points_to_label aag (ThreadCap (obj_ref_of cap)) (pasSubject aag); a = ThreadCap (obj_ref_of cap); is_thread_cap cap\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. obj_ref_of cap \<in> obj_refs c) ptr s}
 3. \<And>x12 x12a. \<lbrakk>\<not> cap_points_to_label aag (ArchObjectCap x12) (pasSubject aag); a = ArchObjectCap x12; cap = ArchObjectCap x12a; same_aobject_as x12 x12a\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. set_option (aobj_ref x12a) \<inter> obj_refs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. set_option (aobj_ref x12) \<inter> obj_refs c \<noteq> {}) ptr s} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> cap_points_to_label aag (ThreadCap (obj_ref_of cap)) (pasSubject aag); a = ThreadCap (obj_ref_of cap); is_thread_cap cap\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. obj_ref_of cap \<in> obj_refs c) ptr s}
 2. \<And>x12 x12a. \<lbrakk>\<not> cap_points_to_label aag (ArchObjectCap x12) (pasSubject aag); a = ArchObjectCap x12; cap = ArchObjectCap x12a; same_aobject_as x12 x12a\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. set_option (aobj_ref x12a) \<inter> obj_refs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. set_option (aobj_ref x12) \<inter> obj_refs c \<noteq> {}) ptr s} proof (prove)
goal (1 subgoal):
 1. \<And>x12 x12a. \<lbrakk>\<not> cap_points_to_label aag (ArchObjectCap x12) (pasSubject aag); a = ArchObjectCap x12; cap = ArchObjectCap x12a; same_aobject_as x12 x12a\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. set_option (aobj_ref x12a) \<inter> obj_refs c \<noteq> {}) ptr s} = {ptr. cte_wp_at (\<lambda>c. set_option (aobj_ref x12) \<inter> obj_refs c \<noteq> {}) ptr s} proof (prove)
goal:
No subgoals!