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