theory Aligned

lemma aligned_add_offset_no_wrap:
  fixes off :: "('a::len) word"
  and     x :: "'a word"
  assumes al: "is_aligned x sz"
  and   offv: "off < 2 ^ sz"
  shows  "unat x + unat off < 2 ^ LENGTH('a)" proof cases assume szv: "sz < LENGTH('a)" from al obtain k where xv: "x = 2 ^ sz * (of_nat k)"
    and kl: "k < 2 ^ (LENGTH('a) - sz)" by (auto elim: is_alignedE) show ?thesis using szv apply (subst xv) apply (subst unat_mult_power_lem[OF kl]) apply (subst mult.commute, rule nat_add_offset_less) apply (rule less_le_trans[OF unat_mono[OF offv, simplified]]) apply (erule eq_imp_le[OF unat_power_lower]) apply (rule kl) apply simp done next assume "\<not> sz < LENGTH('a)" with offv show ?thesis by (simp add: not_less power_overflow ) qed

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
 2. \<not> ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a) proof (chain)
picking this:
is_aligned x sz proof (prove)
using this:
is_aligned x sz

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>x = 2 ^ sz * word_of_nat k; k < 2 ^ (LENGTH('a) - sz)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
x = 2 ^ sz * word_of_nat k
k < 2 ^ (LENGTH('a) - sz)

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

goal (1 subgoal):
 1. unat x + unat off < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz * word_of_nat k) + unat off < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> 2 ^ sz * k + unat off < 2 ^ LENGTH('a) proof (prove)
goal (3 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat off < 2 ^ sz
 2. sz < LENGTH('a) \<Longrightarrow> k < 2 ^ ?m1
 3. sz < LENGTH('a) \<Longrightarrow> LENGTH('a) = ?m1 + sz proof (prove)
goal (3 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz) \<le> 2 ^ sz
 2. sz < LENGTH('a) \<Longrightarrow> k < 2 ^ ?m1
 3. sz < LENGTH('a) \<Longrightarrow> LENGTH('a) = ?m1 + sz proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> k < 2 ^ ?m1
 2. sz < LENGTH('a) \<Longrightarrow> LENGTH('a) = ?m1 + sz proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> LENGTH('a) = LENGTH('a) - sz + sz proof (prove)
goal:
No subgoals! proof (state)
this:
unat x + unat off < 2 ^ LENGTH('a)

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

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

goal (1 subgoal):
 1. unat x + unat off < 2 ^ LENGTH('a) proof (state)
this:
unat x + unat off < 2 ^ LENGTH('a)

goal:
No subgoals!