renamed Discrete -> Discrete_Functions to avoid name clashes;
new function names floor_log/sqrt to avoid long Discrete_Functions.log/sqrt

--- a/NEWS	Sun Nov 17 09:50:54 2024 +0100
+++ b/NEWS	Sun Nov 17 21:20:26 2024 +0100
@@ -185,6 +185,11 @@
     This outputs a suggestion with instantiations of the facts using the
     "of" attribute (e.g. "assms(1)[of x]").
 
+* Theory "HOL-Library/Discrete" has been renamed "HOL-Library/Discrete_Functions"
+  Discrete.log -> floor_log
+  Discrete.sqrt -> floor_sqrt
+  Renamed lemmas accordingly (...log/sqrt... -> ...floor_log/sqrt...)
+
 * Theory "HOL.Wellfounded":
   - Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
     Minor INCOMPATIBILITY.

--- a/src/HOL/Analysis/Summation_Tests.thy	Sun Nov 17 09:50:54 2024 +0100
+++ b/src/HOL/Analysis/Summation_Tests.thy	Sun Nov 17 21:20:26 2024 +0100
@@ -7,7 +7,7 @@
 theory Summation_Tests
 imports
   Complex_Main
-  "HOL-Library.Discrete"
+  "HOL-Library.Discrete_Functions"
   "HOL-Library.Extended_Real"
   "HOL-Library.Liminf_Limsup"
   Extended_Real_Limits
@@ -135,33 +135,33 @@
 
 private lemma condensation_inequality:
   assumes mono: "\<And>m n. 0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> f n \<le> f m"
-  shows   "(\<Sum>k=1..<n. f k) \<ge> (\<Sum>k=1..<n. f (2 * 2 ^ Discrete.log k))" (is "?thesis1")
-          "(\<Sum>k=1..<n. f k) \<le> (\<Sum>k=1..<n. f (2 ^ Discrete.log k))" (is "?thesis2")
-  by (intro sum_mono mono Discrete.log_exp2_ge Discrete.log_exp2_le, simp, simp)+
+  shows   "(\<Sum>k=1..<n. f k) \<ge> (\<Sum>k=1..<n. f (2 * 2 ^ floor_log k))" (is "?thesis1")
+          "(\<Sum>k=1..<n. f k) \<le> (\<Sum>k=1..<n. f (2 ^ floor_log k))" (is "?thesis2")
+  by (intro sum_mono mono floor_log_exp2_ge floor_log_exp2_le, simp, simp)+
 
-private lemma condensation_condense1: "(\<Sum>k=1..<2^n. f (2 ^ Discrete.log k)) = (\<Sum>k<n. 2^k * f (2 ^ k))"
+private lemma condensation_condense1: "(\<Sum>k=1..<2^n. f (2 ^ floor_log k)) = (\<Sum>k<n. 2^k * f (2 ^ k))"
 proof (induction n)
   case (Suc n)
   have "{1..<2^Suc n} = {1..<2^n} \<union> {2^n..<(2^Suc n :: nat)}" by auto
-  also have "(\<Sum>k\<in>\<dots>. f (2 ^ Discrete.log k)) =
-                 (\<Sum>k<n. 2^k * f (2^k)) + (\<Sum>k = 2^n..<2^Suc n. f (2^Discrete.log k))"
+  also have "(\<Sum>k\<in>\<dots>. f (2 ^ floor_log k)) =
+                 (\<Sum>k<n. 2^k * f (2^k)) + (\<Sum>k = 2^n..<2^Suc n. f (2^floor_log k))"
     by (subst sum.union_disjoint) (insert Suc, auto)
-  also have "Discrete.log k = n" if "k \<in> {2^n..<2^Suc n}" for k using that by (intro Discrete.log_eqI) simp_all
-  hence "(\<Sum>k = 2^n..<2^Suc n. f (2^Discrete.log k)) = (\<Sum>(_::nat) = 2^n..<2^Suc n. f (2^n))"
+  also have "floor_log k = n" if "k \<in> {2^n..<2^Suc n}" for k using that by (intro floor_log_eqI) simp_all
+  hence "(\<Sum>k = 2^n..<2^Suc n. f (2^floor_log k)) = (\<Sum>(_::nat) = 2^n..<2^Suc n. f (2^n))"
     by (intro sum.cong) simp_all
   also have "\<dots> = 2^n * f (2^n)" by (simp)
   finally show ?case by simp
 qed simp
 
-private lemma condensation_condense2: "(\<Sum>k=1..<2^n. f (2 * 2 ^ Discrete.log k)) = (\<Sum>k<n. 2^k * f (2 ^ Suc k))"
+private lemma condensation_condense2: "(\<Sum>k=1..<2^n. f (2 * 2 ^ floor_log k)) = (\<Sum>k<n. 2^k * f (2 ^ Suc k))"
 proof (induction n)
   case (Suc n)
   have "{1..<2^Suc n} = {1..<2^n} \<union> {2^n..<(2^Suc n :: nat)}" by auto
