theory FinalCaps

lemma same_object_as_cap_points_to_label:
  "\<lbrakk> same_object_as a cap; \<not> cap_points_to_label aag a (pasSubject aag) \<rbrakk>
     \<Longrightarrow> \<not> cap_points_to_label aag cap (pasSubject aag)" apply (simp add: same_object_as_def cap_points_to_label_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 (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> \<not> cap_points_to_label aag cap (pasSubject aag) proof (prove)
goal (5 subgoals):
 1. \<And>x32 x33. \<lbrakk>pasObjectAbs aag (obj_ref_of cap) \<noteq> pasSubject aag; a = EndpointCap (obj_ref_of cap) x32 x33; is_ep_cap cap\<rbrakk> \<Longrightarrow> (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasSubject aag) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasSubject aag)
 2. \<And>x42 x43. \<lbrakk>pasObjectAbs aag (obj_ref_of cap) \<noteq> pasSubject aag; a = NotificationCap (obj_ref_of cap) x42 x43; is_ntfn_cap cap\<rbrakk> \<Longrightarrow> (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasSubject aag) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasSubject aag)
 3. \<And>x63. \<lbrakk>pasObjectAbs aag (obj_ref_of cap) \<noteq> pasSubject aag; a = CNodeCap (obj_ref_of cap) (bits_of cap) x63; is_cnode_cap cap\<rbrakk> \<Longrightarrow> (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasSubject aag) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasSubject aag)
 4. \<lbrakk>pasObjectAbs aag (obj_ref_of cap) \<noteq> pasSubject aag; a = ThreadCap (obj_ref_of cap); is_thread_cap cap\<rbrakk> \<Longrightarrow> (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasSubject aag) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasSubject aag)
 5. \<And>x12 x12a. \<lbrakk>\<exists>x\<in>set_option (aobj_ref x12). pasObjectAbs aag x \<noteq> pasSubject aag; a = ArchObjectCap x12; cap = ArchObjectCap x12a; same_aobject_as x12 x12a\<rbrakk> \<Longrightarrow> \<exists>x\<in>set_option (aobj_ref x12a). pasObjectAbs aag x \<noteq> pasSubject aag proof (prove)
goal (4 subgoals):
 1. \<And>x42 x43. \<lbrakk>pasObjectAbs aag (obj_ref_of cap) \<noteq> pasSubject aag; a = NotificationCap (obj_ref_of cap) x42 x43; is_ntfn_cap cap\<rbrakk> \<Longrightarrow> (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasSubject aag) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasSubject aag)
 2. \<And>x63. \<lbrakk>pasObjectAbs aag (obj_ref_of cap) \<noteq> pasSubject aag; a = CNodeCap (obj_ref_of cap) (bits_of cap) x63; is_cnode_cap cap\<rbrakk> \<Longrightarrow> (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasSubject aag) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasSubject aag)
 3. \<lbrakk>pasObjectAbs aag (obj_ref_of cap) \<noteq> pasSubject aag; a = ThreadCap (obj_ref_of cap); is_thread_cap cap\<rbrakk> \<Longrightarrow> (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasSubject aag) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasSubject aag)
 4. \<And>x12 x12a. \<lbrakk>\<exists>x\<in>set_option (aobj_ref x12). pasObjectAbs aag x \<noteq> pasSubject aag; a = ArchObjectCap x12; cap = ArchObjectCap x12a; same_aobject_as x12 x12a\<rbrakk> \<Longrightarrow> \<exists>x\<in>set_option (aobj_ref x12a). pasObjectAbs aag x \<noteq> pasSubject aag proof (prove)
goal (3 subgoals):
 1. \<And>x63. \<lbrakk>pasObjectAbs aag (obj_ref_of cap) \<noteq> pasSubject aag; a = CNodeCap (obj_ref_of cap) (bits_of cap) x63; is_cnode_cap cap\<rbrakk> \<Longrightarrow> (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasSubject aag) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasSubject aag)
 2. \<lbrakk>pasObjectAbs aag (obj_ref_of cap) \<noteq> pasSubject aag; a = ThreadCap (obj_ref_of cap); is_thread_cap cap\<rbrakk> \<Longrightarrow> (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasSubject aag) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasSubject aag)
 3. \<And>x12 x12a. \<lbrakk>\<exists>x\<in>set_option (aobj_ref x12). pasObjectAbs aag x \<noteq> pasSubject aag; a = ArchObjectCap x12; cap = ArchObjectCap x12a; same_aobject_as x12 x12a\<rbrakk> \<Longrightarrow> \<exists>x\<in>set_option (aobj_ref x12a). pasObjectAbs aag x \<noteq> pasSubject aag proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pasObjectAbs aag (obj_ref_of cap) \<noteq> pasSubject aag; a = ThreadCap (obj_ref_of cap); is_thread_cap cap\<rbrakk> \<Longrightarrow> (\<exists>x\<in>obj_refs cap. pasObjectAbs aag x \<noteq> pasSubject aag) \<or> (\<exists>x\<in>cap_irqs cap. pasIRQAbs aag x \<noteq> pasSubject aag)
 2. \<And>x12 x12a. \<lbrakk>\<exists>x\<in>set_option (aobj_ref x12). pasObjectAbs aag x \<noteq> pasSubject aag; a = ArchObjectCap x12; cap = ArchObjectCap x12a; same_aobject_as x12 x12a\<rbrakk> \<Longrightarrow> \<exists>x\<in>set_option (aobj_ref x12a). pasObjectAbs aag x \<noteq> pasSubject aag proof (prove)
goal (1 subgoal):
 1. \<And>x12 x12a. \<lbrakk>\<exists>x\<in>set_option (aobj_ref x12). pasObjectAbs aag x \<noteq> pasSubject aag; a = ArchObjectCap x12; cap = ArchObjectCap x12a; same_aobject_as x12 x12a\<rbrakk> \<Longrightarrow> \<exists>x\<in>set_option (aobj_ref x12a). pasObjectAbs aag x \<noteq> pasSubject aag proof (prove)
goal:
No subgoals!