theory CSpace_I

lemma sameRegionAs_trans:
  "\<lbrakk> sameRegionAs a b; sameRegionAs b c \<rbrakk> \<Longrightarrow> sameRegionAs a c" apply (simp add: sameRegionAs_def2, elim conjE disjE, simp_all) apply (auto simp: isCap_simps) apply (auto simp: capRange_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs a b; global.sameRegionAs b c\<rbrakk> \<Longrightarrow> global.sameRegionAs a c proof (prove)
goal (8 subgoals):
 1. \<lbrakk>capRange (capMasterCap b) \<noteq> {}; capRange (capMasterCap b) \<subseteq> capRange (capMasterCap a); capRange (capMasterCap c) \<noteq> {}; capRange (capMasterCap c) \<subseteq> capRange (capMasterCap b); isUntypedCap (capMasterCap a); isUntypedCap (capMasterCap b)\<rbrakk> \<Longrightarrow> capRange (capMasterCap c) \<subseteq> capRange (capMasterCap a) \<or> isIRQControlCap (capMasterCap a) \<and> isIRQHandlerCap (capMasterCap c)
 2. \<lbrakk>capRange (capMasterCap b) \<noteq> {}; capRange (capMasterCap b) \<subseteq> capRange (capMasterCap a); capRange (capMasterCap c) \<noteq> {}; capRange (capMasterCap c) \<subseteq> capRange (capMasterCap b); isUntypedCap (capMasterCap a); isArchPageCap (capMasterCap b); isArchPageCap (capMasterCap c)\<rbrakk> \<Longrightarrow> capRange (capMasterCap c) \<subseteq> capRange (capMasterCap a) \<or> isIRQControlCap (capMasterCap a) \<and> isIRQHandlerCap (capMasterCap c)
 3. \<lbrakk>capRange (capMasterCap b) \<noteq> {}; capRange (capMasterCap b) \<subseteq> capRange (capMasterCap a); capRange (capMasterCap c) \<noteq> {}; capRange (capMasterCap c) \<subseteq> capRange (capMasterCap b); isArchPageCap (capMasterCap a); isArchPageCap (capMasterCap b); isUntypedCap (capMasterCap b)\<rbrakk> \<Longrightarrow> capRange (capMasterCap c) \<subseteq> capRange (capMasterCap a) \<and> (isUntypedCap (capMasterCap a) \<or> isArchPageCap (capMasterCap c)) \<or> isIRQControlCap (capMasterCap a) \<and> isIRQHandlerCap (capMasterCap c)
 4. \<lbrakk>capRange (capMasterCap b) \<noteq> {}; capRange (capMasterCap b) \<subseteq> capRange (capMasterCap a); capRange (capMasterCap c) \<noteq> {}; capRange (capMasterCap c) \<subseteq> capRange (capMasterCap b); isArchPageCap (capMasterCap a); isArchPageCap (capMasterCap b); isArchPageCap (capMasterCap c)\<rbrakk> \<Longrightarrow> capRange (capMasterCap c) \<subseteq> capRange (capMasterCap a) \<or> isIRQControlCap (capMasterCap a) \<and> isIRQHandlerCap (capMasterCap c)
 5. \<lbrakk>capRange (capMasterCap b) \<noteq> {}; capRange (capMasterCap b) \<subseteq> capRange (capMasterCap a); isIRQControlCap (capMasterCap b); isIRQHandlerCap (capMasterCap c); isUntypedCap (capMasterCap a)\<rbrakk> \<Longrightarrow> capRange (capMasterCap c) \<noteq> {} \<and> capRange (capMasterCap c) \<subseteq> capRange (capMasterCap a) \<or> isIRQControlCap (capMasterCap a)
 6. \<lbrakk>capRange (capMasterCap b) \<noteq> {}; capRange (capMasterCap b) \<subseteq> capRange (capMasterCap a); isIRQControlCap (capMasterCap b); isIRQHandlerCap (capMasterCap c); isArchPageCap (capMasterCap a); isArchPageCap (capMasterCap b)\<rbrakk> \<Longrightarrow> capRange (capMasterCap c) \<noteq> {} \<and> capRange (capMasterCap c) \<subseteq> capRange (capMasterCap a) \<and> (isUntypedCap (capMasterCap a) \<or> isArchPageCap (capMasterCap c)) \<or> isIRQControlCap (capMasterCap a)
 7. \<lbrakk>isIRQControlCap (capMasterCap a); isIRQHandlerCap (capMasterCap b); capRange (capMasterCap c) \<noteq> {}; capRange (capMasterCap c) \<subseteq> capRange (capMasterCap b); isUntypedCap (capMasterCap b)\<rbrakk> \<Longrightarrow> capMasterCap a = capMasterCap c \<and> capMasterCap a \<noteq> capability.NullCap \<and> \<not> isZombie (capMasterCap a) \<and> \<not> isUntypedCap (capMasterCap a) \<and> \<not> isArchPageCap (capMasterCap a) \<and> capMasterCap c \<noteq> capability.NullCap \<and> \<not> isZombie (capMasterCap c) \<and> \<not> isUntypedCap (capMasterCap c) \<and> \<not> isArchPageCap (capMasterCap c) \<or> capRange (capMasterCap c) \<subseteq> capRange (capMasterCap a) \<and> (isUntypedCap (capMasterCap a) \<or> isArchPageCap (capMasterCap a) \<and> isArchPageCap (capMasterCap c)) \<or> isIRQHandlerCap (capMasterCap c)
 8. \<lbrakk>isIRQControlCap (capMasterCap a); isIRQHandlerCap (capMasterCap b); capRange (capMasterCap c) \<noteq> {}; capRange (capMasterCap c) \<subseteq> capRange (capMasterCap b); isArchPageCap (capMasterCap b); isArchPageCap (capMasterCap c)\<rbrakk> \<Longrightarrow> capRange (capMasterCap c) \<subseteq> capRange (capMasterCap a) \<and> (isUntypedCap (capMasterCap a) \<or> isArchPageCap (capMasterCap a)) \<or> isIRQHandlerCap (capMasterCap c) proof (prove)
goal (3 subgoals):
 1. \<And>v0 d v0a v1 f x. \<lbrakk>capRange capability.IRQControlCap \<subseteq> {v0a..v0a + 2 ^ v1 - 1}; b = capability.IRQControlCap; c = capability.IRQHandlerCap v0; capMasterCap a = capability.UntypedCap d v0a v1 f; x \<in> capRange capability.IRQControlCap; capRange (capability.IRQHandlerCap v0) = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>v0 d v0a v1 f x xa. \<lbrakk>capRange capability.IRQControlCap \<subseteq> {v0a..v0a + 2 ^ v1 - 1}; b = capability.IRQControlCap; c = capability.IRQHandlerCap v0; capMasterCap a = capability.UntypedCap d v0a v1 f; x \<in> capRange capability.IRQControlCap; xa \<in> capRange (capability.IRQHandlerCap v0)\<rbrakk> \<Longrightarrow> v0a \<le> xa
 3. \<And>v0 d v0a v1 f x xa. \<lbrakk>capRange capability.IRQControlCap \<subseteq> {v0a..v0a + 2 ^ v1 - 1}; b = capability.IRQControlCap; c = capability.IRQHandlerCap v0; capMasterCap a = capability.UntypedCap d v0a v1 f; x \<in> capRange capability.IRQControlCap; xa \<in> capRange (capability.IRQHandlerCap v0)\<rbrakk> \<Longrightarrow> xa \<le> v0a + 2 ^ v1 - 1 proof (prove)
goal:
No subgoals!