149 show ?thesis by (auto intro: fine_Nil) |
148 show ?thesis by (auto intro: fine_Nil) |
150 next |
149 next |
151 case (Cons d1 D1') |
150 case (Cons d1 D1') |
152 with induct(2)[OF `D2 \<noteq> []`, of D1'] induct(8) |
151 with induct(2)[OF `D2 \<noteq> []`, of D1'] induct(8) |
153 have "fine \<delta> (b, fst (hd D2)) D1'" and "fine \<delta> (fst (hd D2), c) D2" and |
152 have "fine \<delta> (b, fst (hd D2)) D1'" and "fine \<delta> (fst (hd D2), c) D2" and |
154 "d1 = (a', x, b)" by auto |
153 "d1 = (a', x, b)" by auto |
155 with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons |
154 with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons |
156 show ?thesis by auto |
155 show ?thesis by auto |
157 qed |
156 qed |
158 qed auto |
157 qed auto |
159 thus ?fine1 and ?fine2 by auto |
158 thus ?fine1 and ?fine2 by auto |
379 |
378 |
380 have "fine \<delta>1 (a,b) D1" unfolding D1_def |
379 have "fine \<delta>1 (a,b) D1" unfolding D1_def |
381 proof (rule fine_append) |
380 proof (rule fine_append) |
382 show "fine \<delta>1 (a, d) ?D1" |
381 show "fine \<delta>1 (a, d) ?D1" |
383 proof (rule fine1[THEN fine_\<delta>_expand]) |
382 proof (rule fine1[THEN fine_\<delta>_expand]) |
384 fix x assume "a \<le> x" "x \<le> d" |
383 fix x assume "a \<le> x" "x \<le> d" |
385 hence "x \<le> b" using `d < b` `x \<le> d` by auto |
384 hence "x \<le> b" using `d < b` `x \<le> d` by auto |
386 thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto |
385 thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto |
387 qed |
386 qed |
388 |
387 |
389 have "b - d < \<delta>1 t" |
388 have "b - d < \<delta>1 t" |
390 using mem_fine3[OF fine in_D] \<delta>_def `b \<le> e` `t = b` by auto |
389 using mem_fine3[OF fine in_D] \<delta>_def `b \<le> e` `t = b` by auto |
391 from `d < b` `d \<le> t` `t = b` this |
390 from `d < b` `d \<le> t` `t = b` this |
392 show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto |
391 show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto |
393 qed |
392 qed |
394 note rsum1 = I1[OF this] |
393 note rsum1 = I1[OF this] |
395 |
394 |
408 from fine_single_boundaries[OF *(1)] |
407 from fine_single_boundaries[OF *(1)] |
409 have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto |
408 have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto |
410 with *(2) have "fine \<delta> (e,c) (drop (Suc N) D)" by auto |
409 with *(2) have "fine \<delta> (e,c) (drop (Suc N) D)" by auto |
411 thus ?thesis |
410 thus ?thesis |
412 proof (rule fine_\<delta>_expand) |
411 proof (rule fine_\<delta>_expand) |
413 fix x assume "e \<le> x" and "x \<le> c" |
412 fix x assume "e \<le> x" and "x \<le> c" |
414 thus "\<delta> x \<le> \<delta>2 x" using `b \<le> e` unfolding \<delta>_def by auto |
413 thus "\<delta> x \<le> \<delta>2 x" using `b \<le> e` unfolding \<delta>_def by auto |
415 qed |
414 qed |
416 qed |
415 qed |
417 |
416 |
418 have "fine \<delta>2 (b, c) D2" |
417 have "fine \<delta>2 (b, c) D2" |
419 proof (cases "e = b") |
418 proof (cases "e = b") |
420 case True thus ?thesis using fine2 by (simp add: D1_def D2_def) |
419 case True thus ?thesis using fine2 by (simp add: D1_def D2_def) |
421 next |
420 next |
422 case False |
421 case False |
423 have "e - b < \<delta>2 b" |
422 have "e - b < \<delta>2 b" |
424 using mem_fine3[OF fine in_D] \<delta>_def `d < b` `t = b` by auto |
423 using mem_fine3[OF fine in_D] \<delta>_def `d < b` `t = b` by auto |
425 with False `t = b` `b \<le> e` |
424 with False `t = b` `b \<le> e` |
426 show ?thesis using D2_def |
425 show ?thesis using D2_def |
427 by (auto intro!: fine_append[OF _ fine2] fine_single |
426 by (auto intro!: fine_append[OF _ fine2] fine_single |
428 simp del: append_Cons) |
427 simp del: append_Cons) |
429 qed |
428 qed |
430 note rsum2 = I2[OF this] |
429 note rsum2 = I2[OF this] |
431 |
430 |
432 have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f" |
431 have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f" |
433 using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto |
432 using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto |