(* Author: Tobias Nipkow *)
section ‹Braun Trees
›
theory Braun_Tree
imports "HOL-Library.Tree_Real"
begin
text ‹Braun Trees were studied
by Braun
and Rem~
🍋‹"BraunRem"›
and later Hoogerwoord~
🍋‹"Hoogerwoord"›.
›
fun braun ::
"'a tree \ bool" where
"braun Leaf = True" |
"braun (Node l x r) = ((size l = size r \ size l = size r + 1) \ braun l \ braun r)"
lemma braun_Node
':
"braun (Node l x r) = (size r \ size l \ size l \ size r + 1 \ braun l \ braun r)"
by auto
text ‹The shape of a Braun-tree
is uniquely determined
by its size:
›
lemma braun_unique:
"\ braun (t1::unit tree); braun t2; size t1 = size t2 \ \ t1 = t2"
proof (
induction t1 arbitrary: t2)
case Leaf
thus ?
case by simp
next
case (Node l1 _ r1)
from Node.prems(3)
have "t2 \ Leaf" by auto
then obtain l2 x2 r2
where [simp]:
"t2 = Node l2 x2 r2" by (meson neq_Leaf_iff)
with Node.prems
have "size l1 = size l2 \ size r1 = size r2" by auto
thus ?
case using Node.prems(1,2) Node.IH
by auto
qed
text ‹Braun trees are almost complete:
›
lemma acomplete_if_braun:
"braun t \ acomplete t"
proof(
induction t)
case Leaf
show ?
case by (simp add: acomplete_def)
next
case (Node l x r)
thus ?
case using acomplete_Node_if_wbal2
by force
qed
subsection ‹Numbering Nodes
›
text ‹We
show that a tree
is a Braun tree iff a parity-based
numbering (
‹braun_indices
›) of nodes yields an interval of numbers.
›
fun braun_indices ::
"'a tree \ nat set" where
"braun_indices Leaf = {}" |
"braun_indices (Node l _ r) = {1} \ (*) 2 ` braun_indices l \ Suc ` (*) 2 ` braun_indices r"
lemma braun_indices1:
"0 \ braun_indices t"
by (
induction t) auto
lemma finite_braun_indices:
"finite(braun_indices t)"
by (
induction t) auto
text "One direction:"
lemma braun_indices_if_braun:
"braun t \ braun_indices t = {1..size t}"
proof(
induction t)
case Leaf
thus ?
case by simp
next
have *:
"(*) 2 ` {a..b} \ Suc ` (*) 2 ` {a..b} = {2*a..2*b+1}" (is "?l = ?r") for a b
proof
show "?l \ ?r" by auto
next
have "\x2\{a..b}. x \ {Suc (2*x2), 2*x2}" if *:
"x \ {2*a .. 2*b+1}" for x
proof -
have "x div 2 \ {a..b}" using *
by auto
moreover have "x \ {2 * (x div 2), Suc(2 * (x div 2))}" by auto
ultimately show ?thesis
by blast
qed
thus "?r \ ?l" by fastforce
qed
case (Node l x r)
hence "size l = size r \ size l = size r + 1" (
is "?A \ ?B")
by auto
thus ?
case
proof
assume ?A
with Node
show ?thesis
by (auto simp: *)
next
assume ?B
with Node
show ?thesis
by (auto simp: * atLeastAtMostSuc_conv)
qed
qed
text "The other direction is more complicated. The following proof is due to Thomas Sewell."
lemma disj_evens_odds:
"(*) 2 ` A \ Suc ` (*) 2 ` B = {}"
using double_not_eq_Suc_double
by auto
lemma card_braun_indices:
"card (braun_indices t) = size t"
proof (
induction t)
case Leaf
thus ?
case by simp
next
case Node
thus ?
case
by(auto simp: UNION_singleton_eq_range finite_braun_indices card_Un_disjoint
card_insert_if disj_evens_odds card_image inj_on_def braun_indices1)
qed
lemma braun_indices_intvl_base_1:
assumes bi:
"braun_indices t = {m..n}"
shows "{m..n} = {1..size t}"
proof (cases
"t = Leaf")
case True
then show ?thesis
using bi
by simp
next
case False
note eqs = eqset_imp_iff[OF bi]
from eqs[of 0]
have 0:
"0 < m"
by (simp add: braun_indices1)
from eqs[of 1]
have 1:
"m \ 1"
by (cases t; simp add: False)
from 0 1
have eq1:
"m = 1" by simp
from card_braun_indices[of t]
show ?thesis
by (simp add: bi eq1)
qed
lemma even_of_intvl_intvl:
fixes S ::
"nat set"
assumes "S = {m..n} \ {i. even i}"
shows "\m' n'. S = (\i. i * 2) ` {m'..n'}"
proof -
have "S = (\i. i * 2) ` {Suc m div 2..n div 2}"
by (fastforce simp add: assms mult.commute)
then show ?thesis
by blast
qed
lemma odd_of_intvl_intvl:
fixes S ::
"nat set"
assumes "S = {m..n} \ {i. odd i}"
shows "\m' n'. S = Suc ` (\i. i * 2) ` {m'..n'}"
proof -
have "S = Suc ` ({if n = 0 then 1 else m - 1..n - 1} \ Collect even)"
by (auto simp: assms image_def elim!: oddE)
thus ?thesis
by (metis even_of_intvl_intvl)
qed
lemma image_int_eq_image:
"(\i \ S. f i \ T) \ (f ` S) \ T = f ` S"
"(\i \ S. f i \ T) \ (f ` S) \ T = {}"
by auto
lemma braun_indices1_le:
"i \ braun_indices t \ Suc 0 \ i"
using braun_indices1 not_less_eq_eq
by blast
lemma braun_if_braun_indices:
"braun_indices t = {1..size t} \ braun t"
proof(
induction t)
case Leaf
then show ?
case by simp
next
case (Node l x r)
obtain t
where t:
"t = Node l x r" by simp
then have "insert (Suc 0) ((*) 2 ` braun_indices l \ Suc ` (*) 2 ` braun_indices r) \ {2..}
= {Suc 0..Suc (size l + size r)}
∩ {2..}
"
by (metis Node.prems One_nat_def Suc_eq_plus1 Un_insert_left braun_indices.simps(2)
sup_bot_left tree.size(4))
then have eq:
"{2 .. size t} = (\i. i * 2) ` braun_indices l \ Suc ` (\i. i * 2) ` braun_indices r"
(
is "?R = ?S \ ?T")
by (simp add: t mult.commute Int_Un_distrib2 image_int_eq_image braun_indices1_le)
then have ST:
"?S = ?R \ {i. even i}" "?T = ?R \ {i. odd i}"
by (simp_all add: Int_Un_distrib2 image_int_eq_image)
from ST
have l:
"braun_indices l = {1 .. size l}"
by (fastforce dest: braun_indices_intvl_base_1 dest!: even_of_intvl_intvl
simp: mult.commute inj_image_eq_iff[OF inj_onI])
from ST
have r:
"braun_indices r = {1 .. size r}"
by (fastforce dest: braun_indices_intvl_base_1 dest!: odd_of_intvl_intvl
simp: mult.commute inj_image_eq_iff[OF inj_onI])
note STa = ST[
THEN eqset_imp_iff,
THEN iffD2]
note STb = STa[of
"size t"] STa[of
"size t - 1"]
then have "size l = size r \ size l = size r + 1"
using t l r
by atomize auto
with l r
show ?
case
by (clarsimp simp: Node.IH)
qed
lemma braun_iff_braun_indices:
"braun t \ braun_indices t = {1..size t}"
using braun_if_braun_indices braun_indices_if_braun
by blast
end
