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