# HG changeset patch
# User blanchet
# Date 1337698767 -7200
# Node ID aada9fd08b58f846331019574c41c170d13d4b36
# Parent  a2c3706c4cb18074d932cf2fdb6db246dd65841c
make higher-order goals more first-order via extensionality

diff -r a2c3706c4cb1 -r aada9fd08b58 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue May 22 16:59:27 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue May 22 16:59:27 2012 +0200
@@ -1272,7 +1272,8 @@
     val is_ho = is_type_enc_higher_order type_enc
   in
     t |> need_trueprop ? HOLogic.mk_Trueprop
-      |> (if is_ho then unextensionalize_def else abs_extensionalize_term ctxt)
+      |> (if is_ho then unextensionalize_def
+          else cong_extensionalize_term thy #> abs_extensionalize_term ctxt)
       |> presimplify_term thy
       |> HOLogic.dest_Trueprop
   end
diff -r a2c3706c4cb1 -r aada9fd08b58 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Tue May 22 16:59:27 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue May 22 16:59:27 2012 +0200
@@ -36,6 +36,7 @@
   val open_form : (string -> string) -> term -> term
   val monomorphic_term : Type.tyenv -> term -> term
   val eta_expand : typ list -> term -> int -> term
+  val cong_extensionalize_term : theory -> term -> term
   val abs_extensionalize_term : Proof.context -> term -> term
   val transform_elim_prop : term -> term
   val specialize_type : theory -> (string * typ) -> term -> term
@@ -298,6 +299,14 @@
              (List.take (binder_types (fastype_of1 (Ts, t)), n))
              (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
 
+fun cong_extensionalize_term thy t =
+  if exists_Const (fn (s, _) => s = @{const_name Not}) t then
+    t |> Skip_Proof.make_thm thy
+      |> Meson.cong_extensionalize_thm thy
+      |> prop_of
+  else
+    t
+
 fun is_fun_equality (@{const_name HOL.eq},
                      Type (_, [Type (@{type_name fun}, _), _])) = true
   | is_fun_equality _ = false
diff -r a2c3706c4cb1 -r aada9fd08b58 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Tue May 22 16:59:27 2012 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Tue May 22 16:59:27 2012 +0200
@@ -24,6 +24,7 @@
   val choice_theorems : theory -> thm list
   val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
   val skolemize : Proof.context -> thm -> thm
+  val cong_extensionalize_thm : theory -> thm -> thm
   val abs_extensionalize_conv : Proof.context -> conv
   val abs_extensionalize_thm : Proof.context -> thm -> thm
   val make_clauses_unsorted: Proof.context -> thm list -> thm list
@@ -571,6 +572,52 @@
     skolemize_with_choice_theorems ctxt (choice_theorems thy)
   end
 
+exception NO_F_PATTERN of unit
+
+fun get_F_pattern t u =
+  let
+    fun pat t u =
+      let
+        val ((head1, args1), (head2, args2)) = (t, u) |> pairself strip_comb
+      in
+        if head1 = head2 then
+          let val pats = map2 pat args1 args2 in
+            case filter (is_some o fst) pats of
+              [(SOME T, _)] => (SOME T, list_comb (head1, map snd pats))
+            | [] => (NONE, t)
+            | _ => raise NO_F_PATTERN ()
+          end
+        else
+          let val T = fastype_of t in
+            if can dest_funT T then (SOME T, Bound 0) else raise NO_F_PATTERN ()
+          end
+      end
+  in
+    (case pat t u of
+       (SOME T, p as _ $ _) => SOME (Abs (Name.uu, T, p))
+     | _ => NONE)
+    handle NO_F_PATTERN () => NONE
+  end
+
+val ext_cong_neq = @{thm ext_cong_neq}
+val F_ext_cong_neq =
+  Term.add_vars (prop_of @{thm ext_cong_neq}) []
+  |> filter (fn ((s, _), _) => s = "F")
+  |> the_single |> Var
+
+(* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
+fun cong_extensionalize_thm thy th =
+  case concl_of th of
+    @{const Trueprop} $ (@{const Not} $ (Const (@{const_name HOL.eq}, _)
+                                         $ (t as _ $ _) $ (u as _ $ _))) =>
+    (case get_F_pattern t u of
+       SOME p =>
+       let val inst = [pairself (cterm_of thy) (F_ext_cong_neq, p)] in
+         th RS cterm_instantiate inst ext_cong_neq
+       end
+     | NONE => th)
+  | _ => th
+
 (* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
    would be desirable to do this symmetrically but there's at least one existing
    proof in "Tarski" that relies on the current behavior. *)
@@ -585,36 +632,24 @@
 
 val abs_extensionalize_thm = Conv.fconv_rule o abs_extensionalize_conv
 
-(*
-(* Weakens negative occurrences of "f g = f h" to
-   "(ALL x. g x = h x) | f g = f h". *)
-fun cong_extensionalize_conv ctxt ct =
-  case term_of ct of
-    @{const Trueprop} $ (@{const Not} $ (Const (@{const_name HOL.eq}, _)
-                                         $ (t as _ $ _) $ (u as _ $ _))) =>
-    (case get_f_pattern t u of
-       SOME _ => Conv.all_conv ct
-     | NONE => Conv.all_conv ct)
-  | _ => Conv.all_conv ct
-
-val cong_extensionalize_thm = Conv.fconv_rule o cong_extensionalize_conv
-*)
-
-fun cong_extensionalize_thm ctxt = I (*###*)
-
 (* "RS" can fail if "unify_search_bound" is too small. *)
 fun try_skolemize_etc ctxt th =
-  (* Extensionalize lambdas in "th", because that makes sense and that's what
-     Sledgehammer does, but also keep an unextensionalized version of "th" for
-     backward compatibility. *)
-  [th |> cong_extensionalize_thm ctxt]
-  |> insert Thm.eq_thm_prop (abs_extensionalize_thm ctxt th)
-  |> map_filter (fn th => th |> try (skolemize ctxt)
-                             |> tap (fn NONE =>
-                                        trace_msg ctxt (fn () =>
-                                            "Failed to skolemize " ^
-                                             Display.string_of_thm ctxt th)
-                                      | _ => ()))
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val th = th |> cong_extensionalize_thm thy
+  in
+    [th]
+    (* Extensionalize lambdas in "th", because that makes sense and that's what
+       Sledgehammer does, but also keep an unextensionalized version of "th" for
+       backward compatibility. *)
+    |> insert Thm.eq_thm_prop (abs_extensionalize_thm ctxt th)
+    |> map_filter (fn th => th |> try (skolemize ctxt)
+                               |> tap (fn NONE =>
+                                          trace_msg ctxt (fn () =>
+                                              "Failed to skolemize " ^
+                                               Display.string_of_thm ctxt th)
+                                        | _ => ()))
+  end
 
 fun add_clauses ctxt th cls =
   let val ctxt0 = Variable.global_thm_context th
diff -r a2c3706c4cb1 -r aada9fd08b58 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue May 22 16:59:27 2012 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue May 22 16:59:27 2012 +0200
@@ -309,7 +309,9 @@
          |> new_skolemizer ? forall_intr_vars
     val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
     val th = th |> Conv.fconv_rule Object_Logic.atomize
-                |> abs_extensionalize_thm ctxt |> make_nnf ctxt
+                |> cong_extensionalize_thm thy
+                |> abs_extensionalize_thm ctxt
+                |> make_nnf ctxt
   in
     if new_skolemizer then
       let