doc-src/TutorialI/IsarOverview/Isar/document/intro.tex

*** empty log message ***

\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 mathematical 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 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 proofs are like
uncommented assembly language programs. 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{Rudnicki92} where proofs are written in 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.  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 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 at
our disposal.  A closer comparison of Isar and Mizar can be found
elsewhere~\cite{WenzelW-JAR}.

Finally, a word of warning for potential writers of Isar proofs.  It
has always been easier to write obscure rather than readable texts.
Similarly, tactic-style 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-style proofs as components of structured ones.

\subsection{A first glimpse of Isar}

Below you find a simplified grammar for Isar proofs.
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 (tactic) offered by the underlying theorem prover.
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.

\subsection{Bits of Isabelle}

In order to make this paper self-contained we recall some basic
notions and notation from Isabelle~\cite{LNCS2283}. Isabelle's
meta-logic offers an implication $\Longrightarrow$ and a universal quantifier $\bigwedge$
for expressing inference rules and generality. Iterated implications
$A_1 \Longrightarrow \dots A_n \Longrightarrow A$ may be abbreviated to $[\![ A_1; \dots; A_n
]\!] \Longrightarrow A$. Applying a theorem $A \Longrightarrow B$ (named \isa{T}) to a theorem
$A$ (named \isa{U}) is written \isa{T[OF U]} and yields theorem $B$.

Isabelle terms are simply typed. Function types are
written $\tau_1 \Rightarrow \tau_2$.

Free variables that may be instantiated (``logical variables'' in Prolog
parlance) are prefixed with a \isa{?}. Typically, theorems are stated with
ordinary free variables but after the proof those are automatically replaced
by \isa{?}-variables. Thus the theorem can be used with arbitrary instances
of its free variables.

Isabelle/HOL offers all the usual logical symbols like $\longrightarrow$, $\land$,
$\forall$ etc. Proof methods include \isa{rule} (which performs a backwards
step with a given rule, unifying the conclusion of the rule with the
current subgoal and replacing the subgoal by the premises of the
rule), \isa{simp} (for simplification) and \isa{blast} (for predicate
calculus reasoning).

\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-TPHOLs01}.  Reasoning about axiomatically
defined structures by means of so called ``locales'' was first described in
\cite{KWP-TPHOLs99} but 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}.