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.