1524 |
1524 |
1525 lemma zero_less_abs_iff [simp]: "(0 < abs a) = (a \<noteq> (0::'a::ordered_ring))" |
1525 lemma zero_less_abs_iff [simp]: "(0 < abs a) = (a \<noteq> (0::'a::ordered_ring))" |
1526 by (simp add: abs_if linorder_neq_iff) |
1526 by (simp add: abs_if linorder_neq_iff) |
1527 |
1527 |
1528 lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::ordered_ring)" |
1528 lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::ordered_ring)" |
|
1529 apply (simp add: abs_if) |
1529 by (simp add: abs_if order_less_not_sym [of a 0]) |
1530 by (simp add: abs_if order_less_not_sym [of a 0]) |
1530 |
1531 |
1531 lemma abs_le_zero_iff [simp]: "(abs a \<le> (0::'a::ordered_ring)) = (a = 0)" |
1532 lemma abs_le_zero_iff [simp]: "(abs a \<le> (0::'a::ordered_ring)) = (a = 0)" |
1532 by (simp add: order_le_less) |
1533 by (simp add: order_le_less) |
1533 |
1534 |
1618 lemma abs_le_iff: "(abs a \<le> b) = (a \<le> b & -a \<le> (b::'a::ordered_ring))" |
1619 lemma abs_le_iff: "(abs a \<le> b) = (a \<le> b & -a \<le> (b::'a::ordered_ring))" |
1619 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) |
1620 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) |
1620 |
1621 |
1621 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_ring))" |
1622 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_ring))" |
1622 apply (simp add: order_less_le abs_le_iff) |
1623 apply (simp add: order_less_le abs_le_iff) |
|
1624 apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff) |
|
1625 apply (simp add: le_minus_self_iff linorder_neq_iff) |
|
1626 done |
|
1627 (* |
|
1628 apply (simp add: order_less_le abs_le_iff) |
1623 apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff) |
1629 apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff) |
1624 apply (simp add: linorder_not_less [symmetric]) |
1630 apply (simp add: linorder_not_less [symmetric]) |
1625 apply (simp add: le_minus_self_iff linorder_neq_iff) |
1631 apply (simp add: le_minus_self_iff linorder_neq_iff) |
1626 apply (simp add: linorder_not_less [symmetric]) |
1632 apply (simp add: linorder_not_less [symmetric]) |
1627 done |
1633 done |
|
1634 *) |
1628 |
1635 |
1629 lemma abs_triangle_ineq: "abs (a+b) \<le> abs a + abs (b::'a::ordered_ring)" |
1636 lemma abs_triangle_ineq: "abs (a+b) \<le> abs a + abs (b::'a::ordered_ring)" |
1630 by (force simp add: abs_le_iff abs_ge_self abs_ge_minus_self add_mono) |
1637 by (force simp add: abs_le_iff abs_ge_self abs_ge_minus_self add_mono) |
1631 |
1638 |
1632 lemma abs_mult_less: |
1639 lemma abs_mult_less: |