doc-src/Intro/intro.tex
author wenzelm
Mon Oct 01 21:19:50 2007 +0200 (2007-10-01)
changeset 24803 38577b4b1fde
parent 14148 6580d374a509
child 30118 df610709eda5
permissions -rw-r--r--
Norbert Schirmer: record improvements;
     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 \emph{Note}: this document is part of the earlier Isabelle documentation, 
    35 which is largely superseded by the Isabelle/HOL
    36 \emph{Tutorial}~\cite{isa-tutorial}. It describes the old-style theory 
    37 syntax and shows how to conduct proofs using the 
    38 ML top level. This style of interaction is largely obsolete:
    39 most Isabelle proofs are now written using the Isar 
    40 language and the Proof General interface. However, this paper contains valuable 
    41 information that is not available elsewhere. Its examples are based 
    42 on first-order logic rather than higher-order logic.
    43 
    44 \thispagestyle{empty}
    45 \vfill
    46 {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
    47 \end{titlepage}
    48 
    49 \pagestyle{headings}
    50 \part*{Preface}
    51 \index{Isabelle!overview} \index{Isabelle!object-logics supported}
    52 Isabelle~\cite{paulson-natural,paulson-found,paulson700} is a generic theorem
    53 prover.  It has been instantiated to support reasoning in several
    54 object-logics:
    55 \begin{itemize}
    56 \item first-order logic, constructive and classical versions
    57 \item higher-order logic, similar to that of Gordon's {\sc
    58 hol}~\cite{mgordon-hol}
    59 \item Zermelo-Fraenkel set theory~\cite{suppes72}
    60 \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}
    61 \item the classical first-order sequent calculus, {\sc lk}
    62 \item the modal logics $T$, $S4$, and $S43$
    63 \item the Logic for Computable Functions~\cite{paulson87}
    64 \end{itemize}
    65 A logic's syntax and inference rules are specified declaratively; this
    66 allows single-step proof construction.  Isabelle provides control
    67 structures for expressing search procedures.  Isabelle also provides
    68 several generic tools, such as simplifiers and classical theorem provers,
    69 which can be applied to object-logics.
    70 
    71 Isabelle is a large system, but beginners can get by with a small
    72 repertoire of commands and a basic knowledge of how Isabelle works.  
    73 The Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial} describes how to get started. Advanced Isabelle users will benefit from some
    74 knowledge of Standard~\ML{}, because Isabelle is written in \ML{};
    75 \index{ML}
    76 if you are prepared to writing \ML{}
    77 code, you can get Isabelle to do almost anything.  My book
    78 on~\ML{}~\cite{paulson-ml2} covers much material connected with Isabelle,
    79 including a simple theorem prover.  Users must be familiar with logic as
    80 used in computer science; there are many good
    81 texts~\cite{galton90,reeves90}.
    82 
    83 \index{LCF}
    84 {\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an
    85 ancestor of {\sc hol}, Nuprl, and several other systems.  Isabelle borrows
    86 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
    87 abstract type; tactics and tacticals support backward proof.  But {\sc lcf}
    88 represents object-level rules by functions, while Isabelle represents them
    89 by terms.  You may find my other writings~\cite{paulson87,paulson-handbook}
    90 helpful in understanding the relationship between {\sc lcf} and Isabelle.
    91 
    92 \index{Isabelle!release history} Isabelle was first distributed in 1986.
    93 The 1987 version introduced a higher-order meta-logic with an improved
    94 treatment of quantifiers.  The 1988 version added limited polymorphism and
    95 support for natural deduction.  The 1989 version included a parser and
    96 pretty printer generator.  The 1992 version introduced type classes, to
    97 support many-sorted and higher-order logics.  The 1994 version introduced
    98 greater support for theories.  The most important recent change is the
    99 introduction of the Isar proof language, thanks to Markus Wenzel.  
   100 Isabelle is still under
   101 development and will continue to change.
   102 
   103 \subsubsection*{Overview} 
   104 This manual consists of three parts.  Part~I discusses the Isabelle's
   105 foundations.  Part~II, presents simple on-line sessions, starting with
   106 forward proof.  It also covers basic tactics and tacticals, and some
   107 commands for invoking them.  Part~III contains further examples for users
   108 with a bit of experience.  It explains how to derive rules define theories,
   109 and concludes with an extended example: a Prolog interpreter.
   110 
   111 Isabelle's Reference Manual and Object-Logics manual contain more details.
   112 They assume familiarity with the concepts presented here.
   113 
   114 
   115 \subsubsection*{Acknowledgements} 
   116 Tobias Nipkow contributed most of the section on defining theories.
   117 Stefan Berghofer, Sara Kalvala and Viktor Kuncak suggested improvements.
   118 
   119 Tobias Nipkow has made immense contributions to Isabelle, including the parser
   120 generator, type classes, and the simplifier.  Carsten Clasohm and Markus
   121 Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann also
   122 helped.  Isabelle was developed using Dave Matthews's Standard~{\sc ml}
   123 compiler, Poly/{\sc ml}.  Many people have contributed to Isabelle's standard
   124 object-logics, including Martin Coen, Philippe de Groote, Philippe No\"el.
   125 The research has been funded by the EPSRC (grants GR/G53279, GR/H40570,
   126 GR/K57381, GR/K77051, GR/M75440) and by ESPRIT (projects 3245: Logical
   127 Frameworks, and 6453: Types), and by the DFG Schwerpunktprogramm
   128 \emph{Deduktion}.
   129 
   130 \newpage
   131 \pagestyle{plain} \tableofcontents 
   132 \newpage
   133 
   134 \newfont{\sanssi}{cmssi12}
   135 \vspace*{2.5cm}
   136 \begin{quote}
   137 \raggedleft
   138 {\sanssi
   139 You can only find truth with logic\\
   140 if you have already found truth without it.}\\
   141 \bigskip
   142 
   143 G.K. Chesterton, {\em The Man who was Orthodox}
   144 \end{quote}
   145 
   146 \clearfirst  \pagestyle{headings}
   147 \include{foundations}
   148 \include{getting}
   149 \include{advanced}
   150 
   151 \bibliographystyle{plain} \small\raggedright\frenchspacing
   152 \bibliography{../manual}
   153 
   154 \printindex
   155 \end{document}