author | nipkow |
Sun, 04 Nov 2018 12:07:24 +0100 | |
changeset 69232 | 2b913054a9cf |
parent 65449 | c82e63b11b8b |
child 69593 | 3dda49e08b9d |
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 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
3 |
Copyright 1994 University of Cambridge |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
4 |
*) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
5 |
|
60770 | 6 |
section \<open>Sample datatype definitions\<close> |
12194
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
7 |
|
65449
c82e63b11b8b
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents:
61798
diff
changeset
|
8 |
theory Datatypes imports ZF begin |
12194
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
9 |
|
60770 | 10 |
subsection \<open>A type with four constructors\<close> |
12194
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
11 |
|
60770 | 12 |
text \<open> |
61798 | 13 |
It has four contructors, of arities 0--3, and two parameters \<open>A\<close> and \<open>B\<close>. |
60770 | 14 |
\<close> |
12194
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
15 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
16 |
consts |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
17 |
data :: "[i, i] => i" |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
18 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
19 |
datatype "data(A, B)" = |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
20 |
Con0 |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
21 |
| Con1 ("a \<in> A") |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
22 |
| Con2 ("a \<in> A", "b \<in> B") |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
23 |
| 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
|
24 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
25 |
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
|
26 |
by (fast intro!: data.intros [unfolded data.con_defs] |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
27 |
elim: data.cases [unfolded data.con_defs]) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
28 |
|
60770 | 29 |
text \<open> |
12194
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
30 |
\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
|
31 |
type definitions. |
60770 | 32 |
\<close> |
12194
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
33 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
34 |
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
|
35 |
apply (unfold data.defs) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
36 |
apply (rule lfp_mono) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
37 |
apply (rule data.bnd_mono)+ |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
38 |
apply (rule univ_mono Un_mono basic_monos | assumption)+ |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
39 |
done |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
40 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
41 |
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
|
42 |
apply (unfold data.defs data.con_defs) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
43 |
apply (rule lfp_lowerbound) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
44 |
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
|
45 |
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
|
46 |
done |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
47 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
48 |
lemma data_subset_univ: |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
49 |
"[| 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
|
50 |
by (rule subset_trans [OF data_mono data_univ]) |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
51 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
52 |
|
60770 | 53 |
subsection \<open>Example of a big enumeration type\<close> |
12194
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
54 |
|
60770 | 55 |
text \<open> |
12194
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
56 |
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
|
57 |
minutes \dots\ (back in 1994 that is). |
60770 | 58 |
\<close> |
12194
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
59 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
60 |
consts |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
61 |
enum :: i |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
62 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
63 |
datatype enum = |
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
64 |
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
|
65 |
| 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
|
66 |
| 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
|
67 |
| 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
|
68 |
| 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
|
69 |
| 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
|
70 |
|
13909cb72129
converted datatype examples moved from ZF/ex to ZF/Induct;
wenzelm
parents:
diff
changeset
|
71 |
end |