src/HOL/Tools/Sledgehammer/metis_tactics.ML
author blanchet
Wed Sep 29 23:55:14 2010 +0200 (2010-09-29)
changeset 39891 8e12f1956fcd
parent 39890 a1695e2169d0
child 39892 699a20afc5bd
permissions -rw-r--r--
"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
blanchet@35826
     1
(*  Title:      HOL/Tools/Sledgehammer/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@39497
    12
  val trace : bool Unsynchronized.ref
blanchet@39497
    13
  val type_lits : bool Config.T
blanchet@39891
    14
  val new_skolemizer : bool Config.T
blanchet@39497
    15
  val metis_tac : Proof.context -> thm list -> int -> tactic
blanchet@39497
    16
  val metisF_tac : Proof.context -> thm list -> int -> tactic
blanchet@39497
    17
  val metisFT_tac : Proof.context -> thm list -> int -> tactic
blanchet@39497
    18
  val setup : theory -> theory
wenzelm@23442
    19
end
wenzelm@23442
    20
blanchet@35826
    21
structure Metis_Tactics : METIS_TACTICS =
wenzelm@23442
    22
struct
wenzelm@23442
    23
blanchet@39494
    24
open Metis_Translate
blanchet@39497
    25
open Metis_Reconstruct
blanchet@35826
    26
blanchet@39497
    27
fun trace_msg msg = if !trace then tracing (msg ()) else ()
wenzelm@32955
    28
blanchet@39891
    29
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
blanchet@39891
    30
val (new_skolemizer, new_skolemizer_setup) =
blanchet@39891
    31
  Attrib.config_bool "metis_new_skolemizer" (K false)
wenzelm@23442
    32
blanchet@39497
    33
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
wenzelm@23442
    34
blanchet@39497
    35
fun have_common_thm ths1 ths2 =
blanchet@39497
    36
  exists (member Thm.eq_thm 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)
wenzelm@32994
    40
  | used_axioms _ _ = NONE;
paulson@24855
    41
blanchet@39450
    42
val clause_params =
blanchet@39450
    43
  {ordering = Metis_KnuthBendixOrder.default,
blanchet@39450
    44
   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
blanchet@39450
    45
   orderTerms = true}
blanchet@39450
    46
val active_params =
blanchet@39450
    47
  {clause = clause_params,
blanchet@39450
    48
   prefactor = #prefactor Metis_Active.default,
blanchet@39450
    49
   postfactor = #postfactor Metis_Active.default}
blanchet@39450
    50
val waiting_params =
blanchet@39450
    51
  {symbolsWeight = 1.0,
blanchet@39450
    52
   variablesWeight = 0.0,
blanchet@39450
    53
   literalsWeight = 0.0,
blanchet@39450
    54
   models = []}
blanchet@39497
    55
val resolution_params = {active = active_params, waiting = waiting_params}
blanchet@37573
    56
blanchet@39887
    57
(* In principle, it should be sufficient to apply "assume_tac" to unify the
blanchet@39887
    58
   conclusion with one of the premises. However, in practice, this fails
blanchet@39887
    59
   horribly because of the mildly higher-order nature of the unification
blanchet@39887
    60
   problems. Typical constraints are of the form "?x a b =?= b", where "a" and
blanchet@39887
    61
   "b" are goal parameters. *)
blanchet@39887
    62
fun unify_one_prem_with_concl thy i th =
blanchet@39887
    63
  let
blanchet@39887
    64
    val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
blanchet@39887
    65
    val prems = Logic.strip_assums_hyp goal
blanchet@39887
    66
    val concl = Logic.strip_assums_concl goal
blanchet@39887
    67
    fun add_types Tp instT =
blanchet@39887
    68
      if exists (curry (op =) Tp) instT then instT
blanchet@39887
    69
      else Tp :: map (apsnd (typ_subst_atomic [Tp])) instT
blanchet@39887
    70
    fun unify_types (T, U) =
blanchet@39887
    71
      if T = U then
blanchet@39887
    72
        I
blanchet@39887
    73
      else case (T, U) of
blanchet@39887
    74
        (TVar _, _) => add_types (T, U)
blanchet@39887
    75
      | (_, TVar _) => add_types (U, T)
blanchet@39887
    76
      | (Type (s, Ts), Type (t, Us)) =>
blanchet@39887
    77
        if s = t andalso length Ts = length Us then fold unify_types (Ts ~~ Us)
blanchet@39887
    78
        else raise TYPE ("unify_types", [T, U], [])
blanchet@39887
    79
      | _ => raise TYPE ("unify_types", [T, U], [])
blanchet@39887
    80
    fun pair_untyped_aconv (t1, t2) (u1, u2) =
blanchet@39887
    81
      untyped_aconv t1 u1 andalso untyped_aconv t2 u2
blanchet@39887
    82
    fun add_terms tp inst =
blanchet@39887
    83
      if exists (pair_untyped_aconv tp) inst then inst
blanchet@39887
    84
      else tp :: map (apsnd (subst_atomic [tp])) inst
blanchet@39887
    85
    fun is_flex t =
blanchet@39887
    86
      case strip_comb t of
blanchet@39887
    87
        (Var _, args) => forall (is_Bound orf is_Var orf is_Free) args
blanchet@39887
    88
      | _ => false
blanchet@39887
    89
    fun unify_flex flex rigid =
blanchet@39887
    90
      case strip_comb flex of
blanchet@39887
    91
        (Var (z as (_, T)), args) =>
blanchet@39887
    92
        add_terms (Var z,
blanchet@39887
    93
          (* FIXME: reindex bound variables *)
blanchet@39887
    94
          fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
blanchet@39887
    95
      | _ => raise TERM ("unify_flex: expected flex", [flex])
blanchet@39887
    96
    fun unify_potential_flex comb atom =
blanchet@39887
    97
      if is_flex comb then unify_flex comb atom
blanchet@39887
    98
      else if is_Var atom then add_terms (atom, comb)
blanchet@39887
    99
      else raise TERM ("unify_terms", [comb, atom])
blanchet@39887
   100
    fun unify_terms (t, u) =
blanchet@39887
   101
      case (t, u) of
blanchet@39887
   102
        (t1 $ t2, u1 $ u2) =>
blanchet@39887
   103
        if is_flex t then unify_flex t u
blanchet@39887
   104
        else if is_flex u then unify_flex u t
blanchet@39887
   105
        else fold unify_terms [(t1, u1), (t2, u2)]
blanchet@39887
   106
      | (_ $ _, _) => unify_potential_flex t u
blanchet@39887
   107
      | (_, _ $ _) => unify_potential_flex u t
blanchet@39887
   108
      | (Var _, _) => add_terms (t, u)
blanchet@39887
   109
      | (_, Var _) => add_terms (u, t)
blanchet@39887
   110
      | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
blanchet@39887
   111
    fun unify_prem prem =
blanchet@39887
   112
      let
blanchet@39887
   113
        val inst = [] |> unify_terms (prem, concl)
blanchet@39887
   114
        val instT = fold (unify_types o pairself fastype_of) inst []
blanchet@39887
   115
        val inst = inst |> map (pairself (subst_atomic_types instT))
blanchet@39887
   116
        val cinstT = instT |> map (pairself (ctyp_of thy))
blanchet@39887
   117
        val cinst = inst |> map (pairself (cterm_of thy))
blanchet@39887
   118
      in th |> Thm.instantiate (cinstT, []) |> Thm.instantiate ([], cinst) end
blanchet@39887
   119
  in
blanchet@39887
   120
    case prems of
blanchet@39887
   121
      [prem] => unify_prem prem
blanchet@39887
   122
    | _ =>
blanchet@39887
   123
      case fold (fn prem => fn th as SOME _ => th
blanchet@39887
   124
                             | NONE => try unify_prem prem) prems NONE of
blanchet@39887
   125
        SOME th => th
blanchet@39887
   126
      | NONE => raise Fail "unify_one_prem_with_concl"
blanchet@39887
   127
  end
blanchet@39887
   128
blanchet@39887
   129
(* Attempts to derive the theorem "False" from a theorem of the form
blanchet@39887
   130
   "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
blanchet@39887
   131
   specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
blanchet@39887
   132
   must be eliminated first. *)
blanchet@39887
   133
fun discharge_skolem_premises ctxt axioms premises_imp_false =
blanchet@39887
   134
  if prop_of premises_imp_false aconv @{prop False} then
blanchet@39887
   135
    premises_imp_false
blanchet@39887
   136
  else
blanchet@39887
   137
    let val thy = ProofContext.theory_of ctxt in
blanchet@39887
   138
      Goal.prove ctxt [] [] @{prop False}
blanchet@39887
   139
          (K (cut_rules_tac axioms 1
blanchet@39887
   140
              THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
blanchet@39887
   141
(* FIXME: THEN etac @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} 1 *)
blanchet@39887
   142
              THEN TRY (REPEAT_ALL_NEW (etac @{thm allE}) 1)
blanchet@39887
   143
              THEN match_tac [premises_imp_false] 1
blanchet@39887
   144
              THEN DETERM_UNTIL_SOLVED
blanchet@39887
   145
                       (PRIMITIVE (unify_one_prem_with_concl thy 1)
blanchet@39887
   146
                        THEN assume_tac 1)))
blanchet@39887
   147
    end
blanchet@39887
   148
blanchet@37516
   149
(* Main function to start Metis proof and reconstruction *)
wenzelm@32956
   150
fun FOL_SOLVE mode ctxt cls ths0 =
wenzelm@32956
   151
  let val thy = ProofContext.theory_of ctxt
blanchet@39497
   152
      val type_lits = Config.get ctxt type_lits
blanchet@39891
   153
      val new_skolemizer = Config.get ctxt new_skolemizer
blanchet@35826
   154
      val th_cls_pairs =
blanchet@39891
   155
        map (fn th => (Thm.get_name_hint th,
blanchet@39891
   156
                       Meson_Clausify.cnf_axiom thy new_skolemizer th)) ths0
blanchet@39887
   157
      val thss = map (snd o snd) th_cls_pairs
blanchet@39887
   158
      val dischargers = map_filter (fst o snd) th_cls_pairs
wenzelm@32956
   159
      val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
wenzelm@32956
   160
      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
wenzelm@32956
   161
      val _ = trace_msg (fn () => "THEOREM CLAUSES")
blanchet@39886
   162
      val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss
blanchet@39886
   163
      val (mode, {axioms, tfrees, old_skolems}) =
blanchet@39886
   164
        build_logic_map mode ctxt type_lits cls thss
wenzelm@32956
   165
      val _ = if null tfrees then ()
wenzelm@32956
   166
              else (trace_msg (fn () => "TFREE CLAUSES");
blanchet@37643
   167
                    app (fn TyLitFree ((s, _), (s', _)) =>
blanchet@39887
   168
                            trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
wenzelm@32956
   169
      val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
wenzelm@32956
   170
      val thms = map #1 axioms
blanchet@39419
   171
      val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms
wenzelm@32956
   172
      val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
wenzelm@32956
   173
      val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
wenzelm@32956
   174
  in
wenzelm@33317
   175
      case filter (is_false o prop_of) cls of
wenzelm@32956
   176
          false_th::_ => [false_th RS @{thm FalseE}]
wenzelm@32956
   177
        | [] =>
blanchet@39497
   178
      case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
blanchet@39497
   179
           |> Metis_Resolution.loop of
blanchet@39419
   180
          Metis_Resolution.Contradiction mth =>
wenzelm@32956
   181
            let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
blanchet@39419
   182
                          Metis_Thm.toString mth)
wenzelm@32956
   183
                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
wenzelm@32956
   184
                             (*add constraints arising from converting goal to clause form*)
blanchet@39419
   185
                val proof = Metis_Proof.proof mth
blanchet@39886
   186
                val result =
blanchet@39886
   187
                  fold (replay_one_inference ctxt' mode old_skolems) proof axioms
wenzelm@32956
   188
                and used = map_filter (used_axioms axioms) proof
wenzelm@32956
   189
                val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
wenzelm@32956
   190
                val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
blanchet@39887
   191
                val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) =>
blanchet@39497
   192
                  if have_common_thm used cls then NONE else SOME name)
wenzelm@32956
   193
            in
blanchet@39497
   194
                if not (null cls) andalso not (have_common_thm used cls) then
blanchet@36383
   195
                  warning "Metis: The assumptions are inconsistent."
blanchet@36383
   196
                else
blanchet@36383
   197
                  ();
blanchet@36383
   198
                if not (null unused) then
blanchet@36230
   199
                  warning ("Metis: Unused theorems: " ^ commas_quote unused
blanchet@36230
   200
                           ^ ".")
blanchet@36230
   201
                else
blanchet@36230
   202
                  ();
wenzelm@32956
   203
                case result of
wenzelm@32956
   204
                    (_,ith)::_ =>
blanchet@36230
   205
                        (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
blanchet@39887
   206
                         [discharge_skolem_premises ctxt dischargers ith])
blanchet@38097
   207
                  | _ => (trace_msg (fn () => "Metis: No result"); [])
wenzelm@32956
   208
            end
blanchet@39419
   209
        | Metis_Resolution.Satisfiable _ =>
wenzelm@32956
   210
            (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
blanchet@38097
   211
             [])
wenzelm@32956
   212
  end;
wenzelm@23442
   213
blanchet@38632
   214
(* Extensionalize "th", because that makes sense and that's what Sledgehammer
blanchet@38632
   215
   does, but also keep an unextensionalized version of "th" for backward
blanchet@38632
   216
   compatibility. *)
blanchet@38632
   217
fun also_extensionalize_theorem th =
blanchet@39890
   218
  let val th' = Meson_Clausify.extensionalize_theorem th in
blanchet@38632
   219
    if Thm.eq_thm (th, th') then [th]
blanchet@38632
   220
    else th :: Meson.make_clauses_unsorted [th']
blanchet@38632
   221
  end
blanchet@38632
   222
blanchet@38028
   223
val neg_clausify =
blanchet@38028
   224
  single
blanchet@38028
   225
  #> Meson.make_clauses_unsorted
blanchet@38632
   226
  #> maps also_extensionalize_theorem
blanchet@39890
   227
  #> map Meson_Clausify.introduce_combinators_in_theorem
blanchet@38028
   228
  #> Meson.finish_cnf
blanchet@38028
   229
blanchet@39269
   230
fun preskolem_tac ctxt st0 =
blanchet@39269
   231
  (if exists (Meson.has_too_many_clauses ctxt)
blanchet@39269
   232
             (Logic.prems_of_goal (prop_of st0) 1) then
blanchet@39269
   233
     cnf.cnfx_rewrite_tac ctxt 1
blanchet@39269
   234
   else
blanchet@39269
   235
     all_tac) st0
blanchet@39269
   236
blanchet@38652
   237
val type_has_top_sort =
blanchet@38652
   238
  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
blanchet@38652
   239
blanchet@37516
   240
fun generic_metis_tac mode ctxt ths i st0 =
blanchet@37926
   241
  let
blanchet@37926
   242
    val _ = trace_msg (fn () =>
wenzelm@32956
   243
        "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
wenzelm@32956
   244
  in
blanchet@37626
   245
    if exists_type type_has_top_sort (prop_of st0) then
blanchet@37516
   246
      (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
wenzelm@35568
   247
    else
blanchet@39594
   248
      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
blanchet@39594
   249
                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
blanchet@39594
   250
                  ctxt i st0
wenzelm@32956
   251
  end
wenzelm@23442
   252
blanchet@37516
   253
val metis_tac = generic_metis_tac HO
blanchet@37516
   254
val metisF_tac = generic_metis_tac FO
blanchet@37516
   255
val metisFT_tac = generic_metis_tac FT
wenzelm@23442
   256
blanchet@38632
   257
(* Whenever "X" has schematic type variables, we treat "using X by metis" as
blanchet@38632
   258
   "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
blanchet@38632
   259
   We don't do it for nonschematic facts "X" because this breaks a few proofs
blanchet@38632
   260
   (in the rare and subtle case where a proof relied on extensionality not being
blanchet@38994
   261
   applied) and brings few benefits. *)
blanchet@38632
   262
val has_tvar =
blanchet@38632
   263
  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
blanchet@37516
   264
fun method name mode =
blanchet@37516
   265
  Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
blanchet@38632
   266
    METHOD (fn facts =>
blanchet@38632
   267
               let
blanchet@38632
   268
                 val (schem_facts, nonschem_facts) =
blanchet@38632
   269
                   List.partition has_tvar facts
blanchet@38632
   270
               in
blanchet@38632
   271
                 HEADGOAL (Method.insert_tac nonschem_facts THEN'
blanchet@38632
   272
                           CHANGED_PROP
blanchet@38632
   273
                           o generic_metis_tac mode ctxt (schem_facts @ ths))
blanchet@38632
   274
               end)))
wenzelm@23442
   275
wenzelm@32956
   276
val setup =
blanchet@37516
   277
  type_lits_setup
blanchet@39891
   278
  #> new_skolemizer_setup
blanchet@37516
   279
  #> method @{binding metis} HO "Metis for FOL/HOL problems"
blanchet@37516
   280
  #> method @{binding metisF} FO "Metis for FOL problems"
blanchet@37516
   281
  #> method @{binding metisFT} FT
blanchet@37516
   282
            "Metis for FOL/HOL problems with fully-typed translation"
wenzelm@23442
   283
wenzelm@23442
   284
end;