author  wenzelm 
Mon, 12 Aug 2019 15:44:41 +0200  
changeset 70513  dc749e0dc6b2 
parent 70489  12d1e6e2c1d0 
child 70514  7a63b16c53c4 
permissions  rwrr 
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 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 
50705
0e943b33d907
use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
blanchet
parents:
50694
diff
changeset

14 
val new_skolem : bool Config.T 
47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

15 
val advisory_simp : bool Config.T 
55521
241c6a2fdda1
added a version of the Metis tactic that returns the unused facts
blanchet
parents:
55520
diff
changeset

16 
val metis_tac_unused : string list > string > Proof.context > thm list > int > thm > 
241c6a2fdda1
added a version of the Metis tactic that returns the unused facts
blanchet
parents:
55520
diff
changeset

17 
thm list * thm Seq.seq 
54756  18 
val metis_tac : string list > string > Proof.context > thm list > int > tactic 
61302  19 
val metis_method : (string list option * string option) * thm list > Proof.context > thm list > 
62219
dbac573b27e7
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61841
diff
changeset

20 
tactic 
45521  21 
val metis_lam_transs : string list 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

22 
val parse_metis_options : (string list option * string option) parser 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

24 

44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
44634
diff
changeset

25 
structure Metis_Tactic : METIS_TACTIC = 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

27 

46320  28 
open ATP_Problem_Generate 
29 
open ATP_Proof_Reconstruct 

30 
open Metis_Generate 

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

31 
open Metis_Reconstruct 
35826  32 

69593  33 
val new_skolem = Attrib.setup_config_bool \<^binding>\<open>metis_new_skolem\<close> (K false) 
34 
val advisory_simp = Attrib.setup_config_bool \<^binding>\<open>metis_advisory_simp\<close> (K true) 

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

35 

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

36 
(* Designed to work also with monomorphic instances of polymorphic theorems. *) 
60358  37 
fun have_common_thm ctxt ths1 ths2 = 
38 
exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1) 

39 
(map (Meson.make_meta_clause ctxt) ths2) 

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

40 

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

42 
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) 
43128  43 
 used_axioms _ _ = NONE 
24855  44 

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

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

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

48 
"t => t". Type tag idempotence is also handled this way. *) 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset

49 
fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth = 
59632  50 
(case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of 
69593  51 
Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ t => 
70489  52 
let 
53 
val ct = Thm.cterm_of ctxt t 

54 
val cT = Thm.ctyp_of_cterm ct 

55 
in refl > Thm.instantiate' [SOME cT] [SOME ct] end 

69593  56 
 Const (\<^const_name>\<open>disj\<close>, _) $ t1 $ t2 => 
70489  57 
(if can HOLogic.dest_not t1 then t2 else t1) 
58 
> HOLogic.mk_Trueprop > Thm.cterm_of ctxt > Thm.trivial 

59632  59 
 _ => raise Fail "expected reflexive or trivial clause") 
60358  60 
> Meson.make_meta_clause ctxt 
43129  61 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset

62 
fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth = 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

63 
let 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

64 
val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac ctxt [refl] 1 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset

65 
val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth 
59632  66 
val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t) 
70489  67 
in 
68 
Goal.prove_internal ctxt [] ct (K tac) 

69 
> Meson.make_meta_clause ctxt 

70 
end 

45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

71 

45570
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

72 
fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u] 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

73 
 add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

74 
 add_vars_and_frees (t as Var _) = insert (op =) t 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

75 
 add_vars_and_frees (t as Free _) = insert (op =) t 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

76 
 add_vars_and_frees _ = I 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

77 

45569
eb30a5490543
wrap lambdas earlier, to get more control over beta/eta
blanchet
parents:
45568
diff
changeset

78 
fun introduce_lam_wrappers ctxt th = 
70489  79 
if Meson_Clausify.is_quasi_lambda_free (Thm.prop_of th) then th 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

80 
else 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

81 
let 
45570
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

82 
fun conv first ctxt ct = 
70489  83 
if Meson_Clausify.is_quasi_lambda_free (Thm.term_of ct) then Thm.reflexive ct 
57408  84 
else 
59582  85 
(case Thm.term_of ct of 
57408  86 
Abs (_, _, u) => 
70489  87 
if first then 
88 
(case add_vars_and_frees u [] of 

89 
[] => 

90 
Conv.abs_conv (conv false o snd) ctxt ct 

91 
> (fn th => Meson.first_order_resolve ctxt th @{thm Metis.eq_lambdaI}) 

92 
 v :: _ => 

93 
Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v 

94 
> Thm.cterm_of ctxt 

95 
> Conv.comb_conv (conv true ctxt)) 

96 
else Conv.abs_conv (conv false o snd) ctxt ct 

69593  97 
 Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ _ => Thm.reflexive ct 
57408  98 
 _ => Conv.comb_conv (conv true ctxt) ct) 
59582  99 
val eq_th = conv true ctxt (Thm.cprop_of th) 
45570
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

100 
(* We replace the equation's lefthand side with a betaequivalent term 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

101 
so that "Thm.equal_elim" works below. *) 
59582  102 
val t0 $ _ $ t2 = Thm.prop_of eq_th 
59632  103 
val eq_ct = t0 $ Thm.prop_of th $ t2 > Thm.cterm_of ctxt 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

104 
val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (resolve_tac ctxt [eq_th] 1)) 
45570
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

105 
in Thm.equal_elim eq_th' th end 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

106 

47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

107 
fun clause_params ordering = 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

108 
{ordering = ordering, 
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

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

110 
orderTerms = true} 
47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

111 
fun active_params ordering = 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

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

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

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

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

116 
{symbolsWeight = 1.0, 
47047
10bece4ac87e
more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV")
blanchet
parents:
47045
diff
changeset

117 
variablesWeight = 0.05, 
10bece4ac87e
more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV")
blanchet
parents:
47045
diff
changeset

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

119 
models = []} 
47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

120 
fun resolution_params ordering = 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

121 
{active = active_params ordering, waiting = waiting_params} 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

122 

1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

123 
fun kbo_advisory_simp_ordering ord_info = 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

124 
let 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

125 
fun weight (m, _) = 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

126 
AList.lookup (op =) ord_info (Metis_Name.toString m) > the_default 1 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

127 
fun precedence p = 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58839
diff
changeset

128 
(case int_ord (apply2 weight p) of 
47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

129 
EQUAL => #precedence Metis_KnuthBendixOrder.default p 
57408  130 
 ord => ord) 
47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

131 
in {weight = weight, precedence = precedence} end 
37573  132 

55285  133 
fun metis_call type_enc lam_trans = 
134 
let 

135 
val type_enc = 

136 
(case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of 

137 
[alias] => alias 

138 
 _ => type_enc) 

139 
val opts = 

140 
[] > type_enc <> partial_typesN ? cons type_enc 

141 
> lam_trans <> default_metis_lam_trans ? cons lam_trans 

142 
in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end 

143 

50875
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset

144 
exception METIS_UNPROVABLE of unit 
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset

145 

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

146 
(* Main function to start Metis proof and reconstruction *) 
70488  147 
fun FOL_SOLVE unused type_encs lam_trans ctxt cls ths0 = 
70489  148 
let 
149 
val thy = Proof_Context.theory_of ctxt 

150 

151 
val new_skolem = Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy) 

152 
val do_lams = 

153 
(lam_trans = liftingN orelse lam_trans = lam_liftingN) ? introduce_lam_wrappers ctxt 

154 
val th_cls_pairs = 

155 
map2 (fn j => fn th => 

156 
(Thm.get_name_hint th, 

157 
th 

158 
> Drule.eta_contraction_rule 

159 
> Meson_Clausify.cnf_axiom ctxt new_skolem (lam_trans = combsN) j 

160 
> map do_lams)) 

161 
(0 upto length ths0  1) ths0 

162 
val ths = maps (snd o snd) th_cls_pairs 

163 
val dischargers = map (fst o snd) th_cls_pairs 

164 
val cls = cls > map (Drule.eta_contraction_rule #> do_lams) 

165 
val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES") 

166 
val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls 

167 

168 
val type_enc :: fallback_type_encs = type_encs 

169 
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) 

170 
val type_enc = type_enc_of_string Strict type_enc 

171 

172 
val (sym_tab, axioms, ord_info, concealed) = 

173 
generate_metis_problem ctxt type_enc lam_trans cls ths 

174 
fun get_isa_thm mth Isa_Reflexive_or_Trivial = 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset

