Andy Gill & Graham Hutton's Worker/Wrapper in HOLCF, partially.
Sun, Mar 02, 2008./hacking/isabelle | LinkIt'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 https://peteg.org/isabelle/worker_wrapper/
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.