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