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>)"
```