49 assume "?B" |
49 assume "?B" |
50 thus ?thesis using Node by(intro balanced_Node_if_wbal1) auto |
50 thus ?thesis using Node by(intro balanced_Node_if_wbal1) auto |
51 qed |
51 qed |
52 qed |
52 qed |
53 |
53 |
|
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 abbreviation double :: "nat \<Rightarrow> nat" where |
|
60 "double \<equiv> (*) 2" |
|
61 |
|
62 abbreviation double1 :: "nat \<Rightarrow> nat" where |
|
63 "double1 \<equiv> \<lambda>n. Suc(2*n)" |
|
64 |
|
65 fun braun_indices :: "'a tree \<Rightarrow> nat set" where |
|
66 "braun_indices Leaf = {}" | |
|
67 "braun_indices (Node l _ r) = {1} \<union> double ` braun_indices l \<union> double1 ` braun_indices r" |
|
68 |
|
69 lemma braun_indices_if_braun: "braun t \<Longrightarrow> braun_indices t = {1..size t}" |
|
70 proof(induction t) |
|
71 case Leaf thus ?case by simp |
|
72 next |
|
73 have *: "double ` {a..b} \<union> double1 ` {a..b} = {2*a..2*b+1}" (is "?l = ?r") for a b |
|
74 proof |
|
75 show "?l \<subseteq> ?r" by auto |
|
76 next |
|
77 have "\<exists>x2\<in>{a..b}. x \<in> {Suc (2*x2), 2*x2}" if *: "x \<in> {2*a .. 2*b+1}" for x |
|
78 proof - |
|
79 have "x div 2 \<in> {a..b}" using * by auto |
|
80 moreover have "x \<in> {2 * (x div 2), Suc(2 * (x div 2))}" by auto |
|
81 ultimately show ?thesis by blast |
|
82 qed |
|
83 thus "?r \<subseteq> ?l" by fastforce |
|
84 qed |
|
85 case (Node l x r) |
|
86 hence "size l = size r \<or> size l = size r + 1" (is "?A \<or> ?B") by auto |
|
87 thus ?case |
|
88 proof |
|
89 assume ?A |
|
90 with Node show ?thesis by (auto simp: *) |
|
91 next |
|
92 assume ?B |
|
93 with Node show ?thesis by (auto simp: * atLeastAtMostSuc_conv) |
|
94 qed |
|
95 qed |
|
96 |
|
97 text \<open>How many even/odd natural numbers are there between m and n?\<close> |
|
98 |
|
99 lemma card_atLeastAtMost_even: |
|
100 "card {i \<in> {m..n::nat}. even i} = (n+1-m + (m+1) mod 2) div 2" (is "?l m n = ?r m n") |
|
101 proof(induction "n+1 - m" arbitrary: n m) |
|
102 case 0 thus ?case by simp |
|
103 next |
|
104 case Suc |
|
105 have "m \<le> n" using Suc(2) by arith |
|
106 hence "{m..n} = insert m {m+1..n}" by auto |
|
107 hence "?l m n = card {i \<in> insert m {m+1..n}. even i}" by simp |
|
108 also have "\<dots> = ?r m n" (is "?l = ?r") |
|
109 proof (cases) |
|
110 assume "even m" |
|
111 hence "{i \<in> insert m {m+1..n}. even i} = insert m {i \<in> {m+1..n}. even i}" by auto |
|
112 hence "?l = card {i \<in> {m+1..n}. even i} + 1" by simp |
|
113 also have "\<dots> = (n-m + (m+2) mod 2) div 2 + 1" using Suc(1)[of n "m+1"] Suc(2) by simp |
|
114 also have "\<dots> = ?r" using \<open>even m\<close> \<open>m \<le> n\<close> by auto |
|
115 finally show ?thesis . |
|
116 next |
|
117 assume "odd m" |
|
118 hence "{i \<in> insert m {m+1..n}. even i} = {i \<in> {m+1..n}. even i}" by auto |
|
119 hence "?l = card ..." by simp |
|
120 also have "\<dots> = (n-m + (m+2) mod 2) div 2" using Suc(1)[of n "m+1"] Suc(2) by simp |
|
121 also have "\<dots> = ?r" using \<open>odd m\<close> \<open>m \<le> n\<close> even_iff_mod_2_eq_zero[of m] by simp |
|
122 finally show ?thesis . |
|
123 qed |
|
124 finally show ?case . |
|
125 qed |
|
126 |
|
127 lemma card_atLeastAtMost_odd: "card {i \<in> {m..n::nat}. odd i} = (n+1-m + m mod 2) div 2" |
|
128 proof - |
|
129 let ?A = "{i \<in> {m..n}. odd i}" |
|
130 let ?B = "{i \<in> {m+1..n+1}. even i}" |
|
131 have "card ?A = card (Suc ` ?A)" by (simp add: card_image) |
|
132 also have "Suc ` ?A = ?B" using Suc_le_D by(force simp: image_iff) |
|
133 also have "card ?B = (n+1-m + (m) mod 2) div 2" |
|
134 using card_atLeastAtMost_even[of "m+1" "n+1"] by simp |
|
135 finally show ?thesis . |
|
136 qed |
|
137 |
|
138 lemma mod2_iff: "x mod 2 = (if even x then 0 else 1)" |
|
139 by (simp add: odd_iff_mod_2_eq_one) |
|
140 |
|
141 lemma compact_ivl_even: assumes "A = {i \<in> {m..n}. even i}" |
|
142 shows "A = (\<lambda>j. 2*(j-1) + m + m mod 2) ` {1..card A}" (is "_ = ?A") |
|
143 proof |
|
144 let ?a = "(n+1-m + (m+1) mod 2) div 2" |
|
145 have "\<exists>j \<in> {1..?a}. i = 2*(j-1) + m + m mod 2" if *: "i \<in> {m..n}" "even i" for i |
|
146 proof - |
|
147 let ?j = "(i - (m + m mod 2)) div 2 + 1" |
|
148 have "?j \<in> {1..?a} \<and> i = 2*(?j-1) + m + m mod 2" using * by(auto simp: mod2_iff) presburger+ |
|
149 thus ?thesis by blast |
|
150 qed |
|
151 thus "A \<subseteq> ?A" using assms |
|
152 by(auto simp: image_iff card_atLeastAtMost_even simp del: atLeastAtMost_iff) |
|
153 next |
|
154 let ?a = "(n+1-m + (m+1) mod 2) div 2" |
|
155 have 1: "2 * (j - 1) + m + m mod 2 \<in> {m..n}" if *: "j \<in> {1..?a}" for j |
|
156 using * by(auto simp: mod2_iff) |
|
157 have 2: "even (2 * (j - 1) + m + m mod 2)" for j by presburger |
|
158 show "?A \<subseteq> A" |
|
159 apply(simp add: assms card_atLeastAtMost_even del: atLeastAtMost_iff One_nat_def) |
|
160 using 1 2 by blast |
|
161 qed |
|
162 |
|
163 lemma compact_ivl_odd: |
|
164 assumes "B = {i \<in> {m..n}. odd i}" shows "B = (\<lambda>i. 2*(i-1) + m + (m+1) mod 2) ` {1..card B}" |
|
165 proof - |
|
166 define A :: " nat set" where "A = Suc ` B" |
|
167 have "A = {i \<in> {m+1..n+1}. even i}" |
|
168 using Suc_le_D by(force simp add: A_def assms image_iff) |
|
169 from compact_ivl_even[OF this] |
|
170 have "A = Suc ` (\<lambda>i. 2 * (i - 1) + m + (m + 1) mod 2) ` {1..card A}" |
|
171 by (simp add: image_comp o_def) |
|
172 hence B: "B = (\<lambda>i. 2 * (i - 1) + m + (m + 1) mod 2) ` {1..card A}" |
|
173 using A_def by (simp add: inj_image_eq_iff) |
|
174 have "card A = card B" by (metis A_def bij_betw_Suc bij_betw_same_card) |
|
175 with B show ?thesis by simp |
|
176 qed |
|
177 |
|
178 lemma even_odd_decomp: assumes "\<forall>x \<in> A. even x" "\<forall>x \<in> B. odd x" "A \<union> B = {m..n}" |
|
179 shows "(let a = card A; b = card B in |
|
180 a + b = n+1-m \<and> |
|
181 A = (\<lambda>i. 2*(i-1) + m + m mod 2) ` {1..a} \<and> |
|
182 B = (\<lambda>i. 2*(i-1) + m + (m+1) mod 2) ` {1..b} \<and> |
|
183 (a = b \<or> a = b+1 \<and> even m \<or> a+1 = b \<and> odd m))" |
|
184 proof - |
|
185 let ?a = "card A" let ?b = "card B" |
|
186 have "finite A \<and> finite B" |
|
187 by (metis \<open>A \<union> B = {m..n}\<close> finite_Un finite_atLeastAtMost) |
|
188 hence ab: "?a + ?b = Suc n - m" |
|
189 by (metis Int_emptyI assms card_Un_disjoint card_atLeastAtMost) |
|
190 have A: "A = {i \<in> {m..n}. even i}" using assms by auto |
|
191 hence A': "A = (\<lambda>i. 2*(i-1) + m + m mod 2) ` {1..?a}" by(rule compact_ivl_even) |
|
192 have B: "B = {i \<in> {m..n}. odd i}" using assms by auto |
|
193 hence B': "B = (\<lambda>i. 2*(i-1) + m + (m+1) mod 2) ` {1..?b}" by(rule compact_ivl_odd) |
|
194 have "?a = ?b \<or> ?a = ?b+1 \<and> even m \<or> ?a+1 = ?b \<and> odd m" |
|
195 apply(simp add: Let_def mod2_iff |
|
196 card_atLeastAtMost_even[of m n, simplified A[symmetric]] |
|
197 card_atLeastAtMost_odd[of m n, simplified B[symmetric]] split!: if_splits) |
|
198 by linarith |
|
199 with ab A' B' show ?thesis by simp |
|
200 qed |
|
201 |
|
202 lemma braun_indices1: "i \<in> braun_indices t \<Longrightarrow> i \<ge> 1" |
|
203 by (induction t arbitrary: i) auto |
|
204 |
|
205 lemma finite_braun_indices: "finite(braun_indices t)" |
|
206 by (induction t) auto |
|
207 |
|
208 lemma evens_odds_disj: "double ` braun_indices A \<inter> double1 ` B = {}" |
|
209 using double_not_eq_Suc_double by auto |
|
210 |
|
211 lemma card_braun_indices: "card (braun_indices t) = size t" |
|
212 proof (induction t) |
|
213 case Leaf thus ?case by simp |
|
214 next |
|
215 case Node |
|
216 thus ?case |
|
217 by(auto simp: UNION_singleton_eq_range finite_braun_indices card_Un_disjoint |
|
218 card_insert_if evens_odds_disj card_image inj_on_def dest: braun_indices1) |
|
219 qed |
|
220 |
|
221 lemma eq: "insert (Suc 0) M = {Suc 0..n} \<Longrightarrow> Suc 0 \<notin> M \<Longrightarrow> M = {2..n}" |
|
222 by (metis Suc_n_not_le_n atLeastAtMost_iff atLeastAtMost_insertL insertI1 insert_ident numeral_2_eq_2) |
|
223 |
|
224 lemma inj_on_Suc: "inj_on f N \<Longrightarrow> inj_on (\<lambda>n. Suc(f n)) N" |
|
225 by (simp add: inj_on_def) |
|
226 |
|
227 lemma braun_if_braun_indices: "braun_indices t = {1..size t} \<Longrightarrow> braun t" |
|
228 proof(induction t) |
|
229 case Leaf |
|
230 then show ?case by simp |
|
231 next |
|
232 case (Node t1 x2 t2) |
|
233 have 1: "i > 0 \<Longrightarrow> Suc(Suc(2 * (i - Suc 0))) = 2*i" for i::nat by(simp add: algebra_simps) |
|
234 have 2: "i > 0 \<Longrightarrow> 2 * (i - Suc 0) + 3 = 2*i + 1" for i::nat by(simp add: algebra_simps) |
|
235 have 3: "double ` braun_indices t1 \<union> double1 ` braun_indices t2 = |
|
236 {2..size t1 + size t2 + 1}" using Node.prems braun_indices1[of 0 t2] |
|
237 apply simp |
|
238 apply(drule eq) |
|
239 apply auto |
|
240 done |
|
241 thus ?case using Node.IH even_odd_decomp[OF _ _ 3] |
|
242 by(simp add: card_image inj_on_def card_braun_indices Let_def 1 2 inj_image_eq_iff |
|
243 cong: image_cong_strong) |
|
244 qed |
|
245 |
|
246 lemma braun_iff_braun_indices: "braun t \<longleftrightarrow> braun_indices t = {1..size t}" |
|
247 using braun_if_braun_indices braun_indices_if_braun by blast |
|
248 |
54 end |
249 end |