1 (* Title: HOL/Tools/Sledgehammer/metis_reconstruct.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 Proof reconstruction for Metis. |
|
8 *) |
|
9 |
|
10 signature METIS_RECONSTRUCT = |
|
11 sig |
|
12 type mode = Metis_Translate.mode |
|
13 |
|
14 val trace : bool Unsynchronized.ref |
|
15 val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a |
|
16 val untyped_aconv : term -> term -> bool |
|
17 val replay_one_inference : |
|
18 Proof.context -> mode -> (string * term) list |
|
19 -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list |
|
20 -> (Metis_Thm.thm * thm) list |
|
21 end; |
|
22 |
|
23 structure Metis_Reconstruct : METIS_RECONSTRUCT = |
|
24 struct |
|
25 |
|
26 open Metis_Translate |
|
27 |
|
28 val trace = Unsynchronized.ref false |
|
29 fun trace_msg msg = if !trace then tracing (msg ()) else () |
|
30 |
|
31 datatype term_or_type = SomeTerm of term | SomeType of typ |
|
32 |
|
33 fun terms_of [] = [] |
|
34 | terms_of (SomeTerm t :: tts) = t :: terms_of tts |
|
35 | terms_of (SomeType _ :: tts) = terms_of tts; |
|
36 |
|
37 fun types_of [] = [] |
|
38 | types_of (SomeTerm (Var ((a,idx), _)) :: tts) = |
|
39 if String.isPrefix "_" a then |
|
40 (*Variable generated by Metis, which might have been a type variable.*) |
|
41 TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts |
|
42 else types_of tts |
|
43 | types_of (SomeTerm _ :: tts) = types_of tts |
|
44 | types_of (SomeType T :: tts) = T :: types_of tts; |
|
45 |
|
46 fun apply_list rator nargs rands = |
|
47 let val trands = terms_of rands |
|
48 in if length trands = nargs then SomeTerm (list_comb(rator, trands)) |
|
49 else raise Fail |
|
50 ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ |
|
51 " expected " ^ Int.toString nargs ^ |
|
52 " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) |
|
53 end; |
|
54 |
|
55 fun infer_types ctxt = |
|
56 Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); |
|
57 |
|
58 (*We use 1 rather than 0 because variable references in clauses may otherwise conflict |
|
59 with variable constraints in the goal...at least, type inference often fails otherwise. |
|
60 SEE ALSO axiom_inf below.*) |
|
61 fun mk_var (w, T) = Var ((w, 1), T) |
|
62 |
|
63 (*include the default sort, if available*) |
|
64 fun mk_tfree ctxt w = |
|
65 let val ww = "'" ^ w |
|
66 in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end; |
|
67 |
|
68 (*Remove the "apply" operator from an HO term*) |
|
69 fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t |
|
70 | strip_happ args x = (x, args); |
|
71 |
|
72 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) |
|
73 |
|
74 fun smart_invert_const "fequal" = @{const_name HOL.eq} |
|
75 | smart_invert_const s = invert_const s |
|
76 |
|
77 fun hol_type_from_metis_term _ (Metis_Term.Var v) = |
|
78 (case strip_prefix_and_unascii tvar_prefix v of |
|
79 SOME w => make_tvar w |
|
80 | NONE => make_tvar v) |
|
81 | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) = |
|
82 (case strip_prefix_and_unascii type_const_prefix x of |
|
83 SOME tc => Type (smart_invert_const tc, |
|
84 map (hol_type_from_metis_term ctxt) tys) |
|
85 | NONE => |
|
86 case strip_prefix_and_unascii tfree_prefix x of |
|
87 SOME tf => mk_tfree ctxt tf |
|
88 | NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); |
|
89 |
|
90 (*Maps metis terms to isabelle terms*) |
|
91 fun hol_term_from_metis_PT ctxt fol_tm = |
|
92 let val thy = ProofContext.theory_of ctxt |
|
93 val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ |
|
94 Metis_Term.toString fol_tm) |
|
95 fun tm_to_tt (Metis_Term.Var v) = |
|
96 (case strip_prefix_and_unascii tvar_prefix v of |
|
97 SOME w => SomeType (make_tvar w) |
|
98 | NONE => |
|
99 case strip_prefix_and_unascii schematic_var_prefix v of |
|
100 SOME w => SomeTerm (mk_var (w, HOLogic.typeT)) |
|
101 | NONE => SomeTerm (mk_var (v, HOLogic.typeT)) ) |
|
102 (*Var from Metis with a name like _nnn; possibly a type variable*) |
|
103 | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) |
|
104 | tm_to_tt (t as Metis_Term.Fn (".",_)) = |
|
105 let val (rator,rands) = strip_happ [] t |
|
106 in case rator of |
|
107 Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) |
|
108 | _ => case tm_to_tt rator of |
|
109 SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands))) |
|
110 | _ => raise Fail "tm_to_tt: HO application" |
|
111 end |
|
112 | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args) |
|
113 and applic_to_tt ("=",ts) = |
|
114 SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts))) |
|
115 | applic_to_tt (a,ts) = |
|
116 case strip_prefix_and_unascii const_prefix a of |
|
117 SOME b => |
|
118 let |
|
119 val c = smart_invert_const b |
|
120 val ntypes = num_type_args thy c |
|
121 val nterms = length ts - ntypes |
|
122 val tts = map tm_to_tt ts |
|
123 val tys = types_of (List.take(tts,ntypes)) |
|
124 val t = |
|
125 if String.isPrefix new_skolem_const_prefix c then |
|
126 Var (new_skolem_var_from_const c, |
|
127 Type_Infer.paramify_vars (tl tys ---> hd tys)) |
|
128 else |
|
129 Const (c, dummyT) |
|
130 in if length tys = ntypes then |
|
131 apply_list t nterms (List.drop(tts,ntypes)) |
|
132 else |
|
133 raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ |
|
134 " but gets " ^ Int.toString (length tys) ^ |
|
135 " type arguments\n" ^ |
|
136 cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ |
|
137 " the terms are \n" ^ |
|
138 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) |
|
139 end |
|
140 | NONE => (*Not a constant. Is it a type constructor?*) |
|
141 case strip_prefix_and_unascii type_const_prefix a of |
|
142 SOME b => |
|
143 SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts))) |
|
144 | NONE => (*Maybe a TFree. Should then check that ts=[].*) |
|
145 case strip_prefix_and_unascii tfree_prefix a of |
|
146 SOME b => SomeType (mk_tfree ctxt b) |
|
147 | NONE => (*a fixed variable? They are Skolem functions.*) |
|
148 case strip_prefix_and_unascii fixed_var_prefix a of |
|
149 SOME b => |
|
150 let val opr = Free (b, HOLogic.typeT) |
|
151 in apply_list opr (length ts) (map tm_to_tt ts) end |
|
152 | NONE => raise Fail ("unexpected metis function: " ^ a) |
|
153 in |
|
154 case tm_to_tt fol_tm of |
|
155 SomeTerm t => t |
|
156 | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], []) |
|
157 end |
|
158 |
|
159 (*Maps fully-typed metis terms to isabelle terms*) |
|
160 fun hol_term_from_metis_FT ctxt fol_tm = |
|
161 let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ |
|
162 Metis_Term.toString fol_tm) |
|
163 fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) = |
|
164 (case strip_prefix_and_unascii schematic_var_prefix v of |
|
165 SOME w => mk_var(w, dummyT) |
|
166 | NONE => mk_var(v, dummyT)) |
|
167 | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) = |
|
168 Const (@{const_name HOL.eq}, HOLogic.typeT) |
|
169 | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) = |
|
170 (case strip_prefix_and_unascii const_prefix x of |
|
171 SOME c => Const (smart_invert_const c, dummyT) |
|
172 | NONE => (*Not a constant. Is it a fixed variable??*) |
|
173 case strip_prefix_and_unascii fixed_var_prefix x of |
|
174 SOME v => Free (v, hol_type_from_metis_term ctxt ty) |
|
175 | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) |
|
176 | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) = |
|
177 cvt tm1 $ cvt tm2 |
|
178 | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*) |
|
179 cvt tm1 $ cvt tm2 |
|
180 | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) |
|
181 | cvt (Metis_Term.Fn ("=", [tm1,tm2])) = |
|
182 list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2]) |
|
183 | cvt (t as Metis_Term.Fn (x, [])) = |
|
184 (case strip_prefix_and_unascii const_prefix x of |
|
185 SOME c => Const (smart_invert_const c, dummyT) |
|
186 | NONE => (*Not a constant. Is it a fixed variable??*) |
|
187 case strip_prefix_and_unascii fixed_var_prefix x of |
|
188 SOME v => Free (v, dummyT) |
|
189 | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); |
|
190 hol_term_from_metis_PT ctxt t)) |
|
191 | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); |
|
192 hol_term_from_metis_PT ctxt t) |
|
193 in fol_tm |> cvt end |
|
194 |
|
195 fun hol_term_from_metis FT = hol_term_from_metis_FT |
|
196 | hol_term_from_metis _ = hol_term_from_metis_PT |
|
197 |
|
198 fun hol_terms_from_fol ctxt mode old_skolems fol_tms = |
|
199 let val ts = map (hol_term_from_metis mode ctxt) fol_tms |
|
200 val _ = trace_msg (fn () => " calling type inference:") |
|
201 val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts |
|
202 val ts' = ts |> map (reveal_old_skolem_terms old_skolems) |
|
203 |> infer_types ctxt |
|
204 val _ = app (fn t => trace_msg |
|
205 (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ |
|
206 " of type " ^ Syntax.string_of_typ ctxt (type_of t))) |
|
207 ts' |
|
208 in ts' end; |
|
209 |
|
210 (* ------------------------------------------------------------------------- *) |
|
211 (* FOL step Inference Rules *) |
|
212 (* ------------------------------------------------------------------------- *) |
|
213 |
|
214 (*for debugging only*) |
|
215 (* |
|
216 fun print_thpair (fth,th) = |
|
217 (trace_msg (fn () => "============================================="); |
|
218 trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth); |
|
219 trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); |
|
220 *) |
|
221 |
|
222 fun lookth thpairs (fth : Metis_Thm.thm) = |
|
223 the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth) |
|
224 handle Option.Option => |
|
225 raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth) |
|
226 |
|
227 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); |
|
228 |
|
229 (* INFERENCE RULE: AXIOM *) |
|
230 |
|
231 fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th); |
|
232 (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) |
|
233 |
|
234 (* INFERENCE RULE: ASSUME *) |
|
235 |
|
236 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} |
|
237 |
|
238 fun inst_excluded_middle thy i_atm = |
|
239 let val th = EXCLUDED_MIDDLE |
|
240 val [vx] = Term.add_vars (prop_of th) [] |
|
241 val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)] |
|
242 in cterm_instantiate substs th end; |
|
243 |
|
244 fun assume_inf ctxt mode old_skolems atm = |
|
245 inst_excluded_middle |
|
246 (ProofContext.theory_of ctxt) |
|
247 (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm)) |
|
248 |
|
249 (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying |
|
250 to reconstruct them admits new possibilities of errors, e.g. concerning |
|
251 sorts. Instead we try to arrange that new TVars are distinct and that types |
|
252 can be inferred from terms. *) |
|
253 |
|
254 fun inst_inf ctxt mode old_skolems thpairs fsubst th = |
|
255 let val thy = ProofContext.theory_of ctxt |
|
256 val i_th = lookth thpairs th |
|
257 val i_th_vars = Term.add_vars (prop_of i_th) [] |
|
258 fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) |
|
259 fun subst_translation (x,y) = |
|
260 let val v = find_var x |
|
261 (* We call "reveal_old_skolem_terms" and "infer_types" below. *) |
|
262 val t = hol_term_from_metis mode ctxt y |
|
263 in SOME (cterm_of thy (Var v), t) end |
|
264 handle Option.Option => |
|
265 (trace_msg (fn () => "\"find_var\" failed for " ^ x ^ |
|
266 " in " ^ Display.string_of_thm ctxt i_th); |
|
267 NONE) |
|
268 | TYPE _ => |
|
269 (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^ |
|
270 " in " ^ Display.string_of_thm ctxt i_th); |
|
271 NONE) |
|
272 fun remove_typeinst (a, t) = |
|
273 case strip_prefix_and_unascii schematic_var_prefix a of |
|
274 SOME b => SOME (b, t) |
|
275 | NONE => case strip_prefix_and_unascii tvar_prefix a of |
|
276 SOME _ => NONE (*type instantiations are forbidden!*) |
|
277 | NONE => SOME (a,t) (*internal Metis var?*) |
|
278 val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) |
|
279 val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) |
|
280 val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) |
|
281 val tms = rawtms |> map (reveal_old_skolem_terms old_skolems) |
|
282 |> infer_types ctxt |
|
283 val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) |
|
284 val substs' = ListPair.zip (vars, map ctm_of tms) |
|
285 val _ = trace_msg (fn () => |
|
286 cat_lines ("subst_translations:" :: |
|
287 (substs' |> map (fn (x, y) => |
|
288 Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ |
|
289 Syntax.string_of_term ctxt (term_of y))))); |
|
290 in cterm_instantiate substs' i_th end |
|
291 handle THM (msg, _, _) => |
|
292 error ("Cannot replay Metis proof in Isabelle:\n" ^ msg) |
|
293 |
|
294 (* INFERENCE RULE: RESOLVE *) |
|
295 |
|
296 (* Like RSN, but we rename apart only the type variables. Vars here typically |
|
297 have an index of 1, and the use of RSN would increase this typically to 3. |
|
298 Instantiations of those Vars could then fail. See comment on "mk_var". *) |
|
299 fun resolve_inc_tyvars thy tha i thb = |
|
300 let |
|
301 val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha |
|
302 fun aux tha thb = |
|
303 case Thm.bicompose false (false, tha, nprems_of tha) i thb |
|
304 |> Seq.list_of |> distinct Thm.eq_thm of |
|
305 [th] => th |
|
306 | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, |
|
307 [tha, thb]) |
|
308 in |
|
309 aux tha thb |
|
310 handle TERM z => |
|
311 (* The unifier, which is invoked from "Thm.bicompose", will sometimes |
|
312 refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a |
|
313 "TERM" exception (with "add_ffpair" as first argument). We then |
|
314 perform unification of the types of variables by hand and try |
|
315 again. We could do this the first time around but this error |
|
316 occurs seldom and we don't want to break existing proofs in subtle |
|
317 ways or slow them down needlessly. *) |
|
318 case [] |> fold (Term.add_vars o prop_of) [tha, thb] |
|
319 |> AList.group (op =) |
|
320 |> maps (fn ((s, _), T :: Ts) => |
|
321 map (fn T' => (Free (s, T), Free (s, T'))) Ts) |
|
322 |> rpair (Envir.empty ~1) |
|
323 |-> fold (Pattern.unify thy) |
|
324 |> Envir.type_env |> Vartab.dest |
|
325 |> map (fn (x, (S, T)) => |
|
326 pairself (ctyp_of thy) (TVar (x, S), T)) of |
|
327 [] => raise TERM z |
|
328 | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb) |
|
329 end |
|
330 |
|
331 fun mk_not (Const (@{const_name Not}, _) $ b) = b |
|
332 | mk_not b = HOLogic.mk_not b |
|
333 |
|
334 (* Match untyped terms. *) |
|
335 fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b) |
|
336 | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b) |
|
337 | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) = |
|
338 (a = b) (* The index is ignored, for some reason. *) |
|
339 | untyped_aconv (Bound i) (Bound j) = (i = j) |
|
340 | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u |
|
341 | untyped_aconv (t1 $ t2) (u1 $ u2) = |
|
342 untyped_aconv t1 u1 andalso untyped_aconv t2 u2 |
|
343 | untyped_aconv _ _ = false |
|
344 |
|
345 (* Finding the relative location of an untyped term within a list of terms *) |
|
346 fun literal_index lit = |
|
347 let |
|
348 val lit = Envir.eta_contract lit |
|
349 fun get _ [] = raise Empty |
|
350 | get n (x :: xs) = |
|
351 if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then |
|
352 n |
|
353 else |
|
354 get (n+1) xs |
|
355 in get 1 end |
|
356 |
|
357 (* Permute a rule's premises to move the i-th premise to the last position. *) |
|
358 fun make_last i th = |
|
359 let val n = nprems_of th |
|
360 in if 1 <= i andalso i <= n |
|
361 then Thm.permute_prems (i-1) 1 th |
|
362 else raise THM("select_literal", i, [th]) |
|
363 end; |
|
364 |
|
365 (* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing |
|
366 double-negations. *) |
|
367 val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection] |
|
368 |
|
369 (* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *) |
|
370 val select_literal = negate_head oo make_last |
|
371 |
|
372 fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 = |
|
373 let |
|
374 val thy = ProofContext.theory_of ctxt |
|
375 val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 |
|
376 val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) |
|
377 val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) |
|
378 in |
|
379 (* Trivial cases where one operand is type info *) |
|
380 if Thm.eq_thm (TrueI, i_th1) then |
|
381 i_th2 |
|
382 else if Thm.eq_thm (TrueI, i_th2) then |
|
383 i_th1 |
|
384 else |
|
385 let |
|
386 val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems) |
|
387 (Metis_Term.Fn atm) |
|
388 val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) |
|
389 val prems_th1 = prems_of i_th1 |
|
390 val prems_th2 = prems_of i_th2 |
|
391 val index_th1 = literal_index (mk_not i_atm) prems_th1 |
|
392 handle Empty => raise Fail "Failed to find literal in th1" |
|
393 val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) |
|
394 val index_th2 = literal_index i_atm prems_th2 |
|
395 handle Empty => raise Fail "Failed to find literal in th2" |
|
396 val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) |
|
397 in |
|
398 resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2 |
|
399 end |
|
400 end; |
|
401 |
|
402 (* INFERENCE RULE: REFL *) |
|
403 |
|
404 val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp} |
|
405 |
|
406 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); |
|
407 val refl_idx = 1 + Thm.maxidx_of REFL_THM; |
|
408 |
|
409 fun refl_inf ctxt mode old_skolems t = |
|
410 let val thy = ProofContext.theory_of ctxt |
|
411 val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t |
|
412 val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) |
|
413 val c_t = cterm_incr_types thy refl_idx i_t |
|
414 in cterm_instantiate [(refl_x, c_t)] REFL_THM end; |
|
415 |
|
416 (* INFERENCE RULE: EQUALITY *) |
|
417 |
|
418 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} |
|
419 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} |
|
420 |
|
421 val metis_eq = Metis_Term.Fn ("=", []); |
|
422 |
|
423 fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*) |
|
424 | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0) |
|
425 | get_ty_arg_size _ _ = 0; |
|
426 |
|
427 fun equality_inf ctxt mode old_skolems (pos, atm) fp fr = |
|
428 let val thy = ProofContext.theory_of ctxt |
|
429 val m_tm = Metis_Term.Fn atm |
|
430 val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr] |
|
431 val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) |
|
432 fun replace_item_list lx 0 (_::ls) = lx::ls |
|
433 | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls |
|
434 fun path_finder_FO tm [] = (tm, Bound 0) |
|
435 | path_finder_FO tm (p::ps) = |
|
436 let val (tm1,args) = strip_comb tm |
|
437 val adjustment = get_ty_arg_size thy tm1 |
|
438 val p' = if adjustment > p then p else p-adjustment |
|
439 val tm_p = List.nth(args,p') |
|
440 handle Subscript => |
|
441 error ("Cannot replay Metis proof in Isabelle:\n" ^ |
|
442 "equality_inf: " ^ Int.toString p ^ " adj " ^ |
|
443 Int.toString adjustment ^ " term " ^ |
|
444 Syntax.string_of_term ctxt tm) |
|
445 val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ |
|
446 " " ^ Syntax.string_of_term ctxt tm_p) |
|
447 val (r,t) = path_finder_FO tm_p ps |
|
448 in |
|
449 (r, list_comb (tm1, replace_item_list t p' args)) |
|
450 end |
|
451 fun path_finder_HO tm [] = (tm, Bound 0) |
|
452 | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) |
|
453 | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) |
|
454 | path_finder_HO tm ps = |
|
455 raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ |
|
456 "equality_inf, path_finder_HO: path = " ^ |
|
457 space_implode " " (map Int.toString ps) ^ |
|
458 " isa-term: " ^ Syntax.string_of_term ctxt tm) |
|
459 fun path_finder_FT tm [] _ = (tm, Bound 0) |
|
460 | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) = |
|
461 path_finder_FT tm ps t1 |
|
462 | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) = |
|
463 (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) |
|
464 | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) = |
|
465 (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) |
|
466 | path_finder_FT tm ps t = |
|
467 raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ |
|
468 "equality_inf, path_finder_FT: path = " ^ |
|
469 space_implode " " (map Int.toString ps) ^ |
|
470 " isa-term: " ^ Syntax.string_of_term ctxt tm ^ |
|
471 " fol-term: " ^ Metis_Term.toString t) |
|
472 fun path_finder FO tm ps _ = path_finder_FO tm ps |
|
473 | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ = |
|
474 (*equality: not curried, as other predicates are*) |
|
475 if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) |
|
476 else path_finder_HO tm (p::ps) (*1 selects second operand*) |
|
477 | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) = |
|
478 path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) |
|
479 | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps) |
|
480 (Metis_Term.Fn ("=", [t1,t2])) = |
|
481 (*equality: not curried, as other predicates are*) |
|
482 if p=0 then path_finder_FT tm (0::1::ps) |
|
483 (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2])) |
|
484 (*select first operand*) |
|
485 else path_finder_FT tm (p::ps) |
|
486 (Metis_Term.Fn (".", [metis_eq,t2])) |
|
487 (*1 selects second operand*) |
|
488 | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 |
|
489 (*if not equality, ignore head to skip the hBOOL predicate*) |
|
490 | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) |
|
491 fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx = |
|
492 let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm |
|
493 in (tm, nt $ tm_rslt) end |
|
494 | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm |
|
495 val (tm_subst, body) = path_finder_lit i_atm fp |
|
496 val tm_abs = Abs ("x", type_of tm_subst, body) |
|
497 val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) |
|
498 val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) |
|
499 val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) |
|
500 val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) |
|
501 val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) |
|
502 val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') |
|
503 val eq_terms = map (pairself (cterm_of thy)) |
|
504 (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) |
|
505 in cterm_instantiate eq_terms subst' end; |
|
506 |
|
507 val factor = Seq.hd o distinct_subgoals_tac; |
|
508 |
|
509 fun step ctxt mode old_skolems thpairs p = |
|
510 case p of |
|
511 (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th) |
|
512 | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm |
|
513 | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => |
|
514 factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1) |
|
515 | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) => |
|
516 factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2) |
|
517 | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm |
|
518 | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => |
|
519 equality_inf ctxt mode old_skolems f_lit f_p f_r |
|
520 |
|
521 fun flexflex_first_order th = |
|
522 case Thm.tpairs_of th of |
|
523 [] => th |
|
524 | pairs => |
|
525 let val thy = theory_of_thm th |
|
526 val (_, tenv) = |
|
527 fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) |
|
528 val t_pairs = map Meson.term_pair_of (Vartab.dest tenv) |
|
529 val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th |
|
530 in th' end |
|
531 handle THM _ => th; |
|
532 |
|
533 fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s) |
|
534 fun is_isabelle_literal_genuine t = |
|
535 case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true |
|
536 |
|
537 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0 |
|
538 |
|
539 fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs = |
|
540 let |
|
541 val _ = trace_msg (fn () => "=============================================") |
|
542 val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) |
|
543 val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) |
|
544 val th = step ctxt mode old_skolems thpairs (fol_th, inf) |
|
545 |> flexflex_first_order |
|
546 val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) |
|
547 val _ = trace_msg (fn () => "=============================================") |
|
548 val num_metis_lits = |
|
549 fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList |
|
550 |> count is_metis_literal_genuine |
|
551 val num_isabelle_lits = |
|
552 th |> prems_of |> count is_isabelle_literal_genuine |
|
553 val _ = if num_metis_lits = num_isabelle_lits then () |
|
554 else error "Cannot replay Metis proof in Isabelle: Out of sync." |
|
555 in (fol_th, th) :: thpairs end |
|
556 |
|
557 end; |
|