Email Gateway (Aug 17 2022 at 14:44): Email Gateway (Aug 17 2022 at 14:44):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
I decided it might be useful to have a class of non trivial types.
axclass
non_trivial <= type
non_trivial: "(? y. y ~= x)"
But it seems I can't handle cross product properly.
instance
"*" :: (non_trivial, type) non_trivial
apply (intro_classes)
apply (auto simp add: trivial_false)
done
works, but then
instance
"*" :: (type, non_trivial) non_trivial
becomes an error.
Is there anyway around this?
If not, is the restriction well-placed in this case?
Dr Brendan Mahony
Information Networks Division ph +61 8 8259 6046
Defence Science and Technology Organisation fx +61 8 8259 5589
Edinburgh, South Australia Brendan.Mahony@dsto.defence.gov.au
Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.
Email Gateway (Aug 17 2022 at 14:44):From: nipkow@in.tum.de
Brendan,
Allowing both
instance
"*" :: (non_trivial, type) non_trivial
instance
"*" :: (type, non_trivial) non_trivial
would raise a type inference problem: given a product type 'a * 'b for which
we know that it must be of class non_trivial, there is no most general way to
express this via the classes of the two type variables: either 'a OR 'b need to
be of class non_trivial. Hence Isabelle disallows such "overlapping"
declarations. Sorry. (Not sure what Haskell does these days).
Tobias
Last updated: May 03 2024 at 04:19 UTC