```
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?

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.

`Monoid`

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

@Fabian Huch I did `Monoid = "UNIV :: char list set"`

but that did not eliminate the spurious ` ⋀M. [] ∈ M`

subgoal.

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)

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

Last updated: Sep 11 2024 at 16:22 UTC