tuned proofs;
authorwenzelm
Sun Feb 16 21:09:47 2014 +0100 (2014-02-16)
changeset 5552223d2cbac6dce
parent 55521 241c6a2fdda1
child 55523 9429e7b5b827
tuned proofs;
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     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    {