# HG changeset patch
# User himmelma
# Date 1267561957 -3600
# Node ID 8f97d8caabfd1e80512d649077669ac57296e274
# Parent  7b1179be2ac51bdcd08705cd7b97c6303b1a6bc2
replaced \<bullet> with inner

diff -r 7b1179be2ac5 -r 8f97d8caabfd src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Mar 02 11:07:17 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Mar 02 21:32:37 2010 +0100
@@ -15,8 +15,6 @@
 
 declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp]
 declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp]
-declare dot_ladd[simp] dot_radd[simp] dot_lsub[simp] dot_rsub[simp]
-declare dot_lmult[simp] dot_rmult[simp] dot_lneg[simp] dot_rneg[simp]
 declare UNIV_1[simp]
 
 (*lemma dim1in[intro]:"Suc 0 \<in> {1::nat .. CARD(1)}" by auto*)
@@ -1717,7 +1715,7 @@
     using norm_basis and dimindex_ge_1 by auto
   thus ?thesis apply(rule_tac x="basis a" in exI, rule_tac x=1 in exI) using True by auto
 next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms]
-    apply - apply(erule exE)+ unfolding dot_rzero apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
+    apply - apply(erule exE)+ unfolding inner.zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
 
 subsection {* Now set-to-set for closed/compact sets. *}
 
diff -r 7b1179be2ac5 -r 8f97d8caabfd src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Mar 02 11:07:17 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Mar 02 21:32:37 2010 +0100
@@ -12,6 +12,9 @@
 (* Because I do not want to type this all the time *)
 lemmas linear_linear = linear_conv_bounded_linear[THEN sym]
 
+(** move this **)
+declare norm_vec1[simp]
+
 subsection {* Derivatives *}
 
 text {* The definition is slightly tricky since we make it work over
@@ -612,7 +615,7 @@
     finally have "\<bar>(f (x + c *\<^sub>R basis j) - f x - D *v (c *\<^sub>R basis j)) $ k\<bar> \<le> \<bar>D $ k $ j\<bar> / 2 * \<bar>c\<bar>" by simp
     hence "\<bar>f (x + c *\<^sub>R basis j) $ k - f x $ k - c * D $ k $ j\<bar> \<le> \<bar>D $ k $ j\<bar> / 2 * \<bar>c\<bar>"
       unfolding vector_component_simps matrix_vector_mul_component unfolding smult_conv_scaleR[symmetric] 
-      unfolding dot_rmult dot_basis unfolding smult_conv_scaleR by simp  } note * = this
+      unfolding inner_simps dot_basis smult_conv_scaleR by simp  } note * = this
   have "x + d *\<^sub>R basis j \<in> ball x e" "x - d *\<^sub>R basis j \<in> ball x e"
     unfolding mem_ball vector_dist_norm using norm_basis[of j] d by auto
   hence **:"((f (x - d *\<^sub>R basis j))$k \<le> (f x)$k \<and> (f (x + d *\<^sub>R basis j))$k \<le> (f x)$k) \<or>
@@ -702,20 +705,17 @@
 
 subsection {* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *}
 
-lemma inner_eq_dot: fixes a::"real^'n"
-  shows "a \<bullet> b = inner a b" unfolding inner_vector_def dot_def by auto
-
 lemma mvt_general: fixes f::"real\<Rightarrow>real^'n"
   assumes "a<b" "continuous_on {a..b} f" "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
   shows "\<exists>x\<in>{a<..<b}. norm(f b - f a) \<le> norm(f'(x) (b - a))" proof-
   have "\<exists>x\<in>{a<..<b}. (op \<bullet> (f b - f a) \<circ> f) b - (op \<bullet> (f b - f a) \<circ> f) a = (f b - f a) \<bullet> f' x (b - a)"
-    apply(rule mvt) apply(rule assms(1))unfolding inner_eq_dot apply(rule continuous_on_inner continuous_on_intros assms(2))+ 
+    apply(rule mvt) apply(rule assms(1)) apply(rule continuous_on_inner continuous_on_intros assms(2))+ 
     unfolding o_def apply(rule,rule has_derivative_lift_dot) using assms(3) by auto
   then guess x .. note x=this
   show ?thesis proof(cases "f a = f b")
     case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:class_semiring.semiring_rules)
-    also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding norm_pow_2 ..
-    also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x by auto
+    also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
+    also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by auto
     also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz)
     finally show ?thesis using False x(1) by(auto simp add: real_mult_left_cancel) next
     case True thus ?thesis using assms(1) apply(rule_tac x="(a + b) /2" in bexI) by auto qed qed
@@ -751,9 +751,6 @@
   also have "\<dots> \<le> B * norm(y - x)" apply(rule **) using * and u by auto
   finally show ?thesis by(auto simp add:norm_minus_commute) qed 
 
