[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 551 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev