[isabelle] Lazy Lists
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
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and