# HG changeset patch
# User huffman
# Date 1272550921 25200
# Node ID 2cdaae32b682fb58035008c1647211498af77282
# Parent  5610eb0b03b26c11e435b5563a5bdd41daecae9f
remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead

diff -r 5610eb0b03b2 -r 2cdaae32b682 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Apr 28 23:08:31 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Apr 29 07:22:01 2010 -0700
@@ -2205,14 +2205,6 @@
 
 subsection {* Use this to derive general bound property of convex function. *}
 
-lemma forall_of_pastecart:
-  "(\<forall>p. P (\<lambda>x. fstcart (p x)) (\<lambda>x. sndcart (p x))) \<longleftrightarrow> (\<forall>x y. P x y)" apply meson
-  apply(erule_tac x="\<lambda>a. pastecart (x a) (y a)" in allE) unfolding o_def by auto
-
-lemma forall_of_pastecart':
-  "(\<forall>p. P (fstcart p) (sndcart p)) \<longleftrightarrow> (\<forall>x y. P x y)" apply meson
-  apply(erule_tac x="pastecart x y" in allE) unfolding o_def by auto
-
 (* TODO: move *)
 lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
 by (cases "finite A", induct set: finite, simp_all)
diff -r 5610eb0b03b2 -r 2cdaae32b682 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Apr 28 23:08:31 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Apr 29 07:22:01 2010 -0700
@@ -1896,77 +1896,6 @@
   apply (auto simp add: vec_add)
   done
 
-text{* Pasting vectors. *}
-
-lemma linear_fstcart[intro]: "linear fstcart"
-  by (auto simp add: linear_def Cart_eq)
-
-lemma linear_sndcart[intro]: "linear sndcart"
-  by (auto simp add: linear_def Cart_eq)
-
-lemma fstcart_vec[simp]: "fstcart(vec x) = vec x"
-  by (simp add: Cart_eq)
-
-lemma fstcart_add[simp]:"fstcart(x + y) = fstcart (x::'a::{plus,times}^('b::finite + 'c::finite)) + fstcart y"
-  by (simp add: Cart_eq)
-
-lemma fstcart_cmul[simp]:"fstcart(c*s x) = c*s fstcart (x::'a::{plus,times}^('b::finite + 'c::finite))"
-  by (simp add: Cart_eq)
-
-lemma fstcart_neg[simp]:"fstcart(- x) = - fstcart (x::'a::ring_1^(_ + _))"
-  by (simp add: Cart_eq)
-
-lemma fstcart_sub[simp]:"fstcart(x - y) = fstcart (x::'a::ring_1^(_ + _)) - fstcart y"
-  by (simp add: Cart_eq)
-
-lemma fstcart_setsum:
-  fixes f:: "'d \<Rightarrow> 'a::semiring_1^_"
-  assumes fS: "finite S"
-  shows "fstcart (setsum f S) = setsum (\<lambda>i. fstcart (f i)) S"
-  by (induct rule: finite_induct[OF fS], simp_all add: vec_0[symmetric] del: vec_0)
-
-lemma sndcart_vec[simp]: "sndcart(vec x) = vec x"
-  by (simp add: Cart_eq)
-
-lemma sndcart_add[simp]:"sndcart(x + y) = sndcart (x::'a::{plus,times}^(_ + _)) + sndcart y"
-  by (simp add: Cart_eq)
-
-lemma sndcart_cmul[simp]:"sndcart(c*s x) = c*s sndcart (x::'a::{plus,times}^(_ + _))"
-  by (simp add: Cart_eq)
-
-lemma sndcart_neg[simp]:"sndcart(- x) = - sndcart (x::'a::ring_1^(_ + _))"
-  by (simp add: Cart_eq)
-
-lemma sndcart_sub[simp]:"sndcart(x - y) = sndcart (x::'a::ring_1^(_ + _)) - sndcart y"
-  by (simp add: Cart_eq)
-
-lemma sndcart_setsum:
-  fixes f:: "'d \<Rightarrow> 'a::semiring_1^_"
-  assumes fS: "finite S"
-  shows "sndcart (setsum f S) = setsum (\<lambda>i. sndcart (f i)) S"
-  by (induct rule: finite_induct[OF fS], simp_all add: vec_0[symmetric] del: vec_0)
-
-lemma pastecart_vec[simp]: "pastecart (vec x) (vec x) = vec x"
-  by (simp add: pastecart_eq)
-
-lemma pastecart_add[simp]:"pastecart (x1::'a::{plus,times}^_) y1 + pastecart x2 y2 = pastecart (x1 + x2) (y1 + y2)"
-  by (simp add: pastecart_eq)
-
-lemma pastecart_cmul[simp]: "pastecart (c *s (x1::'a::{plus,times}^_)) (c *s y1) = c *s pastecart x1 y1"
-  by (simp add: pastecart_eq)
-
-lemma pastecart_neg[simp]: "pastecart (- (x::'a::ring_1^_)) (- y) = - pastecart x y"
-  unfolding vector_sneg_minus1 pastecart_cmul ..
-
-lemma pastecart_sub: "pastecart (x1::'a::ring_1^_) y1 - pastecart x2 y2 = pastecart (x1 - x2) (y1 - y2)"
-  by (simp add: diff_def pastecart_neg[symmetric] del: pastecart_neg)
-
-lemma pastecart_setsum:
-  fixes f:: "'d \<Rightarrow> 'a::semiring_1^_"
-  assumes fS: "finite S"
-  shows "pastecart (setsum f S) (setsum g S) = setsum (\<lambda>i. pastecart (f i) (g i)) S"
-  by (simp  add: pastecart_eq fstcart_setsum[OF fS] sndcart_setsum[OF fS])
-
 lemma setsum_Plus:
   "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow>
     (\<Sum>x\<in>A <+> B. g x) = (\<Sum>x\<in>A. g (Inl x)) + (\<Sum>x\<in>B. g (Inr x))"
