src/HOL/Set_Interval.thy
 author blanchet Tue Nov 07 15:16:42 2017 +0100 (19 months ago) changeset 67022 49309fe530fd parent 66936 cf8d8fc23891 child 67091 1393c2340eec permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
 huffman@47317  1 (* Title: HOL/Set_Interval.thy  wenzelm@32960  2  Author: Tobias Nipkow  wenzelm@32960  3  Author: Clemens Ballarin  wenzelm@32960  4  Author: Jeremy Avigad  nipkow@8924  5 ballarin@13735  6 lessThan, greaterThan, atLeast, atMost and two-sided intervals  nipkow@51334  7 nipkow@51334  8 Modern convention: Ixy stands for an interval where x and y  nipkow@51334  9 describe the lower and upper bound and x,y : {c,o,i}  nipkow@51334  10 where c = closed, o = open, i = infinite.  nipkow@51334  11 Examples: Ico = {_ ..< _} and Ici = {_ ..}  nipkow@8924  12 *)  nipkow@8924  13 wenzelm@60758  14 section \Set intervals\  wenzelm@14577  15 huffman@47317  16 theory Set_Interval  haftmann@66836  17 imports Divides  nipkow@15131  18 begin  nipkow@8924  19 nipkow@24691  20 context ord  nipkow@24691  21 begin  haftmann@44008  22 nipkow@24691  23 definition  wenzelm@32960  24  lessThan :: "'a => 'a set" ("(1{..<_})") where  haftmann@25062  25  "{.. 'a set" ("(1{.._})") where  haftmann@25062  29  "{..u} == {x. x \ u}"  nipkow@24691  30 nipkow@24691  31 definition  wenzelm@32960  32  greaterThan :: "'a => 'a set" ("(1{_<..})") where  haftmann@25062  33  "{l<..} == {x. l 'a set" ("(1{_..})") where  haftmann@25062  37  "{l..} == {x. l\x}"  nipkow@24691  38 nipkow@24691  39 definition  haftmann@25062  40  greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where  haftmann@25062  41  "{l<.. 'a => 'a set" ("(1{_..<_})") where  haftmann@25062  45  "{l.. 'a => 'a set" ("(1{_<.._})") where  haftmann@25062  49  "{l<..u} == {l<..} Int {..u}"  nipkow@24691  50 nipkow@24691  51 definition  haftmann@25062  52  atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where  haftmann@25062  53  "{l..u} == {l..} Int {..u}"  nipkow@24691  54 nipkow@24691  55 end  nipkow@8924  56 ballarin@13735  57 wenzelm@60758  58 text\A note of warning when using @{term"{..  nipkow@15048  61 wenzelm@61955  62 syntax (ASCII)  huffman@36364  63  "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10)  huffman@36364  64  "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" [0, 0, 10] 10)  huffman@36364  65  "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" [0, 0, 10] 10)  huffman@36364  66  "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10)  kleing@14418  67 nipkow@30372  68 syntax (latex output)  wenzelm@62789  69  "_UNION_le" :: "'a \ 'a => 'b set => 'b set" ("(3$$\unbreakable\_ \ _)/ _)" [0, 0, 10] 10)  wenzelm@62789  70  "_UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ < _)/ _)" [0, 0, 10] 10)  wenzelm@62789  71  "_INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ \ _)/ _)" [0, 0, 10] 10)  wenzelm@62789  72  "_INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ < _)/ _)" [0, 0, 10] 10)  kleing@14418  73 wenzelm@61955  74 syntax  wenzelm@61955  75  "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10)  wenzelm@61955  76  "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\_<_./ _)" [0, 0, 10] 10)  wenzelm@61955  77  "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10)  wenzelm@61955  78  "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\_<_./ _)" [0, 0, 10] 10)  wenzelm@61955  79 kleing@14418  80 translations  wenzelm@61955  81  "\i\n. A" \ "\i\{..n}. A"  wenzelm@61955  82  "\i "\i\{..i\n. A" \ "\i\{..n}. A"  wenzelm@61955  84  "\i "\i\{..Various equivalences\  ballarin@13735  88 haftmann@25062  89 lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i { b <..} = { max a b <..}"  hoelzl@50999  126  by auto  hoelzl@50999  127 hoelzl@50999  128 lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \ {..< b} = {..< min a b}"  hoelzl@50999  129  by auto  paulson@13850  130 wenzelm@60758  131 subsection \Logical Equivalences for Set Inclusion and Equality\  paulson@13850  132 lp15@63879  133 lemma atLeast_empty_triv [simp]: "{{}..} = UNIV"  lp15@63879  134  by auto  lp15@63879  135 lp15@63879  136 lemma atMost_UNIV_triv [simp]: "{..UNIV} = UNIV"  lp15@63879  137  by auto  lp15@63879  138 paulson@13850  139 lemma atLeast_subset_iff [iff]:  paulson@15418  140  "(atLeast x \ atLeast y) = (y \ (x::'a::order))"  paulson@15418  141 by (blast intro: order_trans)  paulson@13850  142 paulson@13850  143 lemma atLeast_eq_iff [iff]:  paulson@15418  144  "(atLeast x = atLeast y) = (x = (y::'a::linorder))"  paulson@13850  145 by (blast intro: order_antisym order_trans)  paulson@13850  146 paulson@13850  147 lemma greaterThan_subset_iff [iff]:  paulson@15418  148  "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))"  paulson@15418  149 apply (auto simp add: greaterThan_def)  paulson@15418  150  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  151 done  paulson@13850  152 paulson@13850  153 lemma greaterThan_eq_iff [iff]:  paulson@15418  154  "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"  paulson@15418  155 apply (rule iffI)  paulson@15418  156  apply (erule equalityE)  haftmann@29709  157  apply simp_all  paulson@13850  158 done  paulson@13850  159 paulson@15418  160 lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))"  paulson@13850  161 by (blast intro: order_trans)  paulson@13850  162 paulson@15418  163 lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"  paulson@13850  164 by (blast intro: order_antisym order_trans)  paulson@13850  165 paulson@13850  166 lemma lessThan_subset_iff [iff]:  paulson@15418  167  "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))"  paulson@15418  168 apply (auto simp add: lessThan_def)  paulson@15418  169  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  170 done  paulson@13850  171 paulson@13850  172 lemma lessThan_eq_iff [iff]:  paulson@15418  173  "(lessThan x = lessThan y) = (x = (y::'a::linorder))"  paulson@15418  174 apply (rule iffI)  paulson@15418  175  apply (erule equalityE)  haftmann@29709  176  apply simp_all  ballarin@13735  177 done  ballarin@13735  178 hoelzl@40703  179 lemma lessThan_strict_subset_iff:  hoelzl@40703  180  fixes m n :: "'a::linorder"  hoelzl@40703  181  shows "{.. m < n"  hoelzl@40703  182  by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)  ballarin@13735  183 hoelzl@57448  184 lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \ {b <..} \ b < a"  hoelzl@57448  185  by auto  hoelzl@57448  186 hoelzl@57448  187 lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \ {..< b} \ a < b"  hoelzl@57448  188  by auto  hoelzl@57448  189 hoelzl@62369  190 lemma (in preorder) Ioi_le_Ico: "{a <..} \ {a ..}"  hoelzl@62369  191  by (auto intro: less_imp_le)  hoelzl@62369  192 wenzelm@60758  193 subsection \Two-sided intervals\  ballarin@13735  194 nipkow@24691  195 context ord  nipkow@24691  196 begin  nipkow@24691  197 blanchet@54147  198 lemma greaterThanLessThan_iff [simp]:  haftmann@25062  199  "(i : {l<..The above four lemmas could be declared as iffs. Unfortunately this  haftmann@52729  215 breaks many proofs. Since it only helps blast, it is better to leave them  wenzelm@60758  216 alone.\  nipkow@32436  217 hoelzl@50999  218 lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \ {..< b }"  hoelzl@50999  219  by auto  hoelzl@50999  220 haftmann@66936  221 lemma (in order) atLeast_lessThan_eq_atLeast_atMost_diff:  haftmann@66936  222  "{a..Emptyness, singletons, subset\  nipkow@15554  228 nipkow@24691  229 context order  nipkow@24691  230 begin  nipkow@15554  231 nipkow@32400  232 lemma atLeastatMost_empty[simp]:  nipkow@32400  233  "b < a \ {a..b} = {}"  nipkow@32400  234 by(auto simp: atLeastAtMost_def atLeast_def atMost_def)  nipkow@32400  235 nipkow@32400  236 lemma atLeastatMost_empty_iff[simp]:  nipkow@32400  237  "{a..b} = {} \ (~ a <= b)"  nipkow@32400  238 by auto (blast intro: order_trans)  nipkow@32400  239 nipkow@32400  240 lemma atLeastatMost_empty_iff2[simp]:  nipkow@32400  241  "{} = {a..b} \ (~ a <= b)"  nipkow@32400  242 by auto (blast intro: order_trans)  nipkow@32400  243 nipkow@32400  244 lemma atLeastLessThan_empty[simp]:  nipkow@32400  245  "b <= a \ {a.. (~ a < b)"  nipkow@32400  250 by auto (blast intro: le_less_trans)  nipkow@32400  251 nipkow@32400  252 lemma atLeastLessThan_empty_iff2[simp]:  nipkow@32400  253  "{} = {a.. (~ a < b)"  nipkow@32400  254 by auto (blast intro: le_less_trans)  nipkow@15554  255 nipkow@32400  256 lemma greaterThanAtMost_empty[simp]: "l \ k ==> {k<..l} = {}"  nipkow@17719  257 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)  nipkow@17719  258 nipkow@32400  259 lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ ~ k < l"  nipkow@32400  260 by auto (blast intro: less_le_trans)  nipkow@32400  261 nipkow@32400  262 lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ ~ k < l"  nipkow@32400  263 by auto (blast intro: less_le_trans)  nipkow@32400  264 haftmann@29709  265 lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. {a .. b} = {a}" by simp  hoelzl@36846  272 nipkow@32400  273 lemma atLeastatMost_subset_iff[simp]:  nipkow@32400  274  "{a..b} <= {c..d} \ (~ a <= b) | c <= a & b <= d"  nipkow@32400  275 unfolding atLeastAtMost_def atLeast_def atMost_def  nipkow@32400  276 by (blast intro: order_trans)  nipkow@32400  277 nipkow@32400  278 lemma atLeastatMost_psubset_iff:  nipkow@32400  279  "{a..b} < {c..d} \  nipkow@32400  280  ((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d"  nipkow@39302  281 by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)  nipkow@32400  282 nipkow@51334  283 lemma Icc_eq_Icc[simp]:  nipkow@51334  284  "{l..h} = {l'..h'} = (l=l' \ h=h' \ \ l\h \ \ l'\h')"  nipkow@51334  285 by(simp add: order_class.eq_iff)(auto intro: order_trans)  nipkow@51334  286 hoelzl@36846  287 lemma atLeastAtMost_singleton_iff[simp]:  hoelzl@36846  288  "{a .. b} = {c} \ a = b \ b = c"  hoelzl@36846  289 proof  hoelzl@36846  290  assume "{a..b} = {c}"  wenzelm@53374  291  hence *: "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp  wenzelm@60758  292  with \{a..b} = {c}\ have "c \ a \ b \ c" by auto  wenzelm@53374  293  with * show "a = b \ b = c" by auto  hoelzl@36846  294 qed simp  hoelzl@36846  295 nipkow@51334  296 lemma Icc_subset_Ici_iff[simp]:  nipkow@51334  297  "{l..h} \ {l'..} = (~ l\h \ l\l')"  nipkow@51334  298 by(auto simp: subset_eq intro: order_trans)  nipkow@51334  299 nipkow@51334  300 lemma Icc_subset_Iic_iff[simp]:  nipkow@51334  301  "{l..h} \ {..h'} = (~ l\h \ h\h')"  nipkow@51334  302 by(auto simp: subset_eq intro: order_trans)  nipkow@51334  303 nipkow@51334  304 lemma not_Ici_eq_empty[simp]: "{l..} \ {}"  nipkow@51334  305 by(auto simp: set_eq_iff)  nipkow@51334  306 nipkow@51334  307 lemma not_Iic_eq_empty[simp]: "{..h} \ {}"  nipkow@51334  308 by(auto simp: set_eq_iff)  nipkow@51334  309 nipkow@51334  310 lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric]  nipkow@51334  311 lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric]  nipkow@51334  312 nipkow@24691  313 end  paulson@14485  314 nipkow@51334  315 context no_top  nipkow@51334  316 begin  nipkow@51334  317 nipkow@51334  318 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  319 lemma not_UNIV_le_Icc[simp]: "\ UNIV \ {l..h}"  nipkow@51334  320 using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  321 nipkow@51334  322 lemma not_UNIV_le_Iic[simp]: "\ UNIV \ {..h}"  nipkow@51334  323 using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  324 nipkow@51334  325 lemma not_Ici_le_Icc[simp]: "\ {l..} \ {l'..h'}"  nipkow@51334  326 using gt_ex[of h']  nipkow@51334  327 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  328 nipkow@51334  329 lemma not_Ici_le_Iic[simp]: "\ {l..} \ {..h'}"  nipkow@51334  330 using gt_ex[of h']  nipkow@51334  331 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  332 nipkow@51334  333 end  nipkow@51334  334 nipkow@51334  335 context no_bot  nipkow@51334  336 begin  nipkow@51334  337 nipkow@51334  338 lemma not_UNIV_le_Ici[simp]: "\ UNIV \ {l..}"  nipkow@51334  339 using lt_ex[of l] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  340 nipkow@51334  341 lemma not_Iic_le_Icc[simp]: "\ {..h} \ {l'..h'}"  nipkow@51334  342 using lt_ex[of l']  nipkow@51334  343 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  344 nipkow@51334  345 lemma not_Iic_le_Ici[simp]: "\ {..h} \ {l'..}"  nipkow@51334  346 using lt_ex[of l']  nipkow@51334  347 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  348 nipkow@51334  349 end  nipkow@51334  350 nipkow@51334  351 nipkow@51334  352 context no_top  nipkow@51334  353 begin  nipkow@51334  354 nipkow@51334  355 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  356 lemma not_UNIV_eq_Icc[simp]: "\ UNIV = {l'..h'}"  nipkow@51334  357 using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  358 nipkow@51334  359 lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric]  nipkow@51334  360 nipkow@51334  361 lemma not_UNIV_eq_Iic[simp]: "\ UNIV = {..h'}"  nipkow@51334  362 using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  363 nipkow@51334  364 lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric]  nipkow@51334  365 nipkow@51334  366 lemma not_Icc_eq_Ici[simp]: "\ {l..h} = {l'..}"  nipkow@51334  367 unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast  nipkow@51334  368 nipkow@51334  369 lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric]  nipkow@51334  370 nipkow@51334  371 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  372 lemma not_Iic_eq_Ici[simp]: "\ {..h} = {l'..}"  nipkow@51334  373 using not_Ici_le_Iic[of l' h] by blast  nipkow@51334  374 nipkow@51334  375 lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric]  nipkow@51334  376 nipkow@51334  377 end  nipkow@51334  378 nipkow@51334  379 context no_bot  nipkow@51334  380 begin  nipkow@51334  381 nipkow@51334  382 lemma not_UNIV_eq_Ici[simp]: "\ UNIV = {l'..}"  nipkow@51334  383 using lt_ex[of l'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  384 nipkow@51334  385 lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric]  nipkow@51334  386 nipkow@51334  387 lemma not_Icc_eq_Iic[simp]: "\ {l..h} = {..h'}"  nipkow@51334  388 unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast  nipkow@51334  389 nipkow@51334  390 lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric]  nipkow@51334  391 nipkow@51334  392 end  nipkow@51334  393 nipkow@51334  394 hoelzl@53216  395 context dense_linorder  hoelzl@42891  396 begin  hoelzl@42891  397 hoelzl@42891  398 lemma greaterThanLessThan_empty_iff[simp]:  hoelzl@42891  399  "{ a <..< b } = {} \ b \ a"  hoelzl@42891  400  using dense[of a b] by (cases "a < b") auto  hoelzl@42891  401 hoelzl@42891  402 lemma greaterThanLessThan_empty_iff2[simp]:  hoelzl@42891  403  "{} = { a <..< b } \ b \ a"  hoelzl@42891  404  using dense[of a b] by (cases "a < b") auto  hoelzl@42891  405 hoelzl@42901  406 lemma atLeastLessThan_subseteq_atLeastAtMost_iff:  hoelzl@42901  407  "{a ..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  408  using dense[of "max a d" "b"]  hoelzl@42901  409  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  410 hoelzl@42901  411 lemma greaterThanAtMost_subseteq_atLeastAtMost_iff:  hoelzl@42901  412  "{a <.. b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  413  using dense[of "a" "min c b"]  hoelzl@42901  414  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  415 hoelzl@42901  416 lemma greaterThanLessThan_subseteq_atLeastAtMost_iff:  hoelzl@42901  417  "{a <..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  418  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@42901  419  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  420 hoelzl@43657  421 lemma atLeastAtMost_subseteq_atLeastLessThan_iff:  hoelzl@43657  422  "{a .. b} \ { c ..< d } \ (a \ b \ c \ a \ b < d)"  hoelzl@43657  423  using dense[of "max a d" "b"]  hoelzl@43657  424  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@62369  425 eberlm@61524  426 lemma greaterThanLessThan_subseteq_greaterThanLessThan:  eberlm@61524  427  "{a <..< b} \ {c <..< d} \ (a < b \ a \ c \ b \ d)"  eberlm@61524  428  using dense[of "a" "min c b"] dense[of "max a d" "b"]  eberlm@61524  429  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  430 hoelzl@43657  431 lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:  hoelzl@43657  432  "{a <.. b} \ { c ..< d } \ (a < b \ c \ a \ b < d)"  hoelzl@43657  433  using dense[of "a" "min c b"]  hoelzl@43657  434  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  435 hoelzl@43657  436 lemma greaterThanLessThan_subseteq_atLeastLessThan_iff:  hoelzl@43657  437  "{a <..< b} \ { c ..< d } \ (a < b \ c \ a \ b \ d)"  hoelzl@43657  438  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@43657  439  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  440 hoelzl@56328  441 lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff:  hoelzl@56328  442  "{a <..< b} \ { c <.. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@56328  443  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@56328  444  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@56328  445 hoelzl@42891  446 end  hoelzl@42891  447 hoelzl@51329  448 context no_top  hoelzl@51329  449 begin  hoelzl@51329  450 nipkow@51334  451 lemma greaterThan_non_empty[simp]: "{x <..} \ {}"  hoelzl@51329  452  using gt_ex[of x] by auto  hoelzl@51329  453 hoelzl@51329  454 end  hoelzl@51329  455 hoelzl@51329  456 context no_bot  hoelzl@51329  457 begin  hoelzl@51329  458 nipkow@51334  459 lemma lessThan_non_empty[simp]: "{..< x} \ {}"  hoelzl@51329  460  using lt_ex[of x] by auto  hoelzl@51329  461 hoelzl@51329  462 end  hoelzl@51329  463 nipkow@32408  464 lemma (in linorder) atLeastLessThan_subset_iff:  nipkow@32408  465  "{a.. b <= a | c<=a & b<=d"  nipkow@32408  466 apply (auto simp:subset_eq Ball_def)  nipkow@32408  467 apply(frule_tac x=a in spec)  nipkow@32408  468 apply(erule_tac x=d in allE)  nipkow@32408  469 apply (simp add: less_imp_le)  nipkow@32408  470 done  nipkow@32408  471 hoelzl@40703  472 lemma atLeastLessThan_inj:  hoelzl@40703  473  fixes a b c d :: "'a::linorder"  hoelzl@40703  474  assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"  hoelzl@40703  475  shows "a = c" "b = d"  hoelzl@40703  476 using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+  hoelzl@40703  477 hoelzl@40703  478 lemma atLeastLessThan_eq_iff:  hoelzl@40703  479  fixes a b c d :: "'a::linorder"  hoelzl@40703  480  assumes "a < b" "c < d"  hoelzl@40703  481  shows "{a ..< b} = {c ..< d} \ a = c \ b = d"  hoelzl@40703  482  using atLeastLessThan_inj assms by auto  hoelzl@40703  483 hoelzl@57447  484 lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \ (b \ a \ d \ c) \ a = c \ b = d"  hoelzl@57447  485  by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le)  hoelzl@57447  486 hoelzl@57447  487 lemma (in order) Iio_Int_singleton: "{.. {x} = (if x < k then {x} else {})"  hoelzl@57447  488  by auto  hoelzl@57447  489 hoelzl@57447  490 lemma (in linorder) Ioc_subset_iff: "{a<..b} \ {c<..d} \ (b \ a \ c \ a \ b \ d)"  hoelzl@57447  491  by (auto simp: subset_eq Ball_def) (metis less_le not_less)  hoelzl@57447  492 haftmann@52729  493 lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \ x = bot"  nipkow@51334  494 by (auto simp: set_eq_iff intro: le_bot)  hoelzl@51328  495 haftmann@52729  496 lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \ x = top"  nipkow@51334  497 by (auto simp: set_eq_iff intro: top_le)  hoelzl@51328  498 nipkow@51334  499 lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff:  nipkow@51334  500  "{x..y} = UNIV \ (x = bot \ y = top)"  nipkow@51334  501 by (auto simp: set_eq_iff intro: top_le le_bot)  hoelzl@51328  502 hoelzl@56949  503 lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \ n = bot"  hoelzl@56949  504  by (auto simp: set_eq_iff not_less le_bot)  hoelzl@56949  505 hoelzl@56949  506 lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \ n = 0"  hoelzl@56949  507  by (simp add: Iio_eq_empty_iff bot_nat_def)  hoelzl@56949  508 noschinl@58970  509 lemma mono_image_least:  noschinl@58970  510  assumes f_mono: "mono f" and f_img: "f  {m ..< n} = {m' ..< n'}" "m < n"  noschinl@58970  511  shows "f m = m'"  noschinl@58970  512 proof -  noschinl@58970  513  from f_img have "{m' ..< n'} \ {}"  noschinl@58970  514  by (metis atLeastLessThan_empty_iff image_is_empty)  noschinl@58970  515  with f_img have "m' \ f  {m ..< n}" by auto  noschinl@58970  516  then obtain k where "f k = m'" "m \ k" by auto  noschinl@58970  517  moreover have "m' \ f m" using f_img by auto  noschinl@58970  518  ultimately show "f m = m'"  noschinl@58970  519  using f_mono by (auto elim: monoE[where x=m and y=k])  noschinl@58970  520 qed  noschinl@58970  521 hoelzl@51328  522 wenzelm@60758  523 subsection \Infinite intervals\  hoelzl@56328  524 hoelzl@56328  525 context dense_linorder  hoelzl@56328  526 begin  hoelzl@56328  527 hoelzl@56328  528 lemma infinite_Ioo:  hoelzl@56328  529  assumes "a < b"  hoelzl@56328  530  shows "\ finite {a<.. {}"  wenzelm@60758  534  using \a < b\ by auto  hoelzl@56328  535  ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b"  hoelzl@56328  536  using Max_in[of "{a <..< b}"] by auto  hoelzl@56328  537  then obtain x where "Max {a <..< b} < x" "x < b"  hoelzl@56328  538  using dense[of "Max {a<.. {a <..< b}"  wenzelm@60758  540  using \a < Max {a <..< b}\ by auto  hoelzl@56328  541  then have "x \ Max {a <..< b}"  hoelzl@56328  542  using fin by auto  wenzelm@60758  543  with \Max {a <..< b} < x\ show False by auto  hoelzl@56328  544 qed  hoelzl@56328  545 hoelzl@56328  546 lemma infinite_Icc: "a < b \ \ finite {a .. b}"  hoelzl@56328  547  using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b]  hoelzl@56328  548  by (auto dest: finite_subset)  hoelzl@56328  549 hoelzl@56328  550 lemma infinite_Ico: "a < b \ \ finite {a ..< b}"  hoelzl@56328  551  using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b]  hoelzl@56328  552  by (auto dest: finite_subset)  hoelzl@56328  553 hoelzl@56328  554 lemma infinite_Ioc: "a < b \ \ finite {a <.. b}"  hoelzl@56328  555  using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b]  hoelzl@56328  556  by (auto dest: finite_subset)  hoelzl@56328  557 lp15@63967  558 lemma infinite_Ioo_iff [simp]: "infinite {a<.. a < b"  lp15@63967  559  using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioo)  lp15@63967  560 lp15@63967  561 lemma infinite_Icc_iff [simp]: "infinite {a .. b} \ a < b"  lp15@63967  562  using not_less_iff_gr_or_eq by (fastforce simp: infinite_Icc)  lp15@63967  563 lp15@63967  564 lemma infinite_Ico_iff [simp]: "infinite {a.. a < b"  lp15@63967  565  using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ico)  lp15@63967  566 lp15@63967  567 lemma infinite_Ioc_iff [simp]: "infinite {a<..b} \ a < b"  lp15@63967  568  using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioc)  lp15@63967  569 hoelzl@56328  570 end  hoelzl@56328  571 hoelzl@56328  572 lemma infinite_Iio: "\ finite {..< a :: 'a :: {no_bot, linorder}}"  hoelzl@56328  573 proof  hoelzl@56328  574  assume "finite {..< a}"  hoelzl@56328  575  then have *: "\x. x < a \ Min {..< a} \ x"  hoelzl@56328  576  by auto  hoelzl@56328  577  obtain x where "x < a"  hoelzl@56328  578  using lt_ex by auto  hoelzl@56328  579 hoelzl@56328  580  obtain y where "y < Min {..< a}"  hoelzl@56328  581  using lt_ex by auto  hoelzl@56328  582  also have "Min {..< a} \ x"  wenzelm@60758  583  using \x < a\ by fact  wenzelm@60758  584  also note \x < a\  hoelzl@56328  585  finally have "Min {..< a} \ y"  hoelzl@56328  586  by fact  wenzelm@60758  587  with \y < Min {..< a}\ show False by auto  hoelzl@56328  588 qed  hoelzl@56328  589 hoelzl@56328  590 lemma infinite_Iic: "\ finite {.. a :: 'a :: {no_bot, linorder}}"  hoelzl@56328  591  using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"]  hoelzl@56328  592  by (auto simp: subset_eq less_imp_le)  hoelzl@56328  593 hoelzl@56328  594 lemma infinite_Ioi: "\ finite {a :: 'a :: {no_top, linorder} <..}"  hoelzl@56328  595 proof  hoelzl@56328  596  assume "finite {a <..}"  hoelzl@56328  597  then have *: "\x. a < x \ x \ Max {a <..}"  hoelzl@56328  598  by auto  hoelzl@56328  599 hoelzl@56328  600  obtain y where "Max {a <..} < y"  hoelzl@56328  601  using gt_ex by auto  hoelzl@56328  602 wenzelm@63540  603  obtain x where x: "a < x"  hoelzl@56328  604  using gt_ex by auto  wenzelm@63540  605  also from x have "x \ Max {a <..}"  hoelzl@56328  606  by fact  wenzelm@60758  607  also note \Max {a <..} < y\  hoelzl@56328  608  finally have "y \ Max { a <..}"  hoelzl@56328  609  by fact  wenzelm@60758  610  with \Max {a <..} < y\ show False by auto  hoelzl@56328  611 qed  hoelzl@56328  612 hoelzl@56328  613 lemma infinite_Ici: "\ finite {a :: 'a :: {no_top, linorder} ..}"  hoelzl@56328  614  using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"]  hoelzl@56328  615  by (auto simp: subset_eq less_imp_le)  hoelzl@56328  616 wenzelm@60758  617 subsubsection \Intersection\  nipkow@32456  618 nipkow@32456  619 context linorder  nipkow@32456  620 begin  nipkow@32456  621 nipkow@32456  622 lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"  nipkow@32456  623 by auto  nipkow@32456  624 nipkow@32456  625 lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"  nipkow@32456  626 by auto  nipkow@32456  627 nipkow@32456  628 lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"  nipkow@32456  629 by auto  nipkow@32456  630 nipkow@32456  631 lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"  nipkow@32456  632 by auto  nipkow@32456  633 nipkow@32456  634 lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"  nipkow@32456  635 by auto  nipkow@32456  636 nipkow@32456  637 lemma Int_atLeastLessThan[simp]: "{a.. {..b} = {.. min a b}"  hoelzl@50417  647  by (auto simp: min_def)  hoelzl@50417  648 hoelzl@57447  649 lemma Ioc_disjoint: "{a<..b} \ {c<..d} = {} \ b \ a \ d \ c \ b \ c \ d \ a"  wenzelm@63092  650  by auto  hoelzl@57447  651 nipkow@32456  652 end  nipkow@32456  653 hoelzl@51329  654 context complete_lattice  hoelzl@51329  655 begin  hoelzl@51329  656 hoelzl@51329  657 lemma  hoelzl@51329  658  shows Sup_atLeast[simp]: "Sup {x ..} = top"  hoelzl@51329  659  and Sup_greaterThanAtLeast[simp]: "x < top \ Sup {x <..} = top"  hoelzl@51329  660  and Sup_atMost[simp]: "Sup {.. y} = y"  hoelzl@51329  661  and Sup_atLeastAtMost[simp]: "x \ y \ Sup { x .. y} = y"  hoelzl@51329  662  and Sup_greaterThanAtMost[simp]: "x < y \ Sup { x <.. y} = y"  hoelzl@51329  663  by (auto intro!: Sup_eqI)  hoelzl@51329  664 hoelzl@51329  665 lemma  hoelzl@51329  666  shows Inf_atMost[simp]: "Inf {.. x} = bot"  hoelzl@51329  667  and Inf_atMostLessThan[simp]: "top < x \ Inf {..< x} = bot"  hoelzl@51329  668  and Inf_atLeast[simp]: "Inf {x ..} = x"  hoelzl@51329  669  and Inf_atLeastAtMost[simp]: "x \ y \ Inf { x .. y} = x"  hoelzl@51329  670  and Inf_atLeastLessThan[simp]: "x < y \ Inf { x ..< y} = x"  hoelzl@51329  671  by (auto intro!: Inf_eqI)  hoelzl@51329  672 hoelzl@51329  673 end  hoelzl@51329  674 hoelzl@51329  675 lemma  hoelzl@53216  676  fixes x y :: "'a :: {complete_lattice, dense_linorder}"  hoelzl@51329  677  shows Sup_lessThan[simp]: "Sup {..< y} = y"  hoelzl@51329  678  and Sup_atLeastLessThan[simp]: "x < y \ Sup { x ..< y} = y"  hoelzl@51329  679  and Sup_greaterThanLessThan[simp]: "x < y \ Sup { x <..< y} = y"  hoelzl@51329  680  and Inf_greaterThan[simp]: "Inf {x <..} = x"  hoelzl@51329  681  and Inf_greaterThanAtMost[simp]: "x < y \ Inf { x <.. y} = x"  hoelzl@51329  682  and Inf_greaterThanLessThan[simp]: "x < y \ Inf { x <..< y} = x"  hoelzl@51329  683  by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded)  nipkow@32456  684 wenzelm@60758  685 subsection \Intervals of natural numbers\  paulson@14485  686 wenzelm@60758  687 subsubsection \The Constant @{term lessThan}\  paulson@15047  688 paulson@14485  689 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"  paulson@14485  690 by (simp add: lessThan_def)  paulson@14485  691 paulson@14485  692 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"  paulson@14485  693 by (simp add: lessThan_def less_Suc_eq, blast)  paulson@14485  694 wenzelm@60758  695 text \The following proof is convenient in induction proofs where  hoelzl@39072  696 new elements get indices at the beginning. So it is used to transform  wenzelm@60758  697 @{term "{..  hoelzl@39072  698 hoelzl@59000  699 lemma zero_notin_Suc_image: "0 \ Suc  A"  hoelzl@59000  700  by auto  hoelzl@59000  701 hoelzl@39072  702 lemma lessThan_Suc_eq_insert_0: "{..The Constant @{term greaterThan}\  paulson@15047  715 lp15@65273  716 lemma greaterThan_0: "greaterThan 0 = range Suc"  paulson@14485  717 apply (simp add: greaterThan_def)  paulson@14485  718 apply (blast dest: gr0_conv_Suc [THEN iffD1])  paulson@14485  719 done  paulson@14485  720 paulson@14485  721 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"  paulson@14485  722 apply (simp add: greaterThan_def)  paulson@14485  723 apply (auto elim: linorder_neqE)  paulson@14485  724 done  paulson@14485  725 paulson@14485  726 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"  paulson@14485  727 by blast  paulson@14485  728 wenzelm@60758  729 subsubsection \The Constant @{term atLeast}\  paulson@15047  730 paulson@14485  731 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"  paulson@14485  732 by (unfold atLeast_def UNIV_def, simp)  paulson@14485  733 paulson@14485  734 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"  paulson@14485  735 apply (simp add: atLeast_def)  paulson@14485  736 apply (simp add: Suc_le_eq)  paulson@14485  737 apply (simp add: order_le_less, blast)  paulson@14485  738 done  paulson@14485  739 paulson@14485  740 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"  paulson@14485  741  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)  paulson@14485  742 paulson@14485  743 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"  paulson@14485  744 by blast  paulson@14485  745 wenzelm@60758  746 subsubsection \The Constant @{term atMost}\  paulson@15047  747 paulson@14485  748 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"  paulson@14485  749 by (simp add: atMost_def)  paulson@14485  750 paulson@14485  751 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"  paulson@14485  752 apply (simp add: atMost_def)  paulson@14485  753 apply (simp add: less_Suc_eq order_le_less, blast)  paulson@14485  754 done  paulson@14485  755 paulson@14485  756 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"  paulson@14485  757 by blast  paulson@14485  758 wenzelm@60758  759 subsubsection \The Constant @{term atLeastLessThan}\  paulson@15047  760 wenzelm@60758  761 text\The orientation of the following 2 rules is tricky. The lhs is  nipkow@24449  762 defined in terms of the rhs. Hence the chosen orientation makes sense  nipkow@24449  763 in this theory --- the reverse orientation complicates proofs (eg  nipkow@24449  764 nontermination). But outside, when the definition of the lhs is rarely  nipkow@24449  765 used, the opposite orientation seems preferable because it reduces a  wenzelm@60758  766 specific concept to a more general one.\  nipkow@28068  767 haftmann@63417  768 lemma atLeast0LessThan [code_abbrev]: "{0::nat..The Constant @{term atLeastAtMost}\  haftmann@63417  795 haftmann@63417  796 lemma atLeast0_atMost_Suc:  haftmann@63417  797  "{0..Suc n} = insert (Suc n) {0..n}"  haftmann@63417  798  by (simp add: atLeast0AtMost atMost_Suc)  haftmann@63417  799 haftmann@63417  800 lemma atLeast0_atMost_Suc_eq_insert_0:  haftmann@63417  801  "{0..Suc n} = insert 0 (Suc  {0..n})"  haftmann@63417  802  by (simp add: atLeast0AtMost Iic_Suc_eq_insert_0)  haftmann@63417  803 haftmann@63417  804 wenzelm@60758  805 subsubsection \Intervals of nats with @{term Suc}\  paulson@15047  806 wenzelm@60758  807 text\Not a simprule because the RHS is too messy.\  paulson@15047  808 lemma atLeastLessThanSuc:  paulson@15047  809  "{m.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  833 by (auto simp add: atLeastAtMost_def)  nipkow@15554  834 noschinl@45932  835 lemma atLeastAtMost_insertL: "m \ n \ insert m {Suc m..n} = {m ..n}"  noschinl@45932  836 by auto  noschinl@45932  837 wenzelm@60758  838 text \The analogous result is useful on @{typ int}:\  kleing@43157  839 (* here, because we don't have an own int section *)  kleing@43157  840 lemma atLeastAtMostPlus1_int_conv:  kleing@43157  841  "m <= 1+n \ {m..1+n} = insert (1+n) {m..n::int}"  kleing@43157  842  by (auto intro: set_eqI)  kleing@43157  843 paulson@33044  844 lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j..Intervals and numerals\  lp15@57113  851 wenzelm@61799  852 lemma lessThan_nat_numeral: \\Evaluation for specific numerals\  lp15@57113  853  "lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))"  lp15@57113  854  by (simp add: numeral_eq_Suc lessThan_Suc)  lp15@57113  855 wenzelm@61799  856 lemma atMost_nat_numeral: \\Evaluation for specific numerals\  lp15@57113  857  "atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))"  lp15@57113  858  by (simp add: numeral_eq_Suc atMost_Suc)  lp15@57113  859 wenzelm@61799  860 lemma atLeastLessThan_nat_numeral: \\Evaluation for specific numerals\  hoelzl@62369  861  "atLeastLessThan m (numeral k :: nat) =  lp15@57113  862  (if m \ (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k))  lp15@57113  863  else {})"  lp15@57113  864  by (simp add: numeral_eq_Suc atLeastLessThanSuc)  lp15@57113  865 haftmann@66936  866 wenzelm@60758  867 subsubsection \Image\  nipkow@16733  868 haftmann@66936  869 context linordered_semidom  haftmann@66936  870 begin  haftmann@66936  871 haftmann@66936  872 lemma image_add_atLeast_atMost [simp]:  haftmann@66936  873  "plus k  {i..j} = {i + k..j + k}" (is "?A = ?B")  nipkow@16733  874 proof  haftmann@66936  875  show "?A \ ?B"  haftmann@66936  876  by (auto simp add: ac_simps)  nipkow@16733  877 next  nipkow@16733  878  show "?B \ ?A"  nipkow@16733  879  proof  haftmann@66936  880  fix n  haftmann@66936  881  assume "n \ ?B"  haftmann@66936  882  then have "i \ n - k"  haftmann@66936  883  by (simp add: add_le_imp_le_diff)  haftmann@66936  884  have "n = n - k + k"  lp15@60615  885  proof -  haftmann@66936  886  from \n \ ?B\ have "n = n - (i + k) + (i + k)"  haftmann@66936  887  by simp  haftmann@66936  888  also have "\ = n - k - i + i + k"  haftmann@66936  889  by (simp add: algebra_simps)  haftmann@66936  890  also have "\ = n - k + k"  haftmann@66936  891  using \i \ n - k\ by simp  haftmann@66936  892  finally show ?thesis .  lp15@60615  893  qed  haftmann@66936  894  moreover have "n - k \ {i..j}"  haftmann@66936  895  using \n \ ?B\  haftmann@66936  896  by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le)  haftmann@66936  897  ultimately show "n \ ?A"  haftmann@66936  898  by (simp add: ac_simps)  nipkow@16733  899  qed  nipkow@16733  900 qed  nipkow@16733  901 haftmann@66936  902 lemma image_add_atLeast_atMost' [simp]:  haftmann@66936  903  "(\n. n + k)  {i..j} = {i + k..j + k}"  haftmann@66936  904  by (simp add: add.commute [of _ k])  haftmann@66936  905 haftmann@66936  906 lemma image_add_atLeast_lessThan [simp]:  haftmann@66936  907  "plus k  {i..n. n + k)  {i..0" shows "(op * d  {a..b}) = {d*a..d*b}"  lp15@60809  943  using assms  lp15@60809  944  by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])  lp15@60809  945 lp15@60809  946 lemma image_affinity_atLeastAtMost:  lp15@60809  947  fixes c :: "'a::linordered_field"  lp15@60809  948  shows "((\x. m*x + c)  {a..b}) = (if {a..b}={} then {}  lp15@60809  949  else if 0 \ m then {m*a + c .. m *b + c}  lp15@60809  950  else {m*b + c .. m*a + c})"  lp15@60809  951  apply (case_tac "m=0", auto simp: mult_le_cancel_left)  lp15@60809  952  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)  lp15@60809  953  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)  lp15@60809  954  done  lp15@60809  955 lp15@60809  956 lemma image_affinity_atLeastAtMost_diff:  lp15@60809  957  fixes c :: "'a::linordered_field"  lp15@60809  958  shows "((\x. m*x - c)  {a..b}) = (if {a..b}={} then {}  lp15@60809  959  else if 0 \ m then {m*a - c .. m*b - c}  lp15@60809  960  else {m*b - c .. m*a - c})"  lp15@60809  961  using image_affinity_atLeastAtMost [of m "-c" a b]  lp15@60809  962  by simp  lp15@60809  963 paulson@61204  964 lemma image_affinity_atLeastAtMost_div:  paulson@61204  965  fixes c :: "'a::linordered_field"  paulson@61204  966  shows "((\x. x/m + c)  {a..b}) = (if {a..b}={} then {}  paulson@61204  967  else if 0 \ m then {a/m + c .. b/m + c}  paulson@61204  968  else {b/m + c .. a/m + c})"  paulson@61204  969  using image_affinity_atLeastAtMost [of "inverse m" c a b]  paulson@61204  970  by (simp add: field_class.field_divide_inverse algebra_simps)  hoelzl@62369  971 lp15@60809  972 lemma image_affinity_atLeastAtMost_div_diff:  lp15@60809  973  fixes c :: "'a::linordered_field"  lp15@60809  974  shows "((\x. x/m - c)  {a..b}) = (if {a..b}={} then {}  lp15@60809  975  else if 0 \ m then {a/m - c .. b/m - c}  lp15@60809  976  else {b/m - c .. a/m - c})"  lp15@60809  977  using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]  lp15@60809  978  by (simp add: field_class.field_divide_inverse algebra_simps)  lp15@60809  979 haftmann@63365  980 lemma atLeast1_lessThan_eq_remove0:  haftmann@63365  981  "{Suc 0..i. i - c)  {x ..< y} =  hoelzl@37664  998  (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"  hoelzl@37664  999  (is "_ = ?right")  hoelzl@37664  1000 proof safe  hoelzl@37664  1001  fix a assume a: "a \ ?right"  hoelzl@37664  1002  show "a \ (\i. i - c)  {x ..< y}"  hoelzl@37664  1003  proof cases  hoelzl@37664  1004  assume "c < y" with a show ?thesis  hoelzl@37664  1005  by (auto intro!: image_eqI[of _ _ "a + c"])  hoelzl@37664  1006  next  hoelzl@37664  1007  assume "\ c < y" with a show ?thesis  nipkow@62390  1008  by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)  hoelzl@37664  1009  qed  hoelzl@37664  1010 qed auto  hoelzl@37664  1011 haftmann@66936  1012 lemma image_int_atLeast_lessThan:  haftmann@66936  1013  "int  {a.. uminus  {x<..}"  hoelzl@35580  1031  by (rule imageI) (simp add: *)  hoelzl@35580  1032  thus "y \ uminus  {x<..}" by simp  hoelzl@35580  1033 next  hoelzl@35580  1034  fix y assume "y \ -x"  hoelzl@35580  1035  have "- (-y) \ uminus  {x..}"  wenzelm@60758  1036  by (rule imageI) (insert \y \ -x\[THEN le_imp_neg_le], simp)  hoelzl@35580  1037  thus "y \ uminus  {x..}" by simp  hoelzl@35580  1038 qed simp_all  hoelzl@35580  1039 hoelzl@35580  1040 lemma  hoelzl@35580  1041  fixes x :: 'a  hoelzl@35580  1042  shows image_uminus_lessThan[simp]: "uminus  {..Finiteness\  paulson@14485  1063 nipkow@15045  1064 lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..A bounded set of natural numbers is finite.\  paulson@14485  1087 lemma bounded_nat_set_is_finite:  nipkow@24853  1088  "(ALL i:N. i < (n::nat)) ==> finite N"  nipkow@28068  1089 apply (rule finite_subset)  nipkow@28068  1090  apply (rule_tac [2] finite_lessThan, auto)  nipkow@28068  1091 done  nipkow@28068  1092 wenzelm@60758  1093 text \A set of natural numbers is finite iff it is bounded.\  nipkow@31044  1094 lemma finite_nat_set_iff_bounded:  nipkow@31044  1095  "finite(N::nat set) = (EX m. ALL n:N. n?F\, simplified less_Suc_eq_le[symmetric]] by blast  nipkow@31044  1099 next  wenzelm@60758  1100  assume ?B show ?F using \?B\ by(blast intro:bounded_nat_set_is_finite)  nipkow@31044  1101 qed  nipkow@31044  1102 nipkow@31044  1103 lemma finite_nat_set_iff_bounded_le:  nipkow@31044  1104  "finite(N::nat set) = (EX m. ALL n:N. n<=m)"  nipkow@31044  1105 apply(simp add:finite_nat_set_iff_bounded)  nipkow@31044  1106 apply(blast dest:less_imp_le_nat le_imp_less_Suc)  nipkow@31044  1107 done  nipkow@31044  1108 nipkow@28068  1109 lemma finite_less_ub:  nipkow@28068  1110  "!!f::nat=>nat. (!!n. n \ f n) ==> finite {n. f n \ u}"  nipkow@28068  1111 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)  paulson@14485  1112 lp15@64773  1113 lemma bounded_Max_nat:  lp15@64773  1114  fixes P :: "nat \ bool"  lp15@64773  1115  assumes x: "P x" and M: "\x. P x \ x \ M"  lp15@64773  1116  obtains m where "P m" "\x. P x \ x \ m"  lp15@64773  1117 proof -  lp15@64773  1118  have "finite {x. P x}"  lp15@64773  1119  using M finite_nat_set_iff_bounded_le by auto  lp15@64773  1120  then have "Max {x. P x} \ {x. P x}"  lp15@64773  1121  using Max_in x by auto  lp15@64773  1122  then show ?thesis  lp15@64773  1123  by (simp add: \finite {x. P x}\ that)  lp15@64773  1124 qed  lp15@64773  1125 hoelzl@56328  1126 wenzelm@60758  1127 text\Any subset of an interval of natural numbers the size of the  wenzelm@60758  1128 subset is exactly that interval.\  nipkow@24853  1129 nipkow@24853  1130 lemma subset_card_intvl_is_intvl:  blanchet@55085  1131  assumes "A \ {k.. A" by auto  blanchet@55085  1141  with insert have "A <= {k..Proving Inclusions and Equalities between Unions\  paulson@32596  1152 nipkow@36755  1153 lemma UN_le_eq_Un0:  nipkow@36755  1154  "(\i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B")  nipkow@36755  1155 proof  nipkow@36755  1156  show "?A <= ?B"  nipkow@36755  1157  proof  nipkow@36755  1158  fix x assume "x : ?A"  nipkow@36755  1159  then obtain i where i: "i\n" "x : M i" by auto  nipkow@36755  1160  show "x : ?B"  nipkow@36755  1161  proof(cases i)  nipkow@36755  1162  case 0 with i show ?thesis by simp  nipkow@36755  1163  next  nipkow@36755  1164  case (Suc j) with i show ?thesis by auto  nipkow@36755  1165  qed  nipkow@36755  1166  qed  nipkow@36755  1167 next  wenzelm@63171  1168  show "?B <= ?A" by fastforce  nipkow@36755  1169 qed  nipkow@36755  1170 nipkow@36755  1171 lemma UN_le_add_shift:  nipkow@36755  1172  "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B")  nipkow@36755  1173 proof  nipkow@44890  1174  show "?A <= ?B" by fastforce  nipkow@36755  1175 next  nipkow@36755  1176  show "?B <= ?A"  nipkow@36755  1177  proof  nipkow@36755  1178  fix x assume "x : ?B"  nipkow@36755  1179  then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto  nipkow@36755  1180  hence "i-k\n & x : M((i-k)+k)" by auto  nipkow@36755  1181  thus "x : ?A" by blast  nipkow@36755  1182  qed  nipkow@36755  1183 qed  nipkow@36755  1184 hoelzl@62369  1185 lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)"  hoelzl@62369  1186  by (auto simp add: atLeast0LessThan)  paulson@32596  1187 haftmann@62343  1188 lemma UN_finite_subset:  haftmann@62343  1189  "(\n::nat. (\i\{0.. C) \ (\n. A n) \ C"  paulson@32596  1190  by (subst UN_UN_finite_eq [symmetric]) blast  paulson@32596  1191 hoelzl@62369  1192 lemma UN_finite2_subset:  haftmann@62343  1193  assumes "\n::nat. (\i\{0.. (\i\{0..n. A n) \ (\n. B n)"  haftmann@62343  1195 proof (rule UN_finite_subset, rule)  haftmann@62343  1196  fix n and a  haftmann@62343  1197  from assms have "(\i\{0.. (\i\{0.. (\i\{0.. (\i\{0.. (\i. B i)" by (auto simp add: UN_UN_finite_eq)  haftmann@62343  1201 qed  paulson@32596  1202 paulson@32596  1203 lemma UN_finite2_eq:  haftmann@62343  1204  "(\n::nat. (\i\{0..i\{0..  haftmann@62343  1205  (\n. A n) = (\n. B n)"  paulson@33044  1206  apply (rule subset_antisym)  paulson@33044  1207  apply (rule UN_finite2_subset, blast)  haftmann@62343  1208  apply (rule UN_finite2_subset [where k=k])  haftmann@62343  1209  apply (force simp add: atLeastLessThan_add_Un [of 0])  haftmann@62343  1210  done  paulson@32596  1211 paulson@32596  1212 wenzelm@60758  1213 subsubsection \Cardinality\  paulson@14485  1214 nipkow@15045  1215 lemma card_lessThan [simp]: "card {.. {0.. {0..n}"  wenzelm@63915  1252  shows "finite N"  haftmann@63417  1253  using assms finite_atLeastAtMost by (rule finite_subset)  haftmann@63365  1254 nipkow@26105  1255 lemma ex_bij_betw_nat_finite:  nipkow@26105  1256  "finite M \ \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  1267 apply(drule ex_bij_betw_finite_nat)  nipkow@31438  1268 apply(drule ex_bij_betw_nat_finite)  nipkow@31438  1269 apply(auto intro!:bij_betw_trans)  nipkow@31438  1270 done  nipkow@31438  1271 nipkow@31438  1272 lemma ex_bij_betw_nat_finite_1:  nipkow@31438  1273  "finite M \ \h. bij_betw h {1 .. card M} M"  nipkow@31438  1274 by (rule finite_same_card_bij) auto  nipkow@31438  1275 hoelzl@40703  1276 lemma bij_betw_iff_card:  lp15@63114  1277  assumes "finite A" "finite B"  lp15@63114  1278  shows "(\f. bij_betw f A B) \ (card A = card B)"  lp15@63114  1279 proof  lp15@63114  1280  assume "card A = card B"  lp15@63114  1281  moreover obtain f where "bij_betw f A {0 ..< card A}"  lp15@63114  1282  using assms ex_bij_betw_finite_nat by blast  hoelzl@40703  1283  moreover obtain g where "bij_betw g {0 ..< card B} B"  lp15@63114  1284  using assms ex_bij_betw_nat_finite by blast  hoelzl@40703  1285  ultimately have "bij_betw (g o f) A B"  lp15@63114  1286  by (auto simp: bij_betw_trans)  hoelzl@40703  1287  thus "(\f. bij_betw f A B)" by blast  lp15@63114  1288 qed (auto simp: bij_betw_same_card)  hoelzl@40703  1289 hoelzl@40703  1290 lemma inj_on_iff_card_le:  hoelzl@40703  1291  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  1292  shows "(\f. inj_on f A \ f  A \ B) = (card A \ card B)"  hoelzl@40703  1293 proof (safe intro!: card_inj_on_le)  hoelzl@40703  1294  assume *: "card A \ card B"  hoelzl@40703  1295  obtain f where 1: "inj_on f A" and 2: "f  A = {0 ..< card A}"  hoelzl@40703  1296  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force  hoelzl@40703  1297  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g  {0 ..< card B} = B"  hoelzl@40703  1298  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force  hoelzl@40703  1299  ultimately have "inj_on g (f  A)" using subset_inj_on[of g _ "f  A"] * by force  hoelzl@40703  1300  hence "inj_on (g o f) A" using 1 comp_inj_on by blast  hoelzl@40703  1301  moreover  hoelzl@40703  1302  {have "{0 ..< card A} \ {0 ..< card B}" using * by force  hoelzl@40703  1303  with 2 have "f  A \ {0 ..< card B}" by blast  hoelzl@40703  1304  hence "(g o f)  A \ B" unfolding comp_def using 3 by force  hoelzl@40703  1305  }  hoelzl@40703  1306  ultimately show "(\f. inj_on f A \ f  A \ B)" by blast  hoelzl@40703  1307 qed (insert assms, auto)  nipkow@26105  1308 haftmann@63417  1309 lemma subset_eq_atLeast0_lessThan_card:  haftmann@63365  1310  fixes n :: nat  haftmann@63417  1311  assumes "N \ {0.. n"  haftmann@63365  1313 proof -  haftmann@63417  1314  from assms finite_lessThan have "card N \ card {0..Intervals of integers\  paulson@14485  1321 nipkow@15045  1322 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..Finiteness\  paulson@14485  1333 paulson@15418  1334 lemma image_atLeastZeroLessThan_int: "0 \ u ==>  nipkow@15045  1335  {(0::int).. u")  paulson@14485  1344  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1345  apply (rule finite_imageI)  paulson@14485  1346  apply auto  paulson@14485  1347  done  paulson@14485  1348 nipkow@15045  1349 lemma finite_atLeastLessThan_int [iff]: "finite {l..Cardinality\  paulson@14485  1368 nipkow@15045  1369 lemma card_atLeastZeroLessThan_int: "card {(0::int).. u")  paulson@14485  1371  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1372  apply (subst card_image)  paulson@14485  1373  apply (auto simp add: inj_on_def)  paulson@14485  1374  done  paulson@14485  1375 nipkow@15045  1376 lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}"  bulwahn@27656  1398 proof -  bulwahn@27656  1399  have "{k. P k \ k < i} \ {.. M"  bulwahn@27656  1405 shows "card {k \ M. k < Suc i} \ 0"  bulwahn@27656  1406 proof -  bulwahn@27656  1407  from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto  bulwahn@27656  1408  with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)  bulwahn@27656  1409 qed  bulwahn@27656  1410 bulwahn@27656  1411 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"  haftmann@37388  1412 apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"])  bulwahn@27656  1413 apply auto  bulwahn@27656  1414 apply (rule inj_on_diff_nat)  bulwahn@27656  1415 apply auto  bulwahn@27656  1416 apply (case_tac x)  bulwahn@27656  1417 apply auto  bulwahn@27656  1418 apply (case_tac xa)  bulwahn@27656  1419 apply auto  bulwahn@27656  1420 apply (case_tac xa)  bulwahn@27656  1421 apply auto  bulwahn@27656  1422 done  bulwahn@27656  1423 bulwahn@27656  1424 lemma card_less_Suc:  bulwahn@27656  1425  assumes zero_in_M: "0 \ M"  bulwahn@27656  1426  shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"  bulwahn@27656  1427 proof -  bulwahn@27656  1428  from assms have a: "0 \ {k \ M. k < Suc i}" by simp  bulwahn@27656  1429  hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})"  bulwahn@27656  1430  by (auto simp only: insert_Diff)  bulwahn@27656  1431  have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto  hoelzl@62369  1432  from finite_M_bounded_by_nat[of "\x. x \ M" "Suc i"]  lp15@57113  1433  have "Suc (card {k. Suc k \ M \ k < i}) = card (insert 0 ({k \ M. k < Suc i} - {0}))"  bulwahn@27656  1434  apply (subst card_insert)  bulwahn@27656  1435  apply simp_all  bulwahn@27656  1436  apply (subst b)  bulwahn@27656  1437  apply (subst card_less_Suc2[symmetric])  bulwahn@27656  1438  apply simp_all  bulwahn@27656  1439  done  bulwahn@27656  1440  with c show ?thesis by simp  bulwahn@27656  1441 qed  bulwahn@27656  1442 paulson@14485  1443 nipkow@64267  1444 subsection \Lemmas useful with the summation operator sum\  paulson@13850  1445 wenzelm@60758  1446 text \For examples, see Algebra/poly/UnivPoly2.thy\  ballarin@13735  1447 wenzelm@60758  1448 subsubsection \Disjoint Unions\  ballarin@13735  1449 wenzelm@60758  1450 text \Singletons and open intervals\  ballarin@13735  1451 ballarin@13735  1452 lemma ivl_disj_un_singleton:  nipkow@15045  1453  "{l::'a::linorder} Un {l<..} = {l..}"  nipkow@15045  1454  "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  1458  "(l::'a::linorder) <= u ==> {l..One- and two-sided intervals\  ballarin@13735  1462 ballarin@13735  1463 lemma ivl_disj_un_one:  nipkow@15045  1464  "(l::'a::linorder) < u ==> {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  1467  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  1469  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  1471  "(l::'a::linorder) <= u ==> {l..Two- and two-sided intervals\  ballarin@13735  1475 ballarin@13735  1476 lemma ivl_disj_un_two:  nipkow@15045  1477  "[| (l::'a::linorder) < m; m <= u |] ==> {l<.. {l<..m} Un {m<.. {l.. {l..m} Un {m<.. {l<.. {l<..m} Un {m<..u} = {l<..u}"  nipkow@15045  1483  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  1485 by auto  ballarin@13735  1486 lp15@60150  1487 lemma ivl_disj_un_two_touch:  lp15@60150  1488  "[| (l::'a::linorder) < m; m < u |] ==> {l<..m} Un {m.. {l..m} Un {m.. {l<..m} Un {m..u} = {l<..u}"  lp15@60150  1491  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m..u} = {l..u}"  lp15@60150  1492 by auto  lp15@60150  1493 lp15@60150  1494 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ivl_disj_un_two_touch  ballarin@13735  1495 wenzelm@60758  1496 subsubsection \Disjoint Intersections\  ballarin@13735  1497 wenzelm@60758  1498 text \One- and two-sided intervals\  ballarin@13735  1499 ballarin@13735  1500 lemma ivl_disj_int_one:  nipkow@15045  1501  "{..l::'a::order} Int {l<..Two- and two-sided intervals\  ballarin@13735  1512 ballarin@13735  1513 lemma ivl_disj_int_two:  nipkow@15045  1514  "{l::'a::order<..Some Differences\  nipkow@15542  1527 nipkow@15542  1528 lemma ivl_diff[simp]:  nipkow@15542  1529  "i \ n \ {i..Some Subset Conditions\  nipkow@15542  1542 blanchet@54147  1543 lemma ivl_subset [simp]:  nipkow@15542  1544  "({i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  1545 apply(auto simp:linorder_not_le)  nipkow@15542  1546 apply(rule ccontr)  nipkow@15542  1547 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  1548 apply(clarsimp simp:linorder_not_le)  nipkow@44890  1549 apply(fastforce)  nipkow@15542  1550 done  nipkow@15542  1551 nipkow@15041  1552 haftmann@63417  1553 subsection \Generic big monoid operation over intervals\  haftmann@63417  1554 haftmann@66936  1555 context semiring_char_0  haftmann@66936  1556 begin  haftmann@66936  1557 haftmann@66936  1558 lemma inj_on_of_nat [simp]:  haftmann@66936  1559  "inj_on of_nat N"  haftmann@63417  1560  by rule simp  haftmann@63417  1561 haftmann@66936  1562 lemma bij_betw_of_nat [simp]:  haftmann@66936  1563  "bij_betw of_nat N A \ of_nat  N = A"  haftmann@66936  1564  by (simp add: bij_betw_def)  haftmann@66936  1565 haftmann@66936  1566 end  haftmann@66936  1567 haftmann@63417  1568 context comm_monoid_set  haftmann@63417  1569 begin  haftmann@63417  1570 haftmann@66936  1571 lemma atLeast_lessThan_reindex:  haftmann@66936  1572  "F g {h m.. h) {m.. h) {m..n}"  haftmann@66936  1583  if "bij_betw h {m..n} {h m..h n}" for m n ::nat  haftmann@66936  1584 proof -  haftmann@66936  1585  from that have "inj_on h {m..n}" and "h  {m..n} = {h m..h n}"  haftmann@66936  1586  by (simp_all add: bij_betw_def)  haftmann@66936  1587  then show ?thesis  haftmann@66936  1588  using reindex [of h "{m..n}" g] by simp  haftmann@66936  1589 qed  haftmann@66936  1590 haftmann@66936  1591 lemma atLeast_lessThan_shift_bounds:  haftmann@66936  1592  "F g {m + k.. plus k) {m.. plus k) {m..n}"  haftmann@66936  1599  for m n k :: nat  haftmann@66936  1600  using atLeast_atMost_reindex [of "plus k" m n g]  haftmann@66936  1601  by (simp add: ac_simps)  haftmann@63417  1602 haftmann@63417  1603 lemma atLeast_Suc_lessThan_Suc_shift:  haftmann@63417  1604  "F g {Suc m.. Suc) {m.. Suc) {m..n}"  haftmann@66936  1610  using atLeast_atMost_shift_bounds [of _ _ 1]  haftmann@66936  1611  by (simp add: plus_1_eq_Suc)  haftmann@66936  1612 haftmann@66936  1613 lemma atLeast_int_lessThan_int_shift:  haftmann@66936  1614  "F g {int m.. int) {m.. int) {m..n}"  haftmann@66936  1620  by (rule atLeast_atMost_reindex)  haftmann@66936  1621  (simp add: image_int_atLeast_atMost)  haftmann@63417  1622 haftmann@63417  1623 lemma atLeast0_lessThan_Suc:  haftmann@63417  1624  "F g {0..* g n"  haftmann@63417  1625  by (simp add: atLeast0_lessThan_Suc ac_simps)  haftmann@63417  1626 haftmann@63417  1627 lemma atLeast0_atMost_Suc:  haftmann@63417  1628  "F g {0..Suc n} = F g {0..n} \<^bold>* g (Suc n)"  haftmann@63417  1629  by (simp add: atLeast0_atMost_Suc ac_simps)  haftmann@63417  1630 haftmann@63417  1631 lemma atLeast0_lessThan_Suc_shift:  haftmann@63417  1632  "F g {0..* F (g \ Suc) {0..* F (g \ Suc) {0..n}"  haftmann@63417  1637  by (simp add: atLeast0_atMost_Suc_eq_insert_0 atLeast_Suc_atMost_Suc_shift)  haftmann@63417  1638 haftmann@63417  1639 lemma ivl_cong:  haftmann@63417  1640  "a = c \ b = d \ (\x. c \ x \ x < d \ g x = h x)  haftmann@63417  1641  \ F g {a.. plus m) {0.. n") simp_all  haftmann@63417  1649 haftmann@63417  1650 lemma atLeast_atMost_shift_0:  haftmann@63417  1651  fixes m n p :: nat  haftmann@63417  1652  assumes "m \ n"  haftmann@63417  1653  shows "F g {m..n} = F (g \ plus m) {0..n - m}"  haftmann@63417  1654  using assms atLeast_atMost_shift_bounds [of g 0 m "n - m"] by simp  haftmann@63417  1655 haftmann@63417  1656 lemma atLeast_lessThan_concat:  haftmann@63417  1657  fixes m n p :: nat  haftmann@63417  1658  shows "m \ n \ n \ p \ F g {m..* F g {n..i. g (m + n - Suc i)) {n..i. g (m + n - i)) {n..m}"  haftmann@63417  1668  by (rule reindex_bij_witness [where i="\i. m + n - i" and j="\i. m + n - i"]) auto  haftmann@63417  1669 haftmann@63417  1670 lemma atLeast_lessThan_rev_at_least_Suc_atMost:  haftmann@63417  1671  "F g {n..i. g (m + n - i)) {Suc n..m}"  haftmann@63417  1672  unfolding atLeast_lessThan_rev [of g n m]  haftmann@63417  1673  by (cases m) (simp_all add: atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost)  haftmann@63417  1674 haftmann@63417  1675 end  haftmann@63417  1676 haftmann@63417  1677 wenzelm@60758  1678 subsection \Summation indexed over intervals\  nipkow@15042  1679 wenzelm@61955  1680 syntax (ASCII)  nipkow@64267  1681  "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@64267  1682  "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@64267  1683  "_upt_sum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@64267  1684  "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  wenzelm@61955  1685 nipkow@15056  1686 syntax (latex_sum output)  nipkow@64267  1687  "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b"  wenzelm@63935  1688  ("(3\<^latex>\\\sum_{\_ = _\<^latex>\}^{\_\<^latex>\}\ _)" [0,0,0,10] 10)  nipkow@64267  1689  "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b"  wenzelm@63935  1690  ("(3\<^latex>\\\sum_{\_ = _\<^latex>\}^{<\_\<^latex>\}\ _)" [0,0,0,10] 10)  nipkow@64267  1691  "_upt_sum" :: "idt \ 'a \ 'b \ 'b"  wenzelm@63935  1692  ("(3\<^latex>\\\sum_{\_ < _\<^latex>\}\ _)" [0,0,10] 10)  nipkow@64267  1693  "_upto_sum" :: "idt \ 'a \ 'b \ 'b"  wenzelm@63935  1694  ("(3\<^latex>\\\sum_{\_ \ _\<^latex>\}\ _)" [0,0,10] 10)  nipkow@15041  1695 wenzelm@61955  1696 syntax  nipkow@64267  1697  "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@64267  1698  "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@64267  1699  "_upt_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@64267  1700  "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  wenzelm@61955  1701 nipkow@15048  1702 translations  nipkow@64267  1703  "\x=a..b. t" == "CONST sum (\x. t) {a..b}"  nipkow@64267  1704  "\x=a..x. t) {a..i\n. t" == "CONST sum (\i. t) {..n}"  nipkow@64267  1706  "\ii. t) {..The above introduces some pretty alternative syntaxes for  nipkow@15056  1709 summation over intervals:  nipkow@15052  1710 \begin{center}  nipkow@15052  1711 \begin{tabular}{lll}  nipkow@15056  1712 Old & New & \LaTeX\\  nipkow@15056  1713 @{term[source]"\x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  1714 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  1716 @{term[source]"\x\{..xxlatex_sum\ (e.g.\ via \mode = latex_sum\ in  nipkow@15056  1724 antiquotations). It is not the default \LaTeX\ output because it only  nipkow@15056  1725 works well with italic-style formulae, not tt-style.  nipkow@15052  1726 nipkow@15052  1727 Note that for uniformity on @{typ nat} it is better to use  nipkow@64267  1728 @{term"\x::nat=0..\x: \sum\ may  nipkow@15052  1729 not provide all lemmas available for @{term"{m..  nipkow@15052  1731 wenzelm@60758  1732 text\This congruence rule should be used for sums over intervals as  nipkow@64267  1733 the standard theorem @{text[source]sum.cong} does not work well  nipkow@15542  1734 with the simplifier who adds the unsimplified premise @{term"x:B"} to  wenzelm@60758  1735 the context.\  nipkow@15542  1736 nipkow@64267  1737 lemmas sum_ivl_cong = sum.ivl_cong  nipkow@15041  1738 nipkow@16041  1739 (* FIXME why are the following simp rules but the corresponding eqns  nipkow@16041  1740 on intervals are not? *)  nipkow@16041  1741 nipkow@64267  1742 lemma sum_atMost_Suc [simp]:  haftmann@63417  1743  "(\i \ Suc n. f i) = (\i \ n. f i) + f (Suc n)"  haftmann@63417  1744  by (simp add: atMost_Suc ac_simps)  nipkow@16052  1745 nipkow@64267  1746 lemma sum_lessThan_Suc [simp]:  haftmann@63417  1747  "(\i < Suc n. f i) = (\i < n. f i) + f n"  haftmann@63417  1748  by (simp add: lessThan_Suc ac_simps)  nipkow@15041  1749 nipkow@64267  1750 lemma sum_cl_ivl_Suc [simp]:  nipkow@64267  1751  "sum f {m..Suc n} = (if Suc n < m then 0 else sum f {m..n} + f(Suc n))"  haftmann@63417  1752  by (auto simp: ac_simps atLeastAtMostSuc_conv)  nipkow@15561  1753 nipkow@64267  1754 lemma sum_op_ivl_Suc [simp]:  nipkow@64267  1755  "sum f {m..  nipkow@15561  1759  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  haftmann@57514  1760 by (auto simp:ac_simps atLeastAtMostSuc_conv)  nipkow@16041  1761 *)  nipkow@28068  1762 nipkow@64267  1763 lemma sum_head:  nipkow@28068  1764  fixes n :: nat  hoelzl@62369  1765  assumes mn: "m <= n"  nipkow@28068  1766  shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  nipkow@28068  1767 proof -  nipkow@28068  1768  from mn  nipkow@28068  1769  have "{m..n} = {m} \ {m<..n}"  nipkow@28068  1770  by (auto intro: ivl_disj_un_singleton)  nipkow@28068  1771  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  nipkow@28068  1772  by (simp add: atLeast0LessThan)  nipkow@28068  1773  also have "\ = ?rhs" by simp  nipkow@28068  1774  finally show ?thesis .  nipkow@28068  1775 qed  nipkow@28068  1776 nipkow@64267  1777 lemma sum_head_Suc:  nipkow@64267  1778  "m \ n \ sum f {m..n} = f m + sum f {Suc m..n}"  nipkow@64267  1779 by (simp add: sum_head atLeastSucAtMost_greaterThanAtMost)  nipkow@64267  1780 nipkow@64267  1781 lemma sum_head_upt_Suc:  nipkow@64267  1782  "m < n \ sum f {m.. n + 1"  nipkow@64267  1788  shows "sum f {m..n + p} = sum f {m..n} + sum f {n + 1..n + p}"  nipkow@31501  1789 proof-  wenzelm@60758  1790  have "{m .. n+p} = {m..n} \ {n+1..n+p}" using \m \ n+1\ by auto  nipkow@64267  1791  thus ?thesis by (auto simp: ivl_disj_int sum.union_disjoint  nipkow@31501  1792  atLeastSucAtMost_greaterThanAtMost)  nipkow@31501  1793 qed  nipkow@28068  1794 nipkow@64267  1795 lemmas sum_add_nat_ivl = sum.atLeast_lessThan_concat  nipkow@64267  1796 nipkow@64267  1797 lemma sum_diff_nat_ivl:  nipkow@15539  1798 fixes f :: "nat \ 'a::ab_group_add"  nipkow@15539  1799 shows "\ m \ n; n \ p \ \  nipkow@64267  1800  sum f {m.. ('a::ab_group_add)"  nipkow@64267  1807  shows "sum (\k. f k - f(k + 1)) {(m::nat) .. n} =  nipkow@31505  1808  (if m <= n then f m - f(n + 1) else 0)"  nipkow@31505  1809 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)  nipkow@31505  1810 nipkow@64267  1811 lemma sum_nat_group: "(\m(i,j)\{(i,j). i+j < n}. f i j) = (\ki\k. f i (k - i))"  nipkow@64267  1820  apply (simp add: sum.Sigma)  nipkow@64267  1821  apply (rule sum.reindex_bij_witness[where j="\(i, j). (i+j, i)" and i="\(k, i). (i, k - i)"])  lp15@60150  1822  apply auto  lp15@60150  1823  done  lp15@60150  1824 nipkow@64267  1825 lemma sum_triangle_reindex_eq:  lp15@60150  1826  fixes n :: nat  lp15@60150  1827  shows "(\(i,j)\{(i,j). i+j \ n}. f i j) = (\k\n. \i\k. f i (k - i))"  nipkow@64267  1828 using sum_triangle_reindex [of f "Suc n"]  lp15@60150  1829 by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost)  lp15@60150  1830 nipkow@64267  1831 lemma nat_diff_sum_reindex: "(\iix. Q x \ P x \ (\xxxShifting bounds\  nipkow@16733  1839 nipkow@64267  1840 lemma sum_shift_bounds_nat_ivl:  nipkow@64267  1841  "sum f {m+k.. 'a"  haftmann@66936  1861  assumes "f 0 = 0"  haftmann@66936  1862 begin  nipkow@64267  1863 nipkow@64267  1864 lemma sum_shift_lb_Suc0_0_upt:  haftmann@66936  1865  "sum f {Suc 0..f 0 = 0\ by simp  haftmann@66936  1876 qed  haftmann@66936  1877 haftmann@66936  1878 lemma sum_shift_lb_Suc0_0:  haftmann@66936  1879  "sum f {Suc 0..k} = sum f {0..k}"  haftmann@66936  1880 proof (cases k)  haftmann@66936  1881  case 0  haftmann@66936  1882  with \f 0 = 0\ show ?thesis  haftmann@66936  1883  by simp  haftmann@66936  1884 next  haftmann@66936  1885  case (Suc k)  haftmann@66936  1886  moreover have "{0..Suc k} = insert 0 {Suc 0..Suc k}"  haftmann@66936  1887  by auto  haftmann@66936  1888  ultimately show ?thesis  haftmann@66936  1889  using \f 0 = 0\ by simp  haftmann@66936  1890 qed  haftmann@66936  1891 haftmann@66936  1892 end  haftmann@66936  1893 haftmann@66936  1894 end  kleing@19022  1895 nipkow@64267  1896 lemma sum_atMost_Suc_shift:  haftmann@52380  1897  fixes f :: "nat \ 'a::comm_monoid_add"  haftmann@52380  1898  shows "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))"  haftmann@52380  1899 proof (induct n)  haftmann@52380  1900  case 0 show ?case by simp  haftmann@52380  1901 next  haftmann@52380  1902  case (Suc n) note IH = this  haftmann@52380  1903  have "(\i\Suc (Suc n). f i) = (\i\Suc n. f i) + f (Suc (Suc n))"  nipkow@64267  1904  by (rule sum_atMost_Suc)  haftmann@52380  1905  also have "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))"  haftmann@52380  1906  by (rule IH)  haftmann@52380  1907  also have "f 0 + (\i\n. f (Suc i)) + f (Suc (Suc n)) =  haftmann@52380  1908  f 0 + ((\i\n. f (Suc i)) + f (Suc (Suc n)))"  haftmann@57512  1909  by (rule add.assoc)  haftmann@52380  1910  also have "(\i\n. f (Suc i)) + f (Suc (Suc n)) = (\i\Suc n. f (Suc i))"  nipkow@64267  1911  by (rule sum_atMost_Suc [symmetric])  haftmann@52380  1912  finally show ?case .  haftmann@52380  1913 qed  haftmann@52380  1914 nipkow@64267  1915 lemma sum_lessThan_Suc_shift:  eberlm@63099  1916  "(\ii 'a::comm_monoid_add"  lp15@62379  1921  shows "(\i\n. f i) = f 0 + (\i (\i = m..n. f i) = f n + (\i = m.. 'a::ab_group_add"  lp15@56238  1929  assumes "m \ Suc n"  lp15@56238  1930  shows "(\i = m..n. f(Suc i) - f i) = f (Suc n) - f m"  lp15@56238  1931 using assms by (induct n) (auto simp: le_Suc_eq)  lp15@55718  1932 lp15@65273  1933 lemma sum_Suc_diff':  lp15@65273  1934  fixes f :: "nat \ 'a::ab_group_add"  lp15@65273  1935  assumes "m \ n"  lp15@65273  1936  shows "(\i = m..i = 0..n. (\j = 0..j = 0..i = Suc j..n. a i j)"  nipkow@64267  1941  by (induction n) (auto simp: sum.distrib)  nipkow@64267  1942 nipkow@64267  1943 lemma nested_sum_swap':  lp15@56215  1944  "(\i\n. (\jji = Suc j..n. a i j)"  nipkow@64267  1945  by (induction n) (auto simp: sum.distrib)  nipkow@64267  1946 nipkow@64267  1947 lemma sum_atLeast1_atMost_eq:  nipkow@64267  1948  "sum f {Suc 0..n} = (\k = (\kTelescoping\  eberlm@61524  1959 nipkow@64267  1960 lemma sum_telescope:  eberlm@61524  1961  fixes f::"nat \ 'a::ab_group_add"  nipkow@64267  1962  shows "sum (\i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)"  eberlm@61524  1963  by (induct i) simp_all  eberlm@61524  1964 nipkow@64267  1965 lemma sum_telescope'':  eberlm@61524  1966  assumes "m \ n"  eberlm@61524  1967  shows "(\k\{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)"  eberlm@61524  1968  by (rule dec_induct[OF assms]) (simp_all add: algebra_simps)  eberlm@61524  1969 nipkow@64267  1970 lemma sum_lessThan_telescope:  eberlm@63721  1971  "(\nnThe formula for geometric sums\  ballarin@17149  1980 nipkow@66490  1981 lemma sum_power2: "(\i=0.. 1"  hoelzl@56193  1986  shows "(\i 0" by simp_all  hoelzl@56193  1989  moreover have "(\iy \ 0$$  haftmann@36307  1991  ultimately show ?thesis by simp  haftmann@36307  1992 qed  haftmann@36307  1993 nipkow@64267  1994 lemma diff_power_eq_sum:  lp15@60162  1995  fixes y :: "'a::{comm_ring,monoid_mult}"  lp15@60162  1996  shows  lp15@60162  1997  "x ^ (Suc n) - y ^ (Suc n) =  lp15@60162  1998  (x - y) * (\pppp\\COMPLEX_POLYFUN\ in HOL Light\  lp15@60162  2015  fixes x :: "'a::{comm_ring,monoid_mult}"  lp15@60162  2016  shows "x^n - y^n = (x - y) * (\i 0 \ x^n - 1 = (x - 1) * (\i 0 \ 1 - x^n = (1 - x) * (\i 0 \ 1 - x^n = (1 - x) * (\ii\n. x^i) = 1 - x^Suc n"  lp15@65578  2040  by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)  lp15@65578  2041 lp15@65578  2042 lemma sum_power_shift:  lp15@65578  2043  fixes x :: "'a::{comm_ring,monoid_mult}"  lp15@65578  2044  assumes "m \ n"  lp15@65578  2045  shows "(\i=m..n. x^i) = x^m * (\i\n-m. x^i)"  lp15@65578  2046 proof -  lp15@65578  2047  have "(\i=m..n. x^i) = x^m * (\i=m..n. x^(i-m))"  lp15@65578  2048  by (simp add: sum_distrib_left power_add [symmetric])  lp15@65578  2049  also have "(\i=m..n. x^(i-m)) = (\i\n-m. x^i)"  lp15@65578  2050  using \m \ n\ by (intro sum.reindex_bij_witness[where j="\i. i - m" and i="\i. i + m"]) auto  lp15@65578  2051  finally show ?thesis .  lp15@65578  2052 qed  lp15@65578  2053 lp15@65578  2054 lemma sum_gp_multiplied:  lp15@65578  2055  fixes x :: "'a::{comm_ring,monoid_mult}"  lp15@65578  2056  assumes "m \ n"  lp15@65578  2057  shows "(1 - x) * (\i=m..n. x^i) = x^m - x^Suc n"  lp15@65578  2058 proof -  lp15@65578  2059  have "(1 - x) * (\i=m..n. x^i) = x^m * (1 - x) * (\i\n-m. x^i)"  lp15@65578  2060  by (metis mult.assoc mult.commute assms sum_power_shift)  lp15@65578  2061  also have "... =x^m * (1 - x^Suc(n-m))"  lp15@65578  2062  by (metis mult.assoc sum_gp_basic)  lp15@65578  2063  also have "... = x^m - x^Suc n"  lp15@65578  2064  using assms  lp15@65578  2065  by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)  lp15@65578  2066  finally show ?thesis .  lp15@65578  2067 qed  lp15@65578  2068 lp15@65578  2069 lemma sum_gp:  lp15@65578  2070  fixes x :: "'a::{comm_ring,division_ring}"  lp15@65578  2071  shows "(\i=m..n. x^i) =  lp15@65578  2072  (if n < m then 0  lp15@65578  2073  else if x = 1 then of_nat((n + 1) - m)  lp15@65578  2074  else (x^m - x^Suc n) / (1 - x))"  lp15@65578  2075 using sum_gp_multiplied [of m n x] apply auto  lp15@65578  2076 by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)  lp15@65578  2077 haftmann@66936  2078 haftmann@66936  2079 subsubsection\Geometric progressions\  lp15@65578  2080 lp15@65578  2081 lemma sum_gp0:  lp15@65578  2082  fixes x :: "'a::{comm_ring,division_ring}"  lp15@65578  2083  shows "(\i\n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"  lp15@65578  2084  using sum_gp_basic[of x n]  lp15@65578  2085  by (simp add: mult.commute divide_simps)  lp15@65578  2086 lp15@65578  2087 lemma sum_power_add:  lp15@65578  2088  fixes x :: "'a::{comm_ring,monoid_mult}"  lp15@65578  2089  shows "(\i\I. x^(m+i)) = x^m * (\i\I. x^i)"  lp15@65578  2090  by (simp add: sum_distrib_left power_add)  lp15@65578  2091 lp15@65578  2092 lemma sum_gp_offset:  lp15@65578  2093  fixes x :: "'a::{comm_ring,division_ring}"  lp15@65578  2094  shows "(\i=m..m+n. x^i) =  lp15@65578  2095  (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"  lp15@65578  2096  using sum_gp [of x m "m+n"]  lp15@65578  2097  by (auto simp: power_add algebra_simps)  lp15@65578  2098 lp15@65578  2099 lemma sum_gp_strict:  lp15@65578  2100  fixes x :: "'a::{comm_ring,division_ring}"  lp15@65578  2101  shows "(\iThe formulae for arithmetic sums\  haftmann@66936  2106 haftmann@66936  2107 context comm_semiring_1  haftmann@66936  2108 begin  haftmann@66936  2109 haftmann@66936  2110 lemma double_gauss_sum:  haftmann@66936  2111  "2 * (\i = 0..n. of_nat i) = of_nat n * (of_nat n + 1)"  haftmann@66936  2112  by (induct n) (simp_all add: sum.atLeast0_atMost_Suc algebra_simps left_add_twice)  haftmann@66936  2113 haftmann@66936  2114 lemma double_gauss_sum_from_Suc_0:  haftmann@66936  2115  "2 * (\i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1)"  haftmann@66936  2116 proof -  haftmann@66936  2117  have "sum of_nat {Suc 0..n} = sum of_nat (insert 0 {Suc 0..n})"  haftmann@66936  2118  by simp  haftmann@66936  2119  also have "\ = sum of_nat {0..n}"  haftmann@66936  2120  by (cases n) (simp_all add: atLeast0_atMost_Suc_eq_insert_0)  haftmann@66936  2121  finally show ?thesis  haftmann@66936  2122  by (simp add: double_gauss_sum)  haftmann@66936  2123 qed  haftmann@66936  2124 haftmann@66936  2125 lemma double_arith_series:  haftmann@66936  2126  "2 * (\i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d)"  haftmann@66936  2127 proof -  haftmann@66936  2128  have "(\i = 0..n. a + of_nat i * d) = ((\i = 0..n. a) + (\i = 0..n. of_nat i * d))"  haftmann@66936  2129  by (rule sum.distrib)  haftmann@66936  2130  also have "\ = (of_nat (Suc n) * a + d * (\i = 0..n. of_nat i))"  haftmann@66936  2131  by (simp add: sum_distrib_left algebra_simps)  haftmann@66936  2132  finally show ?thesis  haftmann@66936  2133  by (simp add: algebra_simps double_gauss_sum left_add_twice)  haftmann@66936  2134 qed  haftmann@66936  2135 haftmann@66936  2136 end  haftmann@66936  2137 haftmann@66936  2138 context semiring_parity  haftmann@66936  2139 begin  kleing@19469  2140 huffman@47222  2141 lemma gauss_sum:  haftmann@66936  2142  "(\i = 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2"  haftmann@66936  2143  using double_gauss_sum [of n, symmetric] by simp  haftmann@66936  2144 haftmann@66936  2145 lemma gauss_sum_from_Suc_0:  haftmann@66936  2146  "(\i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2"  haftmann@66936  2147  using double_gauss_sum_from_Suc_0 [of n, symmetric] by simp  haftmann@66936  2148 haftmann@66936  2149 lemma arith_series:  haftmann@66936  2150  "(\i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d) div 2"  haftmann@66936  2151  using double_arith_series [of a d n, symmetric] by simp  haftmann@66936  2152 haftmann@66936  2153 end  haftmann@66936  2154 haftmann@66936  2155 lemma gauss_sum_nat:  haftmann@66936  2156  "\{0..n} = (n * Suc n) div 2"  haftmann@66936  2157  using gauss_sum [of n, where ?'a = nat] by simp  kleing@19469  2158 kleing@19469  2159 lemma arith_series_nat:  haftmann@66936  2160  "(\i = 0..n. a + i * d) = Suc n * (2 * a + n * d) div 2"  haftmann@66936  2161  using arith_series [of a d n] by simp  haftmann@66936  2162 haftmann@66936  2163 lemma Sum_Icc_int:  haftmann@66936  2164  "\{m..n} = (n * (n + 1) - m * (m - 1)) div 2"  haftmann@66936  2165  if "m \ n" for m n :: int  haftmann@66936  2166 using that proof (induct i \ "nat (n - m)" arbitrary: m n)  haftmann@66936  2167  case 0  haftmann@66936  2168  then have "m = n"  haftmann@66936  2169  by arith  haftmann@66936  2170  then show ?case  haftmann@66936  2171  by (simp add: algebra_simps mult_2 [symmetric])  haftmann@66936  2172 next  haftmann@66936  2173  case (Suc i)  haftmann@66936  2174  have 0: "i = nat((n-1) - m)" "m \ n-1" using Suc(2,3) by arith+  haftmann@66936  2175  have "\ {m..n} = \ {m..1+(n-1)}" by simp  haftmann@66936  2176  also have "\ = \ {m..n-1} + n" using \m \ n\  haftmann@66936  2177  by(subst atLeastAtMostPlus1_int_conv) simp_all  haftmann@66936  2178  also have "\ = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n"  haftmann@66936  2179  by(simp add: Suc(1)[OF 0])  haftmann@66936  2180  also have "\ = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp  haftmann@66936  2181  also have "\ = (n*(n+1) - m*(m-1)) div 2"  haftmann@66936  2182  by (simp add: algebra_simps mult_2_right)  haftmann@66936  2183  finally show ?case .  haftmann@66936  2184 qed  haftmann@66936  2185 haftmann@66936  2186 lemma Sum_Icc_nat:  haftmann@66936  2187  "\{m..n} = (n * (n + 1) - m * (m - 1)) div 2"  haftmann@66936  2188  if "m \ n" for m n :: nat  kleing@19469  2189 proof -  haftmann@66936  2190  have *: "m * (m - 1) \ n * (n + 1)"  haftmann@66936  2191  using that by (meson diff_le_self order_trans le_add1 mult_le_mono)  haftmann@66936  2192  have "int (\{m..n}) = (\{int m..int n})"  haftmann@66936  2193  by (simp add: sum.atLeast_int_atMost_int_shift)  haftmann@66936  2194  also have "\ = (int n * (int n + 1) - int m * (int m - 1)) div 2"  haftmann@66936  2195  using that by (simp add: Sum_Icc_int)  haftmann@66936  2196  also have "\ = int ((n * (n + 1) - m * (m - 1)) div 2)"  haftmann@66936  2197  using le_square * by (simp add: algebra_simps of_nat_div of_nat_diff)  haftmann@66936  2198  finally show ?thesis  haftmann@66936  2199  by (simp only: of_nat_eq_iff)  kleing@19469  2200 qed  kleing@19469  2201 haftmann@66936  2202 lemma Sum_Ico_nat:  haftmann@66936  2203  "\{m.. n" for m n :: nat  haftmann@66936  2205 proof -  haftmann@66936  2206  from that consider "m < n" | "m = n"  haftmann@66936  2207  by (auto simp add: less_le)  haftmann@66936  2208  then show ?thesis proof cases  haftmann@66936  2209  case 1  haftmann@66936  2210  then have "{m..{m..{m..n - 1}"  haftmann@66936  2213  by simp  haftmann@66936  2214  also have "\ = (n * (n - 1) - m * (m - 1)) div 2"  haftmann@66936  2215  using \m < n\ by (simp add: Sum_Icc_nat mult.commute)  haftmann@66936  2216  finally show ?thesis .  haftmann@66936  2217  next  haftmann@66936  2218  case 2  haftmann@66936  2219  then show ?thesis  haftmann@66936  2220  by simp  haftmann@66936  2221  qed  haftmann@66936  2222 qed  kleing@19022  2223 wenzelm@61955  2224 haftmann@63417  2225 subsubsection \Division remainder\  haftmann@63417  2226 haftmann@63417  2227 lemma range_mod:  haftmann@63417  2228  fixes n :: nat  haftmann@63417  2229  assumes "n > 0"  haftmann@63417  2230  shows "range (\m. m mod n) = {0.. ?A \ m \ ?B"  haftmann@63417  2234  proof  haftmann@63417  2235  assume "m \ ?A"  haftmann@63417  2236  with assms show "m \ ?B"  wenzelm@63915  2237  by auto  haftmann@63417  2238  next  haftmann@63417  2239  assume "m \ ?B"  haftmann@63417  2240  moreover have "m mod n \ ?A"  haftmann@63417  2241  by (rule rangeI)  haftmann@63417  2242  ultimately show "m \ ?A"  haftmann@63417  2243  by simp  haftmann@63417  2244  qed  haftmann@63417  2245 qed  haftmann@63417  2246 haftmann@63417  2247 wenzelm@60758  2248 subsection \Products indexed over intervals\  paulson@29960  2249 wenzelm@61955  2250 syntax (ASCII)  nipkow@64272  2251  "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)  nipkow@64272  2252  "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@64272  2253  "_upt_prod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10)  nipkow@64272  2254  "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10)  wenzelm@61955  2255 paulson@29960  2256 syntax (latex_prod output)  nipkow@64272  2257  "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b"  wenzelm@63935  2258  ("(3\<^latex>\$\\prod_{\_ = _\<^latex>\}^{\_\<^latex>\}$\ _)" [0,0,0,10] 10)  nipkow@64272  2259  "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b"  wenzelm@63935  2260  ("(3\<^latex>\$\\prod_{\_ = _\<^latex>\}^{<\_\<^latex>\}$\ _)" [0,0,0,10] 10)  nipkow@64272  2261  "_upt_prod" :: "idt \ 'a \ 'b \ 'b"  wenzelm@63935  2262  ("(3\<^latex>\$\\prod_{\_ < _\<^latex>\}$\ _)" [0,0,10] 10)  nipkow@64272  2263  "_upto_prod" :: "idt \ 'a \ 'b \ 'b"  wenzelm@63935  2264  ("(3\<^latex>\$\\prod_{\_ \ _\<^latex>\}$\ _)" [0,0,10] 10)  paulson@29960  2265 wenzelm@61955  2266 syntax  nipkow@64272  2267  "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@64272  2268  "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@64272  2269  "_upt_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@64272  2270  "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  wenzelm@61955  2271 paulson@29960  2272 translations  nipkow@64272  2273  "\x=a..b. t" \ "CONST prod (\x. t) {a..b}"  nipkow@64272  2274  "\x=a.. "CONST prod (\x. t) {a..i\n. t" \ "CONST prod (\i. t) {..n}"  nipkow@64272  2276  "\i "CONST prod (\i. t) {..{int i..int (i+j)}"  lp15@55242  2279  by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)  lp15@55242  2280 nipkow@64272  2281 lemma prod_int_eq: "prod int {i..j} = \{int i..int j}"  lp15@55242  2282 proof (cases "i \ j")  lp15@55242  2283  case True  lp15@55242  2284  then show ?thesis  nipkow@64272  2285  by (metis le_iff_add prod_int_plus_eq)  lp15@55242  2286 next  lp15@55242  2287  case False  lp15@55242  2288  then show ?thesis  lp15@55242  2289  by auto  lp15@55242  2290 qed  lp15@55242  2291 eberlm@61524  2292 haftmann@63417  2293 subsubsection \Shifting bounds\  eberlm@61524  2294 nipkow@64272  2295 lemma prod_shift_bounds_nat_ivl:  nipkow@64272  2296  "prod f {m+k..ii b \ prod f {a.. Suc n"  nipkow@64272  2322  shows "prod f {m..Suc n} = f (Suc n) * prod f {m..n}"  eberlm@61524  2323 proof -  eberlm@61524  2324  from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto  nipkow@64272  2325  also have "prod f \ = f (Suc n) * prod f {m..n}" by simp  eberlm@61524  2326  finally show ?thesis .  eberlm@61524  2327 qed  eberlm@61524  2328 eberlm@62128  2329 eberlm@62128  2330 subsection \Efficient folding over intervals\  eberlm@62128  2331 eberlm@62128  2332 function fold_atLeastAtMost_nat where  eberlm@62128  2333  [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc =  eberlm@62128  2334  (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a acc))"  eberlm@62128  2335 by pat_completeness auto  eberlm@62128  2336 termination by (relation "measure (\(_,a,b,_). Suc b - a)") auto  eberlm@62128  2337 eberlm@62128  2338 lemma fold_atLeastAtMost_nat:  eberlm@62128  2339  assumes "comp_fun_commute f"  eberlm@62128  2340  shows "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}"  eberlm@62128  2341 using assms  eberlm@62128  2342 proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases)  eberlm@62128  2343  case (1 f a b acc)  eberlm@62128  2344  interpret comp_fun_commute f by fact  eberlm@62128  2345  show ?case  eberlm@62128  2346  proof (cases "a > b")  eberlm@62128  2347  case True  eberlm@62128  2348  thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto  eberlm@62128  2349  next  eberlm@62128  2350  case False  eberlm@62128  2351  with 1 show ?thesis  eberlm@62128  2352  by (subst fold_atLeastAtMost_nat.simps)  eberlm@62128  2353  (auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm)  eberlm@62128  2354  qed  eberlm@62128  2355 qed  eberlm@62128  2356 nipkow@64267  2357 lemma sum_atLeastAtMost_code:  nipkow@64267  2358  "sum f {a..b} = fold_atLeastAtMost_nat (\a acc. f a + acc) a b 0"  eberlm@62128  2359 proof -  eberlm@62128  2360  have "comp_fun_commute (\a. op + (f a))"  eberlm@62128  2361  by unfold_locales (auto simp: o_def add_ac)  eberlm@62128  2362  thus ?thesis  nipkow@64267  2363  by (simp add: sum.eq_fold fold_atLeastAtMost_nat o_def)  eberlm@62128  2364 qed  eberlm@62128  2365 nipkow@64272  2366 lemma prod_atLeastAtMost_code:  nipkow@64272  2367  "prod f {a..b} = fold_atLeastAtMost_nat (\a acc. f a * acc) a b 1"  eberlm@62128  2368 proof -  eberlm@62128  2369  have "comp_fun_commute (\a. op * (f a))"  eberlm@62128  2370  by unfold_locales (auto simp: o_def mult_ac)  eberlm@62128  2371  thus ?thesis  nipkow@64272  2372  by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def)  eberlm@62128  2373 qed  eberlm@62128  2374 eberlm@62128  2375 (* TODO: Add support for more kinds of intervals here *)  eberlm@62128  2376 nipkow@8924  2377 end `