Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: NSA.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Nonstandard_Analysis/NSA.thy
    Author:     Jacques D. Fleuriot, University of Cambridge
    Author:     Lawrence C Paulson, University of Cambridge
*)

section \<open>Infinite Numbers, Infinitesimals, Infinitely Close Relation\<close>

theory NSA
  imports HyperDef "HOL-Library.Lub_Glb"
begin

definition hnorm :: "'a::real_normed_vector star \ real star"
  where [transfer_unfold]: "hnorm = *f* norm"

definition Infinitesimal  :: "('a::real_normed_vector) star set"
  where "Infinitesimal = {x. \r \ Reals. 0 < r \ hnorm x < r}"

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

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

definition approx :: "'a::real_normed_vector star \ 'a star \ bool" (infixl "\" 50)
  where "x \ y \ x - y \ Infinitesimal"
    \<comment> \<open>the ``infinitely close'' relation\<close>

definition st :: "hypreal \ hypreal"
  where "st = (\x. SOME r. x \ HFinite \ r \ \ \ r \ x)"
    \<comment> \<open>the standard part of a hyperreal\<close>

definition monad :: "'a::real_normed_vector star \ 'a star set"
  where "monad x = {y. x \ y}"

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

lemma SReal_def: "\ \ {x. \r. x = hypreal_of_real r}"
  by (simp add: Reals_def image_def)

subsection \<open>Nonstandard Extension of the Norm Function\<close>

definition scaleHR :: "real star \ 'a star \ 'a::real_normed_vector star"
  where [transfer_unfold]: "scaleHR = starfun2 scaleR"

lemma Standard_hnorm [simp]: "x \ Standard \ hnorm x \ Standard"
  by (simp add: hnorm_def)

lemma star_of_norm [simp]: "star_of (norm x) = hnorm (star_of x)"
  by transfer (rule refl)

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

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

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

lemma hnorm_triangle_ineq3: "\x y::'a::real_normed_vector star. \hnorm x - hnorm y\ \ hnorm (x - y)"
  by transfer (rule norm_triangle_ineq3)

lemma hnorm_scaleR: "\x::'a::real_normed_vector star. hnorm (a *\<^sub>R x) = \star_of a\ * hnorm x"
  by transfer (rule norm_scaleR)

lemma hnorm_scaleHR: "\a (x::'a::real_normed_vector star). hnorm (scaleHR a x) = \a\ * hnorm x"
  by transfer (rule norm_scaleR)

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

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

lemma hnorm_hyperpow: "\(x::'a::{real_normed_div_algebra} star) n. hnorm (x pow n) = hnorm x pow n"
  by transfer (rule norm_power)

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

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

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

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

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

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

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

lemma abs_hnorm_cancel [simp]: "\a::'a::real_normed_vector star. \hnorm a\ = hnorm a"
  by transfer (rule abs_norm_cancel)

lemma hnorm_of_hypreal [simp]: "\r. hnorm (of_hypreal r::'a::real_normed_algebra_1 star) = \r\"
  by transfer (rule norm_of_real)

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

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

lemma hnorm_divide: "\a b::'a::{real_normed_field, field} star. hnorm (a / b) = hnorm a / hnorm b"
  by transfer (rule norm_divide)

lemma hypreal_hnorm_def [simp]: "\r::hypreal. hnorm r = \r\"
  by transfer (rule real_norm_def)

lemma hnorm_add_less:
  "\(x::'a::real_normed_vector star) y r s. hnorm x < r \ hnorm y < s \ hnorm (x + y) < r + s"
  by transfer (rule norm_add_less)

lemma hnorm_mult_less:
  "\(x::'a::real_normed_algebra star) y r s. hnorm x < r \ hnorm y < s \ hnorm (x * y) < r * s"
  by transfer (rule norm_mult_less)

lemma hnorm_scaleHR_less: "\x\ < r \ hnorm y < s \ hnorm (scaleHR x y) < r * s"
by (simp only: hnorm_scaleHR) (simp add: mult_strict_mono')

subsection \<open>Closure Laws for the Standard Reals\<close>

lemma Reals_add_cancel: "x + y \ \ \ y \ \ \ x \ \"
  by (drule (1) Reals_diff) simp

lemma SReal_hrabs: "x \ \ \ \x\ \ \"
  for x :: hypreal
  by (simp add: Reals_eq_Standard)

lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \ \"
  by (simp add: Reals_eq_Standard)

lemma SReal_divide_numeral: "r \ \ \ r / (numeral w::hypreal) \ \"
  by simp

text \<open>\<open>\<epsilon>\<close> is not in Reals because it is an infinitesimal\<close>
lemma SReal_epsilon_not_mem: "\ \ \"
  by (auto simp: SReal_def hypreal_of_real_not_eq_epsilon [symmetric])

lemma SReal_omega_not_mem: "\ \ \"
  by (auto simp: SReal_def hypreal_of_real_not_eq_omega [symmetric])

lemma SReal_UNIV_real: "{x. hypreal_of_real x \ \} = (UNIV::real set)"
  by simp

lemma SReal_iff: "x \ \ \ (\y. x = hypreal_of_real y)"
  by (simp add: SReal_def)

lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = \"
  by (simp add: Reals_eq_Standard Standard_def)

lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` \ = UNIV"
  by (simp add: Reals_eq_Standard Standard_def inj_star_of)

lemma SReal_dense: "x \ \ \ y \ \ \ x < y \ \r \ Reals. x < r \ r < y"
  for x y :: hypreal
  using dense by (fastforce simp add: SReal_def)

subsection \<open>Set of Finite Elements is a Subring of the Extended Reals\<close>

lemma HFinite_add: "x \ HFinite \ y \ HFinite \ x + y \ HFinite"
  unfolding HFinite_def by (blast intro!: Reals_add hnorm_add_less)

lemma HFinite_mult: "x \ HFinite \ y \ HFinite \ x * y \ HFinite"
  for x y :: "'a::real_normed_algebra star"
  unfolding HFinite_def by (blast intro!: Reals_mult hnorm_mult_less)

lemma HFinite_scaleHR: "x \ HFinite \ y \ HFinite \ scaleHR x y \ HFinite"
  by (auto simp: HFinite_def intro!: Reals_mult hnorm_scaleHR_less)

lemma HFinite_minus_iff: "- x \ HFinite \ x \ HFinite"
  by (simp add: HFinite_def)

lemma HFinite_star_of [simp]: "star_of x \ HFinite"
  by (simp add: HFinite_def) (metis SReal_hypreal_of_real gt_ex star_of_less star_of_norm)

lemma SReal_subset_HFinite: "(\::hypreal set) \ HFinite"
  by (auto simp add: SReal_def)

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

lemma HFinite_hrabs_iff [iff]: "\x\ \ HFinite \ x \ HFinite"
  for x :: hypreal
  by (simp add: HFinite_def)

lemma HFinite_hnorm_iff [iff]: "hnorm x \ HFinite \ x \ HFinite"
  for x :: hypreal
  by (simp add: HFinite_def)

lemma HFinite_numeral [simp]: "numeral w \ HFinite"
  unfolding star_numeral_def by (rule HFinite_star_of)

text \<open>As always with numerals, \<open>0\<close> and \<open>1\<close> are special cases.\<close>

lemma HFinite_0 [simp]: "0 \ HFinite"
  unfolding star_zero_def by (rule HFinite_star_of)

lemma HFinite_1 [simp]: "1 \ HFinite"
  unfolding star_one_def by (rule HFinite_star_of)

lemma hrealpow_HFinite: "x \ HFinite \ x ^ n \ HFinite"
  for x :: "'a::{real_normed_algebra,monoid_mult} star"
  by (induct n) (auto intro: HFinite_mult)

lemma HFinite_bounded:
  fixes x y :: hypreal
  assumes "x \ HFinite" and y: "y \ x" "0 \ y" shows "y \ HFinite"
proof (cases "x \ 0")
  case True
  then have "y = 0"
    using y by auto
  then show ?thesis
    by simp
next
  case False
  then show ?thesis
    using assms le_less_trans by (auto simp: HFinite_def)
qed

subsection \<open>Set of Infinitesimals is a Subring of the Hyperreals\<close>

lemma InfinitesimalI: "(\r. r \ \ \ 0 < r \ hnorm x < r) \ x \ Infinitesimal"
  by (simp add: Infinitesimal_def)

lemma InfinitesimalD: "x \ Infinitesimal \ \r \ Reals. 0 < r \ hnorm x < r"
  by (simp add: Infinitesimal_def)

lemma InfinitesimalI2: "(\r. 0 < r \ hnorm x < star_of r) \ x \ Infinitesimal"
  by (auto simp add: Infinitesimal_def SReal_def)

lemma InfinitesimalD2: "x \ Infinitesimal \ 0 < r \ hnorm x < star_of r"
  by (auto simp add: Infinitesimal_def SReal_def)

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

lemma Infinitesimal_add:
  assumes "x \ Infinitesimal" "y \ Infinitesimal"
  shows "x + y \ Infinitesimal"
proof (rule InfinitesimalI)
  show "hnorm (x + y) < r"
    if "r \ \" and "0 < r" for r :: "real star"
  proof -
    have "hnorm x < r/2" "hnorm y < r/2"
      using InfinitesimalD SReal_divide_numeral assms half_gt_zero that by blast+
    then show ?thesis
      using hnorm_add_less by fastforce
  qed
qed

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

lemma Infinitesimal_hnorm_iff: "hnorm x \ Infinitesimal \ x \ Infinitesimal"
  by (simp add: Infinitesimal_def)

lemma Infinitesimal_hrabs_iff [iff]: "\x\ \ Infinitesimal \ x \ Infinitesimal"
  for x :: hypreal
  by (simp add: abs_if)

lemma Infinitesimal_of_hypreal_iff [simp]:
  "(of_hypreal x::'a::real_normed_algebra_1 star) \ Infinitesimal \ x \ Infinitesimal"
  by (subst Infinitesimal_hnorm_iff [symmetric]) simp

lemma Infinitesimal_diff: "x \ Infinitesimal \ y \ Infinitesimal \ x - y \ Infinitesimal"
  using Infinitesimal_add [of x "- y"] by simp

lemma Infinitesimal_mult:
  fixes x y :: "'a::real_normed_algebra star"
  assumes "x \ Infinitesimal" "y \ Infinitesimal"
  shows "x * y \ Infinitesimal"
  proof (rule InfinitesimalI)
  show "hnorm (x * y) < r"
    if "r \ \" and "0 < r" for r :: "real star"
  proof -
    have "hnorm x < 1" "hnorm y < r"
      using assms that  by (auto simp add: InfinitesimalD)
    then show ?thesis
      using hnorm_mult_less by fastforce
  qed
qed

lemma Infinitesimal_HFinite_mult:
  fixes x y :: "'a::real_normed_algebra star"
  assumes "x \ Infinitesimal" "y \ HFinite"
  shows "x * y \ Infinitesimal"
proof (rule InfinitesimalI)
  obtain t where "hnorm y < t" "t \ Reals"
    using HFiniteD \<open>y \<in> HFinite\<close> by blast
  then have "t > 0"
    using hnorm_ge_zero le_less_trans by blast
  show "hnorm (x * y) < r"
    if "r \ \" and "0 < r" for r :: "real star"
  proof -
    have "hnorm x < r/t"
      by (meson InfinitesimalD Reals_divide \<open>hnorm y < t\<close> \<open>t \<in> \<real>\<close> assms(1) divide_pos_pos hnorm_ge_zero le_less_trans that)
    then have "hnorm (x * y) < (r / t) * t"
      using \<open>hnorm y < t\<close> hnorm_mult_less by blast
    then show ?thesis
      using \<open>0 < t\<close> by auto
  qed
qed

lemma Infinitesimal_HFinite_scaleHR:
  assumes "x \ Infinitesimal" "y \ HFinite"
  shows "scaleHR x y \ Infinitesimal"
proof (rule InfinitesimalI)
  obtain t where "hnorm y < t" "t \ Reals"
    using HFiniteD \<open>y \<in> HFinite\<close> by blast
  then have "t > 0"
    using hnorm_ge_zero le_less_trans by blast
  show "hnorm (scaleHR x y) < r"
    if "r \ \" and "0 < r" for r :: "real star"
  proof -
    have "\x\ * hnorm y < (r / t) * t"
      by (metis InfinitesimalD Reals_divide \<open>0 < t\<close> \<open>hnorm y < t\<close> \<open>t \<in> \<real>\<close> assms(1) divide_pos_pos hnorm_ge_zero hypreal_hnorm_def mult_strict_mono' that)
    then show ?thesis
      by (simp add: \<open>0 < t\<close> hnorm_scaleHR less_imp_not_eq2)
  qed
qed

lemma Infinitesimal_HFinite_mult2:
  fixes x y :: "'a::real_normed_algebra star"
  assumes "x \ Infinitesimal" "y \ HFinite"
  shows  "y * x \ Infinitesimal"
proof (rule InfinitesimalI)
  obtain t where "hnorm y < t" "t \ Reals"
    using HFiniteD \<open>y \<in> HFinite\<close> by blast
  then have "t > 0"
    using hnorm_ge_zero le_less_trans by blast
  show "hnorm (y * x) < r"
    if "r \ \" and "0 < r" for r :: "real star"
  proof -
    have "hnorm x < r/t"
      by (meson InfinitesimalD Reals_divide \<open>hnorm y < t\<close> \<open>t \<in> \<real>\<close> assms(1) divide_pos_pos hnorm_ge_zero le_less_trans that)
    then have "hnorm (y * x) < t * (r / t)"
      using \<open>hnorm y < t\<close> hnorm_mult_less by blast
    then show ?thesis
      using \<open>0 < t\<close> by auto
  qed
qed

lemma Infinitesimal_scaleR2:
  assumes "x \ Infinitesimal" shows "a *\<^sub>R x \ Infinitesimal"
    by (metis HFinite_star_of Infinitesimal_HFinite_mult2 Infinitesimal_hnorm_iff assms hnorm_scaleR hypreal_hnorm_def star_of_norm)

lemma Compl_HFinite: "- HFinite = HInfinite"
  proof -
  have "r < hnorm x" if *: "\s. s \ \ \ s \ hnorm x" and "r \ \"
    for x :: "'a star" and r :: hypreal
    using * [of "r+1"] \<open>r \<in> \<real>\<close> by auto
  then show ?thesis
    by (auto simp add: HInfinite_def HFinite_def linorder_not_less)
qed

lemma HInfinite_inverse_Infinitesimal:
  "x \ HInfinite \ inverse x \ Infinitesimal"
  for x :: "'a::real_normed_div_algebra star"
  by (simp add: HInfinite_def InfinitesimalI hnorm_inverse inverse_less_imp_less)

lemma inverse_Infinitesimal_iff_HInfinite:
  "x \ 0 \ inverse x \ Infinitesimal \ x \ HInfinite"
  for x :: "'a::real_normed_div_algebra star"
  by (metis Compl_HFinite Compl_iff HInfinite_inverse_Infinitesimal InfinitesimalD Infinitesimal_HFinite_mult Reals_1 hnorm_one left_inverse less_irrefl zero_less_one)

lemma HInfiniteI: "(\r. r \ \ \ r < hnorm x) \ x \ HInfinite"
  by (simp add: HInfinite_def)

lemma HInfiniteD: "x \ HInfinite \ r \ \ \ r < hnorm x"
  by (simp add: HInfinite_def)

lemma HInfinite_mult:
  fixes x y :: "'a::real_normed_div_algebra star"
  assumes "x \ HInfinite" "y \ HInfinite" shows "x * y \ HInfinite"
proof (rule HInfiniteI, simp only: hnorm_mult)
  have "x \ 0"
    using Compl_HFinite HFinite_0 assms by blast
  show "r < hnorm x * hnorm y"
    if "r \ \" for r :: "real star"
  proof -
    have "r = r * 1"
      by simp
    also have "\ < hnorm x * hnorm y"
      by (meson HInfiniteD Reals_1 \<open>x \<noteq> 0\<close> assms le_numeral_extra(1) mult_strict_mono that zero_less_hnorm_iff)
    finally show ?thesis .
  qed
qed

lemma hypreal_add_zero_less_le_mono: "r < x \ 0 \ y \ r < x + y"
  for r x y :: hypreal
  by simp

lemma HInfinite_add_ge_zero: "x \ HInfinite \ 0 \ y \ 0 \ x \ x + y \ HInfinite"
  for x y :: hypreal
  by (auto simp: abs_if add.commute HInfinite_def)

lemma HInfinite_add_ge_zero2: "x \ HInfinite \ 0 \ y \ 0 \ x \ y + x \ HInfinite"
  for x y :: hypreal
  by (auto intro!: HInfinite_add_ge_zero simp add: add.commute)

lemma HInfinite_add_gt_zero: "x \ HInfinite \ 0 < y \ 0 < x \ x + y \ HInfinite"
  for x y :: hypreal
  by (blast intro: HInfinite_add_ge_zero order_less_imp_le)

lemma HInfinite_minus_iff: "- x \ HInfinite \ x \ HInfinite"
  by (simp add: HInfinite_def)

lemma HInfinite_add_le_zero: "x \ HInfinite \ y \ 0 \ x \ 0 \ x + y \ HInfinite"
  for x y :: hypreal
  by (metis (no_types, lifting) HInfinite_add_ge_zero2 HInfinite_minus_iff add.inverse_distrib_swap neg_0_le_iff_le)

lemma HInfinite_add_lt_zero: "x \ HInfinite \ y < 0 \ x < 0 \ x + y \ HInfinite"
  for x y :: hypreal
  by (blast intro: HInfinite_add_le_zero order_less_imp_le)

lemma not_Infinitesimal_not_zero: "x \ Infinitesimal \ x \ 0"
  by auto

lemma HFinite_diff_Infinitesimal_hrabs:
  "x \ HFinite - Infinitesimal \ \x\ \ HFinite - Infinitesimal"
  for x :: hypreal
  by blast

lemma hnorm_le_Infinitesimal: "e \ Infinitesimal \ hnorm x \ e \ x \ Infinitesimal"
  by (auto simp: Infinitesimal_def abs_less_iff)

lemma hnorm_less_Infinitesimal: "e \ Infinitesimal \ hnorm x < e \ x \ Infinitesimal"
  by (erule hnorm_le_Infinitesimal, erule order_less_imp_le)

lemma hrabs_le_Infinitesimal: "e \ Infinitesimal \ \x\ \ e \ x \ Infinitesimal"
  for x :: hypreal
  by (erule hnorm_le_Infinitesimal) simp

lemma hrabs_less_Infinitesimal: "e \ Infinitesimal \ \x\ < e \ x \ Infinitesimal"
  for x :: hypreal
  by (erule hnorm_less_Infinitesimal) simp

lemma Infinitesimal_interval:
  "e \ Infinitesimal \ e' \ Infinitesimal \ e' < x \ x < e \ x \ Infinitesimal"
  for x :: hypreal
  by (auto simp add: Infinitesimal_def abs_less_iff)

lemma Infinitesimal_interval2:
  "e \ Infinitesimal \ e' \ Infinitesimal \ e' \ x \ x \ e \ x \ Infinitesimal"
  for x :: hypreal
  by (auto intro: Infinitesimal_interval simp add: order_le_less)

lemma lemma_Infinitesimal_hyperpow: "x \ Infinitesimal \ 0 < N \ \x pow N\ \ \x\"
  for x :: hypreal
  apply (clarsimp simp: Infinitesimal_def)
  by (metis Reals_1 abs_ge_zero hyperpow_Suc_le_self2 hyperpow_hrabs hypnat_gt_zero_iff2 zero_less_one)

lemma Infinitesimal_hyperpow: "x \ Infinitesimal \ 0 < N \ x pow N \ Infinitesimal"
  for x :: hypreal
  using hrabs_le_Infinitesimal lemma_Infinitesimal_hyperpow by blast

lemma hrealpow_hyperpow_Infinitesimal_iff:
  "(x ^ n \ Infinitesimal) \ x pow (hypnat_of_nat n) \ Infinitesimal"
  by (simp only: hyperpow_hypnat_of_nat)

lemma Infinitesimal_hrealpow: "x \ Infinitesimal \ 0 < n \ x ^ n \ Infinitesimal"
  for x :: hypreal
  by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow)

lemma not_Infinitesimal_mult:
  "x \ Infinitesimal \ y \ Infinitesimal \ x * y \ Infinitesimal"
  for x y :: "'a::real_normed_div_algebra star"
  by (metis (no_types, lifting) inverse_Infinitesimal_iff_HInfinite ComplI Compl_HFinite Infinitesimal_HFinite_mult divide_inverse eq_divide_imp inverse_inverse_eq mult_zero_right)

lemma Infinitesimal_mult_disj: "x * y \ Infinitesimal \ x \ Infinitesimal \ y \ Infinitesimal"
  for x y :: "'a::real_normed_div_algebra star"
  using not_Infinitesimal_mult by blast

lemma HFinite_Infinitesimal_not_zero: "x \ HFinite-Infinitesimal \ x \ 0"
  by blast

lemma HFinite_Infinitesimal_diff_mult:
  "x \ HFinite - Infinitesimal \ y \ HFinite - Infinitesimal \ x * y \ HFinite - Infinitesimal"
  for x y :: "'a::real_normed_div_algebra star"
  by (simp add: HFinite_mult not_Infinitesimal_mult)

lemma Infinitesimal_subset_HFinite: "Infinitesimal \ HFinite"
  using HFinite_def InfinitesimalD Reals_1 zero_less_one by blast

lemma Infinitesimal_star_of_mult: "x \ Infinitesimal \ x * star_of r \ Infinitesimal"
  for x :: "'a::real_normed_algebra star"
  by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult])

lemma Infinitesimal_star_of_mult2: "x \ Infinitesimal \ star_of r * x \ Infinitesimal"
  for x :: "'a::real_normed_algebra star"
  by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2])

subsection \<open>The Infinitely Close Relation\<close>

lemma mem_infmal_iff: "x \ 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 approx_sym: "x \ y \ y \ x"
  by (metis Infinitesimal_minus_iff approx_def minus_diff_eq)

lemma approx_trans:
  assumes "x \ y" "y \ z" shows "x \ z"
proof -
  have "x - y \ Infinitesimal" "z - y \ Infinitesimal"
    using assms approx_def approx_sym by auto
  then have "x - z \ Infinitesimal"
    using Infinitesimal_diff by force
  then show ?thesis
    by (simp add: approx_def)
qed

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 approx_reorient: "x \ y \ y \ x"
  by (blast intro: approx_sym)

text \<open>Reorientation simplification procedure: reorients (polymorphic)
  \<open>0 = x\<close>, \<open>1 = x\<close>, \<open>nnn = x\<close> provided \<open>x\<close> isn't \<open>0\<close>, \<open>1\<close> or a numeral.\<close>
simproc_setup approx_reorient_simproc
  ("0 \ x" | "1 \ y" | "numeral w \ z" | "- 1 \ y" | "- numeral w \ r") =
\<open>
  let val rule = @{thm approx_reorient} RS eq_reflection
      fun proc phi ss ct =
        case Thm.term_of ct of
          _ $ t $ u => if can HOLogic.dest_number u then NONE
            else if can HOLogic.dest_number t then SOME rule else NONE
        | _ => NONE
  in proc end
\<close>

lemma Infinitesimal_approx_minus: "x - y \ Infinitesimal \ x \ y"
  by (simp add: approx_minus_iff [symmetric] mem_infmal_iff)

lemma approx_monad_iff: "x \ y \ monad x = monad y"
  apply (simp add: monad_def set_eq_iff)
  using approx_reorient approx_trans by blast

lemma Infinitesimal_approx: "x \ Infinitesimal \ y \ Infinitesimal \ x \ y"
  by (simp add: Infinitesimal_diff approx_def)

lemma approx_add: "a \ b \ c \ d \ a + c \ b + d"
proof (unfold approx_def)
  assume inf: "a - b \ Infinitesimal" "c - d \ Infinitesimal"
  have "a + c - (b + d) = (a - b) + (c - d)" by simp
  also have "... \ Infinitesimal"
    using inf by (rule Infinitesimal_add)
  finally show "a + c - (b + d) \ Infinitesimal" .
qed

lemma approx_minus: "a \ b \ - a \ - b"
  by (metis approx_def approx_sym minus_diff_eq minus_diff_minus)

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_diff: "a \ b \ c \ d \ a - c \ b - d"
  using approx_add [of a b "- c" "- d"] by simp

lemma approx_mult1: "a \ b \ c \ HFinite \ a * c \ b * c"
  for a b c :: "'a::real_normed_algebra star"
  by (simp add: approx_def Infinitesimal_HFinite_mult left_diff_distrib [symmetric])

lemma approx_mult2: "a \ b \ c \ HFinite \ c * a \ c * b"
  for a b c :: "'a::real_normed_algebra star"
  by (simp add: approx_def Infinitesimal_HFinite_mult2 right_diff_distrib [symmetric])

lemma approx_mult_subst: "u \ v * x \ x \ y \ v \ HFinite \ u \ v * y"
  for u v x y :: "'a::real_normed_algebra star"
  by (blast intro: approx_mult2 approx_trans)

lemma approx_mult_subst2: "u \ x * v \ x \ y \ v \ HFinite \ u \ y * v"
  for u v x y :: "'a::real_normed_algebra star"
  by (blast intro: approx_mult1 approx_trans)

lemma approx_mult_subst_star_of: "u \ x * star_of v \ x \ y \ u \ y * star_of v"
  for u x y :: "'a::real_normed_algebra star"
  by (auto intro: approx_mult_subst2)

lemma approx_eq_imp: "a = b \ a \ b"
  by (simp add: approx_def)

lemma Infinitesimal_minus_approx: "x \ Infinitesimal \ - x \ x"
  by (blast intro: Infinitesimal_minus_iff [THEN iffD2] mem_infmal_iff [THEN iffD1] approx_trans2)

lemma bex_Infinitesimal_iff: "(\y \ Infinitesimal. x - z = y) \ x \ z"
  by (simp add: approx_def)

lemma bex_Infinitesimal_iff2: "(\y \ Infinitesimal. x = z + y) \ x \ z"
  by (force simp add: bex_Infinitesimal_iff [symmetric])

lemma Infinitesimal_add_approx: "y \ Infinitesimal \ x + y = z \ x \ z"
  using approx_sym bex_Infinitesimal_iff2 by blast

lemma Infinitesimal_add_approx_self: "y \ Infinitesimal \ x \ x + y"
  by (simp add: Infinitesimal_add_approx)

lemma Infinitesimal_add_approx_self2: "y \ Infinitesimal \ x \ y + x"
  by (auto dest: Infinitesimal_add_approx_self simp add: add.commute)

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

lemma Infinitesimal_add_cancel: "y \ Infinitesimal \ x + y \ z \ x \ z"
  using Infinitesimal_add_approx approx_trans by blast

lemma Infinitesimal_add_right_cancel: "y \ Infinitesimal \ x \ z + y \ x \ z"
  by (metis Infinitesimal_add_approx_self approx_monad_iff)

lemma approx_add_left_cancel: "d + b \ d + c \ b \ c"
  by (metis add_diff_cancel_left bex_Infinitesimal_iff)

lemma approx_add_right_cancel: "b + d \ c + d \ b \ c"
  by (simp add: approx_def)

lemma approx_add_mono1: "b \ c \ d + b \ d + c"
  by (simp add: approx_add)

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 \ HFinite \ x \ y \ y \ HFinite"
  by (metis HFinite_add Infinitesimal_subset_HFinite approx_sym subsetD bex_Infinitesimal_iff2)

lemma approx_star_of_HFinite: "x \ star_of D \ x \ 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"
  for a b c d :: "'a::real_normed_algebra star"
  by (meson approx_HFinite approx_mult2 approx_mult_subst2 approx_sym)

lemma scaleHR_left_diff_distrib: "\a b x. scaleHR (a - b) x = scaleHR a x - scaleHR b x"
  by transfer (rule scaleR_left_diff_distrib)

lemma approx_scaleR1: "a \ star_of b \ c \ HFinite \ scaleHR a c \ b *\<^sub>R c"
  unfolding approx_def
  by (metis Infinitesimal_HFinite_scaleHR scaleHR_def scaleHR_left_diff_distrib star_scaleR_def starfun2_star_of)

lemma approx_scaleR2: "a \ b \ c *\<^sub>R a \ c *\<^sub>R b"
  by (simp add: approx_def Infinitesimal_scaleR2 scaleR_right_diff_distrib [symmetric])

lemma approx_scaleR_HFinite: "a \ star_of b \ c \ d \ d \ HFinite \ scaleHR a c \ b *\<^sub>R d"
  by (meson approx_HFinite approx_scaleR1 approx_scaleR2 approx_sym approx_trans)

lemma approx_mult_star_of: "a \ star_of b \ c \ star_of d \ a * c \ star_of b * star_of d"
  for a c :: "'a::real_normed_algebra star"
  by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)

lemma approx_SReal_mult_cancel_zero:
  fixes a x :: hypreal
  assumes "a \ \" "a \ 0" "a * x \ 0" shows "x \ 0"
proof -
  have "inverse a \ HFinite"
    using Reals_inverse SReal_subset_HFinite assms(1) by blast
  then show ?thesis
    using assms by (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
qed

lemma approx_mult_SReal1: "a \ \ \ x \ 0 \ x * a \ 0"
  for a x :: hypreal
  by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)

lemma approx_mult_SReal2: "a \ \ \ x \ 0 \ a * x \ 0"
  for a x :: hypreal
  by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)

lemma approx_mult_SReal_zero_cancel_iff [simp]: "a \ \ \ a \ 0 \ a * x \ 0 \ x \ 0"
  for a x :: hypreal
  by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)

lemma approx_SReal_mult_cancel:
  fixes a w z :: hypreal
  assumes "a \ \" "a \ 0" "a * w \ a * z" shows "w \ z"
proof -
  have "inverse a \ HFinite"
    using Reals_inverse SReal_subset_HFinite assms(1) by blast
  then show ?thesis
    using assms by (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
qed

lemma approx_SReal_mult_cancel_iff1 [simp]: "a \ \ \ a \ 0 \ a * w \ a * z \ w \ z"
  for a w z :: hypreal
  by (meson SReal_subset_HFinite approx_SReal_mult_cancel approx_mult2 subsetD)

lemma approx_le_bound:
  fixes z :: hypreal
  assumes "z \ f" " f \ g" "g \ z" shows "f \ z"
proof -
  obtain y where "z \ g + y" and "y \ Infinitesimal" "f = g + y"
    using assms bex_Infinitesimal_iff2 by auto
  then have "z - g \ Infinitesimal"
    using assms(3) hrabs_le_Infinitesimal by auto
  then show ?thesis
    by (metis approx_def approx_trans2 assms(2))
qed

lemma approx_hnorm: "x \ y \ hnorm x \ hnorm y"
  for x y :: "'a::real_normed_vector star"
proof (unfold approx_def)
  assume "x - y \ Infinitesimal"
  then have "hnorm (x - y) \ Infinitesimal"
    by (simp only: Infinitesimal_hnorm_iff)
  moreover have "(0::real star) \ Infinitesimal"
    by (rule Infinitesimal_zero)
  moreover have "0 \ \hnorm x - hnorm y\"
    by (rule abs_ge_zero)
  moreover have "\hnorm x - hnorm y\ \ hnorm (x - y)"
    by (rule hnorm_triangle_ineq3)
  ultimately have "\hnorm x - hnorm y\ \ Infinitesimal"
    by (rule Infinitesimal_interval2)
  then show "hnorm x - hnorm y \ Infinitesimal"
    by (simp only: Infinitesimal_hrabs_iff)
qed

subsection \<open>Zero is the Only Infinitesimal that is also a Real\<close>

lemma Infinitesimal_less_SReal: "x \ \ \ y \ Infinitesimal \ 0 < x \ y < x"
  for x y :: hypreal
  using InfinitesimalD by fastforce

lemma Infinitesimal_less_SReal2: "y \ Infinitesimal \ \r \ Reals. 0 < r \ y < r"
  for y :: hypreal
  by (blast intro: Infinitesimal_less_SReal)

lemma SReal_not_Infinitesimal: "0 < y \ y \ \ ==> y \ Infinitesimal"
  for y :: hypreal
  by (auto simp add: Infinitesimal_def abs_if)

lemma SReal_minus_not_Infinitesimal: "y < 0 \ y \ \ \ y \ Infinitesimal"
  for y :: hypreal
  using Infinitesimal_minus_iff Reals_minus SReal_not_Infinitesimal neg_0_less_iff_less by blast

lemma SReal_Int_Infinitesimal_zero: "\ Int Infinitesimal = {0::hypreal}"
  proof -
  have "x = 0" if "x \ \" "x \ Infinitesimal" for x :: "real star"
    using that SReal_minus_not_Infinitesimal SReal_not_Infinitesimal not_less_iff_gr_or_eq by blast
  then show ?thesis
    by auto
qed

lemma SReal_Infinitesimal_zero: "x \ \ \ x \ Infinitesimal \ x = 0"
  for x :: hypreal
  using SReal_Int_Infinitesimal_zero by blast

lemma SReal_HFinite_diff_Infinitesimal: "x \ \ \ x \ 0 \ x \ HFinite - Infinitesimal"
  for x :: hypreal
  by (auto dest: SReal_Infinitesimal_zero SReal_subset_HFinite [THEN subsetD])

lemma hypreal_of_real_HFinite_diff_Infinitesimal:
  "hypreal_of_real x \ 0 \ hypreal_of_real x \ HFinite - Infinitesimal"
  by (rule SReal_HFinite_diff_Infinitesimal) auto

lemma star_of_Infinitesimal_iff_0 [iff]: "star_of x \ Infinitesimal \ x = 0"
proof
  show "x = 0" if "star_of x \ Infinitesimal"
  proof -
    have "hnorm (star_n (\n. x)) \ Standard"
      by (metis Reals_eq_Standard SReal_iff star_of_def star_of_norm)
    then show ?thesis
      by (metis InfinitesimalD2 less_irrefl star_of_norm that zero_less_norm_iff)
  qed
qed auto

lemma star_of_HFinite_diff_Infinitesimal: "x \ 0 \ star_of x \ HFinite - Infinitesimal"
  by simp

lemma numeral_not_Infinitesimal [simp]:
  "numeral w \ (0::hypreal) \ (numeral w :: hypreal) \ Infinitesimal"
  by (fast dest: Reals_numeral [THEN SReal_Infinitesimal_zero])

text \<open>Again: \<open>1\<close> is a special case, but not \<open>0\<close> this time.\<close>
lemma one_not_Infinitesimal [simp]:
  "(1::'a::{real_normed_vector,zero_neq_one} star) \ Infinitesimal"
  by (metis star_of_Infinitesimal_iff_0 star_one_def zero_neq_one)

lemma approx_SReal_not_zero: "y \ \ \ x \ y \ y \ 0 \ x \ 0"
  for x y :: hypreal
  using SReal_Infinitesimal_zero approx_sym mem_infmal_iff by auto

lemma HFinite_diff_Infinitesimal_approx:
  "x \ y \ y \ HFinite - Infinitesimal \ x \ HFinite - Infinitesimal"
  by (meson Diff_iff approx_HFinite approx_sym approx_trans3 mem_infmal_iff)

text \<open>The premise \<open>y \<noteq> 0\<close> is essential; otherwise \<open>x / y = 0\<close> and we lose the
  \<open>HFinite\<close> premise.\<close>
lemma Infinitesimal_ratio:
  "y \ 0 \ y \ Infinitesimal \ x / y \ HFinite \ x \ Infinitesimal"
  for x y :: "'a::{real_normed_div_algebra,field} star"
  using Infinitesimal_HFinite_mult by fastforce

lemma Infinitesimal_SReal_divide: "x \ Infinitesimal \ y \ \ \ x / y \ Infinitesimal"
  for x y :: hypreal
  by (metis HFinite_star_of Infinitesimal_HFinite_mult Reals_inverse SReal_iff divide_inverse)

section \<open>Standard Part Theorem\<close>

text \<open>
  Every finite \<open>x \<in> R*\<close> is infinitely close to a unique real number
  (i.e. a member of \<open>Reals\<close>).
\<close>

subsection \<open>Uniqueness: Two Infinitely Close Reals are Equal\<close>

lemma star_of_approx_iff [simp]: "star_of x \ star_of y \ x = y"
  by (metis approx_def right_minus_eq star_of_Infinitesimal_iff_0 star_of_simps(2))

lemma SReal_approx_iff: "x \ \ \ y \ \ \ x \ y \ x = y"
  for x y :: hypreal
  by (meson Reals_diff SReal_Infinitesimal_zero approx_def approx_refl right_minus_eq)

lemma numeral_approx_iff [simp]:
  "(numeral v \ (numeral w :: 'a::{numeral,real_normed_vector} star)) = (numeral v = (numeral w :: 'a))"
  by (metis star_of_approx_iff star_of_numeral)

text \<open>And also for \<open>0 \<approx> #nn\<close> and \<open>1 \<approx> #nn\<close>, \<open>#nn \<approx> 0\<close> and \<open>#nn \<approx> 1\<close>.\<close>
lemma [simp]:
  "(numeral w \ (0::'a::{numeral,real_normed_vector} star)) = (numeral w = (0::'a))"
  "((0::'a::{numeral,real_normed_vector} star) \ numeral w) = (numeral w = (0::'a))"
  "(numeral w \ (1::'b::{numeral,one,real_normed_vector} star)) = (numeral w = (1::'b))"
  "((1::'b::{numeral,one,real_normed_vector} star) \ numeral w) = (numeral w = (1::'b))"
  "\ (0 \ (1::'c::{zero_neq_one,real_normed_vector} star))"
  "\ (1 \ (0::'c::{zero_neq_one,real_normed_vector} star))"
  unfolding star_numeral_def star_zero_def star_one_def star_of_approx_iff
  by (auto intro: sym)

lemma star_of_approx_numeral_iff [simp]: "star_of k \ numeral w \ k = numeral w"
  by (subst star_of_approx_iff [symmetric]) auto

lemma star_of_approx_zero_iff [simp]: "star_of k \ 0 \ k = 0"
  by (simp_all add: star_of_approx_iff [symmetric])

lemma star_of_approx_one_iff [simp]: "star_of k \ 1 \ k = 1"
  by (simp_all add: star_of_approx_iff [symmetric])

lemma approx_unique_real: "r \ \ \ s \ \ \ r \ x \ s \ x \ r = s"
  for r s :: hypreal
  by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)

subsection \<open>Existence of Unique Real Infinitely Close\<close>

subsubsection \<open>Lifting of the Ub and Lub Properties\<close>

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

lemma hypreal_of_real_isLub_iff:
  "isLub \ (hypreal_of_real ` Q) (hypreal_of_real Y) = isLub (UNIV :: real set) Q Y" (is "?lhs = ?rhs")
  for Q :: "real set" and Y :: real
proof
  assume ?lhs
  then show ?rhs
    by (simp add: isLub_def leastP_def) (metis hypreal_of_real_isUb_iff mem_Collect_eq setge_def star_of_le)
next
  assume ?rhs
  then show ?lhs
  apply (simp add: isLub_def leastP_def hypreal_of_real_isUb_iff setge_def)
    by (metis SReal_iff hypreal_of_real_isUb_iff isUb_def star_of_le)
qed

lemma lemma_isUb_hypreal_of_real: "isUb \ P Y \ \Yo. isUb \ P (hypreal_of_real Yo)"
  by (auto simp add: SReal_iff isUb_def)

lemma lemma_isLub_hypreal_of_real: "isLub \ P Y \ \Yo. isLub \ P (hypreal_of_real Yo)"
  by (auto simp add: isLub_def leastP_def isUb_def SReal_iff)

lemma SReal_complete:
  fixes P :: "hypreal set"
  assumes "isUb \ P Y" "P \ \" "P \ {}"
    shows "\t. isLub \ P t"
proof -
  obtain Q where "P = hypreal_of_real ` Q"
    by (metis \<open>P \<subseteq> \<real>\<close> hypreal_of_real_image subset_imageE)
  then show ?thesis
    by (metis assms(1) \<open>P \<noteq> {}\<close> equals0I hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff image_empty lemma_isUb_hypreal_of_real reals_complete)
qed

text \<open>Lemmas about lubs.\<close>

lemma lemma_st_part_lub:
  fixes x :: hypreal
  assumes "x \ HFinite"
  shows "\t. isLub \ {s. s \ \ \ s < x} t"
proof -
  obtain t where t: "t \ \" "hnorm x < t"
    using HFiniteD assms by blast
  then have "isUb \ {s. s \ \ \ s < x} t"
    by (simp add: abs_less_iff isUbI le_less_linear less_imp_not_less setleI)
  moreover have "\y. y \ \ \ y < x"
    using t by (rule_tac x = "-t" in exI) (auto simp add: abs_less_iff)
  ultimately show ?thesis
    using SReal_complete by fastforce
qed

lemma hypreal_setle_less_trans: "S *<= x \ x < y \ S *<= y"
  for x y :: hypreal
  by (meson le_less_trans less_imp_le setle_def)

lemma hypreal_gt_isUb: "isUb R S x \ x < y \ y \ R \ isUb R S y"
  for x y :: hypreal
  using hypreal_setle_less_trans isUb_def by blast

lemma lemma_SReal_ub: "x \ \ \ isUb \ {s. s \ \ \ s < x} x"
  for x :: hypreal
  by (auto intro: isUbI setleI order_less_imp_le)

lemma lemma_SReal_lub:
  fixes x :: hypreal
  assumes "x \ \" shows "isLub \ {s. s \ \ \ s < x} x"
proof -
  have "x \ y" if "isUb \ {s \ \. s < x} y" for y
  proof -
    have "y \ \"
      using isUbD2a that by blast
    show ?thesis
    proof (cases x y rule: linorder_cases)
      case greater
      then obtain r where "y < r" "r < x"
        using dense by blast
      then show ?thesis
        using isUbD [OF that]
        by simp (meson SReal_dense \<open>y \<in> \<real>\<close> assms greater not_le)
    qed auto
  qed
  with assms show ?thesis
    by (simp add: isLubI2 isUbI setgeI setleI)
qed

lemma lemma_st_part_major:
  fixes x r t :: hypreal
  assumes x: "x \ HFinite" and r: "r \ \" "0 < r" and t: "isLub \ {s. s \ \ \ s < x} t"
  shows "\x - t\ < r"
proof -
  have "t \ \"
    using isLubD1a t by blast
  have lemma_st_part_gt_ub: "x < r \ r \ \ \ isUb \ {s. s \ \ \ s < x} r"
    for  r :: hypreal
    by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)

  have "isUb \ {s \ \. s < x} t"
    by (simp add: t isLub_isUb)
  then have "\ r + t < x"
    by (metis (mono_tags, lifting) Reals_add \<open>t \<in> \<real>\<close> add_le_same_cancel2 isUbD leD mem_Collect_eq r)
  then have "x - t \ r"
    by simp
  moreover have "\ x < t - r"
    using lemma_st_part_gt_ub isLub_le_isUb \<open>t \<in> \<real>\<close> r t x by fastforce
  then have "- (x - t) \ r"
    by linarith
  moreover have False if "x - t = r \ - (x - t) = r"
  proof -
    have "x \ \"
      by (metis \<open>t \<in> \<real>\<close> \<open>r \<in> \<real>\<close> that Reals_add_cancel Reals_minus_iff add_uminus_conv_diff)
    then have "isLub \ {s \ \. s < x} x"
      by (rule lemma_SReal_lub)
    then show False
      using r t that x isLub_unique by force
  qed
  ultimately show ?thesis
    using abs_less_iff dual_order.order_iff_strict by blast
