--- a/src/HOL/Complex.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Complex.thy Mon May 10 09:54:41 2010 +0200
@@ -676,12 +676,12 @@
by (simp add: divide_inverse rcis_def)
lemma cis_divide: "cis a / cis b = cis (a - b)"
-by (simp add: complex_divide_def cis_mult real_diff_def)
+by (simp add: complex_divide_def cis_mult diff_def)
lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
apply (simp add: complex_divide_def)
apply (case_tac "r2=0", simp)
-apply (simp add: rcis_inverse rcis_mult real_diff_def)
+apply (simp add: rcis_inverse rcis_mult diff_def)
done
lemma Re_cis [simp]: "Re(cis a) = cos a"
--- a/src/HOL/Decision_Procs/Approximation.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon May 10 09:54:41 2010 +0200
@@ -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 22:06:24 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Mon May 10 09:54:41 2010 +0200
@@ -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/Deriv.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Deriv.thy Mon May 10 09:54:41 2010 +0200
@@ -482,8 +482,7 @@
shows "\<lbrakk>\<forall>n. f n \<le> f (Suc n); convergent f\<rbrakk> \<Longrightarrow> f n \<le> lim f"
apply (rule linorder_not_less [THEN iffD1])
apply (auto simp add: convergent_LIMSEQ_iff LIMSEQ_iff monoseq_Suc)
-apply (drule real_less_sum_gt_zero)
-apply (drule_tac x = "f n + - lim f" in spec, safe)
+apply (drule_tac x = "f n - lim f" in spec, clarsimp)
apply (drule_tac P = "%na. no\<le>na --> ?Q na" and x = "no + n" in spec, auto)
apply (subgoal_tac "lim f \<le> f (no + n) ")
apply (drule_tac no=no and m=n in lemma_f_mono_add)
@@ -706,7 +705,7 @@
apply safe
apply simp_all
apply (rename_tac x xa ya M Ma)
-apply (metis linorder_not_less order_le_less real_le_trans)
+apply (metis linorder_not_less order_le_less order_trans)
apply (case_tac "a \<le> x & x \<le> b")
prefer 2
apply (rule_tac x = 1 in exI, force)
@@ -1235,16 +1234,16 @@
using assms
apply auto
apply (metis DERIV_isCont)
- apply (metis differentiableI real_less_def)
+ apply (metis differentiableI less_le)
done
then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
and "f b - f a = (b - a) * l"
by auto
from prems have "~(l > 0)"
- by (metis linorder_not_le mult_le_0_iff real_le_eq_diff)
+ by (metis linorder_not_le mult_le_0_iff diff_le_0_iff_le)
with prems show False
- by (metis DERIV_unique real_less_def)
+ by (metis DERIV_unique less_le)
qed
lemma DERIV_nonneg_imp_nonincreasing:
@@ -1264,13 +1263,13 @@
apply (rule MVT)
apply auto
apply (metis DERIV_isCont)
- apply (metis differentiableI real_less_def)
+ apply (metis differentiableI less_le)
done
then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
and "f b - f a = (b - a) * l"
by auto
from prems have "~(l >= 0)"
- by (metis diff_self le_eqI le_iff_diff_le_0 real_le_antisym real_le_linear
+ by (metis diff_self le_eqI le_iff_diff_le_0 order_antisym linear
split_mult_pos_le)
with prems show False
by (metis DERIV_unique order_less_imp_le)
--- a/src/HOL/Fields.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Fields.thy Mon May 10 09:54:41 2010 +0200
@@ -397,6 +397,14 @@
"a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
+lemma one_less_inverse:
+ "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> 1 < inverse a"
+ using less_imp_inverse_less [of a 1, unfolded inverse_1] .
+
+lemma one_le_inverse:
+ "0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a"
+ using le_imp_inverse_le [of a 1, unfolded inverse_1] .
+
lemma pos_le_divide_eq [field_simps]: "0 < c ==> (a \<le> b/c) = (a*c \<le> b)"
proof -
assume less: "0<c"
--- a/src/HOL/Hahn_Banach/Function_Norm.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy Mon May 10 09:54:41 2010 +0200
@@ -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 22:06:24 2010 +0200
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy Mon May 10 09:54:41 2010 +0200
@@ -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/Import/HOL/real.imp Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Import/HOL/real.imp Mon May 10 09:54:41 2010 +0200
@@ -247,7 +247,7 @@
"REAL_INV_POS" > "Rings.positive_imp_inverse_positive"
"REAL_INV_NZ" > "Rings.nonzero_imp_inverse_nonzero"
"REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL"
- "REAL_INV_LT1" > "RealDef.real_inverse_gt_one"
+ "REAL_INV_LT1" > "Fields.one_less_inverse"
"REAL_INV_INV" > "Rings.inverse_inverse_eq"
"REAL_INV_EQ_0" > "Rings.inverse_nonzero_iff_nonzero"
"REAL_INV_1OVER" > "Rings.inverse_eq_divide"
--- a/src/HOL/Library/Convex.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Library/Convex.thy Mon May 10 09:54:41 2010 +0200
@@ -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 22:06:24 2010 +0200
+++ b/src/HOL/Library/Float.thy Mon May 10 09:54:41 2010 +0200
@@ -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 22:06:24 2010 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon May 10 09:54:41 2010 +0200
@@ -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/Ln.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Ln.thy Mon May 10 09:54:41 2010 +0200
@@ -206,7 +206,7 @@
apply auto
done
also have "... = exp (-x)"
- by (auto simp add: exp_minus real_divide_def)
+ by (auto simp add: exp_minus divide_inverse)
finally have "1 - x <= exp (- x)" .
also have "1 - x = exp (ln (1 - x))"
proof -
--- a/src/HOL/Log.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Log.thy Mon May 10 09:54:41 2010 +0200
@@ -64,7 +64,7 @@
by (simp add: powr_def)
lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
-by (simp add: powr_powr real_mult_commute)
+by (simp add: powr_powr mult_commute)
lemma powr_minus: "x powr (-a) = inverse (x powr a)"
by (simp add: powr_def exp_minus [symmetric])
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon May 10 09:54:41 2010 +0200
@@ -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 22:06:24 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon May 10 09:54:41 2010 +0200
@@ -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 22:06:24 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon May 10 09:54:41 2010 +0200
@@ -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 22:06:24 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon May 10 09:54:41 2010 +0200
@@ -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/NSA/NSA.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/NSA/NSA.thy Mon May 10 09:54:41 2010 +0200
@@ -2188,7 +2188,7 @@
apply (subst pos_less_divide_eq, assumption)
apply (subst pos_less_divide_eq)
apply (simp add: real_of_nat_Suc_gt_zero)
-apply (simp add: real_mult_commute)
+apply (simp add: mult_commute)
done
lemma finite_inverse_real_of_posnat_gt_real:
--- a/src/HOL/Probability/Borel.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Probability/Borel.thy Mon May 10 09:54:41 2010 +0200
@@ -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 22:06:24 2010 +0200
+++ b/src/HOL/Probability/Lebesgue.thy Mon May 10 09:54:41 2010 +0200
@@ -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/RealDef.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/RealDef.thy Mon May 10 09:54:41 2010 +0200
@@ -506,26 +506,24 @@
subsection{*More Lemmas*}
+text {* BH: These lemmas should not be necessary; they should be
+covered by existing simp rules and simplification procedures. *}
+
lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
-by auto
+by simp (* redundant with mult_cancel_left *)
lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
-by auto
+by simp (* redundant with mult_cancel_right *)
lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
- by (force elim: order_less_asym
- simp add: mult_less_cancel_right)
+by simp (* solved by linordered_ring_less_cancel_factor simproc *)
lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
-apply (simp add: mult_le_cancel_right)
-apply (blast intro: elim: order_less_asym)
-done
+by simp (* solved by linordered_ring_le_cancel_factor simproc *)
lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
-by(simp add:mult_commute)
-
-lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
-by (simp add: one_less_inverse_iff) (* TODO: generalize/move *)
+by (rule mult_le_cancel_left_pos)
+(* BH: Why doesn't "simp" prove this one, like it does the last one? *)
subsection {* Embedding numbers into the Reals *}
@@ -773,10 +771,6 @@
lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
by (simp add: add: real_of_nat_def)
-(* FIXME: duplicates real_of_nat_ge_zero *)
-lemma real_of_nat_ge_zero_cancel_iff: "(0 \<le> real (n::nat))"
-by (simp add: add: real_of_nat_def)
-
lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"
apply (subgoal_tac "real n + 1 = real (Suc n)")
apply simp
@@ -1013,12 +1007,6 @@
by auto
-(*
-FIXME: we should have this, as for type int, but many proofs would break.
-It replaces x+-y by x-y.
-declare real_diff_def [symmetric, simp]
-*)
-
subsubsection{*Density of the Reals*}
lemma real_lbound_gt_zero:
--- a/src/HOL/RealPow.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/RealPow.thy Mon May 10 09:54:41 2010 +0200
@@ -95,7 +95,7 @@
by (intro add_nonneg_nonneg zero_le_power2)
lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
-by (rule_tac j = 0 in real_le_trans, auto)
+by (rule_tac y = 0 in order_trans, auto)
lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
by (auto simp add: power2_eq_square)
@@ -145,7 +145,7 @@
"[|(0::real) < x; 0 < x1; x1 * y < x * u |]
==> inverse x * y < inverse x1 * u"
apply (rule_tac c=x in mult_less_imp_less_left)
-apply (auto simp add: real_mult_assoc [symmetric])
+apply (auto simp add: mult_assoc [symmetric])
apply (simp (no_asm) add: mult_ac)
apply (rule_tac c=x1 in mult_less_imp_less_right)
apply (auto simp add: mult_ac)
--- a/src/HOL/Relation.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Relation.thy Mon May 10 09:54:41 2010 +0200
@@ -181,6 +181,12 @@
lemma rel_comp_distrib2[simp]: "(S \<union> T) O R = (S O R) \<union> (T O R)"
by auto
+lemma rel_comp_UNION_distrib: "s O UNION I r = UNION I (%i. s O r i)"
+by auto
+
+lemma rel_comp_UNION_distrib2: "UNION I r O s = UNION I (%i. r i O s)"
+by auto
+
subsection {* Reflexivity *}
--- a/src/HOL/SEQ.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/SEQ.thy Mon May 10 09:54:41 2010 +0200
@@ -1289,7 +1289,7 @@
hence x0: "0 < x" by simp
assume x1: "x < 1"
from x0 x1 have "1 < inverse x"
- by (rule real_inverse_gt_one)
+ by (rule one_less_inverse)
hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
by (rule LIMSEQ_inverse_realpow_zero)
thus ?thesis by (simp add: power_inverse)
--- a/src/HOL/SupInf.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/SupInf.thy Mon May 10 09:54:41 2010 +0200
@@ -74,7 +74,7 @@
lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
fixes x :: real
shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
- by (metis Sup_upper real_le_trans)
+ by (metis Sup_upper order_trans)
lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
fixes z :: real
@@ -86,7 +86,7 @@
shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a)
\<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
- insert_not_empty real_le_antisym)
+ insert_not_empty order_antisym)
lemma Sup_le:
fixes S :: "real set"
@@ -109,28 +109,28 @@
apply (simp add: max_def)
apply (rule Sup_eq_maximum)
apply (rule insertI1)
- apply (metis Sup_upper [OF _ z] insertE real_le_linear real_le_trans)
+ apply (metis Sup_upper [OF _ z] insertE linear order_trans)
done
next
case False
hence 1:"a < Sup X" by simp
have "Sup X \<le> Sup (insert a X)"
apply (rule Sup_least)
- apply (metis empty_psubset_nonempty psubset_eq x)
+ apply (metis ex_in_conv x)
apply (rule Sup_upper_EX)
apply blast
- apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
+ apply (metis insert_iff linear order_refl order_trans z)
done
moreover
have "Sup (insert a X) \<le> Sup X"
apply (rule Sup_least)
apply blast
- apply (metis False Sup_upper insertE real_le_linear z)
+ apply (metis False Sup_upper insertE linear z)
done
ultimately have "Sup (insert a X) = Sup X"
by (blast intro: antisym )
thus ?thesis
- by (metis 1 min_max.le_iff_sup real_less_def)
+ by (metis 1 min_max.le_iff_sup less_le)
qed
lemma Sup_insert_if:
@@ -177,7 +177,7 @@
fixes S :: "real set"
assumes fS: "finite S" and Se: "S \<noteq> {}"
shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
-by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS real_le_trans)
+by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS order_trans)
lemma Sup_finite_gt_iff:
fixes S :: "real set"
@@ -291,19 +291,19 @@
lemma Inf_lower2:
fixes x :: real
shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
- by (metis Inf_lower real_le_trans)
+ by (metis Inf_lower order_trans)
lemma Inf_real_iff:
fixes z :: real
shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
- by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear
+ by (metis Inf_greatest Inf_lower less_le_not_le linear
order_less_le_trans)
lemma Inf_eq:
fixes a :: real
shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a"
by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
- insert_absorb insert_not_empty real_le_antisym)
+ insert_absorb insert_not_empty order_antisym)
lemma Inf_ge:
fixes S :: "real set"
@@ -324,27 +324,27 @@
case True
thus ?thesis
by (simp add: min_def)
- (blast intro: Inf_eq_minimum real_le_refl real_le_trans z)
+ (blast intro: Inf_eq_minimum order_trans z)
next
case False
hence 1:"Inf X < a" by simp
have "Inf (insert a X) \<le> Inf X"
apply (rule Inf_greatest)
- apply (metis empty_psubset_nonempty psubset_eq x)
+ apply (metis ex_in_conv x)
apply (rule Inf_lower_EX)
apply (erule insertI2)
- apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
+ apply (metis insert_iff linear order_refl order_trans z)
done
moreover
have "Inf X \<le> Inf (insert a X)"
apply (rule Inf_greatest)
apply blast
- apply (metis False Inf_lower insertE real_le_linear z)
+ apply (metis False Inf_lower insertE linear z)
done
ultimately have "Inf (insert a X) = Inf X"
by (blast intro: antisym )
thus ?thesis
- by (metis False min_max.inf_absorb2 real_le_linear)
+ by (metis False min_max.inf_absorb2 linear)
qed
lemma Inf_insert_if:
@@ -377,13 +377,13 @@
lemma Inf_finite_ge_iff:
fixes S :: "real set"
shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
-by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans)
+by (metis Inf_finite_Min Inf_finite_in Min_le order_trans)
lemma Inf_finite_le_iff:
fixes S :: "real set"
shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
- real_le_antisym real_le_linear)
+ order_antisym linear)
lemma Inf_finite_gt_iff:
fixes S :: "real set"
@@ -417,7 +417,7 @@
also have "... \<le> e"
apply (rule Sup_asclose)
apply (auto simp add: S)
- apply (metis abs_minus_add_cancel b add_commute real_diff_def)
+ apply (metis abs_minus_add_cancel b add_commute diff_def)
done
finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
thus ?thesis
@@ -474,13 +474,13 @@
proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
by (rule SupInf.Sup_upper [where z=b], auto)
- (metis `a < b` `\<not> P b` real_le_linear real_less_def)
+ (metis `a < b` `\<not> P b` linear less_le)
next
show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
apply (rule SupInf.Sup_least)
apply (auto simp add: )
apply (metis less_le_not_le)
- apply (metis `a<b` `~ P b` real_le_linear real_less_def)
+ apply (metis `a<b` `~ P b` linear less_le)
done
next
fix x
@@ -495,7 +495,7 @@
assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
by (rule_tac z="b" in SupInf.Sup_upper, auto)
- (metis `a<b` `~ P b` real_le_linear real_less_def)
+ (metis `a<b` `~ P b` linear less_le)
qed
end
--- a/src/HOL/Tools/Function/mutual.ML Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Mon May 10 09:54:41 2010 +0200
@@ -192,7 +192,7 @@
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
(fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
- THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
+ THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *)
|> restore_cond
|> export
end
--- a/src/HOL/Tools/Function/sum_tree.ML Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Tools/Function/sum_tree.ML Mon May 10 09:54:41 2010 +0200
@@ -8,7 +8,6 @@
struct
(* Theory dependencies *)
-val proj_in_rules = [@{thm Projl_Inl}, @{thm Projr_Inr}]
val sumcase_split_ss =
HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases})
--- a/src/HOL/Tools/semiring_normalizer.ML Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Mon May 10 09:54:41 2010 +0200
@@ -57,7 +57,7 @@
type T = (thm * entry) list;
val empty = [];
val extend = I;
- val merge = AList.merge Thm.eq_thm (K true);
+ fun merge data = AList.merge Thm.eq_thm (K true) data;
);
val get = Data.get o Context.Proof;
--- a/src/HOL/Transcendental.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/Transcendental.thy Mon May 10 09:54:41 2010 +0200
@@ -779,7 +779,7 @@
finally show "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>" unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF `0 < R'`]]] .
show "0 \<le> \<bar>f n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult[symmetric] by auto
qed
- also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult real_mult_assoc[symmetric] by algebra
+ also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult mult_assoc[symmetric] by algebra
finally show ?thesis .
qed }
{ fix n show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
@@ -792,7 +792,7 @@
show "\<bar>f n * x ^ n\<bar> \<le> norm (f n * real (Suc n) * x ^ n)" unfolding real_norm_def abs_mult
by (rule mult_right_mono, auto simp add: le[unfolded mult_1_right])
qed
- from this[THEN summable_mult2[where c=x], unfolded real_mult_assoc, unfolded real_mult_commute]
+ from this[THEN summable_mult2[where c=x], unfolded mult_assoc, unfolded mult_commute]
show "summable (?f x)" by auto }
show "summable (?f' x0)" using converges[OF `x0 \<in> {-R <..< R}`] .
show "x0 \<in> {-R' <..< R'}" using `x0 \<in> {-R' <..< R'}` .
@@ -1022,7 +1022,7 @@
lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) ==> (1 + x) \<le> exp(x)"
apply (drule order_le_imp_less_or_eq, auto)
apply (simp add: exp_def)
-apply (rule real_le_trans)
+apply (rule order_trans)
apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff)
done
@@ -1089,7 +1089,7 @@
apply (rule_tac x = 1 and y = y in linorder_cases)
apply (drule order_less_imp_le [THEN lemma_exp_total])
apply (rule_tac [2] x = 0 in exI)
-apply (frule_tac [3] real_inverse_gt_one)
+apply (frule_tac [3] one_less_inverse)
apply (drule_tac [4] order_less_imp_le [THEN lemma_exp_total], auto)
apply (rule_tac x = "-x" in exI)
apply (simp add: exp_minus)
@@ -1228,7 +1228,7 @@
have "1 / x = 1 / (1 - (1 - x))" by auto
also have "\<dots> = (\<Sum> n. (1 - x)^n)" using geometric_sums[OF `norm (1 - x) < 1`] by (rule sums_unique)
also have "\<dots> = suminf (?f' x)" unfolding power_mult_distrib[symmetric] by (rule arg_cong[where f=suminf], rule arg_cong[where f="op ^"], auto)
- finally have "DERIV ln x :> suminf (?f' x)" using DERIV_ln[OF `0 < x`] unfolding real_divide_def by auto
+ finally have "DERIV ln x :> suminf (?f' x)" using DERIV_ln[OF `0 < x`] unfolding divide_inverse by auto
moreover
have repos: "\<And> h x :: real. h - 1 + x = h + x - 1" by auto
have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> (\<Sum>n. (-1)^n * (1 / real (n + 1)) * real (Suc n) * (x - 1) ^ n)"
@@ -1388,7 +1388,7 @@
lemma DERIV_sin_realpow2 [simp]:
"DERIV (%x. (sin x)\<twosuperior>) x :> cos(x) * sin(x) + cos(x) * sin(x)"
-by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
+by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
lemma DERIV_sin_realpow2a [simp]:
"DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)"
@@ -1406,7 +1406,7 @@
lemma DERIV_cos_realpow2 [simp]:
"DERIV (%x. (cos x)\<twosuperior>) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
-by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
+by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
lemma DERIV_cos_realpow2a [simp]:
"DERIV (%x. (cos x)\<twosuperior>) x :> -2 * cos(x) * sin(x)"
@@ -1705,8 +1705,8 @@
apply (drule_tac f = cos in Rolle)
apply (drule_tac [5] f = cos in Rolle)
apply (auto dest!: DERIV_cos [THEN DERIV_unique] simp add: differentiable_def)
-apply (metis order_less_le_trans real_less_def sin_gt_zero)
-apply (metis order_less_le_trans real_less_def sin_gt_zero)
+apply (metis order_less_le_trans less_le sin_gt_zero)
+apply (metis order_less_le_trans less_le sin_gt_zero)
done
lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
@@ -2138,9 +2138,9 @@
apply (auto simp add: tan_def)
apply (rule inverse_less_iff_less [THEN iffD1])
apply (auto simp add: divide_inverse)
-apply (rule real_mult_order)
+apply (rule mult_pos_pos)
apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
-apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult_commute)
+apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult_commute)
done
lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
@@ -2193,7 +2193,7 @@
hence "0 < cos z" using cos_gt_zero_pi by auto
hence inv_pos: "0 < inverse ((cos z)\<twosuperior>)" by auto
have "0 < x - y" using `y < x` by auto
- from real_mult_order[OF this inv_pos]
+ from mult_pos_pos [OF this inv_pos]
have "0 < tan x - tan y" unfolding tan_diff by auto
thus ?thesis by auto
qed
@@ -2226,7 +2226,7 @@
lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x"
proof (induct n arbitrary: x)
case (Suc n)
- have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
+ have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" 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
@@ -2439,7 +2439,7 @@
apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
apply (erule (1) isCont_inverse_function2 [where f=tan])
apply (metis arctan_tan order_le_less_trans order_less_le_trans)
-apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans real_less_def)
+apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
done
lemma DERIV_arcsin:
@@ -2953,7 +2953,7 @@
}
hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
- unfolding real_diff_def divide_inverse
+ unfolding diff_def divide_inverse
by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum)
ultimately have "0 \<le> ?a 1 n - ?diff 1 n" by (rule LIM_less_bound)
hence "?diff 1 n \<le> ?a 1 n" by auto
@@ -2969,7 +2969,7 @@
have "norm (?diff 1 n - 0) < r" by auto }
thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
qed
- from this[unfolded LIMSEQ_rabs_zero real_diff_def add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
+ from this[unfolded LIMSEQ_rabs_zero diff_def add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
--- a/src/HOL/ex/Sqrt_Script.thy Sun May 09 22:06:24 2010 +0200
+++ b/src/HOL/ex/Sqrt_Script.thy Mon May 10 09:54:41 2010 +0200
@@ -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 =