[isabelle] sets in HOL/CF



Dear Isabelle community,

I am exploring HOLCF at the moment. As a starting point, I tried to
define this function with fixrec:
	f :: nat → nat set
        f b = {b} ∪ f b
I’d expect to find that "f b = {b}".

This approach worked:
______________________________________________________
fixrec f :: "int lift → (int ⇒ one)" where
  "f⋅b = (case b of ⊥ ⇒ ⊥ | Def a ⇒ (f⋅b) (a := ONE))"
declare f.simps[simp del]

lemma "f⋅(Def b) = (λ c. if b = c then ONE else ⊥)"
apply (rule ext)
apply auto
apply (subst f.unfold)
apply simp
apply(induct rule:f.induct)
apply auto
done
______________________________________________________

But I’m wondering: Why can I not write:
______________________________________________________
fixrec f :: "int lift → int set" where
  "f⋅b = (case b of ⊥ ⇒ ⊥ | Def a ⇒ {a} ∪ (f⋅b)"
declare f.simps[simp del]
______________________________________________________
The error message
*** Type unification failed: No type arity bool :: cpo
seems to indicate that fixrec has a problem with me using "int set" as a
pcpo. I assume the reason is that "int set" is just an abbreviation for
"int ⇒ bool", therefore my above work-around. But I’m missing the
convenient syntax of sets in Isabelle.

Is this really the correct way to work with sets in HOL/CF or am I just
overlooking something?

Thank you,
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.