src/HOL/Tools/Metis/metis_tactic.ML
author wenzelm
Mon, 12 Aug 2019 15:44:41 +0200
changeset 70513 dc749e0dc6b2
parent 70489 12d1e6e2c1d0
child 70514 7a63b16c53c4
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
44651
5d6a11e166cf renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents: 44634
diff changeset
     1
(*  Title:      HOL/Tools/Metis/metis_tactic.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
44651
5d6a11e166cf renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents: 44634
diff changeset
    10
signature METIS_TACTIC =
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
50705
0e943b33d907 use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
blanchet
parents: 50694
diff changeset
    14
  val new_skolem : bool Config.T
47039
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
    15
  val advisory_simp : bool Config.T
55521
241c6a2fdda1 added a version of the Metis tactic that returns the unused facts
blanchet
parents: 55520
diff changeset
    16
  val metis_tac_unused : string list -> string -> Proof.context -> thm list -> int -> thm ->
241c6a2fdda1 added a version of the Metis tactic that returns the unused facts
blanchet
parents: 55520
diff changeset
    17
    thm list * thm Seq.seq
54756
blanchet
parents: 54742
diff changeset
    18
  val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic
61302
9f9b088d8824 export proof method in signature
blanchet
parents: 61268
diff changeset
    19
  val metis_method : (string list option * string option) * thm list -> Proof.context -> thm list ->
62219
dbac573b27e7 preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents: 61841
diff changeset
    20
    tactic
45521
0cd6e59bd0b5 give each time slice its own lambda translation
blanchet
parents: 45519
diff changeset
    21
  val metis_lam_transs : string list
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
    22
  val parse_metis_options : (string list option * string option) parser
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    23
end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    24
44651
5d6a11e166cf renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents: 44634
diff changeset
    25
structure Metis_Tactic : METIS_TACTIC =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    26
struct
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    27
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    28
open ATP_Problem_Generate
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    29
open ATP_Proof_Reconstruct
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    30
open Metis_Generate
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
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67379
diff changeset
    33
val new_skolem = Attrib.setup_config_bool \<^binding>\<open>metis_new_skolem\<close> (K false)
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67379
diff changeset
    34
val advisory_simp = Attrib.setup_config_bool \<^binding>\<open>metis_advisory_simp\<close> (K true)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    35
43134
0c82e00ba63e make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents: 43133
diff changeset
    36
(* Designed to work also with monomorphic instances of polymorphic theorems. *)
60358
aebfbcab1eb8 clarified context;
wenzelm
parents: 59632
diff changeset
    37
fun have_common_thm ctxt ths1 ths2 =
aebfbcab1eb8 clarified context;
wenzelm
parents: 59632
diff changeset
    38
  exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1)
aebfbcab1eb8 clarified context;
wenzelm
parents: 59632
diff changeset
    39
    (map (Meson.make_meta_clause ctxt) ths2)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    40
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    41
(*Determining which axiom clauses are actually used*)
39419
c9accfd621a5 "Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents: 39376
diff changeset
    42
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
43128
a19826080596 tuned names
blanchet
parents: 43103
diff changeset
    43
  | used_axioms _ _ = NONE
24855
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
    44
43129
4301f1c123d6 support lightweight tags in new Metis
blanchet
parents: 43128
diff changeset
    45
(* Lightweight predicate type information comes in two flavors, "t = t'" and
4301f1c123d6 support lightweight tags in new Metis
blanchet
parents: 43128
diff changeset
    46
   "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
    47
   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
    48
   "t => t". Type tag idempotence is also handled this way. *)
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51717
diff changeset
    49
fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth =
59632
5980e75a204e clarified context;
wenzelm
parents: 59621
diff changeset
    50
  (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67379
diff changeset
    51
    Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ t =>
70489
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    52
      let
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    53
        val ct = Thm.cterm_of ctxt t
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    54
        val cT = Thm.ctyp_of_cterm ct
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    55
      in refl |> Thm.instantiate' [SOME cT] [SOME ct] end
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67379
diff changeset
    56
  | Const (\<^const_name>\<open>disj\<close>, _) $ t1 $ t2 =>
70489
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    57
      (if can HOLogic.dest_not t1 then t2 else t1)
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    58
      |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
59632
5980e75a204e clarified context;
wenzelm
parents: 59621
diff changeset
    59
  | _ => raise Fail "expected reflexive or trivial clause")
60358
aebfbcab1eb8 clarified context;
wenzelm
parents: 59632
diff changeset
    60
  |> Meson.make_meta_clause ctxt
43129
4301f1c123d6 support lightweight tags in new Metis
blanchet
parents: 43128
diff changeset
    61
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51717
diff changeset
    62
fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45508
diff changeset
    63
  let
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
    64
    val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac ctxt [refl] 1
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51717
diff changeset
    65
    val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
59632
5980e75a204e clarified context;
wenzelm
parents: 59621
diff changeset
    66
    val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
70489
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    67
  in
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    68
    Goal.prove_internal ctxt [] ct (K tac)
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    69
    |> Meson.make_meta_clause ctxt
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    70
  end
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45508
diff changeset
    71
45570
6d95a66cce00 pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents: 45569
diff changeset
    72
fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
6d95a66cce00 pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents: 45569
diff changeset
    73
  | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t
6d95a66cce00 pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents: 45569
diff changeset
    74
  | add_vars_and_frees (t as Var _) = insert (op =) t
6d95a66cce00 pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents: 45569
diff changeset
    75
  | add_vars_and_frees (t as Free _) = insert (op =) t
6d95a66cce00 pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents: 45569
diff changeset
    76
  | add_vars_and_frees _ = I
6d95a66cce00 pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents: 45569
diff changeset
    77
45569
eb30a5490543 wrap lambdas earlier, to get more control over beta/eta
blanchet
parents: 45568
diff changeset
    78
fun introduce_lam_wrappers ctxt th =
70489
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    79
  if Meson_Clausify.is_quasi_lambda_free (Thm.prop_of th) then th
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45508
diff changeset
    80
  else
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45508
diff changeset
    81
    let
45570
6d95a66cce00 pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents: 45569
diff changeset
    82
      fun conv first ctxt ct =
70489
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    83
        if Meson_Clausify.is_quasi_lambda_free (Thm.term_of ct) then Thm.reflexive ct
57408
39b3562e9edc tuned whitespace and parentheses
blanchet
parents: 57263
diff changeset
    84
        else
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
    85
          (case Thm.term_of ct of
57408
39b3562e9edc tuned whitespace and parentheses
blanchet
parents: 57263
diff changeset
    86
            Abs (_, _, u) =>
70489
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    87
              if first then
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    88
                (case add_vars_and_frees u [] of
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    89
                  [] =>
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    90
                  Conv.abs_conv (conv false o snd) ctxt ct
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    91
                  |> (fn th => Meson.first_order_resolve ctxt th @{thm Metis.eq_lambdaI})
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    92
                | v :: _ =>
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    93
                    Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    94
                    |> Thm.cterm_of ctxt
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    95
                    |> Conv.comb_conv (conv true ctxt))
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
    96
              else Conv.abs_conv (conv false o snd) ctxt ct
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67379
diff changeset
    97
          | Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ _ => Thm.reflexive ct
57408
39b3562e9edc tuned whitespace and parentheses
blanchet
parents: 57263
diff changeset
    98
          | _ => Conv.comb_conv (conv true ctxt) ct)
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
    99
      val eq_th = conv true ctxt (Thm.cprop_of th)
45570
6d95a66cce00 pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents: 45569
diff changeset
   100
      (* We replace the equation's left-hand side with a beta-equivalent term
6d95a66cce00 pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents: 45569
diff changeset
   101
         so that "Thm.equal_elim" works below. *)
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   102
      val t0 $ _ $ t2 = Thm.prop_of eq_th
