# HG changeset patch
# User huffman
# Date 1314651047 25200
# Node ID 08ad27488983fb374be3c7b4934d54a5426d2256
# Parent  f23ac1a679d1ec91076ea3f170bd80e0bdec3bc5
simplify some proofs

diff -r f23ac1a679d1 -r 08ad27488983 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 29 22:10:08 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 29 13:50:47 2011 -0700
@@ -443,27 +443,24 @@
   obtains y where "y \<in> S" and "y \<in> T" and "y \<noteq> x"
   using assms unfolding islimpt_def by auto
 
-lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T ==> x islimpt T" by (auto simp add: islimpt_def)
+lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)"
+  unfolding islimpt_def eventually_at_topological by auto
+
+lemma islimpt_subset: "\<lbrakk>x islimpt S; S \<subseteq> T\<rbrakk> \<Longrightarrow> x islimpt T"
+  unfolding islimpt_def by fast
 
 lemma islimpt_approachable:
   fixes x :: "'a::metric_space"
   shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)"
-  unfolding islimpt_def
-  apply auto
-  apply(erule_tac x="ball x e" in allE)
-  apply auto
-  apply(rule_tac x=y in bexI)
-  apply (auto simp add: dist_commute)
-  apply (simp add: open_dist, drule (1) bspec)
-  apply (clarify, drule spec, drule (1) mp, auto)
-  done
+  unfolding islimpt_iff_eventually eventually_at by fast
 
 lemma islimpt_approachable_le:
   fixes x :: "'a::metric_space"
   shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)"
   unfolding islimpt_approachable
-  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 
+  using approachable_lt_le [where f="\<lambda>y. dist y x" and P="\<lambda>y. y \<notin> S \<or> y = x",
+    THEN arg_cong [where f=Not]]
+  by (simp add: Bex_def conj_commute conj_left_commute)
 
 lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}"
   unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast)
@@ -1058,65 +1055,11 @@
   using assms by (simp only: at_within_open)
 
 lemma Lim_within_LIMSEQ:
-  fixes a :: real and L :: "'a::metric_space"
+  fixes a :: "'a::metric_space"
   assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   shows "(X ---> L) (at a within T)"
