# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1479996245 -3600
# Node ID 8c44dfb4ca8a4f67ed33b23fb1969312f3ba0670
# Parent  49b78f1f9e016af29601151edc3bfddce1ba1e75
Merged natlog2 into Discrete.log

diff -r 49b78f1f9e01 -r 8c44dfb4ca8a src/HOL/Analysis/Summation_Tests.thy
--- a/src/HOL/Analysis/Summation_Tests.thy	Wed Nov 23 16:28:42 2016 +0100
+++ b/src/HOL/Analysis/Summation_Tests.thy	Thu Nov 24 15:04:05 2016 +0100
@@ -7,6 +7,7 @@
 theory Summation_Tests
 imports
   Complex_Main
+  "~~/src/HOL/Library/Discrete"
   "~~/src/HOL/Library/Extended_Real"
   "~~/src/HOL/Library/Liminf_Limsup"
 begin
@@ -16,89 +17,6 @@
   various summability tests, lemmas to compute the radius of convergence etc.
 \<close>
 
-subsection \<open>Rounded dual logarithm\<close>
-
-(* This is required for the Cauchy condensation criterion *)
-
-definition "natlog2 n = (if n = 0 then 0 else nat \<lfloor>log 2 (real_of_nat n)\<rfloor>)"
-
-lemma natlog2_0 [simp]: "natlog2 0 = 0" by (simp add: natlog2_def)
-lemma natlog2_1 [simp]: "natlog2 1 = 0" by (simp add: natlog2_def)
-lemma natlog2_eq_0_iff: "natlog2 n = 0 \<longleftrightarrow> n < 2" by (simp add: natlog2_def)
-
-lemma natlog2_power_of_two [simp]: "natlog2 (2 ^ n) = n"
-  by (simp add: natlog2_def log_nat_power)
-
-lemma natlog2_mono: "m \<le> n \<Longrightarrow> natlog2 m \<le> natlog2 n"
-  unfolding natlog2_def by (simp_all add: nat_mono floor_mono)
-
-lemma pow_natlog2_le: "n > 0 \<Longrightarrow> 2 ^ natlog2 n \<le> n"
-proof -
-  assume n: "n > 0"
-  from n have "of_nat (2 ^ natlog2 n) = 2 powr real_of_nat (nat \<lfloor>log 2 (real_of_nat n)\<rfloor>)"
-    by (subst powr_realpow) (simp_all add: natlog2_def)
-  also have "\<dots> = 2 powr of_int \<lfloor>log 2 (real_of_nat n)\<rfloor>" using n by simp
-  also have "\<dots> \<le> 2 powr log 2 (real_of_nat n)" by (intro powr_mono) (linarith, simp_all)
-  also have "\<dots> = of_nat n" using n by simp
-  finally show ?thesis by simp
-qed
-
-lemma pow_natlog2_gt: "n > 0 \<Longrightarrow> 2 * 2 ^ natlog2 n > n"
-  and pow_natlog2_ge: "n > 0 \<Longrightarrow> 2 * 2 ^ natlog2 n \<ge> n"
-proof -
-  assume n: "n > 0"
-  from n have "of_nat n = 2 powr log 2 (real_of_nat n)" by simp
-  also have "\<dots> < 2 powr (1 + of_int \<lfloor>log 2 (real_of_nat n)\<rfloor>)"
-    by (intro powr_less_mono) (linarith, simp_all)
-  also from n have "\<dots> = 2 powr (1 + real_of_nat (nat \<lfloor>log 2 (real_of_nat n)\<rfloor>))" by simp
-  also from n have "\<dots> = of_nat (2 * 2 ^ natlog2 n)"
-    by (simp_all add: natlog2_def powr_real_of_int powr_add)
-  finally show "2 * 2 ^ natlog2 n > n" by (rule of_nat_less_imp_less)
-  thus "2 * 2 ^ natlog2 n \<ge> n" by simp
-qed
-
-lemma natlog2_eqI:
-  assumes "n > 0" "2^k \<le> n" "n < 2 * 2^k"
-  shows   "natlog2 n = k"
-proof -
-  from assms have "of_nat (2 ^ k) \<le> real_of_nat n"  by (subst of_nat_le_iff) simp_all
-  hence "real_of_int (int k) \<le> log (of_nat 2) (real_of_nat n)"
-    by (subst le_log_iff) (simp_all add: powr_realpow assms del: of_nat_le_iff)
-  moreover from assms have "real_of_nat n < of_nat (2 ^ Suc k)" by (subst of_nat_less_iff) simp_all
-  hence "log 2 (real_of_nat n) < of_nat k + 1"
-    by (subst log_less_iff) (simp_all add: assms powr_realpow powr_add)
-  ultimately have "\<lfloor>log 2 (real_of_nat n)\<rfloor> = of_nat k" by (intro floor_unique) simp_all
-  with assms show ?thesis by (simp add: natlog2_def)
-qed
-
-lemma natlog2_rec:
-  assumes "n \<ge> 2"
-  shows   "natlog2 n = 1 + natlog2 (n div 2)"
-proof (rule natlog2_eqI)
-  from assms have "2 ^ (1 + natlog2 (n div 2)) \<le> 2 * (n div 2)"
-    by (simp add: pow_natlog2_le)
-  also have "\<dots> \<le> n" by simp
-  finally show "2 ^ (1 + natlog2 (n div 2)) \<le> n" .
-next
-  from assms have "n < 2 * (n div 2 + 1)" by simp
-  also from assms have "(n div 2) < 2 ^ (1 + natlog2 (n div 2))"
-    by (simp add: pow_natlog2_gt)
-  hence "2 * (n div 2 + 1) \<le> 2 * (2 ^ (1 + natlog2 (n div 2)))"
-    by (intro mult_left_mono) simp_all
-  finally show "n < 2 * 2 ^ (1 + natlog2 (n div 2))" .
-qed (insert assms, simp_all)
-
-fun natlog2_aux where
-  "natlog2_aux n acc = (if (n::nat) < 2 then acc else natlog2_aux (n div 2) (acc + 1))"
-
-lemma natlog2_aux_correct:
-  "natlog2_aux n acc = acc + natlog2 n"
-  by (induction n acc rule: natlog2_aux.induct) (auto simp: natlog2_rec natlog2_eq_0_iff)
-
-lemma natlog2_code [code]: "natlog2 n = natlog2_aux n 0"
-  by (subst natlog2_aux_correct) simp
-
-
 subsection \<open>Convergence tests for infinite sums\<close>
 
 subsubsection \<open>Root test\<close>
