# HG changeset patch
# User wenzelm
# Date 1377703216 -7200
# Node ID 7a4b4b3b9ecdb7aaf9ebf40204d1674dd4b1ed9f
# Parent  bd595338ca1802b0b27098e6911502b321cda6e4
tuned proofs;

diff -r bd595338ca18 -r 7a4b4b3b9ecd src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Aug 28 16:36:46 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Aug 28 17:20:16 2013 +0200
@@ -29,7 +29,8 @@
   apply (cases "b=0")
   defer
   apply (rule divide_nonneg_pos)
-  using assms apply auto
+  using assms
+  apply auto
   done
 
 lemma brouwer_compactness_lemma:
@@ -175,7 +176,8 @@
     apply (rule as(2)[rule_format]) using as(1)
     apply auto
     done
-  show "card s = Suc 0" unfolding * using card_insert by auto
+  show "card s = Suc 0"
+    unfolding * using card_insert by auto
 qed auto
 
 lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. (z = x) \<or> (z = y)))"
@@ -653,12 +655,14 @@
       have "1 \<le> card {k \<in> {1..n}. a k < x k}" "m \<le> card {k \<in> {1..n}. x k < b k}"
         apply (rule kle_strict_set)
         apply (rule a(2)[rule_format])
-        using a and xb apply auto
+        using a and xb
+        apply auto
         done
       thus ?thesis
         apply (rule_tac x=a in bexI, rule_tac x=b in bexI)
         using kle_range_combine[OF a(2)[rule_format] xb(3) Suc(5)[rule_format], of 1 "m"]
-        using a(1) xb(1-2) apply auto
+        using a(1) xb(1-2)
+        apply auto
         done
     next
       case True
@@ -764,10 +768,14 @@
   show ?thesis apply(rule disjI2,rule ext)
   proof -
     fix j
-    have "x j \<ge> b j" using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]]
-      unfolding assms(1)[rule_format] apply-apply(cases "j=k")
+    have "x j \<ge> b j"
+      using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]]
+      unfolding assms(1)[rule_format]
+      apply -
+      apply(cases "j = k")
       using False by auto
-    thus "x j = b j" using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
+    thus "x j = b j"
+      using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
     by auto
   qed
 qed
@@ -818,7 +826,7 @@
     using `s\<noteq>{}` assm using kle_minimal[of s n] by auto
   obtain b where b: "b \<in> s" "\<forall>x\<in>s. kle n x b"
     using `s\<noteq>{}` assm using kle_maximal[of s n] by auto
-  obtain c d where c_d: "c\<in>s" "d\<in>s" "kle n c d" "n \<le> card {k \<in> {1..n}. c k < d k}"
+  obtain c d where c_d: "c \<in> s" "d \<in> s" "kle n c d" "n \<le> card {k \<in> {1..n}. c k < d k}"
     using kle_range_induct[of s n n] using assm by auto
   have "kle n c b \<and> n \<le> card {k \<in> {1..n}. c k < b k}"
     apply (rule kle_range_combine_r[where y=d])
@@ -827,7 +835,7 @@
   hence "kle n a b \<and> n \<le> card {k\<in>{1..n}. a(k) < b(k)}"
     apply -
     apply (rule kle_range_combine_l[where y=c])
-    using a `c\<in>s` `b\<in>s` apply auto
+    using a `c \<in> s` `b \<in> s` apply auto
     done
   moreover
   have "card {1..n} \<ge> card {k\<in>{1..n}. a(k) < b(k)}"
@@ -2774,46 +2782,148 @@
 
 lemma kuhn_induction:
   assumes "0 < p" "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = 0) \<longrightarrow> (lab x j = 0)"
