# HG changeset patch
# User wenzelm
# Date 1379455875 -7200
# Node ID 63892cfef47ff91901500f09d6f7ece5c0288feb
# Parent  4b9894aad6052812fb039faa376ebd3d5b581e2f
tuned proofs;

diff -r 4b9894aad605 -r 63892cfef47f src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Sep 17 21:20:55 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Sep 18 00:11:15 2013 +0200
@@ -43,11 +43,12 @@
   fixes f :: "'a::metric_space \<Rightarrow> 'b::euclidean_space"
   assumes "compact s"
     and "continuous_on s f"
-    and "\<not> (\<exists>x\<in>s. (f x = 0))"
+    and "\<not> (\<exists>x\<in>s. f x = 0)"
   obtains d where "0 < d" and "\<forall>x\<in>s. d \<le> norm (f x)"
 proof (cases "s = {}")
   case True
-  show thesis by (rule that [of 1]) (auto simp: True)
+  show thesis
+    by (rule that [of 1]) (auto simp: True)
 next
   case False
   have "continuous_on s (norm \<circ> f)"
@@ -89,14 +90,14 @@
         (P x \<and> Q xa \<and> y = 0 \<longrightarrow> x \<bullet> xa \<le> f x \<bullet> xa) \<and>
         (P x \<and> Q xa \<and> y = 1 \<longrightarrow> f x \<bullet> xa \<le> x \<bullet> xa)"
     {
-      assume "P x" "Q xa" "xa\<in>Basis"
+      assume "P x" "Q xa" "xa \<in> Basis"
       then have "0 \<le> f x \<bullet> xa \<and> f x \<bullet> xa \<le> 1"
         using assms(2)[rule_format,of "f x" xa]
         apply (drule_tac assms(1)[rule_format])
         apply auto
         done
     }
-    then have "xa\<in>Basis \<Longrightarrow> ?R 0 \<or> ?R 1" by auto
+    then have "xa \<in> Basis \<Longrightarrow> ?R 0 \<or> ?R 1" by auto
     then show ?case by auto
   qed
 qed
@@ -105,32 +106,34 @@
 subsection {* The key "counting" observation, somewhat abstracted. *}
 
 lemma setsum_Un_disjoint':
-  assumes "finite A" "finite B" "A \<inter> B = {}" "A \<union> B = C"
+  assumes "finite A"
+    and "finite B"
+    and "A \<inter> B = {}"
+    and "A \<union> B = C"
   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>
+  assumes "finite faces"
+    and "finite simplices"
+    and "\<forall>f\<in>faces. bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 1)"
+    and "\<forall>f\<in>faces. \<not> bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 2)"
+    and "\<forall>s\<in>simplices. compo s \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 1)"
+    and "\<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})"
+    and "odd(card {f \<in> faces. compo' f \<and> bnd f})"
   shows "odd(card {s \<in> simplices. compo s})"
 proof -
   have "\<And>x. {f\<in>faces. compo' f \<and> bnd f \<and> face f x} \<union> {f\<in>faces. compo' f \<and> \<not>bnd f \<and> face f x} =
       {f\<in>faces. compo' f \<and> face f x}"
     "\<And>x. {f \<in> faces. compo' f \<and> bnd f \<and> face f x} \<inter> {f \<in> faces. compo' f \<and> \<not> bnd f \<and> face f x} = {}"
     by auto
-  then have lem1:"setsum (\<lambda>s. (card {f \<in> faces. face f s \<and> compo' f})) simplices =
+  then have lem1: "setsum (\<lambda>s. (card {f \<in> faces. face f s \<and> compo' f})) simplices =
       setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f s}) simplices +
       setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> \<not> (bnd f)}. face f s}) simplices"
     unfolding setsum_addf[symmetric]
     apply -
-    apply(rule setsum_cong2)
+    apply (rule setsum_cong2)
     using assms(1)
     apply (auto simp add: card_Un_Int, auto simp add:conj_commute)
     done
@@ -139,7 +142,7 @@
       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)
+    apply (rule_tac[!] setsum_multicount)
     using assms
     apply auto
     done
@@ -207,10 +210,11 @@
     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)))"
+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))"
 proof
   assume "card s = 2"
-  then obtain x y where s: "s = {x, y}" "x\<noteq>y" unfolding numeral_2_eq_2
+  then obtain x y where s: "s = {x, y}" "x \<noteq> y"
+    unfolding numeral_2_eq_2
     apply -
     apply (erule exE conjE | drule card_eq_SucD)+
     apply auto
@@ -219,10 +223,12 @@
     using s by auto
 next
   assume "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)"
-  then obtain x y where "x\<in>s" "y\<in>s" "x \<noteq> y" "\<forall>z\<in>s. z = x \<or> z = y"
+  then obtain x y where "x \<in> s" "y \<in> s" "x \<noteq> y" "\<forall>z\<in>s. z = x \<or> z = y"
     by auto
-  then have "s = {x, y}" by auto
-  with `x \<noteq> y` show "card s = 2" by auto
+  then have "s = {x, y}"
+    by auto
+  with `x \<noteq> y` show "card s = 2"
+    by auto
 qed
 
 lemma image_lemma_0:
@@ -244,19 +250,26 @@
 qed
 
 lemma image_lemma_1:
-  assumes "finite s" "finite t" "card s = card t" "f ` s = t" "b \<in> t"
+  assumes "finite s"
+    and "finite t"
+    and "card s = card t"
+    and "f ` s = t"
+    and "b \<in> t"
   shows "card {s'. \<exists>a\<in>s. s' = s - {a} \<and>  f ` s' = t - {b}} = 1"
 proof -
-  obtain a where a: "b = f a" "a\<in>s" using assms(4-5) by auto
+  obtain a where a: "b = f a" "a \<in> s"
+    using assms(4-5) by auto
   have inj: "inj_on f s"
     apply (rule eq_card_imp_inj_on)
-    using assms(1-4) apply auto
+    using assms(1-4)
+    apply auto
     done
   have *: "{a \<in> s. f ` (s - {a}) = t - {b}} = {a}"
     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]
+    unfolding a
+    using a(2) and assms and inj[unfolded inj_on_def]
     apply auto
     done
   show ?thesis
@@ -268,8 +281,8 @@
 
 lemma image_lemma_2:
   assumes "finite s" "finite t" "card s = card t" "f ` s \<subseteq> t" "f ` s \<noteq> t" "b \<in> t"
-  shows "(card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 0) \<or>
-         (card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 2)"
+  shows "card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 0 \<or>
+         card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 2"
 proof (cases "{a\<in>s. f ` (s - {a}) = t - {b}} = {}")
   case True
   then show ?thesis
@@ -281,36 +294,55 @@
 next
   let ?M = "{a\<in>s. f ` (s - {a}) = t - {b}}"
   case False
-  then obtain a where "a\<in>?M" by auto
-  then have a: "a\<in>s" "f ` (s - {a}) = t - {b}" by auto
-  have "f a \<in> t - {b}" using a and assms by auto
+  then obtain a where "a \<in> ?M"
+    by auto
+  then have a: "a \<in> s" "f ` (s - {a}) = t - {b}"
+    by auto
+  have "f a \<in> t - {b}"
+    using a and assms by auto
   then have "\<exists>c \<in> s - {a}. f a = f c"
-    unfolding image_iff[symmetric] and a by auto
-  then obtain c where c: "c \<in> s" "a \<noteq> c" "f a = f c" by auto
+    unfolding image_iff[symmetric] and a
+    by auto
+  then obtain c where c: "c \<in> s" "a \<noteq> c" "f a = f c"
+    by auto
   then have *: "f ` (s - {c}) = f ` (s - {a})"
     apply -
-    apply (rule set_eqI, rule)
+    apply (rule set_eqI)
+    apply rule
   proof -
     fix x
     assume "x \<in> f ` (s - {a})"
-    then obtain y where y: "f y = x" "y\<in>s- {a}" by auto
+    then obtain y where y: "f y = x" "y \<in> s - {a}"
+      by auto
     then show "x \<in> f ` (s - {c})"
       unfolding image_iff
       apply (rule_tac x = "if y = c then a else y" in bexI)
-      using c a apply auto done
+      using c a
+      apply auto
+      done
   qed auto
-  have "c\<in>?M"
+  have "c \<in> ?M"
     unfolding mem_Collect_eq and *
-    using a and c(1) by auto
+    using a and c(1)
+    by auto
   show ?thesis
-    apply (rule disjI2, rule image_lemma_0) unfolding card_2_exists
-    apply (rule bexI[OF _ `a\<in>?M`], rule bexI[OF _ `c\<in>?M`], rule, rule `a\<noteq>c`)
-  proof (rule, unfold mem_Collect_eq, erule conjE)
+    apply (rule disjI2)
+    apply (rule image_lemma_0)
+    unfolding card_2_exists
+    apply (rule bexI[OF _ `a\<in>?M`])
+    apply (rule bexI[OF _ `c\<in>?M`])
+    apply rule
+    apply (rule `a \<noteq> c`)
+    apply rule
+    apply (unfold mem_Collect_eq)
+    apply (erule conjE)
+  proof -
     fix z
     assume as: "z \<in> s" "f ` (s - {z}) = t - {b}"
     have inj: "inj_on f (s - {z})"
       apply (rule eq_card_imp_inj_on)
-      unfolding as using as(1) and assms
+      unfolding as
+      using as(1) and assms
       apply auto
       done
     show "z = a \<or> z = c"
@@ -318,7 +350,7 @@
       assume "\<not> ?thesis"
       then show False
         using inj[unfolded inj_on_def, THEN bspec[where x=a], THEN bspec[where x=c]]
-        using `a\<in>s` `c\<in>s` `f a = f c` `a\<noteq>c`
+        using `a \<in> s` `c \<in> s` `f a = f c` `a \<noteq> c`
         apply auto
         done
     qed
@@ -330,18 +362,20 @@
 
 lemma kuhn_complete_lemma:
   assumes "finite simplices"
-    "\<forall>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s - {a})"
-    "\<forall>s\<in>simplices. card s = n + 2" "\<forall>s\<in>simplices. (rl ` s) \<subseteq> {0..n+1}"
-    "\<forall>f\<in> {f. \<exists>s\<in>simplices. face f s}. bnd f  \<longrightarrow> (card {s\<in>simplices. face f s} = 1)"
-    "\<forall>f\<in> {f. \<exists>s\<in>simplices. face f s}. \<not>bnd f \<longrightarrow> (card {s\<in>simplices. face f s} = 2)"
-    "odd(card {f\<in>{f. \<exists>s\<in>simplices. face f s}. rl ` f = {0..n} \<and> bnd f})"
+    and "\<forall>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s - {a})"
+    and "\<forall>s\<in>simplices. card s = n + 2"
+    and "\<forall>s\<in>simplices. (rl ` s) \<subseteq> {0..n+1}"
+    and "\<forall>f\<in>{f. \<exists>s\<in>simplices. face f s}. bnd f  \<longrightarrow> card {s\<in>simplices. face f s} = 1"
+    and "\<forall>f\<in>{f. \<exists>s\<in>simplices. face f s}. \<not> bnd f \<longrightarrow> card {s\<in>simplices. face f s} = 2"
+    and "odd (card {f\<in>{f. \<exists>s\<in>simplices. face f s}. rl ` f = {0..n} \<and> bnd f})"
   shows "odd (card {s\<in>simplices. (rl ` s = {0..n+1})})"
   apply (rule kuhn_counting_lemma)
   defer
   apply (rule assms)+
   prefer 3
   apply (rule assms)
-proof (rule_tac[1-2] ballI impI)+
+  apply (rule_tac[1-2] ballI impI)+
+proof -
   have *: "{f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s - {a}} = (\<Union>s\<in>simplices. {f. \<exists>a\<in>s. (f = s - {a})})"
     by auto
   have **: "\<forall>s\<in>simplices. card s = n + 2 \<and> finite s"
@@ -353,10 +387,13 @@
     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
-  fix s assume s: "s\<in>simplices"
+    (\<exists>a\<in>s. (f = s - {a})) \<and> P f \<longleftrightarrow> (\<exists>a\<in>s. (f = s - {a}) \<and> P f)"
+    by auto
+  fix s
+  assume s: "s \<in> simplices"
   let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {0..n}}"
-  have "{0..n + 1} - {n + 1} = {0..n}" by auto
+  have "{0..n + 1} - {n + 1} = {0..n}"
+    by auto
   then have S: "?S = {s'. \<exists>a\<in>s. s' = s - {a} \<and> rl ` s' = {0..n + 1} - {n + 1}}"
     apply -
     apply (rule set_eqI)
@@ -364,9 +401,9 @@
     unfolding *[OF s, unfolded mem_Collect_eq, where P="\<lambda>x. rl ` x = {0..n}"]
     apply auto
     done
-  show "rl ` s = {0..n+1} \<Longrightarrow> card ?S = 1" "rl ` s \<noteq> {0..n+1} \<Longrightarrow> card ?S = 0 \<or> card ?S = 2"
+  show "rl ` s = {0..n+1} \<Longrightarrow> card ?S = 1" and "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)
+    apply (rule_tac[!] image_lemma_1 image_lemma_2)
     using ** assms(4) and s
     apply auto
     done
@@ -375,12 +412,12 @@
 
 subsection {*We use the following notion of ordering rather than pointwise indexing. *}
 
-definition "kle n x y \<longleftrightarrow> (\<exists>k\<subseteq>{1..n::nat}. (\<forall>j. y(j) = x(j) + (if j \<in> k then (1::nat) else 0)))"
+definition "kle n x y \<longleftrightarrow> (\<exists>k\<subseteq>{1..n::nat}. \<forall>j. y j = x j + (if j \<in> k then (1::nat) else 0))"
 
 lemma kle_refl [intro]: "kle n x x"
   unfolding kle_def by auto
 
-lemma kle_antisym: "kle n x y \<and> kle n y x \<longleftrightarrow> (x = y)"
+lemma kle_antisym: "kle n x y \<and> kle n y x \<longleftrightarrow> x = y"
   unfolding kle_def
   apply rule
   apply auto
@@ -388,12 +425,17 @@
 
 lemma pointwise_minimal_pointwise_maximal:
   fixes s :: "(nat \<Rightarrow> nat) set"
-  assumes "finite s" "s \<noteq> {}" "\<forall>x\<in>s. \<forall>y\<in>s. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)"
-  shows "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j" "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. x j \<le> a j"
-  using assms unfolding atomize_conj
+  assumes "finite s"
+    and "s \<noteq> {}"
+    and "\<forall>x\<in>s. \<forall>y\<in>s. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)"
+  shows "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j"
+    and "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. x j \<le> a j"
+  using assms
+  unfolding atomize_conj
 proof (induct s rule: finite_induct)
-  fix x and F::"(nat\<Rightarrow>nat) set"
-  assume as:"finite F" "x \<notin> F"
+  fix x
+  fix F :: "(nat \<Rightarrow> nat) set"
+  assume as: "finite F" "x \<notin> F"
     "\<lbrakk>F \<noteq> {}; \<forall>x\<in>F. \<forall>y\<in>F. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)\<rbrakk>
         \<Longrightarrow> (\<exists>a\<in>F. \<forall>x\<in>F. \<forall>j. a j \<le> x j) \<and> (\<exists>a\<in>F. \<forall>x\<in>F. \<forall>j. x j \<le> a j)" "insert x F \<noteq> {}"
     "\<forall>xa\<in>insert x F. \<forall>y\<in>insert x F. (\<forall>j. xa j \<le> y j) \<or> (\<forall>j. y j \<le> xa j)"
@@ -417,7 +459,8 @@
       assume "\<forall>j. a j \<le> x j"
       then show ?thesis
         apply (rule_tac x=a in bexI)
-        using a apply auto
+        using a
+        apply auto
         done
     next
       assume "\<forall>j. x j \<le> a j"
@@ -456,24 +499,28 @@
 qed auto
 
 
-lemma kle_imp_pointwise: "kle n x y \<Longrightarrow> (\<forall>j. x j \<le> y j)"
+lemma kle_imp_pointwise: "kle n x y \<Longrightarrow> \<forall>j. x j \<le> y j"
   unfolding kle_def by auto
 
 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"
-  apply (rule, rule ext, erule conjE)
+  apply rule
+  apply (rule ext)
+  apply (erule conjE)
   apply (erule_tac x = xa in allE)+
   apply auto
   done
 
 lemma kle_trans:
-  assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x"
+  assumes "kle n x y"
+    and "kle n y z"
+    and "kle n x z \<or> kle n z x"
   shows "kle n x z"
   using assms
-    apply -
-    apply (erule disjE)
-    apply assumption
+  apply -
+  apply (erule disjE)
+  apply assumption
 proof -
   case goal1
   then have "x = z"
@@ -487,20 +534,24 @@
 qed
 
 lemma kle_strict:
-  assumes "kle n x y" "x \<noteq> y"
-  shows "\<forall>j. x j \<le> y j"  "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x(k) < y(k)"
+  assumes "kle n x y"
+    and "x \<noteq> y"
+  shows "\<forall>j. x j \<le> y j"
+    and "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x k < y k"
   apply (rule kle_imp_pointwise[OF assms(1)])
 proof -
   guess k using assms(1)[unfolded kle_def] .. note k = this
-  show "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x(k) < y(k)"
+  show "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x k < y k"
 proof (cases "k = {}")
   case True
   then have "x = y"
     apply -
     apply (rule ext)
-    using k apply auto
+    using k
+    apply auto
     done
