Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Selector value with the value command

view this post on Zulip Email Gateway (Apr 27 2025 at 19:31):

From: Pasquale Noce <pasquale.noce.lavoro@gmail.com>
Dear Isabelle users,

The following code listing:

datatype test = Test (num: nat)
value "num (Test n)"

results in the following actual output of the value command:

"num (Test n)"
:: "nat"

instead of the output that I was expecting, namely:

"n"
:: "nat"

What am I missing here to make the value command compute this selector value?
Thank you very much, best regards,
Pasquale Noce

view this post on Zulip Email Gateway (Apr 27 2025 at 22:45):

From: Manuel Eberl <manuel@pruvisto.org>
In Isabelle 2025, importing only HOL.Main, I get "n", which is what you
want.

But generally speaking, the "value" command's behaviour is sometimes a
bit weird when free variables are involved. By default, "value" uses the
code generator. When free variables are involved, this is not possible,
and it instead relies on either "normalisation by evaluation" or using
the simplifier. That sometimes leads odd-looking output, e.g. value "n +
3" gives "n + (1 + 1 + 1)".

So, tl;dr ideally only use "value" on terms without free variables.

Manuel

On 27/04/2025 21:31, Pasquale Noce wrote:

Dear Isabelle users,

The following code listing:

datatype test = Test (num: nat)
value "num (Test n)"

results in the following actual output of the value command:

"num (Test n)"
:: "nat"

instead of the output that I was expecting, namely:

"n"
:: "nat"

What am I missing here to make the value command compute this selector value?
Thank you very much, best regards,
Pasquale Noce

view this post on Zulip Email Gateway (Apr 28 2025 at 10:43):

From: Pasquale Noce <pasquale.noce.lavoro@gmail.com>
Dear Manuel,

Thanks a lot for your kind feedback.
Actually, your answer that you got the expected output by importing Main made
me suspect that I overlooked some relevant piece of information in my previous
message, since I had imported Main in my example as well. So, I found out that
the overlooked piece of information was that the unexpected outcome is
obtained if my code listing is placed inside a locale. That is to say, the
code listing:

datatype test = Test (num: nat)
value "num (Test n)"

placed in the global context, generates the expected output, namely:

"n"
:: "nat"

On the contrary, the code listing:

locale temp
begin

datatype test = Test (num: nat)
value "num (Test n)"

end

generates the unexpected output, namely:

"num (Test n)"
:: "nat"

Hence, my former, incomplete question can be reformulated as follows: how can
I get the expected output within a locale?
Thank you very much, best regards,
Pasquale

view this post on Zulip Email Gateway (Apr 28 2025 at 11:34):

From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear Pasquale,

as far as I know, everything that is defined inside a locale does not have automatic
code generation. So, in particular if you define a function foo inside a locale bar,
you will need to declare

declare bar.foo.simps[code]

outside the locale, and similarly, you have to do this for definitions, partial_functions, etc.

I imagine, that the situation is the same for datatypes.
Perhaps in your case

declare locale_name.test.simps[code]

will suffice, but I’m not sure.

Best,
René

Am 28.04.2025 um 12:42 schrieb Pasquale Noce <pasquale.noce.lavoro@gmail.com>:

Dear Manuel,

Thanks a lot for your kind feedback.
Actually, your answer that you got the expected output by importing Main made
me suspect that I overlooked some relevant piece of information in my previous
message, since I had imported Main in my example as well. So, I found out that
the overlooked piece of information was that the unexpected outcome is
obtained if my code listing is placed inside a locale. That is to say, the
code listing:

datatype test = Test (num: nat)
value "num (Test n)"

placed in the global context, generates the expected output, namely:

"n"
:: "nat"

On the contrary, the code listing:

locale temp
begin

datatype test = Test (num: nat)
value "num (Test n)"

end

generates the unexpected output, namely:

"num (Test n)"
:: "nat"

Hence, my former, incomplete question can be reformulated as follows: how can
I get the expected output within a locale?
Thank you very much, best regards,
Pasquale

view this post on Zulip Email Gateway (Apr 28 2025 at 19:24):

From: Pasquale Noce <pasquale.noce.lavoro@gmail.com>
Dear René,

