\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym,pdfsetup}
%for best-style documents ...
\urlstyle{rm}
%\isabellestyle{it}
\newtheorem{Exercise}{Exercise}[section]
\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
\begin{document}
\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
\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}.
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}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
{\small
\paragraph{Acknowledgment}
I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin,
Gertrud Bauer, Stefan Berghofer, Gerwin Klein, Norbert Schirmer and
Markus Wenzel commented on and improved this document.
}
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{root}
\endgroup
\end{document}