equal
deleted
inserted
replaced
9 imports Plain "~~/src/HOL/Map" |
9 imports Plain "~~/src/HOL/Map" |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Class @{text enum} *} |
12 subsection {* Class @{text enum} *} |
13 |
13 |
14 class enum = itself + |
14 class enum = |
15 fixes enum :: "'a list" |
15 fixes enum :: "'a list" |
16 assumes UNIV_enum [code]: "UNIV = set enum" |
16 assumes UNIV_enum [code]: "UNIV = set enum" |
17 and enum_distinct: "distinct enum" |
17 and enum_distinct: "distinct enum" |
18 begin |
18 begin |
19 |
19 |
20 lemma finite_enum: "finite (UNIV \<Colon> 'a set)" |
20 subclass finite proof |
21 unfolding UNIV_enum .. |
21 qed (simp add: UNIV_enum) |
22 |
22 |
23 lemma enum_all: "set enum = UNIV" unfolding UNIV_enum .. |
23 lemma enum_all: "set enum = UNIV" unfolding UNIV_enum .. |
24 |
24 |
25 lemma in_enum [intro]: "x \<in> set enum" |
25 lemma in_enum [intro]: "x \<in> set enum" |
26 unfolding enum_all by auto |
26 unfolding enum_all by auto |