theory Aligned

lemma word_add_power_off:
  fixes a :: "'a :: len word"
  assumes ak: "a < k"
  and kw: "k < 2 ^ (LENGTH('a) - m)"
  and mw: "m < LENGTH('a)"
  and off: "off < 2 ^ m"
shows "(a * 2 ^ m) + off < k * 2 ^ m" proof (cases "m = 0") case True then show ?thesis using off ak by simp next case False from ak have ak1: "a + 1 \<le> k" by (rule inc_le) then have "(a + 1) * 2 ^ m \<noteq> 0" apply - apply (rule word_power_nonzero) apply (erule order_le_less_trans  [OF _ kw]) apply (rule mw) apply (rule less_is_non_zero_p1 [OF ak]) done then have "(a * 2 ^ m) + off < ((a + 1) * 2 ^ m)" using kw mw apply - apply (simp add: distrib_right) apply (rule word_plus_strict_mono_right [OF off]) apply (rule is_aligned_no_overflow'') apply (rule is_aligned_mult_triv2) apply assumption done also have "\<dots> \<le> k * 2 ^ m" using ak1 mw kw False apply - apply (erule word_mult_le_mono1) apply (simp add: p2_gt_0) apply (simp add: word_less_nat_alt) apply (meson nat_mult_power_less_eq zero_less_numeral) done finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a * 2 ^ m + off < k * 2 ^ m proof (state)
goal (2 subgoals):
 1. m = 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
 2. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m proof (state)
this:
m = 0

goal (2 subgoals):
 1. m = 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
 2. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m proof (chain)
picking this:
m = 0 proof (prove)
using this:
m = 0

goal (1 subgoal):
 1. a * 2 ^ m + off < k * 2 ^ m proof (prove)
using this:
m = 0
off < 2 ^ m
a < k

goal (1 subgoal):
 1. a * 2 ^ m + off < k * 2 ^ m proof (state)
this:
a * 2 ^ m + off < k * 2 ^ m

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m proof (state)
goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m proof (state)
this:
m \<noteq> 0

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m proof (chain)
picking this:
a < k proof (prove)
using this:
a < k

goal (1 subgoal):
 1. a + 1 \<le> k proof (state)
this:
a + 1 \<le> k

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m proof (chain)
picking this:
a + 1 \<le> k proof (prove)
using this:
a + 1 \<le> k

goal (1 subgoal):
 1. (a + 1) * 2 ^ m \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. a + 1 \<le> k \<Longrightarrow> (a + 1) * 2 ^ m \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. a + 1 \<le> k \<Longrightarrow> a + 1 < 2 ^ (LENGTH('a) - m)
 2. a + 1 \<le> k \<Longrightarrow> m < LENGTH('a)
 3. a + 1 \<le> k \<Longrightarrow> a + 1 \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. a + 1 \<le> k \<Longrightarrow> m < LENGTH('a)
 2. a + 1 \<le> k \<Longrightarrow> a + 1 \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. a + 1 \<le> k \<Longrightarrow> a + 1 \<noteq> 0 proof (prove)
goal:
No subgoals! proof (state)
this:
(a + 1) * 2 ^ m \<noteq> 0

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m proof (chain)
picking this:
(a + 1) * 2 ^ m \<noteq> 0 proof (prove)
using this:
(a + 1) * 2 ^ m \<noteq> 0

goal (1 subgoal):
 1. a * 2 ^ m + off < (a + 1) * 2 ^ m proof (prove)
using this:
(a + 1) * 2 ^ m \<noteq> 0
k < 2 ^ (LENGTH('a) - m)
m < LENGTH('a)

goal (1 subgoal):
 1. a * 2 ^ m + off < (a + 1) * 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a + 1) * 2 ^ m \<noteq> 0; k < 2 ^ (LENGTH('a) - m); m < LENGTH('a)\<rbrakk> \<Longrightarrow> a * 2 ^ m + off < (a + 1) * 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a * 2 ^ m + 2 ^ m \<noteq> 0; k < 2 ^ (LENGTH('a) - m); m < LENGTH('a)\<rbrakk> \<Longrightarrow> a * 2 ^ m + off < a * 2 ^ m + 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a * 2 ^ m + 2 ^ m \<noteq> 0; k < 2 ^ (LENGTH('a) - m); m < LENGTH('a)\<rbrakk> \<Longrightarrow> a * 2 ^ m \<le> a * 2 ^ m + 2 ^ m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a * 2 ^ m + 2 ^ m \<noteq> 0; k < 2 ^ (LENGTH('a) - m); m < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned (a * 2 ^ m) m
 2. \<lbrakk>a * 2 ^ m + 2 ^ m \<noteq> 0; k < 2 ^ (LENGTH('a) - m); m < LENGTH('a)\<rbrakk> \<Longrightarrow> a * 2 ^ m + 2 ^ m \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a * 2 ^ m + 2 ^ m \<noteq> 0; k < 2 ^ (LENGTH('a) - m); m < LENGTH('a)\<rbrakk> \<Longrightarrow> a * 2 ^ m + 2 ^ m \<noteq> 0 proof (prove)
goal:
No subgoals! proof (state)
this:
a * 2 ^ m + off < (a + 1) * 2 ^ m

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m proof (state)
this:
a * 2 ^ m + off < (a + 1) * 2 ^ m

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m proof (prove)
goal (1 subgoal):
 1. (a + 1) * 2 ^ m \<le> k * 2 ^ m proof (prove)
using this:
a + 1 \<le> k
m < LENGTH('a)
k < 2 ^ (LENGTH('a) - m)
m \<noteq> 0

goal (1 subgoal):
 1. (a + 1) * 2 ^ m \<le> k * 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a + 1 \<le> k; m < LENGTH('a); k < 2 ^ (LENGTH('a) - m); m \<noteq> 0\<rbrakk> \<Longrightarrow> (a + 1) * 2 ^ m \<le> k * 2 ^ m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m < LENGTH('a); k < 2 ^ (LENGTH('a) - m); m \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < 2 ^ m
 2. \<lbrakk>m < LENGTH('a); k < 2 ^ (LENGTH('a) - m); m \<noteq> 0\<rbrakk> \<Longrightarrow> unat k * unat (2 ^ m) < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < LENGTH('a); k < 2 ^ (LENGTH('a) - m); m \<noteq> 0\<rbrakk> \<Longrightarrow> unat k * unat (2 ^ m) < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < LENGTH('a); unat k < 2 ^ (LENGTH('a) - m); 0 < m\<rbrakk> \<Longrightarrow> unat k * 2 ^ m < 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals! proof (state)
this:
(a + 1) * 2 ^ m \<le> k * 2 ^ m

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m proof (chain)
picking this:
a * 2 ^ m + off < k * 2 ^ m proof (prove)
using this:
a * 2 ^ m + off < k * 2 ^ m

goal (1 subgoal):
 1. a * 2 ^ m + off < k * 2 ^ m proof (state)
this:
a * 2 ^ m + off < k * 2 ^ m

goal:
No subgoals!