src/HOL/Tools/Metis/metis_tactic.ML
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59632 5980e75a204e
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
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@39979
    12
  val trace : bool Config.T
blanchet@40665
    13
  val verbose : bool Config.T
blanchet@50705
    14
  val new_skolem : bool Config.T
blanchet@47039
    15
  val advisory_simp : bool Config.T
blanchet@55521
    16
  val metis_tac_unused : string list -> string -> Proof.context -> thm list -> int -> thm ->
blanchet@55521
    17
    thm list * thm Seq.seq
blanchet@54756
    18
  val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic
blanchet@45521
    19
  val metis_lam_transs : string list
blanchet@45519
    20
  val parse_metis_options : (string list option * string option) parser
wenzelm@23442
    21
end
wenzelm@23442
    22
blanchet@44651
    23
structure Metis_Tactic : METIS_TACTIC =
wenzelm@23442
    24
struct
wenzelm@23442
    25
blanchet@46320
    26
open ATP_Problem_Generate
blanchet@46320
    27
open ATP_Proof_Reconstruct
blanchet@46320
    28
open Metis_Generate
blanchet@39497
    29
open Metis_Reconstruct
blanchet@35826
    30
blanchet@54756
    31
val new_skolem = Attrib.setup_config_bool @{binding metis_new_skolem} (K false)
blanchet@54756
    32
val advisory_simp = Attrib.setup_config_bool @{binding metis_advisory_simp} (K true)
wenzelm@23442
    33
blanchet@43134
    34
(* Designed to work also with monomorphic instances of polymorphic theorems. *)
blanchet@39497
    35
fun have_common_thm ths1 ths2 =
wenzelm@59582
    36
  exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1) (map Meson.make_meta_clause ths2)
wenzelm@23442
    37
wenzelm@32956
    38
(*Determining which axiom clauses are actually used*)
blanchet@39419
    39
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
blanchet@43128
    40
  | used_axioms _ _ = NONE
paulson@24855
    41
blanchet@43129
    42
(* Lightweight predicate type information comes in two flavors, "t = t'" and
blanchet@43129
    43
   "t => t'", where "t" and "t'" are the same term modulo type tags.
blanchet@43129
    44
   In Isabelle, type tags are stripped away, so we are left with "t = t" or
blanchet@43159
    45
   "t => t". Type tag idempotence is also handled this way. *)
blanchet@52031
    46
fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth =
blanchet@43136
    47
  let val thy = Proof_Context.theory_of ctxt in
blanchet@57408
    48
    (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
blanchet@43136
    49
      Const (@{const_name HOL.eq}, _) $ _ $ t =>
blanchet@44408
    50
      let
wenzelm@59621
    51
        val ct = Thm.global_cterm_of thy t
wenzelm@59586
    52
        val cT = Thm.ctyp_of_cterm ct
blanchet@44408
    53
      in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
blanchet@43136
    54
    | Const (@{const_name disj}, _) $ t1 $ t2 =>
blanchet@43136
    55
      (if can HOLogic.dest_not t1 then t2 else t1)
wenzelm@59621
    56
      |> HOLogic.mk_Trueprop |> Thm.global_cterm_of thy |> Thm.trivial
blanchet@57408
    57
    | _ => raise Fail "expected reflexive or trivial clause")
blanchet@43136
    58
  end
blanchet@43129
    59
  |> Meson.make_meta_clause
blanchet@43129
    60
blanchet@52031
    61
fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
blanchet@45511
    62
  let
blanchet@45511
    63
    val thy = Proof_Context.theory_of ctxt
wenzelm@59498
    64
    val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac ctxt [refl] 1
blanchet@52031
    65
    val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
wenzelm@59621
    66
    val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t)
wenzelm@54883
    67
  in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end
blanchet@45511
    68
blanchet@45570
    69
fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
blanchet@45570
    70
  | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t
blanchet@45570
    71
  | add_vars_and_frees (t as Var _) = insert (op =) t
