*To*: Joachim Breitner <mail at joachim-breitner.de>*Subject*: Re: [isabelle] sets in HOL/CF*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 2 Sep 2010 08:29:10 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1283420967.29045.6.camel@kirk>*References*: <1283420967.29045.6.camel@kirk>*Sender*: huffman.brian.c at gmail.com

On Thu, Sep 2, 2010 at 2:49 AM, Joachim Breitner <mail at joachim-breitner.de> wrote: > 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}". [...] > 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 Hi Joachim, If you want to be able to define a function of type "nat -> nat set" with fixrec, it turns out that fixrec can do it, but it requires you to do some work to set things up first. The first requirement is that the return type "nat set" needs to be in the pcpo class. As you pointed out, "nat set" is an abbreviation for "nat => bool", so this means you will need an instance bool :: pcpo. For \sqsubseteq to coincide with the subset relation on sets, you will need to define \sqsubseteq as implication on booleans. (I've pasted a copy of the necessary proof scripts at the end of this email.) The standard HOLCF library doesn't define this pcpo instance for type bool, because in many cases HOL types make more sense with a discrete ordering, and I didn't want to prevent users from defining bool as a discrete cpo. The bool :: pcpo instance might be a good thing to put in HOLCF/Library though, so users can import it if they want to. To write a continuous function type like "nat -> nat set", the argument type "nat" also needs to be in class cpo. The easiest way to do this is to define a discrete ordering on type nat, and prove an instance of the "discrete_cpo" class. It might be useful to put this definition in another theory in HOLCF/Library. The next requirement for fixrec is that it needs to be able to prove continuity. In this case the body of your function uses "union" and "insert", so you will need to prove continuity for those, at least. (Proofs below) If you'd like to see a theory in HOLCF/Library that configures HOLCF to work better with set types, I would welcome any suggestions that you may have. Hope this helps, - Brian --------------------------------------- instantiation bool :: finite_po begin definition "x \<sqsubseteq> y \<longleftrightarrow> (x \<longrightarrow> y)" instance by (default, unfold below_bool_def, fast+) end instance bool :: pcpo proof have "\<forall>y. False \<sqsubseteq> y" by (simp add: below_bool_def) thus "\<exists>x::bool. \<forall>y. x \<sqsubseteq> y" .. qed lemma bottom_eq_False: "\<bottom> = False" apply (rule below_antisym [OF minimal]) apply (simp add: below_bool_def) done lemma cont2cont_disj [simp, cont2cont]: assumes f: "cont (\<lambda>x. f x)" and g: "cont (\<lambda>x. g x)" shows "cont (\<lambda>x. f x \<or> g x)" apply (rule cont_apply [OF f]) apply (rule chfindom_monofun2cont) apply (rule monofunI, simp add: below_bool_def) apply (rule cont_compose [OF _ g]) apply (rule chfindom_monofun2cont) apply (rule monofunI, simp add: below_bool_def) done lemma cont2cont_Collect [simp, cont2cont]: assumes "\<And>y. cont (\<lambda>x. f x y)" shows "cont (\<lambda>x. {y. f x y})" unfolding Collect_def using assms by (rule cont2cont_lambda) lemma cont2cont_mem [simp, cont2cont]: assumes "cont (\<lambda>x. f x)" shows "cont (\<lambda>x. y \<in> f x)" unfolding mem_def using assms by (rule cont2cont_fun) lemma cont2cont_union [simp, cont2cont]: "cont (\<lambda>x. f x) \<Longrightarrow> cont (\<lambda>x. g x) \<Longrightarrow> cont (\<lambda>x. f x \<union> g x)" unfolding Un_def by simp lemma cont2cont_insert [simp, cont2cont]: assumes "cont (\<lambda>x. f x)" shows "cont (\<lambda>x. insert y (f x))" unfolding insert_def using assms by (intro cont2cont) instantiation nat :: discrete_cpo begin definition [simp]: "(x::nat) \<sqsubseteq> y \<longleftrightarrow> x = y" instance by default simp end fixrec f :: "nat \<rightarrow> nat set" where [simp del]: "f\<cdot>b = {b} \<union> f\<cdot>b" lemma "f\<cdot>b = {b}" apply (subst f.simps) apply (rule f.induct) apply (rule adm_eq, simp, simp) apply (simp add: subset_eq Ball_def mem_def bottom_eq_False) apply simp done

**Follow-Ups**:**Re: [isabelle] sets in HOL/CF***From:*Alexander Krauss

**References**:**[isabelle] sets in HOL/CF***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] fixrec’s demand for continuity proofs
- Next by Date: Re: [isabelle] fixrec’s demand for continuity proofs
- Previous by Thread: [isabelle] sets in HOL/CF
- 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