src/HOL/Set_Interval.thy
 author paulson Mon May 23 15:33:24 2016 +0100 (2016-05-23) changeset 63114 27afe7af7379 parent 63099 af0e964aad7b child 63171 a0088f1c049d permissions -rw-r--r--
Lots of new material for multivariate analysis
 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  blanchet@55088  17 imports Lattices_Big 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 paulson@13850  133 lemma atLeast_subset_iff [iff]:  paulson@15418  134  "(atLeast x \ atLeast y) = (y \ (x::'a::order))"  paulson@15418  135 by (blast intro: order_trans)  paulson@13850  136 paulson@13850  137 lemma atLeast_eq_iff [iff]:  paulson@15418  138  "(atLeast x = atLeast y) = (x = (y::'a::linorder))"  paulson@13850  139 by (blast intro: order_antisym order_trans)  paulson@13850  140 paulson@13850  141 lemma greaterThan_subset_iff [iff]:  paulson@15418  142  "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))"  paulson@15418  143 apply (auto simp add: greaterThan_def)  paulson@15418  144  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  145 done  paulson@13850  146 paulson@13850  147 lemma greaterThan_eq_iff [iff]:  paulson@15418  148  "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"  paulson@15418  149 apply (rule iffI)  paulson@15418  150  apply (erule equalityE)  haftmann@29709  151  apply simp_all  paulson@13850  152 done  paulson@13850  153 paulson@15418  154 lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))"  paulson@13850  155 by (blast intro: order_trans)  paulson@13850  156 paulson@15418  157 lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"  paulson@13850  158 by (blast intro: order_antisym order_trans)  paulson@13850  159 paulson@13850  160 lemma lessThan_subset_iff [iff]:  paulson@15418  161  "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))"  paulson@15418  162 apply (auto simp add: lessThan_def)  paulson@15418  163  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  164 done  paulson@13850  165 paulson@13850  166 lemma lessThan_eq_iff [iff]:  paulson@15418  167  "(lessThan x = lessThan y) = (x = (y::'a::linorder))"  paulson@15418  168 apply (rule iffI)  paulson@15418  169  apply (erule equalityE)  haftmann@29709  170  apply simp_all  ballarin@13735  171 done  ballarin@13735  172 hoelzl@40703  173 lemma lessThan_strict_subset_iff:  hoelzl@40703  174  fixes m n :: "'a::linorder"  hoelzl@40703  175  shows "{.. m < n"  hoelzl@40703  176  by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)  ballarin@13735  177 hoelzl@57448  178 lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \ {b <..} \ b < a"  hoelzl@57448  179  by auto  hoelzl@57448  180 hoelzl@57448  181 lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \ {..< b} \ a < b"  hoelzl@57448  182  by auto  hoelzl@57448  183 hoelzl@62369  184 lemma (in preorder) Ioi_le_Ico: "{a <..} \ {a ..}"  hoelzl@62369  185  by (auto intro: less_imp_le)  hoelzl@62369  186 wenzelm@60758  187 subsection \Two-sided intervals\  ballarin@13735  188 nipkow@24691  189 context ord  nipkow@24691  190 begin  nipkow@24691  191 blanchet@54147  192 lemma greaterThanLessThan_iff [simp]:  haftmann@25062  193  "(i : {l<..The above four lemmas could be declared as iffs. Unfortunately this  haftmann@52729  209 breaks many proofs. Since it only helps blast, it is better to leave them  wenzelm@60758  210 alone.\  nipkow@32436  211 hoelzl@50999  212 lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \ {..< b }"  hoelzl@50999  213  by auto  hoelzl@50999  214 nipkow@24691  215 end  ballarin@13735  216 wenzelm@60758  217 subsubsection\Emptyness, singletons, subset\  nipkow@15554  218 nipkow@24691  219 context order  nipkow@24691  220 begin  nipkow@15554  221 nipkow@32400  222 lemma atLeastatMost_empty[simp]:  nipkow@32400  223  "b < a \ {a..b} = {}"  nipkow@32400  224 by(auto simp: atLeastAtMost_def atLeast_def atMost_def)  nipkow@32400  225 nipkow@32400  226 lemma atLeastatMost_empty_iff[simp]:  nipkow@32400  227  "{a..b} = {} \ (~ a <= b)"  nipkow@32400  228 by auto (blast intro: order_trans)  nipkow@32400  229 nipkow@32400  230 lemma atLeastatMost_empty_iff2[simp]:  nipkow@32400  231  "{} = {a..b} \ (~ a <= b)"  nipkow@32400  232 by auto (blast intro: order_trans)  nipkow@32400  233 nipkow@32400  234 lemma atLeastLessThan_empty[simp]:  nipkow@32400  235  "b <= a \ {a.. (~ a < b)"  nipkow@32400  240 by auto (blast intro: le_less_trans)  nipkow@32400  241 nipkow@32400  242 lemma atLeastLessThan_empty_iff2[simp]:  nipkow@32400  243  "{} = {a.. (~ a < b)"  nipkow@32400  244 by auto (blast intro: le_less_trans)  nipkow@15554  245 nipkow@32400  246 lemma greaterThanAtMost_empty[simp]: "l \ k ==> {k<..l} = {}"  nipkow@17719  247 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)  nipkow@17719  248 nipkow@32400  249 lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ ~ k < l"  nipkow@32400  250 by auto (blast intro: less_le_trans)  nipkow@32400  251 nipkow@32400  252 lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ ~ k < l"  nipkow@32400  253 by auto (blast intro: less_le_trans)  nipkow@32400  254 haftmann@29709  255 lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. {a .. b} = {a}" by simp  hoelzl@36846  262 nipkow@32400  263 lemma atLeastatMost_subset_iff[simp]:  nipkow@32400  264  "{a..b} <= {c..d} \ (~ a <= b) | c <= a & b <= d"  nipkow@32400  265 unfolding atLeastAtMost_def atLeast_def atMost_def  nipkow@32400  266 by (blast intro: order_trans)  nipkow@32400  267 nipkow@32400  268 lemma atLeastatMost_psubset_iff:  nipkow@32400  269  "{a..b} < {c..d} \  nipkow@32400  270  ((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d"  nipkow@39302  271 by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)  nipkow@32400  272 nipkow@51334  273 lemma Icc_eq_Icc[simp]:  nipkow@51334  274  "{l..h} = {l'..h'} = (l=l' \ h=h' \ \ l\h \ \ l'\h')"  nipkow@51334  275 by(simp add: order_class.eq_iff)(auto intro: order_trans)  nipkow@51334  276 hoelzl@36846  277 lemma atLeastAtMost_singleton_iff[simp]:  hoelzl@36846  278  "{a .. b} = {c} \ a = b \ b = c"  hoelzl@36846  279 proof  hoelzl@36846  280  assume "{a..b} = {c}"  wenzelm@53374  281  hence *: "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp  wenzelm@60758  282  with \{a..b} = {c}\ have "c \ a \ b \ c" by auto  wenzelm@53374  283  with * show "a = b \ b = c" by auto  hoelzl@36846  284 qed simp  hoelzl@36846  285 nipkow@51334  286 lemma Icc_subset_Ici_iff[simp]:  nipkow@51334  287  "{l..h} \ {l'..} = (~ l\h \ l\l')"  nipkow@51334  288 by(auto simp: subset_eq intro: order_trans)  nipkow@51334  289 nipkow@51334  290 lemma Icc_subset_Iic_iff[simp]:  nipkow@51334  291  "{l..h} \ {..h'} = (~ l\h \ h\h')"  nipkow@51334  292 by(auto simp: subset_eq intro: order_trans)  nipkow@51334  293 nipkow@51334  294 lemma not_Ici_eq_empty[simp]: "{l..} \ {}"  nipkow@51334  295 by(auto simp: set_eq_iff)  nipkow@51334  296 nipkow@51334  297 lemma not_Iic_eq_empty[simp]: "{..h} \ {}"  nipkow@51334  298 by(auto simp: set_eq_iff)  nipkow@51334  299 nipkow@51334  300 lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric]  nipkow@51334  301 lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric]  nipkow@51334  302 nipkow@24691  303 end  paulson@14485  304 nipkow@51334  305 context no_top  nipkow@51334  306 begin  nipkow@51334  307 nipkow@51334  308 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  309 lemma not_UNIV_le_Icc[simp]: "\ UNIV \ {l..h}"  nipkow@51334  310 using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  311 nipkow@51334  312 lemma not_UNIV_le_Iic[simp]: "\ UNIV \ {..h}"  nipkow@51334  313 using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  314 nipkow@51334  315 lemma not_Ici_le_Icc[simp]: "\ {l..} \ {l'..h'}"  nipkow@51334  316 using gt_ex[of h']  nipkow@51334  317 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  318 nipkow@51334  319 lemma not_Ici_le_Iic[simp]: "\ {l..} \ {..h'}"  nipkow@51334  320 using gt_ex[of h']  nipkow@51334  321 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  322 nipkow@51334  323 end  nipkow@51334  324 nipkow@51334  325 context no_bot  nipkow@51334  326 begin  nipkow@51334  327 nipkow@51334  328 lemma not_UNIV_le_Ici[simp]: "\ UNIV \ {l..}"  nipkow@51334  329 using lt_ex[of l] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  330 nipkow@51334  331 lemma not_Iic_le_Icc[simp]: "\ {..h} \ {l'..h'}"  nipkow@51334  332 using lt_ex[of l']  nipkow@51334  333 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  334 nipkow@51334  335 lemma not_Iic_le_Ici[simp]: "\ {..h} \ {l'..}"  nipkow@51334  336 using lt_ex[of l']  nipkow@51334  337 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  338 nipkow@51334  339 end  nipkow@51334  340 nipkow@51334  341 nipkow@51334  342 context no_top  nipkow@51334  343 begin  nipkow@51334  344 nipkow@51334  345 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  346 lemma not_UNIV_eq_Icc[simp]: "\ UNIV = {l'..h'}"  nipkow@51334  347 using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  348 nipkow@51334  349 lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric]  nipkow@51334  350 nipkow@51334  351 lemma not_UNIV_eq_Iic[simp]: "\ UNIV = {..h'}"  nipkow@51334  352 using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  353 nipkow@51334  354 lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric]  nipkow@51334  355 nipkow@51334  356 lemma not_Icc_eq_Ici[simp]: "\ {l..h} = {l'..}"  nipkow@51334  357 unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast  nipkow@51334  358 nipkow@51334  359 lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric]  nipkow@51334  360 nipkow@51334  361 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  362 lemma not_Iic_eq_Ici[simp]: "\ {..h} = {l'..}"  nipkow@51334  363 using not_Ici_le_Iic[of l' h] by blast  nipkow@51334  364 nipkow@51334  365 lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric]  nipkow@51334  366 nipkow@51334  367 end  nipkow@51334  368 nipkow@51334  369 context no_bot  nipkow@51334  370 begin  nipkow@51334  371 nipkow@51334  372 lemma not_UNIV_eq_Ici[simp]: "\ UNIV = {l'..}"  nipkow@51334  373 using lt_ex[of l'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  374 nipkow@51334  375 lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric]  nipkow@51334  376 nipkow@51334  377 lemma not_Icc_eq_Iic[simp]: "\ {l..h} = {..h'}"  nipkow@51334  378 unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast  nipkow@51334  379 nipkow@51334  380 lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric]  nipkow@51334  381 nipkow@51334  382 end  nipkow@51334  383 nipkow@51334  384 hoelzl@53216  385 context dense_linorder  hoelzl@42891  386 begin  hoelzl@42891  387 hoelzl@42891  388 lemma greaterThanLessThan_empty_iff[simp]:  hoelzl@42891  389  "{ a <..< b } = {} \ b \ a"  hoelzl@42891  390  using dense[of a b] by (cases "a < b") auto  hoelzl@42891  391 hoelzl@42891  392 lemma greaterThanLessThan_empty_iff2[simp]:  hoelzl@42891  393  "{} = { a <..< b } \ b \ a"  hoelzl@42891  394  using dense[of a b] by (cases "a < b") auto  hoelzl@42891  395 hoelzl@42901  396 lemma atLeastLessThan_subseteq_atLeastAtMost_iff:  hoelzl@42901  397  "{a ..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  398  using dense[of "max a d" "b"]  hoelzl@42901  399  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  400 hoelzl@42901  401 lemma greaterThanAtMost_subseteq_atLeastAtMost_iff:  hoelzl@42901  402  "{a <.. b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  403  using dense[of "a" "min c b"]  hoelzl@42901  404  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  405 hoelzl@42901  406 lemma greaterThanLessThan_subseteq_atLeastAtMost_iff:  hoelzl@42901  407  "{a <..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  408  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@42901  409  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  410 hoelzl@43657  411 lemma atLeastAtMost_subseteq_atLeastLessThan_iff:  hoelzl@43657  412  "{a .. b} \ { c ..< d } \ (a \ b \ c \ a \ b < d)"  hoelzl@43657  413  using dense[of "max a d" "b"]  hoelzl@43657  414  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@62369  415 eberlm@61524  416 lemma greaterThanLessThan_subseteq_greaterThanLessThan:  eberlm@61524  417  "{a <..< b} \ {c <..< d} \ (a < b \ a \ c \ b \ d)"  eberlm@61524  418  using dense[of "a" "min c b"] dense[of "max a d" "b"]  eberlm@61524  419  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  420 hoelzl@43657  421 lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:  hoelzl@43657  422  "{a <.. b} \ { c ..< d } \ (a < b \ c \ a \ b < d)"  hoelzl@43657  423  using dense[of "a" "min c b"]  hoelzl@43657  424  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  425 hoelzl@43657  426 lemma greaterThanLessThan_subseteq_atLeastLessThan_iff:  hoelzl@43657  427  "{a <..< b} \ { c ..< d } \ (a < b \ c \ a \ b \ d)"  hoelzl@43657  428  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@43657  429  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  430 hoelzl@56328  431 lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff:  hoelzl@56328  432  "{a <..< b} \ { c <.. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@56328  433  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@56328  434  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@56328  435 hoelzl@42891  436 end  hoelzl@42891  437 hoelzl@51329  438 context no_top  hoelzl@51329  439 begin  hoelzl@51329  440 nipkow@51334  441 lemma greaterThan_non_empty[simp]: "{x <..} \ {}"  hoelzl@51329  442  using gt_ex[of x] by auto  hoelzl@51329  443 hoelzl@51329  444 end  hoelzl@51329  445 hoelzl@51329  446 context no_bot  hoelzl@51329  447 begin  hoelzl@51329  448 nipkow@51334  449 lemma lessThan_non_empty[simp]: "{..< x} \ {}"  hoelzl@51329  450  using lt_ex[of x] by auto  hoelzl@51329  451 hoelzl@51329  452 end  hoelzl@51329  453 nipkow@32408  454 lemma (in linorder) atLeastLessThan_subset_iff:  nipkow@32408  455  "{a.. b <= a | c<=a & b<=d"  nipkow@32408  456 apply (auto simp:subset_eq Ball_def)  nipkow@32408  457 apply(frule_tac x=a in spec)  nipkow@32408  458 apply(erule_tac x=d in allE)  nipkow@32408  459 apply (simp add: less_imp_le)  nipkow@32408  460 done  nipkow@32408  461 hoelzl@40703  462 lemma atLeastLessThan_inj:  hoelzl@40703  463  fixes a b c d :: "'a::linorder"  hoelzl@40703  464  assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"  hoelzl@40703  465  shows "a = c" "b = d"  hoelzl@40703  466 using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+  hoelzl@40703  467 hoelzl@40703  468 lemma atLeastLessThan_eq_iff:  hoelzl@40703  469  fixes a b c d :: "'a::linorder"  hoelzl@40703  470  assumes "a < b" "c < d"  hoelzl@40703  471  shows "{a ..< b} = {c ..< d} \ a = c \ b = d"  hoelzl@40703  472  using atLeastLessThan_inj assms by auto  hoelzl@40703  473 hoelzl@57447  474 lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \ (b \ a \ d \ c) \ a = c \ b = d"  hoelzl@57447  475  by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le)  hoelzl@57447  476 hoelzl@57447  477 lemma (in order) Iio_Int_singleton: "{.. {x} = (if x < k then {x} else {})"  hoelzl@57447  478  by auto  hoelzl@57447  479 hoelzl@57447  480 lemma (in linorder) Ioc_subset_iff: "{a<..b} \ {c<..d} \ (b \ a \ c \ a \ b \ d)"  hoelzl@57447  481  by (auto simp: subset_eq Ball_def) (metis less_le not_less)  hoelzl@57447  482 haftmann@52729  483 lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \ x = bot"  nipkow@51334  484 by (auto simp: set_eq_iff intro: le_bot)  hoelzl@51328  485 haftmann@52729  486 lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \ x = top"  nipkow@51334  487 by (auto simp: set_eq_iff intro: top_le)  hoelzl@51328  488 nipkow@51334  489 lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff:  nipkow@51334  490  "{x..y} = UNIV \ (x = bot \ y = top)"  nipkow@51334  491 by (auto simp: set_eq_iff intro: top_le le_bot)  hoelzl@51328  492 hoelzl@56949  493 lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \ n = bot"  hoelzl@56949  494  by (auto simp: set_eq_iff not_less le_bot)  hoelzl@56949  495 hoelzl@56949  496 lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \ n = 0"  hoelzl@56949  497  by (simp add: Iio_eq_empty_iff bot_nat_def)  hoelzl@56949  498 noschinl@58970  499 lemma mono_image_least:  noschinl@58970  500  assumes f_mono: "mono f" and f_img: "f  {m ..< n} = {m' ..< n'}" "m < n"  noschinl@58970  501  shows "f m = m'"  noschinl@58970  502 proof -  noschinl@58970  503  from f_img have "{m' ..< n'} \ {}"  noschinl@58970  504  by (metis atLeastLessThan_empty_iff image_is_empty)  noschinl@58970  505  with f_img have "m' \ f  {m ..< n}" by auto  noschinl@58970  506  then obtain k where "f k = m'" "m \ k" by auto  noschinl@58970  507  moreover have "m' \ f m" using f_img by auto  noschinl@58970  508  ultimately show "f m = m'"  noschinl@58970  509  using f_mono by (auto elim: monoE[where x=m and y=k])  noschinl@58970  510 qed  noschinl@58970  511 hoelzl@51328  512 wenzelm@60758  513 subsection \Infinite intervals\  hoelzl@56328  514 hoelzl@56328  515 context dense_linorder  hoelzl@56328  516 begin  hoelzl@56328  517 hoelzl@56328  518 lemma infinite_Ioo:  hoelzl@56328  519  assumes "a < b"  hoelzl@56328  520  shows "\ finite {a<.. {}"  wenzelm@60758  524  using \a < b\ by auto  hoelzl@56328  525  ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b"  hoelzl@56328  526  using Max_in[of "{a <..< b}"] by auto  hoelzl@56328  527  then obtain x where "Max {a <..< b} < x" "x < b"  hoelzl@56328  528  using dense[of "Max {a<.. {a <..< b}"  wenzelm@60758  530  using \a < Max {a <..< b}\ by auto  hoelzl@56328  531  then have "x \ Max {a <..< b}"  hoelzl@56328  532  using fin by auto  wenzelm@60758  533  with \Max {a <..< b} < x\ show False by auto  hoelzl@56328  534 qed  hoelzl@56328  535 hoelzl@56328  536 lemma infinite_Icc: "a < b \ \ finite {a .. b}"  hoelzl@56328  537  using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b]  hoelzl@56328  538  by (auto dest: finite_subset)  hoelzl@56328  539 hoelzl@56328  540 lemma infinite_Ico: "a < b \ \ finite {a ..< b}"  hoelzl@56328  541  using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b]  hoelzl@56328  542  by (auto dest: finite_subset)  hoelzl@56328  543 hoelzl@56328  544 lemma infinite_Ioc: "a < b \ \ finite {a <.. b}"  hoelzl@56328  545  using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b]  hoelzl@56328  546  by (auto dest: finite_subset)  hoelzl@56328  547 hoelzl@56328  548 end  hoelzl@56328  549 hoelzl@56328  550 lemma infinite_Iio: "\ finite {..< a :: 'a :: {no_bot, linorder}}"  hoelzl@56328  551 proof  hoelzl@56328  552  assume "finite {..< a}"  hoelzl@56328  553  then have *: "\x. x < a \ Min {..< a} \ x"  hoelzl@56328  554  by auto  hoelzl@56328  555  obtain x where "x < a"  hoelzl@56328  556  using lt_ex by auto  hoelzl@56328  557 hoelzl@56328  558  obtain y where "y < Min {..< a}"  hoelzl@56328  559  using lt_ex by auto  hoelzl@56328  560  also have "Min {..< a} \ x"  wenzelm@60758  561  using \x < a\ by fact  wenzelm@60758  562  also note \x < a\  hoelzl@56328  563  finally have "Min {..< a} \ y"  hoelzl@56328  564  by fact  wenzelm@60758  565  with \y < Min {..< a}\ show False by auto  hoelzl@56328  566 qed  hoelzl@56328  567 hoelzl@56328  568 lemma infinite_Iic: "\ finite {.. a :: 'a :: {no_bot, linorder}}"  hoelzl@56328  569  using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"]  hoelzl@56328  570  by (auto simp: subset_eq less_imp_le)  hoelzl@56328  571 hoelzl@56328  572 lemma infinite_Ioi: "\ finite {a :: 'a :: {no_top, linorder} <..}"  hoelzl@56328  573 proof  hoelzl@56328  574  assume "finite {a <..}"  hoelzl@56328  575  then have *: "\x. a < x \ x \ Max {a <..}"  hoelzl@56328  576  by auto  hoelzl@56328  577 hoelzl@56328  578  obtain y where "Max {a <..} < y"  hoelzl@56328  579  using gt_ex by auto  hoelzl@56328  580 hoelzl@56328  581  obtain x where "a < x"  hoelzl@56328  582  using gt_ex by auto  hoelzl@56328  583  also then have "x \ Max {a <..}"  hoelzl@56328  584  by fact  wenzelm@60758  585  also note \Max {a <..} < y\  hoelzl@56328  586  finally have "y \ Max { a <..}"  hoelzl@56328  587  by fact  wenzelm@60758  588  with \Max {a <..} < y\ show False by auto  hoelzl@56328  589 qed  hoelzl@56328  590 hoelzl@56328  591 lemma infinite_Ici: "\ finite {a :: 'a :: {no_top, linorder} ..}"  hoelzl@56328  592  using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"]  hoelzl@56328  593  by (auto simp: subset_eq less_imp_le)  hoelzl@56328  594 wenzelm@60758  595 subsubsection \Intersection\  nipkow@32456  596 nipkow@32456  597 context linorder  nipkow@32456  598 begin  nipkow@32456  599 nipkow@32456  600 lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"  nipkow@32456  601 by auto  nipkow@32456  602 nipkow@32456  603 lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"  nipkow@32456  604 by auto  nipkow@32456  605 nipkow@32456  606 lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"  nipkow@32456  607 by auto  nipkow@32456  608 nipkow@32456  609 lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"  nipkow@32456  610 by auto  nipkow@32456  611 nipkow@32456  612 lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"  nipkow@32456  613 by auto  nipkow@32456  614 nipkow@32456  615 lemma Int_atLeastLessThan[simp]: "{a.. {..b} = {.. min a b}"  hoelzl@50417  625  by (auto simp: min_def)  hoelzl@50417  626 hoelzl@57447  627 lemma Ioc_disjoint: "{a<..b} \ {c<..d} = {} \ b \ a \ d \ c \ b \ c \ d \ a"  wenzelm@63092  628  by auto  hoelzl@57447  629 nipkow@32456  630 end  nipkow@32456  631 hoelzl@51329  632 context complete_lattice  hoelzl@51329  633 begin  hoelzl@51329  634 hoelzl@51329  635 lemma  hoelzl@51329  636  shows Sup_atLeast[simp]: "Sup {x ..} = top"  hoelzl@51329  637  and Sup_greaterThanAtLeast[simp]: "x < top \ Sup {x <..} = top"  hoelzl@51329  638  and Sup_atMost[simp]: "Sup {.. y} = y"  hoelzl@51329  639  and Sup_atLeastAtMost[simp]: "x \ y \ Sup { x .. y} = y"  hoelzl@51329  640  and Sup_greaterThanAtMost[simp]: "x < y \ Sup { x <.. y} = y"  hoelzl@51329  641  by (auto intro!: Sup_eqI)  hoelzl@51329  642 hoelzl@51329  643 lemma  hoelzl@51329  644  shows Inf_atMost[simp]: "Inf {.. x} = bot"  hoelzl@51329  645  and Inf_atMostLessThan[simp]: "top < x \ Inf {..< x} = bot"  hoelzl@51329  646  and Inf_atLeast[simp]: "Inf {x ..} = x"  hoelzl@51329  647  and Inf_atLeastAtMost[simp]: "x \ y \ Inf { x .. y} = x"  hoelzl@51329  648  and Inf_atLeastLessThan[simp]: "x < y \ Inf { x ..< y} = x"  hoelzl@51329  649  by (auto intro!: Inf_eqI)  hoelzl@51329  650 hoelzl@51329  651 end  hoelzl@51329  652 hoelzl@51329  653 lemma  hoelzl@53216  654  fixes x y :: "'a :: {complete_lattice, dense_linorder}"  hoelzl@51329  655  shows Sup_lessThan[simp]: "Sup {..< y} = y"  hoelzl@51329  656  and Sup_atLeastLessThan[simp]: "x < y \ Sup { x ..< y} = y"  hoelzl@51329  657  and Sup_greaterThanLessThan[simp]: "x < y \ Sup { x <..< y} = y"  hoelzl@51329  658  and Inf_greaterThan[simp]: "Inf {x <..} = x"  hoelzl@51329  659  and Inf_greaterThanAtMost[simp]: "x < y \ Inf { x <.. y} = x"  hoelzl@51329  660  and Inf_greaterThanLessThan[simp]: "x < y \ Inf { x <..< y} = x"  hoelzl@51329  661  by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded)  nipkow@32456  662 wenzelm@60758  663 subsection \Intervals of natural numbers\  paulson@14485  664 wenzelm@60758  665 subsubsection \The Constant @{term lessThan}\  paulson@15047  666 paulson@14485  667 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"  paulson@14485  668 by (simp add: lessThan_def)  paulson@14485  669 paulson@14485  670 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"  paulson@14485  671 by (simp add: lessThan_def less_Suc_eq, blast)  paulson@14485  672 wenzelm@60758  673 text \The following proof is convenient in induction proofs where  hoelzl@39072  674 new elements get indices at the beginning. So it is used to transform  wenzelm@60758  675 @{term "{..  hoelzl@39072  676 hoelzl@59000  677 lemma zero_notin_Suc_image: "0 \ Suc  A"  hoelzl@59000  678  by auto  hoelzl@59000  679 hoelzl@39072  680 lemma lessThan_Suc_eq_insert_0: "{..The Constant @{term greaterThan}\  paulson@15047  693 paulson@14485  694 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"  paulson@14485  695 apply (simp add: greaterThan_def)  paulson@14485  696 apply (blast dest: gr0_conv_Suc [THEN iffD1])  paulson@14485  697 done  paulson@14485  698 paulson@14485  699 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"  paulson@14485  700 apply (simp add: greaterThan_def)  paulson@14485  701 apply (auto elim: linorder_neqE)  paulson@14485  702 done  paulson@14485  703 paulson@14485  704 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"  paulson@14485  705 by blast  paulson@14485  706 wenzelm@60758  707 subsubsection \The Constant @{term atLeast}\  paulson@15047  708 paulson@14485  709 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"  paulson@14485  710 by (unfold atLeast_def UNIV_def, simp)  paulson@14485  711 paulson@14485  712 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"  paulson@14485  713 apply (simp add: atLeast_def)  paulson@14485  714 apply (simp add: Suc_le_eq)  paulson@14485  715 apply (simp add: order_le_less, blast)  paulson@14485  716 done  paulson@14485  717 paulson@14485  718 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"  paulson@14485  719  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)  paulson@14485  720 paulson@14485  721 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"  paulson@14485  722 by blast  paulson@14485  723 wenzelm@60758  724 subsubsection \The Constant @{term atMost}\  paulson@15047  725 paulson@14485  726 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"  paulson@14485  727 by (simp add: atMost_def)  paulson@14485  728 paulson@14485  729 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"  paulson@14485  730 apply (simp add: atMost_def)  paulson@14485  731 apply (simp add: less_Suc_eq order_le_less, blast)  paulson@14485  732 done  paulson@14485  733 paulson@14485  734 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"  paulson@14485  735 by blast  paulson@14485  736 wenzelm@60758  737 subsubsection \The Constant @{term atLeastLessThan}\  paulson@15047  738 wenzelm@60758  739 text\The orientation of the following 2 rules is tricky. The lhs is  nipkow@24449  740 defined in terms of the rhs. Hence the chosen orientation makes sense  nipkow@24449  741 in this theory --- the reverse orientation complicates proofs (eg  nipkow@24449  742 nontermination). But outside, when the definition of the lhs is rarely  nipkow@24449  743 used, the opposite orientation seems preferable because it reduces a  wenzelm@60758  744 specific concept to a more general one.\  nipkow@28068  745 paulson@15047  746 lemma atLeast0LessThan: "{0::nat..Intervals of nats with @{term Suc}\  paulson@15047  759 wenzelm@60758  760 text\Not a simprule because the RHS is too messy.\  paulson@15047  761 lemma atLeastLessThanSuc:  paulson@15047  762  "{m.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  786 by (auto simp add: atLeastAtMost_def)  nipkow@15554  787 noschinl@45932  788 lemma atLeastAtMost_insertL: "m \ n \ insert m {Suc m..n} = {m ..n}"  noschinl@45932  789 by auto  noschinl@45932  790 wenzelm@60758  791 text \The analogous result is useful on @{typ int}:\  kleing@43157  792 (* here, because we don't have an own int section *)  kleing@43157  793 lemma atLeastAtMostPlus1_int_conv:  kleing@43157  794  "m <= 1+n \ {m..1+n} = insert (1+n) {m..n::int}"  kleing@43157  795  by (auto intro: set_eqI)  kleing@43157  796 paulson@33044  797 lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j..Intervals and numerals\  lp15@57113  803 wenzelm@61799  804 lemma lessThan_nat_numeral: \\Evaluation for specific numerals\  lp15@57113  805  "lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))"  lp15@57113  806  by (simp add: numeral_eq_Suc lessThan_Suc)  lp15@57113  807 wenzelm@61799  808 lemma atMost_nat_numeral: \\Evaluation for specific numerals\  lp15@57113  809  "atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))"  lp15@57113  810  by (simp add: numeral_eq_Suc atMost_Suc)  lp15@57113  811 wenzelm@61799  812 lemma atLeastLessThan_nat_numeral: \\Evaluation for specific numerals\  hoelzl@62369  813  "atLeastLessThan m (numeral k :: nat) =  lp15@57113  814  (if m \ (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k))  lp15@57113  815  else {})"  lp15@57113  816  by (simp add: numeral_eq_Suc atLeastLessThanSuc)  lp15@57113  817 wenzelm@60758  818 subsubsection \Image\  nipkow@16733  819 lp15@60809  820 lemma image_add_atLeastAtMost [simp]:  lp15@60615  821  fixes k ::"'a::linordered_semidom"  lp15@60615  822  shows "(\n. n+k)  {i..j} = {i+k..j+k}" (is "?A = ?B")  nipkow@16733  823 proof  nipkow@16733  824  show "?A \ ?B" by auto  nipkow@16733  825 next  nipkow@16733  826  show "?B \ ?A"  nipkow@16733  827  proof  nipkow@16733  828  fix n assume a: "n : ?B"  lp15@60615  829  hence "n - k : {i..j}"  lp15@60615  830  by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le)  lp15@60615  831  moreover have "n = (n - k) + k" using a  lp15@60615  832  proof -  lp15@60615  833  have "k + i \ n"  lp15@60615  834  by (metis a add.commute atLeastAtMost_iff)  lp15@60615  835  hence "k + (n - k) = n"  lp15@60615  836  by (metis (no_types) ab_semigroup_add_class.add_ac(1) add_diff_cancel_left' le_add_diff_inverse)  lp15@60615  837  thus ?thesis  lp15@60615  838  by (simp add: add.commute)  lp15@60615  839  qed  nipkow@16733  840  ultimately show "n : ?A" by blast  nipkow@16733  841  qed  nipkow@16733  842 qed  nipkow@16733  843 lp15@60809  844 lemma image_diff_atLeastAtMost [simp]:  lp15@60809  845  fixes d::"'a::linordered_idom" shows "(op - d  {a..b}) = {d-b..d-a}"  lp15@60809  846  apply auto  lp15@60809  847  apply (rule_tac x="d-x" in rev_image_eqI, auto)  lp15@60809  848  done  lp15@60809  849 lp15@60809  850 lemma image_mult_atLeastAtMost [simp]:  lp15@60809  851  fixes d::"'a::linordered_field"  lp15@60809  852  assumes "d>0" shows "(op * d  {a..b}) = {d*a..d*b}"  lp15@60809  853  using assms  lp15@60809  854  by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])  lp15@60809  855 lp15@60809  856 lemma image_affinity_atLeastAtMost:  lp15@60809  857  fixes c :: "'a::linordered_field"  lp15@60809  858  shows "((\x. m*x + c)  {a..b}) = (if {a..b}={} then {}  lp15@60809  859  else if 0 \ m then {m*a + c .. m *b + c}  lp15@60809  860  else {m*b + c .. m*a + c})"  lp15@60809  861  apply (case_tac "m=0", auto simp: mult_le_cancel_left)  lp15@60809  862  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)  lp15@60809  863  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)  lp15@60809  864  done  lp15@60809  865 lp15@60809  866 lemma image_affinity_atLeastAtMost_diff:  lp15@60809  867  fixes c :: "'a::linordered_field"  lp15@60809  868  shows "((\x. m*x - c)  {a..b}) = (if {a..b}={} then {}  lp15@60809  869  else if 0 \ m then {m*a - c .. m*b - c}  lp15@60809  870  else {m*b - c .. m*a - c})"  lp15@60809  871  using image_affinity_atLeastAtMost [of m "-c" a b]  lp15@60809  872  by simp  lp15@60809  873 paulson@61204  874 lemma image_affinity_atLeastAtMost_div:  paulson@61204  875  fixes c :: "'a::linordered_field"  paulson@61204  876  shows "((\x. x/m + c)  {a..b}) = (if {a..b}={} then {}  paulson@61204  877  else if 0 \ m then {a/m + c .. b/m + c}  paulson@61204  878  else {b/m + c .. a/m + c})"  paulson@61204  879  using image_affinity_atLeastAtMost [of "inverse m" c a b]  paulson@61204  880  by (simp add: field_class.field_divide_inverse algebra_simps)  hoelzl@62369  881 lp15@60809  882 lemma image_affinity_atLeastAtMost_div_diff:  lp15@60809  883  fixes c :: "'a::linordered_field"  lp15@60809  884  shows "((\x. x/m - c)  {a..b}) = (if {a..b}={} then {}  lp15@60809  885  else if 0 \ m then {a/m - c .. b/m - c}  lp15@60809  886  else {b/m - c .. a/m - c})"  lp15@60809  887  using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]  lp15@60809  888  by (simp add: field_class.field_divide_inverse algebra_simps)  lp15@60809  889 nipkow@16733  890 lemma image_add_atLeastLessThan:  nipkow@16733  891  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  894 next  nipkow@16733  895  show "?B \ ?A"  nipkow@16733  896  proof  nipkow@16733  897  fix n assume a: "n : ?B"  webertj@20217  898  hence "n - k : {i..i. i - c)  {x ..< y} =  hoelzl@37664  922  (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"  hoelzl@37664  923  (is "_ = ?right")  hoelzl@37664  924 proof safe  hoelzl@37664  925  fix a assume a: "a \ ?right"  hoelzl@37664  926  show "a \ (\i. i - c)  {x ..< y}"  hoelzl@37664  927  proof cases  hoelzl@37664  928  assume "c < y" with a show ?thesis  hoelzl@37664  929  by (auto intro!: image_eqI[of _ _ "a + c"])  hoelzl@37664  930  next  hoelzl@37664  931  assume "\ c < y" with a show ?thesis  nipkow@62390  932  by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)  hoelzl@37664  933  qed  hoelzl@37664  934 qed auto  hoelzl@37664  935 Andreas@51152  936 lemma image_int_atLeastLessThan: "int  {a.. uminus  {x<..}"  hoelzl@35580  950  by (rule imageI) (simp add: *)  hoelzl@35580  951  thus "y \ uminus  {x<..}" by simp  hoelzl@35580  952 next  hoelzl@35580  953  fix y assume "y \ -x"  hoelzl@35580  954  have "- (-y) \ uminus  {x..}"  wenzelm@60758  955  by (rule imageI) (insert \y \ -x\[THEN le_imp_neg_le], simp)  hoelzl@35580  956  thus "y \ uminus  {x..}" by simp  hoelzl@35580  957 qed simp_all  hoelzl@35580  958 hoelzl@35580  959 lemma  hoelzl@35580  960  fixes x :: 'a  hoelzl@35580  961  shows image_uminus_lessThan[simp]: "uminus  {..Finiteness\  paulson@14485  982 nipkow@15045  983 lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..A bounded set of natural numbers is finite.\  paulson@14485  1006 lemma bounded_nat_set_is_finite:  nipkow@24853  1007  "(ALL i:N. i < (n::nat)) ==> finite N"  nipkow@28068  1008 apply (rule finite_subset)  nipkow@28068  1009  apply (rule_tac [2] finite_lessThan, auto)  nipkow@28068  1010 done  nipkow@28068  1011 wenzelm@60758  1012 text \A set of natural numbers is finite iff it is bounded.\  nipkow@31044  1013 lemma finite_nat_set_iff_bounded:  nipkow@31044  1014  "finite(N::nat set) = (EX m. ALL n:N. n?F\, simplified less_Suc_eq_le[symmetric]] by blast  nipkow@31044  1018 next  wenzelm@60758  1019  assume ?B show ?F using \?B\ by(blast intro:bounded_nat_set_is_finite)  nipkow@31044  1020 qed  nipkow@31044  1021 nipkow@31044  1022 lemma finite_nat_set_iff_bounded_le:  nipkow@31044  1023  "finite(N::nat set) = (EX m. ALL n:N. n<=m)"  nipkow@31044  1024 apply(simp add:finite_nat_set_iff_bounded)  nipkow@31044  1025 apply(blast dest:less_imp_le_nat le_imp_less_Suc)  nipkow@31044  1026 done  nipkow@31044  1027 nipkow@28068  1028 lemma finite_less_ub:  nipkow@28068  1029  "!!f::nat=>nat. (!!n. n \ f n) ==> finite {n. f n \ u}"  nipkow@28068  1030 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)  paulson@14485  1031 hoelzl@56328  1032 wenzelm@60758  1033 text\Any subset of an interval of natural numbers the size of the  wenzelm@60758  1034 subset is exactly that interval.\  nipkow@24853  1035 nipkow@24853  1036 lemma subset_card_intvl_is_intvl:  blanchet@55085  1037  assumes "A \ {k.. A" by auto  blanchet@55085  1047  with insert have "A <= {k..Proving Inclusions and Equalities between Unions\  paulson@32596  1058 nipkow@36755  1059 lemma UN_le_eq_Un0:  nipkow@36755  1060  "(\i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B")  nipkow@36755  1061 proof  nipkow@36755  1062  show "?A <= ?B"  nipkow@36755  1063  proof  nipkow@36755  1064  fix x assume "x : ?A"  nipkow@36755  1065  then obtain i where i: "i\n" "x : M i" by auto  nipkow@36755  1066  show "x : ?B"  nipkow@36755  1067  proof(cases i)  nipkow@36755  1068  case 0 with i show ?thesis by simp  nipkow@36755  1069  next  nipkow@36755  1070  case (Suc j) with i show ?thesis by auto  nipkow@36755  1071  qed  nipkow@36755  1072  qed  nipkow@36755  1073 next  nipkow@36755  1074  show "?B <= ?A" by auto  nipkow@36755  1075 qed  nipkow@36755  1076 nipkow@36755  1077 lemma UN_le_add_shift:  nipkow@36755  1078  "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B")  nipkow@36755  1079 proof  nipkow@44890  1080  show "?A <= ?B" by fastforce  nipkow@36755  1081 next  nipkow@36755  1082  show "?B <= ?A"  nipkow@36755  1083  proof  nipkow@36755  1084  fix x assume "x : ?B"  nipkow@36755  1085  then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto  nipkow@36755  1086  hence "i-k\n & x : M((i-k)+k)" by auto  nipkow@36755  1087  thus "x : ?A" by blast  nipkow@36755  1088  qed  nipkow@36755  1089 qed  nipkow@36755  1090 hoelzl@62369  1091 lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)"  hoelzl@62369  1092  by (auto simp add: atLeast0LessThan)  paulson@32596  1093 haftmann@62343  1094 lemma UN_finite_subset:  haftmann@62343  1095  "(\n::nat. (\i\{0.. C) \ (\n. A n) \ C"  paulson@32596  1096  by (subst UN_UN_finite_eq [symmetric]) blast  paulson@32596  1097 hoelzl@62369  1098 lemma UN_finite2_subset:  haftmann@62343  1099  assumes "\n::nat. (\i\{0.. (\i\{0..n. A n) \ (\n. B n)"  haftmann@62343  1101 proof (rule UN_finite_subset, rule)  haftmann@62343  1102  fix n and a  haftmann@62343  1103  from assms have "(\i\{0.. (\i\{0.. (\i\{0.. (\i\{0.. (\i. B i)" by (auto simp add: UN_UN_finite_eq)  haftmann@62343  1107 qed  paulson@32596  1108 paulson@32596  1109 lemma UN_finite2_eq:  haftmann@62343  1110  "(\n::nat. (\i\{0..i\{0..  haftmann@62343  1111  (\n. A n) = (\n. B n)"  paulson@33044  1112  apply (rule subset_antisym)  paulson@33044  1113  apply (rule UN_finite2_subset, blast)  haftmann@62343  1114  apply (rule UN_finite2_subset [where k=k])  haftmann@62343  1115  apply (force simp add: atLeastLessThan_add_Un [of 0])  haftmann@62343  1116  done  paulson@32596  1117 paulson@32596  1118 wenzelm@60758  1119 subsubsection \Cardinality\  paulson@14485  1120 nipkow@15045  1121 lemma card_lessThan [simp]: "card {.. \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  1161 apply(drule ex_bij_betw_finite_nat)  nipkow@31438  1162 apply(drule ex_bij_betw_nat_finite)  nipkow@31438  1163 apply(auto intro!:bij_betw_trans)  nipkow@31438  1164 done  nipkow@31438  1165 nipkow@31438  1166 lemma ex_bij_betw_nat_finite_1:  nipkow@31438  1167  "finite M \ \h. bij_betw h {1 .. card M} M"  nipkow@31438  1168 by (rule finite_same_card_bij) auto  nipkow@31438  1169 hoelzl@40703  1170 lemma bij_betw_iff_card:  lp15@63114  1171  assumes "finite A" "finite B"  lp15@63114  1172  shows "(\f. bij_betw f A B) \ (card A = card B)"  lp15@63114  1173 proof  lp15@63114  1174  assume "card A = card B"  lp15@63114  1175  moreover obtain f where "bij_betw f A {0 ..< card A}"  lp15@63114  1176  using assms ex_bij_betw_finite_nat by blast  hoelzl@40703  1177  moreover obtain g where "bij_betw g {0 ..< card B} B"  lp15@63114  1178  using assms ex_bij_betw_nat_finite by blast  hoelzl@40703  1179  ultimately have "bij_betw (g o f) A B"  lp15@63114  1180  by (auto simp: bij_betw_trans)  hoelzl@40703  1181  thus "(\f. bij_betw f A B)" by blast  lp15@63114  1182 qed (auto simp: bij_betw_same_card)  hoelzl@40703  1183 hoelzl@40703  1184 lemma inj_on_iff_card_le:  hoelzl@40703  1185  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  1186  shows "(\f. inj_on f A \ f  A \ B) = (card A \ card B)"  hoelzl@40703  1187 proof (safe intro!: card_inj_on_le)  hoelzl@40703  1188  assume *: "card A \ card B"  hoelzl@40703  1189  obtain f where 1: "inj_on f A" and 2: "f  A = {0 ..< card A}"  hoelzl@40703  1190  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force  hoelzl@40703  1191  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g  {0 ..< card B} = B"  hoelzl@40703  1192  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force  hoelzl@40703  1193  ultimately have "inj_on g (f  A)" using subset_inj_on[of g _ "f  A"] * by force  hoelzl@40703  1194  hence "inj_on (g o f) A" using 1 comp_inj_on by blast  hoelzl@40703  1195  moreover  hoelzl@40703  1196  {have "{0 ..< card A} \ {0 ..< card B}" using * by force  hoelzl@40703  1197  with 2 have "f  A \ {0 ..< card B}" by blast  hoelzl@40703  1198  hence "(g o f)  A \ B" unfolding comp_def using 3 by force  hoelzl@40703  1199  }  hoelzl@40703  1200  ultimately show "(\f. inj_on f A \ f  A \ B)" by blast  hoelzl@40703  1201 qed (insert assms, auto)  nipkow@26105  1202 wenzelm@60758  1203 subsection \Intervals of integers\  paulson@14485  1204 nipkow@15045  1205 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..Finiteness\  paulson@14485  1216 paulson@15418  1217 lemma image_atLeastZeroLessThan_int: "0 \ u ==>  nipkow@15045  1218  {(0::int).. u")  paulson@14485  1227  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1228  apply (rule finite_imageI)  paulson@14485  1229  apply auto  paulson@14485  1230  done  paulson@14485  1231 nipkow@15045  1232 lemma finite_atLeastLessThan_int [iff]: "finite {l..Cardinality\  paulson@14485  1251 nipkow@15045  1252 lemma card_atLeastZeroLessThan_int: "card {(0::int).. u")  paulson@14485  1254  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1255  apply (subst card_image)  paulson@14485  1256  apply (auto simp add: inj_on_def)  paulson@14485  1257  done  paulson@14485  1258 nipkow@15045  1259 lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}"  bulwahn@27656  1281 proof -  bulwahn@27656  1282  have "{k. P k \ k < i} \ {.. M"  bulwahn@27656  1288 shows "card {k \ M. k < Suc i} \ 0"  bulwahn@27656  1289 proof -  bulwahn@27656  1290  from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto  bulwahn@27656  1291  with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)  bulwahn@27656  1292 qed  bulwahn@27656  1293 bulwahn@27656  1294 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"  haftmann@37388  1295 apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"])  bulwahn@27656  1296 apply auto  bulwahn@27656  1297 apply (rule inj_on_diff_nat)  bulwahn@27656  1298 apply auto  bulwahn@27656  1299 apply (case_tac x)  bulwahn@27656  1300 apply auto  bulwahn@27656  1301 apply (case_tac xa)  bulwahn@27656  1302 apply auto  bulwahn@27656  1303 apply (case_tac xa)  bulwahn@27656  1304 apply auto  bulwahn@27656  1305 done  bulwahn@27656  1306 bulwahn@27656  1307 lemma card_less_Suc:  bulwahn@27656  1308  assumes zero_in_M: "0 \ M"  bulwahn@27656  1309  shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"  bulwahn@27656  1310 proof -  bulwahn@27656  1311  from assms have a: "0 \ {k \ M. k < Suc i}" by simp  bulwahn@27656  1312  hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})"  bulwahn@27656  1313  by (auto simp only: insert_Diff)  bulwahn@27656  1314  have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto  hoelzl@62369  1315  from finite_M_bounded_by_nat[of "\x. x \ M" "Suc i"]  lp15@57113  1316  have "Suc (card {k. Suc k \ M \ k < i}) = card (insert 0 ({k \ M. k < Suc i} - {0}))"  bulwahn@27656  1317  apply (subst card_insert)  bulwahn@27656  1318  apply simp_all  bulwahn@27656  1319  apply (subst b)  bulwahn@27656  1320  apply (subst card_less_Suc2[symmetric])  bulwahn@27656  1321  apply simp_all  bulwahn@27656  1322  done  bulwahn@27656  1323  with c show ?thesis by simp  bulwahn@27656  1324 qed  bulwahn@27656  1325 paulson@14485  1326 wenzelm@60758  1327 subsection \Lemmas useful with the summation operator setsum\  paulson@13850  1328 wenzelm@60758  1329 text \For examples, see Algebra/poly/UnivPoly2.thy\  ballarin@13735  1330 wenzelm@60758  1331 subsubsection \Disjoint Unions\  ballarin@13735  1332 wenzelm@60758  1333 text \Singletons and open intervals\  ballarin@13735  1334 ballarin@13735  1335 lemma ivl_disj_un_singleton:  nipkow@15045  1336  "{l::'a::linorder} Un {l<..} = {l..}"  nipkow@15045  1337  "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  1341  "(l::'a::linorder) <= u ==> {l..One- and two-sided intervals\  ballarin@13735  1345 ballarin@13735  1346 lemma ivl_disj_un_one:  nipkow@15045  1347  "(l::'a::linorder) < u ==> {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  1350  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  1352  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  1354  "(l::'a::linorder) <= u ==> {l..Two- and two-sided intervals\  ballarin@13735  1358 ballarin@13735  1359 lemma ivl_disj_un_two:  nipkow@15045  1360  "[| (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  1366  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  1368 by auto  ballarin@13735  1369 lp15@60150  1370 lemma ivl_disj_un_two_touch:  lp15@60150  1371  "[| (l::'a::linorder) < m; m < u |] ==> {l<..m} Un {m.. {l..m} Un {m.. {l<..m} Un {m..u} = {l<..u}"  lp15@60150  1374  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m..u} = {l..u}"  lp15@60150  1375 by auto  lp15@60150  1376 lp15@60150  1377 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ivl_disj_un_two_touch  ballarin@13735  1378 wenzelm@60758  1379 subsubsection \Disjoint Intersections\  ballarin@13735  1380 wenzelm@60758  1381 text \One- and two-sided intervals\  ballarin@13735  1382 ballarin@13735  1383 lemma ivl_disj_int_one:  nipkow@15045  1384  "{..l::'a::order} Int {l<..Two- and two-sided intervals\  ballarin@13735  1395 ballarin@13735  1396 lemma ivl_disj_int_two:  nipkow@15045  1397  "{l::'a::order<..Some Differences\  nipkow@15542  1410 nipkow@15542  1411 lemma ivl_diff[simp]:  nipkow@15542  1412  "i \ n \ {i..Some Subset Conditions\  nipkow@15542  1425 blanchet@54147  1426 lemma ivl_subset [simp]:  nipkow@15542  1427  "({i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  1428 apply(auto simp:linorder_not_le)  nipkow@15542  1429 apply(rule ccontr)  nipkow@15542  1430 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  1431 apply(clarsimp simp:linorder_not_le)  nipkow@44890  1432 apply(fastforce)  nipkow@15542  1433 done  nipkow@15542  1434 nipkow@15041  1435 wenzelm@60758  1436 subsection \Summation indexed over intervals\  nipkow@15042  1437 wenzelm@61955  1438 syntax (ASCII)  wenzelm@61955  1439  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  wenzelm@61955  1440  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  wenzelm@61955  1441  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  wenzelm@61955  1442  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  wenzelm@61955  1443 nipkow@15056  1444 syntax (latex_sum output)  nipkow@15052  1445  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  1446  ("(3\<^raw:\sum_{>_ = _\<^raw:}^{>_\<^raw:}> _)" [0,0,0,10] 10)  nipkow@15052  1447  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  1448  ("(3\<^raw:\sum_{>_ = _\<^raw:}^{<>_\<^raw:}> _)" [0,0,0,10] 10)  nipkow@16052  1449  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1450  ("(3\<^raw:\sum_{>_ < _\<^raw:}> _)" [0,0,10] 10)  nipkow@15052  1451  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1452  ("(3\<^raw:\sum_{>_ \ _\<^raw:}> _)" [0,0,10] 10)  nipkow@15041  1453 wenzelm@61955  1454 syntax  wenzelm@61955  1455  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  wenzelm@61955  1456  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  wenzelm@61955  1457  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  wenzelm@61955  1458  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  wenzelm@61955  1459 nipkow@15048  1460 translations  wenzelm@61955  1461  "\x=a..b. t" == "CONST setsum (\x. t) {a..b}"  wenzelm@61955  1462  "\x=a..x. t) {a..i\n. t" == "CONST setsum (\i. t) {..n}"  nipkow@28853  1464  "\ii. t) {..The above introduces some pretty alternative syntaxes for  nipkow@15056  1467 summation over intervals:  nipkow@15052  1468 \begin{center}  nipkow@15052  1469 \begin{tabular}{lll}  nipkow@15056  1470 Old & New & \LaTeX\\  nipkow@15056  1471 @{term[source]"\x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  1472 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  1474 @{term[source]"\x\{..xxlatex_sum\ (e.g.\ via \mode = latex_sum\ in  nipkow@15056  1482 antiquotations). It is not the default \LaTeX\ output because it only  nipkow@15056  1483 works well with italic-style formulae, not tt-style.  nipkow@15052  1484 nipkow@15052  1485 Note that for uniformity on @{typ nat} it is better to use  wenzelm@61799  1486 @{term"\x::nat=0..\x: \setsum\ may  nipkow@15052  1487 not provide all lemmas available for @{term"{m..  nipkow@15052  1489 wenzelm@60758  1490 text\This congruence rule should be used for sums over intervals as  haftmann@57418  1491 the standard theorem @{text[source]setsum.cong} does not work well  nipkow@15542  1492 with the simplifier who adds the unsimplified premise @{term"x:B"} to  wenzelm@60758  1493 the context.\  nipkow@15542  1494 nipkow@15542  1495 lemma setsum_ivl_cong:  nipkow@15542  1496  "\a = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \  nipkow@15542  1497  setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)"  haftmann@57514  1504 by (simp add:atMost_Suc ac_simps)  nipkow@16052  1505 nipkow@16041  1506 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n"  haftmann@57514  1507 by (simp add:lessThan_Suc ac_simps)  nipkow@15041  1508 nipkow@15911  1509 lemma setsum_cl_ivl_Suc[simp]:  nipkow@15561  1510  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  haftmann@57514  1511 by (auto simp:ac_simps atLeastAtMostSuc_conv)  nipkow@15561  1512 nipkow@15911  1513 lemma setsum_op_ivl_Suc[simp]:  nipkow@15561  1514  "setsum f {m..  nipkow@15561  1518  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  haftmann@57514  1519 by (auto simp:ac_simps atLeastAtMostSuc_conv)  nipkow@16041  1520 *)  nipkow@28068  1521 nipkow@28068  1522 lemma setsum_head:  nipkow@28068  1523  fixes n :: nat  hoelzl@62369  1524  assumes mn: "m <= n"  nipkow@28068  1525  shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  nipkow@28068  1526 proof -  nipkow@28068  1527  from mn  nipkow@28068  1528  have "{m..n} = {m} \ {m<..n}"  nipkow@28068  1529  by (auto intro: ivl_disj_un_singleton)  nipkow@28068  1530  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  nipkow@28068  1531  by (simp add: atLeast0LessThan)  nipkow@28068  1532  also have "\ = ?rhs" by simp  nipkow@28068  1533  finally show ?thesis .  nipkow@28068  1534 qed  nipkow@28068  1535 nipkow@28068  1536 lemma setsum_head_Suc:  nipkow@28068  1537  "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}"  nipkow@28068  1538 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)  nipkow@28068  1539 nipkow@28068  1540 lemma setsum_head_upt_Suc:  nipkow@28068  1541  "m < n \ setsum f {m.. n + 1"  nipkow@31501  1547  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"  nipkow@31501  1548 proof-  wenzelm@60758  1549  have "{m .. n+p} = {m..n} \ {n+1..n+p}" using \m \ n+1\ by auto  haftmann@57418  1550  thus ?thesis by (auto simp: ivl_disj_int setsum.union_disjoint  nipkow@31501  1551  atLeastSucAtMost_greaterThanAtMost)  nipkow@31501  1552 qed  nipkow@28068  1553 nipkow@15539  1554 lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \  nipkow@15539  1555  setsum f {m.. 'a::ab_group_add"  nipkow@15539  1560 shows "\ m \ n; n \ p \ \  nipkow@15539  1561  setsum f {m.. ('a::ab_group_add)"  nipkow@31505  1568  shows "setsum (\k. f k - f(k + 1)) {(m::nat) .. n} =  nipkow@31505  1569  (if m <= n then f m - f(n + 1) else 0)"  nipkow@31505  1570 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)  nipkow@31505  1571 hoelzl@56194  1572 lemma setsum_nat_group: "(\m(i,j)\{(i,j). i+j < n}. f i j) = (\ki\k. f i (k - i))"  lp15@60150  1581  apply (simp add: setsum.Sigma)  lp15@60150  1582  apply (rule setsum.reindex_bij_witness[where j="\(i, j). (i+j, i)" and i="\(k, i). (i, k - i)"])  lp15@60150  1583  apply auto  lp15@60150  1584  done  lp15@60150  1585 lp15@60150  1586 lemma setsum_triangle_reindex_eq:  lp15@60150  1587  fixes n :: nat  lp15@60150  1588  shows "(\(i,j)\{(i,j). i+j \ n}. f i j) = (\k\n. \i\k. f i (k - i))"  lp15@60150  1589 using setsum_triangle_reindex [of f "Suc n"]  lp15@60150  1590 by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost)  lp15@60150  1591 lp15@60162  1592 lemma nat_diff_setsum_reindex: "(\iiShifting bounds\  nipkow@16733  1596 nipkow@15539  1597 lemma setsum_shift_bounds_nat_ivl:  nipkow@15539  1598  "setsum f {m+k.. setsum f {Suc 0..k} = setsum f {0..k}"  nipkow@28068  1615 by(simp add:setsum_head_Suc)  kleing@19106  1616 nipkow@28068  1617 lemma setsum_shift_lb_Suc0_0_upt:  nipkow@28068  1618  "f(0::nat) = 0 \ setsum f {Suc 0.. 'a::comm_monoid_add"  haftmann@52380  1625  shows "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))"  haftmann@52380  1626 proof (induct n)  haftmann@52380  1627  case 0 show ?case by simp  haftmann@52380  1628 next  haftmann@52380  1629  case (Suc n) note IH = this  haftmann@52380  1630  have "(\i\Suc (Suc n). f i) = (\i\Suc n. f i) + f (Suc (Suc n))"  haftmann@52380  1631  by (rule setsum_atMost_Suc)  haftmann@52380  1632  also have "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))"  haftmann@52380  1633  by (rule IH)  haftmann@52380  1634  also have "f 0 + (\i\n. f (Suc i)) + f (Suc (Suc n)) =  haftmann@52380  1635  f 0 + ((\i\n. f (Suc i)) + f (Suc (Suc n)))"  haftmann@57512  1636  by (rule add.assoc)  haftmann@52380  1637  also have "(\i\n. f (Suc i)) + f (Suc (Suc n)) = (\i\Suc n. f (Suc i))"  haftmann@52380  1638  by (rule setsum_atMost_Suc [symmetric])  haftmann@52380  1639  finally show ?case .  haftmann@52380  1640 qed  haftmann@52380  1641 eberlm@63099  1642 lemma setsum_lessThan_Suc_shift:  eberlm@63099  1643  "(\ii 'a::comm_monoid_add"  lp15@62379  1648  shows "(\i\n. f i) = f 0 + (\i (\i = m..n. f i) = f n + (\i = m.. 'a::ab_group_add"  lp15@56238  1656  assumes "m \ Suc n"  lp15@56238  1657  shows "(\i = m..n. f(Suc i) - f i) = f (Suc n) - f m"  lp15@56238  1658 using assms by (induct n) (auto simp: le_Suc_eq)  lp15@55718  1659 lp15@55718  1660 lemma nested_setsum_swap:  lp15@55718  1661  "(\i = 0..n. (\j = 0..j = 0..i = Suc j..n. a i j)"  haftmann@57418  1662  by (induction n) (auto simp: setsum.distrib)  lp15@55718  1663 lp15@56215  1664 lemma nested_setsum_swap':  lp15@56215  1665  "(\i\n. (\jji = Suc j..n. a i j)"  haftmann@57418  1666  by (induction n) (auto simp: setsum.distrib)  lp15@56215  1667 lp15@56238  1668 lemma setsum_zero_power' [simp]:  lp15@56238  1669  fixes c :: "nat \ 'a::field"  lp15@56238  1670  shows "(\i\A. c i * 0^i / d i) = (if finite A \ 0 \ A then c 0 / d 0 else 0)"  lp15@56238  1671  using setsum_zero_power [of "\i. c i / d i" A]  lp15@56238  1672  by auto  lp15@56238  1673 haftmann@52380  1674 eberlm@61524  1675 subsection \Telescoping\  eberlm@61524  1676 eberlm@61524  1677 lemma setsum_telescope:  eberlm@61524  1678  fixes f::"nat \ 'a::ab_group_add"  eberlm@61524  1679  shows "setsum (\i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)"  eberlm@61524  1680  by (induct i) simp_all  eberlm@61524  1681 eberlm@61524  1682 lemma setsum_telescope'':  eberlm@61524  1683  assumes "m \ n"  eberlm@61524  1684  shows "(\k\{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)"  eberlm@61524  1685  by (rule dec_induct[OF assms]) (simp_all add: algebra_simps)  eberlm@61524  1686 wenzelm@60758  1687 subsection \The formula for geometric sums\  ballarin@17149  1688 ballarin@17149  1689 lemma geometric_sum:  haftmann@36307  1690  assumes "x \ 1"  hoelzl@56193  1691  shows "(\i 0" by simp_all  hoelzl@56193  1694  moreover have "(\iy \ 0$$  haftmann@36307  1696  ultimately show ?thesis by simp  haftmann@36307  1697 qed  haftmann@36307  1698 lp15@60162  1699 lemma diff_power_eq_setsum:  lp15@60162  1700  fixes y :: "'a::{comm_ring,monoid_mult}"  lp15@60162  1701  shows  lp15@60162  1702  "x ^ (Suc n) - y ^ (Suc n) =  lp15@60162  1703  (x - y) * (\pppp\\COMPLEX_POLYFUN\ in HOL Light\  lp15@60162  1720  fixes x :: "'a::{comm_ring,monoid_mult}"  lp15@60162  1721  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) * (\iThe formula for arithmetic sums\  kleing@19469  1744 huffman@47222  1745 lemma gauss_sum:  hoelzl@56193  1746  "(2::'a::comm_semiring_1)*(\i\{1..n}. of_nat i) = of_nat n*((of_nat n)+1)"  kleing@19469  1747 proof (induct n)  kleing@19469  1748  case 0  kleing@19469  1749  show ?case by simp  kleing@19469  1750 next  kleing@19469  1751  case (Suc n)  huffman@47222  1752  then show ?case  huffman@47222  1753  by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one)  huffman@47222  1754  (* FIXME: make numeral cancellation simprocs work for semirings *)  kleing@19469  1755 qed  kleing@19469  1756 kleing@19469  1757 theorem arith_series_general:  huffman@47222  1758  "(2::'a::comm_semiring_1) * (\i\{.. 1"  kleing@19469  1762  let ?I = "\i. of_nat i" and ?n = "of_nat n"  kleing@19469  1763  have  kleing@19469  1764  "(\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  1777  by (simp only: mult.assoc gauss_sum [of "n - 1"], unfold One_nat_def)  haftmann@57514  1778  (simp add: mult.commute trans [OF add.commute of_nat_Suc [symmetric]])  huffman@47222  1779  finally show ?thesis  huffman@47222  1780  unfolding mult_2 by (simp add: algebra_simps)  kleing@19469  1781 next  kleing@19469  1782  assume "\(n > 1)"  kleing@19469  1783  hence "n = 1 \ n = 0" by auto  huffman@47222  1784  thus ?thesis by (auto simp: mult_2)  kleing@19469  1785 qed  kleing@19469  1786 kleing@19469  1787 lemma arith_series_nat:  huffman@47222  1788  "(2::nat) * (\i\{..i\{..i\{..x. Q x \ P x \ (\xxxProducts indexed over intervals\  paulson@29960  1807 wenzelm@61955  1808 syntax (ASCII)  wenzelm@61955  1809  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)  wenzelm@61955  1810  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)  wenzelm@61955  1811  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10)  wenzelm@61955  1812  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10)  wenzelm@61955  1813 paulson@29960  1814 syntax (latex_prod output)  paulson@29960  1815  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1816  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1817  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1818  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1819  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1820  ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1821  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1822  ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1823 wenzelm@61955  1824 syntax  wenzelm@61955  1825  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  wenzelm@61955  1826  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  wenzelm@61955  1827  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  wenzelm@61955  1828  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  wenzelm@61955  1829 paulson@29960  1830 translations  wenzelm@61955  1831  "\x=a..b. t" \ "CONST setprod (\x. t) {a..b}"  wenzelm@61955  1832  "\x=a.. "CONST setprod (\x. t) {a..i\n. t" \ "CONST setprod (\i. t) {..n}"  wenzelm@61955  1834  "\i "CONST setprod (\i. t) {..Transfer setup\  haftmann@33318  1838 haftmann@33318  1839 lemma transfer_nat_int_set_functions:  haftmann@33318  1840  "{..n} = nat  {0..int n}"  haftmann@33318  1841  "{m..n} = nat  {int m..int n}" (* need all variants of these! *)  haftmann@33318  1842  apply (auto simp add: image_def)  haftmann@33318  1843  apply (rule_tac x = "int x" in bexI)  haftmann@33318  1844  apply auto  haftmann@33318  1845  apply (rule_tac x = "int x" in bexI)  haftmann@33318  1846  apply auto  haftmann@33318  1847  done  haftmann@33318  1848 haftmann@33318  1849 lemma transfer_nat_int_set_function_closures:  haftmann@33318  1850  "x >= 0 \ nat_set {x..y}"  haftmann@33318  1851  by (simp add: nat_set_def)  haftmann@33318  1852 haftmann@35644  1853 declare transfer_morphism_nat_int[transfer add  haftmann@33318  1854  return: transfer_nat_int_set_functions  haftmann@33318  1855  transfer_nat_int_set_function_closures  haftmann@33318  1856 ]  haftmann@33318  1857 haftmann@33318  1858 lemma transfer_int_nat_set_functions:  haftmann@33318  1859  "is_nat m \ is_nat n \ {m..n} = int  {nat m..nat n}"  haftmann@33318  1860  by (simp only: is_nat_def transfer_nat_int_set_functions  haftmann@33318  1861  transfer_nat_int_set_function_closures  haftmann@33318  1862  transfer_nat_int_set_return_embed nat_0_le  haftmann@33318  1863  cong: transfer_nat_int_set_cong)  haftmann@33318  1864 haftmann@33318  1865 lemma transfer_int_nat_set_function_closures:  haftmann@33318  1866  "is_nat x \ nat_set {x..y}"  haftmann@33318  1867  by (simp only: transfer_nat_int_set_function_closures is_nat_def)  haftmann@33318  1868 haftmann@35644  1869 declare transfer_morphism_int_nat[transfer add  haftmann@33318  1870  return: transfer_int_nat_set_functions  haftmann@33318  1871  transfer_int_nat_set_function_closures  haftmann@33318  1872 ]  haftmann@33318  1873 lp15@55242  1874 lemma setprod_int_plus_eq: "setprod int {i..i+j} = \{int i..int (i+j)}"  lp15@55242  1875  by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)  lp15@55242  1876 lp15@55242  1877 lemma setprod_int_eq: "setprod int {i..j} = \{int i..int j}"  lp15@55242  1878 proof (cases "i \ j")  lp15@55242  1879  case True  lp15@55242  1880  then show ?thesis  hoelzl@62376  1881  by (metis le_iff_add setprod_int_plus_eq)  lp15@55242  1882 next  lp15@55242  1883  case False  lp15@55242  1884  then show ?thesis  lp15@55242  1885  by auto  lp15@55242  1886 qed  lp15@55242  1887 eberlm@61524  1888 eberlm@61524  1889 subsection \Shifting bounds\  eberlm@61524  1890 eberlm@61524  1891 lemma setprod_shift_bounds_nat_ivl:  eberlm@61524  1892  "setprod f {m+k.. b \ setprod f {a.. Suc n"  eberlm@61524  1915  shows "setprod f {m..Suc n} = f (Suc n) * setprod f {m..n}"  eberlm@61524  1916 proof -  eberlm@61524  1917  from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto  eberlm@61524  1918  also have "setprod f \ = f (Suc n) * setprod f {m..n}" by simp  eberlm@61524  1919  finally show ?thesis .  eberlm@61524  1920 qed  eberlm@61524  1921 eberlm@62128  1922 eberlm@62128  1923 subsection \Efficient folding over intervals\  eberlm@62128  1924 eberlm@62128  1925 function fold_atLeastAtMost_nat where  eberlm@62128  1926  [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc =  eberlm@62128  1927  (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a acc))"  eberlm@62128  1928 by pat_completeness auto  eberlm@62128  1929 termination by (relation "measure (\(_,a,b,_). Suc b - a)") auto  eberlm@62128  1930 eberlm@62128  1931 lemma fold_atLeastAtMost_nat:  eberlm@62128  1932  assumes "comp_fun_commute f"  eberlm@62128  1933  shows "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}"  eberlm@62128  1934 using assms  eberlm@62128  1935 proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases)  eberlm@62128  1936  case (1 f a b acc)  eberlm@62128  1937  interpret comp_fun_commute f by fact  eberlm@62128  1938  show ?case  eberlm@62128  1939  proof (cases "a > b")  eberlm@62128  1940  case True  eberlm@62128  1941  thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto  eberlm@62128  1942  next  eberlm@62128  1943  case False  eberlm@62128  1944  with 1 show ?thesis  eberlm@62128  1945  by (subst fold_atLeastAtMost_nat.simps)  eberlm@62128  1946  (auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm)  eberlm@62128  1947  qed  eberlm@62128  1948 qed  eberlm@62128  1949 eberlm@62128  1950 lemma setsum_atLeastAtMost_code:  eberlm@62128  1951  "setsum f {a..b} = fold_atLeastAtMost_nat (\a acc. f a + acc) a b 0"  eberlm@62128  1952 proof -  eberlm@62128  1953  have "comp_fun_commute (\a. op + (f a))"  eberlm@62128  1954  by unfold_locales (auto simp: o_def add_ac)  eberlm@62128  1955  thus ?thesis  eberlm@62128  1956  by (simp add: setsum.eq_fold fold_atLeastAtMost_nat o_def)  eberlm@62128  1957 qed  eberlm@62128  1958 eberlm@62128  1959 lemma setprod_atLeastAtMost_code:  eberlm@62128  1960  "setprod f {a..b} = fold_atLeastAtMost_nat (\a acc. f a * acc) a b 1"  eberlm@62128  1961 proof -  eberlm@62128  1962  have "comp_fun_commute (\a. op * (f a))"  eberlm@62128  1963  by unfold_locales (auto simp: o_def mult_ac)  eberlm@62128  1964  thus ?thesis  eberlm@62128  1965  by (simp add: setprod.eq_fold fold_atLeastAtMost_nat o_def)  eberlm@62128  1966 qed  eberlm@62128  1967 eberlm@62128  1968 (* TODO: Add support for more kinds of intervals here *)  eberlm@62128  1969 nipkow@8924  1970 end