# HG changeset patch # User huffman # Date 1313506577 25200 # Node ID 5f974bead4365a583087acc052b4b03904f133e8 # Parent 78e033e8ba050a80ddead30a371b599d043aa8db get Multivariate_Analysis/Determinants.thy compiled and working again diff -r 78e033e8ba05 -r 5f974bead436 src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Tue Aug 16 07:06:54 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Tue Aug 16 07:56:17 2011 -0700 @@ -5,7 +5,9 @@ header {* Traces, Determinant of square matrices and some properties *} theory Determinants -imports Euclidean_Space Permutations +imports + Cartesian_Euclidean_Space + "~~/src/HOL/Library/Permutations" begin subsection{* First some facts about products*} @@ -272,7 +274,7 @@ unfolding det_permute_rows[OF p, of ?At] det_transpose .. moreover have "?Ap = transpose (\ i. transpose A $ p i)" - by (simp add: transpose_def Cart_eq) + by (simp add: transpose_def vec_eq_iff) ultimately show ?thesis by simp qed @@ -287,7 +289,7 @@ 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 row_def swap_def) + from r have "A = ?A" by (simp add: vec_eq_iff 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] sign_swap_id ij th1) @@ -308,7 +310,7 @@ assumes r: "row i A = 0" shows "det A = 0" using r -apply (simp add: row_def det_def Cart_eq) +apply (simp add: row_def det_def vec_eq_iff) apply (rule setsum_0') apply (auto simp: sign_nz) done @@ -326,7 +328,7 @@ 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 Cart_lambda_beta setsum_addf[symmetric] +unfolding det_def vec_lambda_beta setsum_addf[symmetric] proof (rule setsum_cong2) let ?U = "UNIV :: 'n set" let ?pU = "{p. p permutes ?U}" @@ -366,7 +368,7 @@ 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 Cart_lambda_beta setsum_right_distrib +unfolding det_def vec_lambda_beta setsum_right_distrib proof (rule setsum_cong2) let ?U = "UNIV :: 'n set" let ?pU = "{p. p permutes ?U}" @@ -495,8 +497,8 @@ (* Multilinearity and the multiplication formula. *) (* ------------------------------------------------------------------------- *) -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 Cart_lambda_cong: "(\x. f x = g x) \ (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)" + apply (rule iffD1[OF vec_lambda_unique]) by vector lemma det_linear_row_setsum: assumes fS: "finite S" @@ -823,7 +825,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) / det A)" unfolding x[symmetric] - using d0 by (simp add: Cart_eq cramer_lemma field_simps)} + using d0 by (simp add: vec_eq_iff cramer_lemma field_simps)} with xe show ?thesis by auto qed @@ -877,9 +879,9 @@ 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] + from fd[rule_format, of "cart_basis i" "cart_basis j", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul] have "?A$i$j = ?m1 $ i $ j" - by (simp add: inner_vector_def matrix_matrix_mult_def columnvector_def rowvector_def basis_def th0 setsum_delta[OF fU] mat_def)} + by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def cart_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 @@ -967,8 +969,8 @@ shows "\g. orthogonal_transformation g \ (\x. norm x = 1 \ g x = f x)" proof- {fix x y x' y' x0 y0 x0' y0' :: "real ^'n" - assume H: "x = norm x *s x0" "y = norm y *s y0" - "x' = norm x *s x0'" "y' = norm y *s y0'" + assume H: "x = norm x *\<^sub>R x0" "y = norm y *\<^sub>R y0" + "x' = norm x *\<^sub>R x0'" "y' = norm y *\<^sub>R y0'" "norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1" "norm(x0' - y0') = norm(x0 - y0)" hence *:"x0 \ y0 = x0' \ y0' + y0' \ x0' - y0 \ x0 " by(simp add: norm_eq norm_eq_1 inner_simps) @@ -982,7 +984,7 @@ apply (simp add: inner_simps smult_conv_scaleR) unfolding * by (simp add: field_simps) } note th0 = this - let ?g = "\x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)" + let ?g = "\x. if x = 0 then 0 else norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)" {fix x:: "real ^'n" assume nx: "norm x = 1" have "?g x = f x" using nx by auto} hence thfg: "\x. norm x = 1 \ ?g x = f x" by blast @@ -1004,14 +1006,14 @@ by(simp add: field_simps)} moreover {assume z: "x \ 0" "y \ 0" - have th00: "x = norm x *s (inverse (norm x) *s x)" "y = norm y *s (inverse (norm y) *s y)" "norm x *s f ((inverse (norm x) *s x)) = norm x *s f (inverse (norm x) *s x)" - "norm y *s f (inverse (norm y) *s y) = norm y *s f (inverse (norm y) *s y)" - "norm (inverse (norm x) *s x) = 1" - "norm (f (inverse (norm x) *s x)) = 1" - "norm (inverse (norm y) *s y) = 1" - "norm (f (inverse (norm y) *s y)) = 1" - "norm (f (inverse (norm x) *s x) - f (inverse (norm y) *s y)) = - norm (inverse (norm x) *s x - inverse (norm y) *s y)" + have th00: "x = norm x *\<^sub>R (inverse (norm x) *\<^sub>R x)" "y = norm y *\<^sub>R (inverse (norm y) *\<^sub>R y)" "norm x *\<^sub>R f ((inverse (norm x) *\<^sub>R x)) = norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)" + "norm y *\<^sub>R f (inverse (norm y) *\<^sub>R y) = norm y *\<^sub>R f (inverse (norm y) *\<^sub>R y)" + "norm (inverse (norm x) *\<^sub>R x) = 1" + "norm (f (inverse (norm x) *\<^sub>R x)) = 1" + "norm (inverse (norm y) *\<^sub>R y) = 1" + "norm (f (inverse (norm y) *\<^sub>R y)) = 1" + "norm (f (inverse (norm x) *\<^sub>R x) - f (inverse (norm y) *\<^sub>R y)) = + norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)" using z by (auto simp add: vector_smult_assoc field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm]) from z th0[OF th00] have "dist (?g x) (?g y) = dist x y" diff -r 78e033e8ba05 -r 5f974bead436 src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy --- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy Tue Aug 16 07:06:54 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy Tue Aug 16 07:56:17 2011 -0700 @@ -1,5 +1,5 @@ theory Multivariate_Analysis -imports Fashoda Extended_Real_Limits +imports Fashoda Extended_Real_Limits Determinants begin end