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

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