Theory Writer_Transformer

section ‹Writer monad transformer›

theory Writer_Transformer
imports Writer_Monad
begin

subsection ‹Type definition›

text ‹Below is the standard Haskell definition of a writer monad
transformer:›

text_raw ‹
\begin{verbatim}
newtype WriterT w m a = WriterT { runWriterT :: m (a, w) }
\end{verbatim}
›

text ‹In this development, since a lazy pair type is not pre-defined
in HOLCF, we will use an equivalent formulation in terms of our
previous \texttt{Writer} type:›

text_raw ‹
\begin{verbatim}
data Writer w a = Writer w a
newtype WriterT w m a = WriterT { runWriterT :: m (Writer w a) }
\end{verbatim}
›

text ‹We can translate this definition directly into HOLCF using
‹tycondef›. \medskip›

tycondef 'a⋅('m::"functor",'w) writerT =
  WriterT (runWriterT :: "('a⋅'w writer)⋅'m")

lemma coerce_writerT_abs [simp]:
  "coerce⋅(writerT_abs⋅x) = writerT_abs⋅(coerce⋅x)"
apply (simp add: writerT_abs_def coerce_def)
apply (simp add: emb_prj_emb prj_emb_prj DEFL_eq_writerT)
done

lemma coerce_WriterT [simp]: "coerce⋅(WriterT⋅k) = WriterT⋅(coerce⋅k)"
unfolding WriterT_def by simp

lemma writerT_cases [case_names WriterT]:
  obtains k where "y = WriterT⋅k"
proof
  show "y = WriterT⋅(runWriterT⋅y)"
    by (cases y, simp_all)
qed

lemma WriterT_runWriterT [simp]: "WriterT⋅(runWriterT⋅m) = m"
by (cases m rule: writerT_cases, simp)

lemma writerT_induct [case_names WriterT]:
  fixes P :: "'a⋅('f::functor,'e) writerT ⇒ bool"
  assumes "⋀k. P (WriterT⋅k)"
  shows "P y"
by (cases y rule: writerT_cases, simp add: assms)

lemma writerT_eq_iff:
  "a = b ⟷ runWriterT⋅a = runWriterT⋅b"
apply (cases a rule: writerT_cases)
apply (cases b rule: writerT_cases)
apply simp
done

lemma writerT_below_iff:
  "a ⊑ b ⟷ runWriterT⋅a ⊑ runWriterT⋅b"
apply (cases a rule: writerT_cases)
apply (cases b rule: writerT_cases)
apply simp
done

lemma writerT_eqI:
  "runWriterT⋅a = runWriterT⋅b ⟹ a = b"
by (simp add: writerT_eq_iff)

lemma writerT_belowI:
  "runWriterT⋅a ⊑ runWriterT⋅b ⟹ a ⊑ b"
by (simp add: writerT_below_iff)

lemma runWriterT_coerce [simp]:
  "runWriterT⋅(coerce⋅k) = coerce⋅(runWriterT⋅k)"
by (induct k rule: writerT_induct, simp)

subsection ‹Functor class instance›

lemma fmap_writer_def: "fmap = writer_map⋅ID"
apply (rule cfun_eqI, rename_tac f)
apply (rule cfun_eqI, rename_tac x)
apply (case_tac x rule: writer.exhaust, simp_all)
apply (simp add: writer_map_def fix_const)
apply (simp add: writer_map_def fix_const Writer_def)
done

lemma fmapU_WriterT [simp]:
  "fmapU⋅f⋅(WriterT⋅m) = WriterT⋅(fmap⋅(fmap⋅f)⋅m)"
unfolding fmapU_writerT_def writerT_map_def fmap_writer_def fix_const
  WriterT_def by simp

lemma runWriterT_fmapU [simp]:
  "runWriterT⋅(fmapU⋅f⋅m) = fmap⋅(fmap⋅f)⋅(runWriterT⋅m)"
by (induct m rule: writerT_induct) simp

