%\section{Isabelle}

Isabelle \cite{paulson-700} is an interactive computer-based proof system.
%described in \cite{isabelle-intro} and \cite{isabelle-ref}.
It is written in Standard ML, and
when it is running, the user can interact with it by
entering further ML commands.

It has the unusual feature that it can be used with the user's own choice of
logical system and syntax, for very little is built in.
The built-in logic is intuitionistic higher-order logic,
with the operators 
\texttt{==>} (implication, or deducibility),
\texttt{==} (equality, or substitutibility), and
\texttt{!!} (universal quantification).
These operators have only the properties necessary to support their
intended meanings.
For example, since
\mbox{\texttt{[| P; Q |]~==>~R}}
means that \texttt R can be deduced from \texttt P and \texttt Q,
it follows that
\mbox{\texttt{[|~P~==>~Q;~P~|] ==> Q},} and that
{\par\noindent\centering
\texttt{([| P; Q |] ==> R) ==> ([| Q; P |] ==> R)}.
\par\noindent}
Likewise, since 
\texttt{P == Q}
means that \texttt P can be replaced by \texttt Q, or vice versa,
\texttt{==} is reflexive, symmetric and transitive.
Anything that can be proved using this built-in logic is a theorem
of Isabelle,
of ML type \texttt{thm}.
To avoid confusion we consistently use ``thm'' when speaking of Isabelle
theorems and use ``theorem'' when speaking of the object logic \Kt.

The user then has to define an object-level logic and syntax,
though normally one would use one of
several which are packaged with the Isabelle distribution.
%\cite{isabelle-object}.
One of these is LK, which is first order logic using the Gentzen sequent
calculus.
In LK, `$\vdash$' is treated as an object-level operator,
and object-level propositions are of the form $\Gamma \vdash \Delta$,
where $\Gamma$ and $\Delta$ are sequences of formulae.

Isabelle uses the strong typing of ML to prevent the user from `proving'
results other than by the inference steps permitted;
only these steps can produce an Isabelle thm.
Naturally the primitive built in inference steps can be combined, both in
the more powerful functions provided in Isabelle, or by the user
programming more complex proof functions in ML.

The user asserts a set of `axioms' in a `theory file', where 
the syntax of the object-logic is also specified.
Isabelle treats these axioms as thms.

\label{isathm}
%In many object-logics the theorems one typically wishes to prove are
%expressible entirely using the constructs of that object-logic;
%in other cases one may often want to prove theorems 
Isabelle thms (including the axioms of the theory)
may or may not involve Isabelle's metalogical operators.
%for example, a result of the form \texttt{([| P; Q |] ==> R)}.
Thus, in the Isabelle implementation of Display Logic, an Isabelle thm
may be either a `simple' sequent of \dKt, of the form $X \vdash Y$,
or a sequent \bfi{rule}, such as those in \fig{logical-rules-dkt}.
The uni-directional and bi-directional rules 
correspond to Isabelle thms containing
the operators \texttt{==>} (meta-implication) or \texttt{==} (meta-equality)
respectively.
%For example, the (cut) rule appears as
%{\par\noindent\centering
%\texttt{"[| \$?X |- ?A; ?A |- \$?Y |] ==> \$?X |- \$?Y"}
%\par\noindent}
%in Isabelle. 
%(The `\verb:?:' denotes a variable which can be instantiated,
%and the `\verb:$:' denotes a structural variable or constant.)
%The variant $A \vdash A$ of the (id) rule (see \S\ref{otm})
%appears as \texttt{"?A |- ?A"}.
%The bi-directional \texttt{sA} rule, shown in \fig{dps},
%appears as \texttt{"* \$?X |- \$?Y == * \$?Y |- \$?X"}.

Isabelle provides a number of basic proof steps for
backwards proof (\textbf{tactics}\index{tactic|textbf}), as well as 
functions for combining these in various ways 
(\textbf{tacticals}\index{tactical|textbf}).
Isabelle automatically keeps track of the subgoals generated by this backward
search procedure and the user can choose to work on any subgoal.
The user can also write complex proof tactics in ML;
many complex tactics and tacticals are supplied with
Isabelle or its standard object logics.
%and there are some which are applicable
%to most or all object logics. 
Some tactics are designed for a more automated style of proof search;
they will repeatedly attempt a large number of tactics.
Others, for example \texttt{rtac}, are designed more for interactive use,
when the user can see what proof steps are needed.
Thus \texttt{rtac} \textit{th sg} attempts to match the conclusion of 
thm \textit{th} to subgoal number \textit{sg} -- if it succeeds,
it will replace that subgoal by the premises (if any) of \textit{th}.

Isabelle also supports forward proof; % a function commonly used is
%\texttt{RS} (which is binary infix);
%for example, if \textit{th} is a rule with a single premise,
%\textit{thsf}~\texttt{RS}~\textit{th} 
%in effect uses the rule \textit{th} 
%to transform the conclusion of \textit{thsf}.
%More precisely, if 
%\textit{thsf} is $A' \texttt{==>} B'$,
%and \textit{th} is $B'' \texttt{==>} C''$,
%and the most general unifier of $B'$ and $B''$ is $\theta$,
%(so $ B' \theta = B'' \theta$)
%taking these to 
%$A' \theta \texttt{==>} B' \theta$ and 
%$B'' \theta \texttt{==>} C'' \theta$,
%then \textit{thsf} \texttt{RS} \textit{th} is 
%$A' \theta \texttt{==>} C'' \theta$.
for example, if $A' \texttt{==>} B'$ and $B'' \texttt{==>} C''$ are thms, 
and the most general unifier of $B'$ and $B''$ is $\theta$,
(so $ B' \theta = B'' \theta$)
then Isabelle can derive the thm 
$A' \theta \texttt{==>} C'' \theta$.