# 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 \ 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 \ b}" proof - @@ -209,7 +209,7 @@ shows "convex s \ (\u. (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\x. u x *\<^sub>R x) s \ s)" unfolding convex_explicit -proof (safe elim!: conjE) +proof (safe) fix t u assume sum: "\u. (\x\s. 0 \ u x) \ setsum u s = 1 \ (\x\s. u x *\<^sub>R x) \ s" and as: "finite t" "t \ s" "\x\t. 0 \ u x" "setsum u t = (1::real)" have *:"s \ t = t" using as(2) by auto @@ -480,9 +480,9 @@ also have "\ = a * (f x - f y) + f y" by (simp add: field_simps) finally have "f t - f y \ a * (f x - f y)" by simp with t show "(f x - f t) / (x - t) \ (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) \ (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: "\ a < b ; 0 < c ; c < (\::ereal)\ \ 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 "\a \ b; 0 \ c\ \ c * a \ 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 \ 0` have "open (S - {0})" "x \ S - {0}" by auto from tendsto[THEN topological_tendstoD, OF this] show "eventually (\x. f x \ 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 \ ((a::'a::comm_monoid_add) +o D) = a +o (C \ 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 \ 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 \ ((a::'a::comm_monoid_mult) *o D) = a *o (C \ 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) \ D <= a *o D \ C \ 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 \ i\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 (\x. f x \ {a<.. S` show "eventually (%x. f x : S) net" by (rule_tac eventually_mono) auto qed @@ -1036,7 +1036,7 @@ proof (rule ccontr) assume "\ ?thesis" then have "\i\A. \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 \ (\i\A. \f i\ = \)" 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: "(\x. f x = g x) \ (f = g)" - by (auto intro: ext) + by auto lemma vec_eq_iff: "(x = y) \ (\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: "\0 \ x; 0 \ y\ \ sqrt (x\ + y\) \ 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\ + y\) \ \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_abs: "setL2 f A \ (\i\A. \f i\)" @@ -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 \ x" and y: "0 \ y" shows "sqrt (x + y) \ 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 @@ \ (\x\ 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"