# Re: [isabelle] Antwort: Coinductive_List and LList/LFilter

Hi Jens,
> Wow, the theory covers 27 DIN A4 pages. Is there a way of
> decomposition and plausification of the proof/theorems?

`these theories are not mine. Larry Paulson wrote LFilter and Stephan
``Merz LList2. I merely ported them such that they now use
``Coinductive_List from HOL/Library instead of Induct/LList.
`
LFilter simply defines the filter functional for lazy lists.
A rough outline of LList2 is:
1. Lazy lists over an alphabet

`There are various sets: "alllsts A" are all lists with elements from A,
``"finlsts A" are only the finite lazy lists with elements from A.
``"inflsts A" are the infinite ones, "fpslsts A" are non-empty, finite
``llists, "poslsts A" are all non-empty llists.
``Most lemmas in LList2 deal with these sets and how some functions on
``lists behave w.r.t. these sets.
`
2. The recursion operator finlsts_rec for finite llists.
3. Some functions for llists:

`- ll2f somewhat models nth for llist, but returns an option: None if the
``index exceeds the list.
`- ltake, ldrop, lset are their list-counterpart for llists
- llength, llast, lrev, lbutlast, llast are defined for finite llists
- lconst (the infinite list where all elements are the same)
4. The prefix order on llist.
5. The set of all prefixes / suffixes / infinite suffixes of a list
6. Some safety and liveliness properties

`For 2. to 6., numerous lemmas are proved about the various notions for
``different combinations of the above types of llists over alphabets.
``What Stephan Merz used these theories for, I do not know. Neither am I
``sure that being focused on the various kinds of lazy lists over some
``alphabet is the best way to work with lazy lists. Moreover, one might
``question some design decisions (like ll2f returning an option, llength
``being only defined for finite llists).
`
Andreas

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