--- 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}