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