Theory Karatsuba_Sqrt_Library

subsection ‹Auxiliary material›
theory Karatsuba_Sqrt_Library
imports
  "HOL-Library.Discrete_Functions"
  "HOL-Library.Log_Nat"
begin

subsection ‹Efficient simultaneous computation of div› and mod›

definition divmod_int :: "int  int  int × int" where
  "divmod_int a b = (a div b, a mod b)"

lemma divmod_int_code [code]:
  "divmod_int a b =
     (case divmod_integer (integer_of_int a) (integer_of_int b) of
       (q, r)  (int_of_integer q, int_of_integer r))"
  by (simp add: divmod_int_def divmod_integer_def)


subsubsection ‹Missing lemmas about constbitlen

lemma drop_bit_eq_0_iff_nat:
  "drop_bit k (n :: nat) = 0  bitlen n  k"
  by (auto simp: drop_bit_eq_div div_eq_0_iff less_power_nat_iff_bitlen)

lemma drop_bit_eq_0_iff_int:
  assumes "n  0"
  shows   "drop_bit k (n :: int) = 0  bitlen n  k"
  by (metis assms drop_bit_eq_0_iff_nat drop_bit_nat_eq drop_bit_of_nat nat_0_le nat_zero_as_int of_nat_0)

lemma drop_bit_bitlen_minus_1: 
  assumes "n > 0"
  shows   "drop_bit (nat (bitlen n - 1)) n = 1"
proof -
  define s where "s = nat (bitlen n - 1)"
  have "bitlen n > 0"
    using assms by (simp add: bitlen_eq_zero_iff bitlen_nonneg order_less_le)
  have "drop_bit s n  drop_bit s (mask (s+1))"
    unfolding drop_bit_eq_div mask_eq_exp_minus_1
    using bitlen n > 0 bitlen_bounds[of n] assms
    by (intro zdiv_mono1)
       (auto simp: s_def nat_diff_distrib simp del: power_Suc)
  also have "drop_bit s (mask (s + 1) :: int) = 1"
    by (simp add: drop_bit_mask_eq)
  finally have "drop_bit s n  1" .
  moreover have "drop_bit s n  0"
    using assms bitlen n > 0
    by (subst drop_bit_eq_0_iff_int) (auto simp: s_def)
  moreover have "drop_bit s n  0"
    using assms by auto
  ultimately show "drop_bit s n = 1"
    by linarith
qed

lemma bitlen_pos: "n > 0  bitlen n > 0"
  using bitlen_def bitlen_eq_zero_iff linorder_not_less by auto

lemma bit_bitlen_minus_1: 
  assumes "n > 0"
  shows   "bit n (nat (bitlen n - 1))"
  using drop_bit_bitlen_minus_1[OF assms]
  by (simp add: bit_iff_and_drop_bit_eq_1)

lemma not_bit_ge_bitlen:
  assumes "int k  bitlen n" "n  0"
  shows   "¬bit n k"
proof
  assume "bit n k"
  hence "odd (n div 2 ^ k)"
    by (auto simp: bit_iff_odd)
  hence "n  2 ^ k"
    using assms(2) linorder_not_le by fastforce 
  hence "int k < bitlen n"
    by (metis bitlen_le_iff_power linorder_not_less nat_int)
  thus False
    using assms by auto
qed

lemma bitlen_eqI:
  assumes "bit n (nat k - 1)" "i. int i  k  ¬bit n i" "k > 0" "n  0"
  shows   "bitlen n = k"
proof -
  from assms(1) have "n  0"
    by auto
  with n  0 have "n > 0"
    by auto
  show ?thesis
  proof (cases "bitlen n" k rule: linorder_cases)
    assume "bitlen n > k"
    hence False
      using assms(2)[of "nat (bitlen n - 1)"] bit_bitlen_minus_1[of n] n > 0
      by (auto split: if_splits simp: bitlen_pos)
    thus ?thesis ..
  next
    assume "bitlen n < k"
    hence False
      using assms(1) k > 0 not_bit_ge_bitlen[of n "nat k - 1"] n > 0
      by (auto simp: of_nat_diff)
    thus ?thesis ..
  qed auto
qed

lemma bitlen_drop_bit:
  assumes "n  0"
  shows   "bitlen (drop_bit k n) = max 0 (bitlen n - k)"
proof (cases "bitlen n > k")
  case False
  hence "drop_bit k n = 0"
    using assms by (subst drop_bit_eq_0_iff_int) auto
  thus ?thesis using False
    by simp
next
  case True
  hence "n  0"
    by auto
  with assms have "n > 0"
    by auto
  show ?thesis
  proof (rule bitlen_eqI)
    show "bit (drop_bit k n) (nat (max 0 (bitlen n - int k)) - 1)"
      using True bit_bitlen_minus_1[of n] n > 0
      by (auto simp: bit_drop_bit_eq nat_diff_distrib)
  next
    fix i :: nat
    assume "max 0 (bitlen n - int k)  int i"
    hence "int (i + k)  bitlen n"
      using True by simp
    thus "¬ bit (drop_bit k n) i"
      using n > 0 by (auto simp: bit_drop_bit_eq not_bit_ge_bitlen)
  qed (use True n > 0 in auto)
qed


subsubsection ‹Missing lemmas about constfloor_sqrt

lemma Discrete_sqrt_lessI:
  assumes "x < y ^ 2"
  shows   "floor_sqrt x < y"
  using assms le_floor_sqrt_iff linorder_not_less by blast

lemma floor_sqrt_conv_floor_of_sqrt:
  "floor_sqrt n = nat (floor (sqrt n))"
proof (rule floor_sqrt_unique)
  have "real (nat (floor (sqrt n)) ^ 2) = real_of_int sqrt (real n) ^ 2"
    by simp
  also have "  sqrt (real n) ^ 2"
    by (intro power_mono) auto
  also have " = real n"
    by simp
  finally show "nat (floor (sqrt n)) ^ 2  n"
    by linarith
next
  have "sqrt (real n) ^ 2 < (real_of_int sqrt (real n) + 1) ^ 2"
    by (rule power_strict_mono) auto
  hence "real n < (real_of_int sqrt (real n) + 1) ^ 2"
    by simp
  also have " = real ((Suc (nat (floor (sqrt n)))) ^ 2)"
    by simp
  finally show "n < Suc (nat (floor (sqrt n))) ^ 2"
    by linarith
qed


subsection ‹Miscellaneous›

lemma Let_cong:
  assumes "a = c" "x. x = a  b x = d x"
  shows   "Let a b = Let c d"
  unfolding Let_def using assms by simp

lemma case_prod_cong:
  assumes "a = b" "x y. a = (x, y)  f x y = g x y"
  shows   "(case a of (x, y)  f x y) = (case b of (x, y)  g x y)"
  using assms by (auto simp: case_prod_unfold)

end