# HG changeset patch
# User huffman
# Date 1244923810 25200
# Node ID f5ffe064412abcc960bee5ca080df288f8a2dd49
# Parent  1dfa55a46d7d44892a554e6a42ae0c82e27c1c58
generalize lemmas

diff -r 1dfa55a46d7d -r f5ffe064412a src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Jun 13 11:56:41 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Jun 13 13:10:10 2009 -0700
@@ -1238,7 +1238,7 @@
 
 text{* Basic arithmetical combining theorems for limits. *}
 
-lemma Lim_linear: fixes f :: "('a \<Rightarrow> real^'n::finite)" and h :: "(real^'n \<Rightarrow> real^'m::finite)"
+lemma Lim_linear:
   assumes "(f ---> l) net" "bounded_linear h"
   shows "((\<lambda>x. h (f x)) ---> h l) net"
 using `bounded_linear h` `(f ---> l) net`
@@ -1251,7 +1251,7 @@
   by (rule tendsto_const)
 
 lemma Lim_cmul:
-  fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   shows "(f ---> l) net ==> ((\<lambda>x. c *\<^sub>R f x) ---> c *\<^sub>R l) net"
   by (intro tendsto_intros)
 
@@ -1433,7 +1433,6 @@
 text{* Limit under bilinear function *}
 
 lemma Lim_bilinear:
-  fixes net :: "'a net" and h:: "real ^'m::finite \<Rightarrow> real ^'n::finite \<Rightarrow> real ^'p::finite"
   assumes "(f ---> l) net" and "(g ---> m) net" and "bounded_bilinear h"
   shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net"
 using `bounded_bilinear h` `(f ---> l) net` `(g ---> m) net`
@@ -2062,7 +2061,6 @@
 qed
 
 lemma bounded_linear_image:
-  fixes f :: "real^'m::finite \<Rightarrow> real^'n::finite"
   assumes "bounded S" "bounded_linear f"
   shows "bounded(f ` S)"
 proof-
@@ -2078,7 +2076,7 @@
 qed
 
 lemma bounded_scaling:
-  fixes S :: "(real ^ 'n::finite) set"
+  fixes S :: "'a::real_normed_vector set"
   shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)"
   apply (rule bounded_linear_image, assumption)
   apply (rule scaleR.bounded_linear_right)
@@ -3426,7 +3424,7 @@
   by (auto simp add: continuous_def Lim_const)
 
 lemma continuous_cmul:
-  fixes f :: "'a::t2_space \<Rightarrow> real ^ 'n::finite"
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous net f ==> continuous net (\<lambda>x. c *\<^sub>R f x)"
   by (auto simp add: continuous_def Lim_cmul)
 
@@ -3452,7 +3450,7 @@
   unfolding continuous_on_eq_continuous_within using continuous_const by blast
 
 lemma continuous_on_cmul:
-  fixes f :: "'a::metric_space \<Rightarrow> real ^ _"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous_on s f ==>  continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
   unfolding continuous_on_eq_continuous_within using continuous_cmul by blast
 
@@ -3480,7 +3478,8 @@
   unfolding uniformly_continuous_on_def by simp
 
 lemma uniformly_continuous_on_cmul:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+    (* FIXME: generalize 'a to metric_space *)
   assumes "uniformly_continuous_on s f"
   shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
 proof-
@@ -3869,7 +3868,7 @@
 qed
 
 lemma open_affinity:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::real_normed_vector set"
   assumes "open s"  "c \<noteq> 0"
   shows "open ((\<lambda>x. a + c *\<^sub>R x) ` s)"
 proof-
@@ -4021,7 +4020,7 @@
 
 subsection{* Topological properties of linear functions.                               *}
 
-lemma linear_lim_0: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma linear_lim_0:
   assumes "bounded_linear f" shows "(f ---> 0) (at (0))"
 proof-
   interpret f: bounded_linear f by fact
@@ -4030,44 +4029,34 @@
   thus ?thesis unfolding f.zero .
 qed
 
-lemma bounded_linear_continuous_at:
+lemma linear_continuous_at:
   assumes "bounded_linear f"  shows "continuous (at a) f"
   unfolding continuous_at using assms
   apply (rule bounded_linear.tendsto)
   apply (rule tendsto_ident_at)
   done
 
-lemma linear_continuous_at:
-  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
-  assumes "bounded_linear f"  shows "continuous (at a) f"
-  using assms by (rule bounded_linear_continuous_at)
-
 lemma linear_continuous_within:
-  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
   shows "bounded_linear f ==> continuous (at x within s) f"
   using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
 
 lemma linear_continuous_on:
-  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
   shows "bounded_linear f ==> continuous_on s f"
   using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
 
 text{* Also bilinear functions, in composition form.                             *}
 
 lemma bilinear_continuous_at_compose:
-  fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
   shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h
         ==> continuous (at x) (\<lambda>x. h (f x) (g x))"
   unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto
 
 lemma bilinear_continuous_within_compose:
-  fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
   shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bounded_bilinear h
         ==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
   unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
 
 lemma bilinear_continuous_on_compose:
-  fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
   shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h
              ==> continuous_on s (\<lambda>x. h (f x) (g x))"
   unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto
@@ -4224,10 +4213,10 @@
 subsection{* We can now extend limit compositions to consider the scalar multiplier.   *}
 
 lemma Lim_mul:
-  fixes f :: "'a \<Rightarrow> real ^ _"
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "(c ---> d) net"  "(f ---> l) net"
   shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net"
-  unfolding smult_conv_scaleR using assms by (rule scaleR.tendsto)
+  using assms by (rule scaleR.tendsto)
 
 lemma Lim_vmul:
   fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector"
@@ -4358,25 +4347,20 @@
 
 text{* Hence some useful properties follow quite easily.                         *}
 
-lemma compact_scaleR_image:
+lemma compact_scaling:
   fixes s :: "'a::real_normed_vector set"
-  assumes "compact s"  shows "compact ((\<lambda>x. scaleR c x) ` s)"
+  assumes "compact s"  shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
 proof-
   let ?f = "\<lambda>x. scaleR c x"
   have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right)
   show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
