# HG changeset patch
# User huffman
# Date 1379003616 25200
# Node ID d29d63460d842216d4dd10904a9507f981a560a6
# Parent  5078034ade163a151be6c38f262b7dd5091d3366
new lemmas

diff -r 5078034ade16 -r d29d63460d84 src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Thu Sep 12 09:06:46 2013 -0700
+++ b/src/HOL/Library/Convex.thy	Thu Sep 12 09:33:36 2013 -0700
@@ -46,6 +46,12 @@
 lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"
   unfolding convex_def by auto
 
+lemma convex_INT: "\<forall>i\<in>A. convex (B i) \<Longrightarrow> convex (\<Inter>i\<in>A. B i)"
+  unfolding convex_def by auto
+
+lemma convex_Times: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<times> t)"
+  unfolding convex_def by auto
+
 lemma convex_halfspace_le: "convex {x. inner a x \<le> b}"
   unfolding convex_def
   by (auto simp: inner_add intro!: convex_bound_le)
diff -r 5078034ade16 -r d29d63460d84 src/HOL/Library/Set_Algebras.thy
--- a/src/HOL/Library/Set_Algebras.thy	Thu Sep 12 09:06:46 2013 -0700
+++ b/src/HOL/Library/Set_Algebras.thy	Thu Sep 12 09:33:36 2013 -0700
@@ -90,6 +90,11 @@
 lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
   by (auto simp add: set_plus_def)
 
+lemma set_plus_elim:
+  assumes "x \<in> A + B"
+  obtains a b where "x = a + b" and "a \<in> A" and "b \<in> B"
+  using assms unfolding set_plus_def by fast
+
 lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
   by (auto simp add: elt_set_plus_def)
 
@@ -201,6 +206,11 @@
 lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
   by (auto simp add: set_times_def)
 
+lemma set_times_elim:
+  assumes "x \<in> A * B"
+  obtains a b where "x = a * b" and "a \<in> A" and "b \<in> B"
+  using assms unfolding set_times_def by fast
+
 lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
   by (auto simp add: elt_set_times_def)
 
@@ -321,10 +331,20 @@
     - a : (- 1) *o C"
   by (auto simp add: elt_set_times_def)
 
-lemma set_plus_image:
-  fixes S T :: "'n::semigroup_add set" shows "S + T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
+lemma set_plus_image: "S + T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
   unfolding set_plus_def by (fastforce simp: image_iff)
 
+lemma set_times_image: "S * T = (\<lambda>(x, y). x * y) ` (S \<times> T)"
+  unfolding set_times_def by (fastforce simp: image_iff)
+
+lemma finite_set_plus:
+  assumes "finite s" and "finite t" shows "finite (s + t)"
+  using assms unfolding set_plus_image by simp
+
+lemma finite_set_times:
+  assumes "finite s" and "finite t" shows "finite (s * t)"
+  using assms unfolding set_times_image by simp
+
 lemma set_setsum_alt:
   assumes fin: "finite I"
   shows "setsum S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
diff -r 5078034ade16 -r d29d63460d84 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Sep 12 09:06:46 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Sep 12 09:33:36 2013 -0700
@@ -560,6 +560,9 @@
 lemma subset_hull: "S t \<Longrightarrow> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t"
   unfolding hull_def by blast
 
+lemma hull_UNIV: "S hull UNIV = UNIV"
+  unfolding hull_def by auto
+
 lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' \<Longrightarrow> t \<subseteq> t') \<Longrightarrow> (S hull s = t)"
   unfolding hull_def by auto