author | blanchet |
Tue, 04 Feb 2014 01:35:48 +0100 | |
changeset 55315 | 54b0352fb46d |
parent 55285 | e88ad20035f4 |
child 55520 | f6fc6d5339f1 |
permissions | -rw-r--r-- |
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 | 2 |
Author: Kong W. Susanto, Cambridge University Computer Laboratory |
3 |
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
|
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 | 6 |
|
29266 | 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 |
54756 | 16 |
val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic |
45521 | 17 |
val metis_lam_transs : string list |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
18 |
val parse_metis_options : (string list option * string option) parser |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
19 |
val setup : theory -> theory |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
20 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
21 |
|
44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
44634
diff
changeset
|
22 |
structure Metis_Tactic : METIS_TACTIC = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
23 |
struct |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
24 |
|
46320 | 25 |
open ATP_Problem_Generate |
26 |
open ATP_Proof_Reconstruct |
|
27 |
open Metis_Generate |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
28 |
open Metis_Reconstruct |
35826 | 29 |
|
54756 | 30 |
val new_skolem = Attrib.setup_config_bool @{binding metis_new_skolem} (K false) |
31 |
val advisory_simp = Attrib.setup_config_bool @{binding metis_advisory_simp} (K true) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
32 |
|
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset
|
33 |
(* 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
|
34 |
fun have_common_thm ths1 ths2 = |
54756 | 35 |
exists (member (Term.aconv_untyped o pairself prop_of) ths1) (map Meson.make_meta_clause ths2) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
36 |
|
32956 | 37 |
(*Determining which axiom clauses are actually used*) |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
38 |
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) |
43128 | 39 |
| used_axioms _ _ = NONE |
24855 | 40 |
|
43129 | 41 |
(* Lightweight predicate type information comes in two flavors, "t = t'" and |
42 |
"t => t'", where "t" and "t'" are the same term modulo type tags. |
|
43 |
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
|
44 |
"t => t". Type tag idempotence is also handled this way. *) |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset
|
45 |
fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth = |
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset
|
46 |
let val thy = Proof_Context.theory_of ctxt in |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset
|
47 |
case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of |
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset
|
48 |
Const (@{const_name HOL.eq}, _) $ _ $ t => |
44408
30ea62ab4f16
made reconstruction of type tag equalities "\?x = \?x" reliable
blanchet
parents:
44402
diff
changeset
|
49 |
let |
30ea62ab4f16
made reconstruction of type tag equalities "\?x = \?x" reliable
blanchet
parents:
44402
diff
changeset
|
50 |
val ct = cterm_of thy t |
30ea62ab4f16
made reconstruction of type tag equalities "\?x = \?x" reliable
blanchet
parents:
44402
diff
changeset
|
51 |
val cT = ctyp_of_term ct |
30ea62ab4f16
made reconstruction of type tag equalities "\?x = \?x" reliable
blanchet
parents:
44402
diff
changeset
|
52 |
in refl |> Drule.instantiate' [SOME cT] [SOME ct] end |
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset
|
53 |
| 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
|
54 |
(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
|
55 |
|> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
56 |
| _ => raise Fail "expected reflexive or trivial clause" |
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset
|
57 |
end |
43129 | 58 |
|> Meson.make_meta_clause |
59 |
||
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset
|
60 |
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
|
61 |
let |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
62 |
val thy = Proof_Context.theory_of ctxt |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54500
diff
changeset
|
63 |
val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN rtac refl 1 |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset
|
64 |
val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
65 |
val ct = cterm_of thy (HOLogic.mk_Trueprop t) |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54756
diff
changeset
|
66 |
in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
67 |
|
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
|
68 |
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
|
69 |
| 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
|
70 |
| 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
|
71 |
| 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
|
72 |
| 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
|
73 |
|
45569
eb30a5490543
wrap lambdas earlier, to get more control over beta/eta
blanchet
parents:
45568
diff
changeset
|
74 |
fun introduce_lam_wrappers ctxt th = |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
75 |
if Meson_Clausify.is_quasi_lambda_free (prop_of th) then |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
76 |
th |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
77 |
else |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
78 |
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
|
79 |
val thy = Proof_Context.theory_of ctxt |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
80 |
fun conv first ctxt ct = |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
81 |
if Meson_Clausify.is_quasi_lambda_free (term_of ct) then |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
82 |
Thm.reflexive ct |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
83 |
else case term_of ct of |
45883 | 84 |
Abs (_, _, u) => |
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
|
85 |
if first then |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
86 |
case add_vars_and_frees u [] of |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
87 |
[] => |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
88 |
Conv.abs_conv (conv false o snd) ctxt ct |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
89 |
|> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI}) |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
90 |
| v :: _ => |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
91 |
Abs (Name.uu, fastype_of v, abstract_over (v, term_of ct)) $ v |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
92 |
|> cterm_of thy |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
93 |
|> Conv.comb_conv (conv true ctxt) |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
94 |
else |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
95 |
Conv.abs_conv (conv false o snd) ctxt ct |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
96 |
| Const (@{const_name Meson.skolem}, _) $ _ => Thm.reflexive ct |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
97 |
| _ => Conv.comb_conv (conv true ctxt) ct |
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
|
98 |
val eq_th = conv true ctxt (cprop_of th) |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
99 |
(* 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
|
100 |
so that "Thm.equal_elim" works below. *) |
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 |
val t0 $ _ $ t2 = prop_of eq_th |
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
blanchet
parents:
45569
diff
changeset
|
102 |
val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54756
diff
changeset
|
103 |
val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (rtac 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
|
104 |
in Thm.equal_elim eq_th' th end |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
105 |
|
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
|
106 |
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
|
107 |
{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
|
108 |
orderLiterals = Metis_Clause.UnsignedLiteralOrder, |
39450
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
109 |
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
|
110 |
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
|
111 |
{clause = clause_params ordering, |
39450
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
112 |
prefactor = #prefactor Metis_Active.default, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
113 |
postfactor = #postfactor Metis_Active.default} |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
114 |
val waiting_params = |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
115 |
{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
|
116 |
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
|
117 |
literalsWeight = 0.01, |
39450
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
118 |
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
|
119 |
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
|
120 |
{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
|
121 |
|
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 |
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
|
123 |
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
|
124 |
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
|
125 |
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
|
126 |
fun precedence p = |
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 |
case int_ord (pairself weight p) of |
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
|
128 |
EQUAL => #precedence Metis_KnuthBendixOrder.default p |
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 |
| ord => ord |
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
|
130 |
in {weight = weight, precedence = precedence} end |
37573 | 131 |
|
55285 | 132 |
fun metis_call type_enc lam_trans = |
133 |
let |
|
134 |
val type_enc = |
|
135 |
(case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of |
|
136 |
[alias] => alias |
|
137 |
| _ => type_enc) |
|
138 |
val opts = |
|
139 |
[] |> type_enc <> partial_typesN ? cons type_enc |
|
140 |
|> lam_trans <> default_metis_lam_trans ? cons lam_trans |
|
141 |
in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end |
|
142 |
||
50875
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
143 |
exception METIS_UNPROVABLE of unit |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
144 |
|
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
145 |
(* Main function to start Metis proof and reconstruction *) |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
146 |
fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 = |
42361 | 147 |
let val thy = Proof_Context.theory_of ctxt |
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
|
148 |
val new_skolem = |
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
|
149 |
Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy) |
46365 | 150 |
val do_lams = |
151 |
(lam_trans = liftingN orelse lam_trans = lam_liftingN) |
|
152 |
? introduce_lam_wrappers ctxt |
|
35826 | 153 |
val th_cls_pairs = |
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset
|
154 |
map2 (fn j => fn th => |
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset
|
155 |
(Thm.get_name_hint 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
|
156 |
th |> Drule.eta_contraction_rule |
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
|
157 |
|> Meson_Clausify.cnf_axiom ctxt new_skolem |
46365 | 158 |
(lam_trans = combsN) j |
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
|
159 |
||> map do_lams)) |
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset
|
160 |
(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
|
161 |
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
|
162 |
val dischargers = map (fst o snd) th_cls_pairs |
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
|
163 |
val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
164 |
val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
165 |
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
44411
e3629929b171
change Metis's default settings if type information axioms are generated
blanchet
parents:
44408
diff
changeset
|
166 |
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset
|
167 |
val type_enc = type_enc_of_string Strict type_enc |
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
|
168 |
val (sym_tab, axioms, ord_info, concealed) = |
45514 | 169 |
prepare_metis_problem ctxt type_enc lam_trans cls ths |
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset
|
170 |
fun get_isa_thm mth Isa_Reflexive_or_Trivial = |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset
|
171 |
reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
172 |
| get_isa_thm mth Isa_Lambda_Lifted = |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset
|
173 |
lam_lifted_of_metis ctxt type_enc sym_tab concealed mth |
45569
eb30a5490543
wrap lambdas earlier, to get more control over beta/eta
blanchet
parents:
45568
diff
changeset
|
174 |
| get_isa_thm _ (Isa_Raw ith) = ith |
eb30a5490543
wrap lambdas earlier, to get more control over beta/eta
blanchet
parents:
45568
diff
changeset
|
175 |
val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) |
45559 | 176 |
val _ = trace_msg ctxt (fn () => "ISABELLE CLAUSES") |
177 |
val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms |
|
178 |
val _ = trace_msg ctxt (fn () => "METIS CLAUSES") |
|
179 |
val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms |
|
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
180 |
val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") |
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
|
181 |
val 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
|
182 |
if Config.get ctxt advisory_simp then |
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
|
183 |
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
|
184 |
else |
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
|
185 |
Metis_KnuthBendixOrder.default |
50875
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
186 |
fun fall_back () = |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
187 |
(verbose_warning ctxt |
55257 | 188 |
("Falling back on " ^ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "..."); |
50875
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
189 |
FOL_SOLVE fallback_type_encs lam_trans ctxt cls ths0) |
32956 | 190 |
in |
50875
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
191 |
(case filter (fn t => prop_of t aconv @{prop False}) cls of |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
192 |
false_th :: _ => [false_th RS @{thm FalseE}] |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
193 |
| [] => |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
194 |
case Metis_Resolution.new (resolution_params ordering) |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
195 |
{axioms = axioms |> map fst, conjecture = []} |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
196 |
|> Metis_Resolution.loop of |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
197 |
Metis_Resolution.Contradiction mth => |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
198 |
let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
199 |
Metis_Thm.toString mth) |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
200 |
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
201 |
(*add constraints arising from converting goal to clause form*) |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
202 |
val proof = Metis_Proof.proof mth |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
203 |
val result = |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
204 |
axioms |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
205 |
|> fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
206 |
val used = proof |> map_filter (used_axioms axioms) |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
207 |
val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
208 |
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
209 |
val names = th_cls_pairs |> map fst |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
210 |
val used_names = |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
211 |
th_cls_pairs |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
212 |
|> map_filter (fn (name, (_, cls)) => |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
213 |
if have_common_thm used cls then SOME name |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
214 |
else NONE) |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
215 |
val unused_names = names |> subtract (op =) used_names |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
216 |
in |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
217 |
if not (null cls) andalso not (have_common_thm used cls) then |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
218 |
verbose_warning ctxt "The assumptions are inconsistent" |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
219 |
else |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
220 |
(); |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
221 |
if not (null unused_names) then |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
222 |
"Unused theorems: " ^ commas_quote unused_names |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
223 |
|> verbose_warning ctxt |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
224 |
else |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
225 |
(); |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
226 |
case result of |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
227 |
(_,ith)::_ => |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
228 |
(trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
229 |
[discharge_skolem_premises ctxt dischargers ith]) |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
230 |
| _ => (trace_msg ctxt (fn () => "Metis: No result"); []) |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
231 |
end |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
232 |
| Metis_Resolution.Satisfiable _ => |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
233 |
(trace_msg ctxt (fn () => |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
234 |
"Metis: No first-order proof with the supplied lemmas"); |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
235 |
raise METIS_UNPROVABLE ())) |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
236 |
handle METIS_UNPROVABLE () => |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
237 |
(case fallback_type_encs of |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
238 |
[] => [] |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
239 |
| _ => fall_back ()) |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
240 |
| METIS_RECONSTRUCT (loc, msg) => |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
241 |
(case fallback_type_encs of |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
242 |
[] => |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
243 |
(verbose_warning ctxt |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
244 |
("Failed to replay Metis proof\n" ^ loc ^ ": " ^ msg); []) |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset
|
245 |
| _ => fall_back ()) |
42733
01ef1c3d9cfd
more robust exception handling in Metis (also works if there are several subgoals)
blanchet
parents:
42650
diff
changeset
|
246 |
end |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
247 |
|
45508 | 248 |
fun neg_clausify ctxt combinators = |
38028 | 249 |
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
|
250 |
#> Meson.make_clauses_unsorted ctxt |
55236 | 251 |
#> combinators ? map (Meson_Clausify.introduce_combinators_in_theorem ctxt) |
38028 | 252 |
#> Meson.finish_cnf |
253 |
||
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
|
254 |
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
|
255 |
(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
|
256 |
(Logic.prems_of_goal (prop_of st0) 1) then |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50875
diff
changeset
|
257 |
Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex} ctxt) 1 |
55239 | 258 |
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
|
259 |
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
|
260 |
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
|
261 |
|
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
262 |
fun generic_metis_tac type_encs lam_trans ctxt ths i st0 = |
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
263 |
let |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
264 |
val _ = trace_msg ctxt (fn () => |
55315 | 265 |
"Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
266 |
val type_encs = type_encs |> maps unalias_type_enc |
55315 | 267 |
fun tac clause = resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1 |
32956 | 268 |
in |
54914
25212efcd0de
removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabelle-metis-proof-state-contains-the-universal-sort/20785045#20785045)
blanchet
parents:
54883
diff
changeset
|
269 |
Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt (lam_trans = combsN))) tac ctxt i st0 |
32956 | 270 |
end |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
271 |
|
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
272 |
fun metis_tac [] = generic_metis_tac partial_type_encs |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
273 |
| metis_tac type_encs = generic_metis_tac type_encs |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
274 |
|
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
275 |
(* Whenever "X" has schematic type variables, we treat "using X by metis" as |
43100 | 276 |
"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
|
277 |
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
|
278 |
(in the rare and subtle case where a proof relied on extensionality not being |
38994 | 279 |
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
|
280 |
val has_tvar = |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
281 |
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
|
282 |
|
55315 | 283 |
fun metis_method ((override_type_encs, lam_trans), ths) ctxt facts = |
43100 | 284 |
let |
285 |
val (schem_facts, nonschem_facts) = List.partition has_tvar facts |
|
55315 | 286 |
val type_encs = override_type_encs |> the_default partial_type_encs |
54500 | 287 |
val lam_trans = lam_trans |> the_default default_metis_lam_trans |
43100 | 288 |
in |
43099 | 289 |
HEADGOAL (Method.insert_tac nonschem_facts THEN' |
54756 | 290 |
CHANGED_PROP o generic_metis_tac type_encs lam_trans ctxt (schem_facts @ ths)) |
43099 | 291 |
end |
43100 | 292 |
|
46365 | 293 |
val metis_lam_transs = [hide_lamsN, liftingN, combsN] |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
294 |
|
45578 | 295 |
fun set_opt _ x NONE = SOME x |
296 |
| set_opt get x (SOME x0) = |
|
55315 | 297 |
error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x) ^ ".") |
54756 | 298 |
|
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
299 |
fun consider_opt s = |
54756 | 300 |
if member (op =) metis_lam_transs s then apsnd (set_opt I s) else apfst (set_opt hd [s]) |
45514 | 301 |
|
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
302 |
val parse_metis_options = |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
303 |
Scan.optional |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
304 |
(Args.parens (Parse.short_ident |
46949 | 305 |
-- Scan.option (@{keyword ","} |-- Parse.short_ident)) |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
306 |
>> (fn (s, s') => |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
307 |
(NONE, NONE) |> consider_opt s |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
308 |
|> (case s' of SOME s' => consider_opt s' | _ => I))) |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
309 |
(NONE, NONE) |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
310 |
|
32956 | 311 |
val setup = |
55315 | 312 |
Method.setup @{binding metis} |
313 |
(Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo metis_method)) |
|
314 |
"Metis for FOL and HOL problems" |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
315 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
316 |
end; |