src/HOL/Tools/Metis/metis_tactics.ML
author blanchet
Tue Oct 05 10:59:12 2010 +0200 (2010-10-05)
changeset 39950 f3c4849868b8
parent 39946 78faa9b31202
child 39952 7fb79905ed72
permissions -rw-r--r--
got rid of overkill "meson_choice" attribute;
tuning
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@39899
    27
structure Int_Pair_Graph =
blanchet@39899
    28
  Graph(type key = int * int val ord = prod_ord int_ord int_ord)
blanchet@39899
    29
blanchet@39497
    30
fun trace_msg msg = if !trace then tracing (msg ()) else ()
wenzelm@32955
    31
blanchet@39891
    32
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
blanchet@39891
    33
val (new_skolemizer, new_skolemizer_setup) =
blanchet@39891
    34
  Attrib.config_bool "metis_new_skolemizer" (K false)
wenzelm@23442
    35
blanchet@39497
    36
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
wenzelm@23442
    37
blanchet@39497
    38
fun have_common_thm ths1 ths2 =
blanchet@39497
    39
  exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2)
wenzelm@23442
    40
wenzelm@32956
    41
(*Determining which axiom clauses are actually used*)
blanchet@39419
    42
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
wenzelm@32994
    43
  | used_axioms _ _ = NONE;
paulson@24855
    44
blanchet@39450
    45
val clause_params =
blanchet@39450
    46
  {ordering = Metis_KnuthBendixOrder.default,
blanchet@39450
    47
   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
blanchet@39450
    48
   orderTerms = true}
blanchet@39450
    49