-    using bounded_linear_continuous_at[OF *] assms by auto
-qed
-
-lemma compact_scaling:
-  fixes s :: "(real ^ _) set"
-  assumes "compact s"  shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
-  using assms unfolding smult_conv_scaleR by (rule compact_scaleR_image)
+    using linear_continuous_at[OF *] assms by auto
+qed
 
 lemma compact_negations:
   fixes s :: "'a::real_normed_vector set"
   assumes "compact s"  shows "compact ((\<lambda>x. -x) ` s)"
-  using compact_scaleR_image [OF assms, of "- 1"] by auto
+  using compact_scaling [OF assms, of "- 1"] by auto
 
 lemma compact_sums:
   fixes s t :: "'a::real_normed_vector set"
@@ -4407,7 +4391,7 @@
 qed
 
 lemma compact_affinity:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::real_normed_vector set"
   assumes "compact s"  shows "compact ((\<lambda>x. a + c *\<^sub>R x) ` s)"
 proof-
   have "op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
@@ -4481,9 +4465,9 @@
 
 text{* Related results with closure as the conclusion.                           *}
 
-lemma closed_scaleR_image:
+lemma closed_scaling:
   fixes s :: "'a::real_normed_vector set"
-  assumes "closed s" shows "closed ((\<lambda>x. scaleR c x) ` s)"
+  assumes "closed s" shows "closed ((\<lambda>x. c *\<^sub>R x) ` s)"
 proof(cases "s={}")
   case True thus ?thesis by auto
 next
@@ -4515,15 +4499,10 @@
   qed
 qed
 
-lemma closed_scaling:
-  fixes s :: "(real ^ _) set"
-  assumes "closed s" shows "closed ((\<lambda>x. c *\<^sub>R x) ` s)"
-  using assms unfolding smult_conv_scaleR by (rule closed_scaleR_image)
-
 lemma closed_negations:
   fixes s :: "'a::real_normed_vector set"
   assumes "closed s"  shows "closed ((\<lambda>x. -x) ` s)"
-  using closed_scaleR_image[OF assms, of "- 1"] by simp
+  using closed_scaling[OF assms, of "- 1"] by simp
 
 lemma compact_closed_sums:
   fixes s :: "'a::real_normed_vector set"
@@ -5140,24 +5119,12 @@
 
 subsection{* Closure of halfspaces and hyperplanes.                                    *}
 
-lemma Lim_dot: fixes f :: "real^'m \<Rightarrow> real^'n::finite"
-  assumes "(f ---> l) net"  shows "((\<lambda>y. a \<bullet> (f y)) ---> a \<bullet> l) net"
-  unfolding dot_def by (intro tendsto_intros assms)
-
-lemma continuous_at_dot:
-  fixes x :: "real ^ _"
-  shows "continuous (at x) (\<lambda>y. a \<bullet> y)"
-proof-
-  have "((\<lambda>x. x) ---> x) (at x)" unfolding Lim_at by auto
-  thus ?thesis unfolding continuous_at and o_def using Lim_dot[of "\<lambda>x. x" x "at x" a] by auto
-qed
-
-lemma continuous_on_dot:
-  fixes s :: "(real ^ _) set"
-  shows "continuous_on s (\<lambda>y. a \<bullet> y)"
-  using continuous_at_imp_continuous_on[of s "\<lambda>y. a \<bullet> y"]
-  using continuous_at_dot
-  by auto
+lemma Lim_inner:
+  assumes "(f ---> l) net"  shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
+  by (intro tendsto_intros assms)
+
+lemma continuous_at_inner: "continuous (at x) (inner a)"
+  unfolding continuous_at by (intro tendsto_intros)
 
 lemma continuous_on_inner:
   fixes s :: "'a::real_inner set"
