7 \isamarkuptrue% |
7 \isamarkuptrue% |
8 \isacommand{theory}\ Group\ {\isacharequal}\ Main{\isacharcolon}\isamarkupfalse% |
8 \isacommand{theory}\ Group\ {\isacharequal}\ Main{\isacharcolon}\isamarkupfalse% |
9 % |
9 % |
10 \begin{isamarkuptext}% |
10 \begin{isamarkuptext}% |
11 \medskip\noindent The meta-level type system of Isabelle supports |
11 \medskip\noindent The meta-level type system of Isabelle supports |
12 \emph{intersections} and \emph{inclusions} of type classes. These |
12 \emph{intersections} and \emph{inclusions} of type classes. These |
13 directly correspond to intersections and inclusions of type |
13 directly correspond to intersections and inclusions of type |
14 predicates in a purely set theoretic sense. This is sufficient as a |
14 predicates in a purely set theoretic sense. This is sufficient as a |
15 means to describe simple hierarchies of structures. As an |
15 means to describe simple hierarchies of structures. As an |
16 illustration, we use the well-known example of semigroups, monoids, |
16 illustration, we use the well-known example of semigroups, monoids, |
17 general groups and Abelian groups.% |
17 general groups and Abelian groups.% |
18 \end{isamarkuptext}% |
18 \end{isamarkuptext}% |
19 \isamarkuptrue% |
19 \isamarkuptrue% |
20 % |
20 % |
21 \isamarkupsubsection{Monoids and Groups% |
21 \isamarkupsubsection{Monoids and Groups% |
22 } |
22 } |
23 \isamarkuptrue% |
23 \isamarkuptrue% |
24 % |
24 % |
25 \begin{isamarkuptext}% |
25 \begin{isamarkuptext}% |
26 First we declare some polymorphic constants required later for the |
26 First we declare some polymorphic constants required later for the |
27 signature parts of our structures.% |
27 signature parts of our structures.% |
28 \end{isamarkuptext}% |
28 \end{isamarkuptext}% |
29 \isamarkuptrue% |
29 \isamarkuptrue% |
30 \isacommand{consts}\isanewline |
30 \isacommand{consts}\isanewline |
31 \ \ 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 |
31 \ \ 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 |
32 \ \ 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 |
32 \ \ 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 |
33 \ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}\isamarkupfalse% |
33 \ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}\isamarkupfalse% |
34 % |
34 % |
35 \begin{isamarkuptext}% |
35 \begin{isamarkuptext}% |
36 \noindent Next we define class \isa{monoid} of monoids with |
36 \noindent Next we define class \isa{monoid} of monoids with |
37 operations \isa{{\isasymodot}} and \isa{{\isasymunit}}. Note that multiple class |
37 operations \isa{{\isasymodot}} and \isa{{\isasymunit}}. Note that multiple class |
38 axioms are allowed for user convenience --- they simply represent the |
38 axioms are allowed for user convenience --- they simply represent |
39 conjunction of their respective universal closures.% |
39 the conjunction of their respective universal closures.% |
40 \end{isamarkuptext}% |
40 \end{isamarkuptext}% |
41 \isamarkuptrue% |
41 \isamarkuptrue% |
42 \isacommand{axclass}\ monoid\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
42 \isacommand{axclass}\ monoid\ {\isasymsubseteq}\ type\isanewline |
43 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
43 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
44 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
44 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
45 \ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse% |
45 \ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse% |
46 % |
46 % |
47 \begin{isamarkuptext}% |
47 \begin{isamarkuptext}% |
48 \noindent So class \isa{monoid} contains exactly those types \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymunit}\ {\isasymColon}\ {\isasymtau}} are |
48 \noindent So class \isa{monoid} contains exactly those types |
49 specified appropriately, such that \isa{{\isasymodot}} is associative and |
49 \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymunit}\ {\isasymColon}\ {\isasymtau}} |
50 \isa{{\isasymunit}} is a left and right unit element for the \isa{{\isasymodot}} |
50 are specified appropriately, such that \isa{{\isasymodot}} is associative and |
51 operation.% |
51 \isa{{\isasymunit}} is a left and right unit element for the \isa{{\isasymodot}} |
|
52 operation.% |
52 \end{isamarkuptext}% |
53 \end{isamarkuptext}% |
53 \isamarkuptrue% |
54 \isamarkuptrue% |
54 % |
55 % |
55 \begin{isamarkuptext}% |
56 \begin{isamarkuptext}% |
56 \medskip Independently of \isa{monoid}, we now define a linear |
57 \medskip Independently of \isa{monoid}, we now define a linear |
57 hierarchy of semigroups, general groups and Abelian groups. Note |
58 hierarchy of semigroups, general groups and Abelian groups. Note |
58 that the names of class axioms are automatically qualified with each |
59 that the names of class axioms are automatically qualified with each |
59 class name, so we may re-use common names such as \isa{assoc}.% |
60 class name, so we may re-use common names such as \isa{assoc}.% |
60 \end{isamarkuptext}% |
61 \end{isamarkuptext}% |
61 \isamarkuptrue% |
62 \isamarkuptrue% |
62 \isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
63 \isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline |
63 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
64 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
64 \isanewline |
65 \isanewline |
65 \isamarkupfalse% |
66 \isamarkupfalse% |
66 \isacommand{axclass}\ group\ {\isasymsubseteq}\ semigroup\isanewline |
67 \isacommand{axclass}\ group\ {\isasymsubseteq}\ semigroup\isanewline |
67 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
68 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
71 \isacommand{axclass}\ agroup\ {\isasymsubseteq}\ group\isanewline |
72 \isacommand{axclass}\ agroup\ {\isasymsubseteq}\ group\isanewline |
72 \ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}\isamarkupfalse% |
73 \ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}\isamarkupfalse% |
73 % |
74 % |
74 \begin{isamarkuptext}% |
75 \begin{isamarkuptext}% |
75 \noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}} |
76 \noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}} |
76 from \isa{semigroup} and adds two further group axioms. Similarly, |
77 from \isa{semigroup} and adds two further group axioms. Similarly, |
77 \isa{agroup} is defined as the subset of \isa{group} such that |
78 \isa{agroup} is defined as the subset of \isa{group} such that |
78 for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.% |
79 for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.% |
79 \end{isamarkuptext}% |
80 \end{isamarkuptext}% |
80 \isamarkuptrue% |
81 \isamarkuptrue% |
81 % |
82 % |
82 \isamarkupsubsection{Abstract reasoning% |
83 \isamarkupsubsection{Abstract reasoning% |
83 } |
84 } |
84 \isamarkuptrue% |
85 \isamarkuptrue% |
85 % |
86 % |
86 \begin{isamarkuptext}% |
87 \begin{isamarkuptext}% |
87 In a sense, axiomatic type classes may be viewed as \emph{abstract |
88 In a sense, axiomatic type classes may be viewed as \emph{abstract |
88 theories}. Above class definitions gives rise to abstract axioms |
89 theories}. Above class definitions gives rise to abstract axioms |
89 \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} |
90 \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 |
90 that is restricted to types of the corresponding class \isa{c}. |
91 precondition for the whole formula. For example, \isa{assoc} |
91 \emph{Sort constraints} like this express a logical precondition for |
92 states that for all \isa{{\isasymtau}}, provided that \isa{{\isasymtau}\ {\isasymColon}\ semigroup}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is associative. |
92 the whole formula. For example, \isa{assoc} states that for all |
93 |
93 \isa{{\isasymtau}}, provided that \isa{{\isasymtau}\ {\isasymColon}\ semigroup}, the operation |
94 \medskip From a technical point of view, abstract axioms are just |
94 \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is associative. |
95 ordinary Isabelle theorems, which may be used in proofs without |
95 |
96 special treatment. Such ``abstract proofs'' usually yield new |
96 \medskip From a technical point of view, abstract axioms are just |
97 ``abstract theorems''. For example, we may now derive the following |
97 ordinary Isabelle theorems, which may be used in proofs without |
98 well-known laws of general groups.% |
98 special treatment. Such ``abstract proofs'' usually yield new |
|
99 ``abstract theorems''. For example, we may now derive the following |
|
100 well-known laws of general groups.% |
|
101 \end{isamarkuptext}% |
99 \end{isamarkuptext}% |
102 \isamarkuptrue% |
100 \isamarkuptrue% |
103 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
101 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
104 \isamarkupfalse% |
102 \isamarkupfalse% |
105 \isacommand{proof}\ {\isacharminus}\isanewline |
103 \isacommand{proof}\ {\isacharminus}\isanewline |
183 \isamarkupfalse% |
181 \isamarkupfalse% |
184 \isacommand{qed}\isamarkupfalse% |
182 \isacommand{qed}\isamarkupfalse% |
185 % |
183 % |
186 \begin{isamarkuptext}% |
184 \begin{isamarkuptext}% |
187 \medskip Abstract theorems may be instantiated to only those types |
185 \medskip Abstract theorems may be instantiated to only those types |
188 \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is |
186 \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is |
189 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}.% |
187 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}.% |
190 \end{isamarkuptext}% |
188 \end{isamarkuptext}% |
191 \isamarkuptrue% |
189 \isamarkuptrue% |
192 % |
190 % |
193 \isamarkupsubsection{Abstract instantiation% |
191 \isamarkupsubsection{Abstract instantiation% |
194 } |
192 } |
195 \isamarkuptrue% |
193 \isamarkuptrue% |
196 % |
194 % |
197 \begin{isamarkuptext}% |
195 \begin{isamarkuptext}% |
198 From the definition, the \isa{monoid} and \isa{group} classes |
196 From the definition, the \isa{monoid} and \isa{group} classes |
199 have been independent. Note that for monoids, \isa{right{\isacharunderscore}unit} had |
197 have been independent. Note that for monoids, \isa{right{\isacharunderscore}unit} |
200 to be included as an axiom, but for groups both \isa{right{\isacharunderscore}unit} |
198 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 |
201 and \isa{right{\isacharunderscore}inverse} are derivable from the other axioms. With |
199 axioms. With \isa{group{\isacharunderscore}right{\isacharunderscore}unit} derived as a theorem of group |
202 \isa{group{\isacharunderscore}right{\isacharunderscore}unit} derived as a theorem of group theory (see |
200 theory (see page~\pageref{thm:group-right-unit}), we may now |
203 page~\pageref{thm:group-right-unit}), we may now instantiate \isa{monoid\ {\isasymsubseteq}\ semigroup} and \isa{group\ {\isasymsubseteq}\ monoid} properly as |
201 instantiate \isa{monoid\ {\isasymsubseteq}\ semigroup} and \isa{group\ {\isasymsubseteq}\ monoid} properly as follows (cf.\ \figref{fig:monoid-group}). |
204 follows (cf.\ \figref{fig:monoid-group}). |
|
205 |
202 |
206 \begin{figure}[htbp] |
203 \begin{figure}[htbp] |
207 \begin{center} |
204 \begin{center} |
208 \small |
205 \small |
209 \unitlength 0.6mm |
206 \unitlength 0.6mm |
211 \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
208 \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
212 \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}} |
209 \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}} |
213 \put(15,5){\makebox(0,0){\isa{agroup}}} |
210 \put(15,5){\makebox(0,0){\isa{agroup}}} |
214 \put(15,25){\makebox(0,0){\isa{group}}} |
211 \put(15,25){\makebox(0,0){\isa{group}}} |
215 \put(15,45){\makebox(0,0){\isa{semigroup}}} |
212 \put(15,45){\makebox(0,0){\isa{semigroup}}} |
216 \put(30,65){\makebox(0,0){\isa{term}}} \put(50,45){\makebox(0,0){\isa{monoid}}} |
213 \put(30,65){\makebox(0,0){\isa{type}}} \put(50,45){\makebox(0,0){\isa{monoid}}} |
217 \end{picture} |
214 \end{picture} |
218 \hspace{4em} |
215 \hspace{4em} |
219 \begin{picture}(30,90)(0,0) |
216 \begin{picture}(30,90)(0,0) |
220 \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
217 \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
221 \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}} |
218 \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}} |
222 \put(15,5){\makebox(0,0){\isa{agroup}}} |
219 \put(15,5){\makebox(0,0){\isa{agroup}}} |
223 \put(15,25){\makebox(0,0){\isa{group}}} |
220 \put(15,25){\makebox(0,0){\isa{group}}} |
224 \put(15,45){\makebox(0,0){\isa{monoid}}} |
221 \put(15,45){\makebox(0,0){\isa{monoid}}} |
225 \put(15,65){\makebox(0,0){\isa{semigroup}}} |
222 \put(15,65){\makebox(0,0){\isa{semigroup}}} |
226 \put(15,85){\makebox(0,0){\isa{term}}} |
223 \put(15,85){\makebox(0,0){\isa{type}}} |
227 \end{picture} |
224 \end{picture} |
228 \caption{Monoids and groups: according to definition, and by proof} |
225 \caption{Monoids and groups: according to definition, and by proof} |
229 \label{fig:monoid-group} |
226 \label{fig:monoid-group} |
230 \end{center} |
227 \end{center} |
231 \end{figure}% |
228 \end{figure}% |
264 \isamarkupfalse% |
261 \isamarkupfalse% |
265 \isacommand{qed}\isamarkupfalse% |
262 \isacommand{qed}\isamarkupfalse% |
266 % |
263 % |
267 \begin{isamarkuptext}% |
264 \begin{isamarkuptext}% |
268 \medskip The $\INSTANCE$ command sets up an appropriate goal that |
265 \medskip The $\INSTANCE$ command sets up an appropriate goal that |
269 represents the class inclusion (or type arity, see |
266 represents the class inclusion (or type arity, see |
270 \secref{sec:inst-arity}) to be proven (see also |
267 \secref{sec:inst-arity}) to be proven (see also |
271 \cite{isabelle-isar-ref}). The initial proof step causes |
268 \cite{isabelle-isar-ref}). The initial proof step causes |
272 back-chaining of class membership statements wrt.\ the hierarchy of |
269 back-chaining of class membership statements wrt.\ the hierarchy of |
273 any classes defined in the current theory; the effect is to reduce to |
270 any classes defined in the current theory; the effect is to reduce |
274 the initial statement to a number of goals that directly correspond |
271 to the initial statement to a number of goals that directly |
275 to any class axioms encountered on the path upwards through the class |
272 correspond to any class axioms encountered on the path upwards |
276 hierarchy.% |
273 through the class hierarchy.% |
277 \end{isamarkuptext}% |
274 \end{isamarkuptext}% |
278 \isamarkuptrue% |
275 \isamarkuptrue% |
279 % |
276 % |
280 \isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}% |
277 \isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}% |
281 } |
278 } |
282 \isamarkuptrue% |
279 \isamarkuptrue% |
283 % |
280 % |
284 \begin{isamarkuptext}% |
281 \begin{isamarkuptext}% |
285 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} --- |
282 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} --- |
286 $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance |
283 $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance |
287 of \isa{c\isactrlsub {\isadigit{2}}}. Even more interesting for practical |
284 of \isa{c\isactrlsub {\isadigit{2}}}. Even more interesting for practical |
288 applications are \emph{concrete instantiations} of axiomatic type |
285 applications are \emph{concrete instantiations} of axiomatic type |
289 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 |
286 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 |
290 logical level and then transferred to Isabelle's type signature |
287 logical level and then transferred to Isabelle's type signature |
291 level. |
288 level. |
292 |
289 |
293 \medskip As a typical example, we show that type \isa{bool} with |
290 \medskip As a typical example, we show that type \isa{bool} with |
294 exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and |
291 exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and |
295 \isa{False} as \isa{{\isasymunit}} forms an Abelian group.% |
292 \isa{False} as \isa{{\isasymunit}} forms an Abelian group.% |
296 \end{isamarkuptext}% |
293 \end{isamarkuptext}% |
297 \isamarkuptrue% |
294 \isamarkuptrue% |
298 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
295 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
299 \ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline |
296 \ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline |
300 \ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline |
297 \ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline |
301 \ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}\isamarkupfalse% |
298 \ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}\isamarkupfalse% |
302 % |
299 % |
303 \begin{isamarkuptext}% |
300 \begin{isamarkuptext}% |
304 \medskip It is important to note that above $\DEFS$ are just |
301 \medskip It is important to note that above $\DEFS$ are just |
305 overloaded meta-level constant definitions, where type classes are |
302 overloaded meta-level constant definitions, where type classes are |
306 not yet involved at all. This form of constant definition with |
303 not yet involved at all. This form of constant definition with |
307 overloading (and optional recursion over the syntactic structure of |
304 overloading (and optional recursion over the syntactic structure of |
308 simple types) are admissible as definitional extensions of plain HOL |
305 simple types) are admissible as definitional extensions of plain HOL |
309 \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not |
306 \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not |
310 required for overloading. Nevertheless, overloaded definitions are |
307 required for overloading. Nevertheless, overloaded definitions are |
311 best applied in the context of type classes. |
308 best applied in the context of type classes. |
312 |
309 |
313 \medskip Since we have chosen above $\DEFS$ of the generic group |
310 \medskip Since we have chosen above $\DEFS$ of the generic group |
314 operations on type \isa{bool} appropriately, the class membership |
311 operations on type \isa{bool} appropriately, the class membership |
315 \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.% |
312 \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.% |
316 \end{isamarkuptext}% |
313 \end{isamarkuptext}% |
317 \isamarkuptrue% |
314 \isamarkuptrue% |
318 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline |
315 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline |
319 \isamarkupfalse% |
316 \isamarkupfalse% |
320 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline |
317 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline |
335 \isacommand{by}\ blast\isanewline |
332 \isacommand{by}\ blast\isanewline |
336 \isamarkupfalse% |
333 \isamarkupfalse% |
337 \isacommand{qed}\isamarkupfalse% |
334 \isacommand{qed}\isamarkupfalse% |
338 % |
335 % |
339 \begin{isamarkuptext}% |
336 \begin{isamarkuptext}% |
340 The result of an $\INSTANCE$ statement is both expressed as a theorem |
337 The result of an $\INSTANCE$ statement is both expressed as a |
341 of Isabelle's meta-logic, and as a type arity of the type signature. |
338 theorem of Isabelle's meta-logic, and as a type arity of the type |
342 The latter enables type-inference system to take care of this new |
339 signature. The latter enables type-inference system to take care of |
343 instance automatically. |
340 this new instance automatically. |
344 |
341 |
345 \medskip We could now also instantiate our group theory classes to |
342 \medskip We could now also instantiate our group theory classes to |
346 many other concrete types. For example, \isa{int\ {\isasymColon}\ agroup} |
343 many other concrete types. For example, \isa{int\ {\isasymColon}\ agroup} |
347 (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation |
344 (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation |
348 and \isa{{\isasymunit}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}term{\isacharparenright}\ semigroup} |
345 and \isa{{\isasymunit}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup} |
349 (e.g.\ if \isa{{\isasymodot}} is defined as list append). Thus, the |
346 (e.g.\ if \isa{{\isasymodot}} is defined as list append). Thus, the |
350 characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymunit}} |
347 characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymunit}} |
351 really become overloaded, i.e.\ have different meanings on different |
348 really become overloaded, i.e.\ have different meanings on different |
352 types.% |
349 types.% |
353 \end{isamarkuptext}% |
350 \end{isamarkuptext}% |
354 \isamarkuptrue% |
351 \isamarkuptrue% |
355 % |
352 % |
356 \isamarkupsubsection{Lifting and Functors% |
353 \isamarkupsubsection{Lifting and Functors% |
357 } |
354 } |
358 \isamarkuptrue% |
355 \isamarkuptrue% |
359 % |
356 % |
360 \begin{isamarkuptext}% |
357 \begin{isamarkuptext}% |
361 As already mentioned above, overloading in the simply-typed HOL |
358 As already mentioned above, overloading in the simply-typed HOL |
362 systems may include recursion over the syntactic structure of types. |
359 systems may include recursion over the syntactic structure of types. |
363 That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also |
360 That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also |
364 contain constants of name \isa{c} on the right-hand side --- if |
361 contain constants of name \isa{c} on the right-hand side --- if |
365 these have types that are structurally simpler than \isa{{\isasymtau}}. |
362 these have types that are structurally simpler than \isa{{\isasymtau}}. |
366 |
363 |
367 This feature enables us to \emph{lift operations}, say to Cartesian |
364 This feature enables us to \emph{lift operations}, say to Cartesian |
368 products, direct sums or function spaces. Subsequently we lift |
365 products, direct sums or function spaces. Subsequently we lift |
369 \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.% |
366 \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.% |
370 \end{isamarkuptext}% |
367 \end{isamarkuptext}% |
371 \isamarkuptrue% |
368 \isamarkuptrue% |
372 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
369 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
373 \ \ 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}\isamarkupfalse% |
370 \ \ 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}\isamarkupfalse% |
374 % |
371 % |
375 \begin{isamarkuptext}% |
372 \begin{isamarkuptext}% |
376 It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a} |
373 It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a} |
377 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 to |
374 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 |
378 semigroups. This may be established formally as follows.% |
375 to semigroups. This may be established formally as follows.% |
379 \end{isamarkuptext}% |
376 \end{isamarkuptext}% |
380 \isamarkuptrue% |
377 \isamarkuptrue% |
381 \isacommand{instance}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline |
378 \isacommand{instance}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline |
382 \isamarkupfalse% |
379 \isamarkupfalse% |
383 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline |
380 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline |