609 by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2]) |
606 by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2]) |
610 |
607 |
611 |
608 |
612 subsection\<open>The Infinitely Close Relation\<close> |
609 subsection\<open>The Infinitely Close Relation\<close> |
613 |
610 |
614 lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)" |
611 lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x \<approx> 0)" |
615 by (simp add: Infinitesimal_def approx_def) |
612 by (simp add: Infinitesimal_def approx_def) |
616 |
613 |
617 lemma approx_minus_iff: " (x @= y) = (x - y @= 0)" |
614 lemma approx_minus_iff: " (x \<approx> y) = (x - y \<approx> 0)" |
618 by (simp add: approx_def) |
615 by (simp add: approx_def) |
619 |
616 |
620 lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)" |
617 lemma approx_minus_iff2: " (x \<approx> y) = (-y + x \<approx> 0)" |
621 by (simp add: approx_def add.commute) |
618 by (simp add: approx_def add.commute) |
622 |
619 |
623 lemma approx_refl [iff]: "x @= x" |
620 lemma approx_refl [iff]: "x \<approx> x" |
624 by (simp add: approx_def Infinitesimal_def) |
621 by (simp add: approx_def Infinitesimal_def) |
625 |
622 |
626 lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y" |
623 lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y" |
627 by (simp add: add.commute) |
624 by (simp add: add.commute) |
628 |
625 |
629 lemma approx_sym: "x @= y ==> y @= x" |
626 lemma approx_sym: "x \<approx> y ==> y \<approx> x" |
630 apply (simp add: approx_def) |
627 apply (simp add: approx_def) |
631 apply (drule Infinitesimal_minus_iff [THEN iffD2]) |
628 apply (drule Infinitesimal_minus_iff [THEN iffD2]) |
632 apply simp |
629 apply simp |
633 done |
630 done |
634 |
631 |
635 lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z" |
632 lemma approx_trans: "[| x \<approx> y; y \<approx> z |] ==> x \<approx> z" |
636 apply (simp add: approx_def) |
633 apply (simp add: approx_def) |
637 apply (drule (1) Infinitesimal_add) |
634 apply (drule (1) Infinitesimal_add) |
638 apply simp |
635 apply simp |
639 done |
636 done |
640 |
637 |
641 lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s" |
638 lemma approx_trans2: "[| r \<approx> x; s \<approx> x |] ==> r \<approx> s" |
642 by (blast intro: approx_sym approx_trans) |
639 by (blast intro: approx_sym approx_trans) |
643 |
640 |
644 lemma approx_trans3: "[| x @= r; x @= s|] ==> r @= s" |
641 lemma approx_trans3: "[| x \<approx> r; x \<approx> s|] ==> r \<approx> s" |
645 by (blast intro: approx_sym approx_trans) |
642 by (blast intro: approx_sym approx_trans) |
646 |
643 |
647 lemma approx_reorient: "(x @= y) = (y @= x)" |
644 lemma approx_reorient: "(x \<approx> y) = (y \<approx> x)" |
648 by (blast intro: approx_sym) |
645 by (blast intro: approx_sym) |
649 |
646 |
650 (*reorientation simplification procedure: reorients (polymorphic) |
647 (*reorientation simplification procedure: reorients (polymorphic) |
651 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) |
648 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) |
652 simproc_setup approx_reorient_simproc |
649 simproc_setup approx_reorient_simproc |
653 ("0 @= x" | "1 @= y" | "numeral w @= z" | "- 1 @= y" | "- numeral w @= r") = |
650 ("0 \<approx> x" | "1 \<approx> y" | "numeral w \<approx> z" | "- 1 \<approx> y" | "- numeral w \<approx> r") = |
654 \<open> |
651 \<open> |
655 let val rule = @{thm approx_reorient} RS eq_reflection |
652 let val rule = @{thm approx_reorient} RS eq_reflection |
656 fun proc phi ss ct = |
653 fun proc phi ss ct = |
657 case Thm.term_of ct of |
654 case Thm.term_of ct of |
658 _ $ t $ u => if can HOLogic.dest_number u then NONE |
655 _ $ t $ u => if can HOLogic.dest_number u then NONE |
659 else if can HOLogic.dest_number t then SOME rule else NONE |
656 else if can HOLogic.dest_number t then SOME rule else NONE |
660 | _ => NONE |
657 | _ => NONE |
661 in proc end |
658 in proc end |
662 \<close> |
659 \<close> |
663 |
660 |
664 lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)" |
661 lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x \<approx> y)" |
665 by (simp add: approx_minus_iff [symmetric] mem_infmal_iff) |
662 by (simp add: approx_minus_iff [symmetric] mem_infmal_iff) |
666 |
663 |
667 lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))" |
664 lemma approx_monad_iff: "(x \<approx> y) = (monad(x)=monad(y))" |
668 apply (simp add: monad_def) |
665 apply (simp add: monad_def) |
669 apply (auto dest: approx_sym elim!: approx_trans equalityCE) |
666 apply (auto dest: approx_sym elim!: approx_trans equalityCE) |
670 done |
667 done |
671 |
668 |
672 lemma Infinitesimal_approx: |
669 lemma Infinitesimal_approx: |
673 "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x @= y" |
670 "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x \<approx> y" |
674 apply (simp add: mem_infmal_iff) |
671 apply (simp add: mem_infmal_iff) |
675 apply (blast intro: approx_trans approx_sym) |
672 apply (blast intro: approx_trans approx_sym) |
676 done |
673 done |
677 |
674 |
678 lemma approx_add: "[| a @= b; c @= d |] ==> a+c @= b+d" |
675 lemma approx_add: "[| a \<approx> b; c \<approx> d |] ==> a+c \<approx> b+d" |
679 proof (unfold approx_def) |
676 proof (unfold approx_def) |
680 assume inf: "a - b \<in> Infinitesimal" "c - d \<in> Infinitesimal" |
677 assume inf: "a - b \<in> Infinitesimal" "c - d \<in> Infinitesimal" |
681 have "a + c - (b + d) = (a - b) + (c - d)" by simp |
678 have "a + c - (b + d) = (a - b) + (c - d)" by simp |
682 also have "... \<in> Infinitesimal" using inf by (rule Infinitesimal_add) |
679 also have "... \<in> Infinitesimal" using inf by (rule Infinitesimal_add) |
683 finally show "a + c - (b + d) \<in> Infinitesimal" . |
680 finally show "a + c - (b + d) \<in> Infinitesimal" . |
684 qed |
681 qed |
685 |
682 |
686 lemma approx_minus: "a @= b ==> -a @= -b" |
683 lemma approx_minus: "a \<approx> b ==> -a \<approx> -b" |
687 apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym]) |
684 apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym]) |
688 apply (drule approx_minus_iff [THEN iffD1]) |
685 apply (drule approx_minus_iff [THEN iffD1]) |
689 apply (simp add: add.commute) |
686 apply (simp add: add.commute) |
690 done |
687 done |
691 |
688 |
692 lemma approx_minus2: "-a @= -b ==> a @= b" |
689 lemma approx_minus2: "-a \<approx> -b ==> a \<approx> b" |
693 by (auto dest: approx_minus) |
690 by (auto dest: approx_minus) |
694 |
691 |
695 lemma approx_minus_cancel [simp]: "(-a @= -b) = (a @= b)" |
692 lemma approx_minus_cancel [simp]: "(-a \<approx> -b) = (a \<approx> b)" |
696 by (blast intro: approx_minus approx_minus2) |
693 by (blast intro: approx_minus approx_minus2) |
697 |
694 |
698 lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d" |
695 lemma approx_add_minus: "[| a \<approx> b; c \<approx> d |] ==> a + -c \<approx> b + -d" |
699 by (blast intro!: approx_add approx_minus) |
696 by (blast intro!: approx_add approx_minus) |
700 |
697 |
701 lemma approx_diff: "[| a @= b; c @= d |] ==> a - c @= b - d" |
698 lemma approx_diff: "[| a \<approx> b; c \<approx> d |] ==> a - c \<approx> b - d" |
702 using approx_add [of a b "- c" "- d"] by simp |
699 using approx_add [of a b "- c" "- d"] by simp |
703 |
700 |
704 lemma approx_mult1: |
701 lemma approx_mult1: |
705 fixes a b c :: "'a::real_normed_algebra star" |
702 fixes a b c :: "'a::real_normed_algebra star" |
706 shows "[| a @= b; c: HFinite|] ==> a*c @= b*c" |
703 shows "[| a \<approx> b; c: HFinite|] ==> a*c \<approx> b*c" |
707 by (simp add: approx_def Infinitesimal_HFinite_mult |
704 by (simp add: approx_def Infinitesimal_HFinite_mult |
708 left_diff_distrib [symmetric]) |
705 left_diff_distrib [symmetric]) |
709 |
706 |
710 lemma approx_mult2: |
707 lemma approx_mult2: |
711 fixes a b c :: "'a::real_normed_algebra star" |
708 fixes a b c :: "'a::real_normed_algebra star" |
712 shows "[|a @= b; c: HFinite|] ==> c*a @= c*b" |
709 shows "[|a \<approx> b; c: HFinite|] ==> c*a \<approx> c*b" |
713 by (simp add: approx_def Infinitesimal_HFinite_mult2 |
710 by (simp add: approx_def Infinitesimal_HFinite_mult2 |
714 right_diff_distrib [symmetric]) |
711 right_diff_distrib [symmetric]) |
715 |
712 |
716 lemma approx_mult_subst: |
713 lemma approx_mult_subst: |
717 fixes u v x y :: "'a::real_normed_algebra star" |
714 fixes u v x y :: "'a::real_normed_algebra star" |
718 shows "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y" |
715 shows "[|u \<approx> v*x; x \<approx> y; v \<in> HFinite|] ==> u \<approx> v*y" |
719 by (blast intro: approx_mult2 approx_trans) |
716 by (blast intro: approx_mult2 approx_trans) |
720 |
717 |
721 lemma approx_mult_subst2: |
718 lemma approx_mult_subst2: |
722 fixes u v x y :: "'a::real_normed_algebra star" |
719 fixes u v x y :: "'a::real_normed_algebra star" |
723 shows "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v" |
720 shows "[| u \<approx> x*v; x \<approx> y; v \<in> HFinite |] ==> u \<approx> y*v" |
724 by (blast intro: approx_mult1 approx_trans) |
721 by (blast intro: approx_mult1 approx_trans) |
725 |
722 |
726 lemma approx_mult_subst_star_of: |
723 lemma approx_mult_subst_star_of: |
727 fixes u x y :: "'a::real_normed_algebra star" |
724 fixes u x y :: "'a::real_normed_algebra star" |
728 shows "[| u @= x*star_of v; x @= y |] ==> u @= y*star_of v" |
725 shows "[| u \<approx> x*star_of v; x \<approx> y |] ==> u \<approx> y*star_of v" |
729 by (auto intro: approx_mult_subst2) |
726 by (auto intro: approx_mult_subst2) |
730 |
727 |
731 lemma approx_eq_imp: "a = b ==> a @= b" |
728 lemma approx_eq_imp: "a = b ==> a \<approx> b" |
732 by (simp add: approx_def) |
729 by (simp add: approx_def) |
733 |
730 |
734 lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x @= x" |
731 lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x \<approx> x" |
735 by (blast intro: Infinitesimal_minus_iff [THEN iffD2] |
732 by (blast intro: Infinitesimal_minus_iff [THEN iffD2] |
736 mem_infmal_iff [THEN iffD1] approx_trans2) |
733 mem_infmal_iff [THEN iffD1] approx_trans2) |
737 |
734 |
738 lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x - z = y) = (x @= z)" |
735 lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x - z = y) = (x \<approx> z)" |
739 by (simp add: approx_def) |
736 by (simp add: approx_def) |
740 |
737 |
741 lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x @= z)" |
738 lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x \<approx> z)" |
742 by (force simp add: bex_Infinitesimal_iff [symmetric]) |
739 by (force simp add: bex_Infinitesimal_iff [symmetric]) |
743 |
740 |
744 lemma Infinitesimal_add_approx: "[| y \<in> Infinitesimal; x + y = z |] ==> x @= z" |
741 lemma Infinitesimal_add_approx: "[| y \<in> Infinitesimal; x + y = z |] ==> x \<approx> z" |
745 apply (rule bex_Infinitesimal_iff [THEN iffD1]) |
742 apply (rule bex_Infinitesimal_iff [THEN iffD1]) |
746 apply (drule Infinitesimal_minus_iff [THEN iffD2]) |
743 apply (drule Infinitesimal_minus_iff [THEN iffD2]) |
747 apply (auto simp add: add.assoc [symmetric]) |
744 apply (auto simp add: add.assoc [symmetric]) |
748 done |
745 done |
749 |
746 |
750 lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal ==> x @= x + y" |
747 lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal ==> x \<approx> x + y" |
751 apply (rule bex_Infinitesimal_iff [THEN iffD1]) |
748 apply (rule bex_Infinitesimal_iff [THEN iffD1]) |
752 apply (drule Infinitesimal_minus_iff [THEN iffD2]) |
749 apply (drule Infinitesimal_minus_iff [THEN iffD2]) |
753 apply (auto simp add: add.assoc [symmetric]) |
750 apply (auto simp add: add.assoc [symmetric]) |
754 done |
751 done |
755 |
752 |
756 lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal ==> x @= y + x" |
753 lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal ==> x \<approx> y + x" |
757 by (auto dest: Infinitesimal_add_approx_self simp add: add.commute) |
754 by (auto dest: Infinitesimal_add_approx_self simp add: add.commute) |
758 |
755 |
759 lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal ==> x @= x + -y" |
756 lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal ==> x \<approx> x + -y" |
760 by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2]) |
757 by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2]) |
761 |
758 |
762 lemma Infinitesimal_add_cancel: "[| y \<in> Infinitesimal; x+y @= z|] ==> x @= z" |
759 lemma Infinitesimal_add_cancel: "[| y \<in> Infinitesimal; x+y \<approx> z|] ==> x \<approx> z" |
763 apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym]) |
760 apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym]) |
764 apply (erule approx_trans3 [THEN approx_sym], assumption) |
761 apply (erule approx_trans3 [THEN approx_sym], assumption) |
765 done |
762 done |
766 |
763 |
767 lemma Infinitesimal_add_right_cancel: |
764 lemma Infinitesimal_add_right_cancel: |
768 "[| y \<in> Infinitesimal; x @= z + y|] ==> x @= z" |
765 "[| y \<in> Infinitesimal; x \<approx> z + y|] ==> x \<approx> z" |
769 apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym]) |
766 apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym]) |
770 apply (erule approx_trans3 [THEN approx_sym]) |
767 apply (erule approx_trans3 [THEN approx_sym]) |
771 apply (simp add: add.commute) |
768 apply (simp add: add.commute) |
772 apply (erule approx_sym) |
769 apply (erule approx_sym) |
773 done |
770 done |
774 |
771 |
775 lemma approx_add_left_cancel: "d + b @= d + c ==> b @= c" |
772 lemma approx_add_left_cancel: "d + b \<approx> d + c ==> b \<approx> c" |
776 apply (drule approx_minus_iff [THEN iffD1]) |
773 apply (drule approx_minus_iff [THEN iffD1]) |
777 apply (simp add: approx_minus_iff [symmetric] ac_simps) |
774 apply (simp add: approx_minus_iff [symmetric] ac_simps) |
778 done |
775 done |
779 |
776 |
780 lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c" |
777 lemma approx_add_right_cancel: "b + d \<approx> c + d ==> b \<approx> c" |
781 apply (rule approx_add_left_cancel) |
778 apply (rule approx_add_left_cancel) |
782 apply (simp add: add.commute) |
779 apply (simp add: add.commute) |
783 done |
780 done |
784 |
781 |
785 lemma approx_add_mono1: "b @= c ==> d + b @= d + c" |
782 lemma approx_add_mono1: "b \<approx> c ==> d + b \<approx> d + c" |
786 apply (rule approx_minus_iff [THEN iffD2]) |
783 apply (rule approx_minus_iff [THEN iffD2]) |
787 apply (simp add: approx_minus_iff [symmetric] ac_simps) |
784 apply (simp add: approx_minus_iff [symmetric] ac_simps) |
788 done |
785 done |
789 |
786 |
790 lemma approx_add_mono2: "b @= c ==> b + a @= c + a" |
787 lemma approx_add_mono2: "b \<approx> c ==> b + a \<approx> c + a" |
791 by (simp add: add.commute approx_add_mono1) |
788 by (simp add: add.commute approx_add_mono1) |
792 |
789 |
793 lemma approx_add_left_iff [simp]: "(a + b @= a + c) = (b @= c)" |
790 lemma approx_add_left_iff [simp]: "(a + b \<approx> a + c) = (b \<approx> c)" |
794 by (fast elim: approx_add_left_cancel approx_add_mono1) |
791 by (fast elim: approx_add_left_cancel approx_add_mono1) |
795 |
792 |
796 lemma approx_add_right_iff [simp]: "(b + a @= c + a) = (b @= c)" |
793 lemma approx_add_right_iff [simp]: "(b + a \<approx> c + a) = (b \<approx> c)" |
797 by (simp add: add.commute) |
794 by (simp add: add.commute) |
798 |
795 |
799 lemma approx_HFinite: "[| x \<in> HFinite; x @= y |] ==> y \<in> HFinite" |
796 lemma approx_HFinite: "[| x \<in> HFinite; x \<approx> y |] ==> y \<in> HFinite" |
800 apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe) |
797 apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe) |
801 apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]]) |
798 apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]]) |
802 apply (drule HFinite_add) |
799 apply (drule HFinite_add) |
803 apply (auto simp add: add.assoc) |
800 apply (auto simp add: add.assoc) |
804 done |
801 done |
805 |
802 |
806 lemma approx_star_of_HFinite: "x @= star_of D ==> x \<in> HFinite" |
803 lemma approx_star_of_HFinite: "x \<approx> star_of D ==> x \<in> HFinite" |
807 by (rule approx_sym [THEN [2] approx_HFinite], auto) |
804 by (rule approx_sym [THEN [2] approx_HFinite], auto) |
808 |
805 |
809 lemma approx_mult_HFinite: |
806 lemma approx_mult_HFinite: |
810 fixes a b c d :: "'a::real_normed_algebra star" |
807 fixes a b c d :: "'a::real_normed_algebra star" |
811 shows "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d" |
808 shows "[|a \<approx> b; c \<approx> d; b: HFinite; d: HFinite|] ==> a*c \<approx> b*d" |
812 apply (rule approx_trans) |
809 apply (rule approx_trans) |
813 apply (rule_tac [2] approx_mult2) |
810 apply (rule_tac [2] approx_mult2) |
814 apply (rule approx_mult1) |
811 apply (rule approx_mult1) |
815 prefer 2 apply (blast intro: approx_HFinite approx_sym, auto) |
812 prefer 2 apply (blast intro: approx_HFinite approx_sym, auto) |
816 done |
813 done |
818 lemma scaleHR_left_diff_distrib: |
815 lemma scaleHR_left_diff_distrib: |
819 "\<And>a b x. scaleHR (a - b) x = scaleHR a x - scaleHR b x" |
816 "\<And>a b x. scaleHR (a - b) x = scaleHR a x - scaleHR b x" |
820 by transfer (rule scaleR_left_diff_distrib) |
817 by transfer (rule scaleR_left_diff_distrib) |
821 |
818 |
822 lemma approx_scaleR1: |
819 lemma approx_scaleR1: |
823 "[| a @= star_of b; c: HFinite|] ==> scaleHR a c @= b *\<^sub>R c" |
820 "[| a \<approx> star_of b; c: HFinite|] ==> scaleHR a c \<approx> b *\<^sub>R c" |
824 apply (unfold approx_def) |
821 apply (unfold approx_def) |
825 apply (drule (1) Infinitesimal_HFinite_scaleHR) |
822 apply (drule (1) Infinitesimal_HFinite_scaleHR) |
826 apply (simp only: scaleHR_left_diff_distrib) |
823 apply (simp only: scaleHR_left_diff_distrib) |
827 apply (simp add: scaleHR_def star_scaleR_def [symmetric]) |
824 apply (simp add: scaleHR_def star_scaleR_def [symmetric]) |
828 done |
825 done |
829 |
826 |
830 lemma approx_scaleR2: |
827 lemma approx_scaleR2: |
831 "a @= b ==> c *\<^sub>R a @= c *\<^sub>R b" |
828 "a \<approx> b ==> c *\<^sub>R a \<approx> c *\<^sub>R b" |
832 by (simp add: approx_def Infinitesimal_scaleR2 |
829 by (simp add: approx_def Infinitesimal_scaleR2 |
833 scaleR_right_diff_distrib [symmetric]) |
830 scaleR_right_diff_distrib [symmetric]) |
834 |
831 |
835 lemma approx_scaleR_HFinite: |
832 lemma approx_scaleR_HFinite: |
836 "[|a @= star_of b; c @= d; d: HFinite|] ==> scaleHR a c @= b *\<^sub>R d" |
833 "[|a \<approx> star_of b; c \<approx> d; d: HFinite|] ==> scaleHR a c \<approx> b *\<^sub>R d" |
837 apply (rule approx_trans) |
834 apply (rule approx_trans) |
838 apply (rule_tac [2] approx_scaleR2) |
835 apply (rule_tac [2] approx_scaleR2) |
839 apply (rule approx_scaleR1) |
836 apply (rule approx_scaleR1) |
840 prefer 2 apply (blast intro: approx_HFinite approx_sym, auto) |
837 prefer 2 apply (blast intro: approx_HFinite approx_sym, auto) |
841 done |
838 done |
842 |
839 |
843 lemma approx_mult_star_of: |
840 lemma approx_mult_star_of: |
844 fixes a c :: "'a::real_normed_algebra star" |
841 fixes a c :: "'a::real_normed_algebra star" |
845 shows "[|a @= star_of b; c @= star_of d |] |
842 shows "[|a \<approx> star_of b; c \<approx> star_of d |] |
846 ==> a*c @= star_of b*star_of d" |
843 ==> a*c \<approx> star_of b*star_of d" |
847 by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of) |
844 by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of) |
848 |
845 |
849 lemma approx_SReal_mult_cancel_zero: |
846 lemma approx_SReal_mult_cancel_zero: |
850 "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a*x @= 0 |] ==> x @= 0" |
847 "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a*x \<approx> 0 |] ==> x \<approx> 0" |
851 apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) |
848 apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) |
852 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric]) |
849 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric]) |
853 done |
850 done |
854 |
851 |
855 lemma approx_mult_SReal1: "[| (a::hypreal) \<in> \<real>; x @= 0 |] ==> x*a @= 0" |
852 lemma approx_mult_SReal1: "[| (a::hypreal) \<in> \<real>; x \<approx> 0 |] ==> x*a \<approx> 0" |
856 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1) |
853 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1) |
857 |
854 |
858 lemma approx_mult_SReal2: "[| (a::hypreal) \<in> \<real>; x @= 0 |] ==> a*x @= 0" |
855 lemma approx_mult_SReal2: "[| (a::hypreal) \<in> \<real>; x \<approx> 0 |] ==> a*x \<approx> 0" |
859 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2) |
856 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2) |
860 |
857 |
861 lemma approx_mult_SReal_zero_cancel_iff [simp]: |
858 lemma approx_mult_SReal_zero_cancel_iff [simp]: |
862 "[|(a::hypreal) \<in> \<real>; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)" |
859 "[|(a::hypreal) \<in> \<real>; a \<noteq> 0 |] ==> (a*x \<approx> 0) = (x \<approx> 0)" |
863 by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2) |
860 by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2) |
864 |
861 |
865 lemma approx_SReal_mult_cancel: |
862 lemma approx_SReal_mult_cancel: |
866 "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a* w @= a*z |] ==> w @= z" |
863 "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a* w \<approx> a*z |] ==> w \<approx> z" |
867 apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) |
864 apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) |
868 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric]) |
865 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric]) |
869 done |
866 done |
870 |
867 |
871 lemma approx_SReal_mult_cancel_iff1 [simp]: |
868 lemma approx_SReal_mult_cancel_iff1 [simp]: |
872 "[| (a::hypreal) \<in> \<real>; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)" |
869 "[| (a::hypreal) \<in> \<real>; a \<noteq> 0|] ==> (a* w \<approx> a*z) = (w \<approx> z)" |
873 by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD] |
870 by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD] |
874 intro: approx_SReal_mult_cancel) |
871 intro: approx_SReal_mult_cancel) |
875 |
872 |
876 lemma approx_le_bound: "[| (z::hypreal) \<le> f; f @= g; g \<le> z |] ==> f @= z" |
873 lemma approx_le_bound: "[| (z::hypreal) \<le> f; f \<approx> g; g \<le> z |] ==> f \<approx> z" |
877 apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto) |
874 apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto) |
878 apply (rule_tac x = "g+y-z" in bexI) |
875 apply (rule_tac x = "g+y-z" in bexI) |
879 apply (simp (no_asm)) |
876 apply (simp (no_asm)) |
880 apply (rule Infinitesimal_interval2) |
877 apply (rule Infinitesimal_interval2) |
881 apply (rule_tac [2] Infinitesimal_zero, auto) |
878 apply (rule_tac [2] Infinitesimal_zero, auto) |
1004 close to a unique real number (i.e a member of Reals) |
1001 close to a unique real number (i.e a member of Reals) |
1005 ------------------------------------------------------------------*) |
1002 ------------------------------------------------------------------*) |
1006 |
1003 |
1007 subsection\<open>Uniqueness: Two Infinitely Close Reals are Equal\<close> |
1004 subsection\<open>Uniqueness: Two Infinitely Close Reals are Equal\<close> |
1008 |
1005 |
1009 lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)" |
1006 lemma star_of_approx_iff [simp]: "(star_of x \<approx> star_of y) = (x = y)" |
1010 apply safe |
1007 apply safe |
1011 apply (simp add: approx_def) |
1008 apply (simp add: approx_def) |
1012 apply (simp only: star_of_diff [symmetric]) |
1009 apply (simp only: star_of_diff [symmetric]) |
1013 apply (simp only: star_of_Infinitesimal_iff_0) |
1010 apply (simp only: star_of_Infinitesimal_iff_0) |
1014 apply simp |
1011 apply simp |
1015 done |
1012 done |
1016 |
1013 |
1017 lemma SReal_approx_iff: |
1014 lemma SReal_approx_iff: |
1018 "[|(x::hypreal) \<in> \<real>; y \<in> \<real>|] ==> (x @= y) = (x = y)" |
1015 "[|(x::hypreal) \<in> \<real>; y \<in> \<real>|] ==> (x \<approx> y) = (x = y)" |
1019 apply auto |
1016 apply auto |
1020 apply (simp add: approx_def) |
1017 apply (simp add: approx_def) |
1021 apply (drule (1) Reals_diff) |
1018 apply (drule (1) Reals_diff) |
1022 apply (drule (1) SReal_Infinitesimal_zero) |
1019 apply (drule (1) SReal_Infinitesimal_zero) |
1023 apply simp |
1020 apply simp |
1024 done |
1021 done |
1025 |
1022 |
1026 lemma numeral_approx_iff [simp]: |
1023 lemma numeral_approx_iff [simp]: |
1027 "(numeral v @= (numeral w :: 'a::{numeral,real_normed_vector} star)) = |
1024 "(numeral v \<approx> (numeral w :: 'a::{numeral,real_normed_vector} star)) = |
1028 (numeral v = (numeral w :: 'a))" |
1025 (numeral v = (numeral w :: 'a))" |
1029 apply (unfold star_numeral_def) |
1026 apply (unfold star_numeral_def) |
1030 apply (rule star_of_approx_iff) |
1027 apply (rule star_of_approx_iff) |
1031 done |
1028 done |
1032 |
1029 |
1033 (*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*) |
1030 (*And also for 0 \<approx> #nn and 1 \<approx> #nn, #nn \<approx> 0 and #nn \<approx> 1.*) |
1034 lemma [simp]: |
1031 lemma [simp]: |
1035 "(numeral w @= (0::'a::{numeral,real_normed_vector} star)) = |
1032 "(numeral w \<approx> (0::'a::{numeral,real_normed_vector} star)) = |
1036 (numeral w = (0::'a))" |
1033 (numeral w = (0::'a))" |
1037 "((0::'a::{numeral,real_normed_vector} star) @= numeral w) = |
1034 "((0::'a::{numeral,real_normed_vector} star) \<approx> numeral w) = |
1038 (numeral w = (0::'a))" |
1035 (numeral w = (0::'a))" |
1039 "(numeral w @= (1::'b::{numeral,one,real_normed_vector} star)) = |
1036 "(numeral w \<approx> (1::'b::{numeral,one,real_normed_vector} star)) = |
1040 (numeral w = (1::'b))" |
1037 (numeral w = (1::'b))" |
1041 "((1::'b::{numeral,one,real_normed_vector} star) @= numeral w) = |
1038 "((1::'b::{numeral,one,real_normed_vector} star) \<approx> numeral w) = |
1042 (numeral w = (1::'b))" |
1039 (numeral w = (1::'b))" |
1043 "~ (0 @= (1::'c::{zero_neq_one,real_normed_vector} star))" |
1040 "~ (0 \<approx> (1::'c::{zero_neq_one,real_normed_vector} star))" |
1044 "~ (1 @= (0::'c::{zero_neq_one,real_normed_vector} star))" |
1041 "~ (1 \<approx> (0::'c::{zero_neq_one,real_normed_vector} star))" |
1045 apply (unfold star_numeral_def star_zero_def star_one_def) |
1042 apply (unfold star_numeral_def star_zero_def star_one_def) |
1046 apply (unfold star_of_approx_iff) |
1043 apply (unfold star_of_approx_iff) |
1047 by (auto intro: sym) |
1044 by (auto intro: sym) |
1048 |
1045 |
1049 lemma star_of_approx_numeral_iff [simp]: |
1046 lemma star_of_approx_numeral_iff [simp]: |
1050 "(star_of k @= numeral w) = (k = numeral w)" |
1047 "(star_of k \<approx> numeral w) = (k = numeral w)" |
1051 by (subst star_of_approx_iff [symmetric], auto) |
1048 by (subst star_of_approx_iff [symmetric], auto) |
1052 |
1049 |
1053 lemma star_of_approx_zero_iff [simp]: "(star_of k @= 0) = (k = 0)" |
1050 lemma star_of_approx_zero_iff [simp]: "(star_of k \<approx> 0) = (k = 0)" |
1054 by (simp_all add: star_of_approx_iff [symmetric]) |
1051 by (simp_all add: star_of_approx_iff [symmetric]) |
1055 |
1052 |
1056 lemma star_of_approx_one_iff [simp]: "(star_of k @= 1) = (k = 1)" |
1053 lemma star_of_approx_one_iff [simp]: "(star_of k \<approx> 1) = (k = 1)" |
1057 by (simp_all add: star_of_approx_iff [symmetric]) |
1054 by (simp_all add: star_of_approx_iff [symmetric]) |
1058 |
1055 |
1059 lemma approx_unique_real: |
1056 lemma approx_unique_real: |
1060 "[| (r::hypreal) \<in> \<real>; s \<in> \<real>; r @= x; s @= x|] ==> r = s" |
1057 "[| (r::hypreal) \<in> \<real>; s \<in> \<real>; r \<approx> x; s \<approx> x|] ==> r = s" |
1061 by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2) |
1058 by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2) |
1062 |
1059 |
1063 |
1060 |
1064 subsection\<open>Existence of Unique Real Infinitely Close\<close> |
1061 subsection\<open>Existence of Unique Real Infinitely Close\<close> |
1065 |
1062 |
1568 apply (erule bex_Infinitesimal_iff [THEN iffD2, THEN bexE]) |
1565 apply (erule bex_Infinitesimal_iff [THEN iffD2, THEN bexE]) |
1569 apply (cut_tac x = "-x" and e = xa in less_Infinitesimal_less, auto) |
1566 apply (cut_tac x = "-x" and e = xa in less_Infinitesimal_less, auto) |
1570 done |
1567 done |
1571 |
1568 |
1572 lemma lemma_approx_gt_zero: |
1569 lemma lemma_approx_gt_zero: |
1573 "[|0 < (x::hypreal); x \<notin> Infinitesimal; x @= y|] ==> 0 < y" |
1570 "[|0 < (x::hypreal); x \<notin> Infinitesimal; x \<approx> y|] ==> 0 < y" |
1574 by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad) |
1571 by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad) |
1575 |
1572 |
1576 lemma lemma_approx_less_zero: |
1573 lemma lemma_approx_less_zero: |
1577 "[|(x::hypreal) < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0" |
1574 "[|(x::hypreal) < 0; x \<notin> Infinitesimal; x \<approx> y|] ==> y < 0" |
1578 by (blast dest: Ball_mem_monad_less_zero approx_subset_monad) |
1575 by (blast dest: Ball_mem_monad_less_zero approx_subset_monad) |
1579 |
1576 |
1580 theorem approx_hrabs: "(x::hypreal) @= y ==> \<bar>x\<bar> @= \<bar>y\<bar>" |
1577 theorem approx_hrabs: "(x::hypreal) \<approx> y ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>" |
1581 by (drule approx_hnorm, simp) |
1578 by (drule approx_hnorm, simp) |
1582 |
1579 |
1583 lemma approx_hrabs_zero_cancel: "\<bar>x::hypreal\<bar> @= 0 ==> x @= 0" |
1580 lemma approx_hrabs_zero_cancel: "\<bar>x::hypreal\<bar> \<approx> 0 ==> x \<approx> 0" |
1584 apply (cut_tac x = x in hrabs_disj) |
1581 apply (cut_tac x = x in hrabs_disj) |
1585 apply (auto dest: approx_minus) |
1582 apply (auto dest: approx_minus) |
1586 done |
1583 done |
1587 |
1584 |
1588 lemma approx_hrabs_add_Infinitesimal: |
1585 lemma approx_hrabs_add_Infinitesimal: |
1589 "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> @= \<bar>x + e\<bar>" |
1586 "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> \<approx> \<bar>x + e\<bar>" |
1590 by (fast intro: approx_hrabs Infinitesimal_add_approx_self) |
1587 by (fast intro: approx_hrabs Infinitesimal_add_approx_self) |
1591 |
1588 |
1592 lemma approx_hrabs_add_minus_Infinitesimal: |
1589 lemma approx_hrabs_add_minus_Infinitesimal: |
1593 "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> @= \<bar>x + -e\<bar>" |
1590 "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> \<approx> \<bar>x + -e\<bar>" |
1594 by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self) |
1591 by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self) |
1595 |
1592 |
1596 lemma hrabs_add_Infinitesimal_cancel: |
1593 lemma hrabs_add_Infinitesimal_cancel: |
1597 "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal; |
1594 "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal; |
1598 \<bar>x + e\<bar> = \<bar>y + e'\<bar>|] ==> \<bar>x\<bar> @= \<bar>y\<bar>" |
1595 \<bar>x + e\<bar> = \<bar>y + e'\<bar>|] ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>" |
1599 apply (drule_tac x = x in approx_hrabs_add_Infinitesimal) |
1596 apply (drule_tac x = x in approx_hrabs_add_Infinitesimal) |
1600 apply (drule_tac x = y in approx_hrabs_add_Infinitesimal) |
1597 apply (drule_tac x = y in approx_hrabs_add_Infinitesimal) |
1601 apply (auto intro: approx_trans2) |
1598 apply (auto intro: approx_trans2) |
1602 done |
1599 done |
1603 |
1600 |
1604 lemma hrabs_add_minus_Infinitesimal_cancel: |
1601 lemma hrabs_add_minus_Infinitesimal_cancel: |
1605 "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal; |
1602 "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal; |
1606 \<bar>x + -e\<bar> = \<bar>y + -e'\<bar>|] ==> \<bar>x\<bar> @= \<bar>y\<bar>" |
1603 \<bar>x + -e\<bar> = \<bar>y + -e'\<bar>|] ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>" |
1607 apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal) |
1604 apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal) |
1608 apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal) |
1605 apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal) |
1609 apply (auto intro: approx_trans2) |
1606 apply (auto intro: approx_trans2) |
1610 done |
1607 done |
1611 |
1608 |