|
haftmann@20967
|
1 |
%
|
|
haftmann@20967
|
2 |
\begin{isabellebody}%
|
|
haftmann@20967
|
3 |
\def\isabellecontext{Classes}%
|
|
haftmann@20967
|
4 |
%
|
|
haftmann@20967
|
5 |
\isadelimtheory
|
|
haftmann@20967
|
6 |
\isanewline
|
|
haftmann@20967
|
7 |
\isanewline
|
|
haftmann@20967
|
8 |
\isanewline
|
|
haftmann@20967
|
9 |
%
|
|
haftmann@20967
|
10 |
\endisadelimtheory
|
|
haftmann@20967
|
11 |
%
|
|
haftmann@20967
|
12 |
\isatagtheory
|
|
haftmann@20967
|
13 |
\isacommand{theory}\isamarkupfalse%
|
|
haftmann@20967
|
14 |
\ Classes\isanewline
|
|
haftmann@20967
|
15 |
\isakeyword{imports}\ Main\isanewline
|
|
haftmann@20967
|
16 |
\isakeyword{begin}\isanewline
|
|
haftmann@20967
|
17 |
%
|
|
haftmann@20967
|
18 |
\endisatagtheory
|
|
haftmann@20967
|
19 |
{\isafoldtheory}%
|
|
haftmann@20967
|
20 |
%
|
|
haftmann@20967
|
21 |
\isadelimtheory
|
|
haftmann@20967
|
22 |
%
|
|
haftmann@20967
|
23 |
\endisadelimtheory
|
|
haftmann@20967
|
24 |
%
|
|
haftmann@20967
|
25 |
\isadelimML
|
|
haftmann@20967
|
26 |
%
|
|
haftmann@20967
|
27 |
\endisadelimML
|
|
haftmann@20967
|
28 |
%
|
|
haftmann@20967
|
29 |
\isatagML
|
|
haftmann@20967
|
30 |
%
|
|
haftmann@20967
|
31 |
\endisatagML
|
|
haftmann@20967
|
32 |
{\isafoldML}%
|
|
haftmann@20967
|
33 |
%
|
|
haftmann@20967
|
34 |
\isadelimML
|
|
haftmann@20967
|
35 |
%
|
|
haftmann@20967
|
36 |
\endisadelimML
|
|
haftmann@20967
|
37 |
%
|
|
haftmann@20967
|
38 |
\isamarkupchapter{Haskell-style classes with Isabelle/Isar%
|
|
haftmann@20967
|
39 |
}
|
|
haftmann@20967
|
40 |
\isamarkuptrue%
|
|
haftmann@20967
|
41 |
%
|
|
haftmann@20967
|
42 |
\isamarkupsection{Introduction%
|
|
haftmann@20967
|
43 |
}
|
|
haftmann@20967
|
44 |
\isamarkuptrue%
|
|
haftmann@20967
|
45 |
%
|
|
haftmann@20967
|
46 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
47 |
The well-known concept of type classes
|
|
haftmann@20967
|
48 |
\cite{wadler89how,peterson93implementing,hall96type,Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}
|
|
haftmann@20967
|
49 |
offers a useful structuring mechanism for programs and proofs, which
|
|
haftmann@20967
|
50 |
is more light-weight than a fully featured module mechanism. Type
|
|
haftmann@20967
|
51 |
classes are able to qualify types by associating operations and
|
|
haftmann@20967
|
52 |
logical properties. For example, class \isa{eq} could provide
|
|
haftmann@20967
|
53 |
an equivalence relation \isa{{\isacharequal}} on type \isa{{\isasymalpha}}, and class
|
|
haftmann@20967
|
54 |
\isa{ord} could extend \isa{eq} by providing a strict order
|
|
haftmann@20967
|
55 |
\isa{{\isacharless}} etc.
|
|
haftmann@20967
|
56 |
|
|
haftmann@20967
|
57 |
Isabelle/Isar offers Haskell-style type classes, combining operational
|
|
haftmann@20967
|
58 |
and logical specifications.%
|
|
haftmann@20967
|
59 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
60 |
\isamarkuptrue%
|
|
haftmann@20967
|
61 |
%
|
|
haftmann@20967
|
62 |
\isamarkupsection{A simple algebra example \label{sec:example}%
|
|
haftmann@20967
|
63 |
}
|
|
haftmann@20967
|
64 |
\isamarkuptrue%
|
|
haftmann@20967
|
65 |
%
|
|
haftmann@20967
|
66 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
67 |
We demonstrate common elements of structured specifications and
|
|
haftmann@20967
|
68 |
abstract reasoning with type classes by the algebraic hierarchy of
|
|
haftmann@20967
|
69 |
semigroups, monoids and groups. Our background theory is that of
|
|
haftmann@20967
|
70 |
Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, which uses fairly
|
|
haftmann@20967
|
71 |
standard notation from mathematics and functional programming. We
|
|
haftmann@20967
|
72 |
also refer to basic vernacular commands for definitions and
|
|
haftmann@20967
|
73 |
statements, e.g.\ \isa{{\isasymDEFINITION}} and \isa{{\isasymLEMMA}};
|
|
haftmann@20967
|
74 |
proofs will be recorded using structured elements of Isabelle/Isar
|
|
haftmann@20967
|
75 |
\cite{Wenzel-PhD,Nipkow:2002}, notably \isa{{\isasymPROOF}}/\isa{{\isasymQED}} and \isa{{\isasymFIX}}/\isa{{\isasymASSUME}}/\isa{{\isasymSHOW}}.
|
|
haftmann@20967
|
76 |
|
|
haftmann@20967
|
77 |
Our main concern are the new \isa{{\isasymCLASS}}
|
|
haftmann@20967
|
78 |
and \isa{{\isasymINSTANCE}} elements used below.
|
|
haftmann@20967
|
79 |
Here we merely present the
|
|
haftmann@20967
|
80 |
look-and-feel for end users, which is quite similar to Haskell's
|
|
haftmann@20967
|
81 |
\texttt{class} and \texttt{instance} \cite{hall96type}, but
|
|
haftmann@20967
|
82 |
augmented by logical specifications and proofs;
|
|
haftmann@20967
|
83 |
Internally, those are mapped to more primitive Isabelle concepts.
|
|
haftmann@20967
|
84 |
See \cite{haftmann_wenzel2006classes} for more detail.%
|
|
haftmann@20967
|
85 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
86 |
\isamarkuptrue%
|
|
haftmann@20967
|
87 |
%
|
|
haftmann@20967
|
88 |
\isamarkupsubsection{Class definition%
|
|
haftmann@20967
|
89 |
}
|
|
haftmann@20967
|
90 |
\isamarkuptrue%
|
|
haftmann@20967
|
91 |
%
|
|
haftmann@20967
|
92 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
93 |
Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operation \isa{{\isasymcirc}} that is
|
|
haftmann@20967
|
94 |
assumed to be associative:%
|
|
haftmann@20967
|
95 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
96 |
\isamarkuptrue%
|
|
haftmann@20967
|
97 |
\ \ \ \ \isacommand{class}\isamarkupfalse%
|
|
haftmann@20967
|
98 |
\ semigroup\ {\isacharequal}\isanewline
|
|
haftmann@20967
|
99 |
\ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}\isactrlloc {\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
|
|
haftmann@20967
|
100 |
\ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}y\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
|
|
haftmann@20967
|
101 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
102 |
\noindent This \isa{{\isasymCLASS}} specification consists of two
|
|
haftmann@20967
|
103 |
parts: the \qn{operational} part names the class operation (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
|
|
haftmann@20967
|
104 |
(\isa{{\isasymASSUMES}}). The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global
|
|
haftmann@20967
|
105 |
operation \isa{{\isachardoublequote}mult\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isacharcolon}{\isacharcolon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
|
|
haftmann@20967
|
106 |
global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isasymalpha}{\isacharcolon}{\isacharcolon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
|
|
haftmann@20967
|
107 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
108 |
\isamarkuptrue%
|
|
haftmann@20967
|
109 |
%
|
|
haftmann@20967
|
110 |
\isamarkupsubsection{Class instantiation \label{sec:class_inst}%
|
|
haftmann@20967
|
111 |
}
|
|
haftmann@20967
|
112 |
\isamarkuptrue%
|
|
haftmann@20967
|
113 |
%
|
|
haftmann@20967
|
114 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
115 |
The concrete type \isa{int} is made a \isa{semigroup}
|
|
haftmann@20967
|
116 |
instance by providing a suitable definition for the class operation
|
|
haftmann@20967
|
117 |
\isa{mult} and a proof for the specification of \isa{assoc}.%
|
|
haftmann@20967
|
118 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
119 |
\isamarkuptrue%
|
|
haftmann@20967
|
120 |
\ \ \ \ \isacommand{instance}\isamarkupfalse%
|
|
haftmann@20967
|
121 |
\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
|
|
haftmann@20967
|
122 |
\ \ \ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isacharcolon}{\isacharcolon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
123 |
%
|
|
haftmann@20967
|
124 |
\isadelimproof
|
|
haftmann@20967
|
125 |
\ \ \ \ %
|
|
haftmann@20967
|
126 |
\endisadelimproof
|
|
haftmann@20967
|
127 |
%
|
|
haftmann@20967
|
128 |
\isatagproof
|
|
haftmann@20967
|
129 |
\isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
130 |
\isanewline
|
|
haftmann@20967
|
131 |
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
|
|
haftmann@20967
|
132 |
\ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
|
|
haftmann@20967
|
133 |
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
134 |
\ simp\isanewline
|
|
haftmann@20967
|
135 |
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
|
|
haftmann@20967
|
136 |
\ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
137 |
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
|
|
haftmann@20967
|
138 |
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
|
|
haftmann@20967
|
139 |
\isanewline
|
|
haftmann@20967
|
140 |
\ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
141 |
%
|
|
haftmann@20967
|
142 |
\endisatagproof
|
|
haftmann@20967
|
143 |
{\isafoldproof}%
|
|
haftmann@20967
|
144 |
%
|
|
haftmann@20967
|
145 |
\isadelimproof
|
|
haftmann@20967
|
146 |
%
|
|
haftmann@20967
|
147 |
\endisadelimproof
|
|
haftmann@20967
|
148 |
%
|
|
haftmann@20967
|
149 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
150 |
\noindent From now on, the type-checker will consider \isa{int}
|
|
haftmann@20967
|
151 |
as a \isa{semigroup} automatically, i.e.\ any general results
|
|
haftmann@20967
|
152 |
are immediately available on concrete instances.
|
|
haftmann@20967
|
153 |
|
|
haftmann@20967
|
154 |
Another instance of \isa{semigroup} are the natural numbers:%
|
|
haftmann@20967
|
155 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
156 |
\isamarkuptrue%
|
|
haftmann@20967
|
157 |
\ \ \ \ \isacommand{instance}\isamarkupfalse%
|
|
haftmann@20967
|
158 |
\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
|
|
haftmann@20967
|
159 |
\ \ \ \ \ \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
160 |
%
|
|
haftmann@20967
|
161 |
\isadelimproof
|
|
haftmann@20967
|
162 |
\ \ \ \ %
|
|
haftmann@20967
|
163 |
\endisadelimproof
|
|
haftmann@20967
|
164 |
%
|
|
haftmann@20967
|
165 |
\isatagproof
|
|
haftmann@20967
|
166 |
\isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
167 |
\isanewline
|
|
haftmann@20967
|
168 |
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
|
|
haftmann@20967
|
169 |
\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
|
|
haftmann@20967
|
170 |
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
171 |
\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
|
|
haftmann@20967
|
172 |
\ semigroup{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
173 |
\ simp\isanewline
|
|
haftmann@20967
|
174 |
\ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
175 |
%
|
|
haftmann@20967
|
176 |
\endisatagproof
|
|
haftmann@20967
|
177 |
{\isafoldproof}%
|
|
haftmann@20967
|
178 |
%
|
|
haftmann@20967
|
179 |
\isadelimproof
|
|
haftmann@20967
|
180 |
%
|
|
haftmann@20967
|
181 |
\endisadelimproof
|
|
haftmann@20967
|
182 |
%
|
|
haftmann@20967
|
183 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
184 |
Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as
|
|
haftmann@20967
|
185 |
operation:%
|
|
haftmann@20967
|
186 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
187 |
\isamarkuptrue%
|
|
haftmann@20967
|
188 |
\ \ \ \ \isacommand{instance}\isamarkupfalse%
|
|
haftmann@20967
|
189 |
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup\isanewline
|
|
haftmann@20967
|
190 |
\ \ \ \ \ \ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
191 |
%
|
|
haftmann@20967
|
192 |
\isadelimproof
|
|
haftmann@20967
|
193 |
\ \ \ \ %
|
|
haftmann@20967
|
194 |
\endisadelimproof
|
|
haftmann@20967
|
195 |
%
|
|
haftmann@20967
|
196 |
\isatagproof
|
|
haftmann@20967
|
197 |
\isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
198 |
\isanewline
|
|
haftmann@20967
|
199 |
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
|
|
haftmann@20967
|
200 |
\ xs\ ys\ zs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
201 |
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
202 |
\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymotimes}\ zs\ {\isacharequal}\ xs\ {\isasymotimes}\ {\isacharparenleft}ys\ {\isasymotimes}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
203 |
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
204 |
\ {\isacharminus}\isanewline
|
|
haftmann@20967
|
205 |
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
|
|
haftmann@20967
|
206 |
\ semigroup{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
|
|
haftmann@20967
|
207 |
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
|
|
haftmann@20967
|
208 |
\isanewline
|
|
haftmann@20967
|
209 |
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
|
|
haftmann@20967
|
210 |
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
211 |
\ simp\isanewline
|
|
haftmann@20967
|
212 |
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
213 |
\isanewline
|
|
haftmann@20967
|
214 |
\ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
215 |
%
|
|
haftmann@20967
|
216 |
\endisatagproof
|
|
haftmann@20967
|
217 |
{\isafoldproof}%
|
|
haftmann@20967
|
218 |
%
|
|
haftmann@20967
|
219 |
\isadelimproof
|
|
haftmann@20967
|
220 |
%
|
|
haftmann@20967
|
221 |
\endisadelimproof
|
|
haftmann@20967
|
222 |
%
|
|
haftmann@20967
|
223 |
\isamarkupsubsection{Subclasses%
|
|
haftmann@20967
|
224 |
}
|
|
haftmann@20967
|
225 |
\isamarkuptrue%
|
|
haftmann@20967
|
226 |
%
|
|
haftmann@20967
|
227 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
228 |
We define a subclass \isa{monoidl} (a semigroup with an left-hand neutral)
|
|
haftmann@20967
|
229 |
by extending \isa{semigroup}
|
|
haftmann@20967
|
230 |
with one additional operation \isa{neutral} together
|
|
haftmann@20967
|
231 |
with its property:%
|
|
haftmann@20967
|
232 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
233 |
\isamarkuptrue%
|
|
haftmann@20967
|
234 |
\ \ \ \ \isacommand{class}\isamarkupfalse%
|
|
haftmann@20967
|
235 |
\ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
|
|
haftmann@20967
|
236 |
\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}\isactrlloc {\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
|
|
haftmann@20967
|
237 |
\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}\isactrlloc {\isasymone}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
|
|
haftmann@20967
|
238 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
239 |
\noindent Again, we make some instances, by
|
|
haftmann@20967
|
240 |
providing suitable operation definitions and proofs for the
|
|
haftmann@20967
|
241 |
additional specifications.%
|
|
haftmann@20967
|
242 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
243 |
\isamarkuptrue%
|
|
haftmann@20967
|
244 |
\ \ \ \ \isacommand{instance}\isamarkupfalse%
|
|
haftmann@20967
|
245 |
\ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
|
|
haftmann@20967
|
246 |
\ \ \ \ \ \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
247 |
%
|
|
haftmann@20967
|
248 |
\isadelimproof
|
|
haftmann@20967
|
249 |
\ \ \ \ %
|
|
haftmann@20967
|
250 |
\endisadelimproof
|
|
haftmann@20967
|
251 |
%
|
|
haftmann@20967
|
252 |
\isatagproof
|
|
haftmann@20967
|
253 |
\isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
254 |
\isanewline
|
|
haftmann@20967
|
255 |
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
|
|
haftmann@20967
|
256 |
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
|
|
haftmann@20967
|
257 |
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
258 |
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
|
|
haftmann@20967
|
259 |
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
260 |
\ simp\isanewline
|
|
haftmann@20967
|
261 |
\ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
262 |
%
|
|
haftmann@20967
|
263 |
\endisatagproof
|
|
haftmann@20967
|
264 |
{\isafoldproof}%
|
|
haftmann@20967
|
265 |
%
|
|
haftmann@20967
|
266 |
\isadelimproof
|
|
haftmann@20967
|
267 |
\isanewline
|
|
haftmann@20967
|
268 |
%
|
|
haftmann@20967
|
269 |
\endisadelimproof
|
|
haftmann@20967
|
270 |
\isanewline
|
|
haftmann@20967
|
271 |
\ \ \ \ \isacommand{instance}\isamarkupfalse%
|
|
haftmann@20967
|
272 |
\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
|
|
haftmann@20967
|
273 |
\ \ \ \ \ \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
274 |
%
|
|
haftmann@20967
|
275 |
\isadelimproof
|
|
haftmann@20967
|
276 |
\ \ \ \ %
|
|
haftmann@20967
|
277 |
\endisadelimproof
|
|
haftmann@20967
|
278 |
%
|
|
haftmann@20967
|
279 |
\isatagproof
|
|
haftmann@20967
|
280 |
\isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
281 |
\isanewline
|
|
haftmann@20967
|
282 |
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
|
|
haftmann@20967
|
283 |
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
|
|
haftmann@20967
|
284 |
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
285 |
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
|
|
haftmann@20967
|
286 |
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
287 |
\ simp\isanewline
|
|
haftmann@20967
|
288 |
\ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
289 |
%
|
|
haftmann@20967
|
290 |
\endisatagproof
|
|
haftmann@20967
|
291 |
{\isafoldproof}%
|
|
haftmann@20967
|
292 |
%
|
|
haftmann@20967
|
293 |
\isadelimproof
|
|
haftmann@20967
|
294 |
\isanewline
|
|
haftmann@20967
|
295 |
%
|
|
haftmann@20967
|
296 |
\endisadelimproof
|
|
haftmann@20967
|
297 |
\isanewline
|
|
haftmann@20967
|
298 |
\ \ \ \ \isacommand{instance}\isamarkupfalse%
|
|
haftmann@20967
|
299 |
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoidl\isanewline
|
|
haftmann@20967
|
300 |
\ \ \ \ \ \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
301 |
%
|
|
haftmann@20967
|
302 |
\isadelimproof
|
|
haftmann@20967
|
303 |
\ \ \ \ %
|
|
haftmann@20967
|
304 |
\endisadelimproof
|
|
haftmann@20967
|
305 |
%
|
|
haftmann@20967
|
306 |
\isatagproof
|
|
haftmann@20967
|
307 |
\isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
308 |
\isanewline
|
|
haftmann@20967
|
309 |
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
|
|
haftmann@20967
|
310 |
\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
311 |
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
312 |
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ xs\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
313 |
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
314 |
\ {\isacharminus}\isanewline
|
|
haftmann@20967
|
315 |
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
|
|
haftmann@20967
|
316 |
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
|
|
haftmann@20967
|
317 |
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isacharprime}a\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
|
|
haftmann@20967
|
318 |
\isanewline
|
|
haftmann@20967
|
319 |
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
|
|
haftmann@20967
|
320 |
\ \isacommand{from}\isamarkupfalse%
|
|
haftmann@20967
|
321 |
\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
|
|
haftmann@20967
|
322 |
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
323 |
\ simp\isanewline
|
|
haftmann@20967
|
324 |
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
|
|
haftmann@20967
|
325 |
\ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
326 |
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
327 |
\ simp\isanewline
|
|
haftmann@20967
|
328 |
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
329 |
\isanewline
|
|
haftmann@20967
|
330 |
\ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
331 |
%
|
|
haftmann@20967
|
332 |
\endisatagproof
|
|
haftmann@20967
|
333 |
{\isafoldproof}%
|
|
haftmann@20967
|
334 |
%
|
|
haftmann@20967
|
335 |
\isadelimproof
|
|
haftmann@20967
|
336 |
%
|
|
haftmann@20967
|
337 |
\endisadelimproof
|
|
haftmann@20967
|
338 |
%
|
|
haftmann@20967
|
339 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
340 |
To finish our small algebra example, we add \isa{monoid}
|
|
haftmann@20967
|
341 |
and \isa{group} classes with corresponding instances%
|
|
haftmann@20967
|
342 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
343 |
\isamarkuptrue%
|
|
haftmann@20967
|
344 |
\ \ \ \ \isacommand{class}\isamarkupfalse%
|
|
haftmann@20967
|
345 |
\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
|
|
haftmann@20967
|
346 |
\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
347 |
\isanewline
|
|
haftmann@20967
|
348 |
\ \ \ \ \isacommand{instance}\isamarkupfalse%
|
|
haftmann@20967
|
349 |
\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
|
|
haftmann@20967
|
350 |
%
|
|
haftmann@20967
|
351 |
\isadelimproof
|
|
haftmann@20967
|
352 |
\ \ \ \ %
|
|
haftmann@20967
|
353 |
\endisadelimproof
|
|
haftmann@20967
|
354 |
%
|
|
haftmann@20967
|
355 |
\isatagproof
|
|
haftmann@20967
|
356 |
\isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
357 |
\isanewline
|
|
haftmann@20967
|
358 |
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
|
|
haftmann@20967
|
359 |
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
|
|
haftmann@20967
|
360 |
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
361 |
\ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
|
|
haftmann@20967
|
362 |
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
363 |
\ simp\isanewline
|
|
haftmann@20967
|
364 |
\ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
365 |
%
|
|
haftmann@20967
|
366 |
\endisatagproof
|
|
haftmann@20967
|
367 |
{\isafoldproof}%
|
|
haftmann@20967
|
368 |
%
|
|
haftmann@20967
|
369 |
\isadelimproof
|
|
haftmann@20967
|
370 |
\isanewline
|
|
haftmann@20967
|
371 |
%
|
|
haftmann@20967
|
372 |
\endisadelimproof
|
|
haftmann@20967
|
373 |
\isanewline
|
|
haftmann@20967
|
374 |
\ \ \ \ \isacommand{instance}\isamarkupfalse%
|
|
haftmann@20967
|
375 |
\ int\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
|
|
haftmann@20967
|
376 |
%
|
|
haftmann@20967
|
377 |
\isadelimproof
|
|
haftmann@20967
|
378 |
\ \ \ \ %
|
|
haftmann@20967
|
379 |
\endisadelimproof
|
|
haftmann@20967
|
380 |
%
|
|
haftmann@20967
|
381 |
\isatagproof
|
|
haftmann@20967
|
382 |
\isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
383 |
\isanewline
|
|
haftmann@20967
|
384 |
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
|
|
haftmann@20967
|
385 |
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
|
|
haftmann@20967
|
386 |
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
387 |
\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
|
|
haftmann@20967
|
388 |
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
389 |
\ simp\isanewline
|
|
haftmann@20967
|
390 |
\ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
391 |
%
|
|
haftmann@20967
|
392 |
\endisatagproof
|
|
haftmann@20967
|
393 |
{\isafoldproof}%
|
|
haftmann@20967
|
394 |
%
|
|
haftmann@20967
|
395 |
\isadelimproof
|
|
haftmann@20967
|
396 |
\isanewline
|
|
haftmann@20967
|
397 |
%
|
|
haftmann@20967
|
398 |
\endisadelimproof
|
|
haftmann@20967
|
399 |
\isanewline
|
|
haftmann@20967
|
400 |
\ \ \ \ \isacommand{instance}\isamarkupfalse%
|
|
haftmann@20967
|
401 |
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoid\isanewline
|
|
haftmann@20967
|
402 |
%
|
|
haftmann@20967
|
403 |
\isadelimproof
|
|
haftmann@20967
|
404 |
\ \ \ \ %
|
|
haftmann@20967
|
405 |
\endisadelimproof
|
|
haftmann@20967
|
406 |
%
|
|
haftmann@20967
|
407 |
\isatagproof
|
|
haftmann@20967
|
408 |
\isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
409 |
\isanewline
|
|
haftmann@20967
|
410 |
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
|
|
haftmann@20967
|
411 |
\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
412 |
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
413 |
\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
414 |
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
415 |
\ {\isacharminus}\isanewline
|
|
haftmann@20967
|
416 |
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
|
|
haftmann@20967
|
417 |
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
|
|
haftmann@20967
|
418 |
\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
|
|
haftmann@20967
|
419 |
\isanewline
|
|
haftmann@20967
|
420 |
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
|
|
haftmann@20967
|
421 |
\ \isacommand{from}\isamarkupfalse%
|
|
haftmann@20967
|
422 |
\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
|
|
haftmann@20967
|
423 |
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isacharprime}a\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
424 |
\ simp\isanewline
|
|
haftmann@20967
|
425 |
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
|
|
haftmann@20967
|
426 |
\ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
427 |
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
428 |
\ simp\isanewline
|
|
haftmann@20967
|
429 |
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
430 |
\isanewline
|
|
haftmann@20967
|
431 |
\ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
432 |
%
|
|
haftmann@20967
|
433 |
\endisatagproof
|
|
haftmann@20967
|
434 |
{\isafoldproof}%
|
|
haftmann@20967
|
435 |
%
|
|
haftmann@20967
|
436 |
\isadelimproof
|
|
haftmann@20967
|
437 |
\ \ \isanewline
|
|
haftmann@20967
|
438 |
%
|
|
haftmann@20967
|
439 |
\endisadelimproof
|
|
haftmann@20967
|
440 |
\isanewline
|
|
haftmann@20967
|
441 |
\ \ \ \ \isacommand{class}\isamarkupfalse%
|
|
haftmann@20967
|
442 |
\ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
|
|
haftmann@20967
|
443 |
\ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}\isactrlloc {\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
|
|
haftmann@20967
|
444 |
\ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
445 |
\isanewline
|
|
haftmann@20967
|
446 |
\ \ \ \ \isacommand{instance}\isamarkupfalse%
|
|
haftmann@20967
|
447 |
\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
|
|
haftmann@20967
|
448 |
\ \ \ \ \ \ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
449 |
%
|
|
haftmann@20967
|
450 |
\isadelimproof
|
|
haftmann@20967
|
451 |
\ \ \ \ %
|
|
haftmann@20967
|
452 |
\endisadelimproof
|
|
haftmann@20967
|
453 |
%
|
|
haftmann@20967
|
454 |
\isatagproof
|
|
haftmann@20967
|
455 |
\isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
456 |
\isanewline
|
|
haftmann@20967
|
457 |
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
|
|
haftmann@20967
|
458 |
\ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline
|
|
haftmann@20967
|
459 |
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
|
|
haftmann@20967
|
460 |
\ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
461 |
\ simp\isanewline
|
|
haftmann@20967
|
462 |
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
|
|
haftmann@20967
|
463 |
\ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
464 |
\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
|
|
haftmann@20967
|
465 |
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ neutral{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
|
|
haftmann@20967
|
466 |
\isanewline
|
|
haftmann@20967
|
467 |
\ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
468 |
%
|
|
haftmann@20967
|
469 |
\endisatagproof
|
|
haftmann@20967
|
470 |
{\isafoldproof}%
|
|
haftmann@20967
|
471 |
%
|
|
haftmann@20967
|
472 |
\isadelimproof
|
|
haftmann@20967
|
473 |
%
|
|
haftmann@20967
|
474 |
\endisadelimproof
|
|
haftmann@20967
|
475 |
%
|
|
haftmann@20967
|
476 |
\isamarkupsubsection{Abstract reasoning%
|
|
haftmann@20967
|
477 |
}
|
|
haftmann@20967
|
478 |
\isamarkuptrue%
|
|
haftmann@20967
|
479 |
%
|
|
haftmann@20967
|
480 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
481 |
Abstract theories enable reasoning at a general level, while results
|
|
haftmann@20967
|
482 |
are implicitly transferred to all instances. For example, we can
|
|
haftmann@20967
|
483 |
now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
|
|
haftmann@20967
|
484 |
states that the function \isa{{\isacharparenleft}x\ {\isasymcirc}{\isacharparenright}} is injective:%
|
|
haftmann@20967
|
485 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
486 |
\isamarkuptrue%
|
|
haftmann@20967
|
487 |
\ \ \ \ \isacommand{lemma}\isamarkupfalse%
|
|
haftmann@20967
|
488 |
\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
489 |
%
|
|
haftmann@20967
|
490 |
\isadelimproof
|
|
haftmann@20967
|
491 |
\ \ \ \ %
|
|
haftmann@20967
|
492 |
\endisadelimproof
|
|
haftmann@20967
|
493 |
%
|
|
haftmann@20967
|
494 |
\isatagproof
|
|
haftmann@20967
|
495 |
\isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
496 |
\isanewline
|
|
haftmann@20967
|
497 |
\ \ \ \ \isacommand{assume}\isamarkupfalse%
|
|
haftmann@20967
|
498 |
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
499 |
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
|
|
haftmann@20967
|
500 |
\ \isacommand{have}\isamarkupfalse%
|
|
haftmann@20967
|
501 |
\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
502 |
\ simp\isanewline
|
|
haftmann@20967
|
503 |
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
|
|
haftmann@20967
|
504 |
\ \isacommand{have}\isamarkupfalse%
|
|
haftmann@20967
|
505 |
\ {\isachardoublequoteopen}{\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
|
|
haftmann@20967
|
506 |
\ assoc\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
507 |
\ simp\isanewline
|
|
haftmann@20967
|
508 |
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
|
|
haftmann@20967
|
509 |
\ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
510 |
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
|
|
haftmann@20967
|
511 |
\ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
512 |
\ simp\isanewline
|
|
haftmann@20967
|
513 |
\ \ \ \ \isacommand{next}\isamarkupfalse%
|
|
haftmann@20967
|
514 |
\isanewline
|
|
haftmann@20967
|
515 |
\ \ \ \ \isacommand{assume}\isamarkupfalse%
|
|
haftmann@20967
|
516 |
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
517 |
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
|
|
haftmann@20967
|
518 |
\ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
519 |
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
520 |
\ simp\isanewline
|
|
haftmann@20967
|
521 |
\ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
522 |
%
|
|
haftmann@20967
|
523 |
\endisatagproof
|
|
haftmann@20967
|
524 |
{\isafoldproof}%
|
|
haftmann@20967
|
525 |
%
|
|
haftmann@20967
|
526 |
\isadelimproof
|
|
haftmann@20967
|
527 |
%
|
|
haftmann@20967
|
528 |
\endisadelimproof
|
|
haftmann@20967
|
529 |
%
|
|
haftmann@20967
|
530 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
531 |
\noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification
|
|
haftmann@20967
|
532 |
indicates that the result is recorded within that context for later
|
|
haftmann@20967
|
533 |
use. This local theorem is also lifted to the global one \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isasymalpha}{\isacharcolon}{\isacharcolon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been made an instance of
|
|
haftmann@20967
|
534 |
\isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
|
|
haftmann@20967
|
535 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
536 |
\isamarkuptrue%
|
|
haftmann@20967
|
537 |
%
|
|
haftmann@20967
|
538 |
\isamarkupsubsection{Additional subclass relations%
|
|
haftmann@20967
|
539 |
}
|
|
haftmann@20967
|
540 |
\isamarkuptrue%
|
|
haftmann@20967
|
541 |
%
|
|
haftmann@20967
|
542 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
543 |
Any \isa{group} is also a \isa{monoid}; this
|
|
haftmann@20967
|
544 |
can be made explicit by claiming an additional subclass relation,
|
|
haftmann@20967
|
545 |
together with a proof of the logical difference:%
|
|
haftmann@20967
|
546 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
547 |
\isamarkuptrue%
|
|
haftmann@20967
|
548 |
\ \ \ \ \isacommand{instance}\isamarkupfalse%
|
|
haftmann@20967
|
549 |
\ group\ {\isacharless}\ monoid\isanewline
|
|
haftmann@20967
|
550 |
%
|
|
haftmann@20967
|
551 |
\isadelimproof
|
|
haftmann@20967
|
552 |
\ \ \ \ %
|
|
haftmann@20967
|
553 |
\endisadelimproof
|
|
haftmann@20967
|
554 |
%
|
|
haftmann@20967
|
555 |
\isatagproof
|
|
haftmann@20967
|
556 |
\isacommand{proof}\isamarkupfalse%
|
|
haftmann@20967
|
557 |
\ {\isacharminus}\isanewline
|
|
haftmann@20967
|
558 |
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
|
|
haftmann@20967
|
559 |
\ x\isanewline
|
|
haftmann@20967
|
560 |
\ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
|
|
haftmann@20967
|
561 |
\ invl\ \isacommand{have}\isamarkupfalse%
|
|
haftmann@20967
|
562 |
\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
563 |
\ simp\isanewline
|
|
haftmann@20967
|
564 |
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
|
|
haftmann@20967
|
565 |
\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
|
|
haftmann@20967
|
566 |
\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
567 |
\ simp\isanewline
|
|
haftmann@20967
|
568 |
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
|
|
haftmann@20967
|
569 |
\ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
|
|
haftmann@20967
|
570 |
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
571 |
\ simp\isanewline
|
|
haftmann@20967
|
572 |
\ \ \ \ \isacommand{qed}\isamarkupfalse%
|
|
haftmann@20967
|
573 |
%
|
|
haftmann@20967
|
574 |
\endisatagproof
|
|
haftmann@20967
|
575 |
{\isafoldproof}%
|
|
haftmann@20967
|
576 |
%
|
|
haftmann@20967
|
577 |
\isadelimproof
|
|
haftmann@20967
|
578 |
%
|
|
haftmann@20967
|
579 |
\endisadelimproof
|
|
haftmann@20967
|
580 |
%
|
|
haftmann@20967
|
581 |
\isamarkupsection{Code generation%
|
|
haftmann@20967
|
582 |
}
|
|
haftmann@20967
|
583 |
\isamarkuptrue%
|
|
haftmann@20967
|
584 |
%
|
|
haftmann@20967
|
585 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
586 |
Code generation takes account of type classes,
|
|
haftmann@20967
|
587 |
resulting either in Haskell type classes or SML dictionaries.
|
|
haftmann@20967
|
588 |
As example, we define the natural power function on groups:%
|
|
haftmann@20967
|
589 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
590 |
\isamarkuptrue%
|
|
haftmann@20967
|
591 |
\ \ \ \ \isacommand{function}\isamarkupfalse%
|
|
haftmann@20967
|
592 |
\isanewline
|
|
haftmann@20967
|
593 |
\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
|
|
haftmann@20967
|
594 |
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
595 |
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
596 |
%
|
|
haftmann@20967
|
597 |
\isadelimproof
|
|
haftmann@20967
|
598 |
\ \ \ \ \ \ %
|
|
haftmann@20967
|
599 |
\endisadelimproof
|
|
haftmann@20967
|
600 |
%
|
|
haftmann@20967
|
601 |
\isatagproof
|
|
haftmann@20967
|
602 |
\isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
603 |
\ pat{\isacharunderscore}completeness\ auto%
|
|
haftmann@20967
|
604 |
\endisatagproof
|
|
haftmann@20967
|
605 |
{\isafoldproof}%
|
|
haftmann@20967
|
606 |
%
|
|
haftmann@20967
|
607 |
\isadelimproof
|
|
haftmann@20967
|
608 |
\isanewline
|
|
haftmann@20967
|
609 |
%
|
|
haftmann@20967
|
610 |
\endisadelimproof
|
|
haftmann@20967
|
611 |
\ \ \ \ \isacommand{termination}\isamarkupfalse%
|
|
haftmann@20967
|
612 |
\ pow{\isacharunderscore}nat%
|
|
haftmann@20967
|
613 |
\isadelimproof
|
|
haftmann@20967
|
614 |
\ %
|
|
haftmann@20967
|
615 |
\endisadelimproof
|
|
haftmann@20967
|
616 |
%
|
|
haftmann@20967
|
617 |
\isatagproof
|
|
haftmann@20967
|
618 |
\isacommand{by}\isamarkupfalse%
|
|
haftmann@20967
|
619 |
\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ fst{\isachardoublequoteclose}{\isacharparenright}%
|
|
haftmann@20967
|
620 |
\endisatagproof
|
|
haftmann@20967
|
621 |
{\isafoldproof}%
|
|
haftmann@20967
|
622 |
%
|
|
haftmann@20967
|
623 |
\isadelimproof
|
|
haftmann@20967
|
624 |
%
|
|
haftmann@20967
|
625 |
\endisadelimproof
|
|
haftmann@20967
|
626 |
\isanewline
|
|
haftmann@20967
|
627 |
\ \ \ \ \isacommand{declare}\isamarkupfalse%
|
|
haftmann@20967
|
628 |
\ pow{\isacharunderscore}nat{\isachardot}simps\ {\isacharbrackleft}code\ func{\isacharbrackright}\isanewline
|
|
haftmann@20967
|
629 |
\isanewline
|
|
haftmann@20967
|
630 |
\ \ \ \ \isacommand{definition}\isamarkupfalse%
|
|
haftmann@20967
|
631 |
\isanewline
|
|
haftmann@20967
|
632 |
\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
633 |
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
|
|
haftmann@20967
|
634 |
\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
|
|
haftmann@20967
|
635 |
\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
|
haftmann@20967
|
636 |
\isanewline
|
|
haftmann@20967
|
637 |
\ \ \ \ \isacommand{definition}\isamarkupfalse%
|
|
haftmann@20967
|
638 |
\isanewline
|
|
haftmann@20967
|
639 |
\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\isanewline
|
|
haftmann@20967
|
640 |
\ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
|
|
haftmann@20967
|
641 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
642 |
\noindent Now we generate and compile code for SML:%
|
|
haftmann@20967
|
643 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
644 |
\isamarkuptrue%
|
|
haftmann@20967
|
645 |
\ \ \ \ \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
|
|
haftmann@20967
|
646 |
\ example\ {\isacharparenleft}SML\ {\isacharminus}{\isacharparenright}%
|
|
haftmann@20967
|
647 |
\begin{isamarkuptext}%
|
|
haftmann@20967
|
648 |
\noindent The result is as expected:%
|
|
haftmann@20967
|
649 |
\end{isamarkuptext}%
|
|
haftmann@20967
|
650 |
\isamarkuptrue%
|
|
haftmann@20967
|
651 |
%
|
|
haftmann@20967
|
652 |
\isadelimML
|
|
haftmann@20967
|
653 |
\ \ \ \ %
|
|
haftmann@20967
|
654 |
\endisadelimML
|
|
haftmann@20967
|
655 |
%
|
|
haftmann@20967
|
656 |
\isatagML
|
|
haftmann@20967
|
657 |
\isacommand{ML}\isamarkupfalse%
|
|
haftmann@20967
|
658 |
\ {\isacharverbatimopen}\isanewline
|
|
haftmann@20967
|
659 |
\ \ \ \ \ \ if\ ROOT{\isachardot}Classes{\isachardot}example\ {\isacharequal}\ {\isachartilde}{\isadigit{2}}{\isadigit{0}}\ then\ {\isacharparenleft}{\isacharparenright}\ else\ error\ {\isachardoublequote}Wrong\ result{\isachardoublequote}\isanewline
|
|
haftmann@20967
|
660 |
\ \ \ \ {\isacharverbatimclose}%
|
|
haftmann@20967
|
661 |
\endisatagML
|
|
haftmann@20967
|
662 |
{\isafoldML}%
|
|
haftmann@20967
|
663 |
%
|
|
haftmann@20967
|
664 |
\isadelimML
|
|
haftmann@20967
|
665 |
%
|
|
haftmann@20967
|
666 |
\endisadelimML
|
|
haftmann@20967
|
667 |
\isanewline
|
|
haftmann@20967
|
668 |
%
|
|
haftmann@20967
|
669 |
\isadelimtheory
|
|
haftmann@20967
|
670 |
\isanewline
|
|
haftmann@20967
|
671 |
%
|
|
haftmann@20967
|
672 |
\endisadelimtheory
|
|
haftmann@20967
|
673 |
%
|
|
haftmann@20967
|
674 |
\isatagtheory
|
|
haftmann@20967
|
675 |
\isacommand{end}\isamarkupfalse%
|
|
haftmann@20967
|
676 |
%
|
|
haftmann@20967
|
677 |
\endisatagtheory
|
|
haftmann@20967
|
678 |
{\isafoldtheory}%
|
|
haftmann@20967
|
679 |
%
|
|
haftmann@20967
|
680 |
\isadelimtheory
|
|
haftmann@20967
|
681 |
%
|
|
haftmann@20967
|
682 |
\endisadelimtheory
|
|
haftmann@20967
|
683 |
\isanewline
|
|
haftmann@20967
|
684 |
\end{isabellebody}%
|
|
haftmann@20967
|
685 |
%%% Local Variables:
|
|
haftmann@20967
|
686 |
%%% mode: latex
|
|
haftmann@20967
|
687 |
%%% TeX-master: "root"
|
|
haftmann@20967
|
688 |
%%% End:
|