theory Detype_R

lemma ko_wp_at_delete':
  "pspace_distinct' s \<Longrightarrow>
   ko_wp_at' P p (s \<lparr> ksPSpace := \<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x \<rparr>)
    = (\<not> (base \<le> p \<and> p \<le> base + (2 ^ magnitude - 1)) \<and> ko_wp_at' P p s)" apply (simp add: ko_wp_at'_def projectKOs ps_clear_def dom_if_None) apply (intro impI iffI) apply clarsimp apply (drule(1) pspace_distinctD') apply (simp add: ps_clear_def) apply (clarsimp simp: Diff_Int_distrib) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_distinct' s \<Longrightarrow> ko_wp_at' P p (s\<lparr>ksPSpace := \<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x\<rparr>) = (\<not> (base \<le> p \<and> p \<le> base + (2 ^ magnitude - 1)) \<and> ko_wp_at' P p s) proof (prove)
goal (1 subgoal):
 1. pspace_distinct' s \<Longrightarrow> (base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1)) \<longrightarrow> (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> (dom (ksPSpace s) - {x. base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1)}) = {}) = (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> dom (ksPSpace s) = {}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_distinct' s; base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1); \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> (dom (ksPSpace s) - {x. base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1)}) = {}\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> dom (ksPSpace s) = {}
 2. \<lbrakk>pspace_distinct' s; base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1); \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> (dom (ksPSpace s) - {x. base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1)}) = {} proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>pspace_distinct' s; base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1); ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P ko; ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> (dom (ksPSpace s) - {x. base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1)}) = {}\<rbrakk> \<Longrightarrow> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> dom (ksPSpace s) = {}
 2. \<lbrakk>pspace_distinct' s; base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1); \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> (dom (ksPSpace s) - {x. base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1)}) = {} proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>pspace_distinct' s; base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1); is_aligned p (objBitsKO ko); P ko; ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> (dom (ksPSpace s) - {x. base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1)}) = {}; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> dom (ksPSpace s) = {}
 2. \<lbrakk>pspace_distinct' s; base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1); \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> (dom (ksPSpace s) - {x. base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1)}) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_distinct' s; base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1); \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> (dom (ksPSpace s) - {x. base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1)}) = {} proof (prove)
goal:
No subgoals!