1.1 --- a/NEWS Thu Aug 18 22:50:28 2011 +0200
1.2 +++ b/NEWS Thu Aug 18 14:08:39 2011 -0700
1.3 @@ -199,6 +199,19 @@
1.4 tendsto_vector ~> vec_tendstoI
1.5 Cauchy_vector ~> vec_CauchyI
1.6
1.7 +* Complex_Main: The locale interpretations for the bounded_linear and
1.8 +bounded_bilinear locales have been removed, in order to reduce the
1.9 +number of duplicate lemmas. Users must use the original names for
1.10 +distributivity theorems, potential INCOMPATIBILITY.
1.11 +
1.12 + divide.add ~> add_divide_distrib
1.13 + divide.diff ~> diff_divide_distrib
1.14 + divide.setsum ~> setsum_divide_distrib
1.15 + mult.add_right ~> right_distrib
1.16 + mult.diff_right ~> right_diff_distrib
1.17 + mult_right.setsum ~> setsum_right_distrib
1.18 + mult_left.diff ~> left_diff_distrib
1.19 +
1.20
1.21 *** Document preparation ***
1.22
2.1 --- a/src/HOL/Import/HOLLightReal.thy Thu Aug 18 22:50:28 2011 +0200
2.2 +++ b/src/HOL/Import/HOLLightReal.thy Thu Aug 18 14:08:39 2011 -0700
2.3 @@ -112,7 +112,7 @@
2.4
2.5 lemma REAL_DIFFSQ:
2.6 "((x :: real) + y) * (x - y) = x * x - y * y"
2.7 - by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) mult.add_right mult_diff_mult)
2.8 + by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) right_distrib mult_diff_mult)
2.9
2.10 lemma REAL_ABS_TRIANGLE_LE:
2.11 "abs (x :: real) + abs (y - x) \<le> z \<longrightarrow> abs y \<le> z"
2.12 @@ -295,7 +295,7 @@
2.13 (\<forall>(x :: real). 0 * x = 0) \<and>
2.14 (\<forall>(x :: real) y z. x * (y + z) = x * y + x * z) \<and>
2.15 (\<forall>(x :: real). x ^ 0 = 1) \<and> (\<forall>(x :: real) n. x ^ Suc n = x * x ^ n)"
2.16 - by (auto simp add: mult.add_right)
2.17 + by (auto simp add: right_distrib)
2.18
2.19 lemma REAL_COMPLETE:
2.20 "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
3.1 --- a/src/HOL/Library/Convex.thy Thu Aug 18 22:50:28 2011 +0200
3.2 +++ b/src/HOL/Library/Convex.thy Thu Aug 18 14:08:39 2011 -0700
3.3 @@ -129,7 +129,7 @@
3.4 have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
3.5 hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
3.6 hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
3.7 - hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
3.8 + hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
3.9 from this asms
3.10 have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastsimp
3.11 hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
3.12 @@ -410,7 +410,7 @@
3.13 have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
3.14 hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
3.15 hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
3.16 - hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
3.17 + hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
3.18 have "convex C" using asms by auto
3.19 hence asum: "(\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
3.20 using asms convex_setsum[OF `finite s`
3.21 @@ -433,7 +433,7 @@
3.22 using add_right_mono[OF mult_left_mono[of _ _ "1 - a i",
3.23 OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp
3.24 also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
3.25 - unfolding mult_right.setsum[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
3.26 + unfolding setsum_right_distrib[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
3.27 also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
3.28 also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
3.29 finally have "f (\<Sum> j \<in> insert i s. a j *\<^sub>R y j) \<le> (\<Sum> j \<in> insert i s. a j * f (y j))"
4.1 --- a/src/HOL/Library/FrechetDeriv.thy Thu Aug 18 22:50:28 2011 +0200
4.2 +++ b/src/HOL/Library/FrechetDeriv.thy Thu Aug 18 14:08:39 2011 -0700
4.3 @@ -5,7 +5,7 @@
4.4 header {* Frechet Derivative *}
4.5
4.6 theory FrechetDeriv
4.7 -imports Lim Complex_Main
4.8 +imports Complex_Main
4.9 begin
4.10
4.11 definition
4.12 @@ -398,9 +398,11 @@
4.13 by (simp only: FDERIV_lemma)
4.14 qed
4.15
4.16 -lemmas FDERIV_mult = mult.FDERIV
4.17 +lemmas FDERIV_mult =
4.18 + bounded_bilinear.FDERIV [OF bounded_bilinear_mult]
4.19
4.20 -lemmas FDERIV_scaleR = scaleR.FDERIV
4.21 +lemmas FDERIV_scaleR =
4.22 + bounded_bilinear.FDERIV [OF bounded_bilinear_scaleR]
4.23
4.24
4.25 subsection {* Powers *}
4.26 @@ -427,10 +429,10 @@
4.27 subsection {* Inverse *}
4.28
4.29 lemmas bounded_linear_mult_const =
4.30 - mult.bounded_linear_left [THEN bounded_linear_compose]
4.31 + bounded_linear_mult_left [THEN bounded_linear_compose]
4.32
4.33 lemmas bounded_linear_const_mult =
4.34 - mult.bounded_linear_right [THEN bounded_linear_compose]
4.35 + bounded_linear_mult_right [THEN bounded_linear_compose]
4.36
4.37 lemma FDERIV_inverse:
4.38 fixes x :: "'a::real_normed_div_algebra"
4.39 @@ -510,7 +512,7 @@
4.40 fixes x :: "'a::real_normed_field" shows
4.41 "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
4.42 apply (unfold fderiv_def)
4.43 - apply (simp add: mult.bounded_linear_left)
4.44 + apply (simp add: bounded_linear_mult_left)
4.45 apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
4.46 apply (subst diff_divide_distrib)
4.47 apply (subst times_divide_eq_left [symmetric])
5.1 --- a/src/HOL/Library/Inner_Product.thy Thu Aug 18 22:50:28 2011 +0200
5.2 +++ b/src/HOL/Library/Inner_Product.thy Thu Aug 18 14:08:39 2011 -0700
5.3 @@ -5,7 +5,7 @@
5.4 header {* Inner Product Spaces and the Gradient Derivative *}
5.5
5.6 theory Inner_Product
5.7 -imports Complex_Main FrechetDeriv
5.8 +imports FrechetDeriv
5.9 begin
5.10
5.11 subsection {* Real inner product spaces *}
5.12 @@ -43,6 +43,9 @@
5.13 lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
5.14 by (simp add: diff_minus inner_add_left)
5.15
5.16 +lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
5.17 + by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
5.18 +
5.19 text {* Transfer distributivity rules to right argument. *}
5.20
5.21 lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
5.22 @@ -60,6 +63,9 @@
5.23 lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
5.24 using inner_diff_left [of y z x] by (simp only: inner_commute)
5.25
5.26 +lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
5.27 + using inner_setsum_left [of f A x] by (simp only: inner_commute)
5.28 +
5.29 lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
5.30 lemmas inner_diff [algebra_simps] = inner_diff_left inner_diff_right
5.31 lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
5.32 @@ -148,8 +154,8 @@
5.33 setup {* Sign.add_const_constraint
5.34 (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
5.35
5.36 -interpretation inner:
5.37 - bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
5.38 +lemma bounded_bilinear_inner:
5.39 + "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
5.40 proof
5.41 fix x y z :: 'a and r :: real
5.42 show "inner (x + y) z = inner x z + inner y z"
5.43 @@ -167,15 +173,20 @@
5.44 qed
5.45 qed
5.46
5.47 -interpretation inner_left:
5.48 - bounded_linear "\<lambda>x::'a::real_inner. inner x y"
5.49 - by (rule inner.bounded_linear_left)
5.50 +lemmas tendsto_inner [tendsto_intros] =
5.51 + bounded_bilinear.tendsto [OF bounded_bilinear_inner]
5.52
5.53 -interpretation inner_right:
5.54 - bounded_linear "\<lambda>y::'a::real_inner. inner x y"
5.55 - by (rule inner.bounded_linear_right)
5.56 +lemmas isCont_inner [simp] =
5.57 + bounded_bilinear.isCont [OF bounded_bilinear_inner]
5.58
5.59 -declare inner.isCont [simp]
5.60 +lemmas FDERIV_inner =
5.61 + bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
5.62 +
5.63 +lemmas bounded_linear_inner_left =
5.64 + bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
5.65 +
5.66 +lemmas bounded_linear_inner_right =
5.67 + bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
5.68
5.69
5.70 subsection {* Class instances *}
5.71 @@ -260,29 +271,29 @@
5.72 by simp
5.73
5.74 lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
5.75 - unfolding gderiv_def inner_right.zero by (rule FDERIV_const)
5.76 + unfolding gderiv_def inner_zero_right by (rule FDERIV_const)
5.77
5.78 lemma GDERIV_add:
5.79 "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
5.80 \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
5.81 - unfolding gderiv_def inner_right.add by (rule FDERIV_add)
5.82 + unfolding gderiv_def inner_add_right by (rule FDERIV_add)
5.83
5.84 lemma GDERIV_minus:
5.85 "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
5.86 - unfolding gderiv_def inner_right.minus by (rule FDERIV_minus)
5.87 + unfolding gderiv_def inner_minus_right by (rule FDERIV_minus)
5.88
5.89 lemma GDERIV_diff:
5.90 "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
5.91 \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
5.92 - unfolding gderiv_def inner_right.diff by (rule FDERIV_diff)
5.93 + unfolding gderiv_def inner_diff_right by (rule FDERIV_diff)
5.94
5.95 lemma GDERIV_scaleR:
5.96 "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
5.97 \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
5.98 :> (scaleR (f x) dg + scaleR df (g x))"
5.99 - unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR
5.100 + unfolding gderiv_def deriv_fderiv inner_add_right inner_scaleR_right
5.101 apply (rule FDERIV_subst)
5.102 - apply (erule (1) scaleR.FDERIV)
5.103 + apply (erule (1) FDERIV_scaleR)
5.104 apply (simp add: mult_ac)
5.105 done
5.106
5.107 @@ -306,7 +317,7 @@
5.108 assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
5.109 proof -
5.110 have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
5.111 - by (intro inner.FDERIV FDERIV_ident)
5.112 + by (intro FDERIV_inner FDERIV_ident)
5.113 have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
5.114 by (simp add: fun_eq_iff inner_commute)
5.115 have "0 < inner x x" using `x \<noteq> 0` by simp
6.1 --- a/src/HOL/Library/Product_Vector.thy Thu Aug 18 22:50:28 2011 +0200
6.2 +++ b/src/HOL/Library/Product_Vector.thy Thu Aug 18 14:08:39 2011 -0700
6.3 @@ -489,11 +489,11 @@
6.4
6.5 subsection {* Pair operations are linear *}
6.6
6.7 -interpretation fst: bounded_linear fst
6.8 +lemma bounded_linear_fst: "bounded_linear fst"
6.9 using fst_add fst_scaleR
6.10 by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
6.11
6.12 -interpretation snd: bounded_linear snd
6.13 +lemma bounded_linear_snd: "bounded_linear snd"
6.14 using snd_add snd_scaleR
6.15 by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
6.16
7.1 --- a/src/HOL/Lim.thy Thu Aug 18 22:50:28 2011 +0200
7.2 +++ b/src/HOL/Lim.thy Thu Aug 18 14:08:39 2011 -0700
7.3 @@ -321,17 +321,23 @@
7.4 "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
7.5 by (rule tendsto_right_zero)
7.6
7.7 -lemmas LIM_mult = mult.LIM
7.8 +lemmas LIM_mult =
7.9 + bounded_bilinear.LIM [OF bounded_bilinear_mult]
7.10
7.11 -lemmas LIM_mult_zero = mult.LIM_prod_zero
7.12 +lemmas LIM_mult_zero =
7.13 + bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult]
7.14
7.15 -lemmas LIM_mult_left_zero = mult.LIM_left_zero
7.16 +lemmas LIM_mult_left_zero =
7.17 + bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult]
7.18
7.19 -lemmas LIM_mult_right_zero = mult.LIM_right_zero
7.20 +lemmas LIM_mult_right_zero =
7.21 + bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult]
7.22
7.23 -lemmas LIM_scaleR = scaleR.LIM
7.24 +lemmas LIM_scaleR =
7.25 + bounded_bilinear.LIM [OF bounded_bilinear_scaleR]
7.26
7.27 -lemmas LIM_of_real = of_real.LIM
7.28 +lemmas LIM_of_real =
7.29 + bounded_linear.LIM [OF bounded_linear_of_real]
7.30
7.31 lemma LIM_power:
7.32 fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
7.33 @@ -446,11 +452,11 @@
7.34 "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
7.35 unfolding isCont_def by (rule LIM)
7.36
7.37 -lemmas isCont_scaleR [simp] = scaleR.isCont
7.38 +lemmas isCont_scaleR [simp] =
7.39 + bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
7.40
7.41 -lemma isCont_of_real [simp]:
7.42 - "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
7.43 - by (rule of_real.isCont)
7.44 +lemmas isCont_of_real [simp] =
7.45 + bounded_linear.isCont [OF bounded_linear_of_real]
7.46
7.47 lemma isCont_power [simp]:
7.48 fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
8.1 --- a/src/HOL/Limits.thy Thu Aug 18 22:50:28 2011 +0200
8.2 +++ b/src/HOL/Limits.thy Thu Aug 18 14:08:39 2011 -0700
8.3 @@ -510,9 +510,9 @@
8.4 "Zfun f F \<Longrightarrow> Zfun (\<lambda>x. a ** f x) F"
8.5 by (rule bounded_linear_right [THEN bounded_linear.Zfun])
8.6
8.7 -lemmas Zfun_mult = mult.Zfun
8.8 -lemmas Zfun_mult_right = mult.Zfun_right
8.9 -lemmas Zfun_mult_left = mult.Zfun_left
8.10 +lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult]
8.11 +lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult]
8.12 +lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult]
8.13
8.14
8.15 subsection {* Limits *}
8.16 @@ -752,7 +752,7 @@
8.17
8.18 subsubsection {* Linear operators and multiplication *}
8.19
8.20 -lemma (in bounded_linear) tendsto [tendsto_intros]:
8.21 +lemma (in bounded_linear) tendsto:
8.22 "(g ---> a) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) F"
8.23 by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
8.24
8.25 @@ -760,7 +760,7 @@
8.26 "(g ---> 0) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> 0) F"
8.27 by (drule tendsto, simp only: zero)
8.28
8.29 -lemma (in bounded_bilinear) tendsto [tendsto_intros]:
8.30 +lemma (in bounded_bilinear) tendsto:
8.31 "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) F"
8.32 by (simp only: tendsto_Zfun_iff prod_diff_prod
8.33 Zfun_add Zfun Zfun_left Zfun_right)
8.34 @@ -779,7 +779,14 @@
8.35 "(f ---> 0) F \<Longrightarrow> ((\<lambda>x. c ** f x) ---> 0) F"
8.36 by (rule bounded_linear.tendsto_zero [OF bounded_linear_right])
8.37
8.38 -lemmas tendsto_mult = mult.tendsto
8.39 +lemmas tendsto_of_real [tendsto_intros] =
8.40 + bounded_linear.tendsto [OF bounded_linear_of_real]
8.41 +
8.42 +lemmas tendsto_scaleR [tendsto_intros] =
8.43 + bounded_bilinear.tendsto [OF bounded_bilinear_scaleR]
8.44 +
8.45 +lemmas tendsto_mult [tendsto_intros] =
8.46 + bounded_bilinear.tendsto [OF bounded_bilinear_mult]
8.47
8.48 lemma tendsto_power [tendsto_intros]:
8.49 fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
8.50 @@ -897,7 +904,7 @@
8.51 apply (erule (1) inverse_diff_inverse)
8.52 apply (rule Zfun_minus)
8.53 apply (rule Zfun_mult_left)
8.54 - apply (rule mult.Bfun_prod_Zfun)
8.55 + apply (rule bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult])
8.56 apply (erule (1) Bfun_inverse)
8.57 apply (simp add: tendsto_Zfun_iff)
8.58 done
8.59 @@ -921,7 +928,7 @@
8.60 fixes a b :: "'a::real_normed_field"
8.61 shows "\<lbrakk>(f ---> a) F; (g ---> b) F; b \<noteq> 0\<rbrakk>
8.62 \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) F"
8.63 - by (simp add: mult.tendsto tendsto_inverse divide_inverse)
8.64 + by (simp add: tendsto_mult tendsto_inverse divide_inverse)
8.65
8.66 lemma tendsto_sgn [tendsto_intros]:
8.67 fixes l :: "'a::real_normed_vector"
9.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Aug 18 22:50:28 2011 +0200
9.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Aug 18 14:08:39 2011 -0700
9.3 @@ -1202,7 +1202,7 @@
9.4 show "\<bar>(f z - z) $$ i\<bar> < d / real n" unfolding euclidean_simps proof(rule *)
9.5 show "\<bar>f x $$ i - x $$ i\<bar> \<le> norm (f y -f x) + norm (y - x)" apply(rule lem1[rule_format]) using as i by auto
9.6 show "\<bar>f x $$ i - f z $$ i\<bar> \<le> norm (f x - f z)" "\<bar>x $$ i - z $$ i\<bar> \<le> norm (x - z)"
9.7 - unfolding euclidean_component.diff[THEN sym] by(rule component_le_norm)+
9.8 + unfolding euclidean_component_diff[THEN sym] by(rule component_le_norm)+
9.9 have tria:"norm (y - x) \<le> norm (y - z) + norm (x - z)" using dist_triangle[of y x z,unfolded dist_norm]
9.10 unfolding norm_minus_commute by auto
9.11 also have "\<dots> < e / 2 + e / 2" apply(rule add_strict_mono) using as(4,5) by auto
9.12 @@ -1234,7 +1234,7 @@
9.13 assume as:"\<forall>i\<in>{1..n}. x i \<le> p" "i \<in> {1..n}"
9.14 { assume "x i = p \<or> x i = 0"
9.15 have "(\<chi>\<chi> i. real (x (b' i)) / real p) \<in> {0::'a..\<chi>\<chi> i. 1}" unfolding mem_interval
9.16 - apply safe unfolding euclidean_lambda_beta euclidean_component.zero
9.17 + apply safe unfolding euclidean_lambda_beta euclidean_component_zero
9.18 proof (simp_all only: if_P) fix j assume j':"j<DIM('a)"
9.19 hence j:"b' j \<in> {1..n}" using b' unfolding n_def bij_betw_def by auto
9.20 show "0 \<le> real (x (b' j)) / real p"
9.21 @@ -1262,11 +1262,11 @@
9.22 have "\<forall>i<DIM('a). q (b' i) \<in> {0..<p}" using q(1) b'[unfolded bij_betw_def] by auto
9.23 hence "\<forall>i<DIM('a). q (b' i) \<in> {0..p}" apply-apply(rule,erule_tac x=i in allE) by auto
9.24 hence "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta
9.25 - unfolding euclidean_component.zero apply (simp_all only: if_P)
9.26 + unfolding euclidean_component_zero apply (simp_all only: if_P)
9.27 apply(rule divide_nonneg_pos) using `p>0` unfolding divide_le_eq_1 by auto
9.28 hence d_fz_z:"d \<le> norm (f z - z)" apply(drule_tac d) .
9.29 case goal1 hence as:"\<forall>i<DIM('a). \<bar>f z $$ i - z $$ i\<bar> < d / real n" using `n>0` by(auto simp add:not_le)
9.30 - have "norm (f z - z) \<le> (\<Sum>i<DIM('a). \<bar>f z $$ i - z $$ i\<bar>)" unfolding euclidean_component.diff[THEN sym] by(rule norm_le_l1)
9.31 + have "norm (f z - z) \<le> (\<Sum>i<DIM('a). \<bar>f z $$ i - z $$ i\<bar>)" unfolding euclidean_component_diff[THEN sym] by(rule norm_le_l1)
9.32 also have "\<dots> < (\<Sum>i<DIM('a). d / real n)" apply(rule setsum_strict_mono) using as by auto
9.33 also have "\<dots> = d" unfolding real_eq_of_nat n_def using n using DIM_positive[where 'a='a] by auto
9.34 finally show False using d_fz_z by auto qed then guess i .. note i=this
9.35 @@ -1276,15 +1276,15 @@
9.36 def r' \<equiv> "(\<chi>\<chi> i. real (r (b' i)) / real p)::'a"
9.37 have "\<And>i. i<DIM('a) \<Longrightarrow> r (b' i) \<le> p" apply(rule order_trans) apply(rule rs(1)[OF b'_im,THEN conjunct2])
9.38 using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq)
9.39 - hence "r' \<in> {0..\<chi>\<chi> i. 1}" unfolding r'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
9.40 + hence "r' \<in> {0..\<chi>\<chi> i. 1}" unfolding r'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
9.41 apply (simp only: if_P)
9.42 apply(rule divide_nonneg_pos) using rs(1)[OF b'_im] q(1)[rule_format,OF b'_im] `p>0` by auto
9.43 def s' \<equiv> "(\<chi>\<chi> i. real (s (b' i)) / real p)::'a"
9.44 have "\<And>i. i<DIM('a) \<Longrightarrow> s (b' i) \<le> p" apply(rule order_trans) apply(rule rs(2)[OF b'_im,THEN conjunct2])
9.45 using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq)
9.46 - hence "s' \<in> {0..\<chi>\<chi> i.1}" unfolding s'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
9.47 + hence "s' \<in> {0..\<chi>\<chi> i.1}" unfolding s'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
9.48 apply (simp_all only: if_P) apply(rule divide_nonneg_pos) using rs(1)[OF b'_im] q(1)[rule_format,OF b'_im] `p>0` by auto
9.49 - have "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
9.50 + have "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
9.51 apply (simp_all only: if_P) apply(rule divide_nonneg_pos) using q(1)[rule_format,OF b'_im] `p>0` by(auto intro:less_imp_le)
9.52 have *:"\<And>x. 1 + real x = real (Suc x)" by auto
9.53 { have "(\<Sum>i<DIM('a). \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>i<DIM('a). 1)"
10.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Aug 18 22:50:28 2011 +0200
10.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Aug 18 14:08:39 2011 -0700
10.3 @@ -1523,7 +1523,7 @@
10.4 have ***:"\<And>y y1 y2 d dx::real. (y1\<le>y\<and>y2\<le>y) \<or> (y\<le>y1\<and>y\<le>y2) \<Longrightarrow> d < abs dx \<Longrightarrow> abs(y1 - y - - dx) \<le> d \<Longrightarrow> (abs (y2 - y - dx) \<le> d) \<Longrightarrow> False" by arith
10.5 show False apply(rule ***[OF **, where dx="d * D $ k $ j" and d="\<bar>D $ k $ j\<bar> / 2 * \<bar>d\<bar>"])
10.6 using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left
10.7 - unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
10.8 + unfolding abs_mult diff_minus_eq_add scaleR_minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
10.9 qed
10.10
10.11 subsection {* Lemmas for working on @{typ "real^1"} *}
11.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 18 22:50:28 2011 +0200
11.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 18 14:08:39 2011 -0700
11.3 @@ -18,7 +18,7 @@
11.4 (* ------------------------------------------------------------------------- *)
11.5
11.6 lemma linear_scaleR: "linear (%(x :: 'n::euclidean_space). scaleR c x)"
11.7 - by (metis linear_conv_bounded_linear scaleR.bounded_linear_right)
11.8 + by (metis linear_conv_bounded_linear bounded_linear_scaleR_right)
11.9
11.10 lemma injective_scaleR:
11.11 assumes "(c :: real) ~= 0"
11.12 @@ -128,7 +128,7 @@
11.13 proof- have *:"\<And>x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto
11.14 have **:"finite d" apply(rule finite_subset[OF assms]) by fastsimp
11.15 have ***:"\<And>i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\<Sum>x\<in>d. if x = i then f x else 0)"
11.16 - unfolding euclidean_component.setsum euclidean_scaleR basis_component *
11.17 + unfolding euclidean_component_setsum euclidean_component_scaleR basis_component *
11.18 apply(rule setsum_cong2) using assms by auto
11.19 show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto
11.20 qed
11.21 @@ -1175,7 +1175,7 @@
11.22 have u2:"u2 \<le> 1" unfolding obt2(3)[THEN sym] and not_le using obt2(2) by auto
11.23 have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
11.24 apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
11.25 - also have "\<dots> \<le> 1" unfolding mult.add_right[THEN sym] and as(3) using u1 u2 by auto
11.26 + also have "\<dots> \<le> 1" unfolding right_distrib[THEN sym] and as(3) using u1 u2 by auto
11.27 finally
11.28 show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI)
11.29 apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
11.30 @@ -2229,7 +2229,7 @@
11.31 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)
11.32 have "x : affine hull S" using assms hull_subset[of S] by auto
11.33 moreover have "1 / e + - ((1 - e) / e) = 1"
11.34 - using `e>0` mult_left.diff[of "1" "(1-e)" "1/e"] by auto
11.35 + using `e>0` left_diff_distrib[of "1" "(1-e)" "1/e"] by auto
11.36 ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x : affine hull S"
11.37 using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"] by (simp add: algebra_simps)
11.38 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)"
11.39 @@ -2957,7 +2957,7 @@
11.40 thus ?thesis apply(rule_tac x="basis 0" in exI, rule_tac x=1 in exI)
11.41 using True using DIM_positive[where 'a='a] by auto
11.42 next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms]
11.43 - apply - apply(erule exE)+ unfolding inner.zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
11.44 + apply - apply(erule exE)+ unfolding inner_zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
11.45
11.46 subsection {* Now set-to-set for closed/compact sets. *}
11.47
11.48 @@ -3053,7 +3053,7 @@
11.49 apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
11.50 apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
11.51 apply(rule assms[unfolded convex_def, rule_format]) prefer 6
11.52 - by (auto intro: tendsto_intros)
11.53 + by (auto intro!: tendsto_intros)
11.54
11.55 lemma convex_interior:
11.56 fixes s :: "'a::real_normed_vector set"
11.57 @@ -3221,13 +3221,13 @@
11.58 ultimately have "z \<in> convex hull {v \<in> c. u v \<le> 0}" unfolding convex_hull_explicit mem_Collect_eq
11.59 apply(rule_tac x="{v \<in> c. u v < 0}" in exI, rule_tac x="\<lambda>y. inverse (setsum u {x\<in>c. u x > 0}) * - u y" in exI)
11.60 using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def
11.61 - by(auto simp add: setsum_negf mult_right.setsum[THEN sym])
11.62 + by(auto simp add: setsum_negf setsum_right_distrib[THEN sym])
11.63 moreover have "\<forall>x\<in>{v \<in> c. 0 < u v}. 0 \<le> inverse (setsum u {x \<in> c. 0 < u x}) * u x"
11.64 apply (rule) apply (rule mult_nonneg_nonneg) using * by auto
11.65 hence "z \<in> convex hull {v \<in> c. u v > 0}" unfolding convex_hull_explicit mem_Collect_eq
11.66 apply(rule_tac x="{v \<in> c. 0 < u v}" in exI, rule_tac x="\<lambda>y. inverse (setsum u {x\<in>c. u x > 0}) * u y" in exI)
11.67 using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def using *
11.68 - by(auto simp add: setsum_negf mult_right.setsum[THEN sym])
11.69 + by(auto simp add: setsum_negf setsum_right_distrib[THEN sym])
11.70 ultimately show ?thesis apply(rule_tac x="{v\<in>c. u v \<le> 0}" in exI, rule_tac x="{v\<in>c. u v > 0}" in exI) by auto
11.71 qed
11.72
11.73 @@ -4157,7 +4157,7 @@
11.74 let ?D = "{..<DIM('a)}" let ?a = "setsum (\<lambda>b::'a. inverse (2 * real DIM('a)) *\<^sub>R b) {(basis i) | i. i<DIM('a)}"
11.75 have *:"{basis i :: 'a | i. i<DIM('a)} = basis ` ?D" by auto
11.76 { fix i assume i:"i<DIM('a)" have "?a $$ i = inverse (2 * real DIM('a))"
11.77 - unfolding euclidean_component.setsum * and setsum_reindex[OF basis_inj] and o_def
11.78 + unfolding euclidean_component_setsum * and setsum_reindex[OF basis_inj] and o_def
11.79 apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real DIM('a)) else 0) ?D"]) apply(rule setsum_cong2)
11.80 defer apply(subst setsum_delta') unfolding euclidean_component_def using i by(auto simp add:dot_basis) }
11.81 note ** = this
11.82 @@ -4270,7 +4270,7 @@
11.83 { fix i assume "i:d" have "?a $$ i = inverse (2 * real (card d))"
11.84 unfolding * setsum_reindex[OF basis_inj_on, OF assms(2)] o_def
11.85 apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real (card d)) else 0) ?D"])
11.86 - unfolding euclidean_component.setsum
11.87 + unfolding euclidean_component_setsum
11.88 apply(rule setsum_cong2)
11.89 using `i:d` `finite d` setsum_delta'[of d i "(%k. inverse (2 * real (card d)))"] d1 assms(2)
11.90 by (auto simp add: Euclidean_Space.basis_component[of i])}
11.91 @@ -4678,7 +4678,7 @@
11.92 hence x1: "x1 : affine hull S" using e1_def hull_subset[of S] by auto
11.93 def x2 == "z+ e2 *\<^sub>R (z-x)"
11.94 hence x2: "x2 : affine hull S" using e2_def hull_subset[of S] by auto
11.95 - have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using divide.add[of e1 e2 "e1+e2"] e1_def e2_def by simp
11.96 + have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using add_divide_distrib[of e1 e2 "e1+e2"] e1_def e2_def by simp
11.97 hence "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2"
11.98 using x1_def x2_def apply (auto simp add: algebra_simps)
11.99 using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z] by auto
12.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Aug 18 22:50:28 2011 +0200
12.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Aug 18 14:08:39 2011 -0700
12.3 @@ -93,13 +93,13 @@
12.4 proof -
12.5 have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) ---> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
12.6 ((\<lambda>t. (f t - f x) / (t - x) - y) ---> 0) (at x within ({x<..} \<inter> I))"
12.7 - by (intro Lim_cong_within) (auto simp add: divide.diff divide.add)
12.8 + by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib)
12.9 also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \<inter> I))"
12.10 by (simp add: Lim_null[symmetric])
12.11 also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \<inter> I))"
12.12 by (intro Lim_cong_within) (simp_all add: field_simps)
12.13 finally show ?thesis
12.14 - by (simp add: mult.bounded_linear_right has_derivative_within)
12.15 + by (simp add: bounded_linear_mult_right has_derivative_within)
12.16 qed
12.17
12.18 lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
12.19 @@ -140,10 +140,31 @@
12.20 apply (simp add: local.scaleR local.diff local.add local.zero)
12.21 done
12.22
12.23 +lemmas scaleR_right_has_derivative =
12.24 + bounded_linear.has_derivative [OF bounded_linear_scaleR_right, standard]
12.25 +
12.26 +lemmas scaleR_left_has_derivative =
12.27 + bounded_linear.has_derivative [OF bounded_linear_scaleR_left, standard]
12.28 +
12.29 +lemmas inner_right_has_derivative =
12.30 + bounded_linear.has_derivative [OF bounded_linear_inner_right, standard]
12.31 +
12.32 +lemmas inner_left_has_derivative =
12.33 + bounded_linear.has_derivative [OF bounded_linear_inner_left, standard]
12.34 +
12.35 +lemmas mult_right_has_derivative =
12.36 + bounded_linear.has_derivative [OF bounded_linear_mult_right, standard]
12.37 +
12.38 +lemmas mult_left_has_derivative =
12.39 + bounded_linear.has_derivative [OF bounded_linear_mult_left, standard]
12.40 +
12.41 +lemmas euclidean_component_has_derivative =
12.42 + bounded_linear.has_derivative [OF bounded_linear_euclidean_component]
12.43 +
12.44 lemma has_derivative_neg:
12.45 assumes "(f has_derivative f') net"
12.46 shows "((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net"
12.47 - using scaleR_right.has_derivative [where r="-1", OF assms] by auto
12.48 + using scaleR_right_has_derivative [where r="-1", OF assms] by auto
12.49
12.50 lemma has_derivative_add:
12.51 assumes "(f has_derivative f') net" and "(g has_derivative g') net"
12.52 @@ -181,9 +202,9 @@
12.53 has_derivative_id has_derivative_const
12.54 has_derivative_add has_derivative_sub has_derivative_neg
12.55 has_derivative_add_const
12.56 - scaleR_left.has_derivative scaleR_right.has_derivative
12.57 - inner_left.has_derivative inner_right.has_derivative
12.58 - euclidean_component.has_derivative
12.59 + scaleR_left_has_derivative scaleR_right_has_derivative
12.60 + inner_left_has_derivative inner_right_has_derivative
12.61 + euclidean_component_has_derivative
12.62
12.63 subsubsection {* Limit transformation for derivatives *}
12.64
12.65 @@ -459,7 +480,7 @@
12.66 "f differentiable net \<Longrightarrow>
12.67 (\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)"
12.68 unfolding differentiable_def
12.69 - apply(erule exE, drule scaleR_right.has_derivative) by auto
12.70 + apply(erule exE, drule scaleR_right_has_derivative) by auto
12.71
12.72 lemma differentiable_neg [intro]:
12.73 "f differentiable net \<Longrightarrow>
12.74 @@ -693,7 +714,7 @@
12.75 show False apply(rule ***[OF **, where dx="d * ?D k $$ j" and d="\<bar>?D k $$ j\<bar> / 2 * \<bar>d\<bar>"])
12.76 using *[of "-d"] and *[of d] and d[THEN conjunct1] and j
12.77 unfolding mult_minus_left
12.78 - unfolding abs_mult diff_minus_eq_add scaleR.minus_left
12.79 + unfolding abs_mult diff_minus_eq_add scaleR_minus_left
12.80 unfolding algebra_simps by (auto intro: mult_pos_pos)
12.81 qed
12.82
12.83 @@ -769,7 +790,7 @@
12.84 fix x assume x:"x \<in> {a<..<b}"
12.85 show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
12.86 by (intro has_derivative_intros assms(3)[rule_format,OF x]
12.87 - mult_right.has_derivative)
12.88 + mult_right_has_derivative)
12.89 qed(insert assms(1), auto simp add:field_simps)
12.90 then guess x ..
12.91 thus ?thesis apply(rule_tac x=x in bexI)
12.92 @@ -1740,7 +1761,7 @@
12.93 lemma has_vector_derivative_cmul:
12.94 "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
12.95 unfolding has_vector_derivative_def
12.96 - apply (drule scaleR_right.has_derivative)
12.97 + apply (drule scaleR_right_has_derivative)
12.98 by (auto simp add: algebra_simps)
12.99
12.100 lemma has_vector_derivative_cmul_eq:
12.101 @@ -1819,7 +1840,7 @@
12.102 shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x)"
12.103 using assms(2) unfolding has_vector_derivative_def apply-
12.104 apply(drule diff_chain_at[OF assms(1)[unfolded has_vector_derivative_def]])
12.105 - unfolding o_def scaleR.scaleR_left by auto
12.106 + unfolding o_def real_scaleR_def scaleR_scaleR .
12.107
12.108 lemma vector_diff_chain_within:
12.109 assumes "(f has_vector_derivative f') (at x within s)"
12.110 @@ -1827,6 +1848,6 @@
12.111 shows "((g o f) has_vector_derivative (f' *\<^sub>R g')) (at x within s)"
12.112 using assms(2) unfolding has_vector_derivative_def apply-
12.113 apply(drule diff_chain_within[OF assms(1)[unfolded has_vector_derivative_def]])
12.114 - unfolding o_def scaleR.scaleR_left by auto
12.115 + unfolding o_def real_scaleR_def scaleR_scaleR .
12.116
12.117 end
13.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 18 22:50:28 2011 +0200
13.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 18 14:08:39 2011 -0700
13.3 @@ -118,20 +118,38 @@
13.4 lemma bounded_linear_euclidean_component:
13.5 "bounded_linear (\<lambda>x. euclidean_component x i)"
13.6 unfolding euclidean_component_def
13.7 - by (rule inner.bounded_linear_right)
13.8 + by (rule bounded_linear_inner_right)
13.9
13.10 -interpretation euclidean_component:
13.11 - bounded_linear "\<lambda>x. euclidean_component x i"
13.12 - by (rule bounded_linear_euclidean_component)
13.13 +lemmas tendsto_euclidean_component [tendsto_intros] =
13.14 + bounded_linear.tendsto [OF bounded_linear_euclidean_component]
13.15
13.16 -declare euclidean_component.isCont [simp]
13.17 +lemmas isCont_euclidean_component [simp] =
13.18 + bounded_linear.isCont [OF bounded_linear_euclidean_component]
13.19 +
13.20 +lemma euclidean_component_zero: "0 $$ i = 0"
13.21 + unfolding euclidean_component_def by (rule inner_zero_right)
13.22 +
13.23 +lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"
13.24 + unfolding euclidean_component_def by (rule inner_add_right)
13.25 +
13.26 +lemma euclidean_component_diff: "(x - y) $$ i = x $$ i - y $$ i"
13.27 + unfolding euclidean_component_def by (rule inner_diff_right)
13.28 +
13.29 +lemma euclidean_component_minus: "(- x) $$ i = - (x $$ i)"
13.30 + unfolding euclidean_component_def by (rule inner_minus_right)
13.31 +
13.32 +lemma euclidean_component_scaleR: "(scaleR a x) $$ i = a * (x $$ i)"
13.33 + unfolding euclidean_component_def by (rule inner_scaleR_right)
13.34 +
13.35 +lemma euclidean_component_setsum: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
13.36 + unfolding euclidean_component_def by (rule inner_setsum_right)
13.37
13.38 lemma euclidean_eqI:
13.39 fixes x y :: "'a::euclidean_space"
13.40 assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
13.41 proof -
13.42 from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0"
13.43 - by (simp add: euclidean_component.diff)
13.44 + by (simp add: euclidean_component_diff)
13.45 then show "x = y"
13.46 unfolding euclidean_component_def euclidean_all_zero by simp
13.47 qed
13.48 @@ -153,23 +171,19 @@
13.49 assumes "i \<ge> DIM('a)" shows "x $$ i = 0"
13.50 unfolding euclidean_component_def basis_zero[OF assms] by simp
13.51
13.52 -lemma euclidean_scaleR:
13.53 - shows "(a *\<^sub>R x) $$ i = a * (x$$i)"
13.54 - unfolding euclidean_component_def by auto
13.55 -
13.56 lemmas euclidean_simps =
13.57 - euclidean_component.add
13.58 - euclidean_component.diff
13.59 - euclidean_scaleR
13.60 - euclidean_component.minus
13.61 - euclidean_component.setsum
13.62 + euclidean_component_add
13.63 + euclidean_component_diff
13.64 + euclidean_component_scaleR
13.65 + euclidean_component_minus
13.66 + euclidean_component_setsum
13.67 basis_component
13.68
13.69 lemma euclidean_representation:
13.70 fixes x :: "'a::euclidean_space"
13.71 shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)"
13.72 apply (rule euclidean_eqI)
13.73 - apply (simp add: euclidean_component.setsum euclidean_component.scaleR)
13.74 + apply (simp add: euclidean_component_setsum euclidean_component_scaleR)
13.75 apply (simp add: if_distrib setsum_delta cong: if_cong)
13.76 done
13.77
13.78 @@ -180,7 +194,7 @@
13.79
13.80 lemma euclidean_lambda_beta [simp]:
13.81 "((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)"
13.82 - by (auto simp: euclidean_component.setsum euclidean_component.scaleR
13.83 + by (auto simp: euclidean_component_setsum euclidean_component_scaleR
13.84 Chi_def if_distrib setsum_cases intro!: setsum_cong)
13.85
13.86 lemma euclidean_lambda_beta':
13.87 @@ -201,7 +215,7 @@
13.88 lemma euclidean_inner:
13.89 "inner x (y::'a) = (\<Sum>i<DIM('a::euclidean_space). (x $$ i) * (y $$ i))"
13.90 by (subst (1 2) euclidean_representation,
13.91 - simp add: inner_left.setsum inner_right.setsum
13.92 + simp add: inner_setsum_left inner_setsum_right
13.93 dot_basis if_distrib setsum_cases mult_commute)
13.94
13.95 lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"
14.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Aug 18 22:50:28 2011 +0200
14.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Aug 18 14:08:39 2011 -0700
14.3 @@ -66,7 +66,7 @@
14.4 apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
14.5 have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
14.6 thus "(0 < sqprojection x $ i) = (0 < x $ i)" "(sqprojection x $ i < 0) = (x $ i < 0)"
14.7 - unfolding sqprojection_def vector_component_simps vec_nth.scaleR real_scaleR_def
14.8 + unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
14.9 unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
14.10 note lem3 = this[rule_format]
14.11 have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto
15.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Aug 18 22:50:28 2011 +0200
15.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Aug 18 14:08:39 2011 -0700
15.3 @@ -401,14 +401,15 @@
15.4 unfolding norm_vec_def
15.5 by (rule member_le_setL2) simp_all
15.6
15.7 -interpretation vec_nth: bounded_linear "\<lambda>x. x $ i"
15.8 +lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
15.9 apply default
15.10 apply (rule vector_add_component)
15.11 apply (rule vector_scaleR_component)
15.12 apply (rule_tac x="1" in exI, simp add: norm_nth_le)
15.13 done
15.14
15.15 -declare vec_nth.isCont [simp]
15.16 +lemmas isCont_vec_nth [simp] =
15.17 + bounded_linear.isCont [OF bounded_linear_vec_nth]
15.18
15.19 instance vec :: (banach, finite) banach ..
15.20
16.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy Thu Aug 18 22:50:28 2011 +0200
16.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Thu Aug 18 14:08:39 2011 -0700
16.3 @@ -16,7 +16,7 @@
16.4
16.5 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
16.6 scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
16.7 - scaleR_cancel_left scaleR_cancel_right scaleR.add_right scaleR.add_left real_vector_class.scaleR_one
16.8 + scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
16.9
16.10 lemma real_arch_invD:
16.11 "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
16.12 @@ -1225,7 +1225,7 @@
16.13 lemma has_integral_cmul:
16.14 shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
16.15 unfolding o_def[THEN sym] apply(rule has_integral_linear,assumption)
16.16 - by(rule scaleR.bounded_linear_right)
16.17 + by(rule bounded_linear_scaleR_right)
16.18
16.19 lemma has_integral_neg:
16.20 shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
16.21 @@ -2262,7 +2262,7 @@
16.22 assumes "p tagged_division_of {a..b}" "\<forall>x\<in>{a..b}. norm(f x - g x) \<le> e"
16.23 shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - setsum (\<lambda>(x,k). content k *\<^sub>R g x) p) \<le> e * content({a..b})"
16.24 apply(rule order_trans[OF _ rsum_bound[OF assms]]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
16.25 - unfolding setsum_subtractf[THEN sym] apply(rule setsum_cong2) unfolding scaleR.diff_right by auto
16.26 + unfolding setsum_subtractf[THEN sym] apply(rule setsum_cong2) unfolding scaleR_diff_right by auto
16.27
16.28 lemma has_integral_bound: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
16.29 assumes "0 \<le> B" "(f has_integral i) ({a..b})" "\<forall>x\<in>{a..b}. norm(f x) \<le> B"
16.30 @@ -2287,7 +2287,7 @@
16.31 lemma rsum_component_le: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
16.32 assumes "p tagged_division_of {a..b}" "\<forall>x\<in>{a..b}. (f x)$$i \<le> (g x)$$i"
16.33 shows "(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p)$$i \<le> (setsum (\<lambda>(x,k). content k *\<^sub>R g x) p)$$i"
16.34 - unfolding euclidean_component.setsum apply(rule setsum_mono) apply safe
16.35 + unfolding euclidean_component_setsum apply(rule setsum_mono) apply safe
16.36 proof- fix a b assume ab:"(a,b) \<in> p" note assm = tagged_division_ofD(2-4)[OF assms(1) ab]
16.37 from this(3) guess u v apply-by(erule exE)+ note b=this
16.38 show "(content b *\<^sub>R f a) $$ i \<le> (content b *\<^sub>R g a) $$ i" unfolding b
16.39 @@ -2988,7 +2988,7 @@
16.40 have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
16.41 norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
16.42 apply(rule order_trans[OF _ norm_triangle_ineq4]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
16.43 - unfolding scaleR.diff_left by(auto simp add:algebra_simps)
16.44 + unfolding scaleR_diff_left by(auto simp add:algebra_simps)
16.45 also have "... \<le> e * norm (u - x) + e * norm (v - x)"
16.46 apply(rule add_mono) apply(rule d(2)[of "x" "u",unfolded o_def]) prefer 4
16.47 apply(rule d(2)[of "x" "v",unfolded o_def])
16.48 @@ -3123,7 +3123,7 @@
16.49 assumes "continuous_on {a..b} f" "x \<in> {a..b}"
16.50 shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b})"
16.51 unfolding has_vector_derivative_def has_derivative_within_alt
16.52 -apply safe apply(rule scaleR.bounded_linear_left)
16.53 +apply safe apply(rule bounded_linear_scaleR_left)
16.54 proof- fix e::real assume e:"e>0"
16.55 note compact_uniformly_continuous[OF assms(1) compact_interval,unfolded uniformly_continuous_on_def]
16.56 from this[rule_format,OF e] guess d apply-by(erule conjE exE)+ note d=this[rule_format]
16.57 @@ -3223,8 +3223,8 @@
16.58 have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _") unfolding algebra_simps add_left_cancel
16.59 unfolding setsum_reindex[OF *] apply(subst scaleR_right.setsum) defer apply(rule setsum_cong2) unfolding o_def split_paired_all split_conv
16.60 apply(drule p(4)) apply safe unfolding assms(7)[rule_format] using p by auto
16.61 - also have "... = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR.diff_right scaleR.scaleR_left[THEN sym]
16.62 - unfolding real_scaleR_def using assms(1) by auto finally have *:"?l = ?r" .
16.63 + also have "... = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR_diff_right scaleR_scaleR
16.64 + using assms(1) by auto finally have *:"?l = ?r" .
16.65 show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e" using ** unfolding * unfolding norm_scaleR
16.66 using assms(1) by(auto simp add:field_simps) qed qed qed
16.67
16.68 @@ -3256,7 +3256,7 @@
16.69 lemma has_integral_affinity: fixes a::"'a::ordered_euclidean_space" assumes "(f has_integral i) {a..b}" "m \<noteq> 0"
16.70 shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral ((1 / (abs(m) ^ DIM('a))) *\<^sub>R i)) ((\<lambda>x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` {a..b})"
16.71 apply(rule has_integral_twiddle,safe) apply(rule zero_less_power) unfolding euclidean_eq[where 'a='a]
16.72 - unfolding scaleR_right_distrib euclidean_simps scaleR.scaleR_left[THEN sym]
16.73 + unfolding scaleR_right_distrib euclidean_simps scaleR_scaleR
16.74 defer apply(insert assms(2), simp add:field_simps) apply(insert assms(2), simp add:field_simps)
16.75 apply(rule continuous_intros)+ apply(rule interval_image_affinity_interval)+ apply(rule content_image_affinity_interval) using assms by auto
16.76
16.77 @@ -3442,7 +3442,7 @@
16.78 show ?case unfolding content_real[OF assms(1)] and *[of "\<lambda>x. x"] *[of f] setsum_subtractf[THEN sym] split_minus
16.79 unfolding setsum_right_distrib apply(subst(2) pA,subst pA) unfolding setsum_Un_disjoint[OF pA(2-)]
16.80 proof(rule norm_triangle_le,rule **)
16.81 - case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst divide.setsum)
16.82 + case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst setsum_divide_distrib)
16.83 proof(rule order_refl,safe,unfold not_le o_def split_conv fst_conv,rule ccontr) fix x k assume as:"(x,k) \<in> p"
16.84 "e * (interval_upperbound k - interval_lowerbound k) / 2
16.85 < norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k)))"
16.86 @@ -4159,7 +4159,7 @@
16.87 "(\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R g x) \<ge> 0"
16.88 "0 \<le> (\<Sum>(x, k)\<in>p1. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x)"
16.89 unfolding setsum_subtractf[THEN sym] apply- apply(rule_tac[!] setsum_nonneg)
16.90 - apply safe unfolding real_scaleR_def mult.diff_right[THEN sym]
16.91 + apply safe unfolding real_scaleR_def right_diff_distrib[THEN sym]
16.92 apply(rule_tac[!] mult_nonneg_nonneg)
16.93 proof- fix a b assume ab:"(a,b) \<in> p1"
16.94 show "0 \<le> content b" using *(3)[OF ab] apply safe using content_pos_le . thus "0 \<le> content b" .
16.95 @@ -4535,7 +4535,7 @@
16.96 show ?case apply(rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content {a..b}))"])
16.97 unfolding setsum_subtractf[THEN sym] apply(rule order_trans,rule norm_setsum)
16.98 apply(rule setsum_mono) unfolding split_paired_all split_conv
16.99 - unfolding split_def setsum_left_distrib[THEN sym] scaleR.diff_right[THEN sym]
16.100 + unfolding split_def setsum_left_distrib[THEN sym] scaleR_diff_right[THEN sym]
16.101 unfolding additive_content_tagged_division[OF p(1), unfolded split_def]
16.102 proof- fix x k assume xk:"(x,k) \<in> p" hence x:"x\<in>{a..b}" using p'(2-3)[OF xk] by auto
16.103 from p'(4)[OF xk] guess u v apply-by(erule exE)+ note uv=this
16.104 @@ -5202,7 +5202,7 @@
16.105 proof- have *:"\<And>x. ((\<chi>\<chi> i. abs(f x$$i))::'c::ordered_euclidean_space) = (setsum (\<lambda>i.
16.106 (((\<lambda>y. (\<chi>\<chi> j. if j = i then y else 0)) o
16.107 (((\<lambda>x. (norm((\<chi>\<chi> j. if j = i then x$$i else 0)::'c::ordered_euclidean_space))) o f))) x)) {..<DIM('c)})"
16.108 - unfolding euclidean_eq[where 'a='c] euclidean_component.setsum apply safe
16.109 + unfolding euclidean_eq[where 'a='c] euclidean_component_setsum apply safe
16.110 unfolding euclidean_lambda_beta'
16.111 proof- case goal1 have *:"\<And>i xa. ((if i = xa then f x $$ xa else 0) * (if i = xa then f x $$ xa else 0)) =
16.112 (if i = xa then (f x $$ xa) * (f x $$ xa) else 0)" by auto
16.113 @@ -5220,7 +5220,7 @@
16.114 apply(rule absolutely_integrable_linear) unfolding o_def apply(rule absolutely_integrable_norm)
16.115 apply(rule absolutely_integrable_linear[OF assms,unfolded o_def]) unfolding linear_linear
16.116 apply(rule_tac[!] linearI) unfolding euclidean_eq[where 'a='c]
16.117 - by(auto simp:euclidean_scaleR[where 'a=real,unfolded real_scaleR_def])
16.118 + by(auto simp:euclidean_component_scaleR[where 'a=real,unfolded real_scaleR_def])
16.119 qed
16.120
16.121 lemma absolutely_integrable_max: fixes f g::"'m::ordered_euclidean_space \<Rightarrow> 'n::ordered_euclidean_space"
16.122 @@ -5266,7 +5266,7 @@
16.123 proof- fix k and i assume "k\<in>d" and i:"i<DIM('m)"
16.124 from d'(4)[OF this(1)] guess a b apply-by(erule exE)+ note ab=this
16.125 show "\<bar>integral k f $$ i\<bar> \<le> integral k (\<lambda>x. (\<chi>\<chi> j. \<bar>f x $$ j\<bar>)::'m) $$ i" apply(rule abs_leI)
16.126 - unfolding euclidean_component.minus[THEN sym] defer apply(subst integral_neg[THEN sym])
16.127 + unfolding euclidean_component_minus[THEN sym] defer apply(subst integral_neg[THEN sym])
16.128 defer apply(rule_tac[1-2] integral_component_le) apply(rule integrable_neg)
16.129 using integrable_on_subinterval[OF assms(1),of a b]
16.130 integrable_on_subinterval[OF assms(2),of a b] unfolding ab by auto
16.131 @@ -5276,7 +5276,7 @@
16.132 using integrable_on_subdivision[OF d assms(2)] by auto
16.133 have "(\<Sum>i\<in>d. integral i (\<lambda>x. (\<chi>\<chi> j. \<bar>f x $$ j\<bar>)::'m) $$ j)
16.134 = integral (\<Union>d) (\<lambda>x. (\<chi>\<chi> j. abs(f x$$j)) ::'m::ordered_euclidean_space) $$ j"
16.135 - unfolding euclidean_component.setsum[THEN sym] integral_combine_division_topdown[OF * d] ..
16.136 + unfolding euclidean_component_setsum[THEN sym] integral_combine_division_topdown[OF * d] ..
16.137 also have "... \<le> integral UNIV (\<lambda>x. (\<chi>\<chi> j. \<bar>f x $$ j\<bar>)::'m) $$ j"
16.138 apply(rule integral_subset_component_le) using assms * by auto
16.139 finally show ?case .
17.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Aug 18 22:50:28 2011 +0200
17.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Aug 18 14:08:39 2011 -0700
17.3 @@ -198,8 +198,8 @@
17.4
17.5 text{* Dot product in terms of the norm rather than conversely. *}
17.6
17.7 -lemmas inner_simps = inner.add_left inner.add_right inner.diff_right inner.diff_left
17.8 -inner.scaleR_left inner.scaleR_right
17.9 +lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
17.10 +inner_scaleR_left inner_scaleR_right
17.11
17.12 lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2"
17.13 unfolding power2_norm_eq_inner inner_simps inner_commute by auto
17.14 @@ -1558,7 +1558,7 @@
17.15 unfolding independent_eq_inj_on [OF basis_inj]
17.16 apply clarify
17.17 apply (drule_tac f="inner (basis a)" in arg_cong)
17.18 - apply (simp add: inner_right.setsum dot_basis)
17.19 + apply (simp add: inner_setsum_right dot_basis)
17.20 done
17.21
17.22 lemma dimensionI:
17.23 @@ -1663,10 +1663,10 @@
17.24 have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+
17.25 have Ppe:"setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp \<le> e"
17.26 using component_le_norm[of "setsum (\<lambda>x. f x) ?Pp" i] fPs[OF PpP]
17.27 - unfolding euclidean_component.setsum by(auto intro: abs_le_D1)
17.28 + unfolding euclidean_component_setsum by(auto intro: abs_le_D1)
17.29 have Pne: "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn \<le> e"
17.30 using component_le_norm[of "setsum (\<lambda>x. - f x) ?Pn" i] fPs[OF PnP]
17.31 - unfolding euclidean_component.setsum euclidean_component.minus
17.32 + unfolding euclidean_component_setsum euclidean_component_minus
17.33 by(auto simp add: setsum_negf intro: abs_le_D1)
17.34 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"
17.35 apply (subst thp)
17.36 @@ -1756,7 +1756,7 @@
17.37 have Kp: "?K > 0" by arith
17.38 { assume C: "B < 0"
17.39 have "((\<chi>\<chi> i. 1)::'a) \<noteq> 0" unfolding euclidean_eq[where 'a='a]
17.40 - by(auto intro!:exI[where x=0] simp add:euclidean_component.zero)
17.41 + by(auto intro!:exI[where x=0] simp add:euclidean_component_zero)
17.42 hence "norm ((\<chi>\<chi> i. 1)::'a) > 0" by auto
17.43 with C have "B * norm ((\<chi>\<chi> i. 1)::'a) < 0"
17.44 by (simp add: mult_less_0_iff)
17.45 @@ -2829,7 +2829,7 @@
17.46 unfolding infnorm_def
17.47 unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
17.48 unfolding infnorm_set_image ball_simps
17.49 - apply(subst (1) euclidean_eq) unfolding euclidean_component.zero
17.50 + apply(subst (1) euclidean_eq) unfolding euclidean_component_zero
17.51 by auto
17.52 then show ?thesis using infnorm_pos_le[of x] by simp
17.53 qed
17.54 @@ -2881,7 +2881,7 @@
17.55 lemma infnorm_mul_lemma: "infnorm(a *\<^sub>R x) <= \<bar>a\<bar> * infnorm x"
17.56 apply (subst infnorm_def)
17.57 unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
17.58 - unfolding infnorm_set_image ball_simps euclidean_scaleR abs_mult
17.59 + unfolding infnorm_set_image ball_simps euclidean_component_scaleR abs_mult
17.60 using component_le_infnorm[of x] by(auto intro: mult_mono)
17.61
17.62 lemma infnorm_mul: "infnorm(a *\<^sub>R x) = abs a * infnorm x"
18.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Aug 18 22:50:28 2011 +0200
18.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Aug 18 14:08:39 2011 -0700
18.3 @@ -14,7 +14,7 @@
18.4
18.5 lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
18.6 unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
18.7 - apply(auto simp add:power2_eq_square) unfolding euclidean_component.diff ..
18.8 + apply(auto simp add:power2_eq_square) unfolding euclidean_component_diff ..
18.9
18.10 lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
18.11 apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
18.12 @@ -1912,7 +1912,7 @@
18.13 fixes S :: "'a::real_normed_vector set"
18.14 shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)"
18.15 apply (rule bounded_linear_image, assumption)
18.16 - apply (rule scaleR.bounded_linear_right)
18.17 + apply (rule bounded_linear_scaleR_right)
18.18 done
18.19
18.20 lemma bounded_translation:
18.21 @@ -3537,7 +3537,7 @@
18.22 proof-
18.23 { fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
18.24 hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially"
18.25 - using scaleR.tendsto [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
18.26 + using tendsto_scaleR [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
18.27 unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
18.28 }
18.29 thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
18.30 @@ -4365,7 +4365,7 @@
18.31 assumes "compact s" shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
18.32 proof-
18.33 let ?f = "\<lambda>x. scaleR c x"
18.34 - have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right)
18.35 + have *:"bounded_linear ?f" by (rule bounded_linear_scaleR_right)
18.36 show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
18.37 using linear_continuous_at[OF *] assms by auto
18.38 qed
18.39 @@ -4951,7 +4951,7 @@
18.40 unfolding Lim_sequentially by(auto simp add: dist_norm)
18.41 hence "(f ---> x) sequentially" unfolding f_def
18.42 using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
18.43 - using scaleR.tendsto [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto }
18.44 + using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto }
18.45 ultimately have "x \<in> closure {a<..<b}"
18.46 using as and open_interval_midpoint[OF assms] unfolding closure_def unfolding islimpt_sequential by(cases "x=?c")auto }
18.47 thus ?thesis using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
18.48 @@ -5571,7 +5571,7 @@
18.49 subsection {* Some properties of a canonical subspace *}
18.50
18.51 (** move **)
18.52 -declare euclidean_component.zero[simp]
18.53 +declare euclidean_component_zero[simp]
18.54
18.55 lemma subspace_substandard:
18.56 "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
18.57 @@ -6027,15 +6027,15 @@
18.58
18.59 lemmas Lim_ident_at = LIM_ident
18.60 lemmas Lim_const = tendsto_const
18.61 -lemmas Lim_cmul = scaleR.tendsto [OF tendsto_const]
18.62 +lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const]
18.63 lemmas Lim_neg = tendsto_minus
18.64 lemmas Lim_add = tendsto_add
18.65 lemmas Lim_sub = tendsto_diff
18.66 -lemmas Lim_mul = scaleR.tendsto
18.67 -lemmas Lim_vmul = scaleR.tendsto [OF _ tendsto_const]
18.68 +lemmas Lim_mul = tendsto_scaleR
18.69 +lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const]
18.70 lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
18.71 lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
18.72 -lemmas Lim_component = euclidean_component.tendsto
18.73 +lemmas Lim_component = tendsto_euclidean_component
18.74 lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
18.75
18.76 end
19.1 --- a/src/HOL/Probability/Borel_Space.thy Thu Aug 18 22:50:28 2011 +0200
19.2 +++ b/src/HOL/Probability/Borel_Space.thy Thu Aug 18 14:08:39 2011 -0700
19.3 @@ -816,7 +816,7 @@
19.4 proof cases
19.5 assume "b \<noteq> 0"
19.6 with `open S` have "((\<lambda>x. (- a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open")
19.7 - by (auto intro!: open_affinity simp: scaleR.add_right mem_def)
19.8 + by (auto intro!: open_affinity simp: scaleR_add_right mem_def)
19.9 hence "?S \<in> sets borel"
19.10 unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic)
19.11 moreover
20.1 --- a/src/HOL/Probability/Independent_Family.thy Thu Aug 18 22:50:28 2011 +0200
20.2 +++ b/src/HOL/Probability/Independent_Family.thy Thu Aug 18 14:08:39 2011 -0700
20.3 @@ -563,7 +563,7 @@
20.4 with F have "(\<lambda>i. prob X * prob (F i)) sums prob (X \<inter> (\<Union>i. F i))"
20.5 by simp
20.6 moreover have "(\<lambda>i. prob X * prob (F i)) sums (prob X * prob (\<Union>i. F i))"
20.7 - by (intro mult_right.sums finite_measure_UNION F dis)
20.8 + by (intro sums_mult finite_measure_UNION F dis)
20.9 ultimately have "prob (X \<inter> (\<Union>i. F i)) = prob X * prob (\<Union>i. F i)"
20.10 by (auto dest!: sums_unique)
20.11 with F show "(\<Union>i. F i) \<in> sets ?D"
21.1 --- a/src/HOL/RealVector.thy Thu Aug 18 22:50:28 2011 +0200
21.2 +++ b/src/HOL/RealVector.thy Thu Aug 18 14:08:39 2011 -0700
21.3 @@ -62,24 +62,28 @@
21.4 and scale_minus_left [simp]: "scale (- a) x = - (scale a x)"
21.5 and scale_left_diff_distrib [algebra_simps]:
21.6 "scale (a - b) x = scale a x - scale b x"
21.7 + and scale_setsum_left: "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)"
21.8 proof -
21.9 interpret s: additive "\<lambda>a. scale a x"
21.10 proof qed (rule scale_left_distrib)
21.11 show "scale 0 x = 0" by (rule s.zero)
21.12 show "scale (- a) x = - (scale a x)" by (rule s.minus)
21.13 show "scale (a - b) x = scale a x - scale b x" by (rule s.diff)
21.14 + show "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)" by (rule s.setsum)
21.15 qed
21.16
21.17 lemma scale_zero_right [simp]: "scale a 0 = 0"
21.18 and scale_minus_right [simp]: "scale a (- x) = - (scale a x)"
21.19 and scale_right_diff_distrib [algebra_simps]:
21.20 "scale a (x - y) = scale a x - scale a y"
21.21 + and scale_setsum_right: "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))"
21.22 proof -
21.23 interpret s: additive "\<lambda>x. scale a x"
21.24 proof qed (rule scale_right_distrib)
21.25 show "scale a 0 = 0" by (rule s.zero)
21.26 show "scale a (- x) = - (scale a x)" by (rule s.minus)
21.27 show "scale a (x - y) = scale a x - scale a y" by (rule s.diff)
21.28 + show "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))" by (rule s.setsum)
21.29 qed
21.30
21.31 lemma scale_eq_0_iff [simp]:
21.32 @@ -140,16 +144,16 @@
21.33 end
21.34
21.35 class real_vector = scaleR + ab_group_add +
21.36 - assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
21.37 - and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
21.38 + assumes scaleR_add_right: "scaleR a (x + y) = scaleR a x + scaleR a y"
21.39 + and scaleR_add_left: "scaleR (a + b) x = scaleR a x + scaleR b x"
21.40 and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x"
21.41 and scaleR_one: "scaleR 1 x = x"
21.42
21.43 interpretation real_vector:
21.44 vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
21.45 apply unfold_locales
21.46 -apply (rule scaleR_right_distrib)
21.47 -apply (rule scaleR_left_distrib)
21.48 +apply (rule scaleR_add_right)
21.49 +apply (rule scaleR_add_left)
21.50 apply (rule scaleR_scaleR)
21.51 apply (rule scaleR_one)
21.52 done
21.53 @@ -159,16 +163,25 @@
21.54 lemmas scaleR_left_commute = real_vector.scale_left_commute
21.55 lemmas scaleR_zero_left = real_vector.scale_zero_left
21.56 lemmas scaleR_minus_left = real_vector.scale_minus_left
21.57 -lemmas scaleR_left_diff_distrib = real_vector.scale_left_diff_distrib
21.58 +lemmas scaleR_diff_left = real_vector.scale_left_diff_distrib
21.59 +lemmas scaleR_setsum_left = real_vector.scale_setsum_left
21.60 lemmas scaleR_zero_right = real_vector.scale_zero_right
21.61 lemmas scaleR_minus_right = real_vector.scale_minus_right
21.62 -lemmas scaleR_right_diff_distrib = real_vector.scale_right_diff_distrib
21.63 +lemmas scaleR_diff_right = real_vector.scale_right_diff_distrib
21.64 +lemmas scaleR_setsum_right = real_vector.scale_setsum_right
21.65 lemmas scaleR_eq_0_iff = real_vector.scale_eq_0_iff
21.66 lemmas scaleR_left_imp_eq = real_vector.scale_left_imp_eq
21.67 lemmas scaleR_right_imp_eq = real_vector.scale_right_imp_eq
21.68 lemmas scaleR_cancel_left = real_vector.scale_cancel_left
21.69 lemmas scaleR_cancel_right = real_vector.scale_cancel_right
21.70
21.71 +text {* Legacy names *}
21.72 +
21.73 +lemmas scaleR_left_distrib = scaleR_add_left
21.74 +lemmas scaleR_right_distrib = scaleR_add_right
21.75 +lemmas scaleR_left_diff_distrib = scaleR_diff_left
21.76 +lemmas scaleR_right_diff_distrib = scaleR_diff_right
21.77 +
21.78 lemma scaleR_minus1_left [simp]:
21.79 fixes x :: "'a::real_vector"
21.80 shows "scaleR (-1) x = - x"
21.81 @@ -1059,8 +1072,8 @@
21.82
21.83 end
21.84
21.85 -interpretation mult:
21.86 - bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
21.87 +lemma bounded_bilinear_mult:
21.88 + "bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
21.89 apply (rule bounded_bilinear.intro)
21.90 apply (rule left_distrib)
21.91 apply (rule right_distrib)
21.92 @@ -1070,19 +1083,21 @@
21.93 apply (simp add: norm_mult_ineq)
21.94 done
21.95
21.96 -interpretation mult_left:
21.97 - bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
21.98 -by (rule mult.bounded_linear_left)
21.99 +lemma bounded_linear_mult_left:
21.100 + "bounded_linear (\<lambda>x::'a::real_normed_algebra. x * y)"
21.101 + using bounded_bilinear_mult
21.102 + by (rule bounded_bilinear.bounded_linear_left)
21.103
21.104 -interpretation mult_right:
21.105 - bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
21.106 -by (rule mult.bounded_linear_right)
21.107 +lemma bounded_linear_mult_right:
21.108 + "bounded_linear (\<lambda>y::'a::real_normed_algebra. x * y)"
21.109 + using bounded_bilinear_mult
21.110 + by (rule bounded_bilinear.bounded_linear_right)
21.111
21.112 -interpretation divide:
21.113 - bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
21.114 -unfolding divide_inverse by (rule mult.bounded_linear_left)
21.115 +lemma bounded_linear_divide:
21.116 + "bounded_linear (\<lambda>x::'a::real_normed_field. x / y)"
21.117 + unfolding divide_inverse by (rule bounded_linear_mult_left)
21.118
21.119 -interpretation scaleR: bounded_bilinear "scaleR"
21.120 +lemma bounded_bilinear_scaleR: "bounded_bilinear scaleR"
21.121 apply (rule bounded_bilinear.intro)
21.122 apply (rule scaleR_left_distrib)
21.123 apply (rule scaleR_right_distrib)
21.124 @@ -1091,14 +1106,16 @@
21.125 apply (rule_tac x="1" in exI, simp)
21.126 done
21.127
21.128 -interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"
21.129 -by (rule scaleR.bounded_linear_left)
21.130 +lemma bounded_linear_scaleR_left: "bounded_linear (\<lambda>r. scaleR r x)"
21.131 + using bounded_bilinear_scaleR
21.132 + by (rule bounded_bilinear.bounded_linear_left)
21.133
21.134 -interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x"
21.135 -by (rule scaleR.bounded_linear_right)
21.136 +lemma bounded_linear_scaleR_right: "bounded_linear (\<lambda>x. scaleR r x)"
21.137 + using bounded_bilinear_scaleR
21.138 + by (rule bounded_bilinear.bounded_linear_right)
21.139
21.140 -interpretation of_real: bounded_linear "\<lambda>r. of_real r"
21.141 -unfolding of_real_def by (rule scaleR.bounded_linear_left)
21.142 +lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)"
21.143 + unfolding of_real_def by (rule bounded_linear_scaleR_left)
21.144
21.145 subsection{* Hausdorff and other separation properties *}
21.146
22.1 --- a/src/HOL/SEQ.thy Thu Aug 18 22:50:28 2011 +0200
22.2 +++ b/src/HOL/SEQ.thy Thu Aug 18 14:08:39 2011 -0700
22.3 @@ -377,7 +377,7 @@
22.4 lemma LIMSEQ_mult:
22.5 fixes a b :: "'a::real_normed_algebra"
22.6 shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
22.7 -by (rule mult.tendsto)
22.8 + by (rule tendsto_mult)
22.9
22.10 lemma increasing_LIMSEQ:
22.11 fixes f :: "nat \<Rightarrow> real"
23.1 --- a/src/HOL/Series.thy Thu Aug 18 22:50:28 2011 +0200
23.2 +++ b/src/HOL/Series.thy Thu Aug 18 14:08:39 2011 -0700
23.3 @@ -211,50 +211,54 @@
23.4 "summable (\<lambda>n. X n) \<Longrightarrow> f (\<Sum>n. X n) = (\<Sum>n. f (X n))"
23.5 by (intro sums_unique sums summable_sums)
23.6
23.7 +lemmas sums_of_real = bounded_linear.sums [OF bounded_linear_of_real]
23.8 +lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]
23.9 +lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]
23.10 +
23.11 lemma sums_mult:
23.12 fixes c :: "'a::real_normed_algebra"
23.13 shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)"
23.14 -by (rule mult_right.sums)
23.15 + by (rule bounded_linear.sums [OF bounded_linear_mult_right])
23.16
23.17 lemma summable_mult:
23.18 fixes c :: "'a::real_normed_algebra"
23.19 shows "summable f \<Longrightarrow> summable (%n. c * f n)"
23.20 -by (rule mult_right.summable)
23.21 + by (rule bounded_linear.summable [OF bounded_linear_mult_right])
23.22
23.23 lemma suminf_mult:
23.24 fixes c :: "'a::real_normed_algebra"
23.25 shows "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f"
23.26 -by (rule mult_right.suminf [symmetric])
23.27 + by (rule bounded_linear.suminf [OF bounded_linear_mult_right, symmetric])
23.28
23.29 lemma sums_mult2:
23.30 fixes c :: "'a::real_normed_algebra"
23.31 shows "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)"
23.32 -by (rule mult_left.sums)
23.33 + by (rule bounded_linear.sums [OF bounded_linear_mult_left])
23.34
23.35 lemma summable_mult2:
23.36 fixes c :: "'a::real_normed_algebra"
23.37 shows "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)"
23.38 -by (rule mult_left.summable)
23.39 + by (rule bounded_linear.summable [OF bounded_linear_mult_left])
23.40
23.41 lemma suminf_mult2:
23.42 fixes c :: "'a::real_normed_algebra"
23.43 shows "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)"
23.44 -by (rule mult_left.suminf)
23.45 + by (rule bounded_linear.suminf [OF bounded_linear_mult_left])
23.46
23.47 lemma sums_divide:
23.48 fixes c :: "'a::real_normed_field"
23.49 shows "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)"
23.50 -by (rule divide.sums)
23.51 + by (rule bounded_linear.sums [OF bounded_linear_divide])
23.52
23.53 lemma summable_divide:
23.54 fixes c :: "'a::real_normed_field"
23.55 shows "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)"
23.56 -by (rule divide.summable)
23.57 + by (rule bounded_linear.summable [OF bounded_linear_divide])
23.58
23.59 lemma suminf_divide:
23.60 fixes c :: "'a::real_normed_field"
23.61 shows "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
23.62 -by (rule divide.suminf [symmetric])
23.63 + by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])
23.64
23.65 lemma sums_add:
23.66 fixes a b :: "'a::real_normed_field"
23.67 @@ -423,7 +427,7 @@
23.68 by auto
23.69 have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
23.70 by simp
23.71 - thus ?thesis using divide.sums [OF 2, of 2]
23.72 + thus ?thesis using sums_divide [OF 2, of 2]
23.73 by simp
23.74 qed
23.75
24.1 --- a/src/HOL/Transcendental.thy Thu Aug 18 22:50:28 2011 +0200
24.2 +++ b/src/HOL/Transcendental.thy Thu Aug 18 14:08:39 2011 -0700
24.3 @@ -971,7 +971,7 @@
24.4
24.5 lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
24.6 unfolding exp_def
24.7 -apply (subst of_real.suminf)
24.8 +apply (subst suminf_of_real)
24.9 apply (rule summable_exp_generic)
24.10 apply (simp add: scaleR_conv_of_real)
24.11 done