theory ArchUserOp_IF

lemma data_at_disjoint_equiv:
  "\<lbrakk> ptr' \<noteq> ptr;data_at sz' ptr' s; data_at sz ptr s; valid_objs s; pspace_aligned s;
     pspace_distinct s; ptr' \<in> obj_range ptr (ArchObj (DataPage dev sz)) \<rbrakk>
     \<Longrightarrow> False" apply (frule (2) data_at_obj_range[where offset = 0,simplified]) apply (clarsimp simp: data_at_def obj_at_def) apply (elim disjE) by (clarsimp dest!: spec simp: obj_at_def pspace_distinct_def'
      , erule impE, erule conjI2[OF conjI2], (fastforce+)[2]
      , fastforce cong: obj_range_data_for_cong)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr' \<noteq> ptr; data_at sz' ptr' s; data_at sz ptr s; valid_objs s; pspace_aligned s; pspace_distinct s; ptr' \<in> obj_range ptr (ArchObj (DataPage dev sz))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr' \<noteq> ptr; data_at sz' ptr' s; data_at sz ptr s; valid_objs s; pspace_aligned s; pspace_distinct s; ptr' \<in> obj_range ptr (ArchObj (DataPage dev sz)); ptr' \<in> obj_range ptr' (ArchObj (DataPage ?dev sz'))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr' \<noteq> ptr; (\<exists>ko. kheap s ptr' = Some ko \<and> a_type ko = AArch (AUserData sz')) \<or> (\<exists>ko. kheap s ptr' = Some ko \<and> a_type ko = AArch (ADeviceData sz')); (\<exists>ko. kheap s ptr = Some ko \<and> a_type ko = AArch (AUserData sz)) \<or> (\<exists>ko. kheap s ptr = Some ko \<and> a_type ko = AArch (ADeviceData sz)); valid_objs s; pspace_aligned s; pspace_distinct s; ptr' \<in> obj_range ptr (ArchObj (DataPage dev sz)); ptr' \<in> obj_range ptr' (ArchObj (DataPage ?dev sz'))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ptr' \<noteq> ptr; valid_objs s; pspace_aligned s; pspace_distinct s; ptr' \<in> obj_range ptr (ArchObj (DataPage dev sz)); ptr' \<in> obj_range ptr' (ArchObj (DataPage ?dev sz')); \<exists>ko. kheap s ptr' = Some ko \<and> a_type ko = AArch (AUserData sz'); \<exists>ko. kheap s ptr = Some ko \<and> a_type ko = AArch (AUserData sz)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>ptr' \<noteq> ptr; valid_objs s; pspace_aligned s; pspace_distinct s; ptr' \<in> obj_range ptr (ArchObj (DataPage dev sz)); ptr' \<in> obj_range ptr' (ArchObj (DataPage ?dev sz')); \<exists>ko. kheap s ptr' = Some ko \<and> a_type ko = AArch (AUserData sz'); \<exists>ko. kheap s ptr = Some ko \<and> a_type ko = AArch (ADeviceData sz)\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>ptr' \<noteq> ptr; valid_objs s; pspace_aligned s; pspace_distinct s; ptr' \<in> obj_range ptr (ArchObj (DataPage dev sz)); ptr' \<in> obj_range ptr' (ArchObj (DataPage ?dev sz')); \<exists>ko. kheap s ptr' = Some ko \<and> a_type ko = AArch (ADeviceData sz'); \<exists>ko. kheap s ptr = Some ko \<and> a_type ko = AArch (AUserData sz)\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>ptr' \<noteq> ptr; valid_objs s; pspace_aligned s; pspace_distinct s; ptr' \<in> obj_range ptr (ArchObj (DataPage dev sz)); ptr' \<in> obj_range ptr' (ArchObj (DataPage ?dev sz')); \<exists>ko. kheap s ptr' = Some ko \<and> a_type ko = AArch (ADeviceData sz'); \<exists>ko. kheap s ptr = Some ko \<and> a_type ko = AArch (ADeviceData sz)\<rbrakk> \<Longrightarrow> False