author wenzelm Wed, 28 Aug 2013 22:50:23 +0200 changeset 53252 4766fbe322b5 parent 53251 7facc08da806 child 53253 220f306f5c4e
tuned proofs;
```--- 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```