@@ -216,33 +134,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 ^ natlog2 k))" (is "?thesis1")
-          "(\<Sum>k=1..<n. f k) \<le> (\<Sum>k=1..<n. f (2 ^ natlog2 k))" (is "?thesis2")
-  by (intro sum_mono mono pow_natlog2_ge pow_natlog2_le, simp, simp)+
+  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)+
 
-private lemma condensation_condense1: "(\<Sum>k=1..<2^n. f (2 ^ natlog2 k)) = (\<Sum>k<n. 2^k * f (2 ^ k))"
+private lemma condensation_condense1: "(\<Sum>k=1..<2^n. f (2 ^ Discrete.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 ^ natlog2 k)) =
-                 (\<Sum>k<n. 2^k * f (2^k)) + (\<Sum>k = 2^n..<2^Suc n. f (2^natlog2 k))"
+  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))"
     by (subst sum.union_disjoint) (insert Suc, auto)
-  also have "natlog2 k = n" if "k \<in> {2^n..<2^Suc n}" for k using that by (intro natlog2_eqI) simp_all
-  hence "(\<Sum>k = 2^n..<2^Suc n. f (2^natlog2 k)) = (\<Sum>(_::nat) = 2^n..<2^Suc n. f (2^n))"
+  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))"
     by (intro sum.cong) simp_all
   also have "\<dots> = 2^n * f (2^n)" by (simp add: of_nat_power)
   finally show ?case by simp
 qed simp
 
-private lemma condensation_condense2: "(\<Sum>k=1..<2^n. f (2 * 2 ^ natlog2 k)) = (\<Sum>k<n. 2^k * f (2 ^ Suc k))"
+private lemma condensation_condense2: "(\<Sum>k=1..<2^n. f (2 * 2 ^ Discrete.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 ^ natlog2 k)) =
-                 (\<Sum>k<n. 2^k * f (2^Suc k)) + (\<Sum>k = 2^n..<2^Suc n. f (2 * 2^natlog2 k))"
+  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))"
     by (subst sum.union_disjoint) (insert Suc, auto)
-  also have "natlog2 k = n" if "k \<in> {2^n..<2^Suc n}" for k using that by (intro natlog2_eqI) simp_all
-  hence "(\<Sum>k = 2^n..<2^Suc n. f (2*2^natlog2 k)) = (\<Sum>(_::nat) = 2^n..<2^Suc n. f (2^Suc n))"
+  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))"
     by (intro sum.cong) simp_all
   also have "\<dots> = 2^n * f (2^Suc n)" by (simp add: of_nat_power)
   finally show ?case by simp
diff -r 49b78f1f9e01 -r 8c44dfb4ca8a src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Wed Nov 23 16:28:42 2016 +0100
+++ b/src/HOL/Library/Discrete.thy	Thu Nov 24 15:04:05 2016 +0100
@@ -3,7 +3,7 @@
 section \<open>Common discrete functions\<close>
 
 theory Discrete
-imports Main
+imports Complex_Main
 begin
 
 subsection \<open>Discrete logarithm\<close>
@@ -111,6 +111,62 @@
   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>