theory Word_Lemmas

lemma signed_shift_guard_to_word:
  \<open>unat x * 2 ^ y < 2 ^ n \<longleftrightarrow> x = 0 \<or> x < 1 << n >> y\<close>
    if \<open>n < LENGTH('a)\<close> \<open>0 < n\<close>
    for x :: \<open>'a::len word\<close> proof (cases \<open>x = 0\<close>) case True then show ?thesis by simp next case False then have \<open>unat x \<noteq> 0\<close> by (simp add: unat_eq_0) then have \<open>unat x \<ge> 1\<close> by simp show ?thesis proof (cases \<open>y < n\<close>) case False then have \<open>n \<le> y\<close> by simp then obtain q where \<open>y = n + q\<close> using le_Suc_ex by blast moreover have \<open>(2 :: nat) ^ n >> n + q \<le> 1\<close> by (simp add: drop_bit_eq_div power_add shiftr_def) ultimately show ?thesis using \<open>x \<noteq> 0\<close> \<open>unat x \<ge> 1\<close> \<open>n < LENGTH('a)\<close> by (simp add: power_add not_less word_le_nat_alt unat_drop_bit_eq shiftr_def shiftl_def) next case True with that have \<open>y < LENGTH('a)\<close> by simp show ?thesis proof (cases \<open>2 ^ n = unat x * 2 ^ y\<close>) case True moreover have \<open>unat x * 2 ^ y < 2 ^ LENGTH('a)\<close> using \<open>n < LENGTH('a)\<close> by (simp flip: True) moreover have \<open>(word_of_nat (2 ^ n) :: 'a word) = word_of_nat (unat x * 2 ^ y)\<close> using True by simp then have \<open>2 ^ n = x * 2 ^ y\<close> by simp ultimately show ?thesis using \<open>y < LENGTH('a)\<close> by (auto simp add: drop_bit_eq_div word_less_nat_alt unat_div unat_word_ariths
                           shiftr_def shiftl_def) next case False with \<open>y < n\<close> have *: \<open>unat x \<noteq> 2 ^ n div 2 ^ y\<close> by (auto simp flip: power_sub power_add) have \<open>unat x * 2 ^ y < 2 ^ n \<longleftrightarrow> unat x * 2 ^ y \<le> 2 ^ n\<close> using False by (simp add: less_le) also have \<open>\<dots> \<longleftrightarrow> unat x \<le> 2 ^ n div 2 ^ y\<close> by (simp add: less_eq_div_iff_mult_less_eq) also have \<open>\<dots> \<longleftrightarrow> unat x < 2 ^ n div 2 ^ y\<close> using * by (simp add: less_le) finally show ?thesis using that \<open>x \<noteq> 0\<close> by (simp flip: push_bit_eq_mult drop_bit_eq_div
                 add: shiftr_def shiftl_def unat_drop_bit_eq word_less_iff_unsigned [where ?'a = nat]) qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. x \<noteq> 0 \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. x \<noteq> 0 \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (chain)
picking this:
x = 0 proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
(unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (chain)
picking this:
x \<noteq> 0 proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. unat x \<noteq> 0 proof (state)
this:
unat x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (chain)
picking this:
unat x \<noteq> 0 proof (prove)
using this:
unat x \<noteq> 0

goal (1 subgoal):
 1. 1 \<le> unat x proof (state)
this:
1 \<le> unat x

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (prove)
goal (1 subgoal):
 1. (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
goal (2 subgoals):
 1. y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. \<not> y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
\<not> y < n

goal (2 subgoals):
 1. y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. \<not> y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (chain)
picking this:
\<not> y < n proof (prove)
using this:
\<not> y < n

goal (1 subgoal):
 1. n \<le> y proof (state)
this:
n \<le> y

goal (2 subgoals):
 1. y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. \<not> y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (chain)
picking this:
n \<le> y proof (prove)
using this:
n \<le> y

goal (1 subgoal):
 1. (\<And>q. y = n + q \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
n \<le> y
?k \<le> ?l \<Longrightarrow> \<exists>n. ?l = ?k + n

goal (1 subgoal):
 1. (\<And>q. y = n + q \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
y = n + q

goal (2 subgoals):
 1. y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. \<not> y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
y = n + q

goal (2 subgoals):
 1. y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. \<not> y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (prove)
goal (1 subgoal):
 1. 2 ^ n >> n + q \<le> 1 proof (state)
this:
2 ^ n >> n + q \<le> 1

goal (2 subgoals):
 1. y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. \<not> y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (chain)
picking this:
y = n + q
2 ^ n >> n + q \<le> 1 proof (prove)
using this:
y = n + q
2 ^ n >> n + q \<le> 1

goal (1 subgoal):
 1. (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (prove)
using this:
y = n + q
2 ^ n >> n + q \<le> 1
x \<noteq> 0
1 \<le> unat x
n < LENGTH('a)

goal (1 subgoal):
 1. (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
(unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)

goal (1 subgoal):
 1. y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
goal (1 subgoal):
 1. y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
y < n

goal (1 subgoal):
 1. y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (chain)
picking this:
n < LENGTH('a)
0 < n
y < n proof (prove)
using this:
n < LENGTH('a)
0 < n
y < n

goal (1 subgoal):
 1. y < LENGTH('a) proof (state)
this:
y < LENGTH('a)

goal (1 subgoal):
 1. y < n \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (prove)
goal (1 subgoal):
 1. (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
goal (2 subgoals):
 1. 2 ^ n = unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
2 ^ n = unat x * 2 ^ y

goal (2 subgoals):
 1. 2 ^ n = unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
2 ^ n = unat x * 2 ^ y

goal (2 subgoals):
 1. 2 ^ n = unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (prove)
goal (1 subgoal):
 1. unat x * 2 ^ y < 2 ^ LENGTH('a) proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. unat x * 2 ^ y < 2 ^ LENGTH('a) proof (state)
this:
unat x * 2 ^ y < 2 ^ LENGTH('a)

goal (2 subgoals):
 1. 2 ^ n = unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
unat x * 2 ^ y < 2 ^ LENGTH('a)

goal (2 subgoals):
 1. 2 ^ n = unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (prove)
goal (1 subgoal):
 1. word_of_nat (2 ^ n) = word_of_nat (unat x * 2 ^ y) proof (prove)
using this:
2 ^ n = unat x * 2 ^ y

goal (1 subgoal):
 1. word_of_nat (2 ^ n) = word_of_nat (unat x * 2 ^ y) proof (state)
this:
word_of_nat (2 ^ n) = word_of_nat (unat x * 2 ^ y)

goal (2 subgoals):
 1. 2 ^ n = unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (chain)
picking this:
word_of_nat (2 ^ n) = word_of_nat (unat x * 2 ^ y) proof (prove)
using this:
word_of_nat (2 ^ n) = word_of_nat (unat x * 2 ^ y)

goal (1 subgoal):
 1. 2 ^ n = x * 2 ^ y proof (state)
this:
2 ^ n = x * 2 ^ y

goal (2 subgoals):
 1. 2 ^ n = unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)
 2. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (chain)
picking this:
2 ^ n = unat x * 2 ^ y
unat x * 2 ^ y < 2 ^ LENGTH('a)
2 ^ n = x * 2 ^ y proof (prove)
using this:
2 ^ n = unat x * 2 ^ y
unat x * 2 ^ y < 2 ^ LENGTH('a)
2 ^ n = x * 2 ^ y

goal (1 subgoal):
 1. (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (prove)
using this:
2 ^ n = unat x * 2 ^ y
unat x * 2 ^ y < 2 ^ LENGTH('a)
2 ^ n = x * 2 ^ y
y < LENGTH('a)

goal (1 subgoal):
 1. (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
(unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)

goal (1 subgoal):
 1. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
goal (1 subgoal):
 1. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
2 ^ n \<noteq> unat x * 2 ^ y

goal (1 subgoal):
 1. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (chain)
picking this:
y < n
2 ^ n \<noteq> unat x * 2 ^ y proof (prove)
using this:
y < n
2 ^ n \<noteq> unat x * 2 ^ y

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

goal (1 subgoal):
 1. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (prove)
goal (1 subgoal):
 1. (unat x * 2 ^ y < 2 ^ n) = (unat x * 2 ^ y \<le> 2 ^ n) proof (prove)
using this:
2 ^ n \<noteq> unat x * 2 ^ y

goal (1 subgoal):
 1. (unat x * 2 ^ y < 2 ^ n) = (unat x * 2 ^ y \<le> 2 ^ n) proof (state)
this:
(unat x * 2 ^ y < 2 ^ n) = (unat x * 2 ^ y \<le> 2 ^ n)

goal (1 subgoal):
 1. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
(unat x * 2 ^ y < 2 ^ n) = (unat x * 2 ^ y \<le> 2 ^ n)

goal (1 subgoal):
 1. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (prove)
goal (1 subgoal):
 1. (unat x * 2 ^ y \<le> 2 ^ n) = (unat x \<le> 2 ^ n div 2 ^ y) proof (state)
this:
(unat x * 2 ^ y \<le> 2 ^ n) = (unat x \<le> 2 ^ n div 2 ^ y)

goal (1 subgoal):
 1. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
(unat x * 2 ^ y \<le> 2 ^ n) = (unat x \<le> 2 ^ n div 2 ^ y)

goal (1 subgoal):
 1. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (prove)
goal (1 subgoal):
 1. (unat x \<le> 2 ^ n div 2 ^ y) = (unat x < 2 ^ n div 2 ^ y) proof (prove)
using this:
unat x \<noteq> 2 ^ n div 2 ^ y

goal (1 subgoal):
 1. (unat x \<le> 2 ^ n div 2 ^ y) = (unat x < 2 ^ n div 2 ^ y) proof (state)
this:
(unat x \<le> 2 ^ n div 2 ^ y) = (unat x < 2 ^ n div 2 ^ y)

goal (1 subgoal):
 1. 2 ^ n \<noteq> unat x * 2 ^ y \<Longrightarrow> (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (chain)
picking this:
(unat x * 2 ^ y < 2 ^ n) = (unat x < 2 ^ n div 2 ^ y) proof (prove)
using this:
(unat x * 2 ^ y < 2 ^ n) = (unat x < 2 ^ n div 2 ^ y)

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

goal (1 subgoal):
 1. (unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y) proof (state)
this:
(unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)

goal:
No subgoals! proof (state)
this:
(unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)

goal:
No subgoals! proof (state)
this:
(unat x * 2 ^ y < 2 ^ n) = (x = 0 \<or> x < 1 << n >> y)

goal:
No subgoals!