# HG changeset patch
# User wenzelm
# Date 1377723023 -7200
# Node ID 4766fbe322b56bda21001d4734293995074d2088
# Parent  7facc08da8060f81f4736f710d07f9489de58c05
tuned proofs;

diff -r 7facc08da806 -r 4766fbe322b5 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Aug 28 22:25:14 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Aug 28 22:50:23 2013 +0200
@@ -96,12 +96,15 @@
   shows "setsum g C = setsum g A + setsum g B"
   using setsum_Un_disjoint[OF assms(1-3)] and assms(4) by auto
 
-lemma kuhn_counting_lemma: assumes "finite faces" "finite simplices"
-  "\<forall>f\<in>faces. bnd f  \<longrightarrow> (card {s \<in> simplices. face f s} = 1)"
-  "\<forall>f\<in>faces. \<not> bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 2)"
-  "\<forall>s\<in>simplices. compo s  \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 1)"
-  "\<forall>s\<in>simplices. \<not> compo s \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 0) \<or>
-                             (card {f \<in> faces. face f s \<and> compo' f} = 2)"
+lemma kuhn_counting_lemma:
+  assumes
+    "finite faces"
+    "finite simplices"
+    "\<forall>f\<in>faces. bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 1)"
+    "\<forall>f\<in>faces. \<not> bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 2)"
+    "\<forall>s\<in>simplices. compo s \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 1)"
+    "\<forall>s\<in>simplices. \<not> compo s \<longrightarrow>
+      (card {f \<in> faces. face f s \<and> compo' f} = 0) \<or> (card {f \<in> faces. face f s \<and> compo' f} = 2)"
     "odd(card {f \<in> faces. compo' f \<and> bnd f})"
   shows "odd(card {s \<in> simplices. compo s})"
 proof -
@@ -118,28 +121,39 @@
     using assms(1)
     apply (auto simp add: card_Un_Int, auto simp add:conj_commute)
     done
-  have lem2:"setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f j}) simplices =
-              1 * card {f \<in> faces. compo' f \<and> bnd f}"
-       "setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> \<not> bnd f}. face f j}) simplices =
-              2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}"
+  have lem2:
+    "setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f j}) simplices =
+      1 * card {f \<in> faces. compo' f \<and> bnd f}"
+    "setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> \<not> bnd f}. face f j}) simplices =
+      2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}"
     apply(rule_tac[!] setsum_multicount)
     using assms
     apply auto
     done
-  have lem3:"setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) simplices =
-    setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices.   compo s}+
-    setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s}"
-    apply(rule setsum_Un_disjoint') using assms(2) by auto
-  have lem4:"setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. compo s}
-    = setsum (\<lambda>s. 1) {s \<in> simplices. compo s}"
-    apply(rule setsum_cong2) using assms(5) by auto
+  have lem3:
+    "setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) simplices =
+      setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices.   compo s}+
+      setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s}"
+    apply (rule setsum_Un_disjoint')
+    using assms(2)
+    apply auto
+    done
+  have lem4: "setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. compo s} =
+    setsum (\<lambda>s. 1) {s \<in> simplices. compo s}"
+    apply (rule setsum_cong2)
+    using assms(5)
+    apply auto
+    done
   have lem5: "setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s} =
     setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f})
            {s \<in> simplices. (\<not> compo s) \<and> (card {f \<in> faces. face f s \<and> compo' f} = 0)} +
     setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f})
            {s \<in> simplices. (\<not> compo s) \<and> (card {f \<in> faces. face f s \<and> compo' f} = 2)}"
-    apply(rule setsum_Un_disjoint') using assms(2,6) by auto
-  have *:"int (\<Sum>s\<in>{s \<in> simplices. compo s}. card {f \<in> faces. face f s \<and> compo' f}) =
+    apply (rule setsum_Un_disjoint')
+    using assms(2,6)
+    apply auto
+    done
+  have *: "int (\<Sum>s\<in>{s \<in> simplices. compo s}. card {f \<in> faces. face f s \<and> compo' f}) =
     int (card {f \<in> faces. compo' f \<and> bnd f} + 2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}) -
     int (card {s \<in> simplices. \<not> compo s \<and> card {f \<in> faces. face f s \<and> compo' f} = 2} * 2)"
     using lem1[unfolded lem3 lem2 lem5] by auto
@@ -229,7 +243,8 @@
     apply (rule set_eqI)
     unfolding singleton_iff
     apply (rule, rule inj[unfolded inj_on_def, rule_format])
-    unfolding a using a(2) and assms and inj[unfolded inj_on_def] apply auto
+    unfolding a using a(2) and assms and inj[unfolded inj_on_def]
+    apply auto
     done
   show ?thesis
     apply (rule image_lemma_0)
@@ -247,7 +262,8 @@
   then show ?thesis
     apply -
     apply (rule disjI1, rule image_lemma_0)
-    using assms(1) apply auto
+    using assms(1)
+    apply auto
     done
 next
   let ?M = "{a\<in>s. f ` (s - {a}) = t - {b}}"
@@ -319,7 +335,9 @@
     using assms(3) by (auto intro: card_ge_0_finite)
   show "finite {f. \<exists>s\<in>simplices. face f s}"
     unfolding assms(2)[rule_format] and *
-    apply (rule finite_UN_I[OF assms(1)]) using ** apply auto
+    apply (rule finite_UN_I[OF assms(1)])
+    using **
+    apply auto
     done
   have *: "\<And>P f s. s\<in>simplices \<Longrightarrow> (f \<in> {f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s - {a}}) \<and>
     (\<exists>a\<in>s. (f = s - {a})) \<and> P f \<longleftrightarrow> (\<exists>a\<in>s. (f = s - {a}) \<and> P f)" by auto
@@ -336,7 +354,8 @@
   show "rl ` s = {0..n+1} \<Longrightarrow> card ?S = 1" "rl ` s \<noteq> {0..n+1} \<Longrightarrow> card ?S = 0 \<or> card ?S = 2"
     unfolding S
     apply(rule_tac[!] image_lemma_1 image_lemma_2)
-    using ** assms(4) and s apply auto
+    using ** assms(4) and s
+    apply auto
     done
 qed
 
@@ -429,9 +448,9 @@
 
 lemma pointwise_antisym:
   fixes x :: "nat \<Rightarrow> nat"
-  shows "(\<forall>j. x j \<le> y j) \<and> (\<forall>j. y j \<le> x j) \<longleftrightarrow> (x = y)"
+  shows "(\<forall>j. x j \<le> y j) \<and> (\<forall>j. y j \<le> x j) \<longleftrightarrow> x = y"
   apply (rule, rule ext, erule conjE)
-  apply (erule_tac x=xa in allE)+
+  apply (erule_tac x = xa in allE)+
   apply auto
   done
 
@@ -491,11 +510,12 @@
     apply (rule pointwise_minimal_pointwise_maximal(1)[OF assms(1-2)])
     apply (rule, rule)
     apply (drule_tac assms(3)[rule_format], assumption)
-    using kle_imp_pointwise apply auto
+    using kle_imp_pointwise
+    apply auto
     done
   then guess a .. note a = this
   show ?thesis
-    apply (rule_tac x=a in bexI)
+    apply (rule_tac x = a in bexI)
   proof
     fix x
     assume "x \<in> s"
@@ -504,13 +524,14 @@
       apply -
     proof (erule disjE)
       assume "kle n x a"
-      hence "x = a"
+      then have "x = a"
         apply -
         unfolding pointwise_antisym[symmetric]
         apply (drule kle_imp_pointwise)
-        using a(2)[rule_format,OF `x\<in>s`] apply auto
+        using a(2)[rule_format,OF `x\<in>s`]
+        apply auto
         done
-      thus ?thesis using kle_refl by auto
+      then show ?thesis using kle_refl by auto
     qed
   qed (insert a, auto)
 qed
@@ -565,16 +586,18 @@
     "m1 \<le> card {k\<in>{1..n}. x k < y k}"
     "m2 \<le> card {k\<in>{1..n}. y k < z k}"
   shows "kle n x z \<and> m1 + m2 \<le> card {k\<in>{1..n}. x k < z k}"
-    apply (rule, rule kle_trans[OF assms(1-3)])
+  apply (rule, rule kle_trans[OF assms(1-3)])
 proof -
   have "\<And>j. x j < y j \<Longrightarrow> x j < z j"
     apply (rule less_le_trans)
-    using kle_imp_pointwise[OF assms(2)] apply auto
+    using kle_imp_pointwise[OF assms(2)]
+    apply auto
     done
   moreover
   have "\<And>j. y j < z j \<Longrightarrow> x j < z j"
     apply (rule le_less_trans)
-    using kle_imp_pointwise[OF assms(1)] apply auto
+    using kle_imp_pointwise[OF assms(1)]
+    apply auto
     done
   ultimately
   have *: "{k\<in>{1..n}. x k < y k} \<union> {k\<in>{1..n}. y k < z k} = {k\<in>{1..n}. x k < z k}"
@@ -695,7 +718,8 @@
   show ?thesis
     unfolding kle_def
     apply (rule_tac x="kk1 \<union> kk2" in exI)
-    apply (rule) defer
+    apply rule
+    defer
   proof
     fix i
     show "c i = a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)"
@@ -746,7 +770,7 @@
 
 lemma kle_adjacent:
   assumes "\<forall>j. b j = (if j = k then a(j) + 1 else a j)" "kle n a x" "kle n x b"
-  shows "(x = a) \<or> (x = b)"
+  shows "x = a \<or> x = b"
 proof (cases "x k = a k")
   case True
   show ?thesis
@@ -761,7 +785,8 @@
       using True
       apply auto
       done
-    thus "x j = a j" using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]] by auto
+    then show "x j = a j"
+      using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]] by auto
   qed
 next
   case False
@@ -774,7 +799,7 @@
       apply -
       apply(cases "j = k")
       using False by auto
-    thus "x j = b j"
+    then show "x j = b j"
       using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
     by auto
   qed
@@ -830,12 +855,14 @@
     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])
-    using c_d a b apply auto
+    using c_d a b
+    apply auto
     done
   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)}"
@@ -905,16 +932,18 @@
   case False
   then obtain b where b: "b\<in>s" "\<not> kle n b a" "\<forall>x\<in>{x \<in> s. \<not> kle n x a}. kle n b x"
     using kle_minimal[of "{x\<in>s. \<not> kle n x a}" n] and assm by auto
-  hence  **: "1 \<le> card {k\<in>{1..n}. a k < b k}"
+  then have **: "1 \<le> card {k\<in>{1..n}. a k < b k}"
     apply -
     apply (rule kle_strict_set)
-    using assm(6) and `a\<in>s` apply (auto simp add:kle_refl)
+    using assm(6) and `a\<in>s`
+    apply (auto simp add:kle_refl)
     done
 
   let ?kle1 = "{x \<in> s. \<not> kle n x a}"
   have "card ?kle1 > 0"
     apply (rule ccontr)
-    using assm(2) and False apply auto
+    using assm(2) and False
+    apply auto
     done
   hence sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)"
     using assm(2) by auto
@@ -925,7 +954,8 @@
   let ?kle2 = "{x \<in> s. kle n x a}"
   have "card ?kle2 > 0"
     apply (rule ccontr)
-    using assm(6)[rule_format,of a a] and `a\<in>s` and assm(2) apply auto
+    using assm(6)[rule_format,of a a] and `a\<in>s` and assm(2)
+    apply auto
     done
   hence sizekle2: "card ?kle2 = Suc (card ?kle2 - 1)"
     using assm(2) by auto
@@ -948,11 +978,13 @@
       by auto
     have "kle n e a \<and> card {x \<in> s. kle n x a} - 1 \<le> card {k \<in> {1..n}. e k < a k}"
       apply (rule kle_range_combine_r[where y=f])
-      using e_f using `a\<in>s` assm(6) apply auto
+      using e_f using `a\<in>s` assm(6)
+      apply auto
       done
     moreover have "kle n b d \<and> card {x \<in> s. \<not> kle n x a} - 1 \<le> card {k \<in> {1..n}. b k < d k}"
       apply (rule kle_range_combine_l[where y=c])
-      using c_d using assm(6) and b apply auto
+      using c_d using assm(6) and b
+      apply auto
       done
     hence "kle n a d \<and> 2 + (card {x \<in> s. \<not> kle n x a} - 1) \<le> card {k \<in> {1..n}. a k < d k}"
       apply -
@@ -983,24 +1015,27 @@
     have kkk: "k \<in> kk"
       apply (rule ccontr)
       using k(1)
-      unfolding kk apply auto
+      unfolding kk
+      apply auto
       done
     show "b j = (if j = k then a j + 1 else a j)"
     proof (cases "j \<in> kk")
       case True
-      hence "j = k"
-      apply - apply (rule k(2)[rule_format])
-      using kk_raw kkk apply auto
-      done
-      thus ?thesis unfolding kk using kkk by auto
+      then have "j = k"
+        apply -
+        apply (rule k(2)[rule_format])
+        using kk_raw kkk
+        apply auto
+        done
+      then show ?thesis unfolding kk using kkk by auto
     next
       case False
-      hence "j \<noteq> k"
+      then have "j \<noteq> k"
         using k(2)[rule_format, of j k] and kk_raw kkk by auto
-      thus ?thesis unfolding kk using kkk and False
+      then show ?thesis unfolding kk using kkk and False
         by auto
     qed
-  qed(insert k(1) `b\<in>s`, auto)
+  qed (insert k(1) `b\<in>s`, auto)
 qed
 
 lemma ksimplex_predecessor:
@@ -1017,13 +1052,15 @@
   hence **: "1 \<le> card {k\<in>{1..n}. a k > b k}"
     apply -
     apply (rule kle_strict_set)
-    using assm(6) and `a\<in>s` apply (auto simp add: kle_refl)
+    using assm(6) and `a\<in>s`
+    apply (auto simp add: kle_refl)
     done
 
   let ?kle1 = "{x \<in> s. \<not> kle n a x}"
   have "card ?kle1 > 0"
     apply (rule ccontr)
-    using assm(2) and False apply auto
+    using assm(2) and False
+    apply auto
     done
   hence sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)"
     using assm(2) by auto
@@ -1034,7 +1071,8 @@
   let ?kle2 = "{x \<in> s. kle n a x}"
   have "card ?kle2 > 0"
     apply (rule ccontr)
-    using assm(6)[rule_format,of a a] and `a\<in>s` and assm(2) apply auto
+    using assm(6)[rule_format,of a a] and `a\<in>s` and assm(2)
+    apply auto
     done
   hence sizekle2:"card ?kle2 = Suc (card ?kle2 - 1)"
     using assm(2) by auto
@@ -1057,11 +1095,13 @@
       by auto
     have "kle n a e \<and> card {x \<in> s. kle n a x} - 1 \<le> card {k \<in> {1..n}. e k > a k}"
       apply (rule kle_range_combine_l[where y=f])
-      using e_f and `a\<in>s` assm(6) apply auto
+      using e_f and `a\<in>s` assm(6)
+      apply auto
       done
     moreover have "kle n d b \<and> card {x \<in> s. \<not> kle n a x} - 1 \<le> card {k \<in> {1..n}. b k > d k}"
       apply (rule kle_range_combine_r[where y=c])
-      using c_d and assm(6) and b apply auto
+      using c_d and assm(6) and b
+      apply auto
       done
     hence "kle n d a \<and> (card {x \<in> s. \<not> kle n a x} - 1) + 2 \<le> card {k \<in> {1..n}. a k > d k}"
       apply -
@@ -1071,7 +1111,8 @@
     ultimately have "kle n d e \<and> (card ?kle1 - 1 + 2) + (card ?kle2 - 1) \<le> card {k\<in>{1..n}. e k > d k}"
       apply -
       apply (rule kle_range_combine[where y=a])
-      using assm(6)[rule_format,OF `e\<in>s` `d\<in>s`] apply blast+
+      using assm(6)[rule_format,OF `e\<in>s` `d\<in>s`]
+      apply blast+
       done
     moreover have "card {k \<in> {1..n}. e k > d k} \<le> card {1..n}"
       by (rule card_mono) auto
@@ -1100,7 +1141,8 @@
       hence "j = k"
         apply -
         apply (rule k(2)[rule_format])
-        using kk_raw kkk apply auto
+        using kk_raw kkk
+        apply auto
         done
       thus ?thesis unfolding kk using kkk by auto
     next
@@ -1123,14 +1165,14 @@
   using assms
   apply -
 proof (induct m arbitrary: s)
-  have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}"
+  case 0
+  have [simp]: "{f. \<forall>x. f x = d} = {\<lambda>x. d}"
     apply (rule set_eqI,rule)
     unfolding mem_Collect_eq
     apply (rule, rule ext)
     apply auto
     done
