theory Aligned

lemma aligned_add_offset_mod:
  fixes x :: "('a::len) word"
  assumes al: "is_aligned x sz"
  and     kv: "k < 2 ^ sz"
  shows   "(x + k) mod 2 ^ sz = k" proof cases assume szv: "sz < LENGTH('a)" have ux: "unat x + unat k < 2 ^ LENGTH('a)" by (rule aligned_add_offset_no_wrap) fact+ show ?thesis using al szv apply (simp flip: take_bit_eq_mod) apply (rule bit_word_eqI) apply (auto simp add: bit_simps) apply (metis assms(2) bit_or_iff is_aligned_mask is_aligned_nth leD less_mask_eq word_and_le1 word_bw_lcs(1) word_neq_0_conv word_plus_and_or_coroll) apply (meson assms(2) leI less_2p_is_upper_bits_unset) apply (metis assms(2) bit_disjunctive_add_iff bit_imp_le_length bit_push_bit_iff is_alignedE' less_2p_is_upper_bits_unset) done next assume "\<not> sz < LENGTH('a)" with al show ?thesis by (simp add: not_less power_overflow is_aligned_mask mask_eq_decr_exp
                  word_mod_by_0) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x + k) mod 2 ^ sz = k proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (x + k) mod 2 ^ sz = k
 2. \<not> ?P \<Longrightarrow> (x + k) mod 2 ^ sz = k proof (state)
this:
sz < LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> (x + k) mod 2 ^ sz = k
 2. \<not> ?P \<Longrightarrow> (x + k) mod 2 ^ sz = k proof (prove)
goal (1 subgoal):
 1. unat x + unat k < 2 ^ LENGTH('a) proof (state)
this:
unat x + unat k < 2 ^ LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> (x + k) mod 2 ^ sz = k
 2. \<not> ?P \<Longrightarrow> (x + k) mod 2 ^ sz = k proof (prove)
goal (1 subgoal):
 1. (x + k) mod 2 ^ sz = k proof (prove)
using this:
is_aligned x sz
sz < LENGTH('a)

goal (1 subgoal):
 1. (x + k) mod 2 ^ sz = k proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit sz (x + k) = k proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (take_bit sz (x + k)) n = bit k n proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < sz; bit (x + k) n\<rbrakk> \<Longrightarrow> bit k n
 2. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < LENGTH('a); bit k n\<rbrakk> \<Longrightarrow> n < sz
 3. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < LENGTH('a); bit k n\<rbrakk> \<Longrightarrow> bit (x + k) n proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < LENGTH('a); bit k n\<rbrakk> \<Longrightarrow> n < sz
 2. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < LENGTH('a); bit k n\<rbrakk> \<Longrightarrow> bit (x + k) n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < LENGTH('a); bit k n\<rbrakk> \<Longrightarrow> bit (x + k) n proof (prove)
goal:
No subgoals! proof (state)
this:
(x + k) mod 2 ^ sz = k

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> (x + k) mod 2 ^ sz = k proof (state)
goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> (x + k) mod 2 ^ sz = k proof (state)
this:
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> (x + k) mod 2 ^ sz = k proof (chain)
picking this:
is_aligned x sz
\<not> sz < LENGTH('a) proof (prove)
using this:
is_aligned x sz
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. (x + k) mod 2 ^ sz = k proof (state)
this:
(x + k) mod 2 ^ sz = k

goal:
No subgoals!