# HG changeset patch
# User wenzelm
# Date 1348338568 -7200
# Node ID d523702bdae731b222d81ce47ce994729f855831
# Parent  789b73fcca722ca79b8303fd91bb31c17be0a2b4
tuned proofs;

diff -r 789b73fcca72 -r d523702bdae7 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Sep 22 19:32:30 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Sep 22 20:29:28 2012 +0200
@@ -24,9 +24,9 @@
   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"
-using linear_add[of f] linear_cmul[of f] assms by (simp) 
+  assumes "linear f"
+  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"
@@ -36,50 +36,56 @@
 lemma mem_convex_alt:
   assumes "convex S" "x : S" "y : S" "u>=0" "v>=0" "u+v>0"
   shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) : S"
-apply (subst mem_convex_2) 
-using assms apply (auto simp add: algebra_simps zero_le_divide_iff)
-using add_divide_distrib[of u v "u+v"] by auto
+  apply (subst mem_convex_2) 
+  using assms apply (auto simp add: algebra_simps zero_le_divide_iff)
+  using add_divide_distrib[of u v "u+v"] apply auto
+  done
 
 lemma inj_on_image_mem_iff: "inj_on f B ==> (A <= B) ==> (f a : f`A) ==> (a : B) ==> (a : A)" 
-by (blast dest: inj_onD)
+  by (blast dest: inj_onD)
 
 lemma independent_injective_on_span_image:
   assumes iS: "independent S" 
-     and lf: "linear f" and fi: "inj_on f (span S)"
+    and lf: "linear f" and fi: "inj_on f (span S)"
   shows "independent (f ` S)"
-proof-
-  {fix a assume a: "a : S" "f a : 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)
+proof -
+  {
+    fix a
+    assume a: "a : S" "f a : 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
+      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})" using fi a span_inc by (auto simp add: inj_on_def)
-    with a(1) iS  have False by (simp add: dependent_def) }
+    with a(1) iS have False by (simp add: dependent_def)
+  }
   then show ?thesis unfolding dependent_def by blast
 qed
 
 lemma dim_image_eq:
-fixes f :: "'n::euclidean_space => 'm::euclidean_space"
-assumes lf: "linear f" and fi: "inj_on f (span S)" 
-shows "dim (f ` S) = dim (S:: ('n::euclidean_space) set)"
-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 S = span B" using span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto
-hence "independent (f ` B)" using independent_injective_on_span_image[of B f] B_def assms by auto
-moreover have "card (f ` B) = card B" using assms card_image[of f B] subset_inj_on[of f "span S" B] 
-   B_def span_inc by auto
-moreover have "(f ` B) <= (f ` S)" using B_def by auto
-ultimately have "dim (f ` S) >= dim S" 
-  using independent_card_le_dim[of "f ` B" "f ` S"] B_def by auto
-from this show ?thesis using dim_image_le[of f S] assms by auto
+  fixes f :: "'n::euclidean_space => 'm::euclidean_space"
+  assumes lf: "linear f" and fi: "inj_on f (span S)" 
+  shows "dim (f ` S) = dim (S:: ('n::euclidean_space) set)"
+proof -
+  obtain B where B_def: "B<=S & independent B & S <= span B & 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
+  then have "independent (f ` B)"
+    using independent_injective_on_span_image[of B f] B_def assms by auto
+  moreover have "card (f ` B) = card B"
+    using assms card_image[of f B] subset_inj_on[of f "span S" B] B_def span_inc by auto
+  moreover have "(f ` B) <= (f ` S)" using B_def by auto
+  ultimately have "dim (f ` S) >= dim S"
+    using independent_card_le_dim[of "f ` B" "f ` S"] B_def by auto
+  then show ?thesis using dim_image_le[of f S] assms by auto
 qed
 
 lemma linear_injective_on_subspace_0:
-assumes lf: "linear f" and "subspace S"
+  assumes lf: "linear f" and "subspace S"
   shows "inj_on f S <-> (!x : S. f x = 0 --> x = 0)"
-proof-
+proof -
   have "inj_on f S <-> (!x : S. !y : S. f x = f y --> x = y)" by (simp add: inj_on_def)
   also have "... <-> (!x : S. !y : S. f x - f y = 0 --> x - y = 0)" by simp
   also have "... <-> (!x : S. !y : S. f (x - y) = 0 --> x - y = 0)"
@@ -96,105 +102,133 @@
   unfolding span_def by (rule hull_eq, rule subspace_Inter)
 
 lemma basis_inj_on: "d \<subseteq> {..<DIM('n)} \<Longrightarrow> inj_on (basis :: nat => 'n::euclidean_space) d"
-  by(auto simp add: inj_on_def euclidean_eq[where 'a='n])
+  by (auto simp add: inj_on_def euclidean_eq[where 'a='n])
   
 lemma finite_substdbasis: "finite {basis i ::'n::euclidean_space |i. i : (d:: nat set)}" (is "finite ?S")
-proof-
+proof -
   have eq: "?S = basis ` d" by blast
-  show ?thesis unfolding eq apply(rule finite_subset[OF _ range_basis_finite]) by auto
-qed
-
-lemma card_substdbasis: assumes "d \<subseteq> {..<DIM('n::euclidean_space)}"
+  show ?thesis
+    unfolding eq
+    apply (rule finite_subset[OF _ range_basis_finite])
+    apply auto
+    done
+qed
+
+lemma card_substdbasis:
+  assumes "d \<subseteq> {..<DIM('n::euclidean_space)}"
   shows "card {basis i ::'n::euclidean_space | i. i : d} = card d" (is "card ?S = _")
-proof-
+proof -
   have eq: "?S = basis ` d" by blast
