author hoelzl Thu, 26 May 2011 14:12:03 +0200 changeset 42986 11fd8c04ea24 parent 42985 1fb670792708 child 42987 73e2d802ea41
generalize setsum_cases
 src/HOL/Big_Operators.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Big_Operators.thy	Thu May 26 14:12:02 2011 +0200
+++ b/src/HOL/Big_Operators.thy	Thu May 26 14:12:03 2011 +0200
@@ -28,6 +28,34 @@
"\<not> finite A \<Longrightarrow> F g A = 1"

+lemma F_cong:
+  assumes "A = B" "\<And>x. x \<in> B \<Longrightarrow> h x = g x"
+  shows "F h A = F g B"
+proof cases
+  assume "finite A"
+  with assms show ?thesis unfolding `A = B` by (simp cong: cong)
+next
+  assume "\<not> finite A"
+  then show ?thesis unfolding `A = B` by simp
+qed
+
+lemma If_cases:
+  fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
+  assumes fA: "finite A"
+  shows "F (\<lambda>x. if P x then h x else g x) A =
+         F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
+proof-
+  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> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
+  let ?g = "\<lambda>x. if P x then h x else g x"
+  from union_disjoint[OF f a(2), of ?g] a(1)
+  show ?thesis
+    by (subst (1 2) F_cong) simp_all
+qed
+
end

text {* for ad-hoc proofs for @{const fold_image} *}
@@ -268,17 +296,7 @@
assumes fA: "finite A"
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> {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> {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
-
+  using setsum.If_cases[OF fA] .

(*But we can't get rid of finite I. If infinite, although the rhs is 0,
the lhs need not be, since UNION I A could still be finite.*)```