Tweaks to is_fol_term, the first-order test. We don't count "=" as a connective
since this test is applied to clause forms.
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
39 val make_clauses_tac : int -> tactic
46 val not_conjD = thm "meson_not_conjD";
47 val not_disjD = thm "meson_not_disjD";
48 val not_notD = thm "meson_not_notD";
49 val not_allD = thm "meson_not_allD";
50 val not_exD = thm "meson_not_exD";
51 val imp_to_disjD = thm "meson_imp_to_disjD";
52 val not_impD = thm "meson_not_impD";
53 val iff_to_disjD = thm "meson_iff_to_disjD";
54 val not_iffD = thm "meson_not_iffD";
55 val conj_exD1 = thm "meson_conj_exD1";
56 val conj_exD2 = thm "meson_conj_exD2";
57 val disj_exD = thm "meson_disj_exD";
58 val disj_exD1 = thm "meson_disj_exD1";
59 val disj_exD2 = thm "meson_disj_exD2";
60 val disj_assoc = thm "meson_disj_assoc";
61 val disj_comm = thm "meson_disj_comm";
62 val disj_FalseD1 = thm "meson_disj_FalseD1";
63 val disj_FalseD2 = thm "meson_disj_FalseD2";
65 val depth_limit = ref 2000;
67 (**** Operators for forward proof ****)
70 (** First-order Resolution **)
72 fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
73 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
75 val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
77 (*FIXME: currently does not "rename variables apart"*)
78 fun first_order_resolve thA thB =
79 let val thy = theory_of_thm thA
80 val tmA = concl_of thA
81 fun match pat = Pattern.first_order_match thy (pat,tmA) (tyenv0,tenv0)
82 val Const("==>",_) $ tmB $ _ = prop_of thB
83 val (tyenv,tenv) = match tmB
84 val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
85 in thA RS (cterm_instantiate ct_pairs thB) end
86 handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);
88 (*raises exception if no rules apply -- unlike RL*)
89 fun tryres (th, rls) =
90 let fun tryall [] = raise THM("tryres", 0, th::rls)
91 | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
94 (*Permits forward proof from rules that discharge assumptions*)
95 fun forward_res nf st =
96 case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
98 | NONE => raise THM("forward_res", 0, [st]);
101 (*Are any of the logical connectives in "bs" present in the term?*)
103 let fun has (Const(a,_)) = false
104 | has (Const("Trueprop",_) $ p) = has p
105 | has (Const("Not",_) $ p) = has p
106 | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
107 | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
108 | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
109 | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
114 (**** Clause handling ****)
116 fun literals (Const("Trueprop",_) $ P) = literals P
117 | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
118 | literals (Const("Not",_) $ P) = [(false,P)]
119 | literals P = [(true,P)];
121 (*number of literals in a term*)
122 val nliterals = length o literals;
125 (*** Tautology Checking ***)
127 fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) =
128 signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
129 | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
130 | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
132 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
134 (*Literals like X=X are tautologous*)
135 fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u
136 | taut_poslit (Const("True",_)) = true
137 | taut_poslit _ = false;
140 let val (poslits,neglits) = signed_lits th
141 in exists taut_poslit poslits
143 exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
145 handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*)
148 (*** To remove trivial negated equality literals from clauses ***)
150 (*They are typically functional reflexivity axioms and are the converses of
151 injectivity equivalences*)
153 val not_refl_disj_D = thm"meson_not_refl_disj_D";
155 (*Is either term a Var that does not properly occur in the other term?*)
156 fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
157 | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
158 | eliminable _ = false;
160 fun refl_clause_aux 0 th = th
161 | refl_clause_aux n th =
162 case HOLogic.dest_Trueprop (concl_of th) of
163 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) =>
164 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
165 | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) =>
167 then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
168 else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
169 | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
170 | _ => (*not a disjunction*) th;
172 fun notequal_lits_count (Const ("op |", _) $ P $ Q) =
173 notequal_lits_count P + notequal_lits_count Q
174 | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
175 | notequal_lits_count _ = 0;
177 (*Simplify a clause by applying reflexivity to its negated equality literals*)
179 let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
180 in zero_var_indexes (refl_clause_aux neqs th) end
181 handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
184 (*** The basic CNF transformation ***)
186 (*Estimate the number of clauses in order to detect infeasible theorems*)
187 fun nclauses (Const("Trueprop",_) $ t) = nclauses t
188 | nclauses (Const("op &",_) $ t $ u) = nclauses t + nclauses u
189 | nclauses (Const("Ex", _) $ Abs (_,_,t)) = nclauses t
190 | nclauses (Const("All",_) $ Abs (_,_,t)) = nclauses t
191 | nclauses (Const("op |",_) $ t $ u) = nclauses t * nclauses u
192 | nclauses _ = 1; (* literal *)
194 (*Replaces universally quantified variables by FREE variables -- because
195 assumptions may not contain scheme variables. Later, call "generalize". *)
197 let val newname = gensym "mes_"
198 val spec' = read_instantiate [("x", newname)] spec
201 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
202 and then normalized via function nf. The normal form is given to resolve_tac,
203 presumably to instantiate a Boolean variable.*)
204 fun resop nf [prem] = resolve_tac (nf prem) 1;
207 exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
209 fun apply_skolem_ths (th, rls) =
210 let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
211 | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
214 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
215 Strips universal quantifiers and breaks up conjunctions.
216 Eliminates existential quantifiers using skoths: Skolemization theorems.*)
217 fun cnf skoths (th,ths) =
218 let fun cnf_aux (th,ths) =
219 if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
220 else if not (has_conns ["All","Ex","op &"] (prop_of th))
221 then th::ths (*no work to do, terminate*)
222 else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
223 Const ("op &", _) => (*conjunction*)
224 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
225 | Const ("All", _) => (*universal quantifier*)
226 cnf_aux (freeze_spec th, ths)
228 (*existential quantifier: Insert Skolem functions*)
229 cnf_aux (apply_skolem_ths (th,skoths), ths)
230 | Const ("op |", _) => (*disjunction*)
232 (METAHYPS (resop cnf_nil) 1) THEN
233 (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
234 in Seq.list_of (tac (th RS disj_forward)) @ ths end
235 | _ => (*no work to do*) th::ths
236 and cnf_nil th = cnf_aux (th,[])
238 if nclauses (concl_of th) > 20
239 then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths)
240 else cnf_aux (th,ths)
243 (*Convert all suitable free variables to schematic variables,
244 but don't discharge assumptions.*)
245 fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th));
247 fun make_cnf skoths th = cnf skoths (th, []);
249 (*Generalization, removal of redundant equalities, removal of tautologies.*)
250 fun finish_cnf ths = filter (not o is_taut) (map (refl_clause o generalize) ths);
253 (**** Removal of duplicate literals ****)
255 (*Forward proof, passing extra assumptions as theorems to the tactic*)
256 fun forward_res2 nf hyps st =
259 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
262 | NONE => raise THM("forward_res2", 0, [st]);
264 (*Remove duplicates in P|Q by assuming ~P in Q
265 rls (initially []) accumulates assumptions of the form P==>False*)
266 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
267 handle THM _ => tryres(th,rls)
268 handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
269 [disj_FalseD1, disj_FalseD2, asm_rl])
272 (*Remove duplicate literals, if there are any*)
274 if null(findrep(literals(prop_of th))) then th
275 else nodups_aux [] th;
278 (**** Generation of contrapositives ****)
280 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
281 fun assoc_right th = assoc_right (th RS disj_assoc)
284 (*Must check for negative literal first!*)
285 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
287 (*For ordinary resolution. *)
288 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
290 (*Create a goal or support clause, conclusing False*)
291 fun make_goal th = (*Must check for negative literal first!*)
292 make_goal (tryres(th, clause_rules))
293 handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
295 (*Sort clauses by number of literals*)
296 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
298 fun sort_clauses ths = sort (make_ord fewerlits) ths;
300 (*True if the given type contains bool anywhere*)
301 fun has_bool (Type("bool",_)) = true
302 | has_bool (Type(_, Ts)) = exists has_bool Ts
303 | has_bool _ = false;
305 (*Is the string the name of a connective? Really only | and Not can remain,
306 since this code expects to be called on a clause form.*)
307 val is_conn = member (op =)
308 ["Trueprop", "op &", "op |", "op -->", "Not",
309 "All", "Ex", "Ball", "Bex"];
311 (*True if the term contains a function--not a logical connective--where the type
312 of any argument contains bool.*)
313 val has_bool_arg_const =
315 (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
317 (*Raises an exception if any Vars in the theorem mention type bool; they
318 could cause make_horn to loop! Also rejects functions whose arguments are
319 Booleans or other functions.*)
321 not (exists (has_bool o fastype_of) (term_vars t) orelse
322 not (Term.is_first_order ["all","All","Ex"] t) orelse
323 has_bool_arg_const t orelse
326 (*Create a meta-level Horn clause*)
327 fun make_horn crules th = make_horn crules (tryres(th,crules))
330 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
331 is a HOL disjunction.*)
332 fun add_contras crules (th,hcs) =
333 let fun rots (0,th) = hcs
334 | rots (k,th) = zero_var_indexes (make_horn crules th) ::
335 rots(k-1, assoc_right (th RS disj_comm))
336 in case nliterals(prop_of th) of
338 | n => rots(n, assoc_right th)
341 (*Use "theorem naming" to label the clauses*)
342 fun name_thms label =
343 let fun name1 (th, (k,ths)) =
344 (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
346 in fn ths => #2 (foldr name1 (length ths, []) ths) end;
348 (*Is the given disjunction an all-negative support clause?*)
349 fun is_negative th = forall (not o #1) (literals (prop_of th));
351 val neg_clauses = List.filter is_negative;
354 (***** MESON PROOF PROCEDURE *****)
356 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
357 As) = rhyps(phi, A::As)
358 | rhyps (_, As) = As;
360 (** Detecting repeated assumptions in a subgoal **)
362 (*The stringtree detects repeated assumptions.*)
363 fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
365 (*detects repetitions in a list of terms*)
366 fun has_reps [] = false
367 | has_reps [_] = false
368 | has_reps [t,u] = (t aconv u)
369 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false)
370 handle Net.INSERT => true;
372 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
373 fun TRYING_eq_assume_tac 0 st = Seq.single st
374 | TRYING_eq_assume_tac i st =
375 TRYING_eq_assume_tac (i-1) (eq_assumption i st)
376 handle THM _ => TRYING_eq_assume_tac (i-1) st;
378 fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
380 (*Loop checking: FAIL if trying to prove the same thing twice
381 -- if *ANY* subgoal has repeated literals*)
383 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
384 then Seq.empty else Seq.single st;
387 (* net_resolve_tac actually made it slower... *)
388 fun prolog_step_tac horns i =
389 (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
390 TRYALL_eq_assume_tac;
392 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
393 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
395 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
398 (*Negation Normal Form*)
399 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
400 not_impD, not_iffD, not_allD, not_exD, not_notD];
402 fun make_nnf1 th = make_nnf1 (tryres(th, nnf_rls))
404 forward_res make_nnf1
405 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
408 (*The simplification removes defined quantifiers and occurrences of True and False.
409 nnf_ss also includes the one-point simprocs,
410 which are needed to avoid the various one-point theorems from generating junk clauses.*)
412 [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
413 if_False, if_cancel, if_eq_cancel, cases_simp];
414 val nnf_extra_simps =
415 thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
418 HOL_basic_ss addsimps nnf_extra_simps
419 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
421 fun make_nnf th = th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
422 |> simplify nnf_ss (*But this doesn't simplify premises...*)
425 (*Pull existential quantifiers to front. This accomplishes Skolemization for
426 clauses that arise from a subgoal.*)
428 if not (has_conns ["Ex"] (prop_of th)) then th
429 else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
430 disj_exD, disj_exD1, disj_exD2])))
432 skolemize (forward_res skolemize
433 (tryres (th, [conj_forward, disj_forward, all_forward])))
434 handle THM _ => forward_res skolemize (th RS ex_forward);
437 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
438 The resulting clauses are HOL disjunctions.*)
439 fun make_clauses ths =
440 (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
442 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
445 (distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
447 (*Could simply use nprems_of, which would count remaining subgoals -- no
448 discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
450 fun best_prolog_tac sizef horns =
451 BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
453 fun depth_prolog_tac horns =
454 DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
456 (*Return all negative clauses, as possible goal clauses*)
457 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
459 fun skolemize_prems_tac prems =
460 cut_facts_tac (map (skolemize o make_nnf) prems) THEN'
463 (*Expand all definitions (presumably of Skolem functions) in a proof state.*)
464 fun expand_defs_tac st =
465 let val defs = filter (can dest_equals) (#hyps (crep_thm st))
466 in PRIMITIVE (LocalDefs.def_export false defs) st end;
468 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions*)
469 fun MESON cltac i st =
471 (EVERY [rtac ccontr 1,
473 EVERY1 [skolemize_prems_tac negs,
474 METAHYPS (cltac o make_clauses)]) 1,
475 expand_defs_tac]) i st
476 handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
478 (** Best-first search versions **)
480 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
481 fun best_meson_tac sizef =
483 THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
484 (has_fewer_prems 1, sizef)
485 (prolog_step_tac (make_horns cls) 1));
487 (*First, breaks the goal into independent units*)
488 val safe_best_meson_tac =
489 SELECT_GOAL (TRY Safe_tac THEN
490 TRYALL (best_meson_tac size_of_subgoals));
492 (** Depth-first search version **)
494 val depth_meson_tac =
495 MESON (fn cls => EVERY [resolve_tac (gocls cls) 1,
496 depth_prolog_tac (make_horns cls)]);
499 (** Iterative deepening version **)
501 (*This version does only one inference per call;
502 having only one eq_assume_tac speeds it up!*)
503 fun prolog_step_tac' horns =
504 let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
505 take_prefix Thm.no_prems horns
506 val nrtac = net_resolve_tac horns
507 in fn i => eq_assume_tac i ORELSE
508 match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*)
509 ((assume_tac i APPEND nrtac i) THEN check_tac)
512 fun iter_deepen_prolog_tac horns =
513 ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
515 fun iter_deepen_meson_tac ths =
517 case (gocls (cls@ths)) of
518 [] => no_tac (*no goal clauses*)
520 (THEN_ITER_DEEPEN (resolve_tac goes 1)
522 (prolog_step_tac' (make_horns (cls@ths)))));
524 fun meson_claset_tac ths cs =
525 SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
527 val meson_tac = CLASET' (meson_claset_tac []);
530 (**** Code to support ordinary resolution, rather than Model Elimination ****)
532 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
533 with no contrapositives, for ordinary resolution.*)
535 (*Rules to convert the head literal into a negated assumption. If the head
536 literal is already negated, then using notEfalse instead of notEfalse'
537 prevents a double negation.*)
538 val notEfalse = read_instantiate [("R","False")] notE;
539 val notEfalse' = rotate_prems 1 notEfalse;
541 fun negated_asm_of_head th =
542 th RS notEfalse handle THM _ => th RS notEfalse';
544 (*Converting one clause*)
545 fun make_meta_clause th =
546 if is_fol_term (prop_of th)
547 then negated_asm_of_head (make_horn resolution_clause_rules th)
548 else raise THM("make_meta_clause", 0, [th]);
550 fun make_meta_clauses ths =
552 (distinct Drule.eq_thm_prop (map make_meta_clause ths));
554 (*Permute a rule's premises to move the i-th premise to the last position.*)
556 let val n = nprems_of th
557 in if 1 <= i andalso i <= n
558 then Thm.permute_prems (i-1) 1 th
559 else raise THM("select_literal", i, [th])
562 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
564 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
566 (*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
567 fun select_literal i cl = negate_head (make_last i cl);
570 (*Top-level Skolemization. Allows part of the conversion to clauses to be
571 expressed as a tactic (or Isar method). Each assumption of the selected
572 goal is converted to NNF and then its existential quantifiers are pulled
573 to the front. Finally, all existential quantifiers are eliminated,
574 leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
575 might generate many subgoals.*)
577 fun skolemize_tac i st =
578 let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
581 (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
582 THEN REPEAT (etac exE 1))),
583 REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
585 handle Subscript => Seq.empty;
587 (*Top-level conversion to meta-level clauses. Each clause has
588 leading !!-bound universal variables, to express generality. To get
589 disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
590 val make_clauses_tac =
593 let val ts = Logic.strip_assums_hyp prop
598 (map forall_intr_vars
599 (make_meta_clauses (make_clauses hyps))) 1)),
600 REPEAT_DETERM_N (length ts) o (etac thin_rl)]
604 (*** setup the special skoklemization methods ***)
606 (*No CHANGED_PROP here, since these always appear in the preamble*)
608 val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac;
610 val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
612 val skolemize_setup =
614 [("skolemize", Method.no_args skolemize_meth,
615 "Skolemization into existential quantifiers"),
616 ("make_clauses", Method.no_args make_clauses_meth,
617 "Conversion to !!-quantified meta-level clauses")];
621 structure BasicMeson: BASIC_MESON = Meson;