Theory Lazy_List_Monad

section ‹Lazy list monad›

theory Lazy_List_Monad
imports Monad_Zero_Plus
begin

text ‹To illustrate the general process of defining a new type
constructor, we formalize the datatype of lazy lists. Below are the
Haskell datatype definition and class instances.›

text_raw ‹
\begin{verbatim}
data List a = Nil | Cons a (List a)

instance Functor List where
  fmap f Nil = Nil
  fmap f (Cons x xs) = Cons (f x) (fmap f xs)

instance Monad List where
  return x        = Cons x Nil
  Nil       >>= k = Nil
  Cons x xs >>= k = mplus (k x) (xs >>= k)

instance MonadZero List where
  mzero = Nil

instance MonadPlus List where
  mplus Nil         ys = ys
  mplus (Cons x xs) ys = Cons x (mplus xs ys)
\end{verbatim}
›

subsection ‹Type definition›

text ‹The first step is to register the datatype definition with
‹tycondef›.›

tycondef 'a⋅llist = LNil | LCons (lazy "'a") (lazy "'a⋅llist")

text ‹The ‹tycondef› command generates lots of theorems
automatically, but there are a few more involving ‹coerce› and
‹fmapU› that we still need to prove manually. These proofs could
be automated in a later version of ‹tycondef›.›

lemma coerce_llist_abs [simp]: "coerce⋅(llist_abs⋅x) = llist_abs⋅(coerce⋅x)"
apply (simp add: llist_abs_def coerce_def)
apply (simp add: emb_prj_emb prj_emb_prj DEFL_eq_llist)
done

lemma coerce_LNil [simp]: "coerce⋅LNil = LNil"
unfolding LNil_def by simp

lemma coerce_LCons [simp]: "coerce⋅(LCons⋅x⋅xs) = LCons⋅(coerce⋅x)⋅(coerce⋅xs)"
unfolding LCons_def by simp

lemma fmapU_llist_simps [simp]:
  "fmapU⋅f⋅(⊥::udom⋅llist) = ⊥"
  "fmapU⋅f⋅LNil = LNil"
  "fmapU⋅f⋅(LCons⋅x⋅xs) = LCons⋅(f⋅x)⋅(fmapU⋅f⋅xs)"
unfolding fmapU_llist_def llist_map_def
apply (subst fix_eq, simp)
apply (subst fix_eq, simp add: LNil_def)
apply (subst fix_eq, simp add: LCons_def)
done

subsection ‹Class instances›

text ‹The ‹tycondef› command defines ‹fmapU› for us and
proves a ‹prefunctor› class instance automatically. For the
‹functor› instance we only need to prove the composition law,
which we can do by induction.›

instance llist :: "functor"
proof
  fix f g and xs :: "udom⋅llist"
  show "fmapU⋅f⋅(fmapU⋅g⋅xs) = fmapU⋅(Λ x. f⋅(g⋅x))⋅xs"
    by (induct xs rule: llist.induct) simp_all
qed

text ‹For the other class instances, we need to provide definitions
for a few constants: ‹returnU›, ‹bindU› ‹zeroU›, and
‹plusU›. We can use ordinary commands like ‹definition›
and ‹fixrec› for this purpose. Finally we prove the class
axioms, along with a few helper lemmas, using ordinary proof
procedures like induction.›

instantiation llist :: monad_zero_plus
begin

fixrec plusU_llist :: "udom⋅llist → udom⋅llist → udom⋅llist"
  where "plusU_llist⋅LNil⋅ys = ys"
  | "plusU_llist⋅(LCons⋅x⋅xs)⋅ys = LCons⋅x⋅(plusU_llist⋅xs⋅ys)"

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

fixrec bindU_llist :: "udom⋅llist → (udom → udom⋅llist) → udom⋅llist"
  where "bindU_llist⋅LNil⋅k = LNil"
  | "bindU_llist⋅(LCons⋅x⋅xs)⋅k = plusU⋅(k⋅x)⋅(bindU_llist⋅xs⋅k)"

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

definition zeroU_llist_def:
  "zeroU = LNil"

definition returnU_llist_def:
  "returnU = (Λ x. LCons⋅x⋅LNil)"

lemma plusU_LNil_right: "plusU⋅xs⋅LNil = xs"
by (induct xs rule: llist.induct) simp_all

lemma plusU_llist_assoc:
  fixes xs ys zs :: "udom⋅llist"
  shows "plusU⋅(plusU⋅xs⋅ys)⋅zs = plusU⋅xs⋅(plusU⋅ys⋅zs)"
