# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1489672529 0
# Node ID 917ae0ba03a26d54bde67b8319f09e25522a0f89
# Parent  7611c55c39d06b28d8097293d672879499664d55
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.

diff -r 7611c55c39d0 -r 917ae0ba03a2 src/HOL/Analysis/Harmonic_Numbers.thy
--- a/src/HOL/Analysis/Harmonic_Numbers.thy	Wed Mar 15 21:52:04 2017 +0100
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Mar 16 13:55:29 2017 +0000
@@ -17,21 +17,6 @@
   and the Euler-Mascheroni constant.
 \<close>
 
-lemma ln_2_less_1: "ln 2 < (1::real)"
-proof -
-  have "2 < 5/(2::real)" by simp
-  also have "5/2 \<le> exp (1::real)" using exp_lower_taylor_quadratic[of 1, simplified] by simp
-  finally have "exp (ln 2) < exp (1::real)" by simp
-  thus "ln 2 < (1::real)" by (subst (asm) exp_less_cancel_iff) simp
-qed
-
-lemma sum_Suc_diff':
-  fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
-  assumes "m \<le> n"
-  shows "(\<Sum>i = m..<n. f (Suc i) - f i) = f n - f m"
-using assms by (induct n) (auto simp: le_Suc_eq)
-
-
 subsection \<open>The Harmonic numbers\<close>
 
 definition harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
diff -r 7611c55c39d0 -r 917ae0ba03a2 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Wed Mar 15 21:52:04 2017 +0100
+++ b/src/HOL/MacLaurin.thy	Thu Mar 16 13:55:29 2017 +0000
@@ -359,10 +359,17 @@
   shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. (x ^ m) / fact m) + (exp t / fact n) * x ^ n"
   using Maclaurin_all_le_objl [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto
 
-lemma exp_lower_taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
+corollary exp_lower_taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
   for x :: real
   using Maclaurin_exp_le [of x 3] by (auto simp: numeral_3_eq_3 power2_eq_square)
 
+corollary ln_2_less_1: "ln 2 < (1::real)"
+proof -
+  have "2 < 5/(2::real)" by simp
+  also have "5/2 \<le> exp (1::real)" using exp_lower_taylor_quadratic[of 1, simplified] by simp
+  finally have "exp (ln 2) < exp (1::real)" by simp
+  thus "ln 2 < (1::real)" by (subst (asm) exp_less_cancel_iff) simp
+qed
 
 subsection \<open>Version for Sine Function\<close>
 
diff -r 7611c55c39d0 -r 917ae0ba03a2 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Wed Mar 15 21:52:04 2017 +0100
+++ b/src/HOL/Set_Interval.thy	Thu Mar 16 13:55:29 2017 +0000
@@ -709,7 +709,7 @@
 
 subsubsection \<open>The Constant @{term greaterThan}\<close>
 
-lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
+lemma greaterThan_0: "greaterThan 0 = range Suc"
 apply (simp add: greaterThan_def)
 apply (blast dest: gr0_conv_Suc [THEN iffD1])
 done
@@ -1846,6 +1846,12 @@
   shows "(\<Sum>i = m..n. f(Suc i) - f i) = f (Suc n) - f m"
 using assms by (induct n) (auto simp: le_Suc_eq)
 
+lemma sum_Suc_diff':
+  fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
+  assumes "m \<le> n"
+  shows "(\<Sum>i = m..<n. f (Suc i) - f i) = f n - f m"
+using assms by (induct n) (auto simp: le_Suc_eq)
+
 lemma nested_sum_swap:
      "(\<Sum>i = 0..n. (\<Sum>j = 0..<i. a i j)) = (\<Sum>j = 0..<n. \<Sum>i = Suc j..n. a i j)"
   by (induction n) (auto simp: sum.distrib)