69133
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
section \<open>Braun Trees\<close>
|
|
4 |
|
|
5 |
theory Braun_Tree
|
|
6 |
imports "HOL-Library.Tree_Real"
|
|
7 |
begin
|
|
8 |
|
|
9 |
text \<open>Braun Trees were studied by Braun and Rem~\cite{BraunRem}
|
69192
|
10 |
and later Hoogerwoord~\cite{Hoogerwoord}.\<close>
|
69133
|
11 |
|
|
12 |
fun braun :: "'a tree \<Rightarrow> bool" where
|
|
13 |
"braun Leaf = True" |
|
69143
|
14 |
"braun (Node l x r) = ((size l = size r \<or> size l = size r + 1) \<and> braun l \<and> braun r)"
|
|
15 |
|
|
16 |
lemma braun_Node':
|
|
17 |
"braun (Node l x r) = (size r \<le> size l \<and> size l \<le> size r + 1 \<and> braun l \<and> braun r)"
|
|
18 |
by auto
|
69133
|
19 |
|
|
20 |
text \<open>The shape of a Braun-tree is uniquely determined by its size:\<close>
|
|
21 |
|
|
22 |
lemma braun_unique: "\<lbrakk> braun (t1::unit tree); braun t2; size t1 = size t2 \<rbrakk> \<Longrightarrow> t1 = t2"
|
|
23 |
proof (induction t1 arbitrary: t2)
|
|
24 |
case Leaf thus ?case by simp
|
|
25 |
next
|
|
26 |
case (Node l1 _ r1)
|
|
27 |
from Node.prems(3) have "t2 \<noteq> Leaf" by auto
|
|
28 |
then obtain l2 x2 r2 where [simp]: "t2 = Node l2 x2 r2" by (meson neq_Leaf_iff)
|
69143
|
29 |
with Node.prems have "size l1 = size l2 \<and> size r1 = size r2" by auto
|
69133
|
30 |
thus ?case using Node.prems(1,2) Node.IH by auto
|
|
31 |
qed
|
|
32 |
|
|
33 |
text \<open>Braun trees are balanced:\<close>
|
|
34 |
|
|
35 |
lemma balanced_if_braun: "braun t \<Longrightarrow> balanced t"
|
|
36 |
proof(induction t)
|
|
37 |
case Leaf show ?case by (simp add: balanced_def)
|
|
38 |
next
|
|
39 |
case (Node l x r)
|
|
40 |
have "size l = size r \<or> size l = size r + 1" (is "?A \<or> ?B")
|
69143
|
41 |
using Node.prems by simp
|
69133
|
42 |
thus ?case
|
|
43 |
proof
|
|
44 |
assume "?A"
|
|
45 |
thus ?thesis using Node
|
|
46 |
apply(simp add: balanced_def min_def max_def)
|
|
47 |
by (metis Node.IH balanced_optimal le_antisym le_refl)
|
|
48 |
next
|
|
49 |
assume "?B"
|
|
50 |
thus ?thesis using Node by(intro balanced_Node_if_wbal1) auto
|
|
51 |
qed
|
|
52 |
qed
|
|
53 |
|
69192
|
54 |
subsection \<open>Numbering Nodes\<close>
|
|
55 |
|
|
56 |
text \<open>We show that a tree is a Braun tree iff a parity-based
|
|
57 |
numbering (\<open>braun_indices\<close>) of nodes yields an interval of numbers.\<close>
|
|
58 |
|
|
59 |
fun braun_indices :: "'a tree \<Rightarrow> nat set" where
|
|
60 |
"braun_indices Leaf = {}" |
|
69195
|
61 |
"braun_indices (Node l _ r) = {1} \<union> (*) 2 ` braun_indices l \<union> Suc ` (*) 2 ` braun_indices r"
|
69192
|
62 |
|
|
63 |
lemma braun_indices_if_braun: "braun t \<Longrightarrow> braun_indices t = {1..size t}"
|
|
64 |
proof(induction t)
|
|
65 |
case Leaf thus ?case by simp
|
|
66 |
next
|
69195
|
67 |
have *: "(*) 2 ` {a..b} \<union> Suc ` (*) 2 ` {a..b} = {2*a..2*b+1}" (is "?l = ?r") for a b
|
69192
|
68 |
proof
|
|
69 |
show "?l \<subseteq> ?r" by auto
|
|
70 |
next
|
|
71 |
have "\<exists>x2\<in>{a..b}. x \<in> {Suc (2*x2), 2*x2}" if *: "x \<in> {2*a .. 2*b+1}" for x
|
|
72 |
proof -
|
|
73 |
have "x div 2 \<in> {a..b}" using * by auto
|
|
74 |
moreover have "x \<in> {2 * (x div 2), Suc(2 * (x div 2))}" by auto
|
|
75 |
ultimately show ?thesis by blast
|
|
76 |
qed
|
|
77 |
thus "?r \<subseteq> ?l" by fastforce
|
|
78 |
qed
|
|
79 |
case (Node l x r)
|
|
80 |
hence "size l = size r \<or> size l = size r + 1" (is "?A \<or> ?B") by auto
|
|
81 |
thus ?case
|
|
82 |
proof
|
|
83 |
assume ?A
|
|
84 |
with Node show ?thesis by (auto simp: *)
|
|
85 |
next
|
|
86 |
assume ?B
|
|
87 |
with Node show ?thesis by (auto simp: * atLeastAtMostSuc_conv)
|
|
88 |
qed
|
|
89 |
qed
|
|
90 |
|
|
91 |
text \<open>How many even/odd natural numbers are there between m and n?\<close>
|
|
92 |
|
|
93 |
lemma card_atLeastAtMost_even:
|
|
94 |
"card {i \<in> {m..n::nat}. even i} = (n+1-m + (m+1) mod 2) div 2" (is "?l m n = ?r m n")
|
|
95 |
proof(induction "n+1 - m" arbitrary: n m)
|
|
96 |
case 0 thus ?case by simp
|
|
97 |
next
|
|
98 |
case Suc
|
|
99 |
have "m \<le> n" using Suc(2) by arith
|
|
100 |
hence "{m..n} = insert m {m+1..n}" by auto
|
|
101 |
hence "?l m n = card {i \<in> insert m {m+1..n}. even i}" by simp
|
|
102 |
also have "\<dots> = ?r m n" (is "?l = ?r")
|
|
103 |
proof (cases)
|
|
104 |
assume "even m"
|
|
105 |
hence "{i \<in> insert m {m+1..n}. even i} = insert m {i \<in> {m+1..n}. even i}" by auto
|
|
106 |
hence "?l = card {i \<in> {m+1..n}. even i} + 1" by simp
|
|
107 |
also have "\<dots> = (n-m + (m+2) mod 2) div 2 + 1" using Suc(1)[of n "m+1"] Suc(2) by simp
|
|
108 |
also have "\<dots> = ?r" using \<open>even m\<close> \<open>m \<le> n\<close> by auto
|
|
109 |
finally show ?thesis .
|
|
110 |
next
|
|
111 |
assume "odd m"
|
|
112 |
hence "{i \<in> insert m {m+1..n}. even i} = {i \<in> {m+1..n}. even i}" by auto
|
|
113 |
hence "?l = card ..." by simp
|
|
114 |
also have "\<dots> = (n-m + (m+2) mod 2) div 2" using Suc(1)[of n "m+1"] Suc(2) by simp
|
|
115 |
also have "\<dots> = ?r" using \<open>odd m\<close> \<open>m \<le> n\<close> even_iff_mod_2_eq_zero[of m] by simp
|
|
116 |
finally show ?thesis .
|
|
117 |
qed
|
|
118 |
finally show ?case .
|
|
119 |
qed
|
|
120 |
|
|
121 |
lemma card_atLeastAtMost_odd: "card {i \<in> {m..n::nat}. odd i} = (n+1-m + m mod 2) div 2"
|
|
122 |
proof -
|
|
123 |
let ?A = "{i \<in> {m..n}. odd i}"
|
|
124 |
let ?B = "{i \<in> {m+1..n+1}. even i}"
|
|
125 |
have "card ?A = card (Suc ` ?A)" by (simp add: card_image)
|
|
126 |
also have "Suc ` ?A = ?B" using Suc_le_D by(force simp: image_iff)
|
|
127 |
also have "card ?B = (n+1-m + (m) mod 2) div 2"
|
|
128 |
using card_atLeastAtMost_even[of "m+1" "n+1"] by simp
|
|
129 |
finally show ?thesis .
|
|
130 |
qed
|
|
131 |
|
|
132 |
lemma mod2_iff: "x mod 2 = (if even x then 0 else 1)"
|
|
133 |
by (simp add: odd_iff_mod_2_eq_one)
|
|
134 |
|
|
135 |
lemma compact_ivl_even: assumes "A = {i \<in> {m..n}. even i}"
|
|
136 |
shows "A = (\<lambda>j. 2*(j-1) + m + m mod 2) ` {1..card A}" (is "_ = ?A")
|
|
137 |
proof
|
|
138 |
let ?a = "(n+1-m + (m+1) mod 2) div 2"
|
|
139 |
have "\<exists>j \<in> {1..?a}. i = 2*(j-1) + m + m mod 2" if *: "i \<in> {m..n}" "even i" for i
|
|
140 |
proof -
|
|
141 |
let ?j = "(i - (m + m mod 2)) div 2 + 1"
|
|
142 |
have "?j \<in> {1..?a} \<and> i = 2*(?j-1) + m + m mod 2" using * by(auto simp: mod2_iff) presburger+
|
|
143 |
thus ?thesis by blast
|
|
144 |
qed
|
|
145 |
thus "A \<subseteq> ?A" using assms
|
|
146 |
by(auto simp: image_iff card_atLeastAtMost_even simp del: atLeastAtMost_iff)
|
|
147 |
next
|
|
148 |
let ?a = "(n+1-m + (m+1) mod 2) div 2"
|
|
149 |
have 1: "2 * (j - 1) + m + m mod 2 \<in> {m..n}" if *: "j \<in> {1..?a}" for j
|
|
150 |
using * by(auto simp: mod2_iff)
|
|
151 |
have 2: "even (2 * (j - 1) + m + m mod 2)" for j by presburger
|
|
152 |
show "?A \<subseteq> A"
|
|
153 |
apply(simp add: assms card_atLeastAtMost_even del: atLeastAtMost_iff One_nat_def)
|
|
154 |
using 1 2 by blast
|
|
155 |
qed
|
|
156 |
|
|
157 |
lemma compact_ivl_odd:
|
|
158 |
assumes "B = {i \<in> {m..n}. odd i}" shows "B = (\<lambda>i. 2*(i-1) + m + (m+1) mod 2) ` {1..card B}"
|
|
159 |
proof -
|
|
160 |
define A :: " nat set" where "A = Suc ` B"
|
|
161 |
have "A = {i \<in> {m+1..n+1}. even i}"
|
|
162 |
using Suc_le_D by(force simp add: A_def assms image_iff)
|
|
163 |
from compact_ivl_even[OF this]
|
|
164 |
have "A = Suc ` (\<lambda>i. 2 * (i - 1) + m + (m + 1) mod 2) ` {1..card A}"
|
|
165 |
by (simp add: image_comp o_def)
|
|
166 |
hence B: "B = (\<lambda>i. 2 * (i - 1) + m + (m + 1) mod 2) ` {1..card A}"
|
|
167 |
using A_def by (simp add: inj_image_eq_iff)
|
|
168 |
have "card A = card B" by (metis A_def bij_betw_Suc bij_betw_same_card)
|
|
169 |
with B show ?thesis by simp
|
|
170 |
qed
|
|
171 |
|
|
172 |
lemma even_odd_decomp: assumes "\<forall>x \<in> A. even x" "\<forall>x \<in> B. odd x" "A \<union> B = {m..n}"
|
|
173 |
shows "(let a = card A; b = card B in
|
|
174 |
a + b = n+1-m \<and>
|
|
175 |
A = (\<lambda>i. 2*(i-1) + m + m mod 2) ` {1..a} \<and>
|
|
176 |
B = (\<lambda>i. 2*(i-1) + m + (m+1) mod 2) ` {1..b} \<and>
|
|
177 |
(a = b \<or> a = b+1 \<and> even m \<or> a+1 = b \<and> odd m))"
|
|
178 |
proof -
|
|
179 |
let ?a = "card A" let ?b = "card B"
|
|
180 |
have "finite A \<and> finite B"
|
|
181 |
by (metis \<open>A \<union> B = {m..n}\<close> finite_Un finite_atLeastAtMost)
|
|
182 |
hence ab: "?a + ?b = Suc n - m"
|
|
183 |
by (metis Int_emptyI assms card_Un_disjoint card_atLeastAtMost)
|
|
184 |
have A: "A = {i \<in> {m..n}. even i}" using assms by auto
|
|
185 |
hence A': "A = (\<lambda>i. 2*(i-1) + m + m mod 2) ` {1..?a}" by(rule compact_ivl_even)
|
|
186 |
have B: "B = {i \<in> {m..n}. odd i}" using assms by auto
|
|
187 |
hence B': "B = (\<lambda>i. 2*(i-1) + m + (m+1) mod 2) ` {1..?b}" by(rule compact_ivl_odd)
|
|
188 |
have "?a = ?b \<or> ?a = ?b+1 \<and> even m \<or> ?a+1 = ?b \<and> odd m"
|
|
189 |
apply(simp add: Let_def mod2_iff
|
|
190 |
card_atLeastAtMost_even[of m n, simplified A[symmetric]]
|
|
191 |
card_atLeastAtMost_odd[of m n, simplified B[symmetric]] split!: if_splits)
|
|
192 |
by linarith
|
|
193 |
with ab A' B' show ?thesis by simp
|
|
194 |
qed
|
|
195 |
|
|
196 |
lemma braun_indices1: "i \<in> braun_indices t \<Longrightarrow> i \<ge> 1"
|
|
197 |
by (induction t arbitrary: i) auto
|
|
198 |
|
|
199 |
lemma finite_braun_indices: "finite(braun_indices t)"
|
|
200 |
by (induction t) auto
|
|
201 |
|
69195
|
202 |
lemma evens_odds_disj: "(*) 2 ` braun_indices A \<inter> Suc ` (*) 2 ` B = {}"
|
69192
|
203 |
using double_not_eq_Suc_double by auto
|
|
204 |
|
|
205 |
lemma card_braun_indices: "card (braun_indices t) = size t"
|
|
206 |
proof (induction t)
|
|
207 |
case Leaf thus ?case by simp
|
|
208 |
next
|
|
209 |
case Node
|
|
210 |
thus ?case
|
|
211 |
by(auto simp: UNION_singleton_eq_range finite_braun_indices card_Un_disjoint
|
|
212 |
card_insert_if evens_odds_disj card_image inj_on_def dest: braun_indices1)
|
|
213 |
qed
|
|
214 |
|
|
215 |
lemma eq: "insert (Suc 0) M = {Suc 0..n} \<Longrightarrow> Suc 0 \<notin> M \<Longrightarrow> M = {2..n}"
|
|
216 |
by (metis Suc_n_not_le_n atLeastAtMost_iff atLeastAtMost_insertL insertI1 insert_ident numeral_2_eq_2)
|
|
217 |
|
|
218 |
lemma inj_on_Suc: "inj_on f N \<Longrightarrow> inj_on (\<lambda>n. Suc(f n)) N"
|
|
219 |
by (simp add: inj_on_def)
|
|
220 |
|
|
221 |
lemma braun_if_braun_indices: "braun_indices t = {1..size t} \<Longrightarrow> braun t"
|
|
222 |
proof(induction t)
|
|
223 |
case Leaf
|
|
224 |
then show ?case by simp
|
|
225 |
next
|
|
226 |
case (Node t1 x2 t2)
|
|
227 |
have 1: "i > 0 \<Longrightarrow> Suc(Suc(2 * (i - Suc 0))) = 2*i" for i::nat by(simp add: algebra_simps)
|
|
228 |
have 2: "i > 0 \<Longrightarrow> 2 * (i - Suc 0) + 3 = 2*i + 1" for i::nat by(simp add: algebra_simps)
|
69195
|
229 |
have 3: "(*) 2 ` braun_indices t1 \<union> Suc ` (*) 2 ` braun_indices t2 =
|
69192
|
230 |
{2..size t1 + size t2 + 1}" using Node.prems braun_indices1[of 0 t2]
|
|
231 |
apply simp
|
|
232 |
apply(drule eq)
|
|
233 |
apply auto
|
|
234 |
done
|
|
235 |
thus ?case using Node.IH even_odd_decomp[OF _ _ 3]
|
69195
|
236 |
by(simp add: card_image inj_on_def card_braun_indices Let_def 1 2 inj_image_eq_iff image_comp
|
69192
|
237 |
cong: image_cong_strong)
|
|
238 |
qed
|
|
239 |
|
|
240 |
lemma braun_iff_braun_indices: "braun t \<longleftrightarrow> braun_indices t = {1..size t}"
|
|
241 |
using braun_if_braun_indices braun_indices_if_braun by blast
|
|
242 |
|
69133
|
243 |
end |