handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
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}
383 (* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
385 fun negate_head thy =
386 rewrite_rule @{thms atomize_not}
387 #> perhaps (try (fn th => resolve_inc_tyvars thy th 1 neg_neg_imp))
389 (* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
390 fun select_literal thy = negate_head thy oo make_last
392 fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 =
394 val thy = ProofContext.theory_of ctxt
395 val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
396 val _ = trace_msg ctxt (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
397 val _ = trace_msg ctxt (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
399 (* Trivial cases where one operand is type info *)
400 if Thm.eq_thm (TrueI, i_th1) then
402 else if Thm.eq_thm (TrueI, i_th2) then
407 singleton (hol_terms_from_metis ctxt mode skolem_params)
409 val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
410 val prems_th1 = prems_of i_th1
411 val prems_th2 = prems_of i_th2
413 index_of_literal (s_not i_atm) prems_th1
414 handle Empty => raise Fail "Failed to find literal in th1"
415 val _ = trace_msg ctxt (fn () => " index_th1: " ^ string_of_int index_th1)
417 index_of_literal i_atm prems_th2
418 handle Empty => raise Fail "Failed to find literal in th2"
419 val _ = trace_msg ctxt (fn () => " index_th2: " ^ string_of_int index_th2)
421 resolve_inc_tyvars thy (select_literal thy index_th1 i_th1) index_th2
426 (* INFERENCE RULE: REFL *)
428 val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
430 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
431 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
433 fun refl_inf ctxt mode skolem_params t =
434 let val thy = ProofContext.theory_of ctxt
435 val i_t = singleton (hol_terms_from_metis ctxt mode skolem_params) t
436 val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
437 val c_t = cterm_incr_types thy refl_idx i_t
438 in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
440 (* INFERENCE RULE: EQUALITY *)
442 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
443 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
445 val metis_eq = Metis_Term.Fn ("=", []);
447 fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*)
448 | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
449 | get_ty_arg_size _ _ = 0;
451 fun equality_inf ctxt mode skolem_params (pos, atm) fp fr =
452 let val thy = ProofContext.theory_of ctxt
453 val m_tm = Metis_Term.Fn atm
454 val [i_atm,i_tm] = hol_terms_from_metis ctxt mode skolem_params [m_tm, fr]
455 val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
456 fun replace_item_list lx 0 (_::ls) = lx::ls
457 | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
458 fun path_finder_FO tm [] = (tm, Bound 0)
459 | path_finder_FO tm (p::ps) =
460 let val (tm1,args) = strip_comb tm
461 val adjustment = get_ty_arg_size thy tm1
462 val p' = if adjustment > p then p else p-adjustment
463 val tm_p = List.nth(args,p')
465 error ("Cannot replay Metis proof in Isabelle:\n" ^
466 "equality_inf: " ^ string_of_int p ^ " adj " ^
467 string_of_int adjustment ^ " term " ^
468 Syntax.string_of_term ctxt tm)
469 val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int p ^
470 " " ^ Syntax.string_of_term ctxt tm_p)
471 val (r,t) = path_finder_FO tm_p ps
473 (r, list_comb (tm1, replace_item_list t p' args))
475 fun path_finder_HO tm [] = (tm, Bound 0)
476 | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
477 | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
478 | path_finder_HO tm ps =
479 raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
480 "equality_inf, path_finder_HO: path = " ^
481 space_implode " " (map string_of_int ps) ^
482 " isa-term: " ^ Syntax.string_of_term ctxt tm)
483 fun path_finder_FT tm [] _ = (tm, 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 =
491 raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
492 "equality_inf, path_finder_FT: path = " ^
493 space_implode " " (map string_of_int ps) ^
494 " isa-term: " ^ Syntax.string_of_term ctxt tm ^
495 " fol-term: " ^ Metis_Term.toString t)
496 fun path_finder FO tm ps _ = path_finder_FO tm ps
497 | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
498 (*equality: not curried, as other predicates are*)
499 if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
500 else path_finder_HO tm (p::ps) (*1 selects second operand*)
501 | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
502 path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
503 | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
504 (Metis_Term.Fn ("=", [t1,t2])) =
505 (*equality: not curried, as other predicates are*)
506 if p=0 then path_finder_FT tm (0::1::ps)
507 (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2]))
508 (*select first operand*)
509 else path_finder_FT tm (p::ps)
510 (Metis_Term.Fn (".", [metis_eq,t2]))
511 (*1 selects second operand*)
512 | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
513 (*if not equality, ignore head to skip the hBOOL predicate*)
514 | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
515 fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
516 let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
517 in (tm, nt $ tm_rslt) end
518 | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
519 val (tm_subst, body) = path_finder_lit i_atm fp
520 val tm_abs = Abs ("x", type_of tm_subst, body)
521 val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
522 val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
523 val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
524 val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
525 val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
526 val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
527 val eq_terms = map (pairself (cterm_of thy))
528 (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
529 in cterm_instantiate eq_terms subst' end;
531 val factor = Seq.hd o distinct_subgoals_tac;
533 fun step ctxt mode skolem_params thpairs p =
535 (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
536 | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolem_params f_atm
537 | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
538 factor (inst_inf ctxt mode skolem_params thpairs f_subst f_th1)
539 | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
540 factor (resolve_inf ctxt mode skolem_params thpairs f_atm f_th1 f_th2)
541 | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolem_params f_tm
542 | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
543 equality_inf ctxt mode skolem_params f_lit f_p f_r
545 fun flexflex_first_order th =
546 case Thm.tpairs_of th of
549 let val thy = theory_of_thm th
551 fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
552 val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
553 val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
557 fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
558 fun is_isabelle_literal_genuine t =
559 case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
561 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
563 (* Seldomly needed hack. A Metis clause is represented as a set, so duplicate
564 disjuncts are impossible. In the Isabelle proof, in spite of efforts to
565 eliminate them, duplicates sometimes appear with slightly different (but
567 fun resynchronize ctxt fol_th th =
570 count is_metis_literal_genuine
571 (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
572 val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th)
574 if num_metis_lits >= num_isabelle_lits then
578 val (prems0, concl) = th |> prop_of |> Logic.strip_horn
579 val prems = prems0 |> distinct (uncurry untyped_aconv)
580 val goal = Logic.list_implies (prems, concl)
582 if length prems = length prems0 then
583 error "Cannot replay Metis proof in Isabelle: Out of sync."
585 Goal.prove ctxt [] [] goal (K (cut_rules_tac [th] 1
586 THEN ALLGOALS assume_tac))
587 |> resynchronize ctxt fol_th
591 fun replay_one_inference ctxt mode skolem_params (fol_th, inf) thpairs =
592 if not (null thpairs) andalso prop_of (snd (hd thpairs)) aconv @{prop False} then
593 (* Isabelle sometimes identifies literals (premises) that are distinct in
594 Metis (e.g., because of type variables). We give the Isabelle proof the
595 benefice of the doubt. *)
599 val _ = trace_msg ctxt
600 (fn () => "=============================================")
601 val _ = trace_msg ctxt
602 (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
603 val _ = trace_msg ctxt
604 (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
605 val th = step ctxt mode skolem_params thpairs (fol_th, inf)
606 |> flexflex_first_order
607 |> resynchronize ctxt fol_th
608 val _ = trace_msg ctxt
609 (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
610 val _ = trace_msg ctxt
611 (fn () => "=============================================")
612 in (fol_th, th) :: thpairs end
614 (* It is normally sufficient to apply "assume_tac" to unify the conclusion with
615 one of the premises. Unfortunately, this sometimes yields "Variable
616 ?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the
617 variables before applying "assume_tac". Typical constraints are of the form
618 ?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,
619 where the nonvariables are goal parameters. *)
620 fun unify_first_prem_with_concl thy i th =
622 val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
623 val prem = goal |> Logic.strip_assums_hyp |> hd
624 val concl = goal |> Logic.strip_assums_concl
625 fun pair_untyped_aconv (t1, t2) (u1, u2) =
626 untyped_aconv t1 u1 andalso untyped_aconv t2 u2
627 fun add_terms tp inst =
628 if exists (pair_untyped_aconv tp) inst then inst
629 else tp :: map (apsnd (subst_atomic [tp])) inst
632 (Var _, args) => forall is_Bound args
634 fun unify_flex flex rigid =
635 case strip_comb flex of
636 (Var (z as (_, T)), args) =>
638 fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
640 fun unify_potential_flex comb atom =
641 if is_flex comb then unify_flex comb atom
642 else if is_Var atom then add_terms (atom, comb)
644 fun unify_terms (t, u) =
646 (t1 $ t2, u1 $ u2) =>
647 if is_flex t then unify_flex t u
648 else if is_flex u then unify_flex u t
649 else fold unify_terms [(t1, u1), (t2, u2)]
650 | (_ $ _, _) => unify_potential_flex t u
651 | (_, _ $ _) => unify_potential_flex u t
652 | (Var _, _) => add_terms (t, u)
653 | (_, Var _) => add_terms (u, t)
655 val t_inst = [] |> unify_terms (prem, concl)
656 |> map (pairself (cterm_of thy))
657 in th |> cterm_instantiate t_inst end
659 val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
661 fun copy_prems_tac [] ns i =
662 if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
663 | copy_prems_tac (1 :: ms) ns i =
664 rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
665 | copy_prems_tac (m :: ms) ns i =
666 etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
668 (* Metis generates variables of the form _nnn. *)
669 val is_metis_fresh_variable = String.isPrefix "_"
671 fun instantiate_forall_tac thy t i st =
673 val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
674 fun repair (t as (Var ((s, _), _))) =
675 (case find_index (fn (s', _) => s' = s) params of
679 (case (repair t, repair u) of
680 (t as Bound j, u as Bound k) =>
681 (* This is a rather subtle trick to repair the discrepancy between
682 the fully skolemized term that MESON gives us (where existentials
683 were pulled out) and the reality. *)
684 if k > j then t else t $ u
687 val t' = t |> repair |> fold (curry absdummy) (map snd params)
688 fun do_instantiate th =
689 case Term.add_vars (prop_of th) []
690 |> filter_out ((Meson_Clausify.is_zapped_var_name orf
691 is_metis_fresh_variable) o fst o fst) of
695 val var_binder_Ts = T |> binder_types |> take (length params) |> rev
696 val var_body_T = T |> funpow (length params) range_type
698 Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
699 var_body_T :: var_binder_Ts)
701 Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
702 tenv = Vartab.empty, tyenv = tyenv}
704 Vartab.fold (fn (x, (S, T)) =>
705 cons (pairself (ctyp_of thy) (TVar (x, S), T)))
708 [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
709 in th |> instantiate (ty_inst, t_inst) end
710 | _ => raise Fail "expected a single non-zapped, non-Metis Var"
712 (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
713 THEN PRIMITIVE do_instantiate) st
716 fun fix_exists_tac t =
718 THEN' rename_tac [t |> dest_Var |> fst |> fst]
720 fun release_quantifier_tac thy (skolem, t) =
721 (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
723 fun release_clusters_tac _ _ _ [] = K all_tac
724 | release_clusters_tac thy ax_counts substs
725 ((ax_no, cluster_no) :: clusters) =
728 Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
729 fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
732 |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
733 if ax_no' = ax_no then
734 tsubst |> map (apfst cluster_of_var)
735 |> filter (in_right_cluster o fst)
740 fun do_cluster_subst cluster_subst =
741 map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
742 val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
744 rotate_tac first_prem
745 THEN' (EVERY' (maps do_cluster_subst cluster_substs))
746 THEN' rotate_tac (~ first_prem - length cluster_substs)
747 THEN' release_clusters_tac thy ax_counts substs clusters
750 fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
751 (ax_no, (cluster_no, (skolem, index_no)))
753 prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord))
754 (pairself cluster_key p)
757 list_ord (prod_ord Term_Ord.fast_indexname_ord
758 (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
760 structure Int_Tysubst_Table =
761 Table(type key = int * (indexname * (sort * typ)) list
762 val ord = prod_ord int_ord tysubst_ord)
764 structure Int_Pair_Graph =
765 Graph(type key = int * int val ord = prod_ord int_ord int_ord)
767 fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
768 fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
770 (* Attempts to derive the theorem "False" from a theorem of the form
771 "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
772 specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
773 must be eliminated first. *)
774 fun discharge_skolem_premises ctxt axioms prems_imp_false =
775 if prop_of prems_imp_false aconv @{prop False} then
779 val thy = ProofContext.theory_of ctxt
783 Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
786 |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
788 o pairself (Meson_Clausify.cluster_of_zapped_var_name
790 |> map (Meson.term_pair_of
791 #> pairself (Envir.subst_term_types tyenv))
792 val tysubst = tyenv |> Vartab.dest
793 in (tysubst, tsubst) end
794 fun subst_info_for_prem subgoal_no prem =
796 _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
797 let val ax_no = HOLogic.dest_nat num in
799 match_term (nth axioms ax_no |> the |> snd, t)))
801 | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
803 fun cluster_of_var_name skolem s =
804 case try Meson_Clausify.cluster_of_zapped_var_name s of
806 | SOME ((ax_no, (cluster_no, _)), skolem') =>
807 if skolem' = skolem andalso cluster_no > 0 then
808 SOME (ax_no, cluster_no)
811 fun clusters_in_term skolem t =
812 Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
813 fun deps_for_term_subst (var, t) =
814 case clusters_in_term false var of
816 | [(ax_no, cluster_no)] =>
817 SOME ((ax_no, cluster_no),
818 clusters_in_term true t
819 |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
820 | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
821 val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
822 val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
823 |> sort (int_ord o pairself fst)
824 val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
825 val clusters = maps (op ::) depss
826 val ordered_clusters =
828 |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
829 |> fold Int_Pair_Graph.add_deps_acyclic depss
830 |> Int_Pair_Graph.topological_order
831 handle Int_Pair_Graph.CYCLES _ =>
832 error "Cannot replay Metis proof in Isabelle without \
833 \\"Hilbert_Choice\"."
835 Int_Tysubst_Table.empty
836 |> fold (fn (ax_no, (_, (tysubst, _))) =>
837 Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
838 (Integer.add 1)) substs
839 |> Int_Tysubst_Table.dest
840 val needed_axiom_props =
841 0 upto length axioms - 1 ~~ axioms
842 |> map_filter (fn (_, NONE) => NONE
843 | (ax_no, SOME (_, t)) =>
844 if exists (fn ((ax_no', _), n) =>
845 ax_no' = ax_no andalso n > 0)
850 val outer_param_names =
851 [] |> fold Term.add_var_names needed_axiom_props
852 |> filter (Meson_Clausify.is_zapped_var_name o fst)
853 |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
854 |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
855 cluster_no = 0 andalso skolem)
856 |> sort shuffle_ord |> map (fst o snd)
857 (* for debugging only:
858 fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
859 "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
860 "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
861 commas (map ((fn (s, t) => s ^ " |-> " ^ t)
862 o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
863 val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
864 val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
865 val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
866 val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
867 cat_lines (map string_for_subst_info substs))
869 fun cut_and_ex_tac axiom =
870 cut_rules_tac [axiom] 1
871 THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
872 fun rotation_for_subgoal i =
873 find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
875 Goal.prove ctxt [] [] @{prop False}
876 (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
878 THEN rename_tac outer_param_names 1
879 THEN copy_prems_tac (map snd ax_counts) [] 1)
880 THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
881 THEN match_tac [prems_imp_false] 1
882 THEN ALLGOALS (fn i =>
883 rtac @{thm Meson.skolem_COMBK_I} i
884 THEN rotate_tac (rotation_for_subgoal i) i
885 THEN PRIMITIVE (unify_first_prem_with_concl thy i)
889 error ("Cannot replay Metis proof in Isabelle:\n\
890 \Error when discharging Skolem assumptions.")
893 val setup = trace_setup #> verbose_setup