src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44584 08ad27488983
parent 44571 bd91b77c4cd6
child 44628 bd17b7543af1
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 29 22:10:08 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 29 13:50:47 2011 -0700
     1.3 @@ -443,27 +443,24 @@
     1.4    obtains y where "y \<in> S" and "y \<in> T" and "y \<noteq> x"
     1.5    using assms unfolding islimpt_def by auto
     1.6  
     1.7 -lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T ==> x islimpt T" by (auto simp add: islimpt_def)
     1.8 +lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)"
     1.9 +  unfolding islimpt_def eventually_at_topological by auto
    1.10 +
    1.11 +lemma islimpt_subset: "\<lbrakk>x islimpt S; S \<subseteq> T\<rbrakk> \<Longrightarrow> x islimpt T"
    1.12 +  unfolding islimpt_def by fast
    1.13  
    1.14  lemma islimpt_approachable:
    1.15    fixes x :: "'a::metric_space"
    1.16    shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)"
    1.17 -  unfolding islimpt_def
    1.18 -  apply auto
    1.19 -  apply(erule_tac x="ball x e" in allE)
    1.20 -  apply auto
    1.21 -  apply(rule_tac x=y in bexI)
    1.22 -  apply (auto simp add: dist_commute)
    1.23 -  apply (simp add: open_dist, drule (1) bspec)
    1.24 -  apply (clarify, drule spec, drule (1) mp, auto)
    1.25 -  done
    1.26 +  unfolding islimpt_iff_eventually eventually_at by fast
    1.27  
    1.28  lemma islimpt_approachable_le:
    1.29    fixes x :: "'a::metric_space"
    1.30    shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)"
    1.31    unfolding islimpt_approachable
    1.32 -  using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
    1.33 -  by metis 
    1.34 +  using approachable_lt_le [where f="\<lambda>y. dist y x" and P="\<lambda>y. y \<notin> S \<or> y = x",
    1.35 +    THEN arg_cong [where f=Not]]
    1.36 +  by (simp add: Bex_def conj_commute conj_left_commute)
    1.37  
    1.38  lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}"
    1.39    unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast)
    1.40 @@ -1058,65 +1055,11 @@
    1.41    using assms by (simp only: at_within_open)
    1.42  
    1.43  lemma Lim_within_LIMSEQ:
    1.44 -  fixes a :: real and L :: "'a::metric_space"
    1.45 +  fixes a :: "'a::metric_space"
    1.46    assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
    1.47    shows "(X ---> L) (at a within T)"
    1.48 -proof (rule ccontr)
    1.49 -  assume "\<not> (X ---> L) (at a within T)"
    1.50 -  hence "\<exists>r>0. \<forall>s>0. \<exists>x\<in>T. x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> r \<le> dist (X x) L"
    1.51 -    unfolding tendsto_iff eventually_within dist_norm by (simp add: not_less[symmetric])
    1.52 -  then obtain r where r: "r > 0" "\<And>s. s > 0 \<Longrightarrow> \<exists>x\<in>T-{a}. \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r" by blast
    1.53 -
    1.54 -  let ?F = "\<lambda>n::nat. SOME x. x \<in> T \<and> x \<noteq> a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
    1.55 -  have "\<And>n. \<exists>x. x \<in> T \<and> x \<noteq> a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
    1.56 -    using r by (simp add: Bex_def)
    1.57 -  hence F: "\<And>n. ?F n \<in> T \<and> ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> dist (X (?F n)) L \<ge> r"
    1.58 -    by (rule someI_ex)
    1.59 -  hence F1: "\<And>n. ?F n \<in> T \<and> ?F n \<noteq> a"
    1.60 -    and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
    1.61 -    and F3: "\<And>n. dist (X (?F n)) L \<ge> r"
    1.62 -    by fast+
    1.63 -
    1.64 -  have "?F ----> a"
    1.65 -  proof (rule LIMSEQ_I, unfold real_norm_def)
    1.66 -      fix e::real
    1.67 -      assume "0 < e"
    1.68 -        (* choose no such that inverse (real (Suc n)) < e *)
    1.69 -      then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
    1.70 -      then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
    1.71 -      show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
    1.72 -      proof (intro exI allI impI)
    1.73 -        fix n
    1.74 -        assume mlen: "m \<le> n"
    1.75 -        have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
    1.76 -          by (rule F2)
    1.77 -        also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
    1.78 -          using mlen by auto
    1.79 -        also from nodef have
    1.80 -          "inverse (real (Suc m)) < e" .
    1.81 -        finally show "\<bar>?F n - a\<bar> < e" .
    1.82 -      qed
    1.83 -  qed
    1.84 -  moreover note `\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L`
    1.85 -  ultimately have "(\<lambda>n. X (?F n)) ----> L" using F1 by simp
    1.86 -  
    1.87 -  moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
    1.88 -  proof -
    1.89 -    {
    1.90 -      fix no::nat
    1.91 -      obtain n where "n = no + 1" by simp
    1.92 -      then have nolen: "no \<le> n" by simp
    1.93 -        (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
    1.94 -      have "dist (X (?F n)) L \<ge> r"
    1.95 -        by (rule F3)
    1.96 -      with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast
    1.97 -    }
    1.98 -    then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp
    1.99 -    with r have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto
   1.100 -    thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less)
   1.101 -  qed
   1.102 -  ultimately show False by simp
   1.103 -qed
   1.104 +  using assms unfolding tendsto_def [where l=L]
   1.105 +  by (simp add: sequentially_imp_eventually_within)
   1.106  
   1.107  lemma Lim_right_bound:
   1.108    fixes f :: "real \<Rightarrow> real"
   1.109 @@ -1160,21 +1103,18 @@
   1.110  proof
   1.111    assume ?lhs
   1.112    then obtain f where f:"\<forall>y. y>0 \<longrightarrow> f y \<in> S \<and> f y \<noteq> x \<and> dist (f y) x < y"
   1.113 -    unfolding islimpt_approachable using choice[of "\<lambda>e y. e>0 \<longrightarrow> y\<in>S \<and> y\<noteq>x \<and> dist y x < e"] by auto
   1.114 -  { fix n::nat
   1.115 -    have "f (inverse (real n + 1)) \<in> S - {x}" using f by auto
   1.116 -  }
   1.117 -  moreover
   1.118 -  { fix e::real assume "e>0"
   1.119 -    hence "\<exists>N::nat. inverse (real (N + 1)) < e" using real_arch_inv[of e] apply (auto simp add: Suc_pred') apply(rule_tac x="n - 1" in exI) by auto
   1.120 -    then obtain N::nat where "inverse (real (N + 1)) < e" by auto
   1.121 -    hence "\<forall>n\<ge>N. inverse (real n + 1) < e" by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero)
   1.122 -    moreover have "\<forall>n\<ge>N. dist (f (inverse (real n + 1))) x < (inverse (real n + 1))" using f `e>0` by auto
   1.123 -    ultimately have "\<exists>N::nat. \<forall>n\<ge>N. dist (f (inverse (real n + 1))) x < e" apply(rule_tac x=N in exI) apply auto apply(erule_tac x=n in allE)+ by auto
   1.124 -  }
   1.125 -  hence " ((\<lambda>n. f (inverse (real n + 1))) ---> x) sequentially"
   1.126 -    unfolding Lim_sequentially using f by auto
   1.127 -  ultimately show ?rhs apply (rule_tac x="(\<lambda>n::nat. f (inverse (real n + 1)))" in exI) by auto
   1.128 +    unfolding islimpt_approachable
   1.129 +    using choice[of "\<lambda>e y. e>0 \<longrightarrow> y\<in>S \<and> y\<noteq>x \<and> dist y x < e"] by auto
   1.130 +  let ?I = "\<lambda>n. inverse (real (Suc n))"
   1.131 +  have "\<forall>n. f (?I n) \<in> S - {x}" using f by simp
   1.132 +  moreover have "(\<lambda>n. f (?I n)) ----> x"
   1.133 +  proof (rule metric_tendsto_imp_tendsto)
   1.134 +    show "?I ----> 0"
   1.135 +      by (rule LIMSEQ_inverse_real_of_nat)
   1.136 +    show "eventually (\<lambda>n. dist (f (?I n)) x \<le> dist (?I n) 0) sequentially"
   1.137 +      by (simp add: norm_conv_dist [symmetric] less_imp_le f)
   1.138 +  qed
   1.139 +  ultimately show ?rhs by fast
   1.140  next
   1.141    assume ?rhs
   1.142    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
   1.143 @@ -1331,7 +1271,7 @@
   1.144    shows "netlimit (at a) = a"
   1.145    apply (subst within_UNIV[symmetric])
   1.146    using netlimit_within[of a UNIV]
   1.147 -  by (simp add: trivial_limit_at within_UNIV)
   1.148 +  by (simp add: within_UNIV)
   1.149  
   1.150  lemma lim_within_interior:
   1.151    "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
   1.152 @@ -1480,8 +1420,7 @@
   1.153  lemma seq_offset:
   1.154    assumes "(f ---> l) sequentially"
   1.155    shows "((\<lambda>i. f (i + k)) ---> l) sequentially"
   1.156 -  using assms unfolding tendsto_def
   1.157 -  by clarify (rule sequentially_offset, simp)
   1.158 +  using assms by (rule LIMSEQ_ignore_initial_segment) (* FIXME: redundant *)
   1.159  
   1.160  lemma seq_offset_neg:
   1.161    "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
   1.162 @@ -1494,21 +1433,10 @@
   1.163  
   1.164  lemma seq_offset_rev:
   1.165    "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
   1.166 -  apply (rule topological_tendstoI)
   1.167 -  apply (drule (2) topological_tendstoD)
   1.168 -  apply (simp only: eventually_sequentially)
   1.169 -  apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k \<and> (n - k) + k = n")
   1.170 -  by metis arith
   1.171 +  by (rule LIMSEQ_offset) (* FIXME: redundant *)
   1.172  
   1.173  lemma seq_harmonic: "((\<lambda>n. inverse (real n)) ---> 0) sequentially"
   1.174 -proof-
   1.175 -  { fix e::real assume "e>0"
   1.176 -    hence "\<exists>N::nat. \<forall>n::nat\<ge>N. inverse (real n) < e"
   1.177 -      using real_arch_inv[of e] apply auto apply(rule_tac x=n in exI)
   1.178 -      by (metis le_imp_inverse_le not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7))
   1.179 -  }
   1.180 -  thus ?thesis unfolding Lim_sequentially dist_norm by simp
   1.181 -qed
   1.182 +  using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc)
   1.183  
   1.184  subsection {* More properties of closed balls *}
   1.185  
   1.186 @@ -3154,7 +3082,7 @@
   1.187  lemma continuous_within_eps_delta:
   1.188    "continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s.  dist x' x < d --> dist (f x') (f x) < e)"
   1.189    unfolding continuous_within and Lim_within
   1.190 -  apply auto unfolding dist_nz[THEN sym] apply(auto elim!:allE) apply(rule_tac x=d in exI) by auto
   1.191 +  apply auto unfolding dist_nz[THEN sym] apply(auto del: allE elim!:allE) apply(rule_tac x=d in exI) by auto
   1.192  
   1.193  lemma continuous_at_eps_delta: "continuous (at x) f \<longleftrightarrow>  (\<forall>e>0. \<exists>d>0.
   1.194                             \<forall>x'. dist x' x < d --> dist(f x')(f x) < e)"
   1.195 @@ -4408,7 +4336,7 @@
   1.196    note * = this
   1.197    { fix x y assume "x\<in>s" "y\<in>s"  hence "s \<noteq> {}" by auto
   1.198      have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s`
   1.199 -      by simp (blast intro!: Sup_upper *) }
   1.200 +      by simp (blast del: Sup_upper intro!: * Sup_upper) }
   1.201    moreover
   1.202    { fix d::real assume "d>0" "d < diameter s"
   1.203      hence "s\<noteq>{}" unfolding diameter_def by auto
   1.204 @@ -4667,39 +4595,26 @@
   1.205    "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i < b$$i)"
   1.206    unfolding interval_eq_empty[of a b] by fastsimp+
   1.207  
   1.208 -lemma interval_sing: fixes a :: "'a::ordered_euclidean_space" shows
   1.209 - "{a .. a} = {a}" "{a<..<a} = {}"
   1.210 -  apply(auto simp add: set_eq_iff euclidean_eq[where 'a='a] eucl_less[where 'a='a] eucl_le[where 'a='a])
   1.211 -  apply (simp add: order_eq_iff) apply(rule_tac x=0 in exI) by (auto simp add: not_less less_imp_le)
   1.212 +lemma interval_sing:
   1.213 +  fixes a :: "'a::ordered_euclidean_space"
   1.214 +  shows "{a .. a} = {a}" and "{a<..<a} = {}"
   1.215 +  unfolding set_eq_iff mem_interval eq_iff [symmetric]
   1.216 +  by (auto simp add: euclidean_eq[where 'a='a] eq_commute
   1.217 +    eucl_less[where 'a='a] eucl_le[where 'a='a])
   1.218  
   1.219  lemma subset_interval_imp: fixes a :: "'a::ordered_euclidean_space" shows
   1.220   "(\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}" and
   1.221   "(\<forall>i<DIM('a). a$$i < c$$i \<and> d$$i < b$$i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}" and
   1.222   "(\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}" and
   1.223   "(\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
   1.224 -  unfolding subset_eq[unfolded Ball_def] unfolding mem_interval 
   1.225 -  by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)
   1.226 -
   1.227 -lemma interval_open_subset_closed:  fixes a :: "'a::ordered_euclidean_space" shows
   1.228 - "{a<..<b} \<subseteq> {a .. b}"
   1.229 -proof(simp add: subset_eq, rule)
   1.230 -  fix x
   1.231 -  assume x:"x \<in>{a<..<b}"
   1.232 -  { fix i assume "i<DIM('a)"
   1.233 -    hence "a $$ i \<le> x $$ i"
   1.234 -      using x order_less_imp_le[of "a$$i" "x$$i"] 
   1.235 -      by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
   1.236 -  }
   1.237 -  moreover
   1.238 -  { fix i assume "i<DIM('a)"
   1.239 -    hence "x $$ i \<le> b $$ i"
   1.240 -      using x order_less_imp_le[of "x$$i" "b$$i"]
   1.241 -      by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
   1.242 -  }
   1.243 -  ultimately
   1.244 -  show "a \<le> x \<and> x \<le> b"
   1.245 -    by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
   1.246 -qed
   1.247 +  unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
   1.248 +  by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
   1.249 +
   1.250 +lemma interval_open_subset_closed:
   1.251 +  fixes a :: "'a::ordered_euclidean_space"
   1.252 +  shows "{a<..<b} \<subseteq> {a .. b}"
   1.253 +  unfolding subset_eq [unfolded Ball_def] mem_interval
   1.254 +  by (fast intro: less_imp_le)
   1.255  
   1.256  lemma subset_interval: fixes a :: "'a::ordered_euclidean_space" shows
   1.257   "{c .. d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i<DIM('a). c$$i \<le> d$$i) --> (\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i)" (is ?th1) and
   1.258 @@ -4825,7 +4740,7 @@
   1.259                       "(x + (e / 2) *\<^sub>R basis i) $$ i \<le> b $$ i"
   1.260          using e[THEN spec[where x="x - (e/2) *\<^sub>R basis i"]]
   1.261          and   e[THEN spec[where x="x + (e/2) *\<^sub>R basis i"]]
   1.262 -        unfolding mem_interval by (auto elim!: allE[where x=i])
   1.263 +        unfolding mem_interval using i by blast+
   1.264        hence "a $$ i < x $$ i" and "x $$ i < b $$ i" unfolding euclidean_simps
   1.265          unfolding basis_component using `e>0` i by auto  }
   1.266      hence "x \<in> {a<..<b}" unfolding mem_interval by auto  }
   1.267 @@ -5009,9 +4924,8 @@
   1.268  
   1.269  lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
   1.270    "is_interval {a<..<b}" (is ?th2) proof -
   1.271 -  have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
   1.272    show ?th1 ?th2  unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
   1.273 -    by(meson order_trans le_less_trans less_le_trans *)+ qed
   1.274 +    by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
   1.275  
   1.276  lemma is_interval_empty:
   1.277   "is_interval {}"