doc-src/Intro/intro.tex
author paulson
Tue, 10 Feb 2004 12:02:11 +0100
changeset 14378 69c4d5997669
parent 14148 6580d374a509
child 30118 df610709eda5
permissions -rw-r--r--
generic of_nat and of_int functions, and generalization of iszero and neg
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7827
c9c615d970db a4paper;
wenzelm
parents: 6611
diff changeset
     1
\documentclass[12pt,a4paper]{article}
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 8979
diff changeset
     2
\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../pdfsetup}
2656
71097a167f0b made a bit more robust;
wenzelm
parents: 1878
diff changeset
     3
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     4
%% $Id$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     5
%% run    bibtex intro         to prepare bibliography
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     6
%% run    ../sedindex intro    to prepare index file
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     7
%prth *(\(.*\));          \1;      
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     8
%{\\out \(.*\)}          {\\out val it = "\1" : thm}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     9
6611
08dfd050b373 pdf setup;
wenzelm
parents: 6592
diff changeset
    10
\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Introduction to Isabelle}   
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    11
\author{{\em Lawrence C. Paulson}\\
3127
4cc2fe62f7c3 New acknowledgements; no Fast_tac
paulson
parents: 3096
diff changeset
    12
        Computer Laboratory \\ University of Cambridge \\
4cc2fe62f7c3 New acknowledgements; no Fast_tac
paulson
parents: 3096
diff changeset
    13
        \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
4cc2fe62f7c3 New acknowledgements; no Fast_tac
paulson
parents: 3096
diff changeset
    14
        With Contributions by Tobias Nipkow and Markus Wenzel
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    15
}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    16
\makeindex
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    17
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    18
\underscoreoff
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    19
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    20
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    21
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    22
\sloppy
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    23
\binperiod     %%%treat . like a binary operator
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    24
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    25
\newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    26
\newcommand{\nand}{\mathbin{\lnot\&}} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    27
\newcommand{\xor}{\mathbin{\#}}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    28
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    29
\pagenumbering{roman} 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    30
\begin{document}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    31
\pagestyle{empty}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    32
\begin{titlepage}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    33
\maketitle 
14148
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    34
\emph{Note}: this document is part of the earlier Isabelle documentation, 
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    35
which is largely superseded by the Isabelle/HOL
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    36
\emph{Tutorial}~\cite{isa-tutorial}. It describes the old-style theory 
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    37
syntax and shows how to conduct proofs using the 
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    38
ML top level. This style of interaction is largely obsolete:
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    39
most Isabelle proofs are now written using the Isar 
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    40
language and the Proof General interface. However, this paper contains valuable 
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    41
information that is not available elsewhere. Its examples are based 
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    42
on first-order logic rather than higher-order logic.
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    43
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    44
\thispagestyle{empty}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    45
\vfill
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    46
{\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    47
\end{titlepage}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    48
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    49
\pagestyle{headings}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    50
\part*{Preface}
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1866
diff changeset
    51
\index{Isabelle!overview} \index{Isabelle!object-logics supported}
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1866
diff changeset
    52
Isabelle~\cite{paulson-natural,paulson-found,paulson700} is a generic theorem
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1866
diff changeset
    53
prover.  It has been instantiated to support reasoning in several
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1866
diff changeset
    54
object-logics:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    55
\begin{itemize}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    56
\item first-order logic, constructive and classical versions
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    57
\item higher-order logic, similar to that of Gordon's {\sc
348
1f5a94209c97 post-CRC corrections
lcp
parents: 311
diff changeset
    58
hol}~\cite{mgordon-hol}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    59
\item Zermelo-Fraenkel set theory~\cite{suppes72}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    60
\item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    61
\item the classical first-order sequent calculus, {\sc lk}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    62
\item the modal logics $T$, $S4$, and $S43$
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    63
\item the Logic for Computable Functions~\cite{paulson87}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    64
\end{itemize}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    65
A logic's syntax and inference rules are specified declaratively; this
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    66
allows single-step proof construction.  Isabelle provides control
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    67
structures for expressing search procedures.  Isabelle also provides
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    68
several generic tools, such as simplifiers and classical theorem provers,
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    69
which can be applied to object-logics.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    70
14148
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    71
Isabelle is a large system, but beginners can get by with a small
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    72
repertoire of commands and a basic knowledge of how Isabelle works.  
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    73
The Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial} describes how to get started. Advanced Isabelle users will benefit from some
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    74
knowledge of Standard~\ML{}, because Isabelle is written in \ML{};
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    75
\index{ML}
14148
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    76
if you are prepared to writing \ML{}
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    77
code, you can get Isabelle to do almost anything.  My book
6592
c120262044b6 Now uses manual.bib; some references updated
paulson
parents: 5170
diff changeset
    78
on~\ML{}~\cite{paulson-ml2} covers much material connected with Isabelle,
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    79
including a simple theorem prover.  Users must be familiar with logic as
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    80
used in computer science; there are many good
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    81
texts~\cite{galton90,reeves90}.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    82
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    83
\index{LCF}
348
1f5a94209c97 post-CRC corrections
lcp
parents: 311
diff changeset
    84
{\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    85
ancestor of {\sc hol}, Nuprl, and several other systems.  Isabelle borrows
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    86
ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    87
abstract type; tactics and tacticals support backward proof.  But {\sc lcf}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    88
represents object-level rules by functions, while Isabelle represents them
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    89
by terms.  You may find my other writings~\cite{paulson87,paulson-handbook}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    90
helpful in understanding the relationship between {\sc lcf} and Isabelle.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    91
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    92
\index{Isabelle!release history} Isabelle was first distributed in 1986.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    93
The 1987 version introduced a higher-order meta-logic with an improved
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    94
treatment of quantifiers.  The 1988 version added limited polymorphism and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    95
support for natural deduction.  The 1989 version included a parser and
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    96
pretty printer generator.  The 1992 version introduced type classes, to
14148
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    97
support many-sorted and higher-order logics.  The 1994 version introduced
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    98
greater support for theories.  The most important recent change is the
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
    99
introduction of the Isar proof language, thanks to Markus Wenzel.  
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
   100
Isabelle is still under
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   101
development and will continue to change.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   102
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   103
\subsubsection*{Overview} 
296
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 184
diff changeset
   104
This manual consists of three parts.  Part~I discusses the Isabelle's
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 184
diff changeset
   105
foundations.  Part~II, presents simple on-line sessions, starting with
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 184
diff changeset
   106
forward proof.  It also covers basic tactics and tacticals, and some
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 184
diff changeset
   107
commands for invoking them.  Part~III contains further examples for users
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 184
diff changeset
   108
with a bit of experience.  It explains how to derive rules define theories,
e1f6cd9f682e revisions to first Springer draft
lcp
parents: 184
diff changeset
   109
and concludes with an extended example: a Prolog interpreter.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   110
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   111
Isabelle's Reference Manual and Object-Logics manual contain more details.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   112
They assume familiarity with the concepts presented here.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   113
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   114
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   115
\subsubsection*{Acknowledgements} 
311
3fb8cdb32e10 penultimate Springer draft
lcp
parents: 296
diff changeset
   116
Tobias Nipkow contributed most of the section on defining theories.
14148
6580d374a509 corrections by Viktor Kuncak and minor updating
paulson
parents: 9695
diff changeset
   117
Stefan Berghofer, Sara Kalvala and Viktor Kuncak suggested improvements.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   118
8979
802acc97fdaf updated acknowledgements
paulson
parents: 8828
diff changeset
   119
Tobias Nipkow has made immense contributions to Isabelle, including the parser
802acc97fdaf updated acknowledgements
paulson
parents: 8828
diff changeset
   120
generator, type classes, and the simplifier.  Carsten Clasohm and Markus
802acc97fdaf updated acknowledgements
paulson
parents: 8828
diff changeset
   121
Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann also
802acc97fdaf updated acknowledgements
paulson
parents: 8828
diff changeset
   122
helped.  Isabelle was developed using Dave Matthews's Standard~{\sc ml}
802acc97fdaf updated acknowledgements
paulson
parents: 8828
diff changeset
   123
compiler, Poly/{\sc ml}.  Many people have contributed to Isabelle's standard
802acc97fdaf updated acknowledgements
paulson
parents: 8828
diff changeset
   124
object-logics, including Martin Coen, Philippe de Groote, Philippe No\"el.
802acc97fdaf updated acknowledgements
paulson
parents: 8828
diff changeset
   125
The research has been funded by the EPSRC (grants GR/G53279, GR/H40570,
802acc97fdaf updated acknowledgements
paulson
parents: 8828
diff changeset
   126
GR/K57381, GR/K77051, GR/M75440) and by ESPRIT (projects 3245: Logical
802acc97fdaf updated acknowledgements
paulson
parents: 8828
diff changeset
   127
Frameworks, and 6453: Types), and by the DFG Schwerpunktprogramm
802acc97fdaf updated acknowledgements
paulson
parents: 8828
diff changeset
   128
\emph{Deduktion}.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   129
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   130
\newpage
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   131
\pagestyle{plain} \tableofcontents 
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   132
\newpage
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   133
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   134
\newfont{\sanssi}{cmssi12}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   135
\vspace*{2.5cm}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   136
\begin{quote}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   137
\raggedleft
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   138
{\sanssi
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   139
You can only find truth with logic\\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   140
if you have already found truth without it.}\\
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   141
\bigskip
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   142
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   143
G.K. Chesterton, {\em The Man who was Orthodox}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   144
\end{quote}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   145
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   146
\clearfirst  \pagestyle{headings}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   147
\include{foundations}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   148
\include{getting}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   149
\include{advanced}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   150
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   151
\bibliographystyle{plain} \small\raggedright\frenchspacing
6592
c120262044b6 Now uses manual.bib; some references updated
paulson
parents: 5170
diff changeset
   152
\bibliography{../manual}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   153
8828
5be2d1745c61 improved indexing;
wenzelm
parents: 7827
diff changeset
   154
\printindex
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   155
\end{document}