1.1 --- a/doc-src/IsarRef/generic.tex Thu Sep 07 20:12:08 2006 +0200
1.2 +++ b/doc-src/IsarRef/generic.tex Fri Sep 08 13:33:11 2006 +0200
1.3 @@ -1,4 +1,3 @@
1.4 -
1.5 \chapter{Generic tools and packages}\label{ch:gen-tools}
1.6
1.7 \section{Theory specification commands}
1.8 @@ -103,59 +102,6 @@
1.9 instantiation.
1.10
1.11
1.12 -\subsection{Axiomatic type classes}\label{sec:axclass}
1.13 -
1.14 -\indexisarcmd{axclass}\indexisarmeth{intro-classes}
1.15 -\begin{matharray}{rcl}
1.16 - \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
1.17 - \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
1.18 - intro_classes & : & \isarmeth \\
1.19 -\end{matharray}
1.20 -
1.21 -Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
1.22 -interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic
1.23 -may make use of this light-weight mechanism of abstract theories
1.24 -\cite{Wenzel:1997:TPHOL}. There is also a tutorial on using axiomatic type
1.25 -classes in Isabelle \cite{isabelle-axclass} that is part of the standard
1.26 -Isabelle documentation.
1.27 -
1.28 -\begin{rail}
1.29 - 'axclass' classdecl (axmdecl prop +)
1.30 - ;
1.31 - 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
1.32 - ;
1.33 -\end{rail}
1.34 -
1.35 -\begin{descr}
1.36 -
1.37 -\item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
1.38 - the intersection of existing classes, with additional axioms holding. Class
1.39 - axioms may not contain more than one type variable. The class axioms (with
1.40 - implicit sort constraints added) are bound to the given names. Furthermore
1.41 - a class introduction rule is generated (being bound as
1.42 - $c_class{\dtt}intro$); this rule is employed by method $intro_classes$ to
1.43 - support instantiation proofs of this class.
1.44 -
1.45 - The ``axioms'' are stored as theorems according to the given name
1.46 - specifications, adding the class name $c$ as name space prefix; the same
1.47 - facts are also stored collectively as $c_class{\dtt}axioms$.
1.48 -
1.49 -\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a
1.50 - goal stating a class relation or type arity. The proof would usually
1.51 - proceed by $intro_classes$, and then establish the characteristic theorems
1.52 - of the type classes involved. After finishing the proof, the theory will be
1.53 - augmented by a type signature declaration corresponding to the resulting
1.54 - theorem.
1.55 -
1.56 -\item [$intro_classes$] repeatedly expands all class introduction rules of
1.57 - this theory. Note that this method usually needs not be named explicitly,
1.58 - as it is already included in the default proof step (of $\PROOFNAME$ etc.).
1.59 - In particular, instantiation of trivial (syntactic) classes may be performed
1.60 - by a single ``$\DDOT$'' proof step.
1.61 -
1.62 -\end{descr}
1.63 -
1.64 -
1.65 \subsection{Locales and local contexts}\label{sec:locale}
1.66
1.67 Locales are named local contexts, consisting of a list of declaration elements
1.68 @@ -482,10 +428,10 @@
1.69 \end{warn}
1.70
1.71
1.72 -\subsection{Constructive type classes}
1.73 +\subsection{Type classes}
1.74
1.75 -A special case of locales are constructive type classes.
1.76 -Constructive type classes
1.77 +A special case of locales are type classes.
1.78 +Type classes
1.79 consist of a locale with \emph{exactly one} type variable
1.80 and an corresponding axclass.
1.81
1.82 @@ -555,6 +501,60 @@
1.83 \end{descr}
1.84
1.85
1.86 +\subsection{Axiomatic type classes}\label{sec:axclass}
1.87 +
1.88 +\indexisarcmd{axclass}\indexisarmeth{intro-classes}
1.89 +\begin{matharray}{rcl}
1.90 + \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
1.91 + \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
1.92 + intro_classes & : & \isarmeth \\
1.93 +\end{matharray}
1.94 +
1.95 +Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
1.96 +interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic
1.97 +may make use of this light-weight mechanism of abstract theories
1.98 +\cite{Wenzel:1997:TPHOL}. There is also a tutorial on using axiomatic type
1.99 +classes in Isabelle \cite{isabelle-axclass} that is part of the standard
1.100 +Isabelle documentation.
1.101 +
1.102 +\begin{rail}
1.103 + 'axclass' classdecl (axmdecl prop +)
1.104 + ;
1.105 + 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
1.106 + ;
1.107 +\end{rail}
1.108 +
1.109 +\begin{descr}
1.110 +
1.111 +\item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
1.112 + the intersection of existing classes, with additional axioms holding. Class
1.113 + axioms may not contain more than one type variable. The class axioms (with
1.114 + implicit sort constraints added) are bound to the given names. Furthermore
1.115 + a class introduction rule is generated (being bound as
1.116 + $c_class{\dtt}intro$); this rule is employed by method $intro_classes$ to
1.117 + support instantiation proofs of this class.
1.118 +
1.119 + The ``axioms'' are stored as theorems according to the given name
1.120 + specifications, adding the class name $c$ as name space prefix; the same
1.121 + facts are also stored collectively as $c_class{\dtt}axioms$.
1.122 +
1.123 +\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a
1.124 + goal stating a class relation or type arity. The proof would usually
1.125 + proceed by $intro_classes$, and then establish the characteristic theorems
1.126 + of the type classes involved. After finishing the proof, the theory will be
1.127 + augmented by a type signature declaration corresponding to the resulting
1.128 + theorem.
1.129 +
1.130 +\item [$intro_classes$] repeatedly expands all class introduction rules of
1.131 + this theory. Note that this method usually needs not be named explicitly,
1.132 + as it is already included in the default proof step (of $\PROOFNAME$ etc.).
1.133 + In particular, instantiation of trivial (syntactic) classes may be performed
1.134 + by a single ``$\DDOT$'' proof step.
1.135 +
1.136 +\end{descr}
1.137 +
1.138 +
1.139 +
1.140 \section{Derived proof schemes}
1.141
1.142 \subsection{Generalized elimination}\label{sec:obtain}