Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Generating fresh type variables

view this post on Zulip Email Gateway (Aug 18 2022 at 17:52):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Hello all,

I'm basically new to the ML part of Isabelle.

I'm defining a ML function to automatically generate specifications of an
Isabelle function (these specifications are given as argument to
Function_Fun.add_fun). During the generation, I obtain terms containing
schematic type variables. I need to constrain (with sorts) the types appearing
in these specifications, and I also transform the schematic type variables to
type variables (I think I have to).

However when I use this function in a locale, my generated type variables can
be the same as the locale's one (and a type capture occurs) which certainly
means I'm doing something wrong. What is the correct way to generate fresh
type variables (TFree) ?

I've searched through the Isabelle Cookbook and the sources
(Pure/{type.ML,term.ML,Isar/local}) without any real clue. Have I to collect
type variables of current locale fixed terms and use Name.variant ?

Thanks,

Mathieu

view this post on Zulip Email Gateway (Aug 18 2022 at 17:52):

From: Sascha Boehme <boehmes@in.tum.de>
Hi Mathieu,

Concerning fresh names relative to a context have a look at the Isar
implementation manual in Chapter 5, Section 1 (Variables), especially
Variable.variant_fixes. For more details, look into
~~/src/Pure/variable.ML.

Cheers,
Sascha

Mathieu Giorgino wrote:

view this post on Zulip Email Gateway (Aug 18 2022 at 17:52):

From: Christian Urban <urbanc@in.tum.de>
Hi Mathieu,

There is also the related function Variable.variant_frees,
which is explained in the Cookbook on page 16 with a
small example about generating fresh names for Frees. ;o)

Hope this helps,
Christian

Sascha Boehme writes:

Hi Mathieu,

Concerning fresh names relative to a context have a look at the Isar
implementation manual in Chapter 5, Section 1 (Variables), especially
Variable.variant_fixes. For more details, look into
~~/src/Pure/variable.ML.

Cheers,
Sascha

Mathieu Giorgino wrote:

Hello all,

I'm basically new to the ML part of Isabelle.

I'm defining a ML function to automatically generate specifications of an
Isabelle function (these specifications are given as argument to
Function_Fun.add_fun). During the generation, I obtain terms containing
schematic type variables. I need to constrain (with sorts) the types appearing
in these specifications, and I also transform the schematic type variables to
type variables (I think I have to).

However when I use this function in a locale, my generated type variables can
be the same as the locale's one (and a type capture occurs) which certainly
means I'm doing something wrong. What is the correct way to generate fresh
type variables (TFree) ?

I've searched through the Isabelle Cookbook and the sources
(Pure/{type.ML,term.ML,Isar/local}) without any real clue. Have I to collect
type variables of current locale fixed terms and use Name.variant ?

Thanks,

Mathieu

view this post on Zulip Email Gateway (Aug 18 2022 at 17:52):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Thanks Sascha and Christian,

I used "Variable.variant_fixes" and it worked great.

I had already used "Variable.variant_frees" for terms, but I hadn't realized
it can also be used for types. If I understand correctly, type variables and
term variables are in the same namespace (implicitly separated by the prefix
"'") ?

By the way, thanks for the Isabelle Cookbook, it's really helpful to start
with Isabelle/ML.

Mathieu

view this post on Zulip Email Gateway (Aug 18 2022 at 17:52):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Thanks Sascha and Christian,

I used "Variable.variant_fixes" and it worked great.

I had already used "Variable.variant_frees" for terms, but I hadn't realized
it can also be used for types. If I understand correctly, type variables and
term variables are in the same namespace (implicitly separated by the prefix
"'") ?

By the way, thanks for the Isabelle Cookbook, it's really helpful to start
with Isabelle/ML.

Mathieu

view this post on Zulip Email Gateway (Aug 18 2022 at 17:52):

From: Makarius <makarius@sketis.net>
On Wed, 29 Jun 2011, Mathieu Giorgino wrote:

Thanks Sascha and Christian,

I used "Variable.variant_fixes" and it worked great.

I had already used "Variable.variant_frees" for terms, but I hadn't
realized it can also be used for types. If I understand correctly, type
variables and term variables are in the same namespace (implicitly
separated by the prefix "'") ?

No you should not do that. Term variables and type variables are
different things. You probably mean Variable.invent_types, or even the
import operations that will put things into context without manual
fiddling.

By the way, thanks for the Isabelle Cookbook, it's really helpful to
start with Isabelle/ML.

It is certainly helpful, but you always need to cross-check with other
sources of information. Many fine points in the cookbook are not exactly
right.

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 17:52):

From: Makarius <makarius@sketis.net>
On Wed, 29 Jun 2011, Mathieu Giorgino wrote:

Thanks Sascha and Christian,

I used "Variable.variant_fixes" and it worked great.

I had already used "Variable.variant_frees" for terms, but I hadn't
realized it can also be used for types. If I understand correctly, type
variables and term variables are in the same namespace (implicitly
separated by the prefix "'") ?

No you should not do that. Term variables and type variables are
different things. You probably mean Variable.invent_types, or even the
import operations that will put things into context without manual
fiddling.

By the way, thanks for the Isabelle Cookbook, it's really helpful to
start with Isabelle/ML.

It is certainly helpful, but you always need to cross-check with other
sources of information. Many fine points in the cookbook are not exactly
right.

Makarius

Last updated: Apr 26 2024 at 08:19 UTC