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