src/HOL/Set_Interval.thy
 author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 57514 bdc2c6b40bf2 child 58889 5b7a9633cfa8 permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
 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@14577  14 header {* 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 hoelzl@51328  491 hoelzl@56328  492 subsection {* Infinite intervals *}  hoelzl@56328  493 hoelzl@56328  494 context dense_linorder  hoelzl@56328  495 begin  hoelzl@56328  496 hoelzl@56328  497 lemma infinite_Ioo:  hoelzl@56328  498  assumes "a < b"  hoelzl@56328  499  shows "\ finite {a<.. {}"  hoelzl@56328  503  using a < b by auto  hoelzl@56328  504  ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b"  hoelzl@56328  505  using Max_in[of "{a <..< b}"] by auto  hoelzl@56328  506  then obtain x where "Max {a <..< b} < x" "x < b"  hoelzl@56328  507  using dense[of "Max {a<.. {a <..< b}"  hoelzl@56328  509  using a < Max {a <..< b} by auto  hoelzl@56328  510  then have "x \ Max {a <..< b}"  hoelzl@56328  511  using fin by auto  hoelzl@56328  512  with Max {a <..< b} < x show False by auto  hoelzl@56328  513 qed  hoelzl@56328  514 hoelzl@56328  515 lemma infinite_Icc: "a < b \ \ finite {a .. b}"  hoelzl@56328  516  using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b]  hoelzl@56328  517  by (auto dest: finite_subset)  hoelzl@56328  518 hoelzl@56328  519 lemma infinite_Ico: "a < b \ \ finite {a ..< b}"  hoelzl@56328  520  using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b]  hoelzl@56328  521  by (auto dest: finite_subset)  hoelzl@56328  522 hoelzl@56328  523 lemma infinite_Ioc: "a < b \ \ finite {a <.. b}"  hoelzl@56328  524  using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b]  hoelzl@56328  525  by (auto dest: finite_subset)  hoelzl@56328  526 hoelzl@56328  527 end  hoelzl@56328  528 hoelzl@56328  529 lemma infinite_Iio: "\ finite {..< a :: 'a :: {no_bot, linorder}}"  hoelzl@56328  530 proof  hoelzl@56328  531  assume "finite {..< a}"  hoelzl@56328  532  then have *: "\x. x < a \ Min {..< a} \ x"  hoelzl@56328  533  by auto  hoelzl@56328  534  obtain x where "x < a"  hoelzl@56328  535  using lt_ex by auto  hoelzl@56328  536 hoelzl@56328  537  obtain y where "y < Min {..< a}"  hoelzl@56328  538  using lt_ex by auto  hoelzl@56328  539  also have "Min {..< a} \ x"  hoelzl@56328  540  using x < a by fact  hoelzl@56328  541  also note x < a  hoelzl@56328  542  finally have "Min {..< a} \ y"  hoelzl@56328  543  by fact  hoelzl@56328  544  with y < Min {..< a} show False by auto  hoelzl@56328  545 qed  hoelzl@56328  546 hoelzl@56328  547 lemma infinite_Iic: "\ finite {.. a :: 'a :: {no_bot, linorder}}"  hoelzl@56328  548  using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"]  hoelzl@56328  549  by (auto simp: subset_eq less_imp_le)  hoelzl@56328  550 hoelzl@56328  551 lemma infinite_Ioi: "\ finite {a :: 'a :: {no_top, linorder} <..}"  hoelzl@56328  552 proof  hoelzl@56328  553  assume "finite {a <..}"  hoelzl@56328  554  then have *: "\x. a < x \ x \ Max {a <..}"  hoelzl@56328  555  by auto  hoelzl@56328  556 hoelzl@56328  557  obtain y where "Max {a <..} < y"  hoelzl@56328  558  using gt_ex by auto  hoelzl@56328  559 hoelzl@56328  560  obtain x where "a < x"  hoelzl@56328  561  using gt_ex by auto  hoelzl@56328  562  also then have "x \ Max {a <..}"  hoelzl@56328  563  by fact  hoelzl@56328  564  also note Max {a <..} < y  hoelzl@56328  565  finally have "y \ Max { a <..}"  hoelzl@56328  566  by fact  hoelzl@56328  567  with Max {a <..} < y show False by auto  hoelzl@56328  568 qed  hoelzl@56328  569 hoelzl@56328  570 lemma infinite_Ici: "\ finite {a :: 'a :: {no_top, linorder} ..}"  hoelzl@56328  571  using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"]  hoelzl@56328  572  by (auto simp: subset_eq less_imp_le)  hoelzl@56328  573 nipkow@32456  574 subsubsection {* Intersection *}  nipkow@32456  575 nipkow@32456  576 context linorder  nipkow@32456  577 begin  nipkow@32456  578 nipkow@32456  579 lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"  nipkow@32456  580 by auto  nipkow@32456  581 nipkow@32456  582 lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"  nipkow@32456  583 by auto  nipkow@32456  584 nipkow@32456  585 lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"  nipkow@32456  586 by auto  nipkow@32456  587 nipkow@32456  588 lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"  nipkow@32456  589 by auto  nipkow@32456  590 nipkow@32456  591 lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"  nipkow@32456  592 by auto  nipkow@32456  593 nipkow@32456  594 lemma Int_atLeastLessThan[simp]: "{a.. {..b} = {.. min a b}"  hoelzl@50417  604  by (auto simp: min_def)  hoelzl@50417  605 hoelzl@57447  606 lemma Ioc_disjoint: "{a<..b} \ {c<..d} = {} \ b \ a \ d \ c \ b \ c \ d \ a"  hoelzl@57447  607  using assms by auto  hoelzl@57447  608 nipkow@32456  609 end  nipkow@32456  610 hoelzl@51329  611 context complete_lattice  hoelzl@51329  612 begin  hoelzl@51329  613 hoelzl@51329  614 lemma  hoelzl@51329  615  shows Sup_atLeast[simp]: "Sup {x ..} = top"  hoelzl@51329  616  and Sup_greaterThanAtLeast[simp]: "x < top \ Sup {x <..} = top"  hoelzl@51329  617  and Sup_atMost[simp]: "Sup {.. y} = y"  hoelzl@51329  618  and Sup_atLeastAtMost[simp]: "x \ y \ Sup { x .. y} = y"  hoelzl@51329  619  and Sup_greaterThanAtMost[simp]: "x < y \ Sup { x <.. y} = y"  hoelzl@51329  620  by (auto intro!: Sup_eqI)  hoelzl@51329  621 hoelzl@51329  622 lemma  hoelzl@51329  623  shows Inf_atMost[simp]: "Inf {.. x} = bot"  hoelzl@51329  624  and Inf_atMostLessThan[simp]: "top < x \ Inf {..< x} = bot"  hoelzl@51329  625  and Inf_atLeast[simp]: "Inf {x ..} = x"  hoelzl@51329  626  and Inf_atLeastAtMost[simp]: "x \ y \ Inf { x .. y} = x"  hoelzl@51329  627  and Inf_atLeastLessThan[simp]: "x < y \ Inf { x ..< y} = x"  hoelzl@51329  628  by (auto intro!: Inf_eqI)  hoelzl@51329  629 hoelzl@51329  630 end  hoelzl@51329  631 hoelzl@51329  632 lemma  hoelzl@53216  633  fixes x y :: "'a :: {complete_lattice, dense_linorder}"  hoelzl@51329  634  shows Sup_lessThan[simp]: "Sup {..< y} = y"  hoelzl@51329  635  and Sup_atLeastLessThan[simp]: "x < y \ Sup { x ..< y} = y"  hoelzl@51329  636  and Sup_greaterThanLessThan[simp]: "x < y \ Sup { x <..< y} = y"  hoelzl@51329  637  and Inf_greaterThan[simp]: "Inf {x <..} = x"  hoelzl@51329  638  and Inf_greaterThanAtMost[simp]: "x < y \ Inf { x <.. y} = x"  hoelzl@51329  639  and Inf_greaterThanLessThan[simp]: "x < y \ Inf { x <..< y} = x"  hoelzl@51329  640  by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded)  nipkow@32456  641 paulson@14485  642 subsection {* Intervals of natural numbers *}  paulson@14485  643 paulson@15047  644 subsubsection {* The Constant @{term lessThan} *}  paulson@15047  645 paulson@14485  646 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"  paulson@14485  647 by (simp add: lessThan_def)  paulson@14485  648 paulson@14485  649 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"  paulson@14485  650 by (simp add: lessThan_def less_Suc_eq, blast)  paulson@14485  651 kleing@43156  652 text {* The following proof is convenient in induction proofs where  hoelzl@39072  653 new elements get indices at the beginning. So it is used to transform  hoelzl@39072  654 @{term "{.. Suc  {.. Suc (x - 1)" by auto  hoelzl@39072  660  with x < Suc n show "x = 0" by auto  hoelzl@39072  661 qed  hoelzl@39072  662 paulson@14485  663 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"  paulson@14485  664 by (simp add: lessThan_def atMost_def less_Suc_eq_le)  paulson@14485  665 paulson@14485  666 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"  paulson@14485  667 by blast  paulson@14485  668 paulson@15047  669 subsubsection {* The Constant @{term greaterThan} *}  paulson@15047  670 paulson@14485  671 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"  paulson@14485  672 apply (simp add: greaterThan_def)  paulson@14485  673 apply (blast dest: gr0_conv_Suc [THEN iffD1])  paulson@14485  674 done  paulson@14485  675 paulson@14485  676 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"  paulson@14485  677 apply (simp add: greaterThan_def)  paulson@14485  678 apply (auto elim: linorder_neqE)  paulson@14485  679 done  paulson@14485  680 paulson@14485  681 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"  paulson@14485  682 by blast  paulson@14485  683 paulson@15047  684 subsubsection {* The Constant @{term atLeast} *}  paulson@15047  685 paulson@14485  686 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"  paulson@14485  687 by (unfold atLeast_def UNIV_def, simp)  paulson@14485  688 paulson@14485  689 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"  paulson@14485  690 apply (simp add: atLeast_def)  paulson@14485  691 apply (simp add: Suc_le_eq)  paulson@14485  692 apply (simp add: order_le_less, blast)  paulson@14485  693 done  paulson@14485  694 paulson@14485  695 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"  paulson@14485  696  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)  paulson@14485  697 paulson@14485  698 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"  paulson@14485  699 by blast  paulson@14485  700 paulson@15047  701 subsubsection {* The Constant @{term atMost} *}  paulson@15047  702 paulson@14485  703 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"  paulson@14485  704 by (simp add: atMost_def)  paulson@14485  705 paulson@14485  706 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"  paulson@14485  707 apply (simp add: atMost_def)  paulson@14485  708 apply (simp add: less_Suc_eq order_le_less, blast)  paulson@14485  709 done  paulson@14485  710 paulson@14485  711 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"  paulson@14485  712 by blast  paulson@14485  713 paulson@15047  714 subsubsection {* The Constant @{term atLeastLessThan} *}  paulson@15047  715 nipkow@28068  716 text{*The orientation of the following 2 rules is tricky. The lhs is  nipkow@24449  717 defined in terms of the rhs. Hence the chosen orientation makes sense  nipkow@24449  718 in this theory --- the reverse orientation complicates proofs (eg  nipkow@24449  719 nontermination). But outside, when the definition of the lhs is rarely  nipkow@24449  720 used, the opposite orientation seems preferable because it reduces a  nipkow@24449  721 specific concept to a more general one. *}  nipkow@28068  722 paulson@15047  723 lemma atLeast0LessThan: "{0::nat.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  763 by (auto simp add: atLeastAtMost_def)  nipkow@15554  764 noschinl@45932  765 lemma atLeastAtMost_insertL: "m \ n \ insert m {Suc m..n} = {m ..n}"  noschinl@45932  766 by auto  noschinl@45932  767 kleing@43157  768 text {* The analogous result is useful on @{typ int}: *}  kleing@43157  769 (* here, because we don't have an own int section *)  kleing@43157  770 lemma atLeastAtMostPlus1_int_conv:  kleing@43157  771  "m <= 1+n \ {m..1+n} = insert (1+n) {m..n::int}"  kleing@43157  772  by (auto intro: set_eqI)  kleing@43157  773 paulson@33044  774 lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j.. (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k))  lp15@57113  792  else {})"  lp15@57113  793  by (simp add: numeral_eq_Suc atLeastLessThanSuc)  lp15@57113  794 nipkow@16733  795 subsubsection {* Image *}  nipkow@16733  796 nipkow@16733  797 lemma image_add_atLeastAtMost:  nipkow@16733  798  "(%n::nat. n+k)  {i..j} = {i+k..j+k}" (is "?A = ?B")  nipkow@16733  799 proof  nipkow@16733  800  show "?A \ ?B" by auto  nipkow@16733  801 next  nipkow@16733  802  show "?B \ ?A"  nipkow@16733  803  proof  nipkow@16733  804  fix n assume a: "n : ?B"  webertj@20217  805  hence "n - k : {i..j}" by auto  nipkow@16733  806  moreover have "n = (n - k) + k" using a by auto  nipkow@16733  807  ultimately show "n : ?A" by blast  nipkow@16733  808  qed  nipkow@16733  809 qed  nipkow@16733  810 nipkow@16733  811 lemma image_add_atLeastLessThan:  nipkow@16733  812  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  815 next  nipkow@16733  816  show "?B \ ?A"  nipkow@16733  817  proof  nipkow@16733  818  fix n assume a: "n : ?B"  webertj@20217  819  hence "n - k : {i..i. i - c)  {x ..< y} =  hoelzl@37664  843  (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"  hoelzl@37664  844  (is "_ = ?right")  hoelzl@37664  845 proof safe  hoelzl@37664  846  fix a assume a: "a \ ?right"  hoelzl@37664  847  show "a \ (\i. i - c)  {x ..< y}"  hoelzl@37664  848  proof cases  hoelzl@37664  849  assume "c < y" with a show ?thesis  hoelzl@37664  850  by (auto intro!: image_eqI[of _ _ "a + c"])  hoelzl@37664  851  next  hoelzl@37664  852  assume "\ c < y" with a show ?thesis  hoelzl@37664  853  by (auto intro!: image_eqI[of _ _ x] split: split_if_asm)  hoelzl@37664  854  qed  hoelzl@37664  855 qed auto  hoelzl@37664  856 Andreas@51152  857 lemma image_int_atLeastLessThan: "int  {a.. uminus  {x<..}"  hoelzl@35580  871  by (rule imageI) (simp add: *)  hoelzl@35580  872  thus "y \ uminus  {x<..}" by simp  hoelzl@35580  873 next  hoelzl@35580  874  fix y assume "y \ -x"  hoelzl@35580  875  have "- (-y) \ uminus  {x..}"  hoelzl@35580  876  by (rule imageI) (insert y \ -x[THEN le_imp_neg_le], simp)  hoelzl@35580  877  thus "y \ uminus  {x..}" by simp  hoelzl@35580  878 qed simp_all  hoelzl@35580  879 hoelzl@35580  880 lemma  hoelzl@35580  881  fixes x :: 'a  hoelzl@35580  882  shows image_uminus_lessThan[simp]: "uminus  {.. finite N"  nipkow@28068  929 apply (rule finite_subset)  nipkow@28068  930  apply (rule_tac [2] finite_lessThan, auto)  nipkow@28068  931 done  nipkow@28068  932 nipkow@31044  933 text {* A set of natural numbers is finite iff it is bounded. *}  nipkow@31044  934 lemma finite_nat_set_iff_bounded:  nipkow@31044  935  "finite(N::nat set) = (EX m. ALL n:N. nnat. (!!n. n \ f n) ==> finite {n. f n \ u}"  nipkow@28068  951 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)  paulson@14485  952 hoelzl@56328  953 nipkow@24853  954 text{* Any subset of an interval of natural numbers the size of the  nipkow@24853  955 subset is exactly that interval. *}  nipkow@24853  956 nipkow@24853  957 lemma subset_card_intvl_is_intvl:  blanchet@55085  958  assumes "A \ {k.. A" by auto  blanchet@55085  968  with insert have "A <= {k..i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B")  nipkow@36755  982 proof  nipkow@36755  983  show "?A <= ?B"  nipkow@36755  984  proof  nipkow@36755  985  fix x assume "x : ?A"  nipkow@36755  986  then obtain i where i: "i\n" "x : M i" by auto  nipkow@36755  987  show "x : ?B"  nipkow@36755  988  proof(cases i)  nipkow@36755  989  case 0 with i show ?thesis by simp  nipkow@36755  990  next  nipkow@36755  991  case (Suc j) with i show ?thesis by auto  nipkow@36755  992  qed  nipkow@36755  993  qed  nipkow@36755  994 next  nipkow@36755  995  show "?B <= ?A" by auto  nipkow@36755  996 qed  nipkow@36755  997 nipkow@36755  998 lemma UN_le_add_shift:  nipkow@36755  999  "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B")  nipkow@36755  1000 proof  nipkow@44890  1001  show "?A <= ?B" by fastforce  nipkow@36755  1002 next  nipkow@36755  1003  show "?B <= ?A"  nipkow@36755  1004  proof  nipkow@36755  1005  fix x assume "x : ?B"  nipkow@36755  1006  then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto  nipkow@36755  1007  hence "i-k\n & x : M((i-k)+k)" by auto  nipkow@36755  1008  thus "x : ?A" by blast  nipkow@36755  1009  qed  nipkow@36755  1010 qed  nipkow@36755  1011 paulson@32596  1012 lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)"  paulson@32596  1013  by (auto simp add: atLeast0LessThan)  paulson@32596  1014 paulson@32596  1015 lemma UN_finite_subset: "(!!n::nat. (\i\{0.. C) \ (\n. A n) \ C"  paulson@32596  1016  by (subst UN_UN_finite_eq [symmetric]) blast  paulson@32596  1017 paulson@33044  1018 lemma UN_finite2_subset:  paulson@33044  1019  "(!!n::nat. (\i\{0.. (\i\{0.. (\n. A n) \ (\n. B n)"  paulson@33044  1020  apply (rule UN_finite_subset)  paulson@33044  1021  apply (subst UN_UN_finite_eq [symmetric, of B])  paulson@33044  1022  apply blast  paulson@33044  1023  done  paulson@32596  1024 paulson@32596  1025 lemma UN_finite2_eq:  paulson@33044  1026  "(!!n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)"  paulson@33044  1027  apply (rule subset_antisym)  paulson@33044  1028  apply (rule UN_finite2_subset, blast)  paulson@33044  1029  apply (rule UN_finite2_subset [where k=k])  huffman@35216  1030  apply (force simp add: atLeastLessThan_add_Un [of 0])  paulson@33044  1031  done  paulson@32596  1032 paulson@32596  1033 paulson@14485  1034 subsubsection {* Cardinality *}  paulson@14485  1035 nipkow@15045  1036 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  1076 apply(drule ex_bij_betw_finite_nat)  nipkow@31438  1077 apply(drule ex_bij_betw_nat_finite)  nipkow@31438  1078 apply(auto intro!:bij_betw_trans)  nipkow@31438  1079 done  nipkow@31438  1080 nipkow@31438  1081 lemma ex_bij_betw_nat_finite_1:  nipkow@31438  1082  "finite M \ \h. bij_betw h {1 .. card M} M"  nipkow@31438  1083 by (rule finite_same_card_bij) auto  nipkow@31438  1084 hoelzl@40703  1085 lemma bij_betw_iff_card:  hoelzl@40703  1086  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  1087  shows BIJ: "(\f. bij_betw f A B) \ (card A = card B)"  hoelzl@40703  1088 using assms  hoelzl@40703  1089 proof(auto simp add: bij_betw_same_card)  hoelzl@40703  1090  assume *: "card A = card B"  hoelzl@40703  1091  obtain f where "bij_betw f A {0 ..< card A}"  hoelzl@40703  1092  using FIN ex_bij_betw_finite_nat by blast  hoelzl@40703  1093  moreover obtain g where "bij_betw g {0 ..< card B} B"  hoelzl@40703  1094  using FIN' ex_bij_betw_nat_finite by blast  hoelzl@40703  1095  ultimately have "bij_betw (g o f) A B"  hoelzl@40703  1096  using * by (auto simp add: bij_betw_trans)  hoelzl@40703  1097  thus "(\f. bij_betw f A B)" by blast  hoelzl@40703  1098 qed  hoelzl@40703  1099 hoelzl@40703  1100 lemma inj_on_iff_card_le:  hoelzl@40703  1101  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  1102  shows "(\f. inj_on f A \ f  A \ B) = (card A \ card B)"  hoelzl@40703  1103 proof (safe intro!: card_inj_on_le)  hoelzl@40703  1104  assume *: "card A \ card B"  hoelzl@40703  1105  obtain f where 1: "inj_on f A" and 2: "f  A = {0 ..< card A}"  hoelzl@40703  1106  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force  hoelzl@40703  1107  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g  {0 ..< card B} = B"  hoelzl@40703  1108  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force  hoelzl@40703  1109  ultimately have "inj_on g (f  A)" using subset_inj_on[of g _ "f  A"] * by force  hoelzl@40703  1110  hence "inj_on (g o f) A" using 1 comp_inj_on by blast  hoelzl@40703  1111  moreover  hoelzl@40703  1112  {have "{0 ..< card A} \ {0 ..< card B}" using * by force  hoelzl@40703  1113  with 2 have "f  A \ {0 ..< card B}" by blast  hoelzl@40703  1114  hence "(g o f)  A \ B" unfolding comp_def using 3 by force  hoelzl@40703  1115  }  hoelzl@40703  1116  ultimately show "(\f. inj_on f A \ f  A \ B)" by blast  hoelzl@40703  1117 qed (insert assms, auto)  nipkow@26105  1118 paulson@14485  1119 subsection {* Intervals of integers *}  paulson@14485  1120 nipkow@15045  1121 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l.. u ==>  nipkow@15045  1134  {(0::int).. u")  paulson@14485  1143  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1144  apply (rule finite_imageI)  paulson@14485  1145  apply auto  paulson@14485  1146  done  paulson@14485  1147 nipkow@15045  1148 lemma finite_atLeastLessThan_int [iff]: "finite {l.. u")  paulson@14485  1170  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1171  apply (subst card_image)  paulson@14485  1172  apply (auto simp add: inj_on_def)  paulson@14485  1173  done  paulson@14485  1174 nipkow@15045  1175 lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}"  bulwahn@27656  1197 proof -  bulwahn@27656  1198  have "{k. P k \ k < i} \ {.. M"  bulwahn@27656  1204 shows "card {k \ M. k < Suc i} \ 0"  bulwahn@27656  1205 proof -  bulwahn@27656  1206  from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto  bulwahn@27656  1207  with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)  bulwahn@27656  1208 qed  bulwahn@27656  1209 bulwahn@27656  1210 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"  haftmann@37388  1211 apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"])  bulwahn@27656  1212 apply auto  bulwahn@27656  1213 apply (rule inj_on_diff_nat)  bulwahn@27656  1214 apply auto  bulwahn@27656  1215 apply (case_tac x)  bulwahn@27656  1216 apply auto  bulwahn@27656  1217 apply (case_tac xa)  bulwahn@27656  1218 apply auto  bulwahn@27656  1219 apply (case_tac xa)  bulwahn@27656  1220 apply auto  bulwahn@27656  1221 done  bulwahn@27656  1222 bulwahn@27656  1223 lemma card_less_Suc:  bulwahn@27656  1224  assumes zero_in_M: "0 \ M"  bulwahn@27656  1225  shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"  bulwahn@27656  1226 proof -  bulwahn@27656  1227  from assms have a: "0 \ {k \ M. k < Suc i}" by simp  bulwahn@27656  1228  hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})"  bulwahn@27656  1229  by (auto simp only: insert_Diff)  bulwahn@27656  1230  have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto  lp15@57113  1231  from finite_M_bounded_by_nat[of "\x. x \ M" "Suc i"]  lp15@57113  1232  have "Suc (card {k. Suc k \ M \ k < i}) = card (insert 0 ({k \ M. k < Suc i} - {0}))"  bulwahn@27656  1233  apply (subst card_insert)  bulwahn@27656  1234  apply simp_all  bulwahn@27656  1235  apply (subst b)  bulwahn@27656  1236  apply (subst card_less_Suc2[symmetric])  bulwahn@27656  1237  apply simp_all  bulwahn@27656  1238  done  bulwahn@27656  1239  with c show ?thesis by simp  bulwahn@27656  1240 qed  bulwahn@27656  1241 paulson@14485  1242 paulson@13850  1243 subsection {*Lemmas useful with the summation operator setsum*}  paulson@13850  1244 ballarin@16102  1245 text {* For examples, see Algebra/poly/UnivPoly2.thy *}  ballarin@13735  1246 wenzelm@14577  1247 subsubsection {* Disjoint Unions *}  ballarin@13735  1248 wenzelm@14577  1249 text {* Singletons and open intervals *}  ballarin@13735  1250 ballarin@13735  1251 lemma ivl_disj_un_singleton:  nipkow@15045  1252  "{l::'a::linorder} Un {l<..} = {l..}"  nipkow@15045  1253  "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  1257  "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  1266  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  1268  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  1270  "(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  1282  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  1284 by auto  ballarin@13735  1285 ballarin@13735  1286 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two  ballarin@13735  1287 wenzelm@14577  1288 subsubsection {* Disjoint Intersections *}  ballarin@13735  1289 wenzelm@14577  1290 text {* One- and two-sided intervals *}  ballarin@13735  1291 ballarin@13735  1292 lemma ivl_disj_int_one:  nipkow@15045  1293  "{..l::'a::order} Int {l<.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  1333 apply(auto simp:linorder_not_le)  nipkow@15542  1334 apply(rule ccontr)  nipkow@15542  1335 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  1336 apply(clarsimp simp:linorder_not_le)  nipkow@44890  1337 apply(fastforce)  nipkow@15542  1338 done  nipkow@15542  1339 nipkow@15041  1340 nipkow@15042  1341 subsection {* Summation indexed over intervals *}  nipkow@15042  1342 nipkow@15042  1343 syntax  nipkow@15042  1344  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  1345  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  1346  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@16052  1347  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  nipkow@15042  1348 syntax (xsymbols)  nipkow@15042  1349  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  1350  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  1351  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  1352  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15042  1353 syntax (HTML output)  nipkow@15042  1354  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  1355  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  1356  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  1357  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15056  1358 syntax (latex_sum output)  nipkow@15052  1359  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  1360  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@15052  1361  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  1362  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@16052  1363  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1364  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15052  1365  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1366  ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15041  1367 nipkow@15048  1368 translations  nipkow@28853  1369  "\x=a..b. t" == "CONST setsum (%x. t) {a..b}"  nipkow@28853  1370  "\x=a..i\n. t" == "CONST setsum (\i. t) {..n}"  nipkow@28853  1372  "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  1380 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  1382 @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \  nipkow@15542  1405  setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)"  haftmann@57514  1412 by (simp add:atMost_Suc ac_simps)  nipkow@16052  1413 nipkow@16041  1414 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n"  haftmann@57514  1415 by (simp add:lessThan_Suc ac_simps)  nipkow@15041  1416 nipkow@15911  1417 lemma setsum_cl_ivl_Suc[simp]:  nipkow@15561  1418  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  haftmann@57514  1419 by (auto simp:ac_simps atLeastAtMostSuc_conv)  nipkow@15561  1420 nipkow@15911  1421 lemma setsum_op_ivl_Suc[simp]:  nipkow@15561  1422  "setsum f {m..  nipkow@15561  1426  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  haftmann@57514  1427 by (auto simp:ac_simps atLeastAtMostSuc_conv)  nipkow@16041  1428 *)  nipkow@28068  1429 nipkow@28068  1430 lemma setsum_head:  nipkow@28068  1431  fixes n :: nat  nipkow@28068  1432  assumes mn: "m <= n"  nipkow@28068  1433  shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  nipkow@28068  1434 proof -  nipkow@28068  1435  from mn  nipkow@28068  1436  have "{m..n} = {m} \ {m<..n}"  nipkow@28068  1437  by (auto intro: ivl_disj_un_singleton)  nipkow@28068  1438  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  nipkow@28068  1439  by (simp add: atLeast0LessThan)  nipkow@28068  1440  also have "\ = ?rhs" by simp  nipkow@28068  1441  finally show ?thesis .  nipkow@28068  1442 qed  nipkow@28068  1443 nipkow@28068  1444 lemma setsum_head_Suc:  nipkow@28068  1445  "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}"  nipkow@28068  1446 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)  nipkow@28068  1447 nipkow@28068  1448 lemma setsum_head_upt_Suc:  nipkow@28068  1449  "m < n \ setsum f {m.. n + 1"  nipkow@31501  1455  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"  nipkow@31501  1456 proof-  nipkow@31501  1457  have "{m .. n+p} = {m..n} \ {n+1..n+p}" using m \ n+1 by auto  haftmann@57418  1458  thus ?thesis by (auto simp: ivl_disj_int setsum.union_disjoint  nipkow@31501  1459  atLeastSucAtMost_greaterThanAtMost)  nipkow@31501  1460 qed  nipkow@28068  1461 nipkow@15539  1462 lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \  nipkow@15539  1463  setsum f {m.. 'a::ab_group_add"  nipkow@15539  1468 shows "\ m \ n; n \ p \ \  nipkow@15539  1469  setsum f {m.. ('a::ab_group_add)"  nipkow@31505  1476  shows "setsum (\k. f k - f(k + 1)) {(m::nat) .. n} =  nipkow@31505  1477  (if m <= n then f m - f(n + 1) else 0)"  nipkow@31505  1478 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)  nipkow@31505  1479 hoelzl@56194  1480 lemma setsum_nat_group: "(\m setsum f {Suc 0..k} = setsum f {0..k}"  nipkow@28068  1506 by(simp add:setsum_head_Suc)  kleing@19106  1507 nipkow@28068  1508 lemma setsum_shift_lb_Suc0_0_upt:  nipkow@28068  1509  "f(0::nat) = 0 \ setsum f {Suc 0.. 'a::comm_monoid_add"  haftmann@52380  1516  shows "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))"  haftmann@52380  1517 proof (induct n)  haftmann@52380  1518  case 0 show ?case by simp  haftmann@52380  1519 next  haftmann@52380  1520  case (Suc n) note IH = this  haftmann@52380  1521  have "(\i\Suc (Suc n). f i) = (\i\Suc n. f i) + f (Suc (Suc n))"  haftmann@52380  1522  by (rule setsum_atMost_Suc)  haftmann@52380  1523  also have "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))"  haftmann@52380  1524  by (rule IH)  haftmann@52380  1525  also have "f 0 + (\i\n. f (Suc i)) + f (Suc (Suc n)) =  haftmann@52380  1526  f 0 + ((\i\n. f (Suc i)) + f (Suc (Suc n)))"  haftmann@57512  1527  by (rule add.assoc)  haftmann@52380  1528  also have "(\i\n. f (Suc i)) + f (Suc (Suc n)) = (\i\Suc n. f (Suc i))"  haftmann@52380  1529  by (rule setsum_atMost_Suc [symmetric])  haftmann@52380  1530  finally show ?case .  haftmann@52380  1531 qed  haftmann@52380  1532 lp15@56238  1533 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  1538  assumes "m \ Suc n"  lp15@56238  1539  shows "(\i = m..n. f(Suc i) - f i) = f (Suc n) - f m"  lp15@56238  1540 using assms by (induct n) (auto simp: le_Suc_eq)  lp15@55718  1541 lp15@55718  1542 lemma nested_setsum_swap:  lp15@55718  1543  "(\i = 0..n. (\j = 0..j = 0..i = Suc j..n. a i j)"  haftmann@57418  1544  by (induction n) (auto simp: setsum.distrib)  lp15@55718  1545 lp15@56215  1546 lemma nested_setsum_swap':  lp15@56215  1547  "(\i\n. (\jji = Suc j..n. a i j)"  haftmann@57418  1548  by (induction n) (auto simp: setsum.distrib)  lp15@56215  1549 lp15@56215  1550 lemma setsum_zero_power [simp]:  lp15@56215  1551  fixes c :: "nat \ 'a::division_ring"  lp15@56215  1552  shows "(\i\A. c i * 0^i) = (if finite A \ 0 \ A then c 0 else 0)"  lp15@56215  1553 apply (cases "finite A")  lp15@56215  1554  by (induction A rule: finite_induct) auto  lp15@56215  1555 lp15@56238  1556 lemma setsum_zero_power' [simp]:  lp15@56238  1557  fixes c :: "nat \ 'a::field"  lp15@56238  1558  shows "(\i\A. c i * 0^i / d i) = (if finite A \ 0 \ A then c 0 / d 0 else 0)"  lp15@56238  1559  using setsum_zero_power [of "\i. c i / d i" A]  lp15@56238  1560  by auto  lp15@56238  1561 haftmann@52380  1562 ballarin@17149  1563 subsection {* The formula for geometric sums *}  ballarin@17149  1564 ballarin@17149  1565 lemma geometric_sum:  haftmann@36307  1566  assumes "x \ 1"  hoelzl@56193  1567  shows "(\i 0" by simp_all  hoelzl@56193  1570  moreover have "(\i 0)  haftmann@36307  1572  ultimately show ?thesis by simp  haftmann@36307  1573 qed  haftmann@36307  1574 ballarin@17149  1575 kleing@19469  1576 subsection {* The formula for arithmetic sums *}  kleing@19469  1577 huffman@47222  1578 lemma gauss_sum:  hoelzl@56193  1579  "(2::'a::comm_semiring_1)*(\i\{1..n}. of_nat i) = of_nat n*((of_nat n)+1)"  kleing@19469  1580 proof (induct n)  kleing@19469  1581  case 0  kleing@19469  1582  show ?case by simp  kleing@19469  1583 next  kleing@19469  1584  case (Suc n)  huffman@47222  1585  then show ?case  huffman@47222  1586  by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one)  huffman@47222  1587  (* FIXME: make numeral cancellation simprocs work for semirings *)  kleing@19469  1588 qed  kleing@19469  1589 kleing@19469  1590 theorem arith_series_general:  huffman@47222  1591  "(2::'a::comm_semiring_1) * (\i\{.. 1"  kleing@19469  1595  let ?I = "\i. of_nat i" and ?n = "of_nat n"  kleing@19469  1596  have  kleing@19469  1597  "(\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  1610  by (simp only: mult.assoc gauss_sum [of "n - 1"], unfold One_nat_def)  haftmann@57514  1611  (simp add: mult.commute trans [OF add.commute of_nat_Suc [symmetric]])  huffman@47222  1612  finally show ?thesis  huffman@47222  1613  unfolding mult_2 by (simp add: algebra_simps)  kleing@19469  1614 next  kleing@19469  1615  assume "\(n > 1)"  kleing@19469  1616  hence "n = 1 \ n = 0" by auto  huffman@47222  1617  thus ?thesis by (auto simp: mult_2)  kleing@19469  1618 qed  kleing@19469  1619 kleing@19469  1620 lemma arith_series_nat:  huffman@47222  1621  "(2::nat) * (\i\{..i\{..i\{..nat"  kleing@19022  1637  shows  kleing@19022  1638  "\x. Q x \ P x \  kleing@19022  1639  (\xxxxxii 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1668  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1669  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10)  paulson@29960  1670  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10)  paulson@29960  1671 syntax (xsymbols)  paulson@29960  1672  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1673  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1674  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1675  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1676 syntax (HTML output)  paulson@29960  1677  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1678  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1679  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1680  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1681 syntax (latex_prod output)  paulson@29960  1682  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1683  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1684  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1685  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1686  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1687  ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1688  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1689  ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1690 paulson@29960  1691 translations  paulson@29960  1692  "\x=a..b. t" == "CONST setprod (%x. t) {a..b}"  paulson@29960  1693  "\x=a..i\n. t" == "CONST setprod (\i. t) {..n}"  paulson@29960  1695  "\ii. t) {..= 0 \ nat_set {x..y}"  haftmann@33318  1711  by (simp add: nat_set_def)  haftmann@33318  1712 haftmann@35644  1713 declare transfer_morphism_nat_int[transfer add  haftmann@33318  1714  return: transfer_nat_int_set_functions  haftmann@33318  1715  transfer_nat_int_set_function_closures  haftmann@33318  1716 ]  haftmann@33318  1717 haftmann@33318  1718 lemma transfer_int_nat_set_functions:  haftmann@33318  1719  "is_nat m \ is_nat n \ {m..n} = int  {nat m..nat n}"  haftmann@33318  1720  by (simp only: is_nat_def transfer_nat_int_set_functions  haftmann@33318  1721  transfer_nat_int_set_function_closures  haftmann@33318  1722  transfer_nat_int_set_return_embed nat_0_le  haftmann@33318  1723  cong: transfer_nat_int_set_cong)  haftmann@33318  1724 haftmann@33318  1725 lemma transfer_int_nat_set_function_closures:  haftmann@33318  1726  "is_nat x \ nat_set {x..y}"  haftmann@33318  1727  by (simp only: transfer_nat_int_set_function_closures is_nat_def)  haftmann@33318  1728 haftmann@35644  1729 declare transfer_morphism_int_nat[transfer add  haftmann@33318  1730  return: transfer_int_nat_set_functions  haftmann@33318  1731  transfer_int_nat_set_function_closures  haftmann@33318  1732 ]  haftmann@33318  1733 lp15@55242  1734 lemma setprod_int_plus_eq: "setprod int {i..i+j} = \{int i..int (i+j)}"  lp15@55242  1735  by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)  lp15@55242  1736 lp15@55242  1737 lemma setprod_int_eq: "setprod int {i..j} = \{int i..int j}"  lp15@55242  1738 proof (cases "i \ j")  lp15@55242  1739  case True  lp15@55242  1740  then show ?thesis  lp15@55242  1741  by (metis Nat.le_iff_add setprod_int_plus_eq)  lp15@55242  1742 next  lp15@55242  1743  case False  lp15@55242  1744  then show ?thesis  lp15@55242  1745  by auto  lp15@55242  1746 qed  lp15@55242  1747 nipkow@8924  1748 end `