1 <!-- $Id$ --> |
1 <!-- $Id$ --> |
2 <HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY> |
|
3 |
2 |
4 <H2>Real--Dedekind Cut Construction of the Real Line</H2> |
3 <html> |
5 |
4 |
6 <ul> |
5 <head> |
7 <LI><A HREF="PNat.html">PNat</A> The positive integers (very much the same as <A HREF="../Nat.html">Nat.thy</A>!) |
6 <meta http-equiv="content-type" content="text/html;charset=iso-8859-1"> |
8 <LI><A HREF="PRat.html">PRat</A> The positive rationals |
7 <title>HOL/Real/README</title> |
9 <LI><A HREF="PReal.html">PReal</A> The positive reals constructed using Dedekind cuts |
8 </head> |
10 <LI><A HREF="RealDef.html">RealDef</A> The real numbers |
|
11 <LI><A HREF="RealOrd.html">RealOrd</A> More real numbers theorems- ordering |
|
12 properties |
|
13 <LI><A HREF="RealInt.html">RealInt</A> Embedding of the integers in the reals |
|
14 <LI><A HREF="RealBin.html">RealBin</A> Binary arithmetic for the reals |
|
15 |
9 |
16 <LI><A HREF="Lubs.html">Lubs</A> Definition of upper bounds, lubs and so on. |
10 <body> |
17 (Useful e.g. in Fleuriot's NSA theory) |
11 <h2>Real: Dedekind Cut Construction of the Real Line</h2> |
18 <LI><A HREF="RComplete.html">RComplete</A> Proof of completeness of reals in form of the supremum |
12 <ul> |
19 property. Also proofs that the reals have the Archimedean |
13 <li><a href="Lubs.html">Lubs</a> Definition of upper bounds, lubs and so on, to support completeness proofs. |
20 property. |
14 <li><a href="PReal.html">PReal</a> The positive reals constructed using Dedekind cuts |
21 <LI><A HREF="RealAbs.html">RealAbs</A> The absolute value function defined for the reals |
|
22 </ul> |
|
23 |
15 |
24 <H2>Hyperreal--Ultrapower Construction of the Non-Standard Reals</H2> |
16 <li><a href="Rational.html">Rational</a> The rational numbers constructed as equivalence classes of integers |
|
17 |
|
18 <li><a href="RComplete.html">RComplete</a> The reals are complete: they satisfy the supremum property. They also have the Archimedean property. |
25 |
19 |
26 <p> |
20 <li><a href="RealDef.html">RealDef</a> The real numbers, their ordering properties, and embedding of the integers and the natural numbers |
27 See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real |
21 |
28 Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190. |
22 <li><a href="RealPow.html">RealPow</a> Real numbers raised to natural number powers |
29 </p> |
23 |
|
24 </ul> |
|
25 <p>Last modified on $Date$</p> |
|
26 <hr> |
|
27 <address><a name="lcp@cl.cam.ac.uk" href="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</a></address> |
|
28 </body> |
30 |
29 |
31 <UL> |
30 </html> |
32 <LI><A HREF="Zorn.html">Zorn</A> |
|
33 Zorn's Lemma: proof based on the <A HREF="../../../ZF/Zorn.html">ZF version</A> |
|
34 |
|
35 <LI><A HREF="Filter.html">Filter</A> |
|
36 Theory of Filters and Ultrafilters. |
|
37 Main result is a version of the Ultrafilter Theorem proved using |
|
38 Zorn's Lemma. |
|
39 |
|
40 <LI><A HREF="HyperDef.html">HyperDef</A> |
|
41 Ultrapower construction of the hyperreals |
|
42 |
|
43 <LI><A HREF="HyperOrd.html">HyperOrd</A> |
|
44 More hyperreal numbers theorems- ordering properties |
|
45 |
|
46 <LI><A HREF="HRealAbs.html">HRealAbs</A> The absolute value function |
|
47 defined for the hyperreals |
|
48 |
|
49 |
|
50 <LI><A HREF="NSA.html">NSA</A> |
|
51 Theory defining sets of infinite numbers, infinitesimals, |
|
52 the infinitely close relation, and their various algebraic properties. |
|
53 |
|
54 <LI><A HREF="HyperNat.html">HyperNat</A> |
|
55 Ultrapower construction of the hypernaturals |
|
56 |
|
57 <LI><A HREF="HyperPow.html">HyperPow</A> |
|
58 Powers theory for the hyperreals |
|
59 |
|
60 <LI><A HREF="Star.html">Star</A> |
|
61 Nonstandard extensions of real sets and real functions |
|
62 |
|
63 <LI><A HREF="NatStar.html">NatStar</A> |
|
64 Nonstandard extensions of sets of naturals and functions on the natural |
|
65 numbers |
|
66 |
|
67 <LI><A HREF="SEQ.html">SEQ</A> |
|
68 Theory of sequences developed using standard and nonstandard analysis |
|
69 |
|
70 <LI><A HREF="Lim.html">Lim</A> |
|
71 Theory of limits, continuous functions, and derivatives |
|
72 |
|
73 <LI><A HREF="Series.html">Series</A> |
|
74 Standard theory of finite summation and infinite series |
|
75 |
|
76 |
|
77 |
|
78 </UL> |
|
79 |
|
80 <P>Last modified on $Date$ |
|
81 |
|
82 <HR> |
|
83 |
|
84 <ADDRESS> |
|
85 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
|
86 </ADDRESS> |
|
87 </BODY></HTML> |
|