-  show ?thesis unfolding eq using card_image[OF basis_inj_on[of d]] assms by auto
-qed
-
-lemma substdbasis_expansion_unique: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
+  show ?thesis
+    unfolding eq
+    using card_image[OF basis_inj_on[of d]] assms by auto
+qed
+
+lemma substdbasis_expansion_unique:
+  assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
   shows "setsum (%i. f i *\<^sub>R basis i) d = (x::'a::euclidean_space)
       <-> (!i<DIM('a). (i:d --> f i = x$$i) & (i ~: d --> x $$ i = 0))"
-proof- 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" apply(rule finite_subset[OF assms]) by fastforce
-  have ***:"\<And>i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\<Sum>x\<in>d. if x = i then f x else 0)"
+proof -
+  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" apply(rule finite_subset[OF assms]) by fastforce
+  have ***: "\<And>i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\<Sum>x\<in>d. if x = i then f x else 0)"
     unfolding euclidean_component_setsum euclidean_component_scaleR basis_component *
-    apply(rule setsum_cong2) using assms by auto
-  show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto
-qed
-
-lemma independent_substdbasis: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
-  shows "independent {basis i ::'a::euclidean_space |i. i : (d :: nat set)}" (is "independent ?A")
+    apply (rule setsum_cong2)
+    using assms apply auto
+    done
+  show ?thesis
+    unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto
+qed
+
+lemma independent_substdbasis:
+  assumes "d \<subseteq> {..<DIM('a::euclidean_space)}"
+  shows "independent {basis i ::'a::euclidean_space |i. i : (d :: nat set)}"
+  (is "independent ?A")
 proof -
   have *: "{basis i |i. i < DIM('a)} = basis ` {..<DIM('a)}" by auto
   show ?thesis
     apply(intro independent_mono[of "{basis i ::'a |i. i : {..<DIM('a::euclidean_space)}}" "?A"] )
-    using independent_basis[where 'a='a] assms by (auto simp: *)
+    using independent_basis[where 'a='a] assms apply (auto simp: *)
+    done
 qed
 
 lemma dim_cball: 
-assumes "0<e"
-shows "dim (cball (0 :: 'n::euclidean_space) e) = DIM('n)"
-proof-
-{ fix x :: "'n::euclidean_space" def y == "(e/norm x) *\<^sub>R x"
-  hence "y : cball 0 e" using cball_def dist_norm[of 0 y] assms by auto
-  moreover have "x = (norm x/e) *\<^sub>R y" using y_def assms by simp
-  moreover hence "x = (norm x/e) *\<^sub>R y"  by auto
-  ultimately have "x : span (cball 0 e)"
-     using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"] by auto
-} hence "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)" by auto 
-from this show ?thesis using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp add: dim_UNIV)
+  assumes "0<e"
+  shows "dim (cball (0 :: 'n::euclidean_space) e) = DIM('n)"
+proof -
+  { fix x :: "'n::euclidean_space"
+    def y == "(e/norm x) *\<^sub>R x"
+    then have "y : cball 0 e" using cball_def dist_norm[of 0 y] assms by auto
+    moreover have "x = (norm x/e) *\<^sub>R y" using y_def assms by simp
+    moreover hence "x = (norm x/e) *\<^sub>R y" by auto
+    ultimately have "x : 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)" 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"
-assumes "independent B"
-shows "finite B & card B = dim (span B)" 
+  fixes B :: "('n::euclidean_space) set"
+  assumes "independent B"
+  shows "finite B & 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 ~= 0 ==> EX a:A. f a ~= 0"
-  apply(rule ccontr) by auto
+  by (rule ccontr) auto
 
 lemma translate_inj_on: 
-fixes A :: "('a::ab_group_add) set"
-shows "inj_on (%x. a+x) A" unfolding inj_on_def by auto
+  fixes A :: "('a::ab_group_add) set"
+  shows "inj_on (%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" by auto
+  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"
-  shows "A=B"
-proof-
-  have "(%x. -a+x) ` ((%x. a+x) ` A) = (%x. -a+x) ` ((%x. a+x) ` B)" using assms by auto
-  from this show ?thesis using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto 
+  shows "A = B"
+proof -
+  have "(%x. -a+x) ` ((%x. a+x) ` A) = (%x. -a+x) ` ((%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
 qed
 
 lemma translation_galois:
   fixes a :: "'a::ab_group_add"
   shows "T=((\<lambda>x. a+x) ` S) <-> S=((\<lambda>x. (-a)+x) ` T)"
   using translation_assoc[of "-a" a S] apply auto
-  using translation_assoc[of a "-a" T] by auto
+  using translation_assoc[of a "-a" T] apply auto
+  done
 
 lemma translation_inverse_subset:
   assumes "((%x. -a+x) ` V) <= (S :: 'n::ab_group_add set)" 
   shows "V <= ((%x. a+x) ` S)"
-proof-
-{ fix x assume "x:V" hence "x-a : S" using assms by auto 
-  hence "x : {a + v |v. v : S}" apply auto apply (rule exI[of _ "x-a"]) apply simp done 
-  hence "x : ((%x. a+x) ` S)" by auto }
-  from this show ?thesis by auto
+proof -
+  { fix x
+    assume "x:V"
+    then have "x-a : S" using assms by auto
+    then have "x : {a + v |v. v : S}"
+      apply auto
+      apply (rule exI[of _ "x-a"])
+      apply simp
+      done
+    then have "x : ((%x. a+x) ` S)" by auto
+  } then show ?thesis by auto
 qed
 
 lemma basis_to_basis_subspace_isomorphism:
   assumes s: "subspace (S:: ('n::euclidean_space) set)"
-  and t: "subspace (T :: ('m::euclidean_space) set)"
-  and d: "dim S = dim T"
-  and B: "B <= S" "independent B" "S <= span B" "card B = dim S"
-  and C: "C <= T" "independent C" "T <= span C" "card C = dim T"
+    and t: "subspace (T :: ('m::euclidean_space) set)"
+    and d: "dim S = dim T"
+    and B: "B <= S" "independent B" "S <= span B" "card B = dim S"
+    and C: "C <= T" "independent C" "T <= span C" "card C = dim T"
   shows "EX f. linear f & f ` B = C & f ` S = T & inj_on f S"
-proof-
+proof -
 (* Proof is a modified copy of the proof of similar lemma subspace_isomorphism
 *)
   from B independent_bound have fB: "finite B" by blast
@@ -214,13 +248,13 @@
   have gi: "inj_on g B" using f(2) g(2)
     by (auto simp add: inj_on_def)
   note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi]
-  {fix x y assume x: "x \<in> S" and y: "y \<in> S" and gxy:"g x = g y"
+  { fix x y
+    assume x: "x \<in> S" and y: "y \<in> S" and gxy: "g x = g y"
     from B(3) x y have x': "x \<in> span B" and y': "y \<in> span B" by blast+
     from gxy have th0: "g (x - y) = 0" by (simp add: linear_sub[OF g(1)])
     have th1: "x - y \<in> span B" using x' y' by (metis span_sub)
-    have "x=y" using g0[OF th1 th0] by simp }
-  then have giS: "inj_on g S"
-    unfolding inj_on_def by blast
+    have "x=y" using g0[OF th1 th0] by simp
+  } then have giS: "inj_on g S" unfolding inj_on_def by blast
   from span_subspace[OF B(1,3) s]
   have "g ` S = span (g ` B)" by (simp add: span_linear_image[OF g(1)])
   also have "\<dots> = span C" unfolding gBC ..
@@ -236,28 +270,29 @@
   by (rule image_closure_subset)
 
 lemma closure_linear_image:
-fixes f :: "('m::euclidean_space) => ('n::real_normed_vector)"
-assumes "linear f"
-shows "f ` (closure S) <= closure (f ` S)"
+  fixes f :: "('m::euclidean_space) => ('n::real_normed_vector)"
+  assumes "linear f"
+  shows "f ` (closure S) <= 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) => ('n::euclidean_space)"
-assumes "linear f" "inj f"
-shows "f ` (closure S) = closure (f ` S)"
-proof-
-obtain f' where f'_def: "linear f' & f o f' = id & f' o f = id" 
-   using assms linear_injective_isomorphism[of f] isomorphism_expand by auto
-hence "f' ` closure (f ` S) <= closure (S)"
-   using closure_linear_image[of f' "f ` S"] image_compose[of f' f] by auto
-hence "f ` f' ` closure (f ` S) <= f ` closure (S)" by auto
-hence "closure (f ` S) <= f ` closure (S)" using image_compose[of f f' "closure (f ` S)"] f'_def by auto
-from this show ?thesis using closure_linear_image[of f S] assms by auto 
+  fixes f :: "('n::euclidean_space) => ('n::euclidean_space)"
+  assumes "linear f" "inj f"
+  shows "f ` (closure S) = closure (f ` S)"
+proof -
+  obtain f' where f'_def: "linear f' & f o f' = id & f' o f = id"
+    using assms linear_injective_isomorphism[of f] isomorphism_expand by auto
+  then have "f' ` closure (f ` S) <= closure (S)"
+    using closure_linear_image[of f' "f ` S"] image_compose[of f' f] by auto
+  then have "f ` f' ` closure (f ` S) <= f ` closure (S)" by auto
+  then have "closure (f ` S) <= 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
 
 lemma closure_direct_sum:
-shows "closure (S <*> T) = closure S <*> closure T"
+  shows "closure (S <*> T) = closure S <*> closure T"
   by (rule closure_Times)
 
 lemma closure_scaleR:
@@ -265,58 +300,73 @@
   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)"
-    using bounded_linear_scaleR_right
-    by (rule closure_bounded_linear_image)
+    using bounded_linear_scaleR_right by (rule closure_bounded_linear_image)
   show "closure ((op *\<^sub>R c) ` S) \<subseteq> (op *\<^sub>R c) ` (closure S)"
-    by (intro closure_minimal image_mono closure_subset
-      closed_scaling closed_closure)
-qed
-
-lemma fst_linear: "linear fst" unfolding linear_def by (simp add: algebra_simps)
-
-lemma snd_linear: "linear snd" unfolding linear_def by (simp add: algebra_simps)
-
-lemma fst_snd_linear: "linear (%(x,y). x + y)" unfolding linear_def by (simp add: algebra_simps)
+    by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
+qed
+
+lemma fst_linear: "linear fst"
+  unfolding linear_def by (simp add: algebra_simps)
+
+lemma snd_linear: "linear snd"
+  unfolding linear_def by (simp add: algebra_simps)
+
+lemma fst_snd_linear: "linear (%(x,y). x + y)"
+  unfolding linear_def by (simp add: algebra_simps)
 
 lemma scaleR_2:
   fixes x :: "'a::real_vector"
   shows "scaleR 2 x = x + x"
-unfolding one_add_one [symmetric] scaleR_left_distrib by simp
-
-lemma vector_choose_size: "0 <= c ==> \<exists>(x::'a::euclidean_space). norm x = c"
-  apply (rule exI[where x="c *\<^sub>R basis 0 ::'a"]) using DIM_positive[where 'a='a] by auto
-
-lemma setsum_delta_notmem: assumes "x\<notin>s"
+  unfolding one_add_one [symmetric] scaleR_left_distrib by simp
+
+lemma vector_choose_size:
+  "0 <= c ==> \<exists>(x::'a::euclidean_space). norm x = c"
+  apply (rule exI[where x="c *\<^sub>R basis 0 ::'a"])
+  using DIM_positive[where 'a='a] apply auto
+  done
+
+lemma setsum_delta_notmem:
+  assumes "x \<notin> s"
   shows "setsum (\<lambda>y. if (y = x) then P x else Q y) s = setsum Q s"
-        "setsum (\<lambda>y. if (x = y) then P x else Q y) s = setsum Q s"
-        "setsum (\<lambda>y. if (y = x) then P y else Q y) s = setsum Q s"
-        "setsum (\<lambda>y. if (x = y) then P y else Q y) s = setsum Q s"
-  apply(rule_tac [!] setsum_cong2) using assms by auto
+    and "setsum (\<lambda>y. if (x = y) then P x else Q y) s = setsum Q s"
+    and "setsum (\<lambda>y. if (y = x) then P y else Q y) s = setsum Q s"
+    and "setsum (\<lambda>y. if (x = y) then P y else Q y) s = setsum Q s"
+  apply(rule_tac [!] setsum_cong2)
+  using assms apply auto
+  done
 
 lemma setsum_delta'':
-  fixes s::"'a::real_vector set" assumes "finite s"
+  fixes s::"'a::real_vector set"
+  assumes "finite s"
   shows "(\<Sum>x\<in>s. (if y = x then f x else 0) *\<^sub>R x) = (if y\<in>s then (f y) *\<^sub>R y else 0)"
-proof-
-  have *:"\<And>x y. (if y = x then f x else (0::real)) *\<^sub>R x = (if x=y then (f x) *\<^sub>R x else 0)" by auto
-  show ?thesis unfolding * using setsum_delta[OF assms, of y "\<lambda>x. f x *\<^sub>R x"] by auto
+proof -
+  have *: "\<And>x y. (if y = x then f x else (0::real)) *\<^sub>R x = (if x=y then (f x) *\<^sub>R x else 0)"
+    by auto
+  show ?thesis
+    unfolding * using setsum_delta[OF assms, of y "\<lambda>x. f x *\<^sub>R x"] by auto
 qed
 
 lemma if_smult:"(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)" by auto
 
-lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::'a::ordered_euclidean_space)) ` {a..b} =
-  (if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
+lemma image_smult_interval:
+  "(\<lambda>x. m *\<^sub>R (x::'a::ordered_euclidean_space)) ` {a..b} =
+    (if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
   using image_affinity_interval[of m 0 a b] by auto
 
 lemma dist_triangle_eq:
   fixes x y z :: "'a::real_inner"
   shows "dist x z = dist x y + dist y z \<longleftrightarrow> norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
-proof- have *:"x - y + (y - z) = x - z" by auto
+proof -
+  have *: "x - y + (y - z) = x - z" by auto
   show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *]
-    by(auto simp add:norm_minus_commute) qed
+    by (auto simp add:norm_minus_commute)
+qed
 
 lemma norm_minus_eqI:"x = - y \<Longrightarrow> norm x = norm y" by auto
 
-lemma Min_grI: assumes "finite A" "A \<noteq> {}" "\<forall>a\<in>A. x < a" shows "x < Min A"
+lemma Min_grI:
+  assumes "finite A" "A \<noteq> {}" "\<forall>a\<in>A. x < a"
+  shows "x < Min A"
   unfolding Min_gr_iff[OF assms(1,2)] using assms(3) by auto
 
 lemma norm_lt: "norm x < norm y \<longleftrightarrow> inner x x < inner y y"
@@ -328,12 +378,11 @@
 
 subsection {* Affine set and affine hull *}
 
-definition
-  affine :: "'a::real_vector set \<Rightarrow> bool" where
-  "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
+definition affine :: "'a::real_vector set \<Rightarrow> bool"
+  where "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
 
 lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> s)"
-unfolding affine_def by(metis eq_diff_eq')
+  unfolding affine_def by (metis eq_diff_eq')
 
 lemma affine_empty[intro]: "affine {}"
   unfolding affine_def by auto
@@ -351,167 +400,278 @@
   unfolding affine_def by auto
 
 lemma affine_affine_hull: "affine(affine hull s)"
-  unfolding hull_def using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"]
-  by auto
+  unfolding hull_def
+  using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"] by auto
 
 lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
-by (metis affine_affine_hull hull_same)
+  by (metis affine_affine_hull hull_same)
+
 
 subsubsection {* Some explicit formulations (from Lars Schewe) *}
 
-lemma affine: fixes V::"'a::real_vector set"
-  shows "affine V \<longleftrightarrow> (\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (setsum (\<lambda>x. (u x) *\<^sub>R x)) s \<in> V)"
-unfolding affine_def apply rule apply(rule, rule, rule) apply(erule conjE)+ 
-defer apply(rule, rule, rule, rule, rule) proof-
-  fix x y u v assume as:"x \<in> V" "y \<in> V" "u + v = (1::real)"
+lemma affine:
+  fixes V::"'a::real_vector set"
+  shows "affine V \<longleftrightarrow>
+    (\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (setsum (\<lambda>x. (u x) *\<^sub>R x)) s \<in> V)"
+  unfolding affine_def
+  apply rule
+  apply(rule, rule, rule)
+  apply(erule conjE)+ 
+  defer
+  apply (rule, rule, rule, rule, rule)
+proof -
+  fix x y u v
+  assume as: "x \<in> V" "y \<in> V" "u + v = (1::real)"
     "\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V"
-  thus "u *\<^sub>R x + v *\<^sub>R y \<in> V" apply(cases "x=y")
-    using as(4)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>w. if w = x then u else v"]] and as(1-3) 
-    by(auto simp add: scaleR_left_distrib[THEN sym])
+  then show "u *\<^sub>R x + v *\<^sub>R y \<in> V"
+    apply (cases "x = y")
+    using as(4)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>w. if w = x then u else v"]]
+      and as(1-3)
+    by (auto simp add: scaleR_left_distrib[THEN sym])
 next
-  fix s u assume as:"\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
+  fix s u
+  assume as: "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
     "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = (1::real)"
   def n \<equiv> "card s"
   have "card s = 0 \<or> card s = 1 \<or> card s = 2 \<or> card s > 2" by auto
-  thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" proof(auto simp only: disjE)
-    assume "card s = 2" hence "card s = Suc (Suc 0)" by auto
+  then show "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V"
+  proof (auto simp only: disjE)
+    assume "card s = 2"
+    then have "card s = Suc (Suc 0)" by auto
     then obtain a b where "s = {a, b}" unfolding card_Suc_eq by auto
-    thus ?thesis using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5)
-      by(auto simp add: setsum_clauses(2))
-  next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s)
-      case (Suc n) fix s::"'a set" and u::"'a \<Rightarrow> real"
-      assume IA:"\<And>u s.  \<lbrakk>2 < card s; \<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V; finite s;
-               s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n = card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and
-        as:"Suc n = card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
+    then show ?thesis
+      using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5)
+      by (auto simp add: setsum_clauses(2))
+  next
+    assume "card s > 2"
+    then show ?thesis using as and n_def
+    proof (induct n arbitrary: u s)
+      case 0
+      then show ?case by auto
+    next
+      case (Suc n)
+      fix s :: "'a set" and u :: "'a \<Rightarrow> real"
+      assume IA:
+        "\<And>u s.  \<lbrakk>2 < card s; \<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V; finite s;
+          s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n = card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V"
+        and as:
+          "Suc n = card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
            "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1"
-      have "\<exists>x\<in>s. u x \<noteq> 1" proof(rule_tac ccontr)
-        assume " \<not> (\<exists>x\<in>s. u x \<noteq> 1)" hence "setsum u s = real_of_nat (card s)" unfolding card_eq_setsum by auto
-        thus False 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)
+      have "\<exists>x\<in>s. u x \<noteq> 1"
+      proof (rule ccontr)
+        assume "\<not> ?thesis"
+        then have "setsum u s = real_of_nat (card s)" unfolding card_eq_setsum by auto
+        then show False
+          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
 
-      have c:"card (s - {x}) = card s - 1" apply(rule card_Diff_singleton) using `x\<in>s` as(4) by auto
-      have *:"s = insert x (s - {x})" "finite (s - {x})" using `x\<in>s` and as(4) by auto
-      have **:"setsum u (s - {x}) = 1 - u x"
+      have c: "card (s - {x}) = card s - 1"
+        apply (rule card_Diff_singleton) using `x\<in>s` as(4) by auto
+      have *: "s = insert x (s - {x})" "finite (s - {x})"
+        using `x\<in>s` and as(4) by auto
+      have **: "setsum u (s - {x}) = 1 - u x"
         using setsum_clauses(2)[OF *(2), of u x, unfolded *(1)[THEN sym] as(7)] by auto
-      have ***:"inverse (1 - u x) * setsum u (s - {x}) = 1" unfolding ** using `u x \<noteq> 1` by auto
-      have "(\<Sum>xa\<in>s - {x}. (inverse (1 - u x) * u xa) *\<^sub>R xa) \<in> V" proof(cases "card (s - {x}) > 2")
-        case True hence "s - {x} \<noteq> {}" "card (s - {x}) = n" unfolding c and as(1)[symmetric] proof(rule_tac ccontr) 
-          assume "\<not> s - {x} \<noteq> {}" hence "card (s - {x}) = 0" unfolding card_0_eq[OF *(2)] by simp 
-          thus False using True by auto qed auto
-        thus ?thesis apply(rule_tac IA[of "s - {x}" "\<lambda>y. (inverse (1 - u x) * u y)"])
-        unfolding setsum_right_distrib[THEN sym] using as and *** and True by auto
-      next case False hence "card (s - {x}) = Suc (Suc 0)" using as(2) and c by auto
+      have ***: "inverse (1 - u x) * setsum u (s - {x}) = 1"
+        unfolding ** using `u x \<noteq> 1` by auto
+      have "(\<Sum>xa\<in>s - {x}. (inverse (1 - u x) * u xa) *\<^sub>R xa) \<in> V"
+      proof (cases "card (s - {x}) > 2")
+        case True
+        then have "s - {x} \<noteq> {}" "card (s - {x}) = n"
+          unfolding c and as(1)[symmetric]
+        proof (rule_tac ccontr) 
+          assume "\<not> s - {x} \<noteq> {}"
+          then have "card (s - {x}) = 0" unfolding card_0_eq[OF *(2)] by simp 
+          then show False using True by auto
+        qed auto
+        then show ?thesis
+          apply (rule_tac IA[of "s - {x}" "\<lambda>y. (inverse (1 - u x) * u y)"])
+          unfolding setsum_right_distrib[THEN sym] using as and *** and True
+          apply auto
+          done
+      next
+        case False
+        then have "card (s - {x}) = Suc (Suc 0)" using as(2) and c by auto
         then obtain a b where "(s - {x}) = {a, b}" "a\<noteq>b" unfolding card_Suc_eq by auto
