Email Gateway (Aug 22 2022 at 12:15): Email Gateway (Aug 22 2022 at 12:15):From: Peter Lammich <lammich@in.tum.de>
Hi,
induction on custom data types may still produce constants like
Basic_BNFs.snds, and these have no default simplifier setup.
(I reported this behaviour to Dmitry privately some time ago, and just
stumbled over it accidentally, hoping it would long be fixed)
Things like thm Basic_BNFs.snds.simp should be in the default simpset,
or rules like
"Basic_BNFs.snds (n, T) = {T}"
Email Gateway (Aug 22 2022 at 12:16):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Peter,
Basic_BNFs.snds is a set function for products, and therefore it naturally (i.e. like for any other type) occurs in induction rules whenever the user write the product types in a datatype declaration explicitly (as opposed to using multiple constructor arguments).
But indeed there should be simp rules. The rules are in principle there:
thm prod_set_simps
thm sum_set_simps
However, we (Jasmin and me) have always been very conservative about default rule. I’m pretty sure there are more such “safe" rules that are not registered by default.
The attached patch, which currently runs on the testboard (https://ci.isabelle.systems/jenkins/job/isabelle-testboard-makeall/53/), makes them simp rules. However, with the testboard still not testing the AFP and isatest testing isabelle-release, we are in the unfortunate situation that it is not possible to test the AFP, unless we do it on our own machines. I currently do not have the hardware at hand to build the big guys from the AFP, although I have good hope that the patch does not break anything. If somebody can confirm that, than we could push it (but it is not a very important thing, since it is easy to add simp rules locally).
Dmitriy
prod_sum_set_simps.patch
Last updated: Apr 25 2024 at 08:20 UTC