*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] sets in HOL/CF*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Thu, 02 Sep 2010 11:49:27 +0200*Sender*: Joachim Breitner <msg at joachim-breitner.de>

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**

**Follow-Ups**:**Re: [isabelle] sets in HOL/CF***From:*Brian Huffman

- Previous by Date: [isabelle] Unifying existentially quantified function
- Next by Date: [isabelle] introduction rule for order bounded quantifiers.
- Previous by Thread: [isabelle] Unifying existentially quantified function
- Next by Thread: Re: [isabelle] sets in HOL/CF
- 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