Theory Resumption_Transformer

section ‹Resumption monad transformer›

theory Resumption_Transformer
imports Monad_Plus
begin

subsection ‹Type definition›

text ‹The standard Haskell libraries do not include a resumption
monad transformer type; below is the Haskell definition for the one we
will use here.›

text_raw ‹
\begin{verbatim}
data ResT m a = Done a | More (m (ResT m a))
\end{verbatim}
›

text ‹The above datatype definition can be translated directly into
HOLCF using ‹tycondef›. \medskip›

tycondef 'a⋅('f::"functor") resT =
  Done (lazy "'a") | More (lazy "('a⋅'f resT)⋅'f")

lemma coerce_resT_abs [simp]: "coerce⋅(resT_abs⋅x) = resT_abs⋅(coerce⋅x)"
apply (simp add: resT_abs_def coerce_def)
apply (simp add: emb_prj_emb prj_emb_prj DEFL_eq_resT)
done

lemma coerce_Done [simp]: "coerce⋅(Done⋅x) = Done⋅(coerce⋅x)"
unfolding Done_def by simp

lemma coerce_More [simp]: "coerce⋅(More⋅m) = More⋅(coerce⋅m)"
unfolding More_def by simp

lemma resT_induct [case_names adm bottom Done More]:
  fixes P :: "'a⋅'f::functor resT ⇒ bool"
  assumes adm: "adm P"
  assumes bottom: "P ⊥"
  assumes Done: "⋀x. P (Done⋅x)"
  assumes More: "⋀m f. (⋀(r::'a⋅'f resT). P (f⋅r)) ⟹ P (More⋅(fmap⋅f⋅m))"
  shows "P r"
proof (induct r rule: resT.take_induct [OF adm])
  fix n show "P (resT_take n⋅r)"
    apply (induct n arbitrary: r)
    apply (simp add: bottom)
    apply (case_tac r rule: resT.exhaust)
    apply (simp add: bottom)
    apply (simp add: Done)
    apply (simp add: More)
    done
qed

subsection ‹Class instance proofs›

lemma fmapU_resT_simps [simp]:
  "fmapU⋅f⋅(⊥::udom⋅'f::functor resT) = ⊥"
  "fmapU⋅f⋅(Done⋅x) = Done⋅(f⋅x)"
  "fmapU⋅f⋅(More⋅m) = More⋅(fmap⋅(fmapU⋅f)⋅m)"
unfolding fmapU_resT_def resT_map_def
apply (subst fix_eq, simp)
apply (subst fix_eq, simp add: Done_def)
apply (subst fix_eq, simp add: More_def)
done

instance resT :: ("functor") "functor"
proof
  fix f g :: "udom → udom" and xs :: "udom⋅'a resT"
  show "fmapU⋅f⋅(fmapU⋅g⋅xs) = fmapU⋅(Λ x. f⋅(g⋅x))⋅xs"
    by (induct xs rule: resT_induct, simp_all add: fmap_fmap)
qed

instantiation resT :: ("functor") monad
begin

fixrec bindU_resT :: "udom⋅'a resT → (udom → udom⋅'a resT) → udom⋅'a resT"
  where "bindU_resT⋅(Done⋅x)⋅f = f⋅x"
  | "bindU_resT⋅(More⋅m)⋅f = More⋅(fmap⋅(Λ r. bindU_resT⋅r⋅f)⋅m)"

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

definition
  "returnU = Done"

instance proof
  fix f :: "udom → udom" and xs :: "udom⋅'a resT"
  show "fmapU⋅f⋅xs = bindU⋅xs⋅(Λ x. returnU⋅(f⋅x))"
    by (induct xs rule: resT_induct)
       (simp_all add: fmap_fmap returnU_resT_def)
next
  fix f :: "udom → udom⋅'a resT" and x :: "udom"
  show "bindU⋅(returnU⋅x)⋅f = f⋅x"
    by (simp add: returnU_resT_def)
next
  fix xs :: "udom⋅'a resT" and h k :: "udom → udom⋅'a resT"
  show "bindU⋅(bindU⋅xs⋅h)⋅k = bindU⋅xs⋅(Λ x. bindU⋅(h⋅x)⋅k)"
    by (induct xs rule: resT_induct)
       (simp_all add: fmap_fmap)
qed

end

subsection ‹Transfer properties to polymorphic versions›

lemma fmap_resT_simps [simp]:
  "fmap⋅f⋅(⊥::'a⋅'f::functor resT) = ⊥"
  "fmap⋅f⋅(Done⋅x :: 'a⋅'f::functor resT) = Done⋅(f⋅x)"
  "fmap⋅f⋅(More⋅m :: 'a⋅'f::functor resT) = More⋅(fmap⋅(fmap⋅f)⋅m)"
