src/HOL/Complex/README.html
author paulson
Thu Jul 01 12:29:53 2004 +0200 (2004-07-01)
changeset 15013 34264f5e4691
parent 14641 79b7bd936264
child 15283 f21466450330
permissions -rw-r--r--
new treatment of binary numerals
paulson@14631
     1
<HTML><HEAD><TITLE>HOL/Complex/README</TITLE>
paulson@14631
     2
		<meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
paulson@14631
     3
	</HEAD><BODY>
paulson@14005
     4
paulson@14631
     5
<H1>Complex: The Complex Numbers</H1>
paulson@14631
     6
		<P>This directory defines the type <KBD>complex</KBD> of the complex numbers,
paulson@14005
     7
with numeric constants and some complex analysis.  The development includes
paulson@14005
     8
nonstandard analysis for the complex numbers.  Note that the image
paulson@14020
     9
<KBD>HOL-Complex</KBD> includes theories from the directories 
paulson@14641
    10
<KBD><a href="#Anchor-Real">HOL/Real</a></KBD>  and <KBD><a href="#Anchor-Hyperreal">HOL/Hyperreal</a></KBD>. They define other types including <kbd>real</kbd> (the real numbers) and <kbd>hypreal</kbd> (the hyperreal or non-standard reals).
paulson@14641
    11
paulson@14641
    12
<ul>
paulson@14641
    13
<li><a href="CLim.html">CLim</a> Limits, continuous functions, and derivatives for the complex numbers
paulson@14641
    14
<li><a href="CSeries.html">CSeries</a> Finite summation and infinite series for the complex numbers
paulson@14641
    15
<li><a href="CStar.html">CStar</a> Star-transforms for the complex numbers, to form non-standard extensions of sets and functions
paulson@14641
    16
<li><a href="Complex.html">Complex</a> The complex numbers
paulson@14641
    17
<li><a href="NSCA.html">NSCA</a> Nonstandard complex analysis
paulson@14641
    18
<li><a href="NSComplex.html">NSComplex</a> Ultrapower construction of the nonstandard complex numbers
paulson@14641
    19
</ul>
paulson@14641
    20
paulson@14641
    21
<h2><a name="Anchor-Real" id="Anchor-Real"></a>Real: Dedekind Cut Construction of the Real Line</h2>
paulson@14641
    22
paulson@14641
    23
<ul>
paulson@14641
    24
<li><a href="Lubs.html">Lubs</a> Definition of upper bounds, lubs and so on, to support completeness proofs.
paulson@14641
    25
<li><a href="PReal.html">PReal</a> The positive reals constructed using Dedekind cuts
paulson@14641
    26
<li><a href="Rational.html">Rational</a> The rational numbers constructed as equivalence classes of integers
paulson@14641
    27
<li><a href="RComplete.html">RComplete</a> The reals are complete: they satisfy the supremum property. They also have the Archimedean property.
paulson@14641
    28
<li><a href="RealDef.html">RealDef</a> The real numbers, their ordering properties, and embedding of the integers and the natural numbers
paulson@14641
    29
<li><a href="RealPow.html">RealPow</a> Real numbers raised to natural number powers
paulson@14641
    30
</ul>
paulson@14641
    31
<h2><a name="Anchor-Hyperreal" id="Anchor-Hyperreal"></a>Hyperreal: Ultrafilter Construction of the Non-Standard Reals</h2>
paulson@14641
    32
See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
paulson@14641
    33
<ul>
paulson@14641
    34
<li><a href="Filter.html">Filter</a> Theory of Filters and Ultrafilters. Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma.
paulson@14641
    35
<li><a href="HLog.html">HLog</a> Non-standard logarithms
paulson@14641
    36
<li><a href="HSeries.html">HSeries</a> Non-standard theory of finite summation and infinite series
paulson@14641
    37
<li><a href="HTranscendental.html">HTranscendental</a> Non-standard extensions of transcendental functions
paulson@14641
    38
<li><a href="HyperDef.html">HyperDef</a> Ultrapower construction of the hyperreals
paulson@14641
    39
<li><a href="HyperNat.html">HyperNat</a> Ultrapower construction of the hypernaturals
paulson@14641
    40
<li><a href="HyperPow.html">HyperPow</a> Powers theory for the hyperreals
paulson@14641
    41
<li><a href="IntFloor.html">IntFloor</a> Floor and Ceiling functions relating the reals and integers
paulson@14641
    42
<li><a href="Integration.html">Integration</a> Gage integrals
paulson@14641
    43
<li><a href="Lim.html">Lim</a> Theory of limits, continuous functions, and derivatives
paulson@14641
    44
<li><a href="Log.html">Log</a> Logarithms for the reals
paulson@14641
    45
<li><a href="MacLaurin.html">MacLaurin</a> MacLaurin series
paulson@14641
    46
<li><a href="NatStar.html">NatStar</a> Star-transforms for the hypernaturals, to form non-standard extensions of sets and functions involving the naturals or reals
paulson@14641
    47
<li><a href="NthRoot.html">NthRoot</a> Existence of n-th roots of real numbers
paulson@14641
    48
<li><a href="NSA.html">NSA</a> Theory defining sets of infinite numbers, infinitesimals, the infinitely close relation, and their various algebraic properties.
paulson@14641
    49
<li><a href="Poly.html">Poly</a> Univariate real polynomials
paulson@14641
    50
<li><a href="SEQ.html">SEQ</a> Convergence of sequences and series using standard and nonstandard analysis
paulson@14641
    51
<li><a href="Series.html">Series</a> Finite summation and infinite series for the reals
paulson@14641
    52
<li><a href="Star.html">Star</a> Nonstandard extensions of real sets and real functions
paulson@14641
    53
<li><a href="Transcendental.html">Transcendental</a> Power series and transcendental functions
paulson@14641
    54
</ul>
paulson@14641
    55
<HR>
paulson@14641
    56
<P>Last modified $Date$
paulson@14005
    57
paulson@14005
    58
</HTML>