5
$\begingroup$

I am trying to define a hierarchy of type classes with binary operations, in which the base class defines a binary operation binop and then each class mult and add redefines the binop to be a different name (add and mult, resp.). I saw the basic syntax in the Isabelle 2021 tutorial:

class binop = 
  fixes binop::"'a ⇒ 'a ⇒ 'a" (infixl "∘" 75)

class mult = binop +
  fixes mult::"'a ⇒ 'a ⇒ 'a" (infixl "⊗" 80)

class add = binop +
  fixes add::"'a ⇒ 'a ⇒ 'a" (infixl "⊕" 70)

But the above approach defines a new operator in each subclass instead of specializing the existing binop. I have also tried instantiation unsuccessfully, but it seems conceptually wrong to begin with.

My question is:

How can I reuse/redefine the class operation of the common base class?

(My goal is to (learn to) define two different semigroups on add and mult, e.g. for some numeric types)

(I originally posted this question in SO, but didn't get much response. So I am deleting the question there and posting it here for more attention.)

$\endgroup$
1
  • $\begingroup$ My goal is to (learn to) define two different semigroups on add and mult, e.g. for some numeric types. A canonical methodology for this can be found in the theory Groups.thy in the main library of Isabelle/HOL. There you will find the definitions of the type classes semigroup_add and semigroup_mult that, I believe, serve the purpose that you intend. I am not certain if I understand the nature of the problem in your question, however. $\endgroup$ Feb 14, 2022 at 18:01

1 Answer 1

4
$\begingroup$

Perhaps you checked the general tutorial, but the one you need to look at is on locales and locale interpretation, or the more specialized Haskell-style type classes with Isabelle/Isar.

I'm more familiar with the first one. Actually, Isabelle classes are a particular case of the more general concept of locale. In Section 6 (“Locale Expressions”) of the first tutorial it is suggested that you use the base locale to define the new one, changing the symbol on the spot.

theory Scratch
  imports Main
begin

class binop = 
  fixes binop::"'a ⇒ 'a ⇒ 'a" (infixl "∘" 75)

locale add = binop add for add (infixl "⊕" 70)

locale mult = binop mult for mult (infixl "⊗" 80)

locale ldistrib = add + mult +
  assumes
    left_distrib: "x ⊗ (y ⊕ z) = x ⊗ y ⊕  x ⊗ z"

end

The for clauses declare the new function names and establish the notation.

$\endgroup$
1
  • $\begingroup$ Surely, there must be a way to do this jsut using the class infrastructure but this was the first thing I got to compile. $\endgroup$ Feb 14, 2022 at 13:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.