author | paulson |
Tue, 21 May 2002 13:06:36 +0200 | |
changeset 13168 | afcbca3498b0 |
parent 12610 | 8b9845807f77 |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
12610 | 1 |
(* Title: ZF/Induct/Datatypes.thy |
12194
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
4 |
Copyright 1994 University of Cambridge |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
5 |
*) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
6 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
7 |
header {* Sample datatype definitions *} |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
8 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
9 |
theory Datatypes = Main: |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
10 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
11 |
subsection {* A type with four constructors *} |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
12 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
13 |
text {* |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
14 |
It has four contructors, of arities 0--3, and two parameters @{text |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
15 |
A} and @{text B}. |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
16 |
*} |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
17 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
18 |
consts |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
19 |
data :: "[i, i] => i" |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
20 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
21 |
datatype "data(A, B)" = |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
22 |
Con0 |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
23 |
| Con1 ("a \<in> A") |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
24 |
| Con2 ("a \<in> A", "b \<in> B") |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
25 |
| Con3 ("a \<in> A", "b \<in> B", "d \<in> data(A, B)") |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
26 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
27 |
lemma data_unfold: "data(A, B) = ({0} + A) + (A \<times> B + A \<times> B \<times> data(A, B))" |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
28 |
by (fast intro!: data.intros [unfolded data.con_defs] |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
29 |
elim: data.cases [unfolded data.con_defs]) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
30 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
31 |
text {* |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
32 |
\medskip Lemmas to justify using @{term data} in other recursive |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
33 |
type definitions. |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
34 |
*} |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
35 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
36 |
lemma data_mono: "[| A \<subseteq> C; B \<subseteq> D |] ==> data(A, B) \<subseteq> data(C, D)" |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
37 |
apply (unfold data.defs) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
38 |
apply (rule lfp_mono) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
39 |
apply (rule data.bnd_mono)+ |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
40 |
apply (rule univ_mono Un_mono basic_monos | assumption)+ |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
41 |
done |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
42 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
43 |
lemma data_univ: "data(univ(A), univ(A)) \<subseteq> univ(A)" |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
44 |
apply (unfold data.defs data.con_defs) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
45 |
apply (rule lfp_lowerbound) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
46 |
apply (rule_tac [2] subset_trans [OF A_subset_univ Un_upper1, THEN univ_mono]) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
47 |
apply (fast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
48 |
done |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
49 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
50 |
lemma data_subset_univ: |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
51 |
"[| A \<subseteq> univ(C); B \<subseteq> univ(C) |] ==> data(A, B) \<subseteq> univ(C)" |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
52 |
by (rule subset_trans [OF data_mono data_univ]) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
53 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
54 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
55 |
subsection {* Example of a big enumeration type *} |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
56 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
57 |
text {* |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
58 |
Can go up to at least 100 constructors, but it takes nearly 7 |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
59 |
minutes \dots\ (back in 1994 that is). |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
60 |
*} |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
61 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
62 |
consts |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
63 |
enum :: i |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
64 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
65 |
datatype enum = |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
66 |
C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09 |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
67 |
| C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19 |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
68 |
| C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29 |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
69 |
| C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39 |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
70 |
| C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49 |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
71 |
| C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59 |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
72 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
73 |
end |