equal
deleted
inserted
replaced
1 (* Title: ZF/Induct/Datatypes.thy |
1 (* Title: ZF/Induct/Datatypes.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 1994 University of Cambridge |
3 Copyright 1994 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section {* Sample datatype definitions *} |
6 section \<open>Sample datatype definitions\<close> |
7 |
7 |
8 theory Datatypes imports Main begin |
8 theory Datatypes imports Main begin |
9 |
9 |
10 subsection {* A type with four constructors *} |
10 subsection \<open>A type with four constructors\<close> |
11 |
11 |
12 text {* |
12 text \<open> |
13 It has four contructors, of arities 0--3, and two parameters @{text |
13 It has four contructors, of arities 0--3, and two parameters @{text |
14 A} and @{text B}. |
14 A} and @{text B}. |
15 *} |
15 \<close> |
16 |
16 |
17 consts |
17 consts |
18 data :: "[i, i] => i" |
18 data :: "[i, i] => i" |
19 |
19 |
20 datatype "data(A, B)" = |
20 datatype "data(A, B)" = |
25 |
25 |
26 lemma data_unfold: "data(A, B) = ({0} + A) + (A \<times> B + A \<times> B \<times> data(A, B))" |
26 lemma data_unfold: "data(A, B) = ({0} + A) + (A \<times> B + A \<times> B \<times> data(A, B))" |
27 by (fast intro!: data.intros [unfolded data.con_defs] |
27 by (fast intro!: data.intros [unfolded data.con_defs] |
28 elim: data.cases [unfolded data.con_defs]) |
28 elim: data.cases [unfolded data.con_defs]) |
29 |
29 |
30 text {* |
30 text \<open> |
31 \medskip Lemmas to justify using @{term data} in other recursive |
31 \medskip Lemmas to justify using @{term data} in other recursive |
32 type definitions. |
32 type definitions. |
33 *} |
33 \<close> |
34 |
34 |
35 lemma data_mono: "[| A \<subseteq> C; B \<subseteq> D |] ==> data(A, B) \<subseteq> data(C, D)" |
35 lemma data_mono: "[| A \<subseteq> C; B \<subseteq> D |] ==> data(A, B) \<subseteq> data(C, D)" |
36 apply (unfold data.defs) |
36 apply (unfold data.defs) |
37 apply (rule lfp_mono) |
37 apply (rule lfp_mono) |
38 apply (rule data.bnd_mono)+ |
38 apply (rule data.bnd_mono)+ |
49 lemma data_subset_univ: |
49 lemma data_subset_univ: |
50 "[| A \<subseteq> univ(C); B \<subseteq> univ(C) |] ==> data(A, B) \<subseteq> univ(C)" |
50 "[| A \<subseteq> univ(C); B \<subseteq> univ(C) |] ==> data(A, B) \<subseteq> univ(C)" |
51 by (rule subset_trans [OF data_mono data_univ]) |
51 by (rule subset_trans [OF data_mono data_univ]) |
52 |
52 |
53 |
53 |
54 subsection {* Example of a big enumeration type *} |
54 subsection \<open>Example of a big enumeration type\<close> |
55 |
55 |
56 text {* |
56 text \<open> |
57 Can go up to at least 100 constructors, but it takes nearly 7 |
57 Can go up to at least 100 constructors, but it takes nearly 7 |
58 minutes \dots\ (back in 1994 that is). |
58 minutes \dots\ (back in 1994 that is). |
59 *} |
59 \<close> |
60 |
60 |
61 consts |
61 consts |
62 enum :: i |
62 enum :: i |
63 |
63 |
64 datatype enum = |
64 datatype enum = |