theory Braun_Tree imports"HOL-Library.Tree_Real" begin
text\<open>Braun Trees were studied by Braun and Rem~\<^cite>\<open>"BraunRem"\<close> and later Hoogerwoord~\<^cite>\<open>"Hoogerwoord"\<close>.\<close>
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\<open>The shape of a Braun-tree is uniquely determined by its size:\<close>
lemma braun_unique: "\ braun (t1::unit tree); braun t2; size t1 = size t2 \ \ t1 = t2" proof (induction t1 arbitrary: t2) case Leaf thus ?caseby simp next case (Node l1 _ r1) from Node.prems(3) have"t2 \ Leaf" by auto thenobtain 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 ?caseusing Node.prems(1,2) Node.IH by auto qed
text\<open>Braun trees are almost complete:\<close>
lemma acomplete_if_braun: "braun t \ acomplete t" proof(induction t) case Leaf show ?caseby (simp add: acomplete_def) next case (Node l x r) thus ?caseusing acomplete_Node_if_wbal2 by force qed
subsection \<open>Numbering Nodes\<close>
text\<open>We show that a tree is a Braun tree iff a parity-based
numbering (\<open>braun_indices\<close>) of nodes yields an interval of numbers.\<close>
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 ?caseby 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 moreoverhave"x \ {2 * (x div 2), Suc(2 * (x div 2))}" by auto ultimatelyshow ?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 ?caseby 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 thenshow ?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) thenshow ?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 thenshow ?caseby simp next case (Node l x r) obtain t where t: "t = Node l x r"by simp thenhave"insert (Suc 0) ((*) 2 ` braun_indices l \ Suc ` (*) 2 ` braun_indices r) \ {2..}
= {Suc 0..Suc (size l + size r)} \<inter> {2..}" by (metis Node.prems One_nat_def Suc_eq_plus1 Un_insert_left braun_indices.simps(2)
sup_bot_left tree.size(4)) thenhave 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) thenhave 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"] thenhave"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
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
