--- 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
--- 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
--- 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
--- 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