equal
deleted
inserted
replaced
1022 |
1022 |
1023 lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" |
1023 lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" |
1024 by (simp add: real_of_nat_ge_zero) |
1024 by (simp add: real_of_nat_ge_zero) |
1025 |
1025 |
1026 lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" |
1026 lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" |
1027 apply (simp add: linorder_not_less) |
1027 by simp |
1028 apply (auto intro: abs_ge_self [THEN order_trans]) |
|
1029 done |
|
1030 |
1028 |
1031 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)" |
1029 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)" |
1032 apply (simp add: real_add_assoc) |
1030 by simp |
1033 apply (rule_tac a1 = y in add_left_commute [THEN ssubst]) |
|
1034 apply (rule real_add_assoc [THEN subst]) |
|
1035 apply (rule abs_triangle_ineq) |
|
1036 done |
|
1037 |
1031 |
1038 end |
1032 end |