Thanks a lot for your kind feedback, too.
Based on it, I have finally found out that the following code listing (which I am posting here in case it may be useful to other Isabelle users as well):

locale sketch
begin

datatype test = Test nat

primrec test_num :: "test => nat" where
"test_num (Test n) = n"

end

code_datatype sketch.Test

declare sketch.test_num.simps [code]

value "sketch.test_num (sketch.Test n)"

triggers the generation of the expected output on the part of the value command, namely:

"n"
:: "nat"

Many thanks again to both you and Manuel.
Best regards,
Pasquale

Il 28/04/2025 13:21, Thiemann, René ha scritto:

Dear Pasquale,

as far as I know, everything that is defined inside a locale does not have automatic
code generation. So, in particular if you define a function foo inside a locale bar,
you will need to declare

declare bar.foo.simps[code]

outside the locale, and similarly, you have to do this for definitions, partial_functions, etc.

I imagine, that the situation is the same for datatypes.
Perhaps in your case

declare locale_name.test.simps[code]

will suffice, but I’m not sure.

Best,
René

Am 28.04.2025 um 12:42 schrieb Pasquale Noce <pasquale.noce.lavoro@gmail.com>:

Dear Manuel,

Thanks a lot for your kind feedback.
Actually, your answer that you got the expected output by importing Main made
me suspect that I overlooked some relevant piece of information in my previous
message, since I had imported Main in my example as well. So, I found out that
the overlooked piece of information was that the unexpected outcome is
obtained if my code listing is placed inside a locale. That is to say, the
code listing:

datatype test = Test (num: nat)
value "num (Test n)"

placed in the global context, generates the expected output, namely:

"n"
:: "nat"

On the contrary, the code listing:

locale temp
begin

datatype test = Test (num: nat)
value "num (Test n)"

end

generates the unexpected output, namely:

"num (Test n)"
:: "nat"

Hence, my former, incomplete question can be reformulated as follows: how can
I get the expected output within a locale?
Thank you very much, best regards,
Pasquale

view this post on Zulip Email Gateway (Apr 28 2025 at 19:25):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
(This should have also gone to the list)

-------- Weitergeleitete Nachricht --------
Betreff: Re: [isabelle] Selector value with the value command
Datum: Mon, 28 Apr 2025 20:25:44 +0200
Von: Florian Haftmann <florian.haftmann@cit.tum.de>
An: Pasquale Noce <pasquale.noce.lavoro@gmail.com>

Hi Pasquale,

note that there is no concept of »localized« code generation.

You always get proper behavior after interpretation:

locale triv
begin

datatype test = Test (num: nat)

end

interpretation I: triv .

value ‹I.num (I.Test n)›

How to proceed from here depends significantly on what you want to
achieve in the first place.

Cheers,
Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

view this post on Zulip Email Gateway (Apr 28 2025 at 19:29):

From: Pasquale Noce <pasquale.noce.lavoro@gmail.com>
Dear Florian,

Thanks a lot for your feedback, too.
Best regards,
Pasquale

view this post on Zulip Email Gateway (May 06 2025 at 07:23):

From: Tobias Nipkow <nipkow@in.tum.de>

On 27/04/2025 22:53, Manuel Eberl wrote:

In Isabelle 2025, importing only HOL.Main, I get "n", which is what you want.

But generally speaking, the "value" command's behaviour is sometimes a bit weird
when free variables are involved. By default, "value" uses the code generator.
When free variables are involved, this is not possible, and it instead relies on
either "normalisation by evaluation" or using the simplifier. That sometimes
leads odd-looking output, e.g. value "n + 3" gives "n + (1 + 1 + 1)".

So, tl;dr ideally only use "value" on terms without free variables.

Otherwise expect the unexpected ;-)

Tobias

Manuel

On 27/04/2025 21:31, Pasquale Noce wrote:

Dear Isabelle users,

The following code listing:

datatype test = Test (num: nat)
value "num (Test n)"

results in the following actual output of the value command:

"num (Test n)"
   :: "nat"

instead of the output that I was expecting, namely:

"n"
   :: "nat"

What am I missing here to make the value command compute this selector value?
Thank you very much, best regards,
Pasquale Noce

smime.p7s

Last updated: May 06 2025 at 08:28 UTC