Bob Rubbens (Sep 14 2023 at 07:48): Bob Rubbens (Sep 14 2023 at 07:48):Hi all, in pen and paper formalizations often functions are defined that do something simple, e.g. collect all entities in some structure. Then they also often state, we implicitly use this function with lists of structures, sets, sequences, etc., the function then behaves in the obvious way. I find this hard to translate to Isabelle. Meaning that you can use some function on various types, and that Isabelle picks the right function depending on the input type. I wanted to use typeclasses for this, since it seems like the obvious candidate, but as you cannot instantiate typeclasses over "set MyType" or a tuple of two types, it doesn't work well in formalizations where I have not newtyped every single thing.
(newtyping also has it's downsides, right? If I newtype a tuple, I'll have to duplicate all the automization Isabelle has for tuples over my own newtyped tuple)
An alternative is to use Isabelle's low-level overloading mechanism, but I've read this is only intended as a primitive to implement typeclasses, so I'm a bit hesitant to use that. In the end I usually add a subscript to distinguish each version of this collection function, but that makes the code noisy. Is there any other way to tackle this that I'm missing? Or is there simply room for improvement here?
Last updated: Apr 27 2024 at 16:16 UTC