src/HOL/Set_Interval.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (23 months ago) changeset 66831 29ea2b900a05 parent 66490 cc66ab2373ce child 66836 4eb431c3f974 permissions -rw-r--r--
tuned: each session has at most one defining entry;
 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@63365  17 imports Lattices_Big Divides Nat_Transfer  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 nipkow@24691  221 end  ballarin@13735  222 wenzelm@60758  223 subsubsection\Emptyness, singletons, subset\  nipkow@15554  224 nipkow@24691  225 context order  nipkow@24691  226 begin  nipkow@15554  227 nipkow@32400  228 lemma atLeastatMost_empty[simp]:  nipkow@32400  229  "b < a \ {a..b} = {}"  nipkow@32400  230 by(auto simp: atLeastAtMost_def atLeast_def atMost_def)  nipkow@32400  231 nipkow@32400  232 lemma atLeastatMost_empty_iff[simp]:  nipkow@32400  233  "{a..b} = {} \ (~ a <= b)"  nipkow@32400  234 by auto (blast intro: order_trans)  nipkow@32400  235 nipkow@32400  236 lemma atLeastatMost_empty_iff2[simp]:  nipkow@32400  237  "{} = {a..b} \ (~ a <= b)"  nipkow@32400  238 by auto (blast intro: order_trans)  nipkow@32400  239 nipkow@32400  240 lemma atLeastLessThan_empty[simp]:  nipkow@32400  241  "b <= a \ {a.. (~ a < b)"  nipkow@32400  246 by auto (blast intro: le_less_trans)  nipkow@32400  247 nipkow@32400  248 lemma atLeastLessThan_empty_iff2[simp]:  nipkow@32400  249  "{} = {a.. (~ a < b)"  nipkow@32400  250 by auto (blast intro: le_less_trans)  nipkow@15554  251 nipkow@32400  252 lemma greaterThanAtMost_empty[simp]: "l \ k ==> {k<..l} = {}"  nipkow@17719  253 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)  nipkow@17719  254 nipkow@32400  255 lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ ~ k < l"  nipkow@32400  256 by auto (blast intro: less_le_trans)  nipkow@32400  257 nipkow@32400  258 lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ ~ k < l"  nipkow@32400  259 by auto (blast intro: less_le_trans)  nipkow@32400  260 haftmann@29709  261 lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. {a .. b} = {a}" by simp  hoelzl@36846  268 nipkow@32400  269 lemma atLeastatMost_subset_iff[simp]:  nipkow@32400  270  "{a..b} <= {c..d} \ (~ a <= b) | c <= a & b <= d"  nipkow@32400  271 unfolding atLeastAtMost_def atLeast_def atMost_def  nipkow@32400  272 by (blast intro: order_trans)  nipkow@32400  273 nipkow@32400  274 lemma atLeastatMost_psubset_iff:  nipkow@32400  275  "{a..b} < {c..d} \  nipkow@32400  276  ((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d"  nipkow@39302  277 by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)  nipkow@32400  278 nipkow@51334  279 lemma Icc_eq_Icc[simp]:  nipkow@51334  280  "{l..h} = {l'..h'} = (l=l' \ h=h' \ \ l\h \ \ l'\h')"  nipkow@51334  281 by(simp add: order_class.eq_iff)(auto intro: order_trans)  nipkow@51334  282 hoelzl@36846  283 lemma atLeastAtMost_singleton_iff[simp]:  hoelzl@36846  284  "{a .. b} = {c} \ a = b \ b = c"  hoelzl@36846  285 proof  hoelzl@36846  286  assume "{a..b} = {c}"  wenzelm@53374  287  hence *: "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp  wenzelm@60758  288  with \{a..b} = {c}\ have "c \ a \ b \ c" by auto  wenzelm@53374  289  with * show "a = b \ b = c" by auto  hoelzl@36846  290 qed simp  hoelzl@36846  291 nipkow@51334  292 lemma Icc_subset_Ici_iff[simp]:  nipkow@51334  293  "{l..h} \ {l'..} = (~ l\h \ l\l')"  nipkow@51334  294 by(auto simp: subset_eq intro: order_trans)  nipkow@51334  295 nipkow@51334  296 lemma Icc_subset_Iic_iff[simp]:  nipkow@51334  297  "{l..h} \ {..h'} = (~ l\h \ h\h')"  nipkow@51334  298 by(auto simp: subset_eq intro: order_trans)  nipkow@51334  299 nipkow@51334  300 lemma not_Ici_eq_empty[simp]: "{l..} \ {}"  nipkow@51334  301 by(auto simp: set_eq_iff)  nipkow@51334  302 nipkow@51334  303 lemma not_Iic_eq_empty[simp]: "{..h} \ {}"  nipkow@51334  304 by(auto simp: set_eq_iff)  nipkow@51334  305 nipkow@51334  306 lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric]  nipkow@51334  307 lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric]  nipkow@51334  308 nipkow@24691  309 end  paulson@14485  310 nipkow@51334  311 context no_top  nipkow@51334  312 begin  nipkow@51334  313 nipkow@51334  314 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  315 lemma not_UNIV_le_Icc[simp]: "\ UNIV \ {l..h}"  nipkow@51334  316 using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  317 nipkow@51334  318 lemma not_UNIV_le_Iic[simp]: "\ UNIV \ {..h}"  nipkow@51334  319 using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  320 nipkow@51334  321 lemma not_Ici_le_Icc[simp]: "\ {l..} \ {l'..h'}"  nipkow@51334  322 using gt_ex[of h']  nipkow@51334  323 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  324 nipkow@51334  325 lemma not_Ici_le_Iic[simp]: "\ {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 end  nipkow@51334  330 nipkow@51334  331 context no_bot  nipkow@51334  332 begin  nipkow@51334  333 nipkow@51334  334 lemma not_UNIV_le_Ici[simp]: "\ UNIV \ {l..}"  nipkow@51334  335 using lt_ex[of l] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  336 nipkow@51334  337 lemma not_Iic_le_Icc[simp]: "\ {..h} \ {l'..h'}"  nipkow@51334  338 using lt_ex[of l']  nipkow@51334  339 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  340 nipkow@51334  341 lemma not_Iic_le_Ici[simp]: "\ {..h} \ {l'..}"  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 end  nipkow@51334  346 nipkow@51334  347 nipkow@51334  348 context no_top  nipkow@51334  349 begin  nipkow@51334  350 nipkow@51334  351 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  352 lemma not_UNIV_eq_Icc[simp]: "\ UNIV = {l'..h'}"  nipkow@51334  353 using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  354 nipkow@51334  355 lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric]  nipkow@51334  356 nipkow@51334  357 lemma not_UNIV_eq_Iic[simp]: "\ UNIV = {..h'}"  nipkow@51334  358 using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  359 nipkow@51334  360 lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric]  nipkow@51334  361 nipkow@51334  362 lemma not_Icc_eq_Ici[simp]: "\ {l..h} = {l'..}"  nipkow@51334  363 unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast  nipkow@51334  364 nipkow@51334  365 lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric]  nipkow@51334  366 nipkow@51334  367 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  368 lemma not_Iic_eq_Ici[simp]: "\ {..h} = {l'..}"  nipkow@51334  369 using not_Ici_le_Iic[of l' h] by blast  nipkow@51334  370 nipkow@51334  371 lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric]  nipkow@51334  372 nipkow@51334  373 end  nipkow@51334  374 nipkow@51334  375 context no_bot  nipkow@51334  376 begin  nipkow@51334  377 nipkow@51334  378 lemma not_UNIV_eq_Ici[simp]: "\ UNIV = {l'..}"  nipkow@51334  379 using lt_ex[of l'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  380 nipkow@51334  381 lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric]  nipkow@51334  382 nipkow@51334  383 lemma not_Icc_eq_Iic[simp]: "\ {l..h} = {..h'}"  nipkow@51334  384 unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast  nipkow@51334  385 nipkow@51334  386 lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric]  nipkow@51334  387 nipkow@51334  388 end  nipkow@51334  389 nipkow@51334  390 hoelzl@53216  391 context dense_linorder  hoelzl@42891  392 begin  hoelzl@42891  393 hoelzl@42891  394 lemma greaterThanLessThan_empty_iff[simp]:  hoelzl@42891  395  "{ a <..< b } = {} \ b \ a"  hoelzl@42891  396  using dense[of a b] by (cases "a < b") auto  hoelzl@42891  397 hoelzl@42891  398 lemma greaterThanLessThan_empty_iff2[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@42901  402 lemma atLeastLessThan_subseteq_atLeastAtMost_iff:  hoelzl@42901  403  "{a ..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  404  using dense[of "max a d" "b"]  hoelzl@42901  405  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  406 hoelzl@42901  407 lemma greaterThanAtMost_subseteq_atLeastAtMost_iff:  hoelzl@42901  408  "{a <.. b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  409  using dense[of "a" "min c b"]  hoelzl@42901  410  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  411 hoelzl@42901  412 lemma greaterThanLessThan_subseteq_atLeastAtMost_iff:  hoelzl@42901  413  "{a <..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  414  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@42901  415  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  416 hoelzl@43657  417 lemma atLeastAtMost_subseteq_atLeastLessThan_iff:  hoelzl@43657  418  "{a .. b} \ { c ..< d } \ (a \ b \ c \ a \ b < d)"  hoelzl@43657  419  using dense[of "max a d" "b"]  hoelzl@43657  420  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@62369  421 eberlm@61524  422 lemma greaterThanLessThan_subseteq_greaterThanLessThan:  eberlm@61524  423  "{a <..< b} \ {c <..< d} \ (a < b \ a \ c \ b \ d)"  eberlm@61524  424  using dense[of "a" "min c b"] dense[of "max a d" "b"]  eberlm@61524  425  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  426 hoelzl@43657  427 lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:  hoelzl@43657  428  "{a <.. b} \ { c ..< d } \ (a < b \ c \ a \ b < d)"  hoelzl@43657  429  using dense[of "a" "min c b"]  hoelzl@43657  430  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  431 hoelzl@43657  432 lemma greaterThanLessThan_subseteq_atLeastLessThan_iff:  hoelzl@43657  433  "{a <..< b} \ { c ..< d } \ (a < b \ c \ a \ b \ d)"  hoelzl@43657  434  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@43657  435  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  436 hoelzl@56328  437 lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff:  hoelzl@56328  438  "{a <..< b} \ { c <.. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@56328  439  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@56328  440  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@56328  441 hoelzl@42891  442 end  hoelzl@42891  443 hoelzl@51329  444 context no_top  hoelzl@51329  445 begin  hoelzl@51329  446 nipkow@51334  447 lemma greaterThan_non_empty[simp]: "{x <..} \ {}"  hoelzl@51329  448  using gt_ex[of x] by auto  hoelzl@51329  449 hoelzl@51329  450 end  hoelzl@51329  451 hoelzl@51329  452 context no_bot  hoelzl@51329  453 begin  hoelzl@51329  454 nipkow@51334  455 lemma lessThan_non_empty[simp]: "{..< x} \ {}"  hoelzl@51329  456  using lt_ex[of x] by auto  hoelzl@51329  457 hoelzl@51329  458 end  hoelzl@51329  459 nipkow@32408  460 lemma (in linorder) atLeastLessThan_subset_iff:  nipkow@32408  461  "{a.. b <= a | c<=a & b<=d"  nipkow@32408  462 apply (auto simp:subset_eq Ball_def)  nipkow@32408  463 apply(frule_tac x=a in spec)  nipkow@32408  464 apply(erule_tac x=d in allE)  nipkow@32408  465 apply (simp add: less_imp_le)  nipkow@32408  466 done  nipkow@32408  467 hoelzl@40703  468 lemma atLeastLessThan_inj:  hoelzl@40703  469  fixes a b c d :: "'a::linorder"  hoelzl@40703  470  assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"  hoelzl@40703  471  shows "a = c" "b = d"  hoelzl@40703  472 using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+  hoelzl@40703  473 hoelzl@40703  474 lemma atLeastLessThan_eq_iff:  hoelzl@40703  475  fixes a b c d :: "'a::linorder"  hoelzl@40703  476  assumes "a < b" "c < d"  hoelzl@40703  477  shows "{a ..< b} = {c ..< d} \ a = c \ b = d"  hoelzl@40703  478  using atLeastLessThan_inj assms by auto  hoelzl@40703  479 hoelzl@57447  480 lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \ (b \ a \ d \ c) \ a = c \ b = d"  hoelzl@57447  481  by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le)  hoelzl@57447  482 hoelzl@57447  483 lemma (in order) Iio_Int_singleton: "{.. {x} = (if x < k then {x} else {})"  hoelzl@57447  484  by auto  hoelzl@57447  485 hoelzl@57447  486 lemma (in linorder) Ioc_subset_iff: "{a<..b} \ {c<..d} \ (b \ a \ c \ a \ b \ d)"  hoelzl@57447  487  by (auto simp: subset_eq Ball_def) (metis less_le not_less)  hoelzl@57447  488 haftmann@52729  489 lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \ x = bot"  nipkow@51334  490 by (auto simp: set_eq_iff intro: le_bot)  hoelzl@51328  491 haftmann@52729  492 lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \ x = top"  nipkow@51334  493 by (auto simp: set_eq_iff intro: top_le)  hoelzl@51328  494 nipkow@51334  495 lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff:  nipkow@51334  496  "{x..y} = UNIV \ (x = bot \ y = top)"  nipkow@51334  497 by (auto simp: set_eq_iff intro: top_le le_bot)  hoelzl@51328  498 hoelzl@56949  499 lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \ n = bot"  hoelzl@56949  500  by (auto simp: set_eq_iff not_less le_bot)  hoelzl@56949  501 hoelzl@56949  502 lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \ n = 0"  hoelzl@56949  503  by (simp add: Iio_eq_empty_iff bot_nat_def)  hoelzl@56949  504 noschinl@58970  505 lemma mono_image_least:  noschinl@58970  506  assumes f_mono: "mono f" and f_img: "f  {m ..< n} = {m' ..< n'}" "m < n"  noschinl@58970  507  shows "f m = m'"  noschinl@58970  508 proof -  noschinl@58970  509  from f_img have "{m' ..< n'} \ {}"  noschinl@58970  510  by (metis atLeastLessThan_empty_iff image_is_empty)  noschinl@58970  511  with f_img have "m' \ f  {m ..< n}" by auto  noschinl@58970  512  then obtain k where "f k = m'" "m \ k" by auto  noschinl@58970  513  moreover have "m' \ f m" using f_img by auto  noschinl@58970  514  ultimately show "f m = m'"  noschinl@58970  515  using f_mono by (auto elim: monoE[where x=m and y=k])  noschinl@58970  516 qed  noschinl@58970  517 hoelzl@51328  518 wenzelm@60758  519 subsection \Infinite intervals\  hoelzl@56328  520 hoelzl@56328  521 context dense_linorder  hoelzl@56328  522 begin  hoelzl@56328  523 hoelzl@56328  524 lemma infinite_Ioo:  hoelzl@56328  525  assumes "a < b"  hoelzl@56328  526  shows "\ finite {a<.. {}"  wenzelm@60758  530  using \a < b\ by auto  hoelzl@56328  531  ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b"  hoelzl@56328  532  using Max_in[of "{a <..< b}"] by auto  hoelzl@56328  533  then obtain x where "Max {a <..< b} < x" "x < b"  hoelzl@56328  534  using dense[of "Max {a<.. {a <..< b}"  wenzelm@60758  536  using \a < Max {a <..< b}\ by auto  hoelzl@56328  537  then have "x \ Max {a <..< b}"  hoelzl@56328  538  using fin by auto  wenzelm@60758  539  with \Max {a <..< b} < x\ show False by auto  hoelzl@56328  540 qed  hoelzl@56328  541 hoelzl@56328  542 lemma infinite_Icc: "a < b \ \ finite {a .. b}"  hoelzl@56328  543  using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b]  hoelzl@56328  544  by (auto dest: finite_subset)  hoelzl@56328  545 hoelzl@56328  546 lemma infinite_Ico: "a < b \ \ finite {a ..< b}"  hoelzl@56328  547  using greaterThanLessThan_subseteq_atLeastLessThan_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_Ioc: "a < b \ \ finite {a <.. b}"  hoelzl@56328  551  using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b]  hoelzl@56328  552  by (auto dest: finite_subset)  hoelzl@56328  553 lp15@63967  554 lemma infinite_Ioo_iff [simp]: "infinite {a<.. a < b"  lp15@63967  555  using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioo)  lp15@63967  556 lp15@63967  557 lemma infinite_Icc_iff [simp]: "infinite {a .. b} \ a < b"  lp15@63967  558  using not_less_iff_gr_or_eq by (fastforce simp: infinite_Icc)  lp15@63967  559 lp15@63967  560 lemma infinite_Ico_iff [simp]: "infinite {a.. a < b"  lp15@63967  561  using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ico)  lp15@63967  562 lp15@63967  563 lemma infinite_Ioc_iff [simp]: "infinite {a<..b} \ a < b"  lp15@63967  564  using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioc)  lp15@63967  565 hoelzl@56328  566 end  hoelzl@56328  567 hoelzl@56328  568 lemma infinite_Iio: "\ finite {..< a :: 'a :: {no_bot, linorder}}"  hoelzl@56328  569 proof  hoelzl@56328  570  assume "finite {..< a}"  hoelzl@56328  571  then have *: "\x. x < a \ Min {..< a} \ x"  hoelzl@56328  572  by auto  hoelzl@56328  573  obtain x where "x < a"  hoelzl@56328  574  using lt_ex by auto  hoelzl@56328  575 hoelzl@56328  576  obtain y where "y < Min {..< a}"  hoelzl@56328  577  using lt_ex by auto  hoelzl@56328  578  also have "Min {..< a} \ x"  wenzelm@60758  579  using \x < a\ by fact  wenzelm@60758  580  also note \x < a\  hoelzl@56328  581  finally have "Min {..< a} \ y"  hoelzl@56328  582  by fact  wenzelm@60758  583  with \y < Min {..< a}\ show False by auto  hoelzl@56328  584 qed  hoelzl@56328  585 hoelzl@56328  586 lemma infinite_Iic: "\ finite {.. a :: 'a :: {no_bot, linorder}}"  hoelzl@56328  587  using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"]  hoelzl@56328  588  by (auto simp: subset_eq less_imp_le)  hoelzl@56328  589 hoelzl@56328  590 lemma infinite_Ioi: "\ finite {a :: 'a :: {no_top, linorder} <..}"  hoelzl@56328  591 proof  hoelzl@56328  592  assume "finite {a <..}"  hoelzl@56328  593  then have *: "\x. a < x \ x \ Max {a <..}"  hoelzl@56328  594  by auto  hoelzl@56328  595 hoelzl@56328  596  obtain y where "Max {a <..} < y"  hoelzl@56328  597  using gt_ex by auto  hoelzl@56328  598 wenzelm@63540  599  obtain x where x: "a < x"  hoelzl@56328  600  using gt_ex by auto  wenzelm@63540  601  also from x have "x \ Max {a <..}"  hoelzl@56328  602  by fact  wenzelm@60758  603  also note \Max {a <..} < y\  hoelzl@56328  604  finally have "y \ Max { a <..}"  hoelzl@56328  605  by fact  wenzelm@60758  606  with \Max {a <..} < y\ show False by auto  hoelzl@56328  607 qed  hoelzl@56328  608 hoelzl@56328  609 lemma infinite_Ici: "\ finite {a :: 'a :: {no_top, linorder} ..}"  hoelzl@56328  610  using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"]  hoelzl@56328  611  by (auto simp: subset_eq less_imp_le)  hoelzl@56328  612 wenzelm@60758  613 subsubsection \Intersection\  nipkow@32456  614 nipkow@32456  615 context linorder  nipkow@32456  616 begin  nipkow@32456  617 nipkow@32456  618 lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"  nipkow@32456  619 by auto  nipkow@32456  620 nipkow@32456  621 lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"  nipkow@32456  622 by auto  nipkow@32456  623 nipkow@32456  624 lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"  nipkow@32456  625 by auto  nipkow@32456  626 nipkow@32456  627 lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"  nipkow@32456  628 by auto  nipkow@32456  629 nipkow@32456  630 lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"  nipkow@32456  631 by auto  nipkow@32456  632 nipkow@32456  633 lemma Int_atLeastLessThan[simp]: "{a.. {..b} = {.. min a b}"  hoelzl@50417  643  by (auto simp: min_def)  hoelzl@50417  644 hoelzl@57447  645 lemma Ioc_disjoint: "{a<..b} \ {c<..d} = {} \ b \ a \ d \ c \ b \ c \ d \ a"  wenzelm@63092  646  by auto  hoelzl@57447  647 nipkow@32456  648 end  nipkow@32456  649 hoelzl@51329  650 context complete_lattice  hoelzl@51329  651 begin  hoelzl@51329  652 hoelzl@51329  653 lemma  hoelzl@51329  654  shows Sup_atLeast[simp]: "Sup {x ..} = top"  hoelzl@51329  655  and Sup_greaterThanAtLeast[simp]: "x < top \ Sup {x <..} = top"  hoelzl@51329  656  and Sup_atMost[simp]: "Sup {.. y} = y"  hoelzl@51329  657  and Sup_atLeastAtMost[simp]: "x \ y \ Sup { x .. y} = y"  hoelzl@51329  658  and Sup_greaterThanAtMost[simp]: "x < y \ Sup { x <.. y} = y"  hoelzl@51329  659  by (auto intro!: Sup_eqI)  hoelzl@51329  660 hoelzl@51329  661 lemma  hoelzl@51329  662  shows Inf_atMost[simp]: "Inf {.. x} = bot"  hoelzl@51329  663  and Inf_atMostLessThan[simp]: "top < x \ Inf {..< x} = bot"  hoelzl@51329  664  and Inf_atLeast[simp]: "Inf {x ..} = x"  hoelzl@51329  665  and Inf_atLeastAtMost[simp]: "x \ y \ Inf { x .. y} = x"  hoelzl@51329  666  and Inf_atLeastLessThan[simp]: "x < y \ Inf { x ..< y} = x"  hoelzl@51329  667  by (auto intro!: Inf_eqI)  hoelzl@51329  668 hoelzl@51329  669 end  hoelzl@51329  670 hoelzl@51329  671 lemma  hoelzl@53216  672  fixes x y :: "'a :: {complete_lattice, dense_linorder}"  hoelzl@51329  673  shows Sup_lessThan[simp]: "Sup {..< y} = y"  hoelzl@51329  674  and Sup_atLeastLessThan[simp]: "x < y \ Sup { x ..< y} = y"  hoelzl@51329  675  and Sup_greaterThanLessThan[simp]: "x < y \ Sup { x <..< y} = y"  hoelzl@51329  676  and Inf_greaterThan[simp]: "Inf {x <..} = x"  hoelzl@51329  677  and Inf_greaterThanAtMost[simp]: "x < y \ Inf { x <.. y} = x"  hoelzl@51329  678  and Inf_greaterThanLessThan[simp]: "x < y \ Inf { x <..< y} = x"  hoelzl@51329  679  by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded)  nipkow@32456  680 wenzelm@60758  681 subsection \Intervals of natural numbers\  paulson@14485  682 wenzelm@60758  683 subsubsection \The Constant @{term lessThan}\  paulson@15047  684 paulson@14485  685 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"  paulson@14485  686 by (simp add: lessThan_def)  paulson@14485  687 paulson@14485  688 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"  paulson@14485  689 by (simp add: lessThan_def less_Suc_eq, blast)  paulson@14485  690 wenzelm@60758  691 text \The following proof is convenient in induction proofs where  hoelzl@39072  692 new elements get indices at the beginning. So it is used to transform  wenzelm@60758  693 @{term "{..  hoelzl@39072  694 hoelzl@59000  695 lemma zero_notin_Suc_image: "0 \ Suc  A"  hoelzl@59000  696  by auto  hoelzl@59000  697 hoelzl@39072  698 lemma lessThan_Suc_eq_insert_0: "{..The Constant @{term greaterThan}\  paulson@15047  711 lp15@65273  712 lemma greaterThan_0: "greaterThan 0 = range Suc"  paulson@14485  713 apply (simp add: greaterThan_def)  paulson@14485  714 apply (blast dest: gr0_conv_Suc [THEN iffD1])  paulson@14485  715 done  paulson@14485  716 paulson@14485  717 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"  paulson@14485  718 apply (simp add: greaterThan_def)  paulson@14485  719 apply (auto elim: linorder_neqE)  paulson@14485  720 done  paulson@14485  721 paulson@14485  722 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"  paulson@14485  723 by blast  paulson@14485  724 wenzelm@60758  725 subsubsection \The Constant @{term atLeast}\  paulson@15047  726 paulson@14485  727 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"  paulson@14485  728 by (unfold atLeast_def UNIV_def, simp)  paulson@14485  729 paulson@14485  730 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"  paulson@14485  731 apply (simp add: atLeast_def)  paulson@14485  732 apply (simp add: Suc_le_eq)  paulson@14485  733 apply (simp add: order_le_less, blast)  paulson@14485  734 done  paulson@14485  735 paulson@14485  736 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"  paulson@14485  737  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)  paulson@14485  738 paulson@14485  739 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"  paulson@14485  740 by blast  paulson@14485  741 wenzelm@60758  742 subsubsection \The Constant @{term atMost}\  paulson@15047  743 paulson@14485  744 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"  paulson@14485  745 by (simp add: atMost_def)  paulson@14485  746 paulson@14485  747 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"  paulson@14485  748 apply (simp add: atMost_def)  paulson@14485  749 apply (simp add: less_Suc_eq order_le_less, blast)  paulson@14485  750 done  paulson@14485  751 paulson@14485  752 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"  paulson@14485  753 by blast  paulson@14485  754 wenzelm@60758  755 subsubsection \The Constant @{term atLeastLessThan}\  paulson@15047  756 wenzelm@60758  757 text\The orientation of the following 2 rules is tricky. The lhs is  nipkow@24449  758 defined in terms of the rhs. Hence the chosen orientation makes sense  nipkow@24449  759 in this theory --- the reverse orientation complicates proofs (eg  nipkow@24449  760 nontermination). But outside, when the definition of the lhs is rarely  nipkow@24449  761 used, the opposite orientation seems preferable because it reduces a  wenzelm@60758  762 specific concept to a more general one.\  nipkow@28068  763 haftmann@63417  764 lemma atLeast0LessThan [code_abbrev]: "{0::nat..The Constant @{term atLeastAtMost}\  haftmann@63417  791 haftmann@63417  792 lemma atLeast0_atMost_Suc:  haftmann@63417  793  "{0..Suc n} = insert (Suc n) {0..n}"  haftmann@63417  794  by (simp add: atLeast0AtMost atMost_Suc)  haftmann@63417  795 haftmann@63417  796 lemma atLeast0_atMost_Suc_eq_insert_0:  haftmann@63417  797  "{0..Suc n} = insert 0 (Suc  {0..n})"  haftmann@63417  798  by (simp add: atLeast0AtMost Iic_Suc_eq_insert_0)  haftmann@63417  799 haftmann@63417  800 wenzelm@60758  801 subsubsection \Intervals of nats with @{term Suc}\  paulson@15047  802 wenzelm@60758  803 text\Not a simprule because the RHS is too messy.\  paulson@15047  804 lemma atLeastLessThanSuc:  paulson@15047  805  "{m.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  829 by (auto simp add: atLeastAtMost_def)  nipkow@15554  830 noschinl@45932  831 lemma atLeastAtMost_insertL: "m \ n \ insert m {Suc m..n} = {m ..n}"  noschinl@45932  832 by auto  noschinl@45932  833 wenzelm@60758  834 text \The analogous result is useful on @{typ int}:\  kleing@43157  835 (* here, because we don't have an own int section *)  kleing@43157  836 lemma atLeastAtMostPlus1_int_conv:  kleing@43157  837  "m <= 1+n \ {m..1+n} = insert (1+n) {m..n::int}"  kleing@43157  838  by (auto intro: set_eqI)  kleing@43157  839 paulson@33044  840 lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j..Intervals and numerals\  lp15@57113  846 wenzelm@61799  847 lemma lessThan_nat_numeral: \\Evaluation for specific numerals\  lp15@57113  848  "lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))"  lp15@57113  849  by (simp add: numeral_eq_Suc lessThan_Suc)  lp15@57113  850 wenzelm@61799  851 lemma atMost_nat_numeral: \\Evaluation for specific numerals\  lp15@57113  852  "atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))"  lp15@57113  853  by (simp add: numeral_eq_Suc atMost_Suc)  lp15@57113  854 wenzelm@61799  855 lemma atLeastLessThan_nat_numeral: \\Evaluation for specific numerals\  hoelzl@62369  856  "atLeastLessThan m (numeral k :: nat) =  lp15@57113  857  (if m \ (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k))  lp15@57113  858  else {})"  lp15@57113  859  by (simp add: numeral_eq_Suc atLeastLessThanSuc)  lp15@57113  860 wenzelm@60758  861 subsubsection \Image\  nipkow@16733  862 lp15@60809  863 lemma image_add_atLeastAtMost [simp]:  lp15@60615  864  fixes k ::"'a::linordered_semidom"  lp15@60615  865  shows "(\n. n+k)  {i..j} = {i+k..j+k}" (is "?A = ?B")  nipkow@16733  866 proof  nipkow@16733  867  show "?A \ ?B" by auto  nipkow@16733  868 next  nipkow@16733  869  show "?B \ ?A"  nipkow@16733  870  proof  nipkow@16733  871  fix n assume a: "n : ?B"  lp15@60615  872  hence "n - k : {i..j}"  lp15@60615  873  by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le)  lp15@60615  874  moreover have "n = (n - k) + k" using a  lp15@60615  875  proof -  lp15@60615  876  have "k + i \ n"  lp15@60615  877  by (metis a add.commute atLeastAtMost_iff)  lp15@60615  878  hence "k + (n - k) = n"  lp15@60615  879  by (metis (no_types) ab_semigroup_add_class.add_ac(1) add_diff_cancel_left' le_add_diff_inverse)  lp15@60615  880  thus ?thesis  lp15@60615  881  by (simp add: add.commute)  lp15@60615  882  qed  nipkow@16733  883  ultimately show "n : ?A" by blast  nipkow@16733  884  qed  nipkow@16733  885 qed  nipkow@16733  886 lp15@60809  887 lemma image_diff_atLeastAtMost [simp]:  lp15@60809  888  fixes d::"'a::linordered_idom" shows "(op - d  {a..b}) = {d-b..d-a}"  lp15@60809  889  apply auto  lp15@60809  890  apply (rule_tac x="d-x" in rev_image_eqI, auto)  lp15@60809  891  done  lp15@60809  892 lp15@60809  893 lemma image_mult_atLeastAtMost [simp]:  lp15@60809  894  fixes d::"'a::linordered_field"  lp15@60809  895  assumes "d>0" shows "(op * d  {a..b}) = {d*a..d*b}"  lp15@60809  896  using assms  lp15@60809  897  by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])  lp15@60809  898 lp15@60809  899 lemma image_affinity_atLeastAtMost:  lp15@60809  900  fixes c :: "'a::linordered_field"  lp15@60809  901  shows "((\x. m*x + c)  {a..b}) = (if {a..b}={} then {}  lp15@60809  902  else if 0 \ m then {m*a + c .. m *b + c}  lp15@60809  903  else {m*b + c .. m*a + c})"  lp15@60809  904  apply (case_tac "m=0", auto simp: mult_le_cancel_left)  lp15@60809  905  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)  lp15@60809  906  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)  lp15@60809  907  done  lp15@60809  908 lp15@60809  909 lemma image_affinity_atLeastAtMost_diff:  lp15@60809  910  fixes c :: "'a::linordered_field"  lp15@60809  911  shows "((\x. m*x - c)  {a..b}) = (if {a..b}={} then {}  lp15@60809  912  else if 0 \ m then {m*a - c .. m*b - c}  lp15@60809  913  else {m*b - c .. m*a - c})"  lp15@60809  914  using image_affinity_atLeastAtMost [of m "-c" a b]  lp15@60809  915  by simp  lp15@60809  916 paulson@61204  917 lemma image_affinity_atLeastAtMost_div:  paulson@61204  918  fixes c :: "'a::linordered_field"  paulson@61204  919  shows "((\x. x/m + c)  {a..b}) = (if {a..b}={} then {}  paulson@61204  920  else if 0 \ m then {a/m + c .. b/m + c}  paulson@61204  921  else {b/m + c .. a/m + c})"  paulson@61204  922  using image_affinity_atLeastAtMost [of "inverse m" c a b]  paulson@61204  923  by (simp add: field_class.field_divide_inverse algebra_simps)  hoelzl@62369  924 lp15@60809  925 lemma image_affinity_atLeastAtMost_div_diff:  lp15@60809  926  fixes c :: "'a::linordered_field"  lp15@60809  927  shows "((\x. x/m - c)  {a..b}) = (if {a..b}={} then {}  lp15@60809  928  else if 0 \ m then {a/m - c .. b/m - c}  lp15@60809  929  else {b/m - c .. a/m - c})"  lp15@60809  930  using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]  lp15@60809  931  by (simp add: field_class.field_divide_inverse algebra_simps)  lp15@60809  932 nipkow@16733  933 lemma image_add_atLeastLessThan:  nipkow@16733  934  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  937 next  nipkow@16733  938  show "?B \ ?A"  nipkow@16733  939  proof  nipkow@16733  940  fix n assume a: "n : ?B"  webertj@20217  941  hence "n - k : {i..i. i - c)  {x ..< y} =  hoelzl@37664  983  (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"  hoelzl@37664  984  (is "_ = ?right")  hoelzl@37664  985 proof safe  hoelzl@37664  986  fix a assume a: "a \ ?right"  hoelzl@37664  987  show "a \ (\i. i - c)  {x ..< y}"  hoelzl@37664  988  proof cases  hoelzl@37664  989  assume "c < y" with a show ?thesis  hoelzl@37664  990  by (auto intro!: image_eqI[of _ _ "a + c"])  hoelzl@37664  991  next  hoelzl@37664  992  assume "\ c < y" with a show ?thesis  nipkow@62390  993  by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)  hoelzl@37664  994  qed  hoelzl@37664  995 qed auto  hoelzl@37664  996 Andreas@51152  997 lemma image_int_atLeastLessThan: "int  {a.. uminus  {x<..}"  hoelzl@35580  1011  by (rule imageI) (simp add: *)  hoelzl@35580  1012  thus "y \ uminus  {x<..}" by simp  hoelzl@35580  1013 next  hoelzl@35580  1014  fix y assume "y \ -x"  hoelzl@35580  1015  have "- (-y) \ uminus  {x..}"  wenzelm@60758  1016  by (rule imageI) (insert \y \ -x\[THEN le_imp_neg_le], simp)  hoelzl@35580  1017  thus "y \ uminus  {x..}" by simp  hoelzl@35580  1018 qed simp_all  hoelzl@35580  1019 hoelzl@35580  1020 lemma  hoelzl@35580  1021  fixes x :: 'a  hoelzl@35580  1022  shows image_uminus_lessThan[simp]: "uminus  {..Finiteness\  paulson@14485  1043 nipkow@15045  1044 lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..A bounded set of natural numbers is finite.\  paulson@14485  1067 lemma bounded_nat_set_is_finite:  nipkow@24853  1068  "(ALL i:N. i < (n::nat)) ==> finite N"  nipkow@28068  1069 apply (rule finite_subset)  nipkow@28068  1070  apply (rule_tac [2] finite_lessThan, auto)  nipkow@28068  1071 done  nipkow@28068  1072 wenzelm@60758  1073 text \A set of natural numbers is finite iff it is bounded.\  nipkow@31044  1074 lemma finite_nat_set_iff_bounded:  nipkow@31044  1075  "finite(N::nat set) = (EX m. ALL n:N. n?F\, simplified less_Suc_eq_le[symmetric]] by blast  nipkow@31044  1079 next  wenzelm@60758  1080  assume ?B show ?F using \?B\ by(blast intro:bounded_nat_set_is_finite)  nipkow@31044  1081 qed  nipkow@31044  1082 nipkow@31044  1083 lemma finite_nat_set_iff_bounded_le:  nipkow@31044  1084  "finite(N::nat set) = (EX m. ALL n:N. n<=m)"  nipkow@31044  1085 apply(simp add:finite_nat_set_iff_bounded)  nipkow@31044  1086 apply(blast dest:less_imp_le_nat le_imp_less_Suc)  nipkow@31044  1087 done  nipkow@31044  1088 nipkow@28068  1089 lemma finite_less_ub:  nipkow@28068  1090  "!!f::nat=>nat. (!!n. n \ f n) ==> finite {n. f n \ u}"  nipkow@28068  1091 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)  paulson@14485  1092 lp15@64773  1093 lemma bounded_Max_nat:  lp15@64773  1094  fixes P :: "nat \ bool"  lp15@64773  1095  assumes x: "P x" and M: "\x. P x \ x \ M"  lp15@64773  1096  obtains m where "P m" "\x. P x \ x \ m"  lp15@64773  1097 proof -  lp15@64773  1098  have "finite {x. P x}"  lp15@64773  1099  using M finite_nat_set_iff_bounded_le by auto  lp15@64773  1100  then have "Max {x. P x} \ {x. P x}"  lp15@64773  1101  using Max_in x by auto  lp15@64773  1102  then show ?thesis  lp15@64773  1103  by (simp add: \finite {x. P x}\ that)  lp15@64773  1104 qed  lp15@64773  1105 hoelzl@56328  1106 wenzelm@60758  1107 text\Any subset of an interval of natural numbers the size of the  wenzelm@60758  1108 subset is exactly that interval.\  nipkow@24853  1109 nipkow@24853  1110 lemma subset_card_intvl_is_intvl:  blanchet@55085  1111  assumes "A \ {k.. A" by auto  blanchet@55085  1121  with insert have "A <= {k..Proving Inclusions and Equalities between Unions\  paulson@32596  1132 nipkow@36755  1133 lemma UN_le_eq_Un0:  nipkow@36755  1134  "(\i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B")  nipkow@36755  1135 proof  nipkow@36755  1136  show "?A <= ?B"  nipkow@36755  1137  proof  nipkow@36755  1138  fix x assume "x : ?A"  nipkow@36755  1139  then obtain i where i: "i\n" "x : M i" by auto  nipkow@36755  1140  show "x : ?B"  nipkow@36755  1141  proof(cases i)  nipkow@36755  1142  case 0 with i show ?thesis by simp  nipkow@36755  1143  next  nipkow@36755  1144  case (Suc j) with i show ?thesis by auto  nipkow@36755  1145  qed  nipkow@36755  1146  qed  nipkow@36755  1147 next  wenzelm@63171  1148  show "?B <= ?A" by fastforce  nipkow@36755  1149 qed  nipkow@36755  1150 nipkow@36755  1151 lemma UN_le_add_shift:  nipkow@36755  1152  "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B")  nipkow@36755  1153 proof  nipkow@44890  1154  show "?A <= ?B" by fastforce  nipkow@36755  1155 next  nipkow@36755  1156  show "?B <= ?A"  nipkow@36755  1157  proof  nipkow@36755  1158  fix x assume "x : ?B"  nipkow@36755  1159  then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto  nipkow@36755  1160  hence "i-k\n & x : M((i-k)+k)" by auto  nipkow@36755  1161  thus "x : ?A" by blast  nipkow@36755  1162  qed  nipkow@36755  1163 qed  nipkow@36755  1164 hoelzl@62369  1165 lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)"  hoelzl@62369  1166  by (auto simp add: atLeast0LessThan)  paulson@32596  1167 haftmann@62343  1168 lemma UN_finite_subset:  haftmann@62343  1169  "(\n::nat. (\i\{0.. C) \ (\n. A n) \ C"  paulson@32596  1170  by (subst UN_UN_finite_eq [symmetric]) blast  paulson@32596  1171 hoelzl@62369  1172 lemma UN_finite2_subset:  haftmann@62343  1173  assumes "\n::nat. (\i\{0.. (\i\{0..n. A n) \ (\n. B n)"  haftmann@62343  1175 proof (rule UN_finite_subset, rule)  haftmann@62343  1176  fix n and a  haftmann@62343  1177  from assms have "(\i\{0.. (\i\{0.. (\i\{0.. (\i\{0.. (\i. B i)" by (auto simp add: UN_UN_finite_eq)  haftmann@62343  1181 qed  paulson@32596  1182 paulson@32596  1183 lemma UN_finite2_eq:  haftmann@62343  1184  "(\n::nat. (\i\{0..i\{0..  haftmann@62343  1185  (\n. A n) = (\n. B n)"  paulson@33044  1186  apply (rule subset_antisym)  paulson@33044  1187  apply (rule UN_finite2_subset, blast)  haftmann@62343  1188  apply (rule UN_finite2_subset [where k=k])  haftmann@62343  1189  apply (force simp add: atLeastLessThan_add_Un [of 0])  haftmann@62343  1190  done  paulson@32596  1191 paulson@32596  1192 wenzelm@60758  1193 subsubsection \Cardinality\  paulson@14485  1194 nipkow@15045  1195 lemma card_lessThan [simp]: "card {.. {0.. {0..n}"  wenzelm@63915  1232  shows "finite N"  haftmann@63417  1233  using assms finite_atLeastAtMost by (rule finite_subset)  haftmann@63365  1234 nipkow@26105  1235 lemma ex_bij_betw_nat_finite:  nipkow@26105  1236  "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  1247 apply(drule ex_bij_betw_finite_nat)  nipkow@31438  1248 apply(drule ex_bij_betw_nat_finite)  nipkow@31438  1249 apply(auto intro!:bij_betw_trans)  nipkow@31438  1250 done  nipkow@31438  1251 nipkow@31438  1252 lemma ex_bij_betw_nat_finite_1:  nipkow@31438  1253  "finite M \ \h. bij_betw h {1 .. card M} M"  nipkow@31438  1254 by (rule finite_same_card_bij) auto  nipkow@31438  1255 hoelzl@40703  1256 lemma bij_betw_iff_card:  lp15@63114  1257  assumes "finite A" "finite B"  lp15@63114  1258  shows "(\f. bij_betw f A B) \ (card A = card B)"  lp15@63114  1259 proof  lp15@63114  1260  assume "card A = card B"  lp15@63114  1261  moreover obtain f where "bij_betw f A {0 ..< card A}"  lp15@63114  1262  using assms ex_bij_betw_finite_nat by blast  hoelzl@40703  1263  moreover obtain g where "bij_betw g {0 ..< card B} B"  lp15@63114  1264  using assms ex_bij_betw_nat_finite by blast  hoelzl@40703  1265  ultimately have "bij_betw (g o f) A B"  lp15@63114  1266  by (auto simp: bij_betw_trans)  hoelzl@40703  1267  thus "(\f. bij_betw f A B)" by blast  lp15@63114  1268 qed (auto simp: bij_betw_same_card)  hoelzl@40703  1269 hoelzl@40703  1270 lemma inj_on_iff_card_le:  hoelzl@40703  1271  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  1272  shows "(\f. inj_on f A \ f  A \ B) = (card A \ card B)"  hoelzl@40703  1273 proof (safe intro!: card_inj_on_le)  hoelzl@40703  1274  assume *: "card A \ card B"  hoelzl@40703  1275  obtain f where 1: "inj_on f A" and 2: "f  A = {0 ..< card A}"  hoelzl@40703  1276  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force  hoelzl@40703  1277  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g  {0 ..< card B} = B"  hoelzl@40703  1278  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force  hoelzl@40703  1279  ultimately have "inj_on g (f  A)" using subset_inj_on[of g _ "f  A"] * by force  hoelzl@40703  1280  hence "inj_on (g o f) A" using 1 comp_inj_on by blast  hoelzl@40703  1281  moreover  hoelzl@40703  1282  {have "{0 ..< card A} \ {0 ..< card B}" using * by force  hoelzl@40703  1283  with 2 have "f  A \ {0 ..< card B}" by blast  hoelzl@40703  1284  hence "(g o f)  A \ B" unfolding comp_def using 3 by force  hoelzl@40703  1285  }  hoelzl@40703  1286  ultimately show "(\f. inj_on f A \ f  A \ B)" by blast  hoelzl@40703  1287 qed (insert assms, auto)  nipkow@26105  1288 haftmann@63417  1289 lemma subset_eq_atLeast0_lessThan_card:  haftmann@63365  1290  fixes n :: nat  haftmann@63417  1291  assumes "N \ {0.. n"  haftmann@63365  1293 proof -  haftmann@63417  1294  from assms finite_lessThan have "card N \ card {0..Intervals of integers\  paulson@14485  1301 nipkow@15045  1302 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..Finiteness\  paulson@14485  1313 paulson@15418  1314 lemma image_atLeastZeroLessThan_int: "0 \ u ==>  nipkow@15045  1315  {(0::int).. u")  paulson@14485  1324  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1325  apply (rule finite_imageI)  paulson@14485  1326  apply auto  paulson@14485  1327  done  paulson@14485  1328 nipkow@15045  1329 lemma finite_atLeastLessThan_int [iff]: "finite {l..Cardinality\  paulson@14485  1348 nipkow@15045  1349 lemma card_atLeastZeroLessThan_int: "card {(0::int).. u")  paulson@14485  1351  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1352  apply (subst card_image)  paulson@14485  1353  apply (auto simp add: inj_on_def)  paulson@14485  1354  done  paulson@14485  1355 nipkow@15045  1356 lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}"  bulwahn@27656  1378 proof -  bulwahn@27656  1379  have "{k. P k \ k < i} \ {.. M"  bulwahn@27656  1385 shows "card {k \ M. k < Suc i} \ 0"  bulwahn@27656  1386 proof -  bulwahn@27656  1387  from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto  bulwahn@27656  1388  with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)  bulwahn@27656  1389 qed  bulwahn@27656  1390 bulwahn@27656  1391 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"  haftmann@37388  1392 apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"])  bulwahn@27656  1393 apply auto  bulwahn@27656  1394 apply (rule inj_on_diff_nat)  bulwahn@27656  1395 apply auto  bulwahn@27656  1396 apply (case_tac x)  bulwahn@27656  1397 apply auto  bulwahn@27656  1398 apply (case_tac xa)  bulwahn@27656  1399 apply auto  bulwahn@27656  1400 apply (case_tac xa)  bulwahn@27656  1401 apply auto  bulwahn@27656  1402 done  bulwahn@27656  1403 bulwahn@27656  1404 lemma card_less_Suc:  bulwahn@27656  1405  assumes zero_in_M: "0 \ M"  bulwahn@27656  1406  shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"  bulwahn@27656  1407 proof -  bulwahn@27656  1408  from assms have a: "0 \ {k \ M. k < Suc i}" by simp  bulwahn@27656  1409  hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})"  bulwahn@27656  1410  by (auto simp only: insert_Diff)  bulwahn@27656  1411  have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto  hoelzl@62369  1412  from finite_M_bounded_by_nat[of "\x. x \ M" "Suc i"]  lp15@57113  1413  have "Suc (card {k. Suc k \ M \ k < i}) = card (insert 0 ({k \ M. k < Suc i} - {0}))"  bulwahn@27656  1414  apply (subst card_insert)  bulwahn@27656  1415  apply simp_all  bulwahn@27656  1416  apply (subst b)  bulwahn@27656  1417  apply (subst card_less_Suc2[symmetric])  bulwahn@27656  1418  apply simp_all  bulwahn@27656  1419  done  bulwahn@27656  1420  with c show ?thesis by simp  bulwahn@27656  1421 qed  bulwahn@27656  1422 paulson@14485  1423 nipkow@64267  1424 subsection \Lemmas useful with the summation operator sum\  paulson@13850  1425 wenzelm@60758  1426 text \For examples, see Algebra/poly/UnivPoly2.thy\  ballarin@13735  1427 wenzelm@60758  1428 subsubsection \Disjoint Unions\  ballarin@13735  1429 wenzelm@60758  1430 text \Singletons and open intervals\  ballarin@13735  1431 ballarin@13735  1432 lemma ivl_disj_un_singleton:  nipkow@15045  1433  "{l::'a::linorder} Un {l<..} = {l..}"  nipkow@15045  1434  "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  1438  "(l::'a::linorder) <= u ==> {l..One- and two-sided intervals\  ballarin@13735  1442 ballarin@13735  1443 lemma ivl_disj_un_one:  nipkow@15045  1444  "(l::'a::linorder) < u ==> {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  1447  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  1449  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  1451  "(l::'a::linorder) <= u ==> {l..Two- and two-sided intervals\  ballarin@13735  1455 ballarin@13735  1456 lemma ivl_disj_un_two:  nipkow@15045  1457  "[| (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  1463  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  1465 by auto  ballarin@13735  1466 lp15@60150  1467 lemma ivl_disj_un_two_touch:  lp15@60150  1468  "[| (l::'a::linorder) < m; m < u |] ==> {l<..m} Un {m.. {l..m} Un {m.. {l<..m} Un {m..u} = {l<..u}"  lp15@60150  1471  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m..u} = {l..u}"  lp15@60150  1472 by auto  lp15@60150  1473 lp15@60150  1474 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ivl_disj_un_two_touch  ballarin@13735  1475 wenzelm@60758  1476 subsubsection \Disjoint Intersections\  ballarin@13735  1477 wenzelm@60758  1478 text \One- and two-sided intervals\  ballarin@13735  1479 ballarin@13735  1480 lemma ivl_disj_int_one:  nipkow@15045  1481  "{..l::'a::order} Int {l<..Two- and two-sided intervals\  ballarin@13735  1492 ballarin@13735  1493 lemma ivl_disj_int_two:  nipkow@15045  1494  "{l::'a::order<..Some Differences\  nipkow@15542  1507 nipkow@15542  1508 lemma ivl_diff[simp]:  nipkow@15542  1509  "i \ n \ {i..Some Subset Conditions\  nipkow@15542  1522 blanchet@54147  1523 lemma ivl_subset [simp]:  nipkow@15542  1524  "({i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  1525 apply(auto simp:linorder_not_le)  nipkow@15542  1526 apply(rule ccontr)  nipkow@15542  1527 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  1528 apply(clarsimp simp:linorder_not_le)  nipkow@44890  1529 apply(fastforce)  nipkow@15542  1530 done  nipkow@15542  1531 nipkow@15041  1532 haftmann@63417  1533 subsection \Generic big monoid operation over intervals\  haftmann@63417  1534 haftmann@63417  1535 lemma inj_on_add_nat' [simp]:  haftmann@63417  1536  "inj_on (plus k) N" for k :: nat  haftmann@63417  1537  by rule simp  haftmann@63417  1538 haftmann@63417  1539 context comm_monoid_set  haftmann@63417  1540 begin  haftmann@63417  1541 haftmann@63417  1542 lemma atLeast_lessThan_shift_bounds:  haftmann@63417  1543  fixes m n k :: nat  haftmann@63417  1544  shows "F g {m + k.. plus k) {m.. plus k) {m.. plus k) {m..n}"  haftmann@63417  1556 proof -  haftmann@63417  1557  have "{m + k..n + k} = plus k  {m..n}"  haftmann@63417  1558  by (auto simp del: image_add_atLeastAtMost simp add: image_add_atLeastAtMost [symmetric])  haftmann@63417  1559  also have "F g (plus k  {m..n}) = F (g \ plus k) {m..n}"  haftmann@63417  1560  by (rule reindex) simp  haftmann@63417  1561  finally show ?thesis .  haftmann@63417  1562 qed  haftmann@63417  1563 haftmann@63417  1564 lemma atLeast_Suc_lessThan_Suc_shift:  haftmann@63417  1565  "F g {Suc m.. Suc) {m.. Suc) {m..n}"  haftmann@63417  1570  using atLeast_atMost_shift_bounds [of _ _ 1] by simp  haftmann@63417  1571 haftmann@63417  1572 lemma atLeast0_lessThan_Suc:  haftmann@63417  1573  "F g {0..* g n"  haftmann@63417  1574  by (simp add: atLeast0_lessThan_Suc ac_simps)  haftmann@63417  1575 haftmann@63417  1576 lemma atLeast0_atMost_Suc:  haftmann@63417  1577  "F g {0..Suc n} = F g {0..n} \<^bold>* g (Suc n)"  haftmann@63417  1578  by (simp add: atLeast0_atMost_Suc ac_simps)  haftmann@63417  1579 haftmann@63417  1580 lemma atLeast0_lessThan_Suc_shift:  haftmann@63417  1581  "F g {0..* F (g \ Suc) {0..* F (g \ Suc) {0..n}"  haftmann@63417  1586  by (simp add: atLeast0_atMost_Suc_eq_insert_0 atLeast_Suc_atMost_Suc_shift)  haftmann@63417  1587 haftmann@63417  1588 lemma ivl_cong:  haftmann@63417  1589  "a = c \ b = d \ (\x. c \ x \ x < d \ g x = h x)  haftmann@63417  1590  \ F g {a.. plus m) {0.. n") simp_all  haftmann@63417  1598 haftmann@63417  1599 lemma atLeast_atMost_shift_0:  haftmann@63417  1600  fixes m n p :: nat  haftmann@63417  1601  assumes "m \ n"  haftmann@63417  1602  shows "F g {m..n} = F (g \ plus m) {0..n - m}"  haftmann@63417  1603  using assms atLeast_atMost_shift_bounds [of g 0 m "n - m"] by simp  haftmann@63417  1604 haftmann@63417  1605 lemma atLeast_lessThan_concat:  haftmann@63417  1606  fixes m n p :: nat  haftmann@63417  1607  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  1617  by (rule reindex_bij_witness [where i="\i. m + n - i" and j="\i. m + n - i"]) auto  haftmann@63417  1618 haftmann@63417  1619 lemma atLeast_lessThan_rev_at_least_Suc_atMost:  haftmann@63417  1620  "F g {n..i. g (m + n - i)) {Suc n..m}"  haftmann@63417  1621  unfolding atLeast_lessThan_rev [of g n m]  haftmann@63417  1622  by (cases m) (simp_all add: atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost)  haftmann@63417  1623 haftmann@63417  1624 end  haftmann@63417  1625 haftmann@63417  1626 wenzelm@60758  1627 subsection \Summation indexed over intervals\  nipkow@15042  1628 wenzelm@61955  1629 syntax (ASCII)  nipkow@64267  1630  "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@64267  1631  "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@64267  1632  "_upt_sum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@64267  1633  "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  wenzelm@61955  1634 nipkow@15056  1635 syntax (latex_sum output)  nipkow@64267  1636  "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b"  wenzelm@63935  1637  ("(3\<^latex>\\\sum_{\_ = _\<^latex>\}^{\_\<^latex>\}\ _)" [0,0,0,10] 10)  nipkow@64267  1638  "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b"  wenzelm@63935  1639  ("(3\<^latex>\\\sum_{\_ = _\<^latex>\}^{<\_\<^latex>\}\ _)" [0,0,0,10] 10)  nipkow@64267  1640  "_upt_sum" :: "idt \ 'a \ 'b \ 'b"  wenzelm@63935  1641  ("(3\<^latex>\\\sum_{\_ < _\<^latex>\}\ _)" [0,0,10] 10)  nipkow@64267  1642  "_upto_sum" :: "idt \ 'a \ 'b \ 'b"  wenzelm@63935  1643  ("(3\<^latex>\\\sum_{\_ \ _\<^latex>\}\ _)" [0,0,10] 10)  nipkow@15041  1644 wenzelm@61955  1645 syntax  nipkow@64267  1646  "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@64267  1647  "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@64267  1648  "_upt_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@64267  1649  "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  wenzelm@61955  1650 nipkow@15048  1651 translations  nipkow@64267  1652  "\x=a..b. t" == "CONST sum (\x. t) {a..b}"  nipkow@64267  1653  "\x=a..x. t) {a..i\n. t" == "CONST sum (\i. t) {..n}"  nipkow@64267  1655  "\ii. t) {..The above introduces some pretty alternative syntaxes for  nipkow@15056  1658 summation over intervals:  nipkow@15052  1659 \begin{center}  nipkow@15052  1660 \begin{tabular}{lll}  nipkow@15056  1661 Old & New & \LaTeX\\  nipkow@15056  1662 @{term[source]"\x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  1663 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  1665 @{term[source]"\x\{..xxlatex_sum\ (e.g.\ via \mode = latex_sum\ in  nipkow@15056  1673 antiquotations). It is not the default \LaTeX\ output because it only  nipkow@15056  1674 works well with italic-style formulae, not tt-style.  nipkow@15052  1675 nipkow@15052  1676 Note that for uniformity on @{typ nat} it is better to use  nipkow@64267  1677 @{term"\x::nat=0..\x: \sum\ may  nipkow@15052  1678 not provide all lemmas available for @{term"{m..  nipkow@15052  1680 wenzelm@60758  1681 text\This congruence rule should be used for sums over intervals as  nipkow@64267  1682 the standard theorem @{text[source]sum.cong} does not work well  nipkow@15542  1683 with the simplifier who adds the unsimplified premise @{term"x:B"} to  wenzelm@60758  1684 the context.\  nipkow@15542  1685 nipkow@64267  1686 lemmas sum_ivl_cong = sum.ivl_cong  nipkow@15041  1687 nipkow@16041  1688 (* FIXME why are the following simp rules but the corresponding eqns  nipkow@16041  1689 on intervals are not? *)  nipkow@16041  1690 nipkow@64267  1691 lemma sum_atMost_Suc [simp]:  haftmann@63417  1692  "(\i \ Suc n. f i) = (\i \ n. f i) + f (Suc n)"  haftmann@63417  1693  by (simp add: atMost_Suc ac_simps)  nipkow@16052  1694 nipkow@64267  1695 lemma sum_lessThan_Suc [simp]:  haftmann@63417  1696  "(\i < Suc n. f i) = (\i < n. f i) + f n"  haftmann@63417  1697  by (simp add: lessThan_Suc ac_simps)  nipkow@15041  1698 nipkow@64267  1699 lemma sum_cl_ivl_Suc [simp]:  nipkow@64267  1700  "sum f {m..Suc n} = (if Suc n < m then 0 else sum f {m..n} + f(Suc n))"  haftmann@63417  1701  by (auto simp: ac_simps atLeastAtMostSuc_conv)  nipkow@15561  1702 nipkow@64267  1703 lemma sum_op_ivl_Suc [simp]:  nipkow@64267  1704  "sum f {m..  nipkow@15561  1708  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  haftmann@57514  1709 by (auto simp:ac_simps atLeastAtMostSuc_conv)  nipkow@16041  1710 *)  nipkow@28068  1711 nipkow@64267  1712 lemma sum_head:  nipkow@28068  1713  fixes n :: nat  hoelzl@62369  1714  assumes mn: "m <= n"  nipkow@28068  1715  shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  nipkow@28068  1716 proof -  nipkow@28068  1717  from mn  nipkow@28068  1718  have "{m..n} = {m} \ {m<..n}"  nipkow@28068  1719  by (auto intro: ivl_disj_un_singleton)  nipkow@28068  1720  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  nipkow@28068  1721  by (simp add: atLeast0LessThan)  nipkow@28068  1722  also have "\ = ?rhs" by simp  nipkow@28068  1723  finally show ?thesis .  nipkow@28068  1724 qed  nipkow@28068  1725 nipkow@64267  1726 lemma sum_head_Suc:  nipkow@64267  1727  "m \ n \ sum f {m..n} = f m + sum f {Suc m..n}"  nipkow@64267  1728 by (simp add: sum_head atLeastSucAtMost_greaterThanAtMost)  nipkow@64267  1729 nipkow@64267  1730 lemma sum_head_upt_Suc:  nipkow@64267  1731  "m < n \ sum f {m.. n + 1"  nipkow@64267  1737  shows "sum f {m..n + p} = sum f {m..n} + sum f {n + 1..n + p}"  nipkow@31501  1738 proof-  wenzelm@60758  1739  have "{m .. n+p} = {m..n} \ {n+1..n+p}" using \m \ n+1\ by auto  nipkow@64267  1740  thus ?thesis by (auto simp: ivl_disj_int sum.union_disjoint  nipkow@31501  1741  atLeastSucAtMost_greaterThanAtMost)  nipkow@31501  1742 qed  nipkow@28068  1743 nipkow@64267  1744 lemmas sum_add_nat_ivl = sum.atLeast_lessThan_concat  nipkow@64267  1745 nipkow@64267  1746 lemma sum_diff_nat_ivl:  nipkow@15539  1747 fixes f :: "nat \ 'a::ab_group_add"  nipkow@15539  1748 shows "\ m \ n; n \ p \ \  nipkow@64267  1749  sum f {m.. ('a::ab_group_add)"  nipkow@64267  1756  shows "sum (\k. f k - f(k + 1)) {(m::nat) .. n} =  nipkow@31505  1757  (if m <= n then f m - f(n + 1) else 0)"  nipkow@31505  1758 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)  nipkow@31505  1759 nipkow@64267  1760 lemma sum_nat_group: "(\m(i,j)\{(i,j). i+j < n}. f i j) = (\ki\k. f i (k - i))"  nipkow@64267  1769  apply (simp add: sum.Sigma)  nipkow@64267  1770  apply (rule sum.reindex_bij_witness[where j="\(i, j). (i+j, i)" and i="\(k, i). (i, k - i)"])  lp15@60150  1771  apply auto  lp15@60150  1772  done  lp15@60150  1773 nipkow@64267  1774 lemma sum_triangle_reindex_eq:  lp15@60150  1775  fixes n :: nat  lp15@60150  1776  shows "(\(i,j)\{(i,j). i+j \ n}. f i j) = (\k\n. \i\k. f i (k - i))"  nipkow@64267  1777 using sum_triangle_reindex [of f "Suc n"]  lp15@60150  1778 by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost)  lp15@60150  1779 nipkow@64267  1780 lemma nat_diff_sum_reindex: "(\iiShifting bounds\  nipkow@16733  1785 nipkow@64267  1786 lemma sum_shift_bounds_nat_ivl:  nipkow@64267  1787  "sum f {m+k.. sum f {Suc 0..k} = sum f {0..k}"  nipkow@64267  1804 by(simp add:sum_head_Suc)  nipkow@64267  1805 nipkow@64267  1806 lemma sum_shift_lb_Suc0_0_upt:  nipkow@64267  1807  "f(0::nat) = 0 \ sum f {Suc 0.. 'a::comm_monoid_add"  haftmann@52380  1814  shows "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))"  haftmann@52380  1815 proof (induct n)  haftmann@52380  1816  case 0 show ?case by simp  haftmann@52380  1817 next  haftmann@52380  1818  case (Suc n) note IH = this  haftmann@52380  1819  have "(\i\Suc (Suc n). f i) = (\i\Suc n. f i) + f (Suc (Suc n))"  nipkow@64267  1820  by (rule sum_atMost_Suc)  haftmann@52380  1821  also have "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))"  haftmann@52380  1822  by (rule IH)  haftmann@52380  1823  also have "f 0 + (\i\n. f (Suc i)) + f (Suc (Suc n)) =  haftmann@52380  1824  f 0 + ((\i\n. f (Suc i)) + f (Suc (Suc n)))"  haftmann@57512  1825  by (rule add.assoc)  haftmann@52380  1826  also have "(\i\n. f (Suc i)) + f (Suc (Suc n)) = (\i\Suc n. f (Suc i))"  nipkow@64267  1827  by (rule sum_atMost_Suc [symmetric])  haftmann@52380  1828  finally show ?case .  haftmann@52380  1829 qed  haftmann@52380  1830 nipkow@64267  1831 lemma sum_lessThan_Suc_shift:  eberlm@63099  1832  "(\ii 'a::comm_monoid_add"  lp15@62379  1837  shows "(\i\n. f i) = f 0 + (\i (\i = m..n. f i) = f n + (\i = m.. 'a::ab_group_add"  lp15@56238  1845  assumes "m \ Suc n"  lp15@56238  1846  shows "(\i = m..n. f(Suc i) - f i) = f (Suc n) - f m"  lp15@56238  1847 using assms by (induct n) (auto simp: le_Suc_eq)  lp15@55718  1848 lp15@65273  1849 lemma sum_Suc_diff':  lp15@65273  1850  fixes f :: "nat \ 'a::ab_group_add"  lp15@65273  1851  assumes "m \ n"  lp15@65273  1852  shows "(\i = m..i = 0..n. (\j = 0..j = 0..i = Suc j..n. a i j)"  nipkow@64267  1857  by (induction n) (auto simp: sum.distrib)  nipkow@64267  1858 nipkow@64267  1859 lemma nested_sum_swap':  lp15@56215  1860  "(\i\n. (\jji = Suc j..n. a i j)"  nipkow@64267  1861  by (induction n) (auto simp: sum.distrib)  nipkow@64267  1862 nipkow@64267  1863 lemma sum_atLeast1_atMost_eq:  nipkow@64267  1864  "sum f {Suc 0..n} = (\k = (\kTelescoping\  eberlm@61524  1875 nipkow@64267  1876 lemma sum_telescope:  eberlm@61524  1877  fixes f::"nat \ 'a::ab_group_add"  nipkow@64267  1878  shows "sum (\i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)"  eberlm@61524  1879  by (induct i) simp_all  eberlm@61524  1880 nipkow@64267  1881 lemma sum_telescope'':  eberlm@61524  1882  assumes "m \ n"  eberlm@61524  1883  shows "(\k\{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)"  eberlm@61524  1884  by (rule dec_induct[OF assms]) (simp_all add: algebra_simps)  eberlm@61524  1885 nipkow@64267  1886 lemma sum_lessThan_telescope:  eberlm@63721  1887  "(\nnThe formula for geometric sums\  ballarin@17149  1896 nipkow@66490  1897 lemma sum_power2: "(\i=0.. 1"  hoelzl@56193  1902  shows "(\i 0" by simp_all  hoelzl@56193  1905  moreover have "(\iy \ 0$$  haftmann@36307  1907  ultimately show ?thesis by simp  haftmann@36307  1908 qed  haftmann@36307  1909 nipkow@64267  1910 lemma diff_power_eq_sum:  lp15@60162  1911  fixes y :: "'a::{comm_ring,monoid_mult}"  lp15@60162  1912  shows  lp15@60162  1913  "x ^ (Suc n) - y ^ (Suc n) =  lp15@60162  1914  (x - y) * (\pppp\\COMPLEX_POLYFUN\ in HOL Light\  lp15@60162  1931  fixes x :: "'a::{comm_ring,monoid_mult}"  lp15@60162  1932  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  1956  by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)  lp15@65578  1957 lp15@65578  1958 lemma sum_power_shift:  lp15@65578  1959  fixes x :: "'a::{comm_ring,monoid_mult}"  lp15@65578  1960  assumes "m \ n"  lp15@65578  1961  shows "(\i=m..n. x^i) = x^m * (\i\n-m. x^i)"  lp15@65578  1962 proof -  lp15@65578  1963  have "(\i=m..n. x^i) = x^m * (\i=m..n. x^(i-m))"  lp15@65578  1964  by (simp add: sum_distrib_left power_add [symmetric])  lp15@65578  1965  also have "(\i=m..n. x^(i-m)) = (\i\n-m. x^i)"  lp15@65578  1966  using \m \ n\ by (intro sum.reindex_bij_witness[where j="\i. i - m" and i="\i. i + m"]) auto  lp15@65578  1967  finally show ?thesis .  lp15@65578  1968 qed  lp15@65578  1969 lp15@65578  1970 lemma sum_gp_multiplied:  lp15@65578  1971  fixes x :: "'a::{comm_ring,monoid_mult}"  lp15@65578  1972  assumes "m \ n"  lp15@65578  1973  shows "(1 - x) * (\i=m..n. x^i) = x^m - x^Suc n"  lp15@65578  1974 proof -  lp15@65578  1975  have "(1 - x) * (\i=m..n. x^i) = x^m * (1 - x) * (\i\n-m. x^i)"  lp15@65578  1976  by (metis mult.assoc mult.commute assms sum_power_shift)  lp15@65578  1977  also have "... =x^m * (1 - x^Suc(n-m))"  lp15@65578  1978  by (metis mult.assoc sum_gp_basic)  lp15@65578  1979  also have "... = x^m - x^Suc n"  lp15@65578  1980  using assms  lp15@65578  1981  by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)  lp15@65578  1982  finally show ?thesis .  lp15@65578  1983 qed  lp15@65578  1984 lp15@65578  1985 lemma sum_gp:  lp15@65578  1986  fixes x :: "'a::{comm_ring,division_ring}"  lp15@65578  1987  shows "(\i=m..n. x^i) =  lp15@65578  1988  (if n < m then 0  lp15@65578  1989  else if x = 1 then of_nat((n + 1) - m)  lp15@65578  1990  else (x^m - x^Suc n) / (1 - x))"  lp15@65578  1991 using sum_gp_multiplied [of m n x] apply auto  lp15@65578  1992 by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)  lp15@65578  1993 lp15@65578  1994 subsection\Geometric progressions\  lp15@65578  1995 lp15@65578  1996 lemma sum_gp0:  lp15@65578  1997  fixes x :: "'a::{comm_ring,division_ring}"  lp15@65578  1998  shows "(\i\n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"  lp15@65578  1999  using sum_gp_basic[of x n]  lp15@65578  2000  by (simp add: mult.commute divide_simps)  lp15@65578  2001 lp15@65578  2002 lemma sum_power_add:  lp15@65578  2003  fixes x :: "'a::{comm_ring,monoid_mult}"  lp15@65578  2004  shows "(\i\I. x^(m+i)) = x^m * (\i\I. x^i)"  lp15@65578  2005  by (simp add: sum_distrib_left power_add)  lp15@65578  2006 lp15@65578  2007 lemma sum_gp_offset:  lp15@65578  2008  fixes x :: "'a::{comm_ring,division_ring}"  lp15@65578  2009  shows "(\i=m..m+n. x^i) =  lp15@65578  2010  (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"  lp15@65578  2011  using sum_gp [of x m "m+n"]  lp15@65578  2012  by (auto simp: power_add algebra_simps)  lp15@65578  2013 lp15@65578  2014 lemma sum_gp_strict:  lp15@65578  2015  fixes x :: "'a::{comm_ring,division_ring}"  lp15@65578  2016  shows "(\iThe formula for arithmetic sums\  kleing@19469  2020 huffman@47222  2021 lemma gauss_sum:  hoelzl@56193  2022  "(2::'a::comm_semiring_1)*(\i\{1..n}. of_nat i) = of_nat n*((of_nat n)+1)"  kleing@19469  2023 proof (induct n)  kleing@19469  2024  case 0  kleing@19469  2025  show ?case by simp  kleing@19469  2026 next  kleing@19469  2027  case (Suc n)  huffman@47222  2028  then show ?case  huffman@47222  2029  by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one)  huffman@47222  2030  (* FIXME: make numeral cancellation simprocs work for semirings *)  kleing@19469  2031 qed  kleing@19469  2032 kleing@19469  2033 theorem arith_series_general:  huffman@47222  2034  "(2::'a::comm_semiring_1) * (\i\{.. 1"  kleing@19469  2038  let ?I = "\i. of_nat i" and ?n = "of_nat n"  kleing@19469  2039  have  kleing@19469  2040  "(\i\{..i\{..i\{.. = ?n*a + (\i\{.. = (?n*a + d*(\i\{1.. = 2*?n*a + d*2*(\i\{1..i\{1..n - 1}. ?I i) = (2*?n*a + d*?I (n - 1)*?I n)"  haftmann@57514  2053  by (simp only: mult.assoc gauss_sum [of "n - 1"], unfold One_nat_def)  haftmann@57514  2054  (simp add: mult.commute trans [OF add.commute of_nat_Suc [symmetric]])  huffman@47222  2055  finally show ?thesis  huffman@47222  2056  unfolding mult_2 by (simp add: algebra_simps)  kleing@19469  2057 next  kleing@19469  2058  assume "\(n > 1)"  kleing@19469  2059  hence "n = 1 \ n = 0" by auto  huffman@47222  2060  thus ?thesis by (auto simp: mult_2)  kleing@19469  2061 qed  kleing@19469  2062 kleing@19469  2063 lemma arith_series_nat:  huffman@47222  2064  "(2::nat) * (\i\{..i\{..i\{..x. Q x \ P x \ (\xxxDivision remainder\  haftmann@63417  2083 haftmann@63417  2084 lemma range_mod:  haftmann@63417  2085  fixes n :: nat  haftmann@63417  2086  assumes "n > 0"  haftmann@63417  2087  shows "range (\m. m mod n) = {0.. ?A \ m \ ?B"  haftmann@63417  2091  proof  haftmann@63417  2092  assume "m \ ?A"  haftmann@63417  2093  with assms show "m \ ?B"  wenzelm@63915  2094  by auto  haftmann@63417  2095  next  haftmann@63417  2096  assume "m \ ?B"  haftmann@63417  2097  moreover have "m mod n \ ?A"  haftmann@63417  2098  by (rule rangeI)  haftmann@63417  2099  ultimately show "m \ ?A"  haftmann@63417  2100  by simp  haftmann@63417  2101  qed  haftmann@63417  2102 qed  haftmann@63417  2103 haftmann@63417  2104 wenzelm@60758  2105 subsection \Products indexed over intervals\  paulson@29960  2106 wenzelm@61955  2107 syntax (ASCII)  nipkow@64272  2108  "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)  nipkow@64272  2109  "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@64272  2110  "_upt_prod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10)  nipkow@64272  2111  "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10)  wenzelm@61955  2112 paulson@29960  2113 syntax (latex_prod output)  nipkow@64272  2114  "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b"  wenzelm@63935  2115  ("(3\<^latex>\$\\prod_{\_ = _\<^latex>\}^{\_\<^latex>\}$\ _)" [0,0,0,10] 10)  nipkow@64272  2116  "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b"  wenzelm@63935  2117  ("(3\<^latex>\$\\prod_{\_ = _\<^latex>\}^{<\_\<^latex>\}$\ _)" [0,0,0,10] 10)  nipkow@64272  2118  "_upt_prod" :: "idt \ 'a \ 'b \ 'b"  wenzelm@63935  2119  ("(3\<^latex>\$\\prod_{\_ < _\<^latex>\}$\ _)" [0,0,10] 10)  nipkow@64272  2120  "_upto_prod" :: "idt \ 'a \ 'b \ 'b"  wenzelm@63935  2121  ("(3\<^latex>\$\\prod_{\_ \ _\<^latex>\}$\ _)" [0,0,10] 10)  paulson@29960  2122 wenzelm@61955  2123 syntax  nipkow@64272  2124  "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@64272  2125  "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@64272  2126  "_upt_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@64272  2127  "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  wenzelm@61955  2128 paulson@29960  2129 translations  nipkow@64272  2130  "\x=a..b. t" \ "CONST prod (\x. t) {a..b}"  nipkow@64272  2131  "\x=a.. "CONST prod (\x. t) {a..i\n. t" \ "CONST prod (\i. t) {..n}"  nipkow@64272  2133  "\i "CONST prod (\i. t) {..{int i..int (i+j)}"  lp15@55242  2136  by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)  lp15@55242  2137 nipkow@64272  2138 lemma prod_int_eq: "prod int {i..j} = \{int i..int j}"  lp15@55242  2139 proof (cases "i \ j")  lp15@55242  2140  case True  lp15@55242  2141  then show ?thesis  nipkow@64272  2142  by (metis le_iff_add prod_int_plus_eq)  lp15@55242  2143 next  lp15@55242  2144  case False  lp15@55242  2145  then show ?thesis  lp15@55242  2146  by auto  lp15@55242  2147 qed  lp15@55242  2148 eberlm@61524  2149 haftmann@63417  2150 subsubsection \Shifting bounds\  eberlm@61524  2151 nipkow@64272  2152 lemma prod_shift_bounds_nat_ivl:  nipkow@64272  2153  "prod f {m+k..ii b \ prod f {a.. Suc n"  nipkow@64272  2179  shows "prod f {m..Suc n} = f (Suc n) * prod f {m..n}"  eberlm@61524  2180 proof -  eberlm@61524  2181  from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto  nipkow@64272  2182  also have "prod f \ = f (Suc n) * prod f {m..n}" by simp  eberlm@61524  2183  finally show ?thesis .  eberlm@61524  2184 qed  eberlm@61524  2185 eberlm@62128  2186 eberlm@62128  2187 subsection \Efficient folding over intervals\  eberlm@62128  2188 eberlm@62128  2189 function fold_atLeastAtMost_nat where  eberlm@62128  2190  [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc =  eberlm@62128  2191  (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a acc))"  eberlm@62128  2192 by pat_completeness auto  eberlm@62128  2193 termination by (relation "measure (\(_,a,b,_). Suc b - a)") auto  eberlm@62128  2194 eberlm@62128  2195 lemma fold_atLeastAtMost_nat:  eberlm@62128  2196  assumes "comp_fun_commute f"  eberlm@62128  2197  shows "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}"  eberlm@62128  2198 using assms  eberlm@62128  2199 proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases)  eberlm@62128  2200  case (1 f a b acc)  eberlm@62128  2201  interpret comp_fun_commute f by fact  eberlm@62128  2202  show ?case  eberlm@62128  2203  proof (cases "a > b")  eberlm@62128  2204  case True  eberlm@62128  2205  thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto  eberlm@62128  2206  next  eberlm@62128  2207  case False  eberlm@62128  2208  with 1 show ?thesis  eberlm@62128  2209  by (subst fold_atLeastAtMost_nat.simps)  eberlm@62128  2210  (auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm)  eberlm@62128  2211  qed  eberlm@62128  2212 qed  eberlm@62128  2213 nipkow@64267  2214 lemma sum_atLeastAtMost_code:  nipkow@64267  2215  "sum f {a..b} = fold_atLeastAtMost_nat (\a acc. f a + acc) a b 0"  eberlm@62128  2216 proof -  eberlm@62128  2217  have "comp_fun_commute (\a. op + (f a))"  eberlm@62128  2218  by unfold_locales (auto simp: o_def add_ac)  eberlm@62128  2219  thus ?thesis  nipkow@64267  2220  by (simp add: sum.eq_fold fold_atLeastAtMost_nat o_def)  eberlm@62128  2221 qed  eberlm@62128  2222 nipkow@64272  2223 lemma prod_atLeastAtMost_code:  nipkow@64272  2224  "prod f {a..b} = fold_atLeastAtMost_nat (\a acc. f a * acc) a b 1"  eberlm@62128  2225 proof -  eberlm@62128  2226  have "comp_fun_commute (\a. op * (f a))"  eberlm@62128  2227  by unfold_locales (auto simp: o_def mult_ac)  eberlm@62128  2228  thus ?thesis  nipkow@64272  2229  by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def)  eberlm@62128  2230 qed  eberlm@62128  2231 eberlm@62128  2232 (* TODO: Add support for more kinds of intervals here *)  eberlm@62128  2233 haftmann@63417  2234 haftmann@63417  2235 subsection \Transfer setup\  haftmann@63417  2236 haftmann@63417  2237 lemma transfer_nat_int_set_functions:  haftmann@63417  2238  "{..n} = nat  {0..int n}"  haftmann@63417  2239  "{m..n} = nat  {int m..int n}" (* need all variants of these! *)  haftmann@63417  2240  apply (auto simp add: image_def)  haftmann@63417  2241  apply (rule_tac x = "int x" in bexI)  haftmann@63417  2242  apply auto  haftmann@63417  2243  apply (rule_tac x = "int x" in bexI)  haftmann@63417  2244  apply auto  haftmann@63417  2245  done  haftmann@63417  2246 haftmann@63417  2247 lemma transfer_nat_int_set_function_closures:  haftmann@63417  2248  "x >= 0 \ nat_set {x..y}"  haftmann@63417  2249  by (simp add: nat_set_def)  haftmann@63417  2250 haftmann@63417  2251 declare transfer_morphism_nat_int[transfer add  haftmann@63417  2252  return: transfer_nat_int_set_functions  haftmann@63417  2253  transfer_nat_int_set_function_closures  haftmann@63417  2254 ]  haftmann@63417  2255 haftmann@63417  2256 lemma transfer_int_nat_set_functions:  haftmann@63417  2257  "is_nat m \ is_nat n \ {m..n} = int  {nat m..nat n}"  haftmann@63417  2258  by (simp only: is_nat_def transfer_nat_int_set_functions  haftmann@63417  2259  transfer_nat_int_set_function_closures  haftmann@63417  2260  transfer_nat_int_set_return_embed nat_0_le  haftmann@63417  2261  cong: transfer_nat_int_set_cong)  haftmann@63417  2262 haftmann@63417  2263 lemma transfer_int_nat_set_function_closures:  haftmann@63417  2264  "is_nat x \ nat_set {x..y}"  haftmann@63417  2265  by (simp only: transfer_nat_int_set_function_closures is_nat_def)  haftmann@63417  2266 haftmann@63417  2267 declare transfer_morphism_int_nat[transfer add  haftmann@63417  2268  return: transfer_int_nat_set_functions  haftmann@63417  2269  transfer_int_nat_set_function_closures  haftmann@63417  2270 ]  haftmann@63417  2271 nipkow@8924  2272 end `