theory VSpace_R

lemma pspace_relation_pd:
  assumes p: "pspace_relation (kheap a) (ksPSpace c)"
  assumes pa: "pspace_aligned a"
  assumes pad: "pspace_aligned' c" "pspace_distinct' c"
  assumes t: "page_directory_at p a"
  shows "page_directory_at' p c" using assms pd_aligned [OF pa t] apply (clarsimp simp: obj_at_def) apply (drule(1) pspace_relation_absD) apply (clarsimp split: Structures_A.kernel_object.split_asm
                        if_split_asm arch_kernel_obj.split_asm) apply (clarsimp simp: page_directory_at'_def pdBits_def pageBits_def
                        typ_at_to_obj_at_arches pdeBits_def) apply (drule_tac x="ucast y" in spec, clarsimp) apply (simp add: ucast_ucast_mask iffD2 [OF mask_eq_iff_w2p] word_size) apply (clarsimp simp add: pde_relation_def) apply (drule(2) aligned_distinct_pde_atI') apply (erule obj_at'_weakenE) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. page_directory_at' p c proof (prove)
using this:
pspace_relation (kheap a) (ksPSpace c)
pspace_aligned a
pspace_aligned' c
pspace_distinct' c
typ_at (AArch APageDirectory) p a
is_aligned p 14

goal (1 subgoal):
 1. page_directory_at' p c proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); pspace_aligned a; pspace_aligned' c; pspace_distinct' c; is_aligned p 14; kheap a p = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> page_directory_at' p c proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); pspace_aligned a; pspace_aligned' c; pspace_distinct' c; is_aligned p 14; \<forall>(x', P)\<in>obj_relation_cuts (ArchObj (PageDirectory pd)) p. \<exists>z. ksPSpace c x' = Some z \<and> P (ArchObj (PageDirectory pd)) z\<rbrakk> \<Longrightarrow> page_directory_at' p c proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); pspace_aligned a; pspace_aligned' c; pspace_distinct' c; is_aligned p 14; \<forall>x. \<exists>z. ksPSpace c (p + (UCAST(12 \<rightarrow> 32) x << 2)) = Some z \<and> pde_relation x (ArchObj (PageDirectory pd)) z\<rbrakk> \<Longrightarrow> page_directory_at' p c proof (prove)
goal (1 subgoal):
 1. \<And>pd y. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); pspace_aligned a; pspace_aligned' c; pspace_distinct' c; is_aligned p 14; \<forall>x. \<exists>z. ksPSpace c (p + (UCAST(12 \<rightarrow> 32) x << 2)) = Some z \<and> pde_relation x (ArchObj (PageDirectory pd)) z; y < 0x1000\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>_. True) (p + (y << 2)) c proof (prove)
goal (1 subgoal):
 1. \<And>pd y z. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); pspace_aligned a; pspace_aligned' c; pspace_distinct' c; is_aligned p 14; y < 0x1000; ksPSpace c (p + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)) = Some z; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) z\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>_. True) (p + (y << 2)) c proof (prove)
goal (1 subgoal):
 1. \<And>pd y z. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); pspace_aligned a; pspace_aligned' c; pspace_distinct' c; is_aligned p 14; y < 0x1000; ksPSpace c (p + (y << 2)) = Some z; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) z\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>_. True) (p + (y << 2)) c proof (prove)
goal (1 subgoal):
 1. \<And>pd y pde. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); pspace_aligned a; pspace_aligned' c; pspace_distinct' c; is_aligned p 14; y < 0x1000; ksPSpace c (p + (y << 2)) = Some (KOArch (KOPDE pde)); pde_relation_aligned (UCAST(32 \<rightarrow> 12) y) (pd (UCAST(32 \<rightarrow> 12) y)) pde\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>_. True) (p + (y << 2)) c proof (prove)
goal (1 subgoal):
 1. \<And>pd y pde. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); pspace_aligned a; pspace_aligned' c; pspace_distinct' c; is_aligned p 14; y < 0x1000; pde_relation_aligned (UCAST(32 \<rightarrow> 12) y) (pd (UCAST(32 \<rightarrow> 12) y)) pde; ko_at' pde (p + (y << 2)) c\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>_. True) (p + (y << 2)) c proof (prove)
goal (1 subgoal):
 1. \<And>pd y pde k. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); pspace_aligned a; pspace_aligned' c; pspace_distinct' c; is_aligned p 14; y < 0x1000; pde_relation_aligned (UCAST(32 \<rightarrow> 12) y) (pd (UCAST(32 \<rightarrow> 12) y)) pde; k = pde\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!