Email Gateway (Aug 19 2022 at 09:35): Email Gateway (Aug 19 2022 at 09:35):From: Peter Lammich <lammich@in.tum.de>
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?
-- 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
Email Gateway (Aug 19 2022 at 09:35):From: Tobias Nipkow <nipkow@in.tum.de>
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 nonelemma [simp]: "f x \<equiv> g x" by simp <-- Here, I actually get the
warning
Last updated: Apr 25 2024 at 16:19 UTC