# HG changeset patch
# User huffman
# Date 1313097845 25200
# Node ID e81d676d598ec7247107a101a9ad0bca2b4e829a
# Parent  d12d89a66742b578db817d276c8b3ee3de33e159
avoid duplicate rule warnings

diff -r d12d89a66742 -r e81d676d598e src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 11 13:05:56 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 11 14:24:05 2011 -0700
@@ -1635,11 +1635,8 @@
 abbreviation dest_vec1:: "'a ^1 \<Rightarrow> 'a"
   where "dest_vec1 x \<equiv> (x$1)"
 
-lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
-  by (simp_all add:  vec_eq_iff)
-
-lemma vec1_component[simp]: "(vec1 x)$1 = x"
-  by (simp_all add:  vec_eq_iff)
+lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x"
+  by (simp add: vec_eq_iff)
 
 lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
   by (metis vec1_dest_vec1(1))
@@ -1647,9 +1644,6 @@
 lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))"
   by (metis vec1_dest_vec1(1))
 
-lemma vec1_eq[simp]:  "vec1 x = vec1 y \<longleftrightarrow> x = y"
-  by (metis vec1_dest_vec1(2))
-
 lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y"
   by (metis vec1_dest_vec1(1))
 
@@ -1741,12 +1735,12 @@
   by (simp add: vec_def norm_real)
 
 lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
-  by (simp only: dist_real vec1_component)
+  by (simp only: dist_real vec_component)
 lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
   by (metis vec1_dest_vec1(1) norm_vec1)
 
 lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
-   vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def real_norm_def
+   vec_inj[where 'b=1] vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def real_norm_def
 
 lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
   unfolding bounded_linear_def additive_def bounded_linear_axioms_def 
diff -r d12d89a66742 -r e81d676d598e src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Aug 11 13:05:56 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Aug 11 14:24:05 2011 -0700
@@ -1146,9 +1146,6 @@
   shows "suminf f = (\<Sum>N<n. f N)"
   using sums_finite[OF assms, THEN sums_unique] by simp
 
-lemma suminf_ereal_0[simp]: "(\<Sum>i. 0) = (0::'a::{comm_monoid_add,t2_space})"
-  using suminf_finite[of 0 "\<lambda>x. 0"] by simp
-
 lemma suminf_upper:
   fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n"
   shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
diff -r d12d89a66742 -r e81d676d598e src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 11 13:05:56 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 11 14:24:05 2011 -0700
@@ -23,8 +23,6 @@
   by(subst(asm) real_arch_inv)
 subsection {* Sundries *}
 
-(*declare basis_component[simp]*)
-
 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
 lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
 lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
@@ -142,7 +140,7 @@
       let ?z = "x - (e/2) *\<^sub>R basis k" assume as:"x$$k = a$$k" have "ball ?z (e / 2) \<inter> i = {}" apply(rule ccontr) unfolding ex_in_conv[THEN sym] proof(erule exE)
         fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
         hence "\<bar>(?z - y) $$ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto
-        hence "y$$k < a$$k" using e[THEN conjunct1] k by(auto simp add:field_simps basis_component as)
+        hence "y$$k < a$$k" using e[THEN conjunct1] k by(auto simp add:field_simps as)
         hence "y \<notin> i" unfolding ab mem_interval not_all apply(rule_tac x=k in exI) using k by auto thus False using yi by auto qed
       moreover have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof
         fix y assume as:"y\<in> ball ?z (e/2)" have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y - (e / 2) *\<^sub>R basis k)"
@@ -417,10 +415,6 @@
   fix k assume k:"k \<in> p1 \<union> p2"  show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
   show "k \<noteq> {}" using k d1(3) d2(3) by auto show "\<exists>a b. k = {a..b}" using k d1(4) d2(4) by auto qed
 
-(* move *)
-lemma Eucl_nth_inverse[simp]: fixes x::"'a::euclidean_space" shows "(\<chi>\<chi> i. x $$ i) = x"
-  apply(subst euclidean_eq) by auto
-
 lemma partial_division_extend_1:
   assumes "{c..d} \<subseteq> {a..b::'a::ordered_euclidean_space}" "{c..d} \<noteq> {}"
   obtains p where "p division_of {a..b}" "{c..d} \<in> p"
@@ -737,7 +731,7 @@
   "(s tagged_division_of i) \<equiv>
         (s tagged_partial_division_of i) \<and> (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
 
-lemma tagged_division_of_finite[dest]: "s tagged_division_of i \<Longrightarrow> finite s"
+lemma tagged_division_of_finite: "s tagged_division_of i \<Longrightarrow> finite s"
   unfolding tagged_division_of_def tagged_partial_division_of_def by auto
 
 lemma tagged_division_of:
diff -r d12d89a66742 -r e81d676d598e src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 11 13:05:56 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 11 14:24:05 2011 -0700
@@ -479,7 +479,7 @@
   { fix e :: real assume "0 < e"
     def y \<equiv> "x + scaleR (e/2) (sgn (basis 0))"
     from `0 < e` have "y \<noteq> x"
-      unfolding y_def by (simp add: sgn_zero_iff basis_eq_0_iff DIM_positive)
+      unfolding y_def by (simp add: sgn_zero_iff DIM_positive)
     from `0 < e` have "dist y x < e"
       unfolding y_def by (simp add: dist_norm norm_sgn)
     from `y \<noteq> x` and `dist y x < e`
@@ -5646,7 +5646,7 @@
 
 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)
+  unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *)
 
 lemma closed_substandard:
  "closed {x::'a::euclidean_space. \<forall>i<DIM('a). P i --> x$$i = 0}" (is "closed ?A")
@@ -5674,7 +5674,7 @@
   let ?D = "{..<DIM('a)}"
   let ?B = "(basis::nat => 'a) ` d"
   let ?bas = "basis::nat \<Rightarrow> 'a"
-  have "?B \<subseteq> ?A" by(auto simp add:basis_component)
+  have "?B \<subseteq> ?A" by auto
   moreover
   { fix x::"'a" assume "x\<in>?A"
     hence "finite d" "x\<in>?A" using assms by(auto intro:finite_subset)
@@ -5690,7 +5690,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 basis_component) }
+          using *[THEN spec[where x=i]] by(auto simp add: euclidean_simps) }
       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)"]
@@ -6025,7 +6025,7 @@
   have lima:"((fst \<circ> (h \<circ> r)) ---> a) sequentially"
    and limb:"((snd \<circ> (h \<circ> r)) ---> b) sequentially"
     using lr
-    unfolding o_def a_def b_def by (simp_all add: tendsto_intros)
+    unfolding o_def a_def b_def by (rule tendsto_intros)+
 
   { fix n::nat
     have *:"\<And>fx fy (x::'a) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (dist (fx - fy) (a - b) < dist a b - dist x y)" unfolding dist_norm by norm