src/HOL/Real/RealDef.thy
changeset 15229 1eb23f805c06
parent 15169 2b5da07a0b89
child 15542 ee6cd48cf840
     1.1 --- a/src/HOL/Real/RealDef.thy	Mon Oct 04 15:28:03 2004 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Tue Oct 05 15:30:50 2004 +0200
     1.3 @@ -810,16 +810,6 @@
     1.4  
     1.5  subsection{*Absolute Value Function for the Reals*}
     1.6  
     1.7 -text{*FIXME: these should go!*}
     1.8 -lemma abs_eqI1: "(0::real)\<le>x ==> abs x = x"
     1.9 -by (simp add: abs_if)
    1.10 -
    1.11 -lemma abs_eqI2: "(0::real) < x ==> abs x = x"
    1.12 -by (simp add: abs_if)
    1.13 -
    1.14 -lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x"
    1.15 -by (simp add: abs_if linorder_not_less [symmetric])
    1.16 -
    1.17  lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
    1.18  by (simp add: abs_if)
    1.19  
    1.20 @@ -834,7 +824,7 @@
    1.21  by (simp add: abs_if)
    1.22  
    1.23  lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
    1.24 -by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero)
    1.25 +by (simp add: real_of_nat_ge_zero)
    1.26  
    1.27  lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
    1.28  apply (simp add: linorder_not_less)
    1.29 @@ -857,27 +847,11 @@
    1.30  val real_less_half_sum = thm"real_less_half_sum";
    1.31  val real_gt_half_sum = thm"real_gt_half_sum";
    1.32  
    1.33 -val abs_eqI1 = thm"abs_eqI1";
    1.34 -val abs_eqI2 = thm"abs_eqI2";
    1.35 -val abs_minus_eqI2 = thm"abs_minus_eqI2";
    1.36 -val abs_ge_zero = thm"abs_ge_zero";
    1.37 -val abs_idempotent = thm"abs_idempotent";
    1.38 -val abs_eq_0 = thm"abs_eq_0";
    1.39 -val abs_ge_self = thm"abs_ge_self";
    1.40 -val abs_ge_minus_self = thm"abs_ge_minus_self";
    1.41 -val abs_mult = thm"abs_mult";
    1.42 -val abs_inverse = thm"abs_inverse";
    1.43 -val abs_triangle_ineq = thm"abs_triangle_ineq";
    1.44 -val abs_minus_cancel = thm"abs_minus_cancel";
    1.45 -val abs_minus_add_cancel = thm"abs_minus_add_cancel";
    1.46  val abs_interval_iff = thm"abs_interval_iff";
    1.47  val abs_le_interval_iff = thm"abs_le_interval_iff";
    1.48  val abs_add_one_gt_zero = thm"abs_add_one_gt_zero";
    1.49 -val abs_le_zero_iff = thm"abs_le_zero_iff";
    1.50  val abs_add_one_not_less_self = thm"abs_add_one_not_less_self";
    1.51  val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq";
    1.52 -
    1.53 -val abs_mult_less = thm"abs_mult_less";
    1.54  *}
    1.55  
    1.56