theory Retype_AI

lemma pspace_no_overlap_into_Int_none:
  assumes ps: "pspace_no_overlap_range_cover ptr sz s"
  and     vp: "valid_pspace s"
  and  cover: "range_cover ptr sz (obj_bits_api ty us) n"
  shows   "set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {}" proof - { fix x ko assume ps': "kheap s x = Some ko" have "x \<notin> {ptr .. (ptr && ~~ mask sz) + (2 ^ sz - 1)}" proof (rule orthD1) show "x \<in> {x .. x + (2 ^ obj_bits ko - 1)}" proof (rule base_member_set) from vp show "is_aligned x (obj_bits ko)" using ps' by (auto elim!: valid_pspaceE) show "obj_bits ko < len_of TYPE(machine_word_len)" by (rule valid_pspace_obj_sizes [OF _ ranI, unfolded word_bits_def]) fact+ qed show "{x..x + (2 ^ obj_bits ko - 1)} \<inter> {ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}" using ps by (rule pspace_no_overlapE) fact+ qed hence "x \<notin> set (retype_addrs ptr ty n us)" using assms subsetD[OF retype_addrs_subset_ptr_bits[OF cover]] by auto } thus ?thesis by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {} proof (state)
goal (1 subgoal):
 1. set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {} proof (state)
goal (1 subgoal):
 1. set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {} proof (state)
goal (1 subgoal):
 1. set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {} proof (state)
this:
kheap s x = Some ko

goal (1 subgoal):
 1. set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {} proof (prove)
goal (1 subgoal):
 1. x \<notin> up_aligned_area ptr sz proof (state)
goal (2 subgoals):
 1. ?S \<inter> up_aligned_area ptr sz = {}
 2. x \<in> ?S proof (prove)
goal (1 subgoal):
 1. x \<in> {x..x + (2 ^ obj_bits ko - 1)} proof (state)
goal (2 subgoals):
 1. is_aligned x (obj_bits ko)
 2. obj_bits ko < LENGTH(32) proof (chain)
picking this:
valid_pspace s proof (prove)
using this:
valid_pspace s

goal (1 subgoal):
 1. is_aligned x (obj_bits ko) proof (prove)
using this:
valid_pspace s
kheap s x = Some ko

goal (1 subgoal):
 1. is_aligned x (obj_bits ko) proof (state)
this:
is_aligned x (obj_bits ko)

goal (1 subgoal):
 1. obj_bits ko < LENGTH(32) proof (prove)
goal (1 subgoal):
 1. obj_bits ko < LENGTH(32) proof (state)
this:
obj_bits ko < LENGTH(32)

goal:
No subgoals! proof (state)
this:
x \<in> {x..x + (2 ^ obj_bits ko - 1)}

goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits ko - 1)} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits ko - 1)} \<inter> up_aligned_area ptr sz = {} proof (prove)
using this:
pspace_no_overlap (up_aligned_area ptr sz) s

goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits ko - 1)} \<inter> up_aligned_area ptr sz = {} proof (state)
this:
{x..x + (2 ^ obj_bits ko - 1)} \<inter> up_aligned_area ptr sz = {}

goal:
No subgoals! proof (state)
this:
x \<notin> up_aligned_area ptr sz

goal (1 subgoal):
 1. set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {} proof (prove)
using this:
x \<notin> up_aligned_area ptr sz

goal (1 subgoal):
 1. x \<notin> set (retype_addrs ptr ty n us) proof (prove)
using this:
x \<notin> up_aligned_area ptr sz
pspace_no_overlap (up_aligned_area ptr sz) s
valid_pspace s
range_cover ptr sz (obj_bits_api ty us) n
?c \<in> set (retype_addrs ptr ty n us) \<Longrightarrow> ?c \<in> up_aligned_area ptr sz

goal (1 subgoal):
 1. x \<notin> set (retype_addrs ptr ty n us) proof (state)
this:
x \<notin> set (retype_addrs ptr ty n us)

goal (1 subgoal):
 1. set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {} proof (state)
this:
kheap s ?x2 = Some ?ko2 \<Longrightarrow> ?x2 \<notin> set (retype_addrs ptr ty n us)

goal (1 subgoal):
 1. set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {} proof (prove)
using this:
kheap s ?x2 = Some ?ko2 \<Longrightarrow> ?x2 \<notin> set (retype_addrs ptr ty n us)

goal (1 subgoal):
 1. set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {} proof (state)
this:
set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {}

goal:
No subgoals!