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