src/HOL/Nonstandard_Analysis/HSeries.thy
changeset 68644 242d298526a3
parent 64604 2bf8cfc98c4d
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Nonstandard_Analysis/HSeries.thy	Sun Jul 15 21:58:50 2018 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/HSeries.thy	Mon Jul 16 23:33:28 2018 +0100
     1.3 @@ -117,10 +117,7 @@
     1.4  
     1.5  lemma sumhr_hrabs_approx [simp]: "sumhr (0, M, f) \<approx> sumhr (0, N, f) \<Longrightarrow> \<bar>sumhr (M, N, f)\<bar> \<approx> 0"
     1.6    using linorder_less_linear [where x = M and y = N]
     1.7 -  apply auto
     1.8 -  apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
     1.9 -  apply (auto dest: approx_hrabs simp add: sumhr_split_diff)
    1.10 -  done
    1.11 +  by (metis (no_types, lifting) abs_zero approx_hrabs approx_minus_iff approx_refl approx_sym sumhr_eq_bounds sumhr_less_bounds_zero sumhr_split_diff)
    1.12  
    1.13  
    1.14  subsection \<open>Infinite sums: Standard and NS theorems\<close>
    1.15 @@ -153,26 +150,16 @@
    1.16        summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
    1.17        NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
    1.18    apply (cut_tac x = M and y = N in linorder_less_linear)
    1.19 -  apply auto
    1.20 -   apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
    1.21 -   apply (rule_tac [2] approx_minus_iff [THEN iffD2])
    1.22 -   apply (auto dest: approx_hrabs_zero_cancel simp: sumhr_split_diff atLeast0LessThan[symmetric])
    1.23 -  done
    1.24 +  by (metis approx_hrabs_zero_cancel approx_minus_iff approx_refl approx_sym sumhr_split_diff)
    1.25  
    1.26  text \<open>Terms of a convergent series tend to zero.\<close>
    1.27  lemma NSsummable_NSLIMSEQ_zero: "NSsummable f \<Longrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
    1.28    apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
    1.29 -  apply (drule bspec)
    1.30 -   apply auto
    1.31 -  apply (drule_tac x = "N + 1 " in bspec)
    1.32 -   apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
    1.33 -  done
    1.34 +  by (metis HNatInfinite_add_one approx_hrabs_zero_cancel sumhr_Suc)
    1.35  
    1.36  text \<open>Nonstandard comparison test.\<close>
    1.37  lemma NSsummable_comparison_test: "\<exists>N. \<forall>n. N \<le> n \<longrightarrow> \<bar>f n\<bar> \<le> g n \<Longrightarrow> NSsummable g \<Longrightarrow> NSsummable f"
    1.38 -  apply (fold summable_NSsummable_iff)
    1.39 -  apply (rule summable_comparison_test, simp, assumption)
    1.40 -  done
    1.41 +  by (metis real_norm_def summable_NSsummable_iff summable_comparison_test)
    1.42  
    1.43  lemma NSsummable_rabs_comparison_test:
    1.44    "\<exists>N. \<forall>n. N \<le> n \<longrightarrow> \<bar>f n\<bar> \<le> g n \<Longrightarrow> NSsummable g \<Longrightarrow> NSsummable (\<lambda>k. \<bar>f k\<bar>)"