-        thus ?thesis using as(3)[THEN bspec[where x=a], THEN bspec[where x=b]]
-          using *** *(2) and `s \<subseteq> V` unfolding setsum_right_distrib by(auto simp add: setsum_clauses(2)) qed
-      hence "u x + (1 - u x) = 1 \<Longrightarrow> u x *\<^sub>R x + (1 - u x) *\<^sub>R ((\<Sum>xa\<in>s - {x}. u xa *\<^sub>R xa) /\<^sub>R (1 - u x)) \<in> V"
-        apply-apply(rule as(3)[rule_format]) 
-        unfolding  RealVector.scaleR_right.setsum using x(1) as(6) by auto
-      thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric]
-         apply(subst *) unfolding setsum_clauses(2)[OF *(2)]
-         using `u x \<noteq> 1` by auto 
-    qed auto
-  next assume "card s = 1" then obtain a where "s={a}" by(auto simp add: card_Suc_eq)
-    thus ?thesis using as(4,5) by simp
-  qed(insert `s\<noteq>{}` `finite s`, auto)
+        then show ?thesis using as(3)[THEN bspec[where x=a], THEN bspec[where x=b]]
+          using *** *(2) and `s \<subseteq> V`
+          unfolding setsum_right_distrib by (auto simp add: setsum_clauses(2))
+      qed
+      then have "u x + (1 - u x) = 1 \<Longrightarrow>
+          u x *\<^sub>R x + (1 - u x) *\<^sub>R ((\<Sum>xa\<in>s - {x}. u xa *\<^sub>R xa) /\<^sub>R (1 - u x)) \<in> V"
+        apply -
+        apply (rule as(3)[rule_format])
+        unfolding  RealVector.scaleR_right.setsum
+        using x(1) as(6) apply auto
+        done
+      then show "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V"
+        unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric]
+        apply (subst *)
+        unfolding setsum_clauses(2)[OF *(2)]
+        using `u x \<noteq> 1` apply auto
+        done
+    qed
+  next
+    assume "card s = 1"
+    then obtain a where "s={a}" by (auto simp add: card_Suc_eq)
+    then show ?thesis using as(4,5) by simp
+  qed (insert `s\<noteq>{}` `finite s`, auto)
 qed
 
 lemma affine_hull_explicit:
   "affine hull p = {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> setsum (\<lambda>v. (u v) *\<^sub>R v) s = y}"
-  apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq
-  apply (erule exE)+ apply(erule conjE)+ prefer 2 apply rule proof-
-  fix x assume "x\<in>p" thus "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
-    apply(rule_tac x="{x}" in exI, rule_tac x="\<lambda>x. 1" in exI) by auto
+  apply (rule hull_unique)
+  apply (subst subset_eq)
+  prefer 3
+  apply rule
+  unfolding mem_Collect_eq
+  apply (erule exE)+
+  apply (erule conjE)+
+  prefer 2
+  apply rule
+proof -
+  fix x
+  assume "x\<in>p"
+  then show "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
+    apply (rule_tac x="{x}" in exI, rule_tac x="\<lambda>x. 1" in exI)
+    apply auto
+    done
 next
-  fix t x s u assume as:"p \<subseteq> t" "affine t" "finite s" "s \<noteq> {}" "s \<subseteq> p" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x" 
-  thus "x \<in> t" using as(2)[unfolded affine, THEN spec[where x=s], THEN spec[where x=u]] by auto
+  fix t x s u
+  assume as: "p \<subseteq> t" "affine t" "finite s" "s \<noteq> {}" "s \<subseteq> p" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
+  then show "x \<in> t"
+    using as(2)[unfolded affine, THEN spec[where x=s], THEN spec[where x=u]] by auto
 next
-  show "affine {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y}" unfolding affine_def
-    apply(rule,rule,rule,rule,rule) unfolding mem_Collect_eq proof-
-    fix u v ::real assume uv:"u + v = 1"
-    fix x assume "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
-    then obtain sx ux where x:"finite sx" "sx \<noteq> {}" "sx \<subseteq> p" "setsum ux sx = 1" "(\<Sum>v\<in>sx. ux v *\<^sub>R v) = x" by auto
+  show "affine {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y}"
+    unfolding affine_def
+    apply (rule, rule, rule, rule, rule)
+    unfolding mem_Collect_eq
+  proof -
+    fix u v :: real
+    assume uv: "u + v = 1"
+    fix x
+    assume "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
+    then obtain sx ux where
+      x: "finite sx" "sx \<noteq> {}" "sx \<subseteq> p" "setsum ux sx = 1" "(\<Sum>v\<in>sx. ux v *\<^sub>R v) = x" by auto
     fix y assume "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
-    then obtain sy uy where y:"finite sy" "sy \<noteq> {}" "sy \<subseteq> p" "setsum uy sy = 1" "(\<Sum>v\<in>sy. uy v *\<^sub>R v) = y" by auto
-    have xy:"finite (sx \<union> sy)" using x(1) y(1) by auto
-    have **:"(sx \<union> sy) \<inter> sx = sx" "(sx \<union> sy) \<inter> sy = sy" by auto
-    show "\<exists>s ua. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum ua s = 1 \<and> (\<Sum>v\<in>s. ua v *\<^sub>R v) = u *\<^sub>R x + v *\<^sub>R y"
-      apply(rule_tac x="sx \<union> sy" in exI)
-      apply(rule_tac x="\<lambda>a. (if a\<in>sx then u * ux a else 0) + (if a\<in>sy then v * uy a else 0)" in exI)
-      unfolding scaleR_left_distrib setsum_addf if_smult scaleR_zero_left  ** setsum_restrict_set[OF xy, THEN sym]
+    then obtain sy uy where
+      y: "finite sy" "sy \<noteq> {}" "sy \<subseteq> p" "setsum uy sy = 1" "(\<Sum>v\<in>sy. uy v *\<^sub>R v) = y" by auto
+    have xy: "finite (sx \<union> sy)" using x(1) y(1) by auto
+    have **: "(sx \<union> sy) \<inter> sx = sx" "(sx \<union> sy) \<inter> sy = sy" by auto
+    show "\<exists>s ua. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and>
+        setsum ua s = 1 \<and> (\<Sum>v\<in>s. ua v *\<^sub>R v) = u *\<^sub>R x + v *\<^sub>R y"
+      apply (rule_tac x="sx \<union> sy" in exI)
+      apply (rule_tac x="\<lambda>a. (if a\<in>sx then u * ux a else 0) + (if a\<in>sy then v * uy a else 0)" in exI)
+      unfolding scaleR_left_distrib setsum_addf if_smult scaleR_zero_left ** setsum_restrict_set[OF xy, THEN sym]
       unfolding scaleR_scaleR[THEN sym] RealVector.scaleR_right.setsum [symmetric] and setsum_right_distrib[THEN sym]
-      unfolding x y using x(1-3) y(1-3) uv by simp qed qed
+      unfolding x y
+      using x(1-3) y(1-3) uv apply simp
+      done
+  qed
+qed
 
 lemma affine_hull_finite:
   assumes "finite s"
   shows "affine hull s = {y. \<exists>u. setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
   unfolding affine_hull_explicit and set_eq_iff and mem_Collect_eq apply (rule,rule)
-  apply(erule exE)+ apply(erule conjE)+ defer apply(erule exE) apply(erule conjE) proof-
-  fix x u assume "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
-  thus "\<exists>sa u. finite sa \<and> \<not> (\<forall>x. (x \<in> sa) = (x \<in> {})) \<and> sa \<subseteq> s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = x"
-    apply(rule_tac x=s in exI, rule_tac x=u in exI) using assms by auto
+  apply(erule exE)+
+  apply(erule conjE)+
+  defer
+  apply (erule exE)
+  apply (erule conjE)
+proof -
+  fix x u
+  assume "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
+  then show "\<exists>sa u. finite sa \<and>
+      \<not> (\<forall>x. (x \<in> sa) = (x \<in> {})) \<and> sa \<subseteq> s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = x"
+    apply (rule_tac x=s in exI, rule_tac x=u in exI)
+    using assms apply auto
+    done
 next
-  fix x t u assume "t \<subseteq> s" hence *:"s \<inter> t = t" by auto
+  fix x t u
+  assume "t \<subseteq> s"
+  then have *: "s \<inter> t = t" by auto
   assume "finite t" "\<not> (\<forall>x. (x \<in> t) = (x \<in> {}))" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"
