# HG changeset patch
# User huffman
# Date 1278024058 25200
# Node ID 40424fc83cc1dfa5922bced3785a91bb40b2db9d
# Parent  f86de9c00c474c84529b845408ea4ee40a282a41# Parent  645eb9fec7940d1db4ce035168a5182f7850890d
merged

diff -r 645eb9fec794 -r 40424fc83cc1 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Jul 01 19:14:54 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Jul 01 15:40:58 2010 -0700
@@ -1998,7 +1998,7 @@
 *)
 subsection {* Another intermediate value theorem formulation. *}
 
-lemma ivt_increasing_component_on_1: fixes f::"real \<Rightarrow> 'a::ordered_euclidean_space"
+lemma ivt_increasing_component_on_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
   assumes "a \<le> b" "continuous_on {a .. b} f" "(f a)$$k \<le> y" "y \<le> (f b)$$k"
   shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
 proof- have "f a \<in> f ` {a..b}" "f b \<in> f ` {a..b}" apply(rule_tac[!] imageI) 
@@ -2007,20 +2007,20 @@
     using connected_continuous_image[OF assms(2) convex_connected[OF convex_real_interval(5)]]
     using assms by(auto intro!: imageI) qed
 
-lemma ivt_increasing_component_1: fixes f::"real \<Rightarrow> 'a::ordered_euclidean_space"
+lemma ivt_increasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
   shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
    \<Longrightarrow> f a$$k \<le> y \<Longrightarrow> y \<le> f b$$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$$k = y"
 by(rule ivt_increasing_component_on_1)
   (auto simp add: continuous_at_imp_continuous_on)
 
-lemma ivt_decreasing_component_on_1: fixes f::"real \<Rightarrow> 'a::ordered_euclidean_space"
+lemma ivt_decreasing_component_on_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
   assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)$$k \<le> y" "y \<le> (f a)$$k"
   shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
   apply(subst neg_equal_iff_equal[THEN sym])
   using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"] using assms using continuous_on_neg
   by (auto simp add:euclidean_simps)
 
-lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::ordered_euclidean_space"
+lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
   shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
     \<Longrightarrow> f b$$k \<le> y \<Longrightarrow> y \<le> f a$$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$$k = y"
 by(rule ivt_decreasing_component_on_1)
@@ -2212,6 +2212,7 @@
 
 lemma convex_on_continuous:
   assumes "open (s::('a::ordered_euclidean_space) set)" "convex_on s f" 
+  (* FIXME: generalize to euclidean_space *)
   shows "continuous_on s f"
   unfolding continuous_on_eq_continuous_at[OF assms(1)] proof
   note dimge1 = DIM_positive[where 'a='a]
diff -r 645eb9fec794 -r 40424fc83cc1 src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Jul 01 19:14:54 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Jul 01 15:40:58 2010 -0700
@@ -4,7 +4,7 @@
 header {* Fashoda meet theorem. *}
 
 theory Fashoda
-imports Brouwer_Fixpoint Path_Connected
+imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
 begin
 
 subsection {*Fashoda meet theorem. *}
diff -r 645eb9fec794 -r 40424fc83cc1 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Jul 01 19:14:54 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Jul 01 15:40:58 2010 -0700
@@ -5,7 +5,7 @@
 header {* Continuous paths and path-connected sets *}
 
 theory Path_Connected
-imports Cartesian_Euclidean_Space
+imports Convex_Euclidean_Space
 begin
 
 subsection {* Paths. *}
@@ -502,71 +502,80 @@
     apply(erule_tac[!] UnE)+ apply(rule_tac[2-3] path_component_trans[of _ _ z])
     by(auto simp add:path_component_of_subset [OF Un_upper1] path_component_of_subset[OF Un_upper2]) qed
 
-subsection {* sphere is path-connected. *}
+lemma path_connected_UNION:
+  assumes "\<And>i. i \<in> A \<Longrightarrow> path_connected (S i)"
+  assumes "\<And>i. i \<in> A \<Longrightarrow> z \<in> S i"
+  shows "path_connected (\<Union>i\<in>A. S i)"
+unfolding path_connected_component proof(clarify)
+  fix x i y j
+  assume *: "i \<in> A" "x \<in> S i" "j \<in> A" "y \<in> S j"
+  hence "path_component (S i) x z" and "path_component (S j) z y"
+    using assms by (simp_all add: path_connected_component)
+  hence "path_component (\<Union>i\<in>A. S i) x z" and "path_component (\<Union>i\<in>A. S i) z y"
+    using *(1,3) by (auto elim!: path_component_of_subset [COMP swap_prems_rl])
+  thus "path_component (\<Union>i\<in>A. S i) x y"
+    by (rule path_component_trans)
+qed
 
