Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Function package creates duplicate simp rule


view this post on Zulip 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: Mar 04 2024 at 10:08 UTC