src/HOL/Set_Interval.thy
 author paulson Sat Apr 11 11:56:40 2015 +0100 (2015-04-11) changeset 60017 b785d6d06430 parent 59416 fde2659085e1 child 60150 bd773c47ad0b permissions -rw-r--r--
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
 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@58889  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 nipkow@15048  58 text{* A note of warning when using @{term"{.. '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 (xsymbols)  huffman@36364  69  "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\ _\_./ _)" [0, 0, 10] 10)  huffman@36364  70  "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" [0, 0, 10] 10)  huffman@36364  71  "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\ _\_./ _)" [0, 0, 10] 10)  huffman@36364  72  "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" [0, 0, 10] 10)  kleing@14418  73 nipkow@30372  74 syntax (latex output)  huffman@36364  75  "_UNION_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" [0, 0, 10] 10)  huffman@36364  76  "_UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" [0, 0, 10] 10)  huffman@36364  77  "_INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" [0, 0, 10] 10)  huffman@36364  78  "_INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" [0, 0, 10] 10)  kleing@14418  79 kleing@14418  80 translations  kleing@14418  81  "UN i<=n. A" == "UN i:{..n}. A"  nipkow@15045  82  "UN 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 paulson@14485  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 paulson@13850  184 subsection {*Two-sided intervals*}  ballarin@13735  185 nipkow@24691  186 context ord  nipkow@24691  187 begin  nipkow@24691  188 blanchet@54147  189 lemma greaterThanLessThan_iff [simp]:  haftmann@25062  190  "(i : {l<.. {..< b }"  hoelzl@50999  210  by auto  hoelzl@50999  211 nipkow@24691  212 end  ballarin@13735  213 nipkow@32400  214 subsubsection{* Emptyness, singletons, subset *}  nipkow@15554  215 nipkow@24691  216 context order  nipkow@24691  217 begin  nipkow@15554  218 nipkow@32400  219 lemma atLeastatMost_empty[simp]:  nipkow@32400  220  "b < a \ {a..b} = {}"  nipkow@32400  221 by(auto simp: atLeastAtMost_def atLeast_def atMost_def)  nipkow@32400  222 nipkow@32400  223 lemma atLeastatMost_empty_iff[simp]:  nipkow@32400  224  "{a..b} = {} \ (~ a <= b)"  nipkow@32400  225 by auto (blast intro: order_trans)  nipkow@32400  226 nipkow@32400  227 lemma atLeastatMost_empty_iff2[simp]:  nipkow@32400  228  "{} = {a..b} \ (~ a <= b)"  nipkow@32400  229 by auto (blast intro: order_trans)  nipkow@32400  230 nipkow@32400  231 lemma atLeastLessThan_empty[simp]:  nipkow@32400  232  "b <= a \ {a.. (~ a < b)"  nipkow@32400  237 by auto (blast intro: le_less_trans)  nipkow@32400  238 nipkow@32400  239 lemma atLeastLessThan_empty_iff2[simp]:  nipkow@32400  240  "{} = {a.. (~ a < b)"  nipkow@32400  241 by auto (blast intro: le_less_trans)  nipkow@15554  242 nipkow@32400  243 lemma greaterThanAtMost_empty[simp]: "l \ k ==> {k<..l} = {}"  nipkow@17719  244 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)  nipkow@17719  245 nipkow@32400  246 lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ ~ k < l"  nipkow@32400  247 by auto (blast intro: less_le_trans)  nipkow@32400  248 nipkow@32400  249 lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ ~ k < l"  nipkow@32400  250 by auto (blast intro: less_le_trans)  nipkow@32400  251 haftmann@29709  252 lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. {a .. b} = {a}" by simp  hoelzl@36846  259 nipkow@32400  260 lemma atLeastatMost_subset_iff[simp]:  nipkow@32400  261  "{a..b} <= {c..d} \ (~ a <= b) | c <= a & b <= d"  nipkow@32400  262 unfolding atLeastAtMost_def atLeast_def atMost_def  nipkow@32400  263 by (blast intro: order_trans)  nipkow@32400  264 nipkow@32400  265 lemma atLeastatMost_psubset_iff:  nipkow@32400  266  "{a..b} < {c..d} \  nipkow@32400  267  ((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d"  nipkow@39302  268 by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)  nipkow@32400  269 nipkow@51334  270 lemma Icc_eq_Icc[simp]:  nipkow@51334  271  "{l..h} = {l'..h'} = (l=l' \ h=h' \ \ l\h \ \ l'\h')"  nipkow@51334  272 by(simp add: order_class.eq_iff)(auto intro: order_trans)  nipkow@51334  273 hoelzl@36846  274 lemma atLeastAtMost_singleton_iff[simp]:  hoelzl@36846  275  "{a .. b} = {c} \ a = b \ b = c"  hoelzl@36846  276 proof  hoelzl@36846  277  assume "{a..b} = {c}"  wenzelm@53374  278  hence *: "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp  wenzelm@53374  279  with {a..b} = {c} have "c \ a \ b \ c" by auto  wenzelm@53374  280  with * show "a = b \ b = c" by auto  hoelzl@36846  281 qed simp  hoelzl@36846  282 nipkow@51334  283 lemma Icc_subset_Ici_iff[simp]:  nipkow@51334  284  "{l..h} \ {l'..} = (~ l\h \ l\l')"  nipkow@51334  285 by(auto simp: subset_eq intro: order_trans)  nipkow@51334  286 nipkow@51334  287 lemma Icc_subset_Iic_iff[simp]:  nipkow@51334  288  "{l..h} \ {..h'} = (~ l\h \ h\h')"  nipkow@51334  289 by(auto simp: subset_eq intro: order_trans)  nipkow@51334  290 nipkow@51334  291 lemma not_Ici_eq_empty[simp]: "{l..} \ {}"  nipkow@51334  292 by(auto simp: set_eq_iff)  nipkow@51334  293 nipkow@51334  294 lemma not_Iic_eq_empty[simp]: "{..h} \ {}"  nipkow@51334  295 by(auto simp: set_eq_iff)  nipkow@51334  296 nipkow@51334  297 lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric]  nipkow@51334  298 lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric]  nipkow@51334  299 nipkow@24691  300 end  paulson@14485  301 nipkow@51334  302 context no_top  nipkow@51334  303 begin  nipkow@51334  304 nipkow@51334  305 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  306 lemma not_UNIV_le_Icc[simp]: "\ UNIV \ {l..h}"  nipkow@51334  307 using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  308 nipkow@51334  309 lemma not_UNIV_le_Iic[simp]: "\ UNIV \ {..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_Ici_le_Icc[simp]: "\ {l..} \ {l'..h'}"  nipkow@51334  313 using gt_ex[of h']  nipkow@51334  314 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  315 nipkow@51334  316 lemma not_Ici_le_Iic[simp]: "\ {l..} \ {..h'}"  nipkow@51334  317 using gt_ex[of h']  nipkow@51334  318 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  319 nipkow@51334  320 end  nipkow@51334  321 nipkow@51334  322 context no_bot  nipkow@51334  323 begin  nipkow@51334  324 nipkow@51334  325 lemma not_UNIV_le_Ici[simp]: "\ UNIV \ {l..}"  nipkow@51334  326 using lt_ex[of l] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  327 nipkow@51334  328 lemma not_Iic_le_Icc[simp]: "\ {..h} \ {l'..h'}"  nipkow@51334  329 using lt_ex[of l']  nipkow@51334  330 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  331 nipkow@51334  332 lemma not_Iic_le_Ici[simp]: "\ {..h} \ {l'..}"  nipkow@51334  333 using lt_ex[of l']  nipkow@51334  334 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  335 nipkow@51334  336 end  nipkow@51334  337 nipkow@51334  338 nipkow@51334  339 context no_top  nipkow@51334  340 begin  nipkow@51334  341 nipkow@51334  342 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  343 lemma not_UNIV_eq_Icc[simp]: "\ UNIV = {l'..h'}"  nipkow@51334  344 using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  345 nipkow@51334  346 lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric]  nipkow@51334  347 nipkow@51334  348 lemma not_UNIV_eq_Iic[simp]: "\ UNIV = {..h'}"  nipkow@51334  349 using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  350 nipkow@51334  351 lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric]  nipkow@51334  352 nipkow@51334  353 lemma not_Icc_eq_Ici[simp]: "\ {l..h} = {l'..}"  nipkow@51334  354 unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast  nipkow@51334  355 nipkow@51334  356 lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric]  nipkow@51334  357 nipkow@51334  358 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  359 lemma not_Iic_eq_Ici[simp]: "\ {..h} = {l'..}"  nipkow@51334  360 using not_Ici_le_Iic[of l' h] by blast  nipkow@51334  361 nipkow@51334  362 lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric]  nipkow@51334  363 nipkow@51334  364 end  nipkow@51334  365 nipkow@51334  366 context no_bot  nipkow@51334  367 begin  nipkow@51334  368 nipkow@51334  369 lemma not_UNIV_eq_Ici[simp]: "\ UNIV = {l'..}"  nipkow@51334  370 using lt_ex[of l'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  371 nipkow@51334  372 lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric]  nipkow@51334  373 nipkow@51334  374 lemma not_Icc_eq_Iic[simp]: "\ {l..h} = {..h'}"  nipkow@51334  375 unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast  nipkow@51334  376 nipkow@51334  377 lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric]  nipkow@51334  378 nipkow@51334  379 end  nipkow@51334  380 nipkow@51334  381 hoelzl@53216  382 context dense_linorder  hoelzl@42891  383 begin  hoelzl@42891  384 hoelzl@42891  385 lemma greaterThanLessThan_empty_iff[simp]:  hoelzl@42891  386  "{ a <..< b } = {} \ b \ a"  hoelzl@42891  387  using dense[of a b] by (cases "a < b") auto  hoelzl@42891  388 hoelzl@42891  389 lemma greaterThanLessThan_empty_iff2[simp]:  hoelzl@42891  390  "{} = { a <..< b } \ b \ a"  hoelzl@42891  391  using dense[of a b] by (cases "a < b") auto  hoelzl@42891  392 hoelzl@42901  393 lemma atLeastLessThan_subseteq_atLeastAtMost_iff:  hoelzl@42901  394  "{a ..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  395  using dense[of "max a d" "b"]  hoelzl@42901  396  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  397 hoelzl@42901  398 lemma greaterThanAtMost_subseteq_atLeastAtMost_iff:  hoelzl@42901  399  "{a <.. b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  400  using dense[of "a" "min c b"]  hoelzl@42901  401  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  402 hoelzl@42901  403 lemma greaterThanLessThan_subseteq_atLeastAtMost_iff:  hoelzl@42901  404  "{a <..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  405  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@42901  406  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  407 hoelzl@43657  408 lemma atLeastAtMost_subseteq_atLeastLessThan_iff:  hoelzl@43657  409  "{a .. b} \ { c ..< d } \ (a \ b \ c \ a \ b < d)"  hoelzl@43657  410  using dense[of "max a d" "b"]  hoelzl@43657  411  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  412 hoelzl@43657  413 lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:  hoelzl@43657  414  "{a <.. b} \ { c ..< d } \ (a < b \ c \ a \ b < d)"  hoelzl@43657  415  using dense[of "a" "min c b"]  hoelzl@43657  416  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  417 hoelzl@43657  418 lemma greaterThanLessThan_subseteq_atLeastLessThan_iff:  hoelzl@43657  419  "{a <..< b} \ { c ..< d } \ (a < b \ c \ a \ b \ d)"  hoelzl@43657  420  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@43657  421  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  422 hoelzl@56328  423 lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff:  hoelzl@56328  424  "{a <..< b} \ { c <.. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@56328  425  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@56328  426  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@56328  427 hoelzl@42891  428 end  hoelzl@42891  429 hoelzl@51329  430 context no_top  hoelzl@51329  431 begin  hoelzl@51329  432 nipkow@51334  433 lemma greaterThan_non_empty[simp]: "{x <..} \ {}"  hoelzl@51329  434  using gt_ex[of x] by auto  hoelzl@51329  435 hoelzl@51329  436 end  hoelzl@51329  437 hoelzl@51329  438 context no_bot  hoelzl@51329  439 begin  hoelzl@51329  440 nipkow@51334  441 lemma lessThan_non_empty[simp]: "{..< x} \ {}"  hoelzl@51329  442  using lt_ex[of x] by auto  hoelzl@51329  443 hoelzl@51329  444 end  hoelzl@51329  445 nipkow@32408  446 lemma (in linorder) atLeastLessThan_subset_iff:  nipkow@32408  447  "{a.. b <= a | c<=a & b<=d"  nipkow@32408  448 apply (auto simp:subset_eq Ball_def)  nipkow@32408  449 apply(frule_tac x=a in spec)  nipkow@32408  450 apply(erule_tac x=d in allE)  nipkow@32408  451 apply (simp add: less_imp_le)  nipkow@32408  452 done  nipkow@32408  453 hoelzl@40703  454 lemma atLeastLessThan_inj:  hoelzl@40703  455  fixes a b c d :: "'a::linorder"  hoelzl@40703  456  assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"  hoelzl@40703  457  shows "a = c" "b = d"  hoelzl@40703  458 using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+  hoelzl@40703  459 hoelzl@40703  460 lemma atLeastLessThan_eq_iff:  hoelzl@40703  461  fixes a b c d :: "'a::linorder"  hoelzl@40703  462  assumes "a < b" "c < d"  hoelzl@40703  463  shows "{a ..< b} = {c ..< d} \ a = c \ b = d"  hoelzl@40703  464  using atLeastLessThan_inj assms by auto  hoelzl@40703  465 hoelzl@57447  466 lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \ (b \ a \ d \ c) \ a = c \ b = d"  hoelzl@57447  467  by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le)  hoelzl@57447  468 hoelzl@57447  469 lemma (in order) Iio_Int_singleton: "{.. {x} = (if x < k then {x} else {})"  hoelzl@57447  470  by auto  hoelzl@57447  471 hoelzl@57447  472 lemma (in linorder) Ioc_subset_iff: "{a<..b} \ {c<..d} \ (b \ a \ c \ a \ b \ d)"  hoelzl@57447  473  by (auto simp: subset_eq Ball_def) (metis less_le not_less)  hoelzl@57447  474 haftmann@52729  475 lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \ x = bot"  nipkow@51334  476 by (auto simp: set_eq_iff intro: le_bot)  hoelzl@51328  477 haftmann@52729  478 lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \ x = top"  nipkow@51334  479 by (auto simp: set_eq_iff intro: top_le)  hoelzl@51328  480 nipkow@51334  481 lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff:  nipkow@51334  482  "{x..y} = UNIV \ (x = bot \ y = top)"  nipkow@51334  483 by (auto simp: set_eq_iff intro: top_le le_bot)  hoelzl@51328  484 hoelzl@56949  485 lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \ n = bot"  hoelzl@56949  486  by (auto simp: set_eq_iff not_less le_bot)  hoelzl@56949  487 hoelzl@56949  488 lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \ n = 0"  hoelzl@56949  489  by (simp add: Iio_eq_empty_iff bot_nat_def)  hoelzl@56949  490 noschinl@58970  491 lemma mono_image_least:  noschinl@58970  492  assumes f_mono: "mono f" and f_img: "f  {m ..< n} = {m' ..< n'}" "m < n"  noschinl@58970  493  shows "f m = m'"  noschinl@58970  494 proof -  noschinl@58970  495  from f_img have "{m' ..< n'} \ {}"  noschinl@58970  496  by (metis atLeastLessThan_empty_iff image_is_empty)  noschinl@58970  497  with f_img have "m' \ f  {m ..< n}" by auto  noschinl@58970  498  then obtain k where "f k = m'" "m \ k" by auto  noschinl@58970  499  moreover have "m' \ f m" using f_img by auto  noschinl@58970  500  ultimately show "f m = m'"  noschinl@58970  501  using f_mono by (auto elim: monoE[where x=m and y=k])  noschinl@58970  502 qed  noschinl@58970  503 hoelzl@51328  504 hoelzl@56328  505 subsection {* Infinite intervals *}  hoelzl@56328  506 hoelzl@56328  507 context dense_linorder  hoelzl@56328  508 begin  hoelzl@56328  509 hoelzl@56328  510 lemma infinite_Ioo:  hoelzl@56328  511  assumes "a < b"  hoelzl@56328  512  shows "\ finite {a<.. {}"  hoelzl@56328  516  using a < b by auto  hoelzl@56328  517  ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b"  hoelzl@56328  518  using Max_in[of "{a <..< b}"] by auto  hoelzl@56328  519  then obtain x where "Max {a <..< b} < x" "x < b"  hoelzl@56328  520  using dense[of "Max {a<.. {a <..< b}"  hoelzl@56328  522  using a < Max {a <..< b} by auto  hoelzl@56328  523  then have "x \ Max {a <..< b}"  hoelzl@56328  524  using fin by auto  hoelzl@56328  525  with Max {a <..< b} < x show False by auto  hoelzl@56328  526 qed  hoelzl@56328  527 hoelzl@56328  528 lemma infinite_Icc: "a < b \ \ finite {a .. b}"  hoelzl@56328  529  using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b]  hoelzl@56328  530  by (auto dest: finite_subset)  hoelzl@56328  531 hoelzl@56328  532 lemma infinite_Ico: "a < b \ \ finite {a ..< b}"  hoelzl@56328  533  using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b]  hoelzl@56328  534  by (auto dest: finite_subset)  hoelzl@56328  535 hoelzl@56328  536 lemma infinite_Ioc: "a < b \ \ finite {a <.. b}"  hoelzl@56328  537  using greaterThanLessThan_subseteq_greaterThanAtMost_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 end  hoelzl@56328  541 hoelzl@56328  542 lemma infinite_Iio: "\ finite {..< a :: 'a :: {no_bot, linorder}}"  hoelzl@56328  543 proof  hoelzl@56328  544  assume "finite {..< a}"  hoelzl@56328  545  then have *: "\x. x < a \ Min {..< a} \ x"  hoelzl@56328  546  by auto  hoelzl@56328  547  obtain x where "x < a"  hoelzl@56328  548  using lt_ex by auto  hoelzl@56328  549 hoelzl@56328  550  obtain y where "y < Min {..< a}"  hoelzl@56328  551  using lt_ex by auto  hoelzl@56328  552  also have "Min {..< a} \ x"  hoelzl@56328  553  using x < a by fact  hoelzl@56328  554  also note x < a  hoelzl@56328  555  finally have "Min {..< a} \ y"  hoelzl@56328  556  by fact  hoelzl@56328  557  with y < Min {..< a} show False by auto  hoelzl@56328  558 qed  hoelzl@56328  559 hoelzl@56328  560 lemma infinite_Iic: "\ finite {.. a :: 'a :: {no_bot, linorder}}"  hoelzl@56328  561  using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"]  hoelzl@56328  562  by (auto simp: subset_eq less_imp_le)  hoelzl@56328  563 hoelzl@56328  564 lemma infinite_Ioi: "\ finite {a :: 'a :: {no_top, linorder} <..}"  hoelzl@56328  565 proof  hoelzl@56328  566  assume "finite {a <..}"  hoelzl@56328  567  then have *: "\x. a < x \ x \ Max {a <..}"  hoelzl@56328  568  by auto  hoelzl@56328  569 hoelzl@56328  570  obtain y where "Max {a <..} < y"  hoelzl@56328  571  using gt_ex by auto  hoelzl@56328  572 hoelzl@56328  573  obtain x where "a < x"  hoelzl@56328  574  using gt_ex by auto  hoelzl@56328  575  also then have "x \ Max {a <..}"  hoelzl@56328  576  by fact  hoelzl@56328  577  also note Max {a <..} < y  hoelzl@56328  578  finally have "y \ Max { a <..}"  hoelzl@56328  579  by fact  hoelzl@56328  580  with Max {a <..} < y show False by auto  hoelzl@56328  581 qed  hoelzl@56328  582 hoelzl@56328  583 lemma infinite_Ici: "\ finite {a :: 'a :: {no_top, linorder} ..}"  hoelzl@56328  584  using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"]  hoelzl@56328  585  by (auto simp: subset_eq less_imp_le)  hoelzl@56328  586 nipkow@32456  587 subsubsection {* Intersection *}  nipkow@32456  588 nipkow@32456  589 context linorder  nipkow@32456  590 begin  nipkow@32456  591 nipkow@32456  592 lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"  nipkow@32456  593 by auto  nipkow@32456  594 nipkow@32456  595 lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"  nipkow@32456  596 by auto  nipkow@32456  597 nipkow@32456  598 lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"  nipkow@32456  599 by auto  nipkow@32456  600 nipkow@32456  601 lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"  nipkow@32456  602 by auto  nipkow@32456  603 nipkow@32456  604 lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"  nipkow@32456  605 by auto  nipkow@32456  606 nipkow@32456  607 lemma Int_atLeastLessThan[simp]: "{a.. {..b} = {.. min a b}"  hoelzl@50417  617  by (auto simp: min_def)  hoelzl@50417  618 hoelzl@57447  619 lemma Ioc_disjoint: "{a<..b} \ {c<..d} = {} \ b \ a \ d \ c \ b \ c \ d \ a"  hoelzl@57447  620  using assms by auto  hoelzl@57447  621 nipkow@32456  622 end  nipkow@32456  623 hoelzl@51329  624 context complete_lattice  hoelzl@51329  625 begin  hoelzl@51329  626 hoelzl@51329  627 lemma  hoelzl@51329  628  shows Sup_atLeast[simp]: "Sup {x ..} = top"  hoelzl@51329  629  and Sup_greaterThanAtLeast[simp]: "x < top \ Sup {x <..} = top"  hoelzl@51329  630  and Sup_atMost[simp]: "Sup {.. y} = y"  hoelzl@51329  631  and Sup_atLeastAtMost[simp]: "x \ y \ Sup { x .. y} = y"  hoelzl@51329  632  and Sup_greaterThanAtMost[simp]: "x < y \ Sup { x <.. y} = y"  hoelzl@51329  633  by (auto intro!: Sup_eqI)  hoelzl@51329  634 hoelzl@51329  635 lemma  hoelzl@51329  636  shows Inf_atMost[simp]: "Inf {.. x} = bot"  hoelzl@51329  637  and Inf_atMostLessThan[simp]: "top < x \ Inf {..< x} = bot"  hoelzl@51329  638  and Inf_atLeast[simp]: "Inf {x ..} = x"  hoelzl@51329  639  and Inf_atLeastAtMost[simp]: "x \ y \ Inf { x .. y} = x"  hoelzl@51329  640  and Inf_atLeastLessThan[simp]: "x < y \ Inf { x ..< y} = x"  hoelzl@51329  641  by (auto intro!: Inf_eqI)  hoelzl@51329  642 hoelzl@51329  643 end  hoelzl@51329  644 hoelzl@51329  645 lemma  hoelzl@53216  646  fixes x y :: "'a :: {complete_lattice, dense_linorder}"  hoelzl@51329  647  shows Sup_lessThan[simp]: "Sup {..< y} = y"  hoelzl@51329  648  and Sup_atLeastLessThan[simp]: "x < y \ Sup { x ..< y} = y"  hoelzl@51329  649  and Sup_greaterThanLessThan[simp]: "x < y \ Sup { x <..< y} = y"  hoelzl@51329  650  and Inf_greaterThan[simp]: "Inf {x <..} = x"  hoelzl@51329  651  and Inf_greaterThanAtMost[simp]: "x < y \ Inf { x <.. y} = x"  hoelzl@51329  652  and Inf_greaterThanLessThan[simp]: "x < y \ Inf { x <..< y} = x"  hoelzl@51329  653  by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded)  nipkow@32456  654 paulson@14485  655 subsection {* Intervals of natural numbers *}  paulson@14485  656 paulson@15047  657 subsubsection {* The Constant @{term lessThan} *}  paulson@15047  658 paulson@14485  659 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"  paulson@14485  660 by (simp add: lessThan_def)  paulson@14485  661 paulson@14485  662 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"  paulson@14485  663 by (simp add: lessThan_def less_Suc_eq, blast)  paulson@14485  664 kleing@43156  665 text {* The following proof is convenient in induction proofs where  hoelzl@39072  666 new elements get indices at the beginning. So it is used to transform  hoelzl@39072  667 @{term "{.. Suc  A"  hoelzl@59000  670  by auto  hoelzl@59000  671 hoelzl@39072  672 lemma lessThan_Suc_eq_insert_0: "{.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  778 by (auto simp add: atLeastAtMost_def)  nipkow@15554  779 noschinl@45932  780 lemma atLeastAtMost_insertL: "m \ n \ insert m {Suc m..n} = {m ..n}"  noschinl@45932  781 by auto  noschinl@45932  782 kleing@43157  783 text {* The analogous result is useful on @{typ int}: *}  kleing@43157  784 (* here, because we don't have an own int section *)  kleing@43157  785 lemma atLeastAtMostPlus1_int_conv:  kleing@43157  786  "m <= 1+n \ {m..1+n} = insert (1+n) {m..n::int}"  kleing@43157  787  by (auto intro: set_eqI)  kleing@43157  788 paulson@33044  789 lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j.. (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k))  lp15@57113  807  else {})"  lp15@57113  808  by (simp add: numeral_eq_Suc atLeastLessThanSuc)  lp15@57113  809 nipkow@16733  810 subsubsection {* Image *}  nipkow@16733  811 nipkow@16733  812 lemma image_add_atLeastAtMost:  nipkow@16733  813  "(%n::nat. n+k)  {i..j} = {i+k..j+k}" (is "?A = ?B")  nipkow@16733  814 proof  nipkow@16733  815  show "?A \ ?B" by auto  nipkow@16733  816 next  nipkow@16733  817  show "?B \ ?A"  nipkow@16733  818  proof  nipkow@16733  819  fix n assume a: "n : ?B"  webertj@20217  820  hence "n - k : {i..j}" by auto  nipkow@16733  821  moreover have "n = (n - k) + k" using a by auto  nipkow@16733  822  ultimately show "n : ?A" by blast  nipkow@16733  823  qed  nipkow@16733  824 qed  nipkow@16733  825 nipkow@16733  826 lemma image_add_atLeastLessThan:  nipkow@16733  827  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  830 next  nipkow@16733  831  show "?B \ ?A"  nipkow@16733  832  proof  nipkow@16733  833  fix n assume a: "n : ?B"  webertj@20217  834  hence "n - k : {i..i. i - c)  {x ..< y} =  hoelzl@37664  858  (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"  hoelzl@37664  859  (is "_ = ?right")  hoelzl@37664  860 proof safe  hoelzl@37664  861  fix a assume a: "a \ ?right"  hoelzl@37664  862  show "a \ (\i. i - c)  {x ..< y}"  hoelzl@37664  863  proof cases  hoelzl@37664  864  assume "c < y" with a show ?thesis  hoelzl@37664  865  by (auto intro!: image_eqI[of _ _ "a + c"])  hoelzl@37664  866  next  hoelzl@37664  867  assume "\ c < y" with a show ?thesis  hoelzl@37664  868  by (auto intro!: image_eqI[of _ _ x] split: split_if_asm)  hoelzl@37664  869  qed  hoelzl@37664  870 qed auto  hoelzl@37664  871 Andreas@51152  872 lemma image_int_atLeastLessThan: "int  {a.. uminus  {x<..}"  hoelzl@35580  886  by (rule imageI) (simp add: *)  hoelzl@35580  887  thus "y \ uminus  {x<..}" by simp  hoelzl@35580  888 next  hoelzl@35580  889  fix y assume "y \ -x"  hoelzl@35580  890  have "- (-y) \ uminus  {x..}"  hoelzl@35580  891  by (rule imageI) (insert y \ -x[THEN le_imp_neg_le], simp)  hoelzl@35580  892  thus "y \ uminus  {x..}" by simp  hoelzl@35580  893 qed simp_all  hoelzl@35580  894 hoelzl@35580  895 lemma  hoelzl@35580  896  fixes x :: 'a  hoelzl@35580  897  shows image_uminus_lessThan[simp]: "uminus  {.. finite N"  nipkow@28068  944 apply (rule finite_subset)  nipkow@28068  945  apply (rule_tac [2] finite_lessThan, auto)  nipkow@28068  946 done  nipkow@28068  947 nipkow@31044  948 text {* A set of natural numbers is finite iff it is bounded. *}  nipkow@31044  949 lemma finite_nat_set_iff_bounded:  nipkow@31044  950  "finite(N::nat set) = (EX m. ALL n:N. nnat. (!!n. n \ f n) ==> finite {n. f n \ u}"  nipkow@28068  966 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)  paulson@14485  967 hoelzl@56328  968 nipkow@24853  969 text{* Any subset of an interval of natural numbers the size of the  nipkow@24853  970 subset is exactly that interval. *}  nipkow@24853  971 nipkow@24853  972 lemma subset_card_intvl_is_intvl:  blanchet@55085  973  assumes "A \ {k.. A" by auto  blanchet@55085  983  with insert have "A <= {k..i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B")  nipkow@36755  997 proof  nipkow@36755  998  show "?A <= ?B"  nipkow@36755  999  proof  nipkow@36755  1000  fix x assume "x : ?A"  nipkow@36755  1001  then obtain i where i: "i\n" "x : M i" by auto  nipkow@36755  1002  show "x : ?B"  nipkow@36755  1003  proof(cases i)  nipkow@36755  1004  case 0 with i show ?thesis by simp  nipkow@36755  1005  next  nipkow@36755  1006  case (Suc j) with i show ?thesis by auto  nipkow@36755  1007  qed  nipkow@36755  1008  qed  nipkow@36755  1009 next  nipkow@36755  1010  show "?B <= ?A" by auto  nipkow@36755  1011 qed  nipkow@36755  1012 nipkow@36755  1013 lemma UN_le_add_shift:  nipkow@36755  1014  "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B")  nipkow@36755  1015 proof  nipkow@44890  1016  show "?A <= ?B" by fastforce  nipkow@36755  1017 next  nipkow@36755  1018  show "?B <= ?A"  nipkow@36755  1019  proof  nipkow@36755  1020  fix x assume "x : ?B"  nipkow@36755  1021  then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto  nipkow@36755  1022  hence "i-k\n & x : M((i-k)+k)" by auto  nipkow@36755  1023  thus "x : ?A" by blast  nipkow@36755  1024  qed  nipkow@36755  1025 qed  nipkow@36755  1026 paulson@32596  1027 lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)"  paulson@32596  1028  by (auto simp add: atLeast0LessThan)  paulson@32596  1029 paulson@32596  1030 lemma UN_finite_subset: "(!!n::nat. (\i\{0.. C) \ (\n. A n) \ C"  paulson@32596  1031  by (subst UN_UN_finite_eq [symmetric]) blast  paulson@32596  1032 paulson@33044  1033 lemma UN_finite2_subset:  paulson@33044  1034  "(!!n::nat. (\i\{0.. (\i\{0.. (\n. A n) \ (\n. B n)"  paulson@33044  1035  apply (rule UN_finite_subset)  paulson@33044  1036  apply (subst UN_UN_finite_eq [symmetric, of B])  paulson@33044  1037  apply blast  paulson@33044  1038  done  paulson@32596  1039 paulson@32596  1040 lemma UN_finite2_eq:  paulson@33044  1041  "(!!n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)"  paulson@33044  1042  apply (rule subset_antisym)  paulson@33044  1043  apply (rule UN_finite2_subset, blast)  paulson@33044  1044  apply (rule UN_finite2_subset [where k=k])  huffman@35216  1045  apply (force simp add: atLeastLessThan_add_Un [of 0])  paulson@33044  1046  done  paulson@32596  1047 paulson@32596  1048 paulson@14485  1049 subsubsection {* Cardinality *}  paulson@14485  1050 nipkow@15045  1051 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  1091 apply(drule ex_bij_betw_finite_nat)  nipkow@31438  1092 apply(drule ex_bij_betw_nat_finite)  nipkow@31438  1093 apply(auto intro!:bij_betw_trans)  nipkow@31438  1094 done  nipkow@31438  1095 nipkow@31438  1096 lemma ex_bij_betw_nat_finite_1:  nipkow@31438  1097  "finite M \ \h. bij_betw h {1 .. card M} M"  nipkow@31438  1098 by (rule finite_same_card_bij) auto  nipkow@31438  1099 hoelzl@40703  1100 lemma bij_betw_iff_card:  hoelzl@40703  1101  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  1102  shows BIJ: "(\f. bij_betw f A B) \ (card A = card B)"  hoelzl@40703  1103 using assms  hoelzl@40703  1104 proof(auto simp add: bij_betw_same_card)  hoelzl@40703  1105  assume *: "card A = card B"  hoelzl@40703  1106  obtain f where "bij_betw f A {0 ..< card A}"  hoelzl@40703  1107  using FIN ex_bij_betw_finite_nat by blast  hoelzl@40703  1108  moreover obtain g where "bij_betw g {0 ..< card B} B"  hoelzl@40703  1109  using FIN' ex_bij_betw_nat_finite by blast  hoelzl@40703  1110  ultimately have "bij_betw (g o f) A B"  hoelzl@40703  1111  using * by (auto simp add: bij_betw_trans)  hoelzl@40703  1112  thus "(\f. bij_betw f A B)" by blast  hoelzl@40703  1113 qed  hoelzl@40703  1114 hoelzl@40703  1115 lemma inj_on_iff_card_le:  hoelzl@40703  1116  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  1117  shows "(\f. inj_on f A \ f  A \ B) = (card A \ card B)"  hoelzl@40703  1118 proof (safe intro!: card_inj_on_le)  hoelzl@40703  1119  assume *: "card A \ card B"  hoelzl@40703  1120  obtain f where 1: "inj_on f A" and 2: "f  A = {0 ..< card A}"  hoelzl@40703  1121  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force  hoelzl@40703  1122  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g  {0 ..< card B} = B"  hoelzl@40703  1123  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force  hoelzl@40703  1124  ultimately have "inj_on g (f  A)" using subset_inj_on[of g _ "f  A"] * by force  hoelzl@40703  1125  hence "inj_on (g o f) A" using 1 comp_inj_on by blast  hoelzl@40703  1126  moreover  hoelzl@40703  1127  {have "{0 ..< card A} \ {0 ..< card B}" using * by force  hoelzl@40703  1128  with 2 have "f  A \ {0 ..< card B}" by blast  hoelzl@40703  1129  hence "(g o f)  A \ B" unfolding comp_def using 3 by force  hoelzl@40703  1130  }  hoelzl@40703  1131  ultimately show "(\f. inj_on f A \ f  A \ B)" by blast  hoelzl@40703  1132 qed (insert assms, auto)  nipkow@26105  1133 paulson@14485  1134 subsection {* Intervals of integers *}  paulson@14485  1135 nipkow@15045  1136 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l.. u ==>  nipkow@15045  1149  {(0::int).. u")  paulson@14485  1158  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1159  apply (rule finite_imageI)  paulson@14485  1160  apply auto  paulson@14485  1161  done  paulson@14485  1162 nipkow@15045  1163 lemma finite_atLeastLessThan_int [iff]: "finite {l.. u")  paulson@14485  1185  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1186  apply (subst card_image)  paulson@14485  1187  apply (auto simp add: inj_on_def)  paulson@14485  1188  done  paulson@14485  1189 nipkow@15045  1190 lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}"  bulwahn@27656  1212 proof -  bulwahn@27656  1213  have "{k. P k \ k < i} \ {.. M"  bulwahn@27656  1219 shows "card {k \ M. k < Suc i} \ 0"  bulwahn@27656  1220 proof -  bulwahn@27656  1221  from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto  bulwahn@27656  1222  with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)  bulwahn@27656  1223 qed  bulwahn@27656  1224 bulwahn@27656  1225 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"  haftmann@37388  1226 apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"])  bulwahn@27656  1227 apply auto  bulwahn@27656  1228 apply (rule inj_on_diff_nat)  bulwahn@27656  1229 apply auto  bulwahn@27656  1230 apply (case_tac x)  bulwahn@27656  1231 apply auto  bulwahn@27656  1232 apply (case_tac xa)  bulwahn@27656  1233 apply auto  bulwahn@27656  1234 apply (case_tac xa)  bulwahn@27656  1235 apply auto  bulwahn@27656  1236 done  bulwahn@27656  1237 bulwahn@27656  1238 lemma card_less_Suc:  bulwahn@27656  1239  assumes zero_in_M: "0 \ M"  bulwahn@27656  1240  shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"  bulwahn@27656  1241 proof -  bulwahn@27656  1242  from assms have a: "0 \ {k \ M. k < Suc i}" by simp  bulwahn@27656  1243  hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})"  bulwahn@27656  1244  by (auto simp only: insert_Diff)  bulwahn@27656  1245  have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto  lp15@57113  1246  from finite_M_bounded_by_nat[of "\x. x \ M" "Suc i"]  lp15@57113  1247  have "Suc (card {k. Suc k \ M \ k < i}) = card (insert 0 ({k \ M. k < Suc i} - {0}))"  bulwahn@27656  1248  apply (subst card_insert)  bulwahn@27656  1249  apply simp_all  bulwahn@27656  1250  apply (subst b)  bulwahn@27656  1251  apply (subst card_less_Suc2[symmetric])  bulwahn@27656  1252  apply simp_all  bulwahn@27656  1253  done  bulwahn@27656  1254  with c show ?thesis by simp  bulwahn@27656  1255 qed  bulwahn@27656  1256 paulson@14485  1257 paulson@13850  1258 subsection {*Lemmas useful with the summation operator setsum*}  paulson@13850  1259 ballarin@16102  1260 text {* For examples, see Algebra/poly/UnivPoly2.thy *}  ballarin@13735  1261 wenzelm@14577  1262 subsubsection {* Disjoint Unions *}  ballarin@13735  1263 wenzelm@14577  1264 text {* Singletons and open intervals *}  ballarin@13735  1265 ballarin@13735  1266 lemma ivl_disj_un_singleton:  nipkow@15045  1267  "{l::'a::linorder} Un {l<..} = {l..}"  nipkow@15045  1268  "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  1272  "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  1281  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  1283  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  1285  "(l::'a::linorder) <= u ==> {l.. {l<.. {l<..m} Un {m<.. {l.. {l..m} Un {m<.. {l<.. {l<..m} Un {m<..u} = {l<..u}"  nipkow@15045  1297  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  1299 by auto  ballarin@13735  1300 ballarin@13735  1301 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two  ballarin@13735  1302 wenzelm@14577  1303 subsubsection {* Disjoint Intersections *}  ballarin@13735  1304 wenzelm@14577  1305 text {* One- and two-sided intervals *}  ballarin@13735  1306 ballarin@13735  1307 lemma ivl_disj_int_one:  nipkow@15045  1308  "{..l::'a::order} Int {l<.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  1348 apply(auto simp:linorder_not_le)  nipkow@15542  1349 apply(rule ccontr)  nipkow@15542  1350 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  1351 apply(clarsimp simp:linorder_not_le)  nipkow@44890  1352 apply(fastforce)  nipkow@15542  1353 done  nipkow@15542  1354 nipkow@15041  1355 nipkow@15042  1356 subsection {* Summation indexed over intervals *}  nipkow@15042  1357 nipkow@15042  1358 syntax  nipkow@15042  1359  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  1360  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  1361  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@16052  1362  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  nipkow@15042  1363 syntax (xsymbols)  nipkow@15042  1364  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  1365  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  1366  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  1367  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15042  1368 syntax (HTML output)  nipkow@15042  1369  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  1370  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  1371  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  1372  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15056  1373 syntax (latex_sum output)  nipkow@15052  1374  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  1375  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@15052  1376  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  1377  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@16052  1378  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1379  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15052  1380  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1381  ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15041  1382 nipkow@15048  1383 translations  nipkow@28853  1384  "\x=a..b. t" == "CONST setsum (%x. t) {a..b}"  nipkow@28853  1385  "\x=a..i\n. t" == "CONST setsum (\i. t) {..n}"  nipkow@28853  1387  "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  1395 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  1397 @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \  nipkow@15542  1420  setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)"  haftmann@57514  1427 by (simp add:atMost_Suc ac_simps)  nipkow@16052  1428 nipkow@16041  1429 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n"  haftmann@57514  1430 by (simp add:lessThan_Suc ac_simps)  nipkow@15041  1431 nipkow@15911  1432 lemma setsum_cl_ivl_Suc[simp]:  nipkow@15561  1433  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  haftmann@57514  1434 by (auto simp:ac_simps atLeastAtMostSuc_conv)  nipkow@15561  1435 nipkow@15911  1436 lemma setsum_op_ivl_Suc[simp]:  nipkow@15561  1437  "setsum f {m..  nipkow@15561  1441  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  haftmann@57514  1442 by (auto simp:ac_simps atLeastAtMostSuc_conv)  nipkow@16041  1443 *)  nipkow@28068  1444 nipkow@28068  1445 lemma setsum_head:  nipkow@28068  1446  fixes n :: nat  nipkow@28068  1447  assumes mn: "m <= n"  nipkow@28068  1448  shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  nipkow@28068  1449 proof -  nipkow@28068  1450  from mn  nipkow@28068  1451  have "{m..n} = {m} \ {m<..n}"  nipkow@28068  1452  by (auto intro: ivl_disj_un_singleton)  nipkow@28068  1453  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  nipkow@28068  1454  by (simp add: atLeast0LessThan)  nipkow@28068  1455  also have "\ = ?rhs" by simp  nipkow@28068  1456  finally show ?thesis .  nipkow@28068  1457 qed  nipkow@28068  1458 nipkow@28068  1459 lemma setsum_head_Suc:  nipkow@28068  1460  "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}"  nipkow@28068  1461 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)  nipkow@28068  1462 nipkow@28068  1463 lemma setsum_head_upt_Suc:  nipkow@28068  1464  "m < n \ setsum f {m.. n + 1"  nipkow@31501  1470  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"  nipkow@31501  1471 proof-  nipkow@31501  1472  have "{m .. n+p} = {m..n} \ {n+1..n+p}" using m \ n+1 by auto  haftmann@57418  1473  thus ?thesis by (auto simp: ivl_disj_int setsum.union_disjoint  nipkow@31501  1474  atLeastSucAtMost_greaterThanAtMost)  nipkow@31501  1475 qed  nipkow@28068  1476 nipkow@15539  1477 lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \  nipkow@15539  1478  setsum f {m.. 'a::ab_group_add"  nipkow@15539  1483 shows "\ m \ n; n \ p \ \  nipkow@15539  1484  setsum f {m.. ('a::ab_group_add)"  nipkow@31505  1491  shows "setsum (\k. f k - f(k + 1)) {(m::nat) .. n} =  nipkow@31505  1492  (if m <= n then f m - f(n + 1) else 0)"  nipkow@31505  1493 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)  nipkow@31505  1494 hoelzl@56194  1495 lemma setsum_nat_group: "(\m setsum f {Suc 0..k} = setsum f {0..k}"  nipkow@28068  1521 by(simp add:setsum_head_Suc)  kleing@19106  1522 nipkow@28068  1523 lemma setsum_shift_lb_Suc0_0_upt:  nipkow@28068  1524  "f(0::nat) = 0 \ setsum f {Suc 0.. 'a::comm_monoid_add"  haftmann@52380  1531  shows "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))"  haftmann@52380  1532 proof (induct n)  haftmann@52380  1533  case 0 show ?case by simp  haftmann@52380  1534 next  haftmann@52380  1535  case (Suc n) note IH = this  haftmann@52380  1536  have "(\i\Suc (Suc n). f i) = (\i\Suc n. f i) + f (Suc (Suc n))"  haftmann@52380  1537  by (rule setsum_atMost_Suc)  haftmann@52380  1538  also have "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))"  haftmann@52380  1539  by (rule IH)  haftmann@52380  1540  also have "f 0 + (\i\n. f (Suc i)) + f (Suc (Suc n)) =  haftmann@52380  1541  f 0 + ((\i\n. f (Suc i)) + f (Suc (Suc n)))"  haftmann@57512  1542  by (rule add.assoc)  haftmann@52380  1543  also have "(\i\n. f (Suc i)) + f (Suc (Suc n)) = (\i\Suc n. f (Suc i))"  haftmann@52380  1544  by (rule setsum_atMost_Suc [symmetric])  haftmann@52380  1545  finally show ?case .  haftmann@52380  1546 qed  haftmann@52380  1547 lp15@56238  1548 lemma setsum_last_plus: fixes n::nat shows "m <= n \ (\i = m..n. f i) = f n + (\i = m.. 'a::ab_group_add"  lp15@56238  1553  assumes "m \ Suc n"  lp15@56238  1554  shows "(\i = m..n. f(Suc i) - f i) = f (Suc n) - f m"  lp15@56238  1555 using assms by (induct n) (auto simp: le_Suc_eq)  lp15@55718  1556 lp15@55718  1557 lemma nested_setsum_swap:  lp15@55718  1558  "(\i = 0..n. (\j = 0..j = 0..i = Suc j..n. a i j)"  haftmann@57418  1559  by (induction n) (auto simp: setsum.distrib)  lp15@55718  1560 lp15@56215  1561 lemma nested_setsum_swap':  lp15@56215  1562  "(\i\n. (\jji = Suc j..n. a i j)"  haftmann@57418  1563  by (induction n) (auto simp: setsum.distrib)  lp15@56215  1564 lp15@56238  1565 lemma setsum_zero_power' [simp]:  lp15@56238  1566  fixes c :: "nat \ 'a::field"  lp15@56238  1567  shows "(\i\A. c i * 0^i / d i) = (if finite A \ 0 \ A then c 0 / d 0 else 0)"  lp15@56238  1568  using setsum_zero_power [of "\i. c i / d i" A]  lp15@56238  1569  by auto  lp15@56238  1570 haftmann@52380  1571 ballarin@17149  1572 subsection {* The formula for geometric sums *}  ballarin@17149  1573 ballarin@17149  1574 lemma geometric_sum:  haftmann@36307  1575  assumes "x \ 1"  hoelzl@56193  1576  shows "(\i 0" by simp_all  hoelzl@56193  1579  moreover have "(\i 0)  haftmann@36307  1581  ultimately show ?thesis by simp  haftmann@36307  1582 qed  haftmann@36307  1583 ballarin@17149  1584 kleing@19469  1585 subsection {* The formula for arithmetic sums *}  kleing@19469  1586 huffman@47222  1587 lemma gauss_sum:  hoelzl@56193  1588  "(2::'a::comm_semiring_1)*(\i\{1..n}. of_nat i) = of_nat n*((of_nat n)+1)"  kleing@19469  1589 proof (induct n)  kleing@19469  1590  case 0  kleing@19469  1591  show ?case by simp  kleing@19469  1592 next  kleing@19469  1593  case (Suc n)  huffman@47222  1594  then show ?case  huffman@47222  1595  by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one)  huffman@47222  1596  (* FIXME: make numeral cancellation simprocs work for semirings *)  kleing@19469  1597 qed  kleing@19469  1598 kleing@19469  1599 theorem arith_series_general:  huffman@47222  1600  "(2::'a::comm_semiring_1) * (\i\{.. 1"  kleing@19469  1604  let ?I = "\i. of_nat i" and ?n = "of_nat n"  kleing@19469  1605  have  kleing@19469  1606  "(\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  1619  by (simp only: mult.assoc gauss_sum [of "n - 1"], unfold One_nat_def)  haftmann@57514  1620  (simp add: mult.commute trans [OF add.commute of_nat_Suc [symmetric]])  huffman@47222  1621  finally show ?thesis  huffman@47222  1622  unfolding mult_2 by (simp add: algebra_simps)  kleing@19469  1623 next  kleing@19469  1624  assume "\(n > 1)"  kleing@19469  1625  hence "n = 1 \ n = 0" by auto  huffman@47222  1626  thus ?thesis by (auto simp: mult_2)  kleing@19469  1627 qed  kleing@19469  1628 kleing@19469  1629 lemma arith_series_nat:  huffman@47222  1630  "(2::nat) * (\i\{..i\{..i\{..x. Q x \ P x \ (\xxxii 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1654  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1655  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10)  paulson@29960  1656  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10)  paulson@29960  1657 syntax (xsymbols)  paulson@29960  1658  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1659  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1660  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1661  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1662 syntax (HTML output)  paulson@29960  1663  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1664  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1665  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1666  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1667 syntax (latex_prod output)  paulson@29960  1668  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1669  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1670  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1671  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1672  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1673  ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1674  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1675  ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1676 paulson@29960  1677 translations  paulson@29960  1678  "\x=a..b. t" == "CONST setprod (%x. t) {a..b}"  paulson@29960  1679  "\x=a..i\n. t" == "CONST setprod (\i. t) {..n}"  paulson@29960  1681  "\ii. t) {..= 0 \ nat_set {x..y}"  haftmann@33318  1697  by (simp add: nat_set_def)  haftmann@33318  1698 haftmann@35644  1699 declare transfer_morphism_nat_int[transfer add  haftmann@33318  1700  return: transfer_nat_int_set_functions  haftmann@33318  1701  transfer_nat_int_set_function_closures  haftmann@33318  1702 ]  haftmann@33318  1703 haftmann@33318  1704 lemma transfer_int_nat_set_functions:  haftmann@33318  1705  "is_nat m \ is_nat n \ {m..n} = int  {nat m..nat n}"  haftmann@33318  1706  by (simp only: is_nat_def transfer_nat_int_set_functions  haftmann@33318  1707  transfer_nat_int_set_function_closures  haftmann@33318  1708  transfer_nat_int_set_return_embed nat_0_le  haftmann@33318  1709  cong: transfer_nat_int_set_cong)  haftmann@33318  1710 haftmann@33318  1711 lemma transfer_int_nat_set_function_closures:  haftmann@33318  1712  "is_nat x \ nat_set {x..y}"  haftmann@33318  1713  by (simp only: transfer_nat_int_set_function_closures is_nat_def)  haftmann@33318  1714 haftmann@35644  1715 declare transfer_morphism_int_nat[transfer add  haftmann@33318  1716  return: transfer_int_nat_set_functions  haftmann@33318  1717  transfer_int_nat_set_function_closures  haftmann@33318  1718 ]  haftmann@33318  1719 lp15@55242  1720 lemma setprod_int_plus_eq: "setprod int {i..i+j} = \{int i..int (i+j)}"  lp15@55242  1721  by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)  lp15@55242  1722 lp15@55242  1723 lemma setprod_int_eq: "setprod int {i..j} = \{int i..int j}"  lp15@55242  1724 proof (cases "i \ j")  lp15@55242  1725  case True  lp15@55242  1726  then show ?thesis  lp15@55242  1727  by (metis Nat.le_iff_add setprod_int_plus_eq)  lp15@55242  1728 next  lp15@55242  1729  case False  lp15@55242  1730  then show ?thesis  lp15@55242  1731  by auto  lp15@55242  1732 qed  lp15@55242  1733 nipkow@8924  1734 end `