# HG changeset patch # User wenzelm # Date 1348339122 -7200 # Node ID 8d68162b78266200030627adecc74c90c8404f56 # Parent 7faf67b411b4157604d4a7d3483cd3c83b51f189 tuned whitespace; diff -r 7faf67b411b4 -r 8d68162b7826 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Sep 22 20:37:47 2012 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Sep 22 20:38:42 2012 +0200 @@ -36,16 +36,16 @@ lemma mem_convex_alt: assumes "convex S" "x : S" "y : S" "u>=0" "v>=0" "u+v>0" shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) : S" - apply (subst mem_convex_2) + apply (subst mem_convex_2) using assms apply (auto simp add: algebra_simps zero_le_divide_iff) using add_divide_distrib[of u v "u+v"] apply auto done -lemma inj_on_image_mem_iff: "inj_on f B ==> (A <= B) ==> (f a : f`A) ==> (a : B) ==> (a : A)" +lemma inj_on_image_mem_iff: "inj_on f B ==> (A <= B) ==> (f a : f`A) ==> (a : B) ==> (a : A)" by (blast dest: inj_onD) lemma independent_injective_on_span_image: - assumes iS: "independent S" + assumes iS: "independent S" and lf: "linear f" and fi: "inj_on f (span S)" shows "independent (f ` S)" proof - @@ -65,10 +65,10 @@ lemma dim_image_eq: fixes f :: "'n::euclidean_space => 'm::euclidean_space" - assumes lf: "linear f" and fi: "inj_on f (span S)" + assumes lf: "linear f" and fi: "inj_on f (span S)" shows "dim (f ` S) = dim (S:: ('n::euclidean_space) set)" proof - - obtain B where B_def: "B<=S & independent B & S <= span B & card B = dim S" + obtain B where B_def: "B<=S & independent B & S <= span B & card B = dim S" using basis_exists[of S] by auto then have "span S = span B" using span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto @@ -90,20 +90,20 @@ also have "... <-> (!x : S. !y : S. f x - f y = 0 --> x - y = 0)" by simp also have "... <-> (!x : S. !y : S. f (x - y) = 0 --> x - y = 0)" by (simp add: linear_sub[OF lf]) - also have "... <-> (! x : S. f x = 0 --> x = 0)" + also have "... <-> (! x : S. f x = 0 --> x = 0)" using `subspace S` subspace_def[of S] subspace_sub[of S] by auto finally show ?thesis . qed lemma subspace_Inter: "(!s : f. subspace s) ==> subspace (Inter f)" - unfolding subspace_def by auto + unfolding subspace_def by auto lemma span_eq[simp]: "(span s = s) <-> subspace s" unfolding span_def by (rule hull_eq, rule subspace_Inter) lemma basis_inj_on: "d \ {.. inj_on (basis :: nat => 'n::euclidean_space) d" by (auto simp add: inj_on_def euclidean_eq[where 'a='n]) - + lemma finite_substdbasis: "finite {basis i ::'n::euclidean_space |i. i : (d:: nat set)}" (is "finite ?S") proof - have eq: "?S = basis ` d" by blast @@ -152,7 +152,7 @@ done qed -lemma dim_cball: +lemma dim_cball: assumes "0R y" by auto ultimately have "x : span (cball 0 e)" using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"] by auto - } then have "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)" by auto + } then have "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)" by auto then show ?thesis using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp add: dim_UNIV) qed @@ -171,13 +171,13 @@ lemma indep_card_eq_dim_span: fixes B :: "('n::euclidean_space) set" assumes "independent B" - shows "finite B & card B = dim (span B)" + shows "finite B & card B = dim (span B)" using assms basis_card_eq_dim[of B "span B"] span_inc by auto lemma setsum_not_0: "setsum f A ~= 0 ==> EX a:A. f a ~= 0" by (rule ccontr) auto -lemma translate_inj_on: +lemma translate_inj_on: fixes A :: "('a::ab_group_add) set" shows "inj_on (%x. a+x) A" unfolding inj_on_def by auto @@ -206,7 +206,7 @@ done lemma translation_inverse_subset: - assumes "((%x. -a+x) ` V) <= (S :: 'n::ab_group_add set)" + assumes "((%x. -a+x) ` V) <= (S :: 'n::ab_group_add set)" shows "V <= ((%x. a+x) ` S)" proof - { fix x @@ -394,7 +394,7 @@ unfolding affine_def by auto lemma affine_Inter: "(\s\f. affine s) \ affine (\ f)" - unfolding affine_def by auto + unfolding affine_def by auto lemma affine_Int: "affine s \ affine t \ affine (s \ t)" unfolding affine_def by auto @@ -416,7 +416,7 @@ unfolding affine_def apply rule apply(rule, rule, rule) - apply(erule conjE)+ + apply(erule conjE)+ defer apply (rule, rule, rule, rule, rule) proof - @@ -480,9 +480,9 @@ case True then have "s - {x} \ {}" "card (s - {x}) = n" unfolding c and as(1)[symmetric] - proof (rule_tac ccontr) + proof (rule_tac ccontr) assume "\ s - {x} \ {}" - then have "card (s - {x}) = 0" unfolding card_0_eq[OF *(2)] by simp + then have "card (s - {x}) = 0" unfolding card_0_eq[OF *(2)] by simp then show False using True by auto qed auto then show ?thesis @@ -640,12 +640,12 @@ then show ?thesis apply (rule_tac x="\x. (if x=a then v else 0) + u x" in exI) unfolding setsum_clauses(2)[OF `?as`] apply simp - unfolding scaleR_left_distrib and setsum_addf + unfolding scaleR_left_distrib and setsum_addf unfolding vu and * and scaleR_zero_left apply (auto simp add: setsum_delta[OF `?as`]) done next - case False + case False then have **: "\x. x \ s \ u x = (if x = a then v else u x)" "\x. x \ s \ u x *\<^sub>R x = (if x = a then v *\<^sub>R x else u x *\<^sub>R x)" by auto @@ -666,7 +666,7 @@ shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs") proof - have *: - "\x y z. z = x - y \ y + z = (x::real)" + "\x y z. z = x - y \ y + z = (x::real)" "\x y z. z = x - y \ y + z = (x::'a)" by auto have "?lhs = {y. \u. setsum u {a, b} = 1 \ (\v\{a, b}. u v *\<^sub>R v) = y}" using affine_hull_finite[of "{a,b}"] by auto @@ -681,7 +681,7 @@ shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs") proof - have *: - "\x y z. z = x - y \ y + z = (x::real)" + "\x y z. z = x - y \ y + z = (x::real)" "\x y z. z = x - y \ y + z = (x::'a)" by auto show ?thesis apply (simp add: affine_hull_finite affine_hull_finite_step) @@ -708,7 +708,7 @@ using hull_mono[of "{x, y, z}" "S"] assms by auto moreover have "affine hull S = S" using assms affine_hull_eq[of S] by auto - ultimately show ?thesis by auto + ultimately show ?thesis by auto qed lemma mem_affine_3_minus: @@ -750,7 +750,7 @@ unfolding subset_eq Ball_def unfolding affine_hull_explicit and mem_Collect_eq proof (rule, rule, erule exE, erule conjE) - fix y v + fix y v assume "y = a + v" "v \ span {x - a |x. x \ s}" then obtain t u where obt:"finite t" "t \ {x - a |x. x \ s}" "a + (\v\t. u v *\<^sub>R v) = y" unfolding span_explicit by auto @@ -780,7 +780,7 @@ lemma affine_parallel_expl_aux: fixes S T :: "'a::real_vector set" - assumes "!x. (x : S <-> (a+x) : T)" + assumes "!x. (x : S <-> (a+x) : T)" shows "T = ((%x. a + x) ` S)" proof - { fix x @@ -788,7 +788,7 @@ then have "(-a)+x : S" using assms by auto then have "x : ((%x. a + x) ` S)" using imageI[of "-a+x" S "(%x. a+x)"] by auto } - moreover have "T >= ((%x. a + x) ` S)" using assms by auto + moreover have "T >= ((%x. a + x) ` S)" using assms by auto ultimately show ?thesis by auto qed @@ -811,11 +811,11 @@ lemma affine_parallel_assoc: assumes "affine_parallel A B" "affine_parallel B C" - shows "affine_parallel A C" + shows "affine_parallel A C" proof - from assms obtain ab where "B=((%x. ab + x) ` A)" - unfolding affine_parallel_def by auto - moreover + unfolding affine_parallel_def by auto + moreover from assms obtain bc where "C=((%x. bc + x) ` B)" unfolding affine_parallel_def by auto ultimately show ?thesis @@ -856,7 +856,7 @@ shows "affine T" proof - from assms obtain a where "T=((%x. a + x) ` S)" - unfolding affine_parallel_def by auto + unfolding affine_parallel_def by auto then show ?thesis using affine_translation assms by auto qed @@ -871,7 +871,7 @@ have h0: "subspace S ==> (affine S & 0 : S)" using subspace_imp_affine[of S] subspace_0 by auto { assume assm: "affine S & 0 : S" - { fix c :: real + { fix c :: real fix x assume x_def: "x : S" have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto moreover @@ -894,7 +894,7 @@ ultimately have "(x+y) : S" using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto } - then have "!x : S. !y : S. (x+y) : S" by auto + then have "!x : S. !y : S. (x+y) : S" by auto then have "subspace S" using h1 assm unfolding subspace_def by auto } then show ?thesis using h0 by metis @@ -905,25 +905,25 @@ shows "subspace ((%x. (-a)+x) ` S)" proof - have "affine ((%x. (-a)+x) ` S)" - using affine_translation assms by auto + using affine_translation assms by auto moreover have "0 : ((%x. (-a)+x) ` S)" using assms exI[of "(%x. x:S & -a+x=0)" a] by auto - ultimately show ?thesis using subspace_affine by auto + ultimately show ?thesis using subspace_affine by auto qed lemma parallel_subspace_explicit: assumes "affine S" "a : S" - assumes "L == {y. ? x : S. (-a)+x=y}" - shows "subspace L & affine_parallel S L" + assumes "L == {y. ? x : S. (-a)+x=y}" + shows "subspace L & affine_parallel S L" proof - have par: "affine_parallel S L" unfolding affine_parallel_def using assms by auto - then have "affine L" using assms parallel_is_affine by auto + then have "affine L" using assms parallel_is_affine by auto moreover have "0 : L" using assms apply auto using exI[of "(%x. x:S & -a+x=0)" a] apply auto done - ultimately show ?thesis using subspace_affine par by auto + ultimately show ?thesis using subspace_affine par by auto qed lemma parallel_subspace_aux: @@ -949,10 +949,10 @@ lemma affine_parallel_subspace: assumes "affine S" "S ~= {}" - shows "?!L. subspace L & affine_parallel S L" + shows "?!L. subspace L & affine_parallel S L" proof - have ex: "? L. subspace L & affine_parallel S L" - using assms parallel_subspace_explicit by auto + using assms parallel_subspace_explicit by auto { fix L1 L2 assume ass: "subspace L1 & affine_parallel S L1" "subspace L2 & affine_parallel S L2" then have "affine_parallel L1 L2" @@ -1084,7 +1084,7 @@ { fix x assume "x : S" then have "1 *\<^sub>R x : ?rhs" - apply auto + apply auto apply (rule_tac x="1" in exI) apply auto done @@ -1253,7 +1253,7 @@ fixes s :: "'a::real_normed_vector set" assumes "convex s" shows "connected s" proof- - { fix e1 e2 assume as:"open e1" "open e2" "e1 \ e2 \ s = {}" "s \ e1 \ e2" + { fix e1 e2 assume as:"open e1" "open e2" "e1 \ e2 \ s = {}" "s \ e1 \ e2" assume "e1 \ s \ {}" "e2 \ s \ {}" then obtain x1 x2 where x1:"x1\e1" "x1\s" and x2:"x2\e2" "x2\s" by auto hence n:"norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto @@ -1277,7 +1277,7 @@ using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2 using as(3) by auto then obtain x where "x\0" "x\1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e2" by auto - hence False using as(4) + hence False using as(4) using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1(2) x2(2) by auto } thus ?thesis unfolding connected_def by auto @@ -1322,7 +1322,7 @@ lemma convex_ball: fixes x :: "'a::real_normed_vector" - shows "convex (ball x e)" + shows "convex (ball x e)" proof(auto simp add: convex_def) fix y z assume yz:"dist x y < e" "dist x z < e" fix u v ::real assume uv:"0 \ u" "0 \ v" "u + v = 1" @@ -1339,7 +1339,7 @@ fix u v ::real assume uv:" 0 \ u" "0 \ v" "u + v = 1" have "dist x (u *\<^sub>R y + v *\<^sub>R z) \ u * dist x y + v * dist x z" using uv yz using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto - thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \ e" using convex_bound_le[OF yz uv] by auto + thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \ e" using convex_bound_le[OF yz uv] by auto qed lemma connected_ball: @@ -1379,15 +1379,15 @@ lemma convex_hull_linear_image: assumes "bounded_linear f" shows "f ` (convex hull s) = convex hull (f ` s)" - apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3 + apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3 apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption proof- interpret f: bounded_linear f by fact - show "convex {x. f x \ convex hull f ` s}" + show "convex {x. f x \ convex hull f ` s}" unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next interpret f: bounded_linear f by fact - show "convex {x. x \ f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s] + show "convex {x. x \ f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s] unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric]) qed auto @@ -1411,7 +1411,7 @@ b \ (convex hull s) \ (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull") apply(rule,rule hull_minimal,rule) unfolding insert_iff prefer 3 apply rule proof- fix x assume x:"x = a \ x \ s" - thus "x\?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer + thus "x\?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto next fix x assume "x\?hull" @@ -1435,11 +1435,11 @@ thus ?thesis unfolding obt1(5) obt2(5) * using assms hull_subset[of s convex] by(auto simp add: ** scaleR_right_distrib) next have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) - also have "\ = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) + also have "\ = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) also have "\ = u * v1 + v * v2" by simp finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto case False have "0 \ u * v1 + v * v2" "0 \ u * v1" "0 \ u * v1 + v * v2" "0 \ v * v2" apply - apply(rule add_nonneg_nonneg) prefer 4 apply(rule add_nonneg_nonneg) apply(rule_tac [!] mult_nonneg_nonneg) - using as(1,2) obt1(1,2) obt2(1,2) by auto + using as(1,2) obt1(1,2) obt2(1,2) by auto thus ?thesis unfolding obt1(5) obt2(5) unfolding * and ** using False apply(rule_tac x="((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) defer apply(rule convex_convex_hull[of s, unfolded convex_def, rule_format]) using obt1(4) obt2(4) @@ -1451,7 +1451,7 @@ have "u1 * u + u2 * v \ (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono) apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto also have "\ \ 1" unfolding right_distrib[symmetric] and as(3) using u1 u2 by auto - finally + finally show "u *\<^sub>R x + v *\<^sub>R y \ ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI) apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def using as(1,2) obt1(1,2) obt2(1,2) * by(auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps) @@ -1484,7 +1484,7 @@ have *:"\P (x1::'a) x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)" "{1..k1 + k2} \ {1..k1} = {1..k1}" "{1..k1 + k2} \ - {1..k1} = (\i. i + k1) ` {1..k2}" prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x - k1" in bexI) by(auto simp add: not_le) - have inj:"inj_on (\i. i + k1) {1..k2}" unfolding inj_on_def by auto + have inj:"inj_on (\i. i + k1) {1..k2}" unfolding inj_on_def by auto show "u *\<^sub>R x + v *\<^sub>R y \ ?hull" apply(rule) apply(rule_tac x="k1 + k2" in exI, rule_tac x="\i. if i \ {1..k1} then u * u1 i else v * u2 (i - k1)" in exI) apply(rule_tac x="\i. if i \ {1..k1} then x1 i else x2 (i - k1)" in exI) apply(rule,rule) defer apply(rule) @@ -1507,9 +1507,9 @@ shows "convex hull s = {y. \u. (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set") proof(rule hull_unique, auto simp add: convex_def[of ?set]) - fix x assume "x\s" thus " \u. (\x\s. 0 \ u x) \ setsum u s = 1 \ (\x\s. u x *\<^sub>R x) = x" + fix x assume "x\s" thus " \u. (\x\s. 0 \ u x) \ setsum u s = 1 \ (\x\s. u x *\<^sub>R x) = x" apply(rule_tac x="\y. if x=y then 1 else 0" in exI) apply auto - unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto + unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto next fix u v ::real assume uv:"0 \ u" "0 \ v" "u + v = 1" fix ux assume ux:"\x\s. 0 \ ux x" "setsum ux s = (1::real)" @@ -1522,9 +1522,9 @@ moreover have "(\x\s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\x\s. ux x *\<^sub>R x) + v *\<^sub>R (\x\s. uy x *\<^sub>R x)" unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[symmetric] and scaleR_right.setsum [symmetric] by auto ultimately show "\uc. (\x\s. 0 \ uc x) \ setsum uc s = 1 \ (\x\s. uc x *\<^sub>R x) = u *\<^sub>R (\x\s. ux x *\<^sub>R x) + v *\<^sub>R (\x\s. uy x *\<^sub>R x)" - apply(rule_tac x="\x. u * ux x + v * uy x" in exI) by auto + apply(rule_tac x="\x. u * ux x + v * uy x" in exI) by auto next - fix t assume t:"s \ t" "convex t" + fix t assume t:"s \ t" "convex t" fix u assume u:"\x\s. 0 \ u x" "setsum u s = (1::real)" thus "(\x\s. u x *\<^sub>R x) \ t" using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]] using assms and t(1) by auto @@ -1554,9 +1554,9 @@ { fix j assume "j\{1..k}" hence "y j \ p" "0 \ setsum u {i. Suc 0 \ i \ i \ k \ y i = y j}" using obt(1)[THEN bspec[where x=j]] and obt(2) apply simp - apply(rule setsum_nonneg) using obt(1) by auto } + apply(rule setsum_nonneg) using obt(1) by auto } moreover - have "(\v\y ` {1..k}. setsum u {i \ {1..k}. y i = v}) = 1" + have "(\v\y ` {1..k}. setsum u {i \ {1..k}. y i = v}) = 1" unfolding setsum_image_gen[OF fin, symmetric] using obt(2) by auto moreover have "(\v\y ` {1..k}. setsum u {i \ {1..k}. y i = v} *\<^sub>R v) = x" using setsum_image_gen[OF fin, of "\i. u i *\<^sub>R y i" y, symmetric] @@ -1570,7 +1570,7 @@ then obtain s u where obt:"finite s" "s \ p" "\x\s. 0 \ u x" "setsum u s = 1" "(\v\s. u v *\<^sub>R v) = y" by auto obtain f where f:"inj_on f {1..card s}" "f ` {1..card s} = s" using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto - + { fix i::nat assume "i\{1..card s}" hence "f i \ s" apply(subst f(2)[symmetric]) by auto hence "0 \ u (f i)" "f i \ p" using obt(2,3) by auto } @@ -1584,10 +1584,10 @@ by (auto simp add: setsum_constant_scaleR) } hence "(\x = 1..card s. u (f x)) = 1" "(\i = 1..card s. u (f i) *\<^sub>R f i) = y" - unfolding setsum_image_gen[OF *(1), of "\x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\x. u (f x)" f] + unfolding setsum_image_gen[OF *(1), of "\x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\x. u (f x)" f] unfolding f using setsum_cong2[of s "\y. (\x\{x \ {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\v. u v *\<^sub>R v"] using setsum_cong2 [of s "\y. (\x\{x \ {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto - + ultimately have "\k u x. (\i\{1..k}. 0 \ u i \ x i \ p) \ setsum u {1..k} = 1 \ (\i::nat = 1..k. u i *\<^sub>R x i) = y" apply(rule_tac x="card s" in exI) apply(rule_tac x="u \ f" in exI) apply(rule_tac x=f in exI) by fastforce hence "y \ ?lhs" unfolding convex_hull_indexed by auto } @@ -1672,22 +1672,22 @@ lemma affine_dependent_imp_dependent: shows "affine_dependent s \ dependent s" - unfolding affine_dependent_def dependent_def + unfolding affine_dependent_def dependent_def using affine_hull_subset_span by auto lemma dependent_imp_affine_dependent: assumes "dependent {x - a| x . x \ s}" "a \ s" shows "affine_dependent (insert a s)" proof- - from assms(1)[unfolded dependent_explicit] obtain S u v + from assms(1)[unfolded dependent_explicit] obtain S u v where obt:"finite S" "S \ {x - a |x. x \ s}" "v\S" "u v \ 0" "(\v\S. u v *\<^sub>R v) = 0" by auto def t \ "(\x. x + a) ` S" have inj:"inj_on (\x. x + a) S" unfolding inj_on_def by auto have "0\S" using obt(2) assms(2) unfolding subset_eq by auto - have fin:"finite t" and "t\s" unfolding t_def using obt(1,2) by auto - - hence "finite (insert a t)" and "insert a t \ insert a s" by auto + have fin:"finite t" and "t\s" unfolding t_def using obt(1,2) by auto + + hence "finite (insert a t)" and "insert a t \ insert a s" by auto moreover have *:"\P Q. (\x\t. (if x = a then P x else Q x)) = (\x\t. Q x)" apply(rule setsum_cong2) using `a\s` `t\s` by auto have "(\x\insert a t. if x = a then - (\x\t. u (x - a)) else u (x - a)) = 0" @@ -1696,13 +1696,13 @@ apply(rule_tac x="v + a" in bexI) using obt(3,4) and `0\S` unfolding t_def by auto moreover have *:"\P Q. (\x\t. (if x = a then P x else Q x) *\<^sub>R x) = (\x\t. Q x *\<^sub>R x)" apply(rule setsum_cong2) using `a\s` `t\s` by auto - have "(\x\t. u (x - a)) *\<^sub>R a = (\v\t. u (v - a) *\<^sub>R v)" + have "(\x\t. u (x - a)) *\<^sub>R a = (\v\t. u (v - a) *\<^sub>R v)" unfolding scaleR_left.setsum unfolding t_def and setsum_reindex[OF inj] and o_def using obt(5) by (auto simp add: setsum_addf scaleR_right_distrib) hence "(\v\insert a t. (if v = a then - (\x\t. u (x - a)) else u (v - a)) *\<^sub>R v) = 0" unfolding setsum_clauses(2)[OF fin] using `a\s` `t\s` by (auto simp add: *) ultimately show ?thesis unfolding affine_dependent_explicit - apply(rule_tac x="insert a t" in exI) by auto + apply(rule_tac x="insert a t" in exI) by auto qed lemma convex_cone: @@ -1722,7 +1722,7 @@ proof- have "s\{}" using assms by auto then obtain a where "a\s" by auto have *:"{x - a |x. x \ s - {a}} = (\x. x - a) ` (s - {a})" by auto - have "card {x - a |x. x \ s - {a}} = card (s - {a})" unfolding * + have "card {x - a |x. x \ s - {a}} = card (s - {a})" unfolding * apply(rule card_image) unfolding inj_on_def by auto also have "\ > DIM('a)" using assms(2) unfolding card_Diff_singleton[OF assms(1) `a\s`] by auto @@ -1737,7 +1737,7 @@ from assms(2) have "s \ {}" by auto then obtain a where "a\s" by auto have *:"{x - a |x. x \ s - {a}} = (\x. x - a) ` (s - {a})" by auto - have **:"card {x - a |x. x \ s - {a}} = card (s - {a})" unfolding * + have **:"card {x - a |x. x \ s - {a}} = card (s - {a})" unfolding * apply(rule card_image) unfolding inj_on_def by auto have "dim {x - a |x. x \ s - {a}} \ dim s" apply(rule subset_le_dim) unfolding subset_eq @@ -1777,14 +1777,14 @@ qed hence "i\{}" unfolding i_def by auto hence "t \ 0" using Min_ge_iff[of i 0 ] and obt(1) unfolding t_def i_def - using obt(4)[unfolded le_less] apply auto unfolding divide_le_0_iff by auto + using obt(4)[unfolded le_less] apply auto unfolding divide_le_0_iff by auto have t:"\v\s. u v + t * w v \ 0" proof fix v assume "v\s" hence v:"0\u v" using obt(4)[THEN bspec[where x=v]] by auto show"0 \ u v + t * w v" proof(cases "w v < 0") - case False thus ?thesis apply(rule_tac add_nonneg_nonneg) + case False thus ?thesis apply(rule_tac add_nonneg_nonneg) using v apply simp apply(rule mult_nonneg_nonneg) using `t\0` by auto next case True hence "t \ u v / (- w v)" using `v\s` - unfolding t_def i_def apply(rule_tac Min_le) using obt(1) by auto + unfolding t_def i_def apply(rule_tac Min_le) using obt(1) by auto thus ?thesis unfolding real_0_le_add_iff using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[symmetric]]] by auto qed qed @@ -1793,10 +1793,10 @@ using Min_in[OF _ `i\{}`] and obt(1) unfolding i_def t_def by auto hence a:"a\s" "u a + t * w a = 0" by auto have *:"\f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)" - unfolding setsum_diff1'[OF obt(1) `a\s`] by auto + unfolding setsum_diff1'[OF obt(1) `a\s`] by auto have "(\v\s. u v + t * w v) = 1" unfolding setsum_addf wv(1) setsum_right_distrib[symmetric] obt(5) by auto - moreover have "(\v\s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y" + moreover have "(\v\s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y" unfolding setsum_addf obt(6) scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] wv(4) using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp ultimately have "?P (n - 1)" apply(rule_tac x="(s - {a})" in exI) @@ -1840,7 +1840,7 @@ moreover have "(%x. a + x) ` S <= (%x. a + x) ` (affine hull S)" using hull_subset[of S] by auto ultimately have h1: "affine hull ((%x. a + x) ` S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal) have "affine((%x. -a + x) ` (affine hull ((%x. a + x) ` S)))" using affine_translation affine_affine_hull by auto -moreover have "(%x. -a + x) ` (%x. a + x) ` S <= (%x. -a + x) ` (affine hull ((%x. a + x) ` S))" using hull_subset[of "(%x. a + x) ` S"] by auto +moreover have "(%x. -a + x) ` (%x. a + x) ` S <= (%x. -a + x) ` (affine hull ((%x. a + x) ` S))" using hull_subset[of "(%x. a + x) ` S"] by auto moreover have "S=(%x. -a + x) ` (%x. a + x) ` S" using translation_assoc[of "-a" a] by auto ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) ` S)) >= (affine hull S)" by (metis hull_minimal) hence "affine hull ((%x. a + x) ` S) >= (%x. a + x) ` (affine hull S)" by auto @@ -1854,15 +1854,15 @@ obtain x where x_def: "x : S & x : affine hull (S - {x})" using assms affine_dependent_def by auto have "op + a ` (S - {x}) = op + a ` S - {a + x}" by auto hence "a+x : affine hull ((%x. a + x) ` S - {a+x})" using affine_hull_translation[of a "S-{x}"] x_def by auto -moreover have "a+x : (%x. a + x) ` S" using x_def by auto -ultimately show ?thesis unfolding affine_dependent_def by auto +moreover have "a+x : (%x. a + x) ` S" using x_def by auto +ultimately show ?thesis unfolding affine_dependent_def by auto qed lemma affine_dependent_translation_eq: "affine_dependent S <-> affine_dependent ((%x. a + x) ` S)" proof- -{ assume "affine_dependent ((%x. a + x) ` S)" - hence "affine_dependent S" using affine_dependent_translation[of "((%x. a + x) ` S)" "-a"] translation_assoc[of "-a" a] by auto +{ assume "affine_dependent ((%x. a + x) ` S)" + hence "affine_dependent S" using affine_dependent_translation[of "((%x. a + x) ` S)" "-a"] translation_assoc[of "-a" a] by auto } from this show ?thesis using affine_dependent_translation by auto qed @@ -1871,7 +1871,7 @@ shows "dependent S" proof- obtain s u where s_u_def: "finite s & s ~= {} & s <= S & setsum u s = 1 & (SUM v:s. u v *\<^sub>R v) = 0" using assms affine_hull_explicit[of S] by auto -hence "EX v:s. u v ~= 0" using setsum_not_0[of "u" "s"] by auto +hence "EX v:s. u v ~= 0" using setsum_not_0[of "u" "s"] by auto hence "finite s & s <= S & (EX v:s. u v ~= 0 & (SUM v:s. u v *\<^sub>R v) = 0)" using s_u_def by auto from this show ?thesis unfolding dependent_explicit[of S] by auto qed @@ -1887,17 +1887,17 @@ hence "(x~=0) ==> dependent S" using x_def dependent_def by auto moreover { assume "x=0" hence "0 : affine hull S" using x_def hull_mono[of "S - {0}" S] by auto - hence "dependent S" using affine_hull_0_dependent by auto + hence "dependent S" using affine_hull_0_dependent by auto } ultimately show ?thesis by auto qed lemma affine_dependent_iff_dependent: assumes "a ~: S" - shows "affine_dependent (insert a S) <-> dependent ((%x. -a + x) ` S)" + shows "affine_dependent (insert a S) <-> dependent ((%x. -a + x) ` S)" proof- have "(op + (- a) ` S)={x - a| x . x : S}" by auto -from this show ?thesis using affine_dependent_translation_eq[of "(insert a S)" "-a"] - affine_dependent_imp_dependent2 assms +from this show ?thesis using affine_dependent_translation_eq[of "(insert a S)" "-a"] + affine_dependent_imp_dependent2 assms dependent_imp_affine_dependent[of a S] by auto qed @@ -1906,25 +1906,25 @@ shows "affine_dependent S <-> dependent ((%x. -a + x) ` (S-{a}))" proof- have "insert a (S - {a})=S" using assms by auto -from this show ?thesis using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto +from this show ?thesis using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto qed lemma affine_hull_insert_span_gen: - shows "affine hull (insert a s) = (%x. a+x) ` span ((%x. -a+x) ` s)" + shows "affine hull (insert a s) = (%x. a+x) ` span ((%x. -a+x) ` s)" proof- have h1: "{x - a |x. x : s}=((%x. -a+x) ` s)" by auto -{ assume "a ~: s" hence ?thesis using affine_hull_insert_span[of a s] h1 by auto} +{ assume "a ~: s" hence ?thesis using affine_hull_insert_span[of a s] h1 by auto} moreover { assume a1: "a : s" have "EX x. x:s & -a+x=0" apply (rule exI[of _ a]) using a1 by auto hence "insert 0 ((%x. -a+x) ` (s - {a}))=(%x. -a+x) ` s" by auto - hence "span ((%x. -a+x) ` (s - {a}))=span ((%x. -a+x) ` s)" + hence "span ((%x. -a+x) ` (s - {a}))=span ((%x. -a+x) ` s)" using span_insert_0[of "op + (- a) ` (s - {a})"] by auto - moreover have "{x - a |x. x : (s - {a})}=((%x. -a+x) ` (s - {a}))" by auto + moreover have "{x - a |x. x : (s - {a})}=((%x. -a+x) ` (s - {a}))" by auto moreover have "insert a (s - {a})=(insert a s)" using assms by auto ultimately have ?thesis using assms affine_hull_insert_span[of "a" "s-{a}"] by auto -} -ultimately show ?thesis by auto +} +ultimately show ?thesis by auto qed lemma affine_hull_span2: @@ -1953,21 +1953,21 @@ proof- obtain a where a_def: "a : S" using assms by auto hence h0: "independent ((%x. -a + x) ` (S-{a}))" using affine_dependent_iff_dependent2 assms by auto -from this obtain B - where B_def: "(%x. -a+x) ` (S - {a}) <= B & B <= (%x. -a+x) ` V & independent B & (%x. -a+x) ` V <= span B" +from this obtain B + where B_def: "(%x. -a+x) ` (S - {a}) <= B & B <= (%x. -a+x) ` V & independent B & (%x. -a+x) ` V <= span B" using maximal_independent_subset_extend[of "(%x. -a+x) ` (S-{a})" "(%x. -a + x) ` V"] assms by blast def T == "(%x. a+x) ` (insert 0 B)" hence "T=insert a ((%x. a+x) ` B)" by auto hence "affine hull T = (%x. a+x) ` span B" using affine_hull_insert_span_gen[of a "((%x. a+x) ` B)"] translation_assoc[of "-a" a B] by auto hence "V <= affine hull T" using B_def assms translation_inverse_subset[of a V "span B"] by auto moreover have "T<=V" using T_def B_def a_def assms by auto -ultimately have "affine hull T = affine hull V" +ultimately have "affine hull T = affine hull V" by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono) moreover have "S<=T" using T_def B_def translation_inverse_subset[of a "S-{a}" B] by auto moreover have "~(affine_dependent T)" using T_def affine_dependent_translation_eq[of "insert 0 B"] affine_dependent_imp_dependent2 B_def by auto ultimately show ?thesis using `T<=V` by auto qed -lemma affine_basis_exists: +lemma affine_basis_exists: fixes V :: "('n::euclidean_space) set" shows "? B. B <= V & ~(affine_dependent B) & affine hull V = affine hull B" proof- @@ -1986,7 +1986,7 @@ definition "aff_dim V = (SOME d :: int. ? B. (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = d+1))" lemma aff_dim_basis_exists: - fixes V :: "('n::euclidean_space) set" + fixes V :: "('n::euclidean_space) set" shows "? B. (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = aff_dim V+1)" proof- obtain B where B_def: "~(affine_dependent B) & (affine hull B=affine hull V)" using affine_basis_exists[of V] by auto @@ -1995,7 +1995,7 @@ lemma affine_hull_nonempty: "(S ~= {}) <-> affine hull S ~= {}" proof- -have "(S = {}) ==> affine hull S = {}"using affine_hull_empty by auto +have "(S = {}) ==> affine hull S = {}"using affine_hull_empty by auto moreover have "affine hull S = {} ==> S = {}" unfolding hull_def by auto ultimately show "(S ~= {}) <-> affine hull S ~= {}" by blast qed @@ -2003,19 +2003,19 @@ lemma aff_dim_parallel_subspace_aux: fixes B :: "('n::euclidean_space) set" assumes "~(affine_dependent B)" "a:B" -shows "finite B & ((card B) - 1 = dim (span ((%x. -a+x) ` (B-{a}))))" +shows "finite B & ((card B) - 1 = dim (span ((%x. -a+x) ` (B-{a}))))" proof- have "independent ((%x. -a + x) ` (B-{a}))" using affine_dependent_iff_dependent2 assms by auto hence fin: "dim (span ((%x. -a+x) ` (B-{a}))) = card ((%x. -a + x) ` (B-{a}))" "finite ((%x. -a + x) ` (B - {a}))" using indep_card_eq_dim_span[of "(%x. -a+x) ` (B-{a})"] by auto -{ assume emp: "(%x. -a + x) ` (B - {a}) = {}" +{ assume emp: "(%x. -a + x) ` (B - {a}) = {}" have "B=insert a ((%x. a + x) ` (%x. -a + x) ` (B - {a}))" using translation_assoc[of "a" "-a" "(B - {a})"] assms by auto hence "B={a}" using emp by auto - hence ?thesis using assms fin by auto + hence ?thesis using assms fin by auto } moreover { assume "(%x. -a + x) ` (B - {a}) ~= {}" hence "card ((%x. -a + x) ` (B - {a}))>0" using fin by auto - moreover have h1: "card ((%x. -a + x) ` (B-{a})) = card (B-{a})" + moreover have h1: "card ((%x. -a + x) ` (B-{a})) = card (B-{a})" apply (rule card_image) using translate_inj_on by auto ultimately have "card (B-{a})>0" by auto hence "finite(B-{a})" using card_gt_0_iff[of "(B - {a})"] by auto @@ -2031,15 +2031,15 @@ shows "aff_dim V=int(dim L)" proof- obtain B where B_def: "affine hull B = affine hull V & ~ affine_dependent B & int (card B) = aff_dim V + 1" using aff_dim_basis_exists by auto -hence "B~={}" using assms B_def affine_hull_nonempty[of V] affine_hull_nonempty[of B] by auto +hence "B~={}" using assms B_def affine_hull_nonempty[of V] affine_hull_nonempty[of B] by auto from this obtain a where a_def: "a : B" by auto def Lb == "span ((%x. -a+x) ` (B-{a}))" moreover have "affine_parallel (affine hull B) Lb" using Lb_def B_def assms affine_hull_span2[of a B] a_def affine_parallel_commut[of "Lb" "(affine hull B)"] unfolding affine_parallel_def by auto moreover have "subspace Lb" using Lb_def subspace_span by auto moreover have "affine hull B ~= {}" using assms B_def affine_hull_nonempty[of V] by auto - ultimately have "L=Lb" using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B_def by auto - hence "dim L=dim Lb" by auto + ultimately have "L=Lb" using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B_def by auto + hence "dim L=dim Lb" by auto moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a_def B_def by auto (* hence "card B=dim Lb+1" using `B~={}` card_gt_0_iff[of B] by auto *) ultimately show ?thesis using B_def `B~={}` card_gt_0_iff[of B] by auto @@ -2050,23 +2050,23 @@ assumes "~(affine_dependent B)" shows "finite B" proof- -{ assume "B~={}" from this obtain a where "a:B" by auto - hence ?thesis using aff_dim_parallel_subspace_aux assms by auto +{ assume "B~={}" from this obtain a where "a:B" by auto + hence ?thesis using aff_dim_parallel_subspace_aux assms by auto } from this show ?thesis by auto qed lemma independent_finite: fixes B :: "('n::euclidean_space) set" -assumes "independent B" +assumes "independent B" shows "finite B" using affine_dependent_imp_dependent[of B] aff_independent_finite[of B] assms by auto lemma subspace_dim_equal: assumes "subspace (S :: ('n::euclidean_space) set)" "subspace T" "S <= T" "dim S >= dim T" shows "S=T" -proof- +proof- obtain B where B_def: "B <= S & independent B & S <= span B & (card B = dim S)" using basis_exists[of S] by auto -hence "span B <= S" using span_mono[of B S] span_eq[of S] assms by metis +hence "span B <= S" using span_mono[of B S] span_eq[of S] assms by metis hence "span B = S" using B_def by auto have "dim S = dim T" using assms dim_subset[of S T] by auto hence "T <= span B" using card_eq_dim[of B T] B_def independent_finite assms by auto @@ -2080,18 +2080,18 @@ have "?A <= ?B" by auto moreover have s: "subspace ?B" using subspace_substandard[of "%i. i ~: d"] . ultimately have "span ?A <= ?B" using span_mono[of "?A" "?B"] span_eq[of "?B"] by blast -moreover have "card d <= dim (span ?A)" using independent_card_le_dim[of "?A" "span ?A"] +moreover have "card d <= dim (span ?A)" using independent_card_le_dim[of "?A" "span ?A"] independent_substdbasis[OF assms] card_substdbasis[OF assms] span_inc[of "?A"] by auto moreover hence "dim ?B <= dim (span ?A)" using dim_substandard[OF assms] by auto -ultimately show ?thesis using s subspace_dim_equal[of "span ?A" "?B"] +ultimately show ?thesis using s subspace_dim_equal[of "span ?A" "?B"] subspace_span[of "?A"] by auto qed lemma basis_to_substdbasis_subspace_isomorphism: -fixes B :: "('a::euclidean_space) set" +fixes B :: "('a::euclidean_space) set" assumes "independent B" -shows "EX f d. card d = card B & linear f & f ` B = {basis i::'a |i. i : (d :: nat set)} & - f ` span B = {x. ALL i x $$ i = (0::real)} & inj_on f (span B) \ d\{.. x $$ i = (0::real)} & inj_on f (span B) \ d\{.. "{.. aff_dim S = -1" proof- obtain B where "affine hull B = affine hull S & ~ affine_dependent B & int (card B) = aff_dim S + 1" using aff_dim_basis_exists by auto @@ -2119,49 +2119,49 @@ qed lemma aff_dim_affine_hull: -shows "aff_dim (affine hull S)=aff_dim S" -unfolding aff_dim_def using hull_hull[of _ S] by auto +shows "aff_dim (affine hull S)=aff_dim S" +unfolding aff_dim_def using hull_hull[of _ S] by auto lemma aff_dim_affine_hull2: assumes "affine hull S=affine hull T" shows "aff_dim S=aff_dim T" unfolding aff_dim_def using assms by auto -lemma aff_dim_unique: -fixes B V :: "('n::euclidean_space) set" +lemma aff_dim_unique: +fixes B V :: "('n::euclidean_space) set" assumes "(affine hull B=affine hull V) & ~(affine_dependent B)" shows "of_nat(card B) = aff_dim V+1" proof- { assume "B={}" hence "V={}" using affine_hull_nonempty[of V] affine_hull_nonempty[of B] assms by auto - hence "aff_dim V = (-1::int)" using aff_dim_empty by auto + hence "aff_dim V = (-1::int)" using aff_dim_empty by auto hence ?thesis using `B={}` by auto } moreover -{ assume "B~={}" from this obtain a where a_def: "a:B" by auto +{ assume "B~={}" from this obtain a where a_def: "a:B" by auto def Lb == "span ((%x. -a+x) ` (B-{a}))" have "affine_parallel (affine hull B) Lb" - using Lb_def affine_hull_span2[of a B] a_def affine_parallel_commut[of "Lb" "(affine hull B)"] + using Lb_def affine_hull_span2[of a B] a_def affine_parallel_commut[of "Lb" "(affine hull B)"] unfolding affine_parallel_def by auto moreover have "subspace Lb" using Lb_def subspace_span by auto - ultimately have "aff_dim B=int(dim Lb)" using aff_dim_parallel_subspace[of B Lb] `B~={}` by auto + ultimately have "aff_dim B=int(dim Lb)" using aff_dim_parallel_subspace[of B Lb] `B~={}` by auto moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a_def assms by auto ultimately have "(of_nat(card B) = aff_dim B+1)" using `B~={}` card_gt_0_iff[of B] by auto hence ?thesis using aff_dim_affine_hull2 assms by auto } ultimately show ?thesis by blast qed -lemma aff_dim_affine_independent: -fixes B :: "('n::euclidean_space) set" +lemma aff_dim_affine_independent: +fixes B :: "('n::euclidean_space) set" assumes "~(affine_dependent B)" shows "of_nat(card B) = aff_dim B+1" using aff_dim_unique[of B B] assms by auto -lemma aff_dim_sing: -fixes a :: "'n::euclidean_space" +lemma aff_dim_sing: +fixes a :: "'n::euclidean_space" shows "aff_dim {a}=0" using aff_dim_affine_independent[of "{a}"] affine_independent_sing by auto lemma aff_dim_inner_basis_exists: - fixes V :: "('n::euclidean_space) set" + fixes V :: "('n::euclidean_space) set" shows "? B. B<=V & (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = aff_dim V+1)" proof- obtain B where B_def: "~(affine_dependent B) & B<=V & (affine hull B=affine hull V)" using affine_basis_exists[of V] by auto @@ -2170,11 +2170,11 @@ qed lemma aff_dim_le_card: -fixes V :: "('n::euclidean_space) set" +fixes V :: "('n::euclidean_space) set" assumes "finite V" shows "aff_dim V <= of_nat(card V) - 1" proof- - obtain B where B_def: "B<=V & (of_nat(card B) = aff_dim V+1)" using aff_dim_inner_basis_exists[of V] by auto + obtain B where B_def: "B<=V & (of_nat(card B) = aff_dim V+1)" using aff_dim_inner_basis_exists[of V] by auto moreover hence "card B <= card V" using assms card_mono by auto ultimately show ?thesis by auto qed @@ -2184,13 +2184,13 @@ assumes "affine_parallel (affine hull S) (affine hull T)" shows "aff_dim S=aff_dim T" proof- -{ assume "T~={}" "S~={}" - from this obtain L where L_def: "subspace L & affine_parallel (affine hull T) L" +{ assume "T~={}" "S~={}" + from this obtain L where L_def: "subspace L & affine_parallel (affine hull T) L" using affine_parallel_subspace[of "affine hull T"] affine_affine_hull[of T] affine_hull_nonempty by auto hence "aff_dim T = int(dim L)" using aff_dim_parallel_subspace `T~={}` by auto - moreover have "subspace L & affine_parallel (affine hull S) L" + moreover have "subspace L & affine_parallel (affine hull S) L" using L_def affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto - moreover hence "aff_dim S = int(dim L)" using aff_dim_parallel_subspace `S~={}` by auto + moreover hence "aff_dim S = int(dim L)" using aff_dim_parallel_subspace `S~={}` by auto ultimately have ?thesis by auto } moreover @@ -2206,21 +2206,21 @@ lemma aff_dim_translation_eq: fixes a :: "'n::euclidean_space" -shows "aff_dim ((%x. a + x) ` S)=aff_dim S" +shows "aff_dim ((%x. a + x) ` S)=aff_dim S" proof- have "affine_parallel (affine hull S) (affine hull ((%x. a + x) ` S))" unfolding affine_parallel_def apply (rule exI[of _ "a"]) using affine_hull_translation[of a S] by auto -from this show ?thesis using aff_dim_parallel_eq[of S "(%x. a + x) ` S"] by auto +from this show ?thesis using aff_dim_parallel_eq[of S "(%x. a + x) ` S"] by auto qed lemma aff_dim_affine: fixes S L :: "('n::euclidean_space) set" assumes "S ~= {}" "affine S" assumes "subspace L" "affine_parallel S L" -shows "aff_dim S=int(dim L)" +shows "aff_dim S=int(dim L)" proof- -have 1: "(affine hull S) = S" using assms affine_hull_eq[of S] by auto +have 1: "(affine hull S) = S" using assms affine_hull_eq[of S] by auto hence "affine_parallel (affine hull S) L" using assms by (simp add:1) -from this show ?thesis using assms aff_dim_parallel_subspace[of S L] by blast +from this show ?thesis using assms aff_dim_parallel_subspace[of S L] by blast qed lemma dim_affine_hull: @@ -2236,7 +2236,7 @@ lemma aff_dim_subspace: fixes S :: "('n::euclidean_space) set" assumes "S ~= {}" "subspace S" -shows "aff_dim S=int(dim S)" using aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] by auto +shows "aff_dim S=int(dim S)" using aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] by auto lemma aff_dim_zero: fixes S :: "('n::euclidean_space) set" @@ -2244,7 +2244,7 @@ shows "aff_dim S=int(dim S)" proof- have "subspace(affine hull S)" using subspace_affine[of "affine hull S"] affine_affine_hull assms by auto -hence "aff_dim (affine hull S) =int(dim (affine hull S))" using assms aff_dim_subspace[of "affine hull S"] by auto +hence "aff_dim (affine hull S) =int(dim (affine hull S))" using assms aff_dim_subspace[of "affine hull S"] by auto from this show ?thesis using aff_dim_affine_hull[of S] dim_affine_hull[of S] by auto qed @@ -2260,13 +2260,13 @@ from this show ?thesis by auto qed -lemma independent_card_le_aff_dim: +lemma independent_card_le_aff_dim: assumes "(B::('n::euclidean_space) set) <= V" - assumes "~(affine_dependent B)" + assumes "~(affine_dependent B)" shows "int(card B) <= aff_dim V+1" proof- -{ assume "B~={}" - from this obtain T where T_def: "~(affine_dependent T) & B<=T & T<=V & affine hull T = affine hull V" +{ assume "B~={}" + from this obtain T where T_def: "~(affine_dependent T) & B<=T & T<=V & affine hull T = affine hull V" using assms extend_to_affine_basis[of B V] by auto hence "of_nat(card T) = aff_dim V+1" using aff_dim_unique by auto hence ?thesis using T_def card_mono[of T B] aff_independent_finite[of T] by auto @@ -2291,7 +2291,7 @@ lemma aff_dim_subset_univ: fixes S :: "('n::euclidean_space) set" shows "aff_dim S <= int(DIM('n))" -proof - +proof - have "aff_dim (UNIV :: ('n::euclidean_space) set) = int(DIM('n))" using aff_dim_univ by auto from this show "aff_dim (S:: ('n::euclidean_space) set) <= int(DIM('n))" using assms aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto qed @@ -2300,21 +2300,21 @@ assumes "affine (S :: ('n::euclidean_space) set)" "affine T" "S ~= {}" "S <= T" "aff_dim S = aff_dim T" shows "S=T" proof- -obtain a where "a : S" using assms by auto +obtain a where "a : S" using assms by auto hence "a : T" using assms by auto def LS == "{y. ? x : S. (-a)+x=y}" -hence ls: "subspace LS & affine_parallel S LS" using assms parallel_subspace_explicit[of S a LS] `a : S` by auto +hence ls: "subspace LS & affine_parallel S LS" using assms parallel_subspace_explicit[of S a LS] `a : S` by auto hence h1: "int(dim LS) = aff_dim S" using assms aff_dim_affine[of S LS] by auto have "T ~= {}" using assms by auto -def LT == "{y. ? x : T. (-a)+x=y}" +def LT == "{y. ? x : T. (-a)+x=y}" hence lt: "subspace LT & affine_parallel T LT" using assms parallel_subspace_explicit[of T a LT] `a : T` by auto -hence "int(dim LT) = aff_dim T" using assms aff_dim_affine[of T LT] `T ~= {}` by auto +hence "int(dim LT) = aff_dim T" using assms aff_dim_affine[of T LT] `T ~= {}` by auto hence "dim LS = dim LT" using h1 assms by auto moreover have "LS <= LT" using LS_def LT_def assms by auto ultimately have "LS=LT" using subspace_dim_equal[of LS LT] ls lt by auto -moreover have "S = {x. ? y : LS. a+y=x}" using LS_def by auto +moreover have "S = {x. ? y : LS. a+y=x}" using LS_def by auto moreover have "T = {x. ? y : LT. a+y=x}" using LT_def by auto -ultimately show ?thesis by auto +ultimately show ?thesis by auto qed lemma affine_hull_univ: @@ -2325,7 +2325,7 @@ have "S ~= {}" using assms aff_dim_empty[of S] by auto have h0: "S <= affine hull S" using hull_subset[of S _] by auto have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S" using aff_dim_univ assms by auto -hence h2: "aff_dim (affine hull S) <= aff_dim (UNIV :: ('n::euclidean_space) set)" using aff_dim_subset_univ[of "affine hull S"] assms h0 by auto +hence h2: "aff_dim (affine hull S) <= aff_dim (UNIV :: ('n::euclidean_space) set)" using aff_dim_subset_univ[of "affine hull S"] assms h0 by auto have h3: "aff_dim S <= aff_dim (affine hull S)" using h0 aff_dim_subset[of S "affine hull S"] assms by auto hence h4: "aff_dim (affine hull S) = aff_dim (UNIV :: ('n::euclidean_space) set)" using h0 h1 h2 by auto from this show ?thesis using affine_dim_equal[of "affine hull S" "(UNIV :: ('n::euclidean_space) set)"] affine_affine_hull[of S] affine_UNIV assms h4 h0 `S ~= {}` by auto @@ -2334,23 +2334,23 @@ lemma aff_dim_convex_hull: fixes S :: "('n::euclidean_space) set" shows "aff_dim (convex hull S)=aff_dim S" - using aff_dim_affine_hull[of S] convex_hull_subset_affine_hull[of S] - hull_subset[of S "convex"] aff_dim_subset[of S "convex hull S"] + using aff_dim_affine_hull[of S] convex_hull_subset_affine_hull[of S] + hull_subset[of S "convex"] aff_dim_subset[of S "convex hull S"] aff_dim_subset[of "convex hull S" "affine hull S"] by auto lemma aff_dim_cball: -fixes a :: "'n::euclidean_space" +fixes a :: "'n::euclidean_space" assumes "00 & cball x e <= S" using open_contains_cball[of S] assms by auto from this have "aff_dim (cball x e) <= aff_dim S" using aff_dim_subset by auto -from this show ?thesis using aff_dim_cball[of e x] aff_dim_subset_univ[of S] e_def by auto +from this show ?thesis using aff_dim_cball[of e x] aff_dim_subset_univ[of S] e_def by auto qed lemma low_dim_interior: @@ -2369,9 +2369,9 @@ assumes "~(aff_dim S = int (DIM('n)))" shows "interior S = {}" proof- -have "aff_dim(interior S) <= aff_dim S" - using interior_subset aff_dim_subset[of "interior S" S] by auto -from this show ?thesis using aff_dim_open[of "interior S"] aff_dim_subset_univ[of S] assms by auto +have "aff_dim(interior S) <= aff_dim S" + using interior_subset aff_dim_subset[of "interior S" S] by auto +from this show ?thesis using aff_dim_open[of "interior S"] aff_dim_subset_univ[of S] assms by auto qed subsection {* Relative interior of a set *} @@ -2388,8 +2388,8 @@ using a h1 by auto qed -lemma mem_rel_interior: - "x : rel_interior S <-> (? T. open T & x : (T Int S) & (T Int (affine hull S)) <= S)" +lemma mem_rel_interior: + "x : rel_interior S <-> (? T. open T & x : (T Int S) & (T Int (affine hull S)) <= S)" by (auto simp add: rel_interior) lemma mem_rel_interior_ball: "x : rel_interior S <-> x : S & (? e. 0 < e & ((ball x e) Int (affine hull S)) <= S)" @@ -2399,12 +2399,12 @@ apply simp done -lemma rel_interior_ball: - "rel_interior S = {x : S. ? e. e>0 & ((ball x e) Int (affine hull S)) <= S}" - using mem_rel_interior_ball [of _ S] by auto +lemma rel_interior_ball: + "rel_interior S = {x : S. ? e. e>0 & ((ball x e) Int (affine hull S)) <= S}" + using mem_rel_interior_ball [of _ S] by auto lemma mem_rel_interior_cball: "x : rel_interior S <-> x : S & (? e. 0 < e & ((cball x e) Int (affine hull S)) <= S)" - apply (simp add: rel_interior, safe) + apply (simp add: rel_interior, safe) apply (force simp add: open_contains_cball) apply (rule_tac x="ball x e" in exI) apply (simp add: subset_trans [OF ball_subset_cball]) @@ -2413,8 +2413,8 @@ lemma rel_interior_cball: "rel_interior S = {x : S. ? e. e>0 & ((cball x e) Int (affine hull S)) <= S}" using mem_rel_interior_cball [of _ S] by auto -lemma rel_interior_empty: "rel_interior {} = {}" - by (auto simp add: rel_interior_def) +lemma rel_interior_empty: "rel_interior {} = {}" + by (auto simp add: rel_interior_def) lemma affine_hull_sing: "affine hull {a :: 'n::euclidean_space} = {a}" by (metis affine_hull_eq affine_sing) @@ -2428,15 +2428,15 @@ fixes S T :: "('n::euclidean_space) set" assumes "S<=T" "affine hull S=affine hull T" shows "rel_interior S <= rel_interior T" - using assms by (auto simp add: rel_interior_def) - -lemma rel_interior_subset: "rel_interior S <= S" + using assms by (auto simp add: rel_interior_def) + +lemma rel_interior_subset: "rel_interior S <= S" by (auto simp add: rel_interior_def) -lemma rel_interior_subset_closure: "rel_interior S <= closure S" - using rel_interior_subset by (auto simp add: closure_def) - -lemma interior_subset_rel_interior: "interior S <= rel_interior S" +lemma rel_interior_subset_closure: "rel_interior S <= closure S" + using rel_interior_subset by (auto simp add: closure_def) + +lemma interior_subset_rel_interior: "interior S <= rel_interior S" by (auto simp add: rel_interior interior_def) lemma interior_rel_interior: @@ -2444,7 +2444,7 @@ assumes "aff_dim S = int(DIM('n))" shows "rel_interior S = interior S" proof - -have "affine hull S = UNIV" using assms affine_hull_univ[of S] by auto +have "affine hull S = UNIV" using assms affine_hull_univ[of S] by auto from this show ?thesis unfolding rel_interior interior_def by auto qed @@ -2459,16 +2459,16 @@ shows "interior S = (if aff_dim S = int(DIM('n)) then rel_interior S else {})" by (metis interior_rel_interior low_dim_interior) -lemma rel_interior_univ: +lemma rel_interior_univ: fixes S :: "('n::euclidean_space) set" shows "rel_interior (affine hull S) = affine hull S" proof- -have h1: "rel_interior (affine hull S) <= affine hull S" using rel_interior_subset by auto +have h1: "rel_interior (affine hull S) <= affine hull S" using rel_interior_subset by auto { fix x assume x_def: "x : affine hull S" obtain e :: real where "e=1" by auto hence "e>0 & ball x e Int affine hull (affine hull S) <= affine hull S" using hull_hull[of _ S] by auto hence "x : rel_interior (affine hull S)" using x_def rel_interior_ball[of "affine hull S"] by auto -} from this show ?thesis using h1 by auto +} from this show ?thesis using h1 by auto qed lemma rel_interior_univ2: "rel_interior (UNIV :: ('n::euclidean_space) set) = UNIV" @@ -2478,25 +2478,25 @@ fixes S :: "('a::euclidean_space) set" assumes "convex S" "c : rel_interior S" "x : S" "0 < e" "e <= 1" shows "x - e *\<^sub>R (x - c) : rel_interior S" -proof- -(* Proof is a modified copy of the proof of similar lemma mem_interior_convex_shrink +proof- +(* Proof is a modified copy of the proof of similar lemma mem_interior_convex_shrink *) -obtain d where "d>0" and d:"ball c d Int affine hull S <= S" +obtain d where "d>0" and d:"ball c d Int affine hull S <= S" using assms(2) unfolding mem_rel_interior_ball by auto { fix y assume as:"dist (x - e *\<^sub>R (x - c)) y < e * d & y : affine hull S" have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib) have "x : affine hull S" using assms hull_subset[of S] by auto - moreover have "1 / e + - ((1 - e) / e) = 1" + moreover have "1 / e + - ((1 - e) / e) = 1" using `e>0` left_diff_distrib[of "1" "(1-e)" "1/e"] by auto ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x : affine hull S" - 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) + 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) have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)" unfolding dist_norm unfolding norm_scaleR[symmetric] apply(rule arg_cong[where f=norm]) using `e>0` - by(auto simp add:euclidean_eq[where 'a='a] field_simps) + by(auto simp add:euclidean_eq[where 'a='a] field_simps) also have "... = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:arg_cong[where f=norm] simp add: algebra_simps) also have "... < d" using as[unfolded dist_norm] and `e>0` by(auto simp add:pos_divide_less_eq[OF `e>0`] mult_commute) - finally have "y : S" apply(subst *) + finally have "y : S" apply(subst *) apply(rule assms(1)[unfolded convex_alt,rule_format]) apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) ** by auto } hence "ball (x - e *\<^sub>R (x - c)) (e*d) Int affine hull S <= S" by auto @@ -2504,7 +2504,7 @@ moreover have "c : S" using assms rel_interior_subset by auto moreover hence "x - e *\<^sub>R (x - c) : S" using mem_convex[of S x c e] apply (simp add: algebra_simps) using assms by auto -ultimately show ?thesis +ultimately show ?thesis using mem_rel_interior_ball[of "x - e *\<^sub>R (x - c)" S] `e>0` by auto qed @@ -2513,13 +2513,13 @@ shows "interior {a..} = {a<..}" proof- { fix y assume "a0 & cball y e \ {a..}" + from this obtain e where e_def: "e>0 & cball y e \ {a..}" using mem_interior_cball[of y "{a..}"] by auto - moreover hence "y-e : cball y e" by (auto simp add: cball_def dist_norm) + moreover hence "y-e : cball y e" by (auto simp add: cball_def dist_norm) ultimately have "a<=y-e" by auto hence "a= affine hull S" +moreover have "affine hull (closure S) >= affine hull S" using hull_mono[of "S" "closure S" "affine"] closure_subset by auto -ultimately show ?thesis by auto -qed - -lemma closure_aff_dim: +ultimately show ?thesis by auto +qed + +lemma closure_aff_dim: fixes S :: "('n::euclidean_space) set" shows "aff_dim (closure S) = aff_dim S" proof- have "aff_dim S <= aff_dim (closure S)" using aff_dim_subset closure_subset by auto -moreover have "aff_dim (closure S) <= aff_dim (affine hull S)" +moreover have "aff_dim (closure S) <= aff_dim (affine hull S)" using aff_dim_subset closure_affine_hull by auto moreover have "aff_dim (affine hull S) = aff_dim S" using aff_dim_affine_hull by auto ultimately show ?thesis by auto @@ -2606,10 +2606,10 @@ fixes S :: "(_::euclidean_space) set" assumes "convex S" "c : rel_interior S" "x : closure S" "0 < e" "e <= 1" shows "x - e *\<^sub>R (x - c) : rel_interior S" -proof- +proof- (* Proof is a modified copy of the proof of similar lemma mem_interior_closure_convex_shrink *) -obtain d where "d>0" and d:"ball c d Int affine hull S <= S" +obtain d where "d>0" and d:"ball c d Int affine hull S <= S" using assms(2) unfolding mem_rel_interior_ball by auto have "EX y : S. norm (y - x) * (1 - e) < e * d" proof(cases "x : S") case True thus ?thesis using `e>0` `d>0` by(rule_tac bexI[where x=x], auto intro!: mult_pos_pos) next @@ -2631,18 +2631,18 @@ have "x : affine hull S" using closure_affine_hull assms by auto moreover have "y : affine hull S" using `y : S` hull_subset[of S] by auto moreover have "c : affine hull S" using assms rel_interior_subset hull_subset[of S] by auto - ultimately have "z : affine hull S" - using z_def affine_affine_hull[of S] - mem_affine_3_minus [of "affine hull S" c x y "(1 - e) / e"] + ultimately have "z : affine hull S" + using z_def affine_affine_hull[of S] + mem_affine_3_minus [of "affine hull S" c x y "(1 - e) / e"] assms by (auto simp add: field_simps) hence "z : S" using d zball by auto obtain d1 where "d1>0" and d1:"ball z d1 <= ball c d" using zball open_ball[of c d] openE[of "ball c d" z] by auto hence "(ball z d1) Int (affine hull S) <= (ball c d) Int (affine hull S)" by auto - hence "(ball z d1) Int (affine hull S) <= S" using d by auto + hence "(ball z d1) Int (affine hull S) <= S" using d by auto hence "z : rel_interior S" using mem_rel_interior_ball using `d1>0` `z : S` by auto hence "y - e *\<^sub>R (y - z) : rel_interior S" using rel_interior_convex_shrink[of S z y e] assms`y : S` by auto - thus ?thesis using * by auto + thus ?thesis using * by auto qed subsubsection{* Relative interior preserves under linear transformations *} @@ -2652,27 +2652,27 @@ shows "((%x. a + x) ` rel_interior S) <= rel_interior ((%x. a + x) ` S)" proof- { fix x assume x_def: "x : rel_interior S" - from this obtain T where T_def: "open T & x : (T Int S) & (T Int (affine hull S)) <= S" using mem_rel_interior[of x S] by auto - from this have "open ((%x. a + x) ` T)" and - "(a + x) : (((%x. a + x) ` T) Int ((%x. a + x) ` S))" and - "(((%x. a + x) ` T) Int (affine hull ((%x. a + x) ` S))) <= ((%x. a + x) ` S)" - using affine_hull_translation[of a S] open_translation[of T a] x_def by auto - from this have "(a+x) : rel_interior ((%x. a + x) ` S)" - using mem_rel_interior[of "a+x" "((%x. a + x) ` S)"] by auto -} from this show ?thesis by auto + from this obtain T where T_def: "open T & x : (T Int S) & (T Int (affine hull S)) <= S" using mem_rel_interior[of x S] by auto + from this have "open ((%x. a + x) ` T)" and + "(a + x) : (((%x. a + x) ` T) Int ((%x. a + x) ` S))" and + "(((%x. a + x) ` T) Int (affine hull ((%x. a + x) ` S))) <= ((%x. a + x) ` S)" + using affine_hull_translation[of a S] open_translation[of T a] x_def by auto + from this have "(a+x) : rel_interior ((%x. a + x) ` S)" + using mem_rel_interior[of "a+x" "((%x. a + x) ` S)"] by auto +} from this show ?thesis by auto qed lemma rel_interior_translation: fixes a :: "'n::euclidean_space" shows "rel_interior ((%x. a + x) ` S) = ((%x. a + x) ` rel_interior S)" proof- -have "(%x. (-a) + x) ` rel_interior ((%x. a + x) ` S) <= rel_interior S" - using rel_interior_translation_aux[of "-a" "(%x. a + x) ` S"] +have "(%x. (-a) + x) ` rel_interior ((%x. a + x) ` S) <= rel_interior S" + using rel_interior_translation_aux[of "-a" "(%x. a + x) ` S"] translation_assoc[of "-a" "a"] by auto -hence "((%x. a + x) ` rel_interior S) >= rel_interior ((%x. a + x) ` S)" - using translation_inverse_subset[of a "rel_interior (op + a ` S)" "rel_interior S"] +hence "((%x. a + x) ` rel_interior S) >= rel_interior ((%x. a + x) ` S)" + using translation_inverse_subset[of a "rel_interior (op + a ` S)" "rel_interior S"] by auto -from this show ?thesis using rel_interior_translation_aux[of a S] by auto +from this show ?thesis using rel_interior_translation_aux[of a S] by auto qed @@ -2681,15 +2681,15 @@ shows "f ` (affine hull s) = affine hull f ` s" (* Proof is a modified copy of the proof of similar lemma convex_hull_linear_image *) - apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3 + apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3 apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption proof- interpret f: bounded_linear f by fact - show "affine {x. f x : affine hull f ` s}" + show "affine {x. f x : affine hull f ` s}" unfolding affine_def by(auto simp add: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format]) next interpret f: bounded_linear f by fact - show "affine {x. x : f ` (affine hull s)}" using affine_affine_hull[unfolded affine_def, of s] + show "affine {x. x : f ` (affine hull s)}" using affine_affine_hull[unfolded affine_def, of s] unfolding affine_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric]) qed auto @@ -2703,61 +2703,61 @@ { fix z assume z_def: "z : rel_interior (f ` S)" have "z : f ` S" using z_def rel_interior_subset[of "f ` S"] by auto from this obtain x where x_def: "x : S & (f x = z)" by auto - obtain e2 where e2_def: "e2>0 & cball z e2 Int affine hull (f ` S) <= (f ` S)" + obtain e2 where e2_def: "e2>0 & cball z e2 Int affine hull (f ` S) <= (f ` S)" using z_def rel_interior_cball[of "f ` S"] by auto - obtain K where K_def: "K>0 & (! x. norm (f x) <= norm x * K)" + obtain K where K_def: "K>0 & (! x. norm (f x) <= norm x * K)" using assms RealVector.bounded_linear.pos_bounded[of f] by auto - def e1 == "1/K" hence e1_def: "e1>0 & (! x. e1 * norm (f x) <= norm x)" + def e1 == "1/K" hence e1_def: "e1>0 & (! x. e1 * norm (f x) <= norm x)" using K_def pos_le_divide_eq[of e1] by auto - def e == "e1 * e2" hence "e>0" using e1_def e2_def mult_pos_pos by auto + def e == "e1 * e2" hence "e>0" using e1_def e2_def mult_pos_pos by auto { fix y assume y_def: "y : cball x e Int affine hull S" - from this have h1: "f y : affine hull (f ` S)" - using affine_hull_linear_image[of f S] assms by auto - from y_def have "norm (x-y)<=e1 * e2" + from this have h1: "f y : affine hull (f ` S)" + using affine_hull_linear_image[of f S] assms by auto + from y_def have "norm (x-y)<=e1 * e2" using cball_def[of x e] dist_norm[of x y] e_def by auto moreover have "(f x)-(f y)=f (x-y)" using assms linear_sub[of f x y] linear_conv_bounded_linear[of f] by auto moreover have "e1 * norm (f (x-y)) <= norm (x-y)" using e1_def by auto ultimately have "e1 * norm ((f x)-(f y)) <= e1 * e2" by auto - hence "(f y) : (cball z e2)" + hence "(f y) : (cball z e2)" using cball_def[of "f x" e2] dist_norm[of "f x" "f y"] e1_def x_def by auto hence "f y : (f ` S)" using y_def e2_def h1 by auto - hence "y : S" using assms y_def hull_subset[of S] affine_hull_subset_span + hence "y : S" using assms y_def hull_subset[of S] affine_hull_subset_span inj_on_image_mem_iff[of f "span S" S y] by auto - } + } hence "z : f ` (rel_interior S)" using mem_rel_interior_cball[of x S] `e>0` x_def by auto -} +} moreover { fix x assume x_def: "x : rel_interior S" - from this obtain e2 where e2_def: "e2>0 & cball x e2 Int affine hull S <= S" + from this obtain e2 where e2_def: "e2>0 & cball x e2 Int affine hull S <= S" using rel_interior_cball[of S] by auto have "x : S" using x_def rel_interior_subset by auto hence *: "f x : f ` S" by auto - have "! x:span S. f x = 0 --> x = 0" - using assms subspace_span linear_conv_bounded_linear[of f] + have "! x:span S. f x = 0 --> x = 0" + using assms subspace_span linear_conv_bounded_linear[of f] linear_injective_on_subspace_0[of f "span S"] by auto - from this obtain e1 where e1_def: "e1>0 & (! x : span S. e1 * norm x <= norm (f x))" - using assms injective_imp_isometric[of "span S" f] + from this obtain e1 where e1_def: "e1>0 & (! x : span S. e1 * norm x <= norm (f x))" + using assms injective_imp_isometric[of "span S" f] subspace_span[of S] closed_subspace[of "span S"] by auto - def e == "e1 * e2" hence "e>0" using e1_def e2_def mult_pos_pos by auto + def e == "e1 * e2" hence "e>0" using e1_def e2_def mult_pos_pos by auto { fix y assume y_def: "y : cball (f x) e Int affine hull (f ` S)" - from this have "y : f ` (affine hull S)" using affine_hull_linear_image[of f S] assms by auto + from this have "y : f ` (affine hull S)" using affine_hull_linear_image[of f S] assms by auto from this obtain xy where xy_def: "xy : affine hull S & (f xy = y)" by auto - from this y_def have "norm ((f x)-(f xy))<=e1 * e2" + from this y_def have "norm ((f x)-(f xy))<=e1 * e2" using cball_def[of "f x" e] dist_norm[of "f x" y] e_def by auto moreover have "(f x)-(f xy)=f (x-xy)" using assms linear_sub[of f x xy] linear_conv_bounded_linear[of f] by auto - moreover have "x-xy : span S" - using subspace_sub[of "span S" x xy] subspace_span `x : S` xy_def + moreover have "x-xy : span S" + using subspace_sub[of "span S" x xy] subspace_span `x : S` xy_def affine_hull_subset_span[of S] span_inc by auto moreover hence "e1 * norm (x-xy) <= norm (f (x-xy))" using e1_def by auto ultimately have "e1 * norm (x-xy) <= e1 * e2" by auto hence "xy : (cball x e2)" using cball_def[of x e2] dist_norm[of x xy] e1_def by auto hence "y : (f ` S)" using xy_def e2_def by auto - } - hence "(f x) : rel_interior (f ` S)" + } + hence "(f x) : rel_interior (f ` S)" using mem_rel_interior_cball[of "(f x)" "(f ` S)"] * `e>0` by auto -} +} ultimately show ?thesis by auto qed @@ -2765,7 +2765,7 @@ fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" assumes "bounded_linear f" and "inj f" shows "rel_interior (f ` S) = f ` (rel_interior S)" -using assms rel_interior_injective_on_span_linear_image[of f S] +using assms rel_interior_injective_on_span_linear_image[of f S] subset_inj_on[of f "UNIV" "span S"] by auto subsection{* Some Properties of subset of standard basis *} @@ -2882,7 +2882,7 @@ case False then obtain w where "w\s" by auto show ?thesis unfolding caratheodory[of s] proof(induct ("DIM('a) + 1")) - have *:"{x.\sa. finite sa \ sa \ s \ card sa \ 0 \ x \ convex hull sa} = {}" + have *:"{x.\sa. finite sa \ sa \ s \ card sa \ 0 \ x \ convex hull sa} = {}" using compact_empty by auto case 0 thus ?case unfolding * by simp next @@ -2902,11 +2902,11 @@ next fix x assume "x\s" thus "\t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t" - apply(rule_tac x="{x}" in exI) unfolding convex_hull_singleton by auto + apply(rule_tac x="{x}" in exI) unfolding convex_hull_singleton by auto qed thus ?thesis using assms by simp next case False have "{x. \t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t} = - { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. + { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \ u \ u \ 1 \ x \ s \ y \ {x. \t. finite t \ t \ s \ card t \ n \ x \ convex hull t}}" unfolding set_eq_iff and mem_Collect_eq proof(rule,rule) fix x assume "\u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \ @@ -2943,7 +2943,7 @@ qed qed qed - thus ?thesis using compact_convex_combinations[OF assms Suc] by simp + thus ?thesis using compact_convex_combinations[OF assms Suc] by simp qed qed qed @@ -2955,12 +2955,12 @@ assumes "d \ 0" shows "dist a (b + d) > dist a b \ dist a (b - d) > dist a b" proof(cases "inner a d - inner b d > 0") - case True hence "0 < inner d d + (inner a d * 2 - inner b d * 2)" + case True hence "0 < inner d d + (inner a d * 2 - inner b d * 2)" apply(rule_tac add_pos_pos) using assms by auto thus ?thesis apply(rule_tac disjI2) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff by (simp add: algebra_simps inner_commute) next - case False hence "0 < inner d d + (inner b d * 2 - inner a d * 2)" + case False hence "0 < inner d d + (inner b d * 2 - inner a d * 2)" apply(rule_tac add_pos_nonneg) using assms by auto thus ?thesis apply(rule_tac disjI1) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff by (simp add: algebra_simps inner_commute) @@ -2996,7 +2996,7 @@ next assume "u\0" "v\0" then obtain w where w:"w>0" "wb" proof(rule ccontr) + have "x\b" proof(rule ccontr) assume "\ x\b" hence "y=b" unfolding obt(5) using obt(3) by(auto simp add: scaleR_left_distrib[symmetric]) thus False using obt(4) and False by simp qed @@ -3008,7 +3008,7 @@ unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps) moreover have "(u + w) *\<^sub>R x + (v - w) *\<^sub>R b \ convex hull insert x s" unfolding convex_hull_insert[OF `s\{}`] and mem_Collect_eq - apply(rule_tac x="u + w" in exI) apply rule defer + apply(rule_tac x="u + w" in exI) apply rule defer apply(rule_tac x="v - w" in exI) using `u\0` and w and obt(3,4) by auto ultimately show ?thesis by auto next @@ -3017,7 +3017,7 @@ unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps) moreover have "(u - w) *\<^sub>R x + (v + w) *\<^sub>R b \ convex hull insert x s" unfolding convex_hull_insert[OF `s\{}`] and mem_Collect_eq - apply(rule_tac x="u - w" in exI) apply rule defer + apply(rule_tac x="u - w" in exI) apply rule defer apply(rule_tac x="v + w" in exI) using `u\0` and w and obt(3,4) by auto ultimately show ?thesis by auto qed @@ -3066,7 +3066,7 @@ thus ?thesis using obt(3)[THEN bspec[where x=u], THEN bspec[where x=y]] and obt(1) by (auto simp add: norm_minus_commute) qed auto -qed +qed lemma simplex_extremal_le_exists: fixes s :: "('a::real_inner) set" @@ -3083,7 +3083,7 @@ lemma closest_point_exists: assumes "closed s" "s \ {}" shows "closest_point s a \ s" "\y\s. dist a (closest_point s a) \ dist a y" - unfolding closest_point_def apply(rule_tac[!] someI2_ex) + unfolding closest_point_def apply(rule_tac[!] someI2_ex) using distance_attains_inf[OF assms(1,2), of a] by auto lemma closest_point_in_set: @@ -3096,7 +3096,7 @@ lemma closest_point_self: assumes "x \ s" shows "closest_point s x = x" - unfolding closest_point_def apply(rule some1_equality, rule ex1I[of _ x]) + unfolding closest_point_def apply(rule some1_equality, rule ex1I[of _ x]) using assms by auto lemma closest_point_refl: @@ -3140,7 +3140,7 @@ lemma closest_point_unique: assumes "convex s" "closed s" "x \ s" "\z\s. dist a x \ dist a z" shows "x = closest_point s a" - using any_closest_point_unique[OF assms(1-3) _ assms(4), of "closest_point s a"] + using any_closest_point_unique[OF assms(1-3) _ assms(4), of "closest_point s a"] using closest_point_exists[OF assms(2)] and assms(3) by auto lemma closest_point_dot: @@ -3171,7 +3171,7 @@ lemma continuous_at_closest_point: assumes "convex s" "closed s" "s \ {}" shows "continuous (at x) (closest_point s)" - unfolding continuous_at_eps_delta + unfolding continuous_at_eps_delta using le_less_trans[OF closest_point_lipschitz[OF assms]] by auto lemma continuous_on_closest_point: @@ -3265,7 +3265,7 @@ hence k:"isLub UNIV ((\x. inner a x) ` t) k" unfolding k_def apply(rule_tac Sup) using assms(5) by auto fix x assume "x\t" thus "inner a x < (k + b / 2)" using `0s" + fix x assume "x\s" hence "k \ inner a x - b" unfolding k_def apply(rule_tac Sup_least) using assms(5) using ab[THEN bspec[where x=x]] by auto thus "k + b / 2 < inner a x" using `0 < b` by auto @@ -3308,16 +3308,16 @@ assumes "convex s" "convex (t::('a::euclidean_space) set)" "s \ {}" "t \ {}" "s \ t = {}" shows "\a b. a \ 0 \ (\x\s. inner a x \ b) \