src/HOL/NumberTheory/document/root.tex
author wenzelm
Wed, 17 May 2006 01:23:44 +0200
changeset 19672 9be07d531694
parent 17159 d5060118122e
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11060
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
     1
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
     2
\documentclass[11pt,a4paper]{article}
11855
bdae1f29f35d include document graph;
wenzelm
parents: 11060
diff changeset
     3
\usepackage{graphicx}
11060
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
     4
\usepackage{isabelle,isabellesym,pdfsetup}
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
     5
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
     6
\urlstyle{rm}
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
     7
\isabellestyle{it}
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
     8
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
     9
\begin{document}
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
    10
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
    11
\title{Some results of number theory}
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    12
\author{Jeremy Avigad\\
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    13
    David Gray\\
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    14
    Adam Kramer\\
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    15
    Thomas M Rasmussen}
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    16
11060
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
    17
\maketitle
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
    18
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    19
\begin{abstract}
19672
wenzelm
parents: 17159
diff changeset
    20
This is a collection of formalized proofs of many results of number theory.
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    21
The proofs of the Chinese Remainder Theorem and Wilson's Theorem are due to
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    22
Rasmussen.  The proof of Gauss's law of quadratic reciprocity is due to
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    23
Avigad, Gray and Kramer.  Proofs can be found in most introductory number
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    24
theory textbooks; Goldman's \emph{The Queen of Mathematics: a Historically
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    25
Motivated Guide to Number Theory} provides some historical context.
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    26
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    27
Avigad, Gray and Kramer have also provided library theories dealing with
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    28
finite sets and finite sums, divisibility and congruences, parity and
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    29
residues.  The authors are engaged in redesigning and polishing these theories
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    30
for more serious use.  For the latest information in this respect, please see
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    31
the web page \url{http://www.andrew.cmu.edu/~avigad/isabelle}.  Other theories
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    32
contain proofs of Euler's criteria, Gauss' lemma, and the law of quadratic
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    33
reciprocity.  The formalization follows Eisenstein's proof, which is the one
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    34
most commonly found in introductory textbooks; in particular, it follows the
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    35
presentation in Niven and Zuckerman, \emph{The Theory of Numbers}.
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    36
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    37
To avoid having to count roots of polynomials, however, we relied on a trick
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    38
previously used by David Russinoff in formalizing quadratic reciprocity for
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    39
the Boyer-Moore theorem prover; see Russinoff, David, ``A mechanical proof
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    40
of quadratic reciprocity,'' \emph{Journal of Automated Reasoning} 8:3-21,
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    41
1992.  We are grateful to Larry Paulson for calling our attention to this
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    42
reference.
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    43
\end{abstract}
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents: 11855
diff changeset
    44
11060
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
    45
\tableofcontents
11855
bdae1f29f35d include document graph;
wenzelm
parents: 11060
diff changeset
    46
bdae1f29f35d include document graph;
wenzelm
parents: 11060
diff changeset
    47
\begin{center}
17159
d5060118122e tuned size of included graph;
wenzelm
parents: 13871
diff changeset
    48
  \includegraphics[scale=0.5]{session_graph}  
11855
bdae1f29f35d include document graph;
wenzelm
parents: 11060
diff changeset
    49
\end{center}
bdae1f29f35d include document graph;
wenzelm
parents: 11060
diff changeset
    50
11060
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
    51
\newpage
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
    52
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
    53
\parindent 0pt\parskip 0.5ex
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
    54
\input{session}
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
    55
a58e0bd448df document setup;
wenzelm
parents:
diff changeset
    56
\end{document}