Email Gateway (Aug 18 2022 at 13:43): Email Gateway (Aug 18 2022 at 13:43):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
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? If so,
can different theories instantiate the type differently? What happens
then at a theory merge?
Are there other ways to fix type parameters such that I don't have to
write them everywhere?
Andreas
Email Gateway (Aug 18 2022 at 13:43):From: Makarius <makarius@sketis.net>
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.
Makarius
Last updated: May 03 2024 at 08:18 UTC