Email Gateway (Apr 28 2023 at 12:41): Email Gateway (Apr 28 2023 at 12:41):From: Liam O'Connor <l.oconnor@ed.ac.uk>
Hi Isabelle-users,
I am working with the Complete_Partial_Order theory (https://isabelle.in.tum.de/library/HOL/HOL/Complete_Partial_Order.html) and I want to make function types an instance of the ccpo class if their result is (via pointwise lifting):
instantiation "fun" :: (type, ccpo) ccpo
begin
But, annoyingly, because the Complete_Partial_Order theory imports Complete_Lattices, and there is such an instance for complete lattices, and all complete lattices are complete partial orders, there already is an instance for "fun", just for "fun" :: (type, complete_lattice) complete_lattice.
I don't want this type class instance, because the ccpo I want to work with is not a complete lattice. Can I remove this instance somehow? Or is there some way to replace it with a more general one?
With best wishes,
Liam O'Connor
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.
Email Gateway (Apr 28 2023 at 13:58):From: Thomas Sewell <tals4@cam.ac.uk>
That sounds like a flaw in the typing hierarchy (which might be tricky to fix).
Maybe there's a clean way to proceed, but failing that, we should also mention a known workaround. You could just work via (approximately) a type synonym.
In full, you can name a new type isomorphic to the function type you need, and expose its lambda and apply operations. Since the new type has a new name, it can be admitted to the various type classes via a new set of canonical rules.
I hope that helps. Well, no, I hope someone has a better idea, and so I'm not helping at all.
Best wishes,
Thomas.
Email Gateway (Apr 28 2023 at 23:55):From: "YAMADA, Akihisa" <ayamada@trs.cm.is.nagoya-u.ac.jp>
Dear Liam,
one can use `instance' in this case:
instance "fun" :: (type, ccpo) ccpo
`instantiation' is for defining operators but Sup and Inf for fun are
already defined properly.
Best,
Akihisa
Last updated: Jan 04 2025 at 20:18 UTC