Theory Error_Monad

section ‹Error monad›

theory Error_Monad
imports Monad_Plus
begin

subsection ‹Type definition›

tycondef 'a⋅'e error = Err (lazy "'e") | Ok (lazy "'a")

lemma coerce_error_abs [simp]: "coerce⋅(error_abs⋅x) = error_abs⋅(coerce⋅x)"
apply (simp add: error_abs_def coerce_def)
apply (simp add: emb_prj_emb prj_emb_prj DEFL_eq_error)
done

lemma coerce_Err [simp]: "coerce⋅(Err⋅x) = Err⋅(coerce⋅x)"
unfolding Err_def by simp

lemma coerce_Ok [simp]: "coerce⋅(Ok⋅m) = Ok⋅(coerce⋅m)"
unfolding Ok_def by simp

lemma fmapU_error_simps [simp]:
  "fmapU⋅f⋅(⊥::udom⋅'a error) = ⊥"
  "fmapU⋅f⋅(Err⋅e) = Err⋅e"
  "fmapU⋅f⋅(Ok⋅x) = Ok⋅(f⋅x)"
unfolding fmapU_error_def error_map_def fix_const
apply simp
apply (simp add: Err_def)
apply (simp add: Ok_def)
done

subsection ‹Monad class instance›

instantiation error :: ("domain") "{monad, functor_plus}"
begin

definition
  "returnU = Ok"

fixrec bindU_error :: "udom⋅'a error → (udom → udom⋅'a error) → udom⋅'a error"
  where "bindU_error⋅(Err⋅e)⋅f = Err⋅e"
  | "bindU_error⋅(Ok⋅x)⋅f = f⋅x"

lemma bindU_error_strict [simp]: "bindU⋅⊥⋅k = (⊥::udom⋅'a error)"
by fixrec_simp

fixrec plusU_error :: "udom⋅'a error → udom⋅'a error → udom⋅'a error"
  where "plusU_error⋅(Err⋅e)⋅f = f"
  | "plusU_error⋅(Ok⋅x)⋅f = Ok⋅x"

lemma plusU_error_strict [simp]: "plusU⋅(⊥ :: udom⋅'a error) = ⊥"
by fixrec_simp

instance proof
  fix f g :: "udom → udom" and r :: "udom⋅'a error"
  show "fmapU⋅f⋅(fmapU⋅g⋅r) = fmapU⋅(Λ x. f⋅(g⋅x))⋅r"
    by (induct r rule: error.induct) simp_all
next
  fix f :: "udom → udom" and r :: "udom⋅'a error"
  show "fmapU⋅f⋅r = bindU⋅r⋅(Λ x. returnU⋅(f⋅x))"
    by (induct r rule: error.induct)
       (simp_all add: returnU_error_def)
next
  fix f :: "udom → udom⋅'a error" and x :: "udom"
  show "bindU⋅(returnU⋅x)⋅f = f⋅x"
    by (simp add: returnU_error_def)
next
  fix r :: "udom⋅'a error" and f g :: "udom → udom⋅'a error"
  show "bindU⋅(bindU⋅r⋅f)⋅g = bindU⋅r⋅(Λ x. bindU⋅(f⋅x)⋅g)"
    by (induct r rule: error.induct)
       simp_all
next
  fix f :: "udom → udom" and a b :: "udom⋅'a error"
  show "fmapU⋅f⋅(plusU⋅a⋅b) = plusU⋅(fmapU⋅f⋅a)⋅(fmapU⋅f⋅b)"
    by (induct a rule: error.induct) simp_all
next
  fix a b c :: "udom⋅'a error"
  show "plusU⋅(plusU⋅a⋅b)⋅c = plusU⋅a⋅(plusU⋅b⋅c)"
    by (induct a rule: error.induct) simp_all
qed

end

subsection ‹Transfer properties to polymorphic versions›

lemma fmap_error_simps [simp]:
  "fmap⋅f⋅(⊥::'a⋅'e error) = ⊥"
  "fmap⋅f⋅(Err⋅e :: 'a⋅'e error) = Err⋅e"
  "fmap⋅f⋅(Ok⋅x :: 'a⋅'e error) = Ok⋅(f⋅x)"
unfolding fmap_def [where 'f="'e error"]
by (simp_all add: coerce_simp)

lemma return_error_def: "return = Ok"
unfolding return_def returnU_error_def
by (simp add: coerce_simp eta_cfun)

lemma bind_error_simps [simp]:
  "bind⋅(⊥ :: 'a⋅'e error)⋅f = ⊥"
  "bind⋅(Err⋅e :: 'a⋅'e error)⋅f = Err⋅e"
  "bind⋅(Ok⋅x :: 'a⋅'e error)⋅f = f⋅x"
unfolding bind_def
by (simp_all add: coerce_simp)

lemma join_error_simps [simp]:
  "join⋅⊥ = (⊥ :: 'a⋅'e error)"
  "join⋅(Err⋅e) = Err⋅e"
  "join⋅(Ok⋅x) = x"
unfolding join_def by simp_all

lemma fplus_error_simps [simp]:
  "fplus⋅⊥⋅r = (⊥ :: 'a⋅'e error)"
  "fplus⋅(Err⋅e)⋅r = r"
  "fplus⋅(Ok⋅x)⋅r = Ok⋅x"
unfolding fplus_def
by (simp_all add: coerce_simp)

end