author paulson Thu Mar 16 13:55:29 2017 +0000 (2017-03-16) changeset 65273 917ae0ba03a2 parent 65272 7611c55c39d0 child 65274 db2de50de28e
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
 src/HOL/Analysis/Harmonic_Numbers.thy file | annotate | diff | revisions src/HOL/MacLaurin.thy file | annotate | diff | revisions src/HOL/Set_Interval.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Wed Mar 15 21:52:04 2017 +0100
1.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Mar 16 13:55:29 2017 +0000
1.3 @@ -17,21 +17,6 @@
1.4    and the Euler-Mascheroni constant.
1.5  \<close>
1.6
1.7 -lemma ln_2_less_1: "ln 2 < (1::real)"
1.8 -proof -
1.9 -  have "2 < 5/(2::real)" by simp
1.10 -  also have "5/2 \<le> exp (1::real)" using exp_lower_taylor_quadratic[of 1, simplified] by simp
1.11 -  finally have "exp (ln 2) < exp (1::real)" by simp
1.12 -  thus "ln 2 < (1::real)" by (subst (asm) exp_less_cancel_iff) simp
1.13 -qed
1.14 -
1.15 -lemma sum_Suc_diff':
1.16 -  fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
1.17 -  assumes "m \<le> n"
1.18 -  shows "(\<Sum>i = m..<n. f (Suc i) - f i) = f n - f m"
1.19 -using assms by (induct n) (auto simp: le_Suc_eq)
1.20 -
1.21 -
1.22  subsection \<open>The Harmonic numbers\<close>
1.23
1.24  definition harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
```
```     2.1 --- a/src/HOL/MacLaurin.thy	Wed Mar 15 21:52:04 2017 +0100
2.2 +++ b/src/HOL/MacLaurin.thy	Thu Mar 16 13:55:29 2017 +0000
2.3 @@ -359,10 +359,17 @@
2.4    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"
2.5    using Maclaurin_all_le_objl [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto
2.6
2.7 -lemma exp_lower_taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
2.8 +corollary exp_lower_taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
2.9    for x :: real
2.10    using Maclaurin_exp_le [of x 3] by (auto simp: numeral_3_eq_3 power2_eq_square)
2.11
2.12 +corollary ln_2_less_1: "ln 2 < (1::real)"
2.13 +proof -
2.14 +  have "2 < 5/(2::real)" by simp
2.15 +  also have "5/2 \<le> exp (1::real)" using exp_lower_taylor_quadratic[of 1, simplified] by simp
2.16 +  finally have "exp (ln 2) < exp (1::real)" by simp
2.17 +  thus "ln 2 < (1::real)" by (subst (asm) exp_less_cancel_iff) simp
2.18 +qed
2.19
2.20  subsection \<open>Version for Sine Function\<close>
2.21
```
```     3.1 --- a/src/HOL/Set_Interval.thy	Wed Mar 15 21:52:04 2017 +0100
3.2 +++ b/src/HOL/Set_Interval.thy	Thu Mar 16 13:55:29 2017 +0000
3.3 @@ -709,7 +709,7 @@
3.4
3.5  subsubsection \<open>The Constant @{term greaterThan}\<close>
3.6
3.7 -lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
3.8 +lemma greaterThan_0: "greaterThan 0 = range Suc"
3.9  apply (simp add: greaterThan_def)
3.10  apply (blast dest: gr0_conv_Suc [THEN iffD1])
3.11  done
3.12 @@ -1846,6 +1846,12 @@
3.13    shows "(\<Sum>i = m..n. f(Suc i) - f i) = f (Suc n) - f m"
3.14  using assms by (induct n) (auto simp: le_Suc_eq)
3.15
3.16 +lemma sum_Suc_diff':
3.17 +  fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
3.18 +  assumes "m \<le> n"
3.19 +  shows "(\<Sum>i = m..<n. f (Suc i) - f i) = f n - f m"
3.20 +using assms by (induct n) (auto simp: le_Suc_eq)
3.21 +
3.22  lemma nested_sum_swap:
3.23       "(\<Sum>i = 0..n. (\<Sum>j = 0..<i. a i j)) = (\<Sum>j = 0..<n. \<Sum>i = Suc j..n. a i j)"
3.24    by (induction n) (auto simp: sum.distrib)
```