[isabelle-dev] Quotient example with partiality?

[Makarius]

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.


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?


 	Makarius