src/HOL/Hyperreal/NSA.thy

define new constant of_real for class real_algebra_1;
define set Reals as range of_real;
add lemmas about of_real and Reals

(*  Title       : NSA.thy
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge

Converted to Isar and polished by lcp
*)

header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}

theory NSA
imports HyperArith "../Real/RComplete"
begin

definition

  hnorm :: "'a::norm star \<Rightarrow> real star"
  "hnorm = *f* norm"

  Infinitesimal  :: "('a::real_normed_vector) star set"
  "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"

  HFinite :: "('a::real_normed_vector) star set"
  "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"

  HInfinite :: "('a::real_normed_vector) star set"
  "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"

  approx :: "['a::real_normed_vector star, 'a star] => bool"
    (infixl "@=" 50)
    --{*the `infinitely close' relation*}
  "(x @= y) = ((x + -y) \<in> Infinitesimal)"

  st        :: "hypreal => hypreal"
    --{*the standard part of a hyperreal*}
  "st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"

  monad     :: "'a::real_normed_vector star => 'a star set"
  "monad x = {y. x @= y}"

  galaxy    :: "'a::real_normed_vector star => 'a star set"
  "galaxy x = {y. (x + -y) \<in> HFinite}"

const_syntax (xsymbols)
  approx  (infixl "\<approx>" 50)

const_syntax (HTML output)
  approx  (infixl "\<approx>" 50)


lemma hypreal_of_real_of_real_eq: "hypreal_of_real r = of_real r"
proof -
  have "hypreal_of_real r = hypreal_of_real (of_real r)" by simp
  also have "\<dots> = of_real r" by (rule star_of_of_real)
  finally show ?thesis .
qed

lemma SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
by (simp add: Reals_def image_def hypreal_of_real_of_real_eq)


subsection{*Nonstandard extension of the norm function*}

declare hnorm_def [transfer_unfold]

lemma hnorm_ge_zero [simp]:
  "\<And>x::'a::real_normed_vector star. 0 \<le> hnorm x"
by transfer (rule norm_ge_zero)

lemma hnorm_eq_zero [simp]:
  "\<And>x::'a::real_normed_vector star. (hnorm x = 0) = (x = 0)"
by transfer (rule norm_eq_zero)

lemma hnorm_triangle_ineq:
  "\<And>x y::'a::real_normed_vector star. hnorm (x + y) \<le> hnorm x + hnorm y"
by transfer (rule norm_triangle_ineq)

lemma hnorm_scaleR:
  "\<And>a (x::'a::real_normed_vector star).
   hnorm (( *f2* scaleR) a x) = \<bar>a\<bar> * hnorm x"
by transfer (rule norm_scaleR)

lemma hnorm_mult_ineq:
  "\<And>x y::'a::real_normed_algebra star. hnorm (x * y) \<le> hnorm x * hnorm y"
by transfer (rule norm_mult_ineq)

lemma hnorm_mult:
  "\<And>x y::'a::real_normed_div_algebra star. hnorm (x * y) = hnorm x * hnorm y"
by transfer (rule norm_mult)

lemma hnorm_one [simp]:
  "hnorm (1\<Colon>'a::real_normed_div_algebra star) = 1"
by transfer (rule norm_one)

lemma hnorm_zero [simp]:
  "hnorm (0\<Colon>'a::real_normed_vector star) = 0"
by transfer (rule norm_zero)

lemma zero_less_hnorm_iff [simp]:
  "\<And>x::'a::real_normed_vector star. (0 < hnorm x) = (x \<noteq> 0)"
by transfer (rule zero_less_norm_iff)

lemma hnorm_minus_cancel [simp]:
  "\<And>x::'a::real_normed_vector star. hnorm (- x) = hnorm x"
by transfer (rule norm_minus_cancel)

lemma hnorm_minus_commute:
  "\<And>a b::'a::real_normed_vector star. hnorm (a - b) = hnorm (b - a)"
by transfer (rule norm_minus_commute)

lemma hnorm_triangle_ineq2:
  "\<And>a b::'a::real_normed_vector star. hnorm a - hnorm b \<le> hnorm (a - b)"
by transfer (rule norm_triangle_ineq2)

lemma hnorm_triangle_ineq4:
  "\<And>a b::'a::real_normed_vector star. hnorm (a - b) \<le> hnorm a + hnorm b"
by transfer (rule norm_triangle_ineq4)

lemma nonzero_hnorm_inverse:
  "\<And>a::'a::real_normed_div_algebra star.
   a \<noteq> 0 \<Longrightarrow> hnorm (inverse a) = inverse (hnorm a)"
by transfer (rule nonzero_norm_inverse)

lemma hnorm_inverse:
  "\<And>a::'a::{real_normed_div_algebra,division_by_zero} star.
   hnorm (inverse a) = inverse (hnorm a)"
by transfer (rule norm_inverse)

lemma hypreal_hnorm_def [simp]:
  "\<And>r::hypreal. hnorm r \<equiv> \<bar>r\<bar>"
by transfer (rule real_norm_def)

lemma hnorm_add_less:
  fixes x y :: "'a::real_normed_vector star"
  shows "\<lbrakk>hnorm x < r; hnorm y < s\<rbrakk> \<Longrightarrow> hnorm (x + y) < r + s"
by (rule order_le_less_trans [OF hnorm_triangle_ineq add_strict_mono])

lemma hnorm_mult_less:
  fixes x y :: "'a::real_normed_algebra star"
  shows "\<lbrakk>hnorm x < r; hnorm y < s\<rbrakk> \<Longrightarrow> hnorm (x * y) < r * s"
apply (rule order_le_less_trans [OF hnorm_mult_ineq])
apply (simp add: mult_strict_mono')
done


subsection{*Closure Laws for the Standard Reals*}

lemma SReal_add [simp]:
     "[| (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))
done

lemma SReal_inverse: "(x::hypreal) \<in> Reals ==> inverse x \<in> Reals"
apply (simp add: SReal_def)
apply (blast intro: star_of_inverse [symmetric])
done

lemma SReal_divide: "[| (x::hypreal) \<in> Reals;  y \<in> Reals |] ==> x/y \<in> Reals"
by (simp (no_asm_simp) add: SReal_mult SReal_inverse divide_inverse)

lemma SReal_minus: "(x::hypreal) \<in> Reals ==> -x \<in> Reals"
apply (simp add: SReal_def)
apply (blast intro: star_of_minus [symmetric])
done

lemma SReal_minus_iff [simp]: "(-x \<in> Reals) = ((x::hypreal) \<in> Reals)"
apply auto
apply (erule_tac [2] SReal_minus)
apply (drule SReal_minus, auto)
done

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 (auto simp add: SReal_def)
apply (rule_tac x="abs r" in exI)
apply simp
done

lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> Reals"
by (simp add: SReal_def)

lemma SReal_number_of [simp]: "(number_of w ::hypreal) \<in> Reals"
apply (simp only: star_of_number_of [symmetric])
apply (rule SReal_hypreal_of_real)
done

(** As always with numerals, 0 and 1 are special cases **)

lemma Reals_0 [simp]: "(0::hypreal) \<in> Reals"
apply (subst numeral_0_eq_0 [symmetric])
apply (rule SReal_number_of)
done

lemma Reals_1 [simp]: "(1::hypreal) \<in> Reals"
apply (subst numeral_1_eq_1 [symmetric])
apply (rule SReal_number_of)
done

lemma SReal_divide_number_of: "r \<in> Reals ==> r/(number_of w::hypreal) \<in> Reals"
apply (simp only: divide_inverse)
apply (blast intro!: SReal_number_of SReal_mult SReal_inverse)
done

text{*epsilon is not in Reals because it is an infinitesimal*}
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 \<subseteq> 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 dense, safe)
apply (rule_tac x = "hypreal_of_real r" in bexI, auto)
done

text{*Completeness of Reals, but both lemmas are unused.*}

lemma SReal_sup_lemma:
     "P \<subseteq> 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 \<subseteq> 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


subsection{*Lifting of the Ub and Lub Properties*}

lemma hypreal_of_real_isUb_iff:
      "(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) =
       (isUb (UNIV :: real set) Q Y)"
by (simp add: isUb_def setle_def)

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)"
by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)

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 \<subseteq> 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


subsection{* 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 hnorm_add_less)
done

lemma HFinite_mult:
  fixes x y :: "'a::real_normed_algebra star"
  shows "[|x \<in> HFinite; y \<in> HFinite|] ==> x*y \<in> HFinite"
apply (simp add: HFinite_def)
apply (blast intro!: SReal_mult hnorm_mult_less)
done

lemma HFinite_minus_iff: "(-x \<in> HFinite) = (x \<in> HFinite)"
by (simp add: HFinite_def)

lemma HFinite_star_of [simp]: "star_of x \<in> HFinite"
apply (simp add: HFinite_def)
apply (rule_tac x="star_of (norm x) + 1" in bexI)
apply (transfer, simp)
apply (blast intro: SReal_add SReal_hypreal_of_real Reals_1)
done

lemma SReal_subset_HFinite: "(Reals::hypreal set) \<subseteq> HFinite"
by (auto simp add: SReal_def)

lemma HFinite_hypreal_of_real: "hypreal_of_real x \<in> HFinite"
by (rule HFinite_star_of)

lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. hnorm x < t"
by (simp add: HFinite_def)

lemma HFinite_hrabs_iff [iff]: "(abs (x::hypreal) \<in> HFinite) = (x \<in> HFinite)"
by (simp add: HFinite_def)

lemma HFinite_hnorm_iff [iff]: "(hnorm x \<in> HFinite) = (x \<in> HFinite)"
by (simp add: HFinite_def)

lemma HFinite_number_of [simp]: "number_of w \<in> HFinite"
by (unfold star_number_def, rule HFinite_star_of)

(** As always with numerals, 0 and 1 are special cases **)

lemma HFinite_0 [simp]: "0 \<in> HFinite"
by (unfold star_zero_def, rule HFinite_star_of)

lemma HFinite_1 [simp]: "1 \<in> HFinite"
by (unfold star_one_def, rule HFinite_star_of)

lemma HFinite_bounded:
  "[|(x::hypreal) \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
apply (case_tac "x \<le> 0")
apply (drule_tac y = x in order_trans)
apply (drule_tac [2] order_antisym)
apply (auto simp add: linorder_not_le)
apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def)
done


subsection{* Set of Infinitesimals is a Subring of the Hyperreals*}

lemma InfinitesimalI:
  "(\<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm x < r) \<Longrightarrow> x \<in> Infinitesimal"
by (simp add: Infinitesimal_def)

lemma InfinitesimalD:
      "x \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> hnorm x < r"
by (simp add: Infinitesimal_def)

lemma Infinitesimal_zero [iff]: "0 \<in> Infinitesimal"
by (simp add: Infinitesimal_def)

lemma hypreal_sum_of_halves: "x/(2::hypreal) + x/(2::hypreal) = x"
by auto

lemma Infinitesimal_add:
     "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> (x+y) \<in> Infinitesimal"
apply (rule InfinitesimalI)
apply (rule hypreal_sum_of_halves [THEN subst])
apply (drule half_gt_zero)
apply (blast intro: hnorm_add_less SReal_divide_number_of dest: InfinitesimalD)
done

lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)"
by (simp add: Infinitesimal_def)

lemma Infinitesimal_diff:
     "[| x \<in> Infinitesimal;  y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
by (simp add: diff_def Infinitesimal_add)

lemma Infinitesimal_mult:
  fixes x y :: "'a::real_normed_algebra star"
  shows "[|x \<in> Infinitesimal; y \<in> Infinitesimal|] ==> (x * y) \<in> Infinitesimal"
apply (rule InfinitesimalI)
apply (case_tac "y = 0", simp)
apply (subgoal_tac "hnorm (x * y) < 1 * r", simp only: mult_1)
apply (rule hnorm_mult_less)
apply (simp_all add: InfinitesimalD)
done

lemma Infinitesimal_HFinite_mult:
  fixes x y :: "'a::real_normed_algebra star"
  shows "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (x * y) \<in> Infinitesimal"
apply (rule InfinitesimalI)
apply (drule HFiniteD, clarify)
apply (subgoal_tac "0 < t")
apply (subgoal_tac "hnorm (x * y) < (r / t) * t", simp)
apply (subgoal_tac "0 < r / t")
apply (rule hnorm_mult_less)
apply (simp add: InfinitesimalD SReal_divide)
apply assumption
apply (simp only: divide_pos_pos)
apply (erule order_le_less_trans [OF hnorm_ge_zero])
done

lemma Infinitesimal_HFinite_mult2:
  fixes x y :: "'a::real_normed_algebra star"
  shows "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (y * x) \<in> Infinitesimal"
apply (rule InfinitesimalI)
apply (drule HFiniteD, clarify)
apply (subgoal_tac "0 < t")
apply (subgoal_tac "hnorm (y * x) < t * (r / t)", simp)
apply (subgoal_tac "0 < r / t")
apply (rule hnorm_mult_less)
apply assumption
apply (simp add: InfinitesimalD SReal_divide)
apply (simp only: divide_pos_pos)
apply (erule order_le_less_trans [OF hnorm_ge_zero])
done

lemma Compl_HFinite: "- HFinite = HInfinite"
apply (auto simp add: HInfinite_def HFinite_def linorder_not_less)
apply (rule_tac y="r + 1" in order_less_le_trans, simp)
apply (simp add: SReal_add Reals_1)
done

lemma HInfinite_inverse_Infinitesimal:
  fixes x :: "'a::real_normed_div_algebra star"
  shows "x \<in> HInfinite ==> inverse x \<in> Infinitesimal"
apply (rule InfinitesimalI)
apply (subgoal_tac "x \<noteq> 0")
apply (rule inverse_less_imp_less)
apply (simp add: nonzero_hnorm_inverse)
apply (simp add: HInfinite_def SReal_inverse)
apply assumption
apply (clarify, simp add: Compl_HFinite [symmetric])
done

lemma HInfiniteI: "(\<And>r. r \<in> \<real> \<Longrightarrow> r < hnorm x) \<Longrightarrow> x \<in> HInfinite"
by (simp add: HInfinite_def)

lemma HInfiniteD: "\<lbrakk>x \<in> HInfinite; r \<in> \<real>\<rbrakk> \<Longrightarrow> r < hnorm x"
by (simp add: HInfinite_def)

lemma HInfinite_mult:
  fixes x y :: "'a::real_normed_div_algebra star"
  shows "[|x \<in> HInfinite; y \<in> HInfinite|] ==> (x*y) \<in> HInfinite"
apply (rule HInfiniteI, simp only: hnorm_mult)
apply (subgoal_tac "r * 1 < hnorm x * hnorm y", simp only: mult_1)
apply (case_tac "x = 0", simp add: HInfinite_def)
apply (rule mult_strict_mono)
apply (simp_all add: HInfiniteD)
done

lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x+y"
by (auto dest: add_less_le_mono)

lemma HInfinite_add_ge_zero:
     "[|(x::hypreal) \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (x + y): HInfinite"
by (auto intro!: hypreal_add_zero_less_le_mono 
       simp add: abs_if add_commute add_nonneg_nonneg HInfinite_def)

lemma HInfinite_add_ge_zero2:
     "[|(x::hypreal) \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (y + x): HInfinite"
by (auto intro!: HInfinite_add_ge_zero simp add: add_commute)

lemma HInfinite_add_gt_zero:
     "[|(x::hypreal) \<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::hypreal) \<in> HInfinite; y \<le> 0; x \<le> 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::hypreal) \<in> HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite"
by (blast intro: HInfinite_add_le_zero order_less_imp_le)

lemma HFinite_sum_squares:
  fixes a b c :: "'a::real_normed_algebra star"
  shows "[|a: HFinite; b: HFinite; c: HFinite|]
      ==> a*a + b*b + c*c \<in> HFinite"
by (auto intro: HFinite_mult HFinite_add)

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 [iff]:
     "(abs (x::hypreal) \<in> Infinitesimal) = (x \<in> Infinitesimal)"
by (auto simp add: abs_if)

lemma HFinite_diff_Infinitesimal_hrabs:
  "(x::hypreal) \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal"
by blast

lemma hrabs_less_Infinitesimal:
      "[| e \<in> Infinitesimal; abs (x::hypreal) < e |] ==> x \<in> Infinitesimal"
by (auto simp add: Infinitesimal_def abs_less_iff)

lemma hrabs_le_Infinitesimal:
     "[| e \<in> Infinitesimal; abs (x::hypreal) \<le> 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::hypreal) \<in> Infinitesimal"
by (auto simp add: Infinitesimal_def abs_less_iff)

lemma Infinitesimal_interval2:
     "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
         e' \<le> x ; x \<le> e |] ==> (x::hypreal) \<in> Infinitesimal"
by (auto intro: Infinitesimal_interval simp add: order_le_less)

lemma not_Infinitesimal_mult:
  fixes x y :: "'a::real_normed_div_algebra star"
  shows "[| x \<notin> Infinitesimal;  y \<notin> Infinitesimal|] ==> (x*y) \<notin>Infinitesimal"
apply (unfold Infinitesimal_def, clarify, rename_tac r s)
apply (simp only: linorder_not_less hnorm_mult)
apply (drule_tac x = "r * s" in bspec)
apply (fast intro: SReal_mult)
apply (drule mp, blast intro: mult_pos_pos)
apply (drule_tac c = s and d = "hnorm y" and a = r and b = "hnorm x" in mult_mono)
apply (simp_all (no_asm_simp))
done

lemma Infinitesimal_mult_disj:
  fixes x y :: "'a::real_normed_div_algebra star"
  shows "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:
  fixes x y :: "'a::real_normed_div_algebra star"
  shows "[| 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 \<subseteq> 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])


subsection{*The 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 add_commute)

lemma approx_refl [iff]: "x @= x"
by (simp add: approx_def Infinitesimal_def)

lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y"
by (simp add: add_commute)

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)


ML {*
local
(*** 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 = thm "zero_approx_reorient" RS eq_reflection;
val meta_one_approx_reorient = thm "one_approx_reorient" RS eq_reflection;
val meta_number_of_approx_reorient = thm "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);

in
val approx_reorient_simproc =
  Int_Numeral_Base_Simprocs.prep_simproc
    ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
end;

Addsimprocs [approx_reorient_simproc];
*}

lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)"
by (auto simp add: diff_def approx_minus_iff [symmetric] mem_infmal_iff)

lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))"
apply (simp add: monad_def)
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 simp
  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: add_commute)
done

lemma approx_minus2: "-a @= -b ==> a @= b"
by (auto dest: approx_minus)

lemma approx_minus_cancel [simp]: "(-a @= -b) = (a @= b)"
by (blast intro: approx_minus approx_minus2)

lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d"
by (blast intro!: approx_add approx_minus)

lemma approx_mult1:
  fixes a b c :: "'a::real_normed_algebra star"
  shows "[| 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:
  fixes a b c :: "'a::real_normed_algebra star"
  shows "[|a @= b; c: HFinite|] ==> c*a @= c*b"
by (simp add: approx_def Infinitesimal_HFinite_mult2 minus_mult_right 
              right_distrib [symmetric] 
         del: minus_mult_right [symmetric])

lemma approx_mult_subst:
  fixes u v x y :: "'a::real_normed_algebra star"
  shows "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"
by (blast intro: approx_mult2 approx_trans)

lemma approx_mult_subst2:
  fixes u v x y :: "'a::real_normed_algebra star"
  shows "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v"
by (blast intro: approx_mult1 approx_trans)

lemma approx_mult_subst_star_of:
  fixes u x y :: "'a::real_normed_algebra star"
  shows "[| u @= x*star_of v; x @= y |] ==> u @= y*star_of v"
by (auto intro: approx_mult_subst2)

lemma approx_mult_subst_SReal:
     "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v"
by (rule approx_mult_subst_star_of)

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: 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: add_assoc [symmetric])
done

lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal ==> x @= y + x"
by (auto dest: Infinitesimal_add_approx_self simp add: add_commute)

lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal ==> x @= x + -y"
by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2])

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: 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: 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: add_commute)
done

lemma approx_add_mono1: "b @= c ==> d + b @= d + c"
apply (rule approx_minus_iff [THEN iffD2])
apply (simp add: approx_minus_iff [symmetric] add_ac)
done

lemma approx_add_mono2: "b @= c ==> b + a @= c + a"
by (simp add: add_commute approx_add_mono1)

lemma approx_add_left_iff [simp]: "(a + b @= a + c) = (b @= c)"
by (fast elim: approx_add_left_cancel approx_add_mono1)

lemma approx_add_right_iff [simp]: "(b + a @= c + a) = (b @= c)"
by (simp add: add_commute)

lemma approx_HFinite: "[| x \<in> HFinite; x @= y |] ==> y \<in> HFinite"
apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe)
apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]])
apply (drule HFinite_add)
apply (auto simp add: add_assoc)
done

lemma approx_star_of_HFinite: "x @= star_of D ==> x \<in> HFinite"
by (rule approx_sym [THEN [2] approx_HFinite], auto)

lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \<in> HFinite"
by (rule approx_star_of_HFinite)

lemma approx_mult_HFinite:
  fixes a b c d :: "'a::real_normed_algebra star"
  shows "[|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_star_of:
  fixes a c :: "'a::real_normed_algebra star"
  shows "[|a @= star_of b; c @= star_of d |]
      ==> a*c @= star_of b*star_of d"
by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)

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"
by (rule approx_mult_star_of)

lemma approx_SReal_mult_cancel_zero:
     "[| (a::hypreal) \<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: mult_assoc [symmetric])
done

lemma approx_mult_SReal1: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> x*a @= 0"
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)

lemma approx_mult_SReal2: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> a*x @= 0"
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)

lemma approx_mult_SReal_zero_cancel_iff [simp]:
     "[|(a::hypreal) \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)

lemma approx_SReal_mult_cancel:
     "[| (a::hypreal) \<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: mult_assoc [symmetric])
done

lemma approx_SReal_mult_cancel_iff1 [simp]:
     "[| (a::hypreal) \<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)

lemma approx_le_bound: "[| (z::hypreal) \<le> f; f @= g; g \<le> 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


subsection{* Zero is the Only Infinitesimal that is also a Real*}

lemma Infinitesimal_less_SReal:
     "[| (x::hypreal) \<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::hypreal) \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> y < r"
by (blast intro: Infinitesimal_less_SReal)

lemma SReal_not_Infinitesimal:
     "[| 0 < y;  (y::hypreal) \<in> Reals|] ==> y \<notin> Infinitesimal"
apply (simp add: Infinitesimal_def)
apply (auto simp add: abs_if)
done

lemma SReal_minus_not_Infinitesimal:
     "[| y < 0;  (y::hypreal) \<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::hypreal}"
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::hypreal) \<in> Reals; x \<in> Infinitesimal|] ==> x = 0"
by (cut_tac SReal_Int_Infinitesimal_zero, blast)

lemma SReal_HFinite_diff_Infinitesimal:
     "[| (x::hypreal) \<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 star_of_Infinitesimal_iff_0 [iff]:
  "(star_of x \<in> Infinitesimal) = (x = 0)"
apply (auto simp add: Infinitesimal_def)
apply (drule_tac x="hnorm (star_of x)" in bspec)
apply (simp add: hnorm_def)
apply simp
done

lemma star_of_HFinite_diff_Infinitesimal:
     "x \<noteq> 0 ==> star_of x \<in> HFinite - Infinitesimal"
by simp

lemma hypreal_of_real_Infinitesimal_iff_0:
     "(hypreal_of_real x \<in> Infinitesimal) = (x=0)"
by (rule star_of_Infinitesimal_iff_0)

lemma number_of_not_Infinitesimal [simp]:
     "number_of w \<noteq> (0::hypreal) ==> (number_of w :: hypreal) \<notin> Infinitesimal"
by (fast dest: SReal_number_of [THEN SReal_Infinitesimal_zero])

(*again: 1 is a special case, but not 0 this time*)
lemma one_not_Infinitesimal [simp]:
  "(1::'a::{real_normed_vector,axclass_0_neq_1} star) \<notin> Infinitesimal"
apply (simp only: star_one_def star_of_Infinitesimal_iff_0)
apply simp
done

lemma approx_SReal_not_zero:
  "[| (y::hypreal) \<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:
  fixes x y :: "'a::{real_normed_div_algebra,field} star"
  shows "[| y \<noteq> 0;  y \<in> Infinitesimal;  x/y \<in> HFinite |]
         ==> x \<in> Infinitesimal"
apply (drule Infinitesimal_HFinite_mult2, assumption)
apply (simp add: divide_inverse mult_assoc)
done

lemma Infinitesimal_SReal_divide: 
  "[| (x::hypreal) \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal"
apply (simp add: divide_inverse)
apply (auto intro!: Infinitesimal_HFinite_mult 
            dest!: SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
done

(*------------------------------------------------------------------
       Standard Part Theorem: Every finite x: R* is infinitely
       close to a unique real number (i.e a member of Reals)
 ------------------------------------------------------------------*)

subsection{* Uniqueness: Two Infinitely Close Reals are Equal*}

lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)"
apply safe
apply (simp add: approx_def)
apply (simp only: star_of_minus [symmetric] star_of_add [symmetric])
apply (simp only: star_of_Infinitesimal_iff_0)
apply (simp only: diff_minus [symmetric] right_minus_eq)
done

lemma SReal_approx_iff:
  "[|(x::hypreal) \<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 [simp]:
     "(number_of v @= (number_of w :: 'a::{number,real_normed_vector} star)) =
      (number_of v = (number_of w :: 'a))"
apply (unfold star_number_def)
apply (rule star_of_approx_iff)
done

(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
lemma [simp]:
  "(number_of w @= (0::'a::{number,real_normed_vector} star)) =
   (number_of w = (0::'a))"
  "((0::'a::{number,real_normed_vector} star) @= number_of w) =
   (number_of w = (0::'a))"
  "(number_of w @= (1::'b::{number,one,real_normed_vector} star)) =
   (number_of w = (1::'b))"
  "((1::'b::{number,one,real_normed_vector} star) @= number_of w) =
   (number_of w = (1::'b))"
  "~ (0 @= (1::'c::{axclass_0_neq_1,real_normed_vector} star))"
  "~ (1 @= (0::'c::{axclass_0_neq_1,real_normed_vector} star))"
apply (unfold star_number_def star_zero_def star_one_def)
apply (unfold star_of_approx_iff)
by (auto intro: sym)

lemma hypreal_of_real_approx_iff:
     "(hypreal_of_real k @= hypreal_of_real m) = (k = m)"
by (rule star_of_approx_iff)

lemma hypreal_of_real_approx_number_of_iff [simp]:
     "(hypreal_of_real k @= number_of w) = (k = number_of w)"
by (subst hypreal_of_real_approx_iff [symmetric], auto)

(*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::hypreal) \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)


subsection{* 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!: order_antisym dest!: isLub_le_isUb)
done

lemma lemma_st_part_ub:
     "(x::hypreal) \<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::hypreal) \<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} \<subseteq> Reals"
by auto

lemma lemma_st_part_lub:
     "(x::hypreal) \<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 \<le> t) = (r \<le> 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: add_assoc [symmetric])
done

lemma lemma_st_part_le1:
     "[| (x::hypreal) \<in> HFinite;  isLub Reals {s. s \<in> Reals & s < x} t;
         r \<in> Reals;  0 < r |] ==> x \<le> 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:
     "[| S *<= (x::hypreal); 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:
     "[| isUb R S (x::hypreal); 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::hypreal) \<in> HFinite; x < y; y \<in> Reals |]
      ==> isUb Reals {s. s \<in> Reals & s < x} y"
by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)

lemma lemma_minus_le_zero: "t \<le> t + -r ==> r \<le> (0::hypreal)"
apply (drule_tac c = "-t" in add_left_mono)
apply (auto simp add: add_assoc [symmetric])
done

lemma lemma_st_part_le2:
     "[| (x::hypreal) \<in> HFinite;
         isLub Reals {s. s \<in> Reals & s < x} t;
         r \<in> Reals; 0 < r |]
      ==> t + -r \<le> 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_st_part1a:
     "[| (x::hypreal) \<in> HFinite;
         isLub Reals {s. s \<in> Reals & s < x} t;
         r \<in> Reals; 0 < r |]
      ==> x + -t \<le> r"
apply (subgoal_tac "x \<le> t+r") 
apply (auto intro: lemma_st_part_le1)
done

lemma lemma_st_part2a:
     "[| (x::hypreal) \<in> HFinite;
         isLub Reals {s. s \<in> Reals & s < x} t;
         r \<in> Reals;  0 < r |]
      ==> -(x + -t) \<le> r"
apply (subgoal_tac "(t + -r \<le> x)") 
apply (auto intro: 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::hypreal) \<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::hypreal) \<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)
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::hypreal) \<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::hypreal) \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t |]
      ==> \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
by (blast dest!: lemma_st_part_major)


text{*Existence of real and Standard Part Theorem*}
lemma lemma_st_part_Ex:
     "(x::hypreal) \<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::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x @= t"
apply (simp add: approx_def Infinitesimal_def)
apply (drule lemma_st_part_Ex, auto)
done

text{*There is a unique real infinitely close*}
lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. 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

subsection{* Finite, Infinite and Infinitesimal*}

lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}"
apply (simp add: HFinite_def HInfinite_def)
apply (auto dest: order_less_trans)
done

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