Email Gateway (Aug 19 2022 at 16:21): Email Gateway (Aug 19 2022 at 16:21):From: Julian Brunner <julianbrunner@gmail.com>
Dear all,
I've stumbled upon a few issues with the theory
Library/Prefix_Order.thy. This theory instantiates the order type
class for lists like this:
definition "(xs::'a list) <= ys == prefixeq xs ys"
definition "(xs::'a list) < ys == xs <= ys & Not (ys <= xs)"
It then goes on to lift theorems about the constants 'prefixeq' and
'prefix' to the constants 'op <=' and 'op <', adding simp/intro/elim
attributes in the process. However, a few things seem to have gone
wrong here. First off, we have:
lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def]
lemmas strict_prefixI [intro?] = prefixI [folded less_list_def]
The first line hides the fact Sublist.prefixI, so the theorem declared
in the second line is just a duplicate of the one in the first and the
'folded less_list_def' attribute is applied in vain.
However, even when using the fully qualified fact Sublist.prefixI, it
doesn't work the way I assume it was intended to, since 'op <' is not
defined in terms of 'prefix', so the 'folded less_list_def' attribute
still doesn't apply.
Attached are my attempts at fixing these and a few other issues.
Please let me know if I should have posted this on the developer
mailing list.
Cheers,
Julian
Prefix_Order.patch
Email Gateway (Aug 19 2022 at 16:21):From: Christian Sternagel <c.sternagel@gmail.com>
A very quick look into the mercurial history indicates that I might have
caused this.
Unfortunately I won't have time until Wednesday to have a closer look,
sorry.
cheers
chris
Last updated: Apr 19 2024 at 12:27 UTC