|
1 (* Title: HOL/Tools/metis_tools.ML |
|
2 Author: Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory |
|
3 Copyright Cambridge University 2007 |
|
4 |
|
5 HOL setup for the Metis prover. |
|
6 *) |
|
7 |
|
8 signature METIS_TOOLS = |
|
9 sig |
|
10 val trace: bool Unsynchronized.ref |
|
11 val type_lits: bool Config.T |
|
12 val metis_tac: Proof.context -> thm list -> int -> tactic |
|
13 val metisF_tac: Proof.context -> thm list -> int -> tactic |
|
14 val metisFT_tac: Proof.context -> thm list -> int -> tactic |
|
15 val setup: theory -> theory |
|
16 end |
|
17 |
|
18 structure MetisTools: METIS_TOOLS = |
|
19 struct |
|
20 |
|
21 val trace = Unsynchronized.ref false; |
|
22 fun trace_msg msg = if ! trace then tracing (msg ()) else (); |
|
23 |
|
24 val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true; |
|
25 |
|
26 datatype mode = FO | HO | FT (*first-order, higher-order, fully-typed*) |
|
27 |
|
28 (* ------------------------------------------------------------------------- *) |
|
29 (* Useful Theorems *) |
|
30 (* ------------------------------------------------------------------------- *) |
|
31 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} |
|
32 val REFL_THM = incr_indexes 2 @{lemma "t ~= t ==> False" by simp} |
|
33 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} |
|
34 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} |
|
35 |
|
36 (* ------------------------------------------------------------------------- *) |
|
37 (* Useful Functions *) |
|
38 (* ------------------------------------------------------------------------- *) |
|
39 |
|
40 (* match untyped terms*) |
|
41 fun untyped_aconv (Const(a,_)) (Const(b,_)) = (a=b) |
|
42 | untyped_aconv (Free(a,_)) (Free(b,_)) = (a=b) |
|
43 | untyped_aconv (Var((a,_),_)) (Var((b,_),_)) = (a=b) (*the index is ignored!*) |
|
44 | untyped_aconv (Bound i) (Bound j) = (i=j) |
|
45 | untyped_aconv (Abs(a,_,t)) (Abs(b,_,u)) = (a=b) andalso untyped_aconv t u |
|
46 | untyped_aconv (t1$t2) (u1$u2) = untyped_aconv t1 u1 andalso untyped_aconv t2 u2 |
|
47 | untyped_aconv _ _ = false; |
|
48 |
|
49 (* Finding the relative location of an untyped term within a list of terms *) |
|
50 fun get_index lit = |
|
51 let val lit = Envir.eta_contract lit |
|
52 fun get n [] = raise Empty |
|
53 | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) |
|
54 then n else get (n+1) xs |
|
55 in get 1 end; |
|
56 |
|
57 (* ------------------------------------------------------------------------- *) |
|
58 (* HOL to FOL (Isabelle to Metis) *) |
|
59 (* ------------------------------------------------------------------------- *) |
|
60 |
|
61 fun fn_isa_to_met "equal" = "=" |
|
62 | fn_isa_to_met x = x; |
|
63 |
|
64 fun metis_lit b c args = (b, (c, args)); |
|
65 |
|
66 fun hol_type_to_fol (Res_Clause.AtomV x) = Metis.Term.Var x |
|
67 | hol_type_to_fol (Res_Clause.AtomF x) = Metis.Term.Fn(x,[]) |
|
68 | hol_type_to_fol (Res_Clause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps); |
|
69 |
|
70 (*These two functions insert type literals before the real literals. That is the |
|
71 opposite order from TPTP linkup, but maybe OK.*) |
|
72 |
|
73 fun hol_term_to_fol_FO tm = |
|
74 case Res_HOL_Clause.strip_comb tm of |
|
75 (Res_HOL_Clause.CombConst(c,_,tys), tms) => |
|
76 let val tyargs = map hol_type_to_fol tys |
|
77 val args = map hol_term_to_fol_FO tms |
|
78 in Metis.Term.Fn (c, tyargs @ args) end |
|
79 | (Res_HOL_Clause.CombVar(v,_), []) => Metis.Term.Var v |
|
80 | _ => error "hol_term_to_fol_FO"; |
|
81 |
|
82 fun hol_term_to_fol_HO (Res_HOL_Clause.CombVar (a, _)) = Metis.Term.Var a |
|
83 | hol_term_to_fol_HO (Res_HOL_Clause.CombConst (a, _, tylist)) = |
|
84 Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist) |
|
85 | hol_term_to_fol_HO (Res_HOL_Clause.CombApp (tm1, tm2)) = |
|
86 Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); |
|
87 |
|
88 (*The fully-typed translation, to avoid type errors*) |
|
89 fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]); |
|
90 |
|
91 fun hol_term_to_fol_FT (Res_HOL_Clause.CombVar(a, ty)) = |
|
92 wrap_type (Metis.Term.Var a, ty) |
|
93 | hol_term_to_fol_FT (Res_HOL_Clause.CombConst(a, ty, _)) = |
|
94 wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty) |
|
95 | hol_term_to_fol_FT (tm as Res_HOL_Clause.CombApp(tm1,tm2)) = |
|
96 wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), |
|
97 Res_HOL_Clause.type_of_combterm tm); |
|
98 |
|
99 fun hol_literal_to_fol FO (Res_HOL_Clause.Literal (pol, tm)) = |
|
100 let val (Res_HOL_Clause.CombConst(p,_,tys), tms) = Res_HOL_Clause.strip_comb tm |
|
101 val tylits = if p = "equal" then [] else map hol_type_to_fol tys |
|
102 val lits = map hol_term_to_fol_FO tms |
|
103 in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end |
|
104 | hol_literal_to_fol HO (Res_HOL_Clause.Literal (pol, tm)) = |
|
105 (case Res_HOL_Clause.strip_comb tm of |
|
106 (Res_HOL_Clause.CombConst("equal",_,_), tms) => |
|
107 metis_lit pol "=" (map hol_term_to_fol_HO tms) |
|
108 | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) |
|
109 | hol_literal_to_fol FT (Res_HOL_Clause.Literal (pol, tm)) = |
|
110 (case Res_HOL_Clause.strip_comb tm of |
|
111 (Res_HOL_Clause.CombConst("equal",_,_), tms) => |
|
112 metis_lit pol "=" (map hol_term_to_fol_FT tms) |
|
113 | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); |
|
114 |
|
115 fun literals_of_hol_thm thy mode t = |
|
116 let val (lits, types_sorts) = Res_HOL_Clause.literals_of_term thy t |
|
117 in (map (hol_literal_to_fol mode) lits, types_sorts) end; |
|
118 |
|
119 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) |
|
120 fun metis_of_typeLit pos (Res_Clause.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x] |
|
121 | metis_of_typeLit pos (Res_Clause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])]; |
|
122 |
|
123 fun default_sort _ (TVar _) = false |
|
124 | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1))); |
|
125 |
|
126 fun metis_of_tfree tf = |
|
127 Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf)); |
|
128 |
|
129 fun hol_thm_to_fol is_conjecture ctxt mode th = |
|
130 let val thy = ProofContext.theory_of ctxt |
|
131 val (mlits, types_sorts) = |
|
132 (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th |
|
133 in |
|
134 if is_conjecture then |
|
135 (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), Res_Clause.add_typs types_sorts) |
|
136 else |
|
137 let val tylits = Res_Clause.add_typs |
|
138 (filter (not o default_sort ctxt) types_sorts) |
|
139 val mtylits = if Config.get ctxt type_lits |
|
140 then map (metis_of_typeLit false) tylits else [] |
|
141 in |
|
142 (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), []) |
|
143 end |
|
144 end; |
|
145 |
|
146 (* ARITY CLAUSE *) |
|
147 |
|
148 fun m_arity_cls (Res_Clause.TConsLit (c,t,args)) = |
|
149 metis_lit true (Res_Clause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)] |
|
150 | m_arity_cls (Res_Clause.TVarLit (c,str)) = |
|
151 metis_lit false (Res_Clause.make_type_class c) [Metis.Term.Var str]; |
|
152 |
|
153 (*TrueI is returned as the Isabelle counterpart because there isn't any.*) |
|
154 fun arity_cls (Res_Clause.ArityClause{conclLit,premLits,...}) = |
|
155 (TrueI, |
|
156 Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits)))); |
|
157 |
|
158 (* CLASSREL CLAUSE *) |
|
159 |
|
160 fun m_classrel_cls subclass superclass = |
|
161 [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]]; |
|
162 |
|
163 fun classrel_cls (Res_Clause.ClassrelClause {subclass, superclass, ...}) = |
|
164 (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass))); |
|
165 |
|
166 (* ------------------------------------------------------------------------- *) |
|
167 (* FOL to HOL (Metis to Isabelle) *) |
|
168 (* ------------------------------------------------------------------------- *) |
|
169 |
|
170 datatype term_or_type = Term of Term.term | Type of Term.typ; |
|
171 |
|
172 fun terms_of [] = [] |
|
173 | terms_of (Term t :: tts) = t :: terms_of tts |
|
174 | terms_of (Type _ :: tts) = terms_of tts; |
|
175 |
|
176 fun types_of [] = [] |
|
177 | types_of (Term (Term.Var ((a,idx), _)) :: tts) = |
|
178 if String.isPrefix "_" a then |
|
179 (*Variable generated by Metis, which might have been a type variable.*) |
|
180 TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts |
|
181 else types_of tts |
|
182 | types_of (Term _ :: tts) = types_of tts |
|
183 | types_of (Type T :: tts) = T :: types_of tts; |
|
184 |
|
185 fun apply_list rator nargs rands = |
|
186 let val trands = terms_of rands |
|
187 in if length trands = nargs then Term (list_comb(rator, trands)) |
|
188 else error |
|
189 ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ |
|
190 " expected " ^ Int.toString nargs ^ |
|
191 " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) |
|
192 end; |
|
193 |
|
194 fun infer_types ctxt = |
|
195 Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); |
|
196 |
|
197 (*We use 1 rather than 0 because variable references in clauses may otherwise conflict |
|
198 with variable constraints in the goal...at least, type inference often fails otherwise. |
|
199 SEE ALSO axiom_inf below.*) |
|
200 fun mk_var (w,T) = Term.Var((w,1), T); |
|
201 |
|
202 (*include the default sort, if available*) |
|
203 fun mk_tfree ctxt w = |
|
204 let val ww = "'" ^ w |
|
205 in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end; |
|
206 |
|
207 (*Remove the "apply" operator from an HO term*) |
|
208 fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t |
|
209 | strip_happ args x = (x, args); |
|
210 |
|
211 fun fol_type_to_isa _ (Metis.Term.Var v) = |
|
212 (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of |
|
213 SOME w => Res_Reconstruct.make_tvar w |
|
214 | NONE => Res_Reconstruct.make_tvar v) |
|
215 | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) = |
|
216 (case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix x of |
|
217 SOME tc => Term.Type (Res_Reconstruct.invert_type_const tc, map (fol_type_to_isa ctxt) tys) |
|
218 | NONE => |
|
219 case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix x of |
|
220 SOME tf => mk_tfree ctxt tf |
|
221 | NONE => error ("fol_type_to_isa: " ^ x)); |
|
222 |
|
223 (*Maps metis terms to isabelle terms*) |
|
224 fun fol_term_to_hol_RAW ctxt fol_tm = |
|
225 let val thy = ProofContext.theory_of ctxt |
|
226 val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm) |
|
227 fun tm_to_tt (Metis.Term.Var v) = |
|
228 (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of |
|
229 SOME w => Type (Res_Reconstruct.make_tvar w) |
|
230 | NONE => |
|
231 case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of |
|
232 SOME w => Term (mk_var (w, HOLogic.typeT)) |
|
233 | NONE => Term (mk_var (v, HOLogic.typeT)) ) |
|
234 (*Var from Metis with a name like _nnn; possibly a type variable*) |
|
235 | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) |
|
236 | tm_to_tt (t as Metis.Term.Fn (".",_)) = |
|
237 let val (rator,rands) = strip_happ [] t |
|
238 in case rator of |
|
239 Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) |
|
240 | _ => case tm_to_tt rator of |
|
241 Term t => Term (list_comb(t, terms_of (map tm_to_tt rands))) |
|
242 | _ => error "tm_to_tt: HO application" |
|
243 end |
|
244 | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args) |
|
245 and applic_to_tt ("=",ts) = |
|
246 Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts))) |
|
247 | applic_to_tt (a,ts) = |
|
248 case Res_Reconstruct.strip_prefix Res_Clause.const_prefix a of |
|
249 SOME b => |
|
250 let val c = Res_Reconstruct.invert_const b |
|
251 val ntypes = Res_Reconstruct.num_typargs thy c |
|
252 val nterms = length ts - ntypes |
|
253 val tts = map tm_to_tt ts |
|
254 val tys = types_of (List.take(tts,ntypes)) |
|
255 val ntyargs = Res_Reconstruct.num_typargs thy c |
|
256 in if length tys = ntyargs then |
|
257 apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) |
|
258 else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^ |
|
259 " but gets " ^ Int.toString (length tys) ^ |
|
260 " type arguments\n" ^ |
|
261 cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ |
|
262 " the terms are \n" ^ |
|
263 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) |
|
264 end |
|
265 | NONE => (*Not a constant. Is it a type constructor?*) |
|
266 case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix a of |
|
267 SOME b => |
|
268 Type (Term.Type (Res_Reconstruct.invert_type_const b, types_of (map tm_to_tt ts))) |
|
269 | NONE => (*Maybe a TFree. Should then check that ts=[].*) |
|
270 case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix a of |
|
271 SOME b => Type (mk_tfree ctxt b) |
|
272 | NONE => (*a fixed variable? They are Skolem functions.*) |
|
273 case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix a of |
|
274 SOME b => |
|
275 let val opr = Term.Free(b, HOLogic.typeT) |
|
276 in apply_list opr (length ts) (map tm_to_tt ts) end |
|
277 | NONE => error ("unexpected metis function: " ^ a) |
|
278 in case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected" end; |
|
279 |
|
280 (*Maps fully-typed metis terms to isabelle terms*) |
|
281 fun fol_term_to_hol_FT ctxt fol_tm = |
|
282 let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm) |
|
283 fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = |
|
284 (case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of |
|
285 SOME w => mk_var(w, dummyT) |
|
286 | NONE => mk_var(v, dummyT)) |
|
287 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = |
|
288 Const ("op =", HOLogic.typeT) |
|
289 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = |
|
290 (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of |
|
291 SOME c => Const (Res_Reconstruct.invert_const c, dummyT) |
|
292 | NONE => (*Not a constant. Is it a fixed variable??*) |
|
293 case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of |
|
294 SOME v => Free (v, fol_type_to_isa ctxt ty) |
|
295 | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x)) |
|
296 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = |
|
297 cvt tm1 $ cvt tm2 |
|
298 | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*) |
|
299 cvt tm1 $ cvt tm2 |
|
300 | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) |
|
301 | cvt (Metis.Term.Fn ("=", [tm1,tm2])) = |
|
302 list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2]) |
|
303 | cvt (t as Metis.Term.Fn (x, [])) = |
|
304 (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of |
|
305 SOME c => Const (Res_Reconstruct.invert_const c, dummyT) |
|
306 | NONE => (*Not a constant. Is it a fixed variable??*) |
|
307 case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of |
|
308 SOME v => Free (v, dummyT) |
|
309 | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); |
|
310 fol_term_to_hol_RAW ctxt t)) |
|
311 | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); |
|
312 fol_term_to_hol_RAW ctxt t) |
|
313 in cvt fol_tm end; |
|
314 |
|
315 fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt |
|
316 | fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt |
|
317 | fol_term_to_hol ctxt FT = fol_term_to_hol_FT ctxt; |
|
318 |
|
319 fun fol_terms_to_hol ctxt mode fol_tms = |
|
320 let val ts = map (fol_term_to_hol ctxt mode) fol_tms |
|
321 val _ = trace_msg (fn () => " calling type inference:") |
|
322 val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts |
|
323 val ts' = infer_types ctxt ts; |
|
324 val _ = app (fn t => trace_msg |
|
325 (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ |
|
326 " of type " ^ Syntax.string_of_typ ctxt (type_of t))) |
|
327 ts' |
|
328 in ts' end; |
|
329 |
|
330 fun mk_not (Const ("Not", _) $ b) = b |
|
331 | mk_not b = HOLogic.mk_not b; |
|
332 |
|
333 val metis_eq = Metis.Term.Fn ("=", []); |
|
334 |
|
335 (* ------------------------------------------------------------------------- *) |
|
336 (* FOL step Inference Rules *) |
|
337 (* ------------------------------------------------------------------------- *) |
|
338 |
|
339 (*for debugging only*) |
|
340 fun print_thpair (fth,th) = |
|
341 (trace_msg (fn () => "============================================="); |
|
342 trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth); |
|
343 trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); |
|
344 |
|
345 fun lookth thpairs (fth : Metis.Thm.thm) = |
|
346 the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth) |
|
347 handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth); |
|
348 |
|
349 fun is_TrueI th = Thm.eq_thm(TrueI,th); |
|
350 |
|
351 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); |
|
352 |
|
353 fun inst_excluded_middle thy i_atm = |
|
354 let val th = EXCLUDED_MIDDLE |
|
355 val [vx] = Term.add_vars (prop_of th) [] |
|
356 val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)] |
|
357 in cterm_instantiate substs th end; |
|
358 |
|
359 (* INFERENCE RULE: AXIOM *) |
|
360 fun axiom_inf thpairs th = incr_indexes 1 (lookth thpairs th); |
|
361 (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) |
|
362 |
|
363 (* INFERENCE RULE: ASSUME *) |
|
364 fun assume_inf ctxt mode atm = |
|
365 inst_excluded_middle |
|
366 (ProofContext.theory_of ctxt) |
|
367 (singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)); |
|
368 |
|
369 (* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct |
|
370 them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange |
|
371 that new TVars are distinct and that types can be inferred from terms.*) |
|
372 fun inst_inf ctxt mode thpairs fsubst th = |
|
373 let val thy = ProofContext.theory_of ctxt |
|
374 val i_th = lookth thpairs th |
|
375 val i_th_vars = Term.add_vars (prop_of i_th) [] |
|
376 fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) |
|
377 fun subst_translation (x,y) = |
|
378 let val v = find_var x |
|
379 val t = fol_term_to_hol ctxt mode y (*we call infer_types below*) |
|
380 in SOME (cterm_of thy (Var v), t) end |
|
381 handle Option => |
|
382 (trace_msg (fn() => "List.find failed for the variable " ^ x ^ |
|
383 " in " ^ Display.string_of_thm ctxt i_th); |
|
384 NONE) |
|
385 fun remove_typeinst (a, t) = |
|
386 case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix a of |
|
387 SOME b => SOME (b, t) |
|
388 | NONE => case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix a of |
|
389 SOME _ => NONE (*type instantiations are forbidden!*) |
|
390 | NONE => SOME (a,t) (*internal Metis var?*) |
|
391 val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) |
|
392 val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst) |
|
393 val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) |
|
394 val tms = infer_types ctxt rawtms; |
|
395 val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) |
|
396 val substs' = ListPair.zip (vars, map ctm_of tms) |
|
397 val _ = trace_msg (fn () => |
|
398 cat_lines ("subst_translations:" :: |
|
399 (substs' |> map (fn (x, y) => |
|
400 Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ |
|
401 Syntax.string_of_term ctxt (term_of y))))); |
|
402 in cterm_instantiate substs' i_th |
|
403 handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg) |
|
404 end; |
|
405 |
|
406 (* INFERENCE RULE: RESOLVE *) |
|
407 |
|
408 (*Like RSN, but we rename apart only the type variables. Vars here typically have an index |
|
409 of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars |
|
410 could then fail. See comment on mk_var.*) |
|
411 fun resolve_inc_tyvars(tha,i,thb) = |
|
412 let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha |
|
413 val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb) |
|
414 in |
|
415 case distinct Thm.eq_thm ths of |
|
416 [th] => th |
|
417 | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb]) |
|
418 end; |
|
419 |
|
420 fun resolve_inf ctxt mode thpairs atm th1 th2 = |
|
421 let |
|
422 val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 |
|
423 val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) |
|
424 val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) |
|
425 in |
|
426 if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*) |
|
427 else if is_TrueI i_th2 then i_th1 |
|
428 else |
|
429 let |
|
430 val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm) |
|
431 val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) |
|
432 val prems_th1 = prems_of i_th1 |
|
433 val prems_th2 = prems_of i_th2 |
|
434 val index_th1 = get_index (mk_not i_atm) prems_th1 |
|
435 handle Empty => error "Failed to find literal in th1" |
|
436 val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) |
|
437 val index_th2 = get_index i_atm prems_th2 |
|
438 handle Empty => error "Failed to find literal in th2" |
|
439 val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) |
|
440 in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end |
|
441 end; |
|
442 |
|
443 (* INFERENCE RULE: REFL *) |
|
444 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); |
|
445 val refl_idx = 1 + Thm.maxidx_of REFL_THM; |
|
446 |
|
447 fun refl_inf ctxt mode t = |
|
448 let val thy = ProofContext.theory_of ctxt |
|
449 val i_t = singleton (fol_terms_to_hol ctxt mode) t |
|
450 val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) |
|
451 val c_t = cterm_incr_types thy refl_idx i_t |
|
452 in cterm_instantiate [(refl_x, c_t)] REFL_THM end; |
|
453 |
|
454 fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*) |
|
455 | get_ty_arg_size thy (Const (c, _)) = (Res_Reconstruct.num_typargs thy c handle TYPE _ => 0) |
|
456 | get_ty_arg_size _ _ = 0; |
|
457 |
|
458 (* INFERENCE RULE: EQUALITY *) |
|
459 fun equality_inf ctxt mode (pos, atm) fp fr = |
|
460 let val thy = ProofContext.theory_of ctxt |
|
461 val m_tm = Metis.Term.Fn atm |
|
462 val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr] |
|
463 val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) |
|
464 fun replace_item_list lx 0 (_::ls) = lx::ls |
|
465 | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls |
|
466 fun path_finder_FO tm [] = (tm, Term.Bound 0) |
|
467 | path_finder_FO tm (p::ps) = |
|
468 let val (tm1,args) = Term.strip_comb tm |
|
469 val adjustment = get_ty_arg_size thy tm1 |
|
470 val p' = if adjustment > p then p else p-adjustment |
|
471 val tm_p = List.nth(args,p') |
|
472 handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^ |
|
473 Int.toString adjustment ^ " term " ^ Syntax.string_of_term ctxt tm) |
|
474 val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ |
|
475 " " ^ Syntax.string_of_term ctxt tm_p) |
|
476 val (r,t) = path_finder_FO tm_p ps |
|
477 in |
|
478 (r, list_comb (tm1, replace_item_list t p' args)) |
|
479 end |
|
480 fun path_finder_HO tm [] = (tm, Term.Bound 0) |
|
481 | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) |
|
482 | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) |
|
483 fun path_finder_FT tm [] _ = (tm, Term.Bound 0) |
|
484 | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) = |
|
485 path_finder_FT tm ps t1 |
|
486 | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) = |
|
487 (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) |
|
488 | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) = |
|
489 (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) |
|
490 | path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^ |
|
491 space_implode " " (map Int.toString ps) ^ |
|
492 " isa-term: " ^ Syntax.string_of_term ctxt tm ^ |
|
493 " fol-term: " ^ Metis.Term.toString t) |
|
494 fun path_finder FO tm ps _ = path_finder_FO tm ps |
|
495 | path_finder HO (tm as Const("op =",_) $ _ $ _) (p::ps) _ = |
|
496 (*equality: not curried, as other predicates are*) |
|
497 if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) |
|
498 else path_finder_HO tm (p::ps) (*1 selects second operand*) |
|
499 | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) = |
|
500 path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) |
|
501 | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps) |
|
502 (Metis.Term.Fn ("=", [t1,t2])) = |
|
503 (*equality: not curried, as other predicates are*) |
|
504 if p=0 then path_finder_FT tm (0::1::ps) |
|
505 (Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2])) |
|
506 (*select first operand*) |
|
507 else path_finder_FT tm (p::ps) |
|
508 (Metis.Term.Fn (".", [metis_eq,t2])) |
|
509 (*1 selects second operand*) |
|
510 | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 |
|
511 (*if not equality, ignore head to skip the hBOOL predicate*) |
|
512 | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) |
|
513 fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx = |
|
514 let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm |
|
515 in (tm, nt $ tm_rslt) end |
|
516 | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm |
|
517 val (tm_subst, body) = path_finder_lit i_atm fp |
|
518 val tm_abs = Term.Abs("x", Term.type_of tm_subst, body) |
|
519 val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) |
|
520 val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) |
|
521 val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) |
|
522 val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) |
|
523 val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em) |
|
524 val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') |
|
525 val eq_terms = map (pairself (cterm_of thy)) |
|
526 (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) |
|
527 in cterm_instantiate eq_terms subst' end; |
|
528 |
|
529 val factor = Seq.hd o distinct_subgoals_tac; |
|
530 |
|
531 fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th) |
|
532 | step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm |
|
533 | step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) = |
|
534 factor (inst_inf ctxt mode thpairs f_subst f_th1) |
|
535 | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) = |
|
536 factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2) |
|
537 | step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm |
|
538 | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) = |
|
539 equality_inf ctxt mode f_lit f_p f_r; |
|
540 |
|
541 fun real_literal (_, (c, _)) = not (String.isPrefix Res_Clause.class_prefix c); |
|
542 |
|
543 fun translate _ _ thpairs [] = thpairs |
|
544 | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) = |
|
545 let val _ = trace_msg (fn () => "=============================================") |
|
546 val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th) |
|
547 val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf) |
|
548 val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf)) |
|
549 val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) |
|
550 val _ = trace_msg (fn () => "=============================================") |
|
551 val n_metis_lits = |
|
552 length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) |
|
553 in |
|
554 if nprems_of th = n_metis_lits then () |
|
555 else error "Metis: proof reconstruction has gone wrong"; |
|
556 translate mode ctxt ((fol_th, th) :: thpairs) infpairs |
|
557 end; |
|
558 |
|
559 (*Determining which axiom clauses are actually used*) |
|
560 fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th) |
|
561 | used_axioms _ _ = NONE; |
|
562 |
|
563 (* ------------------------------------------------------------------------- *) |
|
564 (* Translation of HO Clauses *) |
|
565 (* ------------------------------------------------------------------------- *) |
|
566 |
|
567 fun cnf_th thy th = hd (Res_Axioms.cnf_axiom thy th); |
|
568 |
|
569 val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal}; |
|
570 val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal}; |
|
571 |
|
572 val comb_I = cnf_th @{theory} Res_HOL_Clause.comb_I; |
|
573 val comb_K = cnf_th @{theory} Res_HOL_Clause.comb_K; |
|
574 val comb_B = cnf_th @{theory} Res_HOL_Clause.comb_B; |
|
575 val comb_C = cnf_th @{theory} Res_HOL_Clause.comb_C; |
|
576 val comb_S = cnf_th @{theory} Res_HOL_Clause.comb_S; |
|
577 |
|
578 fun type_ext thy tms = |
|
579 let val subs = Res_ATP.tfree_classes_of_terms tms |
|
580 val supers = Res_ATP.tvar_classes_of_terms tms |
|
581 and tycons = Res_ATP.type_consts_of_terms thy tms |
|
582 val (supers', arity_clauses) = Res_Clause.make_arity_clauses thy tycons supers |
|
583 val classrel_clauses = Res_Clause.make_classrel_clauses thy subs supers' |
|
584 in map classrel_cls classrel_clauses @ map arity_cls arity_clauses |
|
585 end; |
|
586 |
|
587 (* ------------------------------------------------------------------------- *) |
|
588 (* Logic maps manage the interface between HOL and first-order logic. *) |
|
589 (* ------------------------------------------------------------------------- *) |
|
590 |
|
591 type logic_map = |
|
592 {axioms : (Metis.Thm.thm * thm) list, |
|
593 tfrees : Res_Clause.type_literal list}; |
|
594 |
|
595 fun const_in_metis c (pred, tm_list) = |
|
596 let |
|
597 fun in_mterm (Metis.Term.Var _) = false |
|
598 | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list |
|
599 | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list |
|
600 in c = pred orelse exists in_mterm tm_list end; |
|
601 |
|
602 (*Extract TFree constraints from context to include as conjecture clauses*) |
|
603 fun init_tfrees ctxt = |
|
604 let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts |
|
605 in Res_Clause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end; |
|
606 |
|
607 (*transform isabelle type / arity clause to metis clause *) |
|
608 fun add_type_thm [] lmap = lmap |
|
609 | add_type_thm ((ith, mth) :: cls) {axioms, tfrees} = |
|
610 add_type_thm cls {axioms = (mth, ith) :: axioms, |
|
611 tfrees = tfrees} |
|
612 |
|
613 (*Insert non-logical axioms corresponding to all accumulated TFrees*) |
|
614 fun add_tfrees {axioms, tfrees} : logic_map = |
|
615 {axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms, |
|
616 tfrees = tfrees}; |
|
617 |
|
618 fun string_of_mode FO = "FO" |
|
619 | string_of_mode HO = "HO" |
|
620 | string_of_mode FT = "FT" |
|
621 |
|
622 (* Function to generate metis clauses, including comb and type clauses *) |
|
623 fun build_map mode0 ctxt cls ths = |
|
624 let val thy = ProofContext.theory_of ctxt |
|
625 (*The modes FO and FT are sticky. HO can be downgraded to FO.*) |
|
626 fun set_mode FO = FO |
|
627 | set_mode HO = if forall (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO |
|
628 | set_mode FT = FT |
|
629 val mode = set_mode mode0 |
|
630 (*transform isabelle clause to metis clause *) |
|
631 fun add_thm is_conjecture ith {axioms, tfrees} : logic_map = |
|
632 let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith |
|
633 in |
|
634 {axioms = (mth, Meson.make_meta_clause ith) :: axioms, |
|
635 tfrees = union (op =) tfree_lits tfrees} |
|
636 end; |
|
637 val lmap0 = fold (add_thm true) cls {axioms = [], tfrees = init_tfrees ctxt} |
|
638 val lmap = fold (add_thm false) ths (add_tfrees lmap0) |
|
639 val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) |
|
640 fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists |
|
641 (*Now check for the existence of certain combinators*) |
|
642 val thI = if used "c_COMBI" then [comb_I] else [] |
|
643 val thK = if used "c_COMBK" then [comb_K] else [] |
|
644 val thB = if used "c_COMBB" then [comb_B] else [] |
|
645 val thC = if used "c_COMBC" then [comb_C] else [] |
|
646 val thS = if used "c_COMBS" then [comb_S] else [] |
|
647 val thEQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else [] |
|
648 val lmap' = if mode=FO then lmap |
|
649 else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap |
|
650 in |
|
651 (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap') |
|
652 end; |
|
653 |
|
654 fun refute cls = |
|
655 Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls); |
|
656 |
|
657 fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); |
|
658 |
|
659 fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2); |
|
660 |
|
661 exception METIS of string; |
|
662 |
|
663 (* Main function to start metis prove and reconstruction *) |
|
664 fun FOL_SOLVE mode ctxt cls ths0 = |
|
665 let val thy = ProofContext.theory_of ctxt |
|
666 val th_cls_pairs = map (fn th => (Thm.get_name_hint th, Res_Axioms.cnf_axiom thy th)) ths0 |
|
667 val ths = maps #2 th_cls_pairs |
|
668 val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
|
669 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls |
|
670 val _ = trace_msg (fn () => "THEOREM CLAUSES") |
|
671 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths |
|
672 val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths |
|
673 val _ = if null tfrees then () |
|
674 else (trace_msg (fn () => "TFREE CLAUSES"); |
|
675 app (fn tf => trace_msg (fn _ => Res_Clause.tptp_of_typeLit true tf)) tfrees) |
|
676 val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") |
|
677 val thms = map #1 axioms |
|
678 val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms |
|
679 val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode) |
|
680 val _ = trace_msg (fn () => "START METIS PROVE PROCESS") |
|
681 in |
|
682 case filter (is_false o prop_of) cls of |
|
683 false_th::_ => [false_th RS @{thm FalseE}] |
|
684 | [] => |
|
685 case refute thms of |
|
686 Metis.Resolution.Contradiction mth => |
|
687 let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^ |
|
688 Metis.Thm.toString mth) |
|
689 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt |
|
690 (*add constraints arising from converting goal to clause form*) |
|
691 val proof = Metis.Proof.proof mth |
|
692 val result = translate mode ctxt' axioms proof |
|
693 and used = map_filter (used_axioms axioms) proof |
|
694 val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") |
|
695 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used |
|
696 val unused = th_cls_pairs |> map_filter (fn (name, cls) => |
|
697 if common_thm used cls then NONE else SOME name) |
|
698 in |
|
699 if null unused then () |
|
700 else warning ("Metis: unused theorems " ^ commas_quote unused); |
|
701 case result of |
|
702 (_,ith)::_ => |
|
703 (trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith); |
|
704 [ith]) |
|
705 | _ => (trace_msg (fn () => "Metis: no result"); |
|
706 []) |
|
707 end |
|
708 | Metis.Resolution.Satisfiable _ => |
|
709 (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied"); |
|
710 []) |
|
711 end; |
|
712 |
|
713 fun metis_general_tac mode ctxt ths i st0 = |
|
714 let val _ = trace_msg (fn () => |
|
715 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
|
716 in |
|
717 if exists_type Res_Axioms.type_has_topsort (prop_of st0) |
|
718 then raise METIS "Metis: Proof state contains the universal sort {}" |
|
719 else |
|
720 (Meson.MESON Res_Axioms.neg_clausify |
|
721 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i |
|
722 THEN Res_Axioms.expand_defs_tac st0) st0 |
|
723 end |
|
724 handle METIS s => (warning ("Metis: " ^ s); Seq.empty); |
|
725 |
|
726 val metis_tac = metis_general_tac HO; |
|
727 val metisF_tac = metis_general_tac FO; |
|
728 val metisFT_tac = metis_general_tac FT; |
|
729 |
|
730 fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt => |
|
731 SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment; |
|
732 |
|
733 val setup = |
|
734 type_lits_setup #> |
|
735 method @{binding metis} HO "METIS for FOL & HOL problems" #> |
|
736 method @{binding metisF} FO "METIS for FOL problems" #> |
|
737 method @{binding metisFT} FT "METIS with fully-typed translation" #> |
|
738 Method.setup @{binding finish_clausify} |
|
739 (Scan.succeed (K (SIMPLE_METHOD (Res_Axioms.expand_defs_tac refl)))) |
|
740 "cleanup after conversion to clauses"; |
|
741 |
|
742 end; |