src/HOL/Multivariate_Analysis/Determinants.thy

 
 lemma orthogonal_transformation: "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>(v::real ^_). norm (f v) = norm v)"
   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"
 
 lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n)  \<longleftrightarrow> transpose Q ** Q = mat 1"

       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]
       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
   {assume lf: "linear f" and om: "orthogonal_matrix ?mf"
     from lf om have ?lhs

     note th0 = this
     have "f v \<bullet> f w = c^2 * (v \<bullet> w)"
       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:
   "f (0:: real^'n) = (0:: real^'n) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y
         \<Longrightarrow> linear f"

   {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'"
     "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))
       apply (subst H(3))
       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"
     have "?g x = f x" using nx by auto}
   hence thfg: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x" by blast