src/HOL/Tools/meson.ML
author paulson
Fri Aug 25 18:47:36 2006 +0200 (2006-08-25)
changeset 20417 c611b1412056
parent 20361 1aaf9ebe248d
child 20524 1493053fc111
permissions -rw-r--r--
better skolemization, using first-order resolution rather than hoping for the right result
     1 (*  Title:      HOL/Tools/meson.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 The MESON resolution proof procedure for HOL.
     7 
     8 When making clauses, avoids using the rewriter -- instead uses RS recursively
     9 
    10 NEED TO SORT LITERALS BY # OF VARS, USING ==>I/E.  ELIMINATES NEED FOR
    11 FUNCTION nodups -- if done to goal clauses too!
    12 *)
    13 
    14 signature BASIC_MESON =
    15 sig
    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
    40 end
    41 
    42 
    43 structure Meson =
    44 struct
    45 
    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";
    64 
    65 val depth_limit = ref 2000;
    66 
    67 (**** Operators for forward proof ****)
    68 
    69 
    70 (** First-order Resolution **)
    71 
    72 fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
    73 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
    74 
    75 val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
    76 
    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]);
    87 
    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)
    92   in  tryall rls  end;
    93   
    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)
    97   of SOME(th,_) => th
    98    | NONE => raise THM("forward_res", 0, [st]);
    99 
   100 
   101 (*Are any of the logical connectives in "bs" present in the term?*)
   102 fun has_conns bs =
   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
   110 	| has _ = false
   111   in  has  end;
   112   
   113 
   114 (**** Clause handling ****)
   115 
   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)];
   120 
   121 (*number of literals in a term*)
   122 val nliterals = length o literals;
   123 
   124 
   125 (*** Tautology Checking ***)
   126 
   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);
   131   
   132 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
   133 
   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;
   138 
   139 fun is_taut th =
   140   let val (poslits,neglits) = signed_lits th
   141   in  exists taut_poslit poslits
   142       orelse
   143       exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
   144   end
   145   handle TERM _ => false;	(*probably dest_Trueprop on a weird theorem*)		      
   146 
   147 
   148 (*** To remove trivial negated equality literals from clauses ***)
   149 
   150 (*They are typically functional reflexivity axioms and are the converses of
   151   injectivity equivalences*)
   152   
   153 val not_refl_disj_D = thm"meson_not_refl_disj_D";
   154 
   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;
   159 
   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)) $ _) => 
   166 	    if eliminable(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;
   171 
   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;
   176 
   177 (*Simplify a clause by applying reflexivity to its negated equality literals*)
   178 fun refl_clause th = 
   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*)		      
   182 
   183 
   184 (*** The basic CNF transformation ***)
   185 
   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 *)
   193 
   194 (*Replaces universally quantified variables by FREE variables -- because
   195   assumptions may not contain scheme variables.  Later, call "generalize". *)
   196 fun freeze_spec th =
   197   let val newname = gensym "mes_"
   198       val spec' = read_instantiate [("x", newname)] spec
   199   in  th RS spec'  end;
   200 
   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;
   205 
   206 val has_meta_conn = 
   207     exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
   208 
   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)
   212   in  tryall rls  end;
   213   
   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)
   227 	  | Const ("Ex", _) => 
   228 	      (*existential quantifier: Insert Skolem functions*)
   229 	      cnf_aux (apply_skolem_ths (th,skoths), ths)
   230 	  | Const ("op |", _) => (*disjunction*)
   231 	      let val tac =
   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,[])
   237   in 
   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)
   241   end;
   242 
   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));
   246 
   247 fun make_cnf skoths th = cnf skoths (th, []);
   248 
   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);
   251 
   252 
   253 (**** Removal of duplicate literals ****)
   254 
   255 (*Forward proof, passing extra assumptions as theorems to the tactic*)
   256 fun forward_res2 nf hyps st =
   257   case Seq.pull
   258 	(REPEAT
   259 	 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
   260 	 st)
   261   of SOME(th,_) => th
   262    | NONE => raise THM("forward_res2", 0, [st]);
   263 
   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])
   270     handle THM _ => th;
   271 
   272 (*Remove duplicate literals, if there are any*)
   273 fun nodups th =
   274     if null(findrep(literals(prop_of th))) then th
   275     else nodups_aux [] th;
   276 
   277 
   278 (**** Generation of contrapositives ****)
   279 
   280 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
   281 fun assoc_right th = assoc_right (th RS disj_assoc)
   282 	handle THM _ => th;
   283 
   284 (*Must check for negative literal first!*)
   285 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
   286 
   287 (*For ordinary resolution. *)
   288 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
   289 
   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]);
   294 
   295 (*Sort clauses by number of literals*)
   296 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
   297 
   298 fun sort_clauses ths = sort (make_ord fewerlits) ths;
   299 
   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;
   304   
   305 (*Is the string the name of a connective? It doesn't matter if this list is
   306   incomplete, since when actually called, the only connectives likely to
   307   remain are & | Not.*)  
   308 val is_conn = member (op =)
   309     ["Trueprop", "op &", "op |", "op -->", "op =", "Not", 
   310      "All", "Ex", "Ball", "Bex"];
   311 
   312 (*True if the term contains a function where the type of any argument contains
   313   bool.*)
   314 val has_bool_arg_const = 
   315     exists_Const
   316       (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
   317       
   318 (*Raises an exception if any Vars in the theorem mention type bool; they
   319   could cause make_horn to loop! Also rejects functions whose arguments are 
   320   Booleans or other functions.*)
   321 fun is_fol_term t =
   322     not (exists (has_bool o fastype_of) (term_vars t)  orelse
   323 	 not (Term.is_first_order ["all","All","Ex"] t) orelse
   324 	 has_bool_arg_const t  orelse  
   325 	 has_meta_conn t);
   326 
   327 (*Create a meta-level Horn clause*)
   328 fun make_horn crules th = make_horn crules (tryres(th,crules))
   329 			  handle THM _ => th;
   330 
   331 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
   332   is a HOL disjunction.*)
   333 fun add_contras crules (th,hcs) =
   334   let fun rots (0,th) = hcs
   335 	| rots (k,th) = zero_var_indexes (make_horn crules th) ::
   336 			rots(k-1, assoc_right (th RS disj_comm))
   337   in case nliterals(prop_of th) of
   338 	1 => th::hcs
   339       | n => rots(n, assoc_right th)
   340   end;
   341 
   342 (*Use "theorem naming" to label the clauses*)
   343 fun name_thms label =
   344     let fun name1 (th, (k,ths)) =
   345 	  (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
   346 
   347     in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
   348 
   349 (*Is the given disjunction an all-negative support clause?*)
   350 fun is_negative th = forall (not o #1) (literals (prop_of th));
   351 
   352 val neg_clauses = List.filter is_negative;
   353 
   354 
   355 (***** MESON PROOF PROCEDURE *****)
   356 
   357 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
   358 	   As) = rhyps(phi, A::As)
   359   | rhyps (_, As) = As;
   360 
   361 (** Detecting repeated assumptions in a subgoal **)
   362 
   363 (*The stringtree detects repeated assumptions.*)
   364 fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
   365 
   366 (*detects repetitions in a list of terms*)
   367 fun has_reps [] = false
   368   | has_reps [_] = false
   369   | has_reps [t,u] = (t aconv u)
   370   | has_reps ts = (Library.foldl ins_term (Net.empty, ts);  false)
   371 		  handle Net.INSERT => true;
   372 
   373 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
   374 fun TRYING_eq_assume_tac 0 st = Seq.single st
   375   | TRYING_eq_assume_tac i st =
   376        TRYING_eq_assume_tac (i-1) (eq_assumption i st)
   377        handle THM _ => TRYING_eq_assume_tac (i-1) st;
   378 
   379 fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
   380 
   381 (*Loop checking: FAIL if trying to prove the same thing twice
   382   -- if *ANY* subgoal has repeated literals*)
   383 fun check_tac st =
   384   if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
   385   then  Seq.empty  else  Seq.single st;
   386 
   387 
   388 (* net_resolve_tac actually made it slower... *)
   389 fun prolog_step_tac horns i =
   390     (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
   391     TRYALL_eq_assume_tac;
   392 
   393 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   394 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
   395 
   396 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
   397 
   398 
   399 (*Negation Normal Form*)
   400 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
   401                not_impD, not_iffD, not_allD, not_exD, not_notD];
   402 
   403 fun make_nnf1 th = make_nnf1 (tryres(th, nnf_rls))
   404     handle THM _ =>
   405         forward_res make_nnf1
   406            (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
   407     handle THM _ => th;
   408 
   409 (*The simplification removes defined quantifiers and occurrences of True and False. 
   410   nnf_ss also includes the one-point simprocs,
   411   which are needed to avoid the various one-point theorems from generating junk clauses.*)
   412 val nnf_simps =
   413      [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True, 
   414       if_False, if_cancel, if_eq_cancel, cases_simp];
   415 val nnf_extra_simps =
   416       thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
   417 
   418 val nnf_ss =
   419     HOL_basic_ss addsimps nnf_extra_simps 
   420                  addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
   421 
   422 fun make_nnf th = th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
   423                      |> simplify nnf_ss  (*But this doesn't simplify premises...*)
   424                      |> make_nnf1
   425 
   426 (*Pull existential quantifiers to front. This accomplishes Skolemization for
   427   clauses that arise from a subgoal.*)
   428 fun skolemize th =
   429   if not (has_conns ["Ex"] (prop_of th)) then th
   430   else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
   431                               disj_exD, disj_exD1, disj_exD2])))
   432     handle THM _ =>
   433         skolemize (forward_res skolemize
   434                    (tryres (th, [conj_forward, disj_forward, all_forward])))
   435     handle THM _ => forward_res skolemize (th RS ex_forward);
   436 
   437 
   438 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   439   The resulting clauses are HOL disjunctions.*)
   440 fun make_clauses ths =
   441     (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
   442 
   443 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   444 fun make_horns ths =
   445     name_thms "Horn#"
   446       (distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
   447 
   448 (*Could simply use nprems_of, which would count remaining subgoals -- no
   449   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   450 
   451 fun best_prolog_tac sizef horns =
   452     BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
   453 
   454 fun depth_prolog_tac horns =
   455     DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
   456 
   457 (*Return all negative clauses, as possible goal clauses*)
   458 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
   459 
   460 fun skolemize_prems_tac prems =
   461     cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
   462     REPEAT o (etac exE);
   463 
   464 (*Expand all definitions (presumably of Skolem functions) in a proof state.*)
   465 fun expand_defs_tac st =
   466   let val defs = filter (can dest_equals) (#hyps (crep_thm st))
   467   in  PRIMITIVE (LocalDefs.def_export false defs) st  end;
   468 
   469 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
   470 fun MESON cltac i st = 
   471   SELECT_GOAL
   472     (EVERY [rtac ccontr 1,
   473 	    METAHYPS (fn negs =>
   474 		      EVERY1 [skolemize_prems_tac negs,
   475 			      METAHYPS (cltac o make_clauses)]) 1,
   476             expand_defs_tac]) i st
   477   handle THM _ => no_tac st;	(*probably from make_meta_clause, not first-order*)		      
   478 
   479 (** Best-first search versions **)
   480 
   481 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
   482 fun best_meson_tac sizef =
   483   MESON (fn cls =>
   484          THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   485                          (has_fewer_prems 1, sizef)
   486                          (prolog_step_tac (make_horns cls) 1));
   487 
   488 (*First, breaks the goal into independent units*)
   489 val safe_best_meson_tac =
   490      SELECT_GOAL (TRY Safe_tac THEN
   491                   TRYALL (best_meson_tac size_of_subgoals));
   492 
   493 (** Depth-first search version **)
   494 
   495 val depth_meson_tac =
   496      MESON (fn cls => EVERY [resolve_tac (gocls cls) 1,
   497                              depth_prolog_tac (make_horns cls)]);
   498 
   499 
   500 (** Iterative deepening version **)
   501 
   502 (*This version does only one inference per call;
   503   having only one eq_assume_tac speeds it up!*)
   504 fun prolog_step_tac' horns =
   505     let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
   506             take_prefix Thm.no_prems horns
   507         val nrtac = net_resolve_tac horns
   508     in  fn i => eq_assume_tac i ORELSE
   509                 match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   510                 ((assume_tac i APPEND nrtac i) THEN check_tac)
   511     end;
   512 
   513 fun iter_deepen_prolog_tac horns =
   514     ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
   515 
   516 fun iter_deepen_meson_tac ths =
   517   MESON (fn cls =>
   518            case (gocls (cls@ths)) of
   519            	[] => no_tac  (*no goal clauses*)
   520               | goes => 
   521 		 (THEN_ITER_DEEPEN (resolve_tac goes 1)
   522 				   (has_fewer_prems 1)
   523 				   (prolog_step_tac' (make_horns (cls@ths)))));
   524 
   525 fun meson_claset_tac ths cs =
   526   SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
   527 
   528 val meson_tac = CLASET' (meson_claset_tac []);
   529 
   530 
   531 (**** Code to support ordinary resolution, rather than Model Elimination ****)
   532 
   533 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>), 
   534   with no contrapositives, for ordinary resolution.*)
   535 
   536 (*Rules to convert the head literal into a negated assumption. If the head
   537   literal is already negated, then using notEfalse instead of notEfalse'
   538   prevents a double negation.*)
   539 val notEfalse = read_instantiate [("R","False")] notE;
   540 val notEfalse' = rotate_prems 1 notEfalse;
   541 
   542 fun negated_asm_of_head th = 
   543     th RS notEfalse handle THM _ => th RS notEfalse';
   544 
   545 (*Converting one clause*)
   546 fun make_meta_clause th = 
   547   if is_fol_term (prop_of th) 
   548   then negated_asm_of_head (make_horn resolution_clause_rules th)
   549   else raise THM("make_meta_clause", 0, [th]);
   550 
   551 fun make_meta_clauses ths =
   552     name_thms "MClause#"
   553       (distinct Drule.eq_thm_prop (map make_meta_clause ths));
   554 
   555 (*Permute a rule's premises to move the i-th premise to the last position.*)
   556 fun make_last i th =
   557   let val n = nprems_of th 
   558   in  if 1 <= i andalso i <= n 
   559       then Thm.permute_prems (i-1) 1 th
   560       else raise THM("select_literal", i, [th])
   561   end;
   562 
   563 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   564   double-negations.*)
   565 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
   566 
   567 (*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   568 fun select_literal i cl = negate_head (make_last i cl);
   569 
   570 
   571 (*Top-level Skolemization. Allows part of the conversion to clauses to be
   572   expressed as a tactic (or Isar method).  Each assumption of the selected 
   573   goal is converted to NNF and then its existential quantifiers are pulled
   574   to the front. Finally, all existential quantifiers are eliminated, 
   575   leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
   576   might generate many subgoals.*)
   577 
   578 fun skolemize_tac i st = 
   579   let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
   580   in 
   581      EVERY' [METAHYPS
   582 	    (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
   583                          THEN REPEAT (etac exE 1))),
   584             REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
   585   end
   586   handle Subscript => Seq.empty;
   587 
   588 (*Top-level conversion to meta-level clauses. Each clause has  
   589   leading !!-bound universal variables, to express generality. To get 
   590   disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
   591 val make_clauses_tac = 
   592   SUBGOAL
   593     (fn (prop,_) =>
   594      let val ts = Logic.strip_assums_hyp prop
   595      in EVERY1 
   596 	 [METAHYPS
   597 	    (fn hyps => 
   598               (Method.insert_tac
   599                 (map forall_intr_vars 
   600                   (make_meta_clauses (make_clauses hyps))) 1)),
   601 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   602      end);
   603      
   604      
   605 (*** setup the special skoklemization methods ***)
   606 
   607 (*No CHANGED_PROP here, since these always appear in the preamble*)
   608 
   609 val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac;
   610 
   611 val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
   612 
   613 val skolemize_setup =
   614   Method.add_methods
   615     [("skolemize", Method.no_args skolemize_meth, 
   616       "Skolemization into existential quantifiers"),
   617      ("make_clauses", Method.no_args make_clauses_meth, 
   618       "Conversion to !!-quantified meta-level clauses")];
   619 
   620 end;
   621 
   622 structure BasicMeson: BASIC_MESON = Meson;
   623 open BasicMeson;