|
1 (* Title: FOCUS/Classlib.thy |
|
2 ID: $ $ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1995 Technical University Munich |
|
5 |
|
6 Introduce various type classes |
|
7 |
|
8 The 8bit package is needed for this theory |
|
9 |
|
10 The type void of HOLCF/Void.thy is a witness for all the introduced classes. |
|
11 Inspect theory Witness.thy for all the proofs. |
|
12 |
|
13 the trivial instance for ++ -- ** // is LAM x y.(UU::void) |
|
14 the trivial instance for .= and .<= is LAM x y.(UU::tr) |
|
15 |
|
16 the class hierarchy is as follows |
|
17 |
|
18 pcpo |
|
19 | |
|
20 ---------------- |
|
21 | | |
|
22 | --------------------- |
|
23 | | | | | |
|
24 per cplus cminus ctimes cdvi |
|
25 | |
|
26 equiv |
|
27 / \ |
|
28 / \ |
|
29 | | |
|
30 qpo eq |
|
31 | |
|
32 | |
|
33 qlinear |
|
34 |
|
35 |
|
36 *) |
|
37 |
|
38 Classlib = HOLCF + |
|
39 |
|
40 (* -------------------------------------------------------------------- *) |
|
41 (* class cplus with characteristic constant ++ *) |
|
42 |
|
43 classes cplus < pcpo |
|
44 |
|
45 arities void :: cplus |
|
46 |
|
47 ops curried |
|
48 "++" :: "'a::cplus -> 'a -> 'a" (cinfixl 65) |
|
49 |
|
50 |
|
51 (* class cplus has no characteristic axioms *) |
|
52 (* -------------------------------------------------------------------- *) |
|
53 |
|
54 (* -------------------------------------------------------------------- *) |
|
55 (* class cminus with characteristic constant -- *) |
|
56 |
|
57 classes cminus < pcpo |
|
58 |
|
59 arities void :: cminus |
|
60 |
|
61 ops curried |
|
62 "--" :: "'a::cminus -> 'a -> 'a" (cinfixl 65) |
|
63 |
|
64 (* class cminus has no characteristic axioms *) |
|
65 (* -------------------------------------------------------------------- *) |
|
66 |
|
67 (* -------------------------------------------------------------------- *) |
|
68 (* class ctimes with characteristic constant ** *) |
|
69 |
|
70 classes ctimes < pcpo |
|
71 |
|
72 arities void :: ctimes |
|
73 |
|
74 ops curried |
|
75 "**" :: "'a::ctimes -> 'a -> 'a" (cinfixl 70) |
|
76 |
|
77 (* class ctimes has no characteristic axioms *) |
|
78 (* -------------------------------------------------------------------- *) |
|
79 |
|
80 (* -------------------------------------------------------------------- *) |
|
81 (* class cdiv with characteristic constant // *) |
|
82 |
|
83 classes cdiv < pcpo |
|
84 |
|
85 arities void :: cdiv |
|
86 |
|
87 ops curried |
|
88 "//" :: "'a::cdiv -> 'a -> 'a" (cinfixl 70) |
|
89 |
|
90 (* class cdiv has no characteristic axioms *) |
|
91 (* -------------------------------------------------------------------- *) |
|
92 |
|
93 (* -------------------------------------------------------------------- *) |
|
94 (* class per with characteristic constant .= *) |
|
95 |
|
96 classes per < pcpo |
|
97 |
|
98 arities void :: per |
|
99 |
|
100 ops curried |
|
101 ".=" :: "'a::per -> 'a -> tr" (cinfixl 55) |
|
102 syntax (symbols) |
|
103 "op .=" :: "'a::per => 'a => tr" (infixl "\\<doteq>" 55) |
|
104 |
|
105 rules |
|
106 |
|
107 strict_per "(UU .= x) = UU & (x .= UU) = UU" |
|
108 total_per "[|x ~= UU; y ~= UU|] ==> (x .= y) ~= UU" |
|
109 flat_per "flat (UU::'a::per)" |
|
110 |
|
111 sym_per "(x .= y) = (y .= x)" |
|
112 trans_per "[| (x .= y)=TT; (y .= z)=TT |] ==> (x .= z)=TT" |
|
113 |
|
114 (* -------------------------------------------------------------------- *) |
|
115 |
|
116 (* -------------------------------------------------------------------- *) |
|
117 (* class equiv is a refinement of of class per *) |
|
118 |
|
119 classes equiv < per |
|
120 |
|
121 arities void :: equiv |
|
122 |
|
123 rules |
|
124 |
|
125 refl_per "[|(x::'a::equiv) ~= UU|] ==> (x .= x)=TT" |
|
126 |
|
127 (* -------------------------------------------------------------------- *) |
|
128 |
|
129 (* -------------------------------------------------------------------- *) |
|
130 (* class eq is a refinement of of class equiv *) |
|
131 |
|
132 classes eq < equiv |
|
133 |
|
134 arities void :: eq |
|
135 |
|
136 rules |
|
137 |
|
138 weq "[| (x::'a::eq) ~= UU; y ~= UU |] ==> |
|
139 (x = y --> (x .=y) = TT) & (x ~= y --> (x .= y)=FF)" |
|
140 |
|
141 (* -------------------------------------------------------------------- *) |
|
142 |
|
143 (* -------------------------------------------------------------------- *) |
|
144 (* class qpo with characteristic constant .<= *) |
|
145 (* .<= is a partial order wrt an equivalence *) |
|
146 |
|
147 classes qpo < equiv |
|
148 |
|
149 arities void :: qpo |
|
150 |
|
151 ops curried |
|
152 ".<=" :: "'a::qpo -> 'a -> tr" (cinfixl 55) |
|
153 syntax (symbols) |
|
154 "op .<=":: "'a::qpo => 'a => tr" (infixl "\\<preceq>" 55) |
|
155 rules |
|
156 |
|
157 strict_qpo "(UU .<= x) = UU & (x .<= UU) = UU" |
|
158 total_qpo "[|x ~= UU; y ~= UU|] ==> (x .<= y) ~= UU" |
|
159 |
|
160 refl_qpo "[|x ~= UU|] ==> (x .<= x)=TT" |
|
161 antisym_qpo "[| (x .<= y)=TT; (y .<= x)=TT |] ==> (x .= y)=TT" |
|
162 trans_qpo "[| (x .<= y)=TT; (y .<= z)=TT |] ==> (x .<= z)=TT" |
|
163 |
|
164 antisym_qpo_rev "(x .= y)=TT ==> (x .<= y)=TT & (y .<= x)=TT" |
|
165 |
|
166 (* -------------------------------------------------------------------- *) |
|
167 |
|
168 (* -------------------------------------------------------------------- *) |
|
169 (* irreflexive part .< defined via .<= *) |
|
170 |
|
171 ops curried |
|
172 ".<" :: "'a::qpo -> 'a -> tr" (cinfixl 55) |
|
173 syntax (symbols) |
|
174 "op .<" :: "'a::qpo => 'a => tr" (infixl "\\<prec>" 55) |
|
175 |
|
176 defs |
|
177 |
|
178 qless_def "(op .<) Ú LAM x y.If x .= y then FF else x .<= y fi" |
|
179 |
|
180 (* -------------------------------------------------------------------- *) |
|
181 |
|
182 (* -------------------------------------------------------------------- *) |
|
183 (* class qlinear is a refinement of of class qpo *) |
|
184 |
|
185 classes qlinear < qpo |
|
186 |
|
187 arities void :: qlinear |
|
188 |
|
189 rules |
|
190 |
|
191 qlinear "[|(x::'a::qlinear) ~= UU; y ~= UU|] ==> (x .<= y)=TT Á (y .<= x)=TT " |
|
192 |
|
193 (* -------------------------------------------------------------------- *) |
|
194 |
|
195 end |