# HG changeset patch
# User huffman
# Date 1277918762 25200
# Node ID 5cbd5d5959f27fe401d2a08bce1a3e8a1414344a
# Parent  48bdc2a43b46bb6333a0af82e7a40c33eee41255
generalize some euclidean_space lemmas

diff -r 48bdc2a43b46 -r 5cbd5d5959f2 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Jun 30 18:19:53 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Jun 30 10:26:02 2010 -0700
@@ -1891,7 +1891,7 @@
 subsection {* Linearity and Bilinearity continued *}
 
 lemma linear_bounded:
-  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes lf: "linear f"
   shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
 proof-
@@ -1919,7 +1919,7 @@
 qed
 
 lemma linear_bounded_pos:
-  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes lf: "linear f"
   shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
 proof-
@@ -1947,7 +1947,7 @@
 qed
 
 lemma linear_conv_bounded_linear:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   shows "linear f \<longleftrightarrow> bounded_linear f"
 proof
   assume "linear f"
@@ -1971,14 +1971,14 @@
     by (simp add: f.add f.scaleR linear_def)
 qed
 
-lemma bounded_linearI': fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+lemma bounded_linearI': fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
   shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym]
   by(rule linearI[OF assms])
 
 
 lemma bilinear_bounded:
-  fixes h:: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::euclidean_space"
+  fixes h:: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::real_normed_vector"
   assumes bh: "bilinear h"
   shows "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
 proof-
@@ -2008,7 +2008,7 @@
 qed
 
 lemma bilinear_bounded_pos:
-  fixes h:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+  fixes h:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
   assumes bh: "bilinear h"
   shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
 proof-
@@ -2029,7 +2029,7 @@
 qed
 
 lemma bilinear_conv_bounded_bilinear:
-  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
   shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
 proof
   assume "bilinear h"