doc-src/IsarRef/generic.tex

checkpoint;

\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)} \\
\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.
\end{descr}



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


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