doc-src/IsarRef/generic.tex
author wenzelm
Tue Aug 03 18:56:51 1999 +0200 (1999-08-03)
changeset 7167 0b2e3ef1d8f4
parent 7141 a67dde8820c0
child 7175 8263d0b50e12
permissions -rw-r--r--
tuned;
much more material;
     1 
     2 \chapter{Generic Tools and Packages}\label{ch:gen-tools}
     3 
     4 \section{Basic proof methods and attributes}\label{sec:pure-meth}
     5 
     6 \indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
     7 \indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
     8 \indexisarmeth{rule}\indexisarmeth{erule}
     9 \begin{matharray}{rcl}
    10   fail & : & \isarmeth \\
    11   succeed & : & \isarmeth \\
    12   - & : & \isarmeth \\
    13   assumption & : & \isarmeth \\
    14   finish & : & \isarmeth \\
    15   fold & : & \isarmeth \\
    16   unfold & : & \isarmeth \\
    17   rule & : & \isarmeth \\
    18   erule^* & : & \isarmeth \\
    19 \end{matharray}
    20 
    21 \begin{rail}
    22   ('fold' | 'unfold' | 'rule' | 'erule') thmrefs
    23   ;
    24 \end{rail}
    25 
    26 \begin{descr}
    27 \item [$ $]
    28 \end{descr}
    29 
    30 FIXME
    31 
    32 %FIXME sort
    33 %FIXME thmref (single)
    34 %FIXME var vs. term
    35 
    36 \indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
    37 \indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
    38 \indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
    39 \begin{matharray}{rcl}
    40   tag & : & \isaratt \\
    41   untag & : & \isaratt \\
    42   COMP & : & \isaratt \\
    43   RS & : & \isaratt \\
    44   OF & : & \isaratt \\
    45   where & : & \isaratt \\
    46   of & : & \isaratt \\
    47   standard & : & \isaratt \\
    48   elimify & : & \isaratt \\
    49   transfer & : & \isaratt \\
    50   export & : & \isaratt \\
    51 \end{matharray}
    52 
    53 \begin{rail}
    54   ('tag' | 'untag') (nameref+)
    55   ;
    56   ('COMP' | 'RS') nat? thmref
    57   ;
    58   'OF' thmrefs
    59   ;
    60   'where' (term '=' term * 'and')
    61   ;
    62   'of' (inst * ) ('concl:' (inst * ))?
    63   ;
    64 
    65   inst: underscore | term
    66   ;
    67 \end{rail}
    68 
    69 \begin{descr}
    70 \item [$ $]
    71 \end{descr}
    72 
    73 FIXME
    74 
    75 \section{Axiomatic Type Classes}\label{sec:axclass}
    76 
    77 \indexisarcmd{axclass}\indexisarcmd{instance}
    78 \begin{matharray}{rcl}
    79   \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
    80   \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
    81 \end{matharray}
    82 
    83 Axiomatic type classes are provided by Isabelle/Pure as a purely
    84 \emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}).  Thus
    85 any object logic may make use of this light-weight mechanism for abstract
    86 theories.  See \cite{Wenzel:1997:TPHOL} for more information.  There is also a
    87 tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
    88 the standard Isabelle documentation.
    89 
    90 \begin{rail}
    91   'axclass' classdecl (axmdecl prop comment? +)
    92   ;
    93   'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
    94   ;
    95 \end{rail}
    96 
    97 \begin{descr}
    98 \item [$\isarkeyword{axclass}~$] FIXME
    99 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
   100   c@2$] setup up a goal stating the class relation or type arity.  The proof
   101   would usually proceed by the $expand_classes$ method, and then establish the
   102   characteristic theorems of the type classes involved.  After finishing the
   103   proof the theory will be augmented by a type signature declaration
   104   corresponding to the resulting theorem.
   105 \end{descr}
   106 
   107 
   108 
   109 \section{The Simplifier}
   110 
   111 \section{The Classical Reasoner}
   112 
   113 
   114 %\indexisarcmd{}
   115 %\begin{matharray}{rcl}
   116 %  \isarcmd{} & : & \isartrans{}{} \\
   117 %\end{matharray}
   118 
   119 %\begin{rail}
   120   
   121 %\end{rail}
   122 
   123 %\begin{descr}
   124 %\item [$ $]
   125 %\end{descr}
   126 
   127 
   128 %%% Local Variables: 
   129 %%% mode: latex
   130 %%% TeX-master: "isar-ref"
   131 %%% End: