2 header {* Syntactic classes *} |
2 header {* Syntactic classes *} |
3 |
3 |
4 theory Product = Main: |
4 theory Product = Main: |
5 |
5 |
6 text {* |
6 text {* |
7 \medskip\noindent There is still a feature of Isabelle's type system |
7 \medskip\noindent There is still a feature of Isabelle's type system |
8 left that we have not yet discussed. When declaring polymorphic |
8 left that we have not yet discussed. When declaring polymorphic |
9 constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>} |
9 constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>} |
10 may be constrained by type classes (or even general sorts) in an |
10 may be constrained by type classes (or even general sorts) in an |
11 arbitrary way. Note that by default, in Isabelle/HOL the declaration |
11 arbitrary way. Note that by default, in Isabelle/HOL the |
12 @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation for @{text "\<odot> |
12 declaration @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation |
13 \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text "term"} is the universal |
13 for @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text type} is the |
14 class of HOL, this is not really a constraint at all. |
14 universal class of HOL, this is not really a constraint at all. |
15 |
15 |
16 The @{text product} class below provides a less degenerate example of |
16 The @{text product} class below provides a less degenerate example of |
17 syntactic type classes. |
17 syntactic type classes. |
18 *} |
18 *} |
19 |
19 |
20 axclass |
20 axclass |
21 product \<subseteq> "term" |
21 product \<subseteq> type |
22 consts |
22 consts |
23 product :: "'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70) |
23 product :: "'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70) |
24 |
24 |
25 text {* |
25 text {* |
26 Here class @{text product} is defined as subclass of @{text term} |
26 Here class @{text product} is defined as subclass of @{text type} |
27 without any additional axioms. This effects in logical equivalence |
27 without any additional axioms. This effects in logical equivalence |
28 of @{text product} and @{text term}, as is reflected by the trivial |
28 of @{text product} and @{text type}, as is reflected by the trivial |
29 introduction rule generated for this definition. |
29 introduction rule generated for this definition. |
30 |
30 |
31 \medskip So what is the difference of declaring @{text "\<odot> \<Colon> |
31 \medskip So what is the difference of declaring @{text "\<odot> \<Colon> |
32 'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring @{text "\<odot> \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> 'a"} |
32 'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> |
33 anyway? In this particular case where @{text "product \<equiv> term"}, it |
33 'a"} anyway? In this particular case where @{text "product \<equiv> |
34 should be obvious that both declarations are the same from the |
34 type"}, it should be obvious that both declarations are the same |
35 logic's point of view. It even makes the most sense to remove sort |
35 from the logic's point of view. It even makes the most sense to |
36 constraints from constant declarations, as far as the purely logical |
36 remove sort constraints from constant declarations, as far as the |
37 meaning is concerned \cite{Wenzel:1997:TPHOL}. |
37 purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}. |
38 |
38 |
39 On the other hand there are syntactic differences, of course. |
39 On the other hand there are syntactic differences, of course. |
40 Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the |
40 Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the |
41 type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the |
41 type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the |
42 type signature. In our example, this arity may be always added when |
42 type signature. In our example, this arity may be always added when |
43 required by means of an $\INSTANCE$ with the default proof $\DDOT$. |
43 required by means of an $\INSTANCE$ with the default proof $\DDOT$. |
44 |
44 |
45 \medskip Thus, we may observe the following discipline of using |
45 \medskip Thus, we may observe the following discipline of using |
46 syntactic classes. Overloaded polymorphic constants have their type |
46 syntactic classes. Overloaded polymorphic constants have their type |
47 arguments restricted to an associated (logically trivial) class |
47 arguments restricted to an associated (logically trivial) class |
48 @{text c}. Only immediately before \emph{specifying} these constants |
48 @{text c}. Only immediately before \emph{specifying} these |
49 on a certain type @{text \<tau>} do we instantiate @{text "\<tau> \<Colon> c"}. |
49 constants on a certain type @{text \<tau>} do we instantiate @{text "\<tau> \<Colon> |
|
50 c"}. |
50 |
51 |
51 This is done for class @{text product} and type @{typ bool} as |
52 This is done for class @{text product} and type @{typ bool} as |
52 follows. |
53 follows. |
53 *} |
54 *} |
54 |
55 |
55 instance bool :: product .. |
56 instance bool :: product .. |
56 defs (overloaded) |
57 defs (overloaded) |
57 product_bool_def: "x \<odot> y \<equiv> x \<and> y" |
58 product_bool_def: "x \<odot> y \<equiv> x \<and> y" |