-  case 0
-  thus ?case by(auto simp add: *)
+  from 0 show ?case by auto
 next
   case (Suc m)
   guess a using card_eq_SucD[OF Suc(4)] ..
@@ -1254,9 +1296,8 @@
       then guess k unfolding kle_def .. note k = this
       hence *: "n + 1 \<notin> k" using xyp by auto
       have "\<not> (\<exists>x\<in>k. x\<notin>{1..n})"
-        apply (rule ccontr)
-        unfolding not_not
-        apply(erule bexE)
+        apply (rule notI)
+        apply (erule bexE)
       proof -
         fix x
         assume as: "x \<in> k" "x \<notin> {1..n}"
@@ -1276,23 +1317,25 @@
       hence "kle (n + 1) y x"
         using ksimplexD(6)[OF sa(1),rule_format, of x y] and as by auto
       then guess k unfolding kle_def .. note k = this
-      hence *: "n + 1 \<notin> k" using xyp by auto
-      hence "\<not> (\<exists>x\<in>k. x\<notin>{1..n})"
+      then have *: "n + 1 \<notin> k" using xyp by auto
+      then have "\<not> (\<exists>x\<in>k. x\<notin>{1..n})"
         apply -
-        apply (rule ccontr)
-        unfolding not_not
+        apply (rule notI)
         apply (erule bexE)
       proof -
         fix x
         assume as: "x \<in> k" "x \<notin> {1..n}"
         have "x \<noteq> n + 1" using as and * by auto
