Re: [isabelle] Nominal2 fails on Datatypes with Lists



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
________________________________
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

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

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?
>
> Thanks,
> Christian
> ________________________________
> 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&amp;data=01%7C01%7Cchristian.urban%40kcl.ac.uk%7C6029b51d577949c4b47308d7527c960b%7C8370cf1416f34c16b83c724071654356%7C0&amp;sdata=SeCuPvk58tLLSsrNIiZBm%2BZxDcKY1z9CqB9%2Bxl0XUh0%3D&amp;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 MHonArc.