-  also have "(\<Sum>k\<in>\<dots>. f (2 * 2 ^ Discrete.log k)) =
-                 (\<Sum>k<n. 2^k * f (2^Suc k)) + (\<Sum>k = 2^n..<2^Suc n. f (2 * 2^Discrete.log k))"
+  also have "(\<Sum>k\<in>\<dots>. f (2 * 2 ^ floor_log k)) =
+                 (\<Sum>k<n. 2^k * f (2^Suc k)) + (\<Sum>k = 2^n..<2^Suc n. f (2 * 2^floor_log k))"
     by (subst sum.union_disjoint) (insert Suc, auto)
-  also have "Discrete.log k = n" if "k \<in> {2^n..<2^Suc n}" for k using that by (intro Discrete.log_eqI) simp_all
-  hence "(\<Sum>k = 2^n..<2^Suc n. f (2*2^Discrete.log k)) = (\<Sum>(_::nat) = 2^n..<2^Suc n. f (2^Suc n))"
+  also have "floor_log k = n" if "k \<in> {2^n..<2^Suc n}" for k using that by (intro floor_log_eqI) simp_all
+  hence "(\<Sum>k = 2^n..<2^Suc n. f (2*2^floor_log k)) = (\<Sum>(_::nat) = 2^n..<2^Suc n. f (2^Suc n))"
     by (intro sum.cong) simp_all
   also have "\<dots> = 2^n * f (2^Suc n)" by (simp)
   finally show ?case by simp

--- a/src/HOL/Computational_Algebra/Nth_Powers.thy	Sun Nov 17 09:50:54 2024 +0100
+++ b/src/HOL/Computational_Algebra/Nth_Powers.thy	Sun Nov 17 21:20:26 2024 +0100
@@ -155,7 +155,7 @@
   by (auto simp: is_nth_power_nat_def is_nth_power_def power_eq_iff_eq_base self_le_power)
 
 
-(* TODO: Harmonise with Discrete.sqrt *)
+(* TODO: Harmonise with Discrete_Functions.floor_sqrt *)
 
 subsection \<open>The $n$-root of a natural number\<close>
 

