author | wenzelm |
Wed, 06 Dec 2006 01:12:43 +0100 | |
changeset 21672 | 29c346b165d4 |
parent 21669 | c68717c16013 |
child 21905 | 500f91bf992c |
permissions | -rw-r--r-- |
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
1 |
(* Title: HOL/Datatype.thy |
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
20819 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
11954 | 4 |
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
20819 | 5 |
|
6 |
Could <*> be generalized to a general summation (Sigma)? |
|
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
7 |
*) |
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
8 |
|
21669 | 9 |
header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *} |
11954 | 10 |
|
15131 | 11 |
theory Datatype |
21243 | 12 |
imports Nat Sum_Type |
15131 | 13 |
begin |
11954 | 14 |
|
20819 | 15 |
typedef (Node) |
16 |
('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" |
|
17 |
--{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*} |
|
18 |
by auto |
|
19 |
||
20 |
text{*Datatypes will be represented by sets of type @{text node}*} |
|
21 |
||
22 |
types 'a item = "('a, unit) node set" |
|
23 |
('a, 'b) dtree = "('a, 'b) node set" |
|
24 |
||
25 |
consts |
|
26 |
apfst :: "['a=>'c, 'a*'b] => 'c*'b" |
|
27 |
Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))" |
|
28 |
||
29 |
Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node" |
|
30 |
ndepth :: "('a, 'b) node => nat" |
|
31 |
||
32 |
Atom :: "('a + nat) => ('a, 'b) dtree" |
|
33 |
Leaf :: "'a => ('a, 'b) dtree" |
|
34 |
Numb :: "nat => ('a, 'b) dtree" |
|
35 |
Scons :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree" |
|
36 |
In0 :: "('a, 'b) dtree => ('a, 'b) dtree" |
|
37 |
In1 :: "('a, 'b) dtree => ('a, 'b) dtree" |
|
38 |
Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree" |
|
39 |
||
40 |
ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree" |
|
41 |
||
42 |
uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set" |
|
43 |
usum :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set" |
|
44 |
||
45 |
Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c" |
|
46 |
Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c" |
|
47 |
||
48 |
dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] |
|
49 |
=> (('a, 'b) dtree * ('a, 'b) dtree)set" |
|
50 |
dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] |
|
51 |
=> (('a, 'b) dtree * ('a, 'b) dtree)set" |
|
52 |
||
53 |
||
54 |
defs |
|
55 |
||
56 |
Push_Node_def: "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))" |
|
57 |
||
58 |
(*crude "lists" of nats -- needed for the constructions*) |
|
59 |
apfst_def: "apfst == (%f (x,y). (f(x),y))" |
|
60 |
Push_def: "Push == (%b h. nat_case b h)" |
|
61 |
||
62 |
(** operations on S-expressions -- sets of nodes **) |
|
63 |
||
64 |
(*S-expression constructors*) |
|
65 |
Atom_def: "Atom == (%x. {Abs_Node((%k. Inr 0, x))})" |
|
66 |
Scons_def: "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)" |
|
67 |
||
68 |
(*Leaf nodes, with arbitrary or nat labels*) |
|
69 |
Leaf_def: "Leaf == Atom o Inl" |
|
70 |
Numb_def: "Numb == Atom o Inr" |
|
71 |
||
72 |
(*Injections of the "disjoint sum"*) |
|
73 |
In0_def: "In0(M) == Scons (Numb 0) M" |
|
74 |
In1_def: "In1(M) == Scons (Numb 1) M" |
|
75 |
||
76 |
(*Function spaces*) |
|
77 |
Lim_def: "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}" |
|
78 |
||
79 |
(*the set of nodes with depth less than k*) |
|
80 |
ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)" |
|
81 |
ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}" |
|
82 |
||
83 |
(*products and sums for the "universe"*) |
|
84 |
uprod_def: "uprod A B == UN x:A. UN y:B. { Scons x y }" |
|
85 |
usum_def: "usum A B == In0`A Un In1`B" |
|
86 |
||
87 |
(*the corresponding eliminators*) |
|
88 |
Split_def: "Split c M == THE u. EX x y. M = Scons x y & u = c x y" |
|
89 |
||
90 |
Case_def: "Case c d M == THE u. (EX x . M = In0(x) & u = c(x)) |
|
91 |
| (EX y . M = In1(y) & u = d(y))" |
|
92 |
||
93 |
||
94 |
(** equality for the "universe" **) |
|
95 |
||
96 |
dprod_def: "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}" |
|
97 |
||
98 |
dsum_def: "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un |
|
99 |
(UN (y,y'):s. {(In1(y),In1(y'))})" |
|
100 |
||
101 |
||
102 |
||
103 |
(** apfst -- can be used in similar type definitions **) |
|
104 |
||
105 |
lemma apfst_conv [simp]: "apfst f (a,b) = (f(a),b)" |
|
106 |
by (simp add: apfst_def) |
|
107 |
||
108 |
||
109 |
lemma apfst_convE: |
|
110 |
"[| q = apfst f p; !!x y. [| p = (x,y); q = (f(x),y) |] ==> R |
|
111 |
|] ==> R" |
|
112 |
by (force simp add: apfst_def) |
|
113 |
||
114 |
(** Push -- an injection, analogous to Cons on lists **) |
|
115 |
||
116 |
lemma Push_inject1: "Push i f = Push j g ==> i=j" |
|
117 |
apply (simp add: Push_def expand_fun_eq) |
|
118 |
apply (drule_tac x=0 in spec, simp) |
|
119 |
done |
|
120 |
||
121 |
lemma Push_inject2: "Push i f = Push j g ==> f=g" |
|
122 |
apply (auto simp add: Push_def expand_fun_eq) |
|
123 |
apply (drule_tac x="Suc x" in spec, simp) |
|
124 |
done |
|
125 |
||
126 |
lemma Push_inject: |
|
127 |
"[| Push i f =Push j g; [| i=j; f=g |] ==> P |] ==> P" |
|
128 |
by (blast dest: Push_inject1 Push_inject2) |
|
129 |
||
130 |
lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P" |
|
131 |
by (auto simp add: Push_def expand_fun_eq split: nat.split_asm) |
|
132 |
||
133 |
lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1, standard] |
|
134 |
||
135 |
||
136 |
(*** Introduction rules for Node ***) |
|
137 |
||
138 |
lemma Node_K0_I: "(%k. Inr 0, a) : Node" |
|
139 |
by (simp add: Node_def) |
|
140 |
||
141 |
lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node" |
|
142 |
apply (simp add: Node_def Push_def) |
|
143 |
apply (fast intro!: apfst_conv nat_case_Suc [THEN trans]) |
|
144 |
done |
|
145 |
||
146 |
||
147 |
subsection{*Freeness: Distinctness of Constructors*} |
|
148 |
||
149 |
(** Scons vs Atom **) |
|
150 |
||
151 |
lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)" |
|
152 |
apply (simp add: Atom_def Scons_def Push_Node_def One_nat_def) |
|
153 |
apply (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] |
|
154 |
dest!: Abs_Node_inj |
|
155 |
elim!: apfst_convE sym [THEN Push_neq_K0]) |
|
156 |
done |
|
157 |
||
21407 | 158 |
lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym, standard] |
159 |
||
20819 | 160 |
|
161 |
(*** Injectiveness ***) |
|
162 |
||
163 |
(** Atomic nodes **) |
|
164 |
||
165 |
lemma inj_Atom: "inj(Atom)" |
|
166 |
apply (simp add: Atom_def) |
|
167 |
apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj) |
|
168 |
done |
|
169 |
lemmas Atom_inject = inj_Atom [THEN injD, standard] |
|
170 |
||
171 |
lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)" |
|
172 |
by (blast dest!: Atom_inject) |
|
173 |
||
174 |
lemma inj_Leaf: "inj(Leaf)" |
|
175 |
apply (simp add: Leaf_def o_def) |
|
176 |
apply (rule inj_onI) |
|
177 |
apply (erule Atom_inject [THEN Inl_inject]) |
|
178 |
done |
|
179 |
||
21407 | 180 |
lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD, standard] |
20819 | 181 |
|
182 |
lemma inj_Numb: "inj(Numb)" |
|
183 |
apply (simp add: Numb_def o_def) |
|
184 |
apply (rule inj_onI) |
|
185 |
apply (erule Atom_inject [THEN Inr_inject]) |
|
186 |
done |
|
187 |
||
21407 | 188 |
lemmas Numb_inject [dest!] = inj_Numb [THEN injD, standard] |
20819 | 189 |
|
190 |
||
191 |
(** Injectiveness of Push_Node **) |
|
192 |
||
193 |
lemma Push_Node_inject: |
|
194 |
"[| Push_Node i m =Push_Node j n; [| i=j; m=n |] ==> P |
|
195 |
|] ==> P" |
|
196 |
apply (simp add: Push_Node_def) |
|
197 |
apply (erule Abs_Node_inj [THEN apfst_convE]) |
|
198 |
apply (rule Rep_Node [THEN Node_Push_I])+ |
|
199 |
apply (erule sym [THEN apfst_convE]) |
|
200 |
apply (blast intro: Rep_Node_inject [THEN iffD1] trans sym elim!: Push_inject) |
|
201 |
done |
|
202 |
||
203 |
||
204 |
(** Injectiveness of Scons **) |
|
205 |
||
206 |
lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'" |
|
207 |
apply (simp add: Scons_def One_nat_def) |
|
208 |
apply (blast dest!: Push_Node_inject) |
|
209 |
done |
|
210 |
||
211 |
lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'" |
|
212 |
apply (simp add: Scons_def One_nat_def) |
|
213 |
apply (blast dest!: Push_Node_inject) |
|
214 |
done |
|
215 |
||
216 |
lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'" |
|
217 |
apply (erule equalityE) |
|
218 |
apply (iprover intro: equalityI Scons_inject_lemma1) |
|
219 |
done |
|
220 |
||
221 |
lemma Scons_inject2: "Scons M N = Scons M' N' ==> N=N'" |
|
222 |
apply (erule equalityE) |
|
223 |
apply (iprover intro: equalityI Scons_inject_lemma2) |
|
224 |
done |
|
225 |
||
226 |
lemma Scons_inject: |
|
227 |
"[| Scons M N = Scons M' N'; [| M=M'; N=N' |] ==> P |] ==> P" |
|
228 |
by (iprover dest: Scons_inject1 Scons_inject2) |
|
229 |
||
230 |
lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' & N=N')" |
|
231 |
by (blast elim!: Scons_inject) |
|
232 |
||
233 |
(*** Distinctness involving Leaf and Numb ***) |
|
234 |
||
235 |
(** Scons vs Leaf **) |
|
236 |
||
237 |
lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)" |
|
238 |
by (simp add: Leaf_def o_def Scons_not_Atom) |
|
239 |
||
21407 | 240 |
lemmas Leaf_not_Scons [iff] = Scons_not_Leaf [THEN not_sym, standard] |
20819 | 241 |
|
242 |
(** Scons vs Numb **) |
|
243 |
||
244 |
lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)" |
|
245 |
by (simp add: Numb_def o_def Scons_not_Atom) |
|
246 |
||
21407 | 247 |
lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard] |
20819 | 248 |
|
249 |
||
250 |
(** Leaf vs Numb **) |
|
251 |
||
252 |
lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)" |
|
253 |
by (simp add: Leaf_def Numb_def) |
|
254 |
||
21407 | 255 |
lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym, standard] |
20819 | 256 |
|
257 |
||
258 |
(*** ndepth -- the depth of a node ***) |
|
259 |
||
260 |
lemma ndepth_K0: "ndepth (Abs_Node(%k. Inr 0, x)) = 0" |
|
261 |
by (simp add: ndepth_def Node_K0_I [THEN Abs_Node_inverse] Least_equality) |
|
262 |
||
263 |
lemma ndepth_Push_Node_aux: |
|
264 |
"nat_case (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k" |
|
265 |
apply (induct_tac "k", auto) |
|
266 |
apply (erule Least_le) |
|
267 |
done |
|
268 |
||
269 |
lemma ndepth_Push_Node: |
|
270 |
"ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))" |
|
271 |
apply (insert Rep_Node [of n, unfolded Node_def]) |
|
272 |
apply (auto simp add: ndepth_def Push_Node_def |
|
273 |
Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse]) |
|
274 |
apply (rule Least_equality) |
|
275 |
apply (auto simp add: Push_def ndepth_Push_Node_aux) |
|
276 |
apply (erule LeastI) |
|
277 |
done |
|
278 |
||
279 |
||
280 |
(*** ntrunc applied to the various node sets ***) |
|
281 |
||
282 |
lemma ntrunc_0 [simp]: "ntrunc 0 M = {}" |
|
283 |
by (simp add: ntrunc_def) |
|
284 |
||
285 |
lemma ntrunc_Atom [simp]: "ntrunc (Suc k) (Atom a) = Atom(a)" |
|
286 |
by (auto simp add: Atom_def ntrunc_def ndepth_K0) |
|
287 |
||
288 |
lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)" |
|
289 |
by (simp add: Leaf_def o_def ntrunc_Atom) |
|
290 |
||
291 |
lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)" |
|
292 |
by (simp add: Numb_def o_def ntrunc_Atom) |
|
293 |
||
294 |
lemma ntrunc_Scons [simp]: |
|
295 |
"ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)" |
|
296 |
by (auto simp add: Scons_def ntrunc_def One_nat_def ndepth_Push_Node) |
|
297 |
||
298 |
||
299 |
||
300 |
(** Injection nodes **) |
|
301 |
||
302 |
lemma ntrunc_one_In0 [simp]: "ntrunc (Suc 0) (In0 M) = {}" |
|
303 |
apply (simp add: In0_def) |
|
304 |
apply (simp add: Scons_def) |
|
305 |
done |
|
306 |
||
307 |
lemma ntrunc_In0 [simp]: "ntrunc (Suc(Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)" |
|
308 |
by (simp add: In0_def) |
|
309 |
||
310 |
lemma ntrunc_one_In1 [simp]: "ntrunc (Suc 0) (In1 M) = {}" |
|
311 |
apply (simp add: In1_def) |
|
312 |
apply (simp add: Scons_def) |
|
313 |
done |
|
314 |
||
315 |
lemma ntrunc_In1 [simp]: "ntrunc (Suc(Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)" |
|
316 |
by (simp add: In1_def) |
|
317 |
||
318 |
||
319 |
subsection{*Set Constructions*} |
|
320 |
||
321 |
||
322 |
(*** Cartesian Product ***) |
|
323 |
||
324 |
lemma uprodI [intro!]: "[| M:A; N:B |] ==> Scons M N : uprod A B" |
|
325 |
by (simp add: uprod_def) |
|
326 |
||
327 |
(*The general elimination rule*) |
|
328 |
lemma uprodE [elim!]: |
|
329 |
"[| c : uprod A B; |
|
330 |
!!x y. [| x:A; y:B; c = Scons x y |] ==> P |
|
331 |
|] ==> P" |
|
332 |
by (auto simp add: uprod_def) |
|
333 |
||
334 |
||
335 |
(*Elimination of a pair -- introduces no eigenvariables*) |
|
336 |
lemma uprodE2: "[| Scons M N : uprod A B; [| M:A; N:B |] ==> P |] ==> P" |
|
337 |
by (auto simp add: uprod_def) |
|
338 |
||
339 |
||
340 |
(*** Disjoint Sum ***) |
|
341 |
||
342 |
lemma usum_In0I [intro]: "M:A ==> In0(M) : usum A B" |
|
343 |
by (simp add: usum_def) |
|
344 |
||
345 |
lemma usum_In1I [intro]: "N:B ==> In1(N) : usum A B" |
|
346 |
by (simp add: usum_def) |
|
347 |
||
348 |
lemma usumE [elim!]: |
|
349 |
"[| u : usum A B; |
|
350 |
!!x. [| x:A; u=In0(x) |] ==> P; |
|
351 |
!!y. [| y:B; u=In1(y) |] ==> P |
|
352 |
|] ==> P" |
|
353 |
by (auto simp add: usum_def) |
|
354 |
||
355 |
||
356 |
(** Injection **) |
|
357 |
||
358 |
lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)" |
|
359 |
by (auto simp add: In0_def In1_def One_nat_def) |
|
360 |
||
21407 | 361 |
lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard] |
20819 | 362 |
|
363 |
lemma In0_inject: "In0(M) = In0(N) ==> M=N" |
|
364 |
by (simp add: In0_def) |
|
365 |
||
366 |
lemma In1_inject: "In1(M) = In1(N) ==> M=N" |
|
367 |
by (simp add: In1_def) |
|
368 |
||
369 |
lemma In0_eq [iff]: "(In0 M = In0 N) = (M=N)" |
|
370 |
by (blast dest!: In0_inject) |
|
371 |
||
372 |
lemma In1_eq [iff]: "(In1 M = In1 N) = (M=N)" |
|
373 |
by (blast dest!: In1_inject) |
|
374 |
||
375 |
lemma inj_In0: "inj In0" |
|
376 |
by (blast intro!: inj_onI) |
|
377 |
||
378 |
lemma inj_In1: "inj In1" |
|
379 |
by (blast intro!: inj_onI) |
|
380 |
||
381 |
||
382 |
(*** Function spaces ***) |
|
383 |
||
384 |
lemma Lim_inject: "Lim f = Lim g ==> f = g" |
|
385 |
apply (simp add: Lim_def) |
|
386 |
apply (rule ext) |
|
387 |
apply (blast elim!: Push_Node_inject) |
|
388 |
done |
|
389 |
||
390 |
||
391 |
(*** proving equality of sets and functions using ntrunc ***) |
|
392 |
||
393 |
lemma ntrunc_subsetI: "ntrunc k M <= M" |
|
394 |
by (auto simp add: ntrunc_def) |
|
395 |
||
396 |
lemma ntrunc_subsetD: "(!!k. ntrunc k M <= N) ==> M<=N" |
|
397 |
by (auto simp add: ntrunc_def) |
|
398 |
||
399 |
(*A generalized form of the take-lemma*) |
|
400 |
lemma ntrunc_equality: "(!!k. ntrunc k M = ntrunc k N) ==> M=N" |
|
401 |
apply (rule equalityI) |
|
402 |
apply (rule_tac [!] ntrunc_subsetD) |
|
403 |
apply (rule_tac [!] ntrunc_subsetI [THEN [2] subset_trans], auto) |
|
404 |
done |
|
405 |
||
406 |
lemma ntrunc_o_equality: |
|
407 |
"[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2" |
|
408 |
apply (rule ntrunc_equality [THEN ext]) |
|
409 |
apply (simp add: expand_fun_eq) |
|
410 |
done |
|
411 |
||
412 |
||
413 |
(*** Monotonicity ***) |
|
414 |
||
415 |
lemma uprod_mono: "[| A<=A'; B<=B' |] ==> uprod A B <= uprod A' B'" |
|
416 |
by (simp add: uprod_def, blast) |
|
417 |
||
418 |
lemma usum_mono: "[| A<=A'; B<=B' |] ==> usum A B <= usum A' B'" |
|
419 |
by (simp add: usum_def, blast) |
|
420 |
||
421 |
lemma Scons_mono: "[| M<=M'; N<=N' |] ==> Scons M N <= Scons M' N'" |
|
422 |
by (simp add: Scons_def, blast) |
|
423 |
||
424 |
lemma In0_mono: "M<=N ==> In0(M) <= In0(N)" |
|
425 |
by (simp add: In0_def subset_refl Scons_mono) |
|
426 |
||
427 |
lemma In1_mono: "M<=N ==> In1(M) <= In1(N)" |
|
428 |
by (simp add: In1_def subset_refl Scons_mono) |
|
429 |
||
430 |
||
431 |
(*** Split and Case ***) |
|
432 |
||
433 |
lemma Split [simp]: "Split c (Scons M N) = c M N" |
|
434 |
by (simp add: Split_def) |
|
435 |
||
436 |
lemma Case_In0 [simp]: "Case c d (In0 M) = c(M)" |
|
437 |
by (simp add: Case_def) |
|
438 |
||
439 |
lemma Case_In1 [simp]: "Case c d (In1 N) = d(N)" |
|
440 |
by (simp add: Case_def) |
|
441 |
||
442 |
||
443 |
||
444 |
(**** UN x. B(x) rules ****) |
|
445 |
||
446 |
lemma ntrunc_UN1: "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))" |
|
447 |
by (simp add: ntrunc_def, blast) |
|
448 |
||
449 |
lemma Scons_UN1_x: "Scons (UN x. f x) M = (UN x. Scons (f x) M)" |
|
450 |
by (simp add: Scons_def, blast) |
|
451 |
||
452 |
lemma Scons_UN1_y: "Scons M (UN x. f x) = (UN x. Scons M (f x))" |
|
453 |
by (simp add: Scons_def, blast) |
|
454 |
||
455 |
lemma In0_UN1: "In0(UN x. f(x)) = (UN x. In0(f(x)))" |
|
456 |
by (simp add: In0_def Scons_UN1_y) |
|
457 |
||
458 |
lemma In1_UN1: "In1(UN x. f(x)) = (UN x. In1(f(x)))" |
|
459 |
by (simp add: In1_def Scons_UN1_y) |
|
460 |
||
461 |
||
462 |
(*** Equality for Cartesian Product ***) |
|
463 |
||
464 |
lemma dprodI [intro!]: |
|
465 |
"[| (M,M'):r; (N,N'):s |] ==> (Scons M N, Scons M' N') : dprod r s" |
|
466 |
by (auto simp add: dprod_def) |
|
467 |
||
468 |
(*The general elimination rule*) |
|
469 |
lemma dprodE [elim!]: |
|
470 |
"[| c : dprod r s; |
|
471 |
!!x y x' y'. [| (x,x') : r; (y,y') : s; |
|
472 |
c = (Scons x y, Scons x' y') |] ==> P |
|
473 |
|] ==> P" |
|
474 |
by (auto simp add: dprod_def) |
|
475 |
||
476 |
||
477 |
(*** Equality for Disjoint Sum ***) |
|
478 |
||
479 |
lemma dsum_In0I [intro]: "(M,M'):r ==> (In0(M), In0(M')) : dsum r s" |
|
480 |
by (auto simp add: dsum_def) |
|
481 |
||
482 |
lemma dsum_In1I [intro]: "(N,N'):s ==> (In1(N), In1(N')) : dsum r s" |
|
483 |
by (auto simp add: dsum_def) |
|
484 |
||
485 |
lemma dsumE [elim!]: |
|
486 |
"[| w : dsum r s; |
|
487 |
!!x x'. [| (x,x') : r; w = (In0(x), In0(x')) |] ==> P; |
|
488 |
!!y y'. [| (y,y') : s; w = (In1(y), In1(y')) |] ==> P |
|
489 |
|] ==> P" |
|
490 |
by (auto simp add: dsum_def) |
|
491 |
||
492 |
||
493 |
(*** Monotonicity ***) |
|
494 |
||
495 |
lemma dprod_mono: "[| r<=r'; s<=s' |] ==> dprod r s <= dprod r' s'" |
|
496 |
by blast |
|
497 |
||
498 |
lemma dsum_mono: "[| r<=r'; s<=s' |] ==> dsum r s <= dsum r' s'" |
|
499 |
by blast |
|
500 |
||
501 |
||
502 |
(*** Bounding theorems ***) |
|
503 |
||
504 |
lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)" |
|
505 |
by blast |
|
506 |
||
507 |
lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma, standard] |
|
508 |
||
509 |
(*Dependent version*) |
|
510 |
lemma dprod_subset_Sigma2: |
|
511 |
"(dprod (Sigma A B) (Sigma C D)) <= |
|
512 |
Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))" |
|
513 |
by auto |
|
514 |
||
515 |
lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)" |
|
516 |
by blast |
|
517 |
||
518 |
lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard] |
|
519 |
||
520 |
||
521 |
(*** Domain ***) |
|
522 |
||
523 |
lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)" |
|
524 |
by auto |
|
525 |
||
526 |
lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)" |
|
527 |
by auto |
|
528 |
||
529 |
||
530 |
subsection {* Finishing the datatype package setup *} |
|
531 |
||
532 |
text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *} |
|
20847 | 533 |
setup "DatatypeCodegen.setup_hooks" |
20819 | 534 |
hide (open) const Push Node Atom Leaf Numb Lim Split Case |
535 |
hide (open) type node item |
|
536 |
||
537 |
||
538 |
section {* Datatypes *} |
|
539 |
||
11954 | 540 |
subsection {* Representing primitive types *} |
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
541 |
|
5759 | 542 |
rep_datatype bool |
11954 | 543 |
distinct True_not_False False_not_True |
544 |
induction bool_induct |
|
545 |
||
546 |
declare case_split [cases type: bool] |
|
547 |
-- "prefer plain propositional version" |
|
548 |
||
549 |
rep_datatype unit |
|
550 |
induction unit_induct |
|
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
551 |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
552 |
rep_datatype prod |
11954 | 553 |
inject Pair_eq |
554 |
induction prod_induct |
|
555 |
||
12918 | 556 |
rep_datatype sum |
557 |
distinct Inl_not_Inr Inr_not_Inl |
|
558 |
inject Inl_eq Inr_eq |
|
559 |
induction sum_induct |
|
560 |
||
561 |
lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)" |
|
562 |
apply (rule_tac s = s in sumE) |
|
563 |
apply (erule ssubst) |
|
20798 | 564 |
apply (rule sum.cases(1)) |
12918 | 565 |
apply (erule ssubst) |
20798 | 566 |
apply (rule sum.cases(2)) |
12918 | 567 |
done |
568 |
||
569 |
lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t" |
|
570 |
-- {* Prevents simplification of @{text f} and @{text g}: much faster. *} |
|
20798 | 571 |
by simp |
12918 | 572 |
|
573 |
lemma sum_case_inject: |
|
574 |
"sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P" |
|
575 |
proof - |
|
576 |
assume a: "sum_case f1 f2 = sum_case g1 g2" |
|
577 |
assume r: "f1 = g1 ==> f2 = g2 ==> P" |
|
578 |
show P |
|
579 |
apply (rule r) |
|
580 |
apply (rule ext) |
|
14208 | 581 |
apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp) |
12918 | 582 |
apply (rule ext) |
14208 | 583 |
apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp) |
12918 | 584 |
done |
585 |
qed |
|
586 |
||
13635
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
587 |
constdefs |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
588 |
Suml :: "('a => 'c) => 'a + 'b => 'c" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
589 |
"Suml == (%f. sum_case f arbitrary)" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
590 |
|
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
591 |
Sumr :: "('b => 'c) => 'a + 'b => 'c" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
592 |
"Sumr == sum_case arbitrary" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
593 |
|
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
594 |
lemma Suml_inject: "Suml f = Suml g ==> f = g" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
595 |
by (unfold Suml_def) (erule sum_case_inject) |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
596 |
|
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
597 |
lemma Sumr_inject: "Sumr f = Sumr g ==> f = g" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
598 |
by (unfold Sumr_def) (erule sum_case_inject) |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
599 |
|
20798 | 600 |
hide (open) const Suml Sumr |
13635
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
601 |
|
12918 | 602 |
|
603 |
subsection {* Further cases/induct rules for tuples *} |
|
11954 | 604 |
|
20798 | 605 |
lemma prod_cases3 [cases type]: |
606 |
obtains (fields) a b c where "y = (a, b, c)" |
|
607 |
by (cases y, case_tac b) blast |
|
11954 | 608 |
|
609 |
lemma prod_induct3 [case_names fields, induct type]: |
|
610 |
"(!!a b c. P (a, b, c)) ==> P x" |
|
611 |
by (cases x) blast |
|
612 |
||
20798 | 613 |
lemma prod_cases4 [cases type]: |
614 |
obtains (fields) a b c d where "y = (a, b, c, d)" |
|
615 |
by (cases y, case_tac c) blast |
|
11954 | 616 |
|
617 |
lemma prod_induct4 [case_names fields, induct type]: |
|
618 |
"(!!a b c d. P (a, b, c, d)) ==> P x" |
|
619 |
by (cases x) blast |
|
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
620 |
|
20798 | 621 |
lemma prod_cases5 [cases type]: |
622 |
obtains (fields) a b c d e where "y = (a, b, c, d, e)" |
|
623 |
by (cases y, case_tac d) blast |
|
11954 | 624 |
|
625 |
lemma prod_induct5 [case_names fields, induct type]: |
|
626 |
"(!!a b c d e. P (a, b, c, d, e)) ==> P x" |
|
627 |
by (cases x) blast |
|
628 |
||
20798 | 629 |
lemma prod_cases6 [cases type]: |
630 |
obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)" |
|
631 |
by (cases y, case_tac e) blast |
|
11954 | 632 |
|
633 |
lemma prod_induct6 [case_names fields, induct type]: |
|
634 |
"(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" |
|
635 |
by (cases x) blast |
|
636 |
||
20798 | 637 |
lemma prod_cases7 [cases type]: |
638 |
obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)" |
|
639 |
by (cases y, case_tac f) blast |
|
11954 | 640 |
|
641 |
lemma prod_induct7 [case_names fields, induct type]: |
|
642 |
"(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" |
|
643 |
by (cases x) blast |
|
5759 | 644 |
|
12918 | 645 |
|
646 |
subsection {* The option type *} |
|
647 |
||
648 |
datatype 'a option = None | Some 'a |
|
649 |
||
20798 | 650 |
lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)" |
18576 | 651 |
by (induct x) auto |
652 |
||
20798 | 653 |
lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)" |
18447 | 654 |
by (induct x) auto |
655 |
||
18576 | 656 |
text{*Although it may appear that both of these equalities are helpful |
657 |
only when applied to assumptions, in practice it seems better to give |
|
658 |
them the uniform iff attribute. *} |
|
12918 | 659 |
|
660 |
lemma option_caseE: |
|
20798 | 661 |
assumes c: "(case x of None => P | Some y => Q y)" |
662 |
obtains |
|
663 |
(None) "x = None" and P |
|
664 |
| (Some) y where "x = Some y" and "Q y" |
|
665 |
using c by (cases x) simp_all |
|
12918 | 666 |
|
667 |
||
668 |
subsubsection {* Operations *} |
|
669 |
||
670 |
consts |
|
671 |
the :: "'a option => 'a" |
|
672 |
primrec |
|
673 |
"the (Some x) = x" |
|
674 |
||
675 |
consts |
|
676 |
o2s :: "'a option => 'a set" |
|
677 |
primrec |
|
678 |
"o2s None = {}" |
|
679 |
"o2s (Some x) = {x}" |
|
680 |
||
681 |
lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x" |
|
682 |
by simp |
|
683 |
||
17876 | 684 |
ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *} |
12918 | 685 |
|
686 |
lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)" |
|
687 |
by (cases xo) auto |
|
688 |
||
689 |
lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)" |
|
690 |
by (cases xo) auto |
|
691 |
||
692 |
||
693 |
constdefs |
|
694 |
option_map :: "('a => 'b) => ('a option => 'b option)" |
|
695 |
"option_map == %f y. case y of None => None | Some x => Some (f x)" |
|
696 |
||
697 |
lemma option_map_None [simp]: "option_map f None = None" |
|
698 |
by (simp add: option_map_def) |
|
699 |
||
700 |
lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)" |
|
701 |
by (simp add: option_map_def) |
|
702 |
||
20798 | 703 |
lemma option_map_is_None [iff]: |
704 |
"(option_map f opt = None) = (opt = None)" |
|
705 |
by (simp add: option_map_def split add: option.split) |
|
14187 | 706 |
|
12918 | 707 |
lemma option_map_eq_Some [iff]: |
708 |
"(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)" |
|
20798 | 709 |
by (simp add: option_map_def split add: option.split) |
14187 | 710 |
|
711 |
lemma option_map_comp: |
|
20798 | 712 |
"option_map f (option_map g opt) = option_map (f o g) opt" |
713 |
by (simp add: option_map_def split add: option.split) |
|
12918 | 714 |
|
715 |
lemma option_map_o_sum_case [simp]: |
|
716 |
"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)" |
|
20798 | 717 |
by (rule ext) (simp split: sum.split) |
12918 | 718 |
|
19787 | 719 |
|
21111 | 720 |
subsubsection {* Code generator setup *} |
19817 | 721 |
|
21111 | 722 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21243
diff
changeset
|
723 |
is_none :: "'a option \<Rightarrow> bool" where |
21111 | 724 |
is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None" |
19787 | 725 |
|
21111 | 726 |
lemma is_none_code [code]: |
727 |
shows "is_none None \<longleftrightarrow> True" |
|
728 |
and "is_none (Some x) \<longleftrightarrow> False" |
|
729 |
unfolding is_none_none [symmetric] by simp_all |
|
730 |
||
731 |
hide (open) const is_none |
|
19787 | 732 |
|
17458
e42bfad176eb
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
wenzelm
parents:
15140
diff
changeset
|
733 |
lemmas [code] = imp_conv_disj |
e42bfad176eb
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
wenzelm
parents:
15140
diff
changeset
|
734 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
735 |
lemma [code func]: |
19138 | 736 |
"(\<not> True) = False" by (rule HOL.simp_thms) |
737 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
738 |
lemma [code func]: |
19138 | 739 |
"(\<not> False) = True" by (rule HOL.simp_thms) |
740 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
741 |
lemma [code func]: |
19179
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
742 |
shows "(False \<and> x) = False" |
20798 | 743 |
and "(True \<and> x) = x" |
744 |
and "(x \<and> False) = False" |
|
745 |
and "(x \<and> True) = x" by simp_all |
|
19138 | 746 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
747 |
lemma [code func]: |
19179
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
748 |
shows "(False \<or> x) = x" |
20798 | 749 |
and "(True \<or> x) = True" |
750 |
and "(x \<or> False) = x" |
|
751 |
and "(x \<or> True) = True" by simp_all |
|
19138 | 752 |
|
753 |
declare |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
754 |
if_True [code func] |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
755 |
if_False [code func] |
19179
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
756 |
fst_conv [code] |
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
757 |
snd_conv [code] |
19138 | 758 |
|
20105 | 759 |
lemma split_is_prod_case [code inline]: |
20798 | 760 |
"split = prod_case" |
761 |
by (simp add: expand_fun_eq split_def prod.cases) |
|
20105 | 762 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
763 |
code_type bool |
21111 | 764 |
(SML "bool") |
765 |
(Haskell "Bool") |
|
19138 | 766 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
767 |
code_const True and False and Not and "op &" and "op |" and If |
21111 | 768 |
(SML "true" and "false" and "not" |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
769 |
and infixl 1 "andalso" and infixl 0 "orelse" |
21126 | 770 |
and "!(if (_)/ then (_)/ else (_))") |
21111 | 771 |
(Haskell "True" and "False" and "not" |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
772 |
and infixl 3 "&&" and infixl 2 "||" |
21126 | 773 |
and "!(if (_)/ then (_)/ else (_))") |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
774 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
775 |
code_type * |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
776 |
(SML infix 2 "*") |
21126 | 777 |
(Haskell "!((_),/ (_))") |
19138 | 778 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
779 |
code_const Pair |
21126 | 780 |
(SML "!((_),/ (_))") |
781 |
(Haskell "!((_),/ (_))") |
|
18702 | 782 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
783 |
code_type unit |
21111 | 784 |
(SML "unit") |
785 |
(Haskell "()") |
|
19150 | 786 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
787 |
code_const Unity |
21111 | 788 |
(SML "()") |
789 |
(Haskell "()") |
|
19150 | 790 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
791 |
code_type option |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
792 |
(SML "_ option") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
793 |
(Haskell "Maybe _") |
19150 | 794 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
795 |
code_const None and Some |
21111 | 796 |
(SML "NONE" and "SOME") |
797 |
(Haskell "Nothing" and "Just") |
|
19150 | 798 |
|
20588 | 799 |
code_instance option :: eq |
800 |
(Haskell -) |
|
801 |
||
21454 | 802 |
code_const "op = \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool" |
20588 | 803 |
(Haskell infixl 4 "==") |
804 |
||
21079 | 805 |
code_reserved SML |
806 |
bool true false not unit option NONE SOME |
|
807 |
||
808 |
code_reserved Haskell |
|
809 |
Bool True False not Maybe Nothing Just |
|
810 |
||
21669 | 811 |
|
812 |
subsection {* Basic ML bindings *} |
|
813 |
||
814 |
ML {* |
|
815 |
val not_None_eq = thm "not_None_eq"; |
|
816 |
val not_Some_eq = thm "not_Some_eq"; |
|
20819 | 817 |
*} |
818 |
||
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
819 |
end |