author  blanchet 
Tue, 07 Jun 2011 11:12:52 +0200  
changeset 43235  3a8d49bc06e1 
parent 43228  2ed2f092e990 
child 43298  82d4874757df 
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 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset

12 
val metisN : string 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

13 
val full_typesN : string 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

14 
val partial_typesN : string 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

15 
val no_typesN : string 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

16 
val full_type_sys : string 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

17 
val partial_type_sys : string 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

18 
val no_type_sys : string 
39979
b13515940b53
added "trace_meson" configuration option, replacing oldfashioned reference
blanchet
parents:
39978
diff
changeset

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

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

21 
val new_skolemizer : bool Config.T 
43212  22 
val metis_tac : string list > Proof.context > thm list > int > tactic 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

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

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

25 

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

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

28 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43050
diff
changeset

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

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

31 
open Metis_Reconstruct 
35826  32 

43211  33 
val metisN = Binding.qualified_name_of @{binding metis} 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

34 

43205  35 
val full_typesN = "full_types" 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

36 
val partial_typesN = "partial_types" 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

37 
val no_typesN = "no_types" 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset

38 

43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

39 
val full_type_sys = "poly_preds_heavy_query" 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

40 
val partial_type_sys = "poly_args" 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

41 
val no_type_sys = "erased" 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

42 

2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

43 
val type_sys_aliases = 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

44 
[(full_typesN, full_type_sys), 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

45 
(partial_typesN, partial_type_sys), 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

46 
(no_typesN, no_type_sys)] 
43211  47 

43212  48 
fun method_call_for_type_sys type_sys = 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

49 
metisN ^ " (" ^ 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

50 
(case AList.find (op =) type_sys_aliases type_sys of 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

51 
[alias] => alias 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

52 
 _ => type_sys) ^ ")" 
43205  53 

43089  54 
val new_skolemizer = 
55 
Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) 

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

56 

43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

57 
(* Designed to work also with monomorphic instances of polymorphic theorems. *) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

58 
fun have_common_thm ths1 ths2 = 
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

59 
exists (member (untyped_aconv o pairself prop_of) ths1) 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

60 
(map Meson.make_meta_clause ths2) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

61 

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

63 
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) 
43128  64 
 used_axioms _ _ = NONE 
24855  65 

43129  66 
(* Lightweight predicate type information comes in two flavors, "t = t'" and 
67 
"t => t'", where "t" and "t'" are the same term modulo type tags. 

68 
In Isabelle, type tags are stripped away, so we are left with "t = t" or 

43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

69 
"t => t". Type tag idempotence is also handled this way. *) 
43184  70 
fun reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth = 
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

71 
let val thy = Proof_Context.theory_of ctxt in 
43184  72 
case hol_clause_from_metis ctxt sym_tab old_skolems mth of 
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

73 
Const (@{const_name HOL.eq}, _) $ _ $ t => 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

74 
t > cterm_of thy > Thm.reflexive RS @{thm meta_eq_to_obj_eq} 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

75 
 Const (@{const_name disj}, _) $ t1 $ t2 => 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

76 
(if can HOLogic.dest_not t1 then t2 else t1) 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

77 
> HOLogic.mk_Trueprop > cterm_of thy > Thm.trivial 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

78 
 _ => raise Fail "unexpected tags sym clause" 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

79 
end 
43129  80 
> Meson.make_meta_clause 
81 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

95 
val resolution_params = {active = active_params, waiting = waiting_params} 
37573  96 

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

97 
(* Main function to start Metis proof and reconstruction *) 
43212  98 
fun FOL_SOLVE (type_sys :: fallback_type_syss) ctxt cls ths0 = 
42361  99 
let val thy = Proof_Context.theory_of ctxt 
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39899
diff
changeset

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

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

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

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

106 
(0 upto length ths0  1) ths0 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

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

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

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

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

111 
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

112 
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths 
43212  113 
val (sym_tab, axioms, old_skolems) = 
114 
prepare_metis_problem ctxt type_sys cls ths 

43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

115 
fun get_isa_thm mth Isa_Reflexive_or_Trivial = 
43184  116 
reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

117 
 get_isa_thm _ (Isa_Raw ith) = ith 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

118 
val axioms = axioms > map (fn (mth, ith) => (mth, get_isa_thm mth ith)) 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

119 
val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

120 
val thms = axioms > map fst 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

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

123 
val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") 
32956  124 
in 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

125 
case filter (fn t => prop_of t aconv @{prop False}) cls of 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

126 
false_th :: _ => [false_th RS @{thm FalseE}] 
32956  127 
 [] => 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

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

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

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

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

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

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

