src/ZF/ex/enum.ML

Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
particularly delicate. There is a variable renaming problem in
ramsey.ML/pigeon2_lemma. In some cases, rewriting by typechecking rules
had to be replaced by setsolver type_auto_tac... because only the solver
can instantiate variables.

(*  Title: 	ZF/ex/enum
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Example of a BIG enumeration type

Can go up to at least 100 constructors, but it takes over 10 minutes...
*)


(*An enumeration type with 60 contructors!  -- takes about 214 seconds!*)
fun mk_ids a 0 = []
  | mk_ids a n = a :: mk_ids (bump_string a) (n-1);

val consts = mk_ids "con1" 60;

structure Enum = Datatype_Fun
 (val thy = Univ.thy;
  val rec_specs = 
      [("enum", "univ(0)",
	  [(consts, "i")])];
  val rec_styp = "i";
  val ext = None
  val sintrs = map (fn const => const ^ " : enum") consts;
  val monos = [];
  val type_intrs = data_typechecks
  val type_elims = []);

goal Enum.thy "~ con59=con60";
by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);  (*2.3 secs*)
result();