theory Retype_R

lemma retype_aligned_distinct':
  assumes vs': "pspace_aligned' s'" "pspace_distinct' s'"
      and pn': "pspace_no_overlap' ptr sz s'"
      and cover: "range_cover ptr sz (objBitsKO ko) n "
  shows
  "pspace_distinct' (s' \<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko)
                                             (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>)"
  "pspace_aligned' (s' \<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko)
                                             (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>)"
  (is "pspace_aligned' (s'\<lparr>ksPSpace := ?ps\<rparr>)") proof - have al: "is_aligned ptr (objBitsKO ko)" using cover by (simp add:cover range_cover_def) let ?s' = "s'\<lparr>ksPSpace := ?ps\<rparr>" note nc_al = bspec [OF new_cap_addrs_aligned [OF al]] note nc_al' = nc_al[unfolded objBits_def] show pa': "pspace_aligned' ?s'" using vs'(1) apply (subst foldr_upd_app_if[folded data_map_insert_def]) apply (clarsimp simp add: pspace_aligned'_def nc_al'
                       split: if_split_asm) apply (drule bspec, erule domI, simp) done have okov: "objBitsKO ko < word_bits" by (simp add: objBits_def) have new_range_disjoint:
    "\<And>x. x \<in> set (new_cap_addrs n ptr ko) \<Longrightarrow>
         ({x .. x + 2 ^ (objBitsKO ko) - 1} - {x}) \<inter> set (new_cap_addrs n ptr ko) = {}" apply safe apply (rule ccontr) apply (frule(2) aligned_neq_into_no_overlap [OF _ nc_al nc_al]) apply (drule_tac a=xa in equals0D) apply (clarsimp simp: field_simps is_aligned_no_overflow [OF nc_al]) done note new_range_sub = new_range_subset [OF cover] show pd': "pspace_distinct' ?s'" using vs'(2) apply (subst foldr_upd_app_if[folded data_map_insert_def]) apply (simp add: pspace_distinct'_def dom_if_Some ball_Un) apply (intro conjI ballI impI) apply (simp add: ps_clear_def dom_if_Some Int_Un_distrib
                       objBits_def[symmetric]) apply (rule conjI) apply (erule new_range_disjoint) apply (rule disjoint_subset[OF Diff_subset]) apply (erule disjoint_subset[OF new_range_sub]) apply (rule pspace_no_overlap_disjoint'[OF vs'(1) pn']) apply (clarsimp simp add: ps_clear_def dom_if_Some Int_Un_distrib) apply (rule conjI) apply (erule new_range_disjoint) apply (rule disjoint_subset[OF Diff_subset]) apply (erule disjoint_subset[OF new_range_sub]) apply (rule pspace_no_overlap_disjoint'[OF vs'(1) pn']) apply (clarsimp simp add: ps_clear_def dom_if_Some Int_Un_distrib) apply (subst Int_commute) apply (rule disjoint_subset[OF new_cap_addrs_subset,OF cover]) apply (subst Int_commute) apply (simp add:ptr_add_def field_simps) apply (rule disjoint_subset[OF Diff_subset]) apply (erule pspace_no_overlapD' [OF _ pn']) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) &&& pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (state)
goal (2 subgoals):
 1. pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>)
 2. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (prove)
goal (1 subgoal):
 1. is_aligned ptr (objBitsKO ko) proof (prove)
using this:
range_cover ptr sz (objBitsKO ko) n

goal (1 subgoal):
 1. is_aligned ptr (objBitsKO ko) proof (state)
this:
is_aligned ptr (objBitsKO ko)

goal (2 subgoals):
 1. pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>)
 2. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (state)
goal (2 subgoals):
 1. pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>)
 2. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (state)
this:
?x \<in> set (new_cap_addrs ?n1 ptr ko) \<Longrightarrow> is_aligned ?x (objBitsKO ko)

goal (2 subgoals):
 1. pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>)
 2. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (state)
this:
?x \<in> set (new_cap_addrs ?n1 ptr ko) \<Longrightarrow> is_aligned ?x (objBitsKO ko)

goal (2 subgoals):
 1. pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>)
 2. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (prove)
goal (1 subgoal):
 1. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (prove)
using this:
pspace_aligned' s'

goal (1 subgoal):
 1. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (prove)
goal (1 subgoal):
 1. pspace_aligned' s' \<Longrightarrow> pspace_aligned' (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). is_aligned x (objBitsKO (the (ksPSpace s' x))); ksPSpace s' x = Some y; x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO y) proof (prove)
goal:
No subgoals! proof (state)
this:
pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>)

goal (1 subgoal):
 1. pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (prove)
goal (1 subgoal):
 1. objBitsKO ko < word_bits proof (state)
this:
objBitsKO ko < word_bits

