<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <p>The function package produces a duplicate simp rule in some
      circumstances. MWE:</p>
    <blockquote>
      <p>fun a :: "bool ⇒ bool ⇒ bool ⇒ bool" where<br>
          "a True True _ = True" |<br>
          "a False True False = True" |<br>
          "a True _ True = True" |<br>
          "a _ _ _ = False"<br>
      </p>
    </blockquote>
    <p>Creates the warning:</p>
    <blockquote>
      <p>Ignoring duplicate rewrite rule:<br>
        a False False ?uy1 ≡ False <br>
      </p>
    </blockquote>
    <p>and indeed, the simps do contain a duplicate:</p>
    <blockquote>
      <p>  a True True ?uu = True<br>
          a False True False = True<br>
          a True False True = True<br>
          a False False ?uy = False<br>
          a False ?ux True = False<br>
          a False False ?uy = False<br>
          a ?uw False False = False<br>
      </p>
    </blockquote>
    <p>It does not do that when one changes the order of most things, or
      removes a parameter or case.</p>
    <p>We had a somewhat similar problem before [1], but it's a
      different kind of rule that is now duplicated.</p>
    <p>This occurs both in Isabelle2022 and current devel.<br>
    </p>
    <p><br>
    </p>
    <p>Fabian<br>
    </p>
  </body>
</html>