# HG changeset patch
# User blanchet
# Date 1280431224 -7200
# Node ID db90d313cf53d2d24f1d47eb27702cb2ba8d271b
# Parent  5e4ad2df09f339a74f9c59b0037141ef69000cc2
handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs

diff -r 5e4ad2df09f3 -r db90d313cf53 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 20:15:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 21:20:24 2010 +0200
@@ -236,8 +236,8 @@
   #> Meson.presimplify
   #> prop_of
 
-(* FIXME: Guarantee freshness *)
-fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
+(* Freshness almost guaranteed! *)
+fun concealed_bound_name j = das_Tool ^ Int.toString j
 fun conceal_bounds Ts t =
   subst_bounds (map (Free o apfst concealed_bound_name)
                     (length Ts - 1 downto 0 ~~ rev Ts), t)
@@ -282,6 +282,17 @@
            Axiom => HOLogic.true_const
          | Conjecture => HOLogic.false_const
 
+(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
+   same in Sledgehammer to prevent the discovery of unreplable proofs. *)
+fun freeze_term t =
+  let
+    fun aux (t $ u) = aux t $ aux u
+      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
+      | aux (Var ((s, i), T)) =
+        Free (das_Tool ^ "_" ^ s ^ "_" ^ string_of_int i, T)
+      | aux t = t
+  in t |> exists_subterm is_Var t ? aux end
+
 (* making axiom and conjecture formulas *)
 fun make_formula ctxt presimp (formula_name, kind, t) =
   let
@@ -293,6 +304,7 @@
               |> presimp ? presimplify_term thy
               |> perhaps (try (HOLogic.dest_Trueprop))
               |> introduce_combinators_in_term ctxt kind
+              |> kind = Conjecture ? freeze_term
     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   in
     FOLFormula {formula_name = formula_name, combformula = combformula,