Theory Cotree_Algebra
subsection ‹Pointwise arithmetic on infinite binary trees›
theory Cotree_Algebra
imports Cotree
begin
subsubsection ‹Constants and operators›
instantiation tree :: (zero) zero begin
definition [applicative_unfold]: "0 = pure_tree 0"
instance ..
end
instantiation tree :: (one) one begin
definition [applicative_unfold]: "1 = pure_tree 1"
instance ..
end
instantiation tree :: (plus) plus begin
definition [applicative_unfold]: "plus x y = pure (+) ⋄ x ⋄ (y :: 'a tree)"
instance ..
end
lemma plus_tree_simps [simp]:
"root (t + t') = root t + root t'"
"left (t + t') = left t + left t'"
"right (t + t') = right t + right t'"
by(simp_all add: plus_tree_def)