https://gist.github.com/minpou/0f4c4a509c253cd7d555

MonMonoid.thy

theory MonMonoid
imports Main
begin

locale Monad =
  fixes mreturn and mbind (infixl ">>-" 60)
  assumes left_return: "mreturn a >>- f = f a"
  and     right_return: "m >>- mreturn = m"
  and     assoc: "(m >>- f) >>- g = m >>- (λx. f x >>- g)"

locale Monoid =
  fixes mempty and mappend (infixl "⋆" 60)
  assumes left_id: "mempty ⋆ m = m"
  and     right_id: "m ⋆ mempty = m"
  and     assoc: "(l ⋆ m) ⋆ n = l ⋆ (m ⋆ n)"

theorem mon_monoid:
  fixes mreturn and mbind (infixl ">>-" 60) and mempty and mappend (infixl "⋆" 60)
  assumes monad: "PROP Monad mreturn mbind" and monoid: "Monoid mempty mappend"
  shows "Monoid (mreturn mempty) (λm n. m >>- (λx. n >>- (λy. mreturn (x ⋆ y))))"
proof
  fix m
  have "mreturn mempty >>- (λx. m >>- (λy. mreturn (x ⋆ y))) = m >>- (λy. mreturn (mempty ⋆ y))"
    using Monad.left_return [OF monad] by simp
  also have "… = m >>- mreturn"
    using Monoid.left_id [OF monoid] by simp
  also have "… = m"
    using Monad.right_return [OF monad] by simp
  finally
    show "mreturn mempty >>- (λx. m >>- (λy. mreturn (x ⋆ y))) = m" by simp
next
  fix m
  have "m >>- (λx. mreturn mempty >>- (λy. mreturn (x ⋆ y))) = m >>- (λx. mreturn (x ⋆ mempty))"
    using Monad.left_return [OF monad] by simp
  also have "… = m >>- mreturn"
    using Monoid.right_id [OF monoid] by simp
  also have "… = m"
    using Monad.right_return [OF monad] by simp
  finally
    show "m >>- (λx. mreturn mempty >>- (λy. mreturn (x ⋆ y))) = m" by simp
next
  fix l m n
  show "l >>- (λx. m >>- (λy. mreturn (x ⋆ y))) >>- (λx. n >>- (λy. mreturn (x ⋆ y))) =
        l >>- (λx. m >>- (λx. n >>- (λy. mreturn (x ⋆ y))) >>- (λy. mreturn (x ⋆ y)))"
    apply (simp add: Monad.assoc [OF monad])
    apply (simp add: Monad.left_return [OF monad])
    apply (simp add: Monoid.assoc [OF monoid])
    done
qed

end