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

[Brian Huffman]

On Fri, Aug 26, 2011 at 9:36 AM, Andreas Schropp <schropp at in.tum.de> wrote:
> On 08/26/2011 06:50 PM, Tobias Nipkow wrote:
>>
>> I agree. Since predicates are primitive, starting from them is
>> appropriate.
>>
>> Tobias
>
> Did I get this right:
>  the idea is to implement our advanced typedef via a HOL4-style predicate
> typedef?
> That doesn't work because HOL4-style typedefs don't feature our extensions
> to typedef and they are only conservative via a global theory
> transformation.

What exactly are our extensions to typedef?

As far as I understand, the typedef package merely issues global
axioms of the form "type_definition Rep Abs S", as long as it is
provided with a proof of "EX x. x : S".

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

What am I missing here?

- Brian