Re: [isabelle] Lazy Lists in HOL



Thomas,

> I wanted to use the LazyList - theory of HOL (LList.thy) from Lawrence
> Paulson. Unfortunately I didn't find a theory containing the typical
> higher-order functions like filter, zip, etc for "'a llist". Furthermore I
> miss a predicate like is_finite for checking finiteness of a lazy list. Is
> there such an additional theory or do I have to define these functions
> myself?

Unfortunately, the theory of lazy lists is not so well developed, so you
have to define the concepts you need yourself.

You might also want to look at the "Lazy Lists II" theory in the Archive
of Formal Proofs (http://afp.sourceforge.net) by Stefan Friedrich, which
might contain some of the definitions you need.

> Maybe it is possible to use the definitions of SList.thy, does anybody know
> how?

No. Strict and lazy lists are different types, and there is no easy way
to lift definitions. You can of course take the "SList.thy" as a
guideline, but the definition principles on lazy lists are very
different (corecursion vs. recursion) and not automated very well at the
moment. Notably, you must use the "llist_corec" combinator, as in the
definitions of "lmap", "lappend" etc.

Should you decide to extend the available theories with more generally
useful definitions and theorems, your contribution is welcome of course...

Alex





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