author  wenzelm 
Mon, 02 May 2011 16:33:21 +0200  
changeset 42616  92715b528e78 
parent 42552  e155be7125ba 
child 42650  552eae49f97d 
permissions  rwrr 
39958  1 
(* Title: HOL/Tools/Metis/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 
39979
b13515940b53
added "trace_meson" configuration option, replacing oldfashioned reference
blanchet
parents:
39978
diff
changeset

12 
val trace : bool Config.T 
40665
1a65f0c74827
added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents:
40262
diff
changeset

13 
val verbose : bool Config.T 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

14 
val type_lits : bool Config.T 
39891
8e12f1956fcd
"meson_new_skolemizer" > "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
blanchet
parents:
39890
diff
changeset

15 
val new_skolemizer : bool Config.T 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

16 
val metis_tac : Proof.context > thm list > int > tactic 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

17 
val metisF_tac : Proof.context > thm list > int > tactic 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

18 
val metisFT_tac : Proof.context > thm list > int > tactic 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

19 
val setup : theory > theory 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

20 
end 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

21 

35826  22 
structure Metis_Tactics : METIS_TACTICS = 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

23 
struct 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

24 

39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39450
diff
changeset

25 
open Metis_Translate 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

26 
open Metis_Reconstruct 
35826  27 

42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42552
diff
changeset

28 
val type_lits = Attrib.setup_config_bool @{binding metis_type_lits} (K true) 
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42552
diff
changeset

29 
val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

30 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

31 
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

32 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

33 
fun have_common_thm ths1 ths2 = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

34 
exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

35 

32956  36 
(*Determining which axiom clauses are actually used*) 
39419
c9accfd621a5
"Metis." > "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset

37 
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) 
32994  38 
 used_axioms _ _ = NONE; 
24855  39 

39450
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

40 
val clause_params = 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

41 
{ordering = Metis_KnuthBendixOrder.default, 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

42 
orderLiterals = Metis_Clause.UnsignedLiteralOrder, 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

43 
orderTerms = true} 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

44 
val active_params = 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

45 
{clause = clause_params, 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

46 
prefactor = #prefactor Metis_Active.default, 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

47 
postfactor = #postfactor Metis_Active.default} 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

48 
val waiting_params = 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

49 
{symbolsWeight = 1.0, 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

50 
variablesWeight = 0.0, 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

51 
literalsWeight = 0.0, 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

52 
models = []} 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

53 
val resolution_params = {active = active_params, waiting = waiting_params} 
37573  54 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

55 
(* Main function to start Metis proof and reconstruction *) 
32956  56 
fun FOL_SOLVE mode ctxt cls ths0 = 
42361  57 
let val thy = Proof_Context.theory_of ctxt 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

58 
val type_lits = Config.get ctxt type_lits 
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39899
diff
changeset

59 
val new_skolemizer = 
39950  60 
Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) 
35826  61 
val th_cls_pairs = 
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset

62 
map2 (fn j => fn th => 
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset

63 
(Thm.get_name_hint th, 
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39899
diff
changeset

64 
Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) 
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset

65 
(0 upto length ths0  1) ths0 
39887
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

66 
val thss = map (snd o snd) th_cls_pairs 
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset

67 
val dischargers = map (fst o snd) th_cls_pairs 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

68 
val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

69 
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

70 
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

71 
val _ = app (app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th))) thss 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset

72 
val (mode, {axioms, tfrees, old_skolems}) = 
40157  73 
prepare_metis_problem mode ctxt type_lits cls thss 
32956  74 
val _ = if null tfrees then () 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

