Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Canonical types of constants

Email Gateway (Aug 22 2022 at 12:52):

From: Tobias Nipkow <nipkow@in.tum.de>
In order to obtain the type of a constant c I am using this code snippet:

Proof_Context.read_const {proper = true, strict = false} ctxt c

It gives me back a term Const(c,T) and then I proceed with T. How can I make
sure that the type variables in T have canonical names 'a, 'b etc? Should I be
using some other piece of code?

The background is that in 7f5579b12b0a, constant "card" has type "?'b set =>
nat" instead of "?'a set => nat" as in the past. I assume that I should not rely
on canonicity of names in T? If not, how can I convert a type into a `canonical'
one?

Thanks
Tobias
smime.p7s

Email Gateway (Aug 22 2022 at 12:52):

From: Makarius <makarius@sketis.net>
On Tue, 9 Feb 2016, Tobias Nipkow wrote:

In order to obtain the type of a constant c I am using this code snippet:

Proof_Context.read_const {proper = true, strict = false} ctxt c

It gives me back a term Const(c,T) and then I proceed with T. How can I make
sure that the type variables in T have canonical names 'a, 'b etc? Should I
be using some other piece of code?

This correctly produces a type scheme for the constant, according to its
declaration. It uses schematic type variables, but these are considered
"private" to a declaration and not necessarily canonical in an application
context.

The proper way to make schematics visible in a context (and printable) can
be seen in the implementation of the document antiquotation @{const}:
Variable.import_terms.

Note that show_question_marks = false produces unreliable results:
pretending that schematic variables are not schematic is fragile.
LaTeXsugar.thy seems to suffer from that wrong assumption.

The background is that in 7f5579b12b0a, constant "card" has type "?'b
set => nat" instead of "?'a set => nat" as in the past.

The definition of "card" has changed here
http://isabelle.in.tum.de/repos/isabelle/rev/9f4f0dc7be2c and thus its
internal type declaration.

Here is an example that illustrates the situation and shows how to make
canonical types inside a given context:

consts a :: 'a
consts b :: 'b

ML ‹
fun read_const ctxt s =
let
val t = Proof_Context.read_const {proper = true, strict = false} ctxt s;
val ([t'], _) = Variable.import_terms true [t] ctxt;
in (t, t') end;

read_const @{context} "a";
read_const @{context} "b";
read_const @{context} "card";
›

Of course, the result depends on the context. E.g. within the context of
"context fixes x :: 'a begin" new types start at 'b.

Makarius

Email Gateway (Aug 22 2022 at 12:52):

From: Tobias Nipkow <nipkow@in.tum.de>
Thanks, that works fine.

Tobias
smime.p7s

Last updated: Apr 27 2024 at 04:17 UTC