unfolding fmap_def [where 'f="'f resT"]
by (simp_all add: coerce_simp)

lemma return_resT_def: "return = Done"
unfolding return_def returnU_resT_def
by (simp add: coerce_simp eta_cfun)

lemma bind_resT_simps [simp]:
  "bind⋅(⊥ :: 'a⋅'f::functor resT)⋅f = ⊥"
  "bind⋅(Done⋅x :: 'a⋅'f::functor resT)⋅f = f⋅x"
  "bind⋅(More⋅m :: 'a⋅'f::functor resT)⋅f = More⋅(fmap⋅(Λ r. bind⋅r⋅f)⋅m)"
unfolding bind_def
by (simp_all add: coerce_simp)

lemma join_resT_simps [simp]:
  "join⋅⊥ = (⊥ :: 'a⋅'f::functor resT)"
  "join⋅(Done⋅x) = x"
  "join⋅(More⋅m) = More⋅(fmap⋅join⋅m)"
unfolding join_def by simp_all

subsection ‹Nondeterministic interleaving›

text ‹In this section we present a more general formalization of the
nondeterministic interleaving operation presented in Chapter 7 of the
author's PhD thesis \<^cite>‹"holcf11"›. If both arguments are ‹Done›, then ‹zipRT› combines the results with the function
‹f› and terminates. While either argument is ‹More›,
‹zipRT› nondeterministically chooses one such argument, runs
it for one step, and then calls itself recursively.›

fixrec zipRT ::
  "('a → 'b → 'c) → 'a⋅('m::functor_plus) resT → 'b⋅'m resT → 'c⋅'m resT"
  where zipRT_Done_Done:
    "zipRT⋅f⋅(Done⋅x)⋅(Done⋅y) = Done⋅(f⋅x⋅y)"
  | zipRT_Done_More:
    "zipRT⋅f⋅(Done⋅x)⋅(More⋅b) =
      More⋅(fmap⋅(Λ r. zipRT⋅f⋅(Done⋅x)⋅r)⋅b)"
  | zipRT_More_Done:
    "zipRT⋅f⋅(More⋅a)⋅(Done⋅y) =
      More⋅(fmap⋅(Λ r. zipRT⋅f⋅r⋅(Done⋅y))⋅a)"
  | zipRT_More_More:
    "zipRT⋅f⋅(More⋅a)⋅(More⋅b) =
      More⋅(fplus⋅(fmap⋅(Λ r. zipRT⋅f⋅(More⋅a)⋅r)⋅b)
                 ⋅(fmap⋅(Λ r. zipRT⋅f⋅r⋅(More⋅b))⋅a))"

lemma zipRT_strict1 [simp]: "zipRT⋅f⋅⊥⋅r = ⊥"
by fixrec_simp

lemma zipRT_strict2 [simp]: "zipRT⋅f⋅r⋅⊥ = ⊥"
by (fixrec_simp, cases r, simp_all)

abbreviation apR (infixl "⋄" 70)
  where "a ⋄ b ≡ zipRT⋅ID⋅a⋅b"

text ‹Proofs that ‹zipRT› satisfies the applicative functor laws:›

lemma zipRT_homomorphism: "Done⋅f ⋄ Done⋅x = Done⋅(f⋅x)"
  by simp

lemma zipRT_identity: "Done⋅ID ⋄ r = r"
  by (induct r rule: resT_induct, simp_all add: fmap_fmap eta_cfun)

lemma zipRT_interchange: "r ⋄ Done⋅x = Done⋅(Λ f. f⋅x) ⋄ r"
  by (induct r rule: resT_induct, simp_all add: fmap_fmap)

text ‹The associativity rule is the hard one!›

lemma zipRT_associativity: "Done⋅cfcomp ⋄ r1 ⋄ r2 ⋄ r3 = r1 ⋄ (r2 ⋄ r3)"
proof (induct r1 arbitrary: r2 r3 rule: resT_induct)
  case (Done x1) thus ?case
  proof (induct r2 arbitrary: r3 rule: resT_induct)
    case (Done x2) thus ?case
    proof (induct r3 rule: resT_induct)
      case (More p3 c3) thus ?case (* Done/Done/More *)
        by (simp add: fmap_fmap)
    qed simp_all
  next
    case (More p2 c2) thus ?case
    proof (induct r3 rule: resT_induct)
      case (Done x3) thus ?case (* Done/More/Done *)
        by (simp add: fmap_fmap)
    next
      case (More p3 c3) thus ?case (* Done/More/More *)
        by (simp add: fmap_fmap fmap_fplus)
    qed simp_all
  qed simp_all
next
  case (More p1 c1) thus ?case
  proof (induct r2 arbitrary: r3 rule: resT_induct)
    case (Done y) thus ?case
    proof (induct r3 rule: resT_induct)
      case (Done x3) thus ?case
        by (simp add: fmap_fmap)
    next
      case (More p3 c3) thus ?case
        by (simp add: fmap_fmap)
    qed simp_all
  next
    case (More p2 c2) thus ?case
    proof (induct r3 rule: resT_induct)
      case (Done x3) thus ?case
        by (simp add: fmap_fmap fmap_fplus)
    next
      case (More p3 c3) thus ?case
        by (simp add: fmap_fmap fmap_fplus fplus_assoc)
    qed simp_all
  qed simp_all
qed simp_all

end