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

[Makarius]

On Fri, 26 Aug 2011, Brian Huffman wrote:

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

We have had exactly that discussion in 1994.  Nothing is gained 
foundationally by adding or substracting these the mem/Collect axioms. 
It is a matter of what is more useful for the user, without duplicating 
packages at will.  Back then we decided to go with 'a set for typedef, as 
had been the original scheme by Larry from long before.  Whetever becomes 
of the 'a => bool vs. 'a set plan, the typedef package should follow the 
main line without becoming more complicated by additional variants.

Concerning axiomatizations in general, it is good practice to be 
"conservative" in a common sense, sticking to well-understood 
axiomatizations instead of reducing them by mere number.


Anyway the typedef package is right now in a relatively clean state, and 
almost fully "localized".  Any spare time is better invested in other 
packages, such as the HOLCF versions of it, not to speak of our running 
gags of record and datatype.  Nothing to be started before the release, 
though.


 	Makarius