Theory Monad_Plus

section ‹Monad-Plus Class›

theory Monad_Plus
imports Monad
begin

hide_const (open) Fixrec.mplus

class plusU = tycon +
  fixes plusU :: "udom⋅'a → udom⋅'a → udom⋅'a::tycon"

class functor_plus = plusU + "functor" +
  assumes fmapU_plusU [coerce_simp]:
    "fmapU⋅f⋅(plusU⋅a⋅b) = plusU⋅(fmapU⋅f⋅a)⋅(fmapU⋅f⋅b)"
  assumes plusU_assoc:
    "plusU⋅(plusU⋅a⋅b)⋅c = plusU⋅a⋅(plusU⋅b⋅c)"

class monad_plus = plusU + monad +
  assumes bindU_plusU:
    "bindU⋅(plusU⋅xs⋅ys)⋅k = plusU⋅(bindU⋅xs⋅k)⋅(bindU⋅ys⋅k)"
  assumes plusU_assoc':
    "plusU⋅(plusU⋅a⋅b)⋅c = plusU⋅a⋅(plusU⋅b⋅c)"

instance monad_plus ⊆ functor_plus
by standard (simp_all only: fmapU_eq_bindU bindU_plusU plusU_assoc')

definition fplus :: "'a⋅'f::functor_plus → 'a⋅'f → 'a⋅'f"
  where "fplus = coerce⋅(plusU :: udom⋅'f → _)"

lemma fmap_fplus:
  fixes f :: "'a → 'b" and a b :: "'a⋅'f::functor_plus"
  shows "fmap⋅f⋅(fplus⋅a⋅b) = fplus⋅(fmap⋅f⋅a)⋅(fmap⋅f⋅b)"
unfolding fmap_def fplus_def
by (simp add: coerce_simp)

lemma fplus_assoc:
  fixes a b c :: "'a⋅'f::functor_plus"
  shows "fplus⋅(fplus⋅a⋅b)⋅c = fplus⋅a⋅(fplus⋅b⋅c)"
unfolding fplus_def
by (simp add: coerce_simp plusU_assoc)

abbreviation mplus :: "'a⋅'m::monad_plus → 'a⋅'m → 'a⋅'m"
  where "mplus ≡ fplus"

lemmas mplus_def = fplus_def [where 'f="'m::monad_plus" for f]
lemmas fmap_mplus = fmap_fplus [where 'f="'m::monad_plus" for f]
lemmas mplus_assoc = fplus_assoc [where 'f="'m::monad_plus" for f]

lemma bind_mplus:
  fixes a b :: "'a⋅'m::monad_plus"
  shows "bind⋅(mplus⋅a⋅b)⋅k = mplus⋅(bind⋅a⋅k)⋅(bind⋅b⋅k)"
unfolding bind_def mplus_def
by (simp add: coerce_simp bindU_plusU)

lemma join_mplus:
  fixes xss yss :: "('a⋅'m)⋅'m::monad_plus"
  shows "join⋅(mplus⋅xss⋅yss) = mplus⋅(join⋅xss)⋅(join⋅yss)"
by (simp add: join_def bind_mplus)

end