-                  "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)"
-        "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})"
-  shows "odd (card {s. ksimplex p (n+1) s \<and>((reduced lab (n+1)) `  s = {0..n+1})})" proof-
-  have *:"\<And>s t. odd (card s) \<Longrightarrow> s = t \<Longrightarrow> odd (card t)" "\<And>s f. (\<And>x. f x \<le> n +1 ) \<Longrightarrow> f ` s \<subseteq> {0..n+1}" by auto
-  show ?thesis apply(rule kuhn_simplex_lemma[unfolded mem_Collect_eq]) apply(rule,rule,rule *,rule reduced_labelling)
-    apply(rule *(1)[OF assms(4)]) apply(rule set_eqI) unfolding mem_Collect_eq apply(rule,erule conjE) defer apply(rule) proof-(*(rule,rule)*)
-    fix f assume as:"ksimplex p n f" "reduced lab n ` f = {0..n}"
-    have *:"\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = 0 \<longrightarrow> lab x j = 0" "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = p \<longrightarrow> lab x j = 1"
+    "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)"
+    "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})"
+  shows "odd (card {s. ksimplex p (n+1) s \<and>((reduced lab (n+1)) `  s = {0..n+1})})"
+proof -
+  have *: "\<And>s t. odd (card s) \<Longrightarrow> s = t \<Longrightarrow> odd (card t)"
+    "\<And>s f. (\<And>x. f x \<le> n +1 ) \<Longrightarrow> f ` s \<subseteq> {0..n+1}" by auto
+  show ?thesis
+    apply (rule kuhn_simplex_lemma[unfolded mem_Collect_eq])
+    apply (rule, rule, rule *, rule reduced_labelling)
+    apply (rule *(1)[OF assms(4)])
+    apply (rule set_eqI)
+    unfolding mem_Collect_eq
+    apply (rule, erule conjE)
+    defer
+    apply rule
+  proof -
+    fix f
+    assume as: "ksimplex p n f" "reduced lab n ` f = {0..n}"
+    have *: "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = 0 \<longrightarrow> lab x j = 0"
+      "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = p \<longrightarrow> lab x j = 1"
       using assms(2-3) using as(1)[unfolded ksimplex_def] by auto
-    have allp:"\<forall>x\<in>f. x (n + 1) = p" using assms(2) using as(1)[unfolded ksimplex_def] by auto
-    { fix x assume "x\<in>f" hence "reduced lab (n + 1) x < n + 1" apply-apply(rule reduced_labelling_nonzero)
-        defer using assms(3) using as(1)[unfolded ksimplex_def] by auto
-      hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) using reduced_labelling(1) by auto }
-    hence "reduced lab (n + 1) ` f = {0..n}" unfolding as(2)[symmetric] apply- apply(rule set_eqI) unfolding image_iff by auto
-    moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] .. then guess a ..
+    have allp: "\<forall>x\<in>f. x (n + 1) = p"
+      using assms(2) using as(1)[unfolded ksimplex_def] by auto
+    {
+      fix x
+      assume "x \<in> f"
+      hence "reduced lab (n + 1) x < n + 1"
+        apply -
+        apply (rule reduced_labelling_nonzero)
+        defer using assms(3) using as(1)[unfolded ksimplex_def]
+        apply auto
+        done
+      hence "reduced lab (n + 1) x = reduced lab n x"
+        apply -
+        apply (rule reduced_labelling_Suc)
+        using reduced_labelling(1)
+        apply auto
+        done
+    }
+    hence "reduced lab (n + 1) ` f = {0..n}"
+      unfolding as(2)[symmetric]
+      apply -
+      apply (rule set_eqI)
+      unfolding image_iff
+      apply auto
+      done
+    moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] ..
+    then guess a ..
     ultimately show "\<exists>s a. ksimplex p (n + 1) s \<and>
       a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<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))" (is ?ex)
-      apply(rule_tac x=s in exI,rule_tac x=a in exI) unfolding complete_face_top[OF *] using allp as(1) by auto
-  next fix f assume as:"\<exists>s a. ksimplex p (n + 1) s \<and>
+      apply (rule_tac x = s in exI)
+      apply (rule_tac x = a in exI)
+      unfolding complete_face_top[OF *]
+      using allp as(1)
+      apply auto
+      done
+  next
+    fix f
+    assume as: "\<exists>s a. ksimplex p (n + 1) s \<and>
       a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<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))" (is ?ex)
-    then guess s .. then guess a apply-apply(erule exE,(erule conjE)+) . note sa=this
-    { fix x assume "x\<in>f" hence "reduced lab (n + 1) x \<in> reduced lab (n + 1) ` f" by auto
-      hence "reduced lab (n + 1) x < n + 1" using sa(4) by auto
-      hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc)
-        using reduced_labelling(1) by auto }
-    thus part1:"reduced lab n ` f = {0..n}" unfolding sa(4)[symmetric] apply-apply(rule set_eqI) unfolding image_iff by auto
-    have *:"\<forall>x\<in>f. x (n + 1) = p" proof(cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0")
-      case True then guess j .. hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1" apply-apply(rule reduced_labelling_zero) apply assumption
-        apply(rule assms(2)[rule_format]) using sa(1)[unfolded ksimplex_def] unfolding sa by auto moreover
+    then guess s ..
+    then guess a
+      apply -
+      apply (erule exE,(erule conjE)+)
+      done
+    note sa = this
+    {
+      fix x
+      assume "x \<in> f"
+      hence "reduced lab (n + 1) x \<in> reduced lab (n + 1) ` f"
+        by auto
+      hence "reduced lab (n + 1) x < n + 1"
+        using sa(4) by auto
+      hence "reduced lab (n + 1) x = reduced lab n x"
+        apply -
+        apply (rule reduced_labelling_Suc)
+        using reduced_labelling(1)
+        apply auto
+        done
+    }
+    thus part1: "reduced lab n ` f = {0..n}"
+      unfolding sa(4)[symmetric]
+      apply -
+      apply (rule set_eqI)
+      unfolding image_iff
+      apply auto
+      done
+    have *: "\<forall>x\<in>f. x (n + 1) = p"
+    proof (cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0")
+      case True
+      then guess j ..
+      hence "\<And>x. x \<in> f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1"
+        apply -
+        apply (rule reduced_labelling_zero)
+        apply assumption
+        apply (rule assms(2)[rule_format])
+        using sa(1)[unfolded ksimplex_def]
+        unfolding sa
+        apply auto
+        done
+      moreover
       have "j - 1 \<in> {0..n}" using `j\<in>{1..n+1}` by auto
-      ultimately have False unfolding sa(4)[symmetric] unfolding image_iff by fastforce thus ?thesis by auto next
-      case False hence "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p" using sa(5) by fastforce then guess j .. note j=this
-      thus ?thesis proof(cases "j = n+1")
-        case False hence *:"j\<in>{1..n}" using j by auto
-        hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab n x < j" apply(rule reduced_labelling_nonzero) proof- fix x assume "x\<in>f"
-          hence "lab x j = 1" apply-apply(rule assms(3)[rule_format,OF j(1)])
-            using sa(1)[unfolded ksimplex_def] using j unfolding sa by auto thus "lab x j \<noteq> 0" by auto qed
-        moreover have "j\<in>{0..n}" using * by auto
-        ultimately have False unfolding part1[symmetric] using * unfolding image_iff by auto thus ?thesis by auto qed auto qed
-    thus "ksimplex p n f" using as unfolding simplex_top_face[OF assms(1) *,symmetric] by auto qed qed
+      ultimately have False
+        unfolding sa(4)[symmetric]
+        unfolding image_iff
+        by fastforce
+      thus ?thesis by auto
+    next
+      case False
+      hence "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p"
+        using sa(5) by fastforce then guess j .. note j=this
+      thus ?thesis
+      proof (cases "j = n + 1")
+        case False hence *: "j \<in> {1..n}"
+          using j by auto
+        hence "\<And>x. x \<in> f \<Longrightarrow> reduced lab n x < j"
+          apply (rule reduced_labelling_nonzero)
+        proof -
+          fix x
+          assume "x \<in> f"
+          hence "lab x j = 1"
+            apply -
+            apply (rule assms(3)[rule_format,OF j(1)])
+            using sa(1)[unfolded ksimplex_def]
+            using j
+            unfolding sa
+            apply auto
+            done
+          thus "lab x j \<noteq> 0" by auto
+        qed
+        moreover have "j \<in> {0..n}" using * by auto
+        ultimately have False
+          unfolding part1[symmetric]
+          using * unfolding image_iff
+          by auto
+        thus ?thesis by auto
+      qed auto
+    qed
+    thus "ksimplex p n f"
+      using as unfolding simplex_top_face[OF assms(1) *,symmetric] by auto
+  qed
+qed
 
 lemma kuhn_induction_Suc:
   assumes "0 < p" "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> (x j = 0) \<longrightarrow> (lab x j = 0)"
@@ -2822,51 +2932,135 @@
   shows "odd (card {s. ksimplex p (Suc n) s \<and>((reduced lab (Suc n)) `  s = {0..Suc n})})"
   using assms unfolding Suc_eq_plus1 by(rule kuhn_induction)
 
+
 subsection {* And so we get the final combinatorial result. *}
 
-lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}" (is "?l = ?r") proof
-  assume l:?l guess a using ksimplexD(3)[OF l, unfolded add_0] unfolding card_1_exists .. note a=this
-  have "a = (\<lambda>x. p)" using ksimplexD(5)[OF l, rule_format, OF a(1)] by(rule,auto) thus ?r using a by auto next
-  assume r:?r show ?l unfolding r ksimplex_eq by auto qed
+lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}" (is "?l = ?r")
+proof
+  assume l: ?l
+  guess a using ksimplexD(3)[OF l, unfolded add_0] unfolding card_1_exists .. note a = this
+  have "a = (\<lambda>x. p)"
+    using ksimplexD(5)[OF l, rule_format, OF a(1)] by rule auto
+  thus ?r using a by auto
+next
+  assume r: ?r
+  show ?l unfolding r ksimplex_eq by auto
+qed
 
