simplify proof of compact_imp_bounded
authorhuffman
Thu Jan 17 08:31:16 2013 -0800 (2013-01-17)
changeset 50955ada575c605e1
parent 50954 7bc58677860e
child 50963 23ed79fc2b4d
simplify proof of compact_imp_bounded
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 19:20:56 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 08:31:16 2013 -0800
     1.3 @@ -2205,6 +2205,9 @@
     1.4  lemma bounded_Union[intro]: "finite F \<Longrightarrow> (\<forall>S\<in>F. bounded S) \<Longrightarrow> bounded(\<Union>F)"
     1.5    by (induct rule: finite_induct[of F], auto)
     1.6  
     1.7 +lemma bounded_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. bounded (B x) \<Longrightarrow> bounded (\<Union>x\<in>A. B x)"
     1.8 +  by (induct set: finite, auto)
     1.9 +
    1.10  lemma bounded_insert [simp]: "bounded (insert x S) \<longleftrightarrow> bounded S"
    1.11  proof -
    1.12    have "\<forall>y\<in>{x}. dist x y \<le> 0" by simp
    1.13 @@ -2583,21 +2586,10 @@
    1.14    have "compact U" "\<forall>x\<in>U. open (ball x 1)" "U \<subseteq> (\<Union>x\<in>U. ball x 1)" using assms by auto
    1.15    then obtain D where D: "D \<subseteq> U" "finite D" "U \<subseteq> (\<Union>x\<in>D. ball x 1)"
    1.16      by (elim compactE_image)
    1.17 -  def d \<equiv> "SOME d. d \<in> D"
    1.18 -  show "bounded U"
    1.19 -    unfolding bounded_def
    1.20 -  proof (intro exI, safe)
    1.21 -    fix x assume "x \<in> U"
    1.22 -    with D obtain d' where "d' \<in> D" "x \<in> ball d' 1" by auto
    1.23 -    moreover have "dist d x \<le> dist d d' + dist d' x"
    1.24 -      using dist_triangle[of d x d'] by (simp add: dist_commute)
    1.25 -    moreover
    1.26 -    from `x\<in>U` D have "d \<in> D"
    1.27 -      unfolding d_def by (rule_tac someI_ex) auto
    1.28 -    ultimately
    1.29 -    show "dist d x \<le> Max ((\<lambda>d'. dist d d' + 1) ` D)"
    1.30 -      using D by (subst Max_ge_iff) (auto intro!: bexI[of _ d'])
    1.31 -  qed
    1.32 +  from `finite D` have "bounded (\<Union>x\<in>D. ball x 1)"
    1.33 +    by (simp add: bounded_UN)
    1.34 +  thus "bounded U" using `U \<subseteq> (\<Union>x\<in>D. ball x 1)` 
    1.35 +    by (rule bounded_subset)
    1.36  qed
    1.37  
    1.38  text{* In particular, some common special cases. *}