doc-src/IsarRef/generic.tex
author wenzelm
Wed Aug 04 18:20:24 1999 +0200 (1999-08-04)
changeset 7175 8263d0b50e12
parent 7167 0b2e3ef1d8f4
child 7315 76a39a3784b5
permissions -rw-r--r--
tuned;
     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 \end{rail}
    57 
    58 \begin{rail}
    59   ('COMP' | 'RS') nat? thmref
    60   ;
    61   'OF' thmrefs
    62   ;
    63 \end{rail}
    64 
    65 \begin{rail}
    66   'where' (name '=' term * 'and')
    67   ;
    68   'of' (inst * ) ('concl' ':' (inst * ))?
    69   ;
    70 
    71   inst: underscore | term
    72   ;
    73 \end{rail}
    74 
    75 \begin{descr}
    76 \item [$ $]
    77 \end{descr}
    78 
    79 FIXME
    80 
    81 \section{Axiomatic Type Classes}\label{sec:axclass}
    82 
    83 \indexisarcmd{axclass}\indexisarcmd{instance}
    84 \begin{matharray}{rcl}
    85   \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
    86   \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
    87 \end{matharray}
    88 
    89 Axiomatic type classes are provided by Isabelle/Pure as a purely
    90 \emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}).  Thus
    91 any object logic may make use of this light-weight mechanism for abstract
    92 theories.  See \cite{Wenzel:1997:TPHOL} for more information.  There is also a
    93 tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
    94 the standard Isabelle documentation.
    95 
    96 \begin{rail}
    97   'axclass' classdecl (axmdecl prop comment? +)
    98   ;
    99   'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
   100   ;
   101 \end{rail}
   102 
   103 \begin{descr}
   104 \item [$\isarkeyword{axclass}~$] FIXME
   105 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
   106   c@2$] setup up a goal stating the class relation or type arity.  The proof
   107   would usually proceed by the $expand_classes$ method, and then establish the
   108   characteristic theorems of the type classes involved.  After finishing the
   109   proof the theory will be augmented by a type signature declaration
   110   corresponding to the resulting theorem.
   111 \end{descr}
   112 
   113 
   114 
   115 \section{The Simplifier}
   116 
   117 \section{The Classical Reasoner}
   118 
   119 
   120 %\indexisarcmd{}
   121 %\begin{matharray}{rcl}
   122 %  \isarcmd{} & : & \isartrans{}{} \\
   123 %\end{matharray}
   124 
   125 %\begin{rail}
   126   
   127 %\end{rail}
   128 
   129 %\begin{descr}
   130 %\item [$ $]
   131 %\end{descr}
   132 
   133 
   134 %%% Local Variables: 
   135 %%% mode: latex
   136 %%% TeX-master: "isar-ref"
   137 %%% End: