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

(adjustions)

\section{Introduction}

Isabelle is a generic proof assistant.  Isar is an extension of
Isabelle with structured proofs in a stylised language of mathematics.
These proofs are readable for both a human and a machine.
Isabelle/HOL~\cite{LNCS2283} is a specialisation of Isabelle with
higher-order logic (HOL). This paper is a compact introduction to
structured proofs in Isar/HOL, an extension of Isabelle/HOL. 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. 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} (which also discusses related
work) 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 stylised 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}.

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

We recall some basic notions and notation from Isabelle. For more
details and for instructions how to run examples see
elsewhere~\cite{LNCS2283}.

Isabelle's meta-logic comes with a type of \emph{propositions} with
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. HOL formulae are propositions, e.g.\ $\forall$ can appear below
$\Longrightarrow$, but not the other way around. Beware that $\longrightarrow$ binds more
tightly than $\Longrightarrow$: in $\forall x. P \longrightarrow Q$ the $\forall x$ covers $P \longrightarrow Q$, whereas
in $\forall x. P \Longrightarrow Q$ it covers only $P$.

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

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 unclear at beginning, it can be useful to
start in a tactic-based style for exploratory purposes until one has
found a proof which can 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.

%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 formalisation of Java, in
%particular the verification of the bytecode verifier~\cite{KleinN-TCS}.