[isabelle] Overloaded datatype constructors
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] Overloaded datatype constructors
- From: Alexander Krauss <krauss at in.tum.de>
- Date: Fri, 13 Apr 2012 01:16:50 +0200
- User-agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:188.8.131.52) Gecko/20120320 Icedove/3.0.11
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