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 skolemize: thm -> thm
19 val is_fol_term: theory -> term -> bool
20 val make_clauses: thm list -> thm list
21 val make_horns: thm list -> thm list
22 val best_prolog_tac: (thm -> int) -> thm list -> tactic
23 val depth_prolog_tac: thm list -> tactic
24 val gocls: thm list -> thm list
25 val skolemize_prems_tac: thm list -> int -> tactic
26 val MESON: (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic
27 val best_meson_tac: (thm -> int) -> int -> tactic
28 val safe_best_meson_tac: int -> tactic
29 val depth_meson_tac: int -> tactic
30 val prolog_step_tac': thm list -> int -> tactic
31 val iter_deepen_prolog_tac: thm list -> tactic
32 val iter_deepen_meson_tac: thm list -> int -> tactic
33 val make_meta_clause: thm -> thm
34 val make_meta_clauses: thm list -> thm list
35 val meson_claset_tac: thm list -> claset -> int -> tactic
36 val meson_tac: int -> tactic
37 val negate_head: thm -> thm
38 val select_literal: int -> thm -> thm
39 val skolemize_tac: int -> tactic
40 val setup: Context.theory -> Context.theory
43 structure Meson: MESON =
46 val max_clauses_default = 60;
47 val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
49 val not_conjD = thm "meson_not_conjD";
50 val not_disjD = thm "meson_not_disjD";
51 val not_notD = thm "meson_not_notD";
52 val not_allD = thm "meson_not_allD";
53 val not_exD = thm "meson_not_exD";
54 val imp_to_disjD = thm "meson_imp_to_disjD";
55 val not_impD = thm "meson_not_impD";
56 val iff_to_disjD = thm "meson_iff_to_disjD";
57 val not_iffD = thm "meson_not_iffD";
58 val conj_exD1 = thm "meson_conj_exD1";
59 val conj_exD2 = thm "meson_conj_exD2";
60 val disj_exD = thm "meson_disj_exD";
61 val disj_exD1 = thm "meson_disj_exD1";
62 val disj_exD2 = thm "meson_disj_exD2";
63 val disj_assoc = thm "meson_disj_assoc";
64 val disj_comm = thm "meson_disj_comm";
65 val disj_FalseD1 = thm "meson_disj_FalseD1";
66 val disj_FalseD2 = thm "meson_disj_FalseD2";
69 (**** Operators for forward proof ****)
72 (** First-order Resolution **)
74 fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
75 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
77 val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
79 (*FIXME: currently does not "rename variables apart"*)
80 fun first_order_resolve thA thB =
81 let val thy = theory_of_thm thA
82 val tmA = concl_of thA
83 val Const("==>",_) $ tmB $ _ = prop_of thB
84 val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0)
85 val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
86 in thA RS (cterm_instantiate ct_pairs thB) end
87 handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); (* FIXME avoid handle _ *)
89 fun flexflex_first_order th =
90 case (tpairs_of th) of
93 let val thy = theory_of_thm th
95 foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
96 val t_pairs = map term_pair_of (Vartab.dest tenv)
97 val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
101 (*Forward proof while preserving bound variables names*)
102 fun rename_bvs_RS th rl =
103 let val th' = th RS rl
104 in Thm.rename_boundvars (concl_of th') (concl_of th) th' end;
106 (*raises exception if no rules apply*)
107 fun tryres (th, rls) =
108 let fun tryall [] = raise THM("tryres", 0, th::rls)
109 | tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls)
112 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
113 e.g. from conj_forward, should have the form
114 "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
115 and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
116 fun forward_res nf st =
117 let fun forward_tacf [prem] = rtac (nf prem) 1
118 | forward_tacf prems =
119 error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
120 Display.string_of_thm st ^
122 ML_Syntax.print_list Display.string_of_thm prems)
124 case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
126 | NONE => raise THM("forward_res", 0, [st])
129 (*Are any of the logical connectives in "bs" present in the term?*)
131 let fun has (Const(a,_)) = false
132 | has (Const("Trueprop",_) $ p) = has p
133 | has (Const("Not",_) $ p) = has p
134 | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
135 | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
136 | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
137 | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
142 (**** Clause handling ****)
144 fun literals (Const("Trueprop",_) $ P) = literals P
145 | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
146 | literals (Const("Not",_) $ P) = [(false,P)]
147 | literals P = [(true,P)];
149 (*number of literals in a term*)
150 val nliterals = length o literals;
153 (*** Tautology Checking ***)
155 fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) =
156 signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
157 | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
158 | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
160 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
162 (*Literals like X=X are tautologous*)
163 fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u
164 | taut_poslit (Const("True",_)) = true
165 | taut_poslit _ = false;
168 let val (poslits,neglits) = signed_lits th
169 in exists taut_poslit poslits
171 exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
173 handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*)
176 (*** To remove trivial negated equality literals from clauses ***)
178 (*They are typically functional reflexivity axioms and are the converses of
179 injectivity equivalences*)
181 val not_refl_disj_D = thm"meson_not_refl_disj_D";
183 (*Is either term a Var that does not properly occur in the other term?*)
184 fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
185 | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
186 | eliminable _ = false;
188 fun refl_clause_aux 0 th = th
189 | refl_clause_aux n th =
190 case HOLogic.dest_Trueprop (concl_of th) of
191 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) =>
192 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
193 | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) =>
195 then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
196 else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
197 | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
198 | _ => (*not a disjunction*) th;
200 fun notequal_lits_count (Const ("op |", _) $ P $ Q) =
201 notequal_lits_count P + notequal_lits_count Q
202 | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
203 | notequal_lits_count _ = 0;
205 (*Simplify a clause by applying reflexivity to its negated equality literals*)
207 let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
208 in zero_var_indexes (refl_clause_aux neqs th) end
209 handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
212 (*** Removal of duplicate literals ***)
214 (*Forward proof, passing extra assumptions as theorems to the tactic*)
215 fun forward_res2 nf hyps st =
218 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
221 | NONE => raise THM("forward_res2", 0, [st]);
223 (*Remove duplicates in P|Q by assuming ~P in Q
224 rls (initially []) accumulates assumptions of the form P==>False*)
225 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
226 handle THM _ => tryres(th,rls)
227 handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
228 [disj_FalseD1, disj_FalseD2, asm_rl])
231 (*Remove duplicate literals, if there are any*)
233 if has_duplicates (op =) (literals (prop_of th))
234 then nodups_aux [] th
238 (*** The basic CNF transformation ***)
240 fun too_many_clauses ctxto t =
242 val max_cl = case ctxto of SOME ctxt => Config.get ctxt max_clauses
243 | NONE => max_clauses_default
245 fun sum x y = if x < max_cl andalso y < max_cl then x+y else max_cl;
246 fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
248 (*Estimate the number of clauses in order to detect infeasible theorems*)
249 fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
250 | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
251 | signed_nclauses b (Const("op &",_) $ t $ u) =
252 if b then sum (signed_nclauses b t) (signed_nclauses b u)
253 else prod (signed_nclauses b t) (signed_nclauses b u)
254 | signed_nclauses b (Const("op |",_) $ t $ u) =
255 if b then prod (signed_nclauses b t) (signed_nclauses b u)
256 else sum (signed_nclauses b t) (signed_nclauses b u)
257 | signed_nclauses b (Const("op -->",_) $ t $ u) =
258 if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
259 else sum (signed_nclauses (not b) t) (signed_nclauses b u)
260 | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
261 if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
262 if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
263 (prod (signed_nclauses (not b) u) (signed_nclauses b t))
264 else sum (prod (signed_nclauses b t) (signed_nclauses b u))
265 (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
267 | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
268 | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
269 | signed_nclauses _ _ = 1; (* literal *)
271 signed_nclauses true t >= max_cl
274 (*Replaces universally quantified variables by FREE variables -- because
275 assumptions may not contain scheme variables. Later, generalize using Variable.export. *)
277 val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
278 val spec_varT = #T (Thm.rep_cterm spec_var);
279 fun name_of (Const ("All", _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
281 fun freeze_spec th ctxt =
283 val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
284 val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt;
285 val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
286 in (th RS spec', ctxt') end
289 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
290 and then normalized via function nf. The normal form is given to resolve_tac,
291 instantiate a Boolean variable created by resolution with disj_forward. Since
292 (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
293 fun resop nf [prem] = resolve_tac (nf prem) 1;
295 (*Any need to extend this list with
296 "HOL.type_class","HOL.eq_class","Pure.term"?*)
298 exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
300 fun apply_skolem_ths (th, rls) =
301 let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
302 | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
305 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
306 Strips universal quantifiers and breaks up conjunctions.
307 Eliminates existential quantifiers using skoths: Skolemization theorems.*)
308 fun cnf skoths ctxt (th,ths) =
309 let val ctxtr = ref ctxt
310 fun cnf_aux (th,ths) =
311 if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
312 else if not (has_conns ["All","Ex","op &"] (prop_of th))
313 then nodups th :: ths (*no work to do, terminate*)
314 else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
315 Const ("op &", _) => (*conjunction*)
316 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
317 | Const ("All", _) => (*universal quantifier*)
318 let val (th',ctxt') = freeze_spec th (!ctxtr)
319 in ctxtr := ctxt'; cnf_aux (th', ths) end
321 (*existential quantifier: Insert Skolem functions*)
322 cnf_aux (apply_skolem_ths (th,skoths), ths)
323 | Const ("op |", _) =>
324 (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
325 all combinations of converting P, Q to CNF.*)
327 (METAHYPS (resop cnf_nil) 1) THEN
328 (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
329 in Seq.list_of (tac (th RS disj_forward)) @ ths end
330 | _ => nodups th :: ths (*no work to do*)
331 and cnf_nil th = cnf_aux (th,[])
333 if too_many_clauses (SOME ctxt) (concl_of th)
334 then (warning ("cnf is ignoring: " ^ Display.string_of_thm th); ths)
335 else cnf_aux (th,ths)
336 in (cls, !ctxtr) end;
338 fun make_cnf skoths th ctxt = cnf skoths ctxt (th, []);
340 (*Generalization, removal of redundant equalities, removal of tautologies.*)
341 fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
344 (**** Generation of contrapositives ****)
346 fun is_left (Const ("Trueprop", _) $
347 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
350 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
352 if is_left (prop_of th) then assoc_right (th RS disj_assoc)
355 (*Must check for negative literal first!*)
356 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
358 (*For ordinary resolution. *)
359 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
361 (*Create a goal or support clause, conclusing False*)
362 fun make_goal th = (*Must check for negative literal first!*)
363 make_goal (tryres(th, clause_rules))
364 handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
366 (*Sort clauses by number of literals*)
367 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
369 fun sort_clauses ths = sort (make_ord fewerlits) ths;
371 (*True if the given type contains bool anywhere*)
372 fun has_bool (Type("bool",_)) = true
373 | has_bool (Type(_, Ts)) = exists has_bool Ts
374 | has_bool _ = false;
376 (*Is the string the name of a connective? Really only | and Not can remain,
377 since this code expects to be called on a clause form.*)
378 val is_conn = member (op =)
379 ["Trueprop", "op &", "op |", "op -->", "Not",
380 "All", "Ex", "Ball", "Bex"];
382 (*True if the term contains a function--not a logical connective--where the type
383 of any argument contains bool.*)
384 val has_bool_arg_const =
386 (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
388 (*A higher-order instance of a first-order constant? Example is the definition of
389 HOL.one, 1, at a function type in theory SetsAndFunctions.*)
390 fun higher_inst_const thy (c,T) =
391 case binder_types T of
392 [] => false (*not a function type, OK*)
393 | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
395 (*Returns false if any Vars in the theorem mention type bool.
396 Also rejects functions whose arguments are Booleans or other functions.*)
397 fun is_fol_term thy t =
398 Term.is_first_order ["all","All","Ex"] t andalso
399 not (exists_subterm (fn Var (_, T) => has_bool T | _ => false) t orelse
400 has_bool_arg_const t orelse
401 exists_Const (higher_inst_const thy) t orelse
404 fun rigid t = not (is_Var (head_of t));
406 fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t
407 | ok4horn (Const ("Trueprop",_) $ t) = rigid t
410 (*Create a meta-level Horn clause*)
411 fun make_horn crules th =
412 if ok4horn (concl_of th)
413 then make_horn crules (tryres(th,crules)) handle THM _ => th
416 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
417 is a HOL disjunction.*)
418 fun add_contras crules (th,hcs) =
419 let fun rots (0,th) = hcs
420 | rots (k,th) = zero_var_indexes (make_horn crules th) ::
421 rots(k-1, assoc_right (th RS disj_comm))
422 in case nliterals(prop_of th) of
424 | n => rots(n, assoc_right th)
427 (*Use "theorem naming" to label the clauses*)
428 fun name_thms label =
429 let fun name1 (th, (k,ths)) =
430 (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
431 in fn ths => #2 (foldr name1 (length ths, []) ths) end;
433 (*Is the given disjunction an all-negative support clause?*)
434 fun is_negative th = forall (not o #1) (literals (prop_of th));
436 val neg_clauses = List.filter is_negative;
439 (***** MESON PROOF PROCEDURE *****)
441 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
442 As) = rhyps(phi, A::As)
443 | rhyps (_, As) = As;
445 (** Detecting repeated assumptions in a subgoal **)
447 (*The stringtree detects repeated assumptions.*)
448 fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
450 (*detects repetitions in a list of terms*)
451 fun has_reps [] = false
452 | has_reps [_] = false
453 | has_reps [t,u] = (t aconv u)
454 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false)
455 handle Net.INSERT => true;
457 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
458 fun TRYING_eq_assume_tac 0 st = Seq.single st
459 | TRYING_eq_assume_tac i st =
460 TRYING_eq_assume_tac (i-1) (eq_assumption i st)
461 handle THM _ => TRYING_eq_assume_tac (i-1) st;
463 fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
465 (*Loop checking: FAIL if trying to prove the same thing twice
466 -- if *ANY* subgoal has repeated literals*)
468 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
469 then Seq.empty else Seq.single st;
472 (* net_resolve_tac actually made it slower... *)
473 fun prolog_step_tac horns i =
474 (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
475 TRYALL_eq_assume_tac;
477 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
478 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
480 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
483 (*Negation Normal Form*)
484 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
485 not_impD, not_iffD, not_allD, not_exD, not_notD];
487 fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
488 | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
492 if ok4nnf (concl_of th)
493 then make_nnf1 (tryres(th, nnf_rls))
494 handle THM ("tryres", _, _) =>
495 forward_res make_nnf1
496 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
497 handle THM ("tryres", _, _) => th
500 (*The simplification removes defined quantifiers and occurrences of True and False.
501 nnf_ss also includes the one-point simprocs,
502 which are needed to avoid the various one-point theorems from generating junk clauses.*)
504 [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
505 if_False, if_cancel, if_eq_cancel, cases_simp];
506 val nnf_extra_simps =
507 thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
510 HOL_basic_ss addsimps nnf_extra_simps
511 addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
513 fun make_nnf th = case prems_of th of
514 [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
517 | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
519 (*Pull existential quantifiers to front. This accomplishes Skolemization for
520 clauses that arise from a subgoal.*)
522 if not (has_conns ["Ex"] (prop_of th)) then th
523 else (skolemize1 (tryres(th, [choice, conj_exD1, conj_exD2,
524 disj_exD, disj_exD1, disj_exD2])))
525 handle THM ("tryres", _, _) =>
526 skolemize1 (forward_res skolemize1
527 (tryres (th, [conj_forward, disj_forward, all_forward])))
528 handle THM ("tryres", _, _) =>
529 forward_res skolemize1 (rename_bvs_RS th ex_forward);
531 fun skolemize th = skolemize1 (make_nnf th);
533 fun skolemize_nnf_list [] = []
534 | skolemize_nnf_list (th::ths) =
535 skolemize th :: skolemize_nnf_list ths
536 handle THM _ => (*RS can fail if Unify.search_bound is too small*)
537 (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
538 skolemize_nnf_list ths);
540 fun add_clauses (th,cls) =
541 let val ctxt0 = Variable.thm_context th
542 val (cnfs,ctxt) = make_cnf [] th ctxt0
543 in Variable.export ctxt ctxt0 cnfs @ cls end;
545 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
546 The resulting clauses are HOL disjunctions.*)
547 fun make_clauses ths = sort_clauses (foldr add_clauses [] ths);
549 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
552 (distinct Thm.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
554 (*Could simply use nprems_of, which would count remaining subgoals -- no
555 discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
557 fun best_prolog_tac sizef horns =
558 BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
560 fun depth_prolog_tac horns =
561 DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
563 (*Return all negative clauses, as possible goal clauses*)
564 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
566 fun skolemize_prems_tac prems =
567 cut_facts_tac (skolemize_nnf_list prems) THEN'
570 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
571 Function mkcl converts theorems to clauses.*)
572 fun MESON mkcl cltac i st =
574 (EVERY [ObjectLogic.atomize_prems_tac 1,
577 EVERY1 [skolemize_prems_tac negs,
578 METAHYPS (cltac o mkcl)]) 1]) i st
579 handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
581 (** Best-first search versions **)
583 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
584 fun best_meson_tac sizef =
587 THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
588 (has_fewer_prems 1, sizef)
589 (prolog_step_tac (make_horns cls) 1));
591 (*First, breaks the goal into independent units*)
592 val safe_best_meson_tac =
593 SELECT_GOAL (TRY (CLASET safe_tac) THEN
594 TRYALL (best_meson_tac size_of_subgoals));
596 (** Depth-first search version **)
598 val depth_meson_tac =
600 (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
603 (** Iterative deepening version **)
605 (*This version does only one inference per call;
606 having only one eq_assume_tac speeds it up!*)
607 fun prolog_step_tac' horns =
608 let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
609 take_prefix Thm.no_prems horns
610 val nrtac = net_resolve_tac horns
611 in fn i => eq_assume_tac i ORELSE
612 match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*)
613 ((assume_tac i APPEND nrtac i) THEN check_tac)
616 fun iter_deepen_prolog_tac horns =
617 ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
619 fun iter_deepen_meson_tac ths = MESON make_clauses
621 case (gocls (cls@ths)) of
622 [] => no_tac (*no goal clauses*)
624 let val horns = make_horns (cls@ths)
626 Output.debug (fn () => ("meson method called:\n" ^
627 ML_Syntax.print_list Display.string_of_thm (cls@ths) ^
629 ML_Syntax.print_list Display.string_of_thm horns))
630 in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
634 fun meson_claset_tac ths cs =
635 SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
637 val meson_tac = CLASET' (meson_claset_tac []);
640 (**** Code to support ordinary resolution, rather than Model Elimination ****)
642 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
643 with no contrapositives, for ordinary resolution.*)
645 (*Rules to convert the head literal into a negated assumption. If the head
646 literal is already negated, then using notEfalse instead of notEfalse'
647 prevents a double negation.*)
648 val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
649 val notEfalse' = rotate_prems 1 notEfalse;
651 fun negated_asm_of_head th =
652 th RS notEfalse handle THM _ => th RS notEfalse';
654 (*Converting one theorem from a disjunction to a meta-level clause*)
655 fun make_meta_clause th =
656 let val (fth,thaw) = Drule.freeze_thaw_robust th
658 (zero_var_indexes o Thm.varifyT o thaw 0 o
659 negated_asm_of_head o make_horn resolution_clause_rules) fth
662 fun make_meta_clauses ths =
664 (distinct Thm.eq_thm_prop (map make_meta_clause ths));
666 (*Permute a rule's premises to move the i-th premise to the last position.*)
668 let val n = nprems_of th
669 in if 1 <= i andalso i <= n
670 then Thm.permute_prems (i-1) 1 th
671 else raise THM("select_literal", i, [th])
674 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
676 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
678 (*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
679 fun select_literal i cl = negate_head (make_last i cl);
682 (*Top-level Skolemization. Allows part of the conversion to clauses to be
683 expressed as a tactic (or Isar method). Each assumption of the selected
684 goal is converted to NNF and then its existential quantifiers are pulled
685 to the front. Finally, all existential quantifiers are eliminated,
686 leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
687 might generate many subgoals.*)
689 fun skolemize_tac i st =
690 let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
693 (fn hyps => (cut_facts_tac (skolemize_nnf_list hyps) 1
694 THEN REPEAT (etac exE 1))),
695 REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
697 handle Subscript => Seq.empty;