# HG changeset patch
# User blanchet
# Date 1280159770 -7200
# Node ID c0b9efa8bfcaa972dc1504e67677957f88800dd1
# Parent  12a559b5c55045489245eea9b236e271f3854a49
added extensionalization to Sledgehammer, mimicking what the Clausifier used to do

diff -r 12a559b5c550 -r c0b9efa8bfca src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 17:26:02 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 17:56:10 2010 +0200
@@ -153,12 +153,29 @@
                        |>> APred ||> union (op =) ts)
   in do_formula [] end
 
+(* Removes the lambdas from an equation of the form "t = (%x. u)" (cf.
+   "extensionalize_theorem" in "Clausifier"). *)
+fun extensionalize_term t =
+  let
+    fun aux j (Const (@{const_name "op ="}, _) $ t2 $ Abs (s, var_T, t')) =
+        let
+          val T' = fastype_of t'
+          val var_t = Var (("x", j), var_T)
+        in
+          Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT)
+            $ betapply (t2, var_t) $ subst_bound (var_t, t')
+          |> aux (j + 1)
+        end
+      | aux _ t = t
+  in aux (maxidx_of_term t + 1) t end
+
 (* making axiom and conjecture clauses *)
 fun make_clause thy (formula_id, formula_name, kind, t) =
   let
     (* ### FIXME: introduce combinators and perform other transformations
        previously done by Clausifier.to_nnf *)
     val t = t |> Object_Logic.atomize_term thy
+              |> extensionalize_term
     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   in
     FOLFormula {formula_name = formula_name, formula_id = formula_id,
diff -r 12a559b5c550 -r c0b9efa8bfca src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jul 26 17:26:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jul 26 17:56:10 2010 +0200
@@ -82,11 +82,13 @@
 
 val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
 
-(* Removes the lambdas from an equation of the form t = (%x. u). *)
-fun extensionalize th =
+(* ### FIXME: removes only one lambda? *)
+(* Removes the lambdas from an equation of the form "t = (%x. u)" (cf.
+   "extensionalize_term" in "ATP_Systems"). *)
+fun extensionalize_theorem th =
   case prop_of th of
     _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
-         $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
+         $ _ $ Abs (s, _, _)) => extensionalize_theorem (th RS fun_cong_all)
   | _ => th
 
 fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
@@ -226,7 +228,7 @@
   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
-                    |> extensionalize
+                    |> extensionalize_theorem
                     |> Meson.make_nnf ctxt
   in  (th3, ctxt)  end;