-  thus "\<exists>u. setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
-    unfolding if_smult scaleR_zero_left and setsum_restrict_set[OF assms, THEN sym] and * by auto qed
+  then show "\<exists>u. setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
+    apply (rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
+    unfolding if_smult scaleR_zero_left and setsum_restrict_set[OF assms, THEN sym] and *
+    apply auto
+    done
+qed
+
 
 subsubsection {* Stepping theorems and hence small special cases *}
 
 lemma affine_hull_empty[simp]: "affine hull {} = {}"
-  apply(rule hull_unique) by auto
+  by (rule hull_unique) auto
 
 lemma affine_hull_finite_step:
   fixes y :: "'a::real_vector"
-  shows "(\<exists>u. setsum u {} = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) {} = y) \<longleftrightarrow> w = 0 \<and> y = 0" (is ?th1)
-  "finite s \<Longrightarrow> (\<exists>u. setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y) \<longleftrightarrow>
-                (\<exists>v u. setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?as \<Longrightarrow> (?lhs = ?rhs)")
-proof-
+  shows
+    "(\<exists>u. setsum u {} = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) {} = y) \<longleftrightarrow> w = 0 \<and> y = 0" (is ?th1)
+    "finite s \<Longrightarrow>
+      (\<exists>u. setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y) \<longleftrightarrow>
+      (\<exists>v u. setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?as \<Longrightarrow> (?lhs = ?rhs)")
+proof -
   show ?th1 by simp
-  assume ?as 
+  assume ?as
   { assume ?lhs
     then obtain u where u:"setsum u (insert a s) = w \<and> (\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y" by auto
-    have ?rhs proof(cases "a\<in>s")
-      case True hence *:"insert a s = s" by auto
+    have ?rhs
+    proof (cases "a \<in> s")
+      case True
+      then have *: "insert a s = s" by auto
       show ?thesis using u[unfolded *] apply(rule_tac x=0 in exI) by auto
     next
-      case False thus ?thesis apply(rule_tac x="u a" in exI) using u and `?as` by auto 
-    qed  } moreover
+      case False
+      then show ?thesis
+        apply (rule_tac x="u a" in exI)
+        using u and `?as` apply auto
+        done
+    qed }
+  moreover
   { assume ?rhs
     then obtain v u where vu:"setsum u s = w - v"  "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto
-    have *:"\<And>x M. (if x = a then v else M) *\<^sub>R x = (if x = a then v *\<^sub>R x else M *\<^sub>R x)" by auto
-    have ?lhs proof(cases "a\<in>s")
-      case True thus ?thesis
-        apply(rule_tac x="\<lambda>x. (if x=a then v else 0) + u x" in exI)
-        unfolding setsum_clauses(2)[OF `?as`]  apply simp
+    have *: "\<And>x M. (if x = a then v else M) *\<^sub>R x = (if x = a then v *\<^sub>R x else M *\<^sub>R x)" by auto
+    have ?lhs
+    proof (cases "a \<in> s")
+      case True
+      then show ?thesis
+        apply (rule_tac x="\<lambda>x. (if x=a then v else 0) + u x" in exI)
+        unfolding setsum_clauses(2)[OF `?as`] apply simp
         unfolding scaleR_left_distrib and setsum_addf 
         unfolding vu and * and scaleR_zero_left
-        by (auto simp add: setsum_delta[OF `?as`])
+        apply (auto simp add: setsum_delta[OF `?as`])
+        done
     next
       case False 
-      hence **:"\<And>x. x \<in> s \<Longrightarrow> u x = (if x = a then v else u x)"
-               "\<And>x. x \<in> s \<Longrightarrow> u x *\<^sub>R x = (if x = a then v *\<^sub>R x else u x *\<^sub>R x)" by auto
+      then have **:
+        "\<And>x. x \<in> s \<Longrightarrow> u x = (if x = a then v else u x)"
+        "\<And>x. x \<in> s \<Longrightarrow> u x *\<^sub>R x = (if x = a then v *\<^sub>R x else u x *\<^sub>R x)" by auto
       from False show ?thesis
-        apply(rule_tac x="\<lambda>x. if x=a then v else u x" in exI)
+        apply (rule_tac x="\<lambda>x. if x=a then v else u x" in exI)
         unfolding setsum_clauses(2)[OF `?as`] and * using vu
         using setsum_cong2[of s "\<lambda>x. u x *\<^sub>R x" "\<lambda>x. if x = a then v *\<^sub>R x else u x *\<^sub>R x", OF **(2)]
-        using setsum_cong2[of s u "\<lambda>x. if x = a then v else u x", OF **(1)] by auto  
-    qed }
+        using setsum_cong2[of s u "\<lambda>x. if x = a then v else u x", OF **(1)]
+        apply auto
+        done
+    qed
+  }
   ultimately show "?lhs = ?rhs" by blast
 qed
 
 lemma affine_hull_2:
   fixes a b :: "'a::real_vector"
   shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs")
-proof-
-  have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" 
-         "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
+proof -
+  have *:
+    "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" 
+    "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
   have "?lhs = {y. \<exists>u. setsum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}"
     using affine_hull_finite[of "{a,b}"] by auto
   also have "\<dots> = {y. \<exists>v u. u b = 1 - v \<and> u b *\<^sub>R b = y - v *\<^sub>R a}"
-    by(simp add: affine_hull_finite_step(2)[of "{b}" a]) 
+    by (simp add: affine_hull_finite_step(2)[of "{b}" a])
   also have "\<dots> = ?rhs" unfolding * by auto
   finally show ?thesis by auto
 qed
@@ -519,13 +679,17 @@
 lemma affine_hull_3:
   fixes a b c :: "'a::real_vector"
   shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs")
-proof-
-  have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" 
-         "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
-  show ?thesis apply(simp add: affine_hull_finite affine_hull_finite_step)
-    unfolding * apply auto
-    apply(rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto
-    apply(rule_tac x=u in exI) by force
+proof -
+  have *:
+    "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" 
+    "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
+  show ?thesis
+    apply (simp add: affine_hull_finite affine_hull_finite_step)
+    unfolding *
+    apply auto
+    apply (rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto
+    apply (rule_tac x=u in exI) apply force
+    done
 qed
 
 lemma mem_affine:
@@ -536,220 +700,274 @@
 lemma mem_affine_3:
   assumes "affine S" "x : S" "y : S" "z : S" "u+v+w=1"
   shows "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : S"
-proof-
-have "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : affine hull {x, y, z}"
-  using affine_hull_3[of x y z] assms by auto
-moreover have " affine hull {x, y, z} <= affine hull S" 
-  using hull_mono[of "{x, y, z}" "S"] assms by auto
-moreover have "affine hull S = S" 
-  using assms affine_hull_eq[of S] by auto
-ultimately show ?thesis by auto 
+proof -
+  have "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : affine hull {x, y, z}"
+    using affine_hull_3[of x y z] assms by auto
+  moreover
+  have "affine hull {x, y, z} <= affine hull S"
+    using hull_mono[of "{x, y, z}" "S"] assms by auto
+  moreover
+  have "affine hull S = S" using assms affine_hull_eq[of S] by auto
+  ultimately show ?thesis by auto 
 qed
 
 lemma mem_affine_3_minus:
   assumes "affine S" "x : S" "y : S" "z : S"
   shows "x + v *\<^sub>R (y-z) : S"
-using mem_affine_3[of S x y z 1 v "-v"] assms by (simp add: algebra_simps)
+  using mem_affine_3[of S x y z 1 v "-v"] assms by (simp add: algebra_simps)
 
 
 subsubsection {* Some relations between affine hull and subspaces *}
 
 lemma affine_hull_insert_subset_span:
-  shows "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
-  unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq
-  apply(rule,rule) apply(erule exE)+ apply(erule conjE)+ proof-
-  fix x t u assume as:"finite t" "t \<noteq> {}" "t \<subseteq> insert a s" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"
+  "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
+  unfolding subset_eq Ball_def
+  unfolding affine_hull_explicit span_explicit mem_Collect_eq
+  apply (rule, rule) apply (erule exE)+ apply (erule conjE)+
+proof -
+  fix x t u
+  assume as: "finite t" "t \<noteq> {}" "t \<subseteq> insert a s" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"
   have "(\<lambda>x. x - a) ` (t - {a}) \<subseteq> {x - a |x. x \<in> s}" using as(3) by auto
-  thus "\<exists>v. x = a + v \<and> (\<exists>S u. finite S \<and> S \<subseteq> {x - a |x. x \<in> s} \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = v)"
-    apply(rule_tac x="x - a" in exI)
+  then show "\<exists>v. x = a + v \<and> (\<exists>S u. finite S \<and> S \<subseteq> {x - a |x. x \<in> s} \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = v)"
+    apply (rule_tac x="x - a" in exI)
     apply (rule conjI, simp)
-    apply(rule_tac x="(\<lambda>x. x - a) ` (t - {a})" in exI)
-    apply(rule_tac x="\<lambda>x. u (x + a)" in exI)
+    apply (rule_tac x="(\<lambda>x. x - a) ` (t - {a})" in exI)
+    apply (rule_tac x="\<lambda>x. u (x + a)" in exI)
     apply (rule conjI) using as(1) apply simp
     apply (erule conjI)
     using as(1)
-    apply (simp add: setsum_reindex[unfolded inj_on_def] scaleR_right_diff_distrib setsum_subtractf scaleR_left.setsum[THEN sym] setsum_diff1 scaleR_left_diff_distrib)
-    unfolding as by simp qed
+    apply (simp add: setsum_reindex[unfolded inj_on_def] scaleR_right_diff_distrib
+      setsum_subtractf scaleR_left.setsum[THEN sym] setsum_diff1 scaleR_left_diff_distrib)
+    unfolding as
+    apply simp
+    done
+qed
 
 lemma affine_hull_insert_span:
   assumes "a \<notin> s"
-  shows "affine hull (insert a s) =
-            {a + v | v . v \<in> span {x - a | x.  x \<in> s}}"
-  apply(rule, rule affine_hull_insert_subset_span) unfolding subset_eq Ball_def
-  unfolding affine_hull_explicit and mem_Collect_eq 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" unfolding span_explicit by auto
+  shows "affine hull (insert a s) = {a + v | v . v \<in> span {x - a | x.  x \<in> s}}"
+  apply (rule, rule affine_hull_insert_subset_span)
+  unfolding subset_eq Ball_def
+  unfolding affine_hull_explicit and mem_Collect_eq
+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"
+    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" unfolding f_def using obt 
-    by(auto simp add: setsum_reindex[unfolded inj_on_def])
-  have *:"f \<inter> {a} = {}" "f \<inter> - {a} = f" using f(2) assms by auto
+  have f:"finite f" "f \<subseteq> s" "(\<Sum>v\<in>f. u (v - a) *\<^sub>R (v - a)) = y - a"
+    unfolding f_def using obt by (auto simp add: setsum_reindex[unfolded inj_on_def])
+  have *: "f \<inter> {a} = {}" "f \<inter> - {a} = f" using f(2) assms by auto
   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)
+    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
     unfolding setsum_cases[OF f(1), of "\<lambda>x. x = a"]
-    by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps *) qed
+    apply (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps *)
+    done
+qed
 
 lemma affine_hull_span:
   assumes "a \<in> s"
   shows "affine hull s = {a + v | v. v \<in> span {x - a | x. x \<in> s - {a}}}"
   using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
 
+
 subsubsection {* Parallel affine sets *}
 
 definition affine_parallel :: "'a::real_vector set => 'a::real_vector set => bool"
-where "affine_parallel S T = (? a. T = ((%x. a + x) ` S))"
+  where "affine_parallel S T = (? a. T = ((%x. a + x) ` S))"
 
 lemma affine_parallel_expl_aux:
-   fixes S T :: "'a::real_vector set"
-   assumes "!x. (x : S <-> (a+x) : T)" 
-   shows "T = ((%x. a + x) ` S)"
-proof-
-{ fix x assume "x : T" hence "(-a)+x : S" using assms by auto
-  hence " x : ((%x. a + x) ` S)" using imageI[of "-a+x" S "(%x. a+x)"] by auto}
-moreover have "T >= ((%x. a + x) ` S)" using assms by auto 
-ultimately show ?thesis by auto
-qed
-
-lemma affine_parallel_expl: 
-   "affine_parallel S T = (? a. !x. (x : S <-> (a+x) : T))" 
-   unfolding affine_parallel_def using affine_parallel_expl_aux[of S _ T] by auto
-
-lemma affine_parallel_reflex: "affine_parallel S S" unfolding affine_parallel_def apply (rule exI[of _ "0"]) by auto
+  fixes S T :: "'a::real_vector set"
+  assumes "!x. (x : S <-> (a+x) : T)" 
+  shows "T = ((%x. a + x) ` S)"
+proof -
+  { fix x
+    assume "x : T"
+    then have "(-a)+x : S" using assms by auto
+    then have "x : ((%x. a + x) ` S)"
+      using imageI[of "-a+x" S "(%x. a+x)"] by auto }
+  moreover have "T >= ((%x. a + x) ` S)" using assms by auto 
+  ultimately show ?thesis by auto
+qed
+
+lemma affine_parallel_expl: "affine_parallel S T = (? a. !x. (x : S <-> (a+x) : T))"
+  unfolding affine_parallel_def
+  using affine_parallel_expl_aux[of S _ T] by auto
+
+lemma affine_parallel_reflex: "affine_parallel S S"
+  unfolding affine_parallel_def apply (rule exI[of _ "0"]) by auto
 
 lemma affine_parallel_commut:
-assumes "affine_parallel A B" shows "affine_parallel B A" 
-proof-
-from assms obtain a where "B=((%x. a + x) ` A)" unfolding affine_parallel_def by auto 
-from this show ?thesis using translation_galois[of B a A] unfolding affine_parallel_def by auto
+  assumes "affine_parallel A B"
+  shows "affine_parallel B A"
+proof -
+  from assms obtain a where "B=((%x. a + x) ` A)"
+    unfolding affine_parallel_def by auto
+  then show ?thesis
+    using translation_galois[of B a A] unfolding affine_parallel_def by auto
 qed
 
 lemma affine_parallel_assoc:
-assumes "affine_parallel A B" "affine_parallel B C"
-shows "affine_parallel A C" 
-proof-
-from assms obtain ab where "B=((%x. ab + x) ` A)" unfolding affine_parallel_def by auto 
-moreover 
-from assms obtain bc where "C=((%x. bc + x) ` B)" unfolding affine_parallel_def by auto
-ultimately show ?thesis using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto 
+  assumes "affine_parallel A B" "affine_parallel B C"
+  shows "affine_parallel A C" 
+proof -
+  from assms obtain ab where "B=((%x. ab + x) ` A)"
+    unfolding affine_parallel_def by auto 
+  moreover 
+  from assms obtain bc where "C=((%x. bc + x) ` B)"
+    unfolding affine_parallel_def by auto
+  ultimately show ?thesis
+    using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto
 qed
 
 lemma affine_translation_aux:
   fixes a :: "'a::real_vector"
   assumes "affine ((%x. a + x) ` S)" shows "affine S"
 proof-
-{ fix x y u v
-  assume xy: "x : S" "y : S" "(u :: real)+v=1"
-  hence "(a+x):((%x. a + x) ` S)" "(a+y):((%x. a + x) ` S)" by auto
-  hence h1: "u *\<^sub>R  (a+x) + v *\<^sub>R (a+y) : ((%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)" 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)" using h1 by auto
-  hence "u *\<^sub>R x + v *\<^sub>R y : S" by auto
-} from this show ?thesis unfolding affine_def by auto
+  { fix x y u v
+    assume xy: "x : S" "y : S" "(u :: real)+v=1"
+    then have "(a+x):((%x. a + x) ` S)" "(a+y):((%x. a + x) ` S)" by auto
+    then have h1: "u *\<^sub>R  (a+x) + v *\<^sub>R (a+y) : ((%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)"
+      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)" using h1 by auto
+    then have "u *\<^sub>R x + v *\<^sub>R y : S" by auto
+  }
+  then show ?thesis unfolding affine_def by auto
 qed
 
 lemma affine_translation:
   fixes a :: "'a::real_vector"
   shows "affine S <-> affine ((%x. a + x) ` S)"
