# HG changeset patch
# User blanchet
# Date 1277393238 -7200
# Node ID 48273d1ea331fb694cc9d46482127e03aa3f3991
# Parent  c80e77e8d0369b66639aca19f6daae7ede7769ae
better eta-expansion in Sledgehammer's clausification;
make the eta-expansion code more robust in the face of polymorphic arguments + make eta-expansion happen more often, since it first-orderizes things

diff -r c80e77e8d036 -r 48273d1ea331 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Jun 24 17:25:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Jun 24 17:27:18 2010 +0200
@@ -183,25 +183,14 @@
 fun vars_of_thm th =
   map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
 
-(*Make a version of fun_cong with a given variable name*)
-local
-    val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*)
-    val cx = hd (vars_of_thm fun_cong');
-    val ty = typ_of (ctyp_of_term cx);
-    val thy = theory_of_thm fun_cong;
-    fun mkvar a = cterm_of thy (Var((a,0),ty));
-in
-fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong'
-end;
+val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
 
-(*Removes the lambdas from an equation of the form t = (%x. u).  A non-negative n,
-  serves as an upper bound on how many to remove.*)
-fun strip_lambdas 0 th = th
-  | strip_lambdas n th =
-      case prop_of th of
-          _ $ (Const (@{const_name "op ="}, _) $ _ $ Abs (x, _, _)) =>
-              strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
-        | _ => th;
+(* Removes the lambdas from an equation of the form t = (%x. u). *)
+fun extensionalize th =
+  case prop_of th of
+    _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
+         $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
+  | _ => th
 
 fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
   | is_quasi_lambda_free (t1 $ t2) =
@@ -339,9 +328,9 @@
 fun to_nnf th ctxt0 =
   let val th1 = th |> transform_elim |> zero_var_indexes
       val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
-      val th3 = th2
-        |> Conv.fconv_rule Object_Logic.atomize
-        |> Meson.make_nnf ctxt |> strip_lambdas ~1
+      val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
+                    |> extensionalize
+                    |> Meson.make_nnf ctxt
   in  (th3, ctxt)  end;
 
 (*Generate Skolem functions for a theorem supplied in nnf*)