531 by (auto_tac (claset() addSIs [Infinitesimal_hyperpow], |
531 by (auto_tac (claset() addSIs [Infinitesimal_hyperpow], |
532 simpset() addsimps [hrealpow_hyperpow_Infinitesimal_iff, |
532 simpset() addsimps [hrealpow_hyperpow_Infinitesimal_iff, |
533 hypnat_of_nat_less_iff,hypnat_of_nat_zero] |
533 hypnat_of_nat_less_iff,hypnat_of_nat_zero] |
534 delsimps [hypnat_of_nat_less_iff RS sym])); |
534 delsimps [hypnat_of_nat_less_iff RS sym])); |
535 qed "Infinitesimal_hrealpow"; |
535 qed "Infinitesimal_hrealpow"; |
|
536 |
|
537 (* MOVE UP *) |
|
538 Goal "(0::hypreal) <= x * x"; |
|
539 by (auto_tac (claset(),simpset() addsimps |
|
540 [hypreal_0_le_mult_iff])); |
|
541 qed "hypreal_mult_self_ge_zero"; |
|
542 Addsimps [hypreal_mult_self_ge_zero]; |
|
543 |
|
544 Goal "[|(0::hypreal) <= x; 0 <= y; x ^ Suc n = y ^ Suc n |] ==> x = y"; |
|
545 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
546 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
547 by (auto_tac (claset(),simpset() addsimps |
|
548 [hrealpow,hypreal_mult,hypreal_le,hypreal_zero_num])); |
|
549 by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq], |
|
550 simpset()) 1); |
|
551 qed "hrealpow_Suc_cancel_eq"; |
|
552 |