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