Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] datatype omits case_transfer for types without...

Email Gateway (Aug 22 2022 at 10:37):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear BNF developers,

I just noticed that for the case combinator, the BNF package forgets to prove and register
the parametricity theorem as [transfer_rule] for datatypes without type variables. It only
proves and registers the one for the recursor. As the case combinator is also polymorphic,
it would be great if I had not state and prove the theorem manually.

Here's a minimal example:

datatype test = A nat | B bool
thm test.case_transfer (* does not exist *)

datatype 'a test2 = A nat | B bool
thm test2.case_transfer (* does exist *)

Best,
Andreas

Last updated: Apr 25 2024 at 04:18 UTC