# HG changeset patch # User nipkow # Date 1512658130 -3600 # Node ID 9e5b05d54f9dc28c6c3b2da54067e9f429ee8b8c # Parent c7def8f836d09be51fdf5e705f9febaaa8a3abe9 canonical name diff -r c7def8f836d0 -r 9e5b05d54f9d src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Dec 07 11:14:32 2017 +0100 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Dec 07 15:48:50 2017 +0100 @@ -290,7 +290,7 @@ lemma component_le_norm_cart: "\x$i\ <= norm x" apply (simp add: norm_vec_def) - apply (rule member_le_setL2, simp_all) + apply (rule member_le_L2_set, simp_all) done lemma norm_bound_component_le_cart: "norm x <= e ==> \x$i\ <= e" @@ -300,7 +300,7 @@ by (metis component_le_norm_cart le_less_trans) lemma norm_le_l1_cart: "norm x <= sum(\i. \x$i\) UNIV" - by (simp add: norm_vec_def setL2_le_sum) + by (simp add: norm_vec_def L2_set_le_sum) lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x" unfolding scaleR_vec_def vector_scalar_mult_def by simp @@ -984,7 +984,7 @@ { fix n assume n: "\i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))" have "dist (f (r n)) l \ (\i\?d. dist (f (r n) $ i) (l $ i))" - unfolding dist_vec_def using zero_le_dist by (rule setL2_le_sum) + unfolding dist_vec_def using zero_le_dist by (rule L2_set_le_sum) also have "\ < (\i\?d. e / (real_of_nat (card ?d)))" by (rule sum_strict_mono) (simp_all add: n) finally have "dist (f (r n)) l < e" by simp diff -r c7def8f836d0 -r 9e5b05d54f9d src/HOL/Analysis/Connected.thy --- a/src/HOL/Analysis/Connected.thy Thu Dec 07 11:14:32 2017 +0100 +++ b/src/HOL/Analysis/Connected.thy Thu Dec 07 15:48:50 2017 +0100 @@ -2854,7 +2854,7 @@ lemma diameter_cbox: fixes a b::"'a::euclidean_space" shows "(\i \ Basis. a \ i \ b \ i) \ diameter (cbox a b) = dist a b" - by (force simp: diameter_def intro!: cSup_eq_maximum setL2_mono + by (force simp: diameter_def intro!: cSup_eq_maximum L2_set_mono simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm) subsection \Separation between points and sets\ @@ -5038,7 +5038,7 @@ text\But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\ lemma Euclidean_dist_upper: "i \ Basis \ dist (x \ i) (y \ i) \ dist x y" - by (metis (no_types) member_le_setL2 euclidean_dist_l2 finite_Basis) + by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis) text\But is the premise @{term \i \ Basis\} really necessary?\ lemma open_preimage_inner: @@ -5087,17 +5087,17 @@ proof clarify fix e::real assume "0 < e" - have *: "setL2 (\i. dist (f x \ i) (l \ i)) Basis < e" + have *: "L2_set (\i. dist (f x \ i) (l \ i)) Basis < e" if "\i\Basis. dist (f x \ i) (l \ i) < e / real DIM('b)" for x proof - - have "setL2 (\i. dist (f x \ i) (l \ i)) Basis \ sum (\i. dist (f x \ i) (l \ i)) Basis" - by (simp add: setL2_le_sum) + have "L2_set (\i. dist (f x \ i) (l \ i)) Basis \ sum (\i. dist (f x \ i) (l \ i)) Basis" + by (simp add: L2_set_le_sum) also have "... < DIM('b) * (e / real DIM('b))" apply (rule sum_bounded_above_strict) using that by auto also have "... = e" by (simp add: field_simps) - finally show "setL2 (\i. dist (f x \ i) (l \ i)) Basis < e" . + finally show "L2_set (\i. dist (f x \ i) (l \ i)) Basis < e" . qed have "\\<^sub>F x in F. \i\Basis. dist (f x \ i) (l \ i) < e / DIM('b)" apply (rule R') @@ -5516,7 +5516,7 @@ by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric]) then show ?thesis by (auto intro: real_sqrt_le_mono - simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def) + simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def) qed (auto simp: clamp_def) lemma clamp_continuous_at: diff -r c7def8f836d0 -r 9e5b05d54f9d src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Dec 07 11:14:32 2017 +0100 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Dec 07 15:48:50 2017 +0100 @@ -7262,7 +7262,7 @@ unfolding 2 apply clarsimp apply (subst euclidean_dist_l2) - apply (rule order_trans [OF setL2_le_sum]) + apply (rule order_trans [OF L2_set_le_sum]) apply (rule zero_le_dist) unfolding e' apply (rule sum_mono) diff -r c7def8f836d0 -r 9e5b05d54f9d src/HOL/Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Dec 07 11:14:32 2017 +0100 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Dec 07 15:48:50 2017 +0100 @@ -342,7 +342,7 @@ begin definition - "dist x y = setL2 (\i. dist (x$i) (y$i)) UNIV" + "dist x y = L2_set (\i. dist (x$i) (y$i)) UNIV" instance .. end @@ -364,19 +364,19 @@ begin lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \ dist x y" - unfolding dist_vec_def by (rule member_le_setL2) simp_all + unfolding dist_vec_def by (rule member_le_L2_set) simp_all instance proof fix x y :: "'a ^ 'b" show "dist x y = 0 \ x = y" unfolding dist_vec_def - by (simp add: setL2_eq_0_iff vec_eq_iff) + by (simp add: L2_set_eq_0_iff vec_eq_iff) next fix x y z :: "'a ^ 'b" show "dist x y \ dist x z + dist y z" unfolding dist_vec_def - apply (rule order_trans [OF _ setL2_triangle_ineq]) - apply (simp add: setL2_mono dist_triangle2) + apply (rule order_trans [OF _ L2_set_triangle_ineq]) + apply (simp add: L2_set_mono dist_triangle2) done next fix S :: "('a ^ 'b) set" @@ -407,13 +407,13 @@ define r where [abs_def]: "r i = e / sqrt (of_nat CARD('b))" for i :: 'b from \0 < e\ have r: "\i. 0 < r i" unfolding r_def by simp_all - from \0 < e\ have e: "e = setL2 r UNIV" - unfolding r_def by (simp add: setL2_constant) + from \0 < e\ have e: "e = L2_set r UNIV" + unfolding r_def by (simp add: L2_set_constant) define A where "A i = {y. dist (x $ i) y < r i}" for i have "\i. open (A i) \ x $ i \ A i" unfolding A_def by (simp add: open_ball r) moreover have "\y. (\i. y $ i \ A i) \ y \ S" - by (simp add: A_def S dist_vec_def e setL2_strict_mono dist_commute) + by (simp add: A_def S dist_vec_def e L2_set_strict_mono dist_commute) ultimately show "\A. (\i. open (A i) \ x $ i \ A i) \ (\y. (\i. y $ i \ A i) \ y \ S)" by metis qed @@ -447,10 +447,10 @@ { fix m n :: nat assume "M \ m" "M \ n" - have "dist (X m) (X n) = setL2 (\i. dist (X m $ i) (X n $ i)) UNIV" + have "dist (X m) (X n) = L2_set (\i. dist (X m $ i) (X n $ i)) UNIV" unfolding dist_vec_def .. also have "\ \ sum (\i. dist (X m $ i) (X n $ i)) UNIV" - by (rule setL2_le_sum [OF zero_le_dist]) + by (rule L2_set_le_sum [OF zero_le_dist]) also have "\ < sum (\i::'n. ?s) UNIV" by (rule sum_strict_mono, simp_all add: M \M \ m\ \M \ n\) also have "\ = r" @@ -480,7 +480,7 @@ instantiation vec :: (real_normed_vector, finite) real_normed_vector begin -definition "norm x = setL2 (\i. norm (x$i)) UNIV" +definition "norm x = L2_set (\i. norm (x$i)) UNIV" definition "sgn (x::'a^'b) = scaleR (inverse (norm x)) x" @@ -488,15 +488,15 @@ fix a :: real and x y :: "'a ^ 'b" show "norm x = 0 \ x = 0" unfolding norm_vec_def - by (simp add: setL2_eq_0_iff vec_eq_iff) + by (simp add: L2_set_eq_0_iff vec_eq_iff) show "norm (x + y) \ norm x + norm y" unfolding norm_vec_def - apply (rule order_trans [OF _ setL2_triangle_ineq]) - apply (simp add: setL2_mono norm_triangle_ineq) + apply (rule order_trans [OF _ L2_set_triangle_ineq]) + apply (simp add: L2_set_mono norm_triangle_ineq) done show "norm (scaleR a x) = \a\ * norm x" unfolding norm_vec_def - by (simp add: setL2_right_distrib) + by (simp add: L2_set_right_distrib) show "sgn x = scaleR (inverse (norm x)) x" by (rule sgn_vec_def) show "dist x y = norm (x - y)" @@ -508,7 +508,7 @@ lemma norm_nth_le: "norm (x $ i) \ norm x" unfolding norm_vec_def -by (rule member_le_setL2) simp_all +by (rule member_le_L2_set) simp_all lemma bounded_linear_vec_nth: "bounded_linear (\x. x $ i)" apply standard @@ -545,7 +545,7 @@ unfolding inner_vec_def by (simp add: vec_eq_iff sum_nonneg_eq_0_iff) show "norm x = sqrt (inner x x)" - unfolding inner_vec_def norm_vec_def setL2_def + unfolding inner_vec_def norm_vec_def L2_set_def by (simp add: power2_norm_eq_inner) qed diff -r c7def8f836d0 -r 9e5b05d54f9d src/HOL/Analysis/L2_Norm.thy --- a/src/HOL/Analysis/L2_Norm.thy Thu Dec 07 11:14:32 2017 +0100 +++ b/src/HOL/Analysis/L2_Norm.thy Thu Dec 07 15:48:50 2017 +0100 @@ -8,74 +8,73 @@ imports Complex_Main begin -definition - "setL2 f A = sqrt (\i\A. (f i)\<^sup>2)" +definition "L2_set f A = sqrt (\i\A. (f i)\<^sup>2)" -lemma setL2_cong: - "\A = B; \x. x \ B \ f x = g x\ \ setL2 f A = setL2 g B" - unfolding setL2_def by simp +lemma L2_set_cong: + "\A = B; \x. x \ B \ f x = g x\ \ L2_set f A = L2_set g B" + unfolding L2_set_def by simp -lemma strong_setL2_cong: - "\A = B; \x. x \ B =simp=> f x = g x\ \ setL2 f A = setL2 g B" - unfolding setL2_def simp_implies_def by simp +lemma strong_L2_set_cong: + "\A = B; \x. x \ B =simp=> f x = g x\ \ L2_set f A = L2_set g B" + unfolding L2_set_def simp_implies_def by simp -lemma setL2_infinite [simp]: "\ finite A \ setL2 f A = 0" - unfolding setL2_def by simp +lemma L2_set_infinite [simp]: "\ finite A \ L2_set f A = 0" + unfolding L2_set_def by simp + +lemma L2_set_empty [simp]: "L2_set f {} = 0" + unfolding L2_set_def by simp -lemma setL2_empty [simp]: "setL2 f {} = 0" - unfolding setL2_def by simp +lemma L2_set_insert [simp]: + "\finite F; a \ F\ \ + L2_set f (insert a F) = sqrt ((f a)\<^sup>2 + (L2_set f F)\<^sup>2)" + unfolding L2_set_def by (simp add: sum_nonneg) -lemma setL2_insert [simp]: - "\finite F; a \ F\ \ - setL2 f (insert a F) = sqrt ((f a)\<^sup>2 + (setL2 f F)\<^sup>2)" - unfolding setL2_def by (simp add: sum_nonneg) +lemma L2_set_nonneg [simp]: "0 \ L2_set f A" + unfolding L2_set_def by (simp add: sum_nonneg) -lemma setL2_nonneg [simp]: "0 \ setL2 f A" - unfolding setL2_def by (simp add: sum_nonneg) +lemma L2_set_0': "\a\A. f a = 0 \ L2_set f A = 0" + unfolding L2_set_def by simp -lemma setL2_0': "\a\A. f a = 0 \ setL2 f A = 0" - unfolding setL2_def by simp +lemma L2_set_constant: "L2_set (\x. y) A = sqrt (of_nat (card A)) * \y\" + unfolding L2_set_def by (simp add: real_sqrt_mult) -lemma setL2_constant: "setL2 (\x. y) A = sqrt (of_nat (card A)) * \y\" - unfolding setL2_def by (simp add: real_sqrt_mult) - -lemma setL2_mono: +lemma L2_set_mono: assumes "\i. i \ K \ f i \ g i" assumes "\i. i \ K \ 0 \ f i" - shows "setL2 f K \ setL2 g K" - unfolding setL2_def + shows "L2_set f K \ L2_set g K" + unfolding L2_set_def by (simp add: sum_nonneg sum_mono power_mono assms) -lemma setL2_strict_mono: +lemma L2_set_strict_mono: assumes "finite K" and "K \ {}" assumes "\i. i \ K \ f i < g i" assumes "\i. i \ K \ 0 \ f i" - shows "setL2 f K < setL2 g K" - unfolding setL2_def + shows "L2_set f K < L2_set g K" + unfolding L2_set_def by (simp add: sum_strict_mono power_strict_mono assms) -lemma setL2_right_distrib: - "0 \ r \ r * setL2 f A = setL2 (\x. r * f x) A" - unfolding setL2_def +lemma L2_set_right_distrib: + "0 \ r \ r * L2_set f A = L2_set (\x. r * f x) A" + unfolding L2_set_def apply (simp add: power_mult_distrib) apply (simp add: sum_distrib_left [symmetric]) apply (simp add: real_sqrt_mult sum_nonneg) done -lemma setL2_left_distrib: - "0 \ r \ setL2 f A * r = setL2 (\x. f x * r) A" - unfolding setL2_def +lemma L2_set_left_distrib: + "0 \ r \ L2_set f A * r = L2_set (\x. f x * r) A" + unfolding L2_set_def apply (simp add: power_mult_distrib) apply (simp add: sum_distrib_right [symmetric]) apply (simp add: real_sqrt_mult sum_nonneg) done -lemma setL2_eq_0_iff: "finite A \ setL2 f A = 0 \ (\x\A. f x = 0)" - unfolding setL2_def +lemma L2_set_eq_0_iff: "finite A \ L2_set f A = 0 \ (\x\A. f x = 0)" + unfolding L2_set_def by (simp add: sum_nonneg sum_nonneg_eq_0_iff) -lemma setL2_triangle_ineq: - shows "setL2 (\i. f i + g i) A \ setL2 f A + setL2 g A" +lemma L2_set_triangle_ineq: + shows "L2_set (\i. f i + g i) A \ L2_set f A + L2_set g A" proof (cases "finite A") case False thus ?thesis by simp @@ -87,12 +86,12 @@ show ?case by simp next case (insert x F) - hence "sqrt ((f x + g x)\<^sup>2 + (setL2 (\i. f i + g i) F)\<^sup>2) \ - sqrt ((f x + g x)\<^sup>2 + (setL2 f F + setL2 g F)\<^sup>2)" + hence "sqrt ((f x + g x)\<^sup>2 + (L2_set (\i. f i + g i) F)\<^sup>2) \ + sqrt ((f x + g x)\<^sup>2 + (L2_set f F + L2_set g F)\<^sup>2)" by (intro real_sqrt_le_mono add_left_mono power_mono insert - setL2_nonneg add_increasing zero_le_power2) + L2_set_nonneg add_increasing zero_le_power2) also have - "\ \ sqrt ((f x)\<^sup>2 + (setL2 f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (setL2 g F)\<^sup>2)" + "\ \ sqrt ((f x)\<^sup>2 + (L2_set f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (L2_set g F)\<^sup>2)" by (rule real_sqrt_sum_squares_triangle_ineq) finally show ?case using insert by simp @@ -106,8 +105,8 @@ apply simp done -lemma setL2_le_sum [rule_format]: - "(\i\A. 0 \ f i) \ setL2 f A \ sum f A" +lemma L2_set_le_sum [rule_format]: + "(\i\A. 0 \ f i) \ L2_set f A \ sum f A" apply (cases "finite A") apply (induct set: finite) apply simp @@ -124,7 +123,7 @@ apply simp done -lemma setL2_le_sum_abs: "setL2 f A \ (\i\A. \f i\)" +lemma L2_set_le_sum_abs: "L2_set f A \ (\i\A. \f i\)" apply (cases "finite A") apply (induct set: finite) apply simp @@ -134,7 +133,7 @@ apply simp done -lemma setL2_mult_ineq_lemma: +lemma L2_set_mult_ineq_lemma: fixes a b c d :: real shows "2 * (a * c) * (b * d) \ a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2" proof - @@ -147,7 +146,7 @@ by simp qed -lemma setL2_mult_ineq: "(\i\A. \f i\ * \g i\) \ setL2 f A * setL2 g A" +lemma L2_set_mult_ineq: "(\i\A. \f i\ * \g i\) \ L2_set f A * L2_set g A" apply (cases "finite A") apply (induct set: finite) apply simp @@ -160,12 +159,12 @@ apply (simp add: power_mult_distrib) apply (simp add: distrib_left distrib_right) apply (rule ord_le_eq_trans) - apply (rule setL2_mult_ineq_lemma) + apply (rule L2_set_mult_ineq_lemma) apply simp_all done -lemma member_le_setL2: "\finite A; i \ A\ \ f i \ setL2 f A" - unfolding setL2_def +lemma member_le_L2_set: "\finite A; i \ A\ \ f i \ L2_set f A" + unfolding L2_set_def by (auto intro!: member_le_sum real_le_rsqrt) end diff -r c7def8f836d0 -r 9e5b05d54f9d src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Dec 07 11:14:32 2017 +0100 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Dec 07 15:48:50 2017 +0100 @@ -1249,8 +1249,8 @@ lemma euclidean_dist_l2: fixes x y :: "'a :: euclidean_space" - shows "dist x y = setL2 (\i. dist (x \ i) (y \ i)) Basis" - unfolding dist_norm norm_eq_sqrt_inner setL2_def + shows "dist x y = L2_set (\i. dist (x \ i) (y \ i)) Basis" + unfolding dist_norm norm_eq_sqrt_inner L2_set_def by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left) lemma eventually_nhds_ball: "d > 0 \ eventually (\x. x \ ball z d) (nhds z)" @@ -1358,7 +1358,7 @@ fix y :: 'a assume *: "y \ box ?a ?b" have "dist x y = sqrt (\i\Basis. (dist (x \ i) (y \ i))\<^sup>2)" - unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) + unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2) also have "\ < sqrt (\(i::'a)\Basis. e^2 / real (DIM('a)))" proof (rule real_sqrt_less_mono, rule sum_strict_mono) fix i :: "'a" @@ -1460,7 +1460,7 @@ fix y :: 'a assume *: "y \ cbox ?a ?b" have "dist x y = sqrt (\i\Basis. (dist (x \ i) (y \ i))\<^sup>2)" - unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) + unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2) also have "\ < sqrt (\(i::'a)\Basis. e^2 / real (DIM('a)))" proof (rule real_sqrt_less_mono, rule sum_strict_mono) fix i :: "'a" @@ -4579,7 +4579,7 @@ have "dist (f (r n)) l \ (\i\Basis. dist (f (r n) \ i) (l \ i))" apply (subst euclidean_dist_l2) using zero_le_dist - apply (rule setL2_le_sum) + apply (rule L2_set_le_sum) done also have "\ < (\i\(Basis::'a set). e / (real_of_nat DIM('a)))" apply (rule sum_strict_mono)