351 unfolding dyadics_def |
343 unfolding dyadics_def |
352 apply clarify |
344 apply clarify |
353 apply (rule dyadic_413_cases, force+) |
345 apply (rule dyadic_413_cases, force+) |
354 done |
346 done |
355 next |
347 next |
356 show "?rhs \<subseteq> dyadics" |
348 have "range of_nat \<subseteq> (\<Union>k m. {(of_nat m::'a) / 2 ^ k})" |
357 apply (clarsimp simp: dyadics_def Nats_def simp del: power_Suc) |
349 by clarsimp (metis divide_numeral_1 numeral_One power_0) |
358 apply (intro conjI subsetI) |
350 moreover have "\<And>k m. \<exists>k' m'. ((1::'a) + 4 * of_nat m) / 2 ^ Suc k = of_nat m' / 2 ^ k'" |
359 apply (auto simp del: power_Suc) |
351 by (metis (no_types) of_nat_Suc of_nat_mult of_nat_numeral) |
360 apply (metis divide_numeral_1 numeral_One power_0) |
352 moreover have "\<And>k m. \<exists>k' m'. (4 * of_nat m + (3::'a)) / 2 ^ Suc k = of_nat m' / 2 ^ k'" |
361 apply (metis of_nat_Suc of_nat_mult of_nat_numeral) |
|
362 by (metis of_nat_add of_nat_mult of_nat_numeral) |
353 by (metis of_nat_add of_nat_mult of_nat_numeral) |
|
354 ultimately show "?rhs \<subseteq> dyadics" |
|
355 by (auto simp: dyadics_def Nats_def) |
363 qed |
356 qed |
364 |
357 |
365 |
358 |
366 function\<^marker>\<open>tag unimportant\<close> (domintros) dyad_rec :: "[nat \<Rightarrow> 'a, 'a\<Rightarrow>'a, 'a\<Rightarrow>'a, real] \<Rightarrow> 'a" where |
359 function\<^marker>\<open>tag unimportant\<close> (domintros) dyad_rec :: "[nat \<Rightarrow> 'a, 'a\<Rightarrow>'a, 'a\<Rightarrow>'a, real] \<Rightarrow> 'a" where |
367 "dyad_rec b l r (real m) = b m" |
360 "dyad_rec b l r (real m) = b m" |
368 | "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))" |
361 | "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))" |
369 | "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))" |
362 | "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))" |
370 | "x \<notin> dyadics \<Longrightarrow> dyad_rec b l r x = undefined" |
363 | "x \<notin> dyadics \<Longrightarrow> dyad_rec b l r x = undefined" |
371 using iff_4k [of _ 1] iff_4k [of _ 3] |
364 using iff_4k [of _ 1] iff_4k [of _ 3] |
372 apply (simp_all add: nat_neq_4k1 nat_neq_4k3 neq_4k1_k43, atomize_elim) |
365 apply (simp_all add: nat_neq_4k1 nat_neq_4k3 neq_4k1_k43 dyadics_iff Nats_def) |
373 apply (fastforce simp add: dyadics_iff Nats_def field_simps)+ |
366 by (fastforce simp: field_simps)+ |
374 done |
|
375 |
367 |
376 lemma dyadics_levels: "dyadics = (\<Union>K. \<Union>k<K. \<Union> m. {of_nat m / 2^k})" |
368 lemma dyadics_levels: "dyadics = (\<Union>K. \<Union>k<K. \<Union> m. {of_nat m / 2^k})" |
377 unfolding dyadics_def by auto |
369 unfolding dyadics_def by auto |
378 |
370 |
379 lemma dyad_rec_level_termination: |
371 lemma dyad_rec_level_termination: |
450 |
442 |
451 lemma dyad_rec_of_nat [simp]: "dyad_rec b l r (real m) = b m" |
443 lemma dyad_rec_of_nat [simp]: "dyad_rec b l r (real m) = b m" |
452 by (simp add: dyad_rec.psimps dyad_rec_termination) |
444 by (simp add: dyad_rec.psimps dyad_rec_termination) |
453 |
445 |
454 lemma dyad_rec_41 [simp]: "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))" |
446 lemma dyad_rec_41 [simp]: "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))" |
455 apply (rule dyad_rec.psimps) |
447 proof (rule dyad_rec.psimps) |
456 by (metis dyad_rec_level_termination lessI add.commute of_nat_Suc of_nat_mult of_nat_numeral) |
448 show "dyad_rec_dom (b, l, r, (4 * real m + 1) / 2 ^ Suc n)" |
457 |
449 by (metis add.commute dyad_rec_level_termination lessI of_nat_Suc of_nat_mult of_nat_numeral) |
|
450 qed |
458 |
451 |
459 lemma dyad_rec_43 [simp]: "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))" |
452 lemma dyad_rec_43 [simp]: "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))" |
460 apply (rule dyad_rec.psimps) |
453 proof (rule dyad_rec.psimps) |
461 by (metis dyad_rec_level_termination lessI of_nat_add of_nat_mult of_nat_numeral) |
454 show "dyad_rec_dom (b, l, r, (4 * real m + 3) / 2 ^ Suc n)" |
|
455 by (metis dyad_rec_level_termination lessI of_nat_add of_nat_mult of_nat_numeral) |
|
456 qed |
462 |
457 |
463 lemma dyad_rec_41_times2: |
458 lemma dyad_rec_41_times2: |
464 assumes "n > 0" |
459 assumes "n > 0" |
465 shows "dyad_rec b l r (2 * ((4 * real m + 1) / 2^Suc n)) = l (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))" |
460 shows "dyad_rec b l r (2 * ((4 * real m + 1) / 2^Suc n)) = l (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))" |
466 proof - |
461 proof - |
507 |
502 |
508 lemma leftrec_base: "leftrec u v lc rc (real m / 2) = u" |
503 lemma leftrec_base: "leftrec u v lc rc (real m / 2) = u" |
509 by (simp add: dyad_rec2_def) |
504 by (simp add: dyad_rec2_def) |
510 |
505 |
511 lemma leftrec_41: "n > 0 \<Longrightarrow> leftrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = leftrec u v lc rc ((2 * real m + 1) / 2^n)" |
506 lemma leftrec_41: "n > 0 \<Longrightarrow> leftrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = leftrec u v lc rc ((2 * real m + 1) / 2^n)" |
512 apply (simp only: dyad_rec2_def dyad_rec_41_times2) |
507 unfolding dyad_rec2_def dyad_rec_41_times2 |
513 apply (simp add: case_prod_beta) |
508 by (simp add: case_prod_beta) |
514 done |
|
515 |
509 |
516 lemma leftrec_43: "n > 0 \<Longrightarrow> |
510 lemma leftrec_43: "n > 0 \<Longrightarrow> |
517 leftrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = |
511 leftrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = |
518 rc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)) |
512 rc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)) |
519 (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))" |
513 (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))" |
520 apply (simp only: dyad_rec2_def dyad_rec_43_times2) |
514 unfolding dyad_rec2_def dyad_rec_43_times2 |
521 apply (simp add: case_prod_beta) |
515 by (simp add: case_prod_beta) |
522 done |
|
523 |
516 |
524 lemma rightrec_base: "rightrec u v lc rc (real m / 2) = v" |
517 lemma rightrec_base: "rightrec u v lc rc (real m / 2) = v" |
525 by (simp add: dyad_rec2_def) |
518 by (simp add: dyad_rec2_def) |
526 |
519 |
527 lemma rightrec_41: "n > 0 \<Longrightarrow> |
520 lemma rightrec_41: "n > 0 \<Longrightarrow> |
528 rightrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = |
521 rightrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = |
529 lc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)) |
522 lc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)) |
530 (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))" |
523 (midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))" |
531 apply (simp only: dyad_rec2_def dyad_rec_41_times2) |
524 unfolding dyad_rec2_def dyad_rec_41_times2 |
532 apply (simp add: case_prod_beta) |
525 by (simp add: case_prod_beta) |
533 done |
|
534 |
526 |
535 lemma rightrec_43: "n > 0 \<Longrightarrow> rightrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = rightrec u v lc rc ((2 * real m + 1) / 2^n)" |
527 lemma rightrec_43: "n > 0 \<Longrightarrow> rightrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = rightrec u v lc rc ((2 * real m + 1) / 2^n)" |
536 apply (simp only: dyad_rec2_def dyad_rec_43_times2) |
528 unfolding dyad_rec2_def dyad_rec_43_times2 |
537 apply (simp add: case_prod_beta) |
529 by (simp add: case_prod_beta) |
538 done |
|
539 |
530 |
540 lemma dyadics_in_open_unit_interval: |
531 lemma dyadics_in_open_unit_interval: |
541 "{0<..<1} \<inter> (\<Union>k m. {real m / 2^k}) = (\<Union>k. \<Union>m \<in> {0<..<2^k}. {real m / 2^k})" |
532 "{0<..<1} \<inter> (\<Union>k m. {real m / 2^k}) = (\<Union>k. \<Union>m \<in> {0<..<2^k}. {real m / 2^k})" |
542 by (auto simp: field_split_simps) |
533 by (auto simp: field_split_simps) |
543 |
534 |
612 apply atomize |
603 apply atomize |
613 apply (clarsimp simp only: imp_conjL [symmetric] choice_iff choice_iff') |
604 apply (clarsimp simp only: imp_conjL [symmetric] choice_iff choice_iff') |
614 apply (rule that, blast) |
605 apply (rule that, blast) |
615 done |
606 done |
616 then have left_right: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> a \<le> leftcut a b m \<and> rightcut a b m \<le> b" |
607 then have left_right: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> a \<le> leftcut a b m \<and> rightcut a b m \<le> b" |
617 and left_right_m: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> leftcut a b m \<le> m \<and> m \<le> rightcut a b m" |
608 and left_right_m: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> leftcut a b m \<le> m \<and> m \<le> rightcut a b m" |
618 by auto |
609 by auto |
619 have left_neq: "\<lbrakk>a \<le> x; x < leftcut a b m; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m" |
610 have left_neq: "\<lbrakk>a \<le> x; x < leftcut a b m; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m" |
620 and right_neq: "\<lbrakk>rightcut a b m < x; x \<le> b; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m" |
611 and right_neq: "\<lbrakk>rightcut a b m < x; x \<le> b; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m" |
621 and left_right_neq: "\<lbrakk>a \<le> x; x < leftcut a b m; rightcut a b m < y; y \<le> b; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m" |
612 and left_right_neq: "\<lbrakk>a \<le> x; x < leftcut a b m; rightcut a b m < y; y \<le> b; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m" |
622 and feqm: "\<lbrakk>leftcut a b m \<le> x; x \<le> rightcut a b m; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> |
613 and feqm: "\<lbrakk>leftcut a b m \<le> x; x \<le> rightcut a b m; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> |
707 show ?thesis |
698 show ?thesis |
708 proof (cases "even m") |
699 proof (cases "even m") |
709 case True |
700 case True |
710 then obtain r where r: "m = 2*r" by (metis evenE) |
701 then obtain r where r: "m = 2*r" by (metis evenE) |
711 show ?thesis |
702 show ?thesis |
712 using a_le_c [of "m+1"] c_le_b [of "m+1"] a_ge_0 [of "m+1"] b_le_1 [of "m+1"] |
703 using order_trans [OF left_le c_le_v, of "1+2*r"] Suc.IH [of "m+1"] |
713 Suc.IH [of "m+1"] |
704 using a_le_c [of "m+1"] c_le_b [of "m+1"] a_ge_0 [of "m+1"] b_le_1 [of "m+1"] left_right \<open>n > 0\<close> |
714 apply (simp add: r m add.commute [of 1] \<open>n > 0\<close> a41 b41 del: power_Suc) |
705 by (simp_all add: r m add.commute [of 1] a41 b41 del: power_Suc) |
715 apply (auto simp: left_right [THEN conjunct1]) |
|
716 using order_trans [OF left_le c_le_v] |
|
717 by (metis (no_types, hide_lams) add.commute mult_2 of_nat_Suc of_nat_add) |
|
718 next |
706 next |
719 case False |
707 case False |
720 then obtain r where r: "m = 2*r + 1" by (metis oddE) |
708 then obtain r where r: "m = 2*r + 1" by (metis oddE) |
721 show ?thesis |
709 show ?thesis |
722 using a_le_c [of "m"] c_le_b [of "m"] a_ge_0 [of "m"] b_le_1 [of "m"] |
710 using order_trans [OF c_ge_u right_ge, of "1+2*r"] Suc.IH [of "m"] |
723 Suc.IH [of "m+1"] |
711 using a_le_c [of "m"] c_le_b [of "m"] a_ge_0 [of "m"] b_le_1 [of "m"] left_right \<open>n > 0\<close> |
724 apply (simp add: r m add.commute [of 3] \<open>n > 0\<close> a43 b43 del: power_Suc) |
712 apply (simp_all add: r m add.commute [of 3] a43 b43 del: power_Suc) |
725 apply (auto simp: add.commute left_right [THEN conjunct2]) |
713 by (simp add: add.commute) |
726 using order_trans [OF c_ge_u right_ge] |
|
727 apply (metis (no_types, hide_lams) mult_2 numeral_One of_nat_add of_nat_numeral) |
|
728 apply (metis Suc.IH mult_2 of_nat_1 of_nat_add) |
|
729 done |
|
730 qed |
714 qed |
731 qed |
715 qed |
732 qed |
716 qed |
733 qed |
717 qed |
734 have a_ge_0 [simp]: "0 \<le> a(m / 2^n)" and b_le_1 [simp]: "b(m / 2^n) \<le> 1" for m::nat and n |
718 have a_ge_0 [simp]: "0 \<le> a(m / 2^n)" and b_le_1 [simp]: "b(m / 2^n) \<le> 1" for m::nat and n |
784 using False by simp |
767 using False by simp |
785 finally show ?thesis |
768 finally show ?thesis |
786 by (auto simp: ac) |
769 by (auto simp: ac) |
787 next |
770 next |
788 case True show ?thesis |
771 case True show ?thesis |
789 proof (cases "real i / 2^m" "real j / 2^n" rule: linorder_cases) |
772 proof (cases "i / 2^m" "j / 2^n" rule: linorder_cases) |
790 case less |
773 case less |
791 moreover have "real (4 * k + 1) / 2 ^ Suc n + 1 / (2 ^ Suc n) = real j / 2 ^ n" |
774 moreover have "real (4 * k + 1) / 2 ^ Suc n + 1 / (2 ^ Suc n) = real j / 2 ^ n" |
792 using k by (force simp: field_split_simps) |
775 using k by (force simp: field_split_simps) |
793 moreover have "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 2 / (2 ^ Suc n)" |
776 moreover have "\<bar>real i / 2 ^ m - j / 2 ^ n\<bar> < 2 / (2 ^ Suc n)" |
794 using less.prems by simp |
777 using less.prems by simp |
795 ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)" |
778 ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)" |
796 using less.prems by linarith |
779 using less.prems by linarith |
797 have *: "a (real (4 * k + 1) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and> |
780 have "a (real (4 * k + 1) / 2 ^ Suc n) \<le> c (i / 2 ^ m) \<and> |
798 c (real i / 2 ^ m) \<le> b (real (4 * k + 1) / 2 ^ Suc n)" |
781 c (real i / 2 ^ m) \<le> b (real (4 * k + 1) / 2 ^ Suc n)" |
799 apply (rule less.IH [OF _ refl]) |
782 proof (rule less.IH [OF _ refl]) |
800 using closer \<open>n < m\<close> \<open>d = m - n\<close> apply (auto simp: field_split_simps \<open>n < m\<close> diff_less_mono2) |
783 show "m - Suc n < d" |
801 done |
784 using \<open>n < m\<close> diff_less_mono2 less.prems(1) lessI by presburger |
802 show ?thesis |
785 show "\<bar>real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n\<bar> < 1 / 2 ^ Suc n" |
|
786 using closer \<open>n < m\<close> \<open>d = m - n\<close> by (auto simp: field_split_simps \<open>n < m\<close> diff_less_mono2) |
|
787 qed auto |
|
788 then show ?thesis |
803 using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"] |
789 using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"] |
804 using alec [of "2*k+1"] cleb [of "2*k+1"] a_ge_0 [of "2*k+1"] b_le_1 [of "2*k+1"] |
790 using alec [of "2*k+1"] cleb [of "2*k+1"] a_ge_0 [of "2*k+1"] b_le_1 [of "2*k+1"] |
805 using k a41 b41 * \<open>0 < n\<close> |
791 using k a41 b41 \<open>0 < n\<close> |
806 apply (simp add: add.commute) |
792 by (simp add: add.commute) |
807 done |
|
808 next |
793 next |
809 case equal then show ?thesis by simp |
794 case equal then show ?thesis by simp |
810 next |
795 next |
811 case greater |
796 case greater |
812 moreover have "real (4 * k + 3) / 2 ^ Suc n - 1 / (2 ^ Suc n) = real j / 2 ^ n" |
797 moreover have "real (4 * k + 3) / 2 ^ Suc n - 1 / (2 ^ Suc n) = real j / 2 ^ n" |
813 using k by (force simp: field_split_simps) |
798 using k by (force simp: field_split_simps) |
814 moreover have "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 2 * 1 / (2 ^ Suc n)" |
799 moreover have "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 2 * 1 / (2 ^ Suc n)" |
815 using less.prems by simp |
800 using less.prems by simp |
816 ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)" |
801 ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)" |
817 using less.prems by linarith |
802 using less.prems by linarith |
818 have *: "a (real (4 * k + 3) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and> |
803 have "a (real (4 * k + 3) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and> |
819 c (real i / 2 ^ m) \<le> b (real (4 * k + 3) / 2 ^ Suc n)" |
804 c (real i / 2 ^ m) \<le> b (real (4 * k + 3) / 2 ^ Suc n)" |
820 apply (rule less.IH [OF _ refl]) |
805 proof (rule less.IH [OF _ refl]) |
821 using closer \<open>n < m\<close> \<open>d = m - n\<close> apply (auto simp: field_split_simps \<open>n < m\<close> diff_less_mono2) |
806 show "m - Suc n < d" |
822 done |
807 using \<open>n < m\<close> diff_less_mono2 less.prems(1) by blast |
823 show ?thesis |
808 show "\<bar>real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n\<bar> < 1 / 2 ^ Suc n" |
|
809 using closer \<open>n < m\<close> \<open>d = m - n\<close> by (auto simp: field_split_simps \<open>n < m\<close> diff_less_mono2) |
|
810 qed auto |
|
811 then show ?thesis |
824 using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"] |
812 using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"] |
825 using alec [of "2*k+1"] cleb [of "2*k+1"] a_ge_0 [of "2*k+1"] b_le_1 [of "2*k+1"] |
813 using alec [of "2*k+1"] cleb [of "2*k+1"] a_ge_0 [of "2*k+1"] b_le_1 [of "2*k+1"] |
826 using k a43 b43 * \<open>0 < n\<close> |
814 using k a43 b43 \<open>0 < n\<close> |
827 apply (simp add: add.commute) |
815 by (simp add: add.commute) |
828 done |
|
829 qed |
816 qed |
830 qed |
817 qed |
831 qed |
818 qed |
832 qed |
819 qed |
833 then have aj_le_ci: "a (real j / 2 ^ n) \<le> c (real i / 2 ^ m)" |
820 then have aj_le_ci: "a (real j / 2 ^ n) \<le> c (real i / 2 ^ m)" |
910 case True |
897 case True |
911 then obtain k where k: "j = 2*k" by (metis evenE) |
898 then obtain k where k: "j = 2*k" by (metis evenE) |
912 with \<open>0 < j\<close> have "k > 0" "2 * k < 2 ^ n" |
899 with \<open>0 < j\<close> have "k > 0" "2 * k < 2 ^ n" |
913 using Suc.prems(2) k by auto |
900 using Suc.prems(2) k by auto |
914 with k \<open>0 < n\<close> Suc.IH [of k] show ?thesis |
901 with k \<open>0 < n\<close> Suc.IH [of k] show ?thesis |
915 apply (simp add: m1_to_3 a41 b43 del: power_Suc) |
902 by (simp add: m1_to_3 a41 b43 del: power_Suc) (auto simp: of_nat_diff) |
916 apply (subst of_nat_diff, auto) |
|
917 done |
|
918 next |
903 next |
919 case False |
904 case False |
920 then obtain k where k: "j = 2*k + 1" by (metis oddE) |
905 then obtain k where k: "j = 2*k + 1" by (metis oddE) |
921 have "f (leftcut (a ((2 * k + 1) / 2^n)) (b ((2 * k + 1) / 2^n)) (c ((2 * k + 1) / 2^n))) |
906 have "f (leftcut (a ((2 * k + 1) / 2^n)) (b ((2 * k + 1) / 2^n)) (c ((2 * k + 1) / 2^n))) |
922 = f (c ((2 * k + 1) / 2^n))" |
907 = f (c ((2 * k + 1) / 2^n))" |
923 "f (c ((2 * k + 1) / 2^n)) |
908 "f (c ((2 * k + 1) / 2^n)) |
924 = f (rightcut (a ((2 * k + 1) / 2^n)) (b ((2 * k + 1) / 2^n)) (c ((2 * k + 1) / 2^n)))" |
909 = f (rightcut (a ((2 * k + 1) / 2^n)) (b ((2 * k + 1) / 2^n)) (c ((2 * k + 1) / 2^n)))" |
925 using alec [of "2*k+1" n] cleb [of "2*k+1" n] a_ge_0 [of "2*k+1" n] b_le_1 [of "2*k+1" n] k |
910 using alec [of "2*k+1" n] cleb [of "2*k+1" n] a_ge_0 [of "2*k+1" n] b_le_1 [of "2*k+1" n] k |
926 using left_right_m [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"] |
911 using left_right_m [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"] |
927 apply (auto simp: add.commute feqm [OF order_refl] feqm [OF _ order_refl, symmetric]) |
912 by (auto simp: add.commute feqm [OF order_refl] feqm [OF _ order_refl, symmetric]) |
928 done |
|
929 then |
913 then |
930 show ?thesis |
914 show ?thesis |
931 by (simp add: k add.commute [of 1] add.commute [of 3] a43 b41\<open>0 < n\<close> del: power_Suc) |
915 by (simp add: k add.commute [of 1] add.commute [of 3] a43 b41\<open>0 < n\<close> del: power_Suc) |
932 qed |
916 qed |
933 qed |
917 qed |
1107 by auto |
1088 by auto |
1108 finally show ?thesis by simp |
1089 finally show ?thesis by simp |
1109 qed |
1090 qed |
1110 show ?thesis |
1091 show ?thesis |
1111 proof |
1092 proof |
1112 have "real j < 2 ^ n" |
1093 have "2 ^ n * real i / 2 ^ m < 2 ^ n" "2 ^ n * real k / 2 ^ p < 2 ^ n" |
1113 using j_le i k |
1094 using i k by (auto simp: field_simps) |
1114 apply (auto simp: le_max_iff_disj simp del: of_nat_less_numeral_power_cancel_iff |
1095 then have "max (2^n * i / 2^m) (2^n * k / 2^p) < 2^n" |
1115 elim!: le_less_trans) |
1096 by simp |
1116 apply (auto simp: field_simps) |
1097 with j_le have "real j < 2 ^ n" by linarith |
1117 done |
|
1118 then show "j < 2 ^ n" |
1098 then show "j < 2 ^ n" |
1119 by auto |
1099 by auto |
1120 show "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2 ^ n" |
1100 have "\<bar>real i * 2 ^ n - real j * 2 ^ m\<bar> < 2 ^ m" |
1121 using clo less_j1 j_le |
1101 using clo less_j1 j_le |
1122 apply (auto simp: le_max_iff_disj field_split_simps dist_norm) |
1102 by (auto simp: le_max_iff_disj field_split_simps dist_norm abs_if split: if_split_asm dest: 1 2) |
1123 apply (auto simp: algebra_simps abs_if split: if_split_asm dest: 1 2) |
1103 then show "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2 ^ n" |
1124 done |
1104 by (auto simp: field_split_simps) |
1125 show "\<bar>real k / 2 ^ p - real j / 2 ^ n\<bar> < 1/2 ^ n" |
1105 have "\<bar>real k * 2 ^ n - real j * 2 ^ p\<bar> < 2 ^ p" |
1126 using clo less_j1 j_le |
1106 using clo less_j1 j_le |
1127 apply (auto simp: le_max_iff_disj field_split_simps dist_norm) |
1107 by (auto simp: le_max_iff_disj field_split_simps dist_norm abs_if split: if_split_asm dest: 3 2) |
1128 apply (auto simp: algebra_simps not_less abs_if split: if_split_asm dest: 3 2) |
1108 then show "\<bar>real k / 2 ^ p - real j / 2 ^ n\<bar> < 1/2 ^ n" |
1129 done |
1109 by (auto simp: le_max_iff_disj field_split_simps dist_norm) |
1130 qed (use False in simp) |
1110 qed (use False in simp) |
1131 qed |
1111 qed |
1132 qed |
1112 qed |
1133 show "dist (f (c (real k / 2 ^ p))) (f (c (real i / 2 ^ m))) < e" |
1113 show "dist (f (c (real k / 2 ^ p))) (f (c (real i / 2 ^ m))) < e" |
1134 proof (rule dist_triangle_half_l) |
1114 proof (rule dist_triangle_half_l) |
1135 show "dist (f (c (real k / 2 ^ p))) (f(c(j / 2^n))) < e/2" |
1115 show "dist (f (c (real k / 2 ^ p))) (f(c(j / 2^n))) < e/2" |
1136 apply (rule dist_fc_close) |
1116 using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> k clo_kj |
1137 using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> k clo_kj by auto |
1117 by (intro dist_fc_close) auto |
1138 show "dist (f (c (real i / 2 ^ m))) (f (c (real j / 2 ^ n))) < e/2" |
1118 show "dist (f (c (real i / 2 ^ m))) (f (c (real j / 2 ^ n))) < e/2" |
1139 apply (rule dist_fc_close) |
1119 using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> i clo_ij |
1140 using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> i clo_ij by auto |
1120 by (intro dist_fc_close) auto |
1141 qed |
1121 qed |
1142 qed |
1122 qed |
1143 qed |
1123 qed |
1144 qed |
1124 qed |
1145 then obtain h where ucont_h: "uniformly_continuous_on {0..1} h" |
1125 then obtain h where ucont_h: "uniformly_continuous_on {0..1} h" |
1189 using \<open>0 \<le> x\<close> \<open>x \<le> 1\<close> by force |
1169 using \<open>0 \<le> x\<close> \<open>x \<le> 1\<close> by force |
1190 then have "\<exists>y\<ge>a (real 1/2). y \<le> b (real 1/2) \<and> f y = f x" |
1170 then have "\<exists>y\<ge>a (real 1/2). y \<le> b (real 1/2) \<and> f y = f x" |
1191 proof cases |
1171 proof cases |
1192 case 1 |
1172 case 1 |
1193 then show ?thesis |
1173 then show ?thesis |
1194 apply (rule_tac x=u in exI) |
1174 using uabv [of 1 1] f0u [of u] f0u [of x] by force |
1195 using uabv [of 1 1] f0u [of u] f0u [of x] by auto |
|
1196 next |
1175 next |
1197 case 2 |
1176 case 2 |
1198 then show ?thesis |
1177 then show ?thesis |
1199 by (rule_tac x=x in exI) auto |
1178 by (rule_tac x=x in exI) auto |
1200 next |
1179 next |
1201 case 3 |
1180 case 3 |
1202 then show ?thesis |
1181 then show ?thesis |
1203 apply (rule_tac x=v in exI) |
1182 using uabv [of 1 1] fv1 [of v] fv1 [of x] by force |
1204 using uabv [of 1 1] fv1 [of v] fv1 [of x] by auto |
|
1205 qed |
1183 qed |
1206 with \<open>n=0\<close> show ?thesis |
1184 with \<open>n=0\<close> show ?thesis |
1207 by (rule_tac x=1 in exI) auto |
1185 by (rule_tac x=1 in exI) auto |
1208 next |
1186 next |
1209 case False |
1187 case False |
1210 with Suc obtain m y |
1188 with Suc obtain m y |
1211 where "odd m" "0 < m" and mless: "m < 2 ^ n" |
1189 where "odd m" "0 < m" and mless: "m < 2 ^ n" |
1212 and y: "y \<in> {a (real m / 2 ^ n)..b (real m / 2 ^ n)}" and feq: "f y = f x" |
1190 and y: "y \<in> {a (real m / 2 ^ n)..b (real m / 2 ^ n)}" and feq: "f y = f x" |
1213 by metis |
1191 by metis |
1214 then obtain j where j: "m = 2*j + 1" by (metis oddE) |
1192 then obtain j where j: "m = 2*j + 1" by (metis oddE) |
|
1193 have j4: "4 * j + 1 < 2 ^ Suc n" |
|
1194 using mless j by (simp add: algebra_simps) |
|
1195 |
1215 consider "y \<in> {a((2*j + 1) / 2^n) .. b((4*j + 1) / 2 ^ (Suc n))}" |
1196 consider "y \<in> {a((2*j + 1) / 2^n) .. b((4*j + 1) / 2 ^ (Suc n))}" |
1216 | "y \<in> {b((4*j + 1) / 2 ^ (Suc n)) .. a((4*j + 3) / 2 ^ (Suc n))}" |
1197 | "y \<in> {b((4*j + 1) / 2 ^ (Suc n)) .. a((4*j + 3) / 2 ^ (Suc n))}" |
1217 | "y \<in> {a((4*j + 3) / 2 ^ (Suc n)) .. b((2*j + 1) / 2^n)}" |
1198 | "y \<in> {a((4*j + 3) / 2 ^ (Suc n)) .. b((2*j + 1) / 2^n)}" |
1218 using y j by force |
1199 using y j by force |
1219 then show ?thesis |
1200 then show ?thesis |
1220 proof cases |
1201 proof cases |
1221 case 1 |
1202 case 1 |
1222 then show ?thesis |
1203 show ?thesis |
1223 apply (rule_tac x="4*j + 1" in exI) |
1204 proof (intro exI conjI) |
1224 apply (rule_tac x=y in exI) |
1205 show "y \<in> {a (real (4 * j + 1) / 2 ^ Suc n)..b (real (4 * j + 1) / 2 ^ Suc n)}" |
1225 using mless j \<open>n \<noteq> 0\<close> |
1206 using mless j \<open>n \<noteq> 0\<close> 1 by (simp add: a41 b41 add.commute [of 1] del: power_Suc) |
1226 apply (simp add: feq a41 b41 add.commute [of 1] del: power_Suc) |
1207 qed (use feq j4 in auto) |
1227 apply (simp add: algebra_simps) |
|
1228 done |
|
1229 next |
1208 next |
1230 case 2 |
1209 case 2 |
1231 show ?thesis |
1210 show ?thesis |
1232 apply (rule_tac x="4*j + 1" in exI) |
1211 proof (intro exI conjI) |
1233 apply (rule_tac x="b((4*j + 1) / 2 ^ (Suc n))" in exI) |
1212 show "b (real (4 * j + 1) / 2 ^ Suc n) \<in> {a (real (4 * j + 1) / 2 ^ Suc n)..b (real (4 * j + 1) / 2 ^ Suc n)}" |
1234 using mless \<open>n \<noteq> 0\<close> 2 j |
1213 using \<open>n \<noteq> 0\<close> alec [of "2*j+1" n] cleb [of "2*j+1" n] a_ge_0 [of "2*j+1" n] b_le_1 [of "2*j+1" n] |
1235 using alec [of "2*j+1" n] cleb [of "2*j+1" n] a_ge_0 [of "2*j+1" n] b_le_1 [of "2*j+1" n] |
1214 using left_right [of "c((2*j + 1) / 2^n)" "a((2*j + 1) / 2^n)" "b((2*j + 1) / 2^n)"] |
1236 using left_right [of "c((2*j + 1) / 2^n)" "a((2*j + 1) / 2^n)" "b((2*j + 1) / 2^n)"] |
1215 by (simp add: a41 b41 add.commute [of 1] del: power_Suc) |
1237 apply (simp add: a41 b41 a43 b43 add.commute [of 1] add.commute [of 3] del: power_Suc) |
1216 show "f (b (real (4 * j + 1) / 2 ^ Suc n)) = f x" |
1238 apply (auto simp: feq [symmetric] intro: f_eqI) |
1217 using \<open>n \<noteq> 0\<close> 2 |
1239 done |
1218 using alec [of "2*j+1" n] cleb [of "2*j+1" n] a_ge_0 [of "2*j+1" n] b_le_1 [of "2*j+1" n] |
|
1219 by (force simp add: b41 a43 add.commute [of 1] feq [symmetric] simp del: power_Suc intro: f_eqI) |
|
1220 qed (use j4 in auto) |
1240 next |
1221 next |
1241 case 3 |
1222 case 3 |
1242 then show ?thesis |
1223 show ?thesis |
1243 apply (rule_tac x="4*j + 3" in exI) |
1224 proof (intro exI conjI) |
1244 apply (rule_tac x=y in exI) |
1225 show "4 * j + 3 < 2 ^ Suc n" |
1245 using mless j \<open>n \<noteq> 0\<close> |
1226 using mless j by simp |
1246 apply (simp add: feq a43 b43 del: power_Suc) |
1227 show "f y = f x" |
1247 apply (simp add: algebra_simps) |
1228 by fact |
1248 done |
1229 show "y \<in> {a (real (4 * j + 3) / 2 ^ Suc n) .. b (real (4 * j + 3) / 2 ^ Suc n)}" |
|
1230 using 3 False b43 [of n j] by (simp add: add.commute) |
|
1231 qed (use 3 in auto) |
1249 qed |
1232 qed |
1250 qed |
1233 qed |
1251 qed |
1234 qed |
1252 obtain n where n: "1/2^n < min (\<delta> / 2) 1" |
1235 obtain n where n: "1/2^n < min (\<delta> / 2) 1" |
1253 by (metis \<open>0 < \<delta>\<close> divide_less_eq_1 less_numeral_extra(1) min_less_iff_conj one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_divide_iff zero_less_numeral) |
1236 by (metis \<open>0 < \<delta>\<close> divide_less_eq_1 less_numeral_extra(1) min_less_iff_conj one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_divide_iff zero_less_numeral) |
1254 with gr0I have "n \<noteq> 0" |
1237 with gr0I have "n \<noteq> 0" |
1255 by fastforce |
1238 by fastforce |
1256 with * obtain m::nat and y |
1239 with * obtain m::nat and y |
1257 where "odd m" "0 < m" and mless: "m < 2 ^ n" |
1240 where "odd m" "0 < m" and mless: "m < 2 ^ n" |
1258 and y: "y \<in> {a(m / 2^n) .. b(m / 2^n)}" and feq: "f x = f y" |
1241 and y: "a(m / 2^n) \<le> y \<and> y \<le> b(m / 2^n)" and feq: "f x = f y" |
1259 by metis |
1242 by (metis atLeastAtMost_iff) |
1260 then have "0 \<le> y" "y \<le> 1" |
1243 then have "0 \<le> y" "y \<le> 1" |
1261 by (metis atLeastAtMost_iff a_ge_0 b_le_1 order.trans)+ |
1244 by (meson a_ge_0 b_le_1 order.trans)+ |
1262 moreover have "y < \<delta> + c (real m / 2 ^ n)" "c (real m / 2 ^ n) < \<delta> + y" |
1245 moreover have "y < \<delta> + c (real m / 2 ^ n)" "c (real m / 2 ^ n) < \<delta> + y" |
1263 using y apply simp_all |
1246 using y alec [of m n] cleb [of m n] n field_sum_of_halves close_ab [OF \<open>odd m\<close>, of n] |
1264 using alec [of m n] cleb [of m n] n field_sum_of_halves close_ab [OF \<open>odd m\<close>, of n] |
|
1265 by linarith+ |
1247 by linarith+ |
1266 moreover note \<open>0 < m\<close> mless \<open>0 \<le> x\<close> \<open>x \<le> 1\<close> |
1248 moreover note \<open>0 < m\<close> mless \<open>0 \<le> x\<close> \<open>x \<le> 1\<close> |
1267 ultimately show "\<exists>k. \<exists>m\<in>{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e" |
1249 ultimately have "dist (h (real m / 2 ^ n)) (f x) < e" |
1268 apply (rule_tac x=n in exI) |
1250 by (auto simp: dist_norm h_eq feq \<delta>) |
1269 apply (rule_tac x=m in bexI) |
1251 then show "\<exists>k. \<exists>m\<in>{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e" |
1270 apply (auto simp: dist_norm h_eq feq \<delta>) |
1252 using \<open>0 < m\<close> greaterThanLessThan_iff mless by blast |
1271 done |
|
1272 qed |
1253 qed |
1273 also have "... \<subseteq> h ` {0..1}" |
1254 also have "... \<subseteq> h ` {0..1}" |
1274 apply (rule closure_minimal) |
1255 proof (rule closure_minimal) |
1275 using compact_continuous_image [OF cont_h] compact_imp_closed by (auto simp: D01_def) |
1256 show "h ` D01 \<subseteq> h ` {0..1}" |
|
1257 using cloD01 closure_subset by blast |
|
1258 show "closed (h ` {0..1})" |
|
1259 using compact_continuous_image [OF cont_h] compact_imp_closed by auto |
|
1260 qed |
1276 finally show "f ` {0..1} \<subseteq> h ` {0..1}" . |
1261 finally show "f ` {0..1} \<subseteq> h ` {0..1}" . |
1277 qed |
1262 qed |
1278 moreover have "inj_on h {0..1}" |
1263 moreover have "inj_on h {0..1}" |
1279 proof - |
1264 proof - |
1280 have "u < v" |
1265 have "u < v" |
1474 have "c (real i / 2 ^ m) \<le> c((2*q + 1) / 2^n')" |
1468 have "c (real i / 2 ^ m) \<le> c((2*q + 1) / 2^n')" |
1475 proof (cases "i / 2^m = (2*q + 1) / 2^n'") |
1469 proof (cases "i / 2^m = (2*q + 1) / 2^n'") |
1476 case True then show ?thesis by simp |
1470 case True then show ?thesis by simp |
1477 next |
1471 next |
1478 case False |
1472 case False |
1479 with i_le_j q have less: "i / 2^m < (2*q + 1) / 2^n'" |
1473 with i_le_j clo_ij q have "\<bar>real i / 2 ^ m - real (4 * q + 1) / 2 ^ Suc n'\<bar> < 1 / 2 ^ Suc n'" |
1480 by auto |
1474 by (auto simp: field_split_simps) |
1481 have *: "\<lbrakk>i < q; abs(i - q) < s*2; q = r + s\<rbrakk> \<Longrightarrow> abs(i - r) < s" for i q s r::real |
1475 then have "c(i / 2^m) \<le> b(real(4 * q + 1) / 2 ^ (Suc n'))" |
1482 by auto |
1476 by (meson ci_le_bj even_mult_iff even_numeral even_plus_one_iff) |
1483 have "c(i / 2^m) \<le> b(real(4 * q + 1) / 2 ^ (Suc n'))" |
|
1484 apply (rule ci_le_bj, force) |
|
1485 apply (rule * [OF less]) |
|
1486 using i_le_j clo_ij q apply (auto simp: field_split_simps) |
|
1487 done |
|
1488 then show ?thesis |
1477 then show ?thesis |
1489 using alec [of "2*q+1" n'] cleb [of "2*q+1" n'] a_ge_0 [of "2*q+1" n'] b_le_1 [of "2*q+1" n'] b41 [of n' q] \<open>n' \<noteq> 0\<close> |
1478 using alec [of "2*q+1" n'] cleb [of "2*q+1" n'] a_ge_0 [of "2*q+1" n'] b_le_1 [of "2*q+1" n'] b41 [of n' q] \<open>n' \<noteq> 0\<close> |
1490 using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"] |
1479 using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"] |
1491 by (auto simp: algebra_simps) |
1480 by (auto simp: algebra_simps) |
1492 qed |
1481 qed |
1609 qed |
1597 qed |
1610 have m_div: "0 < m / 2^n" "m / 2^n < 1" |
1598 have m_div: "0 < m / 2^n" "m / 2^n < 1" |
1611 using m by (auto simp: field_split_simps) |
1599 using m by (auto simp: field_split_simps) |
1612 have closure0m: "{0..m / 2^n} = closure ({0<..< m / 2^n} \<inter> (\<Union>k m. {real m / 2 ^ k}))" |
1600 have closure0m: "{0..m / 2^n} = closure ({0<..< m / 2^n} \<inter> (\<Union>k m. {real m / 2 ^ k}))" |
1613 by (subst closure_dyadic_rationals_in_convex_set_pos_1, simp_all add: not_le m) |
1601 by (subst closure_dyadic_rationals_in_convex_set_pos_1, simp_all add: not_le m) |
1614 have closurem1: "{m / 2^n .. 1} = closure ({m / 2^n <..< 1} \<inter> (\<Union>k m. {real m / 2 ^ k}))" |
1602 have "2^n > m" |
1615 apply (subst closure_dyadic_rationals_in_convex_set_pos_1; simp add: not_le m) |
1603 by (simp add: m(2) not_le) |
1616 using \<open>0 < real m / 2 ^ n\<close> by linarith |
1604 then have closurem1: "{m / 2^n .. 1} = closure ({m / 2^n <..< 1} \<inter> (\<Union>k m. {real m / 2 ^ k}))" |
|
1605 using closure_dyadic_rationals_in_convex_set_pos_1 m_div(1) by fastforce |
1617 have cont_h': "continuous_on (closure ({u<..<v} \<inter> (\<Union>k m. {real m / 2 ^ k}))) h" |
1606 have cont_h': "continuous_on (closure ({u<..<v} \<inter> (\<Union>k m. {real m / 2 ^ k}))) h" |
1618 if "0 \<le> u" "v \<le> 1" for u v |
1607 if "0 \<le> u" "v \<le> 1" for u v |
1619 apply (rule continuous_on_subset [OF cont_h]) |
1608 using that by (intro continuous_on_subset [OF cont_h] closure_minimal [OF subsetI]) auto |
1620 apply (rule closure_minimal [OF subsetI]) |
|
1621 using that apply auto |
|
1622 done |
|
1623 have closed_f': "closed (f ` {u..v})" if "0 \<le> u" "v \<le> 1" for u v |
1609 have closed_f': "closed (f ` {u..v})" if "0 \<le> u" "v \<le> 1" for u v |
1624 by (metis compact_continuous_image cont_f compact_interval atLeastatMost_subset_iff |
1610 by (metis compact_continuous_image cont_f compact_interval atLeastatMost_subset_iff |
1625 compact_imp_closed continuous_on_subset that) |
1611 compact_imp_closed continuous_on_subset that) |
1626 have less_2I: "\<And>k i. real i / 2 ^ k < 1 \<Longrightarrow> i < 2 ^ k" |
1612 have less_2I: "\<And>k i. real i / 2 ^ k < 1 \<Longrightarrow> i < 2 ^ k" |
1627 by simp |
1613 by simp |
1628 have "h ` ({0<..<m / 2 ^ n} \<inter> (\<Union>q p. {real p / 2 ^ q})) \<subseteq> f ` {0..c (m / 2 ^ n)}" |
1614 have "h ` ({0<..<m / 2 ^ n} \<inter> (\<Union>q p. {real p / 2 ^ q})) \<subseteq> f ` {0..c (m / 2 ^ n)}" |
1629 proof clarsimp |
1615 proof clarsimp |
1630 fix p q |
1616 fix p q |
1631 assume p: "0 < real p / 2 ^ q" "real p / 2 ^ q < real m / 2 ^ n" |
1617 assume p: "0 < real p / 2 ^ q" "real p / 2 ^ q < real m / 2 ^ n" |
1632 then have [simp]: "0 < p" "p < 2 ^ q" |
1618 then have [simp]: "0 < p" |
1633 apply (simp add: field_split_simps) |
1619 by (simp add: field_split_simps) |
1634 apply (blast intro: p less_2I m_div less_trans) |
1620 have [simp]: "p < 2 ^ q" |
1635 done |
1621 by (blast intro: p less_2I m_div less_trans) |
1636 have "f (c (real p / 2 ^ q)) \<in> f ` {0..c (real m / 2 ^ n)}" |
1622 have "f (c (real p / 2 ^ q)) \<in> f ` {0..c (real m / 2 ^ n)}" |
1637 by (auto simp: clec p m) |
1623 by (auto simp: clec p m) |
1638 then show "h (real p / 2 ^ q) \<in> f ` {0..c (real m / 2 ^ n)}" |
1624 then show "h (real p / 2 ^ q) \<in> f ` {0..c (real m / 2 ^ n)}" |
1639 by (simp add: h_eq) |
1625 by (simp add: h_eq) |
1640 qed |
1626 qed |
1641 then have "h ` {0 .. m / 2^n} \<subseteq> f ` {0 .. c(m / 2^n)}" |
1627 with m_div have "h ` {0 .. m / 2^n} \<subseteq> f ` {0 .. c(m / 2^n)}" |
1642 apply (subst closure0m) |
1628 apply (subst closure0m) |
1643 apply (rule image_closure_subset [OF cont_h' closed_f']) |
1629 by (rule image_closure_subset [OF cont_h' closed_f']) auto |
1644 using m_div apply auto |
|
1645 done |
|
1646 then have hx1: "h x1 \<in> f ` {0 .. c(m / 2^n)}" |
1630 then have hx1: "h x1 \<in> f ` {0 .. c(m / 2^n)}" |
1647 using x12 less.prems(1) by auto |
1631 using x12 less.prems(1) by auto |
1648 then obtain t1 where t1: "h x1 = f t1" "0 \<le> t1" "t1 \<le> c (m / 2 ^ n)" |
1632 then obtain t1 where t1: "h x1 = f t1" "0 \<le> t1" "t1 \<le> c (m / 2 ^ n)" |
1649 by auto |
1633 by auto |
1650 have "h ` ({m / 2 ^ n<..<1} \<inter> (\<Union>q p. {real p / 2 ^ q})) \<subseteq> f ` {c (m / 2 ^ n)..1}" |
1634 have "h ` ({m / 2 ^ n<..<1} \<inter> (\<Union>q p. {real p / 2 ^ q})) \<subseteq> f ` {c (m / 2 ^ n)..1}" |
1716 then obtain e where "e > 0" |
1698 then obtain e where "e > 0" |
1717 and e: "\<And>u v. \<lbrakk>u \<in> {0..1}; v \<in> {0..1}; dist v u < e\<rbrakk> \<Longrightarrow> dist (p v) (p u) < norm(p x - p y) / 2" |
1699 and e: "\<And>u v. \<lbrakk>u \<in> {0..1}; v \<in> {0..1}; dist v u < e\<rbrakk> \<Longrightarrow> dist (p v) (p u) < norm(p x - p y) / 2" |
1718 by (metis uniformly_continuous_onE [OF ucont_p]) |
1700 by (metis uniformly_continuous_onE [OF ucont_p]) |
1719 have minxy: "min e (y - x) < (y - x) * (3 / 2)" |
1701 have minxy: "min e (y - x) < (y - x) * (3 / 2)" |
1720 by (subst min_less_iff_disj) (simp add: less) |
1702 by (subst min_less_iff_disj) (simp add: less) |
1721 obtain w z where "w < z" and w: "w \<in> {x<..<y}" and z: "z \<in> {x<..<y}" |
1703 define w where "w \<equiv> x + (min e (y - x) / 3)" |
|
1704 define z where "z \<equiv>y - (min e (y - x) / 3)" |
|
1705 have "w < z" and w: "w \<in> {x<..<y}" and z: "z \<in> {x<..<y}" |
1722 and wxe: "norm(w - x) < e" and zye: "norm(z - y) < e" |
1706 and wxe: "norm(w - x) < e" and zye: "norm(z - y) < e" |
1723 apply (rule_tac w = "x + (min e (y - x) / 3)" and z = "y - (min e (y - x) / 3)" in that) |
1707 using minxy \<open>0 < e\<close> less unfolding w_def z_def by auto |
1724 using minxy \<open>0 < e\<close> less by simp_all |
|
1725 have Fclo: "\<And>T. T \<in> range F \<Longrightarrow> closed T" |
1708 have Fclo: "\<And>T. T \<in> range F \<Longrightarrow> closed T" |
1726 by (metis \<open>\<And>n. closed (F n)\<close> image_iff) |
1709 by (metis \<open>\<And>n. closed (F n)\<close> image_iff) |
1727 have eq: "{w..z} \<inter> \<Inter>(F ` UNIV) = {}" |
1710 have eq: "{w..z} \<inter> \<Inter>(F ` UNIV) = {}" |
1728 using less w z apply (auto simp: open_segment_eq_real_ivl) |
1711 using less w z by (simp add: open_segment_eq_real_ivl disjoint_iff) |
1729 by (metis (no_types, hide_lams) INT_I IntI empty_iff greaterThanLessThan_iff not_le order.trans) |
|
1730 then obtain K where "finite K" and K: "{w..z} \<inter> (\<Inter> (F ` K)) = {}" |
1712 then obtain K where "finite K" and K: "{w..z} \<inter> (\<Inter> (F ` K)) = {}" |
1731 by (metis finite_subset_image compact_imp_fip [OF compact_interval Fclo]) |
1713 by (metis finite_subset_image compact_imp_fip [OF compact_interval Fclo]) |
1732 then have "K \<noteq> {}" |
1714 then have "K \<noteq> {}" |
1733 using \<open>w < z\<close> \<open>{w..z} \<inter> \<Inter>(F ` K) = {}\<close> by auto |
1715 using \<open>w < z\<close> \<open>{w..z} \<inter> \<Inter>(F ` K) = {}\<close> by auto |
1734 define n where "n \<equiv> Max K" |
1716 define n where "n \<equiv> Max K" |
1875 next |
1855 next |
1876 case False |
1856 case False |
1877 have uvT: "closed (closed_segment u v \<inter> T)" "closed_segment u v \<inter> T \<noteq> {}" |
1857 have uvT: "closed (closed_segment u v \<inter> T)" "closed_segment u v \<inter> T \<noteq> {}" |
1878 using False open_closed_segment by (auto simp: \<open>closed T\<close> closed_Int) |
1858 using False open_closed_segment by (auto simp: \<open>closed T\<close> closed_Int) |
1879 obtain w where "w \<in> T" and w: "w \<in> closed_segment u v" "open_segment u w \<inter> T = {}" |
1859 obtain w where "w \<in> T" and w: "w \<in> closed_segment u v" "open_segment u w \<inter> T = {}" |
1880 apply (rule segment_to_point_exists [OF uvT, of u]) |
1860 proof (rule segment_to_point_exists [OF uvT]) |
1881 by (metis IntD1 Int_commute Int_left_commute ends_in_segment(1) inf.orderE subset_oc_segment) |
1861 fix b |
|
1862 assume "b \<in> closed_segment u v \<inter> T" "open_segment u b \<inter> (closed_segment u v \<inter> T) = {}" |
|
1863 then show thesis |
|
1864 by (metis IntD1 IntD2 ends_in_segment(1) inf.orderE inf_assoc subset_oc_segment that) |
|
1865 qed |
1882 then have puw: "dist (p u) (p w) < \<epsilon> / 2" |
1866 then have puw: "dist (p u) (p w) < \<epsilon> / 2" |
1883 by (metis (no_types) \<open>T \<subseteq> {0..1}\<close> \<open>dist v u < \<delta>\<close> \<delta> dist_commute dist_in_closed_segment le_less_trans subsetCE) |
1867 by (metis (no_types) \<open>T \<subseteq> {0..1}\<close> \<open>dist v u < \<delta>\<close> \<delta> dist_commute dist_in_closed_segment le_less_trans subsetCE) |
1884 obtain z where "z \<in> T" and z: "z \<in> closed_segment u v" "open_segment v z \<inter> T = {}" |
1868 obtain z where "z \<in> T" and z: "z \<in> closed_segment u v" "open_segment v z \<inter> T = {}" |
1885 apply (rule segment_to_point_exists [OF uvT, of v]) |
1869 proof (rule segment_to_point_exists [OF uvT]) |
1886 by (metis IntD2 Int_commute Int_left_commute ends_in_segment(2) inf.orderE subset_oc_segment) |
1870 fix b |
|
1871 assume "b \<in> closed_segment u v \<inter> T" "open_segment v b \<inter> (closed_segment u v \<inter> T) = {}" |
|
1872 then show thesis |
|
1873 by (metis IntD1 IntD2 ends_in_segment(2) inf.orderE inf_assoc subset_oc_segment that) |
|
1874 qed |
1887 then have "dist (p u) (p z) < \<epsilon> / 2" |
1875 then have "dist (p u) (p z) < \<epsilon> / 2" |
1888 by (metis \<open>T \<subseteq> {0..1}\<close> \<open>dist v u < \<delta>\<close> \<delta> dist_commute dist_in_closed_segment le_less_trans subsetCE) |
1876 by (metis \<open>T \<subseteq> {0..1}\<close> \<open>dist v u < \<delta>\<close> \<delta> dist_commute dist_in_closed_segment le_less_trans subsetCE) |
1889 then show ?thesis |
1877 then show ?thesis |
1890 using puw by (metis (no_types) \<open>w \<in> T\<close> \<open>z \<in> T\<close> dist_commute dist_triangle_half_l h_eq_p_gen w(2) z(2)) |
1878 using puw by (metis (no_types) \<open>w \<in> T\<close> \<open>z \<in> T\<close> dist_commute dist_triangle_half_l h_eq_p_gen w(2) z(2)) |
1891 qed |
1879 qed |
2046 have "path_connected(ball z r)" |
2034 have "path_connected(ball z r)" |
2047 by (simp add: convex_imp_path_connected) |
2035 by (simp add: convex_imp_path_connected) |
2048 with y \<open>r > 0\<close> obtain g where "arc g" and pig: "path_image g \<subseteq> ball z r" |
2036 with y \<open>r > 0\<close> obtain g where "arc g" and pig: "path_image g \<subseteq> ball z r" |
2049 and g: "pathstart g = y" "pathfinish g = z" |
2037 and g: "pathstart g = y" "pathfinish g = z" |
2050 using \<open>y \<noteq> z\<close> by (force simp: path_connected_arcwise) |
2038 using \<open>y \<noteq> z\<close> by (force simp: path_connected_arcwise) |
2051 have "compact (g -` frontier S \<inter> {0..1})" |
2039 have "continuous_on {0..1} g" |
2052 apply (simp add: compact_eq_bounded_closed bounded_Int) |
2040 using \<open>arc g\<close> arc_imp_path path_def by blast |
2053 apply (rule closed_vimage_Int) |
2041 then have "compact (g -` frontier S \<inter> {0..1})" |
2054 using \<open>arc g\<close> apply (auto simp: arc_def path_def) |
2042 by (simp add: bounded_Int closed_Diff closed_vimage_Int compact_eq_bounded_closed) |
2055 done |
|
2056 moreover have "g -` frontier S \<inter> {0..1} \<noteq> {}" |
2043 moreover have "g -` frontier S \<inter> {0..1} \<noteq> {}" |
2057 proof - |
2044 proof - |
2058 have "\<exists>r. r \<in> g -` frontier S \<and> r \<in> {0..1}" |
2045 have "\<exists>r. r \<in> g -` frontier S \<and> r \<in> {0..1}" |
2059 by (metis \<open>z \<in> frontier S\<close> g(2) imageE path_image_def pathfinish_in_path_image vimageI2) |
2046 by (metis \<open>z \<in> frontier S\<close> g(2) imageE path_image_def pathfinish_in_path_image vimageI2) |
2060 then show ?thesis |
2047 then show ?thesis |
2080 have "g t \<in> V" |
2067 have "g t \<in> V" |
2081 by (metis IntI atLeastAtMost_iff gt image_eqI path_image_def pig r subsetCE \<open>0 \<le> t\<close> \<open>t \<le> 1\<close>) |
2068 by (metis IntI atLeastAtMost_iff gt image_eqI path_image_def pig r subsetCE \<open>0 \<le> t\<close> \<open>t \<le> 1\<close>) |
2082 then show "pathfinish (subpath 0 t g) \<in> V" |
2069 then show "pathfinish (subpath 0 t g) \<in> V" |
2083 by auto |
2070 by auto |
2084 then have "inj_on (subpath 0 t g) {0..1}" |
2071 then have "inj_on (subpath 0 t g) {0..1}" |
2085 using t01 |
2072 using t01 \<open>arc (subpath 0 t g)\<close> arc_imp_inj_on by blast |
2086 apply (clarsimp simp: inj_on_def subpath_def) |
|
2087 apply (drule inj_onD [OF arc_imp_inj_on [OF \<open>arc g\<close>]]) |
|
2088 using mult_le_one apply auto |
|
2089 done |
|
2090 then have "subpath 0 t g ` {0..<1} \<subseteq> subpath 0 t g ` {0..1} - {subpath 0 t g 1}" |
2073 then have "subpath 0 t g ` {0..<1} \<subseteq> subpath 0 t g ` {0..1} - {subpath 0 t g 1}" |
2091 by (force simp: dest: inj_onD) |
2074 by (force simp: dest: inj_onD) |
2092 moreover have False if "subpath 0 t g ` ({0..<1}) - S \<noteq> {}" |
2075 moreover have False if "subpath 0 t g ` ({0..<1}) - S \<noteq> {}" |
2093 proof - |
2076 proof - |
2094 have contg: "continuous_on {0..1} g" |
2077 have contg: "continuous_on {0..1} g" |
2095 using \<open>arc g\<close> by (auto simp: arc_def path_def) |
2078 using \<open>arc g\<close> by (auto simp: arc_def path_def) |
2096 have "subpath 0 t g ` {0..<1} \<inter> frontier S \<noteq> {}" |
2079 have "subpath 0 t g ` {0..<1} \<inter> frontier S \<noteq> {}" |
2097 proof (rule connected_Int_frontier [OF _ _ that]) |
2080 proof (rule connected_Int_frontier [OF _ _ that]) |
2098 show "connected (subpath 0 t g ` {0..<1})" |
2081 show "connected (subpath 0 t g ` {0..<1})" |
2099 apply (rule connected_continuous_image) |
2082 proof (rule connected_continuous_image) |
2100 apply (simp add: subpath_def) |
2083 show "continuous_on {0..<1} (subpath 0 t g)" |
2101 apply (intro continuous_intros continuous_on_compose2 [OF contg]) |
2084 by (meson \<open>arc (subpath 0 t g)\<close> arc_def atLeastLessThan_subseteq_atLeastAtMost_iff continuous_on_subset order_refl path_def) |
2102 apply (auto simp: \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> mult_le_one) |
2085 qed auto |
2103 done |
|
2104 show "subpath 0 t g ` {0..<1} \<inter> S \<noteq> {}" |
2086 show "subpath 0 t g ` {0..<1} \<inter> S \<noteq> {}" |
2105 using \<open>y \<in> S\<close> g(1) by (force simp: subpath_def image_def pathstart_def) |
2087 using \<open>y \<in> S\<close> g(1) by (force simp: subpath_def image_def pathstart_def) |
2106 qed |
2088 qed |
2107 then obtain x where "x \<in> subpath 0 t g ` {0..<1}" "x \<in> frontier S" |
2089 then obtain x where "x \<in> subpath 0 t g ` {0..<1}" "x \<in> frontier S" |
2108 by blast |
2090 by blast |
2137 by (auto simp: path_component_def) |
2119 by (auto simp: path_component_def) |
2138 then have "path (f +++ g)" |
2120 then have "path (f +++ g)" |
2139 by (simp add: \<open>arc g\<close> arc_imp_path) |
2121 by (simp add: \<open>arc g\<close> arc_imp_path) |
2140 then obtain h where "arc h" |
2122 then obtain h where "arc h" |
2141 and h: "path_image h \<subseteq> path_image (f +++ g)" "pathstart h = x" "pathfinish h = pathfinish g" |
2123 and h: "path_image h \<subseteq> path_image (f +++ g)" "pathstart h = x" "pathfinish h = pathfinish g" |
2142 apply (rule path_contains_arc [of "f +++ g" x "pathfinish g"]) |
2124 using path_contains_arc [of "f +++ g" x "pathfinish g"] \<open>x \<notin> V\<close> \<open>pathfinish g \<in> V\<close> f |
2143 using f \<open>x \<notin> V\<close> \<open>pathfinish g \<in> V\<close> by auto |
2125 by (metis pathfinish_join pathstart_join) |
2144 have "h ` {0..1} - {h 1} \<subseteq> S" |
2126 have "path_image h \<subseteq> path_image f \<union> path_image g" |
2145 using f g h apply (clarsimp simp: path_image_join) |
2127 using h(1) path_image_join_subset by auto |
|
2128 then have "h ` {0..1} - {h 1} \<subseteq> S" |
|
2129 using f g h |
2146 apply (simp add: path_image_def pathfinish_def subset_iff image_def Bex_def) |
2130 apply (simp add: path_image_def pathfinish_def subset_iff image_def Bex_def) |
2147 by (metis le_less) |
2131 by (metis le_less) |
2148 then have "h ` {0..<1} \<subseteq> S" |
2132 then have "h ` {0..<1} \<subseteq> S" |
2149 using \<open>arc h\<close> by (force simp: arc_def dest: inj_onD) |
2133 using \<open>arc h\<close> by (force simp: arc_def dest: inj_onD) |
2150 then show thesis |
2134 then show thesis |
2151 apply (rule that [OF \<open>arc h\<close>]) |
2135 using \<open>arc h\<close> g(3) h that by presburger |
2152 using h \<open>pathfinish g \<in> V\<close> by auto |
|
2153 qed |
2136 qed |
2154 |
2137 |
2155 lemma dense_access_fp_aux: |
2138 lemma dense_access_fp_aux: |
2156 fixes S :: "'a::{complete_space,real_normed_vector} set" |
2139 fixes S :: "'a::{complete_space,real_normed_vector} set" |
2157 assumes S: "open S" "connected S" |
2140 assumes S: "open S" "connected S" |