-proof (rule ccontr)
-  assume "\<not> (X ---> L) (at a within T)"
-  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"
-    unfolding tendsto_iff eventually_within dist_norm by (simp add: not_less[symmetric])
-  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
-
-  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"
-  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"
-    using r by (simp add: Bex_def)
-  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"
-    by (rule someI_ex)
-  hence F1: "\<And>n. ?F n \<in> T \<and> ?F n \<noteq> a"
-    and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
-    and F3: "\<And>n. dist (X (?F n)) L \<ge> r"
-    by fast+
-
-  have "?F ----> a"
-  proof (rule LIMSEQ_I, unfold real_norm_def)
-      fix e::real
-      assume "0 < e"
-        (* choose no such that inverse (real (Suc n)) < e *)
-      then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
-      then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
-      show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
-      proof (intro exI allI impI)
-        fix n
-        assume mlen: "m \<le> n"
-        have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
-          by (rule F2)
-        also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
-          using mlen by auto
-        also from nodef have
-          "inverse (real (Suc m)) < e" .
-        finally show "\<bar>?F n - a\<bar> < e" .
-      qed
-  qed
-  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`
-  ultimately have "(\<lambda>n. X (?F n)) ----> L" using F1 by simp
-  
-  moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
-  proof -
-    {
-      fix no::nat
-      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 "dist (X (?F n)) L \<ge> r"
-        by (rule F3)
-      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> dist (X (?F n)) L \<ge> r)" by simp
-    with r 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
+  using assms unfolding tendsto_def [where l=L]
+  by (simp add: sequentially_imp_eventually_within)
 
 lemma Lim_right_bound:
   fixes f :: "real \<Rightarrow> real"
@@ -1160,21 +1103,18 @@
 proof
   assume ?lhs
   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"
-    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
-  { fix n::nat
-    have "f (inverse (real n + 1)) \<in> S - {x}" using f by auto
-  }
-  moreover
-  { fix e::real assume "e>0"
-    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
-    then obtain N::nat where "inverse (real (N + 1)) < e" by auto
-    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)
-    moreover have "\<forall>n\<ge>N. dist (f (inverse (real n + 1))) x < (inverse (real n + 1))" using f `e>0` by auto
-    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
-  }
-  hence " ((\<lambda>n. f (inverse (real n + 1))) ---> x) sequentially"
-    unfolding Lim_sequentially using f by auto
-  ultimately show ?rhs apply (rule_tac x="(\<lambda>n::nat. f (inverse (real n + 1)))" in exI) by auto
+    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
+  let ?I = "\<lambda>n. inverse (real (Suc n))"
+  have "\<forall>n. f (?I n) \<in> S - {x}" using f by simp
+  moreover have "(\<lambda>n. f (?I n)) ----> x"
+  proof (rule metric_tendsto_imp_tendsto)
+    show "?I ----> 0"
+      by (rule LIMSEQ_inverse_real_of_nat)
+    show "eventually (\<lambda>n. dist (f (?I n)) x \<le> dist (?I n) 0) sequentially"
+      by (simp add: norm_conv_dist [symmetric] less_imp_le f)
+  qed
+  ultimately show ?rhs by fast
 next
   assume ?rhs
   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
@@ -1331,7 +1271,7 @@
   shows "netlimit (at a) = a"
   apply (subst within_UNIV[symmetric])
   using netlimit_within[of a UNIV]
-  by (simp add: trivial_limit_at within_UNIV)
+  by (simp add: within_UNIV)
 
 lemma lim_within_interior:
   "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
@@ -1480,8 +1420,7 @@
 lemma seq_offset:
   assumes "(f ---> l) sequentially"
   shows "((\<lambda>i. f (i + k)) ---> l) sequentially"
-  using assms unfolding tendsto_def
-  by clarify (rule sequentially_offset, simp)
+  using assms by (rule LIMSEQ_ignore_initial_segment) (* FIXME: redundant *)
 
 lemma seq_offset_neg:
   "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
@@ -1494,21 +1433,10 @@
 
 lemma seq_offset_rev:
   "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
-  apply (rule topological_tendstoI)
-  apply (drule (2) topological_tendstoD)
-  apply (simp only: eventually_sequentially)
-  apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k \<and> (n - k) + k = n")
-  by metis arith
+  by (rule LIMSEQ_offset) (* FIXME: redundant *)
 
 lemma seq_harmonic: "((\<lambda>n. inverse (real n)) ---> 0) sequentially"
-proof-
-  { fix e::real assume "e>0"
-    hence "\<exists>N::nat. \<forall>n::nat\<ge>N. inverse (real n) < e"
-      using real_arch_inv[of e] apply auto apply(rule_tac x=n in exI)
-      by (metis le_imp_inverse_le not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7))
-  }
-  thus ?thesis unfolding Lim_sequentially dist_norm by simp
-qed
+  using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc)
 
 subsection {* More properties of closed balls *}
 
@@ -3154,7 +3082,7 @@
 lemma continuous_within_eps_delta:
   "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)"
   unfolding continuous_within and Lim_within
-  apply auto unfolding dist_nz[THEN sym] apply(auto elim!:allE) apply(rule_tac x=d in exI) by auto
+  apply auto unfolding dist_nz[THEN sym] apply(auto del: allE elim!:allE) apply(rule_tac x=d in exI) by auto
 
 lemma continuous_at_eps_delta: "continuous (at x) f \<longleftrightarrow>  (\<forall>e>0. \<exists>d>0.
                            \<forall>x'. dist x' x < d --> dist(f x')(f x) < e)"
@@ -4408,7 +4336,7 @@
   note * = this
   { fix x y assume "x\<in>s" "y\<in>s"  hence "s \<noteq> {}" by auto
     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`
