diff -r 55d32e76ef4e -r 531f1f524848 doc-src/TutorialI/IsarOverview/Isar/document/root.tex --- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Mon Sep 30 16:48:15 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Mon Sep 30 16:50:39 2002 +0200 @@ -10,23 +10,162 @@ \begin{document} -\title{A Compact Overview of Structured Proofs in Isar/HOL} +\title{A Compact Introduction to Structured Proofs in Isar/HOL} \author{Tobias Nipkow\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\ {\small\url{http://www.in.tum.de/~nipkow/}}} \date{} \maketitle -\noindent -Isar is an extension of Isabelle with structured proofs in a -stylized language of mathematics. These proofs are readable for both a human -and a machine. +\begin{abstract} + Isar is an extension of the theorem prover Isabelle with a language + for writing human-readable structured proofs. This paper is an + introduction to the basic constructs of this language. It is aimed + at potential users of Isar but also discusses the design rationals + behind the language and its constructs. +\end{abstract} + +\section{Introduction} + +Isar is an extension of Isabelle with structured proofs in a stylized +language of mathematics. These proofs are readable for both a human +and a machine. This document is a very compact introduction to +structured proofs in Isar/HOL, an extension of +Isabelle/HOL~\cite{LNCS2283}. We intentionally do not present the full +language but concentrate on the essentials. Neither do we give a +formal semantics of Isar. Instead we introduce Isar by example. Again +this is intentional: we believe that the language ``speaks for +itself'' in the same way that traditional mathamtical proofs do, which +are also introduced by example rather than by teaching students logic +first. A detailed exposition of Isar can be found in Markus Wenzel's +PhD thesis~\cite{Wenzel-PhD} and the Isar reference +manual~\cite{Isar-Ref-Man}. + +\subsection{Background} + +Interactive theorem proving has been dominated by a model of proof +that goes back to the LCF system~\cite{LCF}: a proof is a more or less +structured sequence of commands that manipulate an implicit proof +state. Thus the proof proof text is only suitable for the machine; for +a human, the proof only comes alive when he can see the state changes +caused by the stepwise execution of the commands. Such a proof is like +an uncommented assembly language program. We call them +\emph{tactic-style} proofs because LCF proof-commands were called +tactics. + +A radically different approach was taken by the Mizar +system~\cite{Mizar} where proofs are written a stylized language akin +to that used in ordinary mathematics texts. The most important +argument in favour of a mathematics-like proof language is +communication: as soon as not just the theorem but also the proof +becomes an object of interest, it should be readable as it is. From a +system development point of view there is a second important argument +against tactic-style proofs: they are much harder to maintain when the +system is modified. The reason is as follows. Since it is usually +quite unclear what exactly is proved at some point in the middle of a +command sequence, updating a failed proof often requires executing the +proof up to the point of failure using the old version of the system. +In contrast, mathematics-like proofs contain enough information +to tell you what is proved at any point. + +For these reasons the Isabelle system, originally firmly in the +LCF-tradition, was extended with a language for writing structured +proofs in a mathematics-like style. As the name already indicates, +Isar was certainly inspired by Mizar. However, there are very many +differences. For a start, Isar is generic: only a few of the language +constructs described below are specific to HOL; many are generic and +thus available for any logic defined in Isabelle, e.g.\ ZF. +Furthermore, we have Isabelle's powerful automatic proof procedures +(e.g.\ simplification and a tableau-style prover) at our disposal. +A closer comparison of Isar and Mizar can be found +elsewhere~\cite{Isar-Mizar}. -This document is a very compact introduction to structured proofs in -Isar/HOL, an extension of Isabelle/HOL~\cite{LNCS2283}. A detailed -exposition of this material can be found in Markus Wenzel's PhD -thesis~\cite{Wenzel-PhD} and the Isar reference manual~\cite{Isar-Ref-Man}. +Finally, a word of warning for potential writers of structured Isar +proofs. It has always been easier to write obscure rather than +readable texts. Similarly, tactic-based proofs are often (though by no +means always!) easier to write than readable ones: structure does not +emerge automatically but needs to be understood and imposed. If the +precise structure of the proof is not clear from the beginning, it can +be useful to start in a tactic-based style for exploratory purposes +until one has found a proof which can then be converted into a +structured text in a second step. Top down conversion is possible +because Isar allows tactic-based proofs as components of structured +ones. + +\subsection{An overview of the Isar syntax} + +We begin by looking at a simplified grammar for Isar proofs +where parentheses are used for grouping and $^?$ indicates an optional item: +\begin{center} +\begin{tabular}{lrl} +\emph{proof} & ::= & \isakeyword{proof} \emph{method}$^?$ + \emph{statement}* + \isakeyword{qed} \\ + &$\mid$& \isakeyword{by} \emph{method}\\[1ex] +\emph{statement} &::= & \isakeyword{fix} \emph{variables} \\ + &$\mid$& \isakeyword{assume} \emph{propositions} \\ + &$\mid$& (\isakeyword{from} \emph{facts})$^?$ + (\isakeyword{show} $\mid$ \isakeyword{have}) + \emph{propositions} \emph{proof} \\[1ex] +\emph{proposition} &::=& (\emph{label}{\bf:})$^?$ \emph{string} \\[1ex] +\emph{fact} &::=& \emph{label} +\end{tabular} +\end{center} +A proof can be either compound (\isakeyword{proof} -- +\isakeyword{qed}) or atomic (\isakeyword{by}). A \emph{method} is a +proof method offered by the underlying theorem prover, for example +\isa{rule} or \isa{simp} in Isabelle. Thus this grammar is +generic both w.r.t.\ the logic and the theorem prover. + +This is a typical proof skeleton: +\begin{center} +\begin{tabular}{@{}ll} +\isakeyword{proof}\\ +\hspace*{3ex}\isakeyword{assume} \isa{"}\emph{the-assm}\isa{"}\\ +\hspace*{3ex}\isakeyword{have} \isa{"}\dots\isa{"} & --- intermediate result\\ +\hspace*{3ex}\vdots\\ +\hspace*{3ex}\isakeyword{have} \isa{"}\dots\isa{"} & --- intermediate result\\ +\hspace*{3ex}\isakeyword{show} \isa{"}\emph{the-concl}\isa{"}\\ +\isakeyword{qed} +\end{tabular} +\end{center} +It proves \emph{the-assm}~$\Longrightarrow$~\emph{the-concl}. Text starting with +``---'' is a comment. The intermediate \isakeyword{have}s are only +there to bridge the gap between the assumption and the conclusion and +do not contribute to the theorem being proved. In contrast, +\isakeyword{show} establishes the conclusion of the theorem. + +As a final bit of syntax note that \emph{propositions} (following +\isakeyword{assume} etc) may but need not be separated by +\isakeyword{and}, whose purpose is to structure them into possibly +named blocks. For example in +\begin{center} +\isakeyword{assume} \isa{A:} $A_1$ $A_2$ \isakeyword{and} \isa{B:} $A_3$ +\isakeyword{and} $A_4$ +\end{center} +label \isa{A} refers to the list of propositions $A_1$ $A_2$ and +label \isa{B} to $A_3$. + +\subsection{Overview of the paper} + +The rest of the paper is divided into two parts. +Section~\ref{sec:Logic} introduces proofs in pure logic based on +natural deduction. Section~\ref{sec:Induct} is dedicated to induction, +the key reasoning principle for computer science applications. + +There are at least two further areas where Isar provides specific +support, but which we do not document here: reasoning by chains of +(in)equations is described elsewhere~\cite{BauerW-TPHOL}, whereas +reasoning about axiomatically defined structures by means of so called +``locales'' \cite{BallarinPW-TPHOL} is only described in a very early +form and has evolved much since then. + +Do not be mislead by the simplicity of the formulae being proved, +especially in the beginning. Isar has been used very successfully in +large applications, for example the formalization of Java, in +particular the verification of the bytecode verifier~\cite{KleinN-TCS}. \input{Logic.tex} +\input{Induction.tex} %\input{Isar.tex}