75 
else (trace_msg ctxt (fn () => "TFREE CLAUSES"); 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset

76 
app (fn TyLitFree ((s, _), (s', _)) => 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

77 
trace_msg ctxt (fn () => s ^ "(" ^ s' ^ ")")) tfrees) 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

78 
val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") 
32956  79 
val thms = map #1 axioms 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

80 
val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

81 
val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode) 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

82 
val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") 
32956  83 
in 
33317  84 
case filter (is_false o prop_of) cls of 
32956  85 
false_th::_ => [false_th RS @{thm FalseE}] 
86 
 [] => 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

87 
case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []} 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

88 
> Metis_Resolution.loop of 
39419
c9accfd621a5
"Metis." > "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset

89 
Metis_Resolution.Contradiction mth => 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

90 
let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ 
39419
c9accfd621a5
"Metis." > "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset

91 
Metis_Thm.toString mth) 
32956  92 
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt 
93 
(*add constraints arising from converting goal to clause form*) 

39419
c9accfd621a5
"Metis." > "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset

94 
val proof = Metis_Proof.proof mth 
42341
5a00af7f4978
removed obsolete Skolem counter in new Skolemizer
blanchet
parents:
42336
diff
changeset

95 
val result = fold (replay_one_inference ctxt' mode old_skolems) 
5a00af7f4978
removed obsolete Skolem counter in new Skolemizer
blanchet
parents:
42336
diff
changeset

96 
proof axioms 
32956  97 
and used = map_filter (used_axioms axioms) proof 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

98 
val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

99 
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used 
39887
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

100 
val unused = th_cls_pairs > map_filter (fn (name, (_, cls)) => 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

101 
if have_common_thm used cls then NONE else SOME name) 
32956  102 
in 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

103 
if not (null cls) andalso not (have_common_thm used cls) then 
40665
1a65f0c74827
added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents:
40262
diff
changeset

104 
verbose_warning ctxt "Metis: The assumptions are inconsistent" 
36383  105 
else 
106 
(); 

107 
if not (null unused) then 

40665
1a65f0c74827
added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents:
40262
diff
changeset

108 
verbose_warning ctxt ("Metis: Unused theorems: " ^ 
1a65f0c74827
added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents:
40262
diff
changeset

109 
commas_quote unused) 
36230
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

110 
else 
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

111 
(); 
32956  112 
case result of 
113 
(_,ith)::_ => 

39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

114 
(trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); 
39887
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

115 
[discharge_skolem_premises ctxt dischargers ith]) 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

116 
 _ => (trace_msg ctxt (fn () => "Metis: No result"); []) 
32956  117 
end 
39419
c9accfd621a5
"Metis." > "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset

118 
 Metis_Resolution.Satisfiable _ => 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

119 
(trace_msg ctxt (fn () => "Metis: No firstorder proof with the lemmas supplied"); 
38097
5e4ad2df09f3
revert exception throwing in FOL_SOLVE, since they're not caught anyway
blanchet
parents:
38028
diff
changeset

120 
[]) 
32956  121 
end; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

122 

38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

123 
(* Extensionalize "th", because that makes sense and that's what Sledgehammer 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

124 
does, but also keep an unextensionalized version of "th" for backward 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

125 
compatibility. *) 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

126 
fun also_extensionalize_theorem th = 
39890  127 
let val th' = Meson_Clausify.extensionalize_theorem th in 
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

128 
if Thm.eq_thm (th, th') then [th] 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

129 
else th :: Meson.make_clauses_unsorted [th'] 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

130 
end 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

131 

38028  132 
val neg_clausify = 
133 
single 

134 
#> Meson.make_clauses_unsorted 

38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

135 
#> maps also_extensionalize_theorem 
39890  136 
#> map Meson_Clausify.introduce_combinators_in_theorem 
38028  137 
#> Meson.finish_cnf 
138 

39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset

139 
fun preskolem_tac ctxt st0 = 
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset

140 
(if exists (Meson.has_too_many_clauses ctxt) 
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset

141 
(Logic.prems_of_goal (prop_of st0) 1) then 
42336
d63d43e85879
improve definitional CNF on goal by moving "not" past the quantifiers
blanchet
parents:
40665
diff
changeset

142 
Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1 
d63d43e85879
improve definitional CNF on goal by moving "not" past the quantifiers
blanchet
parents:
40665
diff
changeset

143 
THEN cnf.cnfx_rewrite_tac ctxt 1 
39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset

144 
else 
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset

145 
all_tac) st0 
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset

146 

38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset

147 
val type_has_top_sort = 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset

148 
exists_subtype (fn TFree (_, []) => true  TVar (_, []) => true  _ => false) 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset

149 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

150 
fun generic_metis_tac mode ctxt ths i st0 = 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

151 
let 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

152 
val _ = trace_msg ctxt (fn () => 
32956  153 
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) 
154 
in 

37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37625
diff
changeset

155 
if exists_type type_has_top_sort (prop_of st0) then 
40665
1a65f0c74827
added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents:
40262
diff
changeset

156 
(verbose_warning ctxt "Metis: Proof state contains the universal sort {}"; 
1a65f0c74827
added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents:
40262
diff
changeset

157 
Seq.empty) 
35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort  {} is the full universal sort;
wenzelm
parents:
34087
diff
changeset

158 
else 
39594
624d6c0e220d
revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
blanchet
parents:
39560
diff
changeset

159 
Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) 
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
40259
diff
changeset

160 
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) 
39594
624d6c0e220d
revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
blanchet
parents:
39560
diff
changeset

161 
ctxt i st0 
42552
e155be7125ba
added a hint to Metis errors suggesting metisFT  it sometimes work
blanchet
parents:
42361
diff
changeset

162 
handle ERROR message => 
e155be7125ba
added a hint to Metis errors suggesting metisFT  it sometimes work
blanchet
parents:
42361
diff
changeset

163 
error (message > mode <> FT 
e155be7125ba
added a hint to Metis errors suggesting metisFT  it sometimes work
blanchet
parents:
42361
diff
changeset

164 
? suffix "\nHint: You might want to try out \ 
e155be7125ba
added a hint to Metis errors suggesting metisFT  it sometimes work
blanchet
parents:
42361
diff
changeset

165 
\\"metisFT\".") 
32956  166 
end 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

167 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

168 
val metis_tac = generic_metis_tac HO 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

169 
val metisF_tac = generic_metis_tac FO 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

170 
val metisFT_tac = generic_metis_tac FT 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

171 

38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

172 
(* Whenever "X" has schematic type variables, we treat "using X by metis" as 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

173 
"by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables. 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

174 
We don't do it for nonschematic facts "X" because this breaks a few proofs 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

175 
(in the rare and subtle case where a proof relied on extensionality not being 
38994  176 
applied) and brings few benefits. *) 
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

177 
val has_tvar = 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

178 
exists_type (exists_subtype (fn TVar _ => true  _ => false)) o prop_of 
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

179 
fun method name mode = 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

180 
Method.setup name (Attrib.thms >> (fn ths => fn ctxt => 
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

181 
METHOD (fn facts => 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

182 
let 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

183 
val (schem_facts, nonschem_facts) = 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

184 
List.partition has_tvar facts 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

185 
in 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

186 
HEADGOAL (Method.insert_tac nonschem_facts THEN' 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

187 
CHANGED_PROP 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

188 
o generic_metis_tac mode ctxt (schem_facts @ ths)) 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

189 
end))) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

190 

32956  191 
val setup = 
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42552
diff
changeset

192 
method @{binding metis} HO "Metis for FOL/HOL problems" 
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

193 
#> method @{binding metisF} FO "Metis for FOL problems" 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

194 
#> method @{binding metisFT} FT 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

195 
"Metis for FOL/HOL problems with fullytyped translation" 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

196 

028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

197 
end; 