doc-src/AxClass/axclass.tex
author wenzelm
Tue, 20 May 1997 19:29:50 +0200
changeset 3257 4e3724e0659f
parent 3167 4e1eae442821
child 4009 6d9bec7b0b9e
permissions -rw-r--r--
README generation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3167
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     1
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     2
\input{style}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     3
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     4
\begin{document}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     5
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     6
\title{Using Axiomatic Type Classes in Isabelle \\ a tutorial}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     7
\author{Markus Wenzel}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     8
%\date{29 August 1995}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
     9
\maketitle
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    10
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    11
\Isa\ features a \Haskell-like type system with ordered type classes
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    12
already since 1991 (see \cite{Nipkow93}). Initially, classes mainly
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    13
served as a \E{syntactic tool} to formulate polymorphic object logics
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    14
in a clean way (like many-sorted \FOL, see
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    15
\cite[\S1.1.2--1.1.3]{Paulson94}).
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    16
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    17
Applying classes at the \E{logical level} to provide a simple notion
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    18
of abstract theories and instantiations to concrete ones, has also
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    19
been long proposed (see \cite{Nipkow-slides} and
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    20
\cite[\S4]{Nipkow93}). At that time, \Isa\ still lacked built-in
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    21
support for these \E{axiomatic type classes}. More importantly, their
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    22
semantics was not yet fully fleshed out and unnecessarily complicated.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    23
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    24
How simple things really are has been shown in \cite[esp.\ 
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    25
\S4]{Wenzel94} which also provided an implementation of the axclass
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    26
package that was eventually released with \Isa94. Unfortunately there
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    27
was a snag: That version of \Isa\ still contained an old conceptual
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    28
bug in the core machinery which caused theories to become inconsistent
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    29
after introducing empty sorts. Note that empty intersections of
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    30
axiomatic type classes easily occur, unless all basic classes are very
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    31
trivial.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    32
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    33
These problems prevented the axclass package to be used seriously ---
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    34
they have been fixed in \Isa95.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    35
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    36
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    37
\section{Some simple examples} \label{sec:ex}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    38
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    39
Axiomatic type classes are a concept of \Isa's meta-logic.  They may
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    40
be applied to any object-logic that directly uses the meta type
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    41
system. Subsequently, we present various examples that are formulated
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    42
within \Isa/\HOL\footnote{See also directory
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    43
  \TT{HOL/AxClasses/Tutorial}.}, except the one of
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    44
\secref{sec:ex-natclass} which is in \Isa/\FOL\footnote{See also files
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    45
  \TT{FOL/ex/NatClass.thy} and \TT{FOL/ex/NatClass.ML}.}.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    46
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    47
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    48
\subsection{Semigroups}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    49
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    50
An axiomatic type class is simply a class of types that all meet
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    51
certain \E{axioms}. Thus, type classes may be also understood as type
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    52
predicates --- i.e.\ abstractions over a single type argument
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    53
$\alpha$.  Class axioms typically contain polymorphic constants that
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    54
depend on this type $\alpha$. These \E{characteristic constants}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    55
behave like operations associated with the ``carrier'' $\alpha$.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    56
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    57
We illustrate these basic concepts with the following theory
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    58
\TT{Semigroup}:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    59
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    60
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    61
Semigroup = HOL +\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    62
consts
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    63
  "<*>"         :: "['a, 'a] => 'a"             (infixl 70)\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    64
axclass
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    65
  semigroup < term
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    66
  assoc         "(x <*> y) <*> z = x <*> (y <*> z)"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    67
end
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    68
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    69
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    70
\TT{Semigroup} first declares a polymorphic constant $\TIMES ::
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    71
[\alpha, \alpha] \To \alpha$ and then defines the class \TT{semigroup}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    72
of all those types $\tau$ such that $\TIMES :: [\tau, \tau] \To \tau$
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    73
is an associative operator\footnote{Note that $\TIMES$ is used here
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    74
  instead of $*$, because the latter is already declared in theory
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    75
  \TT{HOL} in a slightly different way.}. The axiom \TT{assoc}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    76
contains exactly one type variable, which is invisible in the above
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    77
presentation, though.  Also note that free term variables (like $x$,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    78
$y$, $z$) are allowed for user convenience --- conceptually all of
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    79
these are bound by outermost universal quantifiers.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    80
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    81
\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    82
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    83
In general, type classes may be used to describe \E{structures} with
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    84
exactly one carrier $\alpha$ and a fixed \E{signature}. Different
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    85
signatures require different classes. In the following theory
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    86
\TT{Semigroups}, class \TT{plus\_sg} represents semigroups of the form
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    87
$(\tau, \PLUS^\tau)$ while \TT{times\_sg} represents semigroups
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    88
$(\tau, \TIMES^\tau)$:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    89
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    90
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    91
Semigroups = HOL +\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    92
consts
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    93
  "<+>"         :: "['a, 'a] => 'a"             (infixl 65)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    94
  "<*>"         :: "['a, 'a] => 'a"             (infixl 70)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    95
  assoc         :: "(['a, 'a] => 'a) => bool"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    96
