src/HOL/Tools/Sledgehammer/metis_tactics.ML
author blanchet
Mon Sep 27 10:44:08 2010 +0200 (2010-09-27)
changeset 39720 0b93a954da4f
parent 39594 624d6c0e220d
child 39721 76a61ca09d5d
permissions -rw-r--r--
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
     1 (*  Title:      HOL/Tools/Sledgehammer/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 Unsynchronized.ref
    13   val type_lits : bool Config.T
    14   val metis_tac : Proof.context -> thm list -> int -> tactic
    15   val metisF_tac : Proof.context -> thm list -> int -> tactic
    16   val metisFT_tac : Proof.context -> thm list -> int -> tactic
    17   val setup : theory -> theory
    18 end
    19 
    20 structure Metis_Tactics : METIS_TACTICS =
    21 struct
    22 
    23 open Metis_Translate
    24 open Metis_Reconstruct
    25 
    26 fun trace_msg msg = if !trace then tracing (msg ()) else ()
    27 
    28 val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
    29 
    30 fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
    31 
    32 fun have_common_thm ths1 ths2 =
    33   exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2)
    34 
    35 (*Determining which axiom clauses are actually used*)
    36 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
    37   | used_axioms _ _ = NONE;
    38 
    39 val clause_params =
    40   {ordering = Metis_KnuthBendixOrder.default,
    41    orderLiterals = Metis_Clause.UnsignedLiteralOrder,
    42    orderTerms = true}
    43 val active_params =
    44   {clause = clause_params,
    45    prefactor = #prefactor Metis_Active.default,
    46    postfactor = #postfactor Metis_Active.default}
    47 val waiting_params =
    48   {symbolsWeight = 1.0,
    49    variablesWeight = 0.0,
    50    literalsWeight = 0.0,
    51    models = []}
    52 val resolution_params = {active = active_params, waiting = waiting_params}
    53 
    54 (* Main function to start Metis proof and reconstruction *)
    55 fun FOL_SOLVE mode ctxt cls ths0 =
    56   let val thy = ProofContext.theory_of ctxt
    57       val type_lits = Config.get ctxt type_lits
    58       val th_cls_pairs =
    59         map (fn th => (Thm.get_name_hint th,
    60                        Meson_Clausifier.cnf_axiom thy th)) ths0
    61       val ths = maps #2 th_cls_pairs
    62       val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
    63       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
    64       val _ = trace_msg (fn () => "THEOREM CLAUSES")
    65       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
    66       val (mode, {axioms, tfrees, skolems}) =
    67         build_logic_map mode ctxt type_lits cls ths
    68       val _ = if null tfrees then ()
    69               else (trace_msg (fn () => "TFREE CLAUSES");
    70                     app (fn TyLitFree ((s, _), (s', _)) =>
    71                             trace_msg (fn _ => s ^ "(" ^ s' ^ ")")) tfrees)
    72       val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
    73       val thms = map #1 axioms
    74       val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms
    75       val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
    76       val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
    77   in
    78       case filter (is_false o prop_of) cls of
    79           false_th::_ => [false_th RS @{thm FalseE}]
    80         | [] =>
    81       case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
    82            |> Metis_Resolution.loop of
    83           Metis_Resolution.Contradiction mth =>
    84             let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
    85                           Metis_Thm.toString mth)
    86                 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
    87                              (*add constraints arising from converting goal to clause form*)
    88                 val proof = Metis_Proof.proof mth
    89                 val result = fold (replay_one_inference ctxt' mode skolems) proof axioms
    90                 and used = map_filter (used_axioms axioms) proof
    91                 val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
    92                 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
    93                 val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
    94                   if have_common_thm used cls then NONE else SOME name)
    95             in
    96                 if not (null cls) andalso not (have_common_thm used cls) then
    97                   warning "Metis: The assumptions are inconsistent."
    98                 else
    99                   ();
   100                 if not (null unused) then
   101                   warning ("Metis: Unused theorems: " ^ commas_quote unused
   102                            ^ ".")
   103                 else
   104                   ();
   105                 case result of
   106                     (_,ith)::_ =>
   107                         (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
   108                          [ith])
   109                   | _ => (trace_msg (fn () => "Metis: No result"); [])
   110             end
   111         | Metis_Resolution.Satisfiable _ =>
   112             (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
   113              [])
   114   end;
   115 
   116 (* Extensionalize "th", because that makes sense and that's what Sledgehammer
   117    does, but also keep an unextensionalized version of "th" for backward
   118    compatibility. *)
   119 fun also_extensionalize_theorem th =
   120   let val th' = Meson_Clausifier.extensionalize_theorem th in
   121     if Thm.eq_thm (th, th') then [th]
   122     else th :: Meson.make_clauses_unsorted [th']
   123   end
   124 
   125 val neg_clausify =
   126   single
   127   #> Meson.make_clauses_unsorted
   128   #> maps also_extensionalize_theorem
   129   #> map Meson_Clausifier.introduce_combinators_in_theorem
   130   #> Meson.finish_cnf
   131 
   132 fun preskolem_tac ctxt st0 =
   133   (if exists (Meson.has_too_many_clauses ctxt)
   134              (Logic.prems_of_goal (prop_of st0) 1) then
   135      cnf.cnfx_rewrite_tac ctxt 1
   136    else
   137      all_tac) st0
   138 
   139 val type_has_top_sort =
   140   exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
   141 
   142 val preproc_ss =
   143   HOL_basic_ss addsimps @{thms all_simps[symmetric] ex_simps[symmetric]}
   144 
   145 fun generic_metis_tac mode ctxt ths i st0 =
   146   let
   147     val _ = trace_msg (fn () =>
   148         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   149   in
   150     if exists_type type_has_top_sort (prop_of st0) then
   151       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
   152     else
   153       Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
   154                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
   155                   ctxt i st0
   156   end
   157 
   158 val metis_tac = generic_metis_tac HO
   159 val metisF_tac = generic_metis_tac FO
   160 val metisFT_tac = generic_metis_tac FT
   161 
   162 (* Whenever "X" has schematic type variables, we treat "using X by metis" as
   163    "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
   164    We don't do it for nonschematic facts "X" because this breaks a few proofs
   165    (in the rare and subtle case where a proof relied on extensionality not being
   166    applied) and brings few benefits. *)
   167 val has_tvar =
   168   exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
   169 fun method name mode =
   170   Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
   171     METHOD (fn facts =>
   172                let
   173                  val (schem_facts, nonschem_facts) =
   174                    List.partition has_tvar facts
   175                in
   176                  HEADGOAL (Method.insert_tac nonschem_facts THEN'
   177                            CHANGED_PROP
   178                            o generic_metis_tac mode ctxt (schem_facts @ ths))
   179                end)))
   180 
   181 val setup =
   182   type_lits_setup
   183   #> method @{binding metis} HO "Metis for FOL/HOL problems"
   184   #> method @{binding metisF} FO "Metis for FOL problems"
   185   #> method @{binding metisFT} FT
   186             "Metis for FOL/HOL problems with fully-typed translation"
   187 
   188 end;