avoid warnings about duplicate rules
authorhuffman
Wed Aug 10 18:02:16 2011 -0700 (2011-08-10)
changeset 441428e27e0177518
parent 44141 0697c01ff3ea
child 44143 d282b3c5df7c
avoid warnings about duplicate rules
src/HOL/Library/Cardinality.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Set_Algebras.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Multivariate_Analysis/L2_Norm.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
     1.1 --- a/src/HOL/Library/Cardinality.thy	Wed Aug 10 17:02:03 2011 -0700
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Wed Aug 10 18:02:16 2011 -0700
     1.3 @@ -62,7 +62,7 @@
     1.4    by (simp only: card_Pow finite numeral_2_eq_2)
     1.5  
     1.6  lemma card_nat [simp]: "CARD(nat) = 0"
     1.7 -  by (simp add: infinite_UNIV_nat card_eq_0_iff)
     1.8 +  by (simp add: card_eq_0_iff)
     1.9  
    1.10  
    1.11  subsection {* Classes with at least 1 and 2  *}
     2.1 --- a/src/HOL/Library/Convex.thy	Wed Aug 10 17:02:03 2011 -0700
     2.2 +++ b/src/HOL/Library/Convex.thy	Wed Aug 10 18:02:16 2011 -0700
     2.3 @@ -49,7 +49,7 @@
     2.4  
     2.5  lemma convex_halfspace_le: "convex {x. inner a x \<le> b}"
     2.6    unfolding convex_def
     2.7 -  by (auto simp: inner_add inner_scaleR intro!: convex_bound_le)
     2.8 +  by (auto simp: inner_add intro!: convex_bound_le)
     2.9  
    2.10  lemma convex_halfspace_ge: "convex {x. inner a x \<ge> b}"
    2.11  proof -
    2.12 @@ -209,7 +209,7 @@
    2.13    shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1
    2.14                        \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)"
    2.15    unfolding convex_explicit
    2.16 -proof (safe elim!: conjE)
    2.17 +proof (safe)
    2.18    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"
    2.19      and as: "finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
    2.20    have *:"s \<inter> t = t" using as(2) by auto
    2.21 @@ -480,9 +480,9 @@
    2.22    also have "\<dots> = a * (f x - f y) + f y" by (simp add: field_simps)
    2.23    finally have "f t - f y \<le> a * (f x - f y)" by simp
    2.24    with t show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
    2.25 -    by (simp add: times_divide_eq le_divide_eq divide_le_eq field_simps a_def)
    2.26 +    by (simp add: le_divide_eq divide_le_eq field_simps a_def)
    2.27    with t show "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
    2.28 -    by (simp add: times_divide_eq le_divide_eq divide_le_eq field_simps)
    2.29 +    by (simp add: le_divide_eq divide_le_eq field_simps)
    2.30  qed
    2.31  
    2.32  lemma pos_convex_function:
     3.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Aug 10 17:02:03 2011 -0700
     3.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Aug 10 18:02:16 2011 -0700
     3.3 @@ -608,7 +608,7 @@
     3.4    shows "a * c < b * c"
     3.5    using assms
     3.6    by (cases rule: ereal3_cases[of a b c])
     3.7 -     (auto simp: zero_le_mult_iff ereal_less_PInfty)
     3.8 +     (auto simp: zero_le_mult_iff)
     3.9  
    3.10  lemma ereal_mult_strict_left_mono:
    3.11    "\<lbrakk> a < b ; 0 < c ; c < (\<infinity>::ereal)\<rbrakk> \<Longrightarrow> c * a < c * b"
    3.12 @@ -619,7 +619,7 @@
    3.13    using assms
    3.14    apply (cases "c = 0") apply simp
    3.15    by (cases rule: ereal3_cases[of a b c])
    3.16 -     (auto simp: zero_le_mult_iff ereal_less_PInfty)
    3.17 +     (auto simp: zero_le_mult_iff)
    3.18  
    3.19  lemma ereal_mult_left_mono:
    3.20    fixes a b c :: ereal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> c * a \<le> c * b"
    3.21 @@ -710,7 +710,7 @@
    3.22    fixes x y :: ereal
    3.23    assumes "ALL z. x <= ereal z --> y <= ereal z"
    3.24    shows "y <= x"
    3.25 -by (metis assms ereal_bot ereal_cases ereal_infty_less_eq ereal_less_eq linorder_le_cases)
    3.26 +by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)
    3.27  
    3.28  lemma ereal_le_ereal:
    3.29    fixes x y :: ereal
    3.30 @@ -2037,7 +2037,7 @@
    3.31    with `x \<noteq> 0` have "open (S - {0})" "x \<in> S - {0}" by auto
    3.32    from tendsto[THEN topological_tendstoD, OF this]
    3.33    show "eventually (\<lambda>x. f x \<in> S) net"
    3.34 -    by (rule eventually_rev_mp) (auto simp: ereal_real real_of_ereal_0)
    3.35 +    by (rule eventually_rev_mp) (auto simp: ereal_real)
    3.36  qed
    3.37  
    3.38  lemma tendsto_ereal_realI:
     4.1 --- a/src/HOL/Library/Set_Algebras.thy	Wed Aug 10 17:02:03 2011 -0700
     4.2 +++ b/src/HOL/Library/Set_Algebras.thy	Wed Aug 10 18:02:16 2011 -0700
     4.3 @@ -153,7 +153,7 @@
     4.4  
     4.5  theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
     4.6      a +o (C \<oplus> D)"
     4.7 -  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
     4.8 +  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
     4.9     apply (rule_tac x = "aa + ba" in exI)
    4.10     apply (auto simp add: add_ac)
    4.11    done
    4.12 @@ -211,7 +211,7 @@
    4.13    by (auto simp add: elt_set_plus_def)
    4.14  
    4.15  lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
    4.16 -  apply (auto intro!: subsetI simp add: set_plus_def)
    4.17 +  apply (auto simp add: set_plus_def)
    4.18    apply (rule_tac x = 0 in bexI)
    4.19     apply (rule_tac x = x in bexI)
    4.20      apply (auto simp add: add_ac)
    4.21 @@ -264,7 +264,7 @@
    4.22  
    4.23  theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
    4.24      a *o (C \<otimes> D)"
    4.25 -  apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
    4.26 +  apply (auto simp add: elt_set_times_def set_times_def
    4.27      mult_ac)
    4.28     apply (rule_tac x = "aa * ba" in exI)
    4.29     apply (auto simp add: mult_ac)
    4.30 @@ -336,7 +336,7 @@
    4.31  
    4.32  lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
    4.33      a *o D \<oplus> C \<otimes> D"
    4.34 -  apply (auto intro!: subsetI simp add:
    4.35 +  apply (auto simp add:
    4.36      elt_set_plus_def elt_set_times_def set_times_def
    4.37      set_plus_def ring_distribs)
    4.38    apply auto
     5.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 10 17:02:03 2011 -0700
     5.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 10 18:02:16 2011 -0700
     5.3 @@ -198,9 +198,6 @@
     5.4    from this show ?thesis by auto
     5.5  qed
     5.6  
     5.7 -lemma basis_0[simp]:"(basis i::'a::euclidean_space) = 0 \<longleftrightarrow> i\<ge>DIM('a)"
     5.8 -  using norm_basis[of i, where 'a='a] unfolding norm_eq_zero[where 'a='a,THEN sym] by auto
     5.9 -
    5.10  lemma basis_to_basis_subspace_isomorphism:
    5.11    assumes s: "subspace (S:: ('n::euclidean_space) set)"
    5.12    and t: "subspace (T :: ('m::euclidean_space) set)"
    5.13 @@ -2142,7 +2139,7 @@
    5.14    apply (simp add: rel_interior, safe)
    5.15    apply (force simp add: open_contains_ball)
    5.16    apply (rule_tac x="ball x e" in exI)
    5.17 -  apply (simp add: open_ball centre_in_ball)
    5.18 +  apply (simp add: centre_in_ball)
    5.19    done
    5.20  
    5.21  lemma rel_interior_ball: 
     6.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Aug 10 17:02:03 2011 -0700
     6.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Aug 10 18:02:16 2011 -0700
     6.3 @@ -420,7 +420,7 @@
     6.4        using ereal_open_cont_interval2[of S f0] real lim by auto
     6.5      then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
     6.6        unfolding Liminf_Sup Limsup_Inf less_Sup_iff Inf_less_iff
     6.7 -      by (auto intro!: eventually_conj simp add: greaterThanLessThan_iff)
     6.8 +      by (auto intro!: eventually_conj)
     6.9      with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
    6.10        by (rule_tac eventually_mono) auto
    6.11    qed
    6.12 @@ -1036,7 +1036,7 @@
    6.13    proof (rule ccontr)
    6.14      assume "\<not> ?thesis" then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" by auto
    6.15      from bchoice[OF this] guess r ..
    6.16 -    with * show False by (auto simp: setsum_ereal)
    6.17 +    with * show False by auto
    6.18    qed
    6.19    ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" by auto
    6.20  next
     7.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 10 17:02:03 2011 -0700
     7.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 10 18:02:16 2011 -0700
     7.3 @@ -42,7 +42,7 @@
     7.4  *}
     7.5  
     7.6  lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
     7.7 -  by (auto intro: ext)
     7.8 +  by auto
     7.9  
    7.10  lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
    7.11    by (simp add: vec_nth_inject [symmetric] fun_eq_iff)
     8.1 --- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Wed Aug 10 17:02:03 2011 -0700
     8.2 +++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Wed Aug 10 18:02:16 2011 -0700
     8.3 @@ -109,9 +109,8 @@
     8.4  lemma sqrt_sum_squares_le_sum:
     8.5    "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y"
     8.6    apply (rule power2_le_imp_le)
     8.7 -  apply (simp add: power2_sum)
     8.8 -  apply (simp add: mult_nonneg_nonneg)
     8.9 -  apply (simp add: add_nonneg_nonneg)
    8.10 +  apply (simp add: power2_sum mult_nonneg_nonneg)
    8.11 +  apply simp
    8.12    done
    8.13  
    8.14  lemma setL2_le_setsum [rule_format]:
    8.15 @@ -128,9 +127,8 @@
    8.16  
    8.17  lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
    8.18    apply (rule power2_le_imp_le)
    8.19 -  apply (simp add: power2_sum)
    8.20 -  apply (simp add: mult_nonneg_nonneg)
    8.21 -  apply (simp add: add_nonneg_nonneg)
    8.22 +  apply (simp add: power2_sum mult_nonneg_nonneg)
    8.23 +  apply simp
    8.24    done
    8.25  
    8.26  lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
    8.27 @@ -164,7 +162,7 @@
    8.28    apply (rule order_trans)
    8.29    apply (rule power_mono)
    8.30    apply (erule add_left_mono)
    8.31 -  apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg)
    8.32 +  apply (simp add: mult_nonneg_nonneg setsum_nonneg)
    8.33    apply (simp add: power2_sum)
    8.34    apply (simp add: power_mult_distrib)
    8.35    apply (simp add: right_distrib left_distrib)
     9.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 10 17:02:03 2011 -0700
     9.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 10 18:02:16 2011 -0700
     9.3 @@ -641,9 +641,9 @@
     9.4    assumes x: "0 \<le> x" and y: "0 \<le> y"
     9.5    shows "sqrt (x + y) \<le> sqrt x + sqrt y"
     9.6  apply (rule power2_le_imp_le)
     9.7 -apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y)
     9.8 +apply (simp add: real_sum_squared_expand x y)
     9.9  apply (simp add: mult_nonneg_nonneg x y)
    9.10 -apply (simp add: add_nonneg_nonneg x y)
    9.11 +apply (simp add: x y)
    9.12  done
    9.13  
    9.14  subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}
    9.15 @@ -2319,7 +2319,7 @@
    9.16    shows "x = 0"
    9.17    using fB ifB fi xsB fx
    9.18  proof(induct arbitrary: x rule: finite_induct[OF fB])
    9.19 -  case 1 thus ?case by (auto simp add:  span_empty)
    9.20 +  case 1 thus ?case by auto
    9.21  next
    9.22    case (2 a b x)
    9.23    have fb: "finite b" using "2.prems" by simp
    9.24 @@ -2372,7 +2372,7 @@
    9.25             \<and> (\<forall>x\<in> B. g x = f x)"
    9.26  using ib fi
    9.27  proof(induct rule: finite_induct[OF fi])
    9.28 -  case 1 thus ?case by (auto simp add: span_empty)
    9.29 +  case 1 thus ?case by auto
    9.30  next
    9.31    case (2 a b)
    9.32    from "2.prems" "2.hyps" have ibf: "independent b" "finite b"