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 exception METIS of string * string
14 val hol_clause_from_metis :
15 Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
17 val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
18 val untyped_aconv : term * term -> bool
19 val replay_one_inference :
20 Proof.context -> (string * term) list -> int Symtab.table
21 -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
22 -> (Metis_Thm.thm * thm) list
23 val discharge_skolem_premises :
24 Proof.context -> (thm * term) option list -> thm -> thm
27 structure Metis_Reconstruct : METIS_RECONSTRUCT =
35 exception METIS of string * string
37 datatype term_or_type = SomeTerm of term | SomeType of typ
40 | terms_of (SomeTerm t :: tts) = t :: terms_of tts
41 | terms_of (SomeType _ :: tts) = terms_of tts;
44 | types_of (SomeTerm (Var ((a, idx), _)) :: tts) =
46 |> (if String.isPrefix metis_generated_var_prefix a then
47 (* Variable generated by Metis, which might have been a type
49 cons (TVar (("'" ^ a, idx), HOLogic.typeS))
52 | types_of (SomeTerm _ :: tts) = types_of tts
53 | types_of (SomeType T :: tts) = T :: types_of tts
55 fun atp_name_from_metis s =
56 case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
57 SOME ((s, _), (_, swap)) => (s, swap)
59 fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
60 let val (s, swap) = atp_name_from_metis (Metis_Name.toString s) in
61 ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
63 | atp_term_from_metis (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
65 fun hol_term_from_metis ctxt sym_tab =
66 atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
68 fun atp_literal_from_metis (pos, atom) =
69 atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot
70 fun atp_clause_from_metis [] = AAtom (ATerm (tptp_false, []))
71 | atp_clause_from_metis lits =
72 lits |> map atp_literal_from_metis |> mk_aconns AOr
74 fun reveal_old_skolems_and_infer_types ctxt old_skolems =
75 map (reveal_old_skolem_terms old_skolems)
76 #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
78 fun hol_clause_from_metis ctxt sym_tab old_skolems =
80 #> Metis_LiteralSet.toList
81 #> atp_clause_from_metis
82 #> prop_from_atp ctxt false sym_tab
83 #> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems)
85 fun hol_terms_from_metis ctxt old_skolems sym_tab fol_tms =
86 let val ts = map (hol_term_from_metis ctxt sym_tab) fol_tms
87 val _ = trace_msg ctxt (fn () => " calling type inference:")
88 val _ = app (fn t => trace_msg ctxt
89 (fn () => Syntax.string_of_term ctxt t)) ts
91 ts |> reveal_old_skolems_and_infer_types ctxt old_skolems
92 val _ = app (fn t => trace_msg ctxt
93 (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
94 " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
98 (* ------------------------------------------------------------------------- *)
99 (* FOL step Inference Rules *)
100 (* ------------------------------------------------------------------------- *)
102 (*for debugging only*)
104 fun print_thpair ctxt (fth,th) =
105 (trace_msg ctxt (fn () => "=============================================");
106 trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth);
107 trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
110 fun lookth th_pairs fth =
111 the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
112 handle Option.Option =>
113 raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
115 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
117 (* INFERENCE RULE: AXIOM *)
119 (* This causes variables to have an index of 1 by default. See also
120 "term_from_atp" in "ATP_Reconstruct". *)
121 val axiom_inference = Thm.incr_indexes 1 oo lookth
123 (* INFERENCE RULE: ASSUME *)
125 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
127 fun inst_excluded_middle thy i_atom =
128 let val th = EXCLUDED_MIDDLE
129 val [vx] = Term.add_vars (prop_of th) []
130 val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
131 in cterm_instantiate substs th end;
133 fun assume_inference ctxt old_skolems sym_tab atom =
135 (Proof_Context.theory_of ctxt)
136 (singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
137 (Metis_Term.Fn atom))
139 (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
140 to reconstruct them admits new possibilities of errors, e.g. concerning
141 sorts. Instead we try to arrange that new TVars are distinct and that types
142 can be inferred from terms. *)
144 fun inst_inference ctxt old_skolems sym_tab th_pairs fsubst th =
145 let val thy = Proof_Context.theory_of ctxt
146 val i_th = lookth th_pairs th
147 val i_th_vars = Term.add_vars (prop_of i_th) []
148 fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
149 fun subst_translation (x,y) =
150 let val v = find_var x
151 (* We call "reveal_old_skolems_and_infer_types" below. *)
152 val t = hol_term_from_metis ctxt sym_tab y
153 in SOME (cterm_of thy (Var v), t) end
154 handle Option.Option =>
155 (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
156 " in " ^ Display.string_of_thm ctxt i_th);
159 (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
160 " in " ^ Display.string_of_thm ctxt i_th);
162 fun remove_typeinst (a, t) =
163 let val a = Metis_Name.toString a in
164 case strip_prefix_and_unascii schematic_var_prefix a of
165 SOME b => SOME (b, t)
167 case strip_prefix_and_unascii tvar_prefix a of
168 SOME _ => NONE (* type instantiations are forbidden *)
169 | NONE => SOME (a, t) (* internal Metis var? *)
171 val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
172 val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
174 ListPair.unzip (map_filter subst_translation substs)
175 ||> reveal_old_skolems_and_infer_types ctxt old_skolems
176 val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
177 val substs' = ListPair.zip (vars, map ctm_of tms)
178 val _ = trace_msg ctxt (fn () =>
179 cat_lines ("subst_translations:" ::
180 (substs' |> map (fn (x, y) =>
181 Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
182 Syntax.string_of_term ctxt (term_of y)))));
183 in cterm_instantiate substs' i_th end
184 handle THM (msg, _, _) => raise METIS ("inst_inference", msg)
185 | ERROR msg => raise METIS ("inst_inference", msg)
187 (* INFERENCE RULE: RESOLVE *)
189 (* Like RSN, but we rename apart only the type variables. Vars here typically
190 have an index of 1, and the use of RSN would increase this typically to 3.
191 Instantiations of those Vars could then fail. See comment on "make_var". *)
192 fun resolve_inc_tyvars thy tha i thb =
194 val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
196 case Thm.bicompose false (false, tha, nprems_of tha) i thb
197 |> Seq.list_of |> distinct Thm.eq_thm of
199 | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
204 (* The unifier, which is invoked from "Thm.bicompose", will sometimes
205 refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
206 "TERM" exception (with "add_ffpair" as first argument). We then
207 perform unification of the types of variables by hand and try
208 again. We could do this the first time around but this error
209 occurs seldom and we don't want to break existing proofs in subtle
210 ways or slow them down needlessly. *)
211 case [] |> fold (Term.add_vars o prop_of) [tha, thb]
212 |> AList.group (op =)
213 |> maps (fn ((s, _), T :: Ts) =>
214 map (fn T' => (Free (s, T), Free (s, T'))) Ts)
215 |> rpair (Envir.empty ~1)
216 |-> fold (Pattern.unify thy)
217 |> Envir.type_env |> Vartab.dest
218 |> map (fn (x, (S, T)) =>
219 pairself (ctyp_of thy) (TVar (x, S), T)) of
221 | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
224 fun s_not (@{const Not} $ t) = t
225 | s_not t = HOLogic.mk_not t
226 fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t
227 | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
230 (* Match untyped terms. *)
231 fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b)
232 | untyped_aconv (Free (a, _), Free (b, _)) = (a = b)
233 | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) =
234 (a = b) (* ignore variable numbers *)
235 | untyped_aconv (Bound i, Bound j) = (i = j)
236 | untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u)
237 | untyped_aconv (t1 $ t2, u1 $ u2) =
238 untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2)
239 | untyped_aconv _ = false
241 val normalize_literal = simp_not_not o Envir.eta_contract
243 (* Find the relative location of an untyped term within a list of terms as a
244 1-based index. Returns 0 in case of failure. *)
245 fun index_of_literal lit haystack =
247 fun match_lit normalize =
248 HOLogic.dest_Trueprop #> normalize
249 #> curry untyped_aconv (lit |> normalize)
251 (case find_index (match_lit I) haystack of
252 ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack
256 (* Permute a rule's premises to move the i-th premise to the last position. *)
258 let val n = nprems_of th
259 in if 1 <= i andalso i <= n
260 then Thm.permute_prems (i-1) 1 th
261 else raise THM("select_literal", i, [th])
264 (* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
265 to create double negations. The "select" wrapper is a trick to ensure that
266 "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
267 don't use this trick in general because it makes the proof object uglier than
270 if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
271 (th RS @{thm select_FalseI})
272 |> fold (rewrite_rule o single)
273 @{thms not_atomize_select atomize_not_select}
275 th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not}
277 (* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
278 val select_literal = negate_head oo make_last
280 fun resolve_inference ctxt old_skolems sym_tab th_pairs atom th1 th2 =
282 val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
283 val _ = trace_msg ctxt (fn () =>
284 " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\
285 \ isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
287 (* Trivial cases where one operand is type info *)
288 if Thm.eq_thm (TrueI, i_th1) then
290 else if Thm.eq_thm (TrueI, i_th2) then
294 val thy = Proof_Context.theory_of ctxt
296 singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
298 val _ = trace_msg ctxt (fn () =>
299 " atom: " ^ Syntax.string_of_term ctxt i_atom)
301 case index_of_literal (s_not i_atom) (prems_of i_th1) of
303 (trace_msg ctxt (fn () => "Failed to find literal in \"th1\"");
306 (trace_msg ctxt (fn () => " index th1: " ^ string_of_int j1);
307 case index_of_literal i_atom (prems_of i_th2) of
309 (trace_msg ctxt (fn () => "Failed to find literal in \"th2\"");
312 (trace_msg ctxt (fn () => " index th2: " ^ string_of_int j2);
313 resolve_inc_tyvars thy (select_literal j1 i_th1) j2 i_th2
314 handle TERM (s, _) => raise METIS ("resolve_inference", s)))
318 (* INFERENCE RULE: REFL *)
320 val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
322 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
323 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
325 fun refl_inference ctxt old_skolems sym_tab t =
327 val thy = Proof_Context.theory_of ctxt
328 val i_t = singleton (hol_terms_from_metis ctxt old_skolems sym_tab) t
329 val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
330 val c_t = cterm_incr_types thy refl_idx i_t
331 in cterm_instantiate [(refl_x, c_t)] REFL_THM end
333 (* INFERENCE RULE: EQUALITY *)
335 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
336 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
338 fun equality_inference ctxt old_skolems sym_tab (pos, atom) fp fr =
339 let val thy = Proof_Context.theory_of ctxt
340 val m_tm = Metis_Term.Fn atom
342 hol_terms_from_metis ctxt old_skolems sym_tab [m_tm, fr]
343 val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
344 fun replace_item_list lx 0 (_::ls) = lx::ls
345 | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
346 fun path_finder_fail tm ps t =
347 raise METIS ("equality_inference (path_finder)",
348 "path = " ^ space_implode " " (map string_of_int ps) ^
349 " isa-term: " ^ Syntax.string_of_term ctxt tm ^
351 SOME t => " fol-term: " ^ Metis_Term.toString t
353 fun path_finder tm [] _ = (tm, Bound 0)
354 | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
356 val s = s |> Metis_Name.toString
357 |> perhaps (try (strip_prefix_and_unascii const_prefix
358 #> the #> unmangled_const_name))
360 if s = metis_predicator orelse s = predicator_name orelse
361 s = metis_type_tag orelse s = type_tag_name then
362 path_finder tm ps (nth ts p)
363 else if s = metis_app_op orelse s = app_op_name then
365 val (tm1, tm2) = dest_comb tm
366 val p' = p - (length ts - 2)
369 path_finder tm1 ps (nth ts p) ||> (fn y => y $ tm2)
371 path_finder tm2 ps (nth ts p) ||> (fn y => tm1 $ y)
375 val (tm1, args) = strip_comb tm
376 val adjustment = length ts - length args
377 val p' = if adjustment > p then p else p - adjustment
380 handle Subscript => path_finder_fail tm (p :: ps) (SOME t)
381 val _ = trace_msg ctxt (fn () =>
382 "path_finder: " ^ string_of_int p ^ " " ^
383 Syntax.string_of_term ctxt tm_p)
384 val (r, t) = path_finder tm_p ps (nth ts p)
385 in (r, list_comb (tm1, replace_item_list t p' args)) end
387 | path_finder tm ps t = path_finder_fail tm ps (SOME t)
388 val (tm_subst, body) = path_finder i_atom fp m_tm
389 val tm_abs = Abs ("x", type_of tm_subst, body)
390 val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
391 val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
392 val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
393 val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
394 val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
395 val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
396 val eq_terms = map (pairself (cterm_of thy))
397 (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
398 in cterm_instantiate eq_terms subst' end;
400 val factor = Seq.hd o distinct_subgoals_tac
402 fun one_step ctxt old_skolems sym_tab th_pairs p =
404 (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
405 | (_, Metis_Proof.Assume f_atom) =>
406 assume_inference ctxt old_skolems sym_tab f_atom
407 | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
408 inst_inference ctxt old_skolems sym_tab th_pairs f_subst f_th1
410 | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
411 resolve_inference ctxt old_skolems sym_tab th_pairs f_atom f_th1 f_th2
413 | (_, Metis_Proof.Refl f_tm) =>
414 refl_inference ctxt old_skolems sym_tab f_tm
415 | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
416 equality_inference ctxt old_skolems sym_tab f_lit f_p f_r
418 fun flexflex_first_order th =
419 case Thm.tpairs_of th of
422 let val thy = theory_of_thm th
424 fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
425 val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
426 val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
430 fun is_metis_literal_genuine (_, (s, _)) =
431 not (String.isPrefix class_prefix (Metis_Name.toString s))
432 fun is_isabelle_literal_genuine t =
433 case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
435 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
437 (* Seldomly needed hack. A Metis clause is represented as a set, so duplicate
438 disjuncts are impossible. In the Isabelle proof, in spite of efforts to
439 eliminate them, duplicates sometimes appear with slightly different (but
441 fun resynchronize ctxt fol_th th =
444 count is_metis_literal_genuine
445 (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
446 val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th)
448 if num_metis_lits >= num_isabelle_lits then
452 val (prems0, concl) = th |> prop_of |> Logic.strip_horn
453 val prems = prems0 |> map normalize_literal
454 |> distinct untyped_aconv
455 val goal = Logic.list_implies (prems, concl)
456 val tac = cut_rules_tac [th] 1
457 THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
458 THEN ALLGOALS assume_tac
460 if length prems = length prems0 then
461 raise METIS ("resynchronize", "Out of sync")
463 Goal.prove ctxt [] [] goal (K tac)
464 |> resynchronize ctxt fol_th
468 fun replay_one_inference ctxt old_skolems sym_tab (fol_th, inf) th_pairs =
469 if not (null th_pairs) andalso
470 prop_of (snd (hd th_pairs)) aconv @{prop False} then
471 (* Isabelle sometimes identifies literals (premises) that are distinct in
472 Metis (e.g., because of type variables). We give the Isabelle proof the
473 benefice of the doubt. *)
477 val _ = trace_msg ctxt
478 (fn () => "=============================================")
479 val _ = trace_msg ctxt
480 (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
481 val _ = trace_msg ctxt
482 (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
483 val th = one_step ctxt old_skolems sym_tab th_pairs (fol_th, inf)
484 |> flexflex_first_order
485 |> resynchronize ctxt fol_th
486 val _ = trace_msg ctxt
487 (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
488 val _ = trace_msg ctxt
489 (fn () => "=============================================")
490 in (fol_th, th) :: th_pairs end
492 (* It is normally sufficient to apply "assume_tac" to unify the conclusion with
493 one of the premises. Unfortunately, this sometimes yields "Variable
494 ?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the
495 variables before applying "assume_tac". Typical constraints are of the form
496 ?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,
497 where the nonvariables are goal parameters. *)
498 fun unify_first_prem_with_concl thy i th =
500 val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
501 val prem = goal |> Logic.strip_assums_hyp |> hd
502 val concl = goal |> Logic.strip_assums_concl
503 fun pair_untyped_aconv (t1, t2) (u1, u2) =
504 untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2)
505 fun add_terms tp inst =
506 if exists (pair_untyped_aconv tp) inst then inst
507 else tp :: map (apsnd (subst_atomic [tp])) inst
510 (Var _, args) => forall is_Bound args
512 fun unify_flex flex rigid =
513 case strip_comb flex of
514 (Var (z as (_, T)), args) =>
516 fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
518 fun unify_potential_flex comb atom =
519 if is_flex comb then unify_flex comb atom
520 else if is_Var atom then add_terms (atom, comb)
522 fun unify_terms (t, u) =
524 (t1 $ t2, u1 $ u2) =>
525 if is_flex t then unify_flex t u
526 else if is_flex u then unify_flex u t
527 else fold unify_terms [(t1, u1), (t2, u2)]
528 | (_ $ _, _) => unify_potential_flex t u
529 | (_, _ $ _) => unify_potential_flex u t
530 | (Var _, _) => add_terms (t, u)
531 | (_, Var _) => add_terms (u, t)
534 [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy)))
535 |> the_default [] (* FIXME *)
536 in th |> cterm_instantiate t_inst end
538 val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
540 fun copy_prems_tac [] ns i =
541 if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
542 | copy_prems_tac (1 :: ms) ns i =
543 rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
544 | copy_prems_tac (m :: ms) ns i =
545 etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
547 (* Metis generates variables of the form _nnn. *)
548 val is_metis_fresh_variable = String.isPrefix "_"
550 fun instantiate_forall_tac thy t i st =
552 val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
553 fun repair (t as (Var ((s, _), _))) =
554 (case find_index (fn (s', _) => s' = s) params of
558 (case (repair t, repair u) of
559 (t as Bound j, u as Bound k) =>
560 (* This is a rather subtle trick to repair the discrepancy between
561 the fully skolemized term that MESON gives us (where existentials
562 were pulled out) and the reality. *)
563 if k > j then t else t $ u
566 val t' = t |> repair |> fold (curry absdummy) (map snd params)
567 fun do_instantiate th =
568 case Term.add_vars (prop_of th) []
569 |> filter_out ((Meson_Clausify.is_zapped_var_name orf
570 is_metis_fresh_variable) o fst o fst) of
574 val var_binder_Ts = T |> binder_types |> take (length params) |> rev
575 val var_body_T = T |> funpow (length params) range_type
577 Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
578 var_body_T :: var_binder_Ts)
580 Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
581 tenv = Vartab.empty, tyenv = tyenv}
583 Vartab.fold (fn (x, (S, T)) =>
584 cons (pairself (ctyp_of thy) (TVar (x, S), T)))
587 [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
588 in th |> instantiate (ty_inst, t_inst) end
589 | _ => raise Fail "expected a single non-zapped, non-Metis Var"
591 (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
592 THEN PRIMITIVE do_instantiate) st
595 fun fix_exists_tac t =
596 etac @{thm exE} THEN' rename_tac [t |> dest_Var |> fst |> fst]
598 fun release_quantifier_tac thy (skolem, t) =
599 (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
601 fun release_clusters_tac _ _ _ [] = K all_tac
602 | release_clusters_tac thy ax_counts substs
603 ((ax_no, cluster_no) :: clusters) =
606 Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
607 fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
610 |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
611 if ax_no' = ax_no then
612 tsubst |> map (apfst cluster_of_var)
613 |> filter (in_right_cluster o fst)
618 fun do_cluster_subst cluster_subst =
619 map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
620 val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
622 rotate_tac first_prem
623 THEN' (EVERY' (maps do_cluster_subst cluster_substs))
624 THEN' rotate_tac (~ first_prem - length cluster_substs)
625 THEN' release_clusters_tac thy ax_counts substs clusters
628 fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
629 (ax_no, (cluster_no, (skolem, index_no)))
631 prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord))
632 (pairself cluster_key p)
635 list_ord (prod_ord Term_Ord.fast_indexname_ord
636 (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
638 structure Int_Tysubst_Table =
639 Table(type key = int * (indexname * (sort * typ)) list
640 val ord = prod_ord int_ord tysubst_ord)
642 structure Int_Pair_Graph =
643 Graph(type key = int * int val ord = prod_ord int_ord int_ord)
645 fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
646 fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
648 (* Attempts to derive the theorem "False" from a theorem of the form
649 "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
650 specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
651 must be eliminated first. *)
652 fun discharge_skolem_premises ctxt axioms prems_imp_false =
653 if prop_of prems_imp_false aconv @{prop False} then
657 val thy = Proof_Context.theory_of ctxt
661 Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
664 |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
666 o pairself (Meson_Clausify.cluster_of_zapped_var_name
668 |> map (Meson.term_pair_of
669 #> pairself (Envir.subst_term_types tyenv))
670 val tysubst = tyenv |> Vartab.dest
671 in (tysubst, tsubst) end
672 fun subst_info_for_prem subgoal_no prem =
674 _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
675 let val ax_no = HOLogic.dest_nat num in
677 match_term (nth axioms ax_no |> the |> snd, t)))
679 | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
681 fun cluster_of_var_name skolem s =
682 case try Meson_Clausify.cluster_of_zapped_var_name s of
684 | SOME ((ax_no, (cluster_no, _)), skolem') =>
685 if skolem' = skolem andalso cluster_no > 0 then
686 SOME (ax_no, cluster_no)
689 fun clusters_in_term skolem t =
690 Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
691 fun deps_for_term_subst (var, t) =
692 case clusters_in_term false var of
694 | [(ax_no, cluster_no)] =>
695 SOME ((ax_no, cluster_no),
696 clusters_in_term true t
697 |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
698 | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
699 val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
700 val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
701 |> sort (int_ord o pairself fst)
702 val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
703 val clusters = maps (op ::) depss
704 val ordered_clusters =
706 |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
707 |> fold Int_Pair_Graph.add_deps_acyclic depss
708 |> Int_Pair_Graph.topological_order
709 handle Int_Pair_Graph.CYCLES _ =>
710 error "Cannot replay Metis proof in Isabelle without \
711 \\"Hilbert_Choice\"."
713 Int_Tysubst_Table.empty
714 |> fold (fn (ax_no, (_, (tysubst, _))) =>
715 Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
716 (Integer.add 1)) substs
717 |> Int_Tysubst_Table.dest
718 val needed_axiom_props =
719 0 upto length axioms - 1 ~~ axioms
720 |> map_filter (fn (_, NONE) => NONE
721 | (ax_no, SOME (_, t)) =>
722 if exists (fn ((ax_no', _), n) =>
723 ax_no' = ax_no andalso n > 0)
728 val outer_param_names =
729 [] |> fold Term.add_var_names needed_axiom_props
730 |> filter (Meson_Clausify.is_zapped_var_name o fst)
731 |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
732 |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
733 cluster_no = 0 andalso skolem)
734 |> sort shuffle_ord |> map (fst o snd)
735 (* for debugging only:
736 fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
737 "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
738 "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
739 commas (map ((fn (s, t) => s ^ " |-> " ^ t)
740 o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
741 val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
742 val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
743 val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
744 val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
745 cat_lines (map string_for_subst_info substs))
747 fun cut_and_ex_tac axiom =
748 cut_rules_tac [axiom] 1
749 THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
750 fun rotation_for_subgoal i =
751 find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
753 Goal.prove ctxt [] [] @{prop False}
754 (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
756 THEN rename_tac outer_param_names 1
757 THEN copy_prems_tac (map snd ax_counts) [] 1)
758 THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
759 THEN match_tac [prems_imp_false] 1
760 THEN ALLGOALS (fn i =>
761 rtac @{thm Meson.skolem_COMBK_I} i
762 THEN rotate_tac (rotation_for_subgoal i) i
763 THEN PRIMITIVE (unify_first_prem_with_concl thy i)
767 error ("Cannot replay Metis proof in Isabelle:\n\
768 \Error when discharging Skolem assumptions.")