11898
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Typedefs}%
|
17056
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
%
|
|
11 |
\endisatagtheory
|
|
12 |
{\isafoldtheory}%
|
|
13 |
%
|
|
14 |
\isadelimtheory
|
|
15 |
%
|
|
16 |
\endisadelimtheory
|
|
17 |
\isamarkuptrue%
|
11898
|
18 |
%
|
|
19 |
\isamarkupsection{Introducing New Types%
|
|
20 |
}
|
|
21 |
\isamarkuptrue%
|
|
22 |
%
|
|
23 |
\begin{isamarkuptext}%
|
|
24 |
\label{sec:adv-typedef}
|
|
25 |
For most applications, a combination of predefined types like \isa{bool} and
|
|
26 |
\isa{{\isasymRightarrow}} with recursive datatypes and records is quite sufficient. Very
|
|
27 |
occasionally you may feel the need for a more advanced type. If you
|
|
28 |
are certain that your type is not definable by any of the
|
|
29 |
standard means, then read on.
|
|
30 |
\begin{warn}
|
|
31 |
Types in HOL must be non-empty; otherwise the quantifier rules would be
|
|
32 |
unsound, because $\exists x.\ x=x$ is a theorem.
|
|
33 |
\end{warn}%
|
|
34 |
\end{isamarkuptext}%
|
|
35 |
\isamarkuptrue%
|
|
36 |
%
|
|
37 |
\isamarkupsubsection{Declaring New Types%
|
|
38 |
}
|
|
39 |
\isamarkuptrue%
|
|
40 |
%
|
|
41 |
\begin{isamarkuptext}%
|
|
42 |
\label{sec:typedecl}
|
|
43 |
\index{types!declaring|(}%
|
|
44 |
\index{typedecl@\isacommand {typedecl} (command)}%
|
|
45 |
The most trivial way of introducing a new type is by a \textbf{type
|
|
46 |
declaration}:%
|
|
47 |
\end{isamarkuptext}%
|
17056
|
48 |
\isamarkupfalse%
|
|
49 |
\isacommand{typedecl}\ my{\isacharunderscore}new{\isacharunderscore}type\isamarkuptrue%
|
11898
|
50 |
%
|
|
51 |
\begin{isamarkuptext}%
|
|
52 |
\noindent
|
|
53 |
This does not define \isa{my{\isacharunderscore}new{\isacharunderscore}type} at all but merely introduces its
|
|
54 |
name. Thus we know nothing about this type, except that it is
|
|
55 |
non-empty. Such declarations without definitions are
|
|
56 |
useful if that type can be viewed as a parameter of the theory.
|
|
57 |
A typical example is given in \S\ref{sec:VMC}, where we define a transition
|
|
58 |
relation over an arbitrary type of states.
|
|
59 |
|
|
60 |
In principle we can always get rid of such type declarations by making those
|
|
61 |
types parameters of every other type, thus keeping the theory generic. In
|
|
62 |
practice, however, the resulting clutter can make types hard to read.
|
|
63 |
|
|
64 |
If you are looking for a quick and dirty way of introducing a new type
|
|
65 |
together with its properties: declare the type and state its properties as
|
|
66 |
axioms. Example:%
|
|
67 |
\end{isamarkuptext}%
|
17056
|
68 |
\isamarkupfalse%
|
11898
|
69 |
\isacommand{axioms}\isanewline
|
17056
|
70 |
just{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isacharcolon}{\isacharcolon}my{\isacharunderscore}new{\isacharunderscore}type{\isachardot}\ {\isasymforall}y{\isachardot}\ x\ {\isacharequal}\ y{\isachardoublequote}\isamarkuptrue%
|
11898
|
71 |
%
|
|
72 |
\begin{isamarkuptext}%
|
|
73 |
\noindent
|
|
74 |
However, we strongly discourage this approach, except at explorative stages
|
|
75 |
of your development. It is extremely easy to write down contradictory sets of
|
|
76 |
axioms, in which case you will be able to prove everything but it will mean
|
|
77 |
nothing. In the example above, the axiomatic approach is
|
|
78 |
unnecessary: a one-element type called \isa{unit} is already defined in HOL.
|
|
79 |
\index{types!declaring|)}%
|
|
80 |
\end{isamarkuptext}%
|
|
81 |
\isamarkuptrue%
|
|
82 |
%
|
|
83 |
\isamarkupsubsection{Defining New Types%
|
|
84 |
}
|
|
85 |
\isamarkuptrue%
|
|
86 |
%
|
|
87 |
\begin{isamarkuptext}%
|
|
88 |
\label{sec:typedef}
|
|
89 |
\index{types!defining|(}%
|
|
90 |
\index{typedecl@\isacommand {typedef} (command)|(}%
|
|
91 |
Now we come to the most general means of safely introducing a new type, the
|
|
92 |
\textbf{type definition}. All other means, for example
|
|
93 |
\isacommand{datatype}, are based on it. The principle is extremely simple:
|
12334
|
94 |
any non-empty subset of an existing type can be turned into a new type.
|
|
95 |
More precisely, the new type is specified to be isomorphic to some
|
|
96 |
non-empty subset of an existing type.
|
11898
|
97 |
|
|
98 |
Let us work a simple example, the definition of a three-element type.
|
|
99 |
It is easily represented by the first three natural numbers:%
|
|
100 |
\end{isamarkuptext}%
|
17056
|
101 |
\isamarkupfalse%
|
|
102 |
\isacommand{typedef}\ three\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequote}%
|
|
103 |
\isadelimproof
|
|
104 |
%
|
|
105 |
\endisadelimproof
|
|
106 |
%
|
|
107 |
\isatagproof
|
11898
|
108 |
\isamarkuptrue%
|
16353
|
109 |
%
|
|
110 |
\begin{isamarkuptxt}%
|
|
111 |
\noindent
|
|
112 |
In order to enforce that the representing set on the right-hand side is
|
|
113 |
non-empty, this definition actually starts a proof to that effect:
|
|
114 |
\begin{isabelle}%
|
|
115 |
\ {\isadigit{1}}{\isachardot}\ {\isasymexists}x{\isachardot}\ x\ {\isasymin}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}%
|
|
116 |
\end{isabelle}
|
|
117 |
Fortunately, this is easy enough to show, even \isa{auto} could do it.
|
|
118 |
In general, one has to provide a witness, in our case 0:%
|
|
119 |
\end{isamarkuptxt}%
|
17056
|
120 |
\isamarkupfalse%
|
16353
|
121 |
\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isadigit{0}}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
|
11898
|
122 |
\isamarkupfalse%
|
17056
|
123 |
\isacommand{by}\ simp%
|
|
124 |
\endisatagproof
|
|
125 |
{\isafoldproof}%
|
|
126 |
%
|
|
127 |
\isadelimproof
|
|
128 |
%
|
|
129 |
\endisadelimproof
|
|
130 |
\isamarkuptrue%
|
11898
|
131 |
%
|
|
132 |
\begin{isamarkuptext}%
|
|
133 |
This type definition introduces the new type \isa{three} and asserts
|
12334
|
134 |
that it is a copy of the set \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. This assertion
|
11898
|
135 |
is expressed via a bijection between the \emph{type} \isa{three} and the
|
12334
|
136 |
\emph{set} \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. To this end, the command declares the following
|
11898
|
137 |
constants behind the scenes:
|
|
138 |
\begin{center}
|
|
139 |
\begin{tabular}{rcl}
|
|
140 |
\isa{three} &::& \isa{nat\ set} \\
|
|
141 |
\isa{Rep{\isacharunderscore}three} &::& \isa{three\ {\isasymRightarrow}\ nat}\\
|
|
142 |
\isa{Abs{\isacharunderscore}three} &::& \isa{nat\ {\isasymRightarrow}\ three}
|
|
143 |
\end{tabular}
|
|
144 |
\end{center}
|
|
145 |
where constant \isa{three} is explicitly defined as the representing set:
|
|
146 |
\begin{center}
|
12473
|
147 |
\isa{three\ {\isasymequiv}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}\hfill(\isa{three{\isacharunderscore}def})
|
11898
|
148 |
\end{center}
|
|
149 |
The situation is best summarized with the help of the following diagram,
|
12543
|
150 |
where squares denote types and the irregular region denotes a set:
|
11898
|
151 |
\begin{center}
|
12627
|
152 |
\includegraphics[scale=.8]{typedef}
|
11898
|
153 |
\end{center}
|
|
154 |
Finally, \isacommand{typedef} asserts that \isa{Rep{\isacharunderscore}three} is
|
|
155 |
surjective on the subset \isa{three} and \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three} are inverses of each other:
|
|
156 |
\begin{center}
|
|
157 |
\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
|
|
158 |
\isa{Rep{\isacharunderscore}three\ x\ {\isasymin}\ three} & (\isa{Rep{\isacharunderscore}three}) \\
|
|
159 |
\isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ x} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inverse}) \\
|
|
160 |
\isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse})
|
|
161 |
\end{tabular}
|
|
162 |
\end{center}
|
|
163 |
%
|
|
164 |
From this example it should be clear what \isacommand{typedef} does
|
|
165 |
in general given a name (here \isa{three}) and a set
|
12473
|
166 |
(here \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}).
|
11898
|
167 |
|
|
168 |
Our next step is to define the basic functions expected on the new type.
|
|
169 |
Although this depends on the type at hand, the following strategy works well:
|
|
170 |
\begin{itemize}
|
|
171 |
\item define a small kernel of basic functions that can express all other
|
|
172 |
functions you anticipate.
|
|
173 |
\item define the kernel in terms of corresponding functions on the
|
|
174 |
representing type using \isa{Abs} and \isa{Rep} to convert between the
|
|
175 |
two levels.
|
|
176 |
\end{itemize}
|
|
177 |
In our example it suffices to give the three elements of type \isa{three}
|
|
178 |
names:%
|
|
179 |
\end{isamarkuptext}%
|
17056
|
180 |
\isamarkupfalse%
|
11898
|
181 |
\isacommand{constdefs}\isanewline
|
|
182 |
\ \ A{\isacharcolon}{\isacharcolon}\ three\isanewline
|
|
183 |
\ {\isachardoublequote}A\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{0}}{\isachardoublequote}\isanewline
|
|
184 |
\ \ B{\isacharcolon}{\isacharcolon}\ three\isanewline
|
|
185 |
\ {\isachardoublequote}B\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{1}}{\isachardoublequote}\isanewline
|
|
186 |
\ \ C\ {\isacharcolon}{\isacharcolon}\ three\isanewline
|
17056
|
187 |
\ {\isachardoublequote}C\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{2}}{\isachardoublequote}\isamarkuptrue%
|
11898
|
188 |
%
|
|
189 |
\begin{isamarkuptext}%
|
|
190 |
So far, everything was easy. But it is clear that reasoning about \isa{three} will be hell if we have to go back to \isa{nat} every time. Thus our
|
|
191 |
aim must be to raise our level of abstraction by deriving enough theorems
|
|
192 |
about type \isa{three} to characterize it completely. And those theorems
|
|
193 |
should be phrased in terms of \isa{A}, \isa{B} and \isa{C}, not \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three}. Because of the simplicity of the example,
|
|
194 |
we merely need to prove that \isa{A}, \isa{B} and \isa{C} are distinct
|
|
195 |
and that they exhaust the type.
|
|
196 |
|
|
197 |
In processing our \isacommand{typedef} declaration,
|
12473
|
198 |
Isabelle proves several helpful lemmas. The first two
|
|
199 |
express injectivity of \isa{Rep{\isacharunderscore}three} and \isa{Abs{\isacharunderscore}three}:
|
11898
|
200 |
\begin{center}
|
12473
|
201 |
\begin{tabular}{@ {}r@ {\qquad}l@ {}}
|
|
202 |
\isa{{\isacharparenleft}Rep{\isacharunderscore}three\ x\ {\isacharequal}\ Rep{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inject}) \\
|
|
203 |
\begin{tabular}{@ {}l@ {}}
|
|
204 |
\isa{{\isasymlbrakk}x\ {\isasymin}\ three{\isacharsemicolon}\ y\ {\isasymin}\ three\ {\isasymrbrakk}} \\
|
|
205 |
\isa{{\isasymLongrightarrow}\ {\isacharparenleft}Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}}
|
|
206 |
\end{tabular} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inject}) \\
|
|
207 |
\end{tabular}
|
11898
|
208 |
\end{center}
|
12473
|
209 |
The following ones allow to replace some \isa{x{\isacharcolon}{\isacharcolon}three} by
|
|
210 |
\isa{Abs{\isacharunderscore}three{\isacharparenleft}y{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}, and conversely \isa{y} by \isa{Rep{\isacharunderscore}three\ x}:
|
11898
|
211 |
\begin{center}
|
12473
|
212 |
\begin{tabular}{@ {}r@ {\qquad}l@ {}}
|
|
213 |
\isa{{\isasymlbrakk}y\ {\isasymin}\ three{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ y\ {\isacharequal}\ Rep{\isacharunderscore}three\ x\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}cases}) \\
|
|
214 |
\isa{{\isacharparenleft}{\isasymAnd}y{\isachardot}\ {\isasymlbrakk}x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}cases}) \\
|
|
215 |
\isa{{\isasymlbrakk}y\ {\isasymin}\ three{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ P\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}induct}) \\
|
|
216 |
\isa{{\isacharparenleft}{\isasymAnd}y{\isachardot}\ y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P\ x} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}induct}) \\
|
|
217 |
\end{tabular}
|
11898
|
218 |
\end{center}
|
12473
|
219 |
These theorems are proved for any type definition, with \isa{three}
|
|
220 |
replaced by the name of the type in question.
|
|
221 |
|
11898
|
222 |
Distinctness of \isa{A}, \isa{B} and \isa{C} follows immediately
|
|
223 |
if we expand their definitions and rewrite with the injectivity
|
|
224 |
of \isa{Abs{\isacharunderscore}three}:%
|
|
225 |
\end{isamarkuptext}%
|
17056
|
226 |
\isamarkupfalse%
|
11898
|
227 |
\isacommand{lemma}\ {\isachardoublequote}A\ {\isasymnoteq}\ B\ {\isasymand}\ B\ {\isasymnoteq}\ A\ {\isasymand}\ A\ {\isasymnoteq}\ C\ {\isasymand}\ C\ {\isasymnoteq}\ A\ {\isasymand}\ B\ {\isasymnoteq}\ C\ {\isasymand}\ C\ {\isasymnoteq}\ B{\isachardoublequote}\isanewline
|
17056
|
228 |
%
|
|
229 |
\isadelimproof
|
|
230 |
%
|
|
231 |
\endisadelimproof
|
|
232 |
%
|
|
233 |
\isatagproof
|
11898
|
234 |
\isamarkupfalse%
|
17056
|
235 |
\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Abs{\isacharunderscore}three{\isacharunderscore}inject\ A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def\ three{\isacharunderscore}def{\isacharparenright}%
|
|
236 |
\endisatagproof
|
|
237 |
{\isafoldproof}%
|
|
238 |
%
|
|
239 |
\isadelimproof
|
|
240 |
%
|
|
241 |
\endisadelimproof
|
|
242 |
\isamarkuptrue%
|
11898
|
243 |
%
|
|
244 |
\begin{isamarkuptext}%
|
|
245 |
\noindent
|
12473
|
246 |
Of course we rely on the simplifier to solve goals like \isa{{\isadigit{0}}\ {\isasymnoteq}\ {\isadigit{1}}}.
|
11898
|
247 |
|
|
248 |
The fact that \isa{A}, \isa{B} and \isa{C} exhaust type \isa{three} is
|
|
249 |
best phrased as a case distinction theorem: if you want to prove \isa{P\ x}
|
|
250 |
(where \isa{x} is of type \isa{three}) it suffices to prove \isa{P\ A},
|
12473
|
251 |
\isa{P\ B} and \isa{P\ C}:%
|
11898
|
252 |
\end{isamarkuptext}%
|
17056
|
253 |
\isamarkupfalse%
|
|
254 |
\isacommand{lemma}\ three{\isacharunderscore}cases{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}%
|
|
255 |
\isadelimproof
|
|
256 |
%
|
|
257 |
\endisadelimproof
|
|
258 |
%
|
|
259 |
\isatagproof
|
11898
|
260 |
\isamarkuptrue%
|
16353
|
261 |
%
|
|
262 |
\begin{isamarkuptxt}%
|
|
263 |
\noindent Again this follows easily from a pre-proved general theorem:%
|
|
264 |
\end{isamarkuptxt}%
|
17056
|
265 |
\isamarkupfalse%
|
|
266 |
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ rule{\isacharcolon}\ Abs{\isacharunderscore}three{\isacharunderscore}induct{\isacharparenright}\isamarkuptrue%
|
16353
|
267 |
%
|
|
268 |
\begin{isamarkuptxt}%
|
|
269 |
\begin{isabelle}%
|
|
270 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}y{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}%
|
|
271 |
\end{isabelle}
|
|
272 |
Simplification with \isa{three{\isacharunderscore}def} leads to the disjunction \isa{y\ {\isacharequal}\ {\isadigit{0}}\ {\isasymor}\ y\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ y\ {\isacharequal}\ {\isadigit{2}}} which \isa{auto} separates into three
|
|
273 |
subgoals, each of which is easily solved by simplification:%
|
|
274 |
\end{isamarkuptxt}%
|
17056
|
275 |
\isamarkupfalse%
|
16353
|
276 |
\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ three{\isacharunderscore}def\ A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def{\isacharparenright}\isanewline
|
11898
|
277 |
\isamarkupfalse%
|
17056
|
278 |
\isacommand{done}%
|
|
279 |
\endisatagproof
|
|
280 |
{\isafoldproof}%
|
|
281 |
%
|
|
282 |
\isadelimproof
|
|
283 |
%
|
|
284 |
\endisadelimproof
|
|
285 |
\isamarkuptrue%
|
11898
|
286 |
%
|
|
287 |
\begin{isamarkuptext}%
|
|
288 |
\noindent
|
|
289 |
This concludes the derivation of the characteristic theorems for
|
|
290 |
type \isa{three}.
|
|
291 |
|
|
292 |
The attentive reader has realized long ago that the
|
|
293 |
above lengthy definition can be collapsed into one line:%
|
|
294 |
\end{isamarkuptext}%
|
17056
|
295 |
\isamarkupfalse%
|
|
296 |
\isacommand{datatype}\ better{\isacharunderscore}three\ {\isacharequal}\ A\ {\isacharbar}\ B\ {\isacharbar}\ C\isamarkuptrue%
|
11898
|
297 |
%
|
|
298 |
\begin{isamarkuptext}%
|
|
299 |
\noindent
|
|
300 |
In fact, the \isacommand{datatype} command performs internally more or less
|
|
301 |
the same derivations as we did, which gives you some idea what life would be
|
|
302 |
like without \isacommand{datatype}.
|
|
303 |
|
|
304 |
Although \isa{three} could be defined in one line, we have chosen this
|
|
305 |
example to demonstrate \isacommand{typedef} because its simplicity makes the
|
|
306 |
key concepts particularly easy to grasp. If you would like to see a
|
|
307 |
non-trivial example that cannot be defined more directly, we recommend the
|
12473
|
308 |
definition of \emph{finite multisets} in the Library~\cite{HOL-Library}.
|
11898
|
309 |
|
|
310 |
Let us conclude by summarizing the above procedure for defining a new type.
|
|
311 |
Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
|
|
312 |
set of functions $F$, this involves three steps:
|
|
313 |
\begin{enumerate}
|
|
314 |
\item Find an appropriate type $\tau$ and subset $A$ which has the desired
|
|
315 |
properties $P$, and make a type definition based on this representation.
|
|
316 |
\item Define the required functions $F$ on $ty$ by lifting
|
|
317 |
analogous functions on the representation via $Abs_ty$ and $Rep_ty$.
|
|
318 |
\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
|
|
319 |
\end{enumerate}
|
|
320 |
You can now forget about the representation and work solely in terms of the
|
|
321 |
abstract functions $F$ and properties $P$.%
|
|
322 |
\index{typedecl@\isacommand {typedef} (command)|)}%
|
|
323 |
\index{types!defining|)}%
|
|
324 |
\end{isamarkuptext}%
|
17056
|
325 |
%
|
|
326 |
\isadelimtheory
|
|
327 |
%
|
|
328 |
\endisadelimtheory
|
|
329 |
%
|
|
330 |
\isatagtheory
|
|
331 |
%
|
|
332 |
\endisatagtheory
|
|
333 |
{\isafoldtheory}%
|
|
334 |
%
|
|
335 |
\isadelimtheory
|
|
336 |
%
|
|
337 |
\endisadelimtheory
|
11898
|
338 |
\end{isabellebody}%
|
|
339 |
%%% Local Variables:
|
|
340 |
%%% mode: latex
|
|
341 |
%%% TeX-master: "root"
|
|
342 |
%%% End:
|