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



Dear Aaron,

> 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"

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






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