src/HOL/Set_Interval.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 63879 15bbf6360339 child 63918 6bf55e6e0b75 permissions -rw-r--r--
tuned proofs;
 huffman@47317  1 (* Title: HOL/Set_Interval.thy  wenzelm@32960  2  Author: Tobias Nipkow  wenzelm@32960  3  Author: Clemens Ballarin  wenzelm@32960  4  Author: Jeremy Avigad  nipkow@8924  5 ballarin@13735  6 lessThan, greaterThan, atLeast, atMost and two-sided intervals  nipkow@51334  7 nipkow@51334  8 Modern convention: Ixy stands for an interval where x and y  nipkow@51334  9 describe the lower and upper bound and x,y : {c,o,i}  nipkow@51334  10 where c = closed, o = open, i = infinite.  nipkow@51334  11 Examples: Ico = {_ ..< _} and Ici = {_ ..}  nipkow@8924  12 *)  nipkow@8924  13 wenzelm@60758  14 section \Set intervals\  wenzelm@14577  15 huffman@47317  16 theory Set_Interval  haftmann@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 hoelzl@56328  554 end  hoelzl@56328  555 hoelzl@56328  556 lemma infinite_Iio: "\ finite {..< a :: 'a :: {no_bot, linorder}}"  hoelzl@56328  557 proof  hoelzl@56328  558  assume "finite {..< a}"  hoelzl@56328  559  then have *: "\x. x < a \ Min {..< a} \ x"  hoelzl@56328  560  by auto  hoelzl@56328  561  obtain x where "x < a"  hoelzl@56328  562  using lt_ex by auto  hoelzl@56328  563 hoelzl@56328  564  obtain y where "y < Min {..< a}"  hoelzl@56328  565  using lt_ex by auto  hoelzl@56328  566  also have "Min {..< a} \ x"  wenzelm@60758  567  using \x < a\ by fact  wenzelm@60758  568  also note \x < a\  hoelzl@56328  569  finally have "Min {..< a} \ y"  hoelzl@56328  570  by fact  wenzelm@60758  571  with \y < Min {..< a}\ show False by auto  hoelzl@56328  572 qed  hoelzl@56328  573 hoelzl@56328  574 lemma infinite_Iic: "\ finite {.. a :: 'a :: {no_bot, linorder}}"  hoelzl@56328  575  using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"]  hoelzl@56328  576  by (auto simp: subset_eq less_imp_le)  hoelzl@56328  577 hoelzl@56328  578 lemma infinite_Ioi: "\ finite {a :: 'a :: {no_top, linorder} <..}"  hoelzl@56328  579 proof  hoelzl@56328  580  assume "finite {a <..}"  hoelzl@56328  581  then have *: "\x. a < x \ x \ Max {a <..}"  hoelzl@56328  582  by auto  hoelzl@56328  583 hoelzl@56328  584  obtain y where "Max {a <..} < y"  hoelzl@56328  585  using gt_ex by auto  hoelzl@56328  586 wenzelm@63540  587  obtain x where x: "a < x"  hoelzl@56328  588  using gt_ex by auto  wenzelm@63540  589  also from x have "x \ Max {a <..}"  hoelzl@56328  590  by fact  wenzelm@60758  591  also note \Max {a <..} < y\  hoelzl@56328  592  finally have "y \ Max { a <..}"  hoelzl@56328  593  by fact  wenzelm@60758  594  with \Max {a <..} < y\ show False by auto  hoelzl@56328  595 qed  hoelzl@56328  596 hoelzl@56328  597 lemma infinite_Ici: "\ finite {a :: 'a :: {no_top, linorder} ..}"  hoelzl@56328  598  using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"]  hoelzl@56328  599  by (auto simp: subset_eq less_imp_le)  hoelzl@56328  600 wenzelm@60758  601 subsubsection \Intersection\  nipkow@32456  602 nipkow@32456  603 context linorder  nipkow@32456  604 begin  nipkow@32456  605 nipkow@32456  606 lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"  nipkow@32456  607 by auto  nipkow@32456  608 nipkow@32456  609 lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"  nipkow@32456  610 by auto  nipkow@32456  611 nipkow@32456  612 lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"  nipkow@32456  613 by auto  nipkow@32456  614 nipkow@32456  615 lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"  nipkow@32456  616 by auto  nipkow@32456  617 nipkow@32456  618 lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"  nipkow@32456  619 by auto  nipkow@32456  620 nipkow@32456  621 lemma Int_atLeastLessThan[simp]: "{a.. {..b} = {.. min a b}"  hoelzl@50417  631  by (auto simp: min_def)  hoelzl@50417  632 hoelzl@57447  633 lemma Ioc_disjoint: "{a<..b} \ {c<..d} = {} \ b \ a \ d \ c \ b \ c \ d \ a"  wenzelm@63092  634  by auto  hoelzl@57447  635 nipkow@32456  636 end  nipkow@32456  637 hoelzl@51329  638 context complete_lattice  hoelzl@51329  639 begin  hoelzl@51329  640 hoelzl@51329  641 lemma  hoelzl@51329  642  shows Sup_atLeast[simp]: "Sup {x ..} = top"  hoelzl@51329  643  and Sup_greaterThanAtLeast[simp]: "x < top \ Sup {x <..} = top"  hoelzl@51329  644  and Sup_atMost[simp]: "Sup {.. y} = y"  hoelzl@51329  645  and Sup_atLeastAtMost[simp]: "x \ y \ Sup { x .. y} = y"  hoelzl@51329  646  and Sup_greaterThanAtMost[simp]: "x < y \ Sup { x <.. y} = y"  hoelzl@51329  647  by (auto intro!: Sup_eqI)  hoelzl@51329  648 hoelzl@51329  649 lemma  hoelzl@51329  650  shows Inf_atMost[simp]: "Inf {.. x} = bot"  hoelzl@51329  651  and Inf_atMostLessThan[simp]: "top < x \ Inf {..< x} = bot"  hoelzl@51329  652  and Inf_atLeast[simp]: "Inf {x ..} = x"  hoelzl@51329  653  and Inf_atLeastAtMost[simp]: "x \ y \ Inf { x .. y} = x"  hoelzl@51329  654  and Inf_atLeastLessThan[simp]: "x < y \ Inf { x ..< y} = x"  hoelzl@51329  655  by (auto intro!: Inf_eqI)  hoelzl@51329  656 hoelzl@51329  657 end  hoelzl@51329  658 hoelzl@51329  659 lemma  hoelzl@53216  660  fixes x y :: "'a :: {complete_lattice, dense_linorder}"  hoelzl@51329  661  shows Sup_lessThan[simp]: "Sup {..< y} = y"  hoelzl@51329  662  and Sup_atLeastLessThan[simp]: "x < y \ Sup { x ..< y} = y"  hoelzl@51329  663  and Sup_greaterThanLessThan[simp]: "x < y \ Sup { x <..< y} = y"  hoelzl@51329  664  and Inf_greaterThan[simp]: "Inf {x <..} = x"  hoelzl@51329  665  and Inf_greaterThanAtMost[simp]: "x < y \ Inf { x <.. y} = x"  hoelzl@51329  666  and Inf_greaterThanLessThan[simp]: "x < y \ Inf { x <..< y} = x"  hoelzl@51329  667  by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded)  nipkow@32456  668 wenzelm@60758  669 subsection \Intervals of natural numbers\  paulson@14485  670 wenzelm@60758  671 subsubsection \The Constant @{term lessThan}\  paulson@15047  672 paulson@14485  673 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"  paulson@14485  674 by (simp add: lessThan_def)  paulson@14485  675 paulson@14485  676 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"  paulson@14485  677 by (simp add: lessThan_def less_Suc_eq, blast)  paulson@14485  678 wenzelm@60758  679 text \The following proof is convenient in induction proofs where  hoelzl@39072  680 new elements get indices at the beginning. So it is used to transform  wenzelm@60758  681 @{term "{..  hoelzl@39072  682 hoelzl@59000  683 lemma zero_notin_Suc_image: "0 \ Suc  A"  hoelzl@59000  684  by auto  hoelzl@59000  685 hoelzl@39072  686 lemma lessThan_Suc_eq_insert_0: "{..The Constant @{term greaterThan}\  paulson@15047  699 paulson@14485  700 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"  paulson@14485  701 apply (simp add: greaterThan_def)  paulson@14485  702 apply (blast dest: gr0_conv_Suc [THEN iffD1])  paulson@14485  703 done  paulson@14485  704 paulson@14485  705 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"  paulson@14485  706 apply (simp add: greaterThan_def)  paulson@14485  707 apply (auto elim: linorder_neqE)  paulson@14485  708 done  paulson@14485  709 paulson@14485  710 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"  paulson@14485  711 by blast  paulson@14485  712 wenzelm@60758  713 subsubsection \The Constant @{term atLeast}\  paulson@15047  714 paulson@14485  715 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"  paulson@14485  716 by (unfold atLeast_def UNIV_def, simp)  paulson@14485  717 paulson@14485  718 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"  paulson@14485  719 apply (simp add: atLeast_def)  paulson@14485  720 apply (simp add: Suc_le_eq)  paulson@14485  721 apply (simp add: order_le_less, blast)  paulson@14485  722 done  paulson@14485  723 paulson@14485  724 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"  paulson@14485  725  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)  paulson@14485  726 paulson@14485  727 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"  paulson@14485  728 by blast  paulson@14485  729 wenzelm@60758  730 subsubsection \The Constant @{term atMost}\  paulson@15047  731 paulson@14485  732 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"  paulson@14485  733 by (simp add: atMost_def)  paulson@14485  734 paulson@14485  735 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"  paulson@14485  736 apply (simp add: atMost_def)  paulson@14485  737 apply (simp add: less_Suc_eq order_le_less, blast)  paulson@14485  738 done  paulson@14485  739 paulson@14485  740 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"  paulson@14485  741 by blast  paulson@14485  742 wenzelm@60758  743 subsubsection \The Constant @{term atLeastLessThan}\  paulson@15047  744 wenzelm@60758  745 text\The orientation of the following 2 rules is tricky. The lhs is  nipkow@24449  746 defined in terms of the rhs. Hence the chosen orientation makes sense  nipkow@24449  747 in this theory --- the reverse orientation complicates proofs (eg  nipkow@24449  748 nontermination). But outside, when the definition of the lhs is rarely  nipkow@24449  749 used, the opposite orientation seems preferable because it reduces a  wenzelm@60758  750 specific concept to a more general one.\  nipkow@28068  751 haftmann@63417  752 lemma atLeast0LessThan [code_abbrev]: "{0::nat..The Constant @{term atLeastAtMost}\  haftmann@63417  779 haftmann@63417  780 lemma atLeast0_atMost_Suc:  haftmann@63417  781  "{0..Suc n} = insert (Suc n) {0..n}"  haftmann@63417  782  by (simp add: atLeast0AtMost atMost_Suc)  haftmann@63417  783 haftmann@63417  784 lemma atLeast0_atMost_Suc_eq_insert_0:  haftmann@63417  785  "{0..Suc n} = insert 0 (Suc  {0..n})"  haftmann@63417  786  by (simp add: atLeast0AtMost Iic_Suc_eq_insert_0)  haftmann@63417  787 haftmann@63417  788 wenzelm@60758  789 subsubsection \Intervals of nats with @{term Suc}\  paulson@15047  790 wenzelm@60758  791 text\Not a simprule because the RHS is too messy.\  paulson@15047  792 lemma atLeastLessThanSuc:  paulson@15047  793  "{m.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  817 by (auto simp add: atLeastAtMost_def)  nipkow@15554  818 noschinl@45932  819 lemma atLeastAtMost_insertL: "m \ n \ insert m {Suc m..n} = {m ..n}"  noschinl@45932  820 by auto  noschinl@45932  821 wenzelm@60758  822 text \The analogous result is useful on @{typ int}:\  kleing@43157  823 (* here, because we don't have an own int section *)  kleing@43157  824 lemma atLeastAtMostPlus1_int_conv:  kleing@43157  825  "m <= 1+n \ {m..1+n} = insert (1+n) {m..n::int}"  kleing@43157  826  by (auto intro: set_eqI)  kleing@43157  827 paulson@33044  828 lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j..Intervals and numerals\  lp15@57113  834 wenzelm@61799  835 lemma lessThan_nat_numeral: \\Evaluation for specific numerals\  lp15@57113  836  "lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))"  lp15@57113  837  by (simp add: numeral_eq_Suc lessThan_Suc)  lp15@57113  838 wenzelm@61799  839 lemma atMost_nat_numeral: \\Evaluation for specific numerals\  lp15@57113  840  "atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))"  lp15@57113  841  by (simp add: numeral_eq_Suc atMost_Suc)  lp15@57113  842 wenzelm@61799  843 lemma atLeastLessThan_nat_numeral: \\Evaluation for specific numerals\  hoelzl@62369  844  "atLeastLessThan m (numeral k :: nat) =  lp15@57113  845  (if m \ (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k))  lp15@57113  846  else {})"  lp15@57113  847  by (simp add: numeral_eq_Suc atLeastLessThanSuc)  lp15@57113  848 wenzelm@60758  849 subsubsection \Image\  nipkow@16733  850 lp15@60809  851 lemma image_add_atLeastAtMost [simp]:  lp15@60615  852  fixes k ::"'a::linordered_semidom"  lp15@60615  853  shows "(\n. n+k)  {i..j} = {i+k..j+k}" (is "?A = ?B")  nipkow@16733  854 proof  nipkow@16733  855  show "?A \ ?B" by auto  nipkow@16733  856 next  nipkow@16733  857  show "?B \ ?A"  nipkow@16733  858  proof  nipkow@16733  859  fix n assume a: "n : ?B"  lp15@60615  860  hence "n - k : {i..j}"  lp15@60615  861  by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le)  lp15@60615  862  moreover have "n = (n - k) + k" using a  lp15@60615  863  proof -  lp15@60615  864  have "k + i \ n"  lp15@60615  865  by (metis a add.commute atLeastAtMost_iff)  lp15@60615  866  hence "k + (n - k) = n"  lp15@60615  867  by (metis (no_types) ab_semigroup_add_class.add_ac(1) add_diff_cancel_left' le_add_diff_inverse)  lp15@60615  868  thus ?thesis  lp15@60615  869  by (simp add: add.commute)  lp15@60615  870  qed  nipkow@16733  871  ultimately show "n : ?A" by blast  nipkow@16733  872  qed  nipkow@16733  873 qed  nipkow@16733  874 lp15@60809  875 lemma image_diff_atLeastAtMost [simp]:  lp15@60809  876  fixes d::"'a::linordered_idom" shows "(op - d  {a..b}) = {d-b..d-a}"  lp15@60809  877  apply auto  lp15@60809  878  apply (rule_tac x="d-x" in rev_image_eqI, auto)  lp15@60809  879  done  lp15@60809  880 lp15@60809  881 lemma image_mult_atLeastAtMost [simp]:  lp15@60809  882  fixes d::"'a::linordered_field"  lp15@60809  883  assumes "d>0" shows "(op * d  {a..b}) = {d*a..d*b}"  lp15@60809  884  using assms  lp15@60809  885  by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])  lp15@60809  886 lp15@60809  887 lemma image_affinity_atLeastAtMost:  lp15@60809  888  fixes c :: "'a::linordered_field"  lp15@60809  889  shows "((\x. m*x + c)  {a..b}) = (if {a..b}={} then {}  lp15@60809  890  else if 0 \ m then {m*a + c .. m *b + c}  lp15@60809  891  else {m*b + c .. m*a + c})"  lp15@60809  892  apply (case_tac "m=0", auto simp: mult_le_cancel_left)  lp15@60809  893  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)  lp15@60809  894  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)  lp15@60809  895  done  lp15@60809  896 lp15@60809  897 lemma image_affinity_atLeastAtMost_diff:  lp15@60809  898  fixes c :: "'a::linordered_field"  lp15@60809  899  shows "((\x. m*x - c)  {a..b}) = (if {a..b}={} then {}  lp15@60809  900  else if 0 \ m then {m*a - c .. m*b - c}  lp15@60809  901  else {m*b - c .. m*a - c})"  lp15@60809  902  using image_affinity_atLeastAtMost [of m "-c" a b]  lp15@60809  903  by simp  lp15@60809  904 paulson@61204  905 lemma image_affinity_atLeastAtMost_div:  paulson@61204  906  fixes c :: "'a::linordered_field"  paulson@61204  907  shows "((\x. x/m + c)  {a..b}) = (if {a..b}={} then {}  paulson@61204  908  else if 0 \ m then {a/m + c .. b/m + c}  paulson@61204  909  else {b/m + c .. a/m + c})"  paulson@61204  910  using image_affinity_atLeastAtMost [of "inverse m" c a b]  paulson@61204  911  by (simp add: field_class.field_divide_inverse algebra_simps)  hoelzl@62369  912 lp15@60809  913 lemma image_affinity_atLeastAtMost_div_diff:  lp15@60809  914  fixes c :: "'a::linordered_field"  lp15@60809  915  shows "((\x. x/m - c)  {a..b}) = (if {a..b}={} then {}  lp15@60809  916  else if 0 \ m then {a/m - c .. b/m - c}  lp15@60809  917  else {b/m - c .. a/m - c})"  lp15@60809  918  using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]  lp15@60809  919  by (simp add: field_class.field_divide_inverse algebra_simps)  lp15@60809  920 nipkow@16733  921 lemma image_add_atLeastLessThan:  nipkow@16733  922  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  925 next  nipkow@16733  926  show "?B \ ?A"  nipkow@16733  927  proof  nipkow@16733  928  fix n assume a: "n : ?B"  webertj@20217  929  hence "n - k : {i..i. i - c)  {x ..< y} =  hoelzl@37664  971  (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"  hoelzl@37664  972  (is "_ = ?right")  hoelzl@37664  973 proof safe  hoelzl@37664  974  fix a assume a: "a \ ?right"  hoelzl@37664  975  show "a \ (\i. i - c)  {x ..< y}"  hoelzl@37664  976  proof cases  hoelzl@37664  977  assume "c < y" with a show ?thesis  hoelzl@37664  978  by (auto intro!: image_eqI[of _ _ "a + c"])  hoelzl@37664  979  next  hoelzl@37664  980  assume "\ c < y" with a show ?thesis  nipkow@62390  981  by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)  hoelzl@37664  982  qed  hoelzl@37664  983 qed auto  hoelzl@37664  984 Andreas@51152  985 lemma image_int_atLeastLessThan: "int  {a.. uminus  {x<..}"  hoelzl@35580  999  by (rule imageI) (simp add: *)  hoelzl@35580  1000  thus "y \ uminus  {x<..}" by simp  hoelzl@35580  1001 next  hoelzl@35580  1002  fix y assume "y \ -x"  hoelzl@35580  1003  have "- (-y) \ uminus  {x..}"  wenzelm@60758  1004  by (rule imageI) (insert \y \ -x\[THEN le_imp_neg_le], simp)  hoelzl@35580  1005  thus "y \ uminus  {x..}" by simp  hoelzl@35580  1006 qed simp_all  hoelzl@35580  1007 hoelzl@35580  1008 lemma  hoelzl@35580  1009  fixes x :: 'a  hoelzl@35580  1010  shows image_uminus_lessThan[simp]: "uminus  {..Finiteness\  paulson@14485  1031 nipkow@15045  1032 lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..A bounded set of natural numbers is finite.\  paulson@14485  1055 lemma bounded_nat_set_is_finite:  nipkow@24853  1056  "(ALL i:N. i < (n::nat)) ==> finite N"  nipkow@28068  1057 apply (rule finite_subset)  nipkow@28068  1058  apply (rule_tac [2] finite_lessThan, auto)  nipkow@28068  1059 done  nipkow@28068  1060 wenzelm@60758  1061 text \A set of natural numbers is finite iff it is bounded.\  nipkow@31044  1062 lemma finite_nat_set_iff_bounded:  nipkow@31044  1063  "finite(N::nat set) = (EX m. ALL n:N. n?F\, simplified less_Suc_eq_le[symmetric]] by blast  nipkow@31044  1067 next  wenzelm@60758  1068  assume ?B show ?F using \?B\ by(blast intro:bounded_nat_set_is_finite)  nipkow@31044  1069 qed  nipkow@31044  1070 nipkow@31044  1071 lemma finite_nat_set_iff_bounded_le:  nipkow@31044  1072  "finite(N::nat set) = (EX m. ALL n:N. n<=m)"  nipkow@31044  1073 apply(simp add:finite_nat_set_iff_bounded)  nipkow@31044  1074 apply(blast dest:less_imp_le_nat le_imp_less_Suc)  nipkow@31044  1075 done  nipkow@31044  1076 nipkow@28068  1077 lemma finite_less_ub:  nipkow@28068  1078  "!!f::nat=>nat. (!!n. n \ f n) ==> finite {n. f n \ u}"  nipkow@28068  1079 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)  paulson@14485  1080 hoelzl@56328  1081 wenzelm@60758  1082 text\Any subset of an interval of natural numbers the size of the  wenzelm@60758  1083 subset is exactly that interval.\  nipkow@24853  1084 nipkow@24853  1085 lemma subset_card_intvl_is_intvl:  blanchet@55085  1086  assumes "A \ {k.. A" by auto  blanchet@55085  1096  with insert have "A <= {k..Proving Inclusions and Equalities between Unions\  paulson@32596  1107 nipkow@36755  1108 lemma UN_le_eq_Un0:  nipkow@36755  1109  "(\i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B")  nipkow@36755  1110 proof  nipkow@36755  1111  show "?A <= ?B"  nipkow@36755  1112  proof  nipkow@36755  1113  fix x assume "x : ?A"  nipkow@36755  1114  then obtain i where i: "i\n" "x : M i" by auto  nipkow@36755  1115  show "x : ?B"  nipkow@36755  1116  proof(cases i)  nipkow@36755  1117  case 0 with i show ?thesis by simp  nipkow@36755  1118  next  nipkow@36755  1119  case (Suc j) with i show ?thesis by auto  nipkow@36755  1120  qed  nipkow@36755  1121  qed  nipkow@36755  1122 next  wenzelm@63171  1123  show "?B <= ?A" by fastforce  nipkow@36755  1124 qed  nipkow@36755  1125 nipkow@36755  1126 lemma UN_le_add_shift:  nipkow@36755  1127  "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B")  nipkow@36755  1128 proof  nipkow@44890  1129  show "?A <= ?B" by fastforce  nipkow@36755  1130 next  nipkow@36755  1131  show "?B <= ?A"  nipkow@36755  1132  proof  nipkow@36755  1133  fix x assume "x : ?B"  nipkow@36755  1134  then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto  nipkow@36755  1135  hence "i-k\n & x : M((i-k)+k)" by auto  nipkow@36755  1136  thus "x : ?A" by blast  nipkow@36755  1137  qed  nipkow@36755  1138 qed  nipkow@36755  1139 hoelzl@62369  1140 lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)"  hoelzl@62369  1141  by (auto simp add: atLeast0LessThan)  paulson@32596  1142 haftmann@62343  1143 lemma UN_finite_subset:  haftmann@62343  1144  "(\n::nat. (\i\{0.. C) \ (\n. A n) \ C"  paulson@32596  1145  by (subst UN_UN_finite_eq [symmetric]) blast  paulson@32596  1146 hoelzl@62369  1147 lemma UN_finite2_subset:  haftmann@62343  1148  assumes "\n::nat. (\i\{0.. (\i\{0..n. A n) \ (\n. B n)"  haftmann@62343  1150 proof (rule UN_finite_subset, rule)  haftmann@62343  1151  fix n and a  haftmann@62343  1152  from assms have "(\i\{0.. (\i\{0.. (\i\{0.. (\i\{0.. (\i. B i)" by (auto simp add: UN_UN_finite_eq)  haftmann@62343  1156 qed  paulson@32596  1157 paulson@32596  1158 lemma UN_finite2_eq:  haftmann@62343  1159  "(\n::nat. (\i\{0..i\{0..  haftmann@62343  1160  (\n. A n) = (\n. B n)"  paulson@33044  1161  apply (rule subset_antisym)  paulson@33044  1162  apply (rule UN_finite2_subset, blast)  haftmann@62343  1163  apply (rule UN_finite2_subset [where k=k])  haftmann@62343  1164  apply (force simp add: atLeastLessThan_add_Un [of 0])  haftmann@62343  1165  done  paulson@32596  1166 paulson@32596  1167 wenzelm@60758  1168 subsubsection \Cardinality\  paulson@14485  1169 nipkow@15045  1170 lemma card_lessThan [simp]: "card {.. {0.. {0..n}"  wenzelm@63915  1207  shows "finite N"  haftmann@63417  1208  using assms finite_atLeastAtMost by (rule finite_subset)  haftmann@63365  1209 nipkow@26105  1210 lemma ex_bij_betw_nat_finite:  nipkow@26105  1211  "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  1222 apply(drule ex_bij_betw_finite_nat)  nipkow@31438  1223 apply(drule ex_bij_betw_nat_finite)  nipkow@31438  1224 apply(auto intro!:bij_betw_trans)  nipkow@31438  1225 done  nipkow@31438  1226 nipkow@31438  1227 lemma ex_bij_betw_nat_finite_1:  nipkow@31438  1228  "finite M \ \h. bij_betw h {1 .. card M} M"  nipkow@31438  1229 by (rule finite_same_card_bij) auto  nipkow@31438  1230 hoelzl@40703  1231 lemma bij_betw_iff_card:  lp15@63114  1232  assumes "finite A" "finite B"  lp15@63114  1233  shows "(\f. bij_betw f A B) \ (card A = card B)"  lp15@63114  1234 proof  lp15@63114  1235  assume "card A = card B"  lp15@63114  1236  moreover obtain f where "bij_betw f A {0 ..< card A}"  lp15@63114  1237  using assms ex_bij_betw_finite_nat by blast  hoelzl@40703  1238  moreover obtain g where "bij_betw g {0 ..< card B} B"  lp15@63114  1239  using assms ex_bij_betw_nat_finite by blast  hoelzl@40703  1240  ultimately have "bij_betw (g o f) A B"  lp15@63114  1241  by (auto simp: bij_betw_trans)  hoelzl@40703  1242  thus "(\f. bij_betw f A B)" by blast  lp15@63114  1243 qed (auto simp: bij_betw_same_card)  hoelzl@40703  1244 hoelzl@40703  1245 lemma inj_on_iff_card_le:  hoelzl@40703  1246  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  1247  shows "(\f. inj_on f A \ f  A \ B) = (card A \ card B)"  hoelzl@40703  1248 proof (safe intro!: card_inj_on_le)  hoelzl@40703  1249  assume *: "card A \ card B"  hoelzl@40703  1250  obtain f where 1: "inj_on f A" and 2: "f  A = {0 ..< card A}"  hoelzl@40703  1251  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force  hoelzl@40703  1252  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g  {0 ..< card B} = B"  hoelzl@40703  1253  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force  hoelzl@40703  1254  ultimately have "inj_on g (f  A)" using subset_inj_on[of g _ "f  A"] * by force  hoelzl@40703  1255  hence "inj_on (g o f) A" using 1 comp_inj_on by blast  hoelzl@40703  1256  moreover  hoelzl@40703  1257  {have "{0 ..< card A} \ {0 ..< card B}" using * by force  hoelzl@40703  1258  with 2 have "f  A \ {0 ..< card B}" by blast  hoelzl@40703  1259  hence "(g o f)  A \ B" unfolding comp_def using 3 by force  hoelzl@40703  1260  }  hoelzl@40703  1261  ultimately show "(\f. inj_on f A \ f  A \ B)" by blast  hoelzl@40703  1262 qed (insert assms, auto)  nipkow@26105  1263 haftmann@63417  1264 lemma subset_eq_atLeast0_lessThan_card:  haftmann@63365  1265  fixes n :: nat  haftmann@63417  1266  assumes "N \ {0.. n"  haftmann@63365  1268 proof -  haftmann@63417  1269  from assms finite_lessThan have "card N \ card {0..Intervals of integers\  paulson@14485  1276 nipkow@15045  1277 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..Finiteness\  paulson@14485  1288 paulson@15418  1289 lemma image_atLeastZeroLessThan_int: "0 \ u ==>  nipkow@15045  1290  {(0::int).. u")  paulson@14485  1299  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1300  apply (rule finite_imageI)  paulson@14485  1301  apply auto  paulson@14485  1302  done  paulson@14485  1303 nipkow@15045  1304 lemma finite_atLeastLessThan_int [iff]: "finite {l..Cardinality\  paulson@14485  1323 nipkow@15045  1324 lemma card_atLeastZeroLessThan_int: "card {(0::int).. u")  paulson@14485  1326  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1327  apply (subst card_image)  paulson@14485  1328  apply (auto simp add: inj_on_def)  paulson@14485  1329  done  paulson@14485  1330 nipkow@15045  1331 lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}"  bulwahn@27656  1353 proof -  bulwahn@27656  1354  have "{k. P k \ k < i} \ {.. M"  bulwahn@27656  1360 shows "card {k \ M. k < Suc i} \ 0"  bulwahn@27656  1361 proof -  bulwahn@27656  1362  from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto  bulwahn@27656  1363  with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)  bulwahn@27656  1364 qed  bulwahn@27656  1365 bulwahn@27656  1366 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"  haftmann@37388  1367 apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"])  bulwahn@27656  1368 apply auto  bulwahn@27656  1369 apply (rule inj_on_diff_nat)  bulwahn@27656  1370 apply auto  bulwahn@27656  1371 apply (case_tac x)  bulwahn@27656  1372 apply auto  bulwahn@27656  1373 apply (case_tac xa)  bulwahn@27656  1374 apply auto  bulwahn@27656  1375 apply (case_tac xa)  bulwahn@27656  1376 apply auto  bulwahn@27656  1377 done  bulwahn@27656  1378 bulwahn@27656  1379 lemma card_less_Suc:  bulwahn@27656  1380  assumes zero_in_M: "0 \ M"  bulwahn@27656  1381  shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"  bulwahn@27656  1382 proof -  bulwahn@27656  1383  from assms have a: "0 \ {k \ M. k < Suc i}" by simp  bulwahn@27656  1384  hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})"  bulwahn@27656  1385  by (auto simp only: insert_Diff)  bulwahn@27656  1386  have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto  hoelzl@62369  1387  from finite_M_bounded_by_nat[of "\x. x \ M" "Suc i"]  lp15@57113  1388  have "Suc (card {k. Suc k \ M \ k < i}) = card (insert 0 ({k \ M. k < Suc i} - {0}))"  bulwahn@27656  1389  apply (subst card_insert)  bulwahn@27656  1390  apply simp_all  bulwahn@27656  1391  apply (subst b)  bulwahn@27656  1392  apply (subst card_less_Suc2[symmetric])  bulwahn@27656  1393  apply simp_all  bulwahn@27656  1394  done  bulwahn@27656  1395  with c show ?thesis by simp  bulwahn@27656  1396 qed  bulwahn@27656  1397 paulson@14485  1398 wenzelm@60758  1399 subsection \Lemmas useful with the summation operator setsum\  paulson@13850  1400 wenzelm@60758  1401 text \For examples, see Algebra/poly/UnivPoly2.thy\  ballarin@13735  1402 wenzelm@60758  1403 subsubsection \Disjoint Unions\  ballarin@13735  1404 wenzelm@60758  1405 text \Singletons and open intervals\  ballarin@13735  1406 ballarin@13735  1407 lemma ivl_disj_un_singleton:  nipkow@15045  1408  "{l::'a::linorder} Un {l<..} = {l..}"  nipkow@15045  1409  "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  1413  "(l::'a::linorder) <= u ==> {l..One- and two-sided intervals\  ballarin@13735  1417 ballarin@13735  1418 lemma ivl_disj_un_one:  nipkow@15045  1419  "(l::'a::linorder) < u ==> {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  1422  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  1424  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  1426  "(l::'a::linorder) <= u ==> {l..Two- and two-sided intervals\  ballarin@13735  1430 ballarin@13735  1431 lemma ivl_disj_un_two:  nipkow@15045  1432  "[| (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  1438  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  1440 by auto  ballarin@13735  1441 lp15@60150  1442 lemma ivl_disj_un_two_touch:  lp15@60150  1443  "[| (l::'a::linorder) < m; m < u |] ==> {l<..m} Un {m.. {l..m} Un {m.. {l<..m} Un {m..u} = {l<..u}"  lp15@60150  1446  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m..u} = {l..u}"  lp15@60150  1447 by auto  lp15@60150  1448 lp15@60150  1449 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ivl_disj_un_two_touch  ballarin@13735  1450 wenzelm@60758  1451 subsubsection \Disjoint Intersections\  ballarin@13735  1452 wenzelm@60758  1453 text \One- and two-sided intervals\  ballarin@13735  1454 ballarin@13735  1455 lemma ivl_disj_int_one:  nipkow@15045  1456  "{..l::'a::order} Int {l<..Two- and two-sided intervals\  ballarin@13735  1467 ballarin@13735  1468 lemma ivl_disj_int_two:  nipkow@15045  1469  "{l::'a::order<..Some Differences\  nipkow@15542  1482 nipkow@15542  1483 lemma ivl_diff[simp]:  nipkow@15542  1484  "i \ n \ {i..Some Subset Conditions\  nipkow@15542  1497 blanchet@54147  1498 lemma ivl_subset [simp]:  nipkow@15542  1499  "({i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  1500 apply(auto simp:linorder_not_le)  nipkow@15542  1501 apply(rule ccontr)  nipkow@15542  1502 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  1503 apply(clarsimp simp:linorder_not_le)  nipkow@44890  1504 apply(fastforce)  nipkow@15542  1505 done  nipkow@15542  1506 nipkow@15041  1507 haftmann@63417  1508 subsection \Generic big monoid operation over intervals\  haftmann@63417  1509 haftmann@63417  1510 lemma inj_on_add_nat' [simp]:  haftmann@63417  1511  "inj_on (plus k) N" for k :: nat  haftmann@63417  1512  by rule simp  haftmann@63417  1513 haftmann@63417  1514 context comm_monoid_set  haftmann@63417  1515 begin  haftmann@63417  1516 haftmann@63417  1517 lemma atLeast_lessThan_shift_bounds:  haftmann@63417  1518  fixes m n k :: nat  haftmann@63417  1519  shows "F g {m + k.. plus k) {m.. plus k) {m.. plus k) {m..n}"  haftmann@63417  1531 proof -  haftmann@63417  1532  have "{m + k..n + k} = plus k  {m..n}"  haftmann@63417  1533  by (auto simp del: image_add_atLeastAtMost simp add: image_add_atLeastAtMost [symmetric])  haftmann@63417  1534  also have "F g (plus k  {m..n}) = F (g \ plus k) {m..n}"  haftmann@63417  1535  by (rule reindex) simp  haftmann@63417  1536  finally show ?thesis .  haftmann@63417  1537 qed  haftmann@63417  1538 haftmann@63417  1539 lemma atLeast_Suc_lessThan_Suc_shift:  haftmann@63417  1540  "F g {Suc m.. Suc) {m.. Suc) {m..n}"  haftmann@63417  1545  using atLeast_atMost_shift_bounds [of _ _ 1] by simp  haftmann@63417  1546 haftmann@63417  1547 lemma atLeast0_lessThan_Suc:  haftmann@63417  1548  "F g {0..* g n"  haftmann@63417  1549  by (simp add: atLeast0_lessThan_Suc ac_simps)  haftmann@63417  1550 haftmann@63417  1551 lemma atLeast0_atMost_Suc:  haftmann@63417  1552  "F g {0..Suc n} = F g {0..n} \<^bold>* g (Suc n)"  haftmann@63417  1553  by (simp add: atLeast0_atMost_Suc ac_simps)  haftmann@63417  1554 haftmann@63417  1555 lemma atLeast0_lessThan_Suc_shift:  haftmann@63417  1556  "F g {0..* F (g \ Suc) {0..* F (g \ Suc) {0..n}"  haftmann@63417  1561  by (simp add: atLeast0_atMost_Suc_eq_insert_0 atLeast_Suc_atMost_Suc_shift)  haftmann@63417  1562 haftmann@63417  1563 lemma ivl_cong:  haftmann@63417  1564  "a = c \ b = d \ (\x. c \ x \ x < d \ g x = h x)  haftmann@63417  1565  \ F g {a.. plus m) {0.. n") simp_all  haftmann@63417  1573 haftmann@63417  1574 lemma atLeast_atMost_shift_0:  haftmann@63417  1575  fixes m n p :: nat  haftmann@63417  1576  assumes "m \ n"  haftmann@63417  1577  shows "F g {m..n} = F (g \ plus m) {0..n - m}"  haftmann@63417  1578  using assms atLeast_atMost_shift_bounds [of g 0 m "n - m"] by simp  haftmann@63417  1579 haftmann@63417  1580 lemma atLeast_lessThan_concat:  haftmann@63417  1581  fixes m n p :: nat  haftmann@63417  1582  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  1592  by (rule reindex_bij_witness [where i="\i. m + n - i" and j="\i. m + n - i"]) auto  haftmann@63417  1593 haftmann@63417  1594 lemma atLeast_lessThan_rev_at_least_Suc_atMost:  haftmann@63417  1595  "F g {n..i. g (m + n - i)) {Suc n..m}"  haftmann@63417  1596  unfolding atLeast_lessThan_rev [of g n m]  haftmann@63417  1597  by (cases m) (simp_all add: atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost)  haftmann@63417  1598 haftmann@63417  1599 end  haftmann@63417  1600 haftmann@63417  1601 wenzelm@60758  1602 subsection \Summation indexed over intervals\  nipkow@15042  1603 wenzelm@61955  1604 syntax (ASCII)  wenzelm@61955  1605  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  wenzelm@61955  1606  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  wenzelm@61955  1607  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  wenzelm@61955  1608  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  wenzelm@61955  1609 nipkow@15056  1610 syntax (latex_sum output)  nipkow@15052  1611  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  1612  ("(3\<^raw:\sum_{>_ = _\<^raw:}^{>_\<^raw:}> _)" [0,0,0,10] 10)  nipkow@15052  1613  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  1614  ("(3\<^raw:\sum_{>_ = _\<^raw:}^{<>_\<^raw:}> _)" [0,0,0,10] 10)  nipkow@16052  1615  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1616  ("(3\<^raw:\sum_{>_ < _\<^raw:}> _)" [0,0,10] 10)  nipkow@15052  1617  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1618  ("(3\<^raw:\sum_{>_ \ _\<^raw:}> _)" [0,0,10] 10)  nipkow@15041  1619 wenzelm@61955  1620 syntax  wenzelm@61955  1621  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  wenzelm@61955  1622  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  wenzelm@61955  1623  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  wenzelm@61955  1624  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  wenzelm@61955  1625 nipkow@15048  1626 translations  wenzelm@61955  1627  "\x=a..b. t" == "CONST setsum (\x. t) {a..b}"  wenzelm@61955  1628  "\x=a..x. t) {a..i\n. t" == "CONST setsum (\i. t) {..n}"  nipkow@28853  1630  "\ii. t) {..The above introduces some pretty alternative syntaxes for  nipkow@15056  1633 summation over intervals:  nipkow@15052  1634 \begin{center}  nipkow@15052  1635 \begin{tabular}{lll}  nipkow@15056  1636 Old & New & \LaTeX\\  nipkow@15056  1637 @{term[source]"\x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  1638 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  1640 @{term[source]"\x\{..xxlatex_sum\ (e.g.\ via \mode = latex_sum\ in  nipkow@15056  1648 antiquotations). It is not the default \LaTeX\ output because it only  nipkow@15056  1649 works well with italic-style formulae, not tt-style.  nipkow@15052  1650 nipkow@15052  1651 Note that for uniformity on @{typ nat} it is better to use  wenzelm@61799  1652 @{term"\x::nat=0..\x: \setsum\ may  nipkow@15052  1653 not provide all lemmas available for @{term"{m..  nipkow@15052  1655 wenzelm@60758  1656 text\This congruence rule should be used for sums over intervals as  haftmann@57418  1657 the standard theorem @{text[source]setsum.cong} does not work well  nipkow@15542  1658 with the simplifier who adds the unsimplified premise @{term"x:B"} to  wenzelm@60758  1659 the context.\  nipkow@15542  1660 haftmann@63417  1661 lemmas setsum_ivl_cong = setsum.ivl_cong  nipkow@15041  1662 nipkow@16041  1663 (* FIXME why are the following simp rules but the corresponding eqns  nipkow@16041  1664 on intervals are not? *)  nipkow@16041  1665 haftmann@63417  1666 lemma setsum_atMost_Suc [simp]:  haftmann@63417  1667  "(\i \ Suc n. f i) = (\i \ n. f i) + f (Suc n)"  haftmann@63417  1668  by (simp add: atMost_Suc ac_simps)  nipkow@16052  1669 haftmann@63417  1670 lemma setsum_lessThan_Suc [simp]:  haftmann@63417  1671  "(\i < Suc n. f i) = (\i < n. f i) + f n"  haftmann@63417  1672  by (simp add: lessThan_Suc ac_simps)  nipkow@15041  1673 haftmann@63417  1674 lemma setsum_cl_ivl_Suc [simp]:  nipkow@15561  1675  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  haftmann@63417  1676  by (auto simp: ac_simps atLeastAtMostSuc_conv)  nipkow@15561  1677 haftmann@63417  1678 lemma setsum_op_ivl_Suc [simp]:  nipkow@15561  1679  "setsum f {m..  nipkow@15561  1683  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  haftmann@57514  1684 by (auto simp:ac_simps atLeastAtMostSuc_conv)  nipkow@16041  1685 *)  nipkow@28068  1686 nipkow@28068  1687 lemma setsum_head:  nipkow@28068  1688  fixes n :: nat  hoelzl@62369  1689  assumes mn: "m <= n"  nipkow@28068  1690  shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  nipkow@28068  1691 proof -  nipkow@28068  1692  from mn  nipkow@28068  1693  have "{m..n} = {m} \ {m<..n}"  nipkow@28068  1694  by (auto intro: ivl_disj_un_singleton)  nipkow@28068  1695  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  nipkow@28068  1696  by (simp add: atLeast0LessThan)  nipkow@28068  1697  also have "\ = ?rhs" by simp  nipkow@28068  1698  finally show ?thesis .  nipkow@28068  1699 qed  nipkow@28068  1700 nipkow@28068  1701 lemma setsum_head_Suc:  nipkow@28068  1702  "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}"  nipkow@28068  1703 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)  nipkow@28068  1704 nipkow@28068  1705 lemma setsum_head_upt_Suc:  nipkow@28068  1706  "m < n \ setsum f {m.. n + 1"  nipkow@31501  1712  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"  nipkow@31501  1713 proof-  wenzelm@60758  1714  have "{m .. n+p} = {m..n} \ {n+1..n+p}" using \m \ n+1\ by auto  haftmann@57418  1715  thus ?thesis by (auto simp: ivl_disj_int setsum.union_disjoint  nipkow@31501  1716  atLeastSucAtMost_greaterThanAtMost)  nipkow@31501  1717 qed  nipkow@28068  1718 haftmann@63417  1719 lemmas setsum_add_nat_ivl = setsum.atLeast_lessThan_concat  nipkow@15539  1720 nipkow@15539  1721 lemma setsum_diff_nat_ivl:  nipkow@15539  1722 fixes f :: "nat \ 'a::ab_group_add"  nipkow@15539  1723 shows "\ m \ n; n \ p \ \  nipkow@15539  1724  setsum f {m.. ('a::ab_group_add)"  nipkow@31505  1731  shows "setsum (\k. f k - f(k + 1)) {(m::nat) .. n} =  nipkow@31505  1732  (if m <= n then f m - f(n + 1) else 0)"  nipkow@31505  1733 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)  nipkow@31505  1734 hoelzl@56194  1735 lemma setsum_nat_group: "(\m(i,j)\{(i,j). i+j < n}. f i j) = (\ki\k. f i (k - i))"  lp15@60150  1744  apply (simp add: setsum.Sigma)  lp15@60150  1745  apply (rule setsum.reindex_bij_witness[where j="\(i, j). (i+j, i)" and i="\(k, i). (i, k - i)"])  lp15@60150  1746  apply auto  lp15@60150  1747  done  lp15@60150  1748 lp15@60150  1749 lemma setsum_triangle_reindex_eq:  lp15@60150  1750  fixes n :: nat  lp15@60150  1751  shows "(\(i,j)\{(i,j). i+j \ n}. f i j) = (\k\n. \i\k. f i (k - i))"  lp15@60150  1752 using setsum_triangle_reindex [of f "Suc n"]  lp15@60150  1753 by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost)  lp15@60150  1754 lp15@60162  1755 lemma nat_diff_setsum_reindex: "(\iiShifting bounds\  nipkow@16733  1760 nipkow@15539  1761 lemma setsum_shift_bounds_nat_ivl:  nipkow@15539  1762  "setsum f {m+k.. setsum f {Suc 0..k} = setsum f {0..k}"  nipkow@28068  1779 by(simp add:setsum_head_Suc)  kleing@19106  1780 nipkow@28068  1781 lemma setsum_shift_lb_Suc0_0_upt:  nipkow@28068  1782  "f(0::nat) = 0 \ setsum f {Suc 0.. 'a::comm_monoid_add"  haftmann@52380  1789  shows "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))"  haftmann@52380  1790 proof (induct n)  haftmann@52380  1791  case 0 show ?case by simp  haftmann@52380  1792 next  haftmann@52380  1793  case (Suc n) note IH = this  haftmann@52380  1794  have "(\i\Suc (Suc n). f i) = (\i\Suc n. f i) + f (Suc (Suc n))"  haftmann@52380  1795  by (rule setsum_atMost_Suc)  haftmann@52380  1796  also have "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))"  haftmann@52380  1797  by (rule IH)  haftmann@52380  1798  also have "f 0 + (\i\n. f (Suc i)) + f (Suc (Suc n)) =  haftmann@52380  1799  f 0 + ((\i\n. f (Suc i)) + f (Suc (Suc n)))"  haftmann@57512  1800  by (rule add.assoc)  haftmann@52380  1801  also have "(\i\n. f (Suc i)) + f (Suc (Suc n)) = (\i\Suc n. f (Suc i))"  haftmann@52380  1802  by (rule setsum_atMost_Suc [symmetric])  haftmann@52380  1803  finally show ?case .  haftmann@52380  1804 qed  haftmann@52380  1805 eberlm@63099  1806 lemma setsum_lessThan_Suc_shift:  eberlm@63099  1807  "(\ii 'a::comm_monoid_add"  lp15@62379  1812  shows "(\i\n. f i) = f 0 + (\i (\i = m..n. f i) = f n + (\i = m.. 'a::ab_group_add"  lp15@56238  1820  assumes "m \ Suc n"  lp15@56238  1821  shows "(\i = m..n. f(Suc i) - f i) = f (Suc n) - f m"  lp15@56238  1822 using assms by (induct n) (auto simp: le_Suc_eq)  lp15@55718  1823 lp15@55718  1824 lemma nested_setsum_swap:  lp15@55718  1825  "(\i = 0..n. (\j = 0..j = 0..i = Suc j..n. a i j)"  haftmann@57418  1826  by (induction n) (auto simp: setsum.distrib)  lp15@55718  1827 lp15@56215  1828 lemma nested_setsum_swap':  lp15@56215  1829  "(\i\n. (\jji = Suc j..n. a i j)"  haftmann@57418  1830  by (induction n) (auto simp: setsum.distrib)  lp15@56215  1831 haftmann@63365  1832 lemma setsum_atLeast1_atMost_eq:  haftmann@63365  1833  "setsum f {Suc 0..n} = (\k = (\kTelescoping\  eberlm@61524  1844 eberlm@61524  1845 lemma setsum_telescope:  eberlm@61524  1846  fixes f::"nat \ 'a::ab_group_add"  eberlm@61524  1847  shows "setsum (\i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)"  eberlm@61524  1848  by (induct i) simp_all  eberlm@61524  1849 eberlm@61524  1850 lemma setsum_telescope'':  eberlm@61524  1851  assumes "m \ n"  eberlm@61524  1852  shows "(\k\{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)"  eberlm@61524  1853  by (rule dec_induct[OF assms]) (simp_all add: algebra_simps)  eberlm@61524  1854 eberlm@63721  1855 lemma setsum_lessThan_telescope:  eberlm@63721  1856  "(\nnThe formula for geometric sums\  ballarin@17149  1865 ballarin@17149  1866 lemma geometric_sum:  haftmann@36307  1867  assumes "x \ 1"  hoelzl@56193  1868  shows "(\i 0" by simp_all  hoelzl@56193  1871  moreover have "(\iy \ 0$$  haftmann@36307  1873  ultimately show ?thesis by simp  haftmann@36307  1874 qed  haftmann@36307  1875 lp15@60162  1876 lemma diff_power_eq_setsum:  lp15@60162  1877  fixes y :: "'a::{comm_ring,monoid_mult}"  lp15@60162  1878  shows  lp15@60162  1879  "x ^ (Suc n) - y ^ (Suc n) =  lp15@60162  1880  (x - y) * (\pppp\\COMPLEX_POLYFUN\ in HOL Light\  lp15@60162  1897  fixes x :: "'a::{comm_ring,monoid_mult}"  lp15@60162  1898  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  1921 huffman@47222  1922 lemma gauss_sum:  hoelzl@56193  1923  "(2::'a::comm_semiring_1)*(\i\{1..n}. of_nat i) = of_nat n*((of_nat n)+1)"  kleing@19469  1924 proof (induct n)  kleing@19469  1925  case 0  kleing@19469  1926  show ?case by simp  kleing@19469  1927 next  kleing@19469  1928  case (Suc n)  huffman@47222  1929  then show ?case  huffman@47222  1930  by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one)  huffman@47222  1931  (* FIXME: make numeral cancellation simprocs work for semirings *)  kleing@19469  1932 qed  kleing@19469  1933 kleing@19469  1934 theorem arith_series_general:  huffman@47222  1935  "(2::'a::comm_semiring_1) * (\i\{.. 1"  kleing@19469  1939  let ?I = "\i. of_nat i" and ?n = "of_nat n"  kleing@19469  1940  have  kleing@19469  1941  "(\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  1954  by (simp only: mult.assoc gauss_sum [of "n - 1"], unfold One_nat_def)  haftmann@57514  1955  (simp add: mult.commute trans [OF add.commute of_nat_Suc [symmetric]])  huffman@47222  1956  finally show ?thesis  huffman@47222  1957  unfolding mult_2 by (simp add: algebra_simps)  kleing@19469  1958 next  kleing@19469  1959  assume "\(n > 1)"  kleing@19469  1960  hence "n = 1 \ n = 0" by auto  huffman@47222  1961  thus ?thesis by (auto simp: mult_2)  kleing@19469  1962 qed  kleing@19469  1963 kleing@19469  1964 lemma arith_series_nat:  huffman@47222  1965  "(2::nat) * (\i\{..i\{..i\{..x. Q x \ P x \ (\xxxDivision remainder\  haftmann@63417  1984 haftmann@63417  1985 lemma range_mod:  haftmann@63417  1986  fixes n :: nat  haftmann@63417  1987  assumes "n > 0"  haftmann@63417  1988  shows "range (\m. m mod n) = {0.. ?A \ m \ ?B"  haftmann@63417  1992  proof  haftmann@63417  1993  assume "m \ ?A"  haftmann@63417  1994  with assms show "m \ ?B"  wenzelm@63915  1995  by auto  haftmann@63417  1996  next  haftmann@63417  1997  assume "m \ ?B"  haftmann@63417  1998  moreover have "m mod n \ ?A"  haftmann@63417  1999  by (rule rangeI)  haftmann@63417  2000  ultimately show "m \ ?A"  haftmann@63417  2001  by simp  haftmann@63417  2002  qed  haftmann@63417  2003 qed  haftmann@63417  2004 haftmann@63417  2005 wenzelm@60758  2006 subsection \Products indexed over intervals\  paulson@29960  2007 wenzelm@61955  2008 syntax (ASCII)  wenzelm@61955  2009  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)  wenzelm@61955  2010  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)  wenzelm@61955  2011  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10)  wenzelm@61955  2012  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10)  wenzelm@61955  2013 paulson@29960  2014 syntax (latex_prod output)  paulson@29960  2015  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  2016  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  2017  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  2018  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  2019  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  2020  ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  2021  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  2022  ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  2023 wenzelm@61955  2024 syntax  wenzelm@61955  2025  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  wenzelm@61955  2026  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  wenzelm@61955  2027  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  wenzelm@61955  2028  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  wenzelm@61955  2029 paulson@29960  2030 translations  wenzelm@61955  2031  "\x=a..b. t" \ "CONST setprod (\x. t) {a..b}"  wenzelm@61955  2032  "\x=a.. "CONST setprod (\x. t) {a..i\n. t" \ "CONST setprod (\i. t) {..n}"  wenzelm@61955  2034  "\i "CONST setprod (\i. t) {..{int i..int (i+j)}"  lp15@55242  2037  by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)  lp15@55242  2038 lp15@55242  2039 lemma setprod_int_eq: "setprod int {i..j} = \{int i..int j}"  lp15@55242  2040 proof (cases "i \ j")  lp15@55242  2041  case True  lp15@55242  2042  then show ?thesis  hoelzl@62376  2043  by (metis le_iff_add setprod_int_plus_eq)  lp15@55242  2044 next  lp15@55242  2045  case False  lp15@55242  2046  then show ?thesis  lp15@55242  2047  by auto  lp15@55242  2048 qed  lp15@55242  2049 eberlm@61524  2050 haftmann@63417  2051 subsubsection \Shifting bounds\  eberlm@61524  2052 eberlm@61524  2053 lemma setprod_shift_bounds_nat_ivl:  eberlm@61524  2054  "setprod f {m+k..ii b \ setprod f {a.. Suc n"  eberlm@61524  2080  shows "setprod f {m..Suc n} = f (Suc n) * setprod f {m..n}"  eberlm@61524  2081 proof -  eberlm@61524  2082  from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto  eberlm@61524  2083  also have "setprod f \ = f (Suc n) * setprod f {m..n}" by simp  eberlm@61524  2084  finally show ?thesis .  eberlm@61524  2085 qed  eberlm@61524  2086 eberlm@62128  2087 eberlm@62128  2088 subsection \Efficient folding over intervals\  eberlm@62128  2089 eberlm@62128  2090 function fold_atLeastAtMost_nat where  eberlm@62128  2091  [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc =  eberlm@62128  2092  (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a acc))"  eberlm@62128  2093 by pat_completeness auto  eberlm@62128  2094 termination by (relation "measure (\(_,a,b,_). Suc b - a)") auto  eberlm@62128  2095 eberlm@62128  2096 lemma fold_atLeastAtMost_nat:  eberlm@62128  2097  assumes "comp_fun_commute f"  eberlm@62128  2098  shows "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}"  eberlm@62128  2099 using assms  eberlm@62128  2100 proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases)  eberlm@62128  2101  case (1 f a b acc)  eberlm@62128  2102  interpret comp_fun_commute f by fact  eberlm@62128  2103  show ?case  eberlm@62128  2104  proof (cases "a > b")  eberlm@62128  2105  case True  eberlm@62128  2106  thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto  eberlm@62128  2107  next  eberlm@62128  2108  case False  eberlm@62128  2109  with 1 show ?thesis  eberlm@62128  2110  by (subst fold_atLeastAtMost_nat.simps)  eberlm@62128  2111  (auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm)  eberlm@62128  2112  qed  eberlm@62128  2113 qed  eberlm@62128  2114 eberlm@62128  2115 lemma setsum_atLeastAtMost_code:  eberlm@62128  2116  "setsum f {a..b} = fold_atLeastAtMost_nat (\a acc. f a + acc) a b 0"  eberlm@62128  2117 proof -  eberlm@62128  2118  have "comp_fun_commute (\a. op + (f a))"  eberlm@62128  2119  by unfold_locales (auto simp: o_def add_ac)  eberlm@62128  2120  thus ?thesis  eberlm@62128  2121  by (simp add: setsum.eq_fold fold_atLeastAtMost_nat o_def)  eberlm@62128  2122 qed  eberlm@62128  2123 eberlm@62128  2124 lemma setprod_atLeastAtMost_code:  eberlm@62128  2125  "setprod f {a..b} = fold_atLeastAtMost_nat (\a acc. f a * acc) a b 1"  eberlm@62128  2126 proof -  eberlm@62128  2127  have "comp_fun_commute (\a. op * (f a))"  eberlm@62128  2128  by unfold_locales (auto simp: o_def mult_ac)  eberlm@62128  2129  thus ?thesis  eberlm@62128  2130  by (simp add: setprod.eq_fold fold_atLeastAtMost_nat o_def)  eberlm@62128  2131 qed  eberlm@62128  2132 eberlm@62128  2133 (* TODO: Add support for more kinds of intervals here *)  eberlm@62128  2134 haftmann@63417  2135 haftmann@63417  2136 subsection \Transfer setup\  haftmann@63417  2137 haftmann@63417  2138 lemma transfer_nat_int_set_functions:  haftmann@63417  2139  "{..n} = nat  {0..int n}"  haftmann@63417  2140  "{m..n} = nat  {int m..int n}" (* need all variants of these! *)  haftmann@63417  2141  apply (auto simp add: image_def)  haftmann@63417  2142  apply (rule_tac x = "int x" in bexI)  haftmann@63417  2143  apply auto  haftmann@63417  2144  apply (rule_tac x = "int x" in bexI)  haftmann@63417  2145  apply auto  haftmann@63417  2146  done  haftmann@63417  2147 haftmann@63417  2148 lemma transfer_nat_int_set_function_closures:  haftmann@63417  2149  "x >= 0 \ nat_set {x..y}"  haftmann@63417  2150  by (simp add: nat_set_def)  haftmann@63417  2151 haftmann@63417  2152 declare transfer_morphism_nat_int[transfer add  haftmann@63417  2153  return: transfer_nat_int_set_functions  haftmann@63417  2154  transfer_nat_int_set_function_closures  haftmann@63417  2155 ]  haftmann@63417  2156 haftmann@63417  2157 lemma transfer_int_nat_set_functions:  haftmann@63417  2158  "is_nat m \ is_nat n \ {m..n} = int  {nat m..nat n}"  haftmann@63417  2159  by (simp only: is_nat_def transfer_nat_int_set_functions  haftmann@63417  2160  transfer_nat_int_set_function_closures  haftmann@63417  2161  transfer_nat_int_set_return_embed nat_0_le  haftmann@63417  2162  cong: transfer_nat_int_set_cong)  haftmann@63417  2163 haftmann@63417  2164 lemma transfer_int_nat_set_function_closures:  haftmann@63417  2165  "is_nat x \ nat_set {x..y}"  haftmann@63417  2166  by (simp only: transfer_nat_int_set_function_closures is_nat_def)  haftmann@63417  2167 haftmann@63417  2168 declare transfer_morphism_int_nat[transfer add  haftmann@63417  2169  return: transfer_int_nat_set_functions  haftmann@63417  2170  transfer_int_nat_set_function_closures  haftmann@63417  2171 ]  haftmann@63417  2172 nipkow@8924  2173 end `