qed

lemma lemma_st_part_major2:
  "x \ HFinite \ isLub \ {s. s \ \ \ s < x} t \ \r \ Reals. 0 < r \ \x - t\ < r"
  for x t :: hypreal
  by (blast dest!: lemma_st_part_major)

text\<open>Existence of real and Standard Part Theorem.\<close>

lemma lemma_st_part_Ex: "x \ HFinite \ \t\Reals. \r \ Reals. 0 < r \ \x - t\ < r"
  for x :: hypreal
  by (meson isLubD1a lemma_st_part_lub lemma_st_part_major2)

lemma st_part_Ex: "x \ HFinite \ \t\Reals. x \ t"
  for x :: hypreal
  by (metis InfinitesimalI approx_def hypreal_hnorm_def lemma_st_part_Ex)

text \<open>There is a unique real infinitely close.\<close>
lemma st_part_Ex1: "x \ HFinite \ \!t::hypreal. t \ \ \ x \ t"
  by (meson SReal_approx_iff approx_trans2 st_part_Ex)

subsection \<open>Finite, Infinite and Infinitesimal\<close>

lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}"
  using Compl_HFinite by blast

lemma HFinite_not_HInfinite:
  assumes x: "x \ HFinite" shows "x \ HInfinite"
  using Compl_HFinite x by blast