-  then show ?thesis using assms(2) by auto
+  then show ?thesis
+    using assms(2) by auto
 next
   case False
   then have "(SOME k'. k' \<in> k) \<in> k"
@@ -510,19 +561,24 @@
     done
   then show ?thesis
     apply (rule_tac x = "SOME k'. k' \<in> k" in exI)
-    using k apply auto
+    using k
+    apply auto
     done
   qed
 qed
 
 lemma kle_minimal:
-  assumes "finite s" "s \<noteq> {}" "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
+  assumes "finite s"
+    and "s \<noteq> {}"
+    and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
   shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n a x"
 proof -
   have "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j"
     apply (rule pointwise_minimal_pointwise_maximal(1)[OF assms(1-2)])
-    apply (rule, rule)
-    apply (drule_tac assms(3)[rule_format], assumption)
+    apply rule
+    apply rule
+    apply (drule_tac assms(3)[rule_format])
+    apply assumption
     using kle_imp_pointwise
     apply auto
     done
@@ -550,14 +606,18 @@
 qed
 
 lemma kle_maximal:
-  assumes "finite s" "s \<noteq> {}" "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
+  assumes "finite s"
+    and "s \<noteq> {}"
+    and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
   shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n x a"
 proof -
   have "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<ge> x j"
     apply (rule pointwise_minimal_pointwise_maximal(2)[OF assms(1-2)])
-    apply (rule, rule)
+    apply rule
+    apply 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 
@@ -574,15 +634,18 @@
         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
-      then show ?thesis using kle_refl by auto
+      then show ?thesis
+        using kle_refl by auto
     qed
   qed (insert a, auto)
 qed
 
 lemma kle_strict_set:
-  assumes "kle n x y" "x \<noteq> y"
+  assumes "kle n x y"
+    and "x \<noteq> y"
   shows "1 \<le> card {k\<in>{1..n}. x k < y k}"
 proof -
   guess i using kle_strict(2)[OF assms] ..
@@ -591,15 +654,19 @@
     apply (rule card_mono)
     apply auto
     done
-  then show ?thesis by auto
+  then show ?thesis
+    by auto
 qed
 
 lemma kle_range_combine:
-  assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x"
-    "m1 \<le> card {k\<in>{1..n}. x k < y k}"
-    "m2 \<le> card {k\<in>{1..n}. y k < z k}"
+  assumes "kle n x y"
+    and "kle n y z"
+    and "kle n x z \<or> kle n z x"
+    and "m1 \<le> card {k\<in>{1..n}. x k < y k}"
+    and "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
+  apply (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)
@@ -617,37 +684,55 @@
     by auto
   have **: "{k \<in> {1..n}. x k < y k} \<inter> {k \<in> {1..n}. y k < z k} = {}"
     unfolding disjoint_iff_not_equal
-    apply (rule, rule, unfold mem_Collect_eq, rule ccontr)
+    apply rule
+    apply rule
+    apply (unfold mem_Collect_eq)
+    apply (rule notI)
     apply (erule conjE)+
   proof -
     fix i j
-    assume as: "i \<in> {1..n}" "x i < y i" "j \<in> {1..n}" "y j < z j" "\<not> i \<noteq> j"
+    assume as: "i \<in> {1..n}" "x i < y i" "j \<in> {1..n}" "y j < z j" "i = j"
     guess kx using assms(1)[unfolded kle_def] .. note kx = this
-    have "x i < y i" using as by auto
-    then have "i \<in> kx" using as(1) kx
-      apply (rule_tac ccontr)
+    have "x i < y i"
+      using as by auto
+    then have "i \<in> kx"
+      using as(1) kx
+      apply -
+      apply (rule ccontr)
       apply auto
       done
-    then have "x i + 1 = y i" using kx by auto
+    then have "x i + 1 = y i"
+      using kx by auto
     moreover
     guess ky using assms(2)[unfolded kle_def] .. note ky = this
-    have "y i < z i" using as by auto
-    then have "i \<in> ky" using as(1) ky
-      apply (rule_tac ccontr)
+    have "y i < z i"
+      using as by auto
+    then have "i \<in> ky"
+      using as(1) ky
+      apply -
+      apply (rule ccontr)
       apply auto
       done
-    then have "y i + 1 = z i" using ky by auto
+    then have "y i + 1 = z i"
+      using ky by auto
     ultimately
-    have "z i = x i + 2" by auto
-    then show False using assms(3) unfolding kle_def
+    have "z i = x i + 2"
+      by auto
+    then show False
+      using assms(3)
+      unfolding kle_def
       by (auto simp add: split_if_eq1)
   qed
-  have fin: "\<And>P. finite {x\<in>{1..n::nat}. P x}" by auto
+  have fin: "\<And>P. finite {x\<in>{1..n::nat}. P x}"
+    by auto
   have "m1 + m2 \<le> card {k\<in>{1..n}. x k < y k} + card {k\<in>{1..n}. y k < z k}"
     using assms(4-5) by auto
   also have "\<dots> \<le> card {k\<in>{1..n}. x k < z k}"
-    unfolding card_Un_Int[OF fin fin] unfolding * ** by auto
-  finally show " m1 + m2 \<le> card {k \<in> {1..n}. x k < z k}" by auto
+    unfolding card_Un_Int[OF fin fin]
+    unfolding * **
+    by auto
+  finally show "m1 + m2 \<le> card {k \<in> {1..n}. x k < z k}"
+    by auto
 qed
 
 lemma kle_range_combine_l:
@@ -670,12 +755,15 @@
     and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
   shows "\<exists>x\<in>s. \<exists>y\<in>s. kle n x y \<and> m \<le> card {k\<in>{1..n}. x k < y k}"
 proof -
-  have "finite s" "s\<noteq>{}" using assms(1)
+  have "finite s" and "s \<noteq> {}"
+    using assms(1)
     by (auto intro: card_ge_0_finite)
-  then show ?thesis using assms
+  then show ?thesis
+    using assms
   proof (induct m arbitrary: s)
     case 0
-    then show ?case using kle_refl by auto
+    then show ?case
+      using kle_refl by auto
   next
     case (Suc m)
     then obtain a where a: "a \<in> s" "\<forall>x\<in>s. kle n a x"
@@ -683,29 +771,40 @@
     show ?case
     proof (cases "s \<subseteq> {a}")
       case False
-      then have "card (s - {a}) = Suc m" "s - {a} \<noteq> {}"
-        using card_Diff_singleton[OF _ a(1)] Suc(4) `finite s` by auto
-      then obtain x b where xb:"x\<in>s - {a}" "b\<in>s - {a}"
-        "kle n x b" "m \<le> card {k \<in> {1..n}. x k < b k}"
-        using Suc(1)[of "s - {a}"] using Suc(5) `finite s` by auto
-      have "1 \<le> card {k \<in> {1..n}. a k < x k}" "m \<le> card {k \<in> {1..n}. x k < b k}"
+      then have "card (s - {a}) = Suc m" and "s - {a} \<noteq> {}"
+        using card_Diff_singleton[OF _ a(1)] Suc(4) `finite s`
+        by auto
+      then obtain x b where xb:
+        "x \<in> s - {a}"
+        "b \<in> s - {a}"
+        "kle n x b"
+        "m \<le> card {k \<in> {1..n}. x k < b k}"
+        using Suc(1)[of "s - {a}"]
+        using Suc(5) `finite s`
+        by auto
+      have "1 \<le> card {k \<in> {1..n}. a k < x k}" and "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
         done
       then show ?thesis
-        apply (rule_tac x=a in bexI, rule_tac x=b in bexI)
+        apply (rule_tac x=a in bexI)
+        apply (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
         done
     next
       case True
-      then have "s = {a}" using Suc(3) by auto
-      then have "card s = 1" by auto
-      then have False using Suc(4) `finite s` by auto
-      then show ?thesis by auto
+      then have "s = {a}"
+        using Suc(3) by auto
+      then have "card s = 1"
+        by auto
+      then have False
+        using Suc(4) `finite s` by auto
+      then show ?thesis
+        by auto
     qed
   qed
 qed
@@ -719,11 +818,14 @@
 
 lemma kle_trans_1:
   assumes "kle n x y"
-  shows "x j \<le> y j" "y j \<le> x j + 1"
+  shows "x j \<le> y j"
+    and "y j \<le> x j + 1"
   using assms[unfolded kle_def] by auto
 
 lemma kle_trans_2:
-  assumes "kle n a b" "kle n b c" "\<forall>j. c j \<le> a j + 1"
+  assumes "kle n a b"
+    and "kle n b c"
+    and "\<forall>j. c j \<le> a j + 1"
   shows "kle n a c"
 proof -
   guess kk1 using assms(1)[unfolded kle_def] .. note kk1 = this
@@ -747,17 +849,22 @@
       ultimately show ?thesis by auto
     next
       case False
-      then show ?thesis using kk1 kk2 by auto
+      then show ?thesis
+        using kk1 kk2 by auto
     qed
   qed (insert kk1 kk2, auto)
 qed
 
 lemma kle_between_r:
-  assumes "kle n a b" "kle n b c" "kle n a x" "kle n c x"
+  assumes "kle n a b"
+    and "kle n b c"
+    and "kle n a x"
+    and "kle n c x"
   shows "kle n b x"
   apply (rule kle_trans_2[OF assms(2,4)])
 proof
-  have *: "\<And>c b x::nat. x \<le> c + 1 \<Longrightarrow> c \<le> b \<Longrightarrow> x \<le> b + 1" by auto
+  have *: "\<And>c b x::nat. x \<le> c + 1 \<Longrightarrow> c \<le> b \<Longrightarrow> x \<le> b + 1"
+    by auto
   fix j
   show "x j \<le> b j + 1"
     apply (rule *)
@@ -767,7 +874,10 @@
 qed
 
 lemma kle_between_l:
-  assumes "kle n a b" "kle n b c" "kle n x a" "kle n x c"
+  assumes "kle n a b"
+    and "kle n b c"
+    and "kle n x a"
+    and "kle n x c"
   shows "kle n x b"
   apply (rule kle_trans_2[OF assms(3,1)])
 proof
@@ -782,7 +892,9 @@
 qed
 
 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"
+  assumes "\<forall>j. b j = (if j = k then a(j) + 1 else a j)"
+    and "kle n a x"
+    and "kle n x b"
   shows "x = a \<or> x = b"
 proof (cases "x k = a k")
   case True
@@ -791,7 +903,8 @@
     apply (rule ext)
   proof -
     fix j
-    have "x j \<le> a j" using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
+    have "x j \<le> a j"
+      using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
       unfolding assms(1)[rule_format]
       apply -
       apply(cases "j = k")
@@ -799,19 +912,24 @@
       apply auto
       done
     then show "x j = a j"
-      using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]] by auto
+      using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]]
+      by auto
   qed
 next
   case False
-  show ?thesis apply(rule disjI2,rule ext)
+  show ?thesis
+    apply (rule disjI2)
+    apply (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")
-      using False by auto
+      apply (cases "j = k")
+      using False
+      apply auto
+      done
     then show "x j = b j"
       using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
     by auto
@@ -819,7 +937,7 @@
 qed
 
 
-subsection {* kuhn's notion of a simplex (a reformulation to avoid so much indexing). *}
+subsection {* Kuhn's notion of a simplex (a reformulation to avoid so much indexing) *}
 
 definition "ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow>
   card s = n + 1 \<and>
@@ -837,35 +955,47 @@
 
 lemma ksimplex_eq:
   "ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow>
-    (card s = n + 1 \<and> finite s \<and>
+    card s = n + 1 \<and>
+    finite s \<and>
     (\<forall>x\<in>s. \<forall>j. x(j) \<le> p) \<and>
-    (\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> (x j = p)) \<and>
-    (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x))"
+    (\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> x j = p) \<and>
+    (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x)"
   unfolding ksimplex_def by (auto intro: card_ge_0_finite)
 
 lemma ksimplex_extrema:
   assumes "ksimplex p n s"
-  obtains a b where "a \<in> s" "b \<in> s"
-    "\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {1..n} then a(i) + 1 else a(i))"
+  obtains a b where "a \<in> s"
+    and "b \<in> s"
+    and "\<forall>x\<in>s. kle n a x \<and> kle n x b"
+    and "\<forall>i. b i = (if i \<in> {1..n} then a i + 1 else a i)"
 proof (cases "n = 0")
   case True
   obtain x where *: "s = {x}"
     using assms[unfolded ksimplex_eq True,THEN conjunct1]
-    unfolding add_0_left card_1_exists by auto
+    unfolding add_0_left card_1_exists
+    by auto
   show ?thesis
-    apply (rule that[of x x]) unfolding * True
+    apply (rule that[of x x])
+    unfolding * True
     apply auto
     done
 next
   note assm = assms[unfolded ksimplex_eq]
   case False
-  have "s\<noteq>{}" using assm by auto
+  have "s \<noteq> {}"
+    using assm by auto
   obtain a where a: "a \<in> s" "\<forall>x\<in>s. kle n a x"
-    using `s\<noteq>{}` assm using kle_minimal[of s n] by auto
+    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
+    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}"
-    using kle_range_induct[of s n n] using assm by auto
+    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
@@ -889,27 +1019,36 @@
   show ?thesis
     apply (rule that[OF a(1) b(1)])
     defer
-    apply (subst *[symmetric]) unfolding mem_Collect_eq
+    apply (subst *[symmetric])
+    unfolding mem_Collect_eq
   proof
     guess k using a(2)[rule_format,OF b(1),unfolded kle_def] .. note k = this
     fix i
     show "b i = (if i \<in> {1..n} \<and> a i < b i then a i + 1 else a i)"
     proof (cases "i \<in> {1..n}")
       case True
-      then show ?thesis unfolding k[THEN conjunct2,rule_format] by auto
+      then show ?thesis
+        unfolding k[THEN conjunct2,rule_format] by auto
     next
       case False
-      have "a i = p" using assm and False `a\<in>s` by auto
-      moreover have "b i = p" using assm and False `b\<in>s` by auto
-      ultimately show ?thesis by auto
+      have "a i = p"
+        using assm and False `a\<in>s` by auto
+      moreover have "b i = p"
+        using assm and False `b\<in>s` by auto
+      ultimately show ?thesis
+        by auto
     qed
-  qed(insert a(2) b(2) assm, auto)
+  qed (insert a(2) b(2) assm, auto)
 qed
 
 lemma ksimplex_extrema_strong:
-  assumes "ksimplex p n s" "n \<noteq> 0"
-  obtains a b where "a \<in> s" "b \<in> s" "a \<noteq> b"
-    "\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {1..n} then a(i) + 1 else a(i))"
+  assumes "ksimplex p n s"
+    and "n \<noteq> 0"
+  obtains a b where "a \<in> s"
+    and "b \<in> s"
+    and "a \<noteq> b"
+    and "\<forall>x\<in>s. kle n a x \<and> kle n x b"
+    and "\<forall>i. b i = (if i \<in> {1..n} then a(i) + 1 else a i)"
 proof -
   obtain a b where ab: "a \<in> s" "b \<in> s"
     "\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {1..n} then a(i) + 1 else a(i))"
@@ -919,37 +1058,44 @@
   have "a \<noteq> b"
     apply (rule notI)
     apply (drule cong[of _ _ 1 1])
-    using ab(4) assms(2) apply auto
+    using ab(4) assms(2)
+    apply auto
     done
   then show ?thesis
     apply (rule_tac that[of a b])
-    using ab apply auto
+    using ab
+    apply auto
     done
 qed
 
 lemma ksimplexD:
   assumes "ksimplex p n s"
-  shows "card s = n + 1" "finite s" "card s = n + 1"
-    "\<forall>x\<in>s. \<forall>j. x j \<le> p" "\<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
-    "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
+  shows "card s = n + 1"
+    and "finite s"
+    and "card s = n + 1"
+    and "\<forall>x\<in>s. \<forall>j. x j \<le> p"
+    and "\<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
+    and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
   using assms unfolding ksimplex_eq by auto
 
 lemma ksimplex_successor:
-  assumes "ksimplex p n s" "a \<in> s"
-  shows "(\<forall>x\<in>s. kle n x a) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y(j) = (if j = k then a(j) + 1 else a(j)))"
+  assumes "ksimplex p n s"
+    and "a \<in> s"
+  shows "(\<forall>x\<in>s. kle n x a) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a j + 1 else a j))"
 proof (cases "\<forall>x\<in>s. kle n x a")
   case True
   then show ?thesis by auto
 next
   note assm = ksimplexD[OF assms(1)]
   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
+  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
   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)
+    apply (auto simp add: kle_refl)
     done
 
   let ?kle1 = "{x \<in> s. \<not> kle n x a}"
@@ -974,11 +1120,13 @@
     using assm(2) by auto
   obtain e f where e_f: "e \<in> s" "kle n e a" "f \<in> s" "kle n f a"
     "kle n e f" "card ?kle2 - 1 \<le> card {k \<in> {1..n}. e k < f k}"
-    using kle_range_induct[OF sizekle2, of n] using assm by auto
+    using kle_range_induct[OF sizekle2, of n]
+    using assm
+    by auto
 
   have "card {k\<in>{1..n}. a k < b k} = 1"
   proof (rule ccontr)
-    case goal1
+    assume "\<not> ?thesis"
     then have as: "card {k\<in>{1..n}. a k < b k} \<ge> 2"
       using ** by auto
     have *: "finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?kle1 = {}"
@@ -986,12 +1134,14 @@
     have "(card ?kle2 - 1) + 2 + (card ?kle1 - 1) = card ?kle2 + card ?kle1"
       using sizekle1 sizekle2 by auto
     also have "\<dots> = n + 1"
-      unfolding card_Un_Int[OF *(1-2)] *(3-) using assm(3) by auto
+      unfolding card_Un_Int[OF *(1-2)] *(3-)
+      using assm(3)
+      by auto
     finally have n: "(card ?kle2 - 1) + (2 + (card ?kle1 - 1)) = n + 1"
       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)
