src/HOL/Real/RealAbs.ML
changeset 10043 a0364652e115
parent 9432 8b7aad2abcc9
child 10606 e3229a37d53f
     1.1 --- a/src/HOL/Real/RealAbs.ML	Thu Sep 21 10:42:49 2000 +0200
     1.2 +++ b/src/HOL/Real/RealAbs.ML	Thu Sep 21 12:11:38 2000 +0200
     1.3 @@ -271,3 +271,14 @@
     1.4  by (auto_tac (claset(),simpset() addsimps [abs_interval_iff]));
     1.5  qed "abs_diff_less_imp_gt_zero4";
     1.6  
     1.7 +Goalw [abs_real_def] 
     1.8 +     " abs(x) <= abs(x + (-y)) + abs((y::real))";
     1.9 +by Auto_tac;
    1.10 +qed "abs_triangle_ineq_minus_cancel";
    1.11 +
    1.12 +Goal "abs ((x::real) + y + (-l + -m)) <= abs(x + -l) + abs(y + -m)";
    1.13 +by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
    1.14 +by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1);
    1.15 +by (rtac (real_add_assoc RS subst) 1);
    1.16 +by (rtac abs_triangle_ineq 1);
    1.17 +qed "abs_sum_triangle_ineq";