--- a/src/HOL/Multivariate_Analysis/Determinants.thy Tue Mar 02 11:07:17 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Tue Mar 02 21:32:37 2010 +0100
@@ -837,7 +837,7 @@
unfolding orthogonal_transformation_def
apply auto
apply (erule_tac x=v in allE)+
- apply (simp add: real_vector_norm_def)
+ apply (simp add: norm_eq_sqrt_inner)
by (simp add: dot_norm linear_add[symmetric])
definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
@@ -879,7 +879,7 @@
by simp_all
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: dot_def matrix_matrix_mult_def columnvector_def rowvector_def basis_def th0 setsum_delta[OF fU] mat_def)}
+ by (simp add: inner_vector_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
@@ -929,8 +929,7 @@
unfolding dot_norm_neg dist_norm[symmetric]
unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
note fc = this
- show ?thesis unfolding linear_def vector_eq
- by (simp add: dot_lmult dot_ladd dot_rmult dot_radd fc ring_simps)
+ show ?thesis unfolding linear_def vector_eq smult_conv_scaleR by (simp add: inner_simps fc ring_simps)
qed
lemma isometry_linear:
@@ -972,7 +971,7 @@
"x' = norm x *s x0'" "y' = norm y *s 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)
have "norm(x' - y') = norm(x - y)"
apply (subst H(1))
apply (subst H(2))
@@ -980,9 +979,8 @@
apply (subst H(4))
using H(5-9)
apply (simp add: norm_eq norm_eq_1)
- apply (simp add: dot_lsub dot_rsub dot_lmult dot_rmult)
- apply (simp add: ring_simps)
- by (simp only: right_distrib[symmetric])}
+ apply (simp add: inner_simps smult_conv_scaleR) unfolding *
+ by (simp add: ring_simps) }
note th0 = this
let ?g = "\<lambda>x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)"
{fix x:: "real ^'n" assume nx: "norm x = 1"