author | paulson |
Fri, 02 Nov 2001 17:55:24 +0100 | |
changeset 12018 | ec054019c910 |
parent 7825 | 1be9b63e7d93 |
child 14335 | 9c0b5e081037 |
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 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
7825
diff
changeset
|
31 |
"R + S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x + y})" |
5078 | 32 |
|
33 |
preal_mult_def |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
7825
diff
changeset
|
34 |
"R * S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x * y})" |
5078 | 35 |
|
36 |
preal_less_def |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
7825
diff
changeset
|
37 |
"R < (S::preal) == Rep_preal(R) < Rep_preal(S)" |
5078 | 38 |
|
39 |
preal_le_def |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
7825
diff
changeset
|
40 |
"R <= (S::preal) == Rep_preal(R) <= Rep_preal(S)" |
5078 | 41 |
|
42 |
end |
|
43 |