386 apply (drule HFiniteD, clarify) |
386 apply (drule HFiniteD, clarify) |
387 apply (subgoal_tac "0 < t") |
387 apply (subgoal_tac "0 < t") |
388 apply (subgoal_tac "hnorm (x * y) < (r / t) * t", simp) |
388 apply (subgoal_tac "hnorm (x * y) < (r / t) * t", simp) |
389 apply (subgoal_tac "0 < r / t") |
389 apply (subgoal_tac "0 < r / t") |
390 apply (rule hnorm_mult_less) |
390 apply (rule hnorm_mult_less) |
391 apply (simp add: InfinitesimalD Reals_divide) |
391 apply (simp add: InfinitesimalD) |
392 apply assumption |
392 apply assumption |
393 apply (simp only: divide_pos_pos) |
393 apply simp |
394 apply (erule order_le_less_trans [OF hnorm_ge_zero]) |
394 apply (erule order_le_less_trans [OF hnorm_ge_zero]) |
395 done |
395 done |
396 |
396 |
397 lemma Infinitesimal_HFinite_scaleHR: |
397 lemma Infinitesimal_HFinite_scaleHR: |
398 "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> scaleHR x y \<in> Infinitesimal" |
398 "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> scaleHR x y \<in> Infinitesimal" |
402 apply (simp add: hnorm_scaleHR) |
402 apply (simp add: hnorm_scaleHR) |
403 apply (subgoal_tac "0 < t") |
403 apply (subgoal_tac "0 < t") |
404 apply (subgoal_tac "\<bar>x\<bar> * hnorm y < (r / t) * t", simp) |
404 apply (subgoal_tac "\<bar>x\<bar> * hnorm y < (r / t) * t", simp) |
405 apply (subgoal_tac "0 < r / t") |
405 apply (subgoal_tac "0 < r / t") |
406 apply (rule mult_strict_mono', simp_all) |
406 apply (rule mult_strict_mono', simp_all) |
407 apply (simp only: divide_pos_pos) |
|
408 apply (erule order_le_less_trans [OF hnorm_ge_zero]) |
407 apply (erule order_le_less_trans [OF hnorm_ge_zero]) |
409 done |
408 done |
410 |
409 |
411 lemma Infinitesimal_HFinite_mult2: |
410 lemma Infinitesimal_HFinite_mult2: |
412 fixes x y :: "'a::real_normed_algebra star" |
411 fixes x y :: "'a::real_normed_algebra star" |
416 apply (subgoal_tac "0 < t") |
415 apply (subgoal_tac "0 < t") |
417 apply (subgoal_tac "hnorm (y * x) < t * (r / t)", simp) |
416 apply (subgoal_tac "hnorm (y * x) < t * (r / t)", simp) |
418 apply (subgoal_tac "0 < r / t") |
417 apply (subgoal_tac "0 < r / t") |
419 apply (rule hnorm_mult_less) |
418 apply (rule hnorm_mult_less) |
420 apply assumption |
419 apply assumption |
421 apply (simp add: InfinitesimalD Reals_divide) |
420 apply (simp add: InfinitesimalD) |
422 apply (simp only: divide_pos_pos) |
421 apply simp |
423 apply (erule order_le_less_trans [OF hnorm_ge_zero]) |
422 apply (erule order_le_less_trans [OF hnorm_ge_zero]) |
424 done |
423 done |
425 |
424 |
426 lemma Infinitesimal_scaleR2: |
425 lemma Infinitesimal_scaleR2: |
427 "x \<in> Infinitesimal ==> a *\<^sub>R x \<in> Infinitesimal" |
426 "x \<in> Infinitesimal ==> a *\<^sub>R x \<in> Infinitesimal" |
428 apply (case_tac "a = 0", simp) |
427 apply (case_tac "a = 0", simp) |
429 apply (rule InfinitesimalI) |
428 apply (rule InfinitesimalI) |
430 apply (drule InfinitesimalD) |
429 apply (drule InfinitesimalD) |
431 apply (drule_tac x="r / \<bar>star_of a\<bar>" in bspec) |
430 apply (drule_tac x="r / \<bar>star_of a\<bar>" in bspec) |
432 apply (simp add: Reals_eq_Standard) |
431 apply (simp add: Reals_eq_Standard) |
433 apply (simp add: divide_pos_pos) |
432 apply simp |
434 apply (simp add: hnorm_scaleR pos_less_divide_eq mult_commute) |
433 apply (simp add: hnorm_scaleR pos_less_divide_eq mult_commute) |
435 done |
434 done |
436 |
435 |
437 lemma Compl_HFinite: "- HFinite = HInfinite" |
436 lemma Compl_HFinite: "- HFinite = HInfinite" |
438 apply (auto simp add: HInfinite_def HFinite_def linorder_not_less) |
437 apply (auto simp add: HInfinite_def HFinite_def linorder_not_less) |