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