theory Word_Lemmas

lemma unat_shiftl_less_t2n:
  \<open>unat (x << n) < 2 ^ m\<close>
  if \<open>unat (x :: 'a :: len word) < 2 ^ (m - n)\<close> \<open>m < LENGTH('a)\<close> proof (cases \<open>n \<le> m\<close>) case False with that show ?thesis apply (transfer fixing: m n) apply (simp add: not_le take_bit_push_bit) apply (metis diff_le_self order_le_less_trans push_bit_of_0 take_bit_0 take_bit_int_eq_self
      take_bit_int_less_exp take_bit_nonnegative take_bit_tightened) done next case True moreover define q r where \<open>q = m - n\<close> and \<open>r = LENGTH('a) - n - q\<close> ultimately have \<open>m - n = q\<close> \<open>m = n + q\<close> \<open>LENGTH('a) = r + q + n\<close> using that by simp_all with that show ?thesis apply (transfer fixing: m n q r) apply (simp add: not_le take_bit_push_bit) apply (simp add: push_bit_eq_mult power_add) using take_bit_tightened_less_eq_int [of \<open>r + q\<close> \<open>r + q + n\<close>] apply (rule le_less_trans) apply simp_all done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (x << n) < 2 ^ m proof (state)
goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> unat (x << n) < 2 ^ m
 2. \<not> n \<le> m \<Longrightarrow> unat (x << n) < 2 ^ m proof (state)
this:
\<not> n \<le> m

goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> unat (x << n) < 2 ^ m
 2. \<not> n \<le> m \<Longrightarrow> unat (x << n) < 2 ^ m proof (chain)
picking this:
unat x < 2 ^ (m - n)
m < LENGTH('a)
\<not> n \<le> m proof (prove)
using this:
unat x < 2 ^ (m - n)
m < LENGTH('a)
\<not> n \<le> m

goal (1 subgoal):
 1. unat (x << n) < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(nat \<circ> take_bit LENGTH('a)) x < 2 ^ (m - n); m < LENGTH('a); \<not> n \<le> m\<rbrakk> \<Longrightarrow> (nat \<circ> take_bit LENGTH('a)) (push_bit n x) < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>take_bit LENGTH('a) x \<le> 0; m < LENGTH('a); m < n\<rbrakk> \<Longrightarrow> push_bit n (take_bit (LENGTH('a) - n) x) < 2 ^ m proof (prove)
goal:
No subgoals! proof (state)
this:
unat (x << n) < 2 ^ m

goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> unat (x << n) < 2 ^ m proof (state)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> unat (x << n) < 2 ^ m proof (state)
this:
n \<le> m

goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> unat (x << n) < 2 ^ m proof (state)
this:
n \<le> m

goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> unat (x << n) < 2 ^ m proof (state)
this:
q = m - n
r = LENGTH('a) - n - q

goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> unat (x << n) < 2 ^ m proof (chain)
picking this:
n \<le> m
q = m - n
r = LENGTH('a) - n - q proof (prove)
using this:
n \<le> m
q = m - n
r = LENGTH('a) - n - q

goal (1 subgoal):
 1. m - n = q &&& m = n + q &&& LENGTH('a) = r + q + n proof (prove)
using this:
n \<le> m
q = m - n
r = LENGTH('a) - n - q
unat x < 2 ^ (m - n)
m < LENGTH('a)

goal (1 subgoal):
 1. m - n = q &&& m = n + q &&& LENGTH('a) = r + q + n proof (state)
this:
m - n = q
m = n + q
LENGTH('a) = r + q + n

goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> unat (x << n) < 2 ^ m proof (chain)
picking this:
unat x < 2 ^ (m - n)
m < LENGTH('a)
m - n = q
m = n + q
LENGTH('a) = r + q + n proof (prove)
using this:
unat x < 2 ^ (m - n)
m < LENGTH('a)
m - n = q
m = n + q
LENGTH('a) = r + q + n

goal (1 subgoal):
 1. unat (x << n) < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(nat \<circ> take_bit LENGTH('a)) x < 2 ^ (m - n); m < LENGTH('a); m - n = q; m = n + q; LENGTH('a) = r + q + n\<rbrakk> \<Longrightarrow> (nat \<circ> take_bit LENGTH('a)) (push_bit n x) < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>take_bit (r + q + n) x < 2 ^ q; 0 < r; m = n + q; LENGTH('a) = r + q + n\<rbrakk> \<Longrightarrow> push_bit n (take_bit (r + q) x) < 2 ^ (n + q) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>take_bit (r + q + n) x < 2 ^ q; 0 < r; m = n + q; LENGTH('a) = r + q + n\<rbrakk> \<Longrightarrow> take_bit (r + q) x < 2 ^ q proof (prove)
using this:
r + q \<le> r + q + n \<Longrightarrow> take_bit (r + q) ?k \<le> take_bit (r + q + n) ?k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>take_bit (r + q + n) x < 2 ^ q; 0 < r; m = n + q; LENGTH('a) = r + q + n\<rbrakk> \<Longrightarrow> take_bit (r + q) x < 2 ^ q proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>take_bit (r + q + n) x < 2 ^ q; 0 < r; m = n + q; LENGTH('a) = r + q + n\<rbrakk> \<Longrightarrow> r + q \<le> r + q + n
 2. \<And>x. \<lbrakk>take_bit (r + q + n) x < 2 ^ q; 0 < r; m = n + q; LENGTH('a) = r + q + n\<rbrakk> \<Longrightarrow> take_bit (r + q + n) x < 2 ^ q proof (prove)
goal:
No subgoals! proof (state)
this:
unat (x << n) < 2 ^ m

goal:
No subgoals!