diff -r 69a0bdfc7fa5 -r 0dc28fd72c7d src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Aug 30 23:41:09 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Aug 31 00:39:59 2013 +0200
@@ -20,17 +20,17 @@
 lemma linear_scaleR: "linear (\<lambda>x. scaleR c x)"
   by (simp add: linear_def scaleR_add_right)
 
-lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>(x::'a::real_vector). scaleR c x)"
+lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>x::'a::real_vector. scaleR c x)"
   by (simp add: inj_on_def)
 
 lemma linear_add_cmul:
   assumes "linear f"
-  shows "f(a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x +  b *\<^sub>R f y"
+  shows "f (a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x +  b *\<^sub>R f y"
   using linear_add[of f] linear_cmul[of f] assms by simp
 
 lemma mem_convex_2:
-  assumes "convex S" "x : S" "y : S" "u>=0" "v>=0" "u+v=1"
-  shows "(u *\<^sub>R x + v *\<^sub>R y) : S"
+  assumes "convex S" "x \<in> S" "y \<in> S" "u \<ge> 0" "v \<ge> 0" "u + v = 1"
+  shows "u *\<^sub>R x + v *\<^sub>R y \<in> S"
   using assms convex_def[of S] by auto
 
 lemma mem_convex_alt:
@@ -54,14 +54,14 @@
 proof -
   {
     fix a
-    assume a: "a : S" "f a : span (f ` S - {f a})"
+    assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
     have eq: "f ` S - {f a} = f ` (S - {a})"
       using fi a span_inc by (auto simp add: inj_on_def)
-    from a have "f a : f ` span (S -{a})"
-      unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast
-    moreover have "span (S -{a}) <= span S"
-      using span_mono[of "S-{a}" S] by auto
-    ultimately have "a : span (S -{a})"
+    from a have "f a \<in> f ` span (S -{a})"
+      unfolding eq span_linear_image [OF lf, of "S - {a}"] by blast
+    moreover have "span (S - {a}) \<subseteq> span S"
+      using span_mono[of "S - {a}" S] by auto
+    ultimately have "a \<in> span (S - {a})"
       using fi a span_inc by (auto simp add: inj_on_def)
     with a(1) iS have False
       by (simp add: dependent_def)
@@ -71,12 +71,12 @@
 qed
 
 lemma dim_image_eq:
-  fixes f :: "'n::euclidean_space => 'm::euclidean_space"
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes lf: "linear f"
     and fi: "inj_on f (span S)"
-  shows "dim (f ` S) = dim (S::('n::euclidean_space) set)"
+  shows "dim (f ` S) = dim (S:: 'n::euclidean_space set)"
 proof -
-  obtain B where B_def: "B \<subseteq> S & independent B & S \<subseteq> span B & card B = dim S"
+  obtain B where B_def: "B \<subseteq> S \<and> independent B \<and> S \<subseteq> span B \<and> card B = dim S"
     using basis_exists[of S] by auto
   then have "span S = span B"
     using span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto
@@ -119,7 +119,7 @@
   shows "(\<Sum>i\<in>d. f i *\<^sub>R i) = (x::'a::euclidean_space) \<longleftrightarrow>
     (\<forall>i\<in>Basis. (i \<in> d \<longrightarrow> f i = x \<bullet> i) \<and> (i \<notin> d \<longrightarrow> x \<bullet> i = 0))"
 proof -
-  have *: "\<And>x a b P. x * (if P then a else b) = (if P then x*a else x*b)"
+  have *: "\<And>x a b P. x * (if P then a else b) = (if P then x * a else x * b)"
     by auto
   have **: "finite d"
     by (auto intro: finite_subset[OF assms])
@@ -140,46 +140,46 @@
   {
     fix x :: "'n::euclidean_space"
     def y \<equiv> "(e / norm x) *\<^sub>R x"
-    then have "y : cball 0 e"
+    then have "y \<in> cball 0 e"
       using cball_def dist_norm[of 0 y] assms by auto
-    moreover have *: "x = (norm x/e) *\<^sub>R y"
+    moreover have *: "x = (norm x / e) *\<^sub>R y"
       using y_def assms by simp
     moreover from * have "x = (norm x/e) *\<^sub>R y"
       by auto
-    ultimately have "x : span (cball 0 e)"
+    ultimately have "x \<in> span (cball 0 e)"
       using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"] by auto
   }
-  then have "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)"
+  then have "span (cball 0 e) = (UNIV :: 'n::euclidean_space set)"
     by auto
   then show ?thesis
     using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp add: dim_UNIV)
 qed
 
 lemma indep_card_eq_dim_span:
-  fixes B :: "('n::euclidean_space) set"
+  fixes B :: "'n::euclidean_space set"
   assumes "independent B"
-  shows "finite B & card B = dim (span B)"
+  shows "finite B \<and> card B = dim (span B)"
   using assms basis_card_eq_dim[of B "span B"] span_inc by auto
 
-lemma setsum_not_0: "setsum f A \<noteq> 0 \<Longrightarrow> \<exists> a\<in>A. f a \<noteq> 0"
+lemma setsum_not_0: "setsum f A \<noteq> 0 \<Longrightarrow> \<exists>a \<in> A. f a \<noteq> 0"
   by (rule ccontr) auto
 
 lemma translate_inj_on:
-  fixes A :: "('a::ab_group_add) set"
-  shows "inj_on (\<lambda>x. a+x) A"
+  fixes A :: "'a::ab_group_add set"
+  shows "inj_on (\<lambda>x. a + x) A"
   unfolding inj_on_def by auto
 
 lemma translation_assoc:
   fixes a b :: "'a::ab_group_add"
-  shows "(\<lambda>x. b+x) ` ((\<lambda>x. a+x) ` S) = (\<lambda>x. (a+b)+x) ` S"
+  shows "(\<lambda>x. b + x) ` ((\<lambda>x. a + x) ` S) = (\<lambda>x. (a + b) + x) ` S"
   by auto
 
 lemma translation_invert:
   fixes a :: "'a::ab_group_add"
-  assumes "(\<lambda>x. a+x) ` A = (\<lambda>x. a+x) ` B"
+  assumes "(\<lambda>x. a + x) ` A = (\<lambda>x. a + x) ` B"
   shows "A = B"
 proof -
-  have "(\<lambda>x. -a+x) ` ((\<lambda>x. a+x) ` A) = (\<lambda>x. -a+x) ` ((\<lambda>x. a+x) ` B)"
+  have "(\<lambda>x. -a + x) ` ((\<lambda>x. a + x) ` A) = (\<lambda>x. - a + x) ` ((\<lambda>x. a + x) ` B)"
     using assms by auto
   then show ?thesis
     using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto
@@ -187,7 +187,7 @@
 
 lemma translation_galois:
   fixes a :: "'a::ab_group_add"
-  shows "T = ((\<lambda>x. a+x) ` S) \<longleftrightarrow> S = ((\<lambda>x. (-a)+x) ` T)"
+  shows "T = ((\<lambda>x. a + x) ` S) \<longleftrightarrow> S = ((\<lambda>x. (- a) + x) ` T)"
   using translation_assoc[of "-a" a S]
   apply auto
   using translation_assoc[of a "-a" T]
@@ -195,8 +195,8 @@
   done
 
 lemma translation_inverse_subset:
-  assumes "((%x. -a+x) ` V) \<le> (S :: 'n::ab_group_add set)"
-  shows "V \<le> ((%x. a+x) ` S)"
+  assumes "((\<lambda>x. - a + x) ` V) \<le> (S :: 'n::ab_group_add set)"
+  shows "V \<le> ((\<lambda>x. a + x) ` S)"
 proof -
   {
     fix x
@@ -272,23 +272,23 @@
   by (rule image_closure_subset)
 
 lemma closure_linear_image:
-  fixes f :: "('m::euclidean_space) \<Rightarrow> ('n::real_normed_vector)"
+  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::real_normed_vector"
   assumes "linear f"
   shows "f ` (closure S) \<le> closure (f ` S)"
   using assms unfolding linear_conv_bounded_linear
   by (rule closure_bounded_linear_image)
 
 lemma closure_injective_linear_image:
-  fixes f :: "('n::euclidean_space) \<Rightarrow> ('n::euclidean_space)"
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n::euclidean_space"
   assumes "linear f" "inj f"
   shows "f ` (closure S) = closure (f ` S)"
 proof -
-  obtain f' where f'_def: "linear f' \<and> f o f' = id \<and> f' o f = id"
+  obtain f' where f'_def: "linear f' \<and> f \<circ> f' = id \<and> f' \<circ> f = id"
     using assms linear_injective_isomorphism[of f] isomorphism_expand by auto
   then have "f' ` closure (f ` S) \<le> closure (S)"
     using closure_linear_image[of f' "f ` S"] image_compose[of f' f] by auto
-  then have "f ` f' ` closure (f ` S) \<le> f ` closure (S)" by auto
-  then have "closure (f ` S) \<le> f ` closure (S)"
+  then have "f ` f' ` closure (f ` S) \<le> f ` closure S" by auto
+  then have "closure (f ` S) \<le> f ` closure S"
     using image_compose[of f f' "closure (f ` S)"] f'_def by auto
   then show ?thesis using closure_linear_image[of f S] assms by auto
 qed
@@ -297,7 +297,7 @@
   by (rule closure_Times)
 
 lemma closure_scaleR:
-  fixes S :: "('a::real_normed_vector) set"
+  fixes S :: "'a::real_normed_vector set"
   shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)"
 proof
   show "(op *\<^sub>R c) ` (closure S) \<subseteq> closure ((op *\<^sub>R c) ` S)"
@@ -474,7 +474,7 @@
           using as(7) and `card s > 2`
           by (metis One_nat_def less_Suc0 Zero_not_Suc of_nat_1 of_nat_eq_iff numeral_2_eq_2)
       qed
-      then obtain x where x:"x\<in>s" "u x \<noteq> 1" by auto
+      then obtain x where x:"x \<in> s" "u x \<noteq> 1" by auto
 
       have c: "card (s - {x}) = card s - 1"
         apply (rule card_Diff_singleton)
@@ -807,7 +807,7 @@
 proof (rule, rule, erule exE, erule conjE)
   fix y v
   assume "y = a + v" "v \<in> span {x - a |x. x \<in> s}"
-  then obtain t u where obt:"finite t" "t \<subseteq> {x - a |x. x \<in> s}" "a + (\<Sum>v\<in>t. u v *\<^sub>R v) = y"
+  then obtain t u where obt: "finite t" "t \<subseteq> {x - a |x. x \<in> s}" "a + (\<Sum>v\<in>t. u v *\<^sub>R v) = y"
     unfolding span_explicit by auto
   def f \<equiv> "(\<lambda>x. x + a) ` t"
   have f: "finite f" "f \<subseteq> s" "(\<Sum>v\<in>f. u (v - a) *\<^sub>R (v - a)) = y - a"
@@ -817,7 +817,8 @@
   show "\<exists>sa u. finite sa \<and> sa \<noteq> {} \<and> sa \<subseteq> insert a s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y"
     apply (rule_tac x = "insert a f" in exI)
     apply (rule_tac x = "\<lambda>x. if x=a then 1 - setsum (\<lambda>x. u (x - a)) f else u (x - a)" in exI)
-    using assms and f unfolding setsum_clauses(2)[OF f(1)] and if_smult
+    using assms and f
+    unfolding setsum_clauses(2)[OF f(1)] and if_smult
     unfolding setsum_cases[OF f(1), of "\<lambda>x. x = a"]
     apply (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps *)
     done
@@ -832,26 +833,27 @@
 subsubsection {* Parallel affine sets *}
 
 definition affine_parallel :: "'a::real_vector set => 'a::real_vector set => bool"
-  where "affine_parallel S T = (? a. T = ((\<lambda>x. a + x) ` S))"
+  where "affine_parallel S T \<longleftrightarrow> (\<exists>a. T = (\<lambda>x. a + x) ` S)"
 
 lemma affine_parallel_expl_aux:
   fixes S T :: "'a::real_vector set"
-  assumes "\<forall>x. (x : S \<longleftrightarrow> (a+x) \<in> T)"
-  shows "T = ((\<lambda>x. a + x) ` S)"
+  assumes "\<forall>x. x \<in> S \<longleftrightarrow> a + x \<in> T"
+  shows "T = (\<lambda>x. a + x) ` S"
 proof -
   {
     fix x
-    assume "x : T"
-    then have "(-a)+x \<in> S" using assms by auto
-    then have "x : ((\<lambda>x. a + x) ` S)"
+    assume "x \<in> T"
+    then have "( - a) + x \<in> S"
+      using assms by auto
+    then have "x \<in> ((\<lambda>x. a + x) ` S)"
       using imageI[of "-a+x" S "(\<lambda>x. a+x)"] by auto
   }
-  moreover have "T >= ((\<lambda>x. a + x) ` S)"
+  moreover have "T \<ge> (\<lambda>x. a + x) ` S"
     using assms by auto
   ultimately show ?thesis by auto
 qed
 
-lemma affine_parallel_expl: "affine_parallel S T = (\<exists>a. \<forall>x. (x \<in> S \<longleftrightarrow> (a+x) \<in> T))"
+lemma affine_parallel_expl: "affine_parallel S T \<longleftrightarrow> (\<exists>a. \<forall>x. x \<in> S \<longleftrightarrow> a + x \<in> T)"
   unfolding affine_parallel_def
   using affine_parallel_expl_aux[of S _ T] by auto
 
@@ -873,7 +875,8 @@
 qed
 
 lemma affine_parallel_assoc:
-  assumes "affine_parallel A B" "affine_parallel B C"
+  assumes "affine_parallel A B"
+    and "affine_parallel B C"
   shows "affine_parallel A C"
 proof -
   from assms obtain ab where "B = (\<lambda>x. ab + x) ` A"
@@ -895,13 +898,13 @@
     assume xy: "x \<in> S" "y \<in> S" "(u :: real) + v = 1"
     then have "(a + x) \<in> ((\<lambda>x. a + x) ` S)" "(a + y) \<in> ((\<lambda>x. a + x) ` S)"
       by auto
-    then have h1: "u *\<^sub>R  (a+x) + v *\<^sub>R (a+y) \<in> ((\<lambda>x. a + x) ` S)"
+    then have h1: "u *\<^sub>R  (a + x) + v *\<^sub>R (a + y) \<in> (\<lambda>x. a + x) ` S"
       using xy assms unfolding affine_def by auto
-    have "u *\<^sub>R (a+x) + v *\<^sub>R (a+y) = (u+v) *\<^sub>R a + (u *\<^sub>R x + v *\<^sub>R y)"
+    have "u *\<^sub>R (a + x) + v *\<^sub>R (a + y) = (u + v) *\<^sub>R a + (u *\<^sub>R x + v *\<^sub>R y)"
       by (simp add: algebra_simps)
-    also have "...= a + (u *\<^sub>R x + v *\<^sub>R y)"
-      using `u+v=1` by auto
-    ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) : ((%x. a + x) ` S)"
+    also have "\<dots> = a + (u *\<^sub>R x + v *\<^sub>R y)"
+      using `u + v = 1` by auto
+    ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) \<in> (\<lambda>x. a + x) ` S"
       using h1 by auto
     then have "u *\<^sub>R x + v *\<^sub>R y : S" by auto
   }
@@ -910,10 +913,10 @@
 
 lemma affine_translation:
   fixes a :: "'a::real_vector"
-  shows "affine S \<longleftrightarrow> affine ((%x. a + x) ` S)"
+  shows "affine S \<longleftrightarrow> affine ((\<lambda>x. a + x) ` S)"
 proof -
-  have "affine S \<Longrightarrow> affine ((%x. a + x) ` S)"
-    using affine_translation_aux[of "-a" "((%x. a + x) ` S)"]
+  have "affine S \<Longrightarrow> affine ((\<lambda>x. a + x) ` S)"
+    using affine_translation_aux[of "-a" "((\<lambda>x. a + x) ` S)"]
     using translation_assoc[of "-a" a S] by auto
   then show ?thesis using affine_translation_aux by auto
 qed
@@ -923,9 +926,10 @@
   assumes "affine S" "affine_parallel S T"
   shows "affine T"
 proof -
-  from assms obtain a where "T=((%x. a + x) ` S)"
+  from assms obtain a where "T = (\<lambda>x. a + x) ` S"
     unfolding affine_parallel_def by auto
-  then show ?thesis using affine_translation assms by auto
+  then show ?thesis
+    using affine_translation assms by auto
 qed
 
 lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s"
@@ -934,7 +938,7 @@
 
 subsubsection {* Subspace parallel to an affine set *}
 
-lemma subspace_affine: "subspace S \<longleftrightarrow> (affine S \<and> 0 : S)"
+lemma subspace_affine: "subspace S \<longleftrightarrow> affine S \<and> 0 \<in> S"
 proof -
   have h0: "subspace S \<Longrightarrow> affine S \<and> 0 \<in> S"
     using subspace_imp_affine[of S] subspace_0 by auto
@@ -945,7 +949,7 @@
       fix x assume x_def: "x \<in> S"
       have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto
       moreover
-      have "(1-c) *\<^sub>R 0 + c *\<^sub>R x : S"
+      have "(1 - c) *\<^sub>R 0 + c *\<^sub>R x \<in> S"
         using affine_alt[of S] assm x_def by auto
       ultimately have "c *\<^sub>R x \<in> S" by auto
     }
