|
1 (* Title: HOL/Tools/Metis/metis_tactic.ML |
|
2 Author: Kong W. Susanto, Cambridge University Computer Laboratory |
|
3 Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
|
4 Author: Jasmin Blanchette, TU Muenchen |
|
5 Copyright Cambridge University 2007 |
|
6 |
|
7 HOL setup for the Metis prover. |
|
8 *) |
|
9 |
|
10 signature METIS_TACTIC = |
|
11 sig |
|
12 val metisN : string |
|
13 val full_typesN : string |
|
14 val partial_typesN : string |
|
15 val no_typesN : string |
|
16 val really_full_type_enc : string |
|
17 val full_type_enc : string |
|
18 val partial_type_enc : string |
|
19 val no_type_enc : string |
|
20 val full_type_syss : string list |
|
21 val partial_type_syss : string list |
|
22 val trace : bool Config.T |
|
23 val verbose : bool Config.T |
|
24 val new_skolemizer : bool Config.T |
|
25 val metis_tac : string list -> Proof.context -> thm list -> int -> tactic |
|
26 val setup : theory -> theory |
|
27 end |
|
28 |
|
29 structure Metis_Tactic : METIS_TACTIC = |
|
30 struct |
|
31 |
|
32 open ATP_Translate |
|
33 open Metis_Translate |
|
34 open Metis_Reconstruct |
|
35 |
|
36 val metisN = "metis" |
|
37 |
|
38 val full_typesN = "full_types" |
|
39 val partial_typesN = "partial_types" |
|
40 val no_typesN = "no_types" |
|
41 |
|
42 val really_full_type_enc = "mono_tags_uniform" |
|
43 val full_type_enc = "poly_guards_uniform_query" |
|
44 val partial_type_enc = "poly_args" |
|
45 val no_type_enc = "erased" |
|
46 |
|
47 val full_type_syss = [full_type_enc, really_full_type_enc] |
|
48 val partial_type_syss = partial_type_enc :: full_type_syss |
|
49 |
|
50 val type_enc_aliases = |
|
51 [(full_typesN, full_type_syss), |
|
52 (partial_typesN, partial_type_syss), |
|
53 (no_typesN, [no_type_enc])] |
|
54 |
|
55 fun method_call_for_type_enc type_syss = |
|
56 metisN ^ " (" ^ |
|
57 (case AList.find (op =) type_enc_aliases type_syss of |
|
58 [alias] => alias |
|
59 | _ => hd type_syss) ^ ")" |
|
60 |
|
61 val new_skolemizer = |
|
62 Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) |
|
63 |
|
64 (* Designed to work also with monomorphic instances of polymorphic theorems. *) |
|
65 fun have_common_thm ths1 ths2 = |
|
66 exists (member (Term.aconv_untyped o pairself prop_of) ths1) |
|
67 (map Meson.make_meta_clause ths2) |
|
68 |
|
69 (*Determining which axiom clauses are actually used*) |
|
70 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) |
|
71 | used_axioms _ _ = NONE |
|
72 |
|
73 (* Lightweight predicate type information comes in two flavors, "t = t'" and |
|
74 "t => t'", where "t" and "t'" are the same term modulo type tags. |
|
75 In Isabelle, type tags are stripped away, so we are left with "t = t" or |
|
76 "t => t". Type tag idempotence is also handled this way. *) |
|
77 fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth = |
|
78 let val thy = Proof_Context.theory_of ctxt in |
|
79 case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of |
|
80 Const (@{const_name HOL.eq}, _) $ _ $ t => |
|
81 let |
|
82 val ct = cterm_of thy t |
|
83 val cT = ctyp_of_term ct |
|
84 in refl |> Drule.instantiate' [SOME cT] [SOME ct] end |
|
85 | Const (@{const_name disj}, _) $ t1 $ t2 => |
|
86 (if can HOLogic.dest_not t1 then t2 else t1) |
|
87 |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial |
|
88 | _ => raise Fail "unexpected tags sym clause" |
|
89 end |
|
90 |> Meson.make_meta_clause |
|
91 |
|
92 val clause_params = |
|
93 {ordering = Metis_KnuthBendixOrder.default, |
|
94 orderLiterals = Metis_Clause.UnsignedLiteralOrder, |
|
95 orderTerms = true} |
|
96 val active_params = |
|
97 {clause = clause_params, |
|
98 prefactor = #prefactor Metis_Active.default, |
|
99 postfactor = #postfactor Metis_Active.default} |
|
100 val waiting_params = |
|
101 {symbolsWeight = 1.0, |
|
102 variablesWeight = 0.0, |
|
103 literalsWeight = 0.0, |
|
104 models = []} |
|
105 val resolution_params = {active = active_params, waiting = waiting_params} |
|
106 |
|
107 (* Main function to start Metis proof and reconstruction *) |
|
108 fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 = |
|
109 let val thy = Proof_Context.theory_of ctxt |
|
110 val new_skolemizer = |
|
111 Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) |
|
112 val th_cls_pairs = |
|
113 map2 (fn j => fn th => |
|
114 (Thm.get_name_hint th, |
|
115 Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) |
|
116 (0 upto length ths0 - 1) ths0 |
|
117 val ths = maps (snd o snd) th_cls_pairs |
|
118 val dischargers = map (fst o snd) th_cls_pairs |
|
119 val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
|
120 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
|
121 val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") |
|
122 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths |
|
123 val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) |
|
124 val type_enc = type_enc_from_string Sound type_enc |
|
125 val (sym_tab, axioms, old_skolems) = |
|
126 prepare_metis_problem ctxt type_enc cls ths |
|
127 fun get_isa_thm mth Isa_Reflexive_or_Trivial = |
|
128 reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth |
|
129 | get_isa_thm _ (Isa_Raw ith) = ith |
|
130 val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) |
|
131 val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") |
|
132 val thms = axioms |> map fst |
|
133 val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms |
|
134 val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") |
|
135 in |
|
136 case filter (fn t => prop_of t aconv @{prop False}) cls of |
|
137 false_th :: _ => [false_th RS @{thm FalseE}] |
|
138 | [] => |
|
139 case Metis_Resolution.new resolution_params |
|
140 {axioms = thms, conjecture = []} |
|
141 |> Metis_Resolution.loop of |
|
142 Metis_Resolution.Contradiction mth => |
|
143 let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ |
|
144 Metis_Thm.toString mth) |
|
145 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt |
|
146 (*add constraints arising from converting goal to clause form*) |
|
147 val proof = Metis_Proof.proof mth |
|
148 val result = |
|
149 axioms |
|
150 |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof |
|
151 val used = map_filter (used_axioms axioms) proof |
|
152 val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") |
|
153 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used |
|
154 val names = th_cls_pairs |> map fst |
|
155 val used_names = |
|
156 th_cls_pairs |
|
157 |> map_filter (fn (name, (_, cls)) => |
|
158 if have_common_thm used cls then SOME name |
|
159 else NONE) |
|
160 val unused_names = names |> subtract (op =) used_names |
|
161 in |
|
162 if not (null cls) andalso not (have_common_thm used cls) then |
|
163 verbose_warning ctxt "The assumptions are inconsistent" |
|
164 else |
|
165 (); |
|
166 if not (null unused_names) then |
|
167 "Unused theorems: " ^ commas_quote unused_names |
|
168 |> verbose_warning ctxt |
|
169 else |
|
170 (); |
|
171 case result of |
|
172 (_,ith)::_ => |
|
173 (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); |
|
174 [discharge_skolem_premises ctxt dischargers ith]) |
|
175 | _ => (trace_msg ctxt (fn () => "Metis: No result"); []) |
|
176 end |
|
177 | Metis_Resolution.Satisfiable _ => |
|
178 (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied"); |
|
179 if null fallback_type_syss then |
|
180 () |
|
181 else |
|
182 raise METIS ("FOL_SOLVE", |
|
183 "No first-order proof with the lemmas supplied"); |
|
184 []) |
|
185 end |
|
186 handle METIS (loc, msg) => |
|
187 case fallback_type_syss of |
|
188 [] => error ("Failed to replay Metis proof in Isabelle." ^ |
|
189 (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg |
|
190 else "")) |
|
191 | _ => |
|
192 (verbose_warning ctxt |
|
193 ("Falling back on " ^ |
|
194 quote (method_call_for_type_enc fallback_type_syss) ^ "..."); |
|
195 FOL_SOLVE fallback_type_syss ctxt cls ths0) |
|
196 |
|
197 fun neg_clausify ctxt = |
|
198 single |
|
199 #> Meson.make_clauses_unsorted ctxt |
|
200 #> map Meson_Clausify.introduce_combinators_in_theorem |
|
201 #> Meson.finish_cnf |
|
202 |
|
203 fun preskolem_tac ctxt st0 = |
|
204 (if exists (Meson.has_too_many_clauses ctxt) |
|
205 (Logic.prems_of_goal (prop_of st0) 1) then |
|
206 Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1 |
|
207 THEN cnf.cnfx_rewrite_tac ctxt 1 |
|
208 else |
|
209 all_tac) st0 |
|
210 |
|
211 val type_has_top_sort = |
|
212 exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) |
|
213 |
|
214 fun generic_metis_tac type_syss ctxt ths i st0 = |
|
215 let |
|
216 val _ = trace_msg ctxt (fn () => |
|
217 "Metis called with theorems\n" ^ |
|
218 cat_lines (map (Display.string_of_thm ctxt) ths)) |
|
219 fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1 |
|
220 in |
|
221 if exists_type type_has_top_sort (prop_of st0) then |
|
222 verbose_warning ctxt "Proof state contains the universal sort {}" |
|
223 else |
|
224 (); |
|
225 Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0 |
|
226 end |
|
227 |
|
228 fun metis_tac [] = generic_metis_tac partial_type_syss |
|
229 | metis_tac type_syss = generic_metis_tac type_syss |
|
230 |
|
231 (* Whenever "X" has schematic type variables, we treat "using X by metis" as |
|
232 "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables. |
|
233 We don't do it for nonschematic facts "X" because this breaks a few proofs |
|
234 (in the rare and subtle case where a proof relied on extensionality not being |
|
235 applied) and brings few benefits. *) |
|
236 val has_tvar = |
|
237 exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of |
|
238 |
|
239 fun method default_type_syss (override_type_syss, ths) ctxt facts = |
|
240 let |
|
241 val _ = |
|
242 if default_type_syss = full_type_syss then |
|
243 legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead" |
|
244 else |
|
245 () |
|
246 val (schem_facts, nonschem_facts) = List.partition has_tvar facts |
|
247 val type_syss = override_type_syss |> the_default default_type_syss |
|
248 in |
|
249 HEADGOAL (Method.insert_tac nonschem_facts THEN' |
|
250 CHANGED_PROP |
|
251 o generic_metis_tac type_syss ctxt (schem_facts @ ths)) |
|
252 end |
|
253 |
|
254 fun setup_method (binding, type_syss) = |
|
255 ((Args.parens (Scan.repeat Parse.short_ident) |
|
256 >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s])) |
|
257 |> Scan.option |> Scan.lift) |
|
258 -- Attrib.thms >> (METHOD oo method type_syss) |
|
259 |> Method.setup binding |
|
260 |
|
261 val setup = |
|
262 [((@{binding metis}, partial_type_syss), |
|
263 "Metis for FOL and HOL problems"), |
|
264 ((@{binding metisFT}, full_type_syss), |
|
265 "Metis for FOL/HOL problems with fully-typed translation")] |
|
266 |> fold (uncurry setup_method) |
|
267 |
|
268 end; |