Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Dealing with Int and Nat at the same time


view this post on Zulip Email Gateway (Aug 19 2022 at 08:35):

From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Dear Isabelle Users:

I was wondering what the best, most convenient way to deal with
numbers would be. Specifically, I have a datatype that I want
to be something like 'a mytype, where 'a should usually be either
an int or a nat or some other sort of number. Inside this type
will be a list of 'a list. I then want to have another function
that has the type of "'a mytype => 'a list" that will generate
lists containing all zeros. I am not really sure what the best
way to do this is, because Isabelle complains to me about the 0
not matching the type, since Isabelle doesn't know that I only
want 'a to be numbers. Is there some good way to do this"

Yours truly,

Aaron W. Hsu

view this post on Zulip Email Gateway (Aug 19 2022 at 08:44):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Dear Aaron,

Isabelle has a mechanism called "type classes" (or "sorts") to restrict the range of a type variable like 'a. "0" is defined in the "zero" type class, "1" in "one", and arbitrary numerals in "numeral". For example:

datatype 'a mytype = MyType "'a list"

fun only_zeros :: "'a mytype => ('b::zero) list" where
"only_zeros (MyType ns) = map (%x. (0::'b::zero)) ns"

value "only_zeros (MyType [1, 2, 3])"

Notice the syntax: "::" attaches a type class constraint to a type variable in a similar way that it attaches a type to a term; in fact, in "0::'b::zero", both uses of "::" are present.

If you need both zeros and ones, you can use "'b::{zero,one}". See the Isabelle tutorial, section 8.3, for details:

http://isabelle.in.tum.de/dist/Isabelle2012/doc/tutorial.pdf

Regards,

Jasmin


Last updated: Mar 28 2024 at 12:29 UTC