Theory HOL-Library.Discrete
section ‹Common discrete functions›
theory Discrete
imports Complex_Main
begin
subsection ‹Discrete logarithm›
context
begin
qualified fun log :: "nat ⇒ nat"
where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
lemma log_induct [consumes 1, case_names one double]:
fixes n :: nat
assumes "n > 0"
assumes one: "P 1"
assumes double: "⋀n. n ≥ 2 ⟹ P (n div 2) ⟹ P n"
shows "P n"
using ‹n > 0› proof (induct n rule: log.induct)
fix n
assume "¬ n < 2 ⟹
0 < n div 2 ⟹ P (n div 2)"
then have *: "n ≥ 2 ⟹ P (n div 2)" by simp
assume "n > 0"
show "P n"
proof (cases "n = 1")
case True
with one show ?thesis by simp
next
case False
with ‹n > 0› have "n ≥ 2" by auto
with * have "P (n div 2)" .
with ‹n ≥ 2› show ?thesis by (rule double)
qed
qed
lemma log_zero [simp]: "log 0 = 0"
by (simp add: log.simps)
lemma log_one [simp]: "log 1 = 0"
by (simp add: log.simps)
lemma log_Suc_zero [simp]: "log (Suc 0) = 0"
using log_one by simp
lemma log_rec: "n ≥ 2 ⟹ log n = Suc (log (n div 2))"
by (simp add: log.simps)
lemma log_twice [simp]: "n ≠ 0 ⟹ log (2 * n) = Suc (log n)"
by (simp add: log_rec)
lemma log_half [simp]: "log (n div 2) = log n - 1"
proof (cases "n < 2")
case True
then have "n = 0 ∨ n = 1" by arith
then show ?thesis by (auto simp del: One_nat_def)
next
case False
then show ?thesis by (simp add: log_rec)
qed
lemma log_exp [simp]: "log (2 ^ n) = n"
by (induct n) simp_all
lemma log_mono: "mono log"
proof
fix m n :: nat
assume "m ≤ n"
then show "log m ≤ log n"
proof (induct m arbitrary: n rule: log.induct)
case (1 m)
then have mn2: "m div 2 ≤ n div 2" by arith
show "log m ≤ log n"
proof (cases "m ≥ 2")
case False
then have "m = 0 ∨ m = 1" by arith
then show ?thesis by (auto simp del: One_nat_def)
next
case True then have "¬ m < 2" by simp
with mn2 have "n ≥ 2" by arith
from True have m2_0: "m div 2 ≠ 0" by arith
with mn2 have n2_0: "n div 2 ≠ 0" by arith
from ‹¬ m < 2› "1.hyps" mn2 have "log (m div 2) ≤ log (n div 2)" by blast
with m2_0 n2_0 have "log (2 * (m div 2)) ≤ log (2 * (n div 2))" by simp
with m2_0 n2_0 ‹m ≥ 2› ‹n ≥ 2› show ?thesis by (simp only: log_rec [of m] log_rec [of n]) simp
qed
qed
qed
lemma log_exp2_le:
assumes "n > 0"
shows "2 ^ log n ≤ n"
using assms
proof (induct n rule: log_induct)
case one
then show ?case by simp
next
case (double n)
with log_mono have "log n ≥ Suc 0"
by (simp add: log.simps)
assume "2 ^ log (n div 2) ≤ n div 2"
with ‹n ≥ 2› have "2 ^ (log n - Suc 0) ≤ n div 2" by simp
then have "2 ^ (log n - Suc 0) * 2 ^ 1 ≤ n div 2 * 2" by simp
with ‹log n ≥ Suc 0› have "2 ^ log n ≤ n div 2 * 2"
unfolding power_add [symmetric] by simp
also have "n div 2 * 2 ≤ n" by (cases "even n") simp_all
finally show ?case .
qed
lemma log_exp2_gt: "2 * 2 ^ log n > n"
proof (cases "n > 0")
case True
thus ?thesis
proof (induct n rule: log_induct)
case (double n)
thus ?case
by (cases "even n") (auto elim!: evenE oddE simp: field_simps log.simps)
qed simp_all
qed simp_all
lemma log_exp2_ge: "2 * 2 ^ log n ≥ n"
using log_exp2_gt[of n] by simp
lemma log_le_iff: "m ≤ n ⟹ log m ≤ log n"
by (rule monoD [OF log_mono])
lemma log_eqI:
assumes "n > 0" "2^k ≤ n" "n < 2 * 2^k"
shows "log n = k"
proof (rule antisym)
from ‹n > 0› have "2 ^ log n ≤ n" by (rule log_exp2_le)
also have "… < 2 ^ Suc k" using assms by simp
finally have "log n < Suc k" by (subst (asm) power_strict_increasing_iff) simp_all
thus "log n ≤ k" by simp
next
have "2^k ≤ n" by fact
also have "… < 2^(Suc (log n))" by (simp add: log_exp2_gt)
finally have "k < Suc (log n)" by (subst (asm) power_strict_increasing_iff) simp_all
thus "k ≤ log n" by simp
qed
lemma log_altdef: "log n = (if n = 0 then 0 else nat ⌊Transcendental.log 2 (real_of_nat n)⌋)"
proof (cases "n = 0")
case False
have "⌊Transcendental.log 2 (real_of_nat n)⌋ = int (log n)"
proof (rule floor_unique)
from False have "2 powr (real (log n)) ≤ real n"
by (simp add: powr_realpow log_exp2_le)
hence "Transcendental.log 2 (2 powr (real (log n))) ≤ Transcendental.log 2 (real n)"
using False by (subst Transcendental.log_le_cancel_iff) simp_all
also have "Transcendental.log 2 (2 powr (real (log n))) = real (log n)" by simp
finally show "real_of_int (int (log n)) ≤ Transcendental.log 2 (real n)" by simp
next
have "real n < real (2 * 2 ^ log n)"
by (subst of_nat_less_iff) (rule log_exp2_gt)
also have "… = 2 powr (real (log n) + 1)"
by (simp add: powr_add powr_realpow)
finally have "Transcendental.log 2 (real n) < Transcendental.log 2 …"
using False by (subst Transcendental.log_less_cancel_iff) simp_all
also have "… = real (log n) + 1" by simp
finally show "Transcendental.log 2 (real n) < real_of_int (int (log n)) + 1" by simp
qed
thus ?thesis by simp
qed simp_all
subsection ‹Discrete square root›
qualified definition sqrt :: "nat ⇒ nat"
where "sqrt n = Max {m. m⇧2 ≤ n}"
lemma sqrt_aux:
fixes n :: nat
shows "finite {m. m⇧2 ≤ n}" and "{m. m⇧2 ≤ n} ≠ {}"
proof -
{ fix m
assume "m⇧2 ≤ n"
then have "m ≤ n"
by (cases m) (simp_all add: power2_eq_square)
} note ** = this
then have "{m. m⇧2 ≤ n} ⊆ {m. m ≤ n}" by auto
then show "finite {m. m⇧2 ≤ n}" by (rule finite_subset) rule
have "0⇧2 ≤ n" by simp
then show *: "{m. m⇧2 ≤ n} ≠ {}" by blast
qed
lemma sqrt_unique:
assumes "m^2 ≤ n" "n < (Suc m)^2"
shows "Discrete.sqrt n = m"
proof -
have "m' ≤ m" if "m'^2 ≤ n" for m'
proof -
note that
also note assms(2)
finally have "m' < Suc m" by (rule power_less_imp_less_base) simp_all
thus "m' ≤ m" by simp
qed
with ‹m^2 ≤ n› sqrt_aux[of n] show ?thesis unfolding Discrete.sqrt_def
by (intro antisym Max.boundedI Max.coboundedI) simp_all
qed
lemma sqrt_code[code]: "sqrt n = Max (Set.filter (λm. m⇧2 ≤ n) {0..n})"
proof -
from power2_nat_le_imp_le [of _ n] have "{m. m ≤ n ∧ m⇧2 ≤ n} = {m. m⇧2 ≤ n}" by auto
then show ?thesis by (simp add: sqrt_def Set.filter_def)
qed
lemma sqrt_inverse_power2 [simp]: "sqrt (n⇧2) = n"
proof -
have "{m. m ≤ n} ≠ {}" by auto
then have "Max {m. m ≤ n} ≤ n" by auto
then show ?thesis
by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym)
qed
lemma sqrt_zero [simp]: "sqrt 0 = 0"
using sqrt_inverse_power2 [of 0] by simp
lemma sqrt_one [simp]: "sqrt 1 = 1"
using sqrt_inverse_power2 [of 1] by simp
lemma mono_sqrt: "mono sqrt"
proof
fix m n :: nat
have *: "0 * 0 ≤ m" by simp
assume "m ≤ n"
then show "sqrt m ≤ sqrt n"
by (auto intro!: Max_mono ‹0 * 0 ≤ m› finite_less_ub simp add: power2_eq_square sqrt_def)
qed
lemma mono_sqrt': "m ≤ n ⟹ Discrete.sqrt m ≤ Discrete.sqrt n"
using mono_sqrt unfolding mono_def by auto
lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 ⟷ n > 0"
proof -
have *: "0 < Max {m. m⇧2 ≤ n} ⟷ (∃a∈{m. m⇧2 ≤ n}. 0 < a)"
by (rule Max_gr_iff) (fact sqrt_aux)+
show ?thesis
proof
assume "0 < sqrt n"
then have "0 < Max {m. m⇧2 ≤ n}" by (simp add: sqrt_def)
with * show "0 < n" by (auto dest: power2_nat_le_imp_le)
next
assume "0 < n"
then have "1⇧2 ≤ n ∧ 0 < (1::nat)" by simp
then have "∃q. q⇧2 ≤ n ∧ 0 < q" ..
with * have "0 < Max {m. m⇧2 ≤ n}" by blast
then show "0 < sqrt n" by (simp add: sqrt_def)
qed
qed
lemma sqrt_power2_le [simp]: "(sqrt n)⇧2 ≤ n"
proof (cases "n > 0")
case False then show ?thesis by simp
next
case True then have "sqrt n > 0" by simp
then have "mono (times (Max {m. m⇧2 ≤ n}))" by (auto intro: mono_times_nat simp add: sqrt_def)
then have *: "Max {m. m⇧2 ≤ n} * Max {m. m⇧2 ≤ n} = Max (times (Max {m. m⇧2 ≤ n}) ` {m. m⇧2 ≤ n})"
using sqrt_aux [of n] by (rule mono_Max_commute)
have "⋀a. a * a ≤ n ⟹ Max {m. m * m ≤ n} * a ≤ n"
proof -
fix q
assume "q * q ≤ n"
show "Max {m. m * m ≤ n} * q ≤ n"
proof (cases "q > 0")
case False then show ?thesis by simp
next
case True then have "mono (times q)" by (rule mono_times_nat)
then have "q * Max {m. m * m ≤ n} = Max (times q ` {m. m * m ≤ n})"
using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
then have "Max {m. m * m ≤ n} * q = Max (times q ` {m. m * m ≤ n})" by (simp add: ac_simps)
moreover have "finite ((*) q ` {m. m * m ≤ n})"
by (metis (mono_tags) finite_imageI finite_less_ub le_square)
moreover have "∃x. x * x ≤ n"
by (metis ‹q * q ≤ n›)
ultimately show ?thesis
by simp (metis ‹q * q ≤ n› le_cases mult_le_mono1 mult_le_mono2 order_trans)
qed
qed
then have "Max ((*) (Max {m. m * m ≤ n}) ` {m. m * m ≤ n}) ≤ n"
apply (subst Max_le_iff)
apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
apply auto
apply (metis le0 mult_0_right)
done
with * show ?thesis by (simp add: sqrt_def power2_eq_square)
qed
lemma sqrt_le: "sqrt n ≤ n"
using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
text ‹Additional facts about the discrete square root, thanks to Julian Biendarra, Manuel Eberl›
lemma Suc_sqrt_power2_gt: "n < (Suc (Discrete.sqrt n))^2"
using Max_ge[OF Discrete.sqrt_aux(1), of "Discrete.sqrt n + 1" n]
by (cases "n < (Suc (Discrete.sqrt n))^2") (simp_all add: Discrete.sqrt_def)
lemma le_sqrt_iff: "x ≤ Discrete.sqrt y ⟷ x^2 ≤ y"
proof -
have "x ≤ Discrete.sqrt y ⟷ (∃z. z⇧2 ≤ y ∧ x ≤ z)"
using Max_ge_iff[OF Discrete.sqrt_aux, of x y] by (simp add: Discrete.sqrt_def)
also have "… ⟷ x^2 ≤ y"
proof safe
fix z assume "x ≤ z" "z ^ 2 ≤ y"
thus "x^2 ≤ y" by (intro le_trans[of "x^2" "z^2" y]) (simp_all add: power2_nat_le_eq_le)
qed auto
finally show ?thesis .
qed
lemma le_sqrtI: "x^2 ≤ y ⟹ x ≤ Discrete.sqrt y"
by (simp add: le_sqrt_iff)
lemma sqrt_le_iff: "Discrete.sqrt y ≤ x ⟷ (∀z. z^2 ≤ y ⟶ z ≤ x)"
using Max.bounded_iff[OF Discrete.sqrt_aux] by (simp add: Discrete.sqrt_def)
lemma sqrt_leI:
"(⋀z. z^2 ≤ y ⟹ z ≤ x) ⟹ Discrete.sqrt y ≤ x"
by (simp add: sqrt_le_iff)
lemma sqrt_Suc:
"Discrete.sqrt (Suc n) = (if ∃m. Suc n = m^2 then Suc (Discrete.sqrt n) else Discrete.sqrt n)"
proof cases
assume "∃ m. Suc n = m^2"
then obtain m where m_def: "Suc n = m^2" by blast
then have lhs: "Discrete.sqrt (Suc n) = m" by simp
from m_def sqrt_power2_le[of n]
have "(Discrete.sqrt n)^2 < m^2" by linarith
with power2_less_imp_less have lt_m: "Discrete.sqrt n < m" by blast
from m_def Suc_sqrt_power2_gt[of "n"]
have "m^2 ≤ (Suc(Discrete.sqrt n))^2"
by linarith
with power2_nat_le_eq_le have "m ≤ Suc (Discrete.sqrt n)" by blast
with lt_m have "m = Suc (Discrete.sqrt n)" by simp
with lhs m_def show ?thesis by fastforce
next
assume asm: "¬ (∃ m. Suc n = m^2)"
hence "Suc n ≠ (Discrete.sqrt (Suc n))^2" by simp
with sqrt_power2_le[of "Suc n"]
have "Discrete.sqrt (Suc n) ≤ Discrete.sqrt n" by (intro le_sqrtI) linarith
moreover have "Discrete.sqrt (Suc n) ≥ Discrete.sqrt n"
by (intro monoD[OF mono_sqrt]) simp_all
ultimately show ?thesis using asm by simp
qed
end
end