@@ -1003,7 +1007,7 @@
   moreover have "0 \<in> L"
     using assms
     apply auto
-    using exI[of "(%x. x:S & -a+x=0)" a]
+    using exI[of "(\<lambda>x. x:S \<and> -a+x=0)" a]
     apply auto
     done
   ultimately show ?thesis
@@ -1016,7 +1020,7 @@
     and "affine_parallel A B"
   shows "A \<supseteq> B"
 proof -
-  from assms obtain a where a_def: "\<forall>x. (x \<in> A \<longleftrightarrow> (a+x) \<in> B)"
+  from assms obtain a where a_def: "\<forall>x. x \<in> A \<longleftrightarrow> a + x \<in> B"
     using affine_parallel_expl[of A B] by auto
   then have "-a \<in> A"
     using assms subspace_0[of B] by auto
@@ -1040,13 +1044,13 @@
 
 lemma affine_parallel_subspace:
   assumes "affine S" "S \<noteq> {}"
-  shows "\<exists>!L. subspace L & affine_parallel S L"
+  shows "\<exists>!L. subspace L \<and> affine_parallel S L"
 proof -
-  have ex: "\<exists>L. subspace L & affine_parallel S L"
+  have ex: "\<exists>L. subspace L \<and> affine_parallel S L"
     using assms parallel_subspace_explicit by auto
   {
     fix L1 L2
-    assume ass: "subspace L1 & affine_parallel S L1" "subspace L2 & affine_parallel S L2"
+    assume ass: "subspace L1 \<and> affine_parallel S L1" "subspace L2 \<and> affine_parallel S L2"
     then have "affine_parallel L1 L2"
       using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto
     then have "L1 = L2"
@@ -1059,7 +1063,7 @@
 subsection {* Cones *}
 
 definition cone :: "'a::real_vector set \<Rightarrow> bool"
-  where "cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *\<^sub>R x) \<in> s)"
+  where "cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. c *\<^sub>R x \<in> s)"
 
 lemma cone_empty[intro, simp]: "cone {}"
   unfolding cone_def by auto
@@ -1067,7 +1071,7 @@
 lemma cone_univ[intro, simp]: "cone UNIV"
   unfolding cone_def by auto
 
-lemma cone_Inter[intro]: "\<forall>s\<in>f. cone s \<Longrightarrow> cone(\<Inter> f)"
+lemma cone_Inter[intro]: "\<forall>s\<in>f. cone s \<Longrightarrow> cone (\<Inter>f)"
   unfolding cone_def by auto
 
 
@@ -1109,7 +1113,7 @@
 
 lemma cone_iff:
   assumes "S ~= {}"
-  shows "cone S \<longleftrightarrow> 0 \<in> S & (\<forall>c. c>0 \<longrightarrow> (op *\<^sub>R c) ` S = S)"
+  shows "cone S \<longleftrightarrow> 0 \<in> S & (\<forall>c. c > 0 \<longrightarrow> (op *\<^sub>R c) ` S = S)"
 proof -
   {
     assume "cone S"
@@ -1136,12 +1140,12 @@
       }
       ultimately have "(op *\<^sub>R c) ` S = S" by auto
     }
