equal
deleted
inserted
replaced
29 |
29 |
30 lemma hrabs_eqI2: "(0::hypreal)<x ==> abs x = x" |
30 lemma hrabs_eqI2: "(0::hypreal)<x ==> abs x = x" |
31 by (simp add: order_less_imp_le hrabs_eqI1) |
31 by (simp add: order_less_imp_le hrabs_eqI1) |
32 |
32 |
33 lemma hrabs_minus_eqI2: "x<(0::hypreal) ==> abs x = -x" |
33 lemma hrabs_minus_eqI2: "x<(0::hypreal) ==> abs x = -x" |
34 by (simp add: hypreal_le_def hrabs_def) |
34 by (simp add: linorder_not_less [symmetric] hrabs_def) |
35 |
35 |
36 lemma hrabs_minus_eqI1: "x<=(0::hypreal) ==> abs x = -x" |
36 lemma hrabs_minus_eqI1: "x<=(0::hypreal) ==> abs x = -x" |
37 by (auto dest: order_antisym simp add: hrabs_def) |
37 by (auto dest: order_antisym simp add: hrabs_def) |
38 |
38 |
39 declare abs_mult [simp] |
39 declare abs_mult [simp] |