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 type_enc = ATP_Translate.type_enc
14 exception METIS of string * string
16 val hol_clause_from_metis :
17 Proof.context -> type_enc -> int Symtab.table
18 -> (string * term) list * (string * term) list -> Metis_Thm.thm -> term
19 val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
20 val replay_one_inference :
21 Proof.context -> type_enc
22 -> (string * term) list * (string * term) list -> int Symtab.table
23 -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
24 -> (Metis_Thm.thm * thm) list
25 val discharge_skolem_premises :
26 Proof.context -> (thm * term) option list -> thm -> thm
29 structure Metis_Reconstruct : METIS_RECONSTRUCT =
37 exception METIS of string * string
39 fun atp_name_from_metis type_enc s =
40 case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
41 SOME ((s, _), (_, swap)) => (s, swap)
43 fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) =
44 let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in
45 ATerm (s, tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
47 | atp_term_from_metis _ (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
49 fun hol_term_from_metis ctxt type_enc sym_tab =
50 atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE
52 fun atp_literal_from_metis type_enc (pos, atom) =
53 atom |> Metis_Term.Fn |> atp_term_from_metis type_enc
54 |> AAtom |> not pos ? mk_anot
55 fun atp_clause_from_metis _ [] = AAtom (ATerm (tptp_false, []))
56 | atp_clause_from_metis type_enc lits =
57 lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
59 fun polish_hol_terms ctxt (lifted, old_skolems) =
60 map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems)
61 #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
63 fun hol_clause_from_metis ctxt type_enc sym_tab concealed =
65 #> Metis_LiteralSet.toList
66 #> atp_clause_from_metis type_enc
67 #> prop_from_atp ctxt false sym_tab
68 #> singleton (polish_hol_terms ctxt concealed)
70 fun hol_terms_from_metis ctxt type_enc concealed sym_tab fol_tms =
71 let val ts = map (hol_term_from_metis ctxt type_enc sym_tab) fol_tms
72 val _ = trace_msg ctxt (fn () => " calling type inference:")
73 val _ = app (fn t => trace_msg ctxt
74 (fn () => Syntax.string_of_term ctxt t)) ts
75 val ts' = ts |> polish_hol_terms ctxt concealed
76 val _ = app (fn t => trace_msg ctxt
77 (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
78 " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
82 (* ------------------------------------------------------------------------- *)
83 (* FOL step Inference Rules *)
84 (* ------------------------------------------------------------------------- *)
86 (*for debugging only*)
88 fun print_thpair ctxt (fth,th) =
89 (trace_msg ctxt (fn () => "=============================================");
90 trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth);
91 trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
94 fun lookth th_pairs fth =
95 the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
96 handle Option.Option =>
97 raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
99 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
101 (* INFERENCE RULE: AXIOM *)
103 (* This causes variables to have an index of 1 by default. See also
104 "term_from_atp" in "ATP_Reconstruct". *)
105 val axiom_inference = Thm.incr_indexes 1 oo lookth
107 (* INFERENCE RULE: ASSUME *)
109 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
111 fun inst_excluded_middle thy i_atom =
112 let val th = EXCLUDED_MIDDLE
113 val [vx] = Term.add_vars (prop_of th) []
114 val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
115 in cterm_instantiate substs th end;
117 fun assume_inference ctxt type_enc concealed sym_tab atom =
119 (Proof_Context.theory_of ctxt)
120 (singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
121 (Metis_Term.Fn atom))
123 (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
124 to reconstruct them admits new possibilities of errors, e.g. concerning
125 sorts. Instead we try to arrange that new TVars are distinct and that types
126 can be inferred from terms. *)
128 fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th =
129 let val thy = Proof_Context.theory_of ctxt
130 val i_th = lookth th_pairs th
131 val i_th_vars = Term.add_vars (prop_of i_th) []
132 fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
133 fun subst_translation (x,y) =
134 let val v = find_var x
135 (* We call "polish_hol_terms" below. *)
136 val t = hol_term_from_metis ctxt type_enc sym_tab y
137 in SOME (cterm_of thy (Var v), t) end
138 handle Option.Option =>
139 (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
140 " in " ^ Display.string_of_thm ctxt i_th);
143 (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
144 " in " ^ Display.string_of_thm ctxt i_th);
146 fun remove_typeinst (a, t) =
147 let val a = Metis_Name.toString a in
148 case unprefix_and_unascii schematic_var_prefix a of
149 SOME b => SOME (b, t)
151 case unprefix_and_unascii tvar_prefix a of
152 SOME _ => NONE (* type instantiations are forbidden *)
153 | NONE => SOME (a, t) (* internal Metis var? *)
155 val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
156 val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
158 ListPair.unzip (map_filter subst_translation substs)
159 ||> polish_hol_terms ctxt concealed
160 val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
161 val substs' = ListPair.zip (vars, map ctm_of tms)
162 val _ = trace_msg ctxt (fn () =>
163 cat_lines ("subst_translations:" ::
164 (substs' |> map (fn (x, y) =>
165 Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
166 Syntax.string_of_term ctxt (term_of y)))));
167 in cterm_instantiate substs' i_th end
168 handle THM (msg, _, _) => raise METIS ("inst_inference", msg)
169 | ERROR msg => raise METIS ("inst_inference", msg)
171 (* INFERENCE RULE: RESOLVE *)
173 (*Increment the indexes of only the type variables*)
174 fun incr_type_indexes inc th =
175 let val tvs = Term.add_tvars (Thm.full_prop_of th) []
176 and thy = Thm.theory_of_thm th
177 fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s))
178 in Thm.instantiate (map inc_tvar tvs, []) th end;
180 (* Like RSN, but we rename apart only the type variables. Vars here typically
181 have an index of 1, and the use of RSN would increase this typically to 3.
182 Instantiations of those Vars could then fail. *)
183 fun resolve_inc_tyvars thy tha i thb =
185 val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
187 case Thm.bicompose false (false, tha, nprems_of tha) i thb
188 |> Seq.list_of |> distinct Thm.eq_thm of
190 | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
195 (* The unifier, which is invoked from "Thm.bicompose", will sometimes
196 refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
197 "TERM" exception (with "add_ffpair" as first argument). We then
198 perform unification of the types of variables by hand and try
199 again. We could do this the first time around but this error
200 occurs seldom and we don't want to break existing proofs in subtle
201 ways or slow them down needlessly. *)
202 case [] |> fold (Term.add_vars o prop_of) [tha, thb]
203 |> AList.group (op =)
204 |> maps (fn ((s, _), T :: Ts) =>
205 map (fn T' => (Free (s, T), Free (s, T'))) Ts)
206 |> rpair (Envir.empty ~1)
207 |-> fold (Pattern.unify thy)
208 |> Envir.type_env |> Vartab.dest
209 |> map (fn (x, (S, T)) =>
210 pairself (ctyp_of thy) (TVar (x, S), T)) of
212 | ps => (tha, thb) |> pairself (Drule.instantiate_normalize (ps, []))
216 fun s_not (@{const Not} $ t) = t
217 | s_not t = HOLogic.mk_not t
218 fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t
219 | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
222 val normalize_literal = simp_not_not o Envir.eta_contract
224 (* Find the relative location of an untyped term within a list of terms as a
225 1-based index. Returns 0 in case of failure. *)
226 fun index_of_literal lit haystack =
228 fun match_lit normalize =
229 HOLogic.dest_Trueprop #> normalize
230 #> curry Term.aconv_untyped (lit |> normalize)
232 (case find_index (match_lit I) haystack of
233 ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack
237 (* Permute a rule's premises to move the i-th premise to the last position. *)
239 let val n = nprems_of th
240 in if 1 <= i andalso i <= n
241 then Thm.permute_prems (i-1) 1 th
242 else raise THM("select_literal", i, [th])
245 (* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
246 to create double negations. The "select" wrapper is a trick to ensure that
247 "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
248 don't use this trick in general because it makes the proof object uglier than
251 if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
252 (th RS @{thm select_FalseI})
253 |> fold (rewrite_rule o single)
254 @{thms not_atomize_select atomize_not_select}
256 th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not}
258 (* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
259 val select_literal = negate_head oo make_last
261 fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 =
263 val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
264 val _ = trace_msg ctxt (fn () =>
265 " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\
266 \ isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
268 (* Trivial cases where one operand is type info *)
269 if Thm.eq_thm (TrueI, i_th1) then
271 else if Thm.eq_thm (TrueI, i_th2) then
275 val thy = Proof_Context.theory_of ctxt
277 singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
279 val _ = trace_msg ctxt (fn () =>
280 " atom: " ^ Syntax.string_of_term ctxt i_atom)
282 case index_of_literal (s_not i_atom) (prems_of i_th1) of
284 (trace_msg ctxt (fn () => "Failed to find literal in \"th1\"");
287 (trace_msg ctxt (fn () => " index th1: " ^ string_of_int j1);
288 case index_of_literal i_atom (prems_of i_th2) of
290 (trace_msg ctxt (fn () => "Failed to find literal in \"th2\"");
293 (trace_msg ctxt (fn () => " index th2: " ^ string_of_int j2);
294 resolve_inc_tyvars thy (select_literal j1 i_th1) j2 i_th2
295 handle TERM (s, _) => raise METIS ("resolve_inference", s)))
299 (* INFERENCE RULE: REFL *)
301 val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
303 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
304 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
306 fun refl_inference ctxt type_enc concealed sym_tab t =
308 val thy = Proof_Context.theory_of ctxt
310 singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab) t
311 val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
312 val c_t = cterm_incr_types thy refl_idx i_t
313 in cterm_instantiate [(refl_x, c_t)] REFL_THM end
315 (* INFERENCE RULE: EQUALITY *)
317 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
318 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
320 fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr =
321 let val thy = Proof_Context.theory_of ctxt
322 val m_tm = Metis_Term.Fn atom
324 hol_terms_from_metis ctxt type_enc concealed sym_tab [m_tm, fr]
325 val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
326 fun replace_item_list lx 0 (_::ls) = lx::ls
327 | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
328 fun path_finder_fail tm ps t =
329 raise METIS ("equality_inference (path_finder)",
330 "path = " ^ space_implode " " (map string_of_int ps) ^
331 " isa-term: " ^ Syntax.string_of_term ctxt tm ^
333 SOME t => " fol-term: " ^ Metis_Term.toString t
335 fun path_finder tm [] _ = (tm, Bound 0)
336 | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
338 val s = s |> Metis_Name.toString
339 |> perhaps (try (unprefix_and_unascii const_prefix
340 #> the #> unmangled_const_name))
342 if s = metis_predicator orelse s = predicator_name orelse
343 s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag
344 orelse s = type_tag_name then
345 path_finder tm ps (nth ts p)
346 else if s = metis_app_op orelse s = app_op_name then
348 val (tm1, tm2) = dest_comb tm
349 val p' = p - (length ts - 2)
352 path_finder tm1 ps (nth ts p) ||> (fn y => y $ tm2)
354 path_finder tm2 ps (nth ts p) ||> (fn y => tm1 $ y)
358 val (tm1, args) = strip_comb tm
359 val adjustment = length ts - length args
360 val p' = if adjustment > p then p else p - adjustment
363 handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t)
364 val _ = trace_msg ctxt (fn () =>
365 "path_finder: " ^ string_of_int p ^ " " ^
366 Syntax.string_of_term ctxt tm_p)
367 val (r, t) = path_finder tm_p ps (nth ts p)
368 in (r, list_comb (tm1, replace_item_list t p' args)) end
370 | path_finder tm ps t = path_finder_fail tm ps (SOME t)
371 val (tm_subst, body) = path_finder i_atom fp m_tm
372 val tm_abs = Abs ("x", type_of tm_subst, body)
373 val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
374 val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
375 val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
376 val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
377 val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
378 val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
379 val eq_terms = map (pairself (cterm_of thy))
380 (ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
381 in cterm_instantiate eq_terms subst' end;
383 val factor = Seq.hd o distinct_subgoals_tac
385 fun one_step ctxt type_enc concealed sym_tab th_pairs p =
387 (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
388 | (_, Metis_Proof.Assume f_atom) =>
389 assume_inference ctxt type_enc concealed sym_tab f_atom
390 | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
391 inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1
393 | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
394 resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1
397 | (_, Metis_Proof.Refl f_tm) =>
398 refl_inference ctxt type_enc concealed sym_tab f_tm
399 | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
400 equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r
402 fun flexflex_first_order th =
403 case Thm.tpairs_of th of
406 let val thy = theory_of_thm th
408 fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
409 val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
410 val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
414 fun is_metis_literal_genuine (_, (s, _)) =
415 not (String.isPrefix class_prefix (Metis_Name.toString s))
416 fun is_isabelle_literal_genuine t =
417 case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
419 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
421 (* Seldomly needed hack. A Metis clause is represented as a set, so duplicate
422 disjuncts are impossible. In the Isabelle proof, in spite of efforts to
423 eliminate them, duplicates sometimes appear with slightly different (but
425 fun resynchronize ctxt fol_th th =
428 count is_metis_literal_genuine
429 (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
430 val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th)
432 if num_metis_lits >= num_isabelle_lits then
436 val (prems0, concl) = th |> prop_of |> Logic.strip_horn
437 val prems = prems0 |> map normalize_literal
438 |> distinct Term.aconv_untyped
439 val goal = Logic.list_implies (prems, concl)
440 val tac = cut_rules_tac [th] 1
441 THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
442 THEN ALLGOALS assume_tac
444 if length prems = length prems0 then
445 raise METIS ("resynchronize", "Out of sync")
447 Goal.prove ctxt [] [] goal (K tac)
448 |> resynchronize ctxt fol_th
452 fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf)
454 if not (null th_pairs) andalso
455 prop_of (snd (hd th_pairs)) aconv @{prop False} then
456 (* Isabelle sometimes identifies literals (premises) that are distinct in
457 Metis (e.g., because of type variables). We give the Isabelle proof the
458 benefice of the doubt. *)
462 val _ = trace_msg ctxt
463 (fn () => "=============================================")
464 val _ = trace_msg ctxt
465 (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
466 val _ = trace_msg ctxt
467 (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
468 val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
469 |> flexflex_first_order
470 |> resynchronize ctxt fol_th
471 val _ = trace_msg ctxt
472 (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
473 val _ = trace_msg ctxt
474 (fn () => "=============================================")
475 in (fol_th, th) :: th_pairs end
477 (* It is normally sufficient to apply "assume_tac" to unify the conclusion with
478 one of the premises. Unfortunately, this sometimes yields "Variable
479 ?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the
480 variables before applying "assume_tac". Typical constraints are of the form
481 ?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,
482 where the nonvariables are goal parameters. *)
483 fun unify_first_prem_with_concl thy i th =
485 val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
486 val prem = goal |> Logic.strip_assums_hyp |> hd
487 val concl = goal |> Logic.strip_assums_concl
488 fun pair_untyped_aconv (t1, t2) (u1, u2) =
489 Term.aconv_untyped (t1, u1) andalso Term.aconv_untyped (t2, u2)
490 fun add_terms tp inst =
491 if exists (pair_untyped_aconv tp) inst then inst
492 else tp :: map (apsnd (subst_atomic [tp])) inst
495 (Var _, args) => forall is_Bound args
497 fun unify_flex flex rigid =
498 case strip_comb flex of
499 (Var (z as (_, T)), args) =>
501 fold_rev absdummy (take (length args) (binder_types T)) rigid)
503 fun unify_potential_flex comb atom =
504 if is_flex comb then unify_flex comb atom
505 else if is_Var atom then add_terms (atom, comb)
507 fun unify_terms (t, u) =
509 (t1 $ t2, u1 $ u2) =>
510 if is_flex t then unify_flex t u
511 else if is_flex u then unify_flex u t
512 else fold unify_terms [(t1, u1), (t2, u2)]
513 | (_ $ _, _) => unify_potential_flex t u
514 | (_, _ $ _) => unify_potential_flex u t
515 | (Var _, _) => add_terms (t, u)
516 | (_, Var _) => add_terms (u, t)
519 [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy)))
520 |> the_default [] (* FIXME *)
521 in th |> cterm_instantiate t_inst end
523 val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
525 fun copy_prems_tac [] ns i =
526 if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
527 | copy_prems_tac (1 :: ms) ns i =
528 rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
529 | copy_prems_tac (m :: ms) ns i =
530 etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
532 (* Metis generates variables of the form _nnn. *)
533 val is_metis_fresh_variable = String.isPrefix "_"
535 fun instantiate_forall_tac thy t i st =
537 val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
538 fun repair (t as (Var ((s, _), _))) =
539 (case find_index (fn (s', _) => s' = s) params of
543 (case (repair t, repair u) of
544 (t as Bound j, u as Bound k) =>
545 (* This is a rather subtle trick to repair the discrepancy between
546 the fully skolemized term that MESON gives us (where existentials
547 were pulled out) and the reality. *)
548 if k > j then t else t $ u
551 val t' = t |> repair |> fold (absdummy o snd) params
552 fun do_instantiate th =
553 case Term.add_vars (prop_of th) []
554 |> filter_out ((Meson_Clausify.is_zapped_var_name orf
555 is_metis_fresh_variable) o fst o fst) of
559 val var_binder_Ts = T |> binder_types |> take (length params) |> rev
560 val var_body_T = T |> funpow (length params) range_type
562 Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
563 var_body_T :: var_binder_Ts)
565 Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
566 tenv = Vartab.empty, tyenv = tyenv}
568 Vartab.fold (fn (x, (S, T)) =>
569 cons (pairself (ctyp_of thy) (TVar (x, S), T)))
572 [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
573 in th |> Drule.instantiate_normalize (ty_inst, t_inst) end
574 | _ => raise Fail "expected a single non-zapped, non-Metis Var"
576 (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
577 THEN PRIMITIVE do_instantiate) st
580 fun fix_exists_tac t =
581 etac @{thm exE} THEN' rename_tac [t |> dest_Var |> fst |> fst]
583 fun release_quantifier_tac thy (skolem, t) =
584 (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
586 fun release_clusters_tac _ _ _ [] = K all_tac
587 | release_clusters_tac thy ax_counts substs
588 ((ax_no, cluster_no) :: clusters) =
591 Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
592 fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
595 |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
596 if ax_no' = ax_no then
597 tsubst |> map (apfst cluster_of_var)
598 |> filter (in_right_cluster o fst)
603 fun do_cluster_subst cluster_subst =
604 map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
605 val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
607 rotate_tac first_prem
608 THEN' (EVERY' (maps do_cluster_subst cluster_substs))
609 THEN' rotate_tac (~ first_prem - length cluster_substs)
610 THEN' release_clusters_tac thy ax_counts substs clusters
613 fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
614 (ax_no, (cluster_no, (skolem, index_no)))
616 prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord))
617 (pairself cluster_key p)
620 list_ord (prod_ord Term_Ord.fast_indexname_ord
621 (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
623 structure Int_Tysubst_Table =
624 Table(type key = int * (indexname * (sort * typ)) list
625 val ord = prod_ord int_ord tysubst_ord)
627 structure Int_Pair_Graph =
628 Graph(type key = int * int val ord = prod_ord int_ord int_ord)
630 fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
631 fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
633 (* Attempts to derive the theorem "False" from a theorem of the form
634 "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
635 specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
636 must be eliminated first. *)
637 fun discharge_skolem_premises ctxt axioms prems_imp_false =
638 if prop_of prems_imp_false aconv @{prop False} then
642 val thy = Proof_Context.theory_of ctxt
646 Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
649 |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
651 o pairself (Meson_Clausify.cluster_of_zapped_var_name
653 |> map (Meson.term_pair_of
654 #> pairself (Envir.subst_term_types tyenv))
655 val tysubst = tyenv |> Vartab.dest
656 in (tysubst, tsubst) end
657 fun subst_info_for_prem subgoal_no prem =
659 _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
660 let val ax_no = HOLogic.dest_nat num in
662 match_term (nth axioms ax_no |> the |> snd, t)))
664 | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
666 fun cluster_of_var_name skolem s =
667 case try Meson_Clausify.cluster_of_zapped_var_name s of
669 | SOME ((ax_no, (cluster_no, _)), skolem') =>
670 if skolem' = skolem andalso cluster_no > 0 then
671 SOME (ax_no, cluster_no)
674 fun clusters_in_term skolem t =
675 Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
676 fun deps_for_term_subst (var, t) =
677 case clusters_in_term false var of
679 | [(ax_no, cluster_no)] =>
680 SOME ((ax_no, cluster_no),
681 clusters_in_term true t
682 |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
683 | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
684 val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
685 val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
686 |> sort (int_ord o pairself fst)
687 val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
688 val clusters = maps (op ::) depss
689 val ordered_clusters =
691 |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
692 |> fold Int_Pair_Graph.add_deps_acyclic depss
693 |> Int_Pair_Graph.topological_order
694 handle Int_Pair_Graph.CYCLES _ =>
695 error "Cannot replay Metis proof in Isabelle without \
696 \\"Hilbert_Choice\"."
698 Int_Tysubst_Table.empty
699 |> fold (fn (ax_no, (_, (tysubst, _))) =>
700 Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
701 (Integer.add 1)) substs
702 |> Int_Tysubst_Table.dest
703 val needed_axiom_props =
704 0 upto length axioms - 1 ~~ axioms
705 |> map_filter (fn (_, NONE) => NONE
706 | (ax_no, SOME (_, t)) =>
707 if exists (fn ((ax_no', _), n) =>
708 ax_no' = ax_no andalso n > 0)
713 val outer_param_names =
714 [] |> fold Term.add_var_names needed_axiom_props
715 |> filter (Meson_Clausify.is_zapped_var_name o fst)
716 |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
717 |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
718 cluster_no = 0 andalso skolem)
719 |> sort shuffle_ord |> map (fst o snd)
720 (* for debugging only:
721 fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
722 "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
723 "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
724 commas (map ((fn (s, t) => s ^ " |-> " ^ t)
725 o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
726 val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
727 val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
728 val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
729 val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
730 cat_lines (map string_for_subst_info substs))
732 fun cut_and_ex_tac axiom =
733 cut_rules_tac [axiom] 1
734 THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
735 fun rotation_for_subgoal i =
736 find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
738 Goal.prove ctxt [] [] @{prop False}
739 (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
741 THEN rename_tac outer_param_names 1
742 THEN copy_prems_tac (map snd ax_counts) [] 1)
743 THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
744 THEN match_tac [prems_imp_false] 1
745 THEN ALLGOALS (fn i =>
746 rtac @{thm Meson.skolem_COMBK_I} i
747 THEN rotate_tac (rotation_for_subgoal i) i
748 THEN PRIMITIVE (unify_first_prem_with_concl thy i)
752 error ("Cannot replay Metis proof in Isabelle:\n\
753 \Error when discharging Skolem assumptions.")