blanchet@45570
    72
  | add_vars_and_frees (t as Free _) = insert (op =) t
blanchet@45570
    73
  | add_vars_and_frees _ = I
blanchet@45570
    74
blanchet@45569
    75
fun introduce_lam_wrappers ctxt th =
wenzelm@59582
    76
  if Meson_Clausify.is_quasi_lambda_free (Thm.prop_of th) then
blanchet@45511
    77
    th
blanchet@45511
    78
  else
blanchet@45511
    79
    let
blanchet@45570
    80
      val thy = Proof_Context.theory_of ctxt
blanchet@45570
    81
      fun conv first ctxt ct =
wenzelm@59582
    82
        if Meson_Clausify.is_quasi_lambda_free (Thm.term_of ct) then
blanchet@45511
    83
          Thm.reflexive ct
blanchet@57408
    84
        else
wenzelm@59582
    85
          (case Thm.term_of ct of
blanchet@57408
    86
            Abs (_, _, u) =>
blanchet@57408
    87
            if first then
blanchet@57408
    88
              (case add_vars_and_frees u [] of
blanchet@57408
    89
                [] =>
blanchet@57408
    90
                Conv.abs_conv (conv false o snd) ctxt ct
blanchet@57408
    91
                |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
blanchet@57408
    92
              | v :: _ =>
wenzelm@59582
    93
                Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v
wenzelm@59621
    94
                |> Thm.global_cterm_of thy
blanchet@57408
    95
                |> Conv.comb_conv (conv true ctxt))
blanchet@57408
    96
            else
blanchet@45570
    97
              Conv.abs_conv (conv false o snd) ctxt ct
blanchet@57408
    98
          | Const (@{const_name Meson.skolem}, _) $ _ => Thm.reflexive ct
blanchet@57408
    99
          | _ => Conv.comb_conv (conv true ctxt) ct)
wenzelm@59582
   100
      val eq_th = conv true ctxt (Thm.cprop_of th)
blanchet@45570
   101
      (* We replace the equation's left-hand side with a beta-equivalent term
blanchet@45570
   102
         so that "Thm.equal_elim" works below. *)
wenzelm@59582
   103
      val t0 $ _ $ t2 = Thm.prop_of eq_th
wenzelm@59621
   104
      val eq_ct = t0 $ Thm.prop_of th $ t2 |> Thm.global_cterm_of thy
wenzelm@59498
   105
      val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (resolve_tac ctxt [eq_th] 1))
blanchet@45570
   106
    in Thm.equal_elim eq_th' th end
blanchet@45511
   107
blanchet@47039
   108
fun clause_params ordering =
blanchet@47039
   109
  {ordering = ordering,
blanchet@44492
   110
   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
blanchet@39450
   111
   orderTerms = true}
blanchet@47039
   112