59632
5980e75a204e clarified context;
wenzelm
parents: 59621
diff changeset
   103
      val eq_ct = t0 $ Thm.prop_of th $ t2 |> Thm.cterm_of ctxt
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   104
      val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (resolve_tac ctxt [eq_th] 1))
45570
6d95a66cce00 pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents: 45569
diff changeset
   105
    in Thm.equal_elim eq_th' th end
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45508
diff changeset
   106
47039
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   107
fun clause_params ordering =
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   108
  {ordering = ordering,
44492
a330c0608da8 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents: 44411
diff changeset
   109
   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
39450
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
   110
   orderTerms = true}
47039
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   111
fun active_params ordering =
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   112
  {clause = clause_params ordering,
39450
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
   113
   prefactor = #prefactor Metis_Active.default,
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
   114
   postfactor = #postfactor Metis_Active.default}
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
   115
val waiting_params =
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
   116
  {symbolsWeight = 1.0,
47047
10bece4ac87e more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV")
blanchet
parents: 47045
diff changeset
   117
   variablesWeight = 0.05,
10bece4ac87e more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV")
blanchet
parents: 47045
diff changeset
   118
   literalsWeight = 0.01,
39450
7e9879fbb7c5 supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents: 39419
diff changeset
   119
   models = []}
47039
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   120
fun resolution_params ordering =
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   121
  {active = active_params ordering, waiting = waiting_params}
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   122
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   123
fun kbo_advisory_simp_ordering ord_info =
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   124
  let
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   125
    fun weight (m, _) =
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   126
      AList.lookup (op =) ord_info (Metis_Name.toString m) |> the_default 1
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   127
    fun precedence p =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58839
diff changeset
   128
      (case int_ord (apply2 weight p) of
47039
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   129
        EQUAL => #precedence Metis_KnuthBendixOrder.default p
57408
39b3562e9edc tuned whitespace and parentheses
blanchet
parents: 57263
diff changeset
   130
      | ord => ord)
47039
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47015
diff changeset
   131
  in {weight = weight, precedence = precedence} end
37573
7f987e8582a7 fewer dependencies
blanchet
parents: 37572
diff changeset
   132
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55257
diff changeset
   133
fun metis_call type_enc lam_trans =
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55257
diff changeset
   134
  let
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55257
diff changeset
   135
    val type_enc =
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55257
diff changeset
   136
      (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55257
diff changeset
   137
        [alias] => alias
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55257
diff changeset
   138
      | _ => type_enc)
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55257
diff changeset
   139
    val opts =
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55257
diff changeset
   140
      [] |> type_enc <> partial_typesN ? cons type_enc
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55257
diff changeset
   141
         |> lam_trans <> default_metis_lam_trans ? cons lam_trans
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55257
diff changeset
   142
  in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55257
diff changeset
   143
50875
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 50705
diff changeset
   144
exception METIS_UNPROVABLE of unit
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 50705
diff changeset
   145
37516
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   146
(* Main function to start Metis proof and reconstruction *)
70488
c7ef6685c943 clarified signature: fewer warnings in ML IDE;
wenzelm
parents: 69593
diff changeset
   147
fun FOL_SOLVE unused type_encs lam_trans ctxt cls ths0 =
70489
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   148
  let
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   149
    val thy = Proof_Context.theory_of ctxt
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   150
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   151
    val new_skolem = Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy)
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   152
    val do_lams =
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   153
      (lam_trans = liftingN orelse lam_trans = lam_liftingN) ? introduce_lam_wrappers ctxt
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   154
    val th_cls_pairs =
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   155
      map2 (fn j => fn th =>
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   156
        (Thm.get_name_hint th,
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   157
          th
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   158
          |> Drule.eta_contraction_rule
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   159
          |> Meson_Clausify.cnf_axiom ctxt new_skolem (lam_trans = combsN) j
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   160
          ||> map do_lams))
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   161
        (0 upto length ths0 - 1) ths0
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   162
    val ths = maps (snd o snd) th_cls_pairs
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   163
    val dischargers = map (fst o snd) th_cls_pairs
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   164
    val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   165
    val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES")
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   166
    val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   167
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   168
    val type_enc :: fallback_type_encs = type_encs
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   169
    val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   170
    val type_enc = type_enc_of_string Strict type_enc
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   171
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   172
    val (sym_tab, axioms, ord_info, concealed) =
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   173
      generate_metis_problem ctxt type_enc lam_trans cls ths
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   174
    fun get_isa_thm mth Isa_Reflexive_or_Trivial =
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51717
diff changeset
   175
          reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth
70489
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   176
      | get_isa_thm mth Isa_Lambda_Lifted =
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51717
diff changeset
   177
          lam_lifted_of_metis ctxt type_enc sym_tab concealed mth
70489
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   178
      | get_isa_thm _ (Isa_Raw ith) = ith
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   179
    val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   180
    val _ = trace_msg ctxt (K "ISABELLE CLAUSES")
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   181
    val _ = List.app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   182
    val _ = trace_msg ctxt (K "METIS CLAUSES")
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   183
    val _ = List.app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   184
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   185
    val _ = trace_msg ctxt (K "START METIS PROVE PROCESS")
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   186
    val ordering =
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   187
      if Config.get ctxt advisory_simp
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   188
      then kbo_advisory_simp_ordering (ord_info ())
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   189
      else Metis_KnuthBendixOrder.default
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   190
50875
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 50705
diff changeset
   191
    fun fall_back () =
bfb626265782 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents: 50705
diff changeset
   192
      (verbose_warning ctxt
70489
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   193
        ("Falling back on " ^ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "...");
55521
241c6a2fdda1 added a version of the Metis tactic that returns the unused facts
blanchet
parents: 55520
diff changeset
   194
       FOL_SOLVE unused fallback_type_encs lam_trans ctxt cls ths0)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   195
  in
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67379
diff changeset
   196
    (case filter (fn t => Thm.prop_of t aconv \<^prop>\<open>False\<close>) cls of
70489
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   197
      false_th :: _ => [false_th RS @{thm FalseE}]
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   198
    | [] =>
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   199
        (case Metis_Resolution.loop (Metis_Resolution.new (resolution_params ordering)
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   200
            {axioms = axioms |> map fst, conjecture = []}) of
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   201
          Metis_Resolution.Contradiction mth =>
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   202
          let
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   203
            val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ Metis_Thm.toString mth)
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   204
            val ctxt' = fold Variable.declare_constraints (map Thm.prop_of cls) ctxt
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   205
              (*add constraints arising from converting goal to clause form*)
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   206
            val proof = Metis_Proof.proof mth
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   207
            val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   208
            val used = map_filter (used_axioms axioms) proof
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   209
            val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   210
            val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   211
70513
wenzelm
parents: 70489
diff changeset
   212
            val unused_th_cls_pairs = filter_out (have_common_thm ctxt used o #2 o #2) th_cls_pairs
wenzelm
parents: 70489
diff changeset
   213
            val _ = unused := maps (#2 o #2) unused_th_cls_pairs;
70489
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   214
            val _ =
70513
wenzelm
parents: 70489
diff changeset
   215
              if not (null unused_th_cls_pairs) then
wenzelm
parents: 70489
diff changeset
   216
                verbose_warning ctxt ("Unused theorems: " ^ commas_quote (map #1 unused_th_cls_pairs))
70489
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   217
              else ();
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   218
            val _ =
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   219
              if not (null cls) andalso not (have_common_thm ctxt used cls) then
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   220
                verbose_warning ctxt "The assumptions are inconsistent"
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   221
              else ();
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   222
          in
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   223
            (case result of
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   224
              (_, ith) :: _ =>
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   225
                (trace_msg ctxt (fn () => "Success: " ^ Thm.string_of_thm ctxt ith);
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   226
                  [discharge_skolem_premises ctxt dischargers ith])
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   227
            | _ => (trace_msg ctxt (K "Metis: No result"); []))
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   228
          end
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   229
        | Metis_Resolution.Satisfiable _ =>
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   230
            (trace_msg ctxt (K "Metis: No first-order proof with the supplied lemmas");
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   231
              raise METIS_UNPROVABLE ()))
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   232
        handle METIS_UNPROVABLE () => if null fallback_type_encs then [] else fall_back ()
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   233
          | METIS_RECONSTRUCT (loc, msg) =>
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   234
              if null fallback_type_encs then
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   235
                (verbose_warning ctxt ("Failed to replay Metis proof\n" ^ loc ^ ": " ^ msg); [])
12d1e6e2c1d0 tuned whitespace -- slightly more readable;
wenzelm
parents: 70488
diff changeset
   236
              else fall_back ())
42733
01ef1c3d9cfd more robust exception handling in Metis (also works if there are several subgoals)
blanchet
parents: 42650
diff changeset
   237
  end
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   238
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 45042
diff changeset
   239
fun neg_clausify ctxt combinators =
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   240
  single
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43963
diff changeset
   241
  #> Meson.make_clauses_unsorted ctxt
55236
8d61b0aa7a0d proper context for printing;
wenzelm
parents: 54914
diff changeset
   242
  #> combinators ? map (Meson_Clausify.introduce_combinators_in_theorem ctxt)
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   243
  #> Meson.finish_cnf
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   244
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
   245
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
   246
  (if exists (Meson.has_too_many_clauses ctxt)
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   247
             (Logic.prems_of_goal (Thm.prop_of st0) 1) then
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50875
diff changeset
   248
     Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex} ctxt) 1
55239
97921d23ebe3 more standard file/module names;
wenzelm
parents: 55236
diff changeset
   249
     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
   250
   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
   251
     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
   252
55521
241c6a2fdda1 added a version of the Metis tactic that returns the unused facts
blanchet
parents: 55520
diff changeset
   253
fun metis_tac_unused type_encs0 lam_trans ctxt ths i st0 =
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   254
  let
55521
241c6a2fdda1 added a version of the Metis tactic that returns the unused facts
blanchet
parents: 55520
diff changeset
   255
    val unused = Unsynchronized.ref []
55520
f6fc6d5339f1 tuned code
blanchet
parents: 55315
diff changeset
   256
    val type_encs = if null type_encs0 then partial_type_encs else type_encs0
39978
11bfb7e7cc86 added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents: 39964
diff changeset
   257
    val _ = trace_msg ctxt (fn () =>
61268
abe08fb15a12 moved remaining display.ML to more_thm.ML;
wenzelm
parents: 60801
diff changeset
   258
      "Metis called with theorems\n" ^ cat_lines (map (Thm.string_of_thm ctxt) ths))
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   259
    val type_encs = type_encs |> maps unalias_type_enc
55521
241c6a2fdda1 added a version of the Metis tactic that returns the unused facts
blanchet
parents: 55520
diff changeset
   260
    val combs = (lam_trans = combsN)
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   261
    fun tac clause = resolve_tac ctxt (FOL_SOLVE unused type_encs lam_trans ctxt clause ths) 1
55521
241c6a2fdda1 added a version of the Metis tactic that returns the unused facts
blanchet
parents: 55520
diff changeset
   262
    val seq = Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt combs)) tac ctxt i st0
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   263
  in
