Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Bool cpo

Email Gateway (Aug 22 2022 at 11:34):

From: "Roger H." <s57076@hotmail.com>
Hello,
to make set a cpo, its sufficient to make bool a cpo.
If one defines the "⊑" operator as the "⊆" operator on booleans, one obtains a partial order.
instantiation bool :: pobegin definition less_bool_def: "(op ⊑) = (op ⊆)"instanceby (intro_classes, unfold less_bool_def, safe)end
This induces an order on sets, which corresponds to the "⊆" operator.
lemma less_set_eq: "(op ⊑) = (op ⊆)"
But this lemma is not accepted by giving this error message:
---Type unification failed: No type arity set :: below---
Can you help me?
Many thanks!

Email Gateway (Aug 22 2022 at 11:35):

From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Roger,

bool and set are already ccpos:

instance bool :: ccpo .. -- "this proof is actually empty"
instance set :: (type) ccpo .. -- "this proof is actually empty"

Also, your example is strange:

definition less_bool_def: "(op ⊑) = (op ⊆)"

can not work, as ⊆ is specific for set, you need to use <=.
Also where do you get ⊑ from?

- Johannes

Email Gateway (Aug 22 2022 at 11:36):

From: "Roger H." <s57076@hotmail.com>
Correction:
to make set a cpo, its sufficient to make bool a cpo.
If one defines the "⊑" operator as the "-->" operator on booleans, one obtains a partial order.
instantiation bool :: pobegin definition less_bool_def: "(op ⊑) = (op -->)"instanceby (intro_classes, unfold less_bool_def, safe)end

This induces an order on sets, which corresponds to the "⊆" operator.

lemma less_set_eq: "(op ⊑) = (op ⊆)"

But this lemma is not accepted by giving this error message:
---Type unification failed: No type arity set :: below---

Can you help me?

By the way, i am aware of this answer of a similiar question:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-September/msg00010.html

Many thanks!

Email Gateway (Aug 22 2022 at 11:36):

From: "Roger H." <s57076@hotmail.com>
Hello Johannes

my exact question is:
While working in HOLCF(not HOL)...if I copy-paste the following class SetPcpo
http://isabelle.in.tum.de/website-Isabelle2008/dist/library/HOLCF/SetPcpo.html
in the HOLCF folder,
and run it, then I get at the following spot
lemma less_set_eq: "(op ⊑) = (op ⊆)"the following error: --Type unification failed: No type arity set :: below

Type error in application: incompatible operand type

Operator: op = op ⊑ :: (??'a ⇒ ??'a ⇒ bool) ⇒ bool
Operand: op ⊆ :: ??'b set ⇒ ??'b set ⇒ bool--1. Why is the error?

2. How do i prove here "instance bool :: cpo" //notice that this is the class cpo of holcf, as in [Huf 11], and not --hol ccpo-- 3. How do i then prove "instance set :: (type) cpo"
   Thank you!

Email Gateway (Aug 22 2022 at 11:36):

From: "Roger H." <s57076@hotmail.com>
Hello, thank you for your help, it was sucessfully proven and this issue is closed.

Last updated: Nov 21 2024 at 12:39 UTC