# HG changeset patch # User wenzelm # Date 1348260314 -7200 # Node ID 355f3d076924a8e3cfe0e4a520c1983763ce2759 # Parent 06cb12198b928e52c87302113918c72ceb5c8a25 tuned proofs; diff -r 06cb12198b92 -r 355f3d076924 src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Sep 21 21:24:48 2012 +0200 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Sep 21 22:45:14 2012 +0200 @@ -16,13 +16,14 @@ notation inner (infix "\" 70) lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)" -proof- +proof - have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith thus ?thesis by (simp add: field_simps power2_eq_square) qed lemma square_continuous: "0 < (e::real) ==> \d. 0 < d \ (\y. abs(y - x) < d \ abs(y * y - x * x) < e)" - using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_eq, rule_format, of e x] apply (auto simp add: power2_eq_square) + using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_eq, rule_format, of e x] + apply (auto simp add: power2_eq_square) apply (rule_tac x="s" in exI) apply auto apply (erule_tac x=y in allE) @@ -38,9 +39,10 @@ lemma real_less_rsqrt: "x^2 < y \ x < sqrt y" using real_sqrt_less_mono[of "x^2" y] by simp -lemma sqrt_even_pow2: assumes n: "even n" +lemma sqrt_even_pow2: + assumes n: "even n" shows "sqrt(2 ^ n) = 2 ^ (n div 2)" -proof- +proof - from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex .. from m have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)" by (simp only: power_mult[symmetric] mult_commute) @@ -58,9 +60,8 @@ lemma norm_eq_0_dot: "(norm x = 0) \ (inner x x = (0::real))" by simp (* TODO: delete *) -lemma norm_cauchy_schwarz: +lemma norm_cauchy_schwarz: "inner x y <= norm x * norm y" (* TODO: move to Inner_Product.thy *) - shows "inner x y <= norm x * norm y" using Cauchy_Schwarz_ineq2[of x y] by auto lemma norm_triangle_sub: @@ -75,7 +76,9 @@ by (simp add: norm_eq_sqrt_inner) lemma norm_eq: "norm(x) = norm (y) \ x \ x = y \ y" - apply(subst order_eq_iff) unfolding norm_le by auto + apply (subst order_eq_iff) + apply (auto simp: norm_le) + done lemma norm_eq_1: "norm(x) = 1 \ x \ x = 1" by (simp add: norm_eq_sqrt_inner) @@ -119,7 +122,7 @@ text{* Dot product in terms of the norm rather than conversely. *} lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left -inner_scaleR_left inner_scaleR_right + inner_scaleR_left inner_scaleR_right lemma dot_norm: "x \ y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2" unfolding power2_norm_eq_inner inner_simps inner_commute by auto @@ -144,7 +147,8 @@ shows "norm (y - x1) < e / 2 \ norm (y - x2) < e / 2 \ norm (x1 - x2) < e" using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto -lemma norm_triangle_half_l: assumes "norm (x - y) < e / 2" "norm (x' - (y)) < e / 2" +lemma norm_triangle_half_l: + assumes "norm (x - y) < e / 2" "norm (x' - (y)) < e / 2" shows "norm (x - x') < e" using dist_triangle_half_l[OF assms[unfolded dist_norm[THEN sym]]] unfolding dist_norm[THEN sym] . @@ -157,20 +161,19 @@ lemma setsum_clauses: shows "setsum f {} = 0" - and "finite S \ setsum f (insert x S) = - (if x \ S then setsum f S else f x + setsum f S)" + and "finite S \ setsum f (insert x S) = (if x \ S then setsum f S else f x + setsum f S)" by (auto simp add: insert_absorb) lemma setsum_norm_le: fixes f :: "'a \ 'b::real_normed_vector" assumes fg: "\x \ S. norm (f x) \ g x" shows "norm (setsum f S) \ setsum g S" - by (rule order_trans [OF norm_setsum setsum_mono], simp add: fg) + by (rule order_trans [OF norm_setsum setsum_mono]) (simp add: fg) lemma setsum_norm_bound: fixes f :: "'a \ 'b::real_normed_vector" assumes fS: "finite S" - and K: "\x \ S. norm (f x) \ K" + and K: "\x \ S. norm (f x) \ K" shows "norm (setsum f S) \ of_nat (card S) * K" using setsum_norm_le[OF K] setsum_constant[symmetric] by simp @@ -180,25 +183,27 @@ shows "setsum (\y. setsum g {x. x\ S \ f x = y}) T = setsum g S" apply (subst setsum_image_gen[OF fS, of g f]) apply (rule setsum_mono_zero_right[OF fT fST]) - by (auto intro: setsum_0') + apply (auto intro: setsum_0') + done lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = z" proof assume "\x. x \ y = x \ z" - hence "\x. x \ (y - z) = 0" by (simp add: inner_diff) - hence "(y - z) \ (y - z) = 0" .. + then have "\x. x \ (y - z) = 0" by (simp add: inner_diff) + then have "(y - z) \ (y - z) = 0" .. thus "y = z" by simp qed simp lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = y" proof assume "\z. x \ z = y \ z" - hence "\z. (x - y) \ z = 0" by (simp add: inner_diff) - hence "(x - y) \ (x - y) = 0" .. + then have "\z. (x - y) \ z = 0" by (simp add: inner_diff) + then have "(x - y) \ (x - y) = 0" .. thus "x = y" by simp qed simp -subsection{* Orthogonality. *} + +subsection {* Orthogonality. *} context real_inner begin @@ -223,14 +228,16 @@ lemma orthogonal_commute: "orthogonal x y \ orthogonal y x" by (simp add: orthogonal_def inner_commute) -subsection{* Linear functions. *} - -definition - linear :: "('a::real_vector \ 'b::real_vector) \ bool" where - "linear f \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *\<^sub>R x) = c *\<^sub>R f x)" - -lemma linearI: assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" - shows "linear f" using assms unfolding linear_def by auto + +subsection {* Linear functions. *} + +definition linear :: "('a::real_vector \ 'b::real_vector) \ bool" + where "linear f \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *\<^sub>R x) = c *\<^sub>R f x)" + +lemma linearI: + assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" + shows "linear f" + using assms unfolding linear_def by auto lemma linear_compose_cmul: "linear f ==> linear (\x. c *\<^sub>R f x)" by (simp add: linear_def algebra_simps) @@ -256,7 +263,8 @@ shows "linear(\x. setsum (\a. f a x) S)" using lS apply (induct rule: finite_induct[OF fS]) - by (auto simp add: linear_zero intro: linear_compose_add) + apply (auto simp add: linear_zero intro: linear_compose_add) + done lemma linear_0: "linear f \ f 0 = 0" unfolding linear_def @@ -265,12 +273,14 @@ apply simp done -lemma linear_cmul: "linear f ==> f(c *\<^sub>R x) = c *\<^sub>R f x" by (simp add: linear_def) +lemma linear_cmul: "linear f ==> f(c *\<^sub>R x) = c *\<^sub>R f x" + by (simp add: linear_def) lemma linear_neg: "linear f ==> f (-x) = - f x" using linear_cmul [where c="-1"] by simp -lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def) +lemma linear_add: "linear f ==> f(x + y) = f x + f y" + by (metis linear_def) lemma linear_sub: "linear f ==> f(x - y) = f x - f y" by (simp add: diff_minus linear_add linear_neg) @@ -278,22 +288,24 @@ lemma linear_setsum: assumes lf: "linear f" and fS: "finite S" shows "f (setsum g S) = setsum (f o g) S" -proof (induct rule: finite_induct[OF fS]) - case 1 thus ?case by (simp add: linear_0[OF lf]) + using fS +proof (induct rule: finite_induct) + case empty + then show ?case by (simp add: linear_0[OF lf]) next - case (2 x F) - have "f (setsum g (insert x F)) = f (g x + setsum g F)" using "2.hyps" + case (insert x F) + have "f (setsum g (insert x F)) = f (g x + setsum g F)" using insert.hyps by simp also have "\ = f (g x) + f (setsum g F)" using linear_add[OF lf] by simp - also have "\ = setsum (f o g) (insert x F)" using "2.hyps" by simp + also have "\ = setsum (f o g) (insert x F)" using insert.hyps by simp finally show ?case . qed lemma linear_setsum_mul: assumes lf: "linear f" and fS: "finite S" shows "f (setsum (\i. c i *\<^sub>R v i) S) = setsum (\i. c i *\<^sub>R f (v i)) S" - using linear_setsum[OF lf fS, of "\i. c i *\<^sub>R v i" , unfolded o_def] - linear_cmul[OF lf] by simp + using linear_setsum[OF lf fS, of "\i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lf] + by simp lemma linear_injective_0: assumes lf: "linear f" @@ -307,7 +319,8 @@ finally show ?thesis . qed -subsection{* Bilinear functions. *} + +subsection {* Bilinear functions. *} definition "bilinear f \ (\x. linear(\y. f x y)) \ (\y. linear(\x. f x y))" @@ -333,13 +346,11 @@ lemma bilinear_lzero: assumes bh: "bilinear h" shows "h 0 x = 0" - using bilinear_ladd[OF bh, of 0 0 x] - by (simp add: eq_add_iff field_simps) + using bilinear_ladd[OF bh, of 0 0 x] by (simp add: eq_add_iff field_simps) lemma bilinear_rzero: assumes bh: "bilinear h" shows "h x 0 = 0" - using bilinear_radd[OF bh, of x 0 0 ] - by (simp add: eq_add_iff field_simps) + using bilinear_radd[OF bh, of x 0 0 ] by (simp add: eq_add_iff field_simps) lemma bilinear_lsub: "bilinear h ==> h (x - y) z = h x z - h y z" by (simp add: diff_minus bilinear_ladd bilinear_lneg) @@ -350,25 +361,29 @@ lemma bilinear_setsum: assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T" shows "h (setsum f S) (setsum g T) = setsum (\(i,j). h (f i) (g j)) (S \ T) " -proof- +proof - have "h (setsum f S) (setsum g T) = setsum (\x. h (f x) (setsum g T)) S" apply (rule linear_setsum[unfolded o_def]) - using bh fS by (auto simp add: bilinear_def) + using bh fS apply (auto simp add: bilinear_def) + done also have "\ = setsum (\x. setsum (\y. h (f x) (g y)) T) S" apply (rule setsum_cong, simp) apply (rule linear_setsum[unfolded o_def]) - using bh fT by (auto simp add: bilinear_def) + using bh fT + apply (auto simp add: bilinear_def) + done finally show ?thesis unfolding setsum_cartesian_product . qed -subsection{* Adjoints. *} + +subsection {* Adjoints. *} definition "adjoint f = (SOME f'. \x y. f x \ y = x \ f' y)" lemma adjoint_unique: assumes "\x y. inner (f x) y = inner x (g y)" shows "adjoint f = g" -unfolding adjoint_def + unfolding adjoint_def proof (rule some_equality) show "\x y. inner (f x) y = inner x (g y)" using assms . next @@ -382,7 +397,7 @@ lemma choice_iff: "(\x. \y. P x y) \ (\f. \x. P x (f x))" by metis -subsection{* Interlude: Some properties of real sets *} +subsection {* Interlude: Some properties of real sets *} lemma seq_mono_lemma: assumes "\(n::nat) \ m. (d n :: real) < e n" and "\n \ m. e n <= e m" shows "\n \ m. d n < e m" @@ -399,35 +414,36 @@ using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto lemma approachable_lt_le: "(\(d::real)>0. \x. f x < d \ P x) \ (\d>0. \x. f x \ d \ P x)" -apply auto -apply (rule_tac x="d/2" in exI) -apply auto -done + apply auto + apply (rule_tac x="d/2" in exI) + apply auto + done lemma triangle_lemma: assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2" shows "x <= y + z" -proof- +proof - have "y^2 + z^2 \ y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg) with xy have th: "x ^2 \ (y+z)^2" by (simp add: power2_eq_square field_simps) from y z have yz: "y + z \ 0" by arith from power2_le_imp_le[OF th yz] show ?thesis . qed + subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *} -definition hull :: "('a set \ bool) \ 'a set \ 'a set" (infixl "hull" 75) where - "S hull s = Inter {t. S t \ s \ t}" +definition hull :: "('a set \ bool) \ 'a set \ 'a set" (infixl "hull" 75) + where "S hull s = Inter {t. S t \ s \ t}" lemma hull_same: "S s \ S hull s = s" unfolding hull_def by auto lemma hull_in: "(\T. Ball T S ==> S (Inter T)) ==> S (S hull s)" -unfolding hull_def Ball_def by auto + unfolding hull_def Ball_def by auto lemma hull_eq: "(\T. Ball T S ==> S (Inter T)) ==> (S hull s) = s \ S s" -using hull_same[of S s] hull_in[of S s] by metis + using hull_same[of S s] hull_in[of S s] by metis lemma hull_hull: "S hull (S hull s) = S hull s" @@ -456,27 +472,30 @@ using hull_minimal[of S "{x. P x}" Q] by (auto simp add: subset_eq) -lemma hull_inc: "x \ S \ x \ P hull S" by (metis hull_subset subset_eq) +lemma hull_inc: "x \ S \ x \ P hull S" + by (metis hull_subset subset_eq) lemma hull_union_subset: "(S hull s) \ (S hull t) \ (S hull (s \ t))" -unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2) - -lemma hull_union: assumes T: "\T. Ball T S ==> S (Inter T)" + unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2) + +lemma hull_union: + assumes T: "\T. Ball T S ==> S (Inter T)" shows "S hull (s \ t) = S hull (S hull s \ S hull t)" -apply rule -apply (rule hull_mono) -unfolding Un_subset_iff -apply (metis hull_subset Un_upper1 Un_upper2 subset_trans) -apply (rule hull_minimal) -apply (metis hull_union_subset) -apply (metis hull_in T) -done + apply rule + apply (rule hull_mono) + unfolding Un_subset_iff + apply (metis hull_subset Un_upper1 Un_upper2 subset_trans) + apply (rule hull_minimal) + apply (metis hull_union_subset) + apply (metis hull_in T) + done lemma hull_redundant_eq: "a \ (S hull s) \ (S hull (insert a s) = S hull s)" unfolding hull_def by blast lemma hull_redundant: "a \ (S hull s) ==> (S hull (insert a s) = S hull s)" -by (metis hull_redundant_eq) + by (metis hull_redundant_eq) + subsection {* Archimedean properties and useful consequences *} @@ -492,21 +511,23 @@ done lemma real_pow_lbound: "0 <= x ==> 1 + real n * x <= (1 + x) ^ n" -proof(induct n) - case 0 thus ?case by simp +proof (induct n) + case 0 + then show ?case by simp next case (Suc n) - hence h: "1 + real n * x \ (1 + x) ^ n" by simp + then have h: "1 + real n * x \ (1 + x) ^ n" by simp from h have p: "1 \ (1 + x) ^ n" using Suc.prems by simp from h have "1 + real n * x + x \ (1 + x) ^ n + x" by simp also have "\ \ (1 + x) ^ Suc n" apply (subst diff_le_0_iff_le[symmetric]) apply (simp add: field_simps) - using mult_left_mono[OF p Suc.prems] by simp + using mult_left_mono[OF p Suc.prems] apply simp + done finally show ?case by (simp add: real_of_nat_Suc field_simps) qed lemma real_arch_pow: assumes x: "1 < (x::real)" shows "\n. y < x^n" -proof- +proof - from x have x0: "x - 1 > 0" by arith from reals_Archimedean3[OF x0, rule_format, of y] obtain n::nat where n:"y < real n * (x - 1)" by metis @@ -519,24 +540,30 @@ lemma real_arch_pow2: "\n. (x::real) < 2^ n" using real_arch_pow[of 2 x] by simp -lemma real_arch_pow_inv: assumes y: "(y::real) > 0" and x1: "x < 1" +lemma real_arch_pow_inv: + assumes y: "(y::real) > 0" and x1: "x < 1" shows "\n. x^n < y" -proof- - {assume x0: "x > 0" +proof - + { assume x0: "x > 0" from x0 x1 have ix: "1 < 1/x" by (simp add: field_simps) from real_arch_pow[OF ix, of "1/y"] obtain n where n: "1/y < (1/x)^n" by blast - then - have ?thesis using y x0 by (auto simp add: field_simps power_divide) } + then have ?thesis using y x0 + by (auto simp add: field_simps power_divide) } moreover - {assume "\ x > 0" with y x1 have ?thesis apply auto by (rule exI[where x=1], auto)} + { assume "\ x > 0" + with y x1 have ?thesis apply auto by (rule exI[where x=1], auto) } ultimately show ?thesis by metis qed -lemma forall_pos_mono: "(\d e::real. d < e \ P d ==> P e) \ (\n::nat. n \ 0 ==> P(inverse(real n))) \ (\e. 0 < e ==> P e)" +lemma forall_pos_mono: + "(\d e::real. d < e \ P d ==> P e) \ + (\n::nat. n \ 0 ==> P(inverse(real n))) \ (\e. 0 < e ==> P e)" by (metis real_arch_inv) -lemma forall_pos_mono_1: "(\d e::real. d < e \ P d ==> P e) \ (\n. P(inverse(real (Suc n)))) ==> 0 < e ==> P e" +lemma forall_pos_mono_1: + "(\d e::real. d < e \ P d ==> P e) \ + (\n. P(inverse(real (Suc n)))) ==> 0 < e ==> P e" apply (rule forall_pos_mono) apply auto apply (atomize) @@ -544,22 +571,23 @@ apply auto done -lemma real_archimedian_rdiv_eq_0: assumes x0: "x \ 0" and c: "c \ 0" and xc: "\(m::nat)>0. real m * x \ c" +lemma real_archimedian_rdiv_eq_0: + assumes x0: "x \ 0" and c: "c \ 0" and xc: "\(m::nat)>0. real m * x \ c" shows "x = 0" -proof- - {assume "x \ 0" with x0 have xp: "x > 0" by arith +proof - + { assume "x \ 0" with x0 have xp: "x > 0" by arith from reals_Archimedean3[OF xp, rule_format, of c] obtain n::nat where n: "c < real n * x" by blast with xc[rule_format, of n] have "n = 0" by arith - with n c have False by simp} + with n c have False by simp } then show ?thesis by blast qed + subsection{* A bit of linear algebra. *} -definition (in real_vector) - subspace :: "'a set \ bool" where - "subspace S \ 0 \ S \ (\x\ S. \y \S. x + y \ S) \ (\c. \x \S. c *\<^sub>R x \S )" +definition (in real_vector) subspace :: "'a set \ bool" + where "subspace S \ 0 \ S \ (\x\ S. \y \S. x + y \ S) \ (\c. \x \S. c *\<^sub>R x \S )" definition (in real_vector) "span S = (subspace hull S)" definition (in real_vector) "dependent S \ (\a \ S. a \ span(S - {a}))" @@ -585,11 +613,11 @@ lemma (in real_vector) subspace_setsum: assumes sA: "subspace A" and fB: "finite B" - and f: "\x\ B. f x \ A" + and f: "\x\ B. f x \ A" shows "setsum f B \ A" using fB f sA - apply(induct rule: finite_induct[OF fB]) - by (simp add: subspace_def sA, auto simp add: sA subspace_add) + by (induct rule: finite_induct[OF fB]) + (simp add: subspace_def sA, auto simp add: sA subspace_add) lemma subspace_linear_image: assumes lf: "linear f" and sS: "subspace S" @@ -637,16 +665,18 @@ (metis subspace_span subspace_def)+ lemma span_unique: - "\S \ T; subspace T; \T'. \S \ T'; subspace T'\ \ T \ T'\ \ span S = T" + "S \ T \ subspace T \ (\T'. S \ T' \ subspace T' \ T \ T') \ span S = T" unfolding span_def by (rule hull_unique) lemma span_minimal: "S \ T \ subspace T \ span S \ T" unfolding span_def by (rule hull_minimal) lemma (in real_vector) span_induct: - assumes x: "x \ span S" and P: "subspace P" and SP: "\x. x \ S ==> x \ P" + assumes x: "x \ span S" + and P: "subspace P" + and SP: "\x. x \ S ==> x \ P" shows "x \ P" -proof- +proof - from SP have SP': "S \ P" by (simp add: subset_eq) from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]] show "x \ P" by (metis subset_eq) @@ -661,8 +691,7 @@ lemma (in real_vector) independent_empty[intro]: "independent {}" by (simp add: dependent_def) -lemma dependent_single[simp]: - "dependent {x} \ x = 0" +lemma dependent_single[simp]: "dependent {x} \ x = 0" unfolding dependent_def by auto lemma (in real_vector) independent_mono: "independent A \ B \ A ==> independent B" @@ -683,61 +712,63 @@ inductive_set (in real_vector) span_induct_alt_help for S:: "'a set" where span_induct_alt_help_0: "0 \ span_induct_alt_help S" - | span_induct_alt_help_S: "x \ S \ z \ span_induct_alt_help S \ (c *\<^sub>R x + z) \ span_induct_alt_help S" +| span_induct_alt_help_S: + "x \ S \ z \ span_induct_alt_help S \ (c *\<^sub>R x + z) \ span_induct_alt_help S" lemma span_induct_alt': - assumes h0: "h 0" and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" shows "\x \ span S. h x" -proof- - {fix x:: "'a" assume x: "x \ span_induct_alt_help S" + assumes h0: "h 0" and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" + shows "\x \ span S. h x" +proof - + { fix x:: "'a" assume x: "x \ span_induct_alt_help S" have "h x" apply (rule span_induct_alt_help.induct[OF x]) apply (rule h0) apply (rule hS, assumption, assumption) - done} + done } note th0 = this - {fix x assume x: "x \ span S" - + { fix x assume x: "x \ span S" have "x \ span_induct_alt_help S" - proof(rule span_induct[where x=x and S=S]) - show "x \ span S" using x . - next - fix x assume xS : "x \ S" - from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1] - show "x \ span_induct_alt_help S" by simp - next - have "0 \ span_induct_alt_help S" by (rule span_induct_alt_help_0) - moreover - {fix x y assume h: "x \ span_induct_alt_help S" "y \ span_induct_alt_help S" - from h - have "(x + y) \ span_induct_alt_help S" - apply (induct rule: span_induct_alt_help.induct) - apply simp - unfolding add_assoc - apply (rule span_induct_alt_help_S) - apply assumption - apply simp - done} - moreover - {fix c x assume xt: "x \ span_induct_alt_help S" - then have "(c *\<^sub>R x) \ span_induct_alt_help S" - apply (induct rule: span_induct_alt_help.induct) - apply (simp add: span_induct_alt_help_0) - apply (simp add: scaleR_right_distrib) - apply (rule span_induct_alt_help_S) - apply assumption - apply simp - done - } - ultimately show "subspace (span_induct_alt_help S)" - unfolding subspace_def Ball_def by blast - qed} + proof (rule span_induct[where x=x and S=S]) + show "x \ span S" using x . + next + fix x assume xS : "x \ S" + from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1] + show "x \ span_induct_alt_help S" by simp + next + have "0 \ span_induct_alt_help S" by (rule span_induct_alt_help_0) + moreover + { fix x y + assume h: "x \ span_induct_alt_help S" "y \ span_induct_alt_help S" + from h have "(x + y) \ span_induct_alt_help S" + apply (induct rule: span_induct_alt_help.induct) + apply simp + unfolding add_assoc + apply (rule span_induct_alt_help_S) + apply assumption + apply simp + done } + moreover + { fix c x + assume xt: "x \ span_induct_alt_help S" + then have "(c *\<^sub>R x) \ span_induct_alt_help S" + apply (induct rule: span_induct_alt_help.induct) + apply (simp add: span_induct_alt_help_0) + apply (simp add: scaleR_right_distrib) + apply (rule span_induct_alt_help_S) + apply assumption + apply simp + done } + ultimately + show "subspace (span_induct_alt_help S)" + unfolding subspace_def Ball_def by blast + qed } with th0 show ?thesis by blast qed lemma span_induct_alt: assumes h0: "h 0" and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" and x: "x \ span S" shows "h x" -using span_induct_alt'[of h S] h0 hS x by blast + using span_induct_alt'[of h S] h0 hS x by blast text {* Individual closure properties. *} @@ -773,7 +804,8 @@ lemma span_add_eq: "x \ span S \ x + y \ span S \ y \ span S" apply (auto simp only: span_add span_sub) apply (subgoal_tac "(x + y) - x \ span S", simp) - by (simp only: span_add span_sub) + apply (simp only: span_add span_sub) + done text {* Mapping under linear image. *} @@ -789,7 +821,8 @@ show "subspace (f ` span S)" using lf subspace_span by (rule subspace_linear_image) next - fix T assume "f ` S \ T" and "subspace T" thus "f ` span S \ T" + fix T assume "f ` S \ T" and "subspace T" + then show "f ` span S \ T" unfolding image_subset_iff_subset_vimage by (intro span_minimal subspace_linear_vimage lf) qed @@ -807,7 +840,7 @@ by (rule subspace_linear_image) next fix T assume "A \ B \ T" and "subspace T" - thus "(\(a, b). a + b) ` (span A \ span B) \ T" + then show "(\(a, b). a + b) ` (span A \ span B) \ T" by (auto intro!: subspace_add elim: span_induct) qed @@ -824,8 +857,7 @@ unfolding subspace_def by auto qed -lemma span_insert: - "span (insert a S) = {x. \k. (x - k *\<^sub>R a) \ span S}" +lemma span_insert: "span (insert a S) = {x. \k. (x - k *\<^sub>R a) \ span S}" proof - have "span ({a} \ S) = {x. \k. (x - k *\<^sub>R a) \ span S}" unfolding span_union span_singleton @@ -835,7 +867,7 @@ apply simp apply (rule right_minus) done - thus ?thesis by simp + then show ?thesis by simp qed lemma span_breakdown: @@ -844,8 +876,7 @@ using assms span_insert [of b "S - {b}"] by (simp add: insert_absorb) -lemma span_breakdown_eq: - "x \ span (insert a S) \ (\k. (x - k *\<^sub>R a) \ span S)" +lemma span_breakdown_eq: "x \ span (insert a S) \ (\k. (x - k *\<^sub>R a) \ span S)" by (simp add: span_insert) text {* Hence some "reversal" results. *} @@ -856,7 +887,7 @@ proof- from span_breakdown[of b "insert b S" a, OF insertI1 a] obtain k where k: "a - k*\<^sub>R b \ span (S - {b})" by auto - {assume k0: "k = 0" + { assume k0: "k = 0" with k have "a \ span S" apply (simp) apply (rule set_rev_mp) @@ -864,9 +895,9 @@ apply (rule span_mono) apply blast done - with na have ?thesis by blast} + with na have ?thesis by blast } moreover - {assume k0: "k \ 0" + { assume k0: "k \ 0" have eq: "b = (1/k) *\<^sub>R a - ((1/k) *\<^sub>R a - b)" by simp from k0 have eq': "(1/k) *\<^sub>R (a - k*\<^sub>R b) = (1/k) *\<^sub>R a - b" by (simp add: algebra_simps) @@ -885,13 +916,13 @@ apply (rule set_rev_mp) apply (rule th) apply (rule span_mono) - using na by blast} + using na by blast } ultimately show ?thesis by blast qed lemma in_span_delete: assumes a: "a \ span S" - and na: "a \ span (S-{b})" + and na: "a \ span (S-{b})" shows "b \ span (insert a (S - {b}))" apply (rule in_span_insert) apply (rule set_rev_mp) @@ -920,30 +951,32 @@ "span P = {y. \S u. finite S \ S \ P \ setsum (\v. u v *\<^sub>R v) S = y}" (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \S u. ?Q S u y}") proof- - {fix x assume x: "x \ ?E" + { fix x assume x: "x \ ?E" then obtain S u where fS: "finite S" and SP: "S\P" and u: "setsum (\v. u v *\<^sub>R v) S = x" by blast have "x \ span P" unfolding u[symmetric] apply (rule span_setsum[OF fS]) using span_mono[OF SP] - by (auto intro: span_superset span_mul)} + apply (auto intro: span_superset span_mul) + done } moreover have "\x \ span P. x \ ?E" - proof(rule span_induct_alt') + proof (rule span_induct_alt') show "0 \ Collect ?h" unfolding mem_Collect_eq - apply (rule exI[where x="{}"]) by simp + apply (rule exI[where x="{}"]) + apply simp + done next fix c x y assume x: "x \ P" and hy: "y \ Collect ?h" from hy obtain S u where fS: "finite S" and SP: "S\P" and u: "setsum (\v. u v *\<^sub>R v) S = y" by blast let ?S = "insert x S" - let ?u = "\y. if y = x then (if x \ S then u y + c else c) - else u y" + let ?u = "\y. if y = x then (if x \ S then u y + c else c) else u y" from fS SP x have th0: "finite (insert x S)" "insert x S \ P" by blast+ - {assume xS: "x \ S" + { assume xS: "x \ S" have S1: "S = (S - {x}) \ {x}" and Sss:"finite (S - {x})" "finite {x}" "(S -{x}) \ {x} = {}" using xS fS by auto have "setsum (\v. ?u v *\<^sub>R v) ?S =(\v\S - {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x" @@ -952,34 +985,38 @@ setsum_clauses(2)[OF fS] cong del: if_weak_cong) also have "\ = (\v\S. u v *\<^sub>R v) + c *\<^sub>R x" apply (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]]) - by (simp add: algebra_simps) + apply (simp add: algebra_simps) + done also have "\ = c*\<^sub>R x + y" by (simp add: add_commute u) finally have "setsum (\v. ?u v *\<^sub>R v) ?S = c*\<^sub>R x + y" . - then have "?Q ?S ?u (c*\<^sub>R x + y)" using th0 by blast} - moreover - {assume xS: "x \ S" - have th00: "(\v\S. (if v = x then c else u v) *\<^sub>R v) = y" - unfolding u[symmetric] - apply (rule setsum_cong2) - using xS by auto - have "?Q ?S ?u (c*\<^sub>R x + y)" using fS xS th0 - by (simp add: th00 setsum_clauses add_commute cong del: if_weak_cong)} - ultimately have "?Q ?S ?u (c*\<^sub>R x + y)" - by (cases "x \ S", simp, simp) + then have "?Q ?S ?u (c*\<^sub>R x + y)" using th0 by blast } + moreover + { assume xS: "x \ S" + have th00: "(\v\S. (if v = x then c else u v) *\<^sub>R v) = y" + unfolding u[symmetric] + apply (rule setsum_cong2) + using xS apply auto + done + have "?Q ?S ?u (c*\<^sub>R x + y)" using fS xS th0 + by (simp add: th00 setsum_clauses add_commute cong del: if_weak_cong) } + ultimately have "?Q ?S ?u (c*\<^sub>R x + y)" by (cases "x \ S") simp_all then show "(c*\<^sub>R x + y) \ Collect ?h" unfolding mem_Collect_eq apply - apply (rule exI[where x="?S"]) - apply (rule exI[where x="?u"]) by metis + apply (rule exI[where x="?u"]) + apply metis + done qed ultimately show ?thesis by blast qed lemma dependent_explicit: - "dependent P \ (\S u. finite S \ S \ P \ (\v\S. u v \ 0 \ setsum (\v. u v *\<^sub>R v) S = 0))" (is "?lhs = ?rhs") -proof- - {assume dP: "dependent P" + "dependent P \ (\S u. finite S \ S \ P \ (\v\S. u v \ 0 \ setsum (\v. u v *\<^sub>R v) S = 0))" + (is "?lhs = ?rhs") +proof - + { assume dP: "dependent P" then obtain a S u where aP: "a \ P" and fS: "finite S" and SP: "S \ P - {a}" and ua: "setsum (\v. u v *\<^sub>R v) S = a" unfolding dependent_def span_explicit by blast @@ -993,26 +1030,27 @@ apply (simp add: setsum_clauses field_simps) apply (subst (2) ua[symmetric]) apply (rule setsum_cong2) - by auto + apply auto + done with th0 have ?rhs apply - apply (rule exI[where x= "?S"]) apply (rule exI[where x= "?u"]) - by clarsimp} + apply auto + done + } moreover - {fix S u v assume fS: "finite S" + { fix S u v + assume fS: "finite S" and SP: "S \ P" and vS: "v \ S" and uv: "u v \ 0" - and u: "setsum (\v. u v *\<^sub>R v) S = 0" + and u: "setsum (\v. u v *\<^sub>R v) S = 0" let ?a = v let ?S = "S - {v}" let ?u = "\i. (- u i) / u v" - have th0: "?a \ P" "finite ?S" "?S \ P" using fS SP vS by auto + have th0: "?a \ P" "finite ?S" "?S \ P" using fS SP vS by auto have "setsum (\v. ?u v *\<^sub>R v) ?S = setsum (\v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v" - using fS vS uv - by (simp add: setsum_diff1 divide_inverse field_simps) - also have "\ = ?a" - unfolding scaleR_right.setsum [symmetric] u - using uv by simp + using fS vS uv by (simp add: setsum_diff1 divide_inverse field_simps) + also have "\ = ?a" unfolding scaleR_right.setsum [symmetric] u using uv by simp finally have "setsum (\v. ?u v *\<^sub>R v) ?S = ?a" . with th0 have ?lhs unfolding dependent_def span_explicit @@ -1020,7 +1058,9 @@ apply (rule bexI[where x= "?a"]) apply (simp_all del: scaleR_minus_left) apply (rule exI[where x= "?S"]) - by (auto simp del: scaleR_minus_left)} + apply (auto simp del: scaleR_minus_left) + done + } ultimately show ?thesis by blast qed @@ -1029,18 +1069,19 @@ assumes fS: "finite S" shows "span S = {y. \u. setsum (\v. u v *\<^sub>R v) S = y}" (is "_ = ?rhs") -proof- - {fix y assume y: "y \ span S" +proof - + { fix y assume y: "y \ span S" from y obtain S' u where fS': "finite S'" and SS': "S' \ S" and u: "setsum (\v. u v *\<^sub>R v) S' = y" unfolding span_explicit by blast let ?u = "\x. if x \ S' then u x else 0" have "setsum (\v. ?u v *\<^sub>R v) S = setsum (\v. u v *\<^sub>R v) S'" using SS' fS by (auto intro!: setsum_mono_zero_cong_right) - hence "setsum (\v. ?u v *\<^sub>R v) S = y" by (metis u) - hence "y \ ?rhs" by auto} + then have "setsum (\v. ?u v *\<^sub>R v) S = y" by (metis u) + then have "y \ ?rhs" by auto } moreover - {fix y u assume u: "setsum (\v. u v *\<^sub>R v) S = y" - then have "y \ span S" using fS unfolding span_explicit by auto} + { fix y u + assume u: "setsum (\v. u v *\<^sub>R v) S = y" + then have "y \ span S" using fS unfolding span_explicit by auto } ultimately show ?thesis by blast qed @@ -1050,21 +1091,22 @@ "independent(insert a S) \ (if a \ S then independent S else independent S \ a \ span S)" (is "?lhs \ ?rhs") -proof- - {assume aS: "a \ S" - hence ?thesis using insert_absorb[OF aS] by simp} +proof - + { assume aS: "a \ S" + then have ?thesis using insert_absorb[OF aS] by simp } moreover - {assume aS: "a \ S" - {assume i: ?lhs + { assume aS: "a \ S" + { assume i: ?lhs then have ?rhs using aS apply simp apply (rule conjI) apply (rule independent_mono) apply assumption apply blast - by (simp add: dependent_def)} + apply (simp add: dependent_def) + done } moreover - {assume i: ?rhs + { assume i: ?rhs have ?lhs using i aS apply simp apply (auto simp add: dependent_def) @@ -1079,8 +1121,8 @@ apply assumption apply blast apply blast - done} - ultimately have ?thesis by blast} + done } + ultimately have ?thesis by blast } ultimately show ?thesis by blast qed @@ -1091,7 +1133,7 @@ lemma spanning_subset_independent: assumes BA: "B \ A" and iA: "independent A" - and AsB: "A \ span B" + and AsB: "A \ span B" shows "A = B" proof from BA show "B \ A" . @@ -1099,18 +1141,18 @@ from span_mono[OF BA] span_mono[OF AsB] have sAB: "span A = span B" unfolding span_span by blast - {fix x assume x: "x \ A" + { fix x assume x: "x \ A" from iA have th0: "x \ span (A - {x})" unfolding dependent_def using x by blast from x have xsA: "x \ span A" by (blast intro: span_superset) have "A - {x} \ A" by blast hence th1:"span (A - {x}) \ span A" by (metis span_mono) - {assume xB: "x \ B" + { assume xB: "x \ B" from xB BA have "B \ A -{x}" by blast hence "span B \ span (A - {x})" by (metis span_mono) with th1 th0 sAB have "x \ span A" by blast - with x have False by (metis span_superset)} - then have "x \ B" by blast} + with x have False by (metis span_superset) } + then have "x \ B" by blast } then show "A \ B" by blast qed @@ -1118,76 +1160,77 @@ lemma exchange_lemma: assumes f:"finite t" and i: "independent s" - and sp:"s \ span t" + and sp:"s \ span t" shows "\t'. (card t' = card t) \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" using f i sp -proof(induct "card (t - s)" arbitrary: s t rule: less_induct) +proof (induct "card (t - s)" arbitrary: s t rule: less_induct) case less note ft = `finite t` and s = `independent s` and sp = `s \ span t` let ?P = "\t'. (card t' = card t) \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" let ?ths = "\t'. ?P t'" - {assume st: "s \ t" + { assume st: "s \ t" from st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t]) - by (auto intro: span_superset)} + apply (auto intro: span_superset) + done } moreover - {assume st: "t \ s" + { assume st: "t \ s" from spanning_subset_independent[OF st s sp] st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t]) - by (auto intro: span_superset)} + apply (auto intro: span_superset) + done } moreover - {assume st: "\ s \ t" "\ t \ s" + { assume st: "\ s \ t" "\ t \ s" from st(2) obtain b where b: "b \ t" "b \ s" by blast from b have "t - {b} - s \ t - s" by blast then have cardlt: "card (t - {b} - s) < card (t - s)" using ft by (auto intro: psubset_card_mono) from b ft have ct0: "card t \ 0" by auto - {assume stb: "s \ span(t -{b})" + { assume stb: "s \ span(t -{b})" from ft have ftb: "finite (t -{b})" by auto from less(1)[OF cardlt ftb s stb] - obtain u where u: "card u = card (t-{b})" "s \ u" "u \ s \ (t - {b})" "s \ span u" and fu: "finite u" by blast + obtain u where u: "card u = card (t-{b})" "s \ u" "u \ s \ (t - {b})" "s \ span u" + and fu: "finite u" by blast let ?w = "insert b u" have th0: "s \ insert b u" using u by blast from u(3) b have "u \ s \ t" by blast then have th1: "insert b u \ s \ t" using u b by blast have bu: "b \ u" using b u by blast from u(1) ft b have "card u = (card t - 1)" by auto - then - have th2: "card (insert b u) = card t" + then have th2: "card (insert b u) = card t" using card_insert_disjoint[OF fu bu] ct0 by auto from u(4) have "s \ span u" . also have "\ \ span (insert b u)" apply (rule span_mono) by blast finally have th3: "s \ span (insert b u)" . from th0 th1 th2 th3 fu have th: "?P ?w" by blast - from th have ?ths by blast} + from th have ?ths by blast } moreover - {assume stb: "\ s \ span(t -{b})" + { assume stb: "\ s \ span(t -{b})" from stb obtain a where a: "a \ s" "a \ span (t - {b})" by blast have ab: "a \ b" using a b by blast have at: "a \ t" using a ab span_superset[of a "t- {b}"] by auto have mlt: "card ((insert a (t - {b})) - s) < card (t - s)" using cardlt ft a b by auto have ft': "finite (insert a (t - {b}))" using ft by auto - {fix x assume xs: "x \ s" + { fix x assume xs: "x \ s" have t: "t \ (insert b (insert a (t -{b})))" using b by auto from b(1) have "b \ span t" by (simp add: span_superset) have bs: "b \ span (insert a (t - {b}))" apply(rule in_span_delete) - using a sp unfolding subset_eq by auto + using a sp unfolding subset_eq apply auto done from xs sp have "x \ span t" by blast with span_mono[OF t] have x: "x \ span (insert b (insert a (t - {b})))" .. - from span_trans[OF bs x] have "x \ span (insert a (t - {b}))" .} + from span_trans[OF bs x] have "x \ span (insert a (t - {b}))" . } then have sp': "s \ span (insert a (t - {b}))" by blast from less(1)[OF mlt ft' s sp'] obtain u where u: "card u = card (insert a (t -{b}))" "finite u" "s \ u" "u \ s \ insert a (t -{b})" - "s \ span u" by blast + "s \ span u" by blast from u a b ft at ct0 have "?P u" by auto then have ?ths by blast } ultimately have ?ths by blast } - ultimately - show ?ths by blast + ultimately show ?ths by blast qed text {* This implies corresponding size bounds. *} @@ -1199,7 +1242,7 @@ lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\ (UNIV::'a::finite set)}" -proof- +proof - have eq: "{f x |x. x\ UNIV} = f ` UNIV" by auto show ?thesis unfolding eq apply (rule finite_imageI) @@ -1210,7 +1253,8 @@ subsection{* Euclidean Spaces as Typeclass*} lemma independent_eq_inj_on: - fixes D :: nat and f :: "nat \ 'c::real_vector" assumes *: "inj_on f {.. 'c::real_vector" + assumes *: "inj_on f {.. (\a u. a < D \ (\i\{..R f i) \ f a)" proof - from * have eq: "\i. i < D \ f ` {..iR basis i) \ span (range basis :: 'a set)" by (simp add: span_setsum span_mul span_superset) - hence "x \ span (range basis)" + then have "x \ span (range basis)" by (simp only: euclidean_representation [symmetric]) - } thus ?thesis by auto + } then show ?thesis by auto qed lemma basis_representation: @@ -1256,14 +1300,14 @@ have "x\UNIV" by auto from this[unfolded span_basis[THEN sym]] have "\u. (\v\basis ` {..R v) = x" unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto - thus ?thesis by fastforce + then show ?thesis by fastforce qed lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..'a) ` {.. span (basis ` {.. (\ix $$ i\)" apply (subst euclidean_representation[of x]) apply (rule order_trans[OF norm_setsum]) - by (auto intro!: setsum_mono) + apply (auto intro!: setsum_mono) + done lemma setsum_norm_allsubsets_bound: fixes f:: "'a \ 'n::euclidean_space" assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (setsum f Q) \ e" shows "setsum (\x. norm (f x)) P \ 2 * real DIM('n) * e" -proof- +proof - let ?d = "real DIM('n)" let ?nf = "\x. norm (f x)" let ?U = "{.. \ 2 * ?d * e" unfolding th0 th1 - proof(rule setsum_bounded) + proof (rule setsum_bounded) fix i assume i: "i \ ?U" let ?Pp = "{x. x\ P \ f x $$ i \ 0}" let ?Pn = "{x. x \ P \ f x $$ i < 0}" @@ -1310,7 +1355,8 @@ have "setsum (\x. \f x $$ i\) P = setsum (\x. \f x $$ i\) ?Pp + setsum (\x. \f x $$ i\) ?Pn" apply (subst thp) apply (rule setsum_Un_zero) - using fP thp0 by auto + using fP thp0 apply auto + done also have "\ \ 2*e" using Pne Ppe by arith finally show "setsum (\x. \f x $$ i\) P \ 2*e" . qed @@ -1323,46 +1369,48 @@ (\x::'a. \i ?rhs") proof- let ?S = "{..iii 'b::real_normed_vector" assumes lf: "linear f" shows "\B. \x. norm (f x) \ B * norm x" -proof- +proof - let ?S = "{..i. (x$$i) *\<^sub>R (basis i)) ?S))" - apply(subst euclidean_representation[of x]) .. + apply(subst euclidean_representation[of x]) apply rule done also have "\ = norm (setsum (\ i. (x$$i) *\<^sub>R f (basis i)) ?S)" using linear_setsum[OF lf fS, of ?g, unfolded o_def] linear_cmul[OF lf] by auto finally have th0: "norm (f x) = norm (setsum (\i. (x$$i) *\<^sub>R f (basis i))?S)" . - {fix i assume i: "i \ ?S" + { fix i assume i: "i \ ?S" from component_le_norm[of x i] have "norm ((x$$i) *\<^sub>R f (basis i :: 'a)) \ norm (f (basis i)) * norm x" unfolding norm_scaleR apply (simp only: mult_commute) apply (rule mult_mono) - by (auto simp add: field_simps) } - then have th: "\i\ ?S. norm ((x$$i) *\<^sub>R f (basis i :: 'a)) \ norm (f (basis i)) * norm x" by metis + apply (auto simp add: field_simps) + done } + then have th: "\i\ ?S. norm ((x$$i) *\<^sub>R f (basis i :: 'a)) \ norm (f (basis i)) * norm x" + by metis from setsum_norm_le[of _ "\i. (x$$i) *\<^sub>R (f (basis i))", OF th] have "norm (f x) \ ?B * norm x" unfolding th0 setsum_left_distrib by metis} then show ?thesis by blast @@ -1380,13 +1428,13 @@ { assume C: "B < 0" have "((\\ i. 1)::'a) \ 0" unfolding euclidean_eq[where 'a='a] by(auto intro!:exI[where x=0]) - hence "norm ((\\ i. 1)::'a) > 0" by auto + then have "norm ((\\ i. 1)::'a) > 0" by auto with C have "B * norm ((\\ i. 1)::'a) < 0" by (simp add: mult_less_0_iff) with B[rule_format, of "(\\ i. 1)::'a"] norm_ge_zero[of "f ((\\ i. 1)::'a)"] have False by simp } then have Bp: "B \ 0" by (metis not_leE) - {fix x::"'a" + { fix x::"'a" have "norm (f x) \ ?K * norm x" using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp apply (auto simp add: field_simps split add: abs_split) @@ -1411,7 +1459,7 @@ next have "\B. \x. norm (f x) \ B * norm x" using `linear f` by (rule linear_bounded) - thus "\K. \x. norm (f x) \ norm x * K" + then show "\K. \x. norm (f x) \ norm x * K" by (simp add: mult_commute) qed next @@ -1421,25 +1469,29 @@ by (simp add: f.add f.scaleR linear_def) qed -lemma bounded_linearI': fixes f::"'a::euclidean_space \ 'b::real_normed_vector" +lemma bounded_linearI': + fixes f::"'a::euclidean_space \ 'b::real_normed_vector" assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" - shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym] - by(rule linearI[OF assms]) + shows "bounded_linear f" + unfolding linear_conv_bounded_linear[THEN sym] + by (rule linearI[OF assms]) lemma bilinear_bounded: fixes h:: "'m::euclidean_space \ 'n::euclidean_space \ 'k::real_normed_vector" assumes bh: "bilinear h" shows "\B. \x y. norm (h x y) \ B * norm x * norm y" -proof- +proof - let ?M = "{..i. (x$$i) *\<^sub>R basis i) ?M) (setsum (\i. (y$$i) *\<^sub>R basis i) ?N))" apply(subst euclidean_representation[where 'a='m]) - apply(subst euclidean_representation[where 'a='n]) .. + apply(subst euclidean_representation[where 'a='n]) + apply rule + done also have "\ = norm (setsum (\ (i,j). h ((x$$i) *\<^sub>R basis i) ((y$$j) *\<^sub>R basis j)) (?M \ ?N))" unfolding bilinear_setsum[OF bh fM fN] .. finally have th: "norm (h x y) = \" . @@ -1453,7 +1505,7 @@ apply (auto simp add: zero_le_mult_iff component_le_norm) apply (rule mult_mono) apply (auto simp add: zero_le_mult_iff component_le_norm) - done} + done } then show ?thesis by metis qed @@ -1461,20 +1513,21 @@ fixes h:: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" assumes bh: "bilinear h" shows "\B > 0. \x y. norm (h x y) \ B * norm x * norm y" -proof- +proof - from bilinear_bounded[OF bh] obtain B where B: "\x y. norm (h x y) \ B * norm x * norm y" by blast let ?K = "\B\ + 1" have Kp: "?K > 0" by arith have KB: "B < ?K" by arith - {fix x::'a and y::'b + { fix x::'a and y::'b from KB Kp have "B * norm x * norm y \ ?K * norm x * norm y" apply - apply (rule mult_right_mono, rule mult_right_mono) - by auto + apply auto + done then have "norm (h x y) \ ?K * norm x * norm y" - using B[rule_format, of x y] by simp} + using B[rule_format, of x y] by simp } with Kp show ?thesis by blast qed @@ -1501,7 +1554,7 @@ next have "\B. \x y. norm (h x y) \ B * norm x * norm y" using `bilinear h` by (rule bilinear_bounded) - thus "\K. \x y. norm (h x y) \ norm x * norm y * K" + then show "\K. \x y. norm (h x y) \ norm x * norm y * K" by (simp add: mult_ac) qed next @@ -1509,10 +1562,10 @@ then interpret h: bounded_bilinear h . show "bilinear h" unfolding bilinear_def linear_conv_bounded_linear - using h.bounded_linear_left h.bounded_linear_right - by simp + using h.bounded_linear_left h.bounded_linear_right by simp qed + subsection {* We continue. *} lemma independent_bound: @@ -1529,51 +1582,53 @@ assumes sv: "(S::('a::euclidean_space) set) \ V" and iS: "independent S" shows "\B. S \ B \ B \ V \ independent B \ V \ span B" using sv iS -proof(induct "DIM('a) - card S" arbitrary: S rule: less_induct) +proof (induct "DIM('a) - card S" arbitrary: S rule: less_induct) case less note sv = `S \ V` and i = `independent S` let ?P = "\B. S \ B \ B \ V \ independent B \ V \ span B" let ?ths = "\x. ?P x" let ?d = "DIM('a)" - {assume "V \ span S" + { assume "V \ span S" then have ?ths using sv i by blast } moreover - {assume VS: "\ V \ span S" + { assume VS: "\ V \ span S" from VS obtain a where a: "a \ V" "a \ span S" by blast from a have aS: "a \ S" by (auto simp add: span_superset) have th0: "insert a S \ V" using a sv by blast from independent_insert[of a S] i a have th1: "independent (insert a S)" by auto have mlt: "?d - card (insert a S) < ?d - card S" - using aS a independent_bound[OF th1] - by auto + using aS a independent_bound[OF th1] by auto from less(1)[OF mlt th0 th1] obtain B where B: "insert a S \ B" "B \ V" "independent B" " V \ span B" by blast from B have "?P B" by auto - then have ?ths by blast} + then have ?ths by blast } ultimately show ?ths by blast qed lemma maximal_independent_subset: "\(B:: ('a::euclidean_space) set). B\ V \ independent B \ V \ span B" - by (metis maximal_independent_subset_extend[of "{}:: ('a::euclidean_space) set"] empty_subsetI independent_empty) + by (metis maximal_independent_subset_extend[of "{}:: ('a::euclidean_space) set"] + empty_subsetI independent_empty) text {* Notion of dimension. *} definition "dim V = (SOME n. \B. B \ V \ independent B \ V \ span B \ (card B = n))" -lemma basis_exists: "\B. (B :: ('a::euclidean_space) set) \ V \ independent B \ V \ span B \ (card B = dim V)" -unfolding dim_def some_eq_ex[of "\n. \B. B \ V \ independent B \ V \ span B \ (card B = n)"] -using maximal_independent_subset[of V] independent_bound -by auto +lemma basis_exists: + "\B. (B :: ('a::euclidean_space) set) \ V \ independent B \ V \ span B \ (card B = dim V)" + unfolding dim_def some_eq_ex[of "\n. \B. B \ V \ independent B \ V \ span B \ (card B = n)"] + using maximal_independent_subset[of V] independent_bound + by auto text {* Consequences of independence or spanning for cardinality. *} lemma independent_card_le_dim: - assumes "(B::('a::euclidean_space) set) \ V" and "independent B" shows "card B \ dim V" + assumes "(B::('a::euclidean_space) set) \ V" and "independent B" + shows "card B \ dim V" proof - from basis_exists[of V] `B \ V` obtain B' where "independent B'" and "B \ span B'" and "card B' = dim V" by blast @@ -1581,21 +1636,25 @@ show ?thesis by auto qed -lemma span_card_ge_dim: "(B::('a::euclidean_space) set) \ V \ V \ span B \ finite B \ dim V \ card B" +lemma span_card_ge_dim: + "(B::('a::euclidean_space) set) \ V \ V \ span B \ finite B \ dim V \ card B" by (metis basis_exists[of V] independent_span_bound subset_trans) lemma basis_card_eq_dim: - "B \ (V:: ('a::euclidean_space) set) \ V \ span B \ independent B \ finite B \ card B = dim V" + "B \ (V:: ('a::euclidean_space) set) \ V \ span B \ + independent B \ finite B \ card B = dim V" by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_bound) -lemma dim_unique: "(B::('a::euclidean_space) set) \ V \ V \ span B \ independent B \ card B = n \ dim V = n" +lemma dim_unique: "(B::('a::euclidean_space) set) \ V \ V \ span B \ + independent B \ card B = n \ dim V = n" by (metis basis_card_eq_dim) text {* More lemmas about dimension. *} lemma dim_UNIV: "dim (UNIV :: ('a::euclidean_space) set) = DIM('a)" apply (rule dim_unique[of "(basis::nat=>'a) ` {.. T \ dim S \ dim T" @@ -1608,29 +1667,30 @@ text {* Converses to those. *} lemma card_ge_dim_independent: - assumes BV:"(B::('a::euclidean_space) set) \ V" and iB:"independent B" and dVB:"dim V \ card B" + assumes BV:"(B::('a::euclidean_space) set) \ V" + and iB:"independent B" and dVB:"dim V \ card B" shows "V \ span B" -proof- - {fix a assume aV: "a \ V" - {assume aB: "a \ span B" +proof - + { fix a assume aV: "a \ V" + { assume aB: "a \ span B" then have iaB: "independent (insert a B)" using iB aV BV by (simp add: independent_insert) from aV BV have th0: "insert a B \ V" by blast from aB have "a \B" by (auto simp add: span_superset) with independent_card_le_dim[OF th0 iaB] dVB independent_bound[OF iB] have False by auto } - then have "a \ span B" by blast} + then have "a \ span B" by blast } then show ?thesis by blast qed lemma card_le_dim_spanning: assumes BV: "(B:: ('a::euclidean_space) set) \ V" and VB: "V \ span B" - and fB: "finite B" and dVB: "dim V \ card B" + and fB: "finite B" and dVB: "dim V \ card B" shows "independent B" -proof- - {fix a assume a: "a \ B" "a \ span (B -{a})" +proof - + { fix a assume a: "a \ B" "a \ span (B -{a})" from a fB have c0: "card B \ 0" by auto from a fB have cb: "card (B -{a}) = card B - 1" by auto from BV a have th0: "B -{a} \ V" by blast - {fix x assume x: "x \ V" + { fix x assume x: "x \ V" from a have eq: "insert a (B -{a}) = B" by blast from x VB have x': "x \ span B" by blast from span_trans[OF a(2), unfolded eq, OF x'] @@ -1639,13 +1699,13 @@ have th2: "finite (B -{a})" using fB by auto from span_card_ge_dim[OF th0 th1 th2] have c: "dim V \ card (B -{a})" . - from c c0 dVB cb have False by simp} + from c c0 dVB cb have False by simp } then show ?thesis unfolding dependent_def by blast qed -lemma card_eq_dim: "(B:: ('a::euclidean_space) set) \ V \ card B = dim V \ finite B \ independent B \ V \ span B" - by (metis order_eq_iff card_le_dim_spanning - card_ge_dim_independent) +lemma card_eq_dim: "(B:: ('a::euclidean_space) set) \ V \ + card B = dim V \ finite B \ independent B \ V \ span B" + by (metis order_eq_iff card_le_dim_spanning card_ge_dim_independent) text {* More general size bound lemmas. *} @@ -1653,11 +1713,12 @@ "independent (S:: ('a::euclidean_space) set) \ finite S \ card S \ dim S" by (metis independent_card_le_dim independent_bound subset_refl) -lemma dependent_biggerset_general: "(finite (S:: ('a::euclidean_space) set) \ card S > dim S) \ dependent S" +lemma dependent_biggerset_general: + "(finite (S:: ('a::euclidean_space) set) \ card S > dim S) \ dependent S" using independent_bound_general[of S] by (metis linorder_not_le) lemma dim_span: "dim (span (S:: ('a::euclidean_space) set)) = dim S" -proof- +proof - have th0: "dim S \ dim (span S)" by (auto simp add: subset_eq intro: dim_subset span_superset) from basis_exists[of S] @@ -1666,7 +1727,7 @@ have bSS: "B \ span S" using B(1) by (metis subset_eq span_inc) have sssB: "span S \ span B" using span_mono[OF B(3)] by (simp add: span_span) from span_card_ge_dim[OF bSS sssB fB(1)] th0 show ?thesis - using fB(2) by arith + using fB(2) by arith qed lemma subset_le_dim: "(S:: ('a::euclidean_space) set) \ span T \ dim S \ dim T" @@ -1678,19 +1739,19 @@ lemma spans_image: assumes lf: "linear f" and VB: "V \ span B" shows "f ` V \ span (f ` B)" - unfolding span_linear_image[OF lf] - by (metis VB image_mono) + unfolding span_linear_image[OF lf] by (metis VB image_mono) lemma dim_image_le: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes lf: "linear f" shows "dim (f ` S) \ dim (S)" -proof- +proof - from basis_exists[of S] obtain B where B: "B \ S" "independent B" "S \ span B" "card B = dim S" by blast from B have fB: "finite B" "card B = dim S" using independent_bound by blast+ have "dim (f ` S) \ card (f ` B)" apply (rule span_card_ge_dim) - using lf B fB by (auto simp add: span_linear_image spans_image subset_image_iff) + using lf B fB apply (auto simp add: span_linear_image spans_image subset_image_iff) + done also have "\ \ dim S" using card_image_le[OF fB(1)] fB by simp finally show ?thesis . qed @@ -1699,7 +1760,7 @@ lemma spanning_surjective_image: assumes us: "UNIV \ span S" - and lf: "linear f" and sf: "surj f" + and lf: "linear f" and sf: "surj f" shows "UNIV \ span (f ` S)" proof- have "UNIV \ f ` UNIV" using sf by (auto simp add: surj_def) @@ -1711,12 +1772,12 @@ assumes iS: "independent S" and lf: "linear f" and fi: "inj f" shows "independent (f ` S)" proof- - {fix a assume a: "a \ S" "f a \ span (f ` S - {f a})" + { fix a assume a: "a \ S" "f a \ span (f ` S - {f a})" have eq: "f ` S - {f a} = f ` (S - {a})" using fi by (auto simp add: inj_on_def) from a have "f a \ f ` span (S -{a})" unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast - hence "a \ span (S -{a})" using fi by (auto simp add: inj_on_def) + then have "a \ span (S -{a})" using fi by (auto simp add: inj_on_def) with a(1) iS have False by (simp add: dependent_def) } then show ?thesis unfolding dependent_def by blast qed @@ -1731,7 +1792,7 @@ lemma pairwise_orthogonal_insert: assumes "pairwise orthogonal S" - assumes "\y. y \ S \ orthogonal x y" + and "\y. y \ S \ orthogonal x y" shows "pairwise orthogonal (insert x S)" using assms unfolding pairwise_def by (auto simp add: orthogonal_commute) @@ -1741,10 +1802,12 @@ assumes fB: "finite B" shows "\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C" (is " \C. ?P B C") -proof(induct rule: finite_induct[OF fB]) - case 1 thus ?case apply (rule exI[where x="{}"]) by (auto simp add: pairwise_def) + using fB +proof (induct rule: finite_induct) + case empty + then show ?case apply (rule exI[where x="{}"]) by (auto simp add: pairwise_def) next - case (2 a B) + case (insert a B) note fB = `finite B` and aB = `a \ B` from `\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C` obtain C where C: "finite C" "card C \ card B" @@ -1752,9 +1815,11 @@ let ?a = "a - setsum (\x. (x \ a / (x \ x)) *\<^sub>R x) C" let ?C = "insert ?a C" from C(1) have fC: "finite ?C" by simp - from fB aB C(1,2) have cC: "card ?C \ card (insert a B)" by (simp add: card_insert_if) - {fix x k - have th0: "\(a::'a) b c. a - (b - c) = c + (a - b)" by (simp add: field_simps) + from fB aB C(1,2) have cC: "card ?C \ card (insert a B)" + by (simp add: card_insert_if) + { fix x k + have th0: "\(a::'a) b c. a - (b - c) = c + (a - b)" + by (simp add: field_simps) have "x - k *\<^sub>R (a - (\x\C. (x \ a / (x \ x)) *\<^sub>R x)) \ span C \ x - k *\<^sub>R a \ span C" apply (simp only: scaleR_right_diff_distrib th0) apply (rule span_add_eq) @@ -1762,11 +1827,13 @@ apply (rule span_setsum[OF C(1)]) apply clarify apply (rule span_mul) - by (rule span_superset)} + apply (rule span_superset) + apply assumption + done } then have SC: "span ?C = span (insert a B)" unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto { fix y assume yC: "y \ C" - hence Cy: "C = insert y (C - {y})" by blast + then have Cy: "C = insert y (C - {y})" by blast have fth: "finite (C - {y})" using C by simp have "orthogonal ?a y" unfolding orthogonal_def @@ -1787,12 +1854,12 @@ fixes V :: "('a::euclidean_space) set" shows "\B. independent B \ B \ span V \ V \ span B \ (card B = dim V) \ pairwise orthogonal B" proof- - from basis_exists[of V] obtain B where B: "B \ V" "independent B" "V \ span B" "card B = dim V" by blast + from basis_exists[of V] obtain B where + B: "B \ V" "independent B" "V \ span B" "card B = dim V" by blast from B have fB: "finite B" "card B = dim V" using independent_bound by auto from basis_orthogonal[OF fB(1)] obtain C where C: "finite C" "card C \ card B" "span C = span B" "pairwise orthogonal C" by blast - from C B - have CSV: "C \ span V" by (metis span_inc span_mono subset_trans) + from C B have CSV: "C \ span V" by (metis span_inc span_mono subset_trans) from span_mono[OF B(3)] C have SVC: "span V \ span C" by (simp add: span_span) from card_le_dim_spanning[OF CSV SVC C(1)] C(2,3) fB have iC: "independent C" by (simp add: dim_span) @@ -1805,14 +1872,15 @@ lemma span_eq: "span S = span T \ S \ span T \ T \ span S" using span_inc[unfolded subset_eq] using span_mono[of T "span S"] span_mono[of S "span T"] - by(auto simp add: span_span) + by (auto simp add: span_span) text {* Low-dimensional subset is in a hyperplane (weak orthogonal complement). *} -lemma span_not_univ_orthogonal: fixes S::"('a::euclidean_space) set" +lemma span_not_univ_orthogonal: + fixes S::"('a::euclidean_space) set" assumes sU: "span S \ UNIV" shows "\(a::'a). a \0 \ (\x \ span S. a \ x = 0)" -proof- +proof - from sU obtain a where a: "a \ span S" by blast from orthogonal_basis_exists obtain B where B: "independent B" "B \ span S" "S \ span B" "card B = dim S" "pairwise orthogonal B" @@ -1826,13 +1894,16 @@ apply (rule span_setsum[OF fB(1)]) apply clarsimp apply (rule span_mul) - by (rule span_superset) + apply (rule span_superset) + apply assumption + done with a have a0:"?a \ 0" by auto have "\x\span B. ?a \ x = 0" - proof(rule span_induct') - show "subspace {x. ?a \ x = 0}" by (auto simp add: subspace_def inner_add) -next - {fix x assume x: "x \ B" + proof (rule span_induct') + show "subspace {x. ?a \ x = 0}" + by (auto simp add: subspace_def inner_add) + next + { fix x assume x: "x \ B" from x have B': "B = insert x (B - {x})" by blast have fth: "finite (B - {x})" using fB by simp have "?a \ x = 0" @@ -1842,7 +1913,8 @@ apply (clarsimp simp add: inner_add inner_setsum_left) apply (rule setsum_0', rule ballI) unfolding inner_commute - by (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])} + apply (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format]) + done } then show "\x \ B. ?a \ x = 0" by blast qed with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"]) @@ -1856,11 +1928,11 @@ lemma lowdim_subset_hyperplane: fixes S::"('a::euclidean_space) set" assumes d: "dim S < DIM('a)" shows "\(a::'a). a \ 0 \ span S \ {x. a \ x = 0}" -proof- - {assume "span S = UNIV" - hence "dim (span S) = dim (UNIV :: ('a) set)" by simp - hence "dim S = DIM('a)" by (simp add: dim_span dim_UNIV) - with d have False by arith} +proof - + { assume "span S = UNIV" + then have "dim (span S) = dim (UNIV :: ('a) set)" by simp + then have "dim S = DIM('a)" by (simp add: dim_span dim_UNIV) + with d have False by arith } hence th: "span S \ UNIV" by blast from span_not_univ_subset_hyperplane[OF th] show ?thesis . qed @@ -1869,12 +1941,12 @@ lemma linear_indep_image_lemma: assumes lf: "linear f" and fB: "finite B" - and ifB: "independent (f ` B)" - and fi: "inj_on f B" and xsB: "x \ span B" - and fx: "f x = 0" + and ifB: "independent (f ` B)" + and fi: "inj_on f B" and xsB: "x \ span B" + and fx: "f x = 0" shows "x = 0" using fB ifB fi xsB fx -proof(induct arbitrary: x rule: finite_induct[OF fB]) +proof (induct arbitrary: x rule: finite_induct[OF fB]) case 1 thus ?case by auto next case (2 a b x) @@ -1885,23 +1957,25 @@ have ifb: "independent (f ` b)" . have fib: "inj_on f b" apply (rule subset_inj_on [OF "2.prems"(3)]) - by blast + apply blast + done from span_breakdown[of a "insert a b", simplified, OF "2.prems"(4)] obtain k where k: "x - k*\<^sub>R a \ span (b -{a})" by blast have "f (x - k*\<^sub>R a) \ span (f ` b)" unfolding span_linear_image[OF lf] apply (rule imageI) - using k span_mono[of "b-{a}" b] by blast - hence "f x - k*\<^sub>R f a \ span (f ` b)" + using k span_mono[of "b-{a}" b] apply blast + done + then have "f x - k*\<^sub>R f a \ span (f ` b)" by (simp add: linear_sub[OF lf] linear_cmul[OF lf]) - hence th: "-k *\<^sub>R f a \ span (f ` b)" + then have th: "-k *\<^sub>R f a \ span (f ` b)" using "2.prems"(5) by simp - {assume k0: "k = 0" + { assume k0: "k = 0" from k0 k have "x \ span (b -{a})" by simp then have "x \ span b" using span_mono[of "b-{a}" b] - by blast} + by blast } moreover - {assume k0: "k \ 0" + { assume k0: "k \ 0" from span_mul[OF th, of "- 1/ k"] k0 have th1: "f a \ span (f ` b)" by auto @@ -1912,7 +1986,7 @@ using "2.hyps"(2) "2.prems"(3) by auto with th1 have False by blast - then have "x \ span b" by blast} + then have "x \ span b" by blast } ultimately have xsb: "x \ span b" by blast from "2.hyps"(3)[OF fb ifb fib xsb "2.prems"(5)] show "x = 0" . @@ -1927,7 +2001,7 @@ \ (\x\ span B. \c. g (c*\<^sub>R x) = c *\<^sub>R g x) \ (\x\ B. g x = f x)" using ib fi -proof(induct rule: finite_induct[OF fi]) +proof (induct rule: finite_induct[OF fi]) case 1 thus ?case by auto next case (2 a b) @@ -1937,17 +2011,17 @@ g: "\x\span b. \y\span b. g (x + y) = g x + g y" "\x\span b. \c. g (c *\<^sub>R x) = c *\<^sub>R g x" "\x\b. g x = f x" by blast let ?h = "\z. SOME k. (z - k *\<^sub>R a) \ span b" - {fix z assume z: "z \ span (insert a b)" + { fix z assume z: "z \ span (insert a b)" have th0: "z - ?h z *\<^sub>R a \ span b" apply (rule someI_ex) unfolding span_breakdown_eq[symmetric] using z . - {fix k assume k: "z - k *\<^sub>R a \ span b" + { fix k assume k: "z - k *\<^sub>R a \ span b" have eq: "z - ?h z *\<^sub>R a - (z - k*\<^sub>R a) = (k - ?h z) *\<^sub>R a" by (simp add: field_simps scaleR_left_distrib [symmetric]) from span_sub[OF th0 k] have khz: "(k - ?h z) *\<^sub>R a \ span b" by (simp add: eq) - {assume "k \ ?h z" hence k0: "k - ?h z \ 0" by simp + { assume "k \ ?h z" hence k0: "k - ?h z \ 0" by simp from k0 span_mul[OF khz, of "1 /(k - ?h z)"] have "a \ span b" by simp with "2.prems"(1) "2.hyps"(2) have False @@ -1956,7 +2030,7 @@ with th0 have "z - ?h z *\<^sub>R a \ span b \ (\k. z - k *\<^sub>R a \ span b \ k = ?h z)" by blast} note h = this let ?g = "\z. ?h z *\<^sub>R f a + g (z - ?h z *\<^sub>R a)" - {fix x y assume x: "x \ span (insert a b)" and y: "y \ span (insert a b)" + { fix x y assume x: "x \ span (insert a b)" and y: "y \ span (insert a b)" have tha: "\(x::'a) y a k l. (x + y) - (k + l) *\<^sub>R a = (x - k *\<^sub>R a) + (y - l *\<^sub>R a)" by (simp add: algebra_simps) have addh: "?h (x + y) = ?h x + ?h y" @@ -1969,31 +2043,35 @@ g(1)[rule_format,OF conjunct1[OF h, OF x] conjunct1[OF h, OF y]] by (simp add: scaleR_left_distrib)} moreover - {fix x:: "'a" and c:: real assume x: "x \ span (insert a b)" + { fix x:: "'a" and c:: real + assume x: "x \ span (insert a b)" have tha: "\(x::'a) c k a. c *\<^sub>R x - (c * k) *\<^sub>R a = c *\<^sub>R (x - k *\<^sub>R a)" by (simp add: algebra_simps) have hc: "?h (c *\<^sub>R x) = c * ?h x" apply (rule conjunct2[OF h, rule_format, symmetric]) apply (metis span_mul x) - by (metis tha span_mul x conjunct1[OF h]) + apply (metis tha span_mul x conjunct1[OF h]) + done have "?g (c *\<^sub>R x) = c*\<^sub>R ?g x" unfolding hc tha g(2)[rule_format, OF conjunct1[OF h, OF x]] - by (simp add: algebra_simps)} + by (simp add: algebra_simps) } moreover - {fix x assume x: "x \ (insert a b)" - {assume xa: "x = a" + { fix x assume x: "x \ (insert a b)" + { assume xa: "x = a" have ha1: "1 = ?h a" apply (rule conjunct2[OF h, rule_format]) apply (metis span_superset insertI1) using conjunct1[OF h, OF span_superset, OF insertI1] - by (auto simp add: span_0) + apply (auto simp add: span_0) + done from xa ha1[symmetric] have "?g x = f x" apply simp using g(2)[rule_format, OF span_0, of 0] - by simp} + apply simp + done } moreover - {assume xb: "x \ b" + { assume xb: "x \ b" have h0: "0 = ?h x" apply (rule conjunct2[OF h, rule_format]) apply (metis span_superset x) @@ -2001,15 +2079,15 @@ apply (metis span_superset xb) done have "?g x = f x" - by (simp add: h0[symmetric] g(3)[rule_format, OF xb])} + by (simp add: h0[symmetric] g(3)[rule_format, OF xb]) } ultimately have "?g x = f x" using x by blast } - ultimately show ?case apply - apply (rule exI[where x="?g"]) by blast + ultimately show ?case apply - apply (rule exI[where x="?g"]) apply blast done qed lemma linear_independent_extend: assumes iB: "independent (B:: ('a::euclidean_space) set)" shows "\g. linear g \ (\x\B. g x = f x)" -proof- +proof - from maximal_independent_subset_extend[of B UNIV] iB obtain C where C: "B \ C" "independent C" "\x. x \ span C" by auto @@ -2018,21 +2096,25 @@ \ (\x\ span C. \c. g (c*\<^sub>R x) = c *\<^sub>R g x) \ (\x\ C. g x = f x)" by blast from g show ?thesis unfolding linear_def using C - apply clarsimp by blast + apply clarsimp apply blast done qed text {* Can construct an isomorphism between spaces of same dimension. *} -lemma card_le_inj: assumes fA: "finite A" and fB: "finite B" - and c: "card A \ card B" shows "(\f. f ` A \ B \ inj_on f A)" -using fB c -proof(induct arbitrary: B rule: finite_induct[OF fA]) - case 1 thus ?case by simp +lemma card_le_inj: + assumes fA: "finite A" and fB: "finite B" + and c: "card A \ card B" + shows "(\f. f ` A \ B \ inj_on f A)" + using fA fB c +proof (induct arbitrary: B rule: finite_induct) + case empty + then show ?case by simp next - case (2 x s t) - thus ?case - proof(induct rule: finite_induct[OF "2.prems"(1)]) - case 1 then show ?case by simp + case (insert x s t) + then show ?case + proof (induct rule: finite_induct[OF "insert.prems"(1)]) + case 1 + then show ?case by simp next case (2 y t) from "2.prems"(1,2,5) "2.hyps"(1,2) have cst:"card s \ card t" by simp @@ -2041,30 +2123,31 @@ from f "2.prems"(2) "2.hyps"(2) show ?case apply - apply (rule exI[where x = "\z. if z = x then y else f z"]) - by (auto simp add: inj_on_def) + apply (auto simp add: inj_on_def) + done qed qed -lemma card_subset_eq: assumes fB: "finite B" and AB: "A \ B" and - c: "card A = card B" +lemma card_subset_eq: + assumes fB: "finite B" and AB: "A \ B" and c: "card A = card B" shows "A = B" -proof- +proof - from fB AB have fA: "finite A" by (auto intro: finite_subset) from fA fB have fBA: "finite (B - A)" by auto have e: "A \ (B - A) = {}" by blast have eq: "A \ (B - A) = B" using AB by blast from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0" by arith - hence "B - A = {}" unfolding card_eq_0_iff using fA fB by simp + then have "B - A = {}" unfolding card_eq_0_iff using fA fB by simp with AB show "A = B" by blast qed lemma subspace_isomorphism: assumes s: "subspace (S:: ('a::euclidean_space) set)" - and t: "subspace (T :: ('b::euclidean_space) set)" - and d: "dim S = dim T" + and t: "subspace (T :: ('b::euclidean_space) set)" + and d: "dim S = dim T" shows "\f. linear f \ f ` S = T \ inj_on f S" -proof- +proof - from basis_exists[of S] independent_bound obtain B where B: "B \ S" "independent B" "S \ span B" "card B = dim S" and fB: "finite B" by blast from basis_exists[of T] independent_bound obtain C where @@ -2084,7 +2167,7 @@ have gi: "inj_on g B" using f(2) g(2) by (auto simp add: inj_on_def) note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi] - {fix x y assume x: "x \ S" and y: "y \ S" and gxy:"g x = g y" + { fix x y assume x: "x \ S" and y: "y \ S" and gxy: "g x = g y" from B(3) x y have x': "x \ span B" and y': "y \ span B" by blast+ from gxy have th0: "g (x - y) = 0" by (simp add: linear_sub[OF g(1)]) have th1: "x - y \ span B" using x' y' by (metis span_sub) @@ -2104,8 +2187,9 @@ lemma subspace_kernel: assumes lf: "linear f" shows "subspace {x. f x = 0}" -apply (simp add: subspace_def) -by (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf]) + apply (simp add: subspace_def) + apply (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf]) + done lemma linear_eq_0_span: assumes lf: "linear f" and f0: "\x\B. f x = 0" @@ -2120,7 +2204,7 @@ lemma linear_eq: assumes lf: "linear f" and lg: "linear g" and S: "S \ span B" - and fg: "\ x\ B. f x = g x" + and fg: "\ x\ B. f x = g x" shows "\x\ S. f x = g x" proof- let ?h = "\x. f x - g x" @@ -2131,12 +2215,12 @@ lemma linear_eq_stdbasis: assumes lf: "linear (f::'a::euclidean_space \ _)" and lg: "linear g" - and fg: "\ii (UNIV :: 'a set)" + { fix x assume x: "x \ (UNIV :: 'a set)" from equalityD2[OF span_basis'[where 'a='a]] have IU: " (UNIV :: 'a set) \ span ?I" by blast have "f x = g x" apply(rule linear_eq[OF lf lg IU,rule_format]) using fg x by auto } @@ -2147,9 +2231,9 @@ lemma bilinear_eq: assumes bf: "bilinear f" - and bg: "bilinear g" - and SB: "S \ span B" and TC: "T \ span C" - and fg: "\x\ B. \y\ C. f x y = g x y" + and bg: "bilinear g" + and SB: "S \ span B" and TC: "T \ span C" + and fg: "\x\ B. \y\ C. f x y = g x y" shows "\x\S. \y\T. f x y = g x y " proof- let ?P = "{x. \y\ span C. f x y = g x y}" @@ -2164,32 +2248,36 @@ apply (simp add: fg) apply (auto simp add: subspace_def) using bf bg unfolding bilinear_def linear_def - by(auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf]) + apply (auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def + intro: bilinear_ladd[OF bf]) + done then show ?thesis using SB TC by auto qed -lemma bilinear_eq_stdbasis: fixes f::"'a::euclidean_space \ 'b::euclidean_space \ _" +lemma bilinear_eq_stdbasis: + fixes f::"'a::euclidean_space \ 'b::euclidean_space \ _" assumes bf: "bilinear f" - and bg: "bilinear g" - and fg: "\ijijx \ (basis ` {..y\ (basis ` {..x \ (basis ` {..y\ (basis ` {.. 'b::euclidean_space" +lemma linear_injective_left_inverse: + fixes f::"'a::euclidean_space => 'b::euclidean_space" assumes lf: "linear f" and fi: "inj f" shows "\g. linear g \ g o f = id" -proof- +proof - from linear_independent_extend[OF independent_injective_image, OF independent_basis, OF lf fi] obtain h:: "'b => 'a" where h: "linear h" - " \x \ f ` basis ` {..i f) (basis i) = id (basis i)" + "\x \ f ` basis ` {..i f) (basis i) = id (basis i)" using inv_o_cancel[OF fi, unfolded fun_eq_iff id_def o_def] by auto @@ -2198,10 +2286,11 @@ then show ?thesis using h(1) by blast qed -lemma linear_surjective_right_inverse: fixes f::"'a::euclidean_space => 'b::euclidean_space" +lemma linear_surjective_right_inverse: + fixes f::"'a::euclidean_space => 'b::euclidean_space" assumes lf: "linear f" and sf: "surj f" shows "\g. linear g \ f o g = id" -proof- +proof - from linear_independent_extend[OF independent_basis[where 'a='b],of "inv f"] obtain h:: "'b \ 'a" where h: "linear h" "\ x\ basis ` {.. 'b::euclidean_space"} is also surjective. *} -lemma linear_injective_imp_surjective: fixes f::"'a::euclidean_space => 'a::euclidean_space" +lemma linear_injective_imp_surjective: + fixes f::"'a::euclidean_space => 'a::euclidean_space" assumes lf: "linear f" and fi: "inj f" shows "surj f" -proof- +proof - let ?U = "UNIV :: 'a set" from basis_exists[of ?U] obtain B where B: "B \ ?U" "independent B" "?U \ span B" "card B = dim ?U" @@ -2233,7 +2323,8 @@ unfolding d apply (rule card_image) apply (rule subset_inj_on[OF fi]) - by blast + apply blast + done from th show ?thesis unfolding span_linear_image[OF lf] surj_def using B(3) by blast @@ -2243,13 +2334,13 @@ lemma surjective_iff_injective_gen: assumes fS: "finite S" and fT: "finite T" and c: "card S = card T" - and ST: "f ` S \ T" + and ST: "f ` S \ T" shows "(\y \ T. \x \ S. f x = y) \ inj_on f S" (is "?lhs \ ?rhs") -proof- - {assume h: "?lhs" - {fix x y assume x: "x \ S" and y: "y \ S" and f: "f x = f y" +proof - + { assume h: "?lhs" + { fix x y assume x: "x \ S" and y: "y \ S" and f: "f x = f y" from x fS have S0: "card S \ 0" by auto - {assume xy: "x \ y" + { assume xy: "x \ y" have th: "card S \ card (f ` (S - {y}))" unfolding c apply (rule card_mono) @@ -2269,7 +2360,7 @@ then have "x = y" by blast} then have ?rhs unfolding inj_on_def by blast} moreover - {assume h: ?rhs + { assume h: ?rhs have "f ` S = T" apply (rule card_subset_eq[OF fT ST]) unfolding card_image[OF h] using c . @@ -2277,15 +2368,16 @@ ultimately show ?thesis by blast qed -lemma linear_surjective_imp_injective: fixes f::"'a::euclidean_space => 'a::euclidean_space" +lemma linear_surjective_imp_injective: + fixes f::"'a::euclidean_space => 'a::euclidean_space" assumes lf: "linear f" and sf: "surj f" shows "inj f" -proof- +proof - let ?U = "UNIV :: 'a set" from basis_exists[of ?U] obtain B where B: "B \ ?U" "independent B" "?U \ span B" and d: "card B = dim ?U" by blast - {fix x assume x: "x \ span B" and fx: "f x = 0" + { fix x assume x: "x \ span B" and fx: "f x = 0" from B(2) have fB: "finite B" using independent_bound by auto have fBi: "independent (f ` B)" apply (rule card_le_dim_spanning[of "f ` B" ?U]) @@ -2313,7 +2405,8 @@ by (rule card_image_le, rule fB) ultimately have th1: "card B = card (f ` B)" unfolding d by arith have fiB: "inj_on f B" - unfolding surjective_iff_injective_gen[OF fB finite_imageI[OF fB] th1 subset_refl, symmetric] by blast + unfolding surjective_iff_injective_gen[OF fB finite_imageI[OF fB] th1 subset_refl, symmetric] + by blast from linear_indep_image_lemma[OF lf fB fBi fiB x] fx have "x = 0" by blast} note th = this @@ -2326,7 +2419,7 @@ lemma left_right_inverse_eq: assumes fg: "f o g = id" and gh: "g o h = id" shows "f = h" -proof- +proof - have "f = f o (g o h)" unfolding gh by simp also have "\ = (f o g) o h" by (simp add: o_assoc) finally show "f = h" unfolding fg by simp @@ -2336,54 +2429,65 @@ "f o g = id \ g o f = id \ (\x. f(g x) = x) \ (\x. g(f x) = x)" by (simp add: fun_eq_iff o_def id_def) -lemma linear_injective_isomorphism: fixes f::"'a::euclidean_space => 'a::euclidean_space" +lemma linear_injective_isomorphism: + fixes f::"'a::euclidean_space => 'a::euclidean_space" assumes lf: "linear f" and fi: "inj f" shows "\f'. linear f' \ (\x. f' (f x) = x) \ (\x. f (f' x) = x)" -unfolding isomorphism_expand[symmetric] -using linear_surjective_right_inverse[OF lf linear_injective_imp_surjective[OF lf fi]] linear_injective_left_inverse[OF lf fi] -by (metis left_right_inverse_eq) + unfolding isomorphism_expand[symmetric] + using linear_surjective_right_inverse[OF lf linear_injective_imp_surjective[OF lf fi]] + linear_injective_left_inverse[OF lf fi] + by (metis left_right_inverse_eq) lemma linear_surjective_isomorphism: fixes f::"'a::euclidean_space => 'a::euclidean_space" assumes lf: "linear f" and sf: "surj f" shows "\f'. linear f' \ (\x. f' (f x) = x) \ (\x. f (f' x) = x)" -unfolding isomorphism_expand[symmetric] -using linear_surjective_right_inverse[OF lf sf] linear_injective_left_inverse[OF lf linear_surjective_imp_injective[OF lf sf]] -by (metis left_right_inverse_eq) + unfolding isomorphism_expand[symmetric] + using linear_surjective_right_inverse[OF lf sf] + linear_injective_left_inverse[OF lf linear_surjective_imp_injective[OF lf sf]] + by (metis left_right_inverse_eq) text {* Left and right inverses are the same for @{typ "'a::euclidean_space => 'a::euclidean_space"}. *} -lemma linear_inverse_left: fixes f::"'a::euclidean_space => 'a::euclidean_space" +lemma linear_inverse_left: + fixes f::"'a::euclidean_space => 'a::euclidean_space" assumes lf: "linear f" and lf': "linear f'" shows "f o f' = id \ f' o f = id" -proof- - {fix f f':: "'a => 'a" +proof - + { fix f f':: "'a => 'a" assume lf: "linear f" "linear f'" and f: "f o f' = id" from f have sf: "surj f" apply (auto simp add: o_def id_def surj_def) - by metis + apply metis + done from linear_surjective_isomorphism[OF lf(1) sf] lf f have "f' o f = id" unfolding fun_eq_iff o_def id_def - by metis} + by metis } then show ?thesis using lf lf' by metis qed text {* Moreover, a one-sided inverse is automatically linear. *} -lemma left_inverse_linear: fixes f::"'a::euclidean_space => 'a::euclidean_space" +lemma left_inverse_linear: + fixes f::"'a::euclidean_space => 'a::euclidean_space" assumes lf: "linear f" and gf: "g o f = id" shows "linear g" -proof- - from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def fun_eq_iff) - by metis +proof - + from gf have fi: "inj f" + apply (auto simp add: inj_on_def o_def id_def fun_eq_iff) + apply metis + done from linear_injective_isomorphism[OF lf fi] obtain h:: "'a \ 'a" where h: "linear h" "\x. h (f x) = x" "\x. f (h x) = x" by blast - have "h = g" apply (rule ext) using gf h(2,3) + have "h = g" + apply (rule ext) using gf h(2,3) apply (simp add: o_def id_def fun_eq_iff) - by metis + apply metis + done with h(1) show ?thesis by blast qed + subsection {* Infinity norm *} definition "infnorm (x::'a::euclidean_space) = Sup {abs(x$$i) |i. i infnorm x + infnorm y" -proof- +proof - have th: "\x y (z::real). x - y <= z \ x - z <= y" by arith have th1: "\S f. f ` S = { f i| i. i \ S}" by blast have th2: "\x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith @@ -2422,11 +2526,12 @@ unfolding th1 * unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma[where 'a='a]] unfolding infnorm_set_image ball_simps bex_simps - unfolding euclidean_simps by (metis th2) + unfolding euclidean_simps apply (metis th2) + done qed lemma infnorm_eq_0: "infnorm x = 0 \ (x::_::euclidean_space) = 0" -proof- +proof - have "infnorm x <= 0 \ x = 0" unfolding infnorm_def unfolding Sup_finite_le_iff[OF infnorm_set_lemma] @@ -2442,16 +2547,18 @@ lemma infnorm_neg: "infnorm (- x) = infnorm x" unfolding infnorm_def apply (rule cong[of "Sup" "Sup"]) - apply blast by auto + apply blast + apply auto + done lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)" -proof- +proof - have "y - x = - (x - y)" by simp then show ?thesis by (metis infnorm_neg) qed lemma real_abs_sub_infnorm: "\ infnorm x - infnorm y\ \ infnorm (x - y)" -proof- +proof - have th: "\(nx::real) n ny. nx <= n + ny \ ny <= n + nx ==> \nx - ny\ <= n" by arith from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"] @@ -2464,33 +2571,37 @@ lemma real_abs_infnorm: " \infnorm x\ = infnorm x" using infnorm_pos_le[of x] by arith -lemma component_le_infnorm: - shows "\x$$i\ \ infnorm (x::'a::euclidean_space)" -proof(cases "ix$$i\ \ infnorm (x::'a::euclidean_space)" +proof (cases "i {}" by blast have th1: "\S f. f ` S = { f i| i. i \ S}" by blast show ?thesis unfolding infnorm_def apply(subst Sup_finite_ge_iff) using Sup_finite_in[OF fS S0] - using infnorm_set_image using True by auto + using infnorm_set_image using True apply auto + done qed lemma infnorm_mul_lemma: "infnorm(a *\<^sub>R x) <= \a\ * infnorm x" apply (subst infnorm_def) unfolding Sup_finite_le_iff[OF infnorm_set_lemma] unfolding infnorm_set_image ball_simps euclidean_component_scaleR abs_mult - using component_le_infnorm[of x] by(auto intro: mult_mono) + using component_le_infnorm[of x] + apply (auto intro: mult_mono) + done lemma infnorm_mul: "infnorm(a *\<^sub>R x) = abs a * infnorm x" -proof- - {assume a0: "a = 0" hence ?thesis by (simp add: infnorm_0) } +proof - + { assume a0: "a = 0" hence ?thesis by (simp add: infnorm_0) } moreover - {assume a0: "a \ 0" + { assume a0: "a \ 0" from a0 have th: "(1/a) *\<^sub>R (a *\<^sub>R x) = x" by simp from a0 have ap: "\a\ > 0" by arith from infnorm_mul_lemma[of "1/a" "a *\<^sub>R x"] @@ -2514,7 +2625,7 @@ by (metis component_le_norm) lemma norm_le_infnorm: "norm(x) <= sqrt(real DIM('a)) * infnorm(x::'a::euclidean_space)" -proof- +proof - let ?d = "DIM('a)" have "real ?d \ 0" by simp hence d2: "(sqrt (real ?d))^2 = real ?d" @@ -2530,49 +2641,58 @@ apply (subst power2_abs[symmetric]) apply (rule power_mono) unfolding infnorm_def Sup_finite_ge_iff[OF infnorm_set_lemma] - unfolding infnorm_set_image bex_simps apply(rule_tac x=i in bexI) by auto + unfolding infnorm_set_image bex_simps apply(rule_tac x=i in bexI) + apply auto + done from real_le_lsqrt[OF inner_ge_zero th th1] show ?thesis unfolding norm_eq_sqrt_inner id_def . qed lemma tendsto_infnorm [tendsto_intros]: - assumes "(f ---> a) F" shows "((\x. infnorm (f x)) ---> infnorm a) F" + assumes "(f ---> a) F" + shows "((\x. infnorm (f x)) ---> infnorm a) F" proof (rule tendsto_compose [OF LIM_I assms]) fix r :: real assume "0 < r" - thus "\s>0. \x. x \ a \ norm (x - a) < s \ norm (infnorm x - infnorm a) < r" + then show "\s>0. \x. x \ a \ norm (x - a) < s \ norm (infnorm x - infnorm a) < r" by (metis real_norm_def le_less_trans real_abs_sub_infnorm infnorm_le_norm) qed text {* Equality in Cauchy-Schwarz and triangle inequalities. *} lemma norm_cauchy_schwarz_eq: "x \ y = norm x * norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" (is "?lhs \ ?rhs") -proof- - {assume h: "x = 0" - hence ?thesis by simp} +proof - + { assume h: "x = 0" + then have ?thesis by simp } moreover - {assume h: "y = 0" - hence ?thesis by simp} + { assume h: "y = 0" + then have ?thesis by simp } moreover - {assume x: "x \ 0" and y: "y \ 0" + { assume x: "x \ 0" and y: "y \ 0" from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"] - have "?rhs \ (norm y * (norm y * norm x * norm x - norm x * (x \ y)) - norm x * (norm y * (y \ x) - norm x * norm y * norm y) = 0)" + have "?rhs \ + (norm y * (norm y * norm x * norm x - norm x * (x \ y)) - + norm x * (norm y * (y \ x) - norm x * norm y * norm y) = 0)" using x y unfolding inner_simps - unfolding power2_norm_eq_inner[symmetric] power2_eq_square diff_eq_0_iff_eq apply (simp add: inner_commute) - apply (simp add: field_simps) by metis + unfolding power2_norm_eq_inner[symmetric] power2_eq_square diff_eq_0_iff_eq + apply (simp add: inner_commute) + apply (simp add: field_simps) + apply metis + done also have "\ \ (2 * norm x * norm y * (norm x * norm y - x \ y) = 0)" using x y by (simp add: field_simps inner_commute) also have "\ \ ?lhs" using x y apply simp - by metis - finally have ?thesis by blast} + apply metis + done + finally have ?thesis by blast } ultimately show ?thesis by blast qed lemma norm_cauchy_schwarz_abs_eq: - shows "abs(x \ y) = norm x * norm y \ - norm x *\<^sub>R y = norm y *\<^sub>R x \ norm(x) *\<^sub>R y = - norm y *\<^sub>R x" (is "?lhs \ ?rhs") -proof- + "abs(x \ y) = norm x * norm y \ + norm x *\<^sub>R y = norm y *\<^sub>R x \ norm(x) *\<^sub>R y = - norm y *\<^sub>R x" (is "?lhs \ ?rhs") +proof - have th: "\(x::real) a. a \ 0 \ abs x = a \ x = a \ x = - a" by arith have "?rhs \ norm x *\<^sub>R y = norm y *\<^sub>R x \ norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)" by simp @@ -2588,20 +2708,21 @@ lemma norm_triangle_eq: fixes x y :: "'a::real_inner" shows "norm(x + y) = norm x + norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" -proof- - {assume x: "x =0 \ y =0" - hence ?thesis by (cases "x=0", simp_all)} +proof - + { assume x: "x = 0 \ y = 0" + then have ?thesis by (cases "x = 0") simp_all } moreover - {assume x: "x \ 0" and y: "y \ 0" - hence "norm x \ 0" "norm y \ 0" + { assume x: "x \ 0" and y: "y \ 0" + then have "norm x \ 0" "norm y \ 0" by simp_all - hence n: "norm x > 0" "norm y > 0" - using norm_ge_zero[of x] norm_ge_zero[of y] - by arith+ - have th: "\(a::real) b c. a + b + c \ 0 ==> (a = b + c \ a^2 = (b + c)^2)" by algebra + then have n: "norm x > 0" "norm y > 0" + using norm_ge_zero[of x] norm_ge_zero[of y] by arith+ + have th: "\(a::real) b c. a + b + c \ 0 ==> (a = b + c \ a^2 = (b + c)^2)" + by algebra have "norm(x + y) = norm x + norm y \ norm(x + y)^ 2 = (norm x + norm y) ^2" apply (rule th) using n norm_ge_zero[of "x + y"] - by arith + apply arith + done also have "\ \ norm x *\<^sub>R y = norm y *\<^sub>R x" unfolding norm_cauchy_schwarz_eq[symmetric] unfolding power2_norm_eq_inner inner_simps @@ -2610,11 +2731,11 @@ ultimately show ?thesis by blast qed + subsection {* Collinearity *} -definition - collinear :: "'a::real_vector set \ bool" where - "collinear S \ (\u. \x \ S. \ y \ S. \c. x - y = c *\<^sub>R u)" +definition collinear :: "'a::real_vector set \ bool" + where "collinear S \ (\u. \x \ S. \ y \ S. \c. x - y = c *\<^sub>R u)" lemma collinear_empty: "collinear {}" by (simp add: collinear_def) @@ -2629,14 +2750,16 @@ apply (rule exI[where x="- 1"], simp) done -lemma collinear_lemma: "collinear {0,x,y} \ x = 0 \ y = 0 \ (\c. y = c *\<^sub>R x)" (is "?lhs \ ?rhs") -proof- - {assume "x=0 \ y = 0" hence ?thesis - by (cases "x = 0", simp_all add: collinear_2 insert_commute)} +lemma collinear_lemma: + "collinear {0,x,y} \ x = 0 \ y = 0 \ (\c. y = c *\<^sub>R x)" (is "?lhs \ ?rhs") +proof - + { assume "x=0 \ y = 0" + then have ?thesis by (cases "x = 0") (simp_all add: collinear_2 insert_commute) } moreover - {assume x: "x \ 0" and y: "y \ 0" - {assume h: "?lhs" - then obtain u where u: "\ x\ {0,x,y}. \y\ {0,x,y}. \c. x - y = c *\<^sub>R u" unfolding collinear_def by blast + { assume x: "x \ 0" and y: "y \ 0" + { assume h: "?lhs" + then obtain u where u: "\ x\ {0,x,y}. \y\ {0,x,y}. \c. x - y = c *\<^sub>R u" + unfolding collinear_def by blast from u[rule_format, of x 0] u[rule_format, of y 0] obtain cx and cy where cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u" @@ -2646,9 +2769,9 @@ let ?d = "cy / cx" from cx cy cx0 have "y = ?d *\<^sub>R x" by simp - hence ?rhs using x y by blast} + then have ?rhs using x y by blast } moreover - {assume h: "?rhs" + { assume h: "?rhs" then obtain c where c: "y = c *\<^sub>R x" using x y by blast have ?lhs unfolding collinear_def c apply (rule exI[where x=x]) @@ -2658,49 +2781,49 @@ apply (rule exI[where x=1], simp) apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib) apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib) - done} - ultimately have ?thesis by blast} + done } + ultimately have ?thesis by blast } ultimately show ?thesis by blast qed -lemma norm_cauchy_schwarz_equal: - shows "abs(x \ y) = norm x * norm y \ collinear {0,x,y}" -unfolding norm_cauchy_schwarz_abs_eq -apply (cases "x=0", simp_all add: collinear_2) -apply (cases "y=0", simp_all add: collinear_2 insert_commute) -unfolding collinear_lemma -apply simp -apply (subgoal_tac "norm x \ 0") -apply (subgoal_tac "norm y \ 0") -apply (rule iffI) -apply (cases "norm x *\<^sub>R y = norm y *\<^sub>R x") -apply (rule exI[where x="(1/norm x) * norm y"]) -apply (drule sym) -unfolding scaleR_scaleR[symmetric] -apply (simp add: field_simps) -apply (rule exI[where x="(1/norm x) * - norm y"]) -apply clarify -apply (drule sym) -unfolding scaleR_scaleR[symmetric] -apply (simp add: field_simps) -apply (erule exE) -apply (erule ssubst) -unfolding scaleR_scaleR -unfolding norm_scaleR -apply (subgoal_tac "norm x * c = \c\ * norm x \ norm x * c = - \c\ * norm x") -apply (case_tac "c <= 0", simp add: field_simps) -apply (simp add: field_simps) -apply (case_tac "c <= 0", simp add: field_simps) -apply (simp add: field_simps) -apply simp -apply simp -done +lemma norm_cauchy_schwarz_equal: "abs(x \ y) = norm x * norm y \ collinear {0,x,y}" + unfolding norm_cauchy_schwarz_abs_eq + apply (cases "x=0", simp_all add: collinear_2) + apply (cases "y=0", simp_all add: collinear_2 insert_commute) + unfolding collinear_lemma + apply simp + apply (subgoal_tac "norm x \ 0") + apply (subgoal_tac "norm y \ 0") + apply (rule iffI) + apply (cases "norm x *\<^sub>R y = norm y *\<^sub>R x") + apply (rule exI[where x="(1/norm x) * norm y"]) + apply (drule sym) + unfolding scaleR_scaleR[symmetric] + apply (simp add: field_simps) + apply (rule exI[where x="(1/norm x) * - norm y"]) + apply clarify + apply (drule sym) + unfolding scaleR_scaleR[symmetric] + apply (simp add: field_simps) + apply (erule exE) + apply (erule ssubst) + unfolding scaleR_scaleR + unfolding norm_scaleR + apply (subgoal_tac "norm x * c = \c\ * norm x \ norm x * c = - \c\ * norm x") + apply (case_tac "c <= 0", simp add: field_simps) + apply (simp add: field_simps) + apply (case_tac "c <= 0", simp add: field_simps) + apply (simp add: field_simps) + apply simp + apply simp + done + subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *} class ordered_euclidean_space = ord + euclidean_space + assumes eucl_le: "x \ y \ (\i < DIM('a). x $$ i \ y $$ i)" - and eucl_less: "x < y \ (\i < DIM('a). x $$ i < y $$ i)" + and eucl_less: "x < y \ (\i < DIM('a). x $$ i < y $$ i)" lemma eucl_less_not_refl[simp, intro!]: "\ x < (x::'a::ordered_euclidean_space)" unfolding eucl_less[where 'a='a] by auto @@ -2708,8 +2831,8 @@ lemma euclidean_trans[trans]: fixes x y z :: "'a::ordered_euclidean_space" shows "x < y \ y < z \ x < z" - and "x \ y \ y < z \ x < z" - and "x \ y \ y \ z \ x \ z" + and "x \ y \ y < z \ x < z" + and "x \ y \ y \ z \ x \ z" unfolding eucl_less[where 'a='a] eucl_le[where 'a='a] by (fast intro: less_trans, fast intro: le_less_trans, fast intro: order_trans) @@ -2725,7 +2848,8 @@ "\i. i > 0 \ x $$ i = 0" defer apply(subst euclidean_eq) apply safe unfolding euclidean_lambda_beta' - unfolding euclidean_component_def by auto + unfolding euclidean_component_def apply auto + done lemma complex_basis[simp]: shows "basis 0 = (1::complex)" and "basis 1 = ii" and "basis (Suc 0) = ii" @@ -2741,7 +2865,9 @@ definition "x \ (y::('a\'b)) \ (\i'b). x $$ i \ y $$ i)" definition "x < (y::('a\'b)) \ (\i'b). x $$ i < y $$ i)" -instance proof qed (auto simp: less_prod_def less_eq_prod_def) +instance + by default (auto simp: less_prod_def less_eq_prod_def) + end end