55521
241c6a2fdda1 added a version of the Metis tactic that returns the unused facts
blanchet
parents: 55520
diff changeset
   264
    (!unused, seq)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   265
  end
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   266
55521
241c6a2fdda1 added a version of the Metis tactic that returns the unused facts
blanchet
parents: 55520
diff changeset
   267
fun metis_tac type_encs lam_trans ctxt ths i = snd o metis_tac_unused type_encs lam_trans ctxt ths i
241c6a2fdda1 added a version of the Metis tactic that returns the unused facts
blanchet
parents: 55520
diff changeset
   268
55520
f6fc6d5339f1 tuned code
blanchet
parents: 55315
diff changeset
   269
(* Whenever "X" has schematic type variables, we treat "using X by metis" as "by (metis X)" to
f6fc6d5339f1 tuned code
blanchet
parents: 55315
diff changeset
   270
   prevent "Subgoal.FOCUS" from freezing the type variables. We don't do it for nonschematic facts
f6fc6d5339f1 tuned code
blanchet
parents: 55315
diff changeset
   271
   "X" because this breaks a few proofs (in the rare and subtle case where a proof relied on
f6fc6d5339f1 tuned code
blanchet
parents: 55315
diff changeset
   272
   extensionality not being applied) and brings few benefits. *)
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   273
val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o Thm.prop_of
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 42847
diff changeset
   274
