[isabelle] datatype omits case_transfer for types without type variables



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.