Theory Maybe_Monad

section ‹Maybe monad›

theory Maybe_Monad
imports Monad_Zero_Plus
begin

subsection ‹Type definition›

tycondef 'a⋅maybe = Nothing | Just (lazy "'a")

lemma coerce_maybe_abs [simp]: "coerce⋅(maybe_abs⋅x) = maybe_abs⋅(coerce⋅x)"
apply (simp add: maybe_abs_def coerce_def)
apply (simp add: emb_prj_emb prj_emb_prj DEFL_eq_maybe)
done

lemma coerce_Nothing [simp]: "coerce⋅Nothing = Nothing"
unfolding Nothing_def by simp

lemma coerce_Just [simp]: "coerce⋅(Just⋅x) = Just⋅(coerce⋅x)"
unfolding Just_def by simp

lemma fmapU_maybe_simps [simp]:
  "fmapU⋅f⋅(⊥::udom⋅maybe) = ⊥"
  "fmapU⋅f⋅Nothing = Nothing"
  "fmapU⋅f⋅(Just⋅x) = Just⋅(f⋅x)"
unfolding fmapU_maybe_def maybe_map_def fix_const
apply simp
apply (simp add: Nothing_def)
apply (simp add: Just_def)
done

subsection ‹Class instance proofs›

instance maybe :: "functor"
apply standard
apply (induct_tac xs rule: maybe.induct, simp_all)
done

instantiation maybe :: "{functor_zero_plus, monad_zero}"
begin

fixrec plusU_maybe :: "udom⋅maybe → udom⋅maybe → udom⋅maybe"
  where "plusU_maybe⋅Nothing⋅ys = ys"
  | "plusU_maybe⋅(Just⋅x)⋅ys = Just⋅x"

lemma plusU_maybe_strict [simp]: "plusU⋅⊥⋅ys = (⊥::udom⋅maybe)"
by fixrec_simp

fixrec bindU_maybe :: "udom⋅maybe → (udom → udom⋅maybe) → udom⋅maybe"
  where "bindU_maybe⋅Nothing⋅k = Nothing"
  | "bindU_maybe⋅(Just⋅x)⋅k = k⋅x"

lemma bindU_maybe_strict [simp]: "bindU⋅⊥⋅k = (⊥::udom⋅maybe)"
by fixrec_simp

definition zeroU_maybe_def:
  "zeroU = Nothing"

definition returnU_maybe_def:
  "returnU = Just"

lemma plusU_Nothing_right: "plusU⋅xs⋅Nothing = xs"
by (induct xs rule: maybe.induct) simp_all

lemma bindU_plusU_maybe:
  fixes xs ys :: "udom⋅maybe" shows
  "bindU⋅(plusU⋅xs⋅ys)⋅f = plusU⋅(bindU⋅xs⋅f)⋅(bindU⋅ys⋅f)"
apply (induct xs rule: maybe.induct)
apply simp_all
oops

instance proof
  fix x :: "udom"
  fix f :: "udom → udom"
  fix h k :: "udom → udom⋅maybe"
  fix xs ys zs :: "udom⋅maybe"
  show "fmapU⋅f⋅xs = bindU⋅xs⋅(Λ x. returnU⋅(f⋅x))"
    by (induct xs rule: maybe.induct, simp_all add: returnU_maybe_def)
  show "bindU⋅(returnU⋅x)⋅k = k⋅x"
    by (simp add: returnU_maybe_def plusU_Nothing_right)
  show "bindU⋅(bindU⋅xs⋅h)⋅k = bindU⋅xs⋅(Λ x. bindU⋅(h⋅x)⋅k)"
    by (induct xs rule: maybe.induct) simp_all
  show "plusU⋅(plusU⋅xs⋅ys)⋅zs = plusU⋅xs⋅(plusU⋅ys⋅zs)"
    by (induct xs rule: maybe.induct) simp_all
  show "bindU⋅zeroU⋅k = zeroU"
    by (simp add: zeroU_maybe_def)
  show "fmapU⋅f⋅(plusU⋅xs⋅ys) = plusU⋅(fmapU⋅f⋅xs)⋅(fmapU⋅f⋅ys)"
    by (induct xs rule: maybe.induct) simp_all
  show "fmapU⋅f⋅zeroU = (zeroU :: udom⋅maybe)"
    by (simp add: zeroU_maybe_def)
  show "plusU⋅zeroU⋅xs = xs"
    by (simp add: zeroU_maybe_def)
  show "plusU⋅xs⋅zeroU = xs"
    by (simp add: zeroU_maybe_def plusU_Nothing_right)
qed

end

subsection ‹Transfer properties to polymorphic versions›

lemma fmap_maybe_simps [simp]:
  "fmap⋅f⋅(⊥::'a⋅maybe) = ⊥"
  "fmap⋅f⋅Nothing = Nothing"
  "fmap⋅f⋅(Just⋅x) = Just⋅(f⋅x)"
unfolding fmap_def by simp_all

lemma fplus_maybe_simps [simp]:
  "fplus⋅(⊥::'a⋅maybe)⋅ys = ⊥"
  "fplus⋅Nothing⋅ys = ys"
  "fplus⋅(Just⋅x)⋅ys = Just⋅x"
unfolding fplus_def by simp_all

lemma fplus_Nothing_right [simp]:
  "fplus⋅m⋅Nothing = m"
by (simp add: fplus_def plusU_Nothing_right)

lemma bind_maybe_simps [simp]:
  "bind⋅(⊥::'a⋅maybe)⋅f = ⊥"
  "bind⋅Nothing⋅f = Nothing"
  "bind⋅(Just⋅x)⋅f = f⋅x"
unfolding bind_def fplus_def by simp_all

lemma return_maybe_def: "return = Just"
unfolding return_def returnU_maybe_def
by (simp add: coerce_cfun cfcomp1 eta_cfun)

lemma mzero_maybe_def: "mzero = Nothing"
unfolding mzero_def zeroU_maybe_def
by simp

lemma join_maybe_simps [simp]:
  "join⋅(⊥::'a⋅maybe⋅maybe) = ⊥"
  "join⋅Nothing = Nothing"
  "join⋅(Just⋅xs) = xs"
unfolding join_def by simp_all

subsection ‹Maybe is not in ‹monad_plus››

text ‹
  The ‹maybe› type does not satisfy the law ‹bind_mplus›.
›

lemma maybe_counterexample1:
  "⟦a = Just⋅x; b = ⊥; k⋅x = Nothing⟧
    ⟹ fplus⋅a⋅b ⤜ k ≠ fplus⋅(a ⤜ k)⋅(b ⤜ k)"
by simp

lemma maybe_counterexample2:
  "⟦a = Just⋅x; b = Just⋅y; k⋅x = Nothing; k⋅y = Just⋅z⟧
    ⟹ fplus⋅a⋅b ⤜ k ≠ fplus⋅(a ⤜ k)⋅(b ⤜ k)"
by simp

end