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