Theory Stern_Brocot_Tree
section ‹The Stern-Brocot Tree›
theory Stern_Brocot_Tree
imports
HOL.Rat
"HOL-Library.Sublist"
Cotree_Algebra
Applicative_Lifting.Stream_Algebra
begin
text‹
The Stern-Brocot tree is discussed at length by \<^citet>‹‹\S4.5› in "GrahamKnuthPatashnik1994CM"›.
In essence the tree enumerates the rational numbers in their lowest terms by constructing the
‹mediant› of two bounding fractions.
›
type_synonym fraction = "nat × nat"
definition mediant :: "fraction × fraction ⇒ fraction"
where "mediant ≡ λ((a, c), (b, d)). (a + b, c + d)"
definition stern_brocot :: "fraction tree"
where
"stern_brocot = unfold_tree
(λ(lb, ub). mediant (lb, ub))
(λ(lb, ub). (lb, mediant (lb, ub)))
(λ(lb, ub). (mediant (lb, ub), ub))
((0, 1), (1, 0))"
text‹
This process is visualised in Figure~\ref{fig:stern-brocot-iterate}.
Intuitively each node is labelled with the mediant of it's rightmost and leftmost ancestors.
\begin{figure}
\centering
\begin{tikzpicture}[auto,thick,node distance=3cm,main node/.style={circle,draw,font=\sffamily\Large\bfseries}]
\node[main node] (0) at (0, 0) {$\frac{1}{1}$};
\node[main node] (1) at (-4, 1) {$\frac{0}{1}$};
\node[main node] (2) at (4, 1) {$\frac{1}{0}$};
\node[main node] (3) at (-2, -1) {$\frac{1}{2}$};
\node[main node] (4) at (2, -1) {$\frac{2}{1}$};
\node[main node] (5) at (-3, -2) {$\frac{1}{3}$};
\node[main node] (6) at (3, -2) {$\frac{3}{1}$};
\node[main node] (7) at (-1, -2) {$\frac{2}{3}$};
\node[main node] (8) at (1, -2) {$\frac{3}{2}$};
\node (9) at (-3.5, -3) {};
\node (10) at (-2.5, -3) {};
\node (11) at (-1.5, -3) {};
\node (12) at (-0.5, -3) {};
\node (13) at (0.5, -3) {};
\node (14) at (1.5, -3) {};
\node (15) at (2.5, -3) {};
\node (16) at (3.5, -3) {};
\path
(1) edge[dashed] (0)
(2) edge[dashed] (0)
(0) edge (3)
(0) edge (4)
(3) edge (5)
(3) edge (7)
(4) edge (6)
(4) edge (8)
(5) edge[dotted] (9)
(5) edge[dotted] (10)
(6) edge[dotted] (15)
(6) edge[dotted] (16)
(7) edge[dotted] (11)
(7) edge[dotted] (12)
(8) edge[dotted] (13)
(8) edge[dotted] (14);
\end{tikzpicture}
\label{fig:stern-brocot-iterate}
\caption{Constructing the Stern-Brocot tree iteratively.}
\end{figure}
Our ultimate goal is to show that the Stern-Brocot tree contains all rationals (in lowest terms),
and that each occurs exactly once in the tree. A proof is sketched in \<^citet>‹‹\S4.5› in "GrahamKnuthPatashnik1994CM"›.
›
subsection ‹Specification via a recursion equation›
text ‹
\<^cite>‹"Hinze2009JFP"› derives the following recurrence relation for the Stern-Brocot tree.
We will show in \S\ref{section:eq:rec:iterative} that his derivation is sound with respect to the
standard iterative definition of the tree shown above.
›
abbreviation succ :: "fraction ⇒ fraction"
where "succ ≡ λ(m, n). (m + n, n)"
abbreviation recip :: "fraction ⇒ fraction"
where "recip ≡ λ(m, n). (n, m)"
corec stern_brocot_recurse :: "fraction tree"
where
"stern_brocot_recurse =
Node (1, 1)
(map_tree recip (map_tree succ (map_tree recip stern_brocot_recurse)))
(map_tree succ stern_brocot_recurse)"
text ‹Actually, we would like to write the specification below, but ‹(⋄)› cannot be registered as friendly due to varying type parameters›
lemma stern_brocot_unfold:
"stern_brocot_recurse =
Node (1, 1)
(pure recip ⋄ (pure succ ⋄ (pure recip ⋄ stern_brocot_recurse)))
(pure succ ⋄ stern_brocot_recurse)"
by(fact stern_brocot_recurse.code[unfolded map_tree_ap_tree_pure_tree[symmetric]])
lemma stern_brocot_simps [simp]:
"root stern_brocot_recurse = (1, 1)"
"left stern_brocot_recurse = pure recip ⋄ (pure succ ⋄ (pure recip ⋄ stern_brocot_recurse))"
"right stern_brocot_recurse = pure succ ⋄ stern_brocot_recurse"
by (subst stern_brocot_unfold, simp)+
lemma stern_brocot_conv:
"stern_brocot_recurse = tree_recurse (recip ∘ succ ∘ recip) succ (1, 1)"
apply(rule tree_recurse.unique)
apply(subst stern_brocot_unfold)
apply(simp add: o_assoc)
apply(rule conjI; applicative_nf; simp)
done
subsection ‹Basic properties›
text ‹
The recursive definition is useful for showing some basic properties of the tree,
such as that the pairs of numbers at each node are coprime, and have non-zero denominators.
Both are simple inductions on the path.
›
lemma stern_brocot_denominator_non_zero:
"case root (traverse_tree path stern_brocot_recurse) of (m, n) ⇒ m > 0 ∧ n > 0"
by(induct path)(auto split: dir.splits)
lemma stern_brocot_coprime:
"case root (traverse_tree path stern_brocot_recurse) of (m, n) ⇒ coprime m n"
by (induct path) (auto split: dir.splits simp add: coprime_iff_gcd_eq_1, metis gcd.commute gcd_add1)
subsection ‹All the rationals›
text‹
For every pair of positive naturals, we can construct a path into the Stern-Brocot tree such that the naturals at the end of the path define the same rational as the pair we started with.
Intuitively, the choices made by Euclid's algorithm define this path.
›
function mk_path :: "nat ⇒ nat ⇒ path" where
"m = n ⟹ mk_path (Suc m) (Suc n) = []"
| "m < n ⟹ mk_path (Suc m) (Suc n) = L # mk_path (Suc m) (n - m)"
| "m > n ⟹ mk_path (Suc m) (Suc n) = R # mk_path (m - n) (Suc n)"
| "mk_path 0 _ = undefined"
| "mk_path _ 0 = undefined"
by atomize_elim(auto, arith)
termination mk_path by lexicographic_order
lemmas mk_path_induct[case_names equal less greater] = mk_path.induct
abbreviation rat_of :: "fraction ⇒ rat"
where "rat_of ≡ λ(x, y). Fract (int x) (int y)"
theorem stern_brocot_rationals:
"⟦ m > 0; n > 0 ⟧ ⟹
root (traverse_tree (mk_path m n) (pure rat_of ⋄ stern_brocot_recurse)) = Fract (int m) (int n)"
proof(induction m n rule: mk_path_induct)
case (less m n)
with stern_brocot_denominator_non_zero[where path="mk_path (Suc m) (n - m)"]
show ?case
by (simp add: eq_rat field_simps of_nat_diff split: prod.split_asm)
next
case (greater m n)
with stern_brocot_denominator_non_zero[where path="mk_path (m - n) (Suc n)"]
show ?case
by (simp add: eq_rat field_simps of_nat_diff split: prod.split_asm)
qed (simp_all add: eq_rat)
subsection ‹No repetitions›
text ‹
We establish that the Stern-Brocot tree does not contain repetitions, i.e.,
that each rational number appears at most once in it.
Note that this property is stronger than merely requiring that pairs of naturals not be repeated,
though it is implied by that property and @{thm [source] "stern_brocot_coprime"}.
Intuitively, the tree enjoys the \emph{binary search tree} ordering property when we map our
pairs of naturals into rationals. This suffices to show that each rational appears at most once
in the tree. To establish this seems to require more structure than is present in the recursion
equations, and so we follow \<^citet>‹"BackhouseFerreira2008MPC"› and \<^citet>‹"Hinze2009JFP"› by
introducing another definition of the tree, which summarises the path to each node using a matrix.
We then derive an iterative version and use invariant reasoning on that.
We begin by defining some matrix machinery.
This is all elementary and primitive (we do not need much algebra).
›
type_synonym matrix = "fraction × fraction"
type_synonym vector = fraction
definition times_matrix :: "matrix ⇒ matrix ⇒ matrix" (infixl "⊗" 70)
where "times_matrix = (λ((a, c), (b, d)) ((a', c'), (b', d')).
((a * a' + b * c', c * a' + d * c'),
(a * b' + b * d', c * b' + d * d')))"
definition times_vector :: "matrix ⇒ vector ⇒ vector" (infixr "⊙" 70)
where "times_vector = (λ((a, c), (b, d)) (a', c'). (a * a' + b * c', c * a' + d * c'))"
context begin
private definition F :: matrix where "F = ((0, 1), (1, 0))"
private definition I :: matrix where "I = ((1, 0), (0, 1))"
private definition LL :: matrix where "LL = ((1, 1), (0, 1))"
private definition UR :: matrix where "UR = ((1, 0), (1, 1))"
definition Det :: "matrix ⇒ nat" where "Det ≡ λ((a, c), (b, d)). a * d - b * c"
lemma Dets [iff]:
"Det I = 1"
"Det LL = 1"
"Det UR = 1"
unfolding Det_def I_def LL_def UR_def by simp_all
lemma LL_UR_Det:
"Det m = 1 ⟹ Det (m ⊗ LL) = 1"
"Det m = 1 ⟹ Det (LL ⊗ m) = 1"
"Det m = 1 ⟹ Det (m ⊗ UR) = 1"
"Det m = 1 ⟹ Det (UR ⊗ m) = 1"
by (cases m, simp add: Det_def LL_def UR_def times_matrix_def split_def field_simps)+
lemma mediant_I_F [simp]:
"mediant F = (1, 1)"
"mediant I = (1, 1)"
by (simp_all add: F_def I_def mediant_def)
lemma times_matrix_I [simp]:
"I ⊗ x = x"
"x ⊗ I = x"
by (simp_all add: times_matrix_def I_def split_def)
lemma times_matrix_assoc [simp]:
"(x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)"
by (simp add: times_matrix_def field_simps split_def)
lemma LL_UR_pos:
"0 < snd (mediant m) ⟹ 0 < snd (mediant (m ⊗ LL))"
"0 < snd (mediant m) ⟹ 0 < snd (mediant (m ⊗ UR))"
by (cases m) (simp_all add: LL_def UR_def times_matrix_def split_def field_simps mediant_def)
lemma recip_succ_recip: "recip ∘ succ ∘ recip = (λ(x, y). (x, x + y))"
by (clarsimp simp: fun_eq_iff)
text ‹
\citeauthor{BackhouseFerreira2008MPC} work with the identity matrix @{const "I"} at the root.
This has the advantage that all relevant matrices have determinants of @{term "1 :: nat"}.
›
definition stern_brocot_iterate_aux :: "matrix ⇒ matrix tree"
where "stern_brocot_iterate_aux ≡ tree_iterate (λs. s ⊗ LL) (λs. s ⊗ UR)"
definition stern_brocot_iterate :: "fraction tree"
where "stern_brocot_iterate ≡ map_tree mediant (stern_brocot_iterate_aux I)"
lemma stern_brocot_recurse_iterate: "stern_brocot_recurse = stern_brocot_iterate" (is "?lhs = ?rhs")
proof -
have "?rhs = map_tree mediant (tree_recurse ((⊗) LL) ((⊗) UR) I)"
using tree_recurse_iterate[where f="(⊗)" and l="LL" and r="UR" and ε="I"]
by (simp add: stern_brocot_iterate_def stern_brocot_iterate_aux_def)
also have "… = tree_recurse ((⊙) LL) ((⊙) UR) (1, 1)"
unfolding mediant_I_F(2)[symmetric]
by (rule tree_recurse_fusion)(simp_all add: fun_eq_iff mediant_def times_matrix_def times_vector_def LL_def UR_def)[2]
also have "… = ?lhs"
by (simp add: stern_brocot_conv recip_succ_recip times_vector_def LL_def UR_def)
finally show ?thesis by simp
qed
text‹
The following are the key ordering properties derived by \<^citet>‹"BackhouseFerreira2008MPC"›.
They hinge on the matrices containing only natural numbers.
›
lemma tree_ordering_left:
assumes DX: "Det X = 1"
assumes DY: "Det Y = 1"
assumes MX: "0 < snd (mediant X)"
shows "rat_of (mediant (X ⊗ LL ⊗ Y)) < rat_of (mediant X)"
proof -
from DX DY have F: "0 < snd (mediant (X ⊗ LL ⊗ Y))"
by (auto simp: Det_def times_matrix_def LL_def split_def mediant_def)
obtain x11 x12 x21 x22 where X: "X = ((x11, x12), (x21, x22))" by(cases X) auto
obtain y11 y12 y21 y22 where Y: "Y = ((y11, y12), (y21, y22))" by(cases Y) auto
from DX DY have *: "(x12 * x21) * (y12 + y22) < (x11 * x22) * (y12 + y22)"
by(simp add: X Y Det_def)(cases y12, simp_all add: field_simps)
from DX DY MX F show ?thesis
apply (simp add: split_def X Y of_nat_mult [symmetric] del: of_nat_mult)
apply (clarsimp simp: Det_def times_matrix_def LL_def UR_def mediant_def split_def)
using * by (simp add: field_simps)
qed
lemma tree_ordering_right:
assumes DX: "Det X = 1"
assumes DY: "Det Y = 1"
assumes MX: "0 < snd (mediant X)"
shows "rat_of (mediant X) < rat_of (mediant (X ⊗ UR ⊗ Y))"
proof -
from DX DY have F: "0 < snd (mediant (X ⊗ UR ⊗ Y))"
by (auto simp: Det_def times_matrix_def UR_def split_def mediant_def)
obtain x11 x12 x21 x22 where X: "X = ((x11, x12), (x21, x22))" by(cases X) auto
obtain y11 y12 y21 y22 where Y: "Y = ((y11, y12), (y21, y22))" by(cases Y) auto
show ?thesis using DX DY MX F
apply (simp add: X Y split_def of_nat_mult [symmetric] del: of_nat_mult)
apply (simp add: Det_def times_matrix_def LL_def UR_def mediant_def split_def algebra_simps)
apply (simp add: add_mult_distrib2[symmetric] mult.assoc[symmetric])
apply (cases y21; simp)
done
qed
lemma stern_brocot_iterate_aux_Det:
assumes "Det m = 1" "0 < snd (mediant m)"
shows "Det (root (traverse_tree path (stern_brocot_iterate_aux m))) = 1"
and "0 < snd (mediant (root (traverse_tree path (stern_brocot_iterate_aux m))))"
using assms
by (induct path arbitrary: m)
(simp_all add: stern_brocot_iterate_aux_def LL_UR_Det LL_UR_pos split: dir.splits)
lemma stern_brocot_iterate_aux_decompose:
"∃m''. m ⊗ m'' = root (traverse_tree path (stern_brocot_iterate_aux m)) ∧ Det m'' = 1"
proof(induction path arbitrary: m)
case Nil show ?case
by (auto simp add: stern_brocot_iterate_aux_def intro: exI[where x=I] simp del: split_paired_Ex)
next
case (Cons d ds m)
from Cons.IH[where m="m ⊗ UR"] Cons.IH[where m="m ⊗ LL"] show ?case
by(simp add: stern_brocot_iterate_aux_def split: dir.splits del: split_paired_Ex)(fastforce simp: LL_UR_Det)
qed
lemma stern_brocot_fractions_not_repeated_strict_prefix:
assumes "root (traverse_tree path stern_brocot_iterate) = root (traverse_tree path' stern_brocot_iterate)"
assumes pp': "strict_prefix path path'"
shows False
proof -
from pp' obtain d ds where pp': "path' = path @ [d] @ ds" by (auto elim!: strict_prefixE')
define m where "m = root (traverse_tree path (stern_brocot_iterate_aux I))"
then have Dm: "Det m = 1" and Pm: "0 < snd (mediant m)"
using stern_brocot_iterate_aux_Det[where path="path" and m="I"] by simp_all
define m' where "m' = root (traverse_tree path' (stern_brocot_iterate_aux I))"
then have Dm': "Det m' = 1"
using stern_brocot_iterate_aux_Det[where path=path' and m="I"] by simp
let ?M = "case d of L ⇒ m ⊗ LL | R ⇒ m ⊗ UR"
from pp' have "root (traverse_tree ds (stern_brocot_iterate_aux ?M)) = m'"
by(simp add: m_def m'_def stern_brocot_iterate_aux_def traverse_tree_tree_iterate split: dir.splits)
then obtain m'' where mm'm'': "?M ⊗ m''= m'" and Dm'': "Det m'' = 1"
using stern_brocot_iterate_aux_decompose[where path="ds" and m="?M"] by clarsimp
hence "case d of L ⇒ rat_of (mediant m') < rat_of (mediant m) | R ⇒ rat_of (mediant m) < rat_of (mediant m')"
using tree_ordering_left[OF Dm Dm'' Pm] tree_ordering_right[OF Dm Dm'' Pm]
by (simp split: dir.splits)
with assms show False
by (simp add: stern_brocot_iterate_def m_def m'_def split: dir.splits)
qed
lemma stern_brocot_fractions_not_repeated_parallel:
assumes "root (traverse_tree path stern_brocot_iterate) = root (traverse_tree path' stern_brocot_iterate)"
assumes p: "path = pref @ d # ds"
assumes p': "path' = pref @ d' # ds'"
assumes dd': "d ≠ d'"
shows False
proof -
define m where "m = root (traverse_tree pref (stern_brocot_iterate_aux I))"
then have Dm: "Det m = 1" and Pm: "0 < snd (mediant m)"
using stern_brocot_iterate_aux_Det[where path="pref" and m="I"] by simp_all
define pm where "pm = root (traverse_tree path (stern_brocot_iterate_aux I))"
then have Dpm: "Det pm = 1"
using stern_brocot_iterate_aux_Det[where path=path and m="I"] by simp
let ?M = "case d of L ⇒ m ⊗ LL | R ⇒ m ⊗ UR"
from p
have "root (traverse_tree ds (stern_brocot_iterate_aux ?M)) = pm"
by(simp add: stern_brocot_iterate_aux_def m_def pm_def traverse_tree_tree_iterate split: dir.splits)
then obtain pm'
where pm': "?M ⊗ pm'= pm" and Dpm': "Det pm' = 1"
using stern_brocot_iterate_aux_decompose[where path="ds" and m="?M"] by clarsimp
hence "case d of L ⇒ rat_of (mediant pm) < rat_of (mediant m) | R ⇒ rat_of (mediant m) < rat_of (mediant pm)"
using tree_ordering_left[OF Dm Dpm' Pm, unfolded pm']
tree_ordering_right[OF Dm Dpm' Pm, unfolded pm']
by (simp split: dir.splits)
moreover
define p'm where "p'm = root (traverse_tree path' (stern_brocot_iterate_aux I))"
then have Dp'm: "Det p'm = 1"
using stern_brocot_iterate_aux_Det[where path=path' and m="I"] by simp
let ?M' = "case d' of L ⇒ m ⊗ LL | R ⇒ m ⊗ UR"
from p'
have "root (traverse_tree ds' (stern_brocot_iterate_aux ?M')) = p'm"
by(simp add: stern_brocot_iterate_aux_def m_def p'm_def traverse_tree_tree_iterate split: dir.splits)
then obtain p'm'
where p'm': "?M' ⊗ p'm' = p'm" and Dp'm': "Det p'm' = 1"
using stern_brocot_iterate_aux_decompose[where path="ds'" and m="?M'"] by clarsimp
hence "case d' of L ⇒ rat_of (mediant p'm) < rat_of (mediant m) | R ⇒ rat_of (mediant m) < rat_of (mediant p'm)"
using tree_ordering_left[OF Dm Dp'm' Pm, unfolded pm']
tree_ordering_right[OF Dm Dp'm' Pm, unfolded pm']
by (simp split: dir.splits)
ultimately show False using pm' p'm' assms
by(simp add: m_def pm_def p'm_def stern_brocot_iterate_def split: dir.splits)
qed
lemma lists_not_eq:
assumes "xs ≠ ys"
obtains
(c1) "strict_prefix xs ys"
| (c2) "strict_prefix ys xs"
| (c3) ps x y xs' ys'
where "xs = ps @ x # xs'" and "ys = ps @ y # ys'" and "x ≠ y"
using assms
by (cases xs ys rule: prefix_cases)
(blast dest: parallel_decomp prefix_order.neq_le_trans)+
lemma stern_brocot_fractions_not_repeated:
assumes "root (traverse_tree path stern_brocot_iterate) = root (traverse_tree path' stern_brocot_iterate)"
shows "path = path'"
proof(rule ccontr)
assume "path ≠ path'"
then show False using assms
by (cases path path' rule: lists_not_eq)
(blast intro: stern_brocot_fractions_not_repeated_strict_prefix sym
stern_brocot_fractions_not_repeated_parallel)+
qed
text ‹ The function @{const Fract} is injective under certain conditions. ›
lemma rat_inv_eq:
assumes "Fract a b = Fract c d"
assumes "b > 0"
assumes "d > 0"
assumes "coprime a b"
assumes "coprime c d"
shows "a = c ∧ b = d"
proof -
from ‹b > 0› ‹d > 0› ‹Fract a b = Fract c d›
have *: "a * d = c * b" by (simp add: eq_rat)
from arg_cong[where f=sgn, OF this] ‹b > 0› ‹d > 0›
have "sgn a = sgn c" by (simp add: sgn_mult)
with * show ?thesis
using ‹b > 0› ‹d > 0› coprime_crossproduct_int[OF ‹coprime a b› ‹coprime c d›]
by (simp add: abs_sgn)
qed
theorem stern_brocot_rationals_not_repeated:
assumes "root (traverse_tree path (pure rat_of ⋄ stern_brocot_recurse))
= root (traverse_tree path' (pure rat_of ⋄ stern_brocot_recurse))"
shows "path = path'"
using assms
using stern_brocot_coprime[where path=path]
stern_brocot_coprime[where path=path']
stern_brocot_denominator_non_zero[where path=path]
stern_brocot_denominator_non_zero[where path=path']
by(auto simp: gcd_int_def dest!: rat_inv_eq intro: stern_brocot_fractions_not_repeated simp add: stern_brocot_recurse_iterate[symmetric] split: prod.splits)
subsection ‹Equivalence of recursive and iterative version \label{section:eq:rec:iterative}›
text ‹
\citeauthor{Hinze2009JFP} shows that it does not matter whether we use @{const I} or
@{const "F"} at the root provided we swap the left and right matrices too.
›
definition stern_brocot_Hinze_iterate :: "fraction tree"
where "stern_brocot_Hinze_iterate = map_tree mediant (tree_iterate (λs. s ⊗ UR) (λs. s ⊗ LL) F)"
lemma mediant_times_F: "mediant ∘ (λs. s ⊗ F) = mediant"
by(simp add: times_matrix_def F_def mediant_def split_def o_def add.commute)
lemma stern_brocot_iterate: "stern_brocot = stern_brocot_iterate"
proof -
have "stern_brocot = stern_brocot_Hinze_iterate"
unfolding stern_brocot_def stern_brocot_Hinze_iterate_def
by(subst unfold_tree_tree_iterate)(simp add: F_def times_matrix_def mediant_def UR_def LL_def split_def)
also have "… = map_tree mediant (map_tree (λs. s ⊗ F) (tree_iterate (λs. s ⊗ LL) (λs. s ⊗ UR) I))"
unfolding stern_brocot_Hinze_iterate_def
by(subst tree_iterate_fusion[where l'="λs. s ⊗ UR" and r'="λs. s ⊗ LL"])
(simp_all add: fun_eq_iff times_matrix_def UR_def LL_def F_def I_def)
also have "… = stern_brocot_iterate"
by(simp only: tree.map_comp mediant_times_F stern_brocot_iterate_def stern_brocot_iterate_aux_def)
finally show ?thesis .
qed
theorem stern_brocot_mediant_recurse: "stern_brocot = stern_brocot_recurse"
by(simp add: stern_brocot_recurse_iterate stern_brocot_iterate)
end
no_notation times_matrix (infixl "⊗" 70)
and times_vector (infixl "⊙" 70)
section ‹Linearising the Stern-Brocot Tree›
subsection ‹Turning a tree into a stream›
corec tree_chop :: "'a tree ⇒ 'a tree"
where "tree_chop t = Node (root (left t)) (right t) (tree_chop (left t))"
lemma tree_chop_sel [simp]:
"root (tree_chop t) = root (left t)"
"left (tree_chop t) = right t"
"right (tree_chop t) = tree_chop (left t)"
by(subst tree_chop.code; simp; fail)+
text ‹@{const tree_chop} is a idiom homomorphism›
lemma tree_chop_pure_tree [simp]:
"tree_chop (pure x) = pure x"
by(coinduction rule: tree.coinduct_strong) auto
lemma tree_chop_ap_tree [simp]:
"tree_chop (f ⋄ x) = tree_chop f ⋄ tree_chop x"
by(coinduction arbitrary: f x rule: tree.coinduct_strong) auto
lemma tree_chop_plus: "tree_chop (t + t') = tree_chop t + tree_chop t'"
by(simp add: plus_tree_def)