--- a/src/HOL/Meson.thy Mon May 21 16:37:28 2012 +0200
+++ b/src/HOL/Meson.thy Tue May 22 16:59:27 2012 +0200
@@ -125,6 +125,12 @@
lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
by simp
+lemma ext_cong_neq: "F g \<noteq> F h \<Longrightarrow> F g \<noteq> F h \<and> (\<exists>x. g x \<noteq> h x)"
+apply (erule contrapos_np)
+apply clarsimp
+apply (rule cong[where f = F])
+by auto
+
text{* Combinator translation helpers *}
@@ -198,7 +204,7 @@
hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD
not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD
disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI
- COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K abs_B abs_C
- abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D
+ ext_cong_neq COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K
+ abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D
end
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon May 21 16:37:28 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue May 22 16:59:27 2012 +0200
@@ -1272,7 +1272,7 @@
val is_ho = is_type_enc_higher_order type_enc
in
t |> need_trueprop ? HOLogic.mk_Trueprop
- |> (if is_ho then unextensionalize_def else extensionalize_term ctxt)
+ |> (if is_ho then unextensionalize_def else abs_extensionalize_term ctxt)
|> presimplify_term thy
|> HOLogic.dest_Trueprop
end
--- a/src/HOL/Tools/ATP/atp_util.ML Mon May 21 16:37:28 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Tue May 22 16:59:27 2012 +0200
@@ -36,7 +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 extensionalize_term : Proof.context -> term -> term
+ val abs_extensionalize_term : Proof.context -> term -> term
val transform_elim_prop : term -> term
val specialize_type : theory -> (string * typ) -> term -> term
val strip_subgoal :
@@ -302,10 +302,10 @@
Type (_, [Type (@{type_name fun}, _), _])) = true
| is_fun_equality _ = false
-fun extensionalize_term ctxt t =
+fun abs_extensionalize_term ctxt t =
if exists_Const is_fun_equality t then
let val thy = Proof_Context.theory_of ctxt in
- t |> cterm_of thy |> Meson.extensionalize_conv ctxt
+ t |> cterm_of thy |> Meson.abs_extensionalize_conv ctxt
|> prop_of |> Logic.dest_equals |> snd
end
else
--- a/src/HOL/Tools/Meson/meson.ML Mon May 21 16:37:28 2012 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Tue May 22 16:59:27 2012 +0200
@@ -24,8 +24,8 @@
val choice_theorems : theory -> thm list
val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
val skolemize : Proof.context -> thm -> thm
- val extensionalize_conv : Proof.context -> conv
- val extensionalize_theorem : Proof.context -> 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
val make_clauses: Proof.context -> thm list -> thm list
val make_horns: thm list -> thm list
@@ -574,29 +574,47 @@
(* 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. *)
-fun extensionalize_conv ctxt ct =
+fun abs_extensionalize_conv ctxt ct =
case term_of ct of
Const (@{const_name HOL.eq}, _) $ _ $ Abs _ =>
ct |> (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
- then_conv extensionalize_conv ctxt)
- | _ $ _ => Conv.comb_conv (extensionalize_conv ctxt) ct
- | Abs _ => Conv.abs_conv (extensionalize_conv o snd) ctxt ct
+ then_conv abs_extensionalize_conv ctxt)
+ | _ $ _ => Conv.comb_conv (abs_extensionalize_conv ctxt) ct
+ | Abs _ => Conv.abs_conv (abs_extensionalize_conv o snd) ctxt ct
| _ => Conv.all_conv ct
-val extensionalize_theorem = Conv.fconv_rule o extensionalize_conv
+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 "th", because that makes sense and that's what Sledgehammer
- does, but also keep an unextensionalized version of "th" for backward
- compatibility. *)
- [th] |> insert Thm.eq_thm_prop (extensionalize_theorem 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)
- | _ => ()))
+ (* 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)
+ | _ => ()))
fun add_clauses ctxt th cls =
let val ctxt0 = Variable.global_thm_context th
--- a/src/HOL/Tools/Meson/meson_clausify.ML Mon May 21 16:37:28 2012 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue May 22 16:59:27 2012 +0200
@@ -309,8 +309,7 @@
|> 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
- |> extensionalize_theorem ctxt
- |> make_nnf ctxt
+ |> abs_extensionalize_thm ctxt |> make_nnf ctxt
in
if new_skolemizer then
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon May 21 16:37:28 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue May 22 16:59:27 2012 +0200
@@ -391,8 +391,8 @@
| (Abs (_, T, t'), ts) =>
((null ts andalso not ext_arg)
(* Since lambdas on the right-hand side of equalities are usually
- extensionalized later by "extensionalize_term", we don't penalize
- them here. *)
+ extensionalized later by "abs_extensionalize_term", we don't
+ penalize them here. *)
? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, [])))
#> fold (do_term false) (t' :: ts)
| (_, ts) => fold (do_term false) ts