# HG changeset patch
# User blanchet
# Date 1282294681 -7200
# Node ID 01ed56c46259d76b6b760e53fcca21b20905c560
# Parent  a2abe8c2a1c2e932eec846f74642eec32327f853
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
another consequence of the transition to FOF

diff -r a2abe8c2a1c2 -r 01ed56c46259 src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Thu Aug 19 19:34:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Aug 20 10:58:01 2010 +0200
@@ -83,7 +83,7 @@
 val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
 
 (* Removes the lambdas from an equation of the form "t = (%x. u)".
-   (Cf. "extensionalize_term" in "ATP_Systems".) *)
+   (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
 fun extensionalize_theorem th =
   case prop_of th of
     _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
@@ -223,12 +223,13 @@
 (* Converts an Isabelle theorem (intro, elim or simp format, even higher-order)
    into NNF. *)
 fun to_nnf th ctxt0 =
-  let val th1 = th |> transform_elim_theorem |> zero_var_indexes
-      val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
-      val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
-                    |> extensionalize_theorem
-                    |> Meson.make_nnf ctxt
-  in  (th3, ctxt)  end;
+  let
+    val th1 = th |> transform_elim_theorem |> zero_var_indexes
+    val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
+    val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
+                  |> extensionalize_theorem
+                  |> Meson.make_nnf ctxt
+  in (th3, ctxt) end
 
 (* Convert a theorem to CNF, with Skolem functions as additional premises. *)
 fun cnf_axiom thy th =
diff -r a2abe8c2a1c2 -r 01ed56c46259 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 19 19:34:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 20 10:58:01 2010 +0200
@@ -103,6 +103,25 @@
   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
                     (0 upto length Ts - 1 ~~ Ts))
 
+(* 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 introduce_combinators_in_term ctxt kind t =
   let val thy = ProofContext.theory_of ctxt in
     if Meson.is_fol_term thy t then
@@ -170,7 +189,8 @@
 fun make_formula ctxt presimp (name, kind, t) =
   let
     val thy = ProofContext.theory_of ctxt
-    val t = t |> transform_elim_term
+    val t = t |> Envir.beta_eta_contract
+              |> transform_elim_term
               |> atomize_term
     val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
               |> extensionalize_term
diff -r a2abe8c2a1c2 -r 01ed56c46259 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Aug 19 19:34:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Aug 20 10:58:01 2010 +0200
@@ -15,7 +15,6 @@
   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
@@ -101,25 +100,6 @@
            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
diff -r a2abe8c2a1c2 -r 01ed56c46259 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Aug 19 19:34:11 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Fri Aug 20 10:58:01 2010 +0200
@@ -520,15 +520,14 @@
         forward_res ctxt (make_nnf1 ctxt)
            (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
     handle THM ("tryres", _, _) => th
-  else th;
+  else th
 
 (*The simplification removes defined quantifiers and occurrences of True and False.
   nnf_ss also includes the one-point simprocs,
   which are needed to avoid the various one-point theorems from generating junk clauses.*)
 val nnf_simps =
   @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel
-         if_eq_cancel cases_simp (* TODO: mem_def_raw Collect_def_raw *)}
-(* TODO:  @ [@{lemma "{} = (%x. False)" by (rule ext) auto}] *)
+         if_eq_cancel cases_simp}
 val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
 
 val nnf_ss =