instance writerT :: ("functor", "domain") "functor"
proof
  fix f g :: "udom → udom" and xs :: "udom⋅('a,'b) writerT"
  show "fmapU⋅f⋅(fmapU⋅g⋅xs) = fmapU⋅(Λ x. f⋅(g⋅x))⋅xs"
    apply (induct xs rule: writerT_induct)
    apply (simp add: fmap_fmap eta_cfun)
    done
qed

subsection ‹Monad operations›

text ‹The writer monad transformer does not yield a monad in the
usual sense: We cannot prove a ‹monad› class instance, because
type ‹'a⋅('m,'w) writerT› contains values that break the monad
laws. However, it turns out that such values are inaccessible: The
monad laws are satisfied by all values constructible from the abstract
operations.›

text ‹To explore the properties of the writer monad transformer
operations, we define them all as non-overloaded functions. \medskip
›

definition unitWT :: "'a → 'a⋅('m::monad,'w::monoid) writerT"
  where "unitWT = (Λ x. WriterT⋅(return⋅(Writer⋅mempty⋅x)))"

definition bindWT :: "'a⋅('m::monad,'w::monoid) writerT → ('a → 'b⋅('m,'w) writerT) → 'b⋅('m,'w) writerT"
  where "bindWT = (Λ m k. WriterT⋅(bind⋅(runWriterT⋅m)⋅
    (Λ(Writer⋅w⋅x). bind⋅(runWriterT⋅(k⋅x))⋅(Λ(Writer⋅w'⋅y).
      return⋅(Writer⋅(mappend⋅w⋅w')⋅y)))))"

definition liftWT :: "'a⋅'m → 'a⋅('m::monad,'w::monoid) writerT"
  where "liftWT = (Λ m. WriterT⋅(fmap⋅(Writer⋅mempty)⋅m))"

definition tellWT :: "'a → 'w → 'a⋅('m::monad,'w::monoid) writerT"
  where "tellWT = (Λ x w. WriterT⋅(return⋅(Writer⋅w⋅x)))"

definition fmapWT :: "('a → 'b) → 'a⋅('m::monad,'w::monoid) writerT → 'b⋅('m,'w) writerT"
  where "fmapWT = (Λ f m. bindWT⋅m⋅(Λ x. unitWT⋅(f⋅x)))"

lemma runWriterT_fmap [simp]:
  "runWriterT⋅(fmap⋅f⋅m) = fmap⋅(fmap⋅f)⋅(runWriterT⋅m)"
by (subst fmap_def, simp add: coerce_simp eta_cfun)

lemma runWriterT_unitWT [simp]:
  "runWriterT⋅(unitWT⋅x) = return⋅(Writer⋅mempty⋅x)"
unfolding unitWT_def by simp

lemma runWriterT_bindWT [simp]:
  "runWriterT⋅(bindWT⋅m⋅k) = bind⋅(runWriterT⋅m)⋅
    (Λ(Writer⋅w⋅x). bind⋅(runWriterT⋅(k⋅x))⋅(Λ(Writer⋅w'⋅y).
      return⋅(Writer⋅(mappend⋅w⋅w')⋅y)))"
unfolding bindWT_def by simp

lemma runWriterT_liftWT [simp]:
  "runWriterT⋅(liftWT⋅m) = fmap⋅(Writer⋅mempty)⋅m"
unfolding liftWT_def by simp

lemma runWriterT_tellWT [simp]:
  "runWriterT⋅(tellWT⋅x⋅w) = return⋅(Writer⋅w⋅x)"
unfolding tellWT_def by simp

lemma runWriterT_fmapWT [simp]:
  "runWriterT⋅(fmapWT⋅f⋅m) =
    runWriterT⋅m ⤜ (Λ (Writer⋅w⋅x). return⋅(Writer⋅w⋅(f⋅x)))"
by (simp add: fmapWT_def bindWT_def mempty_right)

subsection ‹Laws›

text ‹The ‹liftWT› function maps ‹return› and
‹bind› on the inner monad to ‹unitWT› and ‹bindWT›, as expected. \medskip›

lemma liftWT_return:
  "liftWT⋅(return⋅x) = unitWT⋅x"
by (rule writerT_eqI, simp add: fmap_return)

lemma liftWT_bind:
  "liftWT⋅(bind⋅m⋅k) = bindWT⋅(liftWT⋅m)⋅(liftWT oo k)"
by (rule writerT_eqI)
   (simp add: monad_fmap bind_bind mempty_left)

text ‹The composition rule holds unconditionally for fmap. The fmap
function also interacts as expected with unit and bind. \medskip›

lemma fmapWT_fmapWT:
  "fmapWT⋅f⋅(fmapWT⋅g⋅m) = fmapWT⋅(Λ x. f⋅(g⋅x))⋅m"
apply (simp add: writerT_eq_iff bind_bind)
apply (rule cfun_arg_cong, rule cfun_eqI, simp)
apply (case_tac x, simp add: bind_strict, simp add: mempty_right)
done

lemma fmapWT_unitWT:
  "fmapWT⋅f⋅(unitWT⋅x) = unitWT⋅(f⋅x)"
by (simp add: writerT_eq_iff mempty_right)

lemma fmapWT_bindWT:
  "fmapWT⋅f⋅(bindWT⋅m⋅k) = bindWT⋅m⋅(Λ x. fmapWT⋅f⋅(k⋅x))"
apply (simp add: writerT_eq_iff bind_bind)
apply (rule cfun_arg_cong, rule cfun_eqI, rename_tac x, simp)
apply (case_tac x, simp add: bind_strict, simp add: bind_bind)
apply (rule cfun_arg_cong, rule cfun_eqI, rename_tac y, simp)
apply (case_tac y, simp add: bind_strict, simp add: mempty_right)
done

lemma bindWT_fmapWT:
  "bindWT⋅(fmapWT⋅f⋅m)⋅k = bindWT⋅m⋅(Λ x. k⋅(f⋅x))"
apply (simp add: writerT_eq_iff bind_bind)
apply (rule cfun_arg_cong, rule cfun_eqI, rename_tac x, simp)
apply (case_tac x, simp add: bind_strict, simp add: mempty_right)
done

text ‹The left unit monad law is not satisfied in general. \medskip›

lemma bindWT_unitWT_counterexample:
  fixes k :: "'a → 'b⋅('m::monad,'w::monoid) writerT"
  assumes 1: "k⋅x = WriterT⋅(return⋅⊥)"
  assumes 2: "return⋅⊥ ≠ (⊥ :: ('b⋅'w writer)⋅'m::monad)"
  shows "bindWT⋅(unitWT⋅x)⋅k ≠ k⋅x"
by (simp add: writerT_eq_iff mempty_left assms)

text ‹However, left unit is satisfied for inner monads with a strict
‹return› function.›

lemma bindWT_unitWT_restricted:
  fixes k :: "'a → 'b⋅('m::monad,'w::monoid) writerT"
  assumes "return⋅⊥ = (⊥ :: ('b⋅'w writer)⋅'m)"
  shows "bindWT⋅(unitWT⋅x)⋅k = k⋅x"
unfolding writerT_eq_iff
apply (simp add: mempty_left)
apply (rule trans [OF _ monad_right_unit])
apply (rule cfun_arg_cong)
apply (rule cfun_eqI)
apply (case_tac x, simp_all add: assms)
done

text ‹The associativity of ‹bindWT› holds
unconditionally. \medskip›

lemma bindWT_bindWT:
  "bindWT⋅(bindWT⋅m⋅h)⋅k = bindWT⋅m⋅(Λ x. bindWT⋅(h⋅x)⋅k)"
apply (rule writerT_eqI)
apply simp
apply (simp add: bind_bind)
apply (rule cfun_arg_cong)
apply (rule cfun_eqI, simp)
apply (case_tac x)
apply (simp add: bind_strict)
apply (simp add: bind_bind)
apply (rule cfun_arg_cong)
apply (rule cfun_eqI, simp, rename_tac y)
apply (case_tac y)
apply (simp add: bind_strict)
apply (simp add: bind_bind)
apply (rule cfun_arg_cong)
apply (rule cfun_eqI, simp, rename_tac z)
apply (case_tac z)
apply (simp add: bind_strict)
apply (simp add: mappend_assoc)
done

text ‹The right unit monad law is not satisfied in general. \medskip›

lemma bindWT_unitWT_right_counterexample:
  fixes m :: "'a⋅('m::monad,'w::monoid) writerT"
  assumes "m = WriterT⋅(return⋅⊥)"
  assumes "return⋅⊥ ≠ (⊥ :: ('a⋅'w writer)⋅'m)"
  shows "bindWT⋅m⋅unitWT ≠ m"
by (simp add: writerT_eq_iff assms)

text ‹Right unit is satisfied for inner monads with a strict ‹return› function. \medskip›

lemma bindWT_unitWT_right_restricted:
  fixes m :: "'a⋅('m::monad,'w::monoid) writerT"
  assumes "return⋅⊥ = (⊥ :: ('a⋅'w writer)⋅'m)"
  shows "bindWT⋅m⋅unitWT = m"
unfolding writerT_eq_iff
apply simp
apply (rule trans [OF _ monad_right_unit])
apply (rule cfun_arg_cong)
apply (rule cfun_eqI)
apply (case_tac x, simp_all add: assms mempty_right)
done

subsection ‹Writer monad transformer invariant›

text ‹We inductively define a predicate that includes all values
that can be constructed from the standard ‹writerT› operations.
\medskip›

inductive invar :: "'a⋅('m::monad, 'w::monoid) writerT ⇒ bool"
  where invar_bottom: "invar ⊥"
  | invar_lub: "⋀Y. ⟦chain Y; ⋀i. invar (Y i)⟧ ⟹ invar (⨆i. Y i)"
  | invar_unitWT: "⋀x. invar (unitWT⋅x)"
  | invar_bindWT: "⋀m k. ⟦invar m; ⋀x. invar (k⋅x)⟧ ⟹ invar (bindWT⋅m⋅k)"
  | invar_tellWT: "⋀x w. invar (tellWT⋅x⋅w)"
  | invar_liftWT: "⋀m. invar (liftWT⋅m)"

text ‹Right unit is satisfied for arguments built from standard
functions. \medskip›

lemma bindWT_unitWT_right_invar:
  fixes m :: "'a⋅('m::monad,'w::monoid) writerT"
  assumes "invar m"
  shows "bindWT⋅m⋅unitWT = m"
using assms proof (induct set: invar)
  case invar_bottom thus ?case
    by (rule writerT_eqI, simp add: bind_strict)
next
  case invar_lub thus ?case
    by - (rule admD, simp, assumption, assumption)
next
  case invar_unitWT thus ?case
    by (rule writerT_eqI, simp add: bind_bind mempty_left)
next
  case invar_bindWT thus ?case
    apply (simp add: writerT_eq_iff bind_bind)
    apply (rule cfun_arg_cong, rule cfun_eqI, simp)
    apply (case_tac x, simp add: bind_strict, simp add: bind_bind)
    apply (rule cfun_arg_cong, rule cfun_eqI, simp, rename_tac y)
    apply (case_tac y, simp add: bind_strict, simp add: mempty_right)
    done
next
  case invar_tellWT thus ?case
    by (simp add: writerT_eq_iff mempty_right)
next
  case invar_liftWT thus ?case
    by (rule writerT_eqI, simp add: monad_fmap bind_bind mempty_right)
qed

text ‹Left unit is also satisfied for arguments built from standard
functions. \medskip›

lemma writerT_left_unit_invar_lemma:
  assumes "invar m"
  shows "runWriterT⋅m ⤜ (Λ (Writer⋅w⋅x). return⋅(Writer⋅w⋅x)) = runWriterT⋅m"
using assms proof (induct m set: invar)
  case invar_bottom thus ?case
    by (simp add: bind_strict)
next
  case invar_lub thus ?case
    by - (rule admD, simp, assumption, assumption)
next
  case invar_unitWT thus ?case
    by simp
next
  case invar_bindWT thus ?case
    apply (simp add: bind_bind)
    apply (rule cfun_arg_cong)
    apply (rule cfun_eqI, simp, rename_tac n)
    apply (case_tac n, simp add: bind_strict)
    apply (simp add: bind_bind)
    apply (rule cfun_arg_cong)
    apply (rule cfun_eqI, simp, rename_tac p)
    apply (case_tac p, simp add: bind_strict)
    apply simp
    done
next
  case invar_tellWT thus ?case
    by simp
next
  case invar_liftWT thus ?case
    by (simp add: monad_fmap bind_bind)
qed

lemma bindWT_unitWT_invar:
  assumes "invar (k⋅x)"
  shows "bindWT⋅(unitWT⋅x)⋅k = k⋅x"
apply (simp add: writerT_eq_iff mempty_left)
apply (rule writerT_left_unit_invar_lemma [OF assms])
done

subsection ‹Invariant expressed as a deflation›

definition invar' :: "'a⋅('m::monad, 'w::monoid) writerT ⇒ bool"
  where "invar' m ⟷ fmapWT⋅ID⋅m = m"

text ‹All standard operations preserve the invariant.›

lemma invar'_bottom: "invar' ⊥"
  unfolding invar'_def by (simp add: writerT_eq_iff bind_strict)

lemma adm_invar': "adm invar'"
  unfolding invar'_def [abs_def] by simp

lemma invar'_unitWT: "invar' (unitWT⋅x)"
  unfolding invar'_def by (simp add: writerT_eq_iff)

lemma invar'_bindWT: "⟦invar' m; ⋀x. invar' (k⋅x)⟧ ⟹ invar' (bindWT⋅m⋅k)"
  unfolding invar'_def
  apply (erule subst)
  apply (simp add: writerT_eq_iff)
  apply (simp add: bind_bind)
  apply (rule cfun_arg_cong)
  apply (rule cfun_eqI, case_tac x)
  apply (simp add: bind_strict)
  apply simp
  apply (simp add: bind_bind)
  apply (rule cfun_arg_cong)
  apply (rule cfun_eqI, rename_tac x, case_tac x)
  apply (simp add: bind_strict)
  apply simp
  done

lemma invar'_tellWT: "invar' (tellWT⋅x⋅w)"
  unfolding invar'_def by (simp add: writerT_eq_iff)

lemma invar'_liftWT: "invar' (liftWT⋅m)"
  unfolding invar'_def by (simp add: writerT_eq_iff monad_fmap bind_bind)

text ‹Left unit is satisfied for arguments built from fmap.›

lemma bindWT_unitWT_fmapWT:
  "bindWT⋅(unitWT⋅x)⋅(Λ x. fmapWT⋅f⋅(k⋅x))
    = fmapWT⋅f⋅(k⋅x)"
apply (simp add: fmapWT_def writerT_eq_iff bind_bind)
apply (rule cfun_arg_cong, rule cfun_eqI, simp)
apply (case_tac x, simp_all add: bind_strict mempty_left)
done

text ‹Right unit is satisfied for arguments built from fmap.›

lemma bindWT_fmapWT_unitWT:
  shows "bindWT⋅(fmapWT⋅f⋅m)⋅unitWT = fmapWT⋅f⋅m"
apply (simp add: bindWT_fmapWT)
apply (simp add: fmapWT_def)
done

text ‹All monad laws are preserved by values satisfying the invariant.›

lemma invar'_right_unit: "invar' m ⟹ bindWT⋅m⋅unitWT = m"
unfolding invar'_def by (erule subst, rule bindWT_fmapWT_unitWT)

lemma invar'_monad_fmap:
  "invar' m ⟹ fmapWT⋅f⋅m = bindWT⋅m⋅(Λ x. unitWT⋅(f⋅x))"
  unfolding invar'_def
  by (erule subst, simp add: writerT_eq_iff mempty_right)

lemma invar'_bind_assoc:
  "⟦invar' m; ⋀x. invar' (f⋅x); ⋀y. invar' (g⋅y)⟧
    ⟹ bindWT⋅(bindWT⋅m⋅f)⋅g = bindWT⋅m⋅(Λ x. bindWT⋅(f⋅x)⋅g)"
  by (rule bindWT_bindWT)

end