-      by simp (blast intro!: Sup_upper *) }
+      by simp (blast del: Sup_upper intro!: * Sup_upper) }
   moreover
   { fix d::real assume "d>0" "d < diameter s"
     hence "s\<noteq>{}" unfolding diameter_def by auto
@@ -4667,39 +4595,26 @@
   "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i < b$$i)"
   unfolding interval_eq_empty[of a b] by fastsimp+
 
-lemma interval_sing: fixes a :: "'a::ordered_euclidean_space" shows
- "{a .. a} = {a}" "{a<..<a} = {}"
-  apply(auto simp add: set_eq_iff euclidean_eq[where 'a='a] eucl_less[where 'a='a] eucl_le[where 'a='a])
-  apply (simp add: order_eq_iff) apply(rule_tac x=0 in exI) by (auto simp add: not_less less_imp_le)
+lemma interval_sing:
+  fixes a :: "'a::ordered_euclidean_space"
+  shows "{a .. a} = {a}" and "{a<..<a} = {}"
+  unfolding set_eq_iff mem_interval eq_iff [symmetric]
+  by (auto simp add: euclidean_eq[where 'a='a] eq_commute
+    eucl_less[where 'a='a] eucl_le[where 'a='a])
 
 lemma subset_interval_imp: fixes a :: "'a::ordered_euclidean_space" shows
  "(\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}" and
  "(\<forall>i<DIM('a). a$$i < c$$i \<and> d$$i < b$$i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}" and
  "(\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}" and
  "(\<forall>i<DIM('a). a$$i \<le> c$$i \<and> d$$i \<le> b$$i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
-  unfolding subset_eq[unfolded Ball_def] unfolding mem_interval 
-  by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)
-
-lemma interval_open_subset_closed:  fixes a :: "'a::ordered_euclidean_space" shows
- "{a<..<b} \<subseteq> {a .. b}"
-proof(simp add: subset_eq, rule)
-  fix x
-  assume x:"x \<in>{a<..<b}"
-  { fix i assume "i<DIM('a)"
-    hence "a $$ i \<le> x $$ i"
-      using x order_less_imp_le[of "a$$i" "x$$i"] 
-      by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
-  }
-  moreover
-  { fix i assume "i<DIM('a)"
-    hence "x $$ i \<le> b $$ i"
-      using x order_less_imp_le[of "x$$i" "b$$i"]
-      by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
-  }
-  ultimately
-  show "a \<le> x \<and> x \<le> b"
-    by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
-qed
+  unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
+  by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
+
+lemma interval_open_subset_closed:
+  fixes a :: "'a::ordered_euclidean_space"
+  shows "{a<..<b} \<subseteq> {a .. b}"
+  unfolding subset_eq [unfolded Ball_def] mem_interval
+  by (fast intro: less_imp_le)
 
 lemma subset_interval: fixes a :: "'a::ordered_euclidean_space" shows
  "{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
@@ -4825,7 +4740,7 @@
                      "(x + (e / 2) *\<^sub>R basis i) $$ i \<le> b $$ i"
         using e[THEN spec[where x="x - (e/2) *\<^sub>R basis i"]]
         and   e[THEN spec[where x="x + (e/2) *\<^sub>R basis i"]]
-        unfolding mem_interval by (auto elim!: allE[where x=i])
+        unfolding mem_interval using i by blast+
       hence "a $$ i < x $$ i" and "x $$ i < b $$ i" unfolding euclidean_simps
         unfolding basis_component using `e>0` i by auto  }
     hence "x \<in> {a<..<b}" unfolding mem_interval by auto  }
@@ -5009,9 +4924,8 @@
 
 lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
   "is_interval {a<..<b}" (is ?th2) proof -
-  have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
   show ?th1 ?th2  unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
-    by(meson order_trans le_less_trans less_le_trans *)+ qed
+    by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
 
 lemma is_interval_empty:
  "is_interval {}"