adapt to Isabelle/c726ecfb22b6
authorhuffman
Tue Mar 18 11:58:30 2014 -0700 (2014-03-18)
changeset 56195c7dfd924a165
parent 56194 9ffbb4004c81
child 56196 32b7eafc5a52
adapt to Isabelle/c726ecfb22b6
src/HOL/Decision_Procs/Approximation.thy
src/HOL/ex/HarmonicSeries.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 18 16:29:32 2014 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 18 11:58:30 2014 -0700
     1.3 @@ -371,7 +371,7 @@
     1.4  
     1.5      have "\<bar> real x \<bar> \<le> 1"  using `0 \<le> real x` `real x \<le> 1` by auto
     1.6      from mp[OF summable_Leibniz(2)[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]] prem, THEN spec, of m, unfolded `2 * m = n`]
     1.7 -    show ?thesis unfolding arctan_series[OF `\<bar> real x \<bar> \<le> 1`] Suc_eq_plus1  .
     1.8 +    show ?thesis unfolding arctan_series[OF `\<bar> real x \<bar> \<le> 1`] Suc_eq_plus1 atLeast0LessThan .
     1.9    qed auto
    1.10    note arctan_bounds = this[unfolded atLeastAtMost_iff]
    1.11  
    1.12 @@ -744,7 +744,7 @@
    1.13      also have "\<dots> =
    1.14        (\<Sum> j = 0 ..< n. -1 ^ ((2 * j) div 2) / (real (fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto
    1.15      also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then -1 ^ (i div 2) / (real (fact i)) * x ^ i else 0)"
    1.16 -      unfolding sum_split_even_odd ..
    1.17 +      unfolding sum_split_even_odd atLeast0LessThan ..
    1.18      also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then -1 ^ (i div 2) / (real (fact i)) else 0) * x ^ i)"
    1.19        by (rule setsum_cong2) auto
    1.20      finally show ?thesis by assumption
    1.21 @@ -758,7 +758,7 @@
    1.22        + (cos (t + 1/2 * (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)"
    1.23        (is "_ = ?SUM + ?rest / ?fact * ?pow")
    1.24        using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`]
    1.25 -      unfolding cos_coeff_def by auto
    1.26 +      unfolding cos_coeff_def atLeast0LessThan by auto
    1.27  
    1.28      have "cos t * -1^n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
    1.29      also have "\<dots> = cos (t + n * pi)"  using cos_add by auto
    1.30 @@ -860,7 +860,7 @@
    1.31        have pow: "!!i. x ^ (2 * i + 1) = x * x ^ (2 * i)" by auto
    1.32        have "?SUM = (\<Sum> j = 0 ..< n. 0) + ?SUM" by auto
    1.33        also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i)) * x ^ i)"
    1.34 -        unfolding sum_split_even_odd ..
    1.35 +        unfolding sum_split_even_odd atLeast0LessThan ..
    1.36        also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i))) * x ^ i)"
    1.37          by (rule setsum_cong2) auto
    1.38        finally show ?thesis by assumption
    1.39 @@ -873,7 +873,7 @@
    1.40        + (sin (t + 1/2 * (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)"
    1.41        (is "_ = ?SUM + ?rest / ?fact * ?pow")
    1.42        using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
    1.43 -      unfolding sin_coeff_def by auto
    1.44 +      unfolding sin_coeff_def atLeast0LessThan by auto
    1.45  
    1.46      have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add distrib_right distrib_left by auto
    1.47      moreover
    1.48 @@ -1344,7 +1344,7 @@
    1.49      also have "\<dots> \<le> exp x"
    1.50      proof -
    1.51        obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_even n. real x ^ m / real (fact m)) + exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
    1.52 -        using Maclaurin_exp_le by blast
    1.53 +        using Maclaurin_exp_le unfolding atLeast0LessThan by blast
    1.54        moreover have "0 \<le> exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
    1.55          by (auto intro!: mult_nonneg_nonneg divide_nonneg_pos simp add: zero_le_even_power)
    1.56        ultimately show ?thesis
    1.57 @@ -1364,7 +1364,7 @@
    1.58      qed
    1.59  
    1.60      obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_odd n. (real x) ^ m / real (fact m)) + exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n)"
    1.61 -      using Maclaurin_exp_le by blast
    1.62 +      using Maclaurin_exp_le unfolding atLeast0LessThan by blast
    1.63      moreover have "exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n) \<le> 0"
    1.64        by (auto intro!: mult_nonneg_nonpos divide_nonpos_pos simp add: x_less_zero)
    1.65      ultimately have "exp x \<le> (\<Sum>j = 0..<get_odd n. 1 / real (fact j) * real x ^ j)"
    1.66 @@ -1603,7 +1603,7 @@
    1.67        thus "x ^ Suc (Suc n) \<le> x ^ Suc n" by auto
    1.68      qed auto }
    1.69    from summable_Leibniz'(2,4)[OF `?a ----> 0` `\<And>n. 0 \<le> ?a n`, OF `\<And>n. ?a (Suc n) \<le> ?a n`, unfolded ln_eq]
    1.70 -  show "?lb" and "?ub" by auto
    1.71 +  show "?lb" and "?ub" unfolding atLeast0LessThan by auto
    1.72  qed
    1.73  
    1.74  lemma ln_float_bounds:
    1.75 @@ -3031,7 +3031,7 @@
    1.76          and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) =
    1.77             (\<Sum>m = 0..<Suc n'. F m c / real (fact m) * (xs ! x - c) ^ m) +
    1.78             F (Suc n') t / real (fact (Suc n')) * (xs ! x - c) ^ Suc n'"
    1.79 -        by blast
    1.80 +        unfolding atLeast0LessThan by blast
    1.81  
    1.82        from t_bnd bnd_xs bnd_c have *: "t \<in> {lx .. ux}"
    1.83          by (cases "xs ! x < c", auto)
     2.1 --- a/src/HOL/ex/HarmonicSeries.thy	Tue Mar 18 16:29:32 2014 +0100
     2.2 +++ b/src/HOL/ex/HarmonicSeries.thy	Tue Mar 18 11:58:30 2014 -0700
     2.3 @@ -284,7 +284,7 @@
     2.4    proof -
     2.5      have "\<forall>n. 0 \<le> ?f n" by simp
     2.6      with sf have "?s \<ge> 0"
     2.7 -      by - (rule suminf_0_le, simp_all)
     2.8 +      by - (rule suminf_ge_zero, simp_all)
     2.9      then have cgt0: "\<lceil>2*?s\<rceil> \<ge> 0" by simp
    2.10  
    2.11      from ndef have "n = nat \<lceil>(2*?s)\<rceil>" .
    2.12 @@ -298,7 +298,7 @@
    2.13  
    2.14    obtain j where jdef: "j = (2::nat)^n" by simp
    2.15    have "\<forall>m\<ge>j. 0 < ?f m" by simp
    2.16 -  with sf have "(\<Sum>i\<in>{0..<j}. ?f i) < ?s" by (rule series_pos_less)
    2.17 +  with sf have "(\<Sum>i\<in>{0..<j}. ?f i) < ?s" unfolding atLeast0LessThan by (rule series_pos_less)
    2.18    then have "(\<Sum>i\<in>{1..<Suc j}. 1/(real i)) < ?s"
    2.19      apply -
    2.20      apply (subst(asm) setsum_shift_bounds_Suc_ivl [symmetric])