Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Fixing type variables in locales

Email Gateway (Mar 02 2021 at 13:23):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hello!

I want to define a locale that (among other things) fixes a type 'a
and assumes that the type 'a is infinite but doesn’t fix any variables
with types that include 'a.

I can write the following:

locale l = assumes "infinite (UNIV :: 'a set)"

This results in the following output:

locale l
assumes "l TYPE('a)"
Additional type variable(s) in locale specification "l": 'a

Unfortunately, it seems that I cannot really make use of this type
variable later. Let’s say I add the following declaration to the locale
context:

type_synonym t = "'a ⇒ 'a"

This results in the following output, of which the “Extra variables”
part is an error message:

Ignoring sort constraints in type variables(s): "'a"
in type abbreviation "t"
Extra variables on rhs: "'a"
The error(s) above occurred in type abbreviation "t"

I can also try out the following declaration:

type_synonym 'a t = "'a ⇒ 'a"

However, this results in the following error message:

Locally fixed type arguments "'a" in type declaration "t"

How can I achieve what I want?

All the best,
Wolfgang

Email Gateway (Mar 02 2021 at 13:36):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear Wolfgang,

On Tue, Mar 2, 2021, 14:25 Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
wrote:

Hello!

I want to define a locale that (among other things) fixes a type 'a
and assumes that the type 'a is infinite but doesn’t fix any variables
with types that include 'a.

I can write the following:

locale l = assumes "infinite (UNIV :: 'a set)"

I think this assumption is fine. The problems below result from incorrect
usage of type_synonym. But that is not really related to the initial
question of fixing a type variable for some infinite type.

I don't think that type_synonym is localized (and I'm unsure whether it
could be made so). If that assumption is correct then type_synonym only
makes sense in a global context.

cheers

chris

This results in the following output:

locale l
assumes "l TYPE('a)"
Additional type variable(s) in locale specification "l": 'a

Unfortunately, it seems that I cannot really make use of this type
variable later. Let’s say I add the following declaration to the locale
context:

type_synonym t = "'a ⇒ 'a"

This results in the following output, of which the “Extra variables”
part is an error message:

Ignoring sort constraints in type variables(s): "'a"
in type abbreviation "t"
Extra variables on rhs: "'a"
The error(s) above occurred in type abbreviation "t"

I can also try out the following declaration:

type_synonym 'a t = "'a ⇒ 'a"

However, this results in the following error message:

Locally fixed type arguments "'a" in type declaration "t"

How can I achieve what I want?

All the best,
Wolfgang

Email Gateway (Mar 02 2021 at 14:00):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear Wolfgang,

you can get rid of the warning of the locale declaration by added some dummy argument that
fixes the type. For example,

locale l =
fixes ty :: "'a itself”
assumes "infinite (UNIV :: 'a set)”

as for the type_synonym problem, I think that Chris already hit the point.

Best,
René

Email Gateway (Mar 02 2021 at 14:34):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Ah, that makes sense. Thanks for this explanation.

Initially I thought that the impossibility of using type_synonym in
the way I wanted would pose a problem, but it seems that it can be
worked around. My solution is to leave the locale context immediately
after declaring the locale, declare the type synonym outside the locale
context, and add (in l) to every lemma that needs the infinity
constraint. This seems to work fine for me.

All the best,
Wolfgang

Email Gateway (Mar 03 2021 at 11:15):

From: Makarius <makarius@sketis.net>
Note that you can re-enter the locale context at any time, using

context l
begin

lemma ...

lemma ...

end

Makarius

Email Gateway (Mar 03 2021 at 14:14):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Yes, that’s possible too, and is actually what I used to do in such
situations. However, I discovered that in this particular formalization
I often don’t need the infinity constraint, so that it seemed even more
natural to me to use (in l) in the relevant places.

All the best,
Wolfgang

Last updated: Apr 18 2024 at 16:19 UTC