val active_params =
blanchet@39450
    50
  {clause = clause_params,
blanchet@39450
    51
   prefactor = #prefactor Metis_Active.default,
blanchet@39450
    52
   postfactor = #postfactor Metis_Active.default}
blanchet@39450
    53
val waiting_params =
blanchet@39450
    54
  {symbolsWeight = 1.0,
blanchet@39450
    55
   variablesWeight = 0.0,
blanchet@39450
    56
   literalsWeight = 0.0,
blanchet@39450
    57
   models = []}
blanchet@39497
    58
val resolution_params = {active = active_params, waiting = waiting_params}
blanchet@37573
    59
blanchet@39938
    60
fun instantiate_theorem thy inst th =
blanchet@39938
    61
  let
blanchet@39938
    62
    val tyenv = Vartab.empty |> fold (Type.raw_unify o pairself fastype_of) inst
blanchet@39938
    63
    val instT =
blanchet@39938
    64
      [] |> Vartab.fold (fn (z, (S, T)) =>
blanchet@39938
    65
                            cons (TVar (z, S), Type.devar tyenv T)) tyenv
blanchet@39938
    66
    val inst = inst |> map (pairself (subst_atomic_types instT))
blanchet@39938
    67
    val _ = tracing (cat_lines (map (fn (T, U) =>
blanchet@39938
    68
        Syntax.string_of_typ @{context} T ^ " |-> " ^
blanchet@39938
    69
        Syntax.string_of_typ @{context} U) instT))
blanchet@39938
    70
    val _ = tracing (cat_lines (map (fn (t, u) =>
blanchet@39938
    71
        Syntax.string_of_term @{context} t ^ " |-> " ^
blanchet@39938
    72
        Syntax.string_of_term @{context} u) inst))
blanchet@39938
    73
    val cinstT = instT |> map (pairself (ctyp_of thy))
blanchet@39938
    74
    val cinst = inst |> map (pairself (cterm_of thy))
blanchet@39938
    75
  in th |> Thm.instantiate (cinstT, cinst) end
blanchet@39938
    76
blanchet@39935
    77
(* In principle, it should be sufficient to apply "assume_tac" to unify the
blanchet@39937
    78
   conclusion with one of the premises. However, in practice, this is unreliable
blanchet@39937
    79
   because of the mildly higher-order nature of the unification problems.
blanchet@39937
    80
   Typical constraints are of the form
blanchet@39937
    81
   "?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x",
blanchet@39937
    82
   where the nonvariables are goal parameters. *)
blanchet@39937
    83
fun unify_first_prem_with_concl thy i th =
blanchet@39935
    84
  let
blanchet@39935
    85
    val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
blanchet@39935
    86
    val prem = goal |> Logic.strip_assums_hyp |> hd
blanchet@39935
    87
    val concl = goal |> Logic.strip_assums_concl
blanchet@39935
    88
    fun pair_untyped_aconv (t1, t2) (u1, u2) =
blanchet@39935
    89
      untyped_aconv t1 u1 andalso untyped_aconv t2 u2
blanchet@39935
    90
    fun add_terms tp inst =
blanchet@39935
    91
      if exists (pair_untyped_aconv tp) inst then inst
blanchet@39935
    92
      else tp :: map (apsnd (subst_atomic [tp])) inst
blanchet@39935
    93
    fun is_flex t =
blanchet@39935
    94
      case strip_comb t of
blanchet@39937
    95
        (Var _, args) => forall is_Bound args
blanchet@39935
    96
      | _ => false
blanchet@39935
    97
    fun unify_flex flex rigid =
blanchet@39935
    98
      case strip_comb flex of
blanchet@39935
    99
        (Var (z as (_, T)), args) =>
blanchet@39935
   100
        add_terms (Var z,
blanchet@39935
   101
          fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
blanchet@39935
   102
      | _ => raise TERM ("unify_flex: expected flex", [flex])
blanchet@39935
   103
    fun unify_potential_flex comb atom =
blanchet@39935
   104
      if is_flex comb then unify_flex comb atom
blanchet@39935
   105
      else if is_Var atom then add_terms (atom, comb)
blanchet@39935
   106
      else raise TERM ("unify_terms", [comb, atom])
blanchet@39935
   107
    fun unify_terms (t, u) =
blanchet@39935
   108
      case (t, u) of
blanchet@39935
   109
        (t1 $ t2, u1 $ u2) =>
blanchet@39935
   110
        if is_flex t then unify_flex t u
blanchet@39935
   111
        else if is_flex u then unify_flex u t
blanchet@39935
   112
        else fold unify_terms [(t1, u1), (t2, u2)]
blanchet@39935
   113
      | (_ $ _, _) => unify_potential_flex t u
blanchet@39935
   114
      | (_, _ $ _) => unify_potential_flex u t
blanchet@39935
   115
      | (Var _, _) => add_terms (t, u)
blanchet@39935
   116
      | (_, Var _) => add_terms (u, t)
blanchet@39935
   117
      | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
blanchet@39938
   118
  in th |> instantiate_theorem thy (unify_terms (prem, concl) []) end
blanchet@39935
   119
blanchet@39933
   120
fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no)
blanchet@39933
   121
fun shuffle_ord p =
blanchet@39933
   122
  rev_order (prod_ord int_ord int_ord (pairself shuffle_key p))
blanchet@39933
   123
blanchet@39933
   124
val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
blanchet@39933
   125
blanchet@39933
   126
fun copy_prems_tac [] ns i =
blanchet@39933
   127
    if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
blanchet@39933
   128
  | copy_prems_tac (1 :: ms) ns i =
blanchet@39933
   129
    rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
blanchet@39933
   130
  | copy_prems_tac (m :: ms) ns i =
blanchet@39933
   131
    etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
blanchet@39933
   132
blanchet@39933
   133
fun instantiate_forall_tac thy params t i =
blanchet@39887
   134
  let
blanchet@39933
   135
    fun repair (t as (Var ((s, _), _))) =
blanchet@39933
   136
        (case find_index (fn ((s', _), _) => s' = s) params of
blanchet@39933
   137
           ~1 => t
blanchet@39933
   138
         | j => Bound j)
blanchet@39933
   139
      | repair (t $ u) = repair t $ repair u
blanchet@39933
   140
      | repair t = t
blanchet@39933
   141
    val t' = t |> repair |> fold (curry absdummy) (map snd params)
blanchet@39933
   142
    fun do_instantiate th =
blanchet@39933
   143
      let val var = Term.add_vars (prop_of th) [] |> the_single in
blanchet@39938
   144
        th |> instantiate_theorem thy [(Var var, t')]
blanchet@39933
   145
      end
blanchet@39933
   146
  in
blanchet@39933
   147
    etac @{thm allE} i
blanchet@39933
   148
    THEN rotate_tac ~1 i
blanchet@39933
   149
    THEN PRIMITIVE do_instantiate
blanchet@39933
   150
  end
blanchet@39897
   151
blanchet@39933
   152
fun release_clusters_tac _ _ _ _ [] = K all_tac
blanchet@39933
   153
  | release_clusters_tac thy ax_counts substs params
blanchet@39933
   154
                         ((ax_no, cluster_no) :: clusters) =
blanchet@39933
   155
    let
blanchet@39933
   156
      fun in_right_cluster s =
blanchet@39933
   157
        (s |> Meson_Clausify.cluster_of_zapped_var_name |> fst |> snd |> fst)
blanchet@39933
   158
        = cluster_no
blanchet@39937
   159
      val cluster_substs =
blanchet@39933
   160
        substs
blanchet@39937
   161
        |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
blanchet@39937
   162
                          if ax_no' = ax_no then
blanchet@39937
   163
                            tsubst |> filter (in_right_cluster
blanchet@39937
   164
                                               o fst o fst o dest_Var o fst)
blanchet@39937
   165
                                    |> map snd |> SOME
blanchet@39937
   166
                           else
blanchet@39937
   167
                             NONE)
blanchet@39937
   168
      val n = length cluster_substs
blanchet@39937
   169
      fun do_cluster_subst cluster_subst =
blanchet@39937
   170
        map (instantiate_forall_tac thy params) cluster_subst @ [rotate_tac 1]
blanchet@39938
   171
      val params' = params (* FIXME ### existentials! *)
blanchet@39938
   172
      val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
blanchet@39933
   173
    in
blanchet@39938
   174
      rotate_tac first_prem
blanchet@39937
   175
      THEN' (EVERY' (maps do_cluster_subst cluster_substs))
blanchet@39938
   176
      THEN' rotate_tac (~ first_prem - length cluster_substs)
blanchet@39933
   177
      THEN' release_clusters_tac thy ax_counts substs params' clusters
blanchet@39937
   178
    end
blanchet@39887
   179
blanchet@39933
   180
val cluster_ord =
blanchet@39933
   181
  prod_ord (prod_ord int_ord (prod_ord int_ord int_ord)) bool_ord
blanchet@39899
   182
blanchet@39935
   183
val tysubst_ord =
blanchet@39935
   184
  list_ord (prod_ord Term_Ord.fast_indexname_ord
blanchet@39935
   185
                     (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
blanchet@39935
   186
blanchet@39935
   187
structure Int_Tysubst_Table =
blanchet@39935
   188
  Table(type key = int * (indexname * (sort * typ)) list
blanchet@39935
   189
        val ord = prod_ord int_ord tysubst_ord)
blanchet@39935
   190
blanchet@39887
   191
(* Attempts to derive the theorem "False" from a theorem of the form
blanchet@39887
   192
   "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
blanchet@39887
   193
   specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
blanchet@39887
   194
   must be eliminated first. *)
blanchet@39897
   195
fun discharge_skolem_premises ctxt axioms prems_imp_false =
blanchet@39935
   196
  if prop_of prems_imp_false aconv @{prop False} then
blanchet@39935
   197
    prems_imp_false
blanchet@39935
   198
  else
blanchet@39897
   199
    let
blanchet@39897
   200
      val thy = ProofContext.theory_of ctxt
blanchet@39935
   201
      (* distinguish variables with same name but different types *)
blanchet@39935
   202
      val prems_imp_false' =
blanchet@39936
   203
        prems_imp_false |> try (forall_intr_vars #> gen_all)
blanchet@39935
   204
                        |> the_default prems_imp_false
blanchet@39935
   205
      val prems_imp_false =
blanchet@39935
   206
        if prop_of prems_imp_false aconv prop_of prems_imp_false' then
blanchet@39935
   207
          prems_imp_false
blanchet@39935
   208
        else
blanchet@39935
   209
          prems_imp_false'
blanchet@39897
   210
      fun match_term p =
blanchet@39897
   211
        let
blanchet@39897
   212
          val (tyenv, tenv) =
blanchet@39897
   213
            Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
blanchet@39897
   214
          val tsubst =
blanchet@39897
   215
            tenv |> Vartab.dest
blanchet@39899
   216
                 |> sort (cluster_ord
blanchet@39899
   217
                          o pairself (Meson_Clausify.cluster_of_zapped_var_name
blanchet@39897
   218
                                      o fst o fst))
blanchet@39897
   219
                 |> map (Meson.term_pair_of
blanchet@39897
   220
                         #> pairself (Envir.subst_term_types tyenv))
blanchet@39935
   221
          val tysubst = tyenv |> Vartab.dest
blanchet@39935
   222
        in (tysubst, tsubst) end
blanchet@39934
   223
      fun subst_info_for_prem subgoal_no prem =
blanchet@39897
   224
        case prem of
blanchet@39897
   225
          _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) =>
blanchet@39902
   226
          let val ax_no = HOLogic.dest_nat num in
blanchet@39938
   227
            (ax_no, (subgoal_no,
blanchet@39938
   228
                     match_term (nth axioms ax_no |> the |> snd, t)))
blanchet@39897
   229
          end
blanchet@39897
   230
        | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
blanchet@39897
   231
                           [prem])
blanchet@39899
   232
      fun cluster_of_var_name skolem s =
blanchet@39933
   233
        let
blanchet@39933
   234
          val ((ax_no, (cluster_no, _)), skolem') =
blanchet@39933
   235
            Meson_Clausify.cluster_of_zapped_var_name s
blanchet@39933
   236
        in
blanchet@39933
   237
          if skolem' = skolem andalso cluster_no > 0 then
blanchet@39933
   238
            SOME (ax_no, cluster_no)
blanchet@39933
   239
          else
blanchet@39933
   240
            NONE
blanchet@39899
   241
        end
blanchet@39899
   242
      fun clusters_in_term skolem t =
blanchet@39899
   243
        Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
blanchet@39899
   244
      fun deps_for_term_subst (var, t) =
blanchet@39899
   245
        case clusters_in_term false var of
blanchet@39899
   246
          [] => NONE
blanchet@39899
   247
        | [(ax_no, cluster_no)] =>
blanchet@39899
   248
          SOME ((ax_no, cluster_no),
blanchet@39899
   249
                clusters_in_term true t
blanchet@39933
   250
                |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
blanchet@39899
   251
        | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
blanchet@39935
   252
      val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
blanchet@39934
   253
      val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
blanchet@39933
   254
                         |> sort (int_ord o pairself fst)
blanchet@39899
   255
      val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
blanchet@39899
   256
      val clusters = maps (op ::) depss
blanchet@39899
   257
      val ordered_clusters =
blanchet@39899
   258
        Int_Pair_Graph.empty
blanchet@39899
   259
        |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
blanchet@39899
   260
        |> fold Int_Pair_Graph.add_deps_acyclic depss
blanchet@39899
   261
        |> Int_Pair_Graph.topological_order
blanchet@39899
   262
        handle Int_Pair_Graph.CYCLES _ =>
blanchet@39899
   263
               error "Cannot replay Metis proof in Isabelle without axiom of \
blanchet@39899
   264
                     \choice."
blanchet@39933
   265
      val params0 =
blanchet@39938
   266
        [] |> fold (Term.add_vars o snd) (map_filter I axioms)
blanchet@39933
   267
           |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst))
blanchet@39933
   268
           |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
blanchet@39933
   269
                         cluster_no = 0 andalso skolem)
blanchet@39933
   270
           |> sort shuffle_ord |> map snd
blanchet@39933
   271
      val ax_counts =
blanchet@39935
   272
        Int_Tysubst_Table.empty
blanchet@39935
   273
        |> fold (fn (ax_no, (_, (tysubst, _))) =>
blanchet@39935
   274
                    Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
blanchet@39935
   275
                                                  (Integer.add 1)) substs
blanchet@39935
   276
        |> Int_Tysubst_Table.dest
blanchet@39938
   277
(* for debugging:
blanchet@39935
   278
      fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
blanchet@39934
   279
        "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
blanchet@39935
   280
        "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
blanchet@39933
   281
        commas (map ((fn (s, t) => s ^ " |-> " ^ t)
blanchet@39933
   282
                     o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
blanchet@39936
   283
      val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
blanchet@39936
   284
                       cat_lines (map string_for_subst_info substs))
blanchet@39933
   285
      val _ = tracing ("OUTERMOST SKOLEMS: " ^ PolyML.makestring params0)
blanchet@39933
   286
      val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
blanchet@39935
   287
      val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
blanchet@39938
   288
*)
blanchet@39934
   289
      fun rotation_for_subgoal i =
blanchet@39934
   290
        find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
blanchet@39897
   291
    in
blanchet@39887
   292
      Goal.prove ctxt [] [] @{prop False}
blanchet@39938
   293
          (K (cut_rules_tac
blanchet@39938
   294
                  (map (fst o the o nth axioms o fst o fst) ax_counts) 1
blanchet@39937
   295
              THEN print_tac "cut:"
blanchet@39887
   296
              THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
blanchet@39933
   297
              THEN copy_prems_tac (map snd ax_counts) [] 1
blanchet@39938
   298
              THEN print_tac "eliminated exist and copied prems:"
blanchet@39933
   299
              THEN release_clusters_tac thy ax_counts substs params0
blanchet@39933
   300
                                        ordered_clusters 1
blanchet@39937
   301
              THEN print_tac "released clusters:"
blanchet@39897
   302
              THEN match_tac [prems_imp_false] 1
blanchet@39933
   303
              THEN print_tac "applied rule:"
blanchet@39935
   304
              THEN ALLGOALS (fn i =>
blanchet@39935
   305
                       rtac @{thm skolem_COMBK_I} i
blanchet@39935
   306
                       THEN rotate_tac (rotation_for_subgoal i) i
blanchet@39937
   307
                       THEN PRIMITIVE (unify_first_prem_with_concl thy i)
blanchet@39935
   308
                       THEN assume_tac i)))
blanchet@39887
   309
    end
blanchet@39887
   310
blanchet@37516
   311
(* Main function to start Metis proof and reconstruction *)
wenzelm@32956
   312
fun FOL_SOLVE mode ctxt cls ths0 =
wenzelm@32956
   313
  let val thy = ProofContext.theory_of ctxt
blanchet@39497
   314
      val type_lits = Config.get ctxt type_lits
blanchet@39901
   315
      val new_skolemizer =
blanchet@39950
   316
        Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
blanchet@35826
   317
      val th_cls_pairs =
blanchet@39894
   318
        map2 (fn j => fn th =>
blanchet@39894
   319
                (Thm.get_name_hint th,
blanchet@39901
   320
                 Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
blanchet@39894
   321
             (0 upto length ths0 - 1) ths0
blanchet@39887
   322
      val thss = map (snd o snd) th_cls_pairs
blanchet@39938
   323
      val dischargers = map (fst o snd) th_cls_pairs
wenzelm@32956
   324
      val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
wenzelm@32956
   325
      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
wenzelm@32956
   326
      val _ = trace_msg (fn () => "THEOREM CLAUSES")
blanchet@39886
   327
      val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss
blanchet@39886
   328
      val (mode, {axioms, tfrees, old_skolems}) =
blanchet@39886
   329
        build_logic_map mode ctxt type_lits cls thss
wenzelm@32956
   330
      val _ = if null tfrees then ()
wenzelm@32956
   331
              else (trace_msg (fn () => "TFREE CLAUSES");
blanchet@37643
   332
                    app (fn TyLitFree ((s, _), (s', _)) =>
blanchet@39887
   333
                            trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
wenzelm@32956
   334
      val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
wenzelm@32956
   335
      val thms = map #1 axioms
blanchet@39419
   336
      val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms
wenzelm@32956
   337
      val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
wenzelm@32956
   338
      val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
wenzelm@32956
   339
  in
wenzelm@33317
   340
      case filter (is_false o prop_of) cls of
wenzelm@32956
   341
          false_th::_ => [false_th RS @{thm FalseE}]
wenzelm@32956
   342
        | [] =>
blanchet@39497
   343
      case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
blanchet@39497
   344
           |> Metis_Resolution.loop of
blanchet@39419
   345
          Metis_Resolution.Contradiction mth =>
wenzelm@32956
   346
            let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
blanchet@39419
   347
                          Metis_Thm.toString mth)
wenzelm@32956
   348
                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
wenzelm@32956
   349
                             (*add constraints arising from converting goal to clause form*)
blanchet@39419
   350
                val proof = Metis_Proof.proof mth
blanchet@39886
   351
                val result =
blanchet@39886
   352
                  fold (replay_one_inference ctxt' mode old_skolems) proof axioms
wenzelm@32956
   353
                and used = map_filter (used_axioms axioms) proof
wenzelm@32956
   354
                val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
wenzelm@32956
   355
                val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
blanchet@39887
   356
                val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) =>
blanchet@39497
   357
                  if have_common_thm used cls then NONE else SOME name)
wenzelm@32956
   358
            in
blanchet@39497
   359
                if not (null cls) andalso not (have_common_thm used cls) then
blanchet@36383
   360
                  warning "Metis: The assumptions are inconsistent."
blanchet@36383
   361
                else
blanchet@36383
   362
                  ();
blanchet@36383
   363
                if not (null unused) then
blanchet@36230
   364
                  warning ("Metis: Unused theorems: " ^ commas_quote unused
blanchet@36230
   365
                           ^ ".")
blanchet@36230
   366
                else
blanchet@36230
   367
                  ();
wenzelm@32956
   368
                case result of
wenzelm@32956
   369
                    (_,ith)::_ =>
blanchet@39938
   370
                        (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
blanchet@39887
   371
                         [discharge_skolem_premises ctxt dischargers ith])
blanchet@38097
   372
                  | _ => (trace_msg (fn () => "Metis: No result"); [])
wenzelm@32956
   373
            end
blanchet@39419
   374
        | Metis_Resolution.Satisfiable _ =>
wenzelm@32956
   375
            (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
blanchet@38097
   376
             [])
wenzelm@32956
   377
  end;
wenzelm@23442
   378
blanchet@38632
   379
(* Extensionalize "th", because that makes sense and that's what Sledgehammer
blanchet@38632
   380
   does, but also keep an unextensionalized version of "th" for backward
blanchet@38632
   381
   compatibility. *)
blanchet@38632
   382
fun also_extensionalize_theorem th =
blanchet@39890
   383
  let val th' = Meson_Clausify.extensionalize_theorem th in
blanchet@38632
   384
    if Thm.eq_thm (th, th') then [th]
blanchet@38632
   385
    else th :: Meson.make_clauses_unsorted [th']
blanchet@38632
   386
  end
blanchet@38632
   387
blanchet@38028
   388
val neg_clausify =
blanchet@38028
   389
  single
blanchet@38028
   390
  #> Meson.make_clauses_unsorted
blanchet@38632
   391
  #> maps also_extensionalize_theorem
blanchet@39890
   392
  #> map Meson_Clausify.introduce_combinators_in_theorem
blanchet@38028
   393
  #> Meson.finish_cnf
blanchet@38028
   394
blanchet@39269
   395
fun preskolem_tac ctxt st0 =
blanchet@39269
   396
  (if exists (Meson.has_too_many_clauses ctxt)
blanchet@39269
   397
             (Logic.prems_of_goal (prop_of st0) 1) then
blanchet@39269
   398
     cnf.cnfx_rewrite_tac ctxt 1
blanchet@39269
   399
   else
blanchet@39269
   400
     all_tac) st0
blanchet@39269
   401
blanchet@38652
   402
val type_has_top_sort =
blanchet@38652
   403
  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
blanchet@38652
   404
blanchet@37516
   405
fun generic_metis_tac mode ctxt ths i st0 =
blanchet@37926
   406
  let
blanchet@37926
   407
    val _ = trace_msg (fn () =>
wenzelm@32956
   408
        "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
wenzelm@32956
   409
  in
blanchet@37626
   410
    if exists_type type_has_top_sort (prop_of st0) then
blanchet@37516
   411
      (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
wenzelm@35568
   412
    else
blanchet@39594
   413
      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
blanchet@39594
   414
                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
blanchet@39594
   415
                  ctxt i st0
wenzelm@32956
   416
  end
wenzelm@23442
   417
blanchet@37516
   418
val metis_tac = generic_metis_tac HO
blanchet@37516
   419
val metisF_tac = generic_metis_tac FO
blanchet@37516
   420
val metisFT_tac = generic_metis_tac FT
wenzelm@23442
   421
blanchet@38632
   422
(* Whenever "X" has schematic type variables, we treat "using X by metis" as
blanchet@38632
   423
   "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
blanchet@38632
   424
   We don't do it for nonschematic facts "X" because this breaks a few proofs
blanchet@38632
   425
   (in the rare and subtle case where a proof relied on extensionality not being
blanchet@38994
   426
   applied) and brings few benefits. *)
blanchet@38632
   427
val has_tvar =
blanchet@38632
   428
  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
blanchet@37516
   429
fun method name mode =
blanchet@37516
   430
  Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
blanchet@38632
   431
    METHOD (fn facts =>
blanchet@38632
   432
               let
blanchet@38632
   433
                 val (schem_facts, nonschem_facts) =
blanchet@38632
   434
                   List.partition has_tvar facts
blanchet@38632
   435
               in
blanchet@38632
   436
                 HEADGOAL (Method.insert_tac nonschem_facts THEN'
blanchet@38632
   437
                           CHANGED_PROP
blanchet@38632
   438
                           o generic_metis_tac mode ctxt (schem_facts @ ths))
blanchet@38632
   439
               end)))
wenzelm@23442
   440
wenzelm@32956
   441
val setup =
blanchet@37516
   442
  type_lits_setup
blanchet@39891
   443
  #> new_skolemizer_setup
blanchet@37516
   444
  #> method @{binding metis} HO "Metis for FOL/HOL problems"
blanchet@37516
   445
  #> method @{binding metisF} FO "Metis for FOL problems"
blanchet@37516
   446
  #> method @{binding metisFT} FT
blanchet@37516
   447
            "Metis for FOL/HOL problems with fully-typed translation"
wenzelm@23442
   448
wenzelm@23442
   449
end;