equal
deleted
inserted
replaced
1710 Goal "abs (real x) = real (x::nat)"; |
1710 Goal "abs (real x) = real (x::nat)"; |
1711 by (auto_tac (claset() addIs [abs_eqI1], simpset())); |
1711 by (auto_tac (claset() addIs [abs_eqI1], simpset())); |
1712 qed "abs_real_of_nat_cancel"; |
1712 qed "abs_real_of_nat_cancel"; |
1713 Addsimps [abs_real_of_nat_cancel]; |
1713 Addsimps [abs_real_of_nat_cancel]; |
1714 |
1714 |
1715 Goal "~ abs(x) + 1r < x"; |
1715 Goal "~ abs(x) + (1::real) < x"; |
1716 by (rtac real_leD 1); |
1716 by (rtac real_leD 1); |
1717 by (auto_tac (claset() addIs [abs_ge_self RS order_trans],simpset())); |
1717 by (auto_tac (claset() addIs [abs_ge_self RS order_trans],simpset())); |
1718 qed "abs_add_one_not_less_self"; |
1718 qed "abs_add_one_not_less_self"; |
1719 Addsimps [abs_add_one_not_less_self]; |
1719 Addsimps [abs_add_one_not_less_self]; |
1720 |
1720 |