src/HOL/Complex/README.html
author haftmann
Tue, 04 Oct 2005 10:58:46 +0200
changeset 17749 4fb42f4d61df
parent 15582 7219facb3fd0
permissions -rw-r--r--
removed removed IntFloor
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15283
f21466450330 DOCTYPE declaration added
webertj
parents: 14641
diff changeset
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
f21466450330 DOCTYPE declaration added
webertj
parents: 14641
diff changeset
     2
15582
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     3
<!-- $Id$ -->
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     4
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     5
<HTML>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     6
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     7
<HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     8
  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     9
  <TITLE>HOL/Complex/README</TITLE>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
    10
</HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
    11
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
    12
<BODY>
14005
5ba84fdb680b some information for Complex
paulson
parents:
diff changeset
    13
14631
ec1e67f88f49 badly-needed updates
paulson
parents: 14020
diff changeset
    14
<H1>Complex: The Complex Numbers</H1>
ec1e67f88f49 badly-needed updates
paulson
parents: 14020
diff changeset
    15
		<P>This directory defines the type <KBD>complex</KBD> of the complex numbers,
14005
5ba84fdb680b some information for Complex
paulson
parents:
diff changeset
    16
with numeric constants and some complex analysis.  The development includes
5ba84fdb680b some information for Complex
paulson
parents:
diff changeset
    17
nonstandard analysis for the complex numbers.  Note that the image
14020
paulson
parents: 14005
diff changeset
    18
<KBD>HOL-Complex</KBD> includes theories from the directories 
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    19
<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).
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    20
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    21
<ul>
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    22
<li><a href="CLim.html">CLim</a> Limits, continuous functions, and derivatives for the complex numbers
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    23
<li><a href="CSeries.html">CSeries</a> Finite summation and infinite series for the complex numbers
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    24
<li><a href="CStar.html">CStar</a> Star-transforms for the complex numbers, to form non-standard extensions of sets and functions
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    25
<li><a href="Complex.html">Complex</a> The complex numbers
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    26
<li><a href="NSCA.html">NSCA</a> Nonstandard complex analysis
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    27
<li><a href="NSComplex.html">NSComplex</a> Ultrapower construction of the nonstandard complex numbers
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    28
</ul>
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    29
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    30
<h2><a name="Anchor-Real" id="Anchor-Real"></a>Real: Dedekind Cut Construction of the Real Line</h2>
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    31
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    32
<ul>
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    33
<li><a href="Lubs.html">Lubs</a> Definition of upper bounds, lubs and so on, to support completeness proofs.
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    34
<li><a href="PReal.html">PReal</a> The positive reals constructed using Dedekind cuts
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    35
<li><a href="Rational.html">Rational</a> The rational numbers constructed as equivalence classes of integers
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    36
<li><a href="RComplete.html">RComplete</a> The reals are complete: they satisfy the supremum property. They also have the Archimedean property.
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    37
<li><a href="RealDef.html">RealDef</a> The real numbers, their ordering properties, and embedding of the integers and the natural numbers
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    38
<li><a href="RealPow.html">RealPow</a> Real numbers raised to natural number powers
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    39
</ul>
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    40
<h2><a name="Anchor-Hyperreal" id="Anchor-Hyperreal"></a>Hyperreal: Ultrafilter Construction of the Non-Standard Reals</h2>
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    41
See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    42
<ul>
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    43
<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.
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    44
<li><a href="HLog.html">HLog</a> Non-standard logarithms
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    45
<li><a href="HSeries.html">HSeries</a> Non-standard theory of finite summation and infinite series
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    46
<li><a href="HTranscendental.html">HTranscendental</a> Non-standard extensions of transcendental functions
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    47
<li><a href="HyperDef.html">HyperDef</a> Ultrapower construction of the hyperreals
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    48
<li><a href="HyperNat.html">HyperNat</a> Ultrapower construction of the hypernaturals
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    49
<li><a href="HyperPow.html">HyperPow</a> Powers theory for the hyperreals
17749
4fb42f4d61df removed removed IntFloor
haftmann
parents: 15582
diff changeset
    50
<!-- <li><a href="IntFloor.html">IntFloor</a> Floor and Ceiling functions relating the reals and integers -->
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    51
<li><a href="Integration.html">Integration</a> Gage integrals
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    52
<li><a href="Lim.html">Lim</a> Theory of limits, continuous functions, and derivatives
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    53
<li><a href="Log.html">Log</a> Logarithms for the reals
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    54
<li><a href="MacLaurin.html">MacLaurin</a> MacLaurin series
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    55
<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
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    56
<li><a href="NthRoot.html">NthRoot</a> Existence of n-th roots of real numbers
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    57
<li><a href="NSA.html">NSA</a> Theory defining sets of infinite numbers, infinitesimals, the infinitely close relation, and their various algebraic properties.
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    58
<li><a href="Poly.html">Poly</a> Univariate real polynomials
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    59
<li><a href="SEQ.html">SEQ</a> Convergence of sequences and series using standard and nonstandard analysis
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    60
<li><a href="Series.html">Series</a> Finite summation and infinite series for the reals
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    61
<li><a href="Star.html">Star</a> Nonstandard extensions of real sets and real functions
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    62
<li><a href="Transcendental.html">Transcendental</a> Power series and transcendental functions
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    63
</ul>
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    64
<HR>
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14634
diff changeset
    65
<P>Last modified $Date$
15582
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
    66
</BODY>
14005
5ba84fdb680b some information for Complex
paulson
parents:
diff changeset
    67
</HTML>