1 (* Title: HOL/Tools/meson.ML
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 The MESON resolution proof procedure for HOL.
5 When making clauses, avoids using the rewriter -- instead uses RS recursively.
10 val term_pair_of: indexname * (typ * 'a) -> term * 'a
11 val first_order_resolve: thm -> thm -> thm
12 val flexflex_first_order: thm -> thm
13 val size_of_subgoals: thm -> int
14 val too_many_clauses: Proof.context option -> term -> bool
15 val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
16 val finish_cnf: thm list -> thm list
17 val make_nnf: thm -> thm
18 val make_nnf1: thm -> thm
19 val skolemize: thm -> thm
20 val is_fol_term: theory -> term -> bool
21 val make_clauses: thm list -> thm list
22 val make_horns: thm list -> thm list
23 val best_prolog_tac: (thm -> int) -> thm list -> tactic
24 val depth_prolog_tac: thm list -> tactic
25 val gocls: thm list -> thm list
26 val skolemize_prems_tac: thm list -> int -> tactic
27 val MESON: (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic
28 val best_meson_tac: (thm -> int) -> int -> tactic
29 val safe_best_meson_tac: int -> tactic
30 val depth_meson_tac: int -> tactic
31 val prolog_step_tac': thm list -> int -> tactic
32 val iter_deepen_prolog_tac: thm list -> tactic
33 val iter_deepen_meson_tac: thm list -> int -> tactic
34 val make_meta_clause: thm -> thm
35 val make_meta_clauses: thm list -> thm list
36 val meson_claset_tac: thm list -> claset -> int -> tactic
37 val meson_tac: int -> tactic
38 val negate_head: thm -> thm
39 val select_literal: int -> thm -> thm
40 val skolemize_tac: int -> tactic
41 val setup: Context.theory -> Context.theory
44 structure Meson: MESON =
47 val max_clauses_default = 60;
48 val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
50 val not_conjD = thm "meson_not_conjD";
51 val not_disjD = thm "meson_not_disjD";
52 val not_notD = thm "meson_not_notD";
53 val not_allD = thm "meson_not_allD";
54 val not_exD = thm "meson_not_exD";
55 val imp_to_disjD = thm "meson_imp_to_disjD";
56 val not_impD = thm "meson_not_impD";
57 val iff_to_disjD = thm "meson_iff_to_disjD";
58 val not_iffD = thm "meson_not_iffD";
59 val conj_exD1 = thm "meson_conj_exD1";
60 val conj_exD2 = thm "meson_conj_exD2";
61 val disj_exD = thm "meson_disj_exD";
62 val disj_exD1 = thm "meson_disj_exD1";
63 val disj_exD2 = thm "meson_disj_exD2";
64 val disj_assoc = thm "meson_disj_assoc";
65 val disj_comm = thm "meson_disj_comm";
66 val disj_FalseD1 = thm "meson_disj_FalseD1";
67 val disj_FalseD2 = thm "meson_disj_FalseD2";
70 (**** Operators for forward proof ****)
73 (** First-order Resolution **)
75 fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
76 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
78 val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
80 (*FIXME: currently does not "rename variables apart"*)
81 fun first_order_resolve thA thB =
82 let val thy = theory_of_thm thA
83 val tmA = concl_of thA
84 val Const("==>",_) $ tmB $ _ = prop_of thB
85 val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0)
86 val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
87 in thA RS (cterm_instantiate ct_pairs thB) end
88 handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); (* FIXME avoid handle _ *)
90 fun flexflex_first_order th =
91 case (tpairs_of th) of
94 let val thy = theory_of_thm th
96 foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
97 val t_pairs = map term_pair_of (Vartab.dest tenv)
98 val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
102 (*Forward proof while preserving bound variables names*)
103 fun rename_bvs_RS th rl =
104 let val th' = th RS rl
105 in Thm.rename_boundvars (concl_of th') (concl_of th) th' end;
107 (*raises exception if no rules apply*)
108 fun tryres (th, rls) =
109 let fun tryall [] = raise THM("tryres", 0, th::rls)
110 | tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls)
113 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
114 e.g. from conj_forward, should have the form
115 "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
116 and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
117 fun forward_res nf st =
118 let fun forward_tacf [prem] = rtac (nf prem) 1
119 | forward_tacf prems =
120 error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
121 Display.string_of_thm st ^
123 ML_Syntax.print_list Display.string_of_thm prems)
125 case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
127 | NONE => raise THM("forward_res", 0, [st])
130 (*Are any of the logical connectives in "bs" present in the term?*)
132 let fun has (Const(a,_)) = false
133 | has (Const("Trueprop",_) $ p) = has p
134 | has (Const("Not",_) $ p) = has p
135 | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
136 | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
137 | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
138 | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
143 (**** Clause handling ****)
145 fun literals (Const("Trueprop",_) $ P) = literals P
146 | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
147 | literals (Const("Not",_) $ P) = [(false,P)]
148 | literals P = [(true,P)];
150 (*number of literals in a term*)
151 val nliterals = length o literals;
154 (*** Tautology Checking ***)
156 fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) =
157 signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
158 | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
159 | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
161 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
163 (*Literals like X=X are tautologous*)
164 fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u
165 | taut_poslit (Const("True",_)) = true
166 | taut_poslit _ = false;
169 let val (poslits,neglits) = signed_lits th
170 in exists taut_poslit poslits
172 exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
174 handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*)
177 (*** To remove trivial negated equality literals from clauses ***)
179 (*They are typically functional reflexivity axioms and are the converses of
180 injectivity equivalences*)
182 val not_refl_disj_D = thm"meson_not_refl_disj_D";
184 (*Is either term a Var that does not properly occur in the other term?*)
185 fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
186 | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
187 | eliminable _ = false;
189 fun refl_clause_aux 0 th = th
190 | refl_clause_aux n th =
191 case HOLogic.dest_Trueprop (concl_of th) of
192 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) =>
193 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
194 | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) =>
196 then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
197 else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
198 | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
199 | _ => (*not a disjunction*) th;
201 fun notequal_lits_count (Const ("op |", _) $ P $ Q) =
202 notequal_lits_count P + notequal_lits_count Q
203 | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
204 | notequal_lits_count _ = 0;
206 (*Simplify a clause by applying reflexivity to its negated equality literals*)
208 let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
209 in zero_var_indexes (refl_clause_aux neqs th) end
210 handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
213 (*** Removal of duplicate literals ***)
215 (*Forward proof, passing extra assumptions as theorems to the tactic*)
216 fun forward_res2 nf hyps st =
219 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
222 | NONE => raise THM("forward_res2", 0, [st]);
224 (*Remove duplicates in P|Q by assuming ~P in Q
225 rls (initially []) accumulates assumptions of the form P==>False*)
226 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
227 handle THM _ => tryres(th,rls)
228 handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
229 [disj_FalseD1, disj_FalseD2, asm_rl])
232 (*Remove duplicate literals, if there are any*)
234 if has_duplicates (op =) (literals (prop_of th))
235 then nodups_aux [] th
239 (*** The basic CNF transformation ***)
241 fun too_many_clauses ctxto t =
243 val max_cl = case ctxto of SOME ctxt => Config.get ctxt max_clauses
244 | NONE => max_clauses_default
246 fun sum x y = if x < max_cl andalso y < max_cl then x+y else max_cl;
247 fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
249 (*Estimate the number of clauses in order to detect infeasible theorems*)
250 fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
251 | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
252 | signed_nclauses b (Const("op &",_) $ t $ u) =
253 if b then sum (signed_nclauses b t) (signed_nclauses b u)
254 else prod (signed_nclauses b t) (signed_nclauses b u)
255 | signed_nclauses b (Const("op |",_) $ t $ u) =
256 if b then prod (signed_nclauses b t) (signed_nclauses b u)
257 else sum (signed_nclauses b t) (signed_nclauses b u)
258 | signed_nclauses b (Const("op -->",_) $ t $ u) =
259 if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
260 else sum (signed_nclauses (not b) t) (signed_nclauses b u)
261 | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
262 if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
263 if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
264 (prod (signed_nclauses (not b) u) (signed_nclauses b t))
265 else sum (prod (signed_nclauses b t) (signed_nclauses b u))
266 (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
268 | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
269 | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
270 | signed_nclauses _ _ = 1; (* literal *)
272 signed_nclauses true t >= max_cl
275 (*Replaces universally quantified variables by FREE variables -- because
276 assumptions may not contain scheme variables. Later, generalize using Variable.export. *)
278 val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
279 val spec_varT = #T (Thm.rep_cterm spec_var);
280 fun name_of (Const ("All", _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
282 fun freeze_spec th ctxt =
284 val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
285 val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt;
286 val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
287 in (th RS spec', ctxt') end
290 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
291 and then normalized via function nf. The normal form is given to resolve_tac,
292 instantiate a Boolean variable created by resolution with disj_forward. Since
293 (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
294 fun resop nf [prem] = resolve_tac (nf prem) 1;
296 (*Any need to extend this list with
297 "HOL.type_class","HOL.eq_class","Pure.term"?*)
299 exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1);
301 fun apply_skolem_ths (th, rls) =
302 let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
303 | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
306 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
307 Strips universal quantifiers and breaks up conjunctions.
308 Eliminates existential quantifiers using skoths: Skolemization theorems.*)
309 fun cnf skoths ctxt (th,ths) =
310 let val ctxtr = ref ctxt
311 fun cnf_aux (th,ths) =
312 if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
313 else if not (has_conns ["All","Ex","op &"] (prop_of th))
314 then nodups th :: ths (*no work to do, terminate*)
315 else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
316 Const ("op &", _) => (*conjunction*)
317 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
318 | Const ("All", _) => (*universal quantifier*)
319 let val (th',ctxt') = freeze_spec th (!ctxtr)
320 in ctxtr := ctxt'; cnf_aux (th', ths) end
322 (*existential quantifier: Insert Skolem functions*)
323 cnf_aux (apply_skolem_ths (th,skoths), ths)
324 | Const ("op |", _) =>
325 (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
326 all combinations of converting P, Q to CNF.*)
328 (METAHYPS (resop cnf_nil) 1) THEN
329 (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
330 in Seq.list_of (tac (th RS disj_forward)) @ ths end
331 | _ => nodups th :: ths (*no work to do*)
332 and cnf_nil th = cnf_aux (th,[])
334 if too_many_clauses (SOME ctxt) (concl_of th)
335 then (warning ("cnf is ignoring: " ^ Display.string_of_thm th); ths)
336 else cnf_aux (th,ths)
337 in (cls, !ctxtr) end;
339 fun make_cnf skoths th ctxt = cnf skoths ctxt (th, []);
341 (*Generalization, removal of redundant equalities, removal of tautologies.*)
342 fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
345 (**** Generation of contrapositives ****)
347 fun is_left (Const ("Trueprop", _) $
348 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
351 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
353 if is_left (prop_of th) then assoc_right (th RS disj_assoc)
356 (*Must check for negative literal first!*)
357 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
359 (*For ordinary resolution. *)
360 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
362 (*Create a goal or support clause, conclusing False*)
363 fun make_goal th = (*Must check for negative literal first!*)
364 make_goal (tryres(th, clause_rules))
365 handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
367 (*Sort clauses by number of literals*)
368 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
370 fun sort_clauses ths = sort (make_ord fewerlits) ths;
372 (*True if the given type contains bool anywhere*)
373 fun has_bool (Type("bool",_)) = true
374 | has_bool (Type(_, Ts)) = exists has_bool Ts
375 | has_bool _ = false;
377 (*Is the string the name of a connective? Really only | and Not can remain,
378 since this code expects to be called on a clause form.*)
379 val is_conn = member (op =)
380 ["Trueprop", "op &", "op |", "op -->", "Not",
381 "All", "Ex", "Ball", "Bex"];
383 (*True if the term contains a function--not a logical connective--where the type
384 of any argument contains bool.*)
385 val has_bool_arg_const =
387 (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
389 (*A higher-order instance of a first-order constant? Example is the definition of
390 HOL.one, 1, at a function type in theory SetsAndFunctions.*)
391 fun higher_inst_const thy (c,T) =
392 case binder_types T of
393 [] => false (*not a function type, OK*)
394 | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
396 (*Returns false if any Vars in the theorem mention type bool.
397 Also rejects functions whose arguments are Booleans or other functions.*)
398 fun is_fol_term thy t =
399 Term.is_first_order ["all","All","Ex"] t andalso
400 not (exists_subterm (fn Var (_, T) => has_bool T | _ => false) t orelse
401 has_bool_arg_const t orelse
402 exists_Const (higher_inst_const thy) t orelse
405 fun rigid t = not (is_Var (head_of t));
407 fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t
408 | ok4horn (Const ("Trueprop",_) $ t) = rigid t
411 (*Create a meta-level Horn clause*)
412 fun make_horn crules th =
413 if ok4horn (concl_of th)
414 then make_horn crules (tryres(th,crules)) handle THM _ => th
417 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
418 is a HOL disjunction.*)
419 fun add_contras crules (th,hcs) =
420 let fun rots (0,th) = hcs
421 | rots (k,th) = zero_var_indexes (make_horn crules th) ::
422 rots(k-1, assoc_right (th RS disj_comm))
423 in case nliterals(prop_of th) of
425 | n => rots(n, assoc_right th)
428 (*Use "theorem naming" to label the clauses*)
429 fun name_thms label =
430 let fun name1 (th, (k,ths)) =
431 (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
432 in fn ths => #2 (foldr name1 (length ths, []) ths) end;
434 (*Is the given disjunction an all-negative support clause?*)
435 fun is_negative th = forall (not o #1) (literals (prop_of th));
437 val neg_clauses = List.filter is_negative;
440 (***** MESON PROOF PROCEDURE *****)
442 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
443 As) = rhyps(phi, A::As)
444 | rhyps (_, As) = As;
446 (** Detecting repeated assumptions in a subgoal **)
448 (*The stringtree detects repeated assumptions.*)
449 fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
451 (*detects repetitions in a list of terms*)
452 fun has_reps [] = false
453 | has_reps [_] = false
454 | has_reps [t,u] = (t aconv u)
455 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false)
456 handle Net.INSERT => true;
458 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
459 fun TRYING_eq_assume_tac 0 st = Seq.single st
460 | TRYING_eq_assume_tac i st =
461 TRYING_eq_assume_tac (i-1) (eq_assumption i st)
462 handle THM _ => TRYING_eq_assume_tac (i-1) st;
464 fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
466 (*Loop checking: FAIL if trying to prove the same thing twice
467 -- if *ANY* subgoal has repeated literals*)
469 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
470 then Seq.empty else Seq.single st;
473 (* net_resolve_tac actually made it slower... *)
474 fun prolog_step_tac horns i =
475 (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
476 TRYALL_eq_assume_tac;
478 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
479 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
481 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
484 (*Negation Normal Form*)
485 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
486 not_impD, not_iffD, not_allD, not_exD, not_notD];
488 fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
489 | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
493 if ok4nnf (concl_of th)
494 then make_nnf1 (tryres(th, nnf_rls))
495 handle THM ("tryres", _, _) =>
496 forward_res make_nnf1
497 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
498 handle THM ("tryres", _, _) => th
501 (*The simplification removes defined quantifiers and occurrences of True and False.
502 nnf_ss also includes the one-point simprocs,
503 which are needed to avoid the various one-point theorems from generating junk clauses.*)
505 [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
506 if_False, if_cancel, if_eq_cancel, cases_simp];
507 val nnf_extra_simps =
508 thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
511 HOL_basic_ss addsimps nnf_extra_simps
512 addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
514 fun make_nnf th = case prems_of th of
515 [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
518 | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
520 (*Pull existential quantifiers to front. This accomplishes Skolemization for
521 clauses that arise from a subgoal.*)
523 if not (has_conns ["Ex"] (prop_of th)) then th
524 else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
525 disj_exD, disj_exD1, disj_exD2])))
526 handle THM ("tryres", _, _) =>
527 skolemize (forward_res skolemize
528 (tryres (th, [conj_forward, disj_forward, all_forward])))
529 handle THM ("tryres", _, _) =>
530 forward_res skolemize (rename_bvs_RS th ex_forward);
532 fun skolemize_nnf_list [] = []
533 | skolemize_nnf_list (th::ths) =
534 skolemize (make_nnf th) :: skolemize_nnf_list ths
535 handle THM _ => (*RS can fail if Unify.search_bound is too small*)
536 (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
537 skolemize_nnf_list ths);
539 fun add_clauses (th,cls) =
540 let val ctxt0 = Variable.thm_context th
541 val (cnfs,ctxt) = make_cnf [] th ctxt0
542 in Variable.export ctxt ctxt0 cnfs @ cls end;
544 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
545 The resulting clauses are HOL disjunctions.*)
546 fun make_clauses ths = sort_clauses (foldr add_clauses [] ths);
548 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
551 (distinct Thm.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
553 (*Could simply use nprems_of, which would count remaining subgoals -- no
554 discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
556 fun best_prolog_tac sizef horns =
557 BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
559 fun depth_prolog_tac horns =
560 DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
562 (*Return all negative clauses, as possible goal clauses*)
563 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
565 fun skolemize_prems_tac prems =
566 cut_facts_tac (skolemize_nnf_list prems) THEN'
569 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
570 Function mkcl converts theorems to clauses.*)
571 fun MESON mkcl cltac i st =
573 (EVERY [ObjectLogic.atomize_prems_tac 1,
576 EVERY1 [skolemize_prems_tac negs,
577 METAHYPS (cltac o mkcl)]) 1]) i st
578 handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
580 (** Best-first search versions **)
582 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
583 fun best_meson_tac sizef =
586 THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
587 (has_fewer_prems 1, sizef)
588 (prolog_step_tac (make_horns cls) 1));
590 (*First, breaks the goal into independent units*)
591 val safe_best_meson_tac =
592 SELECT_GOAL (TRY (CLASET safe_tac) THEN
593 TRYALL (best_meson_tac size_of_subgoals));
595 (** Depth-first search version **)
597 val depth_meson_tac =
599 (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
602 (** Iterative deepening version **)
604 (*This version does only one inference per call;
605 having only one eq_assume_tac speeds it up!*)
606 fun prolog_step_tac' horns =
607 let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
608 take_prefix Thm.no_prems horns
609 val nrtac = net_resolve_tac horns
610 in fn i => eq_assume_tac i ORELSE
611 match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*)
612 ((assume_tac i APPEND nrtac i) THEN check_tac)
615 fun iter_deepen_prolog_tac horns =
616 ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
618 fun iter_deepen_meson_tac ths = MESON make_clauses
620 case (gocls (cls@ths)) of
621 [] => no_tac (*no goal clauses*)
623 let val horns = make_horns (cls@ths)
625 Output.debug (fn () => ("meson method called:\n" ^
626 ML_Syntax.print_list Display.string_of_thm (cls@ths) ^
628 ML_Syntax.print_list Display.string_of_thm horns))
629 in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
633 fun meson_claset_tac ths cs =
634 SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
636 val meson_tac = CLASET' (meson_claset_tac []);
639 (**** Code to support ordinary resolution, rather than Model Elimination ****)
641 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
642 with no contrapositives, for ordinary resolution.*)
644 (*Rules to convert the head literal into a negated assumption. If the head
645 literal is already negated, then using notEfalse instead of notEfalse'
646 prevents a double negation.*)
647 val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
648 val notEfalse' = rotate_prems 1 notEfalse;
650 fun negated_asm_of_head th =
651 th RS notEfalse handle THM _ => th RS notEfalse';
653 (*Converting one theorem from a disjunction to a meta-level clause*)
654 fun make_meta_clause th =
655 let val (fth,thaw) = Drule.freeze_thaw_robust th
657 (zero_var_indexes o Thm.varifyT o thaw 0 o
658 negated_asm_of_head o make_horn resolution_clause_rules) fth
661 fun make_meta_clauses ths =
663 (distinct Thm.eq_thm_prop (map make_meta_clause ths));
665 (*Permute a rule's premises to move the i-th premise to the last position.*)
667 let val n = nprems_of th
668 in if 1 <= i andalso i <= n
669 then Thm.permute_prems (i-1) 1 th
670 else raise THM("select_literal", i, [th])
673 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
675 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
677 (*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
678 fun select_literal i cl = negate_head (make_last i cl);
681 (*Top-level Skolemization. Allows part of the conversion to clauses to be
682 expressed as a tactic (or Isar method). Each assumption of the selected
683 goal is converted to NNF and then its existential quantifiers are pulled
684 to the front. Finally, all existential quantifiers are eliminated,
685 leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
686 might generate many subgoals.*)
688 fun skolemize_tac i st =
689 let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
692 (fn hyps => (cut_facts_tac (skolemize_nnf_list hyps) 1
693 THEN REPEAT (etac exE 1))),
694 REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
696 handle Subscript => Seq.empty;