1 (* ========================================================================= *)
2 (* A HOL "by" tactic, doing Mizar-like things, trying something that is *)
3 (* sufficient for HOL's basic rules, trying a few other things like *)
4 (* arithmetic, and finally if all else fails using MESON_TAC[]. *)
5 (* ========================================================================= *)
7 (* ------------------------------------------------------------------------- *)
8 (* More refined net lookup that double-checks conditions like matchability. *)
9 (* ------------------------------------------------------------------------- *)
11 let matching_enter tm y net =
12 enter [] (tm,((fun tm' -> can (term_match [] tm) tm'),y)) net;;
14 let unconditional_enter (tm,y) net =
15 enter [] (tm,((fun t -> true),y)) net;;
17 let conditional_enter (tm,condy) net =
18 enter [] (tm,condy) net;;
20 let careful_lookup tm net =
21 map snd (filter (fun (c,y) -> c tm) (lookup tm net));;
23 (* ------------------------------------------------------------------------- *)
24 (* Transform theorem list to simplify, eliminate redundant connectives and *)
25 (* split the problem into (generally multiple) subproblems. Then, call the *)
26 (* prover given as the first argument on each component. *)
27 (* ------------------------------------------------------------------------- *)
30 let action_false th f oths = th
31 and action_true th f oths = f oths
32 and action_conj th f oths =
33 f (CONJUNCT1 th :: CONJUNCT2 th :: oths)
34 and action_disj th f oths =
35 let th1 = f (ASSUME(lhand(concl th)) :: oths)
36 and th2 = f (ASSUME(rand(concl th)) :: oths) in
39 let pfun = PART_MATCH lhs (TAUT tm) in
40 let prule th = EQ_MP (pfun (concl th)) th in
41 lhand tm,(fun th f oths -> f(prule th :: oths)) in
42 let enet = itlist unconditional_enter
47 action_taut `(p ==> q) <=> ~p \/ q`;
48 action_taut `~F <=> T`;
49 action_taut `~T <=> F`;
50 action_taut `~(~p) <=> p`;
51 action_taut `~(p /\ q) <=> ~p \/ ~q`;
52 action_taut `~(p \/ q) <=> ~p /\ ~q`;
53 action_taut `~(p ==> q) <=> p /\ ~q`;
54 action_taut `p /\ F <=> F`;
55 action_taut `F /\ p <=> F`;
56 action_taut `p /\ T <=> p`;
57 action_taut `T /\ p <=> p`;
58 action_taut `p \/ F <=> p`;
59 action_taut `F \/ p <=> p`;
60 action_taut `p \/ T <=> T`;
61 action_taut `T \/ p <=> T`]
62 (let tm,act = action_taut `~(p <=> q) <=> p /\ ~q \/ ~p /\ q` in
63 let cond tm = type_of(rand(rand tm)) = bool_ty in
64 conditional_enter (tm,(cond,act))
65 (let tm,act = action_taut `(p <=> q) <=> p /\ q \/ ~p /\ ~q` in
66 let cond tm = type_of(rand tm) = bool_ty in
67 conditional_enter (tm,(cond,act)) empty_net)) in
69 let rec splitthen splat tosplit =
71 [] -> prover (rev splat)
73 let funs = careful_lookup (concl th) enet in
74 if funs = [] then splitthen (th::splat) oths
75 else (hd funs) th (splitthen splat) oths in
78 (* ------------------------------------------------------------------------- *)
79 (* A similar thing that also introduces Skolem constants (but not functions) *)
80 (* and does some slight first-order simplification like trivial miniscoping. *)
81 (* ------------------------------------------------------------------------- *)
84 let action_false th f splat oths = th
85 and action_true th f splat oths = f oths
86 and action_conj th f splat oths =
87 f (CONJUNCT1 th :: CONJUNCT2 th :: oths)
88 and action_disj th f splat oths =
89 let th1 = f (ASSUME(lhand(concl th)) :: oths)
90 and th2 = f (ASSUME(rand(concl th)) :: oths) in
92 and action_exists th f splat oths =
93 let v,bod = dest_exists(concl th) in
94 let vars = itlist (union o thm_frees) (oths @ splat) (thm_frees th) in
95 let v' = variant vars v in
96 let th' = ASSUME (subst [v',v] bod) in
97 CHOOSE (v',th) (f (th'::oths))
99 let pfun = PART_MATCH lhs (TAUT tm) in
100 let prule th = EQ_MP (pfun (concl th)) th in
101 lhand tm,(fun th f splat oths -> f(prule th :: oths))
103 let pfun = PART_MATCH lhs (prove(tm,MESON_TAC[])) in
104 let prule th = EQ_MP (pfun (concl th)) th in
105 lhand tm,(fun th f splat oths -> f(prule th :: oths)) in
106 let enet = itlist unconditional_enter
109 `p /\ q`,action_conj;
110 `p \/ q`,action_disj;
111 `?x. P x`,action_exists;
112 action_taut `~(~p) <=> p`;
113 action_taut `~(p /\ q) <=> ~p \/ ~q`;
114 action_taut `~(p \/ q) <=> ~p /\ ~q`;
115 action_fol `~(!x. P x) <=> (?x. ~(P x))`;
116 action_fol `(!x. P x /\ Q x) <=> (!x. P x) /\ (!x. Q x)`]
119 let rec splitthen splat tosplit =
121 [] -> prover (rev splat)
123 let funs = careful_lookup (concl th) enet in
124 if funs = [] then splitthen (th::splat) oths
125 else (hd funs) th (splitthen splat) splat oths in
128 (* ------------------------------------------------------------------------- *)
129 (* Do the basic "semantic correlates" stuff. *)
130 (* This is more like NNF than Mizar's version. *)
131 (* ------------------------------------------------------------------------- *)
135 [TAUT `(a <=> b) <=> (a ==> b) /\ (b ==> a)`;
136 TAUT `(a ==> b) <=> ~a \/ b`;
149 GSYM CONJ_ASSOC; GSYM DISJ_ASSOC;
150 prove(`(?x. P x) <=> ~(!x. ~(P x))`,MESON_TAC[])];;
152 (* ------------------------------------------------------------------------- *)
153 (* Look for an immediate contradictory pair of theorems. This is quadratic, *)
154 (* but I doubt if that's much of an issue in practice. We could do something *)
155 (* fancier, but need to be careful over alpha-equivalence if sorting. *)
156 (* ------------------------------------------------------------------------- *)
158 let THMLIST_CONTR_RULE =
159 let CONTR_PAIR_THM = UNDISCH_ALL(TAUT `p ==> ~p ==> F`)
160 and p_tm = `p:bool` in
162 let ths_n,ths_p = partition (is_neg o concl) ths in
163 let th_n = find (fun thn -> let tm = rand(concl thn) in
164 exists (aconv tm o concl) ths_p) ths_n in
165 let tm = rand(concl th_n) in
166 let th_p = find (aconv tm o concl) ths_p in
167 itlist PROVE_HYP [th_p; th_n] (INST [tm,p_tm] CONTR_PAIR_THM);;
169 (* ------------------------------------------------------------------------- *)
170 (* Hence something similar to Mizar's "prechecker". *)
171 (* ------------------------------------------------------------------------- *)
173 let PRECHECKER_THEN prover =
174 SPLIT_THEN (fun ths -> try THMLIST_CONTR_RULE ths
176 SPLIT_FOL_THEN prover (map CORRELATE_RULE ths));;
178 (* ------------------------------------------------------------------------- *)
179 (* Lazy equations for use in congruence closure. *)
180 (* ------------------------------------------------------------------------- *)
182 type lazyeq = Lazy of (term * term) * (unit -> thm);;
185 let store = ref TRUTH in
186 fun () -> let th = !store in
187 if is_eq(concl th) then th else
189 (store := th'; th');;
192 Lazy((dest_eq(concl th)),(fun () -> th));;
194 let lazy_eval (Lazy(_,f)) = f();;
196 let REFL' t = Lazy((t,t),cache(fun () -> REFL t));;
198 let SYM' = fun (Lazy((t,t'),f)) -> Lazy((t',t),cache(fun () -> SYM(f ())));;
201 fun (Lazy((s,s'),f)) (Lazy((t,t'),g)) ->
202 if not(aconv s' t) then failwith "TRANS'"
203 else Lazy((s,t'),cache(fun () -> TRANS (f ()) (g ())));;
206 fun (Lazy((s,s'),f),Lazy((t,t'),g)) ->
207 Lazy((mk_comb(s,t),mk_comb(s',t')),cache(fun () -> MK_COMB (f (),g ())));;
209 let concl' = fun (Lazy(tmp,g)) -> tmp;;
211 (* ------------------------------------------------------------------------- *)
212 (* Successors of a term, and predecessor function. *)
213 (* ------------------------------------------------------------------------- *)
216 try let f,x = dest_comb tm in [f;x]
217 with Failure _ -> [];;
219 let predecessor_function tms =
220 itlist (fun x -> itlist (fun y f -> (y |-> insert x (tryapplyd f y [])) f)
224 (* ------------------------------------------------------------------------- *)
225 (* A union-find structure for equivalences, with theorems for edges. *)
226 (* ------------------------------------------------------------------------- *)
228 type termnode = Nonterminal of lazyeq | Terminal of term * term list;;
230 type termequivalence = Equivalence of (term,termnode)func;;
232 let rec terminus (Equivalence f as eqv) a =
233 match (apply f a) with
234 Nonterminal(th) -> let b = snd(concl' th) in
235 let th',n = terminus eqv b in
237 | Terminal(t,n) -> (REFL' t,n);;
239 let tryterminus eqv a =
240 try terminus eqv a with Failure _ -> (REFL' a,[a]);;
242 let canonize eqv a = fst(tryterminus eqv a);;
244 let equate th (Equivalence f as eqv) =
245 let a,b = concl' th in
246 let (ath,na) = tryterminus eqv a
247 and (bth,nb) = tryterminus eqv b in
248 let a' = snd(concl' ath) and b' = snd(concl' bth) in
250 (if a' = b' then f else
251 if length na <= length nb then
252 let th' = TRANS' (TRANS' (SYM' ath) th) bth in
253 (a' |-> Nonterminal th') ((b' |-> Terminal(b',na@nb)) f)
255 let th' = TRANS'(SYM'(TRANS' th bth)) ath in
256 (b' |-> Nonterminal th') ((a' |-> Terminal(a',na@nb)) f));;
258 let unequal = Equivalence undefined;;
260 let equated (Equivalence f) = dom f;;
262 let prove_equal eqv (s,t) =
263 let sth = canonize eqv s and tth = canonize eqv t in
264 TRANS' (canonize eqv s) (SYM'(canonize eqv t));;
266 let equivalence_class eqv a = snd(tryterminus eqv a);;
268 (* ------------------------------------------------------------------------- *)
269 (* Prove composite terms equivalent based on 1-step congruence. *)
270 (* ------------------------------------------------------------------------- *)
272 let provecongruent eqv (tm1,tm2) =
273 let f1,x1 = dest_comb tm1
274 and f2,x2 = dest_comb tm2 in
275 MK_COMB'(prove_equal eqv (f1,f2),prove_equal eqv (x1,x2));;
277 (* ------------------------------------------------------------------------- *)
278 (* Merge equivalence classes given equation "th", using congruence closure. *)
279 (* ------------------------------------------------------------------------- *)
281 let rec emerge th (eqv,pfn) =
282 let s,t = concl' th in
283 let sth = canonize eqv s and tth = canonize eqv t in
284 let s' = snd(concl' sth) and t' = snd(concl' tth) in
285 if s' = t' then (eqv,pfn) else
286 let sp = tryapplyd pfn s' [] and tp = tryapplyd pfn t' [] in
287 let eqv' = equate th eqv in
288 let stth = canonize eqv' s' in
289 let sttm = snd(concl' stth) in
290 let pfn' = (sttm |-> union sp tp) pfn in
291 itlist (fun (u,v) (eqv,pfn as eqp) ->
292 try let thuv = provecongruent eqv (u,v) in emerge thuv eqp
293 with Failure _ -> eqp)
294 (allpairs (fun u v -> (u,v)) sp tp) (eqv',pfn');;
296 (* ------------------------------------------------------------------------- *)
297 (* Find subterms of "tm" that contain as a subterm one of the "tms" terms. *)
298 (* This is intended to be more efficient than the obvious "find_terms ...". *)
299 (* ------------------------------------------------------------------------- *)
301 let rec supersubterms tms tm =
303 if mem tm tms then [tm],filter (fun t -> t <> tm) tms
305 if tms' = [] then ltms else
307 try let l,r = dest_comb tm in
308 union (supersubterms tms' l) (supersubterms tms' r)
309 with Failure _ -> [] in
310 if stms = [] then ltms
313 (* ------------------------------------------------------------------------- *)
314 (* Find an appropriate term universe for overall terms "tms". *)
315 (* ------------------------------------------------------------------------- *)
317 let term_universe tms =
318 setify (itlist ((@) o supersubterms tms) tms []);;
320 (* ------------------------------------------------------------------------- *)
321 (* Congruence closure of "eqs" over term universe "tms". *)
322 (* ------------------------------------------------------------------------- *)
324 let congruence_closure tms eqs =
325 let pfn = predecessor_function tms in
326 let eqv,_ = itlist emerge eqs (unequal,pfn) in
329 (* ------------------------------------------------------------------------- *)
330 (* Prove that "eq" follows from "eqs" by congruence closure. *)
331 (* ------------------------------------------------------------------------- *)
334 let tps = dest_eq eq :: map concl' eqs in
335 let otms = itlist (fun (x,y) l -> x::y::l) tps [] in
336 let tms = term_universe(setify otms) in
337 let eqv = congruence_closure tms eqs in
338 prove_equal eqv (dest_eq eq);;
340 (* ------------------------------------------------------------------------- *)
341 (* Inference rule for `eq1 /\ ... /\ eqn ==> eq` *)
342 (* ------------------------------------------------------------------------- *)
344 let CONGRUENCE_CLOSURE tm =
346 let eqs,eq = dest_imp tm in
347 DISCH eqs (lazy_eval(CCPROVE (map lazy_eq (CONJUNCTS(ASSUME eqs))) eq))
348 else lazy_eval(CCPROVE [] tm);;
350 (* ------------------------------------------------------------------------- *)
351 (* Inference rule for contradictoriness of set of +ve and -ve eqns. *)
352 (* ------------------------------------------------------------------------- *)
354 let CONGRUENCE_CLOSURE_CONTR ths =
355 let nths,pths = partition (is_neg o concl) ths in
356 let peqs = filter (is_eq o concl) pths
357 and neqs = filter (is_eq o rand o concl) nths in
358 let tps = map (dest_eq o concl) peqs @ map (dest_eq o rand o concl) neqs in
359 let otms = itlist (fun (x,y) l -> x::y::l) tps [] in
360 let tms = term_universe(setify otms) in
361 let eqv = congruence_closure tms (map lazy_eq peqs) in
363 let eq = dest_eq(rand(concl th)) in
364 let lth = prove_equal eqv eq in
365 EQ_MP (EQF_INTRO th) (lazy_eval lth) in
366 tryfind prover neqs;;
368 (* ------------------------------------------------------------------------- *)
369 (* Attempt to prove equality between terms/formulas based on equivalence. *)
370 (* Note that ABS sideconditions are only checked at inference-time... *)
371 (* ------------------------------------------------------------------------- *)
374 fun (Lazy((s,t),f)) ->
375 Lazy((mk_abs(v,s),mk_abs(v,t)),
376 cache(fun () -> ABS v (f ())));;
378 let ALPHA_EQ' s' t' =
379 fun (Lazy((s,t),f) as inp) ->
380 if s' = s & t' = t then inp else
382 cache(fun () -> EQ_MP (ALPHA (mk_eq(s,t)) (mk_eq(s',t')))
385 let rec PROVE_EQUAL eqv (tm1,tm2 as tmp) =
386 if tm1 = tm2 then REFL' tm1 else
387 try prove_equal eqv tmp with Failure _ ->
388 if is_comb tm1 & is_comb tm2 then
389 let f1,x1 = dest_comb tm1
390 and f2,x2 = dest_comb tm2 in
391 MK_COMB'(PROVE_EQUAL eqv (f1,f2),PROVE_EQUAL eqv (x1,x2))
392 else if is_abs tm1 & is_abs tm2 then
393 let x1,bod1 = dest_abs tm1
394 and x2,bod2 = dest_abs tm2 in
395 let gv = genvar(type_of x1) in
397 (ABS' x1 (PROVE_EQUAL eqv (vsubst[gv,x1] bod1,vsubst[gv,x2] bod2)))
398 else failwith "PROVE_EQUAL";;
400 let PROVE_EQUIVALENT eqv tm1 tm2 = lazy_eval (PROVE_EQUAL eqv (tm1,tm2));;
402 (* ------------------------------------------------------------------------- *)
403 (* Complementary version for formulas. *)
404 (* ------------------------------------------------------------------------- *)
406 let PROVE_COMPLEMENTARY eqv th1 th2 =
407 let tm1 = concl th1 and tm2 = concl th2 in
409 let th = PROVE_EQUIVALENT eqv (rand tm1) tm2 in
410 EQ_MP (EQF_INTRO th1) (EQ_MP (SYM th) th2)
411 else if is_neg tm2 then
412 let th = PROVE_EQUIVALENT eqv (rand tm2) tm1 in
413 EQ_MP (EQF_INTRO th2) (EQ_MP (SYM th) th1)
414 else failwith "PROVE_COMPLEMENTARY";;
416 (* ------------------------------------------------------------------------- *)
417 (* Check equality under equivalence with "env" mapping for first term. *)
418 (* ------------------------------------------------------------------------- *)
420 let rec test_eq eqv (tm1,tm2) env =
421 if is_comb tm1 & is_comb tm2 then
422 let f1,x1 = dest_comb tm1
423 and f2,x2 = dest_comb tm2 in
424 test_eq eqv (f1,f2) env & test_eq eqv (x1,x2) env
425 else if is_abs tm1 & is_abs tm2 then
426 let x1,bod1 = dest_abs tm1
427 and x2,bod2 = dest_abs tm2 in
428 let gv = genvar(type_of x1) in
429 test_eq eqv (vsubst[gv,x1] bod1,vsubst[gv,x2] bod2) env
430 else if is_var tm1 & can (rev_assoc tm1) env then
431 test_eq eqv (rev_assoc tm1 env,tm2) []
432 else can (prove_equal eqv) (tm1,tm2);;
434 (* ------------------------------------------------------------------------- *)
435 (* Map a term to its equivalence class modulo equivalence *)
436 (* ------------------------------------------------------------------------- *)
438 let rec term_equivs eqv tm =
439 let l = equivalence_class eqv tm in
441 else if is_comb tm then
442 let f,x = dest_comb tm in
443 allpairs (curry mk_comb) (term_equivs eqv f) (term_equivs eqv x)
444 else if is_abs tm then
445 let v,bod = dest_abs tm in
446 let gv = genvar(type_of v) in
447 map (fun t -> alpha v (mk_abs(gv,t))) (term_equivs eqv (vsubst [gv,v] bod))
450 (* ------------------------------------------------------------------------- *)
451 (* Replace "outer" universal variables with genvars. This is "outer" in the *)
452 (* second sense, i.e. universals not in scope of an existential or negation. *)
453 (* ------------------------------------------------------------------------- *)
458 let v = bndvar(rand tm) in
459 let gv = genvar(type_of v) in
461 else if is_conj tm then
462 let th1,th2 = CONJ_PAIR th in
463 CONJ (GENSPEC th1) (GENSPEC th2)
464 else if is_disj tm then
465 let th1 = GENSPEC(ASSUME(lhand tm))
466 and th2 = GENSPEC(ASSUME(rand tm)) in
467 let th3 = DISJ1 th1 (concl th2)
468 and th4 = DISJ2 (concl th1) th2 in
469 DISJ_CASES th th3 th4
472 (* ------------------------------------------------------------------------- *)
473 (* Simple first-order matching. *)
474 (* ------------------------------------------------------------------------- *)
476 let rec term_fmatch vars vtm ctm env =
478 if can (rev_assoc vtm) env then
479 term_fmatch vars (rev_assoc vtm env) ctm env
480 else if aconv vtm ctm then env else (ctm,vtm)::env
481 else if is_comb vtm & is_comb ctm then
482 let fv,xv = dest_comb vtm
483 and fc,xc = dest_comb ctm in
484 term_fmatch vars fv fc (term_fmatch vars xv xc env)
485 else if is_abs vtm & is_abs ctm then
486 let xv,bodv = dest_abs vtm
487 and xc,bodc = dest_abs ctm in
488 let gv = genvar(type_of xv) and gc = genvar(type_of xc) in
489 let gbodv = vsubst [gv,xv] bodv
490 and gbodc = vsubst [gc,xc] bodc in
491 term_fmatch (gv::vars) gbodv gbodc ((gc,gv)::env)
492 else if vtm = ctm then env
493 else failwith "term_fmatch";;
495 let rec check_consistency env =
498 | (c,v)::es -> forall (fun (c',v') -> v' <> v or c' = c) es;;
500 let separate_insts env =
501 let tyin = itlist (fun (c,v) -> type_match (type_of v) (type_of c))
503 let ifn(c,v) = (inst tyin c,inst tyin v) in
504 let tmin = setify (map ifn env) in
505 if check_consistency tmin then (tmin,tyin)
506 else failwith "separate_insts";;
508 let first_order_match vars vtm ctm env =
509 let env' = term_fmatch vars vtm ctm env in
510 if can separate_insts env' then env' else failwith "first_order_match";;
512 (* ------------------------------------------------------------------------- *)
513 (* Try to match all leaves to negation of auxiliary propositions. *)
514 (* ------------------------------------------------------------------------- *)
517 let rec matchleaves vars vtm ctms env cont =
519 try matchleaves vars (rand vtm) ctms env cont
520 with Failure _ -> matchleaves vars (lhand vtm) ctms env cont
521 else if is_disj vtm then
522 matchleaves vars (lhand vtm) ctms env
523 (fun e -> matchleaves vars (rand vtm) ctms e cont)
525 tryfind (fun ctm -> cont (first_order_match vars vtm ctm env)) ctms in
526 fun vars vtm ctms env -> matchleaves vars vtm ctms env (fun e -> e);;
528 (* ------------------------------------------------------------------------- *)
529 (* Now actually do the refutation once theorem is instantiated. *)
530 (* ------------------------------------------------------------------------- *)
532 let rec REFUTE_LEAVES eqv cths th =
535 try REFUTE_LEAVES eqv cths (CONJUNCT1 th)
536 with Failure _ -> REFUTE_LEAVES eqv cths (CONJUNCT2 th)
537 else if is_disj tm then
538 let th1 = REFUTE_LEAVES eqv cths (ASSUME(lhand tm))
539 and th2 = REFUTE_LEAVES eqv cths (ASSUME(rand tm)) in
540 DISJ_CASES th th1 th2
542 tryfind (PROVE_COMPLEMENTARY eqv th) cths;;
544 (* ------------------------------------------------------------------------- *)
545 (* Hence the Mizar "unifier" for given universal formula. *)
546 (* ------------------------------------------------------------------------- *)
548 let negate tm = if is_neg tm then rand tm else mk_neg tm;;
550 let MIZAR_UNIFIER eqv ths th =
551 let gth = GENSPEC th in
552 let vtm = concl gth in
553 let vars = subtract (frees vtm) (frees(concl th))
554 and ctms = map (negate o concl) ths in
555 let allctms = itlist (union o term_equivs eqv) ctms [] in
556 let env = matchleaves vars vtm allctms [] in
557 let tmin,tyin = separate_insts env in
558 REFUTE_LEAVES eqv ths (PINST tyin tmin gth);;
560 (* ------------------------------------------------------------------------- *)
561 (* Deduce disequalities of subterms and add symmetric versions at the end. *)
562 (* ------------------------------------------------------------------------- *)
564 let rec DISEQUALITIES ths =
568 let t1,t2 = dest_eq (rand(concl th)) in
569 let f1,args1 = strip_comb t1
570 and f2,args2 = strip_comb t2 in
571 if f1 <> f2 or length args1 <> length args2
572 then th::(GSYM th)::(DISEQUALITIES oths) else
573 let zargs = zip args1 args2 in
574 let diffs = filter (fun (a1,a2) -> a1 <> a2) zargs in
575 if length diffs <> 1 then th::(GSYM th)::(DISEQUALITIES oths) else
576 let eths = map (fun (a1,a2) ->
577 if a1 = a2 then REFL a1 else ASSUME(mk_eq(a1,a2))) zargs in
578 let th1 = rev_itlist (fun x y -> MK_COMB(y,x)) eths (REFL f1) in
580 MP (GEN_REWRITE_RULE I [GSYM CONTRAPOS_THM] (DISCH_ALL th1)) th in
581 th::(GSYM th)::(DISEQUALITIES(th2::oths));;
583 (* ------------------------------------------------------------------------- *)
584 (* Get such a starting inequality from complementary literals. *)
585 (* ------------------------------------------------------------------------- *)
587 let ATOMINEQUALITIES th1 th2 =
588 let t1 = concl th1 and t2' = concl th2 in
589 let t2 = dest_neg t2' in
590 let f1,args1 = strip_comb t1
591 and f2,args2 = strip_comb t2 in
592 if f1 <> f2 or length args1 <> length args2 then [] else
593 let zargs = zip args1 args2 in
594 let diffs = filter (fun (a1,a2) -> a1 <> a2) zargs in
595 if length diffs <> 1 then [] else
596 let eths = map (fun (a1,a2) ->
597 if a1 = a2 then REFL a1 else ASSUME(mk_eq(a1,a2))) zargs in
598 let th3 = rev_itlist (fun x y -> MK_COMB(y,x)) eths (REFL f1) in
599 let th4 = EQ_MP (TRANS th3 (EQF_INTRO th2)) th1 in
600 let th5 = NOT_INTRO(itlist (DISCH o mk_eq) diffs th4) in
601 [itlist PROVE_HYP [th1; th2] th5];;
603 (* ------------------------------------------------------------------------- *)
605 (* ------------------------------------------------------------------------- *)
607 let BASIC_MIZARBY ths =
608 try let nths,pths = partition (is_neg o concl) ths in
609 let peqs,pneqs = partition (is_eq o concl) pths
610 and neqs,nneqs = partition (is_eq o rand o concl) nths in
611 let tps = map (dest_eq o concl) peqs @
612 map (dest_eq o rand o concl) neqs in
613 let otms = itlist (fun (x,y) l -> x::y::l) tps [] in
614 let tms = term_universe(setify otms) in
615 let eqv = congruence_closure tms (map lazy_eq peqs) in
617 let s,t = dest_eq(rand(concl th)) in
618 let th' = PROVE_EQUIVALENT eqv s t in
619 EQ_MP (EQF_INTRO th) th'
620 and contrprover thp thn =
621 let th = PROVE_EQUIVALENT eqv (concl thp) (rand(concl thn)) in
622 EQ_MP (TRANS th (EQF_INTRO thn)) thp in
623 try tryfind eqprover neqs with Failure _ ->
624 try tryfind (fun thp -> tryfind (contrprover thp) nneqs) pneqs
626 let new_neqs = unions(allpairs ATOMINEQUALITIES pneqs nneqs) in
627 let allths = pneqs @ nneqs @ peqs @ DISEQUALITIES(neqs @ new_neqs) in
628 tryfind (MIZAR_UNIFIER eqv allths)
629 (filter (is_forall o concl) allths)
630 with Failure _ -> failwith "BASIC_MIZARBY";;
632 (* ------------------------------------------------------------------------- *)
633 (* Put it all together. *)
634 (* ------------------------------------------------------------------------- *)
636 let MIZAR_REFUTER ths = PRECHECKER_THEN BASIC_MIZARBY ths;;
638 (* ------------------------------------------------------------------------- *)
639 (* The Mizar prover for getting a conclusion from hypotheses. *)
640 (* ------------------------------------------------------------------------- *)
643 let pth = TAUT `(~p ==> F) <=> p` and p_tm = `p:bool` in
645 let tm' = mk_neg tm in
646 let th0 = ASSUME tm' in
647 let th1 = MIZAR_REFUTER (th0::ths) in
648 EQ_MP (INST [tm,p_tm] pth) (DISCH tm' th1);;
650 (* ------------------------------------------------------------------------- *)
651 (* As a standalone prover of formulas. *)
652 (* ------------------------------------------------------------------------- *)
654 let MIZAR_RULE tm = MIZAR_BY [] tm;;
656 (* ------------------------------------------------------------------------- *)
657 (* Some additional stuff for HOL. *)
658 (* ------------------------------------------------------------------------- *)
662 TOP_DEPTH_CONV GEN_BETA_CONV THENC REWRITE_CONV[IN_ELIM_THM]
663 and BUILTIN_CONV tm =
664 try EQT_ELIM(NUM_REDUCE_CONV tm) with Failure _ ->
665 try EQT_ELIM(REAL_RAT_REDUCE_CONV tm) with Failure _ ->
666 try ARITH_RULE tm with Failure _ ->
667 try REAL_ARITH tm with Failure _ ->
668 failwith "BUILTIN_CONV" in
670 try MIZAR_BY ths tm with Failure _ ->
671 try tryfind (fun th -> PART_MATCH I th tm) ths with Failure _ ->
672 try let avs,bod = strip_forall tm in
673 let gvs = map (genvar o type_of) avs in
674 let gtm = vsubst (zip gvs avs) bod in
675 let th = tryfind (fun th -> PART_MATCH I th gtm) ths in
676 let gth = GENL gvs th in
677 EQ_MP (ALPHA (concl gth) tm) gth
678 with Failure _ -> try
679 (let ths' = map BETA_RULE ths
680 and th' = TOP_DEPTH_CONV BETA_CONV tm in
681 let tm' = rand(concl th') in
682 try EQ_MP (SYM th') (tryfind (fun th -> PART_MATCH I th tm') ths)
683 with Failure _ -> try EQ_MP (SYM th') (BUILTIN_CONV tm')
685 let ths'' = map (CONV_RULE BETASET_CONV) ths'
686 and th'' = TRANS th' (BETASET_CONV tm') in
687 EQ_MP (SYM th'') (prove(rand(concl th''),MESON_TAC ths'')))
688 with Failure _ -> failwith "HOL_BY";;
690 (* ------------------------------------------------------------------------- *)
691 (* Standalone prover, breaking down an implication first. *)
692 (* ------------------------------------------------------------------------- *)
695 try let l,r = dest_imp tm in
696 DISCH l (HOL_BY (CONJUNCTS(ASSUME l)) r)
697 with Failure _ -> HOL_BY [] tm;;
699 (* ------------------------------------------------------------------------- *)
700 (* Tautology examples (Pelletier problems). *)
701 (* ------------------------------------------------------------------------- *)
703 let prop_1 = time HOL_RULE
704 `p ==> q <=> ~q ==> ~p`;;
706 let prop_2 = time HOL_RULE
709 let prop_3 = time HOL_RULE
710 `~(p ==> q) ==> q ==> p`;;
712 let prop_4 = time HOL_RULE
713 `~p ==> q <=> ~q ==> p`;;
715 let prop_5 = time HOL_RULE
716 `(p \/ q ==> p \/ r) ==> p \/ (q ==> r)`;;
718 let prop_6 = time HOL_RULE
721 let prop_7 = time HOL_RULE
724 let prop_8 = time HOL_RULE
725 `((p ==> q) ==> p) ==> p`;;
727 let prop_9 = time HOL_RULE
728 `(p \/ q) /\ (~p \/ q) /\ (p \/ ~q) ==> ~(~q \/ ~q)`;;
730 let prop_10 = time HOL_RULE
731 `(q ==> r) /\ (r ==> p /\ q) /\ (p ==> q /\ r) ==> (p <=> q)`;;
733 let prop_11 = time HOL_RULE
736 let prop_12 = time HOL_RULE
737 `((p <=> q) <=> r) <=> (p <=> (q <=> r))`;;
739 let prop_13 = time HOL_RULE
740 `p \/ q /\ r <=> (p \/ q) /\ (p \/ r)`;;
742 let prop_14 = time HOL_RULE
743 `(p <=> q) <=> (q \/ ~p) /\ (~q \/ p)`;;
745 let prop_15 = time HOL_RULE
746 `p ==> q <=> ~p \/ q`;;
748 let prop_16 = time HOL_RULE
749 `(p ==> q) \/ (q ==> p)`;;
751 let prop_17 = time HOL_RULE
752 `p /\ (q ==> r) ==> s <=> (~p \/ q \/ s) /\ (~p \/ ~r \/ s)`;;
754 (* ------------------------------------------------------------------------- *)
755 (* Congruence closure examples. *)
756 (* ------------------------------------------------------------------------- *)
759 `(f(f(f(f(f(x))))) = x) /\ (f(f(f(x))) = x) ==> (f(x) = x)`;;
762 `(f(f(f(f(f(f(x)))))) = x) /\ (f(f(f(f(x)))) = x) ==> (f(f(x)) = x)`;;
764 time HOL_RULE `(f a = a) ==> (f(f a) = a)`;;
767 `(a = f a) /\ ((g b (f a))=(f (f a))) /\ ((g a b)=(f (g b a)))
771 `((s(s(s(s(s(s(s(s(s(s(s(s(s(s(s a)))))))))))))))=a) /\
772 ((s (s (s (s (s (s (s (s (s (s a))))))))))=a) /\
773 ((s (s (s (s (s (s a))))))=a)
776 time HOL_RULE `(u = v) ==> (P u <=> P v)`;;
779 `(b + c + d + e + f + g + h + i + j + k + l + m =
780 m + l + k + j + i + h + g + f + e + d + c + b)
781 ==> (a + b + c + d + e + f + g + h + i + j + k + l + m =
782 a + m + l + k + j + i + h + g + f + e + d + c + b)`;;
785 `(f(f(f(f(a)))) = a) /\ (f(f(f(f(f(f(a)))))) = a) /\
786 something(irrelevant) /\ (11 + 12 = 23) /\
787 (f(f(f(f(b)))) = f(f(f(f(f(f(f(f(f(f(c))))))))))) /\
788 ~(otherthing) /\ ~(f(a) = a) /\ ~(f(b) = b) /\
789 P(f(f(f(a)))) ==> P(f(a))`;;
792 `((a = b) \/ (c = d)) /\ ((a = c) \/ (b = d)) ==> (a = d) \/ (b = c)`;;
794 (* ------------------------------------------------------------------------- *)
795 (* Various combined examples. *)
796 (* ------------------------------------------------------------------------- *)
799 `(f(f(f(f(a:A)))) = a) /\ (f(f(f(f(f(f(a)))))) = a) /\
800 something(irrelevant) /\ (11 + 12 = 23) /\
801 (f(f(f(f(b:A)))) = f(f(f(f(f(f(f(f(f(f(c))))))))))) /\
802 ~(otherthing) /\ ~(f(a) = a) /\ ~(f(b) = b) /\
803 P(f(a)) /\ ~(f(f(f(a))) = f(a)) ==> ?x. P(f(f(f(x))))`;;
806 `(f(f(f(f(a:A)))) = a) /\ (f(f(f(f(f(f(a)))))) = a) /\
807 something(irrelevant) /\ (11 + 12 = 23) /\
808 (f(f(f(f(b:A)))) = f(f(f(f(f(f(f(f(f(f(c))))))))))) /\
809 ~(otherthing) /\ ~(f(a) = a) /\ ~(f(b) = b) /\
814 `(f(f(f(f(a:A)))) = a) /\ (f(f(f(f(f(f(a)))))) = a) /\
815 something(irrelevant) /\ (11 + 12 = 23) /\
816 (f(f(f(f(b:A)))) = f(f(f(f(f(f(f(f(f(f(c))))))))))) /\
817 ~(otherthing) /\ ~(f(a) = a) /\ ~(f(b) = b) /\
819 ==> ?x. P(f(f(f(x))))`;;
822 `(a = f a) /\ ((g b (f a))=(f (f a))) /\ ((g a b)=(f (g b a))) /\
827 `(!x y. x + y = y + x) /\ (1 + 2 = x) /\ (x = 3) ==> (3 = 2 + 1)`;;
830 `(!x:num y. x + y = y + x) ==> (1 + 2 = 2 + 1)`;;
833 `(!x:num y. ~(x + y = y + x)) ==> ~(1 + 2 = 2 + 1)`;;
836 `(1 + 2 = 2 + 1) ==> ?x:num y. x + y = y + x`;;
839 `(1 + x = x + 1) ==> ?x:num y. x + y = y + x`;;
841 time (HOL_BY []) `?x. P x ==> !y. P y`;;
843 (* ------------------------------------------------------------------------- *)
844 (* Testing the HOL extensions. *)
845 (* ------------------------------------------------------------------------- *)
847 time HOL_RULE `1 + 1 = 2`;;
849 time HOL_RULE `(\x. x + 1) 2 = 2 + 1`;;
851 time HOL_RULE `!x. x < 2 ==> 2 * x <= 3`;;
853 time HOL_RULE `y IN {x | x < 2} <=> y < 2`;;
855 time HOL_RULE `(!x. (x = a) \/ x > a) ==> (1 + x = a) \/ 1 + x > a`;;
857 time HOL_RULE `(\(x,y). x + y)(1,2) + 5 = (1 + 2) + 5`;;
859 (* ------------------------------------------------------------------------- *)
860 (* These and only these should go to MESON. *)
861 (* ------------------------------------------------------------------------- *)
863 print_string "***** Now the following (only) should use MESON";
866 time HOL_RULE `?x y. x = y`;;
868 time HOL_RULE `(!Y X Z. p(X,Y) /\ p(Y,Z) ==> p(X,Z)) /\
869 (!Y X Z. q(X,Y) /\ q(Y,Z) ==> q(X,Z)) /\
870 (!Y X. q(X,Y) ==> q(Y,X)) /\
871 (!X Y. p(X,Y) \/ q(X,Y))
872 ==> p(a,b) \/ q(c,d)`;;
874 time HOL_BY [PAIR_EQ] `(1,2) IN {(x,y) | x < y} <=> 1 < 2`;;
876 HOL_BY [] `?x. !y. P x ==> P y`;;