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

[Michael Norrish]

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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 551 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110826/5f4a877d/attachment.sig>