diff -r aae9c9a0735e -r d366fa5551ef src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Aug 23 14:11:02 2011 -0700
@@ -96,11 +96,7 @@
   unfolding subspace_def by auto 
 
 lemma span_eq[simp]: "(span s = s) <-> subspace s"
-proof-
-  { fix f assume "Ball f subspace"
-    hence "subspace (Inter f)" using subspace_Inter[of f] unfolding Ball_def by auto  }
-  thus ?thesis using hull_eq[of subspace s] span_def by auto
-qed
+  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])
@@ -291,8 +287,6 @@
   shows "scaleR 2 x = x + x"
 unfolding one_add_one_is_two [symmetric] scaleR_left_distrib by simp
 
-declare euclidean_simps[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
 
@@ -973,7 +967,7 @@
 lemma convex_box: fixes a::"'a::euclidean_space"
   assumes "\<And>i. i<DIM('a) \<Longrightarrow> convex {x. P i x}"
   shows "convex {x. \<forall>i<DIM('a). P i (x$$i)}"
-  using assms unfolding convex_def by(auto simp add:euclidean_simps)
+  using assms unfolding convex_def by auto
 
 lemma convex_positive_orthant: "convex {x::'a::euclidean_space. (\<forall>i<DIM('a). 0 \<le> x$$i)}"
   by (rule convex_box) (simp add: atLeast_def[symmetric] convex_real_interval)
@@ -1641,7 +1635,7 @@
 hence "V <= affine hull T" using B_def assms translation_inverse_subset[of a V "span B"] by auto
 moreover have "T<=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 Int_commute Int_lower2 assms hull_hull hull_mono) 
+    by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono)
 moreover have "S<=T" using T_def B_def translation_inverse_subset[of a "S-{a}" B] by auto
 moreover have "~(affine_dependent T)" 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
@@ -1675,7 +1669,7 @@
 
 lemma affine_hull_nonempty: "(S ~= {}) <-> affine hull S ~= {}"
 proof-
-fix S have "(S = {}) ==> affine hull S = {}"using affine_hull_empty by auto 
+have "(S = {}) ==> affine hull S = {}"using affine_hull_empty by auto 
 moreover have "affine hull S = {} ==> S = {}" unfolding hull_def by auto
 ultimately show "(S ~= {}) <-> affine hull S ~= {}" by blast
 qed
@@ -2076,7 +2070,7 @@
   apply (simp add: rel_interior, safe)
   apply (force simp add: open_contains_ball)
   apply (rule_tac x="ball x e" in exI)
-  apply (simp add: centre_in_ball)
+  apply simp
   done
 
 lemma rel_interior_ball: 
@@ -2087,7 +2081,7 @@
   apply (simp add: rel_interior, safe) 
   apply (force simp add: open_contains_cball)
   apply (rule_tac x="ball x e" in exI)
-  apply (simp add: open_ball centre_in_ball subset_trans [OF ball_subset_cball])
+  apply (simp add: subset_trans [OF ball_subset_cball])
   apply auto
   done
 
@@ -3370,7 +3364,7 @@
       hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis 0" in ballE) defer 
         apply(erule_tac x="basis 0" in ballE)
         unfolding Ball_def mem_cball dist_norm using DIM_positive[where 'a='a]
-        by(auto simp add:norm_basis[unfolded One_nat_def])
+        by auto
       case True show ?thesis unfolding True continuous_at Lim_at apply(rule,rule) apply(rule_tac x="e / B" in exI)
         apply(rule) apply(rule divide_pos_pos) prefer 3 apply(rule,rule,erule conjE)
         unfolding norm_zero scaleR_zero_left dist_norm diff_0_right norm_scaleR abs_norm_cancel proof-
@@ -3508,7 +3502,7 @@
     hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: field_simps)
     hence "u * a + v * b \<le> b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) }
   ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)])
