src/HOL/Tools/meson.ML
author haftmann
Thu Aug 26 20:51:17 2010 +0200 (2010-08-26)
changeset 38786 e46e7a9cb622
parent 38709 04414091f3b5
child 38795 848be46708dc
permissions -rw-r--r--
formerly unnamed infix impliciation now named HOL.implies
     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 Thm.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 HOL.implies},_) $ 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 HOL.implies}, @{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 |> make_nnf1 ctxt
   543   | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
   544 
   545 (*Pull existential quantifiers to front. This accomplishes Skolemization for
   546   clauses that arise from a subgoal.*)
   547 fun skolemize1 ctxt th =
   548   if not (has_conns [@{const_name Ex}] (prop_of th)) then th
   549   else (skolemize1 ctxt (tryres(th, [choice, conj_exD1, conj_exD2,
   550                               disj_exD, disj_exD1, disj_exD2])))
   551     handle THM ("tryres", _, _) =>
   552         skolemize1 ctxt (forward_res ctxt (skolemize1 ctxt)
   553                    (tryres (th, [conj_forward, disj_forward, all_forward])))
   554     handle THM ("tryres", _, _) => 
   555         forward_res ctxt (skolemize1 ctxt) (rename_bvs_RS th ex_forward);
   556 
   557 fun skolemize ctxt th = skolemize1 ctxt (make_nnf ctxt th);
   558 
   559 fun skolemize_nnf_list _ [] = []
   560   | skolemize_nnf_list ctxt (th::ths) =
   561       skolemize ctxt th :: skolemize_nnf_list ctxt ths
   562       handle THM _ => (*RS can fail if Unify.search_bound is too small*)
   563        (trace_msg (fn () => "Failed to Skolemize " ^ Display.string_of_thm ctxt th);
   564         skolemize_nnf_list ctxt ths);
   565 
   566 fun add_clauses th cls =
   567   let val ctxt0 = Variable.global_thm_context th
   568       val (cnfs, ctxt) = make_cnf [] th ctxt0
   569   in Variable.export ctxt ctxt0 cnfs @ cls end;
   570 
   571 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   572   The resulting clauses are HOL disjunctions.*)
   573 fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
   574 val make_clauses = sort_clauses o make_clauses_unsorted;
   575 
   576 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   577 fun make_horns ths =
   578     name_thms "Horn#"
   579       (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths []));
   580 
   581 (*Could simply use nprems_of, which would count remaining subgoals -- no
   582   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   583 
   584 fun best_prolog_tac sizef horns =
   585     BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
   586 
   587 fun depth_prolog_tac horns =
   588     DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
   589 
   590 (*Return all negative clauses, as possible goal clauses*)
   591 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
   592 
   593 fun skolemize_prems_tac ctxt prems =
   594   cut_facts_tac (skolemize_nnf_list ctxt prems) THEN' REPEAT o etac exE
   595 
   596 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
   597   Function mkcl converts theorems to clauses.*)
   598 fun MESON mkcl cltac ctxt i st =
   599   SELECT_GOAL
   600     (EVERY [Object_Logic.atomize_prems_tac 1,
   601             rtac ccontr 1,
   602             Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
   603                       EVERY1 [skolemize_prems_tac ctxt negs,
   604                               Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
   605   handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
   606 
   607 (** Best-first search versions **)
   608 
   609 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
   610 fun best_meson_tac sizef =
   611   MESON make_clauses
   612     (fn cls =>
   613          THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   614                          (has_fewer_prems 1, sizef)
   615                          (prolog_step_tac (make_horns cls) 1));
   616 
   617 (*First, breaks the goal into independent units*)
   618 fun safe_best_meson_tac ctxt =
   619      SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN
   620                   TRYALL (best_meson_tac size_of_subgoals ctxt));
   621 
   622 (** Depth-first search version **)
   623 
   624 val depth_meson_tac =
   625   MESON make_clauses
   626     (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
   627 
   628 
   629 (** Iterative deepening version **)
   630 
   631 (*This version does only one inference per call;
   632   having only one eq_assume_tac speeds it up!*)
   633 fun prolog_step_tac' horns =
   634     let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
   635             take_prefix Thm.no_prems horns
   636         val nrtac = net_resolve_tac horns
   637     in  fn i => eq_assume_tac i ORELSE
   638                 match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   639                 ((assume_tac i APPEND nrtac i) THEN check_tac)
   640     end;
   641 
   642 fun iter_deepen_prolog_tac horns =
   643     ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
   644 
   645 fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON make_clauses
   646   (fn cls =>
   647     (case (gocls (cls @ ths)) of
   648       [] => no_tac  (*no goal clauses*)
   649     | goes =>
   650         let
   651           val horns = make_horns (cls @ ths)
   652           val _ = trace_msg (fn () =>
   653             cat_lines ("meson method called:" ::
   654               map (Display.string_of_thm ctxt) (cls @ ths) @
   655               ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
   656         in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end));
   657 
   658 fun meson_tac ctxt ths =
   659   SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
   660 
   661 
   662 (**** Code to support ordinary resolution, rather than Model Elimination ****)
   663 
   664 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
   665   with no contrapositives, for ordinary resolution.*)
   666 
   667 (*Rules to convert the head literal into a negated assumption. If the head
   668   literal is already negated, then using notEfalse instead of notEfalse'
   669   prevents a double negation.*)
   670 val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
   671 val notEfalse' = rotate_prems 1 notEfalse;
   672 
   673 fun negated_asm_of_head th =
   674     th RS notEfalse handle THM _ => th RS notEfalse';
   675 
   676 (*Converting one theorem from a disjunction to a meta-level clause*)
   677 fun make_meta_clause th =
   678   let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
   679   in  
   680       (zero_var_indexes o Thm.varifyT_global o thaw 0 o 
   681        negated_asm_of_head o make_horn resolution_clause_rules) fth
   682   end;
   683 
   684 fun make_meta_clauses ths =
   685     name_thms "MClause#"
   686       (distinct Thm.eq_thm_prop (map make_meta_clause ths));
   687 
   688 (*Permute a rule's premises to move the i-th premise to the last position.*)
   689 fun make_last i th =
   690   let val n = nprems_of th
   691   in  if 1 <= i andalso i <= n
   692       then Thm.permute_prems (i-1) 1 th
   693       else raise THM("select_literal", i, [th])
   694   end;
   695 
   696 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   697   double-negations.*)
   698 val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection];
   699 
   700 (*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   701 fun select_literal i cl = negate_head (make_last i cl);
   702 
   703 
   704 (*Top-level Skolemization. Allows part of the conversion to clauses to be
   705   expressed as a tactic (or Isar method).  Each assumption of the selected
   706   goal is converted to NNF and then its existential quantifiers are pulled
   707   to the front. Finally, all existential quantifiers are eliminated,
   708   leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
   709   might generate many subgoals.*)
   710 
   711 fun skolemize_tac ctxt = SUBGOAL (fn (goal, i) =>
   712   let val ts = Logic.strip_assums_hyp goal
   713   in
   714     EVERY'
   715      [Misc_Legacy.METAHYPS (fn hyps =>
   716         (cut_facts_tac (skolemize_nnf_list ctxt hyps) 1
   717           THEN REPEAT (etac exE 1))),
   718       REPEAT_DETERM_N (length ts) o (etac thin_rl)] i
   719   end);
   720 
   721 end;