## Stream: General

### Topic: Proving set membership in a type

#### Gergely Buday (Jun 14 2023 at 14:38):

``````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 ∈ M"
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 list: monoid where
Monoid = "char list" and
composition = List.append and
unitMonoid = "[]"
apply (unfold_locales)
apply auto
``````

gives

``````proof (prove)
goal (2 subgoals):
1. ⋀a b. a ∈ char list ⟹ b ∈ char list ⟹ a @ b ∈ char list
2. ⋀M. [] ∈ M
``````

which seem to be trivial, these set memberships follow from the properties of char list, the type.

But how can I convince Isabelle about them?

#### Fabian Huch (Jun 14 2023 at 14:46):

I think you're mixing up types and terms here. You can't quantify over types in Isabelle, you have to prove set membership of the sets "char list" and "M" here. Of course that doesn't hold, `[]` is certainly not in any set.

#### Fabian Huch (Jun 14 2023 at 14:47):

`Monoid` is a variable (not a type), no matter if you spell it upper- or lowercase.

#### Gergely Buday (Jun 14 2023 at 15:13):

@Fabian Huch I did `Monoid = "UNIV :: char list set"`but that did not eliminate the spurious ` ⋀M. [] ∈ M` subgoal.

#### Fabian Huch (Jun 14 2023 at 15:18):

Then your definition does make sense, the problem with `M` is just that it's not mentioned anywhere else. I think you meant `Monoid`? (in the locale specification)

#### Gergely Buday (Jun 14 2023 at 18:45):

Oh yes, I have failed to rename M to Monoid at one instance, thanks.

Last updated: Dec 07 2023 at 16:21 UTC