[isabelle-dev] Quotient example with partiality?

[Lukas Bulwahn]

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.
While explaining this here, I feel more and more that this is not a good 
idea to do at all, and also Florian's suggestion becomes very questionable.

> Can you explain further what is the purpose of the pre- and post 
> processing mentioned above?  In 5b0b1dc2e40f I've recently seen this, 
> but did not have time to look more closely so far, and the lines are a 
> bit too long for quick reading and understanding.
>
>
> text {* Here is some ML setup that should eventually be incorporated 
> in the typedef command. *}
>
> local_setup {* fn lthy =>
> let
>   val quotients = {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"}, 
> equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
>   val qty_full_name = @{type_name "set"}
>
>   fun qinfo phi = Quotient_Info.transform_quotients phi quotients
>   in lthy
>     |> Local_Theory.declaration {syntax = false, pervasive = true}
>         (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo 
> phi)
>        #> Quotient_Info.update_abs_rep qty_full_name 
> (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = 
> @{term "member"}}))
>   end
> *}
>
>
> At first sight this looks like some dummy data item is retrofitted to 
> typedefs that are not full quotient types.  Couldn't the Quotient_Info 
> lookup do this on the spot as a fall-back?  Or is there anything 
> special with full declarations and morphisms here?
>
>
You are right, some dummy data item is retrofitted to typedef that are 
not full quotient types.

Eventually, some general parts of the quotient type infrastructure 
should also be usable for simple type definitions.
Obviously, it is easy to hook into the quotient type infrastructure with 
dummy data to obtain the wished results, that is what 5b0b1dc2e40f does.

Doing it right, separating the general parts from the specific parts for 
equivalence relations and quotients correctly, is hard work, which we 
addressing
in near future.

The source code above disappears when we understand how the 
generalisation looks like, how the data structures must be separated 
(making dummy data or lookup with default dummy data obsolete), and how 
we present this to the
user on the Isar level.

The current noise in this file will be reduced as we proceed.


Lukas