-    using as(3-) DIM_positive[where 'a='a] by(auto simp add:euclidean_simps) qed
+    using as(3-) DIM_positive[where 'a='a] by auto qed
 
 lemma is_interval_connected:
   fixes s :: "('a::euclidean_space) set"
@@ -3570,7 +3564,7 @@
   shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
   apply(subst neg_equal_iff_equal[THEN sym])
   using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"] using assms using continuous_on_neg
-  by (auto simp add:euclidean_simps)
+  by auto
 
 lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
   shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
@@ -3624,18 +3618,18 @@
           by auto
       next let ?y = "\<lambda>j. if x$$j = 0 then 0 else (x$$j - x$$i) / (1 - x$$i)"
         case False hence *:"x = x$$i *\<^sub>R (\<chi>\<chi> j. if x$$j = 0 then 0 else 1) + (1 - x$$i) *\<^sub>R (\<chi>\<chi> j. ?y j)"
-          apply(subst euclidean_eq) by(auto simp add: field_simps euclidean_simps)
+          apply(subst euclidean_eq) by(auto simp add: field_simps)
         { fix j assume j:"j<DIM('a)"
           have "x$$j \<noteq> 0 \<Longrightarrow> 0 \<le> (x $$ j - x $$ i) / (1 - x $$ i)" "(x $$ j - x $$ i) / (1 - x $$ i) \<le> 1"
             apply(rule_tac divide_nonneg_pos) using i(1)[of j] using False i01
             using Suc(2)[unfolded mem_interval, rule_format, of j] using j
-            by(auto simp add:field_simps euclidean_simps)
+            by(auto simp add:field_simps)
           hence "0 \<le> ?y j \<and> ?y j \<le> 1" by auto }
         moreover have "i\<in>{j. j<DIM('a) \<and> x$$j \<noteq> 0} - {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0}"
           using i01 using i'(3) by auto
         hence "{j. j<DIM('a) \<and> x$$j \<noteq> 0} \<noteq> {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0}" using i'(3) by blast
         hence **:"{j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0} \<subset> {j. j<DIM('a) \<and> x$$j \<noteq> 0}" apply - apply rule 
-          by( auto simp add:euclidean_simps)
+          by auto
         have "card {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0} \<le> n"
           using less_le_trans[OF psubset_card_mono[OF _ **] Suc(4)] by auto
         ultimately show ?thesis apply(subst *) apply(rule convex_convex_hull[unfolded convex_def, rule_format])
@@ -3671,14 +3665,14 @@
     fix y assume as:"y\<in>{x - ?d .. x + ?d}"
     { fix i assume i:"i<DIM('a)" have "x $$ i \<le> d + y $$ i" "y $$ i \<le> d + x $$ i"
         using as[unfolded mem_interval, THEN spec[where x=i]] i
-        by(auto simp add:euclidean_simps)
+        by auto
       hence "1 \<ge> inverse d * (x $$ i - y $$ i)" "1 \<ge> inverse d * (y $$ i - x $$ i)"
         apply(rule_tac[!] mult_left_le_imp_le[OF _ assms]) unfolding mult_assoc[THEN sym]
         using assms by(auto simp add: field_simps)
       hence "inverse d * (x $$ i * 2) \<le> 2 + inverse d * (y $$ i * 2)"
             "inverse d * (y $$ i * 2) \<le> 2 + inverse d * (x $$ i * 2)" by(auto simp add:field_simps) }
     hence "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> {0..\<chi>\<chi> i.1}" unfolding mem_interval using assms
-      by(auto simp add: euclidean_simps field_simps)
+      by(auto simp add: field_simps)
     thus "\<exists>z\<in>{0..\<chi>\<chi> i.1}. y = x - ?d + (2 * d) *\<^sub>R z" apply- apply(rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI) 
       using assms by auto
   next
@@ -3688,7 +3682,7 @@
       apply rule apply(rule mult_nonneg_nonneg) prefer 3 apply(rule mult_right_le_one_le)
       using assms by auto
     thus "y \<in> {x - ?d..x + ?d}" unfolding as(2) mem_interval apply- apply rule using as(1)[unfolded mem_interval]
