theory ArchDetype_AI

lemma mapM_x_storeWord[Detype_AI_asms]:
(* FIXME: taken from Retype_C.thy and adapted wrt. the missing intvl syntax. *)
  assumes al: "is_aligned ptr word_size_bits"
  shows "mapM_x (\<lambda>x. storeWord (ptr + of_nat x * word_size) 0) [0..<n]
  = modify (underlying_memory_update
             (\<lambda>m x. if \<exists>k. x = ptr + of_nat k \<and> k < n * word_size 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 \<exists>k. x = ptr + of_nat k \<and> k < 4 + n' * 4 then 0
             else (m x :: word8)) =
           ((\<lambda>xa. if \<exists>k. xa = ptr + of_nat k \<and> k < 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: "(EX k. x = ptr + of_nat k \<and> k < 4 + n' * 4) =
               ((\<exists>k. x = ptr + of_nat k \<and> k < 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: xin' conj_disj_distribL ex_disj_distrib field_simps) show "?thesis m x" by (simp add: xin word_rsplit_0 word_bits_conv cong: if_cong) 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 word_size_bits_def)+ 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 word_size_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 * word_size) 0) [0..<n] = modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < n * word_size then 0 else m x)) proof (state)
goal (2 subgoals):
 1. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * word_size) 0) [0..<0] = modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < 0 * word_size then 0 else m x))
 2. \<And>n. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * word_size) 0) [0..<n] = modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < n * word_size then 0 else m x)) \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * word_size) 0) [0..<Suc n] = modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < Suc n * word_size then 0 else m x)) proof (state)
this:


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

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

goal (1 subgoal):
 1. \<And>n. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * word_size) 0) [0..<n] = modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < n * word_size then 0 else m x)) \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * word_size) 0) [0..<Suc n] = modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < Suc n * word_size then 0 else m x)) proof (prove)
goal (1 subgoal):
 1. \<And>m x. (if \<exists>k. x = ptr + word_of_nat k \<and> k < 4 + n' * 4 then 0 else m x) = ((\<lambda>xa. if \<exists>k. xa = ptr + word_of_nat k \<and> k < 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 \<exists>k. x = ptr + word_of_nat k \<and> k < 4 + n' * 4 then 0 else m x) = ((\<lambda>xa. if \<exists>k. xa = ptr + word_of_nat k \<and> k < 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 \<exists>k. x = ptr + word_of_nat k \<and> k < 4 + n' * 4 then 0 else m x) = ((\<lambda>xa. if \<exists>k. xa = ptr + word_of_nat k \<and> k < 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:
(?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)

goal (1 subgoal):
 1. \<And>m x. (if \<exists>k. x = ptr + word_of_nat k \<and> k < 4 + n' * 4 then 0 else m x) = ((\<lambda>xa. if \<exists>k. xa = ptr + word_of_nat k \<and> k < 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. (\<exists>k. x = ptr + word_of_nat k \<and> k < 4 + n' * 4) = ((\<exists>k. x = ptr + word_of_nat k \<and> k < 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:
(\<exists>k. x = ptr + word_of_nat k \<and> k < 4 + n' * 4) = ((\<exists>k. x = ptr + word_of_nat k \<and> k < 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 \<exists>k. x = ptr + word_of_nat k \<and> k < 4 + n' * 4 then 0 else m x) = ((\<lambda>xa. if \<exists>k. xa = ptr + word_of_nat k \<and> k < 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 \<exists>k. x = ptr + word_of_nat k \<and> k < 4 + n' * 4 then 0 else m x) = ((\<lambda>xa. if \<exists>k. xa = ptr + word_of_nat k \<and> k < 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)
this:
(if \<exists>k. x = ptr + word_of_nat k \<and> k < 4 + n' * 4 then 0 else m x) = ((\<lambda>xa. if \<exists>k. xa = ptr + word_of_nat k \<and> k < 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 \<exists>k. ?x = ptr + word_of_nat k \<and> k < 4 + n' * 4 then 0 else ?m ?x) = ((\<lambda>xa. if \<exists>k. xa = ptr + word_of_nat k \<and> k < 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 (1 subgoal):
 1. \<And>n. mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * word_size) 0) [0..<n] = modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < n * word_size then 0 else m x)) \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * word_size) 0) [0..<Suc n] = modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < Suc n * word_size then 0 else m x)) proof (chain)
picking this:
is_aligned ptr word_size_bits proof (prove)
using this:
is_aligned ptr word_size_bits

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> word_size_bits proof (prove)
goal (1 subgoal):
 1. 2 \<le> word_size_bits 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 * word_size) 0) [0..<n] = modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < n * word_size then 0 else m x)) \<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + word_of_nat x * word_size) 0) [0..<Suc n] = modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < Suc n * word_size 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 * word_size) 0) [0..<Suc n'] = modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < Suc n' * word_size then 0 else m x)) proof (prove)
goal (1 subgoal):
 1. is_aligned (ptr + word_of_nat n' * 4) 2 \<Longrightarrow> do x <- modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < n' * word_size then 0 else m x));
storeWord (ptr + word_of_nat n' * word_size) 0
od = modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < word_size + n' * word_size 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 \<exists>k. xa = ptr + word_of_nat k \<and> k < 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 \<exists>k. x = ptr + word_of_nat k \<and> k < 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 * word_size) 0) [0..<Suc n'] = modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < Suc n' * word_size then 0 else m x))

goal:
No subgoals!