# HG changeset patch
# User huffman
# Date 1314133862 25200
# Node ID d366fa5551eff1511156991fac2ffb0774d3b4ee
# Parent  aae9c9a0735e8161355a746d9e8ce282488a4e68
declare euclidean_simps [simp] at the point they are proved;
avoid duplicate rule warnings;

diff -r aae9c9a0735e -r d366fa5551ef src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Aug 23 14:11:02 2011 -0700
@@ -533,7 +533,7 @@
   case False hence "t = {}" using `finite t` by auto
   show ?thesis
   proof (cases "s = {}")
-    have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" by (auto intro: ext)
+    have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" by auto
     case True thus ?thesis using `t = {}` by (auto simp: *)
   next
     case False thus ?thesis using `t = {}` by simp
diff -r aae9c9a0735e -r d366fa5551ef src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Aug 23 14:11:02 2011 -0700
@@ -831,7 +831,7 @@
     have IU: " (UNIV :: (real^'m) set) \<subseteq> span ?I" by blast
     from linear_eq[OF lf lg IU] fg x
     have "f x = g x" unfolding Ball_def mem_Collect_eq by metis}
-  then show ?thesis by (auto intro: ext)
+  then show ?thesis by auto
 qed
 
 lemma bilinear_eq_stdbasis_cart:
@@ -841,7 +841,7 @@
   shows "f = g"
 proof-
   from fg have th: "\<forall>x \<in> {cart_basis i| i. i\<in> (UNIV :: 'm set)}. \<forall>y\<in>  {cart_basis j |j. j \<in> (UNIV :: 'n set)}. f x y = g x y" by blast
-  from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by (blast intro: ext)
+  from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by blast
 qed
 
 lemma left_invertible_transpose:
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
diff -r aae9c9a0735e -r d366fa5551ef src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Aug 23 14:11:02 2011 -0700
@@ -598,7 +598,7 @@
     case True thus ?thesis
       apply(rule_tac x="(min (b$$i - a$$i)  e) / 2" in exI)
       using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2)
-      unfolding mem_interval euclidean_simps basis_component
+      unfolding mem_interval euclidean_simps
       using i by (auto simp add: field_simps)
   next note * = assms(2)[unfolded mem_interval,THEN spec[where x=i]]
     case False moreover have "a $$ i < x $$ i" using False * by auto
@@ -614,7 +614,7 @@
     ultimately show ?thesis
       apply(rule_tac x="- (min (x$$i - a$$i) e) / 2" in exI)
       using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2)
-      unfolding mem_interval euclidean_simps basis_component
+      unfolding mem_interval euclidean_simps
       using i by (auto simp add: field_simps)
   qed
 qed
@@ -655,7 +655,7 @@
 proof -
   have fA: "finite {..<DIM('a)}" by simp
   have "?rhs = (\<Sum>i<DIM('a). x$$i *\<^sub>R f (basis i))$$j"
-    by (simp add: euclidean_simps)
+    by simp
   then show ?thesis
     unfolding linear_setsum_mul[OF lf fA, symmetric]
     unfolding euclidean_representation[symmetric] ..
@@ -1550,7 +1550,7 @@
     apply(rule has_derivative_sequence[OF assms(1) _ assms(3), of "\<lambda>n x. f n x + (f 0 a - f n a)"])
     apply(rule,rule)
     apply(rule has_derivative_add_const, rule assms(2)[rule_format], assumption)  
-    apply(rule `a\<in>s`) by(auto intro!: tendsto_const)
+    apply(rule `a\<in>s`) by auto
 qed auto
 
 lemma has_antiderivative_limit:
diff -r aae9c9a0735e -r d366fa5551ef src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Aug 23 14:11:02 2011 -0700
@@ -515,7 +515,7 @@
   shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}"
 proof(induct k)
   case 0
-  have th: "{f. \<forall>i. f i = i} = {id}" by (auto intro: ext)
+  have th: "{f. \<forall>i. f i = i} = {id}" by auto
   show ?case by (auto simp add: th)
 next
   case (Suc k)
