Re: [isabelle] Theory Prefix_Order

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.



On 10/20/2014 05:00 PM, Julian Brunner wrote:
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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.