(*  Title       : NSA.thy

    Author      : Jacques D. Fleuriot

    Copyright   : 1998  University of Cambridge

*)

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

theory NSA = HyperArith + RComplete:

constdefs

  Infinitesimal  :: "hypreal set"

   "Infinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> abs x < r}"

  HFinite :: "hypreal set"

   "HFinite == {x. \<exists>r \<in> Reals. abs x < r}"

  HInfinite :: "hypreal set"

   "HInfinite == {x. \<forall>r \<in> Reals. r < abs x}"

  (* standard part map *)

  st        :: "hypreal => hypreal"

   "st           == (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"

  monad     :: "hypreal => hypreal set"

   "monad x      == {y. x @= y}"

  galaxy    :: "hypreal => hypreal set"

   "galaxy x     == {y. (x + -y) \<in> HFinite}"

  (* infinitely close *)

  approx :: "[hypreal, hypreal] => bool"    (infixl "@=" 50)

   "x @= y       == (x + -y) \<in> Infinitesimal"

defs (overloaded)

   (*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 [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) 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)

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