80 assume ?B |
82 assume ?B |
81 with Node show ?thesis by (auto simp: * atLeastAtMostSuc_conv) |
83 with Node show ?thesis by (auto simp: * atLeastAtMostSuc_conv) |
82 qed |
84 qed |
83 qed |
85 qed |
84 |
86 |
|
87 text "The other direction is more complicated. The following proof is due to Thomas Sewell." |
|
88 |
85 lemma disj_evens_odds: "(*) 2 ` A \<inter> Suc ` (*) 2 ` B = {}" |
89 lemma disj_evens_odds: "(*) 2 ` A \<inter> Suc ` (*) 2 ` B = {}" |
86 using double_not_eq_Suc_double by auto |
90 using double_not_eq_Suc_double by auto |
87 |
|
88 lemma Suc0_notin_double: "Suc 0 \<notin> (*) 2 ` A" |
|
89 by(auto) |
|
90 |
|
91 lemma zero_in_double_iff: "(0::nat) \<in> (*) 2 ` A \<longleftrightarrow> 0 \<in> A" |
|
92 by(auto) |
|
93 |
|
94 lemma Suc_in_Suc_image_iff: "Suc n \<in> Suc ` A \<longleftrightarrow> n \<in> A" |
|
95 by(auto) |
|
96 |
|
97 lemmas nat_in_image = Suc0_notin_double zero_in_double_iff Suc_in_Suc_image_iff |
|
98 |
91 |
99 lemma card_braun_indices: "card (braun_indices t) = size t" |
92 lemma card_braun_indices: "card (braun_indices t) = size t" |
100 proof (induction t) |
93 proof (induction t) |
101 case Leaf thus ?case by simp |
94 case Leaf thus ?case by simp |
102 next |
95 next |
103 case Node |
96 case Node |
104 thus ?case |
97 thus ?case |
105 by(auto simp: UNION_singleton_eq_range finite_braun_indices card_Un_disjoint |
98 by(auto simp: UNION_singleton_eq_range finite_braun_indices card_Un_disjoint |
106 card_insert_if disj_evens_odds card_image inj_on_def braun_indices1) |
99 card_insert_if disj_evens_odds card_image inj_on_def braun_indices1) |
107 qed |
100 qed |
|
101 |
|
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 |
108 |
194 |
109 lemma disj_union_eq_iff: |
195 lemma disj_union_eq_iff: |
110 "\<lbrakk> L1 \<inter> R2 = {}; L2 \<inter> R1 = {} \<rbrakk> \<Longrightarrow> L1 \<union> R1 = L2 \<union> R2 \<longleftrightarrow> L1 = L2 \<and> R1 = R2" |
196 "\<lbrakk> L1 \<inter> R2 = {}; L2 \<inter> R1 = {} \<rbrakk> \<Longrightarrow> L1 \<union> R1 = L2 \<union> R2 \<longleftrightarrow> L1 = L2 \<and> R1 = R2" |
111 by blast |
197 by blast |
112 |
198 |
233 then show ?case by simp |
319 then show ?case by simp |
234 next |
320 next |
235 case (Node t1 x2 t2) |
321 case (Node t1 x2 t2) |
236 have 1: "i > 0 \<Longrightarrow> Suc(Suc(2 * (i - Suc 0))) = 2*i" for i::nat by(simp add: algebra_simps) |
322 have 1: "i > 0 \<Longrightarrow> Suc(Suc(2 * (i - Suc 0))) = 2*i" for i::nat by(simp add: algebra_simps) |
237 have 2: "i > 0 \<Longrightarrow> 2 * (i - Suc 0) + 3 = 2*i + 1" 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) |
238 have 3: "(*) 2 ` braun_indices t1 \<union> Suc ` (*) 2 ` braun_indices t2 = |
324 have 3: "( * ) 2 ` braun_indices t1 \<union> Suc ` ( * ) 2 ` braun_indices t2 = |
239 {2..size t1 + size t2 + 1}" using Node.prems |
325 {2..size t1 + size t2 + 1}" using Node.prems |
240 by (simp add: insert_ident Icc_eq_insert_lb_nat nat_in_image braun_indices1) |
326 by (simp add: insert_ident Icc_eq_insert_lb_nat nat_in_image braun_indices1) |
241 thus ?case using Node.IH even_odd_decomp[OF _ _ 3] |
327 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 image_comp |
328 by(simp add: card_image inj_on_def card_braun_indices Let_def 1 2 inj_image_eq_iff image_comp |
243 cong: image_cong_simp) |
329 cong: image_cong_simp) |
244 qed |
330 qed |
245 |
331 *) |
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 |
332 |
249 end |
333 end |