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