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