src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 55775 1557a391a858
parent 55522 23d2cbac6dce
child 55927 30c41a8eca0e
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Feb 27 15:19:09 2014 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Feb 27 16:07:21 2014 +0000
     1.3 @@ -569,10 +569,7 @@
     1.4      fix K
     1.5      assume K: "K \<subseteq> Collect ?L"
     1.6      have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
     1.7 -      apply (rule set_eqI)
     1.8 -      apply (simp add: Ball_def image_iff)
     1.9 -      apply metis
    1.10 -      done
    1.11 +      by blast
    1.12      from K[unfolded th0 subset_image_iff]
    1.13      obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk"
    1.14        by blast
    1.15 @@ -595,21 +592,11 @@
    1.16  
    1.17  lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
    1.18    unfolding closedin_def topspace_subtopology
    1.19 -  apply (simp add: openin_subtopology)
    1.20 -  apply (rule iffI)
    1.21 -  apply clarify
    1.22 -  apply (rule_tac x="topspace U - T" in exI)
    1.23 -  apply auto
    1.24 -  done
    1.25 +  by (auto simp add: openin_subtopology)
    1.26  
    1.27  lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
    1.28    unfolding openin_subtopology
    1.29 -  apply (rule iffI, clarify)
    1.30 -  apply (frule openin_subset[of U])
    1.31 -  apply blast
    1.32 -  apply (rule exI[where x="topspace U"])
    1.33 -  apply auto
    1.34 -  done
    1.35 +  by auto (metis IntD1 in_mono openin_subset)
    1.36  
    1.37  lemma subtopology_superset:
    1.38    assumes UV: "topspace U \<subseteq> V"
    1.39 @@ -695,11 +682,7 @@
    1.40  
    1.41  lemma closed_closedin_trans:
    1.42    "closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T"
    1.43 -  apply (subgoal_tac "S \<inter> T = T" )
    1.44 -  apply auto
    1.45 -  apply (frule closedin_closed_Int[of T S])
    1.46 -  apply simp
    1.47 -  done
    1.48 +  by (metis closedin_closed inf.absorb2)
    1.49  
    1.50  lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
    1.51    by (auto simp add: closedin_closed)
    1.52 @@ -720,16 +703,10 @@
    1.53      apply clarsimp
    1.54      apply (rule_tac x="d - dist x a" in exI)
    1.55      apply (clarsimp simp add: less_diff_eq)
    1.56 -    apply (erule rev_bexI)
    1.57 -    apply (rule_tac x=d in exI, clarify)
    1.58 -    apply (erule le_less_trans [OF dist_triangle])
    1.59 -    done
    1.60 +    by (metis dist_commute dist_triangle_lt)
    1.61    assume ?rhs then have 2: "S = U \<inter> T"
    1.62 -    unfolding T_def
    1.63 -    apply auto
    1.64 -    apply (drule (1) bspec, erule rev_bexI)
    1.65 -    apply auto
    1.66 -    done
    1.67 +    unfolding T_def 
    1.68 +    by auto (metis dist_self)
    1.69    from 1 2 show ?lhs
    1.70      unfolding openin_open open_dist by fast
    1.71  qed
    1.72 @@ -811,12 +788,6 @@
    1.73    "a - b \<ge> c \<longleftrightarrow> a \<ge> c + b"
    1.74    by arith+
    1.75  
    1.76 -lemma open_vimage: (* TODO: move to Topological_Spaces.thy *)
    1.77 -  assumes "open s" and "continuous_on UNIV f"
    1.78 -  shows "open (vimage f s)"
    1.79 -  using assms unfolding continuous_on_open_vimage [OF open_UNIV]
    1.80 -  by simp
    1.81 -
    1.82  lemma open_ball [intro, simp]: "open (ball x e)"
    1.83  proof -
    1.84    have "open (dist x -` {..<e})"
    1.85 @@ -955,9 +926,7 @@
    1.86        e1 \<noteq> {} \<and>
    1.87        e2 \<noteq> {})"
    1.88    unfolding connected_def openin_open
    1.89 -  apply safe
    1.90 -  apply blast+
    1.91 -  done
    1.92 +  by blast
    1.93  
    1.94  lemma exists_diff:
    1.95    fixes P :: "'a set \<Rightarrow> bool"
    1.96 @@ -984,9 +953,7 @@
    1.97    have "\<not> connected S \<longleftrightarrow>
    1.98      (\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
    1.99      unfolding connected_def openin_open closedin_closed
   1.100 -    apply (subst exists_diff)
   1.101 -    apply blast
   1.102 -    done
   1.103 +    by (metis double_complement)
   1.104    then have th0: "connected S \<longleftrightarrow>
   1.105      \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
   1.106      (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)")
   1.107 @@ -1430,13 +1397,8 @@
   1.108  next
   1.109    assume "\<not> a islimpt S"
   1.110    then show "trivial_limit (at a within S)"
   1.111 -    unfolding trivial_limit_def
   1.112 -    unfolding eventually_at_topological
   1.113 -    unfolding islimpt_def
   1.114 -    apply clarsimp
   1.115 -    apply (rule_tac x=T in exI)
   1.116 -    apply auto
   1.117 -    done
   1.118 +    unfolding trivial_limit_def eventually_at_topological islimpt_def
   1.119 +    by metis
   1.120  qed
   1.121  
   1.122  lemma trivial_limit_at_iff: "trivial_limit (at a) \<longleftrightarrow> \<not> a islimpt UNIV"
   1.123 @@ -1926,9 +1888,7 @@
   1.124  lemma closed_sequential_limits:
   1.125    fixes S :: "'a::first_countable_topology set"
   1.126    shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)"
   1.127 -  using closure_sequential [where 'a='a] closure_closed [where 'a='a]
   1.128 -    closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a]
   1.129 -  by metis
   1.130 +by (metis closure_sequential closure_subset_eq subset_iff)
   1.131  
   1.132  lemma closure_approachable:
   1.133    fixes S :: "'a::metric_space set"
   1.134 @@ -2483,13 +2443,7 @@
   1.135  
   1.136  lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
   1.137    unfolding bounded_def
   1.138 -  apply safe
   1.139 -  apply (rule_tac x="dist a x + e" in exI)
   1.140 -  apply clarify
   1.141 -  apply (drule (1) bspec)
   1.142 -  apply (erule order_trans [OF dist_triangle add_left_mono])
   1.143 -  apply auto
   1.144 -  done
   1.145 +  by auto (metis add_commute add_le_cancel_right dist_commute dist_triangle_le)
   1.146  
   1.147  lemma bounded_iff: "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x \<le> a)"
   1.148    unfolding bounded_any_center [where a=0]
   1.149 @@ -2499,10 +2453,7 @@
   1.150    assumes "\<forall>x\<in>s. abs (x::real) \<le> B"
   1.151    shows "bounded s"
   1.152    unfolding bounded_def dist_real_def
   1.153 -  apply (rule_tac x=0 in exI)
   1.154 -  using assms
   1.155 -  apply auto
   1.156 -  done
   1.157 +  by (metis abs_minus_commute assms diff_0_right)
   1.158  
   1.159  lemma bounded_empty [simp]: "bounded {}"
   1.160    by (simp add: bounded_def)
   1.161 @@ -2550,17 +2501,7 @@
   1.162  
   1.163  lemma bounded_Un[simp]: "bounded (S \<union> T) \<longleftrightarrow> bounded S \<and> bounded T"
   1.164    apply (auto simp add: bounded_def)
   1.165 -  apply (rename_tac x y r s)
   1.166 -  apply (rule_tac x=x in exI)
   1.167 -  apply (rule_tac x="max r (dist x y + s)" in exI)
   1.168 -  apply (rule ballI)
   1.169 -  apply safe
   1.170 -  apply (drule (1) bspec)
   1.171 -  apply simp
   1.172 -  apply (drule (1) bspec)
   1.173 -  apply (rule max.coboundedI2)
   1.174 -  apply (erule order_trans [OF dist_triangle add_left_mono])
   1.175 -  done
   1.176 +  by (metis Un_iff add_le_cancel_left dist_triangle le_max_iff_disj max.order_iff)
   1.177  
   1.178  lemma bounded_Union[intro]: "finite F \<Longrightarrow> \<forall>S\<in>F. bounded S \<Longrightarrow> bounded (\<Union>F)"
   1.179    by (induct rule: finite_induct[of F]) auto
   1.180 @@ -3847,25 +3788,11 @@
   1.181  
   1.182  lemma bounded_fst: "bounded s \<Longrightarrow> bounded (fst ` s)"
   1.183    unfolding bounded_def
   1.184 -  apply clarify
   1.185 -  apply (rule_tac x="a" in exI)
   1.186 -  apply (rule_tac x="e" in exI)
   1.187 -  apply clarsimp
   1.188 -  apply (drule (1) bspec)
   1.189 -  apply (simp add: dist_Pair_Pair)
   1.190 -  apply (erule order_trans [OF real_sqrt_sum_squares_ge1])
   1.191 -  done
   1.192 +  by (metis (erased, hide_lams) dist_fst_le image_iff order_trans)
   1.193  
   1.194  lemma bounded_snd: "bounded s \<Longrightarrow> bounded (snd ` s)"
   1.195    unfolding bounded_def
   1.196 -  apply clarify
   1.197 -  apply (rule_tac x="b" in exI)
   1.198 -  apply (rule_tac x="e" in exI)
   1.199 -  apply clarsimp
   1.200 -  apply (drule (1) bspec)
   1.201 -  apply (simp add: dist_Pair_Pair)
   1.202 -  apply (erule order_trans [OF real_sqrt_sum_squares_ge2])
   1.203 -  done
   1.204 +  by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans)
   1.205  
   1.206  instance prod :: (heine_borel, heine_borel) heine_borel
   1.207  proof
   1.208 @@ -3916,7 +3843,6 @@
   1.209        using assms unfolding compact_def by blast
   1.210  
   1.211      note lr' = seq_suble [OF lr(2)]
   1.212 -
   1.213      {
   1.214        fix e :: real
   1.215        assume "e > 0"
   1.216 @@ -4434,10 +4360,8 @@
   1.217    "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.218    unfolding continuous_within and Lim_within
   1.219    apply auto
   1.220 -  unfolding dist_nz[symmetric]
   1.221 -  apply (auto del: allE elim!:allE)
   1.222 -  apply(rule_tac x=d in exI)
   1.223 -  apply auto
   1.224 +  apply (metis dist_nz dist_self)
   1.225 +  apply blast
   1.226    done
   1.227  
   1.228  lemma continuous_at_eps_delta:
   1.229 @@ -4521,11 +4445,7 @@
   1.230    "continuous_on s f \<longleftrightarrow>
   1.231      (\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
   1.232    unfolding continuous_on_def Lim_within
   1.233 -  apply (intro ball_cong [OF refl] all_cong ex_cong)
   1.234 -  apply (rename_tac y, case_tac "y = x")
   1.235 -  apply simp
   1.236 -  apply (simp add: dist_nz)
   1.237 -  done
   1.238 +  by (metis dist_pos_lt dist_self)
   1.239  
   1.240  definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::metric_space \<Rightarrow> 'b::metric_space) \<Rightarrow> bool"
   1.241    where "uniformly_continuous_on s f \<longleftrightarrow>
   1.242 @@ -4552,10 +4472,7 @@
   1.243  
   1.244  lemma continuous_on_interior:
   1.245    "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
   1.246 -  apply (erule interiorE)
   1.247 -  apply (drule (1) continuous_on_subset)
   1.248 -  apply (simp add: continuous_on_eq_continuous_at)
   1.249 -  done
   1.250 +  by (metis continuous_on_eq_continuous_at continuous_on_subset interiorE)
   1.251  
   1.252  lemma continuous_on_eq:
   1.253    "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"