theory Refine

lemma typ_at_AUserDataI:
  "\<lbrakk> typ_at (AArch (AUserData sz)) p s; pspace_relation (kheap s) (ksPSpace s');
     pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits) \<rbrakk>
        \<Longrightarrow> typ_at' UserDataT (p + n * 2 ^ pageBits) s'" apply (clarsimp simp add: obj_at_def a_type_def ) apply (simp split: Structures_A.kernel_object.split_asm
                     arch_kernel_obj.split_asm split: if_split_asm) apply (drule(1) pspace_relation_absD) apply (clarsimp) apply (drule_tac x = "p + n * 2 ^ pageBits" in spec) apply (drule_tac x = "\<lambda>_ obj. obj = KOUserData" in spec) apply (clarsimp simp: obj_at'_def typ_at'_def ko_wp_at'_def
                        projectKOs) apply (rule exI [where x = KOUserData]) apply (drule mp) apply (rule exI [where x = n]) apply simp apply (clarsimp simp: pspace_aligned'_def) apply (drule (1) bspec [OF _ domI]) apply (clarsimp simp: objBits_simps) apply (fastforce  dest!: pspace_distinctD'  simp: objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch (AUserData sz)) p s; pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); kheap s p = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch (AUserData sz)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>ko x5 x41 x42. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); kheap s p = Some (ArchObj (DataPage False sz)); ko = ArchObj (DataPage False sz); x5 = DataPage False sz; \<not> x41; x42 = sz\<rbrakk> \<Longrightarrow> typ_at' UserDataT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>ko x5 x41 x42. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); ko = ArchObj (DataPage False sz); x5 = DataPage False sz; \<not> x41; x42 = sz; \<forall>(x', P)\<in>obj_relation_cuts (ArchObj (DataPage False sz)) p. \<exists>z. ksPSpace s' x' = Some z \<and> P (ArchObj (DataPage False sz)) z\<rbrakk> \<Longrightarrow> typ_at' UserDataT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); \<not> x41; \<forall>a b. (\<exists>n. a = p + n * 2 ^ pageBits \<and> b = (\<lambda>_ obj. obj = KOUserData) \<and> n < 2 ^ (pageBitsForSize sz - pageBits)) \<longrightarrow> (\<exists>z. ksPSpace s' a = Some z \<and> b (ArchObj (DataPage False sz)) z)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); \<not> x41; \<forall>b. (\<exists>na. p + n * 2 ^ pageBits = p + na * 2 ^ pageBits \<and> b = (\<lambda>_ obj. obj = KOUserData) \<and> na < 2 ^ (pageBitsForSize sz - pageBits)) \<longrightarrow> (\<exists>z. ksPSpace s' (p + n * 2 ^ pageBits) = Some z \<and> b (ArchObj (DataPage False sz)) z)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); \<not> x41; (\<exists>na. p + n * 2 ^ pageBits = p + na * 2 ^ pageBits \<and> (\<lambda>_ obj. obj = KOUserData) = (\<lambda>_ obj. obj = KOUserData) \<and> na < 2 ^ (pageBitsForSize sz - pageBits)) \<longrightarrow> (\<exists>z. ksPSpace s' (p + n * 2 ^ pageBits) = Some z \<and> z = KOUserData)\<rbrakk> \<Longrightarrow> typ_at' UserDataT (p + n * 2 ^ pageBits) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); \<not> x41; (\<exists>na. n * 2 ^ pageBits = na * 2 ^ pageBits \<and> na < 2 ^ (pageBitsForSize sz - pageBits)) \<longrightarrow> ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserData\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s' (p + n * 2 ^ pageBits) = Some ko \<and> is_aligned (p + n * 2 ^ pageBits) (objBitsKO ko) \<and> koTypeOf ko = UserDataT \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO ko) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); \<not> x41; (\<exists>na. n * 2 ^ pageBits = na * 2 ^ pageBits \<and> na < 2 ^ (pageBitsForSize sz - pageBits)) \<longrightarrow> ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserData\<rbrakk> \<Longrightarrow> ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserData \<and> is_aligned (p + n * 2 ^ pageBits) (objBitsKO KOUserData) \<and> koTypeOf KOUserData = UserDataT \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO KOUserData) s' proof (prove)
goal (2 subgoals):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); \<not> x41\<rbrakk> \<Longrightarrow> \<exists>na. n * 2 ^ pageBits = na * 2 ^ pageBits \<and> na < 2 ^ (pageBitsForSize sz - pageBits)
 2. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); \<not> x41; ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserData\<rbrakk> \<Longrightarrow> ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserData \<and> is_aligned (p + n * 2 ^ pageBits) (objBitsKO KOUserData) \<and> koTypeOf KOUserData = UserDataT \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO KOUserData) s' proof (prove)
goal (2 subgoals):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); \<not> x41\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits = n * 2 ^ pageBits \<and> n < 2 ^ (pageBitsForSize sz - pageBits)
 2. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); \<not> x41; ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserData\<rbrakk> \<Longrightarrow> ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserData \<and> is_aligned (p + n * 2 ^ pageBits) (objBitsKO KOUserData) \<and> koTypeOf KOUserData = UserDataT \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO KOUserData) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); \<not> x41; ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserData\<rbrakk> \<Longrightarrow> ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserData \<and> is_aligned (p + n * 2 ^ pageBits) (objBitsKO KOUserData) \<and> koTypeOf KOUserData = UserDataT \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO KOUserData) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); \<forall>x\<in>dom (ksPSpace s'). is_aligned x (objBitsKO (the (ksPSpace s' x))); pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); \<not> x41; ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserData\<rbrakk> \<Longrightarrow> is_aligned (p + n * 2 ^ pageBits) (objBitsKO KOUserData) \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO KOUserData) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); \<not> x41; ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserData; is_aligned (p + n * 2 ^ pageBits) (objBitsKO (the (ksPSpace s' (p + n * 2 ^ pageBits))))\<rbrakk> \<Longrightarrow> is_aligned (p + n * 2 ^ pageBits) (objBitsKO KOUserData) \<and> ps_clear (p + n * 2 ^ pageBits) (objBitsKO KOUserData) s' proof (prove)
goal (1 subgoal):
 1. \<And>x41. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_distinct' s'; n < 2 ^ (pageBitsForSize sz - pageBits); \<not> x41; ksPSpace s' (p + n * 2 ^ pageBits) = Some KOUserData; is_aligned (p + n * 2 ^ pageBits) pageBits\<rbrakk> \<Longrightarrow> ps_clear (p + n * 2 ^ pageBits) pageBits s' proof (prove)
goal:
No subgoals!