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

[Brian Huffman]

On Fri, Aug 26, 2011 at 1:38 PM, Makarius <makarius at sketis.net> wrote:
> 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?

In the current version of Isabelle, not much (although I personally
think that a predicate-based variant of typedef would have value). But
assuming we go ahead and reintroduce "'a set" as a separate type
again, this plan for typedef would reduce the number of primitive
concepts and axioms required to bootstrap HOL.

Of course, axioms like mem_Collect_eq and Collect_mem_eq are rather
uncontroversial, as axioms go. But if there is an easy way to avoid
declaring these as axioms, then keeping them as axioms seems a bit
gratuitous, in my opinion.

- Brian