|
0
|
1 |
(* Title: ZF/ex/enum
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1993 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Example of a BIG enumeration type
|
|
|
7 |
|
|
|
8 |
Can go up to at least 100 constructors, but it takes over 10 minutes...
|
|
|
9 |
*)
|
|
|
10 |
|
|
|
11 |
|
|
|
12 |
(*An enumeration type with 60 contructors! -- takes about 214 seconds!*)
|
|
|
13 |
fun mk_ids a 0 = []
|
|
|
14 |
| mk_ids a n = a :: mk_ids (bump_string a) (n-1);
|
|
|
15 |
|
|
|
16 |
val consts = mk_ids "con1" 60;
|
|
|
17 |
|
|
|
18 |
structure Enum = Datatype_Fun
|
|
|
19 |
(val thy = Univ.thy;
|
|
|
20 |
val rec_specs =
|
|
|
21 |
[("enum", "univ(0)",
|
|
|
22 |
[(consts, "i")])];
|
|
|
23 |
val rec_styp = "i";
|
|
|
24 |
val ext = None
|
|
|
25 |
val sintrs = map (fn const => const ^ " : enum") consts;
|
|
|
26 |
val monos = [];
|
|
|
27 |
val type_intrs = data_typechecks
|
|
|
28 |
val type_elims = []);
|
|
|
29 |
|
|
|
30 |
goal Enum.thy "~ con59=con60";
|
|
|
31 |
by (SIMP_TAC (ZF_ss addrews Enum.free_iffs) 1); (*2.3 secs*)
|
|
|
32 |
result();
|
|
|
33 |
|