--- a/src/HOL/Deriv.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Deriv.thy Tue Jun 02 14:38:10 2009 +0200
@@ -76,7 +76,7 @@
hence "(\<lambda>h. f(x+h) - f(x)) -- 0 --> 0"
by (simp cong: LIM_cong)
thus "(\<lambda>h. f(x+h)) -- 0 --> f(x)"
- by (simp add: LIM_def)
+ by (simp add: LIM_def dist_norm)
qed
lemma DERIV_mult_lemma:
@@ -125,6 +125,7 @@
text{*Alternative definition for differentiability*}
lemma DERIV_LIM_iff:
+ fixes f :: "'a::{real_normed_vector,inverse} \<Rightarrow> 'a" shows
"((%h. (f(a + h) - f(a)) / h) -- 0 --> D) =
((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
apply (rule iffI)
@@ -577,7 +578,7 @@
apply (drule not_P_Bolzano_bisect', assumption+)
apply (rename_tac "l")
apply (drule_tac x = l in spec, clarify)
-apply (simp add: LIMSEQ_def)
+apply (simp add: LIMSEQ_iff)
apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
apply (drule real_less_half_sum, auto)
@@ -614,7 +615,7 @@
apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> ~ (f (u) \<le> y & y \<le> f (v))" in lemma_BOLZANO2)
apply safe
apply simp_all
-apply (simp add: isCont_iff LIM_def)
+apply (simp add: isCont_iff LIM_eq)
apply (rule ccontr)
apply (subgoal_tac "a \<le> x & x \<le> b")
prefer 2
@@ -675,7 +676,7 @@
apply (case_tac "a \<le> x & x \<le> b")
apply (rule_tac [2] x = 1 in exI)
prefer 2 apply force
-apply (simp add: LIM_def isCont_iff)
+apply (simp add: LIM_eq isCont_iff)
apply (drule_tac x = x in spec, auto)
apply (erule_tac V = "\<forall>M. \<exists>x. a \<le> x & x \<le> b & ~ f x \<le> M" in thin_rl)
apply (drule_tac x = 1 in spec, auto)
@@ -1486,7 +1487,7 @@
lemma LIM_fun_gt_zero:
"[| f -- c --> (l::real); 0 < l |]
==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
-apply (auto simp add: LIM_def)
+apply (auto simp add: LIM_eq)
apply (drule_tac x = "l/2" in spec, safe, force)
apply (rule_tac x = s in exI)
apply (auto simp only: abs_less_iff)
@@ -1495,7 +1496,7 @@
lemma LIM_fun_less_zero:
"[| f -- c --> (l::real); l < 0 |]
==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
-apply (auto simp add: LIM_def)
+apply (auto simp add: LIM_eq)
apply (drule_tac x = "-l/2" in spec, safe, force)
apply (rule_tac x = s in exI)
apply (auto simp only: abs_less_iff)
--- a/src/HOL/Integration.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Integration.thy Tue Jun 02 14:38:10 2009 +0200
@@ -108,6 +108,86 @@
with `a \<le> b` show ?thesis by auto
qed
+lemma fine_covers_all:
+ assumes "fine \<delta> (a, c) D" and "a < x" and "x \<le> c"
+ shows "\<exists> N < length D. \<forall> d t e. D ! N = (d,t,e) \<longrightarrow> d < x \<and> x \<le> e"
+ using assms
+proof (induct set: fine)
+ case (2 b c D a t)
+ thus ?case
+ proof (cases "b < x")
+ case True
+ with 2 obtain N where *: "N < length D"
+ and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
+ hence "Suc N < length ((a,t,b)#D) \<and>
+ (\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
+ thus ?thesis by auto
+ next
+ case False with 2
+ have "0 < length ((a,t,b)#D) \<and>
+ (\<forall> d t' e. ((a,t,b)#D) ! 0 = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
+ thus ?thesis by auto
+ qed
+qed auto
+
+lemma fine_append_split:
+ assumes "fine \<delta> (a,b) D" and "D2 \<noteq> []" and "D = D1 @ D2"
+ shows "fine \<delta> (a,fst (hd D2)) D1" (is "?fine1")
+ and "fine \<delta> (fst (hd D2), b) D2" (is "?fine2")
+proof -
+ from assms
+ have "?fine1 \<and> ?fine2"
+ proof (induct arbitrary: D1 D2)
+ case (2 b c D a' x D1 D2)
+ note induct = this
+
+ thus ?case
+ proof (cases D1)
+ case Nil
+ hence "fst (hd D2) = a'" using 2 by auto
+ with fine_Cons[OF `fine \<delta> (b,c) D` induct(3,4,5)] Nil induct
+ show ?thesis by (auto intro: fine_Nil)
+ next
+ case (Cons d1 D1')
+ with induct(2)[OF `D2 \<noteq> []`, of D1'] induct(8)
+ have "fine \<delta> (b, fst (hd D2)) D1'" and "fine \<delta> (fst (hd D2), c) D2" and
+ "d1 = (a', x, b)" by auto
+ with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons
+ show ?thesis by auto
+ qed
+ qed auto
+ thus ?fine1 and ?fine2 by auto
+qed
+
+lemma fine_\<delta>_expand:
+ assumes "fine \<delta> (a,b) D"
+ and "\<And> x. \<lbrakk> a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow> \<delta> x \<le> \<delta>' x"
+ shows "fine \<delta>' (a,b) D"
+using assms proof induct
+ case 1 show ?case by (rule fine_Nil)
+next
+ case (2 b c D a x)
+ show ?case
+ proof (rule fine_Cons)
+ show "fine \<delta>' (b,c) D" using 2 by auto
+ from fine_imp_le[OF 2(1)] 2(6) `x \<le> b`
+ show "b - a < \<delta>' x"
+ using 2(7)[OF `a \<le> x`] by auto
+ qed (auto simp add: 2)
+qed
+
+lemma fine_single_boundaries:
+ assumes "fine \<delta> (a,b) D" and "D = [(d, t, e)]"
+ shows "a = d \<and> b = e"
+using assms proof induct
+ case (2 b c D a x)
+ hence "D = []" and "a = d" and "b = e" by auto
+ moreover
+ from `fine \<delta> (b,c) D` `D = []` have "b = c"
+ by (rule empty_fine_imp_eq)
+ ultimately show ?case by simp
+qed auto
+
subsection {* Riemann sum *}
@@ -133,6 +213,9 @@
lemma rsum_add: "rsum D (\<lambda>x. f x + g x) = rsum D f + rsum D g"
by (induct D, auto simp add: algebra_simps)
+lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
+unfolding rsum_def map_append listsum_append ..
+
subsection {* Gauge integrability (definite) *}
@@ -232,6 +315,144 @@
algebra_simps rsum_right_distrib)
done
+lemma Integral_add:
+ assumes "Integral (a, b) f x1"
+ assumes "Integral (b, c) f x2"
+ assumes "a \<le> b" and "b \<le> c"
+ shows "Integral (a, c) f (x1 + x2)"
+proof (cases "a < b \<and> b < c", simp only: Integral_def split_conv, rule allI, rule impI)
+ fix \<epsilon> :: real assume "0 < \<epsilon>"
+ hence "0 < \<epsilon> / 2" by auto
+
+ assume "a < b \<and> b < c"
+ hence "a < b" and "b < c" by auto
+
+ from `Integral (a, b) f x1`[simplified Integral_def split_conv,
+ rule_format, OF `0 < \<epsilon>/2`]
+ obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
+ and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" by auto
+
+ from `Integral (b, c) f x2`[simplified Integral_def split_conv,
+ rule_format, OF `0 < \<epsilon>/2`]
+ obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
+ and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" by auto
+
+ def \<delta> \<equiv> "\<lambda> x. if x < b then min (\<delta>1 x) (b - x)
+ else if x = b then min (\<delta>1 b) (\<delta>2 b)
+ else min (\<delta>2 x) (x - b)"
+
+ have "gauge {a..c} \<delta>"
+ using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto
+ moreover {
+ fix D :: "(real \<times> real \<times> real) list"
+ assume fine: "fine \<delta> (a,c) D"
+ from fine_covers_all[OF this `a < b` `b \<le> c`]
+ obtain N where "N < length D"
+ and *: "\<forall> d t e. D ! N = (d, t, e) \<longrightarrow> d < b \<and> b \<le> e"
+ by auto
+ obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto)
+ with * have "d < b" and "b \<le> e" by auto
+ have in_D: "(d, t, e) \<in> set D"
+ using D_eq[symmetric] using `N < length D` by auto
+
+ from mem_fine[OF fine in_D]
+ have "d < e" and "d \<le> t" and "t \<le> e" by auto
+
+ have "t = b"
+ proof (rule ccontr)
+ assume "t \<noteq> b"
+ with mem_fine3[OF fine in_D] `b \<le> e` `d \<le> t` `t \<le> e` `d < b` \<delta>_def
+ show False by (cases "t < b") auto
+ qed
+
+ let ?D1 = "take N D"
+ let ?D2 = "drop N D"
+ def D1 \<equiv> "take N D @ [(d, t, b)]"
+ def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D"
+
+ have "D \<noteq> []" using `N < length D` by auto
+ from hd_drop_conv_nth[OF this `N < length D`]
+ have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto
+ with fine_append_split[OF _ _ append_take_drop_id[symmetric]]
+ have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2"
+ using `N < length D` fine by auto
+
+ have "fine \<delta>1 (a,b) D1" unfolding D1_def
+ proof (rule fine_append)
+ show "fine \<delta>1 (a, d) ?D1"
+ proof (rule fine1[THEN fine_\<delta>_expand])
+ fix x assume "a \<le> x" "x \<le> d"
+ hence "x \<le> b" using `d < b` `x \<le> d` by auto
+ thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto
+ qed
+
+ have "b - d < \<delta>1 t"
+ using mem_fine3[OF fine in_D] \<delta>_def `b \<le> e` `t = b` by auto
+ from `d < b` `d \<le> t` `t = b` this
+ show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto
+ qed
+ note rsum1 = I1[OF this]
+
+ have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
+ using nth_drop'[OF `N < length D`] by simp
+
+ have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)"
+ proof (cases "drop (Suc N) D = []")
+ case True
+ note * = fine2[simplified drop_split True D_eq append_Nil2]
+ have "e = c" using fine_single_boundaries[OF * refl] by auto
+ thus ?thesis unfolding True using fine_Nil by auto
+ next
+ case False
+ note * = fine_append_split[OF fine2 False drop_split]
+ from fine_single_boundaries[OF *(1)]
+ have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto
+ with *(2) have "fine \<delta> (e,c) (drop (Suc N) D)" by auto
+ thus ?thesis
+ proof (rule fine_\<delta>_expand)
+ fix x assume "e \<le> x" and "x \<le> c"
+ thus "\<delta> x \<le> \<delta>2 x" using `b \<le> e` unfolding \<delta>_def by auto
+ qed
+ qed
+
+ have "fine \<delta>2 (b, c) D2"
+ proof (cases "e = b")
+ case True thus ?thesis using fine2 by (simp add: D1_def D2_def)
+ next
+ case False
+ have "e - b < \<delta>2 b"
+ using mem_fine3[OF fine in_D] \<delta>_def `d < b` `t = b` by auto
+ with False `t = b` `b \<le> e`
+ show ?thesis using D2_def
+ by (auto intro!: fine_append[OF _ fine2] fine_single
+ simp del: append_Cons)
+ qed
+ note rsum2 = I2[OF this]
+
+ have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
+ using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
+ also have "\<dots> = rsum D1 f + rsum D2 f"
+ by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append ring_simps)
+ finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"
+ using add_strict_mono[OF rsum1 rsum2] by simp
+ }
+ ultimately show "\<exists> \<delta>. gauge {a .. c} \<delta> \<and>
+ (\<forall>D. fine \<delta> (a,c) D \<longrightarrow> \<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>)"
+ by blast
+next
+ case False
+ hence "a = b \<or> b = c" using `a \<le> b` and `b \<le> c` by auto
+ thus ?thesis
+ proof (rule disjE)
+ assume "a = b" hence "x1 = 0"
+ using `Integral (a, b) f x1` Integral_zero Integral_unique[of a b] by auto
+ thus ?thesis using `a = b` `Integral (b, c) f x2` by auto
+ next
+ assume "b = c" hence "x2 = 0"
+ using `Integral (b, c) f x2` Integral_zero Integral_unique[of b c] by auto
+ thus ?thesis using `b = c` `Integral (a, b) f x1` by auto
+ qed
+qed
text{*Fundamental theorem of calculus (Part I)*}
@@ -272,7 +493,7 @@
fix x :: real assume "a \<le> x" and "x \<le> b"
with f' have "DERIV f x :> f'(x)" by simp
then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
- by (simp add: DERIV_iff2 LIM_def)
+ by (simp add: DERIV_iff2 LIM_eq)
with `0 < e` obtain s
where "\<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s"
by (drule_tac x="e/2" in spec, auto)
@@ -339,18 +560,6 @@
lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
by simp
-lemma Integral_add:
- "[| a \<le> b; b \<le> c; Integral(a,b) f' k1; Integral(b,c) f' k2;
- \<forall>x. a \<le> x & x \<le> c --> DERIV f x :> f' x |]
- ==> Integral(a,c) f' (k1 + k2)"
-apply (rule FTC1 [THEN Integral_subst], auto)
-apply (frule FTC1, auto)
-apply (frule_tac a = b in FTC1, auto)
-apply (drule_tac x = x in spec, auto)
-apply (drule_tac ?k2.0 = "f b - f a" in Integral_unique)
-apply (drule_tac [3] ?k2.0 = "f c - f b" in Integral_unique, auto)
-done
-
subsection {* Additivity Theorem of Gauge Integral *}
text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
@@ -430,7 +639,7 @@
lemma Cauchy_iff2:
"Cauchy X =
(\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
-apply (simp add: Cauchy_def, auto)
+apply (simp add: Cauchy_iff, auto)
apply (drule reals_Archimedean, safe)
apply (drule_tac x = n in spec, auto)
apply (rule_tac x = M in exI, auto)
--- a/src/HOL/IsaMakefile Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/IsaMakefile Tue Jun 02 14:38:10 2009 +0200
@@ -280,6 +280,7 @@
Fact.thy \
Integration.thy \
Lim.thy \
+ Limits.thy \
Ln.thy \
Log.thy \
MacLaurin.thy \
@@ -315,6 +316,7 @@
Library/Abstract_Rat.thy \
Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy \
Library/Euclidean_Space.thy Library/Sum_Of_Squares.thy Library/positivstellensatz.ML \
+ Library/Convex_Euclidean_Space.thy \
Library/sum_of_squares.ML Library/Glbs.thy Library/normarith.ML \
Library/Executable_Set.thy Library/Infinite_Set.thy \
Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
--- a/src/HOL/Library/BigO.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Library/BigO.thy Tue Jun 02 14:38:10 2009 +0200
@@ -871,7 +871,7 @@
done
lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)"
- apply (simp add: LIMSEQ_def bigo_alt_def)
+ apply (simp add: LIMSEQ_iff bigo_alt_def)
apply clarify
apply (drule_tac x = "r / c" in spec)
apply (drule mp)
--- a/src/HOL/Library/Convex_Euclidean_Space.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Tue Jun 02 14:38:10 2009 +0200
@@ -1,6 +1,6 @@
-(* Title: Convex
- ID: $Id:
- Author: Robert Himmelmann, TU Muenchen*)
+(* Title: HOL/Library/Convex_Euclidean_Space.thy
+ Author: Robert Himmelmann, TU Muenchen
+*)
header {* Convex sets, functions and related things. *}
@@ -615,7 +615,7 @@
subsection {* One rather trivial consequence. *}
-lemma connected_UNIV: "connected UNIV"
+lemma connected_UNIV: "connected (UNIV :: (real ^ _) set)"
by(simp add: convex_connected convex_UNIV)
subsection {* Convex functions into the reals. *}
@@ -763,10 +763,10 @@
thus "dist x (u *s y + v *s z) \<le> e" using real_convex_bound_le[OF yz uv] by auto
qed
-lemma connected_ball: "connected(ball x e)"
+lemma connected_ball: "connected(ball (x::real^_) e)" (* FIXME: generalize *)
using convex_connected convex_ball by auto
-lemma connected_cball: "connected(cball x e)"
+lemma connected_cball: "connected(cball (x::real^_) e)" (* FIXME: generalize *)
using convex_connected convex_cball by auto
subsection {* Convex hull. *}
@@ -2186,13 +2186,15 @@
ultimately show "u *s x + v *s y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)])
using as(3-) dimindex_ge_1 apply- by(auto simp add: vector_component) qed
-lemma is_interval_connected: "is_interval s \<Longrightarrow> connected s"
+lemma is_interval_connected:
+ fixes s :: "(real ^ _) set"
+ shows "is_interval s \<Longrightarrow> connected s"
using is_interval_convex convex_connected by auto
lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n::finite}"
apply(rule_tac[!] is_interval_convex) using is_interval_interval by auto
-subsection {* On real^1, is_interval, convex and connected are all equivalent. *}
+subsection {* On @{text "real^1"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
lemma is_interval_1:
"is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b \<longrightarrow> x \<in> s)"
@@ -2988,7 +2990,9 @@
subsection {* Special case of straight-line paths. *}
-definition "linepath a b = (\<lambda>x. (1 - dest_vec1 x) *s a + dest_vec1 x *s b)"
+definition
+ linepath :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 1 \<Rightarrow> real ^ 'n" where
+ "linepath a b = (\<lambda>x. (1 - dest_vec1 x) *s a + dest_vec1 x *s b)"
lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a"
unfolding pathstart_def linepath_def by auto
--- a/src/HOL/Library/Euclidean_Space.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy Tue Jun 02 14:38:10 2009 +0200
@@ -498,6 +498,30 @@
apply simp
done
+subsection {* Metric *}
+
+instantiation "^" :: (metric_space, finite) metric_space
+begin
+
+definition dist_vector_def:
+ "dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
+
+instance proof
+ fix x y :: "'a ^ 'b"
+ show "dist x y = 0 \<longleftrightarrow> x = y"
+ unfolding dist_vector_def
+ by (simp add: setL2_eq_0_iff Cart_eq)
+next
+ fix x y z :: "'a ^ 'b"
+ show "dist x y \<le> dist x z + dist y z"
+ unfolding dist_vector_def
+ apply (rule order_trans [OF _ setL2_triangle_ineq])
+ apply (simp add: setL2_mono dist_triangle2)
+ done
+qed
+
+end
+
subsection {* Norms *}
instantiation "^" :: (real_normed_vector, finite) real_normed_vector
@@ -509,9 +533,6 @@
definition vector_sgn_def:
"sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
-definition dist_vector_def:
- "dist (x::'a^'b) y = norm (x - y)"
-
instance proof
fix a :: real and x y :: "'a ^ 'b"
show "0 \<le> norm x"
@@ -531,7 +552,8 @@
show "sgn x = scaleR (inverse (norm x)) x"
by (rule vector_sgn_def)
show "dist x y = norm (x - y)"
- by (rule dist_vector_def)
+ unfolding dist_vector_def vector_norm_def
+ by (simp add: dist_norm)
qed
end
@@ -697,7 +719,7 @@
qed
lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y - x) < d \<longrightarrow> abs(y * y - x * x) < e)"
- using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_def, rule_format, of e x] apply (auto simp add: power2_eq_square)
+ using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_eq, rule_format, of e x] apply (auto simp add: power2_eq_square)
apply (rule_tac x="s" in exI)
apply auto
apply (erule_tac x=y in allE)
@@ -949,6 +971,11 @@
"x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
using norm_ge_zero[of "x - y"] by auto
+lemma vector_dist_norm:
+ fixes x y :: "real ^ _"
+ shows "dist x y = norm (x - y)"
+ by (rule dist_norm)
+
use "normarith.ML"
method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
@@ -2566,7 +2593,7 @@
qed
lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y"
- by (metis dist_vector_def fstcart_sub[symmetric] norm_fstcart)
+ unfolding dist_norm by (metis fstcart_sub[symmetric] norm_fstcart)
lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))"
proof-
@@ -2581,7 +2608,7 @@
qed
lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y"
- by (metis dist_vector_def sndcart_sub[symmetric] norm_sndcart)
+ unfolding dist_norm by (metis sndcart_sub[symmetric] norm_sndcart)
lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n::finite) (x2::'a::{times,comm_monoid_add}^'m::finite)) \<bullet> (pastecart y1 y2) = x1 \<bullet> y1 + x2 \<bullet> y2"
by (simp add: dot_def setsum_UNIV_sum pastecart_def)
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Jun 02 14:38:10 2009 +0200
@@ -306,12 +306,12 @@
from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
by blast
hence x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r"
- unfolding LIMSEQ_def real_norm_def .
+ unfolding LIMSEQ_iff real_norm_def .
from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y"
by blast
hence y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r"
- unfolding LIMSEQ_def real_norm_def .
+ unfolding LIMSEQ_iff real_norm_def .
let ?w = "Complex x y"
from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto
{fix e assume ep: "e > (0::real)"
--- a/src/HOL/Library/Library.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Library/Library.thy Tue Jun 02 14:38:10 2009 +0200
@@ -14,6 +14,7 @@
Commutative_Ring
Continuity
ContNotDenum
+ Convex_Euclidean_Space
Countable
Determinants
Diagonalize
--- a/src/HOL/Library/Product_Vector.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Library/Product_Vector.thy Tue Jun 02 14:38:10 2009 +0200
@@ -39,6 +39,38 @@
end
+subsection {* Product is a metric space *}
+
+instantiation
+ "*" :: (metric_space, metric_space) metric_space
+begin
+
+definition dist_prod_def:
+ "dist (x::'a \<times> 'b) y = sqrt ((dist (fst x) (fst y))\<twosuperior> + (dist (snd x) (snd y))\<twosuperior>)"
+
+lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<twosuperior> + (dist b d)\<twosuperior>)"
+ unfolding dist_prod_def by simp
+
+instance proof
+ fix x y :: "'a \<times> 'b"
+ show "dist x y = 0 \<longleftrightarrow> x = y"
+ unfolding dist_prod_def
+ by (simp add: expand_prod_eq)
+next
+ fix x y z :: "'a \<times> 'b"
+ show "dist x y \<le> dist x z + dist y z"
+ unfolding dist_prod_def
+ apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
+ apply (rule real_sqrt_le_mono)
+ apply (rule order_trans [OF add_mono])
+ apply (rule power_mono [OF dist_triangle2 [of _ _ "fst z"] zero_le_dist])
+ apply (rule power_mono [OF dist_triangle2 [of _ _ "snd z"] zero_le_dist])
+ apply (simp only: real_sum_squared_expand)
+ done
+qed
+
+end
+
subsection {* Product is a normed vector space *}
instantiation
@@ -51,9 +83,6 @@
definition sgn_prod_def:
"sgn (x::'a \<times> 'b) = scaleR (inverse (norm x)) x"
-definition dist_prod_def:
- "dist (x::'a \<times> 'b) y = norm (x - y)"
-
lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<twosuperior> + (norm b)\<twosuperior>)"
unfolding norm_prod_def by simp
@@ -78,7 +107,8 @@
show "sgn x = scaleR (inverse (norm x)) x"
by (rule sgn_prod_def)
show "dist x y = norm (x - y)"
- by (rule dist_prod_def)
+ unfolding dist_prod_def norm_prod_def
+ by (simp add: dist_norm)
qed
end
@@ -179,53 +209,53 @@
lemma LIMSEQ_Pair:
assumes "X ----> a" and "Y ----> b"
shows "(\<lambda>n. (X n, Y n)) ----> (a, b)"
-proof (rule LIMSEQ_I)
+proof (rule metric_LIMSEQ_I)
fix r :: real assume "0 < r"
then have "0 < r / sqrt 2" (is "0 < ?s")
by (simp add: divide_pos_pos)
- obtain M where M: "\<forall>n\<ge>M. norm (X n - a) < ?s"
- using LIMSEQ_D [OF `X ----> a` `0 < ?s`] ..
- obtain N where N: "\<forall>n\<ge>N. norm (Y n - b) < ?s"
- using LIMSEQ_D [OF `Y ----> b` `0 < ?s`] ..
- have "\<forall>n\<ge>max M N. norm ((X n, Y n) - (a, b)) < r"
- using M N by (simp add: real_sqrt_sum_squares_less norm_Pair)
- then show "\<exists>n0. \<forall>n\<ge>n0. norm ((X n, Y n) - (a, b)) < r" ..
+ obtain M where M: "\<forall>n\<ge>M. dist (X n) a < ?s"
+ using metric_LIMSEQ_D [OF `X ----> a` `0 < ?s`] ..
+ obtain N where N: "\<forall>n\<ge>N. dist (Y n) b < ?s"
+ using metric_LIMSEQ_D [OF `Y ----> b` `0 < ?s`] ..
+ have "\<forall>n\<ge>max M N. dist (X n, Y n) (a, b) < r"
+ using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
+ then show "\<exists>n0. \<forall>n\<ge>n0. dist (X n, Y n) (a, b) < r" ..
qed
lemma Cauchy_Pair:
assumes "Cauchy X" and "Cauchy Y"
shows "Cauchy (\<lambda>n. (X n, Y n))"
-proof (rule CauchyI)
+proof (rule metric_CauchyI)
fix r :: real assume "0 < r"
then have "0 < r / sqrt 2" (is "0 < ?s")
by (simp add: divide_pos_pos)
- obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < ?s"
- using CauchyD [OF `Cauchy X` `0 < ?s`] ..
- obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (Y m - Y n) < ?s"
- using CauchyD [OF `Cauchy Y` `0 < ?s`] ..
- have "\<forall>m\<ge>max M N. \<forall>n\<ge>max M N. norm ((X m, Y m) - (X n, Y n)) < r"
- using M N by (simp add: real_sqrt_sum_squares_less norm_Pair)
- then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. norm ((X m, Y m) - (X n, Y n)) < r" ..
+ obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < ?s"
+ using metric_CauchyD [OF `Cauchy X` `0 < ?s`] ..
+ obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (Y m) (Y n) < ?s"
+ using metric_CauchyD [OF `Cauchy Y` `0 < ?s`] ..
+ have "\<forall>m\<ge>max M N. \<forall>n\<ge>max M N. dist (X m, Y m) (X n, Y n) < r"
+ using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
+ then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
qed
lemma LIM_Pair:
assumes "f -- x --> a" and "g -- x --> b"
shows "(\<lambda>x. (f x, g x)) -- x --> (a, b)"
-proof (rule LIM_I)
+proof (rule metric_LIM_I)
fix r :: real assume "0 < r"
then have "0 < r / sqrt 2" (is "0 < ?e")
by (simp add: divide_pos_pos)
obtain s where s: "0 < s"
- "\<forall>z. z \<noteq> x \<and> norm (z - x) < s \<longrightarrow> norm (f z - a) < ?e"
- using LIM_D [OF `f -- x --> a` `0 < ?e`] by fast
+ "\<forall>z. z \<noteq> x \<and> dist z x < s \<longrightarrow> dist (f z) a < ?e"
+ using metric_LIM_D [OF `f -- x --> a` `0 < ?e`] by fast
obtain t where t: "0 < t"
- "\<forall>z. z \<noteq> x \<and> norm (z - x) < t \<longrightarrow> norm (g z - b) < ?e"
- using LIM_D [OF `g -- x --> b` `0 < ?e`] by fast
+ "\<forall>z. z \<noteq> x \<and> dist z x < t \<longrightarrow> dist (g z) b < ?e"
+ using metric_LIM_D [OF `g -- x --> b` `0 < ?e`] by fast
have "0 < min s t \<and>
- (\<forall>z. z \<noteq> x \<and> norm (z - x) < min s t \<longrightarrow> norm ((f z, g z) - (a, b)) < r)"
- using s t by (simp add: real_sqrt_sum_squares_less norm_Pair)
+ (\<forall>z. z \<noteq> x \<and> dist z x < min s t \<longrightarrow> dist (f z, g z) (a, b) < r)"
+ using s t by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
then show
- "\<exists>s>0. \<forall>z. z \<noteq> x \<and> norm (z - x) < s \<longrightarrow> norm ((f z, g z) - (a, b)) < r" ..
+ "\<exists>s>0. \<forall>z. z \<noteq> x \<and> dist z x < s \<longrightarrow> dist (f z, g z) (a, b) < r" ..
qed
lemma isCont_Pair [simp]:
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Tue Jun 02 14:38:10 2009 +0200
@@ -195,7 +195,7 @@
subsection{* The universal Euclidean versions are what we use most of the time *}
definition
- "open" :: "(real ^ 'n::finite) set \<Rightarrow> bool" where
+ "open" :: "'a::metric_space set \<Rightarrow> bool" where
"open S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>e >0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> S)"
definition "closed S \<longleftrightarrow> open(UNIV - S)"
definition "euclidean = topology open"
@@ -288,17 +288,26 @@
subsection{* Open and closed balls. *}
definition
- ball :: "real ^ 'n::finite \<Rightarrow> real \<Rightarrow> (real^'n) set" where
+ ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
"ball x e = {y. dist x y < e}"
definition
- cball :: "real ^ 'n::finite \<Rightarrow> real \<Rightarrow> (real^'n) set" where
+ cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
"cball x e = {y. dist x y \<le> e}"
lemma mem_ball[simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" by (simp add: ball_def)
lemma mem_cball[simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" by (simp add: cball_def)
-lemma mem_ball_0[simp]: "x \<in> ball 0 e \<longleftrightarrow> norm x < e" by (simp add: dist_norm)
-lemma mem_cball_0[simp]: "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" by (simp add: dist_norm)
+
+lemma mem_ball_0 [simp]:
+ fixes x :: "'a::real_normed_vector"
+ shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e"
+ by (simp add: dist_norm)
+
+lemma mem_cball_0 [simp]:
+ fixes x :: "'a::real_normed_vector"
+ shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
+ by (simp add: dist_norm)
+
lemma centre_in_cball[simp]: "x \<in> cball x e \<longleftrightarrow> 0\<le> e" by simp
lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq)
lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq)
@@ -494,8 +503,9 @@
subsection{* Limit points *}
-definition islimpt:: "real ^'n::finite \<Rightarrow> (real^'n) set \<Rightarrow> bool" (infixr "islimpt" 60) where
- islimpt_def: "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
+definition
+ islimpt:: "'a::metric_space \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) where
+ "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
(* FIXME: Sure this form is OK????*)
lemma islimptE: assumes "x islimpt S" and "x \<in> T" and "open T"
@@ -519,17 +529,44 @@
using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
by metis (* FIXME: VERY slow! *)
-lemma islimpt_UNIV[simp, intro]: "(x:: real ^'n::finite) islimpt UNIV"
-proof-
+axclass perfect_space \<subseteq> metric_space
+ islimpt_UNIV [simp, intro]: "x islimpt UNIV"
+
+lemma perfect_choose_dist:
+ fixes x :: "'a::perfect_space"
+ shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
+using islimpt_UNIV [of x]
+by (simp add: islimpt_approachable)
+
+instance real :: perfect_space
+apply default
+apply (rule islimpt_approachable [THEN iffD2])
+apply (clarify, rule_tac x="x + e/2" in bexI)
+apply (auto simp add: dist_norm)
+done
+
+instance "^" :: (perfect_space, finite) perfect_space
+proof
+ fix x :: "'a ^ 'b"
{
- fix e::real assume ep: "e>0"
- from vector_choose_size[of "e/2"] ep have "\<exists>(c:: real ^'n). norm c = e/2" by auto
- then obtain c ::"real^'n" where c: "norm c = e/2" by blast
- let ?x = "x + c"
- have "?x \<noteq> x" using c ep by (auto simp add: norm_eq_0_imp)
- moreover have "dist ?x x < e" using c ep apply simp by norm
- ultimately have "\<exists>x'. x' \<noteq> x\<and> dist x' x < e" by blast}
- then show ?thesis unfolding islimpt_approachable by blast
+ fix e :: real assume "0 < e"
+ def a \<equiv> "x $ arbitrary"
+ have "a islimpt UNIV" by (rule islimpt_UNIV)
+ with `0 < e` obtain b where "b \<noteq> a" and "dist b a < e"
+ unfolding islimpt_approachable by auto
+ def y \<equiv> "Cart_lambda ((Cart_nth x)(arbitrary := b))"
+ from `b \<noteq> a` have "y \<noteq> x"
+ unfolding a_def y_def by (simp add: Cart_eq)
+ from `dist b a < e` have "dist y x < e"
+ unfolding dist_vector_def a_def y_def
+ apply simp
+ apply (rule le_less_trans [OF setL2_le_setsum [OF zero_le_dist]])
+ apply (subst setsum_diff1' [where a=arbitrary], simp, simp, simp)
+ done
+ from `y \<noteq> x` and `dist y x < e`
+ have "\<exists>y\<in>UNIV. y \<noteq> x \<and> dist y x < e" by auto
+ }
+ then show "x islimpt UNIV" unfolding islimpt_approachable by blast
qed
lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
@@ -562,7 +599,7 @@
qed
lemma finite_set_avoid:
- fixes a :: "real ^ 'n::finite"
+ fixes a :: "'a::metric_space"
assumes fS: "finite S" shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
proof(induct rule: finite_induct[OF fS])
case 1 thus ?case apply auto by ferrack
@@ -594,7 +631,7 @@
done
lemma discrete_imp_closed:
- assumes e: "0 < e" and d: "\<forall>x \<in> S. \<forall>y \<in> S. norm(y - x) < e \<longrightarrow> y = x"
+ assumes e: "0 < e" and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
shows "closed S"
proof-
{fix x assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
@@ -603,8 +640,7 @@
let ?m = "min (e/2) (dist x y) "
from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym])
from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" by blast
- have th: "norm (z - y) < e" using z y
- unfolding dist_norm [symmetric]
+ have th: "dist z y < e" using z y
by (intro dist_triangle_lt [where z=x], simp)
from d[rule_format, OF y(1) z(1) th] y z
have False by (auto simp add: dist_commute)}
@@ -644,23 +680,28 @@
apply (metis Int_lower1 Int_lower2 subset_interior)
by (metis Int_mono interior_subset open_inter open_interior open_subset_interior)
-lemma interior_limit_point[intro]: assumes x: "x \<in> interior S" shows "x islimpt S"
+lemma interior_limit_point [intro]:
+ fixes x :: "'a::perfect_space"
+ assumes x: "x \<in> interior S" shows "x islimpt S"
proof-
from x obtain e where e: "e>0" "\<forall>x'. dist x x' < e \<longrightarrow> x' \<in> S"
unfolding mem_interior subset_eq Ball_def mem_ball by blast
- {fix d::real assume d: "d>0"
- let ?m = "min d e / 2"
- have mde2: "?m \<ge> 0" using e(1) d(1) by arith
- from vector_choose_dist[OF mde2, of x]
- obtain y where y: "dist x y = ?m" by blast
- have th: "dist x y < e" "dist x y < d" unfolding y using e(1) d(1) by arith+
+ {
+ fix d::real assume d: "d>0"
+ let ?m = "min d e"
+ have mde2: "0 < ?m" using e(1) d(1) by simp
+ from perfect_choose_dist [OF mde2, of x]
+ obtain y where "y \<noteq> x" and "dist y x < ?m" by blast
+ then have "dist y x < e" "dist y x < d" by simp_all
+ from `dist y x < e` e(2) have "y \<in> S" by (simp add: dist_commute)
have "\<exists>x'\<in>S. x'\<noteq> x \<and> dist x' x < d"
- apply (rule bexI[where x=y])
- using e th y by (auto simp add: dist_commute)}
+ using `y \<in> S` `y \<noteq> x` `dist y x < d` by fast
+ }
then show ?thesis unfolding islimpt_approachable by blast
qed
lemma interior_closed_Un_empty_interior:
+ fixes S T :: "(real ^ 'n::finite) set" (* FIXME: generalize to perfect_space *)
assumes cS: "closed S" and iT: "interior T = {}"
shows "interior(S \<union> T) = interior S"
proof-
@@ -690,7 +731,7 @@
done
then have "\<exists>z. z \<notin> T \<and> z\<noteq> y \<and> dist z y < d \<and> dist x z < e" by blast
then have "\<exists>x' \<in>S. x'\<noteq>y \<and> dist x' y < d" using e by auto}
- then have "y\<in>S" by (metis islimpt_approachable cS closed_limpt) }
+ then have "y\<in>S" by (metis islimpt_approachable [where 'a="real^'n"] cS closed_limpt[where 'a="real^'n"]) }
then have "x \<in> interior S" unfolding mem_interior using e(1) by blast}
hence "interior (S\<union>T) \<subseteq> interior S" unfolding mem_interior Ball_def subset_eq by blast
ultimately show ?thesis by blast
@@ -766,7 +807,7 @@
with * have "closure S \<subseteq> t"
unfolding closure_def
using closed_limpt[of t]
- by blast
+ by auto
}
ultimately show ?thesis
using hull_unique[of S, of "closure S", of closed]
@@ -971,17 +1012,24 @@
subsection{* Common nets and The "within" modifier for nets. *}
definition
- at :: "real ^ 'n::finite \<Rightarrow> (real ^ 'n) net" where
+ at :: "'a::perfect_space \<Rightarrow> 'a net" where
"at a = mknet(\<lambda>x y. 0 < dist x a \<and> dist x a <= dist y a)"
-definition "at_infinity = mknet(\<lambda>x y. norm x \<ge> norm y)"
-definition "sequentially = mknet(\<lambda>(m::nat) n. m >= n)"
-
-definition within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
- within_def: "net within S = mknet (\<lambda>x y. netord net x y \<and> x \<in> S)"
-
-definition indirection :: "real ^'n::finite \<Rightarrow> real ^'n \<Rightarrow> (real ^'n) net" (infixr "indirection" 70) where
- indirection_def: "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = c*s v}"
+definition
+ at_infinity :: "'a::real_normed_vector net" where
+ "at_infinity = mknet (\<lambda>x y. norm x \<ge> norm y)"
+
+definition
+ sequentially :: "nat net" where
+ "sequentially = mknet (\<lambda>m n. n \<le> m)"
+
+definition
+ within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
+ "net within S = mknet (\<lambda>x y. netord net x y \<and> x \<in> S)"
+
+definition
+ indirection :: "real ^'n::finite \<Rightarrow> real ^'n \<Rightarrow> (real ^'n) net" (infixr "indirection" 70) where
+ "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = c*s v}"
text{* Prove That They are all nets. *}
@@ -1024,19 +1072,22 @@
lemma in_direction: "netord (a indirection v) x y \<longleftrightarrow> 0 < dist x a \<and> dist x a \<le> dist y a \<and> (\<exists>c \<ge> 0. x - a = c *s v)"
by (simp add: within at indirection_def)
-lemma within_UNIV: "at x within UNIV = at x"
- by (simp add: within_def at_def netord_inverse)
+lemma within_UNIV: "net within UNIV = net"
+ by (simp add: within_def netord_inverse)
subsection{* Identify Trivial limits, where we can't approach arbitrarily closely. *}
-
-definition "trivial_limit (net:: 'a net) \<longleftrightarrow>
- (\<forall>(a::'a) b. a = b) \<or> (\<exists>(a::'a) b. a \<noteq> b \<and> (\<forall>x. ~(netord (net) x a) \<and> ~(netord(net) x b)))"
-
-
-lemma trivial_limit_within: "trivial_limit (at (a::real^'n::finite) within S) \<longleftrightarrow> ~(a islimpt S)"
+definition
+ trivial_limit :: "'a net \<Rightarrow> bool" where
+ "trivial_limit (net:: 'a net) \<longleftrightarrow>
+ (\<forall>(a::'a) b. a = b) \<or>
+ (\<exists>(a::'a) b. a \<noteq> b \<and> (\<forall>x. ~(netord (net) x a) \<and> ~(netord(net) x b)))"
+
+lemma trivial_limit_within:
+ fixes a :: "'a::perfect_space"
+ shows "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
proof-
- {assume "\<forall>(a::real^'n) b. a = b" hence "\<not> a islimpt S"
+ {assume "\<forall>(a::'a) b. a = b" hence "\<not> a islimpt S"
apply (simp add: islimpt_approachable_le)
by (rule exI[where x=1], auto)}
moreover
@@ -1051,30 +1102,35 @@
{assume "\<not> a islimpt S"
then obtain e where e: "e > 0" "\<forall>x' \<in> S. x' \<noteq> a \<longrightarrow> dist x' a > e"
unfolding islimpt_approachable_le by (auto simp add: not_le)
- from e vector_choose_dist[of e a] obtain b where b: "dist a b = e" by auto
- from b e(1) have "a \<noteq> b" by (simp add: dist_nz)
+ from e perfect_choose_dist[of e a] obtain b where b: "b \<noteq> a" "dist b a < e" by auto
+ then have "a \<noteq> b" by auto
moreover have "\<forall>x. \<not> ((0 < dist x a \<and> dist x a \<le> dist a a) \<and> x \<in> S) \<and>
\<not> ((0 < dist x a \<and> dist x a \<le> dist b a) \<and> x \<in> S)"
using e(2) b by (auto simp add: dist_commute)
- ultimately have "trivial_limit (at a within S)" unfolding trivial_limit_def within at
+ ultimately have "trivial_limit (at a within S)"
+ unfolding trivial_limit_def within at
by blast}
ultimately show ?thesis unfolding trivial_limit_def by blast
qed
-lemma trivial_limit_at: "~(trivial_limit (at a))"
- apply (subst within_UNIV[symmetric])
- by (simp add: trivial_limit_within islimpt_UNIV)
-
-lemma trivial_limit_at_infinity: "~(trivial_limit (at_infinity :: ('a::{norm,zero_neq_one}) net))"
+lemma trivial_limit_at: "\<not> trivial_limit (at a)"
+ using trivial_limit_within [of a UNIV]
+ by (simp add: within_UNIV)
+
+lemma trivial_limit_at_infinity:
+ "\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,zero_neq_one}) net)"
apply (simp add: trivial_limit_def at_infinity)
by (metis order_refl zero_neq_one)
-lemma trivial_limit_sequentially: "~(trivial_limit sequentially)"
+lemma trivial_limit_sequentially: "\<not> trivial_limit sequentially"
by (auto simp add: trivial_limit_def sequentially)
subsection{* Some property holds "sufficiently close" to the limit point. *}
-definition "eventually P net \<longleftrightarrow> trivial_limit net \<or> (\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> P x))"
+definition
+ eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
+ "eventually P net \<longleftrightarrow> trivial_limit net \<or>
+ (\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> P x))"
lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
by (metis eventually_def)
@@ -1100,7 +1156,7 @@
unfolding eventually_def trivial_limit_within islimpt_approachable_le within at unfolding dist_nz[THEN sym] by (clarsimp, rule_tac x=d in exI, auto)
qed
-lemma eventually_within: " eventually P (at a within S) \<longleftrightarrow>
+lemma eventually_within: "eventually P (at a within S) \<longleftrightarrow>
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
proof-
{ fix d
@@ -1134,9 +1190,17 @@
thus "?lhs" unfolding eventually_def at_infinity using b y by auto
qed
-lemma always_eventually: "(\<forall>(x::'a::zero_neq_one). P x) ==> eventually P net"
- apply (auto simp add: eventually_def trivial_limit_def )
- by (rule exI[where x=0], rule exI[where x=1], rule zero_neq_one)
+lemma always_eventually: "(\<forall>x. P x) ==> eventually P net"
+ unfolding eventually_def trivial_limit_def by (clarify, simp)
+
+lemma eventually_True [simp]: "eventually (\<lambda>x. True) net"
+ by (simp add: always_eventually)
+
+lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
+ unfolding eventually_def by simp
+
+lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
+ unfolding eventually_def trivial_limit_def by auto
text{* Combining theorems for "eventually" *}
@@ -1159,9 +1223,24 @@
lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually P net)"
by (auto simp add: eventually_def)
+lemma eventually_rev_mono:
+ "eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net"
+using eventually_mono [of P Q] by fast
+
+lemma eventually_rev_mp:
+ assumes 1: "eventually (\<lambda>x. P x) net"
+ assumes 2: "eventually (\<lambda>x. P x \<longrightarrow> Q x) net"
+ shows "eventually (\<lambda>x. Q x) net"
+using 2 1 by (rule eventually_mp)
+
+lemma eventually_conjI:
+ "\<lbrakk>eventually (\<lambda>x. P x) net; eventually (\<lambda>x. Q x) net\<rbrakk>
+ \<Longrightarrow> eventually (\<lambda>x. P x \<and> Q x) net"
+by (simp add: eventually_and)
+
subsection{* Limits, defined as vacuously true when the limit is trivial. *}
-definition tendsto:: "('a \<Rightarrow> real ^'n::finite) \<Rightarrow> real ^'n \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "--->" 55) where
+definition tendsto:: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "--->" 55) where
tendsto_def: "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
lemma tendstoD: "(f ---> l) net \<Longrightarrow> e>0 \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
@@ -1173,9 +1252,8 @@
lemma Lim:
"(f ---> l) net \<longleftrightarrow>
trivial_limit net \<or>
- (\<forall>e>0. \<exists>y. (\<exists>x. netord net x y) \<and>
- (\<forall>x. netord(net) x y \<longrightarrow> dist (f x) l < e))"
- by (auto simp add: tendsto_def eventually_def)
+ (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
+ unfolding tendsto_def trivial_limit_eq by auto
text{* Show that they yield usual definitions in the various cases. *}
@@ -1192,6 +1270,9 @@
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
by (auto simp add: tendsto_def eventually_at)
+lemma Lim_at_iff_LIM: "(f ---> l) (at a) \<longleftrightarrow> f -- a --> l"
+ unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff)
+
lemma Lim_at_infinity:
"(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x::real^'n::finite. norm x >= b \<longrightarrow> dist (f x) l < e)"
by (auto simp add: tendsto_def eventually_at_infinity)
@@ -1201,8 +1282,11 @@
(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)"
by (auto simp add: tendsto_def eventually_sequentially)
+lemma Lim_sequentially_iff_LIMSEQ: "(S ---> l) sequentially \<longleftrightarrow> S ----> l"
+ unfolding Lim_sequentially LIMSEQ_def ..
+
lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
- by (auto simp add: eventually_def Lim)
+ unfolding tendsto_def by (auto elim: eventually_rev_mono)
text{* The expected monotonicity property. *}
@@ -1226,7 +1310,7 @@
qed
lemma Lim_Un_univ:
- "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow> S \<union> T = (UNIV::(real^'n::finite) set)
+ "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow> S \<union> T = UNIV
==> (f ---> l) (at x)"
by (metis Lim_Un within_UNIV)
@@ -1280,7 +1364,7 @@
ultimately show ?rhs apply (rule_tac x="(\<lambda>n::nat. f (inverse (real n + 1)))" in exI) by auto
next
assume ?rhs
- then obtain f::"nat\<Rightarrow>real^'a" where f:"(\<forall>n. f n \<in> S - {x})" "(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f n) x < e)" unfolding Lim_sequentially by auto
+ then obtain f::"nat\<Rightarrow>'a" where f:"(\<forall>n. f n \<in> S - {x})" "(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f n) x < e)" unfolding Lim_sequentially by auto
{ fix e::real assume "e>0"
then obtain N where "dist (f N) x < e" using f(2) by auto
moreover have "f N\<in>S" "f N \<noteq> x" using f(1) by auto
@@ -1294,44 +1378,43 @@
lemma Lim_linear: fixes f :: "('a \<Rightarrow> real^'n::finite)" and h :: "(real^'n \<Rightarrow> real^'m::finite)"
assumes "(f ---> l) net" "linear h"
shows "((\<lambda>x. h (f x)) ---> h l) net"
-proof (cases "trivial_limit net")
- case True
- thus ?thesis unfolding tendsto_def unfolding eventually_def by auto
-next
- case False note cas = this
- obtain b where b: "b>0" "\<forall>x. norm (h x) \<le> b * norm x" using assms(2) using linear_bounded_pos[of h] by auto
+proof -
+ obtain b where b: "b>0" "\<forall>x. norm (h x) \<le> b * norm x"
+ using assms(2) using linear_bounded_pos[of h] by auto
{ fix e::real assume "e >0"
hence "e/b > 0" using `b>0` by (metis divide_pos_pos)
- then have "(\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (f x) l < e/b))" using assms `e>0` cas
- unfolding tendsto_def unfolding eventually_def by auto
- then obtain y where y: "\<exists>x. netord net x y" "\<forall>x. netord net x y \<longrightarrow> dist (f x) l < e/b" by auto
- { fix x
- have "netord net x y \<longrightarrow> dist (h (f x)) (h l) < e"
- using y(2) b unfolding dist_norm using linear_sub[of h "f x" l] `linear h`
- apply auto by (metis b(1) b(2) dist_vector_def dist_commute less_le_not_le linorder_not_le mult_imp_div_pos_le real_mult_commute xt1(7)) (* FIXME: VERY slow! *)
- }
- hence " (\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (h (f x)) (h l) < e))" using y
- by(rule_tac x="y" in exI) auto
+ with `(f ---> l) net` have "eventually (\<lambda>x. dist (f x) l < e/b) net"
+ by (rule tendstoD)
+ then have "eventually (\<lambda>x. dist (h (f x)) (h l) < e) net"
+ apply (rule eventually_rev_mono [rule_format])
+ apply (simp add: dist_norm linear_sub [OF `linear h`, symmetric])
+ apply (rule le_less_trans [OF b(2) [rule_format]])
+ apply (simp add: pos_less_divide_eq `0 < b` mult_commute)
+ done
}
- thus ?thesis unfolding tendsto_def eventually_def using `b>0` by auto
+ thus ?thesis unfolding tendsto_def by simp
qed
lemma Lim_const: "((\<lambda>x. a) ---> a) net"
by (auto simp add: Lim trivial_limit_def)
-lemma Lim_cmul: "(f ---> l) net ==> ((\<lambda>x. c *s f x) ---> c *s l) net"
+lemma Lim_cmul:
+ fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
+ shows "(f ---> l) net ==> ((\<lambda>x. c *s f x) ---> c *s l) net"
apply (rule Lim_linear[where f = f])
apply simp
apply (rule linear_compose_cmul)
apply (rule linear_id[unfolded id_def])
done
-lemma Lim_neg: "(f ---> l) net ==> ((\<lambda>x. -(f x)) ---> -l) net"
+lemma Lim_neg:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+ shows "(f ---> l) net ==> ((\<lambda>x. -(f x)) ---> -l) net"
apply (simp add: Lim dist_norm group_simps)
apply (subst minus_diff_eq[symmetric])
unfolding norm_minus_cancel by simp
-lemma Lim_add: fixes f :: "'a \<Rightarrow> real^'n::finite" shows
+lemma Lim_add: fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" shows
"(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) + g(x)) ---> l + m) net"
proof-
assume as:"(f ---> l) net" "(g ---> m) net"
@@ -1341,34 +1424,32 @@
"eventually (\<lambda>x. dist (g x) m < e/2) net" using as
by (auto intro: tendstoD simp del: less_divide_eq_number_of1)
hence "eventually (\<lambda>x. dist (f x + g x) (l + m) < e) net"
- proof(cases "trivial_limit net")
- case True
- thus ?thesis unfolding eventually_def by auto
- next
- case False
- hence fl:"(\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (f x) l < e / 2))" and
- gl:"(\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (g x) m < e / 2))"
- using * unfolding eventually_def by auto
- obtain c where c:"(\<exists>x. netord net x c)" "(\<forall>x. netord net x c \<longrightarrow> dist (f x) l < e / 2 \<and> dist (g x) m < e / 2)"
- using net_dilemma[of net, OF fl gl] by auto
- { fix x assume "netord net x c"
- with c(2) have " dist (f x + g x) (l + m) < e" using dist_triangle_add[of "f x" "g x" l m] by auto
- }
- with c show ?thesis unfolding eventually_def by auto
- qed
+ apply (elim eventually_rev_mp)
+ apply (rule always_eventually, clarify)
+ apply (rule le_less_trans [OF dist_triangle_add])
+ apply simp
+ done
}
- thus ?thesis unfolding tendsto_def by auto
-qed
-
-lemma Lim_sub: "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
+ thus ?thesis unfolding tendsto_def by simp
+qed
+
+lemma Lim_sub:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+ shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
unfolding diff_minus
by (simp add: Lim_add Lim_neg)
-lemma Lim_null: "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
-lemma Lim_null_norm: "(f ---> 0) net \<longleftrightarrow> ((\<lambda>x. vec1(norm(f x))) ---> 0) net"
+lemma Lim_null:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+ shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
+
+lemma Lim_null_norm:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+ shows "(f ---> 0) net \<longleftrightarrow> ((\<lambda>x. vec1(norm(f x))) ---> 0) net"
by (simp add: Lim dist_norm norm_vec1)
lemma Lim_null_comparison:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes "eventually (\<lambda>x. norm(f x) <= g x) net" "((\<lambda>x. vec1(g x)) ---> 0) net"
shows "(f ---> 0) net"
proof(simp add: tendsto_def, rule+)
@@ -1386,24 +1467,27 @@
lemma Lim_component: "(f ---> l) net
==> ((\<lambda>a. vec1((f a :: real ^'n::finite)$i)) ---> vec1(l$i)) net"
- apply (simp add: Lim dist_norm vec1_sub[symmetric] norm_vec1 vector_minus_component[symmetric] del: vector_minus_component)
+ unfolding tendsto_def
+ apply (simp add: dist_norm vec1_sub[symmetric] norm_vec1 vector_minus_component[symmetric] del: vector_minus_component)
apply (auto simp del: vector_minus_component)
apply (erule_tac x=e in allE)
apply clarify
- apply (rule_tac x=y in exI)
+ apply (erule eventually_rev_mono)
apply (auto simp del: vector_minus_component)
apply (rule order_le_less_trans)
apply (rule component_le_norm)
by auto
lemma Lim_transform_bound:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+ fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net" "(g ---> 0) net"
shows "(f ---> 0) net"
proof(simp add: tendsto_def, rule+)
fix e::real assume "e>0"
{ fix x
assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
- hence "dist (f x) 0 < e" by norm}
+ hence "dist (f x) 0 < e" by (simp add: dist_norm)}
thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
using eventually_and[of "\<lambda>x. norm (f x) \<le> norm (g x)" "\<lambda>x. dist (g x) 0 < e" net]
using eventually_mono[of "\<lambda>x. norm (f x) \<le> norm (g x) \<and> dist (g x) 0 < e" "\<lambda>x. dist (f x) 0 < e" net]
@@ -1415,52 +1499,57 @@
lemma Lim_in_closed_set:
assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net" "\<not>(trivial_limit net)" "(f ---> l) net"
shows "l \<in> S"
-proof-
- { assume "l \<notin> S"
- obtain e where e:"e>0" "ball l e \<subseteq> UNIV - S" using assms(1) `l \<notin> S` unfolding closed_def open_contains_ball by auto
- hence *:"\<forall>x. dist l x < e \<longrightarrow> x \<notin> S" by auto
- obtain y where "(\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (f x) l < e)"
- using assms(3,4) `e>0` unfolding tendsto_def eventually_def by blast
- hence "(\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> f x \<notin> S)" using * by (auto simp add: dist_commute)
- hence False using assms(2,3)
- using eventually_and[of "(\<lambda>x. f x \<in> S)" "(\<lambda>x. f x \<notin> S)"] not_eventually[of "(\<lambda>x. f x \<in> S \<and> f x \<notin> S)" net]
- unfolding eventually_def by blast
- }
- thus ?thesis by blast
+proof (rule ccontr)
+ assume "l \<notin> S"
+ obtain e where e:"e>0" "ball l e \<subseteq> UNIV - S" using assms(1) `l \<notin> S` unfolding closed_def open_contains_ball by auto
+ hence *:"\<forall>x. dist l x < e \<longrightarrow> x \<notin> S" by auto
+ have "eventually (\<lambda>x. dist (f x) l < e) net"
+ using assms(4) `e>0` by (rule tendstoD)
+ with assms(2) have "eventually (\<lambda>x. f x \<in> S \<and> dist (f x) l < e) net"
+ by (rule eventually_conjI)
+ then obtain x where "f x \<in> S" "dist (f x) l < e"
+ using assms(3) eventually_happens by auto
+ with * show "False" by (simp add: dist_commute)
qed
text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *}
lemma Lim_norm_ubound:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
shows "norm(l) <= e"
-proof-
- obtain y where y: "\<exists>x. netord net x y" "\<forall>x. netord net x y \<longrightarrow> norm (f x) \<le> e" using assms(1,3) unfolding eventually_def by auto
- show ?thesis
- proof(rule ccontr)
- assume "\<not> norm l \<le> e"
- then obtain z where z: "\<exists>x. netord net x z" "\<forall>x. netord net x z \<longrightarrow> dist (f x) l < norm l - e"
- using assms(2)[unfolded Lim] using assms(1) apply simp apply(erule_tac x="norm l - e" in allE) by auto
- obtain w where w:"netord net w z" "netord net w y" using net[of net] using z(1) y(1) by blast
- hence "dist (f w) l < norm l - e \<and> norm (f w) <= e" using z(2) y(2) by auto
- thus False using `\<not> norm l \<le> e` by norm
- qed
+proof (rule ccontr)
+ assume "\<not> norm l \<le> e"
+ then have "0 < norm l - e" by simp
+ with assms(2) have "eventually (\<lambda>x. dist (f x) l < norm l - e) net"
+ by (rule tendstoD)
+ with assms(3) have "eventually (\<lambda>x. norm (f x) \<le> e \<and> dist (f x) l < norm l - e) net"
+ by (rule eventually_conjI)
+ then obtain w where "norm (f w) \<le> e" "dist (f w) l < norm l - e"
+ using assms(1) eventually_happens by auto
+ hence "norm (f w - l) < norm l - e" "norm (f w) \<le> e" by (simp_all add: dist_norm)
+ hence "norm (f w - l) + norm (f w) < norm l" by simp
+ hence "norm (f w - l - f w) < norm l" by (rule le_less_trans [OF norm_triangle_ineq4])
+ thus False using `\<not> norm l \<le> e` by simp
qed
lemma Lim_norm_lbound:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes "\<not> (trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. e <= norm(f x)) net"
shows "e \<le> norm l"
-proof-
- obtain y where y: "\<exists>x. netord net x y" "\<forall>x. netord net x y \<longrightarrow> e \<le> norm (f x)" using assms(1,3) unfolding eventually_def by auto
- show ?thesis
- proof(rule ccontr)
- assume "\<not> e \<le> norm l"
- then obtain z where z: "\<exists>x. netord net x z" "\<forall>x. netord net x z \<longrightarrow> dist (f x) l < e - norm l"
- using assms(2)[unfolded Lim] using assms(1) apply simp apply(erule_tac x="e - norm l" in allE) by auto
- obtain w where w:"netord net w z" "netord net w y" using net[of net] using z(1) y(1) by blast
- hence "dist (f w) l < e - norm l \<and> e \<le> norm (f w)" using z(2) y(2) by auto
- thus False using `\<not> e \<le> norm l` by norm
- qed
+proof (rule ccontr)
+ assume "\<not> e \<le> norm l"
+ then have "0 < e - norm l" by simp
+ with assms(2) have "eventually (\<lambda>x. dist (f x) l < e - norm l) net"
+ by (rule tendstoD)
+ with assms(3) have "eventually (\<lambda>x. e \<le> norm (f x) \<and> dist (f x) l < e - norm l) net"
+ by (rule eventually_conjI)
+ then obtain w where "e \<le> norm (f w)" "dist (f w) l < e - norm l"
+ using assms(1) eventually_happens by auto
+ hence "norm (f w - l) + norm l < e" "e \<le> norm (f w)" by (simp_all add: dist_norm)
+ hence "norm (f w - l) + norm l < norm (f w)" by (rule less_le_trans)
+ hence "norm (f w - l + l) < norm (f w)" by (rule le_less_trans [OF norm_triangle_ineq])
+ thus False by simp
qed
text{* Uniqueness of the limit, when nontrivial. *}
@@ -1482,7 +1571,8 @@
qed
lemma tendsto_Lim:
- "~(trivial_limit (net::('b::zero_neq_one net))) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
+ fixes f :: "'a::zero_neq_one \<Rightarrow> real ^ 'n::finite"
+ shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
unfolding Lim_def using Lim_unique[of net f] by auto
text{* Limit under bilinear function (surprisingly tedious, but important) *}
@@ -1521,10 +1611,7 @@
fixes net :: "'a net" and h:: "real ^'m::finite \<Rightarrow> real ^'n::finite \<Rightarrow> real ^'p::finite"
assumes "(f ---> l) net" and "(g ---> m) net" and "bilinear h"
shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net"
-proof(cases "trivial_limit net")
- case True thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net" unfolding Lim ..
-next
- case False note ntriv = this
+proof -
obtain B where "B>0" and B:"\<forall>x y. norm (h x y) \<le> B * norm x * norm y" using bilinear_bounded_pos[OF assms(3)] by auto
{ fix e::real assume "e>0"
obtain d where "d>0" and d:"\<forall>x' y'. norm (x' - l) < d \<and> norm (y' - m) < d \<longrightarrow> norm x' * norm (y' - m) + norm (x' - l) * norm m < e / B" using `B>0` `e>0`
@@ -1534,6 +1621,15 @@
unfolding bilinear_rsub[OF assms(3)]
unfolding bilinear_lsub[OF assms(3)] by auto
+ have "eventually (\<lambda>x. dist (f x) l < d) net"
+ using assms(1) `d>0` by (rule tendstoD)
+ moreover
+ have "eventually (\<lambda>x. dist (g x) m < d) net"
+ using assms(2) `d>0` by (rule tendstoD)
+ ultimately
+ have "eventually (\<lambda>x. dist (f x) l < d \<and> dist (g x) m < d) net"
+ by (rule eventually_conjI)
+ moreover
{ fix x assume "dist (f x) l < d \<and> dist (g x) m < d"
hence **:"norm (f x) * norm (g x - m) + norm (f x - l) * norm m < e / B"
using d[THEN spec[where x="f x"], THEN spec[where x="g x"]] unfolding dist_norm by auto
@@ -1543,11 +1639,11 @@
also have "\<dots> < e" using ** and `B>0` by(auto simp add: field_simps)
finally have "dist (h (f x) (g x)) (h l m) < e" unfolding dist_norm and * using norm_triangle_lt by auto
}
- moreover
- obtain c where "(\<exists>x. netord net x c) \<and> (\<forall>x. netord net x c \<longrightarrow> dist (f x) l < d \<and> dist (g x) m < d)"
- using net_dilemma[of net "\<lambda>x. dist (f x) l < d" "\<lambda>x. dist (g x) m < d"] using assms(1,2) unfolding Lim using False and `d>0` by (auto elim!: allE[where x=d])
- ultimately have "\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (h (f x) (g x)) (h l m) < e)" by auto }
- thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net" unfolding Lim by auto
+ ultimately have "eventually (\<lambda>x. dist (h (f x) (g x)) (h l m) < e) net"
+ by (auto elim: eventually_rev_mono)
+ }
+ thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net"
+ unfolding tendsto_def by simp
qed
text{* These are special for limits out of the same vector space. *}
@@ -1556,12 +1652,14 @@
lemma Lim_at_id: "(id ---> a) (at a)"
apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
-lemma Lim_at_zero: "(f ---> l) (at (a::real^'a::finite)) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
+lemma Lim_at_zero:
+ fixes a :: "'a::{real_normed_vector, perfect_space}"
+ shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
proof
assume "?lhs"
{ fix e::real assume "e>0"
with `?lhs` obtain d where d:"d>0" "\<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" unfolding Lim_at by auto
- { fix x::"real^'a" assume "0 < dist x 0 \<and> dist x 0 < d"
+ { fix x::"'a" assume "0 < dist x 0 \<and> dist x 0 < d"
hence "dist (f (a + x)) l < e" using d
apply(erule_tac x="x+a" in allE) by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
}
@@ -1573,7 +1671,7 @@
{ fix e::real assume "e>0"
with `?rhs` obtain d where d:"d>0" "\<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f (a + x)) l < e"
unfolding Lim_at by auto
- { fix x::"real^'a" assume "0 < dist x a \<and> dist x a < d"
+ { fix x::"'a" assume "0 < dist x a \<and> dist x a < d"
hence "dist (f x) l < e" using d apply(erule_tac x="x-a" in allE)
by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
}
@@ -1599,27 +1697,31 @@
ultimately show ?thesis unfolding netlimit_def using some_equality[of "\<lambda>x. \<forall>y. \<not> netord (at a within S) y x"] by blast
qed
-lemma netlimit_at:
- fixes a :: "real ^ 'n::finite"
- shows "netlimit(at a) = a"
+lemma netlimit_at: "netlimit (at a) = a"
apply (subst within_UNIV[symmetric])
using netlimit_within[of a UNIV]
by (simp add: trivial_limit_at within_UNIV)
text{* Transformation of limit. *}
-lemma Lim_transform: assumes "((\<lambda>x. f x - g x) ---> 0) net" "(f ---> l) net"
+lemma Lim_transform:
+ fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
+ assumes "((\<lambda>x. f x - g x) ---> 0) net" "(f ---> l) net"
shows "(g ---> l) net"
proof-
from assms have "((\<lambda>x. f x - g x - f x) ---> 0 - l) net" using Lim_sub[of "\<lambda>x. f x - g x" 0 net f l] by auto
thus "?thesis" using Lim_neg [of "\<lambda> x. - g x" "-l" net] by auto
qed
-lemma Lim_transform_eventually: "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
+lemma Lim_transform_eventually:
+ fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
+ (* FIXME: generalize to metric_space *)
+ shows "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
using Lim_eventually[of "\<lambda>x. f x - g x" 0 net] Lim_transform[of f g net l] by auto
lemma Lim_transform_within:
- fixes x :: "real ^ 'n::finite"
+ fixes f g :: "'a::perfect_space \<Rightarrow> 'b::real_normed_vector"
+ (* FIXME: generalize to metric_space *)
assumes "0 < d" "(\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x')"
"(f ---> l) (at x within S)"
shows "(g ---> l) (at x within S)"
@@ -1628,7 +1730,10 @@
thus ?thesis using Lim_transform[of f g "at x within S" l] using assms(3) by auto
qed
-lemma Lim_transform_at: "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
+lemma Lim_transform_at:
+ fixes f g :: "'a::perfect_space \<Rightarrow> 'b::real_normed_vector"
+ (* FIXME: generalize to metric_space *)
+ shows "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
(f ---> l) (at x) ==> (g ---> l) (at x)"
apply (subst within_UNIV[symmetric])
using Lim_transform_within[of d UNIV x f g l]
@@ -1637,7 +1742,8 @@
text{* Common case assuming being away from some crucial point like 0. *}
lemma Lim_transform_away_within:
- fixes f:: "real ^'m::finite \<Rightarrow> real ^'n::finite"
+ fixes f:: "'a::perfect_space \<Rightarrow> 'b::real_normed_vector"
+ (* FIXME: generalize to metric_space *)
assumes "a\<noteq>b" "\<forall>x\<in> S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
and "(f ---> l) (at a within S)"
shows "(g ---> l) (at a within S)"
@@ -1648,7 +1754,8 @@
qed
lemma Lim_transform_away_at:
- fixes f:: "real ^'m::finite \<Rightarrow> real ^'n::finite"
+ fixes f:: "'a::perfect_space \<Rightarrow> 'b::real_normed_vector"
+ (* FIXME: generalize to metric_space *)
assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
and fl: "(f ---> l) (at a)"
shows "(g ---> l) (at a)"
@@ -1658,7 +1765,8 @@
text{* Alternatively, within an open set. *}
lemma Lim_transform_within_open:
- fixes f:: "real ^'m::finite \<Rightarrow> real ^'n::finite"
+ fixes f:: "'a::perfect_space \<Rightarrow> 'b::real_normed_vector"
+ (* FIXME: generalize to metric_space *)
assumes "open S" "a \<in> S" "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x" "(f ---> l) (at a)"
shows "(g ---> l) (at a)"
proof-
@@ -1737,9 +1845,11 @@
text{* More properties of closed balls. *}
-lemma closed_cball: "closed(cball x e)"
+lemma closed_cball:
+ fixes x :: "'a::real_normed_vector" (* FIXME: generalize to metric_space *)
+ shows "closed (cball x e)"
proof-
- { fix xa::"nat\<Rightarrow>real^'a" and l assume as: "\<forall>n. dist x (xa n) \<le> e" "(xa ---> l) sequentially"
+ { fix xa::"nat\<Rightarrow>'a" and l assume as: "\<forall>n. dist x (xa n) \<le> e" "(xa ---> l) sequentially"
from as(2) have "((\<lambda>n. x - xa n) ---> x - l) sequentially" using Lim_sub[of "\<lambda>n. x" x sequentially xa l] Lim_const[of x sequentially] by auto
moreover from as(1) have "eventually (\<lambda>n. norm (x - xa n) \<le> e) sequentially" unfolding eventually_sequentially dist_norm by auto
ultimately have "dist x l \<le> e"
@@ -1764,10 +1874,16 @@
by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball mem_def)
lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
- apply (simp add: interior_def)
- by (metis open_contains_cball subset_trans ball_subset_cball centre_in_ball open_ball)
-
-lemma islimpt_ball: "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e" (is "?lhs = ?rhs")
+ apply (simp add: interior_def, safe)
+ apply (force simp add: open_contains_cball)
+ apply (rule_tac x="ball x e" in exI)
+ apply (simp add: open_ball centre_in_ball subset_trans [OF ball_subset_cball])
+ done
+
+lemma islimpt_ball:
+ fixes x y :: "'a::{real_normed_vector,perfect_space}"
+ (* FIXME: generalize to metric_space *)
+ shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e" (is "?lhs = ?rhs")
proof
assume "?lhs"
{ assume "e \<le> 0"
@@ -1790,38 +1906,41 @@
next
case False
- have "dist x (y - (d / (2 * dist y x)) *s (y - x))
- = norm (x - y + (d / (2 * norm (y - x))) *s (y - x))"
+ have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x))
+ = norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))"
unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[THEN sym] by auto
also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
- using vector_sadd_rdistrib[of "- 1" "d / (2 * norm (y - x))", THEN sym, of "y - x"]
- unfolding vector_smult_lneg vector_smult_lid
- by (auto simp add: norm_minus_commute)
+ using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", THEN sym, of "y - x"]
+ unfolding scaleR_minus_left scaleR_one
+ by (auto simp add: norm_minus_commute norm_scaleR)
also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
unfolding real_add_mult_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
also have "\<dots> \<le> e - d/2" using `d \<le> dist x y` and `d>0` and `?rhs` by(auto simp add: dist_norm)
- finally have "y - (d / (2 * dist y x)) *s (y - x) \<in> ball x e" using `d>0` by auto
+ finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using `d>0` by auto
moreover
- have "(d / (2*dist y x)) *s (y - x) \<noteq> 0"
- using `x\<noteq>y`[unfolded dist_nz] `d>0` unfolding vector_mul_eq_0 by (auto simp add: dist_commute)
+ have "(d / (2*dist y x)) *\<^sub>R (y - x) \<noteq> 0"
+ using `x\<noteq>y`[unfolded dist_nz] `d>0` unfolding scaleR_eq_0_iff by (auto simp add: dist_commute)
moreover
- have "dist (y - (d / (2 * dist y x)) *s (y - x)) y < d" unfolding dist_norm apply simp unfolding norm_minus_cancel norm_mul
+ have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d" unfolding dist_norm apply simp unfolding norm_minus_cancel norm_scaleR
using `d>0` `x\<noteq>y`[unfolded dist_nz] dist_commute[of x y]
unfolding dist_norm by auto
- ultimately show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d" by (rule_tac x="y - (d / (2*dist y x)) *s (y - x)" in bexI) auto
+ ultimately show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d" by (rule_tac x="y - (d / (2*dist y x)) *\<^sub>R (y - x)" in bexI) auto
qed
next
case False hence "d > dist x y" by auto
show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
proof(cases "x=y")
case True
- obtain z where **:"dist y z = (min e d) / 2" using vector_choose_dist[of "(min e d) / 2" y]
+ obtain z where **: "z \<noteq> y" "dist z y < min e d"
+ using perfect_choose_dist[of "min e d" y]
using `d > 0` `e>0` by auto
show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
- apply(rule_tac x=z in bexI) unfolding `x=y` dist_commute dist_nz using ** `d > 0` `e>0` by auto
+ unfolding `x = y`
+ using `z \<noteq> y` **
+ by (rule_tac x=z in bexI, auto simp add: dist_commute)
next
case False thus "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
using `d>0` `d > dist x y` `?rhs` by(rule_tac x=x in bexI, auto)
@@ -1830,11 +1949,16 @@
thus "?lhs" unfolding mem_cball islimpt_approachable mem_ball by auto
qed
-lemma closure_ball: "0 < e ==> (closure(ball x e) = cball x e)"
+lemma closure_ball:
+ fixes x y :: "'a::{real_normed_vector,perfect_space}"
+ (* FIXME: generalize to metric_space *)
+ shows "0 < e ==> (closure(ball x e) = cball x e)"
apply (simp add: closure_def islimpt_ball expand_set_eq)
by arith
-lemma interior_cball: "interior(cball x e) = ball x e"
+lemma interior_cball:
+ fixes x :: "real ^ _" (* FIXME: generalize *)
+ shows "interior(cball x e) = ball x e"
proof(cases "e\<ge>0")
case False note cs = this
from cs have "ball x e = {}" using ball_empty[of e x] by auto moreover
@@ -1880,12 +2004,16 @@
ultimately show ?thesis using interior_unique[of "ball x e" "cball x e"] using open_ball[of x e] by auto
qed
-lemma frontier_ball: "0 < e ==> frontier(ball a e) = {x. dist a x = e}"
+lemma frontier_ball:
+ fixes a :: "real ^ _" (* FIXME: generalize *)
+ shows "0 < e ==> frontier(ball a e) = {x. dist a x = e}"
apply (simp add: frontier_def closure_ball interior_open open_ball order_less_imp_le)
apply (simp add: expand_set_eq)
by arith
-lemma frontier_cball: "frontier(cball a e) = {x. dist a x = e}"
+lemma frontier_cball:
+ fixes a :: "real ^ _" (* FIXME: generalize *)
+ shows "frontier(cball a e) = {x. dist a x = e}"
apply (simp add: frontier_def interior_cball closed_cball closure_closed order_less_imp_le)
apply (simp add: expand_set_eq)
by arith
@@ -1895,7 +2023,9 @@
by (metis zero_le_dist dist_self order_less_le_trans)
lemma cball_empty: "e < 0 ==> cball x e = {}" by (simp add: cball_eq_empty)
-lemma cball_eq_sing: "(cball x e = {x}) \<longleftrightarrow> e = 0"
+lemma cball_eq_sing:
+ fixes x :: "real ^ _" (* FIXME: generalize *)
+ shows "(cball x e = {x}) \<longleftrightarrow> e = 0"
proof-
{ assume as:"\<forall>xa. (dist x xa \<le> e) = (xa = x)"
hence "e \<ge> 0" apply (erule_tac x=x in allE) by auto
@@ -1905,7 +2035,9 @@
thus ?thesis unfolding expand_set_eq mem_cball by (auto simp add: dist_nz)
qed
-lemma cball_sing: "e = 0 ==> cball x e = {x}" by (simp add: cball_eq_sing)
+lemma cball_sing:
+ fixes x :: "real ^ _" (* FIXME: generalize *)
+ shows "e = 0 ==> cball x e = {x}" by (simp add: cball_eq_sing)
text{* For points in the interior, localization of limits makes no difference. *}
@@ -1924,7 +2056,10 @@
lemma lim_within_interior: "x \<in> interior S ==> ((f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x))"
by (simp add: tendsto_def eventually_within_interior)
-lemma netlimit_within_interior: assumes "x \<in> interior S"
+lemma netlimit_within_interior:
+ fixes x :: "'a::{perfect_space, real_normed_vector}"
+ (* FIXME: generalize to perfect_space *)
+ assumes "x \<in> interior S"
shows "netlimit(at x within S) = x" (is "?lhs = ?rhs")
proof-
from assms obtain e::real where e:"e>0" "ball x e \<subseteq> S" using open_interior[of S] unfolding open_contains_ball using interior_subset[of S] by auto
@@ -1949,9 +2084,15 @@
from assms obtain a where a:"\<forall>x\<in>S. norm x \<le> a" unfolding bounded_def by auto
{ fix x assume "x\<in>closure S"
then obtain xa where xa:"\<forall>n. xa n \<in> S" "(xa ---> x) sequentially" unfolding closure_sequential by auto
- moreover have "\<exists>y. \<exists>x. netord sequentially x y" using trivial_limit_sequentially unfolding trivial_limit_def by blast
- hence "\<exists>y. (\<exists>x. netord sequentially x y) \<and> (\<forall>x. netord sequentially x y \<longrightarrow> norm (xa x) \<le> a)" unfolding sequentially_def using a xa(1) by auto
- ultimately have "norm x \<le> a" using Lim_norm_ubound[of sequentially xa x a] trivial_limit_sequentially unfolding eventually_def by auto
+ have "\<forall>n. xa n \<in> S \<longrightarrow> norm (xa n) \<le> a" using a by simp
+ hence "eventually (\<lambda>n. norm (xa n) \<le> a) sequentially"
+ by (rule eventually_mono, simp add: xa(1))
+ have "norm x \<le> a"
+ apply (rule Lim_norm_ubound[of sequentially xa x a])
+ apply (rule trivial_limit_sequentially)
+ apply (rule xa(2))
+ apply fact
+ done
}
thus ?thesis unfolding bounded_def by auto
qed
@@ -2270,16 +2411,14 @@
subsection{* Completeness. *}
- (* FIXME: Unify this with Cauchy from SEQ!!!!!*)
-
-definition
- cauchy :: "(nat \<Rightarrow> real ^ 'n::finite) \<Rightarrow> bool" where
- "cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
-
-definition complete_def:"complete s \<longleftrightarrow> (\<forall>f::(nat=>real^'a::finite). (\<forall>n. f n \<in> s) \<and> cauchy f
+lemma cauchy_def:
+ "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
+unfolding Cauchy_def by blast
+
+definition complete_def:"complete s \<longleftrightarrow> (\<forall>f::(nat=>real^'a::finite). (\<forall>n. f n \<in> s) \<and> Cauchy f
--> (\<exists>l \<in> s. (f ---> l) sequentially))"
-lemma cauchy: "cauchy s \<longleftrightarrow> (\<forall>e>0.\<exists> N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
+lemma cauchy: "Cauchy s \<longleftrightarrow> (\<forall>e>0.\<exists> N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
proof-
{ assume ?rhs
{ fix e::real
@@ -2306,20 +2445,20 @@
qed
lemma convergent_imp_cauchy:
- "(s ---> l) sequentially ==> cauchy s"
+ "(s ---> l) sequentially ==> Cauchy s"
proof(simp only: cauchy_def, rule, rule)
fix e::real assume "e>0" "(s ---> l) sequentially"
then obtain N::nat where N:"\<forall>n\<ge>N. dist (s n) l < e/2" unfolding Lim_sequentially by(erule_tac x="e/2" in allE) auto
thus "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e" using dist_triangle_half_l[of _ l e _] by (rule_tac x=N in exI) auto
qed
-lemma cauchy_imp_bounded: assumes "cauchy s" shows "bounded {y. (\<exists>n::nat. y = s n)}"
+lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded {y. (\<exists>n::nat. y = s n)}"
proof-
from assms obtain N::nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1" unfolding cauchy_def apply(erule_tac x= 1 in allE) by auto
hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
{ fix n::nat assume "n\<ge>N"
hence "norm (s n) \<le> norm (s N) + 1" using N apply(erule_tac x=n in allE) unfolding dist_norm
- using norm_triangle_sub[of "s N" "s n"] by (auto, metis dist_vector_def dist_commute le_add_right_mono norm_triangle_sub real_less_def)
+ using norm_triangle_sub[of "s N" "s n"] by (auto, metis norm_minus_commute le_add_right_mono norm_triangle_sub real_less_def)
}
hence "\<forall>n\<ge>N. norm (s n) \<le> norm (s N) + 1" by auto
moreover
@@ -2332,7 +2471,7 @@
lemma compact_imp_complete: assumes "compact s" shows "complete s"
proof-
- { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "cauchy f"
+ { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
from as(1) obtain l r where lr: "l\<in>s" "(\<forall>m n. m < n \<longrightarrow> r m < r n)" "((f \<circ> r) ---> l) sequentially" using assms unfolding compact_def by blast
{ fix n :: nat have lr':"n \<le> r n"
@@ -2358,11 +2497,11 @@
lemma complete_univ:
"complete UNIV"
proof(simp add: complete_def, rule, rule)
- fix f::"nat \<Rightarrow> real^'n::finite" assume "cauchy f"
+ fix f::"nat \<Rightarrow> real^'n::finite" assume "Cauchy f"
hence "bounded (f`UNIV)" using cauchy_imp_bounded[of f] unfolding image_def by auto
hence "compact (closure (f`UNIV))" using bounded_closed_imp_compact[of "closure (range f)"] by auto
hence "complete (closure (range f))" using compact_imp_complete by auto
- thus "\<exists>l. (f ---> l) sequentially" unfolding complete_def[of "closure (range f)"] using `cauchy f` unfolding closure_def by auto
+ thus "\<exists>l. (f ---> l) sequentially" unfolding complete_def[of "closure (range f)"] using `Cauchy f` unfolding closure_def by auto
qed
lemma complete_eq_closed: "complete s \<longleftrightarrow> closed s" (is "?lhs = ?rhs")
@@ -2375,13 +2514,15 @@
thus ?rhs unfolding closed_limpt by auto
next
assume ?rhs
- { fix f assume as:"\<forall>n::nat. f n \<in> s" "cauchy f"
+ { fix f assume as:"\<forall>n::nat. f n \<in> s" "Cauchy f"
then obtain l where "(f ---> l) sequentially" using complete_univ[unfolded complete_def, THEN spec[where x=f]] by auto
hence "\<exists>l\<in>s. (f ---> l) sequentially" using `?rhs`[unfolded closed_sequential_limits, THEN spec[where x=f], THEN spec[where x=l]] using as(1) by auto }
thus ?lhs unfolding complete_def by auto
qed
-lemma convergent_eq_cauchy: "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> cauchy s" (is "?lhs = ?rhs")
+lemma convergent_eq_cauchy:
+ fixes s :: "nat \<Rightarrow> real ^ 'n::finite"
+ shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s" (is "?lhs = ?rhs")
proof
assume ?lhs then obtain l where "(s ---> l) sequentially" by auto
thus ?rhs using convergent_imp_cauchy by auto
@@ -2420,7 +2561,7 @@
qed }
hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)" by blast+
then obtain l r where "l\<in>s" and r:"\<forall>m n. m < n \<longrightarrow> r m < r n" and "((x \<circ> r) ---> l) sequentially" using assms(1)[unfolded compact_def, THEN spec[where x=x]] by auto
- from this(3) have "cauchy (x \<circ> r)" using convergent_imp_cauchy by auto
+ from this(3) have "Cauchy (x \<circ> r)" using convergent_imp_cauchy by auto
then obtain N::nat where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e" unfolding cauchy_def using `e>0` by auto
show False
using N[THEN spec[where x=N], THEN spec[where x="N+1"]]
@@ -2614,6 +2755,7 @@
qed
lemma bolzano_weierstrass_imp_closed:
+ fixes s :: "(real ^ 'n::finite) set"
assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
shows "closed s"
proof-
@@ -2710,7 +2852,8 @@
qed
lemma finite_imp_closed:
- "finite s ==> closed s"
+ fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+ shows "finite s ==> closed s"
proof-
assume "finite s" hence "\<not>( \<exists>t. t \<subseteq> s \<and> infinite t)" using finite_subset by auto
thus ?thesis using bolzano_weierstrass_imp_closed[of s] by auto
@@ -2728,7 +2871,8 @@
by blast
lemma closed_sing[simp]:
- "closed {a}"
+ fixes a :: "real ^ _" (* FIXME: generalize *)
+ shows "closed {a}"
using compact_eq_bounded_closed compact_sing[of a]
by blast
@@ -2754,7 +2898,8 @@
by blast
lemma open_delete:
- "open s ==> open(s - {x})"
+ fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+ shows "open s ==> open(s - {x})"
using open_diff[of s "{x}"] closed_sing
by blast
@@ -2824,7 +2969,7 @@
}
hence "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (t m) (t n) < e" by auto
}
- hence "cauchy t" unfolding cauchy_def by auto
+ hence "Cauchy t" unfolding cauchy_def by auto
then obtain l where l:"(t ---> l) sequentially" using complete_univ unfolding complete_def by auto
{ fix n::nat
{ fix e::real assume "e>0"
@@ -2876,7 +3021,7 @@
thus ?rhs by auto
next
assume ?rhs
- hence "\<forall>x. P x \<longrightarrow> cauchy (\<lambda>n. s n x)" unfolding cauchy_def apply auto by (erule_tac x=e in allE)auto
+ hence "\<forall>x. P x \<longrightarrow> Cauchy (\<lambda>n. s n x)" unfolding cauchy_def apply auto by (erule_tac x=e in allE)auto
then obtain l where l:"\<forall>x. P x \<longrightarrow> ((\<lambda>n. s n x) ---> l x) sequentially" unfolding convergent_eq_cauchy[THEN sym]
using choice[of "\<lambda>x l. P x \<longrightarrow> ((\<lambda>n. s n x) ---> l) sequentially"] by auto
{ fix e::real assume "e>0"
@@ -2913,17 +3058,16 @@
lemma continuous_trivial_limit:
"trivial_limit net ==> continuous net f"
- unfolding continuous_def tendsto_def eventually_def by auto
+ unfolding continuous_def tendsto_def trivial_limit_eq by auto
lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f(x)) (at x within s)"
unfolding continuous_def
unfolding tendsto_def
using netlimit_within[of x s]
- unfolding eventually_def
- by (cases "trivial_limit (at x within s)") auto
-
-lemma continuous_at: "continuous (at x) f \<longleftrightarrow> (f ---> f(x)) (at x)" using within_UNIV[of x]
- using continuous_within[of x UNIV f] by auto
+ by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually)
+
+lemma continuous_at: "continuous (at x) f \<longleftrightarrow> (f ---> f(x)) (at x)"
+ using continuous_within [of x UNIV f] by (simp add: within_UNIV)
lemma continuous_at_within:
assumes "continuous (at x) f" shows "continuous (at x within s) f"
@@ -2969,8 +3113,8 @@
apply (auto simp add: dist_commute) apply(erule_tac x=e in allE) by auto
qed
-lemma continuous_at_ball: fixes f::"real^'a::finite \<Rightarrow> real^'a"
- shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f ` (ball x d) \<subseteq> ball (f x) e)" (is "?lhs = ?rhs")
+lemma continuous_at_ball:
+ "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f ` (ball x d) \<subseteq> ball (f x) e)" (is "?lhs = ?rhs")
proof
assume ?lhs thus ?rhs unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
apply auto apply(erule_tac x=e in allE) apply auto apply(rule_tac x=d in exI) apply auto apply(erule_tac x=xa in allE) apply (auto simp add: dist_commute dist_nz)
@@ -3072,7 +3216,7 @@
--> ((f o x) ---> f a) sequentially)" (is "?lhs = ?rhs")
proof
assume ?lhs
- { fix x::"nat \<Rightarrow> real^'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (x n) a < e"
+ { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (x n) a < e"
fix e::real assume "e>0"
from `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e" unfolding continuous_within Lim_within using `e>0` by auto
from x(2) `d>0` obtain N where N:"\<forall>n\<ge>N. dist (x n) a < d" by auto
@@ -3166,6 +3310,7 @@
text{* The usual transformation theorems. *}
lemma continuous_transform_within:
+ fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
assumes "0 < d" "x \<in> s" "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
"continuous (at x within s) f"
shows "continuous (at x within s) g"
@@ -3181,6 +3326,7 @@
qed
lemma continuous_transform_at:
+ fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
assumes "0 < d" "\<forall>x'. dist x' x < d --> f x' = g x'"
"continuous (at x) f"
shows "continuous (at x) g"
@@ -3200,25 +3346,27 @@
text{* Combination results for pointwise continuity. *}
lemma continuous_const: "continuous net (\<lambda>x::'a::zero_neq_one. c)"
- by(auto simp add: continuous_def Lim_const)
+ by (auto simp add: continuous_def Lim_const)
lemma continuous_cmul:
- "continuous net f ==> continuous net (\<lambda>x. c *s f x)"
- by(auto simp add: continuous_def Lim_cmul)
+ fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
+ shows "continuous net f ==> continuous net (\<lambda>x. c *s f x)"
+ by (auto simp add: continuous_def Lim_cmul)
lemma continuous_neg:
- "continuous net f ==> continuous net (\<lambda>x. -(f x))"
- by(auto simp add: continuous_def Lim_neg)
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+ shows "continuous net f ==> continuous net (\<lambda>x. -(f x))"
+ by (auto simp add: continuous_def Lim_neg)
lemma continuous_add:
- "continuous net f \<Longrightarrow> continuous net g
- ==> continuous net (\<lambda>x. f x + g x)"
- by(auto simp add: continuous_def Lim_add)
+ fixes f g :: "'a \<Rightarrow> 'b::real_normed_vector"
+ shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x + g x)"
+ by (auto simp add: continuous_def Lim_add)
lemma continuous_sub:
- "continuous net f \<Longrightarrow> continuous net g
- ==> continuous net (\<lambda>x. f(x) - g(x))"
- by(auto simp add: continuous_def Lim_sub)
+ fixes f g :: "'a \<Rightarrow> 'b::real_normed_vector"
+ shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x - g x)"
+ by (auto simp add: continuous_def Lim_sub)
text{* Same thing for setwise continuity. *}
@@ -3476,11 +3624,13 @@
qed
lemma continuous_open_preimage_univ:
- "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
+ fixes f :: "real ^ _ \<Rightarrow> real ^ _" (* FIXME: generalize *)
+ shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
lemma continuous_closed_preimage_univ:
- "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
+ fixes f :: "real ^ _ \<Rightarrow> real ^ _" (* FIXME: generalize *)
+ shows "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
text{* Equality of continuous functions on closure and related results. *}
@@ -3574,6 +3724,7 @@
text{* Some arithmetical combinations (more to prove). *}
lemma open_scaling[intro]:
+ fixes s :: "(real ^ _) set"
assumes "c \<noteq> 0" "open s"
shows "open((\<lambda>x. c *s x) ` s)"
proof-
@@ -3591,9 +3742,11 @@
qed
lemma open_negations:
- "open s ==> open ((\<lambda> x. -x) ` s)" unfolding pth_3 by auto
+ fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+ shows "open s ==> open ((\<lambda> x. -x) ` s)" unfolding pth_3 by auto
lemma open_translation:
+ fixes s :: "(real ^ _) set" (* FIXME: generalize *)
assumes "open s" shows "open((\<lambda>x. a + x) ` s)"
proof-
{ fix x have "continuous (at x) (\<lambda>x. x - a)" using continuous_sub[of "at x" "\<lambda>x. x" "\<lambda>x. a"] continuous_at_id[of x] continuous_const[of "at x" a] by auto }
@@ -3602,6 +3755,7 @@
qed
lemma open_affinity:
+ fixes s :: "(real ^ _) set"
assumes "open s" "c \<noteq> 0"
shows "open ((\<lambda>x. a + c *s x) ` s)"
proof-
@@ -3610,7 +3764,9 @@
thus ?thesis using assms open_translation[of "op *s c ` s" a] unfolding * by auto
qed
-lemma interior_translation: "interior ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (interior s)"
+lemma interior_translation:
+ fixes s :: "'a::real_normed_vector set"
+ shows "interior ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (interior s)"
proof (rule set_ext, rule)
fix x assume "x \<in> interior (op + a ` s)"
then obtain e where "e>0" and e:"ball x e \<subseteq> op + a ` s" unfolding mem_interior by auto
@@ -3757,12 +3913,14 @@
qed
lemma linear_continuous_at:
+ fixes f :: "real ^ _ \<Rightarrow> real ^ _"
assumes "linear f" shows "continuous (at a) f"
unfolding continuous_at Lim_at_zero[of f "f a" a] using linear_lim_0[OF assms]
unfolding Lim_null[of "\<lambda>x. f (a + x)"] unfolding linear_sub[OF assms, THEN sym] by auto
lemma linear_continuous_within:
- "linear f ==> continuous (at x within s) f"
+ fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+ shows "linear f ==> continuous (at x within s) f"
using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
lemma linear_continuous_on:
@@ -3772,12 +3930,14 @@
text{* Also bilinear functions, in composition form. *}
lemma bilinear_continuous_at_compose:
- "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bilinear h
+ fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+ shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bilinear h
==> continuous (at x) (\<lambda>x. h (f x) (g x))"
unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto
lemma bilinear_continuous_within_compose:
- "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bilinear h
+ fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+ shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bilinear h
==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
@@ -3791,16 +3951,19 @@
lemma open_vec1:
+ fixes s :: "real set" shows
"open(vec1 ` s) \<longleftrightarrow>
(\<forall>x \<in> s. \<exists>e>0. \<forall>x'. abs(x' - x) < e --> x' \<in> s)" (is "?lhs = ?rhs")
unfolding open_def apply simp unfolding forall_vec1 dist_vec1 vec1_in_image_vec1 by simp
lemma islimpt_approachable_vec1:
+ fixes s :: "real set" shows
"(vec1 x) islimpt (vec1 ` s) \<longleftrightarrow>
(\<forall>e>0. \<exists>x'\<in> s. x' \<noteq> x \<and> abs(x' - x) < e)"
by (auto simp add: islimpt_approachable dist_vec1 vec1_eq)
lemma closed_vec1:
+ fixes s :: "real set" shows
"closed (vec1 ` s) \<longleftrightarrow>
(\<forall>x. (\<forall>e>0. \<exists>x' \<in> s. x' \<noteq> x \<and> abs(x' - x) < e)
--> x \<in> s)"
@@ -3808,7 +3971,8 @@
unfolding dist_vec1 vec1_in_image_vec1 abs_minus_commute by auto
lemma continuous_at_vec1_range:
- "continuous (at x) (vec1 o f) \<longleftrightarrow> (\<forall>e>0. \<exists>d>0.
+ fixes f :: "real ^ _ \<Rightarrow> real"
+ shows "continuous (at x) (vec1 o f) \<longleftrightarrow> (\<forall>e>0. \<exists>d>0.
\<forall>x'. norm(x' - x) < d --> abs(f x' - f x) < e)"
unfolding continuous_at unfolding Lim_at apply simp unfolding dist_vec1 unfolding dist_nz[THEN sym] unfolding dist_norm apply auto
apply(erule_tac x=e in allE) apply auto apply (rule_tac x=d in exI) apply auto apply (erule_tac x=x' in allE) apply auto
@@ -3819,7 +3983,8 @@
unfolding continuous_on_def apply (simp del: dist_commute) unfolding dist_vec1 unfolding dist_norm ..
lemma continuous_at_vec1_norm:
- "continuous (at x) (vec1 o norm)"
+ fixes x :: "real ^ _"
+ shows "continuous (at x) (vec1 o norm)"
unfolding continuous_at_vec1_range using real_abs_sub_norm order_le_less_trans by blast
lemma continuous_on_vec1_norm:
@@ -3909,6 +4074,7 @@
text{* For *minimal* distance, we only need closure, not compactness. *}
lemma distance_attains_inf:
+ fixes a :: "real ^ _" (* FIXME: generalize *)
assumes "closed s" "s \<noteq> {}"
shows "\<exists>x \<in> s. \<forall>y \<in> s. dist a x \<le> dist a y"
proof-
@@ -3933,6 +4099,7 @@
subsection{* We can now extend limit compositions to consider the scalar multiplier. *}
lemma Lim_mul:
+ fixes f :: "'a \<Rightarrow> real ^ _"
assumes "((vec1 o c) ---> vec1 d) net" "(f ---> l) net"
shows "((\<lambda>x. c(x) *s f x) ---> (d *s l)) net"
proof-
@@ -3943,15 +4110,18 @@
qed
lemma Lim_vmul:
- "((vec1 o c) ---> vec1 d) net ==> ((\<lambda>x. c(x) *s v) ---> d *s v) net"
+ fixes c :: "'a \<Rightarrow> real"
+ shows "((vec1 o c) ---> vec1 d) net ==> ((\<lambda>x. c(x) *s v) ---> d *s v) net"
using Lim_mul[of c d net "\<lambda>x. v" v] using Lim_const[of v] by auto
lemma continuous_vmul:
- "continuous net (vec1 o c) ==> continuous net (\<lambda>x. c(x) *s v)"
+ fixes c :: "'a \<Rightarrow> real"
+ shows "continuous net (vec1 o c) ==> continuous net (\<lambda>x. c(x) *s v)"
unfolding continuous_def using Lim_vmul[of c] by auto
lemma continuous_mul:
- "continuous net (vec1 o c) \<Longrightarrow> continuous net f
+ fixes c :: "'a \<Rightarrow> real"
+ shows "continuous net (vec1 o c) \<Longrightarrow> continuous net f
==> continuous net (\<lambda>x. c(x) *s f x) "
unfolding continuous_def using Lim_mul[of c] by auto
@@ -3967,19 +4137,18 @@
text{* And so we have continuity of inverse. *}
lemma Lim_inv:
+ fixes f :: "'a \<Rightarrow> real"
assumes "((vec1 o f) ---> vec1 l) (net::'a net)" "l \<noteq> 0"
shows "((vec1 o inverse o f) ---> vec1(inverse l)) net"
-proof(cases "trivial_limit net")
- case True thus ?thesis unfolding tendsto_def unfolding eventually_def by auto
-next
- case False note ntriv = this
+proof -
{ fix e::real assume "e>0"
- hence "0 < min (\<bar>l\<bar> / 2) (l\<twosuperior> * e / 2)" using `l\<noteq>0` mult_pos_pos[of "l^2" "e/2"] by auto
- then obtain y where y1:"\<exists>x. netord net x y" and
- y:"\<forall>x. netord net x y \<longrightarrow> dist ((vec1 \<circ> f) x) (vec1 l) < min (\<bar>l\<bar> / 2) (l\<twosuperior> * e / 2)" using ntriv
- using assms(1)[unfolded tendsto_def eventually_def, THEN spec[where x="min (abs l / 2) (l ^ 2 * e / 2)"]] by auto
- { fix x assume "netord net x y"
- hence *:"\<bar>f x - l\<bar> < min (\<bar>l\<bar> / 2) (l\<twosuperior> * e / 2)" using y[THEN spec[where x=x]] unfolding o_def dist_vec1 by auto
+ let ?d = "min (\<bar>l\<bar> / 2) (l\<twosuperior> * e / 2)"
+ have "0 < ?d" using `l\<noteq>0` `e>0` mult_pos_pos[of "l^2" "e/2"] by auto
+ with assms(1) have "eventually (\<lambda>x. dist ((vec1 o f) x) (vec1 l) < ?d) net"
+ by (rule tendstoD)
+ moreover
+ { fix x assume "dist ((vec1 o f) x) (vec1 l) < ?d"
+ hence *:"\<bar>f x - l\<bar> < min (\<bar>l\<bar> / 2) (l\<twosuperior> * e / 2)" unfolding o_def dist_vec1 by auto
hence fx0:"f x \<noteq> 0" using `l \<noteq> 0` by auto
hence fxl0: "(f x) * l \<noteq> 0" using `l \<noteq> 0` by auto
from * have **:"\<bar>f x - l\<bar> < l\<twosuperior> * e / 2" by auto
@@ -3996,31 +4165,33 @@
unfolding divide_divide_eq_left
unfolding nonzero_abs_divide[OF fxl0]
using mult_less_le_imp_less[OF **, of "inverse \<bar>f x * l\<bar>", of "inverse (l^2 / 2)"] using *** using fx0 `l\<noteq>0`
- unfolding inverse_eq_divide using `e>0` by auto }
- hence "(\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist ((vec1 \<circ> inverse \<circ> f) x) (vec1 (inverse l)) < e))"
- using y1 by auto }
- thus ?thesis unfolding tendsto_def eventually_def by auto
+ unfolding inverse_eq_divide using `e>0` by auto
+ }
+ ultimately
+ have "eventually (\<lambda>x. dist ((vec1 o inverse o f) x) (vec1(inverse l)) < e) net"
+ by (auto elim: eventually_rev_mono)
+ }
+ thus ?thesis unfolding tendsto_def by auto
qed
lemma continuous_inv:
- "continuous net (vec1 o f) \<Longrightarrow> f(netlimit net) \<noteq> 0
+ fixes f :: "'a \<Rightarrow> real"
+ shows "continuous net (vec1 o f) \<Longrightarrow> f(netlimit net) \<noteq> 0
==> continuous net (vec1 o inverse o f)"
unfolding continuous_def using Lim_inv by auto
lemma continuous_at_within_inv:
+ fixes f :: "real ^ _ \<Rightarrow> real"
assumes "continuous (at a within s) (vec1 o f)" "f a \<noteq> 0"
shows "continuous (at a within s) (vec1 o inverse o f)"
-proof(cases "trivial_limit (at a within s)")
- case True thus ?thesis unfolding continuous_def tendsto_def eventually_def by auto
-next
- case False note cs = this
- thus ?thesis using netlimit_within[OF cs] assms(2) continuous_inv[OF assms(1)] by auto
-qed
+ using assms unfolding continuous_within o_apply
+ by (rule Lim_inv)
lemma continuous_at_inv:
- "continuous (at a) (vec1 o f) \<Longrightarrow> f a \<noteq> 0
+ fixes f :: "real ^ _ \<Rightarrow> real"
+ shows "continuous (at a) (vec1 o f) \<Longrightarrow> f a \<noteq> 0
==> continuous (at a) (vec1 o inverse o f) "
- using within_UNIV[THEN sym, of a] using continuous_at_within_inv[of a UNIV] by auto
+ using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto
subsection{* Preservation properties for pasted sets. *}
@@ -4036,6 +4207,7 @@
qed
lemma closed_pastecart:
+ fixes s :: "(real ^ 'a::finite) set" (* FIXME: generalize *)
assumes "closed s" "closed t"
shows "closed {pastecart x y | x y . x \<in> s \<and> y \<in> t}"
proof-
@@ -4178,6 +4350,7 @@
text{* Related results with closure as the conclusion. *}
lemma closed_scaling:
+ fixes s :: "(real ^ _) set"
assumes "closed s" shows "closed ((\<lambda>x. c *s x) ` s)"
proof(cases "s={}")
case True thus ?thesis by auto
@@ -4205,6 +4378,7 @@
qed
lemma closed_negations:
+ fixes s :: "(real ^ _) set" (* FIXME: generalize *)
assumes "closed s" shows "closed ((\<lambda>x. -x) ` s)"
using closed_scaling[OF assms, of "-1"] unfolding pth_3 by auto
@@ -4255,6 +4429,7 @@
qed
lemma closed_translation:
+ fixes s :: "(real ^ _) set" (* FIXME: generalize *)
assumes "closed s" shows "closed ((\<lambda>x. a + x) ` s)"
proof-
have "{a + y |y. y \<in> s} = (op + a ` s)" by auto
@@ -4268,20 +4443,23 @@
lemma translation_diff: "(\<lambda>x::real^'a. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)" by auto
lemma closure_translation:
- "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
+ fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+ shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
proof-
have *:"op + a ` (UNIV - s) = UNIV - op + a ` s" apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto
show ?thesis unfolding closure_interior translation_diff translation_UNIV using interior_translation[of a "UNIV - s"] unfolding * by auto
qed
lemma frontier_translation:
- "frontier((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (frontier s)"
+ fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+ shows "frontier((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (frontier s)"
unfolding frontier_def translation_diff interior_translation closure_translation by auto
subsection{* Separation between points and sets. *}
lemma separate_point_closed:
- "closed s \<Longrightarrow> a \<notin> s ==> (\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x)"
+ fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+ shows "closed s \<Longrightarrow> a \<notin> s ==> (\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x)"
proof(cases "s = {}")
case True
thus ?thesis by(auto intro!: exI[where x=1])
@@ -4682,11 +4860,13 @@
using bounded_subset_closed_interval_symmetric[of s] by auto
lemma frontier_closed_interval:
- "frontier {a .. b} = {a .. b} - {a<..<b}"
+ fixes a b :: "real ^ _"
+ shows "frontier {a .. b} = {a .. b} - {a<..<b}"
unfolding frontier_def unfolding interior_closed_interval and closure_closed[OF closed_interval] ..
lemma frontier_open_interval:
- "frontier {a<..<b} = (if {a<..<b} = {} then {} else {a .. b} - {a<..<b})"
+ fixes a b :: "real ^ _"
+ shows "frontier {a<..<b} = (if {a<..<b} = {} then {} else {a .. b} - {a<..<b})"
proof(cases "{a<..<b} = {}")
case True thus ?thesis using frontier_empty by auto
next
@@ -4738,7 +4918,7 @@
using set_eq_subset[of "{a .. b}" "{c .. d}"]
using subset_interval_1(1)[of a b c d]
using subset_interval_1(1)[of c d a b]
-by auto
+by auto (* FIXME: slow *)
lemma disjoint_interval_1: fixes a :: "real^1" shows
"{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d < dest_vec1 c \<or> dest_vec1 b < dest_vec1 c \<or> dest_vec1 d < dest_vec1 a"
@@ -4808,20 +4988,27 @@
next
case False
{ fix e::real
- assume "0 < e" "\<forall>e>0. \<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist l (f x) < e)"
- then obtain x y where x:"netord net x y" and y:"\<forall>x. netord net x y \<longrightarrow> dist l (f x) < e / norm a" apply(erule_tac x="e / norm a" in allE) apply auto using False using norm_ge_zero[of a] apply auto
- using divide_pos_pos[of e "norm a"] by auto
- { fix z assume "netord net z y" hence "dist l (f z) < e / norm a" using y by blast
- hence "norm a * norm (l - f z) < e" unfolding dist_norm and
+ assume "0 < e"
+ with `a \<noteq> vec 0` have "0 < e / norm a" by (simp add: divide_pos_pos)
+ with assms(1) have "eventually (\<lambda>x. dist (f x) l < e / norm a) net"
+ by (rule tendstoD)
+ moreover
+ { fix z assume "dist (f z) l < e / norm a"
+ hence "norm a * norm (f z - l) < e" unfolding dist_norm and
pos_less_divide_eq[OF False[unfolded vec_0 zero_less_norm_iff[of a, THEN sym]]] and real_mult_commute by auto
- hence "\<bar>a \<bullet> l - a \<bullet> f z\<bar> < e" using order_le_less_trans[OF norm_cauchy_schwarz_abs[of a "l - f z"], of e] unfolding dot_rsub[symmetric] by auto }
- hence "\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> \<bar>a \<bullet> l - a \<bullet> f x\<bar> < e)" using x by auto }
- thus ?thesis using assms unfolding Lim apply (auto simp add: dist_commute)
- unfolding dist_vec1 by auto
+ hence "\<bar>a \<bullet> f z - a \<bullet> l\<bar> < e"
+ using order_le_less_trans[OF norm_cauchy_schwarz_abs[of a "f z - l"], of e]
+ unfolding dot_rsub[symmetric] by auto }
+ ultimately have "eventually (\<lambda>x. \<bar>a \<bullet> f x - a \<bullet> l\<bar> < e) net"
+ by (auto elim: eventually_rev_mono)
+ }
+ thus ?thesis unfolding tendsto_def
+ by (auto simp add: dist_vec1)
qed
lemma continuous_at_vec1_dot:
- "continuous (at x) (vec1 o (\<lambda>y. a \<bullet> y))"
+ fixes x :: "real ^ _"
+ shows "continuous (at x) (vec1 o (\<lambda>y. a \<bullet> y))"
proof-
have "((\<lambda>x. x) ---> x) (at x)" unfolding Lim_at by auto
thus ?thesis unfolding continuous_at and o_def using Lim_vec1_dot[of "\<lambda>x. x" x "at x" a] by auto
@@ -4848,10 +5035,10 @@
thus ?thesis unfolding closed_closedin[THEN sym] and * by auto
qed
-lemma closed_halfspace_ge: "closed {x. a \<bullet> x \<ge> b}"
+lemma closed_halfspace_ge: "closed {x::real^_. a \<bullet> x \<ge> b}"
using closed_halfspace_le[of "-a" "-b"] unfolding dot_lneg by auto
-lemma closed_hyperplane: "closed {x. a \<bullet> x = b}"
+lemma closed_hyperplane: "closed {x::real^_. a \<bullet> x = b}"
proof-
have "{x. a \<bullet> x = b} = {x. a \<bullet> x \<ge> b} \<inter> {x. a \<bullet> x \<le> b}" by auto
thus ?thesis using closed_halfspace_le[of a b] and closed_halfspace_ge[of b a] using closed_Int by auto
@@ -4867,13 +5054,13 @@
text{* Openness of halfspaces. *}
-lemma open_halfspace_lt: "open {x. a \<bullet> x < b}"
+lemma open_halfspace_lt: "open {x::real^_. a \<bullet> x < b}"
proof-
have "UNIV - {x. b \<le> a \<bullet> x} = {x. a \<bullet> x < b}" by auto
thus ?thesis using closed_halfspace_ge[unfolded closed_def, of b a] by auto
qed
-lemma open_halfspace_gt: "open {x. a \<bullet> x > b}"
+lemma open_halfspace_gt: "open {x::real^_. a \<bullet> x > b}"
proof-
have "UNIV - {x. b \<ge> a \<bullet> x} = {x. a \<bullet> x > b}" by auto
thus ?thesis using closed_halfspace_le[unfolded closed_def, of a b] by auto
@@ -5145,8 +5332,9 @@
text{* "Isometry" (up to constant bounds) of injective linear map etc. *}
lemma cauchy_isometric:
- assumes e:"0 < e" and s:"subspace s" and f:"linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and xs:"\<forall>n::nat. x n \<in> s" and cf:"cauchy(f o x)"
- shows "cauchy x"
+ fixes x :: "nat \<Rightarrow> real ^ 'n::finite"
+ assumes e:"0 < e" and s:"subspace s" and f:"linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and xs:"\<forall>n::nat. x n \<in> s" and cf:"Cauchy(f o x)"
+ shows "Cauchy x"
proof-
{ fix d::real assume "d>0"
then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
@@ -5166,7 +5354,7 @@
assumes "0 < e" and s:"subspace s" and f:"linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and cs:"complete s"
shows "complete(f ` s)"
proof-
- { fix g assume as:"\<forall>n::nat. g n \<in> f ` s" and cfg:"cauchy g"
+ { fix g assume as:"\<forall>n::nat. g n \<in> f ` s" and cfg:"Cauchy g"
then obtain x where "\<forall>n. x n \<in> s \<and> g n = f (x n)" unfolding image_iff and Bex_def
using choice[of "\<lambda> n xa. xa \<in> s \<and> g n = f xa"] by auto
hence x:"\<forall>n. x n \<in> s" "\<forall>n. g n = f (x n)" by auto
@@ -5236,6 +5424,7 @@
qed
lemma closed_injective_image_subspace:
+ fixes s :: "(real ^ _) set"
assumes "subspace s" "linear f" "\<forall>x\<in>s. f x = 0 --> x = 0" "closed s"
shows "closed(f ` s)"
proof-
@@ -5360,7 +5549,8 @@
by auto
lemma dim_closure:
- "dim(closure s) = dim s" (is "?dc = ?d")
+ fixes s :: "(real ^ _) set"
+ shows "dim(closure s) = dim s" (is "?dc = ?d")
proof-
have "?dc \<le> ?d" using closure_minimal[OF span_inc, of s]
using closed_subspace[OF subspace_span, of s]
@@ -5559,7 +5749,7 @@
thus ?thesis by auto
qed
}
- hence "cauchy z" unfolding cauchy_def by auto
+ hence "Cauchy z" unfolding cauchy_def by auto
then obtain x where "x\<in>s" and x:"(z ---> x) sequentially" using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto
def e \<equiv> "dist (f x) x"
--- a/src/HOL/Library/normarith.ML Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Library/normarith.ML Tue Jun 02 14:38:10 2009 +0200
@@ -391,7 +391,7 @@
fun init_conv ctxt =
Simplifier.rewrite (Simplifier.context ctxt
- (HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm dist_vector_def}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
+ (HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm vector_dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
then_conv field_comp_conv
then_conv nnf_conv
--- a/src/HOL/Lim.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Lim.thy Tue Jun 02 14:38:10 2009 +0200
@@ -13,90 +13,102 @@
text{*Standard Definitions*}
definition
- LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
+ at :: "'a::metric_space \<Rightarrow> 'a filter" where
+ [code del]: "at a = Abs_filter (\<lambda>P. \<exists>r>0. \<forall>x. x \<noteq> a \<and> dist x a < r \<longrightarrow> P x)"
+
+definition
+ LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"
("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
[code del]: "f -- a --> L =
- (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s
- --> norm (f x - L) < r)"
+ (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
+ --> dist (f x) L < r)"
definition
- isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
+ isCont :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a] \<Rightarrow> bool" where
"isCont f a = (f -- a --> (f a))"
definition
- isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
- [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
+ isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
+ [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
+
+subsection {* Neighborhood Filter *}
+lemma eventually_at:
+ "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
+unfolding at_def
+apply (rule eventually_Abs_filter)
+apply (rule_tac x=1 in exI, simp)
+apply (clarify, rule_tac x=r in exI, simp)
+apply (clarify, rename_tac r s)
+apply (rule_tac x="min r s" in exI, simp)
+done
+
+lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> tendsto f L (at a)"
+unfolding LIM_def tendsto_def eventually_at ..
subsection {* Limits of Functions *}
-subsubsection {* Purely standard proofs *}
+lemma metric_LIM_I:
+ "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
+ \<Longrightarrow> f -- a --> L"
+by (simp add: LIM_def)
+
+lemma metric_LIM_D:
+ "\<lbrakk>f -- a --> L; 0 < r\<rbrakk>
+ \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r"
+by (simp add: LIM_def)
lemma LIM_eq:
- "f -- a --> L =
+ fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
+ shows "f -- a --> L =
(\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
-by (simp add: LIM_def diff_minus)
+by (simp add: LIM_def dist_norm)
lemma LIM_I:
- "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
+ fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
+ shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
==> f -- a --> L"
by (simp add: LIM_eq)
lemma LIM_D:
- "[| f -- a --> L; 0<r |]
+ fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
+ shows "[| f -- a --> L; 0<r |]
==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
by (simp add: LIM_eq)
-lemma LIM_offset: "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
-apply (rule LIM_I)
-apply (drule_tac r="r" in LIM_D, safe)
+lemma LIM_offset:
+ fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
+ shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
+unfolding LIM_def dist_norm
+apply clarify
+apply (drule_tac x="r" in spec, safe)
apply (rule_tac x="s" in exI, safe)
apply (drule_tac x="x + k" in spec)
apply (simp add: algebra_simps)
done
-lemma LIM_offset_zero: "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
+lemma LIM_offset_zero:
+ fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
+ shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
by (drule_tac k="a" in LIM_offset, simp add: add_commute)
-lemma LIM_offset_zero_cancel: "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
+lemma LIM_offset_zero_cancel:
+ fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
+ shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
by (drule_tac k="- a" in LIM_offset, simp)
lemma LIM_const [simp]: "(%x. k) -- x --> k"
by (simp add: LIM_def)
lemma LIM_add:
- fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
assumes f: "f -- a --> L" and g: "g -- a --> M"
- shows "(%x. f x + g(x)) -- a --> (L + M)"
-proof (rule LIM_I)
- fix r :: real
- assume r: "0 < r"
- from LIM_D [OF f half_gt_zero [OF r]]
- obtain fs
- where fs: "0 < fs"
- and fs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < fs --> norm (f x - L) < r/2"
- by blast
- from LIM_D [OF g half_gt_zero [OF r]]
- obtain gs
- where gs: "0 < gs"
- and gs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < gs --> norm (g x - M) < r/2"
- by blast
- show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> norm (x-a) < s \<longrightarrow> norm (f x + g x - (L + M)) < r"
- proof (intro exI conjI strip)
- show "0 < min fs gs" by (simp add: fs gs)
- fix x :: 'a
- assume "x \<noteq> a \<and> norm (x-a) < min fs gs"
- hence "x \<noteq> a \<and> norm (x-a) < fs \<and> norm (x-a) < gs" by simp
- with fs_lt gs_lt
- have "norm (f x - L) < r/2" and "norm (g x - M) < r/2" by blast+
- hence "norm (f x - L) + norm (g x - M) < r" by arith
- thus "norm (f x + g x - (L + M)) < r"
- by (blast intro: norm_diff_triangle_ineq order_le_less_trans)
- qed
-qed
+ shows "(\<lambda>x. f x + g x) -- a --> (L + M)"
+using assms unfolding LIM_conv_tendsto by (rule tendsto_add)
lemma LIM_add_zero:
- "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"
by (drule (1) LIM_add, simp)
lemma minus_diff_minus:
@@ -104,46 +116,75 @@
shows "(- a) - (- b) = - (a - b)"
by simp
-lemma LIM_minus: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
-by (simp only: LIM_eq minus_diff_minus norm_minus_cancel)
+lemma LIM_minus:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"
+unfolding LIM_conv_tendsto by (rule tendsto_minus)
+(* TODO: delete *)
lemma LIM_add_minus:
- "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
by (intro LIM_add LIM_minus)
lemma LIM_diff:
- "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
-by (simp only: diff_minus LIM_add LIM_minus)
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m"
+unfolding LIM_conv_tendsto by (rule tendsto_diff)
-lemma LIM_zero: "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
-by (simp add: LIM_def)
-
-lemma LIM_zero_cancel: "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
-by (simp add: LIM_def)
+lemma LIM_zero:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
+by (simp add: LIM_def dist_norm)
-lemma LIM_zero_iff: "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
-by (simp add: LIM_def)
+lemma LIM_zero_cancel:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
+by (simp add: LIM_def dist_norm)
-lemma LIM_imp_LIM:
+lemma LIM_zero_iff:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
+by (simp add: LIM_def dist_norm)
+
+lemma metric_LIM_imp_LIM:
assumes f: "f -- a --> l"
- assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
+ assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
shows "g -- a --> m"
-apply (rule LIM_I, drule LIM_D [OF f], safe)
+apply (rule metric_LIM_I, drule metric_LIM_D [OF f], safe)
apply (rule_tac x="s" in exI, safe)
apply (drule_tac x="x" in spec, safe)
apply (erule (1) order_le_less_trans [OF le])
done
-lemma LIM_norm: "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"
-by (erule LIM_imp_LIM, simp add: norm_triangle_ineq3)
+lemma LIM_imp_LIM:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes g :: "'a::metric_space \<Rightarrow> 'c::real_normed_vector"
+ assumes f: "f -- a --> l"
+ assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
+ shows "g -- a --> m"
+apply (rule metric_LIM_imp_LIM [OF f])
+apply (simp add: dist_norm le)
+done
-lemma LIM_norm_zero: "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0"
+lemma LIM_norm:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"
+unfolding LIM_conv_tendsto by (rule tendsto_norm)
+
+lemma LIM_norm_zero:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0"
by (drule LIM_norm, simp)
-lemma LIM_norm_zero_cancel: "(\<lambda>x. norm (f x)) -- a --> 0 \<Longrightarrow> f -- a --> 0"
+lemma LIM_norm_zero_cancel:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "(\<lambda>x. norm (f x)) -- a --> 0 \<Longrightarrow> f -- a --> 0"
by (erule LIM_imp_LIM, simp)
-lemma LIM_norm_zero_iff: "(\<lambda>x. norm (f x)) -- a --> 0 = f -- a --> 0"
+lemma LIM_norm_zero_iff:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "(\<lambda>x. norm (f x)) -- a --> 0 = f -- a --> 0"
by (rule iffI [OF LIM_norm_zero_cancel LIM_norm_zero])
lemma LIM_rabs: "f -- a --> (l::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> \<bar>l\<bar>"
@@ -161,9 +202,9 @@
lemma LIM_const_not_eq:
fixes a :: "'a::real_normed_algebra_1"
shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
-apply (simp add: LIM_eq)
-apply (rule_tac x="norm (k - L)" in exI, simp, safe)
-apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real)
+apply (simp add: LIM_def)
+apply (rule_tac x="dist k L" in exI, simp add: zero_less_dist_iff, safe)
+apply (rule_tac x="a + of_real (s/2)" in exI, simp add: dist_norm)
done
lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
@@ -176,10 +217,21 @@
done
lemma LIM_unique:
- fixes a :: "'a::real_normed_algebra_1"
+ fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
-apply (drule (1) LIM_diff)
-apply (auto dest!: LIM_const_eq)
+apply (rule ccontr)
+apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff)
+apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff)
+apply (clarify, rename_tac r s)
+apply (subgoal_tac "min r s \<noteq> 0")
+apply (subgoal_tac "dist L M < dist L M / 2 + dist L M / 2", simp)
+apply (subgoal_tac "dist L M \<le> dist (f (a + of_real (min r s / 2))) L +
+ dist (f (a + of_real (min r s / 2))) M")
+apply (erule le_less_trans, rule add_strict_mono)
+apply (drule spec, erule mp, simp add: dist_norm)
+apply (drule spec, erule mp, simp add: dist_norm)
+apply (subst dist_commute, rule dist_triangle)
+apply simp
done
lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
@@ -195,9 +247,9 @@
\<Longrightarrow> ((\<lambda>x. f x) -- a --> l) = ((\<lambda>x. g x) -- b --> m)"
by (simp add: LIM_def)
-lemma LIM_equal2:
+lemma metric_LIM_equal2:
assumes 1: "0 < R"
- assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
+ assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
shows "g -- a --> l \<Longrightarrow> f -- a --> l"
apply (unfold LIM_def, safe)
apply (drule_tac x="r" in spec, safe)
@@ -206,9 +258,22 @@
apply (simp add: 2)
done
-text{*Two uses in Hyperreal/Transcendental.ML*}
+lemma LIM_equal2:
+ fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
+ assumes 1: "0 < R"
+ assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
+ shows "g -- a --> l \<Longrightarrow> f -- a --> l"
+apply (unfold LIM_def dist_norm, safe)
+apply (drule_tac x="r" in spec, safe)
+apply (rule_tac x="min s R" in exI, safe)
+apply (simp add: 1)
+apply (simp add: 2)
+done
+
+text{*Two uses in Transcendental.ML*}
lemma LIM_trans:
- "[| (%x. f(x) + -g(x)) -- a --> 0; g -- a --> l |] ==> f -- a --> l"
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "[| (%x. f(x) + -g(x)) -- a --> 0; g -- a --> l |] ==> f -- a --> l"
apply (drule LIM_add, assumption)
apply (auto simp add: add_assoc)
done
@@ -217,62 +282,70 @@
assumes g: "g -- l --> g l"
assumes f: "f -- a --> l"
shows "(\<lambda>x. g (f x)) -- a --> g l"
-proof (rule LIM_I)
+proof (rule metric_LIM_I)
fix r::real assume r: "0 < r"
obtain s where s: "0 < s"
- and less_r: "\<And>y. \<lbrakk>y \<noteq> l; norm (y - l) < s\<rbrakk> \<Longrightarrow> norm (g y - g l) < r"
- using LIM_D [OF g r] by fast
+ and less_r: "\<And>y. \<lbrakk>y \<noteq> l; dist y l < s\<rbrakk> \<Longrightarrow> dist (g y) (g l) < r"
+ using metric_LIM_D [OF g r] by fast
obtain t where t: "0 < t"
- and less_s: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (f x - l) < s"
- using LIM_D [OF f s] by fast
+ and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) l < s"
+ using metric_LIM_D [OF f s] by fast
- show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < t \<longrightarrow> norm (g (f x) - g l) < r"
+ show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) (g l) < r"
proof (rule exI, safe)
show "0 < t" using t .
next
- fix x assume "x \<noteq> a" and "norm (x - a) < t"
- hence "norm (f x - l) < s" by (rule less_s)
- thus "norm (g (f x) - g l) < r"
+ fix x assume "x \<noteq> a" and "dist x a < t"
+ hence "dist (f x) l < s" by (rule less_s)
+ thus "dist (g (f x)) (g l) < r"
using r less_r by (case_tac "f x = l", simp_all)
qed
qed
+lemma metric_LIM_compose2:
+ assumes f: "f -- a --> b"
+ assumes g: "g -- b --> c"
+ assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
+ shows "(\<lambda>x. g (f x)) -- a --> c"
+proof (rule metric_LIM_I)
+ fix r :: real
+ assume r: "0 < r"
+ obtain s where s: "0 < s"
+ and less_r: "\<And>y. \<lbrakk>y \<noteq> b; dist y b < s\<rbrakk> \<Longrightarrow> dist (g y) c < r"
+ using metric_LIM_D [OF g r] by fast
+ obtain t where t: "0 < t"
+ and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) b < s"
+ using metric_LIM_D [OF f s] by fast
+ obtain d where d: "0 < d"
+ and neq_b: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < d\<rbrakk> \<Longrightarrow> f x \<noteq> b"
+ using inj by fast
+
+ show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) c < r"
+ proof (safe intro!: exI)
+ show "0 < min d t" using d t by simp
+ next
+ fix x
+ assume "x \<noteq> a" and "dist x a < min d t"
+ hence "f x \<noteq> b" and "dist (f x) b < s"
+ using neq_b less_s by simp_all
+ thus "dist (g (f x)) c < r"
+ by (rule less_r)
+ qed
+qed
+
lemma LIM_compose2:
+ fixes a :: "'a::real_normed_vector"
assumes f: "f -- a --> b"
assumes g: "g -- b --> c"
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
shows "(\<lambda>x. g (f x)) -- a --> c"
-proof (rule LIM_I)
- fix r :: real
- assume r: "0 < r"
- obtain s where s: "0 < s"
- and less_r: "\<And>y. \<lbrakk>y \<noteq> b; norm (y - b) < s\<rbrakk> \<Longrightarrow> norm (g y - c) < r"
- using LIM_D [OF g r] by fast
- obtain t where t: "0 < t"
- and less_s: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (f x - b) < s"
- using LIM_D [OF f s] by fast
- obtain d where d: "0 < d"
- and neq_b: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < d\<rbrakk> \<Longrightarrow> f x \<noteq> b"
- using inj by fast
-
- show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < t \<longrightarrow> norm (g (f x) - c) < r"
- proof (safe intro!: exI)
- show "0 < min d t" using d t by simp
- next
- fix x
- assume "x \<noteq> a" and "norm (x - a) < min d t"
- hence "f x \<noteq> b" and "norm (f x - b) < s"
- using neq_b less_s by simp_all
- thus "norm (g (f x) - c) < r"
- by (rule less_r)
- qed
-qed
+by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
unfolding o_def by (rule LIM_compose)
lemma real_LIM_sandwich_zero:
- fixes f g :: "'a::real_normed_vector \<Rightarrow> real"
+ fixes f g :: "'a::metric_space \<Rightarrow> real"
assumes f: "f -- a --> 0"
assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
@@ -288,26 +361,12 @@
text {* Bounded Linear Operators *}
-lemma (in bounded_linear) cont: "f -- a --> f a"
-proof (rule LIM_I)
- fix r::real assume r: "0 < r"
- obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
- using pos_bounded by fast
- show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - f a) < r"
- proof (rule exI, safe)
- from r K show "0 < r / K" by (rule divide_pos_pos)
- next
- fix x assume x: "norm (x - a) < r / K"
- have "norm (f x - f a) = norm (f (x - a))" by (simp only: diff)
- also have "\<dots> \<le> norm (x - a) * K" by (rule norm_le)
- also from K x have "\<dots> < r" by (simp only: pos_less_divide_eq)
- finally show "norm (f x - f a) < r" .
- qed
-qed
-
lemma (in bounded_linear) LIM:
"g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
-by (rule LIM_compose [OF cont])
+unfolding LIM_conv_tendsto by (rule tendsto)
+
+lemma (in bounded_linear) cont: "f -- a --> f a"
+by (rule LIM [OF LIM_ident])
lemma (in bounded_linear) LIM_zero:
"g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
@@ -315,39 +374,16 @@
text {* Bounded Bilinear Operators *}
+lemma (in bounded_bilinear) LIM:
+ "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
+unfolding LIM_conv_tendsto by (rule tendsto)
+
lemma (in bounded_bilinear) LIM_prod_zero:
+ fixes a :: "'d::metric_space"
assumes f: "f -- a --> 0"
assumes g: "g -- a --> 0"
shows "(\<lambda>x. f x ** g x) -- a --> 0"
-proof (rule LIM_I)
- fix r::real assume r: "0 < r"
- obtain K where K: "0 < K"
- and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
- using pos_bounded by fast
- from K have K': "0 < inverse K"
- by (rule positive_imp_inverse_positive)
- obtain s where s: "0 < s"
- and norm_f: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x) < r"
- using LIM_D [OF f r] by auto
- obtain t where t: "0 < t"
- and norm_g: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (g x) < inverse K"
- using LIM_D [OF g K'] by auto
- show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x ** g x - 0) < r"
- proof (rule exI, safe)
- from s t show "0 < min s t" by simp
- next
- fix x assume x: "x \<noteq> a"
- assume "norm (x - a) < min s t"
- hence xs: "norm (x - a) < s" and xt: "norm (x - a) < t" by simp_all
- from x xs have 1: "norm (f x) < r" by (rule norm_f)
- from x xt have 2: "norm (g x) < inverse K" by (rule norm_g)
- have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" by (rule norm_le)
- also from 1 2 K have "\<dots> < r * inverse K * K"
- by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero)
- also from K have "r * inverse K * K = r" by simp
- finally show "norm (f x ** g x - 0) < r" by simp
- qed
-qed
+using LIM [OF f g] by (simp add: zero_left)
lemma (in bounded_bilinear) LIM_left_zero:
"f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0"
@@ -357,19 +393,6 @@
"f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
by (rule bounded_linear.LIM_zero [OF bounded_linear_right])
-lemma (in bounded_bilinear) LIM:
- "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
-apply (drule LIM_zero)
-apply (drule LIM_zero)
-apply (rule LIM_zero_cancel)
-apply (subst prod_diff_prod)
-apply (rule LIM_add_zero)
-apply (rule LIM_add_zero)
-apply (erule (1) LIM_prod_zero)
-apply (erule LIM_left_zero)
-apply (erule LIM_right_zero)
-done
-
lemmas LIM_mult = mult.LIM
lemmas LIM_mult_zero = mult.LIM_prod_zero
@@ -383,89 +406,41 @@
lemmas LIM_of_real = of_real.LIM
lemma LIM_power:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}"
assumes f: "f -- a --> l"
shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
by (induct n, simp, simp add: LIM_mult f)
subsubsection {* Derived theorems about @{term LIM} *}
-lemma LIM_inverse_lemma:
- fixes x :: "'a::real_normed_div_algebra"
- assumes r: "0 < r"
- assumes x: "norm (x - 1) < min (1/2) (r/2)"
- shows "norm (inverse x - 1) < r"
-proof -
- from r have r2: "0 < r/2" by simp
- from x have 0: "x \<noteq> 0" by clarsimp
- from x have x': "norm (1 - x) < min (1/2) (r/2)"
- by (simp only: norm_minus_commute)
- hence less1: "norm (1 - x) < r/2" by simp
- have "norm (1::'a) - norm x \<le> norm (1 - x)" by (rule norm_triangle_ineq2)
- also from x' have "norm (1 - x) < 1/2" by simp
- finally have "1/2 < norm x" by simp
- hence "inverse (norm x) < inverse (1/2)"
- by (rule less_imp_inverse_less, simp)
- hence less2: "norm (inverse x) < 2"
- by (simp add: nonzero_norm_inverse 0)
- from less1 less2 r2 norm_ge_zero
- have "norm (1 - x) * norm (inverse x) < (r/2) * 2"
- by (rule mult_strict_mono)
- thus "norm (inverse x - 1) < r"
- by (simp only: norm_mult [symmetric] left_diff_distrib, simp add: 0)
-qed
+lemma LIM_inverse:
+ fixes L :: "'a::real_normed_div_algebra"
+ shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
+unfolding LIM_conv_tendsto
+by (rule tendsto_inverse)
lemma LIM_inverse_fun:
assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"
shows "inverse -- a --> inverse a"
-proof (rule LIM_equal2)
- from a show "0 < norm a" by simp
-next
- fix x assume "norm (x - a) < norm a"
- hence "x \<noteq> 0" by auto
- with a show "inverse x = inverse (inverse a * x) * inverse a"
- by (simp add: nonzero_inverse_mult_distrib
- nonzero_imp_inverse_nonzero
- nonzero_inverse_inverse_eq mult_assoc)
-next
- have 1: "inverse -- 1 --> inverse (1::'a)"
- apply (rule LIM_I)
- apply (rule_tac x="min (1/2) (r/2)" in exI)
- apply (simp add: LIM_inverse_lemma)
- done
- have "(\<lambda>x. inverse a * x) -- a --> inverse a * a"
- by (intro LIM_mult LIM_ident LIM_const)
- hence "(\<lambda>x. inverse a * x) -- a --> 1"
- by (simp add: a)
- with 1 have "(\<lambda>x. inverse (inverse a * x)) -- a --> inverse 1"
- by (rule LIM_compose)
- hence "(\<lambda>x. inverse (inverse a * x)) -- a --> 1"
- by simp
- hence "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> 1 * inverse a"
- by (intro LIM_mult LIM_const)
- thus "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> inverse a"
- by simp
-qed
-
-lemma LIM_inverse:
- fixes L :: "'a::real_normed_div_algebra"
- shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
-by (rule LIM_inverse_fun [THEN LIM_compose])
+by (rule LIM_inverse [OF LIM_ident a])
lemma LIM_sgn:
- "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
unfolding sgn_div_norm
by (simp add: LIM_scaleR LIM_inverse LIM_norm)
subsection {* Continuity *}
-subsubsection {* Purely standard proofs *}
-
-lemma LIM_isCont_iff: "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
+lemma LIM_isCont_iff:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
+ shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
-lemma isCont_iff: "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
+lemma isCont_iff:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
+ shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
by (simp add: isCont_def LIM_isCont_iff)
lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a"
@@ -474,28 +449,36 @@
lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
unfolding isCont_def by (rule LIM_const)
-lemma isCont_norm: "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
+lemma isCont_norm:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
unfolding isCont_def by (rule LIM_norm)
lemma isCont_rabs: "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x :: real\<bar>) a"
unfolding isCont_def by (rule LIM_rabs)
-lemma isCont_add: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
+lemma isCont_add:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
unfolding isCont_def by (rule LIM_add)
-lemma isCont_minus: "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
+lemma isCont_minus:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
unfolding isCont_def by (rule LIM_minus)
-lemma isCont_diff: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
+lemma isCont_diff:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
unfolding isCont_def by (rule LIM_diff)
lemma isCont_mult:
- fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_algebra"
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
unfolding isCont_def by (rule LIM_mult)
lemma isCont_inverse:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_div_algebra"
shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
unfolding isCont_def by (rule LIM_inverse)
@@ -503,7 +486,15 @@
"\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
unfolding isCont_def by (rule LIM_compose)
+lemma metric_isCont_LIM_compose2:
+ assumes f [unfolded isCont_def]: "isCont f a"
+ assumes g: "g -- f a --> l"
+ assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
+ shows "(\<lambda>x. g (f x)) -- a --> l"
+by (rule metric_LIM_compose2 [OF f g inj])
+
lemma isCont_LIM_compose2:
+ fixes a :: "'a::real_normed_vector"
assumes f [unfolded isCont_def]: "isCont f a"
assumes g: "g -- f a --> l"
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
@@ -526,22 +517,25 @@
lemmas isCont_scaleR = scaleR.isCont
lemma isCont_of_real:
- "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)) a"
+ "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
unfolding isCont_def by (rule LIM_of_real)
lemma isCont_power:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}"
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
unfolding isCont_def by (rule LIM_power)
lemma isCont_sgn:
- "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
unfolding isCont_def by (rule LIM_sgn)
lemma isCont_abs [simp]: "isCont abs (a::real)"
by (rule isCont_rabs [OF isCont_ident])
-lemma isCont_setsum: fixes A :: "nat set" assumes "finite A"
+lemma isCont_setsum:
+ fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::real_normed_vector"
+ fixes A :: "'a set" assumes "finite A"
shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x"
using `finite A`
proof induct
@@ -578,7 +572,7 @@
hence "f ?x < 0" using `f x < 0` by auto
thus False using `0 \<le> f ?x` by auto
qed
-
+
subsection {* Uniform Continuity *}
@@ -588,14 +582,14 @@
lemma isUCont_Cauchy:
"\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
unfolding isUCont_def
-apply (rule CauchyI)
+apply (rule metric_CauchyI)
apply (drule_tac x=e in spec, safe)
-apply (drule_tac e=s in CauchyD, safe)
+apply (drule_tac e=s in metric_CauchyD, safe)
apply (rule_tac x=M in exI, simp)
done
lemma (in bounded_linear) isUCont: "isUCont f"
-unfolding isUCont_def
+unfolding isUCont_def dist_norm
proof (intro allI impI)
fix r::real assume r: "0 < r"
obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
@@ -620,44 +614,46 @@
subsection {* Relation of LIM and LIMSEQ *}
lemma LIMSEQ_SEQ_conv1:
- fixes a :: "'a::real_normed_vector"
+ fixes a :: "'a::metric_space"
assumes X: "X -- a --> L"
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
-proof (safe intro!: LIMSEQ_I)
+proof (safe intro!: metric_LIMSEQ_I)
fix S :: "nat \<Rightarrow> 'a"
fix r :: real
assume rgz: "0 < r"
assume as: "\<forall>n. S n \<noteq> a"
assume S: "S ----> a"
- from LIM_D [OF X rgz] obtain s
+ from metric_LIM_D [OF X rgz] obtain s
where sgz: "0 < s"
- and aux: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (X x - L) < r"
+ and aux: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < s\<rbrakk> \<Longrightarrow> dist (X x) L < r"
by fast
- from LIMSEQ_D [OF S sgz]
- obtain no where "\<forall>n\<ge>no. norm (S n - a) < s" by blast
- hence "\<forall>n\<ge>no. norm (X (S n) - L) < r" by (simp add: aux as)
- thus "\<exists>no. \<forall>n\<ge>no. norm (X (S n) - L) < r" ..
+ from metric_LIMSEQ_D [OF S sgz]
+ obtain no where "\<forall>n\<ge>no. dist (S n) a < s" by blast
+ hence "\<forall>n\<ge>no. dist (X (S n)) L < r" by (simp add: aux as)
+ thus "\<exists>no. \<forall>n\<ge>no. dist (X (S n)) L < r" ..
qed
+
lemma LIMSEQ_SEQ_conv2:
fixes a :: real
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
shows "X -- a --> L"
proof (rule ccontr)
assume "\<not> (X -- a --> L)"
- hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> norm (X x - L) < r)" by (unfold LIM_def)
- hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x - a\<bar> < s --> norm (X x - L) < r)" by simp
- hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r)" by (simp add: linorder_not_less)
- then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r))" by auto
+ hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> dist (X x) L < r)"
+ unfolding LIM_def dist_norm .
+ hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x - a\<bar> < s --> dist (X x) L < r)" by simp
+ hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r)" by (simp add: not_less)
+ then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r))" by auto
- let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r"
- have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r"
+ let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
+ have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
using rdef by simp
- hence F: "\<And>n. ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> norm (X (?F n) - L) \<ge> r"
+ hence F: "\<And>n. ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> dist (X (?F n)) L \<ge> r"
by (rule someI_ex)
hence F1: "\<And>n. ?F n \<noteq> a"
and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
- and F3: "\<And>n. norm (X (?F n) - L) \<ge> r"
+ and F3: "\<And>n. dist (X (?F n)) L \<ge> r"
by fast+
have "?F ----> a"
@@ -694,13 +690,13 @@
obtain n where "n = no + 1" by simp
then have nolen: "no \<le> n" by simp
(* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
- have "norm (X (?F n) - L) \<ge> r"
+ have "dist (X (?F n)) L \<ge> r"
by (rule F3)
- with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r" by fast
+ with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast
}
- then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r)" by simp
- with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> e)" by auto
- thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less)
+ then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp
+ with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto
+ thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less)
qed
ultimately show False by simp
qed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Limits.thy Tue Jun 02 14:38:10 2009 +0200
@@ -0,0 +1,462 @@
+(* Title : Limits.thy
+ Author : Brian Huffman
+*)
+
+header {* Filters and Limits *}
+
+theory Limits
+imports RealVector RComplete
+begin
+
+subsection {* Filters *}
+
+typedef (open) 'a filter =
+ "{f :: ('a \<Rightarrow> bool) \<Rightarrow> bool. f (\<lambda>x. True)
+ \<and> (\<forall>P Q. (\<forall>x. P x \<longrightarrow> Q x) \<longrightarrow> f P \<longrightarrow> f Q)
+ \<and> (\<forall>P Q. f P \<longrightarrow> f Q \<longrightarrow> f (\<lambda>x. P x \<and> Q x))}"
+proof
+ show "(\<lambda>P. True) \<in> ?filter" by simp
+qed
+
+definition
+ eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool" where
+ [code del]: "eventually P F \<longleftrightarrow> Rep_filter F P"
+
+lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
+unfolding eventually_def using Rep_filter [of F] by blast
+
+lemma eventually_mono:
+ "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
+unfolding eventually_def using Rep_filter [of F] by blast
+
+lemma eventually_conj:
+ "\<lbrakk>eventually (\<lambda>x. P x) F; eventually (\<lambda>x. Q x) F\<rbrakk>
+ \<Longrightarrow> eventually (\<lambda>x. P x \<and> Q x) F"
+unfolding eventually_def using Rep_filter [of F] by blast
+
+lemma eventually_mp:
+ assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
+ assumes "eventually (\<lambda>x. P x) F"
+ shows "eventually (\<lambda>x. Q x) F"
+proof (rule eventually_mono)
+ show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
+ show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
+ using assms by (rule eventually_conj)
+qed
+
+lemma eventually_rev_mp:
+ assumes "eventually (\<lambda>x. P x) F"
+ assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
+ shows "eventually (\<lambda>x. Q x) F"
+using assms(2) assms(1) by (rule eventually_mp)
+
+lemma eventually_conj_iff:
+ "eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net"
+by (auto intro: eventually_conj elim: eventually_rev_mp)
+
+lemma eventually_Abs_filter:
+ assumes "f (\<lambda>x. True)"
+ assumes "\<And>P Q. (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> f P \<Longrightarrow> f Q"
+ assumes "\<And>P Q. f P \<Longrightarrow> f Q \<Longrightarrow> f (\<lambda>x. P x \<and> Q x)"
+ shows "eventually P (Abs_filter f) \<longleftrightarrow> f P"
+unfolding eventually_def using assms
+by (subst Abs_filter_inverse, auto)
+
+lemma filter_ext:
+ "(\<And>P. eventually P F \<longleftrightarrow> eventually P F') \<Longrightarrow> F = F'"
+unfolding eventually_def
+by (simp add: Rep_filter_inject [THEN iffD1] ext)
+
+lemma eventually_elim1:
+ assumes "eventually (\<lambda>i. P i) F"
+ assumes "\<And>i. P i \<Longrightarrow> Q i"
+ shows "eventually (\<lambda>i. Q i) F"
+using assms by (auto elim!: eventually_rev_mp)
+
+lemma eventually_elim2:
+ assumes "eventually (\<lambda>i. P i) F"
+ assumes "eventually (\<lambda>i. Q i) F"
+ assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
+ shows "eventually (\<lambda>i. R i) F"
+using assms by (auto elim!: eventually_rev_mp)
+
+
+subsection {* Boundedness *}
+
+definition
+ Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" where
+ [code del]: "Bfun S F = (\<exists>K>0. eventually (\<lambda>i. norm (S i) \<le> K) F)"
+
+lemma BfunI: assumes K: "eventually (\<lambda>i. norm (X i) \<le> K) F" shows "Bfun X F"
+unfolding Bfun_def
+proof (intro exI conjI allI)
+ show "0 < max K 1" by simp
+next
+ show "eventually (\<lambda>i. norm (X i) \<le> max K 1) F"
+ using K by (rule eventually_elim1, simp)
+qed
+
+lemma BfunE:
+ assumes "Bfun S F"
+ obtains B where "0 < B" and "eventually (\<lambda>i. norm (S i) \<le> B) F"
+using assms unfolding Bfun_def by fast
+
+
+subsection {* Convergence to Zero *}
+
+definition
+ Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" where
+ [code del]: "Zfun S F = (\<forall>r>0. eventually (\<lambda>i. norm (S i) < r) F)"
+
+lemma ZfunI:
+ "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) F) \<Longrightarrow> Zfun S F"
+unfolding Zfun_def by simp
+
+lemma ZfunD:
+ "\<lbrakk>Zfun S F; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) F"
+unfolding Zfun_def by simp
+
+lemma Zfun_ssubst:
+ "eventually (\<lambda>i. X i = Y i) F \<Longrightarrow> Zfun Y F \<Longrightarrow> Zfun X F"
+unfolding Zfun_def by (auto elim!: eventually_rev_mp)
+
+lemma Zfun_zero: "Zfun (\<lambda>i. 0) F"
+unfolding Zfun_def by simp
+
+lemma Zfun_norm_iff: "Zfun (\<lambda>i. norm (S i)) F = Zfun (\<lambda>i. S i) F"
+unfolding Zfun_def by simp
+
+lemma Zfun_imp_Zfun:
+ assumes X: "Zfun X F"
+ assumes Y: "eventually (\<lambda>i. norm (Y i) \<le> norm (X i) * K) F"
+ shows "Zfun (\<lambda>n. Y n) F"
+proof (cases)
+ assume K: "0 < K"
+ show ?thesis
+ proof (rule ZfunI)
+ fix r::real assume "0 < r"
+ hence "0 < r / K"
+ using K by (rule divide_pos_pos)
+ then have "eventually (\<lambda>i. norm (X i) < r / K) F"
+ using ZfunD [OF X] by fast
+ with Y show "eventually (\<lambda>i. norm (Y i) < r) F"
+ proof (rule eventually_elim2)
+ fix i
+ assume *: "norm (Y i) \<le> norm (X i) * K"
+ assume "norm (X i) < r / K"
+ hence "norm (X i) * K < r"
+ by (simp add: pos_less_divide_eq K)
+ thus "norm (Y i) < r"
+ by (simp add: order_le_less_trans [OF *])
+ qed
+ qed
+next
+ assume "\<not> 0 < K"
+ hence K: "K \<le> 0" by (simp only: not_less)
+ show ?thesis
+ proof (rule ZfunI)
+ fix r :: real
+ assume "0 < r"
+ from Y show "eventually (\<lambda>i. norm (Y i) < r) F"
+ proof (rule eventually_elim1)
+ fix i
+ assume "norm (Y i) \<le> norm (X i) * K"
+ also have "\<dots> \<le> norm (X i) * 0"
+ using K norm_ge_zero by (rule mult_left_mono)
+ finally show "norm (Y i) < r"
+ using `0 < r` by simp
+ qed
+ qed
+qed
+
+lemma Zfun_le: "\<lbrakk>Zfun Y F; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zfun X F"
+by (erule_tac K="1" in Zfun_imp_Zfun, simp)
+
+lemma Zfun_add:
+ assumes X: "Zfun X F" and Y: "Zfun Y F"
+ shows "Zfun (\<lambda>n. X n + Y n) F"
+proof (rule ZfunI)
+ fix r::real assume "0 < r"
+ hence r: "0 < r / 2" by simp
+ have "eventually (\<lambda>i. norm (X i) < r/2) F"
+ using X r by (rule ZfunD)
+ moreover
+ have "eventually (\<lambda>i. norm (Y i) < r/2) F"
+ using Y r by (rule ZfunD)
+ ultimately
+ show "eventually (\<lambda>i. norm (X i + Y i) < r) F"
+ proof (rule eventually_elim2)
+ fix i
+ assume *: "norm (X i) < r/2" "norm (Y i) < r/2"
+ have "norm (X i + Y i) \<le> norm (X i) + norm (Y i)"
+ by (rule norm_triangle_ineq)
+ also have "\<dots> < r/2 + r/2"
+ using * by (rule add_strict_mono)
+ finally show "norm (X i + Y i) < r"
+ by simp
+ qed
+qed
+
+lemma Zfun_minus: "Zfun X F \<Longrightarrow> Zfun (\<lambda>i. - X i) F"
+unfolding Zfun_def by simp
+
+lemma Zfun_diff: "\<lbrakk>Zfun X F; Zfun Y F\<rbrakk> \<Longrightarrow> Zfun (\<lambda>i. X i - Y i) F"
+by (simp only: diff_minus Zfun_add Zfun_minus)
+
+lemma (in bounded_linear) Zfun:
+ assumes X: "Zfun X F"
+ shows "Zfun (\<lambda>n. f (X n)) F"
+proof -
+ obtain K where "\<And>x. norm (f x) \<le> norm x * K"
+ using bounded by fast
+ then have "eventually (\<lambda>i. norm (f (X i)) \<le> norm (X i) * K) F"
+ by simp
+ with X show ?thesis
+ by (rule Zfun_imp_Zfun)
+qed
+
+lemma (in bounded_bilinear) Zfun:
+ assumes X: "Zfun X F"
+ assumes Y: "Zfun Y F"
+ shows "Zfun (\<lambda>n. X n ** Y n) F"
+proof (rule ZfunI)
+ fix r::real assume r: "0 < r"
+ obtain K where K: "0 < K"
+ and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
+ using pos_bounded by fast
+ from K have K': "0 < inverse K"
+ by (rule positive_imp_inverse_positive)
+ have "eventually (\<lambda>i. norm (X i) < r) F"
+ using X r by (rule ZfunD)
+ moreover
+ have "eventually (\<lambda>i. norm (Y i) < inverse K) F"
+ using Y K' by (rule ZfunD)
+ ultimately
+ show "eventually (\<lambda>i. norm (X i ** Y i) < r) F"
+ proof (rule eventually_elim2)
+ fix i
+ assume *: "norm (X i) < r" "norm (Y i) < inverse K"
+ have "norm (X i ** Y i) \<le> norm (X i) * norm (Y i) * K"
+ by (rule norm_le)
+ also have "norm (X i) * norm (Y i) * K < r * inverse K * K"
+ by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero * K)
+ also from K have "r * inverse K * K = r"
+ by simp
+ finally show "norm (X i ** Y i) < r" .
+ qed
+qed
+
+lemma (in bounded_bilinear) Zfun_left:
+ "Zfun X F \<Longrightarrow> Zfun (\<lambda>n. X n ** a) F"
+by (rule bounded_linear_left [THEN bounded_linear.Zfun])
+
+lemma (in bounded_bilinear) Zfun_right:
+ "Zfun X F \<Longrightarrow> Zfun (\<lambda>n. a ** X n) F"
+by (rule bounded_linear_right [THEN bounded_linear.Zfun])
+
+lemmas Zfun_mult = mult.Zfun
+lemmas Zfun_mult_right = mult.Zfun_right
+lemmas Zfun_mult_left = mult.Zfun_left
+
+
+subsection{* Limits *}
+
+definition
+ tendsto :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a filter \<Rightarrow> bool" where
+ [code del]: "tendsto f l net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
+
+lemma tendstoI:
+ "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net)
+ \<Longrightarrow> tendsto f l net"
+ unfolding tendsto_def by auto
+
+lemma tendstoD:
+ "tendsto f l net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
+ unfolding tendsto_def by auto
+
+lemma tendsto_Zfun_iff: "tendsto (\<lambda>n. X n) L F = Zfun (\<lambda>n. X n - L) F"
+by (simp only: tendsto_def Zfun_def dist_norm)
+
+lemma tendsto_const: "tendsto (\<lambda>n. k) k F"
+by (simp add: tendsto_def)
+
+lemma tendsto_norm:
+ fixes a :: "'a::real_normed_vector"
+ shows "tendsto X a F \<Longrightarrow> tendsto (\<lambda>n. norm (X n)) (norm a) F"
+apply (simp add: tendsto_def dist_norm, safe)
+apply (drule_tac x="e" in spec, safe)
+apply (erule eventually_elim1)
+apply (erule order_le_less_trans [OF norm_triangle_ineq3])
+done
+
+lemma add_diff_add:
+ fixes a b c d :: "'a::ab_group_add"
+ shows "(a + c) - (b + d) = (a - b) + (c - d)"
+by simp
+
+lemma minus_diff_minus:
+ fixes a b :: "'a::ab_group_add"
+ shows "(- a) - (- b) = - (a - b)"
+by simp
+
+lemma tendsto_add:
+ fixes a b :: "'a::real_normed_vector"
+ shows "\<lbrakk>tendsto X a F; tendsto Y b F\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n + Y n) (a + b) F"
+by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
+
+lemma tendsto_minus:
+ fixes a :: "'a::real_normed_vector"
+ shows "tendsto X a F \<Longrightarrow> tendsto (\<lambda>n. - X n) (- a) F"
+by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus)
+
+lemma tendsto_minus_cancel:
+ fixes a :: "'a::real_normed_vector"
+ shows "tendsto (\<lambda>n. - X n) (- a) F \<Longrightarrow> tendsto X a F"
+by (drule tendsto_minus, simp)
+
+lemma tendsto_diff:
+ fixes a b :: "'a::real_normed_vector"
+ shows "\<lbrakk>tendsto X a F; tendsto Y b F\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n - Y n) (a - b) F"
+by (simp add: diff_minus tendsto_add tendsto_minus)
+
+lemma (in bounded_linear) tendsto:
+ "tendsto X a F \<Longrightarrow> tendsto (\<lambda>n. f (X n)) (f a) F"
+by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
+
+lemma (in bounded_bilinear) tendsto:
+ "\<lbrakk>tendsto X a F; tendsto Y b F\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n ** Y n) (a ** b) F"
+by (simp only: tendsto_Zfun_iff prod_diff_prod
+ Zfun_add Zfun Zfun_left Zfun_right)
+
+
+subsection {* Continuity of Inverse *}
+
+lemma (in bounded_bilinear) Zfun_prod_Bfun:
+ assumes X: "Zfun X F"
+ assumes Y: "Bfun Y F"
+ shows "Zfun (\<lambda>n. X n ** Y n) F"
+proof -
+ obtain K where K: "0 \<le> K"
+ and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
+ using nonneg_bounded by fast
+ obtain B where B: "0 < B"
+ and norm_Y: "eventually (\<lambda>i. norm (Y i) \<le> B) F"
+ using Y by (rule BfunE)
+ have "eventually (\<lambda>i. norm (X i ** Y i) \<le> norm (X i) * (B * K)) F"
+ using norm_Y proof (rule eventually_elim1)
+ fix i
+ assume *: "norm (Y i) \<le> B"
+ have "norm (X i ** Y i) \<le> norm (X i) * norm (Y i) * K"
+ by (rule norm_le)
+ also have "\<dots> \<le> norm (X i) * B * K"
+ by (intro mult_mono' order_refl norm_Y norm_ge_zero
+ mult_nonneg_nonneg K *)
+ also have "\<dots> = norm (X i) * (B * K)"
+ by (rule mult_assoc)
+ finally show "norm (X i ** Y i) \<le> norm (X i) * (B * K)" .
+ qed
+ with X show ?thesis
+ by (rule Zfun_imp_Zfun)
+qed
+
+lemma (in bounded_bilinear) flip:
+ "bounded_bilinear (\<lambda>x y. y ** x)"
+apply default
+apply (rule add_right)
+apply (rule add_left)
+apply (rule scaleR_right)
+apply (rule scaleR_left)
+apply (subst mult_commute)
+using bounded by fast
+
+lemma (in bounded_bilinear) Bfun_prod_Zfun:
+ assumes X: "Bfun X F"
+ assumes Y: "Zfun Y F"
+ shows "Zfun (\<lambda>n. X n ** Y n) F"
+using flip Y X by (rule bounded_bilinear.Zfun_prod_Bfun)
+
+lemma inverse_diff_inverse:
+ "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
+ \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
+by (simp add: algebra_simps)
+
+lemma Bfun_inverse_lemma:
+ fixes x :: "'a::real_normed_div_algebra"
+ shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
+apply (subst nonzero_norm_inverse, clarsimp)
+apply (erule (1) le_imp_inverse_le)
+done
+
+lemma Bfun_inverse:
+ fixes a :: "'a::real_normed_div_algebra"
+ assumes X: "tendsto X a F"
+ assumes a: "a \<noteq> 0"
+ shows "Bfun (\<lambda>n. inverse (X n)) F"
+proof -
+ from a have "0 < norm a" by simp
+ hence "\<exists>r>0. r < norm a" by (rule dense)
+ then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
+ have "eventually (\<lambda>i. dist (X i) a < r) F"
+ using tendstoD [OF X r1] by fast
+ hence "eventually (\<lambda>i. norm (inverse (X i)) \<le> inverse (norm a - r)) F"
+ proof (rule eventually_elim1)
+ fix i
+ assume "dist (X i) a < r"
+ hence 1: "norm (X i - a) < r"
+ by (simp add: dist_norm)
+ hence 2: "X i \<noteq> 0" using r2 by auto
+ hence "norm (inverse (X i)) = inverse (norm (X i))"
+ by (rule nonzero_norm_inverse)
+ also have "\<dots> \<le> inverse (norm a - r)"
+ proof (rule le_imp_inverse_le)
+ show "0 < norm a - r" using r2 by simp
+ next
+ have "norm a - norm (X i) \<le> norm (a - X i)"
+ by (rule norm_triangle_ineq2)
+ also have "\<dots> = norm (X i - a)"
+ by (rule norm_minus_commute)
+ also have "\<dots> < r" using 1 .
+ finally show "norm a - r \<le> norm (X i)" by simp
+ qed
+ finally show "norm (inverse (X i)) \<le> inverse (norm a - r)" .
+ qed
+ thus ?thesis by (rule BfunI)
+qed
+
+lemma tendsto_inverse_lemma:
+ fixes a :: "'a::real_normed_div_algebra"
+ shows "\<lbrakk>tendsto X a F; a \<noteq> 0; eventually (\<lambda>i. X i \<noteq> 0) F\<rbrakk>
+ \<Longrightarrow> tendsto (\<lambda>i. inverse (X i)) (inverse a) F"
+apply (subst tendsto_Zfun_iff)
+apply (rule Zfun_ssubst)
+apply (erule eventually_elim1)
+apply (erule (1) inverse_diff_inverse)
+apply (rule Zfun_minus)
+apply (rule Zfun_mult_left)
+apply (rule mult.Bfun_prod_Zfun)
+apply (erule (1) Bfun_inverse)
+apply (simp add: tendsto_Zfun_iff)
+done
+
+lemma tendsto_inverse:
+ fixes a :: "'a::real_normed_div_algebra"
+ assumes X: "tendsto X a F"
+ assumes a: "a \<noteq> 0"
+ shows "tendsto (\<lambda>i. inverse (X i)) (inverse a) F"
+proof -
+ from a have "0 < norm a" by simp
+ with X have "eventually (\<lambda>i. dist (X i) a < norm a) F"
+ by (rule tendstoD)
+ then have "eventually (\<lambda>i. X i \<noteq> 0) F"
+ unfolding dist_norm by (auto elim!: eventually_elim1)
+ with X a show ?thesis
+ by (rule tendsto_inverse_lemma)
+qed
+
+lemma tendsto_divide:
+ fixes a b :: "'a::real_normed_field"
+ shows "\<lbrakk>tendsto X a F; tendsto Y b F; b \<noteq> 0\<rbrakk>
+ \<Longrightarrow> tendsto (\<lambda>n. X n / Y n) (a / b) F"
+by (simp add: mult.tendsto tendsto_inverse divide_inverse)
+
+end
--- a/src/HOL/List.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/List.thy Tue Jun 02 14:38:10 2009 +0200
@@ -2464,6 +2464,12 @@
case False with d show ?thesis by auto
qed
+lemma distinct_concat:
+ assumes "distinct xs"
+ and "\<And> ys. ys \<in> set xs \<Longrightarrow> distinct ys"
+ and "\<And> ys zs. \<lbrakk> ys \<in> set xs ; zs \<in> set xs ; ys \<noteq> zs \<rbrakk> \<Longrightarrow> set ys \<inter> set zs = {}"
+ shows "distinct (concat xs)"
+ using assms by (induct xs) auto
text {* It is best to avoid this indexed version of distinct, but
sometimes it is useful. *}
@@ -2617,6 +2623,10 @@
lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
by (induct n) auto
+lemma map_replicate_const:
+ "map (\<lambda> x. k) lst = replicate (length lst) k"
+ by (induct lst) auto
+
lemma replicate_app_Cons_same:
"(replicate n x) @ (x # xs) = x # replicate n x @ xs"
by (induct n) auto
@@ -2696,6 +2706,9 @@
"map (\<lambda>i. x) [0..<i] = replicate i x"
by (induct i) (simp_all add: replicate_append_same)
+lemma concat_replicate_trivial[simp]:
+ "concat (replicate i []) = []"
+ by (induct i) (auto simp add: map_replicate_const)
lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
by (induct n) auto
--- a/src/HOL/Ln.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Ln.thy Tue Jun 02 14:38:10 2009 +0200
@@ -343,7 +343,7 @@
done
lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"
- apply (unfold deriv_def, unfold LIM_def, clarsimp)
+ apply (unfold deriv_def, unfold LIM_eq, clarsimp)
apply (rule exI)
apply (rule conjI)
prefer 2
--- a/src/HOL/Log.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Log.thy Tue Jun 02 14:38:10 2009 +0200
@@ -248,7 +248,7 @@
qed
lemma LIMSEQ_neg_powr: "0 < s ==> (%x. (real x) powr - s) ----> 0"
- apply (unfold LIMSEQ_def)
+ apply (unfold LIMSEQ_iff)
apply clarsimp
apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI)
apply clarify
--- a/src/HOL/NSA/CLim.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/NSA/CLim.thy Tue Jun 02 14:38:10 2009 +0200
@@ -45,17 +45,25 @@
hIm_hcomplex_of_complex)
(** get this result easily now **)
-lemma LIM_Re: "f -- a --> L ==> (%x. Re(f x)) -- a --> Re(L)"
+lemma LIM_Re:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "f -- a --> L ==> (%x. Re(f x)) -- a --> Re(L)"
by (simp add: LIM_NSLIM_iff NSLIM_Re)
-lemma LIM_Im: "f -- a --> L ==> (%x. Im(f x)) -- a --> Im(L)"
+lemma LIM_Im:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "f -- a --> L ==> (%x. Im(f x)) -- a --> Im(L)"
by (simp add: LIM_NSLIM_iff NSLIM_Im)
-lemma LIM_cnj: "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L"
-by (simp add: LIM_def complex_cnj_diff [symmetric])
+lemma LIM_cnj:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L"
+by (simp add: LIM_eq complex_cnj_diff [symmetric])
-lemma LIM_cnj_iff: "((%x. cnj (f x)) -- a --> cnj L) = (f -- a --> L)"
-by (simp add: LIM_def complex_cnj_diff [symmetric])
+lemma LIM_cnj_iff:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "((%x. cnj (f x)) -- a --> cnj L) = (f -- a --> L)"
+by (simp add: LIM_eq complex_cnj_diff [symmetric])
lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
by transfer (rule refl)
@@ -74,8 +82,10 @@
approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
(** much, much easier standard proof **)
-lemma CLIM_CRLIM_iff: "(f -- x --> L) = ((%y. cmod(f y - L)) -- x --> 0)"
-by (simp add: LIM_def)
+lemma CLIM_CRLIM_iff:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "(f -- x --> L) = ((%y. cmod(f y - L)) -- x --> 0)"
+by (simp add: LIM_eq)
(* so this is nicer nonstandard proof *)
lemma NSCLIM_NSCRLIM_iff2:
@@ -92,7 +102,8 @@
done
lemma LIM_CRLIM_Re_Im_iff:
- "(f -- a --> L) = ((%x. Re(f x)) -- a --> Re(L) &
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "(f -- a --> L) = ((%x. Re(f x)) -- a --> Re(L) &
(%x. Im(f x)) -- a --> Im(L))"
by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
@@ -113,10 +124,14 @@
lemma isContCR_cmod [simp]: "isCont cmod (a)"
by (simp add: isNSCont_isCont_iff [symmetric])
-lemma isCont_Re: "isCont f a ==> isCont (%x. Re (f x)) a"
+lemma isCont_Re:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "isCont f a ==> isCont (%x. Re (f x)) a"
by (simp add: isCont_def LIM_Re)
-lemma isCont_Im: "isCont f a ==> isCont (%x. Im (f x)) a"
+lemma isCont_Im:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "isCont f a ==> isCont (%x. Im (f x)) a"
by (simp add: isCont_def LIM_Im)
subsection{* Differentiation of Natural Number Powers*}
--- a/src/HOL/NSA/HLim.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/NSA/HLim.thy Tue Jun 02 14:38:10 2009 +0200
@@ -287,7 +287,7 @@
fix r::real assume r: "0 < r"
with f obtain s where s: "0 < s" and
less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r"
- by (auto simp add: isUCont_def)
+ by (auto simp add: isUCont_def dist_norm)
from less_r have less_r':
"\<And>x y. hnorm (x - y) < star_of s
\<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
@@ -306,7 +306,7 @@
lemma isNSUCont_isUCont:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes f: "isNSUCont f" shows "isUCont f"
-proof (unfold isUCont_def, safe)
+proof (unfold isUCont_def dist_norm, safe)
fix r::real assume r: "0 < r"
have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s
\<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
--- a/src/HOL/SEQ.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/SEQ.thy Tue Jun 02 14:38:10 2009 +0200
@@ -9,27 +9,31 @@
header {* Sequences and Convergence *}
theory SEQ
-imports RealVector RComplete
+imports Limits
begin
definition
+ sequentially :: "nat filter" where
+ [code del]: "sequentially = Abs_filter (\<lambda>P. \<exists>N. \<forall>n\<ge>N. P n)"
+
+definition
Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
--{*Standard definition of sequence converging to zero*}
[code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
definition
- LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
+ LIMSEQ :: "[nat \<Rightarrow> 'a::metric_space, 'a] \<Rightarrow> bool"
("((_)/ ----> (_))" [60, 60] 60) where
--{*Standard definition of convergence of sequence*}
- [code del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
+ [code del]: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
definition
- lim :: "(nat => 'a::real_normed_vector) => 'a" where
+ lim :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a" where
--{*Standard definition of limit using choice operator*}
"lim X = (THE L. X ----> L)"
definition
- convergent :: "(nat => 'a::real_normed_vector) => bool" where
+ convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
--{*Standard definition of convergence*}
"convergent X = (\<exists>L. X ----> L)"
@@ -62,10 +66,28 @@
[code del]: "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
definition
- Cauchy :: "(nat => 'a::real_normed_vector) => bool" where
+ Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
--{*Standard definition of the Cauchy condition*}
- [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
+ [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
+
+
+subsection {* Sequentially *}
+lemma eventually_sequentially:
+ "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
+unfolding sequentially_def
+apply (rule eventually_Abs_filter)
+apply simp
+apply (clarify, rule_tac x=N in exI, simp)
+apply (clarify, rename_tac M N)
+apply (rule_tac x="max M N" in exI, simp)
+done
+
+lemma Zseq_conv_Zfun: "Zseq X \<longleftrightarrow> Zfun X sequentially"
+unfolding Zseq_def Zfun_def eventually_sequentially ..
+
+lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> tendsto X L sequentially"
+unfolding LIMSEQ_def tendsto_def eventually_sequentially ..
subsection {* Bounded Sequences *}
@@ -110,6 +132,13 @@
apply (drule_tac x="n - k" in spec, simp)
done
+lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially"
+unfolding Bfun_def eventually_sequentially
+apply (rule iffI)
+apply (simp add: Bseq_def, fast)
+apply (fast intro: BseqI2')
+done
+
subsection {* Sequences That Converge to Zero *}
@@ -134,61 +163,15 @@
assumes X: "Zseq X"
assumes Y: "\<And>n. norm (Y n) \<le> norm (X n) * K"
shows "Zseq (\<lambda>n. Y n)"
-proof (cases)
- assume K: "0 < K"
- show ?thesis
- proof (rule ZseqI)
- fix r::real assume "0 < r"
- hence "0 < r / K"
- using K by (rule divide_pos_pos)
- then obtain N where "\<forall>n\<ge>N. norm (X n) < r / K"
- using ZseqD [OF X] by fast
- hence "\<forall>n\<ge>N. norm (X n) * K < r"
- by (simp add: pos_less_divide_eq K)
- hence "\<forall>n\<ge>N. norm (Y n) < r"
- by (simp add: order_le_less_trans [OF Y])
- thus "\<exists>N. \<forall>n\<ge>N. norm (Y n) < r" ..
- qed
-next
- assume "\<not> 0 < K"
- hence K: "K \<le> 0" by (simp only: linorder_not_less)
- {
- fix n::nat
- have "norm (Y n) \<le> norm (X n) * K" by (rule Y)
- also have "\<dots> \<le> norm (X n) * 0"
- using K norm_ge_zero by (rule mult_left_mono)
- finally have "norm (Y n) = 0" by simp
- }
- thus ?thesis by (simp add: Zseq_zero)
-qed
+using X Y Zfun_imp_Zfun [of X sequentially Y K]
+unfolding Zseq_conv_Zfun by simp
lemma Zseq_le: "\<lbrakk>Zseq Y; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zseq X"
by (erule_tac K="1" in Zseq_imp_Zseq, simp)
lemma Zseq_add:
- assumes X: "Zseq X"
- assumes Y: "Zseq Y"
- shows "Zseq (\<lambda>n. X n + Y n)"
-proof (rule ZseqI)
- fix r::real assume "0 < r"
- hence r: "0 < r / 2" by simp
- obtain M where M: "\<forall>n\<ge>M. norm (X n) < r/2"
- using ZseqD [OF X r] by fast
- obtain N where N: "\<forall>n\<ge>N. norm (Y n) < r/2"
- using ZseqD [OF Y r] by fast
- show "\<exists>N. \<forall>n\<ge>N. norm (X n + Y n) < r"
- proof (intro exI allI impI)
- fix n assume n: "max M N \<le> n"
- have "norm (X n + Y n) \<le> norm (X n) + norm (Y n)"
- by (rule norm_triangle_ineq)
- also have "\<dots> < r/2 + r/2"
- proof (rule add_strict_mono)
- from M n show "norm (X n) < r/2" by simp
- from N n show "norm (Y n) < r/2" by simp
- qed
- finally show "norm (X n + Y n) < r" by simp
- qed
-qed
+ "Zseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n + Y n)"
+unfolding Zseq_conv_Zfun by (rule Zfun_add)
lemma Zseq_minus: "Zseq X \<Longrightarrow> Zseq (\<lambda>n. - X n)"
unfolding Zseq_def by simp
@@ -197,94 +180,22 @@
by (simp only: diff_minus Zseq_add Zseq_minus)
lemma (in bounded_linear) Zseq:
- assumes X: "Zseq X"
- shows "Zseq (\<lambda>n. f (X n))"
-proof -
- obtain K where "\<And>x. norm (f x) \<le> norm x * K"
- using bounded by fast
- with X show ?thesis
- by (rule Zseq_imp_Zseq)
-qed
+ "Zseq X \<Longrightarrow> Zseq (\<lambda>n. f (X n))"
+unfolding Zseq_conv_Zfun by (rule Zfun)
lemma (in bounded_bilinear) Zseq:
- assumes X: "Zseq X"
- assumes Y: "Zseq Y"
- shows "Zseq (\<lambda>n. X n ** Y n)"
-proof (rule ZseqI)
- fix r::real assume r: "0 < r"
- obtain K where K: "0 < K"
- and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
- using pos_bounded by fast
- from K have K': "0 < inverse K"
- by (rule positive_imp_inverse_positive)
- obtain M where M: "\<forall>n\<ge>M. norm (X n) < r"
- using ZseqD [OF X r] by fast
- obtain N where N: "\<forall>n\<ge>N. norm (Y n) < inverse K"
- using ZseqD [OF Y K'] by fast
- show "\<exists>N. \<forall>n\<ge>N. norm (X n ** Y n) < r"
- proof (intro exI allI impI)
- fix n assume n: "max M N \<le> n"
- have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K"
- by (rule norm_le)
- also have "norm (X n) * norm (Y n) * K < r * inverse K * K"
- proof (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero K)
- from M n show Xn: "norm (X n) < r" by simp
- from N n show Yn: "norm (Y n) < inverse K" by simp
- qed
- also from K have "r * inverse K * K = r" by simp
- finally show "norm (X n ** Y n) < r" .
- qed
-qed
+ "Zseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
+unfolding Zseq_conv_Zfun by (rule Zfun)
lemma (in bounded_bilinear) Zseq_prod_Bseq:
- assumes X: "Zseq X"
- assumes Y: "Bseq Y"
- shows "Zseq (\<lambda>n. X n ** Y n)"
-proof -
- obtain K where K: "0 \<le> K"
- and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
- using nonneg_bounded by fast
- obtain B where B: "0 < B"
- and norm_Y: "\<And>n. norm (Y n) \<le> B"
- using Y [unfolded Bseq_def] by fast
- from X show ?thesis
- proof (rule Zseq_imp_Zseq)
- fix n::nat
- have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K"
- by (rule norm_le)
- also have "\<dots> \<le> norm (X n) * B * K"
- by (intro mult_mono' order_refl norm_Y norm_ge_zero
- mult_nonneg_nonneg K)
- also have "\<dots> = norm (X n) * (B * K)"
- by (rule mult_assoc)
- finally show "norm (X n ** Y n) \<le> norm (X n) * (B * K)" .
- qed
-qed
+ "Zseq X \<Longrightarrow> Bseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
+unfolding Zseq_conv_Zfun Bseq_conv_Bfun
+by (rule Zfun_prod_Bfun)
lemma (in bounded_bilinear) Bseq_prod_Zseq:
- assumes X: "Bseq X"
- assumes Y: "Zseq Y"
- shows "Zseq (\<lambda>n. X n ** Y n)"
-proof -
- obtain K where K: "0 \<le> K"
- and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
- using nonneg_bounded by fast
- obtain B where B: "0 < B"
- and norm_X: "\<And>n. norm (X n) \<le> B"
- using X [unfolded Bseq_def] by fast
- from Y show ?thesis
- proof (rule Zseq_imp_Zseq)
- fix n::nat
- have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K"
- by (rule norm_le)
- also have "\<dots> \<le> B * norm (Y n) * K"
- by (intro mult_mono' order_refl norm_X norm_ge_zero
- mult_nonneg_nonneg K)
- also have "\<dots> = norm (Y n) * (B * K)"
- by (simp only: mult_ac)
- finally show "norm (X n ** Y n) \<le> norm (Y n) * (B * K)" .
- qed
-qed
+ "Bseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
+unfolding Zseq_conv_Zfun Bseq_conv_Bfun
+by (rule Bfun_prod_Zfun)
lemma (in bounded_bilinear) Zseq_left:
"Zseq X \<Longrightarrow> Zseq (\<lambda>n. X n ** a)"
@@ -302,38 +213,51 @@
subsection {* Limits of Sequences *}
lemma LIMSEQ_iff:
- "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
-by (rule LIMSEQ_def)
+ fixes L :: "'a::real_normed_vector"
+ shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
+unfolding LIMSEQ_def dist_norm ..
lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) ----> L) = Zseq (\<lambda>n. X n - L)"
-by (simp only: LIMSEQ_def Zseq_def)
+by (simp only: LIMSEQ_iff Zseq_def)
+
+lemma metric_LIMSEQ_I:
+ "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> L"
+by (simp add: LIMSEQ_def)
+
+lemma metric_LIMSEQ_D:
+ "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"
+by (simp add: LIMSEQ_def)
lemma LIMSEQ_I:
- "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
-by (simp add: LIMSEQ_def)
+ fixes L :: "'a::real_normed_vector"
+ shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
+by (simp add: LIMSEQ_iff)
lemma LIMSEQ_D:
- "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
-by (simp add: LIMSEQ_def)
+ fixes L :: "'a::real_normed_vector"
+ shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
+by (simp add: LIMSEQ_iff)
lemma LIMSEQ_const: "(\<lambda>n. k) ----> k"
by (simp add: LIMSEQ_def)
-lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l = (k = l)"
-by (simp add: LIMSEQ_Zseq_iff Zseq_const_iff)
+lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
+apply (safe intro!: LIMSEQ_const)
+apply (rule ccontr)
+apply (drule_tac r="dist k l" in metric_LIMSEQ_D)
+apply (simp add: zero_less_dist_iff)
+apply auto
+done
-lemma LIMSEQ_norm: "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a"
-apply (simp add: LIMSEQ_def, safe)
-apply (drule_tac x="r" in spec, safe)
-apply (rule_tac x="no" in exI, safe)
-apply (drule_tac x="n" in spec, safe)
-apply (erule order_le_less_trans [OF norm_triangle_ineq3])
-done
+lemma LIMSEQ_norm:
+ fixes a :: "'a::real_normed_vector"
+ shows "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a"
+unfolding LIMSEQ_conv_tendsto by (rule tendsto_norm)
lemma LIMSEQ_ignore_initial_segment:
"f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
-apply (rule LIMSEQ_I)
-apply (drule (1) LIMSEQ_D)
+apply (rule metric_LIMSEQ_I)
+apply (drule (1) metric_LIMSEQ_D)
apply (erule exE, rename_tac N)
apply (rule_tac x=N in exI)
apply simp
@@ -341,8 +265,8 @@
lemma LIMSEQ_offset:
"(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
-apply (rule LIMSEQ_I)
-apply (drule (1) LIMSEQ_D)
+apply (rule metric_LIMSEQ_I)
+apply (drule (1) metric_LIMSEQ_D)
apply (erule exE, rename_tac N)
apply (rule_tac x="N + k" in exI)
apply clarify
@@ -363,51 +287,50 @@
unfolding LIMSEQ_def
by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
-
-lemma add_diff_add:
- fixes a b c d :: "'a::ab_group_add"
- shows "(a + c) - (b + d) = (a - b) + (c - d)"
-by simp
+lemma LIMSEQ_add:
+ fixes a b :: "'a::real_normed_vector"
+ shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) ----> a + b"
+unfolding LIMSEQ_conv_tendsto by (rule tendsto_add)
-lemma minus_diff_minus:
- fixes a b :: "'a::ab_group_add"
- shows "(- a) - (- b) = - (a - b)"
-by simp
+lemma LIMSEQ_minus:
+ fixes a :: "'a::real_normed_vector"
+ shows "X ----> a \<Longrightarrow> (\<lambda>n. - X n) ----> - a"
+unfolding LIMSEQ_conv_tendsto by (rule tendsto_minus)
-lemma LIMSEQ_add: "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) ----> a + b"
-by (simp only: LIMSEQ_Zseq_iff add_diff_add Zseq_add)
-
-lemma LIMSEQ_minus: "X ----> a \<Longrightarrow> (\<lambda>n. - X n) ----> - a"
-by (simp only: LIMSEQ_Zseq_iff minus_diff_minus Zseq_minus)
-
-lemma LIMSEQ_minus_cancel: "(\<lambda>n. - X n) ----> - a \<Longrightarrow> X ----> a"
+lemma LIMSEQ_minus_cancel:
+ fixes a :: "'a::real_normed_vector"
+ shows "(\<lambda>n. - X n) ----> - a \<Longrightarrow> X ----> a"
by (drule LIMSEQ_minus, simp)
-lemma LIMSEQ_diff: "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b"
-by (simp add: diff_minus LIMSEQ_add LIMSEQ_minus)
+lemma LIMSEQ_diff:
+ fixes a b :: "'a::real_normed_vector"
+ shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b"
+unfolding LIMSEQ_conv_tendsto by (rule tendsto_diff)
lemma LIMSEQ_unique: "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
-by (drule (1) LIMSEQ_diff, simp add: LIMSEQ_const_iff)
+apply (rule ccontr)
+apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
+apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
+apply (clarify, rename_tac M N)
+apply (subgoal_tac "dist a b < dist a b / 2 + dist a b / 2", simp)
+apply (subgoal_tac "dist a b \<le> dist (X (max M N)) a + dist (X (max M N)) b")
+apply (erule le_less_trans, rule add_strict_mono, simp, simp)
+apply (subst dist_commute, rule dist_triangle)
+done
lemma (in bounded_linear) LIMSEQ:
"X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"
-by (simp only: LIMSEQ_Zseq_iff diff [symmetric] Zseq)
+unfolding LIMSEQ_conv_tendsto by (rule tendsto)
lemma (in bounded_bilinear) LIMSEQ:
"\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n ** Y n) ----> a ** b"
-by (simp only: LIMSEQ_Zseq_iff prod_diff_prod
- Zseq_add Zseq Zseq_left Zseq_right)
+unfolding LIMSEQ_conv_tendsto by (rule tendsto)
lemma LIMSEQ_mult:
fixes a b :: "'a::real_normed_algebra"
shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
by (rule mult.LIMSEQ)
-lemma inverse_diff_inverse:
- "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
- \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
-by (simp add: algebra_simps)
-
lemma Bseq_inverse_lemma:
fixes x :: "'a::real_normed_div_algebra"
shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
@@ -417,69 +340,15 @@
lemma Bseq_inverse:
fixes a :: "'a::real_normed_div_algebra"
- assumes X: "X ----> a"
- assumes a: "a \<noteq> 0"
- shows "Bseq (\<lambda>n. inverse (X n))"
-proof -
- from a have "0 < norm a" by simp
- hence "\<exists>r>0. r < norm a" by (rule dense)
- then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
- obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (X n - a) < r"
- using LIMSEQ_D [OF X r1] by fast
- show ?thesis
- proof (rule BseqI2' [rule_format])
- fix n assume n: "N \<le> n"
- hence 1: "norm (X n - a) < r" by (rule N)
- hence 2: "X n \<noteq> 0" using r2 by auto
- hence "norm (inverse (X n)) = inverse (norm (X n))"
- by (rule nonzero_norm_inverse)
- also have "\<dots> \<le> inverse (norm a - r)"
- proof (rule le_imp_inverse_le)
- show "0 < norm a - r" using r2 by simp
- next
- have "norm a - norm (X n) \<le> norm (a - X n)"
- by (rule norm_triangle_ineq2)
- also have "\<dots> = norm (X n - a)"
- by (rule norm_minus_commute)
- also have "\<dots> < r" using 1 .
- finally show "norm a - r \<le> norm (X n)" by simp
- qed
- finally show "norm (inverse (X n)) \<le> inverse (norm a - r)" .
- qed
-qed
-
-lemma LIMSEQ_inverse_lemma:
- fixes a :: "'a::real_normed_div_algebra"
- shows "\<lbrakk>X ----> a; a \<noteq> 0; \<forall>n. X n \<noteq> 0\<rbrakk>
- \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a"
-apply (subst LIMSEQ_Zseq_iff)
-apply (simp add: inverse_diff_inverse nonzero_imp_inverse_nonzero)
-apply (rule Zseq_minus)
-apply (rule Zseq_mult_left)
-apply (rule mult.Bseq_prod_Zseq)
-apply (erule (1) Bseq_inverse)
-apply (simp add: LIMSEQ_Zseq_iff)
-done
+ shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
+unfolding LIMSEQ_conv_tendsto Bseq_conv_Bfun
+by (rule Bfun_inverse)
lemma LIMSEQ_inverse:
fixes a :: "'a::real_normed_div_algebra"
- assumes X: "X ----> a"
- assumes a: "a \<noteq> 0"
- shows "(\<lambda>n. inverse (X n)) ----> inverse a"
-proof -
- from a have "0 < norm a" by simp
- then obtain k where "\<forall>n\<ge>k. norm (X n - a) < norm a"
- using LIMSEQ_D [OF X] by fast
- hence "\<forall>n\<ge>k. X n \<noteq> 0" by auto
- hence k: "\<forall>n. X (n + k) \<noteq> 0" by simp
-
- from X have "(\<lambda>n. X (n + k)) ----> a"
- by (rule LIMSEQ_ignore_initial_segment)
- hence "(\<lambda>n. inverse (X (n + k))) ----> inverse a"
- using a k by (rule LIMSEQ_inverse_lemma)
- thus "(\<lambda>n. inverse (X n)) ----> inverse a"
- by (rule LIMSEQ_offset)
-qed
+ shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a"
+unfolding LIMSEQ_conv_tendsto
+by (rule tendsto_inverse)
lemma LIMSEQ_divide:
fixes a b :: "'a::real_normed_field"
@@ -492,6 +361,7 @@
by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult)
lemma LIMSEQ_setsum:
+ fixes L :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
proof (cases "finite S")
@@ -534,39 +404,40 @@
by (simp add: setprod_def LIMSEQ_const)
qed
-lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b"
+lemma LIMSEQ_add_const:
+ fixes a :: "'a::real_normed_vector"
+ shows "f ----> a ==> (%n.(f n + b)) ----> a + b"
by (simp add: LIMSEQ_add LIMSEQ_const)
(* FIXME: delete *)
lemma LIMSEQ_add_minus:
- "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
+ fixes a b :: "'a::real_normed_vector"
+ shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
by (simp only: LIMSEQ_add LIMSEQ_minus)
-lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n - b)) ----> a - b"
+lemma LIMSEQ_diff_const:
+ fixes a b :: "'a::real_normed_vector"
+ shows "f ----> a ==> (%n.(f n - b)) ----> a - b"
by (simp add: LIMSEQ_diff LIMSEQ_const)
-lemma LIMSEQ_diff_approach_zero:
- "g ----> L ==> (%x. f x - g x) ----> 0 ==>
- f ----> L"
- apply (drule LIMSEQ_add)
- apply assumption
- apply simp
-done
+lemma LIMSEQ_diff_approach_zero:
+ fixes L :: "'a::real_normed_vector"
+ shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
+by (drule (1) LIMSEQ_add, simp)
-lemma LIMSEQ_diff_approach_zero2:
- "f ----> L ==> (%x. f x - g x) ----> 0 ==>
- g ----> L";
- apply (drule LIMSEQ_diff)
- apply assumption
- apply simp
-done
+lemma LIMSEQ_diff_approach_zero2:
+ fixes L :: "'a::real_normed_vector"
+ shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L";
+by (drule (1) LIMSEQ_diff, simp)
text{*A sequence tends to zero iff its abs does*}
-lemma LIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) ----> 0) = (X ----> 0)"
-by (simp add: LIMSEQ_def)
+lemma LIMSEQ_norm_zero:
+ fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+ shows "((\<lambda>n. norm (X n)) ----> 0) \<longleftrightarrow> (X ----> 0)"
+by (simp add: LIMSEQ_iff)
lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> (0::real))"
-by (simp add: LIMSEQ_def)
+by (simp add: LIMSEQ_iff)
lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
by (drule LIMSEQ_norm, simp)
@@ -653,7 +524,9 @@
lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
-lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))"
+lemma convergent_minus_iff:
+ fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+ shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
apply (simp add: convergent_def)
apply (auto dest: LIMSEQ_minus)
apply (drule LIMSEQ_minus, auto)
@@ -1119,20 +992,35 @@
subsection {* Cauchy Sequences *}
-lemma CauchyI:
- "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X"
+lemma metric_CauchyI:
+ "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
+by (simp add: Cauchy_def)
+
+lemma metric_CauchyD:
+ "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
by (simp add: Cauchy_def)
+lemma Cauchy_iff:
+ fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+ shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
+unfolding Cauchy_def dist_norm ..
+
+lemma CauchyI:
+ fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+ shows "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X"
+by (simp add: Cauchy_iff)
+
lemma CauchyD:
- "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
-by (simp add: Cauchy_def)
+ fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+ shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
+by (simp add: Cauchy_iff)
lemma Cauchy_subseq_Cauchy:
"\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)"
-apply (auto simp add: Cauchy_def)
-apply (drule_tac x=e in spec, clarify)
-apply (rule_tac x=M in exI, clarify)
-apply (blast intro: seq_suble le_trans dest!: spec)
+apply (auto simp add: Cauchy_def)
+apply (drule_tac x=e in spec, clarify)
+apply (rule_tac x=M in exI, clarify)
+apply (blast intro: le_trans [OF _ seq_suble] dest!: spec)
done
subsubsection {* Cauchy Sequences are Bounded *}
@@ -1149,7 +1037,7 @@
done
lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
-apply (simp add: Cauchy_def)
+apply (simp add: Cauchy_iff)
apply (drule spec, drule mp, rule zero_less_one, safe)
apply (drule_tac x="M" in spec, simp)
apply (drule lemmaCauchy)
@@ -1167,22 +1055,21 @@
theorem LIMSEQ_imp_Cauchy:
assumes X: "X ----> a" shows "Cauchy X"
-proof (rule CauchyI)
+proof (rule metric_CauchyI)
fix e::real assume "0 < e"
hence "0 < e/2" by simp
- with X have "\<exists>N. \<forall>n\<ge>N. norm (X n - a) < e/2" by (rule LIMSEQ_D)
- then obtain N where N: "\<forall>n\<ge>N. norm (X n - a) < e/2" ..
- show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < e"
+ with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D)
+ then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" ..
+ show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e"
proof (intro exI allI impI)
fix m assume "N \<le> m"
- hence m: "norm (X m - a) < e/2" using N by fast
+ hence m: "dist (X m) a < e/2" using N by fast
fix n assume "N \<le> n"
- hence n: "norm (X n - a) < e/2" using N by fast
- have "norm (X m - X n) = norm ((X m - a) - (X n - a))" by simp
- also have "\<dots> \<le> norm (X m - a) + norm (X n - a)"
- by (rule norm_triangle_ineq4)
- also from m n have "\<dots> < e" by(simp add:field_simps)
- finally show "norm (X m - X n) < e" .
+ hence n: "dist (X n) a < e/2" using N by fast
+ have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a"
+ by (rule dist_triangle2)
+ also from m n have "\<dots> < e" by simp
+ finally show "dist (X m) (X n) < e" .
qed
qed
@@ -1311,7 +1198,7 @@
lemma convergent_subseq_convergent:
fixes X :: "nat \<Rightarrow> 'a::banach"
shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)"
- by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric])
+ by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric])
subsection {* Power Sequences *}
--- a/src/HOL/Series.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Series.thy Tue Jun 02 14:38:10 2009 +0200
@@ -160,7 +160,7 @@
lemma series_zero:
"(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
-apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
+apply (simp add: sums_def LIMSEQ_iff diff_minus[symmetric], safe)
apply (rule_tac x = n in exI)
apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong)
done
@@ -264,7 +264,7 @@
"[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
apply (drule summable_sums)
apply (simp only: sums_def sumr_group)
-apply (unfold LIMSEQ_def, safe)
+apply (unfold LIMSEQ_iff, safe)
apply (drule_tac x="r" in spec, safe)
apply (rule_tac x="no" in exI, safe)
apply (drule_tac x="n*k" in spec)
@@ -361,7 +361,7 @@
lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f ----> 0"
apply (drule summable_convergent_sumr_iff [THEN iffD1])
apply (drule convergent_Cauchy)
-apply (simp only: Cauchy_def LIMSEQ_def, safe)
+apply (simp only: Cauchy_iff LIMSEQ_iff, safe)
apply (drule_tac x="r" in spec, safe)
apply (rule_tac x="M" in exI, safe)
apply (drule_tac x="Suc n" in spec, simp)
@@ -371,7 +371,7 @@
lemma summable_Cauchy:
"summable (f::nat \<Rightarrow> 'a::banach) =
(\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. norm (setsum f {m..<n}) < e)"
-apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def, safe)
+apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_iff, safe)
apply (drule spec, drule (1) mp)
apply (erule exE, rule_tac x="M" in exI, clarify)
apply (rule_tac x="m" and y="n" in linorder_le_cases)
--- a/src/HOL/Tools/datatype_package.ML Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Tools/datatype_package.ML Tue Jun 02 14:38:10 2009 +0200
@@ -386,7 +386,8 @@
val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
descr sorts thy9;
- val dt_infos = map (make_dt_info NONE (flat descr) sorts induct reccomb_names rec_thms)
+ val dt_infos = map
+ (make_dt_info (SOME new_type_names) (flat descr) sorts induct reccomb_names rec_thms)
((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
@@ -586,7 +587,7 @@
val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
[] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
- fun prep_dt_spec (tvs, tname, mx, constrs) (dts', constr_syntax, sorts, i) =
+ fun prep_dt_spec ((tvs, tname, mx, constrs), tname') (dts', constr_syntax, sorts, i) =
let
fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
let
@@ -595,7 +596,7 @@
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs))
in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
- Sign.full_name_path tmp_thy (Binding.name_of tname))
+ Sign.full_name_path tmp_thy tname')
(Binding.map_name (Syntax.const_name mx') cname),
map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
@@ -616,7 +617,8 @@
" in datatype " ^ quote (Binding.str_of tname))
end;
- val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
+ val (dts', constr_syntax, sorts', i) =
+ fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
val dt_info = get_datatypes thy;
val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
--- a/src/HOL/Transcendental.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Transcendental.thy Tue Jun 02 14:38:10 2009 +0200
@@ -438,7 +438,7 @@
assumes k: "0 < (k::real)"
assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
shows "f -- 0 --> 0"
-unfolding LIM_def diff_0_right
+unfolding LIM_eq diff_0_right
proof (safe)
let ?h = "of_real (k / 2)::'a"
have "?h \<noteq> 0" and "norm ?h < k" using k by simp_all
@@ -2145,7 +2145,7 @@
lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
apply (cut_tac LIM_cos_div_sin)
-apply (simp only: LIM_def)
+apply (simp only: LIM_eq)
apply (drule_tac x = "inverse y" in spec, safe, force)
apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
apply (rule_tac x = "(pi/2) - e" in exI)
--- a/src/HOL/Transitive_Closure.thy Tue Jun 02 13:15:16 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy Tue Jun 02 14:38:10 2009 +0200
@@ -698,6 +698,9 @@
apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
done
+lemma rel_pow_add: "R ^^ (m+n) = R^^n O R^^m"
+by(induct n) auto
+
lemma rtrancl_imp_UN_rel_pow:
assumes "p \<in> R^*"
shows "p \<in> (\<Union>n. R ^^ n)"