| author | wenzelm |
| Sat, 18 Mar 2000 19:10:02 +0100 | |
| changeset 8516 | f5f6a97ee43f |
| parent 7825 | 1be9b63e7d93 |
| child 12018 | ec054019c910 |
| permissions | -rw-r--r-- |
| 7219 | 1 |
(* Title : PReal.thy |
2 |
ID : $Id$ |
|
| 5078 | 3 |
Author : Jacques D. Fleuriot |
4 |
Copyright : 1998 University of Cambridge |
|
5 |
Description : The positive reals as Dedekind sections of positive |
|
6 |
rationals. Fundamentals of Abstract Analysis [Gleason- p. 121] |
|
7 |
provides some of the definitions. |
|
8 |
*) |
|
9 |
||
10 |
PReal = PRat + |
|
11 |
||
|
7825
1be9b63e7d93
replaced {x. True} by UNIV to work with the new simprule, Collect_const
paulson
parents:
7219
diff
changeset
|
12 |
typedef preal = "{A::prat set. {} < A & A < UNIV &
|
| 5078 | 13 |
(!y: A. ((!z. z < y --> z: A) & |
14 |
(? u: A. y < u)))}" (preal_1) |
|
15 |
instance |
|
16 |
preal :: {ord, plus, times}
|
|
17 |
||
18 |
constdefs |
|
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5078
diff
changeset
|
19 |
preal_of_prat :: prat => preal |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5078
diff
changeset
|
20 |
"preal_of_prat q == Abs_preal({x::prat. x < q})"
|
| 5078 | 21 |
|
22 |
pinv :: preal => preal |
|
23 |
"pinv(R) == Abs_preal({w. ? y. w < y & qinv y ~: Rep_preal(R)})"
|
|
24 |
||
25 |
psup :: preal set => preal |
|
26 |
"psup(P) == Abs_preal({w. ? X: P. w: Rep_preal(X)})"
|
|
27 |
||
28 |
defs |
|
29 |
||
30 |
preal_add_def |
|
31 |
"R + S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x + y})"
|
|
32 |
||
33 |
preal_mult_def |
|
34 |
"R * S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x * y})"
|
|
35 |
||
36 |
preal_less_def |
|
37 |
"R < (S::preal) == Rep_preal(R) < Rep_preal(S)" |
|
38 |
||
39 |
preal_le_def |
|
40 |
"R <= (S::preal) == Rep_preal(R) <= Rep_preal(S)" |
|
41 |
||
42 |
end |
|
43 |