[isabelle] Overloaded datatype constructors

Hi all,

I wonder if it is possible (possibly via some tricks) to make datatype constructors coincide with overloaded constants.

The only datatype in Isabelle/HOL with overloaded constructors is the type "nat", where 0 is overloaded. That type is defined via an explicit construction followed by rep_datatype, for bootstrapping reasons.

But there are situations where it is natural to use overloading in a datatype, even for only syntactic reasons. For example, in a type of regular expressions it would be natural to use +,*,0,1.

The only way to achieve this that I can think of is the following, but it is rather tricky:

  1) Define an auxiliary datatype with non-overloaded constructors

2) Define an isomorphic copy of that datatype. Define the overloaded constants as the lifted constructors, possibly using lifting machinery.

  3) Use rep_datatype on the isomorphic copy.

Has anybody got a better idea? I feel that the above is too technical to be worth the effort.

Is it conceivable that a fully localized datatype package could do this directly, when used in an instantiation target???


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