--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nonstandard_Analysis/HLog.thy Mon Feb 29 22:34:36 2016 +0100
@@ -0,0 +1,156 @@
+(* Title: HOL/Nonstandard_Analysis/HLog.thy
+ Author: Jacques D. Fleuriot
+ Copyright: 2000, 2001 University of Edinburgh
+*)
+
+section\<open>Logarithms: Non-Standard Version\<close>
+
+theory HLog
+imports HTranscendental
+begin
+
+
+(* should be in NSA.ML *)
+lemma epsilon_ge_zero [simp]: "0 \<le> \<epsilon>"
+by (simp add: epsilon_def star_n_zero_num star_n_le)
+
+lemma hpfinite_witness: "\<epsilon> : {x. 0 \<le> x & x : HFinite}"
+by auto
+
+
+definition
+ powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) where
+ [transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
+
+definition
+ hlog :: "[hypreal,hypreal] => hypreal" where
+ [transfer_unfold]: "hlog a x = starfun2 log a x"
+
+lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
+by (simp add: powhr_def starfun2_star_n)
+
+lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1"
+by (transfer, simp)
+
+lemma powhr_mult:
+ "!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
+by (transfer, simp add: powr_mult)
+
+lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a \<longleftrightarrow> x \<noteq> 0"
+by (transfer, simp)
+
+lemma powhr_not_zero [simp]: "\<And>a x. x powhr a \<noteq> 0 \<longleftrightarrow> x \<noteq> 0"
+by transfer simp
+
+lemma powhr_divide:
+ "!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
+by (transfer, rule powr_divide)
+
+lemma powhr_add: "!!a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
+by (transfer, rule powr_add)
+
+lemma powhr_powhr: "!!a b x. (x powhr a) powhr b = x powhr (a * b)"
+by (transfer, rule powr_powr)
+
+lemma powhr_powhr_swap: "!!a b x. (x powhr a) powhr b = (x powhr b) powhr a"
+by (transfer, rule powr_powr_swap)
+
+lemma powhr_minus: "!!a x. x powhr (-a) = inverse (x powhr a)"
+by (transfer, rule powr_minus)
+
+lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
+by (simp add: divide_inverse powhr_minus)
+
+lemma powhr_less_mono: "!!a b x. [| a < b; 1 < x |] ==> x powhr a < x powhr b"
+by (transfer, simp)
+
+lemma powhr_less_cancel: "!!a b x. [| x powhr a < x powhr b; 1 < x |] ==> a < b"
+by (transfer, simp)
+
+lemma powhr_less_cancel_iff [simp]:
+ "1 < x ==> (x powhr a < x powhr b) = (a < b)"
+by (blast intro: powhr_less_cancel powhr_less_mono)
+
+lemma powhr_le_cancel_iff [simp]:
+ "1 < x ==> (x powhr a \<le> x powhr b) = (a \<le> b)"
+by (simp add: linorder_not_less [symmetric])
+
+lemma hlog:
+ "hlog (star_n X) (star_n Y) =
+ star_n (%n. log (X n) (Y n))"
+by (simp add: hlog_def starfun2_star_n)
+
+lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x"
+by (transfer, rule log_ln)
+
+lemma powhr_hlog_cancel [simp]:
+ "!!a x. [| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
+by (transfer, simp)
+
+lemma hlog_powhr_cancel [simp]:
+ "!!a y. [| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
+by (transfer, simp)
+
+lemma hlog_mult:
+ "!!a x y. [| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]
+ ==> hlog a (x * y) = hlog a x + hlog a y"
+by (transfer, rule log_mult)
+
+lemma hlog_as_starfun:
+ "!!a x. [| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
+by (transfer, simp add: log_def)
+
+lemma hlog_eq_div_starfun_ln_mult_hlog:
+ "!!a b x. [| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]
+ ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
+by (transfer, rule log_eq_div_ln_mult_log)
+
+lemma powhr_as_starfun: "!!a x. x powhr a = (if x=0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
+ by (transfer, simp add: powr_def)
+
+lemma HInfinite_powhr:
+ "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;
+ 0 < a |] ==> x powhr a : HInfinite"
+apply (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite
+ simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
+done
+
+lemma hlog_hrabs_HInfinite_Infinitesimal:
+ "[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |]
+ ==> hlog a \<bar>x\<bar> : Infinitesimal"
+apply (frule HInfinite_gt_zero_gt_one)
+apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
+ HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2
+ simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero
+ hlog_as_starfun divide_inverse)
+done
+
+lemma hlog_HInfinite_as_starfun:
+ "[| a : HInfinite; 0 < a |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
+by (rule hlog_as_starfun, auto)
+
+lemma hlog_one [simp]: "!!a. hlog a 1 = 0"
+by (transfer, simp)
+
+lemma hlog_eq_one [simp]: "!!a. [| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
+by (transfer, rule log_eq_one)
+
+lemma hlog_inverse:
+ "[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"
+apply (rule add_left_cancel [of "hlog a x", THEN iffD1])
+apply (simp add: hlog_mult [symmetric])
+done
+
+lemma hlog_divide:
+ "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y"
+by (simp add: hlog_mult hlog_inverse divide_inverse)
+
+lemma hlog_less_cancel_iff [simp]:
+ "!!a x y. [| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
+by (transfer, simp)
+
+lemma hlog_le_cancel_iff [simp]:
+ "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
+by (simp add: linorder_not_less [symmetric])
+
+end