-lemma reduce_labelling_zero[simp]: "reduced lab 0 x = 0" apply(rule reduced_labelling_unique) by auto
+lemma reduce_labelling_zero[simp]: "reduced lab 0 x = 0"
+  by (rule reduced_labelling_unique) auto
 
 lemma kuhn_combinatorial:
   assumes "0 < p" "\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> (x j = 0) \<longrightarrow> (lab x j = 0)"
-  "\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n  \<and> (x j = p) \<longrightarrow> (lab x j = 1)"
-  shows " odd (card {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})})" using assms proof(induct n)
+    "\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n  \<and> (x j = p) \<longrightarrow> (lab x j = 1)"
+  shows " odd (card {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})})"
+  using assms
+proof (induct n)
   let ?M = "\<lambda>n. {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})}"
-  { case 0 have *:"?M 0 = {{(\<lambda>x. p)}}" unfolding ksimplex_0 by auto show ?case unfolding * by auto }
-  case (Suc n) have "odd (card (?M n))" apply(rule Suc(1)[OF Suc(2)]) using Suc(3-) by auto
-  thus ?case apply-apply(rule kuhn_induction_Suc) using Suc(2-) by auto qed
+  {
+    case 0
+    have *: "?M 0 = {{(\<lambda>x. p)}}"
+      unfolding ksimplex_0 by auto
+    show ?case unfolding * by auto
+  next
+    case (Suc n)
+    have "odd (card (?M n))"
+      apply (rule Suc(1)[OF Suc(2)])
+      using Suc(3-)
+      apply auto
+      done
+    thus ?case
+      apply -
+      apply (rule kuhn_induction_Suc)
+      using Suc(2-)
+      apply auto
+      done
+  }
+qed
 
-lemma kuhn_lemma: assumes "0 < (p::nat)" "0 < (n::nat)"
-  "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (label x i = (0::nat)) \<or> (label x i = 1))"
-  "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = 0) \<longrightarrow> (label x i = 0))"
-  "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = p) \<longrightarrow> (label x i = 1))"
+lemma kuhn_lemma:
+  assumes "0 < (p::nat)" "0 < (n::nat)"
+    "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (label x i = (0::nat)) \<or> (label x i = 1))"
+    "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = 0) \<longrightarrow> (label x i = 0))"
+    "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = p) \<longrightarrow> (label x i = 1))"
   obtains q where "\<forall>i\<in>{1..n}. q i < p"
