1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 18 17:42:35 2011 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 18 13:36:58 2011 -0700
1.3 @@ -18,7 +18,7 @@
1.4 (* ------------------------------------------------------------------------- *)
1.5
1.6 lemma linear_scaleR: "linear (%(x :: 'n::euclidean_space). scaleR c x)"
1.7 - by (metis linear_conv_bounded_linear scaleR.bounded_linear_right)
1.8 + by (metis linear_conv_bounded_linear bounded_linear_scaleR_right)
1.9
1.10 lemma injective_scaleR:
1.11 assumes "(c :: real) ~= 0"
1.12 @@ -128,7 +128,7 @@
1.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
1.14 have **:"finite d" apply(rule finite_subset[OF assms]) by fastsimp
1.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)"
1.16 - unfolding euclidean_component.setsum euclidean_scaleR basis_component *
1.17 + unfolding euclidean_component_setsum euclidean_component_scaleR basis_component *
1.18 apply(rule setsum_cong2) using assms by auto
1.19 show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto
1.20 qed
1.21 @@ -1175,7 +1175,7 @@
1.22 have u2:"u2 \<le> 1" unfolding obt2(3)[THEN sym] and not_le using obt2(2) by auto
1.23 have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
1.24 apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
1.25 - also have "\<dots> \<le> 1" unfolding mult.add_right[THEN sym] and as(3) using u1 u2 by auto
1.26 + also have "\<dots> \<le> 1" unfolding right_distrib[THEN sym] and as(3) using u1 u2 by auto
1.27 finally
1.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)
1.29 apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
1.30 @@ -2229,7 +2229,7 @@
1.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)
1.32 have "x : affine hull S" using assms hull_subset[of S] by auto
1.33 moreover have "1 / e + - ((1 - e) / e) = 1"
1.34 - using `e>0` mult_left.diff[of "1" "(1-e)" "1/e"] by auto
1.35 + using `e>0` left_diff_distrib[of "1" "(1-e)" "1/e"] by auto
1.36 ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x : affine hull S"
1.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)
1.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)"
1.39 @@ -2957,7 +2957,7 @@
1.40 thus ?thesis apply(rule_tac x="basis 0" in exI, rule_tac x=1 in exI)
1.41 using True using DIM_positive[where 'a='a] by auto
1.42 next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms]
1.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
1.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
1.45
1.46 subsection {* Now set-to-set for closed/compact sets. *}
1.47
1.48 @@ -3053,7 +3053,7 @@
1.49 apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
1.50 apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
1.51 apply(rule assms[unfolded convex_def, rule_format]) prefer 6
1.52 - by (auto intro: tendsto_intros)
1.53 + by (auto intro!: tendsto_intros)
1.54
1.55 lemma convex_interior:
1.56 fixes s :: "'a::real_normed_vector set"
1.57 @@ -3221,13 +3221,13 @@
1.58 ultimately have "z \<in> convex hull {v \<in> c. u v \<le> 0}" unfolding convex_hull_explicit mem_Collect_eq
1.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)
1.60 using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def
1.61 - by(auto simp add: setsum_negf mult_right.setsum[THEN sym])
1.62 + by(auto simp add: setsum_negf setsum_right_distrib[THEN sym])
1.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"
1.64 apply (rule) apply (rule mult_nonneg_nonneg) using * by auto
1.65 hence "z \<in> convex hull {v \<in> c. u v > 0}" unfolding convex_hull_explicit mem_Collect_eq
1.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)
1.67 using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def using *
1.68 - by(auto simp add: setsum_negf mult_right.setsum[THEN sym])
1.69 + by(auto simp add: setsum_negf setsum_right_distrib[THEN sym])
1.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
1.71 qed
1.72
1.73 @@ -4157,7 +4157,7 @@
1.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)}"
1.75 have *:"{basis i :: 'a | i. i<DIM('a)} = basis ` ?D" by auto
1.76 { fix i assume i:"i<DIM('a)" have "?a $$ i = inverse (2 * real DIM('a))"
1.77 - unfolding euclidean_component.setsum * and setsum_reindex[OF basis_inj] and o_def
1.78 + unfolding euclidean_component_setsum * and setsum_reindex[OF basis_inj] and o_def
1.79 apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real DIM('a)) else 0) ?D"]) apply(rule setsum_cong2)
1.80 defer apply(subst setsum_delta') unfolding euclidean_component_def using i by(auto simp add:dot_basis) }
1.81 note ** = this
1.82 @@ -4270,7 +4270,7 @@
1.83 { fix i assume "i:d" have "?a $$ i = inverse (2 * real (card d))"
1.84 unfolding * setsum_reindex[OF basis_inj_on, OF assms(2)] o_def
1.85 apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real (card d)) else 0) ?D"])
1.86 - unfolding euclidean_component.setsum
1.87 + unfolding euclidean_component_setsum
1.88 apply(rule setsum_cong2)
1.89 using `i:d` `finite d` setsum_delta'[of d i "(%k. inverse (2 * real (card d)))"] d1 assms(2)
1.90 by (auto simp add: Euclidean_Space.basis_component[of i])}
1.91 @@ -4678,7 +4678,7 @@
1.92 hence x1: "x1 : affine hull S" using e1_def hull_subset[of S] by auto
1.93 def x2 == "z+ e2 *\<^sub>R (z-x)"
1.94 hence x2: "x2 : affine hull S" using e2_def hull_subset[of S] by auto
1.95 - have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using divide.add[of e1 e2 "e1+e2"] e1_def e2_def by simp
1.96 + have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using add_divide_distrib[of e1 e2 "e1+e2"] e1_def e2_def by simp
1.97 hence "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2"
1.98 using x1_def x2_def apply (auto simp add: algebra_simps)
1.99 using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z] by auto