-(** TODO covert this to ordered_euclidean_space **)
+subsection {* sphere is path-connected. *}
 
 lemma path_connected_punctured_universe:
- assumes "2 \<le> CARD('n::finite)" shows "path_connected((UNIV::(real^'n) set) - {a})" proof-
-  obtain \<psi> where \<psi>:"bij_betw \<psi> {1..CARD('n)} (UNIV::'n set)" using ex_bij_betw_nat_finite_1[OF finite_UNIV] by auto
-  let ?U = "UNIV::(real^'n) set" let ?u = "?U - {0}"
-  let ?basis = "\<lambda>k. cart_basis (\<psi> k)"
-  let ?A = "\<lambda>k. {x::real^'n. \<exists>i\<in>{1..k}. inner (cart_basis (\<psi> i)) x \<noteq> 0}"
-  have "\<forall>k\<in>{2..CARD('n)}. path_connected (?A k)" proof
-    have *:"\<And>k. ?A (Suc k) = {x. inner (?basis (Suc k)) x < 0} \<union> {x. inner (?basis (Suc k)) x > 0} \<union> ?A k" apply(rule set_ext,rule) defer
-      apply(erule UnE)+  unfolding mem_Collect_eq apply(rule_tac[1-2] x="Suc k" in bexI)
-      by(auto elim!: ballE simp add: not_less le_Suc_eq)
-    fix k assume "k \<in> {2..CARD('n)}" thus "path_connected (?A k)" proof(induct k)
-      case (Suc k) show ?case proof(cases "k = 1")
-        case False from Suc have d:"k \<in> {1..CARD('n)}" "Suc k \<in> {1..CARD('n)}" by auto
-        hence "\<psi> k \<noteq> \<psi> (Suc k)" using \<psi>[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=k]] by auto
-        hence **:"?basis k + ?basis (Suc k) \<in> {x. 0 < inner (?basis (Suc k)) x} \<inter> (?A k)" 
-          "?basis k - ?basis (Suc k) \<in> {x. 0 > inner (?basis (Suc k)) x} \<inter> ({x. 0 < inner (?basis (Suc k)) x} \<union> (?A k))" using d
-          by(auto simp add: inner_basis intro!:bexI[where x=k])
-        show ?thesis unfolding * Un_assoc apply(rule path_connected_Un) defer apply(rule path_connected_Un) 
-          prefer 5 apply(rule_tac[1-2] convex_imp_path_connected, rule convex_halfspace_lt, rule convex_halfspace_gt)
-          apply(rule Suc(1)) using d ** False by auto
-      next case True hence d:"1\<in>{1..CARD('n)}" "2\<in>{1..CARD('n)}" using Suc(2) by auto
-        have ***:"Suc 1 = 2" by auto
-        have **:"\<And>s t P Q. s \<union> t \<union> {x. P x \<or> Q x} = (s \<union> {x. P x}) \<union> (t \<union> {x. Q x})" by auto
-        have nequals0I:"\<And>x A. x\<in>A \<Longrightarrow> A \<noteq> {}" by auto
-        have "\<psi> 2 \<noteq> \<psi> (Suc 0)" using \<psi>[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=2]] using assms by auto
-        thus ?thesis unfolding * True unfolding ** neq_iff bex_disj_distrib apply -
-          apply(rule path_connected_Un, rule_tac[1-2] path_connected_Un) defer 3 apply(rule_tac[1-4] convex_imp_path_connected) 
-          apply(rule_tac[5] x=" ?basis 1 + ?basis 2" in nequals0I)
-          apply(rule_tac[6] x="-?basis 1 + ?basis 2" in nequals0I)
-          apply(rule_tac[7] x="-?basis 1 - ?basis 2" in nequals0I)
-          using d unfolding *** by(auto intro!: convex_halfspace_gt convex_halfspace_lt, auto simp add: inner_basis)
-  qed qed auto qed note lem = this
+  assumes "2 \<le> DIM('a::euclidean_space)"
+  shows "path_connected((UNIV::'a::euclidean_space set) - {a})"
+proof-
+  let ?A = "{x::'a. \<exists>i\<in>{..<DIM('a)}. x $$ i < a $$ i}"
+  let ?B = "{x::'a. \<exists>i\<in>{..<DIM('a)}. a $$ i < x $$ i}"
 
