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. Larry
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. > > Michael > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev