1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Group}% |
|
4 % |
|
5 \isamarkupheader{Basic group theory% |
|
6 } |
|
7 \isamarkuptrue% |
|
8 % |
|
9 \isadelimtheory |
|
10 % |
|
11 \endisadelimtheory |
|
12 % |
|
13 \isatagtheory |
|
14 \isacommand{theory}\isamarkupfalse% |
|
15 \ Group\ \isakeyword{imports}\ Main\ \isakeyword{begin}% |
|
16 \endisatagtheory |
|
17 {\isafoldtheory}% |
|
18 % |
|
19 \isadelimtheory |
|
20 % |
|
21 \endisadelimtheory |
|
22 % |
|
23 \begin{isamarkuptext}% |
|
24 \medskip\noindent The meta-level type system of Isabelle supports |
|
25 \emph{intersections} and \emph{inclusions} of type classes. These |
|
26 directly correspond to intersections and inclusions of type |
|
27 predicates in a purely set theoretic sense. This is sufficient as a |
|
28 means to describe simple hierarchies of structures. As an |
|
29 illustration, we use the well-known example of semigroups, monoids, |
|
30 general groups and Abelian groups.% |
|
31 \end{isamarkuptext}% |
|
32 \isamarkuptrue% |
|
33 % |
|
34 \isamarkupsubsection{Monoids and Groups% |
|
35 } |
|
36 \isamarkuptrue% |
|
37 % |
|
38 \begin{isamarkuptext}% |
|
39 First we declare some polymorphic constants required later for the |
|
40 signature parts of our structures.% |
|
41 \end{isamarkuptext}% |
|
42 \isamarkuptrue% |
|
43 \isacommand{consts}\isamarkupfalse% |
|
44 \isanewline |
|
45 \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
|
46 \ \ invers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline |
|
47 \ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}% |
|
48 \begin{isamarkuptext}% |
|
49 \noindent Next we define class \isa{monoid} of monoids with |
|
50 operations \isa{{\isasymodot}} and \isa{{\isasymone}}. Note that multiple class |
|
51 axioms are allowed for user convenience --- they simply represent |
|
52 the conjunction of their respective universal closures.% |
|
53 \end{isamarkuptext}% |
|
54 \isamarkuptrue% |
|
55 \isacommand{axclass}\isamarkupfalse% |
|
56 \ monoid\ {\isasymsubseteq}\ type\isanewline |
|
57 \ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
58 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
|
59 \ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}% |
|
60 \begin{isamarkuptext}% |
|
61 \noindent So class \isa{monoid} contains exactly those types |
|
62 \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymone}\ {\isasymColon}\ {\isasymtau}} |
|
63 are specified appropriately, such that \isa{{\isasymodot}} is associative and |
|
64 \isa{{\isasymone}} is a left and right unit element for the \isa{{\isasymodot}} |
|
65 operation.% |
|
66 \end{isamarkuptext}% |
|
67 \isamarkuptrue% |
|
68 % |
|
69 \begin{isamarkuptext}% |
|
70 \medskip Independently of \isa{monoid}, we now define a linear |
|
71 hierarchy of semigroups, general groups and Abelian groups. Note |
|
72 that the names of class axioms are automatically qualified with each |
|
73 class name, so we may re-use common names such as \isa{assoc}.% |
|
74 \end{isamarkuptext}% |
|
75 \isamarkuptrue% |
|
76 \isacommand{axclass}\isamarkupfalse% |
|
77 \ semigroup\ {\isasymsubseteq}\ type\isanewline |
|
78 \ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
79 \isanewline |
|
80 \isacommand{axclass}\isamarkupfalse% |
|
81 \ group\ {\isasymsubseteq}\ semigroup\isanewline |
|
82 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
|
83 \ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
|
84 \isanewline |
|
85 \isacommand{axclass}\isamarkupfalse% |
|
86 \ agroup\ {\isasymsubseteq}\ group\isanewline |
|
87 \ \ commute{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequoteclose}% |
|
88 \begin{isamarkuptext}% |
|
89 \noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}} |
|
90 from \isa{semigroup} and adds two further group axioms. Similarly, |
|
91 \isa{agroup} is defined as the subset of \isa{group} such that |
|
92 for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.% |
|
93 \end{isamarkuptext}% |
|
94 \isamarkuptrue% |
|
95 % |
|
96 \isamarkupsubsection{Abstract reasoning% |
|
97 } |
|
98 \isamarkuptrue% |
|
99 % |
|
100 \begin{isamarkuptext}% |
|
101 In a sense, axiomatic type classes may be viewed as \emph{abstract |
|
102 theories}. Above class definitions gives rise to abstract axioms |
|
103 \isa{assoc}, \isa{left{\isacharunderscore}unit}, \isa{left{\isacharunderscore}inverse}, \isa{commute}, where any of these contain a type variable \isa{{\isacharprime}a\ {\isasymColon}\ c} that is restricted to types of the corresponding class \isa{c}. \emph{Sort constraints} like this express a logical |
|
104 precondition for the whole formula. For example, \isa{assoc} |
|
105 states that for all \isa{{\isasymtau}}, provided that \isa{{\isasymtau}\ {\isasymColon}\ semigroup}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is associative. |
|
106 |
|
107 \medskip From a technical point of view, abstract axioms are just |
|
108 ordinary Isabelle theorems, which may be used in proofs without |
|
109 special treatment. Such ``abstract proofs'' usually yield new |
|
110 ``abstract theorems''. For example, we may now derive the following |
|
111 well-known laws of general groups.% |
|
112 \end{isamarkuptext}% |
|
113 \isamarkuptrue% |
|
114 \isacommand{theorem}\isamarkupfalse% |
|
115 \ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
116 % |
|
117 \isadelimproof |
|
118 % |
|
119 \endisadelimproof |
|
120 % |
|
121 \isatagproof |
|
122 \isacommand{proof}\isamarkupfalse% |
|
123 \ {\isacharminus}\isanewline |
|
124 \ \ \isacommand{have}\isamarkupfalse% |
|
125 \ {\isachardoublequoteopen}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
126 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
127 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
128 \ \ \isacommand{also}\isamarkupfalse% |
|
129 \ \isacommand{have}\isamarkupfalse% |
|
130 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline |
|
131 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
132 \ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline |
|
133 \ \ \isacommand{also}\isamarkupfalse% |
|
134 \ \isacommand{have}\isamarkupfalse% |
|
135 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline |
|
136 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
137 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
|
138 \ \ \isacommand{also}\isamarkupfalse% |
|
139 \ \isacommand{have}\isamarkupfalse% |
|
140 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline |
|
141 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
142 \ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline |
|
143 \ \ \isacommand{also}\isamarkupfalse% |
|
144 \ \isacommand{have}\isamarkupfalse% |
|
145 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline |
|
146 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
147 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
|
148 \ \ \isacommand{also}\isamarkupfalse% |
|
149 \ \isacommand{have}\isamarkupfalse% |
|
150 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
151 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
152 \ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline |
|
153 \ \ \isacommand{also}\isamarkupfalse% |
|
154 \ \isacommand{have}\isamarkupfalse% |
|
155 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline |
|
156 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
157 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
158 \ \ \isacommand{also}\isamarkupfalse% |
|
159 \ \isacommand{have}\isamarkupfalse% |
|
160 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
|
161 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
162 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
|
163 \ \ \isacommand{finally}\isamarkupfalse% |
|
164 \ \isacommand{show}\isamarkupfalse% |
|
165 \ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse% |
|
166 \isanewline |
|
167 \isacommand{qed}\isamarkupfalse% |
|
168 % |
|
169 \endisatagproof |
|
170 {\isafoldproof}% |
|
171 % |
|
172 \isadelimproof |
|
173 % |
|
174 \endisadelimproof |
|
175 % |
|
176 \begin{isamarkuptext}% |
|
177 \noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established |
|
178 much easier.% |
|
179 \end{isamarkuptext}% |
|
180 \isamarkuptrue% |
|
181 \isacommand{theorem}\isamarkupfalse% |
|
182 \ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
183 % |
|
184 \isadelimproof |
|
185 % |
|
186 \endisadelimproof |
|
187 % |
|
188 \isatagproof |
|
189 \isacommand{proof}\isamarkupfalse% |
|
190 \ {\isacharminus}\isanewline |
|
191 \ \ \isacommand{have}\isamarkupfalse% |
|
192 \ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
193 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
194 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
|
195 \ \ \isacommand{also}\isamarkupfalse% |
|
196 \ \isacommand{have}\isamarkupfalse% |
|
197 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline |
|
198 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
199 \ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline |
|
200 \ \ \isacommand{also}\isamarkupfalse% |
|
201 \ \isacommand{have}\isamarkupfalse% |
|
202 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline |
|
203 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
204 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline |
|
205 \ \ \isacommand{also}\isamarkupfalse% |
|
206 \ \isacommand{have}\isamarkupfalse% |
|
207 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
|
208 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
209 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
210 \ \ \isacommand{finally}\isamarkupfalse% |
|
211 \ \isacommand{show}\isamarkupfalse% |
|
212 \ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse% |
|
213 \isanewline |
|
214 \isacommand{qed}\isamarkupfalse% |
|
215 % |
|
216 \endisatagproof |
|
217 {\isafoldproof}% |
|
218 % |
|
219 \isadelimproof |
|
220 % |
|
221 \endisadelimproof |
|
222 % |
|
223 \begin{isamarkuptext}% |
|
224 \medskip Abstract theorems may be instantiated to only those types |
|
225 \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is |
|
226 known at Isabelle's type signature level. Since we have \isa{agroup\ {\isasymsubseteq}\ group\ {\isasymsubseteq}\ semigroup} by definition, all theorems of \isa{semigroup} and \isa{group} are automatically inherited by \isa{group} and \isa{agroup}.% |
|
227 \end{isamarkuptext}% |
|
228 \isamarkuptrue% |
|
229 % |
|
230 \isamarkupsubsection{Abstract instantiation% |
|
231 } |
|
232 \isamarkuptrue% |
|
233 % |
|
234 \begin{isamarkuptext}% |
|
235 From the definition, the \isa{monoid} and \isa{group} classes |
|
236 have been independent. Note that for monoids, \isa{right{\isacharunderscore}unit} |
|
237 had to be included as an axiom, but for groups both \isa{right{\isacharunderscore}unit} and \isa{right{\isacharunderscore}inverse} are derivable from the other |
|
238 axioms. With \isa{group{\isacharunderscore}right{\isacharunderscore}unit} derived as a theorem of group |
|
239 theory (see page~\pageref{thm:group-right-unit}), we may now |
|
240 instantiate \isa{monoid\ {\isasymsubseteq}\ semigroup} and \isa{group\ {\isasymsubseteq}\ monoid} properly as follows (cf.\ \figref{fig:monoid-group}). |
|
241 |
|
242 \begin{figure}[htbp] |
|
243 \begin{center} |
|
244 \small |
|
245 \unitlength 0.6mm |
|
246 \begin{picture}(65,90)(0,-10) |
|
247 \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
|
248 \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}} |
|
249 \put(15,5){\makebox(0,0){\isa{agroup}}} |
|
250 \put(15,25){\makebox(0,0){\isa{group}}} |
|
251 \put(15,45){\makebox(0,0){\isa{semigroup}}} |
|
252 \put(30,65){\makebox(0,0){\isa{type}}} \put(50,45){\makebox(0,0){\isa{monoid}}} |
|
253 \end{picture} |
|
254 \hspace{4em} |
|
255 \begin{picture}(30,90)(0,0) |
|
256 \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
|
257 \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}} |
|
258 \put(15,5){\makebox(0,0){\isa{agroup}}} |
|
259 \put(15,25){\makebox(0,0){\isa{group}}} |
|
260 \put(15,45){\makebox(0,0){\isa{monoid}}} |
|
261 \put(15,65){\makebox(0,0){\isa{semigroup}}} |
|
262 \put(15,85){\makebox(0,0){\isa{type}}} |
|
263 \end{picture} |
|
264 \caption{Monoids and groups: according to definition, and by proof} |
|
265 \label{fig:monoid-group} |
|
266 \end{center} |
|
267 \end{figure}% |
|
268 \end{isamarkuptext}% |
|
269 \isamarkuptrue% |
|
270 \isacommand{instance}\isamarkupfalse% |
|
271 \ monoid\ {\isasymsubseteq}\ semigroup\isanewline |
|
272 % |
|
273 \isadelimproof |
|
274 % |
|
275 \endisadelimproof |
|
276 % |
|
277 \isatagproof |
|
278 \isacommand{proof}\isamarkupfalse% |
|
279 \isanewline |
|
280 \ \ \isacommand{fix}\isamarkupfalse% |
|
281 \ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoid{\isachardoublequoteclose}\isanewline |
|
282 \ \ \isacommand{show}\isamarkupfalse% |
|
283 \ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
284 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
285 \ {\isacharparenleft}rule\ monoid{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline |
|
286 \isacommand{qed}\isamarkupfalse% |
|
287 % |
|
288 \endisatagproof |
|
289 {\isafoldproof}% |
|
290 % |
|
291 \isadelimproof |
|
292 \isanewline |
|
293 % |
|
294 \endisadelimproof |
|
295 \isanewline |
|
296 \isacommand{instance}\isamarkupfalse% |
|
297 \ group\ {\isasymsubseteq}\ monoid\isanewline |
|
298 % |
|
299 \isadelimproof |
|
300 % |
|
301 \endisadelimproof |
|
302 % |
|
303 \isatagproof |
|
304 \isacommand{proof}\isamarkupfalse% |
|
305 \isanewline |
|
306 \ \ \isacommand{fix}\isamarkupfalse% |
|
307 \ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\isanewline |
|
308 \ \ \isacommand{show}\isamarkupfalse% |
|
309 \ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
310 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
311 \ {\isacharparenleft}rule\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline |
|
312 \ \ \isacommand{show}\isamarkupfalse% |
|
313 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
|
314 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
315 \ {\isacharparenleft}rule\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
316 \ \ \isacommand{show}\isamarkupfalse% |
|
317 \ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
|
318 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
319 \ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
320 \isacommand{qed}\isamarkupfalse% |
|
321 % |
|
322 \endisatagproof |
|
323 {\isafoldproof}% |
|
324 % |
|
325 \isadelimproof |
|
326 % |
|
327 \endisadelimproof |
|
328 % |
|
329 \begin{isamarkuptext}% |
|
330 \medskip The \isakeyword{instance} command sets up an appropriate |
|
331 goal that represents the class inclusion (or type arity, see |
|
332 \secref{sec:inst-arity}) to be proven (see also |
|
333 \cite{isabelle-isar-ref}). The initial proof step causes |
|
334 back-chaining of class membership statements wrt.\ the hierarchy of |
|
335 any classes defined in the current theory; the effect is to reduce |
|
336 to the initial statement to a number of goals that directly |
|
337 correspond to any class axioms encountered on the path upwards |
|
338 through the class hierarchy.% |
|
339 \end{isamarkuptext}% |
|
340 \isamarkuptrue% |
|
341 % |
|
342 \isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}% |
|
343 } |
|
344 \isamarkuptrue% |
|
345 % |
|
346 \begin{isamarkuptext}% |
|
347 So far we have covered the case of the form |
|
348 \isakeyword{instance}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}, namely |
|
349 \emph{abstract instantiation} --- $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance of \isa{c\isactrlsub {\isadigit{2}}}. Even more |
|
350 interesting for practical applications are \emph{concrete |
|
351 instantiations} of axiomatic type classes. That is, certain simple |
|
352 schemes \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ c} of class |
|
353 membership may be established at the logical level and then |
|
354 transferred to Isabelle's type signature level. |
|
355 |
|
356 \medskip As a typical example, we show that type \isa{bool} with |
|
357 exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and |
|
358 \isa{False} as \isa{{\isasymone}} forms an Abelian group.% |
|
359 \end{isamarkuptext}% |
|
360 \isamarkuptrue% |
|
361 \isacommand{defs}\isamarkupfalse% |
|
362 \ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
|
363 \ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
364 \ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequoteclose}\isanewline |
|
365 \ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ False{\isachardoublequoteclose}% |
|
366 \begin{isamarkuptext}% |
|
367 \medskip It is important to note that above \isakeyword{defs} are |
|
368 just overloaded meta-level constant definitions, where type classes |
|
369 are not yet involved at all. This form of constant definition with |
|
370 overloading (and optional recursion over the syntactic structure of |
|
371 simple types) are admissible as definitional extensions of plain HOL |
|
372 \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not |
|
373 required for overloading. Nevertheless, overloaded definitions are |
|
374 best applied in the context of type classes. |
|
375 |
|
376 \medskip Since we have chosen above \isakeyword{defs} of the generic |
|
377 group operations on type \isa{bool} appropriately, the class |
|
378 membership \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.% |
|
379 \end{isamarkuptext}% |
|
380 \isamarkuptrue% |
|
381 \isacommand{instance}\isamarkupfalse% |
|
382 \ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline |
|
383 % |
|
384 \isadelimproof |
|
385 % |
|
386 \endisadelimproof |
|
387 % |
|
388 \isatagproof |
|
389 \isacommand{proof}\isamarkupfalse% |
|
390 \ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline |
|
391 \ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline |
|
392 \ \ \isacommand{fix}\isamarkupfalse% |
|
393 \ x\ y\ z\isanewline |
|
394 \ \ \isacommand{show}\isamarkupfalse% |
|
395 \ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
396 \ blast\isanewline |
|
397 \ \ \isacommand{show}\isamarkupfalse% |
|
398 \ {\isachardoublequoteopen}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
399 \ blast\isanewline |
|
400 \ \ \isacommand{show}\isamarkupfalse% |
|
401 \ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
402 \ blast\isanewline |
|
403 \ \ \isacommand{show}\isamarkupfalse% |
|
404 \ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
405 \ blast\isanewline |
|
406 \isacommand{qed}\isamarkupfalse% |
|
407 % |
|
408 \endisatagproof |
|
409 {\isafoldproof}% |
|
410 % |
|
411 \isadelimproof |
|
412 % |
|
413 \endisadelimproof |
|
414 % |
|
415 \begin{isamarkuptext}% |
|
416 The result of an \isakeyword{instance} statement is both expressed |
|
417 as a theorem of Isabelle's meta-logic, and as a type arity of the |
|
418 type signature. The latter enables type-inference system to take |
|
419 care of this new instance automatically. |
|
420 |
|
421 \medskip We could now also instantiate our group theory classes to |
|
422 many other concrete types. For example, \isa{int\ {\isasymColon}\ agroup} |
|
423 (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation |
|
424 and \isa{{\isasymone}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup} |
|
425 (e.g.\ if \isa{{\isasymodot}} is defined as list append). Thus, the |
|
426 characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymone}} |
|
427 really become overloaded, i.e.\ have different meanings on different |
|
428 types.% |
|
429 \end{isamarkuptext}% |
|
430 \isamarkuptrue% |
|
431 % |
|
432 \isamarkupsubsection{Lifting and Functors% |
|
433 } |
|
434 \isamarkuptrue% |
|
435 % |
|
436 \begin{isamarkuptext}% |
|
437 As already mentioned above, overloading in the simply-typed HOL |
|
438 systems may include recursion over the syntactic structure of types. |
|
439 That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also |
|
440 contain constants of name \isa{c} on the right-hand side --- if |
|
441 these have types that are structurally simpler than \isa{{\isasymtau}}. |
|
442 |
|
443 This feature enables us to \emph{lift operations}, say to Cartesian |
|
444 products, direct sums or function spaces. Subsequently we lift |
|
445 \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.% |
|
446 \end{isamarkuptext}% |
|
447 \isamarkuptrue% |
|
448 \isacommand{defs}\isamarkupfalse% |
|
449 \ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
|
450 \ \ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\ {\isasymodot}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}{\isachardoublequoteclose}% |
|
451 \begin{isamarkuptext}% |
|
452 It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a} |
|
453 and \isa{{\isasymodot}} on \isa{{\isacharprime}b} transfers to \isa{{\isasymodot}} on \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}. Hence the binary type constructor \isa{{\isasymodot}} maps semigroups |
|
454 to semigroups. This may be established formally as follows.% |
|
455 \end{isamarkuptext}% |
|
456 \isamarkuptrue% |
|
457 \isacommand{instance}\isamarkupfalse% |
|
458 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline |
|
459 % |
|
460 \isadelimproof |
|
461 % |
|
462 \endisadelimproof |
|
463 % |
|
464 \isatagproof |
|
465 \isacommand{proof}\isamarkupfalse% |
|
466 \ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline |
|
467 \ \ \isacommand{fix}\isamarkupfalse% |
|
468 \ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline |
|
469 \ \ \isacommand{show}\isamarkupfalse% |
|
470 \isanewline |
|
471 \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ fst\ r{\isacharcomma}\isanewline |
|
472 \ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ snd\ r{\isacharparenright}\ {\isacharequal}\isanewline |
|
473 \ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline |
|
474 \ \ \ \ \ \ \ \ snd\ p\ {\isasymodot}\ snd\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
475 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
476 \ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline |
|
477 \isacommand{qed}\isamarkupfalse% |
|
478 % |
|
479 \endisatagproof |
|
480 {\isafoldproof}% |
|
481 % |
|
482 \isadelimproof |
|
483 % |
|
484 \endisadelimproof |
|
485 % |
|
486 \begin{isamarkuptext}% |
|
487 Thus, if we view class instances as ``structures'', then overloaded |
|
488 constant definitions with recursion over types indirectly provide |
|
489 some kind of ``functors'' --- i.e.\ mappings between abstract |
|
490 theories.% |
|
491 \end{isamarkuptext}% |
|
492 \isamarkuptrue% |
|
493 % |
|
494 \isadelimtheory |
|
495 % |
|
496 \endisadelimtheory |
|
497 % |
|
498 \isatagtheory |
|
499 \isacommand{end}\isamarkupfalse% |
|
500 % |
|
501 \endisatagtheory |
|
502 {\isafoldtheory}% |
|
503 % |
|
504 \isadelimtheory |
|
505 % |
|
506 \endisadelimtheory |
|
507 \isanewline |
|
508 \end{isabellebody}% |
|
509 %%% Local Variables: |
|
510 %%% mode: latex |
|
511 %%% TeX-master: "root" |
|
512 %%% End: |
|