-  have ***:"\<And>x::real^'n. (\<exists>i\<in>{1..CARD('n)}. inner (cart_basis (\<psi> i)) x \<noteq> 0) \<longleftrightarrow> (\<exists>i. inner (cart_basis i) x \<noteq> 0)"
-    apply rule apply(erule bexE) apply(rule_tac x="\<psi> i" in exI) defer apply(erule exE) proof- 
-    fix x::"real^'n" and i assume as:"inner (cart_basis i) x \<noteq> 0"
-    have "i\<in>\<psi> ` {1..CARD('n)}" using \<psi>[unfolded bij_betw_def, THEN conjunct2] by auto
-    then obtain j where "j\<in>{1..CARD('n)}" "\<psi> j = i" by auto
-    thus "\<exists>i\<in>{1..CARD('n)}. inner (cart_basis (\<psi> i)) x \<noteq> 0" apply(rule_tac x=j in bexI) using as by auto qed auto
-  have *:"?U - {a} = (\<lambda>x. x + a) ` {x. x \<noteq> 0}" apply(rule set_ext) unfolding image_iff 
-    apply rule apply(rule_tac x="x - a" in bexI) by auto
-  have **:"\<And>x::real^'n. x\<noteq>0 \<longleftrightarrow> (\<exists>i. inner (cart_basis i) x \<noteq> 0)" unfolding Cart_eq by(auto simp add: inner_basis)
-  show ?thesis unfolding * apply(rule path_connected_continuous_image) apply(rule continuous_on_intros)+ 
-    unfolding ** apply(rule lem[THEN bspec[where x="CARD('n)"], unfolded ***]) using assms by auto qed
+  have A: "path_connected ?A" unfolding Collect_bex_eq
+  proof (rule path_connected_UNION)
+    fix i assume "i \<in> {..<DIM('a)}"
+    thus "(\<chi>\<chi> i. a $$ i - 1) \<in> {x::'a. x $$ i < a $$ i}" by simp
+    show "path_connected {x. x $$ i < a $$ i}" unfolding euclidean_component_def
+      by (rule convex_imp_path_connected [OF convex_halfspace_lt])
+  qed
+  have B: "path_connected ?B" unfolding Collect_bex_eq
+  proof (rule path_connected_UNION)
+    fix i assume "i \<in> {..<DIM('a)}"
+    thus "(\<chi>\<chi> i. a $$ i + 1) \<in> {x::'a. a $$ i < x $$ i}" by simp
+    show "path_connected {x. a $$ i < x $$ i}" unfolding euclidean_component_def
+      by (rule convex_imp_path_connected [OF convex_halfspace_gt])
+  qed
+  from assms have "1 < DIM('a)" by auto
+  hence "a + basis 0 - basis 1 \<in> ?A \<inter> ?B" by auto
+  hence "?A \<inter> ?B \<noteq> {}" by fast
+  with A B have "path_connected (?A \<union> ?B)"
+    by (rule path_connected_Un)
+  also have "?A \<union> ?B = {x. \<exists>i\<in>{..<DIM('a)}. x $$ i \<noteq> a $$ i}"
+    unfolding neq_iff bex_disj_distrib Collect_disj_eq ..
+  also have "\<dots> = {x. x \<noteq> a}"
+    unfolding Bex_def euclidean_eq [where 'a='a] by simp
+  also have "\<dots> = UNIV - {a}" by auto
+  finally show ?thesis .
+qed
 
-lemma path_connected_sphere: assumes "2 \<le> CARD('n::finite)" shows "path_connected {x::real^'n. norm(x - a) = r}" proof(cases "r\<le>0")
-  case True thus ?thesis proof(cases "r=0") 
-    case False hence "{x::real^'n. norm(x - a) = r} = {}" using True by auto
-    thus ?thesis using path_connected_empty by auto
-  qed(auto intro!:path_connected_singleton) next
-  case False hence *:"{x::real^'n. norm(x - a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}" unfolding not_le apply -apply(rule set_ext,rule)
+lemma path_connected_sphere:
+  assumes "2 \<le> DIM('a::euclidean_space)"
+  shows "path_connected {x::'a::euclidean_space. norm(x - a) = r}"
+proof (rule linorder_cases [of r 0])
+  assume "r < 0" hence "{x::'a. norm(x - a) = r} = {}" by auto
+  thus ?thesis using path_connected_empty by simp
+next
+  assume "r = 0"
+  thus ?thesis using path_connected_singleton by simp
+next
+  assume r: "0 < r"
+  hence *:"{x::'a. norm(x - a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}" apply -apply(rule set_ext,rule)
     unfolding image_iff apply(rule_tac x="(1/r) *\<^sub>R (x - a)" in bexI) unfolding mem_Collect_eq norm_scaleR by (auto simp add: scaleR_right_diff_distrib)
-  have **:"{x::real^'n. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" apply(rule set_ext,rule)
+  have **:"{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" apply(rule set_ext,rule)
     unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto split:split_if_asm)
-  have "continuous_on (UNIV - {0}) (\<lambda>x::real^'n. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within
+  have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within
     apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
     apply(rule continuous_at_norm[unfolded o_def]) by auto
   thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
