1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/AxClass/Makefile Mon May 12 17:53:36 1997 +0200
1.3 @@ -0,0 +1,23 @@
1.4 +# $Id$
1.5 +#########################################################################
1.6 +# #
1.7 +# Makefile for the report "Introduction to Isabelle" #
1.8 +# #
1.9 +#########################################################################
1.10 +
1.11 +
1.12 +FILES = axclass.tex style.tex
1.13 +
1.14 +axclass.dvi.gz: $(FILES)
1.15 + -rm axclass.dvi*
1.16 + latex axclass
1.17 + latex axclass
1.18 + gzip -f axclass.dvi
1.19 +
1.20 +dist: $(FILES)
1.21 + -rm axclass.dvi*
1.22 + latex axclass
1.23 + latex axclass
1.24 +
1.25 +clean:
1.26 + @rm *.aux *.log
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/AxClass/axclass.tex Mon May 12 17:53:36 1997 +0200
2.3 @@ -0,0 +1,747 @@
2.4 +
2.5 +\input{style}
2.6 +
2.7 +\begin{document}
2.8 +
2.9 +\title{Using Axiomatic Type Classes in Isabelle \\ a tutorial}
2.10 +\author{Markus Wenzel}
2.11 +%\date{29 August 1995}
2.12 +\maketitle
2.13 +
2.14 +\Isa\ features a \Haskell-like type system with ordered type classes
2.15 +already since 1991 (see \cite{Nipkow93}). Initially, classes mainly
2.16 +served as a \E{syntactic tool} to formulate polymorphic object logics
2.17 +in a clean way (like many-sorted \FOL, see
2.18 +\cite[\S1.1.2--1.1.3]{Paulson94}).
2.19 +
2.20 +Applying classes at the \E{logical level} to provide a simple notion
2.21 +of abstract theories and instantiations to concrete ones, has also
2.22 +been long proposed (see \cite{Nipkow-slides} and
2.23 +\cite[\S4]{Nipkow93}). At that time, \Isa\ still lacked built-in
2.24 +support for these \E{axiomatic type classes}. More importantly, their
2.25 +semantics was not yet fully fleshed out and unnecessarily complicated.
2.26 +
2.27 +How simple things really are has been shown in \cite[esp.\
2.28 +\S4]{Wenzel94} which also provided an implementation of the axclass
2.29 +package that was eventually released with \Isa94. Unfortunately there
2.30 +was a snag: That version of \Isa\ still contained an old conceptual
2.31 +bug in the core machinery which caused theories to become inconsistent
2.32 +after introducing empty sorts. Note that empty intersections of
2.33 +axiomatic type classes easily occur, unless all basic classes are very
2.34 +trivial.
2.35 +
2.36 +These problems prevented the axclass package to be used seriously ---
2.37 +they have been fixed in \Isa95.
2.38 +
2.39 +
2.40 +\section{Some simple examples} \label{sec:ex}
2.41 +
2.42 +Axiomatic type classes are a concept of \Isa's meta-logic. They may
2.43 +be applied to any object-logic that directly uses the meta type
2.44 +system. Subsequently, we present various examples that are formulated
2.45 +within \Isa/\HOL\footnote{See also directory
2.46 + \TT{HOL/AxClasses/Tutorial}.}, except the one of
2.47 +\secref{sec:ex-natclass} which is in \Isa/\FOL\footnote{See also files
2.48 + \TT{FOL/ex/NatClass.thy} and \TT{FOL/ex/NatClass.ML}.}.
2.49 +
2.50 +
2.51 +\subsection{Semigroups}
2.52 +
2.53 +An axiomatic type class is simply a class of types that all meet
2.54 +certain \E{axioms}. Thus, type classes may be also understood as type
2.55 +predicates --- i.e.\ abstractions over a single type argument
2.56 +$\alpha$. Class axioms typically contain polymorphic constants that
2.57 +depend on this type $\alpha$. These \E{characteristic constants}
2.58 +behave like operations associated with the ``carrier'' $\alpha$.
2.59 +
2.60 +We illustrate these basic concepts with the following theory
2.61 +\TT{Semigroup}:
2.62 +
2.63 +\begin{ascbox}
2.64 +Semigroup = HOL +\medskip
2.65 +consts
2.66 + "<*>" :: "['a, 'a] => 'a" (infixl 70)\medskip
2.67 +axclass
2.68 + semigroup < term
2.69 + assoc "(x <*> y) <*> z = x <*> (y <*> z)"\medskip
2.70 +end
2.71 +\end{ascbox}
2.72 +
2.73 +\TT{Semigroup} first declares a polymorphic constant $\TIMES ::
2.74 +[\alpha, \alpha] \To \alpha$ and then defines the class \TT{semigroup}
2.75 +of all those types $\tau$ such that $\TIMES :: [\tau, \tau] \To \tau$
2.76 +is an associative operator\footnote{Note that $\TIMES$ is used here
2.77 + instead of $*$, because the latter is already declared in theory
2.78 + \TT{HOL} in a slightly different way.}. The axiom \TT{assoc}
2.79 +contains exactly one type variable, which is invisible in the above
2.80 +presentation, though. Also note that free term variables (like $x$,
2.81 +$y$, $z$) are allowed for user convenience --- conceptually all of
2.82 +these are bound by outermost universal quantifiers.
2.83 +
2.84 +\medskip
2.85 +
2.86 +In general, type classes may be used to describe \E{structures} with
2.87 +exactly one carrier $\alpha$ and a fixed \E{signature}. Different
2.88 +signatures require different classes. In the following theory
2.89 +\TT{Semigroups}, class \TT{plus\_sg} represents semigroups of the form
2.90 +$(\tau, \PLUS^\tau)$ while \TT{times\_sg} represents semigroups
2.91 +$(\tau, \TIMES^\tau)$:
2.92 +
2.93 +\begin{ascbox}
2.94 +Semigroups = HOL +\medskip
2.95 +consts
2.96 + "<+>" :: "['a, 'a] => 'a" (infixl 65)
2.97 + "<*>" :: "['a, 'a] => 'a" (infixl 70)
2.98 + assoc :: "(['a, 'a] => 'a) => bool"\medskip
2.99 +defs
2.100 + assoc_def "assoc f == ALL x y z. f (f x y) z = f x (f y z)"\medskip
2.101 +axclass
2.102 + plus_sg < term
2.103 + plus_assoc "assoc (op <+>)"\medskip
2.104 +axclass
2.105 + times_sg < term
2.106 + times_assoc "assoc (op <*>)"\medskip
2.107 +end
2.108 +\end{ascbox}
2.109 +
2.110 +Even if both classes \TT{plus\_sg} and \TT{times\_sg} represent
2.111 +semigroups in a sense, they are not the same!
2.112 +
2.113 +
2.114 +\subsection{Basic group theory}
2.115 +
2.116 +The meta type system of \Isa\ supports \E{intersections} and
2.117 +\E{inclusions} of type classes. These directly correspond to
2.118 +intersections and inclusions of type predicates in a purely set
2.119 +theoretic sense. This is sufficient as a means to describe simple
2.120 +hierarchies of structures. As an illustration, we use the well-known
2.121 +example of semigroups, monoids, general groups and abelian groups.
2.122 +
2.123 +
2.124 +\subsubsection{Monoids and Groups}
2.125 +
2.126 +First a small theory that provides some polymorphic constants to be
2.127 +used later for the signature parts:
2.128 +
2.129 +\begin{ascbox}
2.130 +Sigs = HOL +\medskip
2.131 +consts
2.132 + "<*>" :: "['a, 'a] => 'a" (infixl 70)
2.133 + inverse :: "'a => 'a"
2.134 + "1" :: "'a" ("1")\medskip
2.135 +end
2.136 +\end{ascbox}
2.137 +
2.138 +Next comes the theory \TT{Monoid} which defines class
2.139 +\TT{monoid}\footnote{Note that multiple class axioms are allowed for
2.140 + user convenience --- they simply represent the conjunction of their
2.141 + respective universal closures.}:
2.142 +
2.143 +\begin{ascbox}
2.144 +Monoid = Sigs +\medskip
2.145 +axclass
2.146 + monoid < term
2.147 + assoc "(x <*> y) <*> z = x <*> (y <*> z)"
2.148 + left_unit "1 <*> x = x"
2.149 + right_unit "x <*> 1 = x"\medskip
2.150 +end
2.151 +\end{ascbox}
2.152 +
2.153 +So class \TT{monoid} contains exactly those types $\tau$ where $\TIMES
2.154 +:: [\tau, \tau] \To \tau$ and $\TT{1} :: \tau$ are specified
2.155 +appropriately, such that $\TIMES$ is associative and $\TT{1}$ is a
2.156 +left and right unit for $\TIMES$.
2.157 +
2.158 +\medskip
2.159 +
2.160 +Independently of \TT{Monoid}, we now define theory \TT{Group} which
2.161 +introduces a linear hierarchy of semigroups, general groups and
2.162 +abelian groups:
2.163 +
2.164 +\begin{ascbox}
2.165 +Group = Sigs +\medskip
2.166 +axclass
2.167 + semigroup < term
2.168 + assoc "(x <*> y) <*> z = x <*> (y <*> z)"\brk
2.169 +axclass
2.170 + group < semigroup
2.171 + left_unit "1 <*> x = x"
2.172 + left_inverse "inverse x <*> x = 1"\medskip
2.173 +axclass
2.174 + agroup < group
2.175 + commut "x <*> y = y <*> x"\medskip
2.176 +end
2.177 +\end{ascbox}
2.178 +
2.179 +Class \TT{group} inherits associativity of $\TIMES$ from
2.180 +\TT{semigroup} and adds the other two group axioms. Similarly,
2.181 +\TT{agroup} is defined as the subset of \TT{group} such that for all
2.182 +of its elements $\tau$, the operation $\TIMES :: [\tau, \tau] \To
2.183 +\tau$ is even commutative.
2.184 +
2.185 +
2.186 +\subsubsection{Abstract reasoning}
2.187 +
2.188 +In a sense, axiomatic type classes may be viewed as \E{abstract
2.189 + theories}. Above class definitions internally generate the
2.190 +following abstract axioms:
2.191 +
2.192 +\begin{ascbox}
2.193 +assoc: (?x::?'a::semigroup) <*> (?y::?'a::semigroup)
2.194 + <*> (?z::?'a::semigroup) = ?x <*> (?y <*> ?z)\medskip
2.195 +left_unit: 1 <*> (?x::?'a::group) = ?x
2.196 +left_inverse: inverse (?x::?'a::group) <*> ?x = 1\medskip
2.197 +commut: (?x::?'a::agroup) <*> (?y::?'a::agroup) = ?y <*> ?x
2.198 +\end{ascbox}
2.199 +
2.200 +All of these contain type variables $\alpha :: c$ that are restricted
2.201 +to types of some class $c$. These \E{sort constraints} express a
2.202 +logical precondition for the whole formula. For example, \TT{assoc}
2.203 +states that for all $\tau$, provided that $\tau :: \TT{semigroup}$,
2.204 +the operation $\TIMES :: [\tau, \tau] \To \tau$ is associative.
2.205 +
2.206 +\medskip
2.207 +
2.208 +From a purely technical point of view, abstract axioms are just
2.209 +ordinary \Isa-theorems (of \ML-type \TT{thm}). They may be used for
2.210 +\Isa-proofs without special treatment. Such ``abstract proofs''
2.211 +usually yield new abstract theorems. For example, in theory \TT{Group}
2.212 +we may derive:
2.213 +
2.214 +\begin{ascbox}
2.215 +right_unit: (?x::?'a::group) <*> 1 = ?x
2.216 +right_inverse: (?x::?'a::group) <*> inverse ?x = 1
2.217 +inverse_product: inverse ((?x::?'a::group) <*> (?y::?'a::group)) =
2.218 + inverse ?y <*> inverse ?x
2.219 +inverse_inv: inverse (inverse (?x::?'a::group)) = ?x
2.220 +ex1_inverse: ALL x::?'a::group. EX! y::?'a::group. y <*> x = 1
2.221 +\end{ascbox}
2.222 +
2.223 +Abstract theorems (which include abstract axioms, of course) may be
2.224 +instantiated to only those types $\tau$ where the appropriate class
2.225 +membership $\tau :: c$ is known at \Isa's type signature level. Since
2.226 +we have $\TT{agroup} \subseteq \TT{group} \subseteq \TT{semigroup}$ by
2.227 +definition, all theorems of \TT{semigroup} and \TT{group} are
2.228 +automatically inherited by \TT{group} and \TT{agroup}.
2.229 +
2.230 +
2.231 +\subsubsection{Abstract instantiation}
2.232 +
2.233 +Until now, theories \TT{Monoid} and \TT{Group} were independent.
2.234 +Forming their union $\TT{Monoid} + \TT{Group}$ we get the following
2.235 +class hierarchy at the type signature level (left hand side):
2.236 +
2.237 +\begin{center}
2.238 + \small
2.239 + \unitlength 0.75mm
2.240 + \begin{picture}(65,90)(0,-10)
2.241 + \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
2.242 + \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
2.243 + \put(15,5){\makebox(0,0){\tt agroup}}
2.244 + \put(15,25){\makebox(0,0){\tt group}}
2.245 + \put(15,45){\makebox(0,0){\tt semigroup}}
2.246 + \put(30,65){\makebox(0,0){\tt term}} \put(50,45){\makebox(0,0){\tt
2.247 + monoid}}
2.248 + \end{picture}
2.249 + \hspace{4em}
2.250 + \begin{picture}(30,90)(0,0)
2.251 + \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
2.252 + \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
2.253 + \put(15,5){\makebox(0,0){\tt agroup}}
2.254 + \put(15,25){\makebox(0,0){\tt group}}
2.255 + \put(15,45){\makebox(0,0){\tt monoid}}
2.256 + \put(15,65){\makebox(0,0){\tt semigroup}}
2.257 + \put(15,85){\makebox(0,0){\tt term}}
2.258 + \end{picture}
2.259 +\end{center}
2.260 +
2.261 +We know by definition that $\TIMES$ is associative for monoids, i.e.\
2.262 +$\TT{monoid} \subseteq \TT{semigroup}$. Furthermore we have
2.263 +\TT{assoc}, \TT{left\_unit} and \TT{right\_unit} for groups (where
2.264 +\TT{right\_unit} is derivable from the group axioms), that is
2.265 +$\TT{group} \subseteq \TT{monoid}$. This way we get the refined class
2.266 +hierarchy shown above at the right hand side.
2.267 +
2.268 +The additional inclusions $\TT{monoid} \subseteq \TT{semigroup}$ and
2.269 +$\TT{group} \subseteq \TT{monoid}$ are established by logical means
2.270 +and have to be explicitly made known at the type signature level. This
2.271 +is what the theory section \TT{instance} does. So we define
2.272 +\TT{MonoidGroupInsts} as follows:
2.273 +
2.274 +\begin{ascbox}
2.275 +MonoidGroupInsts = Monoid + Group +\medskip
2.276 +instance
2.277 + monoid < semigroup (Monoid.assoc)\medskip
2.278 +instance
2.279 + group < monoid (assoc, left_unit, right_unit)\medskip
2.280 +end
2.281 +\end{ascbox}
2.282 +
2.283 +The \TT{instance} section does really check that the class inclusions
2.284 +(or type arities) to be added are derivable. To this end, it sets up a
2.285 +suitable goal and attempts a proof with the help of some internal
2.286 +axioms and user supplied theorems. These latter \E{witnesses} usually
2.287 +should be appropriate type instances of the class axioms (as are
2.288 +\TT{Monoid.assoc} and \TT{assoc}, \TT{left\_unit}, \TT{right\_unit}
2.289 +above).
2.290 +
2.291 +The most important internal tool for instantiation proofs is the class
2.292 +introduction rule that is automatically generated by \TT{axclass}. For
2.293 +class \TT{group} this is axiom \TT{groupI}:
2.294 +
2.295 +\begin{ascbox}
2.296 +groupI: [| OFCLASS(?'a::term, semigroup_class);
2.297 + !!x::?'a::term. 1 <*> x = x;
2.298 + !!x::?'a::term. inverse x <*> x = 1 |]
2.299 + ==> OFCLASS(?'a::term, group_class)
2.300 +\end{ascbox}
2.301 +
2.302 +There are also axioms \TT{monoidI}, \TT{semigroupI} and \TT{agroupI}
2.303 +of a similar form. Note that $\TT{OFCLASS}(\tau, c \TT{\_class})$
2.304 +expresses class membership $\tau :: c$ as a proposition of the
2.305 +meta-logic.
2.306 +
2.307 +
2.308 +\subsubsection{Concrete instantiation}
2.309 +
2.310 +So far we have covered the case of \TT{instance $c_1$ < $c_2$} that
2.311 +could be described as \E{abstract instantiation} --- $c_1$ is more
2.312 +special than $c_2$ and thus an instance of $c_2$. Even more
2.313 +interesting for practical applications are \E{concrete instantiations}
2.314 +of axiomatic type classes. That is, certain simple schemes $(\alpha_1,
2.315 +\ldots, \alpha_n)t :: c$ of class membership may be transferred to
2.316 +\Isa's type signature level. This form of \TT{instance} is a ``safe''
2.317 +variant of the old-style \TT{arities} theory section.
2.318 +
2.319 +As an example, we show that type \TT{bool} with exclusive-or as
2.320 +operation $\TIMES$, identity as \TT{inverse}, and \TT{False} as \TT{1}
2.321 +forms an abelian group. We first define theory \TT{Xor}:
2.322 +
2.323 +\begin{ascbox}
2.324 +Xor = Group +\medskip
2.325 +defs
2.326 + prod_bool_def "x <*> y == x ~= (y::bool)"
2.327 + inverse_bool_def "inverse x == x::bool"
2.328 + unit_bool_def "1 == False"\medskip
2.329 +end
2.330 +\end{ascbox}
2.331 +
2.332 +It is important to note that above \TT{defs} are just overloaded
2.333 +meta-level constant definitions. In particular, type classes are not
2.334 +yet involved at all! This form of constant definition with overloading
2.335 +(and optional primitive recursion over types) would be also possible
2.336 +in traditional versions of \HOL\ that lack type classes.
2.337 +% (see FIXME <foundation> for more details)
2.338 +Nonetheless, such definitions are best applied in the context of
2.339 +classes.
2.340 +
2.341 +\medskip
2.342 +
2.343 +Since we chose the \TT{defs} of theory \TT{Xor} suitably, the class
2.344 +membership $\TT{bool} :: \TT{agroup}$ is now derivable as follows:
2.345 +
2.346 +\begin{ascbox}
2.347 +open AxClass;
2.348 +goal_arity Xor.thy ("bool", [], "agroup");
2.349 +\out{Level 0}
2.350 +\out{OFCLASS(bool, agroup_class)}
2.351 +\out{ 1. OFCLASS(bool, agroup_class)}\brk
2.352 +by (axclass_tac Xor.thy []);
2.353 +\out{Level 1}
2.354 +\out{OFCLASS(bool, agroup_class)}
2.355 +\out{ 1. !!(x::bool) (y::bool) z::bool. x <*> y <*> z = x <*> (y <*> z)}
2.356 +\out{ 2. !!x::bool. 1 <*> x = x}
2.357 +\out{ 3. !!x::bool. inverse x <*> x = 1}
2.358 +\out{ 4. !!(x::bool) y::bool. x <*> y = y <*> x}
2.359 +\end{ascbox}
2.360 +
2.361 +The tactic \TT{axclass\_tac} has applied \TT{agroupI} internally to
2.362 +expand the class definition. It now remains to be shown that the
2.363 +\TT{agroup} axioms hold for bool. To this end, we expand the
2.364 +definitions of \TT{Xor} and solve the new subgoals by \TT{fast\_tac}
2.365 +of \HOL:
2.366 +
2.367 +\begin{ascbox}
2.368 +by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inverse_bool_def,
2.369 + Xor.unit_bool_def]);
2.370 +\out{Level 2}
2.371 +\out{OFCLASS(bool, agroup_class)}
2.372 +\out{ 1. !!(x::bool) (y::bool) z::bool. x ~= y ~= z = (x ~= (y ~= z))}
2.373 +\out{ 2. !!x::bool. False ~= x = x}
2.374 +\out{ 3. !!x::bool. x ~= x = False}
2.375 +\out{ 4. !!(x::bool) y::bool. x ~= y = (y ~= x)}
2.376 +by (ALLGOALS (fast_tac HOL_cs));
2.377 +\out{Level 3}
2.378 +\out{OFCLASS(bool, agroup_class)}
2.379 +\out{No subgoals!}
2.380 +qed "bool_in_agroup";
2.381 +\out{val bool_in_agroup = "OFCLASS(bool, agroup_class)"}
2.382 +\end{ascbox}
2.383 +
2.384 +The result is theorem $\TT{OFCLASS}(\TT{bool}, \TT{agroup\_class})$
2.385 +which expresses $\TT{bool} :: \TT{agroup}$ as a meta-proposition. This
2.386 +is not yet known at the type signature level, though.
2.387 +
2.388 +\medskip
2.389 +
2.390 +What we have done here by hand, can be also performed via
2.391 +\TT{instance} in a similar way behind the scenes. This may look as
2.392 +follows\footnote{Subsequently, theory \TT{Xor} is no longer
2.393 + required.}:
2.394 +
2.395 +\begin{ascbox}
2.396 +BoolGroupInsts = Group +\medskip
2.397 +defs
2.398 + prod_bool_def "x <*> y == x ~= (y::bool)"
2.399 + inverse_bool_def "inverse x == x::bool"
2.400 + unit_bool_def "1 == False"\medskip
2.401 +instance
2.402 + bool :: agroup \{| ALLGOALS (fast_tac HOL_cs) |\}\medskip
2.403 +end
2.404 +\end{ascbox}
2.405 +
2.406 +This way, we have $\TT{bool} :: \TT{agroup}$ in the type signature of
2.407 +\TT{BoolGroupInsts}, and all abstract group theorems are transferred
2.408 +to \TT{bool} for free.
2.409 +
2.410 +Similarly, we could now also instantiate our group theory classes to
2.411 +many other concrete types. For example, $\TT{int} :: \TT{agroup}$ (by
2.412 +defining $\TIMES$ as addition, \TT{inverse} as negation and \TT{1} as
2.413 +zero, say) or $\TT{list} :: (\TT{term})\TT{semigroup}$ (e.g.\ if
2.414 +$\TIMES$ is list append). Thus, the characteristic constants $\TIMES$,
2.415 +\TT{inverse}, \TT{1} really become overloaded, i.e.\ have different
2.416 +meanings on different types.
2.417 +
2.418 +
2.419 +\subsubsection{Lifting and Functors}
2.420 +
2.421 +As already mentioned above, \HOL-like systems not only support
2.422 +overloaded definitions of polymorphic constants (without requiring
2.423 +type classes), but even primitive recursion over types. That is,
2.424 +definitional equations $c^\tau \Eq t$ may also contain constants of
2.425 +name $c$ on the RHS --- provided that these have types that are
2.426 +strictly simpler (structurally) than $\tau$.
2.427 +
2.428 +This feature enables us to \E{lift operations}, e.g.\ to Cartesian
2.429 +products, direct sums or function spaces. Below, theory
2.430 +\TT{ProdGroupInsts} lifts $\TIMES$ componentwise to two-place
2.431 +Cartesian products $\alpha \times \beta$:
2.432 +
2.433 +\begin{ascbox}
2.434 +ProdGroupInsts = Prod + Group +\medskip
2.435 +defs
2.436 + prod_prod_def "p <*> q == (fst p <*> fst q, snd p <*> snd q)"\medskip
2.437 +instance
2.438 + "*" :: (semigroup, semigroup) semigroup
2.439 + \{| simp_tac (prod_ss addsimps [assoc]) 1 |\}
2.440 +end
2.441 +\end{ascbox}
2.442 +
2.443 +Note that \TT{prod\_prod\_def} basically has the form $\edrv
2.444 +{\TIMES}^{\alpha \times \beta} \Eq \ldots {\TIMES}^\alpha \ldots
2.445 +{\TIMES}^\beta \ldots$, i.e.\ the recursive occurrences
2.446 +$\TIMES^\alpha$ and $\TIMES^\beta$ are really at ``simpler'' types.
2.447 +
2.448 +It is very easy to see that associativity of $\TIMES^\alpha$,
2.449 +$\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence
2.450 +the two-place type constructor $\times$ maps semigroups into
2.451 +semigroups. This fact is proven and put into \Isa's type signature by
2.452 +above \TT{instance} section.
2.453 +
2.454 +\medskip
2.455 +
2.456 +Thus, if we view class instances as ``structures'', overloaded
2.457 +constant definitions with primitive recursion over types indirectly
2.458 +provide some kind of ``functors'' (mappings between abstract theories,
2.459 +that is).
2.460 +
2.461 +
2.462 +\subsection{Syntactic classes}
2.463 +
2.464 +There is still a feature of \Isa's type system left that we have not
2.465 +yet used: When declaring polymorphic constants $c :: \tau$, the type
2.466 +variables occurring in $\tau$ may be constrained by type classes (or
2.467 +even general sorts). Note that by default, in \Isa/\HOL\ the
2.468 +declaration:
2.469 +
2.470 +\begin{ascbox}
2.471 + <*> :: ['a, 'a] => 'a
2.472 +\end{ascbox}
2.473 +
2.474 +is actually an abbreviation for:
2.475 +
2.476 +\begin{ascbox}
2.477 + <*> :: ['a::term, 'a::term] => 'a::term
2.478 +\end{ascbox}
2.479 +
2.480 +Since class \TT{term} is the universal class of \HOL, this is not
2.481 +really a restriction at all. A less trivial example is the following
2.482 +theory \TT{Product}:
2.483 +
2.484 +\begin{ascbox}
2.485 +Product = HOL +\medskip
2.486 +axclass
2.487 + product < term\medskip
2.488 +consts
2.489 + "<*>" :: "['a::product, 'a] => 'a" (infixl 70)\medskip
2.490 +end
2.491 +\end{ascbox}
2.492 +
2.493 +Here class \TT{product} is defined as subclass of \TT{term}, but
2.494 +without any additional axioms. This effects in logical equivalence of
2.495 +\TT{product} and \TT{term}, since \TT{productI} is as follows:
2.496 +
2.497 +\begin{ascbox}
2.498 +productI: OFCLASS(?'a::logic, term_class) ==>
2.499 + OFCLASS(?'a::logic, product_class)
2.500 +\end{ascbox}
2.501 +
2.502 +I.e.\ $\TT{term} \subseteq \TT{product}$. The converse inclusion is
2.503 +already contained in the type signature of theory \TT{Product}.
2.504 +
2.505 +Now, what is the difference of declaring $\TIMES :: [\alpha ::
2.506 +\TT{product}, \alpha] \To \alpha$ vs.\ declaring $\TIMES :: [\alpha ::
2.507 +\TT{term}, \alpha] \To \alpha$? In this special case (where
2.508 +$\TT{product} \Eq \TT{term}$), it should be obvious that both
2.509 +declarations are the same from the logic's point of view. It is even
2.510 +most sensible in the general case not to attach any \E{logical}
2.511 +meaning to sort constraints occurring in constant \E{declarations}
2.512 +(see \cite[page 79]{Wenzel94} for more details).
2.513 +
2.514 +On the other hand there are syntactic differences, of course.
2.515 +Constants $\TIMES^\tau$ are rejected by the type checker, unless $\tau
2.516 +:: \TT{product}$ is part of the type signature. In our example, this
2.517 +arity may be always added when required by means of a trivial
2.518 +\TT{instance}.
2.519 +
2.520 +Thus, we can follow this discipline: Overloaded polymorphic constants
2.521 +have their type arguments restricted to an associated (logically
2.522 +trivial) class $c$. Only immediately before \E{specifying} these
2.523 +constants on a certain type $\tau$ do we instantiate $\tau :: c$.
2.524 +
2.525 +This is done for class \TT{product} and type \TT{bool} in theory
2.526 +\TT{ProductInsts} below:
2.527 +
2.528 +\begin{ascbox}
2.529 +ProductInsts = Product +\medskip
2.530 +instance
2.531 + bool :: product\medskip
2.532 +defs
2.533 + prod_bool_def "x <*> y == x & y::bool"\medskip
2.534 +end
2.535 +\end{ascbox}
2.536 +
2.537 +Note that \TT{instance bool ::\ product} does not require any
2.538 +witnesses, since this statement is logically trivial. Nonetheless,
2.539 +\TT{instance} really performs a proof.
2.540 +
2.541 +Only after $\TT{bool} :: \TT{product}$ is made known to the type
2.542 +checker, does \TT{prod\_bool\_def} become syntactically well-formed.
2.543 +
2.544 +\medskip
2.545 +
2.546 +It is very important to see that above \TT{defs} are not directly
2.547 +connected with \TT{instance} at all! We were just following our
2.548 +convention to specify $\TIMES$ on \TT{bool} after having instantiated
2.549 +$\TT{bool} :: \TT{product}$. \Isa\ does not require these definitions,
2.550 +which is in contrast to programming languages like \Haskell.
2.551 +
2.552 +\medskip
2.553 +
2.554 +While \Isa\ type classes and those of \Haskell\ are almost the same as
2.555 +far as type checking and type inference are concerned, there are major
2.556 +semantic differences. \Haskell\ classes require their instances to
2.557 +\E{provide operations} of certain \E{names}. Therefore, its
2.558 +\TT{instance} has a \TT{where} part that tells the system what these
2.559 +``member functions'' should be.
2.560 +
2.561 +This style of \TT{instance} won't make much sense in \Isa, because its
2.562 +meta-logic has no corresponding notion of ``providing operations'' or
2.563 +``names''.
2.564 +
2.565 +
2.566 +\subsection{Defining natural numbers in \FOL}
2.567 +\label{sec:ex-natclass}
2.568 +
2.569 +Axiomatic type classes abstract over exactly one type argument. Thus,
2.570 +any \E{axiomatic} theory extension where each axiom refers to at most
2.571 +one type variable, may be trivially turned into a \E{definitional}
2.572 +one.
2.573 +
2.574 +We illustrate this with the natural numbers in \Isa/\FOL:
2.575 +
2.576 +\begin{ascbox}
2.577 +NatClass = FOL +\medskip
2.578 +consts
2.579 + "0" :: "'a" ("0")
2.580 + Suc :: "'a => 'a"
2.581 + rec :: "['a, 'a, ['a, 'a] => 'a] => 'a"\medskip
2.582 +axclass
2.583 + nat < term
2.584 + induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
2.585 + Suc_inject "Suc(m) = Suc(n) ==> m = n"
2.586 + Suc_neq_0 "Suc(m) = 0 ==> R"
2.587 + rec_0 "rec(0, a, f) = a"
2.588 + rec_Suc "rec(Suc(m), a, f) = f(m, rec(m, a, f))"\medskip
2.589 +consts
2.590 + "+" :: "['a::nat, 'a] => 'a" (infixl 60)\medskip
2.591 +defs
2.592 + add_def "m + n == rec(m, n, %x y. Suc(y))"\medskip
2.593 +end
2.594 +\end{ascbox}
2.595 +
2.596 +\TT{NatClass} is an abstract version of \TT{Nat}\footnote{See
2.597 + directory \TT{FOL/ex}.}. Basically, we have just replaced all
2.598 +occurrences of \E{type} \TT{nat} by $\alpha$ and used the natural
2.599 +number axioms to define \E{class} \TT{nat}\footnote{There's a snag:
2.600 + The original recursion operator \TT{rec} had to be made monomorphic,
2.601 + in a sense.}. Thus class \TT{nat} contains exactly those types
2.602 +$\tau$ that are isomorphic to ``the'' natural numbers (with signature
2.603 +\TT{0}, \TT{Suc}, \TT{rec}).
2.604 +
2.605 +Furthermore, theory \TT{NatClass} defines an ``abstract constant'' $+$
2.606 +based on class \TT{nat}.
2.607 +
2.608 +\medskip
2.609 +
2.610 +What we have done here can be also viewed as \E{type specification}.
2.611 +Of course, it still remains open if there is some type at all that
2.612 +meets the class axioms. Now a very nice property of axiomatic type
2.613 +classes is, that abstract reasoning is always possible --- independent
2.614 +of satisfiability. The meta-logic won't break, even if some class (or
2.615 +general sort) turns out to be empty (``inconsistent'')
2.616 +later\footnote{As a consequence of an old bug, this is \E{not} true
2.617 + for pre-\Isa95 versions.}.
2.618 +
2.619 +For example, we may derive the following abstract natural numbers
2.620 +theorems:
2.621 +
2.622 +\begin{ascbox}
2.623 +add_0: 0 + (?n::?'a::nat) = ?n
2.624 +add_Suc: Suc(?m::?'a::nat) + (?n::?'a::nat) = Suc(?m + ?n)
2.625 +\end{ascbox}
2.626 +
2.627 +See also file \TT{FOL/ex/NatClass.ML}. Note that this required only
2.628 +some trivial modifications of the original \TT{Nat.ML}.
2.629 +
2.630 +
2.631 +\section{The user interface of \Isa's axclass package}
2.632 +
2.633 +The actual axiomatic type class package of \Isa/\Pure\ mainly consists
2.634 +of two new theory sections: \TT{axclass} and \TT{instance}. Some
2.635 +typical applications of these have already been demonstrated in
2.636 +\secref{sec:ex}, below their syntax and semantics are presented more
2.637 +completely.
2.638 +
2.639 +
2.640 +\subsection{The \TT{axclass} section}
2.641 +
2.642 +Within theory files, \TT{axclass} introduces an axiomatic type class
2.643 +definition. Its concrete syntax is:
2.644 +
2.645 +\begin{matharray}{l}
2.646 + \TT{axclass} \\
2.647 + \ \ c \TT{ < } c_1\TT, \ldots\TT, c_n \\
2.648 + \ \ \idt{id}_1\ \idt{axm}_1 \\
2.649 + \ \ \vdots \\
2.650 + \ \ \idt{id}_m\ \idt{axm}_m
2.651 +\end{matharray}
2.652 +
2.653 +Where $c, c_1, \ldots, c_n$ are classes (category $\idt{id}$ or
2.654 +$\idt{string}$) and $\idt{axm}_1, \ldots, \idt{axm}_m$ (with $m \ge
2.655 +0$) are formulas (category $\idt{string}$).
2.656 +
2.657 +Class $c$ has to be new, and sort $\{c_1, \ldots, c_n\}$ a subsort of
2.658 +\TT{logic}. Each class axiom $\idt{axm}_j$ may contain any term
2.659 +variables, but at most one type variable (which need not be the same
2.660 +for all axioms). The sort of this type variable has to be a supersort
2.661 +of $\{c_1, \ldots, c_n\}$.
2.662 +
2.663 +\medskip
2.664 +
2.665 +The \TT{axclass} section declares $c$ as subclass of $c_1, \ldots,
2.666 +c_n$ to the type signature.
2.667 +
2.668 +Furthermore, $\idt{axm}_1, \ldots, \idt{axm}_m$ are turned into the
2.669 +``abstract axioms'' of $c$ with names $\idt{id}_1, \ldots,
2.670 +\idt{id}_m$. This is done by replacing all occurring type variables
2.671 +by $\alpha :: c$. Original axioms that do not contain any type
2.672 +variable will be prefixed by the logical precondition
2.673 +$\TT{OFCLASS}(\alpha :: \TT{logic}, c\TT{\_class})$.
2.674 +
2.675 +Another axiom of name $c\TT{I}$ --- the ``class $c$ introduction
2.676 +rule'' --- is built from the respective universal closures of
2.677 +$\idt{axm}_1, \ldots, \idt{axm}_m$ appropriately.
2.678 +
2.679 +
2.680 +\subsection{The \TT{instance} section}
2.681 +
2.682 +Section \TT{instance} proves class inclusions or type arities at the
2.683 +logical level and then transfers these into the type signature.
2.684 +
2.685 +Its concrete syntax is:
2.686 +
2.687 +\begin{matharray}{l}
2.688 + \TT{instance} \\
2.689 + \ \ [\ c_1 \TT{ < } c_2 \ |\
2.690 + t \TT{ ::\ (}\idt{sort}_1\TT, \ldots \TT, \idt{sort}_n\TT) \idt{sort}\ ] \\
2.691 + \ \ [\ \TT(\idt{name}_1 \TT, \ldots\TT, \idt{name}_m\TT)\ ] \\
2.692 + \ \ [\ \TT{\{|} \idt{text} \TT{|\}}\ ]
2.693 +\end{matharray}
2.694 +
2.695 +Where $c_1, c_2$ are classes and $t$ is an $n$-place type constructor
2.696 +(all of category $\idt{id}$ or $\idt{string})$. Furthermore,
2.697 +$\idt{sort}_i$ are sorts in the usual \Isa-syntax.
2.698 +
2.699 +\medskip
2.700 +
2.701 +Internally, \TT{instance} first sets up an appropriate goal that
2.702 +expresses the class inclusion or type arity as a meta-proposition.
2.703 +Then tactic \TT{AxClass.axclass\_tac} is applied with all preceding
2.704 +meta-definitions of the current theory file and the user-supplied
2.705 +witnesses. The latter are $\idt{name}_1, \ldots, \idt{name}_m$, where
2.706 +$\idt{id}$ refers to an \ML-name of a theorem, and $\idt{string}$ to an
2.707 +axiom of the current theory node\footnote{Thus, the user may reference
2.708 + axioms from above this \TT{instance} in the theory file. Note
2.709 + that new axioms appear at the \ML-toplevel only after the file is
2.710 + processed completely.}.
2.711 +
2.712 +Tactic \TT{AxClass.axclass\_tac} first unfolds the class definition by
2.713 +resolving with rule $c\TT{I}$, and then applies the witnesses
2.714 +according to their form: Meta-definitions are unfolded, all other
2.715 +formulas are repeatedly resolved\footnote{This is done in a way that
2.716 + enables proper object-\E{rules} to be used as witnesses for
2.717 + corresponding class axioms.} with.
2.718 +
2.719 +The final optional argument $\idt{text}$ is \ML-code of an arbitrary
2.720 +user tactic which is applied last to any remaining goals.
2.721 +
2.722 +\medskip
2.723 +
2.724 +Because of the complexity of \TT{instance}'s witnessing mechanisms,
2.725 +new users of the axclass package are advised to only use the simple
2.726 +form $\TT{instance}\ \ldots\ (\idt{id}_1, \ldots, \idt{id}_m)$, where
2.727 +the identifiers refer to theorems that are appropriate type instances
2.728 +of the class axioms. This typically requires an auxiliary theory,
2.729 +though, which defines some constants and then proves these witnesses.
2.730 +
2.731 +
2.732 +\begin{thebibliography}{}
2.733 +
2.734 +\bibitem[Nipkow, 1993a]{Nipkow-slides} T. Nipkow. Axiomatic Type
2.735 + Classes (in Isabelle). Presentation at the workshop \E{Types for
2.736 + Proof and Programs}, Nijmegen, 1993.
2.737 +
2.738 +\bibitem[Nipkow, 1993b]{Nipkow93} T. Nipkow. Order-Sorted Polymorphism
2.739 + in Isabelle. In G. Huet, G. Plotkin, editors, \E{Logical
2.740 + Environments}, pp.\ 164--188, Cambridge University Press, 1993.
2.741 +
2.742 +\bibitem[Paulson, 1994]{Paulson94} L.C. Paulson. \E{Isabelle --- A
2.743 + Generic Theorem Prover}. LNCS 828, 1994.
2.744 +
2.745 +\bibitem[Wenzel, 1994]{Wenzel94} M. Wenzel. \E{Axiomatische
2.746 + Typ-Klassen in Isabelle}. Diplom\-arbeit, TU München, 1994.
2.747 +
2.748 +\end{thebibliography}
2.749 +
2.750 +\end{document}
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/AxClass/out Mon May 12 17:53:36 1997 +0200
3.3 @@ -0,0 +1,70 @@
3.4 +
3.5 +- assoc;
3.6 +val it =
3.7 + "(?x::?'a::semigroup) <*> (?y::?'a::semigroup) <*> (?z::?'a::semigroup) =
3.8 + ?x <*> (?y <*> ?z)" : thm
3.9 +- left_unit;
3.10 +val it = "1 <*> (?x::?'a::group) = ?x" : thm
3.11 +- left_inv;
3.12 +val it = "inv (?x::?'a::group) <*> ?x = 1" : thm
3.13 +- commut;
3.14 +val it = "(?x::?'a::agroup) <*> (?y::?'a::agroup) = ?y <*> ?x" : thm
3.15 +
3.16 +
3.17 +- right_unit;
3.18 +val it = "(?x::?'a::group) <*> 1 = ?x" : thm
3.19 +- right_inv;
3.20 +val it = "(?x::?'a::group) <*> inv ?x = 1" : thm
3.21 +- inv_product;
3.22 +val it = "inv ((?x::?'a::group) <*> (?y::?'a::group)) = inv ?y <*> inv ?x"
3.23 + : thm
3.24 +- inv_inv;
3.25 +val it = "inv (inv (?x::?'a::group)) = ?x" : thm
3.26 +- ex1_inv;
3.27 +val it = "ALL x::?'a::group. EX! y::?'a::group. y <*> x = 1" : thm
3.28 +
3.29 +
3.30 +- groupI;
3.31 +val it =
3.32 + "[| OFCLASS(?'a::term, semigroup_class); !!x::?'a::term. 1 <*> x = x;
3.33 + !!x::?'a::term. inv x <*> x = 1 |] ==> OFCLASS(?'a::term, group_class)"
3.34 + : thm
3.35 +
3.36 +
3.37 +- open AxClass;
3.38 +- goal_arity Xor.thy ("bool", [], "agroup");
3.39 +Level 0
3.40 +OFCLASS(bool, agroup_class)
3.41 + 1. OFCLASS(bool, agroup_class)
3.42 +val it = [] : thm list
3.43 +- by (axclass_tac Xor.thy []);
3.44 +Level 1
3.45 +OFCLASS(bool, agroup_class)
3.46 + 1. !!(x::bool) (y::bool) z::bool. x <*> y <*> z = x <*> (y <*> z)
3.47 + 2. !!x::bool. 1 <*> x = x
3.48 + 3. !!x::bool. inv x <*> x = 1
3.49 + 4. !!(x::bool) y::bool. x <*> y = y <*> x
3.50 +val it = () : unit
3.51 +
3.52 +- by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inv_bool_def, Xor.unit_bool_def]);
3.53 +Level 2
3.54 +OFCLASS(bool, agroup_class)
3.55 + 1. !!(x::bool) (y::bool) z::bool. x ~= y ~= z = (x ~= (y ~= z))
3.56 + 2. !!x::bool. False ~= x = x
3.57 + 3. !!x::bool. x ~= x = False
3.58 + 4. !!(x::bool) y::bool. x ~= y = (y ~= x)
3.59 +val it = () : unit
3.60 +- by (ALLGOALS (fast_tac HOL_cs));
3.61 +Level 3
3.62 +OFCLASS(bool, agroup_class)
3.63 +No subgoals!
3.64 +val it = () : unit
3.65 +- qed "bool_in_agroup";
3.66 +val bool_in_agroup = "OFCLASS(bool, agroup_class)" : thm
3.67 +val it = () : unit
3.68 +
3.69 +
3.70 +- Product.productI;
3.71 +val it =
3.72 + "OFCLASS(?'a::logic, term_class) ==> OFCLASS(?'a::logic, product_class)"
3.73 + : thm
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/AxClass/style.tex Mon May 12 17:53:36 1997 +0200
4.3 @@ -0,0 +1,362 @@
4.4 +
4.5 +\documentclass[11pt,a4paper,fleqn]{article}
4.6 +\usepackage[latin1]{inputenc}
4.7 +\usepackage{english}
4.8 +\usepackage{a4}
4.9 +\usepackage{alltt}
4.10 +\usepackage{bbb}
4.11 +
4.12 +
4.13 +\makeatletter
4.14 +
4.15 +
4.16 +%%% layout
4.17 +
4.18 +\sloppy
4.19 +
4.20 +\parindent 0pt
4.21 +\parskip 0.5ex
4.22 +
4.23 +
4.24 +%%% text mode
4.25 +
4.26 +\newcommand{\B}[1]{\textbf{#1}}
4.27 +\newcommand{\TT}[1]{\ifmmode\mbox{\texttt{#1}}\else\texttt{#1}\fi}
4.28 +\newcommand{\E}[1]{\emph{#1}}
4.29 +\renewcommand{\P}[1]{\textsc{#1}}
4.30 +
4.31 +
4.32 +\renewcommand{\labelenumi}{(\theenumi)}
4.33 +\newcommand{\dfn}[1]{{\bf #1}}
4.34 +
4.35 +\newcommand{\thy}[1]{\mbox{\sc #1}}
4.36 +%\newcommand{\thy}[1]{\mbox{\textsc{#1}}}
4.37 +\newcommand{\IHOL}{\thy{ihol}}
4.38 +\newcommand{\SIHOL}{\thy{sihol}}
4.39 +\newcommand{\HOL}{\thy{hol}}
4.40 +\newcommand{\HOLBB}{\thy{hol88}}
4.41 +\newcommand{\FOL}{\thy{fol}}
4.42 +\newcommand{\SET}{\thy{set}}
4.43 +\newcommand{\Pure}{\thy{Pure}}
4.44 +
4.45 +
4.46 +\newcommand{\secref}[1]{\S\ref{#1}}
4.47 +
4.48 +\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
4.49 +
4.50 +
4.51 +%from alltt.sty
4.52 +\def\docspecials{\do\ \do\$\do\&%
4.53 + \do\#\do\^\do\^^K\do\_\do\^^A\do\%\do\~}
4.54 +
4.55 +\newenvironment{asc}{\small\trivlist \item[]\if@minipage\else\vskip\parskip\fi
4.56 +\leftskip\@totalleftmargin\rightskip\z@
4.57 +\parindent\z@\parfillskip\@flushglue\parskip\z@
4.58 +\@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par}
4.59 +\obeylines \tt \catcode``=13 \@noligs \let\do\@makeother \docspecials
4.60 +\frenchspacing\@vobeyspaces}{\endtrivlist}
4.61 +
4.62 +\newenvironment{ascbox}{\vbox\bgroup\begin{asc}}{\end{asc}\egroup}
4.63 +\newcommand{\brk}{\end{ascbox}\vskip-20pt\begin{ascbox}}
4.64 +
4.65 +\newcommand{\out}[1]{{\fontfamily{cmtt}\fontseries{m}\fontshape{sl}\selectfont\ \ #1}}
4.66 +
4.67 +
4.68 +% warning environment
4.69 +\newcommand{\dbend}{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
4.70 +\newenvironment{warning}{\medskip\medbreak\begingroup \clubpenalty=10000
4.71 + \noindent \hangindent1.5em \hangafter=-2
4.72 + \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
4.73 + {\par\endgroup\medbreak}
4.74 +
4.75 +\newcommand{\Isa}{{\sc Isabelle}}
4.76 +\newcommand{\ML}{{\sc ml}}
4.77 +\newcommand{\Haskell}{{\rm Haskell}}
4.78 +
4.79 +\newcommand{\IMP}{"`$\Longrightarrow$"'}
4.80 +\newcommand{\PMI}{"`$\Longleftarrow$"'}
4.81 +
4.82 +
4.83 +
4.84 +%%% math mode
4.85 +
4.86 +%% generic defs
4.87 +
4.88 +\newcommand{\nquad}{\hskip-1em}
4.89 +
4.90 +\newcommand{\fct}[1]{\mathop{\rm #1}\nolimits}
4.91 +\newcommand{\idt}[1]{{\mathord{\it #1}}}
4.92 +\newcommand{\syn}[1]{{\mathord{\it #1}}}
4.93 +\newcommand{\text}[1]{\mbox{#1}}
4.94 +\newcommand{\rmtext}[1]{\mbox{\rm #1}}
4.95 +%\newcommand{\mtt}[1]{\mbox{\tt #1}}
4.96 +
4.97 +\newcommand{\falls}{\text{falls }}
4.98 +\newcommand{\sonst}{\text{sonst}}
4.99 +
4.100 +\newcommand{\Bool}{\bbbB}
4.101 +\newcommand{\Nat}{\bbbN}
4.102 +\newcommand{\Natz}{{\bbbN_0}}
4.103 +\newcommand{\Rat}{\bbbQ}
4.104 +\newcommand{\Real}{\bbbR}
4.105 +
4.106 +\newcommand{\dt}{{\mathpunct.}}
4.107 +
4.108 +\newcommand{\Gam}{\Gamma}
4.109 +\renewcommand{\epsilon}{\varepsilon}
4.110 +\renewcommand{\phi}{\varphi}
4.111 +\renewcommand{\rho}{\varrho}
4.112 +\newcommand{\eset}{{\{\}}}
4.113 +\newcommand{\etuple}{{\langle\rangle}}
4.114 +
4.115 +\newcommand{\dfneq}{\mathbin{\mathord:\mathord=}}
4.116 +\newcommand{\impl}{\Longrightarrow}
4.117 +\renewcommand{\iff}{{\;\;\mathord{\Longleftrightarrow}\;\;}}
4.118 +\newcommand{\dfniff}{{\;\;\mathord:\mathord{\Longleftrightarrow}\;\;}}
4.119 +\renewcommand{\land}{\mathrel{\,\wedge\,}}
4.120 +\renewcommand{\lor}{\mathrel{\,\vee\,}}
4.121 +\newcommand{\iso}{\cong}
4.122 +
4.123 +\newcommand{\union}{\cup}
4.124 +\newcommand{\sunion}{\mathbin{\;\cup\;}}
4.125 +\newcommand{\dunion}{\mathbin{\dot\union}}
4.126 +\newcommand{\Union}{\bigcup}
4.127 +\newcommand{\inter}{\cap}
4.128 +\newcommand{\where}{\mathrel|}
4.129 +\newcommand{\pto}{\rightharpoonup}
4.130 +\newcommand{\comp}{\circ}
4.131 +\newcommand{\aaast}{{\mathord*\mathord*\mathord*}}
4.132 +
4.133 +\newcommand{\all}[1]{\forall #1\dt\;}
4.134 +\newcommand{\ex}[1]{\exists #1\dt\;}
4.135 +\newcommand{\lam}[1]{\mathop{\lambda} #1\dt}
4.136 +
4.137 +\newcommand\lbrakk{\mathopen{[\![}}
4.138 +\newcommand\rbrakk{\mathclose{]\!]}}
4.139 +
4.140 +\newcommand{\unif}{\mathrel{=^?}}
4.141 +\newcommand{\notunif}{\mathrel{{\not=}^?}}
4.142 +\newcommand{\incompat}{\mathrel{\#}}
4.143 +
4.144 +
4.145 +%% specific defs
4.146 +
4.147 +\newcommand{\PLUS}{\mathord{\langle{+}\rangle}}
4.148 +\newcommand{\TIMES}{\mathord{\langle{*}\rangle}}
4.149 +
4.150 +
4.151 +% IHOL
4.152 +
4.153 +\newcommand{\TV}{\fct{TV}}
4.154 +\newcommand{\FV}{\fct{FV}}
4.155 +\newcommand{\BV}{\fct{BV}}
4.156 +\newcommand{\VN}{\fct{VN}}
4.157 +\newcommand{\AT}{\fct{AT}}
4.158 +\newcommand{\STV}{\fct{STV}}
4.159 +
4.160 +\newcommand{\TyVars}{\syn{TyVars}}
4.161 +\newcommand{\TyNames}{\syn{TyNames}}
4.162 +\newcommand{\TyCons}{\syn{TyCons}}
4.163 +\newcommand{\TyConsSg}{\TyCons_\Sigma}
4.164 +\newcommand{\Types}{\syn{Types}}
4.165 +\newcommand{\TypesSg}{\Types_\Sigma}
4.166 +\newcommand{\GrTypes}{\syn{GrTypes}}
4.167 +\newcommand{\GrTypesSg}{\GrTypes_\Sigma}
4.168 +\newcommand{\VarNames}{\syn{VarNames}}
4.169 +\newcommand{\Vars}{\syn{Vars}}
4.170 +\newcommand{\VarsSg}{\Vars_\Sigma}
4.171 +\newcommand{\GrVars}{\syn{GrVars}}
4.172 +\newcommand{\GrVarsSg}{\GrVars_\Sigma}
4.173 +\newcommand{\ConstNames}{\syn{ConstNames}}
4.174 +\newcommand{\Consts}{\syn{Consts}}
4.175 +\newcommand{\ConstsSg}{\Consts_\Sigma}
4.176 +\newcommand{\GrConsts}{\syn{GrConsts}}
4.177 +\newcommand{\GrConstsSg}{\GrConsts_\Sigma}
4.178 +\newcommand{\Terms}{\syn{Terms}}
4.179 +\newcommand{\TermsSg}{\Terms_\Sigma}
4.180 +\newcommand{\GrTerms}{\syn{GrTerms}}
4.181 +\newcommand{\GrTermsSg}{\GrTerms_\Sigma}
4.182 +\newcommand{\Forms}{\syn{Forms}}
4.183 +\newcommand{\FormsTh}{\Forms_\Theta}
4.184 +\newcommand{\Seqs}{\syn{Seqs}}
4.185 +\newcommand{\SeqsTh}{\Seqs_\Theta}
4.186 +\newcommand{\Axms}{\syn{Axms}}
4.187 +\newcommand{\AxmsTh}{\Axms_\Theta}
4.188 +\newcommand{\Thms}{\syn{Thms}}
4.189 +\newcommand{\ThmsTh}{\Thms_\Theta}
4.190 +
4.191 +
4.192 +\newcommand{\U}{{\cal U}}
4.193 +\newcommand{\UU}{\bbbU}
4.194 +
4.195 +\newcommand{\ty}{{\mathbin{\,:\,}}}
4.196 +\newcommand{\typ}[1]{{\mathord{\sl #1}}}
4.197 +\newcommand{\tap}{\mathord{\,}}
4.198 +\newcommand{\prop}{\typ{prop}}
4.199 +\newcommand{\itself}{\typ{itself}}
4.200 +
4.201 +\newcommand{\cnst}[1]{{\mathord{\sl #1}}}
4.202 +\newcommand{\ap}{\mathbin{}}
4.203 +\newcommand{\To}{\Rightarrow}
4.204 +\newcommand{\Eq}{\equiv}
4.205 +\newcommand{\Impl}{\Rightarrow}
4.206 +\newcommand{\Forall}{\mathop{\textstyle\bigwedge}}
4.207 +\newcommand{\All}[1]{\Forall #1\dt}
4.208 +\newcommand{\True}{\top}
4.209 +\newcommand{\False}{\bot}
4.210 +\newcommand{\Univ}{{\top\!\!\!\!\top}}
4.211 +\newcommand{\Conj}{\wedge}
4.212 +\newcommand{\TYPE}{\cnst{TYPE}}
4.213 +
4.214 +
4.215 +% rules
4.216 +
4.217 +\newcommand{\Axm}{\rmtext{Axm}}
4.218 +\newcommand{\Assm}{\rmtext{Assm}}
4.219 +\newcommand{\Mon}{\rmtext{Mon}}
4.220 +\newcommand{\ImplI}{\mathord{\Impl}\rmtext{I}}
4.221 +\newcommand{\ImplE}{\mathord{\Impl}\rmtext{E}}
4.222 +\newcommand{\ImplMP}{\rmtext{MP}}
4.223 +\newcommand{\ImplRefl}{\mathord{\Impl}\rmtext{Refl}}
4.224 +\newcommand{\ImplTrans}{\mathord{\Impl}\rmtext{Trans}}
4.225 +\newcommand{\EqRefl}{\mathord{\Eq}\rmtext{Refl}}
4.226 +\newcommand{\EqTrans}{\mathord{\Eq}\rmtext{Trans}}
4.227 +\newcommand{\EqSym}{\mathord{\Eq}\rmtext{Sym}}
4.228 +\newcommand{\EqApp}{\mathord{\Eq}\rmtext{App}}
4.229 +\newcommand{\EqAbs}{\mathord{\Eq}\rmtext{Abs}}
4.230 +\newcommand{\Eqa}{\mathord{\Eq}\alpha}
4.231 +\newcommand{\Eqb}{\mathord{\Eq}\beta}
4.232 +\newcommand{\Eqe}{\mathord{\Eq}\eta}
4.233 +\newcommand{\Ext}{\rmtext{Ext}}
4.234 +\newcommand{\EqI}{\mathord{\Eq}\rmtext{I}}
4.235 +\newcommand{\EqMP}{\mathord{\Eq}\rmtext{MP}}
4.236 +\newcommand{\EqUnfold}{\mathord{\Eq}\rmtext{Unfold}}
4.237 +\newcommand{\EqFold}{\mathord{\Eq}\rmtext{Fold}}
4.238 +\newcommand{\AllI}{\mathord{\Forall}\rmtext{I}}
4.239 +\newcommand{\AllE}{\mathord{\Forall}\rmtext{E}}
4.240 +\newcommand{\TypInst}{\rmtext{TypInst}}
4.241 +\newcommand{\Inst}{\rmtext{Inst}}
4.242 +\newcommand{\TrueI}{\True\rmtext{I}}
4.243 +\newcommand{\FalseE}{\False\rmtext{E}}
4.244 +\newcommand{\UnivI}{\Univ\rmtext{I}}
4.245 +\newcommand{\ConjI}{\mathord{\Conj}\rmtext{I}}
4.246 +\newcommand{\ConjE}{\mathord{\Conj}\rmtext{E}}
4.247 +\newcommand{\ConjProj}{\mathord{\Conj}\rmtext{Proj}}
4.248 +\newcommand{\ImplCurry}{\mathord{\Impl}\rmtext{Curry}}
4.249 +\newcommand{\ImplUncurry}{\mathord{\Impl}\rmtext{Uncurry}}
4.250 +\newcommand{\CImplI}{\mathord{\Conj}\mathord{\Impl}\rmtext{I}}
4.251 +\newcommand{\CImplE}{\mathord{\Conj}\mathord{\Impl}\rmtext{E}}
4.252 +\newcommand{\Subclass}{\rmtext{Subclass}}
4.253 +\newcommand{\Subsort}{\rmtext{Subsort}}
4.254 +\newcommand{\VarSort}{\rmtext{VarSort}}
4.255 +\newcommand{\Arity}{\rmtext{Arity}}
4.256 +\newcommand{\SortMP}{\rmtext{SortMP}}
4.257 +\newcommand{\TopSort}{\rmtext{TopSort}}
4.258 +\newcommand{\OfSort}{\rmtext{OfSort}}
4.259 +
4.260 +\newcommand{\infr}{{\mathrel/}}
4.261 +\newcommand{\einfr}{{}{\mathrel/}}
4.262 +
4.263 +\newcommand{\drv}{\mathrel{\vdash}}
4.264 +\newcommand{\Drv}[1]{\mathrel{\mathord{\drv}_{#1}}}
4.265 +\newcommand{\Gdrv}{\Gam\drv}
4.266 +\newcommand{\edrv}{\mathop{\drv}\nolimits}
4.267 +\newcommand{\Edrv}[1]{\mathop{\drv}\nolimits_{#1}}
4.268 +\newcommand{\notEdrv}[1]{\mathop{\not\drv}\nolimits_{#1}}
4.269 +
4.270 +\newcommand{\lsem}{\lbrakk}
4.271 +\newcommand{\rsem}{\rbrakk}
4.272 +\newcommand{\sem}[1]{{\lsem #1\rsem}}
4.273 +
4.274 +\newcommand{\vld}{\mathrel{\models}}
4.275 +\newcommand{\Vld}[1]{\mathrel{\mathord{\models}_#1}}
4.276 +\newcommand{\Evld}[1]{\mathop{\vld}\nolimits_{#1}}
4.277 +\newcommand{\notEvld}[1]{\mathop{\not\vld}\nolimits_{#1}}
4.278 +
4.279 +\newcommand{\EQ}{\fct{EQ}}
4.280 +\newcommand{\IMPL}{\fct{IMPL}}
4.281 +\newcommand{\ALL}{\fct{ALL}}
4.282 +
4.283 +\newcommand{\extcv}{\mathrel{\unlhd}}
4.284 +\newcommand{\weakth}{\preceq}
4.285 +\newcommand{\eqvth}{\approx}
4.286 +\newcommand{\extdcli}{\mathrel{<_{\rm dcl}^1}}
4.287 +\newcommand{\extdcl}{\mathrel{\le_{\rm dcl}}}
4.288 +\newcommand{\extdfni}{\mathrel{<_{\rm dfn}^1}}
4.289 +\newcommand{\extdfn}{\mathrel{\le_{\rm dfn}}}
4.290 +\newcommand{\extsdfn}{\mathrel{\le_{\rm sdfn}}}
4.291 +\newcommand{\extqdfn}{\mathrel{\le_{\rm qdfn}}}
4.292 +
4.293 +\newcommand{\lvarbl}{\langle}
4.294 +\newcommand{\rvarbl}{\rangle}
4.295 +\newcommand{\varbl}[1]{{\lvarbl #1\rvarbl}}
4.296 +\newcommand{\up}{{\scriptstyle\mathord\uparrow}}
4.297 +\newcommand{\down}{{\scriptstyle\mathord\downarrow}}
4.298 +\newcommand{\Down}{{\mathord\downarrow}}
4.299 +
4.300 +
4.301 +\newcommand{\Sle}{{\mathrel{\le_S}}}
4.302 +\newcommand{\Classes}{\syn{Classes}}
4.303 +\newcommand{\ClassNames}{\syn{ClassNames}}
4.304 +\newcommand{\Sorts}{\syn{Sorts}}
4.305 +\newcommand{\TyVarNames}{\syn{TyVarNames}}
4.306 +\newcommand{\STyVars}{\syn{STyVars}}
4.307 +\newcommand{\STyArities}{\syn{STyArities}}
4.308 +\newcommand{\STypes}{\syn{STypes}}
4.309 +\newcommand{\SVars}{\syn{SVars}}
4.310 +\newcommand{\SConsts}{\syn{SConsts}}
4.311 +\newcommand{\STerms}{\syn{STerms}}
4.312 +\newcommand{\SForms}{\syn{SForms}}
4.313 +\newcommand{\SAxms}{\syn{SAxms}}
4.314 +\newcommand{\T}{{\cal T}}
4.315 +
4.316 +\newcommand{\cls}[1]{{\mathord{\sl #1}}}
4.317 +\newcommand{\intsrt}{\sqcap}
4.318 +\newcommand{\Intsrt}{{\mathop\sqcap}}
4.319 +\newcommand{\subcls}{\preceq}
4.320 +\newcommand{\Subcls}[1]{\mathrel{\subcls_{#1}}}
4.321 +\newcommand{\subsrt}{\sqsubseteq}
4.322 +\newcommand{\Subsrt}[1]{\mathrel{\subsrt_{#1}}}
4.323 +\newcommand{\subsrtp}{\sqsubset}
4.324 +\newcommand{\eqvsrt}{\approx}
4.325 +\newcommand{\topsrt}{\top}
4.326 +\newcommand{\srt}{\ty}
4.327 +
4.328 +\newcommand{\sct}[1]{{\bf #1}}
4.329 +\newcommand{\CLASSES}{\sct{classes}}
4.330 +\newcommand{\CLASSREL}{\sct{classrel}}
4.331 +\newcommand{\TYPES}{\sct{types}}
4.332 +\newcommand{\ARITIES}{\sct{arities}}
4.333 +\newcommand{\CONSTS}{\sct{consts}}
4.334 +\newcommand{\AXIOMS}{\sct{axioms}}
4.335 +\newcommand{\DEFNS}{\sct{defns}}
4.336 +\newcommand{\AXCLASS}{\sct{axclass}}
4.337 +\newcommand{\INSTANCE}{\sct{instance}}
4.338 +
4.339 +\newcommand{\Srt}{{\mathbin{\,:\,}}}
4.340 +\newcommand{\insrt}[2]{{\mathopen{(\!|} #1 \Srt #2 \mathclose{|\!)}}}
4.341 +\newcommand{\ofsrt}[2]{{\mathopen{\langle\!|} #1 \Srt #2 \mathclose{|\!\rangle}}}
4.342 +
4.343 +\newcommand{\injV}{{\iota_V}}
4.344 +\newcommand{\inj}{\iota}
4.345 +\newcommand{\injC}{{\iota_C}}
4.346 +\newcommand{\I}{{\cal I}}
4.347 +\newcommand{\C}{{\cal C}}
4.348 +
4.349 +\newcommand{\Sdrv}{\mathrel{\vdash\!\!\!\vdash}}
4.350 +\newcommand{\SDrv}[1]{\mathrel{\mathord{\Sdrv}_{#1}}}
4.351 +\newcommand{\SGdrv}{\Gam\Sdrv}
4.352 +\newcommand{\Sedrv}{\mathop{\Sdrv}\nolimits}
4.353 +\newcommand{\SEdrv}[1]{\mathop{\Sdrv}\nolimits_{#1}}
4.354 +
4.355 +\newcommand{\SSubclass}{\rmtext{S-Subclass}}
4.356 +\newcommand{\SSubsort}{\rmtext{S-Subsort}}
4.357 +\newcommand{\SVarSort}{\rmtext{S-VarSort}}
4.358 +\newcommand{\SArity}{\rmtext{S-Arity}}
4.359 +\newcommand{\SSortMP}{\rmtext{S-SortMP}}
4.360 +\newcommand{\STopSort}{\rmtext{S-TopSort}}
4.361 +\newcommand{\SOfSort}{\rmtext{S-OfSort}}
4.362 +
4.363 +
4.364 +\makeatother
4.365 +