theory Detype_R

lemma modify_pde_psp_no_overlap':
  "\<lbrace>pde_at' ptr and pspace_no_overlap' ptr' sz\<rbrace>
   modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))))
   \<lbrace>\<lambda>a. pspace_no_overlap' ptr' sz\<rbrace>" 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 apply (clarsimp simp:simpler_modify_def ko_wp_at'_def
    valid_def typ_at'_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply (subst pspace_no_overlap'_def) apply (intro allI impI) apply (clarsimp split:if_splits) apply (drule(1) pspace_no_overlapD') apply (simp add:objBits_simps archObjSize_def field_simps) apply (drule(1) pspace_no_overlapD')+ apply (simp add:field_simps) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pde_at' ptr and pspace_no_overlap' ptr' sz\<rbrace> modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde)))) \<lbrace>\<lambda>a. pspace_no_overlap' ptr' sz\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>pde_at' ptr and pspace_no_overlap' ptr' sz\<rbrace> modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde)))) \<lbrace>\<lambda>a. pspace_no_overlap' ptr' sz\<rbrace> 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. \<lbrace>pde_at' ptr and pspace_no_overlap' ptr' sz\<rbrace> modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde)))) \<lbrace>\<lambda>a. pspace_no_overlap' ptr' sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pde_at' ptr and pspace_no_overlap' ptr' sz\<rbrace> modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde)))) \<lbrace>\<lambda>a. pspace_no_overlap' ptr' sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>pspace_no_overlap' ptr' sz s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); koTypeOf ko = ArchT PDET; ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr' sz (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko x8. \<lbrakk>pspace_no_overlap' ptr' sz s; ksPSpace s ptr = Some (KOArch x8); is_aligned ptr (objBitsKO (KOArch x8)); archTypeOf x8 = PDET; ps_clear ptr (objBitsKO (KOArch x8)) s; ko = KOArch x8\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr' sz (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object. \<lbrakk>pspace_no_overlap' ptr' sz s; ksPSpace s ptr = Some (KOArch arch_kernel_object); is_aligned ptr (objBitsKO (KOArch arch_kernel_object)); archTypeOf arch_kernel_object = PDET; ps_clear ptr (objBitsKO (KOArch arch_kernel_object)) s; ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr' sz (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object x3. \<lbrakk>pspace_no_overlap' ptr' sz s; ksPSpace s ptr = Some (KOArch (KOPDE x3)); is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s; ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr' sz (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object x3. \<lbrakk>pspace_no_overlap' ptr' sz s; ksPSpace s ptr = Some (KOArch (KOPDE x3)); is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s; ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> \<forall>x ko. ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr' sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object x3 x koa. \<lbrakk>pspace_no_overlap' ptr' sz s; ksPSpace s ptr = Some (KOArch (KOPDE x3)); is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s; ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3; ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) x = Some koa\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr' sz = {} proof (prove)
goal (2 subgoals):
 1. \<And>s x3. \<lbrakk>pspace_no_overlap' ptr' sz s; ksPSpace s ptr = Some (KOArch (KOPDE x3)); is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s\<rbrakk> \<Longrightarrow> {ptr..ptr + 2 ^ objBitsKO (KOArch (KOPDE new_pde)) - 1} \<inter> up_aligned_area ptr' sz = {}
 2. \<And>s x3 x koa. \<lbrakk>pspace_no_overlap' ptr' sz s; ksPSpace s ptr = Some (KOArch (KOPDE x3)); is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s; x \<noteq> ptr; ksPSpace s x = Some koa\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr' sz = {} proof (prove)
goal (2 subgoals):
 1. \<And>s x3. \<lbrakk>pspace_no_overlap' ptr' sz s; is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s; {ptr..ptr + 2 ^ objBitsKO (KOArch (KOPDE x3)) - 1} \<inter> {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..ptr + 2 ^ objBitsKO (KOArch (KOPDE new_pde)) - 1} \<inter> up_aligned_area ptr' sz = {}
 2. \<And>s x3 x koa. \<lbrakk>pspace_no_overlap' ptr' sz s; ksPSpace s ptr = Some (KOArch (KOPDE x3)); is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s; x \<noteq> ptr; ksPSpace s x = Some koa\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr' sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x koa. \<lbrakk>pspace_no_overlap' ptr' sz s; ksPSpace s ptr = Some (KOArch (KOPDE x3)); is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s; x \<noteq> ptr; ksPSpace s x = Some koa\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr' sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x koa. \<lbrakk>pspace_no_overlap' ptr' sz s; is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s; x \<noteq> ptr; {ptr..ptr + 2 ^ objBitsKO (KOArch (KOPDE x3)) - 1} \<inter> {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} = {}; {x..x + 2 ^ objBitsKO koa - 1} \<inter> {ptr'..(ptr' && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO koa - 1} \<inter> up_aligned_area ptr' sz = {} proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>pde_at' ptr and pspace_no_overlap' ptr' sz\<rbrace> modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde)))) \<lbrace>\<lambda>a. pspace_no_overlap' ptr' sz\<rbrace>

goal:
No subgoals!