src/HOL/Real/Hyperreal/HyperPow.thy
changeset 10045 c76b73e16711
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/HyperPow.thy	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,26 @@
     1.4 +(*  Title       : HyperPow.thy
     1.5 +    Author      : Jacques D. Fleuriot  
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : Powers theory for hyperreals
     1.8 +*)
     1.9 +
    1.10 +HyperPow = HRealAbs + HyperNat + RealPow +  
    1.11 +
    1.12 +instance hypreal :: {power}
    1.13 +
    1.14 +consts hpowr :: "[hypreal,nat] => hypreal"  
    1.15 +primrec
    1.16 +     hpowr_0   "r ^ 0       = 1hr"
    1.17 +     hpowr_Suc "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
    1.18 +
    1.19 +consts
    1.20 +  "pow"  :: [hypreal,hypnat] => hypreal     (infixr 80)
    1.21 +
    1.22 +defs
    1.23 +
    1.24 +  (* hypernatural powers of hyperreals *)
    1.25 +  hyperpow_def
    1.26 +  "(R::hypreal) pow (N::hypnat) 
    1.27 +      == Abs_hypreal(UN X:Rep_hypreal(R). UN Y: Rep_hypnat(N).
    1.28 +             hyprel^^{%n::nat. (X n) ^ (Y n)})"
    1.29 +end