-  "\<forall>i\<in>{1..n}. \<exists>r s. (\<forall>j\<in>{1..n}. q(j) \<le> r(j) \<and> r(j) \<le> q(j) + 1) \<and>
-                               (\<forall>j\<in>{1..n}. q(j) \<le> s(j) \<and> s(j) \<le> q(j) + 1) \<and>
-                               ~(label r i = label s i)" proof-
-  let ?A = "{s. ksimplex p n s \<and> reduced label n ` s = {0..n}}" have "n\<noteq>0" using assms by auto
-  have conjD:"\<And>P Q. P \<and> Q \<Longrightarrow> P" "\<And>P Q. P \<and> Q \<Longrightarrow> Q" by auto
-  have "odd (card ?A)" apply(rule kuhn_combinatorial[of p n label]) using assms by auto
-  hence "card ?A \<noteq> 0" apply-apply(rule ccontr) by auto hence "?A \<noteq> {}" unfolding card_eq_0_iff by auto
-  then obtain s where "s\<in>?A" by auto note s=conjD[OF this[unfolded mem_Collect_eq]]
-  guess a b apply(rule ksimplex_extrema_strong[OF s(1) `n\<noteq>0`]) . note ab=this
-  show ?thesis apply(rule that[of a]) proof(rule_tac[!] ballI) fix i assume "i\<in>{1..n}"
-    hence "a i + 1 \<le> p" apply-apply(rule order_trans[of _ "b i"]) apply(subst ab(5)[THEN spec[where x=i]])
-      using s(1)[unfolded ksimplex_def] defer apply- apply(erule conjE)+ apply(drule_tac bspec[OF _ ab(2)])+ by auto
+    "\<forall>i\<in>{1..n}. \<exists>r s. (\<forall>j\<in>{1..n}. q(j) \<le> r(j) \<and> r(j) \<le> q(j) + 1) \<and>
+                                 (\<forall>j\<in>{1..n}. q(j) \<le> s(j) \<and> s(j) \<le> q(j) + 1) \<and>
+                                 ~(label r i = label s i)"
+proof -
+  let ?A = "{s. ksimplex p n s \<and> reduced label n ` s = {0..n}}"
+  have "n \<noteq> 0" using assms by auto
+  have conjD:"\<And>P Q. P \<and> Q \<Longrightarrow> P" "\<And>P Q. P \<and> Q \<Longrightarrow> Q"
+    by auto
+  have "odd (card ?A)"
+    apply (rule kuhn_combinatorial[of p n label])
+    using assms
+    apply auto
+    done
+  hence "card ?A \<noteq> 0"
+    apply -
+    apply (rule ccontr)
+    apply auto
+    done
+  hence "?A \<noteq> {}" unfolding card_eq_0_iff by auto
+  then obtain s where "s \<in> ?A"
+    by auto note s=conjD[OF this[unfolded mem_Collect_eq]]
+  guess a b by (rule ksimplex_extrema_strong[OF s(1) `n\<noteq>0`]) note ab = this
+  show ?thesis
+    apply (rule that[of a])
+    apply (rule_tac[!] ballI)
+  proof -
+    fix i
+    assume "i\<in>{1..n}"
+    hence "a i + 1 \<le> p"
+      apply -
+      apply (rule order_trans[of _ "b i"])
+      apply (subst ab(5)[THEN spec[where x=i]])
+      using s(1)[unfolded ksimplex_def]
+      defer
+      apply -
+      apply (erule conjE)+
+      apply (drule_tac bspec[OF _ ab(2)])+
+      apply auto
+      done
     thus "a i < p" by auto
-    case goal2 hence "i \<in> reduced label n ` s" using s by auto then guess u unfolding image_iff .. note u=this
-    from goal2 have "i - 1 \<in> reduced label n ` s" using s by auto then guess v unfolding image_iff .. note v=this
-    show ?case apply(rule_tac x=u in exI, rule_tac x=v in exI) apply(rule conjI) defer apply(rule conjI) defer 2 proof(rule_tac[1-2] ballI)
-      show "label u i \<noteq> label v i" using reduced_labelling[of label n u] reduced_labelling[of label n v]
-        unfolding u(2)[symmetric] v(2)[symmetric] using goal2 by auto
-      fix j assume j:"j\<in>{1..n}" show "a j \<le> u j \<and> u j \<le> a j + 1" "a j \<le> v j \<and> v j \<le> a j + 1"
-        using conjD[OF ab(4)[rule_format, OF u(1)]] and conjD[OF ab(4)[rule_format, OF v(1)]] apply-
-        apply(drule_tac[!] kle_imp_pointwise)+ apply(erule_tac[!] x=j in allE)+ unfolding ab(5)[rule_format] using j
-        by auto qed qed qed
+  next
+    case goal2
+    hence "i \<in> reduced label n ` s" using s by auto
+    then guess u unfolding image_iff .. note u = this
+    from goal2 have "i - 1 \<in> reduced label n ` s"
+      using s by auto
+    then guess v unfolding image_iff .. note v = this
+    show ?case
+      apply (rule_tac x = u in exI)
+      apply (rule_tac x = v in exI)
+      apply (rule conjI)
+      defer
+      apply (rule conjI)
+      defer 2
+      apply (rule_tac[1-2] ballI)
+    proof -
+      show "label u i \<noteq> label v i"
+        using reduced_labelling [of label n u] reduced_labelling [of label n v]
+        unfolding u(2)[symmetric] v(2)[symmetric]
+        using goal2
+        apply auto
+        done
+      fix j
+      assume j: "j \<in> {1..n}"
+      show "a j \<le> u j \<and> u j \<le> a j + 1" "a j \<le> v j \<and> v j \<le> a j + 1"
+        using conjD[OF ab(4)[rule_format, OF u(1)]]
+          and conjD[OF ab(4)[rule_format, OF v(1)]]
+        apply -
+        apply (drule_tac[!] kle_imp_pointwise)+
+        apply (erule_tac[!] x=j in allE)+
+        unfolding ab(5)[rule_format]
+        using j
+        apply auto
+        done
+    qed
+  qed
+qed
 
 
 subsection {* The main result for the unit cube. *}
