(* Author: Florian Haftmann, TU Muenchen *)
section \Common discrete functions\
theory Discrete
imports Main
begin
subsection \Discrete logarithm\
fun log :: "nat \ nat"
where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
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 True
then have "m = 0 \ m = 1" by arith
then show ?thesis by (auto simp del: One_nat_def)
next
case False
with mn2 have "m \ 2" and "n \ 2" by auto arith
from False have m2_0: "m div 2 \ 0" by arith
with mn2 have n2_0: "n div 2 \ 0" by arith
from False "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
subsection \Discrete square root\
definition sqrt :: "nat \ nat"
where "sqrt n = Max {m. m\<^sup>2 \ n}"
lemma sqrt_aux:
fixes n :: nat
shows "finite {m. m\<^sup>2 \ n}" and "{m. m\<^sup>2 \ n} \ {}"
proof -
{ fix m
assume "m\<^sup>2 \ n"
then have "m \ n"
by (cases m) (simp_all add: power2_eq_square)
} note ** = this
then have "{m. m\<^sup>2 \ n} \ {m. m \ n}" by auto
then show "finite {m. m\<^sup>2 \ n}" by (rule finite_subset) rule
have "0\<^sup>2 \ n" by simp
then show *: "{m. m\<^sup>2 \ n} \ {}" by blast
qed
lemma [code]: "sqrt n = Max (Set.filter (\m. m\<^sup>2 \ n) {0..n})"
proof -
from power2_nat_le_imp_le [of _ n] have "{m. m \ n \ m\<^sup>2 \ n} = {m. m\<^sup>2 \ n}" by auto
then show ?thesis by (simp add: sqrt_def Set.filter_def)
qed
lemma sqrt_inverse_power2 [simp]: "sqrt (n\<^sup>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 sqrt_greater_zero_iff [simp]: "sqrt n > 0 \ n > 0"
proof -
have *: "0 < Max {m. m\<^sup>2 \ n} \ (\a\{m. m\<^sup>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\<^sup>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\<^sup>2 \ n \ 0 < (1::nat)" by simp
then have "\q. q\<^sup>2 \ n \ 0 < q" ..
with * have "0 < Max {m. m\<^sup>2 \ n}" by blast
then show "0 < sqrt n" by (simp add: sqrt_def)
qed
qed
lemma sqrt_power2_le [simp]: "(sqrt n)\<^sup>2 \ n" (* FIXME tune proof *)
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\<^sup>2 \ n}))" by (auto intro: mono_times_nat simp add: sqrt_def)
then have *: "Max {m. m\<^sup>2 \ n} * Max {m. m\<^sup>2 \ n} = Max (times (Max {m. m\<^sup>2 \ n}) ` {m. m\<^sup>2 \ n})"
using sqrt_aux [of n] by (rule mono_Max_commute)
have "Max (op * (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 simp
apply (metis le0 mult_0_right)
apply auto
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)
then show ?thesis
apply simp
apply (subst Max_le_iff)
apply auto
apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
apply (metis \q * q \ n\)
apply (metis \q * q \ n\ le_cases mult_le_mono1 mult_le_mono2 order_trans)
done
qed
qed
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)
hide_const (open) log sqrt
end