--- 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) \<in> Reals ==> inverse x \<in> 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) \<in> Reals; y \<in> Reals |] ==> x/y \<in> 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) \<in> Reals ==> -x \<in> 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 \<in> Reals) = ((x::hypreal) \<in> Reals)"
@@ -91,15 +90,16 @@
done
lemma SReal_hrabs: "(x::hypreal) \<in> Reals ==> abs x \<in> 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 \<in> Reals"
by (simp add: SReal_def)
lemma SReal_number_of [simp]: "(number_of w ::hypreal) \<in> 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 \<in> Reals ==> r/(number_of w::hypreal) \<in> 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 \<subseteq> 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 \<in> HFinite"
@@ -278,7 +278,7 @@
lemma HFinite_bounded: "[|x \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
apply (case_tac "x \<le> 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 \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
-by (simp add: hypreal_diff_def Infinitesimal_add)
+by (simp add: diff_def Infinitesimal_add)
lemma Infinitesimal_mult:
"[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> (x * y) \<in> Infinitesimal"
@@ -331,7 +331,7 @@
lemma Infinitesimal_HFinite_mult2:
"[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (y * x) \<in> 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 \<in> HInfinite; 0 \<le> y; 0 \<le> 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 \<in> HInfinite; 0 \<le> y; 0 \<le> 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 \<in> 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 \<in> 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 \<in> HFinite|] ==> u @= v*y"
by (blast intro: approx_mult2 approx_trans)
@@ -694,17 +694,17 @@
lemma Infinitesimal_add_approx: "[| y \<in> 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 \<in> 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 \<in> 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 \<in> Infinitesimal ==> x @= x + -y"
by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2])
@@ -718,7 +718,7 @@
"[| y \<in> 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 \<in> HFinite; x @= y |] ==> y \<in> 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 \<in> HFinite"
@@ -773,7 +773,7 @@
lemma approx_SReal_mult_cancel_zero:
"[| a \<in> Reals; a \<noteq> 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 \<in> Reals; x @= 0 |] ==> x*a @= 0"
@@ -789,7 +789,7 @@
lemma approx_SReal_mult_cancel:
"[| a \<in> Reals; a \<noteq> 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 \<noteq> 0; y \<in> Infinitesimal; x/y \<in> HFinite |] ==> x \<in> 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 \<le> t + -r ==> r \<le> (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 \<in> HFinite - Infinitesimal ==> inverse x \<in> 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 \<in> HFinite - Infinitesimal;
h \<in> 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 \<in> HInfinite; y \<in> HFinite |] ==> x + y \<in> 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 \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
==> y * x \<in> 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 \<in> HInfinite; 0 < x; y \<in> 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 \<in> 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 \<in> Infinitesimal; v \<in> Infinitesimal;
hypreal_of_real x + u \<le> hypreal_of_real y + v |]
==> x \<le> 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 \<in> Infinitesimal |] ==> hypreal_of_real x \<le> 0"
@@ -1498,13 +1499,13 @@
lemma Infinitesimal_square_cancel2 [simp]:
"x*x + y*y \<in> Infinitesimal ==> y*y \<in> 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 \<in> HFinite ==> y*y \<in> 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 \<in> Reals; e \<in> 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 \<in> HFinite; y \<in> 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 \<in> HFinite; y \<in> HFinite; st y \<noteq> 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 \<in> 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 \<le> x; x \<in> HFinite |] ==> 0 \<le> st x"
@@ -1781,29 +1782,30 @@
lemma HFinite_FreeUltrafilterNat:
"x \<in> HFinite
==> \<exists>X \<in> Rep_star x. \<exists>u. {n. abs (X n) < u} \<in> 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:
"\<exists>X \<in> Rep_star x.
\<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat
==> x \<in> 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 \<in> HFinite) = (\<exists>X \<in> Rep_star x.
\<exists>u. {n. abs (X n) < u} \<in> 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) \<le> (u::real)} Int {n. u \<le> abs (xa n)}
= {n. abs(xa n) = u}"
-apply auto
-done
+by auto
lemma lemma_FreeUltrafilterNat_one:
"{n. abs (xa n) = u} \<le> {n. abs (xa n) < u + (1::real)}"
@@ -1888,11 +1889,11 @@
\<forall>u. 0 < u --> {n. abs (X n) < u} \<in> 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 @@
\<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat
==> x \<in> 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 \<in> Infinitesimal) = (\<exists>X \<in> Rep_star x.
\<forall>u. 0 < u --> {n. abs (X n) < u} \<in> 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)} \<in> star"
-by auto
-
lemma FreeUltrafilterNat_omega: "{n. u < real n} \<in> 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:
"\<forall>n. abs(X n + -x) < inverse(real(Suc n))
- ==> Abs_star(starrel``{X}) + -hypreal_of_real x \<in> 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 \<in> 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:
"\<forall>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:
"\<forall>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:
"\<forall>n. abs(X n + -Y n) < inverse(real(Suc n))
- ==> Abs_star(starrel``{X}) +
- -Abs_star(starrel``{Y}) \<in> Infinitesimal"
+ ==> star_n X + -star_n Y \<in> 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";