198 show "x \<odot> \<one> = x" |
198 show "x \<odot> \<one> = x" |
199 by (rule group_right_unit) |
199 by (rule group_right_unit) |
200 qed |
200 qed |
201 |
201 |
202 text {* |
202 text {* |
203 \medskip The $\INSTANCE$ command sets up an appropriate goal that |
203 \medskip The \isakeyword{instance} command sets up an appropriate |
204 represents the class inclusion (or type arity, see |
204 goal that represents the class inclusion (or type arity, see |
205 \secref{sec:inst-arity}) to be proven (see also |
205 \secref{sec:inst-arity}) to be proven (see also |
206 \cite{isabelle-isar-ref}). The initial proof step causes |
206 \cite{isabelle-isar-ref}). The initial proof step causes |
207 back-chaining of class membership statements wrt.\ the hierarchy of |
207 back-chaining of class membership statements wrt.\ the hierarchy of |
208 any classes defined in the current theory; the effect is to reduce |
208 any classes defined in the current theory; the effect is to reduce |
209 to the initial statement to a number of goals that directly |
209 to the initial statement to a number of goals that directly |
213 |
213 |
214 |
214 |
215 subsection {* Concrete instantiation \label{sec:inst-arity} *} |
215 subsection {* Concrete instantiation \label{sec:inst-arity} *} |
216 |
216 |
217 text {* |
217 text {* |
218 So far we have covered the case of the form $\INSTANCE$~@{text |
218 So far we have covered the case of the form |
219 "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely \emph{abstract instantiation} --- |
219 \isakeyword{instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely |
220 $c@1$ is more special than @{text "c\<^sub>1"} and thus an instance |
220 \emph{abstract instantiation} --- $c@1$ is more special than @{text |
221 of @{text "c\<^sub>2"}. Even more interesting for practical |
221 "c\<^sub>1"} and thus an instance of @{text "c\<^sub>2"}. Even more |
222 applications are \emph{concrete instantiations} of axiomatic type |
222 interesting for practical applications are \emph{concrete |
223 classes. That is, certain simple schemes @{text "(\<alpha>\<^sub>1, \<dots>, |
223 instantiations} of axiomatic type classes. That is, certain simple |
224 \<alpha>\<^sub>n) t \<Colon> c"} of class membership may be established at the |
224 schemes @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Colon> c"} of class |
225 logical level and then transferred to Isabelle's type signature |
225 membership may be established at the logical level and then |
226 level. |
226 transferred to Isabelle's type signature level. |
227 |
227 |
228 \medskip As a typical example, we show that type @{typ bool} with |
228 \medskip As a typical example, we show that type @{typ bool} with |
229 exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and |
229 exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and |
230 @{term False} as @{text \<one>} forms an Abelian group. |
230 @{term False} as @{text \<one>} forms an Abelian group. |
231 *} |
231 *} |
234 times_bool_def: "x \<odot> y \<equiv> x \<noteq> (y\<Colon>bool)" |
234 times_bool_def: "x \<odot> y \<equiv> x \<noteq> (y\<Colon>bool)" |
235 inverse_bool_def: "x\<inv> \<equiv> x\<Colon>bool" |
235 inverse_bool_def: "x\<inv> \<equiv> x\<Colon>bool" |
236 unit_bool_def: "\<one> \<equiv> False" |
236 unit_bool_def: "\<one> \<equiv> False" |
237 |
237 |
238 text {* |
238 text {* |
239 \medskip It is important to note that above $\DEFS$ are just |
239 \medskip It is important to note that above \isakeyword{defs} are |
240 overloaded meta-level constant definitions, where type classes are |
240 just overloaded meta-level constant definitions, where type classes |
241 not yet involved at all. This form of constant definition with |
241 are not yet involved at all. This form of constant definition with |
242 overloading (and optional recursion over the syntactic structure of |
242 overloading (and optional recursion over the syntactic structure of |
243 simple types) are admissible as definitional extensions of plain HOL |
243 simple types) are admissible as definitional extensions of plain HOL |
244 \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not |
244 \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not |
245 required for overloading. Nevertheless, overloaded definitions are |
245 required for overloading. Nevertheless, overloaded definitions are |
246 best applied in the context of type classes. |
246 best applied in the context of type classes. |
247 |
247 |
248 \medskip Since we have chosen above $\DEFS$ of the generic group |
248 \medskip Since we have chosen above \isakeyword{defs} of the generic |
249 operations on type @{typ bool} appropriately, the class membership |
249 group operations on type @{typ bool} appropriately, the class |
250 @{text "bool \<Colon> agroup"} may be now derived as follows. |
250 membership @{text "bool \<Colon> agroup"} may be now derived as follows. |
251 *} |
251 *} |
252 |
252 |
253 instance bool :: agroup |
253 instance bool :: agroup |
254 proof (intro_classes, |
254 proof (intro_classes, |
255 unfold times_bool_def inverse_bool_def unit_bool_def) |
255 unfold times_bool_def inverse_bool_def unit_bool_def) |
259 show "(x \<noteq> x) = False" by blast |
259 show "(x \<noteq> x) = False" by blast |
260 show "(x \<noteq> y) = (y \<noteq> x)" by blast |
260 show "(x \<noteq> y) = (y \<noteq> x)" by blast |
261 qed |
261 qed |
262 |
262 |
263 text {* |
263 text {* |
264 The result of an $\INSTANCE$ statement is both expressed as a |
264 The result of an \isakeyword{instance} statement is both expressed |
265 theorem of Isabelle's meta-logic, and as a type arity of the type |
265 as a theorem of Isabelle's meta-logic, and as a type arity of the |
266 signature. The latter enables type-inference system to take care of |
266 type signature. The latter enables type-inference system to take |
267 this new instance automatically. |
267 care of this new instance automatically. |
268 |
268 |
269 \medskip We could now also instantiate our group theory classes to |
269 \medskip We could now also instantiate our group theory classes to |
270 many other concrete types. For example, @{text "int \<Colon> agroup"} |
270 many other concrete types. For example, @{text "int \<Colon> agroup"} |
271 (e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation |
271 (e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation |
272 and @{text \<one>} as zero) or @{text "list \<Colon> (type) semigroup"} |
272 and @{text \<one>} as zero) or @{text "list \<Colon> (type) semigroup"} |