1 (* ========================================================================= *)
2 (* Version of the MESON procedure a la PTTP. Various search options. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
13 module Meson_edit = struct
17 first-order formulas that occur in MESON_TAC calls.
20 (1) This just does MESON_TAC, ASM_MESON_TAC is similar.
21 (2) Right now, MESON_TAC runs twice. Optimize to remove.
25 flyspeck_needs "../development/thales/holcode/meson_edit.hl";;
26 let MESON_TAC=Meson_edit.MESON_SAVE_FOF_TAC;; (* redefine *)
27 reneeds"trigonometry/trig2.hl";; (* run file with modified meson *)
28 reneeds "../../hol_light/meson.ml";; (* restore MESON_TAC *)
29 !Meson_edit.fof_list;;
34 (* ------------------------------------------------------------------------- *)
35 (* Some parameters controlling MESON behaviour. *)
36 (* ------------------------------------------------------------------------- *)
39 let meson_depth = ref false;; (* Use depth not inference bound. *)
41 let meson_prefine = ref true;; (* Use Plaisted's positive refinement. *)
43 let meson_dcutin = ref 1;; (* Min size for d-and-c optimization cut-in. *)
45 let meson_skew = ref 3;; (* Skew proof bias (one side is <= n / skew) *)
47 let meson_brand = ref false;; (* Use Brand transformation *)
49 let meson_split_limit = ref 8;; (* Limit of case splits before MESON proper *)
51 let meson_chatty = ref false;; (* Old-style verbose MESON output *)
54 (* ------------------------------------------------------------------------- *)
55 (* Prolog exception. *)
56 (* ------------------------------------------------------------------------- *)
60 (* ------------------------------------------------------------------------- *)
61 (* Shadow syntax for FOL terms in NNF. Functions and predicates have *)
62 (* numeric codes, and negation is done by negating the predicate code. *)
63 (* ------------------------------------------------------------------------- *)
66 type fol_term = Fvar of int
67 | Fnapp of int * fol_term list;;
69 type fol_atom = int * fol_term list;;
71 type fol_form = Atom of fol_atom
72 | Conj of fol_form * fol_form
73 | Disj of fol_form * fol_form
74 | Forallq of int * fol_form;;
76 (* ------------------------------------------------------------------------- *)
77 (* Type for recording a MESON proof tree. *)
78 (* ------------------------------------------------------------------------- *)
81 Subgoal of fol_atom * fol_goal list * (int * thm) *
82 int * (fol_term * int)list;;
86 (* ------------------------------------------------------------------------- *)
87 (* General MESON procedure, using assumptions and with settable limits. *)
88 (* ------------------------------------------------------------------------- *)
92 let inferences = ref 0;;
94 (* ----------------------------------------------------------------------- *)
95 (* Like partition, but with short-circuiting for special situation. *)
96 (* ----------------------------------------------------------------------- *)
100 let rec qpartition l =
101 if l == m then raise Unchanged else
103 [] -> raise Unchanged
104 | (h::t) -> if p h then
105 try let yes,no = qpartition t in h::yes,no
106 with Unchanged -> [h],t
108 let yes,no = qpartition t in yes,h::no in
109 function l -> try qpartition l
110 with Unchanged -> [],l ;;
112 let reset_vars,fol_of_var,hol_of_var =
115 and vcounter = ref 0 in
119 if m >= offinc then failwith "inc_vcounter: too many variables" else
120 (vcounter := m; n) in
121 let reset_vars() = vstore := []; gstore := []; vcounter := 0 in
123 let currentvars = !vstore in
124 try assoc v currentvars with Failure _ ->
125 let n = inc_vcounter() in
126 vstore := (v,n)::currentvars; n in
128 try rev_assoc v (!vstore)
129 with Failure _ -> rev_assoc v (!gstore) in
130 let hol_of_bumped_var v =
131 try hol_of_var v with Failure _ ->
132 let v' = v mod offinc in
133 let hv' = hol_of_var v' in
134 let gv = genvar(type_of hv') in
135 gstore := (gv,v)::(!gstore); gv in
136 reset_vars,fol_of_var,hol_of_bumped_var ;;
138 fol_of_var `x:real`;;
141 let reset_consts,fol_of_const,hol_of_const =
142 let false_tm = `F` in
143 let cstore = ref ([]:(term * int)list)
144 and ccounter = ref 2 in
145 let reset_consts() = cstore := [false_tm,1]; ccounter := 2 in
147 let currentconsts = !cstore in
148 try assoc c currentconsts with Failure _ ->
150 ccounter := n + 1; cstore := (c,n)::currentconsts; n in
151 let hol_of_const c = rev_assoc c (!cstore) in
152 reset_consts,fol_of_const,hol_of_const ;;
158 let rec fol_of_term env consts tm =
159 if is_var tm & not (mem tm consts) then
162 let f,args = strip_comb tm in
163 if mem f env then failwith "fol_of_term: higher order" else
164 let ff = fol_of_const f in
165 Fnapp(ff,map (fol_of_term env consts) args) ;;
167 fol_of_term [] [] `sin x pow 2 + cos x pow 2`;;
170 let fol_of_atom env consts tm =
171 let f,args = strip_comb tm in
172 if mem f env then failwith "fol_of_atom: higher order" else
173 let ff = fol_of_const f in
174 ff,map (fol_of_term env consts) args ;;
176 fol_of_atom [] [] `cos x`;;
178 let fol_of_literal env consts tm =
179 try let tm' = dest_neg tm in
180 let p,a = fol_of_atom env consts tm' in
182 with Failure _ -> fol_of_atom env consts tm ;;
185 let rec fol_of_form env consts tm =
186 try let v,bod = dest_forall tm in
187 let fv = fol_of_var v in
188 let fbod = fol_of_form (v::env) (subtract consts [v]) bod in
190 with Failure _ -> try
191 let l,r = dest_conj tm in
192 let fl = fol_of_form env consts l
193 and fr = fol_of_form env consts r in
195 with Failure _ -> try
196 let l,r = dest_disj tm in
197 let fl = fol_of_form env consts l
198 and fr = fol_of_form env consts r in
201 Atom(fol_of_literal env consts tm) ;;
208 (* ----------------------------------------------------------------------- *)
209 (* Further translation functions for HOL formulas. *)
210 (* ----------------------------------------------------------------------- *)
212 let rec hol_of_term tm =
214 Fvar v -> hol_of_var v
215 | Fnapp(f,args) -> list_mk_comb(hol_of_const f,map hol_of_term args) ;;
217 let hol_of_atom (p,args) =
218 list_mk_comb(hol_of_const p,map hol_of_term args) ;;
220 let hol_of_literal (p,args) =
221 if p < 0 then mk_neg(hol_of_atom(-p,args))
222 else hol_of_atom (p,args) ;;
224 (* ----------------------------------------------------------------------- *)
225 (* Versions of shadow syntax operations with variable bumping. *)
226 (* ----------------------------------------------------------------------- *)
228 let rec fol_free_in v tm =
231 | Fnapp(_,lis) -> exists (fol_free_in v) lis ;;
233 let rec fol_subst theta tm =
235 Fvar v -> rev_assocd v theta tm
237 let args' = qmap (fol_subst theta) args in
238 if args' == args then tm else Fnapp(f,args') ;;
240 let fol_inst theta ((p,args) as at:fol_atom) =
241 let args' = qmap (fol_subst theta) args in
242 if args' == args then at else p,args' ;;
244 let rec fol_subst_bump offset theta tm =
246 Fvar v -> if v < offinc then
247 let v' = v + offset in
248 rev_assocd v' theta (Fvar(v'))
250 rev_assocd v theta tm
252 let args' = qmap (fol_subst_bump offset theta) args in
253 if args' == args then tm else Fnapp(f,args') ;;
255 let fol_inst_bump offset theta ((p,args) as at:fol_atom) =
256 let args' = qmap (fol_subst_bump offset theta) args in
257 if args' == args then at else p,args' ;;
260 let rec istriv env x t =
263 (try let t' = rev_assoc y env in istriv env x t'
264 with Failure "find" -> false)
265 | Fnapp(f,args) -> exists (istriv env x) args & failwith "cyclic" ;;
268 (* ----------------------------------------------------------------------- *)
269 (* Main unification function, maintaining a "graph" instantiation. *)
270 (* We implicitly apply an offset to variables in the second term, so this *)
271 (* is not symmetric between the arguments. *)
272 (* ----------------------------------------------------------------------- *)
274 let rec fol_unify offset tm1 tm2 sofar =
276 Fnapp(f,fargs),Fnapp(g,gargs) ->
277 if f <> g then failwith "" else
278 itlist2 (fol_unify offset) fargs gargs sofar
280 (let x' = x + offset in
281 try let tm2' = rev_assoc x' sofar in
282 fol_unify 0 tm1 tm2' sofar
283 with Failure "find" ->
284 if istriv sofar x' tm1 then sofar
285 else (tm1,x')::sofar)
287 (try let tm1' = rev_assoc x sofar in
288 fol_unify offset tm1' tm2 sofar
289 with Failure "find" ->
290 let tm2' = fol_subst_bump offset [] tm2 in
291 if istriv sofar x tm2' then sofar
292 else (tm2',x)::sofar) ;;
295 (* ----------------------------------------------------------------------- *)
296 (* Test for equality under the pending instantiations. *)
297 (* ----------------------------------------------------------------------- *)
299 let rec fol_eq insts tm1 tm2 =
302 Fnapp(f,fargs),Fnapp(g,gargs) ->
303 f = g & forall2 (fol_eq insts) fargs gargs
305 (try let tm2' = rev_assoc x insts in
306 fol_eq insts tm1 tm2'
307 with Failure "find" ->
308 try istriv insts x tm1 with Failure _ -> false)
310 (try let tm1' = rev_assoc x insts in
311 fol_eq insts tm1' tm2
312 with Failure "find" ->
313 try istriv insts x tm2 with Failure _ -> false) ;;
315 let fol_atom_eq insts (p1,args1) (p2,args2) =
316 p1 = p2 & forall2 (fol_eq insts) args1 args2 ;;
319 (* ----------------------------------------------------------------------- *)
320 (* Cacheing continuations. Very crude, but it works remarkably well. *)
321 (* ----------------------------------------------------------------------- *)
324 let memory = ref [] in
325 fun (gg,(insts,offset,size) as input) ->
326 if exists (fun (_,(insts',_,size')) ->
327 insts = insts' & (size <= size' or !meson_depth))
329 then failwith "cachecont"
330 else memory := input::(!memory); f input ;;
333 (* ----------------------------------------------------------------------- *)
334 (* Check ancestor list for repetition. *)
335 (* ----------------------------------------------------------------------- *)
337 let checkan insts (p,a) ancestors =
340 try let ours = assoc p' ancestors in
341 if exists (fun u -> fol_atom_eq insts t' (snd(fst u))) ours
342 then failwith "checkan"
344 with Failure "find" -> ancestors ;;
346 (* ----------------------------------------------------------------------- *)
347 (* Insert new goal's negation in ancestor clause, given refinement. *)
348 (* ----------------------------------------------------------------------- *)
350 let insertan insts (p,a) ancestors =
353 let ourancp,otheranc =
354 try remove (fun (pr,_) -> pr = p') ancestors
355 with Failure _ -> (p',[]),ancestors in
356 let ouranc = snd ourancp in
357 if exists (fun u -> fol_atom_eq insts t' (snd(fst u))) ouranc
358 then failwith "insertan: loop"
359 else (p',(([],t'),(0,TRUTH))::ouranc)::otheranc ;;
361 (* ----------------------------------------------------------------------- *)
362 (* Apply a multi-level "graph" instantiation. *)
363 (* ----------------------------------------------------------------------- *)
365 let rec fol_subst_partial insts tm =
367 Fvar(v) -> (try let t = rev_assoc v insts in
368 fol_subst_partial insts t
369 with Failure "find" -> tm)
370 | Fnapp(f,args) -> Fnapp(f,map (fol_subst_partial insts) args) ;;
372 (* ----------------------------------------------------------------------- *)
373 (* Tease apart local and global instantiations. *)
374 (* At the moment we also force a full evaluation; should eliminate this. *)
375 (* ----------------------------------------------------------------------- *)
377 let separate_insts offset oldinsts newinsts =
379 qpartition (fun (_,v) -> offset <= v) oldinsts newinsts in
380 if globins = oldinsts then
381 map (fun (t,x) -> fol_subst_partial newinsts t,x) locins,oldinsts
383 map (fun (t,x) -> fol_subst_partial newinsts t,x) locins,
384 map (fun (t,x) -> fol_subst_partial newinsts t,x) globins ;;
386 (* ----------------------------------------------------------------------- *)
387 (* Perform basic MESON expansion. *)
388 (* ----------------------------------------------------------------------- *)
390 let meson_single_expand loffset rule ((g,ancestors),(insts,offset,size)) =
391 let (hyps,conc),tag = rule in
392 let allins = rev_itlist2 (fol_unify loffset) (snd g) (snd conc) insts in
393 let locin,globin = separate_insts offset insts allins in
395 let h' = fol_inst_bump offset locin h in
396 h',checkan insts h' ancestors in
397 let newhyps = map mk_ihyp hyps in
398 inferences := !inferences + 1;
399 newhyps,(globin,offset+offinc,size-length hyps) ;;
401 (* ----------------------------------------------------------------------- *)
402 (* Perform first basic expansion which allows continuation call. *)
403 (* ----------------------------------------------------------------------- *)
405 let meson_expand_cont loffset rules state cont =
407 (fun r -> cont (snd r) (meson_single_expand loffset r state)) rules;;
409 (* ----------------------------------------------------------------------- *)
410 (* Try expansion and continuation call with ancestor or initial rule. *)
411 (* ----------------------------------------------------------------------- *)
413 let meson_expand rules ((g,ancestors),((insts,offset,size) as tup)) cont =
415 let newancestors = insertan insts g ancestors in
416 let newstate = (g,newancestors),tup in
417 try if !meson_prefine & pr > 0 then failwith "meson_expand" else
418 let arules = assoc pr ancestors in
419 meson_expand_cont 0 arules newstate cont
420 with Cut -> failwith "meson_expand" | Failure _ ->
422 filter (fun ((h,_),_) -> length h <= size) (assoc pr rules) in
423 meson_expand_cont offset crules newstate cont
424 with Cut -> failwith "meson_expand"
425 | Failure _ -> failwith "meson_expand" ;;
431 (* ----------------------------------------------------------------------- *)
432 (* Simple Prolog engine organizing search and backtracking. *)
433 (* ----------------------------------------------------------------------- *)
435 let expand_goal rules =
436 let rec expand_goal depth ((g,_),(insts,offset,size) as state) cont =
437 if depth < 0 then failwith "expand_goal: too deep" else
438 meson_expand rules state
439 (fun apprule (_,(pinsts,_,_) as newstate) ->
440 expand_goals (depth-1) newstate
441 (cacheconts(fun (gs,(newinsts,newoffset,newsize)) ->
442 let locin,globin = separate_insts offset pinsts newinsts in
443 let g' = Subgoal(g,gs,apprule,offset,locin) in
444 if globin = insts & gs = [] then
445 try cont(g',(globin,newoffset,size))
446 with Failure _ -> raise Cut
448 try cont(g',(globin,newoffset,newsize))
449 with Cut -> failwith "expand_goal"
450 | Failure _ -> failwith "expand_goal")))
452 and expand_goals depth (gl,(insts,offset,size as tup)) cont =
456 | [g] -> expand_goal depth (g,tup) (fun (g',stup) -> cont([g'],stup))
458 | gl -> if size >= !meson_dcutin then
459 let lsize = size / (!meson_skew) in
460 let rsize = size - lsize in
461 let lgoals,rgoals = chop_list (length gl / 2) gl in
462 try expand_goals depth (lgoals,(insts,offset,lsize))
463 (cacheconts(fun (lg',(i,off,n)) ->
464 expand_goals depth (rgoals,(i,off,n + rsize))
465 (cacheconts(fun (rg',ztup) -> cont (lg'@rg',ztup)))))
467 expand_goals depth (rgoals,(insts,offset,lsize))
468 (cacheconts(fun (rg',(i,off,n)) ->
469 expand_goals depth (lgoals,(i,off,n + rsize))
470 (cacheconts (fun (lg',((_,_,fsize) as ztup)) ->
471 if n + rsize <= lsize + fsize
472 then failwith "repetition of demigoal pair"
473 else cont (lg'@rg',ztup)))))
476 expand_goal depth (g,tup)
477 (cacheconts(fun (g',stup) ->
478 expand_goals depth (gs,stup)
479 (cacheconts(fun (gs',ftup) -> cont(g'::gs',ftup))))) in
481 fun g maxdep maxinf cont ->
482 expand_goal maxdep (g,([],2 * offinc,maxinf)) cont ;;
485 (* ----------------------------------------------------------------------- *)
486 (* With iterative deepening of inferences or depth. *)
487 (* ----------------------------------------------------------------------- *)
489 let solve_goal rules incdepth min max incsize =
491 if n > max then failwith "solve_goal: Too deep" else
492 (if !meson_chatty & !verbose then
494 ((string_of_int (!inferences))^" inferences so far. "^
495 "Searching with maximum size "^(string_of_int n)^".");
496 Format.print_newline())
497 else if !verbose then
498 (Format.print_string(string_of_int (!inferences)^"..");
499 Format.print_flush())
502 if incdepth then expand_goal rules g n 100000 (fun x -> x)
503 else expand_goal rules g 100000 n (fun x -> x) in
504 (if !meson_chatty & !verbose then
506 ("Goal solved with "^(string_of_int (!inferences))^
508 Format.print_newline())
509 else if !verbose then
510 (Format.print_string("solved at "^string_of_int (!inferences));
511 Format.print_newline())
514 with Failure _ -> solve (n + incsize) g in
515 fun g -> solve min (g,[]) ;;
517 (* ----------------------------------------------------------------------- *)
518 (* Creation of tagged contrapositives from a HOL clause. *)
519 (* This includes any possible support clauses (1 = falsity). *)
520 (* The rules are partitioned into association lists. *)
521 (* ----------------------------------------------------------------------- *)
523 let fol_of_hol_clauses =
524 let eqt (a1,(b1,c1)) (a2, (b2,c2)) =
525 ((a1 = a2) & (b1 = b2) & (equals_thm c1 c2)) in
526 let mk_negated (p,a) = -p,a in
527 let rec mk_contraposes n th used unused sofar =
530 | h::t -> let nw = (map mk_negated (used @ t),h),(n,th) in
531 mk_contraposes (n + 1) th (used@[h]) t (nw::sofar) in
532 let fol_of_hol_clause th =
533 let lconsts = freesl (hyp th) in
535 let hlits = disjuncts tm in
536 let flits = map (fol_of_literal [] lconsts) hlits in
537 let basics = mk_contraposes 0 th [] flits [] in
538 if forall (fun (p,_) -> p < 0) flits then
539 ((map mk_negated flits,(1,[])),(-1,th))::basics
542 let rawrules = itlist (union' eqt o fol_of_hol_clause) thms [] in
543 let prs = setify (map (fst o snd o fst) rawrules) in
545 map (fun t -> t,filter ((=) t o fst o snd o fst) rawrules) prs in
546 let srules = sort (fun (p,_) (q,_) -> abs(p) <= abs(q)) prules in
550 (* ----------------------------------------------------------------------- *)
551 (* Optimize set of clauses; changing literal order complicates HOL stuff. *)
552 (* ----------------------------------------------------------------------- *)
555 let optimize_clause_order cls =
556 sort (fun ((l1,_),_) ((l2,_),_) -> length l1 <= length l2) cls in
557 map (fun (a,b) -> a,optimize_clause_order b) ;;
560 (* ----------------------------------------------------------------------- *)
561 (* Create a HOL contrapositive on demand, with a cache. *)
562 (* ----------------------------------------------------------------------- *)
564 let clear_contrapos_cache,make_hol_contrapos =
565 let DISJ_AC = AC DISJ_ACI
566 and imp_CONV = REWR_CONV(TAUT `a \/ b <=> ~b ==> a`)
568 GEN_REWRITE_CONV TOP_SWEEP_CONV
569 [TAUT `~(a \/ b) <=> ~a /\ ~b`; TAUT `~(~a) <=> a`]
570 and pull_CONV = GEN_REWRITE_CONV DEPTH_CONV
571 [TAUT `~a \/ ~b <=> ~(a /\ b)`]
572 and imf_CONV = REWR_CONV(TAUT `~p <=> p ==> F`) in
573 let memory = ref [] in
574 let clear_contrapos_cache() = memory := [] in
575 let make_hol_contrapos (n,th) =
578 try assoc key (!memory) with Failure _ ->
580 CONV_RULE (pull_CONV THENC imf_CONV) th
582 let djs = disjuncts tm in
584 if n = 0 then th else
585 let ldjs,rdjs = chop_list n djs in
586 let ndjs = (hd rdjs)::(ldjs@(tl rdjs)) in
587 EQ_MP (DISJ_AC(mk_eq(tm,list_mk_disj ndjs))) th in
589 if length djs = 1 then acth
590 else CONV_RULE (imp_CONV THENC push_CONV) acth in
591 (memory := (key,fth)::(!memory); fth) in
592 clear_contrapos_cache,make_hol_contrapos ;;
595 (* ----------------------------------------------------------------------- *)
596 (* Translate back the saved proof into HOL. *)
597 (* ----------------------------------------------------------------------- *)
601 try dest_neg tm with Failure _ -> mk_neg tm in
602 let merge_inst (t,x) current =
603 (fol_subst current t,x)::current in
606 [TAUT `(~p ==> p) <=> p`; TAUT `(p ==> ~p) <=> ~p`] in
607 let rec meson_to_hol insts (Subgoal(g,gs,(n,th),offset,locin)) =
608 let newins = itlist merge_inst locin insts in
609 let g' = fol_inst newins g in
610 let hol_g = hol_of_literal g' in
611 let ths = map (meson_to_hol newins) gs in
613 if equals_thm th TRUTH then ASSUME hol_g else
614 let cth = make_hol_contrapos(n,th) in
615 if ths = [] then cth else MATCH_MP cth (end_itlist CONJ ths) in
616 let ith = PART_MATCH I hth hol_g in
617 finish_RULE (DISCH (hol_negate(concl ith)) ith) in
621 (* ----------------------------------------------------------------------- *)
622 (* Create equality axioms for all the function and predicate symbols in *)
623 (* a HOL term. Not very efficient (but then neither is throwing them into *)
624 (* automated proof search!) *)
625 (* ----------------------------------------------------------------------- *)
627 let create_equality_axioms =
628 let eq_thms = (CONJUNCTS o prove)
630 (~(x:A = y) \/ ~(x = z) \/ (y = z))`,
631 REWRITE_TAC[] THEN ASM_CASES_TAC `x:A = y` THEN
632 ASM_REWRITE_TAC[] THEN CONV_TAC TAUT) in
633 let imp_elim_CONV = REWR_CONV
634 (TAUT `(a ==> b) <=> ~a \/ b`) in
636 MATCH_MP(TAUT `(a <=> b) ==> b \/ ~a`) in
637 let veq_tm = rator(rator(concl(hd eq_thms))) in
638 let create_equivalence_axioms (eq,_) =
639 let tyins = type_match (type_of veq_tm) (type_of eq) [] in
640 map (INST_TYPE tyins) eq_thms in
641 let rec tm_consts tm acc =
642 let fn,args = strip_comb tm in
643 if args = [] then acc
644 else itlist tm_consts args (insert (fn,length args) acc) in
645 let rec fm_consts tm ((preds,funs) as acc) =
646 try fm_consts(snd(dest_forall tm)) acc with Failure _ ->
647 try fm_consts(snd(dest_exists tm)) acc with Failure _ ->
648 try let l,r = dest_conj tm in fm_consts l (fm_consts r acc)
649 with Failure _ -> try
650 let l,r = dest_disj tm in fm_consts l (fm_consts r acc)
651 with Failure _ -> try
652 let l,r = dest_imp tm in fm_consts l (fm_consts r acc)
653 with Failure _ -> try
654 fm_consts (dest_neg tm) acc with Failure _ ->
655 try let l,r = dest_eq tm in
656 if type_of l = bool_ty
657 then fm_consts r (fm_consts l acc)
658 else failwith "atomic equality"
660 let pred,args = strip_comb tm in
661 if args = [] then acc else
662 insert (pred,length args) preds,itlist tm_consts args funs in
663 let create_congruence_axiom pflag (tm,len) =
664 let atys,rty = splitlist (fun ty -> let op,l = dest_type ty in
665 if op = "fun" then hd l,hd(tl l)
668 let ctys = fst(chop_list len atys) in
669 let largs = map genvar ctys
670 and rargs = map genvar ctys in
671 let th1 = rev_itlist (C (curry MK_COMB)) (map (ASSUME o mk_eq)
672 (zip largs rargs)) (REFL tm) in
673 let th2 = if pflag then eq_elim_RULE th1 else th1 in
674 itlist (fun e th -> CONV_RULE imp_elim_CONV (DISCH e th)) (hyp th2) th2 in
675 fun tms -> let preds,funs = itlist fm_consts tms ([],[]) in
676 let eqs0,noneqs = partition
677 (fun (t,_) -> is_const t & fst(dest_const t) = "=") preds in
678 if eqs0 = [] then [] else
679 let pcongs = map (create_congruence_axiom true) noneqs
680 and fcongs = map (create_congruence_axiom false) funs in
682 itlist fm_consts (map concl (pcongs @ fcongs)) ([],[]) in
684 (fun (t,_) -> is_const t & fst(dest_const t) = "=") preds1 in
685 let eqs = union eqs0 eqs1 in
687 itlist (union' equals_thm o create_equivalence_axioms)
689 equivs@pcongs@fcongs ;;
691 (* ----------------------------------------------------------------------- *)
692 (* Brand's transformation. *)
693 (* ----------------------------------------------------------------------- *)
695 let perform_brand_modification =
696 let rec subterms_irrefl lconsts tm acc =
697 if is_var tm or is_const tm then acc else
698 let fn,args = strip_comb tm in
699 itlist (subterms_refl lconsts) args acc
700 and subterms_refl lconsts tm acc =
701 if is_var tm then if mem tm lconsts then insert tm acc else acc
702 else if is_const tm then insert tm acc else
703 let fn,args = strip_comb tm in
704 itlist (subterms_refl lconsts) args (insert tm acc) in
705 let CLAUSIFY = CONV_RULE(REWR_CONV(TAUT `a ==> b <=> ~a \/ b`)) in
706 let rec BRAND tms th =
707 if tms = [] then th else
709 let gv = genvar (type_of tm) in
710 let eq = mk_eq(gv,tm) in
711 let th' = CLAUSIFY (DISCH eq (SUBS [SYM (ASSUME eq)] th))
712 and tms' = map (subst [gv,tm]) (tl tms) in
715 let lconsts = freesl (hyp th) in
716 let lits = disjuncts (concl th) in
717 let atoms = map (fun t -> try dest_neg t with Failure _ -> t) lits in
718 let eqs,noneqs = partition
719 (fun t -> try fst(dest_const(fst(strip_comb t))) = "="
720 with Failure _ -> false) atoms in
721 let acc = itlist (subterms_irrefl lconsts) noneqs [] in
723 (itlist (subterms_irrefl lconsts) o snd o strip_comb) eqs acc in
724 let sts = sort (fun s t -> not(free_in s t)) uts in
728 let l,r = dest_eq tm in
729 let gv = genvar(type_of l) in
730 let eq = mk_eq(r,gv) in
731 CLAUSIFY(DISCH eq (EQ_MP (AP_TERM (rator tm) (ASSUME eq)) th)) in
732 let LDISJ_CASES th lth rth =
733 DISJ_CASES th (DISJ1 lth (concl rth)) (DISJ2 (concl lth) rth) in
734 let ASSOCIATE = CONV_RULE(REWR_CONV(GSYM DISJ_ASSOC)) in
735 let rec BRAND_TRANS th =
737 try let l,r = dest_disj tm in
739 let lth = ASSUME l in
740 let lth1 = BRANDE lth
741 and lth2 = BRANDE (SYM lth)
742 and rth = BRAND_TRANS (ASSUME r) in
743 map (ASSOCIATE o LDISJ_CASES th lth1) rth @
744 map (ASSOCIATE o LDISJ_CASES th lth2) rth
746 let rth = BRAND_TRANS (ASSUME r) in
747 map (LDISJ_CASES th (ASSUME l)) rth
749 if is_eq tm then [BRANDE th; BRANDE (SYM th)]
752 find_terms (fun t -> try fst(dest_const t) = "="
753 with Failure _ -> false) in
755 let eqs = itlist (union o find_eqs o concl) ths [] in
756 let tys = map (hd o snd o dest_type o snd o dest_const) eqs in
757 let gvs = map genvar tys in
758 itlist (fun v acc -> (REFL v)::acc) gvs ths in
760 if exists (can (find_term is_eq o concl)) ths then
761 let ths' = map BRAND_CONGS ths in
762 let ths'' = itlist (union' equals_thm o BRAND_TRANS) ths' [] in
767 (* ----------------------------------------------------------------------- *)
768 (* Push duplicated copies of poly theorems to match existing assumptions. *)
769 (* ----------------------------------------------------------------------- *)
771 let POLY_ASSUME_TAC =
775 x::(y::_ as t) -> let t' = uniq' eq t in
776 if eq x y then t' else
777 if t'==t then l else x::t'
779 let setify' le eq s = uniq' eq (sort le s) in
780 let rec grab_constants tm acc =
781 if is_forall tm or is_exists tm then grab_constants (body(rand tm)) acc
782 else if is_iff tm or is_imp tm or is_conj tm or is_disj tm then
783 grab_constants (rand tm) (grab_constants (lhand tm) acc)
784 else if is_neg tm then grab_constants (rand tm) acc
785 else union (find_terms is_const tm) acc in
786 let match_consts (tm1,tm2) =
787 let s1,ty1 = dest_const tm1
788 and s2,ty2 = dest_const tm2 in
789 if s1 = s2 then type_match ty1 ty2 []
790 else failwith "match_consts" in
791 let polymorph mconsts th =
792 let tvs = subtract (type_vars_in_term (concl th))
793 (unions (map type_vars_in_term (hyp th))) in
794 if tvs = [] then [th] else
795 let pconsts = grab_constants (concl th) [] in
796 let tyins = mapfilter match_consts
797 (allpairs (fun x y -> x,y) pconsts mconsts) in
799 setify' (fun th th' -> dest_thm th <= dest_thm th')
800 equals_thm (mapfilter (C INST_TYPE th) tyins) in
802 (warn true "No useful-looking instantiations of lemma"; [th])
804 let rec polymorph_all mconsts ths acc =
805 if ths = [] then acc else
806 let ths' = polymorph mconsts (hd ths) in
807 let mconsts' = itlist grab_constants (map concl ths') mconsts in
808 polymorph_all mconsts' (tl ths) (union' equals_thm ths' acc) in
809 fun ths (asl,w as gl) ->
810 let mconsts = itlist (grab_constants o concl o snd) asl [] in
811 let ths' = polymorph_all mconsts ths [] in
812 MAP_EVERY ASSUME_TAC ths' gl ;;
814 (* ----------------------------------------------------------------------- *)
815 (* Basic HOL MESON procedure. *)
816 (* ----------------------------------------------------------------------- *)
818 let SIMPLE_MESON_REFUTE min max inc ths =
819 clear_contrapos_cache();
821 let old_dcutin = !meson_dcutin in
822 if !meson_depth then meson_dcutin := 100001 else ();
823 let ths' = if !meson_brand then perform_brand_modification ths
824 else ths @ create_equality_axioms (map concl ths) in
825 let rules = optimize_rules(fol_of_hol_clauses ths') in
826 let proof,(insts,_,_) =
827 solve_goal rules (!meson_depth) min max inc (1,[]) in
828 meson_dcutin := old_dcutin;
829 meson_to_hol insts proof ;;
831 let PREP_SIMPLE_MESON_REFUTE ths =
832 clear_contrapos_cache();
834 let old_dcutin = !meson_dcutin in
835 if !meson_depth then meson_dcutin := 100001 else ();
836 let ths' = if !meson_brand then perform_brand_modification ths
837 else ths @ create_equality_axioms (map concl ths) in
838 optimize_rules(fol_of_hol_clauses ths') ;;
840 let CONJUNCTS_THEN' ttac cth =
841 ttac(CONJUNCT1 cth) THEN ttac(CONJUNCT2 cth) ;;
843 let PURE_MESON_TAC min max inc gl =
844 reset_vars(); reset_consts();
845 (FIRST_ASSUM CONTR_TAC ORELSE
846 W(ACCEPT_TAC o SIMPLE_MESON_REFUTE min max inc o map snd o fst)) gl ;;
848 let QUANT_BOOL_CONV =
849 PURE_REWRITE_CONV[FORALL_BOOL_THM; EXISTS_BOOL_THM; COND_CLAUSES;
850 NOT_CLAUSES; IMP_CLAUSES; AND_CLAUSES; OR_CLAUSES;
851 EQ_CLAUSES; FORALL_SIMP; EXISTS_SIMP] ;;
853 let rec SPLIT_TAC n g =
854 ((FIRST_X_ASSUM(CONJUNCTS_THEN' ASSUME_TAC) THEN SPLIT_TAC n) ORELSE
855 (if n > 0 then FIRST_X_ASSUM DISJ_CASES_TAC THEN SPLIT_TAC (n - 1)
860 let SHORT_PREP_MESON_TAC ths =
861 REFUTE_THEN ASSUME_TAC THEN
862 POLY_ASSUME_TAC (map GEN_ALL ths) THEN
863 W(MAP_EVERY(UNDISCH_TAC o concl o snd) o fst) THEN
865 W(fun (asl,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) THEN
866 CONV_TAC(PRESIMP_CONV THENC
867 TOP_DEPTH_CONV BETA_CONV THENC
868 LAMBDA_ELIM_CONV THENC
869 CONDS_CELIM_CONV THENC
870 QUANT_BOOL_CONV) THEN
871 REPEAT(GEN_TAC ORELSE DISCH_TAC) THEN
872 REFUTE_THEN ASSUME_TAC ;;
874 let PREP_MESON_TAC ths =
875 REFUTE_THEN ASSUME_TAC THEN
876 POLY_ASSUME_TAC (map GEN_ALL ths) THEN
877 W(MAP_EVERY(UNDISCH_TAC o concl o snd) o fst) THEN
879 W(fun (asl,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) THEN
880 CONV_TAC(PRESIMP_CONV THENC
881 TOP_DEPTH_CONV BETA_CONV THENC
882 LAMBDA_ELIM_CONV THENC
883 CONDS_CELIM_CONV THENC
884 QUANT_BOOL_CONV) THEN
885 REPEAT(GEN_TAC ORELSE DISCH_TAC) THEN
886 REFUTE_THEN ASSUME_TAC THEN
887 RULE_ASSUM_TAC(CONV_RULE(NNF_CONV THENC SKOLEM_CONV)) THEN
888 REPEAT (FIRST_X_ASSUM CHOOSE_TAC) THEN
890 SPLIT_TAC (!meson_split_limit) THEN
891 RULE_ASSUM_TAC(CONV_RULE(PRENEX_CONV THENC WEAK_CNF_CONV)) THEN
892 RULE_ASSUM_TAC(repeat
893 (fun th -> SPEC(genvar(type_of(fst(dest_forall(concl th))))) th)) THEN
894 REPEAT (FIRST_X_ASSUM (CONJUNCTS_THEN' ASSUME_TAC)) THEN
895 RULE_ASSUM_TAC(CONV_RULE(ASSOC_CONV DISJ_ASSOC)) THEN
896 REPEAT (FIRST_X_ASSUM SUBST_VAR_TAC);;
902 fun min max step ths ->
903 PREP_MESON_TAC ths THEN PURE_MESON_TAC min max step;;
906 (* ------------------------------------------------------------------------- *)
908 (* ------------------------------------------------------------------------- *)
910 let ASM_MESON_TAC = GEN_MESON_TAC 0 50 1;;
912 let MESON_TAC ths = POP_ASSUM_LIST(K ALL_TAC) THEN ASM_MESON_TAC ths;;
914 (* ------------------------------------------------------------------------- *)
915 (* Also introduce a rule. *)
916 (* ------------------------------------------------------------------------- *)
918 let MESON ths tm = prove(tm,MESON_TAC ths);;
922 let fof_list = ref [];;
924 let MESON_SAVE_FOF_TAC thms (asl,g) =
925 let (_,gs,_) = PREP_MESON_TAC thms (asl,g) in
927 let fof = PREP_SIMPLE_MESON_REFUTE (map snd (fst g')) in
928 let _ = fof_list := fof :: !fof_list in
929 MESON_TAC thms (asl,g);;
931 (* print first order formulas *)
933 let rec print_fol_term tm = match tm with
934 Fvar i -> print_string "Fvar("; print_int i; print_string ")"
935 | Fnapp (i,fls) -> print_string "Fnapp ("; print_int i;
937 do_list (fun t -> print_fol_term t;print_string ";") fls; print_string "])";;
939 let print_fol_atom (i,fls) =
940 print_int i; print_string ", [";
941 do_list (fun t -> print_fol_term t;print_string ";") fls; print_string "])";;
943 let rec print_fol_form fo = match fo with
944 | Atom a -> print_string "Atom("; print_fol_atom a; print_string ")"
945 | Conj(a,b) -> print_string "Conj("; print_fol_form a; print_string ","; print_fol_form b; print_string ")"
946 | Disj(a,b) -> print_string "Disj("; print_fol_form a; print_string ","; print_fol_form b; print_string ")"
947 | Forallq (i,f) -> print_string "Forallq("; print_int i; print_string ","; print_fol_form f; print_string ")";;
949 let (print_dl:((fol_atom list * (int * fol_term list)) * (int * thm))->unit)=
950 fun ((fas,(i,fts)),(k,th)) ->
952 do_list print_fol_atom fas;
953 print_string ",("; print_int i;
954 print_string ","; do_list print_fol_term fts;
955 print_string "),("; print_int k;
956 print_string ","; print_thm th; print_string ")) ";;
958 let print_data (i,dls) =
959 print_string "("; print_int i; print_string ",";
960 do_list print_dl dls; print_string ")\n\n";;