Email Gateway (Jul 30 2023 at 13:03): Email Gateway (Jul 30 2023 at 13:03):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hello,
terms like "{0,1}×{0,1}" fail to simplify with the default simp-set of
HOL, even though there are rules that seem to be intended for this purpose.
The reason is that the various simplification rules for explicit sets
often have the condition, that all elements listed within one set are
distinct. E.g., if we encounter {0,1,0}, simplification will usually fail.
This is the case in the example above, however, the simpset rule
insert_Times_insert fails to maintain this invariant. It unnecessarily
lists some elements twice.
I'm attaching an example theory that also contains a suggested improved
rule insert_Times_insert' (supposed to replace insert_Times_insert in
the simpset).
This is not a regression of RC2, the same behavior occurs with 2022, but
it might be a convenient moment for changing this.
Best wishes,
Dominique.
Email Gateway (Aug 06 2023 at 13:08):From: Makarius <makarius@sketis.net>
If it is not a regression from the last release, then the convenient time to
consider is after the Isabelle2023 release, and especially the corresponding
AFP release.
Makarius
Email Gateway (Aug 09 2023 at 17:33):From: Tobias Nipkow <nipkow@in.tum.de>
Hi Dominique,
Done. Only a few proofs in 2 AFP entries were affected - positively :-)
Thanks
Tobias
Last updated: May 05 2024 at 01:11 UTC