# 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 \ Infinitesimal ==> ( *f* exp) x @= 1" +lemma STAR_exp_Infinitesimal: "x \ 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 \ x ==> (1 + x) \ ( *f* exp) x" +lemma starfun_exp_ge_add_one_self [simp]: "!!x::hypreal. 0 \ x ==> (1 + x) \ ( *f* exp) x" by transfer (rule exp_ge_add_one_self_aux) (* exp (oo) is infinite *) lemma starfun_exp_HInfinite: - "[| x \ HInfinite; 0 \ x |] ==> ( *f* exp) x \ HInfinite" + "[| x \ HInfinite; 0 \ x |] ==> ( *f* exp) (x::hypreal) \ 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 \ HInfinite; x \ 0 |] ==> ( *f* exp) x \ Infinitesimal" + "[| x \ HInfinite; x \ 0 |] ==> ( *f* exp) (x::hypreal) \ Infinitesimal" apply (subgoal_tac "\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: "\x. \( *f* exp) x\ = ( *f* exp) x" +lemma starfun_abs_exp_cancel: "\x. \( *f* exp) (x::hypreal)\ = ( *f* exp) x" by transfer (rule abs_exp_cancel) -lemma starfun_exp_less_mono: "\x y. x < y \ ( *f* exp) x < ( *f* exp) y" +lemma starfun_exp_less_mono: "\x y::hypreal. x < y \ ( *f* exp) x < ( *f* exp) y" by transfer (rule exp_less_mono) -lemma starfun_exp_HFinite: "x \ HFinite ==> ( *f* exp) x \ HFinite" +lemma starfun_exp_HFinite: "x \ HFinite ==> ( *f* exp) (x::hypreal) \ 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 \ Infinitesimal; z \ HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z" + "[|x \ Infinitesimal; z \ 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 \ HInfinite ==> ( *f* exp) x \ HInfinite | ( *f* exp) x \ Infinitesimal" + "x \ HInfinite ==> ( *f* exp) x \ HInfinite | ( *f* exp) (x::hypreal) \ 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