-(** move this **)
-declare norm_vec1[simp]
-
 lemma onorm_vec1: fixes f::"real \<Rightarrow> real"
   shows "onorm (\<lambda>x. vec1 (f (dest_vec1 x))) = onorm f" proof-
   have "\<forall>x::real^1. norm x = 1 \<longleftrightarrow> x\<in>{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 by(auto simp add:Cart_eq)
diff -r 7b1179be2ac5 -r 8f97d8caabfd src/HOL/Multivariate_Analysis/Determinants.thy
--- 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"
diff -r 7b1179be2ac5 -r 8f97d8caabfd src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Mar 02 11:07:17 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Mar 02 21:32:37 2010 +0100
@@ -148,25 +148,11 @@
 
 definition "vec x = (\<chi> i. x)"
 
-text{* Dot products. *}
-
-definition dot :: "'a::{comm_monoid_add, times} ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" (infix "\<bullet>" 70) where
-  "x \<bullet> y = setsum (\<lambda>i. x$i * y$i) UNIV"
-
-lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \<bullet> y = (x$1) * (y$1)"
-  by (simp add: dot_def setsum_1)
-
-lemma dot_2[simp]: "(x::'a::{comm_monoid_add, times}^2) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2)"
-  by (simp add: dot_def setsum_2)
-
-lemma dot_3[simp]: "(x::'a::{comm_monoid_add, times}^3) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2) + (x$3) * (y$3)"
-  by (simp add: dot_def setsum_3)
-
 subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}
 
 method_setup vector = {*
 let
-  val ss1 = HOL_basic_ss addsimps [@{thm dot_def}, @{thm setsum_addf} RS sym,
+  val ss1 = HOL_basic_ss addsimps [@{thm setsum_addf} RS sym,
   @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib},
   @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym]
   val ss2 = @{simpset} addsimps
@@ -190,8 +176,6 @@
 lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def)
 lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def)
 
-
-
 text{* Obvious "component-pushing". *}
 
 lemma vec_component [simp]: "vec x $ i = x"
@@ -816,6 +800,8 @@
 
 subsection {* Inner products *}
 
+abbreviation inner_bullet (infix "\<bullet>" 70)  where "x \<bullet> y \<equiv> inner x y"
+
 instantiation cart :: (real_inner, finite) real_inner
 begin
 
@@ -846,27 +832,6 @@
 
 end
 
-subsection{* Properties of the dot product.  *}
-
-lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x"
-  by (vector mult_commute)
-lemma dot_ladd: "((x::'a::ring ^ 'n) + y) \<bullet> z = (x \<bullet> z) + (y \<bullet> z)"
-  by (vector ring_simps)
-lemma dot_radd: "x \<bullet> (y + (z::'a::ring ^ 'n)) = (x \<bullet> y) + (x \<bullet> z)"
-  by (vector ring_simps)
-lemma dot_lsub: "((x::'a::ring ^ 'n) - y) \<bullet> z = (x \<bullet> z) - (y \<bullet> z)"
-  by (vector ring_simps)
-lemma dot_rsub: "(x::'a::ring ^ 'n) \<bullet> (y - z) = (x \<bullet> y) - (x \<bullet> z)"
-  by (vector ring_simps)
-lemma dot_lmult: "(c *s x) \<bullet> y = (c::'a::ring) * (x \<bullet> y)" by (vector ring_simps)
-lemma dot_rmult: "x \<bullet> (c *s y) = (c::'a::comm_ring) * (x \<bullet> y)" by (vector ring_simps)
-lemma dot_lneg: "(-x) \<bullet> (y::'a::ring ^ 'n) = -(x \<bullet> y)" by vector
-lemma dot_rneg: "(x::'a::ring ^ 'n) \<bullet> (-y) = -(x \<bullet> y)" by vector
-lemma dot_lzero[simp]: "0 \<bullet> x = (0::'a::{comm_monoid_add, mult_zero})" by vector
-lemma dot_rzero[simp]: "x \<bullet> 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector
-lemma dot_pos_le[simp]: "(0::'a\<Colon>linordered_ring_strict) <= x \<bullet> x"
-  by (simp add: dot_def setsum_nonneg)
-
 lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\<forall>x \<in> F. f x \<ge> (0 ::'a::ordered_ab_group_add)" shows "setsum f F = 0 \<longleftrightarrow> (ALL x:F. f x = 0)"
 using fS fp setsum_nonneg[OF fp]
 proof (induct set: finite)
@@ -880,12 +845,6 @@
   show ?case by (simp add: h)
 qed
 
-lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{linordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0"
-  by (simp add: dot_def setsum_squares_eq_0_iff Cart_eq)
-
-lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{linordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]
-  by (auto simp add: le_less)
-
 subsection{* The collapse of the general concepts to dimension one. *}
 
 lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
@@ -1019,12 +978,8 @@
 lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x"
   by (simp add: norm_vector_def vector_component setL2_right_distrib
            abs_mult cong: strong_setL2_cong)
-lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))"
-  by (simp add: norm_vector_def dot_def setL2_def power2_eq_square)
-lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)"
-  by (simp add: norm_vector_def setL2_def dot_def power2_eq_square)
-lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
-  by (simp add: real_vector_norm_def)
+lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
+  by (simp add: norm_vector_def setL2_def power2_eq_square)
 lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
 lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
   by vector
