equal
deleted
inserted
replaced
|
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 |