theory More_Word

lemma alignUp_div_helper:
  fixes a :: "'a::len word"
  assumes kv: "k < 2 ^ (LENGTH('a) - n)"
  and     xk: "x = 2 ^ n * of_nat k"
  and    le: "a \<le> x"
  and    sz: "n < LENGTH('a)"
  and   anz: "a mod 2 ^ n \<noteq> 0"
  shows "a div 2 ^ n < of_nat k" proof - have kn: "unat (of_nat k :: 'a word) * unat ((2::'a word) ^ n) < 2 ^ LENGTH('a)" using xk kv sz apply (subst unat_of_nat_eq) apply (erule order_less_le_trans) apply simp apply (subst unat_power_lower, simp) apply (subst mult.commute) apply (rule nat_less_power_trans) apply simp apply simp done have "unat a div 2 ^ n * 2 ^ n \<noteq> unat a" proof - have "unat a = unat a div 2 ^ n * 2 ^ n + unat a mod 2 ^ n" by (simp add: div_mult_mod_eq) also have "\<dots> \<noteq> unat a div 2 ^ n * 2 ^ n" using sz anz by (simp add: unat_arith_simps) finally show ?thesis .. qed then have "a div 2 ^ n * 2 ^ n < a" using sz anz apply (subst word_less_nat_alt) apply (subst unat_word_ariths) apply (subst unat_div) apply simp apply (rule order_le_less_trans [OF mod_less_eq_dividend]) apply (erule order_le_neq_trans [OF div_mult_le]) done also from xk le have "\<dots> \<le> of_nat k * 2 ^ n" by (simp add: field_simps) finally show ?thesis using sz kv apply - apply (erule word_mult_less_dest [OF _ _ kn]) apply (simp add: unat_div) apply (rule order_le_less_trans [OF div_mult_le]) apply (rule unat_lt2p) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k proof (state)
goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat k) * unat (2 ^ n) < 2 ^ LENGTH('a) proof (prove)
using this:
x = 2 ^ n * word_of_nat k
k < 2 ^ (LENGTH('a) - n)
n < LENGTH('a)

goal (1 subgoal):
 1. unat (word_of_nat k) * unat (2 ^ n) < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> k < 2 ^ LENGTH('a)
 2. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> k * unat (2 ^ n) < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH('a) - n) \<le> 2 ^ LENGTH('a)
 2. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> k * unat (2 ^ n) < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> k * unat (2 ^ n) < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> k * 2 ^ n < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n * k < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> k < 2 ^ (LENGTH('a) - n)
 2. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> n \<le> LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> n \<le> LENGTH('a) proof (prove)
goal:
No subgoals! proof (state)
this:
unat (word_of_nat k) * unat (2 ^ n) < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k proof (prove)
goal (1 subgoal):
 1. unat a div 2 ^ n * 2 ^ n \<noteq> unat a proof (state)
goal (1 subgoal):
 1. unat a div 2 ^ n * 2 ^ n \<noteq> unat a proof (prove)
goal (1 subgoal):
 1. unat a = unat a div 2 ^ n * 2 ^ n + unat a mod 2 ^ n proof (state)
this:
unat a = unat a div 2 ^ n * 2 ^ n + unat a mod 2 ^ n

goal (1 subgoal):
 1. unat a div 2 ^ n * 2 ^ n \<noteq> unat a proof (state)
this:
unat a = unat a div 2 ^ n * 2 ^ n + unat a mod 2 ^ n

goal (1 subgoal):
 1. unat a div 2 ^ n * 2 ^ n \<noteq> unat a proof (prove)
goal (1 subgoal):
 1. unat a div 2 ^ n * 2 ^ n + unat a mod 2 ^ n \<noteq> unat a div 2 ^ n * 2 ^ n proof (prove)
using this:
n < LENGTH('a)
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. unat a div 2 ^ n * 2 ^ n + unat a mod 2 ^ n \<noteq> unat a div 2 ^ n * 2 ^ n proof (state)
this:
unat a div 2 ^ n * 2 ^ n + unat a mod 2 ^ n \<noteq> unat a div 2 ^ n * 2 ^ n

goal (1 subgoal):
 1. unat a div 2 ^ n * 2 ^ n \<noteq> unat a proof (chain)
picking this:
unat a \<noteq> unat a div 2 ^ n * 2 ^ n proof (prove)
using this:
unat a \<noteq> unat a div 2 ^ n * 2 ^ n

goal (1 subgoal):
 1. unat a div 2 ^ n * 2 ^ n \<noteq> unat a proof (state)
this:
unat a div 2 ^ n * 2 ^ n \<noteq> unat a

goal:
No subgoals! proof (state)
this:
unat a div 2 ^ n * 2 ^ n \<noteq> unat a

goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k proof (chain)
picking this:
unat a div 2 ^ n * 2 ^ n \<noteq> unat a proof (prove)
using this:
unat a div 2 ^ n * 2 ^ n \<noteq> unat a

goal (1 subgoal):
 1. a div 2 ^ n * 2 ^ n < a proof (prove)
using this:
unat a div 2 ^ n * 2 ^ n \<noteq> unat a
n < LENGTH('a)
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. a div 2 ^ n * 2 ^ n < a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat a div 2 ^ n * 2 ^ n \<noteq> unat a; n < LENGTH('a); a mod 2 ^ n \<noteq> 0\<rbrakk> \<Longrightarrow> unat (a div 2 ^ n * 2 ^ n) < unat a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat a div 2 ^ n * 2 ^ n \<noteq> unat a; n < LENGTH('a); a mod 2 ^ n \<noteq> 0\<rbrakk> \<Longrightarrow> unat (a div 2 ^ n) * unat (2 ^ n) mod 2 ^ LENGTH('a) < unat a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat a div 2 ^ n * 2 ^ n \<noteq> unat a; n < LENGTH('a); a mod 2 ^ n \<noteq> 0\<rbrakk> \<Longrightarrow> unat a div unat (2 ^ n) * unat (2 ^ n) mod 2 ^ LENGTH('a) < unat a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat a div 2 ^ n * 2 ^ n \<noteq> unat a; n < LENGTH('a); a mod 2 ^ n \<noteq> 0\<rbrakk> \<Longrightarrow> unat a div 2 ^ n * 2 ^ n mod 2 ^ LENGTH('a) < unat a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat a div 2 ^ n * 2 ^ n \<noteq> unat a; n < LENGTH('a); a mod 2 ^ n \<noteq> 0\<rbrakk> \<Longrightarrow> unat a div 2 ^ n * 2 ^ n < unat a proof (prove)
goal:
No subgoals! proof (state)
this:
a div 2 ^ n * 2 ^ n < a

goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k proof (state)
this:
a div 2 ^ n * 2 ^ n < a

goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k proof (chain)
picking this:
x = 2 ^ n * word_of_nat k
a \<le> x proof (prove)
using this:
x = 2 ^ n * word_of_nat k
a \<le> x

goal (1 subgoal):
 1. a \<le> word_of_nat k * 2 ^ n proof (state)
this:
a \<le> word_of_nat k * 2 ^ n

goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k proof (chain)
picking this:
a div 2 ^ n * 2 ^ n < word_of_nat k * 2 ^ n proof (prove)
using this:
a div 2 ^ n * 2 ^ n < word_of_nat k * 2 ^ n

goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k proof (prove)
using this:
a div 2 ^ n * 2 ^ n < word_of_nat k * 2 ^ n
n < LENGTH('a)
k < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a div 2 ^ n * 2 ^ n < word_of_nat k * 2 ^ n; n < LENGTH('a); k < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> a div 2 ^ n < word_of_nat k proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); k < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat (a div 2 ^ n) * unat (2 ^ n) < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); k < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat a div 2 ^ n * 2 ^ n < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); k < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> unat a < 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals! proof (state)
this:
a div 2 ^ n < word_of_nat k

goal:
No subgoals!