src/HOL/SetInterval.thy
 author nipkow Mon Sep 01 19:16:40 2008 +0200 (2008-09-01) changeset 28068 f6b2d1995171 parent 27656 d4f6e64ee7cc child 28853 69eb69659bf3 permissions -rw-r--r--
cleaned up code generation for {.._} and {..<_}
moved lemmas into SetInterval where they belong
 nipkow@8924  1 (* Title: HOL/SetInterval.thy  nipkow@8924  2  ID: $Id$  ballarin@13735  3  Author: Tobias Nipkow and Clemens Ballarin  paulson@14485  4  Additions by Jeremy Avigad in March 2004  paulson@8957  5  Copyright 2000 TU Muenchen  nipkow@8924  6 ballarin@13735  7 lessThan, greaterThan, atLeast, atMost and two-sided intervals  nipkow@8924  8 *)  nipkow@8924  9 wenzelm@14577  10 header {* Set intervals *}  wenzelm@14577  11 nipkow@15131  12 theory SetInterval  haftmann@25919  13 imports Int  nipkow@15131  14 begin  nipkow@8924  15 nipkow@24691  16 context ord  nipkow@24691  17 begin  nipkow@24691  18 definition  haftmann@25062  19  lessThan :: "'a => 'a set" ("(1{..<_})") where  haftmann@25062  20  "{.. 'a set" ("(1{.._})") where  haftmann@25062  24  "{..u} == {x. x \ u}"  nipkow@24691  25 nipkow@24691  26 definition  haftmann@25062  27  greaterThan :: "'a => 'a set" ("(1{_<..})") where  haftmann@25062  28  "{l<..} == {x. l 'a set" ("(1{_..})") where  haftmann@25062  32  "{l..} == {x. l\x}"  nipkow@24691  33 nipkow@24691  34 definition  haftmann@25062  35  greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where  haftmann@25062  36  "{l<.. 'a => 'a set" ("(1{_..<_})") where  haftmann@25062  40  "{l.. 'a => 'a set" ("(1{_<.._})") where  haftmann@25062  44  "{l<..u} == {l<..} Int {..u}"  nipkow@24691  45 nipkow@24691  46 definition  haftmann@25062  47  atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where  haftmann@25062  48  "{l..u} == {l..} Int {..u}"  nipkow@24691  49 nipkow@24691  50 end  nipkow@8924  51 ballarin@13735  52 nipkow@15048  53 text{* A note of warning when using @{term"{.. nat => 'b set => 'b set" ("(3UN _<=_./ _)" 10)  kleing@14418  59  "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3UN _<_./ _)" 10)  kleing@14418  60  "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10)  kleing@14418  61  "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3INT _<_./ _)" 10)  kleing@14418  62 kleing@14418  63 syntax (input)  kleing@14418  64  "@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10)  kleing@14418  65  "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10)  kleing@14418  66  "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10)  kleing@14418  67  "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10)  kleing@14418  68 kleing@14418  69 syntax (xsymbols)  wenzelm@14846  70  "@UNION_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10)  wenzelm@14846  71  "@UNION_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10)  wenzelm@14846  72  "@INTER_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10)  wenzelm@14846  73  "@INTER_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10)  kleing@14418  74 kleing@14418  75 translations  kleing@14418  76  "UN i<=n. A" == "UN i:{..n}. A"  nipkow@15045  77  "UN i atLeast y) = (y \ (x::'a::order))"  paulson@15418  125 by (blast intro: order_trans)  paulson@13850  126 paulson@13850  127 lemma atLeast_eq_iff [iff]:  paulson@15418  128  "(atLeast x = atLeast y) = (x = (y::'a::linorder))"  paulson@13850  129 by (blast intro: order_antisym order_trans)  paulson@13850  130 paulson@13850  131 lemma greaterThan_subset_iff [iff]:  paulson@15418  132  "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))"  paulson@15418  133 apply (auto simp add: greaterThan_def)  paulson@15418  134  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  135 done  paulson@13850  136 paulson@13850  137 lemma greaterThan_eq_iff [iff]:  paulson@15418  138  "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"  paulson@15418  139 apply (rule iffI)  paulson@15418  140  apply (erule equalityE)  paulson@15418  141  apply (simp_all add: greaterThan_subset_iff)  paulson@13850  142 done  paulson@13850  143 paulson@15418  144 lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))"  paulson@13850  145 by (blast intro: order_trans)  paulson@13850  146 paulson@15418  147 lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"  paulson@13850  148 by (blast intro: order_antisym order_trans)  paulson@13850  149 paulson@13850  150 lemma lessThan_subset_iff [iff]:  paulson@15418  151  "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))"  paulson@15418  152 apply (auto simp add: lessThan_def)  paulson@15418  153  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  154 done  paulson@13850  155 paulson@13850  156 lemma lessThan_eq_iff [iff]:  paulson@15418  157  "(lessThan x = lessThan y) = (x = (y::'a::linorder))"  paulson@15418  158 apply (rule iffI)  paulson@15418  159  apply (erule equalityE)  paulson@15418  160  apply (simp_all add: lessThan_subset_iff)  ballarin@13735  161 done  ballarin@13735  162 ballarin@13735  163 paulson@13850  164 subsection {*Two-sided intervals*}  ballarin@13735  165 nipkow@24691  166 context ord  nipkow@24691  167 begin  nipkow@24691  168 paulson@24286  169 lemma greaterThanLessThan_iff [simp,noatp]:  haftmann@25062  170  "(i : {l<.. {m..n} = {}";  nipkow@24691  196 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)  nipkow@24691  197 haftmann@25062  198 lemma atLeastLessThan_empty[simp]: "n \ m ==> {m.. k ==> {k<..l} = {}"  nipkow@17719  202 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)  nipkow@17719  203 haftmann@25062  204 lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<..l} = {}"  nipkow@17719  205 by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)  nipkow@17719  206 haftmann@25062  207 lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"  nipkow@24691  208 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)  nipkow@24691  209 nipkow@24691  210 end  paulson@14485  211 paulson@14485  212 subsection {* Intervals of natural numbers *}  paulson@14485  213 paulson@15047  214 subsubsection {* The Constant @{term lessThan} *}  paulson@15047  215 paulson@14485  216 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"  paulson@14485  217 by (simp add: lessThan_def)  paulson@14485  218 paulson@14485  219 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"  paulson@14485  220 by (simp add: lessThan_def less_Suc_eq, blast)  paulson@14485  221 paulson@14485  222 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"  paulson@14485  223 by (simp add: lessThan_def atMost_def less_Suc_eq_le)  paulson@14485  224 paulson@14485  225 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"  paulson@14485  226 by blast  paulson@14485  227 paulson@15047  228 subsubsection {* The Constant @{term greaterThan} *}  paulson@15047  229 paulson@14485  230 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"  paulson@14485  231 apply (simp add: greaterThan_def)  paulson@14485  232 apply (blast dest: gr0_conv_Suc [THEN iffD1])  paulson@14485  233 done  paulson@14485  234 paulson@14485  235 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"  paulson@14485  236 apply (simp add: greaterThan_def)  paulson@14485  237 apply (auto elim: linorder_neqE)  paulson@14485  238 done  paulson@14485  239 paulson@14485  240 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"  paulson@14485  241 by blast  paulson@14485  242 paulson@15047  243 subsubsection {* The Constant @{term atLeast} *}  paulson@15047  244 paulson@14485  245 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"  paulson@14485  246 by (unfold atLeast_def UNIV_def, simp)  paulson@14485  247 paulson@14485  248 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"  paulson@14485  249 apply (simp add: atLeast_def)  paulson@14485  250 apply (simp add: Suc_le_eq)  paulson@14485  251 apply (simp add: order_le_less, blast)  paulson@14485  252 done  paulson@14485  253 paulson@14485  254 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"  paulson@14485  255  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)  paulson@14485  256 paulson@14485  257 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"  paulson@14485  258 by blast  paulson@14485  259 paulson@15047  260 subsubsection {* The Constant @{term atMost} *}  paulson@15047  261 paulson@14485  262 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"  paulson@14485  263 by (simp add: atMost_def)  paulson@14485  264 paulson@14485  265 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"  paulson@14485  266 apply (simp add: atMost_def)  paulson@14485  267 apply (simp add: less_Suc_eq order_le_less, blast)  paulson@14485  268 done  paulson@14485  269 paulson@14485  270 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"  paulson@14485  271 by blast  paulson@14485  272 paulson@15047  273 subsubsection {* The Constant @{term atLeastLessThan} *}  paulson@15047  274 nipkow@28068  275 text{*The orientation of the following 2 rules is tricky. The lhs is  nipkow@24449  276 defined in terms of the rhs. Hence the chosen orientation makes sense  nipkow@24449  277 in this theory --- the reverse orientation complicates proofs (eg  nipkow@24449  278 nontermination). But outside, when the definition of the lhs is rarely  nipkow@24449  279 used, the opposite orientation seems preferable because it reduces a  nipkow@24449  280 specific concept to a more general one. *}  nipkow@28068  281 paulson@15047  282 lemma atLeast0LessThan: "{0::nat.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  322 by (auto simp add: atLeastAtMost_def)  nipkow@15554  323 nipkow@16733  324 subsubsection {* Image *}  nipkow@16733  325 nipkow@16733  326 lemma image_add_atLeastAtMost:  nipkow@16733  327  "(%n::nat. n+k)  {i..j} = {i+k..j+k}" (is "?A = ?B")  nipkow@16733  328 proof  nipkow@16733  329  show "?A \ ?B" by auto  nipkow@16733  330 next  nipkow@16733  331  show "?B \ ?A"  nipkow@16733  332  proof  nipkow@16733  333  fix n assume a: "n : ?B"  webertj@20217  334  hence "n - k : {i..j}" by auto  nipkow@16733  335  moreover have "n = (n - k) + k" using a by auto  nipkow@16733  336  ultimately show "n : ?A" by blast  nipkow@16733  337  qed  nipkow@16733  338 qed  nipkow@16733  339 nipkow@16733  340 lemma image_add_atLeastLessThan:  nipkow@16733  341  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  344 next  nipkow@16733  345  show "?B \ ?A"  nipkow@16733  346  proof  nipkow@16733  347  fix n assume a: "n : ?B"  webertj@20217  348  hence "n - k : {i.. finite N"  nipkow@28068  397 apply (rule finite_subset)  nipkow@28068  398  apply (rule_tac [2] finite_lessThan, auto)  nipkow@28068  399 done  nipkow@28068  400 nipkow@28068  401 lemma finite_less_ub:  nipkow@28068  402  "!!f::nat=>nat. (!!n. n \ f n) ==> finite {n. f n \ u}"  nipkow@28068  403 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)  paulson@14485  404 nipkow@24853  405 text{* Any subset of an interval of natural numbers the size of the  nipkow@24853  406 subset is exactly that interval. *}  nipkow@24853  407 nipkow@24853  408 lemma subset_card_intvl_is_intvl:  nipkow@24853  409  "A <= {k.. A = {k.. \h. bij_betw h {0.. \h. bij_betw h M {0.. u ==>  nipkow@15045  483  {(0::int).. u")  paulson@14485  492  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  493  apply (rule finite_imageI)  paulson@14485  494  apply auto  paulson@14485  495  done  paulson@14485  496 nipkow@15045  497 lemma finite_atLeastLessThan_int [iff]: "finite {l.. u")  paulson@14485  519  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  520  apply (subst card_image)  paulson@14485  521  apply (auto simp add: inj_on_def)  paulson@14485  522  done  paulson@14485  523 nipkow@15045  524 lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}"  bulwahn@27656  546 proof -  bulwahn@27656  547  have "{k. P k \ k < i} \ {.. M"  bulwahn@27656  553 shows "card {k \ M. k < Suc i} \ 0"  bulwahn@27656  554 proof -  bulwahn@27656  555  from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto  bulwahn@27656  556  with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)  bulwahn@27656  557 qed  bulwahn@27656  558 bulwahn@27656  559 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"  bulwahn@27656  560 apply (rule card_bij_eq [of "Suc" _ _ "\x. x - 1"])  bulwahn@27656  561 apply simp  bulwahn@27656  562 apply fastsimp  bulwahn@27656  563 apply auto  bulwahn@27656  564 apply (rule inj_on_diff_nat)  bulwahn@27656  565 apply auto  bulwahn@27656  566 apply (case_tac x)  bulwahn@27656  567 apply auto  bulwahn@27656  568 apply (case_tac xa)  bulwahn@27656  569 apply auto  bulwahn@27656  570 apply (case_tac xa)  bulwahn@27656  571 apply auto  bulwahn@27656  572 apply (auto simp add: finite_M_bounded_by_nat)  bulwahn@27656  573 done  bulwahn@27656  574 bulwahn@27656  575 lemma card_less_Suc:  bulwahn@27656  576  assumes zero_in_M: "0 \ M"  bulwahn@27656  577  shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"  bulwahn@27656  578 proof -  bulwahn@27656  579  from assms have a: "0 \ {k \ M. k < Suc i}" by simp  bulwahn@27656  580  hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})"  bulwahn@27656  581  by (auto simp only: insert_Diff)  bulwahn@27656  582  have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto  bulwahn@27656  583  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  584  apply (subst card_insert)  bulwahn@27656  585  apply simp_all  bulwahn@27656  586  apply (subst b)  bulwahn@27656  587  apply (subst card_less_Suc2[symmetric])  bulwahn@27656  588  apply simp_all  bulwahn@27656  589  done  bulwahn@27656  590  with c show ?thesis by simp  bulwahn@27656  591 qed  bulwahn@27656  592 paulson@14485  593 paulson@13850  594 subsection {*Lemmas useful with the summation operator setsum*}  paulson@13850  595 ballarin@16102  596 text {* For examples, see Algebra/poly/UnivPoly2.thy *}  ballarin@13735  597 wenzelm@14577  598 subsubsection {* Disjoint Unions *}  ballarin@13735  599 wenzelm@14577  600 text {* Singletons and open intervals *}  ballarin@13735  601 ballarin@13735  602 lemma ivl_disj_un_singleton:  nipkow@15045  603  "{l::'a::linorder} Un {l<..} = {l..}"  nipkow@15045  604  "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  608  "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  617  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  619  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  621  "(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  633  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  635 by auto  ballarin@13735  636 ballarin@13735  637 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two  ballarin@13735  638 wenzelm@14577  639 subsubsection {* Disjoint Intersections *}  ballarin@13735  640 wenzelm@14577  641 text {* Singletons and open intervals *}  ballarin@13735  642 ballarin@13735  643 lemma ivl_disj_int_singleton:  nipkow@15045  644  "{l::'a::order} Int {l<..} = {}"  nipkow@15045  645  "{.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  691 apply(auto simp:linorder_not_le)  nipkow@15542  692 apply(rule ccontr)  nipkow@15542  693 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  694 apply(clarsimp simp:linorder_not_le)  nipkow@15542  695 apply(fastsimp)  nipkow@15542  696 done  nipkow@15542  697 nipkow@15041  698 nipkow@15042  699 subsection {* Summation indexed over intervals *}  nipkow@15042  700 nipkow@15042  701 syntax  nipkow@15042  702  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  703  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  704  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@16052  705  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  nipkow@15042  706 syntax (xsymbols)  nipkow@15042  707  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  708  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  709  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  710  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15042  711 syntax (HTML output)  nipkow@15042  712  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  713  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  714  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  715  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15056  716 syntax (latex_sum output)  nipkow@15052  717  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  718  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@15052  719  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  720  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@16052  721  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  722  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15052  723  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  724  ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15041  725 nipkow@15048  726 translations  nipkow@15048  727  "\x=a..b. t" == "setsum (%x. t) {a..b}"  nipkow@15048  728  "\x=a..i\n. t" == "setsum (\i. t) {..n}"  nipkow@15048  730  "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  738 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  740 @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \  nipkow@15542  763  setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)"  nipkow@16052  770 by (simp add:atMost_Suc add_ac)  nipkow@16052  771 nipkow@16041  772 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n"  nipkow@16041  773 by (simp add:lessThan_Suc add_ac)  nipkow@15041  774 nipkow@15911  775 lemma setsum_cl_ivl_Suc[simp]:  nipkow@15561  776  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  nipkow@15561  777 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@15561  778 nipkow@15911  779 lemma setsum_op_ivl_Suc[simp]:  nipkow@15561  780  "setsum f {m..  nipkow@15561  784  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  nipkow@15561  785 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@16041  786 *)  nipkow@28068  787 nipkow@28068  788 lemma setsum_head:  nipkow@28068  789  fixes n :: nat  nipkow@28068  790  assumes mn: "m <= n"  nipkow@28068  791  shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  nipkow@28068  792 proof -  nipkow@28068  793  from mn  nipkow@28068  794  have "{m..n} = {m} \ {m<..n}"  nipkow@28068  795  by (auto intro: ivl_disj_un_singleton)  nipkow@28068  796  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  nipkow@28068  797  by (simp add: atLeast0LessThan)  nipkow@28068  798  also have "\ = ?rhs" by simp  nipkow@28068  799  finally show ?thesis .  nipkow@28068  800 qed  nipkow@28068  801 nipkow@28068  802 lemma setsum_head_Suc:  nipkow@28068  803  "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}"  nipkow@28068  804 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)  nipkow@28068  805 nipkow@28068  806 lemma setsum_head_upt_Suc:  nipkow@28068  807  "m < n \ setsum f {m.. m \ n; n \ p \ \  nipkow@15539  814  setsum f {m.. 'a::ab_group_add"  nipkow@15539  819 shows "\ m \ n; n \ p \ \  nipkow@15539  820  setsum f {m.. setsum f {Suc 0..k} = setsum f {0..k}"  nipkow@28068  848 by(simp add:setsum_head_Suc)  kleing@19106  849 nipkow@28068  850 lemma setsum_shift_lb_Suc0_0_upt:  nipkow@28068  851  "f(0::nat) = 0 \ setsum f {Suc 0.. (\i=0..i\{1..n}. of_nat i) =  kleing@19469  867  of_nat n*((of_nat n)+1)"  kleing@19469  868 proof (induct n)  kleing@19469  869  case 0  kleing@19469  870  show ?case by simp  kleing@19469  871 next  kleing@19469  872  case (Suc n)  nipkow@23477  873  then show ?case by (simp add: ring_simps)  kleing@19469  874 qed  kleing@19469  875 kleing@19469  876 theorem arith_series_general:  huffman@23277  877  "((1::'a::comm_semiring_1) + 1) * (\i\{.. 1"  kleing@19469  881  let ?I = "\i. of_nat i" and ?n = "of_nat n"  kleing@19469  882  have  kleing@19469  883  "(\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)"  kleing@19469  895  by (simp only: mult_ac gauss_sum [of "n - 1"])  huffman@23431  896  (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]])  kleing@19469  897  finally show ?thesis by (simp add: mult_ac add_ac right_distrib)  kleing@19469  898 next  kleing@19469  899  assume "\(n > 1)"  kleing@19469  900  hence "n = 1 \ n = 0" by auto  kleing@19469  901  thus ?thesis by (auto simp: mult_ac right_distrib)  kleing@19469  902 qed  kleing@19469  903 kleing@19469  904 lemma arith_series_nat:  kleing@19469  905  "Suc (Suc 0) * (\i\{..i\{..i\{..i\{..nat"  kleing@19022  927  shows  kleing@19022  928  "\x. Q x \ P x \  kleing@19022  929 ` (\xxxxx