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