defs
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    97
  assoc_def     "assoc f == ALL x y z. f (f x y) z = f x (f y z)"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    98
axclass
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
    99
  plus_sg < term
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   100
  plus_assoc    "assoc (op <+>)"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   101
axclass
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   102
  times_sg < term
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   103
  times_assoc   "assoc (op <*>)"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   104
end
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   105
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   106
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   107
Even if both classes \TT{plus\_sg} and \TT{times\_sg} represent
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   108
semigroups in a sense, they are not the same!
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   109
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   110
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   111
\subsection{Basic group theory}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   112
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   113
The meta type system of \Isa\ supports \E{intersections} and
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   114
\E{inclusions} of type classes. These directly correspond to
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   115
intersections and inclusions of type predicates in a purely set
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   116
theoretic sense. This is sufficient as a means to describe simple
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   117
hierarchies of structures.  As an illustration, we use the well-known
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   118
example of semigroups, monoids, general groups and abelian groups.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   119
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   120
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   121
\subsubsection{Monoids and Groups}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   122
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   123
First a small theory that provides some polymorphic constants to be
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   124
used later for the signature parts:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   125
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   126
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   127
Sigs = HOL +\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   128
consts
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   129
  "<*>"     :: "['a, 'a] => 'a"       (infixl 70)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   130
  inverse   :: "'a => 'a"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   131
  "1"       :: "'a"                   ("1")\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   132
end
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   133
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   134
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   135
Next comes the theory \TT{Monoid} which defines class
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   136
\TT{monoid}\footnote{Note that multiple class axioms are allowed for
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   137
  user convenience --- they simply represent the conjunction of their
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   138
  respective universal closures.}:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   139
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   140
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   141
Monoid = Sigs +\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   142
axclass
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   143
  monoid < term
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   144
  assoc         "(x <*> y) <*> z = x <*> (y <*> z)"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   145
  left_unit     "1 <*> x = x"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   146
  right_unit    "x <*> 1 = x"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   147
end
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   148
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   149
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   150
So class \TT{monoid} contains exactly those types $\tau$ where $\TIMES
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   151
:: [\tau, \tau] \To \tau$ and $\TT{1} :: \tau$ are specified
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   152
appropriately, such that $\TIMES$ is associative and $\TT{1}$ is a
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   153
left and right unit for $\TIMES$.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   154
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   155
\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   156
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   157
Independently of \TT{Monoid}, we now define theory \TT{Group} which
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   158
introduces a linear hierarchy of semigroups, general groups and
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   159
abelian groups:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   160
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   161
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   162
Group = Sigs +\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   163
axclass
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   164
  semigroup < term
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   165
  assoc         "(x <*> y) <*> z = x <*> (y <*> z)"\brk
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   166
axclass
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   167
  group < semigroup
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   168
  left_unit     "1 <*> x = x"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   169
  left_inverse  "inverse x <*> x = 1"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   170
axclass
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   171
  agroup < group
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   172
  commut        "x <*> y = y <*> x"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   173