-      apply(erule_tac x=i in allE) using assms by(auto simp add: euclidean_simps) qed
+      apply(erule_tac x=i in allE) using assms by auto qed
   obtain s where "finite s" "{0::'a..\<chi>\<chi> i.1} = convex hull s" using unit_cube_convex_hull by auto
   thus ?thesis apply(rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` s"]) unfolding * and convex_hull_affinity by auto qed
 
@@ -3774,7 +3768,7 @@
   have "0 < d" unfolding d_def using `e>0` dimge1 by(rule_tac divide_pos_pos, auto) 
   let ?d = "(\<chi>\<chi> i. d)::'a"
   obtain c where c:"finite c" "{x - ?d..x + ?d} = convex hull c" using cube_convex_hull[OF `d>0`, of x] by auto
-  have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by(auto simp add:euclidean_simps)
+  have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by auto
   hence "c\<noteq>{}" using c by auto
   def k \<equiv> "Max (f ` c)"
   have "convex_on {x - ?d..x + ?d} f" apply(rule convex_on_subset[OF assms(2)])
@@ -3783,7 +3777,7 @@
     have e:"e = setsum (\<lambda>i. d) {..<DIM('a)}" unfolding setsum_constant d_def using dimge1
       unfolding real_eq_of_nat by auto
     show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
-      using z[unfolded mem_interval] apply(erule_tac x=i in allE) by(auto simp add:euclidean_simps) qed
+      using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed
   hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption
     unfolding k_def apply(rule, rule Max_ge) using c(1) by auto
   have "d \<le> e" unfolding d_def apply(rule mult_imp_div_pos_le) using `e>0` dimge1 unfolding mult_le_cancel_left1 by auto
@@ -3792,9 +3786,9 @@
   hence "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof
     fix y assume y:"y\<in>cball x d"
     { fix i assume "i<DIM('a)" hence "x $$ i - d \<le> y $$ i"  "y $$ i \<le> x $$ i + d" 
-        using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by(auto simp add:euclidean_simps)  }
+        using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by auto  }
     thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm 
-      by(auto simp add:euclidean_simps) qed
+      by auto qed
   hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous)
     apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball)
     apply force
@@ -3929,10 +3923,10 @@
       proof(rule,rule) fix i assume i:"i<DIM('a)"
           have "((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $$ i =
             ((norm (a - b) - norm (a - x)) * (a $$ i) + norm (a - x) * (b $$ i)) / norm (a - b)"
-            using Fal by(auto simp add: field_simps euclidean_simps)
+            using Fal by(auto simp add: field_simps)
           also have "\<dots> = x$$i" apply(rule divide_eq_imp[OF Fal])
             unfolding as[unfolded dist_norm] using as[unfolded dist_triangle_eq] apply-
-            apply(subst (asm) euclidean_eq) using i apply(erule_tac x=i in allE) by(auto simp add:field_simps euclidean_simps)
+            apply(subst (asm) euclidean_eq) using i apply(erule_tac x=i in allE) by(auto simp add:field_simps)
           finally show "x $$ i = ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $$ i" 
             by auto
         qed(insert Fal2, auto) qed qed
@@ -3943,7 +3937,7 @@
 proof- have *:"\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" by auto
   show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *)
     unfolding euclidean_eq[where 'a='a]
-    by(auto simp add:field_simps euclidean_simps) qed
+    by(auto simp add:field_simps) qed
 
 lemma between_mem_convex_hull:
   "between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
@@ -3962,7 +3956,7 @@
     have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
     have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
       unfolding dist_norm unfolding norm_scaleR[THEN sym] apply(rule arg_cong[where f=norm]) using `e>0`
-      by(auto simp add: euclidean_simps euclidean_eq[where 'a='a] field_simps) 
+      by(auto simp add: euclidean_eq[where 'a='a] field_simps) 
     also have "\<dots> = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
     also have "\<dots> < d" using as[unfolded dist_norm] and `e>0`
       by(auto simp add:pos_divide_less_eq[OF `e>0`] mult_commute)