fun active_params ordering =
blanchet@47039
   113
  {clause = clause_params ordering,
blanchet@39450
   114
   prefactor = #prefactor Metis_Active.default,
blanchet@39450
   115
   postfactor = #postfactor Metis_Active.default}
blanchet@39450
   116
val waiting_params =
blanchet@39450
   117
  {symbolsWeight = 1.0,
blanchet@47047
   118
   variablesWeight = 0.05,
blanchet@47047
   119
   literalsWeight = 0.01,
blanchet@39450
   120
   models = []}
blanchet@47039
   121
fun resolution_params ordering =
blanchet@47039
   122
  {active = active_params ordering, waiting = waiting_params}
blanchet@47039
   123
blanchet@47039
   124
fun kbo_advisory_simp_ordering ord_info =
blanchet@47039
   125
  let
blanchet@47039
   126
    fun weight (m, _) =
blanchet@47039
   127
      AList.lookup (op =) ord_info (Metis_Name.toString m) |> the_default 1
blanchet@47039
   128
    fun precedence p =
wenzelm@59058
   129
      (case int_ord (apply2 weight p) of
blanchet@47039
   130
        EQUAL => #precedence Metis_KnuthBendixOrder.default p
blanchet@57408
   131
      | ord => ord)
blanchet@47039
   132
  in {weight = weight, precedence = precedence} end
blanchet@37573
   133
blanchet@55285
   134
fun metis_call type_enc lam_trans =
blanchet@55285
   135
  let
blanchet@55285
   136
    val type_enc =
blanchet@55285
   137
      (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
blanchet@55285
   138
        [alias] => alias
blanchet@55285
   139
      | _ => type_enc)
blanchet@55285
   140
    val opts =
blanchet@55285
   141
      [] |> type_enc <> partial_typesN ? cons type_enc
blanchet@55285
   142
         |> lam_trans <> default_metis_lam_trans ? cons lam_trans
blanchet@55285
   143
  in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
blanchet@55285
   144
blanchet@50875
   145
exception METIS_UNPROVABLE of unit
blanchet@50875
   146
blanchet@37516
   147
(* Main function to start Metis proof and reconstruction *)
blanchet@55521
   148
fun FOL_SOLVE unused (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
wenzelm@42361
   149
  let val thy = Proof_Context.theory_of ctxt
blanchet@50705
   150
      val new_skolem =
blanchet@50705
   151
        Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy)
blanchet@46365
   152
      val do_lams =
blanchet@46365
   153
        (lam_trans = liftingN orelse lam_trans = lam_liftingN)
blanchet@46365
   154
        ? introduce_lam_wrappers ctxt
blanchet@35826
   155
      val th_cls_pairs =
blanchet@39894
   156
        map2 (fn j => fn th =>
blanchet@39894
   157
                (Thm.get_name_hint th,
blanchet@45570
   158
                 th |> Drule.eta_contraction_rule
blanchet@57263
   159
                    |> Meson_Clausify.cnf_axiom ctxt new_skolem (lam_trans = combsN) j
blanchet@45570
   160
                    ||> map do_lams))
blanchet@39894
   161
             (0 upto length ths0 - 1) ths0
blanchet@43092
   162
      val ths = maps (snd o snd) th_cls_pairs
blanchet@39938
   163
      val dischargers = map (fst o snd) th_cls_pairs
blanchet@45570
   164
      val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
blanchet@55521
   165
      val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES")
blanchet@39978
   166
      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
blanchet@44411
   167
      val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
blanchet@52031
   168
      val type_enc = type_enc_of_string Strict type_enc
blanchet@47039
   169
      val (sym_tab, axioms, ord_info, concealed) =
blanchet@57263
   170
        generate_metis_problem ctxt type_enc lam_trans cls ths
blanchet@43159
   171
      fun get_isa_thm mth Isa_Reflexive_or_Trivial =
blanchet@52031
   172
          reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth
blanchet@45511
   173
        | get_isa_thm mth Isa_Lambda_Lifted =
blanchet@52031
   174
          lam_lifted_of_metis ctxt type_enc sym_tab concealed mth
blanchet@45569
   175
        | get_isa_thm _ (Isa_Raw ith) = ith
blanchet@45569
   176
      val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
blanchet@55521
   177
      val _ = trace_msg ctxt (K "ISABELLE CLAUSES")
blanchet@45559
   178
      val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms
blanchet@55521
   179
      val _ = trace_msg ctxt (K "METIS CLAUSES")
blanchet@45559
   180
      val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
blanchet@55521
   181
      val _ = trace_msg ctxt (K "START METIS PROVE PROCESS")
blanchet@47039
   182
      val ordering =
blanchet@47039
   183
        if Config.get ctxt advisory_simp then
blanchet@47039
   184
          kbo_advisory_simp_ordering (ord_info ())
blanchet@47039
   185
        else
blanchet@47039
   186
          Metis_KnuthBendixOrder.default
blanchet@50875
   187
    fun fall_back () =
blanchet@50875
   188
      (verbose_warning ctxt
blanchet@55257
   189
           ("Falling back on " ^ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "...");
blanchet@55521
   190
       FOL_SOLVE unused fallback_type_encs lam_trans ctxt cls ths0)
wenzelm@32956
   191
  in
wenzelm@59582
   192
    (case filter (fn t => Thm.prop_of t aconv @{prop False}) cls of
blanchet@55521
   193
       false_th :: _ => [false_th RS @{thm FalseE}]
blanchet@55521
   194
     | [] =>
blanchet@55521
   195
     (case Metis_Resolution.loop (Metis_Resolution.new (resolution_params ordering)
blanchet@55521
   196
         {axioms = axioms |> map fst, conjecture = []}) of
blanchet@55521
   197
       Metis_Resolution.Contradiction mth =>
blanchet@55521
   198
       let
blanchet@55521
   199
         val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ Metis_Thm.toString mth)
wenzelm@59582
   200
         val ctxt' = fold Variable.declare_constraints (map Thm.prop_of cls) ctxt
blanchet@55521
   201
                      (*add constraints arising from converting goal to clause form*)
blanchet@55521
   202
         val proof = Metis_Proof.proof mth
blanchet@55521
   203
         val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms
blanchet@55521
   204
         val used = map_filter (used_axioms axioms) proof
blanchet@55521
   205
         val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
blanchet@55521
   206
         val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
blanchet@55521
   207
         val (used_th_cls_pairs, unused_th_cls_pairs) =
blanchet@55521
   208
           List.partition (have_common_thm used o snd o snd) th_cls_pairs
blanchet@55521
   209
         val unused_ths = maps (snd o snd) unused_th_cls_pairs
blanchet@55521
   210
         val unused_names = map fst unused_th_cls_pairs
blanchet@55521
   211
       in
blanchet@55521
   212
         unused := unused_ths;
blanchet@55521
   213
         if not (null unused_names) then
blanchet@55521
   214
           verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused_names)
blanchet@55521
   215
         else
blanchet@55521
   216
           ();
blanchet@55521
   217
         if not (null cls) andalso not (have_common_thm used cls) then
blanchet@55521
   218
           verbose_warning ctxt "The assumptions are inconsistent"
blanchet@55521
   219
         else
blanchet@55521
   220
           ();
blanchet@55521
   221
         (case result of
blanchet@55521
   222
           (_, ith) :: _ =>
blanchet@55521
   223
           (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
blanchet@55521
   224
            [discharge_skolem_premises ctxt dischargers ith])
blanchet@55521
   225
         | _ => (trace_msg ctxt (K "Metis: No result"); []))
blanchet@55521
   226
       end
blanchet@55521
   227
     | Metis_Resolution.Satisfiable _ =>
blanchet@55521
   228
       (trace_msg ctxt (K "Metis: No first-order proof with the supplied lemmas");
blanchet@55521
   229
        raise METIS_UNPROVABLE ()))
