# [isabelle] Interpreting lists as an instance of monoid_mult fails

Hello,

`I am trying to use the fact that lists form a monoid to obtain some
``algebraic properties of lists for free.
`However, I run into the following complaint, which I do not understand:

`Partially applied constant "List.append" on left hand side of
``equation, in theorem:
`monoid_mult.prod_list [] (@) ?xs ≡ foldr (@) ?xs []

The minimal theory featuring the problem is here:

theory ListMonoid
imports Main
begin
interpretation semilist: semigroup_mult append
proof-
show "class.semigroup_mult (@)"
proof
show "⋀a b c. (a @ b) @ c = a @ (b @ c)"
by simp
qed
qed
interpretation monlist: monoid_mult "[]" "(@)"
proof-
show "class.monoid_mult [] (@)"
proof
show "⋀a. [] @ a = a"
by simp
next
show "⋀a. a @ [] = a"
by simp
qed
qed
end

I am using Isabelle2018/HOL with jEdit.

`I should add that I am aware of the following existing interpretations
``of list's "append"
`

interpretation semilist: semigroup append
by (simp add: append.semigroup_axioms)
interpretation monolist: monoid append Nil
by (simp add: append.monoid_axioms)

`The reason why I needed the context monoid_mult is that I wanted to use
``the results of the theory HOL/Power.thy
`

`Is there any way how to fix this? (Obviously, it does not take too much
``effort to just prove all useful facts afresh, but I wanted to understand
``what is going on).
`
Best regards
Stepan Holub

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*