more general lemmas for Ring_and_Field
authorpaulson
Mon Dec 15 16:38:25 2003 +0100 (2003-12-15)
changeset 142957f115e5c5de4
parent 14294 f4d806fd72ce
child 14296 bcba1d67f854
more general lemmas for Ring_and_Field
doc-src/TutorialI/Types/Numbers.thy
doc-src/TutorialI/Types/document/Numbers.tex
doc-src/TutorialI/Types/numerics.tex
src/HOL/HOL.thy
src/HOL/Integ/IntArith.thy
src/HOL/Real/RealArith.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/doc-src/TutorialI/Types/Numbers.thy	Sat Dec 13 09:33:52 2003 +0100
     1.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Mon Dec 15 16:38:25 2003 +0100
     1.3 @@ -200,8 +200,8 @@
     1.4  @{thm[display] realpow_abs[no_vars]}
     1.5  \rulename{realpow_abs}
     1.6  
     1.7 -@{thm[display] real_dense[no_vars]}
     1.8 -\rulename{real_dense}
     1.9 +@{thm[display] dense[no_vars]}
    1.10 +\rulename{dense}
    1.11  
    1.12  @{thm[display] realpow_abs[no_vars]}
    1.13  \rulename{realpow_abs}
    1.14 @@ -218,16 +218,16 @@
    1.15  @{thm[display] divide_divide_eq_left[no_vars]}
    1.16  \rulename{divide_divide_eq_left}
    1.17  
    1.18 -@{thm[display] real_minus_divide_eq[no_vars]}
    1.19 -\rulename{real_minus_divide_eq}
    1.20 +@{thm[display] minus_divide_left[no_vars]}
    1.21 +\rulename{minus_divide_left}
    1.22  
    1.23 -@{thm[display] real_divide_minus_eq[no_vars]}
    1.24 -\rulename{real_divide_minus_eq}
    1.25 +@{thm[display] minus_divide_right[no_vars]}
    1.26 +\rulename{minus_divide_right}
    1.27  
    1.28  This last NOT a simprule
    1.29  
    1.30 -@{thm[display] real_add_divide_distrib[no_vars]}
    1.31 -\rulename{real_add_divide_distrib}
    1.32 +@{thm[display] add_divide_distrib[no_vars]}
    1.33 +\rulename{add_divide_distrib}
    1.34  *}
    1.35  
    1.36  lemma "3/4 < (7/8 :: real)"
     2.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Sat Dec 13 09:33:52 2003 +0100
     2.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Mon Dec 15 16:38:25 2003 +0100
     2.3 @@ -277,7 +277,7 @@
     2.4  \rulename{zmod_zmult2_eq}
     2.5  
     2.6  \begin{isabelle}%
     2.7 -{\isasymbar}x\ {\isacharasterisk}\ y{\isasymbar}\ {\isacharequal}\ {\isasymbar}x{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}y{\isasymbar}%
     2.8 +{\isasymbar}a\ {\isacharasterisk}\ b{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}b{\isasymbar}%
     2.9  \end{isabelle}
    2.10  \rulename{abs_mult}%
    2.11  \end{isamarkuptext}%
    2.12 @@ -325,9 +325,9 @@
    2.13  \rulename{realpow_abs}
    2.14  
    2.15  \begin{isabelle}%
    2.16 -x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ x\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ y%
    2.17 +a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ a\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ b%
    2.18  \end{isabelle}
    2.19 -\rulename{real_dense}
    2.20 +\rulename{dense}
    2.21  
    2.22  \begin{isabelle}%
    2.23  {\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n%
    2.24 @@ -355,21 +355,21 @@
    2.25  \rulename{divide_divide_eq_left}
    2.26  
    2.27  \begin{isabelle}%
    2.28 -{\isacharminus}\ x\ {\isacharslash}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}%
    2.29 +{\isacharminus}\ {\isacharparenleft}a\ {\isacharslash}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharminus}\ a\ {\isacharslash}\ b%
    2.30  \end{isabelle}
    2.31 -\rulename{real_minus_divide_eq}
    2.32 +\rulename{minus_divide_left}
    2.33  
    2.34  \begin{isabelle}%
    2.35 -x\ {\isacharslash}\ {\isacharminus}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}%
    2.36 +{\isacharminus}\ {\isacharparenleft}a\ {\isacharslash}\ b{\isacharparenright}\ {\isacharequal}\ a\ {\isacharslash}\ {\isacharminus}\ b%
    2.37  \end{isabelle}
    2.38 -\rulename{real_divide_minus_eq}
    2.39 +\rulename{minus_divide_right}
    2.40  
    2.41  This last NOT a simprule
    2.42  
    2.43  \begin{isabelle}%
    2.44 -{\isacharparenleft}x\ {\isacharplus}\ y{\isacharparenright}\ {\isacharslash}\ z\ {\isacharequal}\ x\ {\isacharslash}\ z\ {\isacharplus}\ y\ {\isacharslash}\ z%
    2.45 +{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharslash}\ c\ {\isacharequal}\ a\ {\isacharslash}\ c\ {\isacharplus}\ b\ {\isacharslash}\ c%
    2.46  \end{isabelle}
    2.47 -\rulename{real_add_divide_distrib}%
    2.48 +\rulename{add_divide_distrib}%
    2.49  \end{isamarkuptext}%
    2.50  \isamarkuptrue%
    2.51  \isacommand{lemma}\ {\isachardoublequote}{\isadigit{3}}{\isacharslash}{\isadigit{4}}\ {\isacharless}\ {\isacharparenleft}{\isadigit{7}}{\isacharslash}{\isadigit{8}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline
     3.1 --- a/doc-src/TutorialI/Types/numerics.tex	Sat Dec 13 09:33:52 2003 +0100
     3.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Mon Dec 15 16:38:25 2003 +0100
     3.3 @@ -397,7 +397,7 @@
     3.4  Density, however, is trivial to express:
     3.5  \begin{isabelle}
     3.6  x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%
     3.7 -\rulename{real_dense}
     3.8 +\rulename{dense}
     3.9  \end{isabelle}
    3.10  
    3.11  Here is a selection of rules about the division operator.  The following
    3.12 @@ -417,17 +417,17 @@
    3.13  Signs are extracted from quotients in the hope that complementary terms can
    3.14  then be cancelled:
    3.15  \begin{isabelle}
    3.16 --\ x\ /\ y\ =\ -\ (x\ /\ y)
    3.17 -\rulename{real_minus_divide_eq}\isanewline
    3.18 -x\ /\ -\ y\ =\ -\ (x\ /\ y)
    3.19 -\rulename{real_divide_minus_eq}
    3.20 +-\ (a\ /\ b)\ =\ -\ a\ /\ b
    3.21 +\rulename{minus_divide_left}\isanewline
    3.22 +-\ (a\ /\ b)\ =\ a\ /\ -\ b
    3.23 +\rulename{minus_divide_right}
    3.24  \end{isabelle}
    3.25  
    3.26  The following distributive law is available, but it is not installed as a
    3.27  simplification rule.
    3.28  \begin{isabelle}
    3.29 -(x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z%
    3.30 -\rulename{real_add_divide_distrib}
    3.31 +(a\ +\ b)\ /\ c\ =\ a\ /\ c\ +\ b\ /\ c%
    3.32 +\rulename{add_divide_distrib}
    3.33  \end{isabelle}
    3.34  
    3.35  As with the other numeric types, the simplifier can sort the operands of
     4.1 --- a/src/HOL/HOL.thy	Sat Dec 13 09:33:52 2003 +0100
     4.2 +++ b/src/HOL/HOL.thy	Mon Dec 15 16:38:25 2003 +0100
     4.3 @@ -645,6 +645,9 @@
     4.4    "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
     4.5  
     4.6  
     4.7 +lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
     4.8 +by blast
     4.9 +
    4.10  subsubsection {* Monotonicity *}
    4.11  
    4.12  locale mono =
    4.13 @@ -716,6 +719,9 @@
    4.14    apply (erule contrapos_np, simp)
    4.15    done
    4.16  
    4.17 +lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"  
    4.18 +by (blast intro: order_antisym)
    4.19 +
    4.20  
    4.21  text {* Transitivity. *}
    4.22  
     5.1 --- a/src/HOL/Integ/IntArith.thy	Sat Dec 13 09:33:52 2003 +0100
     5.2 +++ b/src/HOL/Integ/IntArith.thy	Mon Dec 15 16:38:25 2003 +0100
     5.3 @@ -93,7 +93,8 @@
     5.4     but arith_tac is not parameterized by such simp rules
     5.5  *)
     5.6  
     5.7 -lemma zabs_split: "P(abs(i::int)) = ((0 \<le> i --> P i) & (i < 0 --> P(-i)))"
     5.8 +lemma zabs_split [arith_split]:
     5.9 +     "P(abs(i::int)) = ((0 \<le> i --> P i) & (i < 0 --> P(-i)))"
    5.10  by (simp add: zabs_def)
    5.11  
    5.12  lemma zero_le_zabs [iff]: "0 \<le> abs (z::int)"
    5.13 @@ -104,8 +105,6 @@
    5.14        z is an integer literal.*}
    5.15  declare int_eq_iff [of _ "number_of v", standard, simp]
    5.16  
    5.17 -declare zabs_split [arith_split]
    5.18 -
    5.19  lemma zabs_eq_iff:
    5.20      "(abs (z::int) = w) = (z = w \<and> 0 \<le> z \<or> z = -w \<and> z < 0)"
    5.21    by (auto simp add: zabs_def)
    5.22 @@ -113,7 +112,7 @@
    5.23  lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
    5.24    by simp
    5.25  
    5.26 -lemma split_nat[arith_split]:
    5.27 +lemma split_nat [arith_split]:
    5.28    "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
    5.29    (is "?P = (?L & ?R)")
    5.30  proof (cases "i < 0")
     6.1 --- a/src/HOL/Real/RealArith.thy	Sat Dec 13 09:33:52 2003 +0100
     6.2 +++ b/src/HOL/Real/RealArith.thy	Mon Dec 15 16:38:25 2003 +0100
     6.3 @@ -76,14 +76,12 @@
     6.4  
     6.5  subsection{*Absolute Value Function for the Reals*}
     6.6  
     6.7 -lemma abs_nat_number_of: 
     6.8 +lemma abs_nat_number_of [simp]: 
     6.9       "abs (number_of v :: real) =  
    6.10          (if neg (number_of v) then number_of (bin_minus v)  
    6.11           else number_of v)"
    6.12 -apply (simp add: real_abs_def bin_arith_simps minus_real_number_of le_real_number_of_eq_not_less less_real_number_of real_of_int_le_iff)
    6.13 -done
    6.14 -
    6.15 -declare abs_nat_number_of [simp]
    6.16 +by (simp add: real_abs_def bin_arith_simps minus_real_number_of
    6.17 +       le_real_number_of_eq_not_less less_real_number_of real_of_int_le_iff)
    6.18  
    6.19  
    6.20  (*----------------------------------------------------------------------------
    6.21 @@ -101,85 +99,30 @@
    6.22  lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x"
    6.23  by (unfold real_abs_def real_le_def, simp)
    6.24  
    6.25 -lemma abs_mult_inverse: "abs (x * inverse y) = (abs x) * inverse (abs (y::real))"
    6.26 -by (simp add: abs_mult abs_inverse)
    6.27 -
    6.28 -text{*Much easier to prove using arithmetic than abstractly!!*}
    6.29 -lemma abs_triangle_ineq: "abs(x+y) \<le> abs x + abs (y::real)"
    6.30 -by (unfold real_abs_def, simp)
    6.31 -
    6.32 -(*Unused, but perhaps interesting as an example*)
    6.33 -lemma abs_triangle_ineq_four: "abs(w + x + y + z) \<le> abs(w) + abs(x) + abs(y) + abs(z::real)"
    6.34 -by (simp add: abs_triangle_ineq [THEN order_trans])
    6.35 -
    6.36  lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
    6.37  by (unfold real_abs_def, simp)
    6.38  
    6.39 -lemma abs_triangle_minus_ineq: "abs(x + (-y)) \<le> abs x + abs (y::real)"
    6.40 -by (unfold real_abs_def, simp)
    6.41 -
    6.42 -lemma abs_add_less [rule_format (no_asm)]: "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)"
    6.43 -by (unfold real_abs_def, simp)
    6.44 -
    6.45 -lemma abs_add_minus_less:
    6.46 -     "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)"
    6.47 -by (unfold real_abs_def, simp)
    6.48 -
    6.49  lemma abs_minus_one [simp]: "abs (-1) = (1::real)"
    6.50  by (unfold real_abs_def, simp)
    6.51  
    6.52  lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))"
    6.53 -by (unfold real_abs_def, auto)
    6.54 +by (force simp add: Ring_and_Field.abs_less_iff)
    6.55  
    6.56  lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
    6.57 -by (unfold real_abs_def, auto)
    6.58 +by (force simp add: Ring_and_Field.abs_le_iff)
    6.59  
    6.60 -lemma abs_add_pos_gt_zero: "(0::real) < k ==> 0 < k + abs(x)"
    6.61 +lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)"
    6.62  by (unfold real_abs_def, auto)
    6.63  
    6.64 -lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
    6.65 -by (unfold real_abs_def, auto)
    6.66 -declare abs_add_one_gt_zero [simp]
    6.67 +lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
    6.68 +by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero)
    6.69  
    6.70 -lemma abs_circle: "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)"
    6.71 -by (auto intro: abs_triangle_ineq [THEN order_le_less_trans])
    6.72 -
    6.73 -lemma abs_real_of_nat_cancel: "abs (real x) = real (x::nat)"
    6.74 -by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero)
    6.75 -declare abs_real_of_nat_cancel [simp]
    6.76 -
    6.77 -lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
    6.78 +lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
    6.79  apply (rule real_leD)
    6.80  apply (auto intro: abs_ge_self [THEN order_trans])
    6.81  done
    6.82 -declare abs_add_one_not_less_self [simp]
    6.83   
    6.84 -(* used in vector theory *)
    6.85 -lemma abs_triangle_ineq_three: "abs(w + x + (y::real)) \<le> abs(w) + abs(x) + abs(y)"
    6.86 -by (auto intro!: abs_triangle_ineq [THEN order_trans] real_add_left_mono
    6.87 -                 simp add: real_add_assoc)
    6.88 -
    6.89 -lemma abs_diff_less_imp_gt_zero: "abs(x - y) < y ==> (0::real) < y"
    6.90 -apply (unfold real_abs_def)
    6.91 -apply (case_tac "0 \<le> x - y", auto)
    6.92 -done
    6.93 -
    6.94 -lemma abs_diff_less_imp_gt_zero2: "abs(x - y) < x ==> (0::real) < x"
    6.95 -apply (unfold real_abs_def)
    6.96 -apply (case_tac "0 \<le> x - y", auto)
    6.97 -done
    6.98 -
    6.99 -lemma abs_diff_less_imp_gt_zero3: "abs(x - y) < y ==> (0::real) < x"
   6.100 -by (auto simp add: abs_interval_iff)
   6.101 -
   6.102 -lemma abs_diff_less_imp_gt_zero4: "abs(x - y) < -y ==> x < (0::real)"
   6.103 -by (auto simp add: abs_interval_iff)
   6.104 -
   6.105 -lemma abs_triangle_ineq_minus_cancel: 
   6.106 -     "abs(x) \<le> abs(x + (-y)) + abs((y::real))"
   6.107 -apply (unfold real_abs_def, auto)
   6.108 -done
   6.109 -
   6.110 +text{*Used only in Hyperreal/Lim.ML*}
   6.111  lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
   6.112  apply (simp add: real_add_assoc)
   6.113  apply (rule_tac x1 = y in real_add_left_commute [THEN ssubst])
   6.114 @@ -220,29 +163,16 @@
   6.115  val abs_ge_minus_self = thm"abs_ge_minus_self";
   6.116  val abs_mult = thm"abs_mult";
   6.117  val abs_inverse = thm"abs_inverse";
   6.118 -val abs_mult_inverse = thm"abs_mult_inverse";
   6.119  val abs_triangle_ineq = thm"abs_triangle_ineq";
   6.120 -val abs_triangle_ineq_four = thm"abs_triangle_ineq_four";
   6.121  val abs_minus_cancel = thm"abs_minus_cancel";
   6.122  val abs_minus_add_cancel = thm"abs_minus_add_cancel";
   6.123 -val abs_triangle_minus_ineq = thm"abs_triangle_minus_ineq";
   6.124 -val abs_add_less = thm"abs_add_less";
   6.125 -val abs_add_minus_less = thm"abs_add_minus_less";
   6.126  val abs_minus_one = thm"abs_minus_one";
   6.127  val abs_interval_iff = thm"abs_interval_iff";
   6.128  val abs_le_interval_iff = thm"abs_le_interval_iff";
   6.129 -val abs_add_pos_gt_zero = thm"abs_add_pos_gt_zero";
   6.130  val abs_add_one_gt_zero = thm"abs_add_one_gt_zero";
   6.131 -val abs_circle = thm"abs_circle";
   6.132  val abs_le_zero_iff = thm"abs_le_zero_iff";
   6.133  val abs_real_of_nat_cancel = thm"abs_real_of_nat_cancel";
   6.134  val abs_add_one_not_less_self = thm"abs_add_one_not_less_self";
   6.135 -val abs_triangle_ineq_three = thm"abs_triangle_ineq_three";
   6.136 -val abs_diff_less_imp_gt_zero = thm"abs_diff_less_imp_gt_zero";
   6.137 -val abs_diff_less_imp_gt_zero2 = thm"abs_diff_less_imp_gt_zero2";
   6.138 -val abs_diff_less_imp_gt_zero3 = thm"abs_diff_less_imp_gt_zero3";
   6.139 -val abs_diff_less_imp_gt_zero4 = thm"abs_diff_less_imp_gt_zero4";
   6.140 -val abs_triangle_ineq_minus_cancel = thm"abs_triangle_ineq_minus_cancel";
   6.141  val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq";
   6.142  
   6.143  val abs_mult_less = thm"abs_mult_less";
     7.1 --- a/src/HOL/Ring_and_Field.thy	Sat Dec 13 09:33:52 2003 +0100
     7.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Dec 15 16:38:25 2003 +0100
     7.3 @@ -1434,11 +1434,55 @@
     7.4  apply (simp add: nonzero_abs_divide) 
     7.5  done
     7.6  
     7.7 -(*TOO DIFFICULT: 6 CASES
     7.8 +lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::ordered_ring)"
     7.9 +by (simp add: abs_if)
    7.10 +
    7.11 +lemma le_minus_self_iff: "(a \<le> -a) = (a \<le> (0::'a::ordered_ring))"
    7.12 +proof 
    7.13 +  assume ale: "a \<le> -a"
    7.14 +  show "a\<le>0"
    7.15 +    apply (rule classical) 
    7.16 +    apply (simp add: linorder_not_le) 
    7.17 +    apply (blast intro: ale order_trans order_less_imp_le
    7.18 +                        neg_0_le_iff_le [THEN iffD1]) 
    7.19 +    done
    7.20 +next
    7.21 +  assume "a\<le>0"
    7.22 +  hence "0 \<le> -a" by (simp only: neg_0_le_iff_le)
    7.23 +  thus "a \<le> -a"  by (blast intro: prems order_trans) 
    7.24 +qed
    7.25 +
    7.26 +lemma minus_le_self_iff: "(-a \<le> a) = (0 \<le> (a::'a::ordered_ring))"
    7.27 +by (insert le_minus_self_iff [of "-a"], simp)
    7.28 +
    7.29 +lemma eq_minus_self_iff: "(a = -a) = (a = (0::'a::ordered_ring))"
    7.30 +by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff)
    7.31 +
    7.32 +lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_ring))"
    7.33 +by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff)
    7.34 +
    7.35 +lemma abs_le_D1: "abs a \<le> b ==> a \<le> (b::'a::ordered_ring)"
    7.36 +apply (simp add: abs_if split: split_if_asm)
    7.37 +apply (rule order_trans [of _ "-a"]) 
    7.38 + apply (simp add: less_minus_self_iff order_less_imp_le, assumption)
    7.39 +done
    7.40 +
    7.41 +lemma abs_le_D2: "abs a \<le> b ==> -a \<le> (b::'a::ordered_ring)"
    7.42 +by (insert abs_le_D1 [of "-a"], simp)
    7.43 +
    7.44 +lemma abs_le_iff: "(abs a \<le> b) = (a \<le> b & -a \<le> (b::'a::ordered_ring))"
    7.45 +by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
    7.46 +
    7.47 +lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_ring))" 
    7.48 +apply (simp add: order_less_le abs_le_iff)  
    7.49 +apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff) 
    7.50 + apply (simp add:  linorder_not_less [symmetric]) 
    7.51 +apply (simp add: le_minus_self_iff linorder_neq_iff) 
    7.52 +apply (simp add:  linorder_not_less [symmetric]) 
    7.53 +done
    7.54 +
    7.55  lemma abs_triangle_ineq: "abs (a+b) \<le> abs a + abs (b::'a::ordered_ring)"
    7.56 -apply (simp add: abs_if)
    7.57 -apply (auto ); 
    7.58 -*)
    7.59 +by (force simp add: abs_le_iff abs_ge_self abs_ge_minus_self add_mono)
    7.60  
    7.61  lemma abs_mult_less:
    7.62       "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_ring)"