theory StoreWord_C

lemma byte_to_word_heap_upd_neq:
  assumes   alb: "is_aligned base 2"
  and       alp: "is_aligned p 2"
  and       neq: "base + ucast off * 4 \<noteq> p"
  and word_byte: "n < 4"
  shows "byte_to_word_heap (m (p + n := v')) base off = byte_to_word_heap m base off" proof - from alb have alw: "is_aligned (base + ucast off * 4) 2" by (fastforce elim: aligned_add_aligned
                intro: is_aligned_mult_triv2 [where n=2, simplified]
                 simp: word_bits_def) from alp have p_intvl: "p + n \<in> {p .. p + 3}" apply (clarsimp simp: word_byte) apply (rule conjI) apply (fastforce elim: is_aligned_no_wrap' simp: word_byte) apply (subst word_plus_mono_right) apply (clarsimp simp: word_byte word_le_make_less) apply (simp add: word_bits_def is_aligned_no_overflow'[OF alp, simplified]) apply simp done hence not_in_range: "p + n \<notin> {(base + ucast off * 4)..+4}" apply (subst intvl_range_conv [OF alw, simplified]) apply (simp add: word_bits_def) apply (cut_tac aligned_neq_into_no_overlap [OF neq alw alp]) apply (auto simp: field_simps range_inter)[1] done thus ?thesis by (rule byte_to_word_heap_upd_outside_range) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. byte_to_word_heap (m(p + n := v')) base off = byte_to_word_heap m base off proof (state)
goal (1 subgoal):
 1. byte_to_word_heap (m(p + n := v')) base off = byte_to_word_heap m base off proof (chain)
picking this:
is_aligned base 2 proof (prove)
using this:
is_aligned base 2

goal (1 subgoal):
 1. is_aligned (base + UCAST(10 \<rightarrow> 32) off * 4) 2 proof (state)
this:
is_aligned (base + UCAST(10 \<rightarrow> 32) off * 4) 2

goal (1 subgoal):
 1. byte_to_word_heap (m(p + n := v')) base off = byte_to_word_heap m base off proof (chain)
picking this:
is_aligned p 2 proof (prove)
using this:
is_aligned p 2

goal (1 subgoal):
 1. p + n \<in> {p..p + 3} proof (prove)
goal (1 subgoal):
 1. is_aligned p 2 \<Longrightarrow> p \<le> p + n \<and> p + n \<le> p + 3 proof (prove)
goal (2 subgoals):
 1. is_aligned p 2 \<Longrightarrow> p \<le> p + n
 2. is_aligned p 2 \<Longrightarrow> p + n \<le> p + 3 proof (prove)
goal (1 subgoal):
 1. is_aligned p 2 \<Longrightarrow> p + n \<le> p + 3 proof (prove)
goal (3 subgoals):
 1. is_aligned p 2 \<Longrightarrow> n \<le> 3
 2. is_aligned p 2 \<Longrightarrow> p \<le> p + 3
 3. is_aligned p 2 \<Longrightarrow> True proof (prove)
goal (2 subgoals):
 1. is_aligned p 2 \<Longrightarrow> p \<le> p + 3
 2. is_aligned p 2 \<Longrightarrow> True proof (prove)
goal (1 subgoal):
 1. is_aligned p 2 \<Longrightarrow> True proof (prove)
goal:
No subgoals! proof (state)
this:
p + n \<in> {p..p + 3}

goal (1 subgoal):
 1. byte_to_word_heap (m(p + n := v')) base off = byte_to_word_heap m base off proof (prove)
using this:
p + n \<in> {p..p + 3}

goal (1 subgoal):
 1. p + n \<notin> {base + UCAST(10 \<rightarrow> 32) off * 4..+4} proof (prove)
goal (1 subgoal):
 1. p + n \<in> {p..p + 3} \<Longrightarrow> p + n \<notin> {base + UCAST(10 \<rightarrow> 32) off * 4..3 + (base + UCAST(10 \<rightarrow> 32) off * 4)} proof (prove)
goal (1 subgoal):
 1. p \<le> p + n \<and> p + n \<le> p + 3 \<Longrightarrow> base + UCAST(10 \<rightarrow> 32) off * 4 \<le> p + n \<longrightarrow> \<not> p + n \<le> 3 + (base + UCAST(10 \<rightarrow> 32) off * 4) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<le> p + n \<and> p + n \<le> p + 3; {base + UCAST(10 \<rightarrow> 32) off * 4..base + UCAST(10 \<rightarrow> 32) off * 4 + (2\<^sup>2 - 1)} \<inter> {p..p + (2\<^sup>2 - 1)} = {}\<rbrakk> \<Longrightarrow> base + UCAST(10 \<rightarrow> 32) off * 4 \<le> p + n \<longrightarrow> \<not> p + n \<le> 3 + (base + UCAST(10 \<rightarrow> 32) off * 4) proof (prove)
goal:
No subgoals! proof (state)
this:
p + n \<notin> {base + UCAST(10 \<rightarrow> 32) off * 4..+4}

goal (1 subgoal):
 1. byte_to_word_heap (m(p + n := v')) base off = byte_to_word_heap m base off proof (prove)
using this:
p + n \<notin> {base + UCAST(10 \<rightarrow> 32) off * 4..+4}

goal (1 subgoal):
 1. byte_to_word_heap (m(p + n := v')) base off = byte_to_word_heap m base off proof (state)
this:
byte_to_word_heap (m(p + n := v')) base off = byte_to_word_heap m base off

goal:
No subgoals!