Re: [isabelle] sets in HOL/CF



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





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