improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)
1 (* Title: HOL/Tools/Metis/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
7 Proof reconstruction for Metis.
10 signature METIS_RECONSTRUCT =
12 type mode = Metis_Translate.mode
14 val trace : bool Config.T
15 val trace_msg : Proof.context -> (unit -> string) -> unit
16 val verbose : bool Config.T
17 val verbose_warning : Proof.context -> string -> unit
18 val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
19 val untyped_aconv : term -> term -> bool
20 val replay_one_inference :
21 Proof.context -> mode -> (string * term) list
22 -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
23 -> (Metis_Thm.thm * thm) list
24 val discharge_skolem_premises :
25 Proof.context -> (thm * term) option list -> thm -> thm
26 val setup : theory -> theory
29 structure Metis_Reconstruct : METIS_RECONSTRUCT =
34 val (trace, trace_setup) = Attrib.config_bool "metis_trace" (K false)
35 val (verbose, verbose_setup) = Attrib.config_bool "metis_verbose" (K true)
37 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
38 fun verbose_warning ctxt msg =
39 if Config.get ctxt verbose then warning msg else ()
41 datatype term_or_type = SomeTerm of term | SomeType of typ
44 | terms_of (SomeTerm t :: tts) = t :: terms_of tts
45 | terms_of (SomeType _ :: tts) = terms_of tts;
48 | types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
49 if String.isPrefix metis_generated_var_prefix a then
50 (*Variable generated by Metis, which might have been a type variable.*)
51 TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
53 | types_of (SomeTerm _ :: tts) = types_of tts
54 | types_of (SomeType T :: tts) = T :: types_of tts;
56 fun apply_list rator nargs rands =
57 let val trands = terms_of rands
58 in if length trands = nargs then SomeTerm (list_comb(rator, trands))
60 ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
61 " expected " ^ string_of_int nargs ^
62 " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
65 fun infer_types ctxt =
66 Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
68 (*We use 1 rather than 0 because variable references in clauses may otherwise conflict
69 with variable constraints in the goal...at least, type inference often fails otherwise.
70 SEE ALSO axiom_inf below.*)
71 fun mk_var (w, T) = Var ((w, 1), T)
73 (*include the default sort, if available*)
76 in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end;
78 (*Remove the "apply" operator from an HO term*)
79 fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t
80 | strip_happ args x = (x, args);
82 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
84 fun hol_type_from_metis_term _ (Metis_Term.Var v) =
85 (case strip_prefix_and_unascii tvar_prefix v of
87 | NONE => make_tvar v)
88 | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
89 (case strip_prefix_and_unascii type_const_prefix x of
90 SOME tc => Type (invert_const tc,
91 map (hol_type_from_metis_term ctxt) tys)
93 case strip_prefix_and_unascii tfree_prefix x of
94 SOME tf => mk_tfree ctxt tf
95 | NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
97 (*Maps metis terms to isabelle terms*)
98 fun hol_term_from_metis_PT ctxt fol_tm =
99 let val thy = ProofContext.theory_of ctxt
100 val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^
101 Metis_Term.toString fol_tm)
102 fun tm_to_tt (Metis_Term.Var v) =
103 (case strip_prefix_and_unascii tvar_prefix v of
104 SOME w => SomeType (make_tvar w)
106 case strip_prefix_and_unascii schematic_var_prefix v of
107 SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
108 | NONE => SomeTerm (mk_var (v, HOLogic.typeT)))
109 (*Var from Metis with a name like _nnn; possibly a type variable*)
110 | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*)
111 | tm_to_tt (t as Metis_Term.Fn (".",_)) =
112 let val (rator,rands) = strip_happ [] t
114 Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
115 | _ => case tm_to_tt rator of
116 SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands)))
117 | _ => raise Fail "tm_to_tt: HO application"
119 | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
120 and applic_to_tt ("=",ts) =
121 SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
122 | applic_to_tt (a,ts) =
123 case strip_prefix_and_unascii const_prefix a of
126 val c = invert_const b
127 val ntypes = num_type_args thy c
128 val nterms = length ts - ntypes
129 val tts = map tm_to_tt ts
130 val tys = types_of (List.take(tts,ntypes))
132 if String.isPrefix new_skolem_const_prefix c then
133 Var ((new_skolem_var_name_from_const c, 1),
134 Type_Infer.paramify_vars (tl tys ---> hd tys))
137 in if length tys = ntypes then
138 apply_list t nterms (List.drop(tts,ntypes))
140 raise Fail ("Constant " ^ c ^ " expects " ^ string_of_int ntypes ^
141 " but gets " ^ string_of_int (length tys) ^
142 " type arguments\n" ^
143 cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
144 " the terms are \n" ^
145 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
147 | NONE => (*Not a constant. Is it a type constructor?*)
148 case strip_prefix_and_unascii type_const_prefix a of
150 SomeType (Type (invert_const b, types_of (map tm_to_tt ts)))
151 | NONE => (*Maybe a TFree. Should then check that ts=[].*)
152 case strip_prefix_and_unascii tfree_prefix a of
153 SOME b => SomeType (mk_tfree ctxt b)
154 | NONE => (*a fixed variable? They are Skolem functions.*)
155 case strip_prefix_and_unascii fixed_var_prefix a of
157 let val opr = Free (b, HOLogic.typeT)
158 in apply_list opr (length ts) (map tm_to_tt ts) end
159 | NONE => raise Fail ("unexpected metis function: " ^ a)
161 case tm_to_tt fol_tm of
163 | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], [])
166 (*Maps fully-typed metis terms to isabelle terms*)
167 fun hol_term_from_metis_FT ctxt fol_tm =
168 let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
169 Metis_Term.toString fol_tm)
171 let val c = c |> invert_const in
172 if String.isPrefix new_skolem_const_prefix c then
173 Var ((new_skolem_var_name_from_const c, 1), dummyT)
177 fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
178 (case strip_prefix_and_unascii schematic_var_prefix v of
179 SOME w => mk_var(w, dummyT)
180 | NONE => mk_var(v, dummyT))
181 | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) =
182 Const (@{const_name HOL.eq}, HOLogic.typeT)
183 | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
184 (case strip_prefix_and_unascii const_prefix x of
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, hol_type_from_metis_term ctxt ty)
189 | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
190 | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) =
192 | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
194 | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
195 | cvt (Metis_Term.Fn ("=", [tm1,tm2])) =
196 list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
197 | cvt (t as Metis_Term.Fn (x, [])) =
198 (case strip_prefix_and_unascii const_prefix x of
200 | NONE => (*Not a constant. Is it a fixed variable??*)
201 case strip_prefix_and_unascii fixed_var_prefix x of
202 SOME v => Free (v, dummyT)
203 | NONE => (trace_msg ctxt (fn () =>
204 "hol_term_from_metis_FT bad const: " ^ x);
205 hol_term_from_metis_PT ctxt t))
206 | cvt t = (trace_msg ctxt (fn () =>
207 "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
208 hol_term_from_metis_PT ctxt t)
211 fun hol_term_from_metis FT = hol_term_from_metis_FT
212 | hol_term_from_metis _ = hol_term_from_metis_PT
214 fun hol_terms_from_metis ctxt mode old_skolems fol_tms =
215 let val ts = map (hol_term_from_metis mode ctxt) fol_tms
216 val _ = trace_msg ctxt (fn () => " calling type inference:")
217 val _ = app (fn t => trace_msg ctxt
218 (fn () => Syntax.string_of_term ctxt t)) ts
219 val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
221 val _ = app (fn t => trace_msg ctxt
222 (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
223 " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
227 (* ------------------------------------------------------------------------- *)
228 (* FOL step Inference Rules *)
229 (* ------------------------------------------------------------------------- *)
231 (*for debugging only*)
233 fun print_thpair ctxt (fth,th) =
234 (trace_msg ctxt (fn () => "=============================================");
235 trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth);
236 trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
239 fun lookth thpairs (fth : Metis_Thm.thm) =
240 the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth)
241 handle Option.Option =>
242 raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
244 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
246 (* INFERENCE RULE: AXIOM *)
248 fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
249 (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
251 (* INFERENCE RULE: ASSUME *)
253 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
255 fun inst_excluded_middle thy i_atm =
256 let val th = EXCLUDED_MIDDLE
257 val [vx] = Term.add_vars (prop_of th) []
258 val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
259 in cterm_instantiate substs th end;
261 fun assume_inf ctxt mode skolem_params atm =
263 (ProofContext.theory_of ctxt)
264 (singleton (hol_terms_from_metis ctxt mode skolem_params)
267 (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
268 to reconstruct them admits new possibilities of errors, e.g. concerning
269 sorts. Instead we try to arrange that new TVars are distinct and that types
270 can be inferred from terms. *)
272 fun inst_inf ctxt mode old_skolems thpairs fsubst th =
273 let val thy = ProofContext.theory_of ctxt
274 val i_th = lookth thpairs th
275 val i_th_vars = Term.add_vars (prop_of i_th) []
276 fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
277 fun subst_translation (x,y) =
278 let val v = find_var x
279 (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
280 val t = hol_term_from_metis mode ctxt y
281 in SOME (cterm_of thy (Var v), t) end
282 handle Option.Option =>
283 (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
284 " in " ^ Display.string_of_thm ctxt i_th);
287 (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
288 " in " ^ Display.string_of_thm ctxt i_th);
290 fun remove_typeinst (a, t) =
291 case strip_prefix_and_unascii schematic_var_prefix a of
292 SOME b => SOME (b, t)
293 | NONE => case strip_prefix_and_unascii tvar_prefix a of
294 SOME _ => NONE (*type instantiations are forbidden!*)
295 | NONE => SOME (a,t) (*internal Metis var?*)
296 val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
297 val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
298 val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
299 val tms = rawtms |> map (reveal_old_skolem_terms old_skolems)
301 val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
302 val substs' = ListPair.zip (vars, map ctm_of tms)
303 val _ = trace_msg ctxt (fn () =>
304 cat_lines ("subst_translations:" ::
305 (substs' |> map (fn (x, y) =>
306 Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
307 Syntax.string_of_term ctxt (term_of y)))));
308 in cterm_instantiate substs' i_th end
309 handle THM (msg, _, _) =>
310 error ("Cannot replay Metis proof in Isabelle:\n" ^ msg)
312 (* INFERENCE RULE: RESOLVE *)
314 (* Like RSN, but we rename apart only the type variables. Vars here typically
315 have an index of 1, and the use of RSN would increase this typically to 3.
316 Instantiations of those Vars could then fail. See comment on "mk_var". *)
317 fun resolve_inc_tyvars thy tha i thb =
319 val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
321 case Thm.bicompose false (false, tha, nprems_of tha) i thb
322 |> Seq.list_of |> distinct Thm.eq_thm of
324 | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
329 (* The unifier, which is invoked from "Thm.bicompose", will sometimes
330 refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
331 "TERM" exception (with "add_ffpair" as first argument). We then
332 perform unification of the types of variables by hand and try
333 again. We could do this the first time around but this error
334 occurs seldom and we don't want to break existing proofs in subtle
335 ways or slow them down needlessly. *)
336 case [] |> fold (Term.add_vars o prop_of) [tha, thb]
337 |> AList.group (op =)
338 |> maps (fn ((s, _), T :: Ts) =>
339 map (fn T' => (Free (s, T), Free (s, T'))) Ts)
340 |> rpair (Envir.empty ~1)
341 |-> fold (Pattern.unify thy)
342 |> Envir.type_env |> Vartab.dest
343 |> map (fn (x, (S, T)) =>
344 pairself (ctyp_of thy) (TVar (x, S), T)) of
346 | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
349 fun s_not (@{const Not} $ t) = t
350 | s_not t = HOLogic.mk_not t
351 fun simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
354 (* Match untyped terms. *)
355 fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
356 | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
357 | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
358 (a = b) (* The index is ignored, for some reason. *)
359 | untyped_aconv (Bound i) (Bound j) = (i = j)
360 | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
361 | untyped_aconv (t1 $ t2) (u1 $ u2) =
362 untyped_aconv t1 u1 andalso untyped_aconv t2 u2
363 | untyped_aconv _ _ = false
365 (* Finding the relative location of an untyped term within a list of terms *)
366 fun index_of_literal lit haystack =
368 val normalize = simp_not_not o Envir.eta_contract
370 HOLogic.dest_Trueprop #> normalize #> untyped_aconv (lit |> normalize)
371 in case find_index match_lit haystack of ~1 => raise Empty | n => n + 1 end
373 (* Permute a rule's premises to move the i-th premise to the last position. *)
375 let val n = nprems_of th
376 in if 1 <= i andalso i <= n
377 then Thm.permute_prems (i-1) 1 th
378 else raise THM("select_literal", i, [th])
381 val neg_neg_imp = @{lemma "~ ~ Q ==> Q" by blast}
384 @{lemma "(~ A ==> False) == Trueprop A"
385 by (cut_tac atomize_not [of "~ A"]) simp}
387 (* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
388 to create double negations. *)
389 val negate_head = fold (rewrite_rule o single) [not_atomize, atomize_not]
391 (* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
392 val select_literal = negate_head oo make_last
394 fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 =
396 val thy = ProofContext.theory_of ctxt
397 val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
398 val _ = trace_msg ctxt (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
399 val _ = trace_msg ctxt (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
401 (* Trivial cases where one operand is type info *)
402 if Thm.eq_thm (TrueI, i_th1) then
404 else if Thm.eq_thm (TrueI, i_th2) then
409 singleton (hol_terms_from_metis ctxt mode skolem_params)
411 val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
412 val prems_th1 = prems_of i_th1
413 val prems_th2 = prems_of i_th2
415 index_of_literal (s_not i_atm) prems_th1
416 handle Empty => raise Fail "Failed to find literal in th1"
417 val _ = trace_msg ctxt (fn () => " index_th1: " ^ string_of_int index_th1)
419 index_of_literal i_atm prems_th2
420 handle Empty => raise Fail "Failed to find literal in th2"
421 val _ = trace_msg ctxt (fn () => " index_th2: " ^ string_of_int index_th2)
423 resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
427 (* INFERENCE RULE: REFL *)
429 val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
431 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
432 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
434 fun refl_inf ctxt mode skolem_params t =
435 let val thy = ProofContext.theory_of ctxt
436 val i_t = singleton (hol_terms_from_metis ctxt mode skolem_params) t
437 val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
438 val c_t = cterm_incr_types thy refl_idx i_t
439 in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
441 (* INFERENCE RULE: EQUALITY *)
443 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
444 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
446 val metis_eq = Metis_Term.Fn ("=", []);
448 fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*)
449 | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
450 | get_ty_arg_size _ _ = 0;
452 fun equality_inf ctxt mode skolem_params (pos, atm) fp fr =
453 let val thy = ProofContext.theory_of ctxt
454 val m_tm = Metis_Term.Fn atm
455 val [i_atm,i_tm] = hol_terms_from_metis ctxt mode skolem_params [m_tm, fr]
456 val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
457 fun replace_item_list lx 0 (_::ls) = lx::ls
458 | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
459 fun path_finder_FO tm [] = (tm, Bound 0)
460 | path_finder_FO tm (p::ps) =
461 let val (tm1,args) = strip_comb tm
462 val adjustment = get_ty_arg_size thy tm1
463 val p' = if adjustment > p then p else p-adjustment
464 val tm_p = List.nth(args,p')
466 error ("Cannot replay Metis proof in Isabelle:\n" ^
467 "equality_inf: " ^ string_of_int p ^ " adj " ^
468 string_of_int adjustment ^ " term " ^
469 Syntax.string_of_term ctxt tm)
470 val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int p ^
471 " " ^ Syntax.string_of_term ctxt tm_p)
472 val (r,t) = path_finder_FO tm_p ps
474 (r, list_comb (tm1, replace_item_list t p' args))
476 fun path_finder_HO tm [] = (tm, Bound 0)
477 | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
478 | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
479 | path_finder_HO tm ps =
480 raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
481 "equality_inf, path_finder_HO: path = " ^
482 space_implode " " (map string_of_int ps) ^
483 " isa-term: " ^ Syntax.string_of_term ctxt tm)
484 fun path_finder_FT tm [] _ = (tm, Bound 0)
485 | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) =
486 path_finder_FT tm ps t1
487 | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
488 (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
489 | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
490 (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
491 | path_finder_FT tm ps t =
492 raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
493 "equality_inf, path_finder_FT: path = " ^
494 space_implode " " (map string_of_int ps) ^
495 " isa-term: " ^ Syntax.string_of_term ctxt tm ^
496 " fol-term: " ^ Metis_Term.toString t)
497 fun path_finder FO tm ps _ = path_finder_FO tm ps
498 | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
499 (*equality: not curried, as other predicates are*)
500 if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
501 else path_finder_HO tm (p::ps) (*1 selects second operand*)
502 | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
503 path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
504 | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
505 (Metis_Term.Fn ("=", [t1,t2])) =
506 (*equality: not curried, as other predicates are*)
507 if p=0 then path_finder_FT tm (0::1::ps)
508 (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2]))
509 (*select first operand*)
510 else path_finder_FT tm (p::ps)
511 (Metis_Term.Fn (".", [metis_eq,t2]))
512 (*1 selects second operand*)
513 | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
514 (*if not equality, ignore head to skip the hBOOL predicate*)
515 | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
516 fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
517 let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
518 in (tm, nt $ tm_rslt) end
519 | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
520 val (tm_subst, body) = path_finder_lit i_atm fp
521 val tm_abs = Abs ("x", type_of tm_subst, body)
522 val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
523 val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
524 val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
525 val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
526 val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
527 val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
528 val eq_terms = map (pairself (cterm_of thy))
529 (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
530 in cterm_instantiate eq_terms subst' end;
532 val factor = Seq.hd o distinct_subgoals_tac;
534 fun step ctxt mode skolem_params thpairs p =
536 (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
537 | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolem_params f_atm
538 | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
539 factor (inst_inf ctxt mode skolem_params thpairs f_subst f_th1)
540 | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
541 factor (resolve_inf ctxt mode skolem_params thpairs f_atm f_th1 f_th2)
542 | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolem_params f_tm
543 | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
544 equality_inf ctxt mode skolem_params f_lit f_p f_r
546 fun flexflex_first_order th =
547 case Thm.tpairs_of th of
550 let val thy = theory_of_thm th
552 fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
553 val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
554 val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
558 fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
559 fun is_isabelle_literal_genuine t =
560 case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
562 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
564 (* Seldomly needed hack. A Metis clause is represented as a set, so duplicate
565 disjuncts are impossible. In the Isabelle proof, in spite of efforts to
566 eliminate them, duplicates sometimes appear with slightly different (but
568 fun resynchronize ctxt fol_th th =
571 count is_metis_literal_genuine
572 (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
573 val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th)
575 if num_metis_lits >= num_isabelle_lits then
579 val (prems0, concl) = th |> prop_of |> Logic.strip_horn
580 val prems = prems0 |> distinct (uncurry untyped_aconv)
581 val goal = Logic.list_implies (prems, concl)
583 if length prems = length prems0 then
584 error "Cannot replay Metis proof in Isabelle: Out of sync."
586 Goal.prove ctxt [] [] goal (K (cut_rules_tac [th] 1
587 THEN ALLGOALS assume_tac))
588 |> resynchronize ctxt fol_th
592 fun replay_one_inference ctxt mode skolem_params (fol_th, inf) thpairs =
593 if not (null thpairs) andalso prop_of (snd (hd thpairs)) aconv @{prop False} then
594 (* Isabelle sometimes identifies literals (premises) that are distinct in
595 Metis (e.g., because of type variables). We give the Isabelle proof the
596 benefice of the doubt. *)
600 val _ = trace_msg ctxt
601 (fn () => "=============================================")
602 val _ = trace_msg ctxt
603 (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
604 val _ = trace_msg ctxt
605 (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
606 val th = step ctxt mode skolem_params thpairs (fol_th, inf)
607 |> flexflex_first_order
608 |> resynchronize ctxt fol_th
609 val _ = trace_msg ctxt
610 (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
611 val _ = trace_msg ctxt
612 (fn () => "=============================================")
613 in (fol_th, th) :: thpairs end
615 (* It is normally sufficient to apply "assume_tac" to unify the conclusion with
616 one of the premises. Unfortunately, this sometimes yields "Variable
617 ?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the
618 variables before applying "assume_tac". Typical constraints are of the form
619 ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x,
620 where the nonvariables are goal parameters. *)
621 fun unify_first_prem_with_concl thy i th =
623 val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
624 val prem = goal |> Logic.strip_assums_hyp |> hd
625 val concl = goal |> Logic.strip_assums_concl
626 fun pair_untyped_aconv (t1, t2) (u1, u2) =
627 untyped_aconv t1 u1 andalso untyped_aconv t2 u2
628 fun add_terms tp inst =
629 if exists (pair_untyped_aconv tp) inst then inst
630 else tp :: map (apsnd (subst_atomic [tp])) inst
633 (Var _, args) => forall is_Bound args
635 fun unify_flex flex rigid =
636 case strip_comb flex of
637 (Var (z as (_, T)), args) =>
639 fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
641 fun unify_potential_flex comb atom =
642 if is_flex comb then unify_flex comb atom
643 else if is_Var atom then add_terms (atom, comb)
645 fun unify_terms (t, u) =
647 (t1 $ t2, u1 $ u2) =>
648 if is_flex t then unify_flex t u
649 else if is_flex u then unify_flex u t
650 else fold unify_terms [(t1, u1), (t2, u2)]
651 | (_ $ _, _) => unify_potential_flex t u
652 | (_, _ $ _) => unify_potential_flex u t
653 | (Var _, _) => add_terms (t, u)
654 | (_, Var _) => add_terms (u, t)
657 [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy)))
658 |> the_default [] (* FIXME *)
659 in th |> cterm_instantiate t_inst end
661 val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
663 fun copy_prems_tac [] ns i =
664 if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
665 | copy_prems_tac (1 :: ms) ns i =
666 rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
667 | copy_prems_tac (m :: ms) ns i =
668 etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
670 (* Metis generates variables of the form _nnn. *)
671 val is_metis_fresh_variable = String.isPrefix "_"
673 fun instantiate_forall_tac thy t i st =
675 val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
676 fun repair (t as (Var ((s, _), _))) =
677 (case find_index (fn (s', _) => s' = s) params of
681 (case (repair t, repair u) of
682 (t as Bound j, u as Bound k) =>
683 (* This is a rather subtle trick to repair the discrepancy between
684 the fully skolemized term that MESON gives us (where existentials
685 were pulled out) and the reality. *)
686 if k > j then t else t $ u
689 val t' = t |> repair |> fold (curry absdummy) (map snd params)
690 fun do_instantiate th =
691 case Term.add_vars (prop_of th) []
692 |> filter_out ((Meson_Clausify.is_zapped_var_name orf
693 is_metis_fresh_variable) o fst o fst) of
697 val var_binder_Ts = T |> binder_types |> take (length params) |> rev
698 val var_body_T = T |> funpow (length params) range_type
700 Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
701 var_body_T :: var_binder_Ts)
703 Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
704 tenv = Vartab.empty, tyenv = tyenv}
706 Vartab.fold (fn (x, (S, T)) =>
707 cons (pairself (ctyp_of thy) (TVar (x, S), T)))
710 [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
711 in th |> instantiate (ty_inst, t_inst) end
712 | _ => raise Fail "expected a single non-zapped, non-Metis Var"
714 (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
715 THEN PRIMITIVE do_instantiate) st
718 fun fix_exists_tac t =
720 THEN' rename_tac [t |> dest_Var |> fst |> fst]
722 fun release_quantifier_tac thy (skolem, t) =
723 (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
725 fun release_clusters_tac _ _ _ [] = K all_tac
726 | release_clusters_tac thy ax_counts substs
727 ((ax_no, cluster_no) :: clusters) =
730 Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
731 fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
734 |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
735 if ax_no' = ax_no then
736 tsubst |> map (apfst cluster_of_var)
737 |> filter (in_right_cluster o fst)
742 fun do_cluster_subst cluster_subst =
743 map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
744 val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
746 rotate_tac first_prem
747 THEN' (EVERY' (maps do_cluster_subst cluster_substs))
748 THEN' rotate_tac (~ first_prem - length cluster_substs)
749 THEN' release_clusters_tac thy ax_counts substs clusters
752 fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
753 (ax_no, (cluster_no, (skolem, index_no)))
755 prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord))
756 (pairself cluster_key p)
759 list_ord (prod_ord Term_Ord.fast_indexname_ord
760 (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
762 structure Int_Tysubst_Table =
763 Table(type key = int * (indexname * (sort * typ)) list
764 val ord = prod_ord int_ord tysubst_ord)
766 structure Int_Pair_Graph =
767 Graph(type key = int * int val ord = prod_ord int_ord int_ord)
769 fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
770 fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
772 (* Attempts to derive the theorem "False" from a theorem of the form
773 "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
774 specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
775 must be eliminated first. *)
776 fun discharge_skolem_premises ctxt axioms prems_imp_false =
777 if prop_of prems_imp_false aconv @{prop False} then
781 val thy = ProofContext.theory_of ctxt
785 Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
788 |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
790 o pairself (Meson_Clausify.cluster_of_zapped_var_name
792 |> map (Meson.term_pair_of
793 #> pairself (Envir.subst_term_types tyenv))
794 val tysubst = tyenv |> Vartab.dest
795 in (tysubst, tsubst) end
796 fun subst_info_for_prem subgoal_no prem =
798 _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
799 let val ax_no = HOLogic.dest_nat num in
801 match_term (nth axioms ax_no |> the |> snd, t)))
803 | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
805 fun cluster_of_var_name skolem s =
806 case try Meson_Clausify.cluster_of_zapped_var_name s of
808 | SOME ((ax_no, (cluster_no, _)), skolem') =>
809 if skolem' = skolem andalso cluster_no > 0 then
810 SOME (ax_no, cluster_no)
813 fun clusters_in_term skolem t =
814 Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
815 fun deps_for_term_subst (var, t) =
816 case clusters_in_term false var of
818 | [(ax_no, cluster_no)] =>
819 SOME ((ax_no, cluster_no),
820 clusters_in_term true t
821 |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
822 | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
823 val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
824 val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
825 |> sort (int_ord o pairself fst)
826 val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
827 val clusters = maps (op ::) depss
828 val ordered_clusters =
830 |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
831 |> fold Int_Pair_Graph.add_deps_acyclic depss
832 |> Int_Pair_Graph.topological_order
833 handle Int_Pair_Graph.CYCLES _ =>
834 error "Cannot replay Metis proof in Isabelle without \
835 \\"Hilbert_Choice\"."
837 Int_Tysubst_Table.empty
838 |> fold (fn (ax_no, (_, (tysubst, _))) =>
839 Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
840 (Integer.add 1)) substs
841 |> Int_Tysubst_Table.dest
842 val needed_axiom_props =
843 0 upto length axioms - 1 ~~ axioms
844 |> map_filter (fn (_, NONE) => NONE
845 | (ax_no, SOME (_, t)) =>
846 if exists (fn ((ax_no', _), n) =>
847 ax_no' = ax_no andalso n > 0)
852 val outer_param_names =
853 [] |> fold Term.add_var_names needed_axiom_props
854 |> filter (Meson_Clausify.is_zapped_var_name o fst)
855 |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
856 |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
857 cluster_no = 0 andalso skolem)
858 |> sort shuffle_ord |> map (fst o snd)
859 (* for debugging only:
860 fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
861 "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
862 "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
863 commas (map ((fn (s, t) => s ^ " |-> " ^ t)
864 o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
865 val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
866 val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
867 val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
868 val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
869 cat_lines (map string_for_subst_info substs))
871 fun cut_and_ex_tac axiom =
872 cut_rules_tac [axiom] 1
873 THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
874 fun rotation_for_subgoal i =
875 find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
877 Goal.prove ctxt [] [] @{prop False}
878 (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
880 THEN rename_tac outer_param_names 1
881 THEN copy_prems_tac (map snd ax_counts) [] 1)
882 THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
883 THEN match_tac [prems_imp_false] 1
884 THEN ALLGOALS (fn i =>
885 rtac @{thm Meson.skolem_COMBK_I} i
886 THEN rotate_tac (rotation_for_subgoal i) i
887 THEN PRIMITIVE (unify_first_prem_with_concl thy i)
891 error ("Cannot replay Metis proof in Isabelle:\n\
892 \Error when discharging Skolem assumptions.")
895 val setup = trace_setup #> verbose_setup