theory Detype_R

lemma detype_pspace_relation:
  assumes psp: "pspace_relation (kheap s) (ksPSpace s')"
  and     bwb: "bits < word_bits"
  and      al: "is_aligned base bits"
  and      vs: "valid_pspace s"
  and      vu: "valid_untyped (cap.UntypedCap d base bits idx) s"
  shows        "pspace_relation (kheap (detype {base .. base + 2 ^ bits - 1} s))
                 (\<lambda>x. if x \<in> {base .. base + 2 ^ bits - 1} then None else ksPSpace s' x)"
  (is "pspace_relation ?ps ?ps'") proof - let ?range = "{base .. base + 2 ^ bits - 1}" let ?ps'' = "(kheap s |` (-?range))" have pa: "pspace_aligned s" and vo: "valid_objs s" using vs by (simp add: valid_pspace_def)+ have pspace:
    "\<And>x. \<lbrakk> x \<notin> ?range; x \<in> dom (kheap s) \<rbrakk> \<Longrightarrow> ?ps x = kheap s x" by (clarsimp simp add: detype_def field_simps) have pspace'':
    "\<And>x. \<lbrakk> x \<notin> ?range; x \<in> dom (kheap s) \<rbrakk> \<Longrightarrow> ?ps'' x = kheap s x" by (clarsimp simp add: detype_def) have psdom_pre: "dom ?ps = (dom (kheap s) - ?range)" by (fastforce simp:field_simps) show ?thesis unfolding pspace_relation_def proof (intro conjI) have domeq': "dom (ksPSpace s') = pspace_dom (kheap s)" using psp by (simp add: pspace_relation_def) note eqv_base_in = obj_relation_cuts_eqv_base_in_detype_range
                          [OF _ _ vo pa vu] note atLeastAtMost_iff[simp del] show domeq: "pspace_dom ?ps = dom ?ps'" apply (simp add: dom_if_None domeq') apply (simp add: pspace_dom_def detype_def dom_if_None) apply (intro set_eqI iffI, simp_all) apply (clarsimp simp: eqv_base_in field_simps) apply (rule rev_bexI, erule domI) apply (simp add: image_def, erule rev_bexI, simp) apply (elim exE bexE DiffE conjE domE) apply (rule bexI, assumption) apply (clarsimp simp add: eqv_base_in field_simps) done show "\<forall>x\<in>dom ?ps.
       \<forall>(y, P)\<in>obj_relation_cuts (the (?ps x)) x.
          P (the (?ps x))
           (the (if y \<in> ?range then None else ksPSpace s' y))" using psp apply (simp add: pspace_relation_def psdom_pre split del: if_split) apply (erule conjE, rule ballI, erule DiffE, drule(1) bspec) apply (erule domE) apply (simp add: field_simps detype_def cong: conj_cong) apply (erule ballEI, clarsimp) apply (simp add: eqv_base_in) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_relation (kheap (detype {base..base + 2 ^ bits - 1} s)) (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x) proof (state)
goal (1 subgoal):
 1. pspace_relation (kheap (detype {base..base + 2 ^ bits - 1} s)) (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x) proof (state)
goal (1 subgoal):
 1. pspace_relation (kheap (detype {base..base + 2 ^ bits - 1} s)) (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x) proof (state)
goal (1 subgoal):
 1. pspace_relation (kheap (detype {base..base + 2 ^ bits - 1} s)) (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x) proof (prove)
goal (1 subgoal):
 1. pspace_aligned s &&& valid_objs s proof (prove)
using this:
valid_pspace s

goal (1 subgoal):
 1. pspace_aligned s &&& valid_objs s proof (state)
this:
pspace_aligned s
valid_objs s

goal (1 subgoal):
 1. pspace_relation (kheap (detype {base..base + 2 ^ bits - 1} s)) (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<notin> {base..base + 2 ^ bits - 1}; x \<in> dom (kheap s)\<rbrakk> \<Longrightarrow> kheap (detype {base..base + 2 ^ bits - 1} s) x = kheap s x proof (state)
this:
\<lbrakk>?x \<notin> {base..base + 2 ^ bits - 1}; ?x \<in> dom (kheap s)\<rbrakk> \<Longrightarrow> kheap (detype {base..base + 2 ^ bits - 1} s) ?x = kheap s ?x

goal (1 subgoal):
 1. pspace_relation (kheap (detype {base..base + 2 ^ bits - 1} s)) (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<notin> {base..base + 2 ^ bits - 1}; x \<in> dom (kheap s)\<rbrakk> \<Longrightarrow> (kheap s |` (- {base..base + 2 ^ bits - 1})) x = kheap s x proof (state)
this:
\<lbrakk>?x \<notin> {base..base + 2 ^ bits - 1}; ?x \<in> dom (kheap s)\<rbrakk> \<Longrightarrow> (kheap s |` (- {base..base + 2 ^ bits - 1})) ?x = kheap s ?x

goal (1 subgoal):
 1. pspace_relation (kheap (detype {base..base + 2 ^ bits - 1} s)) (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x) proof (prove)
goal (1 subgoal):
 1. dom (kheap (detype {base..base + 2 ^ bits - 1} s)) = dom (kheap s) - {base..base + 2 ^ bits - 1} proof (state)
this:
dom (kheap (detype {base..base + 2 ^ bits - 1} s)) = dom (kheap s) - {base..base + 2 ^ bits - 1}

goal (1 subgoal):
 1. pspace_relation (kheap (detype {base..base + 2 ^ bits - 1} s)) (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x) proof (prove)
goal (1 subgoal):
 1. pspace_relation (kheap (detype {base..base + 2 ^ bits - 1} s)) (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x) proof (prove)
goal (1 subgoal):
 1. pspace_dom (kheap (detype {base..base + 2 ^ bits - 1} s)) = dom (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x) \<and> (\<forall>x\<in>dom (kheap (detype {base..base + 2 ^ bits - 1} s)). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) x. P (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) (the (if y \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' y))) proof (state)
goal (2 subgoals):
 1. pspace_dom (kheap (detype {base..base + 2 ^ bits - 1} s)) = dom (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x)
 2. \<forall>x\<in>dom (kheap (detype {base..base + 2 ^ bits - 1} s)). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) x. P (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) (the (if y \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' y)) proof (prove)
goal (1 subgoal):
 1. dom (ksPSpace s') = pspace_dom (kheap s) proof (prove)
using this:
pspace_relation (kheap s) (ksPSpace s')

goal (1 subgoal):
 1. dom (ksPSpace s') = pspace_dom (kheap s) proof (state)
this:
dom (ksPSpace s') = pspace_dom (kheap s)

goal (2 subgoals):
 1. pspace_dom (kheap (detype {base..base + 2 ^ bits - 1} s)) = dom (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x)
 2. \<forall>x\<in>dom (kheap (detype {base..base + 2 ^ bits - 1} s)). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) x. P (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) (the (if y \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' y)) proof (state)
this:
\<lbrakk>(?y, ?P) \<in> obj_relation_cuts ?ko ?x; kheap s ?x = Some ?ko\<rbrakk> \<Longrightarrow> (?x \<in> {base..base + 2 ^ bits - 1}) = (?y \<in> {base..base + 2 ^ bits - 1})

goal (2 subgoals):
 1. pspace_dom (kheap (detype {base..base + 2 ^ bits - 1} s)) = dom (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x)
 2. \<forall>x\<in>dom (kheap (detype {base..base + 2 ^ bits - 1} s)). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) x. P (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) (the (if y \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' y)) proof (state)
this:
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)

goal (2 subgoals):
 1. pspace_dom (kheap (detype {base..base + 2 ^ bits - 1} s)) = dom (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x)
 2. \<forall>x\<in>dom (kheap (detype {base..base + 2 ^ bits - 1} s)). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) x. P (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) (the (if y \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' y)) proof (prove)
goal (1 subgoal):
 1. pspace_dom (kheap (detype {base..base + 2 ^ bits - 1} s)) = dom (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x) proof (prove)
goal (1 subgoal):
 1. pspace_dom (kheap (detype {base..base + 2 ^ bits - 1} s)) = pspace_dom (kheap s) - {base..base + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>dom (kheap s) - {base..base + 2 ^ bits - 1}. fst ` obj_relation_cuts (the (kheap s x)) x) = (\<Union>x\<in>dom (kheap s). fst ` obj_relation_cuts (the (kheap s x)) x) - {base..base + 2 ^ bits - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>xa\<in>dom (kheap s) - {base..base + 2 ^ bits - 1}. x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa \<Longrightarrow> (\<exists>xa\<in>dom (kheap s). x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa) \<and> x \<notin> {base..base + 2 ^ bits - 1}
 2. \<And>x. (\<exists>xa\<in>dom (kheap s). x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa) \<and> x \<notin> {base..base + 2 ^ bits - 1} \<Longrightarrow> \<exists>xa\<in>dom (kheap s) - {base..base + 2 ^ bits - 1}. x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa proof (prove)
goal (2 subgoals):
 1. \<And>xa a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y xa; a \<notin> {base..base + 2 ^ bits - 1}; kheap s xa = Some y\<rbrakk> \<Longrightarrow> \<exists>x\<in>dom (kheap s). a \<in> fst ` obj_relation_cuts (the (kheap s x)) x
 2. \<And>x. (\<exists>xa\<in>dom (kheap s). x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa) \<and> x \<notin> {base..base + 2 ^ bits - 1} \<Longrightarrow> \<exists>xa\<in>dom (kheap s) - {base..base + 2 ^ bits - 1}. x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa proof (prove)
goal (2 subgoals):
 1. \<And>xa a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y xa; a \<notin> {base..base + 2 ^ bits - 1}; kheap s xa = Some y\<rbrakk> \<Longrightarrow> a \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa
 2. \<And>x. (\<exists>xa\<in>dom (kheap s). x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa) \<and> x \<notin> {base..base + 2 ^ bits - 1} \<Longrightarrow> \<exists>xa\<in>dom (kheap s) - {base..base + 2 ^ bits - 1}. x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<exists>xa\<in>dom (kheap s). x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa) \<and> x \<notin> {base..base + 2 ^ bits - 1} \<Longrightarrow> \<exists>xa\<in>dom (kheap s) - {base..base + 2 ^ bits - 1}. x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa r. \<lbrakk>x \<notin> {base..base + 2 ^ bits - 1}; x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa; kheap s xa = Some r\<rbrakk> \<Longrightarrow> \<exists>xa\<in>dom (kheap s) - {base..base + 2 ^ bits - 1}. x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa r. \<lbrakk>x \<notin> {base..base + 2 ^ bits - 1}; x \<in> fst ` obj_relation_cuts (the (kheap s xa)) xa; kheap s xa = Some r\<rbrakk> \<Longrightarrow> xa \<in> dom (kheap s) - {base..base + 2 ^ bits - 1} proof (prove)
goal:
No subgoals! proof (state)
this:
pspace_dom (kheap (detype {base..base + 2 ^ bits - 1} s)) = dom (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x)

goal (1 subgoal):
 1. \<forall>x\<in>dom (kheap (detype {base..base + 2 ^ bits - 1} s)). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) x. P (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) (the (if y \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' y)) proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>dom (kheap (detype {base..base + 2 ^ bits - 1} s)). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) x. P (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) (the (if y \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' y)) proof (prove)
using this:
pspace_relation (kheap s) (ksPSpace s')

goal (1 subgoal):
 1. \<forall>x\<in>dom (kheap (detype {base..base + 2 ^ bits - 1} s)). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) x. P (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) (the (if y \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' y)) proof (prove)
goal (1 subgoal):
 1. pspace_dom (kheap s) = dom (ksPSpace s') \<and> (\<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))) \<Longrightarrow> \<forall>x\<in>dom (kheap s) - {base..base + 2 ^ bits - 1}. \<forall>xa\<in>obj_relation_cuts (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) (the (if y \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' y)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); x \<in> dom (kheap s); x \<notin> {base..base + 2 ^ bits - 1}; \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))\<rbrakk> \<Longrightarrow> \<forall>xa\<in>obj_relation_cuts (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) (the (if y \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' y)) proof (prove)
goal (1 subgoal):
 1. \<And>x r. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); x \<notin> {base..base + 2 ^ bits - 1}; \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); kheap s x = Some r\<rbrakk> \<Longrightarrow> \<forall>xa\<in>obj_relation_cuts (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) (the (if y \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' y)) proof (prove)
goal (1 subgoal):
 1. \<And>x r. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); x \<notin> {base..base + 2 ^ bits - 1}; \<forall>x\<in>obj_relation_cuts r x. case x of (y, P) \<Rightarrow> P r (the (ksPSpace s' y)); kheap s x = Some r\<rbrakk> \<Longrightarrow> \<forall>x\<in>obj_relation_cuts r x. case x of (y, P) \<Rightarrow> P r (the (if y \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' y)) proof (prove)
goal (1 subgoal):
 1. \<And>x r a b. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); x \<notin> {base..base + 2 ^ bits - 1}; kheap s x = Some r; (a, b) \<in> obj_relation_cuts r x; b r (the (ksPSpace s' a)); a \<in> {base..base + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> b r (the None) proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>x\<in>dom (kheap (detype {base..base + 2 ^ bits - 1} s)). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) x. P (the (kheap (detype {base..base + 2 ^ bits - 1} s) x)) (the (if y \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' y))

goal:
No subgoals! proof (state)
this:
pspace_relation (kheap (detype {base..base + 2 ^ bits - 1} s)) (\<lambda>x. if x \<in> {base..base + 2 ^ bits - 1} then None else ksPSpace s' x)

goal:
No subgoals!