doc-src/IsarRef/generic.tex

tuned;

\chapter{Generic Tools and Packages}\label{ch:gen-tools}

\section{Basic proof methods and attributes}\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

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

\section{The Classical Reasoner}


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