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