theory Retype_C

lemma mapM_x_storeWord:
  assumes al: "is_aligned ptr 2"
  shows "mapM_x (\<lambda>x. storeWord (ptr + of_nat x * 4) 0) [0..<n]
  = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+ n * 4} then 0 else m x))" proof (induct n) case 0 thus ?case apply (rule ext) apply (simp add: mapM_x_mapM mapM_def sequence_def
      modify_def get_def put_def bind_def return_def) done next case (Suc n') have funs_eq:
    "\<And>m x. (if x \<in> {ptr..+4 + n' * 4} then 0 else (m x :: word8)) =
           ((\<lambda>xa. if xa \<in> {ptr..+n' * 4} then 0 else m xa)
           (ptr + of_nat n' * 4 := word_rsplit (0 :: word32) ! 3,
            ptr + of_nat n' * 4 + 1 := word_rsplit (0 :: word32) ! 2,
            ptr + of_nat n' * 4 + 2 := word_rsplit (0 :: word32) ! Suc 0,
            ptr + of_nat n' * 4 + 3 := word_rsplit (0 :: word32) ! 0)) x" proof - fix m x have xin': "\<And>x. (x < 4 + n' * 4) = (x < n' * 4 \<or> x = n' * 4
                     \<or> x = (n' * 4) + 1 \<or> x = (n' * 4) + 2 \<or> x = (n' * 4) + 3)" by (safe, simp_all) have xin: "x \<in> {ptr..+4 + n' * 4} = (x \<in> {ptr..+n' * 4} \<or> x = ptr + of_nat n' * 4 \<or>
      x = ptr + of_nat n' * 4 + 1 \<or> x = ptr + of_nat n' * 4 + 2 \<or> x = ptr + of_nat n' * 4 + 3)" by (simp add: intvl_def xin' conj_disj_distribL
                    ex_disj_distrib field_simps) show "?thesis m x" apply (simp add: xin word_rsplit_0 word_bits_def cong: if_cong) apply (simp split: if_split) done qed from al have "is_aligned (ptr + of_nat n' * 4) 2" apply (rule aligned_add_aligned) apply (rule is_aligned_mult_triv2 [where n = 2, simplified]) apply (simp add: word_bits_conv)+ done thus ?case apply (simp add: mapM_x_append bind_assoc Suc.hyps mapM_x_singleton) apply (simp add: storeWord_def assert_def is_aligned_mask modify_modify comp_def) apply (simp only: funs_eq) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+n * 4} then 0 else m x)) proof (state)
goal (2 subgoals):
 1. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<0] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+0 * 4} then 0 else m x))
 2. \<And>n. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+n * 4} then 0 else m x)) \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<Suc n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+Suc n * 4} then 0 else m x)) proof (state)
this:


goal (2 subgoals):
 1. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<0] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+0 * 4} then 0 else m x))
 2. \<And>n. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+n * 4} then 0 else m x)) \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<Suc n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+Suc n * 4} then 0 else m x)) proof (prove)
goal (1 subgoal):
 1. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<0] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+0 * 4} then 0 else m x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<0] x = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+0 * 4} then 0 else m x)) x proof (prove)
goal:
No subgoals! proof (state)
this:
mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<0] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+0 * 4} then 0 else m x))

goal (1 subgoal):
 1. \<And>n. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+n * 4} then 0 else m x)) \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<Suc n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+Suc n * 4} then 0 else m x)) proof (state)
goal (1 subgoal):
 1. \<And>n. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+n * 4} then 0 else m x)) \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<Suc n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+Suc n * 4} then 0 else m x)) proof (state)
this:
mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<n'] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+n' * 4} then 0 else m x))

goal (1 subgoal):
 1. \<And>n. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+n * 4} then 0 else m x)) \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<Suc n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+Suc n * 4} then 0 else m x)) proof (prove)
goal (1 subgoal):
 1. \<And>m x. (if x \<in> {ptr..+4 + n' * 4} then 0 else m x) = ((\<lambda>xa. if xa \<in> {ptr..+n' * 4} then 0 else m xa)(ptr + word_of_nat n' * 4 := word_rsplit 0 ! 3, ptr + word_of_nat n' * 4 + 1 := word_rsplit 0 ! 2, ptr + word_of_nat n' * 4 + 2 := word_rsplit 0 ! Suc 0, ptr + word_of_nat n' * 4 + 3 := word_rsplit 0 ! 0)) x proof (state)