@@ -1980,39 +1909,6 @@
   apply (rule setsum_Plus [OF finite finite])
   done
 
-lemma norm_fstcart: "norm(fstcart x) <= norm (x::real ^('n::finite + 'm::finite))"
-proof-
-  have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"
-    by simp
-  have th1: "fstcart x \<bullet> fstcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"
-    by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg)
-  then show ?thesis
-    unfolding th0
-    unfolding norm_eq_sqrt_inner real_sqrt_le_iff id_def
-    by (simp add: inner_vector_def)
-qed
-
-lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y"
-  unfolding dist_norm by (metis fstcart_sub[symmetric] norm_fstcart)
-
-lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))"
-proof-
-  have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"
-    by simp
-  have th1: "sndcart x \<bullet> sndcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"
-    by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg)
-  then show ?thesis
-    unfolding th0
-    unfolding norm_eq_sqrt_inner real_sqrt_le_iff id_def
-    by (simp add: inner_vector_def)
-qed
-
-lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y"
-  unfolding dist_norm by (metis sndcart_sub[symmetric] norm_sndcart)
-
-lemma dot_pastecart: "(pastecart (x1::real^'n) (x2::real^'m)) \<bullet> (pastecart y1 y2) =  x1 \<bullet> y1 + x2 \<bullet> y2"
-  by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def)
-
 text {* TODO: move to NthRoot *}
 lemma sqrt_add_le_add_sqrt:
   assumes x: "0 \<le> x" and y: "0 \<le> y"
@@ -2023,10 +1919,6 @@
 apply (simp add: add_nonneg_nonneg x y)
 done
 
-lemma norm_pastecart: "norm (pastecart x y) <= norm x + norm y"
-  unfolding norm_vector_def setL2_def setsum_UNIV_sum
-  by (simp add: sqrt_add_le_add_sqrt setsum_nonneg)
-
 subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}
 
 definition hull :: "'a set set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75) where
diff -r 5610eb0b03b2 -r 2cdaae32b682 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Apr 28 23:08:31 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Apr 29 07:22:01 2010 -0700
@@ -53,46 +53,4 @@
 lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g"
   by (simp add: Cart_eq)
 
-text{* A non-standard sum to "paste" Cartesian products. *}
-
-definition "pastecart f g = (\<chi> i. case i of Inl a \<Rightarrow> f$a | Inr b \<Rightarrow> g$b)"
-definition "fstcart f = (\<chi> i. (f$(Inl i)))"
-definition "sndcart f = (\<chi> i. (f$(Inr i)))"
-
-lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a"
-  unfolding pastecart_def by simp
-
-lemma nth_pastecart_Inr [simp]: "pastecart f g $ Inr b = g$b"
-  unfolding pastecart_def by simp
-
-lemma nth_fstcart [simp]: "fstcart f $ i = f $ Inl i"
-  unfolding fstcart_def by simp
-
-lemma nth_sndtcart [simp]: "sndcart f $ i = f $ Inr i"
-  unfolding sndcart_def by simp
-
-lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr"
-  apply auto
-  apply (case_tac x)
-   apply auto
-  done
-
-lemma fstcart_pastecart[simp]: "fstcart (pastecart x y) = x"
-  by (simp add: Cart_eq)
-
-lemma sndcart_pastecart[simp]: "sndcart (pastecart x y) = y"
-  by (simp add: Cart_eq)
-
-lemma pastecart_fst_snd[simp]: "pastecart (fstcart z) (sndcart z) = z"
-  by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split)
-
-lemma pastecart_eq: "(x = y) \<longleftrightarrow> (fstcart x = fstcart y) \<and> (sndcart x = sndcart y)"
-  using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis
-
-lemma forall_pastecart: "(\<forall>p. P p) \<longleftrightarrow> (\<forall>x y. P (pastecart x y))"
-  by (metis pastecart_fst_snd)
-
-lemma exists_pastecart: "(\<exists>p. P p) \<longleftrightarrow> (\<exists>x y. P (pastecart x y))"
-  by (metis pastecart_fst_snd)
-
 end
diff -r 5610eb0b03b2 -r 2cdaae32b682 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Apr 28 23:08:31 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Apr 29 07:22:01 2010 -0700
@@ -4292,18 +4292,6 @@
 
 subsection {* Pasted sets *}
 
-lemma bounded_pastecart:
-  fixes s :: "('a::real_normed_vector ^ _) set" (* FIXME: generalize to metric_space *)
-  assumes "bounded s" "bounded t"
-  shows "bounded { pastecart x y | x y . (x \<in> s \<and> y \<in> t)}"
-proof-
-  obtain a b where ab:"\<forall>x\<in>s. norm x \<le> a" "\<forall>x\<in>t. norm x \<le> b" using assms[unfolded bounded_iff] by auto
-  { fix x y assume "x\<in>s" "y\<in>t"
-    hence "norm x \<le> a" "norm y \<le> b" using ab by auto
-    hence "norm (pastecart x y) \<le> a + b" using norm_pastecart[of x y] by auto }
-  thus ?thesis unfolding bounded_iff by auto
-qed
-
 lemma bounded_Times:
   assumes "bounded s" "bounded t" shows "bounded (s \<times> t)"
 proof-
@@ -4314,33 +4302,6 @@
   thus ?thesis unfolding bounded_any_center [where a="(x, y)"] by auto
 qed
 
-lemma closed_pastecart:
-  fixes s :: "(real ^ 'a) set" (* FIXME: generalize *)
-  assumes "closed s"  "closed t"
-  shows "closed {pastecart x y | x y . x \<in> s \<and> y \<in> t}"
-proof-
-  { fix x l assume as:"\<forall>n::nat. x n \<in> {pastecart x y |x y. x \<in> s \<and> y \<in> t}"  "(x ---> l) sequentially"
-    { fix n::nat have "fstcart (x n) \<in> s" "sndcart (x n) \<in> t" using as(1)[THEN spec[where x=n]] by auto } note * = this
-    moreover
-    { fix e::real assume "e>0"
-      then obtain N::nat where N:"\<forall>n\<ge>N. dist (x n) l < e" using as(2)[unfolded Lim_sequentially, THEN spec[where x=e]] by auto
-      { fix n::nat assume "n\<ge>N"
-        hence "dist (fstcart (x n)) (fstcart l) < e" "dist (sndcart (x n)) (sndcart l) < e"
-          using N[THEN spec[where x=n]] dist_fstcart[of "x n" l] dist_sndcart[of "x n" l] by auto   }
-      hence "\<exists>N. \<forall>n\<ge>N. dist (fstcart (x n)) (fstcart l) < e" "\<exists>N. \<forall>n\<ge>N. dist (sndcart (x n)) (sndcart l) < e" by auto  }
-    ultimately have "fstcart l \<in> s" "sndcart l \<in> t"
-      using assms(1)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. fstcart (x n)"], THEN spec[where x="fstcart l"]]
-      using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. sndcart (x n)"], THEN spec[where x="sndcart l"]]
-      unfolding Lim_sequentially by auto
-    hence "l \<in> {pastecart x y |x y. x \<in> s \<and> y \<in> t}" apply- unfolding mem_Collect_eq apply(rule_tac x="fstcart l" in exI,rule_tac x="sndcart l" in exI) by auto }
-  thus ?thesis unfolding closed_sequential_limits by blast
-qed
-
-lemma compact_pastecart:
-  fixes s t :: "(real ^ _) set"
-  shows "compact s \<Longrightarrow> compact t ==> compact {pastecart x y | x y . x \<in> s \<and> y \<in> t}"
-  unfolding compact_eq_bounded_closed using bounded_pastecart[of s t] closed_pastecart[of s t] by auto
-
 lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B"
 by (induct x) simp