theory CSpace_R

lemma usableUntypedRange_uniq:
  "cteCaps_of s x = Some cp
    \<Longrightarrow> cteCaps_of s y = Some cp'
    \<Longrightarrow> isUntypedCap cp
    \<Longrightarrow> isUntypedCap cp'
    \<Longrightarrow> capAligned cp
    \<Longrightarrow> capAligned cp'
    \<Longrightarrow> untyped_inc' (ctes_of s)
    \<Longrightarrow> usableUntypedRange cp = usableUntypedRange cp'
    \<Longrightarrow> usableUntypedRange cp \<noteq> {}
    \<Longrightarrow> x = y" apply (cases "the (ctes_of s x)") apply (cases "the (ctes_of s y)") apply (clarsimp simp: cteCaps_of_def) apply (frule untyped_incD'[where p=x and p'=y], simp+) apply (drule(1) usableRange_subseteq)+ apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cteCaps_of s x = Some cp; cteCaps_of s y = Some cp'; isUntypedCap cp; isUntypedCap cp'; capAligned cp; capAligned cp'; untyped_inc' (ctes_of s); usableUntypedRange cp = usableUntypedRange cp'; usableUntypedRange cp \<noteq> {}\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>cteCaps_of s x = Some cp; cteCaps_of s y = Some cp'; isUntypedCap cp; isUntypedCap cp'; capAligned cp; capAligned cp'; untyped_inc' (ctes_of s); usableUntypedRange cp = usableUntypedRange cp'; usableUntypedRange cp \<noteq> {}; the (ctes_of s x) = CTE x1 x2\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cteCaps_of s x = Some cp; cteCaps_of s y = Some cp'; isUntypedCap cp; isUntypedCap cp'; capAligned cp; capAligned cp'; untyped_inc' (ctes_of s); usableUntypedRange cp = usableUntypedRange cp'; usableUntypedRange cp \<noteq> {}; the (ctes_of s x) = CTE x1 x2; the (ctes_of s y) = CTE x1a x2a\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a. \<lbrakk>isUntypedCap cp; isUntypedCap cp'; capAligned cp; capAligned cp'; untyped_inc' (ctes_of s); usableUntypedRange cp = usableUntypedRange cp'; usableUntypedRange cp' \<noteq> {}; ctes_of s x = Some (CTE cp x2); ctes_of s y = Some (CTE cp' x2a)\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a. \<lbrakk>isUntypedCap cp; isUntypedCap cp'; capAligned cp; capAligned cp'; untyped_inc' (ctes_of s); usableUntypedRange cp = usableUntypedRange cp'; usableUntypedRange cp' \<noteq> {}; ctes_of s x = Some (CTE cp x2); ctes_of s y = Some (CTE cp' x2a); (untypedRange cp \<subseteq> untypedRange cp' \<or> untypedRange cp' \<subseteq> untypedRange cp \<or> untypedRange cp \<inter> untypedRange cp' = {}) \<and> (untypedRange cp \<subset> untypedRange cp' \<longrightarrow> x \<in> descendants_of' y (ctes_of s) \<and> untypedRange cp \<inter> usableUntypedRange cp' = {}) \<and> (untypedRange cp' \<subset> untypedRange cp \<longrightarrow> y \<in> descendants_of' x (ctes_of s) \<and> untypedRange cp' \<inter> usableUntypedRange cp' = {}) \<and> (untypedRange cp = untypedRange cp' \<longrightarrow> x = y)\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a. \<lbrakk>isUntypedCap cp; isUntypedCap cp'; untyped_inc' (ctes_of s); usableUntypedRange cp = usableUntypedRange cp'; usableUntypedRange cp' \<noteq> {}; ctes_of s x = Some (CTE cp x2); ctes_of s y = Some (CTE cp' x2a); (untypedRange cp \<subseteq> untypedRange cp' \<or> untypedRange cp' \<subseteq> untypedRange cp \<or> untypedRange cp \<inter> untypedRange cp' = {}) \<and> (untypedRange cp \<subset> untypedRange cp' \<longrightarrow> x \<in> descendants_of' y (ctes_of s) \<and> untypedRange cp \<inter> usableUntypedRange cp' = {}) \<and> (untypedRange cp' \<subset> untypedRange cp \<longrightarrow> y \<in> descendants_of' x (ctes_of s) \<and> untypedRange cp' \<inter> usableUntypedRange cp' = {}) \<and> (untypedRange cp = untypedRange cp' \<longrightarrow> x = y); usableUntypedRange cp \<subseteq> untypedRange cp; usableUntypedRange cp' \<subseteq> untypedRange cp'\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal:
No subgoals!