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