Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Interpreting lists as an instance of monoid_mu...

Email Gateway (Aug 22 2022 at 20:14):

From: Stepan Holub <holub@karlin.mff.cuni.cz>
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

Last updated: Apr 26 2024 at 04:17 UTC