--- a/src/HOL/Hyperreal/Deriv.thy Thu May 17 19:49:40 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy Thu May 17 21:51:32 2007 +0200
@@ -857,7 +857,7 @@
lemma lemma_interval_lt:
"[| a < x; x < b |]
==> \<exists>d::real. 0 < d & (\<forall>y. \<bar>x-y\<bar> < d --> a < y & y < b)"
-apply (simp add: abs_interval_iff)
+apply (simp add: abs_less_iff)
apply (insert linorder_linear [of "x-a" "b-x"], safe)
apply (rule_tac x = "x-a" in exI)
apply (rule_tac [2] x = "b-x" in exI, auto)
@@ -1130,7 +1130,7 @@
moreover
hence "g(f x') = g (f(x+d))" by simp
ultimately show False using d inj [of x'] inj [of "x+d"]
- by (simp add: abs_le_interval_iff)
+ by (simp add: abs_le_iff)
next
case ge
from d cont all [of "x-d"]
@@ -1143,7 +1143,7 @@
moreover
hence "g(f x') = g (f(x-d))" by simp
ultimately show False using d inj [of x'] inj [of "x-d"]
- by (simp add: abs_le_interval_iff)
+ by (simp add: abs_le_iff)
qed
qed
@@ -1171,7 +1171,7 @@
shows "\<exists>e>0. \<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y)"
proof -
have "x-d \<le> x+d" "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" using cont d
- by (auto simp add: abs_le_interval_iff)
+ by (auto simp add: abs_le_iff)
from isCont_Lb_Ub [OF this]
obtain L M
where all1 [rule_format]: "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> L \<le> f z \<and> f z \<le> M"
@@ -1206,7 +1206,7 @@
from all2 [OF this]
obtain z where "x - d \<le> z" "z \<le> x + d" "f z = y" by blast
thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y"
- by (force simp add: abs_le_interval_iff)
+ by (force simp add: abs_le_iff)
qed
qed
qed
@@ -1324,7 +1324,7 @@
have "?h b - ?h a =
((f b)*(g b) - (f a)*(g b) - (g b)*(f b) + (g a)*(f b)) -
((f b)*(g a) - (f a)*(g a) - (g b)*(f a) + (g a)*(f a))"
- by (simp add: mult_ac add_ac real_diff_mult_distrib)
+ by (simp add: mult_ac add_ac right_diff_distrib)
hence "?h b - ?h a = 0" by auto
}
ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto
--- a/src/HOL/Hyperreal/Integration.thy Thu May 17 19:49:40 2007 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Thu May 17 21:51:32 2007 +0200
@@ -343,13 +343,13 @@
lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
apply (auto simp add: order_le_less rsum_def Integral_def)
apply (rule_tac x = "%x. b - a" in exI)
-apply (auto simp add: gauge_def abs_interval_iff tpart_def partition)
+apply (auto simp add: gauge_def abs_less_iff tpart_def partition)
done
lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c) (c*(b - a))"
apply (auto simp add: order_le_less rsum_def Integral_def)
apply (rule_tac x = "%x. b - a" in exI)
-apply (auto simp add: setsum_right_distrib [symmetric] gauge_def abs_interval_iff
+apply (auto simp add: setsum_right_distrib [symmetric] gauge_def abs_less_iff
right_diff_distrib [symmetric] partition tpart_def)
done
@@ -358,7 +358,7 @@
apply (auto simp add: order_le_less
dest: Integral_unique [OF order_refl Integral_zero])
apply (auto simp add: rsum_def Integral_def setsum_right_distrib[symmetric] mult_assoc)
-apply (rule_tac a2 = c in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
+apply (rule_tac a2 = c in abs_ge_zero [THEN order_le_imp_less_or_eq, THEN disjE])
prefer 2 apply force
apply (drule_tac x = "e/abs c" in spec, auto)
apply (simp add: zero_less_mult_iff divide_inverse)
@@ -437,7 +437,7 @@
apply (drule_tac x = u in spec, auto)
apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
apply (rule order_trans)
-apply (auto simp add: abs_le_interval_iff)
+apply (auto simp add: abs_le_iff)
apply (simp add: right_diff_distrib)
done
--- a/src/HOL/Hyperreal/Ln.thy Thu May 17 19:49:40 2007 +0200
+++ b/src/HOL/Hyperreal/Ln.thy Thu May 17 21:51:32 2007 +0200
@@ -113,7 +113,7 @@
proof -
have "(%n. (1 / 2::real)^n) sums (1 / (1 - (1/2)))"
apply (rule geometric_sums)
- by (simp add: abs_interval_iff)
+ by (simp add: abs_less_iff)
also have "(1::real) / (1 - 1/2) = 2"
by simp
finally have "(%n. (1 / 2::real)^n) sums 2" .
--- a/src/HOL/Hyperreal/NSA.thy Thu May 17 19:49:40 2007 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Thu May 17 21:51:32 2007 +0200
@@ -2206,7 +2206,7 @@
lemma real_of_nat_inverse_eq_iff:
"(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)"
-by (auto simp add: real_of_nat_Suc_gt_zero real_not_refl2 [THEN not_sym])
+by (auto simp add: real_of_nat_Suc_gt_zero less_imp_neq [THEN not_sym])
lemma lemma_finite_omega_set2: "finite {n::nat. u = inverse(real(Suc n))}"
apply (simp (no_asm_simp) add: real_of_nat_inverse_eq_iff)
--- a/src/HOL/Hyperreal/SEQ.thy Thu May 17 19:49:40 2007 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Thu May 17 21:51:32 2007 +0200
@@ -725,7 +725,7 @@
lemma Bseq_isUb:
"!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
-by (auto intro: isUbI setleI simp add: Bseq_def abs_le_interval_iff)
+by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
text{* Use completeness of reals (supremum property)
--- a/src/HOL/Hyperreal/Series.thy Thu May 17 19:49:40 2007 +0200
+++ b/src/HOL/Hyperreal/Series.thy Thu May 17 21:51:32 2007 +0200
@@ -422,7 +422,7 @@
apply (rule_tac y = "\<Sum>k=m..<n. norm (f k)" in order_le_less_trans)
apply (rule norm_setsum)
apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans)
-apply (auto intro: setsum_mono simp add: abs_interval_iff)
+apply (auto intro: setsum_mono simp add: abs_less_iff)
done
lemma summable_norm_comparison_test:
@@ -456,7 +456,7 @@
shows "\<lbrakk>\<forall>n. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable f \<and> suminf f \<le> suminf g"
apply (subgoal_tac "summable f")
apply (auto intro!: summable_le)
-apply (simp add: abs_le_interval_iff)
+apply (simp add: abs_le_iff)
apply (rule_tac g="g" in summable_comparison_test, simp_all)
done
--- a/src/HOL/Hyperreal/Transcendental.thy Thu May 17 19:49:40 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Thu May 17 21:51:32 2007 +0200
@@ -70,7 +70,7 @@
apply (simp add: mult_assoc [symmetric] positive_imp_inverse_positive)
apply (rule order_less_imp_le)
apply (rule_tac z1 = "real (Suc na)" in real_mult_less_iff1 [THEN iffD1])
-apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc)
+apply (auto simp add: mult_assoc)
apply (erule order_less_trans)
apply (auto simp add: mult_less_cancel_left mult_ac)
done
@@ -641,7 +641,7 @@
qed
lemma exp_ge_add_one_self_aux: "0 \<le> x ==> (1 + x) \<le> exp(x)"
-apply (drule real_le_imp_less_or_eq, auto)
+apply (drule order_le_imp_less_or_eq, auto)
apply (simp add: exp_def)
apply (rule real_le_trans)
apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
@@ -1012,12 +1012,12 @@
lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
apply (insert abs_sin_le_one [of x])
-apply (simp add: abs_le_interval_iff del: abs_sin_le_one)
+apply (simp add: abs_le_iff del: abs_sin_le_one)
done
lemma sin_le_one [simp]: "sin x \<le> 1"
apply (insert abs_sin_le_one [of x])
-apply (simp add: abs_le_interval_iff del: abs_sin_le_one)
+apply (simp add: abs_le_iff del: abs_sin_le_one)
done
lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
@@ -1030,12 +1030,12 @@
lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
apply (insert abs_cos_le_one [of x])
-apply (simp add: abs_le_interval_iff del: abs_cos_le_one)
+apply (simp add: abs_le_iff del: abs_cos_le_one)
done
lemma cos_le_one [simp]: "cos x \<le> 1"
apply (insert abs_cos_le_one [of x])
-apply (simp add: abs_le_interval_iff del: abs_cos_le_one)
+apply (simp add: abs_le_iff del: abs_cos_le_one)
done
lemma DERIV_fun_pow: "DERIV g x :> m ==>
@@ -1268,7 +1268,7 @@
apply (rule fact_less_mono, auto)
done
declare cos_two_less_zero [simp]
-declare cos_two_less_zero [THEN real_not_refl2, simp]
+declare cos_two_less_zero [THEN less_imp_neq, simp]
declare cos_two_less_zero [THEN order_less_imp_le, simp]
lemma cos_is_zero: "EX! x. 0 \<le> x & x \<le> 2 & cos x = 0"
@@ -1299,11 +1299,11 @@
apply (rule cos_is_zero [THEN ex1E])
apply (auto simp add: pi_half)
apply (rule someI2, blast, safe)
-apply (drule_tac y = xa in real_le_imp_less_or_eq)
+apply (drule_tac y = xa in order_le_imp_less_or_eq)
apply (safe, simp)
done
declare pi_half_gt_zero [simp]
-declare pi_half_gt_zero [THEN real_not_refl2, THEN not_sym, simp]
+declare pi_half_gt_zero [THEN less_imp_neq, THEN not_sym, simp]
declare pi_half_gt_zero [THEN order_less_imp_le, simp]
lemma pi_half_less_two: "pi / 2 < 2"
@@ -1314,7 +1314,7 @@
apply (safe, simp)
done
declare pi_half_less_two [simp]
-declare pi_half_less_two [THEN real_not_refl2, simp]
+declare pi_half_less_two [THEN less_imp_neq, simp]
declare pi_half_less_two [THEN order_less_imp_le, simp]
lemma pi_gt_zero [simp]: "0 < pi"
@@ -1323,7 +1323,7 @@
done
lemma pi_neq_zero [simp]: "pi \<noteq> 0"
-by (rule pi_gt_zero [THEN real_not_refl2, THEN not_sym])
+by (rule pi_gt_zero [THEN less_imp_neq, THEN not_sym])
lemma pi_not_less_zero [simp]: "~ (pi < 0)"
apply (insert pi_gt_zero)
@@ -1646,7 +1646,7 @@
done
lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
-apply (frule real_le_imp_less_or_eq, safe)
+apply (frule order_le_imp_less_or_eq, safe)
prefer 2 apply force
apply (drule lemma_tan_total, safe)
apply (cut_tac f = tan and a = 0 and b = x and y = y in IVT_objl)
@@ -1675,7 +1675,7 @@
txt{*Now, simulate TRYALL*}
apply (rule_tac [!] DERIV_tan asm_rl)
apply (auto dest!: DERIV_unique [OF _ DERIV_tan]
- simp add: cos_gt_zero_pi [THEN real_not_refl2, THEN not_sym])
+ simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym])
done
lemma arcsin_pi:
@@ -2100,7 +2100,7 @@
apply (auto simp add: LIM_def)
apply (drule_tac x = "l/2" in spec, safe, force)
apply (rule_tac x = s in exI)
-apply (auto simp only: abs_interval_iff)
+apply (auto simp only: abs_less_iff)
done
lemma LIM_fun_less_zero:
@@ -2109,7 +2109,7 @@
apply (auto simp add: LIM_def)
apply (drule_tac x = "-l/2" in spec, safe, force)
apply (rule_tac x = s in exI)
-apply (auto simp only: abs_interval_iff)
+apply (auto simp only: abs_less_iff)
done
--- a/src/HOL/Real/RComplete.thy Thu May 17 19:49:40 2007 +0200
+++ b/src/HOL/Real/RComplete.thy Thu May 17 21:51:32 2007 +0200
@@ -423,7 +423,7 @@
"r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto)
apply (rename_tac n)
-apply (drule real_le_imp_less_or_eq, auto)
+apply (drule order_le_imp_less_or_eq, auto)
apply (rule_tac x = "- n - 1" in exI)
apply (rule_tac [2] x = "- n" in exI, auto)
done
@@ -547,7 +547,7 @@
done
lemma floor_mono2: "x \<le> y ==> floor x \<le> floor y"
-by (auto dest: real_le_imp_less_or_eq simp add: floor_mono)
+by (auto dest: order_le_imp_less_or_eq simp add: floor_mono)
lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
by (auto intro: lemma_floor)