-    by(auto intro!: path_connected_continuous_image continuous_on_intros) qed
+    by(auto intro!: path_connected_continuous_image continuous_on_intros)
+qed
 
-lemma connected_sphere: "2 \<le> CARD('n) \<Longrightarrow> connected {x::real^'n. norm(x - a) = r}"
+lemma connected_sphere: "2 \<le> DIM('a::euclidean_space) \<Longrightarrow> connected {x::'a. norm(x - a) = r}"
   using path_connected_sphere path_connected_imp_connected by auto
 
 end
diff -r 645eb9fec794 -r 40424fc83cc1 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jul 01 19:14:54 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jul 01 15:40:58 2010 -0700
@@ -4994,7 +4994,7 @@
 
 (* Some stuff for half-infinite intervals too; FIXME: notation?  *)
 
-lemma closed_interval_left: fixes b::"'a::ordered_euclidean_space"
+lemma closed_interval_left: fixes b::"'a::euclidean_space"
   shows "closed {x::'a. \<forall>i<DIM('a). x$$i \<le> b$$i}"
 proof-
   { fix i assume i:"i<DIM('a)"
@@ -5008,7 +5008,7 @@
   thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
 qed
 
-lemma closed_interval_right: fixes a::"'a::ordered_euclidean_space"
+lemma closed_interval_right: fixes a::"'a::euclidean_space"
   shows "closed {x::'a. \<forall>i<DIM('a). a$$i \<le> x$$i}"
 proof-
   { fix i assume i:"i<DIM('a)"
@@ -5076,11 +5076,11 @@
 qed
 
 lemma closed_halfspace_component_le:
-  shows "closed {x::'a::ordered_euclidean_space. x$$i \<le> a}"
+  shows "closed {x::'a::euclidean_space. x$$i \<le> a}"
   using closed_halfspace_le[of "(basis i)::'a" a] unfolding euclidean_component_def .
 
 lemma closed_halfspace_component_ge:
-  shows "closed {x::'a::ordered_euclidean_space. x$$i \<ge> a}"
+  shows "closed {x::'a::euclidean_space. x$$i \<ge> a}"
   using closed_halfspace_ge[of a "(basis i)::'a"] unfolding euclidean_component_def .
 
 text{* Openness of halfspaces.                                                   *}
@@ -5098,16 +5098,16 @@
 qed
 
 lemma open_halfspace_component_lt:
-  shows "open {x::'a::ordered_euclidean_space. x$$i < a}"
+  shows "open {x::'a::euclidean_space. x$$i < a}"
   using open_halfspace_lt[of "(basis i)::'a" a] unfolding euclidean_component_def .
 
 lemma open_halfspace_component_gt:
-  shows "open {x::'a::ordered_euclidean_space. x$$i  > a}"
+  shows "open {x::'a::euclidean_space. x$$i  > a}"
   using open_halfspace_gt[of a "(basis i)::'a"] unfolding euclidean_component_def .
 
 text{* This gives a simple derivation of limit component bounds.                 *}
 
-lemma Lim_component_le: fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
+lemma Lim_component_le: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
   assumes "(f ---> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f(x)$$i \<le> b) net"
   shows "l$$i \<le> b"
 proof-
@@ -5117,7 +5117,7 @@
     using closed_halfspace_le[of "(basis i)::'b" b] and assms(1,2,3) by auto
 qed
 
-lemma Lim_component_ge: fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
+lemma Lim_component_ge: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
   assumes "(f ---> l) net"  "\<not> (trivial_limit net)"  "eventually (\<lambda>x. b \<le> (f x)$$i) net"
   shows "b \<le> l$$i"
 proof-
@@ -5127,7 +5127,7 @@
     using closed_halfspace_ge[of b "(basis i)"] and assms(1,2,3) by auto
 qed
 
-lemma Lim_component_eq: fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
+lemma Lim_component_eq: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
   assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)$$i = b) net"
   shows "l$$i = b"
   using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto
@@ -5187,7 +5187,7 @@
   ultimately show False using assms(1)[unfolded connected_def not_ex, THEN spec[where x="?A"], THEN spec[where x="?B"]] and assms(2-5) by auto
 qed
 
-lemma connected_ivt_component: fixes x::"'a::ordered_euclidean_space" shows
+lemma connected_ivt_component: fixes x::"'a::euclidean_space" shows
  "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x$$k \<le> a \<Longrightarrow> a \<le> y$$k \<Longrightarrow> (\<exists>z\<in>s.  z$$k = a)"
   using connected_ivt_hyperplane[of s x y "(basis k)::'a" a]
   unfolding euclidean_component_def by auto