-proof-
-have "affine S ==> affine ((%x. a + x) ` S)" using affine_translation_aux[of "-a" "((%x. a + x) ` S)"]  using translation_assoc[of "-a" a S] by auto
-from this show ?thesis using affine_translation_aux by auto
+proof -
+  have "affine S ==> affine ((%x. a + x) ` S)"
+    using affine_translation_aux[of "-a" "((%x. a + x) ` S)"]
+    using translation_assoc[of "-a" a S] by auto
+  then show ?thesis using affine_translation_aux by auto
 qed
 
 lemma parallel_is_affine:
-fixes S T :: "'a::real_vector set"
-assumes "affine S" "affine_parallel S T"
-shows "affine T"
-proof-
-  from assms obtain a where "T=((%x. a + x) ` S)" unfolding affine_parallel_def by auto 
-  from this show ?thesis using affine_translation assms by auto
+  fixes S T :: "'a::real_vector set"
+  assumes "affine S" "affine_parallel S T"
+  shows "affine T"
+proof -
+  from assms obtain a where "T=((%x. a + x) ` S)"
+    unfolding affine_parallel_def by auto 
+  then show ?thesis using affine_translation assms by auto
 qed
 
 lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s"
   unfolding subspace_def affine_def by auto
 
+
 subsubsection {* Subspace parallel to an affine set *}
 
