# Re: [isabelle] Simplifier: Ignoring duplicate rewrite rule should be modulo alpha-equivalence

Am 20/12/2012 18:24, schrieb Peter Lammich:
> Hi all,
>
> I just stumbled over the following behaviour of the simplifier, which
> seems to issue "ignoring duplicate rewrite rule" warnings only on
> literally equivalent theorems. I would have expected (at least) alpha
> equivalence here. Any reasons for the current behaviour?
It was simpler to implement. The simplifier actually does check for
alpha-equivalence. But you would like alpha-equivalence of a lifted version of
the thms, namely (%x. f x) = (%x. g x) and (%y. f y) = (%y. g y). The cost /
benefit ratio of a change is too high (for me), sorry.
Tobias
> -- Peter
>
> consts
> f :: "unit \<Rightarrow> unit"
> g :: "unit \<Rightarrow> unit"
> lemma [simp]: "f x \<equiv> g x" by simp
> lemma [simp]: "f y \<equiv> g y" by simp <-- Here, I would expect a
> warning about ignored duplicate rewrite rule, but get none
>
> lemma [simp]: "f x \<equiv> g x" by simp <-- Here, I actually get the
> warning
>
>

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*