src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 55522 23d2cbac6dce parent 55415 05f5fdb8d093 child 55775 1557a391a858
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Feb 16 18:46:13 2014 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Feb 16 21:09:47 2014 +0100
1.3 @@ -139,12 +139,12 @@
1.4      and f :: "'a set \<Rightarrow> 'a"
1.5    assumes "topological_basis B"
1.6      and choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
1.7 -  shows "(\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X))"
1.8 +  shows "\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X)"
1.9  proof (intro allI impI)
1.10    fix X :: "'a set"
1.11    assume "open X" and "X \<noteq> {}"
1.12    from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]]
1.13 -  guess B' . note B' = this
1.14 +  obtain B' where "B' \<in> B" "f X \<in> B'" "B' \<subseteq> X" .
1.15    then show "\<exists>B'\<in>B. f B' \<in> X"
1.16      by (auto intro!: choosefrom_basis)
1.17  qed
1.18 @@ -166,8 +166,12 @@
1.19      from open_prod_elim[OF `open S` this]
1.20      obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
1.21        by (metis mem_Sigma_iff)
1.22 -    moreover from topological_basisE[OF A a] guess A0 .
1.23 -    moreover from topological_basisE[OF B b] guess B0 .
1.24 +    moreover
1.25 +    from A a obtain A0 where "A0 \<in> A" "x \<in> A0" "A0 \<subseteq> a"
1.26 +      by (rule topological_basisE)
1.27 +    moreover
1.28 +    from B b obtain B0 where "B0 \<in> B" "y \<in> B0" "B0 \<subseteq> b"
1.29 +      by (rule topological_basisE)
1.30      ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)"
1.31        by (intro UN_I[of "(A0, B0)"]) auto
1.32    qed auto
1.33 @@ -225,7 +229,12 @@
1.34      "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
1.35      "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A"
1.36  proof atomize_elim
1.37 -  from first_countable_basisE[of x] guess A' . note A' = this
1.38 +  obtain A' where A':
1.39 +    "countable A'"
1.40 +    "\<And>a. a \<in> A' \<Longrightarrow> x \<in> a"
1.41 +    "\<And>a. a \<in> A' \<Longrightarrow> open a"
1.42 +    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A'. a \<subseteq> S"
1.43 +    by (rule first_countable_basisE) blast
1.44    def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)"
1.45    then show "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and>
1.46          (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)"
1.47 @@ -273,8 +282,18 @@
1.48  instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
1.49  proof
1.50    fix x :: "'a \<times> 'b"
1.51 -  from first_countable_basisE[of "fst x"] guess A :: "'a set set" . note A = this
1.52 -  from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this
1.53 +  obtain A where A:
1.54 +      "countable A"
1.55 +      "\<And>a. a \<in> A \<Longrightarrow> fst x \<in> a"
1.56 +      "\<And>a. a \<in> A \<Longrightarrow> open a"
1.57 +      "\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
1.58 +    by (rule first_countable_basisE[of "fst x"]) blast
1.59 +  obtain B where B:
1.60 +      "countable B"
1.61 +      "\<And>a. a \<in> B \<Longrightarrow> snd x \<in> a"
1.62 +      "\<And>a. a \<in> B \<Longrightarrow> open a"
1.63 +      "\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S"
1.64 +    by (rule first_countable_basisE[of "snd x"]) blast
1.65    show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set.
1.66      (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
1.67    proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe)
1.68 @@ -286,10 +305,14 @@
1.69    next
1.70      fix S
1.71      assume "open S" "x \<in> S"
1.72 -    from open_prod_elim[OF this] guess a' b' . note a'b' = this
1.73 -    moreover from a'b' A(4)[of a'] B(4)[of b']
1.74 -    obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto
1.75 -    ultimately show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
1.76 +    then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S"
1.77 +      by (rule open_prod_elim)
1.78 +    moreover
1.79 +    from a'b' A(4)[of a'] B(4)[of b']
1.80 +    obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'"
1.81 +      by auto
1.82 +    ultimately
1.83 +    show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
1.84        by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
1.85    qed (simp add: A B)
1.86  qed
1.87 @@ -328,7 +351,9 @@
1.88        next
1.89          case (UN K)
1.90          then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto
1.91 -        then guess k unfolding bchoice_iff ..
1.92 +        then obtain k where
1.93 +            "\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> UNION (k ka) Inter = ka"
1.94 +          unfolding bchoice_iff ..
1.95          then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K"
1.96            by (intro exI[of _ "UNION K k"]) auto
1.97        next
1.98 @@ -849,14 +874,16 @@
1.99      from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
1.100      show "?th i" by auto
1.101    qed
1.102 -  from choice[OF this] guess a .. note a = this
1.103 +  from choice[OF this] obtain a where
1.104 +    a: "\<forall>xa. a xa \<in> \<rat> \<and> a xa < x \<bullet> xa \<and> x \<bullet> xa - a xa < e'" ..
1.105    have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
1.106    proof
1.107      fix i
1.108      from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
1.109      show "?th i" by auto
1.110    qed
1.111 -  from choice[OF this] guess b .. note b = this
1.112 +  from choice[OF this] obtain b where
1.113 +    b: "\<forall>xa. b xa \<in> \<rat> \<and> x \<bullet> xa < b xa \<and> b xa - x \<bullet> xa < e'" ..
1.114    let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
1.115    show ?thesis
1.116    proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
1.117 @@ -1585,7 +1612,11 @@
1.118      (is "?lhs = ?rhs")
1.119  proof
1.120    assume ?lhs
1.121 -  from countable_basis_at_decseq[of x] guess A . note A = this
1.122 +  from countable_basis_at_decseq[of x] obtain A where A:
1.123 +      "\<And>i. open (A i)"
1.124 +      "\<And>i. x \<in> A i"
1.125 +      "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
1.126 +    by blast
1.127    def f \<equiv> "\<lambda>n. SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
1.128    {
1.129      fix n
1.130 @@ -2759,8 +2790,12 @@
1.131    assumes l: "\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> range f)"
1.132    shows "\<exists>r. subseq r \<and> (f \<circ> r) ----> l"
1.133  proof -
1.134 -  from countable_basis_at_decseq[of l] guess A . note A = this
1.135 -
1.136 +  from countable_basis_at_decseq[of l]
1.137 +  obtain A where A:
1.138 +      "\<And>i. open (A i)"
1.139 +      "\<And>i. l \<in> A i"
1.140 +      "\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
1.141 +    by blast
1.142    def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> f j \<in> A (Suc n)"
1.143    {
1.144      fix n i
1.145 @@ -3043,8 +3078,10 @@
1.146    show "?R (\<lambda>x. True)"
1.147      by (rule exI[of _ "{}"]) (simp add: le_fun_def)
1.148  next
1.149 -  fix P Q assume "?R P" then guess X ..
1.150 -  moreover assume "?R Q" then guess Y ..
1.151 +  fix P Q
1.152 +  assume "?R P" then guess X ..
1.153 +  moreover
1.154 +  assume "?R Q" then guess Y ..
1.155    ultimately show "?R (\<lambda>x. P x \<and> Q x)"
1.156      by (intro exI[of _ "X \<union> Y"]) auto
1.157  next
1.158 @@ -3221,7 +3258,8 @@
1.159      using * by metis
1.160    then have "\<forall>t\<in>T. \<exists>a\<in>A. t \<inter> U \<subseteq> a"
1.161      by (auto simp: C_def)
1.162 -  then guess f unfolding bchoice_iff Bex_def ..
1.163 +  then obtain f where "\<forall>t\<in>T. f t \<in> A \<and> t \<inter> U \<subseteq> f t"
1.164 +    unfolding bchoice_iff Bex_def ..
1.165    with T show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
1.166      unfolding C_def by (intro exI[of _ "f`T"]) fastforce
1.167  qed
1.168 @@ -3231,9 +3269,10 @@
1.169  proof (rule countably_compact_imp_compact)
1.170    fix T and x :: 'a
1.171    assume "open T" "x \<in> T"
1.172 -  from topological_basisE[OF is_basis this] guess b .
1.173 +  from topological_basisE[OF is_basis this] obtain b where
1.174 +    "b \<in> (SOME B. countable B \<and> topological_basis B)" "x \<in> b" "b \<subseteq> T" .
1.175    then show "\<exists>b\<in>SOME B. countable B \<and> topological_basis B. x \<in> b \<and> b \<inter> U \<subseteq> T"
1.176 -    by auto
1.177 +    by blast
1.178  qed (insert countable_basis topological_basis_open[OF is_basis], auto)
1.179
1.180  lemma countably_compact_eq_compact:
1.181 @@ -3354,7 +3393,12 @@
1.182    obtain x where "x \<in> U" and x: "inf (nhds x) (filtermap X sequentially) \<noteq> bot" (is "?F \<noteq> _")
1.183      using `compact U` by (auto simp: compact_filter)
1.184
1.185 -  from countable_basis_at_decseq[of x] guess A . note A = this
1.186 +  from countable_basis_at_decseq[of x]
1.187 +  obtain A where A:
1.188 +      "\<And>i. open (A i)"
1.189 +      "\<And>i. x \<in> A i"
1.190 +      "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
1.191 +    by blast
1.192    def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> X j \<in> A (Suc n)"
1.193    {
1.194      fix n i
1.195 @@ -3426,7 +3470,9 @@
1.196    moreover
1.197    from `countable t` have "countable C"
1.198      unfolding C_def by (auto intro: countable_Collect_finite_subset)
1.199 -  ultimately guess D by (rule countably_compactE)
1.200 +  ultimately
1.201 +  obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> \<Union>D"
1.202 +    by (rule countably_compactE)
1.203    then obtain E where E: "E \<subseteq> {F. finite F \<and> F \<subseteq> t }" "finite E"
1.204      and s: "s \<subseteq> (\<Union>F\<in>E. interior (F \<union> (- t)))"
1.205      by (metis (lifting) Union_image_eq finite_subset_image C_def)
1.206 @@ -3569,7 +3615,8 @@
1.207    shows "compact s"
1.208  proof -
1.209    from seq_compact_imp_totally_bounded[OF `seq_compact s`]
1.210 -  guess f unfolding choice_iff' .. note f = this
1.211 +  obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` f e)"
1.212 +    unfolding choice_iff' ..
1.213    def K \<equiv> "(\<lambda>(x, r). ball x r) ` ((\<Union>e \<in> \<rat> \<inter> {0 <..}. f e) \<times> \<rat>)"
1.214    have "countably_compact s"
1.215      using `seq_compact s` by (rule seq_compact_imp_countably_compact)
1.216 @@ -3944,7 +3991,9 @@
1.217          assume "infinite {n. f n \<in> U}"
1.218          then have "\<exists>b\<in>k (e n). infinite {i\<in>{n. f n \<in> U}. f i \<in> ball b (e n)}"
1.219            using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq)
1.220 -        then guess a ..
1.221 +        then obtain a where
1.222 +          "a \<in> k (e n)"
1.223 +          "infinite {i \<in> {n. f n \<in> U}. f i \<in> ball a (e n)}" ..
1.224          then have "\<exists>b. infinite {i. f i \<in> b} \<and> (\<exists>x. b \<subseteq> ball x (e n) \<inter> U)"
1.225            by (intro exI[of _ "ball a (e n) \<inter> U"] exI[of _ a]) (auto simp: ac_simps)
1.226          from someI_ex[OF this]
1.227 @@ -6617,7 +6666,7 @@
1.228    shows "\<exists>S\<subseteq>A. card S = n"
1.229  proof cases
1.230    assume "finite A"
1.231 -  from ex_bij_betw_nat_finite[OF this] guess f .. note f = this
1.232 +  from ex_bij_betw_nat_finite[OF this] obtain f where f: "bij_betw f {0..<card A} A" ..
1.233    moreover from f `n \<le> card A` have "{..< n} \<subseteq> {..< card A}" "inj_on f {..< n}"
1.234      by (auto simp: bij_betw_def intro: subset_inj_on)
1.235    ultimately have "f ` {..< n} \<subseteq> A" "card (f ` {..< n}) = n"
1.236 @@ -6642,7 +6691,11 @@
1.237        inj_on f {x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
1.238      using dim_substandard[of d] t d assms
1.239      by (intro subspace_isomorphism[OF subspace_substandard[of "\<lambda>i. i \<notin> d"]]) (auto simp: inner_Basis)
1.240 -  then guess f by (elim exE conjE) note f = this
1.241 +  then obtain f where f:
1.242 +      "linear f"
1.243 +      "f ` {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} = s"
1.244 +      "inj_on f {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
1.245 +    by blast
1.246    interpret f: bounded_linear f
1.247      using f unfolding linear_conv_bounded_linear by auto
1.248    {
```