1 (* ========================================================================= *)
2 (* Extensional, classical reasoning with AC starts now! *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
12 (* ------------------------------------------------------------------------- *)
13 (* Eta-axiom, corresponding conversion, and extensionality. *)
14 (* ------------------------------------------------------------------------- *)
16 let ETA_AX = new_axiom
17 `!t:A->B. (\x. t x) = t`;;
21 let pth = prove(`(\x. (t:A->B) x) = t`,MATCH_ACCEPT_TAC ETA_AX) in
23 try let bv,bod = dest_abs tm in
24 let l,r = dest_comb bod in
25 if r = bv & not (vfree_in bv l) then
26 TRANS (REFL tm) (PINST [type_of bv,aty; type_of bod,bty] [l,t] pth)
28 with Failure _ -> failwith "ETA_CONV";;
31 (`!(f:A->B) g. (!x. f x = g x) ==> f = g`,
32 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o ABS `x:A` o SPEC `x:A`) THEN
33 REWRITE_TAC[ETA_AX]);;
35 let FUN_EQ_THM = prove
36 (`!(f:A->B) g. f = g <=> (!x. f x = g x)`,
37 REPEAT GEN_TAC THEN EQ_TAC THENL
38 [DISCH_THEN SUBST1_TAC THEN GEN_TAC THEN REFL_TAC;
39 MATCH_ACCEPT_TAC EQ_EXT]);;
41 (* ------------------------------------------------------------------------- *)
42 (* Indefinite descriptor (giving AC). *)
43 (* ------------------------------------------------------------------------- *)
45 new_constant("@",`:(A->bool)->A`);;
49 let is_select = is_binder "@";;
50 let dest_select = dest_binder "@";;
51 let mk_select = mk_binder "@";;
53 let SELECT_AX = new_axiom
54 `!P (x:A). P x ==> P((@) P)`;;
56 (* ------------------------------------------------------------------------- *)
57 (* Useful for compatibility. (The old EXISTS_DEF.) *)
58 (* ------------------------------------------------------------------------- *)
60 let EXISTS_THM = prove
61 (`(?) = \P:A->bool. P ((@) P)`,
62 MATCH_MP_TAC EQ_EXT THEN BETA_TAC THEN X_GEN_TAC `P:A->bool` THEN
63 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
65 [DISCH_THEN(CHOOSE_THEN MP_TAC) THEN MATCH_ACCEPT_TAC SELECT_AX;
66 DISCH_TAC THEN EXISTS_TAC `((@) P):A` THEN POP_ASSUM ACCEPT_TAC]);;
68 (* ------------------------------------------------------------------------- *)
69 (* Rules and so on for the select operator. *)
70 (* ------------------------------------------------------------------------- *)
73 let P = `P:A->bool` in
75 (`(?) (P:A->bool) ==> P((@) P)`,
76 SIMP_TAC[SELECT_AX; ETA_AX]) in
78 try let abs = rand(concl th) in
79 let ty = type_of(bndvar abs) in
80 CONV_RULE BETA_CONV (MP (PINST [ty,aty] [abs,P] pth) th)
81 with Failure _ -> failwith "SELECT_RULE";;
84 let P = `P:A->bool` in
86 (`(P:A->bool)((@) P) = (?) P`,
87 REWRITE_TAC[EXISTS_THM] THEN BETA_TAC THEN REFL_TAC) in
89 try let is_epsok t = is_select t &
90 let bv,bod = dest_select t in
91 aconv tm (vsubst [t,bv] bod) in
92 let pickeps = find_term is_epsok tm in
93 let abs = rand pickeps in
94 let ty = type_of (bndvar abs) in
95 CONV_RULE (LAND_CONV BETA_CONV) (PINST [ty,aty] [abs,P] pth)
96 with Failure _ -> failwith "SELECT_CONV";;
98 (* ------------------------------------------------------------------------- *)
99 (* Some basic theorems. *)
100 (* ------------------------------------------------------------------------- *)
102 let SELECT_REFL = prove
103 (`!x:A. (@y. y = x) = x`,
104 GEN_TAC THEN CONV_TAC SELECT_CONV THEN
105 EXISTS_TAC `x:A` THEN REFL_TAC);;
107 let SELECT_UNIQUE = prove
108 (`!P x. (!y:A. P y = (y = x)) ==> ((@) P = x)`,
109 REPEAT STRIP_TAC THEN
110 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
111 ASM_REWRITE_TAC[SELECT_REFL]);;
113 extend_basic_rewrites [SELECT_REFL];;
115 (* ------------------------------------------------------------------------- *)
116 (* Now we can derive type definitions from existence; check benignity. *)
117 (* ------------------------------------------------------------------------- *)
119 let the_type_definitions = ref ([]:((string*string*string)*(thm*thm))list);;
121 let new_type_definition tyname (absname,repname) th =
122 try let th',tth' = assoc (tyname,absname,repname) (!the_type_definitions) in
123 if concl th' <> concl th then failwith "" else
124 (warn true "Benign redefinition of type"; tth')
127 CONV_RULE (RATOR_CONV (REWR_CONV EXISTS_THM) THENC BETA_CONV) th in
128 let th1,th2 = new_basic_type_definition tyname (absname,repname) th0 in
129 let tth = CONJ (GEN_ALL th1)
130 (GEN_ALL (CONV_RULE(LAND_CONV (TRY_CONV BETA_CONV)) th2)) in
131 the_type_definitions := ((tyname,absname,repname),(th,tth))::
132 (!the_type_definitions);
135 (* ------------------------------------------------------------------------- *)
136 (* Derive excluded middle. The proof is an optimization due to Mark Adams of *)
137 (* the original Diaconescu proof as presented in Beeson's book. *)
138 (* ------------------------------------------------------------------------- *)
140 let EXCLUDED_MIDDLE = prove
142 GEN_TAC THEN SUBGOAL_THEN
143 `(((@x. (x <=> F) \/ t) <=> F) \/ t) /\ (((@x. (x <=> T) \/ t) <=> T) \/ t)`
145 [CONJ_TAC THEN CONV_TAC SELECT_CONV THENL
146 [EXISTS_TAC `F`; EXISTS_TAC `T`] THEN
147 DISJ1_TAC THEN REFL_TAC;
148 DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
149 TRY(DISJ1_TAC THEN FIRST_ASSUM ACCEPT_TAC) THEN
150 DISJ2_TAC THEN DISCH_TAC THEN MP_TAC(ITAUT `~(T <=> F)`) THEN
151 PURE_ONCE_ASM_REWRITE_TAC[] THEN
152 ASM_REWRITE_TAC[ITAUT `p \/ T <=> T`]]);;
154 let BOOL_CASES_AX = prove
155 (`!t. (t <=> T) \/ (t <=> F)`,
156 GEN_TAC THEN DISJ_CASES_TAC(SPEC `t:bool` EXCLUDED_MIDDLE) THEN
159 (* ------------------------------------------------------------------------- *)
160 (* Classically based tactics. (See also COND_CASES_TAC later on.) *)
161 (* ------------------------------------------------------------------------- *)
163 let BOOL_CASES_TAC p = STRUCT_CASES_TAC (SPEC p BOOL_CASES_AX);;
165 let ASM_CASES_TAC t = DISJ_CASES_TAC(SPEC t EXCLUDED_MIDDLE);;
167 (* ------------------------------------------------------------------------- *)
168 (* Set up a reasonable tautology checker for classical logic. *)
169 (* ------------------------------------------------------------------------- *)
172 let PROP_REWRITE_TAC = REWRITE_TAC[] in
173 let RTAUT_TAC (asl,w) =
174 let ok t = type_of t = bool_ty & can (find_term is_var) t & free_in t w in
175 (PROP_REWRITE_TAC THEN
176 W((fun t1 t2 -> t1 THEN t2) (REWRITE_TAC[]) o BOOL_CASES_TAC o
177 hd o sort free_in o find_terms ok o snd)) (asl,w) in
178 let TAUT_TAC = REPEAT(GEN_TAC ORELSE CONJ_TAC) THEN REPEAT RTAUT_TAC in
179 fun tm -> prove(tm,TAUT_TAC);;
181 (* ------------------------------------------------------------------------- *)
182 (* A few useful classical tautologies. *)
183 (* ------------------------------------------------------------------------- *)
185 let DE_MORGAN_THM = TAUT
186 `!t1 t2. (~(t1 /\ t2) <=> ~t1 \/ ~t2) /\ (~(t1 \/ t2) <=> ~t1 /\ ~t2)`;;
189 TAUT `(!t. ~ ~t <=> t) /\ (~T <=> F) /\ (~F <=> T)`;;
191 let NOT_IMP = TAUT `!t1 t2. ~(t1 ==> t2) <=> t1 /\ ~t2`;;
193 let CONTRAPOS_THM = TAUT `!t1 t2. (~t1 ==> ~t2) <=> (t2 ==> t1)`;;
195 extend_basic_rewrites [CONJUNCT1 NOT_CLAUSES];;
197 (* ------------------------------------------------------------------------- *)
198 (* Some classically based rules. *)
199 (* ------------------------------------------------------------------------- *)
203 let pth = TAUT `(~P ==> F) ==> P` in
205 try let tm' = mk_neg tm in
206 MP (INST [tm,P] pth) (DISCH tm' th)
207 with Failure _ -> failwith "CCONTR";;
210 let a = `a:bool` and b = `b:bool` in
211 let pth = TAUT `(a ==> b) <=> (~b ==> ~a)` in
213 try let P,Q = dest_imp tm in
215 with Failure _ -> failwith "CONTRAPOS_CONV";;
217 (* ------------------------------------------------------------------------- *)
218 (* A classicalal "refutation" tactic. *)
219 (* ------------------------------------------------------------------------- *)
223 and conv = REWR_CONV(TAUT `p <=> ~p ==> F`) in
224 fun ttac (asl,w as gl) ->
225 if w = f_tm then ALL_TAC gl
226 else if is_neg w then DISCH_THEN ttac gl
227 else (CONV_TAC conv THEN DISCH_THEN ttac) gl;;
229 (* ------------------------------------------------------------------------- *)
230 (* Infinite de Morgan laws. *)
231 (* ------------------------------------------------------------------------- *)
233 let NOT_EXISTS_THM = prove
234 (`!P. ~(?x:A. P x) <=> (!x. ~(P x))`,
235 GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
236 [GEN_TAC THEN DISCH_TAC THEN UNDISCH_TAC `~(?x:A. P x)` THEN
237 REWRITE_TAC[] THEN EXISTS_TAC `x:A` THEN POP_ASSUM ACCEPT_TAC;
238 DISCH_THEN(CHOOSE_THEN MP_TAC) THEN ASM_REWRITE_TAC[]]);;
240 let EXISTS_NOT_THM = prove
241 (`!P. (?x:A. ~(P x)) <=> ~(!x. P x)`,
242 ONCE_REWRITE_TAC[TAUT `(a <=> ~b) <=> (~a <=> b)`] THEN
243 REWRITE_TAC[NOT_EXISTS_THM]);;
245 let NOT_FORALL_THM = prove
246 (`!P. ~(!x. P x) <=> (?x:A. ~(P x))`,
247 MATCH_ACCEPT_TAC(GSYM EXISTS_NOT_THM));;
249 let FORALL_NOT_THM = prove
250 (`!P. (!x. ~(P x)) <=> ~(?x:A. P x)`,
251 MATCH_ACCEPT_TAC(GSYM NOT_EXISTS_THM));;
253 (* ------------------------------------------------------------------------- *)
254 (* Expand quantification over Booleans. *)
255 (* ------------------------------------------------------------------------- *)
257 let FORALL_BOOL_THM = prove
258 (`(!b. P b) <=> P T /\ P F`,
259 EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
260 GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[]);;
262 let EXISTS_BOOL_THM = prove
263 (`(?b. P b) <=> P T \/ P F`,
264 MATCH_MP_TAC(TAUT `(~p <=> ~q) ==> (p <=> q)`) THEN
265 REWRITE_TAC[DE_MORGAN_THM; NOT_EXISTS_THM; FORALL_BOOL_THM]);;
267 (* ------------------------------------------------------------------------- *)
268 (* Universal quantifier and disjunction *)
269 (* ------------------------------------------------------------------------- *)
271 let LEFT_FORALL_OR_THM = prove
272 (`!P Q. (!x:A. P x \/ Q) <=> (!x. P x) \/ Q`,
273 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
274 REWRITE_TAC[NOT_FORALL_THM; DE_MORGAN_THM; LEFT_EXISTS_AND_THM]);;
276 let RIGHT_FORALL_OR_THM = prove
277 (`!P Q. (!x:A. P \/ Q x) <=> P \/ (!x. Q x)`,
278 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
279 REWRITE_TAC[NOT_FORALL_THM; DE_MORGAN_THM; RIGHT_EXISTS_AND_THM]);;
281 let LEFT_OR_FORALL_THM = prove
282 (`!P Q. (!x:A. P x) \/ Q <=> (!x. P x \/ Q)`,
283 MATCH_ACCEPT_TAC(GSYM LEFT_FORALL_OR_THM));;
285 let RIGHT_OR_FORALL_THM = prove
286 (`!P Q. P \/ (!x:A. Q x) <=> (!x. P \/ Q x)`,
287 MATCH_ACCEPT_TAC(GSYM RIGHT_FORALL_OR_THM));;
289 (* ------------------------------------------------------------------------- *)
290 (* Implication and quantifiers. *)
291 (* ------------------------------------------------------------------------- *)
293 let LEFT_IMP_FORALL_THM = prove
294 (`!P Q. ((!x:A. P x) ==> Q) <=> (?x. P x ==> Q)`,
295 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
296 REWRITE_TAC[NOT_EXISTS_THM; NOT_IMP; LEFT_AND_FORALL_THM]);;
298 let LEFT_EXISTS_IMP_THM = prove
299 (`!P Q. (?x. P x ==> Q) <=> ((!x:A. P x) ==> Q)`,
300 MATCH_ACCEPT_TAC(GSYM LEFT_IMP_FORALL_THM));;
302 let RIGHT_IMP_EXISTS_THM = prove
303 (`!P Q. (P ==> ?x:A. Q x) <=> (?x:A. P ==> Q x)`,
304 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
305 REWRITE_TAC[NOT_EXISTS_THM; NOT_IMP; RIGHT_AND_FORALL_THM]);;
307 let RIGHT_EXISTS_IMP_THM = prove
308 (`!P Q. (?x:A. P ==> Q x) <=> (P ==> ?x:A. Q x)`,
309 MATCH_ACCEPT_TAC(GSYM RIGHT_IMP_EXISTS_THM));;
311 (* ------------------------------------------------------------------------- *)
312 (* The conditional. *)
313 (* ------------------------------------------------------------------------- *)
315 let COND_DEF = new_definition
316 `COND = \t t1 t2. @x:A. ((t <=> T) ==> (x = t1)) /\
317 ((t <=> F) ==> (x = t2))`;;
319 let COND_CLAUSES = prove
320 (`!(t1:A) t2. ((if T then t1 else t2) = t1) /\
321 ((if F then t1 else t2) = t2)`,
322 REWRITE_TAC[COND_DEF]);;
325 try fst(dest_const(rator(rator (rator tm)))) = "COND"
326 with Failure _ -> false;;
328 let mk_cond (b,x,y) =
329 try let c = mk_const("COND",[type_of x,aty]) in
330 mk_comb(mk_comb(mk_comb(c,b),x),y)
331 with Failure _ -> failwith "mk_cond";;
334 try let tm1,y = dest_comb tm in
335 let tm2,x = dest_comb tm1 in
336 let c,b = dest_comb tm2 in
337 if fst(dest_const c) = "COND" then (b,(x,y)) else fail()
338 with Failure _ -> failwith "dest_cond";;
340 extend_basic_rewrites [COND_CLAUSES];;
342 let COND_EXPAND = prove
343 (`!b t1 t2. (if b then t1 else t2) <=> (~b \/ t1) /\ (b \/ t2)`,
344 REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN
348 (`!b (t:A). (if b then t else t) = t`,
349 REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[]);;
351 let COND_RAND = prove
352 (`!b (f:A->B) x y. f (if b then x else y) = (if b then f x else f y)`,
353 REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[]);;
355 let COND_RATOR = prove
356 (`!b (f:A->B) g x. (if b then f else g)(x) = (if b then f x else g x)`,
357 REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[]);;
360 (`!b (f:A->B) g. (\x. if b then f x else g x) = (if b then f else g)`,
361 REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[ETA_AX]);;
363 (* ------------------------------------------------------------------------- *)
364 (* Redefine TAUT to freeze in the rewrites including COND. *)
365 (* ------------------------------------------------------------------------- *)
368 let PROP_REWRITE_TAC = REWRITE_TAC[] in
369 let RTAUT_TAC (asl,w) =
370 let ok t = type_of t = bool_ty & can (find_term is_var) t & free_in t w in
371 (PROP_REWRITE_TAC THEN
372 W((fun t1 t2 -> t1 THEN t2) (REWRITE_TAC[]) o BOOL_CASES_TAC o
373 hd o sort free_in o find_terms ok o snd)) (asl,w) in
374 let TAUT_TAC = REPEAT(GEN_TAC ORELSE CONJ_TAC) THEN REPEAT RTAUT_TAC in
375 fun tm -> prove(tm,TAUT_TAC);;
377 (* ------------------------------------------------------------------------- *)
378 (* Throw monotonicity in. *)
379 (* ------------------------------------------------------------------------- *)
381 let MONO_COND = prove
382 (`(A ==> B) /\ (C ==> D) ==> (if b then A else C) ==> (if b then B else D)`,
383 STRIP_TAC THEN BOOL_CASES_TAC `b:bool` THEN
386 monotonicity_theorems := MONO_COND::(!monotonicity_theorems);;
388 (* ------------------------------------------------------------------------- *)
389 (* Tactic for splitting over an arbitrarily chosen conditional. *)
390 (* ------------------------------------------------------------------------- *)
392 let COND_ELIM_THM = prove
393 (`(P:A->bool) (if c then x else y) <=> (c ==> P x) /\ (~c ==> P y)`,
394 BOOL_CASES_TAC `c:bool` THEN REWRITE_TAC[]);;
396 let COND_ELIM_CONV = HIGHER_REWRITE_CONV[COND_ELIM_THM] true;;
398 let (COND_CASES_TAC :tactic) =
399 let DENEG_RULE = GEN_REWRITE_RULE I [TAUT `~ ~ p <=> p`] in
400 CONV_TAC COND_ELIM_CONV THEN CONJ_TAC THENL
401 [DISCH_THEN(fun th -> ASSUME_TAC th THEN SUBST1_TAC(EQT_INTRO th));
402 DISCH_THEN(fun th -> try let th' = DENEG_RULE th in
403 ASSUME_TAC th' THEN SUBST1_TAC(EQT_INTRO th')
405 ASSUME_TAC th THEN SUBST1_TAC(EQF_INTRO th))];;
407 (* ------------------------------------------------------------------------- *)
409 (* ------------------------------------------------------------------------- *)
411 let SKOLEM_THM = prove
412 (`!P. (!x:A. ?y:B. P x y) <=> (?y. !x. P x (y x))`,
413 REPEAT(STRIP_TAC ORELSE EQ_TAC) THENL
414 [EXISTS_TAC `\x:A. @y:B. P x y` THEN GEN_TAC THEN
415 BETA_TAC THEN CONV_TAC SELECT_CONV;
416 EXISTS_TAC `(y:A->B) x`] THEN
417 POP_ASSUM MATCH_ACCEPT_TAC);;
419 let SKOLEM_THM_GEN = prove
420 (`!P s. (!x. P x ==> ?y. R x y) <=> (?f. !x. P x ==> R x (f x))`,
421 REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM]);;
423 (* ------------------------------------------------------------------------- *)
424 (* NB: this one is true intutionistically and intensionally. *)
425 (* ------------------------------------------------------------------------- *)
427 let UNIQUE_SKOLEM_ALT = prove
428 (`!P:A->B->bool. (!x. ?!y. P x y) <=> ?f. !x y. P x y <=> (f x = y)`,
429 GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_ALT; SKOLEM_THM]);;
431 (* ------------------------------------------------------------------------- *)
432 (* and this one intuitionistically and extensionally. *)
433 (* ------------------------------------------------------------------------- *)
435 let UNIQUE_SKOLEM_THM = prove
436 (`!P. (!x:A. ?!y:B. P x y) <=> (?!f. !x. P x (f x))`,
437 GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_THM; SKOLEM_THM; FORALL_AND_THM] THEN
438 EQ_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
439 ASM_REWRITE_TAC[] THENL
440 [REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
441 X_GEN_TAC `x:A` THEN FIRST_ASSUM MATCH_MP_TAC THEN
442 EXISTS_TAC `x:A` THEN ASM_REWRITE_TAC[];
443 MAP_EVERY X_GEN_TAC [`x:A`; `y1:B`; `y2:B`] THEN STRIP_TAC THEN
444 FIRST_ASSUM(X_CHOOSE_TAC `f:A->B`) THEN
445 SUBGOAL_THEN `(\z. if z = x then y1 else (f:A->B) z) =
446 (\z. if z = x then y2 else (f:A->B) z)` MP_TAC THENL
447 [FIRST_ASSUM MATCH_MP_TAC THEN
448 REPEAT STRIP_TAC THEN BETA_TAC THEN COND_CASES_TAC THEN
450 DISCH_THEN(MP_TAC o C AP_THM `x:A`) THEN REWRITE_TAC[]]]);;
452 (* ------------------------------------------------------------------------- *)
453 (* Extend default congruences for contextual rewriting. *)
454 (* ------------------------------------------------------------------------- *)
458 (g' ==> (t = t')) ==>
459 (~g' ==> (e = e')) ==>
460 ((if g then t else e) = (if g' then t' else e'))` in
461 extend_basic_congs [COND_CONG];;
463 let COND_EQ_CLAUSE = prove
464 (`(if x = x then y else z) = y`,
466 extend_basic_rewrites [COND_EQ_CLAUSE];;
468 (* ------------------------------------------------------------------------- *)
469 (* We can now treat "bool" as an enumerated type for some purposes. *)
470 (* ------------------------------------------------------------------------- *)
472 let bool_INDUCT = prove
473 (`!P. P F /\ P T ==> !x. P x`,
474 REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SPEC `x:bool` BOOL_CASES_AX) THEN
477 let bool_RECURSION = prove
478 (`!a b:A. ?f. f F = a /\ f T = b`,
479 REPEAT GEN_TAC THEN EXISTS_TAC `\x. if x then b:A else a` THEN
482 let inductive_type_store = ref
483 ["bool",(2,bool_INDUCT,bool_RECURSION)];;