theory Detype_AI

lemma (in Detype_AI) mapM_x_storeWord_step:
  assumes al: "is_aligned ptr sz"
  and    sz2: "word_size_bits \<le> sz"
  and     sz: "sz <= word_bits"
  shows "mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1] =
  modify (underlying_memory_update
    (\<lambda>m x. if x \<in> {x. \<exists>k. x = ptr + of_nat k \<and> k < 2 ^ sz} 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 (simp add: Suc_unat_mask_div_obfuscated[simplified mask_2pm1] min_def) apply (subst mapM_x_storeWord) apply (erule is_aligned_weaken [OF _ sz2]) apply (rule arg_cong) apply (subgoal_tac "2^word_size_bits = (word_size :: nat)") apply (cut_tac power_add[symmetric,of "2::nat" "sz - word_size_bits" word_size_bits]) apply (simp only: le_add_diff_inverse2[OF sz2]) apply (simp add: word_size_size_bits_nat) done

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

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