lemma not_HFinite_HInfinite: "x \ HFinite \ x \ HInfinite"
  using Compl_HFinite by blast

lemma HInfinite_HFinite_disj: "x \ HInfinite \ x \ HFinite"
  by (blast intro: not_HFinite_HInfinite)

lemma HInfinite_HFinite_iff: "x \ HInfinite \ x \ HFinite"
  by (blast dest: HFinite_not_HInfinite not_HFinite_HInfinite)

lemma HFinite_HInfinite_iff: "x \ HFinite \ x \ HInfinite"
  by (simp add: HInfinite_HFinite_iff)

lemma HInfinite_diff_HFinite_Infinitesimal_disj:
  "x \ Infinitesimal \ x \ HInfinite \ x \ HFinite - Infinitesimal"
  by (fast intro: not_HFinite_HInfinite)

lemma HFinite_inverse: "x \ HFinite \ x \ Infinitesimal \ inverse x \ HFinite"
  for x :: "'a::real_normed_div_algebra star"
  using HInfinite_inverse_Infinitesimal not_HFinite_HInfinite by force

lemma HFinite_inverse2: "x \ HFinite - Infinitesimal \ inverse x \ HFinite"
  for x :: "'a::real_normed_div_algebra star"
  by (blast intro: HFinite_inverse)

