# HG changeset patch # User blanchet # Date 1337698767 -7200 # Node ID a2c3706c4cb18074d932cf2fdb6db246dd65841c # Parent 36a8c477dae88b6ba44226e229c99ef66c6312bb added "ext_cong_neq" lemma (not used yet); tuning diff -r 36a8c477dae8 -r a2c3706c4cb1 src/HOL/Meson.thy --- 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 \ Q \ Trueprop P \ Trueprop Q" by simp +lemma ext_cong_neq: "F g \ F h \ F g \ F h \ (\x. g x \ 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 diff -r 36a8c477dae8 -r a2c3706c4cb1 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 diff -r 36a8c477dae8 -r a2c3706c4cb1 src/HOL/Tools/ATP/atp_util.ML --- 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 diff -r 36a8c477dae8 -r a2c3706c4cb1 src/HOL/Tools/Meson/meson.ML --- 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 diff -r 36a8c477dae8 -r a2c3706c4cb1 src/HOL/Tools/Meson/meson_clausify.ML --- 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 diff -r 36a8c477dae8 -r a2c3706c4cb1 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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