160 |
160 |
161 lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = \<real>" |
161 lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = \<real>" |
162 by (simp add: Reals_eq_Standard Standard_def) |
162 by (simp add: Reals_eq_Standard Standard_def) |
163 |
163 |
164 lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` \<real> = UNIV" |
164 lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` \<real> = UNIV" |
165 apply (auto simp add: SReal_def) |
165 by (simp add: Reals_eq_Standard Standard_def inj_star_of) |
166 apply (rule inj_star_of [THEN inv_f_f, THEN subst], blast) |
|
167 done |
|
168 |
|
169 lemma SReal_hypreal_of_real_image: "\<exists>x. x \<in> P \<Longrightarrow> P \<subseteq> \<real> \<Longrightarrow> \<exists>Q. P = hypreal_of_real ` Q" |
|
170 unfolding SReal_def image_def by blast |
|
171 |
166 |
172 lemma SReal_dense: "x \<in> \<real> \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x < y \<Longrightarrow> \<exists>r \<in> Reals. x < r \<and> r < y" |
167 lemma SReal_dense: "x \<in> \<real> \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x < y \<Longrightarrow> \<exists>r \<in> Reals. x < r \<and> r < y" |
173 for x y :: hypreal |
168 for x y :: hypreal |
174 apply (auto simp: SReal_def) |
169 using dense by (fastforce simp add: SReal_def) |
175 apply (drule dense) |
|
176 apply auto |
|
177 done |
|
178 |
|
179 |
|
180 text \<open>Completeness of Reals, but both lemmas are unused.\<close> |
|
181 |
|
182 lemma SReal_sup_lemma: |
|
183 "P \<subseteq> \<real> \<Longrightarrow> (\<exists>x \<in> P. y < x) = (\<exists>X. hypreal_of_real X \<in> P \<and> y < hypreal_of_real X)" |
|
184 by (blast dest!: SReal_iff [THEN iffD1]) |
|
185 |
|
186 lemma SReal_sup_lemma2: |
|
187 "P \<subseteq> \<real> \<Longrightarrow> \<exists>x. x \<in> P \<Longrightarrow> \<exists>y \<in> Reals. \<forall>x \<in> P. x < y \<Longrightarrow> |
|
188 (\<exists>X. X \<in> {w. hypreal_of_real w \<in> P}) \<and> |
|
189 (\<exists>Y. \<forall>X \<in> {w. hypreal_of_real w \<in> P}. X < Y)" |
|
190 apply (rule conjI) |
|
191 apply (fast dest!: SReal_iff [THEN iffD1]) |
|
192 apply (auto, frule subsetD, assumption) |
|
193 apply (drule SReal_iff [THEN iffD1]) |
|
194 apply (auto, rule_tac x = ya in exI, auto) |
|
195 done |
|
196 |
170 |
197 |
171 |
198 subsection \<open>Set of Finite Elements is a Subring of the Extended Reals\<close> |
172 subsection \<open>Set of Finite Elements is a Subring of the Extended Reals\<close> |
199 |
173 |
200 lemma HFinite_add: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x + y \<in> HFinite" |
174 lemma HFinite_add: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x + y \<in> HFinite" |
295 by (subst Infinitesimal_hnorm_iff [symmetric]) simp |
278 by (subst Infinitesimal_hnorm_iff [symmetric]) simp |
296 |
279 |
297 lemma Infinitesimal_diff: "x \<in> Infinitesimal \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x - y \<in> Infinitesimal" |
280 lemma Infinitesimal_diff: "x \<in> Infinitesimal \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x - y \<in> Infinitesimal" |
298 using Infinitesimal_add [of x "- y"] by simp |
281 using Infinitesimal_add [of x "- y"] by simp |
299 |
282 |
300 lemma Infinitesimal_mult: "x \<in> Infinitesimal \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x * y \<in> Infinitesimal" |
283 lemma Infinitesimal_mult: |
301 for x y :: "'a::real_normed_algebra star" |
284 fixes x y :: "'a::real_normed_algebra star" |
302 apply (rule InfinitesimalI) |
285 assumes "x \<in> Infinitesimal" "y \<in> Infinitesimal" |
303 apply (subgoal_tac "hnorm (x * y) < 1 * r") |
286 shows "x * y \<in> Infinitesimal" |
304 apply (simp only: mult_1) |
287 proof (rule InfinitesimalI) |
305 apply (rule hnorm_mult_less) |
288 show "hnorm (x * y) < r" |
306 apply (simp_all add: InfinitesimalD) |
289 if "r \<in> \<real>" and "0 < r" for r :: "real star" |
307 done |
290 proof - |
308 |
291 have "hnorm x < 1" "hnorm y < r" |
309 lemma Infinitesimal_HFinite_mult: "x \<in> Infinitesimal \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x * y \<in> Infinitesimal" |
292 using assms that by (auto simp add: InfinitesimalD) |
310 for x y :: "'a::real_normed_algebra star" |
293 then show ?thesis |
311 apply (rule InfinitesimalI) |
294 using hnorm_mult_less by fastforce |
312 apply (drule HFiniteD, clarify) |
295 qed |
313 apply (subgoal_tac "0 < t") |
296 qed |
314 apply (subgoal_tac "hnorm (x * y) < (r / t) * t", simp) |
297 |
315 apply (subgoal_tac "0 < r / t") |
298 lemma Infinitesimal_HFinite_mult: |
316 apply (rule hnorm_mult_less) |
299 fixes x y :: "'a::real_normed_algebra star" |
317 apply (simp add: InfinitesimalD) |
300 assumes "x \<in> Infinitesimal" "y \<in> HFinite" |
318 apply assumption |
301 shows "x * y \<in> Infinitesimal" |
319 apply simp |
302 proof (rule InfinitesimalI) |
320 apply (erule order_le_less_trans [OF hnorm_ge_zero]) |
303 obtain t where "hnorm y < t" "t \<in> Reals" |
321 done |
304 using HFiniteD \<open>y \<in> HFinite\<close> by blast |
|
305 then have "t > 0" |
|
306 using hnorm_ge_zero le_less_trans by blast |
|
307 show "hnorm (x * y) < r" |
|
308 if "r \<in> \<real>" and "0 < r" for r :: "real star" |
|
309 proof - |
|
310 have "hnorm x < r/t" |
|
311 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) |
|
312 then have "hnorm (x * y) < (r / t) * t" |
|
313 using \<open>hnorm y < t\<close> hnorm_mult_less by blast |
|
314 then show ?thesis |
|
315 using \<open>0 < t\<close> by auto |
|
316 qed |
|
317 qed |
322 |
318 |
323 lemma Infinitesimal_HFinite_scaleHR: |
319 lemma Infinitesimal_HFinite_scaleHR: |
324 "x \<in> Infinitesimal \<Longrightarrow> y \<in> HFinite \<Longrightarrow> scaleHR x y \<in> Infinitesimal" |
320 assumes "x \<in> Infinitesimal" "y \<in> HFinite" |
325 apply (rule InfinitesimalI) |
321 shows "scaleHR x y \<in> Infinitesimal" |
326 apply (drule HFiniteD, clarify) |
322 proof (rule InfinitesimalI) |
327 apply (drule InfinitesimalD) |
323 obtain t where "hnorm y < t" "t \<in> Reals" |
328 apply (simp add: hnorm_scaleHR) |
324 using HFiniteD \<open>y \<in> HFinite\<close> by blast |
329 apply (subgoal_tac "0 < t") |
325 then have "t > 0" |
330 apply (subgoal_tac "\<bar>x\<bar> * hnorm y < (r / t) * t", simp) |
326 using hnorm_ge_zero le_less_trans by blast |
331 apply (subgoal_tac "0 < r / t") |
327 show "hnorm (scaleHR x y) < r" |
332 apply (rule mult_strict_mono', simp_all) |
328 if "r \<in> \<real>" and "0 < r" for r :: "real star" |
333 apply (erule order_le_less_trans [OF hnorm_ge_zero]) |
329 proof - |
334 done |
330 have "\<bar>x\<bar> * hnorm y < (r / t) * t" |
|
331 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) |
|
332 then show ?thesis |
|
333 by (simp add: \<open>0 < t\<close> hnorm_scaleHR less_imp_not_eq2) |
|
334 qed |
|
335 qed |
335 |
336 |
336 lemma Infinitesimal_HFinite_mult2: |
337 lemma Infinitesimal_HFinite_mult2: |
337 "x \<in> Infinitesimal \<Longrightarrow> y \<in> HFinite \<Longrightarrow> y * x \<in> Infinitesimal" |
338 fixes x y :: "'a::real_normed_algebra star" |
338 for x y :: "'a::real_normed_algebra star" |
339 assumes "x \<in> Infinitesimal" "y \<in> HFinite" |
339 apply (rule InfinitesimalI) |
340 shows "y * x \<in> Infinitesimal" |
340 apply (drule HFiniteD, clarify) |
341 proof (rule InfinitesimalI) |
341 apply (subgoal_tac "0 < t") |
342 obtain t where "hnorm y < t" "t \<in> Reals" |
342 apply (subgoal_tac "hnorm (y * x) < t * (r / t)", simp) |
343 using HFiniteD \<open>y \<in> HFinite\<close> by blast |
343 apply (subgoal_tac "0 < r / t") |
344 then have "t > 0" |
344 apply (rule hnorm_mult_less) |
345 using hnorm_ge_zero le_less_trans by blast |
345 apply assumption |
346 show "hnorm (y * x) < r" |
346 apply (simp add: InfinitesimalD) |
347 if "r \<in> \<real>" and "0 < r" for r :: "real star" |
347 apply simp |
348 proof - |
348 apply (erule order_le_less_trans [OF hnorm_ge_zero]) |
349 have "hnorm x < r/t" |
349 done |
350 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) |
350 |
351 then have "hnorm (y * x) < t * (r / t)" |
351 lemma Infinitesimal_scaleR2: "x \<in> Infinitesimal \<Longrightarrow> a *\<^sub>R x \<in> Infinitesimal" |
352 using \<open>hnorm y < t\<close> hnorm_mult_less by blast |
352 apply (case_tac "a = 0", simp) |
353 then show ?thesis |
353 apply (rule InfinitesimalI) |
354 using \<open>0 < t\<close> by auto |
354 apply (drule InfinitesimalD) |
355 qed |
355 apply (drule_tac x="r / \<bar>star_of a\<bar>" in bspec) |
356 qed |
356 apply (simp add: Reals_eq_Standard) |
357 |
357 apply simp |
358 lemma Infinitesimal_scaleR2: |
358 apply (simp add: hnorm_scaleR pos_less_divide_eq mult.commute) |
359 assumes "x \<in> Infinitesimal" shows "a *\<^sub>R x \<in> Infinitesimal" |
359 done |
360 by (metis HFinite_star_of Infinitesimal_HFinite_mult2 Infinitesimal_hnorm_iff assms hnorm_scaleR hypreal_hnorm_def star_of_norm) |
360 |
361 |
361 lemma Compl_HFinite: "- HFinite = HInfinite" |
362 lemma Compl_HFinite: "- HFinite = HInfinite" |
362 apply (auto simp add: HInfinite_def HFinite_def linorder_not_less) |
363 proof - |
363 apply (rule_tac y="r + 1" in order_less_le_trans, simp) |
364 have "r < hnorm x" if *: "\<And>s. s \<in> \<real> \<Longrightarrow> s \<le> hnorm x" and "r \<in> \<real>" |
364 apply simp |
365 for x :: "'a star" and r :: hypreal |
365 done |
366 using * [of "r+1"] \<open>r \<in> \<real>\<close> by auto |
366 |
367 then show ?thesis |
367 lemma HInfinite_inverse_Infinitesimal: "x \<in> HInfinite \<Longrightarrow> inverse x \<in> Infinitesimal" |
368 by (auto simp add: HInfinite_def HFinite_def linorder_not_less) |
|
369 qed |
|
370 |
|
371 lemma HInfinite_inverse_Infinitesimal: |
|
372 "x \<in> HInfinite \<Longrightarrow> inverse x \<in> Infinitesimal" |
368 for x :: "'a::real_normed_div_algebra star" |
373 for x :: "'a::real_normed_div_algebra star" |
369 apply (rule InfinitesimalI) |
374 by (simp add: HInfinite_def InfinitesimalI hnorm_inverse inverse_less_imp_less) |
370 apply (subgoal_tac "x \<noteq> 0") |
375 |
371 apply (rule inverse_less_imp_less) |
376 lemma inverse_Infinitesimal_iff_HInfinite: |
372 apply (simp add: nonzero_hnorm_inverse) |
377 "x \<noteq> 0 \<Longrightarrow> inverse x \<in> Infinitesimal \<longleftrightarrow> x \<in> HInfinite" |
373 apply (simp add: HInfinite_def Reals_inverse) |
378 for x :: "'a::real_normed_div_algebra star" |
374 apply assumption |
379 by (metis Compl_HFinite Compl_iff HInfinite_inverse_Infinitesimal InfinitesimalD Infinitesimal_HFinite_mult Reals_1 hnorm_one left_inverse less_irrefl zero_less_one) |
375 apply (clarify, simp add: Compl_HFinite [symmetric]) |
|
376 done |
|
377 |
380 |
378 lemma HInfiniteI: "(\<And>r. r \<in> \<real> \<Longrightarrow> r < hnorm x) \<Longrightarrow> x \<in> HInfinite" |
381 lemma HInfiniteI: "(\<And>r. r \<in> \<real> \<Longrightarrow> r < hnorm x) \<Longrightarrow> x \<in> HInfinite" |
379 by (simp add: HInfinite_def) |
382 by (simp add: HInfinite_def) |
380 |
383 |
381 lemma HInfiniteD: "x \<in> HInfinite \<Longrightarrow> r \<in> \<real> \<Longrightarrow> r < hnorm x" |
384 lemma HInfiniteD: "x \<in> HInfinite \<Longrightarrow> r \<in> \<real> \<Longrightarrow> r < hnorm x" |
382 by (simp add: HInfinite_def) |
385 by (simp add: HInfinite_def) |
383 |
386 |
384 lemma HInfinite_mult: "x \<in> HInfinite \<Longrightarrow> y \<in> HInfinite \<Longrightarrow> x * y \<in> HInfinite" |
387 lemma HInfinite_mult: |
385 for x y :: "'a::real_normed_div_algebra star" |
388 fixes x y :: "'a::real_normed_div_algebra star" |
386 apply (rule HInfiniteI, simp only: hnorm_mult) |
389 assumes "x \<in> HInfinite" "y \<in> HInfinite" shows "x * y \<in> HInfinite" |
387 apply (subgoal_tac "r * 1 < hnorm x * hnorm y", simp only: mult_1) |
390 proof (rule HInfiniteI, simp only: hnorm_mult) |
388 apply (case_tac "x = 0", simp add: HInfinite_def) |
391 have "x \<noteq> 0" |
389 apply (rule mult_strict_mono) |
392 using Compl_HFinite HFinite_0 assms by blast |
390 apply (simp_all add: HInfiniteD) |
393 show "r < hnorm x * hnorm y" |
391 done |
394 if "r \<in> \<real>" for r :: "real star" |
|
395 proof - |
|
396 have "r = r * 1" |
|
397 by simp |
|
398 also have "\<dots> < hnorm x * hnorm y" |
|
399 by (meson HInfiniteD Reals_1 \<open>x \<noteq> 0\<close> assms le_numeral_extra(1) mult_strict_mono that zero_less_hnorm_iff) |
|
400 finally show ?thesis . |
|
401 qed |
|
402 qed |
392 |
403 |
393 lemma hypreal_add_zero_less_le_mono: "r < x \<Longrightarrow> 0 \<le> y \<Longrightarrow> r < x + y" |
404 lemma hypreal_add_zero_less_le_mono: "r < x \<Longrightarrow> 0 \<le> y \<Longrightarrow> r < x + y" |
394 for r x y :: hypreal |
405 for r x y :: hypreal |
395 by (auto dest: add_less_le_mono) |
406 by simp |
396 |
407 |
397 lemma HInfinite_add_ge_zero: "x \<in> HInfinite \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x + y \<in> HInfinite" |
408 lemma HInfinite_add_ge_zero: "x \<in> HInfinite \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x + y \<in> HInfinite" |
398 for x y :: hypreal |
409 for x y :: hypreal |
399 by (auto simp: abs_if add.commute HInfinite_def) |
410 by (auto simp: abs_if add.commute HInfinite_def) |
400 |
411 |
486 by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow) |
487 by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow) |
487 |
488 |
488 lemma not_Infinitesimal_mult: |
489 lemma not_Infinitesimal_mult: |
489 "x \<notin> Infinitesimal \<Longrightarrow> y \<notin> Infinitesimal \<Longrightarrow> x * y \<notin> Infinitesimal" |
490 "x \<notin> Infinitesimal \<Longrightarrow> y \<notin> Infinitesimal \<Longrightarrow> x * y \<notin> Infinitesimal" |
490 for x y :: "'a::real_normed_div_algebra star" |
491 for x y :: "'a::real_normed_div_algebra star" |
491 apply (unfold Infinitesimal_def, clarify, rename_tac r s) |
492 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) |
492 apply (simp only: linorder_not_less hnorm_mult) |
|
493 apply (drule_tac x = "r * s" in bspec) |
|
494 apply (fast intro: Reals_mult) |
|
495 apply simp |
|
496 apply (drule_tac c = s and d = "hnorm y" and a = r and b = "hnorm x" in mult_mono) |
|
497 apply simp_all |
|
498 done |
|
499 |
493 |
500 lemma Infinitesimal_mult_disj: "x * y \<in> Infinitesimal \<Longrightarrow> x \<in> Infinitesimal \<or> y \<in> Infinitesimal" |
494 lemma Infinitesimal_mult_disj: "x * y \<in> Infinitesimal \<Longrightarrow> x \<in> Infinitesimal \<or> y \<in> Infinitesimal" |
501 for x y :: "'a::real_normed_div_algebra star" |
495 for x y :: "'a::real_normed_div_algebra star" |
502 apply (rule ccontr) |
496 using not_Infinitesimal_mult by blast |
503 apply (drule de_Morgan_disj [THEN iffD1]) |
|
504 apply (fast dest: not_Infinitesimal_mult) |
|
505 done |
|
506 |
497 |
507 lemma HFinite_Infinitesimal_not_zero: "x \<in> HFinite-Infinitesimal \<Longrightarrow> x \<noteq> 0" |
498 lemma HFinite_Infinitesimal_not_zero: "x \<in> HFinite-Infinitesimal \<Longrightarrow> x \<noteq> 0" |
508 by blast |
499 by blast |
509 |
500 |
510 lemma HFinite_Infinitesimal_diff_mult: |
501 lemma HFinite_Infinitesimal_diff_mult: |
511 "x \<in> HFinite - Infinitesimal \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> x * y \<in> HFinite - Infinitesimal" |
502 "x \<in> HFinite - Infinitesimal \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> x * y \<in> HFinite - Infinitesimal" |
512 for x y :: "'a::real_normed_div_algebra star" |
503 for x y :: "'a::real_normed_div_algebra star" |
513 apply clarify |
504 by (simp add: HFinite_mult not_Infinitesimal_mult) |
514 apply (blast dest: HFinite_mult not_Infinitesimal_mult) |
|
515 done |
|
516 |
505 |
517 lemma Infinitesimal_subset_HFinite: "Infinitesimal \<subseteq> HFinite" |
506 lemma Infinitesimal_subset_HFinite: "Infinitesimal \<subseteq> HFinite" |
518 apply (simp add: Infinitesimal_def HFinite_def) |
507 using HFinite_def InfinitesimalD Reals_1 zero_less_one by blast |
519 apply auto |
|
520 apply (rule_tac x = 1 in bexI) |
|
521 apply auto |
|
522 done |
|
523 |
508 |
524 lemma Infinitesimal_star_of_mult: "x \<in> Infinitesimal \<Longrightarrow> x * star_of r \<in> Infinitesimal" |
509 lemma Infinitesimal_star_of_mult: "x \<in> Infinitesimal \<Longrightarrow> x * star_of r \<in> Infinitesimal" |
525 for x :: "'a::real_normed_algebra star" |
510 for x :: "'a::real_normed_algebra star" |
526 by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult]) |
511 by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult]) |
527 |
512 |
652 |
631 |
653 lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) \<longleftrightarrow> x \<approx> z" |
632 lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) \<longleftrightarrow> x \<approx> z" |
654 by (force simp add: bex_Infinitesimal_iff [symmetric]) |
633 by (force simp add: bex_Infinitesimal_iff [symmetric]) |
655 |
634 |
656 lemma Infinitesimal_add_approx: "y \<in> Infinitesimal \<Longrightarrow> x + y = z \<Longrightarrow> x \<approx> z" |
635 lemma Infinitesimal_add_approx: "y \<in> Infinitesimal \<Longrightarrow> x + y = z \<Longrightarrow> x \<approx> z" |
657 apply (rule bex_Infinitesimal_iff [THEN iffD1]) |
636 using approx_sym bex_Infinitesimal_iff2 by blast |
658 apply (drule Infinitesimal_minus_iff [THEN iffD2]) |
|
659 apply (auto simp add: add.assoc [symmetric]) |
|
660 done |
|
661 |
637 |
662 lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> x + y" |
638 lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> x + y" |
663 apply (rule bex_Infinitesimal_iff [THEN iffD1]) |
639 by (simp add: Infinitesimal_add_approx) |
664 apply (drule Infinitesimal_minus_iff [THEN iffD2]) |
|
665 apply (auto simp add: add.assoc [symmetric]) |
|
666 done |
|
667 |
640 |
668 lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> y + x" |
641 lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> y + x" |
669 by (auto dest: Infinitesimal_add_approx_self simp add: add.commute) |
642 by (auto dest: Infinitesimal_add_approx_self simp add: add.commute) |
670 |
643 |
671 lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> x + - y" |
644 lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> x + - y" |
672 by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2]) |
645 by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2]) |
673 |
646 |
674 lemma Infinitesimal_add_cancel: "y \<in> Infinitesimal \<Longrightarrow> x + y \<approx> z \<Longrightarrow> x \<approx> z" |
647 lemma Infinitesimal_add_cancel: "y \<in> Infinitesimal \<Longrightarrow> x + y \<approx> z \<Longrightarrow> x \<approx> z" |
675 apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym]) |
648 using Infinitesimal_add_approx approx_trans by blast |
676 apply (erule approx_trans3 [THEN approx_sym], assumption) |
|
677 done |
|
678 |
649 |
679 lemma Infinitesimal_add_right_cancel: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> z + y \<Longrightarrow> x \<approx> z" |
650 lemma Infinitesimal_add_right_cancel: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> z + y \<Longrightarrow> x \<approx> z" |
680 apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym]) |
651 by (metis Infinitesimal_add_approx_self approx_monad_iff) |
681 apply (erule approx_trans3 [THEN approx_sym]) |
652 |
682 apply (simp add: add.commute) |
653 lemma approx_add_left_cancel: "d + b \<approx> d + c \<Longrightarrow> b \<approx> c" |
683 apply (erule approx_sym) |
654 by (metis add_diff_cancel_left bex_Infinitesimal_iff) |
684 done |
|
685 |
|
686 lemma approx_add_left_cancel: "d + b \<approx> d + c \<Longrightarrow> b \<approx> c" |
|
687 apply (drule approx_minus_iff [THEN iffD1]) |
|
688 apply (simp add: approx_minus_iff [symmetric] ac_simps) |
|
689 done |
|
690 |
655 |
691 lemma approx_add_right_cancel: "b + d \<approx> c + d \<Longrightarrow> b \<approx> c" |
656 lemma approx_add_right_cancel: "b + d \<approx> c + d \<Longrightarrow> b \<approx> c" |
692 apply (rule approx_add_left_cancel) |
657 by (simp add: approx_def) |
693 apply (simp add: add.commute) |
|
694 done |
|
695 |
658 |
696 lemma approx_add_mono1: "b \<approx> c \<Longrightarrow> d + b \<approx> d + c" |
659 lemma approx_add_mono1: "b \<approx> c \<Longrightarrow> d + b \<approx> d + c" |
697 apply (rule approx_minus_iff [THEN iffD2]) |
660 by (simp add: approx_add) |
698 apply (simp add: approx_minus_iff [symmetric] ac_simps) |
|
699 done |
|
700 |
661 |
701 lemma approx_add_mono2: "b \<approx> c \<Longrightarrow> b + a \<approx> c + a" |
662 lemma approx_add_mono2: "b \<approx> c \<Longrightarrow> b + a \<approx> c + a" |
702 by (simp add: add.commute approx_add_mono1) |
663 by (simp add: add.commute approx_add_mono1) |
703 |
664 |
704 lemma approx_add_left_iff [simp]: "a + b \<approx> a + c \<longleftrightarrow> b \<approx> c" |
665 lemma approx_add_left_iff [simp]: "a + b \<approx> a + c \<longleftrightarrow> b \<approx> c" |
706 |
667 |
707 lemma approx_add_right_iff [simp]: "b + a \<approx> c + a \<longleftrightarrow> b \<approx> c" |
668 lemma approx_add_right_iff [simp]: "b + a \<approx> c + a \<longleftrightarrow> b \<approx> c" |
708 by (simp add: add.commute) |
669 by (simp add: add.commute) |
709 |
670 |
710 lemma approx_HFinite: "x \<in> HFinite \<Longrightarrow> x \<approx> y \<Longrightarrow> y \<in> HFinite" |
671 lemma approx_HFinite: "x \<in> HFinite \<Longrightarrow> x \<approx> y \<Longrightarrow> y \<in> HFinite" |
711 apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe) |
672 by (metis HFinite_add Infinitesimal_subset_HFinite approx_sym subsetD bex_Infinitesimal_iff2) |
712 apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]]) |
|
713 apply (drule HFinite_add) |
|
714 apply (auto simp add: add.assoc) |
|
715 done |
|
716 |
673 |
717 lemma approx_star_of_HFinite: "x \<approx> star_of D \<Longrightarrow> x \<in> HFinite" |
674 lemma approx_star_of_HFinite: "x \<approx> star_of D \<Longrightarrow> x \<in> HFinite" |
718 by (rule approx_sym [THEN [2] approx_HFinite], auto) |
675 by (rule approx_sym [THEN [2] approx_HFinite], auto) |
719 |
676 |
720 lemma approx_mult_HFinite: "a \<approx> b \<Longrightarrow> c \<approx> d \<Longrightarrow> b \<in> HFinite \<Longrightarrow> d \<in> HFinite \<Longrightarrow> a * c \<approx> b * d" |
677 lemma approx_mult_HFinite: "a \<approx> b \<Longrightarrow> c \<approx> d \<Longrightarrow> b \<in> HFinite \<Longrightarrow> d \<in> HFinite \<Longrightarrow> a * c \<approx> b * d" |
721 for a b c d :: "'a::real_normed_algebra star" |
678 for a b c d :: "'a::real_normed_algebra star" |
722 apply (rule approx_trans) |
679 by (meson approx_HFinite approx_mult2 approx_mult_subst2 approx_sym) |
723 apply (rule_tac [2] approx_mult2) |
|
724 apply (rule approx_mult1) |
|
725 prefer 2 apply (blast intro: approx_HFinite approx_sym, auto) |
|
726 done |
|
727 |
680 |
728 lemma scaleHR_left_diff_distrib: "\<And>a b x. scaleHR (a - b) x = scaleHR a x - scaleHR b x" |
681 lemma scaleHR_left_diff_distrib: "\<And>a b x. scaleHR (a - b) x = scaleHR a x - scaleHR b x" |
729 by transfer (rule scaleR_left_diff_distrib) |
682 by transfer (rule scaleR_left_diff_distrib) |
730 |
683 |
731 lemma approx_scaleR1: "a \<approx> star_of b \<Longrightarrow> c \<in> HFinite \<Longrightarrow> scaleHR a c \<approx> b *\<^sub>R c" |
684 lemma approx_scaleR1: "a \<approx> star_of b \<Longrightarrow> c \<in> HFinite \<Longrightarrow> scaleHR a c \<approx> b *\<^sub>R c" |
732 apply (unfold approx_def) |
685 unfolding approx_def |
733 apply (drule (1) Infinitesimal_HFinite_scaleHR) |
686 by (metis Infinitesimal_HFinite_scaleHR scaleHR_def scaleHR_left_diff_distrib star_scaleR_def starfun2_star_of) |
734 apply (simp only: scaleHR_left_diff_distrib) |
|
735 apply (simp add: scaleHR_def star_scaleR_def [symmetric]) |
|
736 done |
|
737 |
687 |
738 lemma approx_scaleR2: "a \<approx> b \<Longrightarrow> c *\<^sub>R a \<approx> c *\<^sub>R b" |
688 lemma approx_scaleR2: "a \<approx> b \<Longrightarrow> c *\<^sub>R a \<approx> c *\<^sub>R b" |
739 by (simp add: approx_def Infinitesimal_scaleR2 scaleR_right_diff_distrib [symmetric]) |
689 by (simp add: approx_def Infinitesimal_scaleR2 scaleR_right_diff_distrib [symmetric]) |
740 |
690 |
741 lemma approx_scaleR_HFinite: "a \<approx> star_of b \<Longrightarrow> c \<approx> d \<Longrightarrow> d \<in> HFinite \<Longrightarrow> scaleHR a c \<approx> b *\<^sub>R d" |
691 lemma approx_scaleR_HFinite: "a \<approx> star_of b \<Longrightarrow> c \<approx> d \<Longrightarrow> d \<in> HFinite \<Longrightarrow> scaleHR a c \<approx> b *\<^sub>R d" |
742 apply (rule approx_trans) |
692 by (meson approx_HFinite approx_scaleR1 approx_scaleR2 approx_sym approx_trans) |
743 apply (rule_tac [2] approx_scaleR2) |
|
744 apply (rule approx_scaleR1) |
|
745 prefer 2 apply (blast intro: approx_HFinite approx_sym, auto) |
|
746 done |
|
747 |
693 |
748 lemma approx_mult_star_of: "a \<approx> star_of b \<Longrightarrow> c \<approx> star_of d \<Longrightarrow> a * c \<approx> star_of b * star_of d" |
694 lemma approx_mult_star_of: "a \<approx> star_of b \<Longrightarrow> c \<approx> star_of d \<Longrightarrow> a * c \<approx> star_of b * star_of d" |
749 for a c :: "'a::real_normed_algebra star" |
695 for a c :: "'a::real_normed_algebra star" |
750 by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of) |
696 by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of) |
751 |
697 |
752 lemma approx_SReal_mult_cancel_zero: "a \<in> \<real> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a * x \<approx> 0 \<Longrightarrow> x \<approx> 0" |
698 lemma approx_SReal_mult_cancel_zero: |
753 for a x :: hypreal |
699 fixes a x :: hypreal |
754 apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) |
700 assumes "a \<in> \<real>" "a \<noteq> 0" "a * x \<approx> 0" shows "x \<approx> 0" |
755 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric]) |
701 proof - |
756 done |
702 have "inverse a \<in> HFinite" |
|
703 using Reals_inverse SReal_subset_HFinite assms(1) by blast |
|
704 then show ?thesis |
|
705 using assms by (auto dest: approx_mult2 simp add: mult.assoc [symmetric]) |
|
706 qed |
757 |
707 |
758 lemma approx_mult_SReal1: "a \<in> \<real> \<Longrightarrow> x \<approx> 0 \<Longrightarrow> x * a \<approx> 0" |
708 lemma approx_mult_SReal1: "a \<in> \<real> \<Longrightarrow> x \<approx> 0 \<Longrightarrow> x * a \<approx> 0" |
759 for a x :: hypreal |
709 for a x :: hypreal |
760 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1) |
710 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1) |
761 |
711 |
765 |
715 |
766 lemma approx_mult_SReal_zero_cancel_iff [simp]: "a \<in> \<real> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a * x \<approx> 0 \<longleftrightarrow> x \<approx> 0" |
716 lemma approx_mult_SReal_zero_cancel_iff [simp]: "a \<in> \<real> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a * x \<approx> 0 \<longleftrightarrow> x \<approx> 0" |
767 for a x :: hypreal |
717 for a x :: hypreal |
768 by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2) |
718 by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2) |
769 |
719 |
770 lemma approx_SReal_mult_cancel: "a \<in> \<real> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a * w \<approx> a * z \<Longrightarrow> w \<approx> z" |
720 lemma approx_SReal_mult_cancel: |
771 for a w z :: hypreal |
721 fixes a w z :: hypreal |
772 apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) |
722 assumes "a \<in> \<real>" "a \<noteq> 0" "a * w \<approx> a * z" shows "w \<approx> z" |
773 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric]) |
723 proof - |
774 done |
724 have "inverse a \<in> HFinite" |
|
725 using Reals_inverse SReal_subset_HFinite assms(1) by blast |
|
726 then show ?thesis |
|
727 using assms by (auto dest: approx_mult2 simp add: mult.assoc [symmetric]) |
|
728 qed |
775 |
729 |
776 lemma approx_SReal_mult_cancel_iff1 [simp]: "a \<in> \<real> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a * w \<approx> a * z \<longleftrightarrow> w \<approx> z" |
730 lemma approx_SReal_mult_cancel_iff1 [simp]: "a \<in> \<real> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a * w \<approx> a * z \<longleftrightarrow> w \<approx> z" |
777 for a w z :: hypreal |
731 for a w z :: hypreal |
778 by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD] |
732 by (meson SReal_subset_HFinite approx_SReal_mult_cancel approx_mult2 subsetD) |
779 intro: approx_SReal_mult_cancel) |
733 |
780 |
734 lemma approx_le_bound: |
781 lemma approx_le_bound: "z \<le> f \<Longrightarrow> f \<approx> g \<Longrightarrow> g \<le> z ==> f \<approx> z" |
735 fixes z :: hypreal |
782 for z :: hypreal |
736 assumes "z \<le> f" " f \<approx> g" "g \<le> z" shows "f \<approx> z" |
783 apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto) |
737 proof - |
784 apply (rule_tac x = "g + y - z" in bexI) |
738 obtain y where "z \<le> g + y" and "y \<in> Infinitesimal" "f = g + y" |
785 apply simp |
739 using assms bex_Infinitesimal_iff2 by auto |
786 apply (rule Infinitesimal_interval2) |
740 then have "z - g \<in> Infinitesimal" |
787 apply (rule_tac [2] Infinitesimal_zero, auto) |
741 using assms(3) hrabs_le_Infinitesimal by auto |
788 done |
742 then show ?thesis |
|
743 by (metis approx_def approx_trans2 assms(2)) |
|
744 qed |
789 |
745 |
790 lemma approx_hnorm: "x \<approx> y \<Longrightarrow> hnorm x \<approx> hnorm y" |
746 lemma approx_hnorm: "x \<approx> y \<Longrightarrow> hnorm x \<approx> hnorm y" |
791 for x y :: "'a::real_normed_vector star" |
747 for x y :: "'a::real_normed_vector star" |
792 proof (unfold approx_def) |
748 proof (unfold approx_def) |
793 assume "x - y \<in> Infinitesimal" |
749 assume "x - y \<in> Infinitesimal" |
808 |
764 |
809 subsection \<open>Zero is the Only Infinitesimal that is also a Real\<close> |
765 subsection \<open>Zero is the Only Infinitesimal that is also a Real\<close> |
810 |
766 |
811 lemma Infinitesimal_less_SReal: "x \<in> \<real> \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> 0 < x \<Longrightarrow> y < x" |
767 lemma Infinitesimal_less_SReal: "x \<in> \<real> \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> 0 < x \<Longrightarrow> y < x" |
812 for x y :: hypreal |
768 for x y :: hypreal |
813 apply (simp add: Infinitesimal_def) |
769 using InfinitesimalD by fastforce |
814 apply (rule abs_ge_self [THEN order_le_less_trans], auto) |
|
815 done |
|
816 |
770 |
817 lemma Infinitesimal_less_SReal2: "y \<in> Infinitesimal \<Longrightarrow> \<forall>r \<in> Reals. 0 < r \<longrightarrow> y < r" |
771 lemma Infinitesimal_less_SReal2: "y \<in> Infinitesimal \<Longrightarrow> \<forall>r \<in> Reals. 0 < r \<longrightarrow> y < r" |
818 for y :: hypreal |
772 for y :: hypreal |
819 by (blast intro: Infinitesimal_less_SReal) |
773 by (blast intro: Infinitesimal_less_SReal) |
820 |
774 |
821 lemma SReal_not_Infinitesimal: "0 < y \<Longrightarrow> y \<in> \<real> ==> y \<notin> Infinitesimal" |
775 lemma SReal_not_Infinitesimal: "0 < y \<Longrightarrow> y \<in> \<real> ==> y \<notin> Infinitesimal" |
822 for y :: hypreal |
776 for y :: hypreal |
823 apply (simp add: Infinitesimal_def) |
777 by (auto simp add: Infinitesimal_def abs_if) |
824 apply (auto simp add: abs_if) |
|
825 done |
|
826 |
778 |
827 lemma SReal_minus_not_Infinitesimal: "y < 0 \<Longrightarrow> y \<in> \<real> \<Longrightarrow> y \<notin> Infinitesimal" |
779 lemma SReal_minus_not_Infinitesimal: "y < 0 \<Longrightarrow> y \<in> \<real> \<Longrightarrow> y \<notin> Infinitesimal" |
828 for y :: hypreal |
780 for y :: hypreal |
829 apply (subst Infinitesimal_minus_iff [symmetric]) |
781 using Infinitesimal_minus_iff Reals_minus SReal_not_Infinitesimal neg_0_less_iff_less by blast |
830 apply (rule SReal_not_Infinitesimal, auto) |
|
831 done |
|
832 |
782 |
833 lemma SReal_Int_Infinitesimal_zero: "\<real> Int Infinitesimal = {0::hypreal}" |
783 lemma SReal_Int_Infinitesimal_zero: "\<real> Int Infinitesimal = {0::hypreal}" |
834 apply auto |
784 proof - |
835 apply (cut_tac x = x and y = 0 in linorder_less_linear) |
785 have "x = 0" if "x \<in> \<real>" "x \<in> Infinitesimal" for x :: "real star" |
836 apply (blast dest: SReal_not_Infinitesimal SReal_minus_not_Infinitesimal) |
786 using that SReal_minus_not_Infinitesimal SReal_not_Infinitesimal not_less_iff_gr_or_eq by blast |
837 done |
787 then show ?thesis |
|
788 by auto |
|
789 qed |
838 |
790 |
839 lemma SReal_Infinitesimal_zero: "x \<in> \<real> \<Longrightarrow> x \<in> Infinitesimal \<Longrightarrow> x = 0" |
791 lemma SReal_Infinitesimal_zero: "x \<in> \<real> \<Longrightarrow> x \<in> Infinitesimal \<Longrightarrow> x = 0" |
840 for x :: hypreal |
792 for x :: hypreal |
841 using SReal_Int_Infinitesimal_zero by blast |
793 using SReal_Int_Infinitesimal_zero by blast |
842 |
794 |
864 by (fast dest: Reals_numeral [THEN SReal_Infinitesimal_zero]) |
819 by (fast dest: Reals_numeral [THEN SReal_Infinitesimal_zero]) |
865 |
820 |
866 text \<open>Again: \<open>1\<close> is a special case, but not \<open>0\<close> this time.\<close> |
821 text \<open>Again: \<open>1\<close> is a special case, but not \<open>0\<close> this time.\<close> |
867 lemma one_not_Infinitesimal [simp]: |
822 lemma one_not_Infinitesimal [simp]: |
868 "(1::'a::{real_normed_vector,zero_neq_one} star) \<notin> Infinitesimal" |
823 "(1::'a::{real_normed_vector,zero_neq_one} star) \<notin> Infinitesimal" |
869 apply (simp only: star_one_def star_of_Infinitesimal_iff_0) |
824 by (metis star_of_Infinitesimal_iff_0 star_one_def zero_neq_one) |
870 apply simp |
|
871 done |
|
872 |
825 |
873 lemma approx_SReal_not_zero: "y \<in> \<real> \<Longrightarrow> x \<approx> y \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x \<noteq> 0" |
826 lemma approx_SReal_not_zero: "y \<in> \<real> \<Longrightarrow> x \<approx> y \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x \<noteq> 0" |
874 for x y :: hypreal |
827 for x y :: hypreal |
875 apply (cut_tac x = 0 and y = y in linorder_less_linear, simp) |
828 using SReal_Infinitesimal_zero approx_sym mem_infmal_iff by auto |
876 apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] |
|
877 SReal_not_Infinitesimal SReal_minus_not_Infinitesimal) |
|
878 done |
|
879 |
829 |
880 lemma HFinite_diff_Infinitesimal_approx: |
830 lemma HFinite_diff_Infinitesimal_approx: |
881 "x \<approx> y \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> x \<in> HFinite - Infinitesimal" |
831 "x \<approx> y \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> x \<in> HFinite - Infinitesimal" |
882 apply (auto intro: approx_sym [THEN [2] approx_HFinite] simp: mem_infmal_iff) |
832 by (meson Diff_iff approx_HFinite approx_sym approx_trans3 mem_infmal_iff) |
883 apply (drule approx_trans3, assumption) |
|
884 apply (blast dest: approx_sym) |
|
885 done |
|
886 |
833 |
887 text \<open>The premise \<open>y \<noteq> 0\<close> is essential; otherwise \<open>x / y = 0\<close> and we lose the |
834 text \<open>The premise \<open>y \<noteq> 0\<close> is essential; otherwise \<open>x / y = 0\<close> and we lose the |
888 \<open>HFinite\<close> premise.\<close> |
835 \<open>HFinite\<close> premise.\<close> |
889 lemma Infinitesimal_ratio: |
836 lemma Infinitesimal_ratio: |
890 "y \<noteq> 0 \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x / y \<in> HFinite \<Longrightarrow> x \<in> Infinitesimal" |
837 "y \<noteq> 0 \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x / y \<in> HFinite \<Longrightarrow> x \<in> Infinitesimal" |
891 for x y :: "'a::{real_normed_div_algebra,field} star" |
838 for x y :: "'a::{real_normed_div_algebra,field} star" |
892 apply (drule Infinitesimal_HFinite_mult2, assumption) |
839 using Infinitesimal_HFinite_mult by fastforce |
893 apply (simp add: divide_inverse mult.assoc) |
|
894 done |
|
895 |
840 |
896 lemma Infinitesimal_SReal_divide: "x \<in> Infinitesimal \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x / y \<in> Infinitesimal" |
841 lemma Infinitesimal_SReal_divide: "x \<in> Infinitesimal \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x / y \<in> Infinitesimal" |
897 for x y :: hypreal |
842 for x y :: hypreal |
898 apply (simp add: divide_inverse) |
843 by (metis HFinite_star_of Infinitesimal_HFinite_mult Reals_inverse SReal_iff divide_inverse) |
899 apply (auto intro!: Infinitesimal_HFinite_mult |
|
900 dest!: Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) |
|
901 done |
|
902 |
844 |
903 |
845 |
904 section \<open>Standard Part Theorem\<close> |
846 section \<open>Standard Part Theorem\<close> |
905 |
847 |
906 text \<open> |
848 text \<open> |
910 |
852 |
911 |
853 |
912 subsection \<open>Uniqueness: Two Infinitely Close Reals are Equal\<close> |
854 subsection \<open>Uniqueness: Two Infinitely Close Reals are Equal\<close> |
913 |
855 |
914 lemma star_of_approx_iff [simp]: "star_of x \<approx> star_of y \<longleftrightarrow> x = y" |
856 lemma star_of_approx_iff [simp]: "star_of x \<approx> star_of y \<longleftrightarrow> x = y" |
915 apply safe |
857 by (metis approx_def right_minus_eq star_of_Infinitesimal_iff_0 star_of_simps(2)) |
916 apply (simp add: approx_def) |
|
917 apply (simp only: star_of_diff [symmetric]) |
|
918 apply (simp only: star_of_Infinitesimal_iff_0) |
|
919 apply simp |
|
920 done |
|
921 |
858 |
922 lemma SReal_approx_iff: "x \<in> \<real> \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x \<approx> y \<longleftrightarrow> x = y" |
859 lemma SReal_approx_iff: "x \<in> \<real> \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x \<approx> y \<longleftrightarrow> x = y" |
923 for x y :: hypreal |
860 for x y :: hypreal |
924 apply auto |
861 by (meson Reals_diff SReal_Infinitesimal_zero approx_def approx_refl right_minus_eq) |
925 apply (simp add: approx_def) |
|
926 apply (drule (1) Reals_diff) |
|
927 apply (drule (1) SReal_Infinitesimal_zero) |
|
928 apply simp |
|
929 done |
|
930 |
862 |
931 lemma numeral_approx_iff [simp]: |
863 lemma numeral_approx_iff [simp]: |
932 "(numeral v \<approx> (numeral w :: 'a::{numeral,real_normed_vector} star)) = |
864 "(numeral v \<approx> (numeral w :: 'a::{numeral,real_normed_vector} star)) = (numeral v = (numeral w :: 'a))" |
933 (numeral v = (numeral w :: 'a))" |
865 by (metis star_of_approx_iff star_of_numeral) |
934 apply (unfold star_numeral_def) |
|
935 apply (rule star_of_approx_iff) |
|
936 done |
|
937 |
866 |
938 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> |
867 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> |
939 lemma [simp]: |
868 lemma [simp]: |
940 "(numeral w \<approx> (0::'a::{numeral,real_normed_vector} star)) = (numeral w = (0::'a))" |
869 "(numeral w \<approx> (0::'a::{numeral,real_normed_vector} star)) = (numeral w = (0::'a))" |
941 "((0::'a::{numeral,real_normed_vector} star) \<approx> numeral w) = (numeral w = (0::'a))" |
870 "((0::'a::{numeral,real_normed_vector} star) \<approx> numeral w) = (numeral w = (0::'a))" |
942 "(numeral w \<approx> (1::'b::{numeral,one,real_normed_vector} star)) = (numeral w = (1::'b))" |
871 "(numeral w \<approx> (1::'b::{numeral,one,real_normed_vector} star)) = (numeral w = (1::'b))" |
943 "((1::'b::{numeral,one,real_normed_vector} star) \<approx> numeral w) = (numeral w = (1::'b))" |
872 "((1::'b::{numeral,one,real_normed_vector} star) \<approx> numeral w) = (numeral w = (1::'b))" |
944 "\<not> (0 \<approx> (1::'c::{zero_neq_one,real_normed_vector} star))" |
873 "\<not> (0 \<approx> (1::'c::{zero_neq_one,real_normed_vector} star))" |
945 "\<not> (1 \<approx> (0::'c::{zero_neq_one,real_normed_vector} star))" |
874 "\<not> (1 \<approx> (0::'c::{zero_neq_one,real_normed_vector} star))" |
946 apply (unfold star_numeral_def star_zero_def star_one_def) |
875 unfolding star_numeral_def star_zero_def star_one_def star_of_approx_iff |
947 apply (unfold star_of_approx_iff) |
876 by (auto intro: sym) |
948 apply (auto intro: sym) |
|
949 done |
|
950 |
877 |
951 lemma star_of_approx_numeral_iff [simp]: "star_of k \<approx> numeral w \<longleftrightarrow> k = numeral w" |
878 lemma star_of_approx_numeral_iff [simp]: "star_of k \<approx> numeral w \<longleftrightarrow> k = numeral w" |
952 by (subst star_of_approx_iff [symmetric]) auto |
879 by (subst star_of_approx_iff [symmetric]) auto |
953 |
880 |
954 lemma star_of_approx_zero_iff [simp]: "star_of k \<approx> 0 \<longleftrightarrow> k = 0" |
881 lemma star_of_approx_zero_iff [simp]: "star_of k \<approx> 0 \<longleftrightarrow> k = 0" |
968 |
895 |
969 lemma hypreal_of_real_isUb_iff: "isUb \<real> (hypreal_of_real ` Q) (hypreal_of_real Y) = isUb UNIV Q Y" |
896 lemma hypreal_of_real_isUb_iff: "isUb \<real> (hypreal_of_real ` Q) (hypreal_of_real Y) = isUb UNIV Q Y" |
970 for Q :: "real set" and Y :: real |
897 for Q :: "real set" and Y :: real |
971 by (simp add: isUb_def setle_def) |
898 by (simp add: isUb_def setle_def) |
972 |
899 |
973 lemma hypreal_of_real_isLub1: "isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y) \<Longrightarrow> isLub UNIV Q Y" |
900 lemma hypreal_of_real_isLub_iff: |
|
901 "isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y) = isLub (UNIV :: real set) Q Y" (is "?lhs = ?rhs") |
974 for Q :: "real set" and Y :: real |
902 for Q :: "real set" and Y :: real |
975 apply (simp add: isLub_def leastP_def) |
903 proof |
976 apply (auto intro: hypreal_of_real_isUb_iff [THEN iffD2] |
904 assume ?lhs |
977 simp add: hypreal_of_real_isUb_iff setge_def) |
905 then show ?rhs |
978 done |
906 by (simp add: isLub_def leastP_def) (metis hypreal_of_real_isUb_iff mem_Collect_eq setge_def star_of_le) |
979 |
907 next |
980 lemma hypreal_of_real_isLub2: "isLub UNIV Q Y \<Longrightarrow> isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)" |
908 assume ?rhs |
981 for Q :: "real set" and Y :: real |
909 then show ?lhs |
982 apply (auto simp add: isLub_def leastP_def hypreal_of_real_isUb_iff setge_def) |
910 apply (simp add: isLub_def leastP_def hypreal_of_real_isUb_iff setge_def) |
983 apply (metis SReal_iff hypreal_of_real_isUb_iff isUbD2a star_of_le) |
911 by (metis SReal_iff hypreal_of_real_isUb_iff isUb_def star_of_le) |
984 done |
912 qed |
985 |
|
986 lemma hypreal_of_real_isLub_iff: |
|
987 "isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y) = isLub (UNIV :: real set) Q Y" |
|
988 for Q :: "real set" and Y :: real |
|
989 by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2) |
|
990 |
913 |
991 lemma lemma_isUb_hypreal_of_real: "isUb \<real> P Y \<Longrightarrow> \<exists>Yo. isUb \<real> P (hypreal_of_real Yo)" |
914 lemma lemma_isUb_hypreal_of_real: "isUb \<real> P Y \<Longrightarrow> \<exists>Yo. isUb \<real> P (hypreal_of_real Yo)" |
992 by (auto simp add: SReal_iff isUb_def) |
915 by (auto simp add: SReal_iff isUb_def) |
993 |
916 |
994 lemma lemma_isLub_hypreal_of_real: "isLub \<real> P Y \<Longrightarrow> \<exists>Yo. isLub \<real> P (hypreal_of_real Yo)" |
917 lemma lemma_isLub_hypreal_of_real: "isLub \<real> P Y \<Longrightarrow> \<exists>Yo. isLub \<real> P (hypreal_of_real Yo)" |
995 by (auto simp add: isLub_def leastP_def isUb_def SReal_iff) |
918 by (auto simp add: isLub_def leastP_def isUb_def SReal_iff) |
996 |
919 |
997 lemma lemma_isLub_hypreal_of_real2: "\<exists>Yo. isLub \<real> P (hypreal_of_real Yo) \<Longrightarrow> \<exists>Y. isLub \<real> P Y" |
920 lemma SReal_complete: |
998 by (auto simp add: isLub_def leastP_def isUb_def) |
921 fixes P :: "hypreal set" |
999 |
922 assumes "isUb \<real> P Y" "P \<subseteq> \<real>" "P \<noteq> {}" |
1000 lemma SReal_complete: "P \<subseteq> \<real> \<Longrightarrow> \<exists>x. x \<in> P \<Longrightarrow> \<exists>Y. isUb \<real> P Y \<Longrightarrow> \<exists>t::hypreal. isLub \<real> P t" |
923 shows "\<exists>t. isLub \<real> P t" |
1001 apply (frule SReal_hypreal_of_real_image) |
924 proof - |
1002 apply (auto, drule lemma_isUb_hypreal_of_real) |
925 obtain Q where "P = hypreal_of_real ` Q" |
1003 apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2 |
926 by (metis \<open>P \<subseteq> \<real>\<close> hypreal_of_real_image subset_imageE) |
1004 simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff) |
927 then show ?thesis |
1005 done |
928 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) |
|
929 qed |
1006 |
930 |
1007 |
931 |
1008 text \<open>Lemmas about lubs.\<close> |
932 text \<open>Lemmas about lubs.\<close> |
1009 |
933 |
1010 lemma lemma_st_part_ub: "x \<in> HFinite \<Longrightarrow> \<exists>u. isUb \<real> {s. s \<in> \<real> \<and> s < x} u" |
934 lemma lemma_st_part_lub: |
1011 for x :: hypreal |
935 fixes x :: hypreal |
1012 apply (drule HFiniteD, safe) |
936 assumes "x \<in> HFinite" |
1013 apply (rule exI, rule isUbI) |
937 shows "\<exists>t. isLub \<real> {s. s \<in> \<real> \<and> s < x} t" |
1014 apply (auto intro: setleI isUbI simp add: abs_less_iff) |
938 proof - |
1015 done |
939 obtain t where t: "t \<in> \<real>" "hnorm x < t" |
1016 |
940 using HFiniteD assms by blast |
1017 lemma lemma_st_part_nonempty: "x \<in> HFinite \<Longrightarrow> \<exists>y. y \<in> {s. s \<in> \<real> \<and> s < x}" |
941 then have "isUb \<real> {s. s \<in> \<real> \<and> s < x} t" |
1018 for x :: hypreal |
942 by (simp add: abs_less_iff isUbI le_less_linear less_imp_not_less setleI) |
1019 apply (drule HFiniteD, safe) |
943 moreover have "\<exists>y. y \<in> \<real> \<and> y < x" |
1020 apply (drule Reals_minus) |
944 using t by (rule_tac x = "-t" in exI) (auto simp add: abs_less_iff) |
1021 apply (rule_tac x = "-t" in exI) |
945 ultimately show ?thesis |
1022 apply (auto simp add: abs_less_iff) |
946 using SReal_complete by fastforce |
1023 done |
947 qed |
1024 |
|
1025 lemma lemma_st_part_lub: "x \<in> HFinite \<Longrightarrow> \<exists>t. isLub \<real> {s. s \<in> \<real> \<and> s < x} t" |
|
1026 for x :: hypreal |
|
1027 by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty Collect_restrict) |
|
1028 |
948 |
1029 lemma lemma_st_part_le1: |
949 lemma lemma_st_part_le1: |
1030 "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" |
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" |
1031 for x r t :: hypreal |
951 for x r t :: hypreal |
1032 apply (frule isLubD1a) |
952 by (metis (no_types, lifting) Reals_add add.commute isLubD1a isLubD2 less_add_same_cancel2 mem_Collect_eq not_le) |
1033 apply (rule ccontr, drule linorder_not_le [THEN iffD2]) |
|
1034 apply (drule (1) Reals_add) |
|
1035 apply (drule_tac y = "r + t" in isLubD1 [THEN setleD], auto) |
|
1036 done |
|
1037 |
953 |
1038 lemma hypreal_setle_less_trans: "S *<= x \<Longrightarrow> x < y \<Longrightarrow> S *<= y" |
954 lemma hypreal_setle_less_trans: "S *<= x \<Longrightarrow> x < y \<Longrightarrow> S *<= y" |
1039 for x y :: hypreal |
955 for x y :: hypreal |
1040 apply (simp add: setle_def) |
956 by (meson le_less_trans less_imp_le setle_def) |
1041 apply (auto dest!: bspec order_le_less_trans intro: order_less_imp_le) |
|
1042 done |
|
1043 |
957 |
1044 lemma hypreal_gt_isUb: "isUb R S x \<Longrightarrow> x < y \<Longrightarrow> y \<in> R \<Longrightarrow> isUb R S y" |
958 lemma hypreal_gt_isUb: "isUb R S x \<Longrightarrow> x < y \<Longrightarrow> y \<in> R \<Longrightarrow> isUb R S y" |
1045 for x y :: hypreal |
959 for x y :: hypreal |
1046 apply (simp add: isUb_def) |
960 using hypreal_setle_less_trans isUb_def by blast |
1047 apply (blast intro: hypreal_setle_less_trans) |
|
1048 done |
|
1049 |
961 |
1050 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" |
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" |
1051 for x y :: hypreal |
963 for x y :: hypreal |
1052 by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI) |
964 by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI) |
1053 |
965 |
1054 lemma lemma_minus_le_zero: "t \<le> t + -r \<Longrightarrow> r \<le> 0" |
966 lemma lemma_minus_le_zero: "t \<le> t + -r \<Longrightarrow> r \<le> 0" |
1055 for r t :: hypreal |
967 for r t :: hypreal |
1056 apply (drule_tac c = "-t" in add_left_mono) |
968 by simp |
1057 apply (auto simp add: add.assoc [symmetric]) |
|
1058 done |
|
1059 |
969 |
1060 lemma lemma_st_part_le2: |
970 lemma lemma_st_part_le2: |
1061 "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" |
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" |
1062 for x r t :: hypreal |
972 for x r t :: hypreal |
1063 apply (frule isLubD1a) |
973 apply (frule isLubD1a) |
1139 |
1047 |
1140 text\<open>Existence of real and Standard Part Theorem.\<close> |
1048 text\<open>Existence of real and Standard Part Theorem.\<close> |
1141 |
1049 |
1142 lemma lemma_st_part_Ex: "x \<in> HFinite \<Longrightarrow> \<exists>t\<in>Reals. \<forall>r \<in> Reals. 0 < r \<longrightarrow> \<bar>x - t\<bar> < r" |
1050 lemma lemma_st_part_Ex: "x \<in> HFinite \<Longrightarrow> \<exists>t\<in>Reals. \<forall>r \<in> Reals. 0 < r \<longrightarrow> \<bar>x - t\<bar> < r" |
1143 for x :: hypreal |
1051 for x :: hypreal |
1144 apply (frule lemma_st_part_lub, safe) |
1052 by (meson isLubD1a lemma_st_part_lub lemma_st_part_major2) |
1145 apply (frule isLubD1a) |
|
1146 apply (blast dest: lemma_st_part_major2) |
|
1147 done |
|
1148 |
1053 |
1149 lemma st_part_Ex: "x \<in> HFinite \<Longrightarrow> \<exists>t\<in>Reals. x \<approx> t" |
1054 lemma st_part_Ex: "x \<in> HFinite \<Longrightarrow> \<exists>t\<in>Reals. x \<approx> t" |
1150 for x :: hypreal |
1055 for x :: hypreal |
1151 apply (simp add: approx_def Infinitesimal_def) |
1056 by (metis InfinitesimalI approx_def hypreal_hnorm_def lemma_st_part_Ex) |
1152 apply (drule lemma_st_part_Ex, auto) |
|
1153 done |
|
1154 |
1057 |
1155 text \<open>There is a unique real infinitely close.\<close> |
1058 text \<open>There is a unique real infinitely close.\<close> |
1156 lemma st_part_Ex1: "x \<in> HFinite \<Longrightarrow> \<exists>!t::hypreal. t \<in> \<real> \<and> x \<approx> t" |
1059 lemma st_part_Ex1: "x \<in> HFinite \<Longrightarrow> \<exists>!t::hypreal. t \<in> \<real> \<and> x \<approx> t" |
1157 apply (drule st_part_Ex, safe) |
1060 by (meson SReal_approx_iff approx_trans2 st_part_Ex) |
1158 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) |
|
1159 apply (auto intro!: approx_unique_real) |
|
1160 done |
|
1161 |
1061 |
1162 |
1062 |
1163 subsection \<open>Finite, Infinite and Infinitesimal\<close> |
1063 subsection \<open>Finite, Infinite and Infinitesimal\<close> |
1164 |
1064 |
1165 lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}" |
1065 lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}" |
1166 apply (simp add: HFinite_def HInfinite_def) |
1066 using Compl_HFinite by blast |
1167 apply (auto dest: order_less_trans) |
|
1168 done |
|
1169 |
1067 |
1170 lemma HFinite_not_HInfinite: |
1068 lemma HFinite_not_HInfinite: |
1171 assumes x: "x \<in> HFinite" |
1069 assumes x: "x \<in> HFinite" shows "x \<notin> HInfinite" |
1172 shows "x \<notin> HInfinite" |
1070 using Compl_HFinite x by blast |
1173 proof |
|
1174 assume x': "x \<in> HInfinite" |
|
1175 with x have "x \<in> HFinite \<inter> HInfinite" by blast |
|
1176 then show False by auto |
|
1177 qed |
|
1178 |
1071 |
1179 lemma not_HFinite_HInfinite: "x \<notin> HFinite \<Longrightarrow> x \<in> HInfinite" |
1072 lemma not_HFinite_HInfinite: "x \<notin> HFinite \<Longrightarrow> x \<in> HInfinite" |
1180 apply (simp add: HInfinite_def HFinite_def, auto) |
1073 using Compl_HFinite by blast |
1181 apply (drule_tac x = "r + 1" in bspec) |
|
1182 apply (auto) |
|
1183 done |
|
1184 |
1074 |
1185 lemma HInfinite_HFinite_disj: "x \<in> HInfinite \<or> x \<in> HFinite" |
1075 lemma HInfinite_HFinite_disj: "x \<in> HInfinite \<or> x \<in> HFinite" |
1186 by (blast intro: not_HFinite_HInfinite) |
1076 by (blast intro: not_HFinite_HInfinite) |
1187 |
1077 |
1188 lemma HInfinite_HFinite_iff: "x \<in> HInfinite \<longleftrightarrow> x \<notin> HFinite" |
1078 lemma HInfinite_HFinite_iff: "x \<in> HInfinite \<longleftrightarrow> x \<notin> HFinite" |
1189 by (blast dest: HFinite_not_HInfinite not_HFinite_HInfinite) |
1079 by (blast dest: HFinite_not_HInfinite not_HFinite_HInfinite) |
1190 |
1080 |
1191 lemma HFinite_HInfinite_iff: "x \<in> HFinite \<longleftrightarrow> x \<notin> HInfinite" |
1081 lemma HFinite_HInfinite_iff: "x \<in> HFinite \<longleftrightarrow> x \<notin> HInfinite" |
1192 by (simp add: HInfinite_HFinite_iff) |
1082 by (simp add: HInfinite_HFinite_iff) |
1193 |
|
1194 |
1083 |
1195 lemma HInfinite_diff_HFinite_Infinitesimal_disj: |
1084 lemma HInfinite_diff_HFinite_Infinitesimal_disj: |
1196 "x \<notin> Infinitesimal \<Longrightarrow> x \<in> HInfinite \<or> x \<in> HFinite - Infinitesimal" |
1085 "x \<notin> Infinitesimal \<Longrightarrow> x \<in> HInfinite \<or> x \<in> HFinite - Infinitesimal" |
1197 by (fast intro: not_HFinite_HInfinite) |
1086 by (fast intro: not_HFinite_HInfinite) |
1198 |
1087 |
1199 lemma HFinite_inverse: "x \<in> HFinite \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> inverse x \<in> HFinite" |
1088 lemma HFinite_inverse: "x \<in> HFinite \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> inverse x \<in> HFinite" |
1200 for x :: "'a::real_normed_div_algebra star" |
1089 for x :: "'a::real_normed_div_algebra star" |
1201 apply (subgoal_tac "x \<noteq> 0") |
1090 using HInfinite_inverse_Infinitesimal not_HFinite_HInfinite by force |
1202 apply (cut_tac x = "inverse x" in HInfinite_HFinite_disj) |
|
1203 apply (auto dest!: HInfinite_inverse_Infinitesimal simp: nonzero_inverse_inverse_eq) |
|
1204 done |
|
1205 |
1091 |
1206 lemma HFinite_inverse2: "x \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<in> HFinite" |
1092 lemma HFinite_inverse2: "x \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<in> HFinite" |
1207 for x :: "'a::real_normed_div_algebra star" |
1093 for x :: "'a::real_normed_div_algebra star" |
1208 by (blast intro: HFinite_inverse) |
1094 by (blast intro: HFinite_inverse) |
1209 |
1095 |
1210 text \<open>Stronger statement possible in fact.\<close> |
1096 text \<open>Stronger statement possible in fact.\<close> |
1211 lemma Infinitesimal_inverse_HFinite: "x \<notin> Infinitesimal \<Longrightarrow> inverse x \<in> HFinite" |
1097 lemma Infinitesimal_inverse_HFinite: "x \<notin> Infinitesimal \<Longrightarrow> inverse x \<in> HFinite" |
1212 for x :: "'a::real_normed_div_algebra star" |
1098 for x :: "'a::real_normed_div_algebra star" |
1213 apply (drule HInfinite_diff_HFinite_Infinitesimal_disj) |
1099 using HFinite_HInfinite_iff HInfinite_inverse_Infinitesimal by fastforce |
1214 apply (blast intro: HFinite_inverse HInfinite_inverse_Infinitesimal Infinitesimal_subset_HFinite [THEN subsetD]) |
|
1215 done |
|
1216 |
1100 |
1217 lemma HFinite_not_Infinitesimal_inverse: |
1101 lemma HFinite_not_Infinitesimal_inverse: |
1218 "x \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<in> HFinite - Infinitesimal" |
1102 "x \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<in> HFinite - Infinitesimal" |
1219 for x :: "'a::real_normed_div_algebra star" |
1103 for x :: "'a::real_normed_div_algebra star" |
1220 apply (auto intro: Infinitesimal_inverse_HFinite) |
1104 using HFinite_Infinitesimal_not_zero HFinite_inverse2 Infinitesimal_HFinite_mult2 by fastforce |
1221 apply (drule Infinitesimal_HFinite_mult2, assumption) |
|
1222 apply (simp add: not_Infinitesimal_not_zero) |
|
1223 done |
|
1224 |
1105 |
1225 lemma approx_inverse: "x \<approx> y \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<approx> inverse y" |
1106 lemma approx_inverse: "x \<approx> y \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<approx> inverse y" |
1226 for x y :: "'a::real_normed_div_algebra star" |
1107 for x y :: "'a::real_normed_div_algebra star" |
1227 apply (frule HFinite_diff_Infinitesimal_approx, assumption) |
1108 apply (frule HFinite_diff_Infinitesimal_approx, assumption) |
1228 apply (frule not_Infinitesimal_not_zero2) |
1109 apply (frule not_Infinitesimal_not_zero2) |
1243 by (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self) |
1124 by (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self) |
1244 |
1125 |
1245 lemma inverse_add_Infinitesimal_approx2: |
1126 lemma inverse_add_Infinitesimal_approx2: |
1246 "x \<in> HFinite - Infinitesimal \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> inverse (h + x) \<approx> inverse x" |
1127 "x \<in> HFinite - Infinitesimal \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> inverse (h + x) \<approx> inverse x" |
1247 for x h :: "'a::real_normed_div_algebra star" |
1128 for x h :: "'a::real_normed_div_algebra star" |
1248 apply (rule add.commute [THEN subst]) |
1129 by (metis add.commute inverse_add_Infinitesimal_approx) |
1249 apply (blast intro: inverse_add_Infinitesimal_approx) |
|
1250 done |
|
1251 |
1130 |
1252 lemma inverse_add_Infinitesimal_approx_Infinitesimal: |
1131 lemma inverse_add_Infinitesimal_approx_Infinitesimal: |
1253 "x \<in> HFinite - Infinitesimal \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> inverse (x + h) - inverse x \<approx> h" |
1132 "x \<in> HFinite - Infinitesimal \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> inverse (x + h) - inverse x \<approx> h" |
1254 for x h :: "'a::real_normed_div_algebra star" |
1133 for x h :: "'a::real_normed_div_algebra star" |
1255 apply (rule approx_trans2) |
1134 by (meson Infinitesimal_approx bex_Infinitesimal_iff inverse_add_Infinitesimal_approx) |
1256 apply (auto intro: inverse_add_Infinitesimal_approx |
|
1257 simp add: mem_infmal_iff approx_minus_iff [symmetric]) |
|
1258 done |
|
1259 |
1135 |
1260 lemma Infinitesimal_square_iff: "x \<in> Infinitesimal \<longleftrightarrow> x * x \<in> Infinitesimal" |
1136 lemma Infinitesimal_square_iff: "x \<in> Infinitesimal \<longleftrightarrow> x * x \<in> Infinitesimal" |
1261 for x :: "'a::real_normed_div_algebra star" |
1137 for x :: "'a::real_normed_div_algebra star" |
1262 apply (auto intro: Infinitesimal_mult) |
1138 using Infinitesimal_mult Infinitesimal_mult_disj by auto |
1263 apply (rule ccontr, frule Infinitesimal_inverse_HFinite) |
|
1264 apply (frule not_Infinitesimal_not_zero) |
|
1265 apply (auto dest: Infinitesimal_HFinite_mult simp add: mult.assoc) |
|
1266 done |
|
1267 declare Infinitesimal_square_iff [symmetric, simp] |
1139 declare Infinitesimal_square_iff [symmetric, simp] |
1268 |
1140 |
1269 lemma HFinite_square_iff [simp]: "x * x \<in> HFinite \<longleftrightarrow> x \<in> HFinite" |
1141 lemma HFinite_square_iff [simp]: "x * x \<in> HFinite \<longleftrightarrow> x \<in> HFinite" |
1270 for x :: "'a::real_normed_div_algebra star" |
1142 for x :: "'a::real_normed_div_algebra star" |
1271 apply (auto intro: HFinite_mult) |
1143 using HFinite_HInfinite_iff HFinite_mult HInfinite_mult by blast |
1272 apply (auto dest: HInfinite_mult simp add: HFinite_HInfinite_iff) |
|
1273 done |
|
1274 |
1144 |
1275 lemma HInfinite_square_iff [simp]: "x * x \<in> HInfinite \<longleftrightarrow> x \<in> HInfinite" |
1145 lemma HInfinite_square_iff [simp]: "x * x \<in> HInfinite \<longleftrightarrow> x \<in> HInfinite" |
1276 for x :: "'a::real_normed_div_algebra star" |
1146 for x :: "'a::real_normed_div_algebra star" |
1277 by (auto simp add: HInfinite_HFinite_iff) |
1147 by (auto simp add: HInfinite_HFinite_iff) |
1278 |
1148 |
1279 lemma approx_HFinite_mult_cancel: "a \<in> HFinite - Infinitesimal \<Longrightarrow> a * w \<approx> a * z \<Longrightarrow> w \<approx> z" |
1149 lemma approx_HFinite_mult_cancel: "a \<in> HFinite - Infinitesimal \<Longrightarrow> a * w \<approx> a * z \<Longrightarrow> w \<approx> z" |
1280 for a w z :: "'a::real_normed_div_algebra star" |
1150 for a w z :: "'a::real_normed_div_algebra star" |
1281 apply safe |
1151 by (metis DiffD2 Infinitesimal_mult_disj bex_Infinitesimal_iff right_diff_distrib) |
1282 apply (frule HFinite_inverse, assumption) |
|
1283 apply (drule not_Infinitesimal_not_zero) |
|
1284 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric]) |
|
1285 done |
|
1286 |
1152 |
1287 lemma approx_HFinite_mult_cancel_iff1: "a \<in> HFinite - Infinitesimal \<Longrightarrow> a * w \<approx> a * z \<longleftrightarrow> w \<approx> z" |
1153 lemma approx_HFinite_mult_cancel_iff1: "a \<in> HFinite - Infinitesimal \<Longrightarrow> a * w \<approx> a * z \<longleftrightarrow> w \<approx> z" |
1288 for a w z :: "'a::real_normed_div_algebra star" |
1154 for a w z :: "'a::real_normed_div_algebra star" |
1289 by (auto intro: approx_mult2 approx_HFinite_mult_cancel) |
1155 by (auto intro: approx_mult2 approx_HFinite_mult_cancel) |
1290 |
1156 |
1291 lemma HInfinite_HFinite_add_cancel: "x + y \<in> HInfinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x \<in> HInfinite" |
1157 lemma HInfinite_HFinite_add_cancel: "x + y \<in> HInfinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x \<in> HInfinite" |
1292 apply (rule ccontr) |
1158 using HFinite_add HInfinite_HFinite_iff by blast |
1293 apply (drule HFinite_HInfinite_iff [THEN iffD2]) |
|
1294 apply (auto dest: HFinite_add simp add: HInfinite_HFinite_iff) |
|
1295 done |
|
1296 |
1159 |
1297 lemma HInfinite_HFinite_add: "x \<in> HInfinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x + y \<in> HInfinite" |
1160 lemma HInfinite_HFinite_add: "x \<in> HInfinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x + y \<in> HInfinite" |
1298 apply (rule_tac y = "-y" in HInfinite_HFinite_add_cancel) |
1161 by (metis (no_types, hide_lams) HFinite_HInfinite_iff HFinite_add HFinite_minus_iff add.commute add_minus_cancel) |
1299 apply (auto simp add: add.assoc HFinite_minus_iff) |
|
1300 done |
|
1301 |
1162 |
1302 lemma HInfinite_ge_HInfinite: "x \<in> HInfinite \<Longrightarrow> x \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> y \<in> HInfinite" |
1163 lemma HInfinite_ge_HInfinite: "x \<in> HInfinite \<Longrightarrow> x \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> y \<in> HInfinite" |
1303 for x y :: hypreal |
1164 for x y :: hypreal |
1304 by (auto intro: HFinite_bounded simp add: HInfinite_HFinite_iff) |
1165 by (auto intro: HFinite_bounded simp add: HInfinite_HFinite_iff) |
1305 |
1166 |
1306 lemma Infinitesimal_inverse_HInfinite: "x \<in> Infinitesimal \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> inverse x \<in> HInfinite" |
1167 lemma Infinitesimal_inverse_HInfinite: "x \<in> Infinitesimal \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> inverse x \<in> HInfinite" |
1307 for x :: "'a::real_normed_div_algebra star" |
1168 for x :: "'a::real_normed_div_algebra star" |
1308 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2]) |
1169 by (metis Infinitesimal_HFinite_mult not_HFinite_HInfinite one_not_Infinitesimal right_inverse) |
1309 apply (auto dest: Infinitesimal_HFinite_mult2) |
|
1310 done |
|
1311 |
1170 |
1312 lemma HInfinite_HFinite_not_Infinitesimal_mult: |
1171 lemma HInfinite_HFinite_not_Infinitesimal_mult: |
1313 "x \<in> HInfinite \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> x * y \<in> HInfinite" |
1172 "x \<in> HInfinite \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> x * y \<in> HInfinite" |
1314 for x y :: "'a::real_normed_div_algebra star" |
1173 for x y :: "'a::real_normed_div_algebra star" |
1315 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2]) |
1174 by (metis (no_types, hide_lams) HFinite_HInfinite_iff HFinite_Infinitesimal_not_zero HFinite_inverse2 HFinite_mult mult.assoc mult.right_neutral right_inverse) |
1316 apply (frule HFinite_Infinitesimal_not_zero) |
|
1317 apply (drule HFinite_not_Infinitesimal_inverse) |
|
1318 apply (safe, drule HFinite_mult) |
|
1319 apply (auto simp add: mult.assoc HFinite_HInfinite_iff) |
|
1320 done |
|
1321 |
1175 |
1322 lemma HInfinite_HFinite_not_Infinitesimal_mult2: |
1176 lemma HInfinite_HFinite_not_Infinitesimal_mult2: |
1323 "x \<in> HInfinite \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> y * x \<in> HInfinite" |
1177 "x \<in> HInfinite \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> y * x \<in> HInfinite" |
1324 for x y :: "'a::real_normed_div_algebra star" |
1178 for x y :: "'a::real_normed_div_algebra star" |
1325 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2]) |
1179 by (metis Diff_iff HInfinite_HFinite_iff HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 divide_inverse mult_zero_right nonzero_eq_divide_eq) |
1326 apply (frule HFinite_Infinitesimal_not_zero) |
|
1327 apply (drule HFinite_not_Infinitesimal_inverse) |
|
1328 apply (safe, drule_tac x="inverse y" in HFinite_mult) |
|
1329 apply assumption |
|
1330 apply (auto simp add: mult.assoc [symmetric] HFinite_HInfinite_iff) |
|
1331 done |
|
1332 |
1180 |
1333 lemma HInfinite_gt_SReal: "x \<in> HInfinite \<Longrightarrow> 0 < x \<Longrightarrow> y \<in> \<real> \<Longrightarrow> y < x" |
1181 lemma HInfinite_gt_SReal: "x \<in> HInfinite \<Longrightarrow> 0 < x \<Longrightarrow> y \<in> \<real> \<Longrightarrow> y < x" |
1334 for x y :: hypreal |
1182 for x y :: hypreal |
1335 by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le) |
1183 by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le) |
1336 |
1184 |
1337 lemma HInfinite_gt_zero_gt_one: "x \<in> HInfinite \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x" |
1185 lemma HInfinite_gt_zero_gt_one: "x \<in> HInfinite \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x" |
1338 for x :: hypreal |
1186 for x :: hypreal |
1339 by (auto intro: HInfinite_gt_SReal) |
1187 by (auto intro: HInfinite_gt_SReal) |
1340 |
|
1341 |
1188 |
1342 lemma not_HInfinite_one [simp]: "1 \<notin> HInfinite" |
1189 lemma not_HInfinite_one [simp]: "1 \<notin> HInfinite" |
1343 by (simp add: HInfinite_HFinite_iff) |
1190 by (simp add: HInfinite_HFinite_iff) |
1344 |
1191 |
1345 lemma approx_hrabs_disj: "\<bar>x\<bar> \<approx> x \<or> \<bar>x\<bar> \<approx> -x" |
1192 lemma approx_hrabs_disj: "\<bar>x\<bar> \<approx> x \<or> \<bar>x\<bar> \<approx> -x" |
1377 |
1224 |
1378 lemma approx_subset_monad: "x \<approx> y \<Longrightarrow> {x, y} \<le> monad x" |
1225 lemma approx_subset_monad: "x \<approx> y \<Longrightarrow> {x, y} \<le> monad x" |
1379 by (simp (no_asm)) (simp add: approx_monad_iff) |
1226 by (simp (no_asm)) (simp add: approx_monad_iff) |
1380 |
1227 |
1381 lemma approx_subset_monad2: "x \<approx> y \<Longrightarrow> {x, y} \<le> monad y" |
1228 lemma approx_subset_monad2: "x \<approx> y \<Longrightarrow> {x, y} \<le> monad y" |
1382 apply (drule approx_sym) |
1229 using approx_subset_monad approx_sym by auto |
1383 apply (fast dest: approx_subset_monad) |
|
1384 done |
|
1385 |
1230 |
1386 lemma mem_monad_approx: "u \<in> monad x \<Longrightarrow> x \<approx> u" |
1231 lemma mem_monad_approx: "u \<in> monad x \<Longrightarrow> x \<approx> u" |
1387 by (simp add: monad_def) |
1232 by (simp add: monad_def) |
1388 |
1233 |
1389 lemma approx_mem_monad: "x \<approx> u \<Longrightarrow> u \<in> monad x" |
1234 lemma approx_mem_monad: "x \<approx> u \<Longrightarrow> u \<in> monad x" |
1390 by (simp add: monad_def) |
1235 by (simp add: monad_def) |
1391 |
1236 |
1392 lemma approx_mem_monad2: "x \<approx> u \<Longrightarrow> x \<in> monad u" |
1237 lemma approx_mem_monad2: "x \<approx> u \<Longrightarrow> x \<in> monad u" |
1393 apply (simp add: monad_def) |
1238 using approx_mem_monad approx_sym by blast |
1394 apply (blast intro!: approx_sym) |
|
1395 done |
|
1396 |
1239 |
1397 lemma approx_mem_monad_zero: "x \<approx> y \<Longrightarrow> x \<in> monad 0 \<Longrightarrow> y \<in> monad 0" |
1240 lemma approx_mem_monad_zero: "x \<approx> y \<Longrightarrow> x \<in> monad 0 \<Longrightarrow> y \<in> monad 0" |
1398 apply (drule mem_monad_approx) |
1241 using approx_trans monad_def by blast |
1399 apply (fast intro: approx_mem_monad approx_trans) |
|
1400 done |
|
1401 |
1242 |
1402 lemma Infinitesimal_approx_hrabs: "x \<approx> y \<Longrightarrow> x \<in> Infinitesimal \<Longrightarrow> \<bar>x\<bar> \<approx> \<bar>y\<bar>" |
1243 lemma Infinitesimal_approx_hrabs: "x \<approx> y \<Longrightarrow> x \<in> Infinitesimal \<Longrightarrow> \<bar>x\<bar> \<approx> \<bar>y\<bar>" |
1403 for x y :: hypreal |
1244 for x y :: hypreal |
1404 apply (drule Infinitesimal_monad_zero_iff [THEN iffD1]) |
1245 using approx_hnorm by fastforce |
1405 apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] |
|
1406 mem_monad_approx approx_trans3) |
|
1407 done |
|
1408 |
1246 |
1409 lemma less_Infinitesimal_less: "0 < x \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> e < x" |
1247 lemma less_Infinitesimal_less: "0 < x \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> e < x" |
1410 for x :: hypreal |
1248 for x :: hypreal |
1411 apply (rule ccontr) |
1249 using Infinitesimal_interval less_linear by blast |
1412 apply (auto intro: Infinitesimal_zero [THEN [2] Infinitesimal_interval] |
|
1413 dest!: order_le_imp_less_or_eq simp add: linorder_not_less) |
|
1414 done |
|
1415 |
1250 |
1416 lemma Ball_mem_monad_gt_zero: "0 < x \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> u \<in> monad x \<Longrightarrow> 0 < u" |
1251 lemma Ball_mem_monad_gt_zero: "0 < x \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> u \<in> monad x \<Longrightarrow> 0 < u" |
1417 for u x :: hypreal |
1252 for u x :: hypreal |
1418 apply (drule mem_monad_approx [THEN approx_sym]) |
1253 apply (drule mem_monad_approx [THEN approx_sym]) |
1419 apply (erule bex_Infinitesimal_iff2 [THEN iffD2, THEN bexE]) |
1254 apply (erule bex_Infinitesimal_iff2 [THEN iffD2, THEN bexE]) |
1511 hypreal_of_real x + u \<le> hypreal_of_real y + v \<Longrightarrow> x \<le> y" |
1338 hypreal_of_real x + u \<le> hypreal_of_real y + v \<Longrightarrow> x \<le> y" |
1512 by (blast intro: star_of_le [THEN iffD1] intro!: hypreal_of_real_le_add_Infininitesimal_cancel) |
1339 by (blast intro: star_of_le [THEN iffD1] intro!: hypreal_of_real_le_add_Infininitesimal_cancel) |
1513 |
1340 |
1514 lemma hypreal_of_real_less_Infinitesimal_le_zero: |
1341 lemma hypreal_of_real_less_Infinitesimal_le_zero: |
1515 "hypreal_of_real x < e \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> hypreal_of_real x \<le> 0" |
1342 "hypreal_of_real x < e \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> hypreal_of_real x \<le> 0" |
1516 apply (rule linorder_not_less [THEN iffD1], safe) |
1343 by (metis Infinitesimal_interval eq_iff le_less_linear star_of_Infinitesimal_iff_0 star_of_eq_0) |
1517 apply (drule Infinitesimal_interval) |
|
1518 apply (drule_tac [4] SReal_hypreal_of_real [THEN SReal_Infinitesimal_zero], auto) |
|
1519 done |
|
1520 |
1344 |
1521 (*used once, in Lim/NSDERIV_inverse*) |
1345 (*used once, in Lim/NSDERIV_inverse*) |
1522 lemma Infinitesimal_add_not_zero: "h \<in> Infinitesimal \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> star_of x + h \<noteq> 0" |
1346 lemma Infinitesimal_add_not_zero: "h \<in> Infinitesimal \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> star_of x + h \<noteq> 0" |
1523 apply auto |
1347 apply auto |
1524 apply (subgoal_tac "h = - star_of x") |
1348 apply (subgoal_tac "h = - star_of x") |
1525 apply (auto intro: minus_unique [symmetric]) |
1349 apply (auto intro: minus_unique [symmetric]) |
1526 done |
1350 done |
1527 |
1351 |
1528 lemma Infinitesimal_square_cancel [simp]: "x * x + y * y \<in> Infinitesimal \<Longrightarrow> x * x \<in> Infinitesimal" |
1352 lemma Infinitesimal_square_cancel [simp]: "x * x + y * y \<in> Infinitesimal \<Longrightarrow> x * x \<in> Infinitesimal" |
1529 for x y :: hypreal |
1353 for x y :: hypreal |
1530 apply (rule Infinitesimal_interval2) |
1354 by (meson Infinitesimal_interval2 le_add_same_cancel1 not_Infinitesimal_not_zero zero_le_square) |
1531 apply (rule_tac [3] zero_le_square, assumption) |
|
1532 apply auto |
|
1533 done |
|
1534 |
1355 |
1535 lemma HFinite_square_cancel [simp]: "x * x + y * y \<in> HFinite \<Longrightarrow> x * x \<in> HFinite" |
1356 lemma HFinite_square_cancel [simp]: "x * x + y * y \<in> HFinite \<Longrightarrow> x * x \<in> HFinite" |
1536 for x y :: hypreal |
1357 for x y :: hypreal |
1537 apply (rule HFinite_bounded, assumption) |
1358 using HFinite_bounded le_add_same_cancel1 zero_le_square by blast |
1538 apply auto |
|
1539 done |
|
1540 |
1359 |
1541 lemma Infinitesimal_square_cancel2 [simp]: "x * x + y * y \<in> Infinitesimal \<Longrightarrow> y * y \<in> Infinitesimal" |
1360 lemma Infinitesimal_square_cancel2 [simp]: "x * x + y * y \<in> Infinitesimal \<Longrightarrow> y * y \<in> Infinitesimal" |
1542 for x y :: hypreal |
1361 for x y :: hypreal |
1543 apply (rule Infinitesimal_square_cancel) |
1362 apply (rule Infinitesimal_square_cancel) |
1544 apply (rule add.commute [THEN subst]) |
1363 apply (rule add.commute [THEN subst]) |