[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Andreas Schropp]

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
>