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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
