avoid using real-specific versions of generic lemmas
authorhuffman
Sun May 09 22:51:11 2010 -0700 (2010-05-09)
changeset 36778739a9379e29b
parent 36777 be5461582d0f
child 36779 0713931bd769
child 36797 cb074cec7a30
avoid using real-specific versions of generic lemmas
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Hahn_Banach/Function_Norm.thy
src/HOL/Hahn_Banach/Vector_Space.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Float.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Borel.thy
src/HOL/Probability/Lebesgue.thy
src/HOL/ex/Sqrt_Script.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sun May 09 17:47:43 2010 -0700
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sun May 09 22:51:11 2010 -0700
     1.3 @@ -18,7 +18,7 @@
     1.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)"
     1.5  proof -
     1.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
     1.7 -  show ?thesis unfolding setsum_right_distrib shift_pow real_diff_def setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
     1.8 +  show ?thesis unfolding setsum_right_distrib shift_pow diff_def setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
     1.9      setsum_reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\<lambda> n. (-1)^n  *a n * x^n"] by auto
    1.10  qed
    1.11  
    1.12 @@ -109,8 +109,8 @@
    1.13    proof (rule setsum_cong, simp)
    1.14      fix j assume "j \<in> {0 ..< n}"
    1.15      show "1 / real (f (j' + j)) * real x ^ j = -1 ^ j * (1 / real (f (j' + j))) * real (- x) ^ j"
    1.16 -      unfolding move_minus power_mult_distrib real_mult_assoc[symmetric]
    1.17 -      unfolding real_mult_commute unfolding real_mult_assoc[of "-1 ^ j", symmetric] power_mult_distrib[symmetric]
    1.18 +      unfolding move_minus power_mult_distrib mult_assoc[symmetric]
    1.19 +      unfolding mult_commute unfolding mult_assoc[of "-1 ^ j", symmetric] power_mult_distrib[symmetric]
    1.20        by auto
    1.21    qed
    1.22  
    1.23 @@ -435,8 +435,8 @@
    1.24  
    1.25    { have "real (x * lb_arctan_horner prec n 1 (x*x)) \<le> ?S n"
    1.26        using bounds(1) `0 \<le> real x`
    1.27 -      unfolding real_of_float_mult power_add power_one_right real_mult_assoc[symmetric] setsum_left_distrib[symmetric]
    1.28 -      unfolding real_mult_commute mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"]
    1.29 +      unfolding real_of_float_mult power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric]
    1.30 +      unfolding mult_commute[where 'a=real] mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"]
    1.31        by (auto intro!: mult_left_mono)
    1.32      also have "\<dots> \<le> arctan (real x)" using arctan_bounds ..
    1.33      finally have "real (x * lb_arctan_horner prec n 1 (x*x)) \<le> arctan (real x)" . }
    1.34 @@ -444,8 +444,8 @@
    1.35    { have "arctan (real x) \<le> ?S (Suc n)" using arctan_bounds ..
    1.36      also have "\<dots> \<le> real (x * ub_arctan_horner prec (Suc n) 1 (x*x))"
    1.37        using bounds(2)[of "Suc n"] `0 \<le> real x`
    1.38 -      unfolding real_of_float_mult power_add power_one_right real_mult_assoc[symmetric] setsum_left_distrib[symmetric]
    1.39 -      unfolding real_mult_commute mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"]
    1.40 +      unfolding real_of_float_mult power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric]
    1.41 +      unfolding mult_commute[where 'a=real] mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"]
    1.42        by (auto intro!: mult_left_mono)
    1.43      finally have "arctan (real x) \<le> real (x * ub_arctan_horner prec (Suc n) 1 (x*x))" . }
    1.44    ultimately show ?thesis by auto
    1.45 @@ -616,7 +616,7 @@
    1.46          using arctan_0_1_bounds[OF `0 \<le> real ?DIV` `real ?DIV \<le> 1`] by auto
    1.47        also have "\<dots> \<le> 2 * arctan (real x / ?R)"
    1.48          using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
    1.49 -      also have "2 * arctan (real x / ?R) = arctan (real x)" using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 power_0 real_mult_1 .
    1.50 +      also have "2 * arctan (real x / ?R) = arctan (real x)" using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left .
    1.51        finally show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF True] .
    1.52      next
    1.53        case False
    1.54 @@ -644,7 +644,7 @@
    1.55            using `0 \<le> arctan (real x)` arctan_inverse[OF `1 / real x \<noteq> 0`]
    1.56            unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto
    1.57          moreover
    1.58 -        have "real (lb_pi prec * Float 1 -1) \<le> pi / 2" unfolding real_of_float_mult Float_num times_divide_eq_right real_mult_1 using pi_boundaries by auto
    1.59 +        have "real (lb_pi prec * Float 1 -1) \<le> pi / 2" unfolding real_of_float_mult Float_num times_divide_eq_right mult_1_left using pi_boundaries by auto
    1.60          ultimately
    1.61          show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF `\<not> x \<le> Float 1 1`] if_not_P[OF False]
    1.62            by auto
    1.63 @@ -696,7 +696,7 @@
    1.64        show ?thesis
    1.65        proof (cases "?DIV > 1")
    1.66          case True
    1.67 -        have "pi / 2 \<le> real (ub_pi prec * Float 1 -1)" unfolding real_of_float_mult Float_num times_divide_eq_right real_mult_1 using pi_boundaries by auto
    1.68 +        have "pi / 2 \<le> real (ub_pi prec * Float 1 -1)" unfolding real_of_float_mult Float_num times_divide_eq_right mult_1_left using pi_boundaries by auto
    1.69          from order_less_le_trans[OF arctan_ubound this, THEN less_imp_le]
    1.70          show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF `x \<le> Float 1 1`] if_P[OF True] .
    1.71        next
    1.72 @@ -706,7 +706,7 @@
    1.73          have "0 \<le> real x / ?R" using `0 \<le> real x` `0 < ?R` unfolding real_0_le_divide_iff by auto
    1.74          hence "0 \<le> real ?DIV" using monotone by (rule order_trans)
    1.75  
    1.76 -        have "arctan (real x) = 2 * arctan (real x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 real_mult_1 .
    1.77 +        have "arctan (real x) = 2 * arctan (real x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left .
    1.78          also have "\<dots> \<le> 2 * arctan (real ?DIV)"
    1.79            using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
    1.80          also have "\<dots> \<le> real (Float 1 1 * ?ub_horner ?DIV)" unfolding real_of_float_mult[of "Float 1 1"] Float_num
    1.81 @@ -912,8 +912,8 @@
    1.82    from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
    1.83      OF `0 \<le> real (x * x)` f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
    1.84    show "?lb" and "?ub" using `0 \<le> real x` unfolding real_of_float_mult
    1.85 -    unfolding power_add power_one_right real_mult_assoc[symmetric] setsum_left_distrib[symmetric]
    1.86 -    unfolding real_mult_commute
    1.87 +    unfolding power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric]
    1.88 +    unfolding mult_commute[where 'a=real]
    1.89      by (auto intro!: mult_left_mono simp add: power_mult power2_eq_square[of "real x"])
    1.90  qed
    1.91  
    1.92 @@ -1179,7 +1179,7 @@
    1.93  proof (induct n arbitrary: x)
    1.94    case (Suc n)
    1.95    have split_pi_off: "x + real (Suc n) * 2 * pi = (x + real n * 2 * pi) + 2 * pi"
    1.96 -    unfolding Suc_eq_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
    1.97 +    unfolding Suc_eq_plus1 real_of_nat_add real_of_one left_distrib by auto
    1.98    show ?case unfolding split_pi_off using Suc by auto
    1.99  qed auto
   1.100  
   1.101 @@ -1213,7 +1213,7 @@
   1.102            round_down[of prec "lb_pi prec"] by auto
   1.103    hence "real ?lx \<le> x - real k * 2 * pi \<and> x - real k * 2 * pi \<le> real ?ux"
   1.104      using x by (cases "k = 0") (auto intro!: add_mono
   1.105 -                simp add: real_diff_def k[symmetric] less_float_def)
   1.106 +                simp add: diff_def k[symmetric] less_float_def)
   1.107    note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]
   1.108    hence lx_less_ux: "real ?lx \<le> real ?ux" by (rule order_trans)
   1.109  
   1.110 @@ -1227,7 +1227,7 @@
   1.111      also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
   1.112        using cos_monotone_minus_pi_0'[OF pi_lx lx x_le_0]
   1.113        by (simp only: real_of_float_minus real_of_int_minus
   1.114 -        cos_minus real_diff_def mult_minus_left)
   1.115 +        cos_minus diff_def mult_minus_left)
   1.116      finally have "real (lb_cos prec (- ?lx)) \<le> cos x"
   1.117        unfolding cos_periodic_int . }
   1.118    note negative_lx = this
   1.119 @@ -1240,7 +1240,7 @@
   1.120      have "cos (x + real (-k) * 2 * pi) \<le> cos (real ?lx)"
   1.121        using cos_monotone_0_pi'[OF lx_0 lx pi_x]
   1.122        by (simp only: real_of_float_minus real_of_int_minus
   1.123 -        cos_minus real_diff_def mult_minus_left)
   1.124 +        cos_minus diff_def mult_minus_left)
   1.125      also have "\<dots> \<le> real (ub_cos prec ?lx)"
   1.126        using lb_cos[OF lx_0 pi_lx] by simp
   1.127      finally have "cos x \<le> real (ub_cos prec ?lx)"
   1.128 @@ -1255,7 +1255,7 @@
   1.129      have "cos (x + real (-k) * 2 * pi) \<le> cos (real (- ?ux))"
   1.130        using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
   1.131        by (simp only: real_of_float_minus real_of_int_minus
   1.132 -          cos_minus real_diff_def mult_minus_left)
   1.133 +          cos_minus diff_def mult_minus_left)
   1.134      also have "\<dots> \<le> real (ub_cos prec (- ?ux))"
   1.135        using lb_cos_minus[OF pi_ux ux_0, of prec] by simp
   1.136      finally have "cos x \<le> real (ub_cos prec (- ?ux))"
   1.137 @@ -1272,7 +1272,7 @@
   1.138      also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
   1.139        using cos_monotone_0_pi'[OF x_ge_0 ux pi_ux]
   1.140        by (simp only: real_of_float_minus real_of_int_minus
   1.141 -        cos_minus real_diff_def mult_minus_left)
   1.142 +        cos_minus diff_def mult_minus_left)
   1.143      finally have "real (lb_cos prec ?ux) \<le> cos x"
   1.144        unfolding cos_periodic_int . }
   1.145    note positive_ux = this
   1.146 @@ -1347,7 +1347,7 @@
   1.147        also have "\<dots> \<le> cos (real (?ux - 2 * ?lpi))"
   1.148          using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
   1.149          by (simp only: real_of_float_minus real_of_int_minus real_of_one
   1.150 -            number_of_Min real_diff_def mult_minus_left real_mult_1)
   1.151 +            number_of_Min diff_def mult_minus_left mult_1_left)
   1.152        also have "\<dots> = cos (real (- (?ux - 2 * ?lpi)))"
   1.153          unfolding real_of_float_minus cos_minus ..
   1.154        also have "\<dots> \<le> real (ub_cos prec (- (?ux - 2 * ?lpi)))"
   1.155 @@ -1391,7 +1391,7 @@
   1.156        also have "\<dots> \<le> cos (real (?lx + 2 * ?lpi))"
   1.157          using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
   1.158          by (simp only: real_of_float_minus real_of_int_minus real_of_one
   1.159 -          number_of_Min real_diff_def mult_minus_left real_mult_1)
   1.160 +          number_of_Min diff_def mult_minus_left mult_1_left)
   1.161        also have "\<dots> \<le> real (ub_cos prec (?lx + 2 * ?lpi))"
   1.162          using lb_cos[OF lx_0 pi_lx] by simp
   1.163        finally show ?thesis unfolding u by (simp add: real_of_float_max)
   1.164 @@ -1531,7 +1531,7 @@
   1.165      hence "real (floor_fl x) < 0" unfolding Float_floor real_of_float_simp using zero_less_pow2[of xe] by auto
   1.166      hence "m < 0"
   1.167        unfolding less_float_def real_of_float_0 Float_floor real_of_float_simp
   1.168 -      unfolding pos_prod_lt[OF zero_less_pow2[of e], unfolded real_mult_commute] by auto
   1.169 +      unfolding pos_prod_lt[OF zero_less_pow2[of e], unfolded mult_commute] by auto
   1.170      hence "1 \<le> - m" by auto
   1.171      hence "0 < nat (- m)" by auto
   1.172      moreover
   1.173 @@ -1682,7 +1682,7 @@
   1.174    { fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric]
   1.175      proof (rule mult_mono)
   1.176        show "0 \<le> x ^ Suc (Suc n)" by (auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
   1.177 -      have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 real_mult_assoc[symmetric]
   1.178 +      have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 mult_assoc[symmetric]
   1.179          by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
   1.180        thus "x ^ Suc (Suc n) \<le> x ^ Suc n" by auto
   1.181      qed auto }
   1.182 @@ -1700,7 +1700,7 @@
   1.183  
   1.184    let "?s n" = "-1^n * (1 / real (1 + n)) * (real x)^(Suc n)"
   1.185  
   1.186 -  have "?lb \<le> setsum ?s {0 ..< 2 * ev}" unfolding power_Suc2 real_mult_assoc[symmetric] real_of_float_mult setsum_left_distrib[symmetric] unfolding real_mult_commute[of "real x"] ev
   1.187 +  have "?lb \<le> setsum ?s {0 ..< 2 * ev}" unfolding power_Suc2 mult_assoc[symmetric] real_of_float_mult setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] ev
   1.188      using horner_bounds(1)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*ev",
   1.189        OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
   1.190      by (rule mult_right_mono)
   1.191 @@ -1708,7 +1708,7 @@
   1.192    finally show "?lb \<le> ?ln" .
   1.193  
   1.194    have "?ln \<le> setsum ?s {0 ..< 2 * od + 1}" using ln_bounds(2)[OF `0 \<le> real x` `real x < 1`] by auto
   1.195 -  also have "\<dots> \<le> ?ub" unfolding power_Suc2 real_mult_assoc[symmetric] real_of_float_mult setsum_left_distrib[symmetric] unfolding real_mult_commute[of "real x"] od
   1.196 +  also have "\<dots> \<le> ?ub" unfolding power_Suc2 mult_assoc[symmetric] real_of_float_mult setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] od
   1.197      using horner_bounds(2)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*od+1",
   1.198        OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
   1.199      by (rule mult_right_mono)
   1.200 @@ -2088,28 +2088,28 @@
   1.201  "interpret_floatarith (Var n) vs     = vs ! n"
   1.202  
   1.203  lemma interpret_floatarith_divide: "interpret_floatarith (Mult a (Inverse b)) vs = (interpret_floatarith a vs) / (interpret_floatarith b vs)"
   1.204 -  unfolding real_divide_def interpret_floatarith.simps ..
   1.205 +  unfolding divide_inverse interpret_floatarith.simps ..
   1.206  
   1.207  lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
   1.208 -  unfolding real_diff_def interpret_floatarith.simps ..
   1.209 +  unfolding diff_def interpret_floatarith.simps ..
   1.210  
   1.211  lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
   1.212    sin (interpret_floatarith a vs)"
   1.213    unfolding sin_cos_eq interpret_floatarith.simps
   1.214 -            interpret_floatarith_divide interpret_floatarith_diff real_diff_def
   1.215 +            interpret_floatarith_divide interpret_floatarith_diff diff_def
   1.216    by auto
   1.217  
   1.218  lemma interpret_floatarith_tan:
   1.219    "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (Inverse (Cos a))) vs =
   1.220     tan (interpret_floatarith a vs)"
   1.221 -  unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def real_divide_def
   1.222 +  unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse
   1.223    by auto
   1.224  
   1.225  lemma interpret_floatarith_powr: "interpret_floatarith (Exp (Mult b (Ln a))) vs = (interpret_floatarith a vs) powr (interpret_floatarith b vs)"
   1.226    unfolding powr_def interpret_floatarith.simps ..
   1.227  
   1.228  lemma interpret_floatarith_log: "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = log (interpret_floatarith b vs) (interpret_floatarith x vs)"
   1.229 -  unfolding log_def interpret_floatarith.simps real_divide_def ..
   1.230 +  unfolding log_def interpret_floatarith.simps divide_inverse ..
   1.231  
   1.232  lemma interpret_floatarith_num:
   1.233    shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
     2.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sun May 09 17:47:43 2010 -0700
     2.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sun May 09 22:51:11 2010 -0700
     2.3 @@ -2177,7 +2177,7 @@
     2.4      assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     2.5      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     2.6      with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
     2.7 -      by (simp only:  real_mult_less_mono2[OF rcpos th1])
     2.8 +      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     2.9      hence "real c * real x + Inum (y # bs) e \<noteq> 0"using rcpos  by simp
    2.10      thus "real c * real x + Inum (real x # bs) e \<noteq> 0" 
    2.11        using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp
    2.12 @@ -2194,7 +2194,7 @@
    2.13      assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
    2.14      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
    2.15      with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
    2.16 -      by (simp only:  real_mult_less_mono2[OF rcpos th1])
    2.17 +      by (simp only: mult_strict_left_mono [OF th1 rcpos])
    2.18      hence "real c * real x + Inum (y # bs) e \<noteq> 0"using rcpos  by simp
    2.19      thus "real c * real x + Inum (real x # bs) e \<noteq> 0" 
    2.20        using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp
    2.21 @@ -2211,7 +2211,7 @@
    2.22      assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
    2.23      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
    2.24      with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
    2.25 -      by (simp only:  real_mult_less_mono2[OF rcpos th1])
    2.26 +      by (simp only: mult_strict_left_mono [OF th1 rcpos])
    2.27      thus "real c * real x + Inum (real x # bs) e < 0" 
    2.28        using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
    2.29    qed
    2.30 @@ -2227,7 +2227,7 @@
    2.31      assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
    2.32      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
    2.33      with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
    2.34 -      by (simp only:  real_mult_less_mono2[OF rcpos th1])
    2.35 +      by (simp only: mult_strict_left_mono [OF th1 rcpos])
    2.36      thus "real c * real x + Inum (real x # bs) e \<le> 0" 
    2.37        using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
    2.38    qed
    2.39 @@ -2243,7 +2243,7 @@
    2.40      assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
    2.41      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
    2.42      with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
    2.43 -      by (simp only:  real_mult_less_mono2[OF rcpos th1])
    2.44 +      by (simp only: mult_strict_left_mono [OF th1 rcpos])
    2.45      thus "\<not> (real c * real x + Inum (real x # bs) e>0)" 
    2.46        using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
    2.47    qed
    2.48 @@ -2259,7 +2259,7 @@
    2.49      assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
    2.50      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
    2.51      with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
    2.52 -      by (simp only:  real_mult_less_mono2[OF rcpos th1])
    2.53 +      by (simp only: mult_strict_left_mono [OF th1 rcpos])
    2.54      thus "\<not> real c * real x + Inum (real x # bs) e \<ge> 0" 
    2.55        using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
    2.56    qed
     3.1 --- a/src/HOL/Hahn_Banach/Function_Norm.thy	Sun May 09 17:47:43 2010 -0700
     3.2 +++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Sun May 09 22:51:11 2010 -0700
     3.3 @@ -124,7 +124,7 @@
     3.4            assume "y \<noteq> 0"
     3.5            with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
     3.6                and x: "x \<in> V" and neq: "x \<noteq> 0"
     3.7 -            by (auto simp add: B_def real_divide_def)
     3.8 +            by (auto simp add: B_def divide_inverse)
     3.9            from x neq have gt: "0 < \<parallel>x\<parallel>" ..
    3.10  
    3.11            txt {* The thesis follows by a short calculation using the
    3.12 @@ -139,7 +139,7 @@
    3.13              then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
    3.14            qed
    3.15            also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
    3.16 -            by (rule real_mult_assoc)
    3.17 +            by (rule Groups.mult_assoc)
    3.18            also
    3.19            from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
    3.20            then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp 
    3.21 @@ -224,7 +224,7 @@
    3.22      proof (rule mult_right_mono)
    3.23        from x show "0 \<le> \<parallel>x\<parallel>" ..
    3.24        from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
    3.25 -        by (auto simp add: B_def real_divide_def)
    3.26 +        by (auto simp add: B_def divide_inverse)
    3.27        with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
    3.28          by (rule fn_norm_ub)
    3.29      qed
    3.30 @@ -257,7 +257,7 @@
    3.31        assume "b \<noteq> 0"
    3.32        with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
    3.33          and x_neq: "x \<noteq> 0" and x: "x \<in> V"
    3.34 -        by (auto simp add: B_def real_divide_def)
    3.35 +        by (auto simp add: B_def divide_inverse)
    3.36        note b_rep
    3.37        also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
    3.38        proof (rule mult_right_mono)
     4.1 --- a/src/HOL/Hahn_Banach/Vector_Space.thy	Sun May 09 17:47:43 2010 -0700
     4.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Sun May 09 22:51:11 2010 -0700
     4.3 @@ -118,7 +118,7 @@
     4.4  proof -
     4.5    assume x: "x \<in> V"
     4.6    have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
     4.7 -    by (simp add: real_diff_def)
     4.8 +    by (simp add: diff_def)
     4.9    also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
    4.10      by (rule add_mult_distrib2)
    4.11    also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
    4.12 @@ -255,7 +255,7 @@
    4.13  
    4.14  lemma (in vectorspace) mult_left_commute:
    4.15      "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x"
    4.16 -  by (simp add: real_mult_commute mult_assoc2)
    4.17 +  by (simp add: mult_commute mult_assoc2)
    4.18  
    4.19  lemma (in vectorspace) mult_zero_uniq:
    4.20    "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> a \<cdot> x = 0 \<Longrightarrow> a = 0"
     5.1 --- a/src/HOL/Library/Convex.thy	Sun May 09 17:47:43 2010 -0700
     5.2 +++ b/src/HOL/Library/Convex.thy	Sun May 09 22:51:11 2010 -0700
     5.3 @@ -362,8 +362,7 @@
     5.4    { assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
     5.5      hence "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
     5.6      hence "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms
     5.7 -      using add_nonneg_pos[of "\<mu> *\<^sub>R x" "(1 - \<mu>) *\<^sub>R y"]
     5.8 -        real_mult_order by auto fastsimp }
     5.9 +      by (auto simp add: add_pos_pos mult_pos_pos) }
    5.10    ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastsimp
    5.11  qed
    5.12  
    5.13 @@ -426,7 +425,7 @@
    5.14      also have "\<dots> = f ((1 - a i) *\<^sub>R (\<Sum> j \<in> s. (a j * inverse (1 - a i)) *\<^sub>R y j) + a i *\<^sub>R y i)"
    5.15        using scaleR_right.setsum[of "inverse (1 - a i)" "\<lambda> j. a j *\<^sub>R y j" s, symmetric] by (auto simp:algebra_simps)
    5.16      also have "\<dots> = f ((1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) + a i *\<^sub>R y i)"
    5.17 -      by (auto simp:real_divide_def)
    5.18 +      by (auto simp: divide_inverse)
    5.19      also have "\<dots> \<le> (1 - a i) *\<^sub>R f ((\<Sum> j \<in> s. ?a j *\<^sub>R y j)) + a i * f (y i)"
    5.20        using conv[of "y i" "(\<Sum> j \<in> s. ?a j *\<^sub>R y j)" "a i", OF yai(1) asum yai(2) ai1]
    5.21        by (auto simp add:add_commute)
    5.22 @@ -555,7 +554,7 @@
    5.23      from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
    5.24      from mult_right_mono_neg[OF this le(2)]
    5.25      have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
    5.26 -      unfolding diff_def using real_add_mult_distrib by auto
    5.27 +      by (simp add: algebra_simps)
    5.28      hence "f' y * (x - y) - (f x - f y) \<le> 0" using le by auto
    5.29      hence res: "f' y * (x - y) \<le> f x - f y" by auto
    5.30      have "(f y - f x) / (y - x) - f' x = f' z1 - f' x"
    5.31 @@ -570,7 +569,7 @@
    5.32      from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
    5.33      from mult_right_mono[OF this ge(2)]
    5.34      have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"
    5.35 -      unfolding diff_def using real_add_mult_distrib by auto
    5.36 +      by (simp add: algebra_simps)
    5.37      hence "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto
    5.38      hence "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
    5.39        using res by auto } note less_imp = this
    5.40 @@ -606,9 +605,9 @@
    5.41    have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
    5.42      by auto
    5.43    hence f''0: "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
    5.44 -    unfolding inverse_eq_divide by (auto simp add:real_mult_assoc)
    5.45 +    unfolding inverse_eq_divide by (auto simp add: mult_assoc)
    5.46    have f''_ge0: "\<And> z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
    5.47 -    using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] real_mult_order)
    5.48 +    using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] mult_pos_pos)
    5.49    from f''_ge0_imp_convex[OF pos_is_convex,
    5.50      unfolded greaterThan_iff, OF f' f''0 f''_ge0]
    5.51    show ?thesis by auto
     6.1 --- a/src/HOL/Library/Float.thy	Sun May 09 17:47:43 2010 -0700
     6.2 +++ b/src/HOL/Library/Float.thy	Sun May 09 22:51:11 2010 -0700
     6.3 @@ -508,7 +508,7 @@
     6.4    have "real m < 2^(nat (-e))" using `Float m e < 1`
     6.5      unfolding less_float_def real_of_float_neg_exp[OF `e < 0`] real_of_float_1
     6.6            real_mult_less_iff1[of _ _ 1, OF `0 < 2^(nat (-e))`, symmetric] 
     6.7 -          real_mult_assoc by auto
     6.8 +          mult_assoc by auto
     6.9    thus ?thesis unfolding real_of_int_less_iff[symmetric] by auto
    6.10  qed
    6.11  
    6.12 @@ -619,7 +619,7 @@
    6.13    case True show ?thesis unfolding real_of_float_simp pow2_def using True by auto
    6.14  next
    6.15    case False hence P: "\<not> 0 \<le> - (bitlen m - 1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto
    6.16 -  show ?thesis unfolding real_of_float_nge0_exp[OF P] real_divide_def by auto
    6.17 +  show ?thesis unfolding real_of_float_nge0_exp[OF P] divide_inverse by auto
    6.18  qed
    6.19  
    6.20  lemma bitlen_Pls: "bitlen (Int.Pls) = Int.Pls" by (subst Pls_def, subst Pls_def, simp)
    6.21 @@ -683,7 +683,7 @@
    6.22    have "real (x * 2^?l div y) * inverse (2^?l) \<le> (real (x * 2^?l) / real y) * inverse (2^?l)" 
    6.23      by (rule mult_right_mono, fact real_of_int_div4, simp)
    6.24    also have "\<dots> \<le> (real x / real y) * 2^?l * inverse (2^?l)" by auto
    6.25 -  finally have "real (x * 2^?l div y) * inverse (2^?l) \<le> real x / real y" unfolding real_mult_assoc by auto
    6.26 +  finally have "real (x * 2^?l div y) * inverse (2^?l) \<le> real x / real y" unfolding mult_assoc by auto
    6.27    thus ?thesis unfolding lapprox_posrat_def Let_def normfloat real_of_float_simp
    6.28      unfolding pow2_minus pow2_int minus_minus .
    6.29  qed
    6.30 @@ -700,7 +700,7 @@
    6.31      unfolding real_of_int_mult[symmetric] real_of_int_le_iff zmult_commute by auto
    6.32    hence "real (x div y) * real c * inverse (real c) \<le> real (x * c div y) * inverse (real c)"
    6.33      using `0 < c` by auto
    6.34 -  thus ?thesis unfolding real_mult_assoc using `0 < c` by auto
    6.35 +  thus ?thesis unfolding mult_assoc using `0 < c` by auto
    6.36  qed
    6.37  
    6.38  lemma lapprox_posrat_bottom: assumes "0 < y"
    6.39 @@ -757,7 +757,7 @@
    6.40        by (rule divide_right_mono, simp only: `0 \<le> real y * 2^?l`)
    6.41      also have "\<dots> = real y * real (?X div y + 1) / real y / 2^?l" by auto
    6.42      also have "\<dots> = real (?X div y + 1) * inverse (2^?l)" unfolding nonzero_mult_divide_cancel_left[OF `real y \<noteq> 0`] 
    6.43 -      unfolding real_divide_def ..
    6.44 +      unfolding divide_inverse ..
    6.45      finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
    6.46        unfolding pow2_minus pow2_int minus_minus by auto
    6.47    qed
    6.48 @@ -856,7 +856,7 @@
    6.49        finally have "real y * 2^nat (bitlen x - 1) * inverse (2^nat (bitlen x - 1)) \<le> real x * 2^nat (int (n - 1) + bitlen y) * inverse (2^nat (bitlen x - 1))"
    6.50          unfolding real_of_int_le_iff[symmetric] by auto
    6.51        hence "real y \<le> real x * (2^nat (int (n - 1) + bitlen y) / (2^nat (bitlen x - 1)))" 
    6.52 -        unfolding real_mult_assoc real_divide_def by auto
    6.53 +        unfolding mult_assoc divide_inverse by auto
    6.54        also have "\<dots> = real x * (2^(nat (int (n - 1) + bitlen y) - nat (bitlen x - 1)))" using power_diff[of "2::real", OF _ len_less] by auto
    6.55        finally have "y \<le> x * 2^?l" unfolding exp_eq unfolding real_of_int_le_iff[symmetric] by auto
    6.56        thus ?thesis using zdiv_greater_zero[OF `0 < y`] by auto
    6.57 @@ -1083,7 +1083,7 @@
    6.58      hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
    6.59      hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d"
    6.60        unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto }
    6.61 -  from mult_left_mono[OF this[unfolded pow_split power_add inverse_mult_distrib real_mult_assoc[symmetric] right_inverse[OF pow_not0] real_mult_1], of "2^?e"]
    6.62 +  from mult_left_mono[OF this[unfolded pow_split power_add inverse_mult_distrib mult_assoc[symmetric] right_inverse[OF pow_not0] mult_1_left], of "2^?e"]
    6.63    have "2^?e * inverse (2^?b) \<le> 2^?e * ?d" unfolding pow_split power_add by auto
    6.64    finally have "1 \<le> 2^?e * ?d" .
    6.65    
    6.66 @@ -1269,7 +1269,7 @@
    6.67        also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] ..
    6.68        finally show ?thesis by auto
    6.69      qed
    6.70 -    thus ?thesis unfolding lb_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add real_mult_commute real_mult_assoc by auto
    6.71 +    thus ?thesis unfolding lb_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add mult_commute mult_assoc by auto
    6.72    qed
    6.73    also have "\<dots> = real (x * y)" unfolding normfloat ..
    6.74    finally show ?thesis .
    6.75 @@ -1293,10 +1293,10 @@
    6.76        
    6.77        have "real m = real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding zmod_zdiv_equality[symmetric] ..
    6.78        also have "\<dots> = real (m div 2^(nat ?l)) * 2^(nat ?l) + real (m mod 2^(nat ?l))" unfolding real_of_int_add by auto
    6.79 -      also have "\<dots> \<le> (real (m div 2^(nat ?l)) + 1) * 2^(nat ?l)" unfolding real_add_mult_distrib using mod_uneq by auto
    6.80 +      also have "\<dots> \<le> (real (m div 2^(nat ?l)) + 1) * 2^(nat ?l)" unfolding left_distrib using mod_uneq by auto
    6.81        finally show ?thesis unfolding pow2_int[symmetric] using True by auto
    6.82      qed
    6.83 -    thus ?thesis unfolding ub_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add real_mult_commute real_mult_assoc by auto
    6.84 +    thus ?thesis unfolding ub_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add mult_commute mult_assoc by auto
    6.85    qed
    6.86    finally show ?thesis .
    6.87  qed
    6.88 @@ -1329,7 +1329,7 @@
    6.89      hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
    6.90      have "real (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding real_of_float_simp by auto
    6.91      also have "\<dots> \<le> real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 .
    6.92 -    also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
    6.93 +    also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_number_of divide_inverse ..
    6.94      also have "\<dots> = real (Float m e)" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
    6.95      finally show ?thesis unfolding Float floor_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
    6.96    next
    6.97 @@ -1357,7 +1357,7 @@
    6.98      case False
    6.99      hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
   6.100      have "real (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
   6.101 -    also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
   6.102 +    also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_number_of divide_inverse ..
   6.103      also have "\<dots> \<le> 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] .
   6.104      also have "\<dots> = real (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding real_of_float_simp by auto
   6.105      finally show ?thesis unfolding Float ceiling_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
     7.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun May 09 17:47:43 2010 -0700
     7.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun May 09 22:51:11 2010 -0700
     7.3 @@ -355,7 +355,7 @@
     7.4      from real_lbound_gt_zero[OF one0 em0]
     7.5      obtain d where d: "d >0" "d < 1" "d < e / m" by blast
     7.6      from d(1,3) m(1) have dm: "d*m > 0" "d*m < e"
     7.7 -      by (simp_all add: field_simps real_mult_order)
     7.8 +      by (simp_all add: field_simps mult_pos_pos)
     7.9      show ?case
    7.10        proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
    7.11          fix d w
     8.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun May 09 17:47:43 2010 -0700
     8.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun May 09 22:51:11 2010 -0700
     8.3 @@ -1589,7 +1589,7 @@
     8.4        thus ?thesis unfolding setsum_delta[OF assms(1)] using uv(2) and `u v < 0` and uv(1) by auto qed
     8.5    qed (insert setsum_nonneg_eq_0_iff[of _ u, OF fin(1)] uv(2-3), auto)
     8.6  
     8.7 -  hence *:"setsum u {x\<in>c. u x > 0} > 0" unfolding real_less_def apply(rule_tac conjI, rule_tac setsum_nonneg) by auto
     8.8 +  hence *:"setsum u {x\<in>c. u x > 0} > 0" unfolding less_le apply(rule_tac conjI, rule_tac setsum_nonneg) by auto
     8.9    moreover have "setsum u ({x \<in> c. 0 < u x} \<union> {x \<in> c. u x < 0}) = setsum u c"
    8.10      "(\<Sum>x\<in>{x \<in> c. 0 < u x} \<union> {x \<in> c. u x < 0}. u x *\<^sub>R x) = (\<Sum>x\<in>c. u x *\<^sub>R x)"
    8.11      using assms(1) apply(rule_tac[!] setsum_mono_zero_left) by auto
    8.12 @@ -1943,7 +1943,7 @@
    8.13    apply (drule_tac x="\<lambda>i. (x i, f (x i))" in spec)
    8.14    apply simp
    8.15    using assms[unfolded convex] apply simp
    8.16 -  apply(rule_tac j="\<Sum>i = 1..k. u i * f (fst (x i))" in real_le_trans)
    8.17 +  apply(rule_tac y="\<Sum>i = 1..k. u i * f (fst (x i))" in order_trans)
    8.18    defer apply(rule setsum_mono) apply(erule_tac x=i in allE) unfolding real_scaleR_def
    8.19    apply(rule mult_left_mono)using assms[unfolded convex] by auto
    8.20  
    8.21 @@ -2182,7 +2182,7 @@
    8.22          have "f x \<le> 1 / (1 + t) * f w + (t / (1 + t)) * f y" 
    8.23            using assms(2)[unfolded convex_on_def,rule_format,of w y "1/(1+t)" "t / (1+t)",unfolded w]
    8.24            using `0<t` `2<t` and `y\<in>s` `w\<in>s` by (auto simp add:field_simps)
    8.25 -        also have "\<dots> = (f w + t * f y) / (1 + t)" using `t>0` unfolding real_divide_def by (auto simp add:field_simps)
    8.26 +        also have "\<dots> = (f w + t * f y) / (1 + t)" using `t>0` unfolding divide_inverse by (auto simp add:field_simps)
    8.27          also have "\<dots> < e + f y" using `t>0` * `e>0` by(auto simp add:field_simps)
    8.28          finally have "f x - f y < e" by auto }
    8.29        ultimately show ?thesis by auto 
    8.30 @@ -2231,7 +2231,7 @@
    8.31      apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof 
    8.32      fix z assume z:"z\<in>{x - ?d..x + ?d}"
    8.33      have e:"e = setsum (\<lambda>i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1
    8.34 -      by (metis eq_divide_imp times_divide_eq_left real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute)
    8.35 +      by (metis eq_divide_imp times_divide_eq_left real_dimindex_gt_0 real_eq_of_nat less_le mult_commute)
    8.36      show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
    8.37        using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed
    8.38    hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption
    8.39 @@ -2411,7 +2411,7 @@
    8.40        by(auto simp add: Cart_eq field_simps) 
    8.41      also have "\<dots> = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:norm_eqI simp add: algebra_simps)
    8.42      also have "\<dots> < d" using as[unfolded dist_norm] and `e>0`
    8.43 -      by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute)
    8.44 +      by(auto simp add:pos_divide_less_eq[OF `e>0`] mult_commute)
    8.45      finally show "y \<in> s" apply(subst *) apply(rule assms(1)[unfolded convex_alt,rule_format])
    8.46        apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) by auto
    8.47    qed(rule mult_pos_pos, insert `e>0` `d>0`, auto) qed
    8.48 @@ -2522,7 +2522,7 @@
    8.49    show ?thesis apply(rule that[of ?a]) unfolding interior_std_simplex mem_Collect_eq proof(rule,rule)
    8.50      fix i::'n show "0 < ?a $ i" unfolding ** using dimindex_ge_1 by(auto simp add: Suc_le_eq) next
    8.51      have "setsum (op $ ?a) ?D = setsum (\<lambda>i. inverse (2 * real CARD('n))) ?D" by(rule setsum_cong2, rule **) 
    8.52 -    also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat real_divide_def[THEN sym] by (auto simp add:field_simps)
    8.53 +    also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat divide_inverse[THEN sym] by (auto simp add:field_simps)
    8.54      finally show "setsum (op $ ?a) ?D < 1" by auto qed qed
    8.55  
    8.56  end
     9.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun May 09 17:47:43 2010 -0700
     9.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun May 09 22:51:11 2010 -0700
     9.3 @@ -3677,7 +3677,7 @@
     9.4    from Sup_finite_in[OF fS S0] 
     9.5    show ?thesis unfolding infnorm_def infnorm_set_image 
     9.6      by (metis Sup_finite_ge_iff finite finite_imageI UNIV_not_empty image_is_empty 
     9.7 -              rangeI real_le_refl)
     9.8 +              rangeI order_refl)
     9.9  qed
    9.10  
    9.11  lemma infnorm_mul_lemma: "infnorm(a *s x) <= \<bar>a\<bar> * infnorm x"
    10.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun May 09 17:47:43 2010 -0700
    10.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun May 09 22:51:11 2010 -0700
    10.3 @@ -2195,7 +2195,7 @@
    10.4    shows "norm(setsum (\<lambda>l. content l *\<^sub>R c) p) \<le> e * content({a..b})" (is "?l \<le> ?r")
    10.5    apply(rule order_trans,rule setsum_norm) defer unfolding norm_scaleR setsum_left_distrib[THEN sym]
    10.6    apply(rule order_trans[OF mult_left_mono],rule assms,rule setsum_abs_ge_zero)
    10.7 -  apply(subst real_mult_commute) apply(rule mult_left_mono)
    10.8 +  apply(subst mult_commute) apply(rule mult_left_mono)
    10.9    apply(rule order_trans[of _ "setsum content p"]) apply(rule eq_refl,rule setsum_cong2)
   10.10    apply(subst abs_of_nonneg) unfolding additive_content_division[OF assms(1)]
   10.11  proof- from order_trans[OF norm_ge_zero[of c] assms(2)] show "0 \<le> e" .
   10.12 @@ -2210,7 +2210,7 @@
   10.13  next case False show ?thesis
   10.14      apply(rule order_trans,rule setsum_norm) defer unfolding split_def norm_scaleR
   10.15      apply(rule order_trans[OF setsum_mono]) apply(rule mult_left_mono[OF _ abs_ge_zero, of _ e]) defer
   10.16 -    unfolding setsum_left_distrib[THEN sym] apply(subst real_mult_commute) apply(rule mult_left_mono)
   10.17 +    unfolding setsum_left_distrib[THEN sym] apply(subst mult_commute) apply(rule mult_left_mono)
   10.18      apply(rule order_trans[of _ "setsum (content \<circ> snd) p"]) apply(rule eq_refl,rule setsum_cong2)
   10.19      apply(subst o_def, rule abs_of_nonneg)
   10.20    proof- show "setsum (content \<circ> snd) p \<le> content {a..b}" apply(rule eq_refl)
   10.21 @@ -2395,7 +2395,7 @@
   10.22              using g(1)[OF x, of n] g(1)[OF x, of m] by auto
   10.23          also have "\<dots> \<le> inverse (real M) + inverse (real M)" apply(rule add_mono)
   10.24            apply(rule_tac[!] le_imp_inverse_le) using goal1 M by auto
   10.25 -        also have "\<dots> = 2 / real M" unfolding real_divide_def by auto
   10.26 +        also have "\<dots> = 2 / real M" unfolding divide_inverse by auto
   10.27          finally show "norm (g n x - g m x) \<le> 2 / real M"
   10.28            using norm_triangle_le[of "g n x - f x" "f x - g m x" "2 / real M"]
   10.29            by(auto simp add:algebra_simps simp add:norm_minus_commute)
   10.30 @@ -2672,7 +2672,7 @@
   10.31        also have "... \<le> setsum (\<lambda>i. e / 2 / 2 ^ i) {0..N+1}" apply(rule setsum_mono) 
   10.32        proof- case goal1 thus ?case apply(subst mult_commute, subst pos_le_divide_eq[THEN sym])
   10.33            using d(2)[rule_format,of "q i" i] using q[rule_format] by(auto simp add:field_simps)
   10.34 -      qed also have "... < e * inverse 2 * 2" unfolding real_divide_def setsum_right_distrib[THEN sym]
   10.35 +      qed also have "... < e * inverse 2 * 2" unfolding divide_inverse setsum_right_distrib[THEN sym]
   10.36          apply(rule mult_strict_left_mono) unfolding power_inverse atLeastLessThanSuc_atLeastAtMost[THEN sym]
   10.37          apply(subst sumr_geometric) using goal1 by auto
   10.38        finally show "?goal" by auto qed qed qed
   10.39 @@ -3261,7 +3261,7 @@
   10.40              using as by(auto simp add:field_simps)
   10.41          next assume as:"0 > m i" hence *:"max (m i * a $ i) (m i * b $ i) = m i * a $ i"
   10.42              "min (m i * a $ i) (m i * b $ i) = m i * b $ i" using ab as unfolding min_def max_def 
   10.43 -            by(auto simp add:field_simps mult_le_cancel_left_neg intro:real_le_antisym)
   10.44 +            by(auto simp add:field_simps mult_le_cancel_left_neg intro: order_antisym)
   10.45            show ?thesis unfolding * apply rule defer apply(rule_tac x="1 / m i * x$i" in exI)
   10.46              using as by(auto simp add:field_simps) qed qed qed qed qed 
   10.47  
   10.48 @@ -3567,7 +3567,7 @@
   10.49        hence "c$1 - t$1 < e / 3 / norm (f c)" by auto
   10.50        hence "norm (c - t) < e / 3 / norm (f c)" using as unfolding norm_vector_1 vector_less_def by auto
   10.51        thus "norm (f c) * norm (c - t) < e / 3" using False apply-
   10.52 -        apply(subst real_mult_commute) apply(subst pos_less_divide_eq[THEN sym]) by auto
   10.53 +        apply(subst mult_commute) apply(subst pos_less_divide_eq[THEN sym]) by auto
   10.54      qed next case True show ?thesis apply(rule_tac x=1 in exI) unfolding True using `e>0` by auto
   10.55    qed then guess w .. note w = conjunctD2[OF this,rule_format]
   10.56    
   10.57 @@ -4408,8 +4408,8 @@
   10.58    next  case goal1 have *:"k * real (card r) / (1 + real (card r)) < k" using k by(auto simp add:field_simps)
   10.59      show ?case apply(rule le_less_trans[of _ "setsum (\<lambda>x. k / (real (card r) + 1)) r"])
   10.60        unfolding setsum_subtractf[THEN sym] apply(rule setsum_norm_le,fact)
   10.61 -      apply rule apply(drule qq) defer unfolding real_divide_def setsum_left_distrib[THEN sym]
   10.62 -      unfolding real_divide_def[THEN sym] using * by(auto simp add:field_simps real_eq_of_nat)
   10.63 +      apply rule apply(drule qq) defer unfolding divide_inverse setsum_left_distrib[THEN sym]
   10.64 +      unfolding divide_inverse[THEN sym] using * by(auto simp add:field_simps real_eq_of_nat)
   10.65    qed finally show "?x \<le> e + k" . qed
   10.66  
   10.67  lemma henstock_lemma_part2: fixes f::"real^'m \<Rightarrow> real^'n"
   10.68 @@ -4525,7 +4525,7 @@
   10.69               apply(rule le_less_trans[of _ "setsum (\<lambda>i. e / 2^(i+2)) {0..s}"])
   10.70               apply(rule setsum_norm_le[OF finite_atLeastAtMost])
   10.71             proof show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2"
   10.72 -               unfolding power_add real_divide_def inverse_mult_distrib
   10.73 +               unfolding power_add divide_inverse inverse_mult_distrib
   10.74                 unfolding setsum_right_distrib[THEN sym] setsum_left_distrib[THEN sym]
   10.75                 unfolding power_inverse sum_gp apply(rule mult_strict_left_mono[OF _ e])
   10.76                 unfolding power2_eq_square by auto
    11.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun May 09 17:47:43 2010 -0700
    11.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun May 09 22:51:11 2010 -0700
    11.3 @@ -1777,7 +1777,7 @@
    11.4            by (auto simp add: norm_minus_commute)
    11.5          also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
    11.6            unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
    11.7 -          unfolding real_add_mult_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
    11.8 +          unfolding left_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
    11.9          also have "\<dots> \<le> e - d/2" using `d \<le> dist x y` and `d>0` and `?rhs` by(auto simp add: dist_norm)
   11.10          finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using `d>0` by auto
   11.11  
   11.12 @@ -2104,10 +2104,10 @@
   11.13    { fix x assume "x\<in>S"
   11.14      hence "norm x \<le> b" using b by auto
   11.15      hence "norm (f x) \<le> B * b" using B(2) apply(erule_tac x=x in allE)
   11.16 -      by (metis B(1) B(2) real_le_trans real_mult_le_cancel_iff2)
   11.17 +      by (metis B(1) B(2) order_trans mult_le_cancel_left_pos)
   11.18    }
   11.19    thus ?thesis unfolding bounded_pos apply(rule_tac x="b*B" in exI)
   11.20 -    using b B real_mult_order[of b B] by (auto simp add: real_mult_commute)
   11.21 +    using b B mult_pos_pos [of b B] by (auto simp add: mult_commute)
   11.22  qed
   11.23  
   11.24  lemma bounded_scaling:
   11.25 @@ -3061,7 +3061,7 @@
   11.26      { fix e::real assume "e>0"
   11.27        hence "dist a b < e" using assms(4 )using b using a by blast
   11.28      }
   11.29 -    hence "dist a b = 0" by (metis dist_eq_0_iff dist_nz real_less_def)
   11.30 +    hence "dist a b = 0" by (metis dist_eq_0_iff dist_nz less_le)
   11.31    }
   11.32    with a have "\<Inter>(range s) = {a}" unfolding image_def by auto
   11.33    thus ?thesis ..
   11.34 @@ -3841,7 +3841,7 @@
   11.35  proof-
   11.36    { fix x assume "x \<in> s"
   11.37      then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]] by auto
   11.38 -    have "e * abs c > 0" using assms(1)[unfolded zero_less_abs_iff[THEN sym]] using real_mult_order[OF `e>0`] by auto
   11.39 +    have "e * abs c > 0" using assms(1)[unfolded zero_less_abs_iff[THEN sym]] using mult_pos_pos[OF `e>0`] by auto
   11.40      moreover
   11.41      { fix y assume "dist y (c *\<^sub>R x) < e * \<bar>c\<bar>"
   11.42        hence "norm ((1 / c) *\<^sub>R y - x) < e" unfolding dist_norm
   11.43 @@ -5015,7 +5015,7 @@
   11.44  lemma is_interval_interval: "is_interval {a .. b::real^'n}" (is ?th1) "is_interval {a<..<b}" (is ?th2) proof - 
   11.45    have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
   11.46    show ?th1 ?th2  unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
   11.47 -    by(meson real_le_trans le_less_trans less_le_trans *)+ qed
   11.48 +    by(meson order_trans le_less_trans less_le_trans *)+ qed
   11.49  
   11.50  lemma is_interval_empty:
   11.51   "is_interval {}"
   11.52 @@ -5423,7 +5423,7 @@
   11.53        hence "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}" using `x\<in>s` and `x\<noteq>0` by auto
   11.54        thus "norm (f b) / norm b * norm x \<le> norm (f x)" using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]]
   11.55          unfolding f.scaleR and ba using `x\<noteq>0` `a\<noteq>0`
   11.56 -        by (auto simp add: real_mult_commute pos_le_divide_eq pos_divide_le_eq)
   11.57 +        by (auto simp add: mult_commute pos_le_divide_eq pos_divide_le_eq)
   11.58      qed }
   11.59    ultimately
   11.60    show ?thesis by auto
   11.61 @@ -5647,14 +5647,14 @@
   11.62        unfolding image_iff Bex_def mem_interval vector_le_def
   11.63        apply(auto simp add: vector_smult_assoc pth_3[symmetric]
   11.64          intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
   11.65 -      by(auto simp add: pos_le_divide_eq pos_divide_le_eq real_mult_commute diff_le_iff)
   11.66 +      by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
   11.67    } moreover
   11.68    { fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
   11.69      hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
   11.70        unfolding image_iff Bex_def mem_interval vector_le_def
   11.71        apply(auto simp add: vector_smult_assoc pth_3[symmetric]
   11.72          intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
   11.73 -      by(auto simp add: neg_le_divide_eq neg_divide_le_eq real_mult_commute diff_le_iff)
   11.74 +      by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
   11.75    }
   11.76    ultimately show ?thesis using False by auto
   11.77  qed
   11.78 @@ -5723,7 +5723,7 @@
   11.79        thus ?thesis using `e>0` by auto
   11.80      next
   11.81        case False hence "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]
   11.82 -        by (metis False d_def real_less_def)
   11.83 +        by (metis False d_def less_le)
   11.84        hence "0 < e * (1 - c) / d" using `e>0` and `1-c>0`
   11.85          using divide_pos_pos[of "e * (1 - c)" d] and mult_pos_pos[of e "1 - c"] by auto
   11.86        then obtain N where N:"c ^ N < e * (1 - c) / d" using real_arch_pow_inv[of "e * (1 - c) / d" c] and c by auto
   11.87 @@ -5731,18 +5731,18 @@
   11.88          have *:"c ^ n \<le> c ^ N" using `n\<ge>N` and c using power_decreasing[OF `n\<ge>N`, of c] by auto
   11.89          have "1 - c ^ (m - n) > 0" using c and power_strict_mono[of c 1 "m - n"] using `m>n` by auto
   11.90          hence **:"d * (1 - c ^ (m - n)) / (1 - c) > 0"
   11.91 -          using real_mult_order[OF `d>0`, of "1 - c ^ (m - n)"]
   11.92 +          using mult_pos_pos[OF `d>0`, of "1 - c ^ (m - n)"]
   11.93            using divide_pos_pos[of "d * (1 - c ^ (m - n))" "1 - c"]
   11.94            using `0 < 1 - c` by auto
   11.95  
   11.96          have "dist (z m) (z n) \<le> c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
   11.97            using cf_z2[of n "m - n"] and `m>n` unfolding pos_le_divide_eq[OF `1-c>0`]
   11.98 -          by (auto simp add: real_mult_commute dist_commute)
   11.99 +          by (auto simp add: mult_commute dist_commute)
  11.100          also have "\<dots> \<le> c ^ N * d * (1 - c ^ (m - n)) / (1 - c)"
  11.101            using mult_right_mono[OF * order_less_imp_le[OF **]]
  11.102 -          unfolding real_mult_assoc by auto
  11.103 +          unfolding mult_assoc by auto
  11.104          also have "\<dots> < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)"
  11.105 -          using mult_strict_right_mono[OF N **] unfolding real_mult_assoc by auto
  11.106 +          using mult_strict_right_mono[OF N **] unfolding mult_assoc by auto
  11.107          also have "\<dots> = e * (1 - c ^ (m - n))" using c and `d>0` and `1 - c > 0` by auto
  11.108          also have "\<dots> \<le> e" using c and `1 - c ^ (m - n) > 0` and `e>0` using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto
  11.109          finally have  "dist (z m) (z n) < e" by auto
  11.110 @@ -5770,7 +5770,7 @@
  11.111  
  11.112      have *:"c * dist (z N) x \<le> dist (z N) x" unfolding mult_le_cancel_right2
  11.113        using zero_le_dist[of "z N" x] and c
  11.114 -      by (metis dist_eq_0_iff dist_nz order_less_asym real_less_def)
  11.115 +      by (metis dist_eq_0_iff dist_nz order_less_asym less_le)
  11.116      have "dist (f (z N)) (f x) \<le> c * dist (z N) x" using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]]
  11.117        using z_in_s[of N] `x\<in>s` using c by auto
  11.118      also have "\<dots> < e / 2" using N' and c using * by auto
    12.1 --- a/src/HOL/Probability/Borel.thy	Sun May 09 17:47:43 2010 -0700
    12.2 +++ b/src/HOL/Probability/Borel.thy	Sun May 09 22:51:11 2010 -0700
    12.3 @@ -68,9 +68,9 @@
    12.4      with w have "real(Suc(natceiling(inverse(g w - f w)))) > inverse(g w - f w)"
    12.5        by (metis lessI order_le_less_trans real_natceiling_ge real_of_nat_less_iff)       hence "inverse(real(Suc(natceiling(inverse(g w - f w)))))
    12.6               < inverse(inverse(g w - f w))" 
    12.7 -      by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_linordered_idom nz positive_imp_inverse_positive real_le_antisym real_less_def w)
    12.8 +      by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_linordered_idom nz positive_imp_inverse_positive order_antisym less_le w)
    12.9      hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < g w - f w"
   12.10 -      by (metis inverse_inverse_eq order_less_le_trans real_le_refl) 
   12.11 +      by (metis inverse_inverse_eq order_less_le_trans order_refl)
   12.12      thus "\<exists>n. f w \<le> g w - inverse(real(Suc n))" using w
   12.13        by (rule_tac x="natceiling(inverse(g w - f w))" in exI, auto)
   12.14    next
   12.15 @@ -357,7 +357,7 @@
   12.16                      borel_measurable_uminus_borel_measurable f g)
   12.17    finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
   12.18    show ?thesis
   12.19 -    apply (simp add: times_eq_sum_squares real_diff_def) 
   12.20 +    apply (simp add: times_eq_sum_squares diff_def) 
   12.21      using 1 2 apply (simp add: borel_measurable_add_borel_measurable) 
   12.22      done
   12.23  qed
   12.24 @@ -366,7 +366,7 @@
   12.25    assumes f: "f \<in> borel_measurable M"
   12.26    assumes g: "g \<in> borel_measurable M"
   12.27    shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   12.28 -unfolding real_diff_def
   12.29 +unfolding diff_def
   12.30    by (fast intro: borel_measurable_add_borel_measurable 
   12.31                    borel_measurable_uminus_borel_measurable f g)
   12.32  
   12.33 @@ -397,7 +397,7 @@
   12.34    { fix w
   12.35      from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
   12.36        by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
   12.37 -                linorder_not_le real_le_refl real_le_trans real_less_def
   12.38 +                linorder_not_le order_refl order_trans less_le
   12.39                  xt1(7) zero_less_divide_1_iff) }
   12.40    hence "{w \<in> space M. a \<le> inverse (f w)} =
   12.41      {w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
   12.42 @@ -418,7 +418,7 @@
   12.43        apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9)
   12.44                     zero_le_divide_1_iff)
   12.45        apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg
   12.46 -                   linorder_not_le real_le_refl real_le_trans)
   12.47 +                   linorder_not_le order_refl order_trans)
   12.48        done }
   12.49    hence "{w \<in> space M. a \<le> inverse (f w)} =
   12.50      {w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto
   12.51 @@ -627,11 +627,11 @@
   12.52  proof -
   12.53    from assms have "y - z > 0" by simp
   12.54    hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
   12.55 -    unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def
   12.56 +    unfolding incseq_def LIMSEQ_def dist_real_def diff_def
   12.57      by simp
   12.58    have "\<forall>m. x m \<le> y" using incseq_le assms by auto
   12.59    hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
   12.60 -    by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def)
   12.61 +    by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le diff_def)
   12.62    from A B show ?thesis by auto
   12.63  qed
   12.64  
    13.1 --- a/src/HOL/Probability/Lebesgue.thy	Sun May 09 17:47:43 2010 -0700
    13.2 +++ b/src/HOL/Probability/Lebesgue.thy	Sun May 09 22:51:11 2010 -0700
    13.3 @@ -28,17 +28,17 @@
    13.4  lemma pos_neg_part_abs:
    13.5    fixes f :: "'a \<Rightarrow> real"
    13.6    shows "pos_part f x + neg_part f x = \<bar>f x\<bar>"
    13.7 -unfolding real_abs_def pos_part_def neg_part_def by auto
    13.8 +unfolding abs_if pos_part_def neg_part_def by auto
    13.9  
   13.10  lemma pos_part_abs:
   13.11    fixes f :: "'a \<Rightarrow> real"
   13.12    shows "pos_part (\<lambda> x. \<bar>f x\<bar>) y = \<bar>f y\<bar>"
   13.13 -unfolding pos_part_def real_abs_def by auto
   13.14 +unfolding pos_part_def abs_if by auto
   13.15  
   13.16  lemma neg_part_abs:
   13.17    fixes f :: "'a \<Rightarrow> real"
   13.18    shows "neg_part (\<lambda> x. \<bar>f x\<bar>) y = 0"
   13.19 -unfolding neg_part_def real_abs_def by auto
   13.20 +unfolding neg_part_def abs_if by auto
   13.21  
   13.22  lemma (in measure_space)
   13.23    assumes "f \<in> borel_measurable M"
   13.24 @@ -341,7 +341,8 @@
   13.25    have "pos_simple_integral (k, c, (\<lambda> x. z x + z' x))
   13.26      = (\<Sum> x \<in> k. (z x + z' x) * measure M (c x))"
   13.27      unfolding pos_simple_integral_def by auto
   13.28 -  also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x) + z' x * measure M (c x))" using real_add_mult_distrib by auto
   13.29 +  also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x) + z' x * measure M (c x))"
   13.30 +    by (simp add: left_distrib)
   13.31    also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x)) + (\<Sum> x \<in> k. z' x * measure M (c x))" using setsum_addf by auto
   13.32    also have "\<dots> = pos_simple_integral (k, c, z) + pos_simple_integral (k, c, z')" unfolding pos_simple_integral_def by auto
   13.33    finally have ths: "pos_simple_integral (s, a, x) + pos_simple_integral (s', b, y) =
   13.34 @@ -436,12 +437,12 @@
   13.35  lemma pos_simple_fn_integral_unique:
   13.36    assumes "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple f"
   13.37    shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
   13.38 -using assms real_le_antisym real_le_refl pos_simple_integral_mono by metis
   13.39 +using assms by (rule pos_simple_integral_equal) (* FIXME: redundant lemma *)
   13.40  
   13.41  lemma psfis_unique:
   13.42    assumes "a \<in> psfis f" "b \<in> psfis f"
   13.43    shows "a = b"
   13.44 -using assms real_le_antisym real_le_refl psfis_mono by metis
   13.45 +using assms by (intro order_antisym psfis_mono [OF _ _ order_refl])
   13.46  
   13.47  lemma pos_simple_integral_indicator:
   13.48    assumes "A \<in> sets M"
   13.49 @@ -557,7 +558,7 @@
   13.50        using borel_measurable_indicator using sa'x[unfolded pos_simple_def] by auto
   13.51      hence "(\<lambda> w. x i * indicator_fn (a' i) w) \<in> borel_measurable M"
   13.52        using affine_borel_measurable[of "\<lambda> w. indicator_fn (a' i) w" 0 "x i"]
   13.53 -        real_mult_commute by auto }
   13.54 +        by (simp add: mult_commute) }
   13.55    from borel_measurable_setsum_borel_measurable[OF fs this] affine_borel_measurable
   13.56    have "(\<lambda> w. (\<Sum> i \<in> s. x i * indicator_fn (a' i) w)) \<in> borel_measurable M" by auto
   13.57    from borel_measurable_cong[OF pos_simple_setsum_indicator_fn[OF sa'x]] this
   13.58 @@ -743,7 +744,7 @@
   13.59    assumes a: "a \<in> nnfis f" and b: "b \<in> nnfis f"
   13.60    shows "a = b"
   13.61    using nnfis_mono[OF a b] nnfis_mono[OF b a]
   13.62 -  by (auto intro!: real_le_antisym[of a b])
   13.63 +  by (auto intro!: order_antisym[of a b])
   13.64  
   13.65  lemma psfis_equiv:
   13.66    assumes "a \<in> psfis f" and "nonneg g"
   13.67 @@ -843,7 +844,7 @@
   13.68        from nnfis this mono_convergent_le[OF mc]
   13.69        show "x n \<le> l" by (rule nnfis_mono)
   13.70      qed
   13.71 -    ultimately have "l = z" by (rule real_le_antisym)
   13.72 +    ultimately have "l = z" by (rule order_antisym)
   13.73      thus "c ----> z" using `c ----> l` by simp
   13.74    qed
   13.75  qed
   13.76 @@ -859,7 +860,7 @@
   13.77      by auto
   13.78    thus "0 \<le> f x" using uy[rule_format]
   13.79      unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
   13.80 -    using incseq_le[of "\<lambda> n. u n x" "f x"] real_le_trans
   13.81 +    using incseq_le[of "\<lambda> n. u n x" "f x"] order_trans
   13.82      by fast
   13.83  qed
   13.84  
   13.85 @@ -1335,10 +1336,10 @@
   13.86    also have "\<dots> \<le> integral (\<lambda> t. \<bar> f t \<bar> ^ n)"
   13.87      apply (rule integral_mono)
   13.88      using integral_cmul_indicator[OF w]
   13.89 -      `integrable (\<lambda> x. \<bar>f x\<bar> ^ n)` real_le_trans[OF v1 v2] by auto
   13.90 +      `integrable (\<lambda> x. \<bar>f x\<bar> ^ n)` order_trans[OF v1 v2] by auto
   13.91    finally show "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
   13.92      unfolding atLeast_def
   13.93 -    by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
   13.94 +    by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: mult_commute)
   13.95  qed
   13.96  
   13.97  lemma (in measure_space) integral_0:
    14.1 --- a/src/HOL/ex/Sqrt_Script.thy	Sun May 09 17:47:43 2010 -0700
    14.2 +++ b/src/HOL/ex/Sqrt_Script.thy	Sun May 09 22:51:11 2010 -0700
    14.3 @@ -61,7 +61,7 @@
    14.4    apply (rule notI)
    14.5    apply (erule Rats_abs_nat_div_natE)
    14.6    apply (simp del: real_of_nat_mult
    14.7 -              add: real_abs_def divide_eq_eq prime_not_square real_of_nat_mult [symmetric])
    14.8 +              add: abs_if divide_eq_eq prime_not_square real_of_nat_mult [symmetric])
    14.9    done
   14.10  
   14.11  lemmas two_sqrt_irrational =