944 using t by (rule_tac x = "-t" in exI) (auto simp add: abs_less_iff) |
936 using t by (rule_tac x = "-t" in exI) (auto simp add: abs_less_iff) |
945 ultimately show ?thesis |
937 ultimately show ?thesis |
946 using SReal_complete by fastforce |
938 using SReal_complete by fastforce |
947 qed |
939 qed |
948 |
940 |
949 lemma lemma_st_part_le1: |
|
950 "x \<in> HFinite \<Longrightarrow> isLub \<real> {s. s \<in> \<real> \<and> s < x} t \<Longrightarrow> r \<in> \<real> \<Longrightarrow> 0 < r \<Longrightarrow> x \<le> t + r" |
|
951 for x r t :: hypreal |
|
952 by (metis (no_types, lifting) Reals_add add.commute isLubD1a isLubD2 less_add_same_cancel2 mem_Collect_eq not_le) |
|
953 |
|
954 lemma hypreal_setle_less_trans: "S *<= x \<Longrightarrow> x < y \<Longrightarrow> S *<= y" |
941 lemma hypreal_setle_less_trans: "S *<= x \<Longrightarrow> x < y \<Longrightarrow> S *<= y" |
955 for x y :: hypreal |
942 for x y :: hypreal |
956 by (meson le_less_trans less_imp_le setle_def) |
943 by (meson le_less_trans less_imp_le setle_def) |
957 |
944 |
958 lemma hypreal_gt_isUb: "isUb R S x \<Longrightarrow> x < y \<Longrightarrow> y \<in> R \<Longrightarrow> isUb R S y" |
945 lemma hypreal_gt_isUb: "isUb R S x \<Longrightarrow> x < y \<Longrightarrow> y \<in> R \<Longrightarrow> isUb R S y" |
959 for x y :: hypreal |
946 for x y :: hypreal |
960 using hypreal_setle_less_trans isUb_def by blast |
947 using hypreal_setle_less_trans isUb_def by blast |
961 |
948 |
962 lemma lemma_st_part_gt_ub: "x \<in> HFinite \<Longrightarrow> x < y \<Longrightarrow> y \<in> \<real> \<Longrightarrow> isUb \<real> {s. s \<in> \<real> \<and> s < x} y" |
|
963 for x y :: hypreal |
|
964 by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI) |
|
965 |
|
966 lemma lemma_minus_le_zero: "t \<le> t + -r \<Longrightarrow> r \<le> 0" |
|
967 for r t :: hypreal |
|
968 by simp |
|
969 |
|
970 lemma lemma_st_part_le2: |
|
971 "x \<in> HFinite \<Longrightarrow> isLub \<real> {s. s \<in> \<real> \<and> s < x} t \<Longrightarrow> r \<in> \<real> \<Longrightarrow> 0 < r \<Longrightarrow> t + -r \<le> x" |
|
972 for x r t :: hypreal |
|
973 apply (frule isLubD1a) |
|
974 apply (rule ccontr, drule linorder_not_le [THEN iffD1]) |
|
975 apply (drule Reals_minus, drule_tac a = t in Reals_add, assumption) |
|
976 apply (drule lemma_st_part_gt_ub, assumption+) |
|
977 apply (drule isLub_le_isUb, assumption) |
|
978 apply (drule lemma_minus_le_zero) |
|
979 apply (auto dest: order_less_le_trans) |
|
980 done |
|
981 |
|
982 lemma lemma_st_part1a: |
|
983 "x \<in> HFinite \<Longrightarrow> isLub \<real> {s. s \<in> \<real> \<and> s < x} t \<Longrightarrow> r \<in> \<real> \<Longrightarrow> 0 < r \<Longrightarrow> x + -t \<le> r" |
|
984 for x r t :: hypreal |
|
985 using lemma_st_part_le1 by fastforce |
|
986 |
|
987 lemma lemma_st_part2a: |
|
988 "x \<in> HFinite \<Longrightarrow> isLub \<real> {s. s \<in> \<real> \<and> s < x} t \<Longrightarrow> r \<in> \<real> \<Longrightarrow> 0 < r \<Longrightarrow> - (x + -t) \<le> r" |
|
989 for x r t :: hypreal |
|
990 apply (subgoal_tac "(t + -r \<le> x)") |
|
991 apply simp |
|
992 apply (rule lemma_st_part_le2) |
|
993 apply auto |
|
994 done |
|
995 |
|
996 lemma lemma_SReal_ub: "x \<in> \<real> \<Longrightarrow> isUb \<real> {s. s \<in> \<real> \<and> s < x} x" |
949 lemma lemma_SReal_ub: "x \<in> \<real> \<Longrightarrow> isUb \<real> {s. s \<in> \<real> \<and> s < x} x" |
997 for x :: hypreal |
950 for x :: hypreal |
998 by (auto intro: isUbI setleI order_less_imp_le) |
951 by (auto intro: isUbI setleI order_less_imp_le) |
999 |
952 |
1000 lemma lemma_SReal_lub: "x \<in> \<real> \<Longrightarrow> isLub \<real> {s. s \<in> \<real> \<and> s < x} x" |
953 lemma lemma_SReal_lub: |
1001 for x :: hypreal |
954 fixes x :: hypreal |
1002 apply (auto intro!: isLubI2 lemma_SReal_ub setgeI) |
955 assumes "x \<in> \<real>" shows "isLub \<real> {s. s \<in> \<real> \<and> s < x} x" |
1003 apply (frule isUbD2a) |
956 proof - |
1004 apply (rule_tac x = x and y = y in linorder_cases) |
957 have "x \<le> y" if "isUb \<real> {s \<in> \<real>. s < x} y" for y |
1005 apply (auto intro!: order_less_imp_le) |
958 proof - |
1006 apply (drule SReal_dense, assumption, assumption, safe) |
959 have "y \<in> \<real>" |
1007 apply (drule_tac y = r in isUbD) |
960 using isUbD2a that by blast |
1008 apply (auto dest: order_less_le_trans) |
961 show ?thesis |
1009 done |
962 proof (cases x y rule: linorder_cases) |
1010 |
963 case greater |
1011 lemma lemma_st_part_not_eq1: |
964 then obtain r where "y < r" "r < x" |
1012 "x \<in> HFinite \<Longrightarrow> isLub \<real> {s. s \<in> \<real> \<and> s < x} t \<Longrightarrow> r \<in> \<real> \<Longrightarrow> 0 < r \<Longrightarrow> x + - t \<noteq> r" |
965 using dense by blast |
1013 for x r t :: hypreal |
966 then show ?thesis |
1014 apply auto |
967 using isUbD [OF that] apply (simp add: ) |
1015 apply (frule isLubD1a [THEN Reals_minus]) |
968 by (meson SReal_dense \<open>y \<in> \<real>\<close> assms greater not_le) |
1016 using Reals_add_cancel [of x "- t"] apply simp |
969 qed auto |
1017 apply (drule_tac x = x in lemma_SReal_lub) |
970 qed |
1018 apply (drule isLub_unique, assumption, auto) |
971 with assms show ?thesis |
1019 done |
972 by (simp add: isLubI2 isUbI setgeI setleI) |
1020 |
973 qed |
1021 lemma lemma_st_part_not_eq2: |
|
1022 "x \<in> HFinite \<Longrightarrow> isLub \<real> {s. s \<in> \<real> \<and> s < x} t \<Longrightarrow> r \<in> \<real> \<Longrightarrow> 0 < r \<Longrightarrow> - (x + -t) \<noteq> r" |
|
1023 for x r t :: hypreal |
|
1024 apply (auto) |
|
1025 apply (frule isLubD1a) |
|
1026 using Reals_add_cancel [of "- x" t] apply simp |
|
1027 apply (drule_tac x = x in lemma_SReal_lub) |
|
1028 apply (drule isLub_unique, assumption, auto) |
|
1029 done |
|
1030 |
974 |
1031 lemma lemma_st_part_major: |
975 lemma lemma_st_part_major: |
1032 "x \<in> HFinite \<Longrightarrow> isLub \<real> {s. s \<in> \<real> \<and> s < x} t \<Longrightarrow> r \<in> \<real> \<Longrightarrow> 0 < r \<Longrightarrow> \<bar>x - t\<bar> < r" |
976 fixes x r t :: hypreal |
1033 for x r t :: hypreal |
977 assumes x: "x \<in> HFinite" and r: "r \<in> \<real>" "0 < r" and t: "isLub \<real> {s. s \<in> \<real> \<and> s < x} t" |
1034 apply (frule lemma_st_part1a) |
978 shows "\<bar>x - t\<bar> < r" |
1035 apply (frule_tac [4] lemma_st_part2a, auto) |
979 proof - |
1036 apply (drule order_le_imp_less_or_eq)+ |
980 have "t \<in> \<real>" |
1037 apply auto |
981 using isLubD1a t by blast |
1038 using lemma_st_part_not_eq2 apply fastforce |
982 have lemma_st_part_gt_ub: "x < r \<Longrightarrow> r \<in> \<real> \<Longrightarrow> isUb \<real> {s. s \<in> \<real> \<and> s < x} r" |
1039 using lemma_st_part_not_eq1 apply fastforce |
983 for r :: hypreal |
1040 done |
984 by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI) |
|
985 |
|
986 have "isUb \<real> {s \<in> \<real>. s < x} t" |
|
987 by (simp add: t isLub_isUb) |
|
988 then have "\<not> r + t < x" |
|
989 by (metis (mono_tags, lifting) Reals_add \<open>t \<in> \<real>\<close> add_le_same_cancel2 isUbD leD mem_Collect_eq r) |
|
990 then have "x - t \<le> r" |
|
991 by simp |
|
992 moreover have "\<not> x < t - r" |
|
993 using lemma_st_part_gt_ub isLub_le_isUb \<open>t \<in> \<real>\<close> r t x by fastforce |
|
994 then have "- (x - t) \<le> r" |
|
995 by linarith |
|
996 moreover have False if "x - t = r \<or> - (x - t) = r" |
|
997 proof - |
|
998 have "x \<in> \<real>" |
|
999 by (metis \<open>t \<in> \<real>\<close> \<open>r \<in> \<real>\<close> that Reals_add_cancel Reals_minus_iff add_uminus_conv_diff) |
|
1000 then have "isLub \<real> {s \<in> \<real>. s < x} x" |
|
1001 by (rule lemma_SReal_lub) |
|
1002 then show False |
|
1003 using r t that x isLub_unique by force |
|
1004 qed |
|
1005 ultimately show ?thesis |
|
1006 using abs_less_iff dual_order.order_iff_strict by blast |
|
1007 qed |
1041 |
1008 |
1042 lemma lemma_st_part_major2: |
1009 lemma lemma_st_part_major2: |
1043 "x \<in> HFinite \<Longrightarrow> isLub \<real> {s. s \<in> \<real> \<and> s < x} t \<Longrightarrow> \<forall>r \<in> Reals. 0 < r \<longrightarrow> \<bar>x - t\<bar> < r" |
1010 "x \<in> HFinite \<Longrightarrow> isLub \<real> {s. s \<in> \<real> \<and> s < x} t \<Longrightarrow> \<forall>r \<in> Reals. 0 < r \<longrightarrow> \<bar>x - t\<bar> < r" |
1044 for x t :: hypreal |
1011 for x t :: hypreal |
1045 by (blast dest!: lemma_st_part_major) |
1012 by (blast dest!: lemma_st_part_major) |
1101 lemma HFinite_not_Infinitesimal_inverse: |
1068 lemma HFinite_not_Infinitesimal_inverse: |
1102 "x \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<in> HFinite - Infinitesimal" |
1069 "x \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<in> HFinite - Infinitesimal" |
1103 for x :: "'a::real_normed_div_algebra star" |
1070 for x :: "'a::real_normed_div_algebra star" |
1104 using HFinite_Infinitesimal_not_zero HFinite_inverse2 Infinitesimal_HFinite_mult2 by fastforce |
1071 using HFinite_Infinitesimal_not_zero HFinite_inverse2 Infinitesimal_HFinite_mult2 by fastforce |
1105 |
1072 |
1106 lemma approx_inverse: "x \<approx> y \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<approx> inverse y" |
1073 lemma approx_inverse: |
1107 for x y :: "'a::real_normed_div_algebra star" |
1074 fixes x y :: "'a::real_normed_div_algebra star" |
1108 apply (frule HFinite_diff_Infinitesimal_approx, assumption) |
1075 assumes "x \<approx> y" and y: "y \<in> HFinite - Infinitesimal" shows "inverse x \<approx> inverse y" |
1109 apply (frule not_Infinitesimal_not_zero2) |
1076 proof - |
1110 apply (frule_tac x = x in not_Infinitesimal_not_zero2) |
1077 have x: "x \<in> HFinite - Infinitesimal" |
1111 apply (drule HFinite_inverse2)+ |
1078 using HFinite_diff_Infinitesimal_approx assms(1) y by blast |
1112 apply (drule approx_mult2, assumption, auto) |
1079 with y HFinite_inverse2 have "inverse x \<in> HFinite" "inverse y \<in> HFinite" |
1113 apply (drule_tac c = "inverse x" in approx_mult1, assumption) |
1080 by blast+ |
1114 apply (auto intro: approx_sym simp add: mult.assoc) |
1081 then have "inverse y * x \<approx> 1" |
1115 done |
1082 by (metis Diff_iff approx_mult2 assms(1) left_inverse not_Infinitesimal_not_zero y) |
|
1083 then show ?thesis |
|
1084 by (metis (no_types, lifting) DiffD2 HFinite_Infinitesimal_not_zero Infinitesimal_mult_disj x approx_def approx_sym left_diff_distrib left_inverse) |
|
1085 qed |
1116 |
1086 |
1117 (*Used for NSLIM_inverse, NSLIMSEQ_inverse*) |
1087 (*Used for NSLIM_inverse, NSLIMSEQ_inverse*) |
1118 lemmas star_of_approx_inverse = star_of_HFinite_diff_Infinitesimal [THEN [2] approx_inverse] |
1088 lemmas star_of_approx_inverse = star_of_HFinite_diff_Infinitesimal [THEN [2] approx_inverse] |
1119 lemmas hypreal_of_real_approx_inverse = hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse] |
1089 lemmas hypreal_of_real_approx_inverse = hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse] |
1120 |
1090 |
1302 text \<open> |
1266 text \<open> |
1303 Interesting slightly counterintuitive theorem: necessary |
1267 Interesting slightly counterintuitive theorem: necessary |
1304 for proving that an open interval is an NS open set. |
1268 for proving that an open interval is an NS open set. |
1305 \<close> |
1269 \<close> |
1306 lemma Infinitesimal_add_hypreal_of_real_less: |
1270 lemma Infinitesimal_add_hypreal_of_real_less: |
1307 "x < y \<Longrightarrow> u \<in> Infinitesimal \<Longrightarrow> hypreal_of_real x + u < hypreal_of_real y" |
1271 assumes "x < y" and u: "u \<in> Infinitesimal" |
1308 apply (simp add: Infinitesimal_def) |
1272 shows "hypreal_of_real x + u < hypreal_of_real y" |
1309 apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp) |
1273 proof - |
1310 apply (simp add: abs_less_iff) |
1274 have "\<bar>u\<bar> < hypreal_of_real y - hypreal_of_real x" |
1311 done |
1275 using InfinitesimalD \<open>x < y\<close> u by fastforce |
|
1276 then show ?thesis |
|
1277 by (simp add: abs_less_iff) |
|
1278 qed |
1312 |
1279 |
1313 lemma Infinitesimal_add_hrabs_hypreal_of_real_less: |
1280 lemma Infinitesimal_add_hrabs_hypreal_of_real_less: |
1314 "x \<in> Infinitesimal \<Longrightarrow> \<bar>hypreal_of_real r\<bar> < hypreal_of_real y \<Longrightarrow> |
1281 "x \<in> Infinitesimal \<Longrightarrow> \<bar>hypreal_of_real r\<bar> < hypreal_of_real y \<Longrightarrow> |
1315 \<bar>hypreal_of_real r + x\<bar> < hypreal_of_real y" |
1282 \<bar>hypreal_of_real r + x\<bar> < hypreal_of_real y" |
1316 apply (drule_tac x = "hypreal_of_real r" in approx_hrabs_add_Infinitesimal) |
1283 by (metis Infinitesimal_add_hypreal_of_real_less approx_hrabs_add_Infinitesimal approx_sym bex_Infinitesimal_iff2 star_of_abs star_of_less) |
1317 apply (drule approx_sym [THEN bex_Infinitesimal_iff2 [THEN iffD2]]) |
|
1318 apply (auto intro!: Infinitesimal_add_hypreal_of_real_less |
|
1319 simp del: star_of_abs simp add: star_of_abs [symmetric]) |
|
1320 done |
|
1321 |
1284 |
1322 lemma Infinitesimal_add_hrabs_hypreal_of_real_less2: |
1285 lemma Infinitesimal_add_hrabs_hypreal_of_real_less2: |
1323 "x \<in> Infinitesimal \<Longrightarrow> \<bar>hypreal_of_real r\<bar> < hypreal_of_real y \<Longrightarrow> |
1286 "x \<in> Infinitesimal \<Longrightarrow> \<bar>hypreal_of_real r\<bar> < hypreal_of_real y \<Longrightarrow> |
1324 \<bar>x + hypreal_of_real r\<bar> < hypreal_of_real y" |
1287 \<bar>x + hypreal_of_real r\<bar> < hypreal_of_real y" |
1325 using Infinitesimal_add_hrabs_hypreal_of_real_less by fastforce |
1288 using Infinitesimal_add_hrabs_hypreal_of_real_less by fastforce |
1326 |
1289 |
1327 lemma hypreal_of_real_le_add_Infininitesimal_cancel: |
1290 lemma hypreal_of_real_le_add_Infininitesimal_cancel: |
1328 "u \<in> Infinitesimal \<Longrightarrow> v \<in> Infinitesimal \<Longrightarrow> |
1291 assumes le: "hypreal_of_real x + u \<le> hypreal_of_real y + v" |
1329 hypreal_of_real x + u \<le> hypreal_of_real y + v \<Longrightarrow> |
1292 and u: "u \<in> Infinitesimal" and v: "v \<in> Infinitesimal" |
1330 hypreal_of_real x \<le> hypreal_of_real y" |
1293 shows "hypreal_of_real x \<le> hypreal_of_real y" |
1331 apply (simp add: linorder_not_less [symmetric], auto) |
1294 proof (rule ccontr) |
1332 apply (drule_tac u = "v-u" in Infinitesimal_add_hypreal_of_real_less) |
1295 assume "\<not> hypreal_of_real x \<le> hypreal_of_real y" |
1333 apply (auto simp add: Infinitesimal_diff) |
1296 then have "hypreal_of_real y + (v - u) < hypreal_of_real x" |
1334 done |
1297 by (simp add: Infinitesimal_add_hypreal_of_real_less Infinitesimal_diff u v) |
|
1298 then show False |
|
1299 by (simp add: add_diff_eq add_le_imp_le_diff le leD) |
|
1300 qed |
1335 |
1301 |
1336 lemma hypreal_of_real_le_add_Infininitesimal_cancel2: |
1302 lemma hypreal_of_real_le_add_Infininitesimal_cancel2: |
1337 "u \<in> Infinitesimal \<Longrightarrow> v \<in> Infinitesimal \<Longrightarrow> |
1303 "u \<in> Infinitesimal \<Longrightarrow> v \<in> Infinitesimal \<Longrightarrow> |
1338 hypreal_of_real x + u \<le> hypreal_of_real y + v \<Longrightarrow> x \<le> y" |
1304 hypreal_of_real x + u \<le> hypreal_of_real y + v \<Longrightarrow> x \<le> y" |
1339 by (blast intro: star_of_le [THEN iffD1] intro!: hypreal_of_real_le_add_Infininitesimal_cancel) |
1305 by (blast intro: star_of_le [THEN iffD1] intro!: hypreal_of_real_le_add_Infininitesimal_cancel) |
1340 |
1306 |
1341 lemma hypreal_of_real_less_Infinitesimal_le_zero: |
1307 lemma hypreal_of_real_less_Infinitesimal_le_zero: |
1342 "hypreal_of_real x < e \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> hypreal_of_real x \<le> 0" |
1308 "hypreal_of_real x < e \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> hypreal_of_real x \<le> 0" |
1343 by (metis Infinitesimal_interval eq_iff le_less_linear star_of_Infinitesimal_iff_0 star_of_eq_0) |
1309 by (metis Infinitesimal_interval eq_iff le_less_linear star_of_Infinitesimal_iff_0 star_of_eq_0) |
1344 |
1310 |
1345 (*used once, in Lim/NSDERIV_inverse*) |
|
1346 lemma Infinitesimal_add_not_zero: "h \<in> Infinitesimal \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> star_of x + h \<noteq> 0" |
1311 lemma Infinitesimal_add_not_zero: "h \<in> Infinitesimal \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> star_of x + h \<noteq> 0" |
1347 apply auto |
1312 by (metis Infinitesimal_add_approx_self star_of_approx_zero_iff) |
1348 apply (subgoal_tac "h = - star_of x") |
|
1349 apply (auto intro: minus_unique [symmetric]) |
|
1350 done |
|
1351 |
|
1352 lemma Infinitesimal_square_cancel [simp]: "x * x + y * y \<in> Infinitesimal \<Longrightarrow> x * x \<in> Infinitesimal" |
|
1353 for x y :: hypreal |
|
1354 by (meson Infinitesimal_interval2 le_add_same_cancel1 not_Infinitesimal_not_zero zero_le_square) |
|
1355 |
|
1356 lemma HFinite_square_cancel [simp]: "x * x + y * y \<in> HFinite \<Longrightarrow> x * x \<in> HFinite" |
|
1357 for x y :: hypreal |
|
1358 using HFinite_bounded le_add_same_cancel1 zero_le_square by blast |
|
1359 |
|
1360 lemma Infinitesimal_square_cancel2 [simp]: "x * x + y * y \<in> Infinitesimal \<Longrightarrow> y * y \<in> Infinitesimal" |
|
1361 for x y :: hypreal |
|
1362 apply (rule Infinitesimal_square_cancel) |
|
1363 apply (rule add.commute [THEN subst]) |
|
1364 apply simp |
|
1365 done |
|
1366 |
|
1367 lemma HFinite_square_cancel2 [simp]: "x * x + y * y \<in> HFinite \<Longrightarrow> y * y \<in> HFinite" |
|
1368 for x y :: hypreal |
|
1369 apply (rule HFinite_square_cancel) |
|
1370 apply (rule add.commute [THEN subst]) |
|
1371 apply simp |
|
1372 done |
|
1373 |
|
1374 lemma Infinitesimal_sum_square_cancel [simp]: |
|
1375 "x * x + y * y + z * z \<in> Infinitesimal \<Longrightarrow> x * x \<in> Infinitesimal" |
|
1376 for x y z :: hypreal |
|
1377 apply (rule Infinitesimal_interval2, assumption) |
|
1378 apply (rule_tac [2] zero_le_square, simp) |
|
1379 apply (insert zero_le_square [of y]) |
|
1380 apply (insert zero_le_square [of z], simp del:zero_le_square) |
|
1381 done |
|
1382 |
|
1383 lemma HFinite_sum_square_cancel [simp]: "x * x + y * y + z * z \<in> HFinite \<Longrightarrow> x * x \<in> HFinite" |
|
1384 for x y z :: hypreal |
|
1385 apply (rule HFinite_bounded, assumption) |
|
1386 apply (rule_tac [2] zero_le_square) |
|
1387 apply (insert zero_le_square [of y]) |
|
1388 apply (insert zero_le_square [of z], simp del:zero_le_square) |
|
1389 done |
|
1390 |
|
1391 lemma Infinitesimal_sum_square_cancel2 [simp]: |
|
1392 "y * y + x * x + z * z \<in> Infinitesimal \<Longrightarrow> x * x \<in> Infinitesimal" |
|
1393 for x y z :: hypreal |
|
1394 apply (rule Infinitesimal_sum_square_cancel) |
|
1395 apply (simp add: ac_simps) |
|
1396 done |
|
1397 |
|
1398 lemma HFinite_sum_square_cancel2 [simp]: "y * y + x * x + z * z \<in> HFinite \<Longrightarrow> x * x \<in> HFinite" |
|
1399 for x y z :: hypreal |
|
1400 apply (rule HFinite_sum_square_cancel) |
|
1401 apply (simp add: ac_simps) |
|
1402 done |
|
1403 |
|
1404 lemma Infinitesimal_sum_square_cancel3 [simp]: |
|
1405 "z * z + y * y + x * x \<in> Infinitesimal \<Longrightarrow> x * x \<in> Infinitesimal" |
|
1406 for x y z :: hypreal |
|
1407 apply (rule Infinitesimal_sum_square_cancel) |
|
1408 apply (simp add: ac_simps) |
|
1409 done |
|
1410 |
|
1411 lemma HFinite_sum_square_cancel3 [simp]: "z * z + y * y + x * x \<in> HFinite \<Longrightarrow> x * x \<in> HFinite" |
|
1412 for x y z :: hypreal |
|
1413 apply (rule HFinite_sum_square_cancel) |
|
1414 apply (simp add: ac_simps) |
|
1415 done |
|
1416 |
1313 |
1417 lemma monad_hrabs_less: "y \<in> monad x \<Longrightarrow> 0 < hypreal_of_real e \<Longrightarrow> \<bar>y - x\<bar> < hypreal_of_real e" |
1314 lemma monad_hrabs_less: "y \<in> monad x \<Longrightarrow> 0 < hypreal_of_real e \<Longrightarrow> \<bar>y - x\<bar> < hypreal_of_real e" |
1418 by (simp add: Infinitesimal_approx_minus approx_sym less_Infinitesimal_less mem_monad_approx) |
1315 by (simp add: Infinitesimal_approx_minus approx_sym less_Infinitesimal_less mem_monad_approx) |
1419 |
1316 |
1420 lemma mem_monad_SReal_HFinite: "x \<in> monad (hypreal_of_real a) \<Longrightarrow> x \<in> HFinite" |
1317 lemma mem_monad_SReal_HFinite: "x \<in> monad (hypreal_of_real a) \<Longrightarrow> x \<in> HFinite" |
1515 |
1395 |
1516 lemma st_not_Infinitesimal: "st(x) \<noteq> 0 \<Longrightarrow> x \<notin> Infinitesimal" |
1396 lemma st_not_Infinitesimal: "st(x) \<noteq> 0 \<Longrightarrow> x \<notin> Infinitesimal" |
1517 by (fast intro: st_Infinitesimal) |
1397 by (fast intro: st_Infinitesimal) |
1518 |
1398 |
1519 lemma st_inverse: "x \<in> HFinite \<Longrightarrow> st x \<noteq> 0 \<Longrightarrow> st (inverse x) = inverse (st x)" |
1399 lemma st_inverse: "x \<in> HFinite \<Longrightarrow> st x \<noteq> 0 \<Longrightarrow> st (inverse x) = inverse (st x)" |
1520 apply (rule_tac c1 = "st x" in mult_left_cancel [THEN iffD1]) |
1400 by (simp add: approx_inverse st_SReal st_approx_self st_not_Infinitesimal st_unique) |
1521 apply (auto simp add: st_mult [symmetric] st_not_Infinitesimal HFinite_inverse) |
|
1522 apply (subst right_inverse, auto) |
|
1523 done |
|
1524 |
1401 |
1525 lemma st_divide [simp]: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> st y \<noteq> 0 \<Longrightarrow> st (x / y) = st x / st y" |
1402 lemma st_divide [simp]: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> st y \<noteq> 0 \<Longrightarrow> st (x / y) = st x / st y" |
1526 by (simp add: divide_inverse st_mult st_not_Infinitesimal HFinite_inverse st_inverse) |
1403 by (simp add: divide_inverse st_mult st_not_Infinitesimal HFinite_inverse st_inverse) |
1527 |
1404 |
1528 lemma st_idempotent [simp]: "x \<in> HFinite \<Longrightarrow> st (st x) = st x" |
1405 lemma st_idempotent [simp]: "x \<in> HFinite \<Longrightarrow> st (st x) = st x" |
1529 by (blast intro: st_HFinite st_approx_self approx_st_eq) |
1406 by (blast intro: st_HFinite st_approx_self approx_st_eq) |
1530 |
1407 |
1531 lemma Infinitesimal_add_st_less: |
1408 lemma Infinitesimal_add_st_less: |
1532 "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> u \<in> Infinitesimal \<Longrightarrow> st x < st y \<Longrightarrow> st x + u < st y" |
1409 "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> u \<in> Infinitesimal \<Longrightarrow> st x < st y \<Longrightarrow> st x + u < st y" |
1533 apply (drule st_SReal)+ |
1410 by (metis Infinitesimal_add_hypreal_of_real_less SReal_iff st_SReal star_of_less) |
1534 apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: SReal_iff) |
|
1535 done |
|
1536 |
1411 |
1537 lemma Infinitesimal_add_st_le_cancel: |
1412 lemma Infinitesimal_add_st_le_cancel: |
1538 "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> u \<in> Infinitesimal \<Longrightarrow> |
1413 "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> u \<in> Infinitesimal \<Longrightarrow> |
1539 st x \<le> st y + u \<Longrightarrow> st x \<le> st y" |
1414 st x \<le> st y + u \<Longrightarrow> st x \<le> st y" |
1540 apply (simp add: linorder_not_less [symmetric]) |
1415 by (meson Infinitesimal_add_st_less leD le_less_linear) |
1541 apply (auto dest: Infinitesimal_add_st_less) |
|
1542 done |
|
1543 |
1416 |
1544 lemma st_le: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x \<le> y \<Longrightarrow> st x \<le> st y" |
1417 lemma st_le: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x \<le> y \<Longrightarrow> st x \<le> st y" |
1545 by (metis approx_le_bound approx_sym linear st_SReal st_approx_self st_part_Ex1) |
1418 by (metis approx_le_bound approx_sym linear st_SReal st_approx_self st_part_Ex1) |
1546 |
1419 |
1547 lemma st_zero_le: "0 \<le> x \<Longrightarrow> x \<in> HFinite \<Longrightarrow> 0 \<le> st x" |
1420 lemma st_zero_le: "0 \<le> x \<Longrightarrow> x \<in> HFinite \<Longrightarrow> 0 \<le> st x" |
1548 apply (subst st_0 [symmetric]) |
1421 by (metis HFinite_0 st_0 st_le) |
1549 apply (rule st_le, auto) |
|
1550 done |
|
1551 |
1422 |
1552 lemma st_zero_ge: "x \<le> 0 \<Longrightarrow> x \<in> HFinite \<Longrightarrow> st x \<le> 0" |
1423 lemma st_zero_ge: "x \<le> 0 \<Longrightarrow> x \<in> HFinite \<Longrightarrow> st x \<le> 0" |
1553 apply (subst st_0 [symmetric]) |
1424 by (metis HFinite_0 st_0 st_le) |
1554 apply (rule st_le, auto) |
|
1555 done |
|
1556 |
1425 |
1557 lemma st_hrabs: "x \<in> HFinite \<Longrightarrow> \<bar>st x\<bar> = st \<bar>x\<bar>" |
1426 lemma st_hrabs: "x \<in> HFinite \<Longrightarrow> \<bar>st x\<bar> = st \<bar>x\<bar>" |
1558 apply (simp add: linorder_not_le st_zero_le abs_if st_minus linorder_not_less) |
1427 by (simp add: order_class.order.antisym st_zero_ge linorder_not_le st_zero_le abs_if st_minus linorder_not_less) |
1559 apply (auto dest!: st_zero_ge [OF order_less_imp_le]) |
|
1560 done |
|
1561 |
1428 |
1562 |
1429 |
1563 subsection \<open>Alternative Definitions using Free Ultrafilter\<close> |
1430 subsection \<open>Alternative Definitions using Free Ultrafilter\<close> |
1564 |
1431 |
1565 subsubsection \<open>\<^term>\<open>HFinite\<close>\<close> |
1432 subsubsection \<open>\<^term>\<open>HFinite\<close>\<close> |
1566 |
1433 |
1567 lemma HFinite_FreeUltrafilterNat: |
1434 lemma HFinite_FreeUltrafilterNat: |
1568 "star_n X \<in> HFinite \<Longrightarrow> \<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U>" |
1435 assumes "star_n X \<in> HFinite" |
1569 apply (auto simp add: HFinite_def SReal_def) |
1436 shows "\<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U>" |
1570 apply (rule_tac x=r in exI) |
1437 proof - |
1571 apply (simp add: hnorm_def star_of_def starfun_star_n) |
1438 obtain r where "hnorm (star_n X) < hypreal_of_real r" |
1572 apply (simp add: star_less_def starP2_star_n) |
1439 using HFiniteD SReal_iff assms by fastforce |
1573 done |
1440 then have "\<forall>\<^sub>F n in \<U>. norm (X n) < r" |
|
1441 by (simp add: hnorm_def star_n_less star_of_def starfun_star_n) |
|
1442 then show ?thesis .. |
|
1443 qed |
1574 |
1444 |
1575 lemma FreeUltrafilterNat_HFinite: |
1445 lemma FreeUltrafilterNat_HFinite: |
1576 "\<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U> \<Longrightarrow> star_n X \<in> HFinite" |
1446 assumes "eventually (\<lambda>n. norm (X n) < u) \<U>" |
1577 apply (auto simp add: HFinite_def mem_Rep_star_iff) |
1447 shows "star_n X \<in> HFinite" |
1578 apply (rule_tac x="star_of u" in bexI) |
1448 proof - |
1579 apply (simp add: hnorm_def starfun_star_n star_of_def) |
1449 have "hnorm (star_n X) < hypreal_of_real u" |
1580 apply (simp add: star_less_def starP2_star_n) |
1450 by (simp add: assms hnorm_def star_n_less star_of_def starfun_star_n) |
1581 apply (simp add: SReal_def) |
1451 then show ?thesis |
1582 done |
1452 by (meson HInfiniteD SReal_hypreal_of_real less_asym not_HFinite_HInfinite) |
|
1453 qed |
1583 |
1454 |
1584 lemma HFinite_FreeUltrafilterNat_iff: |
1455 lemma HFinite_FreeUltrafilterNat_iff: |
1585 "star_n X \<in> HFinite \<longleftrightarrow> (\<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U>)" |
1456 "star_n X \<in> HFinite \<longleftrightarrow> (\<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U>)" |
1586 by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite) |
1457 using FreeUltrafilterNat_HFinite HFinite_FreeUltrafilterNat by blast |
1587 |
1458 |
1588 |
1459 |
1589 subsubsection \<open>\<^term>\<open>HInfinite\<close>\<close> |
1460 subsubsection \<open>\<^term>\<open>HInfinite\<close>\<close> |
1590 |
|
1591 lemma lemma_Compl_eq: "- {n. u < norm (f n)} = {n. norm (f n) \<le> u}" |
|
1592 by auto |
|
1593 |
|
1594 lemma lemma_Compl_eq2: "- {n. norm (f n) < u} = {n. u \<le> norm (f n)}" |
|
1595 by auto |
|
1596 |
|
1597 lemma lemma_Int_eq1: "{n. norm (f n) \<le> u} Int {n. u \<le> norm (f n)} = {n. norm(f n) = u}" |
|
1598 by auto |
|
1599 |
|
1600 lemma lemma_FreeUltrafilterNat_one: "{n. norm (f n) = u} \<le> {n. norm (f n) < u + (1::real)}" |
|
1601 by auto |
|
1602 |
1461 |
1603 text \<open>Exclude this type of sets from free ultrafilter for Infinite numbers!\<close> |
1462 text \<open>Exclude this type of sets from free ultrafilter for Infinite numbers!\<close> |
1604 lemma FreeUltrafilterNat_const_Finite: |
1463 lemma FreeUltrafilterNat_const_Finite: |
1605 "eventually (\<lambda>n. norm (X n) = u) \<U> \<Longrightarrow> star_n X \<in> HFinite" |
1464 "eventually (\<lambda>n. norm (X n) = u) \<U> \<Longrightarrow> star_n X \<in> HFinite" |
1606 apply (rule FreeUltrafilterNat_HFinite) |
1465 by (simp add: FreeUltrafilterNat_HFinite [where u = "u+1"] eventually_mono) |
1607 apply (rule_tac x = "u + 1" in exI) |
|
1608 apply (auto elim: eventually_mono) |
|
1609 done |
|
1610 |
1466 |
1611 lemma HInfinite_FreeUltrafilterNat: |
1467 lemma HInfinite_FreeUltrafilterNat: |
1612 "star_n X \<in> HInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < norm (X n)) \<U>" |
1468 "star_n X \<in> HInfinite \<Longrightarrow> eventually (\<lambda>n. u < norm (X n)) \<U>" |
1613 apply (drule HInfinite_HFinite_iff [THEN iffD1]) |
1469 apply (drule HInfinite_HFinite_iff [THEN iffD1]) |
1614 apply (simp add: HFinite_FreeUltrafilterNat_iff) |
1470 apply (simp add: HFinite_FreeUltrafilterNat_iff) |
1615 apply (rule allI, drule_tac x="u + 1" in spec) |
1471 apply (drule_tac x="u + 1" in spec) |
1616 apply (simp add: FreeUltrafilterNat.eventually_not_iff[symmetric]) |
1472 apply (simp add: FreeUltrafilterNat.eventually_not_iff[symmetric]) |
1617 apply (auto elim: eventually_mono) |
1473 apply (auto elim: eventually_mono) |
1618 done |
1474 done |
1619 |
1475 |
1620 lemma lemma_Int_HI: "{n. norm (Xa n) < u} \<inter> {n. X n = Xa n} \<subseteq> {n. norm (X n) < u}" |
|
1621 for u :: real |
|
1622 by auto |
|
1623 |
|
1624 lemma FreeUltrafilterNat_HInfinite: |
1476 lemma FreeUltrafilterNat_HInfinite: |
1625 "\<forall>u. eventually (\<lambda>n. u < norm (X n)) \<U> \<Longrightarrow> star_n X \<in> HInfinite" |
1477 assumes "\<And>u. eventually (\<lambda>n. u < norm (X n)) \<U>" |
1626 apply (rule HInfinite_HFinite_iff [THEN iffD2]) |
1478 shows "star_n X \<in> HInfinite" |
1627 apply (safe, drule HFinite_FreeUltrafilterNat, safe) |
|
1628 apply (drule_tac x = u in spec) |
|
1629 proof - |
1479 proof - |
1630 fix u |
1480 { fix u |
1631 assume "\<forall>\<^sub>Fn in \<U>. norm (X n) < u" "\<forall>\<^sub>Fn in \<U>. u < norm (X n)" |
1481 assume "\<forall>\<^sub>Fn in \<U>. norm (X n) < u" "\<forall>\<^sub>Fn in \<U>. u < norm (X n)" |
1632 then have "\<forall>\<^sub>F x in \<U>. False" |
1482 then have "\<forall>\<^sub>F x in \<U>. False" |
1633 by eventually_elim auto |
1483 by eventually_elim auto |
1634 then show False |
1484 then have False |
1635 by (simp add: eventually_False FreeUltrafilterNat.proper) |
1485 by (simp add: eventually_False FreeUltrafilterNat.proper) } |
|
1486 then show ?thesis |
|
1487 using HFinite_FreeUltrafilterNat HInfinite_HFinite_iff assms by blast |
1636 qed |
1488 qed |
1637 |
1489 |
1638 lemma HInfinite_FreeUltrafilterNat_iff: |
1490 lemma HInfinite_FreeUltrafilterNat_iff: |
1639 "star_n X \<in> HInfinite \<longleftrightarrow> (\<forall>u. eventually (\<lambda>n. u < norm (X n)) \<U>)" |
1491 "star_n X \<in> HInfinite \<longleftrightarrow> (\<forall>u. eventually (\<lambda>n. u < norm (X n)) \<U>)" |
1640 by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite) |
1492 using HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite by blast |
1641 |
1493 |
1642 |
1494 |
1643 subsubsection \<open>\<^term>\<open>Infinitesimal\<close>\<close> |
1495 subsubsection \<open>\<^term>\<open>Infinitesimal\<close>\<close> |
1644 |
1496 |
1645 lemma ball_SReal_eq: "(\<forall>x::hypreal \<in> Reals. P x) \<longleftrightarrow> (\<forall>x::real. P (star_of x))" |
1497 lemma ball_SReal_eq: "(\<forall>x::hypreal \<in> Reals. P x) \<longleftrightarrow> (\<forall>x::real. P (star_of x))" |
1646 by (auto simp: SReal_def) |
1498 by (auto simp: SReal_def) |
1647 |
1499 |
1648 lemma Infinitesimal_FreeUltrafilterNat: |
|
1649 "star_n X \<in> Infinitesimal \<Longrightarrow> \<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>" |
|
1650 apply (simp add: Infinitesimal_def ball_SReal_eq) |
|
1651 apply (simp add: hnorm_def starfun_star_n star_of_def) |
|
1652 apply (simp add: star_less_def starP2_star_n) |
|
1653 done |
|
1654 |
|
1655 lemma FreeUltrafilterNat_Infinitesimal: |
|
1656 "\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U> \<Longrightarrow> star_n X \<in> Infinitesimal" |
|
1657 apply (simp add: Infinitesimal_def ball_SReal_eq) |
|
1658 apply (simp add: hnorm_def starfun_star_n star_of_def) |
|
1659 apply (simp add: star_less_def starP2_star_n) |
|
1660 done |
|
1661 |
1500 |
1662 lemma Infinitesimal_FreeUltrafilterNat_iff: |
1501 lemma Infinitesimal_FreeUltrafilterNat_iff: |
1663 "(star_n X \<in> Infinitesimal) = (\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>)" |
1502 "(star_n X \<in> Infinitesimal) = (\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>)" (is "?lhs = ?rhs") |
1664 by (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal) |
1503 proof |
|
1504 assume ?lhs |
|
1505 then show ?rhs |
|
1506 apply (simp add: Infinitesimal_def ball_SReal_eq) |
|
1507 apply (simp add: hnorm_def starfun_star_n star_of_def star_less_def starP2_star_n) |
|
1508 done |
|
1509 next |
|
1510 assume ?rhs |
|
1511 then show ?lhs |
|
1512 apply (simp add: Infinitesimal_def ball_SReal_eq) |
|
1513 apply (simp add: hnorm_def starfun_star_n star_of_def star_less_def starP2_star_n) |
|
1514 done |
|
1515 qed |
1665 |
1516 |
1666 |
1517 |
1667 text \<open>Infinitesimals as smaller than \<open>1/n\<close> for all \<open>n::nat (> 0)\<close>.\<close> |
1518 text \<open>Infinitesimals as smaller than \<open>1/n\<close> for all \<open>n::nat (> 0)\<close>.\<close> |
1668 |
1519 |
1669 lemma lemma_Infinitesimal: "(\<forall>r. 0 < r \<longrightarrow> x < r) \<longleftrightarrow> (\<forall>n. x < inverse (real (Suc n)))" |
1520 lemma lemma_Infinitesimal: "(\<forall>r. 0 < r \<longrightarrow> x < r) \<longleftrightarrow> (\<forall>n. x < inverse (real (Suc n)))" |