[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.