--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Mar 24 17:49:27 2011 +0100
@@ -9,6 +9,7 @@
sig
val new_skolem_var_prefix : string
val new_nonskolem_var_prefix : string
+ val is_zapped_var_name : string -> bool
val extensionalize_theorem : thm -> thm
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
@@ -27,6 +28,10 @@
val new_skolem_var_prefix = "MesonSK"
val new_nonskolem_var_prefix = "MesonV"
+fun is_zapped_var_name s =
+ exists (fn prefix => String.isPrefix prefix s)
+ [new_skolem_var_prefix, new_nonskolem_var_prefix]
+
(**** Transformation of Elimination Rules into First-Order Formulas****)
val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
@@ -328,13 +333,20 @@
val no_choice = null choice_ths
val discharger_th =
th |> (if no_choice then pull_out else skolemize choice_ths)
- val fully_skolemized_t =
+ val zapped_th =
discharger_th |> prop_of |> rename_bound_vars_to_be_zapped ax_no
|> (if no_choice then
Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> cprop_of
else
cterm_of thy)
- |> zap true |> Drule.export_without_context
+ |> zap true
+ val fixes =
+ Term.add_free_names (prop_of zapped_th) []
+ |> filter is_zapped_var_name
+ val ctxt' = ctxt |> Variable.add_fixes_direct fixes (*###*)
+ val fully_skolemized_t =
+ zapped_th
+ |> singleton (Variable.export ctxt' ctxt)
|> cprop_of |> Thm.dest_equals |> snd |> term_of
in
if exists_subterm (fn Var ((s, _), _) =>
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Mar 24 17:49:27 2011 +0100
@@ -38,10 +38,6 @@
fun verbose_warning ctxt msg =
if Config.get ctxt verbose then warning msg else ()
-val is_zapped_var_name =
- String.isPrefix Meson_Clausify.new_skolem_var_prefix orf
- String.isPrefix Meson_Clausify.new_nonskolem_var_prefix
-
datatype term_or_type = SomeTerm of term | SomeType of typ
fun terms_of [] = []
@@ -619,7 +615,7 @@
fun unify_potential_flex comb atom =
if is_flex comb then unify_flex comb atom
else if is_Var atom then add_terms (atom, comb)
- else raise TERM ("unify_terms", [comb, atom])
+ else raise TERM ("unify_potential_flex", [comb, atom])
fun unify_terms (t, u) =
case (t, u) of
(t1 $ t2, u1 $ u2) =>
@@ -662,7 +658,7 @@
fun do_instantiate th =
let
val var = Term.add_vars (prop_of th) []
- |> filter (is_zapped_var_name o fst o fst)
+ |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
|> the_single
in th |> term_instantiate thy [(Var var, t')] end
in
@@ -751,7 +747,7 @@
Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
val tsubst =
tenv |> Vartab.dest
- |> filter (is_zapped_var_name o fst o fst)
+ |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
|> sort (cluster_ord
o pairself (Meson_Clausify.cluster_of_zapped_var_name
o fst o fst))
@@ -801,7 +797,7 @@
\\"Hilbert_Choice\"."
val outer_param_names =
[] |> fold (Term.add_var_names o snd) (map_filter I axioms)
- |> filter (is_zapped_var_name o fst)
+ |> filter (Meson_Clausify.is_zapped_var_name o fst)
|> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
|> filter (fn (((_, (cluster_no, _)), skolem), _) =>
cluster_no = 0 andalso skolem)
@@ -837,7 +833,7 @@
THEN ALLGOALS (fn i =>
rtac @{thm Meson.skolem_COMBK_I} i
THEN rotate_tac (rotation_for_subgoal i) i
-(* THEN PRIMITIVE (unify_first_prem_with_concl thy i) ### FIXME: needed? *)
+(* THEN PRIMITIVE (unify_first_prem_with_concl thy i) FIXME: needed? *)
THEN assume_tac i)))
handle ERROR _ =>
error ("Cannot replay Metis proof in Isabelle:\n\