8890
|
1 |
\begin{isabelle}%
|
8903
|
2 |
%
|
|
3 |
\isamarkupheader{Basic group theory}
|
9519
|
4 |
\isacommand{theory}\ Group\ =\ Main:%
|
8903
|
5 |
\begin{isamarkuptext}%
|
8907
|
6 |
\medskip\noindent The meta-type system of Isabelle supports
|
8903
|
7 |
\emph{intersections} and \emph{inclusions} of type classes. These
|
|
8 |
directly correspond to intersections and inclusions of type
|
|
9 |
predicates in a purely set theoretic sense. This is sufficient as a
|
|
10 |
means to describe simple hierarchies of structures. As an
|
|
11 |
illustration, we use the well-known example of semigroups, monoids,
|
8907
|
12 |
general groups and Abelian groups.%
|
8903
|
13 |
\end{isamarkuptext}%
|
|
14 |
%
|
|
15 |
\isamarkupsubsection{Monoids and Groups}
|
|
16 |
%
|
|
17 |
\begin{isamarkuptext}%
|
|
18 |
First we declare some polymorphic constants required later for the
|
|
19 |
signature parts of our structures.%
|
|
20 |
\end{isamarkuptext}%
|
8890
|
21 |
\isacommand{consts}\isanewline
|
9665
|
22 |
\ \ times\ ::\ {\isachardoublequote}{\isacharprime}a\ ={\isachargreater}\ {\isacharprime}a\ ={\isachargreater}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ 70{\isacharparenright}\isanewline
|
|
23 |
\ \ inverse\ ::\ {\isachardoublequote}{\isacharprime}a\ ={\isachargreater}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}1000{\isacharbrackright}\ 999{\isacharparenright}\isanewline
|
|
24 |
\ \ one\ ::\ {\isacharprime}a\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}%
|
8903
|
25 |
\begin{isamarkuptext}%
|
|
26 |
\noindent Next we define class $monoid$ of monoids with operations
|
|
27 |
$\TIMES$ and $1$. Note that multiple class axioms are allowed for
|
|
28 |
user convenience --- they simply represent the conjunction of their
|
|
29 |
respective universal closures.%
|
|
30 |
\end{isamarkuptext}%
|
8890
|
31 |
\isacommand{axclass}\isanewline
|
9665
|
32 |
\ \ monoid\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
|
|
33 |
\ \ assoc:\ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
|
|
34 |
\ \ left{\isacharunderscore}unit:\ \ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{\isachardoublequote}\isanewline
|
|
35 |
\ \ right{\isacharunderscore}unit:\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{\isachardoublequote}%
|
8903
|
36 |
\begin{isamarkuptext}%
|
|
37 |
\noindent So class $monoid$ contains exactly those types $\tau$ where
|
|
38 |
$\TIMES :: \tau \To \tau \To \tau$ and $1 :: \tau$ are specified
|
|
39 |
appropriately, such that $\TIMES$ is associative and $1$ is a left
|
9519
|
40 |
and right unit element for the $\TIMES$ operation.%
|
8903
|
41 |
\end{isamarkuptext}%
|
|
42 |
%
|
|
43 |
\begin{isamarkuptext}%
|
|
44 |
\medskip Independently of $monoid$, we now define a linear hierarchy
|
8907
|
45 |
of semigroups, general groups and Abelian groups. Note that the
|
|
46 |
names of class axioms are automatically qualified with each class
|
|
47 |
name, so we may re-use common names such as $assoc$.%
|
8903
|
48 |
\end{isamarkuptext}%
|
8890
|
49 |
\isacommand{axclass}\isanewline
|
9665
|
50 |
\ \ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
|
|
51 |
\ \ assoc:\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
|
8890
|
52 |
\isanewline
|
|
53 |
\isacommand{axclass}\isanewline
|
9665
|
54 |
\ \ group\ {\isacharless}\ semigroup\isanewline
|
|
55 |
\ \ left{\isacharunderscore}unit:\ \ \ \ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{\isachardoublequote}\isanewline
|
|
56 |
\ \ left{\isacharunderscore}inverse:\ {\isachardoublequote}x{\isasyminv}\ {\isasymOtimes}\ x\ =\ {\isasymunit}{\isachardoublequote}\isanewline
|
8903
|
57 |
\isanewline
|
|
58 |
\isacommand{axclass}\isanewline
|
9665
|
59 |
\ \ agroup\ {\isacharless}\ group\isanewline
|
|
60 |
\ \ commute:\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ =\ y\ {\isasymOtimes}\ x{\isachardoublequote}%
|
8903
|
61 |
\begin{isamarkuptext}%
|
|
62 |
\noindent Class $group$ inherits associativity of $\TIMES$ from
|
8907
|
63 |
$semigroup$ and adds two further group axioms. Similarly, $agroup$
|
8903
|
64 |
is defined as the subset of $group$ such that for all of its elements
|
|
65 |
$\tau$, the operation $\TIMES :: \tau \To \tau \To \tau$ is even
|
|
66 |
commutative.%
|
|
67 |
\end{isamarkuptext}%
|
|
68 |
%
|
|
69 |
\isamarkupsubsection{Abstract reasoning}
|
|
70 |
%
|
8890
|
71 |
\begin{isamarkuptext}%
|
8903
|
72 |
In a sense, axiomatic type classes may be viewed as \emph{abstract
|
|
73 |
theories}. Above class definitions gives rise to abstract axioms
|
8907
|
74 |
$assoc$, $left_unit$, $left_inverse$, $commute$, where any of these
|
|
75 |
contain a type variable $\alpha :: c$ that is restricted to types of
|
8903
|
76 |
the corresponding class $c$. \emph{Sort constraints} like this
|
|
77 |
express a logical precondition for the whole formula. For example,
|
|
78 |
$assoc$ states that for all $\tau$, provided that $\tau ::
|
|
79 |
semigroup$, the operation $\TIMES :: \tau \To \tau \To \tau$ is
|
|
80 |
associative.
|
|
81 |
|
|
82 |
\medskip From a technical point of view, abstract axioms are just
|
|
83 |
ordinary Isabelle theorems, which may be used in proofs without
|
|
84 |
special treatment. Such ``abstract proofs'' usually yield new
|
|
85 |
``abstract theorems''. For example, we may now derive the following
|
8907
|
86 |
well-known laws of general groups.%
|
8890
|
87 |
\end{isamarkuptext}%
|
9665
|
88 |
\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse:\ {\isachardoublequote}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
|
|
89 |
\isacommand{proof}\ {\isacharminus}\isanewline
|
|
90 |
\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ {\isasymunit}\ {\isasymOtimes}\ {\isacharparenleft}x\ {\isasymOtimes}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
|
|
91 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline
|
|
92 |
\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
|
|
93 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline
|
|
94 |
\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
|
|
95 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline
|
|
96 |
\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isacharparenleft}x{\isasyminv}\ {\isasymOtimes}\ x{\isacharparenright}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
|
|
97 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline
|
|
98 |
\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
|
|
99 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline
|
|
100 |
\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isacharparenleft}{\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
|
|
101 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline
|
|
102 |
\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
|
|
103 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline
|
|
104 |
\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isasymunit}{\isachardoublequote}\isanewline
|
|
105 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline
|
9519
|
106 |
\ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline
|
8890
|
107 |
\isacommand{qed}%
|
|
108 |
\begin{isamarkuptext}%
|
8903
|
109 |
\noindent With $group_right_inverse$ already available,
|
8890
|
110 |
$group_right_unit$\label{thm:group-right-unit} is now established
|
|
111 |
much easier.%
|
|
112 |
\end{isamarkuptext}%
|
9665
|
113 |
\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit:\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
|
|
114 |
\isacommand{proof}\ {\isacharminus}\isanewline
|
|
115 |
\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}x{\isasyminv}\ {\isasymOtimes}\ x{\isacharparenright}{\isachardoublequote}\isanewline
|
|
116 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline
|
|
117 |
\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ x\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x{\isachardoublequote}\isanewline
|
|
118 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline
|
|
119 |
\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x{\isachardoublequote}\isanewline
|
|
120 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline
|
|
121 |
\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ x{\isachardoublequote}\isanewline
|
|
122 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline
|
9519
|
123 |
\ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline
|
8903
|
124 |
\isacommand{qed}%
|
|
125 |
\begin{isamarkuptext}%
|
|
126 |
\medskip Abstract theorems may be instantiated to only those types
|
|
127 |
$\tau$ where the appropriate class membership $\tau :: c$ is known at
|
|
128 |
Isabelle's type signature level. Since we have $agroup \subseteq
|
|
129 |
group \subseteq semigroup$ by definition, all theorems of $semigroup$
|
|
130 |
and $group$ are automatically inherited by $group$ and $agroup$.%
|
|
131 |
\end{isamarkuptext}%
|
|
132 |
%
|
|
133 |
\isamarkupsubsection{Abstract instantiation}
|
|
134 |
%
|
|
135 |
\begin{isamarkuptext}%
|
|
136 |
From the definition, the $monoid$ and $group$ classes have been
|
|
137 |
independent. Note that for monoids, $right_unit$ had to be included
|
|
138 |
as an axiom, but for groups both $right_unit$ and $right_inverse$ are
|
|
139 |
derivable from the other axioms. With $group_right_unit$ derived as
|
|
140 |
a theorem of group theory (see page~\pageref{thm:group-right-unit}),
|
8907
|
141 |
we may now instantiate $monoid \subseteq semigroup$ and $group
|
|
142 |
\subseteq monoid$ properly as follows
|
8903
|
143 |
(cf.\ \figref{fig:monoid-group}).
|
|
144 |
|
|
145 |
\begin{figure}[htbp]
|
|
146 |
\begin{center}
|
|
147 |
\small
|
|
148 |
\unitlength 0.6mm
|
|
149 |
\begin{picture}(65,90)(0,-10)
|
|
150 |
\put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
|
|
151 |
\put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
|
|
152 |
\put(15,5){\makebox(0,0){$agroup$}}
|
|
153 |
\put(15,25){\makebox(0,0){$group$}}
|
|
154 |
\put(15,45){\makebox(0,0){$semigroup$}}
|
|
155 |
\put(30,65){\makebox(0,0){$term$}} \put(50,45){\makebox(0,0){$monoid$}}
|
|
156 |
\end{picture}
|
|
157 |
\hspace{4em}
|
|
158 |
\begin{picture}(30,90)(0,0)
|
|
159 |
\put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
|
|
160 |
\put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
|
|
161 |
\put(15,5){\makebox(0,0){$agroup$}}
|
|
162 |
\put(15,25){\makebox(0,0){$group$}}
|
|
163 |
\put(15,45){\makebox(0,0){$monoid$}}
|
|
164 |
\put(15,65){\makebox(0,0){$semigroup$}}
|
|
165 |
\put(15,85){\makebox(0,0){$term$}}
|
|
166 |
\end{picture}
|
|
167 |
\caption{Monoids and groups: according to definition, and by proof}
|
|
168 |
\label{fig:monoid-group}
|
|
169 |
\end{center}
|
8907
|
170 |
\end{figure}%
|
8903
|
171 |
\end{isamarkuptext}%
|
9665
|
172 |
\isacommand{instance}\ monoid\ {\isacharless}\ semigroup\isanewline
|
|
173 |
\isacommand{proof}\ intro{\isacharunderscore}classes\isanewline
|
|
174 |
\ \ \isacommand{fix}\ x\ y\ z\ ::\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline
|
|
175 |
\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
|
|
176 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ monoid.assoc{\isacharparenright}\isanewline
|
8890
|
177 |
\isacommand{qed}\isanewline
|
|
178 |
\isanewline
|
9665
|
179 |
\isacommand{instance}\ group\ {\isacharless}\ monoid\isanewline
|
|
180 |
\isacommand{proof}\ intro{\isacharunderscore}classes\isanewline
|
|
181 |
\ \ \isacommand{fix}\ x\ y\ z\ ::\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline
|
|
182 |
\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
|
|
183 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ semigroup.assoc{\isacharparenright}\isanewline
|
|
184 |
\ \ \isacommand{show}\ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{\isachardoublequote}\isanewline
|
|
185 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline
|
|
186 |
\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{\isachardoublequote}\isanewline
|
|
187 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline
|
8903
|
188 |
\isacommand{qed}%
|
|
189 |
\begin{isamarkuptext}%
|
|
190 |
\medskip The $\isakeyword{instance}$ command sets up an appropriate
|
8907
|
191 |
goal that represents the class inclusion (or type arity, see
|
|
192 |
\secref{sec:inst-arity}) to be proven
|
8903
|
193 |
(see also \cite{isabelle-isar-ref}). The $intro_classes$ proof
|
|
194 |
method does back-chaining of class membership statements wrt.\ the
|
|
195 |
hierarchy of any classes defined in the current theory; the effect is
|
8907
|
196 |
to reduce to the initial statement to a number of goals that directly
|
|
197 |
correspond to any class axioms encountered on the path upwards
|
8922
|
198 |
through the class hierarchy.%
|
8903
|
199 |
\end{isamarkuptext}%
|
|
200 |
%
|
8907
|
201 |
\isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}}
|
8903
|
202 |
%
|
|
203 |
\begin{isamarkuptext}%
|
|
204 |
So far we have covered the case of the form
|
|
205 |
$\isakeyword{instance}~c@1 < c@2$, namely \emph{abstract
|
|
206 |
instantiation} --- $c@1$ is more special than $c@2$ and thus an
|
|
207 |
instance of $c@2$. Even more interesting for practical applications
|
|
208 |
are \emph{concrete instantiations} of axiomatic type classes. That
|
|
209 |
is, certain simple schemes $(\alpha@1, \ldots, \alpha@n)t :: c$ of
|
|
210 |
class membership may be established at the logical level and then
|
|
211 |
transferred to Isabelle's type signature level.
|
|
212 |
|
8907
|
213 |
\medskip As a typical example, we show that type $bool$ with
|
9519
|
214 |
exclusive-or as $\TIMES$ operation, identity as $\isasyminv$, and
|
8907
|
215 |
$False$ as $1$ forms an Abelian group.%
|
8903
|
216 |
\end{isamarkuptext}%
|
9665
|
217 |
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
|
|
218 |
\ \ times{\isacharunderscore}bool{\isacharunderscore}def:\ \ \ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline
|
|
219 |
\ \ inverse{\isacharunderscore}bool{\isacharunderscore}def:\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline
|
|
220 |
\ \ unit{\isacharunderscore}bool{\isacharunderscore}def:\ \ \ \ {\isachardoublequote}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}%
|
8903
|
221 |
\begin{isamarkuptext}%
|
|
222 |
\medskip It is important to note that above $\DEFS$ are just
|
8907
|
223 |
overloaded meta-level constant definitions, where type classes are
|
|
224 |
not yet involved at all. This form of constant definition with
|
|
225 |
overloading (and optional recursion over the syntactic structure of
|
|
226 |
simple types) are admissible as definitional extensions of plain HOL
|
|
227 |
\cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not
|
|
228 |
required for overloading. Nevertheless, overloaded definitions are
|
8903
|
229 |
best applied in the context of type classes.
|
|
230 |
|
|
231 |
\medskip Since we have chosen above $\DEFS$ of the generic group
|
|
232 |
operations on type $bool$ appropriately, the class membership $bool
|
|
233 |
:: agroup$ may be now derived as follows.%
|
|
234 |
\end{isamarkuptext}%
|
9519
|
235 |
\isacommand{instance}\ bool\ ::\ agroup\isanewline
|
9665
|
236 |
\isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes,\isanewline
|
|
237 |
\ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline
|
9519
|
238 |
\ \ \isacommand{fix}\ x\ y\ z\isanewline
|
9665
|
239 |
\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ =\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
|
|
240 |
\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ =\ x{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
|
|
241 |
\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ =\ False{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
|
|
242 |
\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ =\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
|
8903
|
243 |
\isacommand{qed}%
|
|
244 |
\begin{isamarkuptext}%
|
8907
|
245 |
The result of an $\isakeyword{instance}$ statement is both expressed
|
|
246 |
as a theorem of Isabelle's meta-logic, and as a type arity of the
|
|
247 |
type signature. The latter enables type-inference system to take
|
|
248 |
care of this new instance automatically.
|
8903
|
249 |
|
8907
|
250 |
\medskip We could now also instantiate our group theory classes to
|
|
251 |
many other concrete types. For example, $int :: agroup$ (e.g.\ by
|
|
252 |
defining $\TIMES$ as addition, $\isasyminv$ as negation and $1$ as
|
|
253 |
zero) or $list :: (term)semigroup$ (e.g.\ if $\TIMES$ is defined as
|
|
254 |
list append). Thus, the characteristic constants $\TIMES$,
|
|
255 |
$\isasyminv$, $1$ really become overloaded, i.e.\ have different
|
|
256 |
meanings on different types.%
|
8903
|
257 |
\end{isamarkuptext}%
|
|
258 |
%
|
|
259 |
\isamarkupsubsection{Lifting and Functors}
|
|
260 |
%
|
|
261 |
\begin{isamarkuptext}%
|
|
262 |
As already mentioned above, overloading in the simply-typed HOL
|
|
263 |
systems may include recursion over the syntactic structure of types.
|
|
264 |
That is, definitional equations $c^\tau \equiv t$ may also contain
|
|
265 |
constants of name $c$ on the right-hand side --- if these have types
|
|
266 |
that are structurally simpler than $\tau$.
|
|
267 |
|
|
268 |
This feature enables us to \emph{lift operations}, say to Cartesian
|
|
269 |
products, direct sums or function spaces. Subsequently we lift
|
8907
|
270 |
$\TIMES$ component-wise to binary products $\alpha \times \beta$.%
|
8903
|
271 |
\end{isamarkuptext}%
|
9665
|
272 |
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
|
|
273 |
\ \ times{\isacharunderscore}prod{\isacharunderscore}def:\ {\isachardoublequote}p\ {\isasymOtimes}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}{\isachardoublequote}%
|
8903
|
274 |
\begin{isamarkuptext}%
|
8907
|
275 |
It is very easy to see that associativity of $\TIMES^\alpha$ and
|
8903
|
276 |
$\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence
|
|
277 |
the binary type constructor $\times$ maps semigroups to semigroups.
|
|
278 |
This may be established formally as follows.%
|
|
279 |
\end{isamarkuptext}%
|
9665
|
280 |
\isacommand{instance}\ {\isacharasterisk}\ ::\ {\isacharparenleft}semigroup,\ semigroup{\isacharparenright}\ semigroup\isanewline
|
|
281 |
\isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes,\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline
|
|
282 |
\ \ \isacommand{fix}\ p\ q\ r\ ::\ {\isachardoublequote}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequote}\isanewline
|
9519
|
283 |
\ \ \isacommand{show}\isanewline
|
9665
|
284 |
\ \ \ \ {\isachardoublequote}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}\ {\isasymOtimes}\ fst\ r,\isanewline
|
|
285 |
\ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}\ {\isasymOtimes}\ snd\ r{\isacharparenright}\ =\isanewline
|
|
286 |
\ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ {\isacharparenleft}fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r{\isacharparenright},\isanewline
|
|
287 |
\ \ \ \ \ \ \ \ snd\ p\ {\isasymOtimes}\ snd\ {\isacharparenleft}fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
|
|
288 |
\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ add:\ semigroup.assoc{\isacharparenright}\isanewline
|
8903
|
289 |
\isacommand{qed}%
|
|
290 |
\begin{isamarkuptext}%
|
|
291 |
Thus, if we view class instances as ``structures'', then overloaded
|
8907
|
292 |
constant definitions with recursion over types indirectly provide
|
|
293 |
some kind of ``functors'' --- i.e.\ mappings between abstract
|
8903
|
294 |
theories.%
|
|
295 |
\end{isamarkuptext}%
|
8890
|
296 |
\isacommand{end}\end{isabelle}%
|
9145
|
297 |
%%% Local Variables:
|
|
298 |
%%% mode: latex
|
|
299 |
%%% TeX-master: "root"
|
|
300 |
%%% End:
|