doc-src/Intro/intro.tex
author lcp
Fri Apr 15 11:48:23 1994 +0200 (1994-04-15)
changeset 311 3fb8cdb32e10
parent 296 e1f6cd9f682e
child 348 1f5a94209c97
permissions -rw-r--r--
penultimate Springer draft
lcp@296
     1
\documentstyle[a4,12pt,proof,iman,extra]{article}
lcp@105
     2
%% $Id$
lcp@105
     3
%% run    bibtex intro         to prepare bibliography
lcp@105
     4
%% run    ../sedindex intro    to prepare index file
lcp@105
     5
%prth *(\(.*\));          \1;      
lcp@105
     6
%{\\out \(.*\)}          {\\out val it = "\1" : thm}
lcp@105
     7
lcp@105
     8
\title{Introduction to Isabelle}   
lcp@105
     9
\author{{\em Lawrence C. Paulson}\\
lcp@105
    10
        Computer Laboratory \\ University of Cambridge \\[2ex]
lcp@105
    11
        {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}}
lcp@105
    12
}
lcp@105
    13
\date{} 
lcp@105
    14
\makeindex
lcp@105
    15
lcp@105
    16
\underscoreoff
lcp@105
    17
lcp@105
    18
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
lcp@105
    19
lcp@105
    20
\sloppy
lcp@105
    21
\binperiod     %%%treat . like a binary operator
lcp@105
    22
lcp@105
    23
\newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
lcp@105
    24
\newcommand{\nand}{\mathbin{\lnot\&}} 
lcp@105
    25
\newcommand{\xor}{\mathbin{\#}}
lcp@105
    26
lcp@105
    27
\pagenumbering{roman} 
lcp@105
    28
\begin{document}
lcp@105
    29
\pagestyle{empty}
lcp@105
    30
\begin{titlepage}
lcp@105
    31
\maketitle 
lcp@105
    32
\thispagestyle{empty}
lcp@105
    33
\vfill
lcp@105
    34
{\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
lcp@105
    35
\end{titlepage}
lcp@105
    36
lcp@105
    37
\pagestyle{headings}
lcp@105
    38
\part*{Preface}
lcp@105
    39
\index{Isabelle!overview}
lcp@105
    40
\index{Isabelle!object-logics supported}
lcp@105
    41
Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover.
lcp@105
    42
It has been instantiated to support reasoning in several object-logics:
lcp@105
    43
\begin{itemize}
lcp@105
    44
\item first-order logic, constructive and classical versions
lcp@105
    45
\item higher-order logic, similar to that of Gordon's {\sc
lcp@105
    46
hol}~\cite{gordon88a}
lcp@105
    47
\item Zermelo-Fraenkel set theory~\cite{suppes72}
lcp@105
    48
\item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}
lcp@105
    49
\item the classical first-order sequent calculus, {\sc lk}
lcp@105
    50
\item the modal logics $T$, $S4$, and $S43$
lcp@105
    51
\item the Logic for Computable Functions~\cite{paulson87}
lcp@105
    52
\end{itemize}
lcp@105
    53
A logic's syntax and inference rules are specified declaratively; this
lcp@105
    54
allows single-step proof construction.  Isabelle provides control
lcp@105
    55
structures for expressing search procedures.  Isabelle also provides
lcp@105
    56
several generic tools, such as simplifiers and classical theorem provers,
lcp@105
    57
which can be applied to object-logics.
lcp@105
    58
lcp@105
    59
\index{ML}
lcp@105
    60
Isabelle is a large system, but beginners can get by with a small
lcp@105
    61
repertoire of commands and a basic knowledge of how Isabelle works.  Some
lcp@105
    62
knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user
lcp@105
    63
interface.  Advanced Isabelle theorem proving can involve writing \ML{}
lcp@105
    64
code, possibly with Isabelle's sources at hand.  My book
lcp@105
    65
on~\ML{}~\cite{paulson91} covers much material connected with Isabelle,
lcp@105
    66
including a simple theorem prover.  Users must be familiar with logic as
lcp@105
    67
used in computer science; there are many good
lcp@105
    68
texts~\cite{galton90,reeves90}.
lcp@105
    69
lcp@105
    70
\index{LCF}
lcp@105
    71
{\sc lcf}, developed by Robin Milner and colleagues~\cite{gordon79}, is an
lcp@105
    72
ancestor of {\sc hol}, Nuprl, and several other systems.  Isabelle borrows
lcp@105
    73
ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
lcp@105
    74
abstract type; tactics and tacticals support backward proof.  But {\sc lcf}
lcp@105
    75
represents object-level rules by functions, while Isabelle represents them
lcp@105
    76
by terms.  You may find my other writings~\cite{paulson87,paulson-handbook}
lcp@105
    77
helpful in understanding the relationship between {\sc lcf} and Isabelle.
lcp@105
    78
lcp@105
    79
Isabelle does not keep a record of inference steps.  Each step is checked
lcp@105
    80
at run time to ensure that theorems can only be constructed by applying
lcp@105
    81
inference rules.  An Isabelle proof typically involves hundreds of
lcp@105
    82
primitive inferences, and would be unintelligible if displayed.
lcp@105
    83
Discarding proofs saves vast amounts of storage.  But can Isabelle be
lcp@105
    84
trusted?  If desired, object-logics can be formalized such that each
lcp@105
    85
theorem carries a proof term, which could be checked by another program.
lcp@105
    86
Proofs can also be traced.
lcp@105
    87
lcp@105
    88
\index{Isabelle!release history} Isabelle was first distributed in 1986.
lcp@105
    89
The 1987 version introduced a higher-order meta-logic with an improved
lcp@105
    90
treatment of quantifiers.  The 1988 version added limited polymorphism and
lcp@105
    91
support for natural deduction.  The 1989 version included a parser and
lcp@105
    92
pretty printer generator.  The 1992 version introduced type classes, to
lcp@105
    93
support many-sorted and higher-order logics.  The current version provides
lcp@105
    94
greater support for theories and is much faster.  Isabelle is still under
lcp@105
    95
development and will continue to change.
lcp@105
    96
lcp@105
    97
\subsubsection*{Overview} 
lcp@296
    98
This manual consists of three parts.  Part~I discusses the Isabelle's
lcp@296
    99
foundations.  Part~II, presents simple on-line sessions, starting with
lcp@296
   100
forward proof.  It also covers basic tactics and tacticals, and some
lcp@296
   101
commands for invoking them.  Part~III contains further examples for users
lcp@296
   102
with a bit of experience.  It explains how to derive rules define theories,
lcp@296
   103
and concludes with an extended example: a Prolog interpreter.
lcp@105
   104
lcp@105
   105
Isabelle's Reference Manual and Object-Logics manual contain more details.
lcp@105
   106
They assume familiarity with the concepts presented here.
lcp@105
   107
lcp@105
   108
lcp@105
   109
\subsubsection*{Acknowledgements} 
lcp@311
   110
Tobias Nipkow contributed most of the section on defining theories.
lcp@105
   111
Sara Kalvala and Markus Wenzel suggested improvements.
lcp@105
   112
lcp@105
   113
Tobias Nipkow has made immense contributions to Isabelle, including the
lcp@184
   114
parser generator, type classes, and the simplifier.  Carsten Clasohm and
lcp@184
   115
Markus Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann
lcp@184
   116
also helped.  Isabelle was developed using Dave Matthews's Standard~{\sc
lcp@184
   117
  ml} compiler, Poly/{\sc ml}.  Many people have contributed to Isabelle's
