1 (* Title: HOL/NSA/NSA.thy |
1 (* Title: HOL/NSA/NSA.thy |
2 Author: Jacques D. Fleuriot, University of Cambridge |
2 Author: Jacques D. Fleuriot, University of Cambridge |
3 Author: Lawrence C Paulson, University of Cambridge |
3 Author: Lawrence C Paulson, University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} |
6 section\<open>Infinite Numbers, Infinitesimals, Infinitely Close Relation\<close> |
7 |
7 |
8 theory NSA |
8 theory NSA |
9 imports HyperDef "~~/src/HOL/Library/Lub_Glb" |
9 imports HyperDef "~~/src/HOL/Library/Lub_Glb" |
10 begin |
10 begin |
11 |
11 |
25 HInfinite :: "('a::real_normed_vector) star set" where |
25 HInfinite :: "('a::real_normed_vector) star set" where |
26 "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}" |
26 "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}" |
27 |
27 |
28 definition |
28 definition |
29 approx :: "['a::real_normed_vector star, 'a star] => bool" (infixl "@=" 50) where |
29 approx :: "['a::real_normed_vector star, 'a star] => bool" (infixl "@=" 50) where |
30 --{*the `infinitely close' relation*} |
30 \<comment>\<open>the `infinitely close' relation\<close> |
31 "(x @= y) = ((x - y) \<in> Infinitesimal)" |
31 "(x @= y) = ((x - y) \<in> Infinitesimal)" |
32 |
32 |
33 definition |
33 definition |
34 st :: "hypreal => hypreal" where |
34 st :: "hypreal => hypreal" where |
35 --{*the standard part of a hyperreal*} |
35 \<comment>\<open>the standard part of a hyperreal\<close> |
36 "st = (%x. @r. x \<in> HFinite & r \<in> \<real> & r @= x)" |
36 "st = (%x. @r. x \<in> HFinite & r \<in> \<real> & r @= x)" |
37 |
37 |
38 definition |
38 definition |
39 monad :: "'a::real_normed_vector star => 'a star set" where |
39 monad :: "'a::real_normed_vector star => 'a star set" where |
40 "monad x = {y. x @= y}" |
40 "monad x = {y. x @= y}" |
47 approx (infixl "\<approx>" 50) |
47 approx (infixl "\<approx>" 50) |
48 |
48 |
49 lemma SReal_def: "\<real> == {x. \<exists>r. x = hypreal_of_real r}" |
49 lemma SReal_def: "\<real> == {x. \<exists>r. x = hypreal_of_real r}" |
50 by (simp add: Reals_def image_def) |
50 by (simp add: Reals_def image_def) |
51 |
51 |
52 subsection {* Nonstandard Extension of the Norm Function *} |
52 subsection \<open>Nonstandard Extension of the Norm Function\<close> |
53 |
53 |
54 definition |
54 definition |
55 scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where |
55 scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where |
56 [transfer_unfold]: "scaleHR = starfun2 scaleR" |
56 [transfer_unfold]: "scaleHR = starfun2 scaleR" |
57 |
57 |
169 "\<lbrakk>\<bar>x\<bar> < r; hnorm y < s\<rbrakk> \<Longrightarrow> hnorm (scaleHR x y) < r * s" |
169 "\<lbrakk>\<bar>x\<bar> < r; hnorm y < s\<rbrakk> \<Longrightarrow> hnorm (scaleHR x y) < r * s" |
170 apply (simp only: hnorm_scaleHR) |
170 apply (simp only: hnorm_scaleHR) |
171 apply (simp add: mult_strict_mono') |
171 apply (simp add: mult_strict_mono') |
172 done |
172 done |
173 |
173 |
174 subsection{*Closure Laws for the Standard Reals*} |
174 subsection\<open>Closure Laws for the Standard Reals\<close> |
175 |
175 |
176 lemma Reals_minus_iff [simp]: "(-x \<in> \<real>) = (x \<in> \<real>)" |
176 lemma Reals_minus_iff [simp]: "(-x \<in> \<real>) = (x \<in> \<real>)" |
177 apply auto |
177 apply auto |
178 apply (drule Reals_minus, auto) |
178 apply (drule Reals_minus, auto) |
179 done |
179 done |
188 by (simp add: Reals_eq_Standard) |
188 by (simp add: Reals_eq_Standard) |
189 |
189 |
190 lemma SReal_divide_numeral: "r \<in> \<real> ==> r/(numeral w::hypreal) \<in> \<real>" |
190 lemma SReal_divide_numeral: "r \<in> \<real> ==> r/(numeral w::hypreal) \<in> \<real>" |
191 by simp |
191 by simp |
192 |
192 |
193 text{*epsilon is not in Reals because it is an infinitesimal*} |
193 text\<open>epsilon is not in Reals because it is an infinitesimal\<close> |
194 lemma SReal_epsilon_not_mem: "epsilon \<notin> \<real>" |
194 lemma SReal_epsilon_not_mem: "epsilon \<notin> \<real>" |
195 apply (simp add: SReal_def) |
195 apply (simp add: SReal_def) |
196 apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym]) |
196 apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym]) |
197 done |
197 done |
198 |
198 |
223 "[| (x::hypreal) \<in> \<real>; y \<in> \<real>; x<y |] ==> \<exists>r \<in> Reals. x<r & r<y" |
223 "[| (x::hypreal) \<in> \<real>; y \<in> \<real>; x<y |] ==> \<exists>r \<in> Reals. x<r & r<y" |
224 apply (auto simp add: SReal_def) |
224 apply (auto simp add: SReal_def) |
225 apply (drule dense, auto) |
225 apply (drule dense, auto) |
226 done |
226 done |
227 |
227 |
228 text{*Completeness of Reals, but both lemmas are unused.*} |
228 text\<open>Completeness of Reals, but both lemmas are unused.\<close> |
229 |
229 |
230 lemma SReal_sup_lemma: |
230 lemma SReal_sup_lemma: |
231 "P \<subseteq> \<real> ==> ((\<exists>x \<in> P. y < x) = |
231 "P \<subseteq> \<real> ==> ((\<exists>x \<in> P. y < x) = |
232 (\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))" |
232 (\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))" |
233 by (blast dest!: SReal_iff [THEN iffD1]) |
233 by (blast dest!: SReal_iff [THEN iffD1]) |
242 apply (drule SReal_iff [THEN iffD1]) |
242 apply (drule SReal_iff [THEN iffD1]) |
243 apply (auto, rule_tac x = ya in exI, auto) |
243 apply (auto, rule_tac x = ya in exI, auto) |
244 done |
244 done |
245 |
245 |
246 |
246 |
247 subsection{* Set of Finite Elements is a Subring of the Extended Reals*} |
247 subsection\<open>Set of Finite Elements is a Subring of the Extended Reals\<close> |
248 |
248 |
249 lemma HFinite_add: "[|x \<in> HFinite; y \<in> HFinite|] ==> (x+y) \<in> HFinite" |
249 lemma HFinite_add: "[|x \<in> HFinite; y \<in> HFinite|] ==> (x+y) \<in> HFinite" |
250 apply (simp add: HFinite_def) |
250 apply (simp add: HFinite_def) |
251 apply (blast intro!: Reals_add hnorm_add_less) |
251 apply (blast intro!: Reals_add hnorm_add_less) |
252 done |
252 done |
313 apply (auto simp add: linorder_not_le) |
313 apply (auto simp add: linorder_not_le) |
314 apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def) |
314 apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def) |
315 done |
315 done |
316 |
316 |
317 |
317 |
318 subsection{* Set of Infinitesimals is a Subring of the Hyperreals*} |
318 subsection\<open>Set of Infinitesimals is a Subring of the Hyperreals\<close> |
319 |
319 |
320 lemma InfinitesimalI: |
320 lemma InfinitesimalI: |
321 "(\<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm x < r) \<Longrightarrow> x \<in> Infinitesimal" |
321 "(\<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm x < r) \<Longrightarrow> x \<in> Infinitesimal" |
322 by (simp add: Infinitesimal_def) |
322 by (simp add: Infinitesimal_def) |
323 |
323 |
607 fixes x :: "'a::real_normed_algebra star" |
607 fixes x :: "'a::real_normed_algebra star" |
608 shows "x \<in> Infinitesimal ==> star_of r * x \<in> Infinitesimal" |
608 shows "x \<in> Infinitesimal ==> star_of r * x \<in> Infinitesimal" |
609 by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2]) |
609 by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2]) |
610 |
610 |
611 |
611 |
612 subsection{*The Infinitely Close Relation*} |
612 subsection\<open>The Infinitely Close Relation\<close> |
613 |
613 |
614 lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)" |
614 lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)" |
615 by (simp add: Infinitesimal_def approx_def) |
615 by (simp add: Infinitesimal_def approx_def) |
616 |
616 |
617 lemma approx_minus_iff: " (x @= y) = (x - y @= 0)" |
617 lemma approx_minus_iff: " (x @= y) = (x - y @= 0)" |
649 |
649 |
650 (*reorientation simplification procedure: reorients (polymorphic) |
650 (*reorientation simplification procedure: reorients (polymorphic) |
651 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) |
651 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) |
652 simproc_setup approx_reorient_simproc |
652 simproc_setup approx_reorient_simproc |
653 ("0 @= x" | "1 @= y" | "numeral w @= z" | "- 1 @= y" | "- numeral w @= r") = |
653 ("0 @= x" | "1 @= y" | "numeral w @= z" | "- 1 @= y" | "- numeral w @= r") = |
654 {* |
654 \<open> |
655 let val rule = @{thm approx_reorient} RS eq_reflection |
655 let val rule = @{thm approx_reorient} RS eq_reflection |
656 fun proc phi ss ct = |
656 fun proc phi ss ct = |
657 case Thm.term_of ct of |
657 case Thm.term_of ct of |
658 _ $ t $ u => if can HOLogic.dest_number u then NONE |
658 _ $ t $ u => if can HOLogic.dest_number u then NONE |
659 else if can HOLogic.dest_number t then SOME rule else NONE |
659 else if can HOLogic.dest_number t then SOME rule else NONE |
660 | _ => NONE |
660 | _ => NONE |
661 in proc end |
661 in proc end |
662 *} |
662 \<close> |
663 |
663 |
664 lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)" |
664 lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)" |
665 by (simp add: approx_minus_iff [symmetric] mem_infmal_iff) |
665 by (simp add: approx_minus_iff [symmetric] mem_infmal_iff) |
666 |
666 |
667 lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))" |
667 lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))" |
899 thus "hnorm x - hnorm y \<in> Infinitesimal" |
899 thus "hnorm x - hnorm y \<in> Infinitesimal" |
900 by (simp only: Infinitesimal_hrabs_iff) |
900 by (simp only: Infinitesimal_hrabs_iff) |
901 qed |
901 qed |
902 |
902 |
903 |
903 |
904 subsection{* Zero is the Only Infinitesimal that is also a Real*} |
904 subsection\<open>Zero is the Only Infinitesimal that is also a Real\<close> |
905 |
905 |
906 lemma Infinitesimal_less_SReal: |
906 lemma Infinitesimal_less_SReal: |
907 "[| (x::hypreal) \<in> \<real>; y \<in> Infinitesimal; 0 < x |] ==> y < x" |
907 "[| (x::hypreal) \<in> \<real>; y \<in> Infinitesimal; 0 < x |] ==> y < x" |
908 apply (simp add: Infinitesimal_def) |
908 apply (simp add: Infinitesimal_def) |
909 apply (rule abs_ge_self [THEN order_le_less_trans], auto) |
909 apply (rule abs_ge_self [THEN order_le_less_trans], auto) |
1002 (*------------------------------------------------------------------ |
1002 (*------------------------------------------------------------------ |
1003 Standard Part Theorem: Every finite x: R* is infinitely |
1003 Standard Part Theorem: Every finite x: R* is infinitely |
1004 close to a unique real number (i.e a member of Reals) |
1004 close to a unique real number (i.e a member of Reals) |
1005 ------------------------------------------------------------------*) |
1005 ------------------------------------------------------------------*) |
1006 |
1006 |
1007 subsection{* Uniqueness: Two Infinitely Close Reals are Equal*} |
1007 subsection\<open>Uniqueness: Two Infinitely Close Reals are Equal\<close> |
1008 |
1008 |
1009 lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)" |
1009 lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)" |
1010 apply safe |
1010 apply safe |
1011 apply (simp add: approx_def) |
1011 apply (simp add: approx_def) |
1012 apply (simp only: star_of_diff [symmetric]) |
1012 apply (simp only: star_of_diff [symmetric]) |
1059 lemma approx_unique_real: |
1059 lemma approx_unique_real: |
1060 "[| (r::hypreal) \<in> \<real>; s \<in> \<real>; r @= x; s @= x|] ==> r = s" |
1060 "[| (r::hypreal) \<in> \<real>; s \<in> \<real>; r @= x; s @= x|] ==> r = s" |
1061 by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2) |
1061 by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2) |
1062 |
1062 |
1063 |
1063 |
1064 subsection{* Existence of Unique Real Infinitely Close*} |
1064 subsection\<open>Existence of Unique Real Infinitely Close\<close> |
1065 |
1065 |
1066 subsubsection{*Lifting of the Ub and Lub Properties*} |
1066 subsubsection\<open>Lifting of the Ub and Lub Properties\<close> |
1067 |
1067 |
1068 lemma hypreal_of_real_isUb_iff: |
1068 lemma hypreal_of_real_isUb_iff: |
1069 "(isUb \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)) = |
1069 "(isUb \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)) = |
1070 (isUb (UNIV :: real set) Q Y)" |
1070 (isUb (UNIV :: real set) Q Y)" |
1071 by (simp add: isUb_def setle_def) |
1071 by (simp add: isUb_def setle_def) |
1253 ==> \<forall>r \<in> Reals. 0 < r --> \<bar>x - t\<bar> < r" |
1253 ==> \<forall>r \<in> Reals. 0 < r --> \<bar>x - t\<bar> < r" |
1254 by (blast dest!: lemma_st_part_major) |
1254 by (blast dest!: lemma_st_part_major) |
1255 |
1255 |
1256 |
1256 |
1257 |
1257 |
1258 text{*Existence of real and Standard Part Theorem*} |
1258 text\<open>Existence of real and Standard Part Theorem\<close> |
1259 lemma lemma_st_part_Ex: |
1259 lemma lemma_st_part_Ex: |
1260 "(x::hypreal) \<in> HFinite |
1260 "(x::hypreal) \<in> HFinite |
1261 ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> \<bar>x - t\<bar> < r" |
1261 ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> \<bar>x - t\<bar> < r" |
1262 apply (frule lemma_st_part_lub, safe) |
1262 apply (frule lemma_st_part_lub, safe) |
1263 apply (frule isLubD1a) |
1263 apply (frule isLubD1a) |
1268 "(x::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x @= t" |
1268 "(x::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x @= t" |
1269 apply (simp add: approx_def Infinitesimal_def) |
1269 apply (simp add: approx_def Infinitesimal_def) |
1270 apply (drule lemma_st_part_Ex, auto) |
1270 apply (drule lemma_st_part_Ex, auto) |
1271 done |
1271 done |
1272 |
1272 |
1273 text{*There is a unique real infinitely close*} |
1273 text\<open>There is a unique real infinitely close\<close> |
1274 lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x @= t" |
1274 lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x @= t" |
1275 apply (drule st_part_Ex, safe) |
1275 apply (drule st_part_Ex, safe) |
1276 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) |
1276 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) |
1277 apply (auto intro!: approx_unique_real) |
1277 apply (auto intro!: approx_unique_real) |
1278 done |
1278 done |
1279 |
1279 |
1280 subsection{* Finite, Infinite and Infinitesimal*} |
1280 subsection\<open>Finite, Infinite and Infinitesimal\<close> |
1281 |
1281 |
1282 lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}" |
1282 lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}" |
1283 apply (simp add: HFinite_def HInfinite_def) |
1283 apply (simp add: HFinite_def HInfinite_def) |
1284 apply (auto dest: order_less_trans) |
1284 apply (auto dest: order_less_trans) |
1285 done |
1285 done |
1485 |
1485 |
1486 lemma approx_hrabs_disj: "\<bar>x::hypreal\<bar> @= x \<or> \<bar>x\<bar> @= -x" |
1486 lemma approx_hrabs_disj: "\<bar>x::hypreal\<bar> @= x \<or> \<bar>x\<bar> @= -x" |
1487 by (cut_tac x = x in hrabs_disj, auto) |
1487 by (cut_tac x = x in hrabs_disj, auto) |
1488 |
1488 |
1489 |
1489 |
1490 subsection{*Theorems about Monads*} |
1490 subsection\<open>Theorems about Monads\<close> |
1491 |
1491 |
1492 lemma monad_hrabs_Un_subset: "monad \<bar>x\<bar> \<le> monad(x::hypreal) Un monad(-x)" |
1492 lemma monad_hrabs_Un_subset: "monad \<bar>x\<bar> \<le> monad(x::hypreal) Un monad(-x)" |
1493 by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto) |
1493 by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto) |
1494 |
1494 |
1495 lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal ==> monad (x+e) = monad x" |
1495 lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal ==> monad (x+e) = monad x" |
1512 |
1512 |
1513 lemma mem_monad_self [simp]: "x \<in> monad x" |
1513 lemma mem_monad_self [simp]: "x \<in> monad x" |
1514 by (simp add: monad_def) |
1514 by (simp add: monad_def) |
1515 |
1515 |
1516 |
1516 |
1517 subsection{*Proof that @{term "x @= y"} implies @{term"\<bar>x\<bar> @= \<bar>y\<bar>"}*} |
1517 subsection\<open>Proof that @{term "x @= y"} implies @{term"\<bar>x\<bar> @= \<bar>y\<bar>"}\<close> |
1518 |
1518 |
1519 lemma approx_subset_monad: "x @= y ==> {x,y} \<le> monad x" |
1519 lemma approx_subset_monad: "x @= y ==> {x,y} \<le> monad x" |
1520 apply (simp (no_asm)) |
1520 apply (simp (no_asm)) |
1521 apply (simp add: approx_monad_iff) |
1521 apply (simp add: approx_monad_iff) |
1522 done |
1522 done |
1607 apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal) |
1607 apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal) |
1608 apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal) |
1608 apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal) |
1609 apply (auto intro: approx_trans2) |
1609 apply (auto intro: approx_trans2) |
1610 done |
1610 done |
1611 |
1611 |
1612 subsection {* More @{term HFinite} and @{term Infinitesimal} Theorems *} |
1612 subsection \<open>More @{term HFinite} and @{term Infinitesimal} Theorems\<close> |
1613 |
1613 |
1614 (* interesting slightly counterintuitive theorem: necessary |
1614 (* interesting slightly counterintuitive theorem: necessary |
1615 for proving that an open interval is an NS open set |
1615 for proving that an open interval is an NS open set |
1616 *) |
1616 *) |
1617 lemma Infinitesimal_add_hypreal_of_real_less: |
1617 lemma Infinitesimal_add_hypreal_of_real_less: |
1751 apply (safe dest!: Infinitesimal_subset_HFinite [THEN subsetD]) |
1751 apply (safe dest!: Infinitesimal_subset_HFinite [THEN subsetD]) |
1752 apply (erule SReal_hypreal_of_real [THEN SReal_subset_HFinite [THEN subsetD], THEN HFinite_add]) |
1752 apply (erule SReal_hypreal_of_real [THEN SReal_subset_HFinite [THEN subsetD], THEN HFinite_add]) |
1753 done |
1753 done |
1754 |
1754 |
1755 |
1755 |
1756 subsection{* Theorems about Standard Part*} |
1756 subsection\<open>Theorems about Standard Part\<close> |
1757 |
1757 |
1758 lemma st_approx_self: "x \<in> HFinite ==> st x @= x" |
1758 lemma st_approx_self: "x \<in> HFinite ==> st x @= x" |
1759 apply (simp add: st_def) |
1759 apply (simp add: st_def) |
1760 apply (frule st_part_Ex, safe) |
1760 apply (frule st_part_Ex, safe) |
1761 apply (rule someI2) |
1761 apply (rule someI2) |
1907 apply (auto dest!: st_zero_ge [OF order_less_imp_le]) |
1907 apply (auto dest!: st_zero_ge [OF order_less_imp_le]) |
1908 done |
1908 done |
1909 |
1909 |
1910 |
1910 |
1911 |
1911 |
1912 subsection {* Alternative Definitions using Free Ultrafilter *} |
1912 subsection \<open>Alternative Definitions using Free Ultrafilter\<close> |
1913 |
1913 |
1914 subsubsection {* @{term HFinite} *} |
1914 subsubsection \<open>@{term HFinite}\<close> |
1915 |
1915 |
1916 lemma HFinite_FreeUltrafilterNat: |
1916 lemma HFinite_FreeUltrafilterNat: |
1917 "star_n X \<in> HFinite |
1917 "star_n X \<in> HFinite |
1918 ==> \<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat" |
1918 ==> \<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat" |
1919 apply (auto simp add: HFinite_def SReal_def) |
1919 apply (auto simp add: HFinite_def SReal_def) |
1934 |
1934 |
1935 lemma HFinite_FreeUltrafilterNat_iff: |
1935 lemma HFinite_FreeUltrafilterNat_iff: |
1936 "(star_n X \<in> HFinite) = (\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat)" |
1936 "(star_n X \<in> HFinite) = (\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat)" |
1937 by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite) |
1937 by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite) |
1938 |
1938 |
1939 subsubsection {* @{term HInfinite} *} |
1939 subsubsection \<open>@{term HInfinite}\<close> |
1940 |
1940 |
1941 lemma lemma_Compl_eq: "- {n. u < norm (f n)} = {n. norm (f n) \<le> u}" |
1941 lemma lemma_Compl_eq: "- {n. u < norm (f n)} = {n. norm (f n) \<le> u}" |
1942 by auto |
1942 by auto |
1943 |
1943 |
1944 lemma lemma_Compl_eq2: "- {n. norm (f n) < u} = {n. u \<le> norm (f n)}" |
1944 lemma lemma_Compl_eq2: "- {n. norm (f n) < u} = {n. u \<le> norm (f n)}" |
1994 |
1994 |
1995 lemma HInfinite_FreeUltrafilterNat_iff: |
1995 lemma HInfinite_FreeUltrafilterNat_iff: |
1996 "(star_n X \<in> HInfinite) = (\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat)" |
1996 "(star_n X \<in> HInfinite) = (\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat)" |
1997 by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite) |
1997 by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite) |
1998 |
1998 |
1999 subsubsection {* @{term Infinitesimal} *} |
1999 subsubsection \<open>@{term Infinitesimal}\<close> |
2000 |
2000 |
2001 lemma ball_SReal_eq: "(\<forall>x::hypreal \<in> Reals. P x) = (\<forall>x::real. P (star_of x))" |
2001 lemma ball_SReal_eq: "(\<forall>x::hypreal \<in> Reals. P x) = (\<forall>x::real. P (star_of x))" |
2002 by (unfold SReal_def, auto) |
2002 by (unfold SReal_def, auto) |
2003 |
2003 |
2004 lemma Infinitesimal_FreeUltrafilterNat: |
2004 lemma Infinitesimal_FreeUltrafilterNat: |
2048 apply (simp add: Infinitesimal_def) |
2048 apply (simp add: Infinitesimal_def) |
2049 apply (auto simp add: lemma_Infinitesimal2) |
2049 apply (auto simp add: lemma_Infinitesimal2) |
2050 done |
2050 done |
2051 |
2051 |
2052 |
2052 |
2053 subsection{*Proof that @{term omega} is an infinite number*} |
2053 subsection\<open>Proof that @{term omega} is an infinite number\<close> |
2054 |
2054 |
2055 text{*It will follow that epsilon is an infinitesimal number.*} |
2055 text\<open>It will follow that epsilon is an infinitesimal number.\<close> |
2056 |
2056 |
2057 lemma Suc_Un_eq: "{n. n < Suc m} = {n. n < m} Un {n. n = m}" |
2057 lemma Suc_Un_eq: "{n. n < Suc m} = {n. n < m} Un {n. n = m}" |
2058 by (auto simp add: less_Suc_eq) |
2058 by (auto simp add: less_Suc_eq) |
2059 |
2059 |
2060 (*------------------------------------------- |
2060 (*------------------------------------------- |
2098 --------------------------------------------------------------*) |
2098 --------------------------------------------------------------*) |
2099 |
2099 |
2100 lemma Compl_real_le_eq: "- {n::nat. real n \<le> u} = {n. u < real n}" |
2100 lemma Compl_real_le_eq: "- {n::nat. real n \<le> u} = {n. u < real n}" |
2101 by (auto dest!: order_le_less_trans simp add: linorder_not_le) |
2101 by (auto dest!: order_le_less_trans simp add: linorder_not_le) |
2102 |
2102 |
2103 text{*@{term omega} is a member of @{term HInfinite}*} |
2103 text\<open>@{term omega} is a member of @{term HInfinite}\<close> |
2104 |
2104 |
2105 theorem HInfinite_omega [simp]: "omega \<in> HInfinite" |
2105 theorem HInfinite_omega [simp]: "omega \<in> HInfinite" |
2106 apply (simp add: omega_def) |
2106 apply (simp add: omega_def) |
2107 apply (rule FreeUltrafilterNat_HInfinite) |
2107 apply (rule FreeUltrafilterNat_HInfinite) |
2108 apply clarify |
2108 apply clarify |
2174 lemma FreeUltrafilterNat_inverse_real_of_posnat: |
2174 lemma FreeUltrafilterNat_inverse_real_of_posnat: |
2175 "0 < u ==> eventually (\<lambda>n. inverse(real(Suc n)) < u) FreeUltrafilterNat" |
2175 "0 < u ==> eventually (\<lambda>n. inverse(real(Suc n)) < u) FreeUltrafilterNat" |
2176 by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat) |
2176 by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat) |
2177 (simp add: FreeUltrafilterNat.eventually_not_iff not_le[symmetric]) |
2177 (simp add: FreeUltrafilterNat.eventually_not_iff not_le[symmetric]) |
2178 |
2178 |
2179 text{* Example of an hypersequence (i.e. an extended standard sequence) |
2179 text\<open>Example of an hypersequence (i.e. an extended standard sequence) |
2180 whose term with an hypernatural suffix is an infinitesimal i.e. |
2180 whose term with an hypernatural suffix is an infinitesimal i.e. |
2181 the whn'nth term of the hypersequence is a member of Infinitesimal*} |
2181 the whn'nth term of the hypersequence is a member of Infinitesimal\<close> |
2182 |
2182 |
2183 lemma SEQ_Infinitesimal: |
2183 lemma SEQ_Infinitesimal: |
2184 "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal" |
2184 "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal" |
2185 by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff |
2185 by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff |
2186 FreeUltrafilterNat_inverse_real_of_posnat del: of_nat_Suc) |
2186 FreeUltrafilterNat_inverse_real_of_posnat del: of_nat_Suc) |
2187 |
2187 |
2188 text{* Example where we get a hyperreal from a real sequence |
2188 text\<open>Example where we get a hyperreal from a real sequence |
2189 for which a particular property holds. The theorem is |
2189 for which a particular property holds. The theorem is |
2190 used in proofs about equivalence of nonstandard and |
2190 used in proofs about equivalence of nonstandard and |
2191 standard neighbourhoods. Also used for equivalence of |
2191 standard neighbourhoods. Also used for equivalence of |
2192 nonstandard ans standard definitions of pointwise |
2192 nonstandard ans standard definitions of pointwise |
2193 limit.*} |
2193 limit.\<close> |
2194 |
2194 |
2195 (*----------------------------------------------------- |
2195 (*----------------------------------------------------- |
2196 |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal |
2196 |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal |
2197 -----------------------------------------------------*) |
2197 -----------------------------------------------------*) |
2198 lemma real_seq_to_hypreal_Infinitesimal: |
2198 lemma real_seq_to_hypreal_Infinitesimal: |