author huffman Thu, 19 Mar 2009 08:13:10 -0700 changeset 30598 eb827cd69fd3 parent 30597 88c29b3b1fa2 child 30599 4216e9c70cfe child 30604 2a9911f4b0a3
add lemma det_diagonal; remove wellorder requirement on several lemmas
```--- a/src/HOL/Library/Determinants.thy	Thu Mar 19 14:08:55 2009 +0100
+++ b/src/HOL/Library/Determinants.thy	Thu Mar 19 08:13:10 2009 -0700
@@ -194,8 +194,28 @@
unfolding det_def by (simp add: sign_id)
qed

-(* FIXME: get rid of wellorder requirement *)
-lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n::{finite,wellorder}) = 1"
+lemma det_diagonal:
+  fixes A :: "'a::comm_ring_1^'n^'n::finite"
+  assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A\$i\$j = 0"
+  shows "det A = setprod (\<lambda>i. A\$i\$i) (UNIV::'n set)"
+proof-
+  let ?U = "UNIV:: 'n set"
+  let ?PU = "{p. p permutes ?U}"
+  let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>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} \<subseteq> ?PU" by (auto simp add: permutes_id)
+  {fix p assume p: "p \<in> ?PU - {id}"
+    then have "p \<noteq> id" by simp
+    then obtain i where i: "p i \<noteq> i" unfolding expand_fun_eq by auto
+    from ld [OF i [symmetric]] have ex:"\<exists>i \<in> ?U. A\$i\$p i = 0" by blast
+    from setprod_zero [OF fU ex] have "?pp p = 0" by simp}
+  then have p0: "\<forall>p \<in> ?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::finite) = 1"
proof-
let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n"
let ?U = "UNIV :: 'n set"
@@ -204,9 +224,9 @@
have "?f i i = 1" using i by (vector mat_def)}
hence th: "setprod (\<lambda>i. ?f i i) ?U = setprod (\<lambda>x. 1) ?U"
by (auto intro: setprod_cong)
-  {fix i j assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i < j"
+  {fix i j assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i \<noteq> j"
have "?f i j = 0" using i j ij by (vector mat_def) }
-  then have "det ?A = setprod (\<lambda>i. ?f i i) ?U" using det_lowerdiagonal
+  then have "det ?A = setprod (\<lambda>i. ?f i i) ?U" using det_diagonal
by blast
also have "\<dots> = 1" unfolding th setprod_1 ..
finally show ?thesis .
@@ -692,9 +712,8 @@
shows "invertible A \<longleftrightarrow> (\<exists>(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::{finite,wellorder}"
+  fixes A::"real ^'n^'n::finite"
shows "invertible A \<longleftrightarrow> det A \<noteq> 0"
proof-
{assume "invertible A"
@@ -787,17 +806,15 @@
let ?U = "UNIV :: 'n set"
have stupid: "\<And>c. setsum (\<lambda>i. c i *s row i (transp A)) ?U = setsum (\<lambda>i. c i *s column i A) ?U"
by (auto simp add: row_transp intro: setsum_cong2)
-  show ?thesis
-  unfolding matrix_mult_vsum
+  show ?thesis  unfolding matrix_mult_vsum
unfolding cramer_lemma_transp[of k x "transp A", unfolded det_transp, symmetric]
unfolding stupid[of "\<lambda>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::{finite,wellorder}"
+  fixes A ::"real^'n^'n::finite"
assumes d0: "det A \<noteq> 0"
shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b\$i else A\$i\$j :: real^'n^'n) / det A)"
proof-
@@ -878,9 +895,8 @@
ultimately show ?thesis by blast
qed

-(* FIXME: get rid of wellorder requirement *)
lemma det_orthogonal_matrix:
-  fixes Q:: "'a::ordered_idom^'n^'n::{finite,wellorder}"
+  fixes Q:: "'a::ordered_idom^'n^'n::finite"
assumes oQ: "orthogonal_matrix Q"
shows "det Q = 1 \<or> det Q = - 1"
proof-
@@ -1020,9 +1036,8 @@
definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"

-(* FIXME: get rid of wellorder requirement *)
lemma orthogonal_rotation_or_rotoinversion:
-  fixes Q :: "'a::ordered_idom^'n^'n::{finite,wellorder}"
+  fixes Q :: "'a::ordered_idom^'n^'n::finite"
shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q"
by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)
(* ------------------------------------------------------------------------- *)```