equal
deleted
inserted
replaced
18 lemma hpowr_Suc [simp]: "r ^ (Suc n) = (r::hypreal) * (r ^ n)" |
18 lemma hpowr_Suc [simp]: "r ^ (Suc n) = (r::hypreal) * (r ^ n)" |
19 by (rule power_Suc) |
19 by (rule power_Suc) |
20 |
20 |
21 definition |
21 definition |
22 (* hypernatural powers of hyperreals *) |
22 (* hypernatural powers of hyperreals *) |
23 pow :: "[hypreal,hypnat] => hypreal" (infixr "pow" 80) |
23 pow :: "[hypreal,hypnat] => hypreal" (infixr "pow" 80) where |
24 hyperpow_def [transfer_unfold]: |
24 hyperpow_def [transfer_unfold]: |
25 "(R::hypreal) pow (N::hypnat) = ( *f2* op ^) R N" |
25 "(R::hypreal) pow (N::hypnat) = ( *f2* op ^) R N" |
26 |
26 |
27 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r" |
27 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r" |
28 by simp |
28 by simp |