theory StoreWord_C

lemma pointerInUserData_c_guard:
  "\<lbrakk> valid_pspace' s; pointerInUserData ptr s  \<or> pointerInDeviceData ptr s ; is_aligned ptr 2 \<rbrakk>
   \<Longrightarrow> c_guard (Ptr ptr :: word32 ptr)" apply (simp add: pointerInUserData_def pointerInDeviceData_def) apply (simp add: c_guard_def ptr_aligned_def is_aligned_def c_null_guard_def) apply (fold is_aligned_def [where n=2, simplified])[1] apply (rule contra_subsetD) apply (rule order_trans [rotated]) apply (rule_tac x="ptr && mask pageBits" and y=4 and z=4096 in intvl_sub_offset) apply (cut_tac y=ptr and a="mask pageBits && (~~ mask 2)" in word_and_le1) apply (subst(asm) word_bw_assocs[symmetric], subst(asm) is_aligned_neg_mask_eq,
           erule is_aligned_andI1) apply (simp add: word_le_nat_alt mask_def pageBits_def) apply (subst word_plus_and_or_coroll2 [where w="~~ mask pageBits", simplified]) apply simp apply (fastforce dest: intvl_le_lower
                 intro: is_aligned_no_overflow' [where n=12, simplified]
                        is_aligned_andI2
                  simp: mask_def pageBits_def is_aligned_def word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; pointerInUserData ptr s \<or> pointerInDeviceData ptr s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) ptr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> c_guard (PTR(32 word) ptr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; 4 dvd unat ptr\<rbrakk> \<Longrightarrow> 0 \<notin> {ptr..+4} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> 0 \<notin> {ptr..+4} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> {ptr..+4} \<subseteq> ?B3
 2. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> 0 \<notin> ?B3 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> ?y6 \<subseteq> ?B3
 2. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> {ptr..+4} \<subseteq> ?y6
 3. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> 0 \<notin> ?B3 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> unat (ptr && mask pageBits) + 4 \<le> 4096
 2. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> {ptr..+4} \<subseteq> {?k9 + (ptr && mask pageBits)..+4}
 3. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> 0 \<notin> {?k9..+4096} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2; ptr && mask pageBits && ~~ mask 2 \<le> mask pageBits && ~~ mask 2\<rbrakk> \<Longrightarrow> unat (ptr && mask pageBits) + 4 \<le> 4096
 2. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> {ptr..+4} \<subseteq> {?k9 + (ptr && mask pageBits)..+4}
 3. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> 0 \<notin> {?k9..+4096} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2; ptr && mask pageBits \<le> mask pageBits && ~~ mask 2\<rbrakk> \<Longrightarrow> unat (ptr && mask pageBits) + 4 \<le> 4096
 2. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> {ptr..+4} \<subseteq> {?k9 + (ptr && mask pageBits)..+4}
 3. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> 0 \<notin> {?k9..+4096} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> {ptr..+4} \<subseteq> {?k9 + (ptr && mask pageBits)..+4}
 2. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> 0 \<notin> {?k9..+4096} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> {ptr..+4} \<subseteq> {ptr..+4}
 2. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> 0 \<notin> {ptr && ~~ mask pageBits..+4096} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; typ_at' UserDataT (ptr && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (ptr && ~~ mask pageBits) s; is_aligned ptr 2\<rbrakk> \<Longrightarrow> 0 \<notin> {ptr && ~~ mask pageBits..+4096} proof (prove)
goal:
No subgoals!