Theory Bird_Tree

(* Author: Andreas Lochbihler, ETH Zurich
   Author: Peter Gammie *)

section ‹ The Bird tree ›

text ‹
  We define the Bird tree following \<^cite>‹"Hinze2009JFP"› and prove that it is a
  permutation of the Stern-Brocot tree. As a corollary, we derive that the Bird tree also
  contains all rational numbers in lowest terms exactly once.
›

theory Bird_Tree imports Stern_Brocot_Tree begin

corec bird :: "fraction tree"
where
  "bird = Node (1, 1) (map_tree recip (map_tree succ bird)) (map_tree succ (map_tree recip bird))"

lemma bird_unfold:
  "bird = Node (1, 1) (pure recip ⋄ (pure succ ⋄ bird)) (pure succ ⋄ (pure recip ⋄ bird))"
using bird.code unfolding map_tree_ap_tree_pure_tree[symmetric] .

lemma bird_simps [simp]:
  "root bird = (1, 1)"
  "left bird = pure recip ⋄ (pure succ ⋄ bird)"
  "right bird = pure succ ⋄ (pure recip ⋄ bird)"
by(subst bird_unfold, simp)+

lemma mirror_bird: "mirror bird = pure recip ⋄ bird" (is "?lhs = ?rhs")
proof(rule sym)
  let ?F = "λt. Node (1, 1) (map_tree succ (map_tree recip t)) (map_tree recip (map_tree succ t))"
  have *: "mirror bird = ?F (mirror bird)"
    by(rule tree.expand; simp add: mirror_ap_tree mirror_pure map_tree_ap_tree_pure_tree[symmetric])
  show "t = mirror bird" when "t = ?F t" for t using that by corec_unique (fact *)
  show "pure recip ⋄ bird = ?F (pure recip ⋄ bird)"
    by(rule tree.expand; simp add: map_tree_ap_tree_pure_tree; applicative_lifting; simp add: split_beta)
qed

primcorec even_odd_mirror :: "bool ⇒ 'a tree ⇒ 'a tree"
where
  "⋀even. root (even_odd_mirror even t) = root t"
| "⋀even. left (even_odd_mirror even t) = even_odd_mirror (¬ even) (if even then right t else left t)"
| "⋀even. right (even_odd_mirror even t) = even_odd_mirror (¬ even) (if even then left t else right t)"

definition even_mirror :: "'a tree ⇒ 'a tree"
where "even_mirror = even_odd_mirror True"

definition odd_mirror :: "'a tree ⇒ 'a tree"
where "odd_mirror = even_odd_mirror False"

lemma even_mirror_simps [simp]:
  "root (even_mirror t) = root t"
  "left (even_mirror t) = odd_mirror (right t)"
  "right (even_mirror t) = odd_mirror (left t)"
  and odd_mirror_simps [simp]:
  "root (odd_mirror t) = root t"
  "left (odd_mirror t) = even_mirror (left t)"
  "right (odd_mirror t) = even_mirror (right t)"
by(simp_all add: even_mirror_def odd_mirror_def)

lemma even_odd_mirror_pure [simp]: fixes even shows
  "even_odd_mirror even (pure_tree x) = pure_tree x"
by(coinduction arbitrary: even) auto

lemma even_odd_mirror_ap_tree [simp]: fixes even shows
  "even_odd_mirror even (f ⋄ x) = even_odd_mirror even f ⋄ even_odd_mirror even x"
by(coinduction arbitrary: even f x) auto

lemma [simp]:
  shows even_mirror_pure: "even_mirror (pure_tree x) = pure_tree x"
  and odd_mirror_pure: "odd_mirror (pure_tree x) = pure_tree x"
by(simp_all add: even_mirror_def odd_mirror_def)

lemma [simp]:
  shows even_mirror_ap_tree: "even_mirror (f ⋄ x) = even_mirror f ⋄ even_mirror x"
  and odd_mirror_ap_tree: "odd_mirror (f ⋄ x) = odd_mirror f ⋄ odd_mirror x"
by(simp_all add: even_mirror_def odd_mirror_def)

fun even_mirror_path :: "path ⇒ path"
  and odd_mirror_path :: "path ⇒ path"
where
  "even_mirror_path [] = []"
| "even_mirror_path (d # ds) = (case d of L ⇒ R | R ⇒ L) # odd_mirror_path ds"
| "odd_mirror_path [] = []"
| "odd_mirror_path (d # ds) = d # even_mirror_path ds"

lemma even_mirror_traverse_tree [simp]: 
  "root (traverse_tree path (even_mirror t)) = root (traverse_tree (even_mirror_path path) t)"
  and odd_mirror_traverse_tree [simp]:
  "root (traverse_tree path (odd_mirror t)) = root (traverse_tree (odd_mirror_path path) t)"
by (induct path arbitrary: t) (simp_all split: dir.splits)

lemma even_odd_mirror_path_involution [simp]:
  "even_mirror_path (even_mirror_path path) = path"
  "odd_mirror_path (odd_mirror_path path) = path"
by (induct path) (simp_all split: dir.splits)

lemma even_odd_mirror_path_injective [simp]:
  "even_mirror_path path = even_mirror_path path' ⟷ path = path'"
  "odd_mirror_path path = odd_mirror_path path' ⟷ path = path'"
by (induct path arbitrary: path') (case_tac path', simp_all split: dir.splits)+

lemma odd_mirror_bird_stern_brocot:
  "odd_mirror bird = stern_brocot_recurse"
proof -
  let ?rsrs = "map_tree (recip ∘ succ ∘ recip ∘ succ)"
  let ?rssr = "map_tree (recip ∘ succ ∘ succ ∘ recip)"
  let ?srrs = "map_tree (succ ∘ recip ∘ recip ∘ succ)"
  let ?srsr = "map_tree (succ ∘ recip ∘ succ ∘ recip)"
  let ?R = "λt. Node (1, 1) (Node (1, 2) (?rssr t) (?rsrs t)) (Node (2, 1) (?srsr t) (?srrs t))"

  have *: "stern_brocot_recurse = ?R stern_brocot_recurse"
    by(rule tree.expand; simp; intro conjI; rule tree.expand; simp; intro conjI) ― ‹Expand the tree twice›
      (applicative_lifting, simp add: split_beta)+
  show "f = stern_brocot_recurse" when "f = ?R f" for f using that * by corec_unique
  show "odd_mirror bird = ?R (odd_mirror bird)"
    by(rule tree.expand; simp; intro conjI; rule tree.expand; simp; intro conjI) ― ‹Expand the tree twice›
      (applicative_lifting; simp)+
qed

theorem bird_rationals:
  assumes "m > 0" "n > 0"
  shows "root (traverse_tree (odd_mirror_path (mk_path m n)) (pure rat_of ⋄ bird)) = Fract (int m) (int n)"
using stern_brocot_rationals[OF assms]
by (simp add: odd_mirror_bird_stern_brocot[symmetric])

theorem bird_rationals_not_repeated:
  "root (traverse_tree path (pure rat_of ⋄ bird)) = root (traverse_tree path' (pure rat_of ⋄ bird))
  ⟹ path = path'"
using stern_brocot_rationals_not_repeated[where path="odd_mirror_path path" and path'="odd_mirror_path path'"]
by (simp add: odd_mirror_bird_stern_brocot[symmetric])

end