Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Type arity declaration in Isabelle

view this post on Zulip Email Gateway (Nov 07 2023 at 17:09):

From: Guilherme Silva <guilhermegfsilva@gmail.com>
Hello,

I'm wondering how to declare an arity for a new type that I've declared in
Isabelle. I've tried following the examples in these two documents:

Old Introduction to Isabelle:
https://isabelle.in.tum.de/dist/Isabelle2023/doc/intro.pdf (Section 11.2)

The Isabelle Reference Manual:
https://www.cl.cam.ac.uk/~lp15/papers/Reports/ref97.pdf (Section 6.1.2)

But Isabelle doesn't recognize the keyword "arities", so I can't proceed.
For context, I want to define a new type using typedecl and declare its
arity as being of sort "enum" and "equal" so I can export code using said
type without getting a "wellsortedness error".

Thanks,
Guilherme Silva

view this post on Zulip Email Gateway (Nov 07 2023 at 17:36):

From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hello,

there may be better ways (without using sorry), but at least the
following works:

typedecl x

instance x :: enum sorry

Of course, due to the sorry, you can also declare a type with impossible
sorts, e.g., instance x :: "{infinite,finite}" or similar.

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Nov 08 2023 at 10:20):

From: Makarius <makarius@sketis.net>
It is better to be honest about the axiomatization. E.g. see this example from
$ISABELLE_HOME/src/HOL/HOLCF/ex/Focus_ex.thy :

typedecl ('a, 'b) tc
axiomatization where tc_arity: "OFCLASS(('a::pcpo, 'b::pcpo) tc, pcop_class)"
instance tc :: (pcpo, pcpo) pcpo by (rule tc_arity)

Makarius

view this post on Zulip Email Gateway (Nov 08 2023 at 13:19):

From: Guilherme Silva <guilhermegfsilva@gmail.com>
Unfortunately, when trying to use these methods, I still get the following
error:

"No code equations for equal_x_inst.equal_x, enum_x_inst.enum_all_x,
enum_x_inst.enum_ex_x", etc.

How can I define the code equations I need?

Also, is there a way to define the arity of a type as belonging to multiple
classes (e.g. enum and equal) in just one axiom? If I try to use two
separate axioms, like as follows, they conflict with each other.

axiomatization where x_arity: "OFCLASS(x, enum_class)"
axiomatization where x_arity: "OFCLASS(x, equal_class)"

view this post on Zulip Email Gateway (Nov 08 2023 at 13:28):

From: Makarius <makarius@sketis.net>

Unfortunately, when trying to use these methods, I still get the following
error:

"No code equations for equal_x_inst.equal_x, enum_x_inst.enum_all_x,
enum_x_inst.enum_ex_x", etc.

How can I define the code equations I need?

Also, is there a way to define the arity of a type as belonging to multiple
classes (e.g. enum and equal) in just one axiom? If I try to use two separate
axioms, like as follows, they conflict with each other.

axiomatization where x_arity: "OFCLASS(x, enum_class)"
axiomatization where x_arity: "OFCLASS(x, equal_class)"

Now it becomes more clear what you actually had in mind. It is not about "type
arity declaration" (from many decades ago), but "type class instantiation".

If you make a hypersearch in Isabelle/jEdit over the directory
$ISABELLE_HOME/src and its subdirectories, file pattern *.thy and regexp
instantiation.*enum you will find some examples.

This will also provide more (con)text how things work in practice.

Makarius

Last updated: Apr 29 2024 at 01:08 UTC