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
     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 nearly 7 minutes...
     9 *)
    10 
    11 
    12 (*An enumeration type with 60 contructors!  -- takes about 150 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 = datatype_intrs
    28   val type_elims = []);
    29 
    30 goal Enum.thy "con59 ~= con60";
    31 by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);
    32 result();
    33