author himmelma Tue Jun 09 16:38:33 2009 +0200 (2009-06-09) changeset 31518 feaf9071f8b9 parent 31514 fed8a95f54db child 31519 77b56af5ccbf
removed duplicate lemmas
```     1.1 --- a/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 09 12:05:22 2009 +0200
1.2 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 09 16:38:33 2009 +0200
1.3 @@ -50,9 +50,6 @@
1.4          "setsum (\<lambda>y. if (x = y) then P y else Q y) s = setsum Q s"
1.5    apply(rule_tac [!] setsum_cong2) using assms by auto
1.6
1.7 -lemma setsum_diff1'':assumes "finite A" "a \<in> A"
1.8 -  shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)" unfolding setsum_diff1'[OF assms] by auto
1.9 -
1.10  lemma setsum_delta'': fixes s::"(real^'n) set" assumes "finite s"
1.11    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)"
1.12  proof-
1.13 @@ -64,34 +61,6 @@
1.14
1.15  lemma if_smult:"(if P then x else (y::real)) *s v = (if P then x *s v else y *s v)" by auto
1.16
1.17 -lemma ex_bij_betw_nat_finite_1:
1.18 -  assumes "finite M"
1.19 -  shows "\<exists>h. bij_betw h {1 .. card M} M"
1.20 -proof-
1.21 -  obtain h where h:"bij_betw h {0..<card M} M" using ex_bij_betw_nat_finite[OF assms] by auto
1.22 -  let ?h = "h \<circ> (\<lambda>i. i - 1)"
1.23 -  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
1.24 -  hence "?h ` {1..card M} = h ` {0..<card M}" unfolding image_compose by auto
1.25 -  hence "?h ` {1..card M} = M" unfolding image_compose using h unfolding * unfolding bij_betw_def by auto
1.26 -  moreover
1.27 -  have "inj_on (\<lambda>i. i - Suc 0) {Suc 0..card M}" unfolding inj_on_def by auto
1.28 -  hence "inj_on ?h {1..card M}" apply(rule_tac comp_inj_on) unfolding * using h[unfolded bij_betw_def] by auto
1.29 -  ultimately show ?thesis apply(rule_tac x="h \<circ> (\<lambda>i. i - 1)" in exI) unfolding o_def and bij_betw_def by auto
1.30 -qed
1.31 -
1.32 -lemma finite_subset_image:
1.33 -  assumes "B \<subseteq> f ` A" "finite B"
1.34 -  shows "\<exists>C\<subseteq>A. finite C \<and> B = f ` C"
1.35 -proof- from assms(1) have "\<forall>x\<in>B. \<exists>y\<in>A. x = f y" by auto
1.36 -  then obtain c where "\<forall>x\<in>B. c x \<in> A \<and> x = f (c x)"
1.37 -    using bchoice[of B "\<lambda>x y. y\<in>A \<and> x = f y"] by auto
1.38 -  thus ?thesis apply(rule_tac x="c ` B" in exI) using assms(2) by auto qed
1.39 -
1.40 -lemma inj_on_image_eq_iff: assumes "inj_on f (A \<union> B)"
1.41 -  shows "f ` A = f ` B \<longleftrightarrow> A = B"
1.42 -  using assms by(blast dest: inj_onD)
1.43 -
1.44 -
1.45  lemma mem_interval_1: fixes x :: "real^1" shows
1.46   "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
1.47   "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
1.48 @@ -559,7 +528,7 @@
1.49    have "s \<noteq> {v}" using as(3,6) by auto
1.50    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"
1.51      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)
1.52 -    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
1.53 +    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
1.54  qed
1.55
1.56  lemma affine_dependent_explicit_finite:
1.57 @@ -1682,7 +1651,7 @@
1.58      apply(rule compact_imp_fip) apply(rule compact_frontier[OF compact_cball])
1.59      defer apply(rule,rule,erule conjE) proof-
1.60      fix f assume as:"f \<subseteq> ?k ` s" "finite f"
1.61 -    obtain c where c:"f = ?k ` c" "c\<subseteq>s" "finite c" using finite_subset_image[OF as] by auto
1.62 +    obtain c where c:"f = ?k ` c" "c\<subseteq>s" "finite c" using finite_subset_image[OF as(2,1)] by auto
1.63      then obtain a b where ab:"a \<noteq> 0" "0 < b"  "\<forall>x\<in>convex hull c. b < a \<bullet> x"
1.64        using separating_hyperplane_closed_0[OF convex_convex_hull, of c]
1.65        using finite_imp_compact_convex_hull[OF c(3), THEN compact_imp_closed] and assms(2)
1.66 @@ -1867,7 +1836,7 @@
1.67      have "m \<subseteq> X ` f" "p \<subseteq> X ` f" using mp(2) by auto
1.68      then obtain g h where gh:"m = X ` g" "p = X ` h" "g \<subseteq> f" "h \<subseteq> f" unfolding subset_image_iff by auto
1.69      hence "f \<union> (g \<union> h) = f" by auto
1.70 -    hence f:"f = g \<union> h" using inj_on_image_eq_iff[of X f "g \<union> h"] and True
1.71 +    hence f:"f = g \<union> h" using inj_on_Un_image_eq_iff[of X f "g \<union> h"] and True
1.72        unfolding mp(2)[unfolded image_Un[THEN sym] gh] by auto
1.73      have *:"g \<inter> h = {}" using mp(1) unfolding gh using inj_on_image_Int[OF True gh(3,4)] by auto
1.74      have "convex hull (X ` h) \<subseteq> \<Inter> g" "convex hull (X ` g) \<subseteq> \<Inter> h"
```
```     2.1 --- a/src/HOL/Library/Euclidean_Space.thy	Tue Jun 09 12:05:22 2009 +0200
2.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Tue Jun 09 16:38:33 2009 +0200
2.3 @@ -1412,51 +1412,6 @@
2.4  (* FIXME : Problem thm setsum_vmul[of _ "f:: 'a \<Rightarrow> real ^'n"]  ---
2.5   Get rid of *s and use real_vector instead! Also prove that ^ creates a real_vector !! *)
2.6
2.7 -lemma setsum_add_split: assumes mn: "(m::nat) \<le> n + 1"
2.8 -  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"
2.9 -proof-
2.10 -  let ?A = "{m .. n}"
2.11 -  let ?B = "{n + 1 .. n + p}"
2.12 -  have eq: "{m .. n+p} = ?A \<union> ?B" using mn by auto
2.13 -  have d: "?A \<inter> ?B = {}" by auto
2.14 -  from setsum_Un_disjoint[of "?A" "?B" f] eq d show ?thesis by auto
2.15 -qed
2.16 -
2.17 -lemma setsum_natinterval_left:
2.18 -  assumes mn: "(m::nat) <= n"
2.19 -  shows "setsum f {m..n} = f m + setsum f {m + 1..n}"
2.20 -proof-
2.21 -  from mn have "{m .. n} = insert m {m+1 .. n}" by auto
2.22 -  then show ?thesis by auto
2.23 -qed
2.24 -
2.25 -lemma setsum_natinterval_difff:
2.26 -  fixes f:: "nat \<Rightarrow> ('a::ab_group_add)"
2.27 -  shows  "setsum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} =
2.28 -          (if m <= n then f m - f(n + 1) else 0)"
2.29 -by (induct n, auto simp add: ring_simps not_le le_Suc_eq)
2.30 -
2.31 -lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]
2.32 -
2.33 -lemma setsum_setsum_restrict:
2.34 -  "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"
2.35 -  apply (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)
2.36 -  by (rule setsum_commute)
2.37 -
2.38 -lemma setsum_image_gen: assumes fS: "finite S"
2.39 -  shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
2.40 -proof-
2.41 -  {fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto}
2.42 -  note th0 = this
2.43 -  have "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
2.44 -    apply (rule setsum_cong2)
2.45 -    by (simp add: th0)
2.46 -  also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
2.47 -    apply (rule setsum_setsum_restrict[OF fS])
2.48 -    by (rule finite_imageI[OF fS])
2.49 -  finally show ?thesis .
2.50 -qed
2.51 -
2.52      (* FIXME: Here too need stupid finiteness assumption on T!!! *)
2.53  lemma setsum_group:
2.54    assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
```