-        thus False using as and k[THEN conjunct1,unfolded subset_eq] by auto
+        then show False using as and k[THEN conjunct1,unfolded subset_eq] by auto
       qed
-      thus ?thesis
+      then show ?thesis
         apply -
         apply (rule disjI2)
         unfolding kle_def
-        using k apply (rule_tac x = k in exI) by auto
+        using k
+        apply (rule_tac x = k in exI)
+        apply auto
+        done
     qed
   next
     fix x j
@@ -1306,13 +1349,14 @@
   qed (insert sa ksimplexD[OF sa(1)], auto)
 next
   assume ?rs note rs=ksimplexD[OF this]
-  guess a b apply (rule ksimplex_extrema[OF `?rs`]) . note ab = this
+  guess a b by (rule ksimplex_extrema[OF `?rs`]) note ab = this
   def c \<equiv> "\<lambda>i. if i = (n + 1) then p - 1 else a i"
   have "c \<notin> f"
-    apply (rule ccontr) unfolding not_not
+    apply (rule notI)
     apply (drule assms(2)[rule_format])
     unfolding c_def
-    using assms(1) apply auto
+    using assms(1)
+    apply auto
     done
   thus ?ls
     apply (rule_tac x = "insert c f" in exI, rule_tac x = c in exI)
