Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
authorpaulson <lp15@cam.ac.uk>
Thu Mar 16 13:55:29 2017 +0000 (2017-03-16)
changeset 65273917ae0ba03a2
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
src/HOL/MacLaurin.thy
src/HOL/Set_Interval.thy
     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)