src/HOL/Tools/meson.ML
author wenzelm
Tue Oct 27 13:15:20 2009 +0100 (2009-10-27)
changeset 33222 89ced80833ac
parent 32960 69916a850301
child 33245 65232054ffd0
permissions -rw-r--r--
critical comments;
     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 (net,t) = 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 = (Library.foldl ins_term (Net.empty, ts);  false)
   472                   handle Net.INSERT => true;
   473 
   474 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
   475 fun TRYING_eq_assume_tac 0 st = Seq.single st
   476   | TRYING_eq_assume_tac i st =
   477        TRYING_eq_assume_tac (i-1) (Thm.eq_assumption i st)
   478        handle THM _ => TRYING_eq_assume_tac (i-1) st;
   479 
   480 fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
   481 
   482 (*Loop checking: FAIL if trying to prove the same thing twice
   483   -- if *ANY* subgoal has repeated literals*)
   484 fun check_tac st =
   485   if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
   486   then  Seq.empty  else  Seq.single st;
   487 
   488 
   489 (* net_resolve_tac actually made it slower... *)
   490 fun prolog_step_tac horns i =
   491     (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
   492     TRYALL_eq_assume_tac;
   493 
   494 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   495 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
   496 
   497 fun size_of_subgoals st = List.foldr addconcl 0 (prems_of st);
   498 
   499 
   500 (*Negation Normal Form*)
   501 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
   502                not_impD, not_iffD, not_allD, not_exD, not_notD];
   503 
   504 fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
   505   | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
   506   | ok4nnf _ = false;
   507 
   508 fun make_nnf1 ctxt th =
   509   if ok4nnf (concl_of th)
   510   then make_nnf1 ctxt (tryres(th, nnf_rls))
   511     handle THM ("tryres", _, _) =>
   512         forward_res ctxt (make_nnf1 ctxt)
   513            (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
   514     handle THM ("tryres", _, _) => th
   515   else th;
   516 
   517 (*The simplification removes defined quantifiers and occurrences of True and False.
   518   nnf_ss also includes the one-point simprocs,
   519   which are needed to avoid the various one-point theorems from generating junk clauses.*)
   520 val nnf_simps =
   521      [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
   522       if_False, if_cancel, if_eq_cancel, cases_simp];
   523 val nnf_extra_simps =
   524       thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
   525 
   526 val nnf_ss =
   527   HOL_basic_ss addsimps nnf_extra_simps
   528     addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
   529 
   530 fun make_nnf ctxt th = case prems_of th of
   531     [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
   532              |> simplify nnf_ss
   533              |> make_nnf1 ctxt
   534   | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
   535 
   536 (*Pull existential quantifiers to front. This accomplishes Skolemization for
   537   clauses that arise from a subgoal.*)
   538 fun skolemize1 ctxt th =
   539   if not (has_conns ["Ex"] (prop_of th)) then th
   540   else (skolemize1 ctxt (tryres(th, [choice, conj_exD1, conj_exD2,
   541                               disj_exD, disj_exD1, disj_exD2])))
   542     handle THM ("tryres", _, _) =>
   543         skolemize1 ctxt (forward_res ctxt (skolemize1 ctxt)
   544                    (tryres (th, [conj_forward, disj_forward, all_forward])))
   545     handle THM ("tryres", _, _) => 
   546         forward_res ctxt (skolemize1 ctxt) (rename_bvs_RS th ex_forward);
   547 
   548 fun skolemize ctxt th = skolemize1 ctxt (make_nnf ctxt th);
   549 
   550 fun skolemize_nnf_list _ [] = []
   551   | skolemize_nnf_list ctxt (th::ths) =
   552       skolemize ctxt th :: skolemize_nnf_list ctxt ths
   553       handle THM _ => (*RS can fail if Unify.search_bound is too small*)
   554        (trace_msg (fn () => "Failed to Skolemize " ^ Display.string_of_thm ctxt th);
   555         skolemize_nnf_list ctxt ths);
   556 
   557 fun add_clauses (th,cls) =
   558   let val ctxt0 = Variable.thm_context th
   559       val (cnfs,ctxt) = make_cnf [] th ctxt0
   560   in Variable.export ctxt ctxt0 cnfs @ cls end;
   561 
   562 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   563   The resulting clauses are HOL disjunctions.*)
   564 fun make_clauses ths = sort_clauses (List.foldr add_clauses [] ths);
   565 
   566 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   567 fun make_horns ths =
   568     name_thms "Horn#"
   569       (distinct Thm.eq_thm_prop (List.foldr (add_contras clause_rules) [] ths));
   570 
   571 (*Could simply use nprems_of, which would count remaining subgoals -- no
   572   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   573 
   574 fun best_prolog_tac sizef horns =
   575     BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
   576 
   577 fun depth_prolog_tac horns =
   578     DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
   579 
   580 (*Return all negative clauses, as possible goal clauses*)
   581 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
   582 
   583 fun skolemize_prems_tac ctxt prems =
   584     cut_facts_tac (skolemize_nnf_list ctxt prems) THEN'
   585     REPEAT o (etac exE);
   586 
   587 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
   588   Function mkcl converts theorems to clauses.*)
   589 fun MESON mkcl cltac ctxt i st =
   590   SELECT_GOAL
   591     (EVERY [ObjectLogic.atomize_prems_tac 1,
   592             rtac ccontr 1,
   593             Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
   594                       EVERY1 [skolemize_prems_tac ctxt negs,
   595                               Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
   596   handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
   597 
   598 (** Best-first search versions **)
   599 
   600 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
   601 fun best_meson_tac sizef =
   602   MESON make_clauses
   603     (fn cls =>
   604          THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   605                          (has_fewer_prems 1, sizef)
   606                          (prolog_step_tac (make_horns cls) 1));
   607 
   608 (*First, breaks the goal into independent units*)
   609 fun safe_best_meson_tac ctxt =
   610      SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN
   611                   TRYALL (best_meson_tac size_of_subgoals ctxt));
   612 
   613 (** Depth-first search version **)
   614 
   615 val depth_meson_tac =
   616   MESON make_clauses
   617     (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
   618 
   619 
   620 (** Iterative deepening version **)
   621 
   622 (*This version does only one inference per call;
   623   having only one eq_assume_tac speeds it up!*)
   624 fun prolog_step_tac' horns =
   625     let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
   626             take_prefix Thm.no_prems horns
   627         val nrtac = net_resolve_tac horns
   628     in  fn i => eq_assume_tac i ORELSE
   629                 match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   630                 ((assume_tac i APPEND nrtac i) THEN check_tac)
   631     end;
   632 
   633 fun iter_deepen_prolog_tac horns =
   634     ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
   635 
   636 fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON make_clauses
   637   (fn cls =>
   638     (case (gocls (cls @ ths)) of
   639       [] => no_tac  (*no goal clauses*)
   640     | goes =>
   641         let
   642           val horns = make_horns (cls @ ths)
   643           val _ = trace_msg (fn () =>
   644             cat_lines ("meson method called:" ::
   645               map (Display.string_of_thm ctxt) (cls @ ths) @
   646               ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
   647         in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end));
   648 
   649 fun meson_tac ctxt ths =
   650   SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
   651 
   652 
   653 (**** Code to support ordinary resolution, rather than Model Elimination ****)
   654 
   655 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
   656   with no contrapositives, for ordinary resolution.*)
   657 
   658 (*Rules to convert the head literal into a negated assumption. If the head
   659   literal is already negated, then using notEfalse instead of notEfalse'
   660   prevents a double negation.*)
   661 val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
   662 val notEfalse' = rotate_prems 1 notEfalse;
   663 
   664 fun negated_asm_of_head th =
   665     th RS notEfalse handle THM _ => th RS notEfalse';
   666 
   667 (*Converting one theorem from a disjunction to a meta-level clause*)
   668 fun make_meta_clause th =
   669   let val (fth,thaw) = Drule.freeze_thaw_robust th
   670   in  
   671       (zero_var_indexes o Thm.varifyT o thaw 0 o 
   672        negated_asm_of_head o make_horn resolution_clause_rules) fth
   673   end;
   674 
   675 fun make_meta_clauses ths =
   676     name_thms "MClause#"
   677       (distinct Thm.eq_thm_prop (map make_meta_clause ths));
   678 
   679 (*Permute a rule's premises to move the i-th premise to the last position.*)
   680 fun make_last i th =
   681   let val n = nprems_of th
   682   in  if 1 <= i andalso i <= n
   683       then Thm.permute_prems (i-1) 1 th
   684       else raise THM("select_literal", i, [th])
   685   end;
   686 
   687 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   688   double-negations.*)
   689 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
   690 
   691 (*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   692 fun select_literal i cl = negate_head (make_last i cl);
   693 
   694 
   695 (*Top-level Skolemization. Allows part of the conversion to clauses to be
   696   expressed as a tactic (or Isar method).  Each assumption of the selected
   697   goal is converted to NNF and then its existential quantifiers are pulled
   698   to the front. Finally, all existential quantifiers are eliminated,
   699   leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
   700   might generate many subgoals.*)
   701 
   702 fun skolemize_tac ctxt = SUBGOAL (fn (goal, i) =>
   703   let val ts = Logic.strip_assums_hyp goal
   704   in
   705     EVERY'
   706      [OldGoals.METAHYPS (fn hyps =>
   707         (cut_facts_tac (skolemize_nnf_list ctxt hyps) 1
   708           THEN REPEAT (etac exE 1))),
   709       REPEAT_DETERM_N (length ts) o (etac thin_rl)] i
   710   end);
   711 
   712 end;