--- 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 (\<chi> 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 = "\<chi> 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((\<chi> i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) =
det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) +
det((\<chi> 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((\<chi> i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) =
c* det((\<chi> 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: "(\<And>x. f x = g x) \<Longrightarrow> (Cart_lambda f::'a^'n) = (Cart_lambda g :: 'a^'n)"
- apply (rule iffD1[OF Cart_lambda_unique]) by vector
+lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (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 = (\<chi> k. det(\<chi> 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: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)"
"\<And>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 "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> 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 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0' - y0 \<bullet> 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 = "\<lambda>x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)"
+ let ?g = "\<lambda>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: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x" by blast
@@ -1004,14 +1006,14 @@
by(simp add: field_simps)}
moreover
{assume z: "x \<noteq> 0" "y \<noteq> 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"
--- 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