author wenzelm Sun Feb 16 21:09:47 2014 +0100 (2014-02-16) changeset 55522 23d2cbac6dce parent 55521 241c6a2fdda1 child 55523 9429e7b5b827
tuned proofs;
```     1.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Feb 16 18:46:13 2014 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Feb 16 21:09:47 2014 +0100
1.3 @@ -622,7 +622,7 @@
1.4      apply auto
1.5      done
1.6    then obtain a where a: "a \<in> s" "\<forall>x\<in>s. \<forall>j. x j \<le> a j" ..
1.7 -  show ?thesis
1.8 +  show ?thesis
1.9      apply (rule_tac x = a in bexI)
1.10    proof
1.11      fix x
1.12 @@ -1755,15 +1755,26 @@
1.13    have **: "\<And>s' a'. ksimplex p n s' \<Longrightarrow> a' \<in> s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s"
1.14    proof -
1.15      case goal1
1.16 -    guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note exta = this[rule_format]
1.17 +    obtain a0 a1 where exta:
1.18 +        "a0 \<in> s"
1.19 +        "a1 \<in> s"
1.20 +        "a0 \<noteq> a1"
1.21 +        "\<And>x. x \<in> s \<Longrightarrow> kle n a0 x \<and> kle n x a1"
1.22 +        "\<And>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
1.23 +      by (rule ksimplex_extrema_strong[OF assms(1,3)]) blast
1.24      have a: "a = a1"
1.25        apply (rule ksimplex_fix_plane_0[OF assms(2,4-5)])
1.26        using exta(1-2,5)
1.27        apply auto
1.28        done
1.29      moreover
1.30 -    guess b0 b1 by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)])
1.31 -    note extb = this[rule_format]
1.32 +    obtain b0 b1 where extb:
1.33 +        "b0 \<in> s'"
1.34 +        "b1 \<in> s'"
1.35 +        "b0 \<noteq> b1"
1.36 +        "\<And>x. x \<in> s' \<Longrightarrow> kle n b0 x \<and> kle n x b1"
1.37 +        "\<And>i. b1 i = (if i \<in> {1..n} then b0 i + 1 else b0 i)"
1.38 +      by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) blast
1.39      have a': "a' = b1"
1.40        apply (rule ksimplex_fix_plane_0[OF goal1(2) assms(4), of b0])
1.41        unfolding goal1(3)
1.42 @@ -1815,15 +1826,26 @@
1.43    have lem: "\<And>s' a'. ksimplex p n s' \<Longrightarrow> a'\<in>s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s"
1.44    proof -
1.45      case goal1
1.46 -    guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note exta = this [rule_format]
1.47 +    obtain a0 a1 where exta:
1.48 +        "a0 \<in> s"
1.49 +        "a1 \<in> s"
1.50 +        "a0 \<noteq> a1"
1.51 +        "\<And>x. x \<in> s \<Longrightarrow> kle n a0 x \<and> kle n x a1"
1.52 +        "\<And>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
1.53 +      by (rule ksimplex_extrema_strong[OF assms(1,3)]) blast
1.54      have a: "a = a0"
1.55        apply (rule ksimplex_fix_plane_p[OF assms(1-2,4-5) exta(1,2)])
1.56        unfolding exta
1.57        apply auto
1.58        done
1.59      moreover
1.60 -    guess b0 b1 by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)])
1.61 -    note extb = this [rule_format]
1.62 +    obtain b0 b1 where extb:
1.63 +        "b0 \<in> s'"
1.64 +        "b1 \<in> s'"
1.65 +        "b0 \<noteq> b1"
1.66 +        "\<And>x. x \<in> s' \<Longrightarrow> kle n b0 x \<and> kle n x b1"
1.67 +        "\<And>i. b1 i = (if i \<in> {1..n} then b0 i + 1 else b0 i)"
1.68 +      by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) blast
1.69      have a': "a' = b0"
1.70        apply (rule ksimplex_fix_plane_p[OF goal1(1-2) assms(4), of _ b1])
1.71        unfolding goal1 extb
1.72 @@ -1891,7 +1913,13 @@
1.73      then show False
1.74        by auto
1.75    qed
1.76 -  guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note a0a1 = this
1.77 +  obtain a0 a1 where a0a1:
1.78 +      "a0 \<in> s"
1.79 +      "a1 \<in> s"
1.80 +      "a0 \<noteq> a1"
1.81 +      "\<forall>x\<in>s. kle n a0 x \<and> kle n x a1"
1.82 +      "\<forall>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
1.83 +    by (rule ksimplex_extrema_strong[OF assms(1,3)])
1.84    {
1.85      assume "a = a0"
1.86      have *: "\<And>P Q. P \<or> Q \<Longrightarrow> \<not> P \<Longrightarrow> Q"
1.87 @@ -1910,8 +1938,10 @@
1.88        apply (rule_tac *[OF ksimplex_successor[OF assms(1-2),unfolded `a=a0`]])
1.89        apply auto
1.90        done
1.91 -    then guess a2 ..
1.92 -    from this(2) guess k .. note k = this note a2 =`a2 \<in> s`
1.93 +    then
1.94 +    obtain a2 k where a2: "a2 \<in> s"
1.95 +      and k: "k \<in> {1..n}" "\<forall>j. a2 j = (if j = k then a0 j + 1 else a0 j)"
1.96 +      by blast
1.97      def a3 \<equiv> "\<lambda>j. if j = k then a1 j + 1 else a1 j"
1.98      have "a3 \<notin> s"
1.99      proof
1.100 @@ -1983,8 +2013,8 @@
1.101                using `a1 \<in> s` ksimplexD(4)[OF assms(1)]
1.102                by auto
1.103            next
1.104 -            guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] ..
1.105 -            note a4 = this
1.106 +            obtain a4 where a4: "a4 \<in> s - {a}" "a4 k \<noteq> p"
1.107 +              using assms(5) k(1) by blast
1.108              have "a2 k \<le> a4 k"
1.109                using lem3[OF a4(1)[unfolded `a = a0`],THEN kle_imp_pointwise]
1.110                by auto
1.111 @@ -2028,9 +2058,11 @@
1.112        have lem4: "\<And>x. x\<in>s \<Longrightarrow> x \<noteq> a0 \<Longrightarrow> kle n x a3"
1.113        proof -
1.114          case goal1
1.115 -        guess kk using a0a1(4)[rule_format, OF `x\<in>s`,THEN conjunct2,unfolded kle_def]
1.116 -          by (elim exE conjE)
1.117 -        note kk = this
1.118 +        obtain kk where kk:
1.119 +            "kk \<subseteq> {1..n}"
1.120 +            "\<forall>j. a1 j = x j + (if j \<in> kk then 1 else 0)"
1.121 +          using a0a1(4)[rule_format, OF `x\<in>s`,THEN conjunct2,unfolded kle_def]
1.122 +          by blast
1.123          have "k \<notin> kk"
1.124          proof
1.125            assume "k \<in> kk"
1.126 @@ -2109,9 +2141,16 @@
1.127        unfolding mem_Collect_eq
1.128      proof (erule conjE)
1.129        fix s'
1.130 -      assume as: "ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
1.131 -      from this(2) guess a' .. note a' = this
1.132 -      guess a_min a_max by (rule ksimplex_extrema_strong[OF as assms(3)]) note min_max = this
1.133 +      assume as: "ksimplex p n s'"
1.134 +      assume "\<exists>b\<in>s'. s' - {b} = s - {a}"
1.135 +      then obtain a' where a': "a' \<in> s'" "s' - {a'} = s - {a}" ..
1.136 +      obtain a_min a_max where min_max:
1.137 +          "a_min \<in> s'"
1.138 +          "a_max \<in> s'"
1.139 +          "a_min \<noteq> a_max"
1.140 +          "\<forall>x\<in>s'. kle n a_min x \<and> kle n x a_max"
1.141 +          "\<forall>i. a_max i = (if i \<in> {1..n} then a_min i + 1 else a_min i)"
1.142 +        by (rule ksimplex_extrema_strong[OF as assms(3)])
1.143        have *: "\<forall>x\<in>s' - {a'}. x k = a2 k"
1.144          unfolding a'
1.145        proof
1.146 @@ -2270,7 +2309,10 @@
1.147        apply (rule_tac *[OF ksimplex_predecessor[OF assms(1-2),unfolded `a=a1`]])
1.148        apply auto
1.149        done
1.150 -    then guess a2 .. from this(2) guess k .. note k=this note a2 = `a2 \<in> s`
1.151 +    then
1.152 +    obtain a2 k where a2: "a2 \<in> s"
1.153 +      and k: "k \<in> {1..n}" "\<forall>j. a1 j = (if j = k then a2 j + 1 else a2 j)"
1.154 +      by blast
1.155      def a3 \<equiv> "\<lambda>j. if j = k then a0 j - 1 else a0 j"
1.156      have "a2 \<noteq> a1"
1.157        using k(2)[THEN spec[where x=k]] by auto
1.158 @@ -2297,8 +2339,8 @@
1.159      qed
1.160      have "a0 k \<noteq> 0"
1.161      proof -
1.162 -      guess a4 using assms(4)[unfolded bex_simps ball_simps,rule_format,OF `k\<in>{1..n}`] ..
1.163 -      note a4 = this
1.164 +      obtain a4 where a4: "a4 \<in> s - {a}" "a4 k \<noteq> 0"
1.165 +        using assms(4) `k\<in>{1..n}` by blast
1.166        have "a4 k \<le> a2 k"
1.167          using lem3[OF a4(1)[unfolded `a=a1`],THEN kle_imp_pointwise]
1.168          by auto
1.169 @@ -2353,9 +2395,10 @@
1.170                using `a0 \<in> s` ksimplexD(4)[OF assms(1)]
1.171                by auto
1.172            next
1.173 -            guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] ..
1.174 -            note a4 = this
1.175 -            case True have "a3 k \<le> a0 k"
1.176 +            case True
1.177 +            obtain a4 where a4: "a4 \<in> s - {a}" "a4 k \<noteq> p"
1.178 +              using assms(5) k(1) by blast
1.179 +            have "a3 k \<le> a0 k"
1.180                unfolding lem4[rule_format] by auto
1.181              also have "\<dots> \<le> p"
1.182                using ksimplexD(4)[OF assms(1),rule_format, of a0 k] a0a1
1.183 @@ -2393,7 +2436,9 @@
1.184          have "kle n a3 a2"
1.185          proof -
1.186            have "kle n a0 a1"
1.187 -            using a0a1 by auto then guess kk unfolding kle_def ..
1.188 +            using a0a1 by auto
1.189 +          then obtain kk where "kk \<subseteq> {1..n}" "(\<forall>j. a1 j = a0 j + (if j \<in> kk then 1 else 0))"
1.190 +            unfolding kle_def by blast
1.191            then show ?thesis
1.192              unfolding kle_def
1.193              apply (rule_tac x=kk in exI)
1.194 @@ -2404,7 +2449,6 @@
1.195              case goal1
1.196              then show ?case
1.197                apply -
1.198 -              apply (erule conjE)
1.199                apply (erule_tac[!] x=j in allE)
1.200                apply (cases "j \<in> kk")
1.201                apply (case_tac[!] "j=k")
1.202 @@ -2481,9 +2525,16 @@
1.203        unfolding mem_Collect_eq
1.204      proof (erule conjE)
1.205        fix s'
1.206 -      assume as: "ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
1.207 -      from this(2) guess a' .. note a' = this
1.208 -      guess a_min a_max by (rule ksimplex_extrema_strong[OF as assms(3)]) note min_max = this
1.209 +      assume as: "ksimplex p n s'"
1.210 +      assume "\<exists>b\<in>s'. s' - {b} = s - {a}"
1.211 +      then obtain a' where a': "a' \<in> s'" "s' - {a'} = s - {a}" ..
1.212 +      obtain a_min a_max where min_max:
1.213 +          "a_min \<in> s'"
1.214 +          "a_max \<in> s'"
1.215 +          "a_min \<noteq> a_max"
1.216 +          "\<forall>x\<in>s'. kle n a_min x \<and> kle n x a_max"
1.217 +          "\<forall>i. a_max i = (if i \<in> {1..n} then a_min i + 1 else a_min i)"
1.218 +        by (rule ksimplex_extrema_strong[OF as assms(3)])
1.219        have *: "\<forall>x\<in>s' - {a'}. x k = a2 k" unfolding a'
1.220        proof
1.221          fix x
1.222 @@ -2644,8 +2695,9 @@
1.223      then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a j = (if j = k then y j + 1 else y j)"
1.224        using ksimplex_predecessor[OF assms(1-2)]
1.225        by blast
1.226 -    then guess u .. from this(2) guess k .. note k = this[rule_format]
1.227 -    note u = `u \<in> s`
1.228 +    then obtain u k where u: "u \<in> s"
1.229 +      and k: "k \<in> {1..n}" "\<And>j. a j = (if j = k then u j + 1 else u j)"
1.230 +      by blast
1.231      have "\<not> (\<forall>x\<in>s. kle n x a)"
1.232      proof
1.233        case goal1
1.234 @@ -2660,9 +2712,9 @@
1.235      qed
1.236      then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a j + 1 else a j)"
1.237        using ksimplex_successor[OF assms(1-2)] by blast
1.238 -    then guess v .. from this(2) guess l ..
1.239 -    note l = this[rule_format]
1.240 -    note v = `v \<in> s`
1.241 +    then obtain v l where v: "v \<in> s"
1.242 +      and l: "l \<in> {1..n}" "\<And>j. v j = (if j = l then a j + 1 else a j)"
1.243 +      by blast
1.244      def a' \<equiv> "\<lambda>j. if j = l then u j + 1 else u j"
1.245      have kl: "k \<noteq> l"
1.246      proof
1.247 @@ -2969,10 +3021,12 @@
1.248        unfolding mem_Collect_eq
1.249      proof (erule conjE)
1.250        fix s'
1.251 -      assume as: "ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
1.252 -      from this(2) guess a'' .. note a'' = this
1.253 +      assume as: "ksimplex p n s'"
1.254 +      assume "\<exists>b\<in>s'. s' - {b} = s - {a}"
1.255 +      then obtain a'' where a'': "a'' \<in> s'" "s' - {a''} = s - {a}"
1.256 +        by blast
1.257        have "u \<noteq> v"
1.258 -        unfolding fun_eq_iff unfolding l(2) k(2) by auto
1.259 +        unfolding fun_eq_iff l(2) k(2) by auto
1.260        then have uv': "\<not> kle n v u"
1.261          using uv using kle_antisym by auto
1.262        have "u \<noteq> a" "v \<noteq> a"
1.263 @@ -2982,7 +3036,8 @@
1.264        have lem6: "a \<in> s' \<or> a' \<in> s'"
1.265        proof (cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x")
1.266          case False
1.267 -        then guess w unfolding ball_simps .. note w = this
1.268 +        then obtain w where w: "w \<in> s'" "\<not> (kle n w u \<or> kle n v w)"
1.269 +          by blast
1.270          then have "kle n u w" "kle n w v"
1.271            using ksimplexD(6)[OF as] uvs' by auto
1.272          then have "w = a' \<or> w = a"
1.273 @@ -3002,8 +3057,13 @@
1.274          then have "\<exists>y\<in>s'. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then u j + 1 else u j)"
1.275            using ksimplex_successor[OF as `u\<in>s'`]
1.276            by blast
1.277 -        then guess w .. note w = this
1.278 -        from this(2) guess kk .. note kk = this[rule_format]
1.279 +        then obtain w where
1.280 +          w: "w \<in> s'" "\<exists>k\<in>{1..n}. \<forall>j. w j = (if j = k then u j + 1 else u j)"
1.281 +          ..
1.282 +        from this(2) obtain kk where kk:
1.283 +            "kk \<in> {1..n}"
1.284 +            "\<And>j. w j = (if j = kk then u j + 1 else u j)"
1.285 +          by blast
1.286          have "\<not> kle n w u"
1.287            apply -
1.288            apply rule
1.289 @@ -3021,7 +3081,7 @@
1.290            then show False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
1.291              apply (erule_tac x=l in allE)
1.292              using `k \<noteq> l`
1.293 -            apply auto
1.294 +            apply auto
1.295              done
1.296          next
1.297            case True
1.298 @@ -3171,11 +3231,12 @@
1.299      done
1.300    have *: "n \<le> n \<and> (label x (n + 1) \<noteq> 0 \<or> n = n)"
1.301      by auto
1.302 -  then guess N
1.303 +  then obtain N where N:
1.304 +      "N \<le> n \<and> (label x (N + 1) \<noteq> 0 \<or> n = N)"
1.305 +      "\<forall>m<N. \<not> (m \<le> n \<and> (label x (m + 1) \<noteq> 0 \<or> n = m))"
1.306      apply (drule_tac num_WOP[of "\<lambda>j. j\<le>n \<and> (label x (j+1) \<noteq> 0 \<or> n = j)"])
1.307 -    apply (erule exE)
1.308 +    apply blast
1.309      done
1.310 -  note N = this
1.311    have N': "N \<le> n"
1.312      "\<forall>i. 1 \<le> i \<and> i < N + 1 \<longrightarrow> label x i = 0" "N = n \<or> label x (N + 1) \<noteq> 0"
1.313      defer
1.314 @@ -3183,10 +3244,10 @@
1.315      fix i
1.316      assume i: "1 \<le> i \<and> i < N + 1"
1.317      then show "label x i = 0"
1.318 -      using N[THEN conjunct2,THEN spec[where x="i - 1"]]
1.319 +      using N(2)[THEN spec[where x="i - 1"]]
1.320        using N
1.321        by auto
1.322 -  qed (insert N, auto)
1.323 +  qed (insert N(1), auto)
1.324    show ?t1 ?t2 ?t3
1.325      unfolding reduced_def
1.326      apply (rule_tac[!] someI2_ex)
1.327 @@ -3251,7 +3312,7 @@
1.328      apply assumption
1.329    proof (cases ?a)
1.330      case True
1.331 -    then guess j .. note j = this
1.332 +    then obtain j where j: "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = 0" ..
1.333      {
1.334        fix x
1.335        assume x: "x \<in> f"
1.336 @@ -3267,8 +3328,12 @@
1.337      }
1.338      moreover have "j - 1 \<in> {0..n}"
1.339        using j by auto
1.340 -    then guess y unfolding `?l`[THEN conjunct1,symmetric] and image_iff .. note y = this
1.341 -    ultimately have False
1.342 +    then obtain y where y:
1.343 +      "y \<in> f"
1.344 +      "j - 1 = reduced lab (n + 1) y"
1.345 +      unfolding `?l`[THEN conjunct1,symmetric] and image_iff ..
1.346 +    ultimately
1.347 +    have False
1.348        by auto
1.349      then show "\<forall>x\<in>f. x (n + 1) = p"
1.350        by auto
1.351 @@ -3276,7 +3341,7 @@
1.352      case False
1.353      then have ?b using `?l`
1.354        by blast
1.355 -    then guess j .. note j = this
1.356 +    then obtain j where j: "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = p" ..
1.357      {
1.358        fix x
1.359        assume x: "x \<in> f"
1.360 @@ -3296,8 +3361,10 @@
1.361        moreover
1.362        have "n \<in> {0..n}"
1.363          by auto
1.364 -      then guess y unfolding `?l`[THEN conjunct1,symmetric] image_iff ..
1.365 -      ultimately show False
1.366 +      then obtain y where "y \<in> f" "n = reduced lab (n + 1) y"
1.367 +        unfolding `?l`[THEN conjunct1,symmetric] image_iff ..
1.368 +      ultimately
1.369 +      show False
1.370          using *[of y] by auto
1.371      qed
1.372      then show "\<forall>x\<in>f. x (n + 1) = p"
1.373 @@ -3368,8 +3435,9 @@
1.374        unfolding image_iff
1.375        apply auto
1.376        done
1.377 -    moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] ..
1.378 -    then guess a ..
1.379 +    moreover
1.380 +    obtain s a where "ksimplex p (n + 1) s \<and> a \<in> s \<and> f = s - {a}"
1.381 +      using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] by blast
1.382      ultimately show "\<exists>s a. ksimplex p (n + 1) s \<and>
1.383          a \<in> s \<and> f = s - {a} \<and>
1.384          reduced lab (n + 1) ` f = {0..n} \<and>
1.385 @@ -3385,8 +3453,13 @@
1.386      assume as: "\<exists>s a. ksimplex p (n + 1) s \<and>
1.387        a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and>
1.388        ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))"
1.389 -    then guess s ..
1.390 -    then guess a by (elim exE conjE) note sa = this
1.391 +    then obtain s a where sa:
1.392 +        "ksimplex p (n + 1) s"
1.393 +        "a \<in> s"
1.394 +        "f = s - {a}"
1.395 +        "reduced lab (n + 1) ` f = {0..n}"
1.396 +        "(\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p)"
1.397 +      by auto
1.398      {
1.399        fix x
1.400        assume "x \<in> f"
1.401 @@ -3411,7 +3484,7 @@
1.402      have *: "\<forall>x\<in>f. x (n + 1) = p"
1.403      proof (cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0")
1.404        case True
1.405 -      then guess j ..
1.406 +      then obtain j where "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = 0" ..
1.407        then have "\<And>x. x \<in> f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1"
1.408          apply -
1.409          apply (rule reduced_labelling_zero)
1.410 @@ -3433,7 +3506,8 @@
1.411      next
1.412        case False
1.413        then have "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p"
1.414 -        using sa(5) by fastforce then guess j .. note j=this
1.415 +        using sa(5) by fastforce
1.416 +      then obtain j where j: "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = p" ..
1.417        then show ?thesis
1.418        proof (cases "j = n + 1")
1.419          case False
1.420 @@ -3489,7 +3563,9 @@
1.421    (is "?l = ?r")
1.422  proof
1.423    assume l: ?l
1.424 -  guess a using ksimplexD(3)[OF l, unfolded add_0] unfolding card_1_exists .. note a = this
1.425 +  obtain a where a: "a \<in> s" "\<forall>y y'. y \<in> s \<and> y' \<in> s \<longrightarrow> y = y'"
1.426 +    using ksimplexD(3)[OF l, unfolded add_0]
1.427 +    unfolding card_1_exists ..
1.428    have "a = (\<lambda>x. p)"
1.429      using ksimplexD(5)[OF l, rule_format, OF a(1)]
1.430      by rule auto
1.431 @@ -3566,7 +3642,13 @@
1.432      unfolding card_eq_0_iff by auto
1.433    then obtain s where "s \<in> ?A"
1.434      by auto note s=conjD[OF this[unfolded mem_Collect_eq]]
1.435 -  guess a b by (rule ksimplex_extrema_strong[OF s(1) `n \<noteq> 0`]) note ab = this
1.436 +  obtain a b where ab:
1.437 +      "a \<in> s"
1.438 +      "b \<in> s"
1.439 +      "a \<noteq> b"
1.440 +      "\<forall>x\<in>s. kle n a x \<and> kle n x b"
1.441 +      "\<forall>i. b i = (if i \<in> {1..n} then a i + 1 else a i)"
1.442 +    by (rule ksimplex_extrema_strong[OF s(1) `n \<noteq> 0`])
1.443    show ?thesis
1.444      apply (rule that[of a])
1.445      apply (rule_tac[!] ballI)
1.446 @@ -3590,10 +3672,12 @@
1.447      case goal2
1.448      then have "i \<in> reduced label n ` s"
1.449        using s by auto
1.450 -    then guess u unfolding image_iff .. note u = this
1.451 +    then obtain u where u: "u \<in> s" "i = reduced label n u"
1.452 +      unfolding image_iff ..
1.453      from goal2 have "i - 1 \<in> reduced label n ` s"
1.454        using s by auto
1.455 -    then guess v unfolding image_iff .. note v = this
1.456 +    then obtain v where v: "v \<in> s" "i - 1 = reduced label n v"
1.457 +      unfolding image_iff ..
1.458      show ?case
1.459        apply (rule_tac x = u in exI)
1.460        apply (rule_tac x = v in exI)
1.461 @@ -3680,16 +3764,24 @@
1.462    assume "\<not> ?thesis"
1.463    then have *: "\<not> (\<exists>x\<in>{0..\<Sum>Basis}. f x - x = 0)"
1.464      by auto
1.465 -  guess d
1.466 +  obtain d where
1.467 +      d: "d > 0" "\<And>x. x \<in> {0..\<Sum>Basis} \<Longrightarrow> d \<le> norm (f x - x)"
1.468      apply (rule brouwer_compactness_lemma[OF compact_interval _ *])
1.469      apply (rule continuous_on_intros assms)+
1.470 +    apply blast
1.471      done
1.472 -  note d = this [rule_format]
1.473 -  have *: "\<forall>x. x \<in> {0..\<Sum>Basis} \<longrightarrow> f x \<in> {0..\<Sum>Basis}"  "\<forall>x. x \<in> {0..(\<Sum>Basis)::'a} \<longrightarrow>
1.474 -    (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
1.475 +  have *: "\<forall>x. x \<in> {0..\<Sum>Basis} \<longrightarrow> f x \<in> {0..\<Sum>Basis}"
1.476 +    "\<forall>x. x \<in> {0..(\<Sum>Basis)::'a} \<longrightarrow> (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
1.477      using assms(2)[unfolded image_subset_iff Ball_def]
1.478 -    unfolding mem_interval by auto
1.479 -  guess label using kuhn_labelling_lemma[OF *] by (elim exE conjE)
1.480 +    unfolding mem_interval
1.481 +    by auto
1.482 +  obtain label :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where
1.483 +    "\<forall>x. \<forall>i\<in>Basis. label x i \<le> 1"
1.484 +    "\<forall>x. \<forall>i\<in>Basis. x \<in> {0..\<Sum>Basis} \<and> True \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
1.485 +    "\<forall>x. \<forall>i\<in>Basis. x \<in> {0..\<Sum>Basis} \<and> True \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
1.486 +    "\<forall>x. \<forall>i\<in>Basis. x \<in> {0..\<Sum>Basis} \<and> True \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
1.487 +    "\<forall>x. \<forall>i\<in>Basis. x \<in> {0..\<Sum>Basis} \<and> True \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
1.488 +    using kuhn_labelling_lemma[OF *] by blast
1.489    note label = this [rule_format]
1.490    have lem1: "\<forall>x\<in>{0..\<Sum>Basis}.\<forall>y\<in>{0..\<Sum>Basis}.\<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
1.491      abs (f x \<bullet> i - x \<bullet> i) \<le> norm (f y - f x) + norm (y - x)"
1.492 @@ -3760,8 +3852,15 @@
1.493        done
1.494      have *: "uniformly_continuous_on {0..\<Sum>Basis} f"
1.495        by (rule compact_uniformly_continuous[OF assms(1) compact_interval])
1.496 -    guess e using *[unfolded uniformly_continuous_on_def,rule_format,OF d'] by (elim exE conjE)
1.497 -    note e=this[rule_format,unfolded dist_norm]
1.498 +    obtain e where e:
1.499 +        "e > 0"
1.500 +        "\<And>x x'. x \<in> {0..\<Sum>Basis} \<Longrightarrow>
1.501 +          x' \<in> {0..\<Sum>Basis} \<Longrightarrow>
1.502 +          norm (x' - x) < e \<Longrightarrow>
1.503 +          norm (f x' - f x) < d / real n / 8"
1.504 +      using *[unfolded uniformly_continuous_on_def,rule_format,OF d']
1.505 +      unfolding dist_norm
1.506 +      by blast
1.507      show ?thesis
1.508        apply (rule_tac x="min (e/2) (d/real n/8)" in exI)
1.509        apply safe
1.510 @@ -3789,7 +3888,7 @@
1.511            apply auto
1.512            done
1.513          show "\<bar>f x \<bullet> i - f z \<bullet> i\<bar> \<le> norm (f x - f z)" "\<bar>x \<bullet> i - z \<bullet> i\<bar> \<le> norm (x - z)"
1.514 -          unfolding inner_diff_left[symmetric]
1.515 +          unfolding inner_diff_left[symmetric]
1.516            by (rule Basis_le_norm[OF i])+
1.517          have tria: "norm (y - x) \<le> norm (y - z) + norm (x - z)"
1.518            using dist_triangle[of y x z, unfolded dist_norm]
1.519 @@ -3822,8 +3921,18 @@
1.520        qed (insert as, auto)
1.521      qed
1.522    qed
1.523 -  then guess e by (elim exE conjE) note e=this[rule_format]
1.524 -  guess p using real_arch_simple[of "1 + real n / e"] .. note p=this
1.525 +  then
1.526 +  obtain e where e:
1.527 +    "e > 0"
1.528 +    "\<And>x y z i. x \<in> {0..\<Sum>Basis} \<Longrightarrow>
1.529 +      y \<in> {0..\<Sum>Basis} \<Longrightarrow>
1.530 +      z \<in> {0..\<Sum>Basis} \<Longrightarrow>
1.531 +      i \<in> Basis \<Longrightarrow>
1.532 +      norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<Longrightarrow>
1.533 +      \<bar>(f z - z) \<bullet> i\<bar> < d / real n"
1.534 +    by blast
1.535 +  obtain p :: nat where p: "1 + real n / e \<le> real p"
1.536 +    using real_arch_simple ..
1.537    have "1 + real n / e > 0"
1.538      apply (rule add_pos_pos)
1.539      defer
1.540 @@ -3898,7 +4007,14 @@
1.541          by (intro label(2)) (auto simp add: b'')
1.542      }
1.543    qed
1.544 -  guess q by (rule kuhn_lemma[OF q1 q2]) note q = this
1.545 +  obtain q where q:
1.546 +      "\<forall>i\<in>{1..n}. q i < p"
1.547 +      "\<forall>i\<in>{1..n}.
1.548 +         \<exists>r s. (\<forall>j\<in>{1..n}. q j \<le> r j \<and> r j \<le> q j + 1) \<and>
1.549 +               (\<forall>j\<in>{1..n}. q j \<le> s j \<and> s j \<le> q j + 1) \<and>
1.550 +               (label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) i \<noteq>
1.551 +               (label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) i"
1.552 +    by (rule kuhn_lemma[OF q1 q2])
1.553    def z \<equiv> "(\<Sum>i\<in>Basis. (real (q (b' i)) / real p) *\<^sub>R i)::'a"
1.554    have "\<exists>i\<in>Basis. d / real n \<le> abs ((f z - z)\<bullet>i)"
1.555    proof (rule ccontr)
1.556 @@ -3929,13 +4045,16 @@
1.557      finally show False
1.558        using d_fz_z by auto
1.559    qed
1.560 -  then guess i .. note i = this
1.561 +  then obtain i where i: "i \<in> Basis" "d / real n \<le> \<bar>(f z - z) \<bullet> i\<bar>" ..
1.562    have *: "b' i \<in> {1..n}"
1.563 -    using i
1.564 -    using b'[unfolded bij_betw_def]
1.565 +    using i and b'[unfolded bij_betw_def]
1.566      by auto
1.567 -  guess r using q(2)[rule_format,OF *] ..
1.568 -  then guess s by (elim exE conjE) note rs = this[rule_format]
1.569 +  obtain r s where rs:
1.570 +    "\<And>j. j \<in> {1..n} \<Longrightarrow> q j \<le> r j \<and> r j \<le> q j + 1"
1.571 +    "\<And>j. j \<in> {1..n} \<Longrightarrow> q j \<le> s j \<and> s j \<le> q j + 1"
1.572 +    "(label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i) \<noteq>
1.573 +      (label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i)"
1.574 +    using q(2)[rule_format,OF *] by blast
1.575    have b'_im: "\<And>i. i \<in> Basis \<Longrightarrow>  b' i \<in> {1..n}"
1.576      using b' unfolding bij_betw_def by auto
1.577    def r' \<equiv> "(\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i)::'a"
1.578 @@ -4040,7 +4159,7 @@
1.579      apply auto
1.580      apply blast
1.581      done
1.582 -  then guess x .. note x = this
1.583 +  then obtain x where x: "x \<in> s" "(i \<circ> g \<circ> r) x = x" ..
1.584    then have *: "g (r x) \<in> t"
1.585      using assms(4,8) by auto
1.586    have "r ((i \<circ> g \<circ> r) x) = r x"
1.587 @@ -4062,8 +4181,16 @@
1.588    shows "(\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)) \<longleftrightarrow>
1.589      (\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))"
1.590  proof -
1.591 -  guess r using assms[unfolded homeomorphic_def homeomorphism_def] ..
1.592 -  then guess i ..
1.593 +  obtain r i where
1.594 +      "\<forall>x\<in>s. i (r x) = x"
1.595 +      "r ` s = t"
1.596 +      "continuous_on s r"
1.597 +      "\<forall>y\<in>t. r (i y) = y"
1.598 +      "i ` t = s"
1.599 +      "continuous_on t i"
1.600 +    using assms
1.601 +    unfolding homeomorphic_def homeomorphism_def
1.602 +    by blast
1.603    then show ?thesis
1.604      apply -
1.605      apply rule
1.606 @@ -4084,7 +4211,8 @@
1.607      and "g ` t \<subseteq> t"
1.608    obtains y where "y \<in> t" and "g y = y"
1.609  proof -
1.610 -  guess h using assms(1) unfolding retract_of_def ..
1.611 +  obtain h where "retraction s t h"
1.612 +    using assms(1) unfolding retract_of_def ..
1.613    then show ?thesis
1.614      unfolding retraction_def
1.615      apply -
1.616 @@ -4161,8 +4289,8 @@
1.617      apply (rule_tac x=b in exI)
1.618      apply (auto simp add: dist_norm)
1.619      done
1.620 -  then guess e by (elim exE conjE)
1.621 -  note e = this
1.622 +  then obtain e where e: "e > 0" "s \<subseteq> cball 0 e"
1.623 +    by blast
1.624    have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point s) x = x"
1.625      apply (rule_tac brouwer_ball[OF e(1), of 0 "f \<circ> closest_point s"])
1.626      apply (rule continuous_on_compose )
1.627 @@ -4174,7 +4302,7 @@
1.628      using e(2)[unfolded subset_eq mem_cball]
1.629      apply (auto simp add: dist_norm)
1.630      done
1.631 -  then guess x .. note x=this
1.632 +  then obtain x where x: "x \<in> cball 0 e" "(f \<circ> closest_point s) x = x" ..
1.633    have *: "closest_point s x = x"
1.634      apply (rule closest_point_self)
1.635      apply (rule assms(5)[unfolded subset_eq,THEN bspec[where x="x"], unfolded image_iff])
1.636 @@ -4203,7 +4331,9 @@
1.637    case goal1
1.638    have *: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
1.639      using scaleR_left_distrib[of 1 1 a] by auto
1.640 -  guess x
1.641 +  obtain x where x:
1.642 +      "x \<in> {x. norm (a - x) = e}"
1.643 +      "2 *\<^sub>R a - x = x"
1.644      apply (rule retract_fixpoint_property[OF goal1, of "\<lambda>x. scaleR 2 a - x"])
1.645      apply rule
1.646      apply rule
1.647 @@ -4219,8 +4349,8 @@
1.648      apply (erule bexE)
1.649      unfolding dist_norm
1.650      apply (simp add: * norm_minus_commute)
1.651 +    apply blast
1.652      done
1.653 -  note x = this
1.654    then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
1.655      by (auto simp add: algebra_simps)
1.656    then have "a = x"
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Feb 16 18:46:13 2014 +0100
2.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Feb 16 21:09:47 2014 +0100
2.3 @@ -1158,7 +1158,7 @@
2.4    by (rule convex_box_cart) (simp add: atLeast_def[symmetric] convex_real_interval)
2.5
2.6  lemma unit_interval_convex_hull_cart:
2.7 -  "{0::real^'n .. 1} = convex hull {x. \<forall>i. (x\$i = 0) \<or> (x\$i = 1)}" (is "?int = convex hull ?points")
2.8 +  "{0::real^'n .. 1} = convex hull {x. \<forall>i. (x\$i = 0) \<or> (x\$i = 1)}"
2.9    unfolding Cart_1 unit_interval_convex_hull[where 'a="real^'n"]
2.10    by (rule arg_cong[where f="\<lambda>x. convex hull x"]) (simp add: Basis_vec_def inner_axis)
2.11
2.12 @@ -1167,8 +1167,11 @@
2.13    obtains s::"(real^'n) set"
2.14      where "finite s" "{x - (\<chi> i. d) .. x + (\<chi> i. d)} = convex hull s"
2.15  proof -
2.16 -  from cube_convex_hull [OF assms, of x] guess s .
2.17 -  with that[of s] show thesis by (simp add: const_vector_cart)
2.18 +  from assms obtain s where "finite s"
2.19 +    and "{x - setsum (op *\<^sub>R d) Basis..x + setsum (op *\<^sub>R d) Basis} = convex hull s"
2.20 +    by (rule cube_convex_hull)
2.21 +  with that[of s] show thesis
2.22 +    by (simp add: const_vector_cart)
2.23  qed
2.24
2.25
```
```     3.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Feb 16 18:46:13 2014 +0100
3.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Feb 16 21:09:47 2014 +0100
3.3 @@ -256,7 +256,12 @@
3.4      using t by auto
3.5    have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0"
3.6      using m by auto
3.7 -  from `open S` [THEN ereal_openE] guess l u . note T = this
3.8 +  from `open S` [THEN ereal_openE]
3.9 +  obtain l u where T:
3.10 +      "open (ereal -` S)"
3.11 +      "\<infinity> \<in> S \<Longrightarrow> {ereal l<..} \<subseteq> S"
3.12 +      "- \<infinity> \<in> S \<Longrightarrow> {..<ereal u} \<subseteq> S"
3.13 +    by blast
3.14    let ?f = "(\<lambda>x. m * x + t)"
3.15    show ?thesis
3.16      unfolding open_ereal_def
```
```     4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Feb 16 18:46:13 2014 +0100
4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Feb 16 21:09:47 2014 +0100
4.3 @@ -139,12 +139,12 @@
4.4      and f :: "'a set \<Rightarrow> 'a"
4.5    assumes "topological_basis B"
4.6      and choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
4.7 -  shows "(\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X))"
4.8 +  shows "\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X)"
4.9  proof (intro allI impI)
4.10    fix X :: "'a set"
4.11    assume "open X" and "X \<noteq> {}"
4.12    from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]]
4.13 -  guess B' . note B' = this
4.14 +  obtain B' where "B' \<in> B" "f X \<in> B'" "B' \<subseteq> X" .
4.15    then show "\<exists>B'\<in>B. f B' \<in> X"
4.16      by (auto intro!: choosefrom_basis)
4.17  qed
4.18 @@ -166,8 +166,12 @@
4.19      from open_prod_elim[OF `open S` this]
4.20      obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
4.21        by (metis mem_Sigma_iff)
4.22 -    moreover from topological_basisE[OF A a] guess A0 .
4.23 -    moreover from topological_basisE[OF B b] guess B0 .
4.24 +    moreover
4.25 +    from A a obtain A0 where "A0 \<in> A" "x \<in> A0" "A0 \<subseteq> a"
4.26 +      by (rule topological_basisE)
4.27 +    moreover
4.28 +    from B b obtain B0 where "B0 \<in> B" "y \<in> B0" "B0 \<subseteq> b"
4.29 +      by (rule topological_basisE)
4.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)"
4.31        by (intro UN_I[of "(A0, B0)"]) auto
4.32    qed auto
4.33 @@ -225,7 +229,12 @@
4.34      "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
4.35      "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A"
4.36  proof atomize_elim
4.37 -  from first_countable_basisE[of x] guess A' . note A' = this
4.38 +  obtain A' where A':
4.39 +    "countable A'"
4.40 +    "\<And>a. a \<in> A' \<Longrightarrow> x \<in> a"
4.41 +    "\<And>a. a \<in> A' \<Longrightarrow> open a"
4.42 +    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A'. a \<subseteq> S"
4.43 +    by (rule first_countable_basisE) blast
4.44    def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)"
4.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>
4.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)"
4.47 @@ -273,8 +282,18 @@
4.48  instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
4.49  proof
4.50    fix x :: "'a \<times> 'b"
4.51 -  from first_countable_basisE[of "fst x"] guess A :: "'a set set" . note A = this
4.52 -  from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this
4.53 +  obtain A where A:
4.54 +      "countable A"
4.55 +      "\<And>a. a \<in> A \<Longrightarrow> fst x \<in> a"
4.56 +      "\<And>a. a \<in> A \<Longrightarrow> open a"
4.57 +      "\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
4.58 +    by (rule first_countable_basisE[of "fst x"]) blast
4.59 +  obtain B where B:
4.60 +      "countable B"
4.61 +      "\<And>a. a \<in> B \<Longrightarrow> snd x \<in> a"
4.62 +      "\<And>a. a \<in> B \<Longrightarrow> open a"
4.63 +      "\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S"
4.64 +    by (rule first_countable_basisE[of "snd x"]) blast
4.65    show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set.
4.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))"
4.67    proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe)
4.68 @@ -286,10 +305,14 @@
4.69    next
4.70      fix S
4.71      assume "open S" "x \<in> S"
4.72 -    from open_prod_elim[OF this] guess a' b' . note a'b' = this
4.73 -    moreover from a'b' A(4)[of a'] B(4)[of b']
4.74 -    obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto
4.75 -    ultimately show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
4.76 +    then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S"
4.77 +      by (rule open_prod_elim)
4.78 +    moreover
4.79 +    from a'b' A(4)[of a'] B(4)[of b']
4.80 +    obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'"
4.81 +      by auto
4.82 +    ultimately
4.83 +    show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
4.84        by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
4.85    qed (simp add: A B)
4.86  qed
4.87 @@ -328,7 +351,9 @@
4.88        next
4.89          case (UN K)
4.90          then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto
4.91 -        then guess k unfolding bchoice_iff ..
4.92 +        then obtain k where
4.93 +            "\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> UNION (k ka) Inter = ka"
4.94 +          unfolding bchoice_iff ..
4.95          then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K"
4.96            by (intro exI[of _ "UNION K k"]) auto
4.97        next
4.98 @@ -849,14 +874,16 @@
4.99      from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
4.100      show "?th i" by auto
4.101    qed
4.102 -  from choice[OF this] guess a .. note a = this
4.103 +  from choice[OF this] obtain a where
4.104 +    a: "\<forall>xa. a xa \<in> \<rat> \<and> a xa < x \<bullet> xa \<and> x \<bullet> xa - a xa < e'" ..
4.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")
4.106    proof
4.107      fix i
4.108      from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
4.109      show "?th i" by auto
4.110    qed
4.111 -  from choice[OF this] guess b .. note b = this
4.112 +  from choice[OF this] obtain b where
4.113 +    b: "\<forall>xa. b xa \<in> \<rat> \<and> x \<bullet> xa < b xa \<and> b xa - x \<bullet> xa < e'" ..
4.114    let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
4.115    show ?thesis
4.116    proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
4.117 @@ -1585,7 +1612,11 @@
4.118      (is "?lhs = ?rhs")
4.119  proof
4.120    assume ?lhs
4.121 -  from countable_basis_at_decseq[of x] guess A . note A = this
4.122 +  from countable_basis_at_decseq[of x] obtain A where A:
4.123 +      "\<And>i. open (A i)"
4.124 +      "\<And>i. x \<in> A i"
4.125 +      "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
4.126 +    by blast
4.127    def f \<equiv> "\<lambda>n. SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
4.128    {
4.129      fix n
4.130 @@ -2759,8 +2790,12 @@
4.131    assumes l: "\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> range f)"
4.132    shows "\<exists>r. subseq r \<and> (f \<circ> r) ----> l"
4.133  proof -
4.134 -  from countable_basis_at_decseq[of l] guess A . note A = this
4.135 -
4.136 +  from countable_basis_at_decseq[of l]
4.137 +  obtain A where A:
4.138 +      "\<And>i. open (A i)"
4.139 +      "\<And>i. l \<in> A i"
4.140 +      "\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
4.141 +    by blast
4.142    def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> f j \<in> A (Suc n)"
4.143    {
4.144      fix n i
4.145 @@ -3043,8 +3078,10 @@
4.146    show "?R (\<lambda>x. True)"
4.147      by (rule exI[of _ "{}"]) (simp add: le_fun_def)
4.148  next
4.149 -  fix P Q assume "?R P" then guess X ..
4.150 -  moreover assume "?R Q" then guess Y ..
4.151 +  fix P Q
4.152 +  assume "?R P" then guess X ..
4.153 +  moreover
4.154 +  assume "?R Q" then guess Y ..
4.155    ultimately show "?R (\<lambda>x. P x \<and> Q x)"
4.156      by (intro exI[of _ "X \<union> Y"]) auto
4.157  next
4.158 @@ -3221,7 +3258,8 @@
4.159      using * by metis
4.160    then have "\<forall>t\<in>T. \<exists>a\<in>A. t \<inter> U \<subseteq> a"
4.161      by (auto simp: C_def)
4.162 -  then guess f unfolding bchoice_iff Bex_def ..
4.163 +  then obtain f where "\<forall>t\<in>T. f t \<in> A \<and> t \<inter> U \<subseteq> f t"
4.164 +    unfolding bchoice_iff Bex_def ..
4.165    with T show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
4.166      unfolding C_def by (intro exI[of _ "f`T"]) fastforce
4.167  qed
4.168 @@ -3231,9 +3269,10 @@
4.169  proof (rule countably_compact_imp_compact)
4.170    fix T and x :: 'a
4.171    assume "open T" "x \<in> T"
4.172 -  from topological_basisE[OF is_basis this] guess b .
4.173 +  from topological_basisE[OF is_basis this] obtain b where
4.174 +    "b \<in> (SOME B. countable B \<and> topological_basis B)" "x \<in> b" "b \<subseteq> T" .
4.175    then show "\<exists>b\<in>SOME B. countable B \<and> topological_basis B. x \<in> b \<and> b \<inter> U \<subseteq> T"
4.176 -    by auto
4.177 +    by blast
4.178  qed (insert countable_basis topological_basis_open[OF is_basis], auto)
4.179
4.180  lemma countably_compact_eq_compact:
4.181 @@ -3354,7 +3393,12 @@
4.182    obtain x where "x \<in> U" and x: "inf (nhds x) (filtermap X sequentially) \<noteq> bot" (is "?F \<noteq> _")
4.183      using `compact U` by (auto simp: compact_filter)
4.184
4.185 -  from countable_basis_at_decseq[of x] guess A . note A = this
4.186 +  from countable_basis_at_decseq[of x]
4.187 +  obtain A where A:
4.188 +      "\<And>i. open (A i)"
4.189 +      "\<And>i. x \<in> A i"
4.190 +      "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
4.191 +    by blast
4.192    def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> X j \<in> A (Suc n)"
4.193    {
4.194      fix n i
4.195 @@ -3426,7 +3470,9 @@
4.196    moreover
4.197    from `countable t` have "countable C"
4.198      unfolding C_def by (auto intro: countable_Collect_finite_subset)
4.199 -  ultimately guess D by (rule countably_compactE)
4.200 +  ultimately
4.201 +  obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> \<Union>D"
4.202 +    by (rule countably_compactE)
4.203    then obtain E where E: "E \<subseteq> {F. finite F \<and> F \<subseteq> t }" "finite E"
4.204      and s: "s \<subseteq> (\<Union>F\<in>E. interior (F \<union> (- t)))"
4.205      by (metis (lifting) Union_image_eq finite_subset_image C_def)
4.206 @@ -3569,7 +3615,8 @@
4.207    shows "compact s"
4.208  proof -
4.209    from seq_compact_imp_totally_bounded[OF `seq_compact s`]
4.210 -  guess f unfolding choice_iff' .. note f = this
4.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)"
4.212 +    unfolding choice_iff' ..
4.213    def K \<equiv> "(\<lambda>(x, r). ball x r) ` ((\<Union>e \<in> \<rat> \<inter> {0 <..}. f e) \<times> \<rat>)"
4.214    have "countably_compact s"
4.215      using `seq_compact s` by (rule seq_compact_imp_countably_compact)
4.216 @@ -3944,7 +3991,9 @@
4.217          assume "infinite {n. f n \<in> U}"
4.218          then have "\<exists>b\<in>k (e n). infinite {i\<in>{n. f n \<in> U}. f i \<in> ball b (e n)}"
4.219            using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq)
4.220 -        then guess a ..
4.221 +        then obtain a where
4.222 +          "a \<in> k (e n)"
4.223 +          "infinite {i \<in> {n. f n \<in> U}. f i \<in> ball a (e n)}" ..
4.224          then have "\<exists>b. infinite {i. f i \<in> b} \<and> (\<exists>x. b \<subseteq> ball x (e n) \<inter> U)"
4.225            by (intro exI[of _ "ball a (e n) \<inter> U"] exI[of _ a]) (auto simp: ac_simps)
4.226          from someI_ex[OF this]
4.227 @@ -6617,7 +6666,7 @@
4.228    shows "\<exists>S\<subseteq>A. card S = n"
4.229  proof cases
4.230    assume "finite A"
4.231 -  from ex_bij_betw_nat_finite[OF this] guess f .. note f = this
4.232 +  from ex_bij_betw_nat_finite[OF this] obtain f where f: "bij_betw f {0..<card A} A" ..
4.233    moreover from f `n \<le> card A` have "{..< n} \<subseteq> {..< card A}" "inj_on f {..< n}"
4.234      by (auto simp: bij_betw_def intro: subset_inj_on)
4.235    ultimately have "f ` {..< n} \<subseteq> A" "card (f ` {..< n}) = n"
4.236 @@ -6642,7 +6691,11 @@
4.237        inj_on f {x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
4.238      using dim_substandard[of d] t d assms
4.239      by (intro subspace_isomorphism[OF subspace_substandard[of "\<lambda>i. i \<notin> d"]]) (auto simp: inner_Basis)
4.240 -  then guess f by (elim exE conjE) note f = this
4.241 +  then obtain f where f:
4.242 +      "linear f"
4.243 +      "f ` {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} = s"
4.244 +      "inj_on f {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
4.245 +    by blast
4.246    interpret f: bounded_linear f
4.247      using f unfolding linear_conv_bounded_linear by auto
4.248    {
```