3 \def\isabellecontext{Typedef}%
5 \isamarkupsection{Introducing new types%
9 \label{sec:adv-typedef}
10 By now we have seen a number of ways for introducing new types, for example
11 type synonyms, recursive datatypes and records. For most applications, this
12 repertoire should be quite sufficient. Very occasionally you may feel the
13 need for a more advanced type. If you cannot avoid that type, and you are
14 quite certain that it is not definable by any of the standard means,
17 Types in HOL must be non-empty; otherwise the quantifier rules would be
18 unsound, because $\exists x.\ x=x$ is a theorem.
22 \isamarkupsubsection{Declaring new types%
25 \begin{isamarkuptext}%
27 The most trivial way of introducing a new type is by a \bfindex{type
30 \isacommand{typedecl}\ my{\isacharunderscore}new{\isacharunderscore}type%
31 \begin{isamarkuptext}%
32 \noindent\indexbold{*typedecl}%
33 This does not define \isa{my{\isacharunderscore}new{\isacharunderscore}type} at all but merely introduces its
34 name. Thus we know nothing about this type, except that it is
35 non-empty. Such declarations without definitions are
36 useful only if that type can be viewed as a parameter of a theory and we do
37 not intend to impose any restrictions on it. A typical example is given in
38 \S\ref{sec:VMC}, where we define transition relations over an arbitrary type
39 of states without any internal structure.
41 In principle we can always get rid of such type declarations by making those
42 types parameters of every other type, thus keeping the theory generic. In
43 practice, however, the resulting clutter can sometimes make types hard to
46 If you are looking for a quick and dirty way of introducing a new type
47 together with its properties: declare the type and state its properties as
50 \isacommand{axioms}\isanewline
51 just{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isacharcolon}{\isacharcolon}my{\isacharunderscore}new{\isacharunderscore}type{\isachardot}\ {\isasymforall}y{\isachardot}\ x\ {\isacharequal}\ y{\isachardoublequote}%
52 \begin{isamarkuptext}%
54 However, we strongly discourage this approach, except at explorative stages
55 of your development. It is extremely easy to write down contradictory sets of
56 axioms, in which case you will be able to prove everything but it will mean
57 nothing. In the above case it also turns out that the axiomatic approach is
58 unnecessary: a one-element type called \isa{unit} is already defined in HOL.%
61 \isamarkupsubsection{Defining new types%
64 \begin{isamarkuptext}%
66 Now we come to the most general method of safely introducing a new type, the
67 \bfindex{type definition}. All other methods, for example
68 \isacommand{datatype}, are based on it. The principle is extremely simple:
69 any non-empty subset of an existing type can be turned into a new type. Thus
70 a type definition is merely a notational device: you introduce a new name for
71 a subset of an existing type. This does not add any logical power to HOL,
72 because you could base all your work directly on the subset of the existing
73 type. However, the resulting theories could easily become undigestible
74 because instead of implicit types you would have explicit sets in your
77 Let us work a simple example, the definition of a three-element type.
78 It is easily represented by the first three natural numbers:%
80 \isacommand{typedef}\ three\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequote}%
82 \noindent\indexbold{*typedef}%
83 In order to enforce that the representing set on the right-hand side is
84 non-empty, this definition actually starts a proof to that effect:
86 \ {\isadigit{1}}{\isachardot}\ {\isasymexists}x{\isachardot}\ x\ {\isasymin}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}%
88 Fortunately, this is easy enough to show: take 0 as a witness.%
90 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isadigit{0}}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
91 \isacommand{by}\ simp%
92 \begin{isamarkuptext}%
93 This type definition introduces the new type \isa{three} and asserts
94 that it is a \emph{copy} of the set \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. This assertion
95 is expressed via a bijection between the \emph{type} \isa{three} and the
96 \emph{set} \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. To this end, the command declares the following
97 constants behind the scenes:
100 \isa{three} &::& \isa{nat\ set} \\
101 \isa{Rep{\isacharunderscore}three} &::& \isa{three\ {\isasymRightarrow}\ nat}\\
102 \isa{Abs{\isacharunderscore}three} &::& \isa{nat\ {\isasymRightarrow}\ three}
105 Constant \isa{three} is just an abbreviation (\isa{three{\isacharunderscore}def}):
107 \ \ \ \ \ three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}%
109 The situation is best summarized with the help of the following diagram,
110 where squares are types and circles are sets:
114 \begin{picture}(100,40)
115 \put(3,13){\framebox(15,15){\isa{three}}}
116 \put(55,5){\framebox(30,30){\isa{three}}}
117 \put(70,32){\makebox(0,0){\isa{nat}}}
118 \put(70,20){\circle{40}}
119 \put(10,15){\vector(1,0){60}}
120 \put(25,14){\makebox(0,0)[tl]{\isa{Rep{\isacharunderscore}three}}}
121 \put(70,25){\vector(-1,0){60}}
122 \put(25,26){\makebox(0,0)[bl]{\isa{Abs{\isacharunderscore}three}}}
125 Finally, \isacommand{typedef} asserts that \isa{Rep{\isacharunderscore}three} is
126 surjective on the subset \isa{three} and \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three} are inverses of each other:
129 \isa{Rep{\isacharunderscore}three\ x\ {\isasymin}\ three} &~~ (\isa{Rep{\isacharunderscore}three}) \\
130 \isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ x} &~~ (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inverse}) \\
131 \isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} &~~ (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse})
135 From the above example it should be clear what \isacommand{typedef} does
136 in general: simply replace the name \isa{three} and the set
137 \isa{{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}} by the respective arguments.
139 Our next step is to define the basic functions expected on the new type.
140 Although this depends on the type at hand, the following strategy works well:
142 \item define a small kernel of basic functions such that all further
143 functions you anticipate can be defined on top of that kernel.
144 \item define the kernel in terms of corresponding functions on the
145 representing type using \isa{Abs} and \isa{Rep} to convert between the
148 In our example it suffices to give the three elements of type \isa{three}
151 \isacommand{constdefs}\isanewline
152 \ \ A{\isacharcolon}{\isacharcolon}\ three\isanewline
153 \ {\isachardoublequote}A\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{0}}{\isachardoublequote}\isanewline
154 \ \ B{\isacharcolon}{\isacharcolon}\ three\isanewline
155 \ {\isachardoublequote}B\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{1}}{\isachardoublequote}\isanewline
156 \ \ C\ {\isacharcolon}{\isacharcolon}\ three\isanewline
157 \ {\isachardoublequote}C\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{2}}{\isachardoublequote}%
158 \begin{isamarkuptext}%
159 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
160 aim must be to raise our level of abstraction by deriving enough theorems
161 about type \isa{three} to characterize it completely. And those theorems
162 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,
163 we merely need to prove that \isa{A}, \isa{B} and \isa{C} are distinct
164 and that they exhaust the type.
166 We start with a helpful version of injectivity of \isa{Abs{\isacharunderscore}three} on the
167 representing subset:%
169 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
170 \ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isasymin}\ three{\isacharsemicolon}\ y\ {\isasymin}\ three\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x{\isacharequal}y{\isacharparenright}{\isachardoublequote}%
171 \begin{isamarkuptxt}%
173 We prove both directions separately. From \isa{Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y}
174 we derive \isa{Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}} (via
175 \isa{arg{\isacharunderscore}cong}: \isa{{\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isacharquery}f\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}f\ {\isacharquery}y}), and thus the required \isa{x\ {\isacharequal}\ y} by simplification with \isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse}. The other direction
176 is trivial by simplification:%
178 \isacommand{apply}{\isacharparenleft}rule\ iffI{\isacharparenright}\isanewline
179 \ \isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ f\ {\isacharequal}\ Rep{\isacharunderscore}three\ \isakeyword{in}\ arg{\isacharunderscore}cong{\isacharparenright}\isanewline
180 \ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Abs{\isacharunderscore}three{\isacharunderscore}inverse{\isacharparenright}\isanewline
181 \isacommand{by}\ simp%
182 \begin{isamarkuptext}%
184 Analogous lemmas can be proved in the same way for arbitrary type definitions.
186 Distinctness of \isa{A}, \isa{B} and \isa{C} follows immediately
187 if we expand their definitions and rewrite with the above simplification rule:%
189 \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
190 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def\ three{\isacharunderscore}def{\isacharparenright}%
191 \begin{isamarkuptext}%
193 Of course we rely on the simplifier to solve goals like \isa{{\isadigit{0}}\ {\isasymnoteq}\ {\isadigit{1}}}.
195 The fact that \isa{A}, \isa{B} and \isa{C} exhaust type \isa{three} is
196 best phrased as a case distinction theorem: if you want to prove \isa{P\ x}
197 (where \isa{x} is of type \isa{three}) it suffices to prove \isa{P\ A},
198 \isa{P\ B} and \isa{P\ C}. First we prove the analogous proposition for the
201 \isacommand{lemma}\ cases{\isacharunderscore}lemma{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ Q\ {\isadigit{0}}{\isacharsemicolon}\ Q\ {\isadigit{1}}{\isacharsemicolon}\ Q\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharcolon}\ three\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ \ Q{\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}%
202 \begin{isamarkuptxt}%
204 Expanding \isa{three{\isacharunderscore}def} yields the premise \isa{n\ {\isasymle}\ {\isadigit{2}}}. Repeated
205 elimination with \isa{le{\isacharunderscore}SucE}
207 \ \ \ \ \ {\isasymlbrakk}{\isacharquery}m\ {\isasymle}\ Suc\ {\isacharquery}n{\isacharsemicolon}\ {\isacharquery}m\ {\isasymle}\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharsemicolon}\ {\isacharquery}m\ {\isacharequal}\ Suc\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R%
209 reduces \isa{n\ {\isasymle}\ {\isadigit{2}}} to the three cases \isa{n\ {\isasymle}\ {\isadigit{0}}}, \isa{n\ {\isacharequal}\ {\isadigit{1}}} and
210 \isa{n\ {\isacharequal}\ {\isadigit{2}}} which are trivial for simplification:%
212 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}three{\isacharunderscore}def{\isacharparenright}\isanewline
213 \isacommand{apply}{\isacharparenleft}{\isacharparenleft}erule\ le{\isacharunderscore}SucE{\isacharparenright}{\isacharplus}{\isacharparenright}\isanewline
214 \isacommand{apply}\ simp{\isacharunderscore}all\isanewline
216 \begin{isamarkuptext}%
217 Now the case distinction lemma on type \isa{three} is easy to derive if you know how to:%
219 \isacommand{lemma}\ three{\isacharunderscore}cases{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}%
220 \begin{isamarkuptxt}%
222 We start by replacing the \isa{x} by \isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}}:%
224 \isacommand{apply}{\isacharparenleft}rule\ subst{\isacharbrackleft}OF\ Rep{\isacharunderscore}three{\isacharunderscore}inverse{\isacharbrackright}{\isacharparenright}%
225 \begin{isamarkuptxt}%
227 This substitution step worked nicely because there was just a single
228 occurrence of a term of type \isa{three}, namely \isa{x}.
229 When we now apply the above lemma, \isa{Q} becomes \isa{{\isasymlambda}n{\isachardot}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ n{\isacharparenright}} because \isa{Rep{\isacharunderscore}three\ x} is the only term of type \isa{nat}:%
231 \isacommand{apply}{\isacharparenleft}rule\ cases{\isacharunderscore}lemma{\isacharparenright}%
232 \begin{isamarkuptxt}%
234 \ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{0}}{\isacharparenright}\isanewline
235 \ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{1}}{\isacharparenright}\isanewline
236 \ {\isadigit{3}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{2}}{\isacharparenright}\isanewline
237 \ {\isadigit{4}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ x\ {\isasymin}\ three%
239 The resulting subgoals are easily solved by simplification:%
241 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def\ Rep{\isacharunderscore}three{\isacharparenright}\isanewline
243 \begin{isamarkuptext}%
245 This concludes the derivation of the characteristic theorems for
248 The attentive reader has realized long ago that the
249 above lengthy definition can be collapsed into one line:%
251 \isacommand{datatype}\ three{\isacharprime}\ {\isacharequal}\ A\ {\isacharbar}\ B\ {\isacharbar}\ C%
252 \begin{isamarkuptext}%
254 In fact, the \isacommand{datatype} command performs internally more or less
255 the same derivations as we did, which gives you some idea what life would be
256 like without \isacommand{datatype}.
258 Although \isa{three} could be defined in one line, we have chosen this
259 example to demonstrate \isacommand{typedef} because its simplicity makes the
260 key concepts particularly easy to grasp. If you would like to see a
261 nontrivial example that cannot be defined more directly, we recommend the
262 definition of \emph{finite multisets} in the HOL library.
264 Let us conclude by summarizing the above procedure for defining a new type.
265 Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
266 set of functions $F$, this involves three steps:
268 \item Find an appropriate type $\tau$ and subset $A$ which has the desired
269 properties $P$, and make a type definition based on this representation.
270 \item Define the required functions $F$ on $ty$ by lifting
271 analogous functions on the representation via $Abs_ty$ and $Rep_ty$.
272 \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
274 You can now forget about the representation and work solely in terms of the
275 abstract functions $F$ and properties $P$.%
280 %%% TeX-master: "root"