# HG changeset patch # User haftmann # Date 1403939802 -7200 # Node ID 6ab1c7cb0b8d07f8a40b7a9f8865e268dae60970 # Parent 29fe9bac501bc4e3b0f711afb3f27e5376d9e91e fact consolidation diff -r 29fe9bac501b -r 6ab1c7cb0b8d NEWS --- a/NEWS Fri Jun 27 22:08:55 2014 +0200 +++ b/NEWS Sat Jun 28 09:16:42 2014 +0200 @@ -375,6 +375,75 @@ * Theory reorganizations: * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy +* Consolidated some facts about big group operators: + + setsum_0' ~> setsum.neutral + setsum_0 ~> setsum.neutral_const + setsum_addf ~> setsum.distrib + setsum_cartesian_product ~> setsum.cartesian_product + setsum_cases ~> setsum.If_cases + setsum_commute ~> setsum.commute + setsum_cong ~> setsum.cong + setsum_delta ~> setsum.delta + setsum_delta' ~> setsum.delta' + setsum_diff1' ~> setsum.remove + setsum_empty ~> setsum.empty + setsum_infinite ~> setsum.infinite + setsum_insert ~> setsum.insert + setsum_inter_restrict'' ~> setsum.inter_filter + setsum_mono_zero_cong_left ~> setsum.mono_neutral_cong_left + setsum_mono_zero_cong_right ~> setsum.mono_neutral_cong_right + setsum_mono_zero_left ~> setsum.mono_neutral_left + setsum_mono_zero_right ~> setsum.mono_neutral_right + setsum_reindex ~> setsum.reindex + setsum_reindex_cong ~> setsum.reindex_cong + setsum_reindex_nonzero ~> setsum.reindex_nontrivial + setsum_restrict_set ~> setsum.inter_restrict + setsum_Plus ~> setsum.Plus + setsum_setsum_restrict ~> setsum.commute_restrict + setsum_Sigma ~> setsum.Sigma + setsum_subset_diff ~> setsum.subset_diff + setsum_Un_disjoint ~> setsum.union_disjoint + setsum_UN_disjoint ~> setsum.UNION_disjoint + setsum_Un_Int ~> setsum.union_inter + setsum_Union_disjoint ~> setsum.Union_disjoint + setsum_UNION_zero ~> setsum.Union_comp + setsum_Un_zero ~> setsum.union_inter_neutral + strong_setprod_cong ~> setprod.strong_cong + strong_setsum_cong ~> setsum.strong_cong + setprod_1' ~> setprod.neutral + setprod_1 ~> setprod.neutral_const + setprod_cartesian_product ~> setprod.cartesian_product + setprod_cong ~> setprod.cong + setprod_delta ~> setprod.delta + setprod_delta' ~> setprod.delta' + setprod_empty ~> setprod.empty + setprod_infinite ~> setprod.infinite + setprod_insert ~> setprod.insert + setprod_mono_one_cong_left ~> setprod.mono_neutral_cong_left + setprod_mono_one_cong_right ~> setprod.mono_neutral_cong_right + setprod_mono_one_left ~> setprod.mono_neutral_left + setprod_mono_one_right ~> setprod.mono_neutral_right + setprod_reindex ~> setprod.reindex + setprod_reindex_cong ~> setprod.reindex_cong + setprod_reindex_nonzero ~> setprod.reindex_nontrivial + setprod_Sigma ~> setprod.Sigma + setprod_subset_diff ~> setprod.subset_diff + setprod_timesf ~> setprod.distrib + setprod_Un2 ~> setprod.union_diff2 + setprod_Un_disjoint ~> setprod.union_disjoint + setprod_UN_disjoint ~> setprod.UNION_disjoint + setprod_Un_Int ~> setprod.union_inter + setprod_Union_disjoint ~> setprod.Union_disjoint + setprod_Un_one ~> setprod.union_inter_neutral + + Dropped setsum_cong2 (simple variant of setsum.cong). + Dropped setsum_inter_restrict' (simple variant of setsum.inter_restrict) + Dropped setsum_reindex_id, setprod_reindex_id + (simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]). + + INCOMPATIBILITY. + * New internal SAT solver "cdclite" that produces models and proof traces. This solver replaces the internal SAT solvers "enumerate" and "dpll". Applications that explicitly used one of these two SAT solvers should diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Sat Jun 28 09:16:42 2014 +0200 @@ -34,7 +34,7 @@ show ?thesis unfolding setsum_right_distrib shift_pow uminus_add_conv_diff [symmetric] setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc] - setsum_reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\ n. (-1)^n *a n * x^n"] by auto + setsum.reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\ n. (-1)^n *a n * x^n"] by auto qed lemma horner_schema: @@ -747,7 +747,7 @@ also have "\ = (\ i = 0 ..< 2 * n. if even i then -1 ^ (i div 2) / (real (fact i)) * x ^ i else 0)" unfolding sum_split_even_odd atLeast0LessThan .. also have "\ = (\ i = 0 ..< 2 * n. (if even i then -1 ^ (i div 2) / (real (fact i)) else 0) * x ^ i)" - by (rule setsum_cong2) auto + by (rule setsum.cong) auto finally show ?thesis by assumption qed } note morph_to_if_power = this @@ -862,7 +862,7 @@ also have "\ = (\ i = 0 ..< 2 * n. if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i)) * x ^ i)" unfolding sum_split_even_odd atLeast0LessThan .. also have "\ = (\ i = 0 ..< 2 * n. (if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i))) * x ^ i)" - by (rule setsum_cong2) auto + by (rule setsum.cong) auto finally show ?thesis by assumption qed } note setsum_morph = this diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Deriv.thy Sat Jun 28 09:16:42 2014 +0200 @@ -357,7 +357,7 @@ have "((\x. f i x * (\i\I. f i x)) has_derivative ?P) (at x within s)" using insert by (intro has_derivative_mult) auto also have "?P = (\y. \i'\insert i I. f' i' y * (\j\insert i I - {i'}. f j x))" - using insert(1,2) by (auto simp add: setsum_right_distrib insert_Diff_if intro!: ext setsum_cong) + using insert(1,2) by (auto simp add: setsum_right_distrib insert_Diff_if intro!: ext setsum.cong) finally show ?case using insert by simp qed simp diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Fact.thy --- a/src/HOL/Fact.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Fact.thy Sat Jun 28 09:16:42 2014 +0200 @@ -202,7 +202,7 @@ also from Suc.hyps have "... = Suc (n + d') * \{n + 1..n + d'}" unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod) also have "... = \{n + 1..n + Suc d'}" - by (simp add: atLeastAtMostSuc_conv setprod_insert) + by (simp add: atLeastAtMostSuc_conv setprod.insert) finally show ?case . qed from this `m = n + d` show ?thesis by simp @@ -314,7 +314,7 @@ assumes "r \ n" shows "fact n div fact (n - r) \ n ^ r" proof - have "\r. r \ n \ \{n - r..n} = (n - r) * \{Suc (n - r)..n}" - by (subst setprod_insert[symmetric]) (auto simp: atLeastAtMost_insertL) + by (subst setprod.insert[symmetric]) (auto simp: atLeastAtMost_insertL) with assms show ?thesis by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono) qed diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Groups_Big.thy Sat Jun 28 09:16:42 2014 +0200 @@ -87,6 +87,15 @@ shows "F g (A \ B) = F g A * F g B" using assms by (simp add: union_inter_neutral) +lemma union_diff2: + assumes "finite A" and "finite B" + shows "F g (A \ B) = F g (A - B) * F g (B - A) * F g (A \ B)" +proof - + have "A \ B = A - B \ (B - A) \ A \ B" + by auto + with assms show ?thesis by simp (subst union_disjoint, auto)+ +qed + lemma subset_diff: assumes "B \ A" and "finite A" shows "F g A = F g (A - B) * F g B" @@ -139,6 +148,13 @@ shows "F (\x. g x) A = F (\x. h x) B" by (rule cong) (insert assms, simp_all add: simp_implies_def) +lemma reindex_cong: + assumes "inj_on l B" + assumes "A = l ` B" + assumes "\x. x \ B \ g (l x) = h x" + shows "F g A = F h B" + using assms by (simp add: reindex) + lemma UNION_disjoint: assumes "finite I" and "\i\I. finite (A i)" and "\i\I. \j\I. i \ j \ A i \ A j = {}" @@ -156,7 +172,7 @@ 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" + shows "F g (Union C) = (F \ F) g C" proof cases assume "finite C" from UNION_disjoint [OF this assms] @@ -257,6 +273,15 @@ qed simp qed +lemma reindex_nontrivial: + assumes "finite A" + and nz: "\x y. x \ A \ y \ A \ x \ y \ h x = h y \ g (h x) = 1" + shows "F g (h ` A) = F (g \ h) A" +proof (subst reindex_bij_betw_not_neutral [symmetric]) + show "bij_betw h (A - {x \ A. (g \ h) x = 1}) (h ` A - h ` {x \ A. (g \ h) x = 1})" + using nz by (auto intro!: inj_onI simp: bij_betw_def) +qed (insert `finite A`, auto) + lemma reindex_bij_witness_not_neutral: assumes fin: "finite S'" "finite T'" assumes witness: @@ -336,6 +361,69 @@ apply (cases "B = {}") apply (auto intro: infinite dest: finite_cartesian_productD1) done +lemma inter_restrict: + assumes "finite A" + shows "F g (A \ B) = F (\x. if x \ B then g x else 1) A" +proof - + let ?g = "\x. if x \ A \ B then g x else 1" + have "\i\A - A \ B. (if i \ A \ B then g i else 1) = 1" + by simp + moreover have "A \ B \ A" by blast + ultimately have "F ?g (A \ B) = F ?g A" using `finite A` + by (intro mono_neutral_left) auto + then show ?thesis by simp +qed + +lemma inter_filter: + "finite A \ F g {x \ A. P x} = F (\x. if P x then g x else 1) A" + by (simp add: inter_restrict [symmetric, of A "{x. P x}" g, simplified mem_Collect_eq] Int_def) + +lemma Union_comp: + assumes "\A \ B. finite A" + and "\A1 A2 x. A1 \ B \ A2 \ B \ A1 \ A2 \ x \ A1 \ x \ A2 \ g x = 1" + shows "F g (\B) = (F \ F) g B" +using assms proof (induct B rule: infinite_finite_induct) + case (infinite A) + then have "\ finite (\A)" by (blast dest: finite_UnionD) + with infinite show ?case by simp +next + case empty then show ?case by simp +next + case (insert A B) + then have "finite A" "finite B" "finite (\B)" "A \ B" + and "\x\A \ \B. g x = 1" + and H: "F g (\B) = (F o F) g B" by auto + then have "F g (A \ \B) = F g A * F g (\B)" + by (simp add: union_inter_neutral) + with `finite B` `A \ B` show ?case + by (simp add: H) +qed + +lemma commute: + "F (\i. F (g i) B) A = F (\j. F (\i. g i j) A) B" + unfolding cartesian_product + by (rule reindex_bij_witness [where i = "\(i, j). (j, i)" and j = "\(i, j). (j, i)"]) auto + +lemma commute_restrict: + "finite A \ finite B \ + F (\x. F (g x) {y. y \ B \ R x y}) A = F (\y. F (\x. g x y) {x. x \ A \ R x y}) B" + by (simp add: inter_filter) (rule commute) + +lemma Plus: + fixes A :: "'b set" and B :: "'c set" + assumes fin: "finite A" "finite B" + shows "F g (A <+> B) = F (g \ Inl) A * F (g \ Inr) B" +proof - + have "A <+> B = Inl ` A \ Inr ` B" by auto + moreover from fin have "finite (Inl ` A :: ('b + 'c) set)" "finite (Inr ` B :: ('b + 'c) set)" + by auto + moreover have "Inl ` A \ Inr ` B = ({} :: ('b + 'c) set)" by auto + moreover have "inj_on (Inl :: 'b \ 'b + 'c) A" "inj_on (Inr :: 'c \ 'b + 'c) B" + by (auto intro: inj_onI) + ultimately show ?thesis using fin + by (simp add: union_disjoint reindex) +qed + end notation times (infixl "*" 70) @@ -410,191 +498,27 @@ in [(@{const_syntax setsum}, K setsum_tr')] end *} -text {* TODO These are candidates for generalization *} - -context comm_monoid_add -begin - -lemma setsum_reindex_id: - "inj_on f B \ setsum f B = setsum id (f ` B)" - by (simp add: setsum.reindex) - -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 \ f) S" -proof (subst setsum.reindex_bij_betw_not_neutral[symmetric]) - show "bij_betw f (S - {x\S. h (f x) = 0}) (f`S - f`{x\S. h (f x) = 0})" - using nz by (auto intro!: inj_onI simp: bij_betw_def) -qed (insert fS, auto) - -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) - -lemma setsum_restrict_set: - assumes fA: "finite A" - shows "setsum f (A \ B) = setsum (\x. if x \ B then f x else 0) A" -proof- - 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_neutral_left [OF fA aba, of ?g] - show ?thesis by simp -qed +text {* TODO generalization candidates *} -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" - using assms by (fact setsum.Union_disjoint) - -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_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" - 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" "\T\F. finite T" "finite F" and TF: "T \ F" - and H: "setsum f (\ F) = setsum (setsum f) F" by auto - from fTF have fUF: "finite (\F)" by auto - from "2.prems" TF fTF - show ?case - 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)" - unfolding setsum_cartesian_product - by (rule setsum.reindex_bij_witness[where i="\(i, j). (j, i)" and j="\(i, j). (j, i)"]) auto - -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) +lemma setsum_image_gen: + assumes fS: "finite S" + shows "setsum g S = setsum (\y. setsum g {x. x \ S \ f x = y}) (f ` S)" +proof- + { fix x assume "x \ S" then have "{y. y\ f`S \ f x = y} = {f x}" by auto } + hence "setsum g S = setsum (\x. setsum (\y. g x) {y. y\ f`S \ f x = y}) S" + by simp + also have "\ = setsum (\y. setsum g {x. x \ S \ f x = y}) (f ` S)" + by (rule setsum.commute_restrict [OF fS finite_imageI [OF fS]]) + finally show ?thesis . 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: - "\ finite S; finite T; \x \ S\T. f x = 0 \ \ - setsum f (S \ T) = setsum f S + setsum f T" - by (fact setsum.union_inter_neutral) subsubsection {* Properties in more restricted classes of structures *} lemma setsum_Un: "finite A ==> finite B ==> (setsum f (A Un B) :: 'a :: ab_group_add) = setsum f A + setsum f B - setsum f (A Int B)" -by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps) +by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps) lemma setsum_Un2: assumes "finite (A \ B)" @@ -602,7 +526,7 @@ proof - have "A \ B = A - B \ (B - A) \ A \ B" by auto - with assms show ?thesis by simp (subst setsum_Un_disjoint, auto)+ + with assms show ?thesis by simp (subst setsum.union_disjoint, auto)+ qed lemma setsum_diff1: "finite A \ @@ -664,12 +588,12 @@ have "setsum f A = setsum f ((A-{a}) \ {a})" by(simp add:insert_absorb[OF `a:A`]) also have "\ = setsum f (A-{a}) + setsum f {a}" - using `finite A` by(subst setsum_Un_disjoint) auto + using `finite A` by(subst setsum.union_disjoint) auto also have "setsum f (A-{a}) \ setsum g (A-{a})" by(rule setsum_mono)(simp add: assms(2)) also have "setsum f {a} < setsum g {a}" using a by simp also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \ {a})" - using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto + using `finite A` by(subst setsum.union_disjoint[symmetric]) auto also have "\ = setsum g A" by(simp add:insert_absorb[OF `a:A`]) finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono) qed @@ -685,7 +609,7 @@ lemma setsum_subtractf: "setsum (%x. ((f x)::'a::ab_group_add) - g x) A = setsum f A - setsum g A" - using setsum_addf [of f "- g" A] by (simp add: setsum_negf) + using setsum.distrib [of f "- g" A] by (simp add: setsum_negf) lemma setsum_nonneg: assumes nn: "\x\A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \ f x" @@ -747,11 +671,32 @@ have "setsum f A \ setsum f A + setsum f (B-A)" by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def) also have "\ = setsum f (A \ (B-A))" using fin finite_subset[OF sub fin] - by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) + by (simp add: setsum.union_disjoint del:Un_Diff_cancel) also have "A \ (B-A) = B" using sub by blast finally show ?thesis . qed +lemma setsum_le_included: + fixes f :: "'a \ 'b::ordered_comm_monoid_add" + assumes "finite s" "finite t" + and "\y\t. 0 \ g y" "(\x\s. \y\t. i y = x \ f x \ g y)" + shows "setsum f s \ setsum g t" +proof - + have "setsum f s \ setsum (\y. setsum g {x. x\t \ i x = y}) s" + proof (rule setsum_mono) + fix y assume "y \ s" + with assms obtain z where z: "z \ t" "y = i z" "f y \ g z" by auto + with assms show "f y \ setsum g {x \ t. i x = y}" (is "?A y \ ?B y") + using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro] + by (auto intro!: setsum_mono2) + qed + also have "... \ setsum (\y. setsum g {x. x\t \ i x = y}) (i ` t)" + using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg) + also have "... \ setsum g t" + using assms by (auto simp: setsum_image_gen[symmetric]) + finally show ?thesis . +qed + lemma setsum_mono3: "finite B ==> A <= B ==> ALL x: B - A. 0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==> @@ -762,7 +707,7 @@ apply simp apply (rule add_left_mono) apply (erule setsum_nonneg) - apply (subst setsum_Un_disjoint [THEN sym]) + apply (subst setsum.union_disjoint [THEN sym]) apply (erule finite_subset, assumption) apply (rule finite_subset) prefer 2 @@ -865,27 +810,21 @@ case False thus ?thesis by simp qed -lemma setsum_diff1'[rule_format]: - "finite A \ a \ A \ (\ x \ A. f x) = f a + (\ x \ (A - {a}). f x)" -apply (erule finite_induct[where F=A and P="% A. (a \ A \ (\ x \ A. f x) = f a + (\ x \ (A - {a}). f x))"]) -apply (auto simp add: insert_Diff_if add_ac) -done - lemma setsum_diff1_ring: assumes "finite A" "a \ A" shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)" -unfolding setsum_diff1'[OF assms] by auto + unfolding setsum.remove [OF assms] by auto lemma setsum_product: fixes f :: "'a => ('b::semiring_0)" shows "setsum f A * setsum g B = (\i\A. \j\B. f i * g j)" - by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute) + by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum.commute) lemma setsum_mult_setsum_if_inj: fixes f :: "'a => ('b::semiring_0)" shows "inj_on (%(a,b). f a * g b) (A \ B) ==> setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}" -by(auto simp: setsum_product setsum_cartesian_product - intro!: setsum_reindex_cong[symmetric]) +by(auto simp: setsum_product setsum.cartesian_product + intro!: setsum.reindex_cong[symmetric]) lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a" apply (case_tac "finite A") @@ -909,7 +848,7 @@ lemma setsum_Un_nat: "finite A ==> finite B ==> (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)" -- {* For the natural numbers, we have subtraction. *} -by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps) +by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps) lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) = (if a:A then setsum f A - f a else setsum f A)" @@ -993,7 +932,7 @@ shows "card (UNION I A) = (\i\I. card(A i))" proof - have "(\i\I. card (A i)) = (\i\I. \x\A i. 1)" by simp - with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant) + with assms show ?thesis by (simp add: card_eq_setsum setsum.UNION_disjoint del: setsum_constant) qed lemma card_Union_disjoint: @@ -1004,13 +943,32 @@ apply simp_all done +lemma setsum_multicount_gen: + assumes "finite s" "finite t" "\j\t. (card {i\s. R i j} = k j)" + shows "setsum (\i. (card {j\t. R i j})) s = setsum k t" (is "?l = ?r") +proof- + have "?l = setsum (\i. setsum (\x.1) {j\t. R i j}) s" by auto + also have "\ = ?r" unfolding setsum.commute_restrict [OF assms(1-2)] + using assms(3) by auto + finally show ?thesis . +qed + +lemma setsum_multicount: + assumes "finite S" "finite T" "\j\T. (card {i\S. R i j} = k)" + shows "setsum (\i. card {j\T. R i j}) S = k * card T" (is "?l = ?r") +proof- + have "?l = setsum (\i. k) T" by (rule setsum_multicount_gen) (auto simp: assms) + also have "\ = ?r" by (simp add: mult_commute) + finally show ?thesis by auto +qed + subsubsection {* Cardinality of products *} lemma card_SigmaI [simp]: "\ finite A; ALL a:A. finite (B a) \ \ card (SIGMA x: A. B x) = (\a\A. card (B a))" -by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant) +by(simp add: card_eq_setsum setsum.Sigma del:setsum_constant) (* lemma SigmaI_insert: "y \ A ==> @@ -1075,124 +1033,6 @@ "PROD x|P. t" => "CONST setprod (%x. t) {x. P}" "\x|P. t" => "CONST setprod (%x. t) {x. P}" -text {* TODO These are candidates for generalization *} - -context comm_monoid_mult -begin - -lemma setprod_reindex_id: - "inj_on f B ==> setprod f B = setprod id (f ` B)" - by (auto simp add: setprod.reindex) - -lemma setprod_reindex_cong: - "inj_on f A ==> B = f ` A ==> g = h \ f ==> setprod h B = setprod g A" - by (frule setprod.reindex, simp) - -lemma strong_setprod_reindex_cong: - "inj_on f A \ B = f ` A \ (\x. x \ A \ g x = (h \ f) x) \ setprod h B = setprod g A" - by (subst setprod.reindex_bij_betw[symmetric, where h=f]) - (auto simp: bij_betw_def) - -lemma setprod_Union_disjoint: - assumes "\A\C. finite A" "\A\C. \B\C. A \ B \ A Int B = {}" - shows "setprod f (Union C) = setprod (setprod f) C" - using assms by (fact setprod.Union_disjoint) - -text{*Here we can eliminate the finiteness assumptions, by cases.*} -lemma setprod_cartesian_product: - "(\x\A. (\y\ B. f x y)) = (\(x,y)\(A <*> B). f x y)" - by (fact setprod.cartesian_product) - -lemma setprod_Un2: - assumes "finite (A \ B)" - shows "setprod f (A \ B) = setprod f (A - B) * setprod f (B - A) * setprod f (A \ B)" -proof - - have "A \ B = A - B \ (B - A) \ A \ B" - by auto - with assms show ?thesis by simp (subst setprod.union_disjoint, auto)+ -qed - -end - -text {* TODO These are legacy *} - -lemma setprod_empty: "setprod f {} = 1" - by (fact setprod.empty) - -lemma setprod_insert: "[| finite A; a \ A |] ==> - setprod f (insert a A) = f a * setprod f A" - by (fact setprod.insert) - -lemma setprod_infinite: "~ finite A ==> setprod f A = 1" - by (fact setprod.infinite) - -lemma setprod_reindex: - "inj_on f B ==> setprod h (f ` B) = setprod (h \ f) B" - by (fact setprod.reindex) - -lemma setprod_cong: - "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B" - by (fact setprod.cong) - -lemma strong_setprod_cong: - "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B" - by (fact setprod.strong_cong) - -lemma setprod_Un_one: - "\ finite S; finite T; \x \ S\T. f x = 1 \ - \ setprod f (S \ T) = setprod f S * setprod f T" - by (fact setprod.union_inter_neutral) - -lemmas setprod_1 = setprod.neutral_const -lemmas setprod_1' = setprod.neutral - -lemma setprod_Un_Int: "finite A ==> finite B - ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B" - by (fact setprod.union_inter) - -lemma setprod_Un_disjoint: "finite A ==> finite B - ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B" - by (fact setprod.union_disjoint) - -lemma setprod_subset_diff: "\ B \ A; finite A \ \ - setprod f A = setprod f (A - B) * setprod f B" - by (fact setprod.subset_diff) - -lemma setprod_mono_one_left: - "\ finite T; S \ T; \i \ T - S. f i = 1 \ \ setprod f S = setprod f T" - by (fact setprod.mono_neutral_left) - -lemmas setprod_mono_one_right = setprod.mono_neutral_right - -lemma setprod_mono_one_cong_left: - "\ finite T; S \ T; \i \ T - S. g i = 1; \x. x \ S \ f x = g x \ - \ setprod f S = setprod g T" - by (fact setprod.mono_neutral_cong_left) - -lemmas setprod_mono_one_cong_right = setprod.mono_neutral_cong_right - -lemma setprod_delta: "finite S \ - setprod (\k. if k=a then b k else 1) S = (if a \ S then b a else 1)" - by (fact setprod.delta) - -lemma setprod_delta': "finite S \ - setprod (\k. if a = k then b k else 1) S = (if a\ S then b a else 1)" - by (fact setprod.delta') - -lemma setprod_UN_disjoint: - "finite I ==> (ALL i:I. finite (A i)) ==> - (ALL i:I. ALL j:I. i \ j --> A i Int A j = {}) ==> - setprod f (UNION I A) = setprod (%i. setprod f (A i)) I" - by (fact setprod.UNION_disjoint) - -lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==> - (\x\A. (\y\ B x. f x y)) = - (\(x,y)\(SIGMA x:A. B x). f x y)" - by (fact setprod.Sigma) - -lemma setprod_timesf: "setprod (\x. f x * g x) A = setprod f A * setprod g A" - by (fact setprod.distrib) - subsubsection {* Properties in more restricted classes of structures *} @@ -1210,7 +1050,7 @@ lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \ 0) ==> (setprod f (A Un B) :: 'a ::{field}) = setprod f A * setprod f B / setprod f (A Int B)" -by (subst setprod_Un_Int [symmetric], auto) +by (subst setprod.union_inter [symmetric], auto) lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) \ f x) --> 0 \ setprod f A" @@ -1238,9 +1078,9 @@ "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \ g) x) A") apply (erule ssubst) apply (subst divide_inverse) -apply (subst setprod_timesf) +apply (subst setprod.distrib) apply (subst setprod_inversef, assumption+, rule refl) -apply (rule setprod_cong, rule refl) +apply (rule setprod.cong, rule refl) apply (subst divide_inverse, auto) done @@ -1257,8 +1097,8 @@ "finite B \ A <= B \ setprod f A dvd setprod f B" apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)") apply (unfold dvd_def, blast) - apply (subst setprod_Un_disjoint [symmetric]) - apply (auto elim: finite_subset intro: setprod_cong) + apply (subst setprod.union_disjoint [symmetric]) + apply (auto elim: finite_subset intro: setprod.cong) done lemma setprod_dvd_setprod_subset2: @@ -1290,7 +1130,7 @@ proof (induct A rule: finite_subset_induct) case (insert a F) thus "setprod f (insert a F) \ setprod g (insert a F)" "0 \ setprod f (insert a F)" - unfolding setprod_insert[OF insert(1,3)] + unfolding setprod.insert[OF insert(1,3)] using assms[rule_format,OF insert(2)] insert by (auto intro: mult_mono) qed auto diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Hoare_Parallel/OG_Examples.thy --- a/src/HOL/Hoare_Parallel/OG_Examples.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Sat Jun 28 09:16:42 2014 +0200 @@ -534,9 +534,9 @@ COEND \\x=n\" apply oghoare -apply (simp_all cong del: strong_setsum_cong) +apply (simp_all cong del: setsum.strong_cong) apply (tactic {* ALLGOALS (clarify_tac @{context}) *}) -apply (simp_all cong del: strong_setsum_cong) +apply (simp_all cong del: setsum.strong_cong) apply(erule (1) Example2_lemma2) apply(erule (1) Example2_lemma2) apply(erule (1) Example2_lemma2) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy Sat Jun 28 09:16:42 2014 +0200 @@ -182,12 +182,12 @@ have "setsum f A = setsum f ((A-{a}) \ {a})" by(simp add:insert_absorb[OF `a:A`]) also have "\ = setsum f (A-{a}) + setsum f {a}" - using `finite A` by(subst setsum_Un_disjoint) auto + using `finite A` by(subst setsum.union_disjoint) auto also have "setsum f (A-{a}) \ setsum g (A-{a})" by(rule setsum_mono)(simp add: assms(2)) also have "setsum f {a} < setsum g {a}" using a by simp also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \ {a})" - using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto + using `finite A` by(subst setsum.union_disjoint[symmetric]) auto also have "\ = setsum g A" by(simp add:insert_absorb[OF `a:A`]) finally show ?thesis by (metis add_right_mono add_strict_left_mono) qed @@ -241,7 +241,7 @@ also have "\ \ (\y\?X'-{u}. m(?f y)+1)" by(simp add: setsum_mono3[OF _ `?Y'\?X-{u} <= ?X'-{u}`]) also have "\ + (\y\{u}. m(?f y)+1)= (\y\(?X'-{u}) \ {u}. m(?f y)+1)" - using `u:?X'` by(subst setsum_Un_disjoint[symmetric]) auto + using `u:?X'` by(subst setsum.union_disjoint[symmetric]) auto also have "\ = (\x\?X'. m(?f x)+1)" using `u : ?X'` by(simp add:insert_absorb) finally show ?thesis by (blast intro: add_right_mono) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Sat Jun 28 09:16:42 2014 +0200 @@ -319,7 +319,7 @@ have "(\y\?Y. m_ivl(?g y)) = (\y\(?Y-?X) \ (?Y\?X). m_ivl(?g y))" by (metis Un_Diff_Int) also have "\ = (\y\?Y-?X. m_ivl(?g y)) + (\y\?Y\?X. m_ivl(?g y))" - by(subst setsum_Un_disjoint) auto + by(subst setsum.union_disjoint) auto also have "(\y\?Y-?X. m_ivl(?g y)) = 0" using 0 by simp also have "0 + (\y\?Y\?X. m_ivl(?g y)) = (\y\?Y\?X. m_ivl(?g y))" by simp also have "\ \ (\y\?Y\?X. m_ivl(?f y))" diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Library/BigO.thy --- a/src/HOL/Library/BigO.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Library/BigO.thy Sat Jun 28 09:16:42 2014 +0200 @@ -641,7 +641,8 @@ apply (erule ssubst) apply (erule bigo_setsum3) apply (rule ext) - apply (rule setsum_cong2) + apply (rule setsum.cong) + apply (rule refl) apply (subst abs_of_nonneg) apply auto done diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Library/Convex.thy --- a/src/HOL/Library/Convex.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Library/Convex.thy Sat Jun 28 09:16:42 2014 +0200 @@ -200,7 +200,7 @@ then have card: "card ({1 :: nat .. 2} \ - {x. x = 1}) = 1" by simp then have "setsum ?u {1 .. 2} = 1" - using setsum_cases[of "{(1 :: nat) .. 2}" "\ x. x = 1" "\ x. \" "\ x. 1 - \"] + using setsum.If_cases[of "{(1 :: nat) .. 2}" "\ x. x = 1" "\ x. \" "\ x. 1 - \"] by auto with asm[rule_format, of "2" ?u ?x] have s: "(\j \ {1..2}. ?u j *\<^sub>R ?x j) \ s" using mu xy by auto @@ -270,7 +270,7 @@ by simp show "(\x\t. u x *\<^sub>R x) \ s" using sum[THEN spec[where x="\x. if x\t then u x else 0"]] as * - by (auto simp: assms setsum_cases if_distrib if_distrib_arg) + by (auto simp: assms setsum.If_cases if_distrib if_distrib_arg) qed (erule_tac x=s in allE, erule_tac x=u in allE, auto) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Library/FSet.thy Sat Jun 28 09:16:42 2014 +0200 @@ -1002,7 +1002,7 @@ lemma fset_size_o_map: "inj f \ size_fset g \ fimage f = size_fset (g \ f)" unfolding size_fset_def fimage_def - by (auto simp: Abs_fset_inverse setsum_reindex_cong[OF subset_inj_on[OF _ top_greatest]]) + by (auto simp: Abs_fset_inverse setsum.reindex_cong[OF subset_inj_on[OF _ top_greatest]]) setup {* BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset} diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Sat Jun 28 09:16:42 2014 +0200 @@ -143,7 +143,7 @@ and f :: "nat \ nat \ nat \ 'a::comm_monoid_add" shows "(\j=0..k. \i=0..j. f i (j - i) (n - j)) = (\j=0..k. \i=0..k - j. f j i (n - j - i))" - by (induct k) (simp_all add: Suc_diff_le setsum_addf add_assoc) + by (induct k) (simp_all add: Suc_diff_le setsum.distrib add_assoc) instance fps :: (semiring_0) semigroup_mult proof @@ -194,8 +194,8 @@ instance fps :: (semiring_1) monoid_mult proof fix a :: "'a fps" - show "1 * a = a" by (simp add: fps_ext fps_mult_nth mult_delta_left setsum_delta) - show "a * 1 = a" by (simp add: fps_ext fps_mult_nth mult_delta_right setsum_delta') + show "1 * a = a" by (simp add: fps_ext fps_mult_nth mult_delta_left setsum.delta) + show "a * 1 = a" by (simp add: fps_ext fps_mult_nth mult_delta_right setsum.delta') qed instance fps :: (cancel_semigroup_add) cancel_semigroup_add @@ -235,9 +235,9 @@ proof fix a b c :: "'a fps" show "(a + b) * c = a * c + b * c" - by (simp add: expand_fps_eq fps_mult_nth distrib_right setsum_addf) + by (simp add: expand_fps_eq fps_mult_nth distrib_right setsum.distrib) show "a * (b + c) = a * b + a * c" - by (simp add: expand_fps_eq fps_mult_nth distrib_left setsum_addf) + by (simp add: expand_fps_eq fps_mult_nth distrib_left setsum.distrib) qed instance fps :: (semiring_0) semiring_0 @@ -306,7 +306,7 @@ by (simp add: fps_ext) lemma fps_const_mult[simp]: "fps_const (c::'a::ring) * fps_const d = fps_const (c * d)" - by (simp add: fps_eq_iff fps_mult_nth setsum_0') + by (simp add: fps_eq_iff fps_mult_nth setsum.neutral) lemma fps_const_add_left: "fps_const (c::'a::monoid_add) + f = Abs_fps (\n. if n = 0 then c + f$0 else f$n)" @@ -318,17 +318,17 @@ lemma fps_const_mult_left: "fps_const (c::'a::semiring_0) * f = Abs_fps (\n. c * f$n)" unfolding fps_eq_iff fps_mult_nth - by (simp add: fps_const_def mult_delta_left setsum_delta) + by (simp add: fps_const_def mult_delta_left setsum.delta) lemma fps_const_mult_right: "f * fps_const (c::'a::semiring_0) = Abs_fps (\n. f$n * c)" unfolding fps_eq_iff fps_mult_nth - by (simp add: fps_const_def mult_delta_right setsum_delta') + by (simp add: fps_const_def mult_delta_right setsum.delta') lemma fps_mult_left_const_nth [simp]: "(fps_const (c::'a::semiring_1) * f)$n = c* f$n" - by (simp add: fps_mult_nth mult_delta_left setsum_delta) + by (simp add: fps_mult_nth mult_delta_left setsum.delta) lemma fps_mult_right_const_nth [simp]: "(f * fps_const (c::'a::semiring_1))$n = f$n * c" - by (simp add: fps_mult_nth mult_delta_right setsum_delta') + by (simp add: fps_mult_nth mult_delta_right setsum.delta') subsection {* Formal power series form an integral domain*} @@ -350,9 +350,9 @@ have "(a * b) $ (i+j) = (\k=0..i+j. a$k * b$(i+j-k))" by (rule fps_mult_nth) also have "\ = (a$i * b$(i+j-i)) + (\k\{0..i+j}-{i}. a$k * b$(i+j-k))" - by (rule setsum_diff1') simp_all + by (rule setsum.remove) simp_all also have "(\k\{0..i+j}-{i}. a$k * b$(i+j-k)) = 0" - proof (rule setsum_0' [rule_format]) + proof (rule setsum.neutral [rule_format]) fix k assume "k \ {0..i+j} - {i}" then have "k < i \ i+j-k < j" by auto then show "a$k * b$(i+j-k) = 0" using i j by auto @@ -388,7 +388,7 @@ have "(X * f) $n = (\i = 0..n. X $ i * f $ (n - i))" by (simp add: fps_mult_nth) also have "\ = f $ (n - 1)" - using False by (simp add: X_def mult_delta_left setsum_delta) + using False by (simp add: X_def mult_delta_left setsum.delta) finally show ?thesis using False by simp next case True @@ -577,7 +577,7 @@ lemma fps_sum_rep_nth: "(setsum (\i. fps_const(a$i)*X^i) {0..m})$n = (if n \ m then a$n else 0::'a::comm_ring_1)" apply (auto simp add: fps_setsum_nth cond_value_iff cong del: if_weak_cong) - apply (simp add: setsum_delta') + apply (simp add: setsum.delta') done lemma fps_notation: "(\n. setsum (\i. fps_const(a$i) * X^i) {0..n}) ----> a" @@ -631,7 +631,7 @@ subsection{* Inverses of formal power series *} -declare setsum_cong[fundef_cong] +declare setsum.cong[fundef_cong] instantiation fps :: ("{comm_monoid_add, inverse, times, uminus}") inverse begin @@ -756,10 +756,10 @@ let ?g = "\i. if i = n then 1 else if i=n - 1 then - 1 else 0" let ?h = "\i. if i=n - 1 then - 1 else 0" have th1: "setsum ?f {0..n} = setsum ?g {0..n}" - by (rule setsum_cong2) auto + by (rule setsum.cong) auto have th2: "setsum ?g {0..n - 1} = setsum ?h {0..n - 1}" apply (insert n) - apply (rule setsum_cong2) + apply (rule setsum.cong) apply auto done have eq: "{0 .. n} = {0.. n - 1} \ {n}" @@ -770,9 +770,9 @@ by auto show "setsum ?f {0..n} = 0" unfolding th1 - apply (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def) + apply (simp add: setsum.union_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def) unfolding th2 - apply (simp add: setsum_delta) + apply (simp add: setsum.delta) done qed @@ -811,15 +811,15 @@ have "(f * ?D g + ?D f * g)$n = (?D g * f + ?D f * g)$n" by (simp only: mult_commute) also have "\ = (\i = 0..n. ?g i)" - by (simp add: fps_mult_nth setsum_addf[symmetric]) + by (simp add: fps_mult_nth setsum.distrib[symmetric]) also have "\ = setsum ?h {0..n+1}" by (rule setsum.reindex_bij_witness_not_neutral [where S'="{}" and T'="{0}" and j="Suc" and i="\i. i - 1"]) auto also have "\ = (fps_deriv (f * g)) $ n" - apply (simp only: fps_deriv_nth fps_mult_nth setsum_addf) + apply (simp only: fps_deriv_nth fps_mult_nth setsum.distrib) unfolding s0 s1 - unfolding setsum_addf[symmetric] setsum_right_distrib - apply (rule setsum_cong2) + unfolding setsum.distrib[symmetric] setsum_right_distrib + apply (rule setsum.cong) apply (auto simp add: of_nat_diff field_simps) done finally have "(f * ?D g + ?D f * g) $ n = ?D (f*g) $ n" . @@ -1030,7 +1030,7 @@ also have "\ = (\i = 0..m. a ^ l $ i * a $ (m - i))" by (simp add: fps_mult_nth) also have "\ = 0" - apply (rule setsum_0') + apply (rule setsum.neutral) apply auto apply (case_tac "x = m") using a0 apply simp @@ -1052,7 +1052,7 @@ assumes a0: "a $0 = (0::'a::idom)" and kn: "n \ k" shows "setsum (\i. (a ^ i)$k) {0 .. n} = setsum (\i. (a ^ i)$k) {0 .. k}" - apply (rule setsum_mono_zero_right) + apply (rule setsum.mono_neutral_right) using kn apply auto apply (rule startsby_zero_power_prefix[rule_format, OF a0]) @@ -1072,7 +1072,7 @@ also have "\ = setsum (\i. a^n$i * a $ (Suc n - i)) {0.. Suc n}" by (simp add: fps_mult_nth) also have "\ = setsum (\i. a^n$i * a $ (Suc n - i)) {n .. Suc n}" - apply (rule setsum_mono_zero_right) + apply (rule setsum.mono_neutral_right) apply simp apply clarsimp apply clarsimp @@ -1255,11 +1255,11 @@ by (simp add: fps_compose_def) lemma fps_compose_X[simp]: "a oo X = (a :: 'a::comm_ring_1 fps)" - by (simp add: fps_ext fps_compose_def mult_delta_right setsum_delta') + by (simp add: fps_ext fps_compose_def mult_delta_right setsum.delta') lemma fps_const_compose[simp]: "fps_const (a::'a::comm_ring_1) oo b = fps_const a" - by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta) + by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum.delta) lemma numeral_compose[simp]: "(numeral k :: 'a::comm_ring_1 fps) oo b = numeral k" unfolding numeral_fps_const by simp @@ -1268,7 +1268,7 @@ unfolding neg_numeral_fps_const by simp lemma X_fps_compose_startby0[simp]: "a$0 = 0 \ X oo a = (a :: 'a::comm_ring_1 fps)" - by (simp add: fps_eq_iff fps_compose_def mult_delta_left setsum_delta not_le) + by (simp add: fps_eq_iff fps_compose_def mult_delta_left setsum.delta not_le) subsection {* Rules from Herbert Wilf's Generatingfunctionology*} @@ -1374,10 +1374,10 @@ by (simp add: fps_mult_nth) also have "\ = a$n" unfolding th0 - unfolding setsum_Un_disjoint[OF f(1) finite_UnI[OF f(2,3)] d(1), unfolded u(1)] - unfolding setsum_Un_disjoint[OF f(2) f(3) d(2)] + unfolding setsum.union_disjoint[OF f(1) finite_UnI[OF f(2,3)] d(1), unfolded u(1)] + unfolding setsum.union_disjoint[OF f(2) f(3) d(2)] apply (simp) - unfolding setsum_Un_disjoint[OF f(4,5) d(3), unfolded u(3)] + unfolding setsum.union_disjoint[OF f(4,5) d(3), unfolded u(3)] apply simp done finally have "a$n = ((1 - X) * ?sa) $ n" @@ -1532,7 +1532,7 @@ apply (auto simp add: atLeastLessThanSuc_atLeastAtMost listsum_setsum_nth) done also have "\ = n + setsum (nth xs) ({0..k} - {i})" - unfolding setsum_Un_disjoint[OF f d, unfolded eqs] using i by simp + unfolding setsum.union_disjoint[OF f d, unfolded eqs] using i by simp finally have zxs: "\ j\ {0..k} - {i}. xs!j = 0" by auto from H have xsl: "length xs = k+1" @@ -1565,8 +1565,8 @@ have "listsum ?xs = setsum (nth ?xs) {0.. = setsum (\j. if j = i then n else 0) {0..< k+1}" - by (rule setsum_cong2) (simp del: replicate.simps) - also have "\ = n" using i by (simp add: setsum_delta) + by (rule setsum.cong) (simp_all del: replicate.simps) + also have "\ = n" using i by (simp add: setsum.delta) finally have "?xs \ natpermute n (k+1)" using xsl unfolding natpermute_def mem_Collect_eq by blast then have "?xs \ ?A" @@ -1600,14 +1600,14 @@ have f0: "finite {0 .. k}" "finite {m}" by auto have d0: "{0 .. k} \ {m} = {}" using Suc by auto have "(setprod a {0 .. m}) $ n = (setprod a {0 .. k} * a m) $ n" - unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0] by simp + unfolding setprod.union_disjoint[OF f0 d0, unfolded u0] by simp also have "\ = (\i = 0..n. (\v\natpermute i (k + 1). \j\{0..k}. a j $ v ! j) * a m $ (n - i))" unfolding fps_mult_nth H[rule_format, OF km] .. also have "\ = (\v\natpermute n (m + 1). \j\{0..m}. a j $ v ! j)" apply (simp add: Suc) unfolding natpermute_split[of m "m + 1", simplified, of n, unfolded natlist_trivial_1[unfolded One_nat_def] Suc] - apply (subst setsum_UN_disjoint) + apply (subst setsum.UNION_disjoint) apply simp apply simp unfolding image_Collect[symmetric] @@ -1616,13 +1616,14 @@ apply (rule natpermute_finite) apply (clarsimp simp add: set_eq_iff) apply auto - apply (rule setsum_cong2) + apply (rule setsum.cong) + apply (rule refl) unfolding setsum_left_distrib apply (rule sym) - apply (rule_tac f="\xs. xs @[n - x]" in setsum_reindex_cong) + apply (rule_tac l = "\xs. xs @ [n - x]" in setsum.reindex_cong) apply (simp add: inj_on_def) apply auto - unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0, unfolded Suc] + unfolding setprod.union_disjoint[OF f0 d0, unfolded u0, unfolded Suc] apply (clarsimp simp add: natpermute_def nth_append) done finally show ?thesis . @@ -1692,16 +1693,16 @@ have eq: "{0 .. n1} \ {n} = {0 .. n}" using n1 by auto have d: "{0 .. n1} \ {n} = {}" using n1 by auto have seq: "(\i = 0..n1. b $ i * a ^ i $ n) = (\i = 0..n1. c $ i * a ^ i $ n)" - apply (rule setsum_cong2) + apply (rule setsum.cong) using H n1 apply auto done have th0: "(b oo a) $n = (\i = 0..n1. c $ i * a ^ i $ n) + b$n * (a$1)^n" - unfolding fps_compose_nth setsum_Un_disjoint[OF f d, unfolded eq] seq + unfolding fps_compose_nth setsum.union_disjoint[OF f d, unfolded eq] seq using startsby_zero_power_nth_same[OF a0] by simp have th1: "(c oo a) $n = (\i = 0..n1. c $ i * a ^ i $ n) + c$n * (a$1)^n" - unfolding fps_compose_nth setsum_Un_disjoint[OF f d, unfolded eq] + unfolding fps_compose_nth setsum.union_disjoint[OF f d, unfolded eq] using startsby_zero_power_nth_same[OF a0] by simp from h[unfolded fps_eq_iff, rule_format, of n] th0 th1 a1 @@ -1715,7 +1716,7 @@ subsection {* Radicals *} -declare setprod_cong [fundef_cong] +declare setprod.cong [fundef_cong] function radical :: "(nat \ 'a \ 'a) \ nat \ 'a::field fps \ nat \ 'a" where @@ -1752,8 +1753,8 @@ also have "\ = setsum (nth xs) {0.. = xs!i + setsum (nth xs) {0..j\{0..h}. fps_radical r k a $ (replicate k 0) ! j)" unfolding fps_power_nth Suc by simp also have "\ = (\j\{0..h}. r k (a$0))" - apply (rule setprod_cong) + apply (rule setprod.cong) apply simp using Suc apply (subgoal_tac "replicate k 0 ! x = 0") @@ -1865,7 +1866,7 @@ by (metis natpermute_finite)+ let ?f = "\v. \j\{0..k}. ?r $ v ! j" have "setsum ?f ?Pnkn = setsum (\v. ?r $ n * r (Suc k) (a $ 0) ^ k) ?Pnkn" - proof (rule setsum_cong2) + proof (rule setsum.cong) fix v assume v: "v \ {xs \ natpermute n (k + 1). n \ set xs}" let ?ths = "(\j\{0..k}. fps_radical r (Suc k) a $ v ! j) = fps_radical r (Suc k) a $ n * r (Suc k) (a $ 0) ^ k" @@ -1873,21 +1874,21 @@ unfolding natpermute_contain_maximal by auto have "(\j\{0..k}. fps_radical r (Suc k) a $ v ! j) = (\j\{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))" - apply (rule setprod_cong, simp) + apply (rule setprod.cong, simp) using i r0 apply (simp del: replicate.simps) done also have "\ = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k" using i r0 by (simp add: setprod_gen_delta) finally show ?ths . - qed + qed rule then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k" by (simp add: natpermute_max_card[OF nz, simplified]) also have "\ = a$n - setsum ?f ?Pnknn" unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc) finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" . have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" - unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] .. + unfolding fps_power_nth_Suc setsum.union_disjoint[OF f d, unfolded eq] .. also have "\ = a$n" unfolding fn by simp finally have "?r ^ Suc k $ n = a $n" . } @@ -1934,13 +1935,13 @@ by (metis natpermute_finite)+ let ?f = "\v. \j\{0..k}. ?r $ v ! j" have "setsum ?f ?Pnkn = setsum (\v. ?r $ n * r (Suc k) (a $ 0) ^ k) ?Pnkn" - proof(rule setsum_cong2) + proof(rule setsum.cong2) fix v assume v: "v \ {xs \ natpermute n (k + 1). n \ set xs}" let ?ths = "(\j\{0..k}. fps_radical r (Suc k) a $ v ! j) = fps_radical r (Suc k) a $ n * r (Suc k) (a $ 0) ^ k" from v obtain i where i: "i \ {0..k}" "v = replicate (k+1) 0 [i:= n]" unfolding natpermute_contain_maximal by auto have "(\j\{0..k}. fps_radical r (Suc k) a $ v ! j) = (\j\{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))" - apply (rule setprod_cong, simp) + apply (rule setprod.cong, simp) using i r0 by (simp del: replicate.simps) also have "\ = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k" unfolding setprod_gen_delta[OF fK] using i r0 by simp @@ -1952,7 +1953,7 @@ unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc ) finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" . have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" - unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] .. + unfolding fps_power_nth_Suc setsum.union_disjoint[OF f d, unfolded eq] .. also have "\ = a$n" unfolding fn by simp finally have "?r ^ Suc k $ n = a $n" .} ultimately show "?r ^ Suc k $ n = a $n" by (cases n, auto) @@ -2010,7 +2011,7 @@ let ?f = "\v. \j\{0..k}. ?r $ v ! j" let ?g = "\v. \j\{0..k}. a $ v ! j" have "setsum ?g ?Pnkn = setsum (\v. a $ n * (?r$0)^k) ?Pnkn" - proof (rule setsum_cong2) + proof (rule setsum.cong) fix v assume v: "v \ {xs \ natpermute n (Suc k). n \ set xs}" let ?ths = "(\j\{0..k}. a $ v ! j) = a $ n * (?r$0)^k" @@ -2018,18 +2019,18 @@ unfolding Suc_eq_plus1 natpermute_contain_maximal by (auto simp del: replicate.simps) have "(\j\{0..k}. a $ v ! j) = (\j\{0..k}. if j = i then a $ n else r (Suc k) (b$0))" - apply (rule setprod_cong, simp) + apply (rule setprod.cong, simp) using i a0 apply (simp del: replicate.simps) done also have "\ = a $ n * (?r $ 0)^k" using i by (simp add: setprod_gen_delta) finally show ?ths . - qed + qed rule then have th0: "setsum ?g ?Pnkn = of_nat (k+1) * a $ n * (?r $ 0)^k" by (simp add: natpermute_max_card[OF nz, simplified]) have th1: "setsum ?g ?Pnknn = setsum ?f ?Pnknn" - proof (rule setsum_cong2, rule setprod_cong, simp) + proof (rule setsum.cong, rule refl, rule setprod.cong, simp) fix xs i assume xs: "xs \ ?Pnknn" and i: "i \ {0..k}" { @@ -2048,8 +2049,8 @@ also have "\ = setsum (nth xs) {0.. = xs!i + setsum (nth xs) {0.. = of_nat (k+1) * a $ n * (?r $ 0)^k + setsum ?f ?Pnknn" unfolding th0 th1 .. @@ -2283,12 +2284,12 @@ also have "\ = setsum (\i. of_nat i * a$i * (setsum (\j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {0.. Suc n}" unfolding fps_mult_nth .. also have "\ = setsum (\i. of_nat i * a$i * (setsum (\j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {1.. Suc n}" - apply (rule setsum_mono_zero_right) - apply (auto simp add: mult_delta_left setsum_delta not_le) + apply (rule setsum.mono_neutral_right) + apply (auto simp add: mult_delta_left setsum.delta not_le) done also have "\ = setsum (\i. of_nat (i + 1) * a$(i+1) * (setsum (\j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" unfolding fps_deriv_nth - by (rule setsum_reindex_cong [where f = Suc]) (auto simp add: mult_assoc) + by (rule setsum.reindex_cong [of Suc]) (auto simp add: mult_assoc) finally have th0: "(fps_deriv (a oo b))$n = setsum (\i. of_nat (i + 1) * a$(i+1) * (setsum (\j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" . @@ -2296,8 +2297,9 @@ unfolding fps_mult_nth by (simp add: mult_ac) also have "\ = setsum (\i. setsum (\j. of_nat (n - i +1) * b$(n - i + 1) * of_nat (j + 1) * a$(j+1) * (b^j)$i) {0..n}) {0..n}" unfolding fps_deriv_nth fps_compose_nth setsum_right_distrib mult_assoc - apply (rule setsum_cong2) - apply (rule setsum_mono_zero_left) + apply (rule setsum.cong) + apply (rule refl) + apply (rule setsum.mono_neutral_left) apply (simp_all add: subset_eq) apply clarify apply (subgoal_tac "b^i$x = 0") @@ -2307,8 +2309,8 @@ done also have "\ = setsum (\i. of_nat (i + 1) * a$(i+1) * (setsum (\j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" unfolding setsum_right_distrib - apply (subst setsum_commute) - apply (rule setsum_cong2)+ + apply (subst setsum.commute) + apply (rule setsum.cong, rule refl)+ apply simp done finally have "(fps_deriv (a oo b))$n = (((fps_deriv a) oo b) * (fps_deriv b)) $n" @@ -2328,7 +2330,7 @@ have "((1+X)*a) $n = setsum (\i. (1+X)$i * a$(n-i)) {0..n}" by (simp add: fps_mult_nth) also have "\ = setsum (\i. (1+X)$i * a$(n-i)) {0.. 1}" - unfolding Suc by (rule setsum_mono_zero_right) auto + unfolding Suc by (rule setsum.mono_neutral_right) auto also have "\ = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))" by (simp add: Suc) finally show ?thesis . @@ -2345,7 +2347,7 @@ fix i have "a$i = ?r$i" unfolding fps_setsum_nth fps_mult_left_const_nth X_power_nth - by (simp add: mult_delta_right setsum_delta' z) + by (simp add: mult_delta_right setsum.delta' z) } then show ?thesis unfolding fps_eq_iff by blast qed @@ -2444,16 +2446,16 @@ done lemma fps_compose_1[simp]: "1 oo a = 1" - by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta) + by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum.delta) lemma fps_compose_0[simp]: "0 oo a = 0" by (simp add: fps_eq_iff fps_compose_nth) lemma fps_compose_0_right[simp]: "a oo 0 = fps_const (a$0)" - by (auto simp add: fps_eq_iff fps_compose_nth power_0_left setsum_0') + by (auto simp add: fps_eq_iff fps_compose_nth power_0_left setsum.neutral) lemma fps_compose_add_distrib: "(a + b) oo c = (a oo c) + (b oo c)" - by (simp add: fps_eq_iff fps_compose_nth field_simps setsum_addf) + by (simp add: fps_eq_iff fps_compose_nth field_simps setsum.distrib) lemma fps_compose_setsum_distrib: "(setsum f S) oo a = setsum (\i. f i oo a) S" proof (cases "finite S") @@ -2493,15 +2495,16 @@ done have "?r = setsum (\i. setsum (\(k,m). a$k * (c^k)$i * b$m * (d^m) $ (n - i)) {(k,m). k + m \ n}) {0..n}" apply (simp add: fps_mult_nth setsum_right_distrib) - apply (subst setsum_commute) - apply (rule setsum_cong2) + apply (subst setsum.commute) + apply (rule setsum.cong) apply (auto simp add: field_simps) done also have "\ = ?l" apply (simp add: fps_mult_nth fps_compose_nth setsum_product) - apply (rule setsum_cong2) - apply (simp add: setsum_cartesian_product mult_assoc) - apply (rule setsum_mono_zero_right[OF f]) + apply (rule setsum.cong) + apply (rule refl) + apply (simp add: setsum.cartesian_product mult_assoc) + apply (rule setsum.mono_neutral_right[OF f]) apply (simp add: subset_eq) apply presburger apply clarsimp @@ -2524,8 +2527,8 @@ shows "((a oo c) * (b oo d))$n = setsum (\k. setsum (\m. a$k * b$m * (c^k * d^m) $ n) {0..n}) {0..n}" (is "?l = ?r") unfolding product_composition_lemma[OF c0 d0] - unfolding setsum_cartesian_product - apply (rule setsum_mono_zero_left) + unfolding setsum.cartesian_product + apply (rule setsum.mono_neutral_left) apply simp apply (clarsimp simp add: subset_eq) apply clarsimp @@ -2533,7 +2536,7 @@ apply (subgoal_tac "(c^aa * d^ba) $ n = 0") apply simp unfolding fps_mult_nth - apply (rule setsum_0') + apply (rule setsum.neutral) apply (clarsimp simp add: not_le) apply (case_tac "x < aa") apply (rule startsby_zero_power_prefix[OF c0, rule_format]) @@ -2558,9 +2561,9 @@ done show "?l = ?r " unfolding th0 - apply (subst setsum_UN_disjoint) + apply (subst setsum.UNION_disjoint) apply auto - apply (subst setsum_UN_disjoint) + apply (subst setsum.UNION_disjoint) apply auto done qed @@ -2613,7 +2616,7 @@ using fps_compose_add_distrib [of a "- b" c] by (simp add: fps_compose_uminus) lemma X_fps_compose: "X oo a = Abs_fps (\n. if n = 0 then (0::'a::comm_ring_1) else a$n)" - by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta) + by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum.delta) lemma fps_inverse_compose: assumes b0: "(b$0 :: 'a::field) = 0" @@ -2706,8 +2709,9 @@ by (simp add: fps_compose_setsum_distrib) also have "\ = ?r$n" apply (simp add: fps_compose_nth fps_setsum_nth setsum_left_distrib mult_assoc) - apply (rule setsum_cong2) - apply (rule setsum_mono_zero_right) + apply (rule setsum.cong) + apply (rule refl) + apply (rule setsum.mono_neutral_right) apply (auto simp add: not_le) apply (erule startsby_zero_power_prefix[OF b0, rule_format]) done @@ -2737,7 +2741,7 @@ { assume kn: "k \ n" then have "?l$n = ?r$n" - by (simp add: fps_compose_nth mult_delta_left setsum_delta) + by (simp add: fps_compose_nth mult_delta_left setsum.delta) } moreover have "k >n \ k\ n" by arith ultimately have "?l$n = ?r$n" by blast @@ -2978,7 +2982,7 @@ lemma Ec_E1_eq: "E (1::'a::field_char_0) oo (fps_const c * X) = E c" apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib) - apply (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong) + apply (simp add: cond_value_iff cond_application_beta setsum.delta' cong del: if_weak_cong) done text{* The generalized binomial theorem as a consequence of @{thm E_add_mult} *} @@ -2994,8 +2998,8 @@ by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib) then show ?thesis apply simp - apply (rule setsum_cong2) - apply simp + apply (rule setsum.cong) + apply simp_all apply (frule binomial_fact[where ?'a = 'a, symmetric]) apply (simp add: field_simps of_nat_mult) done @@ -3207,7 +3211,7 @@ using binomial_Vandermonde[of n n n,symmetric] unfolding mult_2 apply (simp add: power2_eq_square) - apply (rule setsum_cong2) + apply (rule setsum.cong) apply (auto intro: binomial_symmetric) done @@ -3288,19 +3292,19 @@ apply (simp add: field_simps del: fact_Suc) unfolding fact_altdef_nat id_def unfolding of_nat_setprod - unfolding setprod_timesf[symmetric] + unfolding setprod.distrib[symmetric] apply auto unfolding eq1 - apply (subst setprod_Un_disjoint[symmetric]) + apply (subst setprod.union_disjoint[symmetric]) apply (auto) - apply (rule setprod_cong) + apply (rule setprod.cong) apply auto done have th20: "?m1 n * ?p b n = setprod (\i. b - of_nat i) {0..m}" unfolding m1nk unfolding m h pochhammer_Suc_setprod - unfolding setprod_timesf[symmetric] - apply (rule setprod_cong) + unfolding setprod.distrib[symmetric] + apply (rule setprod.cong) apply auto done have th21:"pochhammer (b - of_nat n + 1) k = setprod (\i. b - of_nat i) {n - k .. n - 1}" @@ -3314,10 +3318,10 @@ pochhammer (b - of_nat n + 1) k * setprod (\i. b - of_nat i) {0.. n - k - 1}" unfolding th20 th21 unfolding h m - apply (subst setprod_Un_disjoint[symmetric]) + apply (subst setprod.union_disjoint[symmetric]) using kn' h m apply auto - apply (rule setprod_cong) + apply (rule setprod.cong) apply auto done then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k = @@ -3359,7 +3363,8 @@ unfolding gbinomial_pochhammer using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_simps) - apply (rule setsum_cong2) + apply (rule setsum.cong) + apply (rule refl) apply (drule th00(2)) apply (simp add: field_simps power_add[symmetric]) done @@ -3688,7 +3693,7 @@ have th0: "(fps_const c * X) $ 0 = 0" by simp show ?thesis unfolding gp[OF th0, symmetric] by (auto simp add: fps_eq_iff pochhammer_fact[symmetric] - fps_compose_nth power_mult_distrib cond_value_iff setsum_delta' cong del: if_weak_cong) + fps_compose_nth power_mult_distrib cond_value_iff setsum.delta' cong del: if_weak_cong) qed lemma F_B[simp]: "F [-a] [] (- 1) = fps_binomial a" @@ -3750,7 +3755,7 @@ lemma setsum_eq_if: "setsum f {(n::nat) .. m} = (if m < n then 0 else f n + setsum f {n+1 .. m})" apply simp - apply (subst setsum_insert[symmetric]) + apply (subst setsum.insert[symmetric]) apply (auto simp add: not_less setsum_head_Suc) done diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Library/Indicator_Function.thy --- a/src/HOL/Library/Indicator_Function.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Library/Indicator_Function.thy Sat Jun 28 09:16:42 2014 +0200 @@ -57,7 +57,7 @@ shows setsum_mult_indicator[simp]: "(\x \ A. f x * indicator B x) = (\x \ A \ B. f x)" and setsum_indicator_mult[simp]: "(\x \ A. indicator B x * f x) = (\x \ A \ B. f x)" unfolding indicator_def - using assms by (auto intro!: setsum_mono_zero_cong_right split: split_if_asm) + using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm) lemma setsum_indicator_eq_card: assumes "finite A" @@ -68,6 +68,6 @@ lemma setsum_indicator_scaleR[simp]: "finite A \ (\x \ A. indicator (B x) (g x) *\<^sub>R f x) = (\x \ {x\A. g x \ B x}. f x::'a::real_vector)" - using assms by (auto intro!: setsum_mono_zero_cong_right split: split_if_asm simp: indicator_def) + using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm simp: indicator_def) end \ No newline at end of file diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Library/Multiset.thy Sat Jun 28 09:16:42 2014 +0200 @@ -612,7 +612,7 @@ lemma size_multiset_union [simp]: "size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N" -apply (simp add: size_multiset_def setsum_Un_nat setsum_addf setsum_wcount_Int wcount_union) +apply (simp add: size_multiset_def setsum_Un_nat setsum.distrib setsum_wcount_Int wcount_union) apply (subst Int_commute) apply (simp add: setsum_wcount_Int) done @@ -2287,10 +2287,10 @@ hence "?B = {b. h2 b = c \ ?As b \ {}}" by (auto simp add: setsum_gt_0_iff) hence A: "?A = \ {?As b | b. b \ ?B}" by auto have "setsum (count f) ?A = setsum (setsum (count f)) {?As b | b. b \ ?B}" - unfolding A by transfer (intro setsum_Union_disjoint, auto simp: multiset_def) + unfolding A by transfer (intro setsum.Union_disjoint [simplified], auto simp: multiset_def setsum.Union_disjoint) also have "... = setsum (setsum (count f)) (?As ` ?B)" unfolding 0 .. also have "... = setsum (setsum (count f) o ?As) ?B" - by(intro setsum_reindex) (auto simp add: setsum_gt_0_iff inj_on_def) + by (intro setsum.reindex) (auto simp add: setsum_gt_0_iff inj_on_def) also have "... = setsum (\ b. setsum (count f) (?As b)) ?B" unfolding comp_def .. finally have "setsum (count f) ?A = setsum (\ b. setsum (count f) (?As b)) ?B" . thus "count (mmap (h2 \ h1) f) c = count ((mmap h2 \ mmap h1) f) c" @@ -2300,7 +2300,7 @@ lemma mmap_cong: assumes "\a. a \# M \ f a = g a" shows "mmap f M = mmap g M" -using assms by transfer (auto intro!: setsum_cong) +using assms by transfer (auto intro!: setsum.cong) context begin @@ -2458,7 +2458,7 @@ (* *) let ?ct1 = "N1 o e1" let ?ct2 = "N2 o e2" have ss: "setsum ?ct1 {.. i1. i1 \ n1 \ setsum (\ i2. ct i1 i2) {.. n1" using f1 unfolding bij_betw_def by (metis image_eqI lessThan_iff less_Suc_eq_le) have "(\b2\B2. M (u b1 b2)) = (\i2b2\B2. M (u b1 b2)) = N1 b1" . @@ -2500,8 +2500,8 @@ hence f2b2: "f2 b2 \ n2" using f2 unfolding bij_betw_def by (metis image_eqI lessThan_iff less_Suc_eq_le) have "(\b1\B1. M (u b1 b2)) = (\i1b1\B1. M (u b1 b2)) = N2 b2" . @@ -2610,7 +2610,7 @@ have set1_disj: "\ c c'. c \ c' \ set1 c \ set1 c' = {}" unfolding set1_def by auto have setsum_set1: "\ c. setsum (count N1) (set1 c) = count P c" - unfolding P1 set1_def by transfer (auto intro: setsum_cong) + unfolding P1 set1_def by transfer (auto intro: setsum.cong) def set2 \ "\ c. {b2 \ set_of N2. f2 b2 = c}" have set2[simp]: "\ c b2. b2 \ set2 c \ f2 b2 = c" unfolding set2_def by auto @@ -2625,7 +2625,7 @@ have set2_disj: "\ c c'. c \ c' \ set2 c \ set2 c' = {}" unfolding set2_def by auto have setsum_set2: "\ c. setsum (count N2) (set2 c) = count P c" - unfolding P2 set2_def by transfer (auto intro: setsum_cong) + unfolding P2 set2_def by transfer (auto intro: setsum.cong) have ss: "\ c. c \ set_of P \ setsum (count N1) (set1 c) = setsum (count N2) (set2 c)" unfolding setsum_set1 setsum_set2 .. @@ -2746,9 +2746,9 @@ have c: "c \ set_of P" and b1: "b1 \ set1 c" unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap]) with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \ a \ SET}" - by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm) + by transfer (force intro: setsum.mono_neutral_cong_left split: split_if_asm) also have "... = setsum (count M) ((\ b2. u c b1 b2) ` (set2 c))" - apply(rule setsum_cong) using c b1 proof safe + apply(rule setsum.cong) using c b1 proof safe fix a assume p1a: "p1 a \ set1 c" and "c \ set_of P" and "a \ SET" hence ac: "a \ sset c" using p1_rev by auto hence "a = u c (p1 a) (p2 a)" using c by auto @@ -2756,10 +2756,10 @@ ultimately show "a \ u c (p1 a) ` set2 c" by auto qed auto also have "... = setsum (\ b2. count M (u c b1 b2)) (set2 c)" - unfolding comp_def[symmetric] apply(rule setsum_reindex) + unfolding comp_def[symmetric] apply(rule setsum.reindex) using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast also have "... = count N1 b1" unfolding ss1[OF c b1, symmetric] - apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b1 set2) + apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b1 set2) using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce finally show ?thesis . qed @@ -2781,9 +2781,9 @@ have c: "c \ set_of P" and b2: "b2 \ set2 c" unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap]) with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \ a \ SET}" - by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm) + by transfer (force intro: setsum.mono_neutral_cong_left split: split_if_asm) also have "... = setsum (count M) ((\ b1. u c b1 b2) ` (set1 c))" - apply(rule setsum_cong) using c b2 proof safe + apply(rule setsum.cong) using c b2 proof safe fix a assume p2a: "p2 a \ set2 c" and "c \ set_of P" and "a \ SET" hence ac: "a \ sset c" using p2_rev by auto hence "a = u c (p1 a) (p2 a)" using c by auto @@ -2791,11 +2791,11 @@ ultimately show "a \ (\x. u c x (p2 a)) ` set1 c" by auto qed auto also have "... = setsum (count M o (\ b1. u c b1 b2)) (set1 c)" - apply(rule setsum_reindex) + apply(rule setsum.reindex) using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast also have "... = setsum (\ b1. count M (u c b1 b2)) (set1 c)" by simp also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def - apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1) + apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b2 set1) using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce finally show ?thesis . qed @@ -2855,7 +2855,7 @@ assume "M1 \ multiset" "M2 \ multiset" hence "setsum M1 {a. f a = x \ 0 < M1 a} = setsum M1 {a. f a = x \ 0 < M1 a + M2 a}" "setsum M2 {a. f a = x \ 0 < M2 a} = setsum M2 {a. f a = x \ 0 < M1 a + M2 a}" - by (auto simp: multiset_def intro!: setsum_mono_zero_cong_left) + by (auto simp: multiset_def intro!: setsum.mono_neutral_cong_left) then show "(\a | f a = x \ 0 < M1 a + M2 a. M1 a + M2 a) = setsum M1 {a. f a = x \ 0 < M1 a} + setsum M2 {a. f a = x \ 0 < M2 a}" @@ -2897,7 +2897,7 @@ by (metis (lifting, full_types) mem_Collect_eq neq0_conv setsum.neutral) have 0: "\ b. 0 < setsum (count M) (A b) \ (\ a \ A b. count M a > 0)" apply safe - apply (metis less_not_refl setsum_gt_0_iff setsum_infinite) + apply (metis less_not_refl setsum_gt_0_iff setsum.infinite) by (metis A_def finite_Collect_conjI finite_Collect_mem setsum_gt_0_iff) hence AB: "A ` ?B = {A b | b. \ a \ A b. count M a > 0}" by auto diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Library/Permutations.thy Sat Jun 28 09:16:42 2014 +0200 @@ -955,7 +955,7 @@ using image_inverse_permutations by blast have th2: "?rhs = setsum (f \ inv) ?S" by (simp add: o_def) - from setsum_reindex[OF th0, of f] show ?thesis unfolding th1 th2 . + from setsum.reindex[OF th0, of f] show ?thesis unfolding th1 th2 . qed lemma setum_permutations_compose_left: @@ -979,7 +979,7 @@ qed have th3: "(op \ q) ` ?S = ?S" using image_compose_permutations_left[OF q] by auto - from setsum_reindex[OF th1, of f] show ?thesis unfolding th0 th1 th3 . + from setsum.reindex[OF th1, of f] show ?thesis unfolding th0 th1 th3 . qed lemma sum_permutations_compose_right: @@ -1003,7 +1003,7 @@ qed have th3: "(\p. p \ q) ` ?S = ?S" using image_compose_permutations_right[OF q] by auto - from setsum_reindex[OF th1, of f] + from setsum.reindex[OF th1, of f] show ?thesis unfolding th0 th1 th3 . qed @@ -1024,10 +1024,10 @@ by blast show ?thesis unfolding permutes_insert - unfolding setsum_cartesian_product + unfolding setsum.cartesian_product unfolding th1[symmetric] unfolding th0 - proof (rule setsum_reindex) + proof (rule setsum.reindex) let ?f = "(\(b, y). Fun.swap a b id \ y)" let ?P = "{p. p permutes S}" { diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/List.thy --- a/src/HOL/List.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/List.thy Sat Jun 28 09:16:42 2014 +0200 @@ -4525,7 +4525,7 @@ moreover have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp then have "(card A - k) * \{Suc (card A - k)..card A} = \{Suc (card A - Suc k)..card A}" - by (subst setprod_insert[symmetric]) (simp add: atLeastAtMost_insertL)+ + by (subst setprod.insert[symmetric]) (simp add: atLeastAtMost_insertL)+ ultimately show ?case by (simp add: card_image inj_Cons card_UN_disjoint Suc.hyps algebra_simps) qed diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/MacLaurin.thy --- a/src/HOL/MacLaurin.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/MacLaurin.thy Sat Jun 28 09:16:42 2014 +0200 @@ -87,7 +87,7 @@ + (B * (t^n / real(fact n)))))" have g2: "g 0 = 0 & g h = 0" - by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum_reindex) + by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum.reindex) def difg \ "(%m t. diff m t - (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {..mm x. \m < n; 0 \ x; x \ h\ \ isCont (difg m) x" by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp @@ -225,7 +225,7 @@ by (auto simp add: power_mult_distrib[symmetric]) moreover have "(SUM m - t < 0 \ f h = @@ -419,13 +419,13 @@ apply (simp (no_asm)) apply (simp (no_asm) add: sin_expansion_lemma) apply (force intro!: derivative_eq_intros) -apply (subst (asm) setsum_0', clarify, case_tac "x", simp, simp) +apply (subst (asm) setsum.neutral, clarify, case_tac "x", simp, simp) apply (cases n, simp, simp) apply (rule ccontr, simp) apply (drule_tac x = x in spec, simp) apply (erule ssubst) apply (rule_tac x = t in exI, simp) -apply (rule setsum_cong[OF refl]) +apply (rule setsum.cong[OF refl]) apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex) done @@ -450,7 +450,7 @@ apply (force intro!: derivative_eq_intros) apply (erule ssubst) apply (rule_tac x = t in exI, simp) -apply (rule setsum_cong[OF refl]) +apply (rule setsum.cong[OF refl]) apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex) done @@ -467,7 +467,7 @@ apply (force intro!: derivative_eq_intros) apply (erule ssubst) apply (rule_tac x = t in exI, simp) -apply (rule setsum_cong[OF refl]) +apply (rule setsum.cong[OF refl]) apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex) done @@ -497,7 +497,7 @@ apply (drule_tac x = x in spec, simp) apply (erule ssubst) apply (rule_tac x = t in exI, simp) -apply (rule setsum_cong[OF refl]) +apply (rule setsum.cong[OF refl]) apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex) done @@ -513,7 +513,7 @@ apply (simp (no_asm) add: cos_expansion_lemma) apply (erule ssubst) apply (rule_tac x = t in exI, simp) -apply (rule setsum_cong[OF refl]) +apply (rule setsum.cong[OF refl]) apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex) done @@ -529,7 +529,7 @@ apply (simp (no_asm) add: cos_expansion_lemma) apply (erule ssubst) apply (rule_tac x = t in exI, simp) -apply (rule setsum_cong[OF refl]) +apply (rule setsum.cong[OF refl]) apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex) done @@ -572,7 +572,7 @@ unfolding sin_coeff_def apply (subst t2) apply (rule sin_bound_lemma) - apply (rule setsum_cong[OF refl]) + apply (rule setsum.cong[OF refl]) apply (subst diff_m_0, simp) apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono simp add: est mult_ac divide_inverse power_abs [symmetric] abs_mult) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Metis_Examples/Big_O.thy --- a/src/HOL/Metis_Examples/Big_O.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Metis_Examples/Big_O.thy Sat Jun 28 09:16:42 2014 +0200 @@ -552,7 +552,8 @@ apply (erule ssubst) apply (erule bigo_setsum3) apply (rule ext) -apply (rule setsum_cong2) +apply (rule setsum.cong) +apply (rule refl) by (metis abs_of_nonneg zero_le_mult_iff) lemma bigo_setsum6: "f =o g +o O(h) \ \x y. 0 <= l x y \ diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sat Jun 28 09:16:42 2014 +0200 @@ -64,13 +64,13 @@ apply auto done -lemma setsum_Un_disjoint': +lemma setsum_union_disjoint': assumes "finite A" and "finite B" and "A \ B = {}" and "A \ B = C" shows "setsum g C = setsum g A + setsum g B" - using setsum_Un_disjoint[OF assms(1-3)] and assms(4) by auto + using setsum.union_disjoint[OF assms(1-3)] and assms(4) by auto lemma pointwise_minimal_pointwise_maximal: fixes s :: "(nat \ nat) set" @@ -151,19 +151,19 @@ shows "odd (card {s\S. compo s})" proof - have "(\s | s \ S \ \ compo s. nF s) + (\s | s \ S \ compo s. nF s) = (\s\S. nF s)" - by (subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong) + by (subst setsum.union_disjoint[symmetric]) (auto intro!: setsum.cong) also have "\ = (\s\S. card {f \ {f\F. compo' f \ bnd f}. face f s}) + (\s\S. card {f \ {f\F. compo' f \ \ bnd f}. face f s})" - unfolding setsum_addf[symmetric] + unfolding setsum.distrib[symmetric] by (subst card_Un_disjoint[symmetric]) - (auto simp: nF_def intro!: setsum_cong arg_cong[where f=card]) + (auto simp: nF_def intro!: setsum.cong arg_cong[where f=card]) also have "\ = 1 * card {f\F. compo' f \ bnd f} + 2 * card {f\F. compo' f \ \ bnd f}" using assms(4,5) by (fastforce intro!: arg_cong2[where f="op +"] setsum_multicount) finally have "odd ((\s | s \ S \ \ compo s. nF s) + card {s\S. compo s})" using assms(6,8) by simp moreover have "(\s | s \ S \ \ compo s. nF s) = (\s | s \ S \ \ compo s \ nF s = 0. nF s) + (\s | s \ S \ \ compo s \ nF s = 2. nF s)" - using assms(7) by (subst setsum_Un_disjoint[symmetric]) (fastforce intro!: setsum_cong)+ + using assms(7) by (subst setsum.union_disjoint[symmetric]) (fastforce intro!: setsum.cong)+ ultimately show ?thesis by auto qed diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sat Jun 28 09:16:42 2014 +0200 @@ -8,23 +8,18 @@ "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by (cases "k=a") auto -lemma setsum_Plus: - "\finite A; finite B\ \ - (\x\A <+> B. g x) = (\x\A. g (Inl x)) + (\x\B. g (Inr x))" - unfolding Plus_def - by (subst setsum_Un_disjoint, auto simp add: setsum_reindex) - lemma setsum_UNIV_sum: fixes g :: "'a::finite + 'b::finite \ _" shows "(\x\UNIV. g x) = (\x\UNIV. g (Inl x)) + (\x\UNIV. g (Inr x))" apply (subst UNIV_Plus_UNIV [symmetric]) - apply (rule setsum_Plus [OF finite finite]) + apply (subst setsum.Plus) + apply simp_all done lemma setsum_mult_product: "setsum h {..i\{..j\{..j. j + i * B) {..j. j + i * B) ` {..x. x \ A \ f x = g x) \ setsum f A = setsum g A" + by (auto intro: setsum.cong) + +hide_fact (open) setsum_cong_aux + method_setup vector = {* let val ss1 = simpset_of (put_simpset HOL_basic_ss @{context} - addsimps [@{thm setsum_addf} RS sym, + addsimps [@{thm setsum.distrib} RS sym, @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib}, @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym]) val ss2 = @@ -126,8 +127,8 @@ @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}]) fun vector_arith_tac ctxt ths = simp_tac (put_simpset ss1 ctxt) - THEN' (fn i => rtac @{thm setsum_cong2} i - ORELSE rtac @{thm setsum_0'} i + THEN' (fn i => rtac @{thm Cartesian_Euclidean_Space.setsum_cong_aux} i + ORELSE rtac @{thm setsum.neutral} i ORELSE simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm vec_eq_iff}]) i) (* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) THEN' asm_full_simp_tac (put_simpset ss2 ctxt addsimps ths) @@ -357,14 +358,14 @@ lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def) lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)" - by (vector matrix_matrix_mult_def setsum_addf[symmetric] field_simps) + by (vector matrix_matrix_mult_def setsum.distrib[symmetric] field_simps) lemma matrix_mul_lid: fixes A :: "'a::semiring_1 ^ 'm ^ 'n" shows "mat 1 ** A = A" apply (simp add: matrix_matrix_mult_def mat_def) apply vector - apply (auto simp only: if_distrib cond_application_beta setsum_delta'[OF finite] + apply (auto simp only: if_distrib cond_application_beta setsum.delta'[OF finite] mult_1_left mult_zero_left if_True UNIV_I) done @@ -374,26 +375,26 @@ shows "A ** mat 1 = A" apply (simp add: matrix_matrix_mult_def mat_def) apply vector - apply (auto simp only: if_distrib cond_application_beta setsum_delta[OF finite] + apply (auto simp only: if_distrib cond_application_beta setsum.delta[OF finite] mult_1_right mult_zero_right if_True UNIV_I cong: if_cong) done lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C" apply (vector matrix_matrix_mult_def setsum_right_distrib setsum_left_distrib mult_assoc) - apply (subst setsum_commute) + apply (subst setsum.commute) apply simp done lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x" apply (vector matrix_matrix_mult_def matrix_vector_mult_def setsum_right_distrib setsum_left_distrib mult_assoc) - apply (subst setsum_commute) + apply (subst setsum.commute) apply simp done lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)" apply (vector matrix_vector_mult_def mat_def) - apply (simp add: if_distrib cond_application_beta setsum_delta' cong del: if_weak_cong) + apply (simp add: if_distrib cond_application_beta setsum.delta' cong del: if_weak_cong) done lemma matrix_transpose_mul: @@ -410,7 +411,7 @@ apply (erule_tac x="axis ia 1" in allE) apply (erule_tac x="i" in allE) apply (auto simp add: if_distrib cond_application_beta axis_def - setsum_delta[OF finite] cong del: if_weak_cong) + setsum.delta[OF finite] cong del: if_weak_cong) done lemma matrix_vector_mul_component: "((A::real^_^_) *v x)$k = (A$k) \ x" @@ -418,7 +419,7 @@ lemma dot_lmul_matrix: "((x::real ^_) v* A) \ y = x \ (A *v y)" apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac) - apply (subst setsum_commute) + apply (subst setsum.commute) apply simp done @@ -455,10 +456,10 @@ lemma vector_componentwise: "(x::'a::ring_1^'n) = (\ j. \i\UNIV. (x$i) * (axis i 1 :: 'a^'n) $ j)" - by (simp add: axis_def if_distrib setsum_cases vec_eq_iff) + by (simp add: axis_def if_distrib setsum.If_cases vec_eq_iff) lemma basis_expansion: "setsum (\i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)" - by (auto simp add: axis_def vec_eq_iff if_distrib setsum_cases cong del: if_weak_cong) + by (auto simp add: axis_def vec_eq_iff if_distrib setsum.If_cases cong del: if_weak_cong) lemma linear_componentwise: fixes f:: "real ^'m \ real ^ _" @@ -492,7 +493,7 @@ lemma matrix_vector_mul_linear: "linear(\x. A *v (x::real ^ _))" by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff - field_simps setsum_right_distrib setsum_addf) + field_simps setsum_right_distrib setsum.distrib) lemma matrix_works: assumes lf: "linear f" @@ -523,7 +524,7 @@ apply (rule adjoint_unique) apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib) - apply (subst setsum_commute) + apply (subst setsum.commute) apply (auto simp add: mult_ac) done @@ -707,13 +708,13 @@ using i(1) by (simp add: field_simps) have "setsum (\xa. if xa = i then (c + (x$i)) * ((column xa A)$j) else (x$xa) * ((column xa A$j))) ?U = setsum (\xa. (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))) ?U" - apply (rule setsum_cong[OF refl]) + apply (rule setsum.cong[OF refl]) using th apply blast done also have "\ = setsum (\xa. if xa = i then c * ((column i A)$j) else 0) ?U + setsum (\xa. ((x$xa) * ((column xa A)$j))) ?U" - by (simp add: setsum_addf) + by (simp add: setsum.distrib) also have "\ = c * ((column i A)$j) + setsum (\xa. ((x$xa) * ((column xa A)$j))) ?U" - unfolding setsum_delta[OF fU] + unfolding setsum.delta[OF fU] using i(1) by simp finally show "setsum (\xa. if xa = i then (c + (x$i)) * ((column xa A)$j) else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + setsum (\xa. ((x$xa) * ((column xa A)$j))) ?U" . diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Jun 28 09:16:42 2014 +0200 @@ -121,9 +121,9 @@ by (auto intro: finite_subset[OF assms]) have ***: "\i. i \ Basis \ (\i\d. f i *\<^sub>R i) \ i = (\x\d. if x = i then f x else 0)" using d - by (auto intro!: setsum_cong simp: inner_Basis inner_setsum_left) + by (auto intro!: setsum.cong simp: inner_Basis inner_setsum_left) show ?thesis - unfolding euclidean_eq_iff[where 'a='a] by (auto simp: setsum_delta[OF **] ***) + unfolding euclidean_eq_iff[where 'a='a] by (auto simp: setsum.delta[OF **] ***) qed lemma independent_substdbasis: "d \ Basis \ independent d" @@ -324,7 +324,7 @@ and "setsum (\y. if (x = y) then P x else Q y) s = setsum Q s" and "setsum (\y. if (y = x) then P y else Q y) s = setsum Q s" and "setsum (\y. if (x = y) then P y else Q y) s = setsum Q s" - apply (rule_tac [!] setsum_cong2) + apply (rule_tac [!] setsum.cong) using assms apply auto done @@ -337,11 +337,11 @@ have *: "\x y. (if y = x then f x else (0::real)) *\<^sub>R x = (if x=y then (f x) *\<^sub>R x else 0)" by auto show ?thesis - unfolding * using setsum_delta[OF assms, of y "\x. f x *\<^sub>R x"] by auto + unfolding * using setsum.delta[OF assms, of y "\x. f x *\<^sub>R x"] by auto qed lemma if_smult: "(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)" - by auto + by (fact if_distrib) lemma dist_triangle_eq: fixes x y z :: "'a::real_inner" @@ -578,8 +578,8 @@ setsum ua s = 1 \ (\v\s. ua v *\<^sub>R v) = u *\<^sub>R x + v *\<^sub>R y" apply (rule_tac x="sx \ sy" in exI) apply (rule_tac x="\a. (if a\sx then u * ux a else 0) + (if a\sy then v * uy a else 0)" in exI) - unfolding scaleR_left_distrib setsum_addf if_smult scaleR_zero_left - ** setsum_restrict_set[OF xy, symmetric] + unfolding scaleR_left_distrib setsum.distrib if_smult scaleR_zero_left + ** setsum.inter_restrict[OF xy, symmetric] unfolding scaleR_scaleR[symmetric] Real_Vector_Spaces.scaleR_right.setsum [symmetric] and setsum_right_distrib[symmetric] unfolding x y @@ -616,7 +616,7 @@ assume "finite t" "\ (\x. (x \ t) = (x \ {}))" "setsum u t = 1" "(\v\t. u v *\<^sub>R v) = x" then show "\u. setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = x" apply (rule_tac x="\x. if x\t then u x else 0" in exI) - unfolding if_smult scaleR_zero_left and setsum_restrict_set[OF assms, symmetric] and * + unfolding if_smult scaleR_zero_left and setsum.inter_restrict[OF assms, symmetric] and * apply auto done qed @@ -673,9 +673,9 @@ apply (rule_tac x="\x. (if x=a then v else 0) + u x" in exI) unfolding setsum_clauses(2)[OF fin] apply simp - unfolding scaleR_left_distrib and setsum_addf + unfolding scaleR_left_distrib and setsum.distrib unfolding vu and * and scaleR_zero_left - apply (auto simp add: setsum_delta[OF fin]) + apply (auto simp add: setsum.delta[OF fin]) done next case False @@ -685,8 +685,8 @@ from False show ?thesis apply (rule_tac x="\x. if x=a then v else u x" in exI) unfolding setsum_clauses(2)[OF fin] and * using vu - using setsum_cong2[of s "\x. u x *\<^sub>R x" "\x. if x = a then v *\<^sub>R x else u x *\<^sub>R x", OF **(2)] - using setsum_cong2[of s u "\x. if x = a then v else u x", OF **(1)] + using setsum.cong [of s _ "\x. u x *\<^sub>R x" "\x. if x = a then v *\<^sub>R x else u x *\<^sub>R x", OF _ **(2)] + using setsum.cong [of s _ u "\x. if x = a then v else u x", OF _ **(1)] apply auto done qed @@ -777,7 +777,7 @@ apply (rule conjI) using as(1) apply simp apply (erule conjI) using as(1) - apply (simp add: setsum_reindex[unfolded inj_on_def] scaleR_right_diff_distrib + apply (simp add: setsum.reindex[unfolded inj_on_def] scaleR_right_diff_distrib setsum_subtractf scaleR_left.setsum[symmetric] setsum_diff1 scaleR_left_diff_distrib) unfolding as apply simp @@ -797,7 +797,7 @@ unfolding span_explicit by auto def f \ "(\x. x + a) ` t" have f: "finite f" "f \ s" "(\v\f. u (v - a) *\<^sub>R (v - a)) = y - a" - unfolding f_def using obt by (auto simp add: setsum_reindex[unfolded inj_on_def]) + unfolding f_def using obt by (auto simp add: setsum.reindex[unfolded inj_on_def]) have *: "f \ {a} = {}" "f \ - {a} = f" using f(2) assms by auto show "\sa u. finite sa \ sa \ {} \ sa \ insert a s \ setsum u sa = 1 \ (\v\sa. u v *\<^sub>R v) = y" @@ -805,7 +805,7 @@ apply (rule_tac x = "\x. if x=a then 1 - setsum (\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 "\x. x = a"] + unfolding setsum.If_cases[OF f(1), of "\x. x = a"] apply (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps *) done qed @@ -1284,7 +1284,7 @@ unfolding affine_dependent_explicit by auto then show ?rhs apply (rule_tac x="\x. if x\t then u x else 0" in exI) - apply auto unfolding * and setsum_restrict_set[OF assms, symmetric] + apply auto unfolding * and setsum.inter_restrict[OF assms, symmetric] unfolding Int_absorb1[OF `t\s`] apply auto done @@ -1708,8 +1708,8 @@ 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 Collect_mem_eq + unfolding * and setsum.If_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and + setsum.reindex[OF inj] and o_def Collect_mem_eq unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] setsum_right_distrib[symmetric] proof - fix i @@ -1744,7 +1744,7 @@ then show "\u. (\x\s. 0 \ u x) \ setsum u s = 1 \ (\x\s. u x *\<^sub>R x) = x" apply (rule_tac x="\y. if x=y then 1 else 0" in exI) apply auto - unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] + unfolding setsum.delta'[OF assms] and setsum_delta''[OF assms] apply auto done next @@ -1761,11 +1761,11 @@ } moreover have "(\x\s. u * ux x + v * uy x) = 1" - unfolding setsum_addf and setsum_right_distrib[symmetric] and ux(2) uy(2) + unfolding setsum.distrib and setsum_right_distrib[symmetric] and ux(2) uy(2) using uv(3) by auto moreover have "(\x\s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\x\s. ux x *\<^sub>R x) + v *\<^sub>R (\x\s. uy x *\<^sub>R x)" - unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[symmetric] + unfolding scaleR_left_distrib and setsum.distrib and scaleR_scaleR[symmetric] and scaleR_right.setsum [symmetric] by auto ultimately @@ -1877,8 +1877,8 @@ unfolding setsum_image_gen[OF *(1), of "\x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\x. u (f x)" f] unfolding f - using setsum_cong2[of s "\y. (\x\{x \ {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\v. u v *\<^sub>R v"] - using setsum_cong2 [of s "\y. (\x\{x \ {1..card s}. f x = y}. u (f x))" u] + using setsum.cong [of s s "\y. (\x\{x \ {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\v. u v *\<^sub>R v"] + using setsum.cong [of s s "\y. (\x\{x \ {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto ultimately @@ -1938,7 +1938,7 @@ by auto show ?lhs apply (rule_tac x = "\x. (if a = x then v else 0) + u x" in exI) - unfolding scaleR_left_distrib and setsum_addf and setsum_delta''[OF fin] and setsum_delta'[OF fin] + unfolding scaleR_left_distrib and setsum.distrib and setsum_delta''[OF fin] and setsum.delta'[OF fin] unfolding setsum_clauses(2)[OF assms] using uv and uv(2)[THEN bspec[where x=a]] and `a\s` apply auto @@ -1953,9 +1953,9 @@ moreover have "(\x\s. if a = x then v else u x) = setsum u s" and "(\x\s. (if a = x then v else u x) *\<^sub>R x) = (\x\s. u x *\<^sub>R x)" - apply (rule_tac setsum_cong2) + apply (rule_tac setsum.cong) apply rule defer - apply (rule_tac setsum_cong2) + apply (rule_tac setsum.cong) apply rule using `a \ s` apply auto done @@ -2088,7 +2088,7 @@ then have "finite (insert a t)" and "insert a t \ insert a s" by auto moreover have *: "\P Q. (\x\t. (if x = a then P x else Q x)) = (\x\t. Q x)" - apply (rule setsum_cong2) + apply (rule setsum.cong) using `a\s` `t\s` apply auto done @@ -2106,15 +2106,15 @@ apply auto done moreover have *: "\P Q. (\x\t. (if x = a then P x else Q x) *\<^sub>R x) = (\x\t. Q x *\<^sub>R x)" - apply (rule setsum_cong2) + apply (rule setsum.cong) using `a\s` `t\s` apply auto done have "(\x\t. u (x - a)) *\<^sub>R a = (\v\t. u (v - a) *\<^sub>R v)" unfolding scaleR_left.setsum - unfolding t_def and setsum_reindex[OF inj] and o_def + unfolding t_def and setsum.reindex[OF inj] and o_def using obt(5) - by (auto simp add: setsum_addf scaleR_right_distrib) + by (auto simp add: setsum.distrib scaleR_right_distrib) then have "(\v\insert a t. (if v = a then - (\x\t. u (x - a)) else u (v - a)) *\<^sub>R v) = 0" unfolding setsum_clauses(2)[OF fin] using `a\s` `t\s` @@ -2250,7 +2250,7 @@ apply auto done then have "setsum w s > 0" - unfolding setsum_diff1'[OF obt(1) `v\s`] + unfolding setsum.remove[OF obt(1) `v\s`] using as[THEN bspec[where x=v]] and `v\s` using `w v \ 0` by auto @@ -2293,11 +2293,11 @@ using Min_in[OF _ `i\{}`] and obt(1) unfolding i_def t_def by auto then have a: "a \ s" "u a + t * w a = 0" by auto have *: "\f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)" - unfolding setsum_diff1'[OF obt(1) `a\s`] by auto + unfolding setsum.remove[OF obt(1) `a\s`] by auto have "(\v\s. u v + t * w v) = 1" - unfolding setsum_addf wv(1) setsum_right_distrib[symmetric] obt(5) by auto + unfolding setsum.distrib wv(1) setsum_right_distrib[symmetric] obt(5) by auto moreover have "(\v\s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y" - unfolding setsum_addf obt(6) scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] wv(4) + unfolding setsum.distrib obt(6) scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] wv(4) using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp ultimately have "?P (n - 1)" apply (rule_tac x="(s - {a})" in exI) @@ -3762,10 +3762,10 @@ have *: "inj_on (\v. v + (y - a)) t" unfolding inj_on_def by auto have "(\v\(\v. v + (y - a)) ` t. u (v - (y - a))) = 1" - unfolding setsum_reindex[OF *] o_def using obt(4) by auto + unfolding setsum.reindex[OF *] o_def using obt(4) by auto moreover have "(\v\(\v. v + (y - a)) ` t. u (v - (y - a)) *\<^sub>R v) = y" - unfolding setsum_reindex[OF *] o_def using obt(4,5) - by (simp add: setsum_addf setsum_subtractf scaleR_left.setsum[symmetric] scaleR_right_distrib) + unfolding setsum.reindex[OF *] o_def using obt(4,5) + by (simp add: setsum.distrib setsum_subtractf scaleR_left.setsum[symmetric] scaleR_right_distrib) ultimately show "\sa u. finite sa \ (\x\sa. x \ s) \ (\x\sa. 0 \ u x) \ setsum u sa = 1 \ (\v\sa. u v *\<^sub>R v) = y" apply (rule_tac x="(\v. v + (y - a)) ` t" in exI) @@ -4776,7 +4776,7 @@ by blast then show ?thesis apply (rule_tac x="\v. if v\s then u v else 0" in exI) - unfolding if_smult scaleR_zero_left and setsum_restrict_set[OF assms(1), symmetric] + unfolding if_smult scaleR_zero_left and setsum.inter_restrict[OF assms(1), symmetric] apply (auto simp add: Int_absorb1) done qed @@ -4789,8 +4789,8 @@ have *: "\x. (if f x < 0 then f x else 0) + (if 0 < f x then f x else 0) = f x" by auto show ?thesis - unfolding real_add_eq_0_iff[symmetric] and setsum_restrict_set''[OF assms(1)] - and setsum_addf[symmetric] and * + unfolding real_add_eq_0_iff[symmetric] and setsum.inter_filter[OF assms(1)] + and setsum.distrib[symmetric] and * using assms(2) apply assumption done @@ -4805,8 +4805,8 @@ have *: "\x. (if 0 < g x then f x else 0) + (if g x < 0 then f x else 0) = f x" using assms(3) by auto show ?thesis - unfolding eq_neg_iff_add_eq_0 and setsum_restrict_set''[OF assms(1)] - and setsum_addf[symmetric] and * + unfolding eq_neg_iff_add_eq_0 and setsum.inter_filter[OF assms(1)] + and setsum.distrib[symmetric] and * using assms(2) apply assumption done @@ -4837,7 +4837,7 @@ apply auto done then show ?thesis - unfolding setsum_delta[OF assms(1)] using uv(2) and `u v < 0` and uv(1) by auto + unfolding setsum.delta[OF assms(1)] using uv(2) and `u v < 0` and uv(1) by auto qed qed (insert setsum_nonneg_eq_0_iff[of _ u, OF fin(1)] uv(2-3), auto) @@ -4850,14 +4850,14 @@ moreover have "setsum u ({x \ c. 0 < u x} \ {x \ c. u x < 0}) = setsum u c" "(\x\{x \ c. 0 < u x} \ {x \ c. u x < 0}. u x *\<^sub>R x) = (\x\c. u x *\<^sub>R x)" using assms(1) - apply (rule_tac[!] setsum_mono_zero_left) + apply (rule_tac[!] setsum.mono_neutral_left) apply auto done then have "setsum u {x \ c. 0 < u x} = - setsum u {x \ c. 0 > u x}" "(\x\{x \ c. 0 < u x}. u x *\<^sub>R x) = - (\x\{x \ c. 0 > u x}. u x *\<^sub>R x)" unfolding eq_neg_iff_add_eq_0 using uv(1,4) - by (auto simp add: setsum_Un_zero[OF fin, symmetric]) + by (auto simp add: setsum.union_inter_neutral[OF fin, symmetric]) moreover have "\x\{v \ c. u v < 0}. 0 \ inverse (setsum u {x \ c. 0 < u x}) * - u x" apply rule apply (rule mult_nonneg_nonneg) @@ -5773,7 +5773,7 @@ qed lemma inner_setsum_Basis[simp]: "i \ Basis \ (\Basis) \ i = 1" - by (simp add: inner_setsum_left setsum_cases inner_Basis) + by (simp add: inner_setsum_left setsum.If_cases inner_Basis) lemma convex_set_plus: assumes "convex s" and "convex t" shows "convex (s + t)" @@ -5806,7 +5806,7 @@ apply (rule_tac x="fun_upd f x a" in exI) apply simp apply (rule_tac f="\x. a + x" in arg_cong) - apply (rule setsum_cong [OF refl]) + apply (rule setsum.cong [OF refl]) apply clarsimp apply (fast intro: set_plus_intro) done @@ -5820,10 +5820,10 @@ apply (subgoal_tac "(\x\Basis. f x \ i) = f i \ i") apply (drule (1) bspec) apply clarsimp - apply (frule setsum_diff1' [OF finite_Basis]) + apply (frule setsum.remove [OF finite_Basis]) apply (erule trans) apply simp - apply (rule setsum_0') + apply (rule setsum.neutral) apply clarsimp apply (frule_tac x=i in bspec, assumption) apply (drule_tac x=x in bspec, assumption) @@ -5860,7 +5860,7 @@ (is "?int = convex hull ?points") proof - have One[simp]: "\i. i \ Basis \ One \ i = 1" - by (simp add: One_def inner_setsum_left setsum_cases inner_Basis) + by (simp add: One_def inner_setsum_left setsum.If_cases inner_Basis) have "?int = {x. \i\Basis. x \ i \ cbox 0 1}" by (auto simp: cbox_def) also have "\ = (\i\Basis. (\x. x *\<^sub>R i) ` cbox 0 1)" @@ -6154,7 +6154,7 @@ unfolding c_def convex_hull_set_setsum apply (subst convex_hull_linear_image [symmetric]) apply (simp add: linear_iff scaleR_add_left) - apply (rule setsum_cong [OF refl]) + apply (rule setsum.cong [OF refl]) apply (rule image_cong [OF _ refl]) apply (rule convex_hull_eq_real_cbox) apply (cut_tac `0 < d`, simp) @@ -6625,7 +6625,7 @@ by auto then have **: "setsum u ?D = setsum (op \ x) ?D" apply - - apply (rule setsum_cong2) + apply (rule setsum.cong) using assms apply auto done @@ -6694,13 +6694,13 @@ by (auto simp: SOME_Basis inner_Basis inner_simps) then have *: "setsum (op \ (x + (e / 2) *\<^sub>R (SOME i. i\Basis))) Basis = setsum (\i. x\i + (if (SOME i. i\Basis) = i then e/2 else 0)) Basis" - apply (rule_tac setsum_cong) + apply (rule_tac setsum.cong) apply auto done have "setsum (op \ x) Basis < setsum (op \ (x + (e / 2) *\<^sub>R (SOME i. i\Basis))) Basis" - unfolding * setsum_addf + unfolding * setsum.distrib using `e > 0` DIM_positive[where 'a='a] - apply (subst setsum_delta') + apply (subst setsum.delta') apply (auto simp: SOME_Basis) done also have "\ \ 1" @@ -6744,7 +6744,7 @@ then show "y \ i \ x \ i + ?d" by auto qed also have "\ \ 1" - unfolding setsum_addf setsum_constant real_eq_of_nat + unfolding setsum.distrib setsum_constant real_eq_of_nat by (auto simp add: Suc_le_eq) finally show "(\i\Basis. 0 \ y \ i) \ setsum (op \ y) Basis \ 1" proof safe @@ -6774,7 +6774,7 @@ assume i: "i \ Basis" have "?a \ i = inverse (2 * real DIM('a))" by (rule trans[of _ "setsum (\j. if i = j then inverse (2 * real DIM('a)) else 0) ?D"]) - (simp_all add: setsum_cases i) } + (simp_all add: setsum.If_cases i) } note ** = this show ?thesis apply (rule that[of ?a]) @@ -6786,7 +6786,8 @@ unfolding **[OF i] by (auto simp add: Suc_le_eq DIM_positive) next have "setsum (op \ ?a) ?D = setsum (\i. inverse (2 * real DIM('a))) ?D" - apply (rule setsum_cong2, rule **) + apply (rule setsum.cong) + apply rule apply auto done also have "\ < 1" @@ -6859,16 +6860,16 @@ using a d by (auto simp: inner_simps inner_Basis) then have *: "setsum (op \ (x + (e / 2) *\<^sub>R a)) d = setsum (\i. x\i + (if a = i then e/2 else 0)) d" - using d by (intro setsum_cong) auto + using d by (intro setsum.cong) auto have "a \ Basis" using `a \ d` d by auto then have h1: "(\i\Basis. i \ d \ (x + (e / 2) *\<^sub>R a) \ i = 0)" using x0 d `a\d` by (auto simp add: inner_add_left inner_Basis) have "setsum (op \ x) d < setsum (op \ (x + (e / 2) *\<^sub>R a)) d" - unfolding * setsum_addf + unfolding * setsum.distrib using `e > 0` `a \ d` using `finite d` - by (auto simp add: setsum_delta') + by (auto simp add: setsum.delta') also have "\ \ 1" using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R a"] by auto @@ -6927,7 +6928,7 @@ then show "y \ i \ x \ i + ?d" by auto qed also have "\ \ 1" - unfolding setsum_addf setsum_constant real_eq_of_nat + unfolding setsum.distrib setsum_constant real_eq_of_nat using `0 < card d` by auto finally show "setsum (op \ y) d \ 1" . @@ -6976,10 +6977,10 @@ have "?a \ i = inverse (2 * real (card d))" apply (rule trans[of _ "setsum (\j. if i = j then inverse (2 * real (card d)) else 0) ?D"]) unfolding inner_setsum_left - apply (rule setsum_cong2) - using `i \ d` `finite d` setsum_delta'[of d i "(\k. inverse (2 * real (card d)))"] + apply (rule setsum.cong) + using `i \ d` `finite d` setsum.delta'[of d i "(\k. inverse (2 * real (card d)))"] d1 assms(2) - by (auto simp: inner_simps inner_Basis set_rev_mp[OF _ assms(2)]) + by (auto simp: inner_Basis set_rev_mp[OF _ assms(2)]) } note ** = this show ?thesis @@ -6995,7 +6996,7 @@ finally show "0 < ?a \ i" by auto next have "setsum (op \ ?a) ?D = setsum (\i. inverse (2 * real (card d))) ?D" - by (rule setsum_cong2) (rule **) + by (rule setsum.cong) (rule refl, rule **) also have "\ < 1" unfolding setsum_constant real_eq_of_nat divide_real_def[symmetric] by (auto simp add: field_simps) @@ -8395,13 +8396,13 @@ assume "x \ S i" def c \ "\j. if j = i then 1::real else 0" then have *: "setsum c I = 1" - using `finite I` `i \ I` setsum_delta[of I i "\j::'a. 1::real"] + using `finite I` `i \ I` setsum.delta[of I i "\j::'a. 1::real"] by auto def s \ "\j. if j = i then x else p j" then have "\j. c j *\<^sub>R s j = (if j = i then x else 0)" using c_def by (auto simp add: algebra_simps) then have "x = setsum (\i. c i *\<^sub>R s i) I" - using s_def c_def `finite I` `i \ I` setsum_delta[of I i "\j::'a. x"] + using s_def c_def `finite I` `i \ I` setsum.delta[of I i "\j::'a. x"] by auto then have "x \ ?rhs" apply auto @@ -8434,7 +8435,7 @@ moreover have "setsum (\i. v * d i) I = v * setsum d I" by (simp add: setsum_right_distrib) ultimately have sum1: "setsum e I = 1" - using e_def xc yc uv by (simp add: setsum_addf) + using e_def xc yc uv by (simp add: setsum.distrib) def q \ "\i. if e i = 0 then p i else (u * c i / e i) *\<^sub>R s i + (v * d i / e i) *\<^sub>R t i" { fix i @@ -8477,7 +8478,7 @@ then have *: "\i\I. (u * c i) *\<^sub>R s i + (v * d i) *\<^sub>R t i = e i *\<^sub>R q i" by auto have "u *\<^sub>R x + v *\<^sub>R y = setsum (\i. (u * c i) *\<^sub>R s i + (v * d i) *\<^sub>R t i) I" - using xc yc by (simp add: algebra_simps scaleR_right.setsum setsum_addf) + using xc yc by (simp add: algebra_simps scaleR_right.setsum setsum.distrib) also have "\ = setsum (\i. e i *\<^sub>R q i) I" using * by auto finally have "u *\<^sub>R x + v *\<^sub>R y = setsum (\i. (e i) *\<^sub>R (q i)) I" diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Sat Jun 28 09:16:42 2014 +0200 @@ -12,13 +12,6 @@ subsection{* First some facts about products*} -lemma setprod_insert_eq: - "finite A \ setprod f (insert a A) = (if a \ A then setprod f A else f a * setprod f A)" - apply clarsimp - apply (subgoal_tac "insert a A = A") - apply auto - done - lemma setprod_add_split: fixes m n :: nat assumes mn: "m \ n + 1" @@ -33,7 +26,7 @@ by auto have f: "finite ?B" "finite ?C" by simp_all - from setprod_Un_disjoint[OF f dj, of f, unfolded un] show ?thesis . + from setprod.union_disjoint[OF f dj, of f, unfolded un] show ?thesis . qed @@ -82,7 +75,7 @@ assumes fS: "finite S" and f: "\x\S. f x \ 0 \ f x \ 1" shows "setprod f S \ 1" - using setprod_le[OF fS f] unfolding setprod_1 . + using setprod_le[OF fS f] unfolding setprod.neutral_const . subsection {* Trace *} @@ -97,14 +90,14 @@ by (simp add: trace_def mat_def) lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B" - by (simp add: trace_def setsum_addf) + by (simp add: trace_def setsum.distrib) lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B" by (simp add: trace_def setsum_subtractf) lemma trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)" apply (simp add: trace_def matrix_matrix_mult_def) - apply (subst setsum_commute) + apply (subst setsum.commute) apply (simp add: mult_commute) done @@ -149,7 +142,7 @@ setprod (\i. ?di (transpose A) i (inv p i)) (p ` ?U)" by simp also have "\ = setprod ((\i. ?di (transpose A) i (inv p i)) \ p) ?U" - unfolding setprod_reindex[OF pi] .. + unfolding setprod.reindex[OF pi] .. also have "\ = setprod (\i. ?di A i (p i)) ?U" proof - { @@ -161,7 +154,7 @@ } then show "setprod ((\i. ?di (transpose A) i (inv p i)) \ p) ?U = setprod (\i. ?di A i (p i)) ?U" - by (auto intro: setprod_cong) + by (auto intro: setprod.cong) qed finally have "of_int (sign (inv p)) * (setprod (\i. ?di (transpose A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\i. ?di A i (p i)) ?U)" @@ -170,7 +163,8 @@ then show ?thesis unfolding det_def apply (subst setsum_permutations_inverse) - apply (rule setsum_cong2) + apply (rule setsum.cong) + apply (rule refl) apply blast done qed @@ -202,7 +196,7 @@ } then have p0: "\p \ ?PU - {id}. ?pp p = 0" by blast - from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis + from setsum.mono_neutral_cong_left[OF fPU id0 p0] show ?thesis unfolding det_def by (simp add: sign_id) qed @@ -233,7 +227,7 @@ } then have p0: "\p \ ?PU -{id}. ?pp p = 0" by blast - from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis + from setsum.mono_neutral_cong_left[OF fPU id0 p0] show ?thesis unfolding det_def by (simp add: sign_id) qed @@ -263,7 +257,7 @@ } then have p0: "\p \ ?PU - {id}. ?pp p = 0" by blast - from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis + from setsum.mono_neutral_cong_left[OF fPU id0 p0] show ?thesis unfolding det_def by (simp add: sign_id) qed @@ -279,7 +273,7 @@ using i by (vector mat_def) } then have th: "setprod (\i. ?f i i) ?U = setprod (\x. 1) ?U" - by (auto intro: setprod_cong) + by (auto intro: setprod.cong) { fix i j assume i: "i \ ?U" and j: "j \ ?U" and ij: "i \ j" @@ -289,7 +283,7 @@ then have "det ?A = setprod (\i. ?f i i) ?U" using det_diagonal by blast also have "\ = 1" - unfolding th setprod_1 .. + unfolding th setprod.neutral_const .. finally show ?thesis . qed @@ -302,7 +296,7 @@ shows "det (\ i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric]) apply (subst sum_permutations_compose_right[OF p]) -proof (rule setsum_cong2) +proof (rule setsum.cong) let ?U = "UNIV :: 'n set" let ?PU = "{p. p permutes ?U}" fix q @@ -325,7 +319,7 @@ show "of_int (sign (q \ p)) * setprod (\i. A$ p i$ (q \ p) i) ?U = of_int (sign p) * of_int (sign q) * setprod (\i. A$i$q i) ?U" by (simp only: thp sign_compose[OF qp pp] mult_commute of_int_mult) -qed +qed rule lemma det_permute_columns: fixes A :: "'a::comm_ring_1^'n^'n" @@ -377,7 +371,7 @@ shows "det A = 0" using r apply (simp add: row_def det_def vec_eq_iff) - apply (rule setsum_0') + apply (rule setsum.neutral) apply (auto simp: sign_nz) done @@ -395,8 +389,8 @@ shows "det((\ i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) = det((\ i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) + det((\ i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)" - unfolding det_def vec_lambda_beta setsum_addf[symmetric] -proof (rule setsum_cong2) + unfolding det_def vec_lambda_beta setsum.distrib[symmetric] +proof (rule setsum.cong) let ?U = "UNIV :: 'n set" let ?pU = "{p. p permutes ?U}" let ?f = "(\i. if i = k then a i + b i else c i)::'n \ 'a::comm_ring_1^'n" @@ -418,14 +412,14 @@ then have th1: "setprod (\i. ?f i $ p i) ?Uk = setprod (\i. ?g i $ p i) ?Uk" and th2: "setprod (\i. ?f i $ p i) ?Uk = setprod (\i. ?h i $ p i) ?Uk" apply - - apply (rule setprod_cong, simp_all)+ + apply (rule setprod.cong, simp_all)+ done have th3: "finite ?Uk" "k \ ?Uk" by auto have "setprod (\i. ?f i $ p i) ?U = setprod (\i. ?f i $ p i) (insert k ?Uk)" unfolding kU[symmetric] .. also have "\ = ?f k $ p k * setprod (\i. ?f i $ p i) ?Uk" - apply (rule setprod_insert) + apply (rule setprod.insert) apply simp apply blast done @@ -434,20 +428,20 @@ also have "\ = (a k $ p k * setprod (\i. ?g i $ p i) ?Uk) + (b k$ p k * setprod (\i. ?h i $ p i) ?Uk)" by (metis th1 th2) also have "\ = setprod (\i. ?g i $ p i) (insert k ?Uk) + setprod (\i. ?h i $ p i) (insert k ?Uk)" - unfolding setprod_insert[OF th3] by simp + unfolding setprod.insert[OF th3] by simp finally have "setprod (\i. ?f i $ p i) ?U = setprod (\i. ?g i $ p i) ?U + setprod (\i. ?h i $ p i) ?U" unfolding kU[symmetric] . then show "of_int (sign p) * setprod (\i. ?f i $ p i) ?U = of_int (sign p) * setprod (\i. ?g i $ p i) ?U + of_int (sign p) * setprod (\i. ?h i $ p i) ?U" by (simp add: field_simps) -qed +qed rule lemma det_row_mul: fixes a b :: "'n::finite \ _ ^ 'n" shows "det((\ i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) = c * det((\ i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)" unfolding det_def vec_lambda_beta setsum_right_distrib -proof (rule setsum_cong2) +proof (rule setsum.cong) let ?U = "UNIV :: 'n set" let ?pU = "{p. p permutes ?U}" let ?f = "(\i. if i = k then c*s a i else b i)::'n \ 'a::comm_ring_1^'n" @@ -467,7 +461,7 @@ } then have th1: "setprod (\i. ?f i $ p i) ?Uk = setprod (\i. ?g i $ p i) ?Uk" apply - - apply (rule setprod_cong) + apply (rule setprod.cong) apply simp_all done have th3: "finite ?Uk" "k \ ?Uk" @@ -475,7 +469,7 @@ have "setprod (\i. ?f i $ p i) ?U = setprod (\i. ?f i $ p i) (insert k ?Uk)" unfolding kU[symmetric] .. also have "\ = ?f k $ p k * setprod (\i. ?f i $ p i) ?Uk" - apply (rule setprod_insert) + apply (rule setprod.insert) apply simp apply blast done @@ -484,13 +478,13 @@ also have "\ = c* (a k $ p k * setprod (\i. ?g i $ p i) ?Uk)" unfolding th1 by (simp add: mult_ac) also have "\ = c* (setprod (\i. ?g i $ p i) (insert k ?Uk))" - unfolding setprod_insert[OF th3] by simp + unfolding setprod.insert[OF th3] by simp finally have "setprod (\i. ?f i $ p i) ?U = c* (setprod (\i. ?g i $ p i) ?U)" unfolding kU[symmetric] . then show "of_int (sign p) * setprod (\i. ?f i $ p i) ?U = c * (of_int (sign p) * setprod (\i. ?g i $ p i) ?U)" by (simp add: field_simps) -qed +qed rule lemma det_row_0: fixes b :: "'n::finite \ _ ^ 'n" @@ -617,7 +611,7 @@ case 1 then show ?case apply simp - unfolding setsum_empty det_row_0[of k] + unfolding setsum.empty det_row_0[of k] apply rule done next @@ -695,7 +689,7 @@ (\(j, f)\S \ ?F T. det (\ i. if i \ T then a i (f i) else if i = z then a i j else c i))" - unfolding insert.hyps unfolding setsum_cartesian_product by blast + unfolding insert.hyps unfolding setsum.cartesian_product by blast show ?case unfolding tha using `z \ T` by (intro setsum.reindex_bij_witness[where i="?k" and j="?h"]) @@ -722,7 +716,7 @@ lemma det_rows_mul: "det((\ i. c i *s a i)::'a::comm_ring_1^'n^'n) = setprod (\i. c i) (UNIV:: 'n set) * det((\ i. a i)::'a^'n^'n)" -proof (simp add: det_def setsum_right_distrib cong add: setprod_cong, rule setsum_cong2) +proof (simp add: det_def setsum_right_distrib cong add: setprod.cong, rule setsum.cong) let ?U = "UNIV :: 'n set" let ?PU = "{p. p permutes ?U}" fix p @@ -731,11 +725,11 @@ from pU have p: "p permutes ?U" by blast have "setprod (\i. c i * a i $ p i) ?U = setprod c ?U * setprod (\i. a i $ p i) ?U" - unfolding setprod_timesf .. + unfolding setprod.distrib .. then show "?s * (\xa\?U. c xa * a xa $ p xa) = setprod c ?U * (?s* (\xa\?U. a xa $ p xa))" by (simp add: field_simps) -qed +qed rule lemma det_mul: fixes A B :: "'a::linordered_idom^'n^'n" @@ -816,7 +810,7 @@ (\i\ ?U. (\ i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) = (setsum (\q. ?s p * (\i\ ?U. A $ i $ p i) * (?s q * (\i\ ?U. B $ i $ q i))) ?PU)" unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f] - proof (rule setsum_cong2) + proof (rule setsum.cong) fix q assume qU: "q \ ?PU" then have q: "q permutes ?U" @@ -835,8 +829,8 @@ by (rule setprod_permute[OF p]) have thp: "setprod (\i. (\ i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U = setprod (\i. A$i$p i) ?U * setprod (\i. B$i$ q (inv p i)) ?U" - unfolding th001 setprod_timesf[symmetric] o_def permutes_inverses[OF p] - apply (rule setprod_cong[OF refl]) + unfolding th001 setprod.distrib[symmetric] o_def permutes_inverses[OF p] + apply (rule setprod.cong[OF refl]) using permutes_in_image[OF q] apply vector done @@ -844,16 +838,16 @@ ?s p * (setprod (\i. A$i$p i) ?U) * (?s (q \ inv p) * setprod (\i. B$i$(q \ inv p) i) ?U)" using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp] by (simp add: sign_nz th00 field_simps sign_idempotent sign_compose) - qed + qed rule } then have th2: "setsum (\f. det (\ i. A$i$f i *s B$f i)) ?PU = det A * det B" unfolding det_def setsum_product - by (rule setsum_cong2) + by (rule setsum.cong [OF refl]) have "det (A**B) = setsum (\f. det (\ i. A $ i $ f i *s B $ f i)) ?F" unfolding matrix_mul_setsum_alt det_linear_rows_setsum[OF fU] by simp also have "\ = setsum (\f. det (\ i. A$i$f i *s B$f i)) ?PU" - using setsum_mono_zero_cong_left[OF fF PUF zth, symmetric] + using setsum.mono_neutral_cong_left[OF fF PUF zth, symmetric] unfolding det_rows_mul by auto finally show ?thesis unfolding th2 . qed @@ -902,7 +896,7 @@ done from c ci have thr0: "- row i A = setsum (\j. (1/ c i) *s (c j *s row j A)) (?U - {i})" - unfolding setsum_diff1'[OF fU iU] setsum_cmul + unfolding setsum.remove[OF fU iU] setsum_cmul apply - apply (rule vector_mul_lcancel_imp[OF ci]) apply (auto simp add: field_simps) @@ -962,7 +956,7 @@ done show "?lhs = x$k * det A" apply (subst U) - unfolding setsum_insert[OF fUk kUk] + unfolding setsum.insert[OF fUk kUk] apply (subst th00) unfolding add_assoc apply (subst det_row_add) @@ -980,7 +974,7 @@ proof - let ?U = "UNIV :: 'n set" have *: "\c. setsum (\i. c i *s row i (transpose A)) ?U = setsum (\i. c i *s column i A) ?U" - by (auto simp add: row_transpose intro: setsum_cong2) + by (auto simp add: row_transpose intro: setsum.cong) show ?thesis unfolding matrix_mult_vsum unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric] @@ -1073,7 +1067,7 @@ from fd[rule_format, of "axis i 1" "axis j 1", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul] have "?A$i$j = ?m1 $ i $ j" by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def - th0 setsum_delta[OF fU] mat_def axis_def) + th0 setsum.delta[OF fU] mat_def axis_def) } then have "orthogonal_matrix ?mf" unfolding orthogonal_matrix @@ -1280,8 +1274,8 @@ text {* Explicit formulas for low dimensions. *} -lemma setprod_1: "setprod f {(1::nat)..1} = f 1" - by simp +lemma setprod_neutral_const: "setprod f {(1::nat)..1} = f 1" + by (fact setprod_singleton_nat_seg) lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2" by (simp add: eval_nat_numeral setprod_numseg mult_commute) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sat Jun 28 09:16:42 2014 +0200 @@ -56,7 +56,7 @@ lemma (in euclidean_space) inner_setsum_left_Basis[simp]: "b \ Basis \ inner (\i\Basis. f i *\<^sub>R i) b = f b" - by (simp add: inner_setsum_left inner_Basis if_distrib setsum_cases) + by (simp add: inner_setsum_left inner_Basis if_distrib comm_monoid_add_class.setsum.If_cases) lemma (in euclidean_space) euclidean_eqI: assumes b: "\b. b \ Basis \ inner x b = inner y b" shows "x = y" @@ -166,7 +166,7 @@ by (auto intro!: inj_onI Pair_inject) thus ?thesis unfolding Basis_prod_def - by (subst setsum_Un_disjoint) (auto simp: Basis_prod_def setsum_reindex) + by (subst setsum.union_disjoint) (auto simp: Basis_prod_def setsum.reindex) qed instance proof diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Sat Jun 28 09:16:42 2014 +0200 @@ -841,7 +841,7 @@ by auto from bchoice[OF this] * assms show "\i\A. f i = 0" using setsum_nonneg_eq_0_iff[of A "\i. real (f i)"] by auto -qed (rule setsum_0') +qed (rule setsum.neutral) lemma setsum_ereal_right_distrib: fixes f :: "'a \ ereal" @@ -957,7 +957,7 @@ and "\i. 0 \ g i" shows "(\i. f i + g i) = suminf f + suminf g" apply (subst (1 2 3) suminf_ereal_eq_SUP) - unfolding setsum_addf + unfolding setsum.distrib apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+ done @@ -1237,7 +1237,7 @@ have "(\ii (\i. i + k)) i)" by simp also have "\ = (\i\(\i. i + k) ` {.. \ setsum f {..i setsum f {..x. (\i\Basis. ((v\i - u\i) / (b\i - a\i) * (x\i)) *\<^sub>R i) + (\i\Basis. (u\i - (v\i - u\i) / (b\i - a\i) * (a\i)) *\<^sub>R i))" - by (auto simp: setsum_addf[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff - field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum_cong) + by (auto simp: setsum.distrib[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff + field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum.cong) lemma continuous_interval_bij: fixes a b :: "'a::euclidean_space" diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sat Jun 28 09:16:42 2014 +0200 @@ -435,7 +435,7 @@ by (simp add: inner_commute) show "inner (x + y) z = inner x z + inner y z" unfolding inner_vec_def - by (simp add: inner_add_left setsum_addf) + by (simp add: inner_add_left setsum.distrib) show "inner (scaleR r x) y = r * inner x y" unfolding inner_vec_def by (simp add: setsum_right_distrib) @@ -470,17 +470,17 @@ unfolding inner_vec_def apply (cases "i = j") apply clarsimp - apply (subst setsum_diff1' [where a=j], simp_all) - apply (rule setsum_0', simp add: axis_def) - apply (rule setsum_0', simp add: axis_def) + apply (subst setsum.remove [of _ j], simp_all) + apply (rule setsum.neutral, simp add: axis_def) + apply (rule setsum.neutral, simp add: axis_def) done lemma setsum_single: assumes "finite A" and "k \ A" and "f k = y" assumes "\i. i \ A \ i \ k \ f i = 0" shows "(\i\A. f i) = y" - apply (subst setsum_diff1' [OF assms(1,2)]) - apply (simp add: setsum_0' assms(3,4)) + apply (subst setsum.remove [OF assms(1,2)]) + apply (simp add: setsum.neutral assms(3,4)) done lemma inner_axis: "inner x (axis i y) = inner (x $ i) y" diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Sat Jun 28 09:16:42 2014 +0200 @@ -527,7 +527,7 @@ have "0 \ cbox 0 (One::'a)" unfolding mem_box by auto then show ?thesis - unfolding content_def interval_bounds[OF *] using setprod_1 by auto + unfolding content_def interval_bounds[OF *] using setprod.neutral_const by auto qed lemma content_pos_le[intro]: @@ -1681,7 +1681,7 @@ note assm = tagged_division_ofD[OF assms(1)] show ?thesis unfolding * - proof (rule setsum_reindex_nonzero[symmetric]) + proof (rule setsum.reindex_nontrivial[symmetric]) show "finite p" using assm by auto fix x y @@ -1932,7 +1932,7 @@ assumes "content (cbox a b) = 0" and "p tagged_division_of (cbox a b)" shows "setsum (\(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)" -proof (rule setsum_0', rule) +proof (rule setsum.neutral, rule) fix y assume y: "y \ p" obtain x k where xk: "y = (x, k)" @@ -2541,7 +2541,7 @@ proof - case goal1 have "(\(x, k)\p. content k *\<^sub>R f x) = 0" - proof (rule setsum_0', rule) + proof (rule setsum.neutral, rule) fix x assume x: "x \ p" have "f (fst x) = 0" @@ -2775,8 +2775,8 @@ assume as: "p tagged_division_of (cbox a b)" "(\x. d1 x \ d2 x) fine p" have *: "(\(x, k)\p. content k *\<^sub>R (f x + g x)) = (\(x, k)\p. content k *\<^sub>R f x) + (\(x, k)\p. content k *\<^sub>R g x)" - unfolding scaleR_right_distrib setsum_addf[of "\(x,k). content k *\<^sub>R f x" "\(x,k). content k *\<^sub>R g x" p,symmetric] - by (rule setsum_cong2) auto + unfolding scaleR_right_distrib setsum.distrib[of "\(x,k). content k *\<^sub>R f x" "\(x,k). content k *\<^sub>R g x" p,symmetric] + by (rule setsum.cong) auto have "norm ((\(x, k)\p. content k *\<^sub>R (f x + g x)) - (k + l)) = norm (((\(x, k)\p. content k *\<^sub>R f x) - k) + ((\(x, k)\p. content k *\<^sub>R g x) - l))" unfolding * by (auto simp add: algebra_simps) @@ -2957,7 +2957,7 @@ next case (insert x F) show ?case - unfolding setsum_insert[OF insert(1,3)] + unfolding setsum.insert[OF insert(1,3)] apply (rule has_integral_add) using insert assms apply auto @@ -3257,7 +3257,7 @@ apply (subst *(1)) defer apply (subst *(1)) - unfolding setprod_insert[OF *(2-)] + unfolding setprod.insert[OF *(2-)] apply auto done assume as: "\i\Basis. a \ i \ b \ i" @@ -3270,7 +3270,7 @@ (\i\Basis. (if i = k then min (b \ k) c else b \ i) - a \ i)" "(\i\Basis. b \ i - ((\i\Basis. (if i = k then max (a \ k) c else a \ i) *\<^sub>R i) \ i)) = (\i\Basis. b \ i - (if i = k then max (a \ k) c else a \ i))" - by (auto intro!: setprod_cong) + by (auto intro!: setprod.cong) have "\ a \ k \ c \ \ c \ b \ k \ False" unfolding not_le using as[unfolded ,rule_format,of k] assms @@ -3539,7 +3539,7 @@ have lem3: "\g :: 'a set \ 'a set. finite p \ setsum (\(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \ p \ g k \ {}} = setsum (\(x, k). content k *\<^sub>R f x) ((\(x, k). (x, g k)) ` p)" - apply (rule setsum_mono_zero_left) + apply (rule setsum.mono_neutral_left) prefer 3 proof fix g :: "'a set \ 'a set" @@ -3664,9 +3664,9 @@ also have "\ = (\(x, ka)\p. content (ka \ {x. x \ k \ c}) *\<^sub>R f x) + (\(x, ka)\p. content (ka \ {x. c \ x \ k}) *\<^sub>R f x) - (i + j)" unfolding lem3[OF p(3)] - apply (subst setsum_reindex_nonzero[OF p(3)]) + apply (subst setsum.reindex_nontrivial[OF p(3)]) defer - apply (subst setsum_reindex_nonzero[OF p(3)]) + apply (subst setsum.reindex_nontrivial[OF p(3)]) defer unfolding lem4[symmetric] apply (rule refl) @@ -3689,7 +3689,7 @@ apply auto done qed - also note setsum_addf[symmetric] + also note setsum.distrib[symmetric] also have *: "\x. x \ p \ (\(x,ka). content (ka \ {x. x \ k \ c}) *\<^sub>R f x) x + (\(x,ka). content (ka \ {x. c \ x \ k}) *\<^sub>R f x) x = @@ -3705,7 +3705,7 @@ unfolding uv content_split[OF k,of u v c] by auto qed - note setsum_cong2[OF this] + note setsum.cong [OF _ this] finally have "(\(x, k)\{(x, kk \ {x. x \ k \ c}) |x kk. (x, kk) \ p \ kk \ {x. x \ k \ c} \ {}}. content k *\<^sub>R f x) - i + ((\(x, k)\{(x, kk \ {x. c \ x \ k}) |x kk. (x, kk) \ p \ kk \ {x. c \ x \ k} \ {}}. content k *\<^sub>R f x) - j) = (\(x, ka)\p. content ka *\<^sub>R f x) - (i + j)" @@ -3774,7 +3774,7 @@ note tagged_division_union_interval[OF p1(7) p2(7)] note p12 = tagged_division_ofD[OF this] this have "norm ((\(x, k)\p1. content k *\<^sub>R f x) + (\(x, k)\p2. content k *\<^sub>R f x) - i) = norm ((\(x, k)\p1 \ p2. content k *\<^sub>R f x) - i)" - apply (subst setsum_Un_zero) + apply (subst setsum.union_inter_neutral) apply (rule p1 p2)+ apply rule unfolding split_paired_all split_conv @@ -3799,12 +3799,13 @@ using e k by (auto simp: inner_simps inner_not_same_Basis) have "(\i\Basis. \(x - (x + (e / 2 ) *\<^sub>R k)) \ i\) = (\i\Basis. (if i = k then e / 2 else 0))" - apply (rule setsum_cong2) + apply (rule setsum.cong) + apply (rule refl) apply (subst *) apply auto done also have "\ < e" - apply (subst setsum_delta) + apply (subst setsum.delta) using e apply auto done @@ -4841,7 +4842,7 @@ shows "setsum f s = iterate op + s f" proof - have *: "setsum f s = setsum f (support op + f s)" - apply (rule setsum_mono_zero_right) + apply (rule setsum.mono_neutral_right) unfolding support_def neutral_add using assms apply auto @@ -4923,7 +4924,8 @@ apply (rule mult_left_mono) apply (rule order_trans[of _ "setsum content p"]) apply (rule eq_refl) - apply (rule setsum_cong2) + apply (rule setsum.cong) + apply (rule refl) apply (subst abs_of_nonneg) unfolding additive_content_division[OF assms(1)] proof - @@ -4957,7 +4959,8 @@ apply (rule mult_left_mono) apply (rule order_trans[of _ "setsum (content \ snd) p"]) apply (rule eq_refl) - apply (rule setsum_cong2) + apply (rule setsum.cong) + apply (rule refl) apply (subst o_def) apply (rule abs_of_nonneg) proof - @@ -4995,7 +4998,7 @@ apply (rule eq_refl) apply (rule arg_cong[where f=norm]) unfolding setsum_subtractf[symmetric] - apply (rule setsum_cong2) + apply (rule setsum.cong) unfolding scaleR_diff_right apply auto done @@ -5516,7 +5519,7 @@ (\i\Basis - {k}. interval_upperbound (cbox a b \ {x. \x \ k - c\ \ d}) \ i - interval_lowerbound (cbox a b \ {x. \x \ k - c\ \ d}) \ i) = (\i\Basis - {k}. b\i - a\i)" - apply (rule setprod_cong) + apply (rule setprod.cong) apply (rule refl) unfolding interval_doublesplit[OF k] apply (subst interval_bounds) @@ -5533,7 +5536,7 @@ apply (rule assms) unfolding if_not_P apply (subst *) - apply (subst setprod_insert) + apply (subst setprod.insert) unfolding ** unfolding interval_doublesplit[OF k] box_eq_empty not_ex not_less prefer 3 @@ -5574,7 +5577,8 @@ assume p: "p tagged_division_of (cbox a b) \ (\x. ball x d) fine p" have *: "(\(x, ka)\p. content ka *\<^sub>R ?i x) = (\(x, ka)\p. content (ka \ {x. abs(x\k - c) \ d}) *\<^sub>R ?i x)" - apply (rule setsum_cong2) + apply (rule setsum.cong) + apply (rule refl) unfolding split_paired_all real_scaleR_def mult_cancel_right split_conv apply cases apply (rule disjI1) @@ -5857,14 +5861,14 @@ (\y. (a,y)) ` (t a) \ {(i, j) |i j. i \ s \ j \ t i}" by auto show ?case unfolding * - apply (subst setsum_Un_disjoint) - unfolding setsum_insert[OF insert(1-2)] + apply (subst setsum.union_disjoint) + unfolding setsum.insert[OF insert(1-2)] prefer 4 apply (subst insert(3)) unfolding add_right_cancel proof - show "setsum (x a) (t a) = (\(xa, y)\ Pair a ` t a. x xa y)" - apply (subst setsum_reindex) + apply (subst setsum.reindex) unfolding inj_on_def apply auto done @@ -6678,7 +6682,7 @@ unfolding * apply (subst setsum_iterate[symmetric]) defer - apply (rule setsum_cong2) + apply (rule setsum.cong) unfolding split_paired_all split_conv using assms(2) apply auto @@ -6933,7 +6937,7 @@ have "norm (y - x) < e + setsum (\i. 0) Basis" apply (rule le_less_trans[OF norm_le_l1]) apply (subst *) - apply (subst setsum_insert) + apply (subst setsum.insert) prefer 3 apply (rule add_less_le_mono) proof - @@ -7425,7 +7429,7 @@ using assms(7) unfolding algebra_simps add_left_cancel scaleR_right.setsum by (subst setsum.reindex_bij_betw[symmetric, where h="\(x, k). (g x, g ` k)" and S=p]) - (auto intro!: * setsum_cong simp: bij_betw_def dest!: p(4)) + (auto intro!: * setsum.cong simp: bij_betw_def dest!: p(4)) also have "\ = r *\<^sub>R ((\(x, k)\p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR_diff_right scaleR_scaleR using assms(1) @@ -7449,14 +7453,6 @@ unfolding image_affinity_cbox by auto -lemma setprod_cong2: - assumes "\x. x \ A \ f x = g x" - shows "setprod f A = setprod g A" - apply (rule setprod_cong) - using assms - apply auto - done - lemma content_image_affinity_cbox: "content((\x::'a::euclidean_space. m *\<^sub>R x + c) ` cbox a b) = abs m ^ DIM('a) * content (cbox a b)" (is "?l = ?r") @@ -7486,7 +7482,7 @@ by (simp add: inner_simps field_simps) ultimately show ?thesis by (simp add: image_affinity_cbox True content_cbox' - setprod_timesf setprod_constant inner_diff_left) + setprod.distrib setprod_constant inner_diff_left) next case False with as have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \ {}" @@ -7499,7 +7495,7 @@ by (simp add: inner_simps field_simps) ultimately show ?thesis using False by (simp add: image_affinity_cbox content_cbox' - setprod_timesf[symmetric] setprod_constant[symmetric] inner_diff_left) + setprod.distrib[symmetric] setprod_constant[symmetric] inner_diff_left) qed qed @@ -7593,8 +7589,9 @@ unfolding content_def image_stretch_interval apply - unfolding interval_bounds' if_not_P - unfolding abs_setprod setprod_timesf[symmetric] - apply (rule setprod_cong2) + unfolding abs_setprod setprod.distrib[symmetric] + apply (rule setprod.cong) + apply (rule refl) unfolding lessThan_iff apply (simp only: inner_setsum_left_Basis) proof - @@ -7928,7 +7925,7 @@ unfolding setsum_right_distrib apply (subst(2) pA) apply (subst pA) - unfolding setsum_Un_disjoint[OF pA(2-)] + unfolding setsum.union_disjoint[OF pA(2-)] proof (rule norm_triangle_le, rule **) case goal1 show ?case @@ -7993,7 +7990,7 @@ apply rule apply (unfold split_paired_all split_conv) defer - unfolding setsum_Un_disjoint[OF pA(2-),symmetric] pA(1)[symmetric] + unfolding setsum.union_disjoint[OF pA(2-),symmetric] pA(1)[symmetric] unfolding setsum_right_distrib[symmetric] thm additive_tagged_division_1 apply (subst additive_tagged_division_1[OF _ as(1)]) @@ -8013,7 +8010,7 @@ show "norm (\(x, k)\p \ ?A. content k *\<^sub>R f' x - (f ((Sup k)) - f ((Inf k)))) \ e * (b - a) / 2" apply (rule *[where t="p \ {t. fst t \ {a, b} \ content(snd t) \ 0}"]) - apply (rule setsum_mono_zero_right[OF pA(2)]) + apply (rule setsum.mono_neutral_right[OF pA(2)]) defer apply rule unfolding split_paired_all split_conv o_def @@ -8049,7 +8046,7 @@ case goal2 show ?case apply (subst *) - apply (subst setsum_Un_disjoint) + apply (subst setsum.union_disjoint) prefer 4 apply (rule order_trans[of _ "e * (b - a)/4 + e * (b - a)/4"]) apply (rule norm_triangle_le,rule add_mono) @@ -8480,7 +8477,7 @@ then show ?thesis unfolding ** box_real apply - - apply (subst setsum_insert) + apply (subst setsum.insert) apply (rule p') unfolding split_conv defer @@ -9855,11 +9852,12 @@ unfolding if_P[OF True] apply (rule trans) defer - apply (rule setsum_cong2) + apply (rule setsum.cong) + apply (rule refl) apply (subst *) apply assumption apply (rule refl) - unfolding setsum_delta[OF assms(1)] + unfolding setsum.delta[OF assms(1)] using s apply auto done @@ -9995,7 +9993,7 @@ apply (rule setsum_over_tagged_division_lemma[OF assms(1)]) apply (rule integral_null) apply assumption - apply (rule setsum_cong2) + apply (rule setsum.cong) using assms(2) apply auto done @@ -10153,7 +10151,7 @@ then have "norm ((\(x, k)\p. content k *\<^sub>R f x) + (\(x, k)\\(qq ` r). content k *\<^sub>R f x) - integral (cbox a b) f) < e" - apply (subst setsum_Un_zero[symmetric]) + apply (subst setsum.union_inter_neutral[symmetric]) apply (rule p') prefer 3 apply assumption @@ -10180,13 +10178,9 @@ then have "norm ((\(x, k)\p. content k *\<^sub>R f x) + setsum (setsum (\(x, k). content k *\<^sub>R f x)) (qq ` r) - integral (cbox a b) f) < e" - apply (subst (asm) setsum_UNION_zero) - prefer 4 - apply assumption - apply (rule finite_imageI) - apply fact + apply (subst (asm) setsum.Union_comp) + prefer 2 unfolding split_paired_all split_conv image_iff - defer apply (erule bexE)+ proof - fix x m k l T1 T2 @@ -10215,9 +10209,9 @@ then have **: "norm ((\(x, k)\p. content k *\<^sub>R f x) + setsum (setsum (\(x, k). content k *\<^sub>R f x) \ qq) r - integral (cbox a b) f) < e" - apply (subst (asm) setsum_reindex_nonzero) + apply (subst (asm) setsum.reindex_nontrivial) apply fact - apply (rule setsum_0') + apply (rule setsum.neutral) apply rule unfolding split_paired_all split_conv defer @@ -10247,7 +10241,7 @@ proof - case goal2 have *: "(\(x, k)\p. integral k f) = (\k\snd ` p. integral k f)" - apply (subst setsum_reindex_nonzero) + apply (subst setsum.reindex_nontrivial) apply fact unfolding split_paired_all snd_conv split_def o_def proof - @@ -10264,12 +10258,11 @@ apply auto done qed auto + from q(1) have **: "snd ` p \ q = q" by auto show ?case unfolding integral_combine_division_topdown[OF assms(1) q(2)] * r_def - apply (rule setsum_Un_disjoint'[symmetric]) - using q(1) q'(1) p'(1) - apply auto - done + using ** q'(1) p'(1) setsum.union_disjoint [of "snd ` p" "q - snd ` p" "\k. integral k f", symmetric] + by simp next case goal1 have *: "k * real (card r) / (1 + real (card r)) < k" @@ -10377,7 +10370,7 @@ done have th: "op ^ x o op + m = (\i. x^m * x^i)" by (rule ext) (simp add: power_add power_mult) - from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]] + from setsum.reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]] have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp then show ?thesis @@ -10622,7 +10615,8 @@ [of _ "norm (setsum (\(x,k). content k *\<^sub>R f t x - integral k (f t)) {xk \ p. m (fst xk) = t})"]) apply (rule eq_refl) apply (rule arg_cong[where f=norm]) - apply (rule setsum_cong2) + apply (rule setsum.cong) + apply (rule refl) defer apply (rule henstock_lemma_part1) apply (rule assms(1)[rule_format]) @@ -11507,7 +11501,7 @@ apply auto done also have "\ = (\k\{k \ l |l. l \ snd ` p}. norm (integral k f))" - apply (rule setsum_mono_zero_left) + apply (rule setsum.mono_neutral_left) apply (subst simple_image) apply (rule finite_imageI)+ apply fact @@ -11525,7 +11519,7 @@ qed also have "\ = (\l\snd ` p. norm (integral (k \ l) f))" unfolding simple_image - apply (rule setsum_reindex_nonzero[unfolded o_def]) + apply (rule setsum.reindex_nontrivial [unfolded o_def]) apply (rule finite_imageI) apply (rule p') proof - @@ -11557,7 +11551,7 @@ unfolding split_def .. also have "\ = (\k\{i \ l |i l. i \ d \ l \ snd ` p}. norm (integral k f))" unfolding * - apply (rule setsum_reindex_nonzero[symmetric,unfolded o_def]) + apply (rule setsum.reindex_nontrivial [symmetric, unfolded o_def]) apply (rule finite_product_dependent) apply fact apply (rule finite_imageI) @@ -11598,7 +11592,7 @@ qed also have "\ = (\(x, k)\p'. norm (integral k f))" unfolding sum_p' - apply (rule setsum_mono_zero_right) + apply (rule setsum.mono_neutral_right) apply (subst *) apply (rule finite_imageI[OF finite_product_dependent]) apply fact @@ -11642,7 +11636,7 @@ note pdfin = finite_cartesian_product[OF p'(1) d'(1)] have "(\(x, k)\p'. norm (content k *\<^sub>R f x)) = (\(x, k)\?S. \content k\ * norm (f x))" unfolding norm_scaleR - apply (rule setsum_mono_zero_left) + apply (rule setsum.mono_neutral_left) apply (subst *) apply (rule finite_imageI) apply fact @@ -11656,7 +11650,7 @@ done also have "\ = (\((x,l),i)\p \ d. \content (l \ i)\ * norm (f x))" unfolding * - apply (subst setsum_reindex_nonzero) + apply (subst setsum.reindex_nontrivial) apply fact unfolding split_paired_all unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff Pair_eq @@ -11694,7 +11688,8 @@ apply (rule p') apply rule apply (rule d') - apply (rule setsum_cong2) + apply (rule setsum.cong) + apply (rule refl) unfolding split_paired_all split_conv proof - fix x l @@ -11702,7 +11697,8 @@ note xl = p'(2-4)[OF this] from this(3) guess u v by (elim exE) note uv=this have "(\i\d. \content (l \ i)\) = (\k\d. content (k \ cbox u v))" - apply (rule setsum_cong2) + apply (rule setsum.cong) + apply (rule refl) apply (drule d'(4)) apply safe apply (subst Int_commute) @@ -11712,7 +11708,7 @@ done also have "\ = setsum content {k \ cbox u v| k. k \ d}" unfolding simple_image - apply (rule setsum_reindex_nonzero[unfolded o_def,symmetric]) + apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric]) apply (rule d') proof - case goal1 @@ -11731,7 +11727,7 @@ unfolding uv inter_interval content_eq_0_interior .. qed also have "\ = setsum content {cbox u v \ k |k. k \ d \ cbox u v \ k \ {}}" - apply (rule setsum_mono_zero_right) + apply (rule setsum.mono_neutral_right) unfolding simple_image apply (rule finite_imageI) apply (rule d') @@ -11901,7 +11897,8 @@ using d1(2)[rule_format,OF conjI[OF p(1,2)]] by (simp only: real_norm_def) show "(\(x, k)\p. content k *\<^sub>R norm (f x)) = (\(x, k)\p. norm (content k *\<^sub>R f x))" - apply (rule setsum_cong2) + apply (rule setsum.cong) + apply (rule refl) unfolding split_paired_all split_conv apply (drule tagged_division_ofD(4)[OF p(1)]) unfolding norm_scaleR @@ -11965,7 +11962,7 @@ then have "(\k\d. norm (integral k (\x. f x + g x))) \ (\k\d. norm (integral k f)) + (\k\d. norm (integral k g))" apply - - unfolding setsum_addf[symmetric] + unfolding setsum.distrib [symmetric] apply (rule setsum_mono) apply (subst integral_add) prefer 3 @@ -12080,7 +12077,7 @@ have *: "\x. ?Tf x = (\i\Basis. ((\y. (\j\Basis. (if j = i then y else 0) *\<^sub>R j)) o (\x. (norm (\j\Basis. (if j = i then f x\T i else 0) *\<^sub>R j)))) x)" - by (simp add: comp_def if_distrib setsum_cases) + by (simp add: comp_def if_distrib setsum.If_cases) show ?thesis unfolding * apply (rule absolutely_integrable_setsum[OF finite_Basis]) @@ -12191,7 +12188,7 @@ done qed also have "\ \ setsum (op \ (integral UNIV (\x. (\i\Basis. \f x\i\ *\<^sub>R i)::'m))) Basis" - apply (subst setsum_commute) + apply (subst setsum.commute) apply (rule setsum_mono) proof - case goal1 diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sat Jun 28 09:16:42 2014 +0200 @@ -166,8 +166,8 @@ assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \ T" shows "setsum (\y. setsum g {x. x \ S \ f x = y}) T = setsum g S" apply (subst setsum_image_gen[OF fS, of g f]) - apply (rule setsum_mono_zero_right[OF fT fST]) - apply (auto intro: setsum_0') + apply (rule setsum.mono_neutral_right[OF fT fST]) + apply (auto intro: setsum.neutral) done lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = z" @@ -370,13 +370,13 @@ apply (auto simp add: bilinear_def) done also have "\ = setsum (\x. setsum (\y. h (f x) (g y)) T) S" - apply (rule setsum_cong, simp) + apply (rule setsum.cong, simp) apply (rule linear_setsum[unfolded o_def]) using bh fT apply (auto simp add: bilinear_def) done finally show ?thesis - unfolding setsum_cartesian_product . + unfolding setsum.cartesian_product . qed @@ -1090,7 +1090,7 @@ assume xS: "x \ S" have th00: "(\v\S. (if v = x then c else u v) *\<^sub>R v) = y" unfolding u[symmetric] - apply (rule setsum_cong2) + apply (rule setsum.cong) using xS apply auto done @@ -1123,7 +1123,7 @@ using fS aS apply simp apply (subst (2) ua[symmetric]) - apply (rule setsum_cong2) + apply (rule setsum.cong) apply auto done with th0 have ?rhs by fast @@ -1174,7 +1174,7 @@ unfolding span_explicit by blast let ?u = "\x. if x \ S' then u x else 0" have "setsum (\v. ?u v *\<^sub>R v) S = setsum (\v. u v *\<^sub>R v) S'" - using SS' fS by (auto intro!: setsum_mono_zero_cong_right) + using SS' fS by (auto intro!: setsum.mono_neutral_cong_right) then have "setsum (\v. ?u v *\<^sub>R v) S = y" by (metis u) then have "y \ ?rhs" by auto } @@ -1428,14 +1428,14 @@ have "(\x\P. norm (f x)) \ (\x\P. \b\Basis. \f x \ b\)" by (rule setsum_mono) (rule norm_le_l1) also have "(\x\P. \b\Basis. \f x \ b\) = (\b\Basis. \x\P. \f x \ b\)" - by (rule setsum_commute) + by (rule setsum.commute) also have "\ \ of_nat (card (Basis :: 'n set)) * (2 * e)" proof (rule setsum_bounded) fix i :: 'n assume i: "i \ Basis" have "norm (\x\P. \f x \ i\) \ norm ((\x\P \ - {x. f x \ i < 0}. f x) \ i) + norm ((\x\P \ {x. f x \ i < 0}. f x) \ i)" - by (simp add: abs_real_def setsum_cases[OF fP] setsum_negf norm_triangle_ineq4 inner_setsum_left + by (simp add: abs_real_def setsum.If_cases[OF fP] setsum_negf norm_triangle_ineq4 inner_setsum_left del: real_norm_def) also have "\ \ e + e" unfolding real_norm_def @@ -1538,7 +1538,7 @@ unfolding bilinear_setsum[OF bh finite_Basis finite_Basis] .. finally have th: "norm (h x y) = \" . show "norm (h x y) \ (\i\Basis. \j\Basis. norm (h i j)) * norm x * norm y" - apply (auto simp add: setsum_left_distrib th setsum_cartesian_product) + apply (auto simp add: setsum_left_distrib th setsum.cartesian_product) apply (rule setsum_norm_le) apply simp apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] @@ -1958,9 +1958,9 @@ have "orthogonal ?a y" unfolding orthogonal_def unfolding inner_diff inner_setsum_left right_minus_eq - unfolding setsum_diff1' [OF `finite C` `y \ C`] + unfolding setsum.remove [OF `finite C` `y \ C`] apply (clarsimp simp add: inner_commute[of y a]) - apply (rule setsum_0') + apply (rule setsum.neutral) apply clarsimp apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) using `y \ C` by auto @@ -2052,7 +2052,7 @@ unfolding setsum_clauses(2)[OF fth] apply simp unfolding inner_simps apply (clarsimp simp add: inner_add inner_setsum_left) - apply (rule setsum_0', rule ballI) + apply (rule setsum.neutral, rule ballI) unfolding inner_commute apply (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format]) @@ -2806,8 +2806,8 @@ by (simp add: Basis_le_norm infnorm_Max) lemma (in euclidean_space) euclidean_inner: "inner x y = (\b\Basis. (x \ b) * (y \ b))" - by (subst (1 2) euclidean_representation[symmetric]) - (simp add: inner_setsum_left inner_setsum_right setsum_cases inner_Basis ac_simps if_distrib) + by (subst (1 2) euclidean_representation [symmetric]) + (simp add: inner_setsum_right inner_Basis ac_simps) lemma norm_le_infnorm: fixes x :: "'a::euclidean_space" diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Sat Jun 28 09:16:42 2014 +0200 @@ -48,7 +48,7 @@ lemma inner_Basis_inf_left: "i \ Basis \ inf x y \ i = inf (x \ i) (y \ i)" and inner_Basis_sup_left: "i \ Basis \ sup x y \ i = sup (x \ i) (y \ i)" - by (simp_all add: eucl_inf eucl_sup inner_setsum_left inner_Basis if_distrib setsum_delta + by (simp_all add: eucl_inf eucl_sup inner_setsum_left inner_Basis if_distrib comm_monoid_add_class.setsum.delta cong: if_cong) lemma inner_Basis_INF_left: "i \ Basis \ (INF x:X. f x) \ i = (INF x:X. f x \ i)" @@ -119,7 +119,7 @@ hence "Inf ?proj = x \ b" by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum simp del: Inf_class.Inf_image_eq) hence "x \ b = Inf X \ b" - by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \ Basis` setsum_delta + by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \ Basis` setsum.delta simp del: Inf_class.Inf_image_eq cong: if_cong) with x show "\x. x \ X \ x \ b = Inf X \ b \ (\y. y \ X \ x \ b \ y \ b)" by blast @@ -142,7 +142,7 @@ hence "Sup ?proj = x \ b" by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq) hence "x \ b = Sup X \ b" - by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \ Basis` setsum_delta + by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \ Basis` setsum.delta simp del: Sup_image_eq cong: if_cong) with x show "\x. x \ X \ x \ b = Sup X \ b \ (\y. y \ X \ y \ b \ x \ b)" by blast qed diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Jun 28 09:16:42 2014 +0200 @@ -7173,7 +7173,7 @@ then have "(\i\d. (x \ i) *\<^sub>R i) \ span d" by (simp add: span_setsum span_clauses) also have "(\i\d. (x \ i) *\<^sub>R i) = (\i\Basis. (x \ i) *\<^sub>R i)" - by (rule setsum_mono_zero_cong_left [OF finite_Basis d]) (auto simp add: x) + by (rule setsum.mono_neutral_cong_left [OF finite_Basis d]) (auto simp add: x) finally show "x \ span d" unfolding euclidean_representation . qed diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/NSA/HSeries.thy --- a/src/HOL/NSA/HSeries.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/NSA/HSeries.thy Sat Jun 28 09:16:42 2014 +0200 @@ -55,7 +55,7 @@ lemma sumhr_add: "!!m n. sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)" -unfolding sumhr_app by transfer (rule setsum_addf [symmetric]) +unfolding sumhr_app by transfer (rule setsum.distrib [symmetric]) lemma sumhr_mult: "!!m n. hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)" diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Nat_Transfer.thy --- a/src/HOL/Nat_Transfer.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Nat_Transfer.thy Sat Jun 28 09:16:42 2014 +0200 @@ -194,9 +194,9 @@ lemma transfer_nat_int_sum_prod: "setsum f A = setsum (%x. f (nat x)) (int ` A)" "setprod f A = setprod (%x. f (nat x)) (int ` A)" - apply (subst setsum_reindex) + apply (subst setsum.reindex) apply (unfold inj_on_def, auto) - apply (subst setprod_reindex) + apply (subst setprod.reindex) apply (unfold inj_on_def o_def, auto) done @@ -237,7 +237,7 @@ *) (* Making A = B in this lemma doesn't work. Why not? - Also, why aren't setsum_cong and setprod_cong enough, + Also, why aren't setsum.cong and setprod.cong enough, with the previously mentioned rule turned on? *) lemma transfer_nat_int_sum_prod_cong: @@ -246,9 +246,9 @@ "A = B \ nat_set B \ (!!x. x >= 0 \ f x = g x) \ setprod f A = setprod g B" unfolding nat_set_def - apply (subst setsum_cong, assumption) + apply (subst setsum.cong, assumption) apply auto [2] - apply (subst setprod_cong, assumption, auto) + apply (subst setprod.cong, assumption, auto) done declare transfer_morphism_nat_int [transfer add @@ -399,11 +399,11 @@ lemma transfer_int_nat_sum_prod: "nat_set A \ setsum f A = setsum (%x. f (int x)) (nat ` A)" "nat_set A \ setprod f A = setprod (%x. f (int x)) (nat ` A)" - apply (subst setsum_reindex) + apply (subst setsum.reindex) apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff) - apply (subst setprod_reindex) + apply (subst setprod.reindex) apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff - cong: setprod_cong) + cong: setprod.cong) done (* this handles the case where the *range* of f is int *) @@ -413,11 +413,11 @@ setprod f A = int(setprod (%x. nat (f x)) A)" unfolding is_nat_def apply (subst int_setsum, auto) - apply (subst int_setprod, auto simp add: cong: setprod_cong) + apply (subst int_setprod, auto simp add: cong: setprod.cong) done declare transfer_morphism_int_nat [transfer add return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2 - cong: setsum_cong setprod_cong] + cong: setsum.cong setprod.cong] end diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Number_Theory/Binomial.thy --- a/src/HOL/Number_Theory/Binomial.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Number_Theory/Binomial.thy Sat Jun 28 09:16:42 2014 +0200 @@ -173,7 +173,7 @@ also have "\ = a^(n+1) + b^(n+1) + (\k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))" - by (auto simp add: field_simps setsum_addf [symmetric] choose_reduce_nat) + by (auto simp add: field_simps setsum.distrib [symmetric] choose_reduce_nat) also have "\ = (\k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))" using decomp by (simp add: field_simps) finally show "?P (Suc n)" by simp @@ -263,13 +263,13 @@ have *: "finite {1 .. n}" "0 \ {1 .. n}" by auto have eq: "insert 0 {1 .. n} = {0..n}" by auto have **: "(\n\{1\nat..n}. a + of_nat n) = (\n\{0\nat..n - 1}. a + 1 + of_nat n)" - apply (rule setprod_reindex_cong [where f = Suc]) + apply (rule setprod.reindex_cong [where l = Suc]) using False apply (auto simp add: fun_eq_iff field_simps) done show ?thesis apply (simp add: pochhammer_def) - unfolding setprod_insert [OF *, unfolded eq] + unfolding setprod.insert [OF *, unfolded eq] using ** apply (simp add: field_simps) done qed @@ -278,7 +278,7 @@ unfolding fact_altdef_nat apply (cases n) apply (simp_all add: of_nat_setprod pochhammer_Suc_setprod) - apply (rule setprod_reindex_cong[where f=Suc]) + apply (rule setprod.reindex_cong [where l = Suc]) apply (auto simp add: fun_eq_iff) done @@ -347,7 +347,7 @@ using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"] by auto show ?thesis - unfolding Suc pochhammer_Suc_setprod eq setprod_timesf[symmetric] + unfolding Suc pochhammer_Suc_setprod eq setprod.distrib[symmetric] by (rule setprod.reindex_bij_witness[where i="op - h" and j="op - h"]) (auto simp: of_nat_diff) qed @@ -390,7 +390,7 @@ by auto from False show ?thesis by (simp add: pochhammer_def gbinomial_def field_simps - eq setprod_timesf[symmetric]) + eq setprod.distrib[symmetric]) qed lemma binomial_fact_lemma: "k \ n \ fact k * fact (n - k) * (n choose k) = fact n" @@ -459,10 +459,10 @@ apply (simp add: binomial_fact[OF kn, where ?'a = 'a] gbinomial_pochhammer field_simps pochhammer_Suc_setprod) apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h - of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc) - unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \ 'a"] eq[unfolded h] + of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc) + unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \ 'a"] eq[unfolded h] unfolding mult_assoc[symmetric] - unfolding setprod_timesf[symmetric] + unfolding setprod.distrib[symmetric] apply simp apply (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"]) apply (auto simp: of_nat_diff) @@ -520,7 +520,7 @@ next case (Suc h) have eq0: "(\i\{1..k}. (a + 1) - of_nat i) = (\i\{0..h}. a - of_nat i)" - apply (rule strong_setprod_reindex_cong[where f = Suc]) + apply (rule setprod.reindex_cong [where l = Suc]) using Suc apply auto done @@ -573,7 +573,7 @@ by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost) also have "\ = (\i n` unfolding fact_eq_rev_setprod_nat of_nat_setprod - by (auto simp add: setprod_dividef intro!: setprod_cong of_nat_diff[symmetric]) + by (auto simp add: setprod_dividef intro!: setprod.cong of_nat_diff[symmetric]) finally show ?thesis . next case False @@ -702,15 +702,15 @@ also have "\ = nat (\I | I \ A \ I \ {}. (\_\\I. -1 ^ (card I + 1)))" (is "_ = nat ?rhs") by(subst setsum_right_distrib) simp also have "?rhs = (\(I, _)\Sigma {I. I \ A \ I \ {}} Inter. -1 ^ (card I + 1))" - using assms by(subst setsum_Sigma)(auto) + using assms by(subst setsum.Sigma)(auto) also have "\ = (\(x, I)\(SIGMA x:UNIV. {I. I \ A \ I \ {} \ x \ \I}). -1 ^ (card I + 1))" - by(rule setsum_reindex_cong[where f="\(x, y). (y, x)"])(auto intro: inj_onI simp add: split_beta) + by (rule setsum.reindex_cong [where l = "\(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta) also have "\ = (\(x, I)\(SIGMA x:\A. {I. I \ A \ I \ {} \ x \ \I}). -1 ^ (card I + 1))" - using assms by(auto intro!: setsum_mono_zero_cong_right finite_SigmaI2 intro: finite_subset[where B="\A"]) + using assms by(auto intro!: setsum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\A"]) also have "\ = (\x\\A. (\I|I \ A \ I \ {} \ x \ \I. -1 ^ (card I + 1)))" - using assms by(subst setsum_Sigma) auto + using assms by(subst setsum.Sigma) auto also have "\ = (\_\\A. 1)" (is "setsum ?lhs _ = _") - proof(rule setsum_cong[OF refl]) + proof(rule setsum.cong[OF refl]) fix x assume x: "x \ \A" def K \ "{X \ A. x \ X}" @@ -723,13 +723,13 @@ simp add: card_gt_0_iff[folded Suc_le_eq] dest: finite_subset intro: card_mono) ultimately have "?lhs x = (\(i, I)\(SIGMA i:{1..card A}. ?I i). -1 ^ (i + 1))" - by(rule setsum_reindex_cong[where f=snd]) fastforce + by (rule setsum.reindex_cong [where l = snd]) fastforce also have "\ = (\i=1..card A. (\I|I \ A \ card I = i \ x \ \I. -1 ^ (i + 1)))" - using assms by(subst setsum_Sigma) auto + using assms by(subst setsum.Sigma) auto also have "\ = (\i=1..card A. -1 ^ (i + 1) * (\I|I \ A \ card I = i \ x \ \I. 1))" by(subst setsum_right_distrib) simp also have "\ = (\i=1..card K. -1 ^ (i + 1) * (\I|I \ K \ card I = i. 1))" (is "_ = ?rhs") - proof(rule setsum_mono_zero_cong_right[rule_format]) + proof(rule setsum.mono_neutral_cong_right[rule_format]) show "{1..card K} \ {1..card A}" using `finite A` by(auto simp add: K_def intro: card_mono) next @@ -746,7 +746,7 @@ fix i have "(\I | I \ A \ card I = i \ x \ \I. 1) = (\I | I \ K \ card I = i. 1 :: int)" (is "?lhs = ?rhs") - by(rule setsum_cong)(auto simp add: K_def) + by(rule setsum.cong)(auto simp add: K_def) thus "-1 ^ (i + 1) * ?lhs = -1 ^ (i + 1) * ?rhs" by simp qed simp also have "{I. I \ K \ card I = 0} = {{}}" using assms diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Number_Theory/Cong.thy --- a/src/HOL/Number_Theory/Cong.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Number_Theory/Cong.thy Sat Jun 28 09:16:42 2014 +0200 @@ -805,7 +805,7 @@ proof - from fin a have "?x = (SUM j:{i}. u j * b j) + (SUM j:A-{i}. u j * b j)" - by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong) + by (subst setsum.union_disjoint [symmetric], auto intro: setsum.cong) then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)" by auto also have "[u i * b i + (SUM j:A-{i}. u j * b j) = diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Number_Theory/Gauss.thy --- a/src/HOL/Number_Theory/Gauss.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Number_Theory/Gauss.thy Sat Jun 28 09:16:42 2014 +0200 @@ -239,12 +239,13 @@ by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E) lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C" - by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod_Un_disjoint sup_commute) + by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod.union_disjoint sup_commute) lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)" apply (auto simp add: C_def) apply (insert finite_B SR_B_inj) - apply (frule_tac f = "\x. x mod int p" in setprod_reindex_id [symmetric], auto) + apply (drule setprod.reindex [of "\x. x mod int p" B id]) + apply auto apply (rule cong_setprod_int) apply (auto simp add: cong_int_def) done @@ -291,14 +292,14 @@ by (auto simp add: card_seteq) lemma prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A" - by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod_Un_disjoint) + by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod.union_disjoint) lemma prod_F_zcong: "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)" proof - have FE: "setprod id F = setprod (op - p) E" apply (auto simp add: F_def) apply (insert finite_E inj_on_pminusx_E) - apply (frule setprod_reindex_id, auto) + apply (drule setprod.reindex, auto) done then have "\x \ E. [(p-x) mod p = - x](mod p)" by (metis cong_int_def minus_mod_self1 mod_mod_trivial) @@ -324,7 +325,7 @@ "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)" proof - have "[setprod id A = setprod id F * setprod id D](mod p)" - by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod_cong) + by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod.cong) then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)" apply (rule cong_trans_int) apply (metis cong_scalar_int prod_F_zcong) @@ -338,7 +339,7 @@ by (simp add: B_def) then have "[setprod id A = ((-1)^(card E) * (setprod (\x. x * a) A))] (mod p)" - by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong) + by (simp add: inj_on_xa_A setprod.reindex) moreover have "setprod (\x. x * a) A = setprod (\x. a) A * setprod id A" using finite_A by (induct set: finite) auto @@ -360,7 +361,7 @@ done then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)" apply (rule cong_trans_int) - apply (simp add: aux cong del:setprod_cong) + apply (simp add: aux cong del:setprod.cong) done with A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)" by (metis cong_mult_lcancel_int) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Number_Theory/UniqueFactorization.thy --- a/src/HOL/Number_Theory/UniqueFactorization.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Sat Jun 28 09:16:42 2014 +0200 @@ -89,7 +89,7 @@ then have b: "set_of N = {a} Un (set_of N - {a})" by auto then show ?thesis - by (subst (1) b, subst setprod_Un_disjoint, auto) + by (subst (1) b, subst setprod.union_disjoint, auto) next assume "a ~: set_of N" then show ?thesis by auto @@ -458,18 +458,18 @@ apply (simp only: prime_factors_altdef_nat) apply auto apply (subst power_add) - apply (subst setprod_timesf) + apply (subst setprod.distrib) apply (rule arg_cong2 [where f = "\x y. x*y"]) apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors k Un (prime_factors l - prime_factors k)") apply (erule ssubst) - apply (subst setprod_Un_disjoint) + apply (subst setprod.union_disjoint) apply auto apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const) apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un (prime_factors k - prime_factors l)") apply (erule ssubst) - apply (subst setprod_Un_disjoint) + apply (subst setprod.union_disjoint) apply auto apply (subgoal_tac "(\p\prime_factors k - prime_factors l. p ^ multiplicity p l) = (\p\prime_factors k - prime_factors l. 1)") @@ -545,11 +545,11 @@ [where f = "%x. nat(int(nat(f x)))", transferred direction: nat "op <= (0::int)"]) apply auto - apply (subst (asm) setprod_cong) + apply (subst (asm) setprod.cong) apply (rule refl) apply (rule if_P) apply auto - apply (rule setsum_cong) + apply (rule setsum.cong) apply auto done @@ -566,10 +566,10 @@ prefer 5 apply (rule refl) apply (rule refl) apply auto - apply (subst setprod_mono_one_right) + apply (subst setprod.mono_neutral_right) apply assumption prefer 3 - apply (rule setprod_cong) + apply (rule setprod.cong) apply (rule refl) apply auto done diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Old_Number_Theory/Euler.thy --- a/src/HOL/Old_Number_Theory/Euler.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Old_Number_Theory/Euler.thy Sat Jun 28 09:16:42 2014 +0200 @@ -180,7 +180,7 @@ proof - from assms have "[\(Union (SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)" by (auto simp add: SetS_finite SetS_elems_finite - MultInvPair_prop1c setprod_Union_disjoint) + MultInvPair_prop1c setprod.Union_disjoint) also have "[setprod (setprod (%x. x)) (SetS a p) = setprod (%x. a) (SetS a p)] (mod p)" by (rule setprod_same_function_zcong) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Old_Number_Theory/EulerFermat.thy --- a/src/HOL/Old_Number_Theory/EulerFermat.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Sat Jun 28 09:16:42 2014 +0200 @@ -252,7 +252,7 @@ apply (simplesubst BnorRset.simps) --{*multiple redexes*} apply (unfold Let_def, auto) apply (simp add: Bnor_fin Bnor_mem_zle_swap) - apply (subst setprod_insert) + apply (subst setprod.insert) apply (rule_tac [2] Bnor_prod_power_aux) apply (unfold inj_on_def) apply (simp_all add: mult_ac Bnor_fin Bnor_mem_zle_swap) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Old_Number_Theory/Gauss.thy --- a/src/HOL/Old_Number_Theory/Gauss.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Old_Number_Theory/Gauss.thy Sat Jun 28 09:16:42 2014 +0200 @@ -299,14 +299,15 @@ lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C" apply (insert D_E_disj finite_D finite_E C_eq) - apply (frule setprod_Un_disjoint [of D E id]) + apply (frule setprod.union_disjoint [of D E id]) apply auto done lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)" apply (auto simp add: C_def) apply (insert finite_B SR_B_inj) - apply (frule_tac f = "StandardRes p" in setprod_reindex_id [symmetric], auto) + apply (frule setprod.reindex [of "StandardRes p" B id]) + apply auto apply (rule setprod_same_function_zcong) apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0) done @@ -378,7 +379,7 @@ lemma prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A" apply (insert F_D_disj finite_D finite_F) - apply (frule setprod_Un_disjoint [of F D id]) + apply (frule setprod.union_disjoint [of F D id]) apply (auto simp add: F_Un_D_eq_A) done @@ -390,7 +391,8 @@ then have "setprod id F = setprod (op - p) E" apply simp apply (insert finite_E inj_on_pminusx_E) - apply (frule_tac f = "op - p" in setprod_reindex_id, auto) + apply (frule setprod.reindex [of "minus p" E id]) + apply auto done then have one: "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)" @@ -441,11 +443,11 @@ "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)" proof - have "[setprod id A = setprod id F * setprod id D](mod p)" - by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod_cong) + by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod.cong) then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)" apply (rule zcong_trans) - apply (auto simp add: prod_F_zcong zcong_scalar cong del: setprod_cong) + apply (auto simp add: prod_F_zcong zcong_scalar cong del: setprod.cong) done then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)" apply (rule zcong_trans) @@ -454,14 +456,14 @@ done then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)" apply (rule zcong_trans) - apply (simp add: C_B_zcong_prod zcong_scalar2 cong del:setprod_cong) + apply (simp add: C_B_zcong_prod zcong_scalar2 cong del:setprod.cong) done then have "[setprod id A = ((-1)^(card E) * (setprod id ((%x. x * a) ` A)))] (mod p)" by (simp add: B_def) then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))] (mod p)" - by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong) + by (simp add:finite_A inj_on_xa_A setprod.reindex cong del:setprod.cong) moreover have "setprod (%x. x * a) A = setprod (%x. a) A * setprod id A" using finite_A by (induct set: finite) auto @@ -484,7 +486,7 @@ then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)" apply (rule zcong_trans) - apply (simp add: aux cong del:setprod_cong) + apply (simp add: aux cong del:setprod.cong) done with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"] p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)" diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Old_Number_Theory/Pocklington.thy --- a/src/HOL/Old_Number_Theory/Pocklington.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy Sat Jun 28 09:16:42 2014 +0200 @@ -575,7 +575,7 @@ lemma nproduct_cmul: assumes fS:"finite S" shows "setprod (\m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * setprod a S" -unfolding setprod_timesf setprod_constant[OF fS, of c] .. +unfolding setprod.distrib setprod_constant[OF fS, of c] .. lemma coprime_nproduct: assumes fS: "finite S" and Sn: "\x\S. coprime n (a x)" diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Sat Jun 28 09:16:42 2014 +0200 @@ -24,20 +24,20 @@ also have "setsum (%x. a * x) = setsum (%x. x * a)" by (auto simp add: mult_commute) also have "setsum (%x. x * a) A = setsum id B" - by (simp add: B_def setsum_reindex_id[OF inj_on_xa_A]) + by (simp add: B_def setsum.reindex [OF inj_on_xa_A]) also have "... = setsum (%x. p * (x div p) + StandardRes p x) B" by (auto simp add: StandardRes_def zmod_zdiv_equality) also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B" - by (rule setsum_addf) + by (rule setsum.distrib) also have "setsum (StandardRes p) B = setsum id C" - by (auto simp add: C_def setsum_reindex_id[OF SR_B_inj]) + by (auto simp add: C_def setsum.reindex [OF SR_B_inj]) also from C_eq have "... = setsum id (D \ E)" by auto also from finite_D finite_E have "... = setsum id D + setsum id E" - by (rule setsum_Un_disjoint) (auto simp add: D_def E_def) + by (rule setsum.union_disjoint) (auto simp add: D_def E_def) also have "setsum (%x. p * (x div p)) B = setsum ((%x. p * (x div p)) o (%x. (x * a))) A" - by (auto simp add: B_def setsum_reindex inj_on_xa_A) + by (auto simp add: B_def setsum.reindex inj_on_xa_A) also have "... = setsum (%x. p * ((x * a) div p)) A" by (auto simp add: o_def) also from finite_A have "setsum (%x. p * ((x * a) div p)) A = @@ -53,12 +53,12 @@ by (simp add: Un_commute) also from F_D_disj finite_D finite_F have "... = setsum id D + setsum id F" - by (auto simp add: Int_commute intro: setsum_Un_disjoint) + by (auto simp add: Int_commute intro: setsum.union_disjoint) also from F_def have "F = (%x. (p - x)) ` E" by auto also from finite_E inj_on_pminusx_E have "setsum id ((%x. (p - x)) ` E) = setsum (%x. (p - x)) E" - by (auto simp add: setsum_reindex) + by (auto simp add: setsum.reindex) also from finite_E have "setsum (op - p) E = setsum (%x. p) E - setsum id E" by (auto simp add: setsum_subtractf id_def) also from finite_E have "setsum (%x. p) E = p * int(card E)" @@ -527,7 +527,7 @@ ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set" by auto also have "... = setsum (%j. q * j div p) P_set" - using aux3a by(fastforce intro: setsum_cong) + using aux3a by(fastforce intro: setsum.cong) finally show ?thesis . qed @@ -551,7 +551,7 @@ ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set" by auto also have "... = setsum (%j. p * j div q) Q_set" - using aux3b by(fastforce intro: setsum_cong) + using aux3b by(fastforce intro: setsum.cong) finally show ?thesis . qed diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Old_Number_Theory/WilsonBij.thy --- a/src/HOL/Old_Number_Theory/WilsonBij.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Old_Number_Theory/WilsonBij.thy Sat Jun 28 09:16:42 2014 +0200 @@ -229,9 +229,9 @@ apply (subgoal_tac [2] "a = 1 \ a = p - 1") apply (rule_tac [3] zcong_square_zless) apply auto - apply (subst setprod_insert) + apply (subst setprod.insert) prefer 3 - apply (subst setprod_insert) + apply (subst setprod.insert) apply (auto simp add: fin_bijER) apply (subgoal_tac "zcong ((a * b) * \A) (1 * 1) p") apply (simp add: mult_assoc) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Old_Number_Theory/WilsonRuss.thy --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Sat Jun 28 09:16:42 2014 +0200 @@ -251,8 +251,8 @@ prefer 2 apply (subst wset.simps) apply (auto, unfold Let_def, auto) - apply (subst setprod_insert) - apply (tactic {* stac @{thm setprod_insert} 3 *}) + apply (subst setprod.insert) + apply (tactic {* stac @{thm setprod.insert} 3 *}) apply (subgoal_tac [5] "zcong (a * inv p a * (\x\wset (a - 1) p. x)) (1 * 1) p") prefer 5 diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Power.thy --- a/src/HOL/Power.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Power.thy Sat Jun 28 09:16:42 2014 +0200 @@ -761,6 +761,22 @@ done qed + +subsubsection {* Generalized sum over a set *} + +lemma setsum_zero_power [simp]: + fixes c :: "nat \ 'a::division_ring" + shows "(\i\A. c i * 0^i) = (if finite A \ 0 \ A then c 0 else 0)" +apply (cases "finite A") + by (induction A rule: finite_induct) auto + +lemma setsum_zero_power' [simp]: + fixes c :: "nat \ 'a::field" + shows "(\i\A. c i * 0^i / d i) = (if finite A \ 0 \ A then c 0 / d 0 else 0)" + using setsum_zero_power [of "\i. c i / d i" A] + by auto + + subsubsection {* Generalized product over a set *} lemma setprod_constant: "finite A ==> (\x\ A. (y::'a::{comm_monoid_mult})) = y^(card A)" @@ -768,6 +784,17 @@ apply auto done +lemma setprod_power_distrib: + fixes f :: "'a \ 'b::comm_semiring_1" + shows "setprod f A ^ n = setprod (\x. (f x) ^ n) A" +proof (cases "finite A") + case True then show ?thesis + by (induct A rule: finite_induct) (auto simp add: power_mult_distrib) +next + case False then show ?thesis + by simp +qed + lemma setprod_gen_delta: assumes fS: "finite S" shows "setprod (\k. if k=a then b k else c) S = (if a \ S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)" @@ -784,14 +811,14 @@ have dj: "?A \ ?B = {}" by simp from fS have fAB: "finite ?A" "finite ?B" by auto have fA0:"setprod ?f ?A = setprod (\i. c) ?A" - apply (rule setprod_cong) by auto + apply (rule setprod.cong) by auto have cA: "card ?A = card S - 1" using fS a by auto have fA1: "setprod ?f ?A = c ^ card ?A" unfolding fA0 apply (rule setprod_constant) using fS by auto have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" - using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] + using setprod.union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] by simp then have ?thesis using a cA - by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)} + by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)} ultimately show ?thesis by blast qed diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Bochner_Integration.thy --- a/src/HOL/Probability/Bochner_Integration.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Probability/Bochner_Integration.thy Sat Jun 28 09:16:42 2014 +0200 @@ -165,7 +165,7 @@ shows setsum_mult_indicator[simp]: "(\x \ A. f x * indicator (B x) (g x)) = (\x\{x\A. g x \ B x}. f x)" and setsum_indicator_mult[simp]: "(\x \ A. indicator (B x) (g x) * f x) = (\x\{x\A. g x \ B x}. f x)" unfolding indicator_def - using assms by (auto intro!: setsum_mono_zero_cong_right split: split_if_asm) + using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm) lemma borel_measurable_induct_real[consumes 2, case_names set mult add seq]: fixes P :: "('a \ real) \ bool" @@ -343,7 +343,7 @@ (\y\f`space M. (\z\g`space M. if \x\space M. y = f x \ z = g x then measure M {x\space M. g x = z} else 0) *\<^sub>R y)" unfolding simple_bochner_integral_def - proof (safe intro!: setsum_cong scaleR_cong_right) + proof (safe intro!: setsum.cong scaleR_cong_right) fix y assume y: "y \ space M" "f y \ 0" have [simp]: "g ` space M \ {z. \x\space M. f y = f x \ z = g x} = {z. \x\space M. f y = f x \ z = g x}" @@ -365,17 +365,17 @@ ultimately show "measure M {x \ space M. f x = f y} = (\z\g ` space M. if \x\space M. f y = f x \ z = g x then measure M {x \ space M. g x = z} else 0)" - apply (simp add: setsum_cases eq) + apply (simp add: setsum.If_cases eq) apply (subst measure_finite_Union[symmetric]) apply (auto simp: disjoint_family_on_def) done qed also have "\ = (\y\f`space M. (\z\g`space M. if \x\space M. y = f x \ z = g x then measure M {x\space M. g x = z} *\<^sub>R y else 0))" - by (auto intro!: setsum_cong simp: scaleR_setsum_left) + by (auto intro!: setsum.cong simp: scaleR_setsum_left) also have "\ = ?r" - by (subst setsum_commute) - (auto intro!: setsum_cong simp: setsum_cases scaleR_setsum_right[symmetric] eq) + by (subst setsum.commute) + (auto intro!: setsum.cong simp: setsum.If_cases scaleR_setsum_right[symmetric] eq) finally show "simple_bochner_integral M f = ?r" . qed @@ -397,7 +397,7 @@ by (intro simple_bochner_integral_partition) (auto simp: simple_bochner_integrable_compose2 elim: simple_bochner_integrable.cases) ultimately show ?thesis - by (simp add: setsum_addf[symmetric] scaleR_add_right) + by (simp add: setsum.distrib[symmetric] scaleR_add_right) qed lemma (in linear) simple_bochner_integral_linear: @@ -474,7 +474,7 @@ unfolding simple_integral_def by (subst simple_bochner_integral_partition[OF f(1), where g="\x. ereal (f x)" and v=real]) (auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases - intro!: setsum_cong ereal_cong_mult + intro!: setsum.cong ereal_cong_mult simp: setsum_ereal[symmetric] times_ereal.simps(1)[symmetric] mult_ac simp del: setsum_ereal times_ereal.simps(1)) also have "\ = (\\<^sup>+x. f x \M)" @@ -879,7 +879,7 @@ by (auto simp: space_restrict_space measure_restrict_space[OF \(1)] le_infI2 simple_bochner_integral_def Collect_restrict split: split_indicator split_indicator_asm - intro!: setsum_mono_zero_cong_left arg_cong2[where f=measure]) + intro!: setsum.mono_neutral_cong_left arg_cong2[where f=measure]) qed inductive integrable for M f where @@ -2025,19 +2025,19 @@ shows "(\x. f x \count_space A) = (\a | a \ A \ f a \ 0. f a)" proof - have eq: "\x. x \ A \ (\a | x = a \ a \ A \ f a \ 0. f a) = (\x\{x}. f x)" - by (intro setsum_mono_zero_cong_left) auto + by (intro setsum.mono_neutral_cong_left) auto have "(\x. f x \count_space A) = (\x. (\a | a \ A \ f a \ 0. indicator {a} x *\<^sub>R f a) \count_space A)" by (intro integral_cong refl) (simp add: f eq) also have "\ = (\a | a \ A \ f a \ 0. measure (count_space A) {a} *\<^sub>R f a)" - by (subst integral_setsum) (auto intro!: setsum_cong) + by (subst integral_setsum) (auto intro!: setsum.cong) finally show ?thesis by auto qed lemma lebesgue_integral_count_space_finite: "finite A \ (\x. f x \count_space A) = (\a\A. f a)" by (subst lebesgue_integral_count_space_finite_support) - (auto intro!: setsum_mono_zero_cong_left) + (auto intro!: setsum.mono_neutral_cong_left) subsection {* Point measure *} @@ -2386,7 +2386,7 @@ (\z\s i ` (space N \ space M). measure M {y \ space M. s i (x, y) = z} *\<^sub>R z)" using s(1)[THEN simple_functionD(1)] unfolding simple_bochner_integral_def - by (intro setsum_mono_zero_cong_left) + by (intro setsum.mono_neutral_cong_left) (auto simp: eq_commute space_pair_measure image_iff cong: conj_cong) } note eq = this @@ -2752,7 +2752,7 @@ by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset) interpret I: finite_product_sigma_finite M I by default fact have *: "\x y. (\j\I. f j (if j = i then y else x j)) = (\j\I. f j (x j))" - using `i \ I` by (auto intro!: setprod_cong) + using `i \ I` by (auto intro!: setprod.cong) show ?case unfolding product_integral_insert[OF insert(1,2) prod[OF subset_refl]] by (simp add: * insert prod subset_insertI) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Caratheodory.thy --- a/src/HOL/Probability/Caratheodory.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Probability/Caratheodory.thy Sat Jun 28 09:16:42 2014 +0200 @@ -22,7 +22,7 @@ have g_def: "g = (\m. (\n. f (m,n)))" using assms by (simp add: fun_eq_iff) have reindex: "\B. (\x\B. f (prod_decode x)) = setsum f (prod_decode ` B)" - by (simp add: setsum_reindex[OF inj_prod_decode] comp_def) + by (simp add: setsum.reindex[OF inj_prod_decode] comp_def) { fix n let ?M = "\f. Suc (Max (f ` prod_decode ` {..(A`I)) = (\a\A`I. f a)" unfolding volume_def by blast also have "\ = (\i\I. f (A i))" - proof (subst setsum_reindex_nonzero) + proof (subst setsum.reindex_nontrivial) fix i j assume "i \ I" "j \ I" "i \ j" "A i = A j" with `disjoint_family_on A I` have "A i = {}" by (auto simp: disjoint_family_on_def) @@ -753,7 +753,7 @@ fix D assume D: "D \ M" "finite D" "disjoint D" assume "\C = \D" have "(\d\D. \ d) = (\d\D. \c\C. \ (c \ d))" - proof (intro setsum_cong refl) + proof (intro setsum.cong refl) fix d assume "d \ D" have Un_eq_d: "(\c\C. c \ d) = d" using `d \ D` `\C = \D` by auto @@ -775,7 +775,7 @@ assume "\C = \D" with split_sum[OF C D] split_sum[OF D C] have "(\d\D. \ d) = (\c\C. \ c)" - by (simp, subst setsum_commute, simp add: ac_simps) } + by (simp, subst setsum.commute, simp add: ac_simps) } note sum_eq = this { fix C assume C: "C \ M" "finite C" "disjoint C" @@ -810,7 +810,7 @@ also have "\ = (\c\Ca \ Cb. \ c) + (\c\Ca \ Cb. \ c)" using C_Int_cases volume_empty[OF `volume M \`] by (elim disjE) simp_all also have "\ = (\c\Ca. \ c) + (\c\Cb. \ c)" - using Ca Cb by (simp add: setsum_Un_Int) + using Ca Cb by (simp add: setsum.union_inter) also have "\ = \' a + \' b" using Ca Cb by (simp add: \') finally show "\' (a \ b) = \' a + \' b" @@ -863,7 +863,7 @@ by (simp add: sums_iff) qed also have "\ = (\c\C. \ c)" - using F'(2) by (subst (2) F') (simp add: setsum_reindex) + using F'(2) by (subst (2) F') (simp add: setsum.reindex) finally show "\ (\C) = (\c\C. \ c)" . next show "\ {} = 0" @@ -983,7 +983,7 @@ by (intro suminf_setsum_ereal positiveD2[OF pos] G.Int G.finite_Union) (auto intro: generated_ringI_Basic) also have "\ = (\c\C'. \_r c)" - using eq V C' by (auto intro!: setsum_cong) + using eq V C' by (auto intro!: setsum.cong) also have "\ = \_r (\C')" using C' Un_A by (subst volume_finite_additive[symmetric, OF V(1)]) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Distributions.thy --- a/src/HOL/Probability/Distributions.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Probability/Distributions.thy Sat Jun 28 09:16:42 2014 +0200 @@ -126,7 +126,7 @@ qed qed auto also have "\ = ereal (1 - (\n\k. (a^n * exp (-a)) / fact n))" - by (auto simp: power_0_left if_distrib[where f="\x. x / a" for a] setsum_cases) + by (auto simp: power_0_left if_distrib[where f="\x. x / a" for a] setsum.If_cases) finally show ?thesis by (cases "?I") (auto simp: field_simps) qed diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Finite_Product_Measure.thy --- a/src/HOL/Probability/Finite_Product_Measure.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Sat Jun 28 09:16:42 2014 +0200 @@ -636,12 +636,12 @@ by (auto simp: prod_emb_iff PiE_def Pi_iff split: split_if_asm) blast+ also have "emeasure (Pi\<^sub>M I M) (\\<^sub>E j\I. if j \ J-{i} then E j else space (M j)) = (\ j\I. if j \ J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))" - using E by (subst insert) (auto intro!: setprod_cong) + using E by (subst insert) (auto intro!: setprod.cong) also have "(\j\I. if j \ J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) * emeasure (M i) (if i \ J then E i else space (M i)) = (\j\insert i I. ?f J E j)" - using insert by (auto simp: mult_commute intro!: arg_cong2[where f="op *"] setprod_cong) + using insert by (auto simp: mult_commute intro!: arg_cong2[where f="op *"] setprod.cong) also have "\ = (\j\J \ ?I. ?f J E j)" - using insert(1,2) J E by (intro setprod_mono_one_right) auto + using insert(1,2) J E by (intro setprod.mono_neutral_right) auto finally show "?\ ?p = \" . show "prod_emb (insert i I) M J (Pi\<^sub>E J E) \ Pow (\\<^sub>E i\insert i I. space (M i))" @@ -653,7 +653,7 @@ show "(insert i I \ {} \ insert i I = {}) \ finite (insert i I) \ insert i I \ insert i I \ A \ (\ j\insert i I. sets (M j))" using insert by auto - qed (auto intro!: setprod_cong) + qed (auto intro!: setprod.cong) with insert show ?case by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space) qed simp @@ -764,7 +764,7 @@ using `finite J` `finite I` F unfolding X by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times) also have "\ = (\i\I \ J. emeasure (M i) (F i))" - using `finite J` `finite I` `I \ J = {}` by (simp add: setprod_Un_one) + using `finite J` `finite I` `I \ J = {}` by (simp add: setprod.union_inter_neutral) also have "\ = emeasure ?P (Pi\<^sub>E (I \ J) F)" using `finite J` `finite I` F unfolding A by (intro IJ.measure_times[symmetric]) auto @@ -849,7 +849,7 @@ note `finite I`[intro, simp] interpret I: finite_product_sigma_finite M I by default auto have *: "\x y. (\j\I. f j (if j = i then y else x j)) = (\j\I. f j (x j))" - using insert by (auto intro!: setprod_cong) + using insert by (auto intro!: setprod.cong) have prod: "\J. J \ insert i I \ (\x. (\i\J. f i (x i))) \ borel_measurable (Pi\<^sub>M J M)" using sets.sets_into_space insert by (intro borel_measurable_ereal_setprod diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Independent_Family.thy --- a/src/HOL/Probability/Independent_Family.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Probability/Independent_Family.thy Sat Jun 28 09:16:42 2014 +0200 @@ -203,7 +203,7 @@ have "prob (\i\insert j J. (A(j := X)) i) = (\i\insert j J. prob ((A(j := X)) i))" using J A `j \ K` by (intro indep_setsD[OF G']) auto then have "prob (\i\insert j J. (A(j := X)) i) = prob X * (\i\J. prob (A i))" - using `finite J` `j \ J` by (auto intro!: setprod_cong) } + using `finite J` `j \ J` by (auto intro!: setprod.cong) } ultimately have "prob ((\j\J. A j) \ (space M - X)) = (prob (space M) - prob X) * (\i\J. prob (A i))" by (simp add: field_simps) also have "\ = prob (space M - X) * (\i\J. prob (A i))" @@ -229,7 +229,7 @@ qed moreover { fix k from J A `j \ K` have "prob (\i\insert j J. (A(j := F k)) i) = prob (F k) * (\i\J. prob (A i))" - by (subst indep_setsD[OF F(2)]) (auto intro!: setprod_cong split: split_if_asm) + by (subst indep_setsD[OF F(2)]) (auto intro!: setprod.cong split: split_if_asm) also have "\ = prob (F k) * prob (\i\J. A i)" using J A `j \ K` by (subst indep_setsD[OF G(1)]) auto finally have "prob (\i\insert j J. (A(j := F k)) i) = prob (F k) * prob (\i\J. A i)" . } @@ -455,9 +455,9 @@ also have "\ = (\l\(\k\K. L k). prob (?E' l))" using L K E' by (intro indep_setsD[OF indep]) (simp_all add: UN_mono) also have "\ = (\j\K. \l\L j. prob (E' j l))" - using K L L_inj by (subst setprod_UN_disjoint) auto + using K L L_inj by (subst setprod.UNION_disjoint) auto also have "\ = (\j\K. prob (A j))" - using K L E' by (auto simp add: A intro!: setprod_cong indep_setsD[OF indep, symmetric]) blast + using K L E' by (auto simp add: A intro!: setprod.cong indep_setsD[OF indep, symmetric]) blast finally show "prob (\j\K. A j) = (\j\K. prob (A j))" . qed next @@ -799,7 +799,7 @@ by auto also have "\ = (\j\J. prob (A j))" unfolding if_distrib setprod.If_cases[OF `finite I`] - using prob_space `J \ I` by (simp add: Int_absorb1 setprod_1) + using prob_space `J \ I` by (simp add: Int_absorb1 setprod.neutral_const) finally show "prob (\j\J. A j) = (\j\J. prob (A j))" .. qed qed @@ -1225,7 +1225,7 @@ by (rule indep_vars_cong[THEN iffD1, OF _ _ _ I(2)]) (auto simp: Y_def) have "(\\<^sup>+\. (\i\I. X i \) \M) = (\\<^sup>+\. (\i\I. max 0 (Y i \)) \M)" - using I(3) by (auto intro!: nn_integral_cong setprod_cong simp add: Y_def max_def) + using I(3) by (auto intro!: nn_integral_cong setprod.cong simp add: Y_def max_def) also have "\ = (\\<^sup>+\. (\i\I. max 0 (\ i)) \distr M (Pi\<^sub>M I (\i. borel)) (\x. \i\I. Y i x))" by (subst nn_integral_distr) auto also have "\ = (\\<^sup>+\. (\i\I. max 0 (\ i)) \Pi\<^sub>M I (\i. distr M borel (Y i)))" @@ -1233,7 +1233,7 @@ also have "\ = (\i\I. (\\<^sup>+\. max 0 \ \distr M borel (Y i)))" by (rule product_nn_integral_setprod) (auto intro: `finite I`) also have "\ = (\i\I. \\<^sup>+\. X i \ \M)" - by (intro setprod_cong nn_integral_cong) + by (intro setprod.cong nn_integral_cong) (auto simp: nn_integral_distr nn_integral_max_0 Y_def rv_X) finally show ?thesis . qed (simp add: emeasure_space_1) @@ -1275,7 +1275,7 @@ also have "\ = (\i\I. (\\. \ \distr M borel (Y i)))" by (rule product_integral_setprod) (auto intro: `finite I` simp: integrable_distr_eq int_Y) also have "\ = (\i\I. \\. X i \ \M)" - by (intro setprod_cong integral_cong) + by (intro setprod.cong integral_cong) (auto simp: integral_distr Y_def rv_X) finally show ?eq . diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Infinite_Product_Measure.thy --- a/src/HOL/Probability/Infinite_Product_Measure.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Sat Jun 28 09:16:42 2014 +0200 @@ -322,12 +322,12 @@ using J `I \ {}` by (subst mu_G_spec[OF _ _ _ refl]) (auto simp: emeasure_PiM Pi_iff) also have "\ = (\j\J \ {i \ I. emeasure (M i) (space (M i)) \ 1}. if j \ J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))" - using J `I \ {}` by (intro setprod_mono_one_right) (auto simp: M.emeasure_space_1) + using J `I \ {}` by (intro setprod.mono_neutral_right) (auto simp: M.emeasure_space_1) finally show "\ (emb I J (Pi\<^sub>E J X)) = \" . next let ?F = "\j. if j \ J then emeasure (M j) (X j) else emeasure (M j) (space (M j))" have "(\j\J \ {i \ I. emeasure (M i) (space (M i)) \ 1}. ?F j) = (\j\J. ?F j)" - using X `I \ {}` by (intro setprod_mono_one_right) (auto simp: M.emeasure_space_1) + using X `I \ {}` by (intro setprod.mono_neutral_right) (auto simp: M.emeasure_space_1) then show "(\j\J \ {i \ I. emeasure (M i) (space (M i)) \ 1}. ?F j) = emeasure (Pi\<^sub>M J M) (Pi\<^sub>E J X)" using X by (auto simp add: emeasure_PiM) @@ -560,12 +560,12 @@ also have "emeasure S ?F = (\j\(op + i) -` J. emeasure M (E (i + j)))" using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI inj_on_def) also have "\ = (\j\J - (J \ {..x. x - i"]) (auto simp: image_iff Bex_def not_less nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI) also have "emeasure S ?E = (\j\J \ {..j\J \ {..j\J - (J \ {..j\J. emeasure M (E j))" - by (subst mult_commute) (auto simp: J setprod_subset_diff[symmetric]) + by (subst mult_commute) (auto simp: J setprod.subset_diff[symmetric]) finally show "emeasure ?D ?X = (\j\J. emeasure M (E j))" . qed simp_all @@ -591,7 +591,7 @@ also have "emeasure S ?F = (\j\Suc -` J. emeasure M (E (Suc j)))" using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI) also have "\ = (\j\J - {0}. emeasure M (E j))" - by (rule strong_setprod_reindex_cong[where f="\x. x - 1"]) + by (rule setprod.reindex_cong [of "\x. x - 1"]) (auto simp: image_iff Bex_def not_less nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI) also have "emeasure M ?E * (\j\J - {0}. emeasure M (E j)) = (\j\J. emeasure M (E j))" by (auto simp: M.emeasure_space_1 setprod.remove J) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Information.thy --- a/src/HOL/Probability/Information.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Probability/Information.thy Sat Jun 28 09:16:42 2014 +0200 @@ -19,7 +19,7 @@ lemma setsum_cartesian_product': "(\x\A \ B. f x) = (\x\A. setsum (\y. f (x, y)) B)" - unfolding setsum_cartesian_product by simp + unfolding setsum.cartesian_product by simp lemma split_pairs: "((A, B) = X) \ (fst X = A \ snd X = B)" and @@ -735,8 +735,8 @@ by auto with fin show "(\ x. ?f x \(count_space (X ` space M) \\<^sub>M count_space (Y ` space M))) = (\(x, y)\(\x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y)))" - by (auto simp add: pair_measure_count_space lebesgue_integral_count_space_finite setsum_cases split_beta' - intro!: setsum_cong) + by (auto simp add: pair_measure_count_space lebesgue_integral_count_space_finite setsum.If_cases split_beta' + intro!: setsum.cong) qed lemma (in information_space) @@ -748,7 +748,7 @@ proof (subst mutual_information_simple_distributed[OF Px Py Pxy]) have "(\(x, y)\(\x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) = (\(x, y)\(\x. (X x, Y x)) ` space M. 0)" - by (intro setsum_cong) (auto simp: ae) + by (intro setsum.cong) (auto simp: ae) then show "(\(x, y)\(\x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) = 0" by simp qed @@ -1488,7 +1488,7 @@ have "(\(x, y, z). ?i x y z) = (\x. if x \ (\x. (X x, Y x, Z x)) ` space M then ?j (fst x) (fst (snd x)) (snd (snd x)) else 0)" by (auto intro!: ext) then show "(\ (x, y, z). ?i x y z \?P) = (\(x, y, z)\(\x. (X x, Y x, Z x)) ` space M. ?j x y z)" - by (auto intro!: setsum_cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite setsum_cases split_beta') + by (auto intro!: setsum.cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite setsum.If_cases split_beta') qed lemma (in information_space) conditional_mutual_information_nonneg: @@ -1640,7 +1640,7 @@ by auto from Y show "- (\ (x, y). ?f (x, y) * log b (?f (x, y) / Py y) \?P) = - (\(x, y)\(\x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / Py y))" - by (auto intro!: setsum_cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite eq setsum_cases split_beta') + by (auto intro!: setsum.cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite eq setsum.If_cases split_beta') qed lemma (in information_space) conditional_mutual_information_eq_conditional_entropy: @@ -1671,7 +1671,7 @@ then show ?thesis apply (subst conditional_mutual_information_eq[OF Py Pxy Pxy Pxxy]) apply (subst conditional_entropy_eq[OF Py Pxy]) - apply (auto intro!: setsum_cong simp: Pxxy_eq setsum_negf[symmetric] eq setsum_reindex[OF inj] + apply (auto intro!: setsum.cong simp: Pxxy_eq setsum_negf[symmetric] eq setsum.reindex[OF inj] log_simps zero_less_mult_iff zero_le_mult_iff field_simps mult_less_0_iff AE_count_space) using Py[THEN simple_distributed, THEN distributed_real_AE] Pxy[THEN simple_distributed, THEN distributed_real_AE] apply (auto simp add: not_le[symmetric] AE_count_space) @@ -1857,13 +1857,13 @@ have "\(\x. (X x, Y x)) = - (\x\(\x. (X x, Y x)) ` space M. ?f x * log b (?f x))" using XY by (rule entropy_simple_distributed) also have "\ = - (\x\(\(x, y). (y, x)) ` (\x. (X x, Y x)) ` space M. ?g x * log b (?g x))" - by (subst (2) setsum_reindex) (auto simp: inj_on_def intro!: setsum_cong arg_cong[where f="\A. prob A * log b (prob A)"]) + by (subst (2) setsum.reindex) (auto simp: inj_on_def intro!: setsum.cong arg_cong[where f="\A. prob A * log b (prob A)"]) also have "\ = - (\x\(\x. (Y x, X x)) ` space M. ?h x * log b (?h x))" - by (auto intro!: setsum_cong) + by (auto intro!: setsum.cong) also have "\ = entropy b (count_space (Y ` space M) \\<^sub>M count_space (X ` space M)) (\x. (Y x, X x))" by (subst entropy_distr[OF simple_distributed_joint[OF YX]]) (auto simp: pair_measure_count_space sigma_finite_measure_count_space_finite lebesgue_integral_count_space_finite - cong del: setsum_cong intro!: setsum_mono_zero_left) + cong del: setsum.cong intro!: setsum.mono_neutral_left) finally have "\(\x. (X x, Y x)) = entropy b (count_space (Y ` space M) \\<^sub>M count_space (X ` space M)) (\x. (Y x, X x))" . then show ?thesis unfolding conditional_entropy_eq_entropy_simple[OF Y X] by simp @@ -1882,8 +1882,8 @@ apply (subst entropy_simple_distributed[OF simple_distributedI[OF simple_function_Pair[OF fX X] refl]]) apply (subst entropy_simple_distributed[OF simple_distributedI[OF X refl]]) unfolding eq - apply (subst setsum_reindex[OF inj]) - apply (auto intro!: setsum_cong arg_cong[where f="\A. prob A * log b (prob A)"]) + apply (subst setsum.reindex[OF inj]) + apply (auto intro!: setsum.cong arg_cong[where f="\A. prob A * log b (prob A)"]) done qed @@ -1908,7 +1908,7 @@ unfolding o_assoc apply (subst entropy_simple_distributed[OF simple_distributedI[OF X refl]]) apply (subst entropy_simple_distributed[OF simple_distributedI[OF simple_function_compose[OF X]], where f="\x. prob (X -` {x} \ space M)"]) - apply (auto intro!: setsum_cong arg_cong[where f=prob] image_eqI simp: the_inv_into_f_f[OF inj] comp_def) + apply (auto intro!: setsum.cong arg_cong[where f=prob] image_eqI simp: the_inv_into_f_f[OF inj] comp_def) done also have "... \ \(f \ X)" using entropy_data_processing[OF sf] . diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Measure_Space.thy --- a/src/HOL/Probability/Measure_Space.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Probability/Measure_Space.thy Sat Jun 28 09:16:42 2014 +0200 @@ -51,7 +51,7 @@ have **: "\n. f n * indicator (A n) x = (if n = i then f n else 0 :: ereal)" using `x \ A i` assms unfolding disjoint_family_on_def indicator_def by auto then have "\n. (\jn. n \ UNIV \ (if i < n then f i else 0) \ y" @@ -287,7 +287,7 @@ from fin_not_0 have "(\i. \ (F i)) = (\i | \ (F i) \ 0. \ (F i))" by (rule suminf_finite) auto also have "\ = (\i | F i \ {}. \ (F i))" - using fin_not_empty F_subset by (rule setsum_mono_zero_left) auto + using fin_not_empty F_subset by (rule setsum.mono_neutral_left) auto also have "\ = \ (\i\{i. F i \ {}}. F i)" using `positive M \` `additive M \` fin_not_empty disj_not_empty F by (intro additive_sum) auto also have "\ = \ (\i. F i)" @@ -668,7 +668,7 @@ then have "emeasure M X = (\a\X. emeasure M {a})" using `finite A` by (subst emeasure_eq_setsum_singleton) (auto dest: finite_subset) also have "\ = (\a\X. emeasure N {a})" - using X eq by (auto intro!: setsum_cong) + using X eq by (auto intro!: setsum.cong) also have "\ = emeasure N X" using X `finite A` by (subst emeasure_eq_setsum_singleton) (auto dest: finite_subset) finally show "emeasure M X = emeasure N X" . diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Sat Jun 28 09:16:42 2014 +0200 @@ -72,9 +72,9 @@ proof - have "?r = (\y \ f ` space M. (if y = f x then y * indicator (f -` {y} \ space M) x else 0))" - by (auto intro!: setsum_cong2) + by (auto intro!: setsum.cong) also have "... = f x * indicator (f -` {f x} \ space M) x" - using assms by (auto dest: simple_functionD simp: setsum_delta) + using assms by (auto dest: simple_functionD simp: setsum.delta) also have "... = f x" using x by (auto simp: indicator_def) finally show ?thesis by auto qed @@ -552,7 +552,7 @@ (\y\f`space M. y * (\z\g`space M. if \x\space M. y = f x \ z = g x then emeasure M {x\space M. g x = z} else 0))" unfolding simple_integral_def - proof (safe intro!: setsum_cong ereal_left_mult_cong) + proof (safe intro!: setsum.cong ereal_left_mult_cong) fix y assume y: "y \ space M" "f y \ 0" have [simp]: "g ` space M \ {z. \x\space M. f y = f x \ z = g x} = {z. \x\space M. f y = f x \ z = g x}" @@ -565,17 +565,17 @@ by (rule rev_finite_subset) auto then show "emeasure M (f -` {f y} \ space M) = (\z\g ` space M. if \x\space M. f y = f x \ z = g x then emeasure M {x \ space M. g x = z} else 0)" - apply (simp add: setsum_cases) + apply (simp add: setsum.If_cases) apply (subst setsum_emeasure) apply (auto simp: disjoint_family_on_def eq) done qed also have "\ = (\y\f`space M. (\z\g`space M. if \x\space M. y = f x \ z = g x then y * emeasure M {x\space M. g x = z} else 0))" - by (auto intro!: setsum_cong simp: setsum_ereal_right_distrib emeasure_nonneg) + by (auto intro!: setsum.cong simp: setsum_ereal_right_distrib emeasure_nonneg) also have "\ = ?r" - by (subst setsum_commute) - (auto intro!: setsum_cong simp: setsum_cases scaleR_setsum_right[symmetric] eq) + by (subst setsum.commute) + (auto intro!: setsum.cong simp: setsum.If_cases scaleR_setsum_right[symmetric] eq) finally show "integral\<^sup>S M f = ?r" . qed @@ -588,7 +588,7 @@ by (intro simple_function_partition) (auto intro: f g) also have "\ = (\y\(\x. (f x, g x))`space M. fst y * emeasure M {x\space M. (f x, g x) = y}) + (\y\(\x. (f x, g x))`space M. snd y * emeasure M {x\space M. (f x, g x) = y})" - using assms(2,4) by (auto intro!: setsum_cong ereal_left_distrib simp: setsum_addf[symmetric]) + using assms(2,4) by (auto intro!: setsum.cong ereal_left_distrib simp: setsum.distrib[symmetric]) also have "(\y\(\x. (f x, g x))`space M. fst y * emeasure M {x\space M. (f x, g x) = y}) = (\\<^sup>Sx. f x \M)" by (intro simple_function_partition[symmetric]) (auto intro: f g) also have "(\y\(\x. (f x, g x))`space M. snd y * emeasure M {x\space M. (f x, g x) = y}) = (\\<^sup>Sx. g x \M)" @@ -686,14 +686,14 @@ using assms by (intro simple_function_partition) auto also have "\ = (\y\(\x. (f x, indicator A x::ereal))`space M. if snd y = 1 then fst y * emeasure M (f -` {fst y} \ space M \ A) else 0)" - by (auto simp: indicator_def split: split_if_asm intro!: arg_cong2[where f="op *"] arg_cong2[where f=emeasure] setsum_cong) + by (auto simp: indicator_def split: split_if_asm intro!: arg_cong2[where f="op *"] arg_cong2[where f=emeasure] setsum.cong) also have "\ = (\y\(\x. (f x, 1::ereal))`A. fst y * emeasure M (f -` {fst y} \ space M \ A))" - using assms by (subst setsum_cases) (auto intro!: simple_functionD(1) simp: eq) + using assms by (subst setsum.If_cases) (auto intro!: simple_functionD(1) simp: eq) also have "\ = (\y\fst`(\x. (f x, 1::ereal))`A. y * emeasure M (f -` {y} \ space M \ A))" - by (subst setsum_reindex[where f=fst]) (auto simp: inj_on_def) + by (subst setsum.reindex [of fst]) (auto simp: inj_on_def) also have "\ = (\x \ f ` space M. x * emeasure M (f -` {x} \ space M \ A))" using A[THEN sets.sets_into_space] - by (intro setsum_mono_zero_cong_left simple_functionD f) (auto simp: image_comp comp_def eq2) + by (intro setsum.mono_neutral_cong_left simple_functionD f) (auto simp: image_comp comp_def eq2) finally show ?thesis . qed @@ -929,7 +929,7 @@ next show "integral\<^sup>S M u = (\i\u ` space M. SUP n. i * (emeasure M) (?B' i n))" using measure_conv u_range B_u unfolding simple_integral_def - by (auto intro!: setsum_cong SUP_ereal_cmult [symmetric]) + by (auto intro!: setsum.cong SUP_ereal_cmult [symmetric]) qed moreover have "a * (SUP i. integral\<^sup>S M (?uB i)) \ ?S" @@ -1615,19 +1615,19 @@ have *: "(\\<^sup>+x. max 0 (f x) \count_space A) = (\\<^sup>+ x. (\a|a\A \ 0 < f a. f a * indicator {a} x) \count_space A)" by (auto intro!: nn_integral_cong - simp add: indicator_def if_distrib setsum_cases[OF A] max_def le_less) + simp add: indicator_def if_distrib setsum.If_cases[OF A] max_def le_less) also have "\ = (\a|a\A \ 0 < f a. \\<^sup>+ x. f a * indicator {a} x \count_space A)" by (subst nn_integral_setsum) (simp_all add: AE_count_space ereal_zero_le_0_iff less_imp_le) also have "\ = (\a|a\A \ 0 < f a. f a)" - by (auto intro!: setsum_cong simp: nn_integral_cmult_indicator one_ereal_def[symmetric]) + by (auto intro!: setsum.cong simp: nn_integral_cmult_indicator one_ereal_def[symmetric]) finally show ?thesis by (simp add: nn_integral_max_0) qed lemma nn_integral_count_space_finite: "finite A \ (\\<^sup>+x. f x \count_space A) = (\a\A. max 0 (f a))" by (subst nn_integral_max_0[symmetric]) - (auto intro!: setsum_mono_zero_left simp: nn_integral_count_space less_le) + (auto intro!: setsum.mono_neutral_left simp: nn_integral_count_space less_le) lemma emeasure_UN_countable: assumes sets: "\i. i \ I \ X i \ sets M" and I: "countable I" @@ -1636,7 +1636,7 @@ proof cases assume "finite I" with sets disj show ?thesis by (subst setsum_emeasure[symmetric]) - (auto intro!: setsum_cong simp add: max_def subset_eq nn_integral_count_space_finite emeasure_nonneg) + (auto intro!: setsum.cong simp add: max_def subset_eq nn_integral_count_space_finite emeasure_nonneg) next assume f: "\ finite I" then have [intro]: "I \ {}" by auto @@ -1786,7 +1786,7 @@ using simple_function_restrict_space_ereal[THEN iffD1, OF \, THEN simple_functionD(1)] by (auto simp add: space_restrict_space emeasure_restrict_space[OF \(1)] le_infI2 simple_integral_def split: split_indicator split_indicator_asm - intro!: setsum_mono_zero_cong_left ereal_left_mult_cong arg_cong2[where f=emeasure]) + intro!: setsum.mono_neutral_cong_left ereal_left_mult_cong arg_cong2[where f=emeasure]) lemma one_not_less_zero[simp]: "\ 1 < (0::ereal)" by (simp add: zero_ereal_def one_ereal_def) @@ -2097,12 +2097,12 @@ lemma emeasure_point_measure_finite: "finite A \ (\i. i \ A \ 0 \ f i) \ X \ A \ emeasure (point_measure A f) X = (\a\X. f a)" - by (subst emeasure_point_measure) (auto dest: finite_subset intro!: setsum_mono_zero_left simp: less_le) + by (subst emeasure_point_measure) (auto dest: finite_subset intro!: setsum.mono_neutral_left simp: less_le) lemma emeasure_point_measure_finite2: "X \ A \ finite X \ (\i. i \ X \ 0 \ f i) \ emeasure (point_measure A f) X = (\a\X. f a)" by (subst emeasure_point_measure) - (auto dest: finite_subset intro!: setsum_mono_zero_left simp: less_le) + (auto dest: finite_subset intro!: setsum.mono_neutral_left simp: less_le) lemma null_sets_point_measure_iff: "X \ null_sets (point_measure A f) \ X \ A \ (\x\X. f x \ 0)" @@ -2121,7 +2121,7 @@ apply (subst nn_integral_density) apply (simp_all add: AE_count_space nn_integral_density) apply (subst nn_integral_count_space ) - apply (auto intro!: setsum_cong simp: max_def ereal_zero_less_0_iff) + apply (auto intro!: setsum.cong simp: max_def ereal_zero_less_0_iff) apply (rule finite_subset) prefer 2 apply assumption @@ -2131,7 +2131,7 @@ lemma nn_integral_point_measure_finite: "finite A \ (\a. a \ A \ 0 \ f a) \ (\a. a \ A \ 0 \ g a) \ integral\<^sup>N (point_measure A f) g = (\a\A. f a * g a)" - by (subst nn_integral_point_measure) (auto intro!: setsum_mono_zero_left simp: less_le) + by (subst nn_integral_point_measure) (auto intro!: setsum.mono_neutral_left simp: less_le) subsubsection {* Uniform measure *} diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Probability/Probability_Measure.thy Sat Jun 28 09:16:42 2014 +0200 @@ -364,7 +364,7 @@ sublocale finite_product_prob_space \ prob_space "\\<^sub>M i\I. M i" proof show "emeasure (\\<^sub>M i\I. M i) (space (\\<^sub>M i\I. M i)) = 1" - by (simp add: measure_times M.emeasure_space_1 setprod_1 space_PiM) + by (simp add: measure_times M.emeasure_space_1 setprod.neutral_const space_PiM) qed lemma (in finite_product_prob_space) prob_times: @@ -915,7 +915,7 @@ from X have "setsum f (X`space M) = prob (\i\X`space M. X -` {i} \ space M)" by (subst finite_measure_finite_Union) (auto simp add: disjoint_family_on_def simple_distributed_measure simple_distributed_simple_function simple_functionD - intro!: setsum_cong arg_cong[where f="prob"]) + intro!: setsum.cong arg_cong[where f="prob"]) also have "\ = prob (space M)" by (auto intro!: arg_cong[where f=prob]) finally show ?thesis @@ -943,7 +943,7 @@ Pxy[THEN simple_distributed, THEN distributed_real_AE] show ?thesis unfolding AE_count_space - apply (auto simp add: nn_integral_count_space_finite * intro!: setsum_cong split: split_max) + apply (auto simp add: nn_integral_count_space_finite * intro!: setsum.cong split: split_max) done qed diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Projective_Family.thy --- a/src/HOL/Probability/Projective_Family.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Probability/Projective_Family.thy Sat Jun 28 09:16:42 2014 +0200 @@ -40,7 +40,7 @@ by simp also have "\ = (\ i\K. emeasure (M i) (if i \ J then E i else space (M i)))" using `finite K` `J \ K` - by (intro setprod_mono_one_left) (auto simp: M.emeasure_space_1) + by (intro setprod.mono_neutral_left) (auto simp: M.emeasure_space_1) also have "\ = emeasure (Pi\<^sub>M K M) (\\<^sub>E i\K. if i \ J then E i else space (M i))" using E by (simp add: K.measure_times) also have "(\\<^sub>E i\K. if i \ J then E i else space (M i)) = (\f. restrict f J) -` Pi\<^sub>E J E \ (\\<^sub>E i\K. space (M i))" diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/Projective_Limit.thy --- a/src/HOL/Probability/Projective_Limit.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Probability/Projective_Limit.thy Sat Jun 28 09:16:42 2014 +0200 @@ -353,7 +353,7 @@ also have "\ < ereal (1 * real ?a)" unfolding less_ereal.simps proof (rule mult_strict_right_mono) have "(\i\{1..n}. 2 powr - real i) = (\i\{1.. 'a set) \ nat \ 'a set " diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Sat Jun 28 09:16:42 2014 +0200 @@ -99,8 +99,8 @@ by force+ show ?case unfolding * using Suc[of "\i. P (Suc i)"] - by (simp add: setsum_reindex split_conv setsum_cartesian_product' - lessThan_Suc_eq_insert_0 setprod_reindex setsum_left_distrib[symmetric] setsum_right_distrib[symmetric]) + by (simp add: setsum.reindex split_conv setsum_cartesian_product' + lessThan_Suc_eq_insert_0 setprod.reindex setsum_left_distrib[symmetric] setsum_right_distrib[symmetric]) qed declare space_point_measure[simp] @@ -168,7 +168,7 @@ case (Suc n) then show ?case by (simp add: lists_length_Suc_eq lessThan_Suc_eq_insert_0 - setsum_reindex setprod_reindex) + setsum.reindex setprod.reindex) qed then show "setsum P msgs = 1" unfolding msgs_def P_def by simp @@ -255,7 +255,7 @@ apply (simp add: * P_def) apply (simp add: setsum_cartesian_product') using setprod_setsum_distrib_lists[OF M.finite_space, of M n "\x x. True"] `k \ keys` - by (auto simp add: setsum_right_distrib[symmetric] subset_eq setprod_1) + by (auto simp add: setsum_right_distrib[symmetric] subset_eq setprod.neutral_const) qed lemma fst_image_msgs[simp]: "fst`msgs = keys" @@ -297,8 +297,8 @@ show "- (\x\(\x. (X x, Y x)) ` msgs. (\

