[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
lp15 at cam.ac.uk
Fri Aug 26 09:06:08 CEST 2011
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.
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev