wenzelm@2656: \documentstyle[a4,12pt]{article}
wenzelm@2656: \makeatletter
wenzelm@2656: \input{../proof209.sty}
wenzelm@2656: \input{../iman.sty}
wenzelm@2656: \input{../extra.sty}
wenzelm@2656: \makeatother
wenzelm@2656:
lcp@105: %% $Id$
lcp@105: %% run bibtex intro to prepare bibliography
lcp@105: %% run ../sedindex intro to prepare index file
lcp@105: %prth *(\(.*\)); \1;
lcp@105: %{\\out \(.*\)} {\\out val it = "\1" : thm}
lcp@105:
lcp@105: \title{Introduction to Isabelle}
lcp@105: \author{{\em Lawrence C. Paulson}\\
lcp@105: Computer Laboratory \\ University of Cambridge \\[2ex]
lcp@105: {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}}
lcp@105: }
lcp@105: \makeindex
lcp@105:
lcp@105: \underscoreoff
lcp@105:
lcp@105: \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
lcp@105:
lcp@105: \sloppy
lcp@105: \binperiod %%%treat . like a binary operator
lcp@105:
lcp@105: \newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification
lcp@105: \newcommand{\nand}{\mathbin{\lnot\&}}
lcp@105: \newcommand{\xor}{\mathbin{\#}}
lcp@105:
lcp@105: \pagenumbering{roman}
lcp@105: \begin{document}
lcp@105: \pagestyle{empty}
lcp@105: \begin{titlepage}
lcp@105: \maketitle
lcp@105: \thispagestyle{empty}
lcp@105: \vfill
lcp@105: {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
lcp@105: \end{titlepage}
lcp@105:
lcp@105: \pagestyle{headings}
lcp@105: \part*{Preface}
paulson@1878: \index{Isabelle!overview} \index{Isabelle!object-logics supported}
paulson@1878: Isabelle~\cite{paulson-natural,paulson-found,paulson700} is a generic theorem
paulson@1878: prover. It has been instantiated to support reasoning in several
paulson@1878: object-logics:
lcp@105: \begin{itemize}
lcp@105: \item first-order logic, constructive and classical versions
lcp@105: \item higher-order logic, similar to that of Gordon's {\sc
lcp@348: hol}~\cite{mgordon-hol}
lcp@105: \item Zermelo-Fraenkel set theory~\cite{suppes72}
lcp@105: \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}
lcp@105: \item the classical first-order sequent calculus, {\sc lk}
lcp@105: \item the modal logics $T$, $S4$, and $S43$
lcp@105: \item the Logic for Computable Functions~\cite{paulson87}
lcp@105: \end{itemize}
lcp@105: A logic's syntax and inference rules are specified declaratively; this
lcp@105: allows single-step proof construction. Isabelle provides control
lcp@105: structures for expressing search procedures. Isabelle also provides
lcp@105: several generic tools, such as simplifiers and classical theorem provers,
lcp@105: which can be applied to object-logics.
lcp@105:
lcp@105: \index{ML}
lcp@105: Isabelle is a large system, but beginners can get by with a small
lcp@105: repertoire of commands and a basic knowledge of how Isabelle works. Some
lcp@105: knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user
lcp@105: interface. Advanced Isabelle theorem proving can involve writing \ML{}
lcp@105: code, possibly with Isabelle's sources at hand. My book
lcp@105: on~\ML{}~\cite{paulson91} covers much material connected with Isabelle,
lcp@105: including a simple theorem prover. Users must be familiar with logic as
lcp@105: used in computer science; there are many good
lcp@105: texts~\cite{galton90,reeves90}.
lcp@105:
lcp@105: \index{LCF}
lcp@348: {\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an
lcp@105: ancestor of {\sc hol}, Nuprl, and several other systems. Isabelle borrows
lcp@105: ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
lcp@105: abstract type; tactics and tacticals support backward proof. But {\sc lcf}
lcp@105: represents object-level rules by functions, while Isabelle represents them
lcp@105: by terms. You may find my other writings~\cite{paulson87,paulson-handbook}
lcp@105: helpful in understanding the relationship between {\sc lcf} and Isabelle.
lcp@105:
lcp@105: \index{Isabelle!release history} Isabelle was first distributed in 1986.
lcp@105: The 1987 version introduced a higher-order meta-logic with an improved
lcp@105: treatment of quantifiers. The 1988 version added limited polymorphism and
lcp@105: support for natural deduction. The 1989 version included a parser and
lcp@105: pretty printer generator. The 1992 version introduced type classes, to
lcp@105: support many-sorted and higher-order logics. The current version provides
lcp@105: greater support for theories and is much faster. Isabelle is still under
lcp@105: development and will continue to change.
lcp@105:
lcp@105: \subsubsection*{Overview}
lcp@296: This manual consists of three parts. Part~I discusses the Isabelle's
lcp@296: foundations. Part~II, presents simple on-line sessions, starting with
lcp@296: forward proof. It also covers basic tactics and tacticals, and some
lcp@296: commands for invoking them. Part~III contains further examples for users
lcp@296: with a bit of experience. It explains how to derive rules define theories,
lcp@296: and concludes with an extended example: a Prolog interpreter.
lcp@105:
lcp@105: Isabelle's Reference Manual and Object-Logics manual contain more details.
lcp@105: They assume familiarity with the concepts presented here.
lcp@105:
lcp@105:
lcp@105: \subsubsection*{Acknowledgements}
lcp@311: Tobias Nipkow contributed most of the section on defining theories.
paulson@1866: Stefan Berghofer, Sara Kalvala and Markus Wenzel suggested improvements.
lcp@105:
lcp@105: Tobias Nipkow has made immense contributions to Isabelle, including the
lcp@184: parser generator, type classes, and the simplifier. Carsten Clasohm and
lcp@184: Markus Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann
lcp@184: also helped. Isabelle was developed using Dave Matthews's Standard~{\sc
lcp@184: ml} compiler, Poly/{\sc ml}. Many people have contributed to Isabelle's
lcp@184: standard object-logics, including Martin Coen, Philippe de Groote, Philippe
lcp@184: No\"el. The research has been funded by the SERC (grants GR/G53279,
lcp@184: GR/H40570) and by ESPRIT (projects 3245: Logical Frameworks, and 6453:
lcp@184: Types).
lcp@105:
lcp@105: \newpage
lcp@105: \pagestyle{plain} \tableofcontents
lcp@105: \newpage
lcp@105:
lcp@105: \newfont{\sanssi}{cmssi12}
lcp@105: \vspace*{2.5cm}
lcp@105: \begin{quote}
lcp@105: \raggedleft
lcp@105: {\sanssi
lcp@105: You can only find truth with logic\\
lcp@105: if you have already found truth without it.}\\
lcp@105: \bigskip
lcp@105:
lcp@105: G.K. Chesterton, {\em The Man who was Orthodox}
lcp@105: \end{quote}
lcp@105:
lcp@105: \clearfirst \pagestyle{headings}
lcp@105: \include{foundations}
lcp@105: \include{getting}
lcp@105: \include{advanced}
lcp@105:
lcp@105: \bibliographystyle{plain} \small\raggedright\frenchspacing
lcp@873: \bibliography{string,atp,funprog,general,logicprog,isabelle,theory,crossref}
lcp@105:
lcp@105: \input{intro.ind}
lcp@105: \end{document}