175 
reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth 
70489  176 
 get_isa_thm mth Isa_Lambda_Lifted = 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51717
diff
changeset

177 
lam_lifted_of_metis ctxt type_enc sym_tab concealed mth 
70489  178 
 get_isa_thm _ (Isa_Raw ith) = ith 
179 
val axioms = axioms > map (fn (mth, ith) => (mth, get_isa_thm mth ith)) 

180 
val _ = trace_msg ctxt (K "ISABELLE CLAUSES") 

181 
val _ = List.app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms 

182 
val _ = trace_msg ctxt (K "METIS CLAUSES") 

183 
val _ = List.app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms 

184 

185 
val _ = trace_msg ctxt (K "START METIS PROVE PROCESS") 

186 
val ordering = 

187 
if Config.get ctxt advisory_simp 

188 
then kbo_advisory_simp_ordering (ord_info ()) 

189 
else Metis_KnuthBendixOrder.default 

190 

50875
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset

191 
fun fall_back () = 
bfb626265782
less brutal Metis failure  the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
50705
diff
changeset

192 
(verbose_warning ctxt 
70489  193 
("Falling back on " ^ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "..."); 
55521
241c6a2fdda1
added a version of the Metis tactic that returns the unused facts
blanchet
parents:
55520
diff
changeset

194 
FOL_SOLVE unused fallback_type_encs lam_trans ctxt cls ths0) 
32956  195 
in 
69593  196 
(case filter (fn t => Thm.prop_of t aconv \<^prop>\<open>False\<close>) cls of 
70489  197 
false_th :: _ => [false_th RS @{thm FalseE}] 
198 
 [] => 

199 
(case Metis_Resolution.loop (Metis_Resolution.new (resolution_params ordering) 

200 
{axioms = axioms > map fst, conjecture = []}) of 

201 
Metis_Resolution.Contradiction mth => 

202 
let 

203 
val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ Metis_Thm.toString mth) 

204 
val ctxt' = fold Variable.declare_constraints (map Thm.prop_of cls) ctxt 

205 
(*add constraints arising from converting goal to clause form*) 

206 
val proof = Metis_Proof.proof mth 

207 
val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms 

208 
val used = map_filter (used_axioms axioms) proof 

209 
val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:") 

210 
val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used 

211 

70513  212 
val unused_th_cls_pairs = filter_out (have_common_thm ctxt used o #2 o #2) th_cls_pairs 
213 
val _ = unused := maps (#2 o #2) unused_th_cls_pairs; 

70489  214 
val _ = 
70513  215 
if not (null unused_th_cls_pairs) then 
216 
verbose_warning ctxt ("Unused theorems: " ^ commas_quote (map #1 unused_th_cls_pairs)) 

70489  217 
else (); 
218 
val _ = 

219 
if not (null cls) andalso not (have_common_thm ctxt used cls) then 

220 
verbose_warning ctxt "The assumptions are inconsistent" 

221 
else (); 

222 
in 

223 
(case result of 

224 
(_, ith) :: _ => 

225 
(trace_msg ctxt (fn () => "Success: " ^ Thm.string_of_thm ctxt ith); 

226 
[discharge_skolem_premises ctxt dischargers ith]) 

227 
 _ => (trace_msg ctxt (K "Metis: No result"); [])) 

228 
end 

229 
 Metis_Resolution.Satisfiable _ => 

230 
(trace_msg ctxt (K "Metis: No firstorder proof with the supplied lemmas"); 

231 
raise METIS_UNPROVABLE ())) 

232 
handle METIS_UNPROVABLE () => if null fallback_type_encs then [] else fall_back () 

233 
 METIS_RECONSTRUCT (loc, msg) => 

234 
if null fallback_type_encs then 

235 
(verbose_warning ctxt ("Failed to replay Metis proof\n" ^ loc ^ ": " ^ msg); []) 

236 
else fall_back ()) 

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

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

238 

45508  239 
fun neg_clausify ctxt combinators = 
38028  240 
single 
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43963
diff
changeset

241 
#> Meson.make_clauses_unsorted ctxt 
55236  242 
#> combinators ? map (Meson_Clausify.introduce_combinators_in_theorem ctxt) 
38028  243 
#> Meson.finish_cnf 
244 

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

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

246 
(if exists (Meson.has_too_many_clauses ctxt) 
59582  247 
(Logic.prems_of_goal (Thm.prop_of st0) 1) then 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50875
diff
changeset

248 
Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex} ctxt) 1 
55239  249 
THEN CNF.cnfx_rewrite_tac ctxt 1 
39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset

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

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

252 

55521
241c6a2fdda1
added a version of the Metis tactic that returns the unused facts
blanchet
parents:
55520
diff
changeset

253 
fun metis_tac_unused type_encs0 lam_trans ctxt ths i st0 = 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

254 
let 
55521
241c6a2fdda1
added a version of the Metis tactic that returns the unused facts
blanchet
parents:
55520
diff
changeset

255 
val unused = Unsynchronized.ref [] 
55520  256 
val type_encs = if null type_encs0 then partial_type_encs else type_encs0 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

257 
val _ = trace_msg ctxt (fn () => 
61268  258 
"Metis called with theorems\n" ^ cat_lines (map (Thm.string_of_thm ctxt) ths)) 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

259 
val type_encs = type_encs > maps unalias_type_enc 
55521
241c6a2fdda1
added a version of the Metis tactic that returns the unused facts
blanchet
parents:
55520
diff
changeset

260 
val combs = (lam_trans = combsN) 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

261 
fun tac clause = resolve_tac ctxt (FOL_SOLVE unused type_encs lam_trans ctxt clause ths) 1 
55521
241c6a2fdda1
added a version of the Metis tactic that returns the unused facts
blanchet
parents:
55520
diff
changeset

262 
val seq = Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt combs)) tac ctxt i st0 
32956  263 
in 
55521
241c6a2fdda1
added a version of the Metis tactic that returns the unused facts
blanchet
parents:
55520
diff
changeset

