--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Apr 29 14:32:24 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Apr 29 15:24:22 2010 -0700
@@ -1147,6 +1147,21 @@
definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
+lemma adjoint_unique:
+ assumes "\<forall>x y. inner (f x) y = inner x (g y)"
+ shows "adjoint f = g"
+unfolding adjoint_def
+proof (rule some_equality)
+ show "\<forall>x y. inner (f x) y = inner x (g y)" using assms .
+next
+ fix h assume "\<forall>x y. inner (f x) y = inner x (h y)"
+ hence "\<forall>x y. inner x (g y) = inner x (h y)" using assms by simp
+ hence "\<forall>x y. inner x (g y - h y) = 0" by (simp add: inner_diff_right)
+ hence "\<forall>y. inner (g y - h y) (g y - h y) = 0" by simp
+ hence "\<forall>y. h y = g y" by simp
+ thus "h = g" by (simp add: ext)
+qed
+
lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis
text {* TODO: The following lemmas about adjoints should hold for any
@@ -1206,16 +1221,7 @@
fixes f:: "real ^'n \<Rightarrow> real ^'m"
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:: "real ^'n \<Rightarrow> real ^'m"
- assumes lf: "linear f" and u: "\<forall>x y. f' x \<bullet> y = x \<bullet> f y"
- shows "f' = adjoint f"
- apply (rule ext)
- using u
- by (simp add: vector_eq_rdot[where 'a="real^'n", symmetric] adjoint_clauses[OF lf])
+ by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
subsection {* Matrix operations *}
@@ -1383,8 +1389,7 @@
by (simp add: matrix_vector_mult_def transpose_def Cart_eq mult_commute)
lemma adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
- apply (rule adjoint_unique[symmetric])
- apply (rule matrix_vector_mul_linear)
+ apply (rule adjoint_unique)
apply (simp add: transpose_def inner_vector_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib)
apply (subst setsum_commute)
apply (auto simp add: mult_ac)