theory More_Word

lemma of_nat_less_two_pow_div_set:
  "\<lbrakk> n < LENGTH('a) \<rbrakk> \<Longrightarrow>
   {x. x < (2 ^ n div 2 ^ m :: 'a::len word)}
      = of_nat ` {k. k < 2 ^ n div 2 ^ m}" apply (simp add: image_def) apply (safe dest!: word_less_two_pow_divD less_two_pow_divD
             intro!: word_less_two_pow_divI) apply (rule_tac x="unat x" in exI) apply (simp add: power_sub[symmetric]) apply (subst unat_power_lower[symmetric, where 'a='a]) apply simp apply (erule unat_mono) apply (subst word_unat_power) apply (rule of_nat_mono_maybe) apply (rule power_strict_increasing) apply simp apply simp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> {x. x < 2 ^ n div 2 ^ m} = word_of_nat ` {k. k < 2 ^ n div 2 ^ m} proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> {x. x < 2 ^ n div 2 ^ m} = {y. \<exists>x<2 ^ n div 2 ^ m. y = word_of_nat x} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n < LENGTH('a); m \<le> n; x < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> \<exists>xa<2 ^ n div 2 ^ m. x = word_of_nat xa
 2. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> word_of_nat xa < 2 ^ (n - m) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n < LENGTH('a); m \<le> n; x < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> unat x < 2 ^ n div 2 ^ m \<and> x = word_of_nat (unat x)
 2. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> word_of_nat xa < 2 ^ (n - m) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n < LENGTH('a); m \<le> n; x < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> unat x < 2 ^ (n - m)
 2. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> word_of_nat xa < 2 ^ (n - m) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>n < LENGTH('a); m \<le> n; x < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> n - m < LENGTH('a)
 2. \<And>x. \<lbrakk>n < LENGTH('a); m \<le> n; x < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> unat x < unat (2 ^ (n - m))
 3. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> word_of_nat xa < 2 ^ (n - m) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n < LENGTH('a); m \<le> n; x < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> unat x < unat (2 ^ (n - m))
 2. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> word_of_nat xa < 2 ^ (n - m) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> word_of_nat xa < 2 ^ (n - m) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> word_of_nat xa < word_of_nat (2 ^ (n - m)) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> 2 ^ (n - m) < 2 ^ LENGTH('a)
 2. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> xa < 2 ^ (n - m) proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> n - m < LENGTH('a)
 2. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> xa < 2 ^ (n - m) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> 1 < 2
 2. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> xa < 2 ^ (n - m) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>n < LENGTH('a); m \<le> n; xa < 2 ^ (n - m)\<rbrakk> \<Longrightarrow> xa < 2 ^ (n - m) proof (prove)
goal:
No subgoals!