--- 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
--- 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 *}
--- 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)
--- 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
--- 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
--- 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)
--- 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
--- 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)