+      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}"
@@ -1001,28 +1151,31 @@
       done
     then have "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 -
-      apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a\<in>s` `d\<in>s`
+      apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a \<in> s` `d \<in> s`
       apply blast+
       done
     ultimately
     have "kle n e d \<and> (card ?kle2 - 1) + (2 + (card ?kle1 - 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 (rule kle_range_combine[where y=a]) 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
-    ultimately show False unfolding n by auto
+    ultimately show False
+      unfolding n by auto
   qed
   then guess k unfolding card_1_exists .. note k = this[unfolded mem_Collect_eq]
 
   show ?thesis
     apply (rule disjI2)
-    apply (rule_tac x=b in bexI, rule_tac x=k in bexI)
+    apply (rule_tac x=b in bexI)
+    apply (rule_tac x=k in bexI)
   proof
     fix j :: nat
     have "kle n a b"
-      using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`] by auto
+      using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`]
+      by auto
     then guess kk unfolding kle_def .. note kk_raw = this
     note kk = this[THEN conjunct2, rule_format]
     have kkk: "k \<in> kk"
@@ -1040,32 +1193,38 @@
         using kk_raw kkk
         apply auto
         done
-      then show ?thesis unfolding kk using kkk by auto
+      then show ?thesis
+        unfolding kk using kkk by auto
     next
       case False
       then have "j \<noteq> k"
-        using k(2)[rule_format, of j k] and kk_raw kkk by auto
-      then show ?thesis unfolding kk using kkk and False
+        using k(2)[rule_format, of j k] and kk_raw kkk
+        by auto
+      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:
-  assumes "ksimplex p n s" "a \<in> s"
-  shows "(\<forall>x\<in>s. kle n a x) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a(j) = (if j = k then y(j) + 1 else y(j)))"
+  assumes "ksimplex p n s"
+    and "a \<in> s"
+  shows "(\<forall>x\<in>s. kle n a x) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a j = (if j = k then y j + 1 else y j))"
 proof (cases "\<forall>x\<in>s. kle n a x")
   case True
   then show ?thesis by auto
 next
   note assm = ksimplexD[OF assms(1)]
   case False
-  then obtain b where b:"b\<in>s" "\<not> kle n a b" "\<forall>x\<in>{x \<in> s. \<not> kle n a x}. kle n x b"
-    using kle_maximal[of "{x\<in>s. \<not> kle n a x}" n] and assm by auto
+  then obtain b where b: "b \<in> s" "\<not> kle n a b" "\<forall>x\<in>{x \<in> s. \<not> kle n a x}. kle n x b"
+    using kle_maximal[of "{x\<in>s. \<not> kle n a x}" n] and assm
+    by auto
   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`
+    using assm(6) and `a \<in> s`
     apply (auto simp add: kle_refl)
     done
 
@@ -1079,23 +1238,28 @@
     using assm(2) by auto
   obtain c d where c_d: "c \<in> s" "\<not> kle n a c" "d \<in> s" "\<not> kle n a d"
     "kle n d c" "card ?kle1 - 1 \<le> card {k \<in> {1..n}. c k > d k}"
-    using kle_range_induct[OF sizekle1, of n] using assm by auto
+    using kle_range_induct[OF sizekle1, of n]
+    using assm
+    by auto
 
   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)
+    using assm(6)[rule_format,of a a] and `a \<in> s` and assm(2)
     apply auto
     done
-  then have sizekle2:"card ?kle2 = Suc (card ?kle2 - 1)"
-    using assm(2) by auto
+  then have sizekle2: "card ?kle2 = Suc (card ?kle2 - 1)"
+    using assm(2)
+    by auto
   obtain e f where e_f: "e \<in> s" "kle n a e" "f \<in> s" "kle n a f"
     "kle n f e" "card ?kle2 - 1 \<le> card {k \<in> {1..n}. e k > f k}"
-    using kle_range_induct[OF sizekle2, of n] using assm by auto
+    using kle_range_induct[OF sizekle2, of n]
+    using assm
+    by auto
 
   have "card {k\<in>{1..n}. a k > b k} = 1"
   proof (rule ccontr)
-    case goal1
+    assume "\<not> ?thesis"
     then have as: "card {k\<in>{1..n}. a k > b k} \<ge> 2"
       using ** by auto
     have *: "finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?kle1 = {}"
@@ -1103,7 +1267,8 @@
     have "(card ?kle2 - 1) + 2 + (card ?kle1 - 1) = card ?kle2 + card ?kle1"
       using sizekle1 sizekle2 by auto
     also have "\<dots> = n + 1"
-      unfolding card_Un_Int[OF *(1-2)] *(3-) using assm(3) by auto
+      unfolding card_Un_Int[OF *(1-2)] *(3-)
+      using assm(3) by auto
     finally have n: "(card ?kle1 - 1) + 2 + (card ?kle2 - 1) = n + 1"
       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}"
@@ -1118,7 +1283,7 @@
       done
     then have "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 -
-      apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a\<in>s` `d\<in>s`
+      apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a \<in> s` `d \<in> s`
       apply blast+
       done
     ultimately have "kle n d e \<and> (card ?kle1 - 1 + 2) + (card ?kle2 - 1) \<le> card {k\<in>{1..n}. e k > d k}"
@@ -1129,13 +1294,15 @@
       done
     moreover have "card {k \<in> {1..n}. e k > d k} \<le> card {1..n}"
       by (rule card_mono) auto
-    ultimately show False unfolding n by auto
+    ultimately show False
+      unfolding n by auto
   qed
   then guess k unfolding card_1_exists .. note k = this[unfolded mem_Collect_eq]
 
   show ?thesis
     apply (rule disjI2)
-    apply (rule_tac x=b in bexI,rule_tac x=k in bexI)
+    apply (rule_tac x=b in bexI)
+    apply (rule_tac x=k in bexI)
   proof
     fix j :: nat
     have "kle n b a"
@@ -1157,13 +1324,18 @@
         using kk_raw kkk
         apply auto
         done
-      then show ?thesis unfolding kk using kkk by auto
+      then show ?thesis
+        unfolding kk using kkk by auto
     next
       case False
-      then have "j \<noteq> k" using k(2)[rule_format, of j k]
-        using kk_raw kkk by auto
-      then show ?thesis unfolding kk
-        using kkk and False by auto
+      then have "j \<noteq> k"
+        using k(2)[rule_format, of j k]
+        using kk_raw kkk
+        by auto
+      then show ?thesis
+        unfolding kk
+        using kkk and False
+        by auto
     qed
   qed (insert k(1) `b\<in>s`, auto)
 qed
@@ -1173,25 +1345,32 @@
 
 (* FIXME: These are clones of lemmas in Library/FuncSet *)
 lemma card_funspace':
-  assumes "finite s" "finite t" "card s = m" "card t = n"
-  shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = n ^ m"  (is "card (?M s) = _")
+  assumes "finite s"
+    and "finite t"
+    and "card s = m"
+    and "card t = n"
+  shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = n ^ m"
+    (is "card (?M s) = _")
   using assms
-  apply -
 proof (induct m arbitrary: s)
   case 0
   have [simp]: "{f. \<forall>x. f x = d} = {\<lambda>x. d}"
-    apply (rule set_eqI,rule)
+    apply (rule set_eqI)
+    apply rule
     unfolding mem_Collect_eq
-    apply (rule, rule ext)
+    apply rule
+    apply (rule ext)
     apply auto
     done
-  from 0 show ?case by auto
+  from 0 show ?case
+    by auto
 next
   case (Suc m)
   guess a using card_eq_SucD[OF Suc(4)] ..
   then guess s0 by (elim exE conjE) note as0 = this
   have **: "card s0 = m"
-    using as0 using Suc(2) Suc(4) by auto
+    using as0 using Suc(2) Suc(4)
+    by auto
   let ?l = "(\<lambda>(b, g) x. if x = a then b else g x)"
   have *: "?M (insert a s0) = ?l ` {(b,g). b\<in>t \<and> g\<in>?M s0}"
     apply (rule set_eqI, rule)
@@ -1202,40 +1381,52 @@
     prefer 3
     apply rule
     defer
-    apply (erule bexE, rule)
+    apply (erule bexE)
+    apply rule
     unfolding mem_Collect_eq
     apply (erule splitE)+
     apply (erule conjE)+
   proof -
     fix x xa xb xc y
-    assume as: "x = (\<lambda>(b, g) x. if x = a then b else g x) xa"
-      "xb \<in> UNIV - insert a s0" "xa = (xc, y)" "xc \<in> t"
-      "\<forall>x\<in>s0. y x \<in> t" "\<forall>x\<in>UNIV - s0. y x = d"
-    then show "x xb = d" unfolding as by auto
+    assume as:
+      "x = (\<lambda>(b, g) x. if x = a then b else g x) xa"
+      "xb \<in> UNIV - insert a s0" "xa = (xc, y)"
+      "xc \<in> t"
+      "\<forall>x\<in>s0. y x \<in> t"
+      "\<forall>x\<in>UNIV - s0. y x = d"
+    then show "x xb = d"
+      unfolding as by auto
   qed auto
   have inj: "inj_on ?l {(b,g). b\<in>t \<and> g\<in>?M s0}"
     unfolding inj_on_def
-      apply (rule, rule, rule)
-      unfolding mem_Collect_eq
-      apply (erule splitE conjE)+
+    apply rule
+    apply rule
+    apply rule
+    unfolding mem_Collect_eq
+    apply (erule splitE conjE)+
   proof -
     case goal1 note as = this(1,4-)[unfolded goal1 split_conv]
-    have "xa = xb" using as(1)[THEN cong[of _ _ a]] by auto
+    have "xa = xb"
+      using as(1)[THEN cong[of _ _ a]] by auto
     moreover have "ya = yb"
     proof (rule ext)
       fix x
       show "ya x = yb x"
       proof (cases "x = a")
         case False
-        then show ?thesis using as(1)[THEN cong[of _ _ x x]] by auto
+        then show ?thesis
+          using as(1)[THEN cong[of _ _ x x]] by auto
       next
         case True
-        then show ?thesis using as(5,7) using as0(2) by auto
+        then show ?thesis
+          using as(5,7) using as0(2) by auto
       qed
     qed
-    ultimately show ?case unfolding goal1 by auto
+    ultimately show ?case
+      unfolding goal1 by auto
   qed
-  have "finite s0" using `finite s` unfolding as0 by simp
+  have "finite s0"
+    using `finite s` unfolding as0 by simp
   show ?case
     unfolding as0 * card_image[OF inj]
     using assms
@@ -1246,28 +1437,37 @@
 qed
 
 lemma card_funspace:
-  assumes "finite s" "finite t"
-  shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = (card t) ^ (card s)"
+  assumes "finite s"
+    and "finite t"
+  shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = card t ^ card s"
   using assms by (auto intro: card_funspace')
 
 lemma finite_funspace:
-  assumes "finite s" "finite t"
-  shows "finite {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)}" (is "finite ?S")
+  assumes "finite s"
+    and "finite t"
+  shows "finite {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)}"
+    (is "finite ?S")
 proof (cases "card t > 0")
   case True
-  have "card ?S = (card t) ^ (card s)"
+  have "card ?S = card t ^ card s"
     using assms by (auto intro!: card_funspace)
-  then show ?thesis using True by (rule_tac card_ge_0_finite) simp
+  then show ?thesis
+    using True by (rule_tac card_ge_0_finite) simp
 next
-  case False then have "t = {}" using `finite t` by auto
+  case False
+  then have "t = {}"
+    using `finite t` by auto
   show ?thesis
   proof (cases "s = {}")
-    have *: "{f. \<forall>x. f x = d} = {\<lambda>x. d}" by auto
     case True
-    then show ?thesis using `t = {}` by (auto simp: *)
+    have *: "{f. \<forall>x. f x = d} = {\<lambda>x. d}"
+      by auto
+    from True show ?thesis
+      using `t = {}` by (auto simp: *)
   next
     case False
-    then show ?thesis using `t = {}` by simp
+    then show ?thesis
+      using `t = {}` by simp
   qed
 qed
 
@@ -1281,8 +1481,10 @@
   done
 
 lemma simplex_top_face:
-  assumes "0 < p" "\<forall>x\<in>f. x (n + 1) = p"
-  shows "(\<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a})) \<longleftrightarrow> ksimplex p n f" (is "?ls = ?rs")
+  assumes "0 < p"
+    and "\<forall>x\<in>f. x (n + 1) = p"
+  shows "(\<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a})) \<longleftrightarrow> ksimplex p n f"
+    (is "?ls = ?rs")
 proof
   assume ?ls
   then guess s ..
@@ -1308,14 +1510,16 @@
       case True
       then guess k unfolding kle_def .. note k = this
       then have *: "n + 1 \<notin> k" using xyp by auto
-      have "\<not> (\<exists>x\<in>k. x\<notin>{1..n})"
+      have "\<not> (\<exists>x\<in>k. x \<notin> {1..n})"
         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
-        then show False using as and k[THEN conjunct1,unfolded subset_eq] by auto
+        have "x \<noteq> n + 1"
+          using as and * by auto
+        then show False
+          using as and k[THEN conjunct1,unfolded subset_eq] by auto
       qed
       then show ?thesis
         apply -
@@ -1328,18 +1532,23 @@
     next
       case False
       then have "kle (n + 1) y x"
-        using ksimplexD(6)[OF sa(1),rule_format, of x y] and as by auto
+        using ksimplexD(6)[OF sa(1),rule_format, of x y] and as
+        by auto
       then guess k unfolding kle_def .. note k = this
-      then have *: "n + 1 \<notin> k" using xyp by auto
-      then have "\<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 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
-        then show False using as and k[THEN conjunct1,unfolded subset_eq] by auto
+        have "x \<noteq> n + 1"
+          using as and * by auto
+        then show False
+          using as and k[THEN conjunct1,unfolded subset_eq]
+          by auto
       qed
       then show ?thesis
         apply -
@@ -1352,10 +1561,10 @@
     qed
   next
     fix x j
-    assume as: "x \<in> s - {a}" "j\<notin>{1..n}"
+    assume as: "x \<in> s - {a}" "j \<notin> {1..n}"
     then show "x j = p"
       using as(1)[unfolded sa(3)[symmetric], THEN assms(2)[rule_format]]
-      apply (cases "j = n+1")
+      apply (cases "j = n + 1")
       using sa(1)[unfolded ksimplex_def]
       apply auto
       done
@@ -1372,7 +1581,8 @@
     apply auto
     done
   then show ?ls
-    apply (rule_tac x = "insert c f" in exI, rule_tac x = c in exI)
+    apply (rule_tac x = "insert c f" in exI)
+    apply (rule_tac x = c in exI)
     unfolding ksimplex_def conj_assoc
     apply (rule conjI)
     defer
@@ -1386,15 +1596,19 @@
     fix x j
     assume x: "x \<in> insert c f"
     then show "x j \<le> p"
-    proof (cases "x=c")
+    proof (cases "x = c")
       case True
       show ?thesis
         unfolding True c_def
-        apply (cases "j=n+1")
+        apply (cases "j = n + 1")
         using ab(1) and rs(4)
         apply auto
         done
-    qed (insert x rs(4), auto simp add:c_def)
+    next
+      case False
+      with insert x rs(4) show ?thesis
+        by (auto simp add: c_def)
+    qed
     show "j \<notin> {1..n + 1} \<longrightarrow> x j = p"
       apply (cases "x = c")
       using x ab(1) rs(5)
@@ -1405,10 +1619,10 @@
       fix z
       assume z: "z \<in> insert c f"
       then have "kle (n + 1) c z"
-        apply (cases "z = c") (*defer apply(rule kle_Suc)*)
-      proof -
+      proof (cases "z = c")
         case False
-        then have "z \<in> f" using z by auto
+        then have "z \<in> f"
+          using z by auto
         then guess k
           apply (drule_tac ab(3)[THEN bspec[where x=z], THEN conjunct1])
           unfolding kle_def
@@ -1422,23 +1636,34 @@
           using rs(5)[rule_format,OF ab(1),of "n + 1"] assms(1)
           apply auto
           done
-        qed auto
+      next
+        case True
+        then show ?thesis by auto
+      qed
     } note * = this
     fix y
     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 then have **: "x \<in> f" "y \<in> f" using x y by auto
-      show ?thesis using rs(6)[rule_format,OF **]
+      case False
+      then have **: "x \<in> f" "y \<in> f"
+        using x y by auto
+      show ?thesis
+        using rs(6)[rule_format,OF **]
         by (auto dest: kle_Suc)
     qed (insert * x y, auto)
   qed (insert rs, auto)
 qed
 
 lemma ksimplex_fix_plane:
