author huffman Wed, 10 Aug 2011 18:02:16 -0700 changeset 44142 8e27e0177518 parent 44141 0697c01ff3ea child 44143 d282b3c5df7c
avoid warnings about duplicate rules
--- 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  *}
--- 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:
--- 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:
--- 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)
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)
@@ -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
--- 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:
--- 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
--- 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)
--- 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: 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: 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 (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)
--- 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: 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"