(*  Title       : HyperPow.thy
    Author      : Jacques D. Fleuriot  
    Copyright   : 1998  University of Cambridge
    Description : Powers theory for hyperreals
*)

HyperPow = HRealAbs + HyperNat + RealPow + (* ExtraThms + *) 

instance hypreal :: {power}

consts hpowr :: "[hypreal,nat] => hypreal"  
primrec
     hpowr_0   "r ^ 0       = 1hr"
     hpowr_Suc "r ^ (Suc n) = (r::hypreal) * (r ^ n)"

consts
  "pow"  :: [hypreal,hypnat] => hypreal     (infixr 80)

defs

  (* hypernatural powers of hyperreals *)
  hyperpow_def
  "(R::hypreal) pow (N::hypnat) 
      == Abs_hypreal(UN X:Rep_hypreal(R). UN Y: Rep_hypnat(N).
             hyprel^^{%n::nat. (X n) ^ (Y n)})"
end