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

[Makarius]

On Fri, 26 Aug 2011, Brian Huffman wrote:

> Here's one possible approach to the set-axiomatization/typedef issue:
>
> As a new primitive, we could have something like a "pred_typedef" 
> operation that uses predicates. This would work just like the 
> new_type_definition facility of HOL4, etc.
>
> The type "'a set" could be introduced definitionally using 
> "pred_typedef".
>
> After type "'a set" has been defined, we can implement the "typedef" 
> command, preserving its current behavior, as a thin wrapper on top of 
> "pred_typedef".
>
> This approach would let us avoid having to axiomatize the 'a set type. 
> Also, for those of us who like predicates, "pred_typedef" might be 
> rather useful as a user-level command.

What is gained from that apart from having two versions of typedef?

We have had that very discussion around 1994, when Tobias thought that 
typedef could be a definitional primitive of Pure, but it turned out to be 
non-conservative outside of its special HOL-ish semantic fitting.


 	Makarius