# HG changeset patch
# User blanchet
# Date 1336919461 -7200
# Node ID b12e1fa43ad19fc3fc6da0ef8437671ee8fb4e05
# Parent  12de57c5eee551138bc96f9c64108b9bc7b40c17
eta-reduce definition-like equations for THF provers; Satallax in particular seems to love that

diff -r 12de57c5eee5 -r b12e1fa43ad1 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun May 13 16:31:01 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun May 13 16:31:01 2012 +0200
@@ -1240,6 +1240,19 @@
       | freeze t = t
   in t |> exists_subterm is_Var t ? freeze end
 
+fun eta_reduce_def t =
+  case t of
+    Const (@{const_name HOL.eq}, _) $ lhs $ rhs =>
+    (case strip_comb lhs of
+       (c as Const (_, T), args) =>
+       if forall is_Var args andalso not (has_duplicates (op =) args) then
+         Const (@{const_name HOL.eq}, T --> T --> @{typ bool})
+         $ c $ fold_rev lambda args rhs
+       else
+         t
+     | _ => t)
+  | _ => t
+
 fun presimp_prop ctxt type_enc t =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -1247,9 +1260,11 @@
               |> transform_elim_prop
               |> Object_Logic.atomize_term thy
     val need_trueprop = (fastype_of t = @{typ bool})
+    val is_ho = is_type_enc_higher_order type_enc
   in
-    t |> need_trueprop ? HOLogic.mk_Trueprop
-      |> not (is_type_enc_higher_order type_enc) ? extensionalize_term ctxt
+    t |> is_ho ? eta_reduce_def
+      |> need_trueprop ? HOLogic.mk_Trueprop
+      |> not is_ho ? extensionalize_term ctxt
       |> presimplify_term thy
       |> HOLogic.dest_Trueprop
   end