@@ -1036,34 +991,17 @@
   by (metis vector_mul_lcancel)
 lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
   by (metis vector_mul_rcancel)
+
 lemma norm_cauchy_schwarz:
   fixes x y :: "real ^ 'n"
-  shows "x \<bullet> y <= norm x * norm y"
-proof-
-  {assume "norm x = 0"
-    hence ?thesis by (simp add: dot_lzero dot_rzero)}
-  moreover
-  {assume "norm y = 0"
-    hence ?thesis by (simp add: dot_lzero dot_rzero)}
-  moreover
-  {assume h: "norm x \<noteq> 0" "norm y \<noteq> 0"
-    let ?z = "norm y *s x - norm x *s y"
-    from h have p: "norm x * norm y > 0" by (metis norm_ge_zero le_less zero_compare_simps)
-    from dot_pos_le[of ?z]
-    have "(norm x * norm y) * (x \<bullet> y) \<le> norm x ^2 * norm y ^2"
-      apply (simp add: dot_rsub dot_lsub dot_lmult dot_rmult ring_simps)
-      by (simp add: norm_pow_2[symmetric] power2_eq_square dot_sym)
-    hence "x\<bullet>y \<le> (norm x ^2 * norm y ^2) / (norm x * norm y)" using p
-      by (simp add: field_simps)
-    hence ?thesis using h by (simp add: power2_eq_square)}
-  ultimately show ?thesis by metis
-qed
+  shows "inner x y <= norm x * norm y"
+  using Cauchy_Schwarz_ineq2[of x y] by auto
 
 lemma norm_cauchy_schwarz_abs:
   fixes x y :: "real ^ 'n"
-  shows "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y"
+  shows "\<bar>inner x y\<bar> \<le> norm x * norm y"
   using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"]
-  by (simp add: real_abs_def dot_rneg)
+  by (simp add: real_abs_def)
 
 lemma norm_triangle_sub:
   fixes x y :: "'a::real_normed_vector"
@@ -1089,21 +1027,21 @@
 lemma real_abs_sub_norm: "\<bar>norm (x::real ^ 'n) - norm y\<bar> <= norm(x - y)"
   by (rule norm_triangle_ineq3)
 lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
-  by (simp add: real_vector_norm_def)
+  by (simp add: norm_eq_sqrt_inner) 
 lemma norm_lt: "norm(x::real ^ 'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
-  by (simp add: real_vector_norm_def)
-lemma norm_eq: "norm(x::real ^ 'n) = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
-  by (simp add: order_eq_iff norm_le)
+  by (simp add: norm_eq_sqrt_inner)
+lemma norm_eq: "norm(x::real ^ 'n) = norm (y::real ^ 'n) \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
+  apply(subst order_eq_iff) unfolding norm_le by auto
 lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \<longleftrightarrow> x \<bullet> x = 1"
-  by (simp add: real_vector_norm_def)
+  unfolding norm_eq_sqrt_inner by auto
 
 text{* Squaring equations and inequalities involving norms.  *}
 
 lemma dot_square_norm: "x \<bullet> x = norm(x)^2"
-  by (simp add: real_vector_norm_def)
+  by (simp add: norm_eq_sqrt_inner)
 
 lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
-  by (auto simp add: real_vector_norm_def)
+  by (auto simp add: norm_eq_sqrt_inner)
 
 lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
 proof-
@@ -1131,12 +1069,14 @@
 
 text{* Dot product in terms of the norm rather than conversely. *}
 
+lemmas inner_simps = inner.add_left inner.add_right inner.diff_right inner.diff_left 
+inner.scaleR_left inner.scaleR_right
+
 lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2"
-  by (simp add: norm_pow_2 dot_ladd dot_radd dot_sym)
+  unfolding power2_norm_eq_inner inner_simps inner_commute by auto 
 
 lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2"
-  by (simp add: norm_pow_2 dot_ladd dot_radd dot_lsub dot_rsub dot_sym)
-
+  unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:group_simps)
 
 text{* Equality of vectors in terms of @{term "op \<bullet>"} products.    *}
 
@@ -1145,14 +1085,12 @@
   assume "?lhs" then show ?rhs by simp
 next
   assume ?rhs
