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 (* ========================================================================= *)
12 (* ------------------------------------------------------------------------- *)
13 (* Some parameters controlling MESON behaviour. *)
14 (* ------------------------------------------------------------------------- *)
16 let meson_depth = ref false;; (* Use depth not inference bound. *)
18 let meson_prefine = ref true;; (* Use Plaisted's positive refinement. *)
20 let meson_dcutin = ref 1;; (* Min size for d-and-c optimization cut-in. *)
22 let meson_skew = ref 3;; (* Skew proof bias (one side is <= n / skew) *)
24 let meson_brand = ref false;; (* Use Brand transformation *)
26 let meson_split_limit = ref 8;; (* Limit of case splits before MESON proper *)
28 let meson_chatty = ref false;; (* Old-style verbose MESON output *)
30 (* ------------------------------------------------------------------------- *)
31 (* Prolog exception. *)
32 (* ------------------------------------------------------------------------- *)
36 (* ------------------------------------------------------------------------- *)
37 (* Shadow syntax for FOL terms in NNF. Functions and predicates have *)
38 (* numeric codes, and negation is done by negating the predicate code. *)
39 (* ------------------------------------------------------------------------- *)
41 type fol_term = Fvar of int
42 | Fnapp of int * fol_term list;;
44 type fol_atom = int * fol_term list;;
46 type fol_form = Atom of fol_atom
47 | Conj of fol_form * fol_form
48 | Disj of fol_form * fol_form
49 | Forallq of int * fol_form;;
51 (* ------------------------------------------------------------------------- *)
52 (* Type for recording a MESON proof tree. *)
53 (* ------------------------------------------------------------------------- *)
56 Subgoal of fol_atom * fol_goal list * (int * thm) *
57 int * (fol_term * int)list;;
59 (* ------------------------------------------------------------------------- *)
60 (* General MESON procedure, using assumptions and with settable limits. *)
61 (* ------------------------------------------------------------------------- *)
66 and inferences = ref 0 in
68 (* ----------------------------------------------------------------------- *)
69 (* Like partition, but with short-circuiting for special situation. *)
70 (* ----------------------------------------------------------------------- *)
73 let rec qpartition l =
74 if l == m then raise Unchanged else
77 | (h::t) -> if p h then
78 try let yes,no = qpartition t in h::yes,no
79 with Unchanged -> [h],t
81 let yes,no = qpartition t in yes,h::no in
82 function l -> try qpartition l
83 with Unchanged -> [],l in
85 (* ----------------------------------------------------------------------- *)
86 (* Translate a term (in NNF) into the shadow syntax. *)
87 (* ----------------------------------------------------------------------- *)
89 let reset_vars,fol_of_var,hol_of_var =
92 and vcounter = ref 0 in
96 if m >= offinc then failwith "inc_vcounter: too many variables" else
98 let reset_vars() = vstore := []; gstore := []; vcounter := 0 in
100 let currentvars = !vstore in
101 try assoc v currentvars with Failure _ ->
102 let n = inc_vcounter() in
103 vstore := (v,n)::currentvars; n in
105 try rev_assoc v (!vstore)
106 with Failure _ -> rev_assoc v (!gstore) in
107 let hol_of_bumped_var v =
108 try hol_of_var v with Failure _ ->
109 let v' = v mod offinc in
110 let hv' = hol_of_var v' in
111 let gv = genvar(type_of hv') in
112 gstore := (gv,v)::(!gstore); gv in
113 reset_vars,fol_of_var,hol_of_bumped_var in
115 let reset_consts,fol_of_const,hol_of_const =
116 let false_tm = `F` in
117 let cstore = ref ([]:(term * int)list)
118 and ccounter = ref 2 in
119 let reset_consts() = cstore := [false_tm,1]; ccounter := 2 in
121 let currentconsts = !cstore in
122 try assoc c currentconsts with Failure _ ->
124 ccounter := n + 1; cstore := (c,n)::currentconsts; n in
125 let hol_of_const c = rev_assoc c (!cstore) in
126 reset_consts,fol_of_const,hol_of_const in
128 let rec fol_of_term env consts tm =
129 if is_var tm & not (mem tm consts) then
132 let f,args = strip_comb tm in
133 if mem f env then failwith "fol_of_term: higher order" else
134 let ff = fol_of_const f in
135 Fnapp(ff,map (fol_of_term env consts) args) in
137 let fol_of_atom env consts tm =
138 let f,args = strip_comb tm in
139 if mem f env then failwith "fol_of_atom: higher order" else
140 let ff = fol_of_const f in
141 ff,map (fol_of_term env consts) args in
143 let fol_of_literal env consts tm =
144 try let tm' = dest_neg tm in
145 let p,a = fol_of_atom env consts tm' in
147 with Failure _ -> fol_of_atom env consts tm in
149 let rec fol_of_form env consts tm =
150 try let v,bod = dest_forall tm in
151 let fv = fol_of_var v in
152 let fbod = fol_of_form (v::env) (subtract consts [v]) bod in
154 with Failure _ -> try
155 let l,r = dest_conj tm in
156 let fl = fol_of_form env consts l
157 and fr = fol_of_form env consts r in
159 with Failure _ -> try
160 let l,r = dest_disj tm in
161 let fl = fol_of_form env consts l
162 and fr = fol_of_form env consts r in
165 Atom(fol_of_literal env consts tm) in
167 (* ----------------------------------------------------------------------- *)
168 (* Further translation functions for HOL formulas. *)
169 (* ----------------------------------------------------------------------- *)
171 let rec hol_of_term tm =
173 Fvar v -> hol_of_var v
174 | Fnapp(f,args) -> list_mk_comb(hol_of_const f,map hol_of_term args) in
176 let hol_of_atom (p,args) =
177 list_mk_comb(hol_of_const p,map hol_of_term args) in
179 let hol_of_literal (p,args) =
180 if p < 0 then mk_neg(hol_of_atom(-p,args))
181 else hol_of_atom (p,args) in
183 (* ----------------------------------------------------------------------- *)
184 (* Versions of shadow syntax operations with variable bumping. *)
185 (* ----------------------------------------------------------------------- *)
187 let rec fol_free_in v tm =
190 | Fnapp(_,lis) -> exists (fol_free_in v) lis in
192 let rec fol_subst theta tm =
194 Fvar v -> rev_assocd v theta tm
196 let args' = qmap (fol_subst theta) args in
197 if args' == args then tm else Fnapp(f,args') in
199 let fol_inst theta ((p,args) as at:fol_atom) =
200 let args' = qmap (fol_subst theta) args in
201 if args' == args then at else p,args' in
203 let rec fol_subst_bump offset theta tm =
205 Fvar v -> if v < offinc then
206 let v' = v + offset in
207 rev_assocd v' theta (Fvar(v'))
209 rev_assocd v theta tm
211 let args' = qmap (fol_subst_bump offset theta) args in
212 if args' == args then tm else Fnapp(f,args') in
214 let fol_inst_bump offset theta ((p,args) as at:fol_atom) =
215 let args' = qmap (fol_subst_bump offset theta) args in
216 if args' == args then at else p,args' in
218 (* ----------------------------------------------------------------------- *)
219 (* Main unification function, maintaining a "graph" instantiation. *)
220 (* We implicitly apply an offset to variables in the second term, so this *)
221 (* is not symmetric between the arguments. *)
222 (* ----------------------------------------------------------------------- *)
224 let rec istriv env x t =
227 (try let t' = rev_assoc y env in istriv env x t'
228 with Failure "find" -> false)
229 | Fnapp(f,args) -> exists (istriv env x) args & failwith "cyclic" in
231 let rec fol_unify offset tm1 tm2 sofar =
233 Fnapp(f,fargs),Fnapp(g,gargs) ->
234 if f <> g then failwith "" else
235 itlist2 (fol_unify offset) fargs gargs sofar
237 (let x' = x + offset in
238 try let tm2' = rev_assoc x' sofar in
239 fol_unify 0 tm1 tm2' sofar
240 with Failure "find" ->
241 if istriv sofar x' tm1 then sofar
242 else (tm1,x')::sofar)
244 (try let tm1' = rev_assoc x sofar in
245 fol_unify offset tm1' tm2 sofar
246 with Failure "find" ->
247 let tm2' = fol_subst_bump offset [] tm2 in
248 if istriv sofar x tm2' then sofar
249 else (tm2',x)::sofar) in
251 (* ----------------------------------------------------------------------- *)
252 (* Test for equality under the pending instantiations. *)
253 (* ----------------------------------------------------------------------- *)
255 let rec fol_eq insts tm1 tm2 =
258 Fnapp(f,fargs),Fnapp(g,gargs) ->
259 f = g & forall2 (fol_eq insts) fargs gargs
261 (try let tm2' = rev_assoc x insts in
262 fol_eq insts tm1 tm2'
263 with Failure "find" ->
264 try istriv insts x tm1 with Failure _ -> false)
266 (try let tm1' = rev_assoc x insts in
267 fol_eq insts tm1' tm2
268 with Failure "find" ->
269 try istriv insts x tm2 with Failure _ -> false) in
271 let fol_atom_eq insts (p1,args1) (p2,args2) =
272 p1 = p2 & forall2 (fol_eq insts) args1 args2 in
274 (* ----------------------------------------------------------------------- *)
275 (* Cacheing continuations. Very crude, but it works remarkably well. *)
276 (* ----------------------------------------------------------------------- *)
279 let memory = ref [] in
280 fun (gg,(insts,offset,size) as input) ->
281 if exists (fun (_,(insts',_,size')) ->
282 insts = insts' & (size <= size' or !meson_depth))
284 then failwith "cachecont"
285 else memory := input::(!memory); f input in
287 (* ----------------------------------------------------------------------- *)
288 (* Check ancestor list for repetition. *)
289 (* ----------------------------------------------------------------------- *)
291 let checkan insts (p,a) ancestors =
294 try let ours = assoc p' ancestors in
295 if exists (fun u -> fol_atom_eq insts t' (snd(fst u))) ours
296 then failwith "checkan"
298 with Failure "find" -> ancestors in
300 (* ----------------------------------------------------------------------- *)
301 (* Insert new goal's negation in ancestor clause, given refinement. *)
302 (* ----------------------------------------------------------------------- *)
304 let insertan insts (p,a) ancestors =
307 let ourancp,otheranc =
308 try remove (fun (pr,_) -> pr = p') ancestors
309 with Failure _ -> (p',[]),ancestors in
310 let ouranc = snd ourancp in
311 if exists (fun u -> fol_atom_eq insts t' (snd(fst u))) ouranc
312 then failwith "insertan: loop"
313 else (p',(([],t'),(0,TRUTH))::ouranc)::otheranc in
315 (* ----------------------------------------------------------------------- *)
316 (* Apply a multi-level "graph" instantiation. *)
317 (* ----------------------------------------------------------------------- *)
319 let rec fol_subst_partial insts tm =
321 Fvar(v) -> (try let t = rev_assoc v insts in
322 fol_subst_partial insts t
323 with Failure "find" -> tm)
324 | Fnapp(f,args) -> Fnapp(f,map (fol_subst_partial insts) args) in
326 (* ----------------------------------------------------------------------- *)
327 (* Tease apart local and global instantiations. *)
328 (* At the moment we also force a full evaluation; should eliminate this. *)
329 (* ----------------------------------------------------------------------- *)
331 let separate_insts offset oldinsts newinsts =
333 qpartition (fun (_,v) -> offset <= v) oldinsts newinsts in
334 if globins = oldinsts then
335 map (fun (t,x) -> fol_subst_partial newinsts t,x) locins,oldinsts
337 map (fun (t,x) -> fol_subst_partial newinsts t,x) locins,
338 map (fun (t,x) -> fol_subst_partial newinsts t,x) globins in
340 (* ----------------------------------------------------------------------- *)
341 (* Perform basic MESON expansion. *)
342 (* ----------------------------------------------------------------------- *)
344 let meson_single_expand loffset rule ((g,ancestors),(insts,offset,size)) =
345 let (hyps,conc),tag = rule in
346 let allins = rev_itlist2 (fol_unify loffset) (snd g) (snd conc) insts in
347 let locin,globin = separate_insts offset insts allins in
349 let h' = fol_inst_bump offset locin h in
350 h',checkan insts h' ancestors in
351 let newhyps = map mk_ihyp hyps in
352 inferences := !inferences + 1;
353 newhyps,(globin,offset+offinc,size-length hyps) in
355 (* ----------------------------------------------------------------------- *)
356 (* Perform first basic expansion which allows continuation call. *)
357 (* ----------------------------------------------------------------------- *)
359 let meson_expand_cont loffset rules state cont =
361 (fun r -> cont (snd r) (meson_single_expand loffset r state)) rules in
363 (* ----------------------------------------------------------------------- *)
364 (* Try expansion and continuation call with ancestor or initial rule. *)
365 (* ----------------------------------------------------------------------- *)
367 let meson_expand rules ((g,ancestors),((insts,offset,size) as tup)) cont =
369 let newancestors = insertan insts g ancestors in
370 let newstate = (g,newancestors),tup in
371 try if !meson_prefine & pr > 0 then failwith "meson_expand" else
372 let arules = assoc pr ancestors in
373 meson_expand_cont 0 arules newstate cont
374 with Cut -> failwith "meson_expand" | Failure _ ->
376 filter (fun ((h,_),_) -> length h <= size) (assoc pr rules) in
377 meson_expand_cont offset crules newstate cont
378 with Cut -> failwith "meson_expand"
379 | Failure _ -> failwith "meson_expand" in
381 (* ----------------------------------------------------------------------- *)
382 (* Simple Prolog engine organizing search and backtracking. *)
383 (* ----------------------------------------------------------------------- *)
385 let expand_goal rules =
386 let rec expand_goal depth ((g,_),(insts,offset,size) as state) cont =
387 if depth < 0 then failwith "expand_goal: too deep" else
388 meson_expand rules state
389 (fun apprule (_,(pinsts,_,_) as newstate) ->
390 expand_goals (depth-1) newstate
391 (cacheconts(fun (gs,(newinsts,newoffset,newsize)) ->
392 let locin,globin = separate_insts offset pinsts newinsts in
393 let g' = Subgoal(g,gs,apprule,offset,locin) in
394 if globin = insts & gs = [] then
395 try cont(g',(globin,newoffset,size))
396 with Failure _ -> raise Cut
398 try cont(g',(globin,newoffset,newsize))
399 with Cut -> failwith "expand_goal"
400 | Failure _ -> failwith "expand_goal")))
402 and expand_goals depth (gl,(insts,offset,size as tup)) cont =
406 | [g] -> expand_goal depth (g,tup) (fun (g',stup) -> cont([g'],stup))
408 | gl -> if size >= !meson_dcutin then
409 let lsize = size / (!meson_skew) in
410 let rsize = size - lsize in
411 let lgoals,rgoals = chop_list (length gl / 2) gl in
412 try expand_goals depth (lgoals,(insts,offset,lsize))
413 (cacheconts(fun (lg',(i,off,n)) ->
414 expand_goals depth (rgoals,(i,off,n + rsize))
415 (cacheconts(fun (rg',ztup) -> cont (lg'@rg',ztup)))))
417 expand_goals depth (rgoals,(insts,offset,lsize))
418 (cacheconts(fun (rg',(i,off,n)) ->
419 expand_goals depth (lgoals,(i,off,n + rsize))
420 (cacheconts (fun (lg',((_,_,fsize) as ztup)) ->
421 if n + rsize <= lsize + fsize
422 then failwith "repetition of demigoal pair"
423 else cont (lg'@rg',ztup)))))
426 expand_goal depth (g,tup)
427 (cacheconts(fun (g',stup) ->
428 expand_goals depth (gs,stup)
429 (cacheconts(fun (gs',ftup) -> cont(g'::gs',ftup))))) in
431 fun g maxdep maxinf cont ->
432 expand_goal maxdep (g,([],2 * offinc,maxinf)) cont in
434 (* ----------------------------------------------------------------------- *)
435 (* With iterative deepening of inferences or depth. *)
436 (* ----------------------------------------------------------------------- *)
438 let solve_goal rules incdepth min max incsize =
440 if n > max then failwith "solve_goal: Too deep" else
441 (if !meson_chatty & !verbose then
443 ((string_of_int (!inferences))^" inferences so far. "^
444 "Searching with maximum size "^(string_of_int n)^".");
445 Format.print_newline())
446 else if !verbose then
447 (Format.print_string(string_of_int (!inferences)^"..");
448 Format.print_flush())
451 if incdepth then expand_goal rules g n 100000 (fun x -> x)
452 else expand_goal rules g 100000 n (fun x -> x) in
453 (if !meson_chatty & !verbose then
455 ("Goal solved with "^(string_of_int (!inferences))^
457 Format.print_newline())
458 else if !verbose then
459 (Format.print_string("solved at "^string_of_int (!inferences));
460 Format.print_newline())
463 with Failure _ -> solve (n + incsize) g in
464 fun g -> solve min (g,[]) in
466 (* ----------------------------------------------------------------------- *)
467 (* Creation of tagged contrapositives from a HOL clause. *)
468 (* This includes any possible support clauses (1 = falsity). *)
469 (* The rules are partitioned into association lists. *)
470 (* ----------------------------------------------------------------------- *)
472 let fol_of_hol_clauses =
473 let eqt (a1,(b1,c1)) (a2, (b2,c2)) =
474 ((a1 = a2) & (b1 = b2) & (equals_thm c1 c2)) in
475 let mk_negated (p,a) = -p,a in
476 let rec mk_contraposes n th used unused sofar =
479 | h::t -> let nw = (map mk_negated (used @ t),h),(n,th) in
480 mk_contraposes (n + 1) th (used@[h]) t (nw::sofar) in
481 let fol_of_hol_clause th =
482 let lconsts = freesl (hyp th) in
484 let hlits = disjuncts tm in
485 let flits = map (fol_of_literal [] lconsts) hlits in
486 let basics = mk_contraposes 0 th [] flits [] in
487 if forall (fun (p,_) -> p < 0) flits then
488 ((map mk_negated flits,(1,[])),(-1,th))::basics
491 let rawrules = itlist (union' eqt o fol_of_hol_clause) thms [] in
492 let prs = setify (map (fst o snd o fst) rawrules) in
494 map (fun t -> t,filter ((=) t o fst o snd o fst) rawrules) prs in
495 let srules = sort (fun (p,_) (q,_) -> abs(p) <= abs(q)) prules in
498 (* ----------------------------------------------------------------------- *)
499 (* Optimize set of clauses; changing literal order complicates HOL stuff. *)
500 (* ----------------------------------------------------------------------- *)
503 let optimize_clause_order cls =
504 sort (fun ((l1,_),_) ((l2,_),_) -> length l1 <= length l2) cls in
505 map (fun (a,b) -> a,optimize_clause_order b) in
507 (* ----------------------------------------------------------------------- *)
508 (* Create a HOL contrapositive on demand, with a cache. *)
509 (* ----------------------------------------------------------------------- *)
511 let clear_contrapos_cache,make_hol_contrapos =
512 let DISJ_AC = AC DISJ_ACI
513 and imp_CONV = REWR_CONV(TAUT `a \/ b <=> ~b ==> a`)
515 GEN_REWRITE_CONV TOP_SWEEP_CONV
516 [TAUT `~(a \/ b) <=> ~a /\ ~b`; TAUT `~(~a) <=> a`]
517 and pull_CONV = GEN_REWRITE_CONV DEPTH_CONV
518 [TAUT `~a \/ ~b <=> ~(a /\ b)`]
519 and imf_CONV = REWR_CONV(TAUT `~p <=> p ==> F`) in
520 let memory = ref [] in
521 let clear_contrapos_cache() = memory := [] in
522 let make_hol_contrapos (n,th) =
525 try assoc key (!memory) with Failure _ ->
527 CONV_RULE (pull_CONV THENC imf_CONV) th
529 let djs = disjuncts tm in
531 if n = 0 then th else
532 let ldjs,rdjs = chop_list n djs in
533 let ndjs = (hd rdjs)::(ldjs@(tl rdjs)) in
534 EQ_MP (DISJ_AC(mk_eq(tm,list_mk_disj ndjs))) th in
536 if length djs = 1 then acth
537 else CONV_RULE (imp_CONV THENC push_CONV) acth in
538 (memory := (key,fth)::(!memory); fth) in
539 clear_contrapos_cache,make_hol_contrapos in
541 (* ----------------------------------------------------------------------- *)
542 (* Translate back the saved proof into HOL. *)
543 (* ----------------------------------------------------------------------- *)
547 try dest_neg tm with Failure _ -> mk_neg tm in
548 let merge_inst (t,x) current =
549 (fol_subst current t,x)::current in
552 [TAUT `(~p ==> p) <=> p`; TAUT `(p ==> ~p) <=> ~p`] in
553 let rec meson_to_hol insts (Subgoal(g,gs,(n,th),offset,locin)) =
554 let newins = itlist merge_inst locin insts in
555 let g' = fol_inst newins g in
556 let hol_g = hol_of_literal g' in
557 let ths = map (meson_to_hol newins) gs in
559 if equals_thm th TRUTH then ASSUME hol_g else
560 let cth = make_hol_contrapos(n,th) in
561 if ths = [] then cth else MATCH_MP cth (end_itlist CONJ ths) in
562 let ith = PART_MATCH I hth hol_g in
563 finish_RULE (DISCH (hol_negate(concl ith)) ith) in
566 (* ----------------------------------------------------------------------- *)
567 (* Create equality axioms for all the function and predicate symbols in *)
568 (* a HOL term. Not very efficient (but then neither is throwing them into *)
569 (* automated proof search!) *)
570 (* ----------------------------------------------------------------------- *)
572 let create_equality_axioms =
573 let eq_thms = (CONJUNCTS o prove)
575 (~(x:A = y) \/ ~(x = z) \/ (y = z))`,
576 REWRITE_TAC[] THEN ASM_CASES_TAC `x:A = y` THEN
577 ASM_REWRITE_TAC[] THEN CONV_TAC TAUT) in
578 let imp_elim_CONV = REWR_CONV
579 (TAUT `(a ==> b) <=> ~a \/ b`) in
581 MATCH_MP(TAUT `(a <=> b) ==> b \/ ~a`) in
582 let veq_tm = rator(rator(concl(hd eq_thms))) in
583 let create_equivalence_axioms (eq,_) =
584 let tyins = type_match (type_of veq_tm) (type_of eq) [] in
585 map (INST_TYPE tyins) eq_thms in
586 let rec tm_consts tm acc =
587 let fn,args = strip_comb tm in
588 if args = [] then acc
589 else itlist tm_consts args (insert (fn,length args) acc) in
590 let rec fm_consts tm ((preds,funs) as acc) =
591 try fm_consts(snd(dest_forall tm)) acc with Failure _ ->
592 try fm_consts(snd(dest_exists tm)) acc with Failure _ ->
593 try let l,r = dest_conj tm in fm_consts l (fm_consts r acc)
594 with Failure _ -> try
595 let l,r = dest_disj tm in fm_consts l (fm_consts r acc)
596 with Failure _ -> try
597 let l,r = dest_imp tm in fm_consts l (fm_consts r acc)
598 with Failure _ -> try
599 fm_consts (dest_neg tm) acc with Failure _ ->
600 try let l,r = dest_eq tm in
601 if type_of l = bool_ty
602 then fm_consts r (fm_consts l acc)
603 else failwith "atomic equality"
605 let pred,args = strip_comb tm in
606 if args = [] then acc else
607 insert (pred,length args) preds,itlist tm_consts args funs in
608 let create_congruence_axiom pflag (tm,len) =
609 let atys,rty = splitlist (fun ty -> let op,l = dest_type ty in
610 if op = "fun" then hd l,hd(tl l)
613 let ctys = fst(chop_list len atys) in
614 let largs = map genvar ctys
615 and rargs = map genvar ctys in
616 let th1 = rev_itlist (C (curry MK_COMB)) (map (ASSUME o mk_eq)
617 (zip largs rargs)) (REFL tm) in
618 let th2 = if pflag then eq_elim_RULE th1 else th1 in
619 itlist (fun e th -> CONV_RULE imp_elim_CONV (DISCH e th)) (hyp th2) th2 in
620 fun tms -> let preds,funs = itlist fm_consts tms ([],[]) in
621 let eqs0,noneqs = partition
622 (fun (t,_) -> is_const t & fst(dest_const t) = "=") preds in
623 if eqs0 = [] then [] else
624 let pcongs = map (create_congruence_axiom true) noneqs
625 and fcongs = map (create_congruence_axiom false) funs in
627 itlist fm_consts (map concl (pcongs @ fcongs)) ([],[]) in
629 (fun (t,_) -> is_const t & fst(dest_const t) = "=") preds1 in
630 let eqs = union eqs0 eqs1 in
632 itlist (union' equals_thm o create_equivalence_axioms)
634 equivs@pcongs@fcongs in
636 (* ----------------------------------------------------------------------- *)
637 (* Brand's transformation. *)
638 (* ----------------------------------------------------------------------- *)
640 let perform_brand_modification =
641 let rec subterms_irrefl lconsts tm acc =
642 if is_var tm or is_const tm then acc else
643 let fn,args = strip_comb tm in
644 itlist (subterms_refl lconsts) args acc
645 and subterms_refl lconsts tm acc =
646 if is_var tm then if mem tm lconsts then insert tm acc else acc
647 else if is_const tm then insert tm acc else
648 let fn,args = strip_comb tm in
649 itlist (subterms_refl lconsts) args (insert tm acc) in
650 let CLAUSIFY = CONV_RULE(REWR_CONV(TAUT `a ==> b <=> ~a \/ b`)) in
651 let rec BRAND tms th =
652 if tms = [] then th else
654 let gv = genvar (type_of tm) in
655 let eq = mk_eq(gv,tm) in
656 let th' = CLAUSIFY (DISCH eq (SUBS [SYM (ASSUME eq)] th))
657 and tms' = map (subst [gv,tm]) (tl tms) in
660 let lconsts = freesl (hyp th) in
661 let lits = disjuncts (concl th) in
662 let atoms = map (fun t -> try dest_neg t with Failure _ -> t) lits in
663 let eqs,noneqs = partition
664 (fun t -> try fst(dest_const(fst(strip_comb t))) = "="
665 with Failure _ -> false) atoms in
666 let acc = itlist (subterms_irrefl lconsts) noneqs [] in
668 (itlist (subterms_irrefl lconsts) o snd o strip_comb) eqs acc in
669 let sts = sort (fun s t -> not(free_in s t)) uts in
673 let l,r = dest_eq tm in
674 let gv = genvar(type_of l) in
675 let eq = mk_eq(r,gv) in
676 CLAUSIFY(DISCH eq (EQ_MP (AP_TERM (rator tm) (ASSUME eq)) th)) in
677 let LDISJ_CASES th lth rth =
678 DISJ_CASES th (DISJ1 lth (concl rth)) (DISJ2 (concl lth) rth) in
679 let ASSOCIATE = CONV_RULE(REWR_CONV(GSYM DISJ_ASSOC)) in
680 let rec BRAND_TRANS th =
682 try let l,r = dest_disj tm in
684 let lth = ASSUME l in
685 let lth1 = BRANDE lth
686 and lth2 = BRANDE (SYM lth)
687 and rth = BRAND_TRANS (ASSUME r) in
688 map (ASSOCIATE o LDISJ_CASES th lth1) rth @
689 map (ASSOCIATE o LDISJ_CASES th lth2) rth
691 let rth = BRAND_TRANS (ASSUME r) in
692 map (LDISJ_CASES th (ASSUME l)) rth
694 if is_eq tm then [BRANDE th; BRANDE (SYM th)]
697 find_terms (fun t -> try fst(dest_const t) = "="
698 with Failure _ -> false) in
700 let eqs = itlist (union o find_eqs o concl) ths [] in
701 let tys = map (hd o snd o dest_type o snd o dest_const) eqs in
702 let gvs = map genvar tys in
703 itlist (fun v acc -> (REFL v)::acc) gvs ths in
705 if exists (can (find_term is_eq o concl)) ths then
706 let ths' = map BRAND_CONGS ths in
707 let ths'' = itlist (union' equals_thm o BRAND_TRANS) ths' [] in
711 (* ----------------------------------------------------------------------- *)
712 (* Push duplicated copies of poly theorems to match existing assumptions. *)
713 (* ----------------------------------------------------------------------- *)
715 let POLY_ASSUME_TAC =
719 x::(y::_ as t) -> let t' = uniq' eq t in
720 if eq x y then t' else
721 if t'==t then l else x::t'
723 let setify' le eq s = uniq' eq (sort le s) in
724 let rec grab_constants tm acc =
725 if is_forall tm or is_exists tm then grab_constants (body(rand tm)) acc
726 else if is_iff tm or is_imp tm or is_conj tm or is_disj tm then
727 grab_constants (rand tm) (grab_constants (lhand tm) acc)
728 else if is_neg tm then grab_constants (rand tm) acc
729 else union (find_terms is_const tm) acc in
730 let match_consts (tm1,tm2) =
731 let s1,ty1 = dest_const tm1
732 and s2,ty2 = dest_const tm2 in
733 if s1 = s2 then type_match ty1 ty2 []
734 else failwith "match_consts" in
735 let polymorph mconsts th =
736 let tvs = subtract (type_vars_in_term (concl th))
737 (unions (map type_vars_in_term (hyp th))) in
738 if tvs = [] then [th] else
739 let pconsts = grab_constants (concl th) [] in
740 let tyins = mapfilter match_consts
741 (allpairs (fun x y -> x,y) pconsts mconsts) in
743 setify' (fun th th' -> dest_thm th <= dest_thm th')
744 equals_thm (mapfilter (C INST_TYPE th) tyins) in
746 (warn true "No useful-looking instantiations of lemma"; [th])
748 let rec polymorph_all mconsts ths acc =
749 if ths = [] then acc else
750 let ths' = polymorph mconsts (hd ths) in
751 let mconsts' = itlist grab_constants (map concl ths') mconsts in
752 polymorph_all mconsts' (tl ths) (union' equals_thm ths' acc) in
753 fun ths (asl,w as gl) ->
754 let mconsts = itlist (grab_constants o concl o snd) asl [] in
755 let ths' = polymorph_all mconsts ths [] in
756 MAP_EVERY ASSUME_TAC ths' gl in
758 (* ----------------------------------------------------------------------- *)
759 (* Basic HOL MESON procedure. *)
760 (* ----------------------------------------------------------------------- *)
762 let SIMPLE_MESON_REFUTE min max inc ths =
763 clear_contrapos_cache();
765 let old_dcutin = !meson_dcutin in
766 if !meson_depth then meson_dcutin := 100001 else ();
767 let ths' = if !meson_brand then perform_brand_modification ths
768 else ths @ create_equality_axioms (map concl ths) in
769 let rules = optimize_rules(fol_of_hol_clauses ths') in
770 let proof,(insts,_,_) =
771 solve_goal rules (!meson_depth) min max inc (1,[]) in
772 meson_dcutin := old_dcutin;
773 meson_to_hol insts proof in
775 let CONJUNCTS_THEN' ttac cth =
776 ttac(CONJUNCT1 cth) THEN ttac(CONJUNCT2 cth) in
778 let PURE_MESON_TAC min max inc gl =
779 reset_vars(); reset_consts();
780 (FIRST_ASSUM CONTR_TAC ORELSE
781 W(ACCEPT_TAC o SIMPLE_MESON_REFUTE min max inc o map snd o fst)) gl in
783 let QUANT_BOOL_CONV =
784 PURE_REWRITE_CONV[FORALL_BOOL_THM; EXISTS_BOOL_THM; COND_CLAUSES;
785 NOT_CLAUSES; IMP_CLAUSES; AND_CLAUSES; OR_CLAUSES;
786 EQ_CLAUSES; FORALL_SIMP; EXISTS_SIMP] in
788 let rec SPLIT_TAC n g =
789 ((FIRST_X_ASSUM(CONJUNCTS_THEN' ASSUME_TAC) THEN SPLIT_TAC n) ORELSE
790 (if n > 0 then FIRST_X_ASSUM DISJ_CASES_TAC THEN SPLIT_TAC (n - 1)
794 fun min max step ths ->
795 REFUTE_THEN ASSUME_TAC THEN
796 POLY_ASSUME_TAC (map GEN_ALL ths) THEN
797 W(MAP_EVERY(UNDISCH_TAC o concl o snd) o fst) THEN
799 W(fun (asl,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) THEN
800 CONV_TAC(PRESIMP_CONV THENC
801 TOP_DEPTH_CONV BETA_CONV THENC
802 LAMBDA_ELIM_CONV THENC
803 CONDS_CELIM_CONV THENC
804 QUANT_BOOL_CONV) THEN
805 REPEAT(GEN_TAC ORELSE DISCH_TAC) THEN
806 REFUTE_THEN ASSUME_TAC THEN
807 RULE_ASSUM_TAC(CONV_RULE(NNF_CONV THENC SKOLEM_CONV)) THEN
808 REPEAT (FIRST_X_ASSUM CHOOSE_TAC) THEN
810 SPLIT_TAC (!meson_split_limit) THEN
811 RULE_ASSUM_TAC(CONV_RULE(PRENEX_CONV THENC WEAK_CNF_CONV)) THEN
812 RULE_ASSUM_TAC(repeat
813 (fun th -> SPEC(genvar(type_of(fst(dest_forall(concl th))))) th)) THEN
814 REPEAT (FIRST_X_ASSUM (CONJUNCTS_THEN' ASSUME_TAC)) THEN
815 RULE_ASSUM_TAC(CONV_RULE(ASSOC_CONV DISJ_ASSOC)) THEN
816 REPEAT (FIRST_X_ASSUM SUBST_VAR_TAC) THEN
817 PURE_MESON_TAC min max step;;
819 (* ------------------------------------------------------------------------- *)
821 (* ------------------------------------------------------------------------- *)
823 let ASM_MESON_TAC = GEN_MESON_TAC 0 50 1;;
825 let MESON_TAC ths = POP_ASSUM_LIST(K ALL_TAC) THEN ASM_MESON_TAC ths;;
827 (* ------------------------------------------------------------------------- *)
828 (* Also introduce a rule. *)
829 (* ------------------------------------------------------------------------- *)
831 let MESON ths tm = prove(tm,MESON_TAC ths);;