declare euclidean_simps [simp] at the point they are proved;
avoid duplicate rule warnings;
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Aug 23 14:11:02 2011 -0700
@@ -533,7 +533,7 @@
case False hence "t = {}" using `finite t` by auto
show ?thesis
proof (cases "s = {}")
- have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" by (auto intro: ext)
+ have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" by auto
case True thus ?thesis using `t = {}` by (auto simp: *)
next
case False thus ?thesis using `t = {}` by simp
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Aug 23 14:11:02 2011 -0700
@@ -831,7 +831,7 @@
have IU: " (UNIV :: (real^'m) set) \<subseteq> span ?I" by blast
from linear_eq[OF lf lg IU] fg x
have "f x = g x" unfolding Ball_def mem_Collect_eq by metis}
- then show ?thesis by (auto intro: ext)
+ then show ?thesis by auto
qed
lemma bilinear_eq_stdbasis_cart:
@@ -841,7 +841,7 @@
shows "f = g"
proof-
from fg have th: "\<forall>x \<in> {cart_basis i| i. i\<in> (UNIV :: 'm set)}. \<forall>y\<in> {cart_basis j |j. j \<in> (UNIV :: 'n set)}. f x y = g x y" by blast
- from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by (blast intro: ext)
+ from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by blast
qed
lemma left_invertible_transpose:
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Aug 23 14:11:02 2011 -0700
@@ -96,11 +96,7 @@
unfolding subspace_def by auto
lemma span_eq[simp]: "(span s = s) <-> subspace s"
-proof-
- { fix f assume "Ball f subspace"
- hence "subspace (Inter f)" using subspace_Inter[of f] unfolding Ball_def by auto }
- thus ?thesis using hull_eq[of subspace s] span_def by auto
-qed
+ unfolding span_def by (rule hull_eq, rule subspace_Inter)
lemma basis_inj_on: "d \<subseteq> {..<DIM('n)} \<Longrightarrow> inj_on (basis :: nat => 'n::euclidean_space) d"
by(auto simp add: inj_on_def euclidean_eq[where 'a='n])
@@ -291,8 +287,6 @@
shows "scaleR 2 x = x + x"
unfolding one_add_one_is_two [symmetric] scaleR_left_distrib by simp
-declare euclidean_simps[simp]
-
lemma vector_choose_size: "0 <= c ==> \<exists>(x::'a::euclidean_space). norm x = c"
apply (rule exI[where x="c *\<^sub>R basis 0 ::'a"]) using DIM_positive[where 'a='a] by auto
@@ -973,7 +967,7 @@
lemma convex_box: fixes a::"'a::euclidean_space"
assumes "\<And>i. i<DIM('a) \<Longrightarrow> convex {x. P i x}"
shows "convex {x. \<forall>i<DIM('a). P i (x$$i)}"
- using assms unfolding convex_def by(auto simp add:euclidean_simps)
+ using assms unfolding convex_def by auto
lemma convex_positive_orthant: "convex {x::'a::euclidean_space. (\<forall>i<DIM('a). 0 \<le> x$$i)}"
by (rule convex_box) (simp add: atLeast_def[symmetric] convex_real_interval)
@@ -1641,7 +1635,7 @@
hence "V <= affine hull T" using B_def assms translation_inverse_subset[of a V "span B"] by auto
moreover have "T<=V" using T_def B_def a_def assms by auto
ultimately have "affine hull T = affine hull V"
- by (metis Int_absorb1 Int_absorb2 Int_commute Int_lower2 assms hull_hull hull_mono)
+ by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono)
moreover have "S<=T" using T_def B_def translation_inverse_subset[of a "S-{a}" B] by auto
moreover have "~(affine_dependent T)" using T_def affine_dependent_translation_eq[of "insert 0 B"] affine_dependent_imp_dependent2 B_def by auto
ultimately show ?thesis using `T<=V` by auto
@@ -1675,7 +1669,7 @@
lemma affine_hull_nonempty: "(S ~= {}) <-> affine hull S ~= {}"
proof-
-fix S have "(S = {}) ==> affine hull S = {}"using affine_hull_empty by auto
+have "(S = {}) ==> affine hull S = {}"using affine_hull_empty by auto
moreover have "affine hull S = {} ==> S = {}" unfolding hull_def by auto
ultimately show "(S ~= {}) <-> affine hull S ~= {}" by blast
qed
@@ -2076,7 +2070,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: centre_in_ball)
+ apply simp
done
lemma rel_interior_ball:
@@ -2087,7 +2081,7 @@
apply (simp add: rel_interior, safe)
apply (force simp add: open_contains_cball)
apply (rule_tac x="ball x e" in exI)
- apply (simp add: open_ball centre_in_ball subset_trans [OF ball_subset_cball])
+ apply (simp add: subset_trans [OF ball_subset_cball])
apply auto
done
@@ -3370,7 +3364,7 @@
hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis 0" in ballE) defer
apply(erule_tac x="basis 0" in ballE)
unfolding Ball_def mem_cball dist_norm using DIM_positive[where 'a='a]
- by(auto simp add:norm_basis[unfolded One_nat_def])
+ by auto
case True show ?thesis unfolding True continuous_at Lim_at apply(rule,rule) apply(rule_tac x="e / B" in exI)
apply(rule) apply(rule divide_pos_pos) prefer 3 apply(rule,rule,erule conjE)
unfolding norm_zero scaleR_zero_left dist_norm diff_0_right norm_scaleR abs_norm_cancel proof-
@@ -3508,7 +3502,7 @@
hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: field_simps)
hence "u * a + v * b \<le> b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) }
ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)])
- using as(3-) DIM_positive[where 'a='a] by(auto simp add:euclidean_simps) qed
+ using as(3-) DIM_positive[where 'a='a] by auto qed
lemma is_interval_connected:
fixes s :: "('a::euclidean_space) set"
@@ -3570,7 +3564,7 @@
shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
apply(subst neg_equal_iff_equal[THEN sym])
using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"] using assms using continuous_on_neg
- by (auto simp add:euclidean_simps)
+ by auto
lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
@@ -3624,18 +3618,18 @@
by auto
next let ?y = "\<lambda>j. if x$$j = 0 then 0 else (x$$j - x$$i) / (1 - x$$i)"
case False hence *:"x = x$$i *\<^sub>R (\<chi>\<chi> j. if x$$j = 0 then 0 else 1) + (1 - x$$i) *\<^sub>R (\<chi>\<chi> j. ?y j)"
- apply(subst euclidean_eq) by(auto simp add: field_simps euclidean_simps)
+ apply(subst euclidean_eq) by(auto simp add: field_simps)
{ fix j assume j:"j<DIM('a)"
have "x$$j \<noteq> 0 \<Longrightarrow> 0 \<le> (x $$ j - x $$ i) / (1 - x $$ i)" "(x $$ j - x $$ i) / (1 - x $$ i) \<le> 1"
apply(rule_tac divide_nonneg_pos) using i(1)[of j] using False i01
using Suc(2)[unfolded mem_interval, rule_format, of j] using j
- by(auto simp add:field_simps euclidean_simps)
+ by(auto simp add:field_simps)
hence "0 \<le> ?y j \<and> ?y j \<le> 1" by auto }
moreover have "i\<in>{j. j<DIM('a) \<and> x$$j \<noteq> 0} - {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0}"
using i01 using i'(3) by auto
hence "{j. j<DIM('a) \<and> x$$j \<noteq> 0} \<noteq> {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0}" using i'(3) by blast
hence **:"{j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0} \<subset> {j. j<DIM('a) \<and> x$$j \<noteq> 0}" apply - apply rule
- by( auto simp add:euclidean_simps)
+ by auto
have "card {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0} \<le> n"
using less_le_trans[OF psubset_card_mono[OF _ **] Suc(4)] by auto
ultimately show ?thesis apply(subst *) apply(rule convex_convex_hull[unfolded convex_def, rule_format])
@@ -3671,14 +3665,14 @@
fix y assume as:"y\<in>{x - ?d .. x + ?d}"
{ fix i assume i:"i<DIM('a)" have "x $$ i \<le> d + y $$ i" "y $$ i \<le> d + x $$ i"
using as[unfolded mem_interval, THEN spec[where x=i]] i
- by(auto simp add:euclidean_simps)
+ by auto
hence "1 \<ge> inverse d * (x $$ i - y $$ i)" "1 \<ge> inverse d * (y $$ i - x $$ i)"
apply(rule_tac[!] mult_left_le_imp_le[OF _ assms]) unfolding mult_assoc[THEN sym]
using assms by(auto simp add: field_simps)
hence "inverse d * (x $$ i * 2) \<le> 2 + inverse d * (y $$ i * 2)"
"inverse d * (y $$ i * 2) \<le> 2 + inverse d * (x $$ i * 2)" by(auto simp add:field_simps) }
hence "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> {0..\<chi>\<chi> i.1}" unfolding mem_interval using assms
- by(auto simp add: euclidean_simps field_simps)
+ by(auto simp add: field_simps)
thus "\<exists>z\<in>{0..\<chi>\<chi> i.1}. y = x - ?d + (2 * d) *\<^sub>R z" apply- apply(rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
using assms by auto
next
@@ -3688,7 +3682,7 @@
apply rule apply(rule mult_nonneg_nonneg) prefer 3 apply(rule mult_right_le_one_le)
using assms by auto
thus "y \<in> {x - ?d..x + ?d}" unfolding as(2) mem_interval apply- apply rule using as(1)[unfolded mem_interval]
- apply(erule_tac x=i in allE) using assms by(auto simp add: euclidean_simps) qed
+ apply(erule_tac x=i in allE) using assms by auto qed
obtain s where "finite s" "{0::'a..\<chi>\<chi> i.1} = convex hull s" using unit_cube_convex_hull by auto
thus ?thesis apply(rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` s"]) unfolding * and convex_hull_affinity by auto qed
@@ -3774,7 +3768,7 @@
have "0 < d" unfolding d_def using `e>0` dimge1 by(rule_tac divide_pos_pos, auto)
let ?d = "(\<chi>\<chi> i. d)::'a"
obtain c where c:"finite c" "{x - ?d..x + ?d} = convex hull c" using cube_convex_hull[OF `d>0`, of x] by auto
- have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by(auto simp add:euclidean_simps)
+ have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by auto
hence "c\<noteq>{}" using c by auto
def k \<equiv> "Max (f ` c)"
have "convex_on {x - ?d..x + ?d} f" apply(rule convex_on_subset[OF assms(2)])
@@ -3783,7 +3777,7 @@
have e:"e = setsum (\<lambda>i. d) {..<DIM('a)}" unfolding setsum_constant d_def using dimge1
unfolding real_eq_of_nat by auto
show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
- using z[unfolded mem_interval] apply(erule_tac x=i in allE) by(auto simp add:euclidean_simps) qed
+ using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed
hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption
unfolding k_def apply(rule, rule Max_ge) using c(1) by auto
have "d \<le> e" unfolding d_def apply(rule mult_imp_div_pos_le) using `e>0` dimge1 unfolding mult_le_cancel_left1 by auto
@@ -3792,9 +3786,9 @@
hence "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof
fix y assume y:"y\<in>cball x d"
{ fix i assume "i<DIM('a)" hence "x $$ i - d \<le> y $$ i" "y $$ i \<le> x $$ i + d"
- using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by(auto simp add:euclidean_simps) }
+ using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by auto }
thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm
- by(auto simp add:euclidean_simps) qed
+ by auto qed
hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous)
apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball)
apply force
@@ -3929,10 +3923,10 @@
proof(rule,rule) fix i assume i:"i<DIM('a)"
have "((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $$ i =
((norm (a - b) - norm (a - x)) * (a $$ i) + norm (a - x) * (b $$ i)) / norm (a - b)"
- using Fal by(auto simp add: field_simps euclidean_simps)
+ using Fal by(auto simp add: field_simps)
also have "\<dots> = x$$i" apply(rule divide_eq_imp[OF Fal])
unfolding as[unfolded dist_norm] using as[unfolded dist_triangle_eq] apply-
- apply(subst (asm) euclidean_eq) using i apply(erule_tac x=i in allE) by(auto simp add:field_simps euclidean_simps)
+ apply(subst (asm) euclidean_eq) using i apply(erule_tac x=i in allE) by(auto simp add:field_simps)
finally show "x $$ i = ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $$ i"
by auto
qed(insert Fal2, auto) qed qed
@@ -3943,7 +3937,7 @@
proof- have *:"\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" by auto
show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *)
unfolding euclidean_eq[where 'a='a]
- by(auto simp add:field_simps euclidean_simps) qed
+ by(auto simp add:field_simps) qed
lemma between_mem_convex_hull:
"between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
@@ -3962,7 +3956,7 @@
have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
unfolding dist_norm unfolding norm_scaleR[THEN sym] apply(rule arg_cong[where f=norm]) using `e>0`
- by(auto simp add: euclidean_simps euclidean_eq[where 'a='a] field_simps)
+ by(auto simp add: euclidean_eq[where 'a='a] field_simps)
also have "\<dots> = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
also have "\<dots> < d" using as[unfolded dist_norm] and `e>0`
by(auto simp add:pos_divide_less_eq[OF `e>0`] mult_commute)
@@ -4042,7 +4036,7 @@
apply(rule_tac x="\<lambda>y. inner y x" in exI) apply(rule,rule) unfolding mem_Collect_eq apply(erule exE)
using as(1) apply(erule_tac x=i in allE) unfolding sumbas apply safe unfolding not_less basis_zero
unfolding substdbasis_expansion_unique[OF assms] euclidean_component_def[THEN sym]
- using as(2,3) by(auto simp add:dot_basis not_less basis_zero)
+ using as(2,3) by(auto simp add:dot_basis not_less)
qed qed
lemma std_simplex:
@@ -4058,11 +4052,11 @@
fix x::"'a" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x<DIM('a). 0 \<le> xa $$ x) \<and> setsum (op $$ xa) {..<DIM('a)} \<le> 1"
show "(\<forall>xa<DIM('a). 0 < x $$ xa) \<and> setsum (op $$ x) {..<DIM('a)} < 1" apply(safe) proof-
fix i assume i:"i<DIM('a)" thus "0 < x $$ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`
- unfolding dist_norm by(auto simp add: inner_simps euclidean_component_def dot_basis elim!:allE[where x=i])
+ unfolding dist_norm by (auto elim!:allE[where x=i])
next have **:"dist x (x + (e / 2) *\<^sub>R basis 0) < e" using `e>0`
unfolding dist_norm by(auto intro!: mult_strict_left_mono)
have "\<And>i. i<DIM('a) \<Longrightarrow> (x + (e / 2) *\<^sub>R basis 0) $$ i = x$$i + (if i = 0 then e/2 else 0)"
- unfolding euclidean_component_def by(auto simp add:inner_simps dot_basis)
+ by auto
hence *:"setsum (op $$ (x + (e / 2) *\<^sub>R basis 0)) {..<DIM('a)} = setsum (\<lambda>i. x$$i + (if 0 = i then e/2 else 0)) {..<DIM('a)}"
apply(rule_tac setsum_cong) by auto
have "setsum (op $$ x) {..<DIM('a)} < setsum (op $$ (x + (e / 2) *\<^sub>R basis 0)) {..<DIM('a)}" unfolding * setsum_addf
@@ -4143,7 +4137,7 @@
setsum (\<lambda>i. x$$i + (if a = i then e/2 else 0)) d" by(rule_tac setsum_cong, auto)
have h1: "(ALL i<DIM('a). i ~: d --> (x + (e / 2) *\<^sub>R basis a) $$ i = 0)"
using as[THEN spec[where x="x + (e / 2) *\<^sub>R basis a"]] `a:d` using x0
- by(auto simp add: norm_basis elim:allE[where x=a])
+ by(auto elim:allE[where x=a])
have "setsum (op $$ x) d < setsum (op $$ (x + (e / 2) *\<^sub>R basis a)) d" unfolding * setsum_addf
using `0<e` `a:d` using `finite d` by(auto simp add: setsum_delta')
also have "\<dots> \<le> 1" using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R basis a"] by auto
@@ -4776,7 +4770,7 @@
} from this obtain mS where mS_def: "!S : I. (mS(S) > (1 :: real) &
(!e. (e>1 & e<=mS(S)) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S))" by metis
obtain e where e_def: "e=Min (mS ` I)" by auto
- have "e : (mS ` I)" using e_def assms `I ~= {}` by (simp add: Min_in)
+ have "e : (mS ` I)" using e_def assms `I ~= {}` by simp
hence "e>(1 :: real)" using mS_def by auto
moreover have "!S : I. e<=mS(S)" using e_def assms by auto
ultimately have "EX e>1. (1 - e) *\<^sub>R x + e *\<^sub>R z : Inter I" using mS_def by auto
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Aug 23 14:11:02 2011 -0700
@@ -598,7 +598,7 @@
case True thus ?thesis
apply(rule_tac x="(min (b$$i - a$$i) e) / 2" in exI)
using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2)
- unfolding mem_interval euclidean_simps basis_component
+ unfolding mem_interval euclidean_simps
using i by (auto simp add: field_simps)
next note * = assms(2)[unfolded mem_interval,THEN spec[where x=i]]
case False moreover have "a $$ i < x $$ i" using False * by auto
@@ -614,7 +614,7 @@
ultimately show ?thesis
apply(rule_tac x="- (min (x$$i - a$$i) e) / 2" in exI)
using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2)
- unfolding mem_interval euclidean_simps basis_component
+ unfolding mem_interval euclidean_simps
using i by (auto simp add: field_simps)
qed
qed
@@ -655,7 +655,7 @@
proof -
have fA: "finite {..<DIM('a)}" by simp
have "?rhs = (\<Sum>i<DIM('a). x$$i *\<^sub>R f (basis i))$$j"
- by (simp add: euclidean_simps)
+ by simp
then show ?thesis
unfolding linear_setsum_mul[OF lf fA, symmetric]
unfolding euclidean_representation[symmetric] ..
@@ -1550,7 +1550,7 @@
apply(rule has_derivative_sequence[OF assms(1) _ assms(3), of "\<lambda>n x. f n x + (f 0 a - f n a)"])
apply(rule,rule)
apply(rule has_derivative_add_const, rule assms(2)[rule_format], assumption)
- apply(rule `a\<in>s`) by(auto intro!: tendsto_const)
+ apply(rule `a\<in>s`) by auto
qed auto
lemma has_antiderivative_limit:
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Tue Aug 23 14:11:02 2011 -0700
@@ -515,7 +515,7 @@
shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}"
proof(induct k)
case 0
- have th: "{f. \<forall>i. f i = i} = {id}" by (auto intro: ext)
+ have th: "{f. \<forall>i. f i = i} = {id}" by auto
show ?case by (auto simp add: th)
next
case (Suc k)
@@ -525,14 +525,14 @@
apply (auto simp add: image_iff)
apply (rule_tac x="x (Suc k)" in bexI)
apply (rule_tac x = "\<lambda>i. if i = Suc k then i else x i" in exI)
- apply (auto intro: ext)
+ apply auto
done
with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f]
show ?case by metis
qed
-lemma eq_id_iff[simp]: "(\<forall>x. f x = x) = (f = id)" by (auto intro: ext)
+lemma eq_id_iff[simp]: "(\<forall>x. f x = x) = (f = id)" by auto
lemma det_linear_rows_setsum_lemma:
assumes fS: "finite S" and fT: "finite T"
@@ -575,7 +575,7 @@
blast intro: finite_cartesian_product fS finite,
blast intro: finite_cartesian_product fS finite)
using `z \<notin> T`
- apply (auto intro: ext)
+ apply auto
apply (rule cong[OF refl[of det]])
by vector
qed
@@ -739,7 +739,7 @@
unfolding setsum_diff1'[OF fU iU] setsum_cmul
apply -
apply (rule vector_mul_lcancel_imp[OF ci])
- apply (auto simp add: vector_smult_assoc vector_smult_rneg field_simps)
+ apply (auto simp add: field_simps)
unfolding stupid ..
have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}"
unfolding thr0
@@ -775,7 +775,7 @@
have kUk: "k \<notin> ?Uk" by simp
have th00: "\<And>k s. x$k *s row k A + s = (x$k - 1) *s row k A + row k A + s"
by (vector field_simps)
- have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" by (auto intro: ext)
+ have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" by auto
have "(\<chi> i. row i A) = A" by (vector row_def)
then have thd1: "det (\<chi> i. row i A) = det A" by simp
have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A"
@@ -931,7 +931,7 @@
unfolding dot_norm_neg dist_norm[symmetric]
unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
note fc = this
- show ?thesis unfolding linear_def vector_eq[where 'a="real^'n"] smult_conv_scaleR by (simp add: inner_simps fc field_simps)
+ show ?thesis unfolding linear_def vector_eq[where 'a="real^'n"] smult_conv_scaleR by (simp add: inner_add fc field_simps)
qed
lemma isometry_linear:
@@ -973,7 +973,7 @@
"x' = norm x *\<^sub>R x0'" "y' = norm y *\<^sub>R y0'"
"norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1"
"norm(x0' - y0') = norm(x0 - y0)"
- hence *:"x0 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0' - y0 \<bullet> x0 " by(simp add: norm_eq norm_eq_1 inner_simps)
+ hence *:"x0 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0' - y0 \<bullet> x0 " by(simp add: norm_eq norm_eq_1 inner_add inner_diff)
have "norm(x' - y') = norm(x - y)"
apply (subst H(1))
apply (subst H(2))
@@ -981,7 +981,7 @@
apply (subst H(4))
using H(5-9)
apply (simp add: norm_eq norm_eq_1)
- apply (simp add: inner_simps smult_conv_scaleR) unfolding *
+ apply (simp add: inner_diff smult_conv_scaleR) unfolding *
by (simp add: field_simps) }
note th0 = this
let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)"
@@ -1015,7 +1015,7 @@
"norm (f (inverse (norm x) *\<^sub>R x) - f (inverse (norm y) *\<^sub>R y)) =
norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)"
using z
- by (auto simp add: vector_smult_assoc field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
+ by (auto simp add: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
by (simp add: dist_norm)}
ultimately have "dist (?g x) (?g y) = dist x y" by blast}
@@ -1049,7 +1049,7 @@
by (simp add: eval_nat_numeral setprod_numseg mult_commute)
lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
- by (simp add: det_def sign_id UNIV_1)
+ by (simp add: det_def sign_id)
lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1"
proof-
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Aug 23 14:11:02 2011 -0700
@@ -129,19 +129,19 @@
lemma euclidean_component_zero [simp]: "0 $$ i = 0"
unfolding euclidean_component_def by (rule inner_zero_right)
-lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"
+lemma euclidean_component_add [simp]: "(x + y) $$ i = x $$ i + y $$ i"
unfolding euclidean_component_def by (rule inner_add_right)
-lemma euclidean_component_diff: "(x - y) $$ i = x $$ i - y $$ i"
+lemma euclidean_component_diff [simp]: "(x - y) $$ i = x $$ i - y $$ i"
unfolding euclidean_component_def by (rule inner_diff_right)
-lemma euclidean_component_minus: "(- x) $$ i = - (x $$ i)"
+lemma euclidean_component_minus [simp]: "(- x) $$ i = - (x $$ i)"
unfolding euclidean_component_def by (rule inner_minus_right)
-lemma euclidean_component_scaleR: "(scaleR a x) $$ i = a * (x $$ i)"
+lemma euclidean_component_scaleR [simp]: "(scaleR a x) $$ i = a * (x $$ i)"
unfolding euclidean_component_def by (rule inner_scaleR_right)
-lemma euclidean_component_setsum: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
+lemma euclidean_component_setsum [simp]: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
unfolding euclidean_component_def by (rule inner_setsum_right)
lemma euclidean_eqI:
@@ -183,7 +183,6 @@
fixes x :: "'a::euclidean_space"
shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)"
apply (rule euclidean_eqI)
- apply (simp add: euclidean_component_setsum euclidean_component_scaleR)
apply (simp add: if_distrib setsum_delta cong: if_cong)
done
@@ -194,8 +193,7 @@
lemma euclidean_lambda_beta [simp]:
"((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)"
- by (auto simp: euclidean_component_setsum euclidean_component_scaleR
- Chi_def if_distrib setsum_cases intro!: setsum_cong)
+ by (auto simp: Chi_def if_distrib setsum_cases intro!: setsum_cong)
lemma euclidean_lambda_beta':
"j < DIM('a) \<Longrightarrow> ((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = f j"
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Tue Aug 23 14:11:02 2011 -0700
@@ -180,7 +180,7 @@
"(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
"(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
"(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
- unfolding interval_bij_cart vec_lambda_beta vector_component_simps o_def split_conv
+ unfolding interval_bij_cart vector_component_simps o_def split_conv
unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this
from z(1) guess zf unfolding image_iff .. note zf=this
from z(2) guess zg unfolding image_iff .. note zg=this
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Aug 23 14:11:02 2011 -0700
@@ -485,7 +485,7 @@
show "k\<subseteq>{a..b}" apply(rule,unfold mem_interval,rule,rule)
proof fix i x assume i:"i<DIM('a)" assume "x \<in> k" moreover have "\<pi>' i < l \<or> \<pi>' i = l \<or> \<pi>' i > l" by auto
ultimately show "a$$i \<le> x$$i" "x$$i \<le> b$$i" using abcd[of i] using l using i
- by(auto elim:disjE elim!:allE[where x=i] simp add:eucl_le[where 'a='a])
+ by(auto elim!:allE[where x=i] simp add:eucl_le[where 'a='a]) (* FIXME: SLOW *)
qed have "\<And>l. ?p1 l \<noteq> {}" "\<And>l. ?p2 l \<noteq> {}" unfolding interval_eq_empty not_ex apply(rule_tac[!] allI)
proof- case goal1 thus ?case using abcd[of x] by auto
next case goal2 thus ?case using abcd[of x] by auto
@@ -967,7 +967,7 @@
subsection {* The set we're concerned with must be closed. *}
lemma division_of_closed: "s division_of i \<Longrightarrow> closed (i::('n::ordered_euclidean_space) set)"
- unfolding division_of_def by(fastsimp intro!: closed_Union closed_interval)
+ unfolding division_of_def by fastsimp
subsection {* General bisection principle for intervals; might be useful elsewhere. *}
@@ -2544,7 +2544,7 @@
apply(subst interval_doublesplit[OF k]) apply(rule content_pos_le) apply(rule indicator_pos_le)
proof- have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) * ?i x) \<le> (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}))"
apply(rule setsum_mono) unfolding split_paired_all split_conv
- apply(rule mult_right_le_one_le) apply(drule p'(4)) by(auto simp add:interval_doublesplit[OF k] intro!:content_pos_le)
+ apply(rule mult_right_le_one_le) apply(drule p'(4)) by(auto simp add:interval_doublesplit[OF k])
also have "... < e" apply(subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]])
proof- case goal1 have "content ({u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<le> content {u..v}"
unfolding interval_doublesplit[OF k] apply(rule content_subset) unfolding interval_doublesplit[THEN sym,OF k] by auto
@@ -4627,7 +4627,7 @@
case goal1 show ?case using int .
next case goal2 thus ?case apply-apply(cases "x\<in>s") using assms(3) by auto
next case goal3 thus ?case apply-apply(cases "x\<in>s")
- using assms(4) by (auto intro: tendsto_const)
+ using assms(4) by auto
next case goal4 note * = integral_nonneg
have "\<And>k. norm (integral {a..b} (\<lambda>x. if x \<in> s then f k x else 0)) \<le> norm (integral s (f k))"
unfolding real_norm_def apply(subst abs_of_nonneg) apply(rule *[OF int])
@@ -4678,7 +4678,7 @@
next case goal2 thus ?case apply(rule integrable_sub) using assms(1) by auto
next case goal3 thus ?case using *[of x "Suc k" "Suc (Suc k)"] by auto
next case goal4 thus ?case apply-apply(rule tendsto_diff)
- using seq_offset[OF assms(3)[rule_format],of x 1] by (auto intro: tendsto_const)
+ using seq_offset[OF assms(3)[rule_format],of x 1] by auto
next case goal5 thus ?case using assms(4) unfolding bounded_iff
apply safe apply(rule_tac x="a + norm (integral s (\<lambda>x. f 0 x))" in exI)
apply safe apply(erule_tac x="integral s (\<lambda>x. f (Suc k) x)" in ballE) unfolding sub
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Aug 23 14:11:02 2011 -0700
@@ -1659,10 +1659,9 @@
have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+
have Ppe:"setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp \<le> e"
using component_le_norm[of "setsum (\<lambda>x. f x) ?Pp" i] fPs[OF PpP]
- unfolding euclidean_component_setsum by(auto intro: abs_le_D1)
+ by(auto intro: abs_le_D1)
have Pne: "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn \<le> e"
using component_le_norm[of "setsum (\<lambda>x. - f x) ?Pn" i] fPs[OF PnP]
- unfolding euclidean_component_setsum euclidean_component_minus
by(auto simp add: setsum_negf intro: abs_le_D1)
have "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn"
apply (subst thp)
@@ -2825,7 +2824,7 @@
unfolding infnorm_def
unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
unfolding infnorm_set_image ball_simps
- apply(subst (1) euclidean_eq) unfolding euclidean_component_zero
+ apply(subst (1) euclidean_eq)
by auto
then show ?thesis using infnorm_pos_le[of x] by simp
qed
@@ -2836,7 +2835,7 @@
lemma infnorm_neg: "infnorm (- x) = infnorm x"
unfolding infnorm_def
apply (rule cong[of "Sup" "Sup"])
- apply blast by(auto simp add: euclidean_component_minus)
+ apply blast by auto
lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"
proof-
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 23 14:11:02 2011 -0700
@@ -14,7 +14,7 @@
lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
- apply(auto simp add:power2_eq_square) unfolding euclidean_component_diff ..
+ by(auto simp add:power2_eq_square)
lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
@@ -5601,26 +5601,17 @@
lemma subspace_substandard:
"subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
- unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *)
+ unfolding subspace_def by auto
lemma closed_substandard:
"closed {x::'a::euclidean_space. \<forall>i<DIM('a). P i --> x$$i = 0}" (is "closed ?A")
proof-
let ?D = "{i. P i} \<inter> {..<DIM('a)}"
- let ?Bs = "{{x::'a. inner (basis i) x = 0}| i. i \<in> ?D}"
- { fix x
- { assume "x\<in>?A"
- hence x:"\<forall>i\<in>?D. x $$ i = 0" by auto
- hence "x\<in> \<Inter> ?Bs" by(auto simp add: x euclidean_component_def) }
- moreover
- { assume x:"x\<in>\<Inter>?Bs"
- { fix i assume i:"i \<in> ?D"
- then obtain B where BB:"B \<in> ?Bs" and B:"B = {x::'a. inner (basis i) x = 0}" by auto
- hence "x $$ i = 0" unfolding B using x unfolding euclidean_component_def by auto }
- hence "x\<in>?A" by auto }
- ultimately have "x\<in>?A \<longleftrightarrow> x\<in> \<Inter>?Bs" .. }
- hence "?A = \<Inter> ?Bs" by auto
- thus ?thesis by(auto simp add: closed_Inter closed_hyperplane)
+ have "closed (\<Inter>i\<in>?D. {x::'a. x$$i = 0})"
+ by (simp add: closed_INT closed_Collect_eq)
+ also have "(\<Inter>i\<in>?D. {x::'a. x$$i = 0}) = ?A"
+ by auto
+ finally show "closed ?A" .
qed
lemma dim_substandard: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
@@ -5645,7 +5636,7 @@
have y:"x = y + (x$$k) *\<^sub>R basis k" unfolding y_def by auto
{ fix i assume i':"i \<notin> F"
hence "y $$ i = 0" unfolding y_def
- using *[THEN spec[where x=i]] by(auto simp add: euclidean_simps) }
+ using *[THEN spec[where x=i]] by auto }
hence "y \<in> span (basis ` F)" using insert(3) by auto
hence "y \<in> span (basis ` (insert k F))"
using span_mono[of "?bas ` F" "?bas ` (insert k F)"]
@@ -5763,25 +5754,25 @@
case False
{ fix y assume "a \<le> y" "y \<le> b" "m > 0"
hence "m *\<^sub>R a + c \<le> m *\<^sub>R y + c" "m *\<^sub>R y + c \<le> m *\<^sub>R b + c"
- unfolding eucl_le[where 'a='a] by(auto simp add: euclidean_simps)
+ unfolding eucl_le[where 'a='a] by auto
} moreover
{ fix y assume "a \<le> y" "y \<le> b" "m < 0"
hence "m *\<^sub>R b + c \<le> m *\<^sub>R y + c" "m *\<^sub>R y + c \<le> m *\<^sub>R a + c"
- unfolding eucl_le[where 'a='a] by(auto simp add: mult_left_mono_neg euclidean_simps)
+ unfolding eucl_le[where 'a='a] by(auto simp add: mult_left_mono_neg)
} moreover
{ fix y assume "m > 0" "m *\<^sub>R a + c \<le> y" "y \<le> m *\<^sub>R b + c"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
apply(auto simp add: pth_3[symmetric]
intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
- by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff euclidean_simps)
+ by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
} moreover
{ fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
apply(auto simp add: pth_3[symmetric]
intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
- by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff euclidean_simps)
+ by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
}
ultimately show ?thesis using False by auto
qed