# HG changeset patch # User huffman # Date 1237451359 25200 # Node ID 638b088bb84076eced4df06a90fd4c5e4a2a4980 # Parent ac50e7dedf6d2b5f32182f18a23f17839162d02d imported patch euclidean diff -r ac50e7dedf6d -r 638b088bb840 src/HOL/Library/Determinants.thy --- a/src/HOL/Library/Determinants.thy Wed Mar 18 22:17:23 2009 +0100 +++ b/src/HOL/Library/Determinants.thy Thu Mar 19 01:29:19 2009 -0700 @@ -68,22 +68,22 @@ subsection{* Trace *} definition trace :: "'a::semiring_1^'n^'n \ 'a" where - "trace A = setsum (\i. ((A$i)$i)) {1..dimindex(UNIV::'n set)}" + "trace A = setsum (\i. ((A$i)$i)) (UNIV::'n set)" lemma trace_0: "trace(mat 0) = 0" - by (simp add: trace_def mat_def Cart_lambda_beta setsum_0) + by (simp add: trace_def mat_def) -lemma trace_I: "trace(mat 1 :: 'a::semiring_1^'n^'n) = of_nat(dimindex(UNIV::'n set))" - by (simp add: trace_def mat_def Cart_lambda_beta) +lemma trace_I: "trace(mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))" + by (simp add: trace_def mat_def) lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B" - by (simp add: trace_def setsum_addf Cart_lambda_beta vector_component) + by (simp add: trace_def setsum_addf) lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B" - by (simp add: trace_def setsum_subtractf Cart_lambda_beta vector_component) + by (simp add: trace_def setsum_subtractf) lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'n) ** B) = trace (B**A)" - apply (simp add: trace_def matrix_matrix_mult_def Cart_lambda_beta) + apply (simp add: trace_def matrix_matrix_mult_def) apply (subst setsum_commute) by (simp add: mult_commute) @@ -92,18 +92,12 @@ (* ------------------------------------------------------------------------- *) definition det:: "'a::comm_ring_1^'n^'n \ 'a" where - "det A = setsum (\p. of_int (sign p) * setprod (\i. A$i$p i) {1 .. dimindex(UNIV :: 'n set)}) {p. p permutes {1 .. dimindex(UNIV :: 'n set)}}" + "det A = setsum (\p. of_int (sign p) * setprod (\i. A$i$p i) (UNIV :: 'n set)) {p. p permutes (UNIV :: 'n set)}" (* ------------------------------------------------------------------------- *) (* A few general lemmas we need below. *) (* ------------------------------------------------------------------------- *) -lemma Cart_lambda_beta_perm: assumes p: "p permutes {1..dimindex(UNIV::'n set)}" - and i: "i \ {1..dimindex(UNIV::'n set)}" - shows "Cart_nth (Cart_lambda g ::'a^'n) (p i) = g(p i)" - using permutes_in_image[OF p] i - by (simp add: Cart_lambda_beta permutes_in_image[OF p]) - lemma setprod_permute: assumes p: "p permutes S" shows "setprod f S = setprod (f o p) S" @@ -127,11 +121,11 @@ (* Basic determinant properties. *) (* ------------------------------------------------------------------------- *) -lemma det_transp: "det (transp A) = det (A::'a::comm_ring_1 ^'n^'n)" +lemma det_transp: "det (transp A) = det (A::'a::comm_ring_1 ^'n^'n::finite)" proof- let ?di = "\A i j. A$i$j" - let ?U = "{1 .. dimindex (UNIV :: 'n set)}" - have fU: "finite ?U" by blast + let ?U = "(UNIV :: 'n set)" + have fU: "finite ?U" by simp {fix p assume p: "p \ {p. p permutes ?U}" from p have pU: "p permutes ?U" by blast have sth: "sign (inv p) = sign p" @@ -147,7 +141,7 @@ {fix i assume i: "i \ ?U" from i permutes_inv_o[OF pU] permutes_in_image[OF pU] have "((\i. ?di (transp A) i (inv p i)) o p) i = ?di A i (p i)" - unfolding transp_def by (simp add: Cart_lambda_beta expand_fun_eq)} + unfolding transp_def by (simp add: expand_fun_eq)} then show "setprod ((\i. ?di (transp A) i (inv p i)) o p) ?U = setprod (\i. ?di A i (p i)) ?U" by (auto intro: setprod_cong) qed finally have "of_int (sign (inv p)) * (setprod (\i. ?di (transp A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\i. ?di A i (p i)) ?U)" using sth @@ -157,22 +151,21 @@ qed lemma det_lowerdiagonal: - fixes A :: "'a::comm_ring_1^'n^'n" - assumes ld: "\i j. i \ {1 .. dimindex (UNIV:: 'n set)} \ j \ {1 .. dimindex(UNIV:: 'n set)} \ i < j \ A$i$j = 0" - shows "det A = setprod (\i. A$i$i) {1..dimindex(UNIV:: 'n set)}" + fixes A :: "'a::comm_ring_1^'n^'n::{finite,wellorder}" + assumes ld: "\i j. i < j \ A$i$j = 0" + shows "det A = setprod (\i. A$i$i) (UNIV:: 'n set)" proof- - let ?U = "{1..dimindex(UNIV:: 'n set)}" + let ?U = "UNIV:: 'n set" let ?PU = "{p. p permutes ?U}" - let ?pp = "\p. of_int (sign p) * setprod (\i. A$i$p i) {1 .. dimindex(UNIV :: 'n set)}" - have fU: "finite ?U" by blast + let ?pp = "\p. of_int (sign p) * setprod (\i. A$i$p i) (UNIV :: 'n set)" + have fU: "finite ?U" by simp from finite_permutations[OF fU] have fPU: "finite ?PU" . have id0: "{id} \ ?PU" by (auto simp add: permutes_id) {fix p assume p: "p \ ?PU -{id}" from p have pU: "p permutes ?U" and pid: "p \ id" by blast+ from permutes_natset_le[OF pU] pid obtain i where - i: "i \ ?U" "p i > i" by (metis not_le) - from permutes_in_image[OF pU] i(1) have piU: "p i \ ?U" by blast - from ld[OF i(1) piU i(2)] i(1) have ex:"\i \ ?U. A$i$p i = 0" by blast + i: "p i > i" by (metis not_le) + from ld[OF i] have ex:"\i \ ?U. A$i$p i = 0" by blast from setprod_zero[OF fU ex] have "?pp p = 0" by simp} then have p0: "\p \ ?PU -{id}. ?pp p = 0" by blast from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis @@ -180,32 +173,32 @@ qed lemma det_upperdiagonal: - fixes A :: "'a::comm_ring_1^'n^'n" - assumes ld: "\i j. i \ {1 .. dimindex (UNIV:: 'n set)} \ j \ {1 .. dimindex(UNIV:: 'n set)} \ i > j \ A$i$j = 0" - shows "det A = setprod (\i. A$i$i) {1..dimindex(UNIV:: 'n set)}" + fixes A :: "'a::comm_ring_1^'n^'n::{finite,wellorder}" + assumes ld: "\i j. i > j \ A$i$j = 0" + shows "det A = setprod (\i. A$i$i) (UNIV:: 'n set)" proof- - let ?U = "{1..dimindex(UNIV:: 'n set)}" + let ?U = "UNIV:: 'n set" let ?PU = "{p. p permutes ?U}" - let ?pp = "(\p. of_int (sign p) * setprod (\i. A$i$p i) {1 .. dimindex(UNIV :: 'n set)})" - have fU: "finite ?U" by blast + let ?pp = "(\p. of_int (sign p) * setprod (\i. A$i$p i) (UNIV :: 'n set))" + have fU: "finite ?U" by simp from finite_permutations[OF fU] have fPU: "finite ?PU" . have id0: "{id} \ ?PU" by (auto simp add: permutes_id) {fix p assume p: "p \ ?PU -{id}" from p have pU: "p permutes ?U" and pid: "p \ id" by blast+ from permutes_natset_ge[OF pU] pid obtain i where - i: "i \ ?U" "p i < i" by (metis not_le) - from permutes_in_image[OF pU] i(1) have piU: "p i \ ?U" by blast - from ld[OF i(1) piU i(2)] i(1) have ex:"\i \ ?U. A$i$p i = 0" by blast + i: "p i < i" by (metis not_le) + from ld[OF i] have ex:"\i \ ?U. A$i$p i = 0" by blast from setprod_zero[OF fU ex] have "?pp p = 0" by simp} then have p0: "\p \ ?PU -{id}. ?pp p = 0" by blast from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis unfolding det_def by (simp add: sign_id) qed -lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1" +(* FIXME: get rid of wellorder requirement *) +lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n::{finite,wellorder}) = 1" proof- let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n" - let ?U = "{1 .. dimindex (UNIV :: 'n set)}" + let ?U = "UNIV :: 'n set" let ?f = "\i j. ?A$i$j" {fix i assume i: "i \ ?U" have "?f i i = 1" using i by (vector mat_def)} @@ -219,60 +212,38 @@ finally show ?thesis . qed -lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0" -proof- - let ?A = "mat 0 :: 'a::comm_ring_1^'n^'n" - let ?U = "{1 .. dimindex (UNIV :: 'n set)}" - let ?f = "\i j. ?A$i$j" - have th:"setprod (\i. ?f i i) ?U = 0" - apply (rule setprod_zero) - apply simp - apply (rule bexI[where x=1]) - using dimindex_ge_1[of "UNIV :: 'n set"] - by (simp_all add: mat_def Cart_lambda_beta) - {fix i j assume i: "i \ ?U" and j: "j \ ?U" and ij: "i < j" - have "?f i j = 0" using i j ij by (vector mat_def) } - then have "det ?A = setprod (\i. ?f i i) ?U" using det_lowerdiagonal - by blast - also have "\ = 0" unfolding th .. - finally show ?thesis . -qed +lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n::finite) = 0" + by (simp add: det_def setprod_zero) lemma det_permute_rows: - fixes A :: "'a::comm_ring_1^'n^'n" - assumes p: "p permutes {1 .. dimindex (UNIV :: 'n set)}" + fixes A :: "'a::comm_ring_1^'n^'n::finite" + assumes p: "p permutes (UNIV :: 'n::finite set)" shows "det(\ i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" - apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric] del: One_nat_def) + apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric]) apply (subst sum_permutations_compose_right[OF p]) proof(rule setsum_cong2) - let ?U = "{1 .. dimindex (UNIV :: 'n set)}" + let ?U = "UNIV :: 'n set" let ?PU = "{p. p permutes ?U}" - let ?Ap = "(\ i. A$p i :: 'a^'n^'n)" fix q assume qPU: "q \ ?PU" - have fU: "finite ?U" by blast + have fU: "finite ?U" by simp from qPU have q: "q permutes ?U" by blast from p q have pp: "permutation p" and qp: "permutation q" by (metis fU permutation_permutes)+ from permutes_inv[OF p] have ip: "inv p permutes ?U" . - {fix i assume i: "i \ ?U" - from Cart_lambda_beta[rule_format, OF i, of "\i. A$ p i"] - have "?Ap$i$ (q o p) i = A $ p i $ (q o p) i " by simp} - hence "setprod (\i. ?Ap$i$ (q o p) i) ?U = setprod (\i. A$p i$(q o p) i) ?U" - by (auto intro: setprod_cong) - also have "\ = setprod ((\i. A$p i$(q o p) i) o inv p) ?U" + have "setprod (\i. A$p i$ (q o p) i) ?U = setprod ((\i. A$p i$(q o p) i) o inv p) ?U" by (simp only: setprod_permute[OF ip, symmetric]) also have "\ = setprod (\i. A $ (p o inv p) i $ (q o (p o inv p)) i) ?U" by (simp only: o_def) also have "\ = setprod (\i. A$i$q i) ?U" by (simp only: o_def permutes_inverses[OF p]) - finally have thp: "setprod (\i. ?Ap$i$ (q o p) i) ?U = setprod (\i. A$i$q i) ?U" + finally have thp: "setprod (\i. A$p i$ (q o p) i) ?U = setprod (\i. A$i$q i) ?U" by blast - show "of_int (sign (q o p)) * setprod (\i. ?Ap$i$ (q o p) i) ?U = of_int (sign p) * of_int (sign q) * setprod (\i. A$i$q i) ?U" + show "of_int (sign (q o p)) * setprod (\i. A$ p i$ (q o p) i) ?U = of_int (sign p) * of_int (sign q) * setprod (\i. A$i$q i) ?U" by (simp only: thp sign_compose[OF qp pp] mult_commute of_int_mult) qed lemma det_permute_columns: - fixes A :: "'a::comm_ring_1^'n^'n" - assumes p: "p permutes {1 .. dimindex (UNIV :: 'n set)}" + fixes A :: "'a::comm_ring_1^'n^'n::finite" + assumes p: "p permutes (UNIV :: 'n set)" shows "det(\ i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A" proof- let ?Ap = "\ i j. A$i$ p j :: 'a^'n^'n" @@ -281,15 +252,13 @@ unfolding det_permute_rows[OF p, of ?At] det_transp .. moreover have "?Ap = transp (\ i. transp A $ p i)" - by (simp add: transp_def Cart_eq Cart_lambda_beta Cart_lambda_beta_perm[OF p]) + by (simp add: transp_def Cart_eq) ultimately show ?thesis by simp qed lemma det_identical_rows: - fixes A :: "'a::ordered_idom^'n^'n" - assumes i: "i\{1 .. dimindex (UNIV :: 'n set)}" - and j: "j\{1 .. dimindex (UNIV :: 'n set)}" - and ij: "i \ j" + fixes A :: "'a::ordered_idom^'n^'n::finite" + assumes ij: "i \ j" and r: "row i A = row j A" shows "det A = 0" proof- @@ -298,94 +267,59 @@ have th1: "of_int (-1) = - 1" by (metis of_int_1 of_int_minus number_of_Min) let ?p = "Fun.swap i j id" let ?A = "\ i. A $ ?p i" - from r have "A = ?A" by (simp add: Cart_eq Cart_lambda_beta Cart_lambda_beta_perm[OF permutes_swap_id[OF i j]] row_def swap_def) + from r have "A = ?A" by (simp add: Cart_eq row_def swap_def) hence "det A = det ?A" by simp moreover have "det A = - det ?A" - by (simp add: det_permute_rows[OF permutes_swap_id[OF i j]] sign_swap_id ij th1) + by (simp add: det_permute_rows[OF permutes_swap_id] sign_swap_id ij th1) ultimately show "det A = 0" by (metis tha) qed lemma det_identical_columns: - fixes A :: "'a::ordered_idom^'n^'n" - assumes i: "i\{1 .. dimindex (UNIV :: 'n set)}" - and j: "j\{1 .. dimindex (UNIV :: 'n set)}" - and ij: "i \ j" + fixes A :: "'a::ordered_idom^'n^'n::finite" + assumes ij: "i \ j" and r: "column i A = column j A" shows "det A = 0" apply (subst det_transp[symmetric]) -apply (rule det_identical_rows[OF i j ij]) -by (metis row_transp i j r) +apply (rule det_identical_rows[OF ij]) +by (metis row_transp r) lemma det_zero_row: - fixes A :: "'a::{idom, ring_char_0}^'n^'n" - assumes i: "i\{1 .. dimindex (UNIV :: 'n set)}" - and r: "row i A = 0" + fixes A :: "'a::{idom, ring_char_0}^'n^'n::finite" + assumes r: "row i A = 0" shows "det A = 0" -using i r -apply (simp add: row_def det_def Cart_lambda_beta Cart_eq vector_component del: One_nat_def) +using r +apply (simp add: row_def det_def Cart_eq) apply (rule setsum_0') -apply (clarsimp simp add: sign_nz simp del: One_nat_def) +apply (clarsimp simp add: sign_nz) apply (rule setprod_zero) apply simp -apply (rule bexI[where x=i]) -apply (erule_tac x="a i" in ballE) -apply (subgoal_tac "(0\'a ^ 'n) $ a i = 0") -apply simp -apply (rule zero_index) -apply (drule permutes_in_image[of _ _ i]) -apply simp -apply (drule permutes_in_image[of _ _ i]) -apply simp -apply simp +apply auto done lemma det_zero_column: - fixes A :: "'a::{idom,ring_char_0}^'n^'n" - assumes i: "i\{1 .. dimindex (UNIV :: 'n set)}" - and r: "column i A = 0" + fixes A :: "'a::{idom,ring_char_0}^'n^'n::finite" + assumes r: "column i A = 0" shows "det A = 0" apply (subst det_transp[symmetric]) - apply (rule det_zero_row[OF i]) - by (metis row_transp r i) - -lemma setsum_lambda_beta[simp]: "setsum (\i. ((\ i. g i) :: 'a::{comm_monoid_add}^'n) $ i ) {1 .. dimindex (UNIV :: 'n set)} = setsum g {1 .. dimindex (UNIV :: 'n set)}" - by (simp add: Cart_lambda_beta) - -lemma setprod_lambda_beta[simp]: "setprod (\i. ((\ i. g i) :: 'a::{comm_monoid_mult}^'n) $ i ) {1 .. dimindex (UNIV :: 'n set)} = setprod g {1 .. dimindex (UNIV :: 'n set)}" - apply (rule setprod_cong) - apply simp - apply (simp add: Cart_lambda_beta') - done - -lemma setprod_lambda_beta2[simp]: "setprod (\i. ((\ i. g i) :: 'a::{comm_monoid_mult}^'n^'n) $ i$ f i ) {1 .. dimindex (UNIV :: 'n set)} = setprod (\i. g i $ f i) {1 .. dimindex (UNIV :: 'n set)}" -proof(rule setprod_cong[OF refl]) - let ?U = "{1 .. dimindex (UNIV :: 'n set)}" - fix i assume i: "i \ ?U" - from Cart_lambda_beta'[OF i, of g] have - "((\ i. g i) :: 'a^'n^'n) $ i = g i" . - hence "((\ i. g i) :: 'a^'n^'n) $ i $ f i = g i $ f i" by simp - then - show "((\ i. g i):: 'a^'n^'n) $ i $ f i = g i $ f i" . -qed + apply (rule det_zero_row [of i]) + by (metis row_transp r) lemma det_row_add: - assumes k: "k \ {1 .. dimindex (UNIV :: 'n set)}" + fixes a b c :: "'n::finite \ _ ^ 'n" shows "det((\ i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) = det((\ i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) + det((\ i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)" -unfolding det_def setprod_lambda_beta2 setsum_addf[symmetric] +unfolding det_def Cart_lambda_beta setsum_addf[symmetric] proof (rule setsum_cong2) - let ?U = "{1 .. dimindex (UNIV :: 'n set)}" + let ?U = "UNIV :: 'n set" let ?pU = "{p. p permutes ?U}" - let ?f = "(\i. if i = k then a i + b i else c i)::nat \ 'a::comm_ring_1^'n" - let ?g = "(\ i. if i = k then a i else c i)::nat \ 'a::comm_ring_1^'n" - let ?h = "(\ i. if i = k then b i else c i)::nat \ 'a::comm_ring_1^'n" + let ?f = "(\i. if i = k then a i + b i else c i)::'n \ 'a::comm_ring_1^'n" + let ?g = "(\ i. if i = k then a i else c i)::'n \ 'a::comm_ring_1^'n" + let ?h = "(\ i. if i = k then b i else c i)::'n \ 'a::comm_ring_1^'n" fix p assume p: "p \ ?pU" let ?Uk = "?U - {k}" from p have pU: "p permutes ?U" by blast - from k have pkU: "p k \ ?U" by (simp only: permutes_in_image[OF pU]) - note pin[simp] = permutes_in_image[OF pU] - have kU: "?U = insert k ?Uk" using k by blast + have kU: "?U = insert k ?Uk" by blast {fix j assume j: "j \ ?Uk" from j have "?f j $ p j = ?g j $ p j" and "?f j $ p j= ?h j $ p j" by simp_all} @@ -394,14 +328,14 @@ apply - apply (rule setprod_cong, simp_all)+ done - have th3: "finite ?Uk" "k \ ?Uk" using k by auto + have th3: "finite ?Uk" "k \ ?Uk" by auto have "setprod (\i. ?f i $ p i) ?U = setprod (\i. ?f i $ p i) (insert k ?Uk)" unfolding kU[symmetric] .. also have "\ = ?f k $ p k * setprod (\i. ?f i $ p i) ?Uk" apply (rule setprod_insert) apply simp - using k by blast - also have "\ = (a k $ p k * setprod (\i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\i. ?f i $ p i) ?Uk)" using pkU by (simp add: ring_simps vector_component) + by blast + also have "\ = (a k $ p k * setprod (\i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\i. ?f i $ p i) ?Uk)" by (simp add: ring_simps) also have "\ = (a k $ p k * setprod (\i. ?g i $ p i) ?Uk) + (b k$ p k * setprod (\i. ?h i $ p i) ?Uk)" by (metis th1 th2) also have "\ = setprod (\i. ?g i $ p i) (insert k ?Uk) + setprod (\i. ?h i $ p i) (insert k ?Uk)" unfolding setprod_insert[OF th3] by simp @@ -411,38 +345,36 @@ qed lemma det_row_mul: - assumes k: "k \ {1 .. dimindex (UNIV :: 'n set)}" + fixes a b :: "'n::finite \ _ ^ 'n" shows "det((\ i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) = c* det((\ i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)" -unfolding det_def setprod_lambda_beta2 setsum_right_distrib +unfolding det_def Cart_lambda_beta setsum_right_distrib proof (rule setsum_cong2) - let ?U = "{1 .. dimindex (UNIV :: 'n set)}" + let ?U = "UNIV :: 'n set" let ?pU = "{p. p permutes ?U}" - let ?f = "(\i. if i = k then c*s a i else b i)::nat \ 'a::comm_ring_1^'n" - let ?g = "(\ i. if i = k then a i else b i)::nat \ 'a::comm_ring_1^'n" + let ?f = "(\i. if i = k then c*s a i else b i)::'n \ 'a::comm_ring_1^'n" + let ?g = "(\ i. if i = k then a i else b i)::'n \ 'a::comm_ring_1^'n" fix p assume p: "p \ ?pU" let ?Uk = "?U - {k}" from p have pU: "p permutes ?U" by blast - from k have pkU: "p k \ ?U" by (simp only: permutes_in_image[OF pU]) - note pin[simp] = permutes_in_image[OF pU] - have kU: "?U = insert k ?Uk" using k by blast + have kU: "?U = insert k ?Uk" by blast {fix j assume j: "j \ ?Uk" from j have "?f j $ p j = ?g j $ p j" by simp} then have th1: "setprod (\i. ?f i $ p i) ?Uk = setprod (\i. ?g i $ p i) ?Uk" apply - apply (rule setprod_cong, simp_all) done - have th3: "finite ?Uk" "k \ ?Uk" using k by auto + have th3: "finite ?Uk" "k \ ?Uk" by auto have "setprod (\i. ?f i $ p i) ?U = setprod (\i. ?f i $ p i) (insert k ?Uk)" unfolding kU[symmetric] .. also have "\ = ?f k $ p k * setprod (\i. ?f i $ p i) ?Uk" apply (rule setprod_insert) apply simp - using k by blast - also have "\ = (c*s a k) $ p k * setprod (\i. ?f i $ p i) ?Uk" using pkU by (simp add: ring_simps vector_component) + by blast + also have "\ = (c*s a k) $ p k * setprod (\i. ?f i $ p i) ?Uk" by (simp add: ring_simps) also have "\ = c* (a k $ p k * setprod (\i. ?g i $ p i) ?Uk)" - unfolding th1 using pkU by (simp add: vector_component mult_ac) + unfolding th1 by (simp add: mult_ac) also have "\ = c* (setprod (\i. ?g i $ p i) (insert k ?Uk))" unfolding setprod_insert[OF th3] by simp finally have "setprod (\i. ?f i $ p i) ?U = c* (setprod (\i. ?g i $ p i) ?U)" unfolding kU[symmetric] . @@ -451,36 +383,33 @@ qed lemma det_row_0: - assumes k: "k \ {1 .. dimindex (UNIV :: 'n set)}" + fixes b :: "'n::finite \ _ ^ 'n" shows "det((\ i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0" -using det_row_mul[OF k, of 0 "\i. 1" b] +using det_row_mul[of k 0 "\i. 1" b] apply (simp) unfolding vector_smult_lzero . lemma det_row_operation: - fixes A :: "'a::ordered_idom^'n^'n" - assumes i: "i \ {1 .. dimindex(UNIV :: 'n set)}" - and j: "j \ {1 .. dimindex(UNIV :: 'n set)}" - and ij: "i \ j" + fixes A :: "'a::ordered_idom^'n^'n::finite" + assumes ij: "i \ j" shows "det (\ k. if k = i then row i A + c *s row j A else row k A) = det A" proof- let ?Z = "(\ k. if k = i then row j A else row k A) :: 'a ^'n^'n" - have th: "row i ?Z = row j ?Z" using i j by (vector row_def) + have th: "row i ?Z = row j ?Z" by (vector row_def) have th2: "((\ k. if k = i then row i A else row k A) :: 'a^'n^'n) = A" - using i j by (vector row_def) + by (vector row_def) show ?thesis - unfolding det_row_add [OF i] det_row_mul[OF i] det_identical_rows[OF i j ij th] th2 + unfolding det_row_add [of i] det_row_mul[of i] det_identical_rows[OF ij th] th2 by simp qed lemma det_row_span: - fixes A :: "'a:: ordered_idom^'n^'n" - assumes i: "i \ {1 .. dimindex(UNIV :: 'n set)}" - and x: "x \ span {row j A |j. j\ {1 .. dimindex(UNIV :: 'n set)} \ j\ i}" + fixes A :: "'a:: ordered_idom^'n^'n::finite" + assumes x: "x \ span {row j A |j. j \ i}" shows "det (\ k. if k = i then row i A + x else row k A) = det A" proof- - let ?U = "{1 .. dimindex(UNIV :: 'n set)}" - let ?S = "{row j A |j. j\ ?U \ j\ i}" + let ?U = "UNIV :: 'n set" + let ?S = "{row j A |j. j \ i}" let ?d = "\x. det (\ k. if k = i then x else row k A)" let ?P = "\x. ?d (row i A + x) = det A" {fix k @@ -489,17 +418,17 @@ then have P0: "?P 0" apply - apply (rule cong[of det, OF refl]) - using i by (vector row_def) + by (vector row_def) moreover {fix c z y assume zS: "z \ ?S" and Py: "?P y" - from zS obtain j where j: "z = row j A" "j \ ?U" "i \ j" by blast + from zS obtain j where j: "z = row j A" "i \ j" by blast let ?w = "row i A + y" have th0: "row i A + (c*s z + y) = ?w + c*s z" by vector have thz: "?d z = 0" - apply (rule det_identical_rows[OF i j(2,3)]) - using i j by (vector row_def) + apply (rule det_identical_rows[OF j(2)]) + using j by (vector row_def) have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" unfolding th0 .. - then have "?P (c*s z + y)" unfolding thz Py det_row_mul[OF i] det_row_add[OF i] + then have "?P (c*s z + y)" unfolding thz Py det_row_mul[of i] det_row_add[of i] by simp } ultimately show ?thesis @@ -516,48 +445,47 @@ (* ------------------------------------------------------------------------- *) lemma det_dependent_rows: - fixes A:: "'a::ordered_idom^'n^'n" + fixes A:: "'a::ordered_idom^'n^'n::finite" assumes d: "dependent (rows A)" shows "det A = 0" proof- - let ?U = "{1 .. dimindex (UNIV :: 'n set)}" - from d obtain i where i: "i \ ?U" "row i A \ span (rows A - {row i A})" + let ?U = "UNIV :: 'n set" + from d obtain i where i: "row i A \ span (rows A - {row i A})" unfolding dependent_def rows_def by blast - {fix j k assume j: "j \?U" and k: "k \ ?U" and jk: "j \ k" + {fix j k assume jk: "j \ k" and c: "row j A = row k A" - from det_identical_rows[OF j k jk c] have ?thesis .} + from det_identical_rows[OF jk c] have ?thesis .} moreover - {assume H: "\ i j. i\ ?U \ j \ ?U \ i \ j \ row i A \ row j A" - have th0: "- row i A \ span {row j A|j. j \ ?U \ j \ i}" + {assume H: "\ i j. i \ j \ row i A \ row j A" + have th0: "- row i A \ span {row j A|j. j \ i}" apply (rule span_neg) apply (rule set_rev_mp) - apply (rule i(2)) + apply (rule i) apply (rule span_mono) using H i by (auto simp add: rows_def) - from det_row_span[OF i(1) th0] + from det_row_span[OF th0] have "det A = det (\ k. if k = i then 0 *s 1 else row k A)" unfolding right_minus vector_smult_lzero .. - with det_row_mul[OF i(1), of "0::'a" "\i. 1"] + with det_row_mul[of i "0::'a" "\i. 1"] have "det A = 0" by simp} ultimately show ?thesis by blast qed -lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::ordered_idom^'n^'n))" shows "det A = 0" +lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::ordered_idom^'n^'n::finite))" shows "det A = 0" by (metis d det_dependent_rows rows_transp det_transp) (* ------------------------------------------------------------------------- *) (* Multilinearity and the multiplication formula. *) (* ------------------------------------------------------------------------- *) -lemma Cart_lambda_cong: "(\x. x \ {1 .. dimindex (UNIV :: 'n set)} \ f x = g x) \ (Cart_lambda f::'a^'n) = (Cart_lambda g :: 'a^'n)" +lemma Cart_lambda_cong: "(\x. f x = g x) \ (Cart_lambda f::'a^'n) = (Cart_lambda g :: 'a^'n)" apply (rule iffD1[OF Cart_lambda_unique]) by vector lemma det_linear_row_setsum: - assumes fS: "finite S" and k: "k \ {1 .. dimindex (UNIV :: 'n set)}" - shows "det ((\ i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) = setsum (\j. det ((\ i. if i = k then a i j else c i)::'a^'n^'n)) S" - using k + assumes fS: "finite S" + shows "det ((\ i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n::finite) = setsum (\j. det ((\ i. if i = k then a i j else c i)::'a^'n^'n)) S" proof(induct rule: finite_induct[OF fS]) - case 1 thus ?case apply simp unfolding setsum_empty det_row_0[OF k] .. + case 1 thus ?case apply simp unfolding setsum_empty det_row_0[of k] .. next case (2 x F) then show ?case by (simp add: det_row_add cong del: if_weak_cong) @@ -588,91 +516,89 @@ lemma eq_id_iff[simp]: "(\x. f x = x) = (f = id)" by (auto intro: ext) lemma det_linear_rows_setsum_lemma: - assumes fS: "finite S" and k: "k \ dimindex (UNIV :: 'n set)" - shows "det((\ i. if i <= k then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n) = - setsum (\f. det((\ i. if i <= k then a i (f i) else c i)::'a^'n^'n)) - {f. (\i \ {1 .. k}. f i \ S) \ (\i. i \ {1..k} \ f i = i)}" -using k -proof(induct k arbitrary: a c) - case 0 - have th0: "\x y. (\ i. if i <= 0 then x i else y i) = (\ i. y i)" by vector - from "0.prems" show ?case unfolding th0 by simp + assumes fS: "finite S" and fT: "finite T" + shows "det((\ i. if i \ T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n::finite) = + setsum (\f. det((\ i. if i \ T then a i (f i) else c i)::'a^'n^'n)) + {f. (\i \ T. f i \ S) \ (\i. i \ T \ f i = i)}" +using fT +proof(induct T arbitrary: a c set: finite) + case empty + have th0: "\x y. (\ i. if i \ {} then x i else y i) = (\ i. y i)" by vector + from "empty.prems" show ?case unfolding th0 by simp next - case (Suc k a c) - let ?F = "\k. {f. (\i \ {1 .. k}. f i \ S) \ (\i. i \ {1..k} \ f i = i)}" - let ?h = "\(y::nat,g) i. if i = Suc k then y else g i" - let ?k = "\h. (h(Suc k),(\i. if i = Suc k then i else h i))" - let ?s = "\ k a c f. det((\ i. if i <= k then a i (f i) else c i)::'a^'n^'n)" - let ?c = "\i. if i = Suc k then a i j else c i" - from Suc.prems have Sk: "Suc k \ {1 .. dimindex (UNIV :: 'n set)}" by simp - from Suc.prems have k': "k \ dimindex (UNIV :: 'n set)" by arith - have thif: "\a b c d. (if b \ a then c else d) = (if a then c else if b then c else d)" by simp + case (insert z T a c) + let ?F = "\T. {f. (\i \ T. f i \ S) \ (\i. i \ T \ f i = i)}" + let ?h = "\(y,g) i. if i = z then y else g i" + let ?k = "\h. (h(z),(\i. if i = z then i else h i))" + let ?s = "\ k a c f. det((\ i. if i \ T then a i (f i) else c i)::'a^'n^'n)" + let ?c = "\i. if i = z then a i j else c i" + have thif: "\a b c d. (if a \ b then c else d) = (if a then c else if b then c else d)" by simp have thif2: "\a b c d e. (if a then b else if c then d else e) = (if c then (if a then b else d) else (if a then b else e))" by simp - have "det (\ i. if i \ Suc k then setsum (a i) S else c i) = - det (\ i. if i = Suc k then setsum (a i) S - else if i \ k then setsum (a i) S else c i)" - unfolding le_Suc_eq thif .. - also have "\ = (\j\S. det (\ i. if i \ k then setsum (a i) S - else if i = Suc k then a i j else c i))" - unfolding det_linear_row_setsum[OF fS Sk] + from `z \ T` have nz: "\i. i \ T \ i = z \ False" by auto + have "det (\ i. if i \ insert z T then setsum (a i) S else c i) = + det (\ i. if i = z then setsum (a i) S + else if i \ T then setsum (a i) S else c i)" + unfolding insert_iff thif .. + also have "\ = (\j\S. det (\ i. if i \ T then setsum (a i) S + else if i = z then a i j else c i))" + unfolding det_linear_row_setsum[OF fS] apply (subst thif2) - by (simp cong del: if_weak_cong cong add: if_cong) + using nz by (simp cong del: if_weak_cong cong add: if_cong) finally have tha: - "det (\ i. if i \ Suc k then setsum (a i) S else c i) = - (\(j, f)\S \ ?F k. det (\ i. if i \ k then a i (f i) - else if i = Suc k then a i j + "det (\ i. if i \ insert z T then setsum (a i) S else c i) = + (\(j, f)\S \ ?F T. det (\ i. if i \ T then a i (f i) + else if i = z then a i j else c i))" - unfolding Suc.hyps[OF k'] unfolding setsum_cartesian_product by blast + unfolding insert.hyps unfolding setsum_cartesian_product by blast show ?case unfolding tha apply(rule setsum_eq_general_reverses[where h= "?h" and k= "?k"], - blast intro: finite_cartesian_product fS finite_bounded_functions[OF fS], - blast intro: finite_cartesian_product fS finite_bounded_functions[OF fS], auto intro: ext) + blast intro: finite_cartesian_product fS finite, + blast intro: finite_cartesian_product fS finite) + using `z \ T` + apply (auto intro: ext) apply (rule cong[OF refl[of det]]) by vector qed lemma det_linear_rows_setsum: - assumes fS: "finite S" - shows "det (\ i. setsum (a i) S) = setsum (\f. det (\ i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. (\i \ {1 .. dimindex (UNIV :: 'n set)}. f i \ S) \ (\i. i \ {1.. dimindex (UNIV :: 'n set)} \ f i = i)}" + assumes fS: "finite (S::'n::finite set)" + shows "det (\ i. setsum (a i) S) = setsum (\f. det (\ i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n::finite)) {f. \i. f i \ S}" proof- - have th0: "\x y. ((\ i. if i <= dimindex(UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\ i. x i)" by vector + have th0: "\x y. ((\ i. if i \ (UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\ i. x i)" by vector - from det_linear_rows_setsum_lemma[OF fS, of "dimindex (UNIV :: 'n set)" a, unfolded th0, OF order_refl] show ?thesis by blast + from det_linear_rows_setsum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite] show ?thesis by simp qed lemma matrix_mul_setsum_alt: - fixes A B :: "'a::comm_ring_1^'n^'n" - shows "A ** B = (\ i. setsum (\k. A$i$k *s B $ k) {1 .. dimindex (UNIV :: 'n set)})" + fixes A B :: "'a::comm_ring_1^'n^'n::finite" + shows "A ** B = (\ i. setsum (\k. A$i$k *s B $ k) (UNIV :: 'n set))" by (vector matrix_matrix_mult_def setsum_component) lemma det_rows_mul: - "det((\ i. c i *s a i)::'a::comm_ring_1^'n^'n) = - setprod (\i. c i) {1..dimindex(UNIV:: 'n set)} * det((\ i. a i)::'a^'n^'n)" -proof (simp add: det_def Cart_lambda_beta' setsum_right_distrib vector_component cong add: setprod_cong del: One_nat_def, rule setsum_cong2) - let ?U = "{1 .. dimindex(UNIV :: 'n set)}" + "det((\ i. c i *s a i)::'a::comm_ring_1^'n^'n::finite) = + setprod (\i. c i) (UNIV:: 'n set) * det((\ i. a i)::'a^'n^'n)" +proof (simp add: det_def setsum_right_distrib cong add: setprod_cong, rule setsum_cong2) + let ?U = "UNIV :: 'n set" let ?PU = "{p. p permutes ?U}" fix p assume pU: "p \ ?PU" let ?s = "of_int (sign p)" from pU have p: "p permutes ?U" by blast - have "setprod (\i. (c i *s a i) $ p i) ?U = setprod (\i. c i * a i $ p i) ?U" - apply (rule setprod_cong, blast) - by (auto simp only: permutes_in_image[OF p] intro: vector_smult_component) - also have "\ = setprod c ?U * setprod (\i. a i $ p i) ?U" + have "setprod (\i. c i * a i $ p i) ?U = setprod c ?U * setprod (\i. a i $ p i) ?U" unfolding setprod_timesf .. - finally show "?s * (\xa\?U. (c xa *s a xa) $ p xa) = + then show "?s * (\xa\?U. c xa * a xa $ p xa) = setprod c ?U * (?s* (\xa\?U. a xa $ p xa))" by (simp add: ring_simps) qed lemma det_mul: - fixes A B :: "'a::ordered_idom^'n^'n" + fixes A B :: "'a::ordered_idom^'n^'n::finite" shows "det (A ** B) = det A * det B" proof- - let ?U = "{1 .. dimindex (UNIV :: 'n set)}" + let ?U = "UNIV :: 'n set" let ?F = "{f. (\i\ ?U. f i \ ?U) \ (\i. i \ ?U \ f i = i)}" let ?PU = "{p. p permutes ?U}" have fU: "finite ?U" by simp - have fF: "finite ?F" using finite_bounded_functions[OF fU] . + have fF: "finite ?F" by (rule finite) {fix p assume p: "p permutes ?U" have "p \ ?F" unfolding mem_Collect_eq permutes_in_image[OF p] @@ -687,23 +613,21 @@ let ?A = "(\ i. A$i$f i *s B$f i) :: 'a^'n^'n" let ?B = "(\ i. B$f i) :: 'a^'n^'n" {assume fni: "\ inj_on f ?U" - then obtain i j where ij: "i \ ?U" "j \ ?U" "f i = f j" "i \ j" + then obtain i j where ij: "f i = f j" "i \ j" unfolding inj_on_def by blast from ij have rth: "row i ?B = row j ?B" by (vector row_def) - from det_identical_rows[OF ij(1,2,4) rth] + from det_identical_rows[OF ij(2) rth] have "det (\ i. A$i$f i *s B$f i) = 0" unfolding det_rows_mul by simp} moreover {assume fi: "inj_on f ?U" from f fi have fith: "\i j. f i = f j \ i = j" - unfolding inj_on_def - apply (case_tac "i \ ?U") - apply (case_tac "j \ ?U") by metis+ + unfolding inj_on_def by metis note fs = fi[unfolded surjective_iff_injective_gen[OF fU fU refl fUU, symmetric]] {fix y - from fs f have "\x. f x = y" by (cases "y \ ?U") blast+ + from fs f have "\x. f x = y" by blast then obtain x where x: "f x = y" by blast {fix z assume z: "f z = y" from fith x z have "z = x" by metis} with x have "\!x. f x = y" by blast} @@ -747,7 +671,7 @@ unfolding det_def setsum_product by (rule setsum_cong2) have "det (A**B) = setsum (\f. det (\ i. A $ i $ f i *s B $ f i)) ?F" - unfolding matrix_mul_setsum_alt det_linear_rows_setsum[OF fU] .. + unfolding matrix_mul_setsum_alt det_linear_rows_setsum[OF fU] by simp also have "\ = setsum (\f. det (\ i. A$i$f i *s B$f i)) ?PU" using setsum_mono_zero_cong_left[OF fF PUF zth, symmetric] unfolding det_rows_mul by auto @@ -759,17 +683,18 @@ (* ------------------------------------------------------------------------- *) lemma invertible_left_inverse: - fixes A :: "real^'n^'n" + fixes A :: "real^'n^'n::finite" shows "invertible A \ (\(B::real^'n^'n). B** A = mat 1)" by (metis invertible_def matrix_left_right_inverse) lemma invertible_righ_inverse: - fixes A :: "real^'n^'n" + fixes A :: "real^'n^'n::finite" shows "invertible A \ (\(B::real^'n^'n). A** B = mat 1)" by (metis invertible_def matrix_left_right_inverse) +(* FIXME: get rid of wellorder requirement *) lemma invertible_det_nz: - fixes A::"real ^'n^'n" + fixes A::"real ^'n^'n::{finite,wellorder}" shows "invertible A \ det A \ 0" proof- {assume "invertible A" @@ -780,7 +705,7 @@ apply (simp add: det_mul det_I) by algebra } moreover {assume H: "\ invertible A" - let ?U = "{1 .. dimindex(UNIV :: 'n set)}" + let ?U = "UNIV :: 'n set" have fU: "finite ?U" by simp from H obtain c i where c: "setsum (\i. c i *s row i A) ?U = 0" and iU: "i \ ?U" and ci: "c i \ 0" @@ -794,11 +719,11 @@ from c ci have thr0: "- row i A = setsum (\j. (1/ c i) *s c j *s row j A) (?U - {i})" unfolding setsum_diff1'[OF fU iU] setsum_cmul - apply (simp add: field_simps) + apply - apply (rule vector_mul_lcancel_imp[OF ci]) apply (auto simp add: vector_smult_assoc vector_smult_rneg field_simps) unfolding stupid .. - have thr: "- row i A \ span {row j A| j. j\ ?U \ j \ i}" + have thr: "- row i A \ span {row j A| j. j \ i}" unfolding thr0 apply (rule span_setsum) apply simp @@ -810,8 +735,8 @@ let ?B = "(\ k. if k = i then 0 else row k A) :: real ^'n^'n" have thrb: "row i ?B = 0" using iU by (vector row_def) have "det A = 0" - unfolding det_row_span[OF iU thr, symmetric] right_minus - unfolding det_zero_row[OF iU thrb] ..} + unfolding det_row_span[OF thr, symmetric] right_minus + unfolding det_zero_row[OF thrb] ..} ultimately show ?thesis by blast qed @@ -820,15 +745,14 @@ (* ------------------------------------------------------------------------- *) lemma cramer_lemma_transp: - fixes A:: "'a::ordered_idom^'n^'n" and x :: "'a ^'n" - assumes k: "k \ {1 .. dimindex(UNIV ::'n set)}" - shows "det ((\ i. if i = k then setsum (\i. x$i *s row i A) {1 .. dimindex(UNIV::'n set)} + fixes A:: "'a::ordered_idom^'n^'n::finite" and x :: "'a ^'n::finite" + shows "det ((\ i. if i = k then setsum (\i. x$i *s row i A) (UNIV::'n set) else row i A)::'a^'n^'n) = x$k * det A" (is "?lhs = ?rhs") proof- - let ?U = "{1 .. dimindex (UNIV :: 'n set)}" + let ?U = "UNIV :: 'n set" let ?Uk = "?U - {k}" - have U: "?U = insert k ?Uk" using k by blast + have U: "?U = insert k ?Uk" by blast have fUk: "finite ?Uk" by simp have kUk: "k \ ?Uk" by simp have th00: "\k s. x$k *s row k A + s = (x$k - 1) *s row k A + row k A + s" @@ -837,7 +761,7 @@ have "(\ i. row i A) = A" by (vector row_def) then have thd1: "det (\ i. row i A) = det A" by simp have thd0: "det (\ i. if i = k then row k A + (\i \ ?Uk. x $ i *s row i A) else row i A) = det A" - apply (rule det_row_span[OF k]) + apply (rule det_row_span) apply (rule span_setsum[OF fUk]) apply (rule ballI) apply (rule span_mul) @@ -849,30 +773,31 @@ unfolding setsum_insert[OF fUk kUk] apply (subst th00) unfolding add_assoc - apply (subst det_row_add[OF k]) + apply (subst det_row_add) unfolding thd0 - unfolding det_row_mul[OF k] + unfolding det_row_mul unfolding th001[of k "\i. row i A"] unfolding thd1 by (simp add: ring_simps) qed lemma cramer_lemma: - fixes A :: "'a::ordered_idom ^'n^'n" - assumes k: "k \ {1 .. dimindex (UNIV :: 'n set)}" (is " _ \ ?U") + fixes A :: "'a::ordered_idom ^'n^'n::finite" shows "det((\ i j. if j = k then (A *v x)$i else A$i$j):: 'a^'n^'n) = x$k * det A" proof- + let ?U = "UNIV :: 'n set" have stupid: "\c. setsum (\i. c i *s row i (transp A)) ?U = setsum (\i. c i *s column i A) ?U" by (auto simp add: row_transp intro: setsum_cong2) show ?thesis unfolding matrix_mult_vsum - unfolding cramer_lemma_transp[OF k, of x "transp A", unfolded det_transp, symmetric] + unfolding cramer_lemma_transp[of k x "transp A", unfolded det_transp, symmetric] unfolding stupid[of "\i. x$i"] apply (subst det_transp[symmetric]) apply (rule cong[OF refl[of det]]) by (vector transp_def column_def row_def) qed +(* FIXME: get rid of wellorder requirement *) lemma cramer: - fixes A ::"real^'n^'n" + fixes A ::"real^'n^'n::{finite,wellorder}" assumes d0: "det A \ 0" shows "A *v x = b \ x = (\ k. det(\ i j. if j=k then b$i else A$i$j :: real^'n^'n) / det A)" proof- @@ -884,7 +809,7 @@ {fix x assume x: "A *v x = b" have "x = (\ k. det(\ i j. if j=k then b$i else A$i$j :: real^'n^'n) / det A)" unfolding x[symmetric] - using d0 by (simp add: Cart_eq Cart_lambda_beta' cramer_lemma field_simps)} + using d0 by (simp add: Cart_eq cramer_lemma field_simps)} with xe show ?thesis by auto qed @@ -894,7 +819,7 @@ definition "orthogonal_transformation f \ linear f \ (\v w. f v \ f w = v \ w)" -lemma orthogonal_transformation: "orthogonal_transformation f \ linear f \ (\(v::real ^'n). norm (f v) = norm v)" +lemma orthogonal_transformation: "orthogonal_transformation f \ linear f \ (\(v::real ^_). norm (f v) = norm v)" unfolding orthogonal_transformation_def apply auto apply (erule_tac x=v in allE)+ @@ -903,14 +828,14 @@ definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \ transp Q ** Q = mat 1 \ Q ** transp Q = mat 1" -lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \ transp Q ** Q = mat 1" +lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n::finite) \ transp Q ** Q = mat 1" by (metis matrix_left_right_inverse orthogonal_matrix_def) -lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1)" +lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n::finite)" by (simp add: orthogonal_matrix_def transp_mat matrix_mul_lid) lemma orthogonal_matrix_mul: - fixes A :: "real ^'n^'n" + fixes A :: "real ^'n^'n::finite" assumes oA : "orthogonal_matrix A" and oB: "orthogonal_matrix B" shows "orthogonal_matrix(A ** B)" @@ -921,26 +846,26 @@ by (simp add: matrix_mul_rid) lemma orthogonal_transformation_matrix: - fixes f:: "real^'n \ real^'n" + fixes f:: "real^'n \ real^'n::finite" shows "orthogonal_transformation f \ linear f \ orthogonal_matrix(matrix f)" (is "?lhs \ ?rhs") proof- let ?mf = "matrix f" let ?ot = "orthogonal_transformation f" - let ?U = "{1 .. dimindex (UNIV :: 'n set)}" + let ?U = "UNIV :: 'n set" have fU: "finite ?U" by simp let ?m1 = "mat 1 :: real ^'n^'n" {assume ot: ?ot from ot have lf: "linear f" and fd: "\v w. f v \ f w = v \ w" unfolding orthogonal_transformation_def orthogonal_matrix by blast+ - {fix i j assume i: "i \ ?U" and j: "j \ ?U" + {fix i j let ?A = "transp ?mf ** ?mf" have th0: "\b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)" "\b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)" by simp_all - from fd[rule_format, of "basis i" "basis j", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul] i j + from fd[rule_format, of "basis i" "basis j", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul] have "?A$i$j = ?m1 $ i $ j" - by (simp add: Cart_lambda_beta' dot_def matrix_matrix_mult_def columnvector_def rowvector_def basis_def th0 setsum_delta[OF fU] mat_def del: One_nat_def)} + by (simp add: dot_def matrix_matrix_mult_def columnvector_def rowvector_def basis_def th0 setsum_delta[OF fU] mat_def)} hence "orthogonal_matrix ?mf" unfolding orthogonal_matrix by vector with lf have ?rhs by blast} moreover @@ -949,12 +874,13 @@ unfolding orthogonal_matrix_def norm_eq orthogonal_transformation unfolding matrix_works[OF lf, symmetric] apply (subst dot_matrix_vector_mul) - by (simp add: dot_matrix_product matrix_mul_lid del: One_nat_def)} + by (simp add: dot_matrix_product matrix_mul_lid)} ultimately show ?thesis by blast qed +(* FIXME: get rid of wellorder requirement *) lemma det_orthogonal_matrix: - fixes Q:: "'a::ordered_idom^'n^'n" + fixes Q:: "'a::ordered_idom^'n^'n::{finite,wellorder}" assumes oQ: "orthogonal_matrix Q" shows "det Q = 1 \ det Q = - 1" proof- @@ -979,7 +905,7 @@ (* Linearity of scaling, and hence isometry, that preserves origin. *) (* ------------------------------------------------------------------------- *) lemma scaling_linear: - fixes f :: "real ^'n \ real ^'n" + fixes f :: "real ^'n \ real ^'n::finite" assumes f0: "f 0 = 0" and fd: "\x y. dist (f x) (f y) = c * dist x y" shows "linear f" proof- @@ -995,7 +921,7 @@ qed lemma isometry_linear: - "f (0:: real^'n) = (0:: real^'n) \ \x y. dist(f x) (f y) = dist x y + "f (0:: real^'n) = (0:: real^'n::finite) \ \x y. dist(f x) (f y) = dist x y \ linear f" by (rule scaling_linear[where c=1]) simp_all @@ -1004,7 +930,7 @@ (* ------------------------------------------------------------------------- *) lemma orthogonal_transformation_isometry: - "orthogonal_transformation f \ f(0::real^'n) = (0::real^'n) \ (\x y. dist(f x) (f y) = dist x y)" + "orthogonal_transformation f \ f(0::real^'n) = (0::real^'n::finite) \ (\x y. dist(f x) (f y) = dist x y)" unfolding orthogonal_transformation apply (rule iffI) apply clarify @@ -1023,7 +949,7 @@ (* ------------------------------------------------------------------------- *) lemma isometry_sphere_extend: - fixes f:: "real ^'n \ real ^'n" + fixes f:: "real ^'n \ real ^'n::finite" assumes f1: "\x. norm x = 1 \ norm (f x) = 1" and fd1: "\ x y. norm x = 1 \ norm y = 1 \ dist (f x) (f y) = dist x y" shows "\g. orthogonal_transformation g \ (\x. norm x = 1 \ g x = f x)" @@ -1094,8 +1020,9 @@ definition "rotation_matrix Q \ orthogonal_matrix Q \ det Q = 1" definition "rotoinversion_matrix Q \ orthogonal_matrix Q \ det Q = - 1" +(* FIXME: get rid of wellorder requirement *) lemma orthogonal_rotation_or_rotoinversion: - fixes Q :: "'a::ordered_idom^'n^'n" + fixes Q :: "'a::ordered_idom^'n^'n::{finite,wellorder}" shows " orthogonal_matrix Q \ rotation_matrix Q \ rotoinversion_matrix Q" by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) (* ------------------------------------------------------------------------- *) @@ -1110,17 +1037,16 @@ by (simp add: nat_number setprod_numseg mult_commute) lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1" - by (simp add: det_def dimindex_def permutes_sing sign_id del: One_nat_def) + by (simp add: det_def permutes_sing sign_id UNIV_1) lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1" proof- - have f12: "finite {2::nat}" "1 \ {2::nat}" by auto - have th12: "{1 .. 2} = insert (1::nat) {2}" by auto + have f12: "finite {2::2}" "1 \ {2::2}" by auto show ?thesis - apply (simp add: det_def dimindex_def th12 del: One_nat_def) + unfolding det_def UNIV_2 unfolding setsum_over_permutations_insert[OF f12] unfolding permutes_sing - apply (simp add: sign_swap_id sign_id swap_id_eq del: One_nat_def) + apply (simp add: sign_swap_id sign_id swap_id_eq) by (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31)) qed @@ -1132,18 +1058,17 @@ A$1$2 * A$2$1 * A$3$3 - A$1$3 * A$2$2 * A$3$1" proof- - have f123: "finite {(2::nat), 3}" "1 \ {(2::nat), 3}" by auto - have f23: "finite {(3::nat)}" "2 \ {(3::nat)}" by auto - have th12: "{1 .. 3} = insert (1::nat) (insert 2 {3})" by auto + have f123: "finite {2::3, 3}" "1 \ {2::3, 3}" by auto + have f23: "finite {3::3}" "2 \ {3::3}" by auto show ?thesis - apply (simp add: det_def dimindex_def th12 del: One_nat_def) + unfolding det_def UNIV_3 unfolding setsum_over_permutations_insert[OF f123] unfolding setsum_over_permutations_insert[OF f23] unfolding permutes_sing - apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq del: One_nat_def) - apply (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31) One_nat_def) + apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq) + apply (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31)) by (simp add: ring_simps) qed diff -r ac50e7dedf6d -r 638b088bb840 src/HOL/Library/Euclidean_Space.thy --- a/src/HOL/Library/Euclidean_Space.thy Wed Mar 18 22:17:23 2009 +0100 +++ b/src/HOL/Library/Euclidean_Space.thy Thu Mar 19 01:29:19 2009 -0700 @@ -13,32 +13,50 @@ text{* Some common special cases.*} -lemma forall_1: "(\(i::'a::{order,one}). 1 <= i \ i <= 1 --> P i) \ P 1" - by (metis order_eq_iff) -lemma forall_dimindex_1: "(\i \ {1..dimindex(UNIV:: 1 set)}. P i) \ P 1" - by (simp add: dimindex_def) - -lemma forall_2: "(\(i::nat). 1 <= i \ i <= 2 --> P i) \ P 1 \ P 2" -proof- - have "\i::nat. 1 <= i \ i <= 2 \ i = 1 \ i = 2" by arith - thus ?thesis by metis +lemma forall_1: "(\i::1. P i) \ P 1" + by (metis num1_eq_iff) + +lemma exhaust_2: + fixes x :: 2 shows "x = 1 \ x = 2" +proof (induct x) + case (of_int z) + then have "0 <= z" and "z < 2" by simp_all + then have "z = 0 | z = 1" by arith + then show ?case by auto qed -lemma forall_3: "(\(i::nat). 1 <= i \ i <= 3 --> P i) \ P 1 \ P 2 \ P 3" -proof- - have "\i::nat. 1 <= i \ i <= 3 \ i = 1 \ i = 2 \ i = 3" by arith - thus ?thesis by metis +lemma forall_2: "(\i::2. P i) \ P 1 \ P 2" + by (metis exhaust_2) + +lemma exhaust_3: + fixes x :: 3 shows "x = 1 \ x = 2 \ x = 3" +proof (induct x) + case (of_int z) + then have "0 <= z" and "z < 3" by simp_all + then have "z = 0 \ z = 1 \ z = 2" by arith + then show ?case by auto qed -lemma setsum_singleton[simp]: "setsum f {x} = f x" by simp -lemma setsum_1: "setsum f {(1::'a::{order,one})..1} = f 1" - by (simp add: atLeastAtMost_singleton) - -lemma setsum_2: "setsum f {1::nat..2} = f 1 + f 2" - by (simp add: nat_number atLeastAtMostSuc_conv add_commute) - -lemma setsum_3: "setsum f {1::nat..3} = f 1 + f 2 + f 3" - by (simp add: nat_number atLeastAtMostSuc_conv add_commute) +lemma forall_3: "(\i::3. P i) \ P 1 \ P 2 \ P 3" + by (metis exhaust_3) + +lemma UNIV_1: "UNIV = {1::1}" + by (auto simp add: num1_eq_iff) + +lemma UNIV_2: "UNIV = {1::2, 2::2}" + using exhaust_2 by auto + +lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}" + using exhaust_3 by auto + +lemma setsum_1: "setsum f (UNIV::1 set) = f 1" + unfolding UNIV_1 by simp + +lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2" + unfolding UNIV_2 by simp + +lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3" + unfolding UNIV_3 by (simp add: add_ac) subsection{* Basic componentwise operations on vectors. *} @@ -76,10 +94,8 @@ instantiation "^" :: (ord,type) ord begin definition vector_less_eq_def: - "less_eq (x :: 'a ^'b) y = (ALL i : {1 .. dimindex (UNIV :: 'b set)}. - x$i <= y$i)" -definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i : {1 .. - dimindex (UNIV :: 'b set)}. x$i < y$i)" + "less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)" +definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x$i < y$i)" instance by (intro_classes) end @@ -102,19 +118,19 @@ text{* Dot products. *} definition dot :: "'a::{comm_monoid_add, times} ^ 'n \ 'a ^ 'n \ 'a" (infix "\" 70) where - "x \ y = setsum (\i. x$i * y$i) {1 .. dimindex (UNIV:: 'n set)}" + "x \ y = setsum (\i. x$i * y$i) UNIV" + lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \ y = (x$1) * (y$1)" - by (simp add: dot_def dimindex_def) + by (simp add: dot_def setsum_1) lemma dot_2[simp]: "(x::'a::{comm_monoid_add, times}^2) \ y = (x$1) * (y$1) + (x$2) * (y$2)" - by (simp add: dot_def dimindex_def nat_number) + by (simp add: dot_def setsum_2) lemma dot_3[simp]: "(x::'a::{comm_monoid_add, times}^3) \ y = (x$1) * (y$1) + (x$2) * (y$2) + (x$3) * (y$3)" - by (simp add: dot_def dimindex_def nat_number) + by (simp add: dot_def setsum_3) subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *} -lemmas Cart_lambda_beta' = Cart_lambda_beta[rule_format] method_setup vector = {* let val ss1 = HOL_basic_ss addsimps [@{thm dot_def}, @{thm setsum_addf} RS sym, @@ -125,7 +141,7 @@ @{thm vector_minus_def}, @{thm vector_uminus_def}, @{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def}, @{thm vector_scaleR_def}, - @{thm Cart_lambda_beta'}, @{thm vector_scalar_mult_def}] + @{thm Cart_lambda_beta}, @{thm vector_scalar_mult_def}] fun vector_arith_tac ths = simp_tac ss1 THEN' (fn i => rtac @{thm setsum_cong2} i @@ -145,39 +161,38 @@ text{* Obvious "component-pushing". *} -lemma vec_component: " i \ {1 .. dimindex (UNIV :: 'n set)} \ (vec x :: 'a ^ 'n)$i = x" +lemma vec_component [simp]: "(vec x :: 'a ^ 'n)$i = x" by (vector vec_def) -lemma vector_add_component: - fixes x y :: "'a::{plus} ^ 'n" assumes i: "i \ {1 .. dimindex(UNIV:: 'n set)}" +lemma vector_add_component [simp]: + fixes x y :: "'a::{plus} ^ 'n" shows "(x + y)$i = x$i + y$i" - using i by vector - -lemma vector_minus_component: - fixes x y :: "'a::{minus} ^ 'n" assumes i: "i \ {1 .. dimindex(UNIV:: 'n set)}" + by vector + +lemma vector_minus_component [simp]: + fixes x y :: "'a::{minus} ^ 'n" shows "(x - y)$i = x$i - y$i" - using i by vector - -lemma vector_mult_component: - fixes x y :: "'a::{times} ^ 'n" assumes i: "i \ {1 .. dimindex(UNIV:: 'n set)}" + by vector + +lemma vector_mult_component [simp]: + fixes x y :: "'a::{times} ^ 'n" shows "(x * y)$i = x$i * y$i" - using i by vector - -lemma vector_smult_component: - fixes y :: "'a::{times} ^ 'n" assumes i: "i \ {1 .. dimindex(UNIV:: 'n set)}" + by vector + +lemma vector_smult_component [simp]: + fixes y :: "'a::{times} ^ 'n" shows "(c *s y)$i = c * (y$i)" - using i by vector - -lemma vector_uminus_component: - fixes x :: "'a::{uminus} ^ 'n" assumes i: "i \ {1 .. dimindex(UNIV:: 'n set)}" + by vector + +lemma vector_uminus_component [simp]: + fixes x :: "'a::{uminus} ^ 'n" shows "(- x)$i = - (x$i)" - using i by vector - -lemma vector_scaleR_component: + by vector + +lemma vector_scaleR_component [simp]: fixes x :: "'a::scaleR ^ 'n" - assumes i: "i \ {1 .. dimindex(UNIV :: 'n set)}" shows "(scaleR r x)$i = scaleR r (x$i)" - using i by vector + by vector lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector @@ -250,7 +265,7 @@ instance "^" :: (semiring_0,type) semiring_0 apply (intro_classes) by (vector ring_simps)+ instance "^" :: (semiring_1,type) semiring_1 - apply (intro_classes) apply vector using dimindex_ge_1 by auto + apply (intro_classes) by vector instance "^" :: (comm_semiring,type) comm_semiring apply (intro_classes) by (vector ring_simps)+ @@ -274,16 +289,16 @@ instance "^" :: (real_algebra_1,type) real_algebra_1 .. lemma of_nat_index: - "i\{1 .. dimindex (UNIV :: 'n set)} \ (of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n" + "(of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n" apply (induct n) apply vector apply vector done lemma zero_index[simp]: - "i\{1 .. dimindex (UNIV :: 'n set)} \ (0 :: 'a::zero ^'n)$i = 0" by vector + "(0 :: 'a::zero ^'n)$i = 0" by vector lemma one_index[simp]: - "i\{1 .. dimindex (UNIV :: 'n set)} \ (1 :: 'a::one ^'n)$i = 1" by vector + "(1 :: 'a::one ^'n)$i = 1" by vector lemma one_plus_of_nat_neq_0: "(1::'a::semiring_char_0) + of_nat n \ 0" proof- @@ -296,28 +311,7 @@ proof (intro_classes) fix m n ::nat show "(of_nat m :: 'a^'b) = of_nat n \ m = n" - proof(induct m arbitrary: n) - case 0 thus ?case apply vector - apply (induct n,auto simp add: ring_simps) - using dimindex_ge_1 apply auto - apply vector - by (auto simp add: of_nat_index one_plus_of_nat_neq_0) - next - case (Suc n m) - thus ?case apply vector - apply (induct m, auto simp add: ring_simps of_nat_index zero_index) - using dimindex_ge_1 apply simp apply blast - apply (simp add: one_plus_of_nat_neq_0) - using dimindex_ge_1 apply simp apply blast - apply (simp add: vector_component one_index of_nat_index) - apply (simp only: of_nat.simps(2)[where ?'a = 'a, symmetric] of_nat_eq_iff) - using dimindex_ge_1 apply simp apply blast - apply (simp add: vector_component one_index of_nat_index) - apply (simp only: of_nat.simps(2)[where ?'a = 'a, symmetric] of_nat_eq_iff) - using dimindex_ge_1 apply simp apply blast - apply (simp add: vector_component one_index of_nat_index) - done - qed + by (simp add: Cart_eq of_nat_index) qed instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes @@ -341,8 +335,7 @@ by (vector ring_simps) lemma vec_eq[simp]: "(vec m = vec n) \ (m = n)" - apply (auto simp add: vec_def Cart_eq vec_component Cart_lambda_beta ) - using dimindex_ge_1 apply auto done + by (simp add: Cart_eq) subsection {* Square root of sum of squares *} @@ -513,11 +506,11 @@ subsection {* Norms *} -instantiation "^" :: (real_normed_vector, type) real_normed_vector +instantiation "^" :: (real_normed_vector, finite) real_normed_vector begin definition vector_norm_def: - "norm (x::'a^'b) = setL2 (\i. norm (x$i)) {1 .. dimindex (UNIV:: 'b set)}" + "norm (x::'a^'b) = setL2 (\i. norm (x$i)) UNIV" definition vector_sgn_def: "sgn (x::'a^'b) = scaleR (inverse (norm x)) x" @@ -533,14 +526,11 @@ show "norm (x + y) \ norm x + norm y" unfolding vector_norm_def apply (rule order_trans [OF _ setL2_triangle_ineq]) - apply (rule setL2_mono) - apply (simp add: vector_component norm_triangle_ineq) - apply simp + apply (simp add: setL2_mono norm_triangle_ineq) done show "norm (scaleR a x) = \a\ * norm x" unfolding vector_norm_def - by (simp add: vector_component norm_scaleR setL2_right_distrib - cong: strong_setL2_cong) + by (simp add: norm_scaleR setL2_right_distrib) show "sgn x = scaleR (inverse (norm x)) x" by (rule vector_sgn_def) qed @@ -549,11 +539,11 @@ subsection {* Inner products *} -instantiation "^" :: (real_inner, type) real_inner +instantiation "^" :: (real_inner, finite) real_inner begin definition vector_inner_def: - "inner x y = setsum (\i. inner (x$i) (y$i)) {1 .. dimindex(UNIV::'b set)}" + "inner x y = setsum (\i. inner (x$i) (y$i)) UNIV" instance proof fix r :: real and x y z :: "'a ^ 'b" @@ -562,10 +552,10 @@ by (simp add: inner_commute) show "inner (x + y) z = inner x z + inner y z" unfolding vector_inner_def - by (vector inner_left_distrib) + by (simp add: inner_left_distrib setsum_addf) show "inner (scaleR r x) y = r * inner x y" unfolding vector_inner_def - by (vector inner_scaleR_left) + by (simp add: inner_scaleR_left setsum_right_distrib) show "0 \ inner x x" unfolding vector_inner_def by (simp add: setsum_nonneg) @@ -613,25 +603,16 @@ show ?case by (simp add: h) qed -lemma dot_eq_0: "x \ x = 0 \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0" -proof- - {assume f: "finite (UNIV :: 'n set)" - let ?S = "{Suc 0 .. card (UNIV :: 'n set)}" - have fS: "finite ?S" using f by simp - have fp: "\ i\ ?S. x$i * x$i>= 0" by simp - have ?thesis by (vector dimindex_def f setsum_squares_eq_0_iff[OF fS fp])} - moreover - {assume "\ finite (UNIV :: 'n set)" then have ?thesis by (vector dimindex_def)} - ultimately show ?thesis by metis -qed - -lemma dot_pos_lt[simp]: "(0 < x \ x) \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \ 0" using dot_eq_0[of x] dot_pos_le[of x] +lemma dot_eq_0: "x \ x = 0 \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n::finite) = 0" + by (simp add: dot_def setsum_squares_eq_0_iff Cart_eq) + +lemma dot_pos_lt[simp]: "(0 < x \ x) \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n::finite) \ 0" using dot_eq_0[of x] dot_pos_le[of x] by (auto simp add: le_less) subsection{* The collapse of the general concepts to dimension one. *} lemma vector_one: "(x::'a ^1) = (\ i. (x$1))" - by (vector dimindex_def) + by (simp add: Cart_eq forall_1) lemma forall_one: "(\(x::'a ^1). P x) \ (\x. P(\ i. x))" apply auto @@ -640,7 +621,7 @@ done lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)" - by (simp add: vector_norm_def dimindex_def) + by (simp add: vector_norm_def UNIV_1) lemma norm_real: "norm(x::real ^ 1) = abs(x$1)" by (simp add: norm_vector_1) @@ -648,17 +629,16 @@ text{* Metric *} text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *} -definition dist:: "real ^ 'n \ real ^ 'n \ real" where +definition dist:: "real ^ 'n::finite \ real ^ 'n \ real" where "dist x y = norm (x - y)" lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))" - using dimindex_ge_1[of "UNIV :: 1 set"] - by (auto simp add: norm_real dist_def vector_component Cart_lambda_beta[where ?'a = "1"] ) + by (auto simp add: norm_real dist_def) subsection {* A connectedness or intermediate value lemma with several applications. *} lemma connected_real_lemma: - fixes f :: "real \ real ^ 'n" + fixes f :: "real \ real ^ 'n::finite" assumes ab: "a \ b" and fa: "f a \ e1" and fb: "f b \ e2" and dst: "\e x. a <= x \ x <= b \ 0 < e ==> \d > 0. \y. abs(y - x) < d \ dist(f y) (f x) < e" and e1: "\y \ e1. \e > 0. \y'. dist y' y < e \ y' \ e1" @@ -758,7 +738,11 @@ text{* Hence derive more interesting properties of the norm. *} -lemma norm_0[simp]: "norm (0::real ^ 'n) = 0" +text {* + This type-specific version is only here + to make @{text normarith.ML} happy. +*} +lemma norm_0: "norm (0::real ^ _) = 0" by (rule norm_zero) lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x" @@ -770,7 +754,7 @@ by (simp add: vector_norm_def setL2_def dot_def power2_eq_square) lemma norm_pow_2: "norm x ^ 2 = x \ x" by (simp add: real_vector_norm_def) -lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero) +lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n::finite)" by (metis norm_eq_zero) lemma vector_mul_eq_0[simp]: "(a *s x = 0) \ a = (0::'a::idom) \ x = 0" by vector lemma vector_mul_lcancel[simp]: "a *s x = a *s y \ a = (0::real) \ x = y" @@ -781,7 +765,9 @@ by (metis vector_mul_lcancel) lemma vector_mul_rcancel_imp: "x \ 0 \ (a::real) *s x = b *s x ==> a = b" by (metis vector_mul_rcancel) -lemma norm_cauchy_schwarz: "x \ y <= norm x * norm y" +lemma norm_cauchy_schwarz: + fixes x y :: "real ^ 'n::finite" + shows "x \ y <= norm x * norm y" proof- {assume "norm x = 0" hence ?thesis by (simp add: dot_lzero dot_rzero)} @@ -802,50 +788,74 @@ ultimately show ?thesis by metis qed -lemma norm_cauchy_schwarz_abs: "\x \ y\ \ norm x * norm y" +lemma norm_cauchy_schwarz_abs: + fixes x y :: "real ^ 'n::finite" + shows "\x \ y\ \ norm x * norm y" using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"] by (simp add: real_abs_def dot_rneg) -lemma norm_triangle_sub: "norm (x::real ^'n) <= norm(y) + norm(x - y)" +lemma norm_triangle_sub: "norm (x::real ^'n::finite) <= norm(y) + norm(x - y)" using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps) -lemma norm_triangle_le: "norm(x::real ^'n) + norm y <= e ==> norm(x + y) <= e" +lemma norm_triangle_le: "norm(x::real ^'n::finite) + norm y <= e ==> norm(x + y) <= e" by (metis order_trans norm_triangle_ineq) -lemma norm_triangle_lt: "norm(x::real ^'n) + norm(y) < e ==> norm(x + y) < e" +lemma norm_triangle_lt: "norm(x::real ^'n::finite) + norm(y) < e ==> norm(x + y) < e" by (metis basic_trans_rules(21) norm_triangle_ineq) -lemma component_le_norm: "i \ {1 .. dimindex(UNIV :: 'n set)} ==> \x$i\ <= norm (x::real ^ 'n)" +lemma setsum_delta: + assumes fS: "finite S" + shows "setsum (\k. if k=a then b k else 0) S = (if a \ S then b a else 0)" +proof- + let ?f = "(\k. if k=a then b k else 0)" + {assume a: "a \ S" + hence "\ k\ S. ?f k = 0" by simp + hence ?thesis using a by simp} + moreover + {assume a: "a \ S" + let ?A = "S - {a}" + let ?B = "{a}" + have eq: "S = ?A \ ?B" using a by blast + have dj: "?A \ ?B = {}" by simp + from fS have fAB: "finite ?A" "finite ?B" by auto + have "setsum ?f S = setsum ?f ?A + setsum ?f ?B" + using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] + by simp + then have ?thesis using a by simp} + ultimately show ?thesis by blast +qed + +lemma component_le_norm: "\x$i\ <= norm (x::real ^ 'n::finite)" apply (simp add: vector_norm_def) apply (rule member_le_setL2, simp_all) done -lemma norm_bound_component_le: "norm(x::real ^ 'n) <= e - ==> \i \ {1 .. dimindex(UNIV:: 'n set)}. \x$i\ <= e" +lemma norm_bound_component_le: "norm(x::real ^ 'n::finite) <= e + ==> \x$i\ <= e" by (metis component_le_norm order_trans) -lemma norm_bound_component_lt: "norm(x::real ^ 'n) < e - ==> \i \ {1 .. dimindex(UNIV:: 'n set)}. \x$i\ < e" +lemma norm_bound_component_lt: "norm(x::real ^ 'n::finite) < e + ==> \x$i\ < e" by (metis component_le_norm basic_trans_rules(21)) -lemma norm_le_l1: "norm (x:: real ^'n) <= setsum(\i. \x$i\) {1..dimindex(UNIV::'n set)}" +lemma norm_le_l1: "norm (x:: real ^'n::finite) <= setsum(\i. \x$i\) UNIV" by (simp add: vector_norm_def setL2_le_setsum) -lemma real_abs_norm[simp]: "\ norm x\ = norm (x :: real ^'n)" +lemma real_abs_norm: "\norm x\ = norm (x :: real ^ _)" by (rule abs_norm_cancel) -lemma real_abs_sub_norm: "\norm(x::real ^'n) - norm y\ <= norm(x - y)" +lemma real_abs_sub_norm: "\norm(x::real ^'n::finite) - norm y\ <= norm(x - y)" by (rule norm_triangle_ineq3) -lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \ x \ x <= y \ y" +lemma norm_le: "norm(x::real ^ _) <= norm(y) \ x \ x <= y \ y" by (simp add: real_vector_norm_def) -lemma norm_lt: "norm(x::real ^'n) < norm(y) \ x \ x < y \ y" +lemma norm_lt: "norm(x::real ^ _) < norm(y) \ x \ x < y \ y" by (simp add: real_vector_norm_def) -lemma norm_eq: "norm (x::real ^'n) = norm y \ x \ x = y \ y" +lemma norm_eq: "norm (x::real ^ _) = norm y \ x \ x = y \ y" by (simp add: order_eq_iff norm_le) -lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \ x \ x = 1" +lemma norm_eq_1: "norm(x::real ^ _) = 1 \ x \ x = 1" by (simp add: real_vector_norm_def) text{* Squaring equations and inequalities involving norms. *} lemma dot_square_norm: "x \ x = norm(x)^2" - by (simp add: real_vector_norm_def dot_pos_le ) + by (simp add: real_vector_norm_def) lemma norm_eq_square: "norm(x) = a \ 0 <= a \ x \ x = a^2" by (auto simp add: real_vector_norm_def) @@ -885,7 +895,7 @@ text{* Equality of vectors in terms of @{term "op \"} products. *} -lemma vector_eq: "(x:: real ^ 'n) = y \ x \ x = x \ y\ y \ y = x \ x" (is "?lhs \ ?rhs") +lemma vector_eq: "(x:: real ^ 'n::finite) = y \ x \ x = x \ y\ y \ y = x \ x" (is "?lhs \ ?rhs") proof assume "?lhs" then show ?rhs by simp next @@ -907,7 +917,7 @@ done (* FIXME: Move all these theorems into the ML code using lemma antiquotation *) -lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n) \ b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)" +lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n::finite) \ b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)" apply (rule norm_triangle_le) by simp lemma ge_iff_diff_ge_0: "(a::'a::ordered_ring) \ b == a - b \ 0" @@ -936,13 +946,13 @@ "(c *s x + w) + (d *s y + z) == d *s y + ((c *s x + w) + z)" by ((atomize (full)), vector)+ lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector -lemma norm_imp_pos_and_ge: "norm (x::real ^ 'n) == n \ norm x \ 0 \ n \ norm x" +lemma norm_imp_pos_and_ge: "norm (x::real ^ _) == n \ norm x \ 0 \ n \ norm x" by (atomize) (auto simp add: norm_ge_zero) lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \ 0 \ -x \ 0" by arith lemma norm_pths: - "(x::real ^'n) = y \ norm (x - y) \ 0" + "(x::real ^'n::finite) = y \ norm (x - y) \ 0" "x \ y \ \ (norm (x - y) \ 0)" using norm_ge_zero[of "x - y"] by auto @@ -988,13 +998,13 @@ lemma dist_le_0[simp]: "dist x y <= 0 \ x = y" by norm +lemma setsum_component [simp]: + fixes f:: " 'a \ ('b::comm_monoid_add) ^'n" + shows "(setsum f S)$i = setsum (\x. (f x)$i) S" + by (cases "finite S", induct S set: finite, simp_all) + lemma setsum_eq: "setsum f S = (\ i. setsum (\x. (f x)$i ) S)" - apply vector - apply auto - apply (cases "finite S") - apply (rule finite_induct[of S]) - apply (auto simp add: vector_component zero_index) - done + by (simp add: Cart_eq) lemma setsum_clauses: shows "setsum f {} = 0" @@ -1005,13 +1015,7 @@ lemma setsum_cmul: fixes f:: "'c \ ('a::semiring_1)^'n" shows "setsum (\x. c *s f x) S = c *s setsum f S" - by (simp add: setsum_eq Cart_eq Cart_lambda_beta vector_component setsum_right_distrib) - -lemma setsum_component: - fixes f:: " 'a \ ('b::semiring_1) ^'n" - assumes i: "i \ {1 .. dimindex(UNIV:: 'n set)}" - shows "(setsum f S)$i = setsum (\x. (f x)$i) S" - using i by (simp add: setsum_eq Cart_lambda_beta) + by (simp add: Cart_eq setsum_right_distrib) lemma setsum_norm: fixes f :: "'a \ 'b::real_normed_vector" @@ -1028,7 +1032,7 @@ qed lemma real_setsum_norm: - fixes f :: "'a \ real ^'n" + fixes f :: "'a \ real ^'n::finite" assumes fS: "finite S" shows "norm (setsum f S) <= setsum (\x. norm(f x)) S" proof(induct rule: finite_induct[OF fS]) @@ -1054,7 +1058,7 @@ qed lemma real_setsum_norm_le: - fixes f :: "'a \ real ^ 'n" + fixes f :: "'a \ real ^ 'n::finite" assumes fS: "finite S" and fg: "\x \ S. norm (f x) \ g x" shows "norm (setsum f S) \ setsum g S" @@ -1074,7 +1078,7 @@ by simp lemma real_setsum_norm_bound: - fixes f :: "'a \ real ^ 'n" + fixes f :: "'a \ real ^ 'n::finite" assumes fS: "finite S" and K: "\x \ S. norm (f x) \ K" shows "norm (setsum f S) \ of_nat (card S) * K" @@ -1155,13 +1159,13 @@ by (auto intro: setsum_0') lemma vsum_norm_allsubsets_bound: - fixes f:: "'a \ real ^'n" + fixes f:: "'a \ real ^'n::finite" assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (setsum f Q) \ e" - shows "setsum (\x. norm (f x)) P \ 2 * real (dimindex(UNIV :: 'n set)) * e" + shows "setsum (\x. norm (f x)) P \ 2 * real CARD('n) * e" proof- - let ?d = "real (dimindex (UNIV ::'n set))" + let ?d = "real CARD('n)" let ?nf = "\x. norm (f x)" - let ?U = "{1 .. dimindex (UNIV :: 'n set)}" + let ?U = "UNIV :: 'n set" have th0: "setsum (\x. setsum (\i. \f x $ i\) ?U) P = setsum (\i. setsum (\x. \f x $ i\) P) ?U" by (rule setsum_commute) have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def) @@ -1178,11 +1182,11 @@ have thp0: "?Pp \ ?Pn ={}" by auto have PpP: "?Pp \ P" and PnP: "?Pn \ P" by blast+ have Ppe:"setsum (\x. \f x $ i\) ?Pp \ e" - using i component_le_norm[OF i, of "setsum (\x. f x) ?Pp"] fPs[OF PpP] - by (auto simp add: setsum_component intro: abs_le_D1) + using component_le_norm[of "setsum (\x. f x) ?Pp" i] fPs[OF PpP] + by (auto intro: abs_le_D1) have Pne: "setsum (\x. \f x $ i\) ?Pn \ e" - using i component_le_norm[OF i, of "setsum (\x. - f x) ?Pn"] fPs[OF PnP] - by (auto simp add: setsum_negf setsum_component vector_component intro: abs_le_D1) + using component_le_norm[of "setsum (\x. - f x) ?Pn" i] fPs[OF PnP] + by (auto simp add: setsum_negf intro: abs_le_D1) 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) @@ -1204,32 +1208,29 @@ definition "basis k = (\ i. if i = k then 1 else 0)" +lemma basis_component [simp]: "basis k $ i = (if k=i then 1 else 0)" + unfolding basis_def by simp + lemma delta_mult_idempotent: "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by (cases "k=a", auto) lemma norm_basis: - assumes k: "k \ {1 .. dimindex (UNIV :: 'n set)}" - shows "norm (basis k :: real ^'n) = 1" - using k + shows "norm (basis k :: real ^'n::finite) = 1" apply (simp add: basis_def real_vector_norm_def dot_def) apply (vector delta_mult_idempotent) - using setsum_delta[of "{1 .. dimindex (UNIV :: 'n set)}" "k" "\k. 1::real"] + using setsum_delta[of "UNIV :: 'n set" "k" "\k. 1::real"] apply auto done -lemma norm_basis_1: "norm(basis 1 :: real ^'n) = 1" - apply (simp add: basis_def real_vector_norm_def dot_def) - apply (vector delta_mult_idempotent) - using setsum_delta[of "{1 .. dimindex (UNIV :: 'n set)}" "1" "\k. 1::real"] dimindex_nonzero[of "UNIV :: 'n set"] - apply auto - done - -lemma vector_choose_size: "0 <= c ==> \(x::real^'n). norm x = c" - apply (rule exI[where x="c *s basis 1"]) - by (simp only: norm_mul norm_basis_1) +lemma norm_basis_1: "norm(basis 1 :: real ^'n::{finite,one}) = 1" + by (rule norm_basis) + +lemma vector_choose_size: "0 <= c ==> \(x::real^'n::finite). norm x = c" + apply (rule exI[where x="c *s basis arbitrary"]) + by (simp only: norm_mul norm_basis) lemma vector_choose_dist: assumes e: "0 <= e" - shows "\(y::real^'n). dist x y = e" + shows "\(y::real^'n::finite). dist x y = e" proof- from vector_choose_size[OF e] obtain c:: "real ^'n" where "norm c = e" by blast @@ -1237,56 +1238,50 @@ then show ?thesis by blast qed -lemma basis_inj: "inj_on (basis :: nat \ real ^'n) {1 .. dimindex (UNIV :: 'n set)}" - by (auto simp add: inj_on_def basis_def Cart_eq Cart_lambda_beta) - -lemma basis_component: "i \ {1 .. dimindex(UNIV:: 'n set)} ==> (basis k ::('a::semiring_1)^'n)$i = (if k=i then 1 else 0)" - by (simp add: basis_def Cart_lambda_beta) +lemma basis_inj: "inj (basis :: 'n \ real ^'n::finite)" + by (simp add: inj_on_def Cart_eq) lemma cond_value_iff: "f (if b then x else y) = (if b then f x else f y)" by auto lemma basis_expansion: - "setsum (\i. (x$i) *s basis i) {1 .. dimindex (UNIV :: 'n set)} = (x::('a::ring_1) ^'n)" (is "?lhs = ?rhs" is "setsum ?f ?S = _") - by (auto simp add: Cart_eq basis_component[where ?'n = "'n"] setsum_component vector_component cond_value_iff setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong) + "setsum (\i. (x$i) *s basis i) UNIV = (x::('a::ring_1) ^'n::finite)" (is "?lhs = ?rhs" is "setsum ?f ?S = _") + by (auto simp add: Cart_eq cond_value_iff setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong) lemma basis_expansion_unique: - "setsum (\i. f i *s basis i) {1 .. dimindex (UNIV :: 'n set)} = (x::('a::comm_ring_1) ^'n) \ (\i\{1 .. dimindex(UNIV:: 'n set)}. f i = x$i)" - by (simp add: Cart_eq setsum_component vector_component basis_component setsum_delta cond_value_iff cong del: if_weak_cong) + "setsum (\i. f i *s basis i) UNIV = (x::('a::comm_ring_1) ^'n::finite) \ (\i. f i = x$i)" + by (simp add: Cart_eq setsum_delta cond_value_iff cong del: if_weak_cong) lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" by auto lemma dot_basis: - assumes i: "i \ {1 .. dimindex (UNIV :: 'n set)}" - shows "basis i \ x = x$i" "x \ (basis i :: 'a^'n) = (x$i :: 'a::semiring_1)" - using i - by (auto simp add: dot_def basis_def Cart_lambda_beta cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong) - -lemma basis_eq_0: "basis i = (0::'a::semiring_1^'n) \ i \ {1..dimindex(UNIV ::'n set)}" - by (auto simp add: Cart_eq basis_component zero_index) + shows "basis i \ x = x$i" "x \ (basis i :: 'a^'n::finite) = (x$i :: 'a::semiring_1)" + by (auto simp add: dot_def basis_def cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong) + +lemma basis_eq_0: "basis i = (0::'a::semiring_1^'n) \ False" + by (auto simp add: Cart_eq) lemma basis_nonzero: - assumes k: "k \ {1 .. dimindex(UNIV ::'n set)}" shows "basis k \ (0:: 'a::semiring_1 ^'n)" - using k by (simp add: basis_eq_0) - -lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = (z::'a::semiring_1^'n)" + by (simp add: basis_eq_0) + +lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = (z::'a::semiring_1^'n::finite)" apply (auto simp add: Cart_eq dot_basis) apply (erule_tac x="basis i" in allE) apply (simp add: dot_basis) apply (subgoal_tac "y = z") apply simp - apply vector + apply (simp add: Cart_eq) done -lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = (y::'a::semiring_1^'n)" +lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = (y::'a::semiring_1^'n::finite)" apply (auto simp add: Cart_eq dot_basis) apply (erule_tac x="basis i" in allE) apply (simp add: dot_basis) apply (subgoal_tac "x = y") apply simp - apply vector + apply (simp add: Cart_eq) done subsection{* Orthogonality. *} @@ -1294,16 +1289,12 @@ definition "orthogonal x y \ (x \ y = 0)" lemma orthogonal_basis: - assumes i:"i \ {1 .. dimindex(UNIV ::'n set)}" - shows "orthogonal (basis i :: 'a^'n) x \ x$i = (0::'a::ring_1)" - using i - by (auto simp add: orthogonal_def dot_def basis_def Cart_lambda_beta cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong) + shows "orthogonal (basis i :: 'a^'n::finite) x \ x$i = (0::'a::ring_1)" + by (auto simp add: orthogonal_def dot_def basis_def cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong) lemma orthogonal_basis_basis: - assumes i:"i \ {1 .. dimindex(UNIV ::'n set)}" - and j: "j \ {1 .. dimindex(UNIV ::'n set)}" - shows "orthogonal (basis i :: 'a::ring_1^'n) (basis j) \ i \ j" - unfolding orthogonal_basis[OF i] basis_component[OF i] by simp + shows "orthogonal (basis i :: 'a::ring_1^'n::finite) (basis j) \ i \ j" + unfolding orthogonal_basis[of i] basis_component[of j] by simp (* FIXME : Maybe some of these require less than comm_ring, but not all*) lemma orthogonal_clauses: @@ -1326,51 +1317,43 @@ subsection{* Explicit vector construction from lists. *} -lemma Cart_lambda_beta_1[simp]: "(Cart_lambda g)$1 = g 1" - apply (rule Cart_lambda_beta[rule_format]) - using dimindex_ge_1 apply auto done - -lemma Cart_lambda_beta_1'[simp]: "(Cart_lambda g)$(Suc 0) = g 1" - by (simp only: One_nat_def[symmetric] Cart_lambda_beta_1) - -definition "vector l = (\ i. if i <= length l then l ! (i - 1) else 0)" +primrec from_nat :: "nat \ 'a::{monoid_add,one}" +where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n" + +lemma from_nat [simp]: "from_nat = of_nat" +by (rule ext, induct_tac x, simp_all) + +primrec + list_fun :: "nat \ _ list \ _ \ _" +where + "list_fun n [] = (\x. 0)" +| "list_fun n (x # xs) = fun_upd (list_fun (Suc n) xs) (from_nat n) x" + +definition "vector l = (\ i. list_fun 1 l i)" +(*definition "vector l = (\ i. if i <= length l then l ! (i - 1) else 0)"*) lemma vector_1: "(vector[x]) $1 = x" - using dimindex_ge_1 - by (auto simp add: vector_def Cart_lambda_beta[rule_format]) -lemma dimindex_2[simp]: "2 \ {1 .. dimindex (UNIV :: 2 set)}" - by (auto simp add: dimindex_def) -lemma dimindex_2'[simp]: "2 \ {Suc 0 .. dimindex (UNIV :: 2 set)}" - by (auto simp add: dimindex_def) -lemma dimindex_3[simp]: "2 \ {1 .. dimindex (UNIV :: 3 set)}" "3 \ {1 .. dimindex (UNIV :: 3 set)}" - by (auto simp add: dimindex_def) - -lemma dimindex_3'[simp]: "2 \ {Suc 0 .. dimindex (UNIV :: 3 set)}" "3 \ {Suc 0 .. dimindex (UNIV :: 3 set)}" - by (auto simp add: dimindex_def) + unfolding vector_def by simp lemma vector_2: "(vector[x,y]) $1 = x" "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)" - apply (simp add: vector_def) - using Cart_lambda_beta[rule_format, OF dimindex_2, of "\i. if i \ length [x,y] then [x,y] ! (i - 1) else (0::'a)"] - apply (simp only: vector_def ) - apply auto - done + unfolding vector_def by simp_all lemma vector_3: "(vector [x,y,z] ::('a::zero)^3)$1 = x" "(vector [x,y,z] ::('a::zero)^3)$2 = y" "(vector [x,y,z] ::('a::zero)^3)$3 = z" -apply (simp_all add: vector_def Cart_lambda_beta dimindex_3) - using Cart_lambda_beta[rule_format, OF dimindex_3(1), of "\i. if i \ length [x,y,z] then [x,y,z] ! (i - 1) else (0::'a)"] using Cart_lambda_beta[rule_format, OF dimindex_3(2), of "\i. if i \ length [x,y,z] then [x,y,z] ! (i - 1) else (0::'a)"] - by simp_all + unfolding vector_def by simp_all lemma forall_vector_1: "(\v::'a::zero^1. P v) \ (\x. P(vector[x]))" apply auto apply (erule_tac x="v$1" in allE) apply (subgoal_tac "vector [v$1] = v") apply simp - by (vector vector_def dimindex_def) + apply (vector vector_def) + apply (simp add: forall_1) + done lemma forall_vector_2: "(\v::'a::zero^2. P v) \ (\x y. P(vector[x, y]))" apply auto @@ -1378,9 +1361,8 @@ apply (erule_tac x="v$2" in allE) apply (subgoal_tac "vector [v$1, v$2] = v") apply simp - apply (vector vector_def dimindex_def) - apply auto - apply (subgoal_tac "i = 1 \ i =2", auto) + apply (vector vector_def) + apply (simp add: forall_2) done lemma forall_vector_3: "(\v::'a::zero^3. P v) \ (\x y z. P(vector[x, y, z]))" @@ -1390,9 +1372,8 @@ apply (erule_tac x="v$3" in allE) apply (subgoal_tac "vector [v$1, v$2, v$3] = v") apply simp - apply (vector vector_def dimindex_def) - apply auto - apply (subgoal_tac "i = 1 \ i =2 \ i = 3", auto) + apply (vector vector_def) + apply (simp add: forall_3) done subsection{* Linear functions. *} @@ -1400,7 +1381,7 @@ definition "linear f \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *s x) = c *s f x)" lemma linear_compose_cmul: "linear f ==> linear (\x. (c::'a::comm_semiring) *s f x)" - by (vector linear_def Cart_eq Cart_lambda_beta[rule_format] ring_simps) + by (vector linear_def Cart_eq ring_simps) lemma linear_compose_neg: "linear (f :: 'a ^'n \ 'a::comm_ring ^'m) ==> linear (\x. -(f(x)))" by (vector linear_def Cart_eq) @@ -1426,9 +1407,9 @@ lemma linear_vmul_component: fixes f:: "'a::semiring_1^'m \ 'a^'n" - assumes lf: "linear f" and k: "k \ {1 .. dimindex (UNIV :: 'n set)}" + assumes lf: "linear f" shows "linear (\x. f x $ k *s v)" - using lf k + using lf apply (auto simp add: linear_def ) by (vector ring_simps)+ @@ -1485,15 +1466,15 @@ qed lemma linear_bounded: - fixes f:: "real ^'m \ real ^'n" + fixes f:: "real ^'m::finite \ real ^'n::finite" assumes lf: "linear f" shows "\B. \x. norm (f x) \ B * norm x" proof- - let ?S = "{1..dimindex(UNIV:: 'm set)}" + let ?S = "UNIV:: 'm set" let ?B = "setsum (\i. norm(f(basis i))) ?S" have fS: "finite ?S" by simp {fix x:: "real ^ 'm" - let ?g = "(\i::nat. (x$i) *s (basis i) :: real ^ 'm)" + let ?g = "(\i. (x$i) *s (basis i) :: real ^ 'm)" have "norm (f x) = norm (f (setsum (\i. (x$i) *s (basis i)) ?S))" by (simp only: basis_expansion) also have "\ = norm (setsum (\i. (x$i) *s f (basis i))?S)" @@ -1501,7 +1482,7 @@ by auto finally have th0: "norm (f x) = norm (setsum (\i. (x$i) *s f (basis i))?S)" . {fix i assume i: "i \ ?S" - from component_le_norm[OF i, of x] + from component_le_norm[of x i] have "norm ((x$i) *s f (basis i :: real ^'m)) \ norm (f (basis i)) * norm x" unfolding norm_mul apply (simp only: mult_commute) @@ -1514,7 +1495,7 @@ qed lemma linear_bounded_pos: - fixes f:: "real ^'n \ real ^ 'm" + fixes f:: "real ^'n::finite \ real ^ 'm::finite" assumes lf: "linear f" shows "\B > 0. \x. norm (f x) \ B * norm x" proof- @@ -1595,12 +1576,12 @@ qed lemma bilinear_bounded: - fixes h:: "real ^'m \ real^'n \ real ^ 'k" + fixes h:: "real ^'m::finite \ real^'n::finite \ real ^ 'k::finite" assumes bh: "bilinear h" shows "\B. \x y. norm (h x y) \ B * norm x * norm y" proof- - let ?M = "{1 .. dimindex (UNIV :: 'm set)}" - let ?N = "{1 .. dimindex (UNIV :: 'n set)}" + let ?M = "UNIV :: 'm set" + let ?N = "UNIV :: 'n set" let ?B = "setsum (\(i,j). norm (h (basis i) (basis j))) (?M \ ?N)" have fM: "finite ?M" and fN: "finite ?N" by simp_all {fix x:: "real ^ 'm" and y :: "real^'n" @@ -1622,7 +1603,7 @@ qed lemma bilinear_bounded_pos: - fixes h:: "real ^'m \ real^'n \ real ^ 'k" + fixes h:: "real ^'m::finite \ real^'n::finite \ real ^ 'k::finite" assumes bh: "bilinear h" shows "\B > 0. \x y. norm (h x y) \ B * norm x * norm y" proof- @@ -1649,12 +1630,12 @@ lemma choice_iff: "(\x. \y. P x y) \ (\f. \x. P x (f x))" by metis lemma adjoint_works_lemma: - fixes f:: "'a::ring_1 ^'n \ 'a ^ 'm" + fixes f:: "'a::ring_1 ^'n::finite \ 'a ^ 'm::finite" assumes lf: "linear f" shows "\x y. f x \ y = x \ adjoint f y" proof- - let ?N = "{1 .. dimindex (UNIV :: 'n set)}" - let ?M = "{1 .. dimindex (UNIV :: 'm set)}" + let ?N = "UNIV :: 'n set" + let ?M = "UNIV :: 'm set" have fN: "finite ?N" by simp have fM: "finite ?M" by simp {fix y:: "'a ^ 'm" @@ -1667,7 +1648,7 @@ by (simp add: linear_cmul[OF lf]) finally have "f x \ y = x \ ?w" apply (simp only: ) - apply (simp add: dot_def setsum_component Cart_lambda_beta setsum_left_distrib setsum_right_distrib vector_component setsum_commute[of _ ?M ?N] ring_simps del: One_nat_def) + apply (simp add: dot_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] ring_simps) done} } then show ?thesis unfolding adjoint_def @@ -1677,34 +1658,34 @@ qed lemma adjoint_works: - fixes f:: "'a::ring_1 ^'n \ 'a ^ 'm" + fixes f:: "'a::ring_1 ^'n::finite \ 'a ^ 'm::finite" assumes lf: "linear f" shows "x \ adjoint f y = f x \ y" using adjoint_works_lemma[OF lf] by metis lemma adjoint_linear: - fixes f :: "'a::comm_ring_1 ^'n \ 'a ^ 'm" + fixes f :: "'a::comm_ring_1 ^'n::finite \ 'a ^ 'm::finite" assumes lf: "linear f" shows "linear (adjoint f)" by (simp add: linear_def vector_eq_ldot[symmetric] dot_radd dot_rmult adjoint_works[OF lf]) lemma adjoint_clauses: - fixes f:: "'a::comm_ring_1 ^'n \ 'a ^ 'm" + fixes f:: "'a::comm_ring_1 ^'n::finite \ 'a ^ 'm::finite" assumes lf: "linear f" shows "x \ adjoint f y = f x \ y" and "adjoint f y \ x = y \ f x" by (simp_all add: adjoint_works[OF lf] dot_sym ) lemma adjoint_adjoint: - fixes f:: "'a::comm_ring_1 ^ 'n \ _" + fixes f:: "'a::comm_ring_1 ^ 'n::finite \ 'a ^ 'm::finite" assumes lf: "linear f" shows "adjoint (adjoint f) = f" apply (rule ext) by (simp add: vector_eq_ldot[symmetric] adjoint_clauses[OF adjoint_linear[OF lf]] adjoint_clauses[OF lf]) lemma adjoint_unique: - fixes f:: "'a::comm_ring_1 ^ 'n \ 'a ^ 'm" + fixes f:: "'a::comm_ring_1 ^ 'n::finite \ 'a ^ 'm::finite" assumes lf: "linear f" and u: "\x y. f' x \ y = x \ f y" shows "f' = adjoint f" apply (rule ext) @@ -1716,14 +1697,14 @@ consts generic_mult :: "'a \ 'b \ 'c" (infixr "\" 75) defs (overloaded) -matrix_matrix_mult_def: "(m:: ('a::semiring_1) ^'n^'m) \ (m' :: 'a ^'p^'n) \ (\ i j. setsum (\k. ((m$i)$k) * ((m'$k)$j)) {1 .. dimindex (UNIV :: 'n set)}) ::'a ^ 'p ^'m" +matrix_matrix_mult_def: "(m:: ('a::semiring_1) ^'n^'m) \ (m' :: 'a ^'p^'n) \ (\ i j. setsum (\k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m" abbreviation matrix_matrix_mult' :: "('a::semiring_1) ^'n^'m \ 'a ^'p^'n \ 'a ^ 'p ^'m" (infixl "**" 70) where "m ** m' == m\ m'" defs (overloaded) - matrix_vector_mult_def: "(m::('a::semiring_1) ^'n^'m) \ (x::'a ^'n) \ (\ i. setsum (\j. ((m$i)$j) * (x$j)) {1..dimindex(UNIV ::'n set)}) :: 'a^'m" + matrix_vector_mult_def: "(m::('a::semiring_1) ^'n^'m) \ (x::'a ^'n) \ (\ i. setsum (\j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m" abbreviation matrix_vector_mult' :: "('a::semiring_1) ^'n^'m \ 'a ^'n \ 'a ^ 'm" (infixl "*v" 70) @@ -1731,19 +1712,19 @@ "m *v v == m \ v" defs (overloaded) - vector_matrix_mult_def: "(x::'a^'m) \ (m::('a::semiring_1) ^'n^'m) \ (\ j. setsum (\i. ((m$i)$j) * (x$i)) {1..dimindex(UNIV :: 'm set)}) :: 'a^'n" + vector_matrix_mult_def: "(x::'a^'m) \ (m::('a::semiring_1) ^'n^'m) \ (\ j. setsum (\i. ((m$i)$j) * (x$i)) (UNIV :: 'm set)) :: 'a^'n" abbreviation vactor_matrix_mult' :: "'a ^ 'm \ ('a::semiring_1) ^'n^'m \ 'a ^'n " (infixl "v*" 70) where "v v* m == v \ m" -definition "(mat::'a::zero => 'a ^'n^'m) k = (\ i j. if i = j then k else 0)" +definition "(mat::'a::zero => 'a ^'n^'n) k = (\ i j. if i = j then k else 0)" definition "(transp::'a^'n^'m \ 'a^'m^'n) A = (\ i j. ((A$j)$i))" -definition "(row::nat => 'a ^'n^'m \ 'a ^'n) i A = (\ j. ((A$i)$j))" -definition "(column::nat =>'a^'n^'m =>'a^'m) j A = (\ i. ((A$i)$j))" -definition "rows(A::'a^'n^'m) = { row i A | i. i \ {1 .. dimindex(UNIV :: 'm set)}}" -definition "columns(A::'a^'n^'m) = { column i A | i. i \ {1 .. dimindex(UNIV :: 'n set)}}" +definition "(row::'m => 'a ^'n^'m \ 'a ^'n) i A = (\ j. ((A$i)$j))" +definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\ i. ((A$i)$j))" +definition "rows(A::'a^'n^'m) = { row i A | i. i \ (UNIV :: 'm set)}" +definition "columns(A::'a^'n^'m) = { column i A | i. i \ (UNIV :: 'n set)}" lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def) lemma matrix_add_ldistrib: "(A ** (B + C)) = (A \ B) + (A \ C)" @@ -1756,16 +1737,20 @@ using setsum_delta[OF fS, of a b, symmetric] by (auto intro: setsum_cong) -lemma matrix_mul_lid: "mat 1 ** A = A" +lemma matrix_mul_lid: + fixes A :: "'a::semiring_1 ^ 'm ^ 'n::finite" + shows "mat 1 ** A = A" apply (simp add: matrix_matrix_mult_def mat_def) apply vector - by (auto simp only: cond_value_iff cond_application_beta setsum_delta'[OF finite_atLeastAtMost] mult_1_left mult_zero_left if_True) - - -lemma matrix_mul_rid: "A ** mat 1 = A" + by (auto simp only: cond_value_iff cond_application_beta setsum_delta'[OF finite] mult_1_left mult_zero_left if_True UNIV_I) + + +lemma matrix_mul_rid: + fixes A :: "'a::semiring_1 ^ 'm::finite ^ 'n" + shows "A ** mat 1 = A" apply (simp add: matrix_matrix_mult_def mat_def) apply vector - by (auto simp only: cond_value_iff cond_application_beta setsum_delta[OF finite_atLeastAtMost] mult_1_right mult_zero_right if_True cong: if_cong) + by (auto simp only: cond_value_iff cond_application_beta setsum_delta[OF finite] mult_1_right mult_zero_right if_True UNIV_I cong: if_cong) lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C" apply (vector matrix_matrix_mult_def setsum_right_distrib setsum_left_distrib mult_assoc) @@ -1779,31 +1764,31 @@ apply simp done -lemma matrix_vector_mul_lid: "mat 1 *v x = x" +lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n::finite)" apply (vector matrix_vector_mult_def mat_def) by (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong) lemma matrix_transp_mul: "transp(A ** B) = transp B ** transp (A::'a::comm_semiring_1^'m^'n)" - by (simp add: matrix_matrix_mult_def transp_def Cart_eq Cart_lambda_beta mult_commute) - -lemma matrix_eq: "A = B \ (\x. A *v x = B *v x)" (is "?lhs \ ?rhs") + by (simp add: matrix_matrix_mult_def transp_def Cart_eq mult_commute) + +lemma matrix_eq: + fixes A B :: "'a::semiring_1 ^ 'n::finite ^ 'm" + shows "A = B \ (\x. A *v x = B *v x)" (is "?lhs \ ?rhs") apply auto apply (subst Cart_eq) apply clarify - apply (clarsimp simp add: matrix_vector_mult_def basis_def cond_value_iff cond_application_beta Cart_eq Cart_lambda_beta cong del: if_weak_cong) + apply (clarsimp simp add: matrix_vector_mult_def basis_def cond_value_iff cond_application_beta Cart_eq cong del: if_weak_cong) apply (erule_tac x="basis ia" in allE) - apply (erule_tac x="i" in ballE) - by (auto simp add: basis_def cond_value_iff cond_application_beta Cart_lambda_beta setsum_delta[OF finite_atLeastAtMost] cong del: if_weak_cong) + apply (erule_tac x="i" in allE) + by (auto simp add: basis_def cond_value_iff cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong) lemma matrix_vector_mul_component: - assumes k: "k \ {1.. dimindex (UNIV :: 'm set)}" shows "((A::'a::semiring_1^'n'^'m) *v x)$k = (A$k) \ x" - using k - by (simp add: matrix_vector_mult_def Cart_lambda_beta dot_def) + by (simp add: matrix_vector_mult_def dot_def) lemma dot_lmul_matrix: "((x::'a::comm_semiring_1 ^'n) v* A) \ y = x \ (A *v y)" - apply (simp add: dot_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib Cart_lambda_beta mult_ac) + apply (simp add: dot_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac) apply (subst setsum_commute) by simp @@ -1815,23 +1800,16 @@ lemma row_transp: fixes A:: "'a::semiring_1^'n^'m" - assumes i: "i \ {1.. dimindex (UNIV :: 'n set)}" shows "row i (transp A) = column i A" - using i - by (simp add: row_def column_def transp_def Cart_eq Cart_lambda_beta) + by (simp add: row_def column_def transp_def Cart_eq) lemma column_transp: fixes A:: "'a::semiring_1^'n^'m" - assumes i: "i \ {1.. dimindex (UNIV :: 'm set)}" shows "column i (transp A) = row i A" - using i - by (simp add: row_def column_def transp_def Cart_eq Cart_lambda_beta) + by (simp add: row_def column_def transp_def Cart_eq) lemma rows_transp: "rows(transp (A::'a::semiring_1^'n^'m)) = columns A" -apply (auto simp add: rows_def columns_def row_transp intro: set_ext) -apply (rule_tac x=i in exI) -apply (auto simp add: row_transp) -done +by (auto simp add: rows_def columns_def row_transp intro: set_ext) lemma columns_transp: "columns(transp (A::'a::semiring_1^'n^'m)) = rows A" by (metis transp_transp rows_transp) @@ -1840,25 +1818,25 @@ lemma matrix_mult_dot: "A *v x = (\ i. A$i \ x)" by (simp add: matrix_vector_mult_def dot_def) -lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\i. (x$i) *s column i A) {1 .. dimindex(UNIV:: 'n set)}" - by (simp add: matrix_vector_mult_def Cart_eq setsum_component Cart_lambda_beta vector_component column_def mult_commute) +lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\i. (x$i) *s column i A) (UNIV:: 'n set)" + by (simp add: matrix_vector_mult_def Cart_eq column_def mult_commute) lemma vector_componentwise: - "(x::'a::ring_1^'n) = (\ j. setsum (\i. (x$i) * (basis i :: 'a^'n)$j) {1..dimindex(UNIV :: 'n set)})" + "(x::'a::ring_1^'n::finite) = (\ j. setsum (\i. (x$i) * (basis i :: 'a^'n)$j) (UNIV :: 'n set))" apply (subst basis_expansion[symmetric]) - by (vector Cart_eq Cart_lambda_beta setsum_component) + by (vector Cart_eq setsum_component) lemma linear_componentwise: - fixes f:: "'a::ring_1 ^ 'm \ 'a ^ 'n" - assumes lf: "linear f" and j: "j \ {1 .. dimindex (UNIV :: 'n set)}" - shows "(f x)$j = setsum (\i. (x$i) * (f (basis i)$j)) {1 .. dimindex (UNIV :: 'm set)}" (is "?lhs = ?rhs") + fixes f:: "'a::ring_1 ^ 'm::finite \ 'a ^ 'n" + assumes lf: "linear f" + shows "(f x)$j = setsum (\i. (x$i) * (f (basis i)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") proof- - let ?M = "{1 .. dimindex (UNIV :: 'm set)}" - let ?N = "{1 .. dimindex (UNIV :: 'n set)}" + let ?M = "(UNIV :: 'm set)" + let ?N = "(UNIV :: 'n set)" have fM: "finite ?M" by simp have "?rhs = (setsum (\i.(x$i) *s f (basis i) ) ?M)$j" - unfolding vector_smult_component[OF j, symmetric] - unfolding setsum_component[OF j, of "(\i.(x$i) *s f (basis i :: 'a^'m))" ?M] + unfolding vector_smult_component[symmetric] + unfolding setsum_component[of "(\i.(x$i) *s f (basis i :: 'a^'m))" ?M] .. then show ?thesis unfolding linear_setsum_mul[OF lf fM, symmetric] basis_expansion .. qed @@ -1876,38 +1854,38 @@ where "matrix f = (\ i j. (f(basis j))$i)" lemma matrix_vector_mul_linear: "linear(\x. A *v (x::'a::comm_semiring_1 ^ 'n))" - by (simp add: linear_def matrix_vector_mult_def Cart_eq Cart_lambda_beta vector_component ring_simps setsum_right_distrib setsum_addf) - -lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::'a::comm_ring_1 ^ 'n)" -apply (simp add: matrix_def matrix_vector_mult_def Cart_eq Cart_lambda_beta mult_commute del: One_nat_def) + by (simp add: linear_def matrix_vector_mult_def Cart_eq ring_simps setsum_right_distrib setsum_addf) + +lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::'a::comm_ring_1 ^ 'n::finite)" +apply (simp add: matrix_def matrix_vector_mult_def Cart_eq mult_commute) apply clarify apply (rule linear_componentwise[OF lf, symmetric]) -apply simp done -lemma matrix_vector_mul: "linear f ==> f = (\x. matrix f *v (x::'a::comm_ring_1 ^ 'n))" by (simp add: ext matrix_works) - -lemma matrix_of_matrix_vector_mul: "matrix(\x. A *v (x :: 'a:: comm_ring_1 ^ 'n)) = A" +lemma matrix_vector_mul: "linear f ==> f = (\x. matrix f *v (x::'a::comm_ring_1 ^ 'n::finite))" by (simp add: ext matrix_works) + +lemma matrix_of_matrix_vector_mul: "matrix(\x. A *v (x :: 'a:: comm_ring_1 ^ 'n::finite)) = A" by (simp add: matrix_eq matrix_vector_mul_linear matrix_works) lemma matrix_compose: - assumes lf: "linear (f::'a::comm_ring_1^'n \ _)" and lg: "linear g" + assumes lf: "linear (f::'a::comm_ring_1^'n::finite \ 'a^'m::finite)" + and lg: "linear (g::'a::comm_ring_1^'m::finite \ 'a^'k)" shows "matrix (g o f) = matrix g ** matrix f" using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]] by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) -lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\i. (x$i) *s ((transp A)$i)) {1..dimindex(UNIV:: 'n set)}" - by (simp add: matrix_vector_mult_def transp_def Cart_eq Cart_lambda_beta setsum_component vector_component mult_commute) - -lemma adjoint_matrix: "adjoint(\x. (A::'a::comm_ring_1^'n^'m) *v x) = (\x. transp A *v x)" +lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\i. (x$i) *s ((transp A)$i)) (UNIV:: 'n set)" + by (simp add: matrix_vector_mult_def transp_def Cart_eq mult_commute) + +lemma adjoint_matrix: "adjoint(\x. (A::'a::comm_ring_1^'n::finite^'m::finite) *v x) = (\x. transp A *v x)" apply (rule adjoint_unique[symmetric]) apply (rule matrix_vector_mul_linear) - apply (simp add: transp_def dot_def Cart_lambda_beta matrix_vector_mult_def setsum_left_distrib setsum_right_distrib) + apply (simp add: transp_def dot_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib) apply (subst setsum_commute) apply (auto simp add: mult_ac) done -lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n \ 'a ^ 'm)" +lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n::finite \ 'a ^ 'm::finite)" shows "matrix(adjoint f) = transp(matrix f)" apply (subst matrix_vector_mul[OF lf]) unfolding adjoint_matrix matrix_of_matrix_vector_mul .. @@ -1980,21 +1958,21 @@ qed -lemma lambda_skolem: "(\i \ {1 .. dimindex(UNIV :: 'n set)}. \x. P i x) \ - (\x::'a ^ 'n. \i \ {1 .. dimindex(UNIV:: 'n set)}. P i (x$i))" (is "?lhs \ ?rhs") +lemma lambda_skolem: "(\i. \x. P i x) \ + (\x::'a ^ 'n. \i. P i (x$i))" (is "?lhs \ ?rhs") proof- - let ?S = "{1 .. dimindex(UNIV :: 'n set)}" + let ?S = "(UNIV :: 'n set)" {assume H: "?rhs" then have ?lhs by auto} moreover {assume H: "?lhs" - then obtain f where f:"\i\ ?S. P i (f i)" unfolding Ball_def choice_iff by metis + then obtain f where f:"\i. P i (f i)" unfolding choice_iff by metis let ?x = "(\ i. (f i)) :: 'a ^ 'n" - {fix i assume i: "i \ ?S" - with f i have "P i (f i)" by metis - then have "P i (?x$i)" using Cart_lambda_beta[of f, rule_format, OF i] by auto + {fix i + from f have "P i (f i)" by metis + then have "P i (?x$i)" by auto } - hence "\i \ ?S. P i (?x$i)" by metis + hence "\i. P i (?x$i)" by metis hence ?rhs by metis } ultimately show ?thesis by metis qed @@ -2237,7 +2215,7 @@ definition "onorm f = rsup {norm (f x)| x. norm x = 1}" lemma norm_bound_generalize: - fixes f:: "real ^'n \ real^'m" + fixes f:: "real ^'n::finite \ real^'m::finite" assumes lf: "linear f" shows "(\x. norm x = 1 \ norm (f x) \ b) \ (\x. norm (f x) \ b * norm x)" (is "?lhs \ ?rhs") proof- @@ -2248,8 +2226,8 @@ moreover {assume H: ?lhs - from H[rule_format, of "basis 1"] - have bp: "b \ 0" using norm_ge_zero[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"] + from H[rule_format, of "basis arbitrary"] + have bp: "b \ 0" using norm_ge_zero[of "f (basis arbitrary)"] by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero]) {fix x :: "real ^'n" {assume "x = 0" @@ -2270,14 +2248,14 @@ qed lemma onorm: - fixes f:: "real ^'n \ real ^'m" + fixes f:: "real ^'n::finite \ real ^'m::finite" assumes lf: "linear f" shows "norm (f x) <= onorm f * norm x" and "\x. norm (f x) <= b * norm x \ onorm f <= b" proof- { let ?S = "{norm (f x) |x. norm x = 1}" - have Se: "?S \ {}" using norm_basis_1 by auto + have Se: "?S \ {}" using norm_basis by auto from linear_bounded[OF lf] have b: "\ b. ?S *<= b" unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def) {from rsup[OF Se b, unfolded onorm_def[symmetric]] @@ -2294,10 +2272,10 @@ } qed -lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \ real ^'m)" shows "0 <= onorm f" - using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp - -lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \ real ^'m)" +lemma onorm_pos_le: assumes lf: "linear (f::real ^'n::finite \ real ^'m::finite)" shows "0 <= onorm f" + using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis arbitrary"], unfolded norm_basis] by simp + +lemma onorm_eq_0: assumes lf: "linear (f::real ^'n::finite \ real ^'m::finite)" shows "onorm f = 0 \ (\x. f x = 0)" using onorm[OF lf] apply (auto simp add: onorm_pos_le) @@ -2307,7 +2285,7 @@ apply arith done -lemma onorm_const: "onorm(\x::real^'n. (y::real ^ 'm)) = norm y" +lemma onorm_const: "onorm(\x::real^'n::finite. (y::real ^ 'm::finite)) = norm y" proof- let ?f = "\x::real^'n. (y::real ^ 'm)" have th: "{norm (?f x)| x. norm x = 1} = {norm y}" @@ -2317,13 +2295,14 @@ apply (rule rsup_unique) by (simp_all add: setle_def) qed -lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n \ real ^'m)" +lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n::finite \ real ^'m::finite)" shows "0 < onorm f \ ~(\x. f x = 0)" unfolding onorm_eq_0[OF lf, symmetric] using onorm_pos_le[OF lf] by arith lemma onorm_compose: - assumes lf: "linear (f::real ^'n \ real ^'m)" and lg: "linear g" + assumes lf: "linear (f::real ^'n::finite \ real ^'m::finite)" + and lg: "linear (g::real^'k::finite \ real^'n::finite)" shows "onorm (f o g) <= onorm f * onorm g" apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format]) unfolding o_def @@ -2335,18 +2314,18 @@ apply (rule onorm_pos_le[OF lf]) done -lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \ real^'m)" +lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n::finite \ real^'m::finite)" shows "onorm (\x. - f x) \ onorm f" using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf] unfolding norm_minus_cancel by metis -lemma onorm_neg: assumes lf: "linear (f::real ^'n \ real^'m)" +lemma onorm_neg: assumes lf: "linear (f::real ^'n::finite \ real^'m::finite)" shows "onorm (\x. - f x) = onorm f" using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]] by simp lemma onorm_triangle: - assumes lf: "linear (f::real ^'n \ real ^'m)" and lg: "linear g" + assumes lf: "linear (f::real ^'n::finite \ real ^'m::finite)" and lg: "linear g" shows "onorm (\x. f x + g x) <= onorm f + onorm g" apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format]) apply (rule order_trans) @@ -2357,14 +2336,14 @@ apply (rule onorm(1)[OF lg]) done -lemma onorm_triangle_le: "linear (f::real ^'n \ real ^'m) \ linear g \ onorm(f) + onorm(g) <= e +lemma onorm_triangle_le: "linear (f::real ^'n::finite \ real ^'m::finite) \ linear g \ onorm(f) + onorm(g) <= e \ onorm(\x. f x + g x) <= e" apply (rule order_trans) apply (rule onorm_triangle) apply assumption+ done -lemma onorm_triangle_lt: "linear (f::real ^'n \ real ^'m) \ linear g \ onorm(f) + onorm(g) < e +lemma onorm_triangle_lt: "linear (f::real ^'n::finite \ real ^'m::finite) \ linear g \ onorm(f) + onorm(g) < e ==> onorm(\x. f x + g x) < e" apply (rule order_le_less_trans) apply (rule onorm_triangle) @@ -2381,7 +2360,7 @@ by (simp add: vec1_def) lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y" - by (simp_all add: vec1_def dest_vec1_def Cart_eq Cart_lambda_beta dimindex_def del: One_nat_def) + by (simp_all add: vec1_def dest_vec1_def Cart_eq forall_1) lemma forall_vec1: "(\x. P x) \ (\x. P (vec1 x))" by (metis vec1_dest_vec1) @@ -2451,21 +2430,21 @@ shows "linear f \ linear (\x. dest_vec1(f x) *s v)" unfolding dest_vec1_def apply (rule linear_vmul_component) - by (auto simp add: dimindex_def) + by auto lemma linear_from_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^1 \ 'a^'n)" shows "f = (\x. dest_vec1 x *s column 1 (matrix f))" apply (rule ext) apply (subst matrix_works[OF lf, symmetric]) - apply (auto simp add: Cart_eq matrix_vector_mult_def dest_vec1_def column_def Cart_lambda_beta vector_component dimindex_def mult_commute del: One_nat_def ) + apply (auto simp add: Cart_eq matrix_vector_mult_def dest_vec1_def column_def mult_commute UNIV_1) done -lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n \ 'a^1)" +lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n::finite \ 'a^1)" shows "f = (\x. vec1(row 1 (matrix f) \ x))" apply (rule ext) apply (subst matrix_works[OF lf, symmetric]) - apply (auto simp add: Cart_eq matrix_vector_mult_def vec1_def row_def Cart_lambda_beta vector_component dimindex_def dot_def mult_commute) + apply (simp add: Cart_eq matrix_vector_mult_def vec1_def row_def dot_def mult_commute forall_1) done lemma dest_vec1_eq_0: "dest_vec1 x = 0 \ x = 0" @@ -2485,25 +2464,25 @@ text{* Pasting vectors. *} lemma linear_fstcart: "linear fstcart" - by (auto simp add: linear_def fstcart_def Cart_eq Cart_lambda_beta vector_component dimindex_finite_sum) + by (auto simp add: linear_def Cart_eq) lemma linear_sndcart: "linear sndcart" - by (auto simp add: linear_def sndcart_def Cart_eq Cart_lambda_beta vector_component dimindex_finite_sum) + by (auto simp add: linear_def Cart_eq) lemma fstcart_vec[simp]: "fstcart(vec x) = vec x" - by (vector fstcart_def vec_def dimindex_finite_sum) - -lemma fstcart_add[simp]:"fstcart(x + y) = fstcart (x::'a::{plus,times}^('b,'c) finite_sum) + fstcart y" - using linear_fstcart[unfolded linear_def] by blast - -lemma fstcart_cmul[simp]:"fstcart(c*s x) = c*s fstcart (x::'a::{plus,times}^('b,'c) finite_sum)" - using linear_fstcart[unfolded linear_def] by blast - -lemma fstcart_neg[simp]:"fstcart(- x) = - fstcart (x::'a::ring_1^('b,'c) finite_sum)" -unfolding vector_sneg_minus1 fstcart_cmul .. - -lemma fstcart_sub[simp]:"fstcart(x - y) = fstcart (x::'a::ring_1^('b,'c) finite_sum) - fstcart y" - unfolding diff_def fstcart_add fstcart_neg .. + by (simp add: Cart_eq) + +lemma fstcart_add[simp]:"fstcart(x + y) = fstcart (x::'a::{plus,times}^('b + 'c)) + fstcart y" + by (simp add: Cart_eq) + +lemma fstcart_cmul[simp]:"fstcart(c*s x) = c*s fstcart (x::'a::{plus,times}^('b + 'c))" + by (simp add: Cart_eq) + +lemma fstcart_neg[simp]:"fstcart(- x) = - fstcart (x::'a::ring_1^('b + 'c))" + by (simp add: Cart_eq) + +lemma fstcart_sub[simp]:"fstcart(x - y) = fstcart (x::'a::ring_1^('b + 'c)) - fstcart y" + by (simp add: Cart_eq) lemma fstcart_setsum: fixes f:: "'d \ 'a::semiring_1^_" @@ -2512,19 +2491,19 @@ by (induct rule: finite_induct[OF fS], simp_all add: vec_0[symmetric] del: vec_0) lemma sndcart_vec[simp]: "sndcart(vec x) = vec x" - by (vector sndcart_def vec_def dimindex_finite_sum) - -lemma sndcart_add[simp]:"sndcart(x + y) = sndcart (x::'a::{plus,times}^('b,'c) finite_sum) + sndcart y" - using linear_sndcart[unfolded linear_def] by blast - -lemma sndcart_cmul[simp]:"sndcart(c*s x) = c*s sndcart (x::'a::{plus,times}^('b,'c) finite_sum)" - using linear_sndcart[unfolded linear_def] by blast - -lemma sndcart_neg[simp]:"sndcart(- x) = - sndcart (x::'a::ring_1^('b,'c) finite_sum)" -unfolding vector_sneg_minus1 sndcart_cmul .. - -lemma sndcart_sub[simp]:"sndcart(x - y) = sndcart (x::'a::ring_1^('b,'c) finite_sum) - sndcart y" - unfolding diff_def sndcart_add sndcart_neg .. + by (simp add: Cart_eq) + +lemma sndcart_add[simp]:"sndcart(x + y) = sndcart (x::'a::{plus,times}^('b + 'c)) + sndcart y" + by (simp add: Cart_eq) + +lemma sndcart_cmul[simp]:"sndcart(c*s x) = c*s sndcart (x::'a::{plus,times}^('b + 'c))" + by (simp add: Cart_eq) + +lemma sndcart_neg[simp]:"sndcart(- x) = - sndcart (x::'a::ring_1^('b + 'c))" + by (simp add: Cart_eq) + +lemma sndcart_sub[simp]:"sndcart(x - y) = sndcart (x::'a::ring_1^('b + 'c)) - sndcart y" + by (simp add: Cart_eq) lemma sndcart_setsum: fixes f:: "'d \ 'a::semiring_1^_" @@ -2533,10 +2512,10 @@ by (induct rule: finite_induct[OF fS], simp_all add: vec_0[symmetric] del: vec_0) lemma pastecart_vec[simp]: "pastecart (vec x) (vec x) = vec x" - by (simp add: pastecart_eq fstcart_vec sndcart_vec fstcart_pastecart sndcart_pastecart) + by (simp add: pastecart_eq fstcart_pastecart sndcart_pastecart) lemma pastecart_add[simp]:"pastecart (x1::'a::{plus,times}^_) y1 + pastecart x2 y2 = pastecart (x1 + x2) (y1 + y2)" - by (simp add: pastecart_eq fstcart_add sndcart_add fstcart_pastecart sndcart_pastecart) + by (simp add: pastecart_eq fstcart_pastecart sndcart_pastecart) lemma pastecart_cmul[simp]: "pastecart (c *s (x1::'a::{plus,times}^_)) (c *s y1) = c *s pastecart x1 y1" by (simp add: pastecart_eq fstcart_pastecart sndcart_pastecart) @@ -2553,109 +2532,53 @@ shows "pastecart (setsum f S) (setsum g S) = setsum (\i. pastecart (f i) (g i)) S" by (simp add: pastecart_eq fstcart_setsum[OF fS] sndcart_setsum[OF fS] fstcart_pastecart sndcart_pastecart) -lemma norm_fstcart: "norm(fstcart x) <= norm (x::real ^('n,'m) finite_sum)" +lemma setsum_Plus: + "\finite A; finite B\ \ + (\x\A <+> B. g x) = (\x\A. g (Inl x)) + (\x\B. g (Inr x))" + unfolding Plus_def + by (subst setsum_Un_disjoint, auto simp add: setsum_reindex) + +lemma setsum_UNIV_sum: + fixes g :: "'a::finite + 'b::finite \ _" + shows "(\x\UNIV. g x) = (\x\UNIV. g (Inl x)) + (\x\UNIV. g (Inr x))" + apply (subst UNIV_Plus_UNIV [symmetric]) + apply (rule setsum_Plus [OF finite finite]) + done + +lemma norm_fstcart: "norm(fstcart x) <= norm (x::real ^('n::finite + 'm::finite))" proof- - let ?n = "dimindex (UNIV :: 'n set)" - let ?m = "dimindex (UNIV :: 'm set)" - let ?N = "{1 .. ?n}" - let ?M = "{1 .. ?m}" - let ?NM = "{1 .. dimindex (UNIV :: ('n,'m) finite_sum set)}" - have th_0: "1 \ ?n +1" by simp have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))" by (simp add: pastecart_fst_snd) have th1: "fstcart x \ fstcart x \ pastecart (fstcart x) (sndcart x) \ pastecart (fstcart x) (sndcart x)" - by (simp add: dot_def setsum_add_split[OF th_0, of _ ?m] pastecart_def dimindex_finite_sum Cart_lambda_beta setsum_nonneg zero_le_square del: One_nat_def) + by (simp add: dot_def setsum_UNIV_sum pastecart_def setsum_nonneg) then show ?thesis unfolding th0 unfolding real_vector_norm_def real_sqrt_le_iff id_def - by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta) + by (simp add: dot_def) qed lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y" by (metis dist_def fstcart_sub[symmetric] norm_fstcart) -lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n,'m) finite_sum)" +lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))" proof- - let ?n = "dimindex (UNIV :: 'n set)" - let ?m = "dimindex (UNIV :: 'm set)" - let ?N = "{1 .. ?n}" - let ?M = "{1 .. ?m}" - let ?nm = "dimindex (UNIV :: ('n,'m) finite_sum set)" - let ?NM = "{1 .. ?nm}" - have thnm[simp]: "?nm = ?n + ?m" by (simp add: dimindex_finite_sum) - have th_0: "1 \ ?n +1" by simp have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))" by (simp add: pastecart_fst_snd) - let ?f = "\n. n - ?n" - let ?S = "{?n+1 .. ?nm}" - have finj:"inj_on ?f ?S" - using dimindex_nonzero[of "UNIV :: 'n set"] dimindex_nonzero[of "UNIV :: 'm set"] - apply (simp add: Ball_def atLeastAtMost_iff inj_on_def dimindex_finite_sum del: One_nat_def) - by arith - have fS: "?f ` ?S = ?M" - apply (rule set_ext) - apply (simp add: image_iff Bex_def) using dimindex_nonzero[of "UNIV :: 'n set"] dimindex_nonzero[of "UNIV :: 'm set"] by arith have th1: "sndcart x \ sndcart x \ pastecart (fstcart x) (sndcart x) \ pastecart (fstcart x) (sndcart x)" - by (simp add: dot_def setsum_add_split[OF th_0, of _ ?m] pastecart_def dimindex_finite_sum Cart_lambda_beta setsum_nonneg zero_le_square setsum_reindex[OF finj, unfolded fS] del: One_nat_def) + by (simp add: dot_def setsum_UNIV_sum pastecart_def setsum_nonneg) then show ?thesis unfolding th0 unfolding real_vector_norm_def real_sqrt_le_iff id_def - by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta) + by (simp add: dot_def) qed lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y" by (metis dist_def sndcart_sub[symmetric] norm_sndcart) -lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n) (x2::'a::{times,comm_monoid_add}^'m)) \ (pastecart y1 y2) = x1 \ y1 + x2 \ y2" -proof- - let ?n = "dimindex (UNIV :: 'n set)" - let ?m = "dimindex (UNIV :: 'm set)" - let ?N = "{1 .. ?n}" - let ?M = "{1 .. ?m}" - let ?nm = "dimindex (UNIV :: ('n,'m) finite_sum set)" - let ?NM = "{1 .. ?nm}" - have thnm: "?nm = ?n + ?m" by (simp add: dimindex_finite_sum) - have th_0: "1 \ ?n +1" by simp - have th_1: "\i. i \ {?m + 1 .. ?nm} \ i - ?m \ ?N" apply (simp add: thnm) by arith - let ?f = "\a b i. (a$i) * (b$i)" - let ?g = "?f (pastecart x1 x2) (pastecart y1 y2)" - let ?S = "{?n +1 .. ?nm}" - {fix i - assume i: "i \ ?N" - have "?g i = ?f x1 y1 i" - using i - apply (simp add: pastecart_def Cart_lambda_beta thnm) done - } - hence th2: "setsum ?g ?N = setsum (?f x1 y1) ?N" - apply - - apply (rule setsum_cong) - apply auto - done - {fix i - assume i: "i \ ?S" - have "?g i = ?f x2 y2 (i - ?n)" - using i - apply (simp add: pastecart_def Cart_lambda_beta thnm) done - } - hence th3: "setsum ?g ?S = setsum (\i. ?f x2 y2 (i -?n)) ?S" - apply - - apply (rule setsum_cong) - apply auto - done - let ?r = "\n. n - ?n" - have rinj: "inj_on ?r ?S" apply (simp add: inj_on_def Ball_def thnm) by arith - have rS: "?r ` ?S = ?M" apply (rule set_ext) - apply (simp add: thnm image_iff Bex_def) by arith - have "pastecart x1 x2 \ (pastecart y1 y2) = setsum ?g ?NM" by (simp add: dot_def) - also have "\ = setsum ?g ?N + setsum ?g ?S" - by (simp add: dot_def thnm setsum_add_split[OF th_0, of _ ?m] del: One_nat_def) - also have "\ = setsum (?f x1 y1) ?N + setsum (?f x2 y2) ?M" - unfolding setsum_reindex[OF rinj, unfolded rS o_def] th2 th3 .. - finally - show ?thesis by (simp add: dot_def) -qed - -lemma norm_pastecart: "norm(pastecart x y) <= norm(x :: real ^ _) + norm(y)" +lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n::finite) (x2::'a::{times,comm_monoid_add}^'m::finite)) \ (pastecart y1 y2) = x1 \ y1 + x2 \ y2" + by (simp add: dot_def setsum_UNIV_sum pastecart_def) + +lemma norm_pastecart: "norm(pastecart x y) <= norm(x :: real ^ 'm::finite) + norm(y::real^'n::finite)" unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff id_def apply (rule power2_le_imp_le) apply (simp add: real_sqrt_pow2[OF add_nonneg_nonneg[OF dot_pos_le[of x] dot_pos_le[of y]]]) @@ -3419,7 +3342,7 @@ (* Standard bases are a spanning set, and obviously finite. *) -lemma span_stdbasis:"span {basis i :: 'a::ring_1^'n | i. i \ {1 .. dimindex(UNIV :: 'n set)}} = UNIV" +lemma span_stdbasis:"span {basis i :: 'a::ring_1^'n::finite | i. i \ (UNIV :: 'n set)} = UNIV" apply (rule set_ext) apply auto apply (subst basis_expansion[symmetric]) @@ -3431,47 +3354,43 @@ apply (auto simp add: Collect_def mem_def) done - -lemma has_size_stdbasis: "{basis i ::real ^'n | i. i \ {1 .. dimindex (UNIV :: 'n set)}} hassize (dimindex(UNIV :: 'n set))" (is "?S hassize ?n") +lemma has_size_stdbasis: "{basis i ::real ^'n::finite | i. i \ (UNIV :: 'n set)} hassize CARD('n)" (is "?S hassize ?n") proof- - have eq: "?S = basis ` {1 .. ?n}" by blast + have eq: "?S = basis ` UNIV" by blast show ?thesis unfolding eq apply (rule hassize_image_inj[OF basis_inj]) by (simp add: hassize_def) qed -lemma finite_stdbasis: "finite {basis i ::real^'n |i. i\ {1 .. dimindex(UNIV:: 'n set)}}" +lemma finite_stdbasis: "finite {basis i ::real^'n::finite |i. i\ (UNIV:: 'n set)}" using has_size_stdbasis[unfolded hassize_def] .. -lemma card_stdbasis: "card {basis i ::real^'n |i. i\ {1 .. dimindex(UNIV :: 'n set)}} = dimindex(UNIV :: 'n set)" +lemma card_stdbasis: "card {basis i ::real^'n::finite |i. i\ (UNIV :: 'n set)} = CARD('n)" using has_size_stdbasis[unfolded hassize_def] .. lemma independent_stdbasis_lemma: assumes x: "(x::'a::semiring_1 ^ 'n) \ span (basis ` S)" - and i: "i \ {1 .. dimindex (UNIV :: 'n set)}" and iS: "i \ S" shows "(x$i) = 0" proof- - let ?n = "dimindex (UNIV :: 'n set)" - let ?U = "{1 .. ?n}" + let ?U = "UNIV :: 'n set" let ?B = "basis ` S" let ?P = "\(x::'a^'n). \i\ ?U. i \ S \ x$i =0" {fix x::"'a^'n" assume xS: "x\ ?B" - from xS have "?P x" by (auto simp add: basis_component)} + from xS have "?P x" by auto} moreover have "subspace ?P" - by (auto simp add: subspace_def Collect_def mem_def zero_index vector_component) + by (auto simp add: subspace_def Collect_def mem_def) ultimately show ?thesis - using x span_induct[of ?B ?P x] i iS by blast + using x span_induct[of ?B ?P x] iS by blast qed -lemma independent_stdbasis: "independent {basis i ::real^'n |i. i\ {1 .. dimindex(UNIV :: 'n set)}}" +lemma independent_stdbasis: "independent {basis i ::real^'n::finite |i. i\ (UNIV :: 'n set)}" proof- - let ?n = "dimindex (UNIV :: 'n set)" - let ?I = "{1 .. ?n}" - let ?b = "basis :: nat \ real ^'n" + let ?I = "UNIV :: 'n set" + let ?b = "basis :: _ \ real ^'n" let ?B = "?b ` ?I" have eq: "{?b i|i. i \ ?I} = ?B" by auto @@ -3484,8 +3403,8 @@ apply (rule inj_on_image_set_diff[symmetric]) apply (rule basis_inj) using k(1) by auto from k(2) have th0: "?b k \ span (?b ` (?I - {k}))" unfolding eq2 . - from independent_stdbasis_lemma[OF th0 k(1), simplified] - have False by (simp add: basis_component[OF k(1), of k])} + from independent_stdbasis_lemma[OF th0, of k, simplified] + have False by simp} then show ?thesis unfolding eq dependent_def .. qed @@ -3665,19 +3584,19 @@ done qed -lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\ {(i::nat) .. j}}" +lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\ (UNIV::'a::finite set)}" proof- - have eq: "{f x |x. x\ {i .. j}} = f ` {i .. j}" by auto + have eq: "{f x |x. x\ UNIV} = f ` UNIV" by auto show ?thesis unfolding eq apply (rule finite_imageI) - apply (rule finite_atLeastAtMost) + apply (rule finite) done qed lemma independent_bound: - fixes S:: "(real^'n) set" - shows "independent S \ finite S \ card S <= dimindex(UNIV :: 'n set)" + fixes S:: "(real^'n::finite) set" + shows "independent S \ finite S \ card S <= CARD('n)" apply (subst card_stdbasis[symmetric]) apply (rule independent_span_bound) apply (rule finite_Atleast_Atmost_nat) @@ -3686,23 +3605,23 @@ apply (rule subset_UNIV) done -lemma dependent_biggerset: "(finite (S::(real ^'n) set) ==> card S > dimindex(UNIV:: 'n set)) ==> dependent S" +lemma dependent_biggerset: "(finite (S::(real ^'n::finite) set) ==> card S > CARD('n)) ==> dependent S" by (metis independent_bound not_less) (* Hence we can create a maximal independent subset. *) lemma maximal_independent_subset_extend: - assumes sv: "(S::(real^'n) set) \ V" and iS: "independent S" + assumes sv: "(S::(real^'n::finite) set) \ V" and iS: "independent S" shows "\B. S \ B \ B \ V \ independent B \ V \ span B" using sv iS -proof(induct d\ "dimindex (UNIV :: 'n set) - card S" arbitrary: S rule: nat_less_induct) +proof(induct d\ "CARD('n) - card S" arbitrary: S rule: nat_less_induct) fix n and S:: "(real^'n) set" - assume H: "\mS \ V. independent S \ m = dimindex (UNIV::'n set) - card S \ + assume H: "\mS \ V. independent S \ m = CARD('n) - card S \ (\B. S \ B \ B \ V \ independent B \ V \ span B)" - and sv: "S \ V" and i: "independent S" and n: "n = dimindex (UNIV :: 'n set) - card S" + and sv: "S \ V" and i: "independent S" and n: "n = CARD('n) - card S" let ?P = "\B. S \ B \ B \ V \ independent B \ V \ span B" let ?ths = "\x. ?P x" - let ?d = "dimindex (UNIV :: 'n set)" + let ?d = "CARD('n)" {assume "V \ span S" then have ?ths using sv i by blast } moreover @@ -3713,7 +3632,7 @@ from independent_insert[of a S] i a have th1: "independent (insert a S)" by auto have mlt: "?d - card (insert a S) < n" - using aS a n independent_bound[OF th1] dimindex_ge_1[of "UNIV :: 'n set"] + using aS a n independent_bound[OF th1] by auto from H[rule_format, OF mlt th0 th1 refl] @@ -3725,14 +3644,14 @@ qed lemma maximal_independent_subset: - "\(B:: (real ^'n) set). B\ V \ independent B \ V \ span B" + "\(B:: (real ^'n::finite) set). B\ V \ independent B \ V \ span B" by (metis maximal_independent_subset_extend[of "{}:: (real ^'n) set"] empty_subsetI independent_empty) (* Notion of dimension. *) definition "dim V = (SOME n. \B. B \ V \ independent B \ V \ span B \ (B hassize n))" -lemma basis_exists: "\B. (B :: (real ^'n) set) \ V \ independent B \ V \ span B \ (B hassize dim V)" +lemma basis_exists: "\B. (B :: (real ^'n::finite) set) \ V \ independent B \ V \ span B \ (B hassize dim V)" unfolding dim_def some_eq_ex[of "\n. \B. B \ V \ independent B \ V \ span B \ (B hassize n)"] unfolding hassize_def using maximal_independent_subset[of V] independent_bound @@ -3740,37 +3659,37 @@ (* Consequences of independence or spanning for cardinality. *) -lemma independent_card_le_dim: "(B::(real ^'n) set) \ V \ independent B \ finite B \ card B \ dim V" +lemma independent_card_le_dim: "(B::(real ^'n::finite) set) \ V \ independent B \ finite B \ card B \ dim V" by (metis basis_exists[of V] independent_span_bound[where ?'a=real] hassize_def subset_trans) -lemma span_card_ge_dim: "(B::(real ^'n) set) \ V \ V \ span B \ finite B \ dim V \ card B" +lemma span_card_ge_dim: "(B::(real ^'n::finite) set) \ V \ V \ span B \ finite B \ dim V \ card B" by (metis basis_exists[of V] independent_span_bound hassize_def subset_trans) lemma basis_card_eq_dim: - "B \ (V:: (real ^'n) set) \ V \ span B \ independent B \ finite B \ card B = dim V" + "B \ (V:: (real ^'n::finite) 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_mono) -lemma dim_unique: "(B::(real ^'n) set) \ V \ V \ span B \ independent B \ B hassize n \ dim V = n" +lemma dim_unique: "(B::(real ^'n::finite) set) \ V \ V \ span B \ independent B \ B hassize n \ dim V = n" by (metis basis_card_eq_dim hassize_def) (* More lemmas about dimension. *) -lemma dim_univ: "dim (UNIV :: (real^'n) set) = dimindex (UNIV :: 'n set)" - apply (rule dim_unique[of "{basis i |i. i\ {1 .. dimindex (UNIV :: 'n set)}}"]) +lemma dim_univ: "dim (UNIV :: (real^'n::finite) set) = CARD('n)" + apply (rule dim_unique[of "{basis i |i. i\ (UNIV :: 'n set)}"]) by (auto simp only: span_stdbasis has_size_stdbasis independent_stdbasis) lemma dim_subset: - "(S:: (real ^'n) set) \ T \ dim S \ dim T" + "(S:: (real ^'n::finite) set) \ T \ dim S \ dim T" using basis_exists[of T] basis_exists[of S] by (metis independent_span_bound[where ?'a = real and ?'n = 'n] subset_eq hassize_def) -lemma dim_subset_univ: "dim (S:: (real^'n) set) \ dimindex (UNIV :: 'n set)" +lemma dim_subset_univ: "dim (S:: (real^'n::finite) set) \ CARD('n)" by (metis dim_subset subset_UNIV dim_univ) (* Converses to those. *) lemma card_ge_dim_independent: - assumes BV:"(B::(real ^'n) set) \ V" and iB:"independent B" and dVB:"dim V \ card B" + assumes BV:"(B::(real ^'n::finite) set) \ V" and iB:"independent B" and dVB:"dim V \ card B" shows "V \ span B" proof- {fix a assume aV: "a \ V" @@ -3784,7 +3703,7 @@ qed lemma card_le_dim_spanning: - assumes BV: "(B:: (real ^'n) set) \ V" and VB: "V \ span B" + assumes BV: "(B:: (real ^'n::finite) set) \ V" and VB: "V \ span B" and fB: "finite B" and dVB: "dim V \ card B" shows "independent B" proof- @@ -3805,7 +3724,7 @@ then show ?thesis unfolding dependent_def by blast qed -lemma card_eq_dim: "(B:: (real ^'n) set) \ V \ B hassize dim V \ independent B \ V \ span B" +lemma card_eq_dim: "(B:: (real ^'n::finite) set) \ V \ B hassize dim V \ independent B \ V \ span B" by (metis hassize_def order_eq_iff card_le_dim_spanning card_ge_dim_independent) @@ -3814,13 +3733,13 @@ (* ------------------------------------------------------------------------- *) lemma independent_bound_general: - "independent (S:: (real^'n) set) \ finite S \ card S \ dim S" + "independent (S:: (real^'n::finite) set) \ finite S \ card S \ dim S" by (metis independent_card_le_dim independent_bound subset_refl) -lemma dependent_biggerset_general: "(finite (S:: (real^'n) set) \ card S > dim S) \ dependent S" +lemma dependent_biggerset_general: "(finite (S:: (real^'n::finite) set) \ card S > dim S) \ dependent S" using independent_bound_general[of S] by (metis linorder_not_le) -lemma dim_span: "dim (span (S:: (real ^'n) set)) = dim S" +lemma dim_span: "dim (span (S:: (real ^'n::finite) set)) = dim S" proof- have th0: "dim S \ dim (span S)" by (auto simp add: subset_eq intro: dim_subset span_superset) @@ -3833,10 +3752,10 @@ using fB(2) by arith qed -lemma subset_le_dim: "(S:: (real ^'n) set) \ span T \ dim S \ dim T" +lemma subset_le_dim: "(S:: (real ^'n::finite) set) \ span T \ dim S \ dim T" by (metis dim_span dim_subset) -lemma span_eq_dim: "span (S:: (real ^'n) set) = span T ==> dim S = dim T" +lemma span_eq_dim: "span (S:: (real ^'n::finite) set) = span T ==> dim S = dim T" by (metis dim_span) lemma spans_image: @@ -3845,7 +3764,9 @@ unfolding span_linear_image[OF lf] by (metis VB image_mono) -lemma dim_image_le: assumes lf: "linear f" shows "dim (f ` S) \ dim (S:: (real ^'n) set)" +lemma dim_image_le: + fixes f :: "real^'n::finite \ real^'m::finite" + assumes lf: "linear f" shows "dim (f ` S) \ dim (S:: (real ^'n::finite) set)" proof- from basis_exists[of S] obtain B where B: "B \ S" "independent B" "S \ span B" "B hassize dim S" by blast @@ -3889,14 +3810,14 @@ (* FIXME : Move to some general theory ?*) definition "pairwise R S \ (\x \ S. \y\ S. x\y \ R x y)" -lemma vector_sub_project_orthogonal: "(b::'a::ordered_field^'n) \ (x - ((b \ x) / (b\b)) *s b) = 0" +lemma vector_sub_project_orthogonal: "(b::'a::ordered_field^'n::finite) \ (x - ((b \ x) / (b\b)) *s b) = 0" apply (cases "b = 0", simp) apply (simp add: dot_rsub dot_rmult) unfolding times_divide_eq_right[symmetric] by (simp add: field_simps dot_eq_0) lemma basis_orthogonal: - fixes B :: "(real ^'n) set" + fixes B :: "(real ^'n::finite) set" assumes fB: "finite B" shows "\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C" (is " \C. ?P B C") @@ -3972,7 +3893,7 @@ qed lemma orthogonal_basis_exists: - fixes V :: "(real ^'n) set" + fixes V :: "(real ^'n::finite) set" shows "\B. independent B \ B \ span V \ V \ span B \ (B hassize dim V) \ pairwise orthogonal B" proof- from basis_exists[of V] obtain B where B: "B \ V" "independent B" "V \ span B" "B hassize dim V" by blast @@ -4000,7 +3921,7 @@ lemma span_not_univ_orthogonal: assumes sU: "span S \ UNIV" - shows "\(a:: real ^'n). a \0 \ (\x \ span S. a \ x = 0)" + shows "\(a:: real ^'n::finite). a \0 \ (\x \ span S. a \ x = 0)" proof- from sU obtain a where a: "a \ span S" by blast from orthogonal_basis_exists obtain B where @@ -4039,17 +3960,17 @@ qed lemma span_not_univ_subset_hyperplane: - assumes SU: "span S \ (UNIV ::(real^'n) set)" + assumes SU: "span S \ (UNIV ::(real^'n::finite) set)" shows "\ a. a \0 \ span S \ {x. a \ x = 0}" using span_not_univ_orthogonal[OF SU] by auto lemma lowdim_subset_hyperplane: - assumes d: "dim S < dimindex (UNIV :: 'n set)" - shows "\(a::real ^'n). a \ 0 \ span S \ {x. a \ x = 0}" + assumes d: "dim S < CARD('n::finite)" + shows "\(a::real ^'n::finite). a \ 0 \ span S \ {x. a \ x = 0}" proof- {assume "span S = UNIV" hence "dim (span S) = dim (UNIV :: (real ^'n) set)" by simp - hence "dim S = dimindex (UNIV :: 'n set)" by (simp add: dim_span dim_univ) + hence "dim S = CARD('n)" 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 . @@ -4196,7 +4117,7 @@ qed lemma linear_independent_extend: - assumes iB: "independent (B:: (real ^'n) set)" + assumes iB: "independent (B:: (real ^'n::finite) set)" shows "\g. linear g \ (\x\B. g x = f x)" proof- from maximal_independent_subset_extend[of B UNIV] iB @@ -4249,7 +4170,8 @@ qed lemma subspace_isomorphism: - assumes s: "subspace (S:: (real ^'n) set)" and t: "subspace T" + assumes s: "subspace (S:: (real ^'n::finite) set)" + and t: "subspace (T :: (real ^ 'm::finite) set)" and d: "dim S = dim T" shows "\f. linear f \ f ` S = T \ inj_on f S" proof- @@ -4324,12 +4246,12 @@ qed lemma linear_eq_stdbasis: - assumes lf: "linear (f::'a::ring_1^'m \ 'a^'n)" and lg: "linear g" - and fg: "\i \ {1 .. dimindex(UNIV :: 'm set)}. f (basis i) = g(basis i)" + assumes lf: "linear (f::'a::ring_1^'m::finite \ 'a^'n::finite)" and lg: "linear g" + and fg: "\i. f (basis i) = g(basis i)" shows "f = g" proof- let ?U = "UNIV :: 'm set" - let ?I = "{basis i:: 'a^'m|i. i \ {1 .. dimindex ?U}}" + let ?I = "{basis i:: 'a^'m|i. i \ ?U}" {fix x assume x: "x \ (UNIV :: ('a^'m) set)" from equalityD2[OF span_stdbasis] have IU: " (UNIV :: ('a^'m) set) \ span ?I" by blast @@ -4369,12 +4291,12 @@ qed lemma bilinear_eq_stdbasis: - assumes bf: "bilinear (f:: 'a::ring_1^'m \ 'a^'n \ 'a^'p)" + assumes bf: "bilinear (f:: 'a::ring_1^'m::finite \ 'a^'n::finite \ 'a^'p)" and bg: "bilinear g" - and fg: "\i\ {1 .. dimindex (UNIV :: 'm set)}. \j\ {1 .. dimindex (UNIV :: 'n set)}. f (basis i) (basis j) = g (basis i) (basis j)" + and fg: "\i j. f (basis i) (basis j) = g (basis i) (basis j)" shows "f = g" proof- - from fg have th: "\x \ {basis i| i. i\ {1 .. dimindex (UNIV :: 'm set)}}. \y\ {basis j |j. j \ {1 .. dimindex (UNIV :: 'n set)}}. f x y = g x y" by blast + from fg have th: "\x \ {basis i| i. i\ (UNIV :: 'm set)}. \y\ {basis j |j. j \ (UNIV :: 'n set)}. f x y = g x y" by blast from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by (blast intro: ext) qed @@ -4389,16 +4311,14 @@ by (metis matrix_transp_mul transp_mat transp_transp) lemma linear_injective_left_inverse: - assumes lf: "linear (f::real ^'n \ real ^'m)" and fi: "inj f" + assumes lf: "linear (f::real ^'n::finite \ real ^'m::finite)" and fi: "inj f" shows "\g. linear g \ g o f = id" proof- from linear_independent_extend[OF independent_injective_image, OF independent_stdbasis, OF lf fi] - obtain h:: "real ^'m \ real ^'n" where h: "linear h" " \x \ f ` {basis i|i. i \ {1 .. dimindex (UNIV::'n set)}}. h x = inv f x" by blast + obtain h:: "real ^'m \ real ^'n" where h: "linear h" " \x \ f ` {basis i|i. i \ (UNIV::'n set)}. h x = inv f x" by blast from h(2) - have th: "\i\{1..dimindex (UNIV::'n set)}. (h \ f) (basis i) = id (basis i)" + have th: "\i. (h \ f) (basis i) = id (basis i)" using inv_o_cancel[OF fi, unfolded stupid_ext[symmetric] id_def o_def] - apply auto - apply (erule_tac x="basis i" in allE) by auto from linear_eq_stdbasis[OF linear_compose[OF lf h(1)] linear_id th] @@ -4407,14 +4327,14 @@ qed lemma linear_surjective_right_inverse: - assumes lf: "linear (f:: real ^'m \ real ^'n)" and sf: "surj f" + assumes lf: "linear (f:: real ^'m::finite \ real ^'n::finite)" and sf: "surj f" shows "\g. linear g \ f o g = id" proof- from linear_independent_extend[OF independent_stdbasis] obtain h:: "real ^'n \ real ^'m" where - h: "linear h" "\ x\ {basis i| i. i\ {1 .. dimindex (UNIV :: 'n set)}}. h x = inv f x" by blast + h: "linear h" "\ x\ {basis i| i. i\ (UNIV :: 'n set)}. h x = inv f x" by blast from h(2) - have th: "\i\{1..dimindex (UNIV::'n set)}. (f o h) (basis i) = id (basis i)" + have th: "\i. (f o h) (basis i) = id (basis i)" using sf apply (auto simp add: surj_iff o_def stupid_ext[symmetric]) apply (erule_tac x="basis i" in allE) @@ -4426,7 +4346,7 @@ qed lemma matrix_left_invertible_injective: -"(\B. (B::real^'m^'n) ** (A::real^'n^'m) = mat 1) \ (\x y. A *v x = A *v y \ x = y)" +"(\B. (B::real^'m^'n) ** (A::real^'n::finite^'m::finite) = mat 1) \ (\x y. A *v x = A *v y \ x = y)" proof- {fix B:: "real^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y" from xy have "B*v (A *v x) = B *v (A*v y)" by simp @@ -4445,13 +4365,13 @@ qed lemma matrix_left_invertible_ker: - "(\B. (B::real ^'m^'n) ** (A::real^'n^'m) = mat 1) \ (\x. A *v x = 0 \ x = 0)" + "(\B. (B::real ^'m::finite^'n::finite) ** (A::real^'n^'m) = mat 1) \ (\x. A *v x = 0 \ x = 0)" unfolding matrix_left_invertible_injective using linear_injective_0[OF matrix_vector_mul_linear, of A] by (simp add: inj_on_def) lemma matrix_right_invertible_surjective: -"(\B. (A::real^'n^'m) ** (B::real^'m^'n) = mat 1) \ surj (\x. A *v x)" +"(\B. (A::real^'n::finite^'m::finite) ** (B::real^'m^'n) = mat 1) \ surj (\x. A *v x)" proof- {fix B :: "real ^'m^'n" assume AB: "A ** B = mat 1" {fix x :: "real ^ 'm" @@ -4475,11 +4395,11 @@ qed lemma matrix_left_invertible_independent_columns: - fixes A :: "real^'n^'m" - shows "(\(B::real ^'m^'n). B ** A = mat 1) \ (\c. setsum (\i. c i *s column i A) {1 .. dimindex(UNIV :: 'n set)} = 0 \ (\i\ {1 .. dimindex (UNIV :: 'n set)}. c i = 0))" + fixes A :: "real^'n::finite^'m::finite" + shows "(\(B::real ^'m^'n). B ** A = mat 1) \ (\c. setsum (\i. c i *s column i A) (UNIV :: 'n set) = 0 \ (\i. c i = 0))" (is "?lhs \ ?rhs") proof- - let ?U = "{1 .. dimindex(UNIV :: 'n set)}" + let ?U = "UNIV :: 'n set" {assume k: "\x. A *v x = 0 \ x = 0" {fix c i assume c: "setsum (\i. c i *s column i A) ?U = 0" and i: "i \ ?U" @@ -4487,7 +4407,7 @@ have th0:"A *v ?x = 0" using c unfolding matrix_mult_vsum Cart_eq - by (auto simp add: vector_component zero_index setsum_component Cart_lambda_beta) + by auto from k[rule_format, OF th0] i have "c i = 0" by (vector Cart_eq)} hence ?rhs by blast} @@ -4501,16 +4421,16 @@ qed lemma matrix_right_invertible_independent_rows: - fixes A :: "real^'n^'m" - shows "(\(B::real^'m^'n). A ** B = mat 1) \ (\c. setsum (\i. c i *s row i A) {1 .. dimindex(UNIV :: 'm set)} = 0 \ (\i\ {1 .. dimindex (UNIV :: 'm set)}. c i = 0))" + fixes A :: "real^'n::finite^'m::finite" + shows "(\(B::real^'m^'n). A ** B = mat 1) \ (\c. setsum (\i. c i *s row i A) (UNIV :: 'm set) = 0 \ (\i. c i = 0))" unfolding left_invertible_transp[symmetric] matrix_left_invertible_independent_columns by (simp add: column_transp) lemma matrix_right_invertible_span_columns: - "(\(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \ span (columns A) = UNIV" (is "?lhs = ?rhs") + "(\(B::real ^'n::finite^'m::finite). (A::real ^'m^'n) ** B = mat 1) \ span (columns A) = UNIV" (is "?lhs = ?rhs") proof- - let ?U = "{1 .. dimindex (UNIV :: 'm set)}" + let ?U = "UNIV :: 'm set" have fU: "finite ?U" by simp have lhseq: "?lhs \ (\y. \(x::real^'m). setsum (\i. (x$i) *s column i A) ?U = y)" unfolding matrix_right_invertible_surjective matrix_mult_vsum surj_def @@ -4545,7 +4465,7 @@ x: "setsum (\i. (x$i) *s column i A) ?U = y2" by blast let ?x = "(\ j. if j = i then c + (x$i) else (x$j))::real^'m" show "?P (c*s y1 + y2)" - proof(rule exI[where x= "?x"], vector, auto simp add: i x[symmetric]Cart_lambda_beta setsum_component cond_value_iff right_distrib cond_application_beta vector_component cong del: if_weak_cong, simp only: One_nat_def[symmetric]) + proof(rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] cond_value_iff right_distrib cond_application_beta cong del: if_weak_cong) fix j have th: "\xa \ ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j) else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))" using i(1) @@ -4570,7 +4490,7 @@ qed lemma matrix_left_invertible_span_rows: - "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" + "(\(B::real^'m::finite^'n::finite). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" unfolding right_invertible_transp[symmetric] unfolding columns_transp[symmetric] unfolding matrix_right_invertible_span_columns @@ -4579,7 +4499,7 @@ (* An injective map real^'n->real^'n is also surjective. *) lemma linear_injective_imp_surjective: - assumes lf: "linear (f:: real ^'n \ real ^'n)" and fi: "inj f" + assumes lf: "linear (f:: real ^'n::finite \ real ^'n)" and fi: "inj f" shows "surj f" proof- let ?U = "UNIV :: (real ^'n) set" @@ -4641,7 +4561,7 @@ qed lemma linear_surjective_imp_injective: - assumes lf: "linear (f::real ^'n => real ^'n)" and sf: "surj f" + assumes lf: "linear (f::real ^'n::finite => real ^'n)" and sf: "surj f" shows "inj f" proof- let ?U = "UNIV :: (real ^'n) set" @@ -4701,14 +4621,14 @@ by (simp add: expand_fun_eq o_def id_def) lemma linear_injective_isomorphism: - assumes lf: "linear (f :: real^'n \ real ^'n)" and fi: "inj f" + assumes lf: "linear (f :: real^'n::finite \ real ^'n)" 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) lemma linear_surjective_isomorphism: - assumes lf: "linear (f::real ^'n \ real ^'n)" and sf: "surj f" + assumes lf: "linear (f::real ^'n::finite \ real ^'n)" 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]] @@ -4717,7 +4637,7 @@ (* Left and right inverses are the same for R^N->R^N. *) lemma linear_inverse_left: - assumes lf: "linear (f::real ^'n \ real ^'n)" and lf': "linear f'" + assumes lf: "linear (f::real ^'n::finite \ real ^'n)" and lf': "linear f'" shows "f o f' = id \ f' o f = id" proof- {fix f f':: "real ^'n \ real ^'n" @@ -4735,7 +4655,7 @@ (* Moreover, a one-sided inverse is automatically linear. *) lemma left_inverse_linear: - assumes lf: "linear (f::real ^'n \ real ^'n)" and gf: "g o f = id" + assumes lf: "linear (f::real ^'n::finite \ real ^'n)" 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 stupid_ext[symmetric]) @@ -4750,7 +4670,7 @@ qed lemma right_inverse_linear: - assumes lf: "linear (f:: real ^'n \ real ^'n)" and gf: "f o g = id" + assumes lf: "linear (f:: real ^'n::finite \ real ^'n)" and gf: "f o g = id" shows "linear g" proof- from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def stupid_ext[symmetric]) @@ -4767,7 +4687,7 @@ (* The same result in terms of square matrices. *) lemma matrix_left_right_inverse: - fixes A A' :: "real ^'n^'n" + fixes A A' :: "real ^'n::finite^'n" shows "A ** A' = mat 1 \ A' ** A = mat 1" proof- {fix A A' :: "real ^'n^'n" assume AA': "A ** A' = mat 1" @@ -4796,21 +4716,20 @@ lemma transp_columnvector: "transp(columnvector v) = rowvector v" - by (simp add: transp_def rowvector_def columnvector_def Cart_eq Cart_lambda_beta) + by (simp add: transp_def rowvector_def columnvector_def Cart_eq) lemma transp_rowvector: "transp(rowvector v) = columnvector v" - by (simp add: transp_def columnvector_def rowvector_def Cart_eq Cart_lambda_beta) + by (simp add: transp_def columnvector_def rowvector_def Cart_eq) lemma dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v" by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) -lemma dot_matrix_product: "(x::'a::semiring_1^'n) \ y = (((rowvector x ::'a^'n^1) ** (columnvector y :: 'a^1^'n))$1)$1" - apply (vector matrix_matrix_mult_def rowvector_def columnvector_def dot_def) - by (simp add: Cart_lambda_beta) +lemma dot_matrix_product: "(x::'a::semiring_1^'n::finite) \ y = (((rowvector x ::'a^'n^1) ** (columnvector y :: 'a^1^'n))$1)$1" + by (vector matrix_matrix_mult_def rowvector_def columnvector_def dot_def) lemma dot_matrix_vector_mul: - fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" + fixes A B :: "real ^'n::finite ^'n" and x y :: "real ^'n" shows "(A *v x) \ (B *v y) = (((rowvector x :: real^'n^1) ** ((transp A ** B) ** (columnvector y :: real ^1^'n)))$1)$1" unfolding dot_matrix_product transp_columnvector[symmetric] @@ -4818,30 +4737,28 @@ (* Infinity norm. *) -definition "infnorm (x::real^'n) = rsup {abs(x$i) |i. i\ {1 .. dimindex(UNIV :: 'n set)}}" - -lemma numseg_dimindex_nonempty: "\i. i \ {1 .. dimindex (UNIV :: 'n set)}" - using dimindex_ge_1 by auto +definition "infnorm (x::real^'n::finite) = rsup {abs(x$i) |i. i\ (UNIV :: 'n set)}" + +lemma numseg_dimindex_nonempty: "\i. i \ (UNIV :: 'n set)" + by auto lemma infnorm_set_image: - "{abs(x$i) |i. i\ {1 .. dimindex(UNIV :: 'n set)}} = - (\i. abs(x$i)) ` {1 .. dimindex(UNIV :: 'n set)}" by blast + "{abs(x$i) |i. i\ (UNIV :: 'n set)} = + (\i. abs(x$i)) ` (UNIV :: 'n set)" by blast lemma infnorm_set_lemma: - shows "finite {abs((x::'a::abs ^'n)$i) |i. i\ {1 .. dimindex(UNIV :: 'n set)}}" - and "{abs(x$i) |i. i\ {1 .. dimindex(UNIV :: 'n set)}} \ {}" + shows "finite {abs((x::'a::abs ^'n::finite)$i) |i. i\ (UNIV :: 'n set)}" + and "{abs(x$i) |i. i\ (UNIV :: 'n::finite set)} \ {}" unfolding infnorm_set_image - using dimindex_ge_1[of "UNIV :: 'n set"] by (auto intro: finite_imageI) -lemma infnorm_pos_le: "0 \ infnorm x" +lemma infnorm_pos_le: "0 \ infnorm (x::real^'n::finite)" unfolding infnorm_def unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma] unfolding infnorm_set_image - using dimindex_ge_1 by auto -lemma infnorm_triangle: "infnorm ((x::real^'n) + y) \ infnorm x + infnorm y" +lemma infnorm_triangle: "infnorm ((x::real^'n::finite) + y) \ infnorm x + infnorm y" 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 @@ -4857,12 +4774,12 @@ unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma] unfolding infnorm_set_image ball_simps bex_simps - apply (simp add: vector_add_component) - apply (metis numseg_dimindex_nonempty th2) + apply simp + apply (metis th2) done qed -lemma infnorm_eq_0: "infnorm x = 0 \ (x::real ^'n) = 0" +lemma infnorm_eq_0: "infnorm x = 0 \ (x::real ^'n::finite) = 0" proof- have "infnorm x <= 0 \ x = 0" unfolding infnorm_def @@ -4880,9 +4797,7 @@ apply (rule cong[of "rsup" "rsup"]) apply blast apply (rule set_ext) - apply (auto simp add: vector_component abs_minus_cancel) - apply (rule_tac x="i" in exI) - apply (simp add: vector_component) + apply auto done lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)" @@ -4905,16 +4820,16 @@ lemma real_abs_infnorm: " \infnorm x\ = infnorm x" using infnorm_pos_le[of x] by arith -lemma component_le_infnorm: assumes i: "i \ {1 .. dimindex (UNIV :: 'n set)}" - shows "\x$i\ \ infnorm (x::real^'n)" +lemma component_le_infnorm: + shows "\x$i\ \ infnorm (x::real^'n::finite)" proof- - let ?U = "{1 .. dimindex (UNIV :: 'n set)}" + let ?U = "UNIV :: 'n set" let ?S = "{\x$i\ |i. i\ ?U}" have fS: "finite ?S" unfolding image_Collect[symmetric] apply (rule finite_imageI) unfolding Collect_def mem_def by simp - have S0: "?S \ {}" using numseg_dimindex_nonempty by blast + have S0: "?S \ {}" by blast have th1: "\S f. f ` S = { f i| i. i \ S}" by blast - from rsup_finite_in[OF fS S0] rsup_finite_Ub[OF fS S0] i + from rsup_finite_in[OF fS S0] rsup_finite_Ub[OF fS S0] show ?thesis unfolding infnorm_def isUb_def setle_def unfolding infnorm_set_image ball_simps by auto qed @@ -4923,9 +4838,9 @@ apply (subst infnorm_def) unfolding rsup_finite_le_iff[OF infnorm_set_lemma] unfolding infnorm_set_image ball_simps - apply (simp add: abs_mult vector_component del: One_nat_def) - apply (rule ballI) - apply (drule component_le_infnorm[of _ x]) + apply (simp add: abs_mult) + apply (rule allI) + apply (cut_tac component_le_infnorm[of x]) apply (rule mult_mono) apply auto done @@ -4958,18 +4873,16 @@ unfolding infnorm_set_image ball_simps by (metis component_le_norm) lemma card_enum: "card {1 .. n} = n" by auto -lemma norm_le_infnorm: "norm(x) <= sqrt(real (dimindex(UNIV ::'n set))) * infnorm(x::real ^'n)" +lemma norm_le_infnorm: "norm(x) <= sqrt(real CARD('n)) * infnorm(x::real ^'n::finite)" proof- - let ?d = "dimindex(UNIV ::'n set)" - have d: "?d = card {1 .. ?d}" by auto + let ?d = "CARD('n)" have "real ?d \ 0" by simp hence d2: "(sqrt (real ?d))^2 = real ?d" by (auto intro: real_sqrt_pow2) have th: "sqrt (real ?d) * infnorm x \ 0" - by (simp add: dimindex_ge_1 zero_le_mult_iff real_sqrt_ge_0_iff infnorm_pos_le) + by (simp add: zero_le_mult_iff real_sqrt_ge_0_iff infnorm_pos_le) have th1: "x\x \ (sqrt (real ?d) * infnorm x)^2" unfolding power_mult_distrib d2 - apply (subst d) apply (subst power2_abs[symmetric]) unfolding real_of_nat_def dot_def power2_eq_square[symmetric] apply (subst power2_abs[symmetric]) @@ -4986,7 +4899,7 @@ (* Equality in Cauchy-Schwarz and triangle inequalities. *) -lemma norm_cauchy_schwarz_eq: "(x::real ^'n) \ y = norm x * norm y \ norm x *s y = norm y *s x" (is "?lhs \ ?rhs") +lemma norm_cauchy_schwarz_eq: "(x::real ^'n::finite) \ y = norm x * norm y \ norm x *s y = norm y *s x" (is "?lhs \ ?rhs") proof- {assume h: "x = 0" hence ?thesis by simp} @@ -5012,7 +4925,9 @@ ultimately show ?thesis by blast qed -lemma norm_cauchy_schwarz_abs_eq: "abs(x \ y) = norm x * norm y \ +lemma norm_cauchy_schwarz_abs_eq: + fixes x y :: "real ^ 'n::finite" + shows "abs(x \ y) = norm x * norm y \ norm x *s y = norm y *s x \ norm(x) *s y = - norm y *s x" (is "?lhs \ ?rhs") proof- have th: "\(x::real) a. a \ 0 \ abs x = a \ x = a \ x = - a" by arith @@ -5029,7 +4944,9 @@ finally show ?thesis .. qed -lemma norm_triangle_eq: "norm(x + y) = norm x + norm y \ norm x *s y = norm y *s x" +lemma norm_triangle_eq: + fixes x y :: "real ^ 'n::finite" + shows "norm(x + y) = norm x + norm y \ norm x *s y = norm y *s x" proof- {assume x: "x =0 \ y =0" hence ?thesis by (cases "x=0", simp_all)} @@ -5107,7 +5024,9 @@ ultimately show ?thesis by blast qed -lemma norm_cauchy_schwarz_equal: "abs(x \ y) = norm x * norm y \ collinear {(0::real^'n),x,y}" +lemma norm_cauchy_schwarz_equal: + fixes x y :: "real ^ 'n::finite" + shows "abs(x \ y) = norm x * norm y \ collinear {(0::real^'n),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) diff -r ac50e7dedf6d -r 638b088bb840 src/HOL/Library/Finite_Cartesian_Product.thy --- a/src/HOL/Library/Finite_Cartesian_Product.thy Wed Mar 18 22:17:23 2009 +0100 +++ b/src/HOL/Library/Finite_Cartesian_Product.thy Thu Mar 19 01:29:19 2009 -0700 @@ -10,202 +10,81 @@ begin (* FIXME : ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs*) -subsection{* Dimention of sets *} - -definition "dimindex (S:: 'a set) = (if finite (UNIV::'a set) then card (UNIV:: 'a set) else 1)" - -syntax "_type_dimindex" :: "type => nat" ("(1DIM/(1'(_')))") -translations "DIM(t)" => "CONST dimindex (CONST UNIV :: t set)" - -lemma dimindex_nonzero: "dimindex S \ 0" -unfolding dimindex_def -by (simp add: neq0_conv[symmetric] del: neq0_conv) - -lemma dimindex_ge_1: "dimindex S \ 1" - using dimindex_nonzero[of S] by arith -lemma dimindex_univ: "dimindex (S :: 'a set) = DIM('a)" by (simp add: dimindex_def) definition hassize (infixr "hassize" 12) where "(S hassize n) = (finite S \ card S = n)" -lemma dimindex_unique: " (UNIV :: 'a set) hassize n ==> DIM('a) = n" -by (simp add: dimindex_def hassize_def) - - -subsection{* An indexing type parametrized by base type. *} - -typedef 'a finite_image = "{1 .. DIM('a)}" - using dimindex_ge_1 by auto - -lemma finite_image_image: "(UNIV :: 'a finite_image set) = Abs_finite_image ` {1 .. DIM('a)}" -apply (auto simp add: Abs_finite_image_inverse image_def finite_image_def) -apply (rule_tac x="Rep_finite_image x" in bexI) -apply (simp_all add: Rep_finite_image_inverse Rep_finite_image) -using Rep_finite_image[where ?'a = 'a] -unfolding finite_image_def -apply simp -done - -text{* Dimension of such a type, and indexing over it. *} - -lemma inj_on_Abs_finite_image: - "inj_on (Abs_finite_image:: _ \ 'a finite_image) {1 .. DIM('a)}" -by (auto simp add: inj_on_def finite_image_def Abs_finite_image_inject[where ?'a='a]) - -lemma has_size_finite_image: "(UNIV:: 'a finite_image set) hassize dimindex (S :: 'a set)" - unfolding hassize_def finite_image_image card_image[OF inj_on_Abs_finite_image[where ?'a='a]] by (auto simp add: dimindex_def) - lemma hassize_image_inj: assumes f: "inj_on f S" and S: "S hassize n" shows "f ` S hassize n" using f S card_image[OF f] by (simp add: hassize_def inj_on_def) -lemma card_finite_image: "card (UNIV:: 'a finite_image set) = dimindex(S:: 'a set)" -using has_size_finite_image -unfolding hassize_def by blast - -lemma finite_finite_image: "finite (UNIV:: 'a finite_image set)" -using has_size_finite_image -unfolding hassize_def by blast - -lemma dimindex_finite_image: "dimindex (S:: 'a finite_image set) = dimindex(T:: 'a set)" -unfolding card_finite_image[of T, symmetric] -by (auto simp add: dimindex_def finite_finite_image) - -lemma Abs_finite_image_works: - fixes i:: "'a finite_image" - shows " \!n \ {1 .. DIM('a)}. Abs_finite_image n = i" - unfolding Bex1_def Ex1_def - apply (rule_tac x="Rep_finite_image i" in exI) - using Rep_finite_image_inverse[where ?'a = 'a] - Rep_finite_image[where ?'a = 'a] - Abs_finite_image_inverse[where ?'a='a, symmetric] - by (auto simp add: finite_image_def) - -lemma Abs_finite_image_inj: - "i \ {1 .. DIM('a)} \ j \ {1 .. DIM('a)} - \ (((Abs_finite_image i ::'a finite_image) = Abs_finite_image j) \ (i = j))" - using Abs_finite_image_works[where ?'a = 'a] - by (auto simp add: atLeastAtMost_iff Bex1_def) - -lemma forall_Abs_finite_image: - "(\k:: 'a finite_image. P k) \ (\i \ {1 .. DIM('a)}. P(Abs_finite_image i))" -unfolding Ball_def atLeastAtMost_iff Ex1_def -using Abs_finite_image_works[where ?'a = 'a, unfolded atLeastAtMost_iff Bex1_def] -by metis subsection {* Finite Cartesian products, with indexing and lambdas. *} -typedef (Cart) +typedef (open Cart) ('a, 'b) "^" (infixl "^" 15) - = "{f:: 'b finite_image \ 'a . True}" by simp + = "UNIV :: ('b \ 'a) set" + morphisms Cart_nth Cart_lambda .. -abbreviation dimset:: "('a ^ 'n) \ nat set" where - "dimset a \ {1 .. DIM('n)}" +notation Cart_nth (infixl "$" 90) -definition Cart_nth :: "'a ^ 'b \ nat \ 'a" (infixl "$" 90) where - "x$i = Rep_Cart x (Abs_finite_image i)" +notation (xsymbols) Cart_lambda (binder "\" 10) lemma stupid_ext: "(\x. f x = g x) \ (f = g)" apply auto apply (rule ext) apply auto done -lemma Cart_eq: "((x:: 'a ^ 'b) = y) \ (\i\ dimset x. x$i = y$i)" - unfolding Cart_nth_def forall_Abs_finite_image[symmetric, where P = "\i. Rep_Cart x i = Rep_Cart y i"] stupid_ext - using Rep_Cart_inject[of x y] .. - -consts Cart_lambda :: "(nat \ 'a) \ 'a ^ 'b" -notation (xsymbols) Cart_lambda (binder "\" 10) - -defs Cart_lambda_def: "Cart_lambda g == (SOME (f:: 'a ^ 'b). \i \ {1 .. DIM('b)}. f$i = g i)" -lemma Cart_lambda_beta: " \ i\ {1 .. DIM('b)}. (Cart_lambda g:: 'a ^ 'b)$i = g i" - unfolding Cart_lambda_def -proof (rule someI_ex) - let ?p = "\(i::nat) (k::'b finite_image). i \ {1 .. DIM('b)} \ (Abs_finite_image i = k)" - let ?f = "Abs_Cart (\k. g (THE i. ?p i k)):: 'a ^ 'b" - let ?P = "\f i. f$i = g i" - let ?Q = "\(f::'a ^ 'b). \ i \ {1 .. DIM('b)}. ?P f i" - {fix i - assume i: "i \ {1 .. DIM('b)}" - let ?j = "THE j. ?p j (Abs_finite_image i)" - from theI'[where P = "\j. ?p (j::nat) (Abs_finite_image i :: 'b finite_image)", OF Abs_finite_image_works[of "Abs_finite_image i :: 'b finite_image", unfolded Bex1_def]] - have j: "?j \ {1 .. DIM('b)}" "(Abs_finite_image ?j :: 'b finite_image) = Abs_finite_image i" by blast+ - from i j Abs_finite_image_inject[of i ?j, where ?'a = 'b] - have th: "?j = i" by (simp add: finite_image_def) - have "?P ?f i" - using th - by (simp add: Cart_nth_def Abs_Cart_inverse Rep_Cart_inverse Cart_def) } - hence th0: "?Q ?f" .. - with th0 show "\f. ?Q f" unfolding Ex1_def by auto -qed +lemma Cart_eq: "((x:: 'a ^ 'b) = y) \ (\i. x$i = y$i)" + by (simp add: Cart_nth_inject [symmetric] expand_fun_eq) -lemma Cart_lambda_beta': "i\ {1 .. DIM('b)} \ (Cart_lambda g:: 'a ^ 'b)$i = g i" - using Cart_lambda_beta by blast +lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i" + by (simp add: Cart_lambda_inverse) lemma Cart_lambda_unique: fixes f :: "'a ^ 'b" - shows "(\i\ {1 .. DIM('b)}. f$i = g i) \ Cart_lambda g = f" - by (auto simp add: Cart_eq Cart_lambda_beta) + shows "(\i. f$i = g i) \ Cart_lambda g = f" + by (auto simp add: Cart_eq) -lemma Cart_lambda_eta: "(\ i. (g$i)) = g" by (simp add: Cart_eq Cart_lambda_beta) +lemma Cart_lambda_eta: "(\ i. (g$i)) = g" + by (simp add: Cart_eq) text{* A non-standard sum to "paste" Cartesian products. *} -typedef ('a,'b) finite_sum = "{1 .. DIM('a) + DIM('b)}" - apply (rule exI[where x="1"]) - using dimindex_ge_1[of "UNIV :: 'a set"] dimindex_ge_1[of "UNIV :: 'b set"] - by auto +definition pastecart :: "'a ^ 'm \ 'a ^ 'n \ 'a ^ ('m + 'n)" where + "pastecart f g = (\ i. case i of Inl a \ f$a | Inr b \ g$b)" + +definition fstcart:: "'a ^('m + 'n) \ 'a ^ 'm" where + "fstcart f = (\ i. (f$(Inl i)))" -definition pastecart :: "'a ^ 'm \ 'a ^ 'n \ 'a ^ ('m,'n) finite_sum" where - "pastecart f g = (\ i. (if i <= DIM('m) then f$i else g$(i - DIM('m))))" +definition sndcart:: "'a ^('m + 'n) \ 'a ^ 'n" where + "sndcart f = (\ i. (f$(Inr i)))" -definition fstcart:: "'a ^('m, 'n) finite_sum \ 'a ^ 'm" where - "fstcart f = (\ i. (f$i))" - -definition sndcart:: "'a ^('m, 'n) finite_sum \ 'a ^ 'n" where - "sndcart f = (\ i. (f$(i + DIM('m))))" +lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a" + unfolding pastecart_def by simp -lemma finite_sum_image: "(UNIV::('a,'b) finite_sum set) = Abs_finite_sum ` {1 .. DIM('a) + DIM('b)}" -apply (auto simp add: image_def) -apply (rule_tac x="Rep_finite_sum x" in bexI) -apply (simp add: Rep_finite_sum_inverse) -using Rep_finite_sum[unfolded finite_sum_def, where ?'a = 'a and ?'b = 'b] -apply (simp add: Rep_finite_sum) -done +lemma nth_pastecart_Inr [simp]: "pastecart f g $ Inr b = g$b" + unfolding pastecart_def by simp + +lemma nth_fstcart [simp]: "fstcart f $ i = f $ Inl i" + unfolding fstcart_def by simp -lemma inj_on_Abs_finite_sum: "inj_on (Abs_finite_sum :: _ \ ('a,'b) finite_sum) {1 .. DIM('a) + DIM('b)}" - using Abs_finite_sum_inject[where ?'a = 'a and ?'b = 'b] - by (auto simp add: inj_on_def finite_sum_def) +lemma nth_sndtcart [simp]: "sndcart f $ i = f $ Inr i" + unfolding sndcart_def by simp -lemma dimindex_has_size_finite_sum: - "(UNIV::('m,'n) finite_sum set) hassize (DIM('m) + DIM('n))" - by (simp add: finite_sum_image hassize_def card_image[OF inj_on_Abs_finite_sum[where ?'a = 'm and ?'b = 'n]] del: One_nat_def) - -lemma dimindex_finite_sum: "DIM(('m,'n) finite_sum) = DIM('m) + DIM('n)" - using dimindex_has_size_finite_sum[where ?'n = 'n and ?'m = 'm, unfolded hassize_def] - by (simp add: dimindex_def) +lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \ range Inr" +by (auto, case_tac x, auto) lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = x" - by (simp add: pastecart_def fstcart_def Cart_eq Cart_lambda_beta dimindex_finite_sum) + by (simp add: Cart_eq) lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = y" - by (simp add: pastecart_def sndcart_def Cart_eq Cart_lambda_beta dimindex_finite_sum) + by (simp add: Cart_eq) lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z" -proof - - {fix i - assume H: "i \ DIM('b) + DIM('c)" - "\ i \ DIM('b)" - from H have ith: "i - DIM('b) \ {1 .. DIM('c)}" - apply simp by arith - from H have th0: "i - DIM('b) + DIM('b) = i" - by simp - have "(\ i. (z$(i + DIM('b))) :: 'a ^ 'c)$(i - DIM('b)) = z$i" - unfolding Cart_lambda_beta'[where g = "\ i. z$(i + DIM('b))", OF ith] th0 ..} -thus ?thesis by (auto simp add: pastecart_def fstcart_def sndcart_def Cart_eq Cart_lambda_beta dimindex_finite_sum) -qed + by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split) lemma pastecart_eq: "(x = y) \ (fstcart x = fstcart y) \ (sndcart x = sndcart y)" using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis @@ -216,53 +95,4 @@ lemma exists_pastecart: "(\p. P p) \ (\x y. P (pastecart x y))" by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) -text{* The finiteness lemma. *} - -lemma finite_cart: - "\i \ {1 .. DIM('n)}. finite {x. P i x} - \ finite {v::'a ^ 'n . (\i \ {1 .. DIM('n)}. P i (v$i))}" -proof- - assume f: "\i \ {1 .. DIM('n)}. finite {x. P i x}" - {fix n - assume n: "n \ DIM('n)" - have "finite {v:: 'a ^ 'n . (\i\ {1 .. DIM('n)}. i \ n \ P i (v$i)) - \ (\i\ {1 .. DIM('n)}. n < i \ v$i = (SOME x. False))}" - using n - proof(induct n) - case 0 - have th0: "{v . (\i \ {1 .. DIM('n)}. v$i = (SOME x. False))} = - {(\ i. (SOME x. False)::'a ^ 'n)}" by (auto simp add: Cart_lambda_beta Cart_eq) - with "0.prems" show ?case by auto - next - case (Suc n) - let ?h = "\(x::'a,v:: 'a ^ 'n). (\ i. if i = Suc n then x else v$i):: 'a ^ 'n" - let ?T = "{v\'a ^ 'n. - (\i\nat\{1\nat..DIM('n)}. i \ Suc n \ P i (v$i)) \ - (\i\nat\{1\nat..DIM('n)}. - Suc n < i \ v$i = (SOME x\'a. False))}" - let ?S = "{x::'a . P (Suc n) x} \ {v:: 'a^'n. (\i \ {1 .. DIM('n)}. i <= n \ P i (v$i)) \ (\i \ {1 .. DIM('n)}. n < i \ v$i = (SOME x. False))}" - have th0: " ?T \ (?h ` ?S)" - using Suc.prems - apply (auto simp add: image_def) - apply (rule_tac x = "x$(Suc n)" in exI) - apply (rule conjI) - apply (rotate_tac) - apply (erule ballE[where x="Suc n"]) - apply simp - apply simp - apply (rule_tac x= "\ i. if i = Suc n then (SOME x:: 'a. False) else (x:: 'a ^ 'n)$i:: 'a ^ 'n" in exI) - by (simp add: Cart_eq Cart_lambda_beta) - have th1: "finite ?S" - apply (rule finite_cartesian_product) - using f Suc.hyps Suc.prems by auto - from finite_imageI[OF th1] have th2: "finite (?h ` ?S)" . - from finite_subset[OF th0 th2] show ?case by blast - qed} - - note th = this - from this[of "DIM('n)"] f - show ?thesis by auto -qed - - end diff -r ac50e7dedf6d -r 638b088bb840 src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Wed Mar 18 22:17:23 2009 +0100 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Thu Mar 19 01:29:19 2009 -0700 @@ -488,7 +488,7 @@ subsection{* Limit points *} -definition islimpt:: "real ^'n \ (real^'n) set \ bool" (infixr "islimpt" 60) where +definition islimpt:: "real ^'n::finite \ (real^'n) set \ bool" (infixr "islimpt" 60) where islimpt_def: "x islimpt S \ (\T. x\T \ open T \ (\y\S. y\T \ y\x))" (* FIXME: Sure this form is OK????*) @@ -510,7 +510,7 @@ using approachable_lt_le[where f="\x'. dist x' x" and P="\x'. \ (x'\S \ x'\x)"] by metis -lemma islimpt_UNIV[simp, intro]: "(x:: real ^'n) islimpt UNIV" +lemma islimpt_UNIV[simp, intro]: "(x:: real ^'n::finite) islimpt UNIV" proof- { fix e::real assume ep: "e>0" @@ -532,20 +532,20 @@ lemma islimpt_EMPTY[simp]: "\ x islimpt {}" unfolding islimpt_approachable apply auto by ferrack -lemma closed_positive_orthant: "closed {x::real^'n. \i\{1.. dimindex(UNIV:: 'n set)}. 0 \x$i}" +lemma closed_positive_orthant: "closed {x::real^'n::finite. \i. 0 \x$i}" proof- - let ?U = "{1 .. dimindex(UNIV :: 'n set)}" - let ?O = "{x::real^'n. \i\?U. x$i\0}" - {fix x:: "real^'n" and i::nat assume H: "\e>0. \x'\?O. x' \ x \ dist x' x < e" and i: "i \ ?U" + let ?U = "UNIV :: 'n set" + let ?O = "{x::real^'n. \i. x$i\0}" + {fix x:: "real^'n" and i::'n assume H: "\e>0. \x'\?O. x' \ x \ dist x' x < e" and xi: "x$i < 0" from xi have th0: "-x$i > 0" by arith from H[rule_format, OF th0] obtain x' where x': "x' \?O" "x' \ x" "dist x' x < -x $ i" by blast have th:" \b a (x::real). abs x <= b \ b <= a ==> ~(a + x < 0)" by arith have th': "\x (y::real). x < 0 \ 0 <= y ==> abs x <= abs (y - x)" by arith - have th1: "\x$i\ \ \(x' - x)$i\" using i x'(1) xi + have th1: "\x$i\ \ \(x' - x)$i\" using x'(1) xi apply (simp only: vector_component) by (rule th') auto - have th2: "\dist x x'\ \ \(x' - x)$i\" using component_le_norm[OF i, of "x'-x"] + have th2: "\dist x x'\ \ \(x' - x)$i\" using component_le_norm[of "x'-x" i] apply (simp add: dist_def) by norm from th[OF th1 th2] x'(3) have False by (simp add: dist_sym dist_pos_le) } then show ?thesis unfolding closed_limpt islimpt_approachable @@ -965,7 +965,7 @@ definition within :: "'a net \ 'a set \ 'a net" (infixr "within" 70) where within_def: "net within S = mknet (\x y. netord net x y \ x \ S)" -definition indirection :: "real ^'n \ real ^'n \ (real ^'n) net" (infixr "indirection" 70) where +definition indirection :: "real ^'n::finite \ real ^'n \ (real ^'n) net" (infixr "indirection" 70) where indirection_def: "a indirection v = (at a) within {b. \c\0. b - a = c*s v}" text{* Prove That They are all nets. *} @@ -1019,7 +1019,7 @@ (\(a::'a) b. a = b) \ (\(a::'a) b. a \ b \ (\x. ~(netord (net) x a) \ ~(netord(net) x b)))" -lemma trivial_limit_within: "trivial_limit (at (a::real^'n) within S) \ ~(a islimpt S)" +lemma trivial_limit_within: "trivial_limit (at (a::real^'n::finite) within S) \ ~(a islimpt S)" proof- {assume "\(a::real^'n) b. a = b" hence "\ a islimpt S" apply (simp add: islimpt_approachable_le) @@ -1104,7 +1104,7 @@ apply (metis dlo_simps(7) dlo_simps(9) le_maxI2 min_max.le_iff_sup min_max.sup_absorb1 order_antisym_conv) done (* FIXME Declare this with P::'a::some_type \ bool *) -lemma eventually_at_infinity: "eventually (P::(real^'n \ bool)) at_infinity \ (\b. \x. norm x >= b \ P x)" (is "?lhs = ?rhs") +lemma eventually_at_infinity: "eventually (P::(real^'n::finite \ bool)) at_infinity \ (\b. \x. norm x >= b \ P x)" (is "?lhs = ?rhs") proof assume "?lhs" thus "?rhs" unfolding eventually_def at_infinity @@ -1145,7 +1145,7 @@ subsection{* Limits, defined as vacuously true when the limit is trivial. *} -definition tendsto:: "('a \ real ^'n) \ real ^'n \ 'a net \ bool" (infixr "--->" 55) where +definition tendsto:: "('a \ real ^'n::finite) \ real ^'n \ 'a net \ bool" (infixr "--->" 55) where tendsto_def: "(f ---> l) net \ (\e>0. eventually (\x. dist (f x) l < e) net)" lemma tendstoD: "(f ---> l) net \ e>0 \ eventually (\x. dist (f x) l < e) net" @@ -1177,7 +1177,7 @@ by (auto simp add: tendsto_def eventually_at) lemma Lim_at_infinity: - "(f ---> l) at_infinity \ (\e>0. \b. \x::real^'n. norm x >= b \ dist (f x) l < e)" + "(f ---> l) at_infinity \ (\e>0. \b. \x::real^'n::finite. norm x >= b \ dist (f x) l < e)" by (auto simp add: tendsto_def eventually_at_infinity) lemma Lim_sequentially: @@ -1210,7 +1210,7 @@ qed lemma Lim_Un_univ: - "(f ---> l) (at x within S) \ (f ---> l) (at x within T) \ S \ T = (UNIV::(real^'n) set) + "(f ---> l) (at x within S) \ (f ---> l) (at x within T) \ S \ T = (UNIV::(real^'n::finite) set) ==> (f ---> l) (at x)" by (metis Lim_Un within_UNIV) @@ -1275,7 +1275,7 @@ text{* Basic arithmetical combining theorems for limits. *} -lemma Lim_linear: fixes f :: "('a \ real^'n)" and h :: "(real^'n \ real^'m)" +lemma Lim_linear: fixes f :: "('a \ real^'n::finite)" and h :: "(real^'n \ real^'m::finite)" assumes "(f ---> l) net" "linear h" shows "((\x. h (f x)) ---> h l) net" proof (cases "trivial_limit net") @@ -1315,7 +1315,7 @@ apply (subst minus_diff_eq[symmetric]) unfolding norm_minus_cancel by simp -lemma Lim_add: fixes f :: "'a \ real^'n" shows +lemma Lim_add: fixes f :: "'a \ real^'n::finite" shows "(f ---> l) net \ (g ---> m) net \ ((\x. f(x) + g(x)) ---> l + m) net" proof- assume as:"(f ---> l) net" "(g ---> m) net" @@ -1368,14 +1368,14 @@ using assms `e>0` unfolding tendsto_def by auto qed -lemma Lim_component: "(f ---> l) net \ i \ {1 .. dimindex(UNIV:: 'n set)} - ==> ((\a. vec1((f a :: real ^'n)$i)) ---> vec1(l$i)) net" - apply (simp add: Lim dist_def vec1_sub[symmetric] norm_vec1 vector_minus_component[symmetric] del: One_nat_def) - apply auto +lemma Lim_component: "(f ---> l) net + ==> ((\a. vec1((f a :: real ^'n::finite)$i)) ---> vec1(l$i)) net" + apply (simp add: Lim dist_def vec1_sub[symmetric] norm_vec1 vector_minus_component[symmetric] del: vector_minus_component) + apply (auto simp del: vector_minus_component) apply (erule_tac x=e in allE) apply clarify apply (rule_tac x=y in exI) - apply auto + apply (auto simp del: vector_minus_component) apply (rule order_le_less_trans) apply (rule component_le_norm) by auto @@ -1450,7 +1450,7 @@ text{* Uniqueness of the limit, when nontrivial. *} lemma Lim_unique: - fixes l::"real^'a" and net::"'b::zero_neq_one net" + fixes l::"real^'a::finite" and net::"'b::zero_neq_one net" assumes "\(trivial_limit net)" "(f ---> l) net" "(f ---> l') net" shows "l = l'" proof- @@ -1472,7 +1472,7 @@ text{* Limit under bilinear function (surprisingly tedious, but important) *} lemma norm_bound_lemma: - "0 < e \ \d>0. \(x'::real^'b) y'::real^'a. norm(x' - (x::real^'b)) < d \ norm(y' - y) < d \ norm(x') * norm(y' - y) + norm(x' - x) * norm(y) < e" + "0 < e \ \d>0. \(x'::real^'b::finite) y'::real^'a::finite. norm(x' - (x::real^'b)) < d \ norm(y' - y) < d \ norm(x') * norm(y' - y) + norm(x' - x) * norm(y) < e" proof- assume e: "0 < e" have th1: "(2 * norm x + 2 * norm y + 2) > 0" using norm_ge_zero[of x] norm_ge_zero[of y] by norm @@ -1503,7 +1503,7 @@ qed lemma Lim_bilinear: - fixes net :: "'a net" and h:: "real ^'m \ real ^'n \ real ^'p" + fixes net :: "'a net" and h:: "real ^'m::finite \ real ^'n::finite \ real ^'p::finite" assumes "(f ---> l) net" and "(g ---> m) net" and "bilinear h" shows "((\x. h (f x) (g x)) ---> (h l m)) net" proof(cases "trivial_limit net") @@ -1541,7 +1541,7 @@ lemma Lim_at_id: "(id ---> a) (at a)" apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id) -lemma Lim_at_zero: "(f ---> l) (at (a::real^'a)) \ ((\x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs") +lemma Lim_at_zero: "(f ---> l) (at (a::real^'a::finite)) \ ((\x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs") proof assume "?lhs" { fix e::real assume "e>0" @@ -1619,7 +1619,7 @@ text{* Common case assuming being away from some crucial point like 0. *} lemma Lim_transform_away_within: - fixes f:: "real ^'m \ real ^'n" + fixes f:: "real ^'m::finite \ real ^'n::finite" assumes "a\b" "\x\ S. x \ a \ x \ b \ f x = g x" and "(f ---> l) (at a within S)" shows "(g ---> l) (at a within S)" @@ -1630,7 +1630,7 @@ qed lemma Lim_transform_away_at: - fixes f:: "real ^'m \ real ^'n" + fixes f:: "real ^'m::finite \ real ^'n::finite" assumes ab: "a\b" and fg: "\x. x \ a \ x \ b \ f x = g x" and fl: "(f ---> l) (at a)" shows "(g ---> l) (at a)" @@ -1640,7 +1640,7 @@ text{* Alternatively, within an open set. *} lemma Lim_transform_within_open: - fixes f:: "real ^'m \ real ^'n" + fixes f:: "real ^'m::finite \ real ^'n::finite" assumes "open S" "a \ S" "\x\S. x \ a \ f x = g x" "(f ---> l) (at a)" shows "(g ---> l) (at a)" proof- @@ -1917,7 +1917,7 @@ subsection{* Boundedness. *} (* FIXME: This has to be unified with BSEQ!! *) -definition "bounded S \ (\a. \(x::real^'n) \ S. norm x <= a)" +definition "bounded S \ (\a. \(x::real^'n::finite) \ S. norm x <= a)" lemma bounded_empty[simp]: "bounded {}" by (simp add: bounded_def) lemma bounded_subset: "bounded T \ S \ T ==> bounded S" @@ -1978,7 +1978,7 @@ lemma bounded_insert[intro]:"bounded(insert x S) \ bounded S" by (metis Diff_cancel Un_empty_right Un_insert_right bounded_Un bounded_subset finite.emptyI finite_imp_bounded infinite_remove subset_insertI) -lemma bot_bounded_UNIV[simp, intro]: "~(bounded (UNIV:: (real^'n) set))" +lemma bot_bounded_UNIV[simp, intro]: "~(bounded (UNIV:: (real^'n::finite) set))" proof(auto simp add: bounded_pos not_le) fix b::real assume b: "b >0" have b1: "b +1 \ 0" using b by simp @@ -1988,7 +1988,7 @@ qed lemma bounded_linear_image: - fixes f :: "real^'m \ real^'n" + fixes f :: "real^'m::finite \ real^'n::finite" assumes "bounded S" "linear f" shows "bounded(f ` S)" proof- @@ -2110,7 +2110,7 @@ subsection{* Compactness (the definition is the one based on convegent subsequences). *} definition "compact S \ - (\(f::nat \ real^'n). (\n. f n \ S) \ + (\(f::nat \ real^'n::finite). (\n. f n \ S) \ (\l\S. \r. (\m n. m < n \ r m < r n) \ ((f o r) ---> l) sequentially))" lemma monotone_bigger: fixes r::"nat\nat" @@ -2178,81 +2178,69 @@ qed lemma compact_lemma: - assumes "bounded s" and "\n. (x::nat \real^'a) n \ s" - shows "\d\{1.. dimindex(UNIV::'a set)}. - \l::(real^'a). \ r. (\n m::nat. m < n --> r m < r n) \ - (\e>0. \N. \n\N. \i\{1..d}. \x (r n) $ i - l $ i\ < e)" + assumes "bounded s" and "\n. (x::nat \real^'a::finite) n \ s" + shows "\d. + \l::(real^'a::finite). \ r. (\n m::nat. m < n --> r m < r n) \ + (\e>0. \N. \n\N. \i\d. \x (r n) $ i - l $ i\ < e)" proof- obtain b where b:"\x\s. norm x \ b" using assms(1)[unfolded bounded_def] by auto - { { fix i assume i:"i\{1.. dimindex(UNIV::'a set)}" + { { fix i::'a { fix n::nat - have "\x n $ i\ \ b" using b[THEN bspec[where x="x n"]] and component_le_norm[of i "x n"] and assms(2)[THEN spec[where x=n]] and i by auto } + have "\x n $ i\ \ b" using b[THEN bspec[where x="x n"]] and component_le_norm[of "x n" i] and assms(2)[THEN spec[where x=n]] by auto } hence "\n. \x n $ i\ \ b" by auto } note b' = this - fix d assume "d\{1.. dimindex(UNIV::'a set)}" + fix d::"'a set" have "finite d" by simp hence "\l::(real^'a). \ r. (\n m::nat. m < n --> r m < r n) \ - (\e>0. \N. \n\N. \i\{1..d}. \x (r n) $ i - l $ i\ < e)" - proof(induct d) case 0 thus ?case by auto - (* The induction really starts at Suc 0 *) - next case (Suc d) - show ?case proof(cases "d = 0") - case True hence "Suc d = Suc 0" by auto - obtain l r where r:"\m n::nat. m < n \ r m < r n" and lr:"\e>0. \N. \n\N. \x (r n) $ 1 - l\ < e" using b' and dimindex_ge_1[of "UNIV::'a set"] - using compact_real_lemma[of "\i. (x i)$1" b] by auto - thus ?thesis apply(rule_tac x="vec l" in exI) apply(rule_tac x=r in exI) - unfolding `Suc d = Suc 0` apply auto - unfolding vec_component[OF Suc(2)[unfolded `Suc d = Suc 0`]] by auto - next - case False hence d:"d \{1.. dimindex(UNIV::'a set)}" using Suc(2) by auto - obtain l1::"real^'a" and r1 where r1:"\n m::nat. m < n \ r1 m < r1 n" and lr1:"\e>0. \N. \n\N. \i\{1..d}. \x (r1 n) $ i - l1 $ i\ < e" - using Suc(1)[OF d] by auto - obtain l2 r2 where r2:"\m n::nat. m < n \ r2 m < r2 n" and lr2:"\e>0. \N. \n\N. \(x \ r1) (r2 n) $ (Suc d) - l2\ < e" - using b'[OF Suc(2)] and compact_real_lemma[of "\i. ((x \ r1) i)$(Suc d)" b] by auto + (\e>0. \N. \n\N. \i\d. \x (r n) $ i - l $ i\ < e)" + proof(induct d) case empty thus ?case by auto + next case (insert k d) + obtain l1::"real^'a" and r1 where r1:"\n m::nat. m < n \ r1 m < r1 n" and lr1:"\e>0. \N. \n\N. \i\d. \x (r1 n) $ i - l1 $ i\ < e" + using insert(3) by auto + obtain l2 r2 where r2:"\m n::nat. m < n \ r2 m < r2 n" and lr2:"\e>0. \N. \n\N. \(x \ r1) (r2 n) $ k - l2\ < e" + using b'[of k] and compact_real_lemma[of "\i. ((x \ r1) i)$k" b] by auto def r \ "r1 \ r2" have r:"\m n. m < n \ r m < r n" unfolding r_def o_def using r1 and r2 by auto moreover - def l \ "(\ i. if i = Suc d then l2 else l1$i)::real^'a" + def l \ "(\ i. if i = k then l2 else l1$i)::real^'a" { fix e::real assume "e>0" - from lr1 obtain N1 where N1:"\n\N1. \i\{1..d}. \x (r1 n) $ i - l1 $ i\ < e" using `e>0` by blast - from lr2 obtain N2 where N2:"\n\N2. \(x \ r1) (r2 n) $ (Suc d) - l2\ < e" using `e>0` by blast + from lr1 obtain N1 where N1:"\n\N1. \i\d. \x (r1 n) $ i - l1 $ i\ < e" using `e>0` by blast + from lr2 obtain N2 where N2:"\n\N2. \(x \ r1) (r2 n) $ k - l2\ < e" using `e>0` by blast { fix n assume n:"n\ N1 + N2" - fix i assume i:"i\{1..Suc d}" hence i':"i\{1.. dimindex(UNIV::'a set)}" using Suc by auto + fix i assume i:"i\(insert k d)" hence "\x (r n) $ i - l $ i\ < e" using N2[THEN spec[where x="n"]] and n using N1[THEN spec[where x="r2 n"]] and n using monotone_bigger[OF r] and i - unfolding l_def and r_def and Cart_lambda_beta'[OF i'] + unfolding l_def and r_def using monotone_bigger[OF r2, of n] by auto } - hence "\N. \n\N. \i\{1..Suc d}. \x (r n) $ i - l $ i\ < e" by blast } - ultimately show ?thesis by auto - qed + hence "\N. \n\N. \i\(insert k d). \x (r n) $ i - l $ i\ < e" by blast } + ultimately show ?case by auto qed } thus ?thesis by auto qed -lemma bounded_closed_imp_compact: fixes s::"(real^'a) set" +lemma bounded_closed_imp_compact: fixes s::"(real^'a::finite) set" assumes "bounded s" and "closed s" shows "compact s" proof- - let ?d = "dimindex (UNIV::'a set)" + let ?d = "UNIV::'a set" { fix f assume as:"\n::nat. f n \ s" obtain l::"real^'a" and r where r:"\n m::nat. m < n \ r m < r n" - and lr:"\e>0. \N. \n\N. \i\{1..?d}. \f (r n) $ i - l $ i\ < e" - using compact_lemma[OF assms(1) as, THEN bspec[where x="?d"]] and dimindex_ge_1[of "UNIV::'a set"] by auto + and lr:"\e>0. \N. \n\N. \i\?d. \f (r n) $ i - l $ i\ < e" + using compact_lemma[OF assms(1) as, THEN spec[where x="?d"]] by auto { fix e::real assume "e>0" - hence "0 < e / (real_of_nat ?d)" using dimindex_nonzero[of "UNIV::'a set"] using divide_pos_pos[of e, of "real_of_nat ?d"] by auto - then obtain N::nat where N:"\n\N. \i\{1..?d}. \f (r n) $ i - l $ i\ < e / (real_of_nat ?d)" using lr[THEN spec[where x="e / (real_of_nat ?d)"]] by blast + hence "0 < e / (real_of_nat (card ?d))" using zero_less_card_finite using divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto + then obtain N::nat where N:"\n\N. \i\?d. \f (r n) $ i - l $ i\ < e / (real_of_nat (card ?d))" using lr[THEN spec[where x="e / (real_of_nat (card ?d))"]] by blast { fix n assume n:"n\N" - have "1 \ {1..?d}" using dimindex_nonzero[of "UNIV::'a set"] by auto - hence "finite {1..?d}" "{1..?d} \ {}" by auto + hence "finite ?d" "?d \ {}" by auto moreover - { fix i assume i:"i \ {1..?d}" - hence "\((f \ r) n - l) $ i\ < e / real_of_nat ?d" using `n\N` using N[THEN spec[where x=n]] - apply auto apply(erule_tac x=i in ballE) unfolding vector_minus_component[OF i] by auto } - ultimately have "(\i = 1..?d. \((f \ r) n - l) $ i\) - < (\i = 1..?d. e / real_of_nat ?d)" - using setsum_strict_mono[of "{1..?d}" "\i. \((f \ r) n - l) $ i\" "\i. e / (real_of_nat ?d)"] by auto - hence "(\i = 1..?d. \((f \ r) n - l) $ i\) < e" unfolding setsum_constant using dimindex_nonzero[of "UNIV::'a set"] by auto + { fix i assume i:"i \ ?d" + hence "\((f \ r) n - l) $ i\ < e / real_of_nat (card ?d)" using `n\N` using N[THEN spec[where x=n]] + by auto } + ultimately have "(\i \ ?d. \((f \ r) n - l) $ i\) + < (\i \ ?d. e / real_of_nat (card ?d))" + using setsum_strict_mono[of "?d" "\i. \((f \ r) n - l) $ i\" "\i. e / (real_of_nat (card ?d))"] by auto + hence "(\i \ ?d. \((f \ r) n - l) $ i\) < e" unfolding setsum_constant by auto hence "dist ((f \ r) n) l < e" unfolding dist_def using norm_le_l1[of "(f \ r) n - l"] by auto } hence "\N. \n\N. dist ((f \ r) n) l < e" by auto } hence *:"((f \ r) ---> l) sequentially" unfolding Lim_sequentially by auto @@ -2268,7 +2256,7 @@ definition cauchy_def:"cauchy s \ (\e>0. \N. \m n. m \ N \ n \ N --> dist(s m)(s n) < e)" -definition complete_def:"complete s \ (\f::(nat=>real^'a). (\n. f n \ s) \ cauchy f +definition complete_def:"complete s \ (\f::(nat=>real^'a::finite). (\n. f n \ s) \ cauchy f --> (\l \ s. (f ---> l) sequentially))" lemma cauchy: "cauchy s \ (\e>0.\ N::nat. \n\N. dist(s n)(s N) < e)" (is "?lhs = ?rhs") @@ -2350,7 +2338,7 @@ lemma complete_univ: "complete UNIV" proof(simp add: complete_def, rule, rule) - fix f::"nat \ real^'n" assume "cauchy f" + fix f::"nat \ real^'n::finite" assume "cauchy f" hence "bounded (f`UNIV)" using cauchy_imp_bounded[of f] unfolding image_def by auto hence "compact (closure (f`UNIV))" using bounded_closed_imp_compact[of "closure (range f)"] by auto hence "complete (closure (range f))" using compact_imp_complete by auto @@ -2389,7 +2377,7 @@ subsection{* Total boundedness. *} -fun helper_1::"((real^'n) set) \ real \ nat \ real^'n" where +fun helper_1::"((real^'n::finite) set) \ real \ nat \ real^'n" where "helper_1 s e n = (SOME y::real^'n. y \ s \ (\m (dist (helper_1 s e m) y < e)))" declare helper_1.simps[simp del] @@ -2422,7 +2410,7 @@ subsection{* Heine-Borel theorem (following Burkill \& Burkill vol. 2) *} -lemma heine_borel_lemma: fixes s::"(real^'n) set" +lemma heine_borel_lemma: fixes s::"(real^'n::finite) set" assumes "compact s" "s \ (\ t)" "\b \ t. open b" shows "\e>0. \x \ s. \b \ t. ball x e \ b" proof(rule ccontr) @@ -2513,11 +2501,11 @@ subsection{* Complete the chain of compactness variants. *} -primrec helper_2::"(real \ real^'n) \ nat \ real ^'n" where +primrec helper_2::"(real \ real^'n::finite) \ nat \ real ^'n" where "helper_2 beyond 0 = beyond 0" | "helper_2 beyond (Suc n) = beyond (norm (helper_2 beyond n) + 1 )" -lemma bolzano_weierstrass_imp_bounded: fixes s::"(real^'n) set" +lemma bolzano_weierstrass_imp_bounded: fixes s::"(real^'n::finite) set" assumes "\t. infinite t \ t \ s --> (\x \ s. x islimpt t)" shows "bounded s" proof(rule ccontr) @@ -2576,7 +2564,7 @@ lemma sequence_infinite_lemma: assumes "\n::nat. (f n \ l)" "(f ---> l) sequentially" - shows "infinite {y::real^'a. (\ n. y = f n)}" + shows "infinite {y::real^'a::finite. (\ n. y = f n)}" proof(rule ccontr) let ?A = "(\x. dist x l) ` {y. \n. y = f n}" assume "\ infinite {y. \n. y = f n}" @@ -2771,7 +2759,7 @@ lemma bounded_closed_nest: assumes "\n. closed(s n)" "\n. (s n \ {})" "(\m n. m \ n --> s n \ s m)" "bounded(s 0)" - shows "\ a::real^'a. \n::nat. a \ s(n)" + shows "\ a::real^'a::finite. \n::nat. a \ s(n)" proof- from assms(2) obtain x where x:"\n::nat. x n \ s n" using choice[of "\n x. x\ s n"] by auto from assms(4,1) have *:"compact (s 0)" using bounded_closed_imp_compact[of "s 0"] by auto @@ -2803,7 +2791,7 @@ "\n. (s n \ {})" "\m n. m \ n --> s n \ s m" "\e>0. \n. \x \ (s n). \ y \ (s n). dist x y < e" - shows "\a::real^'a. \n::nat. a \ s n" + shows "\a::real^'a::finite. \n::nat. a \ s n" proof- have "\n. \ x. x\s n" using assms(2) by auto hence "\t. \n. t n \ s n" using choice[of "\ n x. x \ s n"] by auto @@ -2836,7 +2824,7 @@ "\n. s n \ {}" "\m n. m \ n --> s n \ s m" "\e>0. \n. \x \ (s n). \ y\(s n). dist x y < e" - shows "\a::real^'a. \ {t. (\n::nat. t = s n)} = {a}" + shows "\a::real^'a::finite. \ {t. (\n::nat. t = s n)} = {a}" proof- obtain a where a:"\n. a \ s n" using decreasing_closed_nest[of s] using assms by auto { fix b assume b:"b \ \{t. \n. t = s n}" @@ -2851,7 +2839,7 @@ text{* Cauchy-type criteria for uniform convergence. *} -lemma uniformly_convergent_eq_cauchy: fixes s::"nat \ 'b \ real^'a" shows +lemma uniformly_convergent_eq_cauchy: fixes s::"nat \ 'b \ real^'a::finite" shows "(\l. \e>0. \N. \n x. N \ n \ P x --> dist(s n x)(l x) < e) \ (\e>0. \N. \m n x. N \ m \ N \ n \ P x --> dist (s m x) (s n x) < e)" (is "?lhs = ?rhs") proof(rule) @@ -2960,7 +2948,7 @@ apply (auto simp add: dist_sym) apply(erule_tac x=e in allE) by auto qed -lemma continuous_at_ball: fixes f::"real^'a \ real^'a" +lemma continuous_at_ball: fixes f::"real^'a::finite \ real^'a" shows "continuous (at x) f \ (\e>0. \d>0. f ` (ball x d) \ ball (f x) e)" (is "?lhs = ?rhs") proof assume ?lhs thus ?rhs unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball @@ -3255,7 +3243,7 @@ lemma uniformly_continuous_on_add: assumes "uniformly_continuous_on s f" "uniformly_continuous_on s g" - shows "uniformly_continuous_on s (\x. f(x) + g(x) ::real^'n)" + shows "uniformly_continuous_on s (\x. f(x) + g(x) ::real^'n::finite)" proof- have *:"\fx fy gx gy::real^'n. fx - fy + (gx - gy) = fx + gx - (fy + gy)" by auto { fix x y assume "((\n. f (x n) - f (y n)) ---> 0) sequentially" @@ -3729,7 +3717,7 @@ subsection{* Topological properties of linear functions. *} -lemma linear_lim_0: fixes f::"real^'a \ real^'b" +lemma linear_lim_0: fixes f::"real^'a::finite \ real^'b::finite" assumes "linear f" shows "(f ---> 0) (at (0))" proof- obtain B where "B>0" and B:"\x. norm (f x) \ B * norm x" using linear_bounded_pos[OF assms] by auto @@ -3813,19 +3801,18 @@ unfolding continuous_on_vec1_range norm_vec1[THEN sym] by (metis norm_vec1 order_le_less_trans real_abs_sub_norm) lemma continuous_at_vec1_component: - assumes "1 \ i" "i \ dimindex(UNIV::('a set))" - shows "continuous (at (a::real^'a)) (\ x. vec1(x$i))" + shows "continuous (at (a::real^'a::finite)) (\ x. vec1(x$i))" proof- { fix e::real and x assume "0 < dist x a" "dist x a < e" "e>0" - hence "\x $ i - a $ i\ < e" using component_le_norm[of i "x - a"] vector_minus_component[of i x a] assms unfolding dist_def by auto } + hence "\x $ i - a $ i\ < e" using component_le_norm[of "x - a" i] unfolding dist_def by auto } thus ?thesis unfolding continuous_at tendsto_def eventually_at dist_vec1 by auto qed lemma continuous_on_vec1_component: - assumes "i \ {1..dimindex (UNIV::'a set)}" shows "continuous_on s (\ x::real^'a. vec1(x$i))" + shows "continuous_on s (\ x::real^'a::finite. vec1(x$i))" proof- { fix e::real and x xa assume "x\s" "e>0" "xa\s" "0 < norm (xa - x) \ norm (xa - x) < e" - hence "\xa $ i - x $ i\ < e" using component_le_norm[of i "xa - x"] vector_minus_component[of i xa x] assms by auto } + hence "\xa $ i - x $ i\ < e" using component_le_norm[of "xa - x" i] by auto } thus ?thesis unfolding continuous_on Lim_within dist_vec1 unfolding dist_def by auto qed @@ -4070,7 +4057,7 @@ proof- have *:"{x + y | x y. x \ s \ y \ t} =(\z. fstcart z + sndcart z) ` {pastecart x y | x y. x \ s \ y \ t}" apply auto unfolding image_iff apply(rule_tac x="pastecart xa y" in bexI) unfolding fstcart_pastecart sndcart_pastecart by auto - have "linear (\z::real^('a, 'a) finite_sum. fstcart z + sndcart z)" unfolding linear_def + have "linear (\z::real^('a + 'a). fstcart z + sndcart z)" unfolding linear_def unfolding fstcart_add sndcart_add apply auto unfolding vector_add_ldistrib fstcart_cmul[THEN sym] sndcart_cmul[THEN sym] by auto hence "continuous_on {pastecart x y |x y. x \ s \ y \ t} (\z. fstcart z + sndcart z)" @@ -4306,90 +4293,86 @@ (* A cute way of denoting open and closed intervals using overloading. *) -lemma interval: fixes a :: "'a::ord^'n" shows - "{a <..< b} = {x::'a^'n. \i \ dimset a. a$i < x$i \ x$i < b$i}" and - "{a .. b} = {x::'a^'n. \i \ dimset a. a$i \ x$i \ x$i \ b$i}" +lemma interval: fixes a :: "'a::ord^'n::finite" shows + "{a <..< b} = {x::'a^'n. \i. a$i < x$i \ x$i < b$i}" and + "{a .. b} = {x::'a^'n. \i. a$i \ x$i \ x$i \ b$i}" by (auto simp add: expand_set_eq vector_less_def vector_less_eq_def) -lemma mem_interval: - "x \ {a<.. (\i \ dimset a. a$i < x$i \ x$i < b$i)" - "x \ {a .. b} \ (\i \ dimset a. a$i \ x$i \ x$i \ b$i)" +lemma mem_interval: fixes a :: "'a::ord^'n::finite" shows + "x \ {a<.. (\i. a$i < x$i \ x$i < b$i)" + "x \ {a .. b} \ (\i. a$i \ x$i \ x$i \ b$i)" using interval[of a b] by(auto simp add: expand_set_eq vector_less_def vector_less_eq_def) -lemma interval_eq_empty: fixes a :: "real^'n" shows - "({a <..< b} = {} \ (\i \ dimset a. b$i \ a$i))" (is ?th1) and - "({a .. b} = {} \ (\i \ dimset a. b$i < a$i))" (is ?th2) +lemma interval_eq_empty: fixes a :: "real^'n::finite" shows + "({a <..< b} = {} \ (\i. b$i \ a$i))" (is ?th1) and + "({a .. b} = {} \ (\i. b$i < a$i))" (is ?th2) proof- - { fix i x assume i:"i\dimset a" and as:"b$i \ a$i" and x:"x\{a <..< b}" + { fix i x assume as:"b$i \ a$i" and x:"x\{a <..< b}" hence "a $ i < x $ i \ x $ i < b $ i" unfolding mem_interval by auto hence "a$i < b$i" by auto hence False using as by auto } moreover - { assume as:"\i \ dimset a. \ (b$i \ a$i)" + { assume as:"\i. \ (b$i \ a$i)" let ?x = "(1/2) *s (a + b)" - { fix i assume i:"i\dimset a" - hence "a$i < b$i" using as[THEN bspec[where x=i]] by auto + { fix i + have "a$i < b$i" using as[THEN spec[where x=i]] by auto hence "a$i < ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i < b$i" - unfolding vector_smult_component[OF i] and vector_add_component[OF i] + unfolding vector_smult_component and vector_add_component by (auto simp add: Arith_Tools.less_divide_eq_number_of1) } hence "{a <..< b} \ {}" using mem_interval(1)[of "?x" a b] by auto } ultimately show ?th1 by blast - { fix i x assume i:"i\dimset a" and as:"b$i < a$i" and x:"x\{a .. b}" + { fix i x assume as:"b$i < a$i" and x:"x\{a .. b}" hence "a $ i \ x $ i \ x $ i \ b $ i" unfolding mem_interval by auto hence "a$i \ b$i" by auto hence False using as by auto } moreover - { assume as:"\i \ dimset a. \ (b$i < a$i)" + { assume as:"\i. \ (b$i < a$i)" let ?x = "(1/2) *s (a + b)" - { fix i assume i:"i\dimset a" - hence "a$i \ b$i" using as[THEN bspec[where x=i]] by auto + { fix i + have "a$i \ b$i" using as[THEN spec[where x=i]] by auto hence "a$i \ ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i \ b$i" - unfolding vector_smult_component[OF i] and vector_add_component[OF i] + unfolding vector_smult_component and vector_add_component by (auto simp add: Arith_Tools.less_divide_eq_number_of1) } hence "{a .. b} \ {}" using mem_interval(2)[of "?x" a b] by auto } ultimately show ?th2 by blast qed -lemma interval_ne_empty: fixes a :: "real^'n" shows - "{a .. b} \ {} \ (\i \ dimset a. a$i \ b$i)" and - "{a <..< b} \ {} \ (\i \ dimset a. a$i < b$i)" - unfolding interval_eq_empty[of a b] by auto - -lemma subset_interval_imp: fixes a :: "real^'n" shows - "(\i \ dimset a. a$i \ c$i \ d$i \ b$i) \ {c .. d} \ {a .. b}" and - "(\i \ dimset a. a$i < c$i \ d$i < b$i) \ {c .. d} \ {a<..i \ dimset a. a$i \ c$i \ d$i \ b$i) \ {c<.. {a .. b}" and - "(\i \ dimset a. a$i \ c$i \ d$i \ b$i) \ {c<.. {a<.. {} \ (\i. a$i \ b$i)" and + "{a <..< b} \ {} \ (\i. a$i < b$i)" + unfolding interval_eq_empty[of a b] by (auto simp add: not_less not_le) (* BH: Why doesn't just "auto" work here? *) + +lemma subset_interval_imp: fixes a :: "real^'n::finite" shows + "(\i. a$i \ c$i \ d$i \ b$i) \ {c .. d} \ {a .. b}" and + "(\i. a$i < c$i \ d$i < b$i) \ {c .. d} \ {a<..i. a$i \ c$i \ d$i \ b$i) \ {c<.. {a .. b}" and + "(\i. a$i \ c$i \ d$i \ b$i) \ {c<.. {a<.. {a<.. {a .. b}" proof(simp add: subset_eq, rule) fix x assume x:"x \{a<.. dimset a" - hence "a $ i \ x $ i" + { fix i + have "a $ i \ x $ i" using x order_less_imp_le[of "a$i" "x$i"] by(simp add: expand_set_eq vector_less_def vector_less_eq_def Cart_eq) } moreover - { fix i assume "i \ dimset a" - hence "x $ i \ b $ i" - using x + { fix i + have "x $ i \ b $ i" using x order_less_imp_le[of "x$i" "b$i"] by(simp add: expand_set_eq vector_less_def vector_less_eq_def Cart_eq) } @@ -4398,76 +4381,76 @@ by(simp add: expand_set_eq vector_less_def vector_less_eq_def Cart_eq) qed -lemma subset_interval: fixes a :: "real^'n" shows - "{c .. d} \ {a .. b} \ (\i \ dimset a. c$i \ d$i) --> (\i \ dimset a. a$i \ c$i \ d$i \ b$i)" (is ?th1) and - "{c .. d} \ {a<.. (\i \ dimset a. c$i \ d$i) --> (\i \ dimset a. a$i < c$i \ d$i < b$i)" (is ?th2) and - "{c<.. {a .. b} \ (\i \ dimset a. c$i < d$i) --> (\i \ dimset a. a$i \ c$i \ d$i \ b$i)" (is ?th3) and - "{c<.. {a<.. (\i \ dimset a. c$i < d$i) --> (\i \ dimset a. a$i \ c$i \ d$i \ b$i)" (is ?th4) +lemma subset_interval: fixes a :: "real^'n::finite" shows + "{c .. d} \ {a .. b} \ (\i. c$i \ d$i) --> (\i. a$i \ c$i \ d$i \ b$i)" (is ?th1) and + "{c .. d} \ {a<.. (\i. c$i \ d$i) --> (\i. a$i < c$i \ d$i < b$i)" (is ?th2) and + "{c<.. {a .. b} \ (\i. c$i < d$i) --> (\i. a$i \ c$i \ d$i \ b$i)" (is ?th3) and + "{c<.. {a<.. (\i. c$i < d$i) --> (\i. a$i \ c$i \ d$i \ b$i)" (is ?th4) proof- - show ?th1 unfolding subset_eq and Ball_def and mem_interval apply auto by(erule_tac x=xa in allE, simp)+ - show ?th2 unfolding subset_eq and Ball_def and mem_interval apply auto by(erule_tac x=xa in allE, simp)+ - { assume as: "{c<.. {a .. b}" "\i \ dimset a. c$i < d$i" - hence "{c<.. {}" unfolding interval_eq_empty by auto - fix i assume i:"i \ dimset a" + show ?th1 unfolding subset_eq and Ball_def and mem_interval by (auto intro: order_trans) + show ?th2 unfolding subset_eq and Ball_def and mem_interval by (auto intro: le_less_trans less_le_trans order_trans less_imp_le) + { assume as: "{c<.. {a .. b}" "\i. c$i < d$i" + hence "{c<.. {}" unfolding interval_eq_empty by (auto, drule_tac x=i in spec, simp) (* BH: Why doesn't just "auto" work? *) + fix i (** TODO combine the following two parts as done in the HOL_light version. **) { let ?x = "(\ j. (if j=i then ((min (a$j) (d$j))+c$j)/2 else (c$j+d$j)/2))::real^'n" assume as2: "a$i > c$i" - { fix j assume j:"j\dimset a" - hence "c $ j < ?x $ j \ ?x $ j < d $ j" unfolding Cart_lambda_beta[THEN bspec[where x=j], OF j] - apply(cases "j=i") using as(2)[THEN bspec[where x=j], OF j] + { fix j + have "c $ j < ?x $ j \ ?x $ j < d $ j" unfolding Cart_lambda_beta + apply(cases "j=i") using as(2)[THEN spec[where x=j]] by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2) } hence "?x\{c<..{a .. b}" - unfolding mem_interval apply auto apply(rule_tac x=i in bexI) - unfolding Cart_lambda_beta[THEN bspec[where x=i], OF i] - using as(2)[THEN bspec[where x=i], OF i] and as2 and i + unfolding mem_interval apply auto apply(rule_tac x=i in exI) + using as(2)[THEN spec[where x=i]] and as2 by (auto simp add: Arith_Tools.less_divide_eq_number_of1) ultimately have False using as by auto } hence "a$i \ c$i" by(rule ccontr)auto moreover { let ?x = "(\ j. (if j=i then ((max (b$j) (c$j))+d$j)/2 else (c$j+d$j)/2))::real^'n" assume as2: "b$i < d$i" - { fix j assume j:"j\dimset a" - hence "d $ j > ?x $ j \ ?x $ j > c $ j" unfolding Cart_lambda_beta[THEN bspec[where x=j], OF j] - apply(cases "j=i") using as(2)[THEN bspec[where x=j], OF j] + { fix j + have "d $ j > ?x $ j \ ?x $ j > c $ j" unfolding Cart_lambda_beta + apply(cases "j=i") using as(2)[THEN spec[where x=j]] by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2) } hence "?x\{c<..{a .. b}" - unfolding mem_interval apply auto apply(rule_tac x=i in bexI) - unfolding Cart_lambda_beta[THEN bspec[where x=i], OF i] - using as(2)[THEN bspec[where x=i], OF i] and as2 and i + unfolding mem_interval apply auto apply(rule_tac x=i in exI) + using as(2)[THEN spec[where x=i]] and as2 by (auto simp add: Arith_Tools.less_divide_eq_number_of1) ultimately have False using as by auto } hence "b$i \ d$i" by(rule ccontr)auto ultimately have "a$i \ c$i \ d$i \ b$i" by auto } note part1 = this - thus ?th3 unfolding subset_eq and Ball_def and mem_interval apply auto by(erule_tac x=xa in allE, simp)+ - { assume as:"{c<.. {a<..i \ dimset a. c$i < d$i" - fix i assume i:"i \ dimset a" + thus ?th3 unfolding subset_eq and Ball_def and mem_interval apply auto apply (erule_tac x=ia in allE, simp)+ by (erule_tac x=i in allE, erule_tac x=i in allE, simp)+ + { assume as:"{c<.. {a<..i. c$i < d$i" + fix i from as(1) have "{c<.. {a..b}" using interval_open_subset_closed[of a b] by auto - hence "a$i \ c$i \ d$i \ b$i" using part1 and as(2) and i by auto } note * = this - thus ?th4 unfolding subset_eq and Ball_def and mem_interval apply auto by(erule_tac x=xa in allE, simp)+ -qed - -lemma disjoint_interval: fixes a::"real^'n" shows - "{a .. b} \ {c .. d} = {} \ (\i \ dimset a. (b$i < a$i \ d$i < c$i \ b$i < c$i \ d$i < a$i))" (is ?th1) and - "{a .. b} \ {c<.. (\i \ dimset a. (b$i < a$i \ d$i \ c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th2) and - "{a<.. {c .. d} = {} \ (\i \ dimset a. (b$i \ a$i \ d$i < c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th3) and - "{a<.. {c<.. (\i \ dimset a. (b$i \ a$i \ d$i \ c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th4) + hence "a$i \ c$i \ d$i \ b$i" using part1 and as(2) by auto } note * = this + thus ?th4 unfolding subset_eq and Ball_def and mem_interval apply auto apply (erule_tac x=ia in allE, simp)+ by (erule_tac x=i in allE, erule_tac x=i in allE, simp)+ +qed + +lemma disjoint_interval: fixes a::"real^'n::finite" shows + "{a .. b} \ {c .. d} = {} \ (\i. (b$i < a$i \ d$i < c$i \ b$i < c$i \ d$i < a$i))" (is ?th1) and + "{a .. b} \ {c<.. (\i. (b$i < a$i \ d$i \ c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th2) and + "{a<.. {c .. d} = {} \ (\i. (b$i \ a$i \ d$i < c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th3) and + "{a<.. {c<.. (\i. (b$i \ a$i \ d$i \ c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th4) proof- let ?z = "(\ i. ((max (a$i) (c$i)) + (min (b$i) (d$i))) / 2)::real^'n" show ?th1 ?th2 ?th3 ?th4 - unfolding expand_set_eq and Int_iff and empty_iff and mem_interval and ball_conj_distrib[THEN sym] and eq_False - by (auto simp add: Cart_lambda_beta' Arith_Tools.less_divide_eq_number_of1 intro!: bexI elim!: allE[where x="?z"]) -qed - -lemma inter_interval: fixes a :: "'a::linorder^'n" shows + unfolding expand_set_eq and Int_iff and empty_iff and mem_interval and all_conj_distrib[THEN sym] and eq_False + apply (auto elim!: allE[where x="?z"]) + apply ((rule_tac x=x in exI, force) | (rule_tac x=i in exI, force))+ + done +qed + +lemma inter_interval: fixes a :: "'a::linorder^'n::finite" shows "{a .. b} \ {c .. d} = {(\ i. max (a$i) (c$i)) .. (\ i. min (b$i) (d$i))}" unfolding expand_set_eq and Int_iff and mem_interval - by (auto simp add: Cart_lambda_beta' Arith_Tools.less_divide_eq_number_of1 intro!: bexI) + by (auto simp add: Arith_Tools.less_divide_eq_number_of1 intro!: bexI) (* Moved interval_open_subset_closed a bit upwards *) @@ -4475,54 +4458,54 @@ "a < x \ x < b ==> (\d>0. \x'. abs(x' - x) < d --> a < x' \ x' < b)" by(rule_tac x="min (x - a) (b - x)" in exI, auto) -lemma open_interval: fixes a :: "real^'n" shows "open {a<..{a<..dimset x" - hence "\d>0. \x'. abs (x' - (x$i)) < d \ a$i < x' \ x' < b$i" - using x[unfolded mem_interval, THEN bspec[where x=i]] + { fix i + have "\d>0. \x'. abs (x' - (x$i)) < d \ a$i < x' \ x' < b$i" + using x[unfolded mem_interval, THEN spec[where x=i]] using open_interval_lemma[of "a$i" "x$i" "b$i"] by auto } - hence "\i\dimset x. \d>0. \x'. abs (x' - (x$i)) < d \ a$i < x' \ x' < b$i" by auto - then obtain d where d:"\i\dimset x. 0 < d i \ (\x'. \x' - x $ i\ < d i \ a $ i < x' \ x' < b $ i)" - using bchoice[of "dimset x" "\i d. d>0 \ (\x'. \x' - x $ i\ < d \ a $ i < x' \ x' < b $ i)"] by auto - - let ?d = "Min (d ` dimset x)" - have **:"finite (d ` dimset x)" "d ` dimset x \ {}" using dimindex_ge_1[of "UNIV::'n set"] by auto + hence "\i. \d>0. \x'. abs (x' - (x$i)) < d \ a$i < x' \ x' < b$i" by auto + then obtain d where d:"\i. 0 < d i \ (\x'. \x' - x $ i\ < d i \ a $ i < x' \ x' < b $ i)" + using bchoice[of "UNIV" "\i d. d>0 \ (\x'. \x' - x $ i\ < d \ a $ i < x' \ x' < b $ i)"] by auto + + let ?d = "Min (range d)" + have **:"finite (range d)" "range d \ {}" by auto have "?d>0" unfolding Min_gr_iff[OF **] using d by auto moreover { fix x' assume as:"dist x' x < ?d" - { fix i assume i:"i \ dimset x" + { fix i have "\x'$i - x $ i\ < d i" - using norm_bound_component_lt[OF as[unfolded dist_def], THEN bspec[where x=i], OF i] - unfolding vector_minus_component[OF i] and Min_gr_iff[OF **] using i by auto - hence "a $ i < x' $ i" "x' $ i < b $ i" using d[THEN bspec[where x=i], OF i] by auto } + using norm_bound_component_lt[OF as[unfolded dist_def], of i] + unfolding vector_minus_component and Min_gr_iff[OF **] by auto + hence "a $ i < x' $ i" "x' $ i < b $ i" using d[THEN spec[where x=i]] by auto } hence "a < x' \ x' < b" unfolding vector_less_def by auto } - ultimately have "\e>0. \x'. dist x' x < e \ x' \ {a<..e>0. \x'. dist x' x < e \ x' \ {a<..dimset x" and as:"\e>0. \x'\{a..b}. x' \ x \ dist x' x < e"(* and xab:"a$i > x$i \ b$i < x$i"*) + { fix x i assume as:"\e>0. \x'\{a..b}. x' \ x \ dist x' x < e"(* and xab:"a$i > x$i \ b$i < x$i"*) { assume xa:"a$i > x$i" with as obtain y where y:"y\{a..b}" "y \ x" "dist y x < a$i - x$i" by(erule_tac x="a$i - x$i" in allE)auto hence False unfolding mem_interval and dist_def - using component_le_norm[OF i, of "y-x", unfolded vector_minus_component[OF i]] and i and xa by(auto elim!: ballE[where x=i]) + using component_le_norm[of "y-x" i, unfolded vector_minus_component] and xa by(auto elim!: allE[where x=i]) } hence "a$i \ x$i" by(rule ccontr)auto moreover { assume xb:"b$i < x$i" with as obtain y where y:"y\{a..b}" "y \ x" "dist y x < x$i - b$i" by(erule_tac x="x$i - b$i" in allE)auto hence False unfolding mem_interval and dist_def - using component_le_norm[OF i, of "y-x", unfolded vector_minus_component[OF i]] and i and xb by(auto elim!: ballE[where x=i]) + using component_le_norm[of "y-x" i, unfolded vector_minus_component] and xb by(auto elim!: allE[where x=i]) } hence "x$i \ b$i" by(rule ccontr)auto ultimately have "a $ i \ x $ i \ x $ i \ b $ i" by auto } thus ?thesis unfolding closed_limpt islimpt_approachable mem_interval by auto qed -lemma interior_closed_interval: fixes a :: "real^'n" shows +lemma interior_closed_interval: fixes a :: "real^'n::finite" shows "interior {a .. b} = {a<.. ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto @@ -4530,85 +4513,87 @@ { fix x assume "\T. open T \ x \ T \ T \ {a..b}" then obtain s where s:"open s" "x \ s" "s \ {a..b}" by auto then obtain e where "e>0" and e:"\x'. dist x' x < e \ x' \ {a..b}" unfolding open_def and subset_eq by auto - { fix i assume i:"i\dimset x" + { fix i have "dist (x - (e / 2) *s basis i) x < e" "dist (x + (e / 2) *s basis i) x < e" unfolding dist_def apply auto - unfolding norm_minus_cancel and norm_mul using norm_basis[OF i] and `e>0` by auto + unfolding norm_minus_cancel and norm_mul using norm_basis[of i] and `e>0` by auto hence "a $ i \ (x - (e / 2) *s basis i) $ i" "(x + (e / 2) *s basis i) $ i \ b $ i" using e[THEN spec[where x="x - (e/2) *s basis i"]] and e[THEN spec[where x="x + (e/2) *s basis i"]] - unfolding mem_interval using i by auto + unfolding mem_interval by (auto elim!: allE[where x=i]) hence "a $ i < x $ i" and "x $ i < b $ i" - unfolding vector_minus_component[OF i] and vector_add_component[OF i] - unfolding vector_smult_component[OF i] and basis_component[OF i] using `e>0` by auto } + unfolding vector_minus_component and vector_add_component + unfolding vector_smult_component and basis_component using `e>0` by auto } hence "x \ {a<.. ?R" unfolding interior_def and subset_eq by auto qed -lemma bounded_closed_interval: fixes a :: "real^'n" shows +lemma bounded_closed_interval: fixes a :: "real^'n::finite" shows "bounded {a .. b}" proof- - let ?b = "\i\dimset a. \a$i\ + \b$i\" - { fix x::"real^'n" assume x:"\i\dimset a. a $ i \ x $ i \ x $ i \ b $ i" - { fix i assume "i\dimset a" - hence "\x$i\ \ \a$i\ + \b$i\" using x[THEN bspec[where x=i]] by auto } - hence "(\i\dimset a. \x $ i\) \ ?b" by(rule setsum_mono)auto + let ?b = "\i\UNIV. \a$i\ + \b$i\" + { fix x::"real^'n" assume x:"\i. a $ i \ x $ i \ x $ i \ b $ i" + { fix i + have "\x$i\ \ \a$i\ + \b$i\" using x[THEN spec[where x=i]] by auto } + hence "(\i\UNIV. \x $ i\) \ ?b" by(rule setsum_mono) hence "norm x \ ?b" using norm_le_l1[of x] by auto } thus ?thesis unfolding interval and bounded_def by auto qed -lemma bounded_interval: fixes a :: "real^'n" shows +lemma bounded_interval: fixes a :: "real^'n::finite" shows "bounded {a .. b} \ bounded {a<.. UNIV) \ ({a<.. UNIV)" using bounded_interval[of a b] by auto -lemma compact_interval: fixes a :: "real^'n" shows +lemma compact_interval: fixes a :: "real^'n::finite" shows "compact {a .. b}" using bounded_closed_imp_compact using bounded_interval[of a b] using closed_interval[of a b] by auto -lemma open_interval_midpoint: fixes a :: "real^'n" +lemma open_interval_midpoint: fixes a :: "real^'n::finite" assumes "{a<.. {}" shows "((1/2) *s (a + b)) \ {a<..dimset a" - hence "a $ i < ((1 / 2) *s (a + b)) $ i \ ((1 / 2) *s (a + b)) $ i < b $ i" - using assms[unfolded interval_ne_empty, THEN bspec[where x=i]] - unfolding vector_smult_component[OF i] and vector_add_component[OF i] + { fix i + have "a $ i < ((1 / 2) *s (a + b)) $ i \ ((1 / 2) *s (a + b)) $ i < b $ i" + using assms[unfolded interval_ne_empty, THEN spec[where x=i]] + unfolding vector_smult_component and vector_add_component by(auto simp add: Arith_Tools.less_divide_eq_number_of1) } thus ?thesis unfolding mem_interval by auto qed -lemma open_closed_interval_convex: fixes x :: "real^'n" +lemma open_closed_interval_convex: fixes x :: "real^'n::finite" assumes x:"x \ {a<.. {a .. b}" and e:"0 < e" "e \ 1" shows "(e *s x + (1 - e) *s y) \ {a<..dimset a" + { fix i have "a $ i = e * a$i + (1 - e) * a$i" unfolding left_diff_distrib by simp also have "\ < e * x $ i + (1 - e) * y $ i" apply(rule add_less_le_mono) using e unfolding mult_less_cancel_left and mult_le_cancel_left apply simp_all - using x i unfolding mem_interval apply(erule_tac x=i in ballE) apply simp_all - using y i unfolding mem_interval apply(erule_tac x=i in ballE) by simp_all - finally have "a $ i < (e *s x + (1 - e) *s y) $ i" using i by (auto simp add: vector_add_component vector_smult_component) + using x unfolding mem_interval apply simp + using y unfolding mem_interval apply simp + done + finally have "a $ i < (e *s x + (1 - e) *s y) $ i" by auto moreover { have "b $ i = e * b$i + (1 - e) * b$i" unfolding left_diff_distrib by simp also have "\ > e * x $ i + (1 - e) * y $ i" apply(rule add_less_le_mono) using e unfolding mult_less_cancel_left and mult_le_cancel_left apply simp_all - using x i unfolding mem_interval apply(erule_tac x=i in ballE) apply simp_all - using y i unfolding mem_interval apply(erule_tac x=i in ballE) by simp_all - finally have "(e *s x + (1 - e) *s y) $ i < b $ i" using i by (auto simp add: vector_add_component vector_smult_component) + using x unfolding mem_interval apply simp + using y unfolding mem_interval apply simp + done + finally have "(e *s x + (1 - e) *s y) $ i < b $ i" by auto } ultimately have "a $ i < (e *s x + (1 - e) *s y) $ i \ (e *s x + (1 - e) *s y) $ i < b $ i" by auto } thus ?thesis unfolding mem_interval by auto qed -lemma closure_open_interval: fixes a :: "real^'n" +lemma closure_open_interval: fixes a :: "real^'n::finite" assumes "{a<.. {}" shows "closure {a<..a. s \ {-a<..0" and b:"\x\s. norm x \ b" using assms[unfolded bounded_pos] by auto def a \ "(\ i. b+1)::real^'n" { fix x assume "x\s" - fix i assume i:"i\dimset a" - have "(-a)$i < x$i" and "x$i < a$i" using b[THEN bspec[where x=x], OF `x\s`] and component_le_norm[OF i, of x] - unfolding vector_uminus_component[OF i] and a_def and Cart_lambda_beta'[OF i] by auto + fix i + have "(-a)$i < x$i" and "x$i < a$i" using b[THEN bspec[where x=x], OF `x\s`] and component_le_norm[of x i] + unfolding vector_uminus_component and a_def and Cart_lambda_beta by auto } thus ?thesis by(auto intro: exI[where x=a] simp add: vector_less_def) qed @@ -4679,30 +4664,32 @@ case False thus ?thesis unfolding frontier_def and closure_open_interval[OF False] and interior_open[OF open_interval] by auto qed -lemma inter_interval_mixed_eq_empty: fixes a :: "real^'n" +lemma inter_interval_mixed_eq_empty: fixes a :: "real^'n::finite" assumes "{c<.. {}" shows "{a<.. {c .. d} = {} \ {a<.. {c<..x::1. P x) \ P 1" + by (metis num1_eq_iff) + +lemma ex_1: "(\x::1. P x) \ P 1" + by auto (metis num1_eq_iff) lemma interval_cases_1: fixes x :: "real^1" shows "x \ {a .. b} ==> x \ {a<.. (x = a) \ (x = b)" - by(simp add: Cart_eq vector_less_def vector_less_eq_def dim1, auto) + by(simp add: Cart_eq vector_less_def vector_less_eq_def all_1, auto) lemma in_interval_1: fixes x :: "real^1" shows "(x \ {a .. b} \ dest_vec1 a \ dest_vec1 x \ dest_vec1 x \ dest_vec1 b) \ (x \ {a<.. dest_vec1 a < dest_vec1 x \ dest_vec1 x < dest_vec1 b)" -by(simp add: Cart_eq vector_less_def vector_less_eq_def dim1 dest_vec1_def) +by(simp add: Cart_eq vector_less_def vector_less_eq_def all_1 dest_vec1_def) lemma interval_eq_empty_1: fixes a :: "real^1" shows "{a .. b} = {} \ dest_vec1 b < dest_vec1 a" "{a<.. dest_vec1 b \ dest_vec1 a" - unfolding interval_eq_empty and dim1 and dest_vec1_def by auto + unfolding interval_eq_empty and ex_1 and dest_vec1_def by auto lemma subset_interval_1: fixes a :: "real^1" shows "({a .. b} \ {c .. d} \ dest_vec1 b < dest_vec1 a \ @@ -4713,7 +4700,7 @@ dest_vec1 c \ dest_vec1 a \ dest_vec1 a < dest_vec1 b \ dest_vec1 b \ dest_vec1 d)" "({a<.. {c<.. dest_vec1 b \ dest_vec1 a \ dest_vec1 c \ dest_vec1 a \ dest_vec1 a < dest_vec1 b \ dest_vec1 b \ dest_vec1 d)" - unfolding subset_interval[of a b c d] unfolding forall_dimindex_1 and dest_vec1_def by auto + unfolding subset_interval[of a b c d] unfolding all_1 and dest_vec1_def by auto lemma eq_interval_1: fixes a :: "real^1" shows "{a .. b} = {c .. d} \ @@ -4729,37 +4716,37 @@ "{a .. b} \ {c<.. dest_vec1 b < dest_vec1 a \ dest_vec1 d \ dest_vec1 c \ dest_vec1 b \ dest_vec1 c \ dest_vec1 d \ dest_vec1 a" "{a<.. {c .. d} = {} \ dest_vec1 b \ dest_vec1 a \ dest_vec1 d < dest_vec1 c \ dest_vec1 b \ dest_vec1 c \ dest_vec1 d \ dest_vec1 a" "{a<.. {c<.. dest_vec1 b \ dest_vec1 a \ dest_vec1 d \ dest_vec1 c \ dest_vec1 b \ dest_vec1 c \ dest_vec1 d \ dest_vec1 a" - unfolding disjoint_interval and dest_vec1_def and dim1 by auto + unfolding disjoint_interval and dest_vec1_def ex_1 by auto lemma open_closed_interval_1: fixes a :: "real^1" shows "{a<.. dest_vec1 b ==> {a .. b} = {a<.. {a,b}" - unfolding expand_set_eq apply simp unfolding vector_less_def and vector_less_eq_def and dim1 and dest_vec1_eq[THEN sym] and dest_vec1_def by auto + unfolding expand_set_eq apply simp unfolding vector_less_def and vector_less_eq_def and all_1 and dest_vec1_eq[THEN sym] and dest_vec1_def by auto (* Some stuff for half-infinite intervals too; FIXME: notation? *) -lemma closed_interval_left: fixes b::"real^'n" - shows "closed {x::real^'n. \i \ dimset x. x$i \ b$i}" +lemma closed_interval_left: fixes b::"real^'n::finite" + shows "closed {x::real^'n. \i. x$i \ b$i}" proof- - { fix i assume i:"i\dimset b" - fix x::"real^'n" assume x:"\e>0. \x'\{x. \i\dimset b. x $ i \ b $ i}. x' \ x \ dist x' x < e" + { fix i + fix x::"real^'n" assume x:"\e>0. \x'\{x. \i. x $ i \ b $ i}. x' \ x \ dist x' x < e" { assume "x$i > b$i" - then obtain y where "y $ i \ b $ i" "y \ x" "dist y x < x$i - b$i" using x[THEN spec[where x="x$i - b$i"]] and i by (auto, erule_tac x=i in ballE)auto - hence False using component_le_norm[OF i, of "y - x"] unfolding dist_def and vector_minus_component[OF i] by auto } + then obtain y where "y $ i \ b $ i" "y \ x" "dist y x < x$i - b$i" using x[THEN spec[where x="x$i - b$i"]] by auto + hence False using component_le_norm[of "y - x" i] unfolding dist_def and vector_minus_component by auto } hence "x$i \ b$i" by(rule ccontr)auto } thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast qed -lemma closed_interval_right: fixes a::"real^'n" - shows "closed {x::real^'n. \i \ dimset x. a$i \ x$i}" +lemma closed_interval_right: fixes a::"real^'n::finite" + shows "closed {x::real^'n. \i. a$i \ x$i}" proof- - { fix i assume i:"i\dimset a" - fix x::"real^'n" assume x:"\e>0. \x'\{x. \i\dimset a. a $ i \ x $ i}. x' \ x \ dist x' x < e" + { fix i + fix x::"real^'n" assume x:"\e>0. \x'\{x. \i. a $ i \ x $ i}. x' \ x \ dist x' x < e" { assume "a$i > x$i" - then obtain y where "a $ i \ y $ i" "y \ x" "dist y x < a$i - x$i" using x[THEN spec[where x="a$i - x$i"]] and i by(auto, erule_tac x=i in ballE)auto - hence False using component_le_norm[OF i, of "y - x"] unfolding dist_def and vector_minus_component[OF i] by auto } + then obtain y where "a $ i \ y $ i" "y \ x" "dist y x < a$i - x$i" using x[THEN spec[where x="a$i - x$i"]] by auto + hence False using component_le_norm[of "y - x" i] unfolding dist_def and vector_minus_component by auto } hence "a$i \ x$i" by(rule ccontr)auto } thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast qed @@ -4768,13 +4755,13 @@ definition "is_interval s \ (\a\s. \b\s. \x. a \ x \ x \ b \ x \ s)" -lemma is_interval_interval: fixes a::"real^'n" shows +lemma is_interval_interval: fixes a::"real^'n::finite" shows "is_interval {a<.. real^'n" +lemma Lim_vec1_dot: fixes f :: "real^'m \ real^'n::finite" assumes "(f ---> l) net" shows "((vec1 o (\y. a \ (f y))) ---> vec1(a \ l)) net" proof(cases "a = vec 0") case True thus ?thesis using dot_lzero and Lim_const[of 0 net] unfolding vec1_vec and o_def by auto @@ -4821,14 +4808,14 @@ using continuous_at_vec1_dot by auto -lemma closed_halfspace_le: fixes a::"real^'n" +lemma closed_halfspace_le: fixes a::"real^'n::finite" shows "closed {x. a \ x \ b}" proof- have *:"{x \ UNIV. (vec1 \ op \ a) x \ vec1 ` {r. \x. a \ x = r \ r \ b}} = {x. a \ x \ b}" by auto - let ?T = "{x::real^1. (\i\dimset x. x$i \ (vec1 b)$i)}" + let ?T = "{x::real^1. (\i. x$i \ (vec1 b)$i)}" have "closed ?T" using closed_interval_left[of "vec1 b"] by simp - moreover have "vec1 ` {r. \x. a \ x = r \ r \ b} = range (vec1 \ op \ a) \ ?T" unfolding dim1 - unfolding image_def apply auto unfolding vec1_component[unfolded One_nat_def] by auto + moreover have "vec1 ` {r. \x. a \ x = r \ r \ b} = range (vec1 \ op \ a) \ ?T" unfolding all_1 + unfolding image_def by auto ultimately have "\T. closed T \ vec1 ` {r. \x. a \ x = r \ r \ b} = range (vec1 \ op \ a) \ T" by auto hence "closedin euclidean {x \ UNIV. (vec1 \ op \ a) x \ vec1 ` {r. \x. a \ x = r \ r \ b}}" using continuous_on_vec1_dot[of UNIV a, unfolded continuous_on_closed subtopology_UNIV] unfolding closedin_closed @@ -4846,11 +4833,11 @@ qed lemma closed_halfspace_component_le: - assumes "i \ {1 .. dimindex (UNIV::'n set)}" shows "closed {x::real^'n. x$i \ a}" + shows "closed {x::real^'n::finite. x$i \ a}" using closed_halfspace_le[of "(basis i)::real^'n" a] unfolding dot_basis[OF assms] by auto lemma closed_halfspace_component_ge: - assumes "i \ {1 .. dimindex (UNIV::'n set)}" shows "closed {x::real^'n. x$i \ a}" + shows "closed {x::real^'n::finite. x$i \ a}" using closed_halfspace_ge[of a "(basis i)::real^'n"] unfolding dot_basis[OF assms] by auto text{* Openness of halfspaces. *} @@ -4868,48 +4855,45 @@ qed lemma open_halfspace_component_lt: - assumes "i \ {1 .. dimindex(UNIV::'n set)}" shows "open {x::real^'n. x$i < a}" + shows "open {x::real^'n::finite. x$i < a}" using open_halfspace_lt[of "(basis i)::real^'n" a] unfolding dot_basis[OF assms] by auto lemma open_halfspace_component_gt: - assumes "i \ {1 .. dimindex(UNIV::'n set)}" shows "open {x::real^'n. x$i > a}" + shows "open {x::real^'n::finite. x$i > a}" using open_halfspace_gt[of a "(basis i)::real^'n"] unfolding dot_basis[OF assms] by auto text{* This gives a simple derivation of limit component bounds. *} -lemma Lim_component_le: fixes f :: "'a \ real^'n" +lemma Lim_component_le: fixes f :: "'a \ real^'n::finite" assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. f(x)$i \ b) net" - and i:"i\ {1 .. dimindex(UNIV::'n set)}" shows "l$i \ b" proof- - { fix x have "x \ {x::real^'n. basis i \ x \ b} \ x$i \ b" unfolding dot_basis[OF i] by auto } note * = this + { fix x have "x \ {x::real^'n. basis i \ x \ b} \ x$i \ b" unfolding dot_basis by auto } note * = this show ?thesis using Lim_in_closed_set[of "{x. basis i \ x \ b}" f net l] unfolding * using closed_halfspace_le[of "(basis i)::real^'n" b] and assms(1,2,3) by auto qed -lemma Lim_component_ge: fixes f :: "'a \ real^'n" +lemma Lim_component_ge: fixes f :: "'a \ real^'n::finite" assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. b \ (f x)$i) net" - and i:"i\ {1 .. dimindex(UNIV::'n set)}" shows "b \ l$i" proof- - { fix x have "x \ {x::real^'n. basis i \ x \ b} \ x$i \ b" unfolding dot_basis[OF i] by auto } note * = this + { fix x have "x \ {x::real^'n. basis i \ x \ b} \ x$i \ b" unfolding dot_basis by auto } note * = this show ?thesis using Lim_in_closed_set[of "{x. basis i \ x \ b}" f net l] unfolding * using closed_halfspace_ge[of b "(basis i)::real^'n"] and assms(1,2,3) by auto qed -lemma Lim_component_eq: fixes f :: "'a \ real^'n" +lemma Lim_component_eq: fixes f :: "'a \ real^'n::finite" assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\x. f(x)$i = b) net" - and i:"i\ {1 .. dimindex(UNIV::'n set)}" shows "l$i = b" - using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] using i by auto + using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto lemma Lim_drop_le: fixes f :: "'a \ real^1" shows "(f ---> l) net \ ~(trivial_limit net) \ eventually (\x. dest_vec1 (f x) \ b) net ==> dest_vec1 l \ b" - using Lim_component_le[of f l net 1 b] unfolding dest_vec1_def and dim1 by auto + using Lim_component_le[of f l net 1 b] unfolding dest_vec1_def by auto lemma Lim_drop_ge: fixes f :: "'a \ real^1" shows "(f ---> l) net \ ~(trivial_limit net) \ eventually (\x. b \ dest_vec1 (f x)) net ==> b \ dest_vec1 l" - using Lim_component_ge[of f l net b 1] unfolding dest_vec1_def and dim1 by auto + using Lim_component_ge[of f l net b 1] unfolding dest_vec1_def by auto text{* Limits relative to a union. *} @@ -4926,7 +4910,7 @@ using assms unfolding continuous_on unfolding Lim_within_union unfolding Lim unfolding trivial_limit_within unfolding closed_limpt by auto -lemma continuous_on_cases: fixes g :: "real^'m \ real ^'n" +lemma continuous_on_cases: fixes g :: "real^'m::finite \ real ^'n::finite" assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g" "\x. (x\s \ \ P x) \ (x \ t \ P x) \ f x = g x" shows "continuous_on (s \ t) (\x. if P x then f x else g x)" @@ -4943,7 +4927,7 @@ text{* Some more convenient intermediate-value theorem formulations. *} -lemma connected_ivt_hyperplane: fixes y :: "real^'n" +lemma connected_ivt_hyperplane: fixes y :: "real^'n::finite" assumes "connected s" "x \ s" "y \ s" "a \ x \ b" "b \ a \ y" shows "\z \ s. a \ z = b" proof(rule ccontr) @@ -4956,8 +4940,8 @@ ultimately show False using assms(1)[unfolded connected_def not_ex, THEN spec[where x="?A"], THEN spec[where x="?B"]] and assms(2-5) by auto qed -lemma connected_ivt_component: fixes x::"real^'n" shows - "connected s \ x \ s \ y \ s \ k \ dimset x \ x$k \ a \ a \ y$k \ (\z\s. z$k = a)" +lemma connected_ivt_component: fixes x::"real^'n::finite" shows + "connected s \ x \ s \ y \ s \ x$k \ a \ a \ y$k \ (\z\s. z$k = a)" using connected_ivt_hyperplane[of s x y "(basis k)::real^'n" a] by (auto simp add: dot_basis) text{* Also more convenient formulations of monotone convergence. *} @@ -4982,7 +4966,7 @@ (\x\s. (g(f x) = x)) \ (f ` s = t) \ continuous_on s f \ (\y\t. (f(g y) = y)) \ (g ` t = s) \ continuous_on t g" -definition homeomorphic :: "((real^'a) set) \ ((real^'b) set) \ bool" (infixr "homeomorphic" 60) where +definition homeomorphic :: "((real^'a::finite) set) \ ((real^'b::finite) set) \ bool" (infixr "homeomorphic" 60) where homeomorphic_def: "s homeomorphic t \ (\f g. homeomorphism s t f g)" lemma homeomorphic_refl: "s homeomorphic s" @@ -5103,7 +5087,7 @@ using homeomorphic_translation[of "(\x. c *s x) ` s" a] unfolding * by auto qed -lemma homeomorphic_balls: fixes a b ::"real^'a" +lemma homeomorphic_balls: fixes a b ::"real^'a::finite" assumes "0 < d" "0 < e" shows "(ball a d) homeomorphic (ball b e)" (is ?th) "(cball a d) homeomorphic (cball b e)" (is ?cth) @@ -5173,7 +5157,7 @@ lemma dist_0_norm:"dist 0 x = norm x" unfolding dist_def by(auto simp add: norm_minus_cancel) -lemma injective_imp_isometric: fixes f::"real^'m \ real^'n" +lemma injective_imp_isometric: fixes f::"real^'m::finite \ real^'n::finite" assumes s:"closed s" "subspace s" and f:"linear f" "\x\s. (f x = 0) \ (x = 0)" shows "\e>0. \x\s. norm (f x) \ e * norm(x)" proof(cases "s \ {0::real^'m}") @@ -5235,24 +5219,23 @@ subsection{* Some properties of a canonical subspace. *} lemma subspace_substandard: - "subspace {x::real^'n. (\i \ dimset x. d < i \ x$i = 0)}" + "subspace {x::real^'n. (\i. P i \ x$i = 0)}" unfolding subspace_def by(auto simp add: vector_add_component vector_smult_component elim!: ballE) lemma closed_substandard: - "closed {x::real^'n. \i \ dimset x. d < i --> x$i = 0}" (is "closed ?A") + "closed {x::real^'n::finite. \i. P i --> x$i = 0}" (is "closed ?A") proof- - let ?D = "{Suc d..dimindex(UNIV::('n set))}" + let ?D = "{i. P i}" let ?Bs = "{{x::real^'n. basis i \ x = 0}| i. i \ ?D}" { fix x { assume "x\?A" - hence x:"\i\?D. d < i \ x $ i = 0" by auto + hence x:"\i\?D. x $ i = 0" by auto hence "x\ \ ?Bs" by(auto simp add: dot_basis x) } moreover { assume x:"x\\?Bs" - { fix i assume i:"i\dimset x" and "d < i" - hence "i \ ?D" by auto + { fix i assume i:"i \ ?D" then obtain B where BB:"B \ ?Bs" and B:"B = {x::real^'n. basis i \ x = 0}" by auto - hence "x $ i = 0" unfolding B unfolding dot_basis[OF i] using x by auto } + hence "x $ i = 0" unfolding B using x unfolding dot_basis by auto } hence "x\?A" by auto } ultimately have "x\?A \ x\ \?Bs" by auto } hence "?A = \ ?Bs" by auto @@ -5260,40 +5243,40 @@ qed lemma dim_substandard: - assumes "d \ dimindex(UNIV::'n set)" - shows "dim {x::real^'n. \i \ dimset x. d < i --> x$i = 0} = d" (is "dim ?A = d") + shows "dim {x::real^'n::finite. \i. i \ d \ x$i = 0} = card d" (is "dim ?A = _") proof- - let ?D = "{1..dimindex (UNIV::'n set)}" - let ?B = "(basis::nat\real^'n) ` {1..d}" - - let ?bas = "basis::nat \ real^'n" - - have "?B \ ?A" by (auto simp add: basis_component) + let ?D = "UNIV::'n set" + let ?B = "(basis::'n\real^'n) ` d" + + let ?bas = "basis::'n \ real^'n" + + have "?B \ ?A" by auto moreover { fix x::"real^'n" assume "x\?A" - hence "x\ span ?B" + with finite[of d] + have "x\ span ?B" proof(induct d arbitrary: x) - case 0 hence "x=0" unfolding Cart_eq by auto + case empty hence "x=0" unfolding Cart_eq by auto thus ?case using subspace_0[OF subspace_span[of "{}"]] by auto next - case (Suc n) - hence *:"\i\?D. Suc n < i \ x $ i = 0" by auto - have **:"{1..n} \ {1..Suc n}" by auto - def y \ "x - x$(Suc n) *s basis (Suc n)" - have y:"x = y + (x$Suc n) *s basis (Suc n)" unfolding y_def by auto - { fix i assume i:"i\?D" and i':"n < i" - hence "y $ i = 0" unfolding y_def unfolding vector_minus_component[OF i] - and vector_smult_component[OF i] and basis_component[OF i] using i' - using *[THEN bspec[where x=i]] by auto } - hence "y \ span (basis ` {1..Suc n})" using Suc(1)[of y] - using span_mono[of "?bas ` {1..n}" "?bas ` {1..Suc n}"] + case (insert k F) + hence *:"\i. i \ insert k F \ x $ i = 0" by auto + have **:"F \ insert k F" by auto + def y \ "x - x$k *s basis k" + have y:"x = y + (x$k) *s basis k" unfolding y_def by auto + { fix i assume i':"i \ F" + hence "y $ i = 0" unfolding y_def unfolding vector_minus_component + and vector_smult_component and basis_component + using *[THEN spec[where x=i]] by auto } + hence "y \ span (basis ` (insert k F))" using insert(3) + using span_mono[of "?bas ` F" "?bas ` (insert k F)"] using image_mono[OF **, of basis] by auto moreover - have "basis (Suc n) \ span (?bas ` {1..Suc n})" by(rule span_superset, auto) - hence "x$(Suc n) *s basis (Suc n) \ span (?bas ` {1..Suc n})" using span_mul by auto + have "basis k \ span (?bas ` (insert k F))" by(rule span_superset, auto) + hence "x$k *s basis k \ span (?bas ` (insert k F))" using span_mul by auto ultimately - have "y + x$(Suc n) *s basis (Suc n) \ span (?bas ` {1..Suc n})" + have "y + x$k *s basis k \ span (?bas ` (insert k F))" using span_add by auto thus ?case using y by auto qed @@ -5306,27 +5289,39 @@ hence "independent ?B" using independent_mono[OF independent_stdbasis, of ?B] and assms by auto moreover - have "{1..d} \ ?D" unfolding subset_eq using assms by auto - hence *:"inj_on (basis::nat\real^'n) {1..d}" using subset_inj_on[OF basis_inj, of "{1..d}"] using assms by auto - have "?B hassize d" unfolding hassize_def and card_image[OF *] by auto - - ultimately show ?thesis using dim_unique[of "basis ` {1..d}" ?A] by auto + have "d \ ?D" unfolding subset_eq using assms by auto + hence *:"inj_on (basis::'n\real^'n) d" using subset_inj_on[OF basis_inj, of "d"] by auto + have "?B hassize (card d)" unfolding hassize_def and card_image[OF *] by auto + + ultimately show ?thesis using dim_unique[of "basis ` d" ?A] by auto qed text{* Hence closure and completeness of all subspaces. *} -lemma closed_subspace: fixes s::"(real^'n) set" +lemma closed_subspace_lemma: "n \ card (UNIV::'n::finite set) \ \A::'n set. card A = n" +apply (induct n) +apply (rule_tac x="{}" in exI, simp) +apply clarsimp +apply (subgoal_tac "\x. x \ A") +apply (erule exE) +apply (rule_tac x="insert x A" in exI, simp) +apply (subgoal_tac "A \ UNIV", auto) +done + +lemma closed_subspace: fixes s::"(real^'n::finite) set" assumes "subspace s" shows "closed s" proof- - let ?t = "{x::real^'n. \i\{1..dimindex (UNIV :: 'n set)}. dim s x$i = 0}" - have "dim s \ dimindex (UNIV :: 'n set)" using dim_subset_univ by auto + have "dim s \ card (UNIV :: 'n set)" using dim_subset_univ by auto + then obtain d::"'n set" where t: "card d = dim s" + using closed_subspace_lemma by auto + let ?t = "{x::real^'n. \i. i \ d \ x$i = 0}" obtain f where f:"linear f" "f ` ?t = s" "inj_on f ?t" - using subspace_isomorphism[OF subspace_substandard[of "dim s"] assms] - using dim_substandard[OF dim_subset_univ[of s]] by auto + using subspace_isomorphism[OF subspace_substandard[of "\i. i \ d"] assms] + using dim_substandard[of d] and t by auto have "\x\?t. f x = 0 \ x = 0" using linear_0[OF f(1)] using f(3)[unfolded inj_on_def] by(erule_tac x=0 in ballE) auto - moreover have "closed ?t" using closed_substandard by auto - moreover have "subspace ?t" using subspace_substandard by auto + moreover have "closed ?t" using closed_substandard . + moreover have "subspace ?t" using subspace_substandard . ultimately show ?thesis using closed_injective_image_subspace[of ?t f] unfolding f(2) using f(1) by auto qed @@ -5400,13 +5395,14 @@ by metis lemma image_affinity_interval: fixes m::real + fixes a b c :: "real^'n::finite" shows "(\x. m *s x + c) ` {a .. b} = (if {a .. b} = {} then {} else (if 0 \ m then {m *s a + c .. m *s b + c} else {m *s b + c .. m *s a + c}))" proof(cases "m=0") { fix x assume "x \ c" "c \ x" - hence "x=c" unfolding vector_less_eq_def and Cart_eq by(auto elim!: ballE) } + hence "x=c" unfolding vector_less_eq_def and Cart_eq by (auto intro: order_antisym) } moreover case True moreover have "c \ {m *s a + c..m *s b + c}" unfolding True by(auto simp add: vector_less_eq_def) ultimately show ?thesis by auto @@ -5425,14 +5421,14 @@ unfolding image_iff Bex_def mem_interval vector_less_eq_def apply(auto simp add: vector_smult_component vector_add_component vector_minus_component vector_smult_assoc pth_3[symmetric] intro!: exI[where x="(1 / m) *s (y - c)"]) - by(auto elim!: ballE simp add: pos_le_divide_eq pos_divide_le_eq real_mult_commute) + by(auto simp add: pos_le_divide_eq pos_divide_le_eq real_mult_commute diff_le_iff) } moreover { fix y assume "m *s b + c \ y" "y \ m *s a + c" "m < 0" hence "y \ (\x. m *s x + c) ` {a..b}" unfolding image_iff Bex_def mem_interval vector_less_eq_def apply(auto simp add: vector_smult_component vector_add_component vector_minus_component vector_smult_assoc pth_3[symmetric] intro!: exI[where x="(1 / m) *s (y - c)"]) - by(auto elim!: ballE simp add: neg_le_divide_eq neg_divide_le_eq real_mult_commute) + by(auto simp add: neg_le_divide_eq neg_divide_le_eq real_mult_commute diff_le_iff) } ultimately show ?thesis using False by auto qed @@ -5569,7 +5565,7 @@ lemma edelstein_fix: assumes s:"compact s" "s \ {}" and gs:"(g ` s) \ s" and dist:"\x\s. \y\s. x \ y \ dist (g x) (g y) < dist x y" - shows "\! x::real^'a\s. g x = x" + shows "\! x::real^'a::finite\s. g x = x" proof(cases "\x\s. g x \ x") obtain x where "x\s" using s(2) by auto case False hence g:"\x\s. g x = x" by auto