--- a/src/HOL/Library/Discrete.thy	Sun Nov 17 09:50:54 2024 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,349 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-section \<open>Common discrete functions\<close>
-
-theory Discrete
-imports Complex_Main
-begin
-
-subsection \<open>Discrete logarithm\<close>
-
-context
-begin
-
-qualified fun log :: "nat \<Rightarrow> 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: "\<And>n. n \<ge> 2 \<Longrightarrow> P (n div 2) \<Longrightarrow> P n"
-  shows "P n"
-using \<open>n > 0\<close> proof (induct n rule: log.induct)
-  fix n
-  assume "\<not> n < 2 \<Longrightarrow>
-          0 < n div 2 \<Longrightarrow> P (n div 2)"
-  then have *: "n \<ge> 2 \<Longrightarrow> 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 \<open>n > 0\<close> have "n \<ge> 2" by auto
-    with * have "P (n div 2)" .
-    with \<open>n \<ge> 2\<close> 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 \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))"
-  by (simp add: log.simps)
-
-lemma log_twice [simp]: "n \<noteq> 0 \<Longrightarrow> 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 \<or> 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_power [simp]: "log (2 ^ n) = n"
-  by (induct n) simp_all
-
-lemma log_mono: "mono log"
-proof
-  fix m n :: nat
-  assume "m \<le> n"
-  then show "log m \<le> log n"
-  proof (induct m arbitrary: n rule: log.induct)
-    case (1 m)
-    then have mn2: "m div 2 \<le> n div 2" by arith
-    show "log m \<le> log n"
-    proof (cases "m \<ge> 2")
-      case False
-      then have "m = 0 \<or> m = 1" by arith
-      then show ?thesis by (auto simp del: One_nat_def)
-    next
-      case True then have "\<not> m < 2" by simp
-      with mn2 have "n \<ge> 2" by arith
-      from True have m2_0: "m div 2 \<noteq> 0" by arith
-      with mn2 have n2_0: "n div 2 \<noteq> 0" by arith
-      from \<open>\<not> m < 2\<close> "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast
-      with m2_0 n2_0 have "log (2 * (m div 2)) \<le> log (2 * (n div 2))" by simp
-      with m2_0 n2_0 \<open>m \<ge> 2\<close> \<open>n \<ge> 2\<close> 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 \<le> 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 \<ge> Suc 0"
-    by (simp add: log.simps)
-  assume "2 ^ log (n div 2) \<le> n div 2"
-  with \<open>n \<ge> 2\<close> have "2 ^ (log n - Suc 0) \<le> n div 2" by simp
-  then have "2 ^ (log n - Suc 0) * 2 ^ 1 \<le> n div 2 * 2" by simp
-  with \<open>log n \<ge> Suc 0\<close> have "2 ^ log n \<le> n div 2 * 2"
-    unfolding power_add [symmetric] by simp
-  also have "n div 2 * 2 \<le> 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 \<ge> n"
-  using log_exp2_gt[of n] by simp
-
-lemma log_le_iff: "m \<le> n \<Longrightarrow> log m \<le> log n"
-  by (rule monoD [OF log_mono])
-
-lemma log_eqI:
-  assumes "n > 0" "2^k \<le> n" "n < 2 * 2^k"
-  shows   "log n = k"
-proof (rule antisym)
-  from \<open>n > 0\<close> have "2 ^ log n \<le> n" by (rule log_exp2_le)
-  also have "\<dots> < 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 \<le> k" by simp
-next
-  have "2^k \<le> n" by fact
-  also have "\<dots> < 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 \<le> log n" by simp
-qed
-
-lemma log_altdef: "log n = (if n = 0 then 0 else nat \<lfloor>Transcendental.log 2 (real_of_nat n)\<rfloor>)"
-proof (cases "n = 0")
-  case False
-  have "\<lfloor>Transcendental.log 2 (real_of_nat n)\<rfloor> = int (log n)"
-  proof (rule floor_unique)
-    from False have "2 powr (real (log n)) \<le> real n"
-      by (simp add: powr_realpow log_exp2_le)
-    hence "Transcendental.log 2 (2 powr (real (log n))) \<le> 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)) \<le> 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 "\<dots> = 2 powr (real (log n) + 1)"
-      by (simp add: powr_add powr_realpow)
-    finally have "Transcendental.log 2 (real n) < Transcendental.log 2 \<dots>"
-      using False by (subst Transcendental.log_less_cancel_iff) simp_all
-    also have "\<dots> = 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 \<open>Discrete square root\<close>
-
-qualified definition sqrt :: "nat \<Rightarrow> nat"
-  where "sqrt n = Max {m. m\<^sup>2 \<le> n}"
-
-lemma sqrt_aux:
-  fixes n :: nat
-  shows "finite {m. m\<^sup>2 \<le> n}" and "{m. m\<^sup>2 \<le> n} \<noteq> {}"
-proof -
-  have **: "m \<le> n" if "m\<^sup>2 \<le> n" for m
-    using that by (cases m) (simp_all add: power2_eq_square)
-  then have "{m. m\<^sup>2 \<le> n} \<subseteq> {m. m \<le> n}" by auto
-  then show "finite {m. m\<^sup>2 \<le> n}" by (rule finite_subset) rule
-  have "0\<^sup>2 \<le> n" by simp
-  then show *: "{m. m\<^sup>2 \<le> n} \<noteq> {}" by blast
-qed
-
-lemma sqrt_unique:
-  assumes "m^2 \<le> n" "n < (Suc m)^2"
-  shows   "Discrete.sqrt n = m"
-proof -
-  have "m' \<le> m" if "m'^2 \<le> 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' \<le> m" by simp
-  qed
-  with \<open>m^2 \<le> n\<close> 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 (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
-proof -
-  from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<^sup>2 \<le> n} = {m. m\<^sup>2 \<le> 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 \<le> n} \<noteq> {}" by auto
-  then have "Max {m. m \<le> n} \<le> 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 \<le> m" by simp
-  assume "m \<le> n"
-  then show "sqrt m \<le> sqrt n"
-    by (auto intro!: Max_mono \<open>0 * 0 \<le> m\<close> finite_less_ub simp add: power2_eq_square sqrt_def)
-qed
-
-lemma mono_sqrt': "m \<le> n \<Longrightarrow> Discrete.sqrt m \<le> Discrete.sqrt n"
-  using mono_sqrt unfolding mono_def by auto
-
-lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 \<longleftrightarrow> n > 0"
-proof -
-  have *: "0 < Max {m. m\<^sup>2 \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<^sup>2 \<le> 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 \<le> 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 \<le> n \<and> 0 < (1::nat)" by simp
-    then have "\<exists>q. q\<^sup>2 \<le> n \<and> 0 < q" ..
-    with * have "0 < Max {m. m\<^sup>2 \<le> n}" by blast
-    then show "0 < sqrt n" by  (simp add: sqrt_def)
-  qed
-qed
-
-lemma sqrt_power2_le [simp]: "(sqrt n)\<^sup>2 \<le> 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 \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def)
-  then have *: "Max {m. m\<^sup>2 \<le> n} * Max {m. m\<^sup>2 \<le> n} = Max (times (Max {m. m\<^sup>2 \<le> n}) ` {m. m\<^sup>2 \<le> n})"
-    using sqrt_aux [of n] by (rule mono_Max_commute)
-  have "\<And>a. a * a \<le> n \<Longrightarrow> Max {m. m * m \<le> n} * a \<le> n"
-  proof -
-    fix q
-    assume "q * q \<le> n"
-    show "Max {m. m * m \<le> n} * q \<le> 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 \<le> n} = Max (times q ` {m. m * m \<le> n})"
-        using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
-      then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
-      moreover have "finite ((*) q ` {m. m * m \<le> n})"
-        by (metis (mono_tags) finite_imageI finite_less_ub le_square)
-      moreover have "\<exists>x. x * x \<le> n"
-        by (metis \<open>q * q \<le> n\<close>)
-      ultimately show ?thesis
-        by simp (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans)
-    qed
-  qed
-  then have "Max ((*) (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> 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 \<le> n"
-  using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
-
-text \<open>Additional facts about the discrete square root, thanks to Julian Biendarra, Manuel Eberl\<close>
-
-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 \<le> Discrete.sqrt y \<longleftrightarrow> x^2 \<le> y"
-proof -
-  have "x \<le> Discrete.sqrt y \<longleftrightarrow> (\<exists>z. z\<^sup>2 \<le> y \<and> x \<le> z)"
-    using Max_ge_iff[OF Discrete.sqrt_aux, of x y] by (simp add: Discrete.sqrt_def)
-  also have "\<dots> \<longleftrightarrow> x^2 \<le> y"
-  proof safe
-    fix z assume "x \<le> z" "z ^ 2 \<le> y"
-    thus "x^2 \<le> 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 \<le> y \<Longrightarrow> x \<le> Discrete.sqrt y"
-  by (simp add: le_sqrt_iff)
-
-lemma sqrt_le_iff: "Discrete.sqrt y \<le> x \<longleftrightarrow> (\<forall>z. z^2 \<le> y \<longrightarrow> z \<le> x)"
-  using Max.bounded_iff[OF Discrete.sqrt_aux] by (simp add: Discrete.sqrt_def)
-
-lemma sqrt_leI:
-  "(\<And>z. z^2 \<le> y \<Longrightarrow> z \<le> x) \<Longrightarrow> Discrete.sqrt y \<le> x"
-  by (simp add: sqrt_le_iff)
-
-lemma sqrt_Suc:
-  "Discrete.sqrt (Suc n) = (if \<exists>m. Suc n = m^2 then Suc (Discrete.sqrt n) else Discrete.sqrt n)"
-proof cases
-  assume "\<exists> 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 \<le> (Suc(Discrete.sqrt n))^2"
-      by linarith
-  with power2_nat_le_eq_le have "m \<le> 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: "\<not> (\<exists> m. Suc n = m^2)"
-  hence "Suc n \<noteq> (Discrete.sqrt (Suc n))^2" by simp
-  with sqrt_power2_le[of "Suc n"]
-    have "Discrete.sqrt (Suc n) \<le> Discrete.sqrt n" by (intro le_sqrtI) linarith
-  moreover have "Discrete.sqrt (Suc n) \<ge> Discrete.sqrt n"
-    by (intro monoD[OF mono_sqrt]) simp_all
-  ultimately show ?thesis using asm by simp
-qed
-
-end
-
-end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Discrete_Functions.thy	Sun Nov 17 21:20:26 2024 +0100
@@ -0,0 +1,344 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Common discrete functions\<close>
+
+theory Discrete_Functions
+imports Complex_Main
+begin
+
+subsection \<open>Discrete logarithm\<close>
+
+fun floor_log :: "nat \<Rightarrow> nat"
+  where [simp del]: "floor_log n = (if n < 2 then 0 else Suc (floor_log (n div 2)))"
+
+lemma floor_log_induct [consumes 1, case_names one double]:
+  fixes n :: nat
+  assumes "n > 0"
+  assumes one: "P 1"
+  assumes double: "\<And>n. n \<ge> 2 \<Longrightarrow> P (n div 2) \<Longrightarrow> P n"
+  shows "P n"
+using \<open>n > 0\<close> proof (induct n rule: floor_log.induct)
+  fix n
+  assume "\<not> n < 2 \<Longrightarrow>
+          0 < n div 2 \<Longrightarrow> P (n div 2)"
+  then have *: "n \<ge> 2 \<Longrightarrow> 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 \<open>n > 0\<close> have "n \<ge> 2" by auto
+    with * have "P (n div 2)" .
+    with \<open>n \<ge> 2\<close> show ?thesis by (rule double)
+  qed
+qed
+
+lemma floor_log_zero [simp]: "floor_log 0 = 0"
+  by (simp add: floor_log.simps)
+
+lemma floor_log_one [simp]: "floor_log 1 = 0"
+  by (simp add: floor_log.simps)
+
+lemma floor_log_Suc_zero [simp]: "floor_log (Suc 0) = 0"
+  using floor_log_one by simp
+
+lemma floor_log_rec: "n \<ge> 2 \<Longrightarrow> floor_log n = Suc (floor_log (n div 2))"
+  by (simp add: floor_log.simps)
+
+lemma floor_log_twice [simp]: "n \<noteq> 0 \<Longrightarrow> floor_log (2 * n) = Suc (floor_log n)"
+  by (simp add: floor_log_rec)
+
+lemma floor_log_half [simp]: "floor_log (n div 2) = floor_log n - 1"
+proof (cases "n < 2")
+  case True
+  then have "n = 0 \<or> n = 1" by arith
+  then show ?thesis by (auto simp del: One_nat_def)
+next
+  case False
+  then show ?thesis by (simp add: floor_log_rec)
+qed
+
+lemma floor_log_power [simp]: "floor_log (2 ^ n) = n"
+  by (induct n) simp_all
+
+lemma floor_log_mono: "mono floor_log"
+proof
+  fix m n :: nat
+  assume "m \<le> n"
+  then show "floor_log m \<le> floor_log n"
+  proof (induct m arbitrary: n rule: floor_log.induct)
+    case (1 m)
+    then have mn2: "m div 2 \<le> n div 2" by arith
+    show "floor_log m \<le> floor_log n"
+    proof (cases "m \<ge> 2")
+      case False
+      then have "m = 0 \<or> m = 1" by arith
+      then show ?thesis by (auto simp del: One_nat_def)
+    next
+      case True then have "\<not> m < 2" by simp
+      with mn2 have "n \<ge> 2" by arith
+      from True have m2_0: "m div 2 \<noteq> 0" by arith
+      with mn2 have n2_0: "n div 2 \<noteq> 0" by arith
+      from \<open>\<not> m < 2\<close> "1.hyps" mn2 have "floor_log (m div 2) \<le> floor_log (n div 2)" by blast
+      with m2_0 n2_0 have "floor_log (2 * (m div 2)) \<le> floor_log (2 * (n div 2))" by simp
+      with m2_0 n2_0 \<open>m \<ge> 2\<close> \<open>n \<ge> 2\<close> show ?thesis by (simp only: floor_log_rec [of m] floor_log_rec [of n]) simp
+    qed
+  qed
+qed
+
+lemma floor_log_exp2_le:
+  assumes "n > 0"
+  shows "2 ^ floor_log n \<le> n"
+  using assms
+proof (induct n rule: floor_log_induct)
+  case one
+  then show ?case by simp
+next
+  case (double n)
+  with floor_log_mono have "floor_log n \<ge> Suc 0"
+    by (simp add: floor_log.simps)
+  assume "2 ^ floor_log (n div 2) \<le> n div 2"
+  with \<open>n \<ge> 2\<close> have "2 ^ (floor_log n - Suc 0) \<le> n div 2" by simp
+  then have "2 ^ (floor_log n - Suc 0) * 2 ^ 1 \<le> n div 2 * 2" by simp
+  with \<open>floor_log n \<ge> Suc 0\<close> have "2 ^ floor_log n \<le> n div 2 * 2"
+    unfolding power_add [symmetric] by simp
+  also have "n div 2 * 2 \<le> n" by (cases "even n") simp_all
+  finally show ?case .
+qed
+
+lemma floor_log_exp2_gt: "2 * 2 ^ floor_log n > n"
+proof (cases "n > 0")
+  case True
+  thus ?thesis
+  proof (induct n rule: floor_log_induct)
+    case (double n)
+    thus ?case
+      by (cases "even n") (auto elim!: evenE oddE simp: field_simps floor_log.simps)
+  qed simp_all
+qed simp_all
+
+lemma floor_log_exp2_ge: "2 * 2 ^ floor_log n \<ge> n"
+  using floor_log_exp2_gt[of n] by simp
+
+lemma floor_log_le_iff: "m \<le> n \<Longrightarrow> floor_log m \<le> floor_log n"
+  by (rule monoD [OF floor_log_mono])
+
+lemma floor_log_eqI:
+  assumes "n > 0" "2^k \<le> n" "n < 2 * 2^k"
+  shows   "floor_log n = k"
+proof (rule antisym)
+  from \<open>n > 0\<close> have "2 ^ floor_log n \<le> n" by (rule floor_log_exp2_le)
+  also have "\<dots> < 2 ^ Suc k" using assms by simp
+  finally have "floor_log n < Suc k" by (subst (asm) power_strict_increasing_iff) simp_all
+  thus "floor_log n \<le> k" by simp
+next
+  have "2^k \<le> n" by fact
+  also have "\<dots> < 2^(Suc (floor_log n))" by (simp add: floor_log_exp2_gt)
+  finally have "k < Suc (floor_log n)" by (subst (asm) power_strict_increasing_iff) simp_all
+  thus "k \<le> floor_log n" by simp
+qed
+
+lemma floor_log_altdef: "floor_log n = (if n = 0 then 0 else nat \<lfloor>log 2 (real_of_nat n)\<rfloor>)"
+proof (cases "n = 0")
+  case False
+  have "\<lfloor>log 2 (real_of_nat n)\<rfloor> = int (floor_log n)"
+  proof (rule floor_unique)
+    from False have "2 powr (real (floor_log n)) \<le> real n"
+      by (simp add: powr_realpow floor_log_exp2_le)
+    hence "log 2 (2 powr (real (floor_log n))) \<le> log 2 (real n)"
+      using False by (subst log_le_cancel_iff) simp_all
+    also have "log 2 (2 powr (real (floor_log n))) = real (floor_log n)" by simp
+    finally show "real_of_int (int (floor_log n)) \<le> log 2 (real n)" by simp
+  next
+    have "real n < real (2 * 2 ^ floor_log n)"
+      by (subst of_nat_less_iff) (rule floor_log_exp2_gt)
+    also have "\<dots> = 2 powr (real (floor_log n) + 1)"
+      by (simp add: powr_add powr_realpow)
+    finally have "log 2 (real n) < log 2 \<dots>"
+      using False by (subst log_less_cancel_iff) simp_all
+    also have "\<dots> = real (floor_log n) + 1" by simp
+    finally show "log 2 (real n) < real_of_int (int (floor_log n)) + 1" by simp
+  qed
+  thus ?thesis by simp
+qed simp_all
+
+
+subsection \<open>Discrete square root\<close>
+
+definition floor_sqrt :: "nat \<Rightarrow> nat"
+  where "floor_sqrt n = Max {m. m\<^sup>2 \<le> n}"
+
+lemma floor_sqrt_aux:
+  fixes n :: nat
+  shows "finite {m. m\<^sup>2 \<le> n}" and "{m. m\<^sup>2 \<le> n} \<noteq> {}"
+proof -
+  have **: "m \<le> n" if "m\<^sup>2 \<le> n" for m
+    using that by (cases m) (simp_all add: power2_eq_square)
+  then have "{m. m\<^sup>2 \<le> n} \<subseteq> {m. m \<le> n}" by auto
+  then show "finite {m. m\<^sup>2 \<le> n}" by (rule finite_subset) rule
+  have "0\<^sup>2 \<le> n" by simp
+  then show *: "{m. m\<^sup>2 \<le> n} \<noteq> {}" by blast
+qed
+
+lemma floor_sqrt_unique:
+  assumes "m^2 \<le> n" "n < (Suc m)^2"
+  shows   "floor_sqrt n = m"
+proof -
+  have "m' \<le> m" if "m'^2 \<le> 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' \<le> m" by simp
+  qed
+  with \<open>m^2 \<le> n\<close> floor_sqrt_aux[of n] show ?thesis unfolding floor_sqrt_def
+    by (intro antisym Max.boundedI Max.coboundedI) simp_all
+qed
+
+
+lemma floor_sqrt_code[code]: "floor_sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
+proof -
+  from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<^sup>2 \<le> n} = {m. m\<^sup>2 \<le> n}" by auto
+  then show ?thesis by (simp add: floor_sqrt_def Set.filter_def)
+qed
+
+lemma floor_sqrt_inverse_power2 [simp]: "floor_sqrt (n\<^sup>2) = n"
+proof -
+  have "{m. m \<le> n} \<noteq> {}" by auto
+  then have "Max {m. m \<le> n} \<le> n" by auto
+  then show ?thesis
+    by (auto simp add: floor_sqrt_def power2_nat_le_eq_le intro: antisym)
+qed
+
+lemma floor_sqrt_zero [simp]: "floor_sqrt 0 = 0"
+  using floor_sqrt_inverse_power2 [of 0] by simp
+
+lemma floor_sqrt_one [simp]: "floor_sqrt 1 = 1"
+  using floor_sqrt_inverse_power2 [of 1] by simp
+
+lemma mono_floor_sqrt: "mono floor_sqrt"
+proof
+  fix m n :: nat
+  have *: "0 * 0 \<le> m" by simp
+  assume "m \<le> n"
+  then show "floor_sqrt m \<le> floor_sqrt n"
+    by (auto intro!: Max_mono \<open>0 * 0 \<le> m\<close> finite_less_ub simp add: power2_eq_square floor_sqrt_def)
+qed
+
+lemma mono_floor_sqrt': "m \<le> n \<Longrightarrow> floor_sqrt m \<le> floor_sqrt n"
+  using mono_floor_sqrt unfolding mono_def by auto
+
+lemma floor_sqrt_greater_zero_iff [simp]: "floor_sqrt n > 0 \<longleftrightarrow> n > 0"
+proof -
+  have *: "0 < Max {m. m\<^sup>2 \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<^sup>2 \<le> n}. 0 < a)"
+    by (rule Max_gr_iff) (fact floor_sqrt_aux)+
+  show ?thesis
+  proof
+    assume "0 < floor_sqrt n"
+    then have "0 < Max {m. m\<^sup>2 \<le> n}" by (simp add: floor_sqrt_def)
+    with * show "0 < n" by (auto dest: power2_nat_le_imp_le)
+  next
+    assume "0 < n"
+    then have "1\<^sup>2 \<le> n \<and> 0 < (1::nat)" by simp
+    then have "\<exists>q. q\<^sup>2 \<le> n \<and> 0 < q" ..
+    with * have "0 < Max {m. m\<^sup>2 \<le> n}" by blast
+    then show "0 < floor_sqrt n" by  (simp add: floor_sqrt_def)
+  qed
+qed
+
+lemma floor_sqrt_power2_le [simp]: "(floor_sqrt n)\<^sup>2 \<le> n" (* FIXME tune proof *)
+proof (cases "n > 0")
+  case False then show ?thesis by simp
+next
+  case True then have "floor_sqrt n > 0" by simp
+  then have "mono (times (Max {m. m\<^sup>2 \<le> n}))" by (auto intro: mono_times_nat simp add: floor_sqrt_def)
+  then have *: "Max {m. m\<^sup>2 \<le> n} * Max {m. m\<^sup>2 \<le> n} = Max (times (Max {m. m\<^sup>2 \<le> n}) ` {m. m\<^sup>2 \<le> n})"
+    using floor_sqrt_aux [of n] by (rule mono_Max_commute)
+  have "\<And>a. a * a \<le> n \<Longrightarrow> Max {m. m * m \<le> n} * a \<le> n"
+  proof -
+    fix q
+    assume "q * q \<le> n"
+    show "Max {m. m * m \<le> n} * q \<le> 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 \<le> n} = Max (times q ` {m. m * m \<le> n})"
+        using floor_sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
+      then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
+      moreover have "finite ((*) q ` {m. m * m \<le> n})"
+        by (metis (mono_tags) finite_imageI finite_less_ub le_square)
+      moreover have "\<exists>x. x * x \<le> n"
+        by (metis \<open>q * q \<le> n\<close>)
+      ultimately show ?thesis
+        by simp (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans)
+    qed
+  qed
+  then have "Max ((*) (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> 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: floor_sqrt_def power2_eq_square)
+qed
+
+lemma floor_sqrt_le: "floor_sqrt n \<le> n"
+  using floor_sqrt_aux [of n] by (auto simp add: floor_sqrt_def intro: power2_nat_le_imp_le)
+
+text \<open>Additional facts about the discrete square root, thanks to Julian Biendarra, Manuel Eberl\<close>
+
+lemma Suc_floor_sqrt_power2_gt: "n < (Suc (floor_sqrt n))^2"
+  using Max_ge[OF floor_sqrt_aux(1), of "floor_sqrt n + 1" n]
+  by (cases "n < (Suc (floor_sqrt n))^2") (simp_all add: floor_sqrt_def)
+
+lemma le_floor_sqrt_iff: "x \<le> floor_sqrt y \<longleftrightarrow> x^2 \<le> y"
+proof -
+  have "x \<le> floor_sqrt y \<longleftrightarrow> (\<exists>z. z\<^sup>2 \<le> y \<and> x \<le> z)"
+    using Max_ge_iff[OF floor_sqrt_aux, of x y] by (simp add: floor_sqrt_def)
+  also have "\<dots> \<longleftrightarrow> x^2 \<le> y"
+  proof safe
+    fix z assume "x \<le> z" "z ^ 2 \<le> y"
+    thus "x^2 \<le> 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_floor_sqrtI: "x^2 \<le> y \<Longrightarrow> x \<le> floor_sqrt y"
+  by (simp add: le_floor_sqrt_iff)
+
+lemma floor_sqrt_le_iff: "floor_sqrt y \<le> x \<longleftrightarrow> (\<forall>z. z^2 \<le> y \<longrightarrow> z \<le> x)"
+  using Max.bounded_iff[OF floor_sqrt_aux] by (simp add: floor_sqrt_def)
+
+lemma floor_sqrt_leI:
+  "(\<And>z. z^2 \<le> y \<Longrightarrow> z \<le> x) \<Longrightarrow> floor_sqrt y \<le> x"
+  by (simp add: floor_sqrt_le_iff)
+
+lemma floor_sqrt_Suc:
+  "floor_sqrt (Suc n) = (if \<exists>m. Suc n = m^2 then Suc (floor_sqrt n) else floor_sqrt n)"
+proof cases
+  assume "\<exists> m. Suc n = m^2"
+  then obtain m where m_def: "Suc n = m^2" by blast
+  then have lhs: "floor_sqrt (Suc n) = m" by simp
+  from m_def floor_sqrt_power2_le[of n]
+    have "(floor_sqrt n)^2 < m^2" by linarith
+  with power2_less_imp_less have lt_m: "floor_sqrt n < m" by blast
+  from m_def Suc_floor_sqrt_power2_gt[of "n"]
+    have "m^2 \<le> (Suc(floor_sqrt n))^2"
+      by linarith
+  with power2_nat_le_eq_le have "m \<le> Suc (floor_sqrt n)" by blast
+  with lt_m have "m = Suc (floor_sqrt n)" by simp
+  with lhs m_def show ?thesis by fastforce
+next
+  assume asm: "\<not> (\<exists> m. Suc n = m^2)"
+  hence "Suc n \<noteq> (floor_sqrt (Suc n))^2" by simp
+  with floor_sqrt_power2_le[of "Suc n"]
+    have "floor_sqrt (Suc n) \<le> floor_sqrt n" by (intro le_floor_sqrtI) linarith
+  moreover have "floor_sqrt (Suc n) \<ge> floor_sqrt n"
+    by (intro monoD[OF mono_floor_sqrt]) simp_all
+  ultimately show ?thesis using asm by simp
+qed
+
+end

