theory More_Word

lemma word_power_less_diff:
  "\<lbrakk>2 ^ n * q < (2::'a::len word) ^ m; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> q < 2 ^ (m - n)" apply (case_tac "m \<ge> LENGTH('a)") apply (simp add: power_overflow) apply (case_tac "n \<ge> LENGTH('a)") apply (simp add: power_overflow) apply (cases "n = 0") apply simp apply (subst word_less_nat_alt) apply (subst unat_power_lower) apply simp apply (rule nat_power_less_diff) apply (simp add: word_less_nat_alt) apply (subst (asm) iffD1 [OF unat_mult_lem]) apply (simp add:nat_less_power_trans) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> q < 2 ^ (m - n) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); LENGTH('a) \<le> m\<rbrakk> \<Longrightarrow> q < 2 ^ (m - n)
 2. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m\<rbrakk> \<Longrightarrow> q < 2 ^ (m - n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m\<rbrakk> \<Longrightarrow> q < 2 ^ (m - n) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> q < 2 ^ (m - n)
 2. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> q < 2 ^ (m - n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> q < 2 ^ (m - n) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n; n = 0\<rbrakk> \<Longrightarrow> q < 2 ^ (m - n)
 2. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> q < 2 ^ (m - n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> q < 2 ^ (m - n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> unat q < unat (2 ^ (m - n)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> m - n < LENGTH('a)
 2. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> unat q < 2 ^ (m - n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> unat q < 2 ^ (m - n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n * q < 2 ^ m; q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n; n \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ n * unat q < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat (2 ^ n * q) < 2 ^ m; unat q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ n * unat q < 2 ^ m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n; 0 < n\<rbrakk> \<Longrightarrow> unat (2 ^ n) * unat q < 2 ^ LENGTH('a)
 2. \<lbrakk>unat (2 ^ n) * unat q < 2 ^ m; unat q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ n * unat q < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat (2 ^ n) * unat q < 2 ^ m; unat q < 2 ^ (LENGTH('a) - n); \<not> LENGTH('a) \<le> m; \<not> LENGTH('a) \<le> n; 0 < n\<rbrakk> \<Longrightarrow> 2 ^ n * unat q < 2 ^ m proof (prove)
goal:
No subgoals!