diff_minus subsumes diff_def
authorhaftmann
Mon Jul 19 16:09:44 2010 +0200 (2010-07-19)
changeset 378872ae085b07f2f
parent 37886 2f9d3fc1a8ac
child 37888 d78a3cdbd615
diff_minus subsumes diff_def
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/mir_tac.ML
src/HOL/Deriv.thy
src/HOL/Hahn_Banach/Vector_Space.thy
src/HOL/Import/HOL/poly.imp
src/HOL/Import/HOL/real.imp
src/HOL/Int.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/NSA/HDeriv.thy
src/HOL/NSA/HLim.thy
src/HOL/NSA/HTranscendental.thy
src/HOL/NSA/NSA.thy
src/HOL/NSA/NSCA.thy
src/HOL/Probability/Borel.thy
src/HOL/RComplete.thy
src/HOL/RealVector.thy
src/HOL/SEQ.thy
src/HOL/SupInf.thy
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Transcendental.thy
src/HOL/Word/Misc_Numeric.thy
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Complex.thy	Mon Jul 19 16:09:44 2010 +0200
     1.2 +++ b/src/HOL/Complex.thy	Mon Jul 19 16:09:44 2010 +0200
     1.3 @@ -686,12 +686,12 @@
     1.4  by (simp add: divide_inverse rcis_def)
     1.5  
     1.6  lemma cis_divide: "cis a / cis b = cis (a - b)"
     1.7 -by (simp add: complex_divide_def cis_mult diff_def)
     1.8 +by (simp add: complex_divide_def cis_mult diff_minus)
     1.9  
    1.10  lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
    1.11  apply (simp add: complex_divide_def)
    1.12  apply (case_tac "r2=0", simp)
    1.13 -apply (simp add: rcis_inverse rcis_mult diff_def)
    1.14 +apply (simp add: rcis_inverse rcis_mult diff_minus)
    1.15  done
    1.16  
    1.17  lemma Re_cis [simp]: "Re(cis a) = cos a"
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Mon Jul 19 16:09:44 2010 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Jul 19 16:09:44 2010 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4    shows "a 0 - x * (\<Sum> i=0..<n. (-1)^i * a (Suc i) * x^i) = (\<Sum> i=0..<Suc n. (-1)^i * a i * x^i)"
     2.5  proof -
     2.6    have shift_pow: "\<And>i. - (x * ((-1)^i * a (Suc i) * x ^ i)) = (-1)^(Suc i) * a (Suc i) * x ^ (Suc i)" by auto
     2.7 -  show ?thesis unfolding setsum_right_distrib shift_pow diff_def setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
     2.8 +  show ?thesis unfolding setsum_right_distrib shift_pow diff_minus setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
     2.9      setsum_reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\<lambda> n. (-1)^n  *a n * x^n"] by auto
    2.10  qed
    2.11  
    2.12 @@ -45,14 +45,14 @@
    2.13    case 0 thus ?case unfolding lb_0 ub_0 horner.simps by auto
    2.14  next
    2.15    case (Suc n)
    2.16 -  have "?lb (Suc n) j' \<le> ?horner (Suc n) j'" unfolding lb_Suc ub_Suc horner.simps real_of_float_sub diff_def
    2.17 +  have "?lb (Suc n) j' \<le> ?horner (Suc n) j'" unfolding lb_Suc ub_Suc horner.simps real_of_float_sub diff_minus
    2.18    proof (rule add_mono)
    2.19      show "real (lapprox_rat prec 1 (int (f j'))) \<le> 1 / real (f j')" using lapprox_rat[of prec 1  "int (f j')"] by auto
    2.20      from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct2] `0 \<le> real x`
    2.21      show "- real (x * ub n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) x) \<le> - (real x * horner F G n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) (real x))"
    2.22        unfolding real_of_float_mult neg_le_iff_le by (rule mult_left_mono)
    2.23    qed
    2.24 -  moreover have "?horner (Suc n) j' \<le> ?ub (Suc n) j'" unfolding ub_Suc ub_Suc horner.simps real_of_float_sub diff_def
    2.25 +  moreover have "?horner (Suc n) j' \<le> ?ub (Suc n) j'" unfolding ub_Suc ub_Suc horner.simps real_of_float_sub diff_minus
    2.26    proof (rule add_mono)
    2.27      show "1 / real (f j') \<le> real (rapprox_rat prec 1 (int (f j')))" using rapprox_rat[of 1 "int (f j')" prec] by auto
    2.28      from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct1] `0 \<le> real x`
    2.29 @@ -1213,7 +1213,7 @@
    2.30            round_down[of prec "lb_pi prec"] by auto
    2.31    hence "real ?lx \<le> x - real k * 2 * pi \<and> x - real k * 2 * pi \<le> real ?ux"
    2.32      using x by (cases "k = 0") (auto intro!: add_mono
    2.33 -                simp add: diff_def k[symmetric] less_float_def)
    2.34 +                simp add: diff_minus k[symmetric] less_float_def)
    2.35    note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]
    2.36    hence lx_less_ux: "real ?lx \<le> real ?ux" by (rule order_trans)
    2.37  
    2.38 @@ -1227,7 +1227,7 @@
    2.39      also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
    2.40        using cos_monotone_minus_pi_0'[OF pi_lx lx x_le_0]
    2.41        by (simp only: real_of_float_minus real_of_int_minus
    2.42 -        cos_minus diff_def mult_minus_left)
    2.43 +        cos_minus diff_minus mult_minus_left)
    2.44      finally have "real (lb_cos prec (- ?lx)) \<le> cos x"
    2.45        unfolding cos_periodic_int . }
    2.46    note negative_lx = this
    2.47 @@ -1240,7 +1240,7 @@
    2.48      have "cos (x + real (-k) * 2 * pi) \<le> cos (real ?lx)"
    2.49        using cos_monotone_0_pi'[OF lx_0 lx pi_x]
    2.50        by (simp only: real_of_float_minus real_of_int_minus
    2.51 -        cos_minus diff_def mult_minus_left)
    2.52 +        cos_minus diff_minus mult_minus_left)
    2.53      also have "\<dots> \<le> real (ub_cos prec ?lx)"
    2.54        using lb_cos[OF lx_0 pi_lx] by simp
    2.55      finally have "cos x \<le> real (ub_cos prec ?lx)"
    2.56 @@ -1255,7 +1255,7 @@
    2.57      have "cos (x + real (-k) * 2 * pi) \<le> cos (real (- ?ux))"
    2.58        using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
    2.59        by (simp only: real_of_float_minus real_of_int_minus
    2.60 -          cos_minus diff_def mult_minus_left)
    2.61 +          cos_minus diff_minus mult_minus_left)
    2.62      also have "\<dots> \<le> real (ub_cos prec (- ?ux))"
    2.63        using lb_cos_minus[OF pi_ux ux_0, of prec] by simp
    2.64      finally have "cos x \<le> real (ub_cos prec (- ?ux))"
    2.65 @@ -1272,7 +1272,7 @@
    2.66      also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
    2.67        using cos_monotone_0_pi'[OF x_ge_0 ux pi_ux]
    2.68        by (simp only: real_of_float_minus real_of_int_minus
    2.69 -        cos_minus diff_def mult_minus_left)
    2.70 +        cos_minus diff_minus mult_minus_left)
    2.71      finally have "real (lb_cos prec ?ux) \<le> cos x"
    2.72        unfolding cos_periodic_int . }
    2.73    note positive_ux = this
    2.74 @@ -1347,7 +1347,7 @@
    2.75        also have "\<dots> \<le> cos (real (?ux - 2 * ?lpi))"
    2.76          using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
    2.77          by (simp only: real_of_float_minus real_of_int_minus real_of_one
    2.78 -            number_of_Min diff_def mult_minus_left mult_1_left)
    2.79 +            number_of_Min diff_minus mult_minus_left mult_1_left)
    2.80        also have "\<dots> = cos (real (- (?ux - 2 * ?lpi)))"
    2.81          unfolding real_of_float_minus cos_minus ..
    2.82        also have "\<dots> \<le> real (ub_cos prec (- (?ux - 2 * ?lpi)))"
    2.83 @@ -1391,7 +1391,7 @@
    2.84        also have "\<dots> \<le> cos (real (?lx + 2 * ?lpi))"
    2.85          using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
    2.86          by (simp only: real_of_float_minus real_of_int_minus real_of_one
    2.87 -          number_of_Min diff_def mult_minus_left mult_1_left)
    2.88 +          number_of_Min diff_minus mult_minus_left mult_1_left)
    2.89        also have "\<dots> \<le> real (ub_cos prec (?lx + 2 * ?lpi))"
    2.90          using lb_cos[OF lx_0 pi_lx] by simp
    2.91        finally show ?thesis unfolding u by (simp add: real_of_float_max)
    2.92 @@ -2091,12 +2091,12 @@
    2.93    unfolding divide_inverse interpret_floatarith.simps ..
    2.94  
    2.95  lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
    2.96 -  unfolding diff_def interpret_floatarith.simps ..
    2.97 +  unfolding diff_minus interpret_floatarith.simps ..
    2.98  
    2.99  lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
   2.100    sin (interpret_floatarith a vs)"
   2.101    unfolding sin_cos_eq interpret_floatarith.simps
   2.102 -            interpret_floatarith_divide interpret_floatarith_diff diff_def
   2.103 +            interpret_floatarith_divide interpret_floatarith_diff diff_minus
   2.104    by auto
   2.105  
   2.106  lemma interpret_floatarith_tan:
     3.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Mon Jul 19 16:09:44 2010 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Mon Jul 19 16:09:44 2010 +0200
     3.3 @@ -1356,7 +1356,7 @@
     3.4      also have "\<dots> = (j dvd (- (c*x - ?e)))"
     3.5      by (simp only: dvd_minus_iff)
     3.6    also have "\<dots> = (j dvd (c* (- x)) + ?e)"
     3.7 -    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
     3.8 +    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
     3.9      by (simp add: algebra_simps)
    3.10    also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
    3.11      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
    3.12 @@ -1368,7 +1368,7 @@
    3.13      also have "\<dots> = (j dvd (- (c*x - ?e)))"
    3.14      by (simp only: dvd_minus_iff)
    3.15    also have "\<dots> = (j dvd (c* (- x)) + ?e)"
    3.16 -    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
    3.17 +    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
    3.18      by (simp add: algebra_simps)
    3.19    also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
    3.20      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
     4.1 --- a/src/HOL/Decision_Procs/MIR.thy	Mon Jul 19 16:09:44 2010 +0200
     4.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Mon Jul 19 16:09:44 2010 +0200
     4.3 @@ -1768,7 +1768,7 @@
     4.4    have th: "(real a + b >0) = (real (-a) + (-b)< 0)" by arith
     4.5    show ?thesis using myless[rule_format, where b="real (floor b)"] 
     4.6      by (simp only:th split_int_less_real'[where a="-a" and b="-b"]) 
     4.7 -    (simp add: algebra_simps diff_def[symmetric],arith)
     4.8 +    (simp add: algebra_simps diff_minus[symmetric],arith)
     4.9  qed
    4.10  
    4.11  lemma split_int_le_real: 
    4.12 @@ -1795,7 +1795,7 @@
    4.13  proof- 
    4.14    have th: "(real a + b \<ge>0) = (real (-a) + (-b) \<le> 0)" by arith
    4.15    show ?thesis by (simp only: th split_int_le_real'[where a="-a" and b="-b"])
    4.16 -    (simp add: algebra_simps diff_def[symmetric],arith)
    4.17 +    (simp add: algebra_simps diff_minus[symmetric],arith)
    4.18  qed
    4.19  
    4.20  lemma split_int_eq_real: "(real (a::int) = b) = ( a = floor b \<and> b = real (floor b))" (is "?l = ?r")
    4.21 @@ -1828,13 +1828,13 @@
    4.22    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))" 
    4.23        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    4.24      have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)
    4.25 -    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_def)
    4.26 +    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)
    4.27      finally have ?case using l by simp}
    4.28    moreover
    4.29    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))" 
    4.30        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    4.31      have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)
    4.32 -    also from cn cnz have "\<dots> = (?I (?l (Lt a)))" by (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_def[symmetric] add_ac, arith)
    4.33 +    also from cn cnz have "\<dots> = (?I (?l (Lt a)))" by (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac, arith)
    4.34      finally have ?case using l by simp}
    4.35    ultimately show ?case by blast
    4.36  next
    4.37 @@ -1853,13 +1853,13 @@
    4.38    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))" 
    4.39        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    4.40      have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)
    4.41 -    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_def)
    4.42 +    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)
    4.43      finally have ?case using l by simp}
    4.44    moreover
    4.45    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))" 
    4.46        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    4.47      have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)
    4.48 -    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_def[symmetric] add_ac ,arith)
    4.49 +    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)
    4.50      finally have ?case using l by simp}
    4.51    ultimately show ?case by blast
    4.52  next
    4.53 @@ -1878,13 +1878,13 @@
    4.54    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))" 
    4.55        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    4.56      have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)
    4.57 -    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_def)
    4.58 +    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)
    4.59      finally have ?case using l by simp}
    4.60    moreover
    4.61    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))" 
    4.62        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    4.63      have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)
    4.64 -    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_def[symmetric] add_ac, arith)
    4.65 +    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)
    4.66      finally have ?case using l by simp}
    4.67    ultimately show ?case by blast
    4.68  next
    4.69 @@ -1903,13 +1903,13 @@
    4.70    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))" 
    4.71        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    4.72      have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)
    4.73 -    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_def)
    4.74 +    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)
    4.75      finally have ?case using l by simp}
    4.76    moreover
    4.77    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))" 
    4.78        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    4.79      have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)
    4.80 -    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_def[symmetric] add_ac, arith)
    4.81 +    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)
    4.82      finally have ?case using l by simp}
    4.83    ultimately show ?case by blast
    4.84  next
    4.85 @@ -3337,7 +3337,7 @@
    4.86      hence pid: "c*i + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
    4.87      with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + ?fe = j1" by auto
    4.88      hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - ?N i e + real j1" 
    4.89 -      by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps)
    4.90 +      by (simp only: diff_minus[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps)
    4.91      with nob  have ?case by blast }
    4.92    ultimately show ?case by blast
    4.93  next
    4.94 @@ -3360,11 +3360,11 @@
    4.95      hence pid: "c*i + 1 + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
    4.96      with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + 1+ ?fe = j1" by auto
    4.97      hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) + 1= - ?N i e + real j1"
    4.98 -      by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps real_of_one) 
    4.99 +      by (simp only: diff_minus[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps real_of_one) 
   4.100      hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = (- ?N i e + real j1) - 1"
   4.101 -      by (simp only: algebra_simps diff_def[symmetric])
   4.102 +      by (simp only: algebra_simps diff_minus[symmetric])
   4.103          hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - 1 - ?N i e + real j1"
   4.104 -          by (simp only: add_ac diff_def)
   4.105 +          by (simp only: add_ac diff_minus)
   4.106      with nob  have ?case by blast }
   4.107    ultimately show ?case by blast
   4.108  next
   4.109 @@ -3822,7 +3822,7 @@
   4.110        by(simp only: myl[rule_format, where b="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)"]) 
   4.111      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])
   4.112      hence "\<exists> j\<in> {n.. 0}. ?I (?p (p,n,s) j)"
   4.113 -      using pns by (simp add: fp_def nn diff_def add_ac mult_ac numfloor numadd numneg
   4.114 +      using pns by (simp add: fp_def nn diff_minus add_ac mult_ac numfloor numadd numneg
   4.115          del: diff_less_0_iff_less diff_le_0_iff_le) 
   4.116      then obtain "j" where j_def: "j\<in> {n .. 0} \<and> ?I (?p (p,n,s) j)" by blast
   4.117      hence "\<exists>x \<in> {?p (p,n,s) j |j. n\<le> j \<and> j \<le> 0 }. ?I x" by auto
   4.118 @@ -4036,7 +4036,7 @@
   4.119    from foldr_disj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"]
   4.120    have "Ifm (x#bs) (DVDJ i n s) = (\<exists> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" 
   4.121      by (simp add: iupt_set np DVDJ_def del: iupt.simps)
   4.122 -  also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: algebra_simps diff_def[symmetric])
   4.123 +  also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: algebra_simps diff_minus[symmetric])
   4.124    also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] 
   4.125    have "\<dots> = (real i rdvd real n * x - (-?s))" by simp
   4.126    finally show ?thesis by simp
   4.127 @@ -4051,7 +4051,7 @@
   4.128    from foldr_conj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"]
   4.129    have "Ifm (x#bs) (NDVDJ i n s) = (\<forall> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" 
   4.130      by (simp add: iupt_set np NDVDJ_def del: iupt.simps)
   4.131 -  also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: algebra_simps diff_def[symmetric])
   4.132 +  also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: algebra_simps diff_minus[symmetric])
   4.133    also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] 
   4.134    have "\<dots> = (\<not> (real i rdvd real n * x - (-?s)))" by simp
   4.135    finally show ?thesis by simp
   4.136 @@ -5093,7 +5093,7 @@
   4.137    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")
   4.138  proof-
   4.139    have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real i)#bs) (exsplit p))"
   4.140 -    by (simp add: myless[rule_format, where b="1"] myless[rule_format, where b="0"] add_ac diff_def)
   4.141 +    by (simp add: myless[rule_format, where b="1"] myless[rule_format, where b="0"] add_ac diff_minus)
   4.142    also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real i + x) #bs) p)"
   4.143      by (simp only: exsplit[OF qf] add_ac)
   4.144    also have "\<dots> = (\<exists> x. Ifm (x#bs) p)" 
     5.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Mon Jul 19 16:09:44 2010 +0200
     5.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Mon Jul 19 16:09:44 2010 +0200
     5.3 @@ -36,7 +36,7 @@
     5.4               @{thm "divide_zero"}, 
     5.5               @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"}, 
     5.6               @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
     5.7 -             @{thm "diff_def"}, @{thm "minus_divide_left"}]
     5.8 +             @{thm "diff_minus"}, @{thm "minus_divide_left"}]
     5.9  val comp_ths = ths @ comp_arith @ simp_thms 
    5.10  
    5.11  
     6.1 --- a/src/HOL/Deriv.thy	Mon Jul 19 16:09:44 2010 +0200
     6.2 +++ b/src/HOL/Deriv.thy	Mon Jul 19 16:09:44 2010 +0200
     6.3 @@ -57,7 +57,7 @@
     6.4  
     6.5  lemma DERIV_diff:
     6.6    "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x :> D - E"
     6.7 -by (simp only: diff_def DERIV_add DERIV_minus)
     6.8 +by (simp only: diff_minus DERIV_add DERIV_minus)
     6.9  
    6.10  lemma DERIV_add_minus:
    6.11    "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + - g x) x :> D + - E"
    6.12 @@ -1269,7 +1269,7 @@
    6.13        and "f b - f a = (b - a) * l"
    6.14      by auto
    6.15    from prems have "~(l >= 0)"
    6.16 -    by (metis diff_self le_eqI le_iff_diff_le_0 order_antisym linear
    6.17 +    by (metis diff_self diff_eq_diff_less_eq' le_iff_diff_le_0 order_antisym linear
    6.18                split_mult_pos_le)
    6.19    with prems show False
    6.20      by (metis DERIV_unique order_less_imp_le)
     7.1 --- a/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Jul 19 16:09:44 2010 +0200
     7.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Jul 19 16:09:44 2010 +0200
     7.3 @@ -118,7 +118,7 @@
     7.4  proof -
     7.5    assume x: "x \<in> V"
     7.6    have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
     7.7 -    by (simp add: diff_def)
     7.8 +    by (simp add: diff_minus)
     7.9    also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
    7.10      by (rule add_mult_distrib2)
    7.11    also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
     8.1 --- a/src/HOL/Import/HOL/poly.imp	Mon Jul 19 16:09:44 2010 +0200
     8.2 +++ b/src/HOL/Import/HOL/poly.imp	Mon Jul 19 16:09:44 2010 +0200
     8.3 @@ -13,7 +13,7 @@
     8.4    "poly_add" > "poly_add_primdef"
     8.5    "poly" > "poly_primdef"
     8.6    "normalize" > "normalize_def"
     8.7 -  "diff" > "diff_def"
     8.8 +  "diff" > "diff_minus"
     8.9    "degree" > "degree_def"
    8.10    "##" > "##_def"
    8.11  
     9.1 --- a/src/HOL/Import/HOL/real.imp	Mon Jul 19 16:09:44 2010 +0200
     9.2 +++ b/src/HOL/Import/HOL/real.imp	Mon Jul 19 16:09:44 2010 +0200
     9.3 @@ -25,7 +25,7 @@
     9.4    "sumc" > "HOL4Real.real.sumc"
     9.5    "sum_def" > "HOL4Real.real.sum_def"
     9.6    "sum" > "HOL4Real.real.sum"
     9.7 -  "real_sub" > "Groups.diff_def"
     9.8 +  "real_sub" > "Groups.diff_minus"
     9.9    "real_of_num" > "HOL4Compat.real_of_num"
    9.10    "real_lte" > "HOL4Compat.real_lte"
    9.11    "real_lt" > "Orderings.linorder_not_le"
    10.1 --- a/src/HOL/Int.thy	Mon Jul 19 16:09:44 2010 +0200
    10.2 +++ b/src/HOL/Int.thy	Mon Jul 19 16:09:44 2010 +0200
    10.3 @@ -566,7 +566,7 @@
    10.4    obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
    10.5  apply (cases z rule: eq_Abs_Integ)
    10.6  apply (rule_tac m=x and n=y in diff)
    10.7 -apply (simp add: int_def diff_def minus add)
    10.8 +apply (simp add: int_def minus add diff_minus)
    10.9  done
   10.10  
   10.11  
    11.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jul 19 16:09:44 2010 +0200
    11.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jul 19 16:09:44 2010 +0200
    11.3 @@ -221,12 +221,12 @@
    11.4      from unimodular_reduce_norm[OF th0] o
    11.5      have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
    11.6        apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
    11.7 -      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_def)
    11.8 +      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_minus)
    11.9        apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
   11.10        apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
   11.11        apply (rule_tac x="- ii" in exI, simp add: m power_mult)
   11.12 -      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_def)
   11.13 -      apply (rule_tac x="ii" in exI, simp add: m power_mult diff_def)
   11.14 +      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_minus)
   11.15 +      apply (rule_tac x="ii" in exI, simp add: m power_mult diff_minus)
   11.16        done
   11.17      then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
   11.18      let ?w = "v / complex_of_real (root n (cmod b))"
   11.19 @@ -959,7 +959,7 @@
   11.20  
   11.21  lemma mpoly_sub_conv:
   11.22    "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
   11.23 -  by (simp add: diff_def)
   11.24 +  by (simp add: diff_minus)
   11.25  
   11.26  lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp
   11.27  
    12.1 --- a/src/HOL/Library/Univ_Poly.thy	Mon Jul 19 16:09:44 2010 +0200
    12.2 +++ b/src/HOL/Library/Univ_Poly.thy	Mon Jul 19 16:09:44 2010 +0200
    12.3 @@ -204,7 +204,7 @@
    12.4      from Cons.hyps[rule_format, of x]
    12.5      obtain q r where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast
    12.6      have "h#x#xs = [a*r + h] +++ [-a, 1] *** (r#q)"
    12.7 -      using qr by(cases q, simp_all add: algebra_simps diff_def[symmetric]
    12.8 +      using qr by(cases q, simp_all add: algebra_simps diff_minus[symmetric]
    12.9          minus_mult_left[symmetric] right_minus)
   12.10      hence "\<exists>q r. h#x#xs = [r] +++ [-a, 1] *** q" by blast}
   12.11    thus ?case by blast
    13.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Jul 19 16:09:44 2010 +0200
    13.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Jul 19 16:09:44 2010 +0200
    13.3 @@ -523,7 +523,7 @@
    13.4  lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def)
    13.5  
    13.6  lemma linear_sub: "linear f ==> f(x - y) = f x - f y"
    13.7 -  by (simp add: diff_def linear_add linear_neg)
    13.8 +  by (simp add: diff_minus linear_add linear_neg)
    13.9  
   13.10  lemma linear_setsum:
   13.11    assumes lf: "linear f" and fS: "finite S"
   13.12 @@ -592,10 +592,10 @@
   13.13      by (simp add: eq_add_iff field_simps)
   13.14  
   13.15  lemma bilinear_lsub: "bilinear h ==> h (x - y) z = h x z - h y z"
   13.16 -  by (simp  add: diff_def bilinear_ladd bilinear_lneg)
   13.17 +  by (simp  add: diff_minus bilinear_ladd bilinear_lneg)
   13.18  
   13.19  lemma bilinear_rsub: "bilinear h ==> h z (x - y) = h z x - h z y"
   13.20 -  by (simp  add: diff_def bilinear_radd bilinear_rneg)
   13.21 +  by (simp  add: diff_minus bilinear_radd bilinear_rneg)
   13.22  
   13.23  lemma bilinear_setsum:
   13.24    assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T"
   13.25 @@ -902,7 +902,7 @@
   13.26    by (metis scaleR_minus1_left subspace_mul)
   13.27  
   13.28  lemma subspace_sub: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
   13.29 -  by (metis diff_def subspace_add subspace_neg)
   13.30 +  by (metis diff_minus subspace_add subspace_neg)
   13.31  
   13.32  lemma (in real_vector) subspace_setsum:
   13.33    assumes sA: "subspace A" and fB: "finite B"
   13.34 @@ -3082,7 +3082,7 @@
   13.35    from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
   13.36    have ths: "infnorm x \<le> infnorm (x - y) + infnorm y"
   13.37      "infnorm y \<le> infnorm (x - y) + infnorm x"
   13.38 -    by (simp_all add: field_simps infnorm_neg diff_def[symmetric])
   13.39 +    by (simp_all add: field_simps infnorm_neg diff_minus[symmetric])
   13.40    from th[OF ths]  show ?thesis .
   13.41  qed
   13.42  
    14.1 --- a/src/HOL/NSA/HDeriv.thy	Mon Jul 19 16:09:44 2010 +0200
    14.2 +++ b/src/HOL/NSA/HDeriv.thy	Mon Jul 19 16:09:44 2010 +0200
    14.3 @@ -174,7 +174,7 @@
    14.4  apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
    14.5  apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec)
    14.6  apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add)
    14.7 -apply (auto simp add: diff_def add_ac)
    14.8 +apply (auto simp add: diff_minus add_ac)
    14.9  done
   14.10  
   14.11  text{*Product of functions - Proof is trivial but tedious
   14.12 @@ -234,7 +234,7 @@
   14.13    hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) -- 0 --NS> - D"
   14.14      by (rule NSLIM_minus)
   14.15    have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h"
   14.16 -    by (simp add: minus_divide_left diff_def)
   14.17 +    by (simp add: minus_divide_left diff_minus)
   14.18    with deriv
   14.19    show "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
   14.20  qed
   14.21 @@ -353,7 +353,7 @@
   14.22  (*apply (auto simp add: starfun_inverse_inverse realpow_two
   14.23          simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])*)
   14.24  apply (simp add: inverse_add nonzero_inverse_mult_distrib [symmetric] power_Suc
   14.25 -              nonzero_inverse_minus_eq [symmetric] add_ac mult_ac diff_def
   14.26 +              nonzero_inverse_minus_eq [symmetric] add_ac mult_ac diff_minus
   14.27              del: inverse_mult_distrib inverse_minus_eq
   14.28                   minus_mult_left [symmetric] minus_mult_right [symmetric])
   14.29  apply (subst mult_commute, simp add: nonzero_mult_divide_cancel_right)
    15.1 --- a/src/HOL/NSA/HLim.thy	Mon Jul 19 16:09:44 2010 +0200
    15.2 +++ b/src/HOL/NSA/HLim.thy	Mon Jul 19 16:09:44 2010 +0200
    15.3 @@ -73,7 +73,7 @@
    15.4  
    15.5  lemma NSLIM_diff:
    15.6    "\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)"
    15.7 -by (simp only: diff_def NSLIM_add NSLIM_minus)
    15.8 +by (simp only: diff_minus NSLIM_add NSLIM_minus)
    15.9  
   15.10  lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
   15.11  by (simp only: NSLIM_add NSLIM_minus)
   15.12 @@ -245,7 +245,7 @@
   15.13  apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
   15.14  apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
   15.15  apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
   15.16 - prefer 2 apply (simp add: add_commute diff_def [symmetric])
   15.17 + prefer 2 apply (simp add: add_commute diff_minus [symmetric])
   15.18  apply (rule_tac x = x in star_cases)
   15.19  apply (rule_tac [2] x = x in star_cases)
   15.20  apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
    16.1 --- a/src/HOL/NSA/HTranscendental.thy	Mon Jul 19 16:09:44 2010 +0200
    16.2 +++ b/src/HOL/NSA/HTranscendental.thy	Mon Jul 19 16:09:44 2010 +0200
    16.3 @@ -258,7 +258,7 @@
    16.4              simp add: mult_assoc)
    16.5  apply (rule approx_add_right_cancel [where d="-1"])
    16.6  apply (rule approx_sym [THEN [2] approx_trans2])
    16.7 -apply (auto simp add: diff_def mem_infmal_iff)
    16.8 +apply (auto simp add: diff_minus mem_infmal_iff)
    16.9  done
   16.10  
   16.11  lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
   16.12 @@ -450,7 +450,7 @@
   16.13  apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   16.14              simp add: mult_assoc)
   16.15  apply (rule approx_add_right_cancel [where d = "-1"])
   16.16 -apply (simp add: diff_def)
   16.17 +apply (simp add: diff_minus)
   16.18  done
   16.19  
   16.20  lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
    17.1 --- a/src/HOL/NSA/NSA.thy	Mon Jul 19 16:09:44 2010 +0200
    17.2 +++ b/src/HOL/NSA/NSA.thy	Mon Jul 19 16:09:44 2010 +0200
    17.3 @@ -368,7 +368,7 @@
    17.4  
    17.5  lemma Infinitesimal_diff:
    17.6       "[| x \<in> Infinitesimal;  y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
    17.7 -by (simp add: diff_def Infinitesimal_add)
    17.8 +by (simp add: diff_minus Infinitesimal_add)
    17.9  
   17.10  lemma Infinitesimal_mult:
   17.11    fixes x y :: "'a::real_normed_algebra star"
   17.12 @@ -637,7 +637,7 @@
   17.13  lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z"
   17.14  apply (simp add: approx_def)
   17.15  apply (drule (1) Infinitesimal_add)
   17.16 -apply (simp add: diff_def)
   17.17 +apply (simp add: diff_minus)
   17.18  done
   17.19  
   17.20  lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s"
   17.21 @@ -714,7 +714,7 @@
   17.22  lemma approx_minus: "a @= b ==> -a @= -b"
   17.23  apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
   17.24  apply (drule approx_minus_iff [THEN iffD1])
   17.25 -apply (simp add: add_commute diff_def)
   17.26 +apply (simp add: add_commute diff_minus)
   17.27  done
   17.28  
   17.29  lemma approx_minus2: "-a @= -b ==> a @= b"
    18.1 --- a/src/HOL/NSA/NSCA.thy	Mon Jul 19 16:09:44 2010 +0200
    18.2 +++ b/src/HOL/NSA/NSCA.thy	Mon Jul 19 16:09:44 2010 +0200
    18.3 @@ -178,7 +178,7 @@
    18.4       "u @= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
    18.5  apply (drule approx_approx_zero_iff [THEN iffD1])
    18.6  apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
    18.7 -apply (auto simp add: mem_infmal_iff [symmetric] diff_def)
    18.8 +apply (auto simp add: mem_infmal_iff [symmetric] diff_minus)
    18.9  apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1])
   18.10  apply (auto simp add: diff_minus [symmetric])
   18.11  done
    19.1 --- a/src/HOL/Probability/Borel.thy	Mon Jul 19 16:09:44 2010 +0200
    19.2 +++ b/src/HOL/Probability/Borel.thy	Mon Jul 19 16:09:44 2010 +0200
    19.3 @@ -357,7 +357,7 @@
    19.4                      borel_measurable_uminus_borel_measurable f g)
    19.5    finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
    19.6    show ?thesis
    19.7 -    apply (simp add: times_eq_sum_squares diff_def) 
    19.8 +    apply (simp add: times_eq_sum_squares diff_minus) 
    19.9      using 1 2 apply (simp add: borel_measurable_add_borel_measurable) 
   19.10      done
   19.11  qed
   19.12 @@ -366,7 +366,7 @@
   19.13    assumes f: "f \<in> borel_measurable M"
   19.14    assumes g: "g \<in> borel_measurable M"
   19.15    shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   19.16 -unfolding diff_def
   19.17 +unfolding diff_minus
   19.18    by (fast intro: borel_measurable_add_borel_measurable 
   19.19                    borel_measurable_uminus_borel_measurable f g)
   19.20  
   19.21 @@ -626,11 +626,11 @@
   19.22  proof -
   19.23    from assms have "y - z > 0" by simp
   19.24    hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
   19.25 -    unfolding incseq_def LIMSEQ_def dist_real_def diff_def
   19.26 +    unfolding incseq_def LIMSEQ_def dist_real_def diff_minus
   19.27      by simp
   19.28    have "\<forall>m. x m \<le> y" using incseq_le assms by auto
   19.29    hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
   19.30 -    by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le diff_def)
   19.31 +    by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le diff_minus)
   19.32    from A B show ?thesis by auto
   19.33  qed
   19.34  
    20.1 --- a/src/HOL/RComplete.thy	Mon Jul 19 16:09:44 2010 +0200
    20.2 +++ b/src/HOL/RComplete.thy	Mon Jul 19 16:09:44 2010 +0200
    20.3 @@ -153,7 +153,7 @@
    20.4    have "x = y-(y-x)" by simp
    20.5    also from suc q have "\<dots> < real (Suc p)/real q - inverse (real q)" by arith
    20.6    also have "\<dots> = real p / real q"
    20.7 -    by (simp only: inverse_eq_divide diff_def real_of_nat_Suc 
    20.8 +    by (simp only: inverse_eq_divide diff_minus real_of_nat_Suc 
    20.9      minus_divide_left add_divide_distrib[THEN sym]) simp
   20.10    finally have "x<r" by (unfold r_def)
   20.11    have "p<Suc p" .. also note main[THEN sym]
    21.1 --- a/src/HOL/RealVector.thy	Mon Jul 19 16:09:44 2010 +0200
    21.2 +++ b/src/HOL/RealVector.thy	Mon Jul 19 16:09:44 2010 +0200
    21.3 @@ -30,7 +30,7 @@
    21.4  qed
    21.5  
    21.6  lemma diff: "f (x - y) = f x - f y"
    21.7 -by (simp add: diff_def add minus)
    21.8 +by (simp add: add minus diff_minus)
    21.9  
   21.10  lemma setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))"
   21.11  apply (cases "finite A")
    22.1 --- a/src/HOL/SEQ.thy	Mon Jul 19 16:09:44 2010 +0200
    22.2 +++ b/src/HOL/SEQ.thy	Mon Jul 19 16:09:44 2010 +0200
    22.3 @@ -506,8 +506,7 @@
    22.4        from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
    22.5          by blast
    22.6        thus "lim f \<le> x"
    22.7 -        by (metis add_cancel_end add_minus_cancel diff_def linorder_linear 
    22.8 -                  linorder_not_le minus_diff_eq abs_diff_less_iff fn_le) 
    22.9 +        by (metis 1 LIMSEQ_le_const2 fn_le)
   22.10      qed
   22.11  qed
   22.12  
   22.13 @@ -971,7 +970,7 @@
   22.14  apply (rule_tac x = K in exI, simp)
   22.15  apply (rule exI [where x = 0], auto)
   22.16  apply (erule order_less_le_trans, simp)
   22.17 -apply (drule_tac x=n in spec, fold diff_def)
   22.18 +apply (drule_tac x=n in spec, fold diff_minus)
   22.19  apply (drule order_trans [OF norm_triangle_ineq2])
   22.20  apply simp
   22.21  done
    23.1 --- a/src/HOL/SupInf.thy	Mon Jul 19 16:09:44 2010 +0200
    23.2 +++ b/src/HOL/SupInf.thy	Mon Jul 19 16:09:44 2010 +0200
    23.3 @@ -417,7 +417,7 @@
    23.4    also have "... \<le> e" 
    23.5      apply (rule Sup_asclose) 
    23.6      apply (auto simp add: S)
    23.7 -    apply (metis abs_minus_add_cancel b add_commute diff_def)
    23.8 +    apply (metis abs_minus_add_cancel b add_commute diff_minus)
    23.9      done
   23.10    finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
   23.11    thus ?thesis
    24.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Mon Jul 19 16:09:44 2010 +0200
    24.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Jul 19 16:09:44 2010 +0200
    24.3 @@ -734,7 +734,7 @@
    24.4             @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
    24.5             @{thm "times_divide_times_eq"},
    24.6             @{thm "divide_divide_eq_right"},
    24.7 -           @{thm "diff_def"}, @{thm "minus_divide_left"},
    24.8 +           @{thm "diff_minus"}, @{thm "minus_divide_left"},
    24.9             @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
   24.10             @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, 
   24.11             Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute}))))   
    25.1 --- a/src/HOL/Transcendental.thy	Mon Jul 19 16:09:44 2010 +0200
    25.2 +++ b/src/HOL/Transcendental.thy	Mon Jul 19 16:09:44 2010 +0200
    25.3 @@ -2952,7 +2952,7 @@
    25.4        }
    25.5        hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
    25.6        moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
    25.7 -        unfolding diff_def divide_inverse
    25.8 +        unfolding diff_minus divide_inverse
    25.9          by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum)
   25.10        ultimately have "0 \<le> ?a 1 n - ?diff 1 n" by (rule LIM_less_bound)
   25.11        hence "?diff 1 n \<le> ?a 1 n" by auto
   25.12 @@ -2968,7 +2968,7 @@
   25.13          have "norm (?diff 1 n - 0) < r" by auto }
   25.14        thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
   25.15      qed
   25.16 -    from this[unfolded LIMSEQ_rabs_zero diff_def add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
   25.17 +    from this[unfolded LIMSEQ_rabs_zero diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
   25.18      have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
   25.19      hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
   25.20      
    26.1 --- a/src/HOL/Word/Misc_Numeric.thy	Mon Jul 19 16:09:44 2010 +0200
    26.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Mon Jul 19 16:09:44 2010 +0200
    26.3 @@ -292,7 +292,7 @@
    26.4  
    26.5  (* two alternative proofs of this *)
    26.6  lemma RI_eq_diff': "(a, b) : Rep_Integ (int a - int b)"
    26.7 -  apply (unfold diff_def)
    26.8 +  apply (unfold diff_minus)
    26.9    apply (rule mem_same)
   26.10     apply (rule RI_minus RI_add RI_int)+
   26.11    apply simp
    27.1 --- a/src/HOL/Word/Word.thy	Mon Jul 19 16:09:44 2010 +0200
    27.2 +++ b/src/HOL/Word/Word.thy	Mon Jul 19 16:09:44 2010 +0200
    27.3 @@ -1130,14 +1130,14 @@
    27.4  lemmas wi_hom_syms = wi_homs [symmetric]
    27.5  
    27.6  lemma word_sub_def: "a - b == a + - (b :: 'a :: len0 word)"
    27.7 -  unfolding word_sub_wi diff_def
    27.8 +  unfolding word_sub_wi diff_minus
    27.9    by (simp only : word_uint.Rep_inverse wi_hom_syms)
   27.10      
   27.11  lemmas word_diff_minus = word_sub_def [THEN meta_eq_to_obj_eq, standard]
   27.12  
   27.13  lemma word_of_int_sub_hom:
   27.14    "(word_of_int a) - word_of_int b = word_of_int (a - b)"
   27.15 -  unfolding word_sub_def diff_def by (simp only : wi_homs)
   27.16 +  unfolding word_sub_def diff_minus by (simp only : wi_homs)
   27.17  
   27.18  lemmas new_word_of_int_homs = 
   27.19    word_of_int_sub_hom wi_homs word_0_wi word_1_wi