peteg's blog - hacking - isabelle - 2008 03 02 WorkerWrapper

Andy Gill & Graham Hutton's Worker/Wrapper in HOLCF, partially.

/hacking/isabelle | Link

It's about time I pushed this out the door. Their proofs went through fine for the most part, except for the need to do some induction when rewriting the recursive calls. It is unclear to me how to prove the lemma that justifies this step in general, though for each instance the induction is quite straightfoward, and the key lemmas for the inductive steps are given in the paper. In effect we need induction just to convince HOLCF, not an optimisation phase, but it would be nice if their fusion rule handled this for me. (My proposed, unproven variant can be found in worker_wrapper.thy.)

I believe there was a small strictness bug in their streams / memoisation example. Score one to HOLCF.

I also tried to mechanise Andy Gill's nub example, which mostly went OK, modulo proving some auxiliary lemmas. Specifically, as above one needs to use induction to rewrite the recursive call, and coming out with the right statements is made difficult by HOLCF's admissibility requirements. A work in progress. Again, I can feel Larry Paulson laughing at me for wasting my time.

You can look at it here, or utter:

darcs get

Note some proofs are quite rough, though most of the important stuff is as clear as Isar. The Nat theory may end up being interesting, though with too much more monadic machinery one may as well use HOL... and I have begun to realise that proof-reuse for even something as simple as lists is quite difficult. There are at least two mainstream types (fully lazy and fully strict), as well as some in-betweens that might be convenient (e.g. head-strict and tail-strict). The code here just begins down the mainstream-Haskell path; I figure the Standard ML people are wise enough to be using HOL or Coq or whatever in the first place.