Theory More_Arithmetic

(*
 * Copyright Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section ‹Arithmetic lemmas›

theory More_Arithmetic
  imports Main "HOL-Library.Type_Length"
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
    by (subst power_add [symmetric]) simp
qed

lemma nat_le_power_trans:
  fixes n :: nat
  shows "⟦n ≤ 2 ^ (m - k); k ≤ m⟧ ⟹ 2 ^ k * n ≤ 2 ^ m"
  by (metis le_add_diff_inverse mult_le_mono2 semiring_normalization_rules(26))

lemma nat_add_offset_less:
  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"
    by (auto dest: less_imp_add_positive)

  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
      by (simp add: ac_simps ih)
  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 (simp add: le_Suc_ex)
  apply (clarsimp simp: power_add)
  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 only: power_add[symmetric] nat_minus_add_max)
  apply (simp only: power_add[symmetric] nat_minus_add_max ac_simps)
  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

end