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