| author | wenzelm |
| Fri, 01 Dec 2000 19:42:35 +0100 | |
| changeset 10568 | a7701b1d6c6a |
| parent 10045 | c76b73e16711 |
| permissions | -rw-r--r-- |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
1 |
(* Title : HyperPow.thy |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
2 |
Author : Jacques D. Fleuriot |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
3 |
Copyright : 1998 University of Cambridge |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
4 |
Description : Powers theory for hyperreals |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
5 |
*) |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
6 |
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
7 |
HyperPow = HRealAbs + HyperNat + RealPow + |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
8 |
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
9 |
instance hypreal :: {power}
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
10 |
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
11 |
consts hpowr :: "[hypreal,nat] => hypreal" |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
12 |
primrec |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
13 |
hpowr_0 "r ^ 0 = 1hr" |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
14 |
hpowr_Suc "r ^ (Suc n) = (r::hypreal) * (r ^ n)" |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
15 |
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
16 |
consts |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
17 |
"pow" :: [hypreal,hypnat] => hypreal (infixr 80) |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
18 |
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
19 |
defs |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
20 |
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
21 |
(* hypernatural powers of hyperreals *) |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
22 |
hyperpow_def |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
23 |
"(R::hypreal) pow (N::hypnat) |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
24 |
== Abs_hypreal(UN X:Rep_hypreal(R). UN Y: Rep_hypnat(N). |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
25 |
hyprel^^{%n::nat. (X n) ^ (Y n)})"
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
26 |
end |