# Theory Word_Lib.More_Arithmetic

(*
* Copyright Data61, CSIRO (ABN 41 687 119 230)
*
*)

section ‹Arithmetic lemmas›

theory More_Arithmetic
imports Main
begin

lemma n_less_equal_power_2:
"n < 2 ^ n"
by (fact less_exp)

lemma min_pm [simp]: "min a b + (a - b) = a"
for a b :: nat
by arith

lemma min_pm1 [simp]: "a - b + min a b = a"
for a b :: nat
by arith

lemma rev_min_pm [simp]: "min b a + (a - b) = a"
for a b :: nat
by arith

lemma rev_min_pm1 [simp]: "a - b + min b a = a"
for a b :: nat
by arith

lemma min_minus [simp]: "min m (m - k) = m - k"
for m k :: nat
by arith

lemma min_minus' [simp]: "min (m - k) m = m - k"
for m k :: nat
by arith

lemma nat_less_power_trans:
fixes n :: nat
assumes nv: "n < 2 ^ (m - k)"
and     kv: "k  m"
shows "2 ^ k * n < 2 ^ m"
proof (rule order_less_le_trans)
show "2 ^ k * n < 2 ^ k * 2 ^ (m - k)"
by (rule mult_less_mono2 [OF nv zero_less_power]) simp
show "(2::nat) ^ k * 2 ^ (m - k)  2 ^ m" using nv kv
qed

lemma nat_le_power_trans:
fixes n :: nat
shows "n  2 ^ (m - k); k  m  2 ^ k * n  2 ^ m"

fixes x :: nat
assumes yv: "y < 2 ^ n"
and     xv: "x < 2 ^ m"
and     mn: "sz = m + n"
shows   "x * 2 ^ n + y < 2 ^ sz"
proof (subst mn)
from yv obtain qy where "y + qy = 2 ^ n" and "0 < qy"

have "x * 2 ^ n + y < x * 2 ^ n + 2 ^ n" by simp fact+
also have " = (x + 1) * 2 ^ n" by simp
also have "  2 ^ (m + n)" using xv
by (subst power_add) (rule mult_le_mono1, simp)
finally show "x * 2 ^ n + y < 2 ^ (m + n)" .
qed

lemma nat_power_less_diff:
assumes lt: "(2::nat) ^ n * q < 2 ^ m"
shows "q < 2 ^ (m - n)"
using lt
proof (induct n arbitrary: m)
case 0
then show ?case by simp
next
case (Suc n)

have ih: "m. 2 ^ n * q < 2 ^ m  q < 2 ^ (m - n)"
and prem: "2 ^ Suc n * q < 2 ^ m" by fact+

show ?case
proof (cases m)
case 0
then show ?thesis using Suc by simp
next
case (Suc m')
then show ?thesis using prem
qed
qed

lemma power_2_mult_step_le:
"n'  n; 2 ^ n' * k' < 2 ^ n * k  2 ^ n' * (k' + 1)  2 ^ n * (k::nat)"
apply (cases "n'=n", simp)
apply (metis Suc_leI le_refl mult_Suc_right mult_le_mono semiring_normalization_rules(7))
apply (drule (1) le_neq_trans)
apply clarsimp
apply (subgoal_tac "m. n = n' + m")
prefer 2
apply (metis Suc_leI mult.assoc mult_Suc_right nat_mult_le_cancel_disj)
done

lemma nat_mult_power_less_eq:
"b > 0  (a * b ^ n < (b :: nat) ^ m) = (a < b ^ (m - n))"
using mult_less_cancel2[where m = a and k = "b ^ n" and n="b ^ (m - n)"]
mult_less_cancel2[where m="a * b ^ (n - m)" and k="b ^ m" and n=1]
apply (simp add: max_def split: if_split_asm)
done

lemma diff_diff_less:
"(i < m - (m - (n :: nat))) = (i < m  i < n)"
by auto

lemma small_powers_of_2:
x < 2 ^ (x - 1) if x  3 for x :: nat
proof -
define m where m = x - 3
with that have x = m + 3
by simp
moreover have m + 3 < 4 * 2 ^ m
by (induction m) simp_all
ultimately show ?thesis
by simp
qed

lemma msrevs:
"0 < n  (k * n + m) div n = m div n + k"
"(k * n + m) mod n = m mod n"
for n :: nat
by simp_all

lemma eq_mod_iff: "0 < n  b = b mod n  0  b  b < n"
for b n :: int
using pos_mod_sign [of n b] pos_mod_bound [of n b] by safe simp_all

end