# HG changeset patch
# User himmelma
# Date 1244558313 -7200
# Node ID feaf9071f8b9b59cf133cd9e670abd3ecd7a1571
# Parent  fed8a95f54dbd095ab2283238f22d57c59af7913
removed duplicate lemmas

diff -r fed8a95f54db -r feaf9071f8b9 src/HOL/Library/Convex_Euclidean_Space.thy
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 09 12:05:22 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 09 16:38:33 2009 +0200
@@ -50,9 +50,6 @@
         "setsum (\<lambda>y. if (x = y) then P y else Q y) s = setsum Q s"
   apply(rule_tac [!] setsum_cong2) using assms by auto
 
-lemma setsum_diff1'':assumes "finite A" "a \<in> A"
-  shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)" unfolding setsum_diff1'[OF assms] by auto
-
 lemma setsum_delta'': fixes s::"(real^'n) set" assumes "finite s"
   shows "(\<Sum>x\<in>s. (if y = x then f x else 0) *s x) = (if y\<in>s then (f y) *s y else 0)"
 proof-
@@ -64,34 +61,6 @@
 
 lemma if_smult:"(if P then x else (y::real)) *s v = (if P then x *s v else y *s v)" by auto
 
-lemma ex_bij_betw_nat_finite_1:
-  assumes "finite M"
-  shows "\<exists>h. bij_betw h {1 .. card M} M"
-proof-
-  obtain h where h:"bij_betw h {0..<card M} M" using ex_bij_betw_nat_finite[OF assms] by auto
-  let ?h = "h \<circ> (\<lambda>i. i - 1)"
-  have *:"(\<lambda>i. i - 1) ` {1..card M} = {0..<card M}" apply auto  unfolding image_iff apply(rule_tac x="Suc x" in bexI) by auto
-  hence "?h ` {1..card M} = h ` {0..<card M}" unfolding image_compose by auto 
-  hence "?h ` {1..card M} = M" unfolding image_compose using h unfolding * unfolding bij_betw_def by auto
-  moreover
-  have "inj_on (\<lambda>i. i - Suc 0) {Suc 0..card M}" unfolding inj_on_def by auto
-  hence "inj_on ?h {1..card M}" apply(rule_tac comp_inj_on) unfolding * using h[unfolded bij_betw_def] by auto
-  ultimately show ?thesis apply(rule_tac x="h \<circ> (\<lambda>i. i - 1)" in exI) unfolding o_def and bij_betw_def by auto
-qed
-
-lemma finite_subset_image:
-  assumes "B \<subseteq> f ` A" "finite B"
-  shows "\<exists>C\<subseteq>A. finite C \<and> B = f ` C"
-proof- from assms(1) have "\<forall>x\<in>B. \<exists>y\<in>A. x = f y" by auto
-  then obtain c where "\<forall>x\<in>B. c x \<in> A \<and> x = f (c x)"
-    using bchoice[of B "\<lambda>x y. y\<in>A \<and> x = f y"] by auto
-  thus ?thesis apply(rule_tac x="c ` B" in exI) using assms(2) by auto qed
-
-lemma inj_on_image_eq_iff: assumes "inj_on f (A \<union> B)"
-  shows "f ` A = f ` B \<longleftrightarrow> A = B"
-  using assms by(blast dest: inj_onD)
-
-
 lemma mem_interval_1: fixes x :: "real^1" shows
  "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
  "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
@@ -559,7 +528,7 @@
   have "s \<noteq> {v}" using as(3,6) by auto
   thus "\<exists>x\<in>p. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p - {x} \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *s v) = x" 
     apply(rule_tac x=v in bexI, rule_tac x="s - {v}" in exI, rule_tac x="\<lambda>x. - (1 / u v) * u x" in exI)
-    unfolding vector_smult_assoc[THEN sym] and setsum_cmul unfolding setsum_right_distrib[THEN sym] and setsum_diff1''[OF as(1,5)] using as by auto
+    unfolding vector_smult_assoc[THEN sym] and setsum_cmul unfolding setsum_right_distrib[THEN sym] and setsum_diff1_ring[OF as(1,5)] using as by auto
 qed
 
 lemma affine_dependent_explicit_finite:
