src/ZF/ex/enum.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 71 729fe026c5f3
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
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
lcp@56
     8
Can go up to at least 100 constructors, but it takes nearly 7 minutes...
clasohm@0
     9
*)
clasohm@0
    10
clasohm@0
    11
lcp@56
    12
(*An enumeration type with 60 contructors!  -- takes about 150 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 = [];
lcp@71
    27
  val type_intrs = datatype_intrs
clasohm@0
    28
  val type_elims = []);
clasohm@0
    29
lcp@38
    30
goal Enum.thy "con59 ~= con60";
lcp@56
    31
by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);
clasohm@0
    32
result();
clasohm@0
    33