theory Finalise_R

lemma final_matters_sameRegion_sameObject2:
  "\<lbrakk> final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap' \<rbrakk>
     \<Longrightarrow> sameRegionAs cap cap' = sameObjectAs cap cap'" apply (rule iffI) apply (erule sameRegionAsE) apply (simp add: sameObjectAs_def3) apply (fastforce simp: isCap_simps final_matters'_def) apply simp apply (clarsimp simp: final_matters'_def isCap_simps) apply (clarsimp simp: final_matters'_def isCap_simps) apply (erule sameObjectAs_sameRegionAs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' = global.sameObjectAs cap cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 2. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; global.sameObjectAs cap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 2. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 3. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 4. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 5. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; global.sameObjectAs cap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>final_matters' cap'; \<not> isIRQHandlerCap cap'; capMasterCap cap = capMasterCap cap'; cap \<noteq> capability.NullCap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> (isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {})
 2. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 3. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 4. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 5. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; global.sameObjectAs cap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 2. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 3. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 4. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; global.sameObjectAs cap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 2. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 3. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; global.sameObjectAs cap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 2. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; global.sameObjectAs cap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap'; global.sameObjectAs cap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' proof (prove)
goal:
No subgoals!