goal (1 subgoal):
 1. \<And>m x. (if x \<in> {ptr..+4 + n' * 4} then 0 else m x) = ((\<lambda>xa. if xa \<in> {ptr..+n' * 4} then 0 else m xa)(ptr + word_of_nat n' * 4 := word_rsplit 0 ! 3, ptr + word_of_nat n' * 4 + 1 := word_rsplit 0 ! 2, ptr + word_of_nat n' * 4 + 2 := word_rsplit 0 ! Suc 0, ptr + word_of_nat n' * 4 + 3 := word_rsplit 0 ! 0)) x proof (state)
goal (1 subgoal):
 1. \<And>m x. (if x \<in> {ptr..+4 + n' * 4} then 0 else m x) = ((\<lambda>xa. if xa \<in> {ptr..+n' * 4} then 0 else m xa)(ptr + word_of_nat n' * 4 := word_rsplit 0 ! 3, ptr + word_of_nat n' * 4 + 1 := word_rsplit 0 ! 2, ptr + word_of_nat n' * 4 + 2 := word_rsplit 0 ! Suc 0, ptr + word_of_nat n' * 4 + 3 := word_rsplit 0 ! 0)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. (x < 4 + n' * 4) = (x < n' * 4 \<or> x = n' * 4 \<or> x = n' * 4 + 1 \<or> x = n' * 4 + 2 \<or> x = n' * 4 + 3) proof (state)
this:
(?x2 < 4 + n' * 4) = (?x2 < n' * 4 \<or> ?x2 = n' * 4 \<or> ?x2 = n' * 4 + 1 \<or> ?x2 = n' * 4 + 2 \<or> ?x2 = n' * 4 + 3)

goal (1 subgoal):
 1. \<And>m x. (if x \<in> {ptr..+4 + n' * 4} then 0 else m x) = ((\<lambda>xa. if xa \<in> {ptr..+n' * 4} then 0 else m xa)(ptr + word_of_nat n' * 4 := word_rsplit 0 ! 3, ptr + word_of_nat n' * 4 + 1 := word_rsplit 0 ! 2, ptr + word_of_nat n' * 4 + 2 := word_rsplit 0 ! Suc 0, ptr + word_of_nat n' * 4 + 3 := word_rsplit 0 ! 0)) x proof (prove)
goal (1 subgoal):
 1. (x \<in> {ptr..+4 + n' * 4}) = (x \<in> {ptr..+n' * 4} \<or> x = ptr + word_of_nat n' * 4 \<or> x = ptr + word_of_nat n' * 4 + 1 \<or> x = ptr + word_of_nat n' * 4 + 2 \<or> x = ptr + word_of_nat n' * 4 + 3) proof (state)
this:
(x \<in> {ptr..+4 + n' * 4}) = (x \<in> {ptr..+n' * 4} \<or> x = ptr + word_of_nat n' * 4 \<or> x = ptr + word_of_nat n' * 4 + 1 \<or> x = ptr + word_of_nat n' * 4 + 2 \<or> x = ptr + word_of_nat n' * 4 + 3)

goal (1 subgoal):
 1. \<And>m x. (if x \<in> {ptr..+4 + n' * 4} then 0 else m x) = ((\<lambda>xa. if xa \<in> {ptr..+n' * 4} then 0 else m xa)(ptr + word_of_nat n' * 4 := word_rsplit 0 ! 3, ptr + word_of_nat n' * 4 + 1 := word_rsplit 0 ! 2, ptr + word_of_nat n' * 4 + 2 := word_rsplit 0 ! Suc 0, ptr + word_of_nat n' * 4 + 3 := word_rsplit 0 ! 0)) x proof (prove)
goal (1 subgoal):
 1. (if x \<in> {ptr..+4 + n' * 4} then 0 else m x) = ((\<lambda>xa. if xa \<in> {ptr..+n' * 4} then 0 else m xa)(ptr + word_of_nat n' * 4 := word_rsplit 0 ! 3, ptr + word_of_nat n' * 4 + 1 := word_rsplit 0 ! 2, ptr + word_of_nat n' * 4 + 2 := word_rsplit 0 ! Suc 0, ptr + word_of_nat n' * 4 + 3 := word_rsplit 0 ! 0)) x proof (prove)
