diff -r d8205bb279a7 -r 216d6ed87399 doc-src/Intro/intro.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Intro/intro.tex Wed Nov 10 05:06:55 1993 +0100 @@ -0,0 +1,149 @@ +\documentstyle[a4,12pt,proof,iman,alltt]{article} +%% $Id$ +%% run bibtex intro to prepare bibliography +%% run ../sedindex intro to prepare index file +%prth *(\(.*\)); \1; +%{\\out \(.*\)} {\\out val it = "\1" : thm} + +\title{Introduction to Isabelle} +\author{{\em Lawrence C. Paulson}\\ + Computer Laboratory \\ University of Cambridge \\[2ex] + {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}} +} +\date{} +\makeindex + +\underscoreoff + +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} + +\sloppy +\binperiod %%%treat . like a binary operator + +\newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification +\newcommand{\nand}{\mathbin{\lnot\&}} +\newcommand{\xor}{\mathbin{\#}} + +\pagenumbering{roman} +\begin{document} +\pagestyle{empty} +\begin{titlepage} +\maketitle +\thispagestyle{empty} +\vfill +{\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson} +\end{titlepage} + +\pagestyle{headings} +\part*{Preface} +\index{Isabelle!overview} +\index{Isabelle!object-logics supported} +Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover. +It has been instantiated to support reasoning in several object-logics: +\begin{itemize} +\item first-order logic, constructive and classical versions +\item higher-order logic, similar to that of Gordon's {\sc +hol}~\cite{gordon88a} +\item Zermelo-Fraenkel set theory~\cite{suppes72} +\item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90} +\item the classical first-order sequent calculus, {\sc lk} +\item the modal logics $T$, $S4$, and $S43$ +\item the Logic for Computable Functions~\cite{paulson87} +\end{itemize} +A logic's syntax and inference rules are specified declaratively; this +allows single-step proof construction. Isabelle provides control +structures for expressing search procedures. Isabelle also provides +several generic tools, such as simplifiers and classical theorem provers, +which can be applied to object-logics. + +\index{ML} +Isabelle is a large system, but beginners can get by with a small +repertoire of commands and a basic knowledge of how Isabelle works. Some +knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user +interface. Advanced Isabelle theorem proving can involve writing \ML{} +code, possibly with Isabelle's sources at hand. My book +on~\ML{}~\cite{paulson91} covers much material connected with Isabelle, +including a simple theorem prover. Users must be familiar with logic as +used in computer science; there are many good +texts~\cite{galton90,reeves90}. + +\index{LCF} +{\sc lcf}, developed by Robin Milner and colleagues~\cite{gordon79}, is an +ancestor of {\sc hol}, Nuprl, and several other systems. Isabelle borrows +ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an +abstract type; tactics and tacticals support backward proof. But {\sc lcf} +represents object-level rules by functions, while Isabelle represents them +by terms. You may find my other writings~\cite{paulson87,paulson-handbook} +helpful in understanding the relationship between {\sc lcf} and Isabelle. + +Isabelle does not keep a record of inference steps. Each step is checked +at run time to ensure that theorems can only be constructed by applying +inference rules. An Isabelle proof typically involves hundreds of +primitive inferences, and would be unintelligible if displayed. +Discarding proofs saves vast amounts of storage. But can Isabelle be +trusted? If desired, object-logics can be formalized such that each +theorem carries a proof term, which could be checked by another program. +Proofs can also be traced. + +\index{Isabelle!release history} Isabelle was first distributed in 1986. +The 1987 version introduced a higher-order meta-logic with an improved +treatment of quantifiers. The 1988 version added limited polymorphism and +support for natural deduction. The 1989 version included a parser and +pretty printer generator. The 1992 version introduced type classes, to +support many-sorted and higher-order logics. The current version provides +greater support for theories and is much faster. Isabelle is still under +development and will continue to change. + +\subsubsection*{Overview} +This manual consists of three parts. +Part~I discusses the Isabelle's foundations. +Part~II, presents simple on-line sessions, starting with forward proof. +It also covers basic tactics and tacticals, and some commands for invoking +Part~III contains further examples for users with a bit of experience. +It explains how to derive rules define theories, and concludes with an +extended example: a Prolog interpreter. + +Isabelle's Reference Manual and Object-Logics manual contain more details. +They assume familiarity with the concepts presented here. + + +\subsubsection*{Acknowledgements} +Tobias Nipkow contributed most of the section on ``Defining Theories''. +Sara Kalvala and Markus Wenzel suggested improvements. + +Tobias Nipkow has made immense contributions to Isabelle, including the +parser generator, type classes, and the simplifier. Carsten Clasohm, Sonia +Mahjoub, Karin Nimmermann and Markus Wenzel also made improvements. +Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler, +Poly/{\sc ml}. Many people have contributed to Isabelle's standard +object-logics, including Martin Coen, Philippe de Groote, Philippe No\"el. +The research has been funded by the SERC (grants GR/G53279, GR/H40570) and +by ESPRIT (projects 3245: Logical Frameworks, and 6453: Types). + +\newpage +\pagestyle{plain} \tableofcontents +\newpage + +\newfont{\sanssi}{cmssi12} +\vspace*{2.5cm} +\begin{quote} +\raggedleft +{\sanssi +You can only find truth with logic\\ +if you have already found truth without it.}\\ +\bigskip + +G.K. Chesterton, {\em The Man who was Orthodox} +\end{quote} + +\clearfirst \pagestyle{headings} +\include{foundations} +\include{getting} +\include{advanced} + + +\bibliographystyle{plain} \small\raggedright\frenchspacing +\bibliography{atp,funprog,general,logicprog,theory} + +\input{intro.ind} +\end{document}