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
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