author hoelzl Thu, 04 Mar 2010 17:09:44 +0100 changeset 35577 43b93e294522 parent 35576 5f6bd3ac99f9 child 35578 384ad08a1d1b
Generalized setsum_cases
```--- a/src/HOL/Finite_Set.thy	Thu Mar 04 15:44:06 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Mar 04 17:09:44 2010 +0100
@@ -1278,14 +1278,15 @@

lemma setsum_cases:
assumes fA: "finite A"
-  shows "setsum (\<lambda>x. if x \<in> B then f x else g x) A =
-         setsum f (A \<inter> B) + setsum g (A \<inter> - B)"
+  shows "setsum (\<lambda>x. if P x then f x else g x) A =
+         setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
proof-
-  have a: "A = A \<inter> B \<union> A \<inter> -B" "(A \<inter> B) \<inter> (A \<inter> -B) = {}"
+  have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}"
+          "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}"
by blast+
from fA
-  have f: "finite (A \<inter> B)" "finite (A \<inter> -B)" by auto
-  let ?g = "\<lambda>x. if x \<in> B then f x else g x"
+  have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
+  let ?g = "\<lambda>x. if P x then f x else g x"
from setsum_Un_disjoint[OF f a(2), of ?g] a(1)
show ?thesis by simp
qed```
```--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Mar 04 15:44:06 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Mar 04 17:09:44 2010 +0100
@@ -342,8 +342,8 @@
apply(rule_tac x="insert a f" in exI)
apply(rule_tac x="\<lambda>x. if x=a then 1 - setsum (\<lambda>x. u (x - a)) f else u (x - a)" in exI)
using assms and f unfolding setsum_clauses(2)[OF f(1)] and if_smult
-    unfolding setsum_cases[OF f(1), of "{a}", unfolded singleton_iff] and *
-    by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps) qed
+    unfolding setsum_cases[OF f(1), of "\<lambda>x. x = a"]
+    by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps *) qed

lemma affine_hull_span:
fixes a :: "real ^ _"
@@ -492,7 +492,7 @@
fix t u assume as:"\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s" " finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
have *:"s \<inter> t = t" using as(3) by auto
show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" using as(1)[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]]
-    unfolding if_smult and setsum_cases[OF assms] and * using as(2-) by auto
+    unfolding if_smult and setsum_cases[OF assms] using as(2-) * by auto
qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)

subsection {* Cones. *}
@@ -890,7 +890,7 @@
show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" apply(rule)
apply(rule_tac x="k1 + k2" in exI, rule_tac x="\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)" in exI)
apply(rule_tac x="\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i - k1)" in exI) apply(rule,rule) defer apply(rule)
-    unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and setsum_reindex[OF inj] and o_def
+    unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and setsum_reindex[OF inj] and o_def Collect_mem_eq
unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] setsum_right_distrib[THEN sym] proof-
fix i assume i:"i \<in> {1..k1+k2}"
show "0 \<le> (if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)) \<and> (if i \<in> {1..k1} then x1 i else x2 (i - k1)) \<in> s"```