--- a/src/HOL/Hyperreal/NSA.thy Wed Jan 28 17:01:01 2004 +0100
+++ b/src/HOL/Hyperreal/NSA.thy Thu Jan 29 16:51:17 2004 +0100
@@ -1,46 +1,2346 @@
(* Title : NSA.thy
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
- Description : Infinite numbers, Infinitesimals,
- infinitely close relation etc.
-*)
+*)
-NSA = HRealAbs + RComplete +
+header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
+
+theory NSA = HRealAbs + RComplete:
constdefs
Infinitesimal :: "hypreal set"
- "Infinitesimal == {x. ALL r: Reals. 0 < r --> abs x < r}"
+ "Infinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> abs x < r}"
HFinite :: "hypreal set"
- "HFinite == {x. EX r: Reals. abs x < r}"
+ "HFinite == {x. \<exists>r \<in> Reals. abs x < r}"
HInfinite :: "hypreal set"
- "HInfinite == {x. ALL r: Reals. r < abs x}"
+ "HInfinite == {x. \<forall>r \<in> Reals. r < abs x}"
(* standard part map *)
- st :: hypreal => hypreal
- "st == (%x. @r. x : HFinite & r:Reals & r @= x)"
+ st :: "hypreal => hypreal"
+ "st == (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
- monad :: hypreal => hypreal set
+ monad :: "hypreal => hypreal set"
"monad x == {y. x @= y}"
- galaxy :: hypreal => hypreal set
- "galaxy x == {y. (x + -y) : HFinite}"
-
+ galaxy :: "hypreal => hypreal set"
+ "galaxy x == {y. (x + -y) \<in> HFinite}"
+
(* infinitely close *)
approx :: "[hypreal, hypreal] => bool" (infixl "@=" 50)
- "x @= y == (x + -y) : Infinitesimal"
+ "x @= y == (x + -y) \<in> Infinitesimal"
+
+
+defs
+
+ (*standard real numbers as a subset of the hyperreals*)
+ SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
+
+syntax (xsymbols)
+ approx :: "[hypreal, hypreal] => bool" (infixl "\<approx>" 50)
+
+
+
+(*--------------------------------------------------------------------
+ Closure laws for members of (embedded) set standard real Reals
+ --------------------------------------------------------------------*)
+
+lemma SReal_add: "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"
+apply (auto simp add: SReal_def)
+apply (rule_tac x = "r + ra" in exI, simp)
+done
+
+lemma SReal_mult: "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x * y \<in> Reals"
+apply (simp add: SReal_def, safe)
+apply (rule_tac x = "r * ra" in exI)
+apply (simp (no_asm) add: hypreal_of_real_mult)
+done
+
+lemma SReal_inverse: "(x::hypreal) \<in> Reals ==> inverse x \<in> Reals"
+apply (simp add: SReal_def)
+apply (blast intro: hypreal_of_real_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
+
+lemma SReal_minus: "(x::hypreal) \<in> Reals ==> -x \<in> Reals"
+apply (simp add: SReal_def)
+apply (blast intro: hypreal_of_real_minus [symmetric])
+done
+
+lemma SReal_minus_iff: "(-x \<in> Reals) = ((x::hypreal) \<in> Reals)"
+apply auto
+apply (erule_tac [2] SReal_minus)
+apply (drule SReal_minus, auto)
+done
+declare SReal_minus_iff [simp]
+
+lemma SReal_add_cancel: "[| (x::hypreal) + y \<in> Reals; y \<in> Reals |] ==> x \<in> Reals"
+apply (drule_tac x = y in SReal_minus)
+apply (drule SReal_add, assumption, auto)
+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)
+done
+
+lemma SReal_hypreal_of_real: "hypreal_of_real x \<in> Reals"
+by (simp add: SReal_def)
+declare SReal_hypreal_of_real [simp]
+
+lemma SReal_number_of: "(number_of w ::hypreal) \<in> Reals"
+apply (unfold hypreal_number_of_def)
+apply (rule SReal_hypreal_of_real)
+done
+declare SReal_number_of [simp]
+
+(** As always with numerals, 0 and 1 are special cases **)
+
+lemma Reals_0: "(0::hypreal) \<in> Reals"
+apply (subst hypreal_numeral_0_eq_0 [symmetric])
+apply (rule SReal_number_of)
+done
+declare Reals_0 [simp]
+
+lemma Reals_1: "(1::hypreal) \<in> Reals"
+apply (subst hypreal_numeral_1_eq_1 [symmetric])
+apply (rule SReal_number_of)
+done
+declare Reals_1 [simp]
+
+lemma SReal_divide_number_of: "r \<in> Reals ==> r/(number_of w::hypreal) \<in> Reals"
+apply (unfold hypreal_divide_def)
+apply (blast intro!: SReal_number_of SReal_mult SReal_inverse)
+done
+
+(* Infinitesimal epsilon not in Reals *)
+
+lemma SReal_epsilon_not_mem: "epsilon \<notin> Reals"
+apply (simp add: SReal_def)
+apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym])
+done
+
+lemma SReal_omega_not_mem: "omega \<notin> Reals"
+apply (simp add: SReal_def)
+apply (auto simp add: hypreal_of_real_not_eq_omega [THEN not_sym])
+done
+
+lemma SReal_UNIV_real: "{x. hypreal_of_real x \<in> Reals} = (UNIV::real set)"
+by (simp add: SReal_def)
+
+lemma SReal_iff: "(x \<in> Reals) = (\<exists>y. x = hypreal_of_real y)"
+by (simp add: SReal_def)
+
+lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = Reals"
+by (auto simp add: SReal_def)
+
+lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` Reals = UNIV"
+apply (auto simp add: SReal_def)
+apply (rule inj_hypreal_of_real [THEN inv_f_f, THEN subst], blast)
+done
+
+lemma SReal_hypreal_of_real_image:
+ "[| \<exists>x. x: P; P <= Reals |] ==> \<exists>Q. P = hypreal_of_real ` Q"
+apply (simp add: SReal_def, blast)
+done
+
+lemma SReal_dense: "[| (x::hypreal) \<in> Reals; y \<in> Reals; x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
+apply (auto simp add: SReal_iff)
+apply (drule real_dense, safe)
+apply (rule_tac x = "hypreal_of_real r" in bexI, auto)
+done
+
+(*------------------------------------------------------------------
+ Completeness of Reals
+ ------------------------------------------------------------------*)
+lemma SReal_sup_lemma: "P <= Reals ==> ((\<exists>x \<in> P. y < x) =
+ (\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))"
+by (blast dest!: SReal_iff [THEN iffD1])
+
+lemma SReal_sup_lemma2:
+ "[| P <= Reals; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |]
+ ==> (\<exists>X. X \<in> {w. hypreal_of_real w \<in> P}) &
+ (\<exists>Y. \<forall>X \<in> {w. hypreal_of_real w \<in> P}. X < Y)"
+apply (rule conjI)
+apply (fast dest!: SReal_iff [THEN iffD1])
+apply (auto, frule subsetD, assumption)
+apply (drule SReal_iff [THEN iffD1])
+apply (auto, rule_tac x = ya in exI, auto)
+done
+
+(*------------------------------------------------------
+ lifting of ub and property of lub
+ -------------------------------------------------------*)
+lemma hypreal_of_real_isUb_iff:
+ "(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) =
+ (isUb (UNIV :: real set) Q Y)"
+apply (simp add: isUb_def setle_def)
+done
+
+lemma hypreal_of_real_isLub1:
+ "isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)
+ ==> isLub (UNIV :: real set) Q Y"
+apply (simp add: isLub_def leastP_def)
+apply (auto intro: hypreal_of_real_isUb_iff [THEN iffD2]
+ simp add: hypreal_of_real_isUb_iff setge_def)
+done
+
+lemma hypreal_of_real_isLub2:
+ "isLub (UNIV :: real set) Q Y
+ ==> isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)"
+apply (simp add: isLub_def leastP_def)
+apply (auto simp add: hypreal_of_real_isUb_iff setge_def)
+apply (frule_tac x2 = x in isUbD2a [THEN SReal_iff [THEN iffD1], THEN exE])
+ prefer 2 apply assumption
+apply (drule_tac x = xa in spec)
+apply (auto simp add: hypreal_of_real_isUb_iff)
+done
+
+lemma hypreal_of_real_isLub_iff: "(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) =
+ (isLub (UNIV :: real set) Q Y)"
+apply (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)
+done
+
+(* lemmas *)
+lemma lemma_isUb_hypreal_of_real:
+ "isUb Reals P Y ==> \<exists>Yo. isUb Reals P (hypreal_of_real Yo)"
+by (auto simp add: SReal_iff isUb_def)
+
+lemma lemma_isLub_hypreal_of_real:
+ "isLub Reals P Y ==> \<exists>Yo. isLub Reals P (hypreal_of_real Yo)"
+by (auto simp add: isLub_def leastP_def isUb_def SReal_iff)
+
+lemma lemma_isLub_hypreal_of_real2:
+ "\<exists>Yo. isLub Reals P (hypreal_of_real Yo) ==> \<exists>Y. isLub Reals P Y"
+by (auto simp add: isLub_def leastP_def isUb_def)
+
+lemma SReal_complete: "[| P <= Reals; \<exists>x. x \<in> P; \<exists>Y. isUb Reals P Y |]
+ ==> \<exists>t::hypreal. isLub Reals P t"
+apply (frule SReal_hypreal_of_real_image)
+apply (auto, drule lemma_isUb_hypreal_of_real)
+apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2 simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff)
+done
+
+(*--------------------------------------------------------------------
+ Set of finite elements is a subring of the extended reals
+ --------------------------------------------------------------------*)
+lemma HFinite_add: "[|x \<in> HFinite; y \<in> HFinite|] ==> (x+y) \<in> HFinite"
+apply (simp add: HFinite_def)
+apply (blast intro!: SReal_add hrabs_add_less)
+done
+
+lemma HFinite_mult: "[|x \<in> HFinite; y \<in> HFinite|] ==> x*y \<in> HFinite"
+apply (simp add: HFinite_def)
+apply (blast intro!: SReal_mult abs_mult_less)
+done
+
+lemma HFinite_minus_iff: "(-x \<in> HFinite) = (x \<in> HFinite)"
+by (simp add: HFinite_def)
+
+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)
+done
+
+lemma HFinite_hypreal_of_real [simp]: "hypreal_of_real x \<in> HFinite"
+by (auto intro: SReal_subset_HFinite [THEN subsetD])
+
+lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. abs x < t"
+by (simp add: HFinite_def)
+
+lemma HFinite_hrabs_iff: "(abs x \<in> HFinite) = (x \<in> HFinite)"
+by (simp add: HFinite_def)
+declare HFinite_hrabs_iff [iff]
+
+lemma HFinite_number_of: "number_of w \<in> HFinite"
+by (rule SReal_number_of [THEN SReal_subset_HFinite [THEN subsetD]])
+declare HFinite_number_of [simp]
+
+(** As always with numerals, 0 and 1 are special cases **)
+
+lemma HFinite_0: "0 \<in> HFinite"
+apply (subst hypreal_numeral_0_eq_0 [symmetric])
+apply (rule HFinite_number_of)
+done
+declare HFinite_0 [simp]
+
+lemma HFinite_1: "1 \<in> HFinite"
+apply (subst hypreal_numeral_1_eq_1 [symmetric])
+apply (rule HFinite_number_of)
+done
+declare HFinite_1 [simp]
+
+lemma HFinite_bounded: "[|x \<in> HFinite; y <= x; 0 <= y |] ==> y \<in> HFinite"
+apply (case_tac "x <= 0")
+apply (drule_tac y = x in order_trans)
+apply (drule_tac [2] hypreal_le_anti_sym)
+apply (auto simp add: linorder_not_le)
+apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def)
+done
+
+(*------------------------------------------------------------------
+ Set of infinitesimals is a subring of the hyperreals
+ ------------------------------------------------------------------*)
+lemma InfinitesimalD:
+ "x \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> abs x < r"
+apply (simp add: Infinitesimal_def)
+done
+
+lemma Infinitesimal_zero: "0 \<in> Infinitesimal"
+by (simp add: Infinitesimal_def)
+declare Infinitesimal_zero [iff]
+
+lemma hypreal_sum_of_halves: "x/(2::hypreal) + x/(2::hypreal) = x"
+by auto
+
+lemma hypreal_half_gt_zero: "0 < r ==> 0 < r/(2::hypreal)"
+by auto
+
+lemma Infinitesimal_add:
+ "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> (x+y) \<in> Infinitesimal"
+apply (auto simp add: Infinitesimal_def)
+apply (rule hypreal_sum_of_halves [THEN subst])
+apply (drule hypreal_half_gt_zero)
+apply (blast intro: hrabs_add_less hrabs_add_less SReal_divide_number_of)
+done
+
+lemma Infinitesimal_minus_iff: "(-x:Infinitesimal) = (x:Infinitesimal)"
+by (simp add: Infinitesimal_def)
+declare Infinitesimal_minus_iff [simp]
+
+lemma Infinitesimal_diff: "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
+by (simp add: hypreal_diff_def Infinitesimal_add)
+
+lemma Infinitesimal_mult:
+ "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> (x * y) \<in> Infinitesimal"
+apply (auto simp add: Infinitesimal_def)
+apply (case_tac "y=0")
+apply (cut_tac [2] a = "abs x" and b = 1 and c = "abs y" and d = r in mult_strict_mono, auto)
+done
+
+lemma Infinitesimal_HFinite_mult: "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (x * y) \<in> Infinitesimal"
+apply (auto dest!: HFiniteD simp add: Infinitesimal_def)
+apply (frule hrabs_less_gt_zero)
+apply (drule_tac x = "r/t" in bspec)
+apply (blast intro: SReal_divide)
+apply (simp add: zero_less_divide_iff)
+apply (case_tac "x=0 | y=0")
+apply (cut_tac [2] a = "abs x" and b = "r/t" and c = "abs y" in mult_strict_mono)
+apply (auto simp add: zero_less_divide_iff)
+done
+
+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)
+
+(*** rather long proof ***)
+lemma HInfinite_inverse_Infinitesimal:
+ "x \<in> HInfinite ==> inverse x: Infinitesimal"
+apply (auto simp add: HInfinite_def Infinitesimal_def)
+apply (erule_tac x = "inverse r" in ballE)
+apply (frule_tac a1 = r and z = "abs x" in positive_imp_inverse_positive [THEN order_less_trans], assumption)
+apply (drule inverse_inverse_eq [symmetric, THEN subst])
+apply (rule inverse_less_iff_less [THEN iffD1])
+apply (auto simp add: SReal_inverse)
+done
+
+
+
+lemma HInfinite_mult: "[|x \<in> HInfinite;y \<in> HInfinite|] ==> (x*y) \<in> HInfinite"
+apply (simp add: HInfinite_def, auto)
+apply (erule_tac x = 1 in ballE)
+apply (erule_tac x = r in ballE)
+apply (case_tac "y=0")
+apply (cut_tac [2] c = 1 and d = "abs x" and a = r and b = "abs y" in mult_strict_mono)
+apply (auto simp add: mult_ac)
+done
+
+lemma HInfinite_add_ge_zero:
+ "[|x \<in> 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)
+
+lemma HInfinite_add_ge_zero2: "[|x \<in> HInfinite; 0 <= y; 0 <= x|] ==> (y + x): HInfinite"
+by (auto intro!: HInfinite_add_ge_zero simp add: hypreal_add_commute)
+
+lemma HInfinite_add_gt_zero: "[|x \<in> HInfinite; 0 < y; 0 < x|] ==> (x + y): HInfinite"
+by (blast intro: HInfinite_add_ge_zero order_less_imp_le)
+
+lemma HInfinite_minus_iff: "(-x \<in> HInfinite) = (x \<in> HInfinite)"
+by (simp add: HInfinite_def)
+
+lemma HInfinite_add_le_zero: "[|x \<in> HInfinite; y <= 0; x <= 0|] ==> (x + y): HInfinite"
+apply (drule HInfinite_minus_iff [THEN iffD2])
+apply (rule HInfinite_minus_iff [THEN iffD1])
+apply (auto intro: HInfinite_add_ge_zero)
+done
+
+lemma HInfinite_add_lt_zero: "[|x \<in> HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite"
+by (blast intro: HInfinite_add_le_zero order_less_imp_le)
+
+lemma HFinite_sum_squares: "[|a: HFinite; b: HFinite; c: HFinite|]
+ ==> a*a + b*b + c*c \<in> HFinite"
+apply (auto intro: HFinite_mult HFinite_add)
+done
+
+lemma not_Infinitesimal_not_zero: "x \<notin> Infinitesimal ==> x \<noteq> 0"
+by auto
+
+lemma not_Infinitesimal_not_zero2: "x \<in> HFinite - Infinitesimal ==> x \<noteq> 0"
+by auto
+
+lemma Infinitesimal_hrabs_iff: "(abs x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
+by (auto simp add: hrabs_def)
+declare Infinitesimal_hrabs_iff [iff]
+
+lemma HFinite_diff_Infinitesimal_hrabs: "x \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal"
+by blast
+
+lemma hrabs_less_Infinitesimal:
+ "[| e \<in> Infinitesimal; abs x < e |] ==> x \<in> Infinitesimal"
+apply (auto simp add: Infinitesimal_def abs_less_iff)
+done
+
+lemma hrabs_le_Infinitesimal: "[| e \<in> Infinitesimal; abs x <= e |] ==> x \<in> Infinitesimal"
+by (blast dest: order_le_imp_less_or_eq intro: hrabs_less_Infinitesimal)
+
+lemma Infinitesimal_interval:
+ "[| e \<in> Infinitesimal; e' \<in> Infinitesimal; e' < x ; x < e |]
+ ==> x \<in> Infinitesimal"
+apply (auto simp add: Infinitesimal_def abs_less_iff)
+done
+
+lemma Infinitesimal_interval2: "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
+ e' <= x ; x <= e |] ==> x \<in> Infinitesimal"
+apply (auto intro: Infinitesimal_interval simp add: order_le_less)
+done
+
+lemma not_Infinitesimal_mult:
+ "[| x \<notin> Infinitesimal; y \<notin> Infinitesimal|] ==> (x*y) \<notin>Infinitesimal"
+apply (unfold Infinitesimal_def, clarify)
+apply (simp add: linorder_not_less)
+apply (erule_tac x = "r*ra" in ballE)
+prefer 2 apply (fast intro: SReal_mult)
+apply (auto simp add: zero_less_mult_iff)
+apply (cut_tac c = ra and d = "abs y" and a = r and b = "abs x" in mult_mono, auto)
+done
+
+lemma Infinitesimal_mult_disj: "x*y \<in> Infinitesimal ==> x \<in> Infinitesimal | y \<in> Infinitesimal"
+apply (rule ccontr)
+apply (drule de_Morgan_disj [THEN iffD1])
+apply (fast dest: not_Infinitesimal_mult)
+done
+
+lemma HFinite_Infinitesimal_not_zero: "x \<in> HFinite-Infinitesimal ==> x \<noteq> 0"
+by blast
+
+lemma HFinite_Infinitesimal_diff_mult: "[| x \<in> HFinite - Infinitesimal;
+ y \<in> HFinite - Infinitesimal
+ |] ==> (x*y) \<in> HFinite - Infinitesimal"
+apply clarify
+apply (blast dest: HFinite_mult not_Infinitesimal_mult)
+done
+
+lemma Infinitesimal_subset_HFinite:
+ "Infinitesimal <= HFinite"
+apply (simp add: Infinitesimal_def HFinite_def, auto)
+apply (rule_tac x = 1 in bexI, auto)
+done
+
+lemma Infinitesimal_hypreal_of_real_mult: "x \<in> Infinitesimal ==> x * hypreal_of_real r \<in> Infinitesimal"
+by (erule HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult])
+
+lemma Infinitesimal_hypreal_of_real_mult2: "x \<in> Infinitesimal ==> hypreal_of_real r * x \<in> Infinitesimal"
+by (erule HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult2])
+
+(*----------------------------------------------------------------------
+ Infinitely close relation @=
+ ----------------------------------------------------------------------*)
+
+lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)"
+by (simp add: Infinitesimal_def approx_def)
+
+lemma approx_minus_iff: " (x @= y) = (x + -y @= 0)"
+by (simp add: approx_def)
+
+lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)"
+by (simp add: approx_def hypreal_add_commute)
+
+lemma approx_refl: "x @= x"
+by (simp add: approx_def Infinitesimal_def)
+declare approx_refl [iff]
+
+lemma approx_sym: "x @= y ==> y @= x"
+apply (simp add: approx_def)
+apply (rule hypreal_minus_distrib1 [THEN subst])
+apply (erule Infinitesimal_minus_iff [THEN iffD2])
+done
+
+lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z"
+apply (simp add: approx_def)
+apply (drule Infinitesimal_add, assumption, auto)
+done
+
+lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s"
+by (blast intro: approx_sym approx_trans)
+
+lemma approx_trans3: "[| x @= r; x @= s|] ==> r @= s"
+by (blast intro: approx_sym approx_trans)
+
+lemma number_of_approx_reorient: "(number_of w @= x) = (x @= number_of w)"
+by (blast intro: approx_sym)
+
+lemma zero_approx_reorient: "(0 @= x) = (x @= 0)"
+by (blast intro: approx_sym)
+
+lemma one_approx_reorient: "(1 @= x) = (x @= 1)"
+by (blast intro: approx_sym)
-defs
+ML
+{*
+val SReal_add = thm "SReal_add";
+val SReal_mult = thm "SReal_mult";
+val SReal_inverse = thm "SReal_inverse";
+val SReal_divide = thm "SReal_divide";
+val SReal_minus = thm "SReal_minus";
+val SReal_minus_iff = thm "SReal_minus_iff";
+val SReal_add_cancel = thm "SReal_add_cancel";
+val SReal_hrabs = thm "SReal_hrabs";
+val SReal_hypreal_of_real = thm "SReal_hypreal_of_real";
+val SReal_number_of = thm "SReal_number_of";
+val Reals_0 = thm "Reals_0";
+val Reals_1 = thm "Reals_1";
+val SReal_divide_number_of = thm "SReal_divide_number_of";
+val SReal_epsilon_not_mem = thm "SReal_epsilon_not_mem";
+val SReal_omega_not_mem = thm "SReal_omega_not_mem";
+val SReal_UNIV_real = thm "SReal_UNIV_real";
+val SReal_iff = thm "SReal_iff";
+val hypreal_of_real_image = thm "hypreal_of_real_image";
+val inv_hypreal_of_real_image = thm "inv_hypreal_of_real_image";
+val SReal_hypreal_of_real_image = thm "SReal_hypreal_of_real_image";
+val SReal_dense = thm "SReal_dense";
+val SReal_sup_lemma = thm "SReal_sup_lemma";
+val SReal_sup_lemma2 = thm "SReal_sup_lemma2";
+val hypreal_of_real_isUb_iff = thm "hypreal_of_real_isUb_iff";
+val hypreal_of_real_isLub1 = thm "hypreal_of_real_isLub1";
+val hypreal_of_real_isLub2 = thm "hypreal_of_real_isLub2";
+val hypreal_of_real_isLub_iff = thm "hypreal_of_real_isLub_iff";
+val lemma_isUb_hypreal_of_real = thm "lemma_isUb_hypreal_of_real";
+val lemma_isLub_hypreal_of_real = thm "lemma_isLub_hypreal_of_real";
+val lemma_isLub_hypreal_of_real2 = thm "lemma_isLub_hypreal_of_real2";
+val SReal_complete = thm "SReal_complete";
+val HFinite_add = thm "HFinite_add";
+val HFinite_mult = thm "HFinite_mult";
+val HFinite_minus_iff = thm "HFinite_minus_iff";
+val SReal_subset_HFinite = thm "SReal_subset_HFinite";
+val HFinite_hypreal_of_real = thm "HFinite_hypreal_of_real";
+val HFiniteD = thm "HFiniteD";
+val HFinite_hrabs_iff = thm "HFinite_hrabs_iff";
+val HFinite_number_of = thm "HFinite_number_of";
+val HFinite_0 = thm "HFinite_0";
+val HFinite_1 = thm "HFinite_1";
+val HFinite_bounded = thm "HFinite_bounded";
+val InfinitesimalD = thm "InfinitesimalD";
+val Infinitesimal_zero = thm "Infinitesimal_zero";
+val hypreal_sum_of_halves = thm "hypreal_sum_of_halves";
+val hypreal_half_gt_zero = thm "hypreal_half_gt_zero";
+val Infinitesimal_add = thm "Infinitesimal_add";
+val Infinitesimal_minus_iff = thm "Infinitesimal_minus_iff";
+val Infinitesimal_diff = thm "Infinitesimal_diff";
+val Infinitesimal_mult = thm "Infinitesimal_mult";
+val Infinitesimal_HFinite_mult = thm "Infinitesimal_HFinite_mult";
+val Infinitesimal_HFinite_mult2 = thm "Infinitesimal_HFinite_mult2";
+val HInfinite_inverse_Infinitesimal = thm "HInfinite_inverse_Infinitesimal";
+val HInfinite_mult = thm "HInfinite_mult";
+val HInfinite_add_ge_zero = thm "HInfinite_add_ge_zero";
+val HInfinite_add_ge_zero2 = thm "HInfinite_add_ge_zero2";
+val HInfinite_add_gt_zero = thm "HInfinite_add_gt_zero";
+val HInfinite_minus_iff = thm "HInfinite_minus_iff";
+val HInfinite_add_le_zero = thm "HInfinite_add_le_zero";
+val HInfinite_add_lt_zero = thm "HInfinite_add_lt_zero";
+val HFinite_sum_squares = thm "HFinite_sum_squares";
+val not_Infinitesimal_not_zero = thm "not_Infinitesimal_not_zero";
+val not_Infinitesimal_not_zero2 = thm "not_Infinitesimal_not_zero2";
+val Infinitesimal_hrabs_iff = thm "Infinitesimal_hrabs_iff";
+val HFinite_diff_Infinitesimal_hrabs = thm "HFinite_diff_Infinitesimal_hrabs";
+val hrabs_less_Infinitesimal = thm "hrabs_less_Infinitesimal";
+val hrabs_le_Infinitesimal = thm "hrabs_le_Infinitesimal";
+val Infinitesimal_interval = thm "Infinitesimal_interval";
+val Infinitesimal_interval2 = thm "Infinitesimal_interval2";
+val not_Infinitesimal_mult = thm "not_Infinitesimal_mult";
+val Infinitesimal_mult_disj = thm "Infinitesimal_mult_disj";
+val HFinite_Infinitesimal_not_zero = thm "HFinite_Infinitesimal_not_zero";
+val HFinite_Infinitesimal_diff_mult = thm "HFinite_Infinitesimal_diff_mult";
+val Infinitesimal_subset_HFinite = thm "Infinitesimal_subset_HFinite";
+val Infinitesimal_hypreal_of_real_mult = thm "Infinitesimal_hypreal_of_real_mult";
+val Infinitesimal_hypreal_of_real_mult2 = thm "Infinitesimal_hypreal_of_real_mult2";
+val mem_infmal_iff = thm "mem_infmal_iff";
+val approx_minus_iff = thm "approx_minus_iff";
+val approx_minus_iff2 = thm "approx_minus_iff2";
+val approx_refl = thm "approx_refl";
+val approx_sym = thm "approx_sym";
+val approx_trans = thm "approx_trans";
+val approx_trans2 = thm "approx_trans2";
+val approx_trans3 = thm "approx_trans3";
+val number_of_approx_reorient = thm "number_of_approx_reorient";
+val zero_approx_reorient = thm "zero_approx_reorient";
+val one_approx_reorient = thm "one_approx_reorient";
+
+(*** re-orientation, following HOL/Integ/Bin.ML
+ We re-orient x @=y where x is 0, 1 or a numeral, unless y is as well!
+ ***)
+
+(*reorientation simprules using ==, for the following simproc*)
+val meta_zero_approx_reorient = zero_approx_reorient RS eq_reflection;
+val meta_one_approx_reorient = one_approx_reorient RS eq_reflection;
+val meta_number_of_approx_reorient = number_of_approx_reorient RS eq_reflection
+
+(*reorientation simplification procedure: reorients (polymorphic)
+ 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
+fun reorient_proc sg _ (_ $ t $ u) =
+ case u of
+ Const("0", _) => None
+ | Const("1", _) => None
+ | Const("Numeral.number_of", _) $ _ => None
+ | _ => Some (case t of
+ Const("0", _) => meta_zero_approx_reorient
+ | Const("1", _) => meta_one_approx_reorient
+ | Const("Numeral.number_of", _) $ _ =>
+ meta_number_of_approx_reorient);
+
+val approx_reorient_simproc =
+ Bin_Simprocs.prep_simproc
+ ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
+
+Addsimprocs [approx_reorient_simproc];
+*}
+
+lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)"
+by (auto simp add: hypreal_diff_def approx_minus_iff [symmetric] mem_infmal_iff)
+
+lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))"
+apply (simp add: monad_def)
+apply (auto dest: approx_sym elim!: approx_trans equalityCE)
+done
+
+lemma Infinitesimal_approx: "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x @= y"
+apply (simp add: mem_infmal_iff)
+apply (blast intro: approx_trans approx_sym)
+done
+
+lemma approx_add: "[| a @= b; c @= d |] ==> a+c @= b+d"
+proof (unfold approx_def)
+ assume inf: "a + - b \<in> Infinitesimal" "c + - d \<in> Infinitesimal"
+ have "a + c + - (b + d) = (a + - b) + (c + - d)" by arith
+ also have "... \<in> Infinitesimal" using inf by (rule Infinitesimal_add)
+ finally show "a + c + - (b + d) \<in> Infinitesimal" .
+qed
+
+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)
+done
+
+lemma approx_minus2: "-a @= -b ==> a @= b"
+by (auto dest: approx_minus)
+
+lemma approx_minus_cancel: "(-a @= -b) = (a @= b)"
+by (blast intro: approx_minus approx_minus2)
+
+declare approx_minus_cancel [simp]
+
+lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d"
+by (blast intro!: approx_add approx_minus)
+
+lemma approx_mult1: "[| a @= b; c: HFinite|] ==> a*c @= b*c"
+by (simp add: approx_def Infinitesimal_HFinite_mult minus_mult_left
+ left_distrib [symmetric]
+ del: minus_mult_left [symmetric])
+
+lemma approx_mult2: "[|a @= b; c: HFinite|] ==> c*a @= c*b"
+apply (simp (no_asm_simp) add: approx_mult1 hypreal_mult_commute)
+done
+
+lemma approx_mult_subst: "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"
+by (blast intro: approx_mult2 approx_trans)
+
+lemma approx_mult_subst2: "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v"
+by (blast intro: approx_mult1 approx_trans)
+
+lemma approx_mult_subst_SReal: "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v"
+by (auto intro: approx_mult_subst2)
+
+lemma approx_eq_imp: "a = b ==> a @= b"
+by (simp add: approx_def)
+
+lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x @= x"
+by (blast intro: Infinitesimal_minus_iff [THEN iffD2]
+ mem_infmal_iff [THEN iffD1] approx_trans2)
+
+lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x + -z = y) = (x @= z)"
+by (simp add: approx_def)
+
+lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x @= z)"
+by (force simp add: bex_Infinitesimal_iff [symmetric])
+
+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: minus_add_distrib hypreal_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: minus_add_distrib hypreal_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)
+
+lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal ==> x @= x + -y"
+by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2])
+
+lemma Infinitesimal_add_cancel: "[| y \<in> Infinitesimal; x+y @= z|] ==> x @= z"
+apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym])
+apply (erule approx_trans3 [THEN approx_sym], assumption)
+done
+
+lemma Infinitesimal_add_right_cancel: "[| 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 (erule approx_sym)
+done
+
+lemma approx_add_left_cancel: "d + b @= d + c ==> b @= c"
+apply (drule approx_minus_iff [THEN iffD1])
+apply (simp add: minus_add_distrib approx_minus_iff [symmetric] add_ac)
+done
+
+lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c"
+apply (rule approx_add_left_cancel)
+apply (simp add: hypreal_add_commute)
+done
+
+lemma approx_add_mono1: "b @= c ==> d + b @= d + c"
+apply (rule approx_minus_iff [THEN iffD2])
+apply (simp add: minus_add_distrib approx_minus_iff [symmetric] add_ac)
+done
+
+lemma approx_add_mono2: "b @= c ==> b + a @= c + a"
+apply (simp (no_asm_simp) add: hypreal_add_commute approx_add_mono1)
+done
+
+lemma approx_add_left_iff: "(a + b @= a + c) = (b @= c)"
+by (fast elim: approx_add_left_cancel approx_add_mono1)
+
+declare approx_add_left_iff [simp]
+
+lemma approx_add_right_iff: "(b + a @= c + a) = (b @= c)"
+apply (simp (no_asm) add: hypreal_add_commute)
+done
+
+declare approx_add_right_iff [simp]
+
+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)
+done
+
+lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \<in> HFinite"
+by (rule approx_sym [THEN [2] approx_HFinite], auto)
+
+lemma approx_mult_HFinite: "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
+apply (rule approx_trans)
+apply (rule_tac [2] approx_mult2)
+apply (rule approx_mult1)
+prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)
+done
+
+lemma approx_mult_hypreal_of_real: "[|a @= hypreal_of_real b; c @= hypreal_of_real d |]
+ ==> a*c @= hypreal_of_real b*hypreal_of_real d"
+apply (blast intro!: approx_mult_HFinite approx_hypreal_of_real_HFinite HFinite_hypreal_of_real)
+done
+
+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])
+done
+
+(* REM comments: newly added *)
+lemma approx_mult_SReal1: "[| a \<in> Reals; x @= 0 |] ==> x*a @= 0"
+by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)
+
+lemma approx_mult_SReal2: "[| a \<in> Reals; x @= 0 |] ==> a*x @= 0"
+by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
+
+lemma approx_mult_SReal_zero_cancel_iff: "[|a \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
+by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
+declare approx_mult_SReal_zero_cancel_iff [simp]
+
+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])
+done
+
+lemma approx_SReal_mult_cancel_iff1: "[| a \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
+by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD] intro: approx_SReal_mult_cancel)
+declare approx_SReal_mult_cancel_iff1 [simp]
+
+lemma approx_le_bound: "[| z <= f; f @= g; g <= z |] ==> f @= z"
+apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
+apply (rule_tac x = "g+y-z" in bexI)
+apply (simp (no_asm))
+apply (rule Infinitesimal_interval2)
+apply (rule_tac [2] Infinitesimal_zero, auto)
+done
+
+(*-----------------------------------------------------------------
+ Zero is the only infinitesimal that is also a real
+ -----------------------------------------------------------------*)
+
+lemma Infinitesimal_less_SReal:
+ "[| x \<in> Reals; y \<in> Infinitesimal; 0 < x |] ==> y < x"
+apply (simp add: Infinitesimal_def)
+apply (rule abs_ge_self [THEN order_le_less_trans], auto)
+done
+
+lemma Infinitesimal_less_SReal2: "y \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> y < r"
+by (blast intro: Infinitesimal_less_SReal)
+
+lemma SReal_not_Infinitesimal:
+ "[| 0 < y; y \<in> Reals|] ==> y \<notin> Infinitesimal"
+apply (simp add: Infinitesimal_def)
+apply (auto simp add: hrabs_def)
+done
+
+lemma SReal_minus_not_Infinitesimal: "[| y < 0; y \<in> Reals |] ==> y \<notin> Infinitesimal"
+apply (subst Infinitesimal_minus_iff [symmetric])
+apply (rule SReal_not_Infinitesimal, auto)
+done
+
+lemma SReal_Int_Infinitesimal_zero: "Reals Int Infinitesimal = {0}"
+apply auto
+apply (cut_tac x = x and y = 0 in linorder_less_linear)
+apply (blast dest: SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
+done
+
+lemma SReal_Infinitesimal_zero: "[| x \<in> Reals; x \<in> Infinitesimal|] ==> x = 0"
+by (cut_tac SReal_Int_Infinitesimal_zero, blast)
+
+lemma SReal_HFinite_diff_Infinitesimal: "[| x \<in> Reals; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
+by (auto dest: SReal_Infinitesimal_zero SReal_subset_HFinite [THEN subsetD])
+
+lemma hypreal_of_real_HFinite_diff_Infinitesimal: "hypreal_of_real x \<noteq> 0 ==> hypreal_of_real x \<in> HFinite - Infinitesimal"
+by (rule SReal_HFinite_diff_Infinitesimal, auto)
+
+lemma hypreal_of_real_Infinitesimal_iff_0: "(hypreal_of_real x \<in> Infinitesimal) = (x=0)"
+apply auto
+apply (rule ccontr)
+apply (rule hypreal_of_real_HFinite_diff_Infinitesimal [THEN DiffD2], auto)
+done
+declare hypreal_of_real_Infinitesimal_iff_0 [iff]
+
+lemma number_of_not_Infinitesimal: "number_of w \<noteq> (0::hypreal) ==> number_of w \<notin> Infinitesimal"
+by (fast dest: SReal_number_of [THEN SReal_Infinitesimal_zero])
+declare number_of_not_Infinitesimal [simp]
+
+(*again: 1 is a special case, but not 0 this time*)
+lemma one_not_Infinitesimal: "1 \<notin> Infinitesimal"
+apply (subst hypreal_numeral_1_eq_1 [symmetric])
+apply (rule number_of_not_Infinitesimal)
+apply (simp (no_asm))
+done
+declare one_not_Infinitesimal [simp]
+
+lemma approx_SReal_not_zero: "[| y \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
+apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
+apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
+done
+
+lemma HFinite_diff_Infinitesimal_approx: "[| x @= y; y \<in> HFinite - Infinitesimal |]
+ ==> x \<in> HFinite - Infinitesimal"
+apply (auto intro: approx_sym [THEN [2] approx_HFinite]
+ simp add: mem_infmal_iff)
+apply (drule approx_trans3, assumption)
+apply (blast dest: approx_sym)
+done
+
+(*The premise y\<noteq>0 is essential; otherwise x/y =0 and we lose the
+ HFinite premise.*)
+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)
+done
+
+(*------------------------------------------------------------------
+ Standard Part Theorem: Every finite x: R* is infinitely
+ close to a unique real number (i.e a member of Reals)
+ ------------------------------------------------------------------*)
+(*------------------------------------------------------------------
+ Uniqueness: Two infinitely close reals are equal
+ ------------------------------------------------------------------*)
+
+lemma SReal_approx_iff: "[|x \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
+apply auto
+apply (simp add: approx_def)
+apply (drule_tac x = y in SReal_minus)
+apply (drule SReal_add, assumption)
+apply (drule SReal_Infinitesimal_zero, assumption)
+apply (drule sym)
+apply (simp add: hypreal_eq_minus_iff [symmetric])
+done
+
+lemma number_of_approx_iff: "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))"
+by (auto simp add: SReal_approx_iff)
+declare number_of_approx_iff [simp]
+
+(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
+lemma [simp]: "(0 @= number_of w) = ((number_of w :: hypreal) = 0)"
+ "(number_of w @= 0) = ((number_of w :: hypreal) = 0)"
+ "(1 @= number_of w) = ((number_of w :: hypreal) = 1)"
+ "(number_of w @= 1) = ((number_of w :: hypreal) = 1)"
+ "~ (0 @= 1)" "~ (1 @= 0)"
+by (auto simp only: SReal_number_of SReal_approx_iff Reals_0 Reals_1)
+
+lemma hypreal_of_real_approx_iff: "(hypreal_of_real k @= hypreal_of_real m) = (k = m)"
+apply auto
+apply (rule inj_hypreal_of_real [THEN injD])
+apply (rule SReal_approx_iff [THEN iffD1], auto)
+done
+declare hypreal_of_real_approx_iff [simp]
+
+lemma hypreal_of_real_approx_number_of_iff: "(hypreal_of_real k @= number_of w) = (k = number_of w)"
+by (subst hypreal_of_real_approx_iff [symmetric], auto)
+declare hypreal_of_real_approx_number_of_iff [simp]
+
+(*And also for 0 and 1.*)
+(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
+lemma [simp]: "(hypreal_of_real k @= 0) = (k = 0)"
+ "(hypreal_of_real k @= 1) = (k = 1)"
+ by (simp_all add: hypreal_of_real_approx_iff [symmetric])
+
+lemma approx_unique_real: "[| r \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
+by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
+
+(*------------------------------------------------------------------
+ Existence of unique real infinitely close
+ ------------------------------------------------------------------*)
+(* lemma about lubs *)
+lemma hypreal_isLub_unique:
+ "[| 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)
+done
+
+lemma lemma_st_part_ub: "x \<in> HFinite ==> \<exists>u. isUb Reals {s. s \<in> Reals & s < x} u"
+apply (drule HFiniteD, safe)
+apply (rule exI, rule isUbI)
+apply (auto intro: setleI isUbI simp add: abs_less_iff)
+done
+
+lemma lemma_st_part_nonempty: "x \<in> HFinite ==> \<exists>y. y \<in> {s. s \<in> Reals & s < x}"
+apply (drule HFiniteD, safe)
+apply (drule SReal_minus)
+apply (rule_tac x = "-t" in exI)
+apply (auto simp add: abs_less_iff)
+done
+
+lemma lemma_st_part_subset: "{s. s \<in> Reals & s < x} <= Reals"
+by auto
+
+lemma lemma_st_part_lub: "x \<in> HFinite ==> \<exists>t. isLub Reals {s. s \<in> Reals & s < x} t"
+by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty lemma_st_part_subset)
+
+lemma lemma_hypreal_le_left_cancel: "((t::hypreal) + r <= t) = (r <= 0)"
+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])
+done
+
+lemma lemma_st_part_le1: "[| x \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t;
+ r \<in> Reals; 0 < r |] ==> x <= t + r"
+apply (frule isLubD1a)
+apply (rule ccontr, drule linorder_not_le [THEN iffD2])
+apply (drule_tac x = t in SReal_add, assumption)
+apply (drule_tac y = "t + r" in isLubD1 [THEN setleD], auto)
+done
+
+lemma hypreal_setle_less_trans: "!!x::hypreal. [| S *<= x; x < y |] ==> S *<= y"
+apply (simp add: setle_def)
+apply (auto dest!: bspec order_le_less_trans intro: order_less_imp_le)
+done
+
+lemma hypreal_gt_isUb:
+ "!!x::hypreal. [| isUb R S x; x < y; y \<in> R |] ==> isUb R S y"
+apply (simp add: isUb_def)
+apply (blast intro: hypreal_setle_less_trans)
+done
+
+lemma lemma_st_part_gt_ub: "[| x \<in> HFinite; x < y; y \<in> Reals |]
+ ==> isUb Reals {s. s \<in> Reals & s < x} y"
+apply (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)
+done
+
+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])
+done
+
+lemma lemma_st_part_le2: "[| x \<in> HFinite;
+ isLub Reals {s. s \<in> Reals & s < x} t;
+ r \<in> Reals; 0 < r |]
+ ==> t + -r <= x"
+apply (frule isLubD1a)
+apply (rule ccontr, drule linorder_not_le [THEN iffD1])
+apply (drule SReal_minus, drule_tac x = t in SReal_add, assumption)
+apply (drule lemma_st_part_gt_ub, assumption+)
+apply (drule isLub_le_isUb, assumption)
+apply (drule lemma_minus_le_zero)
+apply (auto dest: order_less_le_trans)
+done
+
+lemma lemma_hypreal_le_swap: "((x::hypreal) <= t + r) = (x + -t <= r)"
+by auto
+
+lemma lemma_st_part1a: "[| x \<in> HFinite;
+ isLub Reals {s. s \<in> Reals & s < x} t;
+ r \<in> Reals; 0 < r |]
+ ==> x + -t <= r"
+apply (blast intro!: lemma_hypreal_le_swap [THEN iffD1] lemma_st_part_le1)
+done
+
+lemma lemma_hypreal_le_swap2: "(t + -r <= x) = (-(x + -t) <= (r::hypreal))"
+by auto
+
+lemma lemma_st_part2a: "[| x \<in> HFinite;
+ isLub Reals {s. s \<in> Reals & s < x} t;
+ r \<in> Reals; 0 < r |]
+ ==> -(x + -t) <= r"
+apply (blast intro!: lemma_hypreal_le_swap2 [THEN iffD1] lemma_st_part_le2)
+done
+
+lemma lemma_SReal_ub: "(x::hypreal) \<in> Reals ==> isUb Reals {s. s \<in> Reals & s < x} x"
+by (auto intro: isUbI setleI order_less_imp_le)
+
+lemma lemma_SReal_lub: "(x::hypreal) \<in> Reals ==> isLub Reals {s. s \<in> Reals & s < x} x"
+apply (auto intro!: isLubI2 lemma_SReal_ub setgeI)
+apply (frule isUbD2a)
+apply (rule_tac x = x and y = y in linorder_cases)
+apply (auto intro!: order_less_imp_le)
+apply (drule SReal_dense, assumption, assumption, safe)
+apply (drule_tac y = r in isUbD)
+apply (auto dest: order_less_le_trans)
+done
+
+lemma lemma_st_part_not_eq1: "[| x \<in> HFinite;
+ isLub Reals {s. s \<in> Reals & s < x} t;
+ r \<in> Reals; 0 < r |]
+ ==> x + -t \<noteq> r"
+apply auto
+apply (frule isLubD1a [THEN SReal_minus])
+apply (drule SReal_add_cancel, assumption)
+apply (drule_tac x = x in lemma_SReal_lub)
+apply (drule hypreal_isLub_unique, assumption, auto)
+done
+
+lemma lemma_st_part_not_eq2: "[| x \<in> HFinite;
+ isLub Reals {s. s \<in> Reals & s < x} t;
+ r \<in> Reals; 0 < r |]
+ ==> -(x + -t) \<noteq> r"
+apply (auto simp add: minus_add_distrib)
+apply (frule isLubD1a)
+apply (drule SReal_add_cancel, assumption)
+apply (drule_tac x = "-x" in SReal_minus, simp)
+apply (drule_tac x = x in lemma_SReal_lub)
+apply (drule hypreal_isLub_unique, assumption, auto)
+done
+
+lemma lemma_st_part_major: "[| x \<in> HFinite;
+ isLub Reals {s. s \<in> Reals & s < x} t;
+ r \<in> Reals; 0 < r |]
+ ==> abs (x + -t) < r"
+apply (frule lemma_st_part1a)
+apply (frule_tac [4] lemma_st_part2a, auto)
+apply (drule order_le_imp_less_or_eq)+
+apply (auto dest: lemma_st_part_not_eq1 lemma_st_part_not_eq2 simp add: abs_less_iff)
+done
+
+lemma lemma_st_part_major2: "[| x \<in> HFinite;
+ isLub Reals {s. s \<in> Reals & s < x} t |]
+ ==> \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
+apply (blast dest!: lemma_st_part_major)
+done
+
+(*----------------------------------------------
+ Existence of real and Standard Part Theorem
+ ----------------------------------------------*)
+lemma lemma_st_part_Ex: "x \<in> HFinite ==>
+ \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
+apply (frule lemma_st_part_lub, safe)
+apply (frule isLubD1a)
+apply (blast dest: lemma_st_part_major2)
+done
+
+lemma st_part_Ex:
+ "x \<in> HFinite ==> \<exists>t \<in> Reals. x @= t"
+apply (simp add: approx_def Infinitesimal_def)
+apply (drule lemma_st_part_Ex, auto)
+done
+
+(*--------------------------------
+ Unique real infinitely close
+ -------------------------------*)
+lemma st_part_Ex1: "x \<in> HFinite ==> EX! t. t \<in> Reals & x @= t"
+apply (drule st_part_Ex, safe)
+apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
+apply (auto intro!: approx_unique_real)
+done
+
+(*------------------------------------------------------------------
+ Finite and Infinite --- more theorems
+ ------------------------------------------------------------------*)
+
+lemma HFinite_Int_HInfinite_empty: "HFinite Int HInfinite = {}"
+
+apply (simp add: HFinite_def HInfinite_def)
+apply (auto dest: order_less_trans)
+done
+declare HFinite_Int_HInfinite_empty [simp]
+
+lemma HFinite_not_HInfinite:
+ assumes x: "x \<in> HFinite" shows "x \<notin> HInfinite"
+proof
+ assume x': "x \<in> HInfinite"
+ with x have "x \<in> HFinite \<inter> HInfinite" by blast
+ thus False by auto
+qed
+
+lemma not_HFinite_HInfinite: "x\<notin> HFinite ==> x \<in> HInfinite"
+apply (simp add: HInfinite_def HFinite_def, auto)
+apply (drule_tac x = "r + 1" in bspec)
+apply (auto simp add: SReal_add)
+done
+
+lemma HInfinite_HFinite_disj: "x \<in> HInfinite | x \<in> HFinite"
+by (blast intro: not_HFinite_HInfinite)
+
+lemma HInfinite_HFinite_iff: "(x \<in> HInfinite) = (x \<notin> HFinite)"
+by (blast dest: HFinite_not_HInfinite not_HFinite_HInfinite)
+
+lemma HFinite_HInfinite_iff: "(x \<in> HFinite) = (x \<notin> HInfinite)"
+apply (simp (no_asm) add: HInfinite_HFinite_iff)
+done
+
+(*------------------------------------------------------------------
+ Finite, Infinite and Infinitesimal --- more theorems
+ ------------------------------------------------------------------*)
+
+lemma HInfinite_diff_HFinite_Infinitesimal_disj: "x \<notin> Infinitesimal ==> x \<in> HInfinite | x \<in> HFinite - Infinitesimal"
+by (fast intro: not_HFinite_HInfinite)
+
+lemma HFinite_inverse: "[| x \<in> HFinite; x \<notin> Infinitesimal |] ==> inverse x \<in> HFinite"
+apply (cut_tac x = "inverse x" in HInfinite_HFinite_disj)
+apply (auto dest!: HInfinite_inverse_Infinitesimal)
+done
+
+lemma HFinite_inverse2: "x \<in> HFinite - Infinitesimal ==> inverse x \<in> HFinite"
+by (blast intro: HFinite_inverse)
+
+(* stronger statement possible in fact *)
+lemma Infinitesimal_inverse_HFinite: "x \<notin> Infinitesimal ==> inverse(x) \<in> HFinite"
+apply (drule HInfinite_diff_HFinite_Infinitesimal_disj)
+apply (blast intro: HFinite_inverse HInfinite_inverse_Infinitesimal Infinitesimal_subset_HFinite [THEN subsetD])
+done
+
+lemma HFinite_not_Infinitesimal_inverse: "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)
+done
+
+lemma approx_inverse: "[| x @= y; y \<in> HFinite - Infinitesimal |]
+ ==> inverse x @= inverse y"
+apply (frule HFinite_diff_Infinitesimal_approx, assumption)
+apply (frule not_Infinitesimal_not_zero2)
+apply (frule_tac x = x in not_Infinitesimal_not_zero2)
+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)
+done
+
+(*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
+lemmas hypreal_of_real_approx_inverse = hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
+
+lemma inverse_add_Infinitesimal_approx: "[| x \<in> HFinite - Infinitesimal;
+ h \<in> Infinitesimal |] ==> inverse(x + h) @= inverse x"
+apply (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self)
+done
+
+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 (blast intro: inverse_add_Infinitesimal_approx)
+done
+
+lemma inverse_add_Infinitesimal_approx_Infinitesimal: "[| x \<in> HFinite - Infinitesimal;
+ h \<in> Infinitesimal |] ==> inverse(x + h) + -inverse x @= h"
+apply (rule approx_trans2)
+apply (auto intro: inverse_add_Infinitesimal_approx simp add: mem_infmal_iff approx_minus_iff [symmetric])
+done
+
+lemma Infinitesimal_square_iff: "(x \<in> Infinitesimal) = (x*x \<in> Infinitesimal)"
+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)
+done
+declare Infinitesimal_square_iff [symmetric, simp]
+
+lemma HFinite_square_iff: "(x*x \<in> HFinite) = (x \<in> HFinite)"
+apply (auto intro: HFinite_mult)
+apply (auto dest: HInfinite_mult simp add: HFinite_HInfinite_iff)
+done
+declare HFinite_square_iff [simp]
+
+lemma HInfinite_square_iff: "(x*x \<in> HInfinite) = (x \<in> HInfinite)"
+by (auto simp add: HInfinite_HFinite_iff)
+declare HInfinite_square_iff [simp]
+
+lemma approx_HFinite_mult_cancel: "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
+apply safe
+apply (frule HFinite_inverse, assumption)
+apply (drule not_Infinitesimal_not_zero)
+apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric])
+done
+
+lemma approx_HFinite_mult_cancel_iff1: "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
+by (auto intro: approx_mult2 approx_HFinite_mult_cancel)
+
+lemma HInfinite_HFinite_add_cancel: "[| x + y \<in> HInfinite; y \<in> HFinite |] ==> x \<in> HInfinite"
+apply (rule ccontr)
+apply (drule HFinite_HInfinite_iff [THEN iffD2])
+apply (auto dest: HFinite_add simp add: HInfinite_HFinite_iff)
+done
+
+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)
+done
+
+lemma HInfinite_ge_HInfinite: "[| x \<in> HInfinite; x <= y; 0 <= x |] ==> y \<in> HInfinite"
+by (auto intro: HFinite_bounded simp add: HInfinite_HFinite_iff)
+
+lemma Infinitesimal_inverse_HInfinite: "[| x \<in> Infinitesimal; x \<noteq> 0 |] ==> inverse x \<in> HInfinite"
+apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
+apply (auto dest: Infinitesimal_HFinite_mult2)
+done
+
+lemma HInfinite_HFinite_not_Infinitesimal_mult: "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
+ ==> x * y \<in> HInfinite"
+apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
+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)
+done
+
+lemma HInfinite_HFinite_not_Infinitesimal_mult2: "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
+ ==> y * x \<in> HInfinite"
+apply (auto simp add: hypreal_mult_commute HInfinite_HFinite_not_Infinitesimal_mult)
+done
+
+lemma HInfinite_gt_SReal: "[| x \<in> HInfinite; 0 < x; y \<in> Reals |] ==> y < x"
+by (auto dest!: bspec simp add: HInfinite_def hrabs_def order_less_imp_le)
+
+lemma HInfinite_gt_zero_gt_one: "[| x \<in> HInfinite; 0 < x |] ==> 1 < x"
+by (auto intro: HInfinite_gt_SReal)
+
+
+lemma not_HInfinite_one: "1 \<notin> HInfinite"
+apply (simp (no_asm) add: HInfinite_HFinite_iff)
+done
+declare not_HInfinite_one [simp]
+
+(*------------------------------------------------------------------
+ more about absolute value (hrabs)
+ ------------------------------------------------------------------*)
+
+lemma approx_hrabs_disj: "abs x @= x | abs x @= -x"
+by (cut_tac x = x in hrabs_disj, auto)
+
+(*------------------------------------------------------------------
+ Theorems about monads
+ ------------------------------------------------------------------*)
+
+lemma monad_hrabs_Un_subset: "monad (abs x) <= monad(x) Un monad(-x)"
+by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto)
+
+lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal ==> monad (x+e) = monad x"
+by (fast intro!: Infinitesimal_add_approx_self [THEN approx_sym] approx_monad_iff [THEN iffD1])
+
+lemma mem_monad_iff: "(u \<in> monad x) = (-u \<in> monad (-x))"
+by (simp add: monad_def)
+
+lemma Infinitesimal_monad_zero_iff: "(x \<in> Infinitesimal) = (x \<in> monad 0)"
+by (auto intro: approx_sym simp add: monad_def mem_infmal_iff)
+
+lemma monad_zero_minus_iff: "(x \<in> monad 0) = (-x \<in> monad 0)"
+apply (simp (no_asm) add: Infinitesimal_monad_zero_iff [symmetric])
+done
+
+lemma monad_zero_hrabs_iff: "(x \<in> monad 0) = (abs x \<in> monad 0)"
+apply (rule_tac x1 = x in hrabs_disj [THEN disjE])
+apply (auto simp add: monad_zero_minus_iff [symmetric])
+done
+
+lemma mem_monad_self: "x \<in> monad x"
+by (simp add: monad_def)
+declare mem_monad_self [simp]
+
+(*------------------------------------------------------------------
+ Proof that x @= y ==> abs x @= abs y
+ ------------------------------------------------------------------*)
+lemma approx_subset_monad: "x @= y ==> {x,y}<=monad x"
+apply (simp (no_asm))
+apply (simp add: approx_monad_iff)
+done
+
+lemma approx_subset_monad2: "x @= y ==> {x,y}<=monad y"
+apply (drule approx_sym)
+apply (fast dest: approx_subset_monad)
+done
+
+lemma mem_monad_approx: "u \<in> monad x ==> x @= u"
+by (simp add: monad_def)
+
+lemma approx_mem_monad: "x @= u ==> u \<in> monad x"
+by (simp add: monad_def)
+
+lemma approx_mem_monad2: "x @= u ==> x \<in> monad u"
+apply (simp add: monad_def)
+apply (blast intro!: approx_sym)
+done
+
+lemma approx_mem_monad_zero: "[| x @= y;x \<in> monad 0 |] ==> y \<in> monad 0"
+apply (drule mem_monad_approx)
+apply (fast intro: approx_mem_monad approx_trans)
+done
+
+lemma Infinitesimal_approx_hrabs: "[| x @= y; x \<in> Infinitesimal |] ==> abs x @= abs y"
+apply (drule Infinitesimal_monad_zero_iff [THEN iffD1])
+apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] mem_monad_approx approx_trans3)
+done
+
+lemma less_Infinitesimal_less: "[| 0 < x; x \<notin>Infinitesimal; e :Infinitesimal |] ==> e < x"
+apply (rule ccontr)
+apply (auto intro: Infinitesimal_zero [THEN [2] Infinitesimal_interval]
+ dest!: order_le_imp_less_or_eq simp add: linorder_not_less)
+done
+
+lemma Ball_mem_monad_gt_zero: "[| 0 < x; x \<notin> Infinitesimal; u \<in> monad x |] ==> 0 < u"
+apply (drule mem_monad_approx [THEN approx_sym])
+apply (erule bex_Infinitesimal_iff2 [THEN iffD2, THEN bexE])
+apply (drule_tac e = "-xa" in less_Infinitesimal_less, auto)
+done
+
+lemma Ball_mem_monad_less_zero: "[| x < 0; x \<notin> Infinitesimal; u \<in> monad x |] ==> u < 0"
+apply (drule mem_monad_approx [THEN approx_sym])
+apply (erule bex_Infinitesimal_iff [THEN iffD2, THEN bexE])
+apply (cut_tac x = "-x" and e = xa in less_Infinitesimal_less, auto)
+done
+
+lemma lemma_approx_gt_zero: "[|0 < x; x \<notin> Infinitesimal; x @= y|] ==> 0 < y"
+by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad)
+
+lemma lemma_approx_less_zero: "[|x < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
+by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
+
+lemma approx_hrabs1: "[| x @= y; x < 0; x \<notin> Infinitesimal |] ==> abs x @= abs y"
+apply (frule lemma_approx_less_zero)
+apply (assumption+)
+apply (simp add: abs_if)
+done
+
+lemma approx_hrabs2: "[| x @= y; 0 < x; x \<notin> Infinitesimal |] ==> abs x @= abs y"
+apply (frule lemma_approx_gt_zero)
+apply (assumption+)
+apply (simp add: abs_if)
+done
+
+lemma approx_hrabs: "x @= y ==> abs x @= abs y"
+apply (rule_tac Q = "x \<in> Infinitesimal" in excluded_middle [THEN disjE])
+apply (rule_tac x1 = x and y1 = 0 in linorder_less_linear [THEN disjE])
+apply (auto intro: approx_hrabs1 approx_hrabs2 Infinitesimal_approx_hrabs)
+done
+
+lemma approx_hrabs_zero_cancel: "abs(x) @= 0 ==> x @= 0"
+apply (cut_tac x = x in hrabs_disj)
+apply (auto dest: approx_minus)
+done
+
+lemma approx_hrabs_add_Infinitesimal: "e \<in> Infinitesimal ==> abs x @= abs(x+e)"
+by (fast intro: approx_hrabs Infinitesimal_add_approx_self)
+
+lemma approx_hrabs_add_minus_Infinitesimal: "e \<in> Infinitesimal ==> abs x @= abs(x + -e)"
+by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)
+
+lemma hrabs_add_Infinitesimal_cancel: "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
+ abs(x+e) = abs(y+e')|] ==> abs x @= abs y"
+apply (drule_tac x = x in approx_hrabs_add_Infinitesimal)
+apply (drule_tac x = y in approx_hrabs_add_Infinitesimal)
+apply (auto intro: approx_trans2)
+done
+
+lemma hrabs_add_minus_Infinitesimal_cancel: "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
+ abs(x + -e) = abs(y + -e')|] ==> abs x @= abs y"
+apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal)
+apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal)
+apply (auto intro: approx_trans2)
+done
+
+lemma hypreal_less_minus_iff: "((x::hypreal) < y) = (0 < y + -x)"
+by arith
- (*standard real numbers as a subset of the hyperreals*)
- SReal_def "Reals == {x. EX r. x = hypreal_of_real r}"
+(* interesting slightly counterintuitive theorem: necessary
+ for proving that an open interval is an NS open set
+*)
+lemma Infinitesimal_add_hypreal_of_real_less:
+ "[| x < y; u \<in> Infinitesimal |]
+ ==> hypreal_of_real x + u < hypreal_of_real y"
+apply (simp add: Infinitesimal_def)
+apply (drule hypreal_of_real_less_iff [THEN iffD2])
+apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec)
+apply (auto simp add: hypreal_add_commute abs_less_iff SReal_add SReal_minus)
+done
+
+lemma Infinitesimal_add_hrabs_hypreal_of_real_less: "[| x \<in> Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |]
+ ==> abs (hypreal_of_real r + x) < hypreal_of_real y"
+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 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 (erule Infinitesimal_add_hrabs_hypreal_of_real_less, assumption)
+done
+
+lemma hypreal_of_real_le_add_Infininitesimal_cancel: "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
+ hypreal_of_real x + u <= hypreal_of_real y + v |]
+ ==> hypreal_of_real x <= hypreal_of_real y"
+apply (simp add: linorder_not_less [symmetric], auto)
+apply (drule_tac u = "v-u" in Infinitesimal_add_hypreal_of_real_less)
+apply (auto simp add: Infinitesimal_diff)
+done
+
+lemma hypreal_of_real_le_add_Infininitesimal_cancel2: "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
+ hypreal_of_real x + u <= hypreal_of_real y + v |]
+ ==> x <= y"
+apply (blast intro!: hypreal_of_real_le_iff [THEN iffD1] hypreal_of_real_le_add_Infininitesimal_cancel)
+done
+
+lemma hypreal_of_real_less_Infinitesimal_le_zero: "[| hypreal_of_real x < e; e \<in> Infinitesimal |] ==> hypreal_of_real x <= 0"
+apply (rule linorder_not_less [THEN iffD1], safe)
+apply (drule Infinitesimal_interval)
+apply (drule_tac [4] SReal_hypreal_of_real [THEN SReal_Infinitesimal_zero], auto)
+done
+
+(*used once, in Lim/NSDERIV_inverse*)
+lemma Infinitesimal_add_not_zero: "[| h \<in> Infinitesimal; x \<noteq> 0 |] ==> hypreal_of_real x + h \<noteq> 0"
+apply auto
+apply (subgoal_tac "h = - hypreal_of_real x", auto)
+done
+
+lemma Infinitesimal_square_cancel: "x*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
+apply (rule Infinitesimal_interval2)
+apply (rule_tac [3] zero_le_square, assumption)
+apply (auto simp add: zero_le_square)
+done
+declare Infinitesimal_square_cancel [simp]
+
+lemma HFinite_square_cancel: "x*x + y*y \<in> HFinite ==> x*x \<in> HFinite"
+apply (rule HFinite_bounded, assumption)
+apply (auto simp add: zero_le_square)
+done
+declare HFinite_square_cancel [simp]
+
+lemma Infinitesimal_square_cancel2: "x*x + y*y \<in> Infinitesimal ==> y*y \<in> Infinitesimal"
+apply (rule Infinitesimal_square_cancel)
+apply (rule hypreal_add_commute [THEN subst])
+apply (simp (no_asm))
+done
+declare Infinitesimal_square_cancel2 [simp]
+
+lemma HFinite_square_cancel2: "x*x + y*y \<in> HFinite ==> y*y \<in> HFinite"
+apply (rule HFinite_square_cancel)
+apply (rule hypreal_add_commute [THEN subst])
+apply (simp (no_asm))
+done
+declare HFinite_square_cancel2 [simp]
+
+lemma Infinitesimal_sum_square_cancel: "x*x + y*y + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
+apply (rule Infinitesimal_interval2, assumption)
+apply (rule_tac [2] zero_le_square, simp)
+apply (insert zero_le_square [of y])
+apply (insert zero_le_square [of z], simp)
+done
+declare Infinitesimal_sum_square_cancel [simp]
+
+lemma HFinite_sum_square_cancel: "x*x + y*y + z*z \<in> HFinite ==> x*x \<in> HFinite"
+apply (rule HFinite_bounded, assumption)
+apply (rule_tac [2] zero_le_square)
+apply (insert zero_le_square [of y])
+apply (insert zero_le_square [of z], simp)
+done
+declare HFinite_sum_square_cancel [simp]
+
+lemma Infinitesimal_sum_square_cancel2: "y*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
+apply (rule Infinitesimal_sum_square_cancel)
+apply (simp add: add_ac)
+done
+declare Infinitesimal_sum_square_cancel2 [simp]
+
+lemma HFinite_sum_square_cancel2: "y*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite"
+apply (rule HFinite_sum_square_cancel)
+apply (simp add: add_ac)
+done
+declare HFinite_sum_square_cancel2 [simp]
+
+lemma Infinitesimal_sum_square_cancel3: "z*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
+apply (rule Infinitesimal_sum_square_cancel)
+apply (simp add: add_ac)
+done
+declare Infinitesimal_sum_square_cancel3 [simp]
+
+lemma HFinite_sum_square_cancel3: "z*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite"
+apply (rule HFinite_sum_square_cancel)
+apply (simp add: add_ac)
+done
+declare HFinite_sum_square_cancel3 [simp]
+
+lemma monad_hrabs_less: "[| y \<in> monad x; 0 < hypreal_of_real e |]
+ ==> abs (y + -x) < hypreal_of_real e"
+apply (drule mem_monad_approx [THEN approx_sym])
+apply (drule bex_Infinitesimal_iff [THEN iffD2])
+apply (auto dest!: InfinitesimalD)
+done
+
+lemma mem_monad_SReal_HFinite: "x \<in> monad (hypreal_of_real a) ==> x \<in> HFinite"
+apply (drule mem_monad_approx [THEN approx_sym])
+apply (drule bex_Infinitesimal_iff2 [THEN iffD2])
+apply (safe dest!: Infinitesimal_subset_HFinite [THEN subsetD])
+apply (erule SReal_hypreal_of_real [THEN SReal_subset_HFinite [THEN subsetD], THEN HFinite_add])
+done
+
+(*------------------------------------------------------------------
+ Theorems about standard part
+ ------------------------------------------------------------------*)
+
+lemma st_approx_self: "x \<in> HFinite ==> st x @= x"
+apply (simp add: st_def)
+apply (frule st_part_Ex, safe)
+apply (rule someI2)
+apply (auto intro: approx_sym)
+done
+
+lemma st_SReal: "x \<in> HFinite ==> st x \<in> Reals"
+apply (simp add: st_def)
+apply (frule st_part_Ex, safe)
+apply (rule someI2)
+apply (auto intro: approx_sym)
+done
+
+lemma st_HFinite: "x \<in> HFinite ==> st x \<in> HFinite"
+by (erule st_SReal [THEN SReal_subset_HFinite [THEN subsetD]])
+
+lemma st_SReal_eq: "x \<in> Reals ==> st x = x"
+apply (simp add: st_def)
+apply (rule some_equality)
+apply (fast intro: SReal_subset_HFinite [THEN subsetD])
+apply (blast dest: SReal_approx_iff [THEN iffD1])
+done
+
+(* ???should be added to simpset *)
+lemma st_hypreal_of_real: "st (hypreal_of_real x) = hypreal_of_real x"
+by (rule SReal_hypreal_of_real [THEN st_SReal_eq])
+
+lemma st_eq_approx: "[| x \<in> HFinite; y \<in> HFinite; st x = st y |] ==> x @= y"
+by (auto dest!: st_approx_self elim!: approx_trans3)
+
+lemma approx_st_eq:
+ assumes "x \<in> HFinite" and "y \<in> HFinite" and "x @= y"
+ shows "st x = st y"
+proof -
+ have "st x @= x" "st y @= y" "st x \<in> Reals" "st y \<in> Reals"
+ by (simp_all add: st_approx_self st_SReal prems)
+ with prems show ?thesis
+ by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1])
+qed
+
+lemma st_eq_approx_iff: "[| x \<in> HFinite; y \<in> HFinite|]
+ ==> (x @= y) = (st x = st y)"
+by (blast intro: approx_st_eq st_eq_approx)
+
+lemma st_Infinitesimal_add_SReal: "[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(x + e) = x"
+apply (frule st_SReal_eq [THEN subst])
+prefer 2 apply assumption
+apply (frule SReal_subset_HFinite [THEN subsetD])
+apply (frule Infinitesimal_subset_HFinite [THEN subsetD])
+apply (drule st_SReal_eq)
+apply (rule approx_st_eq)
+apply (auto intro: HFinite_add simp add: Infinitesimal_add_approx_self [THEN approx_sym])
+done
+
+lemma st_Infinitesimal_add_SReal2: "[| x \<in> Reals; e \<in> Infinitesimal |]
+ ==> st(e + x) = x"
+apply (rule hypreal_add_commute [THEN subst])
+apply (blast intro!: st_Infinitesimal_add_SReal)
+done
+
+lemma HFinite_st_Infinitesimal_add: "x \<in> HFinite ==>
+ \<exists>e \<in> Infinitesimal. x = st(x) + e"
+apply (blast dest!: st_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])
+done
+
+lemma st_add:
+ assumes x: "x \<in> HFinite" and y: "y \<in> HFinite"
+ shows "st (x + y) = st(x) + st(y)"
+proof -
+ from HFinite_st_Infinitesimal_add [OF x]
+ obtain ex where ex: "ex \<in> Infinitesimal" "st x + ex = x"
+ by (blast intro: sym)
+ from HFinite_st_Infinitesimal_add [OF y]
+ obtain ey where ey: "ey \<in> Infinitesimal" "st y + ey = y"
+ by (blast intro: sym)
+ have "st (x + y) = st ((st x + ex) + (st y + ey))"
+ by (simp add: ex ey)
+ also have "... = st ((ex + ey) + (st x + st y))" by (simp add: add_ac)
+ also have "... = st x + st y"
+ by (simp add: prems st_SReal SReal_add Infinitesimal_add
+ st_Infinitesimal_add_SReal2)
+ finally show ?thesis .
+qed
+
+lemma st_number_of: "st (number_of w) = number_of w"
+by (rule SReal_number_of [THEN st_SReal_eq])
+declare st_number_of [simp]
+
+(*the theorem above for the special cases of zero and one*)
+lemma [simp]: "st 0 = 0" "st 1 = 1"
+by (simp_all add: st_SReal_eq)
+
+lemma st_minus: assumes "y \<in> HFinite" shows "st(-y) = -st(y)"
+proof -
+ have "st (- y) + st y = 0"
+ by (simp add: prems st_add [symmetric] HFinite_minus_iff)
+ thus ?thesis by arith
+qed
+
+lemma st_diff:
+ "[| x \<in> HFinite; y \<in> HFinite |] ==> st (x-y) = st(x) - st(y)"
+apply (simp add: hypreal_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)
+done
+
+(* lemma *)
+lemma lemma_st_mult: "[| x \<in> HFinite; y \<in> HFinite;
+ e \<in> Infinitesimal;
+ ea \<in> Infinitesimal |]
+ ==> e*y + x*ea + e*ea \<in> Infinitesimal"
+apply (frule_tac x = e and y = y in Infinitesimal_HFinite_mult)
+apply (frule_tac [2] x = ea and y = x in Infinitesimal_HFinite_mult)
+apply (drule_tac [3] Infinitesimal_mult)
+apply (auto intro: Infinitesimal_add simp add: add_ac mult_ac)
+done
+
+lemma st_mult: "[| x \<in> HFinite; y \<in> HFinite |]
+ ==> st (x * y) = st(x) * st(y)"
+apply (frule HFinite_st_Infinitesimal_add)
+apply (frule_tac x = y in HFinite_st_Infinitesimal_add, safe)
+apply (subgoal_tac "st (x * y) = st ((st x + e) * (st y + ea))")
+apply (drule_tac [2] sym, drule_tac [2] sym)
+ prefer 2 apply simp
+apply (erule_tac V = "x = st x + e" in thin_rl)
+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 (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 (blast intro!: lemma_st_mult)
+done
+
+lemma st_Infinitesimal: "x \<in> Infinitesimal ==> st x = 0"
+apply (subst hypreal_numeral_0_eq_0 [symmetric])
+apply (rule st_number_of [THEN subst])
+apply (rule approx_st_eq)
+apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mem_infmal_iff [symmetric])
+done
+
+lemma st_not_Infinitesimal: "st(x) \<noteq> 0 ==> x \<notin> Infinitesimal"
+by (fast intro: st_Infinitesimal)
+
+lemma st_inverse: "[| x \<in> HFinite; st x \<noteq> 0 |]
+ ==> 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)
+done
+
+lemma st_divide: "[| x \<in> HFinite; y \<in> HFinite; st y \<noteq> 0 |]
+ ==> st(x/y) = (st x) / (st y)"
+apply (auto simp add: hypreal_divide_def st_mult st_not_Infinitesimal HFinite_inverse st_inverse)
+done
+declare st_divide [simp]
+
+lemma st_idempotent: "x \<in> HFinite ==> st(st(x)) = st(x)"
+by (blast intro: st_HFinite st_approx_self approx_st_eq)
+declare st_idempotent [simp]
+
+(*** lemmas ***)
+lemma Infinitesimal_add_st_less: "[| x \<in> HFinite; y \<in> HFinite;
+ u \<in> Infinitesimal; st x < st y
+ |] ==> st x + u < st y"
+apply (drule st_SReal)+
+apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: SReal_iff)
+done
+
+lemma Infinitesimal_add_st_le_cancel: "[| x \<in> HFinite; y \<in> HFinite;
+ u \<in> Infinitesimal; st x <= st y + u
+ |] ==> st x <= st y"
+apply (simp add: linorder_not_less [symmetric])
+apply (auto dest: Infinitesimal_add_st_less)
+done
+
+lemma st_le: "[| x \<in> HFinite; y \<in> HFinite; x <= y |] ==> st(x) <= st(y)"
+apply (frule HFinite_st_Infinitesimal_add)
+apply (rotate_tac 1)
+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])
+done
+
+lemma st_zero_le: "[| 0 <= x; x \<in> HFinite |] ==> 0 <= st x"
+apply (subst hypreal_numeral_0_eq_0 [symmetric])
+apply (rule st_number_of [THEN subst])
+apply (rule st_le, auto)
+done
+
+lemma st_zero_ge: "[| x <= 0; x \<in> HFinite |] ==> st x <= 0"
+apply (subst hypreal_numeral_0_eq_0 [symmetric])
+apply (rule st_number_of [THEN subst])
+apply (rule st_le, auto)
+done
+
+lemma st_hrabs: "x \<in> HFinite ==> abs(st x) = st(abs x)"
+apply (simp add: linorder_not_le st_zero_le abs_if st_minus
+ linorder_not_less)
+apply (auto dest!: st_zero_ge [OF order_less_imp_le])
+done
+
+
+
+(*--------------------------------------------------------------------
+ Alternative definitions for HFinite using Free ultrafilter
+ --------------------------------------------------------------------*)
+
+lemma FreeUltrafilterNat_Rep_hypreal: "[| X \<in> Rep_hypreal x; Y \<in> Rep_hypreal x |]
+ ==> {n. X n = Y n} \<in> FreeUltrafilterNat"
+apply (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
+done
+
+lemma HFinite_FreeUltrafilterNat:
+ "x \<in> HFinite
+ ==> \<exists>X \<in> Rep_hypreal x. \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat"
+apply (rule eq_Abs_hypreal [of x])
+apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x]
+ 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)
+done
+
+lemma FreeUltrafilterNat_HFinite:
+ "\<exists>X \<in> Rep_hypreal x.
+ \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat
+ ==> x \<in> HFinite"
+apply (rule eq_Abs_hypreal [of 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, ultra+)
+done
+
+lemma HFinite_FreeUltrafilterNat_iff: "(x \<in> HFinite) = (\<exists>X \<in> Rep_hypreal x.
+ \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
+apply (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
+done
+
+(*--------------------------------------------------------------------
+ Alternative definitions for HInfinite using Free ultrafilter
+ --------------------------------------------------------------------*)
+lemma lemma_Compl_eq: "- {n. (u::real) < abs (xa n)} = {n. abs (xa n) <= u}"
+by auto
+
+lemma lemma_Compl_eq2: "- {n. abs (xa n) < (u::real)} = {n. u <= abs (xa n)}"
+by auto
+
+lemma lemma_Int_eq1: "{n. abs (xa n) <= (u::real)} Int {n. u <= abs (xa n)}
+ = {n. abs(xa n) = u}"
+apply auto
+done
+
+lemma lemma_FreeUltrafilterNat_one: "{n. abs (xa n) = u} <= {n. abs (xa n) < u + (1::real)}"
+by auto
+
+(*-------------------------------------
+ Exclude this type of sets from free
+ ultrafilter for Infinite numbers!
+ -------------------------------------*)
+lemma FreeUltrafilterNat_const_Finite: "[| xa: Rep_hypreal x;
+ {n. abs (xa n) = u} \<in> FreeUltrafilterNat
+ |] ==> x \<in> HFinite"
+apply (rule FreeUltrafilterNat_HFinite)
+apply (rule_tac x = xa in bexI)
+apply (rule_tac x = "u + 1" in exI)
+apply (ultra, assumption)
+done
+
+lemma HInfinite_FreeUltrafilterNat:
+ "x \<in> HInfinite ==> \<exists>X \<in> Rep_hypreal x.
+ \<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat"
+apply (frule HInfinite_HFinite_iff [THEN iffD1])
+apply (cut_tac x = x in Rep_hypreal_nonempty)
+apply (auto simp del: Rep_hypreal_nonempty simp add: HFinite_FreeUltrafilterNat_iff Bex_def)
+apply (drule spec)+
+apply auto
+apply (drule_tac x = u in spec)
+apply (drule FreeUltrafilterNat_Compl_mem)+
+apply (drule FreeUltrafilterNat_Int, assumption)
+apply (simp add: lemma_Compl_eq lemma_Compl_eq2 lemma_Int_eq1)
+apply (auto dest: FreeUltrafilterNat_const_Finite simp
+ add: HInfinite_HFinite_iff [THEN iffD1])
+done
+
+(* yet more lemmas! *)
+lemma lemma_Int_HI: "{n. abs (Xa n) < u} Int {n. X n = Xa n}
+ <= {n. abs (X n) < (u::real)}"
+apply auto
+done
+
+lemma lemma_Int_HIa: "{n. u < abs (X n)} Int {n. abs (X n) < (u::real)} = {}"
+by (auto intro: order_less_asym)
+
+lemma FreeUltrafilterNat_HInfinite: "\<exists>X \<in> Rep_hypreal x. \<forall>u.
+ {n. u < abs (X n)} \<in> FreeUltrafilterNat
+ ==> x \<in> HInfinite"
+apply (rule HInfinite_HFinite_iff [THEN iffD2])
+apply (safe, drule HFinite_FreeUltrafilterNat, auto)
+apply (drule_tac x = u in spec)
+apply (drule FreeUltrafilterNat_Rep_hypreal, assumption)
+apply (drule_tac Y = "{n. X n = Xa n}" in FreeUltrafilterNat_Int, simp)
+apply (drule lemma_Int_HI [THEN [2] FreeUltrafilterNat_subset])
+apply (drule_tac Y = "{n. abs (X n) < u}" in FreeUltrafilterNat_Int)
+apply (auto simp add: lemma_Int_HIa FreeUltrafilterNat_empty)
+done
+
+lemma HInfinite_FreeUltrafilterNat_iff: "(x \<in> HInfinite) = (\<exists>X \<in> Rep_hypreal x.
+ \<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat)"
+apply (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
+done
+
+(*--------------------------------------------------------------------
+ Alternative definitions for Infinitesimal using Free ultrafilter
+ --------------------------------------------------------------------*)
+
-syntax (xsymbols)
- approx :: "[hypreal, hypreal] => bool" (infixl "\\<approx>" 50)
-
+lemma Infinitesimal_FreeUltrafilterNat:
+ "x \<in> Infinitesimal ==> \<exists>X \<in> Rep_hypreal x.
+ \<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 eq_Abs_hypreal [of x])
+apply (auto, rule bexI [OF _ lemma_hyprel_refl], safe)
+apply (drule hypreal_of_real_less_iff [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, ultra)
+done
+
+lemma FreeUltrafilterNat_Infinitesimal:
+ "\<exists>X \<in> Rep_hypreal x.
+ \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat
+ ==> x \<in> Infinitesimal"
+apply (simp add: Infinitesimal_def)
+apply (rule eq_Abs_hypreal [of 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, ultra+)
+done
+
+lemma Infinitesimal_FreeUltrafilterNat_iff: "(x \<in> Infinitesimal) = (\<exists>X \<in> Rep_hypreal x.
+ \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
+apply (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)
+done
+
+(*------------------------------------------------------------------------
+ Infinitesimals as smaller than 1/n for all n::nat (> 0)
+ ------------------------------------------------------------------------*)
+
+lemma lemma_Infinitesimal: "(\<forall>r. 0 < r --> x < r) = (\<forall>n. x < inverse(real (Suc n)))"
+apply (auto simp add: real_of_nat_Suc_gt_zero)
+apply (blast dest!: reals_Archimedean intro: order_less_trans)
+done
+
+lemma lemma_Infinitesimal2: "(\<forall>r \<in> Reals. 0 < r --> x < r) =
+ (\<forall>n. x < inverse(hypreal_of_nat (Suc n)))"
+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])
+prefer 2 apply assumption
+apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_def)
+apply (auto dest!: reals_Archimedean simp add: SReal_iff)
+apply (drule hypreal_of_real_less_iff [THEN iffD2])
+apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_def)
+apply (blast intro: order_less_trans)
+done
+
+lemma Infinitesimal_hypreal_of_nat_iff:
+ "Infinitesimal = {x. \<forall>n. abs x < inverse (hypreal_of_nat (Suc n))}"
+apply (simp add: Infinitesimal_def)
+apply (auto simp add: lemma_Infinitesimal2)
+done
+
+
+(*-------------------------------------------------------------------------
+ Proof that omega is an infinite number and
+ hence that epsilon is an infinitesimal number.
+ -------------------------------------------------------------------------*)
+lemma Suc_Un_eq: "{n. n < Suc m} = {n. n < m} Un {n. n = m}"
+by (auto simp add: less_Suc_eq)
+
+(*-------------------------------------------
+ Prove that any segment is finite and
+ hence cannot belong to FreeUltrafilterNat
+ -------------------------------------------*)
+lemma finite_nat_segment: "finite {n::nat. n < m}"
+apply (induct_tac "m")
+apply (auto simp add: Suc_Un_eq)
+done
+
+lemma finite_real_of_nat_segment: "finite {n::nat. real n < real (m::nat)}"
+by (auto intro: finite_nat_segment)
+
+lemma finite_real_of_nat_less_real: "finite {n::nat. real n < u}"
+apply (cut_tac x = u in reals_Archimedean2, safe)
+apply (rule finite_real_of_nat_segment [THEN [2] finite_subset])
+apply (auto dest: order_less_trans)
+done
+
+lemma lemma_real_le_Un_eq: "{n. f n <= u} = {n. f n < u} Un {n. u = (f n :: real)}"
+by (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)
+
+lemma finite_real_of_nat_le_real: "finite {n::nat. real n <= u}"
+by (auto simp add: lemma_real_le_Un_eq lemma_finite_omega_set finite_real_of_nat_less_real)
+
+lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. abs(real n) <= u}"
+apply (simp (no_asm) add: real_of_nat_Suc_gt_zero finite_real_of_nat_le_real)
+done
+
+lemma rabs_real_of_nat_le_real_FreeUltrafilterNat: "{n. abs(real n) <= u} \<notin> FreeUltrafilterNat"
+by (blast intro!: FreeUltrafilterNat_finite finite_rabs_real_of_nat_le_real)
+
+lemma FreeUltrafilterNat_nat_gt_real: "{n. u < real n} \<in> FreeUltrafilterNat"
+apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
+apply (subgoal_tac "- {n::nat. u < real n} = {n. real n <= u}")
+prefer 2 apply force
+apply (simp add: finite_real_of_nat_le_real [THEN FreeUltrafilterNat_finite])
+done
+
+(*--------------------------------------------------------------
+ The complement of {n. abs(real n) <= u} =
+ {n. u < abs (real n)} is in FreeUltrafilterNat
+ by property of (free) ultrafilters
+ --------------------------------------------------------------*)
+
+lemma Compl_real_le_eq: "- {n::nat. real n <= u} = {n. u < real n}"
+by (auto dest!: order_le_less_trans simp add: linorder_not_le)
+
+(*-----------------------------------------------
+ Omega is a member of HInfinite
+ -----------------------------------------------*)
+
+lemma hypreal_omega: "hyprel``{%n::nat. real (Suc n)} \<in> hypreal"
+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)
+done
+
+lemma HInfinite_omega: "omega: HInfinite"
+apply (simp add: omega_def)
+apply (auto intro!: FreeUltrafilterNat_HInfinite)
+apply (rule bexI)
+apply (rule_tac [2] lemma_hyprel_refl, auto)
+apply (simp (no_asm) add: real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)
+done
+declare HInfinite_omega [simp]
+
+(*-----------------------------------------------
+ Epsilon is a member of Infinitesimal
+ -----------------------------------------------*)
+
+lemma Infinitesimal_epsilon: "epsilon \<in> Infinitesimal"
+by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega simp add: hypreal_epsilon_inverse_omega)
+declare Infinitesimal_epsilon [simp]
+
+lemma HFinite_epsilon: "epsilon \<in> HFinite"
+by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
+declare HFinite_epsilon [simp]
+
+lemma epsilon_approx_zero: "epsilon @= 0"
+apply (simp (no_asm) add: mem_infmal_iff [symmetric])
+done
+declare epsilon_approx_zero [simp]
+
+(*------------------------------------------------------------------------
+ Needed for proof that we define a hyperreal [<X(n)] @= hypreal_of_real a given
+ that \<forall>n. |X n - a| < 1/n. Used in proof of NSLIM => LIM.
+ -----------------------------------------------------------------------*)
+
+lemma real_of_nat_less_inverse_iff: "0 < u ==>
+ (u < inverse (real(Suc n))) = (real(Suc n) < inverse u)"
+apply (simp add: inverse_eq_divide)
+apply (subst pos_less_divide_eq, assumption)
+apply (subst pos_less_divide_eq)
+ apply (simp add: real_of_nat_Suc_gt_zero)
+apply (simp add: real_mult_commute)
+done
+
+lemma finite_inverse_real_of_posnat_gt_real: "0 < u ==> finite {n. u < inverse(real(Suc n))}"
+apply (simp (no_asm_simp) add: real_of_nat_less_inverse_iff)
+apply (simp (no_asm_simp) add: real_of_nat_Suc less_diff_eq [symmetric])
+apply (rule finite_real_of_nat_less_real)
+done
+
+lemma lemma_real_le_Un_eq2: "{n. u <= inverse(real(Suc n))} =
+ {n. u < inverse(real(Suc n))} Un {n. u = inverse(real(Suc n))}"
+apply (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)
+done
+
+lemma real_of_nat_inverse_le_iff: "(inverse (real(Suc n)) <= r) = (1 <= r * real(Suc n))"
+apply (simp (no_asm) add: linorder_not_less [symmetric])
+apply (simp (no_asm) add: inverse_eq_divide)
+apply (subst pos_less_divide_eq)
+apply (simp (no_asm) add: real_of_nat_Suc_gt_zero)
+apply (simp (no_asm) add: real_mult_commute)
+done
+
+lemma real_of_nat_inverse_eq_iff: "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)"
+by (auto simp add: inverse_inverse_eq real_of_nat_Suc_gt_zero real_not_refl2 [THEN not_sym])
+
+lemma lemma_finite_omega_set2: "finite {n::nat. u = inverse(real(Suc n))}"
+apply (simp (no_asm_simp) add: real_of_nat_inverse_eq_iff)
+apply (cut_tac x = "inverse u - 1" in lemma_finite_omega_set)
+apply (simp add: real_of_nat_Suc diff_eq_eq [symmetric] eq_commute)
+done
+
+lemma finite_inverse_real_of_posnat_ge_real: "0 < u ==> finite {n. u <= inverse(real(Suc n))}"
+by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_omega_set2 finite_inverse_real_of_posnat_gt_real)
+
+lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat: "0 < u ==>
+ {n. u <= inverse(real(Suc n))} \<notin> FreeUltrafilterNat"
+apply (blast intro!: FreeUltrafilterNat_finite finite_inverse_real_of_posnat_ge_real)
+done
+
+(*--------------------------------------------------------------
+ The complement of {n. u <= inverse(real(Suc n))} =
+ {n. inverse(real(Suc n)) < u} is in FreeUltrafilterNat
+ by property of (free) ultrafilters
+ --------------------------------------------------------------*)
+lemma Compl_le_inverse_eq: "- {n. u <= inverse(real(Suc n))} =
+ {n. inverse(real(Suc n)) < u}"
+apply (auto dest!: order_le_less_trans simp add: linorder_not_le)
+done
+
+lemma FreeUltrafilterNat_inverse_real_of_posnat: "0 < u ==>
+ {n. inverse(real(Suc n)) < u} \<in> FreeUltrafilterNat"
+apply (cut_tac u = u in inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
+apply (auto dest: FreeUltrafilterNat_Compl_mem simp add: Compl_le_inverse_eq)
+done
+
+(*--------------------------------------------------------------
+ Example where we get a hyperreal from a real sequence
+ for which a particular property holds. The theorem is
+ used in proofs about equivalence of nonstandard and
+ standard neighbourhoods. Also used for equivalence of
+ nonstandard ans standard definitions of pointwise
+ limit (the theorem was previously in REALTOPOS.thy).
+ -------------------------------------------------------------*)
+(*-----------------------------------------------------
+ |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal
+ -----------------------------------------------------*)
+lemma real_seq_to_hypreal_Infinitesimal: "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
+ ==> Abs_hypreal(hyprel``{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 hypreal_add Infinitesimal_FreeUltrafilterNat_iff hypreal_inverse)
+done
+
+lemma real_seq_to_hypreal_approx: "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
+ ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x"
+apply (subst approx_minus_iff)
+apply (rule mem_infmal_iff [THEN subst])
+apply (erule real_seq_to_hypreal_Infinitesimal)
+done
+
+lemma real_seq_to_hypreal_approx2: "\<forall>n. abs(x + -X n) < inverse(real(Suc n))
+ ==> Abs_hypreal(hyprel``{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_hypreal(hyprel``{X}) +
+ -Abs_hypreal(hyprel``{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)
+
+
+ML
+{*
+val Infinitesimal_def = thm"Infinitesimal_def";
+val HFinite_def = thm"HFinite_def";
+val HInfinite_def = thm"HInfinite_def";
+val st_def = thm"st_def";
+val monad_def = thm"monad_def";
+val galaxy_def = thm"galaxy_def";
+val approx_def = thm"approx_def";
+val SReal_def = thm"SReal_def";
+
+val Infinitesimal_approx_minus = thm "Infinitesimal_approx_minus";
+val approx_monad_iff = thm "approx_monad_iff";
+val Infinitesimal_approx = thm "Infinitesimal_approx";
+val approx_add = thm "approx_add";
+val approx_minus = thm "approx_minus";
+val approx_minus2 = thm "approx_minus2";
+val approx_minus_cancel = thm "approx_minus_cancel";
+val approx_add_minus = thm "approx_add_minus";
+val approx_mult1 = thm "approx_mult1";
+val approx_mult2 = thm "approx_mult2";
+val approx_mult_subst = thm "approx_mult_subst";
+val approx_mult_subst2 = thm "approx_mult_subst2";
+val approx_mult_subst_SReal = thm "approx_mult_subst_SReal";
+val approx_eq_imp = thm "approx_eq_imp";
+val Infinitesimal_minus_approx = thm "Infinitesimal_minus_approx";
+val bex_Infinitesimal_iff = thm "bex_Infinitesimal_iff";
+val bex_Infinitesimal_iff2 = thm "bex_Infinitesimal_iff2";
+val Infinitesimal_add_approx = thm "Infinitesimal_add_approx";
+val Infinitesimal_add_approx_self = thm "Infinitesimal_add_approx_self";
+val Infinitesimal_add_approx_self2 = thm "Infinitesimal_add_approx_self2";
+val Infinitesimal_add_minus_approx_self = thm "Infinitesimal_add_minus_approx_self";
+val Infinitesimal_add_cancel = thm "Infinitesimal_add_cancel";
+val Infinitesimal_add_right_cancel = thm "Infinitesimal_add_right_cancel";
+val approx_add_left_cancel = thm "approx_add_left_cancel";
+val approx_add_right_cancel = thm "approx_add_right_cancel";
+val approx_add_mono1 = thm "approx_add_mono1";
+val approx_add_mono2 = thm "approx_add_mono2";
+val approx_add_left_iff = thm "approx_add_left_iff";
+val approx_add_right_iff = thm "approx_add_right_iff";
+val approx_HFinite = thm "approx_HFinite";
+val approx_hypreal_of_real_HFinite = thm "approx_hypreal_of_real_HFinite";
+val approx_mult_HFinite = thm "approx_mult_HFinite";
+val approx_mult_hypreal_of_real = thm "approx_mult_hypreal_of_real";
+val approx_SReal_mult_cancel_zero = thm "approx_SReal_mult_cancel_zero";
+val approx_mult_SReal1 = thm "approx_mult_SReal1";
+val approx_mult_SReal2 = thm "approx_mult_SReal2";
+val approx_mult_SReal_zero_cancel_iff = thm "approx_mult_SReal_zero_cancel_iff";
+val approx_SReal_mult_cancel = thm "approx_SReal_mult_cancel";
+val approx_SReal_mult_cancel_iff1 = thm "approx_SReal_mult_cancel_iff1";
+val approx_le_bound = thm "approx_le_bound";
+val Infinitesimal_less_SReal = thm "Infinitesimal_less_SReal";
+val Infinitesimal_less_SReal2 = thm "Infinitesimal_less_SReal2";
+val SReal_not_Infinitesimal = thm "SReal_not_Infinitesimal";
+val SReal_minus_not_Infinitesimal = thm "SReal_minus_not_Infinitesimal";
+val SReal_Int_Infinitesimal_zero = thm "SReal_Int_Infinitesimal_zero";
+val SReal_Infinitesimal_zero = thm "SReal_Infinitesimal_zero";
+val SReal_HFinite_diff_Infinitesimal = thm "SReal_HFinite_diff_Infinitesimal";
+val hypreal_of_real_HFinite_diff_Infinitesimal = thm "hypreal_of_real_HFinite_diff_Infinitesimal";
+val hypreal_of_real_Infinitesimal_iff_0 = thm "hypreal_of_real_Infinitesimal_iff_0";
+val number_of_not_Infinitesimal = thm "number_of_not_Infinitesimal";
+val one_not_Infinitesimal = thm "one_not_Infinitesimal";
+val approx_SReal_not_zero = thm "approx_SReal_not_zero";
+val HFinite_diff_Infinitesimal_approx = thm "HFinite_diff_Infinitesimal_approx";
+val Infinitesimal_ratio = thm "Infinitesimal_ratio";
+val SReal_approx_iff = thm "SReal_approx_iff";
+val number_of_approx_iff = thm "number_of_approx_iff";
+val hypreal_of_real_approx_iff = thm "hypreal_of_real_approx_iff";
+val hypreal_of_real_approx_number_of_iff = thm "hypreal_of_real_approx_number_of_iff";
+val approx_unique_real = thm "approx_unique_real";
+val hypreal_isLub_unique = thm "hypreal_isLub_unique";
+val hypreal_setle_less_trans = thm "hypreal_setle_less_trans";
+val hypreal_gt_isUb = thm "hypreal_gt_isUb";
+val st_part_Ex = thm "st_part_Ex";
+val st_part_Ex1 = thm "st_part_Ex1";
+val HFinite_Int_HInfinite_empty = thm "HFinite_Int_HInfinite_empty";
+val HFinite_not_HInfinite = thm "HFinite_not_HInfinite";
+val not_HFinite_HInfinite = thm "not_HFinite_HInfinite";
+val HInfinite_HFinite_disj = thm "HInfinite_HFinite_disj";
+val HInfinite_HFinite_iff = thm "HInfinite_HFinite_iff";
+val HFinite_HInfinite_iff = thm "HFinite_HInfinite_iff";
+val HInfinite_diff_HFinite_Infinitesimal_disj = thm "HInfinite_diff_HFinite_Infinitesimal_disj";
+val HFinite_inverse = thm "HFinite_inverse";
+val HFinite_inverse2 = thm "HFinite_inverse2";
+val Infinitesimal_inverse_HFinite = thm "Infinitesimal_inverse_HFinite";
+val HFinite_not_Infinitesimal_inverse = thm "HFinite_not_Infinitesimal_inverse";
+val approx_inverse = thm "approx_inverse";
+val hypreal_of_real_approx_inverse = thm "hypreal_of_real_approx_inverse";
+val inverse_add_Infinitesimal_approx = thm "inverse_add_Infinitesimal_approx";
+val inverse_add_Infinitesimal_approx2 = thm "inverse_add_Infinitesimal_approx2";
+val inverse_add_Infinitesimal_approx_Infinitesimal = thm "inverse_add_Infinitesimal_approx_Infinitesimal";
+val Infinitesimal_square_iff = thm "Infinitesimal_square_iff";
+val HFinite_square_iff = thm "HFinite_square_iff";
+val HInfinite_square_iff = thm "HInfinite_square_iff";
+val approx_HFinite_mult_cancel = thm "approx_HFinite_mult_cancel";
+val approx_HFinite_mult_cancel_iff1 = thm "approx_HFinite_mult_cancel_iff1";
+val approx_hrabs_disj = thm "approx_hrabs_disj";
+val monad_hrabs_Un_subset = thm "monad_hrabs_Un_subset";
+val Infinitesimal_monad_eq = thm "Infinitesimal_monad_eq";
+val mem_monad_iff = thm "mem_monad_iff";
+val Infinitesimal_monad_zero_iff = thm "Infinitesimal_monad_zero_iff";
+val monad_zero_minus_iff = thm "monad_zero_minus_iff";
+val monad_zero_hrabs_iff = thm "monad_zero_hrabs_iff";
+val mem_monad_self = thm "mem_monad_self";
+val approx_subset_monad = thm "approx_subset_monad";
+val approx_subset_monad2 = thm "approx_subset_monad2";
+val mem_monad_approx = thm "mem_monad_approx";
+val approx_mem_monad = thm "approx_mem_monad";
+val approx_mem_monad2 = thm "approx_mem_monad2";
+val approx_mem_monad_zero = thm "approx_mem_monad_zero";
+val Infinitesimal_approx_hrabs = thm "Infinitesimal_approx_hrabs";
+val less_Infinitesimal_less = thm "less_Infinitesimal_less";
+val Ball_mem_monad_gt_zero = thm "Ball_mem_monad_gt_zero";
+val Ball_mem_monad_less_zero = thm "Ball_mem_monad_less_zero";
+val approx_hrabs1 = thm "approx_hrabs1";
+val approx_hrabs2 = thm "approx_hrabs2";
+val approx_hrabs = thm "approx_hrabs";
+val approx_hrabs_zero_cancel = thm "approx_hrabs_zero_cancel";
+val approx_hrabs_add_Infinitesimal = thm "approx_hrabs_add_Infinitesimal";
+val approx_hrabs_add_minus_Infinitesimal = thm "approx_hrabs_add_minus_Infinitesimal";
+val hrabs_add_Infinitesimal_cancel = thm "hrabs_add_Infinitesimal_cancel";
+val hrabs_add_minus_Infinitesimal_cancel = thm "hrabs_add_minus_Infinitesimal_cancel";
+val hypreal_less_minus_iff = thm "hypreal_less_minus_iff";
+val Infinitesimal_add_hypreal_of_real_less = thm "Infinitesimal_add_hypreal_of_real_less";
+val Infinitesimal_add_hrabs_hypreal_of_real_less = thm "Infinitesimal_add_hrabs_hypreal_of_real_less";
+val Infinitesimal_add_hrabs_hypreal_of_real_less2 = thm "Infinitesimal_add_hrabs_hypreal_of_real_less2";
+val hypreal_of_real_le_add_Infininitesimal_cancel2 = thm"hypreal_of_real_le_add_Infininitesimal_cancel2";
+val hypreal_of_real_less_Infinitesimal_le_zero = thm "hypreal_of_real_less_Infinitesimal_le_zero";
+val Infinitesimal_add_not_zero = thm "Infinitesimal_add_not_zero";
+val Infinitesimal_square_cancel = thm "Infinitesimal_square_cancel";
+val HFinite_square_cancel = thm "HFinite_square_cancel";
+val Infinitesimal_square_cancel2 = thm "Infinitesimal_square_cancel2";
+val HFinite_square_cancel2 = thm "HFinite_square_cancel2";
+val Infinitesimal_sum_square_cancel = thm "Infinitesimal_sum_square_cancel";
+val HFinite_sum_square_cancel = thm "HFinite_sum_square_cancel";
+val Infinitesimal_sum_square_cancel2 = thm "Infinitesimal_sum_square_cancel2";
+val HFinite_sum_square_cancel2 = thm "HFinite_sum_square_cancel2";
+val Infinitesimal_sum_square_cancel3 = thm "Infinitesimal_sum_square_cancel3";
+val HFinite_sum_square_cancel3 = thm "HFinite_sum_square_cancel3";
+val monad_hrabs_less = thm "monad_hrabs_less";
+val mem_monad_SReal_HFinite = thm "mem_monad_SReal_HFinite";
+val st_approx_self = thm "st_approx_self";
+val st_SReal = thm "st_SReal";
+val st_HFinite = thm "st_HFinite";
+val st_SReal_eq = thm "st_SReal_eq";
+val st_hypreal_of_real = thm "st_hypreal_of_real";
+val st_eq_approx = thm "st_eq_approx";
+val approx_st_eq = thm "approx_st_eq";
+val st_eq_approx_iff = thm "st_eq_approx_iff";
+val st_Infinitesimal_add_SReal = thm "st_Infinitesimal_add_SReal";
+val st_Infinitesimal_add_SReal2 = thm "st_Infinitesimal_add_SReal2";
+val HFinite_st_Infinitesimal_add = thm "HFinite_st_Infinitesimal_add";
+val st_add = thm "st_add";
+val st_number_of = thm "st_number_of";
+val st_minus = thm "st_minus";
+val st_diff = thm "st_diff";
+val st_mult = thm "st_mult";
+val st_Infinitesimal = thm "st_Infinitesimal";
+val st_not_Infinitesimal = thm "st_not_Infinitesimal";
+val st_inverse = thm "st_inverse";
+val st_divide = thm "st_divide";
+val st_idempotent = thm "st_idempotent";
+val Infinitesimal_add_st_less = thm "Infinitesimal_add_st_less";
+val Infinitesimal_add_st_le_cancel = thm "Infinitesimal_add_st_le_cancel";
+val st_le = thm "st_le";
+val st_zero_le = thm "st_zero_le";
+val st_zero_ge = thm "st_zero_ge";
+val st_hrabs = thm "st_hrabs";
+val FreeUltrafilterNat_HFinite = thm "FreeUltrafilterNat_HFinite";
+val HFinite_FreeUltrafilterNat_iff = thm "HFinite_FreeUltrafilterNat_iff";
+val FreeUltrafilterNat_const_Finite = thm "FreeUltrafilterNat_const_Finite";
+val FreeUltrafilterNat_HInfinite = thm "FreeUltrafilterNat_HInfinite";
+val HInfinite_FreeUltrafilterNat_iff = thm "HInfinite_FreeUltrafilterNat_iff";
+val Infinitesimal_FreeUltrafilterNat = thm "Infinitesimal_FreeUltrafilterNat";
+val FreeUltrafilterNat_Infinitesimal = thm "FreeUltrafilterNat_Infinitesimal";
+val Infinitesimal_FreeUltrafilterNat_iff = thm "Infinitesimal_FreeUltrafilterNat_iff";
+val Infinitesimal_hypreal_of_nat_iff = thm "Infinitesimal_hypreal_of_nat_iff";
+val Suc_Un_eq = thm "Suc_Un_eq";
+val finite_nat_segment = thm "finite_nat_segment";
+val finite_real_of_nat_segment = thm "finite_real_of_nat_segment";
+val finite_real_of_nat_less_real = thm "finite_real_of_nat_less_real";
+val finite_real_of_nat_le_real = thm "finite_real_of_nat_le_real";
+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";
+val HFinite_epsilon = thm "HFinite_epsilon";
+val epsilon_approx_zero = thm "epsilon_approx_zero";
+val real_of_nat_less_inverse_iff = thm "real_of_nat_less_inverse_iff";
+val finite_inverse_real_of_posnat_gt_real = thm "finite_inverse_real_of_posnat_gt_real";
+val real_of_nat_inverse_le_iff = thm "real_of_nat_inverse_le_iff";
+val real_of_nat_inverse_eq_iff = thm "real_of_nat_inverse_eq_iff";
+val finite_inverse_real_of_posnat_ge_real = thm "finite_inverse_real_of_posnat_ge_real";
+val inverse_real_of_posnat_ge_real_FreeUltrafilterNat = thm "inverse_real_of_posnat_ge_real_FreeUltrafilterNat";
+val FreeUltrafilterNat_inverse_real_of_posnat = thm "FreeUltrafilterNat_inverse_real_of_posnat";
+val real_seq_to_hypreal_Infinitesimal = thm "real_seq_to_hypreal_Infinitesimal";
+val real_seq_to_hypreal_approx = thm "real_seq_to_hypreal_approx";
+val real_seq_to_hypreal_approx2 = thm "real_seq_to_hypreal_approx2";
+val real_seq_to_hypreal_Infinitesimal2 = thm "real_seq_to_hypreal_Infinitesimal2";
+val HInfinite_HFinite_add = thm "HInfinite_HFinite_add";
+val HInfinite_ge_HInfinite = thm "HInfinite_ge_HInfinite";
+val Infinitesimal_inverse_HInfinite = thm "Infinitesimal_inverse_HInfinite";
+val HInfinite_HFinite_not_Infinitesimal_mult = thm "HInfinite_HFinite_not_Infinitesimal_mult";
+val HInfinite_HFinite_not_Infinitesimal_mult2 = thm "HInfinite_HFinite_not_Infinitesimal_mult2";
+val HInfinite_gt_SReal = thm "HInfinite_gt_SReal";
+val HInfinite_gt_zero_gt_one = thm "HInfinite_gt_zero_gt_one";
+val not_HInfinite_one = thm "not_HInfinite_one";
+*}
+
end