Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/NSA/HTranscendental.thy
changeset 56194 9ffbb4004c81
parent 54489 03ff4d1e6784
child 57512 cc97b347b301 
--- a/src/HOL/NSA/HTranscendental.thy	Tue Mar 18 15:53:48 2014 +0100
+++ b/src/HOL/NSA/HTranscendental.thy	Tue Mar 18 16:29:32 2014 +0100
@@ -215,22 +215,21 @@
 lemma HFinite_exp [simp]:
      "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
 unfolding sumhr_app
-apply (simp only: star_zero_def starfun2_star_of)
+apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
 apply (rule NSBseqD2)
 apply (rule NSconvergent_NSBseq)
 apply (rule convergent_NSconvergent_iff [THEN iffD1])
-apply (rule summable_convergent_sumr_iff [THEN iffD1])
+apply (rule summable_iff_convergent [THEN iffD1])
 apply (rule summable_exp)
 done
 
 lemma exphr_zero [simp]: "exphr 0 = 1"
-apply (simp add: exphr_def sumhr_split_add
-                   [OF hypnat_one_less_hypnat_omega, symmetric])
+apply (simp add: exphr_def sumhr_split_add [OF hypnat_one_less_hypnat_omega, symmetric])
 apply (rule st_unique, simp)
 apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
 apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
 apply (rule_tac x="whn" in spec)
-apply (unfold sumhr_app, transfer, simp)
+apply (unfold sumhr_app, transfer, simp add: power_0_left)
 done
 
 lemma coshr_zero [simp]: "coshr 0 = 1"
@@ -240,7 +239,7 @@
 apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
 apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
 apply (rule_tac x="whn" in spec)
-apply (unfold sumhr_app, transfer, simp add: cos_coeff_def)
+apply (unfold sumhr_app, transfer, simp add: cos_coeff_def power_0_left)
 done
 
 lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) @= 1"
@@ -271,6 +270,7 @@
 apply (simp add: exphr_def)
 apply (rule st_unique, simp)
 apply (subst starfunNat_sumr [symmetric])
+unfolding atLeast0LessThan
 apply (rule NSLIMSEQ_D [THEN approx_sym])
 apply (rule LIMSEQ_NSLIMSEQ)
 apply (subst sums_def [symmetric])
@@ -406,11 +406,11 @@
 
 lemma HFinite_sin [simp]: "sumhr (0, whn, %n. sin_coeff n * x ^ n) \<in> HFinite"
 unfolding sumhr_app
-apply (simp only: star_zero_def starfun2_star_of)
+apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
 apply (rule NSBseqD2)
 apply (rule NSconvergent_NSBseq)
 apply (rule convergent_NSconvergent_iff [THEN iffD1])
-apply (rule summable_convergent_sumr_iff [THEN iffD1])
+apply (rule summable_iff_convergent [THEN iffD1])
 apply (rule summable_sin)
 done
 
@@ -429,11 +429,11 @@
 
 lemma HFinite_cos [simp]: "sumhr (0, whn, %n. cos_coeff n * x ^ n) \<in> HFinite"
 unfolding sumhr_app
-apply (simp only: star_zero_def starfun2_star_of)
+apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
 apply (rule NSBseqD2)
 apply (rule NSconvergent_NSBseq)
 apply (rule convergent_NSconvergent_iff [THEN iffD1])
-apply (rule summable_convergent_sumr_iff [THEN iffD1])
+apply (rule summable_iff_convergent [THEN iffD1])
 apply (rule summable_cos)
 done
isabelle