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%7C55cfee605fd64ec8e07408d7515bbf66%7C8370cf1416f34c16b83c724071654356%7C0&amp;sdata=8dL9LedsVKotsVQVSNab%2F2vu6ekR%2BDTHC%2BEnhZ%2BRC7U%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.