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