Email Gateway (Aug 22 2022 at 20:45): 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.
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
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
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
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
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
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
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
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 exampleIt 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 ListsHi, 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: Nov 21 2024 at 12:39 UTC