Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Nominal2 fails on Datatypes with Lists


view this post on Zulip Email Gateway (Aug 22 2022 at 20:45):

From: "Jackson, Vincent (Data61, Kensington NSW)" <Vincent.Jackson@data61.csiro.au>
Hello All,

I have been recently experimenting with Nominal2<https://www.isa-afp.org/entries/Nominal2.html>, but have run into a problem with lists in datatypes.

The datatype

nominal_datatype ty

= TRecord ‹ty list›

| TVar typevar

fails with

Proof failed.

  1. ⋀x. TRecord_raw (map (permute p_) (- p_ ∙ x)) = TRecord_raw x

The error(s) above occurred for the goal statement⌂:

p_ ∙ TRecord_raw = TRecord_raw

presumably because the automation does not know (or use) the fact that ‹map (permute p) xs = p ∙ xs›.
Further, although I can prove the lemma, I am unsure how (or if it is possible) to 'inject' the fact into the automation.

Any advice on how to proceed would be appreciated.

Thank you,
Vincent Jackson

view this post on Zulip Email Gateway (Aug 22 2022 at 20:45):

From: "Urban, Christian via Cl-isabelle-users" <cl-isabelle-users@lists.cam.ac.uk>
Dear Vincent,

I have to check what is going on. Would you be able top send me a slimmed-down theory where I can see what the problem is?

Also what is typevar in the TVar constructor?

Thanks,
Christian

view this post on Zulip Email Gateway (Aug 22 2022 at 20:45):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi, Christian!

Is Nominal2 somehow production-ready? From its website I got the
impression that it had been developed only half-way and then development
had halted.

All the best,
Wolfgang

view this post on Zulip Email Gateway (Aug 22 2022 at 20:45):

From: "Urban, Christian via Cl-isabelle-users" <cl-isabelle-users@lists.cam.ac.uk>
Hi Wolfgang,

Is Nominal2 somehow production-ready?

This depends on your point of view. ;o) It is certainly true that it quite rough and not all features are implemented. And it was aeons ago I have done things with it. But at the same time people have found it useful and have used it in interesting formalisations, for example

https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/

It really depends on what your point of view is and what you want to do.

Christian

view this post on Zulip Email Gateway (Aug 22 2022 at 20:46):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi, Christian!

So did I get this correctly that Nominal2 isn’t further developed
anymore?

By the way, is the restriction that values of a nominal data type may
not contain functions also in place in Nominal2?

All the best,
Wolfgang

view this post on Zulip Email Gateway (Aug 22 2022 at 20:46):

From: "Jackson, Vincent (Data61, Kensington NSW)" <Vincent.Jackson@data61.csiro.au>
A small theory that produces the error is

theory SmallLang
imports Nominal2.Nominal2
begin

nominal_datatype ty = TRecord ‹ty list›

end

the typevar was just an

atom_decl typevar

but this seems to be unrelated to the error.

I'm using the AFP Isabelle2019 version of Nominal2, if that helps.

Thanks,
Vincent

view this post on Zulip Email Gateway (Aug 22 2022 at 20:46):

From: "Urban, Christian via Cl-isabelle-users" <cl-isabelle-users@lists.cam.ac.uk>
Dear Vincent,

Sorry, I should have seen this problem earlier. While the datatype package acquired the possibility to have nested datatypes where you can define

datatype ty = TRecord ‹ty list›

the Nominal2 package is still from a time where this was not possible. This means you would have to write something like this

nominal_datatype
ty = TRecord ty_list
and ty_list = Nil2
| Cons2 ty ty_list

Unfortunately this means you define a "copy" of the list-datatype and you would have to reprove the facts you need for this copy.

Hope this helps,
Christian

view this post on Zulip Email Gateway (Aug 22 2022 at 20:46):

From: "Urban, Christian via Cl-isabelle-users" <cl-isabelle-users@lists.cam.ac.uk>
Hi Wolfgang,

So did I get this correctly that Nominal2 isn’t further developed
anymore?

Yes, it is true that it is not currently on the top of my
to-do list. Sorry. I am also not aware whether anybody else
is tinkering with the code. It is part of the AFP and so
will be maintained and kept in a working state.

By the way, is the restriction that values of a nominal data type may
not contain functions also in place in Nominal2?

Yes, unless the function is "trivial" such as

nominal_datatype
ty = TRecord "bool \<Rightarrow> char"
| Test

Hope this helps,
Christian


From: cl-isabelle-users-bounces@lists.cam.ac.uk <cl-isabelle-users-bounces@lists.cam.ac.uk> on behalf of Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Sent: 17 October 2019 16:31
To: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] Nominal2 fails on Datatypes with Lists

Hi, Christian!

So did I get this correctly that Nominal2 isn’t further developed
anymore?

By the way, is the restriction that values of a nominal data type may
not contain functions also in place in Nominal2?

All the best,
Wolfgang

Am Donnerstag, den 17.10.2019, 12:35 +0000 schrieb Urban, Christian:

Hi Wolfgang,

Is Nominal2 somehow production-ready?

This depends on your point of view. ;o) It is certainly true that it
quite rough and not all features are implemented. And it was aeons ago
I have done things with it. But at the same time people have found it
useful and have used it in interesting formalisations, for example

https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.isa-afp.org%2Fbrowser_info%2Fcurrent%2FAFP%2FIncompleteness%2F&data=01%7C01%7Cchristian.urban%40kcl.ac.uk%7Cbac0eaf2865d405c566a08d75317466a%7C8370cf1416f34c16b83c724071654356%7C0&sdata=s6JMWrL4auiYJIzYkyFs9HEwE6maeSio%2Bdp7OWMnTv8%3D&reserved=0

It really depends on what your point of view is and what you want to
do.

Christian


From: cl-isabelle-users-bounces@lists.cam.ac.uk <
cl-isabelle-users-bounces@lists.cam.ac.uk> on behalf of Wolfgang
Jeltsch <wolfgang-it@jeltsch.info>
Sent: 16 October 2019 22:04
To: cl-isabelle-users@lists.cam.ac.uk <
cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] Nominal2 fails on Datatypes with Lists

Hi, Christian!

Is Nominal2 somehow production-ready? From its website I got the
impression that it had been developed only half-way and then
development had halted.

All the best,
Wolfgang


Last updated: Mar 28 2024 at 16:17 UTC