-    then have "0 \<in> S & (\<forall>c. c > 0 \<longrightarrow> (op *\<^sub>R c) ` S = S)"
+    then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (op *\<^sub>R c) ` S = S)"
       using `cone S` cone_contains_0[of S] assms by auto
   }
   moreover
   {
-    assume a: "0 \<in> S & (\<forall>c. c > 0 \<longrightarrow> (op *\<^sub>R c) ` S = S)"
+    assume a: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (op *\<^sub>R c) ` S = S)"
     {
       fix x
       assume "x \<in> S"
@@ -1170,16 +1174,17 @@
   shows "c *\<^sub>R x \<in> cone hull S"
   by (metis assms cone_cone_hull hull_inc mem_cone)
 
-lemma cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 & x \<in> S}" (is "?lhs = ?rhs")
+lemma cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
+  (is "?lhs = ?rhs")
 proof -
   {
     fix x
     assume "x \<in> ?rhs"
-    then obtain cx xx where x_def: "x = cx *\<^sub>R xx & (cx :: real) \<ge> 0 & xx \<in> S"
+    then obtain cx xx where x_def: "x = cx *\<^sub>R xx" "(cx :: real) \<ge> 0" "xx \<in> S"
       by auto
     fix c
     assume c_def: "(c :: real) \<ge> 0"
-    then have "c *\<^sub>R x = (c*cx) *\<^sub>R xx"
+    then have "c *\<^sub>R x = (c * cx) *\<^sub>R xx"
       using x_def by (simp add: algebra_simps)
     moreover
     have "c * cx \<ge> 0"
@@ -1205,8 +1210,10 @@
   {
     fix x
     assume "x \<in> ?rhs"
-    then obtain cx xx where x_def: "x = cx *\<^sub>R xx & (cx :: real) \<ge> 0 & xx \<in> S" by auto
-    then have "xx \<in> cone hull S" using hull_subset[of S] by auto
+    then obtain cx xx where x_def: "x = cx *\<^sub>R xx" "(cx :: real) \<ge> 0" "xx \<in> S"
+      by auto
+    then have "xx \<in> cone hull S"
+      using hull_subset[of S] by auto
     then have "x \<in> ?lhs"
       using x_def cone_cone_hull[of S] cone_def[of "cone hull S"] by auto
   }
@@ -1222,18 +1229,19 @@
   then show ?thesis by auto
 next
   case False
-  then have "0 \<in> S & (!c. c>0 --> op *\<^sub>R c ` S = S)"
+  then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` S = S)"
     using cone_iff[of S] assms by auto
-  then have "0 \<in> closure S & (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` closure S = closure S)"
+  then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` closure S = closure S)"
     using closure_subset by (auto simp add: closure_scaleR)
-  then show ?thesis using cone_iff[of "closure S"] by auto
+  then show ?thesis
+    using cone_iff[of "closure S"] by auto
 qed
 
 
 subsection {* Affine dependence and consequential theorems (from Lars Schewe) *}
 
 definition affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
-  where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> (affine hull (s - {x})))"
+  where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> affine hull (s - {x}))"
 
 lemma affine_dependent_explicit:
   "affine_dependent p \<longleftrightarrow>
@@ -1254,12 +1262,14 @@
   show "\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
     apply (rule_tac x="insert x s" in exI, rule_tac x="\<lambda>v. if v = x then - 1 else u v" in exI)
     unfolding if_smult and setsum_clauses(2)[OF as(2)] and setsum_delta_notmem[OF `x\<notin>s`] and as
-    using as apply auto
+    using as
+    apply auto
     done
 next
   fix s u v
   assume as: "finite s" "s \<subseteq> p" "setsum u s = 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" "v \<in> s" "u v \<noteq> 0"
-  have "s \<noteq> {v}" using as(3,6) by auto
+  have "s \<noteq> {v}"
+    using as(3,6) by auto
   then show "\<exists>x\<in>p. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p - {x} \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
     apply (rule_tac x=v in bexI)
     apply (rule_tac x="s - {v}" in exI)
@@ -1282,7 +1292,7 @@
     by auto
   assume ?lhs
   then obtain t u v where
-      "finite t" "t \<subseteq> s" "setsum u t = 0" "v\<in>t" "u v \<noteq> 0"  "(\<Sum>v\<in>t. u v *\<^sub>R v) = 0"
+    "finite t" "t \<subseteq> s" "setsum u t = 0" "v\<in>t" "u v \<noteq> 0"  "(\<Sum>v\<in>t. u v *\<^sub>R v) = 0"
     unfolding affine_dependent_explicit by auto
   then show ?rhs
     apply (rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
@@ -1292,7 +1302,8 @@
     done
 next
   assume ?rhs
-  then obtain u v where "setsum u s = 0"  "v\<in>s" "u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" by auto
+  then obtain u v where "setsum u s = 0"  "v\<in>s" "u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
+    by auto
   then show ?lhs unfolding affine_dependent_explicit
     using assms by auto
 qed
@@ -1484,7 +1495,7 @@
 
 lemma in_convex_hull_linear_image:
   assumes "bounded_linear f" "x \<in> convex hull s"
-  shows "(f x) \<in> convex hull (f ` s)"
+  shows "f x \<in> convex hull (f ` s)"
   using convex_hull_linear_image[OF assms(1)] assms(2) by auto
 
 
@@ -1523,7 +1534,7 @@
   assume "x \<in> ?hull"
   then obtain u v b where obt: "u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b"
     by auto
-  have "a \<in> convex hull insert a s" "b\<in>convex hull insert a s"
+  have "a \<in> convex hull insert a s" "b \<in> convex hull insert a s"
     using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4)
     by auto
   then show "x \<in> convex hull insert a s"
@@ -1542,10 +1553,12 @@
   proof -
     fix x y u v
     assume as: "(0::real) \<le> u" "0 \<le> v" "u + v = 1" "x\<in>?hull" "y\<in>?hull"
-    from as(4) obtain u1 v1 b1
-      where obt1: "u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto
-    from as(5) obtain u2 v2 b2
-      where obt2: "u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto
+    from as(4) obtain u1 v1 b1 where
+      obt1: "u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1"
+      by auto
+    from as(5) obtain u2 v2 b2 where
+      obt2: "u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2"
+      by auto
     have *: "\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x"
       by (auto simp add: algebra_simps)
     have **: "\<exists>b \<in> convex hull s. u *\<^sub>R x + v *\<^sub>R y =
@@ -1584,7 +1597,8 @@
         unfolding obt1(5) obt2(5)
         unfolding * and **
         using False
