summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/AxClass/axclass.tex

changeset 3167 | 4e1eae442821 |

child 4009 | 6d9bec7b0b9e |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/AxClass/axclass.tex Mon May 12 17:53:36 1997 +0200 @@ -0,0 +1,747 @@ + +\input{style} + +\begin{document} + +\title{Using Axiomatic Type Classes in Isabelle \\ a tutorial} +\author{Markus Wenzel} +%\date{29 August 1995} +\maketitle + +\Isa\ features a \Haskell-like type system with ordered type classes +already since 1991 (see \cite{Nipkow93}). Initially, classes mainly +served as a \E{syntactic tool} to formulate polymorphic object logics +in a clean way (like many-sorted \FOL, see +\cite[\S1.1.2--1.1.3]{Paulson94}). + +Applying classes at the \E{logical level} to provide a simple notion +of abstract theories and instantiations to concrete ones, has also +been long proposed (see \cite{Nipkow-slides} and +\cite[\S4]{Nipkow93}). At that time, \Isa\ still lacked built-in +support for these \E{axiomatic type classes}. More importantly, their +semantics was not yet fully fleshed out and unnecessarily complicated. + +How simple things really are has been shown in \cite[esp.\ +\S4]{Wenzel94} which also provided an implementation of the axclass +package that was eventually released with \Isa94. Unfortunately there +was a snag: That version of \Isa\ still contained an old conceptual +bug in the core machinery which caused theories to become inconsistent +after introducing empty sorts. Note that empty intersections of +axiomatic type classes easily occur, unless all basic classes are very +trivial. + +These problems prevented the axclass package to be used seriously --- +they have been fixed in \Isa95. + + +\section{Some simple examples} \label{sec:ex} + +Axiomatic type classes are a concept of \Isa's meta-logic. They may +be applied to any object-logic that directly uses the meta type +system. Subsequently, we present various examples that are formulated +within \Isa/\HOL\footnote{See also directory + \TT{HOL/AxClasses/Tutorial}.}, except the one of +\secref{sec:ex-natclass} which is in \Isa/\FOL\footnote{See also files + \TT{FOL/ex/NatClass.thy} and \TT{FOL/ex/NatClass.ML}.}. + + +\subsection{Semigroups} + +An axiomatic type class is simply a class of types that all meet +certain \E{axioms}. Thus, type classes may be also understood as type +predicates --- i.e.\ abstractions over a single type argument +$\alpha$. Class axioms typically contain polymorphic constants that +depend on this type $\alpha$. These \E{characteristic constants} +behave like operations associated with the ``carrier'' $\alpha$. + +We illustrate these basic concepts with the following theory +\TT{Semigroup}: + +\begin{ascbox} +Semigroup = HOL +\medskip +consts + "<*>" :: "['a, 'a] => 'a" (infixl 70)\medskip +axclass + semigroup < term + assoc "(x <*> y) <*> z = x <*> (y <*> z)"\medskip +end +\end{ascbox} + +\TT{Semigroup} first declares a polymorphic constant $\TIMES :: +[\alpha, \alpha] \To \alpha$ and then defines the class \TT{semigroup} +of all those types $\tau$ such that $\TIMES :: [\tau, \tau] \To \tau$ +is an associative operator\footnote{Note that $\TIMES$ is used here + instead of $*$, because the latter is already declared in theory + \TT{HOL} in a slightly different way.}. The axiom \TT{assoc} +contains exactly one type variable, which is invisible in the above +presentation, though. Also note that free term variables (like $x$, +$y$, $z$) are allowed for user convenience --- conceptually all of +these are bound by outermost universal quantifiers. + +\medskip + +In general, type classes may be used to describe \E{structures} with +exactly one carrier $\alpha$ and a fixed \E{signature}. Different +signatures require different classes. In the following theory +\TT{Semigroups}, class \TT{plus\_sg} represents semigroups of the form +$(\tau, \PLUS^\tau)$ while \TT{times\_sg} represents semigroups +$(\tau, \TIMES^\tau)$: + +\begin{ascbox} +Semigroups = HOL +\medskip +consts + "<+>" :: "['a, 'a] => 'a" (infixl 65) + "<*>" :: "['a, 'a] => 'a" (infixl 70) + assoc :: "(['a, 'a] => 'a) => bool"\medskip +defs + assoc_def "assoc f == ALL x y z. f (f x y) z = f x (f y z)"\medskip +axclass + plus_sg < term + plus_assoc "assoc (op <+>)"\medskip +axclass + times_sg < term + times_assoc "assoc (op <*>)"\medskip +end +\end{ascbox} + +Even if both classes \TT{plus\_sg} and \TT{times\_sg} represent +semigroups in a sense, they are not the same! + + +\subsection{Basic group theory} + +The meta type system of \Isa\ supports \E{intersections} and +\E{inclusions} of type classes. These directly correspond to +intersections and inclusions of type predicates in a purely set +theoretic sense. This is sufficient as a means to describe simple +hierarchies of structures. As an illustration, we use the well-known +example of semigroups, monoids, general groups and abelian groups. + + +\subsubsection{Monoids and Groups} + +First a small theory that provides some polymorphic constants to be +used later for the signature parts: + +\begin{ascbox} +Sigs = HOL +\medskip +consts + "<*>" :: "['a, 'a] => 'a" (infixl 70) + inverse :: "'a => 'a" + "1" :: "'a" ("1")\medskip +end +\end{ascbox} + +Next comes the theory \TT{Monoid} which defines class +\TT{monoid}\footnote{Note that multiple class axioms are allowed for + user convenience --- they simply represent the conjunction of their + respective universal closures.}: + +\begin{ascbox} +Monoid = Sigs +\medskip +axclass + monoid < term + assoc "(x <*> y) <*> z = x <*> (y <*> z)" + left_unit "1 <*> x = x" + right_unit "x <*> 1 = x"\medskip +end +\end{ascbox} + +So class \TT{monoid} contains exactly those types $\tau$ where $\TIMES +:: [\tau, \tau] \To \tau$ and $\TT{1} :: \tau$ are specified +appropriately, such that $\TIMES$ is associative and $\TT{1}$ is a +left and right unit for $\TIMES$. + +\medskip + +Independently of \TT{Monoid}, we now define theory \TT{Group} which +introduces a linear hierarchy of semigroups, general groups and +abelian groups: + +\begin{ascbox} +Group = Sigs +\medskip +axclass + semigroup < term + assoc "(x <*> y) <*> z = x <*> (y <*> z)"\brk +axclass + group < semigroup + left_unit "1 <*> x = x" + left_inverse "inverse x <*> x = 1"\medskip +axclass + agroup < group + commut "x <*> y = y <*> x"\medskip +end +\end{ascbox} + +Class \TT{group} inherits associativity of $\TIMES$ from +\TT{semigroup} and adds the other two group axioms. Similarly, +\TT{agroup} is defined as the subset of \TT{group} such that for all +of its elements $\tau$, the operation $\TIMES :: [\tau, \tau] \To +\tau$ is even commutative. + + +\subsubsection{Abstract reasoning} + +In a sense, axiomatic type classes may be viewed as \E{abstract + theories}. Above class definitions internally generate the +following abstract axioms: + +\begin{ascbox} +assoc: (?x::?'a::semigroup) <*> (?y::?'a::semigroup) + <*> (?z::?'a::semigroup) = ?x <*> (?y <*> ?z)\medskip +left_unit: 1 <*> (?x::?'a::group) = ?x +left_inverse: inverse (?x::?'a::group) <*> ?x = 1\medskip +commut: (?x::?'a::agroup) <*> (?y::?'a::agroup) = ?y <*> ?x +\end{ascbox} + +All of these contain type variables $\alpha :: c$ that are restricted +to types of some class $c$. These \E{sort constraints} express a +logical precondition for the whole formula. For example, \TT{assoc} +states that for all $\tau$, provided that $\tau :: \TT{semigroup}$, +the operation $\TIMES :: [\tau, \tau] \To \tau$ is associative. + +\medskip + +From a purely technical point of view, abstract axioms are just +ordinary \Isa-theorems (of \ML-type \TT{thm}). They may be used for +\Isa-proofs without special treatment. Such ``abstract proofs'' +usually yield new abstract theorems. For example, in theory \TT{Group} +we may derive: + +\begin{ascbox} +right_unit: (?x::?'a::group) <*> 1 = ?x +right_inverse: (?x::?'a::group) <*> inverse ?x = 1 +inverse_product: inverse ((?x::?'a::group) <*> (?y::?'a::group)) = + inverse ?y <*> inverse ?x +inverse_inv: inverse (inverse (?x::?'a::group)) = ?x +ex1_inverse: ALL x::?'a::group. EX! y::?'a::group. y <*> x = 1 +\end{ascbox} + +Abstract theorems (which include abstract axioms, of course) may be +instantiated to only those types $\tau$ where the appropriate class +membership $\tau :: c$ is known at \Isa's type signature level. Since +we have $\TT{agroup} \subseteq \TT{group} \subseteq \TT{semigroup}$ by +definition, all theorems of \TT{semigroup} and \TT{group} are +automatically inherited by \TT{group} and \TT{agroup}. + + +\subsubsection{Abstract instantiation} + +Until now, theories \TT{Monoid} and \TT{Group} were independent. +Forming their union $\TT{Monoid} + \TT{Group}$ we get the following +class hierarchy at the type signature level (left hand side): + +\begin{center} + \small + \unitlength 0.75mm + \begin{picture}(65,90)(0,-10) + \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} + \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}} + \put(15,5){\makebox(0,0){\tt agroup}} + \put(15,25){\makebox(0,0){\tt group}} + \put(15,45){\makebox(0,0){\tt semigroup}} + \put(30,65){\makebox(0,0){\tt term}} \put(50,45){\makebox(0,0){\tt + monoid}} + \end{picture} + \hspace{4em} + \begin{picture}(30,90)(0,0) + \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} + \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}} + \put(15,5){\makebox(0,0){\tt agroup}} + \put(15,25){\makebox(0,0){\tt group}} + \put(15,45){\makebox(0,0){\tt monoid}} + \put(15,65){\makebox(0,0){\tt semigroup}} + \put(15,85){\makebox(0,0){\tt term}} + \end{picture} +\end{center} + +We know by definition that $\TIMES$ is associative for monoids, i.e.\ +$\TT{monoid} \subseteq \TT{semigroup}$. Furthermore we have +\TT{assoc}, \TT{left\_unit} and \TT{right\_unit} for groups (where +\TT{right\_unit} is derivable from the group axioms), that is +$\TT{group} \subseteq \TT{monoid}$. This way we get the refined class +hierarchy shown above at the right hand side. + +The additional inclusions $\TT{monoid} \subseteq \TT{semigroup}$ and +$\TT{group} \subseteq \TT{monoid}$ are established by logical means +and have to be explicitly made known at the type signature level. This +is what the theory section \TT{instance} does. So we define +\TT{MonoidGroupInsts} as follows: + +\begin{ascbox} +MonoidGroupInsts = Monoid + Group +\medskip +instance + monoid < semigroup (Monoid.assoc)\medskip +instance + group < monoid (assoc, left_unit, right_unit)\medskip +end +\end{ascbox} + +The \TT{instance} section does really check that the class inclusions +(or type arities) to be added are derivable. To this end, it sets up a +suitable goal and attempts a proof with the help of some internal +axioms and user supplied theorems. These latter \E{witnesses} usually +should be appropriate type instances of the class axioms (as are +\TT{Monoid.assoc} and \TT{assoc}, \TT{left\_unit}, \TT{right\_unit} +above). + +The most important internal tool for instantiation proofs is the class +introduction rule that is automatically generated by \TT{axclass}. For +class \TT{group} this is axiom \TT{groupI}: + +\begin{ascbox} +groupI: [| OFCLASS(?'a::term, semigroup_class); + !!x::?'a::term. 1 <*> x = x; + !!x::?'a::term. inverse x <*> x = 1 |] + ==> OFCLASS(?'a::term, group_class) +\end{ascbox} + +There are also axioms \TT{monoidI}, \TT{semigroupI} and \TT{agroupI} +of a similar form. Note that $\TT{OFCLASS}(\tau, c \TT{\_class})$ +expresses class membership $\tau :: c$ as a proposition of the +meta-logic. + + +\subsubsection{Concrete instantiation} + +So far we have covered the case of \TT{instance $c_1$ < $c_2$} that +could be described as \E{abstract instantiation} --- $c_1$ is more +special than $c_2$ and thus an instance of $c_2$. Even more +interesting for practical applications are \E{concrete instantiations} +of axiomatic type classes. That is, certain simple schemes $(\alpha_1, +\ldots, \alpha_n)t :: c$ of class membership may be transferred to +\Isa's type signature level. This form of \TT{instance} is a ``safe'' +variant of the old-style \TT{arities} theory section. + +As an example, we show that type \TT{bool} with exclusive-or as +operation $\TIMES$, identity as \TT{inverse}, and \TT{False} as \TT{1} +forms an abelian group. We first define theory \TT{Xor}: + +\begin{ascbox} +Xor = Group +\medskip +defs + prod_bool_def "x <*> y == x ~= (y::bool)" + inverse_bool_def "inverse x == x::bool" + unit_bool_def "1 == False"\medskip +end +\end{ascbox} + +It is important to note that above \TT{defs} are just overloaded +meta-level constant definitions. In particular, type classes are not +yet involved at all! This form of constant definition with overloading +(and optional primitive recursion over types) would be also possible +in traditional versions of \HOL\ that lack type classes. +% (see FIXME <foundation> for more details) +Nonetheless, such definitions are best applied in the context of +classes. + +\medskip + +Since we chose the \TT{defs} of theory \TT{Xor} suitably, the class +membership $\TT{bool} :: \TT{agroup}$ is now derivable as follows: + +\begin{ascbox} +open AxClass; +goal_arity Xor.thy ("bool", [], "agroup"); +\out{Level 0} +\out{OFCLASS(bool, agroup_class)} +\out{ 1. OFCLASS(bool, agroup_class)}\brk +by (axclass_tac Xor.thy []); +\out{Level 1} +\out{OFCLASS(bool, agroup_class)} +\out{ 1. !!(x::bool) (y::bool) z::bool. x <*> y <*> z = x <*> (y <*> z)} +\out{ 2. !!x::bool. 1 <*> x = x} +\out{ 3. !!x::bool. inverse x <*> x = 1} +\out{ 4. !!(x::bool) y::bool. x <*> y = y <*> x} +\end{ascbox} + +The tactic \TT{axclass\_tac} has applied \TT{agroupI} internally to +expand the class definition. It now remains to be shown that the +\TT{agroup} axioms hold for bool. To this end, we expand the +definitions of \TT{Xor} and solve the new subgoals by \TT{fast\_tac} +of \HOL: + +\begin{ascbox} +by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inverse_bool_def, + Xor.unit_bool_def]); +\out{Level 2} +\out{OFCLASS(bool, agroup_class)} +\out{ 1. !!(x::bool) (y::bool) z::bool. x ~= y ~= z = (x ~= (y ~= z))} +\out{ 2. !!x::bool. False ~= x = x} +\out{ 3. !!x::bool. x ~= x = False} +\out{ 4. !!(x::bool) y::bool. x ~= y = (y ~= x)} +by (ALLGOALS (fast_tac HOL_cs)); +\out{Level 3} +\out{OFCLASS(bool, agroup_class)} +\out{No subgoals!} +qed "bool_in_agroup"; +\out{val bool_in_agroup = "OFCLASS(bool, agroup_class)"} +\end{ascbox} + +The result is theorem $\TT{OFCLASS}(\TT{bool}, \TT{agroup\_class})$ +which expresses $\TT{bool} :: \TT{agroup}$ as a meta-proposition. This +is not yet known at the type signature level, though. + +\medskip + +What we have done here by hand, can be also performed via +\TT{instance} in a similar way behind the scenes. This may look as +follows\footnote{Subsequently, theory \TT{Xor} is no longer + required.}: + +\begin{ascbox} +BoolGroupInsts = Group +\medskip +defs + prod_bool_def "x <*> y == x ~= (y::bool)" + inverse_bool_def "inverse x == x::bool" + unit_bool_def "1 == False"\medskip +instance + bool :: agroup \{| ALLGOALS (fast_tac HOL_cs) |\}\medskip +end +\end{ascbox} + +This way, we have $\TT{bool} :: \TT{agroup}$ in the type signature of +\TT{BoolGroupInsts}, and all abstract group theorems are transferred +to \TT{bool} for free. + +Similarly, we could now also instantiate our group theory classes to +many other concrete types. For example, $\TT{int} :: \TT{agroup}$ (by +defining $\TIMES$ as addition, \TT{inverse} as negation and \TT{1} as +zero, say) or $\TT{list} :: (\TT{term})\TT{semigroup}$ (e.g.\ if +$\TIMES$ is list append). Thus, the characteristic constants $\TIMES$, +\TT{inverse}, \TT{1} really become overloaded, i.e.\ have different +meanings on different types. + + +\subsubsection{Lifting and Functors} + +As already mentioned above, \HOL-like systems not only support +overloaded definitions of polymorphic constants (without requiring +type classes), but even primitive recursion over types. That is, +definitional equations $c^\tau \Eq t$ may also contain constants of +name $c$ on the RHS --- provided that these have types that are +strictly simpler (structurally) than $\tau$. + +This feature enables us to \E{lift operations}, e.g.\ to Cartesian +products, direct sums or function spaces. Below, theory +\TT{ProdGroupInsts} lifts $\TIMES$ componentwise to two-place +Cartesian products $\alpha \times \beta$: + +\begin{ascbox} +ProdGroupInsts = Prod + Group +\medskip +defs + prod_prod_def "p <*> q == (fst p <*> fst q, snd p <*> snd q)"\medskip +instance + "*" :: (semigroup, semigroup) semigroup + \{| simp_tac (prod_ss addsimps [assoc]) 1 |\} +end +\end{ascbox} + +Note that \TT{prod\_prod\_def} basically has the form $\edrv +{\TIMES}^{\alpha \times \beta} \Eq \ldots {\TIMES}^\alpha \ldots +{\TIMES}^\beta \ldots$, i.e.\ the recursive occurrences +$\TIMES^\alpha$ and $\TIMES^\beta$ are really at ``simpler'' types. + +It is very easy to see that associativity of $\TIMES^\alpha$, +$\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence +the two-place type constructor $\times$ maps semigroups into +semigroups. This fact is proven and put into \Isa's type signature by +above \TT{instance} section. + +\medskip + +Thus, if we view class instances as ``structures'', overloaded +constant definitions with primitive recursion over types indirectly +provide some kind of ``functors'' (mappings between abstract theories, +that is). + + +\subsection{Syntactic classes} + +There is still a feature of \Isa's type system left that we have not +yet used: When declaring polymorphic constants $c :: \tau$, the type +variables occurring in $\tau$ may be constrained by type classes (or +even general sorts). Note that by default, in \Isa/\HOL\ the +declaration: + +\begin{ascbox} + <*> :: ['a, 'a] => 'a +\end{ascbox} + +is actually an abbreviation for: + +\begin{ascbox} + <*> :: ['a::term, 'a::term] => 'a::term +\end{ascbox} + +Since class \TT{term} is the universal class of \HOL, this is not +really a restriction at all. A less trivial example is the following +theory \TT{Product}: + +\begin{ascbox} +Product = HOL +\medskip +axclass + product < term\medskip +consts + "<*>" :: "['a::product, 'a] => 'a" (infixl 70)\medskip +end +\end{ascbox} + +Here class \TT{product} is defined as subclass of \TT{term}, but +without any additional axioms. This effects in logical equivalence of +\TT{product} and \TT{term}, since \TT{productI} is as follows: + +\begin{ascbox} +productI: OFCLASS(?'a::logic, term_class) ==> + OFCLASS(?'a::logic, product_class) +\end{ascbox} + +I.e.\ $\TT{term} \subseteq \TT{product}$. The converse inclusion is +already contained in the type signature of theory \TT{Product}. + +Now, what is the difference of declaring $\TIMES :: [\alpha :: +\TT{product}, \alpha] \To \alpha$ vs.\ declaring $\TIMES :: [\alpha :: +\TT{term}, \alpha] \To \alpha$? In this special case (where +$\TT{product} \Eq \TT{term}$), it should be obvious that both +declarations are the same from the logic's point of view. It is even +most sensible in the general case not to attach any \E{logical} +meaning to sort constraints occurring in constant \E{declarations} +(see \cite[page 79]{Wenzel94} for more details). + +On the other hand there are syntactic differences, of course. +Constants $\TIMES^\tau$ are rejected by the type checker, unless $\tau +:: \TT{product}$ is part of the type signature. In our example, this +arity may be always added when required by means of a trivial +\TT{instance}. + +Thus, we can follow this discipline: Overloaded polymorphic constants +have their type arguments restricted to an associated (logically +trivial) class $c$. Only immediately before \E{specifying} these +constants on a certain type $\tau$ do we instantiate $\tau :: c$. + +This is done for class \TT{product} and type \TT{bool} in theory +\TT{ProductInsts} below: + +\begin{ascbox} +ProductInsts = Product +\medskip +instance + bool :: product\medskip +defs + prod_bool_def "x <*> y == x & y::bool"\medskip +end +\end{ascbox} + +Note that \TT{instance bool ::\ product} does not require any +witnesses, since this statement is logically trivial. Nonetheless, +\TT{instance} really performs a proof. + +Only after $\TT{bool} :: \TT{product}$ is made known to the type +checker, does \TT{prod\_bool\_def} become syntactically well-formed. + +\medskip + +It is very important to see that above \TT{defs} are not directly +connected with \TT{instance} at all! We were just following our +convention to specify $\TIMES$ on \TT{bool} after having instantiated +$\TT{bool} :: \TT{product}$. \Isa\ does not require these definitions, +which is in contrast to programming languages like \Haskell. + +\medskip + +While \Isa\ type classes and those of \Haskell\ are almost the same as +far as type checking and type inference are concerned, there are major +semantic differences. \Haskell\ classes require their instances to +\E{provide operations} of certain \E{names}. Therefore, its +\TT{instance} has a \TT{where} part that tells the system what these +``member functions'' should be. + +This style of \TT{instance} won't make much sense in \Isa, because its +meta-logic has no corresponding notion of ``providing operations'' or +``names''. + + +\subsection{Defining natural numbers in \FOL} +\label{sec:ex-natclass} + +Axiomatic type classes abstract over exactly one type argument. Thus, +any \E{axiomatic} theory extension where each axiom refers to at most +one type variable, may be trivially turned into a \E{definitional} +one. + +We illustrate this with the natural numbers in \Isa/\FOL: + +\begin{ascbox} +NatClass = FOL +\medskip +consts + "0" :: "'a" ("0") + Suc :: "'a => 'a" + rec :: "['a, 'a, ['a, 'a] => 'a] => 'a"\medskip +axclass + nat < term + induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" + Suc_inject "Suc(m) = Suc(n) ==> m = n" + Suc_neq_0 "Suc(m) = 0 ==> R" + rec_0 "rec(0, a, f) = a" + rec_Suc "rec(Suc(m), a, f) = f(m, rec(m, a, f))"\medskip +consts + "+" :: "['a::nat, 'a] => 'a" (infixl 60)\medskip +defs + add_def "m + n == rec(m, n, %x y. Suc(y))"\medskip +end +\end{ascbox} + +\TT{NatClass} is an abstract version of \TT{Nat}\footnote{See + directory \TT{FOL/ex}.}. Basically, we have just replaced all +occurrences of \E{type} \TT{nat} by $\alpha$ and used the natural +number axioms to define \E{class} \TT{nat}\footnote{There's a snag: + The original recursion operator \TT{rec} had to be made monomorphic, + in a sense.}. Thus class \TT{nat} contains exactly those types +$\tau$ that are isomorphic to ``the'' natural numbers (with signature +\TT{0}, \TT{Suc}, \TT{rec}). + +Furthermore, theory \TT{NatClass} defines an ``abstract constant'' $+$ +based on class \TT{nat}. + +\medskip + +What we have done here can be also viewed as \E{type specification}. +Of course, it still remains open if there is some type at all that +meets the class axioms. Now a very nice property of axiomatic type +classes is, that abstract reasoning is always possible --- independent +of satisfiability. The meta-logic won't break, even if some class (or +general sort) turns out to be empty (``inconsistent'') +later\footnote{As a consequence of an old bug, this is \E{not} true + for pre-\Isa95 versions.}. + +For example, we may derive the following abstract natural numbers +theorems: + +\begin{ascbox} +add_0: 0 + (?n::?'a::nat) = ?n +add_Suc: Suc(?m::?'a::nat) + (?n::?'a::nat) = Suc(?m + ?n) +\end{ascbox} + +See also file \TT{FOL/ex/NatClass.ML}. Note that this required only +some trivial modifications of the original \TT{Nat.ML}. + + +\section{The user interface of \Isa's axclass package} + +The actual axiomatic type class package of \Isa/\Pure\ mainly consists +of two new theory sections: \TT{axclass} and \TT{instance}. Some +typical applications of these have already been demonstrated in +\secref{sec:ex}, below their syntax and semantics are presented more +completely. + + +\subsection{The \TT{axclass} section} + +Within theory files, \TT{axclass} introduces an axiomatic type class +definition. Its concrete syntax is: + +\begin{matharray}{l} + \TT{axclass} \\ + \ \ c \TT{ < } c_1\TT, \ldots\TT, c_n \\ + \ \ \idt{id}_1\ \idt{axm}_1 \\ + \ \ \vdots \\ + \ \ \idt{id}_m\ \idt{axm}_m +\end{matharray} + +Where $c, c_1, \ldots, c_n$ are classes (category $\idt{id}$ or +$\idt{string}$) and $\idt{axm}_1, \ldots, \idt{axm}_m$ (with $m \ge +0$) are formulas (category $\idt{string}$). + +Class $c$ has to be new, and sort $\{c_1, \ldots, c_n\}$ a subsort of +\TT{logic}. Each class axiom $\idt{axm}_j$ may contain any term +variables, but at most one type variable (which need not be the same +for all axioms). The sort of this type variable has to be a supersort +of $\{c_1, \ldots, c_n\}$. + +\medskip + +The \TT{axclass} section declares $c$ as subclass of $c_1, \ldots, +c_n$ to the type signature. + +Furthermore, $\idt{axm}_1, \ldots, \idt{axm}_m$ are turned into the +``abstract axioms'' of $c$ with names $\idt{id}_1, \ldots, +\idt{id}_m$. This is done by replacing all occurring type variables +by $\alpha :: c$. Original axioms that do not contain any type +variable will be prefixed by the logical precondition +$\TT{OFCLASS}(\alpha :: \TT{logic}, c\TT{\_class})$. + +Another axiom of name $c\TT{I}$ --- the ``class $c$ introduction +rule'' --- is built from the respective universal closures of +$\idt{axm}_1, \ldots, \idt{axm}_m$ appropriately. + + +\subsection{The \TT{instance} section} + +Section \TT{instance} proves class inclusions or type arities at the +logical level and then transfers these into the type signature. + +Its concrete syntax is: + +\begin{matharray}{l} + \TT{instance} \\ + \ \ [\ c_1 \TT{ < } c_2 \ |\ + t \TT{ ::\ (}\idt{sort}_1\TT, \ldots \TT, \idt{sort}_n\TT) \idt{sort}\ ] \\ + \ \ [\ \TT(\idt{name}_1 \TT, \ldots\TT, \idt{name}_m\TT)\ ] \\ + \ \ [\ \TT{\{|} \idt{text} \TT{|\}}\ ] +\end{matharray} + +Where $c_1, c_2$ are classes and $t$ is an $n$-place type constructor +(all of category $\idt{id}$ or $\idt{string})$. Furthermore, +$\idt{sort}_i$ are sorts in the usual \Isa-syntax. + +\medskip + +Internally, \TT{instance} first sets up an appropriate goal that +expresses the class inclusion or type arity as a meta-proposition. +Then tactic \TT{AxClass.axclass\_tac} is applied with all preceding +meta-definitions of the current theory file and the user-supplied +witnesses. The latter are $\idt{name}_1, \ldots, \idt{name}_m$, where +$\idt{id}$ refers to an \ML-name of a theorem, and $\idt{string}$ to an +axiom of the current theory node\footnote{Thus, the user may reference + axioms from above this \TT{instance} in the theory file. Note + that new axioms appear at the \ML-toplevel only after the file is + processed completely.}. + +Tactic \TT{AxClass.axclass\_tac} first unfolds the class definition by +resolving with rule $c\TT{I}$, and then applies the witnesses +according to their form: Meta-definitions are unfolded, all other +formulas are repeatedly resolved\footnote{This is done in a way that + enables proper object-\E{rules} to be used as witnesses for + corresponding class axioms.} with. + +The final optional argument $\idt{text}$ is \ML-code of an arbitrary +user tactic which is applied last to any remaining goals. + +\medskip + +Because of the complexity of \TT{instance}'s witnessing mechanisms, +new users of the axclass package are advised to only use the simple +form $\TT{instance}\ \ldots\ (\idt{id}_1, \ldots, \idt{id}_m)$, where +the identifiers refer to theorems that are appropriate type instances +of the class axioms. This typically requires an auxiliary theory, +though, which defines some constants and then proves these witnesses. + + +\begin{thebibliography}{} + +\bibitem[Nipkow, 1993a]{Nipkow-slides} T. Nipkow. Axiomatic Type + Classes (in Isabelle). Presentation at the workshop \E{Types for + Proof and Programs}, Nijmegen, 1993. + +\bibitem[Nipkow, 1993b]{Nipkow93} T. Nipkow. Order-Sorted Polymorphism + in Isabelle. In G. Huet, G. Plotkin, editors, \E{Logical + Environments}, pp.\ 164--188, Cambridge University Press, 1993. + +\bibitem[Paulson, 1994]{Paulson94} L.C. Paulson. \E{Isabelle --- A + Generic Theorem Prover}. LNCS 828, 1994. + +\bibitem[Wenzel, 1994]{Wenzel94} M. Wenzel. \E{Axiomatische + Typ-Klassen in Isabelle}. Diplom\-arbeit, TU München, 1994. + +\end{thebibliography} + +\end{document}