src/HOL/Hyperreal/NSA.thy
 changeset 20563 44eda2314aab parent 20562 c2f672be8522 child 20584 60b1d52a455d
equal inserted replaced
20562:c2f672be8522 20563:44eda2314aab
`    26   "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"`
`    26   "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"`
`    27 `
`    27 `
`    28   approx :: "['a::real_normed_vector star, 'a star] => bool"`
`    28   approx :: "['a::real_normed_vector star, 'a star] => bool"`
`    29     (infixl "@=" 50)`
`    29     (infixl "@=" 50)`
`    30     --{*the `infinitely close' relation*}`
`    30     --{*the `infinitely close' relation*}`
`    31   "(x @= y) = ((x + -y) \<in> Infinitesimal)"`
`    31   "(x @= y) = ((x - y) \<in> Infinitesimal)"`
`    32 `
`    32 `
`    33   st        :: "hypreal => hypreal"`
`    33   st        :: "hypreal => hypreal"`
`    34     --{*the standard part of a hyperreal*}`
`    34     --{*the standard part of a hyperreal*}`
`    35   "st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"`
`    35   "st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"`
`    36 `
`    36 `
`   146 `
`   146 `
`   147 lemma SReal_add [simp]:`
`   147 lemma SReal_add [simp]:`
`   148      "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"`
`   148      "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"`
`   149 apply (auto simp add: SReal_def)`
`   149 apply (auto simp add: SReal_def)`
`   150 apply (rule_tac x = "r + ra" in exI, simp)`
`   150 apply (rule_tac x = "r + ra" in exI, simp)`
`       `
`   151 done`
`       `
`   152 `
`       `
`   153 lemma SReal_diff [simp]:`
`       `
`   154      "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x - y \<in> Reals"`
`       `
`   155 apply (auto simp add: SReal_def)`
`       `
`   156 apply (rule_tac x = "r - ra" in exI, simp)`
`   151 done`
`   157 done`
`   152 `
`   158 `
`   153 lemma SReal_mult: "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x * y \<in> Reals"`
`   159 lemma SReal_mult: "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x * y \<in> Reals"`
`   154 apply (simp add: SReal_def, safe)`
`   160 apply (simp add: SReal_def, safe)`
`   155 apply (rule_tac x = "r * ra" in exI)`
`   161 apply (rule_tac x = "r * ra" in exI)`
`   605 subsection{*The Infinitely Close Relation*}`
`   611 subsection{*The Infinitely Close Relation*}`
`   606 `
`   612 `
`   607 lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)"`
`   613 lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)"`
`   608 by (simp add: Infinitesimal_def approx_def)`
`   614 by (simp add: Infinitesimal_def approx_def)`
`   609 `
`   615 `
`   610 lemma approx_minus_iff: " (x @= y) = (x + -y @= 0)"`
`   616 lemma approx_minus_iff: " (x @= y) = (x - y @= 0)"`
`   611 by (simp add: approx_def)`
`   617 by (simp add: approx_def)`
`   612 `
`   618 `
`   613 lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)"`
`   619 lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)"`
`   614 by (simp add: approx_def add_commute)`
`   620 by (simp add: approx_def diff_minus add_commute)`
`   615 `
`   621 `
`   616 lemma approx_refl [iff]: "x @= x"`
`   622 lemma approx_refl [iff]: "x @= x"`
`   617 by (simp add: approx_def Infinitesimal_def)`
`   623 by (simp add: approx_def Infinitesimal_def)`
`   618 `
`   624 `
`   619 lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y"`
`   625 lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y"`
`   620 by (simp add: add_commute)`
`   626 by (simp add: add_commute)`
`   621 `
`   627 `
`   622 lemma approx_sym: "x @= y ==> y @= x"`
`   628 lemma approx_sym: "x @= y ==> y @= x"`
`   623 apply (simp add: approx_def)`
`   629 apply (simp add: approx_def)`
`   624 apply (rule hypreal_minus_distrib1 [THEN subst])`
`   630 apply (drule Infinitesimal_minus_iff [THEN iffD2])`
`   625 apply (erule Infinitesimal_minus_iff [THEN iffD2])`
`   631 apply simp`
`   626 done`
`   632 done`
`   627 `
`   633 `
`   628 lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z"`
`   634 lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z"`
`   629 apply (simp add: approx_def)`
`   635 apply (simp add: approx_def)`
`   630 apply (drule Infinitesimal_add, assumption, auto)`
`   636 apply (drule (1) Infinitesimal_add)`
`       `
`   637 apply (simp add: diff_def)`
`   631 done`
`   638 done`
`   632 `
`   639 `
`   633 lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s"`
`   640 lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s"`
`   634 by (blast intro: approx_sym approx_trans)`
`   641 by (blast intro: approx_sym approx_trans)`
`   635 `
`   642 `
`   678 `
`   685 `
`   679 Addsimprocs [approx_reorient_simproc];`
`   686 Addsimprocs [approx_reorient_simproc];`
`   680 *}`
`   687 *}`
`   681 `
`   688 `
`   682 lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)"`
`   689 lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)"`
`   683 by (auto simp add: diff_def approx_minus_iff [symmetric] mem_infmal_iff)`
`   690 by (simp add: approx_minus_iff [symmetric] mem_infmal_iff)`
`   684 `
`   691 `
`   685 lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))"`
`   692 lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))"`
`   686 apply (simp add: monad_def)`
`   693 apply (simp add: monad_def)`
`   687 apply (auto dest: approx_sym elim!: approx_trans equalityCE)`
`   694 apply (auto dest: approx_sym elim!: approx_trans equalityCE)`
`   688 done`
`   695 done`
`   693 apply (blast intro: approx_trans approx_sym)`
`   700 apply (blast intro: approx_trans approx_sym)`
`   694 done`
`   701 done`
`   695 `
`   702 `
`   696 lemma approx_add: "[| a @= b; c @= d |] ==> a+c @= b+d"`
`   703 lemma approx_add: "[| a @= b; c @= d |] ==> a+c @= b+d"`
`   697 proof (unfold approx_def)`
`   704 proof (unfold approx_def)`
`   698   assume inf: "a + - b \<in> Infinitesimal" "c + - d \<in> Infinitesimal"`
`   705   assume inf: "a - b \<in> Infinitesimal" "c - d \<in> Infinitesimal"`
`   699   have "a + c + - (b + d) = (a + - b) + (c + - d)" by simp`
`   706   have "a + c - (b + d) = (a - b) + (c - d)" by simp`
`   700   also have "... \<in> Infinitesimal" using inf by (rule Infinitesimal_add)`
`   707   also have "... \<in> Infinitesimal" using inf by (rule Infinitesimal_add)`
`   701   finally show "a + c + - (b + d) \<in> Infinitesimal" .`
`   708   finally show "a + c - (b + d) \<in> Infinitesimal" .`
`   702 qed`
`   709 qed`
`   703 `
`   710 `
`   704 lemma approx_minus: "a @= b ==> -a @= -b"`
`   711 lemma approx_minus: "a @= b ==> -a @= -b"`
`   705 apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])`
`   712 apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])`
`   706 apply (drule approx_minus_iff [THEN iffD1])`
`   713 apply (drule approx_minus_iff [THEN iffD1])`
`   707 apply (simp (no_asm) add: add_commute)`
`   714 apply (simp add: add_commute diff_def)`
`   708 done`
`   715 done`
`   709 `
`   716 `
`   710 lemma approx_minus2: "-a @= -b ==> a @= b"`
`   717 lemma approx_minus2: "-a @= -b ==> a @= b"`
`   711 by (auto dest: approx_minus)`
`   718 by (auto dest: approx_minus)`
`   712 `
`   719 `
`   717 by (blast intro!: approx_add approx_minus)`
`   724 by (blast intro!: approx_add approx_minus)`
`   718 `
`   725 `
`   719 lemma approx_mult1:`
`   726 lemma approx_mult1:`
`   720   fixes a b c :: "'a::real_normed_algebra star"`
`   727   fixes a b c :: "'a::real_normed_algebra star"`
`   721   shows "[| a @= b; c: HFinite|] ==> a*c @= b*c"`
`   728   shows "[| a @= b; c: HFinite|] ==> a*c @= b*c"`
`   722 by (simp add: approx_def Infinitesimal_HFinite_mult minus_mult_left `
`   729 by (simp add: approx_def Infinitesimal_HFinite_mult`
`   723               left_distrib [symmetric] `
`   730               left_diff_distrib [symmetric])`
`   724          del: minus_mult_left [symmetric])`
`       `
`   725 `
`   731 `
`   726 lemma approx_mult2:`
`   732 lemma approx_mult2:`
`   727   fixes a b c :: "'a::real_normed_algebra star"`
`   733   fixes a b c :: "'a::real_normed_algebra star"`
`   728   shows "[|a @= b; c: HFinite|] ==> c*a @= c*b"`
`   734   shows "[|a @= b; c: HFinite|] ==> c*a @= c*b"`
`   729 by (simp add: approx_def Infinitesimal_HFinite_mult2 minus_mult_right `
`   735 by (simp add: approx_def Infinitesimal_HFinite_mult2`
`   730               right_distrib [symmetric] `
`   736               right_diff_distrib [symmetric])`
`   731          del: minus_mult_right [symmetric])`
`       `
`   732 `
`   737 `
`   733 lemma approx_mult_subst:`
`   738 lemma approx_mult_subst:`
`   734   fixes u v x y :: "'a::real_normed_algebra star"`
`   739   fixes u v x y :: "'a::real_normed_algebra star"`
`   735   shows "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"`
`   740   shows "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"`
`   736 by (blast intro: approx_mult2 approx_trans)`
`   741 by (blast intro: approx_mult2 approx_trans)`
`   754 `
`   759 `
`   755 lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x @= x"`
`   760 lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x @= x"`
`   756 by (blast intro: Infinitesimal_minus_iff [THEN iffD2] `
`   761 by (blast intro: Infinitesimal_minus_iff [THEN iffD2] `
`   757                     mem_infmal_iff [THEN iffD1] approx_trans2)`
`   762                     mem_infmal_iff [THEN iffD1] approx_trans2)`
`   758 `
`   763 `
`   759 lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x + -z = y) = (x @= z)"`
`   764 lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x - z = y) = (x @= z)"`
`   760 by (simp add: approx_def)`
`   765 by (simp add: approx_def)`
`   761 `
`   766 `
`   762 lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x @= z)"`
`   767 lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x @= z)"`
`   763 by (force simp add: bex_Infinitesimal_iff [symmetric])`
`   768 by (force simp add: bex_Infinitesimal_iff [symmetric])`
`   764 `
`   769 `
`   995 subsection{* Uniqueness: Two Infinitely Close Reals are Equal*}`
`  1000 subsection{* Uniqueness: Two Infinitely Close Reals are Equal*}`
`   996 `
`  1001 `
`   997 lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)"`
`  1002 lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)"`
`   998 apply safe`
`  1003 apply safe`
`   999 apply (simp add: approx_def)`
`  1004 apply (simp add: approx_def)`
`  1000 apply (simp only: star_of_minus [symmetric] star_of_add [symmetric])`
`  1005 apply (simp only: star_of_diff [symmetric])`
`  1001 apply (simp only: star_of_Infinitesimal_iff_0)`
`  1006 apply (simp only: star_of_Infinitesimal_iff_0)`
`  1002 apply (simp only: diff_minus [symmetric] right_minus_eq)`
`  1007 apply simp`
`  1003 done`
`  1008 done`
`  1004 `
`  1009 `
`  1005 lemma SReal_approx_iff:`
`  1010 lemma SReal_approx_iff:`
`  1006   "[|(x::hypreal) \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"`
`  1011   "[|(x::hypreal) \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"`
`  1007 apply auto`
`  1012 apply auto`
`  1008 apply (simp add: approx_def)`
`  1013 apply (simp add: approx_def)`
`  1009 apply (drule_tac x = y in SReal_minus)`
`  1014 apply (drule (1) SReal_diff)`
`  1010 apply (drule SReal_add, assumption)`
`  1015 apply (drule (1) SReal_Infinitesimal_zero)`
`  1011 apply (drule SReal_Infinitesimal_zero, assumption)`
`  1016 apply simp`
`  1012 apply (drule sym)`
`       `
`  1013 apply (simp add: hypreal_eq_minus_iff [symmetric])`
`       `
`  1014 done`
`  1017 done`
`  1015 `
`  1018 `
`  1016 lemma number_of_approx_iff [simp]:`
`  1019 lemma number_of_approx_iff [simp]:`
`  1017      "(number_of v @= (number_of w :: 'a::{number,real_normed_vector} star)) =`
`  1020      "(number_of v @= (number_of w :: 'a::{number,real_normed_vector} star)) =`
`  1018       (number_of v = (number_of w :: 'a))"`
`  1021       (number_of v = (number_of w :: 'a))"`
`  1199 `
`  1202 `
`  1200 lemma lemma_st_part_major:`
`  1203 lemma lemma_st_part_major:`
`  1201      "[| (x::hypreal) \<in> HFinite;`
`  1204      "[| (x::hypreal) \<in> HFinite;`
`  1202          isLub Reals {s. s \<in> Reals & s < x} t;`
`  1205          isLub Reals {s. s \<in> Reals & s < x} t;`
`  1203          r \<in> Reals; 0 < r |]`
`  1206          r \<in> Reals; 0 < r |]`
`  1204       ==> abs (x + -t) < r"`
`  1207       ==> abs (x - t) < r"`
`  1205 apply (frule lemma_st_part1a)`
`  1208 apply (frule lemma_st_part1a)`
`  1206 apply (frule_tac [4] lemma_st_part2a, auto)`
`  1209 apply (frule_tac [4] lemma_st_part2a, auto)`
`  1207 apply (drule order_le_imp_less_or_eq)+`
`  1210 apply (drule order_le_imp_less_or_eq)+`
`  1208 apply (auto dest: lemma_st_part_not_eq1 lemma_st_part_not_eq2 simp add: abs_less_iff)`
`  1211 apply (auto dest: lemma_st_part_not_eq1 lemma_st_part_not_eq2 simp add: abs_less_iff)`
`  1209 done`
`  1212 done`
`  1210 `
`  1213 `
`  1211 lemma lemma_st_part_major2:`
`  1214 lemma lemma_st_part_major2:`
`  1212      "[| (x::hypreal) \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t |]`
`  1215      "[| (x::hypreal) \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t |]`
`  1213       ==> \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"`
`  1216       ==> \<forall>r \<in> Reals. 0 < r --> abs (x - t) < r"`
`  1214 by (blast dest!: lemma_st_part_major)`
`  1217 by (blast dest!: lemma_st_part_major)`
`  1215 `
`  1218 `
`  1216 `
`  1219 `
`  1217 text{*Existence of real and Standard Part Theorem*}`
`  1220 text{*Existence of real and Standard Part Theorem*}`
`  1218 lemma lemma_st_part_Ex:`
`  1221 lemma lemma_st_part_Ex:`
`  1219      "(x::hypreal) \<in> HFinite`
`  1222      "(x::hypreal) \<in> HFinite`
`  1220        ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"`
`  1223        ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x - t) < r"`
`  1221 apply (frule lemma_st_part_lub, safe)`
`  1224 apply (frule lemma_st_part_lub, safe)`
`  1222 apply (frule isLubD1a)`
`  1225 apply (frule isLubD1a)`
`  1223 apply (blast dest: lemma_st_part_major2)`
`  1226 apply (blast dest: lemma_st_part_major2)`
`  1224 done`
`  1227 done`
`  1225 `
`  1228 `
`  1336 `
`  1339 `
`  1337 lemma inverse_add_Infinitesimal_approx_Infinitesimal:`
`  1340 lemma inverse_add_Infinitesimal_approx_Infinitesimal:`
`  1338   fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"`
`  1341   fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"`
`  1339   shows`
`  1342   shows`
`  1340      "[| x \<in> HFinite - Infinitesimal;`
`  1343      "[| x \<in> HFinite - Infinitesimal;`
`  1341          h \<in> Infinitesimal |] ==> inverse(x + h) + -inverse x @= h"`
`  1344          h \<in> Infinitesimal |] ==> inverse(x + h) - inverse x @= h"`
`  1342 apply (rule approx_trans2)`
`  1345 apply (rule approx_trans2)`
`  1343 apply (auto intro: inverse_add_Infinitesimal_approx `
`  1346 apply (auto intro: inverse_add_Infinitesimal_approx `
`  1344             simp add: mem_infmal_iff approx_minus_iff [symmetric])`
`  1347             simp add: mem_infmal_iff approx_minus_iff [symmetric])`
`  1345 done`
`  1348 done`
`  1346 `
`  1349 `
`  1696 apply (simp add: add_ac)`
`  1699 apply (simp add: add_ac)`
`  1697 done`
`  1700 done`
`  1698 `
`  1701 `
`  1699 lemma monad_hrabs_less:`
`  1702 lemma monad_hrabs_less:`
`  1700      "[| y \<in> monad x; 0 < hypreal_of_real e |]`
`  1703      "[| y \<in> monad x; 0 < hypreal_of_real e |]`
`  1701       ==> abs (y + -x) < hypreal_of_real e"`
`  1704       ==> abs (y - x) < hypreal_of_real e"`
`  1702 apply (drule mem_monad_approx [THEN approx_sym])`
`  1705 apply (drule mem_monad_approx [THEN approx_sym])`
`  1703 apply (drule bex_Infinitesimal_iff [THEN iffD2])`
`  1706 apply (drule bex_Infinitesimal_iff [THEN iffD2])`
`  1704 apply (auto dest!: InfinitesimalD)`
`  1707 apply (auto dest!: InfinitesimalD)`
`  1705 done`
`  1708 done`
`  1706 `
`  1709 `
`  2229 `
`  2232 `
`  2230 (*-----------------------------------------------------`
`  2233 (*-----------------------------------------------------`
`  2231     |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal`
`  2234     |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal`
`  2232  -----------------------------------------------------*)`
`  2235  -----------------------------------------------------*)`
`  2233 lemma real_seq_to_hypreal_Infinitesimal:`
`  2236 lemma real_seq_to_hypreal_Infinitesimal:`
`  2234      "\<forall>n. norm(X n + -x) < inverse(real(Suc n))`
`  2237      "\<forall>n. norm(X n - x) < inverse(real(Suc n))`
`  2235      ==> star_n X + -star_of x \<in> Infinitesimal"`
`  2238      ==> star_n X - star_of x \<in> Infinitesimal"`
`  2236 apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: star_n_minus star_of_def star_n_add Infinitesimal_FreeUltrafilterNat_iff star_n_inverse)`
`  2239 apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse)`
`  2237 done`
`  2240 done`
`  2238 `
`  2241 `
`  2239 lemma real_seq_to_hypreal_approx:`
`  2242 lemma real_seq_to_hypreal_approx:`
`  2240      "\<forall>n. norm(X n + -x) < inverse(real(Suc n))`
`  2243      "\<forall>n. norm(X n - x) < inverse(real(Suc n))`
`  2241       ==> star_n X @= star_of x"`
`  2244       ==> star_n X @= star_of x"`
`  2242 apply (subst approx_minus_iff)`
`  2245 apply (subst approx_minus_iff)`
`  2243 apply (rule mem_infmal_iff [THEN subst])`
`  2246 apply (rule mem_infmal_iff [THEN subst])`
`  2244 apply (erule real_seq_to_hypreal_Infinitesimal)`
`  2247 apply (erule real_seq_to_hypreal_Infinitesimal)`
`  2245 done`
`  2248 done`
`  2246 `
`  2249 `
`  2247 lemma real_seq_to_hypreal_approx2:`
`  2250 lemma real_seq_to_hypreal_approx2:`
`  2248      "\<forall>n. norm(x + -X n) < inverse(real(Suc n))`
`  2251      "\<forall>n. norm(x - X n) < inverse(real(Suc n))`
`  2249                ==> star_n X @= star_of x"`
`  2252                ==> star_n X @= star_of x"`
`  2250 apply (rule real_seq_to_hypreal_approx)`
`  2253 apply (rule real_seq_to_hypreal_approx)`
`  2251 apply (subst norm_minus_cancel [symmetric])`
`  2254 apply (subst norm_minus_cancel [symmetric])`
`  2252 apply (simp del: norm_minus_cancel)`
`  2255 apply (simp del: norm_minus_cancel)`
`  2254 done`
`  2256 done`
`  2255 `
`  2257 `
`  2256 lemma real_seq_to_hypreal_Infinitesimal2:`
`  2258 lemma real_seq_to_hypreal_Infinitesimal2:`
`  2257      "\<forall>n. norm(X n + -Y n) < inverse(real(Suc n))`
`  2259      "\<forall>n. norm(X n - Y n) < inverse(real(Suc n))`
`  2258       ==> star_n X + -star_n Y \<in> Infinitesimal"`
`  2260       ==> star_n X - star_n Y \<in> Infinitesimal"`
`  2259 by (auto intro!: bexI`
`  2261 by (auto intro!: bexI`
`  2260 	 dest: FreeUltrafilterNat_inverse_real_of_posnat `
`  2262 	 dest: FreeUltrafilterNat_inverse_real_of_posnat `
`  2261 	       FreeUltrafilterNat_all FreeUltrafilterNat_Int`
`  2263 	       FreeUltrafilterNat_all FreeUltrafilterNat_Int`
`  2262 	 intro: order_less_trans FreeUltrafilterNat_subset `
`  2264 	 intro: order_less_trans FreeUltrafilterNat_subset `
`  2263 	 simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_minus `
`  2265 	 simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_diff `
`  2264                    star_n_add star_n_inverse)`
`  2266                    star_n_inverse)`
`  2265 `
`  2267 `
`  2266 end`
`  2268 end`