theory CSpace_R

lemma ut_src_only_ut_c_parents:
  "\<lbrakk> isUntypedCap src_cap; sameRegionAs cap c'; m p = Some (CTE cap node) \<rbrakk> \<Longrightarrow> isUntypedCap cap" using safe_parent src unfolding safe_parent_for'_def apply clarsimp apply (erule disjE, clarsimp simp: isCap_simps) apply clarsimp apply (rule ccontr) apply (drule (3) untyped_mdbD') apply (frule sameRegion_capRange_sub) apply (insert utCapRange_c')[1] apply blast apply (rule untyped_mdb) apply simp done

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

goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node)\<rbrakk> \<Longrightarrow> isUntypedCap 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. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node)\<rbrakk> \<Longrightarrow> isUntypedCap cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); (\<exists>irq. c' = capability.IRQHandlerCap irq) \<and> src_cap = capability.IRQControlCap \<and> (\<forall>p n'. m p \<noteq> Some (CTE c' n')) \<or> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits src_cap; m src = Some (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> isUntypedCap cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); m src = Some (CTE src_cap src_node); descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits src_cap\<rbrakk> \<Longrightarrow> isUntypedCap cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; 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\<rbrakk> \<Longrightarrow> isUntypedCap cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; 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; \<not> isUntypedCap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; \<not> isUntypedCap cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> untypedRange src_cap \<noteq> {}
 2. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; \<not> isUntypedCap cap\<rbrakk> \<Longrightarrow> untyped_mdb' m
 3. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; \<not> isUntypedCap cap; p \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; \<not> isUntypedCap cap; capRange c' \<subseteq> capRange cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> untypedRange src_cap \<noteq> {}
 2. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; \<not> isUntypedCap cap\<rbrakk> \<Longrightarrow> untyped_mdb' m
 3. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; \<not> isUntypedCap cap; p \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; \<not> isUntypedCap cap; capRange c' \<subseteq> capRange cap; capRange c' \<subseteq> untypedRange src_cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> untypedRange src_cap \<noteq> {}
 2. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; \<not> isUntypedCap cap\<rbrakk> \<Longrightarrow> untyped_mdb' m
 3. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; \<not> isUntypedCap cap; p \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; \<not> isUntypedCap cap\<rbrakk> \<Longrightarrow> untyped_mdb' m
 2. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; \<not> isUntypedCap cap; p \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); descendants_of' src m = {}; capRange c' \<noteq> {}; capBits c' \<le> capBits src_cap; \<not> isUntypedCap cap; p \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!