-  then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y\<bullet> y = 0" by simp
-  hence "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0"
-    by (simp add: dot_rsub dot_lsub dot_sym)
-  then have "(x - y) \<bullet> (x - y) = 0" by (simp add: ring_simps dot_lsub dot_rsub)
-  then show "x = y" by (simp add: dot_eq_0)
+  then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y \<bullet> y = 0" by simp
+  hence "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0" by (simp add: inner_simps inner_commute)
+  then have "(x - y) \<bullet> (x - y) = 0" by (simp add: ring_simps inner_simps inner_commute)
+  then show "x = y" by (simp)
 qed
 
-
 subsection{* General linear decision procedure for normed spaces. *}
 
 lemma norm_cmul_rule_thm:
@@ -1481,15 +1419,14 @@
   finally show ?thesis .
 qed
 
-lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{comm_ring}^'n) = setsum (\<lambda>x. f x \<bullet> y) S "
-  by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd dot_radd)
-
-lemma dot_rsum: "finite S \<Longrightarrow> (y::'a::{comm_ring}^'n) \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
-  by (induct rule: finite_induct, auto simp add: dot_rzero dot_radd)
+lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{real_inner}^'n) = setsum (\<lambda>x. f x \<bullet> y) S "
+  apply(induct rule: finite_induct) by(auto simp add: inner_simps)
+
+lemma dot_rsum: "finite S \<Longrightarrow> (y::'a::{real_inner}^'n) \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
+  apply(induct rule: finite_induct) by(auto simp add: inner_simps)
 
 subsection{* Basis vectors in coordinate directions. *}
 
-
 definition "basis k = (\<chi> i. if i = k then 1 else 0)"
 
 lemma basis_component [simp]: "basis k $ i = (if k=i then 1 else 0)"
@@ -1500,11 +1437,9 @@
 
 lemma norm_basis:
   shows "norm (basis k :: real ^'n) = 1"
-  apply (simp add: basis_def real_vector_norm_def dot_def)
+  apply (simp add: basis_def norm_eq_sqrt_inner) unfolding inner_vector_def
   apply (vector delta_mult_idempotent)
-  using setsum_delta[of "UNIV :: 'n set" "k" "\<lambda>k. 1::real"]
-  apply auto
-  done
+  using setsum_delta[of "UNIV :: 'n set" "k" "\<lambda>k. 1::real"] by auto
 
 lemma norm_basis_1: "norm(basis 1 :: real ^'n::{finite,one}) = 1"
   by (rule norm_basis)
@@ -1540,8 +1475,8 @@
   by auto
 
 lemma dot_basis:
-  shows "basis i \<bullet> x = x$i" "x \<bullet> (basis i :: 'a^'n) = (x$i :: 'a::semiring_1)"
-  by (auto simp add: dot_def basis_def cond_application_beta  cond_value_iff setsum_delta cong del: if_weak_cong)
+  shows "basis i \<bullet> x = x$i" "x \<bullet> (basis i) = (x$i)"
+  unfolding inner_vector_def by (auto simp add: basis_def cond_application_beta  cond_value_iff setsum_delta cong del: if_weak_cong)
 
 lemma inner_basis:
   fixes x :: "'a::{real_inner, real_algebra_1} ^ 'n"
@@ -1557,7 +1492,7 @@
   shows "basis k \<noteq> (0:: 'a::semiring_1 ^'n)"
   by (simp add: basis_eq_0)
 
-lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = (z::'a::semiring_1^'n)"
+lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = (z::real^'n)"
   apply (auto simp add: Cart_eq dot_basis)
   apply (erule_tac x="basis i" in allE)
   apply (simp add: dot_basis)
@@ -1566,7 +1501,7 @@
   apply (simp add: Cart_eq)
   done
 
-lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = (y::'a::semiring_1^'n)"
+lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = (y::real^'n)"
   apply (auto simp add: Cart_eq dot_basis)
   apply (erule_tac x="basis i" in allE)
   apply (simp add: dot_basis)
@@ -1580,31 +1515,29 @@
 definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)"
 
 lemma orthogonal_basis:
-  shows "orthogonal (basis i :: 'a^'n) x \<longleftrightarrow> x$i = (0::'a::ring_1)"
-  by (auto simp add: orthogonal_def dot_def basis_def cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong)
+  shows "orthogonal (basis i) x \<longleftrightarrow> x$i = (0::real)"
+  by (auto simp add: orthogonal_def inner_vector_def basis_def cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong)
 
 lemma orthogonal_basis_basis:
-  shows "orthogonal (basis i :: 'a::ring_1^'n) (basis j) \<longleftrightarrow> i \<noteq> j"
+  shows "orthogonal (basis i :: real^'n) (basis j) \<longleftrightarrow> i \<noteq> j"
   unfolding orthogonal_basis[of i] basis_component[of j] by simp
 
   (* FIXME : Maybe some of these require less than comm_ring, but not all*)
 lemma orthogonal_clauses:
-  "orthogonal a (0::'a::comm_ring ^'n)"
-  "orthogonal a x ==> orthogonal a (c *s x)"
+  "orthogonal a (0::real ^'n)"
+  "orthogonal a x ==> orthogonal a (c *\<^sub>R x)"
   "orthogonal a x ==> orthogonal a (-x)"
   "orthogonal a x \<Longrightarrow> orthogonal a y ==> orthogonal a (x + y)"
   "orthogonal a x \<Longrightarrow> orthogonal a y ==> orthogonal a (x - y)"
   "orthogonal 0 a"
-  "orthogonal x a ==> orthogonal (c *s x) a"
+  "orthogonal x a ==> orthogonal (c *\<^sub>R x) a"
   "orthogonal x a ==> orthogonal (-x) a"
   "orthogonal x a \<Longrightarrow> orthogonal y a ==> orthogonal (x + y) a"
   "orthogonal x a \<Longrightarrow> orthogonal y a ==> orthogonal (x - y) a"
-  unfolding orthogonal_def dot_rneg dot_rmult dot_radd dot_rsub
-  dot_lzero dot_rzero dot_lneg dot_lmult dot_ladd dot_lsub
-  by simp_all
-
-lemma orthogonal_commute: "orthogonal (x::'a::{ab_semigroup_mult,comm_monoid_add} ^'n)y \<longleftrightarrow> orthogonal y x"
-  by (simp add: orthogonal_def dot_sym)
+  unfolding orthogonal_def inner_simps by auto
+
+lemma orthogonal_commute: "orthogonal (x::real ^'n)y \<longleftrightarrow> orthogonal y x"
+  by (simp add: orthogonal_def inner_commute)
 
 subsection{* Explicit vector construction from lists. *}
 
@@ -1994,7 +1927,7 @@
 lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis
 
 lemma adjoint_works_lemma:
-  fixes f:: "'a::ring_1 ^'n \<Rightarrow> 'a ^'m"
+  fixes f:: "real ^'n \<Rightarrow> real ^'m"
   assumes lf: "linear f"
   shows "\<forall>x y. f x \<bullet> y = x \<bullet> adjoint f y"
 proof-
@@ -2002,8 +1935,8 @@
   let ?M = "UNIV :: 'm set"
   have fN: "finite ?N" by simp
   have fM: "finite ?M" by simp
-  {fix y:: "'a ^ 'm"
-    let ?w = "(\<chi> i. (f (basis i) \<bullet> y)) :: 'a ^ 'n"
+  {fix y:: "real ^ 'm"
+    let ?w = "(\<chi> i. (f (basis i) \<bullet> y)) :: real ^ 'n"
     {fix x
       have "f x \<bullet> y = f (setsum (\<lambda>i. (x$i) *s basis i) ?N) \<bullet> y"
         by (simp only: basis_expansion)
@@ -2012,7 +1945,7 @@
         by (simp add: linear_cmul[OF lf])
       finally have "f x \<bullet> y = x \<bullet> ?w"
         apply (simp only: )
-        apply (simp add: dot_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] ring_simps)
+        apply (simp add: inner_vector_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] ring_simps)
         done}
   }
   then show ?thesis unfolding adjoint_def
@@ -2022,34 +1955,34 @@
 qed
 
 lemma adjoint_works:
-  fixes f:: "'a::ring_1 ^'n \<Rightarrow> 'a ^'m"
+  fixes f:: "real ^'n \<Rightarrow> real ^'m"
   assumes lf: "linear f"
   shows "x \<bullet> adjoint f y = f x \<bullet> y"
   using adjoint_works_lemma[OF lf] by metis
 
-
 lemma adjoint_linear:
-  fixes f :: "'a::comm_ring_1 ^'n \<Rightarrow> 'a ^'m"
+  fixes f:: "real ^'n \<Rightarrow> real ^'m"
   assumes lf: "linear f"
   shows "linear (adjoint f)"
-  by (simp add: linear_def vector_eq_ldot[symmetric] dot_radd dot_rmult adjoint_works[OF lf])
+  unfolding linear_def vector_eq_ldot[symmetric] apply safe
+  unfolding inner_simps smult_conv_scaleR adjoint_works[OF lf] by auto
 
 lemma adjoint_clauses:
-  fixes f:: "'a::comm_ring_1 ^'n \<Rightarrow> 'a ^'m"
+  fixes f:: "real ^'n \<Rightarrow> real ^'m"
   assumes lf: "linear f"
   shows "x \<bullet> adjoint f y = f x \<bullet> y"
   and "adjoint f y \<bullet> x = y \<bullet> f x"
-  by (simp_all add: adjoint_works[OF lf] dot_sym )
+  by (simp_all add: adjoint_works[OF lf] inner_commute)
 
 lemma adjoint_adjoint:
-  fixes f:: "'a::comm_ring_1 ^ 'n \<Rightarrow> 'a ^'m"
+  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:: "'a::comm_ring_1 ^ 'n \<Rightarrow> 'a ^'m"
+  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)
@@ -2126,11 +2059,11 @@
   by (auto simp add: basis_def cond_value_iff cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong)
 
 lemma matrix_vector_mul_component:
-  shows "((A::'a::semiring_1^_^_) *v x)$k = (A$k) \<bullet> x"
-  by (simp add: matrix_vector_mult_def dot_def)
-
-lemma dot_lmul_matrix: "((x::'a::comm_semiring_1 ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
-  apply (simp add: dot_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)
+  shows "((A::real^_^_) *v x)$k = (A$k) \<bullet> x"
+  by (simp add: matrix_vector_mult_def inner_vector_def)
+
+lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
+  apply (simp add: inner_vector_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)
   apply (subst setsum_commute)
   by simp
 
@@ -2158,7 +2091,7 @@
 text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *}
 
 lemma matrix_mult_dot: "A *v x = (\<chi> i. A$i \<bullet> x)"
-  by (simp add: matrix_vector_mult_def dot_def)
+  by (simp add: matrix_vector_mult_def inner_vector_def)
 
 lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
   by (simp add: matrix_vector_mult_def Cart_eq column_def mult_commute)
@@ -2219,15 +2152,15 @@
 lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
   by (simp add: matrix_vector_mult_def transpose_def Cart_eq mult_commute)
 
-lemma adjoint_matrix: "adjoint(\<lambda>x. (A::'a::comm_ring_1^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
+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 (simp add: transpose_def dot_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib)
+  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)
   done
 
-lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n \<Rightarrow> 'a ^'m)"
+lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
   shows "matrix(adjoint f) = transpose(matrix f)"
   apply (subst matrix_vector_mul[OF lf])
   unfolding adjoint_matrix matrix_of_matrix_vector_mul ..
@@ -2539,11 +2472,11 @@
   apply (auto simp add: Cart_eq matrix_vector_mult_def column_def  mult_commute UNIV_1)
   done
 
-lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n \<Rightarrow> 'a^1)"
+lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \<Rightarrow> real^1)"
   shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
   apply (rule ext)
   apply (subst matrix_works[OF lf, symmetric])
-  apply (simp add: Cart_eq matrix_vector_mult_def row_def dot_def mult_commute forall_1)
+  apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute forall_1)
   done
 
 lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
@@ -2649,11 +2582,11 @@
   have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"
     by (simp add: pastecart_fst_snd)
   have th1: "fstcart x \<bullet> fstcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"
-    by (simp add: dot_def setsum_UNIV_sum pastecart_def setsum_nonneg)
+    by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg)
   then show ?thesis
     unfolding th0
-    unfolding real_vector_norm_def real_sqrt_le_iff id_def
-    by (simp add: dot_def)
+    unfolding norm_eq_sqrt_inner real_sqrt_le_iff id_def
+    by (simp add: inner_vector_def)
 qed
 
 lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y"
@@ -2664,18 +2597,18 @@
   have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"
     by (simp add: pastecart_fst_snd)
   have th1: "sndcart x \<bullet> sndcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"
-    by (simp add: dot_def setsum_UNIV_sum pastecart_def setsum_nonneg)
+    by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg)
   then show ?thesis
     unfolding th0
-    unfolding real_vector_norm_def real_sqrt_le_iff id_def
-    by (simp add: dot_def)
+    unfolding norm_eq_sqrt_inner real_sqrt_le_iff id_def
+    by (simp add: inner_vector_def)
 qed
 
 lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y"
   unfolding dist_norm by (metis sndcart_sub[symmetric] norm_sndcart)
 
-lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n) (x2::'a::{times,comm_monoid_add}^'m)) \<bullet> (pastecart y1 y2) =  x1 \<bullet> y1 + x2 \<bullet> y2"
-  by (simp add: dot_def setsum_UNIV_sum pastecart_def)
+lemma dot_pastecart: "(pastecart (x1::real^'n) (x2::real^'m)) \<bullet> (pastecart y1 y2) =  x1 \<bullet> y1 + x2 \<bullet> y2"
+  by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def)
 
 text {* TODO: move to NthRoot *}
 lemma sqrt_add_le_add_sqrt:
@@ -3867,11 +3800,8 @@
     (* FIXME : Move to some general theory ?*)
 definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)"
 
