theory Word_Lemmas

lemma nasty_split_less:
  "\<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a::len); x < 2 ^ (nm - n)\<rbrakk>
   \<Longrightarrow> (x :: 'a word) * 2 ^ n + (2 ^ m - 1) < 2 ^ nm" apply (simp only: word_less_sub_le[symmetric]) apply (rule order_trans [OF _ nasty_split_lt]) apply (rule word_plus_mono_right) apply (rule word_sub_mono) apply (simp add: word_le_nat_alt) apply simp apply (simp add: word_sub_1_le[OF power_not_zero]) apply (simp add: word_sub_1_le[OF power_not_zero]) apply (rule is_aligned_no_wrap') apply (rule is_aligned_mult_triv2) apply simp apply (erule order_le_less_trans, simp) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x < 2 ^ (nm - n)\<rbrakk> \<Longrightarrow> x * 2 ^ n + (2 ^ m - 1) < 2 ^ nm proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x * 2 ^ n + (2 ^ m - 1) \<le> 2 ^ nm - 1 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x * 2 ^ n + (2 ^ m - 1) \<le> ?x27 * 2 ^ ?n27 + (2 ^ ?n27 - 1)
 2. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> ?x27 < 2 ^ (nm - ?n27)
 3. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> ?n27 \<le> nm
 4. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> nm < LENGTH('a) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> 2 ^ m - 1 \<le> 2 ^ n - 1
 2. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x * 2 ^ n \<le> x * 2 ^ n + (2 ^ n - 1)
 3. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x < 2 ^ (nm - n)
 4. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> n \<le> nm
 5. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> nm < LENGTH('a) proof (prove)
goal (8 subgoals):
 1. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> 2 ^ m \<le> 2 ^ n
 2. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> 1 \<le> 1
 3. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> 2 ^ m - 1 \<le> 2 ^ m
 4. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> 2 ^ n - 1 \<le> 2 ^ n
 5. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x * 2 ^ n \<le> x * 2 ^ n + (2 ^ n - 1)
 6. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x < 2 ^ (nm - n)
 7. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> n \<le> nm
 8. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> nm < LENGTH('a) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> 1 \<le> 1
 2. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> 2 ^ m - 1 \<le> 2 ^ m
 3. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> 2 ^ n - 1 \<le> 2 ^ n
 4. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x * 2 ^ n \<le> x * 2 ^ n + (2 ^ n - 1)
 5. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x < 2 ^ (nm - n)
 6. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> n \<le> nm
 7. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> nm < LENGTH('a) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> 2 ^ m - 1 \<le> 2 ^ m
 2. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> 2 ^ n - 1 \<le> 2 ^ n
 3. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x * 2 ^ n \<le> x * 2 ^ n + (2 ^ n - 1)
 4. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x < 2 ^ (nm - n)
 5. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> n \<le> nm
 6. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> nm < LENGTH('a) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> 2 ^ n - 1 \<le> 2 ^ n
 2. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x * 2 ^ n \<le> x * 2 ^ n + (2 ^ n - 1)
 3. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x < 2 ^ (nm - n)
 4. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> n \<le> nm
 5. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> nm < LENGTH('a) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x * 2 ^ n \<le> x * 2 ^ n + (2 ^ n - 1)
 2. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x < 2 ^ (nm - n)
 3. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> n \<le> nm
 4. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> nm < LENGTH('a) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> is_aligned (x * 2 ^ n) ?sz41
 2. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> 2 ^ n - 1 < 2 ^ ?sz41
 3. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x < 2 ^ (nm - n)
 4. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> n \<le> nm
 5. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> nm < LENGTH('a) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> 2 ^ n - 1 < 2 ^ n
 2. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x < 2 ^ (nm - n)
 3. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> n \<le> nm
 4. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> nm < LENGTH('a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> x < 2 ^ (nm - n)
 2. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> n \<le> nm
 3. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> nm < LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> n \<le> nm
 2. \<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a); x \<le> 2 ^ (nm - n) - 1\<rbrakk> \<Longrightarrow> nm < LENGTH('a) proof (prove)
goal:
No subgoals!