1 (* Title: HOL/Tools/meson.ML
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1992 University of Cambridge
6 The MESON resolution proof procedure for HOL.
8 When making clauses, avoids using the rewriter -- instead uses RS recursively
10 NEED TO SORT LITERALS BY # OF VARS, USING ==>I/E. ELIMINATES NEED FOR
11 FUNCTION nodups -- if done to goal clauses too!
16 val term_pair_of: indexname * (typ * 'a) -> term * 'a
17 val first_order_resolve: thm -> thm -> thm
18 val flexflex_first_order: thm -> thm
19 val size_of_subgoals: thm -> int
20 val too_many_clauses: term -> bool
21 val make_cnf: thm list -> thm -> thm list
22 val finish_cnf: thm list -> thm list
23 val generalize: thm -> thm
24 val make_nnf: thm -> thm
25 val make_nnf1: thm -> thm
26 val skolemize: thm -> thm
27 val is_fol_term: theory -> term -> bool
28 val make_clauses: thm list -> thm list
29 val make_horns: thm list -> thm list
30 val best_prolog_tac: (thm -> int) -> thm list -> tactic
31 val depth_prolog_tac: thm list -> tactic
32 val gocls: thm list -> thm list
33 val skolemize_prems_tac: thm list -> int -> tactic
34 val MESON: (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic
35 val best_meson_tac: (thm -> int) -> int -> tactic
36 val safe_best_meson_tac: int -> tactic
37 val depth_meson_tac: int -> tactic
38 val prolog_step_tac': thm list -> int -> tactic
39 val iter_deepen_prolog_tac: thm list -> tactic
40 val iter_deepen_meson_tac: thm list -> int -> tactic
41 val make_meta_clause: thm -> thm
42 val make_meta_clauses: thm list -> thm list
43 val meson_claset_tac: thm list -> claset -> int -> tactic
44 val meson_tac: int -> tactic
45 val negate_head: thm -> thm
46 val select_literal: int -> thm -> thm
47 val skolemize_tac: int -> tactic
50 structure Meson: MESON =
53 val not_conjD = thm "meson_not_conjD";
54 val not_disjD = thm "meson_not_disjD";
55 val not_notD = thm "meson_not_notD";
56 val not_allD = thm "meson_not_allD";
57 val not_exD = thm "meson_not_exD";
58 val imp_to_disjD = thm "meson_imp_to_disjD";
59 val not_impD = thm "meson_not_impD";
60 val iff_to_disjD = thm "meson_iff_to_disjD";
61 val not_iffD = thm "meson_not_iffD";
62 val conj_exD1 = thm "meson_conj_exD1";
63 val conj_exD2 = thm "meson_conj_exD2";
64 val disj_exD = thm "meson_disj_exD";
65 val disj_exD1 = thm "meson_disj_exD1";
66 val disj_exD2 = thm "meson_disj_exD2";
67 val disj_assoc = thm "meson_disj_assoc";
68 val disj_comm = thm "meson_disj_comm";
69 val disj_FalseD1 = thm "meson_disj_FalseD1";
70 val disj_FalseD2 = thm "meson_disj_FalseD2";
73 (**** Operators for forward proof ****)
76 (** First-order Resolution **)
78 fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
79 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
81 val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
83 (*FIXME: currently does not "rename variables apart"*)
84 fun first_order_resolve thA thB =
85 let val thy = theory_of_thm thA
86 val tmA = concl_of thA
87 val Const("==>",_) $ tmB $ _ = prop_of thB
88 val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0)
89 val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
90 in thA RS (cterm_instantiate ct_pairs thB) end
91 handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);
93 fun flexflex_first_order th =
94 case (tpairs_of th) of
97 let val thy = theory_of_thm th
99 foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
100 val t_pairs = map term_pair_of (Vartab.dest tenv)
101 val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
105 (*raises exception if no rules apply -- unlike RL*)
106 fun tryres (th, rls) =
107 let fun tryall [] = raise THM("tryres", 0, th::rls)
108 | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
111 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
112 e.g. from conj_forward, should have the form
113 "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
114 and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
115 fun forward_res nf st =
116 let fun forward_tacf [prem] = rtac (nf prem) 1
117 | forward_tacf prems =
118 error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
121 cat_lines (map string_of_thm prems))
123 case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
125 | NONE => raise THM("forward_res", 0, [st])
128 (*Are any of the logical connectives in "bs" present in the term?*)
130 let fun has (Const(a,_)) = false
131 | has (Const("Trueprop",_) $ p) = has p
132 | has (Const("Not",_) $ p) = has p
133 | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
134 | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
135 | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
136 | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
141 (**** Clause handling ****)
143 fun literals (Const("Trueprop",_) $ P) = literals P
144 | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
145 | literals (Const("Not",_) $ P) = [(false,P)]
146 | literals P = [(true,P)];
148 (*number of literals in a term*)
149 val nliterals = length o literals;
152 (*** Tautology Checking ***)
154 fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) =
155 signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
156 | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
157 | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
159 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
161 (*Literals like X=X are tautologous*)
162 fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u
163 | taut_poslit (Const("True",_)) = true
164 | taut_poslit _ = false;
167 let val (poslits,neglits) = signed_lits th
168 in exists taut_poslit poslits
170 exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
172 handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*)
175 (*** To remove trivial negated equality literals from clauses ***)
177 (*They are typically functional reflexivity axioms and are the converses of
178 injectivity equivalences*)
180 val not_refl_disj_D = thm"meson_not_refl_disj_D";
182 (*Is either term a Var that does not properly occur in the other term?*)
183 fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
184 | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
185 | eliminable _ = false;
187 fun refl_clause_aux 0 th = th
188 | refl_clause_aux n th =
189 case HOLogic.dest_Trueprop (concl_of th) of
190 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) =>
191 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
192 | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) =>
194 then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
195 else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
196 | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
197 | _ => (*not a disjunction*) th;
199 fun notequal_lits_count (Const ("op |", _) $ P $ Q) =
200 notequal_lits_count P + notequal_lits_count Q
201 | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
202 | notequal_lits_count _ = 0;
204 (*Simplify a clause by applying reflexivity to its negated equality literals*)
206 let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
207 in zero_var_indexes (refl_clause_aux neqs th) end
208 handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
211 (*** The basic CNF transformation ***)
213 val max_clauses = 40;
215 fun sum x y = if x < max_clauses andalso y < max_clauses then x+y else max_clauses;
216 fun prod x y = if x < max_clauses andalso y < max_clauses then x*y else max_clauses;
218 (*Estimate the number of clauses in order to detect infeasible theorems*)
219 fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
220 | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
221 | signed_nclauses b (Const("op &",_) $ t $ u) =
222 if b then sum (signed_nclauses b t) (signed_nclauses b u)
223 else prod (signed_nclauses b t) (signed_nclauses b u)
224 | signed_nclauses b (Const("op |",_) $ t $ u) =
225 if b then prod (signed_nclauses b t) (signed_nclauses b u)
226 else sum (signed_nclauses b t) (signed_nclauses b u)
227 | signed_nclauses b (Const("op -->",_) $ t $ u) =
228 if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
229 else sum (signed_nclauses (not b) t) (signed_nclauses b u)
230 | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
231 if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
232 if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
233 (prod (signed_nclauses (not b) u) (signed_nclauses b t))
234 else sum (prod (signed_nclauses b t) (signed_nclauses b u))
235 (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
237 | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
238 | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
239 | signed_nclauses _ _ = 1; (* literal *)
241 val nclauses = signed_nclauses true;
243 fun too_many_clauses t = nclauses t >= max_clauses;
245 (*Replaces universally quantified variables by FREE variables -- because
246 assumptions may not contain scheme variables. Later, we call "generalize". *)
248 let val newname = gensym "mes_"
249 val spec' = read_instantiate [("x", newname)] spec
252 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
253 and then normalized via function nf. The normal form is given to resolve_tac,
254 instantiate a Boolean variable created by resolution with disj_forward. Since
255 (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
256 fun resop nf [prem] = resolve_tac (nf prem) 1;
258 (*Any need to extend this list with
259 "HOL.type_class","HOL.eq_class","ProtoPure.term"?*)
261 exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1);
263 fun apply_skolem_ths (th, rls) =
264 let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
265 | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
268 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
269 Strips universal quantifiers and breaks up conjunctions.
270 Eliminates existential quantifiers using skoths: Skolemization theorems.*)
271 fun cnf skoths (th,ths) =
272 let fun cnf_aux (th,ths) =
273 if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
274 else if not (has_conns ["All","Ex","op &"] (prop_of th))
275 then th::ths (*no work to do, terminate*)
276 else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
277 Const ("op &", _) => (*conjunction*)
278 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
279 | Const ("All", _) => (*universal quantifier*)
280 cnf_aux (freeze_spec th, ths)
282 (*existential quantifier: Insert Skolem functions*)
283 cnf_aux (apply_skolem_ths (th,skoths), ths)
284 | Const ("op |", _) =>
285 (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
286 all combinations of converting P, Q to CNF.*)
288 (METAHYPS (resop cnf_nil) 1) THEN
289 (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
290 in Seq.list_of (tac (th RS disj_forward)) @ ths end
291 | _ => (*no work to do*) th::ths
292 and cnf_nil th = cnf_aux (th,[])
294 if too_many_clauses (concl_of th)
295 then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
296 else cnf_aux (th,ths)
299 fun all_names (Const ("all", _) $ Abs(x,_,P)) = x :: all_names P
302 fun new_names n [] = []
303 | new_names n (x::xs) =
304 if String.isPrefix "mes_" x then (x, radixstring(26,"A",n)) :: new_names (n+1) xs
307 (*The gensym names are ugly, so don't let the user see them. When forall_elim_vars
308 is called, it will ensure that no name clauses ensue.*)
310 let val old_names = all_names (prop_of th)
311 in Drule.rename_bvars (new_names 0 old_names) th end;
313 (*Convert all suitable free variables to schematic variables,
314 but don't discharge assumptions.*)
315 fun generalize th = Thm.varifyT (forall_elim_vars 0 (nice_names (forall_intr_frees th)));
317 fun make_cnf skoths th = cnf skoths (th, []);
319 (*Generalization, removal of redundant equalities, removal of tautologies.*)
320 fun finish_cnf ths = filter (not o is_taut) (map (refl_clause o generalize) ths);
323 (**** Removal of duplicate literals ****)
325 (*Forward proof, passing extra assumptions as theorems to the tactic*)
326 fun forward_res2 nf hyps st =
329 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
332 | NONE => raise THM("forward_res2", 0, [st]);
334 (*Remove duplicates in P|Q by assuming ~P in Q
335 rls (initially []) accumulates assumptions of the form P==>False*)
336 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
337 handle THM _ => tryres(th,rls)
338 handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
339 [disj_FalseD1, disj_FalseD2, asm_rl])
342 (*Remove duplicate literals, if there are any*)
344 if has_duplicates (op =) (literals (prop_of th))
345 then nodups_aux [] th
349 (**** Generation of contrapositives ****)
351 fun is_left (Const ("Trueprop", _) $
352 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
355 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
357 if is_left (prop_of th) then assoc_right (th RS disj_assoc)
360 (*Must check for negative literal first!*)
361 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
363 (*For ordinary resolution. *)
364 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
366 (*Create a goal or support clause, conclusing False*)
367 fun make_goal th = (*Must check for negative literal first!*)
368 make_goal (tryres(th, clause_rules))
369 handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
371 (*Sort clauses by number of literals*)
372 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
374 fun sort_clauses ths = sort (make_ord fewerlits) ths;
376 (*True if the given type contains bool anywhere*)
377 fun has_bool (Type("bool",_)) = true
378 | has_bool (Type(_, Ts)) = exists has_bool Ts
379 | has_bool _ = false;
381 (*Is the string the name of a connective? Really only | and Not can remain,
382 since this code expects to be called on a clause form.*)
383 val is_conn = member (op =)
384 ["Trueprop", "op &", "op |", "op -->", "Not",
385 "All", "Ex", "Ball", "Bex"];
387 (*True if the term contains a function--not a logical connective--where the type
388 of any argument contains bool.*)
389 val has_bool_arg_const =
391 (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
393 (*A higher-order instance of a first-order constant? Example is the definition of
394 HOL.one, 1, at a function type in theory SetsAndFunctions.*)
395 fun higher_inst_const thy (c,T) =
396 case binder_types T of
397 [] => false (*not a function type, OK*)
398 | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
400 (*Returns false if any Vars in the theorem mention type bool.
401 Also rejects functions whose arguments are Booleans or other functions.*)
402 fun is_fol_term thy t =
403 Term.is_first_order ["all","All","Ex"] t andalso
404 not (exists (has_bool o fastype_of) (term_vars t) orelse
405 has_bool_arg_const t orelse
406 exists_Const (higher_inst_const thy) t orelse
409 fun rigid t = not (is_Var (head_of t));
411 fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t
412 | ok4horn (Const ("Trueprop",_) $ t) = rigid t
415 (*Create a meta-level Horn clause*)
416 fun make_horn crules th =
417 if ok4horn (concl_of th)
418 then make_horn crules (tryres(th,crules)) handle THM _ => th
421 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
422 is a HOL disjunction.*)
423 fun add_contras crules (th,hcs) =
424 let fun rots (0,th) = hcs
425 | rots (k,th) = zero_var_indexes (make_horn crules th) ::
426 rots(k-1, assoc_right (th RS disj_comm))
427 in case nliterals(prop_of th) of
429 | n => rots(n, assoc_right th)
432 (*Use "theorem naming" to label the clauses*)
433 fun name_thms label =
434 let fun name1 (th, (k,ths)) =
435 (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths)
436 in fn ths => #2 (foldr name1 (length ths, []) ths) end;
438 (*Is the given disjunction an all-negative support clause?*)
439 fun is_negative th = forall (not o #1) (literals (prop_of th));
441 val neg_clauses = List.filter is_negative;
444 (***** MESON PROOF PROCEDURE *****)
446 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
447 As) = rhyps(phi, A::As)
448 | rhyps (_, As) = As;
450 (** Detecting repeated assumptions in a subgoal **)
452 (*The stringtree detects repeated assumptions.*)
453 fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
455 (*detects repetitions in a list of terms*)
456 fun has_reps [] = false
457 | has_reps [_] = false
458 | has_reps [t,u] = (t aconv u)
459 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false)
460 handle Net.INSERT => true;
462 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
463 fun TRYING_eq_assume_tac 0 st = Seq.single st
464 | TRYING_eq_assume_tac i st =
465 TRYING_eq_assume_tac (i-1) (eq_assumption i st)
466 handle THM _ => TRYING_eq_assume_tac (i-1) st;
468 fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
470 (*Loop checking: FAIL if trying to prove the same thing twice
471 -- if *ANY* subgoal has repeated literals*)
473 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
474 then Seq.empty else Seq.single st;
477 (* net_resolve_tac actually made it slower... *)
478 fun prolog_step_tac horns i =
479 (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
480 TRYALL_eq_assume_tac;
482 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
483 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
485 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
488 (*Negation Normal Form*)
489 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
490 not_impD, not_iffD, not_allD, not_exD, not_notD];
492 fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
493 | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
497 if ok4nnf (concl_of th)
498 then make_nnf1 (tryres(th, nnf_rls))
500 forward_res make_nnf1
501 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
505 (*The simplification removes defined quantifiers and occurrences of True and False.
506 nnf_ss also includes the one-point simprocs,
507 which are needed to avoid the various one-point theorems from generating junk clauses.*)
509 [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
510 if_False, if_cancel, if_eq_cancel, cases_simp];
511 val nnf_extra_simps =
512 thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
515 HOL_basic_ss addsimps nnf_extra_simps
516 addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
518 fun make_nnf th = case prems_of th of
519 [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
522 | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
524 (*Pull existential quantifiers to front. This accomplishes Skolemization for
525 clauses that arise from a subgoal.*)
527 if not (has_conns ["Ex"] (prop_of th)) then th
528 else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
529 disj_exD, disj_exD1, disj_exD2])))
531 skolemize (forward_res skolemize
532 (tryres (th, [conj_forward, disj_forward, all_forward])))
533 handle THM _ => forward_res skolemize (th RS ex_forward);
536 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
537 The resulting clauses are HOL disjunctions.*)
538 fun make_clauses ths =
539 (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
541 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
544 (distinct Thm.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
546 (*Could simply use nprems_of, which would count remaining subgoals -- no
547 discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
549 fun best_prolog_tac sizef horns =
550 BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
552 fun depth_prolog_tac horns =
553 DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
555 (*Return all negative clauses, as possible goal clauses*)
556 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
558 fun skolemize_prems_tac prems =
559 cut_facts_tac (map (skolemize o make_nnf) prems) THEN'
562 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
563 Function mkcl converts theorems to clauses.*)
564 fun MESON mkcl cltac i st =
566 (EVERY [ObjectLogic.atomize_prems_tac 1,
569 EVERY1 [skolemize_prems_tac negs,
570 METAHYPS (cltac o mkcl)]) 1]) i st
571 handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
573 (** Best-first search versions **)
575 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
576 fun best_meson_tac sizef =
579 THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
580 (has_fewer_prems 1, sizef)
581 (prolog_step_tac (make_horns cls) 1));
583 (*First, breaks the goal into independent units*)
584 val safe_best_meson_tac =
585 SELECT_GOAL (TRY (CLASET safe_tac) THEN
586 TRYALL (best_meson_tac size_of_subgoals));
588 (** Depth-first search version **)
590 val depth_meson_tac =
592 (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
595 (** Iterative deepening version **)
597 (*This version does only one inference per call;
598 having only one eq_assume_tac speeds it up!*)
599 fun prolog_step_tac' horns =
600 let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
601 take_prefix Thm.no_prems horns
602 val nrtac = net_resolve_tac horns
603 in fn i => eq_assume_tac i ORELSE
604 match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*)
605 ((assume_tac i APPEND nrtac i) THEN check_tac)
608 fun iter_deepen_prolog_tac horns =
609 ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
611 fun iter_deepen_meson_tac ths = MESON make_clauses
613 case (gocls (cls@ths)) of
614 [] => no_tac (*no goal clauses*)
616 let val horns = make_horns (cls@ths)
618 Output.debug (fn () => ("meson method called:\n" ^
619 space_implode "\n" (map string_of_thm (cls@ths)) ^
621 space_implode "\n" (map string_of_thm horns)))
622 in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
626 fun meson_claset_tac ths cs =
627 SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
629 val meson_tac = CLASET' (meson_claset_tac []);
632 (**** Code to support ordinary resolution, rather than Model Elimination ****)
634 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
635 with no contrapositives, for ordinary resolution.*)
637 (*Rules to convert the head literal into a negated assumption. If the head
638 literal is already negated, then using notEfalse instead of notEfalse'
639 prevents a double negation.*)
640 val notEfalse = read_instantiate [("R","False")] notE;
641 val notEfalse' = rotate_prems 1 notEfalse;
643 fun negated_asm_of_head th =
644 th RS notEfalse handle THM _ => th RS notEfalse';
646 (*Converting one clause*)
647 val make_meta_clause =
648 zero_var_indexes o negated_asm_of_head o make_horn resolution_clause_rules;
650 fun make_meta_clauses ths =
652 (distinct Thm.eq_thm_prop (map make_meta_clause ths));
654 (*Permute a rule's premises to move the i-th premise to the last position.*)
656 let val n = nprems_of th
657 in if 1 <= i andalso i <= n
658 then Thm.permute_prems (i-1) 1 th
659 else raise THM("select_literal", i, [th])
662 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
664 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
666 (*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
667 fun select_literal i cl = negate_head (make_last i cl);
670 (*Top-level Skolemization. Allows part of the conversion to clauses to be
671 expressed as a tactic (or Isar method). Each assumption of the selected
672 goal is converted to NNF and then its existential quantifiers are pulled
673 to the front. Finally, all existential quantifiers are eliminated,
674 leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
675 might generate many subgoals.*)
677 fun skolemize_tac i st =
678 let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
681 (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
682 THEN REPEAT (etac exE 1))),
683 REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
685 handle Subscript => Seq.empty;