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

[Lawrence Paulson]

indeed yes I'm the person who decided that this primitive should introduce a type as a copy of an existing non-empty set. I have always preferred sets to predicates and the examples I have looked at lately have only strengthened my view. Not to mention numerous occasions when people have re-invented the notion of an image.
Larry

On 25 Aug 2011, at 23:24, Michael Norrish wrote:

> On 26/08/11 7:26 AM, Florian Haftmann wrote:
>> Hi Andreas,
>> 
>>> Let me ask something stupid:
>>>  why exactly do you guys axiomatize 'a set?
>>> Sure it's admissable and all, but why not do this definitionally
>>> via the obvious typedef?
>> 
>> the answer is rather technical: »typedef« in its current implementation
>> needs set syntax / set type as prerequisite.  Of course you could change
>> »typedef« to be based on predicates, but there is some kind of unspoken
>> agreement not to set one's hand on that ancient and time-honoured Gordon
>> HOL primitive.
> 
> HOL88, hol90, hol98 and HOL4 all have new_type_definition.  This
> principle takes a theorem of the form
> 
>  ?x. P x
> 
> HOL Light takes a theorem of the form  P x (removing the dependency on
> the existential quantifier).
> 
> To the best of my knowledge, none of these systems ever used sets in
> this role.
> 
> Michael
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev