Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] translations and numerals

view this post on Zulip Email Gateway (Aug 19 2022 at 13:18):

From: Tobias Nipkow <nipkow@in.tum.de>
On 21/01/2014 15:18, Christian Sternagel wrote:

Well, what I wrote in my previous mail does not work for "int"s and "nat"s. The
following does

translations
"i" <= "CONST Fin (i::'a::numeral)"
"i" <= "CONST Fin (i::int)"

But this causes "Fin x" to be reduced to "x", no matter what "x" is, as long as
it is of type int. That's not what I want.

Tobias

"i" <= "CONST Fin (i::nat)"
"0" <= "CONST Fin (0::'a::zero)"
"1" <= "CONST Fin (1::'a::one)"

But I should mention that I have no clue why ;)... I was just doing trial and
error.

cheers

chris

On 01/21/2014 03:07 PM, Christian Sternagel wrote:

Dear Tobias,

how about (I used "datatype 'a fin = Fin 'a"),

translations
"_Numeral i" <= "CONST Fin (i::'a::numeral)"
"0" <= "CONST Fin (0::'a::zero)"
"1" <= "CONST Fin (1::'a::one)"

then for

term "(Fin 0, Fin 1, Fin 10, Fin x)"

I get

"(0, 1, 10, Fin x)"
:: "'a fin × 'b fin × 'c fin × 'd fin"

Note that when leaving of "zero" and "one I get "Fin 0" and "Fin 1" as
output.

On 01/21/2014 02:41 PM, Tobias Nipkow wrote:

I am using Library/Extended that defines a datatype with a unary
constructor
Fin. I want to print terms like "Fin 5" as "5" and am using the following
translations:

translations
"_Numeral i" <= "CONST Fin(_Numeral i)"
"0" <= "CONST Fin 0"
"1" <= "CONST Fin 1"

When I generate latex from

text{* @{term "Fin(5::int)"} *}

this works fine, I get "5".

But when I write

term "Fin(5::int)"

in a theory, the output is "Fin 5". Why is that? And what can I do to
obtain the
output "5" always, not just from an antiquotation in a text block.

Note that when I use this translation

translations
"x" <= "CONST Fin(x)"

then "Fin" disappears for good, but that is not what I want.

Thanks
Tobias

view this post on Zulip Email Gateway (Aug 19 2022 at 13:18):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Tobias,

here's just another data point. In Isabelle2013-2, your original translation works fine
with ProofGeneral 3.7.1.1, but not with jEdit. I haven't tried PG 4.x.

Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 13:18):

From: Tobias Nipkow <nipkow@in.tum.de>
Thank you, that explains why the translations worked for me when I wrote them -
I used PG then.

Tobias

view this post on Zulip Email Gateway (Aug 19 2022 at 13:18):

From: Makarius <makarius@sketis.net>
Printing is a black art, especially when using the AST representation of
'translations', which can contain additional annotations unexpectedly.

The configuration option syntax_ast_trace generally helps to see what
happens to happen in a particular situation, and it shows additional
constraints and markup in the rich document output of Isabelle/PIDE.

In other print modes, there can be different add-ons.

Instead of these fragile and complicated syntax translations, the usual
way to modify term output systematically is via the "uncheck" phase. It
has the advantage that it operates on regular type-correct lambda terms:
that requires a few more cases to cover (in Isabelle/ML), but there is no
black magic.

The included theory No_Fin demonstrates that. Note that I am using a
fully official constant no_Fin here, which is not printed in the end due
to its special notation.

Makarius
No_Fin.thy

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

From: Tobias Nipkow <nipkow@in.tum.de>
Works like a charm, thanks!

Tobias

view this post on Zulip Email Gateway (Aug 19 2022 at 13:34):

From: Tobias Nipkow <nipkow@in.tum.de>
I am using Library/Extended that defines a datatype with a unary constructor
Fin. I want to print terms like "Fin 5" as "5" and am using the following
translations:

translations
"_Numeral i" <= "CONST Fin(_Numeral i)"
"0" <= "CONST Fin 0"
"1" <= "CONST Fin 1"

When I generate latex from

text{* @{term "Fin(5::int)"} *}

this works fine, I get "5".

But when I write

term "Fin(5::int)"

in a theory, the output is "Fin 5". Why is that? And what can I do to obtain the
output "5" always, not just from an antiquotation in a text block.

Note that when I use this translation

translations
"x" <= "CONST Fin(x)"

then "Fin" disappears for good, but that is not what I want.

Thanks
Tobias

view this post on Zulip Email Gateway (Aug 19 2022 at 13:34):

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

how about (I used "datatype 'a fin = Fin 'a"),

translations
"_Numeral i" <= "CONST Fin (i::'a::numeral)"
"0" <= "CONST Fin (0::'a::zero)"
"1" <= "CONST Fin (1::'a::one)"

then for

term "(Fin 0, Fin 1, Fin 10, Fin x)"

I get

"(0, 1, 10, Fin x)"
:: "'a fin × 'b fin × 'c fin × 'd fin"

Note that when leaving of "zero" and "one I get "Fin 0" and "Fin 1" as
output.

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

From: Christian Sternagel <c.sternagel@gmail.com>
Well, what I wrote in my previous mail does not work for "int"s and
"nat"s. The following does

translations
"i" <= "CONST Fin (i::'a::numeral)"
"i" <= "CONST Fin (i::int)"
"i" <= "CONST Fin (i::nat)"
"0" <= "CONST Fin (0::'a::zero)"
"1" <= "CONST Fin (1::'a::one)"

But I should mention that I have no clue why ;)... I was just doing
trial and error.

cheers

chris

Last updated: Apr 26 2024 at 20:16 UTC