-  assumes "a \<in> s" "j\<in>{1..n::nat}" "\<forall>x\<in>s - {a}. x j = q" "a0 \<in> s" "a1 \<in> s"
-    "\<forall>i. a1 i = ((if i\<in>{1..n} then a0 i + 1 else a0 i)::nat)"
-  shows "(a = a0) \<or> (a = a1)"
+  fixes a a0 a1 :: "nat \<Rightarrow> nat"
+  assumes "a \<in> s"
+    and "j \<in> {1..n}"
+    and "\<forall>x\<in>s - {a}. x j = q"
+    and "a0 \<in> s"
+    and "a1 \<in> s"
+    and "\<forall>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
+  shows "a = a0 \<or> a = a1"
 proof -
   have *: "\<And>P A x y. \<forall>x\<in>A. P x \<Longrightarrow> x\<in>A \<Longrightarrow> y\<in>A \<Longrightarrow> P x \<and> P y"
     by auto
@@ -1452,8 +1677,13 @@
 qed
 
 lemma ksimplex_fix_plane_0:
-  assumes "a \<in> s" "j\<in>{1..n::nat}" "\<forall>x\<in>s - {a}. x j = 0" "a0 \<in> s" "a1 \<in> s"
-    "\<forall>i. a1 i = ((if i\<in>{1..n} then a0 i + 1 else a0 i)::nat)"
+  fixes a a0 a1 :: "nat \<Rightarrow> nat"
+  assumes "a \<in> s"
+    and "j \<in> {1..n}"
+    and "\<forall>x\<in>s - {a}. x j = 0"
+    and "a0 \<in> s"
+    and "a1 \<in> s"
+    and "\<forall>i. a1 i = (if i\<in>{1..n} then a0 i + 1 else a0 i)"
   shows "a = a1"
     apply (rule ccontr)
     using ksimplex_fix_plane[OF assms]
@@ -1464,12 +1694,17 @@
     done
 
 lemma ksimplex_fix_plane_p:
-  assumes "ksimplex p n s" "a \<in> s" "j\<in>{1..n}" "\<forall>x\<in>s - {a}. x j = p" "a0 \<in> s" "a1 \<in> s"
-    "\<forall>i. a1 i = (if i\<in>{1..n} then a0 i + 1 else a0 i)"
+  assumes "ksimplex p n s"
+    and "a \<in> s"
+    and "j \<in> {1..n}"
+    and "\<forall>x\<in>s - {a}. x j = p"
+    and "a0 \<in> s"
+    and "a1 \<in> s"
+    and "\<forall>i. a1 i = (if i\<in>{1..n} then a0 i + 1 else a0 i)"
   shows "a = a0"
 proof (rule ccontr)
   note s = ksimplexD[OF assms(1),rule_format]
-  assume as: "a \<noteq> a0"
+  assume as: "\<not> ?thesis"
   then have *: "a0 \<in> s - {a}"
     using assms(5) by auto
   then have "a1 = a"
@@ -1482,16 +1717,19 @@
 qed
 
 lemma ksimplex_replace_0:
-  assumes "ksimplex p n s" "a \<in> s" "n \<noteq> 0" "j\<in>{1..n}" "\<forall>x\<in>s - {a}. x j = 0"
+  assumes "ksimplex p n s" "a \<in> s"
+    and "n \<noteq> 0"
+    and "j \<in> {1..n}"
+    and "\<forall>x\<in>s - {a}. x j = 0"
   shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
 proof -
-  have *: "\<And>s' a a'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> (s' = s)"
+  have *: "\<And>s' a a'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s"
     by auto
   have **: "\<And>s' a'. ksimplex p n s' \<Longrightarrow> a' \<in> s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s"
   proof -
     case goal1
     guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note exta = this[rule_format]
-    have a:"a = a1"
+    have a: "a = a1"
       apply (rule ksimplex_fix_plane_0[OF assms(2,4-5)])
       using exta(1-2,5)
       apply auto
@@ -1538,7 +1776,11 @@
 qed
 
 lemma ksimplex_replace_1:
-  assumes "ksimplex p n s" "a \<in> s" "n \<noteq> 0" "j\<in>{1..n}" "\<forall>x\<in>s - {a}. x j = p"
+  assumes "ksimplex p n s"
+    and "a \<in> s"
+    and "n \<noteq> 0"
+    and "j \<in> {1..n}"
+    and "\<forall>x\<in>s - {a}. x j = p"
   shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
 proof -
   have lem: "\<And>a a' s'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s"
@@ -1570,16 +1812,12 @@
       by blast
     moreover
     have "a0 = b0"
-      apply (rule ext)
-    proof -
-      case goal1
+    proof (rule ext)
+      fix x
       show "a0 x = b0 x"
         using *[THEN cong, of x x]
         unfolding exta extb
-        apply -
-        apply (cases "x \<in> {1..n}")
-        apply auto
-        done
+        by (cases "x \<in> {1..n}") auto
     qed
     ultimately
     show "s' = s"
@@ -1592,7 +1830,8 @@
     unfolding card_1_exists
     apply (rule ex1I[of _ s])
     unfolding mem_Collect_eq
-    apply (rule, rule assms(1))
+    apply rule
+    apply (rule assms(1))
     apply (rule_tac x = a in bexI)
     prefer 3
     apply (erule conjE bexE)+
@@ -1603,26 +1842,33 @@
 qed
 
 lemma ksimplex_replace_2:
-  assumes "ksimplex p n s" "a \<in> s"
-    "n \<noteq> 0"
-    "~(\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = 0)"
-    "~(\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = p)"
+  assumes "ksimplex p n s"
+    and "a \<in> s"
+    and "n \<noteq> 0"
+    and "\<not> (\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = 0)"
+    and "\<not> (\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = p)"
   shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 2"
-  (is "card ?A = 2")
+    (is "card ?A = 2")
 proof -
   have lem1: "\<And>a a' s s'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s"
     by auto
-  have lem2: "\<And>a b. a\<in>s \<Longrightarrow> b\<noteq>a \<Longrightarrow> s \<noteq> insert b (s - {a})"
+  have lem2: "\<And>a b. a \<in> s \<Longrightarrow> b \<noteq> a \<Longrightarrow> s \<noteq> insert b (s - {a})"
   proof
     case goal1
-    then have "a \<in> insert b (s - {a})" by auto
-    then have "a \<in> s - {a}" unfolding insert_iff using goal1 by auto
-    then show False by auto
+    then have "a \<in> insert b (s - {a})"
+      by auto
+    then have "a \<in> s - {a}"
+      unfolding insert_iff
+      using goal1
+      by auto
+    then show False
+      by auto
   qed
   guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note a0a1 = this
   {
     assume "a = a0"
-    have *: "\<And>P Q. (P \<or> Q) \<Longrightarrow> \<not> P \<Longrightarrow> Q" by auto
+    have *: "\<And>P Q. P \<or> Q \<Longrightarrow> \<not> P \<Longrightarrow> Q"
+      by auto
     have "\<exists>x\<in>s. \<not> kle n x a0"
       apply (rule_tac x=a1 in bexI)
     proof
@@ -1630,7 +1876,8 @@
       show False
         using kle_imp_pointwise[OF as,THEN spec[where x=1]]
         unfolding a0a1(5)[THEN spec[where x=1]]
-        using assms(3) by auto
+        using assms(3)
+        by auto
     qed (insert a0a1, auto)
     then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a0 j + 1 else a0 j)"
       apply (rule_tac *[OF ksimplex_successor[OF assms(1-2),unfolded `a=a0`]])
@@ -1643,86 +1890,115 @@
     proof
       assume "a3\<in>s"
       then have "kle n a3 a1"
-      using a0a1(4) by auto
+        using a0a1(4) by auto
       then show False
-        apply (drule_tac kle_imp_pointwise) unfolding a3_def
+        apply (drule_tac kle_imp_pointwise)
+        unfolding a3_def
         apply (erule_tac x = k in allE)
         apply auto
         done
     qed
-    then have "a3 \<noteq> a0" "a3 \<noteq> a1" using a0a1 by auto
-    have "a2 \<noteq> a0" using k(2)[THEN spec[where x=k]] by auto
-    have lem3: "\<And>x. x\<in>(s - {a0}) \<Longrightarrow> kle n a2 x"
+    then have "a3 \<noteq> a0" and "a3 \<noteq> a1"
+      using a0a1 by auto
+    have "a2 \<noteq> a0"
+      using k(2)[THEN spec[where x=k]] by auto
+    have lem3: "\<And>x. x \<in> (s - {a0}) \<Longrightarrow> kle n a2 x"
     proof (rule ccontr)
       case goal1
-      then have as: "x\<in>s" "x\<noteq>a0" by auto
+      then have as: "x \<in> s" "x \<noteq> a0"
+        by auto
       have "kle n a2 x \<or> kle n x a2"
-        using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto
+        using ksimplexD(6)[OF assms(1)] and as `a2 \<in> s`
+        by auto
       moreover
-      have "kle n a0 x" using a0a1(4) as by auto
+      have "kle n a0 x"
+        using a0a1(4) as by auto
       ultimately have "x = a0 \<or> x = a2"
         apply -
         apply (rule kle_adjacent[OF k(2)])
         using goal1(2)
         apply auto
         done
-      then have "x = a2" using as by auto
-      then show False using goal1(2) using kle_refl by auto
+      then have "x = a2"
+        using as by auto
+      then show False
+        using goal1(2)
+        using kle_refl
+        by auto
     qed
     let ?s = "insert a3 (s - {a0})"
     have "ksimplex p n ?s"
       apply (rule ksimplexI)
-    proof (rule_tac[2-] ballI,rule_tac[4] ballI)
+      apply (rule_tac[2-] ballI)
+      apply (rule_tac[4] ballI)
+    proof -
       show "card ?s = n + 1"
         using ksimplexD(2-3)[OF assms(1)]
-        using `a3\<noteq>a0` `a3\<notin>s` `a0\<in>s`
-        by (auto simp add:card_insert_if)
+        using `a3 \<noteq> a0` `a3 \<notin> s` `a0 \<in> s`
+        by (auto simp add: card_insert_if)
       fix x
       assume x: "x \<in> insert a3 (s - {a0})"
       show "\<forall>j. x j \<le> p"
-      proof (rule, cases "x = a3")
+      proof
         fix j
-        case False
-        then show "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto
-      next
-        fix j
-        case True
-        show "x j\<le>p" unfolding True
-        proof (cases "j = k")
+        show "x j \<le> p"
+        proof (cases "x = a3")
           case False
-          then show "a3 j \<le>p" unfolding True a3_def
-          using `a1\<in>s` ksimplexD(4)[OF assms(1)] by auto
+          then show ?thesis
+            using x ksimplexD(4)[OF assms(1)] by auto
         next
-          guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] ..
-          note a4 = this
-          have "a2 k \<le> a4 k"
-            using lem3[OF a4(1)[unfolded `a=a0`],THEN kle_imp_pointwise] by auto
-          also have "\<dots> < p"
-            using ksimplexD(4)[OF assms(1),rule_format,of a4 k] using a4 by auto
-          finally have *:"a0 k + 1 < p"
-            unfolding k(2)[rule_format] by auto
           case True
-          then show "a3 j \<le>p" unfolding a3_def unfolding a0a1(5)[rule_format]
-            using k(1) k(2)assms(5) using * by simp
+          show ?thesis unfolding True
+          proof (cases "j = k")
+            case False
+            then show "a3 j \<le> p"
+              unfolding True a3_def
+              using `a1 \<in> s` ksimplexD(4)[OF assms(1)]
+              by auto
+          next
+            guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] ..
+            note a4 = this
+            have "a2 k \<le> a4 k"
+              using lem3[OF a4(1)[unfolded `a = a0`],THEN kle_imp_pointwise]
+              by auto
+            also have "\<dots> < p"
+              using ksimplexD(4)[OF assms(1),rule_format,of a4 k]
+              using a4 by auto
+            finally have *: "a0 k + 1 < p"
+              unfolding k(2)[rule_format]
+              by auto
+            case True
+            then show "a3 j \<le>p"
+              unfolding a3_def
+              unfolding a0a1(5)[rule_format]
+              using k(1) k(2)assms(5)
+              using *
+              by simp
+          qed
         qed
       qed
       show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
-      proof (rule, rule, cases "x=a3")
+      proof (rule, rule)
         fix j :: nat
         assume j: "j \<notin> {1..n}"
-        {
+        show "x j = p"
+        proof (cases "x = a3")
           case False
-          then show "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto
-        }
-        case True
-        show "x j = p"
-          unfolding True a3_def
-          using j k(1)
-          using ksimplexD(5)[OF assms(1),rule_format,OF `a1\<in>s` j] by auto
+          then show ?thesis
+            using j x ksimplexD(5)[OF assms(1)]
+            by auto
+        next
+          case True
+          show ?thesis
+            unfolding True a3_def
+            using j k(1)
+            using ksimplexD(5)[OF assms(1),rule_format,OF `a1\<in>s` j]
+            by auto
+        qed
       qed
       fix y
       assume y: "y \<in> insert a3 (s - {a0})"
-      have lem4: "\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a0 \<Longrightarrow> kle n x a3"
+      have lem4: "\<And>x. x\<in>s \<Longrightarrow> x \<noteq> a0 \<Longrightarrow> kle n x a3"
       proof -
         case goal1
         guess kk using a0a1(4)[rule_format, OF `x\<in>s`,THEN conjunct2,unfolded kle_def]
@@ -1731,12 +2007,17 @@
         have "k \<notin> kk"
         proof
           assume "k \<in> kk"
-          then have "a1 k = x k + 1" using kk by auto
-          then have "a0 k = x k" unfolding a0a1(5)[rule_format] using k(1) by auto
-          then have "a2 k = x k + 1" unfolding k(2)[rule_format] by auto
+          then have "a1 k = x k + 1"
+            using kk by auto
+          then have "a0 k = x k"
+            unfolding a0a1(5)[rule_format] using k(1) by auto
+          then have "a2 k = x k + 1"
+            unfolding k(2)[rule_format] by auto
           moreover
-          have "a2 k \<le> x k" using lem3[of x,THEN kle_imp_pointwise] goal1 by auto
-          ultimately show False by auto
+          have "a2 k \<le> x k"
+            using lem3[of x,THEN kle_imp_pointwise] goal1 by auto
+          ultimately show False
+            by auto
         qed
         then show ?case
           unfolding kle_def
@@ -1765,7 +2046,8 @@
           case True
           show ?thesis
             unfolding True
-            apply (rule disjI2, rule lem4)
+            apply (rule disjI2)
+            apply (rule lem4)
             using y False
             apply auto
             done
@@ -1782,15 +2064,18 @@
     then have "insert a3 (s - {a0}) \<in> ?A"
       unfolding mem_Collect_eq
       apply -
-      apply (rule, assumption)
+      apply rule
+      apply assumption
       apply (rule_tac x = "a3" in bexI)
       unfolding `a = a0`
       using `a3 \<notin> s`
       apply auto
       done
     moreover
-    have "s \<in> ?A" using assms(1,2) by auto
-    ultimately have  "?A \<supseteq> {s, insert a3 (s - {a0})}" by auto
+    have "s \<in> ?A"
+      using assms(1,2) by auto
+    ultimately have "?A \<supseteq> {s, insert a3 (s - {a0})}"
+      by auto
     moreover
     have "?A \<subseteq> {s, insert a3 (s - {a0})}"
       apply rule
@@ -1819,8 +2104,10 @@
         have "x k \<le> a2 k"
           unfolding k(2)[rule_format]
           using a0a1(4)[rule_format,of x, THEN conjunct1]
