author blanchet Mon, 06 Oct 2014 19:19:16 +0200 changeset 58597 21a741e96970 parent 58596 877c5ecee253 child 58598 d9892c88cb56
improved unskolemization of SPASS problems
```--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Oct 06 18:17:44 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Oct 06 19:19:16 2014 +0200
@@ -626,36 +626,31 @@

fun unskolemize_term skos =
let
-    val is_skolem = member (op =) skos
+    val is_skolem_name = member (op =) skos

fun find_argless_skolem (Free _ \$ Var _) = NONE
-      | find_argless_skolem (Free (x as (s, _))) = if is_skolem s then SOME x else NONE
+      | find_argless_skolem (Free (x as (s, _))) = if is_skolem_name s then SOME x else NONE
| find_argless_skolem (t \$ u) =
(case find_argless_skolem t of NONE => find_argless_skolem u | sk => sk)
| find_argless_skolem (Abs (_, _, t)) = find_argless_skolem t
| find_argless_skolem _ = NONE

-    fun find_skolem_arg (Free (s, _) \$ Var v) = if is_skolem s then SOME v else NONE
+    fun find_skolem_arg (Free (s, _) \$ Var v) = if is_skolem_name s then SOME v else NONE
| find_skolem_arg (t \$ u) = (case find_skolem_arg t of NONE => find_skolem_arg u | v => v)
| find_skolem_arg (Abs (_, _, t)) = find_skolem_arg t
| find_skolem_arg _ = NONE

+    fun kill_skolem_arg (t as Free (s, T) \$ Var _) =
+        if is_skolem_name s then Free (s, range_type T) else t
+      | kill_skolem_arg (t \$ u) = kill_skolem_arg t \$ kill_skolem_arg u
+      | kill_skolem_arg (Abs (s, T, t)) = Abs (s, T, kill_skolem_arg t)
+      | kill_skolem_arg t = t
+
fun find_var (Var v) = SOME v
| find_var (t \$ u) = (case find_var t of NONE => find_var u | v => v)
| find_var (Abs (_, _, t)) = find_var t
| find_var _ = NONE

-    fun find_next_var t =
-      (case find_skolem_arg t of
-        NONE => find_var t
-      | v => v)
-
-    fun kill_skolem_arg (t as Free (s, T) \$ Var _) =
-        if is_skolem s then Free (s, range_type T) else t
-      | kill_skolem_arg (t \$ u) = kill_skolem_arg t \$ kill_skolem_arg u
-      | kill_skolem_arg (Abs (s, T, t)) = Abs (s, T, kill_skolem_arg t)
-      | kill_skolem_arg t = t
-
val safe_abstract_over = abstract_over o apsnd (incr_boundvars 1)

fun unskolem t =
@@ -663,19 +658,23 @@
SOME (x as (s, T)) =>
HOLogic.exists_const T \$ Abs (s, T, unskolem (safe_abstract_over (Free x, t)))
| NONE =>
-        (case find_next_var t of
+        (case find_skolem_arg t of
SOME (v as ((s, _), T)) =>
let
val (haves, have_nots) =
HOLogic.disjuncts t
-              |> List.partition (Term.exists_subterm (curry (op =) (Var v)))
+              |> List.partition (exists_subterm (curry (op =) (Var v)))
|> pairself (fn lits => fold (curry s_disj) lits @{term False})
in
s_disj (HOLogic.all_const T
\$ Abs (s, T, unskolem (safe_abstract_over (Var v, kill_skolem_arg haves))),
unskolem have_nots)
end
-        | NONE => t))
+        | NONE =>
+          (case find_var t of
+            SOME (v as ((s, _), T)) =>
+            HOLogic.all_const T \$ Abs (s, T, unskolem (safe_abstract_over (Var v, t)))
+          | NONE => t)))
in
HOLogic.mk_Trueprop o unskolem o HOLogic.dest_Trueprop
end
@@ -714,38 +713,41 @@

val (input_steps, other_steps) = List.partition (null o #5) proof

-    val skoss = map (fn (_, _, t, _, _) => Term.fold_aterms add_skolem t []) input_steps
-    val skoss_input_steps = filter_out (null o fst) (skoss ~~ input_steps)
-    val groups = Graph.strong_conn (fold add_cycle skoss Graph.empty)
+    (* The names of the formulas are added to the Skolem constants, to ensure that formulas giving
+       rise to several clauses are skolemized together. *)
+    val skoXss = map (fn ((_, ss), _, t, _, _) => Term.fold_aterms add_skolem t ss) input_steps
+    val skoXss_input_steps = filter_out (null o fst) (skoXss ~~ input_steps)
+    val groups = Graph.strong_conn (fold add_cycle skoXss Graph.empty)

-    fun step_name_of_group skos = (implode skos, [])
+    fun step_name_of_group skoXs = (implode skoXs, [])
fun in_group group = member (op =) group o hd
-    fun group_of sko = the (find_first (fn group => in_group group sko) groups)
+    fun group_of skoX = the (find_first (fn group => in_group group skoX) groups)

-    fun new_steps (skoss_steps : (string list * (term, 'a) atp_step) list) group =
+    fun new_steps (skoXss_steps : (string list * (term, 'a) atp_step) list) group =
let
val name = step_name_of_group group
val name0 = name |>> prefix "0"
val t =
-          (case map (snd #> #3) skoss_steps of
+          (case map (snd #> #3) skoXss_steps of
[t] => t
| ts => ts
|> map (HOLogic.dest_Trueprop #> rename_skolem_args)
|> Library.foldr1 s_conj
|> HOLogic.mk_Trueprop)
-        val skos = fold (union (op =) o fst) skoss_steps []
-        val deps = map (snd #> #1) skoss_steps
+        val skos =
+          fold (union (op =) o filter (String.isPrefix spass_skolem_prefix) o fst) skoXss_steps []
+        val deps = map (snd #> #1) skoXss_steps
in
[(name0, Unknown, unskolemize_term skos t, spass_pre_skolemize_rule, deps),
(name, Unknown, t, spass_skolemize_rule, [name0])]
end

val sko_steps =
-      maps (fn group => new_steps (filter (in_group group o fst) skoss_input_steps) group) groups
+      maps (fn group => new_steps (filter (in_group group o fst) skoXss_input_steps) group) groups

val old_news =
map (fn (skos, (name, _, _, _, _)) => (name, [step_name_of_group (group_of skos)]))
-        skoss_input_steps
+        skoXss_input_steps
val repair_deps = fold replace_dependencies_in_line old_news
in
input_steps @ sko_steps @ map repair_deps other_steps```