src/HOL/Tools/Metis/metis_tactics.ML
author wenzelm
Mon, 02 May 2011 16:33:21 +0200
changeset 42616 92715b528e78
parent 42552 e155be7125ba
child 42650 552eae49f97d
permissions -rw-r--r--
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39958
88c9aa5666de tuned comments
blanchet
parents: 39953
diff changeset
     1
(*  Title:      HOL/Tools/Metis/metis_tactics.ML
38027
505657ddb047 standardize "Author" tags
blanchet
parents: 38016
diff changeset
     2
    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
505657ddb047 standardize "Author" tags
blanchet
parents: 38016
diff changeset
     3
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
505657ddb047 standardize "Author" tags
blanchet
parents: 38016
diff changeset
     4
    Author:     Jasmin Blanchette, TU Muenchen
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     5
    Copyright   Cambridge University 2007
23447
1f16190e3836 tuned comments;
wenzelm
parents: 23442
diff changeset
     6
29266
4a478f9d2847 use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 28700
diff changeset
     7
HOL setup for the Metis prover.
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     8
*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     9
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    10
signature METIS_TACTICS =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    11
sig
39979
b13515940b53 added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents: 39978
diff changeset
    12
  val trace : bool Config.T
40665
1a65f0c74827 added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents: 40262
diff changeset
    13
  val verbose : bool Config.T
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    14
  val type_lits : bool Config.T
39891
8e12f1956fcd "meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
blanchet
parents: 39890
diff changeset
    15
  val new_skolemizer : bool Config.T
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    16
  val metis_tac : Proof.context -> thm list -> int -> tactic
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    17
  val metisF_tac : Proof.context -> thm list -> int -> tactic
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    18
  val metisFT_tac : Proof.context -> thm list -> int -> tactic
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    19
  val setup : theory -> theory
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    20
end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    21
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    22
structure Metis_Tactics : METIS_TACTICS =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    23
struct
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    24
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39450
diff changeset
    25
open Metis_Translate
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    26
open Metis_Reconstruct
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    27
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42552
diff changeset
    28
val type_lits = Attrib.setup_config_bool @{binding metis_type_lits} (K true)
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42552
diff changeset
    29
val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    30
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    31
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    32
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    33
fun have_common_thm ths1 ths2 =
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    34
  exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    35
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    36
(*Determining which axiom clauses are actually used*)
39419
c9accfd621a5 "Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents: 39376
diff changeset
    37
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
    38
  | used_axioms _ _ = NONE;
24855
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
    39
39450
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    40
val clause_params =
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    41
  {ordering = Metis_KnuthBendixOrder.default,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    42
   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    43
   orderTerms = true}
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    44
val active_params =
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    45
  {clause = clause_params,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    46
   prefactor = #prefactor Metis_Active.default,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    47
   postfactor = #postfactor Metis_Active.default}
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    48
val waiting_params =
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    49
  {symbolsWeight = 1.0,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    50
   variablesWeight = 0.0,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    51
   literalsWeight = 0.0,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    52
   models = []}
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    53
val resolution_params = {active = active_params, waiting = waiting_params}
37573
7f987e8582a7 fewer dependencies
blanchet
parents: 37572
diff changeset
    54
37516
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
    55
(* Main function to start Metis proof and reconstruction *)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    56
fun FOL_SOLVE mode ctxt cls ths0 =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42341
diff changeset
    57
  let val thy = Proof_Context.theory_of ctxt
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    58
      val type_lits = Config.get ctxt type_lits
39901
75d792edf634 make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents: 39899
diff changeset
    59
      val new_skolemizer =
39950
f3c4849868b8 got rid of overkill "meson_choice" attribute;
blanchet
parents: 39946
diff changeset
    60
        Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    61
      val th_cls_pairs =
39894
35ae5cf8c96a encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents: 39892
diff changeset
    62
        map2 (fn j => fn th =>
35ae5cf8c96a encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents: 39892
diff changeset
    63
                (Thm.get_name_hint th,
39901
75d792edf634 make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents: 39899
diff changeset
    64
                 Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
39894
35ae5cf8c96a encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents: 39892
diff changeset
    65
             (0 upto length ths0 - 1) ths0
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
    66
      val thss = map (snd o snd) th_cls_pairs
39938
0a2091f86eb4 fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents: 39937
diff changeset
    67
      val dischargers = map (fst o snd) th_cls_pairs
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    68
      val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    69
      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    70
      val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    71
      val _ = app (app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th))) thss
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39721
diff changeset
    72
      val (mode, {axioms, tfrees, old_skolems}) =
40157
a2f01956220e renaming
blanchet
parents: 39979
diff changeset
    73
        prepare_metis_problem mode ctxt type_lits cls thss
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    74
      val _ = if null tfrees then ()
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    75
              else (trace_msg ctxt (fn () => "TFREE CLAUSES");
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37632
diff changeset
    76
                    app (fn TyLitFree ((s, _), (s', _)) =>
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    77
                            trace_msg ctxt (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    78
      val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    79
      val thms = map #1 axioms
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    80
      val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    81
      val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode)
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    82
      val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    83
  in
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 33316
diff changeset
    84
      case filter (is_false o prop_of) cls of
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    85
          false_th::_ => [false_th RS @{thm FalseE}]
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    86
        | [] =>
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    87
      case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    88
           |> Metis_Resolution.loop of
39419
c9accfd621a5 "Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents: 39376
diff changeset
    89
          Metis_Resolution.Contradiction mth =>
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    90
            let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
39419
c9accfd621a5 "Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents: 39376
diff changeset
    91
                          Metis_Thm.toString mth)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    92
                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    93
                             (*add constraints arising from converting goal to clause form*)
39419
c9accfd621a5 "Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents: 39376
diff changeset
    94
                val proof = Metis_Proof.proof mth
42341
5a00af7f4978 removed obsolete Skolem counter in new Skolemizer
blanchet
parents: 42336
diff changeset
    95
                val result = fold (replay_one_inference ctxt' mode old_skolems)
5a00af7f4978 removed obsolete Skolem counter in new Skolemizer
blanchet
parents: 42336
diff changeset
    96
                                  proof axioms
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    97
                and used = map_filter (used_axioms axioms) proof
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    98
                val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
    99
                val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   100
                val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) =>
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   101
                  if have_common_thm used cls then NONE else SOME name)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   102
            in
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   103
                if not (null cls) andalso not (have_common_thm used cls) then
40665
1a65f0c74827 added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents: 40262
diff changeset
   104
                  verbose_warning ctxt "Metis: The assumptions are inconsistent"
36383
6adf1068ac0f better error reporting;
blanchet
parents: 36230
diff changeset
   105
                else
6adf1068ac0f better error reporting;
blanchet
parents: 36230
diff changeset
   106
                  ();
6adf1068ac0f better error reporting;
blanchet
parents: 36230
diff changeset
   107
                if not (null unused) then
40665
1a65f0c74827 added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents: 40262
diff changeset
   108
                  verbose_warning ctxt ("Metis: Unused theorems: " ^
1a65f0c74827 added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents: 40262
diff changeset
   109
                                        commas_quote unused)
36230
43d10a494c91 added warning about inconsistent context to Metis;
blanchet
parents: 36170
diff changeset
   110
                else
43d10a494c91 added warning about inconsistent context to Metis;
blanchet
parents: 36170
diff changeset
   111
                  ();
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   112
                case result of
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   113
                    (_,ith)::_ =>
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   114
                        (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   115
                         [discharge_skolem_premises ctxt dischargers ith])
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   116
                  | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   117
            end
39419
c9accfd621a5 "Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents: 39376
diff changeset
   118
        | Metis_Resolution.Satisfiable _ =>
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   119
            (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
38097
5e4ad2df09f3 revert exception throwing in FOL_SOLVE, since they're not caught anyway
blanchet
parents: 38028
diff changeset
   120
             [])
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   121
  end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   122
38632
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   123
(* Extensionalize "th", because that makes sense and that's what Sledgehammer
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   124
   does, but also keep an unextensionalized version of "th" for backward
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   125
   compatibility. *)
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   126
fun also_extensionalize_theorem th =
39890
a1695e2169d0 finished renaming file and module
blanchet
parents: 39887
diff changeset
   127
  let val th' = Meson_Clausify.extensionalize_theorem th in
38632
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   128
    if Thm.eq_thm (th, th') then [th]
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   129
    else th :: Meson.make_clauses_unsorted [th']
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   130
  end
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   131
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   132
val neg_clausify =
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   133
  single
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   134
  #> Meson.make_clauses_unsorted
38632
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   135
  #> maps also_extensionalize_theorem
39890
a1695e2169d0 finished renaming file and module
blanchet
parents: 39887
diff changeset
   136
  #> map Meson_Clausify.introduce_combinators_in_theorem
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   137
  #> Meson.finish_cnf
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   138
39269
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39267
diff changeset
   139
fun preskolem_tac ctxt st0 =
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39267
diff changeset
   140
  (if exists (Meson.has_too_many_clauses ctxt)
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39267
diff changeset
   141
             (Logic.prems_of_goal (prop_of st0) 1) then
42336
d63d43e85879 improve definitional CNF on goal by moving "not" past the quantifiers
blanchet
parents: 40665
diff changeset
   142
     Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
d63d43e85879 improve definitional CNF on goal by moving "not" past the quantifiers
blanchet
parents: 40665
diff changeset
   143
     THEN cnf.cnfx_rewrite_tac ctxt 1
39269
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39267
diff changeset
   144
   else
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39267
diff changeset
   145
     all_tac) st0
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39267
diff changeset
   146
38652
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38632
diff changeset
   147
val type_has_top_sort =
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38632
diff changeset
   148
  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38632
diff changeset
   149
37516
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   150
fun generic_metis_tac mode ctxt ths i st0 =
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   151
  let
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   152
    val _ = trace_msg ctxt (fn () =>
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   153
        "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   154
  in
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37625
diff changeset
   155
    if exists_type type_has_top_sort (prop_of st0) then
40665
1a65f0c74827 added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents: 40262
diff changeset
   156
      (verbose_warning ctxt "Metis: Proof state contains the universal sort {}";
1a65f0c74827 added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents: 40262
diff changeset
   157
       Seq.empty)
35568
8fbbfc39508f renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents: 34087
diff changeset
   158
    else
39594
624d6c0e220d revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
blanchet
parents: 39560
diff changeset
   159
      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
40262
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 40259
diff changeset
   160
                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
39594
624d6c0e220d revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
blanchet
parents: 39560
diff changeset
   161
                  ctxt i st0
42552
e155be7125ba added a hint to Metis errors suggesting metisFT -- it sometimes work
blanchet
parents: 42361
diff changeset
   162
      handle ERROR message =>
e155be7125ba added a hint to Metis errors suggesting metisFT -- it sometimes work
blanchet
parents: 42361
diff changeset
   163
             error (message |> mode <> FT
e155be7125ba added a hint to Metis errors suggesting metisFT -- it sometimes work
blanchet
parents: 42361
diff changeset
   164
                               ? suffix "\nHint: You might want to try out \
e155be7125ba added a hint to Metis errors suggesting metisFT -- it sometimes work
blanchet
parents: 42361
diff changeset
   165
                                        \\"metisFT\".")
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   166
  end
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   167
37516
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   168
val metis_tac = generic_metis_tac HO
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   169
val metisF_tac = generic_metis_tac FO
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   170
val metisFT_tac = generic_metis_tac FT
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   171
38632
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   172
(* Whenever "X" has schematic type variables, we treat "using X by metis" as
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   173
   "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   174
   We don't do it for nonschematic facts "X" because this breaks a few proofs
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   175
   (in the rare and subtle case where a proof relied on extensionality not being
38994
7c655a491bce fiddled with fudge factor (based on Mirabelle)
blanchet
parents: 38864
diff changeset
   176
   applied) and brings few benefits. *)
38632
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   177
val has_tvar =
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   178
  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
37516
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   179
fun method name mode =
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   180
  Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
38632
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   181
    METHOD (fn facts =>
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   182
               let
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   183
                 val (schem_facts, nonschem_facts) =
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   184
                   List.partition has_tvar facts
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   185
               in
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   186
                 HEADGOAL (Method.insert_tac nonschem_facts THEN'
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   187
                           CHANGED_PROP
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   188
                           o generic_metis_tac mode ctxt (schem_facts @ ths))
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   189
               end)))
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   190
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   191
val setup =
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42552
diff changeset
   192
  method @{binding metis} HO "Metis for FOL/HOL problems"
37516
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   193
  #> method @{binding metisF} FO "Metis for FOL problems"
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   194
  #> method @{binding metisFT} FT
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   195
            "Metis for FOL/HOL problems with fully-typed translation"
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   196
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   197
end;