Stream: General

Topic: Type construction

view this post on Zulip Gergely Buday (Jun 15 2023 at 15:14):

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