@@ -525,14 +525,14 @@
     apply (auto simp add: image_iff)
     apply (rule_tac x="x (Suc k)" in bexI)
     apply (rule_tac x = "\<lambda>i. if i = Suc k then i else x i" in exI)
-    apply (auto intro: ext)
+    apply auto
     done
   with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f]
   show ?case by metis
 qed
 
 
-lemma eq_id_iff[simp]: "(\<forall>x. f x = x) = (f = id)" by (auto intro: ext)
+lemma eq_id_iff[simp]: "(\<forall>x. f x = x) = (f = id)" by auto
 
 lemma det_linear_rows_setsum_lemma:
   assumes fS: "finite S" and fT: "finite T"
@@ -575,7 +575,7 @@
       blast intro: finite_cartesian_product fS finite,
       blast intro: finite_cartesian_product fS finite)
     using `z \<notin> T`
-    apply (auto intro: ext)
+    apply auto
     apply (rule cong[OF refl[of det]])
     by vector
 qed
@@ -739,7 +739,7 @@
       unfolding setsum_diff1'[OF fU iU] setsum_cmul
       apply -
       apply (rule vector_mul_lcancel_imp[OF ci])
-      apply (auto simp add: vector_smult_assoc vector_smult_rneg field_simps)
+      apply (auto simp add: field_simps)
       unfolding stupid ..
     have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}"
       unfolding thr0
@@ -775,7 +775,7 @@
   have kUk: "k \<notin> ?Uk" by simp
   have th00: "\<And>k s. x$k *s row k A + s = (x$k - 1) *s row k A + row k A + s"
     by (vector field_simps)
-  have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" by (auto intro: ext)
+  have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" by auto
   have "(\<chi> i. row i A) = A" by (vector row_def)
   then have thd1: "det (\<chi> i. row i A) = det A"  by simp
   have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A"
@@ -931,7 +931,7 @@
       unfolding dot_norm_neg dist_norm[symmetric]
       unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
   note fc = this
-  show ?thesis unfolding linear_def vector_eq[where 'a="real^'n"] smult_conv_scaleR by (simp add: inner_simps fc field_simps)
+  show ?thesis unfolding linear_def vector_eq[where 'a="real^'n"] smult_conv_scaleR by (simp add: inner_add fc field_simps)
 qed
 
 lemma isometry_linear:
@@ -973,7 +973,7 @@
     "x' = norm x *\<^sub>R x0'" "y' = norm y *\<^sub>R y0'"
     "norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1"
     "norm(x0' - y0') = norm(x0 - y0)"
-    hence *:"x0 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0' - y0 \<bullet> x0 " by(simp add: norm_eq norm_eq_1 inner_simps)
+    hence *:"x0 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0' - y0 \<bullet> x0 " by(simp add: norm_eq norm_eq_1 inner_add inner_diff)
     have "norm(x' - y') = norm(x - y)"
       apply (subst H(1))
       apply (subst H(2))
@@ -981,7 +981,7 @@
       apply (subst H(4))
       using H(5-9)
       apply (simp add: norm_eq norm_eq_1)
-      apply (simp add: inner_simps smult_conv_scaleR) unfolding *
+      apply (simp add: inner_diff smult_conv_scaleR) unfolding *
       by (simp add: field_simps) }
   note th0 = this
   let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)"
@@ -1015,7 +1015,7 @@
         "norm (f (inverse (norm x) *\<^sub>R x) - f (inverse (norm y) *\<^sub>R y)) =
         norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)"
         using z
-        by (auto simp add: vector_smult_assoc field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
+        by (auto simp add: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
       from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
         by (simp add: dist_norm)}
     ultimately have "dist (?g x) (?g y) = dist x y" by blast}
@@ -1049,7 +1049,7 @@
   by (simp add: eval_nat_numeral setprod_numseg mult_commute)
 
 lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
-  by (simp add: det_def sign_id UNIV_1)
+  by (simp add: det_def sign_id)
 
 lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1"
 proof-
