src/HOL/Tools/Metis/metis_tactic.ML
author blanchet
Tue Nov 15 22:13:39 2011 +0100 (2011-11-15)
changeset 45511 9b0f8ca4388e
parent 45508 b216dc1b3630
child 45512 a6cce8032fff
permissions -rw-r--r--
continued implementation of lambda-lifting in Metis
blanchet@44651
     1
(*  Title:      HOL/Tools/Metis/metis_tactic.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@44651
    10
signature METIS_TACTIC =
wenzelm@23442
    11
sig
blanchet@43050
    12
  val metisN : string
blanchet@43228
    13
  val full_typesN : string
blanchet@43228
    14
  val partial_typesN : string
blanchet@43228
    15
  val no_typesN : string
blanchet@43626
    16
  val really_full_type_enc : string
blanchet@43626
    17
  val full_type_enc : string
blanchet@43626
    18
  val partial_type_enc : string
blanchet@43626
    19
  val no_type_enc : string
blanchet@43303
    20
  val full_type_syss : string list
blanchet@43303
    21
  val partial_type_syss : string list
blanchet@39979
    22
  val trace : bool Config.T
blanchet@40665
    23
  val verbose : bool Config.T
blanchet@39891
    24
  val new_skolemizer : bool Config.T
blanchet@44934
    25
  val type_has_top_sort : typ -> bool
blanchet@43212
    26
  val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
blanchet@39497
    27
  val setup : theory -> theory
wenzelm@23442
    28
end
wenzelm@23442
    29
blanchet@44651
    30
structure Metis_Tactic : METIS_TACTIC =
wenzelm@23442
    31
struct
wenzelm@23442
    32
blanchet@43085
    33
open ATP_Translate
blanchet@39494
    34
open Metis_Translate
blanchet@39497
    35
open Metis_Reconstruct
blanchet@35826
    36
wenzelm@43545
    37
val metisN = "metis"
blanchet@43228
    38
blanchet@43205
    39
val full_typesN = "full_types"
blanchet@43228
    40
val partial_typesN = "partial_types"
blanchet@43228
    41
val no_typesN = "no_types"
blanchet@43050
    42
blanchet@44768
    43
val really_full_type_enc = "mono_tags"
blanchet@44768
    44
val full_type_enc = "poly_guards_query"
blanchet@43626
    45
val partial_type_enc = "poly_args"
blanchet@43626
    46
val no_type_enc = "erased"
blanchet@43228
    47
blanchet@43626
    48
val full_type_syss = [full_type_enc, really_full_type_enc]
blanchet@43626
    49
val partial_type_syss = partial_type_enc :: full_type_syss
blanchet@43211
    50
blanchet@43626
    51
val type_enc_aliases =
blanchet@43303
    52
  [(full_typesN, full_type_syss),
blanchet@43303
    53
   (partial_typesN, partial_type_syss),
blanchet@43626
    54
   (no_typesN, [no_type_enc])]
blanchet@43303
    55
blanchet@43626
    56
fun method_call_for_type_enc type_syss =
blanchet@43228
    57
  metisN ^ " (" ^
blanchet@43626
    58
  (case AList.find (op =) type_enc_aliases type_syss of
blanchet@43228
    59
     [alias] => alias
blanchet@43303
    60
   | _ => hd type_syss) ^ ")"
blanchet@43205
    61
blanchet@43089
    62
val new_skolemizer =
blanchet@43089
    63
  Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
wenzelm@23442
    64
blanchet@43134
    65
(* Designed to work also with monomorphic instances of polymorphic theorems. *)
blanchet@39497
    66
fun have_common_thm ths1 ths2 =
blanchet@43301
    67
  exists (member (Term.aconv_untyped o pairself prop_of) ths1)
blanchet@43134
    68
         (map Meson.make_meta_clause ths2)
wenzelm@23442
    69
wenzelm@32956
    70
(*Determining which axiom clauses are actually used*)
blanchet@39419
    71
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
blanchet@43128
    72
  | used_axioms _ _ = NONE
paulson@24855
    73
blanchet@43129
    74
(* Lightweight predicate type information comes in two flavors, "t = t'" and
blanchet@43129
    75
   "t => t'", where "t" and "t'" are the same term modulo type tags.
blanchet@43129
    76
   In Isabelle, type tags are stripped away, so we are left with "t = t" or
blanchet@43159
    77
   "t => t". Type tag idempotence is also handled this way. *)
blanchet@45508
    78
fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth =
blanchet@43136
    79
  let val thy = Proof_Context.theory_of ctxt in
blanchet@45508
    80
    case hol_clause_from_metis ctxt type_enc sym_tab concealed mth of
blanchet@43136
    81
      Const (@{const_name HOL.eq}, _) $ _ $ t =>
blanchet@44408
    82
      let
blanchet@44408
    83
        val ct = cterm_of thy t
blanchet@44408
    84
        val cT = ctyp_of_term ct
blanchet@44408
    85
      in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
blanchet@43136
    86
    | Const (@{const_name disj}, _) $ t1 $ t2 =>
blanchet@43136
    87
      (if can HOLogic.dest_not t1 then t2 else t1)
blanchet@43136
    88
      |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
blanchet@45511
    89
    | _ => raise Fail "expected reflexive or trivial clause"
blanchet@43136
    90
  end
blanchet@43129
    91
  |> Meson.make_meta_clause
blanchet@43129
    92
blanchet@45511
    93
fun lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth =
blanchet@45511
    94
  let
blanchet@45511
    95
    val thy = Proof_Context.theory_of ctxt
blanchet@45511
    96
    val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1
blanchet@45511
    97
    val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth
blanchet@45511
    98
    val ct = cterm_of thy (HOLogic.mk_Trueprop t)
blanchet@45511
    99
  in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
blanchet@45511
   100
blanchet@45511
   101
fun introduce_lambda_wrappers_in_theorem ctxt th =
blanchet@45511
   102
  if Meson_Clausify.is_quasi_lambda_free (prop_of th) then
blanchet@45511
   103
    th
blanchet@45511
   104
  else
blanchet@45511
   105
    let
blanchet@45511
   106
      fun conv wrap ctxt ct =
blanchet@45511
   107
        if Meson_Clausify.is_quasi_lambda_free (term_of ct) then
blanchet@45511
   108
          Thm.reflexive ct
blanchet@45511
   109
        else case term_of ct of
blanchet@45511
   110
          Abs _ =>
blanchet@45511
   111
          Conv.abs_conv (conv false o snd) ctxt ct
blanchet@45511
   112
          |> wrap ? (fn th => th RS @{thm Metis.eq_lambdaI})
blanchet@45511
   113
        | _ => Conv.comb_conv (conv true ctxt) ct
blanchet@45511
   114
      val eqth = conv true ctxt (cprop_of th)
blanchet@45511
   115
    in Thm.equal_elim eqth th end
blanchet@45511
   116
blanchet@44588
   117
val clause_params =
blanchet@39450
   118
  {ordering = Metis_KnuthBendixOrder.default,
blanchet@44492
   119
   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
blanchet@39450
   120
   orderTerms = true}
blanchet@44588
   121
val active_params =
blanchet@44588
   122
  {clause = clause_params,
blanchet@39450
   123
   prefactor = #prefactor Metis_Active.default,
blanchet@39450
   124
   postfactor = #postfactor Metis_Active.default}
blanchet@39450
   125
val waiting_params =
blanchet@39450
   126
  {symbolsWeight = 1.0,
blanchet@39450
   127
   variablesWeight = 0.0,
blanchet@39450
   128
   literalsWeight = 0.0,
blanchet@39450
   129
   models = []}
blanchet@44588
   130
val resolution_params = {active = active_params, waiting = waiting_params}
blanchet@37573
   131
blanchet@37516
   132
(* Main function to start Metis proof and reconstruction *)
blanchet@45508
   133
fun FOL_SOLVE (type_enc :: fallback_type_syss) lambda_trans ctxt cls ths0 =
wenzelm@42361
   134
  let val thy = Proof_Context.theory_of ctxt
blanchet@39901
   135
      val new_skolemizer =
blanchet@39950
   136
        Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
blanchet@35826
   137
      val th_cls_pairs =
blanchet@39894
   138
        map2 (fn j => fn th =>
blanchet@39894
   139
                (Thm.get_name_hint th,
blanchet@45508
   140
                 Meson_Clausify.cnf_axiom ctxt new_skolemizer
blanchet@45508
   141
                                          (lambda_trans = combinatorsN) j th))
blanchet@39894
   142
             (0 upto length ths0 - 1) ths0
blanchet@43092
   143
      val ths = maps (snd o snd) th_cls_pairs
blanchet@39938
   144
      val dischargers = map (fst o snd) th_cls_pairs
blanchet@39978
   145
      val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
blanchet@39978
   146
      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
blanchet@44411
   147
      val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
blanchet@44634
   148
      val type_enc = type_enc_from_string Sound type_enc
blanchet@45508
   149
      val (sym_tab, axioms, concealed) =
blanchet@45508
   150
        prepare_metis_problem ctxt type_enc lambda_trans cls ths
blanchet@43159
   151
      fun get_isa_thm mth Isa_Reflexive_or_Trivial =
blanchet@45508
   152
          reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
blanchet@45511
   153
        | get_isa_thm mth Isa_Lambda_Lifted =
blanchet@45511
   154
          lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth
blanchet@45511
   155
        | get_isa_thm _ (Isa_Raw ith) =
blanchet@45511
   156
          ith |> lambda_trans = liftingN
blanchet@45511
   157
                 ? introduce_lambda_wrappers_in_theorem ctxt
blanchet@43159
   158
      val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
blanchet@45042
   159
      val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
blanchet@45042
   160
      val _ = app (fn (_, th) => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) axioms
blanchet@39978
   161
      val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
blanchet@43159
   162
      val thms = axioms |> map fst
blanchet@39978
   163
      val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
blanchet@39978
   164
      val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
wenzelm@32956
   165
  in
blanchet@43159
   166
      case filter (fn t => prop_of t aconv @{prop False}) cls of
blanchet@43159
   167
          false_th :: _ => [false_th RS @{thm FalseE}]
wenzelm@32956
   168
        | [] =>
blanchet@44588
   169
      case Metis_Resolution.new resolution_params
blanchet@44411
   170
                                {axioms = thms, conjecture = []}
blanchet@39497
   171
           |> Metis_Resolution.loop of
blanchet@39419
   172
          Metis_Resolution.Contradiction mth =>
blanchet@39978
   173
            let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
blanchet@39419
   174
                          Metis_Thm.toString mth)
wenzelm@32956
   175
                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
wenzelm@32956
   176
                             (*add constraints arising from converting goal to clause form*)
blanchet@39419
   177
                val proof = Metis_Proof.proof mth
blanchet@43094
   178
                val result =
blanchet@43212
   179
                  axioms
blanchet@45508
   180
                  |> fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof
blanchet@43134
   181
                val used = map_filter (used_axioms axioms) proof
blanchet@39978
   182
                val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
blanchet@39978
   183
                val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
blanchet@43134
   184
                val names = th_cls_pairs |> map fst
blanchet@43134
   185
                val used_names =
blanchet@43134
   186
                  th_cls_pairs
blanchet@43134
   187
                  |> map_filter (fn (name, (_, cls)) =>
blanchet@43134
   188
                                    if have_common_thm used cls then SOME name
blanchet@43134
   189
                                    else NONE)
blanchet@43134
   190
                val unused_names = names |> subtract (op =) used_names
wenzelm@32956
   191
            in
blanchet@39497
   192
                if not (null cls) andalso not (have_common_thm used cls) then
blanchet@42650
   193
                  verbose_warning ctxt "The assumptions are inconsistent"
blanchet@36383
   194
                else
blanchet@36383
   195
                  ();
blanchet@43134
   196
                if not (null unused_names) then
blanchet@43134
   197
                  "Unused theorems: " ^ commas_quote unused_names
blanchet@43134
   198
                  |> verbose_warning ctxt
blanchet@36230
   199
                else
blanchet@36230
   200
                  ();
wenzelm@32956
   201
                case result of
wenzelm@32956
   202
                    (_,ith)::_ =>
blanchet@39978
   203
                        (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
blanchet@39887
   204
                         [discharge_skolem_premises ctxt dischargers ith])
blanchet@39978
   205
                  | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
wenzelm@32956
   206
            end
blanchet@39419
   207
        | Metis_Resolution.Satisfiable _ =>
blanchet@39978
   208
            (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
blanchet@43212
   209
             if null fallback_type_syss then
blanchet@43034
   210
               ()
blanchet@43034
   211
             else
blanchet@42650
   212
               raise METIS ("FOL_SOLVE",
blanchet@43034
   213
                            "No first-order proof with the lemmas supplied");
blanchet@38097
   214
             [])
blanchet@42733
   215
  end
blanchet@42733
   216
  handle METIS (loc, msg) =>
blanchet@43212
   217
         case fallback_type_syss of
blanchet@43034
   218
           [] => error ("Failed to replay Metis proof in Isabelle." ^
blanchet@43034
   219
                        (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
blanchet@43034
   220
                         else ""))
blanchet@43303
   221
         | _ =>
blanchet@43228
   222
           (verbose_warning ctxt
blanchet@43228
   223
                ("Falling back on " ^
blanchet@43626
   224
                 quote (method_call_for_type_enc fallback_type_syss) ^ "...");
blanchet@45508
   225
            FOL_SOLVE fallback_type_syss lambda_trans ctxt cls ths0)
wenzelm@23442
   226
blanchet@45508
   227
fun neg_clausify ctxt combinators =
blanchet@38028
   228
  single
blanchet@43964
   229
  #> Meson.make_clauses_unsorted ctxt
blanchet@45508
   230
  #> combinators ? map Meson_Clausify.introduce_combinators_in_theorem
blanchet@38028
   231
  #> Meson.finish_cnf
blanchet@38028
   232
blanchet@39269
   233
fun preskolem_tac ctxt st0 =
blanchet@39269
   234
  (if exists (Meson.has_too_many_clauses ctxt)
blanchet@39269
   235
             (Logic.prems_of_goal (prop_of st0) 1) then
blanchet@42336
   236
     Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
blanchet@42336
   237
     THEN cnf.cnfx_rewrite_tac ctxt 1
blanchet@39269
   238
   else
blanchet@39269
   239
     all_tac) st0
blanchet@39269
   240
blanchet@38652
   241
val type_has_top_sort =
blanchet@38652
   242
  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
blanchet@38652
   243
blanchet@43212
   244
fun generic_metis_tac type_syss ctxt ths i st0 =
blanchet@37926
   245
  let
blanchet@45508
   246
    val lambda_trans = Config.get ctxt lambda_translation
blanchet@39978
   247
    val _ = trace_msg ctxt (fn () =>
blanchet@43194
   248
        "Metis called with theorems\n" ^
blanchet@43034
   249
        cat_lines (map (Display.string_of_thm ctxt) ths))
blanchet@45508
   250
    fun tac clause =
blanchet@45508
   251
      resolve_tac (FOL_SOLVE type_syss lambda_trans ctxt clause ths) 1
wenzelm@32956
   252
  in
blanchet@37626
   253
    if exists_type type_has_top_sort (prop_of st0) then
blanchet@43299
   254
      verbose_warning ctxt "Proof state contains the universal sort {}"
wenzelm@35568
   255
    else
blanchet@43299
   256
      ();
blanchet@45508
   257
    Meson.MESON (preskolem_tac ctxt)
blanchet@45508
   258
        (maps (neg_clausify ctxt (lambda_trans = combinatorsN))) tac ctxt i st0
wenzelm@32956
   259
  end
wenzelm@23442
   260
blanchet@43303
   261
fun metis_tac [] = generic_metis_tac partial_type_syss
blanchet@43212
   262
  | metis_tac type_syss = generic_metis_tac type_syss
wenzelm@23442
   263
blanchet@38632
   264
(* Whenever "X" has schematic type variables, we treat "using X by metis" as
blanchet@43100
   265
   "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
blanchet@38632
   266
   We don't do it for nonschematic facts "X" because this breaks a few proofs
blanchet@38632
   267
   (in the rare and subtle case where a proof relied on extensionality not being
blanchet@38994
   268
   applied) and brings few benefits. *)
blanchet@38632
   269
val has_tvar =
blanchet@38632
   270
  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
blanchet@43034
   271
blanchet@43303
   272
fun method default_type_syss (override_type_syss, ths) ctxt facts =
blanchet@43100
   273
  let
blanchet@43228
   274
    val _ =
blanchet@43303
   275
      if default_type_syss = full_type_syss then
wenzelm@44052
   276
        legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead"
blanchet@43228
   277
      else
blanchet@43228
   278
        ()
blanchet@43100
   279
    val (schem_facts, nonschem_facts) = List.partition has_tvar facts
blanchet@43303
   280
    val type_syss = override_type_syss |> the_default default_type_syss
blanchet@43100
   281
  in
blanchet@43099
   282
    HEADGOAL (Method.insert_tac nonschem_facts THEN'
blanchet@43212
   283
              CHANGED_PROP
blanchet@43212
   284
              o generic_metis_tac type_syss ctxt (schem_facts @ ths))
blanchet@43099
   285
  end
blanchet@43100
   286
blanchet@43235
   287
fun setup_method (binding, type_syss) =
blanchet@43303
   288
  ((Args.parens (Scan.repeat Parse.short_ident)
blanchet@43963
   289
    >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s]))
blanchet@43303
   290
    |> Scan.option |> Scan.lift)
blanchet@43212
   291
  -- Attrib.thms >> (METHOD oo method type_syss)
blanchet@43228
   292
  |> Method.setup binding
wenzelm@23442
   293
wenzelm@32956
   294
val setup =
blanchet@43303
   295
  [((@{binding metis}, partial_type_syss),
blanchet@43228
   296
    "Metis for FOL and HOL problems"),
blanchet@43303
   297
   ((@{binding metisFT}, full_type_syss),
blanchet@43212
   298
    "Metis for FOL/HOL problems with fully-typed translation")]
blanchet@43034
   299
  |> fold (uncurry setup_method)
wenzelm@23442
   300
wenzelm@23442
   301
end;