Some of Jeremy Gibbons & Graham Hutton's Proof Methods for Corecursive Programs in HOLCF.
Mon, Mar 03, 2008./hacking/isabelle | LinkI abandoned this attempt at mechanising a proof of the "approx lemma" about eighteen months ago, for what now seem like spurious reasons; what I had was quite close to what was needed. I was initially interested in the "take lemma" made famous by Richard Bird & Philip Wadler, and how it took the magic step from assertions about finite lists to ones about possibly infinite objects. Well, I definitely feel some awareness of vacuity now.
You can read it here.
The magic is how the continuity underpinning the semantics of functions is reflected into the term language. As such it's unbelievably cute. The proof of correctness is not particularly interesting though, except perhaps as an exercise in fiddling with fixpoints and continuity.