[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Andreas Schropp
schropp at in.tum.de
Fri Aug 26 18:56:08 CEST 2011
On 08/26/2011 07:08 PM, Brian Huffman wrote:
> What exactly are our extensions to typedef?
>
I enumerated them in the other thread:
local typedefs, sort constraints on type parameters,
overloaded constants in representation sets.
Hopefully I am not missing others.
> My understanding of the localized typedef is that it works by
> declaring a global typedef behind the scenes (much like a local
> definition of a polymorphic constant works by declaring a global
> polymorphic definition behind the scenes).
>
Last time I looked local typedefs were primitive. Makarius?
Actually I suggested exactly this treatment of local typedefs
back in the day, so thanks for bringing this up.
> What am I missing here?
>
Most importantly you are missing (indirectly) overloaded constants in
representing sets of typedefs. E.g.
typedef 'a matrix = {f . finite (nonzero_positions f) }
depends on nonzero_positions, which depends on the
overloaded constant zero['a].
If we try to transform this to HOL4-style typedef without (indirectly)
overloaded
constants, we have to abstract out a dictionary for zero['a], which
would give rise to
dependent typedefs. A solution is to eliminate such typedefs completely,
replacing them by their representing sets, regarded as soft-types.
This is an extremely non-trivial global theory-transformation.
> - Brian
>
More information about the isabelle-dev
mailing list