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