theory More_Word

lemma word_less_two_pow_divD:
  "\<lbrakk> (x :: 'a::len word) < 2 ^ n div 2 ^ m \<rbrakk>
     \<Longrightarrow> n \<ge> m \<and> (x < 2 ^ (n - m))" apply (cases "n < LENGTH('a)") apply (cases "m < LENGTH('a)") apply (simp add: word_less_nat_alt) apply (subst(asm) unat_word_ariths) apply (subst(asm) mod_less) apply (rule order_le_less_trans [OF div_le_dividend]) apply (rule unat_lt2p) apply (clarsimp dest!: less_two_pow_divD) apply (simp add: power_overflow) apply (simp add: word_div_def) apply (simp add: power_overflow word_div_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ n div 2 ^ m \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < 2 ^ n div 2 ^ m; n < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m)
 2. \<lbrakk>x < 2 ^ n div 2 ^ m; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x < 2 ^ n div 2 ^ m; n < LENGTH('a); m < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m)
 2. \<lbrakk>x < 2 ^ n div 2 ^ m; n < LENGTH('a); \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m)
 3. \<lbrakk>x < 2 ^ n div 2 ^ m; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>unat x < unat (2 ^ n div 2 ^ m); n < LENGTH('a); m < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> unat x < 2 ^ (n - m)
 2. \<lbrakk>x < 2 ^ n div 2 ^ m; n < LENGTH('a); \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m)
 3. \<lbrakk>x < 2 ^ n div 2 ^ m; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>unat x < unat (2 ^ n) div unat (2 ^ m) mod 2 ^ LENGTH('a); n < LENGTH('a); m < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> unat x < 2 ^ (n - m)
 2. \<lbrakk>x < 2 ^ n div 2 ^ m; n < LENGTH('a); \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m)
 3. \<lbrakk>x < 2 ^ n div 2 ^ m; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n < LENGTH('a); m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ n) div unat (2 ^ m) < 2 ^ LENGTH('a)
 2. \<lbrakk>unat x < unat (2 ^ n) div unat (2 ^ m); n < LENGTH('a); m < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> unat x < 2 ^ (n - m)
 3. \<lbrakk>x < 2 ^ n div 2 ^ m; n < LENGTH('a); \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m)
 4. \<lbrakk>x < 2 ^ n div 2 ^ m; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n < LENGTH('a); m < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ n) < 2 ^ LENGTH('a)
 2. \<lbrakk>unat x < unat (2 ^ n) div unat (2 ^ m); n < LENGTH('a); m < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> unat x < 2 ^ (n - m)
 3. \<lbrakk>x < 2 ^ n div 2 ^ m; n < LENGTH('a); \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m)
 4. \<lbrakk>x < 2 ^ n div 2 ^ m; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>unat x < unat (2 ^ n) div unat (2 ^ m); n < LENGTH('a); m < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> unat x < 2 ^ (n - m)
 2. \<lbrakk>x < 2 ^ n div 2 ^ m; n < LENGTH('a); \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m)
 3. \<lbrakk>x < 2 ^ n div 2 ^ m; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < 2 ^ n div 2 ^ m; n < LENGTH('a); \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m)
 2. \<lbrakk>x < 2 ^ n div 2 ^ m; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n div 2 ^ m; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < word_of_int (uint (2 ^ n) div uint (2 ^ m)); \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> m \<le> n \<and> x < 2 ^ (n - m) proof (prove)
goal:
No subgoals!