[isabelle-dev] Function package creates duplicate simp rule

[Fabian Huch]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230125/f18ca370/attachment.htm>