theory Retype_C

lemma mapM_x_storeWord_step:
  assumes al: "is_aligned ptr sz"
  and    sz2: "2 \<le> sz"
  and     sz: "sz < word_bits"
  shows "mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + 4 .e. ptr + 2 ^ sz - 1] =
  modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+2 ^ (sz - 2) * 4} then 0 else m x))" using al sz apply (simp only: upto_enum_step_def field_simps cong: if_cong) apply (subst if_not_P) apply (subst not_less) apply (erule is_aligned_no_overflow) apply (simp add: mapM_x_map comp_def upto_enum_word del: upt.simps) apply (subst div_power_helper_32 [OF sz2, simplified]) apply assumption apply (simp add: word_bits_def unat_minus_one del: upt.simps) apply (subst mapM_x_storeWord) apply (erule is_aligned_weaken [OF _ sz2]) apply (simp add: field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + 4 .e. ptr + 2 ^ sz - 1] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+2 ^ (sz - 2) * 4} then 0 else m x)) proof (prove)
using this:
is_aligned ptr sz
sz < word_bits

goal (1 subgoal):
 1. mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + 4 .e. ptr + 2 ^ sz - 1] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+2 ^ (sz - 2) * 4} then 0 else m x)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> mapM_x (\<lambda>p. storeWord p 0) (if ptr + 2 ^ sz - 1 < ptr then [] else map (\<lambda>x. ptr + x * (ptr + 4 - ptr)) [0 .e. (ptr + 2 ^ sz - (1 + ptr)) div (ptr + 4 - ptr)]) = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> \<not> ptr + 2 ^ sz - 1 < ptr
 2. \<lbrakk>is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> mapM_x (\<lambda>p. storeWord p 0) (map (\<lambda>x. ptr + x * (ptr + 4 - ptr)) [0 .e. (ptr + 2 ^ sz - (1 + ptr)) div (ptr + 4 - ptr)]) = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 2 ^ sz - 1
 2. \<lbrakk>is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> mapM_x (\<lambda>p. storeWord p 0) (map (\<lambda>x. ptr + x * (ptr + 4 - ptr)) [0 .e. (ptr + 2 ^ sz - (1 + ptr)) div (ptr + 4 - ptr)]) = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> mapM_x (\<lambda>p. storeWord p 0) (map (\<lambda>x. ptr + x * (ptr + 4 - ptr)) [0 .e. (ptr + 2 ^ sz - (1 + ptr)) div (ptr + 4 - ptr)]) = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<Suc (unat ((2 ^ sz - 1) div 4))] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<lbrakk>is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<Suc (unat (2 ^ (sz - 2) - 1))] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<Suc (unat (2 ^ (sz - 2) - 1))] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < 32\<rbrakk> \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<2 ^ (sz - 2)] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < 32\<rbrakk> \<Longrightarrow> is_aligned ptr 2
 2. \<lbrakk>is_aligned ptr sz; sz < 32\<rbrakk> \<Longrightarrow> modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+2 ^ (sz - 2) * 4} then 0 else m x)) = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < 32\<rbrakk> \<Longrightarrow> modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+2 ^ (sz - 2) * 4} then 0 else m x)) = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x)) proof (prove)
goal:
No subgoals!