more simplification rules on unary and binary minus
authorhaftmann
Fri Nov 01 18:51:14 2013 +0100 (2013-11-01)
changeset 54230b1d955791529
parent 54229 ca638d713ff8
child 54231 2975658d49cd
more simplification rules on unary and binary minus
NEWS
src/HOL/Big_Operators.thy
src/HOL/Complex.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Deriv.thy
src/HOL/Divides.thy
src/HOL/Fields.thy
src/HOL/Groups.thy
src/HOL/Hahn_Banach/Vector_Space.thy
src/HOL/Int.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Float.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Library/Function_Algebras.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Lattice_Algebras.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Product_plus.thy
src/HOL/Library/Set_Algebras.thy
src/HOL/Limits.thy
src/HOL/Matrix_LP/LP.thy
src/HOL/Matrix_LP/Matrix.thy
src/HOL/Metis_Examples/Big_O.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/CLim.thy
src/HOL/NSA/HDeriv.thy
src/HOL/NSA/HLim.thy
src/HOL/NSA/HSEQ.thy
src/HOL/NSA/HSeries.thy
src/HOL/NSA/HTranscendental.thy
src/HOL/NSA/NSA.thy
src/HOL/NSA/NSCA.thy
src/HOL/NSA/StarDef.thy
src/HOL/Num.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Rings.thy
src/HOL/Semiring_Normalization.thy
src/HOL/Series.thy
src/HOL/Tools/group_cancel.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Transcendental.thy
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/WordBitwise.thy
src/HOL/ex/Dedekind_Real.thy
src/HOL/ex/Gauge_Integration.thy
     1.1 --- a/NEWS	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/NEWS	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -15,6 +15,39 @@
     1.4      even_zero_(nat|int) ~> even_zero
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Elimination of fact duplicates:
    1.10 +    equals_zero_I ~> minus_unique
    1.11 +    diff_eq_0_iff_eq ~> right_minus_eq
    1.12 +INCOMPATIBILITY.
    1.13 +
    1.14 +* Fact name consolidation:
    1.15 +    diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus
    1.16 +INCOMPATIBILITY.
    1.17 +
    1.18 +* More simplification rules on unary and binary minus:
    1.19 +add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,
    1.20 +add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,
    1.21 +add_minus_cancel, diff_add_cancel, le_add_same_cancel1,
    1.22 +le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,
    1.23 +minus_add_cancel, uminus_add_conv_diff.  These correspondingly
    1.24 +have been taken away from fact collections algebra_simps and
    1.25 +field_simps.  INCOMPATIBILITY.
    1.26 +
    1.27 +To restore proofs, the following patterns are helpful:
    1.28 +
    1.29 +a) Arbitrary failing proof not involving "diff_def":
    1.30 +Consider simplification with algebra_simps or field_simps.
    1.31 +
    1.32 +b) Lifting rules from addition to subtraction:
    1.33 +Try with "using <rule for addition> of [… "- _" …]" by simp".
    1.34 +
    1.35 +c) Simplification with "diff_def": just drop "diff_def".
    1.36 +Consider simplification with algebra_simps or field_simps;
    1.37 +or the brute way with
    1.38 +"simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
    1.39 +
    1.40  
    1.41  New in Isabelle2013-1 (November 2013)
    1.42  -------------------------------------
     2.1 --- a/src/HOL/Big_Operators.thy	Thu Oct 31 16:54:22 2013 +0100
     2.2 +++ b/src/HOL/Big_Operators.thy	Fri Nov 01 18:51:14 2013 +0100
     2.3 @@ -696,11 +696,7 @@
     2.4  lemma setsum_subtractf:
     2.5    "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
     2.6      setsum f A - setsum g A"
     2.7 -proof (cases "finite A")
     2.8 -  case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
     2.9 -next
    2.10 -  case False thus ?thesis by simp
    2.11 -qed
    2.12 +  using setsum_addf [of f "- g" A] by (simp add: setsum_negf)
    2.13  
    2.14  lemma setsum_nonneg:
    2.15    assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
     3.1 --- a/src/HOL/Complex.thy	Thu Oct 31 16:54:22 2013 +0100
     3.2 +++ b/src/HOL/Complex.thy	Fri Nov 01 18:51:14 2013 +0100
     3.3 @@ -587,7 +587,7 @@
     3.4    by (simp add: cis_def)
     3.5  
     3.6  lemma cis_divide: "cis a / cis b = cis (a - b)"
     3.7 -  by (simp add: complex_divide_def cis_mult diff_minus)
     3.8 +  by (simp add: complex_divide_def cis_mult)
     3.9  
    3.10  lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
    3.11    by (auto simp add: DeMoivre)
     4.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Oct 31 16:54:22 2013 +0100
     4.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Nov 01 18:51:14 2013 +0100
     4.3 @@ -29,7 +29,7 @@
     4.4    have shift_pow: "\<And>i. - (x * ((-1)^i * a (Suc i) * x ^ i)) = (-1)^(Suc i) * a (Suc i) * x ^ (Suc i)"
     4.5      by auto
     4.6    show ?thesis
     4.7 -    unfolding setsum_right_distrib shift_pow diff_minus setsum_negf[symmetric]
     4.8 +    unfolding setsum_right_distrib shift_pow uminus_add_conv_diff [symmetric] setsum_negf[symmetric]
     4.9      setsum_head_upt_Suc[OF zero_less_Suc]
    4.10      setsum_reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\<lambda> n. (-1)^n  *a n * x^n"] by auto
    4.11  qed
    4.12 @@ -533,12 +533,12 @@
    4.13    have "pi \<le> ub_pi n"
    4.14      unfolding ub_pi_def machin_pi Let_def unfolding Float_num
    4.15      using lb_arctan[of 239] ub_arctan[of 5] powr_realpow[of 2 2]
    4.16 -    by (auto intro!: mult_left_mono add_mono simp add: diff_minus)
    4.17 +    by (auto intro!: mult_left_mono add_mono simp add: uminus_add_conv_diff [symmetric] simp del: uminus_add_conv_diff)
    4.18    moreover
    4.19    have "lb_pi n \<le> pi"
    4.20      unfolding lb_pi_def machin_pi Let_def Float_num
    4.21      using lb_arctan[of 5] ub_arctan[of 239] powr_realpow[of 2 2]
    4.22 -    by (auto intro!: mult_left_mono add_mono simp add: diff_minus)
    4.23 +    by (auto intro!: mult_left_mono add_mono simp add: uminus_add_conv_diff [symmetric] simp del: uminus_add_conv_diff)
    4.24    ultimately show ?thesis by auto
    4.25  qed
    4.26  
    4.27 @@ -1208,8 +1208,8 @@
    4.28      using x unfolding k[symmetric]
    4.29      by (cases "k = 0")
    4.30         (auto intro!: add_mono
    4.31 -                simp add: diff_minus k[symmetric]
    4.32 -                simp del: float_of_numeral)
    4.33 +                simp add: k [symmetric] uminus_add_conv_diff [symmetric]
    4.34 +                simp del: float_of_numeral uminus_add_conv_diff)
    4.35    note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]
    4.36    hence lx_less_ux: "?lx \<le> real ?ux" by (rule order_trans)
    4.37  
    4.38 @@ -1223,7 +1223,7 @@
    4.39      also have "\<dots> \<le> cos (x + (-k) * (2 * pi))"
    4.40        using cos_monotone_minus_pi_0'[OF pi_lx lx x_le_0]
    4.41        by (simp only: uminus_float.rep_eq real_of_int_minus
    4.42 -        cos_minus diff_minus mult_minus_left)
    4.43 +        cos_minus mult_minus_left) simp
    4.44      finally have "(lb_cos prec (- ?lx)) \<le> cos x"
    4.45        unfolding cos_periodic_int . }
    4.46    note negative_lx = this
    4.47 @@ -1236,7 +1236,7 @@
    4.48      have "cos (x + (-k) * (2 * pi)) \<le> cos ?lx"
    4.49        using cos_monotone_0_pi'[OF lx_0 lx pi_x]
    4.50        by (simp only: real_of_int_minus
    4.51 -        cos_minus diff_minus mult_minus_left)
    4.52 +        cos_minus mult_minus_left) simp
    4.53      also have "\<dots> \<le> (ub_cos prec ?lx)"
    4.54        using lb_cos[OF lx_0 pi_lx] by simp
    4.55      finally have "cos x \<le> (ub_cos prec ?lx)"
    4.56 @@ -1251,7 +1251,7 @@
    4.57      have "cos (x + (-k) * (2 * pi)) \<le> cos (real (- ?ux))"
    4.58        using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
    4.59        by (simp only: uminus_float.rep_eq real_of_int_minus
    4.60 -          cos_minus diff_minus mult_minus_left)
    4.61 +          cos_minus mult_minus_left) simp
    4.62      also have "\<dots> \<le> (ub_cos prec (- ?ux))"
    4.63        using lb_cos_minus[OF pi_ux ux_0, of prec] by simp
    4.64      finally have "cos x \<le> (ub_cos prec (- ?ux))"
    4.65 @@ -1268,7 +1268,7 @@
    4.66      also have "\<dots> \<le> cos (x + (-k) * (2 * pi))"
    4.67        using cos_monotone_0_pi'[OF x_ge_0 ux pi_ux]
    4.68        by (simp only: real_of_int_minus
    4.69 -        cos_minus diff_minus mult_minus_left)
    4.70 +        cos_minus mult_minus_left) simp
    4.71      finally have "(lb_cos prec ?ux) \<le> cos x"
    4.72        unfolding cos_periodic_int . }
    4.73    note positive_ux = this
    4.74 @@ -1343,7 +1343,7 @@
    4.75        also have "\<dots> \<le> cos ((?ux - 2 * ?lpi))"
    4.76          using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
    4.77          by (simp only: minus_float.rep_eq real_of_int_minus real_of_one minus_one[symmetric]
    4.78 -            diff_minus mult_minus_left mult_1_left)
    4.79 +            mult_minus_left mult_1_left) simp
    4.80        also have "\<dots> = cos ((- (?ux - 2 * ?lpi)))"
    4.81          unfolding uminus_float.rep_eq cos_minus ..
    4.82        also have "\<dots> \<le> (ub_cos prec (- (?ux - 2 * ?lpi)))"
    4.83 @@ -1387,7 +1387,7 @@
    4.84        also have "\<dots> \<le> cos ((?lx + 2 * ?lpi))"
    4.85          using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
    4.86          by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
    4.87 -          minus_one[symmetric] diff_minus mult_minus_left mult_1_left)
    4.88 +          minus_one[symmetric] mult_minus_left mult_1_left) simp
    4.89        also have "\<dots> \<le> (ub_cos prec (?lx + 2 * ?lpi))"
    4.90          using lb_cos[OF lx_0 pi_lx] by simp
    4.91        finally show ?thesis unfolding u by (simp add: real_of_float_max)
    4.92 @@ -2164,12 +2164,12 @@
    4.93    unfolding divide_inverse interpret_floatarith.simps ..
    4.94  
    4.95  lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
    4.96 -  unfolding diff_minus interpret_floatarith.simps ..
    4.97 +  unfolding interpret_floatarith.simps by simp
    4.98  
    4.99  lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
   4.100    sin (interpret_floatarith a vs)"
   4.101    unfolding sin_cos_eq interpret_floatarith.simps
   4.102 -            interpret_floatarith_divide interpret_floatarith_diff diff_minus
   4.103 +            interpret_floatarith_divide interpret_floatarith_diff
   4.104    by auto
   4.105  
   4.106  lemma interpret_floatarith_tan:
   4.107 @@ -3192,7 +3192,7 @@
   4.108  
   4.109    from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
   4.110    have "ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
   4.111 -    by (auto simp add: diff_minus)
   4.112 +    by auto
   4.113    from order_less_le_trans[OF _ this, of 0] `0 < ly`
   4.114    show ?thesis by auto
   4.115  qed
   4.116 @@ -3214,7 +3214,7 @@
   4.117  
   4.118    from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
   4.119    have "ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
   4.120 -    by (auto simp add: diff_minus)
   4.121 +    by auto
   4.122    from order_trans[OF _ this, of 0] `0 \<le> ly`
   4.123    show ?thesis by auto
   4.124  qed
     5.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Thu Oct 31 16:54:22 2013 +0100
     5.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Nov 01 18:51:14 2013 +0100
     5.3 @@ -1400,9 +1400,8 @@
     5.4    also have "\<dots> = (j dvd (- (c*x - ?e)))"
     5.5      by (simp only: dvd_minus_iff)
     5.6    also have "\<dots> = (j dvd (c* (- x)) + ?e)"
     5.7 -    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
     5.8 -    apply (simp add: algebra_simps)
     5.9 -    done
    5.10 +    by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
    5.11 +      (simp add: algebra_simps)
    5.12    also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
    5.13      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
    5.14    finally show ?case .
    5.15 @@ -1413,9 +1412,8 @@
    5.16    also have "\<dots> = (j dvd (- (c*x - ?e)))"
    5.17      by (simp only: dvd_minus_iff)
    5.18    also have "\<dots> = (j dvd (c* (- x)) + ?e)"
    5.19 -    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
    5.20 -    apply (simp add: algebra_simps)
    5.21 -    done
    5.22 +    by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
    5.23 +      (simp add: algebra_simps)
    5.24    also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
    5.25      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
    5.26    finally show ?case by simp
     6.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Oct 31 16:54:22 2013 +0100
     6.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Fri Nov 01 18:51:14 2013 +0100
     6.3 @@ -1727,7 +1727,7 @@
     6.4    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))" 
     6.5        by (simp add: nb Let_def split_def isint_Floor isint_neg)
     6.6      have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)
     6.7 -    also have "\<dots> = (?I (?l (Lt a)))" apply (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) by (simp add: Ia cp cnz Let_def split_def diff_minus)
     6.8 +    also have "\<dots> = (?I (?l (Lt a)))" apply (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) by (simp add: Ia cp cnz Let_def split_def)
     6.9      finally have ?case using l by simp}
    6.10    moreover
    6.11    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))" 
    6.12 @@ -1752,13 +1752,13 @@
    6.13    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))" 
    6.14        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    6.15      have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)
    6.16 -    also have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_minus)
    6.17 +    also have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def)
    6.18      finally have ?case using l by simp}
    6.19    moreover
    6.20    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))" 
    6.21        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    6.22      have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)
    6.23 -    also from cn cnz have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac ,arith)
    6.24 +    also from cn cnz have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
    6.25      finally have ?case using l by simp}
    6.26    ultimately show ?case by blast
    6.27  next
    6.28 @@ -1777,13 +1777,13 @@
    6.29    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))" 
    6.30        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    6.31      have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)
    6.32 -    also have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_minus)
    6.33 +    also have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def)
    6.34      finally have ?case using l by simp}
    6.35    moreover
    6.36    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))" 
    6.37        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    6.38      have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)
    6.39 -    also from cn cnz have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac, arith)
    6.40 +    also from cn cnz have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
    6.41      finally have ?case using l by simp}
    6.42    ultimately show ?case by blast
    6.43  next
    6.44 @@ -1802,13 +1802,13 @@
    6.45    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))" 
    6.46        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    6.47      have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)
    6.48 -    also have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_minus)
    6.49 +    also have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def)
    6.50      finally have ?case using l by simp}
    6.51    moreover
    6.52    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))" 
    6.53        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    6.54      have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)
    6.55 -    also from cn cnz have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac, arith)
    6.56 +    also from cn cnz have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
    6.57      finally have ?case using l by simp}
    6.58    ultimately show ?case by blast
    6.59  next
    6.60 @@ -3125,7 +3125,8 @@
    6.61      hence pid: "c*i + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
    6.62      with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + ?fe = j1" by auto
    6.63      hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - ?N i e + real j1" 
    6.64 -      by (simp only: real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps)
    6.65 +      by (simp only: real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff])
    6.66 +        (simp add: algebra_simps)
    6.67      with nob  have ?case by blast }
    6.68    ultimately show ?case by blast
    6.69  next
    6.70 @@ -3148,11 +3149,12 @@
    6.71      hence pid: "c*i + 1 + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
    6.72      with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + 1+ ?fe = j1" by auto
    6.73      hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) + 1= - ?N i e + real j1"
    6.74 -      by (simp only: real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps real_of_one) 
    6.75 +      by (simp only: real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] real_of_one) 
    6.76 +        (simp add: algebra_simps)
    6.77      hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = (- ?N i e + real j1) - 1"
    6.78        by (simp only: algebra_simps)
    6.79          hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - 1 - ?N i e + real j1"
    6.80 -          by (simp only: add_ac diff_minus)
    6.81 +          by (simp add: algebra_simps minus_one [symmetric] del: minus_one)
    6.82      with nob  have ?case by blast }
    6.83    ultimately show ?case by blast
    6.84  next
    6.85 @@ -3477,10 +3479,7 @@
    6.86    qed
    6.87  next
    6.88    case (3 a b) then show ?case
    6.89 -    apply auto
    6.90 -    apply (erule_tac x = "(aa, aaa, ba)" in ballE) apply simp_all
    6.91 -    apply (erule_tac x = "(ab, ac, baa)" in ballE) apply simp_all
    6.92 -    done
    6.93 +    by auto
    6.94  qed (auto simp add: Let_def split_def algebra_simps)
    6.95  
    6.96  lemma real_in_int_intervals: 
    6.97 @@ -3615,7 +3614,7 @@
    6.98        by(simp only: myle[of _ "real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"]) 
    6.99      hence "\<exists> j\<in> {n .. 0}. 0 \<ge> - (real n *x + ?N s - ?N (Floor s) - real j) \<and> - (real n *x + ?N s - ?N (Floor s) - real (j+1)) > 0" by (simp only: th1[rule_format] th2[rule_format])
   6.100      hence "\<exists> j\<in> {n.. 0}. ?I (?p (p,n,s) j)"
   6.101 -      using pns by (simp add: fp_def nn diff_minus add_ac mult_ac
   6.102 +      using pns by (simp add: fp_def nn algebra_simps
   6.103          del: diff_less_0_iff_less diff_le_0_iff_le) 
   6.104      then obtain "j" where j_def: "j\<in> {n .. 0} \<and> ?I (?p (p,n,s) j)" by blast
   6.105      hence "\<exists>x \<in> {?p (p,n,s) j |j. n\<le> j \<and> j \<le> 0 }. ?I x" by auto
   6.106 @@ -4832,7 +4831,7 @@
   6.107    shows "(Ifm bs (E p)) = (\<exists> (i::int). Ifm (real i#bs) (E (And (And (Ge(CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))) (exsplit p))))" (is "?lhs = ?rhs")
   6.108  proof-
   6.109    have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real i)#bs) (exsplit p))"
   6.110 -    by (simp add: myless[of _ "1"] myless[of _ "0"] add_ac diff_minus)
   6.111 +    by (simp add: myless[of _ "1"] myless[of _ "0"] add_ac)
   6.112    also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real i + x) #bs) p)"
   6.113      by (simp only: exsplit[OF qf] add_ac)
   6.114    also have "\<dots> = (\<exists> x. Ifm (x#bs) p)" 
   6.115 @@ -5196,7 +5195,7 @@
   6.116    hence "\<forall> j\<in> set ?js. bound0 (subst0 (C j) ?smq)" 
   6.117      by (auto simp only: subst0_bound0[OF qfmq])
   6.118    hence th: "\<forall> j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
   6.119 -    by (auto simp add: simpfm_bound0)
   6.120 +    by auto
   6.121    from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp 
   6.122    from Bn jsnb have "\<forall> (b,j) \<in> set ?bjs. numbound0 (Add b (C j))"
   6.123      by simp
     7.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Oct 31 16:54:22 2013 +0100
     7.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Nov 01 18:51:14 2013 +0100
     7.3 @@ -1959,7 +1959,7 @@
     7.4        by (simp add: field_simps)
     7.5      have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Eq (CNP 0 a r))" by (simp only: th)
     7.6      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r = 0" 
     7.7 -      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
     7.8 +      by (simp add: r [of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
     7.9      also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) =0 "
    7.10        using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
    7.11      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r =0" 
    7.12 @@ -2041,7 +2041,7 @@
    7.13        by (simp add: field_simps)
    7.14      have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (NEq (CNP 0 a r))" by (simp only: th)
    7.15      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r \<noteq> 0" 
    7.16 -      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
    7.17 +      by (simp add: r [of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
    7.18      also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) \<noteq> 0 "
    7.19        using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
    7.20      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0" 
    7.21 @@ -2106,7 +2106,7 @@
    7.22        by (simp add: field_simps)
    7.23      have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
    7.24      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r < 0" 
    7.25 -      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
    7.26 +      by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
    7.27      also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) < 0"
    7.28        
    7.29        using dc' dc'' mult_less_cancel_left_disj[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
    7.30 @@ -2127,7 +2127,7 @@
    7.31        by (simp add: field_simps)
    7.32      have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
    7.33      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r < 0" 
    7.34 -      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
    7.35 +      by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
    7.36  
    7.37      also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) > 0"
    7.38        
    7.39 @@ -2251,7 +2251,7 @@
    7.40        by (simp add: field_simps)
    7.41      have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
    7.42      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r <= 0" 
    7.43 -      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
    7.44 +      by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
    7.45      also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) <= 0"
    7.46        
    7.47        using dc' dc'' mult_le_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
    7.48 @@ -2272,7 +2272,7 @@
    7.49        by (simp add: field_simps)
    7.50      have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
    7.51      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r <= 0" 
    7.52 -      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
    7.53 +      by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
    7.54  
    7.55      also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) >= 0"
    7.56        
    7.57 @@ -2356,8 +2356,11 @@
    7.58  
    7.59  lemma msubst_I: assumes lp: "islin p" and nc: "isnpoly c" and nd: "isnpoly d"
    7.60    shows "Ifm vs (x#bs) (msubst p ((c,t),(d,s))) = Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) p"
    7.61 -  using lp
    7.62 -by (induct p rule: islin.induct, auto simp add: tmbound0_I[where b="(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) + - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) / 2" and b'=x and bs = bs and vs=vs] bound0_I[where b="(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) + - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) / 2" and b'=x and bs = bs and vs=vs] msubsteq msubstneq msubstlt[OF nc nd] msubstle[OF nc nd])
    7.63 +  using lp by (induct p rule: islin.induct)
    7.64 +    (auto simp add: tmbound0_I
    7.65 +    [where b = "(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) / 2"
    7.66 +      and b' = x and bs = bs and vs = vs]
    7.67 +    msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd])
    7.68  
    7.69  lemma msubst_nb: assumes lp: "islin p" and t: "tmbound0 t" and s: "tmbound0 s"
    7.70    shows "bound0 (msubst p ((c,t),(d,s)))"
    7.71 @@ -2429,7 +2432,7 @@
    7.72    with evaldjf_bound0[of ?Up "(simpfm o (msubst (simpfm p)))"]
    7.73    have "bound0 (evaldjf (simpfm o (msubst (simpfm p))) ?Up)" by blast
    7.74    with mp_nb pp_nb 
    7.75 -  have th1: "bound0 (disj ?mp (disj ?pp (evaldjf (simpfm o (msubst ?q)) ?Up )))" by (simp add: disj_nb)
    7.76 +  have th1: "bound0 (disj ?mp (disj ?pp (evaldjf (simpfm o (msubst ?q)) ?Up )))" by simp
    7.77    from decr0_qf[OF th1] have thqf: "qfree (ferrack p)" by (simp add: ferrack_def Let_def)
    7.78    have "?lhs \<longleftrightarrow> (\<exists>x. Ifm vs (x#bs) ?q)" by simp
    7.79    also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> (\<exists>(c, t)\<in>set ?U. \<exists>(d, s)\<in>set ?U. ?I (msubst (simpfm p) ((c, t), d, s)))" using fr_eq_msubst[OF lq, of vs bs x] by simp
    7.80 @@ -2612,7 +2615,7 @@
    7.81  lemma msubst2_nb: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and lp: "islin p" and tnb: "tmbound0 t"
    7.82    shows "bound0 (msubst2 p c t)"
    7.83  using lp tnb
    7.84 -by (simp add: msubst2_def msubstneg_nb msubstpos_nb conj_nb disj_nb lt_nb simpfm_bound0)
    7.85 +by (simp add: msubst2_def msubstneg_nb msubstpos_nb lt_nb simpfm_bound0)
    7.86  
    7.87  lemma mult_minus2_left: "-2 * (x::'a::comm_ring_1) = - (2 * x)"
    7.88    by simp
    7.89 @@ -2666,8 +2669,8 @@
    7.90          using H(3) by (auto simp add: msubst2_def lt[OF stupid(1)]  lt[OF stupid(2)] zero_less_mult_iff mult_less_0_iff)
    7.91        from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn'
    7.92        have "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p"
    7.93 -        apply (simp add: add_divide_distrib mult_minus2_left)
    7.94 -        by (simp add: mult_commute)}
    7.95 +        by (simp add: add_divide_distrib diff_divide_distrib mult_minus2_left mult_commute)
    7.96 +    }
    7.97      moreover
    7.98      {fix c t d s assume H: "(c,t) \<in> set (uset p)" "(d,s) \<in> set (uset p)" 
    7.99        "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p"
   7.100 @@ -2675,7 +2678,9 @@
   7.101        hence nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)" "\<lparr>(C (-2, 1) *\<^sub>p c*\<^sub>p d)\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
   7.102          using H(3,4) by (simp_all add: polymul_norm n2)
   7.103        from msubst2[OF lp nn, of x bs ] H(3,4,5) 
   7.104 -      have "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))" apply (simp add: add_divide_distrib mult_minus2_left) by (simp add: mult_commute)}
   7.105 +      have "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))"
   7.106 +        by (simp add: diff_divide_distrib add_divide_distrib mult_minus2_left mult_commute)
   7.107 +    }
   7.108      ultimately show ?thesis by blast
   7.109    qed
   7.110    from fr_eq2[OF lp, of vs bs x] show ?thesis
     8.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Thu Oct 31 16:54:22 2013 +0100
     8.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Fri Nov 01 18:51:14 2013 +0100
     8.3 @@ -419,7 +419,7 @@
     8.4  
     8.5  lemma (in comm_ring_1) poly_add_minus_mult_eq:
     8.6    "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
     8.7 -  by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult distrib_left)
     8.8 +  by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult algebra_simps)
     8.9  
    8.10  subclass (in idom_char_0) comm_ring_1 ..
    8.11  
    8.12 @@ -445,10 +445,7 @@
    8.13  lemma (in comm_ring_1) poly_prime_eq_zero[simp]: "poly [a,1] \<noteq> poly []"
    8.14    apply (simp add: fun_eq)
    8.15    apply (rule_tac x = "minus one a" in exI)
    8.16 -  apply (unfold diff_minus)
    8.17 -  apply (subst add_commute)
    8.18 -  apply (subst add_assoc)
    8.19 -  apply simp
    8.20 +  apply (simp add: add_commute [of a])
    8.21    done
    8.22  
    8.23  lemma (in idom) poly_exp_prime_eq_zero: "poly ([a, 1] %^ n) \<noteq> poly []"
    8.24 @@ -639,7 +636,7 @@
    8.25    have "[- a, 1] %^ n divides mulexp n [- a, 1] q"
    8.26    proof (rule dividesI)
    8.27      show "poly (mulexp n [- a, 1] q) = poly ([- a, 1] %^ n *** q)"
    8.28 -      by (induct n) (simp_all add: poly_add poly_cmult poly_mult distrib_left mult_ac)
    8.29 +      by (induct n) (simp_all add: poly_add poly_cmult poly_mult algebra_simps)
    8.30    qed
    8.31    moreover have "\<not> [- a, 1] %^ Suc n divides mulexp n [- a, 1] q"
    8.32    proof
    8.33 @@ -873,7 +870,7 @@
    8.34  proof
    8.35    assume eq: ?lhs
    8.36    hence "\<And>x. poly ((c#cs) +++ -- (d#ds)) x = 0"
    8.37 -    by (simp only: poly_minus poly_add algebra_simps) simp
    8.38 +    by (simp only: poly_minus poly_add algebra_simps) (simp add: algebra_simps)
    8.39    hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add: fun_eq_iff)
    8.40    hence "c = d \<and> list_all (\<lambda>x. x=0) ((cs +++ -- ds))"
    8.41      unfolding poly_zero by (simp add: poly_minus_def algebra_simps)
     9.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Oct 31 16:54:22 2013 +0100
     9.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Fri Nov 01 18:51:14 2013 +0100
     9.3 @@ -266,12 +266,13 @@
     9.4          by (simp add: x y th Nadd_def normNum_def INum_def split_def) }
     9.5      moreover {
     9.6        assume z: "a * b' + b * a' \<noteq> 0"
     9.7 -      let ?g = "gcd (a * b' + b * a') (b*b')"
     9.8 +      let ?g = "gcd (a * b' + b * a') (b * b')"
     9.9        have gz: "?g \<noteq> 0" using z by simp
    9.10        have ?thesis using aa' bb' z gz
    9.11          of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]
    9.12          of_int_div[where ?'a = 'a, OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
    9.13 -        by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib) }
    9.14 +        by (simp add: x y Nadd_def INum_def normNum_def Let_def) (simp add: field_simps)
    9.15 +    }
    9.16      ultimately have ?thesis using aa' bb'
    9.17        by (simp add: x y Nadd_def INum_def normNum_def Let_def) }
    9.18    ultimately show ?thesis by blast
    10.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Thu Oct 31 16:54:22 2013 +0100
    10.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri Nov 01 18:51:14 2013 +0100
    10.3 @@ -34,7 +34,7 @@
    10.4               @{thm "divide_zero"}, 
    10.5               @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"}, 
    10.6               @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
    10.7 -             @{thm "diff_minus"}, @{thm "minus_divide_left"}]
    10.8 +             @{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}]
    10.9  val comp_ths = ths @ comp_arith @ @{thms simp_thms};
   10.10  
   10.11  
    11.1 --- a/src/HOL/Deriv.thy	Thu Oct 31 16:54:22 2013 +0100
    11.2 +++ b/src/HOL/Deriv.thy	Fri Nov 01 18:51:14 2013 +0100
    11.3 @@ -98,7 +98,7 @@
    11.4  
    11.5  lemma FDERIV_diff[simp, FDERIV_intros]:
    11.6    "(f has_derivative f') F \<Longrightarrow> (g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f x - g x) has_derivative (\<lambda>x. f' x - g' x)) F"
    11.7 -  by (simp only: diff_minus FDERIV_add FDERIV_minus)
    11.8 +  by (simp only: diff_conv_add_uminus FDERIV_add FDERIV_minus)
    11.9  
   11.10  abbreviation
   11.11    -- {* Frechet derivative: D is derivative of function f at x within s *}
   11.12 @@ -718,13 +718,13 @@
   11.13        ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
   11.14  apply (rule iffI)
   11.15  apply (drule_tac k="- a" in LIM_offset)
   11.16 -apply (simp add: diff_minus)
   11.17 +apply simp
   11.18  apply (drule_tac k="a" in LIM_offset)
   11.19  apply (simp add: add_commute)
   11.20  done
   11.21  
   11.22  lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) --x --> D"
   11.23 -  by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)
   11.24 +  by (simp add: deriv_def DERIV_LIM_iff)
   11.25  
   11.26  lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
   11.27      DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
   11.28 @@ -758,8 +758,7 @@
   11.29      let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
   11.30      show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
   11.31      show "isCont ?g x" using der
   11.32 -      by (simp add: isCont_iff DERIV_iff diff_minus
   11.33 -               cong: LIM_equal [rule_format])
   11.34 +      by (simp add: isCont_iff DERIV_iff cong: LIM_equal [rule_format])
   11.35      show "?g x = l" by simp
   11.36    qed
   11.37  next
   11.38 @@ -787,7 +786,7 @@
   11.39  proof -
   11.40    from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]]
   11.41    have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
   11.42 -    by (simp add: diff_minus)
   11.43 +    by simp
   11.44    then obtain s
   11.45          where s:   "0 < s"
   11.46            and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l"
   11.47 @@ -798,8 +797,7 @@
   11.48      fix h::real
   11.49      assume "0 < h" "h < s"
   11.50      with all [of h] show "f x < f (x+h)"
   11.51 -    proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
   11.52 -    split add: split_if_asm)
   11.53 +    proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
   11.54        assume "~ (f (x+h) - f x) / h < l" and h: "0 < h"
   11.55        with l
   11.56        have "0 < (f (x+h) - f x) / h" by arith
   11.57 @@ -817,7 +815,7 @@
   11.58  proof -
   11.59    from l der [THEN DERIV_D, THEN LIM_D [where r = "-l"]]
   11.60    have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l)"
   11.61 -    by (simp add: diff_minus)
   11.62 +    by simp
   11.63    then obtain s
   11.64          where s:   "0 < s"
   11.65            and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l"
   11.66 @@ -828,8 +826,7 @@
   11.67      fix h::real
   11.68      assume "0 < h" "h < s"
   11.69      with all [of "-h"] show "f x < f (x-h)"
   11.70 -    proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
   11.71 -    split add: split_if_asm)
   11.72 +    proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
   11.73        assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
   11.74        with l
   11.75        have "0 < (f (x-h) - f x) / h" by arith
   11.76 @@ -1131,7 +1128,7 @@
   11.77  apply (rule linorder_cases [of a b], auto)
   11.78  apply (drule_tac [!] f = f in MVT)
   11.79  apply (auto dest: DERIV_isCont DERIV_unique simp add: differentiable_def)
   11.80 -apply (auto dest: DERIV_unique simp add: ring_distribs diff_minus)
   11.81 +apply (auto dest: DERIV_unique simp add: ring_distribs)
   11.82  done
   11.83  
   11.84  lemma DERIV_const_ratio_const2:
    12.1 --- a/src/HOL/Divides.thy	Thu Oct 31 16:54:22 2013 +0100
    12.2 +++ b/src/HOL/Divides.thy	Fri Nov 01 18:51:14 2013 +0100
    12.3 @@ -439,24 +439,23 @@
    12.4  
    12.5  text {* Subtraction respects modular equivalence. *}
    12.6  
    12.7 -lemma mod_diff_left_eq: "(a - b) mod c = (a mod c - b) mod c"
    12.8 -  unfolding diff_minus
    12.9 -  by (intro mod_add_cong mod_minus_cong) simp_all
   12.10 -
   12.11 -lemma mod_diff_right_eq: "(a - b) mod c = (a - b mod c) mod c"
   12.12 -  unfolding diff_minus
   12.13 -  by (intro mod_add_cong mod_minus_cong) simp_all
   12.14 -
   12.15 -lemma mod_diff_eq: "(a - b) mod c = (a mod c - b mod c) mod c"
   12.16 -  unfolding diff_minus
   12.17 -  by (intro mod_add_cong mod_minus_cong) simp_all
   12.18 +lemma mod_diff_left_eq:
   12.19 +  "(a - b) mod c = (a mod c - b) mod c"
   12.20 +  using mod_add_cong [of a c "a mod c" "- b" "- b"] by simp
   12.21 +
   12.22 +lemma mod_diff_right_eq:
   12.23 +  "(a - b) mod c = (a - b mod c) mod c"
   12.24 +  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
   12.25 +
   12.26 +lemma mod_diff_eq:
   12.27 +  "(a - b) mod c = (a mod c - b mod c) mod c"
   12.28 +  using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
   12.29  
   12.30  lemma mod_diff_cong:
   12.31    assumes "a mod c = a' mod c"
   12.32    assumes "b mod c = b' mod c"
   12.33    shows "(a - b) mod c = (a' - b') mod c"
   12.34 -  unfolding diff_minus using assms
   12.35 -  by (intro mod_add_cong mod_minus_cong)
   12.36 +  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] by simp
   12.37  
   12.38  lemma dvd_neg_div: "y dvd x \<Longrightarrow> -x div y = - (x div y)"
   12.39  apply (case_tac "y = 0") apply simp
   12.40 @@ -502,10 +501,7 @@
   12.41  
   12.42  lemma minus_mod_self1 [simp]: 
   12.43    "(b - a) mod b = - a mod b"
   12.44 -proof -
   12.45 -  have "b - a = - a + b" by (simp add: diff_minus add.commute)
   12.46 -  then show ?thesis by simp
   12.47 -qed
   12.48 +  using mod_add_self2 [of "- a" b] by simp
   12.49  
   12.50  end
   12.51  
   12.52 @@ -1749,7 +1745,7 @@
   12.53    val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
   12.54  
   12.55    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
   12.56 -    (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
   12.57 +    (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms add_ac}))
   12.58  )
   12.59  *}
   12.60  
    13.1 --- a/src/HOL/Fields.thy	Thu Oct 31 16:54:22 2013 +0100
    13.2 +++ b/src/HOL/Fields.thy	Fri Nov 01 18:51:14 2013 +0100
    13.3 @@ -156,7 +156,7 @@
    13.4    by (simp add: divide_inverse)
    13.5  
    13.6  lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
    13.7 -  by (simp add: diff_minus add_divide_distrib)
    13.8 +  using add_divide_distrib [of a "- b" c] by simp
    13.9  
   13.10  lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
   13.11  proof -
   13.12 @@ -845,7 +845,7 @@
   13.13    fix x y :: 'a
   13.14    from less_add_one show "\<exists>y. x < y" .. 
   13.15    from less_add_one have "x + (- 1) < (x + 1) + (- 1)" by (rule add_strict_right_mono)
   13.16 -  then have "x - 1 < x + 1 - 1" by (simp only: diff_minus [symmetric])
   13.17 +  then have "x - 1 < x + 1 - 1" by simp
   13.18    then have "x - 1 < x" by (simp add: algebra_simps)
   13.19    then show "\<exists>y. y < x" ..
   13.20    show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
    14.1 --- a/src/HOL/Groups.thy	Thu Oct 31 16:54:22 2013 +0100
    14.2 +++ b/src/HOL/Groups.thy	Fri Nov 01 18:51:14 2013 +0100
    14.3 @@ -321,9 +321,13 @@
    14.4  
    14.5  class group_add = minus + uminus + monoid_add +
    14.6    assumes left_minus [simp]: "- a + a = 0"
    14.7 -  assumes diff_minus: "a - b = a + (- b)"
    14.8 +  assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"
    14.9  begin
   14.10  
   14.11 +lemma diff_conv_add_uminus:
   14.12 +  "a - b = a + (- b)"
   14.13 +  by simp
   14.14 +
   14.15  lemma minus_unique:
   14.16    assumes "a + b = 0" shows "- a = b"
   14.17  proof -
   14.18 @@ -332,8 +336,6 @@
   14.19    finally show ?thesis .
   14.20  qed
   14.21  
   14.22 -lemmas equals_zero_I = minus_unique (* legacy name *)
   14.23 -
   14.24  lemma minus_zero [simp]: "- 0 = 0"
   14.25  proof -
   14.26    have "0 + 0 = 0" by (rule add_0_right)
   14.27 @@ -346,13 +348,17 @@
   14.28    thus "- (- a) = a" by (rule minus_unique)
   14.29  qed
   14.30  
   14.31 -lemma right_minus [simp]: "a + - a = 0"
   14.32 +lemma right_minus: "a + - a = 0"
   14.33  proof -
   14.34    have "a + - a = - (- a) + - a" by simp
   14.35    also have "\<dots> = 0" by (rule left_minus)
   14.36    finally show ?thesis .
   14.37  qed
   14.38  
   14.39 +lemma diff_self [simp]:
   14.40 +  "a - a = 0"
   14.41 +  using right_minus [of a] by simp
   14.42 +
   14.43  subclass cancel_semigroup_add
   14.44  proof
   14.45    fix a b c :: 'a
   14.46 @@ -367,41 +373,57 @@
   14.47    then show "b = c" unfolding add_assoc by simp
   14.48  qed
   14.49  
   14.50 -lemma minus_add_cancel: "- a + (a + b) = b"
   14.51 -by (simp add: add_assoc [symmetric])
   14.52 +lemma minus_add_cancel [simp]:
   14.53 +  "- a + (a + b) = b"
   14.54 +  by (simp add: add_assoc [symmetric])
   14.55 +
   14.56 +lemma add_minus_cancel [simp]:
   14.57 +  "a + (- a + b) = b"
   14.58 +  by (simp add: add_assoc [symmetric])
   14.59  
   14.60 -lemma add_minus_cancel: "a + (- a + b) = b"
   14.61 -by (simp add: add_assoc [symmetric])
   14.62 +lemma diff_add_cancel [simp]:
   14.63 +  "a - b + b = a"
   14.64 +  by (simp only: diff_conv_add_uminus add_assoc) simp
   14.65  
   14.66 -lemma minus_add: "- (a + b) = - b + - a"
   14.67 +lemma add_diff_cancel [simp]:
   14.68 +  "a + b - b = a"
   14.69 +  by (simp only: diff_conv_add_uminus add_assoc) simp
   14.70 +
   14.71 +lemma minus_add:
   14.72 +  "- (a + b) = - b + - a"
   14.73  proof -
   14.74    have "(a + b) + (- b + - a) = 0"
   14.75 -    by (simp add: add_assoc add_minus_cancel)
   14.76 -  thus "- (a + b) = - b + - a"
   14.77 +    by (simp only: add_assoc add_minus_cancel) simp
   14.78 +  then show "- (a + b) = - b + - a"
   14.79      by (rule minus_unique)
   14.80  qed
   14.81  
   14.82 -lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
   14.83 +lemma right_minus_eq [simp]:
   14.84 +  "a - b = 0 \<longleftrightarrow> a = b"
   14.85  proof
   14.86    assume "a - b = 0"
   14.87 -  have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
   14.88 +  have "a = (a - b) + b" by (simp add: add_assoc)
   14.89    also have "\<dots> = b" using `a - b = 0` by simp
   14.90    finally show "a = b" .
   14.91  next
   14.92 -  assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
   14.93 +  assume "a = b" thus "a - b = 0" by simp
   14.94  qed
   14.95  
   14.96 -lemma diff_self [simp]: "a - a = 0"
   14.97 -by (simp add: diff_minus)
   14.98 +lemma eq_iff_diff_eq_0:
   14.99 +  "a = b \<longleftrightarrow> a - b = 0"
  14.100 +  by (fact right_minus_eq [symmetric])
  14.101  
  14.102 -lemma diff_0 [simp]: "0 - a = - a"
  14.103 -by (simp add: diff_minus)
  14.104 +lemma diff_0 [simp]:
  14.105 +  "0 - a = - a"
  14.106 +  by (simp only: diff_conv_add_uminus add_0_left)
  14.107  
  14.108 -lemma diff_0_right [simp]: "a - 0 = a" 
  14.109 -by (simp add: diff_minus)
  14.110 +lemma diff_0_right [simp]:
  14.111 +  "a - 0 = a" 
  14.112 +  by (simp only: diff_conv_add_uminus minus_zero add_0_right)
  14.113  
  14.114 -lemma diff_minus_eq_add [simp]: "a - - b = a + b"
  14.115 -by (simp add: diff_minus)
  14.116 +lemma diff_minus_eq_add [simp]:
  14.117 +  "a - - b = a + b"
  14.118 +  by (simp only: diff_conv_add_uminus minus_minus)
  14.119  
  14.120  lemma neg_equal_iff_equal [simp]:
  14.121    "- a = - b \<longleftrightarrow> a = b" 
  14.122 @@ -416,11 +438,11 @@
  14.123  
  14.124  lemma neg_equal_0_iff_equal [simp]:
  14.125    "- a = 0 \<longleftrightarrow> a = 0"
  14.126 -by (subst neg_equal_iff_equal [symmetric], simp)
  14.127 +  by (subst neg_equal_iff_equal [symmetric]) simp
  14.128  
  14.129  lemma neg_0_equal_iff_equal [simp]:
  14.130    "0 = - a \<longleftrightarrow> 0 = a"
  14.131 -by (subst neg_equal_iff_equal [symmetric], simp)
  14.132 +  by (subst neg_equal_iff_equal [symmetric]) simp
  14.133  
  14.134  text{*The next two equations can make the simplifier loop!*}
  14.135  
  14.136 @@ -438,15 +460,8 @@
  14.137    thus ?thesis by (simp add: eq_commute)
  14.138  qed
  14.139  
  14.140 -lemma diff_add_cancel: "a - b + b = a"
  14.141 -by (simp add: diff_minus add_assoc)
  14.142 -
  14.143 -lemma add_diff_cancel: "a + b - b = a"
  14.144 -by (simp add: diff_minus add_assoc)
  14.145 -
  14.146 -declare diff_minus[symmetric, algebra_simps, field_simps]
  14.147 -
  14.148 -lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
  14.149 +lemma eq_neg_iff_add_eq_0:
  14.150 +  "a = - b \<longleftrightarrow> a + b = 0"
  14.151  proof
  14.152    assume "a = - b" then show "a + b = 0" by simp
  14.153  next
  14.154 @@ -456,72 +471,88 @@
  14.155    ultimately show "a = - b" by simp
  14.156  qed
  14.157  
  14.158 -lemma add_eq_0_iff: "x + y = 0 \<longleftrightarrow> y = - x"
  14.159 -  unfolding eq_neg_iff_add_eq_0 [symmetric]
  14.160 -  by (rule equation_minus_iff)
  14.161 +lemma add_eq_0_iff2:
  14.162 +  "a + b = 0 \<longleftrightarrow> a = - b"
  14.163 +  by (fact eq_neg_iff_add_eq_0 [symmetric])
  14.164 +
  14.165 +lemma neg_eq_iff_add_eq_0:
  14.166 +  "- a = b \<longleftrightarrow> a + b = 0"
  14.167 +  by (auto simp add: add_eq_0_iff2)
  14.168  
  14.169 -lemma minus_diff_eq [simp]: "- (a - b) = b - a"
  14.170 -  by (simp add: diff_minus minus_add)
  14.171 +lemma add_eq_0_iff:
  14.172 +  "a + b = 0 \<longleftrightarrow> b = - a"
  14.173 +  by (auto simp add: neg_eq_iff_add_eq_0 [symmetric])
  14.174  
  14.175 -lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
  14.176 -  by (simp add: diff_minus add_assoc)
  14.177 +lemma minus_diff_eq [simp]:
  14.178 +  "- (a - b) = b - a"
  14.179 +  by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add_assoc minus_add_cancel) simp
  14.180  
  14.181 -lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
  14.182 -  by (auto simp add: diff_minus add_assoc)
  14.183 +lemma add_diff_eq [algebra_simps, field_simps]:
  14.184 +  "a + (b - c) = (a + b) - c"
  14.185 +  by (simp only: diff_conv_add_uminus add_assoc)
  14.186  
  14.187 -lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
  14.188 -  by (auto simp add: diff_minus add_assoc)
  14.189 +lemma diff_add_eq_diff_diff_swap:
  14.190 +  "a - (b + c) = a - c - b"
  14.191 +  by (simp only: diff_conv_add_uminus add_assoc minus_add)
  14.192  
  14.193 -lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
  14.194 -  by (simp add: diff_minus minus_add add_assoc)
  14.195 +lemma diff_eq_eq [algebra_simps, field_simps]:
  14.196 +  "a - b = c \<longleftrightarrow> a = c + b"
  14.197 +  by auto
  14.198  
  14.199 -lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
  14.200 -  by (fact right_minus_eq [symmetric])
  14.201 +lemma eq_diff_eq [algebra_simps, field_simps]:
  14.202 +  "a = c - b \<longleftrightarrow> a + b = c"
  14.203 +  by auto
  14.204 +
  14.205 +lemma diff_diff_eq2 [algebra_simps, field_simps]:
  14.206 +  "a - (b - c) = (a + c) - b"
  14.207 +  by (simp only: diff_conv_add_uminus add_assoc) simp
  14.208  
  14.209  lemma diff_eq_diff_eq:
  14.210    "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
  14.211 -  by (simp add: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
  14.212 +  by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
  14.213  
  14.214  end
  14.215  
  14.216  class ab_group_add = minus + uminus + comm_monoid_add +
  14.217    assumes ab_left_minus: "- a + a = 0"
  14.218 -  assumes ab_diff_minus: "a - b = a + (- b)"
  14.219 +  assumes ab_add_uminus_conv_diff: "a - b = a + (- b)"
  14.220  begin
  14.221  
  14.222  subclass group_add
  14.223 -  proof qed (simp_all add: ab_left_minus ab_diff_minus)
  14.224 +  proof qed (simp_all add: ab_left_minus ab_add_uminus_conv_diff)
  14.225  
  14.226  subclass cancel_comm_monoid_add
  14.227  proof
  14.228    fix a b c :: 'a
  14.229    assume "a + b = a + c"
  14.230    then have "- a + a + b = - a + a + c"
  14.231 -    unfolding add_assoc by simp
  14.232 +    by (simp only: add_assoc)
  14.233    then show "b = c" by simp
  14.234  qed
  14.235  
  14.236 -lemma uminus_add_conv_diff[algebra_simps, field_simps]:
  14.237 +lemma uminus_add_conv_diff [simp]:
  14.238    "- a + b = b - a"
  14.239 -by (simp add:diff_minus add_commute)
  14.240 +  by (simp add: add_commute)
  14.241  
  14.242  lemma minus_add_distrib [simp]:
  14.243    "- (a + b) = - a + - b"
  14.244 -by (rule minus_unique) (simp add: add_ac)
  14.245 +  by (simp add: algebra_simps)
  14.246  
  14.247 -lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
  14.248 -by (simp add: diff_minus add_ac)
  14.249 -
  14.250 -lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)"
  14.251 -by (simp add: diff_minus add_ac)
  14.252 +lemma diff_add_eq [algebra_simps, field_simps]:
  14.253 +  "(a - b) + c = (a + c) - b"
  14.254 +  by (simp add: algebra_simps)
  14.255  
  14.256 -(* FIXME: duplicates right_minus_eq from class group_add *)
  14.257 -(* but only this one is declared as a simp rule. *)
  14.258 -lemma diff_eq_0_iff_eq [simp]: "a - b = 0 \<longleftrightarrow> a = b"
  14.259 -  by (rule right_minus_eq)
  14.260 +lemma diff_diff_eq [algebra_simps, field_simps]:
  14.261 +  "(a - b) - c = a - (b + c)"
  14.262 +  by (simp add: algebra_simps)
  14.263  
  14.264 -lemma add_diff_cancel_left: "(c + a) - (c + b) = a - b"
  14.265 -  by (simp add: diff_minus add_ac)
  14.266 +lemma diff_add_eq_diff_diff:
  14.267 +  "a - (b + c) = a - b - c"
  14.268 +  using diff_add_eq_diff_diff_swap [of a c b] by (simp add: add.commute)
  14.269 +
  14.270 +lemma add_diff_cancel_left [simp]:
  14.271 +  "(c + a) - (c + b) = a - b"
  14.272 +  by (simp add: algebra_simps)
  14.273  
  14.274  end
  14.275  
  14.276 @@ -622,19 +653,19 @@
  14.277  
  14.278  lemma add_less_cancel_left [simp]:
  14.279    "c + a < c + b \<longleftrightarrow> a < b"
  14.280 -by (blast intro: add_less_imp_less_left add_strict_left_mono) 
  14.281 +  by (blast intro: add_less_imp_less_left add_strict_left_mono) 
  14.282  
  14.283  lemma add_less_cancel_right [simp]:
  14.284    "a + c < b + c \<longleftrightarrow> a < b"
  14.285 -by (blast intro: add_less_imp_less_right add_strict_right_mono)
  14.286 +  by (blast intro: add_less_imp_less_right add_strict_right_mono)
  14.287  
  14.288  lemma add_le_cancel_left [simp]:
  14.289    "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
  14.290 -by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
  14.291 +  by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
  14.292  
  14.293  lemma add_le_cancel_right [simp]:
  14.294    "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
  14.295 -by (simp add: add_commute [of a c] add_commute [of b c])
  14.296 +  by (simp add: add_commute [of a c] add_commute [of b c])
  14.297  
  14.298  lemma add_le_imp_le_right:
  14.299    "a + c \<le> b + c \<Longrightarrow> a \<le> b"
  14.300 @@ -806,6 +837,22 @@
  14.301    then show "x + y = 0" by simp
  14.302  qed
  14.303  
  14.304 +lemma add_increasing:
  14.305 +  "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
  14.306 +  by (insert add_mono [of 0 a b c], simp)
  14.307 +
  14.308 +lemma add_increasing2:
  14.309 +  "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
  14.310 +  by (simp add: add_increasing add_commute [of a])
  14.311 +
  14.312 +lemma add_strict_increasing:
  14.313 +  "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
  14.314 +  by (insert add_less_le_mono [of 0 a b c], simp)
  14.315 +
  14.316 +lemma add_strict_increasing2:
  14.317 +  "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  14.318 +  by (insert add_le_less_mono [of 0 a b c], simp)
  14.319 +
  14.320  end
  14.321  
  14.322  class ordered_ab_group_add =
  14.323 @@ -825,21 +872,53 @@
  14.324  
  14.325  subclass ordered_comm_monoid_add ..
  14.326  
  14.327 +lemma add_less_same_cancel1 [simp]:
  14.328 +  "b + a < b \<longleftrightarrow> a < 0"
  14.329 +  using add_less_cancel_left [of _ _ 0] by simp
  14.330 +
  14.331 +lemma add_less_same_cancel2 [simp]:
  14.332 +  "a + b < b \<longleftrightarrow> a < 0"
  14.333 +  using add_less_cancel_right [of _ _ 0] by simp
  14.334 +
  14.335 +lemma less_add_same_cancel1 [simp]:
  14.336 +  "a < a + b \<longleftrightarrow> 0 < b"
  14.337 +  using add_less_cancel_left [of _ 0] by simp
  14.338 +
  14.339 +lemma less_add_same_cancel2 [simp]:
  14.340 +  "a < b + a \<longleftrightarrow> 0 < b"
  14.341 +  using add_less_cancel_right [of 0] by simp
  14.342 +
  14.343 +lemma add_le_same_cancel1 [simp]:
  14.344 +  "b + a \<le> b \<longleftrightarrow> a \<le> 0"
  14.345 +  using add_le_cancel_left [of _ _ 0] by simp
  14.346 +
  14.347 +lemma add_le_same_cancel2 [simp]:
  14.348 +  "a + b \<le> b \<longleftrightarrow> a \<le> 0"
  14.349 +  using add_le_cancel_right [of _ _ 0] by simp
  14.350 +
  14.351 +lemma le_add_same_cancel1 [simp]:
  14.352 +  "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
  14.353 +  using add_le_cancel_left [of _ 0] by simp
  14.354 +
  14.355 +lemma le_add_same_cancel2 [simp]:
  14.356 +  "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
  14.357 +  using add_le_cancel_right [of 0] by simp
  14.358 +
  14.359  lemma max_diff_distrib_left:
  14.360    shows "max x y - z = max (x - z) (y - z)"
  14.361 -by (simp add: diff_minus, rule max_add_distrib_left) 
  14.362 +  using max_add_distrib_left [of x y "- z"] by simp
  14.363  
  14.364  lemma min_diff_distrib_left:
  14.365    shows "min x y - z = min (x - z) (y - z)"
  14.366 -by (simp add: diff_minus, rule min_add_distrib_left) 
  14.367 +  using min_add_distrib_left [of x y "- z"] by simp
  14.368  
  14.369  lemma le_imp_neg_le:
  14.370    assumes "a \<le> b" shows "-b \<le> -a"
  14.371  proof -
  14.372    have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono) 
  14.373 -  hence "0 \<le> -a+b" by simp
  14.374 -  hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
  14.375 -  thus ?thesis by (simp add: add_assoc)
  14.376 +  then have "0 \<le> -a+b" by simp
  14.377 +  then have "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
  14.378 +  then show ?thesis by (simp add: algebra_simps)
  14.379  qed
  14.380  
  14.381  lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
  14.382 @@ -899,30 +978,32 @@
  14.383  lemma diff_less_0_iff_less [simp]:
  14.384    "a - b < 0 \<longleftrightarrow> a < b"
  14.385  proof -
  14.386 -  have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
  14.387 +  have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by simp
  14.388    also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
  14.389    finally show ?thesis .
  14.390  qed
  14.391  
  14.392  lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
  14.393  
  14.394 -lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
  14.395 +lemma diff_less_eq [algebra_simps, field_simps]:
  14.396 +  "a - b < c \<longleftrightarrow> a < c + b"
  14.397  apply (subst less_iff_diff_less_0 [of a])
  14.398  apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
  14.399 -apply (simp add: diff_minus add_ac)
  14.400 +apply (simp add: algebra_simps)
  14.401  done
  14.402  
  14.403 -lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"
  14.404 +lemma less_diff_eq[algebra_simps, field_simps]:
  14.405 +  "a < c - b \<longleftrightarrow> a + b < c"
  14.406  apply (subst less_iff_diff_less_0 [of "a + b"])
  14.407  apply (subst less_iff_diff_less_0 [of a])
  14.408 -apply (simp add: diff_minus add_ac)
  14.409 +apply (simp add: algebra_simps)
  14.410  done
  14.411  
  14.412  lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
  14.413 -by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
  14.414 +by (auto simp add: le_less diff_less_eq )
  14.415  
  14.416  lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
  14.417 -by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
  14.418 +by (auto simp add: le_less less_diff_eq)
  14.419  
  14.420  lemma diff_le_0_iff_le [simp]:
  14.421    "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
  14.422 @@ -1118,21 +1199,11 @@
  14.423  
  14.424  lemma le_minus_self_iff:
  14.425    "a \<le> - a \<longleftrightarrow> a \<le> 0"
  14.426 -proof -
  14.427 -  from add_le_cancel_left [of "- a" "a + a" 0]
  14.428 -  have "a \<le> - a \<longleftrightarrow> a + a \<le> 0" 
  14.429 -    by (simp add: add_assoc [symmetric])
  14.430 -  thus ?thesis by simp
  14.431 -qed
  14.432 +  by (fact less_eq_neg_nonpos)
  14.433  
  14.434  lemma minus_le_self_iff:
  14.435    "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  14.436 -proof -
  14.437 -  from add_le_cancel_left [of "- a" 0 "a + a"]
  14.438 -  have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
  14.439 -    by (simp add: add_assoc [symmetric])
  14.440 -  thus ?thesis by simp
  14.441 -qed
  14.442 +  by (fact neg_less_eq_nonneg)
  14.443  
  14.444  lemma minus_max_eq_min:
  14.445    "- max x y = min (-x) (-y)"
  14.446 @@ -1144,27 +1215,6 @@
  14.447  
  14.448  end
  14.449  
  14.450 -context ordered_comm_monoid_add
  14.451 -begin
  14.452 -
  14.453 -lemma add_increasing:
  14.454 -  "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
  14.455 -  by (insert add_mono [of 0 a b c], simp)
  14.456 -
  14.457 -lemma add_increasing2:
  14.458 -  "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
  14.459 -  by (simp add: add_increasing add_commute [of a])
  14.460 -
  14.461 -lemma add_strict_increasing:
  14.462 -  "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
  14.463 -  by (insert add_less_le_mono [of 0 a b c], simp)
  14.464 -
  14.465 -lemma add_strict_increasing2:
  14.466 -  "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  14.467 -  by (insert add_le_less_mono [of 0 a b c], simp)
  14.468 -
  14.469 -end
  14.470 -
  14.471  class abs =
  14.472    fixes abs :: "'a \<Rightarrow> 'a"
  14.473  begin
  14.474 @@ -1299,7 +1349,7 @@
  14.475  lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  14.476  proof -
  14.477    have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  14.478 -    by (simp add: algebra_simps add_diff_cancel)
  14.479 +    by (simp add: algebra_simps)
  14.480    then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  14.481      by (simp add: abs_triangle_ineq)
  14.482    then show ?thesis
  14.483 @@ -1314,14 +1364,14 @@
  14.484  
  14.485  lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  14.486  proof -
  14.487 -  have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
  14.488 +  have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (simp add: algebra_simps)
  14.489    also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
  14.490    finally show ?thesis by simp
  14.491  qed
  14.492  
  14.493  lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  14.494  proof -
  14.495 -  have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
  14.496 +  have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: algebra_simps)
  14.497    also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
  14.498    finally show ?thesis .
  14.499  qed
  14.500 @@ -1362,10 +1412,5 @@
  14.501  code_identifier
  14.502    code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  14.503  
  14.504 -
  14.505 -text {* Legacy *}
  14.506 -
  14.507 -lemmas diff_def = diff_minus
  14.508 -
  14.509  end
  14.510  
    15.1 --- a/src/HOL/Hahn_Banach/Vector_Space.thy	Thu Oct 31 16:54:22 2013 +0100
    15.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Fri Nov 01 18:51:14 2013 +0100
    15.3 @@ -112,7 +112,7 @@
    15.4  proof -
    15.5    assume x: "x \<in> V"
    15.6    have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
    15.7 -    by (simp add: diff_minus)
    15.8 +    by simp
    15.9    also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
   15.10      by (rule add_mult_distrib2)
   15.11    also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
    16.1 --- a/src/HOL/Int.thy	Thu Oct 31 16:54:22 2013 +0100
    16.2 +++ b/src/HOL/Int.thy	Fri Nov 01 18:51:14 2013 +0100
    16.3 @@ -220,7 +220,7 @@
    16.4    by (transfer fixing: uminus) clarsimp
    16.5  
    16.6  lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
    16.7 -by (simp add: diff_minus Groups.diff_minus)
    16.8 +  using of_int_add [of w "- z"] by simp
    16.9  
   16.10  lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
   16.11    by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult)
   16.12 @@ -749,7 +749,7 @@
   16.13  
   16.14  lemmas int_arith_rules =
   16.15    neg_le_iff_le numeral_One
   16.16 -  minus_zero diff_minus left_minus right_minus
   16.17 +  minus_zero left_minus right_minus
   16.18    mult_zero_left mult_zero_right mult_1_left mult_1_right
   16.19    mult_minus_left mult_minus_right
   16.20    minus_add_distrib minus_minus mult_assoc
   16.21 @@ -793,7 +793,6 @@
   16.22  subsection{*The functions @{term nat} and @{term int}*}
   16.23  
   16.24  text{*Simplify the term @{term "w + - z"}*}
   16.25 -lemmas diff_int_def_symmetric = diff_def [where 'a=int, symmetric, simp]
   16.26  
   16.27  lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
   16.28  apply (insert zless_nat_conj [of 1 z])
   16.29 @@ -1510,10 +1509,13 @@
   16.30    "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
   16.31    "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
   16.32    "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
   16.33 -  unfolding sub_def dup_def numeral.simps Pos_def Neg_def
   16.34 -    neg_numeral_def numeral_BitM
   16.35 -  by (simp_all only: algebra_simps)
   16.36 -
   16.37 +  apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def
   16.38 +    neg_numeral_def numeral_BitM)
   16.39 +  apply (simp_all only: algebra_simps minus_diff_eq)
   16.40 +  apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
   16.41 +  apply (simp_all only: minus_add add.assoc left_minus)
   16.42 +  apply (simp_all only: algebra_simps right_minus)
   16.43 +  done
   16.44  
   16.45  text {* Implementations *}
   16.46  
    17.1 --- a/src/HOL/Library/BigO.thy	Thu Oct 31 16:54:22 2013 +0100
    17.2 +++ b/src/HOL/Library/BigO.thy	Fri Nov 01 18:51:14 2013 +0100
    17.3 @@ -215,7 +215,7 @@
    17.4      f : lb +o O(g)"
    17.5    apply (rule set_minus_imp_plus)
    17.6    apply (rule bigo_bounded)
    17.7 -  apply (auto simp add: diff_minus fun_Compl_def func_plus)
    17.8 +  apply (auto simp add: fun_Compl_def func_plus)
    17.9    apply (drule_tac x = x in spec)+
   17.10    apply force
   17.11    apply (drule_tac x = x in spec)+
   17.12 @@ -390,7 +390,7 @@
   17.13    apply (rule set_minus_imp_plus)
   17.14    apply (drule set_plus_imp_minus)
   17.15    apply (drule bigo_minus)
   17.16 -  apply (simp add: diff_minus)
   17.17 +  apply simp
   17.18    done
   17.19  
   17.20  lemma bigo_minus3: "O(-f) = O(f)"
   17.21 @@ -446,7 +446,7 @@
   17.22    apply (rule bigo_minus)
   17.23    apply (subst set_minus_plus)
   17.24    apply assumption
   17.25 -  apply  (simp add: diff_minus add_ac)
   17.26 +  apply (simp add: add_ac)
   17.27    done
   17.28  
   17.29  lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
   17.30 @@ -545,10 +545,9 @@
   17.31  
   17.32  lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o 
   17.33      O(%x. h(k x))"
   17.34 -  apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
   17.35 -      func_plus)
   17.36 -  apply (erule bigo_compose1)
   17.37 -done
   17.38 +  apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus)
   17.39 +  apply (drule bigo_compose1) apply (simp add: fun_diff_def)
   17.40 +  done
   17.41  
   17.42  
   17.43  subsection {* Setsum *}
   17.44 @@ -779,7 +778,7 @@
   17.45    apply (subst abs_of_nonneg)
   17.46    apply (drule_tac x = x in spec) back
   17.47    apply (simp add: algebra_simps)
   17.48 -  apply (subst diff_minus)+
   17.49 +  apply (subst diff_conv_add_uminus)+
   17.50    apply (rule add_right_mono)
   17.51    apply (erule spec)
   17.52    apply (rule order_trans) 
   17.53 @@ -803,7 +802,7 @@
   17.54    apply (subst abs_of_nonneg)
   17.55    apply (drule_tac x = x in spec) back
   17.56    apply (simp add: algebra_simps)
   17.57 -  apply (subst diff_minus)+
   17.58 +  apply (subst diff_conv_add_uminus)+
   17.59    apply (rule add_left_mono)
   17.60    apply (rule le_imp_neg_le)
   17.61    apply (erule spec)
    18.1 --- a/src/HOL/Library/Convex.thy	Thu Oct 31 16:54:22 2013 +0100
    18.2 +++ b/src/HOL/Library/Convex.thy	Fri Nov 01 18:51:14 2013 +0100
    18.3 @@ -362,7 +362,7 @@
    18.4    shows "convex {x - y| x y. x \<in> s \<and> y \<in> t}"
    18.5  proof -
    18.6    have "{x - y| x y. x \<in> s \<and> y \<in> t} = {x + y |x y. x \<in> s \<and> y \<in> uminus ` t}"
    18.7 -    unfolding diff_def by auto
    18.8 +    by (auto simp add: diff_conv_add_uminus simp del: add_uminus_conv_diff)
    18.9    then show ?thesis
   18.10      using convex_sums[OF assms(1) convex_negations[OF assms(2)]] by auto
   18.11  qed
    19.1 --- a/src/HOL/Library/Float.thy	Thu Oct 31 16:54:22 2013 +0100
    19.2 +++ b/src/HOL/Library/Float.thy	Fri Nov 01 18:51:14 2013 +0100
    19.3 @@ -88,7 +88,7 @@
    19.4    done
    19.5  
    19.6  lemma minus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x - y \<in> float"
    19.7 -  unfolding ab_diff_minus by (intro uminus_float plus_float)
    19.8 +  using plus_float [of x "- y"] by simp
    19.9  
   19.10  lemma abs_float[simp]: "x \<in> float \<Longrightarrow> abs x \<in> float"
   19.11    by (cases x rule: linorder_cases[of 0]) auto
   19.12 @@ -960,7 +960,7 @@
   19.13    also have "... < (1 / 2) * 2 powr real (rat_precision n (int x) (int y))"
   19.14      apply (rule mult_strict_right_mono) by (insert assms) auto
   19.15    also have "\<dots> = 2 powr real (rat_precision n (int x) (int y) - 1)"
   19.16 -    by (simp add: powr_add diff_def powr_neg_numeral)
   19.17 +    using powr_add [of 2 _ "- 1", simplified add_uminus_conv_diff] by (simp add: powr_neg_numeral)
   19.18    also have "\<dots> = 2 ^ nat (rat_precision n (int x) (int y) - 1)"
   19.19      using rat_precision_pos[of x y n] assms by (simp add: powr_realpow[symmetric])
   19.20    also have "\<dots> \<le> 2 ^ nat (rat_precision n (int x) (int y)) - 1"
    20.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Oct 31 16:54:22 2013 +0100
    20.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Nov 01 18:51:14 2013 +0100
    20.3 @@ -231,7 +231,7 @@
    20.4  proof
    20.5    fix a b :: "'a fps"
    20.6    show "- a + a = 0" by (simp add: fps_ext)
    20.7 -  show "a - b = a + - b" by (simp add: fps_ext diff_minus)
    20.8 +  show "a + - b = a - b" by (simp add: fps_ext)
    20.9  qed
   20.10  
   20.11  instance fps :: (ab_group_add) ab_group_add
   20.12 @@ -348,10 +348,10 @@
   20.13  instance fps :: (ring) ring ..
   20.14  
   20.15  instance fps :: (ring_1) ring_1
   20.16 -  by (intro_classes, auto simp add: diff_minus distrib_right)
   20.17 +  by (intro_classes, auto simp add: distrib_right)
   20.18  
   20.19  instance fps :: (comm_ring_1) comm_ring_1
   20.20 -  by (intro_classes, auto simp add: diff_minus distrib_right)
   20.21 +  by (intro_classes, auto simp add: distrib_right)
   20.22  
   20.23  instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors
   20.24  proof
   20.25 @@ -888,7 +888,7 @@
   20.26    using fps_deriv_linear[of 1 f 1 g] by simp
   20.27  
   20.28  lemma fps_deriv_sub[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps) - g) = fps_deriv f - fps_deriv g"
   20.29 -  unfolding diff_minus by simp
   20.30 +  using fps_deriv_add [of f "- g"] by simp
   20.31  
   20.32  lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0"
   20.33    by (simp add: fps_ext fps_deriv_def fps_const_def)
   20.34 @@ -978,7 +978,7 @@
   20.35  
   20.36  lemma fps_nth_deriv_sub[simp]:
   20.37    "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g"
   20.38 -  unfolding diff_minus fps_nth_deriv_add by simp
   20.39 +  using fps_nth_deriv_add [of n f "- g"] by simp
   20.40  
   20.41  lemma fps_nth_deriv_0[simp]: "fps_nth_deriv n 0 = 0"
   20.42    by (induct n) simp_all
   20.43 @@ -2634,7 +2634,7 @@
   20.44    by (simp add: fps_eq_iff fps_compose_nth field_simps setsum_negf[symmetric])
   20.45  
   20.46  lemma fps_compose_sub_distrib: "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)"
   20.47 -  unfolding diff_minus fps_compose_uminus fps_compose_add_distrib ..
   20.48 +  using fps_compose_add_distrib [of a "- b" c] by (simp add: fps_compose_uminus)
   20.49  
   20.50  lemma X_fps_compose: "X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
   20.51    by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta)
    21.1 --- a/src/HOL/Library/Fraction_Field.thy	Thu Oct 31 16:54:22 2013 +0100
    21.2 +++ b/src/HOL/Library/Fraction_Field.thy	Fri Nov 01 18:51:14 2013 +0100
    21.3 @@ -132,7 +132,7 @@
    21.4  lemma diff_fract [simp]:
    21.5    assumes "b \<noteq> 0" and "d \<noteq> 0"
    21.6    shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)"
    21.7 -  using assms by (simp add: diff_fract_def diff_minus)
    21.8 +  using assms by (simp add: diff_fract_def)
    21.9  
   21.10  definition mult_fract_def:
   21.11    "q * r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
    22.1 --- a/src/HOL/Library/Function_Algebras.thy	Thu Oct 31 16:54:22 2013 +0100
    22.2 +++ b/src/HOL/Library/Function_Algebras.thy	Fri Nov 01 18:51:14 2013 +0100
    22.3 @@ -83,10 +83,10 @@
    22.4  
    22.5  instance "fun" :: (type, group_add) group_add
    22.6    by default
    22.7 -    (simp_all add: fun_eq_iff diff_minus)
    22.8 +    (simp_all add: fun_eq_iff)
    22.9  
   22.10  instance "fun" :: (type, ab_group_add) ab_group_add
   22.11 -  by default (simp_all add: diff_minus)
   22.12 +  by default simp_all
   22.13  
   22.14  
   22.15  text {* Multiplicative structures *}
    23.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu Oct 31 16:54:22 2013 +0100
    23.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Nov 01 18:51:14 2013 +0100
    23.3 @@ -224,12 +224,12 @@
    23.4      from unimodular_reduce_norm[OF th0] o
    23.5      have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
    23.6        apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
    23.7 -      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_minus)
    23.8 +      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp del: minus_one add: minus_one [symmetric])
    23.9        apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
   23.10        apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
   23.11        apply (rule_tac x="- ii" in exI, simp add: m power_mult)
   23.12 -      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_minus)
   23.13 -      apply (rule_tac x="ii" in exI, simp add: m power_mult diff_minus)
   23.14 +      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult)
   23.15 +      apply (rule_tac x="ii" in exI, simp add: m power_mult)
   23.16        done
   23.17      then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
   23.18      let ?w = "v / complex_of_real (root n (cmod b))"
   23.19 @@ -954,7 +954,7 @@
   23.20  
   23.21  lemma mpoly_sub_conv:
   23.22    "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
   23.23 -  by (simp add: diff_minus)
   23.24 +  by simp
   23.25  
   23.26  lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp
   23.27  
    24.1 --- a/src/HOL/Library/Inner_Product.thy	Thu Oct 31 16:54:22 2013 +0100
    24.2 +++ b/src/HOL/Library/Inner_Product.thy	Fri Nov 01 18:51:14 2013 +0100
    24.3 @@ -41,7 +41,7 @@
    24.4    using inner_add_left [of x "- x" y] by simp
    24.5  
    24.6  lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
    24.7 -  by (simp add: diff_minus inner_add_left)
    24.8 +  using inner_add_left [of x "- y" z] by simp
    24.9  
   24.10  lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
   24.11    by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
    25.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Thu Oct 31 16:54:22 2013 +0100
    25.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Fri Nov 01 18:51:14 2013 +0100
    25.3 @@ -13,9 +13,7 @@
    25.4    apply (rule antisym)
    25.5    apply (simp_all add: le_infI)
    25.6    apply (rule add_le_imp_le_left [of "uminus a"])
    25.7 -  apply (simp only: add_assoc [symmetric], simp)
    25.8 -  apply rule
    25.9 -  apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
   25.10 +  apply (simp only: add_assoc [symmetric], simp add: diff_le_eq add.commute)
   25.11    done
   25.12  
   25.13  lemma add_inf_distrib_right: "inf a b + c = inf (a + c) (b + c)"
   25.14 @@ -33,11 +31,10 @@
   25.15  lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)"
   25.16    apply (rule antisym)
   25.17    apply (rule add_le_imp_le_left [of "uminus a"])
   25.18 -  apply (simp only: add_assoc[symmetric], simp)
   25.19 -  apply rule
   25.20 +  apply (simp only: add_assoc [symmetric], simp)
   25.21 +  apply (simp add: le_diff_eq add.commute)
   25.22 +  apply (rule le_supI)
   25.23    apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
   25.24 -  apply (rule le_supI)
   25.25 -  apply (simp_all)
   25.26    done
   25.27  
   25.28  lemma add_sup_distrib_right: "sup a b + c = sup (a+c) (b+c)"
   25.29 @@ -87,9 +84,15 @@
   25.30  lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)"
   25.31    by (simp add: inf_eq_neg_sup)
   25.32  
   25.33 +lemma diff_inf_eq_sup: "a - inf b c = a + sup (- b) (- c)"
   25.34 +  using neg_inf_eq_sup [of b c, symmetric] by simp
   25.35 +
   25.36  lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)"
   25.37    by (simp add: sup_eq_neg_inf)
   25.38  
   25.39 +lemma diff_sup_eq_inf: "a - sup b c = a + inf (- b) (- c)"
   25.40 +  using neg_sup_eq_inf [of b c, symmetric] by simp
   25.41 +
   25.42  lemma add_eq_inf_sup: "a + b = sup a b + inf a b"
   25.43  proof -
   25.44    have "0 = - inf 0 (a-b) + inf (a-b) 0"
   25.45 @@ -97,8 +100,8 @@
   25.46    hence "0 = sup 0 (b-a) + inf (a-b) 0"
   25.47      by (simp add: inf_eq_neg_sup)
   25.48    hence "0 = (-a + sup a b) + (inf a b + (-b))"
   25.49 -    by (simp add: add_sup_distrib_left add_inf_distrib_right) (simp add: algebra_simps)
   25.50 -  thus ?thesis by (simp add: algebra_simps)
   25.51 +    by (simp only: add_sup_distrib_left add_inf_distrib_right) simp
   25.52 +  then show ?thesis by (simp add: algebra_simps)
   25.53  qed
   25.54  
   25.55  
   25.56 @@ -251,7 +254,7 @@
   25.57      apply assumption
   25.58      apply (rule notI)
   25.59      unfolding double_zero [symmetric, of a]
   25.60 -    apply simp
   25.61 +    apply blast
   25.62      done
   25.63  qed
   25.64  
   25.65 @@ -259,7 +262,8 @@
   25.66    "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
   25.67  proof -
   25.68    have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp)
   25.69 -  moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by simp
   25.70 +  moreover have "\<dots> \<longleftrightarrow> a \<le> 0"
   25.71 +    by (simp only: minus_add_distrib zero_le_double_add_iff_zero_le_single_add) simp
   25.72    ultimately show ?thesis by blast
   25.73  qed
   25.74  
   25.75 @@ -267,11 +271,12 @@
   25.76    "a + a < 0 \<longleftrightarrow> a < 0"
   25.77  proof -
   25.78    have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp)
   25.79 -  moreover have "\<dots> \<longleftrightarrow> a < 0" by simp
   25.80 +  moreover have "\<dots> \<longleftrightarrow> a < 0"
   25.81 +    by (simp only: minus_add_distrib zero_less_double_add_iff_zero_less_single_add) simp
   25.82    ultimately show ?thesis by blast
   25.83  qed
   25.84  
   25.85 -declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp]
   25.86 +declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp] diff_inf_eq_sup [simp] diff_sup_eq_inf [simp]
   25.87  
   25.88  lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
   25.89  proof -
   25.90 @@ -326,7 +331,7 @@
   25.91    then have "0 \<le> sup a (- a)" unfolding abs_lattice .
   25.92    then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
   25.93    then show ?thesis
   25.94 -    by (simp add: add_sup_inf_distribs sup_aci pprt_def nprt_def diff_minus abs_lattice)
   25.95 +    by (simp add: add_sup_inf_distribs ac_simps pprt_def nprt_def abs_lattice)
   25.96  qed
   25.97  
   25.98  subclass ordered_ab_group_add_abs
   25.99 @@ -355,16 +360,17 @@
  25.100    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  25.101    proof -
  25.102      have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
  25.103 -      by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
  25.104 +      by (simp add: abs_lattice add_sup_inf_distribs sup_aci ac_simps)
  25.105      have a: "a + b <= sup ?m ?n" by simp
  25.106      have b: "- a - b <= ?n" by simp
  25.107      have c: "?n <= sup ?m ?n" by simp
  25.108      from b c have d: "-a-b <= sup ?m ?n" by (rule order_trans)
  25.109 -    have e:"-a-b = -(a+b)" by (simp add: diff_minus)
  25.110 +    have e:"-a-b = -(a+b)" by simp
  25.111      from a d e have "abs(a+b) <= sup ?m ?n"
  25.112        apply -
  25.113        apply (drule abs_leI)
  25.114 -      apply auto
  25.115 +      apply (simp_all only: algebra_simps ac_simps minus_add)
  25.116 +      apply (metis add_uminus_conv_diff d sup_commute uminus_add_conv_diff)
  25.117        done
  25.118      with g[symmetric] show ?thesis by simp
  25.119    qed
  25.120 @@ -421,14 +427,12 @@
  25.121    }
  25.122    note b = this[OF refl[of a] refl[of b]]
  25.123    have xy: "- ?x <= ?y"
  25.124 -    apply (simp)
  25.125 -    apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
  25.126 -    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
  25.127 +    apply simp
  25.128 +    apply (metis (full_types) add_increasing add_uminus_conv_diff lattice_ab_group_add_class.minus_le_self_iff minus_add_distrib mult_nonneg_nonneg mult_nonpos_nonpos nprt_le_zero zero_le_pprt)
  25.129      done
  25.130    have yx: "?y <= ?x"
  25.131 -    apply (simp add:diff_minus)
  25.132 -    apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
  25.133 -    apply (simp_all add: mult_nonneg_nonpos mult_nonpos_nonneg)
  25.134 +    apply simp
  25.135 +    apply (metis (full_types) add_nonpos_nonpos add_uminus_conv_diff lattice_ab_group_add_class.le_minus_self_iff minus_add_distrib mult_nonneg_nonpos mult_nonpos_nonneg nprt_le_zero zero_le_pprt)
  25.136      done
  25.137    have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
  25.138    have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
  25.139 @@ -549,7 +553,7 @@
  25.140      by simp
  25.141    then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
  25.142      by (simp only: minus_le_iff)
  25.143 -  then show ?thesis by simp
  25.144 +  then show ?thesis by (simp add: algebra_simps)
  25.145  qed
  25.146  
  25.147  instance int :: lattice_ring
  25.148 @@ -567,3 +571,4 @@
  25.149  qed
  25.150  
  25.151  end
  25.152 +
    26.1 --- a/src/HOL/Library/Polynomial.thy	Thu Oct 31 16:54:22 2013 +0100
    26.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Nov 01 18:51:14 2013 +0100
    26.3 @@ -667,7 +667,7 @@
    26.4    show "- p + p = 0"
    26.5      by (simp add: poly_eq_iff)
    26.6    show "p - q = p + - q"
    26.7 -    by (simp add: poly_eq_iff diff_minus)
    26.8 +    by (simp add: poly_eq_iff)
    26.9  qed
   26.10  
   26.11  end
   26.12 @@ -714,15 +714,15 @@
   26.13  
   26.14  lemma degree_diff_le_max: "degree (p - q) \<le> max (degree p) (degree q)"
   26.15    using degree_add_le [where p=p and q="-q"]
   26.16 -  by (simp add: diff_minus)
   26.17 +  by simp
   26.18  
   26.19  lemma degree_diff_le:
   26.20    "\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p - q) \<le> n"
   26.21 -  by (simp add: diff_minus degree_add_le)
   26.22 +  using degree_add_le [of p n "- q"] by simp
   26.23  
   26.24  lemma degree_diff_less:
   26.25    "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p - q) < n"
   26.26 -  by (simp add: diff_minus degree_add_less)
   26.27 +  using degree_add_less [of p n "- q"] by simp
   26.28  
   26.29  lemma add_monom: "monom a n + monom b n = monom (a + b) n"
   26.30    by (rule poly_eqI) simp
   26.31 @@ -793,7 +793,7 @@
   26.32  lemma poly_diff [simp]:
   26.33    fixes x :: "'a::comm_ring"
   26.34    shows "poly (p - q) x = poly p x - poly q x"
   26.35 -  by (simp add: diff_minus)
   26.36 +  using poly_add [of p "- q" x] by simp
   26.37  
   26.38  lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
   26.39    by (induct A rule: infinite_finite_induct) simp_all
    27.1 --- a/src/HOL/Library/Product_plus.thy	Thu Oct 31 16:54:22 2013 +0100
    27.2 +++ b/src/HOL/Library/Product_plus.thy	Fri Nov 01 18:51:14 2013 +0100
    27.3 @@ -104,7 +104,7 @@
    27.4    (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
    27.5  
    27.6  instance prod :: (group_add, group_add) group_add
    27.7 -  by default (simp_all add: prod_eq_iff diff_minus)
    27.8 +  by default (simp_all add: prod_eq_iff)
    27.9  
   27.10  instance prod :: (ab_group_add, ab_group_add) ab_group_add
   27.11    by default (simp_all add: prod_eq_iff)
    28.1 --- a/src/HOL/Library/Set_Algebras.thy	Thu Oct 31 16:54:22 2013 +0100
    28.2 +++ b/src/HOL/Library/Set_Algebras.thy	Fri Nov 01 18:51:14 2013 +0100
    28.3 @@ -190,12 +190,12 @@
    28.4    done
    28.5  
    28.6  lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
    28.7 -  by (auto simp add: elt_set_plus_def add_ac diff_minus)
    28.8 +  by (auto simp add: elt_set_plus_def add_ac)
    28.9  
   28.10  lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
   28.11 -  apply (auto simp add: elt_set_plus_def add_ac diff_minus)
   28.12 +  apply (auto simp add: elt_set_plus_def add_ac)
   28.13    apply (subgoal_tac "a = (a + - b) + b")
   28.14 -   apply (rule bexI, assumption, assumption)
   28.15 +   apply (rule bexI, assumption)
   28.16    apply (auto simp add: add_ac)
   28.17    done
   28.18  
    29.1 --- a/src/HOL/Limits.thy	Thu Oct 31 16:54:22 2013 +0100
    29.2 +++ b/src/HOL/Limits.thy	Fri Nov 01 18:51:14 2013 +0100
    29.3 @@ -179,7 +179,7 @@
    29.4  apply (rule_tac x = K in exI, simp)
    29.5  apply (rule exI [where x = 0], auto)
    29.6  apply (erule order_less_le_trans, simp)
    29.7 -apply (drule_tac x=n in spec, fold diff_minus)
    29.8 +apply (drule_tac x=n in spec)
    29.9  apply (drule order_trans [OF norm_triangle_ineq2])
   29.10  apply simp
   29.11  done
   29.12 @@ -192,9 +192,11 @@
   29.13    then obtain K
   29.14      where *: "0 < K" and **: "\<And>n. norm (X n) \<le> K" by (auto simp add: Bseq_def)
   29.15    from * have "0 < K + norm (X 0)" by (rule order_less_le_trans) simp
   29.16 -  moreover from ** have "\<forall>n. norm (X n + - X 0) \<le> K + norm (X 0)"
   29.17 -    by (auto intro: order_trans norm_triangle_ineq)
   29.18 -  ultimately show ?Q by blast
   29.19 +  from ** have "\<forall>n. norm (X n - X 0) \<le> K + norm (X 0)"
   29.20 +    by (auto intro: order_trans norm_triangle_ineq4)
   29.21 +  then have "\<forall>n. norm (X n + - X 0) \<le> K + norm (X 0)"
   29.22 +    by simp
   29.23 +  with `0 < K + norm (X 0)` show ?Q by blast
   29.24  next
   29.25    assume ?Q then show ?P by (auto simp add: Bseq_iff2)
   29.26  qed
   29.27 @@ -205,6 +207,7 @@
   29.28  apply (drule_tac x = n in spec, arith)
   29.29  done
   29.30  
   29.31 +
   29.32  subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
   29.33  
   29.34  lemma Bseq_isUb:
   29.35 @@ -342,7 +345,7 @@
   29.36    unfolding Zfun_def by simp
   29.37  
   29.38  lemma Zfun_diff: "\<lbrakk>Zfun f F; Zfun g F\<rbrakk> \<Longrightarrow> Zfun (\<lambda>x. f x - g x) F"
   29.39 -  by (simp only: diff_minus Zfun_add Zfun_minus)
   29.40 +  using Zfun_add [of f F "\<lambda>x. - g x"] by (simp add: Zfun_minus)
   29.41  
   29.42  lemma (in bounded_linear) Zfun:
   29.43    assumes g: "Zfun g F"
   29.44 @@ -532,7 +535,7 @@
   29.45  lemma tendsto_diff [tendsto_intros]:
   29.46    fixes a b :: "'a::real_normed_vector"
   29.47    shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) F"
   29.48 -  by (simp add: diff_minus tendsto_add tendsto_minus)
   29.49 +  using tendsto_add [of f a F "\<lambda>x. - g x" "- b"] by (simp add: tendsto_minus)
   29.50  
   29.51  lemma continuous_diff [continuous_intros]:
   29.52    fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    30.1 --- a/src/HOL/Matrix_LP/LP.thy	Thu Oct 31 16:54:22 2013 +0100
    30.2 +++ b/src/HOL/Matrix_LP/LP.thy	Fri Nov 01 18:51:14 2013 +0100
    30.3 @@ -72,8 +72,7 @@
    30.4  proof -
    30.5    have "0 <= A - A1"    
    30.6    proof -
    30.7 -    have 1: "A - A1 = A + (- A1)" by simp
    30.8 -    show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified assms])
    30.9 +    from assms add_right_mono [of A1 A "- A1"] show ?thesis by simp
   30.10    qed
   30.11    then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg)
   30.12    with assms show "abs (A-A1) <= (A2-A1)" by simp
   30.13 @@ -147,9 +146,9 @@
   30.14    then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
   30.15    then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps)
   30.16    have s2: "c - y * A <= c2 - y * A1"
   30.17 -    by (simp add: diff_minus assms add_mono mult_left_mono)
   30.18 +    by (simp add: assms add_mono mult_left_mono algebra_simps)
   30.19    have s1: "c1 - y * A2 <= c - y * A"
   30.20 -    by (simp add: diff_minus assms add_mono mult_left_mono)
   30.21 +    by (simp add: assms add_mono mult_left_mono algebra_simps)
   30.22    have prts: "(c - y * A) * x <= ?C"
   30.23      apply (simp add: Let_def)
   30.24      apply (rule mult_le_prts)
    31.1 --- a/src/HOL/Matrix_LP/Matrix.thy	Thu Oct 31 16:54:22 2013 +0100
    31.2 +++ b/src/HOL/Matrix_LP/Matrix.thy	Fri Nov 01 18:51:14 2013 +0100
    31.3 @@ -1542,8 +1542,8 @@
    31.4    fix A B :: "'a matrix"
    31.5    show "- A + A = 0" 
    31.6      by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
    31.7 -  show "A - B = A + - B"
    31.8 -    by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext diff_minus)
    31.9 +  show "A + - B = A - B"
   31.10 +    by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext)
   31.11  qed
   31.12  
   31.13  instance matrix :: (ab_group_add) ab_group_add
    32.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Thu Oct 31 16:54:22 2013 +0100
    32.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Fri Nov 01 18:51:14 2013 +0100
    32.3 @@ -493,8 +493,10 @@
    32.4  
    32.5  lemma bigo_compose2:
    32.6  "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. f(k x)) =o (\<lambda>x. g(k x)) +o O(\<lambda>x. h(k x))"
    32.7 -apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def func_plus)
    32.8 -by (erule bigo_compose1)
    32.9 +apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus)
   32.10 +apply (drule bigo_compose1 [of "f - g" h k])
   32.11 +apply (simp add: fun_diff_def)
   32.12 +done
   32.13  
   32.14  subsection {* Setsum *}
   32.15  
    33.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Oct 31 16:54:22 2013 +0100
    33.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Nov 01 18:51:14 2013 +0100
    33.3 @@ -1099,8 +1099,8 @@
    33.4    shows "(\<lambda>x. m *s x + c) o (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
    33.5    "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) o (\<lambda>x. m *s x + c) = id"
    33.6    using m0
    33.7 -  apply (auto simp add: fun_eq_iff vector_add_ldistrib)
    33.8 -  apply (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric])
    33.9 +  apply (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff)
   33.10 +  apply (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1 [symmetric])
   33.11    done
   33.12  
   33.13  lemma vector_affinity_eq:
   33.14 @@ -1114,7 +1114,7 @@
   33.15      using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
   33.16  next
   33.17    assume h: "x = inverse m *s y + - (inverse m *s c)"
   33.18 -  show "m *s x + c = y" unfolding h diff_minus[symmetric]
   33.19 +  show "m *s x + c = y" unfolding h
   33.20      using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
   33.21  qed
   33.22  
    34.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Oct 31 16:54:22 2013 +0100
    34.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 01 18:51:14 2013 +0100
    34.3 @@ -858,9 +858,10 @@
    34.4    assumes "affine_parallel A B"
    34.5    shows "affine_parallel B A"
    34.6  proof -
    34.7 -  from assms obtain a where "B = (\<lambda>x. a + x) ` A"
    34.8 +  from assms obtain a where B: "B = (\<lambda>x. a + x) ` A"
    34.9      unfolding affine_parallel_def by auto
   34.10 -  then show ?thesis
   34.11 +  have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
   34.12 +  from B show ?thesis
   34.13      using translation_galois [of B a A]
   34.14      unfolding affine_parallel_def by auto
   34.15  qed
   34.16 @@ -980,6 +981,7 @@
   34.17    assumes "affine S" "a \<in> S"
   34.18    shows "subspace ((\<lambda>x. (-a)+x) ` S)"
   34.19  proof -
   34.20 +  have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
   34.21    have "affine ((\<lambda>x. (-a)+x) ` S)"
   34.22      using  affine_translation assms by auto
   34.23    moreover have "0 : ((\<lambda>x. (-a)+x) ` S)"
   34.24 @@ -992,15 +994,12 @@
   34.25    assumes "L \<equiv> {y. \<exists>x \<in> S. (-a)+x=y}"
   34.26    shows "subspace L & affine_parallel S L"
   34.27  proof -
   34.28 -  have par: "affine_parallel S L"
   34.29 -    unfolding affine_parallel_def using assms by auto
   34.30 +  from assms have "L = plus (- a) ` S" by auto
   34.31 +  then have par: "affine_parallel S L"
   34.32 +    unfolding affine_parallel_def .. 
   34.33    then have "affine L" using assms parallel_is_affine by auto
   34.34    moreover have "0 \<in> L"
   34.35 -    using assms
   34.36 -    apply auto
   34.37 -    using exI[of "(\<lambda>x. x:S \<and> -a+x=0)" a]
   34.38 -    apply auto
   34.39 -    done
   34.40 +    using assms by auto
   34.41    ultimately show ?thesis
   34.42      using subspace_affine par by auto
   34.43  qed
   34.44 @@ -2390,7 +2389,7 @@
   34.45    ultimately have h1: "affine hull ((\<lambda>x. a + x) `  S) \<subseteq> (\<lambda>x. a + x) ` (affine hull S)"
   34.46      by (metis hull_minimal)
   34.47    have "affine((\<lambda>x. -a + x) ` (affine hull ((\<lambda>x. a + x) `  S)))"
   34.48 -    using affine_translation affine_affine_hull by auto
   34.49 +    using affine_translation affine_affine_hull by (auto simp del: uminus_add_conv_diff)
   34.50    moreover have "(\<lambda>x. -a + x) ` (\<lambda>x. a + x) `  S \<subseteq> (\<lambda>x. -a + x) ` (affine hull ((\<lambda>x. a + x) `  S))"
   34.51      using hull_subset[of "(\<lambda>x. a + x) `  S"] by auto
   34.52    moreover have "S = (\<lambda>x. -a + x) ` (\<lambda>x. a + x) `  S"
   34.53 @@ -2478,7 +2477,7 @@
   34.54      using affine_dependent_translation_eq[of "(insert a S)" "-a"]
   34.55        affine_dependent_imp_dependent2 assms
   34.56        dependent_imp_affine_dependent[of a S]
   34.57 -    by auto
   34.58 +    by (auto simp del: uminus_add_conv_diff)
   34.59  qed
   34.60  
   34.61  lemma affine_dependent_iff_dependent2:
   34.62 @@ -2512,7 +2511,7 @@
   34.63      then have "insert 0 ((\<lambda>x. -a+x) ` (s - {a})) = (\<lambda>x. -a+x) ` s"
   34.64        by auto
   34.65      then have "span ((\<lambda>x. -a+x) ` (s - {a}))=span ((\<lambda>x. -a+x) ` s)"
   34.66 -      using span_insert_0[of "op + (- a) ` (s - {a})"] by auto
   34.67 +      using span_insert_0[of "op + (- a) ` (s - {a})"] by (auto simp del: uminus_add_conv_diff)
   34.68      moreover have "{x - a |x. x \<in> (s - {a})} = ((\<lambda>x. -a+x) ` (s - {a}))"
   34.69        by auto
   34.70      moreover have "insert a (s - {a}) = insert a s"
   34.71 @@ -2652,7 +2651,7 @@
   34.72      moreover have h1: "card ((\<lambda>x. -a + x) ` (B-{a})) = card (B-{a})"
   34.73         apply (rule card_image)
   34.74         using translate_inj_on
   34.75 -       apply auto
   34.76 +       apply (auto simp del: uminus_add_conv_diff)
   34.77         done
   34.78      ultimately have "card (B-{a}) > 0" by auto
   34.79      then have *: "finite (B - {a})"
    35.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Oct 31 16:54:22 2013 +0100
    35.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Nov 01 18:51:14 2013 +0100
    35.3 @@ -516,7 +516,7 @@
    35.4        unfolding e_def
    35.5        using c[THEN conjunct1]
    35.6        using norm_minus_cancel[of "f' i - f'' i"]
    35.7 -      by (auto simp add: add.commute ab_diff_minus)
    35.8 +      by auto
    35.9      finally show False
   35.10        using c
   35.11        using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R i"]
    36.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Oct 31 16:54:22 2013 +0100
    36.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Nov 01 18:51:14 2013 +0100
    36.3 @@ -115,7 +115,7 @@
    36.4  instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
    36.5  
    36.6  instance vec :: (group_add, finite) group_add
    36.7 -  by default (simp_all add: vec_eq_iff diff_minus)
    36.8 +  by default (simp_all add: vec_eq_iff)
    36.9  
   36.10  instance vec :: (ab_group_add, finite) ab_group_add
   36.11    by default (simp_all add: vec_eq_iff)
    37.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Oct 31 16:54:22 2013 +0100
    37.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 01 18:51:14 2013 +0100
    37.3 @@ -44,9 +44,7 @@
    37.4      by auto
    37.5    also have "\<dots> \<le> e"
    37.6      apply (rule cSup_asclose)
    37.7 -    apply (auto simp add: S)
    37.8 -    apply (metis abs_minus_add_cancel b add_commute diff_minus)
    37.9 -    done
   37.10 +    using abs_minus_add_cancel b by (auto simp add: S)
   37.11    finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
   37.12    then show ?thesis
   37.13      by (simp add: Inf_real_def)
   37.14 @@ -380,7 +378,7 @@
   37.15                  using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
   37.16                then have "y\<bullet>k < a\<bullet>k"
   37.17                  using e[THEN conjunct1] k
   37.18 -                by (auto simp add: field_simps as inner_Basis inner_simps)
   37.19 +                by (auto simp add: field_simps abs_less_iff as inner_Basis inner_simps)
   37.20                then have "y \<notin> i"
   37.21                  unfolding ab mem_interval by (auto intro!: bexI[OF _ k])
   37.22                then show False using yi by auto
   37.23 @@ -11975,7 +11973,7 @@
   37.24      and "g absolutely_integrable_on s"
   37.25    shows "(\<lambda>x. f x - g x) absolutely_integrable_on s"
   37.26    using absolutely_integrable_add[OF assms(1) absolutely_integrable_neg[OF assms(2)]]
   37.27 -  by (simp only: algebra_simps)
   37.28 +  by (simp add: algebra_simps)
   37.29  
   37.30  lemma absolutely_integrable_linear:
   37.31    fixes f :: "'m::ordered_euclidean_space \<Rightarrow> 'n::ordered_euclidean_space"
    38.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Oct 31 16:54:22 2013 +0100
    38.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Nov 01 18:51:14 2013 +0100
    38.3 @@ -303,7 +303,7 @@
    38.4    by (metis linear_iff)
    38.5  
    38.6  lemma linear_sub: "linear f \<Longrightarrow> f (x - y) = f x - f y"
    38.7 -  by (simp add: diff_minus linear_add linear_neg)
    38.8 +  using linear_add [of f x "- y"] by (simp add: linear_neg)
    38.9  
   38.10  lemma linear_setsum:
   38.11    assumes lin: "linear f"
   38.12 @@ -384,10 +384,10 @@
   38.13    using bilinear_radd [OF assms, of x 0 0 ] by (simp add: eq_add_iff field_simps)
   38.14  
   38.15  lemma bilinear_lsub: "bilinear h \<Longrightarrow> h (x - y) z = h x z - h y z"
   38.16 -  by (simp  add: diff_minus bilinear_ladd bilinear_lneg)
   38.17 +  using bilinear_ladd [of h x "- y"] by (simp add: bilinear_lneg)
   38.18  
   38.19  lemma bilinear_rsub: "bilinear h \<Longrightarrow> h z (x - y) = h z x - h z y"
   38.20 -  by (simp  add: diff_minus bilinear_radd bilinear_rneg)
   38.21 +  using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg)
   38.22  
   38.23  lemma bilinear_setsum:
   38.24    assumes bh: "bilinear h"
   38.25 @@ -730,7 +730,7 @@
   38.26    by (metis scaleR_minus1_left subspace_mul)
   38.27  
   38.28  lemma subspace_sub: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
   38.29 -  by (metis diff_minus subspace_add subspace_neg)
   38.30 +  using subspace_add [of S x "- y"] by (simp add: subspace_neg)
   38.31  
   38.32  lemma (in real_vector) subspace_setsum:
   38.33    assumes sA: "subspace A"
   38.34 @@ -1021,8 +1021,7 @@
   38.35      apply safe
   38.36      apply (rule_tac x=k in exI, simp)
   38.37      apply (erule rev_image_eqI [OF SigmaI [OF rangeI]])
   38.38 -    apply simp
   38.39 -    apply (rule right_minus)
   38.40 +    apply auto
   38.41      done
   38.42    then show ?thesis by simp
   38.43  qed
   38.44 @@ -2064,7 +2063,7 @@
   38.45        using C by simp
   38.46      have "orthogonal ?a y"
   38.47        unfolding orthogonal_def
   38.48 -      unfolding inner_diff inner_setsum_left diff_eq_0_iff_eq
   38.49 +      unfolding inner_diff inner_setsum_left right_minus_eq
   38.50        unfolding setsum_diff1' [OF `finite C` `y \<in> C`]
   38.51        apply (clarsimp simp add: inner_commute[of y a])
   38.52        apply (rule setsum_0')
   38.53 @@ -3026,7 +3025,7 @@
   38.54          norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) =  0)"
   38.55        using x y
   38.56        unfolding inner_simps
   38.57 -      unfolding power2_norm_eq_inner[symmetric] power2_eq_square diff_eq_0_iff_eq
   38.58 +      unfolding power2_norm_eq_inner[symmetric] power2_eq_square right_minus_eq
   38.59        apply (simp add: inner_commute)
   38.60        apply (simp add: field_simps)
   38.61        apply metis
    39.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Oct 31 16:54:22 2013 +0100
    39.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Nov 01 18:51:14 2013 +0100
    39.3 @@ -4858,8 +4858,8 @@
    39.4    assumes "uniformly_continuous_on s f"
    39.5      and "uniformly_continuous_on s g"
    39.6    shows "uniformly_continuous_on s (\<lambda>x. f x - g x)"
    39.7 -  unfolding ab_diff_minus using assms
    39.8 -  by (intro uniformly_continuous_on_add uniformly_continuous_on_minus)
    39.9 +  using assms uniformly_continuous_on_add [of s f "- g"]
   39.10 +    by (simp add: fun_Compl_def uniformly_continuous_on_minus)
   39.11  
   39.12  text{* Continuity of all kinds is preserved under composition. *}
   39.13  
   39.14 @@ -5680,8 +5680,6 @@
   39.15      apply auto
   39.16      apply (rule_tac x= xa in exI)
   39.17      apply auto
   39.18 -    apply (rule_tac x=xa in exI)
   39.19 -    apply auto
   39.20      done
   39.21    then show ?thesis
   39.22      using compact_sums[OF assms(1) compact_negations[OF assms(2)]] by auto
   39.23 @@ -7032,7 +7030,8 @@
   39.24    unfolding homeomorphic_minimal
   39.25    apply (rule_tac x="\<lambda>x. a + x" in exI)
   39.26    apply (rule_tac x="\<lambda>x. -a + x" in exI)
   39.27 -  using continuous_on_add[OF continuous_on_const continuous_on_id]
   39.28 +  using continuous_on_add [OF continuous_on_const continuous_on_id, of s a]
   39.29 +    continuous_on_add [OF continuous_on_const continuous_on_id, of "plus a ` s" "- a"]
   39.30    apply auto
   39.31    done
   39.32  
    40.1 --- a/src/HOL/NSA/CLim.thy	Thu Oct 31 16:54:22 2013 +0100
    40.2 +++ b/src/HOL/NSA/CLim.thy	Fri Nov 01 18:51:14 2013 +0100
    40.3 @@ -22,11 +22,11 @@
    40.4  lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))";
    40.5  apply auto 
    40.6  apply (drule_tac x="x+a" in spec) 
    40.7 -apply (simp add: diff_minus add_assoc) 
    40.8 +apply (simp add: add_assoc) 
    40.9  done
   40.10  
   40.11  lemma complex_add_minus_iff [simp]: "(x + - a = (0::complex)) = (x=a)"
   40.12 -by (simp add: diff_eq_eq diff_minus [symmetric])
   40.13 +by (simp add: diff_eq_eq)
   40.14  
   40.15  lemma complex_add_eq_0_iff [iff]: "(x+y = (0::complex)) = (y = -x)"
   40.16  apply auto
    41.1 --- a/src/HOL/NSA/HDeriv.thy	Thu Oct 31 16:54:22 2013 +0100
    41.2 +++ b/src/HOL/NSA/HDeriv.thy	Fri Nov 01 18:51:14 2013 +0100
    41.3 @@ -81,8 +81,7 @@
    41.4  text{*second equivalence *}
    41.5  lemma NSDERIV_NSLIM_iff2:
    41.6       "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --NS> D)"
    41.7 -by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff  diff_minus [symmetric]
    41.8 -              LIM_NSLIM_iff [symmetric])
    41.9 +  by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff LIM_NSLIM_iff [symmetric])
   41.10  
   41.11  (* while we're at it! *)
   41.12  
   41.13 @@ -120,11 +119,10 @@
   41.14                   hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)"
   41.15  apply (auto simp add: nsderiv_def)
   41.16  apply (case_tac "h = (0::hypreal) ")
   41.17 -apply (auto simp add: diff_minus)
   41.18 +apply auto
   41.19  apply (drule_tac x = h in bspec)
   41.20  apply (drule_tac [2] c = h in approx_mult1)
   41.21 -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   41.22 -            simp add: diff_minus)
   41.23 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
   41.24  done
   41.25  
   41.26  lemma NSDERIVD3:
   41.27 @@ -135,8 +133,7 @@
   41.28  apply (auto simp add: nsderiv_def)
   41.29  apply (rule ccontr, drule_tac x = h in bspec)
   41.30  apply (drule_tac [2] c = h in approx_mult1)
   41.31 -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   41.32 -            simp add: mult_assoc diff_minus)
   41.33 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult_assoc)
   41.34  done
   41.35  
   41.36  text{*Differentiability implies continuity
   41.37 @@ -174,7 +171,7 @@
   41.38  apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
   41.39  apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec)
   41.40  apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add)
   41.41 -apply (auto simp add: diff_minus add_ac)
   41.42 +apply (auto simp add: add_ac algebra_simps)
   41.43  done
   41.44  
   41.45  text{*Product of functions - Proof is trivial but tedious
   41.46 @@ -234,9 +231,11 @@
   41.47    hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) -- 0 --NS> - D"
   41.48      by (rule NSLIM_minus)
   41.49    have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h"
   41.50 -    by (simp add: minus_divide_left diff_minus)
   41.51 +    by (simp add: minus_divide_left)
   41.52    with deriv
   41.53 -  show "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
   41.54 +  have "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
   41.55 +  then show "(\<lambda>h. (f (x + h) - f x) / h) -- 0 --NS> D \<Longrightarrow>
   41.56 +    (\<lambda>h. (f x - f (x + h)) / h) -- 0 --NS> - D" by simp
   41.57  qed
   41.58  
   41.59  text{*Subtraction*}
   41.60 @@ -244,11 +243,8 @@
   41.61  by (blast dest: NSDERIV_add NSDERIV_minus)
   41.62  
   41.63  lemma NSDERIV_diff:
   41.64 -     "[| NSDERIV f x :> Da; NSDERIV g x :> Db |]
   41.65 -      ==> NSDERIV (%x. f x - g x) x :> Da-Db"
   41.66 -apply (simp add: diff_minus)
   41.67 -apply (blast intro: NSDERIV_add_minus)
   41.68 -done
   41.69 +  "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x - g x) x :> Da-Db"
   41.70 +  using NSDERIV_add_minus [of f x Da g Db] by simp
   41.71  
   41.72  text{*  Similarly to the above, the chain rule admits an entirely
   41.73     straightforward derivation. Compare this with Harrison's
   41.74 @@ -294,7 +290,7 @@
   41.75                     - star_of (f (g x)))
   41.76                / (( *f* g) (star_of(x) + xa) - star_of (g x))
   41.77               \<approx> star_of(Da)"
   41.78 -by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def diff_minus [symmetric])
   41.79 +by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
   41.80  
   41.81  (*--------------------------------------------------------------
   41.82     from other version of differentiability
   41.83 @@ -354,13 +350,23 @@
   41.84      from h_Inf have "h * star_of x \<in> Infinitesimal" by (rule Infinitesimal_HFinite_mult) simp
   41.85      with assms have "inverse (- (h * star_of x) + - (star_of x * star_of x)) \<approx>
   41.86        inverse (- (star_of x * star_of x))"
   41.87 -      by (auto intro: inverse_add_Infinitesimal_approx2
   41.88 +      apply - apply (rule inverse_add_Infinitesimal_approx2)
   41.89 +      apply (auto
   41.90          dest!: hypreal_of_real_HFinite_diff_Infinitesimal
   41.91          simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
   41.92 -    with not_0 `h \<noteq> 0` assms have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
   41.93 +      done
   41.94 +    moreover from not_0 `h \<noteq> 0` assms
   41.95 +      have "inverse (- (h * star_of x) + - (star_of x * star_of x)) =
   41.96 +        (inverse (star_of x + h) - inverse (star_of x)) / h"
   41.97 +      apply (simp add: division_ring_inverse_diff nonzero_inverse_mult_distrib [symmetric]
   41.98 +        nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs)
   41.99 +      apply (subst nonzero_inverse_minus_eq [symmetric])
  41.100 +      using distrib_right [symmetric, of h "star_of x" "star_of x"] apply simp
  41.101 +      apply (simp add: field_simps) 
  41.102 +      done
  41.103 +    ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
  41.104        - (inverse (star_of x) * inverse (star_of x))"
  41.105 -      by (simp add: inverse_add nonzero_inverse_mult_distrib [symmetric]
  41.106 -        nonzero_inverse_minus_eq [symmetric] add_ac mult_ac diff_minus ring_distribs)
  41.107 +      using assms by (simp add: nonzero_inverse_mult_distrib [symmetric] nonzero_inverse_minus_eq [symmetric])
  41.108    } then show ?thesis by (simp add: nsderiv_def)
  41.109  qed
  41.110  
    42.1 --- a/src/HOL/NSA/HLim.thy	Thu Oct 31 16:54:22 2013 +0100
    42.2 +++ b/src/HOL/NSA/HLim.thy	Fri Nov 01 18:51:14 2013 +0100
    42.3 @@ -71,7 +71,7 @@
    42.4  
    42.5  lemma NSLIM_diff:
    42.6    "\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)"
    42.7 -by (simp only: diff_minus NSLIM_add NSLIM_minus)
    42.8 +  by (simp only: NSLIM_add NSLIM_minus diff_conv_add_uminus)
    42.9  
   42.10  lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
   42.11  by (simp only: NSLIM_add NSLIM_minus)
   42.12 @@ -95,7 +95,7 @@
   42.13  
   42.14  lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
   42.15  apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
   42.16 -apply (auto simp add: diff_minus add_assoc)
   42.17 +apply (auto simp add: add_assoc)
   42.18  done
   42.19  
   42.20  lemma NSLIM_const_not_eq:
   42.21 @@ -243,14 +243,14 @@
   42.22  apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
   42.23  apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
   42.24  apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
   42.25 - prefer 2 apply (simp add: add_commute diff_minus [symmetric])
   42.26 + prefer 2 apply (simp add: add_commute)
   42.27  apply (rule_tac x = x in star_cases)
   42.28  apply (rule_tac [2] x = x in star_cases)
   42.29 -apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
   42.30 +apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc star_n_zero_num)
   42.31  done
   42.32  
   42.33  lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
   42.34 -by (rule NSLIM_h_iff)
   42.35 +  by (fact NSLIM_h_iff)
   42.36  
   42.37  lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
   42.38  by (simp add: isNSCont_def)
    43.1 --- a/src/HOL/NSA/HSEQ.thy	Thu Oct 31 16:54:22 2013 +0100
    43.2 +++ b/src/HOL/NSA/HSEQ.thy	Fri Nov 01 18:51:14 2013 +0100
    43.3 @@ -73,14 +73,14 @@
    43.4  lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a"
    43.5  by (drule NSLIMSEQ_minus, simp)
    43.6  
    43.7 +lemma NSLIMSEQ_diff:
    43.8 +     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
    43.9 +  using NSLIMSEQ_add [of X a "- Y" "- b"] by (simp add: NSLIMSEQ_minus fun_Compl_def)
   43.10 +
   43.11  (* FIXME: delete *)
   43.12  lemma NSLIMSEQ_add_minus:
   43.13       "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b"
   43.14 -by (simp add: NSLIMSEQ_add NSLIMSEQ_minus)
   43.15 -
   43.16 -lemma NSLIMSEQ_diff:
   43.17 -     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
   43.18 -by (simp add: diff_minus NSLIMSEQ_add NSLIMSEQ_minus)
   43.19 +  by (simp add: NSLIMSEQ_diff)
   43.20  
   43.21  lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b"
   43.22  by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
   43.23 @@ -233,11 +233,11 @@
   43.24  
   43.25  lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
   43.26       "(%n. r + -inverse(real(Suc n))) ----NS> r"
   43.27 -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus)
   43.28 +  using LIMSEQ_inverse_real_of_nat_add_minus by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
   43.29  
   43.30  lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
   43.31       "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"
   43.32 -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult)
   43.33 +  using LIMSEQ_inverse_real_of_nat_add_minus_mult by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
   43.34  
   43.35  
   43.36  subsection {* Convergence *}
    44.1 --- a/src/HOL/NSA/HSeries.thy	Thu Oct 31 16:54:22 2013 +0100
    44.2 +++ b/src/HOL/NSA/HSeries.thy	Fri Nov 01 18:51:14 2013 +0100
    44.3 @@ -131,7 +131,7 @@
    44.4  apply (auto simp add: approx_refl)
    44.5  apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
    44.6  apply (auto dest: approx_hrabs 
    44.7 -            simp add: sumhr_split_diff diff_minus [symmetric])
    44.8 +            simp add: sumhr_split_diff)
    44.9  done
   44.10  
   44.11  (*----------------------------------------------------------------
   44.12 @@ -172,7 +172,7 @@
   44.13  apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
   44.14  apply (rule_tac [2] approx_minus_iff [THEN iffD2])
   44.15  apply (auto dest: approx_hrabs_zero_cancel 
   44.16 -            simp add: sumhr_split_diff diff_minus [symmetric])
   44.17 +            simp add: sumhr_split_diff)
   44.18  done
   44.19  
   44.20  
    45.1 --- a/src/HOL/NSA/HTranscendental.thy	Thu Oct 31 16:54:22 2013 +0100
    45.2 +++ b/src/HOL/NSA/HTranscendental.thy	Fri Nov 01 18:51:14 2013 +0100
    45.3 @@ -258,7 +258,7 @@
    45.4              simp add: mult_assoc)
    45.5  apply (rule approx_add_right_cancel [where d="-1"])
    45.6  apply (rule approx_sym [THEN [2] approx_trans2])
    45.7 -apply (auto simp add: diff_minus mem_infmal_iff)
    45.8 +apply (auto simp add: mem_infmal_iff minus_one [symmetric] simp del: minus_one)
    45.9  done
   45.10  
   45.11  lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
   45.12 @@ -450,7 +450,7 @@
   45.13  apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   45.14              simp add: mult_assoc)
   45.15  apply (rule approx_add_right_cancel [where d = "-1"])
   45.16 -apply (simp add: diff_minus)
   45.17 +apply (simp add: minus_one [symmetric] del: minus_one)
   45.18  done
   45.19  
   45.20  lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
   45.21 @@ -587,7 +587,7 @@
   45.22       "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x\<^sup>2"
   45.23  apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   45.24  apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
   45.25 -            diff_minus add_assoc [symmetric] numeral_2_eq_2)
   45.26 +            add_assoc [symmetric] numeral_2_eq_2)
   45.27  done
   45.28  
   45.29  lemma STAR_cos_Infinitesimal_approx2:
    46.1 --- a/src/HOL/NSA/NSA.thy	Thu Oct 31 16:54:22 2013 +0100
    46.2 +++ b/src/HOL/NSA/NSA.thy	Fri Nov 01 18:51:14 2013 +0100
    46.3 @@ -368,7 +368,7 @@
    46.4  
    46.5  lemma Infinitesimal_diff:
    46.6       "[| x \<in> Infinitesimal;  y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
    46.7 -by (simp add: diff_minus Infinitesimal_add)
    46.8 +  using Infinitesimal_add [of x "- y"] by simp
    46.9  
   46.10  lemma Infinitesimal_mult:
   46.11    fixes x y :: "'a::real_normed_algebra star"
   46.12 @@ -491,7 +491,9 @@
   46.13       "[|(x::hypreal) \<in> HInfinite; y \<le> 0; x \<le> 0|] ==> (x + y): HInfinite"
   46.14  apply (drule HInfinite_minus_iff [THEN iffD2])
   46.15  apply (rule HInfinite_minus_iff [THEN iffD1])
   46.16 -apply (auto intro: HInfinite_add_ge_zero)
   46.17 +apply (simp only: minus_add add.commute)
   46.18 +apply (rule HInfinite_add_ge_zero)
   46.19 +apply simp_all
   46.20  done
   46.21  
   46.22  lemma HInfinite_add_lt_zero:
   46.23 @@ -620,7 +622,7 @@
   46.24  by (simp add: approx_def)
   46.25  
   46.26  lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)"
   46.27 -by (simp add: approx_def diff_minus add_commute)
   46.28 +by (simp add: approx_def add_commute)
   46.29  
   46.30  lemma approx_refl [iff]: "x @= x"
   46.31  by (simp add: approx_def Infinitesimal_def)
   46.32 @@ -637,7 +639,7 @@
   46.33  lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z"
   46.34  apply (simp add: approx_def)
   46.35  apply (drule (1) Infinitesimal_add)
   46.36 -apply (simp add: diff_minus)
   46.37 +apply simp
   46.38  done
   46.39  
   46.40  lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s"
   46.41 @@ -687,7 +689,7 @@
   46.42  lemma approx_minus: "a @= b ==> -a @= -b"
   46.43  apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
   46.44  apply (drule approx_minus_iff [THEN iffD1])
   46.45 -apply (simp add: add_commute diff_minus)
   46.46 +apply (simp add: add_commute)
   46.47  done
   46.48  
   46.49  lemma approx_minus2: "-a @= -b ==> a @= b"
   46.50 @@ -700,7 +702,7 @@
   46.51  by (blast intro!: approx_add approx_minus)
   46.52  
   46.53  lemma approx_diff: "[| a @= b; c @= d |] ==> a - c @= b - d"
   46.54 -by (simp only: diff_minus approx_add approx_minus)
   46.55 +  using approx_add [of a b "- c" "- d"] by simp
   46.56  
   46.57  lemma approx_mult1:
   46.58    fixes a b c :: "'a::real_normed_algebra star"
   46.59 @@ -1213,7 +1215,9 @@
   46.60           r \<in> Reals;  0 < r |]
   46.61        ==> -(x + -t) \<le> r"
   46.62  apply (subgoal_tac "(t + -r \<le> x)") 
   46.63 -apply (auto intro: lemma_st_part_le2)
   46.64 +apply simp
   46.65 +apply (rule lemma_st_part_le2)
   46.66 +apply auto
   46.67  done
   46.68  
   46.69  lemma lemma_SReal_ub:
   46.70 @@ -1238,7 +1242,7 @@
   46.71        ==> x + -t \<noteq> r"
   46.72  apply auto
   46.73  apply (frule isLubD1a [THEN Reals_minus])
   46.74 -apply (drule Reals_add_cancel, assumption)
   46.75 +using Reals_add_cancel [of x "- t"] apply simp
   46.76  apply (drule_tac x = x in lemma_SReal_lub)
   46.77  apply (drule hypreal_isLub_unique, assumption, auto)
   46.78  done
   46.79 @@ -1250,8 +1254,7 @@
   46.80        ==> -(x + -t) \<noteq> r"
   46.81  apply (auto)
   46.82  apply (frule isLubD1a)
   46.83 -apply (drule Reals_add_cancel, assumption)
   46.84 -apply (drule_tac a = "-x" in Reals_minus, simp)
   46.85 +using Reals_add_cancel [of "- x" t] apply simp
   46.86  apply (drule_tac x = x in lemma_SReal_lub)
   46.87  apply (drule hypreal_isLub_unique, assumption, auto)
   46.88  done
    47.1 --- a/src/HOL/NSA/NSCA.thy	Thu Oct 31 16:54:22 2013 +0100
    47.2 +++ b/src/HOL/NSA/NSCA.thy	Fri Nov 01 18:51:14 2013 +0100
    47.3 @@ -165,7 +165,7 @@
    47.4  
    47.5  lemma approx_hcmod_approx_zero: "(x @= y) = (hcmod (y - x) @= 0)"
    47.6  apply (subst hnorm_minus_commute)
    47.7 -apply (simp add: approx_def Infinitesimal_hcmod_iff diff_minus)
    47.8 +apply (simp add: approx_def Infinitesimal_hcmod_iff)
    47.9  done
   47.10  
   47.11  lemma approx_approx_zero_iff: "(x @= 0) = (hcmod x @= 0)"
   47.12 @@ -178,14 +178,14 @@
   47.13       "u @= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
   47.14  apply (drule approx_approx_zero_iff [THEN iffD1])
   47.15  apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
   47.16 -apply (auto simp add: mem_infmal_iff [symmetric] diff_minus)
   47.17 +apply (auto simp add: mem_infmal_iff [symmetric])
   47.18  apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1])
   47.19 -apply (auto simp add: diff_minus [symmetric])
   47.20 +apply auto
   47.21  done
   47.22  
   47.23  lemma approx_hcmod_add_hcmod: "u @= 0 ==> hcmod(x + u) @= hcmod x"
   47.24  apply (rule approx_minus_iff [THEN iffD2])
   47.25 -apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric])
   47.26 +apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric])
   47.27  done
   47.28  
   47.29  
    48.1 --- a/src/HOL/NSA/StarDef.thy	Thu Oct 31 16:54:22 2013 +0100
    48.2 +++ b/src/HOL/NSA/StarDef.thy	Fri Nov 01 18:51:14 2013 +0100
    48.3 @@ -803,7 +803,7 @@
    48.4  instance star :: (ab_group_add) ab_group_add
    48.5  apply (intro_classes)
    48.6  apply (transfer, rule left_minus)
    48.7 -apply (transfer, rule diff_minus)
    48.8 +apply (transfer, rule diff_conv_add_uminus)
    48.9  done
   48.10  
   48.11  instance star :: (ordered_ab_semigroup_add) ordered_ab_semigroup_add
    49.1 --- a/src/HOL/Num.thy	Thu Oct 31 16:54:22 2013 +0100
    49.2 +++ b/src/HOL/Num.thy	Fri Nov 01 18:51:14 2013 +0100
    49.3 @@ -407,7 +407,7 @@
    49.4    apply (simp add: add_assoc [symmetric], simp add: add_assoc)
    49.5    apply (rule_tac a=x in add_left_imp_eq)
    49.6    apply (rule_tac a=x in add_right_imp_eq)
    49.7 -  apply (simp add: add_assoc minus_add_cancel add_minus_cancel)
    49.8 +  apply (simp add: add_assoc)
    49.9    apply (simp add: add_assoc, simp add: add_assoc [symmetric])
   49.10    done
   49.11  
   49.12 @@ -418,7 +418,7 @@
   49.13  lemmas is_num_normalize =
   49.14    add_assoc is_num_add_commute is_num_add_left_commute
   49.15    is_num.intros is_num_numeral
   49.16 -  diff_minus minus_add add_minus_cancel minus_add_cancel
   49.17 +  minus_add
   49.18  
   49.19  definition dbl :: "'a \<Rightarrow> 'a" where "dbl x = x + x"
   49.20  definition dbl_inc :: "'a \<Rightarrow> 'a" where "dbl_inc x = x + x + 1"
   49.21 @@ -435,24 +435,21 @@
   49.22    "dbl 0 = 0"
   49.23    "dbl 1 = 2"
   49.24    "dbl (numeral k) = numeral (Bit0 k)"
   49.25 -  unfolding dbl_def neg_numeral_def numeral.simps
   49.26 -  by (simp_all add: minus_add)
   49.27 +  by (simp_all add: dbl_def neg_numeral_def numeral.simps minus_add)
   49.28  
   49.29  lemma dbl_inc_simps [simp]:
   49.30    "dbl_inc (neg_numeral k) = neg_numeral (BitM k)"
   49.31    "dbl_inc 0 = 1"
   49.32    "dbl_inc 1 = 3"
   49.33    "dbl_inc (numeral k) = numeral (Bit1 k)"
   49.34 -  unfolding dbl_inc_def neg_numeral_def numeral.simps numeral_BitM
   49.35 -  by (simp_all add: is_num_normalize)
   49.36 +  by (simp_all add: dbl_inc_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize algebra_simps del: add_uminus_conv_diff)
   49.37  
   49.38  lemma dbl_dec_simps [simp]:
   49.39    "dbl_dec (neg_numeral k) = neg_numeral (Bit1 k)"
   49.40    "dbl_dec 0 = -1"
   49.41    "dbl_dec 1 = 1"
   49.42    "dbl_dec (numeral k) = numeral (BitM k)"
   49.43 -  unfolding dbl_dec_def neg_numeral_def numeral.simps numeral_BitM
   49.44 -  by (simp_all add: is_num_normalize)
   49.45 +  by (simp_all add: dbl_dec_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize)
   49.46  
   49.47  lemma sub_num_simps [simp]:
   49.48    "sub One One = 0"
   49.49 @@ -464,38 +461,35 @@
   49.50    "sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)"
   49.51    "sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)"
   49.52    "sub (Bit1 k) (Bit1 l) = dbl (sub k l)"
   49.53 -  unfolding dbl_def dbl_dec_def dbl_inc_def sub_def
   49.54 -  unfolding neg_numeral_def numeral.simps numeral_BitM
   49.55 -  by (simp_all add: is_num_normalize)
   49.56 +  by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def neg_numeral_def numeral.simps
   49.57 +    numeral_BitM is_num_normalize del: add_uminus_conv_diff add: diff_conv_add_uminus)
   49.58  
   49.59  lemma add_neg_numeral_simps:
   49.60    "numeral m + neg_numeral n = sub m n"
   49.61    "neg_numeral m + numeral n = sub n m"
   49.62    "neg_numeral m + neg_numeral n = neg_numeral (m + n)"
   49.63 -  unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps
   49.64 -  by (simp_all add: is_num_normalize)
   49.65 +  by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize
   49.66 +    del: add_uminus_conv_diff add: diff_conv_add_uminus)
   49.67  
   49.68  lemma add_neg_numeral_special:
   49.69    "1 + neg_numeral m = sub One m"
   49.70    "neg_numeral m + 1 = sub One m"
   49.71 -  unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps
   49.72 -  by (simp_all add: is_num_normalize)
   49.73 +  by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize)
   49.74  
   49.75  lemma diff_numeral_simps:
   49.76    "numeral m - numeral n = sub m n"
   49.77    "numeral m - neg_numeral n = numeral (m + n)"
   49.78    "neg_numeral m - numeral n = neg_numeral (m + n)"
   49.79    "neg_numeral m - neg_numeral n = sub n m"
   49.80 -  unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps
   49.81 -  by (simp_all add: is_num_normalize)
   49.82 +  by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps is_num_normalize
   49.83 +    del: add_uminus_conv_diff add: diff_conv_add_uminus)
   49.84  
   49.85  lemma diff_numeral_special:
   49.86    "1 - numeral n = sub One n"
   49.87    "1 - neg_numeral n = numeral (One + n)"
   49.88    "numeral m - 1 = sub m One"
   49.89    "neg_numeral m - 1 = neg_numeral (m + One)"
   49.90 -  unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps
   49.91 -  by (simp_all add: is_num_normalize)
   49.92 +  by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps add: is_num_normalize)
   49.93  
   49.94  lemma minus_one: "- 1 = -1"
   49.95    unfolding neg_numeral_def numeral.simps ..
    50.1 --- a/src/HOL/Number_Theory/Cong.thy	Thu Oct 31 16:54:22 2013 +0100
    50.2 +++ b/src/HOL/Number_Theory/Cong.thy	Fri Nov 01 18:51:14 2013 +0100
    50.3 @@ -543,7 +543,8 @@
    50.4    apply (subgoal_tac "a * b = (-a * -b)")
    50.5    apply (erule ssubst)
    50.6    apply (subst zmod_zmult2_eq)
    50.7 -  apply (auto simp add: mod_add_left_eq)
    50.8 +  apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right)
    50.9 +  apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 semiring_numeral_div_class.diff_zero)+
   50.10    done
   50.11  
   50.12  lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
    51.1 --- a/src/HOL/Probability/Borel_Space.thy	Thu Oct 31 16:54:22 2013 +0100
    51.2 +++ b/src/HOL/Probability/Borel_Space.thy	Fri Nov 01 18:51:14 2013 +0100
    51.3 @@ -677,7 +677,7 @@
    51.4    assumes f: "f \<in> borel_measurable M"
    51.5    assumes g: "g \<in> borel_measurable M"
    51.6    shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
    51.7 -  unfolding diff_minus using assms by simp
    51.8 +  using borel_measurable_add [of f M "- g"] assms by (simp add: fun_Compl_def)
    51.9  
   51.10  lemma borel_measurable_times[measurable (raw)]:
   51.11    fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_algebra}"
   51.12 @@ -719,7 +719,8 @@
   51.13    proof cases
   51.14      assume "b \<noteq> 0"
   51.15      with `open S` have "open ((\<lambda>x. (- a + x) /\<^sub>R b) ` S)" (is "open ?S")
   51.16 -      by (auto intro!: open_affinity simp: scaleR_add_right)
   51.17 +      using open_affinity [of S "inverse b" "- a /\<^sub>R b"]
   51.18 +      by (auto simp: algebra_simps)
   51.19      hence "?S \<in> sets borel" by auto
   51.20      moreover
   51.21      from `b \<noteq> 0` have "(\<lambda>x. a + b *\<^sub>R f x) -` S = f -` ?S"
    52.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Oct 31 16:54:22 2013 +0100
    52.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 01 18:51:14 2013 +0100
    52.3 @@ -1528,7 +1528,7 @@
    52.4      using mono by auto
    52.5    ultimately show ?thesis using fg
    52.6      by (auto intro!: add_mono positive_integral_mono_AE real_of_ereal_positive_mono
    52.7 -             simp: positive_integral_positive lebesgue_integral_def diff_minus)
    52.8 +             simp: positive_integral_positive lebesgue_integral_def algebra_simps)
    52.9  qed
   52.10  
   52.11  lemma integral_mono:
   52.12 @@ -1732,7 +1732,7 @@
   52.13    shows "integrable M (\<lambda>t. f t - g t)"
   52.14    and "(\<integral> t. f t - g t \<partial>M) = integral\<^sup>L M f - integral\<^sup>L M g"
   52.15    using integral_add[OF f integral_minus(1)[OF g]]
   52.16 -  unfolding diff_minus integral_minus(2)[OF g]
   52.17 +  unfolding integral_minus(2)[OF g]
   52.18    by auto
   52.19  
   52.20  lemma integral_indicator[simp, intro]:
    53.1 --- a/src/HOL/Rat.thy	Thu Oct 31 16:54:22 2013 +0100
    53.2 +++ b/src/HOL/Rat.thy	Fri Nov 01 18:51:14 2013 +0100
    53.3 @@ -468,7 +468,7 @@
    53.4      unfolding less_eq_rat_def less_rat_def
    53.5      by (auto, drule (1) positive_add, simp add: positive_zero)
    53.6    show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
    53.7 -    unfolding less_eq_rat_def less_rat_def by (auto simp: diff_minus)
    53.8 +    unfolding less_eq_rat_def less_rat_def by auto
    53.9    show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
   53.10      by (rule sgn_rat_def)
   53.11    show "a \<le> b \<or> b \<le> a"
   53.12 @@ -665,7 +665,7 @@
   53.13    by transfer simp
   53.14  
   53.15  lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b"
   53.16 -by (simp only: diff_minus of_rat_add of_rat_minus)
   53.17 +  using of_rat_add [of a "- b"] by (simp add: of_rat_minus)
   53.18  
   53.19  lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b"
   53.20  apply transfer
    54.1 --- a/src/HOL/Real.thy	Thu Oct 31 16:54:22 2013 +0100
    54.2 +++ b/src/HOL/Real.thy	Fri Nov 01 18:51:14 2013 +0100
    54.3 @@ -98,7 +98,7 @@
    54.4  lemma vanishes_diff:
    54.5    assumes X: "vanishes X" and Y: "vanishes Y"
    54.6    shows "vanishes (\<lambda>n. X n - Y n)"
    54.7 -unfolding diff_minus by (intro vanishes_add vanishes_minus X Y)
    54.8 +  unfolding diff_conv_add_uminus by (intro vanishes_add vanishes_minus X Y)
    54.9  
   54.10  lemma vanishes_mult_bounded:
   54.11    assumes X: "\<exists>a>0. \<forall>n. \<bar>X n\<bar> < a"
   54.12 @@ -170,7 +170,7 @@
   54.13  lemma cauchy_diff [simp]:
   54.14    assumes X: "cauchy X" and Y: "cauchy Y"
   54.15    shows "cauchy (\<lambda>n. X n - Y n)"
   54.16 -using assms unfolding diff_minus by simp
   54.17 +  using assms unfolding diff_conv_add_uminus by (simp del: add_uminus_conv_diff)
   54.18  
   54.19  lemma cauchy_imp_bounded:
   54.20    assumes "cauchy X" shows "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"
   54.21 @@ -456,7 +456,7 @@
   54.22  lemma diff_Real:
   54.23    assumes X: "cauchy X" and Y: "cauchy Y"
   54.24    shows "Real X - Real Y = Real (\<lambda>n. X n - Y n)"
   54.25 -  unfolding minus_real_def diff_minus
   54.26 +  unfolding minus_real_def
   54.27    by (simp add: minus_Real add_Real X Y)
   54.28  
   54.29  lemma mult_Real:
   54.30 @@ -607,7 +607,7 @@
   54.31      unfolding less_eq_real_def less_real_def
   54.32      by (auto, drule (1) positive_add, simp add: positive_zero)
   54.33    show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   54.34 -    unfolding less_eq_real_def less_real_def by (auto simp: diff_minus) (* by auto *)
   54.35 +    unfolding less_eq_real_def less_real_def by auto
   54.36      (* FIXME: Procedure int_combine_numerals: c + b - (c + a) \<equiv> b + - a *)
   54.37      (* Should produce c + b - (c + a) \<equiv> b - a *)
   54.38    show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
    55.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Oct 31 16:54:22 2013 +0100
    55.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Fri Nov 01 18:51:14 2013 +0100
    55.3 @@ -31,7 +31,7 @@
    55.4  qed
    55.5  
    55.6  lemma diff: "f (x - y) = f x - f y"
    55.7 -by (simp add: add minus diff_minus)
    55.8 +  using add [of x "- y"] by (simp add: minus)
    55.9  
   55.10  lemma setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))"
   55.11  apply (cases "finite A")
   55.12 @@ -553,8 +553,7 @@
   55.13  proof -
   55.14    have "norm (a + - b) \<le> norm a + norm (- b)"
   55.15      by (rule norm_triangle_ineq)
   55.16 -  thus ?thesis
   55.17 -    by (simp only: diff_minus norm_minus_cancel)
   55.18 +  then show ?thesis by simp
   55.19  qed
   55.20  
   55.21  lemma norm_diff_ineq:
   55.22 @@ -571,7 +570,7 @@
   55.23    shows "norm ((a + b) - (c + d)) \<le> norm (a - c) + norm (b - d)"
   55.24  proof -
   55.25    have "norm ((a + b) - (c + d)) = norm ((a - c) + (b - d))"
   55.26 -    by (simp add: diff_minus add_ac)
   55.27 +    by (simp add: algebra_simps)
   55.28    also have "\<dots> \<le> norm (a - c) + norm (b - d)"
   55.29      by (rule norm_triangle_ineq)
   55.30    finally show ?thesis .
    56.1 --- a/src/HOL/Rings.thy	Thu Oct 31 16:54:22 2013 +0100
    56.2 +++ b/src/HOL/Rings.thy	Fri Nov 01 18:51:14 2013 +0100
    56.3 @@ -255,11 +255,13 @@
    56.4  lemma minus_mult_commute: "- a * b = a * - b"
    56.5  by simp
    56.6  
    56.7 -lemma right_diff_distrib[algebra_simps, field_simps]: "a * (b - c) = a * b - a * c"
    56.8 -by (simp add: distrib_left diff_minus)
    56.9 +lemma right_diff_distrib [algebra_simps, field_simps]:
   56.10 +  "a * (b - c) = a * b - a * c"
   56.11 +  using distrib_left [of a b "-c "] by simp
   56.12  
   56.13 -lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"
   56.14 -by (simp add: distrib_right diff_minus)
   56.15 +lemma left_diff_distrib [algebra_simps, field_simps]:
   56.16 +  "(a - b) * c = a * c - b * c"
   56.17 +  using distrib_right [of a "- b" c] by simp
   56.18  
   56.19  lemmas ring_distribs =
   56.20    distrib_left distrib_right left_diff_distrib right_diff_distrib
   56.21 @@ -331,8 +333,9 @@
   56.22    then show "- x dvd y" ..
   56.23  qed
   56.24  
   56.25 -lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
   56.26 -by (simp only: diff_minus dvd_add dvd_minus_iff)
   56.27 +lemma dvd_diff [simp]:
   56.28 +  "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
   56.29 +  using dvd_add [of x y "- z"] by simp
   56.30  
   56.31  end
   56.32  
   56.33 @@ -755,9 +758,7 @@
   56.34  proof
   56.35    fix a b
   56.36    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   56.37 -    by (auto simp add: abs_if not_less)
   56.38 -    (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],
   56.39 -     auto intro!: less_imp_le add_neg_neg)
   56.40 +    by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)
   56.41  qed (auto simp add: abs_if)
   56.42  
   56.43  lemma zero_le_square [simp]: "0 \<le> a * a"
    57.1 --- a/src/HOL/Semiring_Normalization.thy	Thu Oct 31 16:54:22 2013 +0100
    57.2 +++ b/src/HOL/Semiring_Normalization.thy	Fri Nov 01 18:51:14 2013 +0100
    57.3 @@ -137,7 +137,7 @@
    57.4  lemma normalizing_ring_rules:
    57.5    "- x = (- 1) * x"
    57.6    "x - y = x + (- y)"
    57.7 -  by (simp_all add: diff_minus)
    57.8 +  by simp_all
    57.9  
   57.10  lemmas normalizing_comm_ring_1_axioms =
   57.11    comm_ring_1_axioms [normalizer
    58.1 --- a/src/HOL/Series.thy	Thu Oct 31 16:54:22 2013 +0100
    58.2 +++ b/src/HOL/Series.thy	Fri Nov 01 18:51:14 2013 +0100
    58.3 @@ -34,7 +34,7 @@
    58.4  
    58.5  lemma sumr_diff_mult_const:
    58.6   "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
    58.7 -by (simp add: diff_minus setsum_addf real_of_nat_def)
    58.8 +  by (simp add: setsum_subtractf real_of_nat_def)
    58.9  
   58.10  lemma real_setsum_nat_ivl_bounded:
   58.11       "(!!p. p < n \<Longrightarrow> f(p) \<le> K)
    59.1 --- a/src/HOL/Tools/group_cancel.ML	Thu Oct 31 16:54:22 2013 +0100
    59.2 +++ b/src/HOL/Tools/group_cancel.ML	Fri Nov 01 18:51:14 2013 +0100
    59.3 @@ -25,7 +25,7 @@
    59.4  val sub1 = @{lemma "(A::'a::ab_group_add) == k + a ==> A - b == k + (a - b)"
    59.5        by (simp only: add_diff_eq)}
    59.6  val sub2 = @{lemma "(B::'a::ab_group_add) == k + b ==> a - B == - k + (a - b)"
    59.7 -      by (simp only: diff_minus minus_add add_ac)}
    59.8 +      by (simp only: minus_add diff_conv_add_uminus add_ac)}
    59.9  val neg1 = @{lemma "(A::'a::ab_group_add) == k + a ==> - A == - k + - a"
   59.10        by (simp only: minus_add_distrib)}
   59.11  val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
    60.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 31 16:54:22 2013 +0100
    60.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Nov 01 18:51:14 2013 +0100
    60.3 @@ -220,7 +220,7 @@
    60.4  val minus_simps = [@{thm minus_zero}, @{thm minus_one}, @{thm minus_numeral}, @{thm minus_neg_numeral}];
    60.5  
    60.6  (*To let us treat subtraction as addition*)
    60.7 -val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}];
    60.8 +val diff_simps = [@{thm diff_conv_add_uminus}, @{thm minus_add_distrib}, @{thm minus_minus}];
    60.9  
   60.10  (*To let us treat division as multiplication*)
   60.11  val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
   60.12 @@ -719,7 +719,7 @@
   60.13             @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
   60.14             @{thm "times_divide_times_eq"},
   60.15             @{thm "divide_divide_eq_right"},
   60.16 -           @{thm "diff_minus"}, @{thm "minus_divide_left"},
   60.17 +           @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"},
   60.18             @{thm "add_divide_distrib"} RS sym,
   60.19             @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, 
   60.20             Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute}))))   
    61.1 --- a/src/HOL/Transcendental.thy	Thu Oct 31 16:54:22 2013 +0100
    61.2 +++ b/src/HOL/Transcendental.thy	Fri Nov 01 18:51:14 2013 +0100
    61.3 @@ -453,7 +453,7 @@
    61.4    apply simp
    61.5    apply (simp only: lemma_termdiff1 setsum_right_distrib)
    61.6    apply (rule setsum_cong [OF refl])
    61.7 -  apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
    61.8 +  apply (simp add: less_iff_Suc_add)
    61.9    apply (clarify)
   61.10    apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
   61.11                del: setsum_op_ivl_Suc power_Suc)
   61.12 @@ -1129,8 +1129,7 @@
   61.13    by (rule inverse_unique [symmetric], simp add: mult_exp_exp)
   61.14  
   61.15  lemma exp_diff: "exp (x - y) = exp x / exp y"
   61.16 -  unfolding diff_minus divide_inverse
   61.17 -  by (simp add: exp_add exp_minus)
   61.18 +  using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
   61.19  
   61.20  
   61.21  subsubsection {* Properties of the Exponential Function on Reals *}
   61.22 @@ -2410,13 +2409,13 @@
   61.23    using sin_cos_minus_lemma [where x=x] by simp
   61.24  
   61.25  lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
   61.26 -  by (simp add: diff_minus sin_add)
   61.27 +  using sin_add [of x "- y"] by simp
   61.28  
   61.29  lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
   61.30    by (simp add: sin_diff mult_commute)
   61.31  
   61.32  lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
   61.33 -  by (simp add: diff_minus cos_add)
   61.34 +  using cos_add [of x "- y"] by simp
   61.35  
   61.36  lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
   61.37    by (simp add: cos_diff mult_commute)
   61.38 @@ -2526,8 +2525,9 @@
   61.39          by (simp add: inverse_eq_divide less_divide_eq)
   61.40      }
   61.41      note *** = this
   61.42 +    have [simp]: "\<And>x y::real. 0 < x - y \<longleftrightarrow> y < x" by arith
   61.43      from ** show ?thesis by (rule sumr_pos_lt_pair)
   61.44 -      (simp add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] ***)
   61.45 +      (simp add: divide_inverse mult_assoc [symmetric] ***)
   61.46    qed
   61.47    ultimately have "0 < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   61.48      by (rule order_less_trans)
   61.49 @@ -2810,7 +2810,7 @@
   61.50  apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
   61.51  apply (force simp add: minus_equation_iff [of x])
   61.52  apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
   61.53 -apply (auto simp add: cos_add)
   61.54 +apply (auto simp add: cos_diff cos_add)
   61.55  done
   61.56  
   61.57  (* ditto: but to a lesser extent *)
   61.58 @@ -3833,7 +3833,7 @@
   61.59                by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
   61.60              from DERIV_add_minus[OF this DERIV_arctan]
   61.61              show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
   61.62 -              unfolding diff_minus by auto
   61.63 +              by auto
   61.64            qed
   61.65            hence DERIV_in_rball: "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
   61.66              using `-r < a` `b < r` by auto
   61.67 @@ -3922,9 +3922,10 @@
   61.68        }
   61.69        hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
   61.70        moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
   61.71 -        unfolding diff_minus divide_inverse
   61.72 +        unfolding diff_conv_add_uminus divide_inverse
   61.73          by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan
   61.74 -          isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum)
   61.75 +          isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum
   61.76 +          simp del: add_uminus_conv_diff)
   61.77        ultimately have "0 \<le> ?a 1 n - ?diff 1 n"
   61.78          by (rule LIM_less_bound)
   61.79        hence "?diff 1 n \<le> ?a 1 n" by auto
    62.1 --- a/src/HOL/Word/Bit_Representation.thy	Thu Oct 31 16:54:22 2013 +0100
    62.2 +++ b/src/HOL/Word/Bit_Representation.thy	Fri Nov 01 18:51:14 2013 +0100
    62.3 @@ -636,12 +636,12 @@
    62.4    unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp
    62.5  
    62.6  lemma sb_dec_lem:
    62.7 -  "(0::int) <= - (2^k) + a ==> (a + 2^k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
    62.8 -  by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified])
    62.9 +  "(0::int) \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
   62.10 +  using int_mod_le'[where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"] by simp
   62.11  
   62.12  lemma sb_dec_lem':
   62.13 -  "(2::int) ^ k <= a ==> (a + 2 ^ k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
   62.14 -  by (rule iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified])
   62.15 +  "(2::int) ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
   62.16 +  by (rule sb_dec_lem) simp
   62.17  
   62.18  lemma sbintrunc_dec:
   62.19    "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
    63.1 --- a/src/HOL/Word/WordBitwise.thy	Thu Oct 31 16:54:22 2013 +0100
    63.2 +++ b/src/HOL/Word/WordBitwise.thy	Fri Nov 01 18:51:14 2013 +0100
    63.3 @@ -65,7 +65,7 @@
    63.4  
    63.5  lemma bl_word_sub:
    63.6    "to_bl (x - y) = to_bl (x + (- y))"
    63.7 -  by (simp add: diff_def)
    63.8 +  by simp
    63.9  
   63.10  lemma rbl_word_1:
   63.11    "rev (to_bl (1 :: ('a :: len0) word))
    64.1 --- a/src/HOL/ex/Dedekind_Real.thy	Thu Oct 31 16:54:22 2013 +0100
    64.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Fri Nov 01 18:51:14 2013 +0100
    64.3 @@ -1520,14 +1520,14 @@
    64.4    have "z + x - (z + y) = (z + -z) + (x - y)" 
    64.5      by (simp add: algebra_simps) 
    64.6    with le show ?thesis 
    64.7 -    by (simp add: real_le_eq_diff[of x] real_le_eq_diff[of "z+x"] diff_minus)
    64.8 +    by (simp add: real_le_eq_diff[of x] real_le_eq_diff[of "z+x"])
    64.9  qed
   64.10  
   64.11  lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)"
   64.12 -by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus)
   64.13 +by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S])
   64.14  
   64.15  lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))"
   64.16 -by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus)
   64.17 +by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S])
   64.18  
   64.19  lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y"
   64.20  apply (cases x, cases y)
   64.21 @@ -1543,7 +1543,7 @@
   64.22  apply (rule real_sum_gt_zero_less)
   64.23  apply (drule real_less_sum_gt_zero [of x y])
   64.24  apply (drule real_mult_order, assumption)
   64.25 -apply (simp add: distrib_left)
   64.26 +apply (simp add: algebra_simps)
   64.27  done
   64.28  
   64.29  instantiation real :: distrib_lattice
    65.1 --- a/src/HOL/ex/Gauge_Integration.thy	Thu Oct 31 16:54:22 2013 +0100
    65.2 +++ b/src/HOL/ex/Gauge_Integration.thy	Fri Nov 01 18:51:14 2013 +0100
    65.3 @@ -511,9 +511,9 @@
    65.4    case False
    65.5    then have "inverse (z - x) * (f z - f x - f' x * (z - x)) = (f z - f x) / (z - x) - f' x"
    65.6      apply (subst mult_commute)
    65.7 -    apply (simp add: distrib_right diff_minus)
    65.8 +    apply (simp add: left_diff_distrib)
    65.9      apply (simp add: mult_assoc divide_inverse)
   65.10 -    apply (simp add: distrib_right)
   65.11 +    apply (simp add: ring_distribs)
   65.12      done
   65.13    moreover from False `\<bar>z - x\<bar> < s` have "\<bar>(f z - f x) / (z - x) - f' x\<bar> < e / 2"
   65.14      by (rule P)