--- a/src/HOL/Decision_Procs/Approximation.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Decision_Procs/Approximation.thy Sun May 09 22:51:11 2010 -0700
@@ -18,7 +18,7 @@
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)"
proof -
have shift_pow: "\<And>i. - (x * ((-1)^i * a (Suc i) * x ^ i)) = (-1)^(Suc i) * a (Suc i) * x ^ (Suc i)" by auto
- show ?thesis unfolding setsum_right_distrib shift_pow real_diff_def setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
+ show ?thesis unfolding setsum_right_distrib shift_pow diff_def setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
setsum_reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\<lambda> n. (-1)^n *a n * x^n"] by auto
qed
@@ -109,8 +109,8 @@
proof (rule setsum_cong, simp)
fix j assume "j \<in> {0 ..< n}"
show "1 / real (f (j' + j)) * real x ^ j = -1 ^ j * (1 / real (f (j' + j))) * real (- x) ^ j"
- unfolding move_minus power_mult_distrib real_mult_assoc[symmetric]
- unfolding real_mult_commute unfolding real_mult_assoc[of "-1 ^ j", symmetric] power_mult_distrib[symmetric]
+ unfolding move_minus power_mult_distrib mult_assoc[symmetric]
+ unfolding mult_commute unfolding mult_assoc[of "-1 ^ j", symmetric] power_mult_distrib[symmetric]
by auto
qed
@@ -435,8 +435,8 @@
{ have "real (x * lb_arctan_horner prec n 1 (x*x)) \<le> ?S n"
using bounds(1) `0 \<le> real x`
- unfolding real_of_float_mult power_add power_one_right real_mult_assoc[symmetric] setsum_left_distrib[symmetric]
- unfolding real_mult_commute mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"]
+ unfolding real_of_float_mult power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric]
+ unfolding mult_commute[where 'a=real] mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"]
by (auto intro!: mult_left_mono)
also have "\<dots> \<le> arctan (real x)" using arctan_bounds ..
finally have "real (x * lb_arctan_horner prec n 1 (x*x)) \<le> arctan (real x)" . }
@@ -444,8 +444,8 @@
{ have "arctan (real x) \<le> ?S (Suc n)" using arctan_bounds ..
also have "\<dots> \<le> real (x * ub_arctan_horner prec (Suc n) 1 (x*x))"
using bounds(2)[of "Suc n"] `0 \<le> real x`
- unfolding real_of_float_mult power_add power_one_right real_mult_assoc[symmetric] setsum_left_distrib[symmetric]
- unfolding real_mult_commute mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"]
+ unfolding real_of_float_mult power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric]
+ unfolding mult_commute[where 'a=real] mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"]
by (auto intro!: mult_left_mono)
finally have "arctan (real x) \<le> real (x * ub_arctan_horner prec (Suc n) 1 (x*x))" . }
ultimately show ?thesis by auto
@@ -616,7 +616,7 @@
using arctan_0_1_bounds[OF `0 \<le> real ?DIV` `real ?DIV \<le> 1`] by auto
also have "\<dots> \<le> 2 * arctan (real x / ?R)"
using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
- 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 .
+ 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 .
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] .
next
case False
@@ -644,7 +644,7 @@
using `0 \<le> arctan (real x)` arctan_inverse[OF `1 / real x \<noteq> 0`]
unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto
moreover
- 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
+ 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
ultimately
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]
by auto
@@ -696,7 +696,7 @@
show ?thesis
proof (cases "?DIV > 1")
case True
- 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
+ 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
from order_less_le_trans[OF arctan_ubound this, THEN less_imp_le]
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] .
next
@@ -706,7 +706,7 @@
have "0 \<le> real x / ?R" using `0 \<le> real x` `0 < ?R` unfolding real_0_le_divide_iff by auto
hence "0 \<le> real ?DIV" using monotone by (rule order_trans)
- have "arctan (real x) = 2 * arctan (real x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 real_mult_1 .
+ have "arctan (real x) = 2 * arctan (real x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left .
also have "\<dots> \<le> 2 * arctan (real ?DIV)"
using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
also have "\<dots> \<le> real (Float 1 1 * ?ub_horner ?DIV)" unfolding real_of_float_mult[of "Float 1 1"] Float_num
@@ -912,8 +912,8 @@
from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
OF `0 \<le> real (x * x)` f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
show "?lb" and "?ub" using `0 \<le> real x` unfolding real_of_float_mult
- unfolding power_add power_one_right real_mult_assoc[symmetric] setsum_left_distrib[symmetric]
- unfolding real_mult_commute
+ unfolding power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric]
+ unfolding mult_commute[where 'a=real]
by (auto intro!: mult_left_mono simp add: power_mult power2_eq_square[of "real x"])
qed
@@ -1179,7 +1179,7 @@
proof (induct n arbitrary: x)
case (Suc n)
have split_pi_off: "x + real (Suc n) * 2 * pi = (x + real n * 2 * pi) + 2 * pi"
- unfolding Suc_eq_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
+ unfolding Suc_eq_plus1 real_of_nat_add real_of_one left_distrib by auto
show ?case unfolding split_pi_off using Suc by auto
qed auto
@@ -1213,7 +1213,7 @@
round_down[of prec "lb_pi prec"] by auto
hence "real ?lx \<le> x - real k * 2 * pi \<and> x - real k * 2 * pi \<le> real ?ux"
using x by (cases "k = 0") (auto intro!: add_mono
- simp add: real_diff_def k[symmetric] less_float_def)
+ simp add: diff_def k[symmetric] less_float_def)
note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]
hence lx_less_ux: "real ?lx \<le> real ?ux" by (rule order_trans)
@@ -1227,7 +1227,7 @@
also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
using cos_monotone_minus_pi_0'[OF pi_lx lx x_le_0]
by (simp only: real_of_float_minus real_of_int_minus
- cos_minus real_diff_def mult_minus_left)
+ cos_minus diff_def mult_minus_left)
finally have "real (lb_cos prec (- ?lx)) \<le> cos x"
unfolding cos_periodic_int . }
note negative_lx = this
@@ -1240,7 +1240,7 @@
have "cos (x + real (-k) * 2 * pi) \<le> cos (real ?lx)"
using cos_monotone_0_pi'[OF lx_0 lx pi_x]
by (simp only: real_of_float_minus real_of_int_minus
- cos_minus real_diff_def mult_minus_left)
+ cos_minus diff_def mult_minus_left)
also have "\<dots> \<le> real (ub_cos prec ?lx)"
using lb_cos[OF lx_0 pi_lx] by simp
finally have "cos x \<le> real (ub_cos prec ?lx)"
@@ -1255,7 +1255,7 @@
have "cos (x + real (-k) * 2 * pi) \<le> cos (real (- ?ux))"
using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
by (simp only: real_of_float_minus real_of_int_minus
- cos_minus real_diff_def mult_minus_left)
+ cos_minus diff_def mult_minus_left)
also have "\<dots> \<le> real (ub_cos prec (- ?ux))"
using lb_cos_minus[OF pi_ux ux_0, of prec] by simp
finally have "cos x \<le> real (ub_cos prec (- ?ux))"
@@ -1272,7 +1272,7 @@
also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
using cos_monotone_0_pi'[OF x_ge_0 ux pi_ux]
by (simp only: real_of_float_minus real_of_int_minus
- cos_minus real_diff_def mult_minus_left)
+ cos_minus diff_def mult_minus_left)
finally have "real (lb_cos prec ?ux) \<le> cos x"
unfolding cos_periodic_int . }
note positive_ux = this
@@ -1347,7 +1347,7 @@
also have "\<dots> \<le> cos (real (?ux - 2 * ?lpi))"
using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
by (simp only: real_of_float_minus real_of_int_minus real_of_one
- number_of_Min real_diff_def mult_minus_left real_mult_1)
+ number_of_Min diff_def mult_minus_left mult_1_left)
also have "\<dots> = cos (real (- (?ux - 2 * ?lpi)))"
unfolding real_of_float_minus cos_minus ..
also have "\<dots> \<le> real (ub_cos prec (- (?ux - 2 * ?lpi)))"
@@ -1391,7 +1391,7 @@
also have "\<dots> \<le> cos (real (?lx + 2 * ?lpi))"
using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
by (simp only: real_of_float_minus real_of_int_minus real_of_one
- number_of_Min real_diff_def mult_minus_left real_mult_1)
+ number_of_Min diff_def mult_minus_left mult_1_left)
also have "\<dots> \<le> real (ub_cos prec (?lx + 2 * ?lpi))"
using lb_cos[OF lx_0 pi_lx] by simp
finally show ?thesis unfolding u by (simp add: real_of_float_max)
@@ -1531,7 +1531,7 @@
hence "real (floor_fl x) < 0" unfolding Float_floor real_of_float_simp using zero_less_pow2[of xe] by auto
hence "m < 0"
unfolding less_float_def real_of_float_0 Float_floor real_of_float_simp
- unfolding pos_prod_lt[OF zero_less_pow2[of e], unfolded real_mult_commute] by auto
+ unfolding pos_prod_lt[OF zero_less_pow2[of e], unfolded mult_commute] by auto
hence "1 \<le> - m" by auto
hence "0 < nat (- m)" by auto
moreover
@@ -1682,7 +1682,7 @@
{ fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric]
proof (rule mult_mono)
show "0 \<le> x ^ Suc (Suc n)" by (auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
- have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 real_mult_assoc[symmetric]
+ have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 mult_assoc[symmetric]
by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
thus "x ^ Suc (Suc n) \<le> x ^ Suc n" by auto
qed auto }
@@ -1700,7 +1700,7 @@
let "?s n" = "-1^n * (1 / real (1 + n)) * (real x)^(Suc n)"
- 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
+ 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
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",
OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
by (rule mult_right_mono)
@@ -1708,7 +1708,7 @@
finally show "?lb \<le> ?ln" .
have "?ln \<le> setsum ?s {0 ..< 2 * od + 1}" using ln_bounds(2)[OF `0 \<le> real x` `real x < 1`] by auto
- 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
+ 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
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",
OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
by (rule mult_right_mono)
@@ -2088,28 +2088,28 @@
"interpret_floatarith (Var n) vs = vs ! n"
lemma interpret_floatarith_divide: "interpret_floatarith (Mult a (Inverse b)) vs = (interpret_floatarith a vs) / (interpret_floatarith b vs)"
- unfolding real_divide_def interpret_floatarith.simps ..
+ unfolding divide_inverse interpret_floatarith.simps ..
lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
- unfolding real_diff_def interpret_floatarith.simps ..
+ unfolding diff_def interpret_floatarith.simps ..
lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
sin (interpret_floatarith a vs)"
unfolding sin_cos_eq interpret_floatarith.simps
- interpret_floatarith_divide interpret_floatarith_diff real_diff_def
+ interpret_floatarith_divide interpret_floatarith_diff diff_def
by auto
lemma interpret_floatarith_tan:
"interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (Inverse (Cos a))) vs =
tan (interpret_floatarith a vs)"
- unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def real_divide_def
+ unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse
by auto
lemma interpret_floatarith_powr: "interpret_floatarith (Exp (Mult b (Ln a))) vs = (interpret_floatarith a vs) powr (interpret_floatarith b vs)"
unfolding powr_def interpret_floatarith.simps ..
lemma interpret_floatarith_log: "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = log (interpret_floatarith b vs) (interpret_floatarith x vs)"
- unfolding log_def interpret_floatarith.simps real_divide_def ..
+ unfolding log_def interpret_floatarith.simps divide_inverse ..
lemma interpret_floatarith_num:
shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
--- a/src/HOL/Decision_Procs/MIR.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Decision_Procs/MIR.thy Sun May 09 22:51:11 2010 -0700
@@ -2177,7 +2177,7 @@
assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
with rcpos have "(real c)*(real x) < (real c)*(- (Inum (y # bs) e / real c))"
- by (simp only: real_mult_less_mono2[OF rcpos th1])
+ by (simp only: mult_strict_left_mono [OF th1 rcpos])
hence "real c * real x + Inum (y # bs) e \<noteq> 0"using rcpos by simp
thus "real c * real x + Inum (real x # bs) e \<noteq> 0"
using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] by simp
@@ -2194,7 +2194,7 @@
assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
with rcpos have "(real c)*(real x) < (real c)*(- (Inum (y # bs) e / real c))"
- by (simp only: real_mult_less_mono2[OF rcpos th1])
+ by (simp only: mult_strict_left_mono [OF th1 rcpos])
hence "real c * real x + Inum (y # bs) e \<noteq> 0"using rcpos by simp
thus "real c * real x + Inum (real x # bs) e \<noteq> 0"
using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] by simp
@@ -2211,7 +2211,7 @@
assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
with rcpos have "(real c)*(real x) < (real c)*(- (Inum (y # bs) e / real c))"
- by (simp only: real_mult_less_mono2[OF rcpos th1])
+ by (simp only: mult_strict_left_mono [OF th1 rcpos])
thus "real c * real x + Inum (real x # bs) e < 0"
using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
qed
@@ -2227,7 +2227,7 @@
assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
with rcpos have "(real c)*(real x) < (real c)*(- (Inum (y # bs) e / real c))"
- by (simp only: real_mult_less_mono2[OF rcpos th1])
+ by (simp only: mult_strict_left_mono [OF th1 rcpos])
thus "real c * real x + Inum (real x # bs) e \<le> 0"
using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
qed
@@ -2243,7 +2243,7 @@
assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
with rcpos have "(real c)*(real x) < (real c)*(- (Inum (y # bs) e / real c))"
- by (simp only: real_mult_less_mono2[OF rcpos th1])
+ by (simp only: mult_strict_left_mono [OF th1 rcpos])
thus "\<not> (real c * real x + Inum (real x # bs) e>0)"
using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
qed
@@ -2259,7 +2259,7 @@
assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
with rcpos have "(real c)*(real x) < (real c)*(- (Inum (y # bs) e / real c))"
- by (simp only: real_mult_less_mono2[OF rcpos th1])
+ by (simp only: mult_strict_left_mono [OF th1 rcpos])
thus "\<not> real c * real x + Inum (real x # bs) e \<ge> 0"
using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
qed
--- a/src/HOL/Hahn_Banach/Function_Norm.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy Sun May 09 22:51:11 2010 -0700
@@ -124,7 +124,7 @@
assume "y \<noteq> 0"
with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
and x: "x \<in> V" and neq: "x \<noteq> 0"
- by (auto simp add: B_def real_divide_def)
+ by (auto simp add: B_def divide_inverse)
from x neq have gt: "0 < \<parallel>x\<parallel>" ..
txt {* The thesis follows by a short calculation using the
@@ -139,7 +139,7 @@
then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
qed
also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
- by (rule real_mult_assoc)
+ by (rule Groups.mult_assoc)
also
from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp
@@ -224,7 +224,7 @@
proof (rule mult_right_mono)
from x show "0 \<le> \<parallel>x\<parallel>" ..
from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
- by (auto simp add: B_def real_divide_def)
+ by (auto simp add: B_def divide_inverse)
with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
by (rule fn_norm_ub)
qed
@@ -257,7 +257,7 @@
assume "b \<noteq> 0"
with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
and x_neq: "x \<noteq> 0" and x: "x \<in> V"
- by (auto simp add: B_def real_divide_def)
+ by (auto simp add: B_def divide_inverse)
note b_rep
also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
proof (rule mult_right_mono)
--- a/src/HOL/Hahn_Banach/Vector_Space.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy Sun May 09 22:51:11 2010 -0700
@@ -118,7 +118,7 @@
proof -
assume x: "x \<in> V"
have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
- by (simp add: real_diff_def)
+ by (simp add: diff_def)
also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
by (rule add_mult_distrib2)
also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
@@ -255,7 +255,7 @@
lemma (in vectorspace) mult_left_commute:
"x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x"
- by (simp add: real_mult_commute mult_assoc2)
+ by (simp add: mult_commute mult_assoc2)
lemma (in vectorspace) mult_zero_uniq:
"x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> a \<cdot> x = 0 \<Longrightarrow> a = 0"
--- a/src/HOL/Library/Convex.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Library/Convex.thy Sun May 09 22:51:11 2010 -0700
@@ -362,8 +362,7 @@
{ assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
hence "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
hence "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms
- using add_nonneg_pos[of "\<mu> *\<^sub>R x" "(1 - \<mu>) *\<^sub>R y"]
- real_mult_order by auto fastsimp }
+ by (auto simp add: add_pos_pos mult_pos_pos) }
ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastsimp
qed
@@ -426,7 +425,7 @@
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)"
using scaleR_right.setsum[of "inverse (1 - a i)" "\<lambda> j. a j *\<^sub>R y j" s, symmetric] by (auto simp:algebra_simps)
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)"
- by (auto simp:real_divide_def)
+ by (auto simp: divide_inverse)
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)"
using conv[of "y i" "(\<Sum> j \<in> s. ?a j *\<^sub>R y j)" "a i", OF yai(1) asum yai(2) ai1]
by (auto simp add:add_commute)
@@ -555,7 +554,7 @@
from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
from mult_right_mono_neg[OF this le(2)]
have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
- unfolding diff_def using real_add_mult_distrib by auto
+ by (simp add: algebra_simps)
hence "f' y * (x - y) - (f x - f y) \<le> 0" using le by auto
hence res: "f' y * (x - y) \<le> f x - f y" by auto
have "(f y - f x) / (y - x) - f' x = f' z1 - f' x"
@@ -570,7 +569,7 @@
from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
from mult_right_mono[OF this ge(2)]
have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"
- unfolding diff_def using real_add_mult_distrib by auto
+ by (simp add: algebra_simps)
hence "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto
hence "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
using res by auto } note less_imp = this
@@ -606,9 +605,9 @@
have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
by auto
hence f''0: "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
- unfolding inverse_eq_divide by (auto simp add:real_mult_assoc)
+ unfolding inverse_eq_divide by (auto simp add: mult_assoc)
have f''_ge0: "\<And> z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
- using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] real_mult_order)
+ using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] mult_pos_pos)
from f''_ge0_imp_convex[OF pos_is_convex,
unfolded greaterThan_iff, OF f' f''0 f''_ge0]
show ?thesis by auto
--- a/src/HOL/Library/Float.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Library/Float.thy Sun May 09 22:51:11 2010 -0700
@@ -508,7 +508,7 @@
have "real m < 2^(nat (-e))" using `Float m e < 1`
unfolding less_float_def real_of_float_neg_exp[OF `e < 0`] real_of_float_1
real_mult_less_iff1[of _ _ 1, OF `0 < 2^(nat (-e))`, symmetric]
- real_mult_assoc by auto
+ mult_assoc by auto
thus ?thesis unfolding real_of_int_less_iff[symmetric] by auto
qed
@@ -619,7 +619,7 @@
case True show ?thesis unfolding real_of_float_simp pow2_def using True by auto
next
case False hence P: "\<not> 0 \<le> - (bitlen m - 1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto
- show ?thesis unfolding real_of_float_nge0_exp[OF P] real_divide_def by auto
+ show ?thesis unfolding real_of_float_nge0_exp[OF P] divide_inverse by auto
qed
lemma bitlen_Pls: "bitlen (Int.Pls) = Int.Pls" by (subst Pls_def, subst Pls_def, simp)
@@ -683,7 +683,7 @@
have "real (x * 2^?l div y) * inverse (2^?l) \<le> (real (x * 2^?l) / real y) * inverse (2^?l)"
by (rule mult_right_mono, fact real_of_int_div4, simp)
also have "\<dots> \<le> (real x / real y) * 2^?l * inverse (2^?l)" by auto
- finally have "real (x * 2^?l div y) * inverse (2^?l) \<le> real x / real y" unfolding real_mult_assoc by auto
+ finally have "real (x * 2^?l div y) * inverse (2^?l) \<le> real x / real y" unfolding mult_assoc by auto
thus ?thesis unfolding lapprox_posrat_def Let_def normfloat real_of_float_simp
unfolding pow2_minus pow2_int minus_minus .
qed
@@ -700,7 +700,7 @@
unfolding real_of_int_mult[symmetric] real_of_int_le_iff zmult_commute by auto
hence "real (x div y) * real c * inverse (real c) \<le> real (x * c div y) * inverse (real c)"
using `0 < c` by auto
- thus ?thesis unfolding real_mult_assoc using `0 < c` by auto
+ thus ?thesis unfolding mult_assoc using `0 < c` by auto
qed
lemma lapprox_posrat_bottom: assumes "0 < y"
@@ -757,7 +757,7 @@
by (rule divide_right_mono, simp only: `0 \<le> real y * 2^?l`)
also have "\<dots> = real y * real (?X div y + 1) / real y / 2^?l" by auto
also have "\<dots> = real (?X div y + 1) * inverse (2^?l)" unfolding nonzero_mult_divide_cancel_left[OF `real y \<noteq> 0`]
- unfolding real_divide_def ..
+ unfolding divide_inverse ..
finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
unfolding pow2_minus pow2_int minus_minus by auto
qed
@@ -856,7 +856,7 @@
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))"
unfolding real_of_int_le_iff[symmetric] by auto
hence "real y \<le> real x * (2^nat (int (n - 1) + bitlen y) / (2^nat (bitlen x - 1)))"
- unfolding real_mult_assoc real_divide_def by auto
+ unfolding mult_assoc divide_inverse by auto
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
finally have "y \<le> x * 2^?l" unfolding exp_eq unfolding real_of_int_le_iff[symmetric] by auto
thus ?thesis using zdiv_greater_zero[OF `0 < y`] by auto
@@ -1083,7 +1083,7 @@
hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d"
unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto }
- 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"]
+ 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"]
have "2^?e * inverse (2^?b) \<le> 2^?e * ?d" unfolding pow_split power_add by auto
finally have "1 \<le> 2^?e * ?d" .
@@ -1269,7 +1269,7 @@
also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] ..
finally show ?thesis by auto
qed
- 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
+ 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
qed
also have "\<dots> = real (x * y)" unfolding normfloat ..
finally show ?thesis .
@@ -1293,10 +1293,10 @@
have "real m = real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding zmod_zdiv_equality[symmetric] ..
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
- also have "\<dots> \<le> (real (m div 2^(nat ?l)) + 1) * 2^(nat ?l)" unfolding real_add_mult_distrib using mod_uneq by auto
+ also have "\<dots> \<le> (real (m div 2^(nat ?l)) + 1) * 2^(nat ?l)" unfolding left_distrib using mod_uneq by auto
finally show ?thesis unfolding pow2_int[symmetric] using True by auto
qed
- 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
+ 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
qed
finally show ?thesis .
qed
@@ -1329,7 +1329,7 @@
hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
have "real (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding real_of_float_simp by auto
also have "\<dots> \<le> real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 .
- also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
+ also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_number_of divide_inverse ..
also have "\<dots> = real (Float m e)" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
finally show ?thesis unfolding Float floor_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
next
@@ -1357,7 +1357,7 @@
case False
hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
have "real (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
- also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
+ also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_number_of divide_inverse ..
also have "\<dots> \<le> 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] .
also have "\<dots> = real (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding real_of_float_simp by auto
finally show ?thesis unfolding Float ceiling_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sun May 09 22:51:11 2010 -0700
@@ -355,7 +355,7 @@
from real_lbound_gt_zero[OF one0 em0]
obtain d where d: "d >0" "d < 1" "d < e / m" by blast
from d(1,3) m(1) have dm: "d*m > 0" "d*m < e"
- by (simp_all add: field_simps real_mult_order)
+ by (simp_all add: field_simps mult_pos_pos)
show ?case
proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
fix d w
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun May 09 22:51:11 2010 -0700
@@ -1589,7 +1589,7 @@
thus ?thesis unfolding setsum_delta[OF assms(1)] using uv(2) and `u v < 0` and uv(1) by auto qed
qed (insert setsum_nonneg_eq_0_iff[of _ u, OF fin(1)] uv(2-3), auto)
- hence *:"setsum u {x\<in>c. u x > 0} > 0" unfolding real_less_def apply(rule_tac conjI, rule_tac setsum_nonneg) by auto
+ hence *:"setsum u {x\<in>c. u x > 0} > 0" unfolding less_le apply(rule_tac conjI, rule_tac setsum_nonneg) by auto
moreover have "setsum u ({x \<in> c. 0 < u x} \<union> {x \<in> c. u x < 0}) = setsum u c"
"(\<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)"
using assms(1) apply(rule_tac[!] setsum_mono_zero_left) by auto
@@ -1943,7 +1943,7 @@
apply (drule_tac x="\<lambda>i. (x i, f (x i))" in spec)
apply simp
using assms[unfolded convex] apply simp
- apply(rule_tac j="\<Sum>i = 1..k. u i * f (fst (x i))" in real_le_trans)
+ apply(rule_tac y="\<Sum>i = 1..k. u i * f (fst (x i))" in order_trans)
defer apply(rule setsum_mono) apply(erule_tac x=i in allE) unfolding real_scaleR_def
apply(rule mult_left_mono)using assms[unfolded convex] by auto
@@ -2182,7 +2182,7 @@
have "f x \<le> 1 / (1 + t) * f w + (t / (1 + t)) * f y"
using assms(2)[unfolded convex_on_def,rule_format,of w y "1/(1+t)" "t / (1+t)",unfolded w]
using `0<t` `2<t` and `y\<in>s` `w\<in>s` by (auto simp add:field_simps)
- also have "\<dots> = (f w + t * f y) / (1 + t)" using `t>0` unfolding real_divide_def by (auto simp add:field_simps)
+ also have "\<dots> = (f w + t * f y) / (1 + t)" using `t>0` unfolding divide_inverse by (auto simp add:field_simps)
also have "\<dots> < e + f y" using `t>0` * `e>0` by(auto simp add:field_simps)
finally have "f x - f y < e" by auto }
ultimately show ?thesis by auto
@@ -2231,7 +2231,7 @@
apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof
fix z assume z:"z\<in>{x - ?d..x + ?d}"
have e:"e = setsum (\<lambda>i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1
- by (metis eq_divide_imp times_divide_eq_left real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute)
+ by (metis eq_divide_imp times_divide_eq_left real_dimindex_gt_0 real_eq_of_nat less_le mult_commute)
show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed
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
@@ -2411,7 +2411,7 @@
by(auto simp add: Cart_eq field_simps)
also have "\<dots> = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:norm_eqI simp add: algebra_simps)
also have "\<dots> < d" using as[unfolded dist_norm] and `e>0`
- by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute)
+ by(auto simp add:pos_divide_less_eq[OF `e>0`] mult_commute)
finally show "y \<in> s" apply(subst *) apply(rule assms(1)[unfolded convex_alt,rule_format])
apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) by auto
qed(rule mult_pos_pos, insert `e>0` `d>0`, auto) qed
@@ -2522,7 +2522,7 @@
show ?thesis apply(rule that[of ?a]) unfolding interior_std_simplex mem_Collect_eq proof(rule,rule)
fix i::'n show "0 < ?a $ i" unfolding ** using dimindex_ge_1 by(auto simp add: Suc_le_eq) next
have "setsum (op $ ?a) ?D = setsum (\<lambda>i. inverse (2 * real CARD('n))) ?D" by(rule setsum_cong2, rule **)
- also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat real_divide_def[THEN sym] by (auto simp add:field_simps)
+ also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat divide_inverse[THEN sym] by (auto simp add:field_simps)
finally show "setsum (op $ ?a) ?D < 1" by auto qed qed
end
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun May 09 22:51:11 2010 -0700
@@ -3677,7 +3677,7 @@
from Sup_finite_in[OF fS S0]
show ?thesis unfolding infnorm_def infnorm_set_image
by (metis Sup_finite_ge_iff finite finite_imageI UNIV_not_empty image_is_empty
- rangeI real_le_refl)
+ rangeI order_refl)
qed
lemma infnorm_mul_lemma: "infnorm(a *s x) <= \<bar>a\<bar> * infnorm x"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Sun May 09 22:51:11 2010 -0700
@@ -2195,7 +2195,7 @@
shows "norm(setsum (\<lambda>l. content l *\<^sub>R c) p) \<le> e * content({a..b})" (is "?l \<le> ?r")
apply(rule order_trans,rule setsum_norm) defer unfolding norm_scaleR setsum_left_distrib[THEN sym]
apply(rule order_trans[OF mult_left_mono],rule assms,rule setsum_abs_ge_zero)
- apply(subst real_mult_commute) apply(rule mult_left_mono)
+ apply(subst mult_commute) apply(rule mult_left_mono)
apply(rule order_trans[of _ "setsum content p"]) apply(rule eq_refl,rule setsum_cong2)
apply(subst abs_of_nonneg) unfolding additive_content_division[OF assms(1)]
proof- from order_trans[OF norm_ge_zero[of c] assms(2)] show "0 \<le> e" .
@@ -2210,7 +2210,7 @@
next case False show ?thesis
apply(rule order_trans,rule setsum_norm) defer unfolding split_def norm_scaleR
apply(rule order_trans[OF setsum_mono]) apply(rule mult_left_mono[OF _ abs_ge_zero, of _ e]) defer
- unfolding setsum_left_distrib[THEN sym] apply(subst real_mult_commute) apply(rule mult_left_mono)
+ unfolding setsum_left_distrib[THEN sym] apply(subst mult_commute) apply(rule mult_left_mono)
apply(rule order_trans[of _ "setsum (content \<circ> snd) p"]) apply(rule eq_refl,rule setsum_cong2)
apply(subst o_def, rule abs_of_nonneg)
proof- show "setsum (content \<circ> snd) p \<le> content {a..b}" apply(rule eq_refl)
@@ -2395,7 +2395,7 @@
using g(1)[OF x, of n] g(1)[OF x, of m] by auto
also have "\<dots> \<le> inverse (real M) + inverse (real M)" apply(rule add_mono)
apply(rule_tac[!] le_imp_inverse_le) using goal1 M by auto
- also have "\<dots> = 2 / real M" unfolding real_divide_def by auto
+ also have "\<dots> = 2 / real M" unfolding divide_inverse by auto
finally show "norm (g n x - g m x) \<le> 2 / real M"
using norm_triangle_le[of "g n x - f x" "f x - g m x" "2 / real M"]
by(auto simp add:algebra_simps simp add:norm_minus_commute)
@@ -2672,7 +2672,7 @@
also have "... \<le> setsum (\<lambda>i. e / 2 / 2 ^ i) {0..N+1}" apply(rule setsum_mono)
proof- case goal1 thus ?case apply(subst mult_commute, subst pos_le_divide_eq[THEN sym])
using d(2)[rule_format,of "q i" i] using q[rule_format] by(auto simp add:field_simps)
- qed also have "... < e * inverse 2 * 2" unfolding real_divide_def setsum_right_distrib[THEN sym]
+ qed also have "... < e * inverse 2 * 2" unfolding divide_inverse setsum_right_distrib[THEN sym]
apply(rule mult_strict_left_mono) unfolding power_inverse atLeastLessThanSuc_atLeastAtMost[THEN sym]
apply(subst sumr_geometric) using goal1 by auto
finally show "?goal" by auto qed qed qed
@@ -3261,7 +3261,7 @@
using as by(auto simp add:field_simps)
next assume as:"0 > m i" hence *:"max (m i * a $ i) (m i * b $ i) = m i * a $ i"
"min (m i * a $ i) (m i * b $ i) = m i * b $ i" using ab as unfolding min_def max_def
- by(auto simp add:field_simps mult_le_cancel_left_neg intro:real_le_antisym)
+ by(auto simp add:field_simps mult_le_cancel_left_neg intro: order_antisym)
show ?thesis unfolding * apply rule defer apply(rule_tac x="1 / m i * x$i" in exI)
using as by(auto simp add:field_simps) qed qed qed qed qed
@@ -3567,7 +3567,7 @@
hence "c$1 - t$1 < e / 3 / norm (f c)" by auto
hence "norm (c - t) < e / 3 / norm (f c)" using as unfolding norm_vector_1 vector_less_def by auto
thus "norm (f c) * norm (c - t) < e / 3" using False apply-
- apply(subst real_mult_commute) apply(subst pos_less_divide_eq[THEN sym]) by auto
+ apply(subst mult_commute) apply(subst pos_less_divide_eq[THEN sym]) by auto
qed next case True show ?thesis apply(rule_tac x=1 in exI) unfolding True using `e>0` by auto
qed then guess w .. note w = conjunctD2[OF this,rule_format]
@@ -4408,8 +4408,8 @@
next case goal1 have *:"k * real (card r) / (1 + real (card r)) < k" using k by(auto simp add:field_simps)
show ?case apply(rule le_less_trans[of _ "setsum (\<lambda>x. k / (real (card r) + 1)) r"])
unfolding setsum_subtractf[THEN sym] apply(rule setsum_norm_le,fact)
- apply rule apply(drule qq) defer unfolding real_divide_def setsum_left_distrib[THEN sym]
- unfolding real_divide_def[THEN sym] using * by(auto simp add:field_simps real_eq_of_nat)
+ apply rule apply(drule qq) defer unfolding divide_inverse setsum_left_distrib[THEN sym]
+ unfolding divide_inverse[THEN sym] using * by(auto simp add:field_simps real_eq_of_nat)
qed finally show "?x \<le> e + k" . qed
lemma henstock_lemma_part2: fixes f::"real^'m \<Rightarrow> real^'n"
@@ -4525,7 +4525,7 @@
apply(rule le_less_trans[of _ "setsum (\<lambda>i. e / 2^(i+2)) {0..s}"])
apply(rule setsum_norm_le[OF finite_atLeastAtMost])
proof show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2"
- unfolding power_add real_divide_def inverse_mult_distrib
+ unfolding power_add divide_inverse inverse_mult_distrib
unfolding setsum_right_distrib[THEN sym] setsum_left_distrib[THEN sym]
unfolding power_inverse sum_gp apply(rule mult_strict_left_mono[OF _ e])
unfolding power2_eq_square by auto
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun May 09 22:51:11 2010 -0700
@@ -1777,7 +1777,7 @@
by (auto simp add: norm_minus_commute)
also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
- unfolding real_add_mult_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
+ unfolding left_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
also have "\<dots> \<le> e - d/2" using `d \<le> dist x y` and `d>0` and `?rhs` by(auto simp add: dist_norm)
finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using `d>0` by auto
@@ -2104,10 +2104,10 @@
{ fix x assume "x\<in>S"
hence "norm x \<le> b" using b by auto
hence "norm (f x) \<le> B * b" using B(2) apply(erule_tac x=x in allE)
- by (metis B(1) B(2) real_le_trans real_mult_le_cancel_iff2)
+ by (metis B(1) B(2) order_trans mult_le_cancel_left_pos)
}
thus ?thesis unfolding bounded_pos apply(rule_tac x="b*B" in exI)
- using b B real_mult_order[of b B] by (auto simp add: real_mult_commute)
+ using b B mult_pos_pos [of b B] by (auto simp add: mult_commute)
qed
lemma bounded_scaling:
@@ -3061,7 +3061,7 @@
{ fix e::real assume "e>0"
hence "dist a b < e" using assms(4 )using b using a by blast
}
- hence "dist a b = 0" by (metis dist_eq_0_iff dist_nz real_less_def)
+ hence "dist a b = 0" by (metis dist_eq_0_iff dist_nz less_le)
}
with a have "\<Inter>(range s) = {a}" unfolding image_def by auto
thus ?thesis ..
@@ -3841,7 +3841,7 @@
proof-
{ fix x assume "x \<in> s"
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
- have "e * abs c > 0" using assms(1)[unfolded zero_less_abs_iff[THEN sym]] using real_mult_order[OF `e>0`] by auto
+ have "e * abs c > 0" using assms(1)[unfolded zero_less_abs_iff[THEN sym]] using mult_pos_pos[OF `e>0`] by auto
moreover
{ fix y assume "dist y (c *\<^sub>R x) < e * \<bar>c\<bar>"
hence "norm ((1 / c) *\<^sub>R y - x) < e" unfolding dist_norm
@@ -5015,7 +5015,7 @@
lemma is_interval_interval: "is_interval {a .. b::real^'n}" (is ?th1) "is_interval {a<..<b}" (is ?th2) proof -
have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
show ?th1 ?th2 unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
- by(meson real_le_trans le_less_trans less_le_trans *)+ qed
+ by(meson order_trans le_less_trans less_le_trans *)+ qed
lemma is_interval_empty:
"is_interval {}"
@@ -5423,7 +5423,7 @@
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
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"]]
unfolding f.scaleR and ba using `x\<noteq>0` `a\<noteq>0`
- by (auto simp add: real_mult_commute pos_le_divide_eq pos_divide_le_eq)
+ by (auto simp add: mult_commute pos_le_divide_eq pos_divide_le_eq)
qed }
ultimately
show ?thesis by auto
@@ -5647,14 +5647,14 @@
unfolding image_iff Bex_def mem_interval vector_le_def
apply(auto simp add: vector_smult_assoc pth_3[symmetric]
intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
- by(auto simp add: pos_le_divide_eq pos_divide_le_eq real_mult_commute diff_le_iff)
+ by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
} moreover
{ fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval vector_le_def
apply(auto simp add: vector_smult_assoc pth_3[symmetric]
intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
- by(auto simp add: neg_le_divide_eq neg_divide_le_eq real_mult_commute diff_le_iff)
+ by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
}
ultimately show ?thesis using False by auto
qed
@@ -5723,7 +5723,7 @@
thus ?thesis using `e>0` by auto
next
case False hence "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]
- by (metis False d_def real_less_def)
+ by (metis False d_def less_le)
hence "0 < e * (1 - c) / d" using `e>0` and `1-c>0`
using divide_pos_pos[of "e * (1 - c)" d] and mult_pos_pos[of e "1 - c"] by auto
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
@@ -5731,18 +5731,18 @@
have *:"c ^ n \<le> c ^ N" using `n\<ge>N` and c using power_decreasing[OF `n\<ge>N`, of c] by auto
have "1 - c ^ (m - n) > 0" using c and power_strict_mono[of c 1 "m - n"] using `m>n` by auto
hence **:"d * (1 - c ^ (m - n)) / (1 - c) > 0"
- using real_mult_order[OF `d>0`, of "1 - c ^ (m - n)"]
+ using mult_pos_pos[OF `d>0`, of "1 - c ^ (m - n)"]
using divide_pos_pos[of "d * (1 - c ^ (m - n))" "1 - c"]
using `0 < 1 - c` by auto
have "dist (z m) (z n) \<le> c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
using cf_z2[of n "m - n"] and `m>n` unfolding pos_le_divide_eq[OF `1-c>0`]
- by (auto simp add: real_mult_commute dist_commute)
+ by (auto simp add: mult_commute dist_commute)
also have "\<dots> \<le> c ^ N * d * (1 - c ^ (m - n)) / (1 - c)"
using mult_right_mono[OF * order_less_imp_le[OF **]]
- unfolding real_mult_assoc by auto
+ unfolding mult_assoc by auto
also have "\<dots> < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)"
- using mult_strict_right_mono[OF N **] unfolding real_mult_assoc by auto
+ using mult_strict_right_mono[OF N **] unfolding mult_assoc by auto
also have "\<dots> = e * (1 - c ^ (m - n))" using c and `d>0` and `1 - c > 0` by auto
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
finally have "dist (z m) (z n) < e" by auto
@@ -5770,7 +5770,7 @@
have *:"c * dist (z N) x \<le> dist (z N) x" unfolding mult_le_cancel_right2
using zero_le_dist[of "z N" x] and c
- by (metis dist_eq_0_iff dist_nz order_less_asym real_less_def)
+ by (metis dist_eq_0_iff dist_nz order_less_asym less_le)
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]]
using z_in_s[of N] `x\<in>s` using c by auto
also have "\<dots> < e / 2" using N' and c using * by auto
--- a/src/HOL/Probability/Borel.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Probability/Borel.thy Sun May 09 22:51:11 2010 -0700
@@ -68,9 +68,9 @@
with w have "real(Suc(natceiling(inverse(g w - f w)))) > inverse(g w - f w)"
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)))))
< inverse(inverse(g w - f w))"
- 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)
+ 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)
hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < g w - f w"
- by (metis inverse_inverse_eq order_less_le_trans real_le_refl)
+ by (metis inverse_inverse_eq order_less_le_trans order_refl)
thus "\<exists>n. f w \<le> g w - inverse(real(Suc n))" using w
by (rule_tac x="natceiling(inverse(g w - f w))" in exI, auto)
next
@@ -357,7 +357,7 @@
borel_measurable_uminus_borel_measurable f g)
finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
show ?thesis
- apply (simp add: times_eq_sum_squares real_diff_def)
+ apply (simp add: times_eq_sum_squares diff_def)
using 1 2 apply (simp add: borel_measurable_add_borel_measurable)
done
qed
@@ -366,7 +366,7 @@
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
-unfolding real_diff_def
+unfolding diff_def
by (fast intro: borel_measurable_add_borel_measurable
borel_measurable_uminus_borel_measurable f g)
@@ -397,7 +397,7 @@
{ fix w
from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
- linorder_not_le real_le_refl real_le_trans real_less_def
+ linorder_not_le order_refl order_trans less_le
xt1(7) zero_less_divide_1_iff) }
hence "{w \<in> space M. a \<le> inverse (f w)} =
{w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
@@ -418,7 +418,7 @@
apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9)
zero_le_divide_1_iff)
apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg
- linorder_not_le real_le_refl real_le_trans)
+ linorder_not_le order_refl order_trans)
done }
hence "{w \<in> space M. a \<le> inverse (f w)} =
{w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto
@@ -627,11 +627,11 @@
proof -
from assms have "y - z > 0" by simp
hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
- unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def
+ unfolding incseq_def LIMSEQ_def dist_real_def diff_def
by simp
have "\<forall>m. x m \<le> y" using incseq_le assms by auto
hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
- by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def)
+ by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le diff_def)
from A B show ?thesis by auto
qed
--- a/src/HOL/Probability/Lebesgue.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Probability/Lebesgue.thy Sun May 09 22:51:11 2010 -0700
@@ -28,17 +28,17 @@
lemma pos_neg_part_abs:
fixes f :: "'a \<Rightarrow> real"
shows "pos_part f x + neg_part f x = \<bar>f x\<bar>"
-unfolding real_abs_def pos_part_def neg_part_def by auto
+unfolding abs_if pos_part_def neg_part_def by auto
lemma pos_part_abs:
fixes f :: "'a \<Rightarrow> real"
shows "pos_part (\<lambda> x. \<bar>f x\<bar>) y = \<bar>f y\<bar>"
-unfolding pos_part_def real_abs_def by auto
+unfolding pos_part_def abs_if by auto
lemma neg_part_abs:
fixes f :: "'a \<Rightarrow> real"
shows "neg_part (\<lambda> x. \<bar>f x\<bar>) y = 0"
-unfolding neg_part_def real_abs_def by auto
+unfolding neg_part_def abs_if by auto
lemma (in measure_space)
assumes "f \<in> borel_measurable M"
@@ -341,7 +341,8 @@
have "pos_simple_integral (k, c, (\<lambda> x. z x + z' x))
= (\<Sum> x \<in> k. (z x + z' x) * measure M (c x))"
unfolding pos_simple_integral_def by auto
- 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
+ also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x) + z' x * measure M (c x))"
+ by (simp add: left_distrib)
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
also have "\<dots> = pos_simple_integral (k, c, z) + pos_simple_integral (k, c, z')" unfolding pos_simple_integral_def by auto
finally have ths: "pos_simple_integral (s, a, x) + pos_simple_integral (s', b, y) =
@@ -436,12 +437,12 @@
lemma pos_simple_fn_integral_unique:
assumes "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple f"
shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
-using assms real_le_antisym real_le_refl pos_simple_integral_mono by metis
+using assms by (rule pos_simple_integral_equal) (* FIXME: redundant lemma *)
lemma psfis_unique:
assumes "a \<in> psfis f" "b \<in> psfis f"
shows "a = b"
-using assms real_le_antisym real_le_refl psfis_mono by metis
+using assms by (intro order_antisym psfis_mono [OF _ _ order_refl])
lemma pos_simple_integral_indicator:
assumes "A \<in> sets M"
@@ -557,7 +558,7 @@
using borel_measurable_indicator using sa'x[unfolded pos_simple_def] by auto
hence "(\<lambda> w. x i * indicator_fn (a' i) w) \<in> borel_measurable M"
using affine_borel_measurable[of "\<lambda> w. indicator_fn (a' i) w" 0 "x i"]
- real_mult_commute by auto }
+ by (simp add: mult_commute) }
from borel_measurable_setsum_borel_measurable[OF fs this] affine_borel_measurable
have "(\<lambda> w. (\<Sum> i \<in> s. x i * indicator_fn (a' i) w)) \<in> borel_measurable M" by auto
from borel_measurable_cong[OF pos_simple_setsum_indicator_fn[OF sa'x]] this
@@ -743,7 +744,7 @@
assumes a: "a \<in> nnfis f" and b: "b \<in> nnfis f"
shows "a = b"
using nnfis_mono[OF a b] nnfis_mono[OF b a]
- by (auto intro!: real_le_antisym[of a b])
+ by (auto intro!: order_antisym[of a b])
lemma psfis_equiv:
assumes "a \<in> psfis f" and "nonneg g"
@@ -843,7 +844,7 @@
from nnfis this mono_convergent_le[OF mc]
show "x n \<le> l" by (rule nnfis_mono)
qed
- ultimately have "l = z" by (rule real_le_antisym)
+ ultimately have "l = z" by (rule order_antisym)
thus "c ----> z" using `c ----> l` by simp
qed
qed
@@ -859,7 +860,7 @@
by auto
thus "0 \<le> f x" using uy[rule_format]
unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
- using incseq_le[of "\<lambda> n. u n x" "f x"] real_le_trans
+ using incseq_le[of "\<lambda> n. u n x" "f x"] order_trans
by fast
qed
@@ -1335,10 +1336,10 @@
also have "\<dots> \<le> integral (\<lambda> t. \<bar> f t \<bar> ^ n)"
apply (rule integral_mono)
using integral_cmul_indicator[OF w]
- `integrable (\<lambda> x. \<bar>f x\<bar> ^ n)` real_le_trans[OF v1 v2] by auto
+ `integrable (\<lambda> x. \<bar>f x\<bar> ^ n)` order_trans[OF v1 v2] by auto
finally show "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
unfolding atLeast_def
- by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
+ by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: mult_commute)
qed
lemma (in measure_space) integral_0:
--- a/src/HOL/ex/Sqrt_Script.thy Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/ex/Sqrt_Script.thy Sun May 09 22:51:11 2010 -0700
@@ -61,7 +61,7 @@
apply (rule notI)
apply (erule Rats_abs_nat_div_natE)
apply (simp del: real_of_nat_mult
- add: real_abs_def divide_eq_eq prime_not_square real_of_nat_mult [symmetric])
+ add: abs_if divide_eq_eq prime_not_square real_of_nat_mult [symmetric])
done
lemmas two_sqrt_irrational =