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: Dec 07 2023 at 16:21 UTC