text \<open>Stronger statement possible in fact.\<close>
lemma Infinitesimal_inverse_HFinite: "x \ Infinitesimal \ inverse x \ HFinite"
  for x :: "'a::real_normed_div_algebra star"
  using HFinite_HInfinite_iff HInfinite_inverse_Infinitesimal by fastforce

lemma HFinite_not_Infinitesimal_inverse:
  "x \ HFinite - Infinitesimal \ inverse x \ HFinite - Infinitesimal"
  for x :: "'a::real_normed_div_algebra star"
  using HFinite_Infinitesimal_not_zero HFinite_inverse2 Infinitesimal_HFinite_mult2 by fastforce

lemma approx_inverse:
  fixes x y :: "'a::real_normed_div_algebra star"
  assumes "x \ y" and y: "y \ HFinite - Infinitesimal" shows "inverse x \ inverse y"
proof -
  have x: "x \ HFinite - Infinitesimal"
    using HFinite_diff_Infinitesimal_approx assms(1) y by blast
  with y HFinite_inverse2 have "inverse x \ HFinite" "inverse y \ HFinite"
    by blast+
  then have "inverse y * x \ 1"
    by (metis Diff_iff approx_mult2 assms(1) left_inverse not_Infinitesimal_not_zero y)
  then show ?thesis
    by (metis (no_types, lifting) DiffD2 HFinite_Infinitesimal_not_zero Infinitesimal_mult_disj x approx_def approx_sym left_diff_distrib left_inverse)
