--- a/src/HOL/Complex.thy Sun May 09 14:21:44 2010 -0700
+++ b/src/HOL/Complex.thy Sun May 09 17:47:43 2010 -0700
@@ -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/Deriv.thy Sun May 09 14:21:44 2010 -0700
+++ b/src/HOL/Deriv.thy Sun May 09 17:47:43 2010 -0700
@@ -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/Ln.thy Sun May 09 14:21:44 2010 -0700
+++ b/src/HOL/Ln.thy Sun May 09 17:47:43 2010 -0700
@@ -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 14:21:44 2010 -0700
+++ b/src/HOL/Log.thy Sun May 09 17:47:43 2010 -0700
@@ -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/RealPow.thy Sun May 09 14:21:44 2010 -0700
+++ b/src/HOL/RealPow.thy Sun May 09 17:47:43 2010 -0700
@@ -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/SupInf.thy Sun May 09 14:21:44 2010 -0700
+++ b/src/HOL/SupInf.thy Sun May 09 17:47:43 2010 -0700
@@ -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/Transcendental.thy Sun May 09 14:21:44 2010 -0700
+++ b/src/HOL/Transcendental.thy Sun May 09 17:47:43 2010 -0700
@@ -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
@@ -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)