--- a/Admin/build/TUM.toml Thu Nov 21 23:07:06 2024 +0100
+++ b/Admin/build/TUM.toml Fri Nov 22 20:21:36 2024 +0100
@@ -1,11 +1,11 @@
# Build cluster resources at TUM
[host.lxbroy10]
-hostname = "lxbroy10.informatik.tu-muenchen.de"
+hostname = "lxbroy10.in.tum.de"
numa = true
[host.vmnipkow9]
-hostname = "vmnipkow9.informatik.tu-muenchen.de"
+hostname = "vmnipkow9.in.tum.de"
[host.mini1]
hostname = "131.159.47.71"
--- a/Admin/etc/options Thu Nov 21 23:07:06 2024 +0100
+++ b/Admin/etc/options Fri Nov 22 20:21:36 2024 +0100
@@ -2,7 +2,7 @@
section "Admin tools"
-option isabelle_components_server : string = "lxbroy10.informatik.tu-muenchen.de"
+option isabelle_components_server : string = "lxbroy10.in.tum.de"
-- "user@host for SSH connection"
option isabelle_components_dir : string = "/p/home/isabelle/components"
--- a/NEWS Thu Nov 21 23:07:06 2024 +0100
+++ b/NEWS Fri Nov 22 20:21:36 2024 +0100
@@ -187,6 +187,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/Cartesian_Space.thy Thu Nov 21 23:07:06 2024 +0100
+++ b/src/HOL/Analysis/Cartesian_Space.thy Fri Nov 22 20:21:36 2024 +0100
@@ -353,11 +353,6 @@
shows "invertible (transpose A)"
by (meson assms invertible_def matrix_left_right_inverse right_invertible_transpose)
-lemma vector_matrix_mul_assoc:
- fixes v :: "('a::comm_semiring_1)^'n"
- shows "(v v* M) v* N = v v* (M ** N)"
- by (metis (no_types, opaque_lifting) matrix_transpose_mul matrix_vector_mul_assoc transpose_matrix_vector)
-
lemma matrix_scaleR_vector_ac:
fixes A :: "real^('m::finite)^'n"
shows "A *v (k *\<^sub>R v) = k *\<^sub>R A *v v"
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Nov 21 23:07:06 2024 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Fri Nov 22 20:21:36 2024 +0100
@@ -986,7 +986,7 @@
definition\<^marker>\<open>tag important\<close> vector_matrix_mult :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "
(infixl \<open>v*\<close> 70)
- where "v v* m == (\<chi> j. sum (\<lambda>i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n"
+ where "v v* m == (\<chi> j. sum (\<lambda>i. ((v$i) * (m$i)$j)) (UNIV :: 'm set)) :: 'a^'n"
definition\<^marker>\<open>tag unimportant\<close> "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
definition\<^marker>\<open>tag unimportant\<close> transpose where
@@ -1018,25 +1018,26 @@
unfolding matrix_matrix_mult_def mat_def
by (auto simp: if_distrib if_distribR sum.delta'[OF finite] cong: if_cong)
-proposition matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
+lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc)
- apply (subst sum.swap)
- apply simp
- done
+ using sum.swap by fastforce
-proposition matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
+lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
apply (vector matrix_matrix_mult_def matrix_vector_mult_def
sum_distrib_left sum_distrib_right mult.assoc)
- apply (subst sum.swap)
- apply simp
- done
+ using sum.swap by fastforce
-proposition scalar_matrix_assoc:
+lemma vector_matrix_mul_assoc: "(x v* A) v* B = x v* (A**B)"
+ apply (vector matrix_matrix_mult_def vector_matrix_mult_def
+ sum_distrib_left sum_distrib_right mult.assoc)
+ using sum.swap by fastforce
+
+lemma scalar_matrix_assoc:
fixes A :: "('a::real_algebra_1)^'m^'n"
shows "k *\<^sub>R (A ** B) = (k *\<^sub>R A) ** B"
by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff scaleR_sum_right)
-proposition matrix_scalar_ac:
+lemma matrix_scalar_ac:
fixes A :: "('a::real_algebra_1)^'m^'n"
shows "A ** (k *\<^sub>R B) = k *\<^sub>R A ** B"
by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff)
@@ -1046,6 +1047,13 @@
apply (simp add: if_distrib if_distribR cong del: if_weak_cong)
done
+lemma vector_matrix_mul_rid [simp]:
+ fixes v :: "('a::semiring_1)^'n"
+ shows "v v* mat 1 = v"
+ apply (vector vector_matrix_mult_def mat_def)
+ apply (simp add: if_distrib if_distribR cong del: if_weak_cong)
+ done
+
lemma matrix_transpose_mul:
"transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"
by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult.commute)
@@ -1139,6 +1147,11 @@
unfolding vector_matrix_mult_def
by (simp add: algebra_simps sum.distrib vec_eq_iff)
+lemma vector_matrix_mult_diff_distrib [algebra_simps]:
+ fixes A :: "'a::ring_1^'n^'m"
+ shows "(x - y) v* A = x v* A - y v* A"
+ by (vector vector_matrix_mult_def sum_subtractf left_diff_distrib)
+
lemma matrix_vector_right_distrib [algebra_simps]:
"A *v (x + y) = A *v x + A *v y"
by (vector matrix_vector_mult_def sum.distrib distrib_left)
@@ -1168,6 +1181,15 @@
shows "(A - B) *v x = (A *v x) - (B *v x)"
by (vector matrix_vector_mult_def sum_subtractf left_diff_distrib)
+lemma vector_matrix_mult_add_rdistrib [algebra_simps]:
+ "x v* (A + B) = (x v* A) + (x v* B)"
+ by (vector vector_matrix_mult_def sum.distrib distrib_left)
+
+lemma vector_matrix_mult_diff_rdistrib [algebra_simps]:
+ fixes A :: "'a :: ring_1^'n^'m"
+ shows "x v* (A - B) = (x v* A) - (x v* B)"
+ by (vector vector_matrix_mult_def sum_subtractf right_diff_distrib)
+
lemma matrix_vector_column:
"(A::'a::comm_semiring_1^'n^_) *v x = sum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult.commute)
@@ -1201,19 +1223,19 @@
unfolding invertible_def by auto
qed
-proposition scalar_invertible_iff:
+lemma scalar_invertible_iff:
fixes A :: "('a::real_algebra_1)^'m^'n"
assumes "k \<noteq> 0" and "invertible A"
shows "invertible (k *\<^sub>R A) \<longleftrightarrow> k \<noteq> 0 \<and> invertible A"
by (simp add: assms scalar_invertible)
-lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v x"
+lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v (x:: 'a::{comm_semiring_1}^'n)"
unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
- by simp
+ by (simp add: mult.commute)
-lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* A"
+lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* (A:: 'a::{comm_semiring_1}^'m^'n)"
unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
- by simp
+ by (simp add: mult.commute)
lemma vector_scalar_commute:
fixes A :: "'a::{field}^'m^'n"
@@ -1231,23 +1253,17 @@
lemma vector_matrix_mult_0_right [simp]: "x v* 0 = 0"
unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
-lemma vector_matrix_mul_rid [simp]:
- fixes v :: "('a::semiring_1)^'n"
- shows "v v* mat 1 = v"
- by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix)
-
lemma scaleR_vector_matrix_assoc:
fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)"
by (metis matrix_vector_mult_scaleR transpose_matrix_vector)
-proposition vector_scaleR_matrix_ac:
+lemma vector_scaleR_matrix_ac:
fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
proof -
have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A"
- unfolding vector_matrix_mult_def
- by (simp add: algebra_simps)
+ by (simp add: vector_matrix_mult_def algebra_simps)
with scaleR_vector_matrix_assoc
show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
by auto
--- a/src/HOL/Analysis/Summation_Tests.thy Thu Nov 21 23:07:06 2024 +0100
+++ b/src/HOL/Analysis/Summation_Tests.thy Fri Nov 22 20:21:36 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 Thu Nov 21 23:07:06 2024 +0100
+++ b/src/HOL/Computational_Algebra/Nth_Powers.thy Fri Nov 22 20:21:36 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/Hilbert_Choice.thy Thu Nov 21 23:07:06 2024 +0100
+++ b/src/HOL/Hilbert_Choice.thy Fri Nov 22 20:21:36 2024 +0100
@@ -147,6 +147,34 @@
qed
+subsection \<open>Getting an element of a nonempty set\<close>
+
+definition some_elem :: "'a set \<Rightarrow> 'a"
+ where "some_elem A = (SOME x. x \<in> A)"
+
+lemma some_elem_eq [simp]: "some_elem {x} = x"
+ by (simp add: some_elem_def)
+
+lemma some_elem_nonempty: "A \<noteq> {} \<Longrightarrow> some_elem A \<in> A"
+ unfolding some_elem_def by (auto intro: someI)
+
+lemma is_singleton_some_elem: "is_singleton A \<longleftrightarrow> A = {some_elem A}"
+ by (auto simp: is_singleton_def)
+
+lemma some_elem_image_unique:
+ assumes "A \<noteq> {}"
+ and *: "\<And>y. y \<in> A \<Longrightarrow> f y = a"
+ shows "some_elem (f ` A) = a"
+ unfolding some_elem_def
+proof (rule some1_equality)
+ from \<open>A \<noteq> {}\<close> obtain y where "y \<in> A" by auto
+ with * \<open>y \<in> A\<close> have "a \<in> f ` A" by blast
+ then show "a \<in> f ` A" by auto
+ with * show "\<exists>!x. x \<in> f ` A"
+ by auto
+qed
+
+
subsection \<open>Function Inverse\<close>
lemma inv_def: "inv f = (\<lambda>y. SOME x. f x = y)"
--- a/src/HOL/Library/Discrete.thy Thu Nov 21 23:07:06 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 Fri Nov 22 20:21:36 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 Thu Nov 21 23:07:06 2024 +0100
+++ b/src/HOL/Library/Library.thy Fri Nov 22 20:21:36 2024 +0100
@@ -21,7 +21,7 @@
Countable_Set_Type
Debug
Diagonal_Subsequence
- Discrete
+ Discrete_Functions
Disjoint_Sets
Disjoint_FSets
Dlist
--- a/src/HOL/Set.thy Thu Nov 21 23:07:06 2024 +0100
+++ b/src/HOL/Set.thy Fri Nov 22 20:21:36 2024 +0100
@@ -1834,14 +1834,13 @@
lemma the_elem_image_unique:
assumes "A \<noteq> {}"
- and *: "\<And>y. y \<in> A \<Longrightarrow> f y = f x"
- shows "the_elem (f ` A) = f x"
+ and *: "\<And>y. y \<in> A \<Longrightarrow> f y = a"
+ shows "the_elem (f ` A) = a"
unfolding the_elem_def
proof (rule the1_equality)
from \<open>A \<noteq> {}\<close> obtain y where "y \<in> A" by auto
- with * have "f x = f y" by simp
- with \<open>y \<in> A\<close> have "f x \<in> f ` A" by blast
- with * show "f ` A = {f x}" by auto
+ with * \<open>y \<in> A\<close> have "a \<in> f ` A" by blast
+ with * show "f ` A = {a}" by auto
then show "\<exists>!x. f ` A = {x}" by auto
qed
--- a/src/HOL/Tools/try0.ML Thu Nov 21 23:07:06 2024 +0100
+++ b/src/HOL/Tools/try0.ML Fri Nov 22 20:21:36 2024 +0100
@@ -48,8 +48,11 @@
datatype modifier = Use | Simp | Intro | Elim | Dest
fun string_of_xthm (xref, args) =
- (case xref of Facts.Fact literal => cartouche literal | _ => Facts.string_of_ref xref) ^
- implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
+ (case xref of
+ Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche
+ | _ =>
+ Facts.string_of_ref xref) ^ implode
+ (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
fun add_attr_text tagged (tag, src) s =
let
@@ -74,19 +77,16 @@
val ctxt = Proof.context_of st
- val using_text =
- (K (Method.insert (Attrib.eval_thms ctxt unused)))
- |> Method.Basic
-
val text =
name ^ attrs
|> parse_method ctxt
|> Method.method_cmd ctxt
|> Method.Basic
|> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m]))
- |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Then, [using_text, m]))
- val apply = text |> Proof.refine #> Seq.filter_results
+ val apply =
+ Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)]
+ #> Proof.refine text #> Seq.filter_results
val num_before = num_goals st
val multiple_goals = all_goals andalso num_before > 1
val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st
--- a/src/HOL/ex/Function_Growth.thy Thu Nov 21 23:07:06 2024 +0100
+++ b/src/HOL/ex/Function_Growth.thy Fri Nov 22 20:21:36 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