--- a/src/HOL/Library/Library.thy	Sun Nov 17 09:50:54 2024 +0100
+++ b/src/HOL/Library/Library.thy	Sun Nov 17 21:20:26 2024 +0100
@@ -21,7 +21,7 @@
   Countable_Set_Type
   Debug
   Diagonal_Subsequence
-  Discrete
+  Discrete_Functions
   Disjoint_Sets
   Disjoint_FSets
   Dlist

--- a/src/HOL/ex/Function_Growth.thy	Sun Nov 17 09:50:54 2024 +0100
+++ b/src/HOL/ex/Function_Growth.thy	Sun Nov 17 21:20:26 2024 +0100
@@ -7,7 +7,7 @@
 imports
   Main
   "HOL-Library.Preorder"
-  "HOL-Library.Discrete"
+  "HOL-Library.Discrete_Functions"
 begin
 
 subsection \<open>Motivation\<close>
@@ -23,7 +23,7 @@
   \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  From a didactic point of view, this does not only
   avoid the notational oddities mentioned above but also emphasizes the key insight
   of a growth hierarchy of functions:
-  \<open>(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>\<close>.
+  \<open>(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> floor_log \<lesssim> floor_sqrt \<lesssim> id \<lesssim> \<dots>\<close>.
 \<close>
 
 subsection \<open>Model\<close>
@@ -365,46 +365,46 @@
   by (rule less_fun_strongI) auto
 
 lemma
-  "(\<lambda>_. k) \<prec> Discrete.log"
+  "(\<lambda>_. k) \<prec> floor_log"
 proof (rule less_fun_strongI)
   fix c :: nat
-  have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m"
+  have "\<forall>m>2 ^ (Suc (c * k)). c * k < floor_log m"
   proof (rule allI, rule impI)
     fix m :: nat
     assume "2 ^ Suc (c * k) < m"
     then have "2 ^ Suc (c * k) \<le> m" by simp
-    with log_mono have "Discrete.log (2 ^ (Suc (c * k))) \<le> Discrete.log m"
+    with floor_log_mono have "floor_log (2 ^ (Suc (c * k))) \<le> floor_log m"
       by (blast dest: monoD)
-    moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp
-    ultimately show "c * k < Discrete.log m" by auto
+    moreover have "c * k < floor_log (2 ^ (Suc (c * k)))" by simp
+    ultimately show "c * k < floor_log m" by auto
   qed
-  then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" ..
+  then show "\<exists>n. \<forall>m>n. c * k < floor_log m" ..
 qed
 
 (*lemma
-  "Discrete.log \<prec> Discrete.sqrt"
+  "floor_log \<prec> floor_sqrt"
 proof (rule less_fun_strongI)*)
-text \<open>\<^prop>\<open>Discrete.log \<prec> Discrete.sqrt\<close>\<close>
+text \<open>\<^prop>\<open>floor_log \<prec> floor_sqrt\<close>\<close>
 
 lemma
-  "Discrete.sqrt \<prec> id"
+  "floor_sqrt \<prec> id"
 proof (rule less_fun_strongI)
   fix c :: nat
   assume "0 < c"
-  have "\<forall>m>(Suc c)\<^sup>2. c * Discrete.sqrt m < id m"
+  have "\<forall>m>(Suc c)\<^sup>2. c * floor_sqrt m < id m"
   proof (rule allI, rule impI)
     fix m
     assume "(Suc c)\<^sup>2 < m"
     then have "(Suc c)\<^sup>2 \<le> m" by simp
-    with mono_sqrt have "Discrete.sqrt ((Suc c)\<^sup>2) \<le> Discrete.sqrt m" by (rule monoE)
-    then have "Suc c \<le> Discrete.sqrt m" by simp
-    then have "c < Discrete.sqrt m" by simp
-    moreover from \<open>(Suc c)\<^sup>2 < m\<close> have "Discrete.sqrt m > 0" by simp
-    ultimately have "c * Discrete.sqrt m < Discrete.sqrt m * Discrete.sqrt m" by simp
+    with mono_floor_sqrt have "floor_sqrt ((Suc c)\<^sup>2) \<le> floor_sqrt m" by (rule monoE)
+    then have "Suc c \<le> floor_sqrt m" by simp
+    then have "c < floor_sqrt m" by simp
+    moreover from \<open>(Suc c)\<^sup>2 < m\<close> have "floor_sqrt m > 0" by simp
+    ultimately have "c * floor_sqrt m < floor_sqrt m * floor_sqrt m" by simp
     also have "\<dots> \<le> m" by (simp add: power2_eq_square [symmetric])
-    finally show "c * Discrete.sqrt m < id m" by simp
+    finally show "c * floor_sqrt m < id m" by simp
   qed
-  then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" ..
+  then show "\<exists>n. \<forall>m>n. c * floor_sqrt m < id m" ..
 qed
 
 lemma