qed

(*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
lemmas star_of_approx_inverse = star_of_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
lemmas hypreal_of_real_approx_inverse =  hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]

lemma inverse_add_Infinitesimal_approx:
  "x \ HFinite - Infinitesimal \ h \ Infinitesimal \ inverse (x + h) \ inverse x"
  for x h :: "'a::real_normed_div_algebra star"
  by (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self)

lemma inverse_add_Infinitesimal_approx2:
  "x \ HFinite - Infinitesimal \ h \ Infinitesimal \ inverse (h + x) \ inverse x"
  for x h :: "'a::real_normed_div_algebra star"
  by (metis add.commute inverse_add_Infinitesimal_approx)

lemma inverse_add_Infinitesimal_approx_Infinitesimal:
  "x \ HFinite - Infinitesimal \ h \ Infinitesimal \ inverse (x + h) - inverse x \ h"
  for x h :: "'a::real_normed_div_algebra star"
  by (meson Infinitesimal_approx bex_Infinitesimal_iff inverse_add_Infinitesimal_approx)

lemma Infinitesimal_square_iff: "x \ Infinitesimal \ x * x \ Infinitesimal"
  for x :: "'a::real_normed_div_algebra star"
  using Infinitesimal_mult Infinitesimal_mult_disj by auto
declare Infinitesimal_square_iff [symmetric, simp]

