Re: [isabelle] Lazy Lists



On Mon, Jun 25, 2012 at 8:43 AM, Andreas Lochbihler
<andreas.lochbihler at kit.edu> wrote:
>> If I'm correct, the new transfer package should be able (after appropriate
>> setup) to transfer facts from "'a list" to "'a llist" with additional
>> "lfinite
>> ..." assumptions (and also the other way round?). But how this setup is
>> actually
>> done, I did not find out.
>
> I tried to set it up in the attached theory, but it only seems to works in
> the wrong direction: You can prove theorems on 'a list by transferring them
> to 'a llist with the lfinite predicate. Since neither 'a llist nor 'a list
> are defined in terms of each other, you need to do the setup manually, i.e.,
> prove all those transfer rules that relate functions on 'a llist with those
> on 'a list. Maybe the transfer package experts can improve my attempt.

That's right: The automation provided by the setup_lifting command is
designed for transferring theorems from supertype to subtype, not the
other way around. But you can always define your own transfer relation
manually, in whichever direction you want. The attached theory file
defines a relation for transferring from list to llist (it is the
converse of the relation that would be generated by setup_lifting),
and shows how it can be used.

Using the "transfer" proof method (which acts like the "descending"
method from the Quotient package) is rather cumbersome for these kinds
of examples; once we get around to implementing counterparts to the
"lifting" method and "lifted" attribute, transferring theorems from
list to llist should be a lot easier.


>> So, here is a wish-list:
>> - in contexts where we have "lfinite", reuse facts on "'a list" functions

Using the planned but yet-to-be-implemented "transferred" attribute,
this kind of transfer should be completely automatic. You should be
able to write

map_append [transferred tr_llist]

and get the theorem

"lfinite xs ==> lfinite ys ==> lmap f (lappend xs ys) = lappend (lmap
f xs) (lmap f ys)"

(assuming that the transfer rules are set up as in the attached theory file).

This feature will definitely be available before the next Isabelle release.

- Brian

Attachment: List_LList.thy
Description: Binary data



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