# HG changeset patch
# User blanchet
# Date 1272462797 -7200
# Node ID 60532b9bcd1c22e3268afb458566f92766859bdb
# Parent  6769f8eacaaceea592c85e66b14aaaffe34ae486
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code

diff -r 6769f8eacaac -r 60532b9bcd1c src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Wed Apr 28 15:34:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Wed Apr 28 15:53:17 2010 +0200
@@ -10,6 +10,7 @@
   val trace: bool Unsynchronized.ref
   val trace_msg: (unit -> string) -> unit
   val skolem_prefix: string
+  val skolem_infix: string
   val cnf_axiom: theory -> thm -> thm list
   val multi_base_blacklist: string list
   val bad_for_atp: thm -> bool
@@ -34,6 +35,7 @@
 fun trace_msg msg = if !trace then tracing (msg ()) else ();
 
 val skolem_prefix = "sko_"
+val skolem_infix = "$"
 
 fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
 
@@ -65,6 +67,13 @@
 
 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
 
+(*Keep the full complexity of the original name*)
+fun flatten_name s = space_implode "_X" (Long_Name.explode s);
+
+fun skolem_name thm_name nref var_name =
+  skolem_prefix ^ thm_name ^ "_" ^ Int.toString (Unsynchronized.inc nref) ^
+  skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name)
+
 fun rhs_extra_types lhsT rhs =
   let val lhs_vars = Term.add_tfreesT lhsT []
       fun add_new_TFrees (TFree v) =
@@ -78,10 +87,10 @@
 fun declare_skofuns s th =
   let
     val nref = Unsynchronized.ref 0    (* FIXME ??? *)
-    fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (_, T, p))) (axs, thy) =
+    fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) (axs, thy) =
           (*Existential: declare a Skolem function, then insert into body and continue*)
           let
-            val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
+            val cname = skolem_name s nref s'
             val args0 = OldTerm.term_frees xtp  (*get the formal parameter list*)
             val Ts = map type_of args0
             val extraTs = rhs_extra_types (Ts ---> T) xtp
@@ -110,13 +119,13 @@
 (*Traverse a theorem, accumulating Skolem function definitions.*)
 fun assume_skofuns s th =
   let val sko_count = Unsynchronized.ref 0   (* FIXME ??? *)
-      fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs(_,T,p))) defs =
+      fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) defs =
             (*Existential: declare a Skolem function, then insert into body and continue*)
             let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
                 val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
                 val Ts = map type_of args
                 val cT = Ts ---> T
-                val id = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
+                val id = skolem_name s sko_count s'
                 val c = Free (id, cT)
                 val rhs = list_abs_free (map dest_Free args,
                                          HOLogic.choice_const T $ xtp)
@@ -337,9 +346,6 @@
   ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
    "split_asm", "cases", "ext_cases"];
 
-(*Keep the full complexity of the original name*)
-fun flatten_name s = space_implode "_X" (Long_Name.explode s);
-
 fun fake_name th =
   if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
   else gensym "unknown_thm_";
diff -r 6769f8eacaac -r 60532b9bcd1c src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 28 15:34:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 28 15:53:17 2010 +0200
@@ -50,14 +50,10 @@
       SOME s' => s'
     | NONE => s
 
-(* Hack: Could return false positives (e.g., a user happens to declare a
-   constant called "SomeTheory.sko_means_shoe_in_swedish". *)
-val is_skolem_const_name = String.isPrefix skolem_prefix o Long_Name.base_name
-
 fun smart_lambda v t =
     Abs (case v of
-           Const (s, _) => if is_skolem_const_name s then "g"
-                           else Long_Name.base_name s
+           Const (s, _) =>
+           List.last (space_explode skolem_infix (Long_Name.base_name s))
          | Var ((s, _), _) => s
          | Free (s, _) => s
          | _ => "", fastype_of v, abstract_over (v, t))
@@ -772,6 +768,13 @@
     and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   in do_proof end
 
+
+(* Hack: Could return false positives (e.g., a user happens to declare a
+   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
+val is_skolem_const_name =
+  Long_Name.base_name
+  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
+
 fun unskolemize_term t =
   fold exists_of (Term.add_consts t []
                   |> filter (is_skolem_const_name o fst) |> map Const) t