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