-          unfolding kle_def using x by auto
-        ultimately show "x k = a2 k" by auto
+          unfolding kle_def using x
+          by auto
+        ultimately show "x k = a2 k"
+        by auto
       qed
       have **: "a' = a_min \<or> a' = a_max"
         apply (rule ksimplex_fix_plane[OF a'(1) k(1) *])
@@ -1836,53 +2123,72 @@
           apply (rule a0a1(4)[rule_format,THEN conjunct2])
           defer
         proof (rule min_max(4)[rule_format,THEN conjunct2])
-          show "a1\<in>s'" using a' unfolding `a=a0` using a0a1 by auto
+          show "a1 \<in> s'"
+            using a'
+            unfolding `a = a0`
+            using a0a1
+            by auto
           show "a_max \<in> s"
           proof (rule ccontr)
-            assume "a_max \<notin> s"
-            then have "a_max = a'" using a' min_max by auto
-            then show False unfolding True using min_max by auto
+            assume "\<not> ?thesis"
+            then have "a_max = a'"
+              using a' min_max by auto
+            then show False
+              unfolding True using min_max by auto
           qed
         qed
-        then have "\<forall>i. a_max i = a1 i" by auto
-        then have "a' = a" unfolding True `a = a0`
+        then have "\<forall>i. a_max i = a1 i"
+          by auto
+        then have "a' = a"
+          unfolding True `a = a0`
           apply -
-          apply (subst fun_eq_iff, rule)
+          apply (subst fun_eq_iff)
+          apply rule
           apply (erule_tac x=x in allE)
           unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
         proof -
           case goal1
-          then show ?case by (cases "x\<in>{1..n}") auto
+          then show ?case
+            by (cases "x \<in> {1..n}") auto
         qed
         then have "s' = s"
           apply -
           apply (rule lem1[OF a'(2)])
-          using `a\<in>s` `a'\<in>s'`
+          using `a \<in> s` `a' \<in> s'`
           apply auto
           done
-        then show ?thesis by auto
+        then show ?thesis
+          by auto
       next
         case False
-        then have as:"a' = a_max" using ** by auto
-        have "a_min = a2" unfolding kle_antisym[symmetric, of _ _ n]
+        then have as: "a' = a_max"
+          using ** by auto
+        have "a_min = a2"
+          unfolding kle_antisym[symmetric, of _ _ n]
           apply rule
           apply (rule min_max(4)[rule_format,THEN conjunct1])
           defer
         proof (rule lem3)
           show "a_min \<in> s - {a0}"
             unfolding a'(2)[symmetric,unfolded `a = a0`]
-            unfolding as using min_max(1-3) by auto
+            unfolding as
+            using min_max(1-3)
+            by auto
           have "a2 \<noteq> a"
-            unfolding `a = a0` using k(2)[rule_format,of k] by auto
+            unfolding `a = a0`
+            using k(2)[rule_format,of k]
+            by auto
           then have "a2 \<in> s - {a}"
             using a2 by auto
-          then show "a2 \<in> s'" unfolding a'(2)[symmetric] by auto
+          then show "a2 \<in> s'"
+            unfolding a'(2)[symmetric] by auto
         qed
-        then have "\<forall>i. a_min i = a2 i" by auto
+        then have "\<forall>i. a_min i = a2 i"
+          by auto
         then have "a' = a3"
           unfolding as `a = a0`
-          apply -
-          apply (subst fun_eq_iff, rule)
+          apply (subst fun_eq_iff)
+          apply rule
           apply (erule_tac x=x in allE)
           unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
           unfolding a3_def k(2)[rule_format]
@@ -1891,10 +2197,10 @@
           case goal1
           show ?case
             unfolding goal1
-            apply (cases "x\<in>{1..n}")
+            apply (cases "x \<in> {1..n}")
             defer
             apply (cases "x = k")
-            using `k\<in>{1..n}`
+            using `k \<in> {1..n}`
             apply auto
             done
         qed
@@ -1911,14 +2217,18 @@
         then show ?thesis by auto
       qed
     qed
-    ultimately have *: "?A = {s, insert a3 (s - {a0})}" by blast
-    have "s \<noteq> insert a3 (s - {a0})" using `a3\<notin>s` by auto
-    then have ?thesis unfolding * by auto
+    ultimately have *: "?A = {s, insert a3 (s - {a0})}"
+      by blast
+    have "s \<noteq> insert a3 (s - {a0})"
+      using `a3\<notin>s` by auto
+    then have ?thesis
+      unfolding * by auto
   }
   moreover
   {
     assume "a = a1"
-    have *: "\<And>P Q. (P \<or> Q) \<Longrightarrow> \<not> P \<Longrightarrow> Q" by auto
+    have *: "\<And>P Q. P \<or> Q \<Longrightarrow> \<not> P \<Longrightarrow> Q"
+      by auto
     have "\<exists>x\<in>s. \<not> kle n a1 x"
       apply (rule_tac x=a0 in bexI)
     proof
@@ -1935,101 +2245,124 @@
       done
     then guess a2 .. from this(2) guess k .. note k=this note a2 = `a2 \<in> s`
     def a3 \<equiv> "\<lambda>j. if j = k then a0 j - 1 else a0 j"
-    have "a2 \<noteq> a1" using k(2)[THEN spec[where x=k]] by auto
-    have lem3: "\<And>x. x\<in>(s - {a1}) \<Longrightarrow> kle n x a2"
+    have "a2 \<noteq> a1"
+      using k(2)[THEN spec[where x=k]] by auto
+    have lem3: "\<And>x. x \<in> s - {a1} \<Longrightarrow> kle n x a2"
     proof (rule ccontr)
       case goal1
-      then have as: "x\<in>s" "x\<noteq>a1" by auto
+      then have as: "x \<in> s" "x \<noteq> a1" by auto
       have "kle n a2 x \<or> kle n x a2"
-        using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto
+        using ksimplexD(6)[OF assms(1)] and as `a2\<in>s`
+        by auto
       moreover
-      have "kle n x a1" using a0a1(4) as by auto
+      have "kle n x a1"
+        using a0a1(4) as by auto
       ultimately have "x = a2 \<or> x = a1"
         apply -
         apply (rule kle_adjacent[OF k(2)])
         using goal1(2)
         apply auto
         done
-      then have "x = a2" using as by auto
-      then show False using goal1(2) using kle_refl by auto
+      then have "x = a2"
+        using as by auto
+      then show False
+        using goal1(2) using kle_refl by auto
     qed
     have "a0 k \<noteq> 0"
     proof -
       guess a4 using assms(4)[unfolded bex_simps ball_simps,rule_format,OF `k\<in>{1..n}`] ..
       note a4 = this
-      have "a4 k \<le> a2 k" using lem3[OF a4(1)[unfolded `a=a1`],THEN kle_imp_pointwise]
+      have "a4 k \<le> a2 k"
+        using lem3[OF a4(1)[unfolded `a=a1`],THEN kle_imp_pointwise]
+        by auto
+      moreover have "a4 k > 0"
+        using a4 by auto
+      ultimately have "a2 k > 0"
         by auto
-      moreover have "a4 k > 0" using a4 by auto
-      ultimately have "a2 k > 0" by auto
-      then have "a1 k > 1" unfolding k(2)[rule_format] by simp
-      then show ?thesis unfolding a0a1(5)[rule_format] using k(1) by simp
+      then have "a1 k > 1"
+        unfolding k(2)[rule_format] by simp
+      then show ?thesis
+        unfolding a0a1(5)[rule_format] using k(1) by simp
     qed
-    then have lem4: "\<forall>j. a0 j = (if j=k then a3 j + 1 else a3 j)"
+    then have lem4: "\<forall>j. a0 j = (if j = k then a3 j + 1 else a3 j)"
       unfolding a3_def by simp
     have "\<not> kle n a0 a3"
-      apply (rule ccontr)
-      unfolding not_not
+      apply (rule notI)
       apply (drule kle_imp_pointwise)
       unfolding lem4[rule_format]
       apply (erule_tac x=k in allE)
       apply auto
       done
-    then have "a3 \<notin> s" using a0a1(4) by auto
-    then have "a3 \<noteq> a1" "a3 \<noteq> a0" using a0a1 by auto
+    then have "a3 \<notin> s"
+      using a0a1(4) by auto
+    then have "a3 \<noteq> a1" "a3 \<noteq> a0"
+      using a0a1 by auto
     let ?s = "insert a3 (s - {a1})"
     have "ksimplex p n ?s"
       apply (rule ksimplexI)
     proof (rule_tac[2-] ballI,rule_tac[4] ballI)
       show "card ?s = n+1"
         using ksimplexD(2-3)[OF assms(1)]
-        using `a3\<noteq>a0` `a3\<notin>s` `a1\<in>s`
-        by(auto simp add:card_insert_if)
+        using `a3 \<noteq> a0` `a3 \<notin> s` `a1 \<in> s`
+        by (auto simp add:card_insert_if)
       fix x
       assume x: "x \<in> insert a3 (s - {a1})"
-      show "\<forall>j. x j \<le> p" proof(rule,cases "x = a3")
+      show "\<forall>j. x j \<le> p"
+      proof
         fix j
-        case False
-        then show "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto
-      next
-        fix j
-        case True
-        show "x j\<le>p" unfolding True
-        proof (cases "j = k")
+        show "x j \<le> p"
+        proof (cases "x = a3")
           case False
-          then show "a3 j \<le>p"
-            unfolding True a3_def
-            using `a0\<in>s` ksimplexD(4)[OF assms(1)]
-            by auto
+          then show ?thesis
+            using x ksimplexD(4)[OF assms(1)] by auto
         next
-          guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] ..
-          note a4 = this
-          case True have "a3 k \<le> a0 k"
-            unfolding lem4[rule_format] by auto
-          also have "\<dots> \<le> p"
-            using ksimplexD(4)[OF assms(1),rule_format,of a0 k] a0a1 by auto
-          finally show "a3 j \<le> p"
-            unfolding True by auto
+          case True
+          show ?thesis
+            unfolding True
+          proof (cases "j = k")
+            case False
+            then show "a3 j \<le> p"
+              unfolding True a3_def
+              using `a0 \<in> s` ksimplexD(4)[OF assms(1)]
+              by auto
+          next
+            guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] ..
+            note a4 = this
+            case True have "a3 k \<le> a0 k"
+              unfolding lem4[rule_format] by auto
+            also have "\<dots> \<le> p"
+              using ksimplexD(4)[OF assms(1),rule_format, of a0 k] a0a1
+              by auto
+            finally show "a3 j \<le> p"
+              unfolding True by auto
+          qed
         qed
       qed
       show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
-      proof (rule, rule, cases "x = a3")
+      proof (rule, rule)
         fix j :: nat
         assume j: "j \<notin> {1..n}"
-        {
+        show "x j = p"
+        proof (cases "x = a3")
           case False
-          then show "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto
+          then show ?thesis
+            using j x ksimplexD(5)[OF assms(1)] by auto
         next
           case True
-          show "x j = p" unfolding True a3_def using j k(1)
-            using ksimplexD(5)[OF assms(1),rule_format,OF `a0\<in>s` j] by auto
-        }
+          show ?thesis
+            unfolding True a3_def
+            using j k(1)
+            using ksimplexD(5)[OF assms(1),rule_format,OF `a0\<in>s` j]
+            by auto
+        qed
       qed
       fix y
-      assume y: "y\<in>insert a3 (s - {a1})"
-      have lem4: "\<And>x. x\<in>s \<Longrightarrow> x \<noteq> a1 \<Longrightarrow> kle n a3 x"
+      assume y: "y \<in> insert a3 (s - {a1})"
+      have lem4: "\<And>x. x \<in> s \<Longrightarrow> x \<noteq> a1 \<Longrightarrow> kle n a3 x"
       proof -
         case goal1
-        then have *: "x\<in>s - {a1}" by auto
+        then have *: "x\<in>s - {a1}"
+          by auto
         have "kle n a3 a2"
         proof -
           have "kle n a0 a1"
@@ -2075,7 +2408,8 @@
           unfolding True
           apply (cases "x = a3")
           defer
-          apply (rule disjI2, rule lem4)
+          apply (rule disjI2)
+          apply (rule lem4)
           using x
           apply auto
           done
@@ -2086,7 +2420,8 @@
           case True
           show ?thesis
             unfolding True
-            apply (rule disjI1, rule lem4)
+            apply (rule disjI1)
+            apply (rule lem4)
             using y False
             apply auto
             done
@@ -2094,7 +2429,7 @@
           case False
           then show ?thesis
             apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])
-            using x y `y\<noteq>a3`
+            using x y `y \<noteq> a3`
             apply auto
             done
         qed
@@ -2110,8 +2445,10 @@
         apply auto
         done
     moreover
-    have "s \<in> ?A" using assms(1,2) by auto
-    ultimately have "?A \<supseteq> {s, insert a3 (s - {a1})}" by auto
+    have "s \<in> ?A"
+      using assms(1,2) by auto
+    ultimately have "?A \<supseteq> {s, insert a3 (s - {a1})}"
+      by auto
     moreover have "?A \<subseteq> {s, insert a3 (s - {a1})}"
       apply rule
       unfolding mem_Collect_eq
@@ -2146,7 +2483,8 @@
             by auto
           finally have "a2 k \<le> x k" .
         }
-        ultimately show "x k = a2 k" by auto
+        ultimately show "x k = a2 k"
+          by auto
       qed
       have **: "a' = a_min \<or> a' = a_max"
         apply (rule ksimplex_fix_plane[OF a'(1) k(1) *])
@@ -2179,36 +2517,47 @@
           unfolding kle_antisym[symmetric,of a_max a2 n]
           apply -
           apply rule
-          apply (rule lem3,assumption)
+          apply (rule lem3)
+          apply assumption
           apply (rule min_max(4)[rule_format,THEN conjunct2])
           using a2'
           apply auto
           done
-        then have a_max:"\<forall>i. a_max i = a2 i" by auto
-        have *: "\<forall>j. a2 j = (if j\<in>{1..n} then a3 j + 1 else a3 j)"
+        then have a_max: "\<forall>i. a_max i = a2 i"
+          by auto
+        have *: "\<forall>j. a2 j = (if j \<in> {1..n} then a3 j + 1 else a3 j)"
           using k(2)
           unfolding lem4[rule_format] a0a1(5)[rule_format]
           apply -
-          apply (rule,erule_tac x=j in allE)
+          apply rule
+          apply (erule_tac x=j in allE)
         proof -
           case goal1
-          then show ?case by (cases "j\<in>{1..n}",case_tac[!] "j=k") auto
+          then show ?case by (cases "j \<in> {1..n}", case_tac[!] "j = k") auto
         qed
         have "\<forall>i. a_min i = a3 i"
           using a_max
             apply -
-            apply (rule,erule_tac x=i in allE)
+            apply rule
+            apply (erule_tac x=i in allE)
             unfolding min_max(5)[rule_format] *[rule_format]
         proof -
           case goal1
-          then show ?case by (cases "i\<in>{1..n}") auto
+          then show ?case
+            by (cases "i \<in> {1..n}") auto
         qed
-        then have "a_min = a3" unfolding fun_eq_iff .
+        then have "a_min = a3"
+          unfolding fun_eq_iff .
         then have "s' = insert a3 (s - {a1})"
-          using a' unfolding `a = a1` True by auto
-        then show ?thesis by auto
+          using a'
+          unfolding `a = a1` True
+          by auto
+        then show ?thesis
+          by auto
       next
-        case False then have as:"a'=a_max" using ** by auto
+        case False
+        then have as: "a' = a_max"
+          using ** by auto
         have "a_min = a0"
           unfolding kle_antisym[symmetric,of _ _ n]
           apply rule
@@ -2220,12 +2569,17 @@
             using min_max(1,3)
             unfolding a'(2)[symmetric,unfolded `a=a1`] as
             by auto
-          then show "a_min \<in> s" by auto
-          have "a0 \<in> s - {a1}" using a0a1(1-3) by auto
-          then show "a0 \<in> s'" unfolding a'(2)[symmetric,unfolded `a=a1`] by auto
+          then show "a_min \<in> s"
+            by auto
+          have "a0 \<in> s - {a1}"
+            using a0a1(1-3) by auto
+          then show "a0 \<in> s'"
+            unfolding a'(2)[symmetric,unfolded `a=a1`]
+            by auto
         qed
         then have "\<forall>i. a_max i = a1 i"
-          unfolding a0a1(5)[rule_format] min_max(5)[rule_format] by auto
+          unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
+          by auto
         then have "s' = s"
           apply -
           apply (rule lem1[OF a'(2)])
@@ -2234,16 +2588,21 @@
           unfolding fun_eq_iff
           apply auto
           done
-        then show ?thesis by auto
+        then show ?thesis
+          by auto
       qed
     qed
-    ultimately have *: "?A = {s, insert a3 (s - {a1})}" by blast
-    have "s \<noteq> insert a3 (s - {a1})" using `a3\<notin>s` by auto
-    then have ?thesis unfolding * by auto
+    ultimately have *: "?A = {s, insert a3 (s - {a1})}"
+      by blast
+    have "s \<noteq> insert a3 (s - {a1})"
+      using `a3\<notin>s` by auto
+    then have ?thesis
+      unfolding * by auto
   }
   moreover
   {
-    assume as: "a \<noteq> a0" "a \<noteq> a1" have "\<not> (\<forall>x\<in>s. kle n a x)"
+    assume as: "a \<noteq> a0" "a \<noteq> a1"
+    have "\<not> (\<forall>x\<in>s. kle n a x)"
     proof
       case goal1
       have "a = a0"
@@ -2252,10 +2611,12 @@
         using goal1 a0a1 assms(2)
         apply auto
         done
-      then show False using as by auto
+      then show False
+        using as by auto
     qed
     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)"
-      using ksimplex_predecessor[OF assms(1-2)] by blast
+      using ksimplex_predecessor[OF assms(1-2)]
+      by blast
     then guess u .. from this(2) guess k .. note k = this[rule_format]
     note u = `u \<in> s`
     have "\<not> (\<forall>x\<in>s. kle n x a)"
@@ -2267,19 +2628,23 @@
         using goal1 a0a1 assms(2)
         apply auto
         done
-      then show False using as by auto
+      then show False
+        using as by auto
     qed
     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)"
       using ksimplex_successor[OF assms(1-2)] by blast
     then guess v .. from this(2) guess l ..
     note l = this[rule_format]
-    note v = `v\<in>s`
+    note v = `v \<in> s`
     def a' \<equiv> "\<lambda>j. if j = l then u j + 1 else u j"
     have kl: "k \<noteq> l"
     proof
       assume "k = l"
-      have *: "\<And>P. (if P then (1::nat) else 0) \<noteq> 2" by auto
-      then show False using ksimplexD(6)[OF assms(1),rule_format,OF u v] unfolding kle_def
+      have *: "\<And>P. (if P then (1::nat) else 0) \<noteq> 2"
+        by auto
+      then show False
+        using ksimplexD(6)[OF assms(1),rule_format,OF u v]
+        unfolding kle_def
         unfolding l(2) k(2) `k = l`
         apply -
         apply (erule disjE)
@@ -2301,7 +2666,8 @@
       apply (drule ksimplexD(6)[OF assms(1),rule_format,OF `a\<in>s`])
     proof (cases "kle n a a'")
       case goal2
-      then have "kle n a' a" by auto
+      then have "kle n a' a"
+        by auto
       then show False
         apply (drule_tac kle_imp_pointwise)
         apply (erule_tac x=l in allE)
@@ -2334,8 +2700,10 @@
       then show ?case
       proof (cases "x k = u k", case_tac[!] "x l = u l")
         assume as: "x l = u l" "x k = u k"
-        have "x = u" unfolding fun_eq_iff
-          using goal1(2)[THEN kle_imp_pointwise,unfolded l(2)] unfolding k(2)
+        have "x = u"
+          unfolding fun_eq_iff
+          using goal1(2)[THEN kle_imp_pointwise,unfolded l(2)]
+          unfolding k(2)
           apply -
           using goal1(1)[THEN kle_imp_pointwise]
           apply -
@@ -2346,9 +2714,11 @@
           then show ?case
             apply (cases "x = l")
             apply (case_tac[!] "x = k")
-            using as by auto
+            using as
+            by auto
         qed
-        then show ?case by auto
+        then show ?case
+          by auto
       next
         assume as: "x l \<noteq> u l" "x k = u k"
         have "x = a'"
@@ -2389,7 +2759,8 @@
             apply auto
             done
         qed
-        then show ?case by auto
+        then show ?case
+          by auto
       next
         assume as: "x l \<noteq> u l" "x k \<noteq> u k"
         have "x = v"
@@ -2424,16 +2795,16 @@
       apply (rule kle_trans[OF uv])
       defer
       apply (rule ksimplexD(6)[OF assms(1), rule_format])
-      using kle_uv `u\<in>s`
+      using kle_uv `u \<in> s`
       apply auto
       done
-    have lem4: "\<And>x. x\<in>s \<Longrightarrow> kle n x u \<Longrightarrow> kle n x a'"
+    have lem4: "\<And>x. x \<in> s \<Longrightarrow> kle n x u \<Longrightarrow> kle n x a'"
       apply (rule kle_between_l[of _ u _ v])
       prefer 4
       apply (rule kle_trans[OF _ uv])
       defer
       apply (rule ksimplexD(6)[OF assms(1), rule_format])
-      using kle_uv `v\<in>s`
+      using kle_uv `v \<in> s`
       apply auto
       done
     have lem5: "\<And>x. x \<in> s \<Longrightarrow> x \<noteq> a \<Longrightarrow> kle n x a' \<or> kle n a' x"
@@ -2442,12 +2813,13 @@
       then show ?case
       proof (cases "kle n v x \<or> kle n x u")
         case True
-        then show ?thesis using goal1 by(auto intro:lem3 lem4)
+        then show ?thesis
+          using goal1 by (auto intro: lem3 lem4)
       next
         case False
         then have *: "kle n u x" "kle n x v"
           using ksimplexD(6)[OF assms(1)]
-          using goal1 `u\<in>s` `v\<in>s`
+          using goal1 `u \<in> s` `v \<in> s`
           by auto
         show ?thesis
           using uxv[OF *]
@@ -2458,7 +2830,9 @@
     qed
     have "ksimplex p n (insert a' (s - {a}))"
       apply (rule ksimplexI)
-    proof (rule_tac[2-] ballI, rule_tac[4] ballI)
+      apply (rule_tac[2-] ballI)
+      apply (rule_tac[4] ballI)
+    proof -
       show "card (insert a' (s - {a})) = n + 1"
         using ksimplexD(2-3)[OF assms(1)]
         using `a' \<noteq> a` `a' \<notin> s` `a \<in> s`
@@ -2466,45 +2840,59 @@
       fix x
       assume x: "x \<in> insert a' (s - {a})"
       show "\<forall>j. x j \<le> p"
-      proof (rule, cases "x = a'")
-        fix j
-        case False
-        then show "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto
-      next
+      proof
         fix j
-        case True
-        show "x j\<le>p" unfolding True
-        proof (cases "j = l")
+        show "x j \<le> p"
+        proof (cases "x = a'")
           case False
-          then show "a' j \<le>p"
-            unfolding True a'_def using `u\<in>s` ksimplexD(4)[OF assms(1)] by auto
+          then show ?thesis
+            using x ksimplexD(4)[OF assms(1)] by auto
         next
           case True
-          have *: "a l = u l" "v l = a l + 1"
-            using k(2)[of l] l(2)[of l] `k\<noteq>l` by auto
-          have "u l + 1 \<le> p"
-            unfolding *[symmetric] using ksimplexD(4)[OF assms(1)] using `v\<in>s` by auto
-          then show "a' j \<le>p" unfolding a'_def True by auto
+          show ?thesis
+            unfolding True
+          proof (cases "j = l")
+            case False
+            then show "a' j \<le>p"
+              unfolding True a'_def
+              using `u\<in>s` ksimplexD(4)[OF assms(1)]
+              by auto
+          next
+            case True
+            have *: "a l = u l" "v l = a l + 1"
+              using k(2)[of l] l(2)[of l] `k \<noteq> l`
+              by auto
+            have "u l + 1 \<le> p"
+              unfolding *[symmetric]
+              using ksimplexD(4)[OF assms(1)]
+              using `v \<in> s`
+              by auto
+            then show "a' j \<le>p"
+              unfolding a'_def True
+              by auto
+          qed
         qed
       qed
       show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
-      proof (rule, rule,cases "x = a'")
+      proof (rule, rule)
         fix j :: nat
         assume j: "j \<notin> {1..n}"
-        {
+        show "x j = p"
+        proof (cases "x = a'")
           case False
-          then show "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto
+          then show ?thesis
+            using j x ksimplexD(5)[OF assms(1)] by auto
         next
           case True
-          show "x j = p"
+          show ?thesis
             unfolding True a'_def
             using j l(1)
             using ksimplexD(5)[OF assms(1),rule_format,OF `u\<in>s` j]
             by auto
-        }
+        qed
       qed
       fix y
-      assume y: "y\<in>insert a' (s - {a})"
+      assume y: "y \<in> insert a' (s - {a})"
       show "kle n x y \<or> kle n y x"
       proof (cases "y = a'")
         case True
@@ -2528,7 +2916,7 @@
           case False
           then show ?thesis
             apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])