diff -r aae9c9a0735e -r d366fa5551ef src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 23 14:11:02 2011 -0700
@@ -129,19 +129,19 @@
 lemma euclidean_component_zero [simp]: "0 $$ i = 0"
   unfolding euclidean_component_def by (rule inner_zero_right)
 
-lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"
+lemma euclidean_component_add [simp]: "(x + y) $$ i = x $$ i + y $$ i"
   unfolding euclidean_component_def by (rule inner_add_right)
 
-lemma euclidean_component_diff: "(x - y) $$ i = x $$ i - y $$ i"
+lemma euclidean_component_diff [simp]: "(x - y) $$ i = x $$ i - y $$ i"
   unfolding euclidean_component_def by (rule inner_diff_right)
 
-lemma euclidean_component_minus: "(- x) $$ i = - (x $$ i)"
+lemma euclidean_component_minus [simp]: "(- x) $$ i = - (x $$ i)"
   unfolding euclidean_component_def by (rule inner_minus_right)
 
-lemma euclidean_component_scaleR: "(scaleR a x) $$ i = a * (x $$ i)"
+lemma euclidean_component_scaleR [simp]: "(scaleR a x) $$ i = a * (x $$ i)"
   unfolding euclidean_component_def by (rule inner_scaleR_right)
 
-lemma euclidean_component_setsum: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
+lemma euclidean_component_setsum [simp]: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
   unfolding euclidean_component_def by (rule inner_setsum_right)
 
 lemma euclidean_eqI:
@@ -183,7 +183,6 @@
   fixes x :: "'a::euclidean_space"
   shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)"
   apply (rule euclidean_eqI)
-  apply (simp add: euclidean_component_setsum euclidean_component_scaleR)
   apply (simp add: if_distrib setsum_delta cong: if_cong)
   done
 
@@ -194,8 +193,7 @@
 
 lemma euclidean_lambda_beta [simp]:
   "((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)"
-  by (auto simp: euclidean_component_setsum euclidean_component_scaleR
-    Chi_def if_distrib setsum_cases intro!: setsum_cong)
+  by (auto simp: Chi_def if_distrib setsum_cases intro!: setsum_cong)
 
 lemma euclidean_lambda_beta':
   "j < DIM('a) \<Longrightarrow> ((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = f j"
diff -r aae9c9a0735e -r d366fa5551ef src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Tue Aug 23 14:11:02 2011 -0700
@@ -180,7 +180,7 @@
       "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
       "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
       "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
-      unfolding interval_bij_cart vec_lambda_beta vector_component_simps o_def split_conv
+      unfolding interval_bij_cart vector_component_simps o_def split_conv
       unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this
   from z(1) guess zf unfolding image_iff .. note zf=this
   from z(2) guess zg unfolding image_iff .. note zg=this
diff -r aae9c9a0735e -r d366fa5551ef src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Aug 23 14:11:02 2011 -0700
@@ -485,7 +485,7 @@
     show "k\<subseteq>{a..b}" apply(rule,unfold mem_interval,rule,rule) 
     proof fix i x assume i:"i<DIM('a)" assume "x \<in> k" moreover have "\<pi>' i < l \<or> \<pi>' i = l \<or> \<pi>' i > l" by auto
       ultimately show "a$$i \<le> x$$i" "x$$i \<le> b$$i" using abcd[of i] using l using i
-        by(auto elim:disjE elim!:allE[where x=i] simp add:eucl_le[where 'a='a])
+        by(auto elim!:allE[where x=i] simp add:eucl_le[where 'a='a]) (* FIXME: SLOW *)
     qed have "\<And>l. ?p1 l \<noteq> {}" "\<And>l. ?p2 l \<noteq> {}" unfolding interval_eq_empty not_ex apply(rule_tac[!] allI)
     proof- case goal1 thus ?case using abcd[of x] by auto
     next   case goal2 thus ?case using abcd[of x] by auto
