Theory Binary_Tree_Monad

section ‹Binary tree monad›

theory Binary_Tree_Monad
imports Monad
begin

subsection ‹Type definition›

tycondef 'a⋅btree =
  Leaf (lazy "'a") | Node (lazy "'a⋅btree") (lazy "'a⋅btree")

lemma coerce_btree_abs [simp]: "coerce⋅(btree_abs⋅x) = btree_abs⋅(coerce⋅x)"
apply (simp add: btree_abs_def coerce_def)
apply (simp add: emb_prj_emb prj_emb_prj DEFL_eq_btree)
done

lemma coerce_Leaf [simp]: "coerce⋅(Leaf⋅x) = Leaf⋅(coerce⋅x)"
unfolding Leaf_def by simp

lemma coerce_Node [simp]: "coerce⋅(Node⋅xs⋅ys) = Node⋅(coerce⋅xs)⋅(coerce⋅ys)"
unfolding Node_def by simp

lemma fmapU_btree_simps [simp]:
  "fmapU⋅f⋅(⊥::udom⋅btree) = ⊥"
  "fmapU⋅f⋅(Leaf⋅x) = Leaf⋅(f⋅x)"
  "fmapU⋅f⋅(Node⋅xs⋅ys) = Node⋅(fmapU⋅f⋅xs)⋅(fmapU⋅f⋅ys)"
unfolding fmapU_btree_def btree_map_def
apply (subst fix_eq, simp)
apply (subst fix_eq, simp add: Leaf_def)
apply (subst fix_eq, simp add: Node_def)
done

subsection ‹Class instance proofs›

instance btree :: "functor"
apply standard
apply (induct_tac xs rule: btree.induct, simp_all)
done

instantiation btree :: monad
begin

definition
  "returnU = Leaf"

fixrec bindU_btree :: "udom⋅btree → (udom → udom⋅btree) → udom⋅btree"
  where "bindU_btree⋅(Leaf⋅x)⋅k = k⋅x"
  | "bindU_btree⋅(Node⋅xs⋅ys)⋅k =
      Node⋅(bindU_btree⋅xs⋅k)⋅(bindU_btree⋅ys⋅k)"

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

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

end

subsection ‹Transfer properties to polymorphic versions›

lemma fmap_btree_simps [simp]:
  "fmap⋅f⋅(⊥::'a⋅btree) = ⊥"
  "fmap⋅f⋅(Leaf⋅x) = Leaf⋅(f⋅x)"
  "fmap⋅f⋅(Node⋅xs⋅ys) = Node⋅(fmap⋅f⋅xs)⋅(fmap⋅f⋅ys)"
unfolding fmap_def by simp_all

lemma bind_btree_simps [simp]:
  "bind⋅(⊥::'a⋅btree)⋅k = ⊥"
  "bind⋅(Leaf⋅x)⋅k = k⋅x"
  "bind⋅(Node⋅xs⋅ys)⋅k = Node⋅(bind⋅xs⋅k)⋅(bind⋅ys⋅k)"
unfolding bind_def
by (simp_all add: coerce_simp)

lemma return_btree_def:
  "return = Leaf"
unfolding return_def returnU_btree_def
by (simp add: coerce_simp eta_cfun)

lemma join_btree_simps [simp]:
  "join⋅(⊥::'a⋅btree⋅btree) = ⊥"
  "join⋅(Leaf⋅xs) = xs"
  "join⋅(Node⋅xss⋅yss) = Node⋅(join⋅xss)⋅(join⋅yss)"
unfolding join_def by simp_all

end