[isabelle] fixrec’s demand for continuity proofs



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
Description: This is a digitally signed message part



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