Re: [isabelle] Antwort: Coinductive_List and LList/LFilter
> 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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and