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