Theory Lift_Monad

section ‹Lift monad›

theory Lift_Monad
imports Monad
begin

subsection ‹Type definition›

tycondef 'a⋅lifted = Lifted (lazy "'a")

lemma coerce_lifted_abs [simp]: "coerce⋅(lifted_abs⋅x) = lifted_abs⋅(coerce⋅x)"
apply (simp add: lifted_abs_def coerce_def)
apply (simp add: emb_prj_emb prj_emb_prj DEFL_eq_lifted)
done

lemma coerce_Lifted [simp]: "coerce⋅(Lifted⋅x) = Lifted⋅(coerce⋅x)"
unfolding Lifted_def by simp

lemma fmapU_lifted_simps [simp]:
  "fmapU⋅f⋅(⊥::udom⋅lifted) = ⊥"
  "fmapU⋅f⋅(Lifted⋅x) = Lifted⋅(f⋅x)"
unfolding fmapU_lifted_def lifted_map_def fix_const
apply simp
apply (simp add: Lifted_def)
done

subsection ‹Class instance proofs›

instance lifted :: "functor"
  by standard (induct_tac xs rule: lifted.induct, simp_all)

instantiation lifted :: monad
begin

fixrec bindU_lifted :: "udom⋅lifted → (udom → udom⋅lifted) → udom⋅lifted"
  where "bindU_lifted⋅(Lifted⋅x)⋅k = k⋅x"

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

definition returnU_lifted_def:
  "returnU = Lifted"

instance proof
  fix x :: "udom"
  fix f :: "udom → udom"
  fix h k :: "udom → udom⋅lifted"
  fix xs :: "udom⋅lifted"
  show "fmapU⋅f⋅xs = bindU⋅xs⋅(Λ x. returnU⋅(f⋅x))"
    by (induct xs rule: lifted.induct, simp_all add: returnU_lifted_def)
  show "bindU⋅(returnU⋅x)⋅k = k⋅x"
    by (simp add: returnU_lifted_def)
  show "bindU⋅(bindU⋅xs⋅h)⋅k = bindU⋅xs⋅(Λ x. bindU⋅(h⋅x)⋅k)"
    by (induct xs rule: lifted.induct) simp_all
qed

end

subsection ‹Transfer properties to polymorphic versions›

lemma fmap_lifted_simps [simp]:
  "fmap⋅f⋅(⊥::'a⋅lifted) = ⊥"
  "fmap⋅f⋅(Lifted⋅x) = Lifted⋅(f⋅x)"
unfolding fmap_def by simp_all

lemma bind_lifted_simps [simp]:
  "bind⋅(⊥::'a⋅lifted)⋅f = ⊥"
  "bind⋅(Lifted⋅x)⋅f = f⋅x"
unfolding bind_def by simp_all

lemma return_lifted_def: "return = Lifted"
unfolding return_def returnU_lifted_def
by (simp add: coerce_cfun cfcomp1 eta_cfun)

lemma join_lifted_simps [simp]:
  "join⋅(⊥::'a⋅lifted⋅lifted) = ⊥"
  "join⋅(Lifted⋅xs) = xs"
unfolding join_def by simp_all

end