Email Gateway (Aug 18 2022 at 15:56): Email Gateway (Aug 18 2022 at 15:56):From: Brian Huffman <brianh@cs.pdx.edu>
On Thu, Sep 2, 2010 at 2:49 AM, Joachim Breitner
<mail@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,
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
Email Gateway (Aug 18 2022 at 16:00):From: Alexander Krauss <krauss@in.tum.de>
Brian Huffman wrote:
A related remark: A recursive function that returns a set can also be
defined using the inductive(_set) package. You have to rephrase the
definition using introduction rules, and manually derive the recursive
equations afterwards, but that is usually straightforward.
Alex
Email Gateway (Aug 18 2022 at 16:01):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Actually, Lukas's newly introduced "inductive_simps" command makes it easier than ever to derive recursive equations from inductive definitions. I think it's in Isabelle2009-2. I'm not aware of any documentation (beyond a few uses in Isabelle theories, which you can grep for) but it works pretty much like "inductive_cases".
Jasmin
Email Gateway (Aug 18 2022 at 16:03):From: Joachim Breitner <mail@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
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC