3156
|
1 |
(* Title: HOLCF/ex/Classlib.thy
|
|
2 |
ID: $Id$
|
2570
|
3 |
Author: Franz Regensburger
|
|
4 |
Copyright 1995 Technical University Munich
|
|
5 |
|
3156
|
6 |
Introduce various type classes.
|
2570
|
7 |
|
3154
|
8 |
!!! Has to be adapted to axclasses !!!
|
|
9 |
--------------------------------------
|
2642
|
10 |
|
2570
|
11 |
|
3156
|
12 |
The class hierarchy is as follows:
|
2570
|
13 |
|
|
14 |
pcpo
|
|
15 |
|
|
|
16 |
----------------
|
|
17 |
| |
|
|
18 |
| ---------------------
|
|
19 |
| | | | |
|
|
20 |
per cplus cminus ctimes cdvi
|
|
21 |
|
|
|
22 |
equiv
|
|
23 |
/ \
|
|
24 |
/ \
|
|
25 |
| |
|
|
26 |
qpo eq
|
|
27 |
|
|
|
28 |
|
|
|
29 |
qlinear
|
|
30 |
|
|
31 |
|
|
32 |
*)
|
|
33 |
|
|
34 |
Classlib = HOLCF +
|
|
35 |
|
|
36 |
(* -------------------------------------------------------------------- *)
|
|
37 |
(* class cplus with characteristic constant ++ *)
|
|
38 |
|
3156
|
39 |
axclass cplus < pcpo
|
2570
|
40 |
|
3156
|
41 |
instance lift :: (term)cplus
|
2570
|
42 |
|
|
43 |
ops curried
|
|
44 |
"++" :: "'a::cplus -> 'a -> 'a" (cinfixl 65)
|
|
45 |
|
|
46 |
|
|
47 |
|
|
48 |
(* -------------------------------------------------------------------- *)
|
|
49 |
(* class cminus with characteristic constant -- *)
|
|
50 |
|
3156
|
51 |
axclass cminus < pcpo
|
2570
|
52 |
|
3156
|
53 |
instance lift :: (term)cminus
|
2570
|
54 |
|
|
55 |
ops curried
|
|
56 |
"--" :: "'a::cminus -> 'a -> 'a" (cinfixl 65)
|
|
57 |
|
3156
|
58 |
|
2570
|
59 |
|
|
60 |
(* -------------------------------------------------------------------- *)
|
|
61 |
(* class ctimes with characteristic constant ** *)
|
|
62 |
|
3156
|
63 |
axclass ctimes < pcpo
|
2570
|
64 |
|
3156
|
65 |
instance lift :: (term)ctimes
|
2570
|
66 |
|
|
67 |
ops curried
|
|
68 |
"**" :: "'a::ctimes -> 'a -> 'a" (cinfixl 70)
|
|
69 |
|
3156
|
70 |
|
2570
|
71 |
|
|
72 |
(* -------------------------------------------------------------------- *)
|
|
73 |
(* class cdiv with characteristic constant // *)
|
|
74 |
|
3156
|
75 |
axclass cdiv < pcpo
|
2570
|
76 |
|
3156
|
77 |
instance lift :: (term)cdiv
|
2570
|
78 |
|
|
79 |
ops curried
|
|
80 |
"//" :: "'a::cdiv -> 'a -> 'a" (cinfixl 70)
|
|
81 |
|
3156
|
82 |
|
2570
|
83 |
|
|
84 |
(* -------------------------------------------------------------------- *)
|
|
85 |
(* class per with characteristic constant .= *)
|
|
86 |
|
|
87 |
classes per < pcpo
|
|
88 |
|
2642
|
89 |
arities lift :: (term)per
|
2570
|
90 |
|
|
91 |
ops curried
|
|
92 |
".=" :: "'a::per -> 'a -> tr" (cinfixl 55)
|
|
93 |
syntax (symbols)
|
|
94 |
"op .=" :: "'a::per => 'a => tr" (infixl "\\<doteq>" 55)
|
|
95 |
|
|
96 |
rules
|
|
97 |
|
|
98 |
strict_per "(UU .= x) = UU & (x .= UU) = UU"
|
|
99 |
total_per "[|x ~= UU; y ~= UU|] ==> (x .= y) ~= UU"
|
2642
|
100 |
flat_per "flat (x::'a::per)"
|
2570
|
101 |
|
|
102 |
sym_per "(x .= y) = (y .= x)"
|
|
103 |
trans_per "[| (x .= y)=TT; (y .= z)=TT |] ==> (x .= z)=TT"
|
|
104 |
|
|
105 |
(* -------------------------------------------------------------------- *)
|
|
106 |
|
|
107 |
(* -------------------------------------------------------------------- *)
|
|
108 |
(* class equiv is a refinement of of class per *)
|
|
109 |
|
|
110 |
classes equiv < per
|
|
111 |
|
2642
|
112 |
arities lift :: (term)equiv
|
2570
|
113 |
|
|
114 |
rules
|
|
115 |
|
|
116 |
refl_per "[|(x::'a::equiv) ~= UU|] ==> (x .= x)=TT"
|
|
117 |
|
|
118 |
(* -------------------------------------------------------------------- *)
|
|
119 |
|
|
120 |
(* -------------------------------------------------------------------- *)
|
|
121 |
(* class eq is a refinement of of class equiv *)
|
|
122 |
|
|
123 |
classes eq < equiv
|
|
124 |
|
2642
|
125 |
arities lift :: (term)eq
|
2570
|
126 |
|
|
127 |
rules
|
|
128 |
|
|
129 |
weq "[| (x::'a::eq) ~= UU; y ~= UU |] ==>
|
|
130 |
(x = y --> (x .=y) = TT) & (x ~= y --> (x .= y)=FF)"
|
|
131 |
|
|
132 |
end
|