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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
