<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>