10366
|
1 |
(*<*)theory Typedef = Main:(*>*)
|
|
2 |
|
10885
|
3 |
section{*Introducing New Types*}
|
10366
|
4 |
|
|
5 |
text{*\label{sec:adv-typedef}
|
|
6 |
By now we have seen a number of ways for introducing new types, for example
|
|
7 |
type synonyms, recursive datatypes and records. For most applications, this
|
|
8 |
repertoire should be quite sufficient. Very occasionally you may feel the
|
10885
|
9 |
need for a more advanced type. If you cannot do without that type, and you are
|
|
10 |
certain that it is not definable by any of the standard means,
|
10366
|
11 |
then read on.
|
|
12 |
\begin{warn}
|
|
13 |
Types in HOL must be non-empty; otherwise the quantifier rules would be
|
10420
|
14 |
unsound, because $\exists x.\ x=x$ is a theorem.
|
10366
|
15 |
\end{warn}
|
|
16 |
*}
|
|
17 |
|
10885
|
18 |
subsection{*Declaring New Types*}
|
10366
|
19 |
|
|
20 |
text{*\label{sec:typedecl}
|
|
21 |
The most trivial way of introducing a new type is by a \bfindex{type
|
|
22 |
declaration}: *}
|
|
23 |
|
|
24 |
typedecl my_new_type
|
|
25 |
|
|
26 |
text{*\noindent\indexbold{*typedecl}%
|
10420
|
27 |
This does not define @{typ my_new_type} at all but merely introduces its
|
|
28 |
name. Thus we know nothing about this type, except that it is
|
10366
|
29 |
non-empty. Such declarations without definitions are
|
|
30 |
useful only if that type can be viewed as a parameter of a theory and we do
|
|
31 |
not intend to impose any restrictions on it. A typical example is given in
|
|
32 |
\S\ref{sec:VMC}, where we define transition relations over an arbitrary type
|
|
33 |
of states without any internal structure.
|
|
34 |
|
|
35 |
In principle we can always get rid of such type declarations by making those
|
|
36 |
types parameters of every other type, thus keeping the theory generic. In
|
|
37 |
practice, however, the resulting clutter can sometimes make types hard to
|
|
38 |
read.
|
|
39 |
|
|
40 |
If you are looking for a quick and dirty way of introducing a new type
|
|
41 |
together with its properties: declare the type and state its properties as
|
|
42 |
axioms. Example:
|
|
43 |
*}
|
|
44 |
|
|
45 |
axioms
|
10420
|
46 |
just_one: "\<exists>x::my_new_type. \<forall>y. x = y"
|
10366
|
47 |
|
|
48 |
text{*\noindent
|
|
49 |
However, we strongly discourage this approach, except at explorative stages
|
|
50 |
of your development. It is extremely easy to write down contradictory sets of
|
|
51 |
axioms, in which case you will be able to prove everything but it will mean
|
10885
|
52 |
nothing. Here the axiomatic approach is
|
10366
|
53 |
unnecessary: a one-element type called @{typ unit} is already defined in HOL.
|
|
54 |
*}
|
|
55 |
|
10885
|
56 |
subsection{*Defining New Types*}
|
10366
|
57 |
|
|
58 |
text{*\label{sec:typedef}
|
|
59 |
Now we come to the most general method of safely introducing a new type, the
|
|
60 |
\bfindex{type definition}. All other methods, for example
|
|
61 |
\isacommand{datatype}, are based on it. The principle is extremely simple:
|
|
62 |
any non-empty subset of an existing type can be turned into a new type. Thus
|
|
63 |
a type definition is merely a notational device: you introduce a new name for
|
|
64 |
a subset of an existing type. This does not add any logical power to HOL,
|
|
65 |
because you could base all your work directly on the subset of the existing
|
|
66 |
type. However, the resulting theories could easily become undigestible
|
|
67 |
because instead of implicit types you would have explicit sets in your
|
|
68 |
formulae.
|
|
69 |
|
|
70 |
Let us work a simple example, the definition of a three-element type.
|
|
71 |
It is easily represented by the first three natural numbers:
|
|
72 |
*}
|
|
73 |
|
|
74 |
typedef three = "{n. n \<le> 2}"
|
|
75 |
|
|
76 |
txt{*\noindent\indexbold{*typedef}%
|
|
77 |
In order to enforce that the representing set on the right-hand side is
|
|
78 |
non-empty, this definition actually starts a proof to that effect:
|
|
79 |
@{subgoals[display,indent=0]}
|
|
80 |
Fortunately, this is easy enough to show: take 0 as a witness.
|
|
81 |
*}
|
|
82 |
|
|
83 |
apply(rule_tac x = 0 in exI);
|
|
84 |
by simp
|
|
85 |
|
|
86 |
text{*
|
|
87 |
This type definition introduces the new type @{typ three} and asserts
|
|
88 |
that it is a \emph{copy} of the set @{term"{0,1,2}"}. This assertion
|
|
89 |
is expressed via a bijection between the \emph{type} @{typ three} and the
|
|
90 |
\emph{set} @{term"{0,1,2}"}. To this end, the command declares the following
|
|
91 |
constants behind the scenes:
|
|
92 |
\begin{center}
|
|
93 |
\begin{tabular}{rcl}
|
|
94 |
@{term three} &::& @{typ"nat set"} \\
|
|
95 |
@{term Rep_three} &::& @{typ"three \<Rightarrow> nat"}\\
|
|
96 |
@{term Abs_three} &::& @{typ"nat \<Rightarrow> three"}
|
|
97 |
\end{tabular}
|
|
98 |
\end{center}
|
10983
|
99 |
Constant @{term three} is explicitly defined as the representing set:
|
|
100 |
\begin{center}
|
|
101 |
@{thm three_def}\hfill(@{thm[source]three_def})
|
|
102 |
\end{center}
|
10366
|
103 |
The situation is best summarized with the help of the following diagram,
|
|
104 |
where squares are types and circles are sets:
|
|
105 |
\begin{center}
|
|
106 |
\unitlength1mm
|
|
107 |
\thicklines
|
|
108 |
\begin{picture}(100,40)
|
|
109 |
\put(3,13){\framebox(15,15){@{typ three}}}
|
|
110 |
\put(55,5){\framebox(30,30){@{term three}}}
|
|
111 |
\put(70,32){\makebox(0,0){@{typ nat}}}
|
|
112 |
\put(70,20){\circle{40}}
|
|
113 |
\put(10,15){\vector(1,0){60}}
|
|
114 |
\put(25,14){\makebox(0,0)[tl]{@{term Rep_three}}}
|
|
115 |
\put(70,25){\vector(-1,0){60}}
|
|
116 |
\put(25,26){\makebox(0,0)[bl]{@{term Abs_three}}}
|
|
117 |
\end{picture}
|
|
118 |
\end{center}
|
|
119 |
Finally, \isacommand{typedef} asserts that @{term Rep_three} is
|
|
120 |
surjective on the subset @{term three} and @{term Abs_three} and @{term
|
|
121 |
Rep_three} are inverses of each other:
|
|
122 |
\begin{center}
|
10983
|
123 |
\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
|
|
124 |
@{thm Rep_three[no_vars]} & (@{thm[source]Rep_three}) \\
|
|
125 |
@{thm Rep_three_inverse[no_vars]} & (@{thm[source]Rep_three_inverse}) \\
|
|
126 |
@{thm Abs_three_inverse[no_vars]} & (@{thm[source]Abs_three_inverse})
|
10366
|
127 |
\end{tabular}
|
|
128 |
\end{center}
|
10885
|
129 |
%
|
|
130 |
From this example it should be clear what \isacommand{typedef} does
|
|
131 |
in general given a name (here @{text three}) and a set
|
|
132 |
(here @{term"{n. n\<le>2}"}).
|
10366
|
133 |
|
|
134 |
Our next step is to define the basic functions expected on the new type.
|
|
135 |
Although this depends on the type at hand, the following strategy works well:
|
|
136 |
\begin{itemize}
|
10885
|
137 |
\item define a small kernel of basic functions that can express all other
|
|
138 |
functions you anticipate.
|
10366
|
139 |
\item define the kernel in terms of corresponding functions on the
|
|
140 |
representing type using @{term Abs} and @{term Rep} to convert between the
|
|
141 |
two levels.
|
|
142 |
\end{itemize}
|
|
143 |
In our example it suffices to give the three elements of type @{typ three}
|
|
144 |
names:
|
|
145 |
*}
|
|
146 |
|
|
147 |
constdefs
|
|
148 |
A:: three
|
|
149 |
"A \<equiv> Abs_three 0"
|
|
150 |
B:: three
|
|
151 |
"B \<equiv> Abs_three 1"
|
|
152 |
C :: three
|
|
153 |
"C \<equiv> Abs_three 2";
|
|
154 |
|
|
155 |
text{*
|
|
156 |
So far, everything was easy. But it is clear that reasoning about @{typ
|
|
157 |
three} will be hell if we have to go back to @{typ nat} every time. Thus our
|
|
158 |
aim must be to raise our level of abstraction by deriving enough theorems
|
|
159 |
about type @{typ three} to characterize it completely. And those theorems
|
|
160 |
should be phrased in terms of @{term A}, @{term B} and @{term C}, not @{term
|
|
161 |
Abs_three} and @{term Rep_three}. Because of the simplicity of the example,
|
|
162 |
we merely need to prove that @{term A}, @{term B} and @{term C} are distinct
|
|
163 |
and that they exhaust the type.
|
|
164 |
|
|
165 |
We start with a helpful version of injectivity of @{term Abs_three} on the
|
|
166 |
representing subset:
|
|
167 |
*}
|
|
168 |
|
|
169 |
lemma [simp]:
|
|
170 |
"\<lbrakk> x \<in> three; y \<in> three \<rbrakk> \<Longrightarrow> (Abs_three x = Abs_three y) = (x=y)";
|
|
171 |
|
|
172 |
txt{*\noindent
|
10885
|
173 |
We prove each direction separately. From @{prop"Abs_three x = Abs_three y"}
|
|
174 |
we use @{thm[source]arg_cong} to apply @{term Rep_three} to both sides,
|
|
175 |
deriving @{prop[display]"Rep_three(Abs_three x) = Rep_three(Abs_three y)"}
|
|
176 |
Thus we get the required @{prop"x =
|
|
177 |
y"} by simplification with @{thm[source]Abs_three_inverse}.
|
|
178 |
The other direction
|
10366
|
179 |
is trivial by simplification:
|
|
180 |
*}
|
|
181 |
|
|
182 |
apply(rule iffI);
|
|
183 |
apply(drule_tac f = Rep_three in arg_cong);
|
|
184 |
apply(simp add:Abs_three_inverse);
|
|
185 |
by simp;
|
|
186 |
|
|
187 |
text{*\noindent
|
|
188 |
Analogous lemmas can be proved in the same way for arbitrary type definitions.
|
|
189 |
|
|
190 |
Distinctness of @{term A}, @{term B} and @{term C} follows immediately
|
|
191 |
if we expand their definitions and rewrite with the above simplification rule:
|
|
192 |
*}
|
|
193 |
|
|
194 |
lemma "A \<noteq> B \<and> B \<noteq> A \<and> A \<noteq> C \<and> C \<noteq> A \<and> B \<noteq> C \<and> C \<noteq> B";
|
|
195 |
by(simp add:A_def B_def C_def three_def);
|
|
196 |
|
|
197 |
text{*\noindent
|
|
198 |
Of course we rely on the simplifier to solve goals like @{prop"0 \<noteq> 1"}.
|
|
199 |
|
|
200 |
The fact that @{term A}, @{term B} and @{term C} exhaust type @{typ three} is
|
|
201 |
best phrased as a case distinction theorem: if you want to prove @{prop"P x"}
|
|
202 |
(where @{term x} is of type @{typ three}) it suffices to prove @{prop"P A"},
|
|
203 |
@{prop"P B"} and @{prop"P C"}. First we prove the analogous proposition for the
|
|
204 |
representation: *}
|
|
205 |
|
10654
|
206 |
lemma cases_lemma: "\<lbrakk> Q 0; Q 1; Q 2; n : three \<rbrakk> \<Longrightarrow> Q n";
|
10366
|
207 |
|
|
208 |
txt{*\noindent
|
|
209 |
Expanding @{thm[source]three_def} yields the premise @{prop"n\<le>2"}. Repeated
|
|
210 |
elimination with @{thm[source]le_SucE}
|
|
211 |
@{thm[display]le_SucE}
|
|
212 |
reduces @{prop"n\<le>2"} to the three cases @{prop"n\<le>0"}, @{prop"n=1"} and
|
|
213 |
@{prop"n=2"} which are trivial for simplification:
|
|
214 |
*}
|
|
215 |
|
|
216 |
apply(simp add:three_def);
|
|
217 |
apply((erule le_SucE)+);
|
|
218 |
apply simp_all;
|
|
219 |
done
|
|
220 |
|
|
221 |
text{*
|
|
222 |
Now the case distinction lemma on type @{typ three} is easy to derive if you know how to:
|
|
223 |
*}
|
|
224 |
|
|
225 |
lemma three_cases: "\<lbrakk> P A; P B; P C \<rbrakk> \<Longrightarrow> P x";
|
|
226 |
|
|
227 |
txt{*\noindent
|
|
228 |
We start by replacing the @{term x} by @{term"Abs_three(Rep_three x)"}:
|
|
229 |
*}
|
|
230 |
|
|
231 |
apply(rule subst[OF Rep_three_inverse]);
|
|
232 |
|
|
233 |
txt{*\noindent
|
|
234 |
This substitution step worked nicely because there was just a single
|
|
235 |
occurrence of a term of type @{typ three}, namely @{term x}.
|
10885
|
236 |
When we now apply the lemma, @{term Q} becomes @{term"\<lambda>n. P(Abs_three
|
10366
|
237 |
n)"} because @{term"Rep_three x"} is the only term of type @{typ nat}:
|
|
238 |
*}
|
|
239 |
|
|
240 |
apply(rule cases_lemma);
|
|
241 |
|
|
242 |
txt{*
|
|
243 |
@{subgoals[display,indent=0]}
|
|
244 |
The resulting subgoals are easily solved by simplification:
|
|
245 |
*}
|
|
246 |
|
|
247 |
apply(simp_all add:A_def B_def C_def Rep_three);
|
|
248 |
done
|
|
249 |
|
|
250 |
text{*\noindent
|
|
251 |
This concludes the derivation of the characteristic theorems for
|
|
252 |
type @{typ three}.
|
|
253 |
|
|
254 |
The attentive reader has realized long ago that the
|
|
255 |
above lengthy definition can be collapsed into one line:
|
|
256 |
*}
|
|
257 |
|
|
258 |
datatype three' = A | B | C;
|
|
259 |
|
|
260 |
text{*\noindent
|
|
261 |
In fact, the \isacommand{datatype} command performs internally more or less
|
|
262 |
the same derivations as we did, which gives you some idea what life would be
|
|
263 |
like without \isacommand{datatype}.
|
|
264 |
|
|
265 |
Although @{typ three} could be defined in one line, we have chosen this
|
|
266 |
example to demonstrate \isacommand{typedef} because its simplicity makes the
|
|
267 |
key concepts particularly easy to grasp. If you would like to see a
|
11149
|
268 |
non-trivial example that cannot be defined more directly, we recommend the
|
10885
|
269 |
definition of \emph{finite multisets} in the HOL Library.
|
10366
|
270 |
|
|
271 |
Let us conclude by summarizing the above procedure for defining a new type.
|
|
272 |
Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
|
|
273 |
set of functions $F$, this involves three steps:
|
|
274 |
\begin{enumerate}
|
|
275 |
\item Find an appropriate type $\tau$ and subset $A$ which has the desired
|
|
276 |
properties $P$, and make a type definition based on this representation.
|
|
277 |
\item Define the required functions $F$ on $ty$ by lifting
|
|
278 |
analogous functions on the representation via $Abs_ty$ and $Rep_ty$.
|
|
279 |
\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
|
|
280 |
\end{enumerate}
|
|
281 |
You can now forget about the representation and work solely in terms of the
|
|
282 |
abstract functions $F$ and properties $P$.
|
|
283 |
*}
|
|
284 |
|
|
285 |
(*<*)end(*>*)
|