I have

```
locale monoid =
fixes Monoid and composition (infixl "oMonoid" 70) and unitMonoid
assumes composition_closed [intro, simp]: "⟦ a ∈ Monoid; b ∈ Monoid ⟧ ⟹ a oMonoid b ∈ Monoid"
and unit_closed [intro, simp]: "unitMonoid ∈ Monoid"
and associative [intro]: "⟦ a ∈ Monoid; b ∈ Monoid; c ∈ Monoid ⟧ ⟹ (a oMonoid b) oMonoid c = a oMonoid (b oMonoid c)"
and left_unit [intro, simp]: "a ∈ Monoid ⟹ unitMonoid oMonoid a = a"
and right_unit [intro, simp]: "a ∈ Monoid ⟹ a oMonoid unitMonoid = a"
interpretation charlist: monoid where
Monoid = "UNIV :: char list set" and
composition = List.append and
unitMonoid = "[]"
by (unfold_locales) auto
```

Now I would like to construct a type synonym that would have a constraint:

type_synonym ('a, 'm: monoid) tyop = ...

May I use a type class or a locale construct for this, or this is not possible due to the limitations of the type system?

Also, I see a problem here that monoid is not a type but a locale, a different syntactic category.

Please let me know whether my goal is doable in Isabelle in any way.

Last updated: Oct 12 2024 at 20:18 UTC