1open HolKernel boolLib Prim_rec Parse simpLib boolSimps 2 numTheory prim_recTheory arithmeticTheory InductiveDefinition; 3 4val hol_ss = bool_ss ++ numSimps.old_ARITH_ss ++ numSimps.REDUCE_ss 5 6val lhand = rand o rator 7val AND_FORALL_THM = GSYM FORALL_AND_THM; 8val GEN_REWRITE_TAC = fn c => fn thl => 9 Rewrite.GEN_REWRITE_TAC c Rewrite.empty_rewrites thl 10 11 12val _ = new_theory "ind_type"; 13 14(* ------------------------------------------------------------------------- *) 15(* Abstract left inverses for binary injections (we could construct them...) *) 16(* ------------------------------------------------------------------------- *) 17 18val INJ_INVERSE2 = store_thm( 19 "INJ_INVERSE2", 20 ``!P:'A->'B->'C. 21 (!x1 y1 x2 y2. (P x1 y1 = P x2 y2) = (x1 = x2) /\ (y1 = y2)) ==> 22 ?X Y. !x y. (X(P x y) = x) /\ (Y(P x y) = y)``, 23 GEN_TAC THEN DISCH_TAC THEN 24 Q.EXISTS_TAC `\z:'C. @x:'A. ?y:'B. P x y = z` THEN 25 Q.EXISTS_TAC `\z:'C. @y:'B. ?x:'A. P x y = z` THEN 26 REPEAT GEN_TAC THEN ASM_SIMP_TAC hol_ss []); 27 28(* ------------------------------------------------------------------------- *) 29(* Define an injective pairing function on ":num". *) 30(* ------------------------------------------------------------------------- *) 31 32val NUMPAIR = new_definition( 33 "NUMPAIR", 34 Term`NUMPAIR x y = (2 EXP x) * (2 * y + 1)`); 35 36val NUMPAIR_INJ_LEMMA = store_thm( 37 "NUMPAIR_INJ_LEMMA", 38 ``!x1 y1 x2 y2. (NUMPAIR x1 y1 = NUMPAIR x2 y2) ==> (x1 = x2)``, 39 REWRITE_TAC[NUMPAIR] THEN REPEAT(numLib.INDUCT_TAC THEN GEN_TAC) THEN 40 ASM_SIMP_TAC hol_ss [EXP, GSYM MULT_ASSOC, EQ_MULT_LCANCEL, 41 NOT_SUC, GSYM NOT_SUC, INV_SUC_EQ] THEN 42 TRY (FIRST_ASSUM MATCH_ACCEPT_TAC) THEN 43 DISCH_THEN(MP_TAC o Q.AP_TERM `EVEN`) THEN 44 SIMP_TAC hol_ss [EVEN_MULT, EVEN_ADD]); 45 46val NUMPAIR_INJ = store_thm ( 47 "NUMPAIR_INJ", 48 ``!x1 y1 x2 y2. (NUMPAIR x1 y1 = NUMPAIR x2 y2) = (x1 = x2) /\ (y1 = y2)``, 49 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 50 FIRST_ASSUM(SUBST_ALL_TAC o MATCH_MP NUMPAIR_INJ_LEMMA) THEN 51 POP_ASSUM MP_TAC THEN REWRITE_TAC[NUMPAIR] THEN 52 SIMP_TAC hol_ss [EQ_MULT_LCANCEL, EQ_ADD_RCANCEL, EXP_EQ_0]); 53 54val NUMPAIR_DEST = Rsyntax.new_specification { 55 consts = [{const_name = "NUMFST", fixity = NONE}, 56 {const_name = "NUMSND", fixity = NONE}], 57 name = "NUMPAIR_DEST", 58 sat_thm = MATCH_MP INJ_INVERSE2 NUMPAIR_INJ}; 59 60(* ------------------------------------------------------------------------- *) 61(* Also, an injective map bool->num->num (even easier!) *) 62(* ------------------------------------------------------------------------- *) 63 64val NUMSUM = new_definition("NUMSUM", 65 Term`NUMSUM b x = if b then SUC(2 * x) else 2 * x`); 66 67val NUMSUM_INJ = store_thm( 68 "NUMSUM_INJ", 69 Term`!b1 x1 b2 x2. (NUMSUM b1 x1 = NUMSUM b2 x2) = (b1 = b2) /\ (x1 = x2)`, 70 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 71 POP_ASSUM(MP_TAC o REWRITE_RULE[NUMSUM]) THEN 72 DISCH_THEN(fn th => MP_TAC th THEN MP_TAC(Q.AP_TERM `EVEN` th)) THEN 73 REPEAT COND_CASES_TAC THEN REWRITE_TAC[EVEN, EVEN_DOUBLE] THEN 74 SIMP_TAC hol_ss [INV_SUC_EQ, EQ_MULT_LCANCEL]); 75 76val NUMSUM_DEST = Rsyntax.new_specification{ 77 consts = [{const_name = "NUMLEFT", fixity = NONE}, 78 {const_name = "NUMRIGHT", fixity = NONE}], 79 name = "NUMSUM_DEST", 80 sat_thm = MATCH_MP INJ_INVERSE2 NUMSUM_INJ}; 81 82(* ------------------------------------------------------------------------- *) 83(* Injection num->Z, where Z == num->A->bool. *) 84(* ------------------------------------------------------------------------- *) 85 86val INJN = new_definition( 87 "INJN", 88 Term`INJN (m:num) = \(n:num) (a:'a). n = m`); 89 90val INJN_INJ = store_thm ( 91 "INJN_INJ", 92 ``!n1 n2. (INJN n1 :num->'a->bool = INJN n2) = (n1 = n2)``, 93 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 94 POP_ASSUM(MP_TAC o C Q.AP_THM `n1:num` o REWRITE_RULE[INJN]) THEN 95 DISCH_THEN(MP_TAC o C Q.AP_THM `a:'a`) THEN SIMP_TAC bool_ss []); 96 97(* ------------------------------------------------------------------------- *) 98(* Injection A->Z, where Z == num->A->bool. *) 99(* ------------------------------------------------------------------------- *) 100 101val INJA = new_definition( 102 "INJA", 103 Term`INJA (a:'a) = \(n:num) b. b = a`); 104 105val INJA_INJ = store_thm( 106 "INJA_INJ", 107 ``!a1 a2. (INJA a1 = INJA a2) = (a1:'a = a2)``, 108 REPEAT GEN_TAC THEN SIMP_TAC bool_ss [INJA, FUN_EQ_THM] THEN 109 EQ_TAC THENL [ 110 DISCH_THEN(MP_TAC o Q.SPEC `a1:'a`) THEN REWRITE_TAC[], 111 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[] 112 ]); 113 114(* ------------------------------------------------------------------------- *) 115(* Injection (num->Z)->Z, where Z == num->A->bool. *) 116(* ------------------------------------------------------------------------- *) 117 118val INJF = new_definition( 119 "INJF", 120 Term`INJF (f:num->(num->'a->bool)) = \n. f (NUMFST n) (NUMSND n)`); 121 122val INJF_INJ = store_thm( 123 "INJF_INJ", 124 ``!f1 f2. (INJF f1 :num->'a->bool = INJF f2) = (f1 = f2)``, 125 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 126 REWRITE_TAC[FUN_EQ_THM] THEN 127 MAP_EVERY Q.X_GEN_TAC [`n:num`, `m:num`, `a:'a`] THEN 128 POP_ASSUM(MP_TAC o REWRITE_RULE[INJF]) THEN 129 DISCH_THEN(MP_TAC o C Q.AP_THM `a:'a` o C Q.AP_THM `NUMPAIR n m`) THEN 130 SIMP_TAC bool_ss [NUMPAIR_DEST]); 131 132(* ------------------------------------------------------------------------- *) 133(* Injection Z->Z->Z, where Z == num->A->bool. *) 134(* ------------------------------------------------------------------------- *) 135 136val INJP = new_definition( 137 "INJP", 138 Term`INJP f1 f2:num->'a->bool = 139 \n a. if NUMLEFT n then f1 (NUMRIGHT n) a else f2 (NUMRIGHT n) a`); 140 141val INJP_INJ = store_thm( 142 "INJP_INJ", 143 Term`!(f1:num->'a->bool) f1' f2 f2'. 144 (INJP f1 f2 = INJP f1' f2') = (f1 = f1') /\ (f2 = f2')`, 145 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 146 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 147 SIMP_TAC bool_ss [AND_FORALL_THM] THEN 148 Q.X_GEN_TAC `n:num` THEN POP_ASSUM(MP_TAC o REWRITE_RULE[INJP]) THEN 149 DISCH_THEN(MP_TAC o GEN ``b:bool`` o C Q.AP_THM `NUMSUM b n`) THEN 150 DISCH_THEN(fn th => MP_TAC(Q.SPEC `T` th) THEN MP_TAC(Q.SPEC `F` th)) THEN 151 SIMP_TAC (bool_ss ++ ETA_ss) [NUMSUM_DEST]); 152 153(* ------------------------------------------------------------------------- *) 154(* Now, set up "constructor" and "bottom" element. *) 155(* ------------------------------------------------------------------------- *) 156 157val ZCONSTR = new_definition( 158 "ZCONSTR", 159 ``ZCONSTR c i r :num->'a->bool = 160 INJP (INJN (SUC c)) (INJP (INJA i) (INJF r))``); 161 162val ZBOT = new_definition( 163 "ZBOT", 164 Term`ZBOT = INJP (INJN 0) (@z:num->'a->bool. T)`); 165 166val ZCONSTR_ZBOT = store_thm( 167 "ZCONSTR_ZBOT", 168 Term`!c i r. ~(ZCONSTR c i r :num->'a->bool = ZBOT)`, 169 REWRITE_TAC[ZCONSTR, ZBOT, INJP_INJ, INJN_INJ, NOT_SUC]); 170 171(* ------------------------------------------------------------------------- *) 172(* Carve out an inductively defined set. *) 173(* ------------------------------------------------------------------------- *) 174 175val (ZRECSPACE_RULES,ZRECSPACE_INDUCT,ZRECSPACE_CASES) = 176 IndDefLib.Hol_reln 177 `ZRECSPACE (ZBOT:num->'a->bool) /\ 178 (!c i r. (!n. ZRECSPACE (r n)) ==> ZRECSPACE (ZCONSTR c i r))`; 179 180local fun new_basic_type_definition tyname (mkname, destname) thm = 181 let val (pred, witness) = dest_comb(concl thm) 182 val predty = type_of pred 183 val dom_ty = #1 (dom_rng predty) 184 val x = mk_var("x", dom_ty) 185 val witness_exists = EXISTS 186 (mk_exists(x, mk_comb(pred, x)),witness) thm 187 val tyax = new_type_definition(tyname,witness_exists) 188 val (mk_dest, dest_mk) = CONJ_PAIR(define_new_type_bijections 189 {name=(tyname^"_repfns"), ABS=mkname, REP=destname, tyax=tyax}) 190 in 191 (SPEC_ALL mk_dest, SPEC_ALL dest_mk) 192 end 193in 194val recspace_tydef = 195 new_basic_type_definition "recspace" 196 ("mk_rec","dest_rec") (CONJUNCT1 ZRECSPACE_RULES) 197end; 198 199(* ------------------------------------------------------------------------- *) 200(* Define lifted constructors. *) 201(* ------------------------------------------------------------------------- *) 202 203val BOTTOM = new_definition( 204 "BOTTOM", 205 Term`BOTTOM = mk_rec (ZBOT:num->'a->bool)`); 206 207val CONSTR = new_definition( 208 "CONSTR", 209 Term`CONSTR c i r : 'a recspace = mk_rec (ZCONSTR c i (\n. dest_rec(r n)))`); 210 211(* ------------------------------------------------------------------------- *) 212(* Some lemmas. *) 213(* ------------------------------------------------------------------------- *) 214 215val MK_REC_INJ = store_thm( 216 "MK_REC_INJ", 217 ``!x y. (mk_rec x :'a recspace = mk_rec y) 218 ==> (ZRECSPACE x /\ ZRECSPACE y ==> (x = y))``, 219 REPEAT GEN_TAC THEN DISCH_TAC THEN 220 REWRITE_TAC[snd recspace_tydef] THEN 221 DISCH_THEN(fn th => ONCE_REWRITE_TAC[GSYM th]) THEN 222 ASM_REWRITE_TAC[]); 223 224val DEST_REC_INJ = store_thm( 225 "DEST_REC_INJ", 226 ``!x y. (dest_rec x = dest_rec y) = (x:'a recspace = y)``, 227 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 228 POP_ASSUM(MP_TAC o Q.AP_TERM `mk_rec:(num->'a->bool)->'a recspace`) THEN 229 REWRITE_TAC[fst recspace_tydef]); 230 231(* ------------------------------------------------------------------------- *) 232(* Show that the set is freely inductively generated. *) 233(* ------------------------------------------------------------------------- *) 234 235val CONSTR_BOT = store_thm( 236 "CONSTR_BOT", 237 ``!c i r. ~(CONSTR c i r :'a recspace = BOTTOM)``, 238 REPEAT GEN_TAC THEN REWRITE_TAC[CONSTR, BOTTOM] THEN 239 DISCH_THEN(MP_TAC o MATCH_MP MK_REC_INJ) THEN 240 REWRITE_TAC[ZCONSTR_ZBOT, ZRECSPACE_RULES] THEN 241 MATCH_MP_TAC(CONJUNCT2 ZRECSPACE_RULES) THEN 242 SIMP_TAC bool_ss [fst recspace_tydef, snd recspace_tydef]); 243 244val CONSTR_INJ = store_thm( 245 "CONSTR_INJ", 246 ``!c1 i1 r1 c2 i2 r2. (CONSTR c1 i1 r1 :'a recspace = CONSTR c2 i2 r2) = 247 (c1 = c2) /\ (i1 = i2) /\ (r1 = r2)``, 248 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 249 POP_ASSUM(MP_TAC o REWRITE_RULE[CONSTR]) THEN 250 DISCH_THEN(MP_TAC o MATCH_MP MK_REC_INJ) THEN 251 W(C SUBGOAL_THEN ASSUME_TAC o funpow 2 lhand o snd) THENL [ 252 CONJ_TAC THEN MATCH_MP_TAC(CONJUNCT2 ZRECSPACE_RULES) THEN 253 SIMP_TAC bool_ss [fst recspace_tydef, snd recspace_tydef], 254 ASM_REWRITE_TAC[] THEN REWRITE_TAC[ZCONSTR] THEN 255 REWRITE_TAC[INJP_INJ, INJN_INJ, INJF_INJ, INJA_INJ] THEN 256 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN BETA_TAC THEN 257 REWRITE_TAC[INV_SUC_EQ, DEST_REC_INJ] 258 ]); 259 260val CONSTR_IND = store_thm( 261 "CONSTR_IND", 262 ``!P. P(BOTTOM) /\ 263 (!c i r. (!n. P(r n)) ==> P(CONSTR c i r)) ==> 264 !x:'a recspace. P(x)``, 265 REPEAT STRIP_TAC THEN 266 MP_TAC(Q.SPEC `\z:num->'a->bool. ZRECSPACE(z) /\ P(mk_rec z)` 267 ZRECSPACE_INDUCT) THEN 268 BETA_TAC THEN ASM_REWRITE_TAC[ZRECSPACE_RULES, GSYM BOTTOM] THEN 269 W(C SUBGOAL_THEN ASSUME_TAC o funpow 2 lhand o snd) THENL [ 270 REPEAT GEN_TAC THEN SIMP_TAC bool_ss [FORALL_AND_THM] THEN 271 REPEAT STRIP_TAC THENL [ 272 MATCH_MP_TAC(CONJUNCT2 ZRECSPACE_RULES) THEN ASM_REWRITE_TAC[], 273 FIRST_ASSUM (fn implhs => 274 FIRST_ASSUM (fn imp => (MP_TAC (HO_MATCH_MP imp implhs)))) THEN 275 REWRITE_TAC[CONSTR] THEN 276 RULE_ASSUM_TAC(REWRITE_RULE[snd recspace_tydef]) THEN 277 ASM_SIMP_TAC (bool_ss ++ ETA_ss) [] 278 ], 279 ASM_REWRITE_TAC[] THEN 280 DISCH_THEN(MP_TAC o Q.SPEC `dest_rec (x:'a recspace)`) THEN 281 REWRITE_TAC[fst recspace_tydef] THEN 282 REWRITE_TAC[tautLib.TAUT_PROVE ``(a ==> a /\ b) = (a ==> b)``] THEN 283 DISCH_THEN MATCH_MP_TAC THEN 284 REWRITE_TAC[fst recspace_tydef, snd recspace_tydef] 285 ]);; 286 287(* ------------------------------------------------------------------------- *) 288(* Now prove the recursion theorem (this subcase is all we need). *) 289(* ------------------------------------------------------------------------- *) 290 291val CONSTR_REC = store_thm( 292 "CONSTR_REC", 293 ``!Fn:num->'a->(num->'a recspace)->(num->'b)->'b. 294 ?f. (!c i r. f (CONSTR c i r) = Fn c i r (\n. f (r n)))``, 295 REPEAT STRIP_TAC THEN 296 (MP_TAC o prove_nonschematic_inductive_relations_exist bool_monoset) 297 ``(Z:'a recspace->'b->bool) BOTTOM b /\ 298 (!c i r y. (!n. Z (r n) (y n)) ==> Z (CONSTR c i r) (Fn c i r y))`` THEN 299 DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN 300 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (ASSUME_TAC o GSYM)) THEN 301 Q.SUBGOAL_THEN `!x. ?!y. (Z:'a recspace->'b->bool) x y` MP_TAC THENL [ 302 W(MP_TAC o HO_PART_MATCH rand CONSTR_IND o snd) THEN 303 DISCH_THEN MATCH_MP_TAC THEN CONJ_TAC THEN REPEAT GEN_TAC THENL [ 304 FIRST_ASSUM 305 (fn t => GEN_REWRITE_TAC BINDER_CONV [GSYM t]) THEN 306 REWRITE_TAC[GSYM CONSTR_BOT, EXISTS_UNIQUE_REFL], 307 DISCH_THEN(MP_TAC o SIMP_RULE bool_ss [EXISTS_UNIQUE_THM,FORALL_AND_THM]) 308 THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN 309 DISCH_THEN(MP_TAC o SIMP_RULE bool_ss [SKOLEM_THM]) THEN 310 DISCH_THEN(Q.X_CHOOSE_THEN `y:num->'b` ASSUME_TAC) THEN 311 REWRITE_TAC[EXISTS_UNIQUE_THM] THEN 312 FIRST_ASSUM(fn th => CHANGED_TAC(ONCE_REWRITE_TAC[GSYM th])) THEN 313 CONJ_TAC THENL [ 314 Q.EXISTS_TAC 315 `(Fn:num->'a->(num->'a recspace)->(num->'b)->'b) c i r y` THEN 316 REWRITE_TAC[CONSTR_BOT, CONSTR_INJ, GSYM CONJ_ASSOC] THEN 317 SIMP_TAC hol_ss [RIGHT_EXISTS_AND_THM] THEN 318 Q.EXISTS_TAC `y:num->'b` THEN ASM_REWRITE_TAC[], 319 REWRITE_TAC[CONSTR_BOT, CONSTR_INJ, GSYM CONJ_ASSOC] THEN 320 SIMP_TAC hol_ss [RIGHT_EXISTS_AND_THM] THEN 321 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN 322 REPEAT AP_TERM_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 323 Q.X_GEN_TAC `w:num` THEN FIRST_ASSUM MATCH_MP_TAC THEN 324 Q.EXISTS_TAC `w` THEN ASM_REWRITE_TAC[] 325 ] 326 ], 327 REWRITE_TAC[UNIQUE_SKOLEM_ALT] THEN 328 DISCH_THEN(Q.X_CHOOSE_THEN `fn:'a recspace->'b` (ASSUME_TAC o GSYM)) THEN 329 Q.EXISTS_TAC `fn:'a recspace->'b` THEN ASM_REWRITE_TAC[] THEN 330 REPEAT GEN_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN GEN_TAC THEN 331 FIRST_ASSUM(fn th => GEN_REWRITE_TAC I [GSYM th]) THEN 332 SIMP_TAC bool_ss [] 333 ]); 334 335(* ------------------------------------------------------------------------- *) 336(* The following is useful for coding up functions casewise. *) 337(* ------------------------------------------------------------------------- *) 338 339val FCONS = new_recursive_definition { 340 rec_axiom = num_Axiom, 341 name = "FCONS", 342 def = ``(!a f. FCONS (a:'a) f 0 = a) /\ 343 (!a f n. FCONS (a:'a) f (SUC n) = f n)``}; 344 345val FCONS_UNDO = prove( 346 ``!f:num->'a. f = FCONS (f 0) (f o SUC)``, 347 GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN 348 numLib.INDUCT_TAC THEN REWRITE_TAC[FCONS, combinTheory.o_THM]); 349 350val FNIL = new_definition("FNIL", ``FNIL (n:num) = (ARB:'a)``); 351 352(*---------------------------------------------------------------------------*) 353(* Destructor-style FCONS equation *) 354(*---------------------------------------------------------------------------*) 355 356val FCONS_DEST = Q.store_thm 357("FCONS_DEST", 358 `FCONS a f n = if n = 0 then a else f (n-1)`, 359 BasicProvers.Cases_on `n` THEN ASM_SIMP_TAC numLib.arith_ss [FCONS]); 360 361(* ------------------------------------------------------------------------- *) 362(* Convenient definitions for type isomorphism. *) 363(* ------------------------------------------------------------------------- *) 364 365val ISO = new_definition( 366 "ISO", 367 Term`ISO (f:'a->'b) (g:'b->'a) = (!x. f(g x) = x) /\ (!y. g(f y) = y)`); 368 369(* ------------------------------------------------------------------------- *) 370(* Composition theorems. *) 371(* ------------------------------------------------------------------------- *) 372 373val ISO_REFL = store_thm( 374 "ISO_REFL", 375 Term`ISO (\x:'a. x) (\x. x)`, 376 SIMP_TAC bool_ss [ISO]); 377 378open mesonLib 379val ISO_FUN = store_thm( 380 "ISO_FUN", 381 Term`ISO (f:'a->'c) f' /\ ISO (g:'b->'d) g' ==> 382 ISO (\h a'. g(h(f' a'))) (\h a. g'(h(f a)))`, 383 REWRITE_TAC [ISO] THEN SIMP_TAC bool_ss [ISO, FUN_EQ_THM]); 384 (* bug in the simplifier requires first rewrite to be performed *) 385 386(* ------------------------------------------------------------------------- *) 387(* The use we make of isomorphism when finished. *) 388(* ------------------------------------------------------------------------- *) 389 390val ISO_USAGE = store_thm( 391 "ISO_USAGE", 392 Term`ISO f g ==> 393 (!P. (!x. P x) = (!x. P(g x))) /\ 394 (!P. (?x. P x) = (?x. P(g x))) /\ 395 (!a b. (a = g b) = (f a = b))`, 396 SIMP_TAC bool_ss [ISO, FUN_EQ_THM] THEN MESON_TAC[]); 397 398(* ---------------------------------------------------------------------- 399 Remove constants from top-level name-space 400 ---------------------------------------------------------------------- *) 401 402val _ = app (fn s => remove_ovl_mapping s {Name = s, Thy = "ind_type"}) 403 ["NUMPAIR", "NUMSUM", "INJN", "INJA", "INJF", "INJP", 404 "FCONS", "ZCONSTR", "ZBOT", "BOTTOM", "CONSTR", "FNIL", "ISO"] 405 406local open OpenTheoryMap in 407 val ns = ["HOL4","Datatype"] 408 fun c x = OpenTheory_const_name{const={Thy="ind_type",Name=x},name=(ns,x)} 409 val _ = OpenTheory_tyop_name{tyop={Thy="ind_type",Tyop="recspace"},name=(ns,"recspace")} 410 val _ = c "CONSTR" 411 val _ = c "FCONS" 412 val _ = c "FNIL" 413 val _ = c "BOTTOM" 414end 415 416val _ = export_theory(); 417