src/HOL/NSA/HTranscendental.thy
changeset 60017 b785d6d06430
parent 59730 b7c394c7a619
child 61945 1135b8de26c3
     1.1 --- a/src/HOL/NSA/HTranscendental.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/NSA/HTranscendental.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -306,34 +306,37 @@
     1.4  lemma starfun_exp_gt_one [simp]: "!!x::hypreal. 0 < x ==> 1 < ( *f* exp) x"
     1.5  by transfer (rule exp_gt_one)
     1.6  
     1.7 -lemma starfun_ln_exp [simp]: "!!x. ( *f* ln) (( *f* exp) x) = x"
     1.8 +abbreviation real_ln :: "real \<Rightarrow> real" where 
     1.9 +  "real_ln \<equiv> ln"
    1.10 +
    1.11 +lemma starfun_ln_exp [simp]: "!!x. ( *f* real_ln) (( *f* exp) x) = x"
    1.12  by transfer (rule ln_exp)
    1.13  
    1.14 -lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* ln) x) = x) = (0 < x)"
    1.15 +lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)"
    1.16  by transfer (rule exp_ln_iff)
    1.17  
    1.18 -lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* ln) x = u"
    1.19 +lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* real_ln) x = u"
    1.20  by transfer (rule ln_unique)
    1.21  
    1.22 -lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* ln) x < x"
    1.23 +lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* real_ln) x < x"
    1.24  by transfer (rule ln_less_self)
    1.25  
    1.26 -lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* ln) x"
    1.27 +lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* real_ln) x"
    1.28  by transfer (rule ln_ge_zero)
    1.29  
    1.30 -lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* ln) x"
    1.31 +lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* real_ln) x"
    1.32  by transfer (rule ln_gt_zero)
    1.33  
    1.34 -lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
    1.35 +lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* real_ln) x \<noteq> 0"
    1.36  by transfer simp
    1.37  
    1.38 -lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
    1.39 +lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* real_ln) x \<in> HFinite"
    1.40  apply (rule HFinite_bounded)
    1.41  apply assumption 
    1.42  apply (simp_all add: starfun_ln_less_self order_less_imp_le)
    1.43  done
    1.44  
    1.45 -lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
    1.46 +lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* real_ln) (inverse x) = -( *f* ln) x"
    1.47  by transfer (rule ln_inverse)
    1.48  
    1.49  lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) (x::hypreal)\<bar> = ( *f* exp) x"
    1.50 @@ -360,7 +363,7 @@
    1.51  
    1.52  (* using previous result to get to result *)
    1.53  lemma starfun_ln_HInfinite:
    1.54 -     "[| x \<in> HInfinite; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
    1.55 +     "[| x \<in> HInfinite; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
    1.56  apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
    1.57  apply (drule starfun_exp_HFinite)
    1.58  apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
    1.59 @@ -374,7 +377,7 @@
    1.60  
    1.61  (* check out this proof!!! *)
    1.62  lemma starfun_ln_HFinite_not_Infinitesimal:
    1.63 -     "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HFinite"
    1.64 +     "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HFinite"
    1.65  apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
    1.66  apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
    1.67  apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
    1.68 @@ -383,22 +386,22 @@
    1.69  
    1.70  (* we do proof by considering ln of 1/x *)
    1.71  lemma starfun_ln_Infinitesimal_HInfinite:
    1.72 -     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
    1.73 +     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
    1.74  apply (drule Infinitesimal_inverse_HInfinite)
    1.75  apply (frule positive_imp_inverse_positive)
    1.76  apply (drule_tac [2] starfun_ln_HInfinite)
    1.77  apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
    1.78  done
    1.79  
    1.80 -lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
    1.81 +lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* real_ln) x < 0"
    1.82  by transfer (rule ln_less_zero)
    1.83  
    1.84  lemma starfun_ln_Infinitesimal_less_zero:
    1.85 -     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
    1.86 +     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x < 0"
    1.87  by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
    1.88  
    1.89  lemma starfun_ln_HInfinite_gt_zero:
    1.90 -     "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"
    1.91 +     "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* real_ln) x"
    1.92  by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
    1.93  
    1.94