theory Detype_R

lemma modify_pde_pspace_distinct':
  "\<lbrace>pde_at' ptr and pspace_distinct'\<rbrace>
   modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))))
   \<lbrace>\<lambda>a. pspace_distinct'\<rbrace>" apply (clarsimp simp: simpler_modify_def ko_wp_at'_def valid_def typ_at'_def) apply (case_tac ko; simp) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply (subst pspace_distinct'_def) apply (intro ballI) apply (erule domE) apply (clarsimp split:if_splits) apply (drule(1) pspace_distinctD') apply (simp add:objBits_simps archObjSize_def) apply (simp add:ps_clear_def) apply (drule_tac x = x in pspace_distinctD') apply simp unfolding ps_clear_def apply (erule disjoint_subset2[rotated]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pde_at' ptr and pspace_distinct'\<rbrace> modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde)))) \<lbrace>\<lambda>a. pspace_distinct'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); koTypeOf ko = ArchT PDET; ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> pspace_distinct' (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko x8. \<lbrakk>pspace_distinct' 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_distinct' (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_distinct' 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_distinct' (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_distinct' 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_distinct' (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_distinct' 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\<in>dom (ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s)). ps_clear x (objBitsKO (the (ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) x))) (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 x. \<lbrakk>pspace_distinct' 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; x \<in> dom (ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s))\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) x))) (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 x r. \<lbrakk>pspace_distinct' 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 r\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO (the (ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) x))) (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (2 subgoals):
 1. \<And>s x3. \<lbrakk>pspace_distinct' 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> ps_clear ptr (objBitsKO (KOArch (KOPDE new_pde))) (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s)
 2. \<And>s x3 x r. \<lbrakk>pspace_distinct' 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 r\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO r) (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (2 subgoals):
 1. \<And>s x3. \<lbrakk>pspace_distinct' s; is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s; ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO (KOArch (KOPDE new_pde))) (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s)
 2. \<And>s x3 x r. \<lbrakk>pspace_distinct' 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 r\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO r) (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pspace_distinct' s; is_aligned ptr pdeBits; ps_clear ptr pdeBits s\<rbrakk> \<Longrightarrow> ps_clear ptr pdeBits (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s)
 2. \<And>s x3 x r. \<lbrakk>pspace_distinct' 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 r\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO r) (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x r. \<lbrakk>pspace_distinct' 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 r\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO r) (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (2 subgoals):
 1. \<And>s x3 x r. \<lbrakk>pspace_distinct' 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\<rbrakk> \<Longrightarrow> pspace_distinct' s
 2. \<And>s x3 x r. \<lbrakk>pspace_distinct' 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; ps_clear x (objBitsKO r) s\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO r) (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x r. \<lbrakk>pspace_distinct' 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; ps_clear x (objBitsKO r) s\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO r) (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x r. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE x3)); is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ({ptr..ptr + (1 << objBitsKO (KOArch (KOPDE x3))) - 1} - {ptr}) \<inter> dom (ksPSpace s) = {}; x \<noteq> ptr; ({x..x + (1 << objBitsKO r) - 1} - {x}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> ({x..x + (1 << objBitsKO r) - 1} - {x}) \<inter> dom (ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s)) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x r. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE x3)); is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ({ptr..ptr + (1 << objBitsKO (KOArch (KOPDE x3))) - 1} - {ptr}) \<inter> dom (ksPSpace s) = {}; x \<noteq> ptr\<rbrakk> \<Longrightarrow> dom (ksPSpace (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s)) \<subseteq> dom (ksPSpace s) proof (prove)
goal:
No subgoals!