1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Axioms}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \isamarkupsubsection{Axioms% |
|
19 } |
|
20 \isamarkuptrue% |
|
21 % |
|
22 \begin{isamarkuptext}% |
|
23 Attaching axioms to our classes lets us reason on the level of |
|
24 classes. The results will be applicable to all types in a class, just |
|
25 as in axiomatic mathematics. |
|
26 |
|
27 \begin{warn} |
|
28 Proofs in this section use structured \emph{Isar} proofs, which are not |
|
29 covered in this tutorial; but see \cite{Nipkow-TYPES02}.% |
|
30 \end{warn}% |
|
31 \end{isamarkuptext}% |
|
32 \isamarkuptrue% |
|
33 % |
|
34 \isamarkupsubsubsection{Semigroups% |
|
35 } |
|
36 \isamarkuptrue% |
|
37 % |
|
38 \begin{isamarkuptext}% |
|
39 We specify \emph{semigroups} as subclass of \isa{plus}:% |
|
40 \end{isamarkuptext}% |
|
41 \isamarkuptrue% |
|
42 \isacommand{class}\isamarkupfalse% |
|
43 \ semigroup\ {\isaliteral{3D}{\isacharequal}}\ plus\ {\isaliteral{2B}{\isacharplus}}\isanewline |
|
44 \ \ \isakeyword{assumes}\ assoc{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
45 \begin{isamarkuptext}% |
|
46 \noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification requires that |
|
47 all instances of \isa{semigroup} obey \hyperlink{fact.assoc:}{\mbox{\isa{assoc{\isaliteral{3A}{\isacharcolon}}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. |
|
48 |
|
49 We can use this class axiom to derive further abstract theorems |
|
50 relative to class \isa{semigroup}:% |
|
51 \end{isamarkuptext}% |
|
52 \isamarkuptrue% |
|
53 \isacommand{lemma}\isamarkupfalse% |
|
54 \ assoc{\isaliteral{5F}{\isacharunderscore}}left{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
55 \ \ \isakeyword{fixes}\ x\ y\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
56 \ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
57 % |
|
58 \isadelimproof |
|
59 \ \ % |
|
60 \endisadelimproof |
|
61 % |
|
62 \isatagproof |
|
63 \isacommand{using}\isamarkupfalse% |
|
64 \ assoc\ \isacommand{by}\isamarkupfalse% |
|
65 \ {\isaliteral{28}{\isacharparenleft}}rule\ sym{\isaliteral{29}{\isacharparenright}}% |
|
66 \endisatagproof |
|
67 {\isafoldproof}% |
|
68 % |
|
69 \isadelimproof |
|
70 % |
|
71 \endisadelimproof |
|
72 % |
|
73 \begin{isamarkuptext}% |
|
74 \noindent The \isa{semigroup} constraint on type \isa{{\isaliteral{27}{\isacharprime}}a} restricts instantiations of \isa{{\isaliteral{27}{\isacharprime}}a} to types of class |
|
75 \isa{semigroup} and during the proof enables us to use the fact |
|
76 \hyperlink{fact.assoc}{\mbox{\isa{assoc}}} whose type parameter is itself constrained to class |
|
77 \isa{semigroup}. The main advantage of classes is that theorems |
|
78 can be proved in the abstract and freely reused for each instance. |
|
79 |
|
80 On instantiation, we have to give a proof that the given operations |
|
81 obey the class axioms:% |
|
82 \end{isamarkuptext}% |
|
83 \isamarkuptrue% |
|
84 \isacommand{instantiation}\isamarkupfalse% |
|
85 \ nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ semigroup\isanewline |
|
86 \isakeyword{begin}\isanewline |
|
87 \isanewline |
|
88 \isacommand{instance}\isamarkupfalse% |
|
89 % |
|
90 \isadelimproof |
|
91 \ % |
|
92 \endisadelimproof |
|
93 % |
|
94 \isatagproof |
|
95 \isacommand{proof}\isamarkupfalse% |
|
96 % |
|
97 \begin{isamarkuptxt}% |
|
98 \noindent The proof opens with a default proof step, which for |
|
99 instance judgements invokes method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}}.% |
|
100 \end{isamarkuptxt}% |
|
101 \isamarkuptrue% |
|
102 \ \ \isacommand{fix}\isamarkupfalse% |
|
103 \ m\ n\ q\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
|
104 \ \ \isacommand{show}\isamarkupfalse% |
|
105 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ q\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ q{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
106 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
107 \ {\isaliteral{28}{\isacharparenleft}}induct\ m{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all\isanewline |
|
108 \isacommand{qed}\isamarkupfalse% |
|
109 % |
|
110 \endisatagproof |
|
111 {\isafoldproof}% |
|
112 % |
|
113 \isadelimproof |
|
114 % |
|
115 \endisadelimproof |
|
116 \isanewline |
|
117 \isanewline |
|
118 \isacommand{end}\isamarkupfalse% |
|
119 % |
|
120 \begin{isamarkuptext}% |
|
121 \noindent Again, the interesting things enter the stage with |
|
122 parametric types:% |
|
123 \end{isamarkuptext}% |
|
124 \isamarkuptrue% |
|
125 \isacommand{instantiation}\isamarkupfalse% |
|
126 \ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}semigroup{\isaliteral{2C}{\isacharcomma}}\ semigroup{\isaliteral{29}{\isacharparenright}}\ semigroup\isanewline |
|
127 \isakeyword{begin}\isanewline |
|
128 \isanewline |
|
129 \isacommand{instance}\isamarkupfalse% |
|
130 % |
|
131 \isadelimproof |
|
132 \ % |
|
133 \endisadelimproof |
|
134 % |
|
135 \isatagproof |
|
136 \isacommand{proof}\isamarkupfalse% |
|
137 \isanewline |
|
138 \ \ \isacommand{fix}\isamarkupfalse% |
|
139 \ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
140 \ \ \isacommand{show}\isamarkupfalse% |
|
141 \ {\isaliteral{22}{\isachardoublequoteopen}}p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
142 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
143 \ {\isaliteral{28}{\isacharparenleft}}cases\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ cases\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ cases\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ assoc{\isaliteral{29}{\isacharparenright}}% |
|
144 \begin{isamarkuptxt}% |
|
145 \noindent Associativity of product semigroups is established |
|
146 using the hypothetical associativity \hyperlink{fact.assoc}{\mbox{\isa{assoc}}} of the type |
|
147 components, which holds due to the \isa{semigroup} constraints |
|
148 imposed on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition. |
|
149 Indeed, this pattern often occurs with parametric types and type |
|
150 classes.% |
|
151 \end{isamarkuptxt}% |
|
152 \isamarkuptrue% |
|
153 \isacommand{qed}\isamarkupfalse% |
|
154 % |
|
155 \endisatagproof |
|
156 {\isafoldproof}% |
|
157 % |
|
158 \isadelimproof |
|
159 % |
|
160 \endisadelimproof |
|
161 \isanewline |
|
162 \isanewline |
|
163 \isacommand{end}\isamarkupfalse% |
|
164 % |
|
165 \isamarkupsubsubsection{Monoids% |
|
166 } |
|
167 \isamarkuptrue% |
|
168 % |
|
169 \begin{isamarkuptext}% |
|
170 We define a subclass \isa{monoidl} (a semigroup with a |
|
171 left-hand neutral) by extending \isa{semigroup} with one additional |
|
172 parameter \isa{neutral} together with its property:% |
|
173 \end{isamarkuptext}% |
|
174 \isamarkuptrue% |
|
175 \isacommand{class}\isamarkupfalse% |
|
176 \ monoidl\ {\isaliteral{3D}{\isacharequal}}\ semigroup\ {\isaliteral{2B}{\isacharplus}}\isanewline |
|
177 \ \ \isakeyword{fixes}\ neutral\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7A65726F3E}{\isasymzero}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
178 \ \ \isakeyword{assumes}\ neutl{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7A65726F3E}{\isasymzero}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}% |
|
179 \begin{isamarkuptext}% |
|
180 \noindent Again, we prove some instances, by providing |
|
181 suitable parameter definitions and proofs for the additional |
|
182 specifications.% |
|
183 \end{isamarkuptext}% |
|
184 \isamarkuptrue% |
|
185 \isacommand{instantiation}\isamarkupfalse% |
|
186 \ nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ monoidl\isanewline |
|
187 \isakeyword{begin}\isanewline |
|
188 \isanewline |
|
189 \isacommand{definition}\isamarkupfalse% |
|
190 \isanewline |
|
191 \ \ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7A65726F3E}{\isasymzero}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
192 \isanewline |
|
193 \isacommand{instance}\isamarkupfalse% |
|
194 % |
|
195 \isadelimproof |
|
196 \ % |
|
197 \endisadelimproof |
|
198 % |
|
199 \isatagproof |
|
200 \isacommand{proof}\isamarkupfalse% |
|
201 \isanewline |
|
202 \ \ \isacommand{fix}\isamarkupfalse% |
|
203 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
|
204 \ \ \isacommand{show}\isamarkupfalse% |
|
205 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7A65726F3E}{\isasymzero}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
206 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
207 \ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
|
208 \ simp\isanewline |
|
209 \isacommand{qed}\isamarkupfalse% |
|
210 % |
|
211 \endisatagproof |
|
212 {\isafoldproof}% |
|
213 % |
|
214 \isadelimproof |
|
215 % |
|
216 \endisadelimproof |
|
217 \isanewline |
|
218 \isanewline |
|
219 \isacommand{end}\isamarkupfalse% |
|
220 % |
|
221 \begin{isamarkuptext}% |
|
222 \noindent In contrast to the examples above, we here have both |
|
223 specification of class operations and a non-trivial instance proof. |
|
224 |
|
225 This covers products as well:% |
|
226 \end{isamarkuptext}% |
|
227 \isamarkuptrue% |
|
228 \isacommand{instantiation}\isamarkupfalse% |
|
229 \ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}monoidl{\isaliteral{2C}{\isacharcomma}}\ monoidl{\isaliteral{29}{\isacharparenright}}\ monoidl\isanewline |
|
230 \isakeyword{begin}\isanewline |
|
231 \isanewline |
|
232 \isacommand{definition}\isamarkupfalse% |
|
233 \isanewline |
|
234 \ \ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7A65726F3E}{\isasymzero}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7A65726F3E}{\isasymzero}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7A65726F3E}{\isasymzero}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
235 \isanewline |
|
236 \isacommand{instance}\isamarkupfalse% |
|
237 % |
|
238 \isadelimproof |
|
239 \ % |
|
240 \endisadelimproof |
|
241 % |
|
242 \isatagproof |
|
243 \isacommand{proof}\isamarkupfalse% |
|
244 \isanewline |
|
245 \ \ \isacommand{fix}\isamarkupfalse% |
|
246 \ p\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoidl\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoidl{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
247 \ \ \isacommand{show}\isamarkupfalse% |
|
248 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7A65726F3E}{\isasymzero}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ p\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
249 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
250 \ {\isaliteral{28}{\isacharparenleft}}cases\ p{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ neutl{\isaliteral{29}{\isacharparenright}}\isanewline |
|
251 \isacommand{qed}\isamarkupfalse% |
|
252 % |
|
253 \endisatagproof |
|
254 {\isafoldproof}% |
|
255 % |
|
256 \isadelimproof |
|
257 % |
|
258 \endisadelimproof |
|
259 \isanewline |
|
260 \isanewline |
|
261 \isacommand{end}\isamarkupfalse% |
|
262 % |
|
263 \begin{isamarkuptext}% |
|
264 \noindent Fully-fledged monoids are modelled by another |
|
265 subclass which does not add new parameters but tightens the |
|
266 specification:% |
|
267 \end{isamarkuptext}% |
|
268 \isamarkuptrue% |
|
269 \isacommand{class}\isamarkupfalse% |
|
270 \ monoid\ {\isaliteral{3D}{\isacharequal}}\ monoidl\ {\isaliteral{2B}{\isacharplus}}\isanewline |
|
271 \ \ \isakeyword{assumes}\ neutr{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{5C3C7A65726F3E}{\isasymzero}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}% |
|
272 \begin{isamarkuptext}% |
|
273 \noindent Corresponding instances for \isa{nat} and products |
|
274 are left as an exercise to the reader.% |
|
275 \end{isamarkuptext}% |
|
276 \isamarkuptrue% |
|
277 % |
|
278 \isamarkupsubsubsection{Groups% |
|
279 } |
|
280 \isamarkuptrue% |
|
281 % |
|
282 \begin{isamarkuptext}% |
|
283 \noindent To finish our small algebra example, we add a \isa{group} class:% |
|
284 \end{isamarkuptext}% |
|
285 \isamarkuptrue% |
|
286 \isacommand{class}\isamarkupfalse% |
|
287 \ group\ {\isaliteral{3D}{\isacharequal}}\ monoidl\ {\isaliteral{2B}{\isacharplus}}\isanewline |
|
288 \ \ \isakeyword{fixes}\ inv\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{8}}{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{8}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
289 \ \ \isakeyword{assumes}\ invl{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7A65726F3E}{\isasymzero}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
290 \begin{isamarkuptext}% |
|
291 \noindent We continue with a further example for abstract |
|
292 proofs relative to type classes:% |
|
293 \end{isamarkuptext}% |
|
294 \isamarkuptrue% |
|
295 \isacommand{lemma}\isamarkupfalse% |
|
296 \ left{\isaliteral{5F}{\isacharunderscore}}cancel{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
297 \ \ \isakeyword{fixes}\ x\ y\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}group{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
298 \ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
299 % |
|
300 \isadelimproof |
|
301 % |
|
302 \endisadelimproof |
|
303 % |
|
304 \isatagproof |
|
305 \isacommand{proof}\isamarkupfalse% |
|
306 \isanewline |
|
307 \ \ \isacommand{assume}\isamarkupfalse% |
|
308 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
309 \ \ \isacommand{then}\isamarkupfalse% |
|
310 \ \isacommand{have}\isamarkupfalse% |
|
311 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
312 \ simp\isanewline |
|
313 \ \ \isacommand{then}\isamarkupfalse% |
|
314 \ \isacommand{have}\isamarkupfalse% |
|
315 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
316 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ assoc{\isaliteral{29}{\isacharparenright}}\isanewline |
|
317 \ \ \isacommand{then}\isamarkupfalse% |
|
318 \ \isacommand{show}\isamarkupfalse% |
|
319 \ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
320 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ invl\ neutl{\isaliteral{29}{\isacharparenright}}\isanewline |
|
321 \isacommand{next}\isamarkupfalse% |
|
322 \isanewline |
|
323 \ \ \isacommand{assume}\isamarkupfalse% |
|
324 \ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
325 \ \ \isacommand{then}\isamarkupfalse% |
|
326 \ \isacommand{show}\isamarkupfalse% |
|
327 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
328 \ simp\isanewline |
|
329 \isacommand{qed}\isamarkupfalse% |
|
330 % |
|
331 \endisatagproof |
|
332 {\isafoldproof}% |
|
333 % |
|
334 \isadelimproof |
|
335 % |
|
336 \endisadelimproof |
|
337 % |
|
338 \begin{isamarkuptext}% |
|
339 \noindent Any \isa{group} is also a \isa{monoid}; this |
|
340 can be made explicit by claiming an additional subclass relation, |
|
341 together with a proof of the logical difference:% |
|
342 \end{isamarkuptext}% |
|
343 \isamarkuptrue% |
|
344 \isacommand{instance}\isamarkupfalse% |
|
345 \ group\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ monoid\isanewline |
|
346 % |
|
347 \isadelimproof |
|
348 % |
|
349 \endisadelimproof |
|
350 % |
|
351 \isatagproof |
|
352 \isacommand{proof}\isamarkupfalse% |
|
353 \isanewline |
|
354 \ \ \isacommand{fix}\isamarkupfalse% |
|
355 \ x\isanewline |
|
356 \ \ \isacommand{from}\isamarkupfalse% |
|
357 \ invl\ \isacommand{have}\isamarkupfalse% |
|
358 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7A65726F3E}{\isasymzero}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
359 \isanewline |
|
360 \ \ \isacommand{then}\isamarkupfalse% |
|
361 \ \isacommand{have}\isamarkupfalse% |
|
362 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{5C3C7A65726F3E}{\isasymzero}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
363 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
364 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ neutl\ invl\ assoc\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
365 \ \ \isacommand{then}\isamarkupfalse% |
|
366 \ \isacommand{show}\isamarkupfalse% |
|
367 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{5C3C7A65726F3E}{\isasymzero}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
|
368 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ left{\isaliteral{5F}{\isacharunderscore}}cancel{\isaliteral{29}{\isacharparenright}}\isanewline |
|
369 \isacommand{qed}\isamarkupfalse% |
|
370 % |
|
371 \endisatagproof |
|
372 {\isafoldproof}% |
|
373 % |
|
374 \isadelimproof |
|
375 % |
|
376 \endisadelimproof |
|
377 % |
|
378 \begin{isamarkuptext}% |
|
379 \noindent The proof result is propagated to the type system, |
|
380 making \isa{group} an instance of \isa{monoid} by adding an |
|
381 additional edge to the graph of subclass relation; see also |
|
382 Figure~\ref{fig:subclass}. |
|
383 |
|
384 \begin{figure}[htbp] |
|
385 \begin{center} |
|
386 \small |
|
387 \unitlength 0.6mm |
|
388 \begin{picture}(40,60)(0,0) |
|
389 \put(20,60){\makebox(0,0){\isa{semigroup}}} |
|
390 \put(20,40){\makebox(0,0){\isa{monoidl}}} |
|
391 \put(00,20){\makebox(0,0){\isa{monoid}}} |
|
392 \put(40,00){\makebox(0,0){\isa{group}}} |
|
393 \put(20,55){\vector(0,-1){10}} |
|
394 \put(15,35){\vector(-1,-1){10}} |
|
395 \put(25,35){\vector(1,-3){10}} |
|
396 \end{picture} |
|
397 \hspace{8em} |
|
398 \begin{picture}(40,60)(0,0) |
|
399 \put(20,60){\makebox(0,0){\isa{semigroup}}} |
|
400 \put(20,40){\makebox(0,0){\isa{monoidl}}} |
|
401 \put(00,20){\makebox(0,0){\isa{monoid}}} |
|
402 \put(40,00){\makebox(0,0){\isa{group}}} |
|
403 \put(20,55){\vector(0,-1){10}} |
|
404 \put(15,35){\vector(-1,-1){10}} |
|
405 \put(05,15){\vector(3,-1){30}} |
|
406 \end{picture} |
|
407 \caption{Subclass relationship of monoids and groups: |
|
408 before and after establishing the relationship |
|
409 \isa{group\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ monoid}; transitive edges are left out.} |
|
410 \label{fig:subclass} |
|
411 \end{center} |
|
412 \end{figure}% |
|
413 \end{isamarkuptext}% |
|
414 \isamarkuptrue% |
|
415 % |
|
416 \isamarkupsubsubsection{Inconsistencies% |
|
417 } |
|
418 \isamarkuptrue% |
|
419 % |
|
420 \begin{isamarkuptext}% |
|
421 The reader may be wondering what happens if we attach an |
|
422 inconsistent set of axioms to a class. So far we have always avoided |
|
423 to add new axioms to HOL for fear of inconsistencies and suddenly it |
|
424 seems that we are throwing all caution to the wind. So why is there no |
|
425 problem? |
|
426 |
|
427 The point is that by construction, all type variables in the axioms of |
|
428 a \isacommand{class} are automatically constrained with the class |
|
429 being defined (as shown for axiom \isa{refl} above). These |
|
430 constraints are always carried around and Isabelle takes care that |
|
431 they are never lost, unless the type variable is instantiated with a |
|
432 type that has been shown to belong to that class. Thus you may be able |
|
433 to prove \isa{False} from your axioms, but Isabelle will remind you |
|
434 that this theorem has the hidden hypothesis that the class is |
|
435 non-empty. |
|
436 |
|
437 Even if each individual class is consistent, intersections of |
|
438 (unrelated) classes readily become inconsistent in practice. Now we |
|
439 know this need not worry us.% |
|
440 \end{isamarkuptext}% |
|
441 \isamarkuptrue% |
|
442 % |
|
443 \isamarkupsubsubsection{Syntactic Classes and Predefined Overloading% |
|
444 } |
|
445 \isamarkuptrue% |
|
446 % |
|
447 \begin{isamarkuptext}% |
|
448 In our algebra example, we have started with a \emph{syntactic |
|
449 class} \isa{plus} which only specifies operations but no axioms; it |
|
450 would have been also possible to start immediately with class \isa{semigroup}, specifying the \isa{{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}} operation and associativity at |
|
451 the same time. |
|
452 |
|
453 Which approach is more appropriate depends. Usually it is more |
|
454 convenient to introduce operations and axioms in the same class: then |
|
455 the type checker will automatically insert the corresponding class |
|
456 constraints whenever the operations occur, reducing the need of manual |
|
457 annotations. However, when operations are decorated with popular |
|
458 syntax, syntactic classes can be an option to re-use the syntax in |
|
459 different contexts; this is indeed the way most overloaded constants |
|
460 in HOL are introduced, of which the most important are listed in |
|
461 Table~\ref{tab:overloading} in the appendix. Section |
|
462 \ref{sec:numeric-classes} covers a range of corresponding classes |
|
463 \emph{with} axioms. |
|
464 |
|
465 Further note that classes may contain axioms but \emph{no} operations. |
|
466 An example is class \isa{finite} from theory \isa{Finite{\isaliteral{5F}{\isacharunderscore}}Set} |
|
467 which specifies a type to be finite: \isa{{\isaliteral{22}{\isachardoublequote}}finite\ {\isaliteral{28}{\isacharparenleft}}UNIV\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}finite\ set{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.% |
|
468 \end{isamarkuptext}% |
|
469 \isamarkuptrue% |
|
470 % |
|
471 \isadelimtheory |
|
472 % |
|
473 \endisadelimtheory |
|
474 % |
|
475 \isatagtheory |
|
476 % |
|
477 \endisatagtheory |
|
478 {\isafoldtheory}% |
|
479 % |
|
480 \isadelimtheory |
|
481 % |
|
482 \endisadelimtheory |
|
483 \end{isabellebody}% |
|
484 %%% Local Variables: |
|
485 %%% mode: latex |
|
486 %%% TeX-master: "root" |
|
487 %%% End: |
|