@@ -1682,7 +1651,7 @@
     apply(rule compact_imp_fip) apply(rule compact_frontier[OF compact_cball])
     defer apply(rule,rule,erule conjE) proof-
     fix f assume as:"f \<subseteq> ?k ` s" "finite f"
-    obtain c where c:"f = ?k ` c" "c\<subseteq>s" "finite c" using finite_subset_image[OF as] by auto
+    obtain c where c:"f = ?k ` c" "c\<subseteq>s" "finite c" using finite_subset_image[OF as(2,1)] by auto
     then obtain a b where ab:"a \<noteq> 0" "0 < b"  "\<forall>x\<in>convex hull c. b < a \<bullet> x"
       using separating_hyperplane_closed_0[OF convex_convex_hull, of c]
       using finite_imp_compact_convex_hull[OF c(3), THEN compact_imp_closed] and assms(2)
@@ -1867,7 +1836,7 @@
     have "m \<subseteq> X ` f" "p \<subseteq> X ` f" using mp(2) by auto
     then obtain g h where gh:"m = X ` g" "p = X ` h" "g \<subseteq> f" "h \<subseteq> f" unfolding subset_image_iff by auto 
     hence "f \<union> (g \<union> h) = f" by auto
-    hence f:"f = g \<union> h" using inj_on_image_eq_iff[of X f "g \<union> h"] and True
+    hence f:"f = g \<union> h" using inj_on_Un_image_eq_iff[of X f "g \<union> h"] and True
       unfolding mp(2)[unfolded image_Un[THEN sym] gh] by auto
     have *:"g \<inter> h = {}" using mp(1) unfolding gh using inj_on_image_Int[OF True gh(3,4)] by auto
     have "convex hull (X ` h) \<subseteq> \<Inter> g" "convex hull (X ` g) \<subseteq> \<Inter> h"
diff -r fed8a95f54db -r feaf9071f8b9 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Tue Jun 09 12:05:22 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Tue Jun 09 16:38:33 2009 +0200
@@ -1412,51 +1412,6 @@
 (* FIXME : Problem thm setsum_vmul[of _ "f:: 'a \<Rightarrow> real ^'n"]  ---
  Get rid of *s and use real_vector instead! Also prove that ^ creates a real_vector !! *)
 
-lemma setsum_add_split: assumes mn: "(m::nat) \<le> n + 1"
-  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"
-proof-
-  let ?A = "{m .. n}"
-  let ?B = "{n + 1 .. n + p}"
-  have eq: "{m .. n+p} = ?A \<union> ?B" using mn by auto
-  have d: "?A \<inter> ?B = {}" by auto
-  from setsum_Un_disjoint[of "?A" "?B" f] eq d show ?thesis by auto
-qed
-
-lemma setsum_natinterval_left:
-  assumes mn: "(m::nat) <= n"
-  shows "setsum f {m..n} = f m + setsum f {m + 1..n}"
-proof-
-  from mn have "{m .. n} = insert m {m+1 .. n}" by auto
-  then show ?thesis by auto
-qed
-
-lemma setsum_natinterval_difff:
-  fixes f:: "nat \<Rightarrow> ('a::ab_group_add)"
-  shows  "setsum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} =
-          (if m <= n then f m - f(n + 1) else 0)"
-by (induct n, auto simp add: ring_simps not_le le_Suc_eq)
-
-lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]
-
-lemma setsum_setsum_restrict:
-  "finite S \<Longrightarrow> finite T \<Longrightarrow> setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y\<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T"
-  apply (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)
-  by (rule setsum_commute)
-
-lemma setsum_image_gen: assumes fS: "finite S"
-  shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
-proof-
-  {fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto}
-  note th0 = this
-  have "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
-    apply (rule setsum_cong2)
-    by (simp add: th0)
-  also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
-    apply (rule setsum_setsum_restrict[OF fS])
-    by (rule finite_imageI[OF fS])
-  finally show ?thesis .
-qed
-
     (* FIXME: Here too need stupid finiteness assumption on T!!! *)
 lemma setsum_group:
   assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"