Re: [isabelle] Nominal2 fails on Datatypes with Lists



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
________________________________
From: Jackson, Vincent (Data61, Kensington NSW) <Vincent.Jackson at data61.csiro.au>
Sent: 17 October 2019 23:44
To: Urban, Christian <christian.urban at kcl.ac.uk>; cl-isabelle-users at lists.cam.ac.uk <cl-isabelle-users at lists.cam.ac.uk>
Subject: Re: Nominal2 fails on Datatypes with Lists

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

On Tue, 2019-10-15 at 10:46 +0000, Urban, Christian wrote:
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<mailto:cl-isabelle-users-bounces at lists.cam.ac.uk> <cl-isabelle-users-bounces at lists.cam.ac.uk<mailto:cl-isabelle-users-bounces at lists.cam.ac.uk>> on behalf of Jackson, Vincent (Data61, Kensington NSW) <Vincent.Jackson at data61.csiro.au<mailto:Vincent.Jackson at data61.csiro.au>>
Sent: 15 October 2019 03:20
To: cl-isabelle-users at lists.cam.ac.uk<mailto:cl-isabelle-users at lists.cam.ac.uk> <cl-isabelle-users at lists.cam.ac.uk<mailto: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><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%7C7fa4274811494bd3605808d75353924c%7C8370cf1416f34c16b83c724071654356%7C0&sdata=Fe8f3rcVz184tGkJ0dmBPk59jwubs5OnL2K0Upb0Oag%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 MHonArc.