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