# HG changeset patch
# User huffman
# Date 1273600976 25200
# Node ID 84ee370b4b1b208b12768c9b06097bd15e1317a2
# Parent  4d4462d644aec537e459295667957da0ab4837ae# Parent  fc672bf92fc2d7d2161caf04aacd3da8c208a77c
merged

diff -r fc672bf92fc2 -r 84ee370b4b1b src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue May 11 17:55:19 2010 +0200
+++ b/src/HOL/Complex.thy	Tue May 11 11:02:56 2010 -0700
@@ -353,16 +353,26 @@
 apply (simp add: complex_norm_def)
 done
 
+lemma tendsto_Complex [tendsto_intros]:
+  assumes "(f ---> a) net" and "(g ---> b) net"
+  shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) net"
+proof (rule tendstoI)
+  fix r :: real assume "0 < r"
+  hence "0 < r / sqrt 2" by (simp add: divide_pos_pos)
+  have "eventually (\<lambda>x. dist (f x) a < r / sqrt 2) net"
+    using `(f ---> a) net` and `0 < r / sqrt 2` by (rule tendstoD)
+  moreover
+  have "eventually (\<lambda>x. dist (g x) b < r / sqrt 2) net"
+    using `(g ---> b) net` and `0 < r / sqrt 2` by (rule tendstoD)
+  ultimately
+  show "eventually (\<lambda>x. dist (Complex (f x) (g x)) (Complex a b) < r) net"
+    by (rule eventually_elim2)
+       (simp add: dist_norm real_sqrt_sum_squares_less)
+qed
+
 lemma LIMSEQ_Complex:
   "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. Complex (X n) (Y n)) ----> Complex a b"
-apply (rule LIMSEQ_I)
-apply (subgoal_tac "0 < r / sqrt 2")
-apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
-apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
-apply (rename_tac M N, rule_tac x="max M N" in exI, safe)
-apply (simp add: real_sqrt_sum_squares_less)
-apply (simp add: divide_pos_pos)
-done
+by (rule tendsto_Complex)
 
 instance complex :: banach
 proof
diff -r fc672bf92fc2 -r 84ee370b4b1b src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue May 11 17:55:19 2010 +0200
+++ b/src/HOL/Limits.thy	Tue May 11 11:02:56 2010 -0700
@@ -5,7 +5,7 @@
 header {* Filters and Limits *}
 
 theory Limits
-imports RealVector RComplete
+imports RealVector
 begin
 
 subsection {* Nets *}
diff -r fc672bf92fc2 -r 84ee370b4b1b src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Tue May 11 17:55:19 2010 +0200
+++ b/src/HOL/Nat_Numeral.thy	Tue May 11 11:02:56 2010 -0700
@@ -83,7 +83,7 @@
 
 end
 
-context comm_ring_1
+context ring_1
 begin
 
 lemma power2_minus [simp]:
@@ -113,6 +113,19 @@
 
 end
 
+context ring_1_no_zero_divisors
+begin
+
+lemma zero_eq_power2 [simp]:
+  "a\<twosuperior> = 0 \<longleftrightarrow> a = 0"
+  unfolding power2_eq_square by simp
+
+lemma power2_eq_1_iff [simp]:
+  "a\<twosuperior> = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
+  unfolding power2_eq_square by simp
+
+end
+
 context linordered_ring
 begin
 
@@ -163,10 +176,6 @@
 context linordered_idom
 begin
 
-lemma zero_eq_power2 [simp]:
-  "a\<twosuperior> = 0 \<longleftrightarrow> a = 0"
-  by (force simp add: power2_eq_square)
-
 lemma zero_le_power2 [simp]:
   "0 \<le> a\<twosuperior>"
   by (simp add: power2_eq_square)
diff -r fc672bf92fc2 -r 84ee370b4b1b src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Tue May 11 17:55:19 2010 +0200
+++ b/src/HOL/RComplete.thy	Tue May 11 11:02:56 2010 -0700
@@ -837,5 +837,27 @@
   apply simp
 done
 
+subsection {* Exponentiation with floor *}
+
+lemma floor_power:
+  assumes "x = real (floor x)"
+  shows "floor (x ^ n) = floor x ^ n"
+proof -
+  have *: "x ^ n = real (floor x ^ n)"
+    using assms by (induct n arbitrary: x) simp_all
+  show ?thesis unfolding real_of_int_inject[symmetric]
+    unfolding * floor_real_of_int ..
+qed
+
+lemma natfloor_power:
+  assumes "x = real (natfloor x)"
+  shows "natfloor (x ^ n) = natfloor x ^ n"
+proof -
+  from assms have "0 \<le> floor x" by auto
+  note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
+  from floor_power[OF this]
+  show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
+    by simp
+qed
 
 end