lemma HFinite_square_iff [simp]: "x * x \ HFinite \ x \ HFinite"
  for x :: "'a::real_normed_div_algebra star"
  using HFinite_HInfinite_iff HFinite_mult HInfinite_mult by blast

lemma HInfinite_square_iff [simp]: "x * x \ HInfinite \ x \ HInfinite"
  for x :: "'a::real_normed_div_algebra star"
  by (auto simp add: HInfinite_HFinite_iff)

lemma approx_HFinite_mult_cancel: "a \ HFinite - Infinitesimal \ a * w \ a * z \ w \ z"
  for a w z :: "'a::real_normed_div_algebra star"
  by (metis DiffD2 Infinitesimal_mult_disj bex_Infinitesimal_iff right_diff_distrib)

lemma approx_HFinite_mult_cancel_iff1: "a \ HFinite - Infinitesimal \ a * w \ a * z \ w \ z"
  for a w z :: "'a::real_normed_div_algebra star"
  by (auto intro: approx_mult2 approx_HFinite_mult_cancel)

lemma HInfinite_HFinite_add_cancel: "x + y \ HInfinite \ y \ HFinite \ x \ HInfinite"
  using HFinite_add HInfinite_HFinite_iff by blast

lemma HInfinite_HFinite_add: "x \ HInfinite \ y \ HFinite \ x + y \ HInfinite"
  by (metis (no_types, hide_lams) HFinite_HInfinite_iff HFinite_add HFinite_minus_iff add.commute add_minus_cancel)

