--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 29 12:49:05 2010 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 29 12:49:05 2010 +0200
@@ -233,7 +233,7 @@
fun zapped_var_name ((ax_no, cluster_no), skolem) index_no s =
(if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
"_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^
- string_of_int index_no ^ "_" ^ s
+ string_of_int index_no ^ "_" ^ Name.desymbolize false s
fun cluster_of_zapped_var_name s =
let val get_int = the o Int.fromString o nth (space_explode "_" s) in
@@ -299,7 +299,7 @@
fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths
-val no_choice =
+val cheat_choice =
@{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"}
|> Logic.varify_global
|> Skip_Proof.make_thm @{theory}
@@ -324,11 +324,16 @@
#> simplify (ss_only @{thms all_simps[symmetric]})
val pull_out =
simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
+ val no_choice = null choice_ths
val discharger_th =
- th |> (if null choice_ths then pull_out else skolemize choice_ths)
+ th |> (if no_choice then pull_out else skolemize choice_ths)
val fully_skolemized_t =
- th |> prop_of |> rename_bound_vars_to_be_zapped ax_no
- |> Skip_Proof.make_thm thy |> skolemize [no_choice] |> cprop_of
+ th |> prop_of
+ |> no_choice ? rename_bound_vars_to_be_zapped ax_no
+ |> Skip_Proof.make_thm thy |> skolemize [cheat_choice] |> cprop_of
+ |> not no_choice
+ ? (term_of #> rename_bound_vars_to_be_zapped ax_no
+ #> cterm_of thy)
|> zap true |> Drule.export_without_context
|> cprop_of |> Thm.dest_equals |> snd |> term_of
in
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Oct 29 12:49:05 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Oct 29 12:49:05 2010 +0200
@@ -628,7 +628,14 @@
(case find_index (fn (s', _) => s' = s) params of
~1 => t
| j => Bound j)
- | repair (t $ u) = repair t $ repair u
+ | repair (t $ u) =
+ (case (repair t, repair u) of
+ (t as Bound j, u as Bound k) =>
+ (* This is a rather subtle trick to repair the discrepancy between
+ the fully skolemized term that MESON gives us (where existentials
+ were pulled out) and the reality. *)
+ if k > j then t else t $ u
+ | (t, u) => t $ u)
| repair t = t
val t' = t |> repair |> fold (curry absdummy) (map snd params)
fun do_instantiate th =
@@ -641,24 +648,32 @@
THEN PRIMITIVE do_instantiate) st
end
+fun fix_exists_tac thy t =
+ etac @{thm exE}
+ THEN' rename_tac [t |> dest_Var |> fst |> fst]
+
+fun release_quantifier_tac thy (skolem, t) =
+ (if skolem then fix_exists_tac else instantiate_forall_tac) thy t
+
fun release_clusters_tac _ _ _ [] = K all_tac
| release_clusters_tac thy ax_counts substs
((ax_no, cluster_no) :: clusters) =
let
- fun in_right_cluster s =
- (s |> Meson_Clausify.cluster_of_zapped_var_name |> fst |> snd |> fst)
- = cluster_no
+ val cluster_of_var =
+ Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
+ fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
val cluster_substs =
substs
|> map_filter (fn (ax_no', (_, (_, tsubst))) =>
if ax_no' = ax_no then
- tsubst |> filter (in_right_cluster
- o fst o fst o dest_Var o fst)
- |> map snd |> SOME
- else
- NONE)
+ tsubst |> map (apfst cluster_of_var)
+ |> filter (in_right_cluster o fst)
+ |> map (apfst snd)
+ |> SOME
+ else
+ NONE)
fun do_cluster_subst cluster_subst =
- map (instantiate_forall_tac thy) cluster_subst @ [rotate_tac 1]
+ map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
in
rotate_tac first_prem
@@ -695,6 +710,7 @@
let
val thy = ProofContext.theory_of ctxt
(* distinguish variables with same name but different types *)
+ (* ### FIXME: needed? *)
val prems_imp_false' =
prems_imp_false |> try (forall_intr_vars #> gen_all)
|> the_default prems_imp_false
@@ -779,7 +795,6 @@
val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
cat_lines (map string_for_subst_info substs))
val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
- val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
*)
fun rotation_for_subgoal i =