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 \<^const>‹bitlen››
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 \<^const>‹floor_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