1 |
1 |
2 \chapter{Introduction} |
2 \chapter{Introduction} |
3 |
3 |
4 A Haskell-style type-system \cite{haskell-report} with ordered type-classes |
4 A Haskell-style type-system \cite{haskell-report} with ordered type-classes |
5 has been present in Isabelle since 1991 \cite{nipkow-sorts93}. Initially, |
5 has been present in Isabelle since 1991 already \cite{nipkow-sorts93}. |
6 classes have mainly served as a \emph{purely syntactic} tool to formulate |
6 Initially, classes have mainly served as a \emph{purely syntactic} tool to |
7 polymorphic object-logics in a clean way, such as the standard Isabelle |
7 formulate polymorphic object-logics in a clean way, such as the standard |
8 formulation of many-sorted FOL \cite{paulson-isa-book}. |
8 Isabelle formulation of many-sorted FOL \cite{paulson-isa-book}. |
9 |
9 |
10 Applying classes at the \emph{logical level} to provide a simple notion of |
10 Applying classes at the \emph{logical level} to provide a simple notion of |
11 abstract theories and instantiations to concrete ones, has been long proposed |
11 abstract theories and instantiations to concrete ones, has been long proposed |
12 as well \cite{nipkow-types93,nipkow-sorts93}). At that time, Isabelle still |
12 as well \cite{nipkow-types93,nipkow-sorts93}. At that time, Isabelle still |
13 lacked built-in support for these \emph{axiomatic type classes}. More |
13 lacked built-in support for these \emph{axiomatic type classes}. More |
14 importantly, their semantics was not yet fully fleshed out (and unnecessarily |
14 importantly, their semantics was not yet fully fleshed out (and unnecessarily |
15 complicated, too). |
15 complicated, too). |
16 |
16 |
17 Since the Isabelle94 releases, actual axiomatic type classes have been an |
17 Since Isabelle94, actual axiomatic type classes have been an integral part of |
18 integral part of Isabelle's meta-logic. This very simple implementation is |
18 Isabelle's meta-logic. This very simple implementation is based on a |
19 based on a straight-forward extension of traditional simple-typed Higher-Order |
19 straight-forward extension of traditional simply-typed Higher-Order Logic, by |
20 Logic, including types qualified by logical predicates and overloaded constant |
20 including types qualified by logical predicates and overloaded constant |
21 definitions; see \cite{Wenzel:1997:TPHOL} for further details. |
21 definitions (see \cite{Wenzel:1997:TPHOL} for further details). |
22 |
22 |
23 Yet until Isabelle99, there used to be still a fundamental methodological |
23 Yet even until Isabelle99, there used to be still a fundamental methodological |
24 problem in using axiomatic type classes conveniently, due to the traditional |
24 problem in using axiomatic type classes conveniently, due to the traditional |
25 distinction of Isabelle theory files vs.\ ML proof scripts. This has been |
25 distinction of Isabelle theory files vs.\ ML proof scripts. This has been |
26 finally overcome with the advent of Isabelle/Isar theories |
26 finally overcome with the advent of Isabelle/Isar theories |
27 \cite{isabelle-isar-ref}: now definitions and proofs may be freely intermixed. |
27 \cite{isabelle-isar-ref}: now definitions and proofs may be freely intermixed. |
28 This nicely accommodates the usual procedure of defining axiomatic type |
28 This nicely accommodates the usual procedure of defining axiomatic type |
30 proving concrete properties for instantiation of classes etc. |
30 proving concrete properties for instantiation of classes etc. |
31 |
31 |
32 \medskip |
32 \medskip |
33 |
33 |
34 So to cut a long story short, the present version of axiomatic type classes |
34 So to cut a long story short, the present version of axiomatic type classes |
35 (Isabelle99 or later) now provides an even more useful and convenient |
35 now provides an even more useful and convenient mechanism for light-weight |
36 mechanism for light-weight abstract theories, without any special provisions |
36 abstract theories, without any special technical provisions to be observed by |
37 to be observed by the user. |
37 the user. |
38 |
38 |
39 |
39 |
40 \chapter{Examples}\label{sec:ex} |
40 \chapter{Examples}\label{sec:ex} |
41 |
41 |
42 Axiomatic type classes are a concept of Isabelle's meta-logic |
42 Axiomatic type classes are a concept of Isabelle's meta-logic |