Re: [isabelle] typedecl vs. type synonym



Hi Matthias,

that's more of an open question, really.

> Now I try to get an idea what the advantages of the two approaches are,
> but I cannot find a suitable starting point for this in the Isabelle
> documentation.  Any hints?  A short reply when to use which style would
> also be very welcome.

First, to clarify, "type synonyms" are just syntactic abbreviations.
They don't exist inside the logic and are not useful to abstract over
anything.

"typedecl" are unspecified types. It's impossible to "instantiate" them
later. If you want to assume anything non-trivial on them, you're going
to need "axiomatization". There's no tooling in Isabelle that will make
you prove that your assumptions are consistent. However, type
declarations can be polymorphic; i.e., it is possible to declare a
polymorphic type and axiomatize polymorphic constants.

However, if you fix a type variable in a locale or some other context,
it is monomorphic. This point is rather subtle. For example, you can't
abstract over the "map" function of functors in HOL, because it would
require a variable type constructor. On the other hand, the advantage is
that you can in fact instantiate locales later on and can give a proof
that the assumptions are consistent.

For locales in particular, see the tutorial:
<https://isabelle.in.tum.de/dist/Isabelle2016-1/doc/locales.pdf>.

Hope that helps.

Cheers
Lars




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