@@ -967,7 +967,7 @@
 subsection {* The set we're concerned with must be closed. *}
 
 lemma division_of_closed: "s division_of i \<Longrightarrow> closed (i::('n::ordered_euclidean_space) set)"
-  unfolding division_of_def by(fastsimp intro!: closed_Union closed_interval)
+  unfolding division_of_def by fastsimp
 
 subsection {* General bisection principle for intervals; might be useful elsewhere. *}
 
@@ -2544,7 +2544,7 @@
       apply(subst interval_doublesplit[OF k]) apply(rule content_pos_le) apply(rule indicator_pos_le)
     proof- have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) * ?i x) \<le> (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}))"
         apply(rule setsum_mono) unfolding split_paired_all split_conv 
-        apply(rule mult_right_le_one_le) apply(drule p'(4)) by(auto simp add:interval_doublesplit[OF k] intro!:content_pos_le)
+        apply(rule mult_right_le_one_le) apply(drule p'(4)) by(auto simp add:interval_doublesplit[OF k])
       also have "... < e" apply(subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]])
       proof- case goal1 have "content ({u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<le> content {u..v}"
           unfolding interval_doublesplit[OF k] apply(rule content_subset) unfolding interval_doublesplit[THEN sym,OF k] by auto
@@ -4627,7 +4627,7 @@
       case goal1 show ?case using int .
     next case goal2 thus ?case apply-apply(cases "x\<in>s") using assms(3) by auto
     next case goal3 thus ?case apply-apply(cases "x\<in>s")
-        using assms(4) by (auto intro: tendsto_const)
+        using assms(4) by auto
     next case goal4 note * = integral_nonneg
       have "\<And>k. norm (integral {a..b} (\<lambda>x. if x \<in> s then f k x else 0)) \<le> norm (integral s (f k))"
         unfolding real_norm_def apply(subst abs_of_nonneg) apply(rule *[OF int])
@@ -4678,7 +4678,7 @@
   next case goal2 thus ?case apply(rule integrable_sub) using assms(1) by auto
   next case goal3 thus ?case using *[of x "Suc k" "Suc (Suc k)"] by auto
   next case goal4 thus ?case apply-apply(rule tendsto_diff) 
-      using seq_offset[OF assms(3)[rule_format],of x 1] by (auto intro: tendsto_const)
+      using seq_offset[OF assms(3)[rule_format],of x 1] by auto
   next case goal5 thus ?case using assms(4) unfolding bounded_iff
       apply safe apply(rule_tac x="a + norm (integral s (\<lambda>x. f 0 x))" in exI)
       apply safe apply(erule_tac x="integral s (\<lambda>x. f (Suc k) x)" in ballE) unfolding sub
diff -r aae9c9a0735e -r d366fa5551ef src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Aug 23 14:11:02 2011 -0700
@@ -1659,10 +1659,9 @@
     have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+
     have Ppe:"setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp \<le> e"
       using component_le_norm[of "setsum (\<lambda>x. f x) ?Pp" i]  fPs[OF PpP]
-      unfolding euclidean_component_setsum by(auto intro: abs_le_D1)
+      by(auto intro: abs_le_D1)
     have Pne: "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn \<le> e"
       using component_le_norm[of "setsum (\<lambda>x. - f x) ?Pn" i]  fPs[OF PnP]
-      unfolding euclidean_component_setsum euclidean_component_minus
       by(auto simp add: setsum_negf intro: abs_le_D1)
     have "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn"
       apply (subst thp)
@@ -2825,7 +2824,7 @@
     unfolding infnorm_def
     unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
     unfolding infnorm_set_image ball_simps
-    apply(subst (1) euclidean_eq) unfolding euclidean_component_zero
+    apply(subst (1) euclidean_eq)
     by auto
   then show ?thesis using infnorm_pos_le[of x] by simp
 qed
@@ -2836,7 +2835,7 @@
 lemma infnorm_neg: "infnorm (- x) = infnorm x"
   unfolding infnorm_def
   apply (rule cong[of "Sup" "Sup"])
-  apply blast by(auto simp add: euclidean_component_minus)
+  apply blast by auto
 
 lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"
 proof-
diff -r aae9c9a0735e -r d366fa5551ef src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 23 14:11:02 2011 -0700
@@ -14,7 +14,7 @@
 
 lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
   unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
