summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Intro/intro.tex

author | paulson |

Tue, 10 Feb 2004 12:02:11 +0100 | |

changeset 14378 | 69c4d5997669 |

parent 14148 | 6580d374a509 |

child 30118 | df610709eda5 |

permissions | -rw-r--r-- |

generic of_nat and of_int functions, and generalization of iszero
and neg

\documentclass[12pt,a4paper]{article} \usepackage{graphicx,../iman,../extra,../ttbox,../proof,../pdfsetup} %% $Id$ %% run bibtex intro to prepare bibliography %% run ../sedindex intro to prepare index file %prth *(\(.*\)); \1; %{\\out \(.*\)} {\\out val it = "\1" : thm} \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Introduction to Isabelle} \author{{\em Lawrence C. Paulson}\\ Computer Laboratory \\ University of Cambridge \\ \texttt{lcp@cl.cam.ac.uk}\\[3ex] With Contributions by Tobias Nipkow and Markus Wenzel } \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 \emph{Note}: this document is part of the earlier Isabelle documentation, which is largely superseded by the Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial}. It describes the old-style theory syntax and shows how to conduct proofs using the ML top level. This style of interaction is largely obsolete: most Isabelle proofs are now written using the Isar language and the Proof General interface. However, this paper contains valuable information that is not available elsewhere. Its examples are based on first-order logic rather than higher-order logic. \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{paulson-natural,paulson-found,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{mgordon-hol} \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. Isabelle is a large system, but beginners can get by with a small repertoire of commands and a basic knowledge of how Isabelle works. The Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial} describes how to get started. Advanced Isabelle users will benefit from some knowledge of Standard~\ML{}, because Isabelle is written in \ML{}; \index{ML} if you are prepared to writing \ML{} code, you can get Isabelle to do almost anything. My book on~\ML{}~\cite{paulson-ml2} 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{mgordon79}, 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. \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 1994 version introduced greater support for theories. The most important recent change is the introduction of the Isar proof language, thanks to Markus Wenzel. 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 them. 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. Stefan Berghofer, Sara Kalvala and Viktor Kuncak suggested improvements. Tobias Nipkow has made immense contributions to Isabelle, including the parser generator, type classes, and the simplifier. Carsten Clasohm and Markus Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann also helped. 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 EPSRC (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG Schwerpunktprogramm \emph{Deduktion}. \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{../manual} \printindex \end{document}