264 
(!unused, seq) 
32956  265 
end 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

266 

55521
241c6a2fdda1
added a version of the Metis tactic that returns the unused facts
blanchet
parents:
55520
diff
changeset

267 
fun metis_tac type_encs lam_trans ctxt ths i = snd o metis_tac_unused type_encs lam_trans ctxt ths i 
241c6a2fdda1
added a version of the Metis tactic that returns the unused facts
blanchet
parents:
55520
diff
changeset

268 

55520  269 
(* Whenever "X" has schematic type variables, we treat "using X by metis" as "by (metis X)" to 
270 
prevent "Subgoal.FOCUS" from freezing the type variables. We don't do it for nonschematic facts 

271 
"X" because this breaks a few proofs (in the rare and subtle case where a proof relied on 

272 
extensionality not being applied) and brings few benefits. *) 

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

274 

55315  275 
fun metis_method ((override_type_encs, lam_trans), ths) ctxt facts = 
55520  276 
let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in 
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61302
diff
changeset

277 
HEADGOAL (Method.insert_tac ctxt nonschem_facts THEN' 
55520  278 
CHANGED_PROP o metis_tac (these override_type_encs) 
279 
(the_default default_metis_lam_trans lam_trans) ctxt (schem_facts @ ths)) 

43099  280 
end 
43100  281 

46365  282 
val metis_lam_transs = [hide_lamsN, liftingN, combsN] 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

283 

45578  284 
fun set_opt _ x NONE = SOME x 
285 
 set_opt get x (SOME x0) = 

55523
9429e7b5b827
removed final periods in messages for proof methods
blanchet
parents:
55521
diff
changeset

286 
error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x)) 
54756  287 

45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

288 
fun consider_opt s = 
54756  289 
if member (op =) metis_lam_transs s then apsnd (set_opt I s) else apfst (set_opt hd [s]) 
45514  290 

45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

291 
val parse_metis_options = 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

292 
Scan.optional 
69593  293 
(Args.parens (Args.name  Scan.option (\<^keyword>\<open>,\<close>  Args.name)) 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

294 
>> (fn (s, s') => 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

295 
(NONE, NONE) > consider_opt s 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

296 
> (case s' of SOME s' => consider_opt s'  _ => I))) 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

297 
(NONE, NONE) 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

298 

58818  299 
val _ = 
300 
Theory.setup 

69593  301 
(Method.setup \<^binding>\<open>metis\<close> 
58818  302 
(Scan.lift parse_metis_options  Attrib.thms >> (METHOD oo metis_method)) 
303 
"Metis for FOL and HOL problems") 

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

304 

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

305 
end; 