-  apply(auto simp add:power2_eq_square) unfolding euclidean_component_diff ..
+  by(auto simp add:power2_eq_square)
 
 lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
   apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
@@ -5601,26 +5601,17 @@
 
 lemma subspace_substandard:
   "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
-  unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *)
+  unfolding subspace_def by auto
 
 lemma closed_substandard:
  "closed {x::'a::euclidean_space. \<forall>i<DIM('a). P i --> x$$i = 0}" (is "closed ?A")
 proof-
   let ?D = "{i. P i} \<inter> {..<DIM('a)}"
-  let ?Bs = "{{x::'a. inner (basis i) x = 0}| i. i \<in> ?D}"
-  { fix x
-    { assume "x\<in>?A"
-      hence x:"\<forall>i\<in>?D. x $$ i = 0" by auto
-      hence "x\<in> \<Inter> ?Bs" by(auto simp add: x euclidean_component_def) }
-    moreover
-    { assume x:"x\<in>\<Inter>?Bs"
-      { fix i assume i:"i \<in> ?D"
-        then obtain B where BB:"B \<in> ?Bs" and B:"B = {x::'a. inner (basis i) x = 0}" by auto
-        hence "x $$ i = 0" unfolding B using x unfolding euclidean_component_def by auto  }
-      hence "x\<in>?A" by auto }
-    ultimately have "x\<in>?A \<longleftrightarrow> x\<in> \<Inter>?Bs" .. }
-  hence "?A = \<Inter> ?Bs" by auto
-  thus ?thesis by(auto simp add: closed_Inter closed_hyperplane)
+  have "closed (\<Inter>i\<in>?D. {x::'a. x$$i = 0})"
+    by (simp add: closed_INT closed_Collect_eq)
+  also have "(\<Inter>i\<in>?D. {x::'a. x$$i = 0}) = ?A"
+    by auto
+  finally show "closed ?A" .
 qed
 
 lemma dim_substandard: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
@@ -5645,7 +5636,7 @@
       have y:"x = y + (x$$k) *\<^sub>R basis k" unfolding y_def by auto
       { fix i assume i':"i \<notin> F"
         hence "y $$ i = 0" unfolding y_def 
-          using *[THEN spec[where x=i]] by(auto simp add: euclidean_simps) }
+          using *[THEN spec[where x=i]] by auto }
       hence "y \<in> span (basis ` F)" using insert(3) by auto
       hence "y \<in> span (basis ` (insert k F))"
         using span_mono[of "?bas ` F" "?bas ` (insert k F)"]
@@ -5763,25 +5754,25 @@
   case False
   { fix y assume "a \<le> y" "y \<le> b" "m > 0"
     hence "m *\<^sub>R a + c \<le> m *\<^sub>R y + c"  "m *\<^sub>R y + c \<le> m *\<^sub>R b + c"
-      unfolding eucl_le[where 'a='a] by(auto simp add: euclidean_simps)
+      unfolding eucl_le[where 'a='a] by auto
   } moreover
   { fix y assume "a \<le> y" "y \<le> b" "m < 0"
     hence "m *\<^sub>R b + c \<le> m *\<^sub>R y + c"  "m *\<^sub>R y + c \<le> m *\<^sub>R a + c"
-      unfolding eucl_le[where 'a='a] by(auto simp add: mult_left_mono_neg euclidean_simps)
+      unfolding eucl_le[where 'a='a] by(auto simp add: mult_left_mono_neg)
   } moreover
   { fix y assume "m > 0"  "m *\<^sub>R a + c \<le> y"  "y \<le> m *\<^sub>R b + c"
     hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
       unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
       apply(auto simp add: pth_3[symmetric] 
         intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"]) 
-      by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff euclidean_simps)
+      by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
   } moreover
   { fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
     hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
       unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
       apply(auto simp add: pth_3[symmetric]
         intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
-      by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff euclidean_simps)
+      by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
   }
   ultimately show ?thesis using False by auto
 qed