Re: [isabelle] Nominal2 fails on Datatypes with Lists

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 <cl-isabelle-users-bounces at> on behalf of Jackson, Vincent (Data61, Kensington NSW) <Vincent.Jackson at>
Sent: 15 October 2019 03:20
To: cl-isabelle-users at <cl-isabelle-users at>
Subject: [isabelle] Nominal2 fails on Datatypes with Lists

Hello All,

I have been recently experimenting with Nominal2<;;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.