\chapter{Generic Tools and Packages}\label{ch:gen-tools}
\section{Basic proof methods}\label{sec:pure-meth}
\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
\indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
\indexisarmeth{rule}\indexisarmeth{erule}
\begin{matharray}{rcl}
fail & : & \isarmeth \\
succeed & : & \isarmeth \\
- & : & \isarmeth \\
assumption & : & \isarmeth \\
finish & : & \isarmeth \\
fold & : & \isarmeth \\
unfold & : & \isarmeth \\
rule & : & \isarmeth \\
erule^* & : & \isarmeth \\
\end{matharray}
\begin{rail}
('fold' | 'unfold' | 'rule' | 'erule') thmrefs
;
\end{rail}
\begin{descr}
\item [$ $]
\end{descr}
FIXME
%FIXME sort
%FIXME thmref (single)
%FIXME var vs. term
\section{Miscellaneous attributes}
\indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
\indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
\indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
\begin{matharray}{rcl}
tag & : & \isaratt \\
untag & : & \isaratt \\
COMP & : & \isaratt \\
RS & : & \isaratt \\
OF & : & \isaratt \\
where & : & \isaratt \\
of & : & \isaratt \\
standard & : & \isaratt \\
elimify & : & \isaratt \\
transfer & : & \isaratt \\
export & : & \isaratt \\
\end{matharray}
\begin{rail}
('tag' | 'untag') (nameref+)
;
\end{rail}
\begin{rail}
('COMP' | 'RS') nat? thmref
;
'OF' thmrefs
;
\end{rail}
\begin{rail}
'where' (name '=' term * 'and')
;
'of' (inst * ) ('concl' ':' (inst * ))?
;
inst: underscore | term
;
\end{rail}
\begin{descr}
\item [$ $]
\end{descr}
FIXME
\section{Calculational proof}\label{sec:calculation}
\indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}
\begin{matharray}{rcl}
\isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
\isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
trans & : & \isaratt \\
\end{matharray}
Calculational proof is forward reasoning with implicit application of
transitivity rules (such those of $=$, $\le$, $<$). Isabelle/Isar maintains
an auxiliary register $calculation$\indexisarreg{calculation} for accumulating
results obtained by transitivity obtained together with the current facts.
Command $\ALSO$ updates $calculation$ from the most recent result, while
$\FINALLY$ exhibits the final result by forward chaining towards the next goal
statement. Both commands require valid current facts, i.e.\ may occur only
after commands that produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or
some finished $\HAVENAME$ or $\SHOWNAME$.
Also note that the automatic term abbreviation ``$\dots$'' has its canonical
application with calculational proofs. It automatically refers to the
argument\footnote{The argument of a curried infix expression is its right-hand
side.} of the preceding statement.
Isabelle/Isar calculations are implicitly subject to block structure in the
sense that new threads of calculational reasoning are commenced for any new
block (as opened by a local goal, for example). This means that, apart from
being able to nest calculations, there is no separate \emph{begin-calculation}
command required.
\begin{rail}
('also' | 'finally') transrules? comment?
;
'trans' (() | 'add' ':' | 'del' ':') thmrefs
;
transrules: '(' thmrefs ')' interest?
;
\end{rail}
\begin{descr}
\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
follows. The first occurrence of $\ALSO$ in some calculational thread
initialises $calculation$ by $facts$. Any subsequent $\ALSO$ on the
\emph{same} level of block-structure updates $calculation$ by some
transitivity rule applied to $calculation$ and $facts$ (in that order).
Transitivity rules are picked from the current context plus those given as
$thms$ (the latter have precedence).
\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
$\ALSO$, and concludes the current calculational thread. The final result
is exhibited as fact for forward chaining towards the next goal. Basically,
$\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. A typical proof
idiom is $\FINALLY~\SHOW~\VVar{thesis}~\DOT$.
\item [Attribute $trans$] maintains the set of transitivity rules of the
theory or proof context, by adding or deleting the theorems provided as
arguments. The default is adding of rules.
\end{descr}
See theory \texttt{HOL/Isar_examples/Group} for a simple applications of
calculations for basic equational reasoning.
\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
calculational steps in combination with natural deduction.
\section{Axiomatic Type Classes}\label{sec:axclass}
\indexisarcmd{axclass}\indexisarcmd{instance}
\begin{matharray}{rcl}
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
expand_classes & : & \isarmeth \\
\end{matharray}
Axiomatic type classes are provided by Isabelle/Pure as a purely
\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}). Thus
any object logic may make use of this light-weight mechanism for abstract
theories. See \cite{Wenzel:1997:TPHOL} for more information. There is also a
tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
the standard Isabelle documentation.
\begin{rail}
'axclass' classdecl (axmdecl prop comment? +)
;
'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
;
\end{rail}
\begin{descr}
\item [$\isarkeyword{axclass}~$] FIXME
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
c@2$] setup up a goal stating the class relation or type arity. The proof
would usually proceed by the $expand_classes$ method, and then establish the
characteristic theorems of the type classes involved. After finishing the
proof the theory will be augmented by a type signature declaration
corresponding to the resulting theorem.
\item [Method $expand_classes$] iteratively expands the class introduction
rules
\end{descr}
See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
axiomatic type classes, including instantiation proofs.
\section{The Simplifier}
\subsection{Simplification methods}
\indexisarmeth{simp}\indexisarmeth{asm_simp}\indexisaratt{simp}
\begin{matharray}{rcl}
simp & : & \isarmeth \\
asm_simp & : & \isarmeth \\
simp & : & \isaratt \\
\end{matharray}
\begin{rail}
'simp' (simpmod * )
;
simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
;
\end{rail}
FIXME
\subsection{Forward simplification}
\indexisaratt{simplify}\indexisaratt{asm_simplify}\indexisaratt{full_simplify}\indexisaratt{asm_full_simplify}
\begin{matharray}{rcl}
simplify & : & \isaratt \\
asm_simplify & : & \isaratt \\
full_simplify & : & \isaratt \\
asm_full_simplify & : & \isaratt \\
\end{matharray}
FIXME
\section{The Classical Reasoner}
\subsection{Single step methods}
\subsection{Automatic methods}
\subsection{Combined automatic methods}
\subsection{Modifying the context}
%\indexisarcmd{}
%\begin{matharray}{rcl}
% \isarcmd{} & : & \isartrans{}{} \\
%\end{matharray}
%\begin{rail}
%\end{rail}
%\begin{descr}
%\item [$ $]
%\end{descr}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"
%%% End: