diff -r eb64ffccfc75 -r d74182c93f04 src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Mon Aug 08 10:26:26 2011 -0700 +++ b/src/HOL/Library/Product_Vector.thy Mon Aug 08 10:32:55 2011 -0700 @@ -28,13 +28,13 @@ instance proof fix a b :: real and x y :: "'a \ 'b" show "scaleR a (x + y) = scaleR a x + scaleR a y" - by (simp add: expand_prod_eq scaleR_right_distrib) + by (simp add: prod_eq_iff scaleR_right_distrib) show "scaleR (a + b) x = scaleR a x + scaleR b x" - by (simp add: expand_prod_eq scaleR_left_distrib) + by (simp add: prod_eq_iff scaleR_left_distrib) show "scaleR a (scaleR b x) = scaleR (a * b) x" - by (simp add: expand_prod_eq) + by (simp add: prod_eq_iff) show "scaleR 1 x = x" - by (simp add: expand_prod_eq) + by (simp add: prod_eq_iff) qed end @@ -174,7 +174,7 @@ instance proof fix x y :: "'a \ 'b" show "dist x y = 0 \ x = y" - unfolding dist_prod_def expand_prod_eq by simp + unfolding dist_prod_def prod_eq_iff by simp next fix x y z :: "'a \ 'b" show "dist x y \ dist x z + dist y z" @@ -373,7 +373,7 @@ unfolding norm_prod_def by simp show "norm x = 0 \ x = 0" unfolding norm_prod_def - by (simp add: expand_prod_eq) + by (simp add: prod_eq_iff) show "norm (x + y) \ norm x + norm y" unfolding norm_prod_def apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]) @@ -423,7 +423,7 @@ unfolding inner_prod_def by (intro add_nonneg_nonneg inner_ge_zero) show "inner x x = 0 \ x = 0" - unfolding inner_prod_def expand_prod_eq + unfolding inner_prod_def prod_eq_iff by (simp add: add_nonneg_eq_0_iff) show "norm x = sqrt (inner x x)" unfolding norm_prod_def inner_prod_def