1 |
|
2 header {* Basic group theory *} |
|
3 |
|
4 theory Group imports Main begin |
|
5 |
|
6 text {* |
|
7 \medskip\noindent The meta-level type system of Isabelle supports |
|
8 \emph{intersections} and \emph{inclusions} of type classes. These |
|
9 directly correspond to intersections and inclusions of type |
|
10 predicates in a purely set theoretic sense. This is sufficient as a |
|
11 means to describe simple hierarchies of structures. As an |
|
12 illustration, we use the well-known example of semigroups, monoids, |
|
13 general groups and Abelian groups. |
|
14 *} |
|
15 |
|
16 subsection {* Monoids and Groups *} |
|
17 |
|
18 text {* |
|
19 First we declare some polymorphic constants required later for the |
|
20 signature parts of our structures. |
|
21 *} |
|
22 |
|
23 consts |
|
24 times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70) |
|
25 invers :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999) |
|
26 one :: 'a ("\<one>") |
|
27 |
|
28 text {* |
|
29 \noindent Next we define class @{text monoid} of monoids with |
|
30 operations @{text \<odot>} and @{text \<one>}. Note that multiple class |
|
31 axioms are allowed for user convenience --- they simply represent |
|
32 the conjunction of their respective universal closures. |
|
33 *} |
|
34 |
|
35 axclass monoid \<subseteq> type |
|
36 assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)" |
|
37 left_unit: "\<one> \<odot> x = x" |
|
38 right_unit: "x \<odot> \<one> = x" |
|
39 |
|
40 text {* |
|
41 \noindent So class @{text monoid} contains exactly those types |
|
42 @{text \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<one> \<Colon> \<tau>"} |
|
43 are specified appropriately, such that @{text \<odot>} is associative and |
|
44 @{text \<one>} is a left and right unit element for the @{text \<odot>} |
|
45 operation. |
|
46 *} |
|
47 |
|
48 text {* |
|
49 \medskip Independently of @{text monoid}, we now define a linear |
|
50 hierarchy of semigroups, general groups and Abelian groups. Note |
|
51 that the names of class axioms are automatically qualified with each |
|
52 class name, so we may re-use common names such as @{text assoc}. |
|
53 *} |
|
54 |
|
55 axclass semigroup \<subseteq> type |
|
56 assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)" |
|
57 |
|
58 axclass group \<subseteq> semigroup |
|
59 left_unit: "\<one> \<odot> x = x" |
|
60 left_inverse: "x\<inv> \<odot> x = \<one>" |
|
61 |
|
62 axclass agroup \<subseteq> group |
|
63 commute: "x \<odot> y = y \<odot> x" |
|
64 |
|
65 text {* |
|
66 \noindent Class @{text group} inherits associativity of @{text \<odot>} |
|
67 from @{text semigroup} and adds two further group axioms. Similarly, |
|
68 @{text agroup} is defined as the subset of @{text group} such that |
|
69 for all of its elements @{text \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> |
|
70 \<tau>"} is even commutative. |
|
71 *} |
|
72 |
|
73 |
|
74 subsection {* Abstract reasoning *} |
|
75 |
|
76 text {* |
|
77 In a sense, axiomatic type classes may be viewed as \emph{abstract |
|
78 theories}. Above class definitions gives rise to abstract axioms |
|
79 @{text assoc}, @{text left_unit}, @{text left_inverse}, @{text |
|
80 commute}, where any of these contain a type variable @{text "'a \<Colon> |
|
81 c"} that is restricted to types of the corresponding class @{text |
|
82 c}. \emph{Sort constraints} like this express a logical |
|
83 precondition for the whole formula. For example, @{text assoc} |
|
84 states that for all @{text \<tau>}, provided that @{text "\<tau> \<Colon> |
|
85 semigroup"}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is associative. |
|
86 |
|
87 \medskip From a technical point of view, abstract axioms are just |
|
88 ordinary Isabelle theorems, which may be used in proofs without |
|
89 special treatment. Such ``abstract proofs'' usually yield new |
|
90 ``abstract theorems''. For example, we may now derive the following |
|
91 well-known laws of general groups. |
|
92 *} |
|
93 |
|
94 theorem group_right_inverse: "x \<odot> x\<inv> = (\<one>\<Colon>'a\<Colon>group)" |
|
95 proof - |
|
96 have "x \<odot> x\<inv> = \<one> \<odot> (x \<odot> x\<inv>)" |
|
97 by (simp only: group_class.left_unit) |
|
98 also have "... = \<one> \<odot> x \<odot> x\<inv>" |
|
99 by (simp only: semigroup_class.assoc) |
|
100 also have "... = (x\<inv>)\<inv> \<odot> x\<inv> \<odot> x \<odot> x\<inv>" |
|
101 by (simp only: group_class.left_inverse) |
|
102 also have "... = (x\<inv>)\<inv> \<odot> (x\<inv> \<odot> x) \<odot> x\<inv>" |
|
103 by (simp only: semigroup_class.assoc) |
|
104 also have "... = (x\<inv>)\<inv> \<odot> \<one> \<odot> x\<inv>" |
|
105 by (simp only: group_class.left_inverse) |
|
106 also have "... = (x\<inv>)\<inv> \<odot> (\<one> \<odot> x\<inv>)" |
|
107 by (simp only: semigroup_class.assoc) |
|
108 also have "... = (x\<inv>)\<inv> \<odot> x\<inv>" |
|
109 by (simp only: group_class.left_unit) |
|
110 also have "... = \<one>" |
|
111 by (simp only: group_class.left_inverse) |
|
112 finally show ?thesis . |
|
113 qed |
|
114 |
|
115 text {* |
|
116 \noindent With @{text group_right_inverse} already available, @{text |
|
117 group_right_unit}\label{thm:group-right-unit} is now established |
|
118 much easier. |
|
119 *} |
|
120 |
|
121 theorem group_right_unit: "x \<odot> \<one> = (x\<Colon>'a\<Colon>group)" |
|
122 proof - |
|
123 have "x \<odot> \<one> = x \<odot> (x\<inv> \<odot> x)" |
|
124 by (simp only: group_class.left_inverse) |
|
125 also have "... = x \<odot> x\<inv> \<odot> x" |
|
126 by (simp only: semigroup_class.assoc) |
|
127 also have "... = \<one> \<odot> x" |
|
128 by (simp only: group_right_inverse) |
|
129 also have "... = x" |
|
130 by (simp only: group_class.left_unit) |
|
131 finally show ?thesis . |
|
132 qed |
|
133 |
|
134 text {* |
|
135 \medskip Abstract theorems may be instantiated to only those types |
|
136 @{text \<tau>} where the appropriate class membership @{text "\<tau> \<Colon> c"} is |
|
137 known at Isabelle's type signature level. Since we have @{text |
|
138 "agroup \<subseteq> group \<subseteq> semigroup"} by definition, all theorems of @{text |
|
139 semigroup} and @{text group} are automatically inherited by @{text |
|
140 group} and @{text agroup}. |
|
141 *} |
|
142 |
|
143 |
|
144 subsection {* Abstract instantiation *} |
|
145 |
|
146 text {* |
|
147 From the definition, the @{text monoid} and @{text group} classes |
|
148 have been independent. Note that for monoids, @{text right_unit} |
|
149 had to be included as an axiom, but for groups both @{text |
|
150 right_unit} and @{text right_inverse} are derivable from the other |
|
151 axioms. With @{text group_right_unit} derived as a theorem of group |
|
152 theory (see page~\pageref{thm:group-right-unit}), we may now |
|
153 instantiate @{text "monoid \<subseteq> semigroup"} and @{text "group \<subseteq> |
|
154 monoid"} properly as follows (cf.\ \figref{fig:monoid-group}). |
|
155 |
|
156 \begin{figure}[htbp] |
|
157 \begin{center} |
|
158 \small |
|
159 \unitlength 0.6mm |
|
160 \begin{picture}(65,90)(0,-10) |
|
161 \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
|
162 \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}} |
|
163 \put(15,5){\makebox(0,0){@{text agroup}}} |
|
164 \put(15,25){\makebox(0,0){@{text group}}} |
|
165 \put(15,45){\makebox(0,0){@{text semigroup}}} |
|
166 \put(30,65){\makebox(0,0){@{text type}}} \put(50,45){\makebox(0,0){@{text monoid}}} |
|
167 \end{picture} |
|
168 \hspace{4em} |
|
169 \begin{picture}(30,90)(0,0) |
|
170 \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
|
171 \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}} |
|
172 \put(15,5){\makebox(0,0){@{text agroup}}} |
|
173 \put(15,25){\makebox(0,0){@{text group}}} |
|
174 \put(15,45){\makebox(0,0){@{text monoid}}} |
|
175 \put(15,65){\makebox(0,0){@{text semigroup}}} |
|
176 \put(15,85){\makebox(0,0){@{text type}}} |
|
177 \end{picture} |
|
178 \caption{Monoids and groups: according to definition, and by proof} |
|
179 \label{fig:monoid-group} |
|
180 \end{center} |
|
181 \end{figure} |
|
182 *} |
|
183 |
|
184 instance monoid \<subseteq> semigroup |
|
185 proof |
|
186 fix x y z :: "'a\<Colon>monoid" |
|
187 show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)" |
|
188 by (rule monoid_class.assoc) |
|
189 qed |
|
190 |
|
191 instance group \<subseteq> monoid |
|
192 proof |
|
193 fix x y z :: "'a\<Colon>group" |
|
194 show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)" |
|
195 by (rule semigroup_class.assoc) |
|
196 show "\<one> \<odot> x = x" |
|
197 by (rule group_class.left_unit) |
|
198 show "x \<odot> \<one> = x" |
|
199 by (rule group_right_unit) |
|
200 qed |
|
201 |
|
202 text {* |
|
203 \medskip The \isakeyword{instance} command sets up an appropriate |
|
204 goal that represents the class inclusion (or type arity, see |
|
205 \secref{sec:inst-arity}) to be proven (see also |
|
206 \cite{isabelle-isar-ref}). The initial proof step causes |
|
207 back-chaining of class membership statements wrt.\ the hierarchy of |
|
208 any classes defined in the current theory; the effect is to reduce |
|
209 to the initial statement to a number of goals that directly |
|
210 correspond to any class axioms encountered on the path upwards |
|
211 through the class hierarchy. |
|
212 *} |
|
213 |
|
214 |
|
215 subsection {* Concrete instantiation \label{sec:inst-arity} *} |
|
216 |
|
217 text {* |
|
218 So far we have covered the case of the form |
|
219 \isakeyword{instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely |
|
220 \emph{abstract instantiation} --- $c@1$ is more special than @{text |
|
221 "c\<^sub>1"} and thus an instance of @{text "c\<^sub>2"}. Even more |
|
222 interesting for practical applications are \emph{concrete |
|
223 instantiations} of axiomatic type classes. That is, certain simple |
|
224 schemes @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Colon> c"} of class |
|
225 membership may be established at the logical level and then |
|
226 transferred to Isabelle's type signature level. |
|
227 |
|
228 \medskip As a typical example, we show that type @{typ bool} with |
|
229 exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and |
|
230 @{term False} as @{text \<one>} forms an Abelian group. |
|
231 *} |
|
232 |
|
233 defs (overloaded) |
|
234 times_bool_def: "x \<odot> y \<equiv> x \<noteq> (y\<Colon>bool)" |
|
235 inverse_bool_def: "x\<inv> \<equiv> x\<Colon>bool" |
|
236 unit_bool_def: "\<one> \<equiv> False" |
|
237 |
|
238 text {* |
|
239 \medskip It is important to note that above \isakeyword{defs} are |
|
240 just overloaded meta-level constant definitions, where type classes |
|
241 are not yet involved at all. This form of constant definition with |
|
242 overloading (and optional recursion over the syntactic structure of |
|
243 simple types) are admissible as definitional extensions of plain HOL |
|
244 \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not |
|
245 required for overloading. Nevertheless, overloaded definitions are |
|
246 best applied in the context of type classes. |
|
247 |
|
248 \medskip Since we have chosen above \isakeyword{defs} of the generic |
|
249 group operations on type @{typ bool} appropriately, the class |
|
250 membership @{text "bool \<Colon> agroup"} may be now derived as follows. |
|
251 *} |
|
252 |
|
253 instance bool :: agroup |
|
254 proof (intro_classes, |
|
255 unfold times_bool_def inverse_bool_def unit_bool_def) |
|
256 fix x y z |
|
257 show "((x \<noteq> y) \<noteq> z) = (x \<noteq> (y \<noteq> z))" by blast |
|
258 show "(False \<noteq> x) = x" by blast |
|
259 show "(x \<noteq> x) = False" by blast |
|
260 show "(x \<noteq> y) = (y \<noteq> x)" by blast |
|
261 qed |
|
262 |
|
263 text {* |
|
264 The result of an \isakeyword{instance} statement is both expressed |
|
265 as a theorem of Isabelle's meta-logic, and as a type arity of the |
|
266 type signature. The latter enables type-inference system to take |
|
267 care of this new instance automatically. |
|
268 |
|
269 \medskip We could now also instantiate our group theory classes to |
|
270 many other concrete types. For example, @{text "int \<Colon> agroup"} |
|
271 (e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation |
|
272 and @{text \<one>} as zero) or @{text "list \<Colon> (type) semigroup"} |
|
273 (e.g.\ if @{text \<odot>} is defined as list append). Thus, the |
|
274 characteristic constants @{text \<odot>}, @{text \<inv>}, @{text \<one>} |
|
275 really become overloaded, i.e.\ have different meanings on different |
|
276 types. |
|
277 *} |
|
278 |
|
279 |
|
280 subsection {* Lifting and Functors *} |
|
281 |
|
282 text {* |
|
283 As already mentioned above, overloading in the simply-typed HOL |
|
284 systems may include recursion over the syntactic structure of types. |
|
285 That is, definitional equations @{text "c\<^sup>\<tau> \<equiv> t"} may also |
|
286 contain constants of name @{text c} on the right-hand side --- if |
|
287 these have types that are structurally simpler than @{text \<tau>}. |
|
288 |
|
289 This feature enables us to \emph{lift operations}, say to Cartesian |
|
290 products, direct sums or function spaces. Subsequently we lift |
|
291 @{text \<odot>} component-wise to binary products @{typ "'a \<times> 'b"}. |
|
292 *} |
|
293 |
|
294 defs (overloaded) |
|
295 times_prod_def: "p \<odot> q \<equiv> (fst p \<odot> fst q, snd p \<odot> snd q)" |
|
296 |
|
297 text {* |
|
298 It is very easy to see that associativity of @{text \<odot>} on @{typ 'a} |
|
299 and @{text \<odot>} on @{typ 'b} transfers to @{text \<odot>} on @{typ "'a \<times> |
|
300 'b"}. Hence the binary type constructor @{text \<odot>} maps semigroups |
|
301 to semigroups. This may be established formally as follows. |
|
302 *} |
|
303 |
|
304 instance * :: (semigroup, semigroup) semigroup |
|
305 proof (intro_classes, unfold times_prod_def) |
|
306 fix p q r :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup" |
|
307 show |
|
308 "(fst (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> fst r, |
|
309 snd (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> snd r) = |
|
310 (fst p \<odot> fst (fst q \<odot> fst r, snd q \<odot> snd r), |
|
311 snd p \<odot> snd (fst q \<odot> fst r, snd q \<odot> snd r))" |
|
312 by (simp add: semigroup_class.assoc) |
|
313 qed |
|
314 |
|
315 text {* |
|
316 Thus, if we view class instances as ``structures'', then overloaded |
|
317 constant definitions with recursion over types indirectly provide |
|
318 some kind of ``functors'' --- i.e.\ mappings between abstract |
|
319 theories. |
|
320 *} |
|
321 |
|
322 end |
|