theory Detype_R

lemma pspace_no_overlap'_le2:
  assumes "pspace_no_overlap' ptr sz s" "ptr \<le> ptr'"  "ptr' &&~~ mask sz = ptr && ~~ mask sz"
  shows "pspace_no_overlap' ptr' sz s" proof - note blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex show ?thesis using assms apply (clarsimp simp:pspace_no_overlap'_def) apply (drule_tac x = x in spec) apply clarsimp apply (erule disjoint_subset2[rotated]) apply (clarsimp simp:blah) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap' ptr' sz s proof (state)
goal (1 subgoal):
 1. pspace_no_overlap' ptr' sz s proof (state)
this:
untyped_range (cap.UntypedCap ?dev ?p ?n ?f) = {?p..?p + (1 << ?n) - 1}
untyped_range cap.NullCap = {}
untyped_range (cap.EndpointCap ?r ?badge ?rights) = {}
untyped_range (cap.NotificationCap ?r ?badge ?rights) = {}
untyped_range (cap.CNodeCap ?r ?bits ?guard) = {}
untyped_range (cap.ThreadCap ?r) = {}
untyped_range cap.DomainCap = {}
untyped_range (cap.ReplyCap ?r ?master ?rights) = {}
untyped_range cap.IRQControlCap = {}
untyped_range (cap.IRQHandlerCap ?irq) = {}
untyped_range (cap.Zombie ?r ?b ?n) = {}
untyped_range (cap.ArchObjectCap ?cap) = {}
usable_untyped_range (cap.UntypedCap ?uu ?p ?n ?f) = (if ?f < 2 ^ ?n then {?p + word_of_nat ?f..?p + 2 ^ ?n - 1} else {})
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)
({?a..?b} \<subseteq> {?c..?d}) = (\<not> ?a \<le> ?b \<or> ?c \<le> ?a \<and> ?b \<le> ?d)
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
{?a..?b} \<inter> {?c..?d} = {max ?a ?c..min ?b ?d}
({?a..?b} = {}) = (\<not> ?a \<le> ?b)
(\<exists>x. ?P x) = (\<exists>a b. ?P (a, b))

goal (1 subgoal):
 1. pspace_no_overlap' ptr' sz s proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap' ptr' sz s proof (prove)
using this:
pspace_no_overlap' ptr sz s
ptr \<le> ptr'
ptr' && ~~ mask sz = ptr && ~~ mask sz

goal (1 subgoal):
 1. pspace_no_overlap' ptr' sz s proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>\<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr sz = {}; ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr'..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; ksPSpace s x = Some ko; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr sz = {}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr'..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; ksPSpace s x = Some ko; {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr sz = {}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr'..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>ptr \<le> ptr'; ptr' && ~~ mask sz = ptr && ~~ mask sz; ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {ptr'..(ptr && ~~ mask sz) + (2 ^ sz - 1)} \<subseteq> up_aligned_area ptr sz proof (prove)
goal:
No subgoals! proof (state)
this:
pspace_no_overlap' ptr' sz s

goal:
No subgoals!