-lemma subspace_affine:
-  shows "subspace S <-> (affine S & 0 : S)"
-proof-
-have h0: "subspace S ==> (affine S & 0 : S)" using subspace_imp_affine[of S] subspace_0 by auto
-{ assume assm: "affine S & 0 : S"
-  { fix c :: real 
-    fix x assume x_def: "x : 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" using affine_alt[of S] assm x_def by auto
-    ultimately have "c *\<^sub>R x : S" by auto
-  } hence h1: "!c. !x : S. c *\<^sub>R x : S" by auto
-  { fix x y assume xy_def: "x : S" "y : S"
-    def u == "(1 :: real)/2"
-    have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)" by auto
-    moreover have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y" by (simp add: algebra_simps)
-    moreover have "(1-u) *\<^sub>R x + u *\<^sub>R y : S" using affine_alt[of S] assm xy_def by auto
-    ultimately have "(1/2) *\<^sub>R (x+y) : S" using u_def by auto
-    moreover have "(x+y) = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))" by auto
-    ultimately have "(x+y) : S" using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto
-  } hence "!x : S. !y : S. (x+y) : S" by auto 
-  hence "subspace S" using h1 assm unfolding subspace_def by auto
-} from this show ?thesis using h0 by metis
+lemma subspace_affine: "subspace S <-> (affine S & 0 : S)"
+proof -
+  have h0: "subspace S ==> (affine S & 0 : S)"
+    using subspace_imp_affine[of S] subspace_0 by auto
+  { assume assm: "affine S & 0 : S"
+    { fix c :: real 
+      fix x assume x_def: "x : 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" using affine_alt[of S] assm x_def by auto
+      ultimately have "c *\<^sub>R x : S" by auto
+    }
+    then have h1: "!c. !x : S. c *\<^sub>R x : S" by auto
+
+    { fix x y assume xy_def: "x : S" "y : S"
+      def u == "(1 :: real)/2"
+      have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)" by auto
+      moreover
+      have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y" by (simp add: algebra_simps)
+      moreover
+      have "(1-u) *\<^sub>R x + u *\<^sub>R y : S" using affine_alt[of S] assm xy_def by auto
+      ultimately
+      have "(1/2) *\<^sub>R (x+y) : S" using u_def by auto
+      moreover
+      have "(x+y) = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))" by auto
+      ultimately
+      have "(x+y) : S" using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto
+    }
+    then have "!x : S. !y : S. (x+y) : S" by auto 
+    then have "subspace S" using h1 assm unfolding subspace_def by auto
+  }
+  then show ?thesis using h0 by metis
 qed
 
 lemma affine_diffs_subspace:
   assumes "affine S" "a : S"
   shows "subspace ((%x. (-a)+x) ` S)"
-proof-
-have "affine ((%x. (-a)+x) ` S)" using  affine_translation assms by auto  
-moreover have "0 : ((%x. (-a)+x) ` S)" using assms exI[of "(%x. x:S & -a+x=0)" a] by auto
-ultimately show ?thesis using subspace_affine by auto 
+proof -
+  have "affine ((%x. (-a)+x) ` S)"
+    using  affine_translation assms by auto  
+  moreover have "0 : ((%x. (-a)+x) ` S)"
+    using assms exI[of "(%x. x:S & -a+x=0)" a] by auto
+  ultimately show ?thesis using subspace_affine by auto 
 qed
 
 lemma parallel_subspace_explicit:
-assumes "affine S" "a : S"
-assumes "L == {y. ? x : S. (-a)+x=y}" 
-shows "subspace L & affine_parallel S L" 
-proof-
-have par: "affine_parallel S L" unfolding affine_parallel_def using assms by auto
-hence "affine L" using assms parallel_is_affine by auto  
-moreover have "0 : L" using assms apply auto using exI[of "(%x. x:S & -a+x=0)" a] by auto
-ultimately show ?thesis using subspace_affine par by auto 
+  assumes "affine S" "a : S"
+  assumes "L == {y. ? x : S. (-a)+x=y}" 
+  shows "subspace L & affine_parallel S L" 
+proof -
+  have par: "affine_parallel S L"
+    unfolding affine_parallel_def using assms by auto
+  then have "affine L" using assms parallel_is_affine by auto  
+  moreover have "0 : L"
+    using assms apply auto
+    using exI[of "(%x. x:S & -a+x=0)" a] apply auto
+    done
+  ultimately show ?thesis using subspace_affine par by auto 
 qed
 
 lemma parallel_subspace_aux:
-assumes "subspace A" "subspace B" "affine_parallel A B"
-shows "A>=B"
-proof-
-from assms obtain a where a_def: "!x. (x : A <-> (a+x) : B)" using affine_parallel_expl[of A B] by auto
-hence "-a : A" using assms subspace_0[of B] by auto
-hence "a : A" using assms subspace_neg[of A "-a"] by auto
-from this show ?thesis using assms a_def unfolding subspace_def by auto
+  assumes "subspace A" "subspace B" "affine_parallel A B"
+  shows "A>=B"
+proof -
+  from assms obtain a where a_def: "!x. (x : A <-> (a+x) : B)"
+    using affine_parallel_expl[of A B] by auto
+  then have "-a : A" using assms subspace_0[of B] by auto
+  then have "a : A" using assms subspace_neg[of A "-a"] by auto
+  then show ?thesis using assms a_def unfolding subspace_def by auto
 qed
 
 lemma parallel_subspace:
-assumes "subspace A" "subspace B" "affine_parallel A B"
-shows "A=B"
-proof-
-have "A>=B" using assms parallel_subspace_aux by auto
-moreover have "A<=B" using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto
-ultimately show ?thesis by auto  
+  assumes "subspace A" "subspace B" "affine_parallel A B"
+  shows "A = B"
+proof
+  show "A >= B"
+    using assms parallel_subspace_aux by auto
+  show "A <= B"
+    using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto
 qed
 
 lemma affine_parallel_subspace:
-assumes "affine S" "S ~= {}"
-shows "?!L. subspace L & affine_parallel S L" 
-proof-
-have ex: "? L. subspace L & 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"
-  hence "affine_parallel L1 L2" using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto
-  hence "L1=L2" using ass parallel_subspace by auto
-} from this show ?thesis using ex by auto
-qed
+  assumes "affine S" "S ~= {}"
+  shows "?!L. subspace L & affine_parallel S L" 
+proof -
+  have ex: "? L. subspace L & 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"
+    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"
+      using ass parallel_subspace by auto
+  }
+  then show ?thesis using ex by auto
+qed
+
 
 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)"
+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)"
 
 lemma cone_empty[intro, simp]: "cone {}"
   unfolding cone_def by auto
@@ -760,14 +978,16 @@
 lemma cone_Inter[intro]: "(\<forall>s\<in>f. cone s) \<Longrightarrow> cone(\<Inter> f)"
   unfolding cone_def by auto
 
+
 subsubsection {* Conic hull *}
 
 lemma cone_cone_hull: "cone (cone hull s)"
   unfolding hull_def by auto
 
 lemma cone_hull_eq: "(cone hull s = s) \<longleftrightarrow> cone s"
-  apply(rule hull_eq)
-  using cone_Inter unfolding subset_eq by auto
+  apply (rule hull_eq)
+  using cone_Inter unfolding subset_eq apply auto
+  done
 
 lemma mem_cone:
   assumes "cone S" "x : S" "c>=0"
@@ -775,158 +995,207 @@
   using assms cone_def[of S] by auto
 
 lemma cone_contains_0:
-assumes "cone S"
-shows "(S ~= {}) <-> (0 : S)"
-proof-
-{ assume "S ~= {}" from this obtain a where "a:S" by auto
-  hence "0 : S" using assms mem_cone[of S a 0] by auto
-} from this show ?thesis by auto
+  assumes "cone S"
+  shows "(S ~= {}) <-> (0 : S)"
+proof -
+  { assume "S ~= {}" then obtain a where "a:S" by auto
+    then have "0 : S" using assms mem_cone[of S a 0] by auto
+  }
+  then show ?thesis by auto
 qed
 
 lemma cone_0: "cone {0}"
-unfolding cone_def by auto
+  unfolding cone_def by auto
 
 lemma cone_Union[intro]: "(!s:f. cone s) --> (cone (Union f))"
   unfolding cone_def by blast
 
 lemma cone_iff:
