*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] fixrec’s demand for continuity proofs*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Thu, 02 Sep 2010 16:14:12 +0200*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Hi again, I have more questions about HOL/CF, especially about the fixrec package: Consider again the function from my last example: f b = {b} ∪ f b I have this working definition: ______________________________________________________ fixrec f :: "int discr → (int ⇒ one)" where "f⋅b = (f⋅b) (undiscr b := ONE)" ______________________________________________________ but I do not like how I have to use undiscr here (especially as in my real example, the argument is more complex). Shouldn’t fixrec be able to define the function having the type "int ⇒ (int ⇒ one)"? Based on my understanding, this type is also a pcpo and therefore the operator based on the recursive definition with type "(int ⇒ (int ⇒ one)) → (int ⇒ (int ⇒ one))" can be used to define f. Unfortunately, this does not work: ______________________________________________________ fixrec f :: "int ⇒ int ⇒ one" where "f b = (f b) (b := ONE)" ______________________________________________________ gives me *** fixrec definition error: *** unknown term *** At command "fixrec". while ______________________________________________________ fixrec f :: "int ⇒ int ⇒ one" where "f = (λb. (f b) (b := ONE))" ______________________________________________________ gives *** Continuity proof failed; please check that cont2cont rules *** or simp rules are configured for all non-HOLCF constants. *** The error occurred for the goal statement: *** cont (λf b. (f b)(b := ONE)) *** At command "fixrec". I’m also wondering why this works ______________________________________________________ fixrec g :: "(int×int) discr → ((int×int) ⇒ one)" where "g⋅b = (case undiscr b of t ⇒ (g⋅(Discr t)) (t := ONE))" ______________________________________________________ but this does not: ______________________________________________________ fixrec g :: "(int×int) discr → ((int×int) ⇒ one)" where "g⋅b = (case undiscr b of (a,c) ⇒ (g⋅(Discr (a,c))) ((a,c) := ONE))" ______________________________________________________ *** Continuity proof failed; please check that cont2cont rules *** or simp rules are configured for all non-HOLCF constants. *** The error occurred for the goal statement: *** cont (λg. Λ a. case undiscr a of (a, c) ⇒ (g⋅(Discr (a, c)))((a, c) := ONE)) *** At command "fixrec". Is all this a limitation of fixrec, or a limitation in my understanding it? :-) Thank in advance for your help, Joachim -- Joachim Breitner e-Mail: mail at joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata at joachim-breitner.de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Joachim Breitner

**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Peter Gammie

- Previous by Date: Re: [isabelle] introduction rule for order bounded quantifiers.
- Next by Date: Re: [isabelle] fixrec’s demand for continuity proofs
- Previous by Thread: [isabelle] Post-Doc and PhD positions - Semantics of Real-World Computer Systems
- Next by Thread: Re: [isabelle] fixrec’s demand for continuity proofs
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list