Re: [isabelle] fixrec’s demand for continuity proofs


Just a quick response, as it is late here. I'd suggest you read more background material before trying to prove anything. In particular, the original HOLCF paper is great, and there are some theories in the AFP that illustrate how to use HOLCF - Brian Huffman's stream fusion one is very well presented, and I hacked some things together in my worker/wrapper entry. There you will find a theory for the natural numbers that handles some of these issues.

I'd be very wary about mixing the continuous (HOLCF) and total (HOL) function spaces. It does work if you obey the design principles spelt out in the original paper.

Start with easy stuff - reasoning about lists defined using 'domain', e.g. The naturals, unless defined as a domain, are already fiddly. Sets are a long way from obvious, probably leading you to power domains if you have a non-trivial recursive definition.

Take a look at the examples in the HOLCF directory of the Isabelle distribution too.

It might help to switch on "Show sorts" in proof general and remember that if a type isn't annotated with pcpo (etc) then HOLCF doesn't know much about it.



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