[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
makarius at sketis.net
Fri Aug 26 22:38:47 CEST 2011
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
> After type "'a set" has been defined, we can implement the "typedef"
> command, preserving its current behavior, as a thin wrapper on top of
> 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.
More information about the isabelle-dev