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

[Tobias Nipkow]

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