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