src/HOL/SetInterval.thy
 author nipkow Wed Jul 15 15:09:33 2009 +0200 (2009-07-15) changeset 32006 0e209ff7f236 parent 31998 2c7a24f74db9 child 32400 6c62363cf0d7 permissions -rw-r--r--
More finite set induction rules
 nipkow@8924  1 (* Title: HOL/SetInterval.thy  ballarin@13735  2  Author: Tobias Nipkow and Clemens Ballarin  paulson@14485  3  Additions by Jeremy Avigad in March 2004  paulson@8957  4  Copyright 2000 TU Muenchen  nipkow@8924  5 ballarin@13735  6 lessThan, greaterThan, atLeast, atMost and two-sided intervals  nipkow@8924  7 *)  nipkow@8924  8 wenzelm@14577  9 header {* Set intervals *}  wenzelm@14577  10 nipkow@15131  11 theory SetInterval  haftmann@25919  12 imports Int  nipkow@15131  13 begin  nipkow@8924  14 nipkow@24691  15 context ord  nipkow@24691  16 begin  nipkow@24691  17 definition  haftmann@25062  18  lessThan :: "'a => 'a set" ("(1{..<_})") where  haftmann@25062  19  "{.. 'a set" ("(1{.._})") where  haftmann@25062  23  "{..u} == {x. x \ u}"  nipkow@24691  24 nipkow@24691  25 definition  haftmann@25062  26  greaterThan :: "'a => 'a set" ("(1{_<..})") where  haftmann@25062  27  "{l<..} == {x. l 'a set" ("(1{_..})") where  haftmann@25062  31  "{l..} == {x. l\x}"  nipkow@24691  32 nipkow@24691  33 definition  haftmann@25062  34  greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where  haftmann@25062  35  "{l<.. 'a => 'a set" ("(1{_..<_})") where  haftmann@25062  39  "{l.. 'a => 'a set" ("(1{_<.._})") where  haftmann@25062  43  "{l<..u} == {l<..} Int {..u}"  nipkow@24691  44 nipkow@24691  45 definition  haftmann@25062  46  atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where  haftmann@25062  47  "{l..u} == {l..} Int {..u}"  nipkow@24691  48 nipkow@24691  49 end  nipkow@8924  50 ballarin@13735  51 nipkow@15048  52 text{* A note of warning when using @{term"{.. 'a => 'b set => 'b set" ("(3UN _<=_./ _)" 10)  nipkow@30384  58  "@UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" 10)  nipkow@30384  59  "@INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" 10)  nipkow@30384  60  "@INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" 10)  kleing@14418  61 nipkow@30372  62 syntax (xsymbols)  nipkow@30384  63  "@UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\ _\_./ _)" 10)  nipkow@30384  64  "@UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" 10)  nipkow@30384  65  "@INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\ _\_./ _)" 10)  nipkow@30384  66  "@INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" 10)  kleing@14418  67 nipkow@30372  68 syntax (latex output)  nipkow@30384  69  "@UNION_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10)  nipkow@30384  70  "@UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10)  nipkow@30384  71  "@INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10)  nipkow@30384  72  "@INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10)  kleing@14418  73 kleing@14418  74 translations  kleing@14418  75  "UN i<=n. A" == "UN i:{..n}. A"  nipkow@15045  76  "UN i atLeast y) = (y \ (x::'a::order))"  paulson@15418  124 by (blast intro: order_trans)  paulson@13850  125 paulson@13850  126 lemma atLeast_eq_iff [iff]:  paulson@15418  127  "(atLeast x = atLeast y) = (x = (y::'a::linorder))"  paulson@13850  128 by (blast intro: order_antisym order_trans)  paulson@13850  129 paulson@13850  130 lemma greaterThan_subset_iff [iff]:  paulson@15418  131  "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))"  paulson@15418  132 apply (auto simp add: greaterThan_def)  paulson@15418  133  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  134 done  paulson@13850  135 paulson@13850  136 lemma greaterThan_eq_iff [iff]:  paulson@15418  137  "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"  paulson@15418  138 apply (rule iffI)  paulson@15418  139  apply (erule equalityE)  haftmann@29709  140  apply simp_all  paulson@13850  141 done  paulson@13850  142 paulson@15418  143 lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))"  paulson@13850  144 by (blast intro: order_trans)  paulson@13850  145 paulson@15418  146 lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"  paulson@13850  147 by (blast intro: order_antisym order_trans)  paulson@13850  148 paulson@13850  149 lemma lessThan_subset_iff [iff]:  paulson@15418  150  "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))"  paulson@15418  151 apply (auto simp add: lessThan_def)  paulson@15418  152  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  153 done  paulson@13850  154 paulson@13850  155 lemma lessThan_eq_iff [iff]:  paulson@15418  156  "(lessThan x = lessThan y) = (x = (y::'a::linorder))"  paulson@15418  157 apply (rule iffI)  paulson@15418  158  apply (erule equalityE)  haftmann@29709  159  apply simp_all  ballarin@13735  160 done  ballarin@13735  161 ballarin@13735  162 paulson@13850  163 subsection {*Two-sided intervals*}  ballarin@13735  164 nipkow@24691  165 context ord  nipkow@24691  166 begin  nipkow@24691  167 paulson@24286  168 lemma greaterThanLessThan_iff [simp,noatp]:  haftmann@25062  169  "(i : {l<.. {m..n} = {}";  nipkow@24691  195 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)  nipkow@24691  196 haftmann@25062  197 lemma atLeastLessThan_empty[simp]: "n \ m ==> {m.. k ==> {k<..l} = {}"  nipkow@17719  201 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)  nipkow@17719  202 haftmann@29709  203 lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  321 by (auto simp add: atLeastAtMost_def)  nipkow@15554  322 nipkow@16733  323 subsubsection {* Image *}  nipkow@16733  324 nipkow@16733  325 lemma image_add_atLeastAtMost:  nipkow@16733  326  "(%n::nat. n+k)  {i..j} = {i+k..j+k}" (is "?A = ?B")  nipkow@16733  327 proof  nipkow@16733  328  show "?A \ ?B" by auto  nipkow@16733  329 next  nipkow@16733  330  show "?B \ ?A"  nipkow@16733  331  proof  nipkow@16733  332  fix n assume a: "n : ?B"  webertj@20217  333  hence "n - k : {i..j}" by auto  nipkow@16733  334  moreover have "n = (n - k) + k" using a by auto  nipkow@16733  335  ultimately show "n : ?A" by blast  nipkow@16733  336  qed  nipkow@16733  337 qed  nipkow@16733  338 nipkow@16733  339 lemma image_add_atLeastLessThan:  nipkow@16733  340  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  343 next  nipkow@16733  344  show "?B \ ?A"  nipkow@16733  345  proof  nipkow@16733  346  fix n assume a: "n : ?B"  webertj@20217  347  hence "n - k : {i.. finite N"  nipkow@28068  396 apply (rule finite_subset)  nipkow@28068  397  apply (rule_tac [2] finite_lessThan, auto)  nipkow@28068  398 done  nipkow@28068  399 nipkow@31044  400 text {* A set of natural numbers is finite iff it is bounded. *}  nipkow@31044  401 lemma finite_nat_set_iff_bounded:  nipkow@31044  402  "finite(N::nat set) = (EX m. ALL n:N. nnat. (!!n. n \ f n) ==> finite {n. f n \ u}"  nipkow@28068  418 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)  paulson@14485  419 nipkow@24853  420 text{* Any subset of an interval of natural numbers the size of the  nipkow@24853  421 subset is exactly that interval. *}  nipkow@24853  422 nipkow@24853  423 lemma subset_card_intvl_is_intvl:  nipkow@24853  424  "A <= {k.. A = {k.. \h. bij_betw h {0.. \h. bij_betw h M {0.. finite B \ card A = card B \ EX h. bij_betw h A B"  nipkow@31438  483 apply(drule ex_bij_betw_finite_nat)  nipkow@31438  484 apply(drule ex_bij_betw_nat_finite)  nipkow@31438  485 apply(auto intro!:bij_betw_trans)  nipkow@31438  486 done  nipkow@31438  487 nipkow@31438  488 lemma ex_bij_betw_nat_finite_1:  nipkow@31438  489  "finite M \ \h. bij_betw h {1 .. card M} M"  nipkow@31438  490 by (rule finite_same_card_bij) auto  nipkow@31438  491 nipkow@26105  492 paulson@14485  493 subsection {* Intervals of integers *}  paulson@14485  494 nipkow@15045  495 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l.. u ==>  nipkow@15045  508  {(0::int).. u")  paulson@14485  517  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  518  apply (rule finite_imageI)  paulson@14485  519  apply auto  paulson@14485  520  done  paulson@14485  521 nipkow@15045  522 lemma finite_atLeastLessThan_int [iff]: "finite {l.. u")  paulson@14485  544  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  545  apply (subst card_image)  paulson@14485  546  apply (auto simp add: inj_on_def)  paulson@14485  547  done  paulson@14485  548 nipkow@15045  549 lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}"  bulwahn@27656  571 proof -  bulwahn@27656  572  have "{k. P k \ k < i} \ {.. M"  bulwahn@27656  578 shows "card {k \ M. k < Suc i} \ 0"  bulwahn@27656  579 proof -  bulwahn@27656  580  from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto  bulwahn@27656  581  with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)  bulwahn@27656  582 qed  bulwahn@27656  583 bulwahn@27656  584 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"  huffman@30079  585 apply (rule card_bij_eq [of "Suc" _ _ "\x. x - Suc 0"])  bulwahn@27656  586 apply simp  bulwahn@27656  587 apply fastsimp  bulwahn@27656  588 apply auto  bulwahn@27656  589 apply (rule inj_on_diff_nat)  bulwahn@27656  590 apply auto  bulwahn@27656  591 apply (case_tac x)  bulwahn@27656  592 apply auto  bulwahn@27656  593 apply (case_tac xa)  bulwahn@27656  594 apply auto  bulwahn@27656  595 apply (case_tac xa)  bulwahn@27656  596 apply auto  bulwahn@27656  597 done  bulwahn@27656  598 bulwahn@27656  599 lemma card_less_Suc:  bulwahn@27656  600  assumes zero_in_M: "0 \ M"  bulwahn@27656  601  shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"  bulwahn@27656  602 proof -  bulwahn@27656  603  from assms have a: "0 \ {k \ M. k < Suc i}" by simp  bulwahn@27656  604  hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})"  bulwahn@27656  605  by (auto simp only: insert_Diff)  bulwahn@27656  606  have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto  bulwahn@27656  607  from finite_M_bounded_by_nat[of "\x. x \ M" "Suc i"] have "Suc (card {k. Suc k \ M \ k < i}) = card (insert 0 ({k \ M. k < Suc i} - {0}))"  bulwahn@27656  608  apply (subst card_insert)  bulwahn@27656  609  apply simp_all  bulwahn@27656  610  apply (subst b)  bulwahn@27656  611  apply (subst card_less_Suc2[symmetric])  bulwahn@27656  612  apply simp_all  bulwahn@27656  613  done  bulwahn@27656  614  with c show ?thesis by simp  bulwahn@27656  615 qed  bulwahn@27656  616 paulson@14485  617 paulson@13850  618 subsection {*Lemmas useful with the summation operator setsum*}  paulson@13850  619 ballarin@16102  620 text {* For examples, see Algebra/poly/UnivPoly2.thy *}  ballarin@13735  621 wenzelm@14577  622 subsubsection {* Disjoint Unions *}  ballarin@13735  623 wenzelm@14577  624 text {* Singletons and open intervals *}  ballarin@13735  625 ballarin@13735  626 lemma ivl_disj_un_singleton:  nipkow@15045  627  "{l::'a::linorder} Un {l<..} = {l..}"  nipkow@15045  628  "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  632  "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  641  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  643  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  645  "(l::'a::linorder) <= u ==> {l.. {l<.. {l<..m} Un {m<.. {l.. {l..m} Un {m<.. {l<.. {l<..m} Un {m<..u} = {l<..u}"  nipkow@15045  657  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  659 by auto  ballarin@13735  660 ballarin@13735  661 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two  ballarin@13735  662 wenzelm@14577  663 subsubsection {* Disjoint Intersections *}  ballarin@13735  664 wenzelm@14577  665 text {* Singletons and open intervals *}  ballarin@13735  666 ballarin@13735  667 lemma ivl_disj_int_singleton:  nipkow@15045  668  "{l::'a::order} Int {l<..} = {}"  nipkow@15045  669  "{.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  715 apply(auto simp:linorder_not_le)  nipkow@15542  716 apply(rule ccontr)  nipkow@15542  717 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  718 apply(clarsimp simp:linorder_not_le)  nipkow@15542  719 apply(fastsimp)  nipkow@15542  720 done  nipkow@15542  721 nipkow@15041  722 nipkow@15042  723 subsection {* Summation indexed over intervals *}  nipkow@15042  724 nipkow@15042  725 syntax  nipkow@15042  726  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  727  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  728  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@16052  729  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  nipkow@15042  730 syntax (xsymbols)  nipkow@15042  731  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  732  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  733  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  734  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15042  735 syntax (HTML output)  nipkow@15042  736  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  737  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  738  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  739  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15056  740 syntax (latex_sum output)  nipkow@15052  741  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  742  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@15052  743  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  744  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@16052  745  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  746  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15052  747  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  748  ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15041  749 nipkow@15048  750 translations  nipkow@28853  751  "\x=a..b. t" == "CONST setsum (%x. t) {a..b}"  nipkow@28853  752  "\x=a..i\n. t" == "CONST setsum (\i. t) {..n}"  nipkow@28853  754  "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  762 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  764 @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \  nipkow@15542  787  setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)"  nipkow@16052  794 by (simp add:atMost_Suc add_ac)  nipkow@16052  795 nipkow@16041  796 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n"  nipkow@16041  797 by (simp add:lessThan_Suc add_ac)  nipkow@15041  798 nipkow@15911  799 lemma setsum_cl_ivl_Suc[simp]:  nipkow@15561  800  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  nipkow@15561  801 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@15561  802 nipkow@15911  803 lemma setsum_op_ivl_Suc[simp]:  nipkow@15561  804  "setsum f {m..  nipkow@15561  808  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  nipkow@15561  809 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@16041  810 *)  nipkow@28068  811 nipkow@28068  812 lemma setsum_head:  nipkow@28068  813  fixes n :: nat  nipkow@28068  814  assumes mn: "m <= n"  nipkow@28068  815  shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  nipkow@28068  816 proof -  nipkow@28068  817  from mn  nipkow@28068  818  have "{m..n} = {m} \ {m<..n}"  nipkow@28068  819  by (auto intro: ivl_disj_un_singleton)  nipkow@28068  820  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  nipkow@28068  821  by (simp add: atLeast0LessThan)  nipkow@28068  822  also have "\ = ?rhs" by simp  nipkow@28068  823  finally show ?thesis .  nipkow@28068  824 qed  nipkow@28068  825 nipkow@28068  826 lemma setsum_head_Suc:  nipkow@28068  827  "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}"  nipkow@28068  828 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)  nipkow@28068  829 nipkow@28068  830 lemma setsum_head_upt_Suc:  nipkow@28068  831  "m < n \ setsum f {m.. n + 1"  nipkow@31501  837  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"  nipkow@31501  838 proof-  nipkow@31501  839  have "{m .. n+p} = {m..n} \ {n+1..n+p}" using m \ n+1 by auto  nipkow@31501  840  thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint  nipkow@31501  841  atLeastSucAtMost_greaterThanAtMost)  nipkow@31501  842 qed  nipkow@28068  843 nipkow@15539  844 lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \  nipkow@15539  845  setsum f {m.. 'a::ab_group_add"  nipkow@15539  850 shows "\ m \ n; n \ p \ \  nipkow@15539  851  setsum f {m.. ('a::ab_group_add)"  nipkow@31505  858  shows "setsum (\k. f k - f(k + 1)) {(m::nat) .. n} =  nipkow@31505  859  (if m <= n then f m - f(n + 1) else 0)"  nipkow@31505  860 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)  nipkow@31505  861 nipkow@31509  862 lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]  nipkow@31509  863 nipkow@31509  864 lemma setsum_setsum_restrict:  nipkow@31509  865  "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"  nipkow@31509  866  by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)  nipkow@31509  867  (rule setsum_commute)  nipkow@31509  868 nipkow@31509  869 lemma setsum_image_gen: assumes fS: "finite S"  nipkow@31509  870  shows "setsum g S = setsum (\y. setsum g {x. x \ S \ f x = y}) (f  S)"  nipkow@31509  871 proof-  nipkow@31509  872  { fix x assume "x \ S" then have "{y. y\ fS \ f x = y} = {f x}" by auto }  nipkow@31509  873  hence "setsum g S = setsum (\x. setsum (\y. g x) {y. y\ fS \ f x = y}) S"  nipkow@31509  874  by simp  nipkow@31509  875  also have "\ = setsum (\y. setsum g {x. x \ S \ f x = y}) (f  S)"  nipkow@31509  876  by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]])  nipkow@31509  877  finally show ?thesis .  nipkow@31509  878 qed  nipkow@31509  879 nipkow@31509  880 lemma setsum_multicount_gen:  nipkow@31509  881  assumes "finite s" "finite t" "\j\t. (card {i\s. R i j} = k j)"  nipkow@31509  882  shows "setsum (\i. (card {j\t. R i j})) s = setsum k t" (is "?l = ?r")  nipkow@31509  883 proof-  nipkow@31509  884  have "?l = setsum (\i. setsum (\x.1) {j\t. R i j}) s" by auto  nipkow@31509  885  also have "\ = ?r" unfolding setsum_setsum_restrict[OF assms(1-2)]  nipkow@31509  886  using assms(3) by auto  nipkow@31509  887  finally show ?thesis .  nipkow@31509  888 qed  nipkow@31509  889 nipkow@31509  890 lemma setsum_multicount:  nipkow@31509  891  assumes "finite S" "finite T" "\j\T. (card {i\S. R i j} = k)"  nipkow@31509  892  shows "setsum (\i. card {j\T. R i j}) S = k * card T" (is "?l = ?r")  nipkow@31509  893 proof-  nipkow@31509  894  have "?l = setsum (\i. k) T" by(rule setsum_multicount_gen)(auto simp:assms)  nipkow@31509  895  also have "\ = ?r" by(simp add: setsum_constant mult_commute)  nipkow@31509  896  finally show ?thesis by auto  nipkow@31509  897 qed  nipkow@31509  898 nipkow@28068  899 nipkow@16733  900 subsection{* Shifting bounds *}  nipkow@16733  901 nipkow@15539  902 lemma setsum_shift_bounds_nat_ivl:  nipkow@15539  903  "setsum f {m+k.. setsum f {Suc 0..k} = setsum f {0..k}"  nipkow@28068  922 by(simp add:setsum_head_Suc)  kleing@19106  923 nipkow@28068  924 lemma setsum_shift_lb_Suc0_0_upt:  nipkow@28068  925  "f(0::nat) = 0 \ setsum f {Suc 0.. (\i=0..i\{1..n}. of_nat i) =  kleing@19469  941  of_nat n*((of_nat n)+1)"  kleing@19469  942 proof (induct n)  kleing@19469  943  case 0  kleing@19469  944  show ?case by simp  kleing@19469  945 next  kleing@19469  946  case (Suc n)  nipkow@29667  947  then show ?case by (simp add: algebra_simps)  kleing@19469  948 qed  kleing@19469  949 kleing@19469  950 theorem arith_series_general:  huffman@23277  951  "((1::'a::comm_semiring_1) + 1) * (\i\{.. 1"  kleing@19469  955  let ?I = "\i. of_nat i" and ?n = "of_nat n"  kleing@19469  956  have  kleing@19469  957  "(\i\{..i\{..i\{.. = ?n*a + (\i\{.. = (?n*a + d*(\i\{1.. = (1+1)*?n*a + d*(1+1)*(\i\{1..i\{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"  huffman@30079  970  by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)  huffman@23431  971  (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]])  nipkow@29667  972  finally show ?thesis by (simp add: algebra_simps)  kleing@19469  973 next  kleing@19469  974  assume "\(n > 1)"  kleing@19469  975  hence "n = 1 \ n = 0" by auto  nipkow@29667  976  thus ?thesis by (auto simp: algebra_simps)  kleing@19469  977 qed  kleing@19469  978 kleing@19469  979 lemma arith_series_nat:  kleing@19469  980  "Suc (Suc 0) * (\i\{..i\{..i\{..i\{..nat"  kleing@19022  1003  shows  kleing@19022  1004  "\x. Q x \ P x \  kleing@19022  1005  (\xxxxx 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1031  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1032  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10)  paulson@29960  1033  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10)  paulson@29960  1034 syntax (xsymbols)  paulson@29960  1035  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1036  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1037  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1038  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1039 syntax (HTML output)  paulson@29960  1040  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1041  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1042  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1043  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1044 syntax (latex_prod output)  paulson@29960  1045  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1046  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1047  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1048  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1049  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1050  ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1051  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1052  ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1053 paulson@29960  1054 translations  paulson@29960  1055  "\x=a..b. t" == "CONST setprod (%x. t) {a..b}"  paulson@29960  1056  "\x=a..i\n. t" == "CONST setprod (\i. t) {..n}"  paulson@29960  1058 ` "\ii. t) {..