-assumes "S ~= {}"
-shows "cone S <-> 0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)"
-proof-
-{ assume "cone S"
-  { fix c assume "(c :: real)>0"
-    { fix x assume "x : S" hence "x : (op *\<^sub>R c) ` S" unfolding image_def
-        using `cone S` `c>0` mem_cone[of S x "1/c"]
-        exI[of "(%t. t:S & x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"] by auto
-    }
-    moreover
-    { fix x assume "x : (op *\<^sub>R c) ` S"
-      (*from this obtain t where "t:S & x = c *\<^sub>R t" by auto*)
-      hence "x:S" using `cone S` `c>0` unfolding cone_def image_def `c>0` by auto
+  assumes "S ~= {}"
+  shows "cone S <-> 0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)"
+proof -
+  { assume "cone S"
+    { fix c
+      assume "(c :: real) > 0"
+      { fix x
+        assume "x : S"
+        then have "x : (op *\<^sub>R c) ` S"
+          unfolding image_def
+          using `cone S` `c>0` mem_cone[of S x "1/c"]
+            exI[of "(%t. t:S & x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"] apply auto
+          done
+      }
+      moreover
+      { fix x assume "x : (op *\<^sub>R c) ` S"
+        (*from this obtain t where "t:S & x = c *\<^sub>R t" by auto*)
+        then have "x:S"
+          using `cone S` `c>0` unfolding cone_def image_def `c>0` by auto
+      }
+      ultimately have "((op *\<^sub>R c) ` S) = S" by auto
     }
-    ultimately have "((op *\<^sub>R c) ` S) = S" by auto
-  } hence "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)" using `cone S` cone_contains_0[of S] assms by auto
-}
-moreover
-{ assume a: "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)"
-  { fix x assume "x:S"
-    fix c1 assume "(c1 :: real)>=0"
-    hence "(c1=0) | (c1>0)" by auto
-    hence "c1 *\<^sub>R x : S" using a `x:S` by auto
+    then have "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)"
+      using `cone S` cone_contains_0[of S] assms by auto
+  }
+  moreover
+  { assume a: "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)"
+    { fix x assume "x:S"
+      fix c1
+      assume "(c1 :: real) >= 0"
+      then have "(c1=0) | (c1>0)" by auto
+      then have "c1 *\<^sub>R x : S" using a `x:S` by auto
+    }
+    then have "cone S" unfolding cone_def by auto
   }
- hence "cone S" unfolding cone_def by auto
-} ultimately show ?thesis by blast
-qed
-
-lemma cone_hull_empty:
-"cone hull {} = {}"
-by (metis cone_empty cone_hull_eq)
-
-lemma cone_hull_empty_iff:
-shows "(S = {}) <-> (cone hull S = {})"
-by (metis bot_least cone_hull_empty hull_subset xtrans(5))
-
-lemma cone_hull_contains_0: 
-shows "(S ~= {}) <-> (0 : cone hull S)"
-using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S] by auto
+  ultimately show ?thesis by blast
+qed
+
+lemma cone_hull_empty: "cone hull {} = {}"
+  by (metis cone_empty cone_hull_eq)
+
+lemma cone_hull_empty_iff: "(S = {}) <-> (cone hull S = {})"
+  by (metis bot_least cone_hull_empty hull_subset xtrans(5))
+
+lemma cone_hull_contains_0: "(S ~= {}) <-> (0 : cone hull S)"
+  using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S]
+  by auto
 
 lemma mem_cone_hull:
   assumes "x : S" "c>=0"
   shows "c *\<^sub>R x : cone hull S"
-by (metis assms cone_cone_hull hull_inc mem_cone)
-
-lemma cone_hull_expl:
-shows "cone hull S = {c *\<^sub>R x | c x. c>=0 & x : S}" (is "?lhs = ?rhs")
-proof-
-{ fix x assume "x : ?rhs"
-  from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto
-  fix c assume c_def: "(c :: real)>=0"
-  hence "c *\<^sub>R x = (c*cx) *\<^sub>R xx" using x_def by (simp add: algebra_simps)
-  moreover have "(c*cx) >= 0" using c_def x_def using mult_nonneg_nonneg by auto
-  ultimately have "c *\<^sub>R x : ?rhs" using x_def by auto
-} hence "cone ?rhs" unfolding cone_def by auto
-  hence "?rhs : Collect cone" unfolding mem_Collect_eq by auto
-{ fix x assume "x : S" hence "1 *\<^sub>R x : ?rhs" apply auto apply(rule_tac x="1" in exI) by auto
-  hence "x : ?rhs" by auto
-} hence "S <= ?rhs" by auto
-hence "?lhs <= ?rhs" using `?rhs : Collect cone` hull_minimal[of S "?rhs" "cone"] by auto
-moreover
-{ fix x assume "x : ?rhs"
-  from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto
-  hence "xx : cone hull S" using hull_subset[of S] by auto
-  hence "x : ?lhs" using x_def cone_cone_hull[of S] cone_def[of "cone hull S"] by auto
-} ultimately show ?thesis by auto
+  by (metis assms cone_cone_hull hull_inc mem_cone)
+
+lemma cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c>=0 & x : S}" (is "?lhs = ?rhs")
+proof -
+  { fix x
+    assume "x : ?rhs"
+    then obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S"
+      by auto
+    fix c
+    assume c_def: "(c :: real) >= 0"
+    then have "c *\<^sub>R x = (c*cx) *\<^sub>R xx"
+      using x_def by (simp add: algebra_simps)
+    moreover
+    have "(c*cx) >= 0"
+      using c_def x_def using mult_nonneg_nonneg by auto
+    ultimately
+    have "c *\<^sub>R x : ?rhs" using x_def by auto
+  } then have "cone ?rhs" unfolding cone_def by auto
+  then have "?rhs : Collect cone" unfolding mem_Collect_eq by auto
+  { fix x
+    assume "x : S"
+    then have "1 *\<^sub>R x : ?rhs"
+      apply auto  
+      apply (rule_tac x="1" in exI)
+      apply auto
+      done
+    then have "x : ?rhs" by auto
+  } then have "S <= ?rhs" by auto
+  then have "?lhs <= ?rhs"
+    using `?rhs : Collect cone` hull_minimal[of S "?rhs" "cone"] by auto
+  moreover
+  { fix x
+    assume "x : ?rhs"
+    then obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto
+    then have "xx : cone hull S" using hull_subset[of S] by auto
+    then have "x : ?lhs"
+      using x_def cone_cone_hull[of S] cone_def[of "cone hull S"] by auto
+  }
+  ultimately show ?thesis by auto
 qed
 
 lemma cone_closure:
   fixes S :: "('a::real_normed_vector) set"
-  assumes "cone S" shows "cone (closure S)"
-proof-
-{ assume "S = {}" hence ?thesis by auto }
-moreover
-{ assume "S ~= {}" hence "0:S & (!c. c>0 --> op *\<^sub>R c ` S = S)" using cone_iff[of S] assms by auto
-  hence "0:(closure S) & (!c. c>0 --> op *\<^sub>R c ` (closure S) = (closure S))"
-     using closure_subset by (auto simp add: closure_scaleR)
-  hence ?thesis using cone_iff[of "closure S"] by auto
-}
-ultimately show ?thesis by blast
-qed
+  assumes "cone S"
+  shows "cone (closure S)"
+proof (cases "S = {}")
+  case True
+  then show ?thesis by auto
+next
+  case False
+  then have "0:S & (!c. c>0 --> op *\<^sub>R c ` S = S)"
+    using cone_iff[of S] assms by auto
+  then have "0:(closure S) & (!c. c>0 --> 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
+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})))"
+definition affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
+  where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> (affine hull (s - {x})))"
 
 lemma affine_dependent_explicit:
   "affine_dependent p \<longleftrightarrow>
     (\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and>
     (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)"
-  unfolding affine_dependent_def affine_hull_explicit mem_Collect_eq apply(rule)
-  apply(erule bexE,erule exE,erule exE) apply(erule conjE)+ defer apply(erule exE,erule exE) apply(erule conjE)+ apply(erule bexE)
-proof-
-  fix x s u assume as:"x \<in> p" "finite s" "s \<noteq> {}" "s \<subseteq> p - {x}" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
+  unfolding affine_dependent_def affine_hull_explicit mem_Collect_eq
+  apply rule
+  apply (erule bexE, erule exE, erule exE)
+  apply (erule conjE)+
+  defer
+  apply (erule exE, erule exE)
+  apply (erule conjE)+
+  apply (erule bexE)
+proof -
+  fix x s u
+  assume as: "x \<in> p" "finite s" "s \<noteq> {}" "s \<subseteq> p - {x}" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
   have "x\<notin>s" using as(1,4) by auto
   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 by auto 
+    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
+    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"
+  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
-  thus "\<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, rule_tac x="s - {v}" in exI, rule_tac x="\<lambda>x. - (1 / u v) * u x" in exI)
-    unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] unfolding setsum_right_distrib[THEN sym] and setsum_diff1[OF as(1)] using as 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, rule_tac x="s - {v}" in exI,
+      rule_tac x="\<lambda>x. - (1 / u v) * u x" in exI)
+    unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric]
+    unfolding setsum_right_distrib[THEN sym] and setsum_diff1[OF as(1)]
+    using as apply auto
+    done
 qed
 
 lemma affine_dependent_explicit_finite:
-  fixes s :: "'a::real_vector set" assumes "finite s"
+  fixes s :: "'a::real_vector set"
+  assumes "finite s"
   shows "affine_dependent s \<longleftrightarrow> (\<exists>u. setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)"
   (is "?lhs = ?rhs")
 proof
-  have *:"\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::'a))" by auto
+  have *: "\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::'a))"
+    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"
+  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"
     unfolding affine_dependent_explicit by auto
-  thus ?rhs apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
+  then show ?rhs
+    apply (rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
     apply auto unfolding * and setsum_restrict_set[OF assms, THEN sym]
-    unfolding Int_absorb1[OF `t\<subseteq>s`] by auto
+    unfolding Int_absorb1[OF `t\<subseteq>s`]
+    apply auto
+    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
-  thus ?lhs unfolding affine_dependent_explicit using assms by auto
-qed
+  then show ?lhs unfolding affine_dependent_explicit
+    using assms by auto
+qed
+
 
 subsection {* Connectedness of convex sets *}
 
 lemma connected_real_lemma:
   fixes f :: "real \<Rightarrow> 'a::metric_space"
   assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2"
-  and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y - x) < d \<longrightarrow> dist(f y) (f x) < e"
-  and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"
-  and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2"
-  and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)"
+    and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y - x) < d \<longrightarrow> dist(f y) (f x) < e"
+    and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"
+    and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2"
+    and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)"
   shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x")
-proof-
+proof -
   let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}"
   have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa)
   have Sub: "\<exists>y. isUb UNIV ?S y"