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