src/HOL/Tools/Metis/metis_tactics.ML
author wenzelm
Mon May 02 16:33:21 2011 +0200 (2011-05-02)
changeset 42616 92715b528e78
parent 42552 e155be7125ba
child 42650 552eae49f97d
permissions -rw-r--r--
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
proper name bindings;
     1 (*  Title:      HOL/Tools/Metis/metis_tactics.ML
     2     Author:     Kong W. Susanto, Cambridge University Computer Laboratory
     3     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     4     Author:     Jasmin Blanchette, TU Muenchen
     5     Copyright   Cambridge University 2007
     6 
     7 HOL setup for the Metis prover.
     8 *)
     9 
    10 signature METIS_TACTICS =
    11 sig
    12   val trace : bool Config.T
    13   val verbose : bool Config.T
    14   val type_lits : bool Config.T
    15   val new_skolemizer : bool Config.T
    16   val metis_tac : Proof.context -> thm list -> int -> tactic
    17   val metisF_tac : Proof.context -> thm list -> int -> tactic
    18   val metisFT_tac : Proof.context -> thm list -> int -> tactic
    19   val setup : theory -> theory
    20 end
    21 
    22 structure Metis_Tactics : METIS_TACTICS =
    23 struct
    24 
    25 open Metis_Translate
    26 open Metis_Reconstruct
    27 
    28 val type_lits = Attrib.setup_config_bool @{binding metis_type_lits} (K true)
    29 val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    30 
    31 fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
    32 
    33 fun have_common_thm ths1 ths2 =
    34   exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2)
    35 
    36 (*Determining which axiom clauses are actually used*)
    37 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
    38   | used_axioms _ _ = NONE;
    39 
    40 val clause_params =
    41   {ordering = Metis_KnuthBendixOrder.default,
    42    orderLiterals = Metis_Clause.UnsignedLiteralOrder,
    43    orderTerms = true}
    44 val active_params =
    45   {clause = clause_params,
    46    prefactor = #prefactor Metis_Active.default,
    47    postfactor = #postfactor Metis_Active.default}
    48 val waiting_params =
    49   {symbolsWeight = 1.0,
    50    variablesWeight = 0.0,
    51    literalsWeight = 0.0,
    52    models = []}
    53 val resolution_params = {active = active_params, waiting = waiting_params}
    54 
    55 (* Main function to start Metis proof and reconstruction *)
    56 fun FOL_SOLVE mode ctxt cls ths0 =
    57   let val thy = Proof_Context.theory_of ctxt
    58       val type_lits = Config.get ctxt type_lits
    59       val new_skolemizer =
    60         Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
    61       val th_cls_pairs =
    62         map2 (fn j => fn th =>
    63                 (Thm.get_name_hint th,
    64                  Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
    65              (0 upto length ths0 - 1) ths0
    66       val thss = map (snd o snd) th_cls_pairs
    67       val dischargers = map (fst o snd) th_cls_pairs
    68       val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
    69       val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
    70       val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
    71       val _ = app (app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th))) thss
    72       val (mode, {axioms, tfrees, old_skolems}) =
    73         prepare_metis_problem mode ctxt type_lits cls thss
    74       val _ = if null tfrees then ()
    75               else (trace_msg ctxt (fn () => "TFREE CLAUSES");
    76                     app (fn TyLitFree ((s, _), (s', _)) =>
    77                             trace_msg ctxt (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
    78       val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
    79       val thms = map #1 axioms
    80       val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
    81       val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode)
    82       val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
    83   in
    84       case filter (is_false o prop_of) cls of
    85           false_th::_ => [false_th RS @{thm FalseE}]
    86         | [] =>
    87       case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
    88            |> Metis_Resolution.loop of
    89           Metis_Resolution.Contradiction mth =>
    90             let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
    91                           Metis_Thm.toString mth)
    92                 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
    93                              (*add constraints arising from converting goal to clause form*)
    94                 val proof = Metis_Proof.proof mth
    95                 val result = fold (replay_one_inference ctxt' mode old_skolems)
    96                                   proof axioms
    97                 and used = map_filter (used_axioms axioms) proof
    98                 val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
    99                 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
   100                 val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) =>
   101                   if have_common_thm used cls then NONE else SOME name)
   102             in
   103                 if not (null cls) andalso not (have_common_thm used cls) then
   104                   verbose_warning ctxt "Metis: The assumptions are inconsistent"
   105                 else
   106                   ();
   107                 if not (null unused) then
   108                   verbose_warning ctxt ("Metis: Unused theorems: " ^
   109                                         commas_quote unused)
   110                 else
   111                   ();
   112                 case result of
   113                     (_,ith)::_ =>
   114                         (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
   115                          [discharge_skolem_premises ctxt dischargers ith])
   116                   | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
   117             end
   118         | Metis_Resolution.Satisfiable _ =>
   119             (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
   120              [])
   121   end;
   122 
   123 (* Extensionalize "th", because that makes sense and that's what Sledgehammer
   124    does, but also keep an unextensionalized version of "th" for backward
   125    compatibility. *)
   126 fun also_extensionalize_theorem th =
   127   let val th' = Meson_Clausify.extensionalize_theorem th in
   128     if Thm.eq_thm (th, th') then [th]
   129     else th :: Meson.make_clauses_unsorted [th']
   130   end
   131 
   132 val neg_clausify =
   133   single
   134   #> Meson.make_clauses_unsorted
   135   #> maps also_extensionalize_theorem
   136   #> map Meson_Clausify.introduce_combinators_in_theorem
   137   #> Meson.finish_cnf
   138 
   139 fun preskolem_tac ctxt st0 =
   140   (if exists (Meson.has_too_many_clauses ctxt)
   141              (Logic.prems_of_goal (prop_of st0) 1) then
   142      Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
   143      THEN cnf.cnfx_rewrite_tac ctxt 1
   144    else
   145      all_tac) st0
   146 
   147 val type_has_top_sort =
   148   exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
   149 
   150 fun generic_metis_tac mode ctxt ths i st0 =
   151   let
   152     val _ = trace_msg ctxt (fn () =>
   153         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   154   in
   155     if exists_type type_has_top_sort (prop_of st0) then
   156       (verbose_warning ctxt "Metis: Proof state contains the universal sort {}";
   157        Seq.empty)
   158     else
   159       Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
   160                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
   161                   ctxt i st0
   162       handle ERROR message =>
   163              error (message |> mode <> FT
   164                                ? suffix "\nHint: You might want to try out \
   165                                         \\"metisFT\".")
   166   end
   167 
   168 val metis_tac = generic_metis_tac HO
   169 val metisF_tac = generic_metis_tac FO
   170 val metisFT_tac = generic_metis_tac FT
   171 
   172 (* Whenever "X" has schematic type variables, we treat "using X by metis" as
   173    "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
   174    We don't do it for nonschematic facts "X" because this breaks a few proofs
   175    (in the rare and subtle case where a proof relied on extensionality not being
   176    applied) and brings few benefits. *)
   177 val has_tvar =
   178   exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
   179 fun method name mode =
   180   Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
   181     METHOD (fn facts =>
   182                let
   183                  val (schem_facts, nonschem_facts) =
   184                    List.partition has_tvar facts
   185                in
   186                  HEADGOAL (Method.insert_tac nonschem_facts THEN'
   187                            CHANGED_PROP
   188                            o generic_metis_tac mode ctxt (schem_facts @ ths))
   189                end)))
   190 
   191 val setup =
   192   method @{binding metis} HO "Metis for FOL/HOL problems"
   193   #> method @{binding metisF} FO "Metis for FOL problems"
   194   #> method @{binding metisFT} FT
   195             "Metis for FOL/HOL problems with fully-typed translation"
   196 
   197 end;