# HG changeset patch
# User paulson
# Date 1091113061 -7200
# Node ID e6a2a98d5ef5470ea26c95fe61b08b9aed2d39ad
# Parent  5693a977a767c7128e13a33cf26101754df924d6
removal of more iff-rules from RealDef.thy

diff -r 5693a977a767 -r e6a2a98d5ef5 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Thu Jul 29 16:14:42 2004 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Thu Jul 29 16:57:41 2004 +0200
@@ -144,7 +144,7 @@
   show "\<exists>r. 0 < r \<and>
         (\<forall>s. 0 < s \<longrightarrow> (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r)"
   proof (intro exI conjI strip)
-    show "0 < L-k" by (simp add: k)
+    show "0 < L-k" by (simp add: k compare_rls)
     fix s :: real
     assume s: "0<s"
     { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
@@ -158,7 +158,7 @@
   show "\<exists>r. 0 < r \<and>
         (\<forall>s. 0 < s \<longrightarrow> (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r)"
   proof (intro exI conjI strip)
-    show "0 < k-L" by (simp add: k)
+    show "0 < k-L" by (simp add: k compare_rls)
     fix s :: real
     assume s: "0<s"
     { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
@@ -1607,7 +1607,7 @@
       from isCont_bounded [OF le this]
       obtain k where k: "!!x. a \<le> x & x \<le> b --> inverse (M - f x) \<le> k" by auto
       have Minv: "!!x. a \<le> x & x \<le> b --> 0 < inverse (M - f (x))"
-        by (simp add: M3) 
+        by (simp add: M3 compare_rls) 
       have "!!x. a \<le> x & x \<le> b --> inverse (M - f x) < k+1" using k 
         by (auto intro: order_le_less_trans [of _ k]) 
       with Minv 
diff -r 5693a977a767 -r e6a2a98d5ef5 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Thu Jul 29 16:14:42 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Thu Jul 29 16:57:41 2004 +0200
@@ -1675,8 +1675,9 @@
 lemma cos_zero_lemma: "[| 0 \<le> x; cos x = 0 |] ==>  
       \<exists>n::nat. ~even n & x = real n * (pi/2)"
 apply (drule pi_gt_zero [THEN reals_Archimedean4], safe)
-apply (subgoal_tac "0 \<le> x - real n * pi & (x - real n * pi) \<le> pi & (cos (x - real n * pi) = 0) ")
-apply safe
+apply (subgoal_tac "0 \<le> x - real n * pi & 
+                    (x - real n * pi) \<le> pi & (cos (x - real n * pi) = 0) ")
+apply (auto simp add: compare_rls) 
   prefer 3 apply (simp add: cos_diff) 
  prefer 2 apply (simp add: real_of_nat_Suc left_distrib) 
 apply (simp add: cos_diff)
@@ -1699,7 +1700,6 @@
 done
 
 
-(* also spoilt by numeral arithmetic *)
 lemma cos_zero_iff: "(cos x = 0) =  
       ((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |    
        (\<exists>n::nat. ~even n & (x = -(real n * (pi/2)))))"
diff -r 5693a977a767 -r e6a2a98d5ef5 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Thu Jul 29 16:14:42 2004 +0200
+++ b/src/HOL/Real/RealDef.thy	Thu Jul 29 16:57:41 2004 +0200
@@ -781,24 +781,15 @@
 by auto
 
 
-(** Simprules combining x-y and 0 (needed??) **)
-
-lemma real_0_less_diff_iff [iff]: "((0::real) < x-y) = (y < x)"
-by auto
-
-lemma real_0_le_diff_iff [iff]: "((0::real) \<le> x-y) = (y \<le> x)"
-by auto
-
 (*
 FIXME: we should have this, as for type int, but many proofs would break.
 It replaces x+-y by x-y.
-Addsimps [symmetric real_diff_def]
+declare real_diff_def [symmetric, simp]
 *)
 
 
 subsubsection{*Density of the Reals*}
 
-(*????FIXME: rename d1, d2 to x, y*)
 lemma real_lbound_gt_zero:
      "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2"
 apply (rule_tac x = " (min d1 d2) /2" in exI)
@@ -859,9 +850,6 @@
 
 ML
 {*
-val real_0_le_divide_iff = thm"real_0_le_divide_iff";
-val real_0_less_diff_iff = thm"real_0_less_diff_iff";
-val real_0_le_diff_iff = thm"real_0_le_diff_iff";
 val real_lbound_gt_zero = thm"real_lbound_gt_zero";
 val real_less_half_sum = thm"real_less_half_sum";
 val real_gt_half_sum = thm"real_gt_half_sum";