135 
val proof = Metis_Proof.proof mth 
43094  136 
val result = 
43212  137 
axioms 
138 
> fold (replay_one_inference ctxt' old_skolems sym_tab) proof 

43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

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

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

141 
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used 
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

142 
val names = th_cls_pairs > map fst 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

143 
val used_names = 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

144 
th_cls_pairs 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

145 
> map_filter (fn (name, (_, cls)) => 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

146 
if have_common_thm used cls then SOME name 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

147 
else NONE) 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

148 
val unused_names = names > subtract (op =) used_names 
32956  149 
in 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

150 
if not (null cls) andalso not (have_common_thm used cls) then 
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis"  I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset

151 
verbose_warning ctxt "The assumptions are inconsistent" 
36383  152 
else 
153 
(); 

43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

154 
if not (null unused_names) then 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

155 
"Unused theorems: " ^ commas_quote unused_names 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

156 
> verbose_warning ctxt 
36230
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

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

158 
(); 
32956  159 
case result of 
160 
(_,ith)::_ => 

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

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

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

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

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

166 
(trace_msg ctxt (fn () => "Metis: No firstorder proof with the lemmas supplied"); 
43212  167 
if null fallback_type_syss then 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

168 
() 
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

169 
else 
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis"  I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset

170 
raise METIS ("FOL_SOLVE", 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

171 
"No 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

172 
[]) 
42733
01ef1c3d9cfd
more robust exception handling in Metis (also works if there are several subgoals)
blanchet
parents:
42650
diff
changeset

173 
end 
01ef1c3d9cfd
more robust exception handling in Metis (also works if there are several subgoals)
blanchet
parents:
42650
diff
changeset

174 
handle METIS (loc, msg) => 
43212  175 
case fallback_type_syss of 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

176 
[] => error ("Failed to replay Metis proof in Isabelle." ^ 
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

177 
(if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg 
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

178 
else "")) 
43212  179 
 type_sys :: _ => 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

180 
(verbose_warning ctxt 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

181 
("Falling back on " ^ 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

182 
quote (method_call_for_type_sys type_sys) ^ "..."); 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

183 
FOL_SOLVE fallback_type_syss ctxt cls ths0) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

184 

42847  185 
val neg_clausify = 
38028  186 
single 
187 
#> Meson.make_clauses_unsorted 

39890  188 
#> map Meson_Clausify.introduce_combinators_in_theorem 
38028  189 
#> Meson.finish_cnf 
190 

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

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

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

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

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

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

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

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

198 

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

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

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

201 

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

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

204 
val _ = trace_msg ctxt (fn () => 
43194  205 
"Metis called with theorems\n" ^ 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

206 
cat_lines (map (Display.string_of_thm ctxt) ths)) 
43212  207 
fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1 
32956  208 
in 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37625
diff
changeset

209 
if exists_type type_has_top_sort (prop_of st0) then 
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis"  I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset

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

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

212 
else 
43100  213 
Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0 
32956  214 
end 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

215 

43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

216 
val metis_default_type_syss = [partial_type_sys, full_type_sys] 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

217 
val metisFT_type_syss = [full_type_sys] 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

218 

43212  219 
fun metis_tac [] = generic_metis_tac metis_default_type_syss 
220 
 metis_tac type_syss = generic_metis_tac type_syss 

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

221 

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

222 
(* Whenever "X" has schematic type variables, we treat "using X by metis" as 
43100  223 
"by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables. 
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

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

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

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

228 
exists_type (exists_subtype (fn TVar _ => true  _ => false)) o prop_of 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

229 

43212  230 
fun method type_syss (type_sys, ths) ctxt facts = 
43100  231 
let 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

232 
val _ = 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

233 
if type_syss = metisFT_type_syss then 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

234 
legacy_feature "Old 'metisFT' method  \ 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

235 
\use 'metis (full_types)' instead" 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

236 
else 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

237 
() 
43100  238 
val (schem_facts, nonschem_facts) = List.partition has_tvar facts 
43212  239 
val type_syss = type_sys > Option.map single > the_default type_syss 
43100  240 
in 
43099  241 
HEADGOAL (Method.insert_tac nonschem_facts THEN' 
43212  242 
CHANGED_PROP 
243 
o generic_metis_tac type_syss ctxt (schem_facts @ ths)) 

43099  244 
end 
43100  245 

43235  246 
fun setup_method (binding, type_syss) = 
43212  247 
(if type_syss = metis_default_type_syss then 
43205  248 
(Args.parens Parse.short_ident 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

249 
>> (fn s => AList.lookup (op =) type_sys_aliases s > the_default s)) 
43205  250 
> Scan.option > Scan.lift 
251 
else 

252 
Scan.succeed NONE) 

43212  253 
 Attrib.thms >> (METHOD oo method type_syss) 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

254 
> Method.setup binding 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

255 

32956  256 
val setup = 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

257 
[((@{binding metis}, metis_default_type_syss), 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

258 
"Metis for FOL and HOL problems"), 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

259 
((@{binding metisFT}, metisFT_type_syss), 
43212  260 
"Metis for FOL/HOL problems with fullytyped translation")] 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

261 
> fold (uncurry setup_method) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

262 

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

263 
end; 