src/HOL/Hyperreal/HTranscendental.thy
changeset 14430 5cb24165a2e1
parent 14420 4e72cd222e0b
child 14468 6be497cacab5
     1.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Thu Mar 04 10:06:13 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu Mar 04 12:06:07 2004 +0100
     1.3 @@ -555,13 +555,13 @@
     1.4       "n \<in> HNatInfinite  
     1.5        ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
     1.6  apply (frule lemma_sin_pi)
     1.7 -apply (simp add: divide_inverse_zero)
     1.8 +apply (simp add: divide_inverse)
     1.9  done
    1.10  
    1.11  lemma Infinitesimal_pi_divide_HNatInfinite: 
    1.12       "N \<in> HNatInfinite  
    1.13        ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
    1.14 -apply (simp add: divide_inverse_zero)
    1.15 +apply (simp add: divide_inverse)
    1.16  apply (auto intro: Infinitesimal_HFinite_mult2)
    1.17  done
    1.18  
    1.19 @@ -578,7 +578,7 @@
    1.20                     pi_divide_HNatInfinite_not_zero])
    1.21  apply (auto simp add: hypreal_inverse_distrib)
    1.22  apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
    1.23 -apply (auto intro: SReal_inverse simp add: divide_inverse_zero mult_ac)
    1.24 +apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac)
    1.25  done
    1.26  
    1.27  lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
    1.28 @@ -593,7 +593,7 @@
    1.29  lemma starfunNat_pi_divide_n_Infinitesimal: 
    1.30       "N \<in> HNatInfinite ==> ( *fNat* (%x. pi / real x)) N \<in> Infinitesimal"
    1.31  by (auto intro!: Infinitesimal_HFinite_mult2 
    1.32 -         simp add: starfunNat_mult [symmetric] divide_inverse_zero
    1.33 +         simp add: starfunNat_mult [symmetric] divide_inverse
    1.34                     starfunNat_inverse [symmetric] starfunNat_real_of_nat)
    1.35  
    1.36  lemma STAR_sin_pi_divide_n_approx:
    1.37 @@ -601,16 +601,16 @@
    1.38        ( *f* sin) (( *fNat* (%x. pi / real x)) N) @=  
    1.39        hypreal_of_real pi/(hypreal_of_hypnat N)"
    1.40  by (auto intro!: STAR_sin_Infinitesimal Infinitesimal_HFinite_mult2 
    1.41 -         simp add: starfunNat_mult [symmetric] divide_inverse_zero
    1.42 +         simp add: starfunNat_mult [symmetric] divide_inverse
    1.43                     starfunNat_inverse_real_of_nat_eq)
    1.44  
    1.45  lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi"
    1.46  apply (auto simp add: NSLIMSEQ_def starfunNat_mult [symmetric] starfunNat_real_of_nat)
    1.47  apply (rule_tac f1 = sin in starfun_stafunNat_o2 [THEN subst])
    1.48 -apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse_zero)
    1.49 +apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse)
    1.50  apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
    1.51  apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi 
    1.52 -            simp add: starfunNat_real_of_nat mult_commute divide_inverse_zero)
    1.53 +            simp add: starfunNat_real_of_nat mult_commute divide_inverse)
    1.54  done
    1.55  
    1.56  lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1"
    1.57 @@ -618,7 +618,7 @@
    1.58  apply (rule_tac f1 = cos in starfun_stafunNat_o2 [THEN subst])
    1.59  apply (rule STAR_cos_Infinitesimal)
    1.60  apply (auto intro!: Infinitesimal_HFinite_mult2 
    1.61 -            simp add: starfunNat_mult [symmetric] divide_inverse_zero
    1.62 +            simp add: starfunNat_mult [symmetric] divide_inverse
    1.63                        starfunNat_inverse [symmetric] starfunNat_real_of_nat)
    1.64  done
    1.65