lcp@184
   118
standard object-logics, including Martin Coen, Philippe de Groote, Philippe
lcp@184
   119
No\"el.  The research has been funded by the SERC (grants GR/G53279,
lcp@184
   120
GR/H40570) and by ESPRIT (projects 3245: Logical Frameworks, and 6453:
lcp@184
   121
Types).
lcp@105
   122
lcp@105
   123
\newpage
lcp@105
   124
\pagestyle{plain} \tableofcontents 
lcp@105
   125
\newpage
lcp@105
   126
lcp@105
   127
\newfont{\sanssi}{cmssi12}
lcp@105
   128
\vspace*{2.5cm}
lcp@105
   129
\begin{quote}
lcp@105
   130
\raggedleft
lcp@105
   131
{\sanssi
lcp@105
   132
You can only find truth with logic\\
lcp@105
   133
if you have already found truth without it.}\\
lcp@105
   134
\bigskip
lcp@105
   135
lcp@105
   136
G.K. Chesterton, {\em The Man who was Orthodox}
lcp@105
   137
\end{quote}
lcp@105
   138
lcp@105
   139
\clearfirst  \pagestyle{headings}
lcp@105
   140
\include{foundations}
lcp@105
   141
\include{getting}
lcp@105
   142
\include{advanced}
lcp@105
   143
lcp@105
   144
\bibliographystyle{plain} \small\raggedright\frenchspacing
lcp@296
   145
\bibliography{string,atp,funprog,general,logicprog,theory}
lcp@105
   146
lcp@105
   147
\input{intro.ind}
lcp@105
   148
\end{document}