Re: [isabelle] Theory Prefix_Order
A very quick look into the mercurial history indicates that I might have
Unfortunately I won't have time until Wednesday to have a closer look,
On 10/20/2014 05:00 PM, Julian Brunner wrote:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and