@@ -4042,7 +4036,7 @@
       apply(rule_tac x="\<lambda>y. inner y x" in exI) apply(rule,rule) unfolding mem_Collect_eq apply(erule exE)
       using as(1) apply(erule_tac x=i in allE) unfolding sumbas apply safe unfolding not_less basis_zero
       unfolding substdbasis_expansion_unique[OF assms] euclidean_component_def[THEN sym]
-      using as(2,3) by(auto simp add:dot_basis not_less  basis_zero) 
+      using as(2,3) by(auto simp add:dot_basis not_less)
   qed qed
 
 lemma std_simplex:
@@ -4058,11 +4052,11 @@
   fix x::"'a" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x<DIM('a). 0 \<le> xa $$ x) \<and> setsum (op $$ xa) {..<DIM('a)} \<le> 1"
   show "(\<forall>xa<DIM('a). 0 < x $$ xa) \<and> setsum (op $$ x) {..<DIM('a)} < 1" apply(safe) proof-
     fix i assume i:"i<DIM('a)" thus "0 < x $$ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`
-      unfolding dist_norm  by(auto simp add: inner_simps euclidean_component_def dot_basis elim!:allE[where x=i])
+      unfolding dist_norm by (auto elim!:allE[where x=i])
   next have **:"dist x (x + (e / 2) *\<^sub>R basis 0) < e" using  `e>0`
       unfolding dist_norm by(auto intro!: mult_strict_left_mono)
     have "\<And>i. i<DIM('a) \<Longrightarrow> (x + (e / 2) *\<^sub>R basis 0) $$ i = x$$i + (if i = 0 then e/2 else 0)"
-      unfolding euclidean_component_def by(auto simp add:inner_simps dot_basis)
+      by auto
     hence *:"setsum (op $$ (x + (e / 2) *\<^sub>R basis 0)) {..<DIM('a)} = setsum (\<lambda>i. x$$i + (if 0 = i then e/2 else 0)) {..<DIM('a)}"
       apply(rule_tac setsum_cong) by auto
     have "setsum (op $$ x) {..<DIM('a)} < setsum (op $$ (x + (e / 2) *\<^sub>R basis 0)) {..<DIM('a)}" unfolding * setsum_addf
@@ -4143,7 +4137,7 @@
       setsum (\<lambda>i. x$$i + (if a = i then e/2 else 0)) d" by(rule_tac setsum_cong, auto)
     have h1: "(ALL i<DIM('a). i ~: d --> (x + (e / 2) *\<^sub>R basis a) $$ i = 0)"
       using as[THEN spec[where x="x + (e / 2) *\<^sub>R basis a"]] `a:d` using x0
-      by(auto simp add: norm_basis elim:allE[where x=a]) 
+      by(auto elim:allE[where x=a])
     have "setsum (op $$ x) d < setsum (op $$ (x + (e / 2) *\<^sub>R basis a)) d" unfolding * setsum_addf
       using `0<e` `a:d` using `finite d` by(auto simp add: setsum_delta')
     also have "\<dots> \<le> 1" using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R basis a"] by auto
@@ -4776,7 +4770,7 @@
     } from this obtain mS where mS_def: "!S : I. (mS(S) > (1 :: real) & 
          (!e. (e>1 & e<=mS(S)) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S))" by metis
     obtain e where e_def: "e=Min (mS ` I)" by auto 
-    have "e : (mS ` I)" using e_def assms `I ~= {}` by (simp add: Min_in) 
+    have "e : (mS ` I)" using e_def assms `I ~= {}` by simp
     hence "e>(1 :: real)" using mS_def by auto
     moreover have "!S : I. e<=mS(S)" using e_def assms by auto
     ultimately have "EX e>1. (1 - e) *\<^sub>R x + e *\<^sub>R z : Inter I" using mS_def by auto