-            using x y `y\<noteq>a'`
+            using x y `y \<noteq> a'`
             apply auto
             done
         qed
@@ -2537,25 +2925,33 @@
     then have "insert a' (s - {a}) \<in> ?A"
       unfolding mem_Collect_eq
       apply -
-      apply (rule, assumption)
+      apply rule
+      apply assumption
       apply (rule_tac x = "a'" in bexI)
       using aa' `a' \<notin> s`
       apply auto
       done
     moreover
-    have "s \<in> ?A" using assms(1,2) by auto
-    ultimately have  "?A \<supseteq> {s, insert a' (s - {a})}" by auto
+    have "s \<in> ?A"
+      using assms(1,2) by auto
+    ultimately have  "?A \<supseteq> {s, insert a' (s - {a})}"
+      by auto
     moreover
     have "?A \<subseteq> {s, insert a' (s - {a})}"
-      apply rule unfolding mem_Collect_eq
+      apply rule
+      unfolding mem_Collect_eq
     proof (erule conjE)
       fix s'
       assume as: "ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
       from this(2) guess a'' .. note a'' = this
-      have "u \<noteq> v" unfolding fun_eq_iff unfolding l(2) k(2) by auto
-      then have uv': "\<not> kle n v u" using uv using kle_antisym by auto
-      have "u \<noteq> a" "v \<noteq> a" unfolding fun_eq_iff k(2) l(2) by auto
-      then have uvs': "u \<in> s'" "v \<in> s'" using `u \<in> s` `v \<in> s` using a'' by auto
+      have "u \<noteq> v"
+        unfolding fun_eq_iff unfolding l(2) k(2) by auto
+      then have uv': "\<not> kle n v u"
+        using uv using kle_antisym by auto
+      have "u \<noteq> a" "v \<noteq> a"
+        unfolding fun_eq_iff k(2) l(2) by auto
+      then have uvs': "u \<in> s'" "v \<in> s'"
+        using `u \<in> s` `v \<in> s` using a'' by auto
       have lem6: "a \<in> s' \<or> a' \<in> s'"
       proof (cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x")
         case False
@@ -2564,7 +2960,8 @@
           using ksimplexD(6)[OF as] uvs' by auto
         then have "w = a' \<or> w = a"
           using uxv[of w] uvs' w by auto
-        then show ?thesis using w by auto
+        then show ?thesis
+          using w by auto
       next
         case True
         have "\<not> (\<forall>x\<in>s'. kle n x u)"
@@ -2572,42 +2969,48 @@
           apply (rule_tac x=v in bexI)
           using uv `u \<noteq> v`
           unfolding kle_antisym [of n u v,symmetric]
-          using `v\<in>s'`
+          using `v \<in> s'`
           apply auto
           done
         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)"
-          using ksimplex_successor[OF as `u\<in>s'`] by blast
+          using ksimplex_successor[OF as `u\<in>s'`]
+          by blast
         then guess w .. note w = this
         from this(2) guess kk .. note kk = this[rule_format]
         have "\<not> kle n w u"
           apply -
-          apply (rule, drule kle_imp_pointwise)
+          apply rule
+          apply (drule kle_imp_pointwise)
           apply (erule_tac x = kk in allE)
           unfolding kk
           apply auto
           done
         then have *: "kle n v w"
-          using True[rule_format,OF w(1)] by auto
+          using True[rule_format,OF w(1)]
+          by auto
         then have False
-        proof (cases "kk \<noteq> l")
-          case True
+        proof (cases "kk = l")
+          case False
           then show False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
             apply (erule_tac x=l in allE)
             using `k \<noteq> l`
             apply auto  
             done
         next
-          case False
+          case True
           then have "kk \<noteq> k" using `k \<noteq> l` by auto
-          then show False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
+          then show False
+            using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
             apply (erule_tac x=k in allE)
             using `k \<noteq> l`
             apply auto
             done
         qed
-        then show ?thesis by auto
+        then show ?thesis
+          by auto
       qed
-      then show "s' \<in> {s, insert a' (s - {a})}" proof(cases "a\<in>s'")
+      then show "s' \<in> {s, insert a' (s - {a})}"
+      proof (cases "a \<in> s'")
         case True
         then have "s' = s"
           apply -
@@ -2615,38 +3018,46 @@
           using a'' `a \<in> s`
           apply auto
           done
-        then show ?thesis by auto
+        then show ?thesis
+          by auto
       next
-        case False then have "a'\<in>s'" using lem6 by auto
+        case False
+        then have "a' \<in> s'"
+          using lem6 by auto
         then have "s' = insert a' (s - {a})"
           apply -
           apply (rule lem1[of _ a'' _ a'])
-          unfolding a''(2)[symmetric] using a'' and `a'\<notin>s` by auto
-        then show ?thesis by auto
+          unfolding a''(2)[symmetric]
+          using a'' and `a' \<notin> s`
+          by auto
+        then show ?thesis
+          by auto
       qed
     qed
-    ultimately have *: "?A = {s, insert a' (s - {a})}" by blast
-    have "s \<noteq> insert a' (s - {a})" using `a'\<notin>s` by auto
-    then have ?thesis unfolding * by auto
+    ultimately have *: "?A = {s, insert a' (s - {a})}"
+      by blast
+    have "s \<noteq> insert a' (s - {a})"
+      using `a'\<notin>s` by auto
+    then have ?thesis
+      unfolding * by auto
   }
-  ultimately show ?thesis by auto
+  ultimately show ?thesis
+    by auto
 qed
 
 
-subsection {* Hence another step towards concreteness. *}
+text {* Hence another step towards concreteness. *}
 
 lemma kuhn_simplex_lemma:
-  assumes "\<forall>s. ksimplex p (n + 1) s \<longrightarrow> (rl ` s \<subseteq>{0..n+1})"
-    "odd (card{f. \<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a}) \<and>
-    (rl ` 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))})"
-  shows "odd(card {s\<in>{s. ksimplex p (n + 1) s}. rl ` s = {0..n+1} })"
+  assumes "\<forall>s. ksimplex p (n + 1) s \<longrightarrow> rl ` s \<subseteq> {0..n+1}"
+    and "odd (card {f. \<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a}) \<and>
+      rl ` 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))})"
+  shows "odd (card {s \<in> {s. ksimplex p (n + 1) s}. rl ` s = {0..n+1}})"
 proof -
   have *: "\<And>x y. x = y \<Longrightarrow> odd (card x) \<Longrightarrow> odd (card y)"
     by auto
-  have *: "odd(card {f\<in>{f. \<exists>s\<in>{s. ksimplex p (n + 1) s}. (\<exists>a\<in>s. f = s - {a})}.
-    (rl ` 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))})"
+  have *: "odd (card {f \<in> {f. \<exists>s\<in>{s. ksimplex p (n + 1) s}. (\<exists>a\<in>s. f = s - {a})}.
+    rl ` 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))})"
     apply (rule *[OF _ assms(2)])
     apply auto
     done
@@ -2654,10 +3065,13 @@
     apply (rule kuhn_complete_lemma[OF finite_simplices])
     prefer 6
     apply (rule *)
-    apply (rule, rule, rule)
+    apply rule
+    apply rule
+    apply rule
     apply (subst ksimplex_def)
     defer
-    apply (rule, rule assms(1)[rule_format])
+    apply rule
+    apply (rule assms(1)[rule_format])
     unfolding mem_Collect_eq
     apply assumption
     apply default+
@@ -2672,7 +3086,7 @@
     unfolding mem_Collect_eq
   proof -
     fix f s a
-    assume as: "ksimplex p (n + 1) s" "a\<in>s" "f = s - {a}"
+    assume as: "ksimplex p (n + 1) s" "a \<in> s" "f = s - {a}"
     let ?S = "{s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})}"
     have S: "?S = {s'. ksimplex p (n + 1) s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})}"
       unfolding as by blast
@@ -2711,23 +3125,25 @@
 qed
 
 
-subsection {* Reduced labelling. *}
+subsection {* Reduced labelling *}
 
-definition "reduced label (n::nat) (x::nat\<Rightarrow>nat) =
-  (SOME k. k \<le> n \<and> (\<forall>i. 1\<le>i \<and> i<k+1 \<longrightarrow> label x i = 0) \<and>
+definition "reduced label (n::nat) (x::nat \<Rightarrow> nat) =
+  (SOME k. k \<le> n \<and> (\<forall>i. 1 \<le> i \<and> i < k + 1 \<longrightarrow> label x i = 0) \<and>
     (k = n \<or> label x (k + 1) \<noteq> (0::nat)))"
 
 lemma reduced_labelling:
   shows "reduced label n x \<le> n" (is ?t1)
-    and "\<forall>i. 1\<le>i \<and> i < reduced label n x + 1 \<longrightarrow> (label x i = 0)" (is ?t2)
-    and "(reduced label n x = n) \<or> (label x (reduced label n x + 1) \<noteq> 0)"  (is ?t3)
+    and "\<forall>i. 1 \<le> i \<and> i < reduced label n x + 1 \<longrightarrow> label x i = 0" (is ?t2)
+    and "reduced label n x = n \<or> label x (reduced label n x + 1) \<noteq> 0"  (is ?t3)
 proof -
   have num_WOP: "\<And>P k. P (k::nat) \<Longrightarrow> \<exists>n. P n \<and> (\<forall>m<n. \<not> P m)"
     apply (drule ex_has_least_nat[where m="\<lambda>x. x"])
-    apply (erule exE,rule_tac x=x in exI)
+    apply (erule exE)
+    apply (rule_tac x=x in exI)
     apply auto
     done
-  have *: "n \<le> n \<and> (label x (n + 1) \<noteq> 0 \<or> n = n)" by auto
+  have *: "n \<le> n \<and> (label x (n + 1) \<noteq> 0 \<or> n = n)"
+    by auto
   then guess N
     apply (drule_tac num_WOP[of "\<lambda>j. j\<le>n \<and> (label x (j+1) \<noteq> 0 \<or> n = j)"])
     apply (erule exE)
@@ -2738,10 +3154,11 @@
     defer
   proof (rule, rule)
     fix i
-    assume i: "1\<le>i \<and> i<N+1"
+    assume i: "1 \<le> i \<and> i < N + 1"
     then show "label x i = 0"
       using N[THEN conjunct2,THEN spec[where x="i - 1"]]
-      using N by auto
+      using N
+      by auto
   qed (insert N, auto)
   show ?t1 ?t2 ?t3
     unfolding reduced_def
@@ -2754,7 +3171,8 @@
 lemma reduced_labelling_unique:
   fixes x :: "nat \<Rightarrow> nat"
   assumes "r \<le> n"
-    "\<forall>i. 1 \<le> i \<and> i < r + 1 \<longrightarrow> (label x i = 0)" "(r = n) \<or> (label x (r + 1) \<noteq> 0)"
+    and "\<forall>i. 1 \<le> i \<and> i < r + 1 \<longrightarrow> label x i = 0"
+    and "r = n \<or> label x (r + 1) \<noteq> 0"
   shows "reduced label n x = r"
   apply (rule le_antisym)
   apply (rule_tac[!] ccontr)
@@ -2765,13 +3183,16 @@
   done
 
 lemma reduced_labelling_zero:
-  assumes "j\<in>{1..n}" "label x j = 0"
+  assumes "j \<in> {1..n}"
+    and "label x j = 0"
   shows "reduced label n x \<noteq> j - 1"
   using reduced_labelling[of label n x]
-  using assms by fastforce
+  using assms
+  by fastforce
 
 lemma reduced_labelling_nonzero:
-  assumes "j\<in>{1..n}" "label x j \<noteq> 0"
+  assumes "j\<in>{1..n}"
+    and "label x j \<noteq> 0"
   shows "reduced label n x < j"
   using assms and reduced_labelling[of label n x]
   apply (erule_tac x=j in allE)
@@ -2789,14 +3210,18 @@
 
 lemma complete_face_top:
   assumes "\<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"
-  shows "((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)) \<longleftrightarrow>
-  ((reduced lab (n + 1)) ` f = {0..n}) \<and> (\<forall>x\<in>f. x (n + 1) = p)" (is "?l = ?r")
+    and "\<forall>x\<in>f. \<forall>j\<in>{1..n+1}. x j = p \<longrightarrow> lab x j = 1"
+  shows "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)) \<longleftrightarrow>
+    reduced lab (n + 1) ` f = {0..n} \<and> (\<forall>x\<in>f. x (n + 1) = p)"
+    (is "?l = ?r")
 proof
   assume ?l (is "?as \<and> (?a \<or> ?b)")
   then show ?r
     apply -
-    apply (rule, erule conjE, assumption)
+    apply rule
+    apply (erule conjE)
+    apply assumption
   proof (cases ?a)
     case True
     then guess j .. note j = this
@@ -2813,13 +3238,17 @@
         apply auto
         done
     }
-    moreover have "j - 1 \<in> {0..n}" using j by auto
+    moreover have "j - 1 \<in> {0..n}"
+      using j by auto
     then guess y unfolding `?l`[THEN conjunct1,symmetric] and image_iff .. note y = this
-    ultimately have False by auto
-    then show "\<forall>x\<in>f. x (n + 1) = p" by auto
+    ultimately have False
+      by auto
+    then show "\<forall>x\<in>f. x (n + 1) = p"
+      by auto
   next
     case False
-    then have ?b using `?l` by blast
+    then have ?b using `?l`
+      by blast
     then guess j .. note j = this
     {
       fix x
@@ -2834,35 +3263,45 @@
     } note * = this
     have "j = n + 1"
     proof (rule ccontr)
-      case goal1
-      then have "j < n + 1" using j by auto
+      assume "\<not> ?thesis"
+      then have "j < n + 1"
+        using j by auto
       moreover
-      have "n \<in> {0..n}" by auto
+      have "n \<in> {0..n}"
+        by auto
       then guess y unfolding `?l`[THEN conjunct1,symmetric] image_iff ..
-      ultimately show False using *[of y] by auto
+      ultimately show False
+        using *[of y] by auto
     qed
-    then show "\<forall>x\<in>f. x (n + 1) = p" using j by auto
+    then show "\<forall>x\<in>f. x (n + 1) = p"
+      using j by auto
   qed
-qed(auto)
+qed auto
 
 
-subsection {* Hence we get just about the nice induction. *}
+text {* Hence we get just about the nice induction. *}
 
 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})})"
