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!
14 signature BASIC_MESON =
16 val size_of_subgoals : thm -> int
17 val make_cnf : thm list -> thm -> thm list
18 val finish_cnf : thm list -> thm list
19 val make_nnf : thm -> thm
20 val make_nnf1 : thm -> thm
21 val skolemize : thm -> thm
22 val make_clauses : thm list -> thm list
23 val make_horns : thm list -> thm list
24 val best_prolog_tac : (thm -> int) -> thm list -> tactic
25 val depth_prolog_tac : thm list -> tactic
26 val gocls : thm list -> thm list
27 val skolemize_prems_tac : thm list -> int -> tactic
28 val MESON : (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic
29 val best_meson_tac : (thm -> int) -> int -> tactic
30 val safe_best_meson_tac : int -> tactic
31 val depth_meson_tac : int -> tactic
32 val prolog_step_tac' : thm list -> int -> tactic
33 val iter_deepen_prolog_tac : thm list -> tactic
34 val iter_deepen_meson_tac : thm list -> int -> tactic
35 val meson_tac : int -> tactic
36 val negate_head : thm -> thm
37 val select_literal : int -> thm -> thm
38 val skolemize_tac : int -> tactic
45 val not_conjD = thm "meson_not_conjD";
46 val not_disjD = thm "meson_not_disjD";
47 val not_notD = thm "meson_not_notD";
48 val not_allD = thm "meson_not_allD";
49 val not_exD = thm "meson_not_exD";
50 val imp_to_disjD = thm "meson_imp_to_disjD";
51 val not_impD = thm "meson_not_impD";
52 val iff_to_disjD = thm "meson_iff_to_disjD";
53 val not_iffD = thm "meson_not_iffD";
54 val conj_exD1 = thm "meson_conj_exD1";
55 val conj_exD2 = thm "meson_conj_exD2";
56 val disj_exD = thm "meson_disj_exD";
57 val disj_exD1 = thm "meson_disj_exD1";
58 val disj_exD2 = thm "meson_disj_exD2";
59 val disj_assoc = thm "meson_disj_assoc";
60 val disj_comm = thm "meson_disj_comm";
61 val disj_FalseD1 = thm "meson_disj_FalseD1";
62 val disj_FalseD2 = thm "meson_disj_FalseD2";
65 (**** Operators for forward proof ****)
68 (** First-order Resolution **)
70 fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
71 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
73 val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
75 (*FIXME: currently does not "rename variables apart"*)
76 fun first_order_resolve thA thB =
77 let val thy = theory_of_thm thA
78 val tmA = concl_of thA
79 val Const("==>",_) $ tmB $ _ = prop_of thB
80 val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0)
81 val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
82 in thA RS (cterm_instantiate ct_pairs thB) end
83 handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);
85 fun flexflex_first_order th =
86 case (tpairs_of th) of
89 let val thy = theory_of_thm th
91 foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
92 val t_pairs = map term_pair_of (Vartab.dest tenv)
93 val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
97 (*raises exception if no rules apply -- unlike RL*)
98 fun tryres (th, rls) =
99 let fun tryall [] = raise THM("tryres", 0, th::rls)
100 | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
103 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
104 e.g. from conj_forward, should have the form
105 "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
106 and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
107 fun forward_res nf st =
108 let fun forward_tacf [prem] = rtac (nf prem) 1
109 | forward_tacf prems =
110 error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
113 cat_lines (map string_of_thm prems))
115 case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
117 | NONE => raise THM("forward_res", 0, [st])
120 (*Are any of the logical connectives in "bs" present in the term?*)
122 let fun has (Const(a,_)) = false
123 | has (Const("Trueprop",_) $ p) = has p
124 | has (Const("Not",_) $ p) = has p
125 | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
126 | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
127 | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
128 | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
133 (**** Clause handling ****)
135 fun literals (Const("Trueprop",_) $ P) = literals P
136 | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
137 | literals (Const("Not",_) $ P) = [(false,P)]
138 | literals P = [(true,P)];
140 (*number of literals in a term*)
141 val nliterals = length o literals;
144 (*** Tautology Checking ***)
146 fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) =
147 signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
148 | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
149 | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
151 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
153 (*Literals like X=X are tautologous*)
154 fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u
155 | taut_poslit (Const("True",_)) = true
156 | taut_poslit _ = false;
159 let val (poslits,neglits) = signed_lits th
160 in exists taut_poslit poslits
162 exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
164 handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*)
167 (*** To remove trivial negated equality literals from clauses ***)
169 (*They are typically functional reflexivity axioms and are the converses of
170 injectivity equivalences*)
172 val not_refl_disj_D = thm"meson_not_refl_disj_D";
174 (*Is either term a Var that does not properly occur in the other term?*)
175 fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
176 | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
177 | eliminable _ = false;
179 fun refl_clause_aux 0 th = th
180 | refl_clause_aux n th =
181 case HOLogic.dest_Trueprop (concl_of th) of
182 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) =>
183 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
184 | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) =>
186 then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
187 else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
188 | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
189 | _ => (*not a disjunction*) th;
191 fun notequal_lits_count (Const ("op |", _) $ P $ Q) =
192 notequal_lits_count P + notequal_lits_count Q
193 | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
194 | notequal_lits_count _ = 0;
196 (*Simplify a clause by applying reflexivity to its negated equality literals*)
198 let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
199 in zero_var_indexes (refl_clause_aux neqs th) end
200 handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
203 (*** The basic CNF transformation ***)
205 val max_clauses = ref 40;
207 fun sum x y = if x < !max_clauses andalso y < !max_clauses then x+y else !max_clauses;
208 fun prod x y = if x < !max_clauses andalso y < !max_clauses then x*y else !max_clauses;
210 (*Estimate the number of clauses in order to detect infeasible theorems*)
211 fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
212 | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
213 | signed_nclauses b (Const("op &",_) $ t $ u) =
214 if b then sum (signed_nclauses b t) (signed_nclauses b u)
215 else prod (signed_nclauses b t) (signed_nclauses b u)
216 | signed_nclauses b (Const("op |",_) $ t $ u) =
217 if b then prod (signed_nclauses b t) (signed_nclauses b u)
218 else sum (signed_nclauses b t) (signed_nclauses b u)
219 | signed_nclauses b (Const("op -->",_) $ t $ u) =
220 if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
221 else sum (signed_nclauses (not b) t) (signed_nclauses b u)
222 | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
223 if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
224 if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
225 (prod (signed_nclauses (not b) u) (signed_nclauses b t))
226 else sum (prod (signed_nclauses b t) (signed_nclauses b u))
227 (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
229 | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
230 | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
231 | signed_nclauses _ _ = 1; (* literal *)
233 val nclauses = signed_nclauses true;
235 fun too_many_clauses t = nclauses t >= !max_clauses;
237 (*Replaces universally quantified variables by FREE variables -- because
238 assumptions may not contain scheme variables. Later, we call "generalize". *)
240 let val newname = gensym "mes_"
241 val spec' = read_instantiate [("x", newname)] spec
244 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
245 and then normalized via function nf. The normal form is given to resolve_tac,
246 instantiate a Boolean variable created by resolution with disj_forward. Since
247 (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
248 fun resop nf [prem] = resolve_tac (nf prem) 1;
250 (*Any need to extend this list with
251 "HOL.type_class","HOL.eq_class","ProtoPure.term"?*)
253 exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1);
255 fun apply_skolem_ths (th, rls) =
256 let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
257 | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
260 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
261 Strips universal quantifiers and breaks up conjunctions.
262 Eliminates existential quantifiers using skoths: Skolemization theorems.*)
263 fun cnf skoths (th,ths) =
264 let fun cnf_aux (th,ths) =
265 if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
266 else if not (has_conns ["All","Ex","op &"] (prop_of th))
267 then th::ths (*no work to do, terminate*)
268 else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
269 Const ("op &", _) => (*conjunction*)
270 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
271 | Const ("All", _) => (*universal quantifier*)
272 cnf_aux (freeze_spec th, ths)
274 (*existential quantifier: Insert Skolem functions*)
275 cnf_aux (apply_skolem_ths (th,skoths), ths)
276 | Const ("op |", _) =>
277 (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
278 all combinations of converting P, Q to CNF.*)
280 (METAHYPS (resop cnf_nil) 1) THEN
281 (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
282 in Seq.list_of (tac (th RS disj_forward)) @ ths end
283 | _ => (*no work to do*) th::ths
284 and cnf_nil th = cnf_aux (th,[])
286 if too_many_clauses (concl_of th)
287 then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
288 else cnf_aux (th,ths)
291 fun all_names (Const ("all", _) $ Abs(x,_,P)) = x :: all_names P
294 fun new_names n [] = []
295 | new_names n (x::xs) =
296 if String.isPrefix "mes_" x then (x, radixstring(26,"A",n)) :: new_names (n+1) xs
299 (*The gensym names are ugly, so don't let the user see them. When forall_elim_vars
300 is called, it will ensure that no name clauses ensue.*)
302 let val old_names = all_names (prop_of th)
303 in Drule.rename_bvars (new_names 0 old_names) th end;
305 (*Convert all suitable free variables to schematic variables,
306 but don't discharge assumptions.*)
307 fun generalize th = Thm.varifyT (forall_elim_vars 0 (nice_names (forall_intr_frees th)));
309 fun make_cnf skoths th = cnf skoths (th, []);
311 (*Generalization, removal of redundant equalities, removal of tautologies.*)
312 fun finish_cnf ths = filter (not o is_taut) (map (refl_clause o generalize) ths);
315 (**** Removal of duplicate literals ****)
317 (*Forward proof, passing extra assumptions as theorems to the tactic*)
318 fun forward_res2 nf hyps st =
321 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
324 | NONE => raise THM("forward_res2", 0, [st]);
326 (*Remove duplicates in P|Q by assuming ~P in Q
327 rls (initially []) accumulates assumptions of the form P==>False*)
328 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
329 handle THM _ => tryres(th,rls)
330 handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
331 [disj_FalseD1, disj_FalseD2, asm_rl])
334 (*Remove duplicate literals, if there are any*)
336 if has_duplicates (op =) (literals (prop_of th))
337 then nodups_aux [] th
341 (**** Generation of contrapositives ****)
343 fun is_left (Const ("Trueprop", _) $
344 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
347 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
349 if is_left (prop_of th) then assoc_right (th RS disj_assoc)
352 (*Must check for negative literal first!*)
353 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
355 (*For ordinary resolution. *)
356 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
358 (*Create a goal or support clause, conclusing False*)
359 fun make_goal th = (*Must check for negative literal first!*)
360 make_goal (tryres(th, clause_rules))
361 handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
363 (*Sort clauses by number of literals*)
364 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
366 fun sort_clauses ths = sort (make_ord fewerlits) ths;
368 (*True if the given type contains bool anywhere*)
369 fun has_bool (Type("bool",_)) = true
370 | has_bool (Type(_, Ts)) = exists has_bool Ts
371 | has_bool _ = false;
373 (*Is the string the name of a connective? Really only | and Not can remain,
374 since this code expects to be called on a clause form.*)
375 val is_conn = member (op =)
376 ["Trueprop", "op &", "op |", "op -->", "Not",
377 "All", "Ex", "Ball", "Bex"];
379 (*True if the term contains a function--not a logical connective--where the type
380 of any argument contains bool.*)
381 val has_bool_arg_const =
383 (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
385 (*A higher-order instance of a first-order constant? Example is the definition of
386 HOL.one, 1, at a function type in theory SetsAndFunctions.*)
387 fun higher_inst_const thy (c,T) =
388 case binder_types T of
389 [] => false (*not a function type, OK*)
390 | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
392 (*Raises an exception if any Vars in the theorem mention type bool.
393 Also rejects functions whose arguments are Booleans or other functions.*)
394 fun is_fol_term thy t =
395 Term.is_first_order ["all","All","Ex"] t andalso
396 not (exists (has_bool o fastype_of) (term_vars t) orelse
397 has_bool_arg_const t orelse
398 exists_Const (higher_inst_const thy) t orelse
401 fun rigid t = not (is_Var (head_of t));
403 fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t
404 | ok4horn (Const ("Trueprop",_) $ t) = rigid t
407 (*Create a meta-level Horn clause*)
408 fun make_horn crules th =
409 if ok4horn (concl_of th)
410 then make_horn crules (tryres(th,crules)) handle THM _ => th
413 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
414 is a HOL disjunction.*)
415 fun add_contras crules (th,hcs) =
416 let fun rots (0,th) = hcs
417 | rots (k,th) = zero_var_indexes (make_horn crules th) ::
418 rots(k-1, assoc_right (th RS disj_comm))
419 in case nliterals(prop_of th) of
421 | n => rots(n, assoc_right th)
424 (*Use "theorem naming" to label the clauses*)
425 fun name_thms label =
426 let fun name1 (th, (k,ths)) =
427 (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths)
428 in fn ths => #2 (foldr name1 (length ths, []) ths) end;
430 (*Is the given disjunction an all-negative support clause?*)
431 fun is_negative th = forall (not o #1) (literals (prop_of th));
433 val neg_clauses = List.filter is_negative;
436 (***** MESON PROOF PROCEDURE *****)
438 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
439 As) = rhyps(phi, A::As)
440 | rhyps (_, As) = As;
442 (** Detecting repeated assumptions in a subgoal **)
444 (*The stringtree detects repeated assumptions.*)
445 fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
447 (*detects repetitions in a list of terms*)
448 fun has_reps [] = false
449 | has_reps [_] = false
450 | has_reps [t,u] = (t aconv u)
451 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false)
452 handle Net.INSERT => true;
454 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
455 fun TRYING_eq_assume_tac 0 st = Seq.single st
456 | TRYING_eq_assume_tac i st =
457 TRYING_eq_assume_tac (i-1) (eq_assumption i st)
458 handle THM _ => TRYING_eq_assume_tac (i-1) st;
460 fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
462 (*Loop checking: FAIL if trying to prove the same thing twice
463 -- if *ANY* subgoal has repeated literals*)
465 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
466 then Seq.empty else Seq.single st;
469 (* net_resolve_tac actually made it slower... *)
470 fun prolog_step_tac horns i =
471 (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
472 TRYALL_eq_assume_tac;
474 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
475 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
477 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
480 (*Negation Normal Form*)
481 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
482 not_impD, not_iffD, not_allD, not_exD, not_notD];
484 fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
485 | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
489 if ok4nnf (concl_of th)
490 then make_nnf1 (tryres(th, nnf_rls))
492 forward_res make_nnf1
493 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
497 (*The simplification removes defined quantifiers and occurrences of True and False.
498 nnf_ss also includes the one-point simprocs,
499 which are needed to avoid the various one-point theorems from generating junk clauses.*)
501 [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
502 if_False, if_cancel, if_eq_cancel, cases_simp];
503 val nnf_extra_simps =
504 thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
507 HOL_basic_ss addsimps nnf_extra_simps
508 addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
510 fun make_nnf th = case prems_of th of
511 [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
514 | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
516 (*Pull existential quantifiers to front. This accomplishes Skolemization for
517 clauses that arise from a subgoal.*)
519 if not (has_conns ["Ex"] (prop_of th)) then th
520 else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
521 disj_exD, disj_exD1, disj_exD2])))
523 skolemize (forward_res skolemize
524 (tryres (th, [conj_forward, disj_forward, all_forward])))
525 handle THM _ => forward_res skolemize (th RS ex_forward);
528 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
529 The resulting clauses are HOL disjunctions.*)
530 fun make_clauses ths =
531 (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
533 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
536 (distinct Thm.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
538 (*Could simply use nprems_of, which would count remaining subgoals -- no
539 discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
541 fun best_prolog_tac sizef horns =
542 BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
544 fun depth_prolog_tac horns =
545 DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
547 (*Return all negative clauses, as possible goal clauses*)
548 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
550 fun skolemize_prems_tac prems =
551 cut_facts_tac (map (skolemize o make_nnf) prems) THEN'
554 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
555 Function mkcl converts theorems to clauses.*)
556 fun MESON mkcl cltac i st =
558 (EVERY [ObjectLogic.atomize_prems_tac 1,
561 EVERY1 [skolemize_prems_tac negs,
562 METAHYPS (cltac o mkcl)]) 1]) i st
563 handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
565 (** Best-first search versions **)
567 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
568 fun best_meson_tac sizef =
571 THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
572 (has_fewer_prems 1, sizef)
573 (prolog_step_tac (make_horns cls) 1));
575 (*First, breaks the goal into independent units*)
576 val safe_best_meson_tac =
577 SELECT_GOAL (TRY (CLASET safe_tac) THEN
578 TRYALL (best_meson_tac size_of_subgoals));
580 (** Depth-first search version **)
582 val depth_meson_tac =
584 (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
587 (** Iterative deepening version **)
589 (*This version does only one inference per call;
590 having only one eq_assume_tac speeds it up!*)
591 fun prolog_step_tac' horns =
592 let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
593 take_prefix Thm.no_prems horns
594 val nrtac = net_resolve_tac horns
595 in fn i => eq_assume_tac i ORELSE
596 match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*)
597 ((assume_tac i APPEND nrtac i) THEN check_tac)
600 fun iter_deepen_prolog_tac horns =
601 ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
603 fun iter_deepen_meson_tac ths = MESON make_clauses
605 case (gocls (cls@ths)) of
606 [] => no_tac (*no goal clauses*)
608 let val horns = make_horns (cls@ths)
610 Output.debug (fn () => ("meson method called:\n" ^
611 space_implode "\n" (map string_of_thm (cls@ths)) ^
613 space_implode "\n" (map string_of_thm horns)))
614 in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
618 fun meson_claset_tac ths cs =
619 SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
621 val meson_tac = CLASET' (meson_claset_tac []);
624 (**** Code to support ordinary resolution, rather than Model Elimination ****)
626 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
627 with no contrapositives, for ordinary resolution.*)
629 (*Rules to convert the head literal into a negated assumption. If the head
630 literal is already negated, then using notEfalse instead of notEfalse'
631 prevents a double negation.*)
632 val notEfalse = read_instantiate [("R","False")] notE;
633 val notEfalse' = rotate_prems 1 notEfalse;
635 fun negated_asm_of_head th =
636 th RS notEfalse handle THM _ => th RS notEfalse';
638 (*Converting one clause*)
639 val make_meta_clause =
640 zero_var_indexes o negated_asm_of_head o make_horn resolution_clause_rules;
642 fun make_meta_clauses ths =
644 (distinct Thm.eq_thm_prop (map make_meta_clause ths));
646 (*Permute a rule's premises to move the i-th premise to the last position.*)
648 let val n = nprems_of th
649 in if 1 <= i andalso i <= n
650 then Thm.permute_prems (i-1) 1 th
651 else raise THM("select_literal", i, [th])
654 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
656 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
658 (*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
659 fun select_literal i cl = negate_head (make_last i cl);
662 (*Top-level Skolemization. Allows part of the conversion to clauses to be
663 expressed as a tactic (or Isar method). Each assumption of the selected
664 goal is converted to NNF and then its existential quantifiers are pulled
665 to the front. Finally, all existential quantifiers are eliminated,
666 leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
667 might generate many subgoals.*)
669 fun skolemize_tac i st =
670 let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
673 (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
674 THEN REPEAT (etac exE 1))),
675 REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
677 handle Subscript => Seq.empty;
681 structure BasicMeson: BASIC_MESON = Meson;