src/HOL/Tools/Metis/metis_tactics.ML
author blanchet
Tue, 07 Jun 2011 11:12:52 +0200
changeset 43235 3a8d49bc06e1
parent 43228 2ed2f092e990
child 43298 82d4874757df
permissions -rw-r--r--
tuning
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
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43034
diff changeset
    12
  val metisN : string
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    13
  val full_typesN : string
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    14
  val partial_typesN : string
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    15
  val no_typesN : string
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    16
  val full_type_sys : string
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    17
  val partial_type_sys : string
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    18
  val no_type_sys : string
39979
b13515940b53 added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents: 39978
diff changeset
    19
  val trace : bool Config.T
40665
1a65f0c74827 added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents: 40262
diff changeset
    20
  val verbose : 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
    21
  val new_skolemizer : bool Config.T
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
    22
  val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    23
  val setup : theory -> theory
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    24
end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    25
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    26
structure Metis_Tactics : METIS_TACTICS =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    27
struct
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    28
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43050
diff changeset
    29
open ATP_Translate
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39450
diff changeset
    30
open Metis_Translate
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    31
open Metis_Reconstruct
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    32
43211
77c432fe28ff enable new Metis
blanchet
parents: 43206
diff changeset
    33
val metisN = Binding.qualified_name_of @{binding metis}
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    34
43205
23b81469499f more preparations towards hijacking Metis
blanchet
parents: 43204
diff changeset
    35
val full_typesN = "full_types"
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    36
val partial_typesN = "partial_types"
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    37
val no_typesN = "no_types"
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43034
diff changeset
    38
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    39
val full_type_sys = "poly_preds_heavy_query"
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    40
val partial_type_sys = "poly_args"
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    41
val no_type_sys = "erased"
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    42
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    43
val type_sys_aliases =
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    44
  [(full_typesN, full_type_sys),
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    45
   (partial_typesN, partial_type_sys),
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    46
   (no_typesN, no_type_sys)]
43211
77c432fe28ff enable new Metis
blanchet
parents: 43206
diff changeset
    47
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
    48
fun method_call_for_type_sys type_sys =
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    49
  metisN ^ " (" ^
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    50
  (case AList.find (op =) type_sys_aliases type_sys of
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    51
     [alias] => alias
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
    52
   | _ => type_sys) ^ ")"
43205
23b81469499f more preparations towards hijacking Metis
blanchet
parents: 43204
diff changeset
    53
43089
c2ec08b0d217 added "metisX" syntax (temporary)
blanchet
parents: 43085
diff changeset
    54
val new_skolemizer =
c2ec08b0d217 added "metisX" syntax (temporary)
blanchet
parents: 43085
diff changeset
    55
  Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    56
43134
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
    57
(* Designed to work also with monomorphic instances of polymorphic theorems. *)
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    58
fun have_common_thm ths1 ths2 =
43134
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
    59
  exists (member (untyped_aconv o pairself prop_of) ths1)
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
    60
         (map Meson.make_meta_clause ths2)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    61
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    62
(*Determining which axiom clauses are actually used*)
39419
c9accfd621a5 "Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents: 39376
diff changeset
    63
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
43128
a19826080596 tuned names
blanchet
parents: 43103
diff changeset
    64
  | used_axioms _ _ = NONE
24855
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
    65
43129
4301f1c123d6 support lightweight tags in new Metis
blanchet
parents: 43128
diff changeset
    66
(* Lightweight predicate type information comes in two flavors, "t = t'" and
4301f1c123d6 support lightweight tags in new Metis
blanchet
parents: 43128
diff changeset
    67
   "t => t'", where "t" and "t'" are the same term modulo type tags.
4301f1c123d6 support lightweight tags in new Metis
blanchet
parents: 43128
diff changeset
    68
   In Isabelle, type tags are stripped away, so we are left with "t = t" or
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
    69
   "t => t". Type tag idempotence is also handled this way. *)
43184
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43169
diff changeset
    70
