# HG changeset patch
# User huffman
# Date 1272162740 25200
# Node ID 87b6c83d7ed7119b7ac76f34d1a7006ba83eaaac
# Parent  1c8fc1bae0b53ffb59d055fbcff899438404d82d
generalize constant closest_point

diff -r 1c8fc1bae0b5 -r 87b6c83d7ed7 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Apr 24 14:06:19 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Apr 24 19:32:20 2010 -0700
@@ -1519,7 +1519,7 @@
 subsection {* Closest point of a convex set is unique, with a continuous projection. *}
 
 definition
-  closest_point :: "(real ^ 'n) set \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
+  closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a" where
  "closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"
 
 lemma closest_point_exists:
@@ -1553,7 +1553,7 @@
 lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y"
   unfolding norm_eq_sqrt_inner by simp
 
-lemma closer_points_lemma: fixes y::"real^'n"
+lemma closer_points_lemma:
   assumes "inner y z > 0"
   shows "\<exists>u>0. \<forall>v>0. v \<le> u \<longrightarrow> norm(v *\<^sub>R z - y) < norm y"
 proof- have z:"inner z z > 0" unfolding inner_gt_zero_iff using assms by auto
@@ -1564,7 +1564,6 @@
   qed(rule divide_pos_pos, auto) qed
 
 lemma closer_point_lemma:
-  fixes x y z :: "real ^ 'n"
   assumes "inner (y - x) (z - x) > 0"
   shows "\<exists>u>0. u \<le> 1 \<and> dist (x + u *\<^sub>R (z - x)) y < dist x y"
 proof- obtain u where "u>0" and u:"\<forall>v>0. v \<le> u \<longrightarrow> norm (v *\<^sub>R (z - x) - (y - x)) < norm (y - x)"
@@ -1573,7 +1572,6 @@
     unfolding dist_norm by(auto simp add: norm_minus_commute field_simps) qed
 
 lemma any_closest_point_dot:
-  fixes s :: "(real ^ _) set"
   assumes "convex s" "closed s" "x \<in> s" "y \<in> s" "\<forall>z\<in>s. dist a x \<le> dist a z"
   shows "inner (a - x) (y - x) \<le> 0"
 proof(rule ccontr) assume "\<not> inner (a - x) (y - x) \<le> 0"
@@ -1582,7 +1580,7 @@
   thus False using assms(5)[THEN bspec[where x="?z"]] and u(3) by (auto simp add: dist_commute algebra_simps) qed
 
 lemma any_closest_point_unique:
-  fixes s :: "(real ^ _) set"
+  fixes x :: "'a::real_inner"
   assumes "convex s" "closed s" "x \<in> s" "y \<in> s"
   "\<forall>z\<in>s. dist a x \<le> dist a z" "\<forall>z\<in>s. dist a y \<le> dist a z"
   shows "x = y" using any_closest_point_dot[OF assms(1-4,5)] and any_closest_point_dot[OF assms(1-2,4,3,6)]
@@ -1634,7 +1632,7 @@
 subsection {* Various point-to-set separating/supporting hyperplane theorems. *}
 
 lemma supporting_hyperplane_closed_point:
-  fixes s :: "(real ^ _) set"
+  fixes z :: "'a::{real_inner,heine_borel}"
   assumes "convex s" "closed s" "s \<noteq> {}" "z \<notin> s"
   shows "\<exists>a b. \<exists>y\<in>s. inner a z < b \<and> (inner a y = b) \<and> (\<forall>x\<in>s. inner a x \<ge> b)"
 proof-
@@ -1653,7 +1651,7 @@
 qed
 
 lemma separating_hyperplane_closed_point:
-  fixes s :: "(real ^ _) set"
+  fixes z :: "'a::{real_inner,heine_borel}"
   assumes "convex s" "closed s" "z \<notin> s"
   shows "\<exists>a b. inner a z < b \<and> (\<forall>x\<in>s. inner a x > b)"
 proof(cases "s={}")