I agree. Since predicates are primitive, starting from them is appropriate.
Tobias Am 26/08/2011 18:33, schrieb Brian Huffman: > Here's one possible approach to the set-axiomatization/typedef issue: > > As a new primitive, we could have something like a "pred_typedef" > operation that uses predicates. This would work just like the > new_type_definition facility of HOL4, etc. > > The type "'a set" could be introduced definitionally using "pred_typedef". > > After type "'a set" has been defined, we can implement the "typedef" > command, preserving its current behavior, as a thin wrapper on top of > "pred_typedef". > > This approach would let us avoid having to axiomatize the 'a set type. > Also, for those of us who like predicates, "pred_typedef" might be > rather useful as a user-level command. > > - Brian > > On Fri, Aug 26, 2011 at 12:06 AM, Lawrence Paulson <l...@cam.ac.uk> wrote: >> 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 >> > _______________________________________________ > 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