author | blanchet |
Mon, 27 Sep 2010 12:00:53 +0200 | |
changeset 39721 | 76a61ca09d5d |
parent 39720 | 0b93a954da4f |
child 39886 | 8a9f0c97d550 |
permissions | -rw-r--r-- |
35826 | 1 |
(* Title: HOL/Tools/Sledgehammer/metis_tactics.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 |
|
35826 | 10 |
signature METIS_TACTICS = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
11 |
sig |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
12 |
val trace : bool Unsynchronized.ref |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
13 |
val type_lits : bool Config.T |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
14 |
val metis_tac : Proof.context -> thm list -> int -> tactic |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
15 |
val metisF_tac : Proof.context -> thm list -> int -> tactic |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
16 |
val metisFT_tac : Proof.context -> thm list -> int -> tactic |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
17 |
val setup : theory -> theory |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
18 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
19 |
|
35826 | 20 |
structure Metis_Tactics : METIS_TACTICS = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
21 |
struct |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
22 |
|
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39450
diff
changeset
|
23 |
open Metis_Translate |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
24 |
open Metis_Reconstruct |
35826 | 25 |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
26 |
fun trace_msg msg = if !trace then tracing (msg ()) else () |
32955 | 27 |
|
36001 | 28 |
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
29 |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
30 |
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
31 |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
32 |
fun have_common_thm ths1 ths2 = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
33 |
exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
34 |
|
32956 | 35 |
(*Determining which axiom clauses are actually used*) |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
36 |
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) |
32994 | 37 |
| used_axioms _ _ = NONE; |
24855 | 38 |
|
39450
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
39 |
val clause_params = |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
40 |
{ordering = Metis_KnuthBendixOrder.default, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
41 |
orderLiterals = Metis_Clause.UnsignedLiteralOrder, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
42 |
orderTerms = true} |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
43 |
val active_params = |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
44 |
{clause = clause_params, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
45 |
prefactor = #prefactor Metis_Active.default, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
46 |
postfactor = #postfactor Metis_Active.default} |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
47 |
val waiting_params = |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
48 |
{symbolsWeight = 1.0, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
49 |
variablesWeight = 0.0, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
50 |
literalsWeight = 0.0, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
51 |
models = []} |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
52 |
val resolution_params = {active = active_params, waiting = waiting_params} |
37573 | 53 |
|
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
54 |
(* Main function to start Metis proof and reconstruction *) |
32956 | 55 |
fun FOL_SOLVE mode ctxt cls ths0 = |
56 |
let val thy = ProofContext.theory_of ctxt |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
57 |
val type_lits = Config.get ctxt type_lits |
35826 | 58 |
val th_cls_pairs = |
39720
0b93a954da4f
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
blanchet
parents:
39594
diff
changeset
|
59 |
map (fn th => (Thm.get_name_hint th, |
39721 | 60 |
Meson_Clausifier.meson_cnf_axiom thy th)) ths0 |
32956 | 61 |
val ths = maps #2 th_cls_pairs |
62 |
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
|
63 |
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls |
|
64 |
val _ = trace_msg (fn () => "THEOREM CLAUSES") |
|
65 |
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
66 |
val (mode, {axioms, tfrees, skolems}) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
67 |
build_logic_map mode ctxt type_lits cls ths |
32956 | 68 |
val _ = if null tfrees then () |
69 |
else (trace_msg (fn () => "TFREE CLAUSES"); |
|
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
70 |
app (fn TyLitFree ((s, _), (s', _)) => |
37573 | 71 |
trace_msg (fn _ => s ^ "(" ^ s' ^ ")")) tfrees) |
32956 | 72 |
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") |
73 |
val thms = map #1 axioms |
|
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
74 |
val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms |
32956 | 75 |
val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode) |
76 |
val _ = trace_msg (fn () => "START METIS PROVE PROCESS") |
|
77 |
in |
|
33317 | 78 |
case filter (is_false o prop_of) cls of |
32956 | 79 |
false_th::_ => [false_th RS @{thm FalseE}] |
80 |
| [] => |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
81 |
case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []} |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
82 |
|> Metis_Resolution.loop of |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
83 |
Metis_Resolution.Contradiction mth => |
32956 | 84 |
let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^ |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
85 |
Metis_Thm.toString mth) |
32956 | 86 |
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt |
87 |
(*add constraints arising from converting goal to clause form*) |
|
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
88 |
val proof = Metis_Proof.proof mth |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
89 |
val result = fold (replay_one_inference ctxt' mode skolems) proof axioms |
32956 | 90 |
and used = map_filter (used_axioms axioms) proof |
91 |
val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") |
|
92 |
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used |
|
33305 | 93 |
val unused = th_cls_pairs |> map_filter (fn (name, cls) => |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
94 |
if have_common_thm used cls then NONE else SOME name) |
32956 | 95 |
in |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
96 |
if not (null cls) andalso not (have_common_thm used cls) then |
36383 | 97 |
warning "Metis: The assumptions are inconsistent." |
98 |
else |
|
99 |
(); |
|
100 |
if not (null unused) then |
|
36230
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset
|
101 |
warning ("Metis: Unused theorems: " ^ commas_quote unused |
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset
|
102 |
^ ".") |
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset
|
103 |
else |
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset
|
104 |
(); |
32956 | 105 |
case result of |
106 |
(_,ith)::_ => |
|
36230
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset
|
107 |
(trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); |
32956 | 108 |
[ith]) |
38097
5e4ad2df09f3
revert exception throwing in FOL_SOLVE, since they're not caught anyway
blanchet
parents:
38028
diff
changeset
|
109 |
| _ => (trace_msg (fn () => "Metis: No result"); []) |
32956 | 110 |
end |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
111 |
| Metis_Resolution.Satisfiable _ => |
32956 | 112 |
(trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied"); |
38097
5e4ad2df09f3
revert exception throwing in FOL_SOLVE, since they're not caught anyway
blanchet
parents:
38028
diff
changeset
|
113 |
[]) |
32956 | 114 |
end; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
115 |
|
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
116 |
(* Extensionalize "th", because that makes sense and that's what Sledgehammer |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
117 |
does, but also keep an unextensionalized version of "th" for backward |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
118 |
compatibility. *) |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
119 |
fun also_extensionalize_theorem th = |
39720
0b93a954da4f
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
blanchet
parents:
39594
diff
changeset
|
120 |
let val th' = Meson_Clausifier.extensionalize_theorem th in |
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
121 |
if Thm.eq_thm (th, th') then [th] |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
122 |
else th :: Meson.make_clauses_unsorted [th'] |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
123 |
end |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
124 |
|
38028 | 125 |
val neg_clausify = |
126 |
single |
|
127 |
#> Meson.make_clauses_unsorted |
|
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
128 |
#> maps also_extensionalize_theorem |
39720
0b93a954da4f
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
blanchet
parents:
39594
diff
changeset
|
129 |
#> map Meson_Clausifier.introduce_combinators_in_theorem |
38028 | 130 |
#> Meson.finish_cnf |
131 |
||
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
|
132 |
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
|
133 |
(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
|
134 |
(Logic.prems_of_goal (prop_of st0) 1) then |
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
|
135 |
cnf.cnfx_rewrite_tac ctxt 1 |
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
|
136 |
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
|
137 |
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
|
138 |
|
38652
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset
|
139 |
val type_has_top_sort = |
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset
|
140 |
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) |
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset
|
141 |
|
39560
c13b4589fddf
preprocess "Ex" before doing clausification in Metis;
blanchet
parents:
39550
diff
changeset
|
142 |
val preproc_ss = |
c13b4589fddf
preprocess "Ex" before doing clausification in Metis;
blanchet
parents:
39550
diff
changeset
|
143 |
HOL_basic_ss addsimps @{thms all_simps[symmetric] ex_simps[symmetric]} |
39548
b96941dddd04
preprocess "All" before doing clausification in Metis;
blanchet
parents:
39497
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 |
fun generic_metis_tac mode ctxt ths i st0 = |
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
146 |
let |
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
147 |
val _ = trace_msg (fn () => |
32956 | 148 |
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
149 |
in |
|
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37625
diff
changeset
|
150 |
if exists_type type_has_top_sort (prop_of st0) then |
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
151 |
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) |
35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents:
34087
diff
changeset
|
152 |
else |
39594
624d6c0e220d
revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
blanchet
parents:
39560
diff
changeset
|
153 |
Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) |
624d6c0e220d
revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
blanchet
parents:
39560
diff
changeset
|
154 |
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) |
624d6c0e220d
revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
blanchet
parents:
39560
diff
changeset
|
155 |
ctxt i st0 |
32956 | 156 |
end |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
157 |
|
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
158 |
val metis_tac = generic_metis_tac HO |
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
159 |
val metisF_tac = generic_metis_tac FO |
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
160 |
val metisFT_tac = generic_metis_tac FT |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
161 |
|
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
162 |
(* Whenever "X" has schematic type variables, we treat "using X by metis" as |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
163 |
"by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables. |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
164 |
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
|
165 |
(in the rare and subtle case where a proof relied on extensionality not being |
38994 | 166 |
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
|
167 |
val has_tvar = |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
168 |
exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of |
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
169 |
fun method name mode = |
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
170 |
Method.setup name (Attrib.thms >> (fn ths => fn ctxt => |
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
171 |
METHOD (fn facts => |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
172 |
let |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
173 |
val (schem_facts, nonschem_facts) = |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
174 |
List.partition has_tvar facts |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
175 |
in |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
176 |
HEADGOAL (Method.insert_tac nonschem_facts THEN' |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
177 |
CHANGED_PROP |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
178 |
o generic_metis_tac mode ctxt (schem_facts @ ths)) |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
179 |
end))) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
180 |
|
32956 | 181 |
val setup = |
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
182 |
type_lits_setup |
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
183 |
#> method @{binding metis} HO "Metis for FOL/HOL problems" |
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
184 |
#> method @{binding metisF} FO "Metis for FOL problems" |
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
185 |
#> method @{binding metisFT} FT |
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
186 |
"Metis for FOL/HOL problems with fully-typed translation" |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
187 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
188 |
end; |