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

prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);

\section{Introduction}

This is a tutorial introduction to structured proofs in Isabelle/HOL.
It introduces the core of the proof language Isar by example. Isar is
an extension of the \isa{apply}-style proofs introduced in the
Isabelle/HOL tutorial~\cite{LNCS2283} with structured proofs in a
stylised language of mathematics.  These proofs are readable for both
human and machine.

\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{fact}*)$^?$ 
                    (\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.

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{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. Their Isabelle incarnation are
sequences of \isa{apply}-commands.

In contrast there is the model of a mathematics-like proof language
pioneered in the Mizar system~\cite{Rudnicki92} and followed by
Isar~\cite{WenzelW-JAR}.
The most important arguments in favour of this style are
\emph{communication} and \emph{maintainance}: structured proofs are
immensly more readable and maintainable than \isa{apply}-scripts.

For reading this tutorial you should be familiar with natural
deduction and the basics of Isabelle/HOL~\cite{LNCS2283} although we
summarize the most important aspects of Isabelle below.  The
definitive Isar reference is its manual~\cite{Isar-Ref-Man}. For an
example-based account of Isar's support for reasoning by chains of
(in)equations see~\cite{BauerW-TPHOLs01}.


\subsection{Bits of Isabelle}

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

A word of warning for potential writers of Isar proofs.  It
is easier to write obscure rather than readable texts.  Similarly,
\isa{apply}-style proofs are sometimes 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 with \isa{apply} 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 \isa{apply}-style proofs as components
of structured ones.

Finally, 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
dialects~\cite{KleinN-TOPLAS}.
\medskip

The rest of this tutorial 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.