-        apply (rule_tac x = "((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI)
+        apply (rule_tac
+          x = "((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI)
         defer
         apply (rule convex_convex_hull[of s, unfolded convex_def, rule_format])
         using obt1(4) obt2(4)
@@ -1596,7 +1610,7 @@
       unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto
     have u2: "u2 \<le> 1"
       unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto
-    have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v"
+    have "u1 * u + u2 * v \<le> max u1 u2 * u + max u1 u2 * v"
       apply (rule add_mono)
       apply (rule_tac [!] mult_right_mono)
       using as(1,2) obt1(1,2) obt2(1,2)
@@ -1625,7 +1639,8 @@
   shows "convex hull s =
     {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
         (setsum u {1..k} = 1) \<and>
-        (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull")
+        (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}"
+  (is "?xyz = ?hull")
   apply (rule hull_unique)
   apply rule
   defer
@@ -1661,10 +1676,10 @@
   fix x y u v
   assume uv: "0 \<le> u" "0 \<le> v" "u + v = (1::real)" and xy: "x \<in> ?hull" "y \<in> ?hull"
   from xy obtain k1 u1 x1 where
-      x: "\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "setsum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x"
+    x: "\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "setsum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x"
     by auto
   from xy obtain k2 u2 x2 where
-      y: "\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "setsum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y"
+    y: "\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "setsum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y"
     by auto
   have *: "\<And>P (x1::'a) x2 s1 s2 i.
     (if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)"
@@ -1715,7 +1730,8 @@
   fixes s :: "'a::real_vector set"
   assumes "finite s"
   shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
-    setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")
+    setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}"
+  (is "?HULL = ?set")
 proof (rule hull_unique, auto simp add: convex_def[of ?set])
   fix x
   assume "x \<in> s"
@@ -1730,7 +1746,8 @@
   assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
   fix ux assume ux: "\<forall>x\<in>s. 0 \<le> ux x" "setsum ux s = (1::real)"
   fix uy assume uy: "\<forall>x\<in>s. 0 \<le> uy x" "setsum uy s = (1::real)"
-  { fix x
+  {
+    fix x
     assume "x\<in>s"
     then have "0 \<le> u * ux x + v * uy x"
       using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2)
@@ -1744,7 +1761,8 @@
     using uv(3) by auto
   moreover
   have "(\<Sum>x\<in>s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
-    unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[symmetric] and scaleR_right.setsum [symmetric]
+    unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[symmetric]
+      and scaleR_right.setsum [symmetric]
     by auto
   ultimately
   show "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> setsum uc s = 1 \<and>
@@ -1776,7 +1794,8 @@
 lemma convex_hull_explicit:
   fixes p :: "'a::real_vector set"
   shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and>
-    (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs")
+    (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
+  (is "?lhs = ?rhs")
 proof -
   {
     fix x
@@ -1817,7 +1836,8 @@
     fix y
     assume "y\<in>?rhs"
     then obtain s u where
-      obt: "finite s" "s \<subseteq> p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
+      obt: "finite s" "s \<subseteq> p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y"
+      by auto
 
     obtain f where f: "inj_on f {1..card s}" "f ` {1..card s} = s"
       using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto
@@ -1850,8 +1870,10 @@
         by (auto simp add: setsum_constant_scaleR)
     }
     then have "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"
-      unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
-      unfolding f using setsum_cong2[of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"]
+      unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f]
+        and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
+      unfolding f
+      using setsum_cong2[of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"]
       using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u]
       unfolding obt(4,5)
       by auto
@@ -1882,7 +1904,7 @@
   (is "?lhs = ?rhs")
 proof (rule, case_tac[!] "a\<in>s")
   assume "a \<in> s"
-  then have *:" insert a s = s" by auto
+  then have *: "insert a s = s" by auto
   assume ?lhs
   then show ?rhs
     unfolding *
@@ -1919,7 +1941,8 @@
     done
 next
   assume ?rhs
-  then obtain v u where uv: "v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a"
+  then obtain v u where
+    uv: "v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a"
     by auto
   moreover
   assume "a \<notin> s"
@@ -2354,27 +2377,27 @@
 
 lemma affine_dependent_translation:
   assumes "affine_dependent S"
-  shows "affine_dependent ((%x. a + x) ` S)"
+  shows "affine_dependent ((\<lambda>x. a + x) ` S)"
 proof -
-  obtain x where x_def: "x : S & x : affine hull (S - {x})"
+  obtain x where x_def: "x \<in> S \<and> x \<in> affine hull (S - {x})"
     using assms affine_dependent_def by auto
   have "op + a ` (S - {x}) = op + a ` S - {a + x}"
     by auto
-  then have "a+x \<in> affine hull ((%x. a + x) ` S - {a+x})"
+  then have "a+x \<in> affine hull ((\<lambda>x. a + x) ` S - {a+x})"
     using affine_hull_translation[of a "S-{x}"] x_def by auto
-  moreover have "a+x : (\<lambda>x. a + x) ` S"
+  moreover have "a+x \<in> (\<lambda>x. a + x) ` S"
     using x_def by auto
   ultimately show ?thesis
     unfolding affine_dependent_def by auto
 qed
 
 lemma affine_dependent_translation_eq:
-  "affine_dependent S <-> affine_dependent ((%x. a + x) ` S)"
+  "affine_dependent S <-> affine_dependent ((\<lambda>x. a + x) ` S)"
 proof -
   {
-    assume "affine_dependent ((%x. a + x) ` S)"
+    assume "affine_dependent ((\<lambda>x. a + x) ` S)"
     then have "affine_dependent S"
-      using affine_dependent_translation[of "((%x. a + x) ` S)" "-a"] translation_assoc[of "-a" a]
+      using affine_dependent_translation[of "((\<lambda>x. a + x) ` S)" "-a"] translation_assoc[of "-a" a]
       by auto
   }
   then show ?thesis
@@ -2382,14 +2405,14 @@
 qed
 
 lemma affine_hull_0_dependent:
-  assumes "0 : affine hull S"
+  assumes "0 \<in> affine hull S"
   shows "dependent S"
 proof -
-  obtain s u where s_u_def: "finite s & s ~= {} & s <= S & setsum u s = 1 & (SUM v:s. u v *\<^sub>R v) = 0"
+  obtain s u where s_u_def: "finite s \<and> s \<noteq> {} \<and> s \<subseteq> S \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
     using assms affine_hull_explicit[of S] by auto
-  then have "EX v:s. u v \<noteq> 0"
+  then have "\<exists>v\<in>s. u v \<noteq> 0"
     using setsum_not_0[of "u" "s"] by auto
-  then have "finite s & s <= S & (EX v:s. u v ~= 0 & (SUM v:s. u v *\<^sub>R v) = 0)"
+  then have "finite s \<and> s \<subseteq> S \<and> (\<exists>v\<in>s. u v \<noteq> 0 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0)"
     using s_u_def by auto
   then show ?thesis
     unfolding dependent_explicit[of S] by auto
@@ -2399,7 +2422,7 @@
   assumes "affine_dependent (insert 0 S)"
   shows "dependent S"
 proof -
-  obtain x where x_def: "x:insert 0 S & x : affine hull (insert 0 S - {x})"
+  obtain x where x_def: "x \<in> insert 0 S \<and> x \<in> affine hull (insert 0 S - {x})"
     using affine_dependent_def[of "(insert 0 S)"] assms by blast
   then have "x \<in> span (insert 0 S - {x})"
     using affine_hull_subset_span by auto
@@ -2432,19 +2455,19 @@
 qed
 
 lemma affine_dependent_iff_dependent2:
-  assumes "a : S"
-  shows "affine_dependent S <-> dependent ((%x. -a + x) ` (S-{a}))"
+  assumes "a \<in> S"
+  shows "affine_dependent S \<longleftrightarrow> dependent ((\<lambda>x. -a + x) ` (S-{a}))"
 proof -
-  have "insert a (S - {a})=S"
+  have "insert a (S - {a}) = S"
     using assms by auto
   then show ?thesis
     using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto
 qed
 
 lemma affine_hull_insert_span_gen:
-  "affine hull (insert a s) = (%x. a+x) ` span ((%x. -a+x) ` s)"
+  "affine hull (insert a s) = (\<lambda>x. a + x) ` span ((\<lambda>x. - a + x) ` s)"
 proof -
-  have h1: "{x - a |x. x : s}=((%x. -a+x) ` s)"
+  have h1: "{x - a |x. x \<in> s} = ((\<lambda>x. -a+x) ` s)"
     by auto
   {
     assume "a \<notin> s"
@@ -2454,18 +2477,18 @@
   moreover
   {
     assume a1: "a \<in> s"
-    have "\<exists>x. x \<in> s & -a+x=0"
+    have "\<exists>x. x \<in> s \<and> -a+x=0"
       apply (rule exI[of _ a])
       using a1
       apply auto
       done
-    then have "insert 0 ((%x. -a+x) ` (s - {a}))=(%x. -a+x) ` s"
+    then have "insert 0 ((\<lambda>x. -a+x) ` (s - {a})) = (\<lambda>x. -a+x) ` s"
       by auto
-    then have "span ((%x. -a+x) ` (s - {a}))=span ((%x. -a+x) ` s)"
+    then have "span ((\<lambda>x. -a+x) ` (s - {a}))=span ((\<lambda>x. -a+x) ` s)"
       using span_insert_0[of "op + (- a) ` (s - {a})"] by auto
-    moreover have "{x - a |x. x : (s - {a})}=((%x. -a+x) ` (s - {a}))"
+    moreover have "{x - a |x. x \<in> (s - {a})} = ((\<lambda>x. -a+x) ` (s - {a}))"
       by auto
-    moreover have "insert a (s - {a})=(insert a s)"
+    moreover have "insert a (s - {a}) = insert a s"
       using assms by auto
     ultimately have ?thesis
       using assms affine_hull_insert_span[of "a" "s-{a}"] by auto
@@ -2480,8 +2503,8 @@
   by auto
 
 lemma affine_hull_span_gen:
-  assumes "a : affine hull s"
-  shows "affine hull s = (%x. a+x) ` span ((%x. -a+x) ` s)"
+  assumes "a \<in> affine hull s"
+  shows "affine hull s = (\<lambda>x. a+x) ` span ((\<lambda>x. -a+x) ` s)"
 proof -
   have "affine hull (insert a s) = affine hull s"
     using hull_redundant[of a affine s] assms by auto
@@ -2490,33 +2513,34 @@
 qed
 
 lemma affine_hull_span_0:
-  assumes "0 : affine hull S"
+  assumes "0 \<in> affine hull S"
   shows "affine hull S = span S"
   using affine_hull_span_gen[of "0" S] assms by auto
 
 
 lemma extend_to_affine_basis:
-  fixes S V :: "('n::euclidean_space) set"
-  assumes "\<not> affine_dependent S" "S <= V" "S \<noteq> {}"
-  shows "\<exists>T. \<not> affine_dependent T & S <=T & T <= V & affine hull T = affine hull V"
+  fixes S V :: "'n::euclidean_space set"
+  assumes "\<not> affine_dependent S" "S \<subseteq> V" "S \<noteq> {}"
+  shows "\<exists>T. \<not> affine_dependent T \<and> S \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V"
 proof -
   obtain a where a_def: "a \<in> S"
     using assms by auto
-  then have h0: "independent  ((%x. -a + x) ` (S-{a}))"
+  then have h0: "independent  ((\<lambda>x. -a + x) ` (S-{a}))"
     using affine_dependent_iff_dependent2 assms by auto
   then obtain B where B_def:
-    "(%x. -a+x) ` (S - {a}) <= B & B <= (%x. -a+x) ` V & independent B & (%x. -a+x) ` V <= span B"
-     using maximal_independent_subset_extend[of "(%x. -a+x) ` (S-{a})" "(%x. -a + x) ` V"] assms
+    "(\<lambda>x. -a+x) ` (S - {a}) \<subseteq> B \<and> B \<subseteq> (\<lambda>x. -a+x) ` V \<and> independent B \<and> (\<lambda>x. -a+x) ` V \<subseteq> span B"
+     using maximal_independent_subset_extend[of "(\<lambda>x. -a+x) ` (S-{a})" "(\<lambda>x. -a + x) ` V"] assms
      by blast
-  def T \<equiv> "(%x. a+x) ` (insert 0 B)"
-  then have "T = insert a ((%x. a+x) ` B)" by auto
-  then have "affine hull T = (%x. a+x) ` span B"
-    using affine_hull_insert_span_gen[of a "((%x. a+x) ` B)"] translation_assoc[of "-a" a B]
+  def T \<equiv> "(\<lambda>x. a+x) ` insert 0 B"
+  then have "T = insert a ((\<lambda>x. a+x) ` B)"
+    by auto
+  then have "affine hull T = (\<lambda>x. a+x) ` span B"
+    using affine_hull_insert_span_gen[of a "((\<lambda>x. a+x) ` B)"] translation_assoc[of "-a" a B]
     by auto
   then have "V <= affine hull T"
     using B_def assms translation_inverse_subset[of a V "span B"]
     by auto
-  moreover have "T<=V"
+  moreover have "T \<subseteq> V"
     using T_def B_def a_def assms by auto
   ultimately have "affine hull T = affine hull V"
     by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono)
@@ -2524,14 +2548,15 @@
     using T_def B_def translation_inverse_subset[of a "S-{a}" B]
     by auto
   moreover have "\<not> affine_dependent T"
-    using T_def affine_dependent_translation_eq[of "insert 0 B"] affine_dependent_imp_dependent2 B_def
+    using T_def affine_dependent_translation_eq[of "insert 0 B"]
+      affine_dependent_imp_dependent2 B_def
     by auto
-  ultimately show ?thesis using `T<=V` by auto
+  ultimately show ?thesis using `T \<subseteq> V` by auto
 qed
 
 lemma affine_basis_exists:
-  fixes V :: "('n::euclidean_space) set"
-  shows "\<exists>B. B <= V & \<not> affine_dependent B & affine hull V = affine hull B"
+  fixes V :: "'n::euclidean_space set"
+  shows "\<exists>B. B \<subseteq> V \<and> \<not> affine_dependent B \<and> affine hull V = affine hull B"
 proof (cases "V = {}")
   case True
   then show ?thesis
@@ -2540,7 +2565,8 @@
   case False
   then obtain x where "x \<in> V" by auto
   then show ?thesis
-    using affine_dependent_def[of "{x}"] extend_to_affine_basis[of "{x}:: ('n::euclidean_space) set" V]
+    using affine_dependent_def[of "{x}"]
+      extend_to_affine_basis[of "{x}:: ('n::euclidean_space) set" V]
     by auto
 qed
 
@@ -2548,19 +2574,21 @@
 subsection {* Affine Dimension of a Set *}
 
 definition "aff_dim V =
-  (SOME d :: int. ? B. (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = d+1))"
+  (SOME d :: int.
+    \<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1)"
 
 lemma aff_dim_basis_exists:
   fixes V :: "('n::euclidean_space) set"
-  shows "? B. (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = aff_dim V+1)"
+  shows "\<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = aff_dim V + 1"
 proof -
-  obtain B where B_def: "\<not> affine_dependent B & affine hull B = affine hull V"
+  obtain B where B_def: "\<not> affine_dependent B \<and> affine hull B = affine hull V"
     using affine_basis_exists[of V] by auto
   then show ?thesis
-    unfolding aff_dim_def some_eq_ex[of "\<lambda>d. \<exists>(B :: ('n::euclidean_space) set). affine hull B = affine hull V
-      & \<not> affine_dependent B & of_nat (card B) = d+1"]
+    unfolding aff_dim_def
+      some_eq_ex[of "\<lambda>d. \<exists>(B :: ('n::euclidean_space) set). affine hull B = affine hull V
+        \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1"]
     apply auto
-    apply (rule exI[of _ "int (card B)-(1 :: int)"])
+    apply (rule exI[of _ "int (card B) - (1 :: int)"])
     apply (rule exI[of _ "B"])
     apply auto
     done
@@ -2578,45 +2606,47 @@
 lemma aff_dim_parallel_subspace_aux:
   fixes B :: "('n::euclidean_space) set"
   assumes "\<not> affine_dependent B" "a \<in> B"
-  shows "finite B & ((card B) - 1 = dim (span ((%x. -a+x) ` (B-{a}))))"
+  shows "finite B \<and> ((card B) - 1 = dim (span ((\<lambda>x. -a+x) ` (B-{a}))))"
 proof -
-  have "independent ((%x. -a + x) ` (B-{a}))"
+  have "independent ((\<lambda>x. -a + x) ` (B-{a}))"
     using affine_dependent_iff_dependent2 assms by auto
-  then have fin: "dim (span ((%x. -a+x) ` (B-{a}))) = card ((%x. -a + x) ` (B-{a}))"
-    "finite ((%x. -a + x) ` (B - {a}))"  using indep_card_eq_dim_span[of "(%x. -a+x) ` (B-{a})"]
-    by auto
+  then have fin: "dim (span ((\<lambda>x. -a+x) ` (B-{a}))) = card ((\<lambda>x. -a + x) ` (B-{a}))"
+    "finite ((\<lambda>x. -a + x) ` (B - {a}))"
+    using indep_card_eq_dim_span[of "(%x. -a+x) ` (B-{a})"] by auto
   show ?thesis
-  proof (cases "(%x. -a + x) ` (B - {a}) = {}")
+  proof (cases "(\<lambda>x. -a + x) ` (B - {a}) = {}")
     case True
-    have "B = insert a ((%x. a + x) ` (%x. -a + x) ` (B - {a}))"
+    have "B = insert a ((\<lambda>x. a + x) ` (\<lambda>x. -a + x) ` (B - {a}))"
       using translation_assoc[of "a" "-a" "(B - {a})"] assms by auto
-    then have "B={a}" using True by auto
+    then have "B = {a}" using True by auto
     then show ?thesis using assms fin by auto
   next
     case False
-    then have "card ((%x. -a + x) ` (B - {a}))>0"
+    then have "card ((\<lambda>x. -a + x) ` (B - {a})) > 0"
       using fin by auto
-    moreover have h1: "card ((%x. -a + x) ` (B-{a})) = card (B-{a})"
+    moreover have h1: "card ((\<lambda>x. -a + x) ` (B-{a})) = card (B-{a})"
        apply (rule card_image)
        using translate_inj_on
        apply auto
        done
-    ultimately have "card (B-{a})>0" by auto
-    then have *: "finite(B-{a})"
+    ultimately have "card (B-{a}) > 0" by auto
+    then have *: "finite (B - {a})"
       using card_gt_0_iff[of "(B - {a})"] by auto
-    then have "(card (B-{a})= (card B) - 1)"
+    then have "card (B - {a}) = card B - 1"
       using card_Diff_singleton assms by auto
     with * show ?thesis using fin h1 by auto
   qed
 qed
 
 lemma aff_dim_parallel_subspace:
-  fixes V L :: "('n::euclidean_space) set"
+  fixes V L :: "'n::euclidean_space set"
   assumes "V \<noteq> {}"
-  assumes "subspace L" "affine_parallel (affine hull V) L"
+    and "subspace L"
+    and "affine_parallel (affine hull V) L"
   shows "aff_dim V = int (dim L)"
 proof -
-  obtain B where B_def: "affine hull B = affine hull V & ~ affine_dependent B & int (card B) = aff_dim V + 1"
+  obtain B where
+    B_def: "affine hull B = affine hull V & ~ affine_dependent B & int (card B) = aff_dim V + 1"
     using aff_dim_basis_exists by auto
   then have "B \<noteq> {}"
     using assms B_def affine_hull_nonempty[of V] affine_hull_nonempty[of B]
@@ -2624,8 +2654,10 @@
   then obtain a where a_def: "a \<in> B" by auto
   def Lb \<equiv> "span ((\<lambda>x. -a+x) ` (B-{a}))"
   moreover have "affine_parallel (affine hull B) Lb"
-    using Lb_def B_def assms affine_hull_span2[of a B] a_def  affine_parallel_commut[of "Lb" "(affine hull B)"]
-    unfolding affine_parallel_def by auto
+    using Lb_def B_def assms affine_hull_span2[of a B] a_def
+      affine_parallel_commut[of "Lb" "(affine hull B)"]
+    unfolding affine_parallel_def
+    by auto
   moreover have "subspace Lb"
     using Lb_def subspace_span by auto
   moreover have "affine hull B \<noteq> {}"
@@ -2633,8 +2665,9 @@
   ultimately have "L = Lb"
     using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B_def
     by auto
-  then have "dim L = dim Lb" by auto
-  moreover have "(card B) - 1 = dim Lb" "finite B"
+  then have "dim L = dim Lb"
+    by auto
+  moreover have "card B - 1 = dim Lb" and "finite B"
     using Lb_def aff_dim_parallel_subspace_aux a_def B_def by auto
 (*  hence "card B=dim Lb+1" using `B~={}` card_gt_0_iff[of B] by auto *)
   ultimately show ?thesis
@@ -2642,8 +2675,8 @@
 qed
 
 lemma aff_independent_finite:
-  fixes B :: "('n::euclidean_space) set"
-  assumes "~(affine_dependent B)"
+  fixes B :: "'n::euclidean_space set"
+  assumes "\<not> affine_dependent B"
   shows "finite B"
 proof -
   {
@@ -2656,244 +2689,337 @@
 qed
 
 lemma independent_finite:
-  fixes B :: "('n::euclidean_space) set"
+  fixes B :: "'n::euclidean_space set"
   assumes "independent B"
   shows "finite B"
   using affine_dependent_imp_dependent[of B] aff_independent_finite[of B] assms
   by auto
 
 lemma subspace_dim_equal:
-  assumes "subspace (S :: ('n::euclidean_space) set)" "subspace T" "S <= T" "dim S >= dim T"
+  assumes "subspace (S :: ('n::euclidean_space) set)"
+    and "subspace T"
+    and "S \<subseteq> T"
+    and "dim S \<ge> dim T"
   shows "S = T"
 proof -
-  obtain B where B_def: "B <= S & independent B & S <= span B & (card B = dim S)" using basis_exists[of S] by auto
-  hence "span B <= S" using span_mono[of B S] span_eq[of S] assms by metis
-  hence "span B = S" using B_def by auto
-  have "dim S = dim T" using assms dim_subset[of S T] by auto
-  hence "T <= span B" using card_eq_dim[of B T] B_def independent_finite assms by auto
-  from this show ?thesis using assms `span B=S` by auto
+  obtain B where B_def: "B \<le> S \<and> independent B \<and> S \<subseteq> span B \<and> card B = dim S"
+    using basis_exists[of S] by auto
+  then have "span B \<subseteq> S"
+    using span_mono[of B S] span_eq[of S] assms by metis
+  then have "span B = S"
+    using B_def by auto
+  have "dim S = dim T"
+    using assms dim_subset[of S T] by auto
+  then have "T \<subseteq> span B"
+    using card_eq_dim[of B T] B_def independent_finite assms by auto
+  then show ?thesis
+    using assms `span B = S` by auto
 qed
 
 lemma span_substd_basis:
   assumes d: "d \<subseteq> Basis"
   shows "span d = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}" (is "_ = ?B")
-proof-
-have "d <= ?B" using d by (auto simp: inner_Basis)
-moreover have s: "subspace ?B" using subspace_substandard[of "%i. i ~: d"] .
-ultimately have "span d <= ?B" using span_mono[of d "?B"] span_eq[of "?B"] by blast
-moreover have "card d <= dim (span d)" using independent_card_le_dim[of d "span d"]
-   independent_substdbasis[OF assms] span_inc[of d] by auto
-moreover hence "dim ?B <= dim (span d)" using dim_substandard[OF assms] by auto
-ultimately show ?thesis using s subspace_dim_equal[of "span d" "?B"]
-  subspace_span[of d] by auto
+proof -
+  have "d \<subseteq> ?B"
+    using d by (auto simp: inner_Basis)
+  moreover have s: "subspace ?B"
+    using subspace_substandard[of "\<lambda>i. i \<notin> d"] .
+  ultimately have "span d \<subseteq> ?B"
+    using span_mono[of d "?B"] span_eq[of "?B"] by blast
+  moreover have "card d \<le> dim (span d)"
+    using independent_card_le_dim[of d "span d"] independent_substdbasis[OF assms] span_inc[of d]
+    by auto
+  moreover then have "dim ?B \<le> dim (span d)"
+    using dim_substandard[OF assms] by auto
+  ultimately show ?thesis
+    using s subspace_dim_equal[of "span d" "?B"] subspace_span[of d] by auto
 qed
 
 lemma basis_to_substdbasis_subspace_isomorphism:
-fixes B :: "('a::euclidean_space) set"
-assumes "independent B"
-shows "EX f (d::'a set). card d = card B \<and> linear f \<and> f ` B = d \<and>
-       f ` span B = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} \<and> inj_on f (span B) \<and> d \<subseteq> Basis"
-proof-
-  have B:"card B=dim B" using dim_unique[of B B "card B"] assms span_inc[of B] by auto
-  have "dim B \<le> card (Basis :: 'a set)" using dim_subset_UNIV[of B] by simp
-  from ex_card[OF this] obtain d :: "'a set" where d: "d \<subseteq> Basis" and t: "card d = dim B" by auto
+  fixes B :: "'a::euclidean_space set"
+  assumes "independent B"
+  shows "\<exists>f d::'a set. card d = card B \<and> linear f \<and> f ` B = d \<and>
+    f ` span B = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} \<and> inj_on f (span B) \<and> d \<subseteq> Basis"
+proof -
+  have B: "card B = dim B"
+    using dim_unique[of B B "card B"] assms span_inc[of B] by auto
+  have "dim B \<le> card (Basis :: 'a set)"
+    using dim_subset_UNIV[of B] by simp
+  from ex_card[OF this] obtain d :: "'a set" where d: "d \<subseteq> Basis" and t: "card d = dim B"
+    by auto
   let ?t = "{x::'a::euclidean_space. \<forall>i\<in>Basis. i ~: d --> x\<bullet>i = 0}"
-  have "EX f. linear f & f ` B = d & f ` span B = ?t & inj_on f (span B)"
+  have "\<exists>f. linear f \<and> f ` B = d \<and> f ` span B = ?t \<and> inj_on f (span B)"
     apply (rule basis_to_basis_subspace_isomorphism[of "span B" ?t B "d"])
-    apply(rule subspace_span) apply(rule subspace_substandard) defer
-    apply(rule span_inc) apply(rule assms) defer unfolding dim_span[of B] apply(rule B)
+    apply (rule subspace_span)
+    apply (rule subspace_substandard)
+    defer
+    apply (rule span_inc)
+    apply (rule assms)
+    defer
+    unfolding dim_span[of B]
+    apply(rule B)
     unfolding span_substd_basis[OF d, symmetric] 
-    apply(rule span_inc)
-    apply(rule independent_substdbasis[OF d]) apply(rule,assumption)
-    unfolding t[symmetric] span_substd_basis[OF d] dim_substandard[OF d] by auto
+    apply (rule span_inc)
+    apply (rule independent_substdbasis[OF d])
+    apply rule
+    apply assumption
+    unfolding t[symmetric] span_substd_basis[OF d] dim_substandard[OF d]
+    apply auto
+    done
   with t `card B = dim B` d show ?thesis by auto
 qed
 
 lemma aff_dim_empty:
-fixes S :: "('n::euclidean_space) set"
-shows "S = {} <-> aff_dim S = -1"
-proof-
-obtain B where "affine hull B = affine hull S & ~ affine_dependent B & int (card B) = aff_dim S + 1" using aff_dim_basis_exists by auto
-moreover hence "S={} <-> B={}" using affine_hull_nonempty[of B] affine_hull_nonempty[of S] by auto
-ultimately show ?thesis using aff_independent_finite[of B] card_gt_0_iff[of B] by auto
-qed
-
-lemma aff_dim_affine_hull:
-shows "aff_dim (affine hull S)=aff_dim S"
-unfolding aff_dim_def using hull_hull[of _ S] by auto
+  fixes S :: "'n::euclidean_space set"
+  shows "S = {} \<longleftrightarrow> aff_dim S = -1"
+proof -
+  obtain B where *: "affine hull B = affine hull S"
+    and "\<not> affine_dependent B"
+    and "int (card B) = aff_dim S + 1"
+    using aff_dim_basis_exists by auto
+  moreover
+  from * have "S = {} \<longleftrightarrow> B = {}"
+    using affine_hull_nonempty[of B] affine_hull_nonempty[of S] by auto
+  ultimately show ?thesis
+    using aff_independent_finite[of B] card_gt_0_iff[of B] by auto
+qed
+
+lemma aff_dim_affine_hull: "aff_dim (affine hull S) = aff_dim S"
+  unfolding aff_dim_def using hull_hull[of _ S] by auto
 
 lemma aff_dim_affine_hull2:
-assumes "affine hull S=affine hull T"
-shows "aff_dim S=aff_dim T" unfolding aff_dim_def using assms by auto
+  assumes "affine hull S = affine hull T"
+  shows "aff_dim S = aff_dim T"
+  unfolding aff_dim_def using assms by auto
 
 lemma aff_dim_unique:
-fixes B V :: "('n::euclidean_space) set"
-assumes "(affine hull B=affine hull V) & ~(affine_dependent B)"
-shows "of_nat(card B) = aff_dim V+1"
-proof-
-{ assume "B={}" hence "V={}" using affine_hull_nonempty[of V] affine_hull_nonempty[of B] assms by auto
-  hence "aff_dim V = (-1::int)"  using aff_dim_empty by auto
-  hence ?thesis using `B={}` by auto
-}
-moreover
-{ assume "B~={}" from this obtain a where a_def: "a:B" by auto
-  def Lb == "span ((%x. -a+x) ` (B-{a}))"
+  fixes B V :: "'n::euclidean_space set"
+  assumes "affine hull B = affine hull V \<and> \<not> affine_dependent B"
+  shows "of_nat (card B) = aff_dim V + 1"
+proof (cases "B = {}")
+  case True
+  then have "V = {}"
+    using affine_hull_nonempty[of V] affine_hull_nonempty[of B] assms
+    by auto
+  then have "aff_dim V = (-1::int)"
+    using aff_dim_empty by auto
+  then show ?thesis
+    using `B={}` by auto
+next
+  case False
+  then obtain a where a_def: "a \<in> B" by auto
+  def Lb \<equiv> "span ((\<lambda>x. -a+x) ` (B-{a}))"
   have "affine_parallel (affine hull B) Lb"
-     using Lb_def affine_hull_span2[of a B] a_def  affine_parallel_commut[of "Lb" "(affine hull B)"]
-     unfolding affine_parallel_def by auto
-  moreover have "subspace Lb" using Lb_def subspace_span by auto
-  ultimately have "aff_dim B=int(dim Lb)" using aff_dim_parallel_subspace[of B Lb] `B~={}` by auto
-  moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a_def assms by auto
-  ultimately have "(of_nat(card B) = aff_dim B+1)" using  `B~={}` card_gt_0_iff[of B] by auto
-  hence ?thesis using aff_dim_affine_hull2 assms by auto
-} ultimately show ?thesis by blast
+    using Lb_def affine_hull_span2[of a B] a_def
+      affine_parallel_commut[of "Lb" "(affine hull B)"]
+    unfolding affine_parallel_def by auto
+  moreover have "subspace Lb"
+    using Lb_def subspace_span by auto
+  ultimately have "aff_dim B = int(dim Lb)"
+    using aff_dim_parallel_subspace[of B Lb] `B~={}` by auto
+  moreover have "(card B) - 1 = dim Lb" "finite B"
+    using Lb_def aff_dim_parallel_subspace_aux a_def assms by auto
+  ultimately have "of_nat (card B) = aff_dim B + 1"
+    using `B \<noteq> {}` card_gt_0_iff[of B] by auto
+  then show ?thesis
+    using aff_dim_affine_hull2 assms by auto
 qed
 
 lemma aff_dim_affine_independent:
-fixes B :: "('n::euclidean_space) set"
-assumes "~(affine_dependent B)"
-shows "of_nat(card B) = aff_dim B+1"
+  fixes B :: "'n::euclidean_space set"
+  assumes "\<not> affine_dependent B"
+  shows "of_nat (card B) = aff_dim B + 1"
   using aff_dim_unique[of B B] assms by auto
 
 lemma aff_dim_sing:
-fixes a :: "'n::euclidean_space"
-shows "aff_dim {a}=0"
+  fixes a :: "'n::euclidean_space"
+  shows "aff_dim {a} = 0"
   using aff_dim_affine_independent[of "{a}"] affine_independent_sing by auto
 
 lemma aff_dim_inner_basis_exists:
   fixes V :: "('n::euclidean_space) set"
-  shows "? B. B<=V & (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = aff_dim V+1)"
-proof-
-obtain B where B_def: "~(affine_dependent B) & B<=V & (affine hull B=affine hull V)" using affine_basis_exists[of V] by auto
-moreover hence "of_nat(card B) = aff_dim V+1" using aff_dim_unique by auto
-ultimately show ?thesis by auto
+  shows "\<exists>B. B \<subseteq> V \<and> affine hull B = affine hull V \<and>
+    \<not> affine_dependent B \<and> of_nat (card B) = aff_dim V + 1"
+proof -
+  obtain B where B_def: "\<not> affine_dependent B" "B \<subseteq> V" "affine hull B = affine hull V"
+    using affine_basis_exists[of V] by auto
+  then have "of_nat(card B) = aff_dim V+1" using aff_dim_unique by auto
+  with B_def show ?thesis by auto
 qed
 
 lemma aff_dim_le_card:
-fixes V :: "('n::euclidean_space) set"
-assumes "finite V"
-shows "aff_dim V <= of_nat(card V) - 1"
- proof-
- obtain B where B_def: "B<=V & (of_nat(card B) = aff_dim V+1)" using aff_dim_inner_basis_exists[of V] by auto
- moreover hence "card B <= card V" using assms card_mono by auto
- ultimately show ?thesis by auto
+  fixes V :: "('n::euclidean_space) set"
+  assumes "finite V"
+  shows "aff_dim V <= of_nat(card V) - 1"
+proof -
+  obtain B where B_def: "B \<subseteq> V" "of_nat (card B) = aff_dim V + 1"
+    using aff_dim_inner_basis_exists[of V] by auto
+  then have "card B \<le> card V"
+    using assms card_mono by auto
+  with B_def show ?thesis by auto
 qed
 
 lemma aff_dim_parallel_eq:
-fixes S T :: "('n::euclidean_space) set"
-assumes "affine_parallel (affine hull S) (affine hull T)"
-shows "aff_dim S=aff_dim T"
-proof-
-{ assume "T~={}" "S~={}"
-  from this obtain L where L_def: "subspace L & affine_parallel (affine hull T) L"
-       using affine_parallel_subspace[of "affine hull T"] affine_affine_hull[of T] affine_hull_nonempty by auto
-  hence "aff_dim T = int(dim L)" using aff_dim_parallel_subspace `T~={}` by auto
-  moreover have "subspace L & affine_parallel (affine hull S) L"
-     using L_def affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto
-  moreover hence "aff_dim S = int(dim L)" using aff_dim_parallel_subspace `S~={}` by auto
-  ultimately have ?thesis by auto
-}
-moreover
-{ assume "S={}" hence "S={} & T={}" using assms affine_hull_nonempty unfolding affine_parallel_def by auto
-  hence ?thesis using aff_dim_empty by auto
-}
-moreover
-{ assume "T={}" hence "S={} & T={}" using assms affine_hull_nonempty unfolding affine_parallel_def by auto
-  hence ?thesis using aff_dim_empty by auto
-}
-ultimately show ?thesis by blast
+  fixes S T :: "'n::euclidean_space set"
+  assumes "affine_parallel (affine hull S) (affine hull T)"
+  shows "aff_dim S = aff_dim T"
+proof -
+  {
+    assume "T \<noteq> {}" "S \<noteq> {}"
+    then obtain L where L_def: "subspace L & affine_parallel (affine hull T) L"
+      using affine_parallel_subspace[of "affine hull T"] affine_affine_hull[of T] affine_hull_nonempty
+      by auto
+    then have "aff_dim T = int (dim L)"
+      using aff_dim_parallel_subspace `T \<noteq> {}` by auto
+    moreover have *: "subspace L \<and> affine_parallel (affine hull S) L"
+       using L_def affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto
+    moreover from * have "aff_dim S = int (dim L)"
+      using aff_dim_parallel_subspace `S \<noteq> {}` by auto
+    ultimately have ?thesis by auto
+  }
+  moreover
+  {
+    assume "S = {}"
+    then have "S = {}" and "T = {}"
+      using assms affine_hull_nonempty
+      unfolding affine_parallel_def
+      by auto
+    then have ?thesis using aff_dim_empty by auto
+  }
+  moreover
+  {
+    assume "T = {}"
+    then have "S = {}" and "T = {}"
+      using assms affine_hull_nonempty
+      unfolding affine_parallel_def
+      by auto
+    then have ?thesis
+      using aff_dim_empty by auto
+  }
+  ultimately show ?thesis by blast
 qed
 
 lemma aff_dim_translation_eq:
-fixes a :: "'n::euclidean_space"
-shows "aff_dim ((%x. a + x) ` S)=aff_dim S"
-proof-
-have "affine_parallel (affine hull S) (affine hull ((%x. a + x) ` S))" unfolding affine_parallel_def apply (rule exI[of _ "a"]) using affine_hull_translation[of a S] by auto
-from this show ?thesis using  aff_dim_parallel_eq[of S "(%x. a + x) ` S"] by auto
+  fixes a :: "'n::euclidean_space"
+  shows "aff_dim ((\<lambda>x. a + x) ` S) = aff_dim S"
+proof -
+  have "affine_parallel (affine hull S) (affine hull ((%x. a + x) ` S))"
+    unfolding affine_parallel_def
+    apply (rule exI[of _ "a"])
+    using affine_hull_translation[of a S]
+    apply auto
+    done
+  then show ?thesis
+    using aff_dim_parallel_eq[of S "(\<lambda>x. a + x) ` S"] by auto
 qed
 
 lemma aff_dim_affine:
-fixes S L :: "('n::euclidean_space) set"
-assumes "S ~= {}" "affine S"
-assumes "subspace L" "affine_parallel S L"
-shows "aff_dim S=int(dim L)"
-proof-
-have 1: "(affine hull S) = S" using assms affine_hull_eq[of S] by auto
-hence "affine_parallel (affine hull S) L" using assms by (simp add:1)
-from this show ?thesis using assms aff_dim_parallel_subspace[of S L] by blast
+  fixes S L :: "'n::euclidean_space set"
+  assumes "S \<noteq> {}"
+    and "affine S"
+    and "subspace L"
+    and "affine_parallel S L"
+  shows "aff_dim S = int (dim L)"
+proof -
+  have *: "affine hull S = S"
+    using assms affine_hull_eq[of S] by auto
+  then have "affine_parallel (affine hull S) L"
+    using assms by (simp add: *)
+  then show ?thesis
+    using assms aff_dim_parallel_subspace[of S L] by blast
 qed
 
 lemma dim_affine_hull:
-fixes S :: "('n::euclidean_space) set"
-shows "dim (affine hull S)=dim S"
-proof-
-have "dim (affine hull S)>=dim S" using dim_subset by auto
-moreover have "dim(span S) >= dim (affine hull S)" using dim_subset affine_hull_subset_span by auto
-moreover have "dim(span S)=dim S" using dim_span by auto
-ultimately show ?thesis by auto
+  fixes S :: "'n::euclidean_space set"
+  shows "dim (affine hull S) = dim S"
+proof -
+  have "dim (affine hull S) \<ge> dim S"
+    using dim_subset by auto
+  moreover have "dim (span S) \<ge> dim (affine hull S)"
+    using dim_subset affine_hull_subset_span by auto
+  moreover have "dim (span S) = dim S"
+    using dim_span by auto
+  ultimately show ?thesis by auto
 qed
 
 lemma aff_dim_subspace:
-fixes S :: "('n::euclidean_space) set"
-assumes "S ~= {}" "subspace S"
-shows "aff_dim S=int(dim S)" using aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] by auto
+  fixes S :: "'n::euclidean_space set"
+  assumes "S \<noteq> {}"
+    and "subspace S"
+  shows "aff_dim S = int (dim S)"
+  using aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S]
+  by auto
 
 lemma aff_dim_zero:
-fixes S :: "('n::euclidean_space) set"
-assumes "0 : affine hull S"
-shows "aff_dim S=int(dim S)"
-proof-
-have "subspace(affine hull S)" using subspace_affine[of "affine hull S"] affine_affine_hull assms by auto
-hence "aff_dim (affine hull S) =int(dim (affine hull S))" using assms aff_dim_subspace[of "affine hull S"] by auto
-from this show ?thesis using aff_dim_affine_hull[of S] dim_affine_hull[of S] by auto
+  fixes S :: "'n::euclidean_space set"
+  assumes "0 \<in> affine hull S"
+  shows "aff_dim S = int (dim S)"
+proof -
+  have "subspace (affine hull S)"
+    using subspace_affine[of "affine hull S"] affine_affine_hull assms
+    by auto
+  then have "aff_dim (affine hull S) = int (dim (affine hull S))"
+    using assms aff_dim_subspace[of "affine hull S"] by auto
+  then show ?thesis
+    using aff_dim_affine_hull[of S] dim_affine_hull[of S]
+    by auto
 qed
 
 lemma aff_dim_univ: "aff_dim (UNIV :: ('n::euclidean_space) set) = int(DIM('n))"
   using aff_dim_subspace[of "(UNIV :: ('n::euclidean_space) set)"]
-    dim_UNIV[where 'a="'n::euclidean_space"] by auto
+    dim_UNIV[where 'a="'n::euclidean_space"]
+  by auto
 
 lemma aff_dim_geq:
-  fixes V :: "('n::euclidean_space) set"
-  shows "aff_dim V >= -1"
-proof-
-obtain B where B_def: "affine hull B = affine hull V & ~ affine_dependent B & int (card B) = aff_dim V + 1" using aff_dim_basis_exists by auto
-from this show ?thesis by auto
+  fixes V :: "'n::euclidean_space set"
+  shows "aff_dim V \<ge> -1"
+proof -
+  obtain B where
+    B_def: "affine hull B = affine hull V" "\<not> affine_dependent B" "int (card B) = aff_dim V + 1"
+    using aff_dim_basis_exists by auto
+  then show ?thesis by auto
 qed
 
 lemma independent_card_le_aff_dim:
-  assumes "(B::('n::euclidean_space) set) <= V"
-  assumes "~(affine_dependent B)"
-  shows "int(card B) <= aff_dim V+1"
-proof-
-{ assume "B~={}"
-  from this obtain T where T_def: "~(affine_dependent T) & B<=T & T<=V & affine hull T = affine hull V"
-  using assms extend_to_affine_basis[of B V] by auto
-  hence "of_nat(card T) = aff_dim V+1" using aff_dim_unique by auto
-  hence ?thesis using T_def card_mono[of T B] aff_independent_finite[of T] by auto
-}
-moreover
-{ assume "B={}"
-  moreover have "-1<= aff_dim V" using aff_dim_geq by auto
-  ultimately have ?thesis by auto
-}  ultimately show ?thesis by blast
+  assumes "(B:: 'n::euclidean_space set) \<subseteq> V"
+  assumes "\<not> affine_dependent B"
+  shows "int (card B) \<le> aff_dim V + 1"
+proof (cases "B = {}")
+  case True
+  then have "-1 \<le> aff_dim V"
+    using aff_dim_geq by auto
+  with True show ?thesis by auto
+next
+  case False
+  then obtain T where T_def: "\<not> affine_dependent T \<and> B \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V"
+    using assms extend_to_affine_basis[of B V] by auto
+  then have "of_nat (card T) = aff_dim V + 1"
+    using aff_dim_unique by auto
+  then show ?thesis
+    using T_def card_mono[of T B] aff_independent_finite[of T] by auto
 qed
 
 lemma aff_dim_subset:
   fixes S T :: "('n::euclidean_space) set"
   assumes "S <= T"
   shows "aff_dim S <= aff_dim T"
-proof-
-obtain B where B_def: "~(affine_dependent B) & B<=S & (affine hull B=affine hull S) & of_nat(card B) = aff_dim S+1" using aff_dim_inner_basis_exists[of S] by auto
-moreover hence "int (card B) <= aff_dim T + 1" using assms independent_card_le_aff_dim[of B T] by auto
-ultimately show ?thesis by auto
+proof -
+  obtain B where B_def: "\<not> affine_dependent B \<and> B \<subseteq> S \<and> affine hull B = affine hull S \<and>
+    of_nat (card B) = aff_dim S + 1"
+    using aff_dim_inner_basis_exists[of S] by auto
+  then have "int (card B) \<le> aff_dim T + 1"
+    using assms independent_card_le_aff_dim[of B T] by auto
+  with B_def show ?thesis by auto
 qed
 
 lemma aff_dim_subset_univ:
-fixes S :: "('n::euclidean_space) set"
-shows "aff_dim S <= int(DIM('n))"
+  fixes S :: "'n::euclidean_space set"
+  shows "aff_dim S \<le> int (DIM('n))"
 proof -
-  have "aff_dim (UNIV :: ('n::euclidean_space) set) = int(DIM('n))" using aff_dim_univ by auto
-  from this show "aff_dim (S:: ('n::euclidean_space) set) <= int(DIM('n))" using assms aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
+  have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
+    using aff_dim_univ by auto
+  then show "aff_dim (S:: 'n::euclidean_space set) \<le> int(DIM('n))"
+    using assms aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
 qed
 
 lemma affine_dim_equal: