theory Detype_R

lemma objRefs_notrange:
  assumes asms: "ctes_of s p = Some c" "\<not> isUntypedCap (cteCap c)"
  shows "capRange (cteCap c) \<inter> base_bits = {}" proof - from cap obtain node
    where ctes_of: "ctes_of s ptr = Some (CTE (UntypedCap d base bits idx) node)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done show ?thesis using asms cap apply - apply (rule ccontr) apply (drule untyped_mdbD' [OF ctes_of _ _ _ _ umdb]) apply (simp add: isUntypedCap_def) apply (simp add: field_simps) apply assumption using nodesc apply (simp add:descendants_range'_def2) apply (drule(1) descendants_range_inD') apply (simp add:asms) apply (simp add:p_assoc_help) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capRange (cteCap c) \<inter> base_bits = {} proof (state)
goal (1 subgoal):
 1. capRange (cteCap c) \<inter> base_bits = {} proof (chain)
picking this:
cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s proof (prove)
using this:
cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s

goal (1 subgoal):
 1. (\<And>node. ctes_of s ptr = Some (CTE (capability.UntypedCap d base bits idx) node) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>\<And>node. cte = CTE (capability.UntypedCap d base bits idx) node \<Longrightarrow> thesis; ctes_of s ptr = Some cte; cteCap cte = capability.UntypedCap d base bits idx\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal:
No subgoals! proof (state)
this:
ctes_of s ptr = Some (CTE (capability.UntypedCap d base bits idx) node)

goal (1 subgoal):
 1. capRange (cteCap c) \<inter> base_bits = {} proof (prove)
goal (1 subgoal):
 1. capRange (cteCap c) \<inter> base_bits = {} proof (prove)
using this:
ctes_of s p = Some c
\<not> isUntypedCap (cteCap c)
cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s

goal (1 subgoal):
 1. capRange (cteCap c) \<inter> base_bits = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some c; \<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s\<rbrakk> \<Longrightarrow> capRange (cteCap c) \<inter> base_bits = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some c; \<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap (CTE (capability.UntypedCap d base bits idx) node))
 2. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}\<rbrakk> \<Longrightarrow> capRange (cteCap c) \<inter> untypedRange (cteCap (CTE (capability.UntypedCap d base bits idx) node)) \<noteq> {}
 3. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap c)
 4. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}; p \<in> descendants_of' ptr (ctes_of s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}\<rbrakk> \<Longrightarrow> capRange (cteCap c) \<inter> untypedRange (cteCap (CTE (capability.UntypedCap d base bits idx) node)) \<noteq> {}
 2. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap c)
 3. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}; p \<in> descendants_of' ptr (ctes_of s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap c)
 2. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}; p \<in> descendants_of' ptr (ctes_of s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}; p \<in> descendants_of' ptr (ctes_of s)\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
descendants_range' (capability.UntypedCap d base bits idx) ptr (ctes_of s)

goal (1 subgoal):
 1. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}; p \<in> descendants_of' ptr (ctes_of s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}; p \<in> descendants_of' ptr (ctes_of s); descendants_range_in' {base..base + 2 ^ bits - 1} ptr (ctes_of s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}; p \<in> descendants_of' ptr (ctes_of s)\<rbrakk> \<Longrightarrow> ctes_of s p = Some ?cte11
 2. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}; p \<in> descendants_of' ptr (ctes_of s); capRange (cteCap ?cte11) \<inter> {base..base + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> isUntypedCap (cteCap c); cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s; capRange (cteCap c) \<inter> base_bits \<noteq> {}; p \<in> descendants_of' ptr (ctes_of s); capRange (cteCap c) \<inter> {base..base + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
capRange (cteCap c) \<inter> base_bits = {}

goal:
No subgoals!