# HG changeset patch
# User huffman
# Date 1179431492 -7200
# Node ID 97e1f9c2cc46b96c6d47d2da9710bd015bf1a689
# Parent  d4f3b015b50b02f9a87d37cc25bac87b5f0046dd
avoid using redundant lemmas from RealDef.thy

diff -r d4f3b015b50b -r 97e1f9c2cc46 src/HOL/Hyperreal/Deriv.thy
--- 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
diff -r d4f3b015b50b -r 97e1f9c2cc46 src/HOL/Hyperreal/Integration.thy
--- 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
 
diff -r d4f3b015b50b -r 97e1f9c2cc46 src/HOL/Hyperreal/Ln.thy
--- 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" .
diff -r d4f3b015b50b -r 97e1f9c2cc46 src/HOL/Hyperreal/NSA.thy
--- 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)
diff -r d4f3b015b50b -r 97e1f9c2cc46 src/HOL/Hyperreal/SEQ.thy
--- 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)
diff -r d4f3b015b50b -r 97e1f9c2cc46 src/HOL/Hyperreal/Series.thy
--- 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
 
diff -r d4f3b015b50b -r 97e1f9c2cc46 src/HOL/Hyperreal/Transcendental.thy
--- 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
 
 
diff -r d4f3b015b50b -r 97e1f9c2cc46 src/HOL/Real/RComplete.thy
--- 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)