blanchet@55521
   230
    handle METIS_UNPROVABLE () => if null fallback_type_encs then [] else fall_back ()
blanchet@50875
   231
         | METIS_RECONSTRUCT (loc, msg) =>
blanchet@55521
   232
           if null fallback_type_encs then
blanchet@55521
   233
             (verbose_warning ctxt ("Failed to replay Metis proof\n" ^ loc ^ ": " ^ msg); [])
blanchet@55521
   234
           else
blanchet@55521
   235
             fall_back ())
blanchet@42733
   236
  end
wenzelm@23442
   237
blanchet@45508
   238
fun neg_clausify ctxt combinators =
blanchet@38028
   239
  single
blanchet@43964
   240
  #> Meson.make_clauses_unsorted ctxt
wenzelm@55236
   241
  #> combinators ? map (Meson_Clausify.introduce_combinators_in_theorem ctxt)
blanchet@38028
   242
  #> Meson.finish_cnf
blanchet@38028
   243
blanchet@39269
   244
fun preskolem_tac ctxt st0 =
blanchet@39269
   245
  (if exists (Meson.has_too_many_clauses ctxt)
wenzelm@59582
   246
             (Logic.prems_of_goal (Thm.prop_of st0) 1) then
wenzelm@51717
   247
     Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex} ctxt) 1