fun reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth =
43136
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    71
  let val thy = Proof_Context.theory_of ctxt in
43184
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43169
diff changeset
    72
    case hol_clause_from_metis ctxt sym_tab old_skolems mth of
43136
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    73
      Const (@{const_name HOL.eq}, _) $ _ $ t =>
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    74
      t |> cterm_of thy |> Thm.reflexive RS @{thm meta_eq_to_obj_eq}
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    75
    | Const (@{const_name disj}, _) $ t1 $ t2 =>
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    76
      (if can HOLogic.dest_not t1 then t2 else t1)
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    77
      |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    78
    | _ => raise Fail "unexpected tags sym clause"
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43135
diff changeset
    79
  end
43129
4301f1c123d6 support lightweight tags in new Metis
blanchet
parents: 43128
diff changeset
    80
  |> Meson.make_meta_clause
4301f1c123d6 support lightweight tags in new Metis
blanchet
parents: 43128
diff changeset
    81
39450
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    82
val clause_params =
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    83
  {ordering = Metis_KnuthBendixOrder.default,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    84
   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    85
   orderTerms = true}
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    86
val active_params =
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    87
  {clause = clause_params,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    88
   prefactor = #prefactor Metis_Active.default,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    89
   postfactor = #postfactor Metis_Active.default}
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    90
val waiting_params =
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    91
  {symbolsWeight = 1.0,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    92
   variablesWeight = 0.0,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    93
   literalsWeight = 0.0,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
    94
   models = []}
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
    95
val resolution_params = {active = active_params, waiting = waiting_params}
37573
7f987e8582a7 fewer dependencies
blanchet
parents: 37572
diff changeset
    96
37516
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
    97
(* Main function to start Metis proof and reconstruction *)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
    98
fun FOL_SOLVE (type_sys :: fallback_type_syss) ctxt cls ths0 =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42341
diff changeset
    99
  let val thy = Proof_Context.theory_of ctxt
39901
75d792edf634 make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents: 39899
diff changeset
   100
      val new_skolemizer =
39950
f3c4849868b8 got rid of overkill "meson_choice" attribute;
blanchet
parents: 39946
diff changeset
   101
        Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
   102
      val th_cls_pairs =
39894
35ae5cf8c96a encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents: 39892
diff changeset
   103
        map2 (fn j => fn th =>
35ae5cf8c96a encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents: 39892
diff changeset
   104
                (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
   105
                 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
   106
             (0 upto length ths0 - 1) ths0
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
   107
      val ths = maps (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
   108
      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
   109
      val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   110
      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
   111
      val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43091
diff changeset
   112
      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   113
      val (sym_tab, axioms, old_skolems) =
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   114
        prepare_metis_problem ctxt type_sys cls ths
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
   115
      fun get_isa_thm mth Isa_Reflexive_or_Trivial =
43184
b16693484c5d reveal Skolems in new Metis
blanchet
parents: 43169
diff changeset
   116
          reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
   117
        | get_isa_thm _ (Isa_Raw ith) = ith
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
   118
      val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   119
      val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
   120
      val thms = axioms |> map fst
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   121
      val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   122
      val _ = trace_msg ctxt (fn () => "type_sys = " ^ type_sys)
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   123
      val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   124
  in
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
   125
      case filter (fn t => prop_of t aconv @{prop False}) cls of
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43136
diff changeset
   126
          false_th :: _ => [false_th RS @{thm FalseE}]
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   127
        | [] =>
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   128
      case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   129
           |> Metis_Resolution.loop of
39419
c9accfd621a5 "Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents: 39376
diff changeset
   130
          Metis_Resolution.Contradiction mth =>
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   131
            let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
39419
c9accfd621a5 "Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents: 39376
diff changeset
   132
                          Metis_Thm.toString mth)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   133
                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   134
                             (*add constraints arising from converting goal to clause form*)
39419
c9accfd621a5 "Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents: 39376
diff changeset
   135
                val proof = Metis_Proof.proof mth
43094
269300fb83d0 more work on new Metis
blanchet
parents: 43092
diff changeset
   136
                val result =
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   137
                  axioms
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   138
                  |> fold (replay_one_inference ctxt' old_skolems sym_tab) proof
43134
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
   139
                val used = map_filter (used_axioms axioms) proof
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   140
                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
   141
                val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
43134
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
   142
                val names = th_cls_pairs |> map fst
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
   143
                val used_names =
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
   144
                  th_cls_pairs
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
   145
                  |> map_filter (fn (name, (_, cls)) =>
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
   146
                                    if have_common_thm used cls then SOME name
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
   147
                                    else NONE)
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
   148
                val unused_names = names |> subtract (op =) used_names
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   149
            in
39497
fa16349939b7 complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents: 39494
diff changeset
   150
                if not (null cls) andalso not (have_common_thm used cls) then
42650
552eae49f97d reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents: 42616
diff changeset
   151
                  verbose_warning ctxt "The assumptions are inconsistent"
36383
6adf1068ac0f better error reporting;
blanchet
parents: 36230
diff changeset
   152
                else
6adf1068ac0f better error reporting;
blanchet
parents: 36230
diff changeset
   153
                  ();
43134
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
   154
                if not (null unused_names) then
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
   155
                  "Unused theorems: " ^ commas_quote unused_names
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
   156
                  |> verbose_warning ctxt
36230
43d10a494c91 added warning about inconsistent context to Metis;
blanchet
parents: 36170
diff changeset
   157
                else
43d10a494c91 added warning about inconsistent context to Metis;
blanchet
parents: 36170
diff changeset
   158
                  ();
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   159
                case result of
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   160
                    (_,ith)::_ =>
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   161
                        (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
   162
                         [discharge_skolem_premises ctxt dischargers ith])
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   163
                  | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   164
            end
39419
c9accfd621a5 "Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents: 39376
diff changeset
   165
        | Metis_Resolution.Satisfiable _ =>
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   166
            (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   167
             if null fallback_type_syss then
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 42847
diff changeset
   168
               ()
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 42847
diff changeset
   169
             else
42650
552eae49f97d reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents: 42616
diff changeset
   170
               raise METIS ("FOL_SOLVE",
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 42847
diff changeset
   171
                            "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
   172
             [])
42733
01ef1c3d9cfd more robust exception handling in Metis (also works if there are several subgoals)
blanchet
parents: 42650
diff changeset
   173
  end
01ef1c3d9cfd more robust exception handling in Metis (also works if there are several subgoals)
blanchet
parents: 42650
diff changeset
   174
  handle METIS (loc, msg) =>
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   175
         case fallback_type_syss of
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 42847
diff changeset
   176
           [] => error ("Failed to replay Metis proof in Isabelle." ^
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 42847
diff changeset
   177
                        (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 42847
diff changeset
   178
                         else ""))
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   179
         | type_sys :: _ =>
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   180
           (verbose_warning ctxt
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   181
                ("Falling back on " ^
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   182
                 quote (method_call_for_type_sys type_sys) ^ "...");
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   183
            FOL_SOLVE fallback_type_syss ctxt cls ths0)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   184
42847
blanchet
parents: 42747
diff changeset
   185
val neg_clausify =
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   186
  single
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   187
  #> Meson.make_clauses_unsorted
39890
a1695e2169d0 finished renaming file and module
blanchet
parents: 39887
diff changeset
   188
  #> map Meson_Clausify.introduce_combinators_in_theorem
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   189
  #> Meson.finish_cnf
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   190
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
   191
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
   192
  (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
   193
             (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
   194
     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
   195
     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
   196
   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
   197
     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
   198
38652
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38632
diff changeset
   199
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
   200
  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
   201
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   202
fun generic_metis_tac type_syss ctxt ths i st0 =
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   203
  let
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   204
    val _ = trace_msg ctxt (fn () =>
43194
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43184
diff changeset
   205
        "Metis called with theorems\n" ^
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 42847
diff changeset
   206
        cat_lines (map (Display.string_of_thm ctxt) ths))
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   207
    fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   208
  in
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37625
diff changeset
   209
    if exists_type type_has_top_sort (prop_of st0) then
42650
552eae49f97d reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents: 42616
diff changeset
   210
      (verbose_warning ctxt "Proof state contains the universal sort {}";
40665
1a65f0c74827 added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents: 40262
diff changeset
   211
       Seq.empty)
35568
8fbbfc39508f renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents: 34087
diff changeset
   212
    else
43100
49347c6354b5 parse optional type system specification
blanchet
parents: 43099
diff changeset
   213
      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   214
  end
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   215
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   216
val metis_default_type_syss = [partial_type_sys, full_type_sys]
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   217
val metisFT_type_syss = [full_type_sys]
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 42847
diff changeset
   218
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   219
fun metis_tac [] = generic_metis_tac metis_default_type_syss
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   220
  | metis_tac type_syss = generic_metis_tac type_syss
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   221
38632
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   222
(* Whenever "X" has schematic type variables, we treat "using X by metis" as
43100
49347c6354b5 parse optional type system specification
blanchet
parents: 43099
diff changeset
   223
   "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
38632
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   224
   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
   225
   (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
   226
   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
   227
val has_tvar =
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   228
  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 42847
diff changeset
   229
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   230
fun method type_syss (type_sys, ths) ctxt facts =
43100
49347c6354b5 parse optional type system specification
blanchet
parents: 43099
diff changeset
   231
  let
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   232
    val _ =
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   233
      if type_syss = metisFT_type_syss then
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   234
        legacy_feature "Old 'metisFT' method -- \
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   235
                       \use 'metis (full_types)' instead"
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   236
      else
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   237
        ()
43100
49347c6354b5 parse optional type system specification
blanchet
parents: 43099
diff changeset
   238
    val (schem_facts, nonschem_facts) = List.partition has_tvar facts
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   239
    val type_syss = type_sys |> Option.map single |> the_default type_syss
43100
49347c6354b5 parse optional type system specification
blanchet
parents: 43099
diff changeset
   240
  in
43099
blanchet
parents: 43094
diff changeset
   241
    HEADGOAL (Method.insert_tac nonschem_facts THEN'
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   242
              CHANGED_PROP
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   243
              o generic_metis_tac type_syss ctxt (schem_facts @ ths))
43099
blanchet
parents: 43094
diff changeset
   244
  end
43100
49347c6354b5 parse optional type system specification
blanchet
parents: 43099
diff changeset
   245
43235
blanchet
parents: 43228
diff changeset
   246
fun setup_method (binding, type_syss) =
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   247
  (if type_syss = metis_default_type_syss then
43205
23b81469499f more preparations towards hijacking Metis
blanchet
parents: 43204
diff changeset
   248
     (Args.parens Parse.short_ident
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   249
      >> (fn s => AList.lookup (op =) type_sys_aliases s |> the_default s))
43205
23b81469499f more preparations towards hijacking Metis
blanchet
parents: 43204
diff changeset
   250
     |> Scan.option |> Scan.lift
23b81469499f more preparations towards hijacking Metis
blanchet
parents: 43204
diff changeset
   251
   else
23b81469499f more preparations towards hijacking Metis
blanchet
parents: 43204
diff changeset
   252
     Scan.succeed NONE)
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   253
  -- Attrib.thms >> (METHOD oo method type_syss)
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   254
  |> Method.setup binding
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   255
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   256
val setup =
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   257
  [((@{binding metis}, metis_default_type_syss),
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   258
    "Metis for FOL and HOL problems"),
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43212
diff changeset
   259
   ((@{binding metisFT}, metisFT_type_syss),
43212
050a03afe024 Metis code cleanup
blanchet
parents: 43211
diff changeset
   260
    "Metis for FOL/HOL problems with fully-typed translation")]
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 42847
diff changeset
   261
  |> fold (uncurry setup_method)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   262
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   263
end;