end
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   174
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   175
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   176
Class \TT{group} inherits associativity of $\TIMES$ from
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   177
\TT{semigroup} and adds the other two group axioms. Similarly,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   178
\TT{agroup} is defined as the subset of \TT{group} such that for all
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   179
of its elements $\tau$, the operation $\TIMES :: [\tau, \tau] \To
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   180
\tau$ is even commutative.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   181
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   182
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   183
\subsubsection{Abstract reasoning}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   184
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   185
In a sense, axiomatic type classes may be viewed as \E{abstract
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   186
  theories}.  Above class definitions internally generate the
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   187
following abstract axioms:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   188
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   189
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   190
assoc:        (?x::?'a::semigroup) <*> (?y::?'a::semigroup)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   191
                <*> (?z::?'a::semigroup) = ?x <*> (?y <*> ?z)\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   192
left_unit:    1 <*> (?x::?'a::group) = ?x
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   193
left_inverse: inverse (?x::?'a::group) <*> ?x = 1\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   194
commut:       (?x::?'a::agroup) <*> (?y::?'a::agroup) = ?y <*> ?x
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   195
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   196
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   197
All of these contain type variables $\alpha :: c$ that are restricted
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   198
to types of some class $c$. These \E{sort constraints} express a
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   199
logical precondition for the whole formula. For example, \TT{assoc}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   200
states that for all $\tau$, provided that $\tau :: \TT{semigroup}$,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   201
the operation $\TIMES :: [\tau, \tau] \To \tau$ is associative.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   202
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   203
\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   204
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   205
From a purely technical point of view, abstract axioms are just
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   206
ordinary \Isa-theorems (of \ML-type \TT{thm}). They may be used for
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   207
\Isa-proofs without special treatment. Such ``abstract proofs''
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   208
usually yield new abstract theorems. For example, in theory \TT{Group}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   209
we may derive:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   210
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   211
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   212
right_unit:      (?x::?'a::group) <*> 1 = ?x
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   213
right_inverse:   (?x::?'a::group) <*> inverse ?x = 1
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   214
inverse_product: inverse ((?x::?'a::group) <*> (?y::?'a::group)) =
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   215
                   inverse ?y <*> inverse ?x
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   216
inverse_inv:     inverse (inverse (?x::?'a::group)) = ?x
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   217
ex1_inverse:     ALL x::?'a::group. EX! y::?'a::group. y <*> x = 1
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   218
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   219
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   220
Abstract theorems (which include abstract axioms, of course) may be
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   221
instantiated to only those types $\tau$ where the appropriate class
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   222
membership $\tau :: c$ is known at \Isa's type signature level.  Since
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   223
we have $\TT{agroup} \subseteq \TT{group} \subseteq \TT{semigroup}$ by
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   224
definition, all theorems of \TT{semigroup} and \TT{group} are
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   225
automatically inherited by \TT{group} and \TT{agroup}.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   226
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   227
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   228
\subsubsection{Abstract instantiation}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   229
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   230
Until now, theories \TT{Monoid} and \TT{Group} were independent.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   231
Forming their union $\TT{Monoid} + \TT{Group}$ we get the following
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   232
class hierarchy at the type signature level (left hand side):
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   233
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   234
\begin{center}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   235
  \small
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   236
  \unitlength 0.75mm
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   237
  \begin{picture}(65,90)(0,-10)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   238
    \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   239
    \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   240
    \put(15,5){\makebox(0,0){\tt agroup}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   241
    \put(15,25){\makebox(0,0){\tt group}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   242
    \put(15,45){\makebox(0,0){\tt semigroup}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   243
    \put(30,65){\makebox(0,0){\tt term}} \put(50,45){\makebox(0,0){\tt
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   244
    monoid}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   245
  \end{picture}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   246
  \hspace{4em}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   247
  \begin{picture}(30,90)(0,0)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   248
    \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   249
    \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   250
    \put(15,5){\makebox(0,0){\tt agroup}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   251
    \put(15,25){\makebox(0,0){\tt group}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   252
    \put(15,45){\makebox(0,0){\tt monoid}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   253
    \put(15,65){\makebox(0,0){\tt semigroup}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   254
    \put(15,85){\makebox(0,0){\tt term}}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   255
  \end{picture}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   256
\end{center}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   257
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   258
We know by definition that $\TIMES$ is associative for monoids, i.e.\ 
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   259
$\TT{monoid} \subseteq \TT{semigroup}$. Furthermore we have
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   260
\TT{assoc}, \TT{left\_unit} and \TT{right\_unit} for groups (where
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   261
\TT{right\_unit} is derivable from the group axioms), that is
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   262
$\TT{group} \subseteq \TT{monoid}$. This way we get the refined class
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   263
hierarchy shown above at the right hand side.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   264
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   265
The additional inclusions $\TT{monoid} \subseteq \TT{semigroup}$ and
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   266
$\TT{group} \subseteq \TT{monoid}$ are established by logical means
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   267
and have to be explicitly made known at the type signature level. This
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   268
is what the theory section \TT{instance} does. So we define
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   269
\TT{MonoidGroupInsts} as follows:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   270
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   271
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   272
MonoidGroupInsts = Monoid + Group +\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   273
instance
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   274
  monoid < semigroup            (Monoid.assoc)\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   275
instance
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   276
  group < monoid                (assoc, left_unit, right_unit)\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   277
end
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   278
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   279
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   280
The \TT{instance} section does really check that the class inclusions
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   281
(or type arities) to be added are derivable. To this end, it sets up a
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   282
suitable goal and attempts a proof with the help of some internal
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   283
axioms and user supplied theorems. These latter \E{witnesses} usually
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   284
should be appropriate type instances of the class axioms (as are
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   285
\TT{Monoid.assoc} and \TT{assoc}, \TT{left\_unit}, \TT{right\_unit}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   286
above).
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   287
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   288
The most important internal tool for instantiation proofs is the class
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   289
introduction rule that is automatically generated by \TT{axclass}. For
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   290
class \TT{group} this is axiom \TT{groupI}:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   291
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   292
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   293
groupI:   [| OFCLASS(?'a::term, semigroup_class);
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   294
             !!x::?'a::term. 1 <*> x = x;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   295
             !!x::?'a::term. inverse x <*> x = 1 |]
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   296
          ==> OFCLASS(?'a::term, group_class)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   297
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   298
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   299
There are also axioms \TT{monoidI}, \TT{semigroupI} and \TT{agroupI}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   300
of a similar form.  Note that $\TT{OFCLASS}(\tau, c \TT{\_class})$
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   301
expresses class membership $\tau :: c$ as a proposition of the
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   302
meta-logic.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   303
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   304
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   305
\subsubsection{Concrete instantiation}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   306
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   307
So far we have covered the case of \TT{instance $c_1$ < $c_2$} that
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   308
could be described as \E{abstract instantiation} --- $c_1$ is more
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   309
special than $c_2$ and thus an instance of $c_2$. Even more
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   310
interesting for practical applications are \E{concrete instantiations}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   311
of axiomatic type classes. That is, certain simple schemes $(\alpha_1,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   312
\ldots, \alpha_n)t :: c$ of class membership may be transferred to
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   313
\Isa's type signature level. This form of \TT{instance} is a ``safe''
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   314
variant of the old-style \TT{arities} theory section.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   315
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   316
As an example, we show that type \TT{bool} with exclusive-or as
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   317
operation $\TIMES$, identity as \TT{inverse}, and \TT{False} as \TT{1}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   318
forms an abelian group. We first define theory \TT{Xor}:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   319
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   320
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   321
Xor = Group +\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   322
defs
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   323
  prod_bool_def     "x <*> y   == x ~= (y::bool)"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   324
  inverse_bool_def  "inverse x == x::bool"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   325
  unit_bool_def     "1         == False"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   326
end
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   327
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   328
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   329
It is important to note that above \TT{defs} are just overloaded
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   330
meta-level constant definitions. In particular, type classes are not
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   331
yet involved at all! This form of constant definition with overloading
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   332
(and optional primitive recursion over types) would be also possible
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   333
in traditional versions of \HOL\ that lack type classes.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   334
% (see FIXME <foundation> for more details)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   335
Nonetheless, such definitions are best applied in the context of
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   336
classes.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   337
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   338
\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   339
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   340
Since we chose the \TT{defs} of theory \TT{Xor} suitably, the class
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   341
membership $\TT{bool} :: \TT{agroup}$ is now derivable as follows:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   342
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   343
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   344
open AxClass;
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   345
goal_arity Xor.thy ("bool", [], "agroup");
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   346
\out{Level 0}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   347
\out{OFCLASS(bool, agroup_class)}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   348
\out{ 1. OFCLASS(bool, agroup_class)}\brk
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   349
by (axclass_tac Xor.thy []);
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   350
\out{Level 1}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   351
\out{OFCLASS(bool, agroup_class)}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   352
\out{ 1. !!(x::bool) (y::bool) z::bool. x <*> y <*> z = x <*> (y <*> z)}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   353
\out{ 2. !!x::bool. 1 <*> x = x}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   354
\out{ 3. !!x::bool. inverse x <*> x = 1}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   355
\out{ 4. !!(x::bool) y::bool. x <*> y = y <*> x}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   356
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   357
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   358
The tactic \TT{axclass\_tac} has applied \TT{agroupI} internally to
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   359
expand the class definition. It now remains to be shown that the
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   360
\TT{agroup} axioms hold for bool. To this end, we expand the
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   361
definitions of \TT{Xor} and solve the new subgoals by \TT{fast\_tac}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   362
of \HOL:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   363
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   364
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   365
by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inverse_bool_def,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   366
        Xor.unit_bool_def]);
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   367
\out{Level 2}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   368
\out{OFCLASS(bool, agroup_class)}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   369
\out{ 1. !!(x::bool) (y::bool) z::bool. x ~= y ~= z = (x ~= (y ~= z))}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   370
\out{ 2. !!x::bool. False ~= x = x}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   371
\out{ 3. !!x::bool. x ~= x = False}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   372
\out{ 4. !!(x::bool) y::bool. x ~= y = (y ~= x)}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   373
by (ALLGOALS (fast_tac HOL_cs));
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   374
\out{Level 3}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   375
\out{OFCLASS(bool, agroup_class)}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   376
\out{No subgoals!}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   377
qed "bool_in_agroup";
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   378
\out{val bool_in_agroup = "OFCLASS(bool, agroup_class)"}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   379
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   380
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   381
The result is theorem $\TT{OFCLASS}(\TT{bool}, \TT{agroup\_class})$
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   382
which expresses $\TT{bool} :: \TT{agroup}$ as a meta-proposition. This
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   383
is not yet known at the type signature level, though.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   384
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   385
\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   386
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   387
What we have done here by hand, can be also performed via
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   388
\TT{instance} in a similar way behind the scenes. This may look as
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   389
follows\footnote{Subsequently, theory \TT{Xor} is no longer
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   390
  required.}:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   391
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   392
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   393
BoolGroupInsts = Group +\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   394
defs
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   395
  prod_bool_def     "x <*> y   == x ~= (y::bool)"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   396
  inverse_bool_def  "inverse x == x::bool"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   397
  unit_bool_def     "1         == False"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   398
instance
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   399
  bool :: agroup                \{| ALLGOALS (fast_tac HOL_cs) |\}\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   400
end
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   401
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   402
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   403
This way, we have $\TT{bool} :: \TT{agroup}$ in the type signature of
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   404
\TT{BoolGroupInsts}, and all abstract group theorems are transferred
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   405
to \TT{bool} for free.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   406
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   407
Similarly, we could now also instantiate our group theory classes to
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   408
many other concrete types. For example, $\TT{int} :: \TT{agroup}$ (by
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   409
defining $\TIMES$ as addition, \TT{inverse} as negation and \TT{1} as
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   410
zero, say) or $\TT{list} :: (\TT{term})\TT{semigroup}$ (e.g.\ if
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   411
$\TIMES$ is list append). Thus, the characteristic constants $\TIMES$,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   412
\TT{inverse}, \TT{1} really become overloaded, i.e.\ have different
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   413
meanings on different types.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   414
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   415
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   416
\subsubsection{Lifting and Functors}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   417
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   418
As already mentioned above, \HOL-like systems not only support
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   419
overloaded definitions of polymorphic constants (without requiring
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   420
type classes), but even primitive recursion over types. That is,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   421
definitional equations $c^\tau \Eq t$ may also contain constants of
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   422
name $c$ on the RHS --- provided that these have types that are
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   423
strictly simpler (structurally) than $\tau$.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   424
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   425
This feature enables us to \E{lift operations}, e.g.\ to Cartesian
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   426
products, direct sums or function spaces. Below, theory
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   427
\TT{ProdGroupInsts} lifts $\TIMES$ componentwise to two-place
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   428
Cartesian products $\alpha \times \beta$:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   429
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   430
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   431
ProdGroupInsts = Prod + Group +\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   432
defs
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   433
  prod_prod_def "p <*> q == (fst p <*> fst q, snd p <*> snd q)"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   434
instance
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   435
  "*" :: (semigroup, semigroup) semigroup
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   436
    \{| simp_tac (prod_ss addsimps [assoc]) 1 |\}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   437
end
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   438
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   439
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   440
Note that \TT{prod\_prod\_def} basically has the form $\edrv
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   441
{\TIMES}^{\alpha \times \beta} \Eq \ldots {\TIMES}^\alpha \ldots
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   442
{\TIMES}^\beta \ldots$, i.e.\ the recursive occurrences
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   443
$\TIMES^\alpha$ and $\TIMES^\beta$ are really at ``simpler'' types.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   444
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   445
It is very easy to see that associativity of $\TIMES^\alpha$,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   446
$\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   447
the two-place type constructor $\times$ maps semigroups into
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   448
semigroups. This fact is proven and put into \Isa's type signature by
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   449
above \TT{instance} section.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   450
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   451
\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   452
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   453
Thus, if we view class instances as ``structures'', overloaded
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   454
constant definitions with primitive recursion over types indirectly
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   455
provide some kind of ``functors'' (mappings between abstract theories,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   456
that is).
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   457
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   458
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   459
\subsection{Syntactic classes}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   460
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   461
There is still a feature of \Isa's type system left that we have not
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   462
yet used: When declaring polymorphic constants $c :: \tau$, the type
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   463
variables occurring in $\tau$ may be constrained by type classes (or
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   464
even general sorts). Note that by default, in \Isa/\HOL\ the
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   465
declaration:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   466
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   467
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   468
  <*> :: ['a, 'a] => 'a
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   469
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   470
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   471
is actually an abbreviation for:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   472
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   473
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   474
  <*> :: ['a::term, 'a::term] => 'a::term
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   475
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   476
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   477
Since class \TT{term} is the universal class of \HOL, this is not
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   478
really a restriction at all. A less trivial example is the following
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   479
theory \TT{Product}:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   480
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   481
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   482
Product = HOL +\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   483
axclass
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   484
  product < term\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   485
consts
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   486
  "<*>" :: "['a::product, 'a] => 'a"      (infixl 70)\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   487
end
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   488
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   489
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   490
Here class \TT{product} is defined as subclass of \TT{term}, but
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   491
without any additional axioms. This effects in logical equivalence of
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   492
\TT{product} and \TT{term}, since \TT{productI} is as follows:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   493
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   494
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   495
productI: OFCLASS(?'a::logic, term_class) ==>
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   496
            OFCLASS(?'a::logic, product_class)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   497
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   498
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   499
I.e.\ $\TT{term} \subseteq \TT{product}$. The converse inclusion is
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   500
already contained in the type signature of theory \TT{Product}.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   501
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   502
Now, what is the difference of declaring $\TIMES :: [\alpha ::
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   503
\TT{product}, \alpha] \To \alpha$ vs.\ declaring $\TIMES :: [\alpha ::
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   504
\TT{term}, \alpha] \To \alpha$? In this special case (where
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   505
$\TT{product} \Eq \TT{term}$), it should be obvious that both
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   506
declarations are the same from the logic's point of view.  It is even
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   507
most sensible in the general case not to attach any \E{logical}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   508
meaning to sort constraints occurring in constant \E{declarations}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   509
(see \cite[page 79]{Wenzel94} for more details).
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   510
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   511
On the other hand there are syntactic differences, of course.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   512
Constants $\TIMES^\tau$ are rejected by the type checker, unless $\tau
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   513
:: \TT{product}$ is part of the type signature.  In our example, this
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   514
arity may be always added when required by means of a trivial
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   515
\TT{instance}.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   516
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   517
Thus, we can follow this discipline: Overloaded polymorphic constants
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   518
have their type arguments restricted to an associated (logically
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   519
trivial) class $c$. Only immediately before \E{specifying} these
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   520
constants on a certain type $\tau$ do we instantiate $\tau :: c$.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   521
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   522
This is done for class \TT{product} and type \TT{bool} in theory
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   523
\TT{ProductInsts} below:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   524
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   525
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   526
ProductInsts = Product +\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   527
instance
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   528
  bool :: product\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   529
defs
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   530
  prod_bool_def "x <*> y  == x & y::bool"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   531
end
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   532
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   533
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   534
Note that \TT{instance bool ::\ product} does not require any
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   535
witnesses, since this statement is logically trivial. Nonetheless,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   536
\TT{instance} really performs a proof.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   537
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   538
Only after $\TT{bool} :: \TT{product}$ is made known to the type
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   539
checker, does \TT{prod\_bool\_def} become syntactically well-formed.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   540
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   541
\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   542
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   543
It is very important to see that above \TT{defs} are not directly
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   544
connected with \TT{instance} at all! We were just following our
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   545
convention to specify $\TIMES$ on \TT{bool} after having instantiated
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   546
$\TT{bool} :: \TT{product}$. \Isa\ does not require these definitions,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   547
which is in contrast to programming languages like \Haskell.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   548
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   549
\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   550
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   551
While \Isa\ type classes and those of \Haskell\ are almost the same as
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   552
far as type checking and type inference are concerned, there are major
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   553
semantic differences. \Haskell\ classes require their instances to
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   554
\E{provide operations} of certain \E{names}. Therefore, its
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   555
\TT{instance} has a \TT{where} part that tells the system what these
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   556
``member functions'' should be.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   557
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   558
This style of \TT{instance} won't make much sense in \Isa, because its
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   559
meta-logic has no corresponding notion of ``providing operations'' or
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   560
``names''.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   561
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   562
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   563
\subsection{Defining natural numbers in \FOL}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   564
\label{sec:ex-natclass}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   565
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   566
Axiomatic type classes abstract over exactly one type argument. Thus,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   567
any \E{axiomatic} theory extension where each axiom refers to at most
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   568
one type variable, may be trivially turned into a \E{definitional}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   569
one.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   570
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   571
We illustrate this with the natural numbers in \Isa/\FOL:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   572
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   573
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   574
NatClass = FOL +\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   575
consts
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   576
  "0"           :: "'a"                                 ("0")
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   577
  Suc           :: "'a => 'a"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   578
  rec           :: "['a, 'a, ['a, 'a] => 'a] => 'a"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   579
axclass
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   580
  nat < term
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   581
  induct        "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   582
  Suc_inject    "Suc(m) = Suc(n) ==> m = n"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   583
  Suc_neq_0     "Suc(m) = 0 ==> R"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   584
  rec_0         "rec(0, a, f) = a"
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   585
  rec_Suc       "rec(Suc(m), a, f) = f(m, rec(m, a, f))"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   586
consts
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   587
  "+"           :: "['a::nat, 'a] => 'a"                (infixl 60)\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   588
defs
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   589
  add_def       "m + n == rec(m, n, %x y. Suc(y))"\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   590
end
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   591
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   592
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   593
\TT{NatClass} is an abstract version of \TT{Nat}\footnote{See
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   594
  directory \TT{FOL/ex}.}. Basically, we have just replaced all
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   595
occurrences of \E{type} \TT{nat} by $\alpha$ and used the natural
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   596
number axioms to define \E{class} \TT{nat}\footnote{There's a snag:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   597
  The original recursion operator \TT{rec} had to be made monomorphic,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   598
  in a sense.}. Thus class \TT{nat} contains exactly those types
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   599
$\tau$ that are isomorphic to ``the'' natural numbers (with signature
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   600
\TT{0}, \TT{Suc}, \TT{rec}).
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   601
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   602
Furthermore, theory \TT{NatClass} defines an ``abstract constant'' $+$
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   603
based on class \TT{nat}.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   604
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   605
\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   606
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   607
What we have done here can be also viewed as \E{type specification}.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   608
Of course, it still remains open if there is some type at all that
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   609
meets the class axioms. Now a very nice property of axiomatic type
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   610
classes is, that abstract reasoning is always possible --- independent
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   611
of satisfiability. The meta-logic won't break, even if some class (or
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   612
general sort) turns out to be empty (``inconsistent'')
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   613
later\footnote{As a consequence of an old bug, this is \E{not} true
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   614
  for pre-\Isa95 versions.}.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   615
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   616
For example, we may derive the following abstract natural numbers
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   617
theorems:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   618
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   619
\begin{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   620
add_0:    0 + (?n::?'a::nat) = ?n
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   621
add_Suc:  Suc(?m::?'a::nat) + (?n::?'a::nat) = Suc(?m + ?n)
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   622
\end{ascbox}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   623
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   624
See also file \TT{FOL/ex/NatClass.ML}. Note that this required only
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   625
some trivial modifications of the original \TT{Nat.ML}.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   626
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   627
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   628
\section{The user interface of \Isa's axclass package}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   629
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   630
The actual axiomatic type class package of \Isa/\Pure\ mainly consists
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   631
of two new theory sections: \TT{axclass} and \TT{instance}.  Some
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   632
typical applications of these have already been demonstrated in
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   633
\secref{sec:ex}, below their syntax and semantics are presented more
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   634
completely.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   635
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   636
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   637
\subsection{The \TT{axclass} section}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   638
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   639
Within theory files, \TT{axclass} introduces an axiomatic type class
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   640
definition. Its concrete syntax is:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   641
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   642
\begin{matharray}{l}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   643
  \TT{axclass} \\
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   644
  \ \ c \TT{ < } c_1\TT, \ldots\TT, c_n \\
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   645
  \ \ \idt{id}_1\ \idt{axm}_1 \\
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   646
  \ \ \vdots \\
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   647
  \ \ \idt{id}_m\ \idt{axm}_m
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   648
\end{matharray}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   649
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   650
Where $c, c_1, \ldots, c_n$ are classes (category $\idt{id}$ or
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   651
$\idt{string}$) and $\idt{axm}_1, \ldots, \idt{axm}_m$ (with $m \ge
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   652
0$) are formulas (category $\idt{string}$).
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   653
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   654
Class $c$ has to be new, and sort $\{c_1, \ldots, c_n\}$ a subsort of
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   655
\TT{logic}. Each class axiom $\idt{axm}_j$ may contain any term
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   656
variables, but at most one type variable (which need not be the same
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   657
for all axioms). The sort of this type variable has to be a supersort
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   658
of $\{c_1, \ldots, c_n\}$.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   659
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   660
\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   661
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   662
The \TT{axclass} section declares $c$ as subclass of $c_1, \ldots,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   663
c_n$ to the type signature.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   664
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   665
Furthermore, $\idt{axm}_1, \ldots, \idt{axm}_m$ are turned into the
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   666
``abstract axioms'' of $c$ with names $\idt{id}_1, \ldots,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   667
\idt{id}_m$.  This is done by replacing all occurring type variables
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   668
by $\alpha :: c$. Original axioms that do not contain any type
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   669
variable will be prefixed by the logical precondition
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   670
$\TT{OFCLASS}(\alpha :: \TT{logic}, c\TT{\_class})$.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   671
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   672
Another axiom of name $c\TT{I}$ --- the ``class $c$ introduction
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   673
rule'' --- is built from the respective universal closures of
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   674
$\idt{axm}_1, \ldots, \idt{axm}_m$ appropriately.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   675
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   676
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   677
\subsection{The \TT{instance} section}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   678
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   679
Section \TT{instance} proves class inclusions or type arities at the
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   680
logical level and then transfers these into the type signature.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   681
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   682
Its concrete syntax is:
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   683
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   684
\begin{matharray}{l}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   685
  \TT{instance} \\
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   686
  \ \ [\ c_1 \TT{ < } c_2 \ |\
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   687
      t \TT{ ::\ (}\idt{sort}_1\TT, \ldots \TT, \idt{sort}_n\TT) \idt{sort}\ ] \\
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   688
  \ \ [\ \TT(\idt{name}_1 \TT, \ldots\TT, \idt{name}_m\TT)\ ] \\
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   689
  \ \ [\ \TT{\{|} \idt{text} \TT{|\}}\ ]
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   690
\end{matharray}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   691
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   692
Where $c_1, c_2$ are classes and $t$ is an $n$-place type constructor
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   693
(all of category $\idt{id}$ or $\idt{string})$. Furthermore,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   694
$\idt{sort}_i$ are sorts in the usual \Isa-syntax.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   695
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   696
\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   697
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   698
Internally, \TT{instance} first sets up an appropriate goal that
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   699
expresses the class inclusion or type arity as a meta-proposition.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   700
Then tactic \TT{AxClass.axclass\_tac} is applied with all preceding
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   701
meta-definitions of the current theory file and the user-supplied
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   702
witnesses. The latter are $\idt{name}_1, \ldots, \idt{name}_m$, where
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   703
$\idt{id}$ refers to an \ML-name of a theorem, and $\idt{string}$ to an
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   704
axiom of the current theory node\footnote{Thus, the user may reference
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   705
  axioms from above this \TT{instance} in the theory file. Note
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   706
  that new axioms appear at the \ML-toplevel only after the file is
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   707
  processed completely.}.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   708
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   709
Tactic \TT{AxClass.axclass\_tac} first unfolds the class definition by
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   710
resolving with rule $c\TT{I}$, and then applies the witnesses
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   711
according to their form: Meta-definitions are unfolded, all other
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   712
formulas are repeatedly resolved\footnote{This is done in a way that
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   713
  enables proper object-\E{rules} to be used as witnesses for
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   714
  corresponding class axioms.} with.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   715
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   716
The final optional argument $\idt{text}$ is \ML-code of an arbitrary
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   717
user tactic which is applied last to any remaining goals.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   718
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   719
\medskip
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   720
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   721
Because of the complexity of \TT{instance}'s witnessing mechanisms,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   722
new users of the axclass package are advised to only use the simple
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   723
form $\TT{instance}\ \ldots\ (\idt{id}_1, \ldots, \idt{id}_m)$, where
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   724
the identifiers refer to theorems that are appropriate type instances
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   725
of the class axioms. This typically requires an auxiliary theory,
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   726
though, which defines some constants and then proves these witnesses.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   727
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   728
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   729
\begin{thebibliography}{}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   730
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   731
\bibitem[Nipkow, 1993a]{Nipkow-slides} T. Nipkow. Axiomatic Type
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   732
  Classes (in Isabelle). Presentation at the workshop \E{Types for
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   733
    Proof and Programs}, Nijmegen, 1993.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   734
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   735
\bibitem[Nipkow, 1993b]{Nipkow93} T. Nipkow. Order-Sorted Polymorphism
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   736
  in Isabelle. In G. Huet, G. Plotkin, editors, \E{Logical
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   737
    Environments}, pp.\ 164--188, Cambridge University Press, 1993.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   738
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   739
\bibitem[Paulson, 1994]{Paulson94} L.C. Paulson. \E{Isabelle --- A
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   740
    Generic Theorem Prover}. LNCS 828, 1994.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   741
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   742
\bibitem[Wenzel, 1994]{Wenzel94} M. Wenzel. \E{Axiomatische
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   743
    Typ-Klassen in Isabelle}. Diplom\-arbeit, TU München, 1994.
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   744
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   745
\end{thebibliography}
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   746
4e1eae442821 Tutorial on Axiomatic Type Classes;
wenzelm
parents:
diff changeset
   747
\end{document}