--- 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)
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
--- 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: 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)
--- 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"