# HG changeset patch
# User blanchet
# Date 1281004812 -7200
# Node ID 2f531f620cb8cab47722642e262ff9652cdaccd2
# Parent  8a9cace789d6c4da57bfac729fe660b7b03bdc96
fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization

diff -r 8a9cace789d6 -r 2f531f620cb8 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 05 11:54:53 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 05 12:40:12 2010 +0200
@@ -1728,12 +1728,15 @@
 (** Axiom extraction/generation **)
 
 fun equationalize t =
-  case Logic.strip_horn t of
-    (_, @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ _)) => t
-  | (prems, @{const Trueprop} $ t') =>
+  let val (prems, concl) = Logic.strip_horn t in
     Logic.list_implies (prems,
-                        @{const Trueprop} $ HOLogic.mk_eq (t', @{const True}))
-  | _ => t
+        case concl of
+          @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ _) =>
+          extensionalize_term concl
+        | @{const Trueprop} $ t' =>
+          @{const Trueprop} $ HOLogic.mk_eq (t', @{const True})
+        | _ => extensionalize_term concl)
+  end
 
 fun pair_for_prop t =
   case term_under_def t of
diff -r 8a9cace789d6 -r 2f531f620cb8 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Aug 05 11:54:53 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Aug 05 12:40:12 2010 +0200
@@ -64,6 +64,7 @@
     -> typ
   val is_of_class_const : theory -> string * typ -> bool
   val get_class_def : theory -> string -> (string * term) option
+  val extensionalize_term : term -> term
   val monomorphic_term : Type.tyenv -> term -> term
   val specialize_type : theory -> string * typ -> term -> term
   val nat_subscript : int -> string
@@ -250,6 +251,7 @@
 val typ_of_dtyp = Refute.typ_of_dtyp
 val is_of_class_const = Refute.is_const_of_class
 val get_class_def = Refute.get_classdef
+val extensionalize_term = Sledgehammer_Util.extensionalize_term
 val monomorphic_term = Sledgehammer_Util.monomorphic_term
 val specialize_type = Sledgehammer_Util.specialize_type
 
diff -r 8a9cace789d6 -r 2f531f620cb8 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Aug 05 11:54:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Aug 05 12:40:12 2010 +0200
@@ -220,20 +220,6 @@
   | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t
   | _ => t
 
-(* 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 ="}, Type (_, [Type (_, [_, T']), _]))
-               $ t2 $ Abs (s, var_T, t')) =
-        let 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
-
 fun presimplify_term thy =
   Skip_Proof.make_thm thy
   #> Meson.presimplify
diff -r 8a9cace789d6 -r 2f531f620cb8 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Aug 05 11:54:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Aug 05 12:40:12 2010 +0200
@@ -15,6 +15,7 @@
   val nat_subscript : int -> string
   val unyxml : string -> string
   val maybe_quote : string -> string
+  val extensionalize_term : term -> term
   val monomorphic_term : Type.tyenv -> term -> term
   val specialize_type : theory -> (string * typ) -> term -> term
   val subgoal_count : Proof.state -> int
@@ -100,6 +101,25 @@
            Keyword.is_keyword s) ? quote
   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 Trueprop} $ t') = @{const Trueprop} $ aux j t'
+      | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
+                                        Type (_, [_, res_T])]))
+                    $ t2 $ Abs (var_s, var_T, t')) =
+        if s = @{const_name "op ="} orelse s = @{const_name "=="} then
+          let val var_t = Var ((var_s, j), var_T) in
+            Const (s, T' --> T' --> res_T)
+              $ betapply (t2, var_t) $ subst_bound (var_t, t')
+            |> aux (j + 1)
+          end
+        else
+          t
+      | aux _ t = t
+  in aux (maxidx_of_term t + 1) t end
+
 fun monomorphic_term subst t =
   map_types (map_type_tvar (fn v =>
       case Type.lookup subst v of