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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
