diff -r 3f12de2e2e6e -r bc1c75855f3d src/HOL/Hyperreal/NSA.thy --- a/src/HOL/Hyperreal/NSA.thy Fri Sep 09 17:47:37 2005 +0200 +++ b/src/HOL/Hyperreal/NSA.thy Fri Sep 09 19:34:22 2005 +0200 @@ -8,7 +8,7 @@ header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} theory NSA -imports HyperArith RComplete +imports HyperArith "../Real/RComplete" begin constdefs @@ -66,16 +66,15 @@ lemma SReal_inverse: "(x::hypreal) \ Reals ==> inverse x \ Reals" apply (simp add: SReal_def) -apply (blast intro: hypreal_of_real_inverse [symmetric]) +apply (blast intro: star_of_inverse [symmetric]) done lemma SReal_divide: "[| (x::hypreal) \ Reals; y \ Reals |] ==> x/y \ Reals" -apply (simp (no_asm_simp) add: SReal_mult SReal_inverse hypreal_divide_def) -done +by (simp (no_asm_simp) add: SReal_mult SReal_inverse divide_inverse) lemma SReal_minus: "(x::hypreal) \ Reals ==> -x \ Reals" apply (simp add: SReal_def) -apply (blast intro: hypreal_of_real_minus [symmetric]) +apply (blast intro: star_of_minus [symmetric]) done lemma SReal_minus_iff [simp]: "(-x \ Reals) = ((x::hypreal) \ Reals)" @@ -91,15 +90,16 @@ done lemma SReal_hrabs: "(x::hypreal) \ Reals ==> abs x \ Reals" -apply (simp add: SReal_def) -apply (auto simp add: hypreal_of_real_hrabs) +apply (auto simp add: SReal_def) +apply (rule_tac x="abs r" in exI) +apply simp done lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \ Reals" by (simp add: SReal_def) lemma SReal_number_of [simp]: "(number_of w ::hypreal) \ Reals" -apply (simp only: hypreal_number_of [symmetric]) +apply (simp only: star_of_number_of [symmetric]) apply (rule SReal_hypreal_of_real) done @@ -116,7 +116,7 @@ done lemma SReal_divide_number_of: "r \ Reals ==> r/(number_of w::hypreal) \ Reals" -apply (unfold hypreal_divide_def) +apply (simp only: divide_inverse) apply (blast intro!: SReal_number_of SReal_mult SReal_inverse) done @@ -247,8 +247,8 @@ lemma SReal_subset_HFinite: "Reals \ HFinite" apply (auto simp add: SReal_def HFinite_def) apply (rule_tac x = "1 + abs (hypreal_of_real r) " in exI) -apply (auto simp add: hypreal_of_real_hrabs) -apply (rule_tac x = "1 + abs r" in exI, simp) +apply (rule conjI, rule_tac x = "1 + abs r" in exI) +apply simp_all done lemma HFinite_hypreal_of_real [simp]: "hypreal_of_real x \ HFinite" @@ -278,7 +278,7 @@ lemma HFinite_bounded: "[|x \ HFinite; y \ x; 0 \ y |] ==> y \ HFinite" apply (case_tac "x \ 0") apply (drule_tac y = x in order_trans) -apply (drule_tac [2] hypreal_le_anti_sym) +apply (drule_tac [2] order_antisym) apply (auto simp add: linorder_not_le) apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def) done @@ -309,7 +309,7 @@ lemma Infinitesimal_diff: "[| x \ Infinitesimal; y \ Infinitesimal |] ==> x-y \ Infinitesimal" -by (simp add: hypreal_diff_def Infinitesimal_add) +by (simp add: diff_def Infinitesimal_add) lemma Infinitesimal_mult: "[| x \ Infinitesimal; y \ Infinitesimal |] ==> (x * y) \ Infinitesimal" @@ -331,7 +331,7 @@ lemma Infinitesimal_HFinite_mult2: "[| x \ Infinitesimal; y \ HFinite |] ==> (y * x) \ Infinitesimal" -by (auto dest: Infinitesimal_HFinite_mult simp add: hypreal_mult_commute) +by (auto dest: Infinitesimal_HFinite_mult simp add: mult_commute) (*** rather long proof ***) lemma HInfinite_inverse_Infinitesimal: @@ -359,11 +359,11 @@ lemma HInfinite_add_ge_zero: "[|x \ HInfinite; 0 \ y; 0 \ x|] ==> (x + y): HInfinite" by (auto intro!: hypreal_add_zero_less_le_mono - simp add: abs_if hypreal_add_commute hypreal_le_add_order HInfinite_def) + simp add: abs_if add_commute add_nonneg_nonneg HInfinite_def) lemma HInfinite_add_ge_zero2: "[|x \ HInfinite; 0 \ y; 0 \ x|] ==> (y + x): HInfinite" -by (auto intro!: HInfinite_add_ge_zero simp add: hypreal_add_commute) +by (auto intro!: HInfinite_add_ge_zero simp add: add_commute) lemma HInfinite_add_gt_zero: "[|x \ HInfinite; 0 < y; 0 < x|] ==> (x + y): HInfinite" @@ -472,13 +472,13 @@ by (simp add: approx_def) lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)" -by (simp add: approx_def hypreal_add_commute) +by (simp add: approx_def add_commute) lemma approx_refl [iff]: "x @= x" by (simp add: approx_def Infinitesimal_def) lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y" -by (simp add: hypreal_add_commute) +by (simp add: add_commute) lemma approx_sym: "x @= y ==> y @= x" apply (simp add: approx_def) @@ -624,7 +624,7 @@ *} lemma Infinitesimal_approx_minus: "(x-y \ Infinitesimal) = (x @= y)" -by (auto simp add: hypreal_diff_def approx_minus_iff [symmetric] mem_infmal_iff) +by (auto simp add: diff_def approx_minus_iff [symmetric] mem_infmal_iff) lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))" apply (simp add: monad_def) @@ -648,7 +648,7 @@ lemma approx_minus: "a @= b ==> -a @= -b" apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym]) apply (drule approx_minus_iff [THEN iffD1]) -apply (simp (no_asm) add: hypreal_add_commute) +apply (simp (no_asm) add: add_commute) done lemma approx_minus2: "-a @= -b ==> a @= b" @@ -666,7 +666,7 @@ del: minus_mult_left [symmetric]) lemma approx_mult2: "[|a @= b; c: HFinite|] ==> c*a @= c*b" -by (simp add: approx_mult1 hypreal_mult_commute) +by (simp add: approx_mult1 mult_commute) lemma approx_mult_subst: "[|u @= v*x; x @= y; v \ HFinite|] ==> u @= v*y" by (blast intro: approx_mult2 approx_trans) @@ -694,17 +694,17 @@ lemma Infinitesimal_add_approx: "[| y \ Infinitesimal; x + y = z |] ==> x @= z" apply (rule bex_Infinitesimal_iff [THEN iffD1]) apply (drule Infinitesimal_minus_iff [THEN iffD2]) -apply (auto simp add: hypreal_add_assoc [symmetric]) +apply (auto simp add: add_assoc [symmetric]) done lemma Infinitesimal_add_approx_self: "y \ Infinitesimal ==> x @= x + y" apply (rule bex_Infinitesimal_iff [THEN iffD1]) apply (drule Infinitesimal_minus_iff [THEN iffD2]) -apply (auto simp add: hypreal_add_assoc [symmetric]) +apply (auto simp add: add_assoc [symmetric]) done lemma Infinitesimal_add_approx_self2: "y \ Infinitesimal ==> x @= y + x" -by (auto dest: Infinitesimal_add_approx_self simp add: hypreal_add_commute) +by (auto dest: Infinitesimal_add_approx_self simp add: add_commute) lemma Infinitesimal_add_minus_approx_self: "y \ Infinitesimal ==> x @= x + -y" by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2]) @@ -718,7 +718,7 @@ "[| y \ Infinitesimal; x @= z + y|] ==> x @= z" apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym]) apply (erule approx_trans3 [THEN approx_sym]) -apply (simp add: hypreal_add_commute) +apply (simp add: add_commute) apply (erule approx_sym) done @@ -729,7 +729,7 @@ lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c" apply (rule approx_add_left_cancel) -apply (simp add: hypreal_add_commute) +apply (simp add: add_commute) done lemma approx_add_mono1: "b @= c ==> d + b @= d + c" @@ -738,19 +738,19 @@ done lemma approx_add_mono2: "b @= c ==> b + a @= c + a" -by (simp add: hypreal_add_commute approx_add_mono1) +by (simp add: add_commute approx_add_mono1) lemma approx_add_left_iff [simp]: "(a + b @= a + c) = (b @= c)" by (fast elim: approx_add_left_cancel approx_add_mono1) lemma approx_add_right_iff [simp]: "(b + a @= c + a) = (b @= c)" -by (simp add: hypreal_add_commute) +by (simp add: add_commute) lemma approx_HFinite: "[| x \ HFinite; x @= y |] ==> y \ HFinite" apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe) apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]]) apply (drule HFinite_add) -apply (auto simp add: hypreal_add_assoc) +apply (auto simp add: add_assoc) done lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \ HFinite" @@ -773,7 +773,7 @@ lemma approx_SReal_mult_cancel_zero: "[| a \ Reals; a \ 0; a*x @= 0 |] ==> x @= 0" apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) -apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric]) +apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) done lemma approx_mult_SReal1: "[| a \ Reals; x @= 0 |] ==> x*a @= 0" @@ -789,7 +789,7 @@ lemma approx_SReal_mult_cancel: "[| a \ Reals; a \ 0; a* w @= a*z |] ==> w @= z" apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) -apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric]) +apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) done lemma approx_SReal_mult_cancel_iff1 [simp]: @@ -884,7 +884,7 @@ lemma Infinitesimal_ratio: "[| y \ 0; y \ Infinitesimal; x/y \ HFinite |] ==> x \ Infinitesimal" apply (drule Infinitesimal_HFinite_mult2, assumption) -apply (simp add: hypreal_divide_def hypreal_mult_assoc) +apply (simp add: divide_inverse mult_assoc) done lemma Infinitesimal_SReal_divide: @@ -952,7 +952,7 @@ "[| isLub R S x; isLub R S y |] ==> x = (y::hypreal)" apply (frule isLub_isUb) apply (frule_tac x = y in isLub_isUb) -apply (blast intro!: hypreal_le_anti_sym dest!: isLub_le_isUb) +apply (blast intro!: order_antisym dest!: isLub_le_isUb) done lemma lemma_st_part_ub: @@ -980,7 +980,7 @@ apply safe apply (drule_tac c = "-t" in add_left_mono) apply (drule_tac [2] c = t in add_left_mono) -apply (auto simp add: hypreal_add_assoc [symmetric]) +apply (auto simp add: add_assoc [symmetric]) done lemma lemma_st_part_le1: @@ -1011,7 +1011,7 @@ lemma lemma_minus_le_zero: "t \ t + -r ==> r \ (0::hypreal)" apply (drule_tac c = "-t" in add_left_mono) -apply (auto simp add: hypreal_add_assoc [symmetric]) +apply (auto simp add: add_assoc [symmetric]) done lemma lemma_st_part_le2: @@ -1179,7 +1179,7 @@ "x \ HFinite - Infinitesimal ==> inverse x \ HFinite - Infinitesimal" apply (auto intro: Infinitesimal_inverse_HFinite) apply (drule Infinitesimal_HFinite_mult2, assumption) -apply (simp add: not_Infinitesimal_not_zero hypreal_mult_inverse) +apply (simp add: not_Infinitesimal_not_zero right_inverse) done lemma approx_inverse: @@ -1191,7 +1191,7 @@ apply (drule HFinite_inverse2)+ apply (drule approx_mult2, assumption, auto) apply (drule_tac c = "inverse x" in approx_mult1, assumption) -apply (auto intro: approx_sym simp add: hypreal_mult_assoc) +apply (auto intro: approx_sym simp add: mult_assoc) done (*Used for NSLIM_inverse, NSLIMSEQ_inverse*) @@ -1206,7 +1206,7 @@ lemma inverse_add_Infinitesimal_approx2: "[| x \ HFinite - Infinitesimal; h \ Infinitesimal |] ==> inverse(h + x) @= inverse x" -apply (rule hypreal_add_commute [THEN subst]) +apply (rule add_commute [THEN subst]) apply (blast intro: inverse_add_Infinitesimal_approx) done @@ -1222,7 +1222,7 @@ apply (auto intro: Infinitesimal_mult) apply (rule ccontr, frule Infinitesimal_inverse_HFinite) apply (frule not_Infinitesimal_not_zero) -apply (auto dest: Infinitesimal_HFinite_mult simp add: hypreal_mult_assoc) +apply (auto dest: Infinitesimal_HFinite_mult simp add: mult_assoc) done declare Infinitesimal_square_iff [symmetric, simp] @@ -1239,7 +1239,7 @@ apply safe apply (frule HFinite_inverse, assumption) apply (drule not_Infinitesimal_not_zero) -apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric]) +apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) done lemma approx_HFinite_mult_cancel_iff1: @@ -1256,7 +1256,7 @@ lemma HInfinite_HFinite_add: "[| x \ HInfinite; y \ HFinite |] ==> x + y \ HInfinite" apply (rule_tac y = "-y" in HInfinite_HFinite_add_cancel) -apply (auto simp add: hypreal_add_assoc HFinite_minus_iff) +apply (auto simp add: add_assoc HFinite_minus_iff) done lemma HInfinite_ge_HInfinite: @@ -1276,13 +1276,13 @@ apply (frule HFinite_Infinitesimal_not_zero) apply (drule HFinite_not_Infinitesimal_inverse) apply (safe, drule HFinite_mult) -apply (auto simp add: hypreal_mult_assoc HFinite_HInfinite_iff) +apply (auto simp add: mult_assoc HFinite_HInfinite_iff) done lemma HInfinite_HFinite_not_Infinitesimal_mult2: "[| x \ HInfinite; y \ HFinite - Infinitesimal |] ==> y * x \ HInfinite" -by (auto simp add: hypreal_mult_commute HInfinite_HFinite_not_Infinitesimal_mult) +by (auto simp add: mult_commute HInfinite_HFinite_not_Infinitesimal_mult) lemma HInfinite_gt_SReal: "[| x \ HInfinite; 0 < x; y \ Reals |] ==> y < x" by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le) @@ -1443,13 +1443,14 @@ apply (drule_tac x = "hypreal_of_real r" in approx_hrabs_add_Infinitesimal) apply (drule approx_sym [THEN bex_Infinitesimal_iff2 [THEN iffD2]]) apply (auto intro!: Infinitesimal_add_hypreal_of_real_less + simp del: star_of_abs simp add: hypreal_of_real_hrabs) done lemma Infinitesimal_add_hrabs_hypreal_of_real_less2: "[| x \ Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |] ==> abs (x + hypreal_of_real r) < hypreal_of_real y" -apply (rule hypreal_add_commute [THEN subst]) +apply (rule add_commute [THEN subst]) apply (erule Infinitesimal_add_hrabs_hypreal_of_real_less, assumption) done @@ -1466,8 +1467,8 @@ "[| u \ Infinitesimal; v \ Infinitesimal; hypreal_of_real x + u \ hypreal_of_real y + v |] ==> x \ y" -by (blast intro!: hypreal_of_real_le_iff [THEN iffD1] - hypreal_of_real_le_add_Infininitesimal_cancel) +by (blast intro: star_of_le [THEN iffD1] + intro!: hypreal_of_real_le_add_Infininitesimal_cancel) lemma hypreal_of_real_less_Infinitesimal_le_zero: "[| hypreal_of_real x < e; e \ Infinitesimal |] ==> hypreal_of_real x \ 0" @@ -1498,13 +1499,13 @@ lemma Infinitesimal_square_cancel2 [simp]: "x*x + y*y \ Infinitesimal ==> y*y \ Infinitesimal" apply (rule Infinitesimal_square_cancel) -apply (rule hypreal_add_commute [THEN subst]) +apply (rule add_commute [THEN subst]) apply (simp (no_asm)) done lemma HFinite_square_cancel2 [simp]: "x*x + y*y \ HFinite ==> y*y \ HFinite" apply (rule HFinite_square_cancel) -apply (rule hypreal_add_commute [THEN subst]) +apply (rule add_commute [THEN subst]) apply (simp (no_asm)) done @@ -1625,7 +1626,7 @@ lemma st_Infinitesimal_add_SReal2: "[| x \ Reals; e \ Infinitesimal |] ==> st(e + x) = x" -apply (rule hypreal_add_commute [THEN subst]) +apply (rule add_commute [THEN subst]) apply (blast intro!: st_Infinitesimal_add_SReal) done @@ -1667,7 +1668,7 @@ qed lemma st_diff: "[| x \ HFinite; y \ HFinite |] ==> st (x-y) = st(x) - st(y)" -apply (simp add: hypreal_diff_def) +apply (simp add: diff_def) apply (frule_tac y1 = y in st_minus [symmetric]) apply (drule_tac x1 = y in HFinite_minus_iff [THEN iffD2]) apply (simp (no_asm_simp) add: st_add) @@ -1692,11 +1693,11 @@ apply (erule_tac V = "y = st y + ea" in thin_rl) apply (simp add: left_distrib right_distrib) apply (drule st_SReal)+ -apply (simp (no_asm_use) add: hypreal_add_assoc) +apply (simp (no_asm_use) add: add_assoc) apply (rule st_Infinitesimal_add_SReal) apply (blast intro!: SReal_mult) apply (drule SReal_subset_HFinite [THEN subsetD])+ -apply (rule hypreal_add_assoc [THEN subst]) +apply (rule add_assoc [THEN subst]) apply (blast intro!: lemma_st_mult) done @@ -1716,13 +1717,13 @@ ==> st(inverse x) = inverse (st x)" apply (rule_tac c1 = "st x" in hypreal_mult_left_cancel [THEN iffD1]) apply (auto simp add: st_mult [symmetric] st_not_Infinitesimal HFinite_inverse) -apply (subst hypreal_mult_inverse, auto) +apply (subst right_inverse, auto) done lemma st_divide [simp]: "[| x \ HFinite; y \ HFinite; st y \ 0 |] ==> st(x/y) = (st x) / (st y)" -by (simp add: hypreal_divide_def st_mult st_not_Infinitesimal HFinite_inverse st_inverse) +by (simp add: divide_inverse st_mult st_not_Infinitesimal HFinite_inverse st_inverse) lemma st_idempotent [simp]: "x \ HFinite ==> st(st(x)) = st(x)" by (blast intro: st_HFinite st_approx_self approx_st_eq) @@ -1748,7 +1749,7 @@ apply (frule HFinite_st_Infinitesimal_add, safe) apply (rule Infinitesimal_add_st_le_cancel) apply (rule_tac [3] x = ea and y = e in Infinitesimal_diff) -apply (auto simp add: hypreal_add_assoc [symmetric]) +apply (auto simp add: add_assoc [symmetric]) done lemma st_zero_le: "[| 0 \ x; x \ HFinite |] ==> 0 \ st x" @@ -1781,29 +1782,30 @@ lemma HFinite_FreeUltrafilterNat: "x \ HFinite ==> \X \ Rep_star x. \u. {n. abs (X n) < u} \ FreeUltrafilterNat" -apply (rule_tac z = x in eq_Abs_star) +apply (cases x) apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x] - star_of_def star_n_def - hypreal_less SReal_iff hypreal_minus hypreal_of_real_def) -apply (rule_tac x=x in bexI) -apply (rule_tac x=y in exI, auto, ultra) + star_of_def + star_n_less SReal_iff star_n_minus) +apply (rule_tac x=X in bexI) +apply (rule_tac x=y in exI, ultra) +apply simp done lemma FreeUltrafilterNat_HFinite: "\X \ Rep_star x. \u. {n. abs (X n) < u} \ FreeUltrafilterNat ==> x \ HFinite" -apply (rule_tac z = x in eq_Abs_star) +apply (cases x) apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x]) apply (rule_tac x = "hypreal_of_real u" in bexI) -apply (auto simp add: hypreal_less SReal_iff hypreal_minus hypreal_of_real_def star_of_def star_n_def, ultra+) +apply (auto simp add: star_n_less SReal_iff star_n_minus star_of_def) +apply ultra+ done lemma HFinite_FreeUltrafilterNat_iff: "(x \ HFinite) = (\X \ Rep_star x. \u. {n. abs (X n) < u} \ FreeUltrafilterNat)" -apply (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite) -done +by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite) subsection{*Alternative Definitions for @{term HInfinite} using Free Ultrafilter*} @@ -1817,8 +1819,7 @@ lemma lemma_Int_eq1: "{n. abs (xa n) \ (u::real)} Int {n. u \ abs (xa n)} = {n. abs(xa n) = u}" -apply auto -done +by auto lemma lemma_FreeUltrafilterNat_one: "{n. abs (xa n) = u} \ {n. abs (xa n) < u + (1::real)}" @@ -1888,11 +1889,11 @@ \u. 0 < u --> {n. abs (X n) < u} \ FreeUltrafilterNat" apply (simp add: Infinitesimal_def) apply (auto simp add: abs_less_iff minus_less_iff [of x]) -apply (rule_tac z = x in eq_Abs_star) -apply (auto, rule bexI [OF _ lemma_starrel_refl], safe) -apply (drule hypreal_of_real_less_iff [THEN iffD2]) +apply (cases x) +apply (auto, rule bexI [OF _ Rep_star_star_n], safe) +apply (drule star_of_less [THEN iffD2]) apply (drule_tac x = "hypreal_of_real u" in bspec, auto) -apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def star_of_def star_n_def, ultra) +apply (auto simp add: star_n_less star_n_minus star_of_def, ultra) done lemma FreeUltrafilterNat_Infinitesimal: @@ -1900,18 +1901,17 @@ \u. 0 < u --> {n. abs (X n) < u} \ FreeUltrafilterNat ==> x \ Infinitesimal" apply (simp add: Infinitesimal_def) -apply (rule_tac z = x in eq_Abs_star) +apply (cases x) apply (auto simp add: abs_less_iff abs_interval_iff minus_less_iff [of x]) apply (auto simp add: SReal_iff) apply (drule_tac [!] x=y in spec) -apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def star_of_def star_n_def, ultra+) +apply (auto simp add: star_n_less star_n_minus star_of_def, ultra+) done lemma Infinitesimal_FreeUltrafilterNat_iff: "(x \ Infinitesimal) = (\X \ Rep_star x. \u. 0 < u --> {n. abs (X n) < u} \ FreeUltrafilterNat)" -apply (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal) -done +by (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal) (*------------------------------------------------------------------------ Infinitesimals as smaller than 1/n for all n::nat (> 0) @@ -1934,11 +1934,11 @@ apply safe apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec) apply (simp (no_asm_use) add: SReal_inverse) -apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN hypreal_of_real_less_iff [THEN iffD2], THEN [2] impE]) +apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN star_of_less [THEN iffD2], THEN [2] impE]) prefer 2 apply assumption apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_eq) apply (auto dest!: reals_Archimedean simp add: SReal_iff) -apply (drule hypreal_of_real_less_iff [THEN iffD2]) +apply (drule star_of_less [THEN iffD2]) apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_eq) apply (blast intro: order_less_trans) done @@ -2009,9 +2009,6 @@ text{*@{term omega} is a member of @{term HInfinite}*} -lemma hypreal_omega: "starrel``{%n::nat. real (Suc n)} \ star" -by auto - lemma FreeUltrafilterNat_omega: "{n. u < real n} \ FreeUltrafilterNat" apply (cut_tac u = u in rabs_real_of_nat_le_real_FreeUltrafilterNat) apply (auto dest: FreeUltrafilterNat_Compl_mem simp add: Compl_real_le_eq) @@ -2123,13 +2120,13 @@ -----------------------------------------------------*) lemma real_seq_to_hypreal_Infinitesimal: "\n. abs(X n + -x) < inverse(real(Suc n)) - ==> Abs_star(starrel``{X}) + -hypreal_of_real x \ Infinitesimal" -apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: hypreal_minus hypreal_of_real_def star_of_def star_n_def hypreal_add Infinitesimal_FreeUltrafilterNat_iff hypreal_inverse) + ==> star_n X + -hypreal_of_real x \ Infinitesimal" +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) done lemma real_seq_to_hypreal_approx: "\n. abs(X n + -x) < inverse(real(Suc n)) - ==> Abs_star(starrel``{X}) @= hypreal_of_real x" + ==> star_n X @= hypreal_of_real x" apply (subst approx_minus_iff) apply (rule mem_infmal_iff [THEN subst]) apply (erule real_seq_to_hypreal_Infinitesimal) @@ -2137,20 +2134,19 @@ lemma real_seq_to_hypreal_approx2: "\n. abs(x + -X n) < inverse(real(Suc n)) - ==> Abs_star(starrel``{X}) @= hypreal_of_real x" + ==> star_n X @= hypreal_of_real x" apply (simp add: abs_minus_add_cancel real_seq_to_hypreal_approx) done lemma real_seq_to_hypreal_Infinitesimal2: "\n. abs(X n + -Y n) < inverse(real(Suc n)) - ==> Abs_star(starrel``{X}) + - -Abs_star(starrel``{Y}) \ Infinitesimal" + ==> star_n X + -star_n Y \ Infinitesimal" by (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset - simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_minus - hypreal_add hypreal_inverse) + simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_minus + star_n_add star_n_inverse) ML @@ -2335,7 +2331,6 @@ val finite_rabs_real_of_nat_le_real = thm "finite_rabs_real_of_nat_le_real"; val rabs_real_of_nat_le_real_FreeUltrafilterNat = thm "rabs_real_of_nat_le_real_FreeUltrafilterNat"; val FreeUltrafilterNat_nat_gt_real = thm "FreeUltrafilterNat_nat_gt_real"; -val hypreal_omega = thm "hypreal_omega"; val FreeUltrafilterNat_omega = thm "FreeUltrafilterNat_omega"; val HInfinite_omega = thm "HInfinite_omega"; val Infinitesimal_epsilon = thm "Infinitesimal_epsilon";