1(* ---------------------------------------------------------------------*) 2(* Enumerated datatypes. An enumerated type with k constructors is *) 3(* represented by the natural numbers < k. *) 4(* ---------------------------------------------------------------------*) 5 6structure EnumType :> EnumType = 7struct 8 9open HolKernel boolLib Parse numLib; 10 11type tyinfo = TypeBasePure.tyinfo; 12 13val ERR = mk_HOL_ERR "EnumType"; 14val NUM = num; 15 16(* Fix the grammar used by this file *) 17val ambient_grammars = Parse.current_grammars(); 18val _ = Parse.temp_set_grammars arithmeticTheory.arithmetic_grammars; 19 20fun enum_pred k = 21 let val n = mk_var("n",num) 22 val topnum = term_of_int k 23 in mk_abs(n,mk_less(n,topnum)) 24 end; 25 26fun type_exists k = 27 let val n = mk_var("n",num) 28 in prove (mk_exists(n, mk_comb(enum_pred k, n)), 29 EXISTS_TAC zero_tm THEN REDUCE_TAC) 30 end 31 32fun num_values REP_ABS defs = 33 let val len = length defs 34 val top_numeral = term_of_int len 35 fun rep_of def = 36 let val n = rand(rhs(concl def)) 37 val less_thm = EQT_ELIM (REDUCE_CONV (mk_less(n,top_numeral))) 38 val thm = EQ_MP (SPEC n REP_ABS) less_thm 39 in SUBS [SYM def] thm 40 end 41 in 42 map rep_of defs 43 end; 44 45(* ---------------------------------------------------------------------- 46 Prove the datatype's cases theorem. I.e., 47 !a. (a = c1) \/ (a = c2) \/ ... (a = cn) 48 ---------------------------------------------------------------------- *) 49 50(* first need a simple lemma: *) 51val n_less_cases = prove( 52 Term`!m n. n < m = ~(m = 0) /\ (let x = m - 1 in n < x \/ (n = x))`, 53 REWRITE_TAC [LET_THM] THEN BETA_TAC THEN CONV_TAC numLib.ARITH_CONV); 54 55fun onestep thm = let 56 (* thm of form x < n, where n is a non-zero numeral *) 57 val (x,n) = dest_less (concl thm) 58 val thm0 = SPECL [n,x] n_less_cases 59 val thm1 = EQ_MP thm0 thm 60in 61 CONV_RULE numLib.REDUCE_CONV thm1 62end 63 64fun prove_cases_thm repthm eqns = let 65 (* repthm of form !a. ?n. (a = f n) /\ (n < x) *) 66 val (avar, spec_rep_t) = dest_forall (concl repthm) 67 val (nvar, rep_body_t) = dest_exists spec_rep_t 68 val ass_rep_body = ASSUME rep_body_t 69 val (aeq_thm, nlt_thm) = CONJ_PAIR ass_rep_body 70 (* aeq_thm is of the form |- a = f n *) 71 val repfn = rator (rand (concl aeq_thm)) 72 fun prove_cases nlt_thm eqns = let 73 (* nlt_thm is of the form |- n < x where x is non-zero *) 74 (* eqns are of the form |- d = f m for various d and decreasing m *) 75 (* the first m is x - 1 *) 76 fun prove_aeq neq eqn = let 77 (* neq is of the form n = x *) 78 (* eqn is of the form d = f x *) 79 val fn_eq_fx = AP_TERM repfn neq 80 in 81 TRANS aeq_thm (TRANS fn_eq_fx (SYM eqn)) 82 end 83 val ndisj_thm = onestep nlt_thm 84 val ndisj_t = concl ndisj_thm 85 in 86 if is_disj ndisj_t then let 87 (* recursive case *) 88 val (new_lt_t, eq_t) = dest_disj ndisj_t 89 val eq_thm = prove_aeq (ASSUME eq_t) (hd eqns) 90 val eq_t = concl eq_thm 91 val lt_thm = prove_cases (ASSUME new_lt_t) (tl eqns) 92 val lt_t = concl lt_thm 93 in 94 DISJ_CASES ndisj_thm (DISJ1 lt_thm eq_t) (DISJ2 lt_t eq_thm) 95 end 96 else 97 (* ndisjthm is |- n = 0 (base case) *) 98 prove_aeq ndisj_thm (hd eqns) 99 end 100in 101 REWRITE_RULE [GSYM DISJ_ASSOC] 102 (GEN avar (CHOOSE (nvar, SPEC avar repthm) (prove_cases nlt_thm eqns))) 103end 104 105(* ---------------------------------------------------------------------- 106 Prove a datatype's induction theorem 107 ---------------------------------------------------------------------- *) 108 109fun prove_induction_thm cases_thm = let 110 val (avar, cases_body) = dest_forall (concl cases_thm) 111 val body_cases_thm = SPEC avar cases_thm 112 val Pvar = mk_var("P", type_of avar --> bool) 113 fun basecase eqthm = let 114 (* eqthm of form |- a = c *) 115 val ass_P = ASSUME (mk_comb(Pvar, rand (concl eqthm))) 116 in 117 EQ_MP (SYM (AP_TERM Pvar eqthm)) ass_P 118 end 119 fun recurse thm = let 120 val (d1, d2) = dest_disj (concl thm) 121 in 122 DISJ_CASES thm (basecase (ASSUME d1)) (recurse (ASSUME d2)) 123 end handle HOL_ERR _ => basecase thm 124 val base_thm = GEN avar (recurse body_cases_thm) 125 val hyp_thm = ASSUME (list_mk_conj (hyp base_thm)) 126 fun foldfn (ass,th) = PROVE_HYP ass th 127in 128 GEN Pvar (DISCH_ALL (foldl foldfn base_thm (CONJUNCTS hyp_thm))) 129end 130 131(* ---------------------------------------------------------------------- 132 Make a size definition for an enumerated type (everywhere zero) 133 ---------------------------------------------------------------------- *) 134 135fun mk_size_definition ty = 136 let val tyname = #1 (dest_type ty) 137 val cname = tyname^"_size" 138 val var_t = mk_var(cname, ty --> NUM) 139 val avar = mk_var("x", ty) 140 val def = new_definition(cname^"_def", 141 mk_eq(mk_comb(var_t, avar), zero_tm)) 142 in 143 SOME (rator (lhs (#2 (strip_forall (concl def)))), TypeBasePure.ORIG def) 144 end 145 146(* ---------------------------------------------------------------------- 147 Prove distinctness theorem for an enumerated type 148 (only done if there are not too many possibilities as there will 149 be n-squared many of these) 150 ---------------------------------------------------------------------- *) 151 152fun gen_triangle l = let 153 (* generate the upper triangle of the cross product of the list with *) 154 (* itself. Leave out the diagonal *) 155 fun gen_row i [] acc = acc 156 | gen_row i (h::t) acc = gen_row i t ((i,h)::acc) 157 fun doitall [] acc = acc 158 | doitall (h::t) acc = doitall t (gen_row h t acc) 159in 160 List.rev (doitall l []) 161end 162 163fun prove_distinctness_thm simpls constrs = 164 let val upper_triangle = gen_triangle constrs 165 fun prove_inequality (c1, c2) = 166 (REWRITE_CONV simpls THENC numLib.REDUCE_CONV) (mk_eq(c1,c2)) 167 in 168 if null upper_triangle then NONE else 169 SOME (LIST_CONJ (map (EQF_ELIM o prove_inequality) upper_triangle)) 170 end 171 172(* ---------------------------------------------------------------------- 173 Prove initiality theorem for type 174 ---------------------------------------------------------------------- *) 175 176fun alphavar n = mk_var("x"^Int.toString n, alpha) 177 178local 179 val n = mk_var("n", NUM) 180in 181fun prove_initiality_thm rep ty constrs simpls = let 182 val ncases = length constrs 183 184 fun generate_ntree lo hi = 185 (* invariant: lo <= hi *) 186 if lo = hi then alphavar lo 187 else let 188 val midpoint = (lo + hi) div 2 189 val ltree = generate_ntree lo midpoint 190 val rtree = generate_ntree (midpoint + 1) hi 191 in 192 mk_cond (mk_leq(n, term_of_int midpoint), ltree, rtree) 193 end 194 195 val witness = let 196 val x = mk_var("x", ty) 197 val body = generate_ntree 0 (ncases - 1) 198 in 199 mk_abs(x, mk_let(mk_abs(n, body), mk_comb(rep, x))) 200 end 201 202 fun prove_clause (n, constr) = 203 EQT_ELIM 204 ((LAND_CONV BETA_CONV THENC REWRITE_CONV simpls THENC 205 numLib.REDUCE_CONV) 206 (mk_eq(mk_comb(witness, constr), alphavar n))) 207 208 fun gen_clauses (_, []) = [] 209 | gen_clauses (n, (h::t)) = prove_clause (n, h) :: gen_clauses (n + 1, t) 210 211 val clauses_thm = LIST_CONJ (gen_clauses (0, constrs)) 212 val f = mk_var("f", ty --> alpha) 213 val clauses = subst [witness |-> f] (concl clauses_thm) 214 215 val exists_thm = EXISTS(mk_exists(f, clauses), witness) clauses_thm 216 217 fun gen_it n th = if n < 0 then th 218 else gen_it (n - 1) (GEN (alphavar n) th) 219in 220 gen_it (ncases - 1) exists_thm 221end; 222 223end (* local *) 224 225 226(*---------------------------------------------------------------------------*) 227(* The main entrypoints *) 228(*---------------------------------------------------------------------------*) 229 230fun define_enum_type(name,clist,ABS,REP) = 231 let val tydef = new_type_definition(name, type_exists (length clist)) 232 val bij = define_new_type_bijections 233 {ABS=ABS, REP=REP,name=name^"_BIJ", tyax=tydef} 234 val ABS_REP = save_thm(ABS^"_"^REP, CONJUNCT1 bij) 235 val REP_ABS = save_thm(REP^"_"^ABS, BETA_RULE (CONJUNCT2 bij)) 236 val ABS_11 = save_thm(ABS^"_11", BETA_RULE (prove_abs_fn_one_one bij)) 237 val REP_11 = save_thm(REP^"_11", BETA_RULE (prove_rep_fn_one_one bij)) 238 val ABS_ONTO = save_thm(ABS^"_ONTO", BETA_RULE (prove_abs_fn_onto bij)) 239 val REP_ONTO = save_thm(REP^"_ONTO", BETA_RULE (prove_rep_fn_onto bij)) 240 val TYPE = type_of(fst(dest_forall(concl REP_11))) 241 val ABSconst = mk_const(ABS, NUM --> TYPE) 242 val REPconst = mk_const(REP, TYPE --> NUM) 243 val nclist = enumerate 0 clist 244 fun def(n,s) = (temp_binding (s ^ "_def"), 245 mk_eq(mk_var(s,TYPE), 246 mk_comb(ABSconst,term_of_int n))) 247 val defs = map (new_definition o def) nclist 248 val constrs = map (lhs o concl) defs 249 in 250 {TYPE = TYPE, 251 constrs = constrs, 252 defs = defs, 253 ABSconst = ABSconst, 254 REPconst = REPconst, 255 ABS_REP = ABS_REP, 256 REP_ABS = REP_ABS, 257 ABS_11 = ABS_11, 258 REP_11 = REP_11, 259 ABS_ONTO = ABS_ONTO, 260 REP_ONTO = REP_ONTO 261 } 262 end; 263 264val (COND_T, COND_F) = CONJ_PAIR (SPEC_ALL COND_CLAUSES) 265fun define_case (type_name, rep_t, rep_th, constrs) = let 266 val sz = length constrs 267 val m = mk_var("m", numSyntax.num) 268 fun V n = mk_var("v" ^ Int.toString n, alpha) 269 open numSyntax 270 fun mk_decision_tree lo hi = 271 if lo < hi then 272 if lo + 1 = hi then 273 mk_cond(mk_eq(m, mk_numeral (Arbnum.fromInt lo)), 274 V lo, V hi) 275 else let 276 val mid = (lo + hi) div 2 277 in 278 mk_cond(mk_less(m, mk_numeral (Arbnum.fromInt mid)), 279 mk_decision_tree lo (mid - 1), 280 mk_decision_tree mid hi) 281 end 282 else if lo = hi then V lo 283 else raise Fail "can't happen 101" 284 val (ty, _) = dom_rng (type_of rep_t) 285 val case_const_name = case_constant_name{type_name = type_name} 286 val case_t = mk_var(case_const_name, 287 ty --> list_mk_fun(List.tabulate(sz, K alpha), alpha)) 288 val args = List.tabulate(sz, (fn n => mk_var("v" ^ Int.toString n, 289 alpha))) 290 val e_t = mk_var("x", ty) 291 val def_t = mk_eq(list_mk_comb(case_t, e_t::args), 292 mk_comb(mk_abs(m, mk_decision_tree 0 (sz - 1)), 293 mk_comb(rep_t, e_t))) 294 val def_th = new_definition(case_const_name, def_t) 295 val bare_def_th = SPEC_ALL def_th 296 fun mk_consequence e = let 297 val th = INST [e_t |-> e] bare_def_th 298 val th = CONV_RULE (RAND_CONV (RAND_CONV (REWRITE_CONV [rep_th]) THENC 299 BETA_CONV)) th 300 fun follow_conds t = 301 if is_cond t then 302 (RATOR_CONV (RATOR_CONV (RAND_CONV (numLib.REDUCE_CONV))) THENC 303 (REWR_CONV COND_T ORELSEC REWR_CONV COND_F) THENC follow_conds) t 304 else ALL_CONV t 305 in 306 GENL args (CONV_RULE (RAND_CONV follow_conds) th) 307 end 308in 309 save_thm(case_constant_defn_name {type_name = type_name}, 310 LIST_CONJ (map mk_consequence constrs)) 311end 312 313fun enum_eq_CONV repth = 314 let 315 val r_rwts = repth |> CONJUNCTS 316 val r_t = r_rwts |> hd |> concl |> lhs |> strip_comb |> #1 317 val (d_ty, _) = dom_rng (type_of r_t) 318 fun cnv t = 319 let 320 val reqn = AP_TERM r_t (ASSUME t) 321 val (r1, r2) = dest_eq (concl reqn) 322 val rth = FIRST_CONV (map REWR_CONV r_rwts) 323 val r1th = rth r1 and r2th = rth r2 324 val num_eqn = TRANS (SYM r1th) (TRANS reqn r2th) 325 val falsity = CONV_RULE numLib.REDUCE_CONV num_eqn 326 in 327 DISCH_ALL falsity |> EQ_MP (SPEC t boolTheory.IMP_F_EQ_F) 328 end 329 fun finalconv _ _ t = 330 let 331 (* keying will have already ensured that t is an equality between two 332 values in the enumerated type *) 333 val (l, r) = boolSyntax.dest_eq t 334 in 335 if Term.is_const l andalso Term.is_const r andalso 336 type_of l = d_ty 337 then cnv t 338 else raise ERR "enum_eq_CONV" 339 "Equality not between constants of right type" 340 end 341 in 342 {name = #1 (dest_type d_ty) ^ "_enum_neq_conv", 343 key = SOME ([], mk_eq(mk_var("x", d_ty), mk_var("y", d_ty))), 344 trace = 2, 345 conv = finalconv} : simpfrag.convdata 346 end 347 348val _ = simpfrag.register_simpfrag_conv {name = "EnumType", code = enum_eq_CONV} 349 350fun enum_type_to_tyinfo (ty, clist) = let 351 val abs = "num2" ^ ty 352 val rep = ty ^ "2num" 353 val (result as {constrs,TYPE,...}) = define_enum_type (ty,clist,abs,rep) 354 val abs_name = abs ^ "_thm" 355 val abs_thm = save_thm (abs_name, LIST_CONJ (map SYM (#defs result))) 356 val rep_name = rep ^ "_thm" 357 val rep_thm = save_thm (rep_name, 358 LIST_CONJ (num_values (#REP_ABS result) (#defs result))) 359 val eq_elim_name = ty ^ "_EQ_" ^ ty 360 val eq_elim_th = save_thm (eq_elim_name, GSYM (#REP_11 result)) 361 val simpls = [rep_thm, eq_elim_th] 362 val nchotomy = prove_cases_thm (#ABS_ONTO result) (List.rev (#defs result)) 363 val induction = prove_induction_thm nchotomy 364 val size = mk_size_definition TYPE 365 val distinct = if length constrs > 15 then NONE 366 else prove_distinctness_thm simpls constrs 367 val initiality = prove_initiality_thm (#REPconst result) TYPE constrs simpls 368 val rep_t = rator (lhs (hd (strip_conj (concl rep_thm)))) 369 val case_def = define_case (ty, rep_t, rep_thm, constrs) 370 val case_cong = Prim_rec.case_cong_thm nchotomy case_def 371 fun add_rewrs l tyi = 372 let 373 val {convs, rewrs} = TypeBasePure.simpls_of tyi 374 in 375 TypeBasePure.put_simpls {convs=convs, rewrs = rewrs @ l} tyi 376 end 377 378 val tyinfo0 = 379 TypeBasePure.mk_datatype_info 380 {ax = TypeBasePure.ORIG initiality, 381 induction = TypeBasePure.ORIG induction, 382 case_def = case_def, 383 case_cong = case_cong, 384 case_eq = 385 Prim_rec.prove_case_eq_thm{case_def = case_def, nchotomy = nchotomy}, 386 nchotomy = nchotomy, 387 size = size, 388 encode = NONE, 389 lift = NONE, 390 one_one = NONE, 391 fields = [], 392 accessors = [], 393 updates = [], 394 recognizers = [], 395 destructors = [], 396 distinct = distinct } 397 |> add_rewrs [rep_thm, abs_thm] 398 open ThyDataSexp 399in 400 List.app (fn s => Theory.delete_binding (s ^ "_def")) clist 401 ; Theory.add_ML_dependency "EnumType" 402 ; if isSome distinct then tyinfo0 403 else tyinfo0 404 |> TypeBasePure.add_extra 405 [List [Sym simpfrag.simpfrag_conv_tag, 406 String "EnumType", Thm rep_thm]] 407end 408 409val _ = Parse.temp_set_grammars ambient_grammars 410 411end (* struct *) 412 413(*--------------------------------------------------------------------------- 414 Examples 415 ---------------------------------------------------------------------------*) 416 417(* 418 419val {TYPE,constrs,defs, ABSconst, REPconst, 420 ABS_REP, REP_ABS, ABS_11, REP_11, ABS_ONTO, REP_ONTO} 421 = time define_enum_type 422 ("colour", ["red", "green", "blue", "brown", "white"], 423 "num2colour", "colour2num"); 424 425val initiality = 426 Count.apply (prove_initiality_thm REPconst TYPE constrs) simpls; 427val case_def = Count.apply define_case initiality; 428val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs); 429val case_cong = Count.apply (case_cong_thm nchotomy) case_def; 430 431val {TYPE,constrs,defs, ABSconst, REPconst, 432 ABS_REP, REP_ABS, ABS_11, REP_11, ABS_ONTO, REP_ONTO, simpls} 433 = define_enum_type 434 ("foo", ["B0", "B1", "B2", "B3", "B4", "B5", "B6", "B7", "B8", 435 "B9", "B10", "B11", "B12", "B13", "B14", "B15", "B16", 436 "B17", "B18", "B19", "B20", "B21", "B22", "B23", "B24", 437 "B25", "B26", "B27", "B28", "B29", "B30"], 438 "num2foo", "foo2num"); 439 440val initiality = 441 Count.apply (prove_initiality_thm REPconst TYPE constrs) simpls; 442val case_def = Count.apply define_case initiality; 443val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs); 444val case_cong = Count.apply (case_cong_thm nchotomy) case_def; 445 446val {TYPE,constrs,defs, ABSconst, REPconst, 447 ABS_REP, REP_ABS, ABS_11, REP_11, ABS_ONTO, REP_ONTO, simpls} 448 = define_enum_type 449 ("bar", ["C0", "C1", "C2", "C3", "C4", "C5", "C6", "C7", "C8", 450 "C9", "C10", "C11", "C12", "C13", "C14", "C15", "C16", 451 "C17", "C18", "C19", "C20", "C21", "C22", "C23", "C24", 452 "C25", "C26", "C27", "C28", "C29", "C30", "C31", "C32", 453 "C33", "C34", "C35", "C36", "C37", "C38", "C39", "C40"], 454 "num2bar", "bar2num"); 455val initiality = 456 Count.apply (prove_initiality_thm REPconst TYPE constrs) simpls; 457val case_def = Count.apply define_case initiality; 458val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs); 459val case_cong = Count.apply (case_cong_thm nchotomy) case_def; 460 461 462val {TYPE,constrs,defs, ABSconst, REPconst, 463 ABS_REP, REP_ABS, ABS_11, REP_11, ABS_ONTO, REP_ONTO, simpls} 464 = define_enum_type 465 ("dar", ["D0", "D1", "D2", "D3", "D4", "D5", "D6", "D7", "D8", 466 "D9", "D10", "D11", "D12", "D13", "D14", "D15", "D16", 467 "D17", "D18", "D19", "D20", "D21", "D22", "D23", "D24", 468 "D25", "D26", "D27", "D28", "D29", "D30", "D31", "D32", 469 "D33", "D34", "D35", "D36", "D37", "D38", "D39", "D40", 470 "D41", "D42", "D43", "D44", "D45", "D46", "D47", "D48", 471 "D49", "D50", "D51","D52","D53","D54","D55"], 472 "num2dar", "dar2num"); 473val initiality = 474 Count.apply (prove_initiality_thm REPconst TYPE constrs) simpls; 475val case_def = Count.apply define_case initiality; 476val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs); 477val case_cong = Count.apply (case_cong_thm nchotomy) case_def; 478 479val {TYPE,constrs,defs, ABSconst, REPconst, 480 ABS_REP, REP_ABS, ABS_11, REP_11, ABS_ONTO, REP_ONTO} 481 = Count.apply define_enum_type 482 ("thing", ["a0", "a1", "a2", "a3", "a4", "a5", "a6", "a7", "a8", 483 "a9", "a10", "a11", "a12", "a13", "a14", "a15", "a16", 484 "a17", "a18", "a19", "a20", "a21", "a22", "a23", "a24", 485 "a25", "a26", "a27", "a28", "a29", "a30", "a31", "a32", 486 "a33", "a34", "a35", "a36", "a37", "a38", "a39", "a40", 487 "a41", "a42", "a43", "a44", "a45", "a46", "a47", "a48", 488 "a49", "a50", "a51", "a52", "a53", "a54", "a55", "a56", 489 "a57", "a58", "a59", "a60", "a61", "a62", "a63", "a64"], 490 "num2thing", "thing2num"); 491val initiality = 492 Count.apply (prove_initiality_thm REPconst TYPE constrs) simpls; 493val case_def = Count.apply define_case initiality; 494val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs); 495val case_cong = Count.apply (case_cong_thm nchotomy) case_def; 496 497val {TYPE,constrs,defs, ABSconst, REPconst, 498 ABS_REP, REP_ABS, ABS_11, REP_11, ABS_ONTO, REP_ONTO, simpls} 499 = Count.apply define_enum_type 500 ("thing", ["z0", "z1", "z2", "z3", "z4", "z5", "z6", "z7", "z8", 501 "z9", "z10", "z11", "z12", "z13", "z14", "z15", "z16", 502 "z17", "z18", "z19", "z20", "z21", "z22", "z23", "z24", 503 "z25", "z26", "z27", "z28", "z29", "z30", "z31", "z32", 504 "z33", "z34", "z35", "z36", "z37", "z38", "z39", "z40", 505 "z41", "z42", "z43", "z44", "z45", "z46", "z47", "z48", 506 "z49", "z50", "z51", "z52", "z53", "z54", "z55", "z56", 507 "z57", "z58", "z59", "z60", "z61", "z62", "z63", "z64", 508 "z65", "z66", "z67", "z68", "z69", "z70", "z71", "z72", 509 "z73", "z74", "z75"], 510 "num2thing", "thing2num"); 511 512val initiality = 513 Count.apply (prove_initiality_thm REPconst TYPE constrs) simpls; 514val case_def = Count.apply define_case initiality; 515val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs); 516val case_cong = Count.apply (case_cong_thm nchotomy) case_def; 517 518 519val {TYPE,constrs,defs, ABSconst, REPconst, 520 ABS_REP, REP_ABS, ABS_11, REP_11, ABS_ONTO, REP_ONTO, simpls} 521 = Count.apply define_enum_type 522 ("thing", ["Z0", "Z1", "Z2", "Z3", "Z4", "Z5", "Z6", "Z7", "Z8", 523 "Z9", "Z10", "Z11", "Z12", "Z13", "Z14", "Z15", "Z16", 524 "Z17", "Z18", "Z19", "Z20", "Z21", "Z22", "Z23", "Z24", 525 "Z25", "Z26", "Z27", "Z28", "Z29", "Z30", "Z31", "Z32", 526 "Z33", "Z34", "Z35", "Z36", "Z37", "Z38", "Z39", "Z40", 527 "Z41", "Z42", "Z43", "Z44", "Z45", "Z46", "Z47", "Z48", 528 "Z49", "Z50", "Z51", "Z52", "Z53", "Z54", "Z55", "Z56", 529 "Z57", "Z58", "Z59", "Z60", "Z61", "Z62", "Z63", "Z64", 530 "Z65", "Z66", "Z67", "Z68", "Z69", "Z70", "Z71", "Z72", 531 "Z73", "Z74", "Z75", "Z76", "Z77", "Z78", "Z79", "Z80", 532 "Z81", "Z82", "Z83", "Z84", "Z85", "Z86", "Z87", "Z88", 533 "Z89", "Z90", "Z91", "Z92", "Z93", "Z94", "Z95", "Z96", 534 "Z97", "Z98", "Z99"], 535 "num2thing", "thing2num"); 536 537val initiality = 538 Count.apply (prove_initiality_thm REPconst TYPE constrs) simpls; 539val case_def = Count.apply define_case initiality; 540val nchotomy = Count.apply (prove_cases_thm ABS_ONTO) (rev defs); 541val case_cong = Count.apply (case_cong_thm nchotomy) case_def; 542 543 544fun gen_enum n = let 545 fun recurse acc n = 546 if n <= 0 then [QUOTE (String.concat ("foo = " :: acc))] 547 else recurse (("E"^Int.toString n^ " | ") :: acc) (n - 1) 548in 549 recurse ["E"^Int.toString n] (n - 1) 550end 551 552fun enum_test n = Hol_datatype (gen_enum n) 553 554*) 555