# HG changeset patch
# User huffman
# Date 1244673122 25200
# Node ID a5e168fd2bb9f05c08f8b7d2d184dbecd3428287
# Parent  88347c12e2674d1dbf445e8344e3893b4eccaf45
rewrite proof of compact_convex_combinations to avoid pastecart and vec1

diff -r 88347c12e267 -r a5e168fd2bb9 src/HOL/Library/Convex_Euclidean_Space.thy
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Wed Jun 10 15:29:05 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Wed Jun 10 15:32:02 2009 -0700
@@ -1227,32 +1227,68 @@
 lemma continuous_dest_vec1: "continuous net f \<Longrightarrow> continuous net (\<lambda>x. dest_vec1 (f x))"
   unfolding continuous_def by (rule tendsto_dest_vec1)
 
+lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B"
+by (induct x) simp
+
+(* TODO: move *)
+lemma compact_Times: "compact s \<Longrightarrow> compact t \<Longrightarrow> compact (s \<times> t)"
+unfolding compact_def
+apply clarify
+apply (drule_tac x="fst \<circ> f" in spec)
+apply (drule mp, simp add: mem_Times_iff)
+apply (clarify, rename_tac l1 r1)
+apply (drule_tac x="snd \<circ> f \<circ> r1" in spec)
+apply (drule mp, simp add: mem_Times_iff)
+apply (clarify, rename_tac l2 r2)
+apply (rule_tac x="(l1, l2)" in rev_bexI, simp)
+apply (rule_tac x="r1 \<circ> r2" in exI)
+apply (rule conjI, simp add: subseq_def)
+apply (drule_tac r=r2 in lim_subseq [COMP swap_prems_rl], assumption)
+apply (drule (1) tendsto_Pair) back
+apply (simp add: o_def)
+done
+
+(* TODO: move *)
+lemma compact_real_interval:
+  fixes a b :: real shows "compact {a..b}"
+proof -
+  have "continuous_on {vec1 a .. vec1 b} dest_vec1"
+    unfolding continuous_on
+    by (simp add: tendsto_dest_vec1 Lim_at_within Lim_ident_at)
+  moreover have "compact {vec1 a .. vec1 b}" by (rule compact_interval)
+  ultimately have "compact (dest_vec1 ` {vec1 a .. vec1 b})"
+    by (rule compact_continuous_image)
+  also have "dest_vec1 ` {vec1 a .. vec1 b} = {a..b}"
+    by (auto simp add: image_def Bex_def exists_vec1)
+  finally show ?thesis .
+qed
+
 lemma compact_convex_combinations:
   fixes s t :: "(real ^ 'n::finite) set"
   assumes "compact s" "compact t"
   shows "compact { (1 - u) *s x + u *s y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t}"
 proof-
-  let ?X = "{ pastecart u w | u w. u \<in> {vec1 0 .. vec1 1} \<and> w \<in> { pastecart x y |x y. x \<in> s \<and> y \<in> t} }"
-  let ?h = "(\<lambda>z. (1 - dest_vec1(fstcart z)) *s fstcart(sndcart z) + dest_vec1(fstcart z) *s sndcart(sndcart z))"
+  let ?X = "{0..1} \<times> s \<times> t"
+  let ?h = "(\<lambda>z. (1 - fst z) *s fst (snd z) + fst z *s snd (snd z))"
   have *:"{ (1 - u) *s x + u *s y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t} = ?h ` ?X"
-    apply(rule set_ext) unfolding image_iff mem_Collect_eq unfolding mem_interval_1 vec1_dest_vec1
-    apply rule apply auto apply(rule_tac x="pastecart (vec1 u) (pastecart xa y)" in exI) apply simp
-    apply(rule_tac x="vec1 u" in exI) apply(rule_tac x="pastecart xa y" in exI) by auto 
-  { fix u::"real^1" fix x y assume as:"0 \<le> dest_vec1 u" "dest_vec1 u \<le> 1" "x \<in> s" "y \<in> t"
-    hence "continuous (at (pastecart u (pastecart x y)))
-           (\<lambda>z. fstcart (sndcart z) - dest_vec1 (fstcart z) *s fstcart (sndcart z) +
-                dest_vec1 (fstcart z) *s sndcart (sndcart z))"
-      apply (auto intro!: continuous_add continuous_sub continuous_mul continuous_dest_vec1
-                  simp add: o_def vec1_dest_vec1)
-      using linear_continuous_at linear_fstcart linear_sndcart linear_sndcart
-      using linear_compose[unfolded o_def] by auto  }
-  hence "continuous_on {pastecart u w |u w. u \<in> {vec1 0..vec1 1} \<and> w \<in> {pastecart x y |x y. x \<in> s \<and> y \<in> t}}
-     (\<lambda>z. (1 - dest_vec1 (fstcart z)) *s fstcart (sndcart z) + dest_vec1 (fstcart z) *s sndcart (sndcart z))"
-    apply(rule_tac continuous_at_imp_continuous_on) unfolding mem_Collect_eq
-    unfolding mem_interval_1 vec1_dest_vec1 by auto
+    apply(rule set_ext) unfolding image_iff mem_Collect_eq
+    apply rule apply auto
+    apply (rule_tac x=u in rev_bexI, simp)
+    apply (erule rev_bexI, erule rev_bexI, simp)
+    by auto
+  { fix u::"real" fix x y assume as:"0 \<le> u" "u \<le> 1" "x \<in> s" "y \<in> t"
+    hence "continuous (at (u, x, y))
+           (\<lambda>z. fst (snd z) - fst z *s fst (snd z) + fst z *s snd (snd z))"
+      apply (auto intro!: continuous_add continuous_sub continuous_mul)
+      unfolding continuous_at
+      by (safe intro!: tendsto_fst tendsto_snd Lim_at_id [unfolded id_def])
+  }
+  hence "continuous_on ({0..1} \<times> s \<times> t)
+     (\<lambda>z. (1 - fst z) *s fst (snd z) + fst z *s snd (snd z))"
+    apply(rule_tac continuous_at_imp_continuous_on) by auto
  thus ?thesis unfolding * apply(rule compact_continuous_image)
-    defer apply(rule compact_pastecart) defer apply(rule compact_pastecart)
-    using compact_interval assms by auto
+    defer apply(rule compact_Times) defer apply(rule compact_Times)
+    using compact_real_interval assms by auto
 qed
 
 lemma compact_convex_hull: fixes s::"(real^'n::finite) set"