# HG changeset patch
# User huffman
# Date 1272515954 25200
# Node ID f2faab7b46e7cc33f40abfe6e0bfe292e8897a64
# Parent  1535841fc2e981ca35d40d3e2fa27f9c55c925cb
generalize some euclidean space lemmas

diff -r 1535841fc2e9 -r f2faab7b46e7 src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Wed Apr 28 17:48:59 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Wed Apr 28 21:39:14 2010 -0700
@@ -929,7 +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 smult_conv_scaleR by (simp add: inner_simps fc field_simps)
+  show ?thesis unfolding linear_def vector_eq[where 'a="real^'n"] smult_conv_scaleR by (simp add: inner_simps fc field_simps)
 qed
 
 lemma isometry_linear:
diff -r 1535841fc2e9 -r f2faab7b46e7 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Apr 28 17:48:59 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Apr 28 21:39:14 2010 -0700
@@ -726,15 +726,12 @@
   by (metis vector_mul_rcancel)
 
 lemma norm_cauchy_schwarz:
-  fixes x y :: "real ^ 'n"
   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>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)
+  by (rule Cauchy_Schwarz_ineq2)
 
 lemma norm_triangle_sub:
   fixes x y :: "'a::real_normed_vector"
@@ -757,15 +754,15 @@
 
 lemma real_abs_norm: "\<bar>norm x\<bar> = norm x"
   by (rule abs_norm_cancel)
-lemma real_abs_sub_norm: "\<bar>norm (x::real ^ 'n) - norm y\<bar> <= norm(x - y)"
+lemma real_abs_sub_norm: "\<bar>norm x - 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"
+lemma norm_le: "norm(x) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
   by (simp add: norm_eq_sqrt_inner) 
-lemma norm_lt: "norm(x::real ^ 'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
+lemma norm_lt: "norm(x) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
   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"
+lemma norm_eq: "norm(x) = norm (y) \<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"
+lemma norm_eq_1: "norm(x) = 1 \<longleftrightarrow> x \<bullet> x = 1"
   unfolding norm_eq_sqrt_inner by auto
 
 text{* Squaring equations and inequalities involving norms.  *}
@@ -817,9 +814,9 @@
 
 text{* Equality of vectors in terms of @{term "op \<bullet>"} products.    *}
 
-lemma vector_eq: "(x:: real ^ 'n) = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y\<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs")
+lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs")
 proof
-  assume "?lhs" then show ?rhs by simp
+  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
@@ -941,7 +938,7 @@
 lemma dist_triangle_alt:
   fixes x y z :: "'a::metric_space"
   shows "dist y z <= dist x y + dist x z"
-using dist_triangle [of y z x] by (simp add: dist_commute)
+by (rule dist_triangle3)
 
 lemma dist_pos_lt:
   fixes x y :: "'a::metric_space"
@@ -1035,20 +1032,6 @@
   finally  show ?case  using "2.hyps" by simp
 qed
 
-lemma real_setsum_norm:
-  fixes f :: "'a \<Rightarrow> real ^'n"
-  assumes fS: "finite S"
-  shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
-proof(induct rule: finite_induct[OF fS])
-  case 1 thus ?case by simp
-next
-  case (2 x S)
-  from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq)
-  also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S"
-    using "2.hyps" by simp
-  finally  show ?case  using "2.hyps" by simp
-qed
-
 lemma setsum_norm_le:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes fS: "finite S"
@@ -1061,18 +1044,6 @@
     by arith
 qed
 
-lemma real_setsum_norm_le:
-  fixes f :: "'a \<Rightarrow> real ^ 'n"
-  assumes fS: "finite S"
-  and fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
-  shows "norm (setsum f S) \<le> setsum g S"
-proof-
-  from fg have "setsum (\<lambda>x. norm(f x)) S <= setsum g S"
-    by - (rule setsum_mono, simp)
-  then show ?thesis using real_setsum_norm[OF fS, of f] fg
-    by arith
-qed
-
 lemma setsum_norm_bound:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes fS: "finite S"
@@ -1081,16 +1052,8 @@
   using setsum_norm_le[OF fS K] setsum_constant[symmetric]
   by simp
 
