In my theory developent I have one concept "bar" of function for a bunch of types (say, bar_atom, bar_clause, etc.), so I figured I'd abstract that out using a typeclass for readability (since I'd rather just type "bar" everywhere and have the type system figure out which function to use).
I tried the following:
theory Sat
imports Main
begin
type_synonym atom = nat
class foo =
fixes bar :: "'a ⇒ nat"
instantiation atom :: foo begin
end
end
Isabelle gives an error at "instantiation atom", as follows:
Bad type name: "Sat.atom"⌂
I know this is already partially answered in How to define a class instance of type_synonym?. However, I was hoping that problem was caused by the fact a that there was already a pre-existing typeclass. In my case it's a custom and completely local typeclass, so I was hoping in that case a typeclass over a type synonym is no problem. But I can't get it to work. I wouldn't mind inlining the type synonym, but that doesn't seem to work either. It only seems to work for primitive types like "nat" and "int".
The answer says I could also define my own type, but I'd like my base types to stay simple if I can. I'm assuming the proofs will be more automated if I stick to type synonyms like atom = nat and such, but maybe that's overly cautious? Maybe when this theory development is finished I'd like to abstract the entire thing over the types used (since most of the type synonyms can be opaque, I think, as long as equality is defined) and then this is more relevant, but at the moment as just a proof of concept that's not necessary.
Unfortunately, this does not work. You can either choose to instantiate the class with nat, or to define a wrapper type. If it’s your own class, I’d recommend the former.