-lemma vector_sub_project_orthogonal: "(b::'a::linordered_field^'n) \<bullet> (x - ((b \<bullet> x) / (b\<bullet>b)) *s b) = 0"
-  apply (cases "b = 0", simp)
-  apply (simp add: dot_rsub dot_rmult)
-  unfolding times_divide_eq_right[symmetric]
-  by (simp add: field_simps dot_eq_0)
+lemma vector_sub_project_orthogonal: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0"
+  unfolding inner_simps smult_conv_scaleR by auto
 
 lemma basis_orthogonal:
   fixes B :: "(real ^'n) set"
@@ -3886,7 +3816,7 @@
   from `\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C`
   obtain C where C: "finite C" "card C \<le> card B"
     "span C = span B" "pairwise orthogonal C" by blast
-  let ?a = "a - setsum (\<lambda>x. (x\<bullet>a / (x\<bullet>x)) *s x) C"
+  let ?a = "a - setsum (\<lambda>x. (x \<bullet> a / (x \<bullet> x)) *s x) C"
   let ?C = "insert ?a C"
   from C(1) have fC: "finite ?C" by simp
   from fB aB C(1,2) have cC: "card ?C \<le> card (insert a B)" by (simp add: card_insert_if)
@@ -3912,13 +3842,12 @@
       have fth: "finite (C - {y})" using C by simp
       have "orthogonal x y"
         using xa ya
-        unfolding orthogonal_def xa dot_lsub dot_rsub diff_eq_0_iff_eq
+        unfolding orthogonal_def xa inner_simps diff_eq_0_iff_eq
         apply simp
         apply (subst Cy)
         using C(1) fth
