# [isabelle] Lazy Lists

Dear all,

`just for fun, I recently wanted to formalize the first "pearl" from the
``book "Pearls of Functional Algorithm Design" (by Richard Bird) inside
``Isabelle/HOL. The solutions in the book are implemented in Haskell and
``sometimes rely on lazy evaluation.
`

`I stumbled across the following points. In proofs the case of infinite
``lists is (as far as I read) never considered (i.e., plain structural
``induction on finite lists is used). However, the implementations
``sometimes contain infinite lists like [0..]. Since this "omissions" are
``only done in contexts where the lists that are used for induction are
``really finite, this seems to be fine.
`

`My question is now, how closely can such a kind of proof be imitated
``inside Isabelle/HOL?
`

`Lets consider we use "'a llist" (from AFP/Coinductive) for lazy lists
``and "'a list" for finite lists.
`

`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. The current
``documentation of the transfer package is rather inaccessible (in fact I
``only know of the example theories that are mentioned in the NEWS file).
`

`Another issue is that Haskell functions (on lazy lists) are defined
``using notation like "fun" of Isabelle/HOL despite not being based on
``well-founded recursion, whereas for function definitions on "'a llist"
``in Isabelle/HOL this does not work (at least I don't know how). That is,
``there is a gap between what is used in Haskell programming and how this
``can be "simulated" in Isabelle/HOL.
`
So, here is a wish-list:
- in contexts where we have "lfinite", reuse facts on "'a list" functions

`- provide a command that allows to define functions on "'a llist" using
``the same notation as "fun" (is this already possible?)
``- for Haskell code generation Nil and LNil as well as Cons and LCons
``should be unified and mapped to [] and (:) of Haskell
``- moreover, would it be possible to unify "equivalent" (modulo
``infiniteness) functions like "map" and "lmap", "filter" and "lfilter"
``..., for code generation?
`
My main questions are:
1) how would the above mentioned transfer setup work?
2) how realistic is the above wish-list and what do you think about it?
cheers
chris

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