equal
deleted
inserted
replaced
1082 show ?thesis |
1082 show ?thesis |
1083 by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z]) |
1083 by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z]) |
1084 qed |
1084 qed |
1085 |
1085 |
1086 lemma setsum_mono_zero_right: |
1086 lemma setsum_mono_zero_right: |
1087 assumes fT: "finite T" and ST: "S \<subseteq> T" |
1087 "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S" |
1088 and z: "\<forall>i \<in> T - S. f i = 0" |
1088 by(blast intro!: setsum_mono_zero_left[symmetric]) |
1089 shows "setsum f T = setsum f S" |
|
1090 using setsum_mono_zero_left[OF fT ST z] by simp |
|
1091 |
1089 |
1092 lemma setsum_mono_zero_cong_left: |
1090 lemma setsum_mono_zero_cong_left: |
1093 assumes fT: "finite T" and ST: "S \<subseteq> T" |
1091 assumes fT: "finite T" and ST: "S \<subseteq> T" |
1094 and z: "\<forall>i \<in> T - S. g i = 0" |
1092 and z: "\<forall>i \<in> T - S. g i = 0" |
1095 and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x" |
1093 and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x" |
1643 |
1641 |
1644 lemma setprod_cong: |
1642 lemma setprod_cong: |
1645 "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B" |
1643 "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B" |
1646 by(fastsimp simp: setprod_def intro: fold_image_cong) |
1644 by(fastsimp simp: setprod_def intro: fold_image_cong) |
1647 |
1645 |
1648 lemma strong_setprod_cong: |
1646 lemma strong_setprod_cong[cong]: |
1649 "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B" |
1647 "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B" |
1650 by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong) |
1648 by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong) |
1651 |
1649 |
1652 lemma setprod_reindex_cong: "inj_on f A ==> |
1650 lemma setprod_reindex_cong: "inj_on f A ==> |
1653 B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A" |
1651 B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A" |
1660 have "setprod h B = setprod (h o f) A" |
1658 have "setprod h B = setprod (h o f) A" |
1661 by (simp add: B setprod_reindex[OF i, of h]) |
1659 by (simp add: B setprod_reindex[OF i, of h]) |
1662 then show ?thesis apply simp |
1660 then show ?thesis apply simp |
1663 apply (rule setprod_cong) |
1661 apply (rule setprod_cong) |
1664 apply simp |
1662 apply simp |
1665 by (erule eq[symmetric]) |
1663 by (simp add: eq) |
1666 qed |
1664 qed |
1667 |
1665 |
1668 lemma setprod_Un_one: |
1666 lemma setprod_Un_one: |
1669 assumes fS: "finite S" and fT: "finite T" |
1667 assumes fS: "finite S" and fT: "finite T" |
1670 and I0: "\<forall>x \<in> S\<inter>T. f x = 1" |
1668 and I0: "\<forall>x \<in> S\<inter>T. f x = 1" |
1691 by(simp add: setprod_def fold_image_Un_Int[symmetric]) |
1689 by(simp add: setprod_def fold_image_Un_Int[symmetric]) |
1692 |
1690 |
1693 lemma setprod_Un_disjoint: "finite A ==> finite B |
1691 lemma setprod_Un_disjoint: "finite A ==> finite B |
1694 ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B" |
1692 ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B" |
1695 by (subst setprod_Un_Int [symmetric], auto) |
1693 by (subst setprod_Un_Int [symmetric], auto) |
|
1694 |
|
1695 lemma setprod_mono_one_left: |
|
1696 assumes fT: "finite T" and ST: "S \<subseteq> T" |
|
1697 and z: "\<forall>i \<in> T - S. f i = 1" |
|
1698 shows "setprod f S = setprod f T" |
|
1699 proof- |
|
1700 have eq: "T = S \<union> (T - S)" using ST by blast |
|
1701 have d: "S \<inter> (T - S) = {}" using ST by blast |
|
1702 from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset) |
|
1703 show ?thesis |
|
1704 by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z]) |
|
1705 qed |
|
1706 |
|
1707 lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym] |
1696 |
1708 |
1697 lemma setprod_delta: |
1709 lemma setprod_delta: |
1698 assumes fS: "finite S" |
1710 assumes fS: "finite S" |
1699 shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)" |
1711 shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)" |
1700 proof- |
1712 proof- |