+  assumes "0 < p"
+    and "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> x j = 0 \<longrightarrow> lab x j = 0"
+    and "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> x j = p \<longrightarrow> lab x j = 1"
+    and "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
+    "\<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
+    apply rule
+    apply (rule *)
+    apply (rule reduced_labelling)
     apply (rule *(1)[OF assms(4)])
     apply (rule set_eqI)
     unfolding mem_Collect_eq
-    apply (rule, erule conjE)
+    apply rule
+    apply (erule conjE)
     defer
     apply rule
   proof -
@@ -2870,16 +3309,22 @@
     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
+      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
+      using assms(2)
+      using as(1)[unfolded ksimplex_def]
+      by auto
     {
       fix x
       assume "x \<in> f"
       then have "reduced lab (n + 1) x < n + 1"
         apply -
         apply (rule reduced_labelling_nonzero)
-        defer using assms(3) using as(1)[unfolded ksimplex_def]
+        defer
+        using assms(3)
+        using as(1)[unfolded ksimplex_def]
         apply auto
         done
       then have "reduced lab (n + 1) x = reduced lab n x"
@@ -2911,11 +3356,7 @@
     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)+)
-      done
-    note sa = this
+    then guess a by (elim exE conjE) note sa = this
     {
       fix x
       assume "x \<in> f"
@@ -2951,19 +3392,22 @@
         apply auto
         done
       moreover
-      have "j - 1 \<in> {0..n}" using `j\<in>{1..n+1}` by auto
+      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
-      then show ?thesis by auto
+      then show ?thesis
+        by auto
     next
       case False
       then have "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p"
         using sa(5) by fastforce then guess j .. note j=this
       then show ?thesis
       proof (cases "j = n + 1")
-        case False then have *: "j \<in> {1..n}"
+        case False
+        then have *: "j \<in> {1..n}"
           using j by auto
         then have "\<And>x. x \<in> f \<Longrightarrow> reduced lab n x < j"
           apply (rule reduced_labelling_nonzero)
@@ -2978,58 +3422,72 @@
             unfolding sa
             apply auto
             done
-          then show "lab x j \<noteq> 0" by auto
+          then show "lab x j \<noteq> 0"
+            by auto
         qed
-        moreover have "j \<in> {0..n}" using * by auto
+        moreover have "j \<in> {0..n}"
+          using * by auto
         ultimately have False
           unfolding part1[symmetric]
           using * unfolding image_iff
           by auto
-        then show ?thesis by auto
+        then show ?thesis
+          by auto
       qed auto
     qed
     then show "ksimplex p n f"
-      using as unfolding simplex_top_face[OF assms(1) *,symmetric] by auto
+      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)"
-                  "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<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 (Suc n) s \<and>((reduced lab (Suc n)) `  s = {0..Suc n})})"
-  using assms unfolding Suc_eq_plus1 by(rule kuhn_induction)
+  assumes "0 < p"
+    and "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> x j = 0 \<longrightarrow> lab x j = 0"
+    and "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> x j = p \<longrightarrow> lab x j = 1"
+    and "odd (card {f. ksimplex p n f \<and> reduced lab n ` f = {0..n}})"
+  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. *}
+text {* And so we get the final combinatorial result. *}
 
-lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}" (is "?l = ?r")
+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
-  then show ?r using a by auto
+    using ksimplexD(5)[OF l, rule_format, OF a(1)]
+    by rule auto
+  then show ?r
+    using a by auto
 next
   assume r: ?r
-  show ?l unfolding r ksimplex_eq by auto
+  show ?l
+    unfolding r ksimplex_eq by auto
 qed
 
 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})})"
+  assumes "0 < p"
+    and "\<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"
+    and "\<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})}"
+  let ?M = "\<lambda>n. {s. ksimplex p n s \<and> reduced lab n ` s = {0..n}}"
   {
     case 0
-    have *: "?M 0 = {{(\<lambda>x. p)}}"
+    have *: "?M 0 = {{\<lambda>x. p}}"
       unfolding ksimplex_0 by auto
-    show ?case unfolding * by auto
+    show ?case
+      unfolding * by auto
   next
     case (Suc n)
     have "odd (card (?M n))"
@@ -3047,18 +3505,22 @@
 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))"
+  fixes n p :: nat
+  assumes "0 < p"
+    and "0 < n"
+    and "\<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)"
+    and "\<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)"
+    and "\<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)"
+    and "\<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 \<noteq> 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"
+  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])
@@ -3070,16 +3532,17 @@
     apply (rule ccontr)
     apply auto
     done
-  then have "?A \<noteq> {}" unfolding card_eq_0_iff by auto
+  then have "?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
+  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}"
+    assume "i \<in> {1..n}"
     then have "a i + 1 \<le> p"
       apply -
       apply (rule order_trans[of _ "b i"])
@@ -3091,10 +3554,12 @@
       apply (drule_tac bspec[OF _ ab(2)])+
       apply auto
       done
-    then show "a i < p" by auto
+    then show "a i < p"
+      by auto
   next
     case goal2
-    then have "i \<in> reduced label n ` s" using s by auto
+    then have "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
@@ -3116,7 +3581,7 @@
         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"
+      show "a j \<le> u j \<and> u j \<le> a j + 1" and "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 -
@@ -3131,38 +3596,45 @@
 qed
 
 
-subsection {* The main result for the unit cube. *}
+subsection {* The main result for the unit cube *}
 
 lemma kuhn_labelling_lemma':
-  assumes "(\<forall>x::nat\<Rightarrow>real. P x \<longrightarrow> P (f x))"  "\<forall>x. P x \<longrightarrow> (\<forall>i::nat. Q i \<longrightarrow> 0 \<le> x i \<and> x i \<le> 1)"
+  assumes "(\<forall>x::nat\<Rightarrow>real. P x \<longrightarrow> P (f x))"
+    and "\<forall>x. P x \<longrightarrow> (\<forall>i::nat. Q i \<longrightarrow> 0 \<le> x i \<and> x i \<le> 1)"
   shows "\<exists>l. (\<forall>x i. l x i \<le> (1::nat)) \<and>
-             (\<forall>x i. P x \<and> Q i \<and> (x i = 0) \<longrightarrow> (l x i = 0)) \<and>
-             (\<forall>x i. P x \<and> Q i \<and> (x i = 1) \<longrightarrow> (l x i = 1)) \<and>
-             (\<forall>x i. P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x i \<le> f(x) i) \<and>
-             (\<forall>x i. P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x) i \<le> x i)"
+             (\<forall>x i. P x \<and> Q i \<and> x i = 0 \<longrightarrow> l x i = 0) \<and>
+             (\<forall>x i. P x \<and> Q i \<and> x i = 1 \<longrightarrow> l x i = 1) \<and>
+             (\<forall>x i. P x \<and> Q i \<and> l x i = 0 \<longrightarrow> x i \<le> f x i) \<and>
+             (\<forall>x i. P x \<and> Q i \<and> l x i = 1 \<longrightarrow> f x i \<le> x i)"
 proof -
-  have and_forall_thm: "\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)" by auto
-  have *: "\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> (x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x)"
+  have and_forall_thm: "\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)"
+    by auto
+  have *: "\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x"
     by auto
   show ?thesis
     unfolding and_forall_thm
     apply (subst choice_iff[symmetric])+
-  proof (rule, rule)
+    apply rule
+    apply rule
+  proof -
     case goal1
-    let ?R = "\<lambda>y. (P x \<and> Q xa \<and> x xa = 0 \<longrightarrow> y = (0::nat)) \<and>
+    let ?R = "\<lambda>y::nat.
+      (P x \<and> Q xa \<and> x xa = 0 \<longrightarrow> y = 0) \<and>
       (P x \<and> Q xa \<and> x xa = 1 \<longrightarrow> y = 1) \<and>
       (P x \<and> Q xa \<and> y = 0 \<longrightarrow> x xa \<le> (f x) xa) \<and>
       (P x \<and> Q xa \<and> y = 1 \<longrightarrow> (f x) xa \<le> x xa)"
     {
-      assume "P x" "Q xa"
-      then have "0 \<le> (f x) xa \<and> (f x) xa \<le> 1"
+      assume "P x" and "Q xa"
+      then have "0 \<le> f x xa \<and> f x xa \<le> 1"
         using assms(2)[rule_format,of "f x" xa]
         apply (drule_tac assms(1)[rule_format])
         apply auto
         done
     }
-    then have "?R 0 \<or> ?R 1" by auto
-    then show ?case by auto
+    then have "?R 0 \<or> ?R 1"
+      by auto
+    then show ?case
+      by auto
   qed
 qed
 
@@ -3193,22 +3665,26 @@
     abs (f x \<bullet> i - x \<bullet> i) \<le> norm (f y - f x) + norm (y - x)"
   proof safe
     fix x y :: 'a
-    assume x: "x\<in>{0..\<Sum>Basis}"
-    assume y: "y\<in>{0..\<Sum>Basis}"
+    assume x: "x \<in> {0..\<Sum>Basis}"
+    assume y: "y \<in> {0..\<Sum>Basis}"
     fix i
     assume i: "label x i \<noteq> label y i" "i \<in> Basis"
     have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
       abs (fx - x) \<le> abs (fy - fx) + abs (y - x)" by auto
-    have "\<bar>(f x - x) \<bullet> i\<bar> \<le> abs((f y - f x)\<bullet>i) + abs((y - x)\<bullet>i)"
+    have "\<bar>(f x - x) \<bullet> i\<bar> \<le> abs ((f y - f x)\<bullet>i) + abs ((y - x)\<bullet>i)"
       unfolding inner_simps
       apply (rule *)
       apply (cases "label x i = 0")
-      apply (rule disjI1, rule)
+      apply (rule disjI1)
+      apply rule
       prefer 3
-    proof (rule disjI2, rule)
+      apply (rule disjI2)
+      apply rule
+    proof -
       assume lx: "label x i = 0"
       then have ly: "label y i = 1"
-        using i label(1)[of i y] by auto
+        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 x y lx i(2)
@@ -3221,8 +3697,9 @@
         done
     next
       assume "label x i \<noteq> 0"
-      then have l:"label x i = 1" "label y i = 0"
-        using i label(1)[of i x] label(1)[of i y] by auto
+      then have l: "label x i = 1" "label y i = 0"
+        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 x y l i(2)
@@ -3242,11 +3719,13 @@
       unfolding inner_simps .
   qed
   have "\<exists>e>0. \<forall>x\<in>{0..\<Sum>Basis}. \<forall>y\<in>{0..\<Sum>Basis}. \<forall>z\<in>{0..\<Sum>Basis}. \<forall>i\<in>Basis.
-    norm(x - z) < e \<and> norm(y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow> abs((f(z) - z)\<bullet>i) < d / (real n)"
+    norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow>
+      abs ((f(z) - z)\<bullet>i) < d / (real n)"
   proof -
-    have d':"d / real n / 8 > 0"
+    have d': "d / real n / 8 > 0"
       apply (rule divide_pos_pos)+
-      using d(1) unfolding n_def
+      using d(1)
+      unfolding n_def
       apply (auto simp:  DIM_positive)
       done
     have *: "uniformly_continuous_on {0..\<Sum>Basis} f"
@@ -3260,25 +3739,32 @@
       show "0 < min (e / 2) (d / real n / 8)"
         using d' e by auto
       fix x y z i
-      assume as: "x \<in> {0..\<Sum>Basis}" "y \<in> {0..\<Sum>Basis}" "z \<in> {0..\<Sum>Basis}"
+      assume as:
+        "x \<in> {0..\<Sum>Basis}" "y \<in> {0..\<Sum>Basis}" "z \<in> {0..\<Sum>Basis}"
         "norm (x - z) < min (e / 2) (d / real n / 8)"
-        "norm (y - z) < min (e / 2) (d / real n / 8)" "label x i \<noteq> label y i"
-        and i: "i \<in> Basis"
+        "norm (y - z) < min (e / 2) (d / real n / 8)"
+        "label x i \<noteq> label y i"
+      assume i: "i \<in> Basis"
       have *: "\<And>z fz x fx n1 n2 n3 n4 d4 d :: real. abs(fx - x) \<le> n1 + n2 \<Longrightarrow>
-        abs(fx - fz) \<le> n3 \<Longrightarrow> abs(x - z) \<le> n4 \<Longrightarrow>
+        abs (fx - fz) \<le> n3 \<Longrightarrow> abs (x - z) \<le> n4 \<Longrightarrow>
         n1 < d4 \<Longrightarrow> n2 < 2 * d4 \<Longrightarrow> n3 < d4 \<Longrightarrow> n4 < d4 \<Longrightarrow>
-        (8 * d4 = d) \<Longrightarrow> abs(fz - z) < d" by auto
-      show "\<bar>(f z - z) \<bullet> i\<bar> < d / real n" unfolding inner_simps
+        (8 * d4 = d) \<Longrightarrow> abs(fz - z) < d"
+        by auto
+      show "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
+        unfolding inner_simps
       proof (rule *)
         show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y -f x) + norm (y - x)"
           apply (rule lem1[rule_format])
-          using as i apply auto
+          using as i
+          apply auto
           done
         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)"
-          unfolding inner_diff_left[symmetric] by(rule Basis_le_norm[OF i])+
-        have tria:"norm (y - x) \<le> norm (y - z) + norm (x - z)"
+          unfolding inner_diff_left[symmetric]  
+          by (rule Basis_le_norm[OF i])+
+        have tria: "norm (y - x) \<le> norm (y - z) + norm (x - z)"
           using dist_triangle[of y x z, unfolded dist_norm]
-          unfolding norm_minus_commute by auto
+          unfolding norm_minus_commute
+          by auto
         also have "\<dots> < e / 2 + e / 2"
           apply (rule add_strict_mono)
           using as(4,5)
@@ -3295,7 +3781,9 @@
           using as
           apply auto
           done
-        then show "norm (y - x) < 2 * (d / real n / 8)" using tria by auto
+        then show "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)
@@ -3313,7 +3801,8 @@
     using e(1) n
     apply auto
     done
-  then have "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)
@@ -3323,71 +3812,98 @@
   then have b'_Basis: "\<And>i. i \<in> Basis \<Longrightarrow> b' i \<in> {Suc 0 .. n}"
     unfolding bij_betw_def by (auto simp: set_eq_iff)
   have bb'[simp]:"\<And>i. i \<in> Basis \<Longrightarrow> b (b' i) = i"
-    unfolding b'_def using b by (auto simp: f_inv_into_f bij_betw_def)
+    unfolding b'_def
+    using b
+    by (auto simp: f_inv_into_f bij_betw_def)
   have b'b[simp]:"\<And>i. i \<in> {1..n} \<Longrightarrow> b' (b i) = i"
