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