moved eq_thm etc. to structure Thm in Pure/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
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 -> 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";
64 val depth_limit = ref 2000;
66 (**** Operators for forward proof ****)
69 (** First-order Resolution **)
71 fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
72 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
74 val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
76 (*FIXME: currently does not "rename variables apart"*)
77 fun first_order_resolve thA thB =
78 let val thy = theory_of_thm thA
79 val tmA = concl_of thA
80 fun match pat = Pattern.first_order_match thy (pat,tmA) (tyenv0,tenv0)
81 val Const("==>",_) $ tmB $ _ = prop_of thB
82 val (tyenv,tenv) = match tmB
83 val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
84 in thA RS (cterm_instantiate ct_pairs thB) end
85 handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);
87 (*raises exception if no rules apply -- unlike RL*)
88 fun tryres (th, rls) =
89 let fun tryall [] = raise THM("tryres", 0, th::rls)
90 | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
93 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
94 e.g. from conj_forward, should have the form
95 "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
96 and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
97 fun forward_res nf st =
98 let fun forward_tacf [prem] = rtac (nf prem) 1
99 | forward_tacf prems =
100 error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
103 cat_lines (map string_of_thm prems))
105 case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
107 | NONE => raise THM("forward_res", 0, [st])
110 (*Are any of the logical connectives in "bs" present in the term?*)
112 let fun has (Const(a,_)) = false
113 | has (Const("Trueprop",_) $ p) = has p
114 | has (Const("Not",_) $ p) = has p
115 | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
116 | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
117 | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
118 | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
123 (**** Clause handling ****)
125 fun literals (Const("Trueprop",_) $ P) = literals P
126 | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
127 | literals (Const("Not",_) $ P) = [(false,P)]
128 | literals P = [(true,P)];
130 (*number of literals in a term*)
131 val nliterals = length o literals;
134 (*** Tautology Checking ***)
136 fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) =
137 signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
138 | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
139 | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
141 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
143 (*Literals like X=X are tautologous*)
144 fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u
145 | taut_poslit (Const("True",_)) = true
146 | taut_poslit _ = false;
149 let val (poslits,neglits) = signed_lits th
150 in exists taut_poslit poslits
152 exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
154 handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*)
157 (*** To remove trivial negated equality literals from clauses ***)
159 (*They are typically functional reflexivity axioms and are the converses of
160 injectivity equivalences*)
162 val not_refl_disj_D = thm"meson_not_refl_disj_D";
164 (*Is either term a Var that does not properly occur in the other term?*)
165 fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
166 | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
167 | eliminable _ = false;
169 fun refl_clause_aux 0 th = th
170 | refl_clause_aux n th =
171 case HOLogic.dest_Trueprop (concl_of th) of
172 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) =>
173 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
174 | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) =>
176 then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
177 else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
178 | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
179 | _ => (*not a disjunction*) th;
181 fun notequal_lits_count (Const ("op |", _) $ P $ Q) =
182 notequal_lits_count P + notequal_lits_count Q
183 | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
184 | notequal_lits_count _ = 0;
186 (*Simplify a clause by applying reflexivity to its negated equality literals*)
188 let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
189 in zero_var_indexes (refl_clause_aux neqs th) end
190 handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
193 (*** The basic CNF transformation ***)
195 val max_clauses = ref 40;
197 fun sum x y = if x < !max_clauses andalso y < !max_clauses then x+y else !max_clauses;
198 fun prod x y = if x < !max_clauses andalso y < !max_clauses then x*y else !max_clauses;
200 (*Estimate the number of clauses in order to detect infeasible theorems*)
201 fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
202 | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
203 | signed_nclauses b (Const("op &",_) $ t $ u) =
204 if b then sum (signed_nclauses b t) (signed_nclauses b u)
205 else prod (signed_nclauses b t) (signed_nclauses b u)
206 | signed_nclauses b (Const("op |",_) $ t $ u) =
207 if b then prod (signed_nclauses b t) (signed_nclauses b u)
208 else sum (signed_nclauses b t) (signed_nclauses b u)
209 | signed_nclauses b (Const("op -->",_) $ t $ u) =
210 if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
211 else sum (signed_nclauses (not b) t) (signed_nclauses b u)
212 | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
213 if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
214 if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
215 (prod (signed_nclauses (not b) u) (signed_nclauses b t))
216 else sum (prod (signed_nclauses b t) (signed_nclauses b u))
217 (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
219 | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
220 | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
221 | signed_nclauses _ _ = 1; (* literal *)
223 val nclauses = signed_nclauses true;
225 fun too_many_clauses t = nclauses t >= !max_clauses;
227 (*Replaces universally quantified variables by FREE variables -- because
228 assumptions may not contain scheme variables. Later, call "generalize". *)
230 let val newname = gensym "mes_"
231 val spec' = read_instantiate [("x", newname)] spec
234 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
235 and then normalized via function nf. The normal form is given to resolve_tac,
236 presumably to instantiate a Boolean variable.*)
237 fun resop nf [prem] = resolve_tac (nf prem) 1;
239 (*Any need to extend this list with
240 "HOL.type_class","Code_Generator.eq_class","ProtoPure.term"?*)
242 exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
244 fun apply_skolem_ths (th, rls) =
245 let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
246 | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
249 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
250 Strips universal quantifiers and breaks up conjunctions.
251 Eliminates existential quantifiers using skoths: Skolemization theorems.*)
252 fun cnf skoths (th,ths) =
253 let fun cnf_aux (th,ths) =
254 if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
255 else if not (has_conns ["All","Ex","op &"] (prop_of th))
256 then th::ths (*no work to do, terminate*)
257 else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
258 Const ("op &", _) => (*conjunction*)
259 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
260 | Const ("All", _) => (*universal quantifier*)
261 cnf_aux (freeze_spec th, ths)
263 (*existential quantifier: Insert Skolem functions*)
264 cnf_aux (apply_skolem_ths (th,skoths), ths)
265 | Const ("op |", _) => (*disjunction*)
267 (METAHYPS (resop cnf_nil) 1) THEN
268 (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
269 in Seq.list_of (tac (th RS disj_forward)) @ ths end
270 | _ => (*no work to do*) th::ths
271 and cnf_nil th = cnf_aux (th,[])
273 if too_many_clauses (concl_of th)
274 then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
275 else cnf_aux (th,ths)
278 (*Convert all suitable free variables to schematic variables,
279 but don't discharge assumptions.*)
280 fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th));
282 fun make_cnf skoths th = cnf skoths (th, []);
284 (*Generalization, removal of redundant equalities, removal of tautologies.*)
285 fun finish_cnf ths = filter (not o is_taut) (map (refl_clause o generalize) ths);
288 (**** Removal of duplicate literals ****)
290 (*Forward proof, passing extra assumptions as theorems to the tactic*)
291 fun forward_res2 nf hyps st =
294 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
297 | NONE => raise THM("forward_res2", 0, [st]);
299 (*Remove duplicates in P|Q by assuming ~P in Q
300 rls (initially []) accumulates assumptions of the form P==>False*)
301 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
302 handle THM _ => tryres(th,rls)
303 handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
304 [disj_FalseD1, disj_FalseD2, asm_rl])
307 (*Remove duplicate literals, if there are any*)
309 if has_duplicates (op =) (literals (prop_of th))
310 then nodups_aux [] th
314 (**** Generation of contrapositives ****)
316 fun is_left (Const ("Trueprop", _) $
317 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
320 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
322 if is_left (prop_of th) then assoc_right (th RS disj_assoc)
325 (*Must check for negative literal first!*)
326 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
328 (*For ordinary resolution. *)
329 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
331 (*Create a goal or support clause, conclusing False*)
332 fun make_goal th = (*Must check for negative literal first!*)
333 make_goal (tryres(th, clause_rules))
334 handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
336 (*Sort clauses by number of literals*)
337 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
339 fun sort_clauses ths = sort (make_ord fewerlits) ths;
341 (*True if the given type contains bool anywhere*)
342 fun has_bool (Type("bool",_)) = true
343 | has_bool (Type(_, Ts)) = exists has_bool Ts
344 | has_bool _ = false;
346 (*Is the string the name of a connective? Really only | and Not can remain,
347 since this code expects to be called on a clause form.*)
348 val is_conn = member (op =)
349 ["Trueprop", "op &", "op |", "op -->", "Not",
350 "All", "Ex", "Ball", "Bex"];
352 (*True if the term contains a function--not a logical connective--where the type
353 of any argument contains bool.*)
354 val has_bool_arg_const =
356 (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
358 (*Raises an exception if any Vars in the theorem mention type bool.
359 Also rejects functions whose arguments are Booleans or other functions.*)
361 not (exists (has_bool o fastype_of) (term_vars t) orelse
362 not (Term.is_first_order ["all","All","Ex"] t) orelse
363 has_bool_arg_const t orelse
366 fun rigid t = not (is_Var (head_of t));
368 fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t
369 | ok4horn (Const ("Trueprop",_) $ t) = rigid t
372 (*Create a meta-level Horn clause*)
373 fun make_horn crules th =
374 if ok4horn (concl_of th)
375 then make_horn crules (tryres(th,crules)) handle THM _ => th
378 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
379 is a HOL disjunction.*)
380 fun add_contras crules (th,hcs) =
381 let fun rots (0,th) = hcs
382 | rots (k,th) = zero_var_indexes (make_horn crules th) ::
383 rots(k-1, assoc_right (th RS disj_comm))
384 in case nliterals(prop_of th) of
386 | n => rots(n, assoc_right th)
389 (*Use "theorem naming" to label the clauses*)
390 fun name_thms label =
391 let fun name1 (th, (k,ths)) =
392 (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths)
393 in fn ths => #2 (foldr name1 (length ths, []) ths) end;
395 (*Is the given disjunction an all-negative support clause?*)
396 fun is_negative th = forall (not o #1) (literals (prop_of th));
398 val neg_clauses = List.filter is_negative;
401 (***** MESON PROOF PROCEDURE *****)
403 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
404 As) = rhyps(phi, A::As)
405 | rhyps (_, As) = As;
407 (** Detecting repeated assumptions in a subgoal **)
409 (*The stringtree detects repeated assumptions.*)
410 fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
412 (*detects repetitions in a list of terms*)
413 fun has_reps [] = false
414 | has_reps [_] = false
415 | has_reps [t,u] = (t aconv u)
416 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false)
417 handle Net.INSERT => true;
419 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
420 fun TRYING_eq_assume_tac 0 st = Seq.single st
421 | TRYING_eq_assume_tac i st =
422 TRYING_eq_assume_tac (i-1) (eq_assumption i st)
423 handle THM _ => TRYING_eq_assume_tac (i-1) st;
425 fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
427 (*Loop checking: FAIL if trying to prove the same thing twice
428 -- if *ANY* subgoal has repeated literals*)
430 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
431 then Seq.empty else Seq.single st;
434 (* net_resolve_tac actually made it slower... *)
435 fun prolog_step_tac horns i =
436 (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
437 TRYALL_eq_assume_tac;
439 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
440 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
442 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
445 (*Negation Normal Form*)
446 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
447 not_impD, not_iffD, not_allD, not_exD, not_notD];
449 fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
450 | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
454 if ok4nnf (concl_of th)
455 then make_nnf1 (tryres(th, nnf_rls))
457 forward_res make_nnf1
458 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
462 (*The simplification removes defined quantifiers and occurrences of True and False.
463 nnf_ss also includes the one-point simprocs,
464 which are needed to avoid the various one-point theorems from generating junk clauses.*)
466 [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
467 if_False, if_cancel, if_eq_cancel, cases_simp];
468 val nnf_extra_simps =
469 thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
472 HOL_basic_ss addsimps nnf_extra_simps
473 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
475 fun make_nnf th = case prems_of th of
476 [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
479 | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
481 (*Pull existential quantifiers to front. This accomplishes Skolemization for
482 clauses that arise from a subgoal.*)
484 if not (has_conns ["Ex"] (prop_of th)) then th
485 else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
486 disj_exD, disj_exD1, disj_exD2])))
488 skolemize (forward_res skolemize
489 (tryres (th, [conj_forward, disj_forward, all_forward])))
490 handle THM _ => forward_res skolemize (th RS ex_forward);
493 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
494 The resulting clauses are HOL disjunctions.*)
495 fun make_clauses ths =
496 (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
498 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
501 (distinct Thm.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
503 (*Could simply use nprems_of, which would count remaining subgoals -- no
504 discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
506 fun best_prolog_tac sizef horns =
507 BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
509 fun depth_prolog_tac horns =
510 DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
512 (*Return all negative clauses, as possible goal clauses*)
513 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
515 fun skolemize_prems_tac prems =
516 cut_facts_tac (map (skolemize o make_nnf) prems) THEN'
519 (*Expand all definitions (presumably of Skolem functions) in a proof state.*)
520 fun expand_defs_tac st =
521 let val defs = filter (can dest_equals) (#hyps (crep_thm st))
522 in PRIMITIVE (LocalDefs.expand defs) st end;
524 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions*)
525 fun MESON cltac i st =
527 (EVERY [rtac ccontr 1,
529 EVERY1 [skolemize_prems_tac negs,
530 METAHYPS (cltac o make_clauses)]) 1,
531 expand_defs_tac]) i st
532 handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
534 (** Best-first search versions **)
536 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
537 fun best_meson_tac sizef =
539 THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
540 (has_fewer_prems 1, sizef)
541 (prolog_step_tac (make_horns cls) 1));
543 (*First, breaks the goal into independent units*)
544 val safe_best_meson_tac =
545 SELECT_GOAL (TRY Safe_tac THEN
546 TRYALL (best_meson_tac size_of_subgoals));
548 (** Depth-first search version **)
550 val depth_meson_tac =
551 MESON (fn cls => EVERY [resolve_tac (gocls cls) 1,
552 depth_prolog_tac (make_horns cls)]);
555 (** Iterative deepening version **)
557 (*This version does only one inference per call;
558 having only one eq_assume_tac speeds it up!*)
559 fun prolog_step_tac' horns =
560 let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
561 take_prefix Thm.no_prems horns
562 val nrtac = net_resolve_tac horns
563 in fn i => eq_assume_tac i ORELSE
564 match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*)
565 ((assume_tac i APPEND nrtac i) THEN check_tac)
568 fun iter_deepen_prolog_tac horns =
569 ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
571 fun iter_deepen_meson_tac ths = MESON
573 case (gocls (cls@ths)) of
574 [] => no_tac (*no goal clauses*)
576 let val horns = make_horns (cls@ths)
578 Output.debug (fn () => ("meson method called:\n" ^
579 space_implode "\n" (map string_of_thm (cls@ths)) ^
581 space_implode "\n" (map string_of_thm horns)))
582 in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
586 fun meson_claset_tac ths cs =
587 SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
589 val meson_tac = CLASET' (meson_claset_tac []);
592 (**** Code to support ordinary resolution, rather than Model Elimination ****)
594 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
595 with no contrapositives, for ordinary resolution.*)
597 (*Rules to convert the head literal into a negated assumption. If the head
598 literal is already negated, then using notEfalse instead of notEfalse'
599 prevents a double negation.*)
600 val notEfalse = read_instantiate [("R","False")] notE;
601 val notEfalse' = rotate_prems 1 notEfalse;
603 fun negated_asm_of_head th =
604 th RS notEfalse handle THM _ => th RS notEfalse';
606 (*Converting one clause*)
607 fun make_meta_clause th =
608 negated_asm_of_head (make_horn resolution_clause_rules th);
610 fun make_meta_clauses ths =
612 (distinct Thm.eq_thm_prop (map make_meta_clause ths));
614 (*Permute a rule's premises to move the i-th premise to the last position.*)
616 let val n = nprems_of th
617 in if 1 <= i andalso i <= n
618 then Thm.permute_prems (i-1) 1 th
619 else raise THM("select_literal", i, [th])
622 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
624 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
626 (*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
627 fun select_literal i cl = negate_head (make_last i cl);
630 (*Top-level Skolemization. Allows part of the conversion to clauses to be
631 expressed as a tactic (or Isar method). Each assumption of the selected
632 goal is converted to NNF and then its existential quantifiers are pulled
633 to the front. Finally, all existential quantifiers are eliminated,
634 leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
635 might generate many subgoals.*)
637 fun skolemize_tac i st =
638 let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
641 (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
642 THEN REPEAT (etac exE 1))),
643 REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
645 handle Subscript => Seq.empty;
649 structure BasicMeson: BASIC_MESON = Meson;