55315
54b0352fb46d removed legacy 'metisFT' method
blanchet
parents: 55285
diff changeset
   275
fun metis_method ((override_type_encs, lam_trans), ths) ctxt facts =
55520
f6fc6d5339f1 tuned code
blanchet
parents: 55315
diff changeset
   276
  let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in
61841
4d3527b94f2a more general types Proof.method / context_tactic;
wenzelm
parents: 61302
diff changeset
   277
    HEADGOAL (Method.insert_tac ctxt nonschem_facts THEN'
55520
f6fc6d5339f1 tuned code
blanchet
parents: 55315
diff changeset
   278
      CHANGED_PROP o metis_tac (these override_type_encs)
f6fc6d5339f1 tuned code
blanchet
parents: 55315
diff changeset
   279
        (the_default default_metis_lam_trans lam_trans) ctxt (schem_facts @ ths))
43099
blanchet
parents: 43094
diff changeset
   280
  end
43100
49347c6354b5 parse optional type system specification
blanchet
parents: 43099
diff changeset
   281
46365
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46320
diff changeset
   282
val metis_lam_transs = [hide_lamsN, liftingN, combsN]
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   283
45578
66f31d77b05f more robust options
blanchet
parents: 45570
diff changeset
   284
fun set_opt _ x NONE = SOME x
66f31d77b05f more robust options
blanchet
parents: 45570
diff changeset
   285
  | set_opt get x (SOME x0) =
55523
9429e7b5b827 removed final periods in messages for proof methods
blanchet
parents: 55521
diff changeset
   286
    error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x))
54756
blanchet
parents: 54742
diff changeset
   287
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   288
fun consider_opt s =
54756
blanchet
parents: 54742
diff changeset
   289
  if member (op =) metis_lam_transs s then apsnd (set_opt I s) else apfst (set_opt hd [s])
45514
973bb7846505 parse lambda translation option in Metis
blanchet
parents: 45513
diff changeset
   290
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   291
val parse_metis_options =
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   292
  Scan.optional
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67379
diff changeset
   293
      (Args.parens (Args.name -- Scan.option (\<^keyword>\<open>,\<close> |-- Args.name))
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   294
       >> (fn (s, s') =>
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   295
              (NONE, NONE) |> consider_opt s
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   296
                           |> (case s' of SOME s' => consider_opt s' | _ => I)))
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   297
      (NONE, NONE)
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   298
58818
ee85e7b82d00 modernized setup;
wenzelm
parents: 57408
diff changeset
   299
val _ =
ee85e7b82d00 modernized setup;
wenzelm
parents: 57408
diff changeset
   300
  Theory.setup
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67379
diff changeset
   301
    (Method.setup \<^binding>\<open>metis\<close>
58818
ee85e7b82d00 modernized setup;
wenzelm
parents: 57408
diff changeset
   302
      (Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo metis_method))
ee85e7b82d00 modernized setup;
wenzelm
parents: 57408
diff changeset
   303
      "Metis for FOL and HOL problems")
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   304
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   305
end;