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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
