[isabelle-dev] Quotient example with partiality?

[Makarius]

On Tue, 29 Nov 2011, Lukas Bulwahn wrote:

> On 11/28/2011 10:41 PM, Makarius wrote:
>> On Mon, 28 Nov 2011, Lukas Bulwahn wrote:
>>
>>>>>  many recent requests for adjusting the user-space behavior of 
>>>>> typedef
>>> would then rather apply to quotient_type.
>>> 
>>> Also, I do not see the clear advantage how the suggested change would 
>>> make the adjustments simpler. I would rather imagine that the 
>>> quotient_type command could be assimilated by extending the typedef 
>>> command to enable to hook the pre- and post processing of quotient 
>>> type into typedef.
>> 
>> This reminds me of datatype interpretation, but it is more like an 
>> example of super package bloat.
>> 
>> 
> The quotient type defines a type with typedef, defines some further 
> constants, and sets some declarations. If typedef becomes a super 
> package, all this could be done somewhere in typedef with some setup.

BTW, there is already Typedef.interpretation, which means other packages 
can participate in each foundational defition of a typedef -- the internal 
name is passed as a handle.  This allows to "consolidate" derived content 
in the context, e.g. add-on definitions. It also requires some care, 
because interpretations refer to all past and future items being 
introduced -- a bad interpretation function can easily bomb the theory, in 
particular after unexpected merges.

If the augmented content is just a plain function over the existing data, 
it is easier to add it to the lookup function of the other package, to 
produce extra stuff on the spot in a non-persistent manner.


 	Makarius