-lemma real_setsum_norm_bound:
-  fixes f :: "'a \<Rightarrow> real ^ 'n"
-  assumes fS: "finite S"
-  and K: "\<forall>x \<in> S. norm (f x) \<le> K"
-  shows "norm (setsum f S) \<le> of_nat (card S) * K"
-  using real_setsum_norm_le[OF fS K] setsum_constant[symmetric]
-  by simp
-
 lemma setsum_vmul:
-  fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector,semiring, mult_zero}"
+  fixes f :: "'a \<Rightarrow> 'b::semiring_0"
   assumes fS: "finite S"
   shows "setsum f S *s v = setsum (\<lambda>x. f x *s v) S"
 proof(induct rule: finite_induct[OF fS])
@@ -1156,10 +1119,10 @@
   finally show ?thesis .
 qed
 
-lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{real_inner}^'n) = setsum (\<lambda>x. f x \<bullet> y) S "
+lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> y = 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 "
+lemma dot_rsum: "finite S \<Longrightarrow> y \<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. *}
@@ -1229,23 +1192,21 @@
   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::real^'n)"
-  apply (auto simp add: Cart_eq dot_basis)
-  apply (erule_tac x="basis i" in allE)
-  apply (simp add: dot_basis)
-  apply (subgoal_tac "y = z")
-  apply simp
-  apply (simp add: Cart_eq)
-  done
-
-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)
-  apply (subgoal_tac "x = y")
-  apply simp
-  apply (simp add: Cart_eq)
-  done
+lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
+proof
+  assume "\<forall>x. x \<bullet> y = x \<bullet> z"
+  hence "\<forall>x. x \<bullet> (y - z) = 0" by (simp add: inner_simps)
+  hence "(y - z) \<bullet> (y - z) = 0" ..
+  thus "y = z" by simp
+qed simp
+
+lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = y"
+proof
+  assume "\<forall>z. x \<bullet> z = y \<bullet> z"
+  hence "\<forall>z. (x - y) \<bullet> z = 0" by (simp add: inner_simps)
+  hence "(x - y) \<bullet> (x - y) = 0" ..
+  thus "x = y" by simp
+qed simp
 
 subsection{* Orthogonality. *}
 
@@ -1273,7 +1234,7 @@
   "orthogonal x a \<Longrightarrow> orthogonal y a ==> orthogonal (x - y) a"
   unfolding orthogonal_def inner_simps by auto
 
-lemma orthogonal_commute: "orthogonal (x::real ^'n)y \<longleftrightarrow> orthogonal y x"
+lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
   by (simp add: orthogonal_def inner_commute)
 
 subsection{* Linear functions. *}
@@ -1392,7 +1353,7 @@
       apply (rule mult_mono)
       by (auto simp add: field_simps) }
     then have th: "\<forall>i\<in> ?S. norm ((x$i) *s f (basis i :: real ^'m)) \<le> norm (f (basis i)) * norm x" by metis
-    from real_setsum_norm_le[OF fS, of "\<lambda>i. (x$i) *s (f (basis i))", OF th]
+    from setsum_norm_le[OF fS, of "\<lambda>i. (x$i) *s (f (basis i))", OF th]
     have "norm (f x) \<le> ?B * norm x" unfolding th0 setsum_left_distrib by metis}
   then show ?thesis by blast
 qed
@@ -1528,7 +1489,7 @@
     finally have th: "norm (h x y) = \<dots>" .
     have "norm (h x y) \<le> ?B * norm x * norm y"
       apply (simp add: setsum_left_distrib th)
-      apply (rule real_setsum_norm_le)
+      apply (rule setsum_norm_le)
       using fN fM
       apply simp
       apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps)
@@ -1640,7 +1601,7 @@
   fixes f:: "real ^'n \<Rightarrow> real ^'m"
   assumes lf: "linear f"
   shows "linear (adjoint f)"
-  unfolding linear_def vector_eq_ldot[symmetric] apply safe
+  unfolding linear_def vector_eq_ldot[where 'a="real^'n", symmetric] apply safe
   unfolding inner_simps smult_conv_scaleR adjoint_works[OF lf] by auto
 
 lemma adjoint_clauses:
@@ -1663,7 +1624,7 @@
   shows "f' = adjoint f"
   apply (rule ext)
   using u
-  by (simp add: vector_eq_rdot[symmetric] adjoint_clauses[OF lf])
+  by (simp add: vector_eq_rdot[where 'a="real^'n", symmetric] adjoint_clauses[OF lf])
 
 subsection {* Matrix operations *}