[isabelle-dev] [isabelle] Theory Prefix_Order

[Julian Brunner]

Dear Christian,

Yes, I haven't considered AFP entries or anything, this was just my
personal hack to get it to work for my theories. I'll adjust the names
in my theories to whatever you see fit for Prefix_Order.

However, it seems like there is still an issue. The lemma
"strict_prefixI" gets unfolded from "prefixeq ?xs ?ys ⟹ ?xs ≠ ?ys ⟹
prefix ?xs ?ys" to "prefixeq ?xs ?ys ⟹ ?xs ≠ ?ys ⟹ ?xs < ?ys". My
guess is that it should be unfolded completely to "?xs ≤ ?ys ⟹ ?xs ≠
?ys ⟹ ?xs < ?ys". For this to happen, the attribute "folded
less_eq_list_def less_list_def" has to be used instead of just "folded
less_list_def". The lemma "strict_prefixE" behaves the same.

Cheers,
 Julian

On Tue, Oct 21, 2014 at 4:28 PM, Christian Sternagel
<c.sternagel at gmail.com> wrote:
> (moved from isabelle-users since I'm referring to the development versions
> of Isabelle and the AFP below)
>
> Dear Julian,
>
> unexpectedly I found some time to have a look earlier.
>
> First, the "naming layer" provided by the "lemmas" statements in
> Prefix_Order is there to keep compatibility with some AFP entries. (There
> are mainly two naming schemes around, either "Peq" "P" for weak and strict
> part of an order or "P" and "strict_P" for the same; and Sublist uses the
> former, while some AFP entries use the latter.)
>
> I think (without trying, however) your suggested changes would break some
> AFP entries.
>
> Instead I suggest the attached changes (the order of patches is to be found
> in "series") which are tested against
> Isabelle: 9239a33935c6 and
> AFP: 42be0138cfe5
>
> Thanks for spotting this.
>
> cheers
>
> chris
>
> 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.
>>
>> Cheers,
>>   Julian
>>
>