lemma HInfinite_ge_HInfinite: "x \ HInfinite \ x \ y \ 0 \ x \ y \ HInfinite"
  for x y :: hypreal
  by (auto intro: HFinite_bounded simp add: HInfinite_HFinite_iff)

lemma Infinitesimal_inverse_HInfinite: "x \ Infinitesimal \ x \ 0 \ inverse x \ HInfinite"
  for x :: "'a::real_normed_div_algebra star"
  by (metis Infinitesimal_HFinite_mult not_HFinite_HInfinite one_not_Infinitesimal right_inverse)

lemma HInfinite_HFinite_not_Infinitesimal_mult:
  "x \ HInfinite \ y \ HFinite - Infinitesimal \ x * y \ HInfinite"
  for x y :: "'a::real_normed_div_algebra star"
  by (metis (no_types, hide_lams) HFinite_HInfinite_iff HFinite_Infinitesimal_not_zero HFinite_inverse2 HFinite_mult mult.assoc mult.right_neutral right_inverse)

lemma HInfinite_HFinite_not_Infinitesimal_mult2:
  "x \ HInfinite \ y \ HFinite - Infinitesimal \ y * x \ HInfinite"
  for x y :: "'a::real_normed_div_algebra star"
  by (metis Diff_iff HInfinite_HFinite_iff HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 divide_inverse mult_zero_right nonzero_eq_divide_eq)

lemma HInfinite_gt_SReal: "x \ HInfinite \ 0 < x \ y \ \ \ y < x"
  for x y :: hypreal
  by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le)

lemma HInfinite_gt_zero_gt_one: "x \ HInfinite \ 0 < x \ 1 < x"
  for x :: hypreal
  by (auto intro: HInfinite_gt_SReal)

lemma not_HInfinite_one [simp]: "1 \ HInfinite"
  by (simp add: HInfinite_HFinite_iff)

lemma approx_hrabs_disj: "\x\ \ x \ \x\ \ -x"
  for x :: hypreal
  by (simp add: abs_if)

subsection \<open>Theorems about Monads\<close>

lemma monad_hrabs_Un_subset: "monad \x\ \ monad x \ monad (- x)"
  for x :: hypreal
  by (simp add: abs_if)

lemma Infinitesimal_monad_eq: "e \ 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 \ monad x \ - u \ monad (- x)"
  by (simp add: monad_def)

lemma Infinitesimal_monad_zero_iff: "x \ Infinitesimal \ x \ monad 0"
  by (auto intro: approx_sym simp add: monad_def mem_infmal_iff)

lemma monad_zero_minus_iff: "x \ monad 0 \ - x \ monad 0"
  by (simp add: Infinitesimal_monad_zero_iff [symmetric])

lemma monad_zero_hrabs_iff: "x \ monad 0 \ \x\ \ monad 0"
  for x :: hypreal
  using Infinitesimal_monad_zero_iff by blast

lemma mem_monad_self [simp]: "x \ monad x"
  by (simp add: monad_def)

subsection \<open>Proof that \<^term>\<open>x \<approx> y\<close> implies \<^term>\<open>\<bar>x\<bar> \<approx> \<bar>y\<bar>\<close>\<close>

lemma approx_subset_monad: "x \ y \ {x, y} \ monad x"
  by (simp (no_asm)) (simp add: approx_monad_iff)

lemma approx_subset_monad2: "x \ y \ {x, y} \ monad y"
  using approx_subset_monad approx_sym by auto

lemma mem_monad_approx: "u \ monad x \ x \ u"
  by (simp add: monad_def)

lemma approx_mem_monad: "x \ u \ u \ monad x"
  by (simp add: monad_def)

lemma approx_mem_monad2: "x \ u \ x \ monad u"
  using approx_mem_monad approx_sym by blast

lemma approx_mem_monad_zero: "x \ y \ x \ monad 0 \ y \ monad 0"
  using approx_trans monad_def by blast

lemma Infinitesimal_approx_hrabs: "x \ y \ x \ Infinitesimal \ \x\ \ \y\"
  for x y :: hypreal
  using approx_hnorm by fastforce

lemma less_Infinitesimal_less: "0 < x \ x \ Infinitesimal \ e \ Infinitesimal \ e < x"
  for x :: hypreal
  using Infinitesimal_interval less_linear by blast

lemma Ball_mem_monad_gt_zero: "0 < x \ x \ Infinitesimal \ u \ monad x \ 0 < u"
  for u x :: hypreal
  by (metis bex_Infinitesimal_iff2 less_Infinitesimal_less less_add_same_cancel2 mem_monad_approx)

lemma Ball_mem_monad_less_zero: "x < 0 \ x \ Infinitesimal \ u \ monad x \ u < 0"
  for u x :: hypreal
  by (metis Ball_mem_monad_gt_zero approx_monad_iff less_asym linorder_neqE_linordered_idom mem_infmal_iff mem_monad_approx mem_monad_self)

lemma lemma_approx_gt_zero: "0 < x \ x \ Infinitesimal \ x \ y \ 0 < y"
  for x y :: hypreal
  by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad)

lemma lemma_approx_less_zero: "x < 0 \ x \ Infinitesimal \ x \ y \ y < 0"
  for x y :: hypreal
  by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)

lemma approx_hrabs: "x \ y \ \x\ \ \y\"
  for x y :: hypreal
  by (drule approx_hnorm) simp

lemma approx_hrabs_zero_cancel: "\x\ \ 0 \ x \ 0"
  for x :: hypreal
  using mem_infmal_iff by blast

lemma approx_hrabs_add_Infinitesimal: "e \ Infinitesimal \ \x\ \ \x + e\"
  for e x :: hypreal
  by (fast intro: approx_hrabs Infinitesimal_add_approx_self)

lemma approx_hrabs_add_minus_Infinitesimal: "e \ Infinitesimal ==> \x\ \ \x + -e\"
  for e x :: hypreal
  by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)

