theory More_Word

lemma word_less_power_trans:
  fixes n :: "'a :: len word"
  assumes nv: "n < 2 ^ (m - k)"
  and     kv: "k \<le> m"
  and     mv: "m < len_of TYPE ('a)"
  shows "2 ^ k * n < 2 ^ m" using nv kv mv apply - apply (subst word_less_nat_alt) apply (subst unat_word_ariths) apply (subst mod_less) apply simp apply (rule nat_less_power_trans) apply (erule order_less_trans [OF unat_mono]) apply simp apply simp apply simp apply (rule nat_less_power_trans) apply (subst unat_power_lower[where 'a = 'a, symmetric]) apply simp apply (erule unat_mono) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * n < 2 ^ m proof (prove)
using this:
n < 2 ^ (m - k)
k \<le> m
m < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ k * n < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ k * n < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ k * n) < unat (2 ^ m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ k) * unat n mod 2 ^ LENGTH('a) < unat (2 ^ m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ k) * unat n < 2 ^ LENGTH('a)
 2. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ k) * unat n < unat (2 ^ m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ k * unat n < 2 ^ LENGTH('a)
 2. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ k) * unat n < unat (2 ^ m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat n < 2 ^ (LENGTH('a) - k)
 2. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> k \<le> LENGTH('a)
 3. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ k) * unat n < unat (2 ^ m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ (m - k)) < 2 ^ (LENGTH('a) - k)
 2. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> k \<le> LENGTH('a)
 3. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ k) * unat n < unat (2 ^ m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> k \<le> LENGTH('a)
 2. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ k) * unat n < unat (2 ^ m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ k) * unat n < unat (2 ^ m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ k * unat n < 2 ^ m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat n < 2 ^ (m - k)
 2. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> k \<le> m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> m - k < LENGTH('a)
 2. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat n < unat (2 ^ (m - k))
 3. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> k \<le> m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat n < unat (2 ^ (m - k))
 2. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> k \<le> m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> k \<le> m proof (prove)
goal:
No subgoals!