wenzelm@55239
   248
     THEN CNF.cnfx_rewrite_tac ctxt 1
blanchet@39269
   249
   else
blanchet@39269
   250
     all_tac) st0
blanchet@39269
   251
blanchet@55521
   252
fun metis_tac_unused type_encs0 lam_trans ctxt ths i st0 =
blanchet@37926
   253
  let
blanchet@55521
   254
    val unused = Unsynchronized.ref []
blanchet@55520
   255
    val type_encs = if null type_encs0 then partial_type_encs else type_encs0
blanchet@39978
   256
    val _ = trace_msg ctxt (fn () =>
blanchet@55315
   257
      "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths))
blanchet@45519
   258
    val type_encs = type_encs |> maps unalias_type_enc
blanchet@55521
   259
    val combs = (lam_trans = combsN)
wenzelm@59498
   260
    fun tac clause = resolve_tac ctxt (FOL_SOLVE unused type_encs lam_trans ctxt clause ths) 1
blanchet@55521
   261
    val seq = Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt combs)) tac ctxt i st0
wenzelm@32956
   262
  in
blanchet@55521
   263
    (!unused, seq)
wenzelm@32956
   264
  end
wenzelm@23442
   265
blanchet@55521
   266
fun metis_tac type_encs lam_trans ctxt ths i = snd o metis_tac_unused type_encs lam_trans ctxt ths i
blanchet@55521
   267
blanchet@55520
   268
(* Whenever "X" has schematic type variables, we treat "using X by metis" as "by (metis X)" to
blanchet@55520
   269
   prevent "Subgoal.FOCUS" from freezing the type variables. We don't do it for nonschematic facts
blanchet@55520
   270
   "X" because this breaks a few proofs (in the rare and subtle case where a proof relied on
blanchet@55520
   271
   extensionality not being applied) and brings few benefits. *)
wenzelm@59582
   272
val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o Thm.prop_of
blanchet@43034
   273
blanchet@55315
   274
fun metis_method ((override_type_encs, lam_trans), ths) ctxt facts =
blanchet@55520
   275
  let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in
blanchet@43099
   276
    HEADGOAL (Method.insert_tac nonschem_facts THEN'
blanchet@55520
   277
      CHANGED_PROP o metis_tac (these override_type_encs)
blanchet@55520
   278
        (the_default default_metis_lam_trans lam_trans) ctxt (schem_facts @ ths))
blanchet@43099
   279
  end
blanchet@43100
   280
blanchet@46365
   281
val metis_lam_transs = [hide_lamsN, liftingN, combsN]
blanchet@45519
   282
blanchet@45578
   283
fun set_opt _ x NONE = SOME x
blanchet@45578
   284
  | set_opt get x (SOME x0) =
blanchet@55523
   285
    error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x))
blanchet@54756
   286
blanchet@45519
   287
fun consider_opt s =
blanchet@54756
   288
  if member (op =) metis_lam_transs s then apsnd (set_opt I s) else apfst (set_opt hd [s])
blanchet@45514
   289
blanchet@45519
   290
val parse_metis_options =
blanchet@45519
   291
  Scan.optional
wenzelm@58831
   292
      (Args.parens (Args.name -- Scan.option (@{keyword ","} |-- Args.name))
blanchet@45519
   293
       >> (fn (s, s') =>
blanchet@45519
   294
              (NONE, NONE) |> consider_opt s
blanchet@45519
   295
                           |> (case s' of SOME s' => consider_opt s' | _ => I)))
blanchet@45519
   296
      (NONE, NONE)
blanchet@45519
   297
wenzelm@58818
   298
val _ =
wenzelm@58818
   299
  Theory.setup
wenzelm@58818
   300
    (Method.setup @{binding metis}
wenzelm@58818
   301
      (Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo metis_method))
wenzelm@58818
   302
      "Metis for FOL and HOL problems")
wenzelm@23442
   303
wenzelm@23442
   304
end;