8 |
8 |
9 theory Log |
9 theory Log |
10 imports Transcendental |
10 imports Transcendental |
11 begin |
11 begin |
12 |
12 |
13 constdefs |
13 definition |
14 |
|
15 powr :: "[real,real] => real" (infixr "powr" 80) |
14 powr :: "[real,real] => real" (infixr "powr" 80) |
16 --{*exponentation with real exponent*} |
15 --{*exponentation with real exponent*} |
17 "x powr a == exp(a * ln x)" |
16 "x powr a = exp(a * ln x)" |
18 |
17 |
19 log :: "[real,real] => real" |
18 log :: "[real,real] => real" |
20 --{*logarithm of @{term x} to base @{term a}*} |
19 --{*logarithm of @{term x} to base @{term a}*} |
21 "log a x == ln x / ln a" |
20 "log a x = ln x / ln a" |
22 |
21 |
23 |
22 |
24 |
23 |
25 lemma powr_one_eq_one [simp]: "1 powr a = 1" |
24 lemma powr_one_eq_one [simp]: "1 powr a = 1" |
26 by (simp add: powr_def) |
25 by (simp add: powr_def) |
271 also have "... = r" |
270 also have "... = r" |
272 by (simp add: powr_powr prems less_imp_neq [THEN not_sym]) |
271 by (simp add: powr_powr prems less_imp_neq [THEN not_sym]) |
273 finally show "real n powr - s < r" . |
272 finally show "real n powr - s < r" . |
274 qed |
273 qed |
275 |
274 |
276 |
|
277 |
|
278 ML |
|
279 {* |
|
280 val powr_one_eq_one = thm "powr_one_eq_one"; |
|
281 val powr_zero_eq_one = thm "powr_zero_eq_one"; |
|
282 val powr_one_gt_zero_iff = thm "powr_one_gt_zero_iff"; |
|
283 val powr_mult = thm "powr_mult"; |
|
284 val powr_gt_zero = thm "powr_gt_zero"; |
|
285 val powr_not_zero = thm "powr_not_zero"; |
|
286 val powr_divide = thm "powr_divide"; |
|
287 val powr_add = thm "powr_add"; |
|
288 val powr_powr = thm "powr_powr"; |
|
289 val powr_powr_swap = thm "powr_powr_swap"; |
|
290 val powr_minus = thm "powr_minus"; |
|
291 val powr_minus_divide = thm "powr_minus_divide"; |
|
292 val powr_less_mono = thm "powr_less_mono"; |
|
293 val powr_less_cancel = thm "powr_less_cancel"; |
|
294 val powr_less_cancel_iff = thm "powr_less_cancel_iff"; |
|
295 val powr_le_cancel_iff = thm "powr_le_cancel_iff"; |
|
296 val log_ln = thm "log_ln"; |
|
297 val powr_log_cancel = thm "powr_log_cancel"; |
|
298 val log_powr_cancel = thm "log_powr_cancel"; |
|
299 val log_mult = thm "log_mult"; |
|
300 val log_eq_div_ln_mult_log = thm "log_eq_div_ln_mult_log"; |
|
301 val log_base_10_eq1 = thm "log_base_10_eq1"; |
|
302 val log_base_10_eq2 = thm "log_base_10_eq2"; |
|
303 val log_one = thm "log_one"; |
|
304 val log_eq_one = thm "log_eq_one"; |
|
305 val log_inverse = thm "log_inverse"; |
|
306 val log_divide = thm "log_divide"; |
|
307 val log_less_cancel_iff = thm "log_less_cancel_iff"; |
|
308 val log_le_cancel_iff = thm "log_le_cancel_iff"; |
|
309 *} |
|
310 |
|
311 end |
275 end |