|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
cooper_tac.ML
Sprache: 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.25 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