(X ; Y) {x}) * log b (\

(X ; Y) {x})) = - (\x\(\x. (Y x, X x)) ` msgs. (\

(Y ; X) {x}) * log b (\

(Y ; X) {x}))" unfolding eq - apply (subst setsum_reindex) - apply (auto simp: vimage_def inj_on_def intro!: setsum_cong arg_cong[where f="\x. prob x * log b (prob x)"]) + apply (subst setsum.reindex) + apply (auto simp: vimage_def inj_on_def intro!: setsum.cong arg_cong[where f="\x. prob x * log b (prob x)"]) done qed @@ -314,15 +314,15 @@ proof - have "- (\(x, y)\(\x. (X x, Y x)) ` msgs. (\

(X ; Y) {(x, y)}) * log b ((\

(X ; Y) {(x, y)}) / (\

(Y) {y}))) = - (\x\X`msgs. (\y\Y`msgs. (\

(X ; Y) {(x, y)}) * log b ((\

(X ; Y) {(x, y)}) / (\

(Y) {y}))))" - unfolding setsum_cartesian_product - apply (intro arg_cong[where f=uminus] setsum_mono_zero_left) + unfolding setsum.cartesian_product + apply (intro arg_cong[where f=uminus] setsum.mono_neutral_left) apply (auto simp: vimage_def image_iff intro!: measure_eq_0I) apply metis done also have "\ = - (\y\Y`msgs. (\x\X`msgs. (\

(X ; Y) {(x, y)}) * log b ((\

(X ; Y) {(x, y)}) / (\

(Y) {y}))))" - by (subst setsum_commute) rule + by (subst setsum.commute) rule also have "\ = -(\y\Y`msgs. (\

(Y) {y}) * (\x\X`msgs. (\

(X ; Y) {(x,y)}) / (\

(Y) {y}) * log b ((\

(X ; Y) {(x,y)}) / (\

(Y) {y}))))" - by (auto simp add: setsum_right_distrib vimage_def intro!: setsum_cong prob_conj_imp1) + by (auto simp add: setsum_right_distrib vimage_def intro!: setsum.cong prob_conj_imp1) finally show "- (\(x, y)\(\x. (X x, Y x)) ` msgs. (\

(X ; Y) {(x, y)}) * log b ((\

(X ; Y) {(x, y)}) / (\

(Y) {y}))) = -(\y\Y`msgs. (\

(Y) {y}) * (\x\X`msgs. (\

(X ; Y) {(x,y)}) / (\

(Y) {y}) * log b ((\

(X ; Y) {(x,y)}) / (\

(Y) {y}))))" . qed @@ -358,7 +358,7 @@ have "(\

(OB ; fst) {(obs, k)}) / K k = (\

(OB ; fst) {(obs', k)}) / K k" unfolding *[OF obs] *[OF obs'] - using t_f(1) obs_t_f by (subst (2) t_f(2)) (simp add: setprod_reindex) + using t_f(1) obs_t_f by (subst (2) t_f(2)) (simp add: setprod.reindex) then have "(\

(OB ; fst) {(obs, k)}) = (\

(OB ; fst) {(obs', k)})" using `K k \ 0` by auto } note t_eq_imp = this @@ -396,17 +396,17 @@ using finite_measure_mono[of "{x. t (OB x) = t obs \ fst x = k} \ msgs" "{x. fst x = k} \ msgs"] using measure_nonneg[of \ "{x. fst x = k \ t (OB x) = t obs} \ msgs"] apply (simp add: setsum_distribution_cut[of "t\OB" "t obs" fst]) - apply (auto intro!: setsum_cong simp: subset_eq vimage_def prob_conj_imp1) + apply (auto intro!: setsum.cong simp: subset_eq vimage_def prob_conj_imp1) done also have "\

(t\OB | fst) {(t obs, k)} * \

(fst) {k} / (\k'\keys. \

(t\OB|fst) {(t obs, k')} * \

(fst) {k'}) = \

(OB | fst) {(obs, k)} * \

(fst) {k} / (\k'\keys. \

(OB|fst) {(obs, k')} * \

(fst) {k'})" using CP_t_K[OF `k\keys` obs] CP_t_K[OF _ obs] `real (card ?S) \ 0` by (simp only: setsum_right_distrib[symmetric] ac_simps mult_divide_mult_cancel_left[OF `real (card ?S) \ 0`] - cong: setsum_cong) + cong: setsum.cong) also have "(\k'\keys. \

(OB|fst) {(obs, k')} * \

(fst) {k'}) = \

(OB) {obs}" using setsum_distribution_cut[of OB obs fst] - by (auto intro!: setsum_cong simp: prob_conj_imp1 vimage_def) + by (auto intro!: setsum.cong simp: prob_conj_imp1 vimage_def) also have "\

(OB | fst) {(obs, k)} * \

(fst) {k} / \

(OB) {obs} = \

(fst | OB) {(k, obs)}" by (auto simp: vimage_def conj_commute prob_conj_imp2) finally have "\

(fst | t\OB) {(k, t obs)} = \

(fst | OB) {(k, obs)}" . } @@ -440,13 +440,13 @@ unfolding conditional_entropy_eq_ce_with_hypothesis using * by simp also have "\ = -(\obs\t`OB`msgs. \

(t\OB) {obs} * ?Ht obs)" apply (subst SIGMA_image_vimage[symmetric, of "OB`msgs" t]) - apply (subst setsum_reindex) + apply (subst setsum.reindex) apply (fastforce intro!: inj_onI) apply simp - apply (subst setsum_Sigma[symmetric, unfolded split_def]) + apply (subst setsum.Sigma[symmetric, unfolded split_def]) using finite_space apply fastforce using finite_space apply fastforce - apply (safe intro!: setsum_cong) + apply (safe intro!: setsum.cong) using P_t_sum_P_O by (simp add: setsum_divide_distrib[symmetric] field_simps ** setsum_right_distrib[symmetric] setsum_left_distrib[symmetric]) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Sat Jun 28 09:16:42 2014 +0200 @@ -450,7 +450,7 @@ by (induct s rule: finite_induct) auto next case False then show ?thesis using assms - by (metis Reals_0 setsum_infinite) + by (metis Reals_0 setsum.infinite) qed lemma setprod_in_Reals: assumes "\i. i \ s \ f i \ \" shows "setprod f s \ \" @@ -459,7 +459,7 @@ by (induct s rule: finite_induct) auto next case False then show ?thesis using assms - by (metis Reals_1 setprod_infinite) + by (metis Reals_1 setprod.infinite) qed lemma Reals_induct [case_names of_real, induct set: Reals]: diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Series.thy --- a/src/HOL/Series.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Series.thy Sat Jun 28 09:16:42 2014 +0200 @@ -75,7 +75,7 @@ next assume [simp]: "N \ {}" show ?thesis - proof (safe intro!: setsum_mono_zero_right f) + proof (safe intro!: setsum.mono_neutral_right f) fix i assume "i \ N" then have "i \ Max N" by simp then show "i < n + Suc (Max N)" by simp @@ -225,7 +225,7 @@ have "f sums (s + f 0) \ (\i. \j s + f 0" by (subst LIMSEQ_Suc_iff) (simp add: sums_def) also have "\ \ (\i. (\j s + f 0" - by (simp add: ac_simps setsum_reindex image_iff lessThan_Suc_eq_insert_0) + by (simp add: ac_simps setsum.reindex image_iff lessThan_Suc_eq_insert_0) also have "\ \ (\n. f (Suc n)) sums s" proof assume "(\i. (\j s + f 0" @@ -241,7 +241,7 @@ begin lemma sums_add: "f sums a \ g sums b \ (\n. f n + g n) sums (a + b)" - unfolding sums_def by (simp add: setsum_addf tendsto_add) + unfolding sums_def by (simp add: setsum.distrib tendsto_add) lemma summable_add: "summable f \ summable g \ summable (\n. f n + g n)" unfolding summable_def by (auto intro: sums_add) @@ -568,7 +568,7 @@ lemma setsum_triangle_reindex: fixes n :: nat shows "(\(i,j)\{(i,j). i+j < n}. f i j) = (\ki\k. f i (k - i))" - apply (simp add: setsum_Sigma) + apply (simp add: setsum.Sigma) apply (rule setsum.reindex_bij_witness[where j="\(i, j). (i+j, i)" and i="\(k, i). (i, k - i)"]) apply auto done @@ -597,12 +597,12 @@ have "(\n. (\kk (\k. a k) * (\k. b k)" by (intro tendsto_mult summable_LIMSEQ summable_norm_cancel [OF a] summable_norm_cancel [OF b]) hence 1: "(\n. setsum ?g (?S1 n)) ----> (\k. a k) * (\k. b k)" - by (simp only: setsum_product setsum_Sigma [rule_format] finite_lessThan) + by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan) have "(\n. (\kk (\k. norm (a k)) * (\k. norm (b k))" using a b by (intro tendsto_mult summable_LIMSEQ) hence "(\n. setsum ?f (?S1 n)) ----> (\k. norm (a k)) * (\k. norm (b k))" - by (simp only: setsum_product setsum_Sigma [rule_format] finite_lessThan) + by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan) hence "convergent (\n. setsum ?f (?S1 n))" by (rule convergentI) hence Cauchy: "Cauchy (\n. setsum ?f (?S1 n))" diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Set_Interval.thy Sat Jun 28 09:16:42 2014 +0200 @@ -1378,14 +1378,14 @@ special form for @{term"{..a = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \ setsum f {a.. {n+1..n+p}" using `m \ n+1` by auto - thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint + thus ?thesis by (auto simp: ivl_disj_int setsum.union_disjoint atLeastSucAtMost_greaterThanAtMost) qed lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \ setsum f {m.. 'a::ab_group_add" @@ -1459,70 +1459,6 @@ (if m <= n then f m - f(n + 1) else 0)" by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) -lemma setsum_restrict_set': - "finite A \ setsum f {x \ A. x \ B} = (\x\A. if x \ B then f x else 0)" - by (simp add: setsum_restrict_set [symmetric] Int_def) - -lemma setsum_restrict_set'': - "finite A \ setsum f {x \ A. P x} = (\x\A. if P x then f x else 0)" - by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq]) - -lemma setsum_setsum_restrict: - "finite S \ finite T \ - setsum (\x. setsum (\y. f x y) {y. y \ T \ R x y}) S = setsum (\y. setsum (\x. f x y) {x. x \ S \ R x y}) T" - by (simp add: setsum_restrict_set'') (rule setsum_commute) - -lemma setsum_image_gen: assumes fS: "finite S" - shows "setsum g S = setsum (\y. setsum g {x. x \ S \ f x = y}) (f ` S)" -proof- - { fix x assume "x \ S" then have "{y. y\ f`S \ f x = y} = {f x}" by auto } - hence "setsum g S = setsum (\x. setsum (\y. g x) {y. y\ f`S \ f x = y}) S" - by simp - also have "\ = setsum (\y. setsum g {x. x \ S \ f x = y}) (f ` S)" - by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]]) - finally show ?thesis . -qed - -lemma setsum_le_included: - fixes f :: "'a \ 'b::ordered_comm_monoid_add" - assumes "finite s" "finite t" - and "\y\t. 0 \ g y" "(\x\s. \y\t. i y = x \ f x \ g y)" - shows "setsum f s \ setsum g t" -proof - - have "setsum f s \ setsum (\y. setsum g {x. x\t \ i x = y}) s" - proof (rule setsum_mono) - fix y assume "y \ s" - with assms obtain z where z: "z \ t" "y = i z" "f y \ g z" by auto - with assms show "f y \ setsum g {x \ t. i x = y}" (is "?A y \ ?B y") - using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro] - by (auto intro!: setsum_mono2) - qed - also have "... \ setsum (\y. setsum g {x. x\t \ i x = y}) (i ` t)" - using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg) - also have "... \ setsum g t" - using assms by (auto simp: setsum_image_gen[symmetric]) - finally show ?thesis . -qed - -lemma setsum_multicount_gen: - assumes "finite s" "finite t" "\j\t. (card {i\s. R i j} = k j)" - shows "setsum (\i. (card {j\t. R i j})) s = setsum k t" (is "?l = ?r") -proof- - have "?l = setsum (\i. setsum (\x.1) {j\t. R i j}) s" by auto - also have "\ = ?r" unfolding setsum_setsum_restrict[OF assms(1-2)] - using assms(3) by auto - finally show ?thesis . -qed - -lemma setsum_multicount: - assumes "finite S" "finite T" "\j\T. (card {i\S. R i j} = k)" - shows "setsum (\i. card {j\T. R i j}) S = k * card T" (is "?l = ?r") -proof- - have "?l = setsum (\i. k) T" by(rule setsum_multicount_gen)(auto simp:assms) - also have "\ = ?r" by(simp add: mult_commute) - finally show ?thesis by auto -qed - lemma setsum_nat_group: "(\mi = 0..n. (\j = 0..j = 0..i = Suc j..n. a i j)" - by (induction n) (auto simp: setsum_addf) + by (induction n) (auto simp: setsum.distrib) lemma nested_setsum_swap': "(\i\n. (\jji = Suc j..n. a i j)" - by (induction n) (auto simp: setsum_addf) + by (induction n) (auto simp: setsum.distrib) lemma setsum_zero_power [simp]: fixes c :: "nat \ 'a::division_ring" @@ -1642,7 +1578,7 @@ have "(\i\{..i\{..i\{.. = ?n*a + (\i\{.. = (?n*a + d*(\i\{1.. 'b::comm_semiring_1" - shows "setprod f A ^ n = setprod (\x. (f x)^n) A" -proof (cases "finite A") - case True then show ?thesis - by (induct A rule: finite_induct) (auto simp add: power_mult_distrib) -next - case False then show ?thesis - by (metis setprod_infinite power_one) -qed - end diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Transcendental.thy Sat Jun 28 09:16:42 2014 +0200 @@ -237,7 +237,7 @@ have "?s sums y" using sums_if'[OF `f sums y`] . from this[unfolded sums_def, THEN LIMSEQ_Suc] have "(\ n. if even n then f (n div 2) else 0) sums y" - by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum_reindex if_eq sums_def cong del: if_cong) + by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum.reindex if_eq sums_def cong del: if_cong) } from sums_add[OF g_sums this] show ?thesis unfolding if_sum . qed @@ -478,7 +478,7 @@ apply (subst sumr_diff_mult_const2) apply simp apply (simp only: lemma_termdiff1 setsum_right_distrib) - apply (rule setsum_cong [OF refl]) + apply (rule setsum.cong [OF refl]) apply (simp add: less_iff_Suc_add) apply (clarify) apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac @@ -1071,7 +1071,7 @@ also have "(\i\Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) + (\i\Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) = (\i\Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))" - by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric] + by (simp only: setsum.distrib [symmetric] scaleR_left_distrib [symmetric] real_of_nat_add [symmetric]) simp also have "\ = real (Suc n) *\<^sub>R (\i\Suc n. S x i * S y (Suc n-i))" by (simp only: scaleR_right.setsum) diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/UNITY/Comp/AllocBase.thy --- a/src/HOL/UNITY/Comp/AllocBase.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/UNITY/Comp/AllocBase.thy Sat Jun 28 09:16:42 2014 +0200 @@ -51,12 +51,12 @@ (** setsum **) -declare setsum_cong [cong] +declare setsum.cong [cong] lemma bag_of_sublist_lemma: "(\i\ A Int lessThan k. {#if ii\ A Int lessThan k. {#f i#})" -by (rule setsum_cong, auto) +by (rule setsum.cong, auto) lemma bag_of_sublist: "bag_of (sublist l A) = @@ -72,7 +72,7 @@ bag_of (sublist l A) + bag_of (sublist l B)" apply (subgoal_tac "A Int B Int {..i\I. bag_of (sublist l (A i)))" apply (simp del: UN_simps add: UN_simps [symmetric] add: bag_of_sublist) -apply (subst setsum_UN_disjoint, auto) +apply (subst setsum.UNION_disjoint, auto) done end diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/ex/HarmonicSeries.thy --- a/src/HOL/ex/HarmonicSeries.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/ex/HarmonicSeries.thy Sat Jun 28 09:16:42 2014 +0200 @@ -196,7 +196,7 @@ "finite {1..(2::nat)^M}" and "finite {(2::nat)^M+1..(2::nat)^(Suc M)}" by auto ultimately show ?thesis - by (auto intro: setsum_Un_disjoint) + by (auto intro: setsum.union_disjoint) qed moreover { diff -r 29fe9bac501b -r 6ab1c7cb0b8d src/HOL/ex/Transfer_Int_Nat.thy --- a/src/HOL/ex/Transfer_Int_Nat.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/ex/Transfer_Int_Nat.thy Sat Jun 28 09:16:42 2014 +0200 @@ -110,7 +110,8 @@ apply (intro rel_funI) apply (erule (1) bi_unique_rel_set_lemma) apply (simp add: setsum.reindex int_setsum ZN_def rel_fun_def) - apply (rule setsum_cong2, simp) + apply (rule setsum.cong) + apply simp_all done text {* For derived operations, we can use the @{text "transfer_prover"}