moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
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
13 val term_pair_of: indexname * (typ * 'a) -> term * 'a
14 val first_order_resolve: thm -> thm -> thm
15 val flexflex_first_order: thm -> thm
16 val size_of_subgoals: thm -> int
17 val too_many_clauses: Proof.context option -> term -> bool
18 val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
19 val finish_cnf: thm list -> thm list
20 val make_nnf: thm -> thm
21 val make_nnf1: thm -> thm
22 val skolemize: thm -> thm
23 val is_fol_term: theory -> term -> bool
24 val make_clauses: thm list -> thm list
25 val make_horns: thm list -> thm list
26 val best_prolog_tac: (thm -> int) -> thm list -> tactic
27 val depth_prolog_tac: thm list -> tactic
28 val gocls: thm list -> thm list
29 val skolemize_prems_tac: thm list -> int -> tactic
30 val MESON: (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic
31 val best_meson_tac: (thm -> int) -> int -> tactic
32 val safe_best_meson_tac: int -> tactic
33 val depth_meson_tac: int -> tactic
34 val prolog_step_tac': thm list -> int -> tactic
35 val iter_deepen_prolog_tac: thm list -> tactic
36 val iter_deepen_meson_tac: thm list -> int -> tactic
37 val make_meta_clause: thm -> thm
38 val make_meta_clauses: thm list -> thm list
39 val meson_claset_tac: thm list -> claset -> int -> tactic
40 val meson_tac: int -> tactic
41 val negate_head: thm -> thm
42 val select_literal: int -> thm -> thm
43 val skolemize_tac: int -> tactic
44 val setup: Context.theory -> Context.theory
47 structure Meson: MESON =
50 val max_clauses_default = 60;
51 val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
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 (*Forward proof while preserving bound variables names*)
106 fun rename_bvs_RS th rl =
107 let val th' = th RS rl
108 in Thm.rename_boundvars (concl_of th') (concl_of th) th' end;
110 (*raises exception if no rules apply*)
111 fun tryres (th, rls) =
112 let fun tryall [] = raise THM("tryres", 0, th::rls)
113 | tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls)
116 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
117 e.g. from conj_forward, should have the form
118 "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
119 and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
120 fun forward_res nf st =
121 let fun forward_tacf [prem] = rtac (nf prem) 1
122 | forward_tacf prems =
123 error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
124 Display.string_of_thm st ^
126 cat_lines (map Display.string_of_thm prems))
128 case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
130 | NONE => raise THM("forward_res", 0, [st])
133 (*Are any of the logical connectives in "bs" present in the term?*)
135 let fun has (Const(a,_)) = false
136 | has (Const("Trueprop",_) $ p) = has p
137 | has (Const("Not",_) $ p) = has p
138 | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
139 | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
140 | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
141 | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
146 (**** Clause handling ****)
148 fun literals (Const("Trueprop",_) $ P) = literals P
149 | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
150 | literals (Const("Not",_) $ P) = [(false,P)]
151 | literals P = [(true,P)];
153 (*number of literals in a term*)
154 val nliterals = length o literals;
157 (*** Tautology Checking ***)
159 fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) =
160 signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
161 | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
162 | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
164 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
166 (*Literals like X=X are tautologous*)
167 fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u
168 | taut_poslit (Const("True",_)) = true
169 | taut_poslit _ = false;
172 let val (poslits,neglits) = signed_lits th
173 in exists taut_poslit poslits
175 exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
177 handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*)
180 (*** To remove trivial negated equality literals from clauses ***)
182 (*They are typically functional reflexivity axioms and are the converses of
183 injectivity equivalences*)
185 val not_refl_disj_D = thm"meson_not_refl_disj_D";
187 (*Is either term a Var that does not properly occur in the other term?*)
188 fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
189 | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
190 | eliminable _ = false;
192 fun refl_clause_aux 0 th = th
193 | refl_clause_aux n th =
194 case HOLogic.dest_Trueprop (concl_of th) of
195 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) =>
196 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
197 | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) =>
199 then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
200 else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
201 | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
202 | _ => (*not a disjunction*) th;
204 fun notequal_lits_count (Const ("op |", _) $ P $ Q) =
205 notequal_lits_count P + notequal_lits_count Q
206 | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
207 | notequal_lits_count _ = 0;
209 (*Simplify a clause by applying reflexivity to its negated equality literals*)
211 let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
212 in zero_var_indexes (refl_clause_aux neqs th) end
213 handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
216 (*** Removal of duplicate literals ***)
218 (*Forward proof, passing extra assumptions as theorems to the tactic*)
219 fun forward_res2 nf hyps st =
222 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
225 | NONE => raise THM("forward_res2", 0, [st]);
227 (*Remove duplicates in P|Q by assuming ~P in Q
228 rls (initially []) accumulates assumptions of the form P==>False*)
229 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
230 handle THM _ => tryres(th,rls)
231 handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
232 [disj_FalseD1, disj_FalseD2, asm_rl])
235 (*Remove duplicate literals, if there are any*)
237 if has_duplicates (op =) (literals (prop_of th))
238 then nodups_aux [] th
242 (*** The basic CNF transformation ***)
244 fun too_many_clauses ctxto t =
246 val max_cl = case ctxto of SOME ctxt => Config.get ctxt max_clauses
247 | NONE => max_clauses_default
249 fun sum x y = if x < max_cl andalso y < max_cl then x+y else max_cl;
250 fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
252 (*Estimate the number of clauses in order to detect infeasible theorems*)
253 fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
254 | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
255 | signed_nclauses b (Const("op &",_) $ t $ u) =
256 if b then sum (signed_nclauses b t) (signed_nclauses b u)
257 else prod (signed_nclauses b t) (signed_nclauses b u)
258 | signed_nclauses b (Const("op |",_) $ t $ u) =
259 if b then prod (signed_nclauses b t) (signed_nclauses b u)
260 else sum (signed_nclauses b t) (signed_nclauses b u)
261 | signed_nclauses b (Const("op -->",_) $ t $ u) =
262 if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
263 else sum (signed_nclauses (not b) t) (signed_nclauses b u)
264 | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
265 if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
266 if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
267 (prod (signed_nclauses (not b) u) (signed_nclauses b t))
268 else sum (prod (signed_nclauses b t) (signed_nclauses b u))
269 (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
271 | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
272 | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
273 | signed_nclauses _ _ = 1; (* literal *)
275 signed_nclauses true t >= max_cl
278 (*Replaces universally quantified variables by FREE variables -- because
279 assumptions may not contain scheme variables. Later, generalize using Variable.export. *)
281 val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
282 val spec_varT = #T (Thm.rep_cterm spec_var);
283 fun name_of (Const ("All", _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
285 fun freeze_spec th ctxt =
287 val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
288 val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt;
289 val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
290 in (th RS spec', ctxt') end
293 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
294 and then normalized via function nf. The normal form is given to resolve_tac,
295 instantiate a Boolean variable created by resolution with disj_forward. Since
296 (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
297 fun resop nf [prem] = resolve_tac (nf prem) 1;
299 (*Any need to extend this list with
300 "HOL.type_class","HOL.eq_class","Pure.term"?*)
302 exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1);
304 fun apply_skolem_ths (th, rls) =
305 let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
306 | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
309 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
310 Strips universal quantifiers and breaks up conjunctions.
311 Eliminates existential quantifiers using skoths: Skolemization theorems.*)
312 fun cnf skoths ctxt (th,ths) =
313 let val ctxtr = ref ctxt
314 fun cnf_aux (th,ths) =
315 if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
316 else if not (has_conns ["All","Ex","op &"] (prop_of th))
317 then nodups th :: ths (*no work to do, terminate*)
318 else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
319 Const ("op &", _) => (*conjunction*)
320 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
321 | Const ("All", _) => (*universal quantifier*)
322 let val (th',ctxt') = freeze_spec th (!ctxtr)
323 in ctxtr := ctxt'; cnf_aux (th', ths) end
325 (*existential quantifier: Insert Skolem functions*)
326 cnf_aux (apply_skolem_ths (th,skoths), ths)
327 | Const ("op |", _) =>
328 (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
329 all combinations of converting P, Q to CNF.*)
331 (METAHYPS (resop cnf_nil) 1) THEN
332 (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
333 in Seq.list_of (tac (th RS disj_forward)) @ ths end
334 | _ => nodups th :: ths (*no work to do*)
335 and cnf_nil th = cnf_aux (th,[])
337 if too_many_clauses (SOME ctxt) (concl_of th)
338 then (warning ("cnf is ignoring: " ^ Display.string_of_thm th); ths)
339 else cnf_aux (th,ths)
340 in (cls, !ctxtr) end;
342 fun make_cnf skoths th ctxt = cnf skoths ctxt (th, []);
344 (*Generalization, removal of redundant equalities, removal of tautologies.*)
345 fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
348 (**** Generation of contrapositives ****)
350 fun is_left (Const ("Trueprop", _) $
351 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
354 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
356 if is_left (prop_of th) then assoc_right (th RS disj_assoc)
359 (*Must check for negative literal first!*)
360 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
362 (*For ordinary resolution. *)
363 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
365 (*Create a goal or support clause, conclusing False*)
366 fun make_goal th = (*Must check for negative literal first!*)
367 make_goal (tryres(th, clause_rules))
368 handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
370 (*Sort clauses by number of literals*)
371 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
373 fun sort_clauses ths = sort (make_ord fewerlits) ths;
375 (*True if the given type contains bool anywhere*)
376 fun has_bool (Type("bool",_)) = true
377 | has_bool (Type(_, Ts)) = exists has_bool Ts
378 | has_bool _ = false;
380 (*Is the string the name of a connective? Really only | and Not can remain,
381 since this code expects to be called on a clause form.*)
382 val is_conn = member (op =)
383 ["Trueprop", "op &", "op |", "op -->", "Not",
384 "All", "Ex", "Ball", "Bex"];
386 (*True if the term contains a function--not a logical connective--where the type
387 of any argument contains bool.*)
388 val has_bool_arg_const =
390 (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
392 (*A higher-order instance of a first-order constant? Example is the definition of
393 HOL.one, 1, at a function type in theory SetsAndFunctions.*)
394 fun higher_inst_const thy (c,T) =
395 case binder_types T of
396 [] => false (*not a function type, OK*)
397 | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
399 (*Returns false if any Vars in the theorem mention type bool.
400 Also rejects functions whose arguments are Booleans or other functions.*)
401 fun is_fol_term thy t =
402 Term.is_first_order ["all","All","Ex"] t andalso
403 not (exists (has_bool o fastype_of) (term_vars t) orelse
404 has_bool_arg_const t orelse
405 exists_Const (higher_inst_const thy) t orelse
408 fun rigid t = not (is_Var (head_of t));
410 fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t
411 | ok4horn (Const ("Trueprop",_) $ t) = rigid t
414 (*Create a meta-level Horn clause*)
415 fun make_horn crules th =
416 if ok4horn (concl_of th)
417 then make_horn crules (tryres(th,crules)) handle THM _ => th
420 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
421 is a HOL disjunction.*)
422 fun add_contras crules (th,hcs) =
423 let fun rots (0,th) = hcs
424 | rots (k,th) = zero_var_indexes (make_horn crules th) ::
425 rots(k-1, assoc_right (th RS disj_comm))
426 in case nliterals(prop_of th) of
428 | n => rots(n, assoc_right th)
431 (*Use "theorem naming" to label the clauses*)
432 fun name_thms label =
433 let fun name1 (th, (k,ths)) =
434 (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
435 in fn ths => #2 (foldr name1 (length ths, []) ths) end;
437 (*Is the given disjunction an all-negative support clause?*)
438 fun is_negative th = forall (not o #1) (literals (prop_of th));
440 val neg_clauses = List.filter is_negative;
443 (***** MESON PROOF PROCEDURE *****)
445 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
446 As) = rhyps(phi, A::As)
447 | rhyps (_, As) = As;
449 (** Detecting repeated assumptions in a subgoal **)
451 (*The stringtree detects repeated assumptions.*)
452 fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
454 (*detects repetitions in a list of terms*)
455 fun has_reps [] = false
456 | has_reps [_] = false
457 | has_reps [t,u] = (t aconv u)
458 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false)
459 handle Net.INSERT => true;
461 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
462 fun TRYING_eq_assume_tac 0 st = Seq.single st
463 | TRYING_eq_assume_tac i st =
464 TRYING_eq_assume_tac (i-1) (eq_assumption i st)
465 handle THM _ => TRYING_eq_assume_tac (i-1) st;
467 fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
469 (*Loop checking: FAIL if trying to prove the same thing twice
470 -- if *ANY* subgoal has repeated literals*)
472 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
473 then Seq.empty else Seq.single st;
476 (* net_resolve_tac actually made it slower... *)
477 fun prolog_step_tac horns i =
478 (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
479 TRYALL_eq_assume_tac;
481 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
482 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
484 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
487 (*Negation Normal Form*)
488 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
489 not_impD, not_iffD, not_allD, not_exD, not_notD];
491 fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
492 | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
496 if ok4nnf (concl_of th)
497 then make_nnf1 (tryres(th, nnf_rls))
499 forward_res make_nnf1
500 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
504 (*The simplification removes defined quantifiers and occurrences of True and False.
505 nnf_ss also includes the one-point simprocs,
506 which are needed to avoid the various one-point theorems from generating junk clauses.*)
508 [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
509 if_False, if_cancel, if_eq_cancel, cases_simp];
510 val nnf_extra_simps =
511 thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
514 HOL_basic_ss addsimps nnf_extra_simps
515 addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
517 fun make_nnf th = case prems_of th of
518 [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
521 | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
523 (*Pull existential quantifiers to front. This accomplishes Skolemization for
524 clauses that arise from a subgoal.*)
526 if not (has_conns ["Ex"] (prop_of th)) then th
527 else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
528 disj_exD, disj_exD1, disj_exD2])))
530 skolemize (forward_res skolemize
531 (tryres (th, [conj_forward, disj_forward, all_forward])))
532 handle THM _ => forward_res skolemize (rename_bvs_RS th ex_forward);
534 fun skolemize_nnf_list [] = []
535 | skolemize_nnf_list (th::ths) =
536 skolemize (make_nnf th) :: skolemize_nnf_list ths
537 handle THM _ => (*RS can fail if Unify.search_bound is too small*)
538 (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
539 skolemize_nnf_list ths);
541 fun add_clauses (th,cls) =
542 let val ctxt0 = Variable.thm_context th
543 val (cnfs,ctxt) = make_cnf [] th ctxt0
544 in Variable.export ctxt ctxt0 cnfs @ cls end;
546 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
547 The resulting clauses are HOL disjunctions.*)
548 fun make_clauses ths = sort_clauses (foldr add_clauses [] ths);
550 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
553 (distinct Thm.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
555 (*Could simply use nprems_of, which would count remaining subgoals -- no
556 discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
558 fun best_prolog_tac sizef horns =
559 BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
561 fun depth_prolog_tac horns =
562 DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
564 (*Return all negative clauses, as possible goal clauses*)
565 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
567 fun skolemize_prems_tac prems =
568 cut_facts_tac (skolemize_nnf_list prems) THEN'
571 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
572 Function mkcl converts theorems to clauses.*)
573 fun MESON mkcl cltac i st =
575 (EVERY [ObjectLogic.atomize_prems_tac 1,
578 EVERY1 [skolemize_prems_tac negs,
579 METAHYPS (cltac o mkcl)]) 1]) i st
580 handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
582 (** Best-first search versions **)
584 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
585 fun best_meson_tac sizef =
588 THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
589 (has_fewer_prems 1, sizef)
590 (prolog_step_tac (make_horns cls) 1));
592 (*First, breaks the goal into independent units*)
593 val safe_best_meson_tac =
594 SELECT_GOAL (TRY (CLASET safe_tac) THEN
595 TRYALL (best_meson_tac size_of_subgoals));
597 (** Depth-first search version **)
599 val depth_meson_tac =
601 (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
604 (** Iterative deepening version **)
606 (*This version does only one inference per call;
607 having only one eq_assume_tac speeds it up!*)
608 fun prolog_step_tac' horns =
609 let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
610 take_prefix Thm.no_prems horns
611 val nrtac = net_resolve_tac horns
612 in fn i => eq_assume_tac i ORELSE
613 match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*)
614 ((assume_tac i APPEND nrtac i) THEN check_tac)
617 fun iter_deepen_prolog_tac horns =
618 ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
620 fun iter_deepen_meson_tac ths = MESON make_clauses
622 case (gocls (cls@ths)) of
623 [] => no_tac (*no goal clauses*)
625 let val horns = make_horns (cls@ths)
627 Output.debug (fn () => ("meson method called:\n" ^
628 cat_lines (map Display.string_of_thm (cls@ths)) ^
630 cat_lines (map Display.string_of_thm horns)))
631 in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
635 fun meson_claset_tac ths cs =
636 SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
638 val meson_tac = CLASET' (meson_claset_tac []);
641 (**** Code to support ordinary resolution, rather than Model Elimination ****)
643 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
644 with no contrapositives, for ordinary resolution.*)
646 (*Rules to convert the head literal into a negated assumption. If the head
647 literal is already negated, then using notEfalse instead of notEfalse'
648 prevents a double negation.*)
649 val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
650 val notEfalse' = rotate_prems 1 notEfalse;
652 fun negated_asm_of_head th =
653 th RS notEfalse handle THM _ => th RS notEfalse';
655 (*Converting one theorem from a disjunction to a meta-level clause*)
656 fun make_meta_clause th =
657 let val (fth,thaw) = Drule.freeze_thaw_robust th
659 (zero_var_indexes o Thm.varifyT o thaw 0 o
660 negated_asm_of_head o make_horn resolution_clause_rules) fth
663 fun make_meta_clauses ths =
665 (distinct Thm.eq_thm_prop (map make_meta_clause ths));
667 (*Permute a rule's premises to move the i-th premise to the last position.*)
669 let val n = nprems_of th
670 in if 1 <= i andalso i <= n
671 then Thm.permute_prems (i-1) 1 th
672 else raise THM("select_literal", i, [th])
675 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
677 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
679 (*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
680 fun select_literal i cl = negate_head (make_last i cl);
683 (*Top-level Skolemization. Allows part of the conversion to clauses to be
684 expressed as a tactic (or Isar method). Each assumption of the selected
685 goal is converted to NNF and then its existential quantifiers are pulled
686 to the front. Finally, all existential quantifiers are eliminated,
687 leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
688 might generate many subgoals.*)
690 fun skolemize_tac i st =
691 let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
694 (fn hyps => (cut_facts_tac (skolemize_nnf_list hyps) 1
695 THEN REPEAT (etac exE 1))),
696 REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
698 handle Subscript => Seq.empty;