src/HOL/Tools/Metis/metis_tactics.ML
author blanchet
Thu May 12 15:29:19 2011 +0200 (2011-05-12)
changeset 42739 017e5dac8642
parent 42733 01ef1c3d9cfd
child 42747 f132d13fcf75
permissions -rw-r--r--
added unfold set constant functionality to Meson/Metis -- disabled by default for now
     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 "The assumptions are inconsistent"
   105                 else
   106                   ();
   107                 if not (null unused) then
   108                   verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused)
   109                 else
   110                   ();
   111                 case result of
   112                     (_,ith)::_ =>
   113                         (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
   114                          [discharge_skolem_premises ctxt dischargers ith])
   115                   | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
   116             end
   117         | Metis_Resolution.Satisfiable _ =>
   118             (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
   119              if mode <> FT then
   120                raise METIS ("FOL_SOLVE",
   121                             "No first-order proof with the lemmas supplied")
   122              else
   123                ();
   124              [])
   125   end
   126   handle METIS (loc, msg) =>
   127          if mode <> FT then
   128            (verbose_warning ctxt ("Falling back on \"metisFT\".");
   129             FOL_SOLVE FT ctxt cls ths0)
   130          else
   131            error ("Failed to replay Metis proof in Isabelle." ^
   132                   (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
   133                    else ""))
   134 
   135 (* Extensionalize "th", because that makes sense and that's what Sledgehammer
   136    does, but also keep an unextensionalized version of "th" for backward
   137    compatibility. *)
   138 fun also_extensionalize_theorem th =
   139   let val th' = Meson_Clausify.extensionalize_theorem th in
   140     if Thm.eq_thm (th, th') then [th]
   141     else th :: Meson.make_clauses_unsorted [th']
   142   end
   143 
   144 fun neg_clausify ctxt =
   145   single
   146   #> Meson.make_clauses_unsorted
   147   #> maps (Raw_Simplifier.rewrite_rule (Meson.unfold_set_const_simps ctxt)
   148            #> also_extensionalize_theorem)
   149   #> map Meson_Clausify.introduce_combinators_in_theorem
   150   #> Meson.finish_cnf
   151 
   152 fun preskolem_tac ctxt st0 =
   153   (if exists (Meson.has_too_many_clauses ctxt)
   154              (Logic.prems_of_goal (prop_of st0) 1) then
   155      Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
   156      THEN cnf.cnfx_rewrite_tac ctxt 1
   157    else
   158      all_tac) st0
   159 
   160 val type_has_top_sort =
   161   exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
   162 
   163 fun generic_metis_tac mode ctxt ths i st0 =
   164   let
   165     val _ = trace_msg ctxt (fn () =>
   166         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   167   in
   168     if exists_type type_has_top_sort (prop_of st0) then
   169       (verbose_warning ctxt "Proof state contains the universal sort {}";
   170        Seq.empty)
   171     else
   172       Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt))
   173                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
   174                   ctxt i st0
   175   end
   176 
   177 val metis_tac = generic_metis_tac HO
   178 val metisF_tac = generic_metis_tac FO
   179 val metisFT_tac = generic_metis_tac FT
   180 
   181 (* Whenever "X" has schematic type variables, we treat "using X by metis" as
   182    "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
   183    We don't do it for nonschematic facts "X" because this breaks a few proofs
   184    (in the rare and subtle case where a proof relied on extensionality not being
   185    applied) and brings few benefits. *)
   186 val has_tvar =
   187   exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
   188 fun method name mode =
   189   Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
   190     METHOD (fn facts =>
   191                let
   192                  val (schem_facts, nonschem_facts) =
   193                    List.partition has_tvar facts
   194                in
   195                  HEADGOAL (Method.insert_tac nonschem_facts THEN'
   196                            CHANGED_PROP
   197                            o generic_metis_tac mode ctxt (schem_facts @ ths))
   198                end)))
   199 
   200 val setup =
   201   method @{binding metis} HO "Metis for FOL/HOL problems"
   202   #> method @{binding metisF} FO "Metis for FOL problems"
   203   #> method @{binding metisFT} FT
   204             "Metis for FOL/HOL problems with fully-typed translation"
   205 
   206 end;