by (induct xs rule: llist.induct) simp_all

lemma bindU_plusU_llist:
  fixes xs ys :: "udom⋅llist" shows
  "bindU⋅(plusU⋅xs⋅ys)⋅f = plusU⋅(bindU⋅xs⋅f)⋅(bindU⋅ys⋅f)"
by (induct xs rule: llist.induct) (simp_all add: plusU_llist_assoc)

instance proof
  fix x :: "udom"
  fix f :: "udom → udom"
  fix h k :: "udom → udom⋅llist"
  fix xs ys zs :: "udom⋅llist"
  show "fmapU⋅f⋅xs = bindU⋅xs⋅(Λ x. returnU⋅(f⋅x))"
    by (induct xs rule: llist.induct, simp_all add: returnU_llist_def)
  show "bindU⋅(returnU⋅x)⋅k = k⋅x"
    by (simp add: returnU_llist_def plusU_LNil_right)
  show "bindU⋅(bindU⋅xs⋅h)⋅k = bindU⋅xs⋅(Λ x. bindU⋅(h⋅x)⋅k)"
    by (induct xs rule: llist.induct)
       (simp_all add: bindU_plusU_llist)
  show "bindU⋅(plusU⋅xs⋅ys)⋅k = plusU⋅(bindU⋅xs⋅k)⋅(bindU⋅ys⋅k)"
    by (induct xs rule: llist.induct)
       (simp_all add: plusU_llist_assoc)
  show "plusU⋅(plusU⋅xs⋅ys)⋅zs = plusU⋅xs⋅(plusU⋅ys⋅zs)"
    by (rule plusU_llist_assoc)
  show "bindU⋅zeroU⋅k = zeroU"
    by (simp add: zeroU_llist_def)
  show "fmapU⋅f⋅(plusU⋅xs⋅ys) = plusU⋅(fmapU⋅f⋅xs)⋅(fmapU⋅f⋅ys)"
    by (induct xs rule: llist.induct) simp_all
  show "fmapU⋅f⋅zeroU = (zeroU :: udom⋅llist)"
    by (simp add: zeroU_llist_def)
  show "plusU⋅zeroU⋅xs = xs"
    by (simp add: zeroU_llist_def)
  show "plusU⋅xs⋅zeroU = xs"
    by (simp add: zeroU_llist_def plusU_LNil_right)
qed

end

subsection ‹Transfer properties to polymorphic versions›

text ‹After proving the class instances, there is still one more
step: We must transfer all the list-specific lemmas about the
monomorphic constants (e.g., ‹fmapU› and ‹bindU›) to the
corresponding polymorphic constants (‹fmap› and ‹bind›).
These lemmas primarily consist of the defining equations for each
constant. The polymorphic constants are defined using ‹coerce›,
so the proofs proceed by unfolding the definitions and simplifying
with the ‹coerce_simp› rules.›

lemma fmap_llist_simps [simp]:
  "fmap⋅f⋅(⊥::'a⋅llist) = ⊥"
  "fmap⋅f⋅LNil = LNil"
  "fmap⋅f⋅(LCons⋅x⋅xs) = LCons⋅(f⋅x)⋅(fmap⋅f⋅xs)"
unfolding fmap_def by simp_all

lemma mplus_llist_simps [simp]:
  "mplus⋅(⊥::'a⋅llist)⋅ys = ⊥"
  "mplus⋅LNil⋅ys = ys"
  "mplus⋅(LCons⋅x⋅xs)⋅ys = LCons⋅x⋅(mplus⋅xs⋅ys)"
unfolding mplus_def by simp_all

lemma bind_llist_simps [simp]:
  "bind⋅(⊥::'a⋅llist)⋅f = ⊥"
  "bind⋅LNil⋅f = LNil"
  "bind⋅(LCons⋅x⋅xs)⋅f = mplus⋅(f⋅x)⋅(bind⋅xs⋅f)"
unfolding bind_def mplus_def
by (simp_all add: coerce_simp)

lemma return_llist_def:
  "return = (Λ x. LCons⋅x⋅LNil)"
unfolding return_def returnU_llist_def
by (simp add: coerce_simp)

lemma mzero_llist_def:
  "mzero = LNil"
unfolding mzero_def zeroU_llist_def
by simp

lemma join_llist_simps [simp]:
  "join⋅(⊥::'a⋅llist⋅llist) = ⊥"
  "join⋅LNil = LNil"
  "join⋅(LCons⋅xs⋅xss) = mplus⋅xs⋅(join⋅xss)"
unfolding join_def by simp_all

end