# HG changeset patch
# User blanchet
# Date 1288349345 -7200
# Node ID 7a02144874f3434760908a74b66d886863169d06
# Parent  73ecbe2d432bda26056787ca9b9f43fccbd5dd1f
more work on new Skolemizer without Hilbert_Choice

diff -r 73ecbe2d432b -r 7a02144874f3 src/HOL/Tools/Meson/meson_clausify.ML
--- 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
diff -r 73ecbe2d432b -r 7a02144874f3 src/HOL/Tools/Metis/metis_reconstruct.ML
--- 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 =