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

Michael Norrish Michael.Norrish at nicta.com.au
Fri Aug 26 00:24:46 CEST 2011

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.


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

More information about the isabelle-dev mailing list