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.