src/HOL/Analysis/Harmonic_Numbers.thy

 
 lemma of_real_harm: "of_real (harm n) = harm n"
   unfolding harm_def by simp
 
 lemma abs_harm [simp]: "(abs (harm n) :: real) = harm n"
-  using harm_nonneg[of n] by (rule abs_of_nonneg)    
+  using harm_nonneg[of n] by (rule abs_of_nonneg)
 
 lemma norm_harm: "norm (harm n) = harm n"
   by (subst of_real_harm [symmetric]) (simp add: harm_nonneg)
 
 lemma harm_expand:

 lemma harm_at_top: "filterlim (harm :: nat \<Rightarrow> real) at_top sequentially"
 proof (rule filterlim_at_top_mono)
   show "eventually (\<lambda>n. harm n \<ge> ln (real (Suc n))) at_top"
     using ln_le_harm by (intro always_eventually allI) (simp_all add: add_ac)
   show "filterlim (\<lambda>n. ln (real (Suc n))) at_top sequentially"
-    by (intro filterlim_compose[OF ln_at_top] filterlim_compose[OF filterlim_real_sequentially] 
+    by (intro filterlim_compose[OF ln_at_top] filterlim_compose[OF filterlim_real_sequentially]
               filterlim_Suc)
 qed
 
 
-subsection \<open>The Euler--Mascheroni constant\<close>
+subsection \<open>The Euler-Mascheroni constant\<close>
 
 text \<open>
   The limit of the difference between the partial harmonic sum and the natural logarithm
   (approximately 0.577216). This value occurs e.g. in the definition of the Gamma function.
  \<close>

       by (induction n) (simp_all add: inverse_eq_divide)
   qed
 qed
 
 
-subsection \<open>Bounds on the Euler--Mascheroni constant\<close>
+subsection \<open>Bounds on the Euler-Mascheroni constant\<close>
 
 (* TODO: Move? *)
 lemma ln_inverse_approx_le:
   assumes "(x::real) > 0" "a > 0"
   shows   "ln (x + a) - ln x \<le> a * (inverse x + inverse (x + a))/2" (is "_ \<le> ?A")

     also have "\<dots> = (t - x) * f' + inverse x" using assms
       by (simp add: f'_def divide_simps) (simp add: f'_def field_simps)
     finally show "inverse t \<le> (t - x) * f' + inverse x" .
   qed
   hence "integral {x..x+a} inverse \<le> integral {x..x+a} ?f" using f'_nonpos assms
-    by (intro integral_le has_integral_integrable[OF int1] has_integral_integrable[OF int2] ineq)
+    by (blast intro: integral_le has_integral_integrable[OF int1] has_integral_integrable[OF int2] ineq)
   also have "\<dots> = ?A" using int1 by (rule integral_unique)
   finally show ?thesis .
 qed
 
 lemma ln_inverse_approx_ge:

       by (intro convex_on_imp_above_tangent[of "{0<..}"] convex_on_inverse)
          (auto simp: m_def interior_open f'_def power2_eq_square intro!: derivative_eq_intros)
     thus "(t - m) * f' + inverse m \<le> inverse t" by (simp add: algebra_simps)
   qed
   hence "integral {x..y} inverse \<ge> integral {x..y} (\<lambda>t. (t - m) * f' + inverse m)"
-    using int1 int2 by (intro integral_le has_integral_integrable)
+    using int1 int2 by (blast intro: integral_le has_integral_integrable)
   also have "integral {x..y} (\<lambda>t. (t - m) * f' + inverse m) = ?A"
     using integral_unique[OF int1] by simp
   finally show ?thesis .
 qed
 

     unfolding inv_def
     by (intro sums_divide telescope_sums' LIMSEQ_ignore_initial_segment LIMSEQ_inverse_real_of_nat)
   from euler_mascheroni_sum_real have "euler_mascheroni = (\<Sum>k. D k)"
     by (simp add: sums_iff D_def)
   also have "\<dots> = (\<Sum>k. D (k + Suc n)) + (\<Sum>k\<le>n. D k)"
-    by (subst suminf_split_initial_segment[OF summable, of "Suc n"], 
+    by (subst suminf_split_initial_segment[OF summable, of "Suc n"],
         subst lessThan_Suc_atMost) simp
   finally have sum: "(\<Sum>k\<le>n. D k) - euler_mascheroni = -(\<Sum>k. D (k + Suc n))" by simp
 
   note sum
   also have "\<dots> \<le> -(\<Sum>k. (inv (k + Suc n + 1) - inv (k + Suc n + 2)) / 2)"

   and ln2_le_25_over_36: "ln (2::real) \<le> 25/36"
   using ln_approx_bounds[of 2 1, simplified, simplified eval_nat_numeral, simplified] by simp_all
 
 
 text \<open>
-  Approximation of the Euler--Mascheroni constant. The lower bound is accurate to about 0.0015;
+  Approximation of the Euler-Mascheroni constant. The lower bound is accurate to about 0.0015;
   the upper bound is accurate to about 0.015.
 \<close>
 lemma euler_mascheroni_gt_19_over_33: "(euler_mascheroni :: real) > 19/33" (is ?th1)
   and euler_mascheroni_less_13_over_22: "(euler_mascheroni :: real) < 13/22" (is ?th2)
 proof -