theory CSpace_R

lemma c'_new:
  "m p = Some (CTE cap node) \<Longrightarrow> \<not> sameRegionAs c' cap" using safe_parent src unfolding safe_parent_for'_def apply (elim exE conjE) apply (erule disjE) apply (erule irq_c'_new [rotated]) apply (clarsimp simp: isCap_simps) apply clarsimp apply (drule (1) ut_c'_new) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<not> global.sameRegionAs c' cap proof (prove)
using this:
safe_parent_for' m src c'
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<not> global.sameRegionAs c' cap proof (prove)
using this:
\<exists>parent node. m src = Some (CTE parent node) \<and> global.sameRegionAs parent c' \<and> ((\<exists>irq. c' = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. m p \<noteq> Some (CTE c' n')) \<or> isUntypedCap parent \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits parent)
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<not> global.sameRegionAs c' cap proof (prove)
goal (1 subgoal):
 1. \<And>parent nodea. \<lbrakk>m p = Some (CTE cap node); m src = Some (CTE src_cap src_node); m src = Some (CTE parent nodea); global.sameRegionAs parent c'; (\<exists>irq. c' = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. m p \<noteq> Some (CTE c' n')) \<or> isUntypedCap parent \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits parent\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c' cap proof (prove)
goal (2 subgoals):
 1. \<And>parent nodea. \<lbrakk>m p = Some (CTE cap node); m src = Some (CTE src_cap src_node); m src = Some (CTE parent nodea); global.sameRegionAs parent c'; (\<exists>irq. c' = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. m p \<noteq> Some (CTE c' n'))\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c' cap
 2. \<And>parent nodea. \<lbrakk>m p = Some (CTE cap node); m src = Some (CTE src_cap src_node); m src = Some (CTE parent nodea); global.sameRegionAs parent c'; isUntypedCap parent \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits parent\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c' cap proof (prove)
goal (2 subgoals):
 1. \<And>parent node. \<lbrakk>m src = Some (CTE src_cap src_node); m src = Some (CTE parent node); global.sameRegionAs parent c'; (\<exists>irq. c' = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. m p \<noteq> Some (CTE c' n'))\<rbrakk> \<Longrightarrow> isIRQControlCap src_cap
 2. \<And>parent nodea. \<lbrakk>m p = Some (CTE cap node); m src = Some (CTE src_cap src_node); m src = Some (CTE parent nodea); global.sameRegionAs parent c'; isUntypedCap parent \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits parent\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c' cap proof (prove)
goal (1 subgoal):
 1. \<And>parent nodea. \<lbrakk>m p = Some (CTE cap node); m src = Some (CTE src_cap src_node); m src = Some (CTE parent nodea); global.sameRegionAs parent c'; isUntypedCap parent \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits parent\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c' cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); m src = Some (CTE src_cap src_node); isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); m src = Some (CTE src_cap src_node); descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; global.sameRegionAs c' cap; \<not> global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!