tuned proofs;
authorwenzelm
Fri Feb 14 16:11:14 2014 +0100 (2014-02-14)
changeset 5549347cac23e3d22
parent 55492 28d4db6c6e79
child 55494 009b71c1ed23
tuned proofs;
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Feb 14 15:42:27 2014 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Feb 14 16:11:14 2014 +0100
     1.3 @@ -541,30 +541,31 @@
     1.4      and "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x k < y k"
     1.5    apply (rule kle_imp_pointwise[OF assms(1)])
     1.6  proof -
     1.7 -  guess k using assms(1)[unfolded kle_def] .. note k = this
     1.8 +  obtain k where k: "k \<subseteq> {1..n} \<and> (\<forall>j. y j = x j + (if j \<in> k then 1 else 0))"
     1.9 +    using assms(1)[unfolded kle_def] ..
    1.10    show "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x k < y k"
    1.11 -proof (cases "k = {}")
    1.12 -  case True
    1.13 -  then have "x = y"
    1.14 -    apply -
    1.15 -    apply (rule ext)
    1.16 -    using k
    1.17 -    apply auto
    1.18 -    done
    1.19 -  then show ?thesis
    1.20 -    using assms(2) by auto
    1.21 -next
    1.22 -  case False
    1.23 -  then have "(SOME k'. k' \<in> k) \<in> k"
    1.24 -    apply -
    1.25 -    apply (rule someI_ex)
    1.26 -    apply auto
    1.27 -    done
    1.28 -  then show ?thesis
    1.29 -    apply (rule_tac x = "SOME k'. k' \<in> k" in exI)
    1.30 -    using k
    1.31 -    apply auto
    1.32 -    done
    1.33 +  proof (cases "k = {}")
    1.34 +    case True
    1.35 +    then have "x = y"
    1.36 +      apply -
    1.37 +      apply (rule ext)
    1.38 +      using k
    1.39 +      apply auto
    1.40 +      done
    1.41 +    then show ?thesis
    1.42 +      using assms(2) by auto
    1.43 +  next
    1.44 +    case False
    1.45 +    then have "(SOME k'. k' \<in> k) \<in> k"
    1.46 +      apply -
    1.47 +      apply (rule someI_ex)
    1.48 +      apply auto
    1.49 +      done
    1.50 +    then show ?thesis
    1.51 +      apply (rule_tac x = "SOME k'. k' \<in> k" in exI)
    1.52 +      using k
    1.53 +      apply auto
    1.54 +      done
    1.55    qed
    1.56  qed
    1.57  
    1.58 @@ -583,7 +584,7 @@
    1.59      using kle_imp_pointwise
    1.60      apply auto
    1.61      done
    1.62 -  then guess a .. note a = this
    1.63 +  then obtain a where a: "a \<in> s" "\<forall>x\<in>s. \<forall>j. a j \<le> x j" ..
    1.64    show ?thesis
    1.65      apply (rule_tac x = a in bexI)
    1.66    proof
    1.67 @@ -620,7 +621,7 @@
    1.68      using kle_imp_pointwise
    1.69      apply auto
    1.70      done
    1.71 -  then guess a .. note a = this
    1.72 +  then obtain a where a: "a \<in> s" "\<forall>x\<in>s. \<forall>j. x j \<le> a j" ..
    1.73    show ?thesis 
    1.74      apply (rule_tac x = a in bexI)
    1.75    proof
    1.76 @@ -649,7 +650,8 @@
    1.77      and "x \<noteq> y"
    1.78    shows "1 \<le> card {k\<in>{1..n}. x k < y k}"
    1.79  proof -
    1.80 -  guess i using kle_strict(2)[OF assms] ..
    1.81 +  obtain i where "1 \<le> i" "i \<le> n" "x i < y i"
    1.82 +    using kle_strict(2)[OF assms] by blast
    1.83    then have "card {i} \<le> card {k\<in>{1..n}. x k < y k}"
    1.84      apply -
    1.85      apply (rule card_mono)
    1.86 @@ -693,7 +695,8 @@
    1.87    proof -
    1.88      fix i j
    1.89      assume as: "i \<in> {1..n}" "x i < y i" "j \<in> {1..n}" "y j < z j" "i = j"
    1.90 -    guess kx using assms(1)[unfolded kle_def] .. note kx = this
    1.91 +    obtain kx where kx: "kx \<subseteq> {1..n} \<and> (\<forall>j. y j = x j + (if j \<in> kx then 1 else 0))"
    1.92 +      using assms(1)[unfolded kle_def] ..
    1.93      have "x i < y i"
    1.94        using as by auto
    1.95      then have "i \<in> kx"
    1.96 @@ -705,7 +708,8 @@
    1.97      then have "x i + 1 = y i"
    1.98        using kx by auto
    1.99      moreover
   1.100 -    guess ky using assms(2)[unfolded kle_def] .. note ky = this
   1.101 +    obtain ky where ky: "ky \<subseteq> {1..n} \<and> (\<forall>j. z j = y j + (if j \<in> ky then 1 else 0))"
   1.102 +      using assms(2)[unfolded kle_def] ..
   1.103      have "y i < z i"
   1.104        using as by auto
   1.105      then have "i \<in> ky"
   1.106 @@ -829,8 +833,10 @@
   1.107      and "\<forall>j. c j \<le> a j + 1"
   1.108    shows "kle n a c"
   1.109  proof -
   1.110 -  guess kk1 using assms(1)[unfolded kle_def] .. note kk1 = this
   1.111 -  guess kk2 using assms(2)[unfolded kle_def] .. note kk2 = this
   1.112 +  obtain kk1 where kk1: "kk1 \<subseteq> {1..n} \<and> (\<forall>j. b j = a j + (if j \<in> kk1 then 1 else 0))"
   1.113 +    using assms(1)[unfolded kle_def] ..
   1.114 +  obtain kk2 where kk2: "kk2 \<subseteq> {1..n} \<and> (\<forall>j. c j = b j + (if j \<in> kk2 then 1 else 0))"
   1.115 +    using assms(2)[unfolded kle_def] ..
   1.116    show ?thesis
   1.117      unfolding kle_def
   1.118      apply (rule_tac x="kk1 \<union> kk2" in exI)
   1.119 @@ -1023,7 +1029,8 @@
   1.120      apply (subst *[symmetric])
   1.121      unfolding mem_Collect_eq
   1.122    proof
   1.123 -    guess k using a(2)[rule_format,OF b(1),unfolded kle_def] .. note k = this
   1.124 +    obtain k where k: "k \<subseteq> {1..n} \<and> (\<forall>j. b j = a j + (if j \<in> k then 1 else 0))"
   1.125 +      using a(2)[rule_format, OF b(1), unfolded kle_def] ..
   1.126      fix i
   1.127      show "b i = (if i \<in> {1..n} \<and> a i < b i then a i + 1 else a i)"
   1.128      proof (cases "i \<in> {1..n}")
   1.129 @@ -1166,7 +1173,10 @@
   1.130      ultimately show False
   1.131        unfolding n by auto
   1.132    qed
   1.133 -  then guess k unfolding card_1_exists .. note k = this[unfolded mem_Collect_eq]
   1.134 +  then obtain k where k:
   1.135 +      "k \<in> {1..n} \<and> a k < b k"
   1.136 +      "\<And>y y'. (y \<in> {1..n} \<and> a y < b y) \<and> y' \<in> {1..n} \<and> a y' < b y' \<Longrightarrow> y = y'"
   1.137 +    unfolding card_1_exists by blast
   1.138  
   1.139    show ?thesis
   1.140      apply (rule disjI2)
   1.141 @@ -1177,12 +1187,12 @@
   1.142      have "kle n a b"
   1.143        using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`]
   1.144        by auto
   1.145 -    then guess kk unfolding kle_def .. note kk_raw = this
   1.146 -    note kk = this[THEN conjunct2, rule_format]
   1.147 +    then obtain kk where kk: "kk \<subseteq> {1..n}" "\<And>j. b j = a j + (if j \<in> kk then 1 else 0)"
   1.148 +      unfolding kle_def by blast
   1.149      have kkk: "k \<in> kk"
   1.150        apply (rule ccontr)
   1.151        using k(1)
   1.152 -      unfolding kk
   1.153 +      unfolding kk(2)
   1.154        apply auto
   1.155        done
   1.156      show "b j = (if j = k then a j + 1 else a j)"
   1.157 @@ -1190,19 +1200,19 @@
   1.158        case True
   1.159        then have "j = k"
   1.160          apply -
   1.161 -        apply (rule k(2)[rule_format])
   1.162 -        using kk_raw kkk
   1.163 +        apply (rule k(2))
   1.164 +        using kk kkk
   1.165          apply auto
   1.166          done
   1.167        then show ?thesis
   1.168 -        unfolding kk using kkk by auto
   1.169 +        unfolding kk(2) using kkk by auto
   1.170      next
   1.171        case False
   1.172        then have "j \<noteq> k"
   1.173 -        using k(2)[rule_format, of j k] and kk_raw kkk
   1.174 +        using k(2)[of j k] and kkk
   1.175          by auto
   1.176        then show ?thesis
   1.177 -        unfolding kk
   1.178 +        unfolding kk(2)
   1.179          using kkk and False
   1.180          by auto
   1.181      qed
   1.182 @@ -1298,7 +1308,10 @@
   1.183      ultimately show False
   1.184        unfolding n by auto
   1.185    qed
   1.186 -  then guess k unfolding card_1_exists .. note k = this[unfolded mem_Collect_eq]
   1.187 +  then obtain k where k:
   1.188 +    "k \<in> {1..n} \<and> b k < a k"
   1.189 +    "\<And>y y'. (y \<in> {1..n} \<and> b y < a y) \<and> y' \<in> {1..n} \<and> b y' < a y' \<Longrightarrow> y = y'"
   1.190 +    unfolding card_1_exists by blast
   1.191  
   1.192    show ?thesis
   1.193      apply (rule disjI2)
   1.194 @@ -1308,12 +1321,12 @@
   1.195      fix j :: nat
   1.196      have "kle n b a"
   1.197        using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`] by auto
   1.198 -    then guess kk unfolding kle_def .. note kk_raw = this
   1.199 -    note kk = this[THEN conjunct2,rule_format]
   1.200 +    then obtain kk where kk: "kk \<subseteq> {1..n}" "\<And>j. a j = b j + (if j \<in> kk then 1 else 0)"
   1.201 +      unfolding kle_def by blast
   1.202      have kkk: "k \<in> kk"
   1.203        apply (rule ccontr)
   1.204        using k(1)
   1.205 -      unfolding kk
   1.206 +      unfolding kk(2)
   1.207        apply auto
   1.208        done
   1.209      show "a j = (if j = k then b j + 1 else b j)"
   1.210 @@ -1321,20 +1334,20 @@
   1.211        case True
   1.212        then have "j = k"
   1.213          apply -
   1.214 -        apply (rule k(2)[rule_format])
   1.215 -        using kk_raw kkk
   1.216 +        apply (rule k(2))
   1.217 +        using kk kkk
   1.218          apply auto
   1.219          done
   1.220        then show ?thesis
   1.221 -        unfolding kk using kkk by auto
   1.222 +        unfolding kk(2) using kkk by auto
   1.223      next
   1.224        case False
   1.225        then have "j \<noteq> k"
   1.226 -        using k(2)[rule_format, of j k]
   1.227 -        using kk_raw kkk
   1.228 +        using k(2)[of j k]
   1.229 +        using kkk
   1.230          by auto
   1.231        then show ?thesis
   1.232 -        unfolding kk
   1.233 +        unfolding kk(2)
   1.234          using kkk and False
   1.235          by auto
   1.236      qed
   1.237 @@ -1367,8 +1380,12 @@
   1.238      by auto
   1.239  next
   1.240    case (Suc m)
   1.241 -  guess a using card_eq_SucD[OF Suc(4)] ..
   1.242 -  then guess s0 by (elim exE conjE) note as0 = this
   1.243 +  obtain a s0 where as0:
   1.244 +    "s = insert a s0"
   1.245 +    "a \<notin> s0"
   1.246 +    "card s0 = m"
   1.247 +    "m = 0 \<longrightarrow> s0 = {}"
   1.248 +    using card_eq_SucD[OF Suc(4)] by auto
   1.249    have **: "card s0 = m"
   1.250      using as0 using Suc(2) Suc(4)
   1.251      by auto
   1.252 @@ -1489,8 +1506,11 @@
   1.253      (is "?ls = ?rs")
   1.254  proof
   1.255    assume ?ls
   1.256 -  then guess s ..
   1.257 -  then guess a by (elim exE conjE) note sa = this
   1.258 +  then obtain s a where sa:
   1.259 +    "ksimplex p (n + 1) s"
   1.260 +    "a \<in> s"
   1.261 +    "f = s - {a}"
   1.262 +    by auto
   1.263    show ?rs
   1.264      unfolding ksimplex_def sa(3)
   1.265      apply rule
   1.266 @@ -1510,7 +1530,8 @@
   1.267      show "kle n x y \<or> kle n y x"
   1.268      proof (cases "kle (n + 1) x y")
   1.269        case True
   1.270 -      then guess k unfolding kle_def .. note k = this
   1.271 +      then obtain k where k: "k \<subseteq> {1..n + 1}" "\<And>j. y j = x j + (if j \<in> k then 1 else 0)"
   1.272 +        unfolding kle_def by blast
   1.273        then have *: "n + 1 \<notin> k" using xyp by auto
   1.274        have "\<not> (\<exists>x\<in>k. x \<notin> {1..n})"
   1.275          apply (rule notI)
   1.276 @@ -1521,13 +1542,13 @@
   1.277          have "x \<noteq> n + 1"
   1.278            using as and * by auto
   1.279          then show False
   1.280 -          using as and k[THEN conjunct1,unfolded subset_eq] by auto
   1.281 +          using as and k(1) by auto
   1.282        qed
   1.283        then show ?thesis
   1.284          apply -
   1.285          apply (rule disjI1)
   1.286          unfolding kle_def
   1.287 -        using k
   1.288 +        using k(2)
   1.289          apply (rule_tac x=k in exI)
   1.290          apply auto
   1.291          done
   1.292 @@ -1536,7 +1557,8 @@
   1.293        then have "kle (n + 1) y x"
   1.294          using ksimplexD(6)[OF sa(1),rule_format, of x y] and as
   1.295          by auto
   1.296 -      then guess k unfolding kle_def .. note k = this
   1.297 +      then obtain k where k: "k \<subseteq> {1..n + 1}" "\<And>j. x j = y j + (if j \<in> k then 1 else 0)"
   1.298 +        unfolding kle_def by auto
   1.299        then have *: "n + 1 \<notin> k"
   1.300          using xyp by auto
   1.301        then have "\<not> (\<exists>x\<in>k. x \<notin> {1..n})"
   1.302 @@ -1549,14 +1571,14 @@
   1.303          have "x \<noteq> n + 1"
   1.304            using as and * by auto
   1.305          then show False
   1.306 -          using as and k[THEN conjunct1,unfolded subset_eq]
   1.307 +          using as and k(1)
   1.308            by auto
   1.309        qed
   1.310        then show ?thesis
   1.311          apply -
   1.312          apply (rule disjI2)
   1.313          unfolding kle_def
   1.314 -        using k
   1.315 +        using k(2)
   1.316          apply (rule_tac x = k in exI)
   1.317          apply auto
   1.318          done
   1.319 @@ -1573,7 +1595,12 @@
   1.320    qed (insert sa ksimplexD[OF sa(1)], auto)
   1.321  next
   1.322    assume ?rs note rs=ksimplexD[OF this]
   1.323 -  guess a b by (rule ksimplex_extrema[OF `?rs`]) note ab = this
   1.324 +  obtain a b where ab:
   1.325 +    "a \<in> f"
   1.326 +    "b \<in> f"
   1.327 +    "\<forall>x\<in>f. kle n a x \<and> kle n x b"
   1.328 +    "\<forall>i. b i = (if i \<in> {1..n} then a i + 1 else a i)"
   1.329 +    by (rule ksimplex_extrema[OF `?rs`])
   1.330    def c \<equiv> "\<lambda>i. if i = (n + 1) then p - 1 else a i"
   1.331    have "c \<notin> f"
   1.332      apply (rule notI)
   1.333 @@ -1625,11 +1652,9 @@
   1.334          case False
   1.335          then have "z \<in> f"
   1.336            using z by auto
   1.337 -        then guess k
   1.338 -          apply (drule_tac ab(3)[THEN bspec[where x=z], THEN conjunct1])
   1.339 -          unfolding kle_def
   1.340 -          apply (erule exE)
   1.341 -          done
   1.342 +        with ab(3) have "kle n a z" by blast
   1.343 +        then obtain k where "k \<subseteq> {1..n}" "\<And>j. z j = a j + (if j \<in> k then 1 else 0)"
   1.344 +          unfolding kle_def by blast
   1.345          then show "kle (n + 1) c z"
   1.346            unfolding kle_def
   1.347            apply (rule_tac x="insert (n + 1) k" in exI)