removed duplicate lemmas
authorhimmelma
Tue Jun 09 16:38:33 2009 +0200 (2009-06-09)
changeset 31518feaf9071f8b9
parent 31514 fed8a95f54db
child 31519 77b56af5ccbf
removed duplicate lemmas
src/HOL/Library/Convex_Euclidean_Space.thy
src/HOL/Library/Euclidean_Space.thy
     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"