@@ -5266,7 +5233,7 @@
   using assms unfolding continuous_on unfolding Lim_within_union
   unfolding Lim unfolding trivial_limit_within unfolding closed_limpt by auto
 
-lemma continuous_on_cases: fixes g :: "real^'m::finite \<Rightarrow> real ^'n::finite"
+lemma continuous_on_cases:
   assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g"
           "\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x"
   shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
@@ -5322,22 +5289,24 @@
      (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
      (\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
 
-definition homeomorphic :: "((real^'a::finite) set) \<Rightarrow> ((real^'b::finite) set) \<Rightarrow> bool" (infixr "homeomorphic" 60) where
+definition
+  homeomorphic :: "'a::metric_space set \<Rightarrow> 'b::metric_space set \<Rightarrow> bool"
+    (infixr "homeomorphic" 60) where
   homeomorphic_def: "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)"
 
 lemma homeomorphic_refl: "s homeomorphic s"
   unfolding homeomorphic_def
   unfolding homeomorphism_def
   using continuous_on_id
-  apply(rule_tac x = "(\<lambda>x::real^'a.x)" in exI)
-  apply(rule_tac x = "(\<lambda>x::real^'b.x)" in exI)
+  apply(rule_tac x = "(\<lambda>x. x)" in exI)
+  apply(rule_tac x = "(\<lambda>x. x)" in exI)
   by blast
 
 lemma homeomorphic_sym:
  "s homeomorphic t \<longleftrightarrow> t homeomorphic s"
 unfolding homeomorphic_def
 unfolding homeomorphism_def
-by blast
+by blast (* FIXME: slow *)
 
 lemma homeomorphic_trans:
   assumes "s homeomorphic t" "t homeomorphic u" shows "s homeomorphic u"
@@ -5379,7 +5348,8 @@
  using assms unfolding inj_on_def inv_on_def by auto
 
 lemma homeomorphism_compact:
-  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+  fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
+    (* class constraint due to continuous_on_inverse *)
   assumes "compact s" "continuous_on s f"  "f ` s = t"  "inj_on f s"
   shows "\<exists>g. homeomorphism s t f g"
 proof-
@@ -5406,7 +5376,9 @@
 qed
 
 lemma homeomorphic_compact:
- "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
+  fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
+    (* class constraint due to continuous_on_inverse *)
+  shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
           \<Longrightarrow> s homeomorphic t"
   unfolding homeomorphic_def by(metis homeomorphism_compact)
 
@@ -5420,6 +5392,7 @@
 text{* Results on translation, scaling etc.                                      *}
 
 lemma homeomorphic_scaling:
+  fixes s :: "'a::real_normed_vector set"
   assumes "c \<noteq> 0"  shows "s homeomorphic ((\<lambda>x. c *\<^sub>R x) ` s)"
   unfolding homeomorphic_minimal
   apply(rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
@@ -5428,13 +5401,15 @@
   using continuous_on_cmul[OF continuous_on_id] by auto
 
 lemma homeomorphic_translation:
- "s homeomorphic ((\<lambda>x. a + x) ` s)"
+  fixes s :: "'a::real_normed_vector set"
+  shows "s homeomorphic ((\<lambda>x. a + x) ` s)"
   unfolding homeomorphic_minimal
   apply(rule_tac x="\<lambda>x. a + x" in exI)
   apply(rule_tac x="\<lambda>x. -a + x" in exI)
   using continuous_on_add[OF continuous_on_const continuous_on_id] by auto
 
 lemma homeomorphic_affinity:
+  fixes s :: "'a::real_normed_vector set"
   assumes "c \<noteq> 0"  shows "s homeomorphic ((\<lambda>x. a + c *\<^sub>R x) ` s)"
 proof-
   have *:"op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
@@ -5444,7 +5419,8 @@
     using homeomorphic_translation[of "(\<lambda>x. c *\<^sub>R x) ` s" a] unfolding * by auto
 qed
 
-lemma homeomorphic_balls: fixes a b ::"real^'a::finite"
+lemma homeomorphic_balls:
+  fixes a b ::"'a::real_normed_vector" (* FIXME: generalize to metric_space *)
   assumes "0 < d"  "0 < e"
   shows "(ball a d) homeomorphic  (ball b e)" (is ?th)
         "(cball a d) homeomorphic (cball b e)" (is ?cth)