Re: [isabelle] typedecl versus explicit type parameters

On Wed, 29 Jul 2009, Andreas Lochbihler wrote:

The Isabelle tutorial mentions typedecl as a simple way to say that a type is actually a parameter to some theory development. In particular, explicit type parameters for constants, datatypes etc. do not clutter the definitions and proofs.

But what if later on, I want to instantiate such a type to a concrete type in some application that uses the theory? Can this be done?

You would have to produce a post-hoc axiomatic specification of the type. E.g. by postulating "type_definition rep abs A" and maybe reinitializing some declarations in imitation of the 'typedef' package.

A slightly more disciplined way would be to reinterpret the whole theory in the manner of the AWE tool from Bremen.

If so, can different theories instantiate the type differently? What happens then at a theory merge?

With raw axiomatizations you would just get an inconsistent theory.

Are there other ways to fix type parameters such that I don't have to write them everywhere?

A locale context can abstract over simple types, but not type constructors (this is a fundamental limitation of the logical framework, which lacks true polymorphism). See Isabelle2009/src/HOL/ex/Abstract_NAT.thy for an example. We are still working on "localizing" more definitional packages, to allow them within such a local context (record, datatype in particular).

The "target" mechanism behind this idea is fully generic in terms of logical interpretation. So one could even think of wrapping up AWE as a local theory target, and then allow users to interpret polymorphic type and term constants in a disciplined way.


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