774 apply (erule approx_sym) |
774 apply (erule approx_sym) |
775 done |
775 done |
776 |
776 |
777 lemma approx_add_left_cancel: "d + b @= d + c ==> b @= c" |
777 lemma approx_add_left_cancel: "d + b @= d + c ==> b @= c" |
778 apply (drule approx_minus_iff [THEN iffD1]) |
778 apply (drule approx_minus_iff [THEN iffD1]) |
779 apply (simp add: approx_minus_iff [symmetric] add_ac) |
779 apply (simp add: approx_minus_iff [symmetric] ac_simps) |
780 done |
780 done |
781 |
781 |
782 lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c" |
782 lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c" |
783 apply (rule approx_add_left_cancel) |
783 apply (rule approx_add_left_cancel) |
784 apply (simp add: add.commute) |
784 apply (simp add: add.commute) |
785 done |
785 done |
786 |
786 |
787 lemma approx_add_mono1: "b @= c ==> d + b @= d + c" |
787 lemma approx_add_mono1: "b @= c ==> d + b @= d + c" |
788 apply (rule approx_minus_iff [THEN iffD2]) |
788 apply (rule approx_minus_iff [THEN iffD2]) |
789 apply (simp add: approx_minus_iff [symmetric] add_ac) |
789 apply (simp add: approx_minus_iff [symmetric] ac_simps) |
790 done |
790 done |
791 |
791 |
792 lemma approx_add_mono2: "b @= c ==> b + a @= c + a" |
792 lemma approx_add_mono2: "b @= c ==> b + a @= c + a" |
793 by (simp add: add.commute approx_add_mono1) |
793 by (simp add: add.commute approx_add_mono1) |
794 |
794 |
1712 done |
1712 done |
1713 |
1713 |
1714 lemma Infinitesimal_sum_square_cancel2 [simp]: |
1714 lemma Infinitesimal_sum_square_cancel2 [simp]: |
1715 "(y::hypreal)*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
1715 "(y::hypreal)*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
1716 apply (rule Infinitesimal_sum_square_cancel) |
1716 apply (rule Infinitesimal_sum_square_cancel) |
1717 apply (simp add: add_ac) |
1717 apply (simp add: ac_simps) |
1718 done |
1718 done |
1719 |
1719 |
1720 lemma HFinite_sum_square_cancel2 [simp]: |
1720 lemma HFinite_sum_square_cancel2 [simp]: |
1721 "(y::hypreal)*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite" |
1721 "(y::hypreal)*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite" |
1722 apply (rule HFinite_sum_square_cancel) |
1722 apply (rule HFinite_sum_square_cancel) |
1723 apply (simp add: add_ac) |
1723 apply (simp add: ac_simps) |
1724 done |
1724 done |
1725 |
1725 |
1726 lemma Infinitesimal_sum_square_cancel3 [simp]: |
1726 lemma Infinitesimal_sum_square_cancel3 [simp]: |
1727 "(z::hypreal)*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
1727 "(z::hypreal)*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
1728 apply (rule Infinitesimal_sum_square_cancel) |
1728 apply (rule Infinitesimal_sum_square_cancel) |
1729 apply (simp add: add_ac) |
1729 apply (simp add: ac_simps) |
1730 done |
1730 done |
1731 |
1731 |
1732 lemma HFinite_sum_square_cancel3 [simp]: |
1732 lemma HFinite_sum_square_cancel3 [simp]: |
1733 "(z::hypreal)*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite" |
1733 "(z::hypreal)*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite" |
1734 apply (rule HFinite_sum_square_cancel) |
1734 apply (rule HFinite_sum_square_cancel) |
1735 apply (simp add: add_ac) |
1735 apply (simp add: ac_simps) |
1736 done |
1736 done |
1737 |
1737 |
1738 lemma monad_hrabs_less: |
1738 lemma monad_hrabs_less: |
1739 "[| y \<in> monad x; 0 < hypreal_of_real e |] |
1739 "[| y \<in> monad x; 0 < hypreal_of_real e |] |
1740 ==> abs (y - x) < hypreal_of_real e" |
1740 ==> abs (y - x) < hypreal_of_real e" |