author | wenzelm |
Sat, 25 May 2024 20:26:06 +0200 | |
changeset 80200 | 5f053991315c |
parent 76987 | 4c275405faae |
permissions | -rw-r--r-- |
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 |
||
76987 | 9 |
text \<open>Braun Trees were studied by Braun and Rem~\<^cite>\<open>"BraunRem"\<close> |
10 |
and later Hoogerwoord~\<^cite>\<open>"Hoogerwoord"\<close>.\<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 |
||
72566
831f17da1aab
renamed "balanced" -> "acomplete" because balanced has other meanings in the literature
nipkow
parents:
71294
diff
changeset
|
33 |
text \<open>Braun trees are almost complete:\<close> |
69133 | 34 |
|
72566
831f17da1aab
renamed "balanced" -> "acomplete" because balanced has other meanings in the literature
nipkow
parents:
71294
diff
changeset
|
35 |
lemma acomplete_if_braun: "braun t \<Longrightarrow> acomplete t" |
69133 | 36 |
proof(induction t) |
72566
831f17da1aab
renamed "balanced" -> "acomplete" because balanced has other meanings in the literature
nipkow
parents:
71294
diff
changeset
|
37 |
case Leaf show ?case by (simp add: acomplete_def) |
69133 | 38 |
next |
72566
831f17da1aab
renamed "balanced" -> "acomplete" because balanced has other meanings in the literature
nipkow
parents:
71294
diff
changeset
|
39 |
case (Node l x r) thus ?case using acomplete_Node_if_wbal2 by force |
69133 | 40 |
qed |
41 |
||
69192 | 42 |
subsection \<open>Numbering Nodes\<close> |
43 |
||
44 |
text \<open>We show that a tree is a Braun tree iff a parity-based |
|
45 |
numbering (\<open>braun_indices\<close>) of nodes yields an interval of numbers.\<close> |
|
46 |
||
47 |
fun braun_indices :: "'a tree \<Rightarrow> nat set" where |
|
48 |
"braun_indices Leaf = {}" | |
|
69195 | 49 |
"braun_indices (Node l _ r) = {1} \<union> (*) 2 ` braun_indices l \<union> Suc ` (*) 2 ` braun_indices r" |
69192 | 50 |
|
69196 | 51 |
lemma braun_indices1: "0 \<notin> braun_indices t" |
52 |
by (induction t) auto |
|
53 |
||
54 |
lemma finite_braun_indices: "finite(braun_indices t)" |
|
55 |
by (induction t) auto |
|
56 |
||
71294 | 57 |
text "One direction:" |
58 |
||
69192 | 59 |
lemma braun_indices_if_braun: "braun t \<Longrightarrow> braun_indices t = {1..size t}" |
60 |
proof(induction t) |
|
61 |
case Leaf thus ?case by simp |
|
62 |
next |
|
69195 | 63 |
have *: "(*) 2 ` {a..b} \<union> Suc ` (*) 2 ` {a..b} = {2*a..2*b+1}" (is "?l = ?r") for a b |
69192 | 64 |
proof |
65 |
show "?l \<subseteq> ?r" by auto |
|
66 |
next |
|
67 |
have "\<exists>x2\<in>{a..b}. x \<in> {Suc (2*x2), 2*x2}" if *: "x \<in> {2*a .. 2*b+1}" for x |
|
68 |
proof - |
|
69 |
have "x div 2 \<in> {a..b}" using * by auto |
|
70 |
moreover have "x \<in> {2 * (x div 2), Suc(2 * (x div 2))}" by auto |
|
71 |
ultimately show ?thesis by blast |
|
72 |
qed |
|
73 |
thus "?r \<subseteq> ?l" by fastforce |
|
74 |
qed |
|
75 |
case (Node l x r) |
|
76 |
hence "size l = size r \<or> size l = size r + 1" (is "?A \<or> ?B") by auto |
|
77 |
thus ?case |
|
78 |
proof |
|
79 |
assume ?A |
|
80 |
with Node show ?thesis by (auto simp: *) |
|
81 |
next |
|
82 |
assume ?B |
|
83 |
with Node show ?thesis by (auto simp: * atLeastAtMostSuc_conv) |
|
84 |
qed |
|
85 |
qed |
|
86 |
||
71294 | 87 |
text "The other direction is more complicated. The following proof is due to Thomas Sewell." |
88 |
||
69196 | 89 |
lemma disj_evens_odds: "(*) 2 ` A \<inter> Suc ` (*) 2 ` B = {}" |
90 |
using double_not_eq_Suc_double by auto |
|
91 |
||
92 |
lemma card_braun_indices: "card (braun_indices t) = size t" |
|
93 |
proof (induction t) |
|
94 |
case Leaf thus ?case by simp |
|
95 |
next |
|
96 |
case Node |
|
97 |
thus ?case |
|
98 |
by(auto simp: UNION_singleton_eq_range finite_braun_indices card_Un_disjoint |
|
99 |
card_insert_if disj_evens_odds card_image inj_on_def braun_indices1) |
|
100 |
qed |
|
101 |
||
71294 | 102 |
lemma braun_indices_intvl_base_1: |
103 |
assumes bi: "braun_indices t = {m..n}" |
|
104 |
shows "{m..n} = {1..size t}" |
|
105 |
proof (cases "t = Leaf") |
|
106 |
case True then show ?thesis using bi by simp |
|
107 |
next |
|
108 |
case False |
|
109 |
note eqs = eqset_imp_iff[OF bi] |
|
110 |
from eqs[of 0] have 0: "0 < m" |
|
111 |
by (simp add: braun_indices1) |
|
112 |
from eqs[of 1] have 1: "m \<le> 1" |
|
113 |
by (cases t; simp add: False) |
|
114 |
from 0 1 have eq1: "m = 1" by simp |
|
115 |
from card_braun_indices[of t] show ?thesis |
|
116 |
by (simp add: bi eq1) |
|
117 |
qed |
|
118 |
||
119 |
lemma even_of_intvl_intvl: |
|
120 |
fixes S :: "nat set" |
|
121 |
assumes "S = {m..n} \<inter> {i. even i}" |
|
122 |
shows "\<exists>m' n'. S = (\<lambda>i. i * 2) ` {m'..n'}" |
|
123 |
apply (rule exI[where x="Suc m div 2"], rule exI[where x="n div 2"]) |
|
124 |
apply (fastforce simp add: assms mult.commute) |
|
125 |
done |
|
126 |
||
127 |
lemma odd_of_intvl_intvl: |
|
128 |
fixes S :: "nat set" |
|
129 |
assumes "S = {m..n} \<inter> {i. odd i}" |
|
130 |
shows "\<exists>m' n'. S = Suc ` (\<lambda>i. i * 2) ` {m'..n'}" |
|
131 |
proof - |
|
132 |
have step1: "\<exists>m'. S = Suc ` ({m'..n - 1} \<inter> {i. even i})" |
|
133 |
apply (rule_tac x="if n = 0 then 1 else m - 1" in exI) |
|
134 |
apply (auto simp: assms image_def elim!: oddE) |
|
135 |
done |
|
136 |
thus ?thesis |
|
137 |
by (metis even_of_intvl_intvl) |
|
138 |
qed |
|
139 |
||
140 |
lemma image_int_eq_image: |
|
141 |
"(\<forall>i \<in> S. f i \<in> T) \<Longrightarrow> (f ` S) \<inter> T = f ` S" |
|
142 |
"(\<forall>i \<in> S. f i \<notin> T) \<Longrightarrow> (f ` S) \<inter> T = {}" |
|
143 |
by auto |
|
144 |
||
145 |
lemma braun_indices1_le: |
|
146 |
"i \<in> braun_indices t \<Longrightarrow> Suc 0 \<le> i" |
|
147 |
using braun_indices1 not_less_eq_eq by blast |
|
148 |
||
149 |
lemma braun_if_braun_indices: "braun_indices t = {1..size t} \<Longrightarrow> braun t" |
|
150 |
proof(induction t) |
|
151 |
case Leaf |
|
152 |
then show ?case by simp |
|
153 |
next |
|
154 |
case (Node l x r) |
|
155 |
obtain t where t: "t = Node l x r" by simp |
|
156 |
from Node.prems have eq: "{2 .. size t} = (\<lambda>i. i * 2) ` braun_indices l \<union> Suc ` (\<lambda>i. i * 2) ` braun_indices r" |
|
157 |
(is "?R = ?S \<union> ?T") |
|
158 |
apply clarsimp |
|
159 |
apply (drule_tac f="\<lambda>S. S \<inter> {2..}" in arg_cong) |
|
160 |
apply (simp add: t mult.commute Int_Un_distrib2 image_int_eq_image braun_indices1_le) |
|
161 |
done |
|
162 |
then have ST: "?S = ?R \<inter> {i. even i}" "?T = ?R \<inter> {i. odd i}" |
|
163 |
by (simp_all add: Int_Un_distrib2 image_int_eq_image) |
|
164 |
from ST have l: "braun_indices l = {1 .. size l}" |
|
165 |
by (fastforce dest: braun_indices_intvl_base_1 dest!: even_of_intvl_intvl |
|
166 |
simp: mult.commute inj_image_eq_iff[OF inj_onI]) |
|
167 |
from ST have r: "braun_indices r = {1 .. size r}" |
|
168 |
by (fastforce dest: braun_indices_intvl_base_1 dest!: odd_of_intvl_intvl |
|
169 |
simp: mult.commute inj_image_eq_iff[OF inj_onI]) |
|
170 |
note STa = ST[THEN eqset_imp_iff, THEN iffD2] |
|
171 |
note STb = STa[of "size t"] STa[of "size t - 1"] |
|
172 |
then have sizes: "size l = size r \<or> size l = size r + 1" |
|
173 |
apply (clarsimp simp: t l r inj_image_mem_iff[OF inj_onI]) |
|
174 |
apply (cases "even (size l)"; cases "even (size r)"; clarsimp elim!: oddE; fastforce) |
|
175 |
done |
|
176 |
from l r sizes show ?case |
|
177 |
by (clarsimp simp: Node.IH) |
|
178 |
qed |
|
179 |
||
180 |
lemma braun_iff_braun_indices: "braun t \<longleftrightarrow> braun_indices t = {1..size t}" |
|
181 |
using braun_if_braun_indices braun_indices_if_braun by blast |
|
182 |
||
183 |
(* An older less appealing proof: |
|
184 |
lemma Suc0_notin_double: "Suc 0 \<notin> ( * ) 2 ` A" |
|
185 |
by(auto) |
|
186 |
||
187 |
lemma zero_in_double_iff: "(0::nat) \<in> ( * ) 2 ` A \<longleftrightarrow> 0 \<in> A" |
|
188 |
by(auto) |
|
189 |
||
190 |
lemma Suc_in_Suc_image_iff: "Suc n \<in> Suc ` A \<longleftrightarrow> n \<in> A" |
|
191 |
by(auto) |
|
192 |
||
193 |
lemmas nat_in_image = Suc0_notin_double zero_in_double_iff Suc_in_Suc_image_iff |
|
194 |
||
69197 | 195 |
lemma disj_union_eq_iff: |
196 |
"\<lbrakk> L1 \<inter> R2 = {}; L2 \<inter> R1 = {} \<rbrakk> \<Longrightarrow> L1 \<union> R1 = L2 \<union> R2 \<longleftrightarrow> L1 = L2 \<and> R1 = R2" |
|
197 |
by blast |
|
198 |
||
199 |
lemma inj_braun_indices: "braun_indices t1 = braun_indices t2 \<Longrightarrow> t1 = (t2::unit tree)" |
|
200 |
proof(induction t1 arbitrary: t2) |
|
201 |
case Leaf thus ?case using braun_indices.elims by blast |
|
202 |
next |
|
203 |
case (Node l1 x1 r1) |
|
204 |
have "t2 \<noteq> Leaf" |
|
205 |
proof |
|
206 |
assume "t2 = Leaf" |
|
207 |
with Node.prems show False by simp |
|
208 |
qed |
|
209 |
thus ?case using Node |
|
210 |
by (auto simp: neq_Leaf_iff insert_ident nat_in_image braun_indices1 |
|
211 |
disj_union_eq_iff disj_evens_odds inj_image_eq_iff inj_def) |
|
212 |
qed |
|
213 |
||
69192 | 214 |
text \<open>How many even/odd natural numbers are there between m and n?\<close> |
215 |
||
69200 | 216 |
lemma card_Icc_even_nat: |
69192 | 217 |
"card {i \<in> {m..n::nat}. even i} = (n+1-m + (m+1) mod 2) div 2" (is "?l m n = ?r m n") |
218 |
proof(induction "n+1 - m" arbitrary: n m) |
|
219 |
case 0 thus ?case by simp |
|
220 |
next |
|
221 |
case Suc |
|
222 |
have "m \<le> n" using Suc(2) by arith |
|
223 |
hence "{m..n} = insert m {m+1..n}" by auto |
|
224 |
hence "?l m n = card {i \<in> insert m {m+1..n}. even i}" by simp |
|
225 |
also have "\<dots> = ?r m n" (is "?l = ?r") |
|
226 |
proof (cases) |
|
227 |
assume "even m" |
|
228 |
hence "{i \<in> insert m {m+1..n}. even i} = insert m {i \<in> {m+1..n}. even i}" by auto |
|
229 |
hence "?l = card {i \<in> {m+1..n}. even i} + 1" by simp |
|
230 |
also have "\<dots> = (n-m + (m+2) mod 2) div 2 + 1" using Suc(1)[of n "m+1"] Suc(2) by simp |
|
231 |
also have "\<dots> = ?r" using \<open>even m\<close> \<open>m \<le> n\<close> by auto |
|
232 |
finally show ?thesis . |
|
233 |
next |
|
234 |
assume "odd m" |
|
235 |
hence "{i \<in> insert m {m+1..n}. even i} = {i \<in> {m+1..n}. even i}" by auto |
|
236 |
hence "?l = card ..." by simp |
|
237 |
also have "\<dots> = (n-m + (m+2) mod 2) div 2" using Suc(1)[of n "m+1"] Suc(2) by simp |
|
238 |
also have "\<dots> = ?r" using \<open>odd m\<close> \<open>m \<le> n\<close> even_iff_mod_2_eq_zero[of m] by simp |
|
239 |
finally show ?thesis . |
|
240 |
qed |
|
241 |
finally show ?case . |
|
242 |
qed |
|
243 |
||
69200 | 244 |
lemma card_Icc_odd_nat: "card {i \<in> {m..n::nat}. odd i} = (n+1-m + m mod 2) div 2" |
69192 | 245 |
proof - |
246 |
let ?A = "{i \<in> {m..n}. odd i}" |
|
247 |
let ?B = "{i \<in> {m+1..n+1}. even i}" |
|
248 |
have "card ?A = card (Suc ` ?A)" by (simp add: card_image) |
|
249 |
also have "Suc ` ?A = ?B" using Suc_le_D by(force simp: image_iff) |
|
250 |
also have "card ?B = (n+1-m + (m) mod 2) div 2" |
|
69200 | 251 |
using card_Icc_even_nat[of "m+1" "n+1"] by simp |
69192 | 252 |
finally show ?thesis . |
253 |
qed |
|
254 |
||
69200 | 255 |
lemma compact_Icc_even: assumes "A = {i \<in> {m..n}. even i}" |
69192 | 256 |
shows "A = (\<lambda>j. 2*(j-1) + m + m mod 2) ` {1..card A}" (is "_ = ?A") |
257 |
proof |
|
258 |
let ?a = "(n+1-m + (m+1) mod 2) div 2" |
|
259 |
have "\<exists>j \<in> {1..?a}. i = 2*(j-1) + m + m mod 2" if *: "i \<in> {m..n}" "even i" for i |
|
260 |
proof - |
|
261 |
let ?j = "(i - (m + m mod 2)) div 2 + 1" |
|
69198 | 262 |
have "?j \<in> {1..?a} \<and> i = 2*(?j-1) + m + m mod 2" using * by(auto simp: mod2_eq_if) presburger+ |
69192 | 263 |
thus ?thesis by blast |
264 |
qed |
|
265 |
thus "A \<subseteq> ?A" using assms |
|
69200 | 266 |
by(auto simp: image_iff card_Icc_even_nat simp del: atLeastAtMost_iff) |
69192 | 267 |
next |
268 |
let ?a = "(n+1-m + (m+1) mod 2) div 2" |
|
269 |
have 1: "2 * (j - 1) + m + m mod 2 \<in> {m..n}" if *: "j \<in> {1..?a}" for j |
|
69198 | 270 |
using * by(auto simp: mod2_eq_if) |
69192 | 271 |
have 2: "even (2 * (j - 1) + m + m mod 2)" for j by presburger |
272 |
show "?A \<subseteq> A" |
|
69200 | 273 |
apply(simp add: assms card_Icc_even_nat del: atLeastAtMost_iff One_nat_def) |
69192 | 274 |
using 1 2 by blast |
275 |
qed |
|
276 |
||
69200 | 277 |
lemma compact_Icc_odd: |
69192 | 278 |
assumes "B = {i \<in> {m..n}. odd i}" shows "B = (\<lambda>i. 2*(i-1) + m + (m+1) mod 2) ` {1..card B}" |
279 |
proof - |
|
280 |
define A :: " nat set" where "A = Suc ` B" |
|
281 |
have "A = {i \<in> {m+1..n+1}. even i}" |
|
282 |
using Suc_le_D by(force simp add: A_def assms image_iff) |
|
69200 | 283 |
from compact_Icc_even[OF this] |
69192 | 284 |
have "A = Suc ` (\<lambda>i. 2 * (i - 1) + m + (m + 1) mod 2) ` {1..card A}" |
285 |
by (simp add: image_comp o_def) |
|
286 |
hence B: "B = (\<lambda>i. 2 * (i - 1) + m + (m + 1) mod 2) ` {1..card A}" |
|
287 |
using A_def by (simp add: inj_image_eq_iff) |
|
288 |
have "card A = card B" by (metis A_def bij_betw_Suc bij_betw_same_card) |
|
289 |
with B show ?thesis by simp |
|
290 |
qed |
|
291 |
||
292 |
lemma even_odd_decomp: assumes "\<forall>x \<in> A. even x" "\<forall>x \<in> B. odd x" "A \<union> B = {m..n}" |
|
293 |
shows "(let a = card A; b = card B in |
|
294 |
a + b = n+1-m \<and> |
|
295 |
A = (\<lambda>i. 2*(i-1) + m + m mod 2) ` {1..a} \<and> |
|
296 |
B = (\<lambda>i. 2*(i-1) + m + (m+1) mod 2) ` {1..b} \<and> |
|
297 |
(a = b \<or> a = b+1 \<and> even m \<or> a+1 = b \<and> odd m))" |
|
298 |
proof - |
|
299 |
let ?a = "card A" let ?b = "card B" |
|
300 |
have "finite A \<and> finite B" |
|
301 |
by (metis \<open>A \<union> B = {m..n}\<close> finite_Un finite_atLeastAtMost) |
|
302 |
hence ab: "?a + ?b = Suc n - m" |
|
303 |
by (metis Int_emptyI assms card_Un_disjoint card_atLeastAtMost) |
|
304 |
have A: "A = {i \<in> {m..n}. even i}" using assms by auto |
|
69200 | 305 |
hence A': "A = (\<lambda>i. 2*(i-1) + m + m mod 2) ` {1..?a}" by(rule compact_Icc_even) |
69192 | 306 |
have B: "B = {i \<in> {m..n}. odd i}" using assms by auto |
69200 | 307 |
hence B': "B = (\<lambda>i. 2*(i-1) + m + (m+1) mod 2) ` {1..?b}" by(rule compact_Icc_odd) |
69192 | 308 |
have "?a = ?b \<or> ?a = ?b+1 \<and> even m \<or> ?a+1 = ?b \<and> odd m" |
69198 | 309 |
apply(simp add: Let_def mod2_eq_if |
69200 | 310 |
card_Icc_even_nat[of m n, simplified A[symmetric]] |
311 |
card_Icc_odd_nat[of m n, simplified B[symmetric]] split!: if_splits) |
|
69192 | 312 |
by linarith |
313 |
with ab A' B' show ?thesis by simp |
|
314 |
qed |
|
315 |
||
316 |
lemma braun_if_braun_indices: "braun_indices t = {1..size t} \<Longrightarrow> braun t" |
|
317 |
proof(induction t) |
|
318 |
case Leaf |
|
319 |
then show ?case by simp |
|
320 |
next |
|
321 |
case (Node t1 x2 t2) |
|
322 |
have 1: "i > 0 \<Longrightarrow> Suc(Suc(2 * (i - Suc 0))) = 2*i" for i::nat by(simp add: algebra_simps) |
|
323 |
have 2: "i > 0 \<Longrightarrow> 2 * (i - Suc 0) + 3 = 2*i + 1" for i::nat by(simp add: algebra_simps) |
|
71294 | 324 |
have 3: "( * ) 2 ` braun_indices t1 \<union> Suc ` ( * ) 2 ` braun_indices t2 = |
69196 | 325 |
{2..size t1 + size t2 + 1}" using Node.prems |
326 |
by (simp add: insert_ident Icc_eq_insert_lb_nat nat_in_image braun_indices1) |
|
69192 | 327 |
thus ?case using Node.IH even_odd_decomp[OF _ _ 3] |
69195 | 328 |
by(simp add: card_image inj_on_def card_braun_indices Let_def 1 2 inj_image_eq_iff image_comp |
69546
27dae626822b
prefer naming convention from datatype package for strong congruence rules
haftmann
parents:
69200
diff
changeset
|
329 |
cong: image_cong_simp) |
69192 | 330 |
qed |
71294 | 331 |
*) |
69192 | 332 |
|
69133 | 333 |
end |