--- a/src/HOL/Algebra/Divisibility.thy Tue Aug 05 16:21:27 2014 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Tue Aug 05 16:58:19 2014 +0200
@@ -74,7 +74,7 @@
have c: "inv (a \<otimes> b) \<otimes> a \<in> carrier G" by simp
have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)" by (simp add: m_assoc)
- also have "\<dots> = \<one>" by (simp add: Units_l_inv)
+ also have "\<dots> = \<one>" by simp
finally have li: "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = \<one>" .
have "\<one> = inv a \<otimes> a" by (simp add: Units_l_inv[symmetric])
@@ -83,7 +83,7 @@
by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv)
also have "\<dots> = ((inv a \<otimes> a) \<otimes> b) \<otimes> inv (a \<otimes> b) \<otimes> a"
by (simp add: m_assoc del: Units_l_inv)
- also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by (simp add: Units_l_inv)
+ also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp
also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> a)" by (simp add: m_assoc)
finally have ri: "b \<otimes> (inv (a \<otimes> b) \<otimes> a) = \<one> " by simp
@@ -327,7 +327,7 @@
unfolding a
apply (intro associatedI)
apply (rule dividesI[of "inv u"], simp)
- apply (simp add: m_assoc Units_closed Units_r_inv)
+ apply (simp add: m_assoc Units_closed)
apply fast
done
@@ -1764,7 +1764,7 @@
note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit]
have "a = a \<otimes> \<one>" by simp
- also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: Units_r_inv uunit)
+ also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: uunit)
also have "\<dots> = a' \<otimes> inv u" by (simp add: m_assoc[symmetric] a'[symmetric])
finally
have a: "a = a' \<otimes> inv u" .
@@ -2646,7 +2646,7 @@
hence yb: "fmset G ys \<le> fmset G bs" by (rule divides_fmsubset) fact+
from ya yb csmset
- have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def multiset_inter_count)
+ have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def)
thus "y divides c" by (rule fmsubset_divides) fact+
qed
@@ -3208,7 +3208,7 @@
and nyx: "\<not> y \<sim> x"
by - (fast elim: properfactorE2)+
hence "\<exists>z. z \<in> carrier G \<and> x = y \<otimes> z"
- by (fast elim: dividesE)
+ by fast
from this obtain z
where zcarr: "z \<in> carrier G"
@@ -3327,7 +3327,7 @@
and afs': "wfactors G as' a"
hence ahdvda: "ah divides a"
by (intro wfactors_dividesI[of "ah#as" "a"], simp+)
- hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by (fast elim: dividesE)
+ hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by fast
from this obtain a'
where a'carr: "a' \<in> carrier G"
and a: "a = ah \<otimes> a'"
@@ -3360,7 +3360,7 @@
have asicarr[simp]: "as'!i \<in> carrier G" by (unfold set_conv_nth, force)
note carr = carr asicarr
- from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by (fast elim: dividesE)
+ from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by fast
from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto
with carr irrasi[simplified asi]
@@ -3454,7 +3454,7 @@
next
show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"
apply (simp add: list_all2_append)
- apply (simp add: asiah[symmetric] ahcarr asicarr)
+ apply (simp add: asiah[symmetric])
done
qed
@@ -3463,12 +3463,12 @@
also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
(take i as' @ as' ! i # drop (Suc i) as')"
apply (intro essentially_equalI)
- apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
+ apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
take i as' @ as' ! i # drop (Suc i) as'")
- apply simp
+ apply simp
apply (rule perm_append_Cons)
apply simp
- done
+ done
finally
have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" by simp
then show "essentially_equal G (ah # as) as'" by (subst as', assumption)
@@ -3617,7 +3617,7 @@
also from ccarr acarr cunit
have "\<dots> = a \<otimes> (c \<otimes> inv c)" by (fast intro: m_assoc)
also from ccarr cunit
- have "\<dots> = a \<otimes> \<one>" by (simp add: Units_r_inv)
+ have "\<dots> = a \<otimes> \<one>" by simp
also from acarr
have "\<dots> = a" by simp
finally have "a = b \<otimes> inv c" by simp
@@ -3706,7 +3706,7 @@
shows "(divisor_chain_condition_monoid G \<and> gcd_condition_monoid G) = factorial_monoid G"
apply rule
proof clarify
- assume dcc: "divisor_chain_condition_monoid G"
+ assume dcc: "divisor_chain_condition_monoid G"
and gc: "gcd_condition_monoid G"
interpret divisor_chain_condition_monoid "G" by (rule dcc)
interpret gcd_condition_monoid "G" by (rule gc)
--- a/src/HOL/Algebra/Exponent.thy Tue Aug 05 16:21:27 2014 +0200
+++ b/src/HOL/Algebra/Exponent.thy Tue Aug 05 16:58:19 2014 +0200
@@ -249,7 +249,7 @@
apply (simp (no_asm))
(*induction step*)
apply (subgoal_tac "(Suc (j+k) choose Suc k) > 0")
- prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
+ prefer 2 apply (simp, clarify)
apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) =
exponent p (Suc k)")
txt{*First, use the assumed equation. We simplify the LHS to
@@ -260,7 +260,7 @@
@{text Suc_times_binomial_eq} ...*}
apply (simp del: bad_Sucs add: Suc_times_binomial_eq [symmetric])
txt{*...then @{text exponent_mult_add} and the quantified premise.*}
-apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add)
+apply (simp del: bad_Sucs add: exponent_mult_add)
done
(*The lemma above, with two changes of variables*)
--- a/src/HOL/Algebra/UnivPoly.thy Tue Aug 05 16:21:27 2014 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Tue Aug 05 16:58:19 2014 +0200
@@ -528,7 +528,7 @@
case 0 with R show ?thesis by simp
next
case Suc with R show ?thesis
- using R.finsum_Suc2 by (simp del: R.finsum_Suc add: R.r_null Pi_def)
+ using R.finsum_Suc2 by (simp del: R.finsum_Suc add: Pi_def)
qed
qed (simp_all add: R)
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Aug 05 16:21:27 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Aug 05 16:58:19 2014 +0200
@@ -137,17 +137,17 @@
end
*} "lift trivial vector statements to real arith statements"
-lemma vec_0[simp]: "vec 0 = 0" by (vector zero_vec_def)
-lemma vec_1[simp]: "vec 1 = 1" by (vector one_vec_def)
+lemma vec_0[simp]: "vec 0 = 0" by vector
+lemma vec_1[simp]: "vec 1 = 1" by vector
lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector
lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
-lemma vec_add: "vec(x + y) = vec x + vec y" by (vector vec_def)
-lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def)
-lemma vec_cmul: "vec(c * x) = c *s vec x " by (vector vec_def)
-lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)
+lemma vec_add: "vec(x + y) = vec x + vec y" by vector
+lemma vec_sub: "vec(x - y) = vec x - vec y" by vector
+lemma vec_cmul: "vec(c * x) = c *s vec x " by vector
+lemma vec_neg: "vec(- x) = - vec x " by vector
lemma vec_setsum:
assumes "finite S"
@@ -164,7 +164,7 @@
text{* Obvious "component-pushing". *}
lemma vec_component [simp]: "vec x $ i = x"
- by (vector vec_def)
+ by vector
lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
by vector
@@ -330,7 +330,7 @@
assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) * e"
using setsum_norm_allsubsets_bound[OF assms]
- by (simp add: DIM_cart Basis_real_def)
+ by simp
subsection {* Matrix operations *}
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Aug 05 16:21:27 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Aug 05 16:58:19 2014 +0200
@@ -1502,7 +1502,7 @@
by (intro convex_linear_vimage convex_translation convex_convex_hull,
simp add: linear_iff)
also have "?S = {y. (x, y) \<in> convex hull (s \<times> t)}"
- by (auto simp add: uminus_add_conv_diff image_def Bex_def)
+ by (auto simp add: image_def Bex_def)
finally show "convex {y. (x, y) \<in> convex hull (s \<times> t)}" .
next
show "convex {x. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)}"
@@ -1512,7 +1512,7 @@
by (intro convex_linear_vimage convex_translation convex_convex_hull,
simp add: linear_iff)
also have "?S = {x. (x, y) \<in> convex hull (s \<times> t)}"
- by (auto simp add: uminus_add_conv_diff image_def Bex_def)
+ by (auto simp add: image_def Bex_def)
finally show "convex {x. (x, y) \<in> convex hull (s \<times> t)}" .
qed
qed
@@ -5504,12 +5504,12 @@
using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` s",
OF convex_affinity compact_affinity]
using assms(1,2)
- by (auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib)
+ by (auto simp add: scaleR_right_diff_distrib)
then show ?thesis
apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]])
using `d>0` `e>0`
- apply (auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib)
+ apply (auto simp add: scaleR_right_diff_distrib)
done
qed
@@ -5808,7 +5808,7 @@
apply (rule_tac f="\<lambda>x. a + x" in arg_cong)
apply (rule setsum.cong [OF refl])
apply clarsimp
- apply (fast intro: set_plus_intro)
+ apply fast
done
lemma box_eq_set_setsum_Basis:
@@ -5895,7 +5895,7 @@
apply (rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
using as
apply (subst euclidean_eq_iff)
- apply (auto simp: inner_setsum_left_Basis)
+ apply auto
done
qed auto
@@ -6430,7 +6430,7 @@
apply (subst (asm) euclidean_eq_iff)
using i
apply (erule_tac x=i in ballE)
- apply (auto simp add:field_simps inner_simps)
+ apply (auto simp add: field_simps inner_simps)
done
finally show "x \<bullet> i =
((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) \<bullet> i"
@@ -8138,8 +8138,7 @@
and "convex S"
and "rel_open S"
shows "convex (f ` S) \<and> rel_open (f ` S)"
- by (metis assms convex_linear_image rel_interior_convex_linear_image
- linear_conv_bounded_linear rel_open_def)
+ by (metis assms convex_linear_image rel_interior_convex_linear_image rel_open_def)
lemma convex_rel_open_linear_preimage:
fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Aug 05 16:21:27 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Aug 05 16:58:19 2014 +0200
@@ -69,7 +69,7 @@
lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)"
unfolding has_derivative_def Lim
- by (auto simp add: netlimit_within inverse_eq_divide field_simps)
+ by (auto simp add: netlimit_within field_simps)
lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)"
@@ -1773,9 +1773,9 @@
apply (rule lem3[rule_format])+
done
obtain N where N: "\<forall>h. norm (f' N x h - g' x h) \<le> 1 * norm h"
- using assms(3) `x \<in> s` by (fast intro: zero_less_one order_refl)
+ using assms(3) `x \<in> s` by (fast intro: zero_less_one)
have "bounded_linear (f' N x)"
- using assms(2) `x \<in> s` by (fast dest: has_derivative_bounded_linear)
+ using assms(2) `x \<in> s` by fast
from bounded_linear.bounded [OF this]
obtain K where K: "\<forall>h. norm (f' N x h) \<le> norm h * K" ..
{
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Aug 05 16:21:27 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Aug 05 16:58:19 2014 +0200
@@ -1125,7 +1125,7 @@
note fin = this
have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
using f
- by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def)
+ by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
also have "\<dots> = ereal r"
using fin r by (auto simp: ereal_real)
finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
@@ -1252,7 +1252,8 @@
apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
apply (drule sym)
apply auto
- by (metis INF_absorb centre_in_ball)
+ apply (metis INF_absorb centre_in_ball)
+ done
lemma suminf_ereal_offset_le:
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Aug 05 16:21:27 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Aug 05 16:58:19 2014 +0200
@@ -343,7 +343,7 @@
using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
then have "y\<bullet>k < a\<bullet>k"
using e[THEN conjunct1] k
- by (auto simp add: field_simps abs_less_iff as inner_Basis inner_simps)
+ by (auto simp add: field_simps abs_less_iff as inner_simps)
then have "y \<notin> i"
unfolding ab mem_box by (auto intro!: bexI[OF _ k])
then show False using yi by auto
@@ -12092,7 +12092,7 @@
by (induct I) (auto intro!: bounded_linear_add bounded_linear_zero)
next
case False
- then show ?thesis by (simp add: bounded_linear_zero)
+ then show ?thesis by simp
qed
lemma absolutely_integrable_vector_abs:
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 05 16:21:27 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 05 16:58:19 2014 +0200
@@ -7307,27 +7307,27 @@
lemma real_affinity_le:
"0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c \<le> y \<longleftrightarrow> x \<le> inverse(m) * y + -(c / m))"
- by (simp add: field_simps inverse_eq_divide)
+ by (simp add: field_simps)
lemma real_le_affinity:
"0 < (m::'a::linordered_field) \<Longrightarrow> (y \<le> m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) \<le> x)"
- by (simp add: field_simps inverse_eq_divide)
+ by (simp add: field_simps)
lemma real_affinity_lt:
"0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c < y \<longleftrightarrow> x < inverse(m) * y + -(c / m))"
- by (simp add: field_simps inverse_eq_divide)
+ by (simp add: field_simps)
lemma real_lt_affinity:
"0 < (m::'a::linordered_field) \<Longrightarrow> (y < m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) < x)"
- by (simp add: field_simps inverse_eq_divide)
+ by (simp add: field_simps)
lemma real_affinity_eq:
"(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (m * x + c = y \<longleftrightarrow> x = inverse(m) * y + -(c / m))"
- by (simp add: field_simps inverse_eq_divide)
+ by (simp add: field_simps)
lemma real_eq_affinity:
"(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (y = m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
- by (simp add: field_simps inverse_eq_divide)
+ by (simp add: field_simps)
subsection {* Banach fixed point theorem (not really topological...) *}