# HG changeset patch
# User huffman
# Date 1336395857 -7200
# Node ID 25a6ca50fe1407060ce57aa7a4da29bf982288c6
# Parent  6440a74b2f62773d0f3a6cef1d4e1e7e6e8e8bb7
tuned ordering of lemmas

diff -r 6440a74b2f62 -r 25a6ca50fe14 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Thu May 10 10:07:41 2012 +0200
+++ b/src/HOL/RealDef.thy	Mon May 07 15:04:17 2012 +0200
@@ -301,6 +301,44 @@
   thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>inverse (X m) - inverse (X n)\<bar> < r" ..
 qed
 
+lemma vanishes_diff_inverse:
+  assumes X: "cauchy X" "\<not> vanishes X"
+  assumes Y: "cauchy Y" "\<not> vanishes Y"
+  assumes XY: "vanishes (\<lambda>n. X n - Y n)"
+  shows "vanishes (\<lambda>n. inverse (X n) - inverse (Y n))"
+proof (rule vanishesI)
+  fix r :: rat assume r: "0 < r"
+  obtain a i where a: "0 < a" and i: "\<forall>n\<ge>i. a < \<bar>X n\<bar>"
+    using cauchy_not_vanishes [OF X] by fast
+  obtain b j where b: "0 < b" and j: "\<forall>n\<ge>j. b < \<bar>Y n\<bar>"
+    using cauchy_not_vanishes [OF Y] by fast
+  obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
+  proof
+    show "0 < a * r * b"
+      using a r b by (simp add: mult_pos_pos)
+    show "inverse a * (a * r * b) * inverse b = r"
+      using a r b by simp
+  qed
+  obtain k where k: "\<forall>n\<ge>k. \<bar>X n - Y n\<bar> < s"
+    using vanishesD [OF XY s] ..
+  have "\<forall>n\<ge>max (max i j) k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r"
+  proof (clarsimp)
+    fix n assume n: "i \<le> n" "j \<le> n" "k \<le> n"
+    have "X n \<noteq> 0" and "Y n \<noteq> 0"
+      using i j a b n by auto
+    hence "\<bar>inverse (X n) - inverse (Y n)\<bar> =
+        inverse \<bar>X n\<bar> * \<bar>X n - Y n\<bar> * inverse \<bar>Y n\<bar>"
+      by (simp add: inverse_diff_inverse abs_mult)
+    also have "\<dots> < inverse a * s * inverse b"
+      apply (intro mult_strict_mono' less_imp_inverse_less)
+      apply (simp_all add: a b i j k n mult_nonneg_nonneg)
+      done
+    also note `inverse a * s * inverse b = r`
+    finally show "\<bar>inverse (X n) - inverse (Y n)\<bar> < r" .
+  qed
+  thus "\<exists>k. \<forall>n\<ge>k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r" ..
+qed
+
 subsection {* Equivalence relation on Cauchy sequences *}
 
 definition
@@ -451,44 +489,6 @@
   qed
 qed
 
-lemma vanishes_diff_inverse:
-  assumes X: "cauchy X" "\<not> vanishes X"
-  assumes Y: "cauchy Y" "\<not> vanishes Y"
-  assumes XY: "vanishes (\<lambda>n. X n - Y n)"
-  shows "vanishes (\<lambda>n. inverse (X n) - inverse (Y n))"
-proof (rule vanishesI)
-  fix r :: rat assume r: "0 < r"
-  obtain a i where a: "0 < a" and i: "\<forall>n\<ge>i. a < \<bar>X n\<bar>"
-    using cauchy_not_vanishes [OF X] by fast
-  obtain b j where b: "0 < b" and j: "\<forall>n\<ge>j. b < \<bar>Y n\<bar>"
-    using cauchy_not_vanishes [OF Y] by fast
-  obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
-  proof
-    show "0 < a * r * b"
-      using a r b by (simp add: mult_pos_pos)
-    show "inverse a * (a * r * b) * inverse b = r"
-      using a r b by simp
-  qed
-  obtain k where k: "\<forall>n\<ge>k. \<bar>X n - Y n\<bar> < s"
-    using vanishesD [OF XY s] ..
-  have "\<forall>n\<ge>max (max i j) k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r"
-  proof (clarsimp)
-    fix n assume n: "i \<le> n" "j \<le> n" "k \<le> n"
-    have "X n \<noteq> 0" and "Y n \<noteq> 0"
-      using i j a b n by auto
-    hence "\<bar>inverse (X n) - inverse (Y n)\<bar> =
-        inverse \<bar>X n\<bar> * \<bar>X n - Y n\<bar> * inverse \<bar>Y n\<bar>"
-      by (simp add: inverse_diff_inverse abs_mult)
-    also have "\<dots> < inverse a * s * inverse b"
-      apply (intro mult_strict_mono' less_imp_inverse_less)
-      apply (simp_all add: a b i j k n mult_nonneg_nonneg)
-      done
-    also note `inverse a * s * inverse b = r`
-    finally show "\<bar>inverse (X n) - inverse (Y n)\<bar> < r" .
-  qed
-  thus "\<exists>k. \<forall>n\<ge>k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r" ..
-qed
-
 lemma inverse_respects_realrel:
   "(\<lambda>X. if vanishes X then c else Real (\<lambda>n. inverse (X n))) respects realrel"
     (is "?inv respects realrel")