# HG changeset patch
# User huffman
# Date 1180362453 -7200
# Node ID 1bd84606b403b32972ebdaa2435eecd70eb7fdce
# Parent  d5cdaa3b7517af5736e74dc1564b9a4316f6dbda
add type annotations for exp

diff -r d5cdaa3b7517 -r 1bd84606b403 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Mon May 28 04:22:44 2007 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Mon May 28 16:27:33 2007 +0200
@@ -245,12 +245,12 @@
 apply (unfold sumhr_app, transfer, simp)
 done
 
-lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1"
-apply (subgoal_tac "( *f* exp) 0 = 1", simp)
+lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) @= 1"
+apply (subgoal_tac "( *f* exp) (0::hypreal) = 1", simp)
 apply (transfer, simp)
 done
 
-lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) x @= 1"
+lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) (x::hypreal) @= 1"
 apply (case_tac "x = 0")
 apply (cut_tac [2] x = 0 in DERIV_exp)
 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
@@ -276,16 +276,16 @@
 apply (rule NSLIMSEQ_D [THEN approx_sym])
 apply (rule LIMSEQ_NSLIMSEQ)
 apply (subst sums_def [symmetric])
-apply (rule exp_converges)
+apply (cut_tac exp_converges [where x=x], simp)
 apply (rule HNatInfinite_whn)
 done
 
-lemma starfun_exp_ge_add_one_self [simp]: "!!x. 0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
+lemma starfun_exp_ge_add_one_self [simp]: "!!x::hypreal. 0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
 by transfer (rule exp_ge_add_one_self_aux)
 
 (* exp (oo) is infinite *)
 lemma starfun_exp_HInfinite:
-     "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) x \<in> HInfinite"
+     "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) (x::hypreal) \<in> HInfinite"
 apply (frule starfun_exp_ge_add_one_self)
 apply (rule HInfinite_ge_HInfinite, assumption)
 apply (rule order_trans [of _ "1+x"], auto) 
@@ -296,14 +296,14 @@
 
 (* exp (-oo) is infinitesimal *)
 lemma starfun_exp_Infinitesimal:
-     "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) x \<in> Infinitesimal"
+     "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) (x::hypreal) \<in> Infinitesimal"
 apply (subgoal_tac "\<exists>y. x = - y")
 apply (rule_tac [2] x = "- x" in exI)
 apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite
             simp add: starfun_exp_minus HInfinite_minus_iff)
 done
 
-lemma starfun_exp_gt_one [simp]: "!!x. 0 < x ==> 1 < ( *f* exp) x"
+lemma starfun_exp_gt_one [simp]: "!!x::hypreal. 0 < x ==> 1 < ( *f* exp) x"
 by transfer (rule exp_gt_one)
 
 (* needs derivative of inverse function
@@ -349,13 +349,13 @@
 lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
 by transfer (rule ln_inverse)
 
-lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) x\<bar> = ( *f* exp) x"
+lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) (x::hypreal)\<bar> = ( *f* exp) x"
 by transfer (rule abs_exp_cancel)
 
-lemma starfun_exp_less_mono: "\<And>x y. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y"
+lemma starfun_exp_less_mono: "\<And>x y::hypreal. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y"
 by transfer (rule exp_less_mono)
 
-lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
+lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) (x::hypreal) \<in> HFinite"
 apply (auto simp add: HFinite_def, rename_tac u)
 apply (rule_tac x="( *f* exp) u" in rev_bexI)
 apply (simp add: Reals_eq_Standard)
@@ -364,7 +364,7 @@
 done
 
 lemma starfun_exp_add_HFinite_Infinitesimal_approx:
-     "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z"
+     "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x::hypreal) @= ( *f* exp) z"
 apply (simp add: STAR_exp_add)
 apply (frule STAR_exp_Infinitesimal)
 apply (drule approx_mult2)
@@ -380,7 +380,7 @@
 done
 
 lemma starfun_exp_HInfinite_Infinitesimal_disj:
- "x \<in> HInfinite ==> ( *f* exp) x \<in> HInfinite | ( *f* exp) x \<in> Infinitesimal"
+ "x \<in> HInfinite ==> ( *f* exp) x \<in> HInfinite | ( *f* exp) (x::hypreal) \<in> Infinitesimal"
 apply (insert linorder_linear [of x 0]) 
 apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
 done
diff -r d5cdaa3b7517 -r 1bd84606b403 src/HOL/Hyperreal/Ln.thy
--- a/src/HOL/Hyperreal/Ln.thy	Mon May 28 04:22:44 2007 +0200
+++ b/src/HOL/Hyperreal/Ln.thy	Mon May 28 16:27:33 2007 +0200
@@ -124,7 +124,7 @@
   finally show ?thesis .
 qed
 
-lemma exp_bound: "0 <= x ==> x <= 1 ==> exp x <= 1 + x + x^2"
+lemma exp_bound: "0 <= (x::real) ==> x <= 1 ==> exp x <= 1 + x + x^2"
 proof -
   assume a: "0 <= x"
   assume b: "x <= 1"
@@ -153,7 +153,7 @@
   apply (simp add: ring_eq_simps zero_compare_simps)
 done
 
-lemma aux4: "0 <= x ==> x <= 1 ==> exp (x - x^2) <= 1 + x" 
+lemma aux4: "0 <= (x::real) ==> x <= 1 ==> exp (x - x^2) <= 1 + x" 
 proof -
   assume a: "0 <= x" and b: "x <= 1"
   have "exp (x - x^2) = exp x / exp (x^2)"
@@ -294,7 +294,7 @@
     by (rule order_trans)
 qed
 
-lemma exp_ge_add_one_self [simp]: "1 + x <= exp x"
+lemma exp_ge_add_one_self [simp]: "1 + (x::real) <= exp x"
   apply (case_tac "0 <= x")
   apply (erule exp_ge_add_one_self_aux)
   apply (case_tac "x <= -1")
@@ -415,10 +415,10 @@
   assume "exp 1 <= x" and "x <= y"
   have a: "0 < x" and b: "0 < y"
     apply (insert prems)
-    apply (subgoal_tac "0 < exp 1")
+    apply (subgoal_tac "0 < exp (1::real)")
     apply arith
     apply auto
-    apply (subgoal_tac "0 < exp 1")
+    apply (subgoal_tac "0 < exp (1::real)")
     apply arith
     apply auto
     done