@@ -2986,7 +3180,8 @@
     note e=this[rule_format,unfolded dist_norm]
     show ?thesis
       apply (rule_tac x="min (e/2) (d/real n/8)" in exI)
-    proof safe
+      apply safe
+    proof -
       show "0 < min (e / 2) (d / real n / 8)"
         using d' e by auto
       fix x y z i
@@ -3216,7 +3411,7 @@
     and t :: "('b::euclidean_space) set"
   assumes "s homeomorphic t"
   shows "(\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)) \<longleftrightarrow>
-         (\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))"
+    (\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))"
 proof -
   guess r using assms[unfolded homeomorphic_def homeomorphism_def] ..
   then guess i ..
@@ -3244,8 +3439,9 @@
     apply -
     apply (rule invertible_fixpoint_property[OF continuous_on_id _ _ _ _ assms(2), of t h g])
     prefer 7
-    apply (rule_tac y=y in that)
-    using assms apply auto
+    apply (rule_tac y = y in that)
+    using assms
+    apply auto
     done
 qed
 
@@ -3253,7 +3449,7 @@
 subsection {*So the Brouwer theorem for any set with nonempty interior. *}
 
 lemma brouwer_weak:
-  fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'a::ordered_euclidean_space"
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'a::ordered_euclidean_space"
   assumes "compact s" "convex s" "interior s \<noteq> {}" "continuous_on s f" "f ` s \<subseteq> s"
   obtains x where "x \<in> s" "f x = x"
 proof -
@@ -3290,7 +3486,8 @@
   rather involved @{text "HOMEOMORPHIC_CONVEX_COMPACT"} theorem, just using
   a scaling and translation to put the set inside the unit cube. *}
 
-lemma brouwer: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'a"
+lemma brouwer:
+  fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'a"
   assumes "compact s" "convex s" "s \<noteq> {}" "continuous_on s f" "f ` s \<subseteq> s"
   obtains x where "x \<in> s" "f x = x"
 proof -
@@ -3353,7 +3550,8 @@
     apply (simp add: * norm_minus_commute)
     done
   note x = this
-  hence "scaleR 2 a = scaleR 1 x + scaleR 1 x" by (auto simp add:algebra_simps)
+  hence "scaleR 2 a = scaleR 1 x + scaleR 1 x"
+    by (auto simp add: algebra_simps)
   hence "a = x" unfolding scaleR_left_distrib[symmetric] by auto
   thus False using x assms by auto
 qed
@@ -3361,14 +3559,15 @@
 
 subsection {*Bijections between intervals. *}
 
-definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::ordered_euclidean_space" where
-  "interval_bij \<equiv> \<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i)"
+definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::ordered_euclidean_space"
+  where "interval_bij =
+    (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))"
 
 lemma interval_bij_affine:
   "interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) +
     (\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))"
   by (auto simp: setsum_addf[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff
-                 field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum_cong)
+    field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum_cong)
 
 lemma continuous_interval_bij:
   "continuous (at x) (interval_bij (a,b::'a::ordered_euclidean_space) (u,v::'a))"
@@ -3384,7 +3583,8 @@
   assumes "x \<in> {a..b}" "{u..v} \<noteq> {}"
   shows "interval_bij (a,b) (u,v) x \<in> {u..v}"
   apply (simp only: interval_bij_def split_conv mem_interval inner_setsum_left_Basis cong: ball_cong)
-proof safe
+  apply safe
+proof -
   fix i :: 'a
   assume i: "i \<in> Basis"
   have "{a..b} \<noteq> {}" using assms by auto