doc-src/Intro/intro.tex
changeset 105 216d6ed87399
child 184 236b655114a1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Intro/intro.tex	Wed Nov 10 05:06:55 1993 +0100
     1.3 @@ -0,0 +1,149 @@
     1.4 +\documentstyle[a4,12pt,proof,iman,alltt]{article}
     1.5 +%% $Id$
     1.6 +%% run    bibtex intro         to prepare bibliography
     1.7 +%% run    ../sedindex intro    to prepare index file
     1.8 +%prth *(\(.*\));          \1;      
     1.9 +%{\\out \(.*\)}          {\\out val it = "\1" : thm}
    1.10 +
    1.11 +\title{Introduction to Isabelle}   
    1.12 +\author{{\em Lawrence C. Paulson}\\
    1.13 +        Computer Laboratory \\ University of Cambridge \\[2ex]
    1.14 +        {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}}
    1.15 +}
    1.16 +\date{} 
    1.17 +\makeindex
    1.18 +
    1.19 +\underscoreoff
    1.20 +
    1.21 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    1.22 +
    1.23 +\sloppy
    1.24 +\binperiod     %%%treat . like a binary operator
    1.25 +
    1.26 +\newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
    1.27 +\newcommand{\nand}{\mathbin{\lnot\&}} 
    1.28 +\newcommand{\xor}{\mathbin{\#}}
    1.29 +
    1.30 +\pagenumbering{roman} 
    1.31 +\begin{document}
    1.32 +\pagestyle{empty}
    1.33 +\begin{titlepage}
    1.34 +\maketitle 
    1.35 +\thispagestyle{empty}
    1.36 +\vfill
    1.37 +{\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
    1.38 +\end{titlepage}
    1.39 +
    1.40 +\pagestyle{headings}
    1.41 +\part*{Preface}
    1.42 +\index{Isabelle!overview}
    1.43 +\index{Isabelle!object-logics supported}
    1.44 +Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover.
    1.45 +It has been instantiated to support reasoning in several object-logics:
    1.46 +\begin{itemize}
    1.47 +\item first-order logic, constructive and classical versions
    1.48 +\item higher-order logic, similar to that of Gordon's {\sc
    1.49 +hol}~\cite{gordon88a}
    1.50 +\item Zermelo-Fraenkel set theory~\cite{suppes72}
    1.51 +\item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}
    1.52 +\item the classical first-order sequent calculus, {\sc lk}
    1.53 +\item the modal logics $T$, $S4$, and $S43$
    1.54 +\item the Logic for Computable Functions~\cite{paulson87}
    1.55 +\end{itemize}
    1.56 +A logic's syntax and inference rules are specified declaratively; this
    1.57 +allows single-step proof construction.  Isabelle provides control
    1.58 +structures for expressing search procedures.  Isabelle also provides
    1.59 +several generic tools, such as simplifiers and classical theorem provers,
    1.60 +which can be applied to object-logics.
    1.61 +
    1.62 +\index{ML}
    1.63 +Isabelle is a large system, but beginners can get by with a small
    1.64 +repertoire of commands and a basic knowledge of how Isabelle works.  Some
    1.65 +knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user
    1.66 +interface.  Advanced Isabelle theorem proving can involve writing \ML{}
    1.67 +code, possibly with Isabelle's sources at hand.  My book
    1.68 +on~\ML{}~\cite{paulson91} covers much material connected with Isabelle,
    1.69 +including a simple theorem prover.  Users must be familiar with logic as
    1.70 +used in computer science; there are many good
    1.71 +texts~\cite{galton90,reeves90}.
    1.72 +
    1.73 +\index{LCF}
    1.74 +{\sc lcf}, developed by Robin Milner and colleagues~\cite{gordon79}, is an
    1.75 +ancestor of {\sc hol}, Nuprl, and several other systems.  Isabelle borrows
    1.76 +ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
    1.77 +abstract type; tactics and tacticals support backward proof.  But {\sc lcf}
    1.78 +represents object-level rules by functions, while Isabelle represents them
    1.79 +by terms.  You may find my other writings~\cite{paulson87,paulson-handbook}
    1.80 +helpful in understanding the relationship between {\sc lcf} and Isabelle.
    1.81 +
    1.82 +Isabelle does not keep a record of inference steps.  Each step is checked
    1.83 +at run time to ensure that theorems can only be constructed by applying
    1.84 +inference rules.  An Isabelle proof typically involves hundreds of
    1.85 +primitive inferences, and would be unintelligible if displayed.
    1.86 +Discarding proofs saves vast amounts of storage.  But can Isabelle be
    1.87 +trusted?  If desired, object-logics can be formalized such that each
    1.88 +theorem carries a proof term, which could be checked by another program.
    1.89 +Proofs can also be traced.
    1.90 +
    1.91 +\index{Isabelle!release history} Isabelle was first distributed in 1986.
    1.92 +The 1987 version introduced a higher-order meta-logic with an improved
    1.93 +treatment of quantifiers.  The 1988 version added limited polymorphism and
    1.94 +support for natural deduction.  The 1989 version included a parser and
    1.95 +pretty printer generator.  The 1992 version introduced type classes, to
    1.96 +support many-sorted and higher-order logics.  The current version provides
    1.97 +greater support for theories and is much faster.  Isabelle is still under
    1.98 +development and will continue to change.
    1.99 +
   1.100 +\subsubsection*{Overview} 
   1.101 +This manual consists of three parts.  
   1.102 +Part~I discusses the Isabelle's foundations.
   1.103 +Part~II, presents simple on-line sessions, starting with forward proof.
   1.104 +It also covers basic tactics and tacticals, and some commands for invoking
   1.105 +Part~III contains further examples for users with a bit of experience.
   1.106 +It explains how to derive rules define theories, and concludes with an
   1.107 +extended example: a Prolog interpreter.
   1.108 +
   1.109 +Isabelle's Reference Manual and Object-Logics manual contain more details.
   1.110 +They assume familiarity with the concepts presented here.
   1.111 +
   1.112 +
   1.113 +\subsubsection*{Acknowledgements} 
   1.114 +Tobias Nipkow contributed most of the section on ``Defining Theories''.
   1.115 +Sara Kalvala and Markus Wenzel suggested improvements.
   1.116 +
   1.117 +Tobias Nipkow has made immense contributions to Isabelle, including the
   1.118 +parser generator, type classes, and the simplifier.  Carsten Clasohm, Sonia
   1.119 +Mahjoub, Karin Nimmermann and Markus Wenzel also made improvements.
   1.120 +Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler,
   1.121 +Poly/{\sc ml}.  Many people have contributed to Isabelle's standard
   1.122 +object-logics, including Martin Coen, Philippe de Groote, Philippe No\"el.
   1.123 +The research has been funded by the SERC (grants GR/G53279, GR/H40570) and
   1.124 +by ESPRIT (projects 3245: Logical Frameworks, and 6453: Types).
   1.125 +
   1.126 +\newpage
   1.127 +\pagestyle{plain} \tableofcontents 
   1.128 +\newpage
   1.129 +
   1.130 +\newfont{\sanssi}{cmssi12}
   1.131 +\vspace*{2.5cm}
   1.132 +\begin{quote}
   1.133 +\raggedleft
   1.134 +{\sanssi
   1.135 +You can only find truth with logic\\
   1.136 +if you have already found truth without it.}\\
   1.137 +\bigskip
   1.138 +
   1.139 +G.K. Chesterton, {\em The Man who was Orthodox}
   1.140 +\end{quote}
   1.141 +
   1.142 +\clearfirst  \pagestyle{headings}
   1.143 +\include{foundations}
   1.144 +\include{getting}
   1.145 +\include{advanced}
   1.146 +
   1.147 +
   1.148 +\bibliographystyle{plain} \small\raggedright\frenchspacing
   1.149 +\bibliography{atp,funprog,general,logicprog,theory}
   1.150 +
   1.151 +\input{intro.ind}
   1.152 +\end{document}