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