Theory Monad_Zero

section ‹Monad-Zero Class›

theory Monad_Zero
imports Monad
begin

class zeroU = tycon +
  fixes zeroU :: "udom⋅'a::tycon"

class functor_zero = zeroU + "functor" +
  assumes fmapU_zeroU [coerce_simp]:
    "fmapU⋅f⋅zeroU = zeroU"

class monad_zero = zeroU + monad +
  assumes bindU_zeroU:
    "bindU⋅zeroU⋅f = zeroU"

instance monad_zero ⊆ functor_zero
proof
  fix f show "fmapU⋅f⋅zeroU = (zeroU :: udom⋅'a)"
    unfolding fmapU_eq_bindU
    by (rule bindU_zeroU)
qed

definition fzero :: "'a⋅'f::functor_zero"
  where "fzero = coerce⋅(zeroU :: udom⋅'f)"

lemma fmap_fzero:
  "fmap⋅f⋅(fzero :: 'a⋅'f::functor_zero) = (fzero :: 'b⋅'f)"
unfolding fmap_def fzero_def
by (simp add: coerce_simp)

abbreviation mzero :: "'a⋅'m::monad_zero"
  where "mzero ≡ fzero"

lemmas mzero_def = fzero_def [where 'f="'m::monad_zero"] for f
lemmas fmap_mzero = fmap_fzero [where 'f="'m::monad_zero"] for f

lemma bindU_eq_bind: "bindU = bind"
unfolding bind_def by simp

lemma bind_mzero:
  "bind⋅(fzero :: 'a⋅'m::monad_zero)⋅k = (mzero :: 'b⋅'m)"
unfolding bind_def mzero_def
by (simp add: coerce_simp bindU_zeroU)

end