goal (1 subgoal):
 1. pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (new_cap_addrs n ptr ko) \<Longrightarrow> ({x..x + 2 ^ objBitsKO ko - 1} - {x}) \<inter> set (new_cap_addrs n ptr ko) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> set (new_cap_addrs n ptr ko); xa \<in> set (new_cap_addrs n ptr ko); xa \<in> {x..x + 2 ^ objBitsKO ko - 1}; xa \<notin> {}; xa \<notin> {}\<rbrakk> \<Longrightarrow> xa = x proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> set (new_cap_addrs n ptr ko); xa \<in> set (new_cap_addrs n ptr ko); xa \<in> {x..x + 2 ^ objBitsKO ko - 1}; xa \<notin> {}; xa \<notin> {}; xa \<noteq> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> set (new_cap_addrs n ptr ko); xa \<in> set (new_cap_addrs n ptr ko); xa \<in> {x..x + 2 ^ objBitsKO ko - 1}; xa \<notin> {}; xa \<notin> {}; xa \<noteq> x; {xa..xa + (2 ^ objBitsKO ko - 1)} \<inter> {x..x + (2 ^ objBitsKO ko - 1)} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> set (new_cap_addrs n ptr ko); xa \<in> set (new_cap_addrs n ptr ko); xa \<in> {x..x + 2 ^ objBitsKO ko - 1}; xa \<notin> {}; xa \<notin> {}; xa \<noteq> x; xa \<notin> {xa..xa + (2 ^ objBitsKO ko - 1)} \<inter> {x..x + (2 ^ objBitsKO ko - 1)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
?x \<in> set (new_cap_addrs n ptr ko) \<Longrightarrow> ({?x..?x + 2 ^ objBitsKO ko - 1} - {?x}) \<inter> set (new_cap_addrs n ptr ko) = {}

goal (1 subgoal):
 1. pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (state)
this:
?x \<in> set (new_cap_addrs n ptr ko) \<Longrightarrow> {?x..?x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}

goal (1 subgoal):
 1. pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (prove)
goal (1 subgoal):
 1. pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (prove)
using this:
pspace_distinct' s'

goal (1 subgoal):
 1. pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>) proof (prove)
goal (1 subgoal):
 1. pspace_distinct' s' \<Longrightarrow> pspace_distinct' (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s' \<Longrightarrow> (\<forall>x\<in>set (new_cap_addrs n ptr ko). ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>)) \<and> (\<forall>x\<in>dom (ksPSpace s'). (x \<in> set (new_cap_addrs n ptr ko) \<longrightarrow> ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>)) \<and> (x \<notin> set (new_cap_addrs n ptr ko) \<longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>))) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>)
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>)
 3. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ({x..x + 2 ^ objBitsKO ko - 1} - {x}) \<inter> set (new_cap_addrs n ptr ko) = {} \<and> ({x..x + 2 ^ objBitsKO ko - 1} - {x}) \<inter> dom (ksPSpace s') = {}
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>)
 3. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ({x..x + 2 ^ objBitsKO ko - 1} - {x}) \<inter> set (new_cap_addrs n ptr ko) = {}
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ({x..x + 2 ^ objBitsKO ko - 1} - {x}) \<inter> dom (ksPSpace s') = {}
 3. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>)
 4. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ({x..x + 2 ^ objBitsKO ko - 1} - {x}) \<inter> dom (ksPSpace s') = {}
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>)
 3. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> dom (ksPSpace s') = {}
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>)
 3. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {} \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s') = {}
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>)
 3. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<in> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>)
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<in> set (new_cap_addrs n ptr ko); ksPSpace s' x = Some y\<rbrakk> \<Longrightarrow> ({x..x + 2 ^ objBitsKO ko - 1} - {x}) \<inter> set (new_cap_addrs n ptr ko) = {} \<and> ({x..x + 2 ^ objBitsKO ko - 1} - {x}) \<inter> dom (ksPSpace s') = {}
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<in> set (new_cap_addrs n ptr ko); ksPSpace s' x = Some y\<rbrakk> \<Longrightarrow> ({x..x + 2 ^ objBitsKO ko - 1} - {x}) \<inter> set (new_cap_addrs n ptr ko) = {}
 2. \<And>x y. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<in> set (new_cap_addrs n ptr ko); ksPSpace s' x = Some y\<rbrakk> \<Longrightarrow> ({x..x + 2 ^ objBitsKO ko - 1} - {x}) \<inter> dom (ksPSpace s') = {}
 3. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<in> set (new_cap_addrs n ptr ko); ksPSpace s' x = Some y\<rbrakk> \<Longrightarrow> ({x..x + 2 ^ objBitsKO ko - 1} - {x}) \<inter> dom (ksPSpace s') = {}
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<in> set (new_cap_addrs n ptr ko); ksPSpace s' x = Some y\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> dom (ksPSpace s') = {}
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; ksPSpace s' x = Some y\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s') = {}
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ps_clear x (objBitsKO (the (ksPSpace s' x))) s'; x \<in> dom (ksPSpace s'); x \<notin> set (new_cap_addrs n ptr ko)\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace s' x))) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace s' x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<notin> set (new_cap_addrs n ptr ko); ksPSpace s' x = Some y\<rbrakk> \<Longrightarrow> ({x..x + 2 ^ objBitsKO y - 1} - {x}) \<inter> set (new_cap_addrs n ptr ko) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<notin> set (new_cap_addrs n ptr ko); ksPSpace s' x = Some y\<rbrakk> \<Longrightarrow> set (new_cap_addrs n ptr ko) \<inter> ({x..x + 2 ^ objBitsKO y - 1} - {x}) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<notin> set (new_cap_addrs n ptr ko); ksPSpace s' x = Some y\<rbrakk> \<Longrightarrow> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)} \<inter> ({x..x + 2 ^ objBitsKO y - 1} - {x}) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<notin> set (new_cap_addrs n ptr ko); ksPSpace s' x = Some y\<rbrakk> \<Longrightarrow> ({x..x + 2 ^ objBitsKO y - 1} - {x}) \<inter> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<notin> set (new_cap_addrs n ptr ko); ksPSpace s' x = Some y\<rbrakk> \<Longrightarrow> ({x..x + 2 ^ objBitsKO y - 1} - {x}) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom (ksPSpace s'). ({x..x + 2 ^ objBitsKO (the (ksPSpace s' x)) - 1} - {x}) \<inter> dom (ksPSpace s') = {}; x \<notin> set (new_cap_addrs n ptr ko); ksPSpace s' x = Some y\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO y - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal:
No subgoals! proof (state)
this:
pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs n ptr ko) (ksPSpace s')\<rparr>)

goal:
No subgoals!