# HG changeset patch # User haftmann # Date 1364068239 -3600 # Node ID f738e6dbd844e4d0f060b04492d08c9527458872 # Parent 3c886fe611b85637c4fc092144ed63627336747c fundamental revision of big operators on sets diff -r 3c886fe611b8 -r f738e6dbd844 CONTRIBUTORS --- a/CONTRIBUTORS Sat Mar 23 17:11:06 2013 +0100 +++ b/CONTRIBUTORS Sat Mar 23 20:50:39 2013 +0100 @@ -7,6 +7,9 @@ -------------------------------------- * March 2013: Florian Haftmann, TUM + Reform of "big operators" on sets. + +* March 2013: Florian Haftmann, TUM Algebraic locale hierarchy for orderings and (semi)lattices. * Feb. 2013: Florian Haftmann, TUM diff -r 3c886fe611b8 -r f738e6dbd844 NEWS --- a/NEWS Sat Mar 23 17:11:06 2013 +0100 +++ b/NEWS Sat Mar 23 20:50:39 2013 +0100 @@ -33,6 +33,28 @@ *** HOL *** +* Revised devices for recursive definitions over finite sets: + - Only one fundamental fold combinator on finite set remains: + Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b + This is now identity on infinite sets. + - Locales (»mini packages«) for fundamental definitions with + Finite_Set.fold: folding, folding_idem. + - Locales comm_monoid_set, semilattice_order_set and + semilattice_neutr_order_set for big operators on sets. + See theory Big_Operators for canonical examples. + Note that foundational constants comm_monoid_set.F and + semilattice_set.F correspond to former combinators fold_image + and fold1 respectively. These are now gone. You may use + those foundational counstants as substitutes, but it is + preferable to interpret the above locales accordingly. + - Dropped class ab_semigroup_idem_mult (special case of lattice, + no longer needed in connection with Finite_Set.fold etc.) + - Fact renames: + card.union_inter ~> card_Un_Int [symmetric] + card.union_disjoint ~> card_Un_disjoint + +INCOMPATIBILITY. + * Locale hierarchy for abstract orderings and (semi)lattices. * Discontinued theory src/HOL/Library/Eval_Witness. diff -r 3c886fe611b8 -r f738e6dbd844 src/Doc/Main/Main_Doc.thy --- a/src/Doc/Main/Main_Doc.thy Sat Mar 23 17:11:06 2013 +0100 +++ b/src/Doc/Main/Main_Doc.thy Sat Mar 23 20:50:39 2013 +0100 @@ -406,7 +406,6 @@ @{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\bool"}\\ @{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\ @{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b"}\\ -@{const Finite_Set.fold_image} & @{typ "('b \ 'b \ 'b) \ ('a \ 'b) \ 'b \ 'a set \ 'b"}\\ @{const Big_Operators.setsum} & @{term_type_only Big_Operators.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\ @{const Big_Operators.setprod} & @{term_type_only Big_Operators.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\ \end{supertabular} diff -r 3c886fe611b8 -r f738e6dbd844 src/HOL/Algebra/poly/UnivPoly2.thy --- a/src/HOL/Algebra/poly/UnivPoly2.thy Sat Mar 23 17:11:06 2013 +0100 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy Sat Mar 23 20:50:39 2013 +0100 @@ -687,7 +687,7 @@ proof (cases "finite A") case True then show ?thesis by induct auto next - case False then show ?thesis by (simp add: setsum_def) + case False then show ?thesis by simp qed (* Instance of a more general result!!! *) diff -r 3c886fe611b8 -r f738e6dbd844 src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Sat Mar 23 17:11:06 2013 +0100 +++ b/src/HOL/BNF/More_BNFs.thy Sat Mar 23 20:50:39 2013 +0100 @@ -548,16 +548,16 @@ unfolding mcard_def by auto lemma mcard_Plus[simp]: "mcard (M + N) = mcard M + mcard N" -proof- +proof - have "setsum (count M) {a. 0 < count M a + count N a} = setsum (count M) {a. a \# M}" - apply(rule setsum_mono_zero_cong_right) by auto + apply (rule setsum_mono_zero_cong_right) by auto moreover have "setsum (count N) {a. 0 < count M a + count N a} = setsum (count N) {a. a \# N}" - apply(rule setsum_mono_zero_cong_right) by auto + apply (rule setsum_mono_zero_cong_right) by auto ultimately show ?thesis - unfolding mcard_def count_union[THEN ext] comm_monoid_add_class.setsum.F_fun_f by simp + unfolding mcard_def count_union [THEN ext] by (simp add: setsum.distrib) qed lemma setsum_gt_0_iff: @@ -1207,7 +1207,7 @@ have "setsum L {aa. f aa = a \ 0 < L aa} = setsum L {aa. f aa = a \ 0 < K aa + L aa}" apply(rule setsum_mono_zero_cong_left) using C by auto ultimately show ?thesis - unfolding mmap_def unfolding comm_monoid_add_class.setsum.F_fun_f by auto + unfolding mmap_def by (auto simp add: setsum.distrib) qed lemma multiset_map_Plus[simp]: @@ -1265,10 +1265,10 @@ have "setsum (\ x. setsum (count M) (A x)) ?B = setsum (setsum (count M) o A) ?B" unfolding comp_def .. also have "... = (\x\ A ` ?B. setsum (count M) x)" - unfolding comm_monoid_add_class.setsum_reindex[OF i, symmetric] .. + unfolding setsum.reindex [OF i, symmetric] .. also have "... = setsum (count M) (\x\A ` {b. 0 < setsum (count M) (A b)}. x)" (is "_ = setsum (count M) ?J") - apply(rule comm_monoid_add_class.setsum_UN_disjoint[symmetric]) + apply(rule setsum.UNION_disjoint[symmetric]) using 0 fin unfolding A_def by (auto intro!: finite_imageI) also have "?J = {a. a \# M}" unfolding AB unfolding A_def by auto finally have "setsum (\ x. setsum (count M) (A x)) ?B = diff -r 3c886fe611b8 -r f738e6dbd844 src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Sat Mar 23 17:11:06 2013 +0100 +++ b/src/HOL/Big_Operators.thy Sat Mar 23 20:50:39 2013 +0100 @@ -6,7 +6,7 @@ header {* Big operators and finite (non-empty) sets *} theory Big_Operators -imports Finite_Set Metis +imports Finite_Set Option Metis begin subsection {* Generic monoid operation over a set *} @@ -14,46 +14,223 @@ no_notation times (infixl "*" 70) no_notation Groups.one ("1") -locale comm_monoid_big = comm_monoid + - fixes F :: "('b \ 'a) \ 'b set \ 'a" - assumes F_eq: "F g A = (if finite A then fold_image (op *) g 1 A else 1)" +locale comm_monoid_set = comm_monoid +begin -sublocale comm_monoid_big < folding_image proof -qed (simp add: F_eq) - -context comm_monoid_big -begin +definition F :: "('b \ 'a) \ 'b set \ 'a" +where + eq_fold: "F g A = Finite_Set.fold (f \ g) 1 A" lemma infinite [simp]: "\ finite A \ F g A = 1" - by (simp add: F_eq) + by (simp add: eq_fold) + +lemma empty [simp]: + "F g {} = 1" + by (simp add: eq_fold) + +lemma insert [simp]: + assumes "finite A" and "x \ A" + shows "F g (insert x A) = g x * F g A" +proof - + interpret comp_fun_commute f + by default (simp add: fun_eq_iff left_commute) + interpret comp_fun_commute "f \ g" + by (rule comp_comp_fun_commute) + from assms show ?thesis by (simp add: eq_fold) +qed + +lemma remove: + assumes "finite A" and "x \ A" + shows "F g A = g x * F g (A - {x})" +proof - + from `x \ A` obtain B where A: "A = insert x B" and "x \ B" + by (auto dest: mk_disjoint_insert) + moreover from `finite A` this have "finite B" by simp + ultimately show ?thesis by simp +qed + +lemma insert_remove: + assumes "finite A" + shows "F g (insert x A) = g x * F g (A - {x})" + using assms by (cases "x \ A") (simp_all add: remove insert_absorb) + +lemma neutral: + assumes "\x\A. g x = 1" + shows "F g A = 1" +proof (cases "finite A") + case True from `finite A` assms show ?thesis by (induct A) simp_all +next + case False then show ?thesis by simp +qed -lemma F_cong: - assumes "A = B" "\x. x \ B \ 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) +lemma neutral_const [simp]: + "F (\_. 1) A = 1" + by (simp add: neutral) + +lemma union_inter: + assumes "finite A" and "finite B" + shows "F g (A \ B) * F g (A \ B) = F g A * F g B" + -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} +using assms proof (induct A) + case empty then show ?case by simp next - assume "\ finite A" - then show ?thesis unfolding `A = B` by simp + case (insert x A) then show ?case + by (auto simp add: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute) +qed + +corollary union_inter_neutral: + assumes "finite A" and "finite B" + and I0: "\x \ A \ B. g x = 1" + shows "F g (A \ B) = F g A * F g B" + using assms by (simp add: union_inter [symmetric] neutral) + +corollary union_disjoint: + assumes "finite A" and "finite B" + assumes "A \ B = {}" + shows "F g (A \ B) = F g A * F g B" + using assms by (simp add: union_inter_neutral) + +lemma subset_diff: + "B \ A \ finite A \ F g A = F g (A - B) * F g B" + by (metis Diff_partition union_disjoint Diff_disjoint finite_Un inf_commute sup_commute) + +lemma reindex: + assumes "inj_on h A" + shows "F g (h ` A) = F (g \ h) A" +proof (cases "finite A") + case True + interpret comp_fun_commute f + by default (simp add: fun_eq_iff left_commute) + interpret comp_fun_commute "f \ g" + by (rule comp_comp_fun_commute) + from assms `finite A` show ?thesis by (simp add: eq_fold fold_image comp_assoc) +next + case False with assms have "\ finite (h ` A)" by (blast dest: finite_imageD) + with False show ?thesis by simp qed -lemma strong_F_cong [cong]: - "\ A = B; !!x. x:B =simp=> g x = h x \ - \ F (%x. g x) A = F (%x. h x) B" -by (rule F_cong) (simp_all add: simp_implies_def) +lemma cong: + assumes "A = B" + assumes g_h: "\x. x \ B \ g x = h x" + shows "F g A = F h B" +proof (cases "finite A") + case True + then have "\C. C \ A \ (\x\C. g x = h x) \ F g C = F h C" + proof induct + case empty then show ?case by simp + next + case (insert x F) then show ?case apply - + apply (simp add: subset_insert_iff, clarify) + apply (subgoal_tac "finite C") + prefer 2 apply (blast dest: finite_subset [rotated]) + apply (subgoal_tac "C = insert x (C - {x})") + prefer 2 apply blast + apply (erule ssubst) + apply (simp add: Ball_def del: insert_Diff_single) + done + qed + with `A = B` g_h show ?thesis by simp +next + case False + with `A = B` show ?thesis by simp +qed -lemma F_neutral[simp]: "F (%i. 1) A = 1" -by (cases "finite A") (simp_all add: neutral) +lemma strong_cong [cong]: + assumes "A = B" "\x. x \ B =simp=> g x = h x" + shows "F (\x. g x) A = F (\x. h x) B" + by (rule cong) (insert assms, simp_all add: simp_implies_def) + +lemma UNION_disjoint: + assumes "finite I" and "\i\I. finite (A i)" + and "\i\I. \j\I. i \ j \ A i \ A j = {}" + shows "F g (UNION I A) = F (\x. F g (A x)) I" +apply (insert assms) +apply (induct rule: finite_induct) +apply simp +apply atomize +apply (subgoal_tac "\i\Fa. x \ i") + prefer 2 apply blast +apply (subgoal_tac "A x Int UNION Fa A = {}") + prefer 2 apply blast +apply (simp add: union_disjoint) +done + +lemma Union_disjoint: + assumes "\A\C. finite A" "\A\C. \B\C. A \ B \ A \ B = {}" + shows "F g (Union C) = F (F g) C" +proof cases + assume "finite C" + from UNION_disjoint [OF this assms] + show ?thesis + by (simp add: SUP_def) +qed (auto dest: finite_UnionD intro: infinite) -lemma F_neutral': "ALL a:A. g a = 1 \ F g A = 1" -by simp +lemma distrib: + "F (\x. g x * h x) A = F g A * F h A" +proof (cases "finite A") + case False then show ?thesis by simp +next + case True then show ?thesis by (rule finite_induct) (simp_all add: assoc commute left_commute) +qed + +lemma Sigma: + "finite A \ \x\A. finite (B x) \ F (\x. F (g x) (B x)) A = F (split g) (SIGMA x:A. B x)" +apply (subst Sigma_def) +apply (subst UNION_disjoint, assumption, simp) + apply blast +apply (rule cong) +apply rule +apply (simp add: fun_eq_iff) +apply (subst UNION_disjoint, simp, simp) + apply blast +apply (simp add: comp_def) +done + +lemma related: + assumes Re: "R 1 1" + and Rop: "\x1 y1 x2 y2. R x1 x2 \ R y1 y2 \ R (x1 * y1) (x2 * y2)" + and fS: "finite S" and Rfg: "\x\S. R (h x) (g x)" + shows "R (F h S) (F g S)" + using fS by (rule finite_subset_induct) (insert assms, auto) -lemma F_subset_diff: "\ B \ A; finite A \ \ F g A = F g (A - B) * F g B" -by (metis Diff_partition union_disjoint Diff_disjoint finite_Un inf_commute sup_commute) +lemma eq_general: + assumes h: "\y\S'. \!x. x \ S \ h x = y" + and f12: "\x\S. h x \ S' \ f2 (h x) = f1 x" + shows "F f1 S = F f2 S'" +proof- + from h f12 have hS: "h ` S = S'" by blast + {fix x y assume H: "x \ S" "y \ 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: "\x. x \ S \ (f2 \ h) x = f1 x" by auto + from hS have "F f2 S' = F f2 (h ` S)" by simp + also have "\ = F (f2 o h) S" using reindex [OF hinj, of f2] . + also have "\ = F f1 S " using th cong [of _ _ "f2 o h" f1] + by blast + finally show ?thesis .. +qed -lemma F_mono_neutral_cong_left: +lemma eq_general_reverses: + assumes kh: "\y. y \ T \ k y \ S \ h (k y) = y" + and hk: "\x. x \ S \ h x \ T \ k (h x) = x \ g (h x) = j x" + shows "F j S = F g T" + (* metis solves it, but not yet available here *) + apply (rule eq_general [of T S h g j]) + 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 + +lemma mono_neutral_cong_left: assumes "finite T" and "S \ T" and "\i \ T - S. h i = 1" and "\x. x \ S \ g x = h x" shows "F g S = F h T" proof- @@ -62,25 +239,25 @@ from `finite T` `S \ T` have f: "finite S" "finite (T - S)" by (auto intro: finite_subset) show ?thesis using assms(4) - by (simp add: union_disjoint[OF f d, unfolded eq[symmetric]] F_neutral'[OF assms(3)]) + by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)]) qed -lemma F_mono_neutral_cong_right: +lemma mono_neutral_cong_right: "\ finite T; S \ T; \i \ T - S. g i = 1; \x. x \ S \ g x = h x \ \ F g T = F h S" -by(auto intro!: F_mono_neutral_cong_left[symmetric]) + by (auto intro!: mono_neutral_cong_left [symmetric]) -lemma F_mono_neutral_left: +lemma mono_neutral_left: "\ finite T; S \ T; \i \ T - S. g i = 1 \ \ F g S = F g T" -by(blast intro: F_mono_neutral_cong_left) + by (blast intro: mono_neutral_cong_left) -lemma F_mono_neutral_right: +lemma mono_neutral_right: "\ finite T; S \ T; \i \ T - S. g i = 1 \ \ F g T = F g S" -by(blast intro!: F_mono_neutral_left[symmetric]) + by (blast intro!: mono_neutral_left [symmetric]) -lemma F_delta: +lemma delta: assumes fS: "finite S" - shows "F (\k. if k=a then b k else 1) S = (if a \ S then b a else 1)" + shows "F (\k. if k = a then b k else 1) S = (if a \ S then b a else 1)" proof- let ?f = "(\k. if k=a then b k else 1)" { assume a: "a \ S" @@ -94,78 +271,71 @@ have dj: "?A \ ?B = {}" by simp from fS have fAB: "finite ?A" "finite ?B" by auto have "F ?f S = F ?f ?A * F ?f ?B" - using union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] + using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp - then have ?thesis using a by simp } + then have ?thesis using a by simp } ultimately show ?thesis by blast qed -lemma F_delta': - assumes fS: "finite S" shows - "F (\k. if a = k then b k else 1) S = (if a \ S then b a else 1)" -using F_delta[OF fS, of a b, symmetric] by (auto intro: F_cong) - -lemma F_fun_f: "F (%x. g x * h x) A = (F g A * F h A)" -by (cases "finite A") (simp_all add: distrib) - - -text {* for ad-hoc proofs for @{const fold_image} *} -lemma comm_monoid_mult: "class.comm_monoid_mult (op *) 1" -proof qed (auto intro: assoc commute) - -lemma F_Un_neutral: - assumes fS: "finite S" and fT: "finite T" - and I1: "\x \ S\T. g x = 1" - shows "F g (S \ T) = F g S * F g T" -proof - - interpret comm_monoid_mult "op *" 1 by (fact comm_monoid_mult) - show ?thesis - using fS fT - apply (simp add: F_eq) - apply (rule fold_image_Un_one) - using I1 by auto -qed +lemma delta': + assumes fS: "finite S" + shows "F (\k. if a = k then b k else 1) S = (if a \ S then b a else 1)" + using delta [OF fS, of a b, symmetric] by (auto intro: cong) lemma If_cases: fixes P :: "'b \ bool" and g h :: "'b \ 'a" assumes fA: "finite A" shows "F (\x. if P x then h x else g x) A = - F h (A \ {x. P x}) * F g (A \ - {x. P x})" -proof- + F h (A \ {x. P x}) * F g (A \ - {x. P x})" +proof - have a: "A = A \ {x. P x} \ A \ -{x. P x}" "(A \ {x. P x}) \ (A \ -{x. P x}) = {}" by blast+ from fA have f: "finite (A \ {x. P x})" "finite (A \ -{x. P x})" by auto let ?g = "\x. if P x then h x else g x" - from union_disjoint[OF f a(2), of ?g] a(1) + from union_disjoint [OF f a(2), of ?g] a(1) show ?thesis - by (subst (1 2) F_cong) simp_all + by (subst (1 2) cong) simp_all qed +lemma cartesian_product: + "F (\x. F (g x) B) A = F (split g) (A <*> B)" +apply (rule sym) +apply (cases "finite A") + apply (cases "finite B") + apply (simp add: Sigma) + apply (cases "A={}", simp) + apply simp +apply (auto intro: infinite dest: finite_cartesian_productD2) +apply (cases "B = {}") apply (auto intro: infinite dest: finite_cartesian_productD1) +done + end -text {* for ad-hoc proofs for @{const fold_image} *} - -lemma (in comm_monoid_add) comm_monoid_mult: - "class.comm_monoid_mult (op +) 0" -proof qed (auto intro: add_assoc add_commute) - notation times (infixl "*" 70) notation Groups.one ("1") subsection {* Generalized summation over a set *} -definition (in comm_monoid_add) setsum :: "('b \ 'a) => 'b set => 'a" where - "setsum f A = (if finite A then fold_image (op +) f 0 A else 0)" +definition (in comm_monoid_add) setsum :: "('b \ 'a) \ 'b set \ 'a" +where + "setsum = comm_monoid_set.F plus 0" -sublocale comm_monoid_add < setsum!: comm_monoid_big "op +" 0 setsum proof -qed (fact setsum_def) +sublocale comm_monoid_add < setsum!: comm_monoid_set plus 0 +where + "setsum.F = setsum" +proof - + show "comm_monoid_set plus 0" .. + then interpret setsum!: comm_monoid_set plus 0 . + show "setsum.F = setsum" + by (simp only: setsum_def) +qed abbreviation - Setsum ("\_" [1000] 999) where - "\A == setsum (%x. x) A" + Setsum ("\_" [1000] 999) where + "\A \ setsum (%x. x) A" text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is written @{text"\x\A. e"}. *} @@ -211,48 +381,32 @@ in [(@{const_syntax setsum}, setsum_tr')] end *} -lemma setsum_empty: - "setsum f {} = 0" - by (fact setsum.empty) +text {* TODO These are candidates for generalization *} -lemma setsum_insert: - "finite F ==> a \ F ==> setsum f (insert a F) = f a + setsum f F" - by (fact setsum.insert) - -lemma setsum_infinite: - "~ finite A ==> setsum f A = 0" - by (fact setsum.infinite) +context comm_monoid_add +begin -lemma (in comm_monoid_add) setsum_reindex: - assumes "inj_on f B" shows "setsum h (f ` B) = setsum (h \ f) B" -proof - - interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult) - from assms show ?thesis by (auto simp add: setsum_def fold_image_reindex o_def dest!:finite_imageD) -qed - -lemma setsum_reindex_id: +lemma setsum_reindex_id: "inj_on f B ==> setsum f B = setsum id (f ` B)" -by (simp add: setsum_reindex) + by (simp add: setsum.reindex) -lemma setsum_reindex_nonzero: +lemma setsum_reindex_nonzero: assumes fS: "finite S" - and nz: "\ x y. x \ S \ y \ S \ x \ y \ f x = f y \ h (f x) = 0" - shows "setsum h (f ` S) = setsum (h o f) S" -using nz -proof(induct rule: finite_induct[OF fS]) + and nz: "\x y. x \ S \ y \ S \ x \ y \ f x = f y \ h (f x) = 0" + shows "setsum h (f ` S) = setsum (h \ f) S" +using nz proof (induct rule: finite_induct [OF fS]) case 1 thus ?case by simp next case (2 x F) { assume fxF: "f x \ f ` F" hence "\y \ F . f y = f x" by auto then obtain y where y: "y \ F" "f x = f y" by auto from "2.hyps" y have xy: "x \ y" by auto - - from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp + from "2.prems" [of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto also have "\ = setsum (h o f) (insert x F)" unfolding setsum.insert[OF `finite F` `x\F`] using h0 - apply (simp cong del:setsum.strong_F_cong) + apply (simp cong del: setsum.strong_cong) apply (rule "2.hyps"(3)) apply (rule_tac y="y" in "2.prems") apply simp_all @@ -264,7 +418,7 @@ using fxF "2.hyps" by simp also have "\ = setsum (h o f) (insert x F)" unfolding setsum.insert[OF `finite F` `x\F`] - apply (simp cong del:setsum.strong_F_cong) + apply (simp cong del: setsum.strong_cong) apply (rule cong [OF refl [of "op + (h (f x))"]]) apply (rule "2.hyps"(3)) apply (rule_tac y="y" in "2.prems") @@ -274,59 +428,14 @@ ultimately show ?case by blast qed -lemma setsum_cong: - "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" -by (fact setsum.F_cong) - -lemma strong_setsum_cong: - "A = B ==> (!!x. x:B =simp=> f x = g x) - ==> setsum (%x. f x) A = setsum (%x. g x) B" -by (fact setsum.strong_F_cong) - -lemma setsum_cong2: "\\x. x \ A \ f x = g x\ \ setsum f A = setsum g A" -by (auto intro: setsum_cong) +lemma setsum_cong2: + "(\x. x \ A \ f x = g x) \ setsum f A = setsum g A" + by (auto intro: setsum.cong) lemma setsum_reindex_cong: "[|inj_on f A; B = f ` A; !!a. a:A \ g a = h (f a)|] ==> setsum h B = setsum g A" -by (simp add: setsum_reindex) - -lemmas setsum_0 = setsum.F_neutral -lemmas setsum_0' = setsum.F_neutral' - -lemma setsum_Un_Int: "finite A ==> finite B ==> - setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" - -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} -by (fact setsum.union_inter) - -lemma setsum_Un_disjoint: "finite A ==> finite B - ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B" -by (fact setsum.union_disjoint) - -lemma setsum_subset_diff: "\ B \ A; finite A \ \ - setsum f A = setsum f (A - B) + setsum f B" -by(fact setsum.F_subset_diff) - -lemma setsum_mono_zero_left: - "\ finite T; S \ T; \i \ T - S. f i = 0 \ \ setsum f S = setsum f T" -by(fact setsum.F_mono_neutral_left) - -lemmas setsum_mono_zero_right = setsum.F_mono_neutral_right - -lemma setsum_mono_zero_cong_left: - "\ finite T; S \ T; \i \ T - S. g i = 0; \x. x \ S \ f x = g x \ - \ setsum f S = setsum g T" -by(fact setsum.F_mono_neutral_cong_left) - -lemmas setsum_mono_zero_cong_right = setsum.F_mono_neutral_cong_right - -lemma setsum_delta: "finite S \ - setsum (\k. if k=a then b k else 0) S = (if a \ S then b a else 0)" -by(fact setsum.F_delta) - -lemma setsum_delta': "finite S \ - setsum (\k. if a = k then b k else 0) S = (if a\ S then b a else 0)" -by(fact setsum.F_delta') + by (simp add: setsum.reindex) lemma setsum_restrict_set: assumes fA: "finite A" @@ -335,70 +444,20 @@ from fA have fab: "finite (A \ B)" by auto have aba: "A \ B \ A" by blast let ?g = "\x. if x \ A\B then f x else 0" - from setsum_mono_zero_left[OF fA aba, of ?g] + from setsum.mono_neutral_left [OF fA aba, of ?g] show ?thesis by simp qed -lemma setsum_cases: - assumes fA: "finite A" - shows "setsum (\x. if P x then f x else g x) A = - setsum f (A \ {x. P x}) + setsum g (A \ - {x. P x})" - 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.*) -lemma (in comm_monoid_add) setsum_UN_disjoint: - assumes "finite I" and "ALL i:I. finite (A i)" - and "ALL i:I. ALL j:I. i \ j --> A i Int A j = {}" - shows "setsum f (UNION I A) = (\i\I. setsum f (A i))" -proof - - interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult) - from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint) -qed - -text{*No need to assume that @{term C} is finite. If infinite, the rhs is -directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*} lemma setsum_Union_disjoint: assumes "\A\C. finite A" "\A\C. \B\C. A \ B \ A Int B = {}" shows "setsum f (Union C) = setsum (setsum f) C" -proof cases - assume "finite C" - from setsum_UN_disjoint[OF this assms] - show ?thesis - by (simp add: SUP_def) -qed (force dest: finite_UnionD simp add: setsum_def) - -(*But we can't get rid of finite A. If infinite, although the lhs is 0, - the rhs need not be, since SIGMA A B could still be finite.*) -lemma (in comm_monoid_add) setsum_Sigma: - assumes "finite A" and "ALL x:A. finite (B x)" - shows "(\x\A. (\y\B x. f x y)) = (\(x,y)\(SIGMA x:A. B x). f x y)" -proof - - interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult) - from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def) -qed + using assms by (fact setsum.Union_disjoint) -text{*Here we can eliminate the finiteness assumptions, by cases.*} -lemma setsum_cartesian_product: - "(\x\A. (\y\B. f x y)) = (\(x,y) \ A <*> B. f x y)" -apply (cases "finite A") - apply (cases "finite B") - apply (simp add: setsum_Sigma) - apply (cases "A={}", simp) - apply (simp) -apply (auto simp add: setsum_def - dest: finite_cartesian_productD1 finite_cartesian_productD2) -done +lemma setsum_cartesian_product: + "(\x\A. (\y\B. f x y)) = (\(x,y) \ A <*> B. f x y)" + by (fact setsum.cartesian_product) -lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)" -by (fact setsum.F_fun_f) - -lemma setsum_Un_zero: - "\ finite S; finite T; \x \ S\T. f x = 0 \ \ - setsum f (S \ T) = setsum f S + setsum f T" -by(fact setsum.F_Un_neutral) - -lemma setsum_UNION_zero: +lemma setsum_UNION_zero: assumes fS: "finite S" and fSS: "\T \ S. finite T" and f0: "\T1 T2 x. T1\S \ T2\S \ T1 \ T2 \ x \ T1 \ x \ T2 \ f x = 0" shows "setsum f (\S) = setsum (\T. setsum f T) S" @@ -412,36 +471,145 @@ from fTF have fUF: "finite (\F)" by auto from "2.prems" TF fTF show ?case - by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f]) + by (auto simp add: H [symmetric] intro: setsum.union_inter_neutral [OF fTF(1) fUF, of f]) +qed + +text {* Commuting outer and inner summation *} + +lemma setsum_commute: + "(\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)" +proof (simp add: setsum_cartesian_product) + have "(\(x,y) \ A <*> B. f x y) = + (\(y,x) \ (%(i, j). (j, i)) ` (A \ B). f x y)" + (is "?s = _") + apply (simp add: setsum.reindex [where h = "%(i, j). (j, i)"] swap_inj_on) + apply (simp add: split_def) + done + also have "... = (\(y,x)\B \ A. f x y)" + (is "_ = ?t") + apply (simp add: swap_product) + done + finally show "?s = ?t" . +qed + +lemma setsum_Plus: + fixes A :: "'a set" and B :: "'b set" + assumes fin: "finite A" "finite B" + shows "setsum f (A <+> B) = setsum (f \ Inl) A + setsum (f \ Inr) B" +proof - + have "A <+> B = Inl ` A \ Inr ` B" by auto + moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)" + by auto + moreover have "Inl ` A \ Inr ` B = ({} :: ('a + 'b) set)" by auto + moreover have "inj_on (Inl :: 'a \ 'a + 'b) A" "inj_on (Inr :: 'b \ 'a + 'b) B" by(auto intro: inj_onI) + ultimately show ?thesis using fin by(simp add: setsum.union_disjoint setsum.reindex) qed +end + +text {* TODO These are legacy *} + +lemma setsum_empty: + "setsum f {} = 0" + by (fact setsum.empty) + +lemma setsum_insert: + "finite F ==> a \ F ==> setsum f (insert a F) = f a + setsum f F" + by (fact setsum.insert) + +lemma setsum_infinite: + "~ finite A ==> setsum f A = 0" + by (fact setsum.infinite) + +lemma setsum_reindex: + "inj_on f B \ setsum h (f ` B) = setsum (h \ f) B" + by (fact setsum.reindex) + +lemma setsum_cong: + "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" + by (fact setsum.cong) + +lemma strong_setsum_cong: + "A = B ==> (!!x. x:B =simp=> f x = g x) + ==> setsum (%x. f x) A = setsum (%x. g x) B" + by (fact setsum.strong_cong) + +lemmas setsum_0 = setsum.neutral_const +lemmas setsum_0' = setsum.neutral + +lemma setsum_Un_Int: "finite A ==> finite B ==> + setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" + -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} + by (fact setsum.union_inter) + +lemma setsum_Un_disjoint: "finite A ==> finite B + ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B" + by (fact setsum.union_disjoint) + +lemma setsum_subset_diff: "\ B \ A; finite A \ \ + setsum f A = setsum f (A - B) + setsum f B" + by (fact setsum.subset_diff) + +lemma setsum_mono_zero_left: + "\ finite T; S \ T; \i \ T - S. f i = 0 \ \ setsum f S = setsum f T" + by (fact setsum.mono_neutral_left) + +lemmas setsum_mono_zero_right = setsum.mono_neutral_right + +lemma setsum_mono_zero_cong_left: + "\ finite T; S \ T; \i \ T - S. g i = 0; \x. x \ S \ f x = g x \ + \ setsum f S = setsum g T" + by (fact setsum.mono_neutral_cong_left) + +lemmas setsum_mono_zero_cong_right = setsum.mono_neutral_cong_right + +lemma setsum_delta: "finite S \ + setsum (\k. if k=a then b k else 0) S = (if a \ S then b a else 0)" + by (fact setsum.delta) + +lemma setsum_delta': "finite S \ + setsum (\k. if a = k then b k else 0) S = (if a\ S then b a else 0)" + by (fact setsum.delta') + +lemma setsum_cases: + assumes "finite A" + shows "setsum (\x. if P x then f x else g x) A = + setsum f (A \ {x. P x}) + setsum g (A \ - {x. P x})" + using assms by (fact setsum.If_cases) + +(*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.*) +lemma setsum_UN_disjoint: + assumes "finite I" and "ALL i:I. finite (A i)" + and "ALL i:I. ALL j:I. i \ j --> A i Int A j = {}" + shows "setsum f (UNION I A) = (\i\I. setsum f (A i))" + using assms by (fact setsum.UNION_disjoint) + +(*But we can't get rid of finite A. If infinite, although the lhs is 0, + the rhs need not be, since SIGMA A B could still be finite.*) +lemma setsum_Sigma: + assumes "finite A" and "ALL x:A. finite (B x)" + shows "(\x\A. (\y\B x. f x y)) = (\(x,y)\(SIGMA x:A. B x). f x y)" + using assms by (fact setsum.Sigma) + +lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)" + by (fact setsum.distrib) + +lemma setsum_Un_zero: + "\