--- 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"
--- 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"