-    unfolding b'_def using b by (auto simp: inv_into_f_eq bij_betw_def)
-  have *: "\<And>x :: nat. x=0 \<or> x=1 \<longleftrightarrow> x\<le>1" by auto
+    unfolding b'_def
+    using b
+    by (auto simp: inv_into_f_eq bij_betw_def)
+  have *: "\<And>x :: nat. x = 0 \<or> x = 1 \<longleftrightarrow> x \<le> 1"
+    by auto
   have b'': "\<And>j. j \<in> {Suc 0..n} \<Longrightarrow> b j \<in> Basis"
     using b unfolding bij_betw_def by auto
   have q1: "0 < p" "0 < n"  "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow>
     (\<forall>i\<in>{1..n}. (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0 \<or>
                 (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
-    unfolding * using `p>0` `n>0` using label(1)[OF b''] by auto
+    unfolding *
+    using `p > 0` `n > 0`
+    using label(1)[OF b'']
+    by auto
   have q2: "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. x i = 0 \<longrightarrow>
       (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
     "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. x i = p \<longrightarrow>
       (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
-    apply (rule, rule, rule, rule)
+    apply rule
+    apply rule
+    apply rule
+    apply rule
     defer
-  proof (rule, rule, rule, rule)
+    apply rule
+    apply rule
+    apply rule
+    apply rule
+  proof -
     fix x i
     assume as: "\<forall>i\<in>{1..n}. x i \<le> p" "i \<in> {1..n}"
     {
       assume "x i = p \<or> x i = 0"
       have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> {0::'a..\<Sum>Basis}"
-        unfolding mem_interval using as b'_Basis
+        unfolding mem_interval
+        using as b'_Basis
         by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)
     }
     note cube = this
     {
       assume "x i = p"
       then show "(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1"
-        unfolding o_def using cube as `p>0`
+        unfolding o_def
+        using cube as `p > 0`
         by (intro label(3)) (auto simp add: b'')
     }
     {
       assume "x i = 0"
       then show "(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0"
-        unfolding o_def using cube as `p>0`
+        unfolding o_def using cube as `p > 0`
         by (intro label(2)) (auto simp add: b'')
     }
   qed
   guess q by (rule kuhn_lemma[OF q1 q2]) note q = this
   def z \<equiv> "(\<Sum>i\<in>Basis. (real (q (b' i)) / real p) *\<^sub>R i)::'a"
-  have "\<exists>i\<in>Basis. d / real n \<le> abs((f z - z)\<bullet>i)"
+  have "\<exists>i\<in>Basis. d / real n \<le> abs ((f z - z)\<bullet>i)"
   proof (rule ccontr)
     have "\<forall>i\<in>Basis. q (b' i) \<in> {0..p}"
-      using q(1) b' by (auto intro: less_imp_le simp: bij_betw_def)
-    then have "z\<in>{0..\<Sum>Basis}"
-      unfolding z_def mem_interval using b'_Basis
+      using q(1) b'
+      by (auto intro: less_imp_le simp: bij_betw_def)
+    then have "z \<in> {0..\<Sum>Basis}"
+      unfolding z_def mem_interval
+      using b'_Basis
       by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)
-    then have d_fz_z:"d \<le> norm (f z - z)" by (rule d)
-    case goal1
+    then have d_fz_z: "d \<le> norm (f z - z)"
+      by (rule d)
+    assume "\<not> ?thesis"
     then have as: "\<forall>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar> < d / real n"
-      using `n > 0` by (auto simp add: not_le inner_simps)
+      using `n > 0`
+      by (auto simp add: not_le inner_simps)
     have "norm (f z - z) \<le> (\<Sum>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar>)"
-      unfolding inner_diff_left[symmetric] by(rule norm_le_l1)
+      unfolding inner_diff_left[symmetric]
+      by (rule norm_le_l1)
     also have "\<dots> < (\<Sum>(i::'a) \<in> Basis. d / real n)"
       apply (rule setsum_strict_mono)
-      using as apply auto
+      using as
+      apply auto
       done
     also have "\<dots> = d"
-      using DIM_positive[where 'a='a] by (auto simp: real_eq_of_nat n_def)
-    finally show False using d_fz_z by auto
+      using DIM_positive[where 'a='a]
+      by (auto simp: real_eq_of_nat n_def)
+    finally show False
+      using d_fz_z by auto
   qed
   then guess i .. note i = this
   have *: "b' i \<in> {1..n}"
-    using i using b'[unfolded bij_betw_def] by auto
+    using i
+    using b'[unfolded bij_betw_def]
+    by auto
   guess r using q(2)[rule_format,OF *] ..
   then guess s by (elim exE conjE) note rs = this[rule_format]
   have b'_im: "\<And>i. i \<in> Basis \<Longrightarrow>  b' i \<in> {1..n}"
@@ -3400,59 +3916,68 @@
     apply (auto simp add: Suc_le_eq)
     done
   then have "r' \<in> {0..\<Sum>Basis}"
-    unfolding r'_def mem_interval using b'_Basis
+    unfolding r'_def mem_interval
+    using b'_Basis
     by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)
   def s' \<equiv> "(\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i)::'a"
-  have "\<And>i. i\<in>Basis \<Longrightarrow> s (b' i) \<le> p"
+  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)
     done
   then have "s' \<in> {0..\<Sum>Basis}"
-    unfolding s'_def mem_interval using b'_Basis
+    unfolding s'_def mem_interval
+    using b'_Basis
     by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)
   have "z \<in> {0..\<Sum>Basis}"
-    unfolding z_def mem_interval using b'_Basis q(1)[rule_format,OF b'_im] `p>0`
+    unfolding z_def mem_interval
+    using b'_Basis q(1)[rule_format,OF b'_im] `p > 0`
     by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
-  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)"
+  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)
       done
-    also have "\<dots> < e * real p" using p `e>0` `p>0`
+    also have "\<dots> < e * real p"
+      using p `e > 0` `p > 0`
       by (auto simp add: field_simps n_def real_of_nat_def)
     finally have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) < e * real p" .
   }
   moreover
-  { have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
+  {
+    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)
       done
-    also have "\<dots> < e * real p" using p `e > 0` `p > 0`
+    also have "\<dots> < e * real p"
+      using p `e > 0` `p > 0`
       by (auto simp add: field_simps n_def real_of_nat_def)
     finally have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) < e * real p" .
   }
   ultimately
-  have "norm (r' - z) < e" "norm (s' - z) < e"
+  have "norm (r' - z) < e" and "norm (s' - z) < e"
     unfolding r'_def s'_def z_def
-    using `p>0`
+    using `p > 0`
     apply (rule_tac[!] le_less_trans[OF norm_le_l1])
     apply (auto simp add: field_simps setsum_divide_distrib[symmetric] inner_diff_left)
     done
   then have "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
-    using rs(3) i unfolding r'_def[symmetric] s'_def[symmetric] o_def bb'
+    using rs(3) i
+    unfolding r'_def[symmetric] s'_def[symmetric] o_def bb'
     by (intro e(2)[OF `r'\<in>{0..\<Sum>Basis}` `s'\<in>{0..\<Sum>Basis}` `z\<in>{0..\<Sum>Basis}`]) auto
-  then show False using i by auto
+  then show False
+    using i by auto
 qed
 
 
-subsection {* Retractions. *}
+subsection {* Retractions *}
 
-definition "retraction s t r \<longleftrightarrow>
-  t \<subseteq> s \<and> continuous_on s r \<and> (r ` s \<subseteq> t) \<and> (\<forall>x\<in>t. r x = x)"
+definition "retraction s t r \<longleftrightarrow> t \<subseteq> s \<and> continuous_on s r \<and> r ` s \<subseteq> t \<and> (\<forall>x\<in>t. r x = x)"
 
 definition retract_of (infixl "retract'_of" 12)
   where "(t retract_of s) \<longleftrightarrow> (\<exists>r. retraction s t r)"
@@ -3460,14 +3985,15 @@
 lemma retraction_idempotent: "retraction s t r \<Longrightarrow> x \<in> s \<Longrightarrow>  r (r x) = r x"
   unfolding retraction_def by auto
 
-subsection {*preservation of fixpoints under (more general notion of) retraction. *}
+subsection {* Preservation of fixpoints under (more general notion of) retraction *}
 
 lemma invertible_fixpoint_property:
   fixes s :: "'a::euclidean_space set"
     and t :: "'b::euclidean_space set"
   assumes "continuous_on t i"
     and "i ` t \<subseteq> s"
-    and "continuous_on s r" "r ` s \<subseteq> t"
+    and "continuous_on s r"
+    and "r ` s \<subseteq> t"
     and "\<forall>y\<in>t. r (i y) = y"
     and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
     and "continuous_on t g"
@@ -3475,10 +4001,12 @@
   obtains y where "y \<in> t" and "g y = y"
 proof -
   have "\<exists>x\<in>s. (i \<circ> g \<circ> r) x = x"
-    apply (rule assms(6)[rule_format], rule)
+    apply (rule assms(6)[rule_format])
+    apply rule
     apply (rule continuous_on_compose assms)+
-    apply ((rule continuous_on_subset)?,rule assms)+
-    using assms(2,4,8) unfolding image_compose
+    apply ((rule continuous_on_subset)?, rule assms)+
+    using assms(2,4,8)
+    unfolding image_compose
     apply auto
     apply blast
     done
@@ -3518,7 +4046,7 @@
 qed
 
 lemma retract_fixpoint_property:
-  fixes f :: "'a::euclidean_space => 'b::euclidean_space"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
     and s :: "'a set"
   assumes "t retract_of s"
     and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
@@ -3539,7 +4067,7 @@
 qed
 
 
-subsection {*So the Brouwer theorem for any set with nonempty interior. *}
+subsection {* The Brouwer theorem for any set with nonempty interior *}
 
 lemma brouwer_weak:
   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'a::ordered_euclidean_space"
@@ -3571,13 +4099,13 @@
 qed
 
 
-subsection {* And in particular for a closed ball. *}
+text {* And in particular for a closed ball. *}
 
 lemma brouwer_ball:
   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'a"
   assumes "e > 0"
     and "continuous_on (cball a e) f"
-    and "f ` (cball a e) \<subseteq> cball a e"
+    and "f ` cball a e \<subseteq> cball a e"
   obtains x where "x \<in> cball a e" and "f x = x"
   using brouwer_weak[OF compact_cball convex_cball, of a e f]
   unfolding interior_cball ball_eq_empty
@@ -3597,7 +4125,8 @@
   obtains x where "x \<in> s" and "f x = x"
 proof -
   have "\<exists>e>0. s \<subseteq> cball 0 e"
-    using compact_imp_bounded[OF assms(1)] unfolding bounded_pos
+    using compact_imp_bounded[OF assms(1)]
+    unfolding bounded_pos
     apply (erule_tac exE)
     apply (rule_tac x=b in exI)
     apply (auto simp add: dist_norm)
@@ -3665,7 +4194,8 @@
   then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
     by (auto simp add: algebra_simps)
   then have "a = x"
-    unfolding scaleR_left_distrib[symmetric] by auto
+    unfolding scaleR_left_distrib[symmetric]
+    by auto
   then show False
     using x assms by auto
 qed
@@ -3697,7 +4227,7 @@
   fixes a b u v x :: "'a::ordered_euclidean_space"
   assumes "x \<in> {a..b}"
     and "{u..v} \<noteq> {}"
-  shows "interval_bij (a,b) (u,v) x \<in> {u..v}"
+  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)
   apply safe
 proof -
diff -r 4b9894aad605 -r 63892cfef47f src/HOL/Multivariate_Analysis/Operator_Norm.thy
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Tue Sep 17 21:20:55 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Wed Sep 18 00:11:15 2013 +0200
@@ -20,7 +20,8 @@
   {
     fix x :: "'a"
     assume x: "norm x = 1"
-    from H[rule_format, of x] x have "norm (f x) \<le> b" by simp
+    from H[rule_format, of x] x have "norm (f x) \<le> b"
+      by simp
   }
   then show ?lhs by blast
 next
@@ -41,16 +42,21 @@
     moreover
     {
       assume x0: "x \<noteq> 0"
-      then have n0: "norm x \<noteq> 0" by (metis norm_eq_zero)
+      then have n0: "norm x \<noteq> 0"
+        by (metis norm_eq_zero)
       let ?c = "1/ norm x"
-      have "norm (?c *\<^sub>R x) = 1" using x0 by (simp add: n0)
-      with H have "norm (f (?c *\<^sub>R x)) \<le> b" by blast
+      have "norm (?c *\<^sub>R x) = 1"
+        using x0 by (simp add: n0)
+      with H have "norm (f (?c *\<^sub>R x)) \<le> b"
+        by blast
       then have "?c * norm (f x) \<le> b"
         by (simp add: linear_cmul[OF lf])
       then have "norm (f x) \<le> b * norm x"
-        using n0 norm_ge_zero[of x] by (auto simp add: field_simps)
+        using n0 norm_ge_zero[of x]
+        by (auto simp add: field_simps)
     }
-    ultimately have "norm (f x) \<le> b * norm x" by blast
+    ultimately have "norm (f x) \<le> b * norm x"
+      by blast
   }
   then show ?rhs by blast
 qed
@@ -64,30 +70,34 @@
   let ?S = "{norm (f x) |x. norm x = 1}"
   have "norm (f (SOME i. i \<in> Basis)) \<in> ?S"
     by (auto intro!: exI[of _ "SOME i. i \<in> Basis"] norm_Basis SOME_Basis)
-  then have Se: "?S \<noteq> {}" by auto
+  then have Se: "?S \<noteq> {}"
+    by auto
   from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
-    unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)
+    unfolding norm_bound_generalize[OF lf, symmetric]
+    by (auto simp add: setle_def)
   from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
-  show "norm (f x) <= onorm f * norm x"
+  show "norm (f x) \<le> onorm f * norm x"
     apply -
     apply (rule spec[where x = x])
     unfolding norm_bound_generalize[OF lf, symmetric]
     apply (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
     done
-  show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
+  show "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
     using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
     unfolding norm_bound_generalize[OF lf, symmetric]
     by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
 qed
 
 lemma onorm_pos_le:
-  assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)"
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes lf: "linear f"
   shows "0 \<le> onorm f"
   using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "SOME i. i \<in> Basis"]]
   by (simp add: SOME_Basis)
 
 lemma onorm_eq_0:
-  assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes lf: "linear f"
   shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
   using onorm[OF lf]
   apply (auto simp add: onorm_pos_le)
@@ -97,9 +107,10 @@
   apply arith
   done
 
-lemma onorm_const: "onorm(\<lambda>x::'a::euclidean_space. (y::'b::euclidean_space)) = norm y"
+lemma onorm_const:
+  "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y"
 proof -
-  let ?f = "\<lambda>x::'a. (y::'b)"
+  let ?f = "\<lambda>x::'a. y::'b"
   have th: "{norm (?f x)| x. norm x = 1} = {norm y}"
     by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \<in> Basis"])
   show ?thesis
@@ -110,15 +121,18 @@
 qed
 
 lemma onorm_pos_lt:
-  assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
-  shows "0 < onorm f \<longleftrightarrow> ~(\<forall>x. f x = 0)"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes lf: "linear f"
+  shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)"
   unfolding onorm_eq_0[OF lf, symmetric]
   using onorm_pos_le[OF lf] by arith
 
 lemma onorm_compose:
-  assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)"
-    and lg: "linear (g::'k::euclidean_space \<Rightarrow> 'n::euclidean_space)"
-  shows "onorm (f o g) \<le> onorm f * onorm g"
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+    and g :: "'k::euclidean_space \<Rightarrow> 'n::euclidean_space"
+  assumes lf: "linear f"
+    and lg: "linear g"
+  shows "onorm (f \<circ> g) \<le> onorm f * onorm g"
     apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format])
     unfolding o_def
     apply (subst mult_assoc)
@@ -130,19 +144,22 @@
     done
 
 lemma onorm_neg_lemma:
-  assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes lf: "linear f"
   shows "onorm (\<lambda>x. - f x) \<le> onorm f"
   using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]
   unfolding norm_minus_cancel by metis
 
 lemma onorm_neg:
-  assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes lf: "linear f"
   shows "onorm (\<lambda>x. - f x) = onorm f"
   using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]]
   by simp
 
 lemma onorm_triangle:
-  assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)"
+  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes lf: "linear f"
     and lg: "linear g"
   shows "onorm (\<lambda>x. f x + g x) \<le> onorm f + onorm g"
   apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])
@@ -155,19 +172,25 @@
   done
 
 lemma onorm_triangle_le:
-  "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space) \<Longrightarrow>
-    linear g \<Longrightarrow> onorm f + onorm g \<le> e \<Longrightarrow> onorm (\<lambda>x. f x + g x) \<le> e"
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes "linear f"
+    and "linear g"
+    and "onorm f + onorm g \<le> e"
+  shows "onorm (\<lambda>x. f x + g x) \<le> e"
   apply (rule order_trans)
   apply (rule onorm_triangle)
-  apply assumption+
+  apply (rule assms)+
   done
 
 lemma onorm_triangle_lt:
-  "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space) \<Longrightarrow> linear g \<Longrightarrow>
-    onorm f + onorm g < e \<Longrightarrow> onorm(\<lambda>x. f x + g x) < e"
+  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes "linear f"
+    and "linear g"
+    and "onorm f + onorm g < e"
+  shows "onorm (\<lambda>x. f x + g x) < e"
   apply (rule order_le_less_trans)
   apply (rule onorm_triangle)
-  apply assumption+
+  apply (rule assms)+
   done
 
 end