diff -r fc672bf92fc2 -r 84ee370b4b1b src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Tue May 11 17:55:19 2010 +0200
+++ b/src/HOL/RealPow.thy	Tue May 11 11:02:56 2010 -0700
@@ -69,18 +69,6 @@
   shows "x * x - 1 = (x + 1) * (x - 1)"
 by (simp add: algebra_simps)
 
-(* TODO: no longer real-specific; rename and move elsewhere *)
-lemma real_mult_is_one [simp]:
-  fixes x :: "'a::ring_1_no_zero_divisors"
-  shows "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
-proof -
-  have "x * x = 1 \<longleftrightarrow> (x + 1) * (x - 1) = 0"
-    by (simp add: algebra_simps)
-  also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1"
-    by (auto simp add: add_eq_0_iff minus_equation_iff [of _ 1])
-  finally show ?thesis .
-qed
-
 (* FIXME: declare this [simp] for all types, or not at all *)
 lemma realpow_two_sum_zero_iff [simp]:
      "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
@@ -113,54 +101,4 @@
     by (rule power_le_imp_le_base)
 qed
 
-subsection {*Floor*}
-
-lemma floor_power:
-  assumes "x = real (floor x)"
-  shows "floor (x ^ n) = floor x ^ n"
-proof -
-  have *: "x ^ n = real (floor x ^ n)"
-    using assms by (induct n arbitrary: x) simp_all
-  show ?thesis unfolding real_of_int_inject[symmetric]
-    unfolding * floor_real_of_int ..
-qed
-
-lemma natfloor_power:
-  assumes "x = real (natfloor x)"
-  shows "natfloor (x ^ n) = natfloor x ^ n"
-proof -
-  from assms have "0 \<le> floor x" by auto
-  note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
-  from floor_power[OF this]
-  show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
-    by simp
-qed
-
-subsection {*Various Other Theorems*}
-
-lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
-by auto
-
-lemma real_mult_inverse_cancel:
-     "[|(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: 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)
-done
-
-lemma real_mult_inverse_cancel2:
-     "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
-apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
-done
-
-(* TODO: no longer real-specific; rename and move elsewhere *)
-lemma realpow_num_eq_if:
-  fixes m :: "'a::power"
-  shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
-by (cases n, auto)
-
-
 end
diff -r fc672bf92fc2 -r 84ee370b4b1b src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue May 11 17:55:19 2010 +0200
+++ b/src/HOL/Rings.thy	Tue May 11 11:02:56 2010 -0700
@@ -349,6 +349,17 @@
 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
 begin
 
+lemma square_eq_1_iff [simp]:
+  "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
+proof -
+  have "(x - 1) * (x + 1) = x * x - 1"
+    by (simp add: algebra_simps)
+  hence "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
+    by simp
+  thus ?thesis
+    by (simp add: eq_neg_iff_add_eq_0)
+qed
+
 lemma mult_cancel_right1 [simp]:
   "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
 by (insert mult_cancel_right [of 1 c b], force)
diff -r fc672bf92fc2 -r 84ee370b4b1b src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Tue May 11 17:55:19 2010 +0200
+++ b/src/HOL/SEQ.thy	Tue May 11 11:02:56 2010 -0700
@@ -10,7 +10,7 @@
 header {* Sequences and Convergence *}
 
 theory SEQ
-imports Limits
+imports Limits RComplete
 begin
 
 abbreviation
diff -r fc672bf92fc2 -r 84ee370b4b1b src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue May 11 17:55:19 2010 +0200
+++ b/src/HOL/Transcendental.thy	Tue May 11 11:02:56 2010 -0700
@@ -1663,6 +1663,26 @@
 lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)"
 by simp
 
+lemma real_mult_inverse_cancel:
+     "[|(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: 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)
+done
+
+lemma real_mult_inverse_cancel2:
+     "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
+apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
+done
+
+lemma realpow_num_eq_if:
+  fixes m :: "'a::power"
+  shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
+by (cases n, auto)
+
 lemma cos_two_less_zero [simp]: "cos (2) < 0"
 apply (cut_tac x = 2 in cos_paired)
 apply (drule sums_minus)