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