1(*  Title:      HOL/Nonstandard_Analysis/HLog.thy
2    Author:     Jacques D. Fleuriot
3    Copyright:  2000, 2001 University of Edinburgh
4*)
5
6section \<open>Logarithms: Non-Standard Version\<close>
7
8theory HLog
9  imports HTranscendental
10begin
11
12definition powhr :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"  (infixr "powhr" 80)
13  where [transfer_unfold]: "x powhr a = starfun2 (powr) x a"
14
15definition hlog :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"
16  where [transfer_unfold]: "hlog a x = starfun2 log a x"
17
18lemma powhr: "(star_n X) powhr (star_n Y) = star_n (\<lambda>n. (X n) powr (Y n))"
19  by (simp add: powhr_def starfun2_star_n)
20
21lemma powhr_one_eq_one [simp]: "\<And>a. 1 powhr a = 1"
22  by transfer simp
23
24lemma powhr_mult: "\<And>a x y. 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powhr a = (x powhr a) * (y powhr a)"
25  by transfer (simp add: powr_mult)
26
27lemma powhr_gt_zero [simp]: "\<And>a x. 0 < x powhr a \<longleftrightarrow> x \<noteq> 0"
28  by transfer simp
29
30lemma powhr_not_zero [simp]: "\<And>a x. x powhr a \<noteq> 0 \<longleftrightarrow> x \<noteq> 0"
31  by transfer simp
32
33lemma powhr_divide: "\<And>a x y. 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> (x / y) powhr a = (x powhr a) / (y powhr a)"
34  by transfer (rule powr_divide)
35
36lemma powhr_add: "\<And>a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
37  by transfer (rule powr_add)
38
39lemma powhr_powhr: "\<And>a b x. (x powhr a) powhr b = x powhr (a * b)"
40  by transfer (rule powr_powr)
41
42lemma powhr_powhr_swap: "\<And>a b x. (x powhr a) powhr b = (x powhr b) powhr a"
43  by transfer (rule powr_powr_swap)
44
45lemma powhr_minus: "\<And>a x. x powhr (- a) = inverse (x powhr a)"
46  by transfer (rule powr_minus)
47
48lemma powhr_minus_divide: "x powhr (- a) = 1 / (x powhr a)"
49  by (simp add: divide_inverse powhr_minus)
50
51lemma powhr_less_mono: "\<And>a b x. a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powhr a < x powhr b"
52  by transfer simp
53
54lemma powhr_less_cancel: "\<And>a b x. x powhr a < x powhr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
55  by transfer simp
56
57lemma powhr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> x powhr a < x powhr b \<longleftrightarrow> a < b"
58  by (blast intro: powhr_less_cancel powhr_less_mono)
59
60lemma powhr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> x powhr a \<le> x powhr b \<longleftrightarrow> a \<le> b"
61  by (simp add: linorder_not_less [symmetric])
62
63lemma hlog: "hlog (star_n X) (star_n Y) = star_n (\<lambda>n. log (X n) (Y n))"
64  by (simp add: hlog_def starfun2_star_n)
65
66lemma hlog_starfun_ln: "\<And>x. ( *f* ln) x = hlog (( *f* exp) 1) x"
67  by transfer (rule log_ln)
68
69lemma powhr_hlog_cancel [simp]: "\<And>a x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powhr (hlog a x) = x"
70  by transfer simp
71
72lemma hlog_powhr_cancel [simp]: "\<And>a y. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a (a powhr y) = y"
73  by transfer simp
74
75lemma hlog_mult:
76  "\<And>a x y. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a (x * y) = hlog a x + hlog a y"
77  by transfer (rule log_mult)
78
79lemma hlog_as_starfun: "\<And>a x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a x = ( *f* ln) x / ( *f* ln) a"
80  by transfer (simp add: log_def)
81
82lemma hlog_eq_div_starfun_ln_mult_hlog:
83  "\<And>a b x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow>
84    hlog a x = (( *f* ln) b / ( *f* ln) a) * hlog b x"
85  by transfer (rule log_eq_div_ln_mult_log)
86
87lemma powhr_as_starfun: "\<And>a x. x powhr a = (if x = 0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
88  by transfer (simp add: powr_def)
89
90lemma HInfinite_powhr:
91  "x \<in> HInfinite \<Longrightarrow> 0 < x \<Longrightarrow> a \<in> HFinite - Infinitesimal \<Longrightarrow> 0 < a \<Longrightarrow> x powhr a \<in> HInfinite"
92  by (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite
93        HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite
94      simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
95
96lemma hlog_hrabs_HInfinite_Infinitesimal:
97  "x \<in> HFinite - Infinitesimal \<Longrightarrow> a \<in> HInfinite \<Longrightarrow> 0 < a \<Longrightarrow> hlog a \<bar>x\<bar> \<in> Infinitesimal"
98  apply (frule HInfinite_gt_zero_gt_one)
99   apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
100      HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2
101      simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero
102      hlog_as_starfun divide_inverse)
103  done
104
105lemma hlog_HInfinite_as_starfun: "a \<in> HInfinite \<Longrightarrow> 0 < a \<Longrightarrow> hlog a x = ( *f* ln) x / ( *f* ln) a"
106  by (rule hlog_as_starfun) auto
107
108lemma hlog_one [simp]: "\<And>a. hlog a 1 = 0"
109  by transfer simp
110
111lemma hlog_eq_one [simp]: "\<And>a. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a a = 1"
112  by transfer (rule log_eq_one)
113
114lemma hlog_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> hlog a (inverse x) = - hlog a x"
115  by (rule add_left_cancel [of "hlog a x", THEN iffD1]) (simp add: hlog_mult [symmetric])
116
117lemma hlog_divide: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a (x / y) = hlog a x - hlog a y"
118  by (simp add: hlog_mult hlog_inverse divide_inverse)
119
120lemma hlog_less_cancel_iff [simp]:
121  "\<And>a x y. 1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a x < hlog a y \<longleftrightarrow> x < y"
122  by transfer simp
123
124lemma hlog_le_cancel_iff [simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a x \<le> hlog a y \<longleftrightarrow> x \<le> y"
125  by (simp add: linorder_not_less [symmetric])
126
127end
128