@@ -1334,12 +1378,16 @@
       show ?thesis
         unfolding True c_def
         apply (cases "j=n+1")
-        using ab(1) and rs(4) apply auto
+        using ab(1) and rs(4)
+        apply auto
         done
     qed (insert x rs(4), auto simp add:c_def)
     show "j \<notin> {1..n + 1} \<longrightarrow> x j = p"
       apply (cases "x = c")
-      using x ab(1) rs(5) unfolding c_def by auto
+      using x ab(1) rs(5)
+      unfolding c_def
+      apply auto
+      done
     {
       fix z
       assume z: "z \<in> insert c f"
@@ -1367,9 +1415,9 @@
     assume y: "y \<in> insert c f"
     show "kle (n + 1) x y \<or> kle (n + 1) y x"
     proof (cases "x = c \<or> y = c")
-      case False hence **:"x\<in>f" "y\<in>f" using x y by auto
+      case False hence **: "x \<in> f" "y \<in> f" using x y by auto
       show ?thesis using rs(6)[rule_format,OF **]
-        by(auto dest: kle_Suc)
+        by (auto dest: kle_Suc)
     qed (insert * x y, auto)
   qed (insert rs, auto)
 qed
@@ -1385,7 +1433,9 @@
     apply (rule ccontr)
     using *[OF assms(3), of a0 a1]
     unfolding assms(6)[THEN spec[where x=j]]
-    using assms(1-2,4-5) by auto
+    using assms(1-2,4-5)
+    apply auto
+    done
 qed
 
 lemma ksimplex_fix_plane_0:
@@ -1407,11 +1457,11 @@
 proof (rule ccontr)
   note s = ksimplexD[OF assms(1),rule_format]
   assume as: "a \<noteq> a0"
-  hence *: "a0 \<in> s - {a}"
+  then have *: "a0 \<in> s - {a}"
     using assms(5) by auto
-  hence "a1 = a"
+  then have "a1 = a"
     using ksimplex_fix_plane[OF assms(2-)] by auto
-  thus False
+  then show False
     using as and assms(3,5) and assms(7)[rule_format,of j]
     unfolding assms(4)[rule_format,OF *]
     using s(4)[OF assms(6), of j]
@@ -1430,7 +1480,8 @@
     guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note exta = this[rule_format]
     have a:"a = a1"
       apply (rule ksimplex_fix_plane_0[OF assms(2,4-5)])
-      using exta(1-2,5) apply auto
+      using exta(1-2,5)
+      apply auto
       done
     moreover
     guess b0 b1 by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)])
