author chaieb Wed, 04 Mar 2009 19:21:55 +0000 changeset 30260 be39acd3ac85 parent 30259 11cb411913b4 child 30261 4db36ab8d1c4
Added general theorems for fold_image, setsum and set_prod
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Finite_Set.thy	Wed Mar 04 19:21:28 2009 +0000
+++ b/src/HOL/Finite_Set.thy	Wed Mar 04 19:21:55 2009 +0000
@@ -878,9 +878,54 @@
fold_image times g 1 A *  fold_image times h 1 A"
by (erule finite_induct) (simp_all add: mult_ac)

+lemma fold_image_related:
+  assumes Re: "R e e"
+  and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)"
+  and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
+  shows "R (fold_image (op *) h e S) (fold_image (op *) g e S)"
+  using fS by (rule finite_subset_induct) (insert assms, auto)
+
+lemma  fold_image_eq_general:
+  assumes fS: "finite S"
+  and h: "\<forall>y\<in>S'. \<exists>!x. x\<in> S \<and> h(x) = y"
+  and f12:  "\<forall>x\<in>S. h x \<in> S' \<and> f2(h x) = f1 x"
+  shows "fold_image (op *) f1 e S = fold_image (op *) f2 e S'"
+proof-
+  from h f12 have hS: "h ` S = S'" by auto
+  {fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y"
+    from f12 h H  have "x = y" by auto }
+  hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast
+  from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto
+  from hS have "fold_image (op *) f2 e S' = fold_image (op *) f2 e (h ` S)" by simp
+  also have "\<dots> = fold_image (op *) (f2 o h) e S"
+    using fold_image_reindex[OF fS hinj, of f2 e] .
+  also have "\<dots> = fold_image (op *) f1 e S " using th fold_image_cong[OF fS, of "f2 o h" f1 e]
+    by blast
+  finally show ?thesis ..
+qed
+
+lemma fold_image_eq_general_inverses:
+  assumes fS: "finite S"
+  and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
+  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x  \<and> g (h x) = f x"
+  shows "fold_image (op *) f e S = fold_image (op *) g e T"
+  (* metis solves it, but not yet available here *)
+  apply (rule fold_image_eq_general[OF fS, of T h g f e])
+  apply (rule ballI)
+  apply (frule kh)
+  apply (rule ex1I[])
+  apply blast
+  apply clarsimp
+  apply (drule hk) apply simp
+  apply (rule sym)
+  apply (erule conjunct1[OF conjunct2[OF hk]])
+  apply (rule ballI)
+  apply (drule  hk)
+  apply blast
+  done
+
end

-
subsection {* Generalized summation over a set *}

@@ -1092,6 +1137,31 @@
using setsum_delta[OF fS, of a b, symmetric]
by (auto intro: setsum_cong)

+lemma setsum_restrict_set:
+  assumes fA: "finite A"
+  shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
+proof-
+  from fA have fab: "finite (A \<inter> B)" by auto
+  have aba: "A \<inter> B \<subseteq> A" by blast
+  let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
+  from setsum_mono_zero_left[OF fA aba, of ?g]
+  show ?thesis by simp
+qed
+
+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)"
+proof-
+  have a: "A = A \<inter> B \<union> A \<inter> -B" "(A \<inter> B) \<inter> (A \<inter> -B) = {}"
+    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"
+  from setsum_Un_disjoint[OF f a(2), of ?g] a(1)
+  show ?thesis by simp
+qed
+

(*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.*)
@@ -1158,6 +1228,62 @@
setsum f A + setsum f B - setsum f (A Int B)"
by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)

+lemma (in comm_monoid_mult) fold_image_1: "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1"
+  apply (induct set: finite)
+  apply simp by (auto simp add: fold_image_insert)
+
+lemma (in comm_monoid_mult) fold_image_Un_one:
+  assumes fS: "finite S" and fT: "finite T"
+  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
+  shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
+proof-
+  have "fold_image op * f 1 (S \<inter> T) = 1"
+    apply (rule fold_image_1)
+    using fS fT I0 by auto
+  with fold_image_Un_Int[OF fS fT] show ?thesis by simp
+qed
+
+lemma setsum_eq_general_reverses:
+  assumes fS: "finite S" and fT: "finite T"
+  and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
+  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
+  shows "setsum f S = setsum g T"
+  apply (simp add: setsum_def fS fT)
+  apply (erule kh)
+  apply (erule hk)
+  done
+
+
+
+lemma setsum_Un_zero:
+  assumes fS: "finite S" and fT: "finite T"
+  and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
+  shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
+  using fS fT
+  using I0 by auto
+
+
+lemma setsum_UNION_zero:
+  assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
+  and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
+  shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
+  using fSS f0
+proof(induct rule: finite_induct[OF fS])
+  case 1 thus ?case by simp
+next
+  case (2 T F)
+  then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F"
+    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by (auto simp add: finite_insert)
+  from fTF have fUF: "finite (\<Union>F)" by (auto intro: finite_Union)
+  from "2.prems" TF fTF
+  show ?case
+    by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
+qed
+
+
lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
(if a:A then setsum f A - f a else setsum f A)"
apply (case_tac "finite A")
@@ -1539,6 +1665,15 @@
by (erule eq[symmetric])
qed

+lemma setprod_Un_one:
+  assumes fS: "finite S" and fT: "finite T"
+  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
+  shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
+  using fS fT