equal
deleted
inserted
replaced
18 by auto |
18 by auto |
19 |
19 |
20 |
20 |
21 definition |
21 definition |
22 powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) where |
22 powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) where |
23 [transfer_unfold, code func del]: "x powhr a = starfun2 (op powr) x a" |
23 [transfer_unfold, code del]: "x powhr a = starfun2 (op powr) x a" |
24 |
24 |
25 definition |
25 definition |
26 hlog :: "[hypreal,hypreal] => hypreal" where |
26 hlog :: "[hypreal,hypreal] => hypreal" where |
27 [transfer_unfold, code func del]: "hlog a x = starfun2 log a x" |
27 [transfer_unfold, code del]: "hlog a x = starfun2 log a x" |
28 |
28 |
29 lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))" |
29 lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))" |
30 by (simp add: powhr_def starfun2_star_n) |
30 by (simp add: powhr_def starfun2_star_n) |
31 |
31 |
32 lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1" |
32 lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1" |