# HG changeset patch
# User huffman
# Date 1313024536 25200
# Node ID 8e27e0177518022490bf5011fcf0d7a48cf905f1
# Parent  0697c01ff3ea0edc2a503705ed7a8a47b6231dc7
avoid warnings about duplicate rules

diff -r 0697c01ff3ea -r 8e27e0177518 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Wed Aug 10 17:02:03 2011 -0700
+++ b/src/HOL/Library/Cardinality.thy	Wed Aug 10 18:02:16 2011 -0700
@@ -62,7 +62,7 @@
   by (simp only: card_Pow finite numeral_2_eq_2)
 
 lemma card_nat [simp]: "CARD(nat) = 0"
-  by (simp add: infinite_UNIV_nat card_eq_0_iff)
+  by (simp add: card_eq_0_iff)
 
 
 subsection {* Classes with at least 1 and 2  *}
diff -r 0697c01ff3ea -r 8e27e0177518 src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Wed Aug 10 17:02:03 2011 -0700
+++ b/src/HOL/Library/Convex.thy	Wed Aug 10 18:02:16 2011 -0700
@@ -49,7 +49,7 @@
 
 lemma convex_halfspace_le: "convex {x. inner a x \<le> b}"
   unfolding convex_def
-  by (auto simp: inner_add inner_scaleR intro!: convex_bound_le)
+  by (auto simp: inner_add intro!: convex_bound_le)
 
 lemma convex_halfspace_ge: "convex {x. inner a x \<ge> b}"
 proof -
@@ -209,7 +209,7 @@
   shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1
                       \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)"
   unfolding convex_explicit
-proof (safe elim!: conjE)
+proof (safe)
   fix t u assume sum: "\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s"
     and as: "finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
   have *:"s \<inter> t = t" using as(2) by auto
@@ -480,9 +480,9 @@
   also have "\<dots> = a * (f x - f y) + f y" by (simp add: field_simps)
   finally have "f t - f y \<le> a * (f x - f y)" by simp
   with t show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
-    by (simp add: times_divide_eq le_divide_eq divide_le_eq field_simps a_def)
+    by (simp add: le_divide_eq divide_le_eq field_simps a_def)
   with t show "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
-    by (simp add: times_divide_eq le_divide_eq divide_le_eq field_simps)
+    by (simp add: le_divide_eq divide_le_eq field_simps)
 qed
 
 lemma pos_convex_function:
diff -r 0697c01ff3ea -r 8e27e0177518 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Aug 10 17:02:03 2011 -0700
+++ b/src/HOL/Library/Extended_Real.thy	Wed Aug 10 18:02:16 2011 -0700
@@ -608,7 +608,7 @@
   shows "a * c < b * c"
   using assms
   by (cases rule: ereal3_cases[of a b c])
-     (auto simp: zero_le_mult_iff ereal_less_PInfty)
+     (auto simp: zero_le_mult_iff)
 
 lemma ereal_mult_strict_left_mono:
   "\<lbrakk> a < b ; 0 < c ; c < (\<infinity>::ereal)\<rbrakk> \<Longrightarrow> c * a < c * b"
@@ -619,7 +619,7 @@
   using assms
   apply (cases "c = 0") apply simp
   by (cases rule: ereal3_cases[of a b c])
-     (auto simp: zero_le_mult_iff ereal_less_PInfty)
+     (auto simp: zero_le_mult_iff)
 
 lemma ereal_mult_left_mono:
   fixes a b c :: ereal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> c * a \<le> c * b"
@@ -710,7 +710,7 @@
   fixes x y :: ereal
   assumes "ALL z. x <= ereal z --> y <= ereal z"
   shows "y <= x"
-by (metis assms ereal_bot ereal_cases ereal_infty_less_eq ereal_less_eq linorder_le_cases)
+by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)
 
 lemma ereal_le_ereal:
   fixes x y :: ereal
@@ -2037,7 +2037,7 @@
   with `x \<noteq> 0` have "open (S - {0})" "x \<in> S - {0}" by auto
   from tendsto[THEN topological_tendstoD, OF this]
   show "eventually (\<lambda>x. f x \<in> S) net"
-    by (rule eventually_rev_mp) (auto simp: ereal_real real_of_ereal_0)
+    by (rule eventually_rev_mp) (auto simp: ereal_real)
 qed
 
 lemma tendsto_ereal_realI:
diff -r 0697c01ff3ea -r 8e27e0177518 src/HOL/Library/Set_Algebras.thy
--- a/src/HOL/Library/Set_Algebras.thy	Wed Aug 10 17:02:03 2011 -0700
+++ b/src/HOL/Library/Set_Algebras.thy	Wed Aug 10 18:02:16 2011 -0700
@@ -153,7 +153,7 @@
 
 theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
     a +o (C \<oplus> D)"
-  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
+  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
    apply (rule_tac x = "aa + ba" in exI)
    apply (auto simp add: add_ac)
   done
@@ -211,7 +211,7 @@
   by (auto simp add: elt_set_plus_def)
 
 lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
-  apply (auto intro!: subsetI simp add: set_plus_def)
+  apply (auto simp add: set_plus_def)
   apply (rule_tac x = 0 in bexI)
    apply (rule_tac x = x in bexI)
     apply (auto simp add: add_ac)
@@ -264,7 +264,7 @@
 
 theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
     a *o (C \<otimes> D)"
