src/ZF/ex/enum.ML
changeset 0 a5a9c433f639
child 7 268f93ab3bc4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/ex/enum.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,33 @@
     1.4 +(*  Title: 	ZF/ex/enum
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Example of a BIG enumeration type
    1.10 +
    1.11 +Can go up to at least 100 constructors, but it takes over 10 minutes...
    1.12 +*)
    1.13 +
    1.14 +
    1.15 +(*An enumeration type with 60 contructors!  -- takes about 214 seconds!*)
    1.16 +fun mk_ids a 0 = []
    1.17 +  | mk_ids a n = a :: mk_ids (bump_string a) (n-1);
    1.18 +
    1.19 +val consts = mk_ids "con1" 60;
    1.20 +
    1.21 +structure Enum = Datatype_Fun
    1.22 + (val thy = Univ.thy;
    1.23 +  val rec_specs = 
    1.24 +      [("enum", "univ(0)",
    1.25 +	  [(consts, "i")])];
    1.26 +  val rec_styp = "i";
    1.27 +  val ext = None
    1.28 +  val sintrs = map (fn const => const ^ " : enum") consts;
    1.29 +  val monos = [];
    1.30 +  val type_intrs = data_typechecks
    1.31 +  val type_elims = []);
    1.32 +
    1.33 +goal Enum.thy "~ con59=con60";
    1.34 +by (SIMP_TAC (ZF_ss addrews Enum.free_iffs) 1);  (*2.3 secs*)
    1.35 +result();
    1.36 +