-        apply (simp only: setsum_clauses)
-        thm dot_ladd
-        apply (auto simp add: dot_ladd dot_radd dot_lmult dot_rmult dot_eq_0 dot_sym[of y a] dot_lsum[OF fth])
+        apply (simp only: setsum_clauses) unfolding smult_conv_scaleR
+        apply (auto simp add: inner_simps inner_eq_zero_iff inner_commute[of y a] dot_lsum[OF fth])
         apply (rule setsum_0')
         apply clarsimp
         apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
@@ -3929,13 +3858,13 @@
       have fth: "finite (C - {x})" using C by simp
       have "orthogonal x y"
         using xa ya
-        unfolding orthogonal_def ya dot_rsub dot_lsub diff_eq_0_iff_eq
+        unfolding orthogonal_def ya inner_simps diff_eq_0_iff_eq
         apply simp
         apply (subst Cx)
         using C(1) fth
-        apply (simp only: setsum_clauses)
-        apply (subst dot_sym[of x])
-        apply (auto simp add: dot_radd dot_rmult dot_eq_0 dot_sym[of x a] dot_rsum[OF fth])
+        apply (simp only: setsum_clauses) unfolding smult_conv_scaleR
+        apply (subst inner_commute[of x])
+        apply (auto simp add: inner_simps inner_eq_zero_iff inner_commute[of x a] dot_rsum[OF fth])
         apply (rule setsum_0')
         apply clarsimp
         apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
@@ -3988,8 +3917,8 @@
   from B have fB: "finite B" "card B = dim S" using independent_bound by auto
   from span_mono[OF B(2)] span_mono[OF B(3)]
   have sSB: "span S = span B" by (simp add: span_span)
-  let ?a = "a - setsum (\<lambda>b. (a\<bullet>b / (b\<bullet>b)) *s b) B"
-  have "setsum (\<lambda>b. (a\<bullet>b / (b\<bullet>b)) *s b) B \<in> span S"
+  let ?a = "a - setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *s b) B"
+  have "setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *s b) B \<in> span S"
     unfolding sSB
     apply (rule span_setsum[OF fB(1)])
     apply clarsimp
@@ -3998,20 +3927,20 @@
   with a have a0:"?a  \<noteq> 0" by auto
   have "\<forall>x\<in>span B. ?a \<bullet> x = 0"
   proof(rule span_induct')
-    show "subspace (\<lambda>x. ?a \<bullet> x = 0)"
-      by (auto simp add: subspace_def mem_def dot_radd dot_rmult)
-  next
+    show "subspace (\<lambda>x. ?a \<bullet> x = 0)" by (auto simp add: subspace_def mem_def inner_simps smult_conv_scaleR)
+  
+next
     {fix x assume x: "x \<in> B"
       from x have B': "B = insert x (B - {x})" by blast
       have fth: "finite (B - {x})" using fB by simp
       have "?a \<bullet> x = 0"
         apply (subst B') using fB fth
         unfolding setsum_clauses(2)[OF fth]
-        apply simp
-        apply (clarsimp simp add: dot_lsub dot_ladd dot_lmult dot_lsum dot_eq_0)
+        apply simp unfolding inner_simps smult_conv_scaleR
+        apply (clarsimp simp add: inner_simps inner_eq_zero_iff smult_conv_scaleR dot_lsum)
         apply (rule setsum_0', rule ballI)
-        unfolding dot_sym
-        by (auto simp add: x field_simps dot_eq_0 intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
+        unfolding inner_commute
+        by (auto simp add: x field_simps inner_eq_zero_iff intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
     then show "\<forall>x \<in> B. ?a \<bullet> x = 0" by blast
   qed
   with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"])
@@ -4780,8 +4709,8 @@
   "columnvector (A *v v) = A ** columnvector v"
   by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)
 
-lemma dot_matrix_product: "(x::'a::semiring_1^'n) \<bullet> y = (((rowvector x ::'a^'n^1) ** (columnvector y :: 'a^1^'n))$1)$1"
-  by (vector matrix_matrix_mult_def rowvector_def columnvector_def dot_def)
+lemma dot_matrix_product: "(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1"
+  by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vector_def)
 
 lemma dot_matrix_vector_mul:
   fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
@@ -4937,20 +4866,18 @@
     by (auto intro: real_sqrt_pow2)
   have th: "sqrt (real ?d) * infnorm x \<ge> 0"
     by (simp add: zero_le_mult_iff real_sqrt_ge_0_iff infnorm_pos_le)
-  have th1: "x\<bullet>x \<le> (sqrt (real ?d) * infnorm x)^2"
+  have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)^2"
     unfolding power_mult_distrib d2
+    unfolding real_of_nat_def inner_vector_def
+    apply (subst power2_abs[symmetric]) 
+    apply (rule setsum_bounded)
+    apply(auto simp add: power2_eq_square[symmetric])
     apply (subst power2_abs[symmetric])
-    unfolding real_of_nat_def dot_def power2_eq_square[symmetric]
-    apply (subst power2_abs[symmetric])
-    apply (rule setsum_bounded)
     apply (rule power_mono)
-    unfolding abs_of_nonneg[OF infnorm_pos_le]
     unfolding infnorm_def  Sup_finite_ge_iff[OF infnorm_set_lemma]
-    unfolding infnorm_set_image bex_simps
-    apply blast
-    by (rule abs_ge_zero)
-  from real_le_lsqrt[OF dot_pos_le th th1]
-  show ?thesis unfolding real_vector_norm_def id_def .
+    unfolding infnorm_set_image bex_simps apply(rule_tac x=i in exI) by auto
+  from real_le_lsqrt[OF inner_ge_zero th th1]
+  show ?thesis unfolding norm_eq_sqrt_inner id_def .
 qed
 
 (* Equality in Cauchy-Schwarz and triangle inequalities.                     *)
@@ -4964,16 +4891,14 @@
     hence ?thesis by simp}
   moreover
   {assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
-    from dot_eq_0[of "norm y *s x - norm x *s y"]
+    from inner_eq_zero_iff[of "norm y *s x - norm x *s y"]
     have "?rhs \<longleftrightarrow> (norm y * (norm y * norm x * norm x - norm x * (x \<bullet> y)) - norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) =  0)"
       using x y
-      unfolding dot_rsub dot_lsub dot_lmult dot_rmult
-      unfolding norm_pow_2[symmetric] power2_eq_square diff_eq_0_iff_eq apply (simp add: dot_sym)
-      apply (simp add: ring_simps)
-      apply metis
-      done
+      unfolding inner_simps smult_conv_scaleR
+      unfolding power2_norm_eq_inner[symmetric] power2_eq_square diff_eq_0_iff_eq apply (simp add: inner_commute)
+      apply (simp add: ring_simps) by metis
     also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
-      by (simp add: ring_simps dot_sym)
+      by (simp add: ring_simps inner_commute)
     also have "\<dots> \<longleftrightarrow> ?lhs" using x y
       apply simp
       by metis
@@ -4995,8 +4920,7 @@
     unfolding norm_minus_cancel
       norm_mul by blast
   also have "\<dots> \<longleftrightarrow> ?lhs"
-    unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] dot_lneg
-    by arith
+    unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] inner_simps by auto
   finally show ?thesis ..
 qed
 
@@ -5019,8 +4943,8 @@
       by arith
     also have "\<dots> \<longleftrightarrow> norm x *s y = norm y *s x"
       unfolding norm_cauchy_schwarz_eq[symmetric]
-      unfolding norm_pow_2 dot_ladd dot_radd
-      by (simp add: norm_pow_2[symmetric] power2_eq_square dot_sym ring_simps)
+      unfolding power2_norm_eq_inner inner_simps
+      by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute ring_simps)
     finally have ?thesis .}
   ultimately show ?thesis by blast
 qed
@@ -5115,3 +5039,4 @@
 done
 
 end
+ 
\ No newline at end of file