|
1 (*<*)theory Typedef = Main:(*>*) |
|
2 |
|
3 section{*Introducing new types*} |
|
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 |
|
9 need for a more advanced type. If you cannot avoid that type, and you are |
|
10 quite certain that it is not definable by any of the standard means, |
|
11 then read on. |
|
12 \begin{warn} |
|
13 Types in HOL must be non-empty; otherwise the quantifier rules would be |
|
14 unsound, because $\exists x. x=x$ is a theorem. |
|
15 \end{warn} |
|
16 *} |
|
17 |
|
18 subsection{*Declaring new types*} |
|
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}% |
|
27 This does not define the type at all but merely introduces its name, @{typ |
|
28 my_new_type}. Thus we know nothing about this type, except that it is |
|
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 |
|
46 just_one: "\<exists>! x::my_new_type. True" |
|
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 |
|
52 nothing. In the above case it also turns out that the axiomatic approach is |
|
53 unnecessary: a one-element type called @{typ unit} is already defined in HOL. |
|
54 *} |
|
55 |
|
56 subsection{*Defining new types*} |
|
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} |
|
99 Constant @{term three} is just an abbreviation (@{thm[source]three_def}): |
|
100 @{thm[display]three_def} |
|
101 The situation is best summarized with the help of the following diagram, |
|
102 where squares are types and circles are sets: |
|
103 \begin{center} |
|
104 \unitlength1mm |
|
105 \thicklines |
|
106 \begin{picture}(100,40) |
|
107 \put(3,13){\framebox(15,15){@{typ three}}} |
|
108 \put(55,5){\framebox(30,30){@{term three}}} |
|
109 \put(70,32){\makebox(0,0){@{typ nat}}} |
|
110 \put(70,20){\circle{40}} |
|
111 \put(10,15){\vector(1,0){60}} |
|
112 \put(25,14){\makebox(0,0)[tl]{@{term Rep_three}}} |
|
113 \put(70,25){\vector(-1,0){60}} |
|
114 \put(25,26){\makebox(0,0)[bl]{@{term Abs_three}}} |
|
115 \end{picture} |
|
116 \end{center} |
|
117 Finally, \isacommand{typedef} asserts that @{term Rep_three} is |
|
118 surjective on the subset @{term three} and @{term Abs_three} and @{term |
|
119 Rep_three} are inverses of each other: |
|
120 \begin{center} |
|
121 \begin{tabular}{rl} |
|
122 @{thm Rep_three[no_vars]} &~~ (@{thm[source]Rep_three}) \\ |
|
123 @{thm Rep_three_inverse[no_vars]} &~~ (@{thm[source]Rep_three_inverse}) \\ |
|
124 @{thm Abs_three_inverse[no_vars]} &~~ (@{thm[source]Abs_three_inverse}) |
|
125 \end{tabular} |
|
126 \end{center} |
|
127 |
|
128 From the above example it should be clear what \isacommand{typedef} does |
|
129 in general: simply replace the name @{text three} and the set |
|
130 @{term"{n. n\<le>2}"} by the respective arguments. |
|
131 |
|
132 Our next step is to define the basic functions expected on the new type. |
|
133 Although this depends on the type at hand, the following strategy works well: |
|
134 \begin{itemize} |
|
135 \item define a small kernel of basic functions such that all further |
|
136 functions you anticipate can be defined on top of that kernel. |
|
137 \item define the kernel in terms of corresponding functions on the |
|
138 representing type using @{term Abs} and @{term Rep} to convert between the |
|
139 two levels. |
|
140 \end{itemize} |
|
141 In our example it suffices to give the three elements of type @{typ three} |
|
142 names: |
|
143 *} |
|
144 |
|
145 constdefs |
|
146 A:: three |
|
147 "A \<equiv> Abs_three 0" |
|
148 B:: three |
|
149 "B \<equiv> Abs_three 1" |
|
150 C :: three |
|
151 "C \<equiv> Abs_three 2"; |
|
152 |
|
153 text{* |
|
154 So far, everything was easy. But it is clear that reasoning about @{typ |
|
155 three} will be hell if we have to go back to @{typ nat} every time. Thus our |
|
156 aim must be to raise our level of abstraction by deriving enough theorems |
|
157 about type @{typ three} to characterize it completely. And those theorems |
|
158 should be phrased in terms of @{term A}, @{term B} and @{term C}, not @{term |
|
159 Abs_three} and @{term Rep_three}. Because of the simplicity of the example, |
|
160 we merely need to prove that @{term A}, @{term B} and @{term C} are distinct |
|
161 and that they exhaust the type. |
|
162 |
|
163 We start with a helpful version of injectivity of @{term Abs_three} on the |
|
164 representing subset: |
|
165 *} |
|
166 |
|
167 lemma [simp]: |
|
168 "\<lbrakk> x \<in> three; y \<in> three \<rbrakk> \<Longrightarrow> (Abs_three x = Abs_three y) = (x=y)"; |
|
169 |
|
170 txt{*\noindent |
|
171 We prove both directions separately. From @{prop"Abs_three x = Abs_three y"} |
|
172 we derive @{prop"Rep_three(Abs_three x) = Rep_three(Abs_three y)"} (via |
|
173 @{thm[source]arg_cong}: @{thm arg_cong}), and thus the required @{prop"x = |
|
174 y"} by simplification with @{thm[source]Abs_three_inverse}. The other direction |
|
175 is trivial by simplification: |
|
176 *} |
|
177 |
|
178 apply(rule iffI); |
|
179 apply(drule_tac f = Rep_three in arg_cong); |
|
180 apply(simp add:Abs_three_inverse); |
|
181 by simp; |
|
182 |
|
183 text{*\noindent |
|
184 Analogous lemmas can be proved in the same way for arbitrary type definitions. |
|
185 |
|
186 Distinctness of @{term A}, @{term B} and @{term C} follows immediately |
|
187 if we expand their definitions and rewrite with the above simplification rule: |
|
188 *} |
|
189 |
|
190 lemma "A \<noteq> B \<and> B \<noteq> A \<and> A \<noteq> C \<and> C \<noteq> A \<and> B \<noteq> C \<and> C \<noteq> B"; |
|
191 by(simp add:A_def B_def C_def three_def); |
|
192 |
|
193 text{*\noindent |
|
194 Of course we rely on the simplifier to solve goals like @{prop"0 \<noteq> 1"}. |
|
195 |
|
196 The fact that @{term A}, @{term B} and @{term C} exhaust type @{typ three} is |
|
197 best phrased as a case distinction theorem: if you want to prove @{prop"P x"} |
|
198 (where @{term x} is of type @{typ three}) it suffices to prove @{prop"P A"}, |
|
199 @{prop"P B"} and @{prop"P C"}. First we prove the analogous proposition for the |
|
200 representation: *} |
|
201 |
|
202 lemma cases_lemma: "\<lbrakk> Q 0; Q 1; Q 2; n : three \<rbrakk> \<Longrightarrow> Q(n::nat)"; |
|
203 |
|
204 txt{*\noindent |
|
205 Expanding @{thm[source]three_def} yields the premise @{prop"n\<le>2"}. Repeated |
|
206 elimination with @{thm[source]le_SucE} |
|
207 @{thm[display]le_SucE} |
|
208 reduces @{prop"n\<le>2"} to the three cases @{prop"n\<le>0"}, @{prop"n=1"} and |
|
209 @{prop"n=2"} which are trivial for simplification: |
|
210 *} |
|
211 |
|
212 apply(simp add:three_def); |
|
213 apply((erule le_SucE)+); |
|
214 apply simp_all; |
|
215 done |
|
216 |
|
217 text{* |
|
218 Now the case distinction lemma on type @{typ three} is easy to derive if you know how to: |
|
219 *} |
|
220 |
|
221 lemma three_cases: "\<lbrakk> P A; P B; P C \<rbrakk> \<Longrightarrow> P x"; |
|
222 |
|
223 txt{*\noindent |
|
224 We start by replacing the @{term x} by @{term"Abs_three(Rep_three x)"}: |
|
225 *} |
|
226 |
|
227 apply(rule subst[OF Rep_three_inverse]); |
|
228 |
|
229 txt{*\noindent |
|
230 This substitution step worked nicely because there was just a single |
|
231 occurrence of a term of type @{typ three}, namely @{term x}. |
|
232 When we now apply the above lemma, @{term Q} becomes @{term"\<lambda>n. P(Abs_three |
|
233 n)"} because @{term"Rep_three x"} is the only term of type @{typ nat}: |
|
234 *} |
|
235 |
|
236 apply(rule cases_lemma); |
|
237 |
|
238 txt{* |
|
239 @{subgoals[display,indent=0]} |
|
240 The resulting subgoals are easily solved by simplification: |
|
241 *} |
|
242 |
|
243 apply(simp_all add:A_def B_def C_def Rep_three); |
|
244 done |
|
245 |
|
246 text{*\noindent |
|
247 This concludes the derivation of the characteristic theorems for |
|
248 type @{typ three}. |
|
249 |
|
250 The attentive reader has realized long ago that the |
|
251 above lengthy definition can be collapsed into one line: |
|
252 *} |
|
253 |
|
254 datatype three' = A | B | C; |
|
255 |
|
256 text{*\noindent |
|
257 In fact, the \isacommand{datatype} command performs internally more or less |
|
258 the same derivations as we did, which gives you some idea what life would be |
|
259 like without \isacommand{datatype}. |
|
260 |
|
261 Although @{typ three} could be defined in one line, we have chosen this |
|
262 example to demonstrate \isacommand{typedef} because its simplicity makes the |
|
263 key concepts particularly easy to grasp. If you would like to see a |
|
264 nontrivial example that cannot be defined more directly, we recommend the |
|
265 definition of \emph{finite multisets} in the HOL library. |
|
266 |
|
267 Let us conclude by summarizing the above procedure for defining a new type. |
|
268 Given some abstract axiomatic description $P$ of a type $ty$ in terms of a |
|
269 set of functions $F$, this involves three steps: |
|
270 \begin{enumerate} |
|
271 \item Find an appropriate type $\tau$ and subset $A$ which has the desired |
|
272 properties $P$, and make a type definition based on this representation. |
|
273 \item Define the required functions $F$ on $ty$ by lifting |
|
274 analogous functions on the representation via $Abs_ty$ and $Rep_ty$. |
|
275 \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation. |
|
276 \end{enumerate} |
|
277 You can now forget about the representation and work solely in terms of the |
|
278 abstract functions $F$ and properties $P$. |
|
279 *} |
|
280 |
|
281 (*<*)end(*>*) |