# HG changeset patch
# User blanchet
# Date 1391110789 -3600
# Node ID b75b52c7cf9443acd4ef7a8049a4aac4e749375e
# Parent  f127ab7368cfe8ba8c18b7c3fb45d8e4ed7b9d4a
unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer

diff -r f127ab7368cf -r b75b52c7cf94 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Jan 30 18:37:08 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Jan 30 20:39:49 2014 +0100
@@ -44,6 +44,7 @@
   val agsyhol_core_rule : string
   val satallax_core_rule : string
   val spass_input_rule : string
+  val spass_pre_skolemize_rule : string
   val spass_skolemize_rule : string
   val z3_tptp_core_rule : string
 
@@ -73,6 +74,7 @@
 val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
 val satallax_core_rule = "__satallax_core" (* arbitrary *)
 val spass_input_rule = "Inp"
+val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *)
 val spass_skolemize_rule = "__Sko" (* arbitrary *)
 val z3_tptp_core_rule = "__z3_tptp_core" (* arbitrary *)
 
diff -r f127ab7368cf -r b75b52c7cf94 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jan 30 18:37:08 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jan 30 20:39:49 2014 +0100
@@ -535,6 +535,55 @@
   #> map (termify_line ctxt lifted sym_tab)
   #> repair_waldmeister_endgame
 
+fun take_distinct_vars seen ((t as Var _) :: ts) =
+    if member (op aconv) seen t then rev seen else take_distinct_vars (t :: seen) ts
+  | take_distinct_vars seen _ = rev seen
+
+fun unskolemize_term skos t =
+  let
+    val is_sko = member (op =) skos
+
+    fun find_args args (t $ u) = find_args (u :: args) t #> find_args [] u
+      | find_args _ (Abs (_, _, t)) = find_args [] t
+      | find_args args (Free (s, _)) =
+        if is_sko s then
+          let val new = take_distinct_vars [] args in
+            (fn [] => new | old => if length new < length old then new else old)
+          end
+        else
+          I
+      | find_args _ _ = I
+
+    val alls = find_args [] t []
+    val num_alls = length alls
+  in
+    if num_alls = 0 then
+      t
+    else
+      let
+        fun fix_skos args (t $ u) = fix_skos (fix_skos [] u :: args) t
+          | fix_skos args (t as Free (s, T)) =
+            if is_sko s then list_comb (Free (s, funpow num_alls body_type T), drop num_alls args)
+            else list_comb (t, args)
+          | fix_skos [] (Abs (s, T, t)) = Abs (s, T, fix_skos [] t)
+          | fix_skos [] t = t
+          | fix_skos args t = list_comb (fix_skos [] t, args)
+
+        val t' = fix_skos [] t
+
+        fun add_sko (t as Free (s, _)) = is_sko s ? insert (op aconv) t
+          | add_sko _ = I
+
+        val exs = Term.fold_aterms add_sko t' []
+      in
+        t'
+        |> HOLogic.dest_Trueprop
+        |> fold exists_of exs |> Term.map_abs_vars (K Name.uu)
+        |> fold_rev forall_of alls
+        |> HOLogic.mk_Trueprop
+      end
+  end
+
 fun introduce_spass_skolem [] = []
   | introduce_spass_skolem (proof as (_, _, _, rule1, _) :: _) =
     if rule1 = spass_input_rule then
@@ -558,20 +607,25 @@
         fun in_group group = member (op =) group o hd
         fun group_of sko = the (find_first (fn group => in_group group sko) groups)
 
-        fun new_step group (skoss_steps : ('a * (term, 'b) atp_step) list) =
+        fun new_steps (skoss_steps : (string list * (term, 'a) atp_step) list) group =
           let
+            val name = step_name_of_group group
+            val name0 = name |>> prefix "0"
             val t =
               skoss_steps
               |> map (snd #> #3 #> HOLogic.dest_Trueprop)
               |> Library.foldr1 s_conj
               |> HOLogic.mk_Trueprop
+            val skos = fold (union (op =) o fst) skoss_steps []
             val deps = map (snd #> #1) skoss_steps
           in
-            (step_name_of_group group, Plain, t, spass_skolemize_rule, deps)
+            [(name0, Lemma, unskolemize_term skos t, spass_pre_skolemize_rule, deps),
+             (name, Plain, t, spass_skolemize_rule, [name0])]
           end
 
         val sko_steps =
-          map (fn group => new_step group (filter (in_group group o fst) skoss_input_steps)) groups
+          maps (fn group => new_steps (filter (in_group group o fst) skoss_input_steps) group)
+            groups
 
         val old_news =
           map (fn (skos, (name, _, _, _, _)) => (name, [step_name_of_group (group_of skos)]))