[isabelle-dev] Quotient example with partiality?
makarius at sketis.net
Wed Nov 30 13:30:16 CET 2011
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
>>> 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.
More information about the isabelle-dev