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    {