# HG changeset patch
# User blanchet
# Date 1302171387 -7200
# Node ID 7d08265f181dfb0c12dd1bb1d2cf443c5001782e
# Parent  5f2960582e45fef2649daba4d4f8b8433c62d2f8
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind

diff -r 5f2960582e45 -r 7d08265f181d src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 07 12:16:26 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 07 12:16:27 2011 +0200
@@ -128,7 +128,7 @@
                     val nterms = length ts - ntypes
                     val tts = map tm_to_tt ts
                     val tys = types_of (List.take(tts,ntypes))
-                    val j = !new_skolem_var_count + 1
+                    val j = !new_skolem_var_count + 0 (* FIXME ### *)
                     val _ = new_skolem_var_count := j
                     val t =
                       if String.isPrefix new_skolem_const_prefix c then
@@ -594,6 +594,9 @@
   | copy_prems_tac (m :: ms) ns i =
     etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
 
+(* Metis generates variables of the form _nnn. *)
+val is_metis_fresh_variable = String.isPrefix "_"
+
 fun instantiate_forall_tac thy t i st =
   let
     val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
@@ -613,13 +616,31 @@
     val t' = t |> repair |> fold (curry absdummy) (map snd params)
     fun do_instantiate th =
       case Term.add_vars (prop_of th) []
-           |> filter_out (Meson_Clausify.is_zapped_var_name o fst o fst) of
+           |> filter_out ((Meson_Clausify.is_zapped_var_name orf
+                           is_metis_fresh_variable) o fst o fst) of
         [] => th
-      | [var] => th |> term_instantiate thy [(Var var, t')]
-      | _ => raise Fail "expected a single non-zapped Var"
+      | [var as (_, T)] =>
+        let
+          val var_binder_Ts = T |> binder_types |> take (length params) |> rev
+          val var_body_T = T |> funpow (length params) range_type
+          val tyenv =
+            Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
+                                             var_body_T :: var_binder_Ts)
+          val env =
+            Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
+                         tenv = Vartab.empty, tyenv = tyenv}
+          val ty_inst =
+            Vartab.fold (fn (x, (S, T)) =>
+                            cons (pairself (ctyp_of thy) (TVar (x, S), T)))
+                        tyenv []
+          val t_inst =
+            [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
+        in
+          th |> instantiate (ty_inst, t_inst)
+        end
+      | _ => raise Fail "expected a single non-zapped, non-Metis Var"
   in
-    (etac @{thm allE} i
-     THEN rotate_tac ~1 i
+    (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
      THEN PRIMITIVE do_instantiate) st
   end
 
@@ -674,7 +695,7 @@
 structure Int_Pair_Graph =
   Graph(type key = int * int val ord = prod_ord int_ord int_ord)
 
-fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no)
+fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
 fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
 
 (* Attempts to derive the theorem "False" from a theorem of the form
@@ -760,26 +781,29 @@
         "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
         commas (map ((fn (s, t) => s ^ " |-> " ^ t)
                      o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
+      val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
       val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
       val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
       val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
                        cat_lines (map string_for_subst_info substs))
 *)
+      fun cut_and_ex_tac axiom =
+        cut_rules_tac [axiom] 1
+        THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
       fun rotation_for_subgoal i =
         find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
     in
       Goal.prove ctxt [] [] @{prop False}
-          (K (cut_rules_tac
-                  (map (fst o the o nth axioms o fst o fst) ax_counts) 1
-              THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
-              THEN rename_tac outer_param_names 1
-              THEN copy_prems_tac (map snd ax_counts) [] 1
+          (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
+                                  o fst) ax_counts)
+                      THEN rename_tac outer_param_names 1
+                      THEN copy_prems_tac (map snd ax_counts) [] 1)
               THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
               THEN match_tac [prems_imp_false] 1
               THEN ALLGOALS (fn i =>
                        rtac @{thm Meson.skolem_COMBK_I} i
                        THEN rotate_tac (rotation_for_subgoal i) i
-                       THEN assume_tac 1
+                       THEN assume_tac i
                        THEN flexflex_tac)))
       handle ERROR _ =>
              error ("Cannot replay Metis proof in Isabelle:\n\