Email Gateway (Jan 25 2023 at 17:04): Email Gateway (Jan 25 2023 at 17:04):From: Fabian Huch <huch@in.tum.de>
The function package produces a duplicate simp rule in some
circumstances. MWE:
fun a :: "bool ⇒ bool ⇒ bool ⇒ bool" where
"a True True _ = True" |
"a False True False = True" |
"a True _ True = True" |
"a _ _ _ = False"
Creates the warning:
Ignoring duplicate rewrite rule:
a False False ?uy1 ≡ False
and indeed, the simps do contain a duplicate:
a True True ?uu = True
a False True False = True
a True False True = True
a False False ?uy = False
a False ?ux True = False
a False False ?uy = False
a ?uw False False = False
It does not do that when one changes the order of most things, or
removes a parameter or case.
We had a somewhat similar problem before [1], but it's a different kind
of rule that is now duplicated.
This occurs both in Isabelle2022 and current devel.
Fabian
Last updated: Apr 28 2024 at 08:19 UTC