lemma hrabs_add_Infinitesimal_cancel:
  "e \ Infinitesimal \ e' \ Infinitesimal \ \x + e\ = \y + e'\ \ \x\ \ \y\"
  for e e' x y :: hypreal
  by (metis approx_hrabs_add_Infinitesimal approx_trans2)

lemma hrabs_add_minus_Infinitesimal_cancel:
  "e \ Infinitesimal \ e' \ Infinitesimal \ \x + -e\ = \y + -e'\ \ \x\ \ \y\"
  for e e' x y :: hypreal
  by (meson Infinitesimal_minus_iff hrabs_add_Infinitesimal_cancel)

subsection \<open>More \<^term>\<open>HFinite\<close> and \<^term>\<open>Infinitesimal\<close> Theorems\<close>

text \<open>
  Interesting slightly counterintuitive theorem: necessary
  for proving that an open interval is an NS open set.
\<close>
lemma Infinitesimal_add_hypreal_of_real_less:
  assumes "x < y" and u: "u \ Infinitesimal"
  shows "hypreal_of_real x + u < hypreal_of_real y"
proof -
  have "\u\ < hypreal_of_real y - hypreal_of_real x"
    using InfinitesimalD \<open>x < y\<close> u by fastforce
  then show ?thesis
    by (simp add: abs_less_iff)
qed

lemma Infinitesimal_add_hrabs_hypreal_of_real_less:
  "x \ Infinitesimal \ \hypreal_of_real r\ < hypreal_of_real y \
    \<bar>hypreal_of_real r + x\<bar> < hypreal_of_real y"
  by (metis Infinitesimal_add_hypreal_of_real_less approx_hrabs_add_Infinitesimal approx_sym bex_Infinitesimal_iff2 star_of_abs star_of_less)

lemma Infinitesimal_add_hrabs_hypreal_of_real_less2:
  "x \ Infinitesimal \ \hypreal_of_real r\ < hypreal_of_real y \
    \<bar>x + hypreal_of_real r\<bar> < hypreal_of_real y"
  using Infinitesimal_add_hrabs_hypreal_of_real_less by fastforce

lemma hypreal_of_real_le_add_Infininitesimal_cancel:
  assumes le: "hypreal_of_real x + u \ hypreal_of_real y + v"
      and u: "u \ Infinitesimal" and v: "v \ Infinitesimal"
  shows "hypreal_of_real x \ hypreal_of_real y"
proof (rule ccontr)
  assume "\ hypreal_of_real x \ hypreal_of_real y"
  then have "hypreal_of_real y + (v - u) < hypreal_of_real x"
    by (simp add: Infinitesimal_add_hypreal_of_real_less Infinitesimal_diff u v)
  then show False
    by (simp add: add_diff_eq add_le_imp_le_diff le leD)
qed

lemma hypreal_of_real_le_add_Infininitesimal_cancel2:
  "u \ Infinitesimal \ v \ Infinitesimal \
    hypreal_of_real x + u \<le> hypreal_of_real y + v \<Longrightarrow> x \<le> y"
  by (blast intro: star_of_le [THEN iffD1] intro!: hypreal_of_real_le_add_Infininitesimal_cancel)

lemma hypreal_of_real_less_Infinitesimal_le_zero:
  "hypreal_of_real x < e \ e \ Infinitesimal \ hypreal_of_real x \ 0"
  by (metis Infinitesimal_interval eq_iff le_less_linear star_of_Infinitesimal_iff_0 star_of_eq_0)

lemma Infinitesimal_add_not_zero: "h \ Infinitesimal \ x \ 0 \ star_of x + h \ 0"
  by (metis Infinitesimal_add_approx_self star_of_approx_zero_iff)

lemma monad_hrabs_less: "y \ monad x \ 0 < hypreal_of_real e \ \y - x\ < hypreal_of_real e"
  by (simp add: Infinitesimal_approx_minus approx_sym less_Infinitesimal_less mem_monad_approx)

lemma mem_monad_SReal_HFinite: "x \ monad (hypreal_of_real a) \ x \ HFinite"
  using HFinite_star_of approx_HFinite mem_monad_approx by blast

subsection \<open>Theorems about Standard Part\<close>

lemma st_approx_self: "x \ HFinite \ st x \ x"
  by (metis (no_types, lifting) approx_refl approx_trans3 someI_ex st_def st_part_Ex st_part_Ex1)

lemma st_SReal: "x \ HFinite \ st x \ \"
  by (metis (mono_tags, lifting) approx_sym someI_ex st_def st_part_Ex)

lemma st_HFinite: "x \ HFinite \ st x \ HFinite"
  by (erule st_SReal [THEN SReal_subset_HFinite [THEN subsetD]])

lemma st_unique: "r \ \ \ r \ x \ st x = r"
  by (meson SReal_subset_HFinite approx_HFinite approx_unique_real st_SReal st_approx_self subsetD)

lemma st_SReal_eq: "x \ \ \ st x = x"
  by (metis approx_refl st_unique)

lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x"
  by (rule SReal_hypreal_of_real [THEN st_SReal_eq])

lemma st_eq_approx: "x \ HFinite \ y \ HFinite \ st x = st y \ x \ y"
  by (auto dest!: st_approx_self elim!: approx_trans3)

lemma approx_st_eq:
  assumes x: "x \ HFinite" and y: "y \ HFinite" and xy: "x \ y"
  shows "st x = st y"
proof -
  have "st x \ x" "st y \ y" "st x \ \" "st y \ \"
    by (simp_all add: st_approx_self st_SReal x y)
  with xy show ?thesis
    by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1])
qed

lemma st_eq_approx_iff: "x \ HFinite \ y \ HFinite \ x \ y \ st x = st y"
  by (blast intro: approx_st_eq st_eq_approx)

lemma st_Infinitesimal_add_SReal: "x \ \ \ e \ Infinitesimal \ st (x + e) = x"
  by (simp add: Infinitesimal_add_approx_self st_unique)

lemma st_Infinitesimal_add_SReal2: "x \ \ \ e \ Infinitesimal \ st (e + x) = x"
  by (metis add.commute st_Infinitesimal_add_SReal)

lemma HFinite_st_Infinitesimal_add: "x \ HFinite \ \e \ Infinitesimal. x = st(x) + e"
  by (blast dest!: st_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])

lemma st_add: "x \ HFinite \ y \ HFinite \ st (x + y) = st x + st y"
  by (simp add: st_unique st_SReal st_approx_self approx_add)

lemma st_numeral [simp]: "st (numeral w) = numeral w"
  by (rule Reals_numeral [THEN st_SReal_eq])

lemma st_neg_numeral [simp]: "st (- numeral w) = - numeral w"
  using st_unique by auto

lemma st_0 [simp]: "st 0 = 0"
  by (simp add: st_SReal_eq)

lemma st_1 [simp]: "st 1 = 1"
  by (simp add: st_SReal_eq)

lemma st_neg_1 [simp]: "st (- 1) = - 1"
  by (simp add: st_SReal_eq)

lemma st_minus: "x \ HFinite \ st (- x) = - st x"
  by (simp add: st_unique st_SReal st_approx_self approx_minus)

lemma st_diff: "\x \ HFinite; y \ HFinite\ \ st (x - y) = st x - st y"
  by (simp add: st_unique st_SReal st_approx_self approx_diff)

lemma st_mult: "\x \ HFinite; y \ HFinite\ \ st (x * y) = st x * st y"
  by (simp add: st_unique st_SReal st_approx_self approx_mult_HFinite)

lemma st_Infinitesimal: "x \ Infinitesimal \ st x = 0"
  by (simp add: st_unique mem_infmal_iff)

lemma st_not_Infinitesimal: "st(x) \ 0 \ x \ Infinitesimal"
by (fast intro: st_Infinitesimal)

lemma st_inverse: "x \ HFinite \ st x \ 0 \ st (inverse x) = inverse (st x)"
  by (simp add: approx_inverse st_SReal st_approx_self st_not_Infinitesimal st_unique)

lemma st_divide [simp]: "x \ HFinite \ y \ HFinite \ st y \ 0 \ st (x / y) = st x / st y"
  by (simp add: divide_inverse st_mult st_not_Infinitesimal HFinite_inverse st_inverse)

lemma st_idempotent [simp]: "x \ HFinite \ st (st x) = st x"
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.63 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.