goal (1 subgoal):
 1. (if x \<in> {ptr..+n' * 4} \<or> x = ptr + word_of_nat n' * 4 \<or> x = ptr + word_of_nat n' * 4 + 1 \<or> x = ptr + word_of_nat n' * 4 + 2 \<or> x = ptr + word_of_nat n' * 4 + 3 then 0 else m x) = (if x = ptr + word_of_nat n' * 4 + 3 then 0 else if x = ptr + word_of_nat n' * 4 + 2 then 0 else if x = ptr + word_of_nat n' * 4 + 1 then 0 else if x = ptr + word_of_nat n' * 4 then 0 else if x \<in> {ptr..+n' * 4} then 0 else m x) proof (prove)
goal:
No subgoals! proof (state)
this:
(if x \<in> {ptr..+4 + n' * 4} then 0 else m x) = ((\<lambda>xa. if xa \<in> {ptr..+n' * 4} then 0 else m xa)(ptr + word_of_nat n' * 4 := word_rsplit 0 ! 3, ptr + word_of_nat n' * 4 + 1 := word_rsplit 0 ! 2, ptr + word_of_nat n' * 4 + 2 := word_rsplit 0 ! Suc 0, ptr + word_of_nat n' * 4 + 3 := word_rsplit 0 ! 0)) x

goal:
No subgoals! proof (state)
this:
(if ?x2 \<in> {ptr..+4 + n' * 4} then 0 else ?m2 ?x2) = ((\<lambda>xa. if xa \<in> {ptr..+n' * 4} then 0 else ?m2 xa)(ptr + word_of_nat n' * 4 := word_rsplit 0 ! 3, ptr + word_of_nat n' * 4 + 1 := word_rsplit 0 ! 2, ptr + word_of_nat n' * 4 + 2 := word_rsplit 0 ! Suc 0, ptr + word_of_nat n' * 4 + 3 := word_rsplit 0 ! 0)) ?x2

goal (1 subgoal):
 1. \<And>n. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+n * 4} then 0 else m x)) \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<Suc n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+Suc n * 4} then 0 else m x)) proof (chain)
picking this:
is_aligned ptr 2 proof (prove)
using this:
is_aligned ptr 2

goal (1 subgoal):
 1. is_aligned (ptr + word_of_nat n' * 4) 2 proof (prove)
goal (2 subgoals):
 1. is_aligned (word_of_nat n' * 4) 2
 2. 2 \<le> 2 proof (prove)
goal (1 subgoal):
 1. 2 \<le> 2 proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned (ptr + word_of_nat n' * 4) 2

goal (1 subgoal):
 1. \<And>n. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+n * 4} then 0 else m x)) \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<Suc n] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+Suc n * 4} then 0 else m x)) proof (prove)
using this:
is_aligned (ptr + word_of_nat n' * 4) 2

goal (1 subgoal):
 1. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<Suc n'] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+Suc n' * 4} then 0 else m x)) proof (prove)
goal (1 subgoal):
 1. is_aligned (ptr + word_of_nat n' * 4) 2 \<Longrightarrow> do y <- modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+n' * 4} then 0 else m x));
storeWord (ptr + word_of_nat n' * 4) 0
od = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 + n' * 4} then 0 else m x)) proof (prove)
goal (1 subgoal):
 1. ptr + word_of_nat n' * 4 && mask 2 = 0 \<Longrightarrow> modify (underlying_memory_update (\<lambda>x. (\<lambda>xa. if xa \<in> {ptr..+n' * 4} then 0 else x xa)(ptr + word_of_nat n' * 4 := word_rsplit 0 ! 3, ptr + word_of_nat n' * 4 + 1 := word_rsplit 0 ! 2, ptr + word_of_nat n' * 4 + 2 := word_rsplit 0 ! Suc 0, ptr + word_of_nat n' * 4 + 3 := word_rsplit 0 ! 0))) = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 + n' * 4} then 0 else m x)) proof (prove)
goal:
No subgoals! proof (state)
this:
mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * 4) 0) [0..<Suc n'] = modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+Suc n' * 4} then 0 else m x))

goal:
No subgoals!