-  apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
+  apply (auto simp add: elt_set_times_def set_times_def
     mult_ac)
    apply (rule_tac x = "aa * ba" in exI)
    apply (auto simp add: mult_ac)
@@ -336,7 +336,7 @@
 
 lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
     a *o D \<oplus> C \<otimes> D"
-  apply (auto intro!: subsetI simp add:
+  apply (auto simp add:
     elt_set_plus_def elt_set_times_def set_times_def
     set_plus_def ring_distribs)
   apply auto
diff -r 0697c01ff3ea -r 8e27e0177518 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 10 17:02:03 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 10 18:02:16 2011 -0700
@@ -198,9 +198,6 @@
   from this show ?thesis by auto
 qed
 
-lemma basis_0[simp]:"(basis i::'a::euclidean_space) = 0 \<longleftrightarrow> i\<ge>DIM('a)"
-  using norm_basis[of i, where 'a='a] unfolding norm_eq_zero[where 'a='a,THEN sym] by auto
-
 lemma basis_to_basis_subspace_isomorphism:
   assumes s: "subspace (S:: ('n::euclidean_space) set)"
   and t: "subspace (T :: ('m::euclidean_space) set)"
@@ -2142,7 +2139,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: open_ball centre_in_ball)
+  apply (simp add: centre_in_ball)
   done
 
 lemma rel_interior_ball: 
diff -r 0697c01ff3ea -r 8e27e0177518 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Aug 10 17:02:03 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Aug 10 18:02:16 2011 -0700
@@ -420,7 +420,7 @@
       using ereal_open_cont_interval2[of S f0] real lim by auto
     then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
       unfolding Liminf_Sup Limsup_Inf less_Sup_iff Inf_less_iff
-      by (auto intro!: eventually_conj simp add: greaterThanLessThan_iff)
+      by (auto intro!: eventually_conj)
     with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
       by (rule_tac eventually_mono) auto
   qed
@@ -1036,7 +1036,7 @@
   proof (rule ccontr)
     assume "\<not> ?thesis" then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" by auto
     from bchoice[OF this] guess r ..
-    with * show False by (auto simp: setsum_ereal)
+    with * show False by auto
   qed
   ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" by auto
 next
diff -r 0697c01ff3ea -r 8e27e0177518 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 10 17:02:03 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 10 18:02:16 2011 -0700
@@ -42,7 +42,7 @@
 *}
 
 lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
-  by (auto intro: ext)
+  by auto
 
 lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
   by (simp add: vec_nth_inject [symmetric] fun_eq_iff)
diff -r 0697c01ff3ea -r 8e27e0177518 src/HOL/Multivariate_Analysis/L2_Norm.thy
--- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Wed Aug 10 17:02:03 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Wed Aug 10 18:02:16 2011 -0700
@@ -109,9 +109,8 @@
 lemma sqrt_sum_squares_le_sum:
   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y"
   apply (rule power2_le_imp_le)
-  apply (simp add: power2_sum)
-  apply (simp add: mult_nonneg_nonneg)
-  apply (simp add: add_nonneg_nonneg)
+  apply (simp add: power2_sum mult_nonneg_nonneg)
+  apply simp
   done
 
 lemma setL2_le_setsum [rule_format]:
@@ -128,9 +127,8 @@
 
 lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
   apply (rule power2_le_imp_le)
-  apply (simp add: power2_sum)
-  apply (simp add: mult_nonneg_nonneg)
-  apply (simp add: add_nonneg_nonneg)
+  apply (simp add: power2_sum mult_nonneg_nonneg)
+  apply simp
   done
 
 lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
@@ -164,7 +162,7 @@
   apply (rule order_trans)
   apply (rule power_mono)
   apply (erule add_left_mono)
-  apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg)
+  apply (simp add: mult_nonneg_nonneg setsum_nonneg)
   apply (simp add: power2_sum)
   apply (simp add: power_mult_distrib)
   apply (simp add: right_distrib left_distrib)
diff -r 0697c01ff3ea -r 8e27e0177518 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 10 17:02:03 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 10 18:02:16 2011 -0700
@@ -641,9 +641,9 @@
   assumes x: "0 \<le> x" and y: "0 \<le> y"
   shows "sqrt (x + y) \<le> sqrt x + sqrt y"
 apply (rule power2_le_imp_le)
-apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y)
+apply (simp add: real_sum_squared_expand x y)
 apply (simp add: mult_nonneg_nonneg x y)
-apply (simp add: add_nonneg_nonneg x y)
+apply (simp add: x y)
 done
 
 subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}
@@ -2319,7 +2319,7 @@
   shows "x = 0"
   using fB ifB fi xsB fx
 proof(induct arbitrary: x rule: finite_induct[OF fB])
-  case 1 thus ?case by (auto simp add:  span_empty)
+  case 1 thus ?case by auto
 next
   case (2 a b x)
   have fb: "finite b" using "2.prems" by simp
@@ -2372,7 +2372,7 @@
            \<and> (\<forall>x\<in> B. g x = f x)"
 using ib fi
 proof(induct rule: finite_induct[OF fi])
-  case 1 thus ?case by (auto simp add: span_empty)
+  case 1 thus ?case by auto
 next
   case (2 a b)
   from "2.prems" "2.hyps" have ibf: "independent b" "finite b"