theory Intent_DR

lemma underlying_memory_storeWord:
  "\<lbrakk> is_aligned ptr 2;is_aligned x 2;x \<noteq> ptr;n\<le> 3 \<rbrakk>
    \<Longrightarrow>underlying_memory (storeWord_ms ptr b ms) (x + n) =
            underlying_memory ms (x + n)" apply (simp add:storeWord_ms_def) using iffD2[OF and_mask_eq_iff_le_mask[where n = 2 and w = n]] apply (intro conjI) apply (clarsimp simp:is_aligned_mask mask_add_aligned) apply (simp add:mask_2pm1) apply (clarsimp simp:|rule conjI)+ apply (case_tac "n=1") apply simp apply (drule arg_cong[where f = "\<lambda>x. x && mask 2"]) apply (clarsimp simp:mask_add_aligned) using iffD2[OF and_mask_eq_iff_le_mask[where n = 2 and w = n]] apply (simp add:mask_2pm1) apply (clarsimp simp:|rule conjI)+ apply (case_tac "n=2") apply simp apply (drule arg_cong[where f = "\<lambda>x. x && mask 2"]) apply (clarsimp simp:mask_add_aligned) using iffD2[OF and_mask_eq_iff_le_mask[where n = 2 and w = n]] apply (simp add:mask_2pm1) apply clarsimp apply (case_tac "n=3") apply simp apply (drule arg_cong[where f = "\<lambda>x. x && mask 2"]) apply (clarsimp simp:mask_add_aligned) using iffD2[OF and_mask_eq_iff_le_mask[where n = 2 and w = n]] apply (simp add:mask_2pm1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3\<rbrakk> \<Longrightarrow> underlying_memory (storeWord_ms ptr b ms) (x + n) = underlying_memory ms (x + n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3\<rbrakk> \<Longrightarrow> (x + n = ptr \<longrightarrow> word_rsplit b ! 3 = underlying_memory ms ptr) \<and> (x + n \<noteq> ptr \<longrightarrow> (x + n = ptr + 1 \<longrightarrow> word_rsplit b ! 2 = underlying_memory ms (ptr + 1)) \<and> (x + n \<noteq> ptr + 1 \<longrightarrow> (x + n = ptr + 2 \<longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)) \<and> (x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3)))) proof (prove)
using this:
n \<le> mask 2 \<Longrightarrow> n && mask 2 = n

goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3\<rbrakk> \<Longrightarrow> (x + n = ptr \<longrightarrow> word_rsplit b ! 3 = underlying_memory ms ptr) \<and> (x + n \<noteq> ptr \<longrightarrow> (x + n = ptr + 1 \<longrightarrow> word_rsplit b ! 2 = underlying_memory ms (ptr + 1)) \<and> (x + n \<noteq> ptr + 1 \<longrightarrow> (x + n = ptr + 2 \<longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)) \<and> (x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n\<rbrakk> \<Longrightarrow> x + n = ptr \<longrightarrow> word_rsplit b ! 3 = underlying_memory ms ptr
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr \<longrightarrow> (x + n = ptr + 1 \<longrightarrow> word_rsplit b ! 2 = underlying_memory ms (ptr + 1)) \<and> (x + n \<noteq> ptr + 1 \<longrightarrow> (x + n = ptr + 2 \<longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)) \<and> (x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n && mask 2 = 0; x && mask 2 = 0; n \<noteq> 0; n \<le> 3; n \<le> mask 2 \<Longrightarrow> False; ptr = x + n\<rbrakk> \<Longrightarrow> word_rsplit b ! 3 = underlying_memory ms (x + n)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr \<longrightarrow> (x + n = ptr + 1 \<longrightarrow> word_rsplit b ! 2 = underlying_memory ms (ptr + 1)) \<and> (x + n \<noteq> ptr + 1 \<longrightarrow> (x + n = ptr + 2 \<longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)) \<and> (x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr \<longrightarrow> (x + n = ptr + 1 \<longrightarrow> word_rsplit b ! 2 = underlying_memory ms (ptr + 1)) \<and> (x + n \<noteq> ptr + 1 \<longrightarrow> (x + n = ptr + 2 \<longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)) \<and> (x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n = ptr + 1\<rbrakk> \<Longrightarrow> word_rsplit b ! 2 = underlying_memory ms (ptr + 1)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 1 \<longrightarrow> (x + n = ptr + 2 \<longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)) \<and> (x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n = ptr + 1; n = 1\<rbrakk> \<Longrightarrow> word_rsplit b ! 2 = underlying_memory ms (ptr + 1)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n = ptr + 1; n \<noteq> 1\<rbrakk> \<Longrightarrow> word_rsplit b ! 2 = underlying_memory ms (ptr + 1)
 3. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 1 \<longrightarrow> (x + n = ptr + 2 \<longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)) \<and> (x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n = ptr + 1; n \<noteq> 1\<rbrakk> \<Longrightarrow> word_rsplit b ! 2 = underlying_memory ms (ptr + 1)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 1 \<longrightarrow> (x + n = ptr + 2 \<longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)) \<and> (x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; n \<noteq> 1; x + n && mask 2 = ptr + 1 && mask 2\<rbrakk> \<Longrightarrow> word_rsplit b ! 2 = underlying_memory ms (ptr + 1)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 1 \<longrightarrow> (x + n = ptr + 2 \<longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)) \<and> (x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> 1 && mask 2 = n; n \<noteq> 1; n && mask 2 = 1 && mask 2\<rbrakk> \<Longrightarrow> word_rsplit b ! 2 = underlying_memory ms (ptr + 1)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 1 \<longrightarrow> (x + n = ptr + 2 \<longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)) \<and> (x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3)) proof (prove)
using this:
n \<le> mask 2 \<Longrightarrow> n && mask 2 = n

goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> 1 && mask 2 = n; n \<noteq> 1; n && mask 2 = 1 && mask 2\<rbrakk> \<Longrightarrow> word_rsplit b ! 2 = underlying_memory ms (ptr + 1)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 1 \<longrightarrow> (x + n = ptr + 2 \<longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)) \<and> (x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 1 \<longrightarrow> (x + n = ptr + 2 \<longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)) \<and> (x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n = ptr + 2\<rbrakk> \<Longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr; x + n \<noteq> ptr + 1\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n = ptr + 2; n = 2\<rbrakk> \<Longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n = ptr + 2; n \<noteq> 2\<rbrakk> \<Longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)
 3. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr; x + n \<noteq> ptr + 1\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n = ptr + 2; n \<noteq> 2\<rbrakk> \<Longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr; x + n \<noteq> ptr + 1\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; n \<noteq> 2; x + n && mask 2 = ptr + 2 && mask 2\<rbrakk> \<Longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr; x + n \<noteq> ptr + 1\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> 2 && mask 2 = n; n \<noteq> 2; n && mask 2 = 2 && mask 2\<rbrakk> \<Longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr; x + n \<noteq> ptr + 1\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3) proof (prove)
using this:
n \<le> mask 2 \<Longrightarrow> n && mask 2 = n

goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> 2 && mask 2 = n; n \<noteq> 2; n && mask 2 = 2 && mask 2\<rbrakk> \<Longrightarrow> word_rsplit b ! Suc 0 = underlying_memory ms (ptr + 2)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr; x + n \<noteq> ptr + 1\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n \<noteq> ptr; x + n \<noteq> ptr + 1\<rbrakk> \<Longrightarrow> x + n \<noteq> ptr + 2 \<longrightarrow> x + n = ptr + 3 \<longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n = ptr + 3\<rbrakk> \<Longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n = ptr + 3; n = 3\<rbrakk> \<Longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3)
 2. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n = ptr + 3; n \<noteq> 3\<rbrakk> \<Longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; x + n = ptr + 3; n \<noteq> 3\<rbrakk> \<Longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> n && mask 2 = n; n \<noteq> 3; x + n && mask 2 = ptr + 3 && mask 2\<rbrakk> \<Longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> 3 && mask 2 = n; n \<noteq> 3; n && mask 2 = 3 && mask 2\<rbrakk> \<Longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3) proof (prove)
using this:
n \<le> mask 2 \<Longrightarrow> n && mask 2 = n

goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; is_aligned x 2; x \<noteq> ptr; n \<le> 3; n \<le> mask 2 \<Longrightarrow> 3 && mask 2 = n; n \<noteq> 3; n && mask 2 = 3 && mask 2\<rbrakk> \<Longrightarrow> word_rsplit b ! 0 = underlying_memory ms (ptr + 3) proof (prove)
goal:
No subgoals!