1.1 --- a/src/HOL/Meson.thy	Mon May 21 16:37:28 2012 +0200
     1.2 +++ b/src/HOL/Meson.thy	Tue May 22 16:59:27 2012 +0200
     1.3 @@ -125,6 +125,12 @@
     1.4  lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
     1.5  by simp
     1.6  
     1.7 +lemma ext_cong_neq: "F g \<noteq> F h \<Longrightarrow> F g \<noteq> F h \<and> (\<exists>x. g x \<noteq> h x)"
     1.8 +apply (erule contrapos_np)
     1.9 +apply clarsimp
    1.10 +apply (rule cong[where f = F])
    1.11 +by auto
    1.12 +
    1.13  
    1.14  text{* Combinator translation helpers *}
    1.15  
    1.16 @@ -198,7 +204,7 @@
    1.17  hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD
    1.18      not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD
    1.19      disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI
    1.20 -    COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K abs_B abs_C
    1.21 -    abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D
    1.22 +    ext_cong_neq COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K
    1.23 +    abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D
    1.24  
    1.25  end

     2.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon May 21 16:37:28 2012 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue May 22 16:59:27 2012 +0200
     2.3 @@ -1272,7 +1272,7 @@
     2.4      val is_ho = is_type_enc_higher_order type_enc
     2.5    in
     2.6      t |> need_trueprop ? HOLogic.mk_Trueprop
     2.7 -      |> (if is_ho then unextensionalize_def else extensionalize_term ctxt)
     2.8 +      |> (if is_ho then unextensionalize_def else abs_extensionalize_term ctxt)
     2.9        |> presimplify_term thy
    2.10        |> HOLogic.dest_Trueprop
    2.11    end

     3.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Mon May 21 16:37:28 2012 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Tue May 22 16:59:27 2012 +0200
     3.3 @@ -36,7 +36,7 @@
     3.4    val open_form : (string -> string) -> term -> term
     3.5    val monomorphic_term : Type.tyenv -> term -> term
     3.6    val eta_expand : typ list -> term -> int -> term
     3.7 -  val extensionalize_term : Proof.context -> term -> term
     3.8 +  val abs_extensionalize_term : Proof.context -> term -> term
     3.9    val transform_elim_prop : term -> term
    3.10    val specialize_type : theory -> (string * typ) -> term -> term
    3.11    val strip_subgoal :
    3.12 @@ -302,10 +302,10 @@
    3.13                       Type (_, [Type (@{type_name fun}, _), _])) = true
    3.14    | is_fun_equality _ = false
    3.15  
    3.16 -fun extensionalize_term ctxt t =
    3.17 +fun abs_extensionalize_term ctxt t =
    3.18    if exists_Const is_fun_equality t then
    3.19      let val thy = Proof_Context.theory_of ctxt in
    3.20 -      t |> cterm_of thy |> Meson.extensionalize_conv ctxt
    3.21 +      t |> cterm_of thy |> Meson.abs_extensionalize_conv ctxt
    3.22          |> prop_of |> Logic.dest_equals |> snd
    3.23      end
    3.24    else

     4.1 --- a/src/HOL/Tools/Meson/meson.ML	Mon May 21 16:37:28 2012 +0200
     4.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue May 22 16:59:27 2012 +0200
     4.3 @@ -24,8 +24,8 @@
     4.4    val choice_theorems : theory -> thm list
     4.5    val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
     4.6    val skolemize : Proof.context -> thm -> thm
     4.7 -  val extensionalize_conv : Proof.context -> conv
     4.8 -  val extensionalize_theorem : Proof.context -> thm -> thm
     4.9 +  val abs_extensionalize_conv : Proof.context -> conv
    4.10 +  val abs_extensionalize_thm : Proof.context -> thm -> thm
    4.11    val make_clauses_unsorted: Proof.context -> thm list -> thm list
    4.12    val make_clauses: Proof.context -> thm list -> thm list
    4.13    val make_horns: thm list -> thm list
    4.14 @@ -574,29 +574,47 @@
    4.15  (* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
    4.16     would be desirable to do this symmetrically but there's at least one existing
    4.17     proof in "Tarski" that relies on the current behavior. *)
    4.18 -fun extensionalize_conv ctxt ct =
    4.19 +fun abs_extensionalize_conv ctxt ct =
    4.20    case term_of ct of
    4.21      Const (@{const_name HOL.eq}, _) $ _ $ Abs _ =>
    4.22      ct |> (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
    4.23 -           then_conv extensionalize_conv ctxt)
    4.24 -  | _ $ _ => Conv.comb_conv (extensionalize_conv ctxt) ct
    4.25 -  | Abs _ => Conv.abs_conv (extensionalize_conv o snd) ctxt ct
    4.26 +           then_conv abs_extensionalize_conv ctxt)
    4.27 +  | _ $ _ => Conv.comb_conv (abs_extensionalize_conv ctxt) ct
    4.28 +  | Abs _ => Conv.abs_conv (abs_extensionalize_conv o snd) ctxt ct
    4.29    | _ => Conv.all_conv ct
    4.30  
    4.31 -val extensionalize_theorem = Conv.fconv_rule o extensionalize_conv
    4.32 +val abs_extensionalize_thm = Conv.fconv_rule o abs_extensionalize_conv
    4.33 +
    4.34 +(*
    4.35 +(* Weakens negative occurrences of "f g = f h" to
    4.36 +   "(ALL x. g x = h x) | f g = f h". *)
    4.37 +fun cong_extensionalize_conv ctxt ct =
    4.38 +  case term_of ct of
    4.39 +    @{const Trueprop} $ (@{const Not} $ (Const (@{const_name HOL.eq}, _)
    4.40 +                                         $ (t as _ $ _) $ (u as _ $ _))) =>
    4.41 +    (case get_f_pattern t u of
    4.42 +       SOME _ => Conv.all_conv ct
    4.43 +     | NONE => Conv.all_conv ct)
    4.44 +  | _ => Conv.all_conv ct
    4.45 +
    4.46 +val cong_extensionalize_thm = Conv.fconv_rule o cong_extensionalize_conv
    4.47 +*)
    4.48 +
    4.49 +fun cong_extensionalize_thm ctxt = I (*###*)
    4.50  
    4.51  (* "RS" can fail if "unify_search_bound" is too small. *)
    4.52  fun try_skolemize_etc ctxt th =
    4.53 -  (* Extensionalize "th", because that makes sense and that's what Sledgehammer
    4.54 -     does, but also keep an unextensionalized version of "th" for backward
    4.55 -     compatibility. *)
    4.56 -  [th] |> insert Thm.eq_thm_prop (extensionalize_theorem ctxt th)
    4.57 -       |> map_filter (fn th => th |> try (skolemize ctxt)
    4.58 -                                  |> tap (fn NONE =>
    4.59 -                                             trace_msg ctxt (fn () =>
    4.60 -                                                 "Failed to skolemize " ^
    4.61 -                                                  Display.string_of_thm ctxt th)
    4.62 -                                           | _ => ()))
    4.63 +  (* Extensionalize lambdas in "th", because that makes sense and that's what
    4.64 +     Sledgehammer does, but also keep an unextensionalized version of "th" for
    4.65 +     backward compatibility. *)
    4.66 +  [th |> cong_extensionalize_thm ctxt]
    4.67 +  |> insert Thm.eq_thm_prop (abs_extensionalize_thm ctxt th)
    4.68 +  |> map_filter (fn th => th |> try (skolemize ctxt)
    4.69 +                             |> tap (fn NONE =>
    4.70 +                                        trace_msg ctxt (fn () =>
    4.71 +                                            "Failed to skolemize " ^
    4.72 +                                             Display.string_of_thm ctxt th)
    4.73 +                                      | _ => ()))
    4.74  
    4.75  fun add_clauses ctxt th cls =
    4.76    let val ctxt0 = Variable.global_thm_context th

     5.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Mon May 21 16:37:28 2012 +0200
     5.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue May 22 16:59:27 2012 +0200
     5.3 @@ -309,8 +309,7 @@
     5.4           |> new_skolemizer ? forall_intr_vars
     5.5      val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
     5.6      val th = th |> Conv.fconv_rule Object_Logic.atomize
     5.7 -                |> extensionalize_theorem ctxt
     5.8 -                |> make_nnf ctxt
     5.9 +                |> abs_extensionalize_thm ctxt |> make_nnf ctxt
    5.10    in
    5.11      if new_skolemizer then
    5.12        let

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon May 21 16:37:28 2012 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue May 22 16:59:27 2012 +0200
     6.3 @@ -391,8 +391,8 @@
     6.4        | (Abs (_, T, t'), ts) =>
     6.5          ((null ts andalso not ext_arg)
     6.6           (* Since lambdas on the right-hand side of equalities are usually
     6.7 -            extensionalized later by "extensionalize_term", we don't penalize
     6.8 -            them here. *)
     6.9 +            extensionalized later by "abs_extensionalize_term", we don't
    6.10 +            penalize them here. *)
    6.11           ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, [])))
    6.12          #> fold (do_term false) (t' :: ts)
    6.13        | (_, ts) => fold (do_term false) ts