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