[isabelle] Interpreting lists as an instance of monoid_mult fails
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:
interpretation semilist: semigroup_mult append
show "class.semigroup_mult (@)"
show "⋀a b c. (a @ b) @ c = a @ (b @ c)"
interpretation monlist: monoid_mult "" "(@)"
show "class.monoid_mult  (@)"
show "⋀a.  @ a = a"
show "⋀a. a @  = a"
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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and