Quelle  Maybe.thy

(*<*)
(*
 * The Maybe monad.
 * (C)opyright 2009-2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory Maybe
imports HOLCF
begin
(*>*)

section‹The ‹'a Maybe› Monad›

text‹This section defines the monadic machinery for the ‹'a
 › type. @{term "return"} is @{term "Just"}.›

domain 'a Maybe = Nothing | Just (lazy "'a")

definition
  mfail :: "'a Maybe"
where
  "mfail ≡ Nothing"

definition
  mcatch :: "'a Maybe → 'a Maybe → 'a Maybe"
where
  "mcatch ≡ Λ body handler. case body of Nothing ==> handler | Just⋅x ==> Just⋅x"

lemma mcatch_strict[simp]: "mcatch⋅⊥ = ⊥"
  by (rule cfun_eqI, simp add: mcatch_def)

definition
  mbind :: "'a Maybe → ('a → 'b Maybe) → 'b Maybe" where
  "mbind ≡ Λ f g. (case f of Nothing ==> Nothing | Just⋅f' ==> g⋅f')"

abbreviation
  mbind_syn :: "'a Maybe ==> ('a → 'b Maybe) ==> 'b Maybe" (infixl ‹>>=_M› 55) where
  "f >>=_M g ≡ mbind⋅f⋅g"

lemma mbind_strict1[simp]: "⊥ >>=_M g = ⊥" by (simp add: mbind_def)

text‹The standard monad laws.›

lemma leftID[simp]: "Just⋅a >>=_M f = f⋅a" by (simp add: mbind_def)
lemma rightID[simp]: "m >>=_M Just = m" by (cases m, simp_all add: mbind_def)

lemma assoc[simp]: "(m >>=_M f) >>=_M g = m >>=_M (Λ x. f⋅x >>=_M g)"
  by (cases m, simp_all add: mbind_def)

text‹Reduction for the Maybe monad.›

lemma nothing_bind[simp]: "Nothing >>=_M f = Nothing" by (simp add: mbind_def)
lemma just_bind[simp]: "Just⋅x >>=_M f = f⋅x" by (simp add: mbind_def)

definition
  mliftM2 :: "('a → 'b → 'c) ==> 'a Maybe → 'b Maybe → 'c Maybe" where
  "mliftM2 f ≡ Λ x y. x >>=_M (Λ x'. y >>=_M (Λ y'. Just⋅(f⋅x'⋅y')))"

lemma mliftM2_Nothing1[simp]: "mliftM2 f⋅Nothing⋅y = Nothing" by (simp add: mliftM2_def)
lemma mliftM2_Nothing2[simp]: "mliftM2 f⋅(Just⋅x)⋅Nothing = Nothing" by (simp add: mliftM2_def)
lemma mliftM2_op[simp]: "mliftM2 f⋅(Just⋅x)⋅(Just⋅y) = Just⋅(f⋅x⋅y)" by (simp add: mliftM2_def)

lemma mliftM2_strict1[simp]: "mliftM2 f⋅⊥ = ⊥" by (rule cfun_eqI)+ (simp add: mliftM2_def)
lemma mliftM2_strict2[simp]: "mliftM2 f⋅(Just⋅x)⋅⊥ = ⊥" by (simp add: mliftM2_def)

end