Re: [isabelle] Nominal2 fails on Datatypes with Lists
> 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
It really depends on what your point of view is and what you want to do.
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Wolfgang Jeltsch <wolfgang-it at jeltsch.info>
Sent: 16 October 2019 22:04
To: cl-isabelle-users at lists.cam.ac.uk <cl-isabelle-users at lists.cam.ac.uk>
Subject: Re: [isabelle] Nominal2 fails on Datatypes with Lists
Is Nominal2 somehow production-ready? From its website I got the
impression that it had been developed only half-way and then development
All the best,
Am Dienstag, den 15.10.2019, 10:46 +0000 schrieb Urban, Christian:
> 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?
> From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Jackson, Vincent (Data61, Kensington NSW) <Vincent.Jackson at data61.csiro.au>
> Sent: 15 October 2019 03:20
> To: cl-isabelle-users at lists.cam.ac.uk <cl-isabelle-users at lists.cam.ac.uk>
> Subject: [isabelle] Nominal2 fails on Datatypes with Lists
> Hello All,
> I have been recently experimenting with Nominal2<https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.isa-afp.org%2Fentries%2FNominal2.html&data=01%7C01%7Cchristian.urban%40kcl.ac.uk%7C6029b51d577949c4b47308d7527c960b%7C8370cf1416f34c16b83c724071654356%7C0&sdata=SeCuPvk58tLLSsrNIiZBm%2BZxDcKY1z9CqB9%2Bxl0XUh0%3D&reserved=0>, 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and