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