[isabelle-dev] typedef

[Makarius]

On Fri, 26 Aug 2011, Andreas Schropp wrote:

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

I also remember this part of the discussion from some years ago.  IIRC it 
was only HOL-Matrix and HOLCF that where using this further genuine 
extension of typedef wrt. overloading.  My gut feelings say it is somehow 
right, but one would need proper proofs (preferably formal ones) for it. 
In a pitch one could also refrain from using that form in main 
Isabelle/HOL.


 	Makarius