Theory Monad_Zero_Plus

section ‹Monad-Zero-Plus Class›

theory Monad_Zero_Plus
imports Monad_Zero Monad_Plus
begin

hide_const (open) Fixrec.mplus

class functor_zero_plus = functor_zero + functor_plus +
  assumes plusU_zeroU_left:
    "plusU⋅zeroU⋅m = m"
  assumes plusU_zeroU_right:
    "plusU⋅m⋅zeroU = m"

class monad_zero_plus = monad_zero + monad_plus + functor_zero_plus

lemma fplus_fzero_left:
  fixes m :: "'a⋅'f::functor_zero_plus"
  shows "fplus⋅fzero⋅m = m"
unfolding fplus_def fzero_def
by (simp add: coerce_simp plusU_zeroU_left)

lemma fplus_fzero_right:
  fixes m :: "'a⋅'f::functor_zero_plus"
  shows "fplus⋅m⋅fzero = m"
unfolding fplus_def fzero_def
by (simp add: coerce_simp plusU_zeroU_right)

lemmas mplus_mzero_left =
  fplus_fzero_left [where 'f="'m::monad_zero_plus"] for f

lemmas mplus_mzero_right =
  fplus_fzero_right [where 'f="'m::monad_zero_plus"] for f

end