John Hughes (Feb 13 2025 at 01:32): John Hughes (Feb 13 2025 at 01:32):I'd like to define a type that has a different notion of equality from that automatically produced by a datatype definition. In hopes of building a simple example, making "A" and "B" be equal, and "C" and "D" be equal, in an enumerated data type, and everything equal to itself, I tried to mimic the apparent definition of equality on page 91 of the matrix-and-Jordan-form doc, https://www.isa-afp.org/browser_info/current/AFP/Jordan_Normal_Form/document.pdf.
I wrote this:
theory MWE4
imports Complex_Main
begin
datatype s = A | B | C | D
instantiation s::(type) equal begin
definition (equal_s :: (s ⇒ s ⇒ bool)) = (=)
instance
by (intro-classes, auto simp: equal-s-def)
end
end
If you try this at home, you'll see that I never got a chance to define anything, because on the "instantiation" line, I got an error:
No parameters and no pending instance proof obligations in instantiation.
Is this kind of "I want to redefine equality for my kind of datatype" thing even possible? Can someone tell me what the error means?
Yong Kiam (Feb 13 2025 at 01:38):I think redefining = is not possible. You could certainly define a different relation.
See Sec 2.3.1, https://isabelle.in.tum.de/doc/prog-prove.pdf
specifically, distinctness of constructors
Yong Kiam (Feb 13 2025 at 01:40):^ and specifically you may be able to quotient under the new relation to get a new type s' that obeys the equality, but I've never tried that... probably need who knows more could help on that
Mathias Fleury (Feb 13 2025 at 06:20):Yeah you are going to have to normalize the type somehow. Either you go for a new equality (see for example https://isabelle.in.tum.de/library/HOL/HOL/Rat.html#Rat.ratrel|const) or for a new type (where you sort the elements in a pair).
Last updated: Mar 09 2025 at 12:28 UTC