src/HOL/SetInterval.thy
 author nipkow Fri Oct 05 08:38:09 2007 +0200 (2007-10-05) changeset 24853 aab5798e5a33 parent 24748 ee0a0eb6b738 child 25062 af5ef0d4d655 permissions -rw-r--r--
 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  nipkow@15140  13 imports IntArith  nipkow@15131  14 begin  nipkow@8924  15 nipkow@24691  16 context ord  nipkow@24691  17 begin  nipkow@24691  18 definition  nipkow@24691  19  lessThan :: "'a => 'a set" ("(1\<^loc>{..<_})") where  haftmann@24748  20  "\<^loc>{..< u}"  nipkow@24691  21 nipkow@24691  22 definition  nipkow@24691  23  atMost :: "'a => 'a set" ("(1\<^loc>{.._})") where  haftmann@24748  24  "\<^loc>{..u} == {x. x \<^loc>\ u}"  nipkow@24691  25 nipkow@24691  26 definition  nipkow@24691  27  greaterThan :: "'a => 'a set" ("(1\<^loc>{_<..})") where  haftmann@24748  28  "\<^loc>{l<..} == {x. l\<^loc> 'a set" ("(1\<^loc>{_..})") where  haftmann@24748  32  "\<^loc>{l..} == {x. l\<^loc>\x}"  nipkow@24691  33 nipkow@24691  34 definition  nipkow@24691  35  greaterThanLessThan :: "'a => 'a => 'a set" ("(1\<^loc>{_<..<_})") where  nipkow@24691  36  "\<^loc>{l<..{l<..} Int \<^loc>{.. 'a => 'a set" ("(1\<^loc>{_..<_})") where  nipkow@24691  40  "\<^loc>{l..{l..} Int \<^loc>{.. 'a => 'a set" ("(1\<^loc>{_<.._})") where  nipkow@24691  44  "\<^loc>{l<..u} == \<^loc>{l<..} Int \<^loc>{..u}"  nipkow@24691  45 nipkow@24691  46 definition  nipkow@24691  47  atLeastAtMost :: "'a => 'a => 'a set" ("(1\<^loc>{_.._})") where  nipkow@24691  48  "\<^loc>{l..u} == \<^loc>{l..} Int \<^loc>{..u}"  nipkow@24691  49 nipkow@24691  50 end  nipkow@24691  51 (*  nipkow@8924  52 constdefs  nipkow@15045  53  lessThan :: "('a::ord) => 'a set" ("(1{..<_})")  nipkow@15045  54  "{.. 'a set" ("(1{.._})")  wenzelm@11609  57  "{..u} == {x. x<=u}"  nipkow@8924  58 nipkow@15045  59  greaterThan :: "('a::ord) => 'a set" ("(1{_<..})")  nipkow@15045  60  "{l<..} == {x. l 'a set" ("(1{_..})")  wenzelm@11609  63  "{l..} == {x. l<=x}"  nipkow@8924  64 nipkow@15045  65  greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{_<..<_})")  nipkow@15045  66  "{l<.. 'a set" ("(1{_..<_})")  nipkow@15045  69  "{l.. 'a set" ("(1{_<.._})")  nipkow@15045  72  "{l<..u} == {l<..} Int {..u}"  ballarin@13735  73 ballarin@13735  74  atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})")  ballarin@13735  75  "{l..u} == {l..} Int {..u}"  nipkow@24691  76 *)  ballarin@13735  77 nipkow@15048  78 text{* A note of warning when using @{term"{.. nat => 'b set => 'b set" ("(3UN _<=_./ _)" 10)  kleing@14418  84  "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3UN _<_./ _)" 10)  kleing@14418  85  "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10)  kleing@14418  86  "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3INT _<_./ _)" 10)  kleing@14418  87 kleing@14418  88 syntax (input)  kleing@14418  89  "@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10)  kleing@14418  90  "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10)  kleing@14418  91  "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10)  kleing@14418  92  "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10)  kleing@14418  93 kleing@14418  94 syntax (xsymbols)  wenzelm@14846  95  "@UNION_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10)  wenzelm@14846  96  "@UNION_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10)  wenzelm@14846  97  "@INTER_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10)  wenzelm@14846  98  "@INTER_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10)  kleing@14418  99 kleing@14418  100 translations  kleing@14418  101  "UN i<=n. A" == "UN i:{..n}. A"  nipkow@15045  102  "UN i<=i)"  paulson@13850  134 by (simp add: atLeast_def)  ballarin@13735  135 paulson@15418  136 lemma Compl_atLeast [simp]:  ballarin@13735  137  "!!k:: 'a::linorder. -atLeast k = lessThan k"  paulson@13850  138 apply (simp add: lessThan_def atLeast_def le_def, auto)  ballarin@13735  139 done  ballarin@13735  140 nipkow@24691  141 lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i\<^loc><=k)"  paulson@13850  142 by (simp add: atMost_def)  ballarin@13735  143 paulson@14485  144 lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"  paulson@14485  145 by (blast intro: order_antisym)  paulson@13850  146 paulson@13850  147 paulson@14485  148 subsection {* Logical Equivalences for Set Inclusion and Equality *}  paulson@13850  149 paulson@13850  150 lemma atLeast_subset_iff [iff]:  paulson@15418  151  "(atLeast x \ atLeast y) = (y \ (x::'a::order))"  paulson@15418  152 by (blast intro: order_trans)  paulson@13850  153 paulson@13850  154 lemma atLeast_eq_iff [iff]:  paulson@15418  155  "(atLeast x = atLeast y) = (x = (y::'a::linorder))"  paulson@13850  156 by (blast intro: order_antisym order_trans)  paulson@13850  157 paulson@13850  158 lemma greaterThan_subset_iff [iff]:  paulson@15418  159  "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))"  paulson@15418  160 apply (auto simp add: greaterThan_def)  paulson@15418  161  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  162 done  paulson@13850  163 paulson@13850  164 lemma greaterThan_eq_iff [iff]:  paulson@15418  165  "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"  paulson@15418  166 apply (rule iffI)  paulson@15418  167  apply (erule equalityE)  paulson@15418  168  apply (simp_all add: greaterThan_subset_iff)  paulson@13850  169 done  paulson@13850  170 paulson@15418  171 lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))"  paulson@13850  172 by (blast intro: order_trans)  paulson@13850  173 paulson@15418  174 lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"  paulson@13850  175 by (blast intro: order_antisym order_trans)  paulson@13850  176 paulson@13850  177 lemma lessThan_subset_iff [iff]:  paulson@15418  178  "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))"  paulson@15418  179 apply (auto simp add: lessThan_def)  paulson@15418  180  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  181 done  paulson@13850  182 paulson@13850  183 lemma lessThan_eq_iff [iff]:  paulson@15418  184  "(lessThan x = lessThan y) = (x = (y::'a::linorder))"  paulson@15418  185 apply (rule iffI)  paulson@15418  186  apply (erule equalityE)  paulson@15418  187  apply (simp_all add: lessThan_subset_iff)  ballarin@13735  188 done  ballarin@13735  189 ballarin@13735  190 paulson@13850  191 subsection {*Two-sided intervals*}  ballarin@13735  192 nipkow@24691  193 context ord  nipkow@24691  194 begin  nipkow@24691  195 paulson@24286  196 lemma greaterThanLessThan_iff [simp,noatp]:  nipkow@24691  197  "(i : \<^loc>{l<..< i & i \<^loc>< u)"  ballarin@13735  198 by (simp add: greaterThanLessThan_def)  ballarin@13735  199 paulson@24286  200 lemma atLeastLessThan_iff [simp,noatp]:  nipkow@24691  201  "(i : \<^loc>{l..<= i & i \<^loc>< u)"  ballarin@13735  202 by (simp add: atLeastLessThan_def)  ballarin@13735  203 paulson@24286  204 lemma greaterThanAtMost_iff [simp,noatp]:  nipkow@24691  205  "(i : \<^loc>{l<..u}) = (l \<^loc>< i & i \<^loc><= u)"  ballarin@13735  206 by (simp add: greaterThanAtMost_def)  ballarin@13735  207 paulson@24286  208 lemma atLeastAtMost_iff [simp,noatp]:  nipkow@24691  209  "(i : \<^loc>{l..u}) = (l \<^loc><= i & i \<^loc><= u)"  ballarin@13735  210 by (simp add: atLeastAtMost_def)  ballarin@13735  211 wenzelm@14577  212 text {* The above four lemmas could be declared as iffs.  wenzelm@14577  213  If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}  wenzelm@14577  214  seems to take forever (more than one hour). *}  nipkow@24691  215 end  ballarin@13735  216 nipkow@15554  217 subsubsection{* Emptyness and singletons *}  nipkow@15554  218 nipkow@24691  219 context order  nipkow@24691  220 begin  nipkow@15554  221 nipkow@24691  222 lemma atLeastAtMost_empty [simp]: "n \<^loc>< m ==> \<^loc>{m..n} = {}";  nipkow@24691  223 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)  nipkow@24691  224 nipkow@24691  225 lemma atLeastLessThan_empty[simp]: "n \<^loc>\ m ==> \<^loc>{m..\ k ==> \<^loc>{k<..l} = {}"  nipkow@17719  229 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)  nipkow@17719  230 nipkow@24691  231 lemma greaterThanLessThan_empty[simp]:"l \<^loc>\ k ==> \<^loc>{k<..l} = {}"  nipkow@17719  232 by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)  nipkow@17719  233 nipkow@24691  234 lemma atLeastAtMost_singleton [simp]: "\<^loc>{a..a} = {a}"  nipkow@24691  235 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)  nipkow@24691  236 nipkow@24691  237 end  paulson@14485  238 paulson@14485  239 subsection {* Intervals of natural numbers *}  paulson@14485  240 paulson@15047  241 subsubsection {* The Constant @{term lessThan} *}  paulson@15047  242 paulson@14485  243 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"  paulson@14485  244 by (simp add: lessThan_def)  paulson@14485  245 paulson@14485  246 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"  paulson@14485  247 by (simp add: lessThan_def less_Suc_eq, blast)  paulson@14485  248 paulson@14485  249 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"  paulson@14485  250 by (simp add: lessThan_def atMost_def less_Suc_eq_le)  paulson@14485  251 paulson@14485  252 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"  paulson@14485  253 by blast  paulson@14485  254 paulson@15047  255 subsubsection {* The Constant @{term greaterThan} *}  paulson@15047  256 paulson@14485  257 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"  paulson@14485  258 apply (simp add: greaterThan_def)  paulson@14485  259 apply (blast dest: gr0_conv_Suc [THEN iffD1])  paulson@14485  260 done  paulson@14485  261 paulson@14485  262 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"  paulson@14485  263 apply (simp add: greaterThan_def)  paulson@14485  264 apply (auto elim: linorder_neqE)  paulson@14485  265 done  paulson@14485  266 paulson@14485  267 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"  paulson@14485  268 by blast  paulson@14485  269 paulson@15047  270 subsubsection {* The Constant @{term atLeast} *}  paulson@15047  271 paulson@14485  272 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"  paulson@14485  273 by (unfold atLeast_def UNIV_def, simp)  paulson@14485  274 paulson@14485  275 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"  paulson@14485  276 apply (simp add: atLeast_def)  paulson@14485  277 apply (simp add: Suc_le_eq)  paulson@14485  278 apply (simp add: order_le_less, blast)  paulson@14485  279 done  paulson@14485  280 paulson@14485  281 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"  paulson@14485  282  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)  paulson@14485  283 paulson@14485  284 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"  paulson@14485  285 by blast  paulson@14485  286 paulson@15047  287 subsubsection {* The Constant @{term atMost} *}  paulson@15047  288 paulson@14485  289 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"  paulson@14485  290 by (simp add: atMost_def)  paulson@14485  291 paulson@14485  292 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"  paulson@14485  293 apply (simp add: atMost_def)  paulson@14485  294 apply (simp add: less_Suc_eq order_le_less, blast)  paulson@14485  295 done  paulson@14485  296 paulson@14485  297 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"  paulson@14485  298 by blast  paulson@14485  299 paulson@15047  300 subsubsection {* The Constant @{term atLeastLessThan} *}  paulson@15047  301 nipkow@24449  302 text{*The orientation of the following rule is tricky. The lhs is  nipkow@24449  303 defined in terms of the rhs. Hence the chosen orientation makes sense  nipkow@24449  304 in this theory --- the reverse orientation complicates proofs (eg  nipkow@24449  305 nontermination). But outside, when the definition of the lhs is rarely  nipkow@24449  306 used, the opposite orientation seems preferable because it reduces a  nipkow@24449  307 specific concept to a more general one. *}  paulson@15047  308 lemma atLeast0LessThan: "{0::nat.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  344 by (auto simp add: atLeastAtMost_def)  nipkow@15554  345 nipkow@16733  346 subsubsection {* Image *}  nipkow@16733  347 nipkow@16733  348 lemma image_add_atLeastAtMost:  nipkow@16733  349  "(%n::nat. n+k)  {i..j} = {i+k..j+k}" (is "?A = ?B")  nipkow@16733  350 proof  nipkow@16733  351  show "?A \ ?B" by auto  nipkow@16733  352 next  nipkow@16733  353  show "?B \ ?A"  nipkow@16733  354  proof  nipkow@16733  355  fix n assume a: "n : ?B"  webertj@20217  356  hence "n - k : {i..j}" by auto  nipkow@16733  357  moreover have "n = (n - k) + k" using a by auto  nipkow@16733  358  ultimately show "n : ?A" by blast  nipkow@16733  359  qed  nipkow@16733  360 qed  nipkow@16733  361 nipkow@16733  362 lemma image_add_atLeastLessThan:  nipkow@16733  363  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  366 next  nipkow@16733  367  show "?B \ ?A"  nipkow@16733  368  proof  nipkow@16733  369  fix n assume a: "n : ?B"  webertj@20217  370  hence "n - k : {i.. finite N"  paulson@14485  418  -- {* A bounded set of natural numbers is finite. *}  paulson@14485  419  apply (rule finite_subset)  paulson@14485  420  apply (rule_tac [2] finite_lessThan, auto)  paulson@14485  421  done  paulson@14485  422 nipkow@24853  423 text{* Any subset of an interval of natural numbers the size of the  nipkow@24853  424 subset is exactly that interval. *}  nipkow@24853  425 nipkow@24853  426 lemma subset_card_intvl_is_intvl:  nipkow@24853  427  "A <= {k.. A = {k.. u ==>  nipkow@15045  489  {(0::int).. u")  paulson@14485  498  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  499  apply (rule finite_imageI)  paulson@14485  500  apply auto  paulson@14485  501  done  paulson@14485  502 nipkow@15045  503 lemma finite_atLeastLessThan_int [iff]: "finite {l.. u")  paulson@14485  525  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  526  apply (subst card_image)  paulson@14485  527  apply (auto simp add: inj_on_def)  paulson@14485  528  done  paulson@14485  529 nipkow@15045  530 lemma card_atLeastLessThan_int [simp]: "card {l.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  566  "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  575  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  577  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  579  "(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  591  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  593 by auto  ballarin@13735  594 ballarin@13735  595 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two  ballarin@13735  596 wenzelm@14577  597 subsubsection {* Disjoint Intersections *}  ballarin@13735  598 wenzelm@14577  599 text {* Singletons and open intervals *}  ballarin@13735  600 ballarin@13735  601 lemma ivl_disj_int_singleton:  nipkow@15045  602  "{l::'a::order} Int {l<..} = {}"  nipkow@15045  603  "{.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  649 apply(auto simp:linorder_not_le)  nipkow@15542  650 apply(rule ccontr)  nipkow@15542  651 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  652 apply(clarsimp simp:linorder_not_le)  nipkow@15542  653 apply(fastsimp)  nipkow@15542  654 done  nipkow@15542  655 nipkow@15041  656 nipkow@15042  657 subsection {* Summation indexed over intervals *}  nipkow@15042  658 nipkow@15042  659 syntax  nipkow@15042  660  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  661  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  662  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@16052  663  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  nipkow@15042  664 syntax (xsymbols)  nipkow@15042  665  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  666  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  667  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  668  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15042  669 syntax (HTML output)  nipkow@15042  670  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  671  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  672  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  673  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15056  674 syntax (latex_sum output)  nipkow@15052  675  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  676  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@15052  677  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  678  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@16052  679  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  680  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15052  681  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  682  ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15041  683 nipkow@15048  684 translations  nipkow@15048  685  "\x=a..b. t" == "setsum (%x. t) {a..b}"  nipkow@15048  686  "\x=a..i\n. t" == "setsum (\i. t) {..n}"  nipkow@15048  688  "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  696 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  698 @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \  nipkow@15542  721  setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)"  nipkow@16052  728 by (simp add:atMost_Suc add_ac)  nipkow@16052  729 nipkow@16041  730 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n"  nipkow@16041  731 by (simp add:lessThan_Suc add_ac)  nipkow@15041  732 nipkow@15911  733 lemma setsum_cl_ivl_Suc[simp]:  nipkow@15561  734  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  nipkow@15561  735 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@15561  736 nipkow@15911  737 lemma setsum_op_ivl_Suc[simp]:  nipkow@15561  738  "setsum f {m..  nipkow@15561  742  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  nipkow@15561  743 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@16041  744 *)  nipkow@15539  745 lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \  nipkow@15539  746  setsum f {m.. 'a::ab_group_add"  nipkow@15539  751 shows "\ m \ n; n \ p \ \  nipkow@15539  752  setsum f {m..x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  kleing@19106  781 proof -  kleing@19106  782  from mn  kleing@19106  783  have "{m..n} = {m} \ {m<..n}"  kleing@19106  784  by (auto intro: ivl_disj_un_singleton)  kleing@19106  785  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  kleing@19106  786  by (simp add: atLeast0LessThan)  kleing@19106  787  also have "\ = ?rhs" by simp  kleing@19106  788  finally show ?thesis .  kleing@19106  789 qed  kleing@19106  790 kleing@19106  791 lemma setsum_head_upt:  kleing@19022  792  fixes m::nat  kleing@19022  793  assumes m: "0 < m"  kleing@19106  794  shows "(\xx\{1..xx\{0.. = (\x\{0..m - 1}. P x)"  kleing@19106  801  by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost)  kleing@19106  802  also  kleing@19106  803  have "\ = P 0 + (\x\{0<..m - 1}. P x)"  kleing@19106  804  by (simp add: setsum_head)  kleing@19106  805  also  kleing@19106  806  from m  kleing@19106  807  have "{0<..m - 1} = {1.. (\i=0..i\{1..n}. of_nat i) =  kleing@19469  823  of_nat n*((of_nat n)+1)"  kleing@19469  824 proof (induct n)  kleing@19469  825  case 0  kleing@19469  826  show ?case by simp  kleing@19469  827 next  kleing@19469  828  case (Suc n)  nipkow@23477  829  then show ?case by (simp add: ring_simps)  kleing@19469  830 qed  kleing@19469  831 kleing@19469  832 theorem arith_series_general:  huffman@23277  833  "((1::'a::comm_semiring_1) + 1) * (\i\{.. 1"  kleing@19469  837  let ?I = "\i. of_nat i" and ?n = "of_nat n"  kleing@19469  838  have  kleing@19469  839  "(\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  851  by (simp only: mult_ac gauss_sum [of "n - 1"])  huffman@23431  852  (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]])  kleing@19469  853  finally show ?thesis by (simp add: mult_ac add_ac right_distrib)  kleing@19469  854 next  kleing@19469  855  assume "\(n > 1)"  kleing@19469  856  hence "n = 1 \ n = 0" by auto  kleing@19469  857  thus ?thesis by (auto simp: mult_ac right_distrib)  kleing@19469  858 qed  kleing@19469  859 kleing@19469  860 lemma arith_series_nat:  kleing@19469  861  "Suc (Suc 0) * (\i\{..i\{..i\{..i\{..nat"  kleing@19022  883  shows  kleing@19022  884  "\x. Q x \ P x \  kleing@19022  885 ` (\xxxxx