Theory Maybe

(*<*)
(*
 * 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
Maybe› 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