@@ -1438,7 +1489,9 @@
     have a': "a' = b1"
       apply (rule ksimplex_fix_plane_0[OF goal1(2) assms(4), of b0])
       unfolding goal1(3)
-      using assms extb goal1 apply auto done
+      using assms extb goal1
+      apply auto
+      done
     moreover
     have "b0 = a0"
       unfolding kle_antisym[symmetric, of b0 a0 n]
@@ -1454,7 +1507,8 @@
     show "s' = s"
       apply -
       apply (rule *[of _ a1 b1])
-      using exta(1-2) extb(1-2) goal1 apply auto
+      using exta(1-2) extb(1-2) goal1
+      apply auto
       done
   qed
   show ?thesis
@@ -1465,7 +1519,8 @@
     defer
     apply (erule conjE bexE)+
     apply (rule_tac a'=b in **)
-    using assms(1,2) apply auto
+    using assms(1,2)
+    apply auto
     done
 qed
 
@@ -3140,11 +3195,13 @@
         using i label(1)[of i y] by auto
       show "x \<bullet> i \<le> f x \<bullet> i"
         apply (rule label(4)[rule_format])
-        using xy lx i(2) apply auto
+        using xy lx i(2)
+        apply auto
         done
       show "f y \<bullet> i \<le> y \<bullet> i"
         apply (rule label(5)[rule_format])
-        using xy ly i(2) apply auto
+        using xy ly i(2)
+        apply auto
         done
     next
       assume "label x i \<noteq> 0"
@@ -3152,11 +3209,13 @@
         using i label(1)[of i x] label(1)[of i y] by auto
       show "f x \<bullet> i \<le> x \<bullet> i"
         apply (rule label(5)[rule_format])
-        using xy l i(2) apply auto
+        using xy l i(2)
+        apply auto
         done
       show "y \<bullet> i \<le> f y \<bullet> i"
         apply (rule label(4)[rule_format])
-        using xy l i(2) apply auto
+        using xy l i(2)
+        apply auto
         done
     qed
     also have "\<dots> \<le> norm (f y - f x) + norm (y - x)"
@@ -3206,21 +3265,25 @@
           unfolding norm_minus_commute by auto
         also have "\<dots> < e / 2 + e / 2"
           apply (rule add_strict_mono)
-          using as(4,5) apply auto
+          using as(4,5)
+          apply auto
           done
         finally show "norm (f y - f x) < d / real n / 8"
           apply -
           apply (rule e(2))
-          using as apply auto
+          using as
+          apply auto
           done
         have "norm (y - z) + norm (x - z) < d / real n / 8 + d / real n / 8"
           apply (rule add_strict_mono)
-          using as apply auto
+          using as
+          apply auto
           done
         thus "norm (y - x) < 2 * (d / real n / 8)" using tria by auto
         show "norm (f x - f z) < d / real n / 8"
           apply (rule e(2))
-          using as e(1) apply auto
+          using as e(1)
+          apply auto
           done
       qed (insert as, auto)
     qed
@@ -3231,9 +3294,10 @@
     apply (rule add_pos_pos)
     defer
     apply (rule divide_pos_pos)
-    using e(1) n apply auto
+    using e(1) n
+    apply auto
     done
-  hence "p > 0" using p by auto
+  then have "p > 0" using p by auto
 
   obtain b :: "nat \<Rightarrow> 'a" where b: "bij_betw b {1..n} Basis"
     by atomize_elim (auto simp: n_def intro!: finite_same_card_bij)
@@ -3316,7 +3380,8 @@
   have "\<And>i. i \<in> Basis \<Longrightarrow> r (b' i) \<le> p"
     apply (rule order_trans)
     apply (rule rs(1)[OF b'_im,THEN conjunct2])
-    using q(1)[rule_format,OF b'_im] apply (auto simp add: Suc_le_eq)
+    using q(1)[rule_format,OF b'_im]
+    apply (auto simp add: Suc_le_eq)
     done
   hence "r' \<in> {0..\<Sum>Basis}"
     unfolding r'_def mem_interval using b'_Basis
@@ -3325,7 +3390,8 @@
   have "\<And>i. i\<in>Basis \<Longrightarrow> s (b' i) \<le> p"
     apply (rule order_trans)
     apply (rule rs(2)[OF b'_im, THEN conjunct2])
-    using q(1)[rule_format,OF b'_im] apply (auto simp add: Suc_le_eq)
+    using q(1)[rule_format,OF b'_im]
+    apply (auto simp add: Suc_le_eq)
     done
   hence "s' \<in> {0..\<Sum>Basis}"
     unfolding s'_def mem_interval using b'_Basis
@@ -3336,7 +3402,8 @@
   have *: "\<And>x. 1 + real x = real (Suc x)" by auto
   { have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
       apply (rule setsum_mono)
-      using rs(1)[OF b'_im] apply (auto simp add:* field_simps)
+      using rs(1)[OF b'_im]
+      apply (auto simp add:* field_simps)
       done
     also have "\<dots> < e * real p" using p `e>0` `p>0`
       by (auto simp add: field_simps n_def real_of_nat_def)
@@ -3345,7 +3412,8 @@
   moreover
   { have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
       apply (rule setsum_mono)
-      using rs(2)[OF b'_im] apply (auto simp add:* field_simps)
+      using rs(2)[OF b'_im]
+      apply (auto simp add:* field_simps)
       done
     also have "\<dots> < e * real p" using p `e > 0` `p > 0`
       by (auto simp add: field_simps n_def real_of_nat_def)
@@ -3467,7 +3535,8 @@
     defer
     apply (erule bexE)
     apply (rule_tac x=y in that)
-    using assms apply auto
+    using assms
+    apply auto
     done
 qed
 
@@ -3599,7 +3668,8 @@
   have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)"
     apply (rule mult_right_mono)
     unfolding divide_le_eq_1
-    using * x apply auto
+    using * x
+    apply auto
     done
   thus "u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i"
     using * by auto