In Isabelle's NEWS
file, I found
Command 'typedef' now works within a local theory context -- without introducing dependencies on parameters or assumptions, which is not possible in Isabelle/Pure/HOL. Note that the logical environment may contain multiple interpretations of local typedefs (with different non-emptiness proofs), even in a global theory context.
(which dates back to Isabelle2009-2). Is this the latest news with respect to typedef
and local theory contexts? Further, what does the restriction "without introducing dependencies on parameters or assumptions" actually mean?
If it would mean that I cannot use locale parameters in the defining set of a typedef
, then I would not consider typedef
to be localized at all (since the only allowed instances can easily be moved outside the local context, or am I missing something?).
Is it (or should it, or will it ever be) possible to do something along the lines (where the set used for a typedef
depends on the locale parameter V
):
datatype ('a, 'b) "term" = Var 'b | Fun 'a "('a, 'b) term list"
locale term_algebra =
fixes F :: "'a set"
and V :: "'b set"
begin
definition "domain α = {x : V. α x ~= Var x}"
typedef ('a, 'b) subst =
"{α :: 'b => ('a, 'b) term. finite (domain α)}"
end
for which I currently obtain:
Locally fixed type arguments "'a", "'b" in type declaration "subst"
A few more notes on this:
The local theory infrastructure merely organizes existing module concepts (
locale
,class
etc.) such that definitional mechanisms (definition
,theorem
,inductive
,function
etc.) can work uniformly in a variety of contexts. This does not change the logical foundations, so specification elements that cannot depend on term parameters (fixes
) or premises (assumes
) won't become fundamentally better. They are merely retrofitted into the greater framework, which is already an extra-logical benefit.The canonical local theory targets are
locale
and its derivatives likeclass
. These work within the logic according to the principles sketched above: lambda-lifting via some context offixes
andassumes
. Other targets with more ambition can be imagined, but need to be implemented by some brave and heroic guys. For example, one could wrap up the AWE theory interpretation mechanism as another local theory target, and then get parametrization of types/consts/axioms --- at the usual cost of going through explicit proof terms to implement admissible inferences within an LCF prover (or at the cost of giving up LCF-ness and do it via some oracle).Plain
typedef
as sketched above (and its derivatives like the localizedcodatatype
anddatatype
of recent HOL-BNF) could be slightly improved in its dependecy type parameters, but this would mean some implementation efforts that don't justify the meagre outcome right now. It would merely allow to write polymorphic type constructions with implicit arguments like this:After export you would get
'a list
as usual.Further complication:
fixes type 'a
does not exist. Isabelle/Pure handles type parameters implicitly via Hindley-Milner.In the meanwhile, this question was answered on the Isabelle mailing list. The short version is that what I tried to do is simply impossible. What follows is an explanation by @makarius:
As for my specific example: