464 done |
464 done |
465 |
465 |
466 instance .. |
466 instance .. |
467 |
467 |
468 end |
468 end |
469 |
|
470 lemma fps_nonzero_least_unique: |
|
471 assumes a0: "a \<noteq> 0" |
|
472 shows "\<exists>!n. leastP (\<lambda>n. a$n \<noteq> 0) n" |
|
473 proof - |
|
474 from fps_nonzero_nth_minimal [of a] a0 |
|
475 obtain n where "a$n \<noteq> 0" "\<forall>m < n. a$m = 0" by blast |
|
476 then have ln: "leastP (\<lambda>n. a$n \<noteq> 0) n" |
|
477 by (auto simp add: leastP_def setge_def not_le [symmetric]) |
|
478 moreover |
|
479 { |
|
480 fix m |
|
481 assume "leastP (\<lambda>n. a $ n \<noteq> 0) m" |
|
482 then have "m = n" using ln |
|
483 apply (auto simp add: leastP_def setge_def) |
|
484 apply (erule allE[where x=n]) |
|
485 apply (erule allE[where x=m]) |
|
486 apply simp |
|
487 done |
|
488 } |
|
489 ultimately show ?thesis by blast |
|
490 qed |
|
491 |
|
492 lemma fps_eq_least_unique: |
|
493 assumes "(a::('a::ab_group_add) fps) \<noteq> b" |
|
494 shows "\<exists>! n. leastP (\<lambda>n. a$n \<noteq> b$n) n" |
|
495 using fps_nonzero_least_unique[of "a - b"] assms |
|
496 by auto |
|
497 |
469 |
498 instantiation fps :: (comm_ring_1) metric_space |
470 instantiation fps :: (comm_ring_1) metric_space |
499 begin |
471 begin |
500 |
472 |
501 definition open_fps_def: "open (S :: 'a fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)" |
473 definition open_fps_def: "open (S :: 'a fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)" |
538 by (cases "c = a") (simp_all add: th dist_fps_sym) |
510 by (cases "c = a") (simp_all add: th dist_fps_sym) |
539 } |
511 } |
540 moreover |
512 moreover |
541 { |
513 { |
542 assume ab: "a \<noteq> b" and ac: "a \<noteq> c" and bc: "b \<noteq> c" |
514 assume ab: "a \<noteq> b" and ac: "a \<noteq> c" and bc: "b \<noteq> c" |
543 let ?P = "\<lambda>a b n. a$n \<noteq> b$n" |
515 def n \<equiv> "\<lambda>a b::'a fps. LEAST n. a$n \<noteq> b$n" |
544 from fps_eq_least_unique[OF ab] fps_eq_least_unique[OF ac] |
516 then have n': "\<And>m a b. m < n a b \<Longrightarrow> a$m = b$m" |
545 fps_eq_least_unique[OF bc] |
517 by (auto dest: not_less_Least) |
546 obtain nab nac nbc where nab: "leastP (?P a b) nab" |
518 |
547 and nac: "leastP (?P a c) nac" |
519 from ab ac bc |
548 and nbc: "leastP (?P b c) nbc" by blast |
520 have dab: "dist a b = inverse (2 ^ n a b)" |
549 from nab have nab': "\<And>m. m < nab \<Longrightarrow> a$m = b$m" "a$nab \<noteq> b$nab" |
521 and dac: "dist a c = inverse (2 ^ n a c)" |
550 by (auto simp add: leastP_def setge_def) |
522 and dbc: "dist b c = inverse (2 ^ n b c)" |
551 from nac have nac': "\<And>m. m < nac \<Longrightarrow> a$m = c$m" "a$nac \<noteq> c$nac" |
523 by (simp_all add: dist_fps_def n_def fps_eq_iff) |
552 by (auto simp add: leastP_def setge_def) |
|
553 from nbc have nbc': "\<And>m. m < nbc \<Longrightarrow> b$m = c$m" "b$nbc \<noteq> c$nbc" |
|
554 by (auto simp add: leastP_def setge_def) |
|
555 |
|
556 have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)" |
|
557 by (simp add: fps_eq_iff) |
|
558 from ab ac bc nab nac nbc |
|
559 have dab: "dist a b = inverse (2 ^ nab)" |
|
560 and dac: "dist a c = inverse (2 ^ nac)" |
|
561 and dbc: "dist b c = inverse (2 ^ nbc)" |
|
562 unfolding th0 |
|
563 apply (simp_all add: dist_fps_def) |
|
564 apply (erule the1_equality[OF fps_eq_least_unique[OF ab]]) |
|
565 apply (erule the1_equality[OF fps_eq_least_unique[OF ac]]) |
|
566 apply (erule the1_equality[OF fps_eq_least_unique[OF bc]]) |
|
567 done |
|
568 from ab ac bc have nz: "dist a b \<noteq> 0" "dist a c \<noteq> 0" "dist b c \<noteq> 0" |
524 from ab ac bc have nz: "dist a b \<noteq> 0" "dist a c \<noteq> 0" "dist b c \<noteq> 0" |
569 unfolding th by simp_all |
525 unfolding th by simp_all |
570 from nz have pos: "dist a b > 0" "dist a c > 0" "dist b c > 0" |
526 from nz have pos: "dist a b > 0" "dist a c > 0" "dist b c > 0" |
571 using dist_fps_ge0[of a b] dist_fps_ge0[of a c] dist_fps_ge0[of b c] |
527 using dist_fps_ge0[of a b] dist_fps_ge0[of a c] dist_fps_ge0[of b c] |
572 by auto |
528 by auto |
573 have th1: "\<And>n. (2::real)^n >0" by auto |
529 have th1: "\<And>n. (2::real)^n >0" by auto |
574 { |
530 { |
575 assume h: "dist a b > dist a c + dist b c" |
531 assume h: "dist a b > dist a c + dist b c" |
576 then have gt: "dist a b > dist a c" "dist a b > dist b c" |
532 then have gt: "dist a b > dist a c" "dist a b > dist b c" |
577 using pos by auto |
533 using pos by auto |
578 from gt have gtn: "nab < nbc" "nab < nac" |
534 from gt have gtn: "n a b < n b c" "n a b < n a c" |
579 unfolding dab dbc dac by (auto simp add: th1) |
535 unfolding dab dbc dac by (auto simp add: th1) |
580 from nac'(1)[OF gtn(2)] nbc'(1)[OF gtn(1)] |
536 from n'[OF gtn(2)] n'(1)[OF gtn(1)] |
581 have "a $ nab = b $ nab" by simp |
537 have "a $ n a b = b $ n a b" by simp |
582 with nab'(2) have False by simp |
538 moreover have "a $ n a b \<noteq> b $ n a b" |
|
539 unfolding n_def by (rule LeastI_ex) (insert ab, simp add: fps_eq_iff) |
|
540 ultimately have False by contradiction |
583 } |
541 } |
584 then have "dist a b \<le> dist a c + dist b c" |
542 then have "dist a b \<le> dist a c + dist b c" |
585 by (auto simp add: not_le[symmetric]) |
543 by (auto simp add: not_le[symmetric]) |
586 } |
544 } |
587 ultimately show "dist a b \<le> dist a c + dist b c" by blast |
545 ultimately show "dist a b \<le> dist a c + dist b c" by blast |
647 using rp by (simp del: dist_eq_0_iff) |
605 using rp by (simp del: dist_eq_0_iff) |
648 } |
606 } |
649 moreover |
607 moreover |
650 { |
608 { |
651 assume neq: "?s n \<noteq> a" |
609 assume neq: "?s n \<noteq> a" |
652 from fps_eq_least_unique[OF neq] |
610 def k \<equiv> "LEAST i. ?s n $ i \<noteq> a $ i" |
653 obtain k where k: "leastP (\<lambda>i. ?s n $ i \<noteq> a$i) k" by blast |
|
654 have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)" |
|
655 by (simp add: fps_eq_iff) |
|
656 from neq have dth: "dist (?s n) a = (1/2)^k" |
611 from neq have dth: "dist (?s n) a = (1/2)^k" |
657 unfolding th0 dist_fps_def |
612 by (auto simp add: dist_fps_def inverse_eq_divide power_divide k_def fps_eq_iff) |
658 unfolding the1_equality[OF fps_eq_least_unique[OF neq], OF k] |
613 |
659 by (auto simp add: inverse_eq_divide power_divide) |
614 from neq have kn: "k > n" |
660 |
615 by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff split: split_if_asm intro: LeastI2_ex) |
661 from k have kn: "k > n" |
|
662 by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm) |
|
663 then have "dist (?s n) a < (1/2)^n" unfolding dth |
616 then have "dist (?s n) a < (1/2)^n" unfolding dth |
664 by (auto intro: power_strict_decreasing) |
617 by (auto intro: power_strict_decreasing) |
665 also have "\<dots> <= (1/2)^n0" using nn0 |
618 also have "\<dots> <= (1/2)^n0" using nn0 |
666 by (auto intro: power_decreasing) |
619 by (auto intro: power_decreasing) |
667 also have "\<dots> < r" using n0 by simp |
620 also have "\<dots> < r" using n0 by simp |
3795 |
3748 |
3796 lemma dist_less_imp_nth_equal: |
3749 lemma dist_less_imp_nth_equal: |
3797 assumes "dist f g < inverse (2 ^ i)" |
3750 assumes "dist f g < inverse (2 ^ i)" |
3798 and"j \<le> i" |
3751 and"j \<le> i" |
3799 shows "f $ j = g $ j" |
3752 shows "f $ j = g $ j" |
3800 proof (cases "f = g") |
3753 proof (rule ccontr) |
3801 case False |
3754 assume "f $ j \<noteq> g $ j" |
3802 hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff) |
3755 then have "\<exists>n. f $ n \<noteq> g $ n" by auto |
3803 with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))" |
3756 with assms have "i < (LEAST n. f $ n \<noteq> g $ n)" |
3804 by (simp add: split_if_asm dist_fps_def) |
3757 by (simp add: split_if_asm dist_fps_def) |
3805 moreover |
3758 also have "\<dots> \<le> j" |
3806 from fps_eq_least_unique[OF `f \<noteq> g`] |
3759 using `f $ j \<noteq> g $ j` by (auto intro: Least_le) |
3807 obtain n where n: "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast |
3760 finally show False using `j \<le> i` by simp |
3808 moreover from n have "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n" |
|
3809 by (auto simp add: leastP_def setge_def) |
|
3810 ultimately show ?thesis using `j \<le> i` by simp |
|
3811 next |
|
3812 case True |
|
3813 then show ?thesis by simp |
|
3814 qed |
3761 qed |
3815 |
3762 |
3816 lemma nth_equal_imp_dist_less: |
3763 lemma nth_equal_imp_dist_less: |
3817 assumes "\<And>j. j \<le> i \<Longrightarrow> f $ j = g $ j" |
3764 assumes "\<And>j. j \<le> i \<Longrightarrow> f $ j = g $ j" |
3818 shows "dist f g < inverse (2 ^ i)" |
3765 shows "dist f g < inverse (2 ^ i)" |
3819 proof (cases "f = g") |
3766 proof (cases "f = g") |
3820 case False |
3767 case False |
3821 hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff) |
3768 hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff) |
3822 with assms have "dist f g = inverse (2 ^ (The (leastP (\<lambda>n. f $ n \<noteq> g $ n))))" |
3769 with assms have "dist f g = inverse (2 ^ (LEAST n. f $ n \<noteq> g $ n))" |
3823 by (simp add: split_if_asm dist_fps_def) |
3770 by (simp add: split_if_asm dist_fps_def) |
3824 moreover |
3771 moreover |
3825 from fps_eq_least_unique[OF `f \<noteq> g`] |
3772 from assms `\<exists>n. f $ n \<noteq> g $ n` have "i < (LEAST n. f $ n \<noteq> g $ n)" |
3826 obtain n where "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast |
3773 by (metis (mono_tags) LeastI not_less) |
3827 with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))" |
|
3828 by (metis (full_types) leastPD1 not_le) |
|
3829 ultimately show ?thesis by simp |
3774 ultimately show ?thesis by simp |
3830 next |
3775 qed simp |
3831 case True |
|
3832 then show ?thesis by simp |
|
3833 qed |
|
3834 |
3776 |
3835 lemma dist_less_eq_nth_equal: "dist f g < inverse (2 ^ i) \<longleftrightarrow> (\<forall>j \<le> i. f $ j = g $ j)" |
3777 lemma dist_less_eq_nth_equal: "dist f g < inverse (2 ^ i) \<longleftrightarrow> (\<forall>j \<le> i. f $ j = g $ j)" |
3836 using dist_less_imp_nth_equal nth_equal_imp_dist_less by blast |
3778 using dist_less_imp_nth_equal nth_equal_imp_dist_less by blast |
3837 |
3779 |
3838 instance fps :: (comm_ring_1) complete_space |
3780 instance fps :: (comm_ring_1) complete_space |