src/HOL/Set_Interval.thy
 author wenzelm Wed Apr 10 21:20:35 2013 +0200 (2013-04-10) changeset 51692 ecd34f863242 parent 51334 fd531bd984d8 child 52380 3cc46b8cca5e permissions -rw-r--r--
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
declare command "print_case_translations" where it is actually defined;
 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  haftmann@33318  17 imports Int 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 paulson@13850  178 subsection {*Two-sided intervals*}  ballarin@13735  179 nipkow@24691  180 context ord  nipkow@24691  181 begin  nipkow@24691  182 blanchet@35828  183 lemma greaterThanLessThan_iff [simp,no_atp]:  haftmann@25062  184  "(i : {l<.. {..< b }"  hoelzl@50999  204  by auto  hoelzl@50999  205 nipkow@24691  206 end  ballarin@13735  207 nipkow@32400  208 subsubsection{* Emptyness, singletons, subset *}  nipkow@15554  209 nipkow@24691  210 context order  nipkow@24691  211 begin  nipkow@15554  212 nipkow@32400  213 lemma atLeastatMost_empty[simp]:  nipkow@32400  214  "b < a \ {a..b} = {}"  nipkow@32400  215 by(auto simp: atLeastAtMost_def atLeast_def atMost_def)  nipkow@32400  216 nipkow@32400  217 lemma atLeastatMost_empty_iff[simp]:  nipkow@32400  218  "{a..b} = {} \ (~ a <= b)"  nipkow@32400  219 by auto (blast intro: order_trans)  nipkow@32400  220 nipkow@32400  221 lemma atLeastatMost_empty_iff2[simp]:  nipkow@32400  222  "{} = {a..b} \ (~ a <= b)"  nipkow@32400  223 by auto (blast intro: order_trans)  nipkow@32400  224 nipkow@32400  225 lemma atLeastLessThan_empty[simp]:  nipkow@32400  226  "b <= a \ {a.. (~ a < b)"  nipkow@32400  231 by auto (blast intro: le_less_trans)  nipkow@32400  232 nipkow@32400  233 lemma atLeastLessThan_empty_iff2[simp]:  nipkow@32400  234  "{} = {a.. (~ a < b)"  nipkow@32400  235 by auto (blast intro: le_less_trans)  nipkow@15554  236 nipkow@32400  237 lemma greaterThanAtMost_empty[simp]: "l \ k ==> {k<..l} = {}"  nipkow@17719  238 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)  nipkow@17719  239 nipkow@32400  240 lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ ~ k < l"  nipkow@32400  241 by auto (blast intro: less_le_trans)  nipkow@32400  242 nipkow@32400  243 lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ ~ k < l"  nipkow@32400  244 by auto (blast intro: less_le_trans)  nipkow@32400  245 haftmann@29709  246 lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. {a .. b} = {a}" by simp  hoelzl@36846  253 nipkow@32400  254 lemma atLeastatMost_subset_iff[simp]:  nipkow@32400  255  "{a..b} <= {c..d} \ (~ a <= b) | c <= a & b <= d"  nipkow@32400  256 unfolding atLeastAtMost_def atLeast_def atMost_def  nipkow@32400  257 by (blast intro: order_trans)  nipkow@32400  258 nipkow@32400  259 lemma atLeastatMost_psubset_iff:  nipkow@32400  260  "{a..b} < {c..d} \  nipkow@32400  261  ((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d"  nipkow@39302  262 by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)  nipkow@32400  263 nipkow@51334  264 lemma Icc_eq_Icc[simp]:  nipkow@51334  265  "{l..h} = {l'..h'} = (l=l' \ h=h' \ \ l\h \ \ l'\h')"  nipkow@51334  266 by(simp add: order_class.eq_iff)(auto intro: order_trans)  nipkow@51334  267 hoelzl@36846  268 lemma atLeastAtMost_singleton_iff[simp]:  hoelzl@36846  269  "{a .. b} = {c} \ a = b \ b = c"  hoelzl@36846  270 proof  hoelzl@36846  271  assume "{a..b} = {c}"  hoelzl@36846  272  hence "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp  hoelzl@36846  273  moreover with {a..b} = {c} have "c \ a \ b \ c" by auto  hoelzl@36846  274  ultimately show "a = b \ b = c" by auto  hoelzl@36846  275 qed simp  hoelzl@36846  276 nipkow@51334  277 lemma Icc_subset_Ici_iff[simp]:  nipkow@51334  278  "{l..h} \ {l'..} = (~ l\h \ l\l')"  nipkow@51334  279 by(auto simp: subset_eq intro: order_trans)  nipkow@51334  280 nipkow@51334  281 lemma Icc_subset_Iic_iff[simp]:  nipkow@51334  282  "{l..h} \ {..h'} = (~ l\h \ h\h')"  nipkow@51334  283 by(auto simp: subset_eq intro: order_trans)  nipkow@51334  284 nipkow@51334  285 lemma not_Ici_eq_empty[simp]: "{l..} \ {}"  nipkow@51334  286 by(auto simp: set_eq_iff)  nipkow@51334  287 nipkow@51334  288 lemma not_Iic_eq_empty[simp]: "{..h} \ {}"  nipkow@51334  289 by(auto simp: set_eq_iff)  nipkow@51334  290 nipkow@51334  291 lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric]  nipkow@51334  292 lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric]  nipkow@51334  293 nipkow@24691  294 end  paulson@14485  295 nipkow@51334  296 context no_top  nipkow@51334  297 begin  nipkow@51334  298 nipkow@51334  299 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  300 lemma not_UNIV_le_Icc[simp]: "\ UNIV \ {l..h}"  nipkow@51334  301 using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  302 nipkow@51334  303 lemma not_UNIV_le_Iic[simp]: "\ UNIV \ {..h}"  nipkow@51334  304 using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  305 nipkow@51334  306 lemma not_Ici_le_Icc[simp]: "\ {l..} \ {l'..h'}"  nipkow@51334  307 using gt_ex[of h']  nipkow@51334  308 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  309 nipkow@51334  310 lemma not_Ici_le_Iic[simp]: "\ {l..} \ {..h'}"  nipkow@51334  311 using gt_ex[of h']  nipkow@51334  312 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  313 nipkow@51334  314 end  nipkow@51334  315 nipkow@51334  316 context no_bot  nipkow@51334  317 begin  nipkow@51334  318 nipkow@51334  319 lemma not_UNIV_le_Ici[simp]: "\ UNIV \ {l..}"  nipkow@51334  320 using lt_ex[of l] by(auto simp: subset_eq less_le_not_le)  nipkow@51334  321 nipkow@51334  322 lemma not_Iic_le_Icc[simp]: "\ {..h} \ {l'..h'}"  nipkow@51334  323 using lt_ex[of l']  nipkow@51334  324 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  325 nipkow@51334  326 lemma not_Iic_le_Ici[simp]: "\ {..h} \ {l'..}"  nipkow@51334  327 using lt_ex[of l']  nipkow@51334  328 by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)  nipkow@51334  329 nipkow@51334  330 end  nipkow@51334  331 nipkow@51334  332 nipkow@51334  333 context no_top  nipkow@51334  334 begin  nipkow@51334  335 nipkow@51334  336 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  337 lemma not_UNIV_eq_Icc[simp]: "\ UNIV = {l'..h'}"  nipkow@51334  338 using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  339 nipkow@51334  340 lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric]  nipkow@51334  341 nipkow@51334  342 lemma not_UNIV_eq_Iic[simp]: "\ UNIV = {..h'}"  nipkow@51334  343 using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  344 nipkow@51334  345 lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric]  nipkow@51334  346 nipkow@51334  347 lemma not_Icc_eq_Ici[simp]: "\ {l..h} = {l'..}"  nipkow@51334  348 unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast  nipkow@51334  349 nipkow@51334  350 lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric]  nipkow@51334  351 nipkow@51334  352 (* also holds for no_bot but no_top should suffice *)  nipkow@51334  353 lemma not_Iic_eq_Ici[simp]: "\ {..h} = {l'..}"  nipkow@51334  354 using not_Ici_le_Iic[of l' h] by blast  nipkow@51334  355 nipkow@51334  356 lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric]  nipkow@51334  357 nipkow@51334  358 end  nipkow@51334  359 nipkow@51334  360 context no_bot  nipkow@51334  361 begin  nipkow@51334  362 nipkow@51334  363 lemma not_UNIV_eq_Ici[simp]: "\ UNIV = {l'..}"  nipkow@51334  364 using lt_ex[of l'] by(auto simp: set_eq_iff less_le_not_le)  nipkow@51334  365 nipkow@51334  366 lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric]  nipkow@51334  367 nipkow@51334  368 lemma not_Icc_eq_Iic[simp]: "\ {l..h} = {..h'}"  nipkow@51334  369 unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast  nipkow@51334  370 nipkow@51334  371 lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric]  nipkow@51334  372 nipkow@51334  373 end  nipkow@51334  374 nipkow@51334  375 hoelzl@51329  376 context inner_dense_linorder  hoelzl@42891  377 begin  hoelzl@42891  378 hoelzl@42891  379 lemma greaterThanLessThan_empty_iff[simp]:  hoelzl@42891  380  "{ a <..< b } = {} \ b \ a"  hoelzl@42891  381  using dense[of a b] by (cases "a < b") auto  hoelzl@42891  382 hoelzl@42891  383 lemma greaterThanLessThan_empty_iff2[simp]:  hoelzl@42891  384  "{} = { a <..< b } \ b \ a"  hoelzl@42891  385  using dense[of a b] by (cases "a < b") auto  hoelzl@42891  386 hoelzl@42901  387 lemma atLeastLessThan_subseteq_atLeastAtMost_iff:  hoelzl@42901  388  "{a ..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  389  using dense[of "max a d" "b"]  hoelzl@42901  390  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  391 hoelzl@42901  392 lemma greaterThanAtMost_subseteq_atLeastAtMost_iff:  hoelzl@42901  393  "{a <.. b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  394  using dense[of "a" "min c b"]  hoelzl@42901  395  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  396 hoelzl@42901  397 lemma greaterThanLessThan_subseteq_atLeastAtMost_iff:  hoelzl@42901  398  "{a <..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  399  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@42901  400  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  401 hoelzl@43657  402 lemma atLeastAtMost_subseteq_atLeastLessThan_iff:  hoelzl@43657  403  "{a .. b} \ { c ..< d } \ (a \ b \ c \ a \ b < d)"  hoelzl@43657  404  using dense[of "max a d" "b"]  hoelzl@43657  405  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  406 hoelzl@43657  407 lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:  hoelzl@43657  408  "{a <.. b} \ { c ..< d } \ (a < b \ c \ a \ b < d)"  hoelzl@43657  409  using dense[of "a" "min c b"]  hoelzl@43657  410  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  411 hoelzl@43657  412 lemma greaterThanLessThan_subseteq_atLeastLessThan_iff:  hoelzl@43657  413  "{a <..< b} \ { c ..< d } \ (a < b \ c \ a \ b \ d)"  hoelzl@43657  414  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@43657  415  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  416 hoelzl@42891  417 end  hoelzl@42891  418 hoelzl@51329  419 context no_top  hoelzl@51329  420 begin  hoelzl@51329  421 nipkow@51334  422 lemma greaterThan_non_empty[simp]: "{x <..} \ {}"  hoelzl@51329  423  using gt_ex[of x] by auto  hoelzl@51329  424 hoelzl@51329  425 end  hoelzl@51329  426 hoelzl@51329  427 context no_bot  hoelzl@51329  428 begin  hoelzl@51329  429 nipkow@51334  430 lemma lessThan_non_empty[simp]: "{..< x} \ {}"  hoelzl@51329  431  using lt_ex[of x] by auto  hoelzl@51329  432 hoelzl@51329  433 end  hoelzl@51329  434 nipkow@32408  435 lemma (in linorder) atLeastLessThan_subset_iff:  nipkow@32408  436  "{a.. b <= a | c<=a & b<=d"  nipkow@32408  437 apply (auto simp:subset_eq Ball_def)  nipkow@32408  438 apply(frule_tac x=a in spec)  nipkow@32408  439 apply(erule_tac x=d in allE)  nipkow@32408  440 apply (simp add: less_imp_le)  nipkow@32408  441 done  nipkow@32408  442 hoelzl@40703  443 lemma atLeastLessThan_inj:  hoelzl@40703  444  fixes a b c d :: "'a::linorder"  hoelzl@40703  445  assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"  hoelzl@40703  446  shows "a = c" "b = d"  hoelzl@40703  447 using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+  hoelzl@40703  448 hoelzl@40703  449 lemma atLeastLessThan_eq_iff:  hoelzl@40703  450  fixes a b c d :: "'a::linorder"  hoelzl@40703  451  assumes "a < b" "c < d"  hoelzl@40703  452  shows "{a ..< b} = {c ..< d} \ a = c \ b = d"  hoelzl@40703  453  using atLeastLessThan_inj assms by auto  hoelzl@40703  454 nipkow@51334  455 lemma (in bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \ x = bot"  nipkow@51334  456 by (auto simp: set_eq_iff intro: le_bot)  hoelzl@51328  457 nipkow@51334  458 lemma (in top) atMost_eq_UNIV_iff: "{..x} = UNIV \ x = top"  nipkow@51334  459 by (auto simp: set_eq_iff intro: top_le)  hoelzl@51328  460 nipkow@51334  461 lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff:  nipkow@51334  462  "{x..y} = UNIV \ (x = bot \ y = top)"  nipkow@51334  463 by (auto simp: set_eq_iff intro: top_le le_bot)  hoelzl@51328  464 hoelzl@51328  465 nipkow@32456  466 subsubsection {* Intersection *}  nipkow@32456  467 nipkow@32456  468 context linorder  nipkow@32456  469 begin  nipkow@32456  470 nipkow@32456  471 lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"  nipkow@32456  472 by auto  nipkow@32456  473 nipkow@32456  474 lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"  nipkow@32456  475 by auto  nipkow@32456  476 nipkow@32456  477 lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"  nipkow@32456  478 by auto  nipkow@32456  479 nipkow@32456  480 lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"  nipkow@32456  481 by auto  nipkow@32456  482 nipkow@32456  483 lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"  nipkow@32456  484 by auto  nipkow@32456  485 nipkow@32456  486 lemma Int_atLeastLessThan[simp]: "{a.. {..b} = {.. min a b}"  hoelzl@50417  496  by (auto simp: min_def)  hoelzl@50417  497 nipkow@32456  498 end  nipkow@32456  499 hoelzl@51329  500 context complete_lattice  hoelzl@51329  501 begin  hoelzl@51329  502 hoelzl@51329  503 lemma  hoelzl@51329  504  shows Sup_atLeast[simp]: "Sup {x ..} = top"  hoelzl@51329  505  and Sup_greaterThanAtLeast[simp]: "x < top \ Sup {x <..} = top"  hoelzl@51329  506  and Sup_atMost[simp]: "Sup {.. y} = y"  hoelzl@51329  507  and Sup_atLeastAtMost[simp]: "x \ y \ Sup { x .. y} = y"  hoelzl@51329  508  and Sup_greaterThanAtMost[simp]: "x < y \ Sup { x <.. y} = y"  hoelzl@51329  509  by (auto intro!: Sup_eqI)  hoelzl@51329  510 hoelzl@51329  511 lemma  hoelzl@51329  512  shows Inf_atMost[simp]: "Inf {.. x} = bot"  hoelzl@51329  513  and Inf_atMostLessThan[simp]: "top < x \ Inf {..< x} = bot"  hoelzl@51329  514  and Inf_atLeast[simp]: "Inf {x ..} = x"  hoelzl@51329  515  and Inf_atLeastAtMost[simp]: "x \ y \ Inf { x .. y} = x"  hoelzl@51329  516  and Inf_atLeastLessThan[simp]: "x < y \ Inf { x ..< y} = x"  hoelzl@51329  517  by (auto intro!: Inf_eqI)  hoelzl@51329  518 hoelzl@51329  519 end  hoelzl@51329  520 hoelzl@51329  521 lemma  hoelzl@51329  522  fixes x y :: "'a :: {complete_lattice, inner_dense_linorder}"  hoelzl@51329  523  shows Sup_lessThan[simp]: "Sup {..< y} = y"  hoelzl@51329  524  and Sup_atLeastLessThan[simp]: "x < y \ Sup { x ..< y} = y"  hoelzl@51329  525  and Sup_greaterThanLessThan[simp]: "x < y \ Sup { x <..< y} = y"  hoelzl@51329  526  and Inf_greaterThan[simp]: "Inf {x <..} = x"  hoelzl@51329  527  and Inf_greaterThanAtMost[simp]: "x < y \ Inf { x <.. y} = x"  hoelzl@51329  528  and Inf_greaterThanLessThan[simp]: "x < y \ Inf { x <..< y} = x"  hoelzl@51329  529  by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded)  nipkow@32456  530 paulson@14485  531 subsection {* Intervals of natural numbers *}  paulson@14485  532 paulson@15047  533 subsubsection {* The Constant @{term lessThan} *}  paulson@15047  534 paulson@14485  535 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"  paulson@14485  536 by (simp add: lessThan_def)  paulson@14485  537 paulson@14485  538 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"  paulson@14485  539 by (simp add: lessThan_def less_Suc_eq, blast)  paulson@14485  540 kleing@43156  541 text {* The following proof is convenient in induction proofs where  hoelzl@39072  542 new elements get indices at the beginning. So it is used to transform  hoelzl@39072  543 @{term "{.. Suc  {.. Suc (x - 1)" by auto  hoelzl@39072  549  with x < Suc n show "x = 0" by auto  hoelzl@39072  550 qed  hoelzl@39072  551 paulson@14485  552 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"  paulson@14485  553 by (simp add: lessThan_def atMost_def less_Suc_eq_le)  paulson@14485  554 paulson@14485  555 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"  paulson@14485  556 by blast  paulson@14485  557 paulson@15047  558 subsubsection {* The Constant @{term greaterThan} *}  paulson@15047  559 paulson@14485  560 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"  paulson@14485  561 apply (simp add: greaterThan_def)  paulson@14485  562 apply (blast dest: gr0_conv_Suc [THEN iffD1])  paulson@14485  563 done  paulson@14485  564 paulson@14485  565 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"  paulson@14485  566 apply (simp add: greaterThan_def)  paulson@14485  567 apply (auto elim: linorder_neqE)  paulson@14485  568 done  paulson@14485  569 paulson@14485  570 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"  paulson@14485  571 by blast  paulson@14485  572 paulson@15047  573 subsubsection {* The Constant @{term atLeast} *}  paulson@15047  574 paulson@14485  575 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"  paulson@14485  576 by (unfold atLeast_def UNIV_def, simp)  paulson@14485  577 paulson@14485  578 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"  paulson@14485  579 apply (simp add: atLeast_def)  paulson@14485  580 apply (simp add: Suc_le_eq)  paulson@14485  581 apply (simp add: order_le_less, blast)  paulson@14485  582 done  paulson@14485  583 paulson@14485  584 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"  paulson@14485  585  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)  paulson@14485  586 paulson@14485  587 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"  paulson@14485  588 by blast  paulson@14485  589 paulson@15047  590 subsubsection {* The Constant @{term atMost} *}  paulson@15047  591 paulson@14485  592 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"  paulson@14485  593 by (simp add: atMost_def)  paulson@14485  594 paulson@14485  595 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"  paulson@14485  596 apply (simp add: atMost_def)  paulson@14485  597 apply (simp add: less_Suc_eq order_le_less, blast)  paulson@14485  598 done  paulson@14485  599 paulson@14485  600 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"  paulson@14485  601 by blast  paulson@14485  602 paulson@15047  603 subsubsection {* The Constant @{term atLeastLessThan} *}  paulson@15047  604 nipkow@28068  605 text{*The orientation of the following 2 rules is tricky. The lhs is  nipkow@24449  606 defined in terms of the rhs. Hence the chosen orientation makes sense  nipkow@24449  607 in this theory --- the reverse orientation complicates proofs (eg  nipkow@24449  608 nontermination). But outside, when the definition of the lhs is rarely  nipkow@24449  609 used, the opposite orientation seems preferable because it reduces a  nipkow@24449  610 specific concept to a more general one. *}  nipkow@28068  611 paulson@15047  612 lemma atLeast0LessThan: "{0::nat.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  652 by (auto simp add: atLeastAtMost_def)  nipkow@15554  653 noschinl@45932  654 lemma atLeastAtMost_insertL: "m \ n \ insert m {Suc m..n} = {m ..n}"  noschinl@45932  655 by auto  noschinl@45932  656 kleing@43157  657 text {* The analogous result is useful on @{typ int}: *}  kleing@43157  658 (* here, because we don't have an own int section *)  kleing@43157  659 lemma atLeastAtMostPlus1_int_conv:  kleing@43157  660  "m <= 1+n \ {m..1+n} = insert (1+n) {m..n::int}"  kleing@43157  661  by (auto intro: set_eqI)  kleing@43157  662 paulson@33044  663 lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j.. ?B" by auto  nipkow@16733  674 next  nipkow@16733  675  show "?B \ ?A"  nipkow@16733  676  proof  nipkow@16733  677  fix n assume a: "n : ?B"  webertj@20217  678  hence "n - k : {i..j}" by auto  nipkow@16733  679  moreover have "n = (n - k) + k" using a by auto  nipkow@16733  680  ultimately show "n : ?A" by blast  nipkow@16733  681  qed  nipkow@16733  682 qed  nipkow@16733  683 nipkow@16733  684 lemma image_add_atLeastLessThan:  nipkow@16733  685  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  688 next  nipkow@16733  689  show "?B \ ?A"  nipkow@16733  690  proof  nipkow@16733  691  fix n assume a: "n : ?B"  webertj@20217  692  hence "n - k : {i..i. i - c)  {x ..< y} =  hoelzl@37664  716  (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"  hoelzl@37664  717  (is "_ = ?right")  hoelzl@37664  718 proof safe  hoelzl@37664  719  fix a assume a: "a \ ?right"  hoelzl@37664  720  show "a \ (\i. i - c)  {x ..< y}"  hoelzl@37664  721  proof cases  hoelzl@37664  722  assume "c < y" with a show ?thesis  hoelzl@37664  723  by (auto intro!: image_eqI[of _ _ "a + c"])  hoelzl@37664  724  next  hoelzl@37664  725  assume "\ c < y" with a show ?thesis  hoelzl@37664  726  by (auto intro!: image_eqI[of _ _ x] split: split_if_asm)  hoelzl@37664  727  qed  hoelzl@37664  728 qed auto  hoelzl@37664  729 Andreas@51152  730 lemma image_int_atLeastLessThan: "int  {a.. uminus  {x<..}"  hoelzl@35580  744  by (rule imageI) (simp add: *)  hoelzl@35580  745  thus "y \ uminus  {x<..}" by simp  hoelzl@35580  746 next  hoelzl@35580  747  fix y assume "y \ -x"  hoelzl@35580  748  have "- (-y) \ uminus  {x..}"  hoelzl@35580  749  by (rule imageI) (insert y \ -x[THEN le_imp_neg_le], simp)  hoelzl@35580  750  thus "y \ uminus  {x..}" by simp  hoelzl@35580  751 qed simp_all  hoelzl@35580  752 hoelzl@35580  753 lemma  hoelzl@35580  754  fixes x :: 'a  hoelzl@35580  755  shows image_uminus_lessThan[simp]: "uminus  {.. finite N"  nipkow@28068  802 apply (rule finite_subset)  nipkow@28068  803  apply (rule_tac [2] finite_lessThan, auto)  nipkow@28068  804 done  nipkow@28068  805 nipkow@31044  806 text {* A set of natural numbers is finite iff it is bounded. *}  nipkow@31044  807 lemma finite_nat_set_iff_bounded:  nipkow@31044  808  "finite(N::nat set) = (EX m. ALL n:N. nnat. (!!n. n \ f n) ==> finite {n. f n \ u}"  nipkow@28068  824 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)  paulson@14485  825 nipkow@24853  826 text{* Any subset of an interval of natural numbers the size of the  nipkow@24853  827 subset is exactly that interval. *}  nipkow@24853  828 nipkow@24853  829 lemma subset_card_intvl_is_intvl:  nipkow@24853  830  "A <= {k.. A = {k..i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B")  nipkow@36755  852 proof  nipkow@36755  853  show "?A <= ?B"  nipkow@36755  854  proof  nipkow@36755  855  fix x assume "x : ?A"  nipkow@36755  856  then obtain i where i: "i\n" "x : M i" by auto  nipkow@36755  857  show "x : ?B"  nipkow@36755  858  proof(cases i)  nipkow@36755  859  case 0 with i show ?thesis by simp  nipkow@36755  860  next  nipkow@36755  861  case (Suc j) with i show ?thesis by auto  nipkow@36755  862  qed  nipkow@36755  863  qed  nipkow@36755  864 next  nipkow@36755  865  show "?B <= ?A" by auto  nipkow@36755  866 qed  nipkow@36755  867 nipkow@36755  868 lemma UN_le_add_shift:  nipkow@36755  869  "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B")  nipkow@36755  870 proof  nipkow@44890  871  show "?A <= ?B" by fastforce  nipkow@36755  872 next  nipkow@36755  873  show "?B <= ?A"  nipkow@36755  874  proof  nipkow@36755  875  fix x assume "x : ?B"  nipkow@36755  876  then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto  nipkow@36755  877  hence "i-k\n & x : M((i-k)+k)" by auto  nipkow@36755  878  thus "x : ?A" by blast  nipkow@36755  879  qed  nipkow@36755  880 qed  nipkow@36755  881 paulson@32596  882 lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)"  paulson@32596  883  by (auto simp add: atLeast0LessThan)  paulson@32596  884 paulson@32596  885 lemma UN_finite_subset: "(!!n::nat. (\i\{0.. C) \ (\n. A n) \ C"  paulson@32596  886  by (subst UN_UN_finite_eq [symmetric]) blast  paulson@32596  887 paulson@33044  888 lemma UN_finite2_subset:  paulson@33044  889  "(!!n::nat. (\i\{0.. (\i\{0.. (\n. A n) \ (\n. B n)"  paulson@33044  890  apply (rule UN_finite_subset)  paulson@33044  891  apply (subst UN_UN_finite_eq [symmetric, of B])  paulson@33044  892  apply blast  paulson@33044  893  done  paulson@32596  894 paulson@32596  895 lemma UN_finite2_eq:  paulson@33044  896  "(!!n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)"  paulson@33044  897  apply (rule subset_antisym)  paulson@33044  898  apply (rule UN_finite2_subset, blast)  paulson@33044  899  apply (rule UN_finite2_subset [where k=k])  huffman@35216  900  apply (force simp add: atLeastLessThan_add_Un [of 0])  paulson@33044  901  done  paulson@32596  902 paulson@32596  903 paulson@14485  904 subsubsection {* Cardinality *}  paulson@14485  905 nipkow@15045  906 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  945 apply(drule ex_bij_betw_finite_nat)  nipkow@31438  946 apply(drule ex_bij_betw_nat_finite)  nipkow@31438  947 apply(auto intro!:bij_betw_trans)  nipkow@31438  948 done  nipkow@31438  949 nipkow@31438  950 lemma ex_bij_betw_nat_finite_1:  nipkow@31438  951  "finite M \ \h. bij_betw h {1 .. card M} M"  nipkow@31438  952 by (rule finite_same_card_bij) auto  nipkow@31438  953 hoelzl@40703  954 lemma bij_betw_iff_card:  hoelzl@40703  955  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  956  shows BIJ: "(\f. bij_betw f A B) \ (card A = card B)"  hoelzl@40703  957 using assms  hoelzl@40703  958 proof(auto simp add: bij_betw_same_card)  hoelzl@40703  959  assume *: "card A = card B"  hoelzl@40703  960  obtain f where "bij_betw f A {0 ..< card A}"  hoelzl@40703  961  using FIN ex_bij_betw_finite_nat by blast  hoelzl@40703  962  moreover obtain g where "bij_betw g {0 ..< card B} B"  hoelzl@40703  963  using FIN' ex_bij_betw_nat_finite by blast  hoelzl@40703  964  ultimately have "bij_betw (g o f) A B"  hoelzl@40703  965  using * by (auto simp add: bij_betw_trans)  hoelzl@40703  966  thus "(\f. bij_betw f A B)" by blast  hoelzl@40703  967 qed  hoelzl@40703  968 hoelzl@40703  969 lemma inj_on_iff_card_le:  hoelzl@40703  970  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  971  shows "(\f. inj_on f A \ f  A \ B) = (card A \ card B)"  hoelzl@40703  972 proof (safe intro!: card_inj_on_le)  hoelzl@40703  973  assume *: "card A \ card B"  hoelzl@40703  974  obtain f where 1: "inj_on f A" and 2: "f  A = {0 ..< card A}"  hoelzl@40703  975  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force  hoelzl@40703  976  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g  {0 ..< card B} = B"  hoelzl@40703  977  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force  hoelzl@40703  978  ultimately have "inj_on g (f  A)" using subset_inj_on[of g _ "f  A"] * by force  hoelzl@40703  979  hence "inj_on (g o f) A" using 1 comp_inj_on by blast  hoelzl@40703  980  moreover  hoelzl@40703  981  {have "{0 ..< card A} \ {0 ..< card B}" using * by force  hoelzl@40703  982  with 2 have "f  A \ {0 ..< card B}" by blast  hoelzl@40703  983  hence "(g o f)  A \ B" unfolding comp_def using 3 by force  hoelzl@40703  984  }  hoelzl@40703  985  ultimately show "(\f. inj_on f A \ f  A \ B)" by blast  hoelzl@40703  986 qed (insert assms, auto)  nipkow@26105  987 paulson@14485  988 subsection {* Intervals of integers *}  paulson@14485  989 nipkow@15045  990 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l.. u ==>  nipkow@15045  1003  {(0::int).. u")  paulson@14485  1012  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1013  apply (rule finite_imageI)  paulson@14485  1014  apply auto  paulson@14485  1015  done  paulson@14485  1016 nipkow@15045  1017 lemma finite_atLeastLessThan_int [iff]: "finite {l.. u")  paulson@14485  1039  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  1040  apply (subst card_image)  paulson@14485  1041  apply (auto simp add: inj_on_def)  paulson@14485  1042  done  paulson@14485  1043 nipkow@15045  1044 lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}"  bulwahn@27656  1066 proof -  bulwahn@27656  1067  have "{k. P k \ k < i} \ {.. M"  bulwahn@27656  1073 shows "card {k \ M. k < Suc i} \ 0"  bulwahn@27656  1074 proof -  bulwahn@27656  1075  from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto  bulwahn@27656  1076  with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)  bulwahn@27656  1077 qed  bulwahn@27656  1078 bulwahn@27656  1079 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"  haftmann@37388  1080 apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"])  bulwahn@27656  1081 apply simp  nipkow@44890  1082 apply fastforce  bulwahn@27656  1083 apply auto  bulwahn@27656  1084 apply (rule inj_on_diff_nat)  bulwahn@27656  1085 apply auto  bulwahn@27656  1086 apply (case_tac x)  bulwahn@27656  1087 apply auto  bulwahn@27656  1088 apply (case_tac xa)  bulwahn@27656  1089 apply auto  bulwahn@27656  1090 apply (case_tac xa)  bulwahn@27656  1091 apply auto  bulwahn@27656  1092 done  bulwahn@27656  1093 bulwahn@27656  1094 lemma card_less_Suc:  bulwahn@27656  1095  assumes zero_in_M: "0 \ M"  bulwahn@27656  1096  shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"  bulwahn@27656  1097 proof -  bulwahn@27656  1098  from assms have a: "0 \ {k \ M. k < Suc i}" by simp  bulwahn@27656  1099  hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})"  bulwahn@27656  1100  by (auto simp only: insert_Diff)  bulwahn@27656  1101  have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto  bulwahn@27656  1102  from finite_M_bounded_by_nat[of "\x. x \ M" "Suc i"] have "Suc (card {k. Suc k \ M \ k < i}) = card (insert 0 ({k \ M. k < Suc i} - {0}))"  bulwahn@27656  1103  apply (subst card_insert)  bulwahn@27656  1104  apply simp_all  bulwahn@27656  1105  apply (subst b)  bulwahn@27656  1106  apply (subst card_less_Suc2[symmetric])  bulwahn@27656  1107  apply simp_all  bulwahn@27656  1108  done  bulwahn@27656  1109  with c show ?thesis by simp  bulwahn@27656  1110 qed  bulwahn@27656  1111 paulson@14485  1112 paulson@13850  1113 subsection {*Lemmas useful with the summation operator setsum*}  paulson@13850  1114 ballarin@16102  1115 text {* For examples, see Algebra/poly/UnivPoly2.thy *}  ballarin@13735  1116 wenzelm@14577  1117 subsubsection {* Disjoint Unions *}  ballarin@13735  1118 wenzelm@14577  1119 text {* Singletons and open intervals *}  ballarin@13735  1120 ballarin@13735  1121 lemma ivl_disj_un_singleton:  nipkow@15045  1122  "{l::'a::linorder} Un {l<..} = {l..}"  nipkow@15045  1123  "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  1127  "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  1136  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  1138  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  1140  "(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  1152  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  1154 by auto  ballarin@13735  1155 ballarin@13735  1156 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two  ballarin@13735  1157 wenzelm@14577  1158 subsubsection {* Disjoint Intersections *}  ballarin@13735  1159 wenzelm@14577  1160 text {* One- and two-sided intervals *}  ballarin@13735  1161 ballarin@13735  1162 lemma ivl_disj_int_one:  nipkow@15045  1163  "{..l::'a::order} Int {l<.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  1199 apply(auto simp:linorder_not_le)  nipkow@15542  1200 apply(rule ccontr)  nipkow@15542  1201 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  1202 apply(clarsimp simp:linorder_not_le)  nipkow@44890  1203 apply(fastforce)  nipkow@15542  1204 done  nipkow@15542  1205 nipkow@15041  1206 nipkow@15042  1207 subsection {* Summation indexed over intervals *}  nipkow@15042  1208 nipkow@15042  1209 syntax  nipkow@15042  1210  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  1211  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  1212  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@16052  1213  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  nipkow@15042  1214 syntax (xsymbols)  nipkow@15042  1215  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  1216  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  1217  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  1218  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15042  1219 syntax (HTML output)  nipkow@15042  1220  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  1221  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  1222  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  1223  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15056  1224 syntax (latex_sum output)  nipkow@15052  1225  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  1226  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@15052  1227  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  1228  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@16052  1229  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1230  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15052  1231  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1232  ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15041  1233 nipkow@15048  1234 translations  nipkow@28853  1235  "\x=a..b. t" == "CONST setsum (%x. t) {a..b}"  nipkow@28853  1236  "\x=a..i\n. t" == "CONST setsum (\i. t) {..n}"  nipkow@28853  1238  "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  1246 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  1248 @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \  nipkow@15542  1271  setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)"  nipkow@16052  1278 by (simp add:atMost_Suc add_ac)  nipkow@16052  1279 nipkow@16041  1280 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n"  nipkow@16041  1281 by (simp add:lessThan_Suc add_ac)  nipkow@15041  1282 nipkow@15911  1283 lemma setsum_cl_ivl_Suc[simp]:  nipkow@15561  1284  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  nipkow@15561  1285 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@15561  1286 nipkow@15911  1287 lemma setsum_op_ivl_Suc[simp]:  nipkow@15561  1288  "setsum f {m..  nipkow@15561  1292  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  nipkow@15561  1293 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@16041  1294 *)  nipkow@28068  1295 nipkow@28068  1296 lemma setsum_head:  nipkow@28068  1297  fixes n :: nat  nipkow@28068  1298  assumes mn: "m <= n"  nipkow@28068  1299  shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  nipkow@28068  1300 proof -  nipkow@28068  1301  from mn  nipkow@28068  1302  have "{m..n} = {m} \ {m<..n}"  nipkow@28068  1303  by (auto intro: ivl_disj_un_singleton)  nipkow@28068  1304  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  nipkow@28068  1305  by (simp add: atLeast0LessThan)  nipkow@28068  1306  also have "\ = ?rhs" by simp  nipkow@28068  1307  finally show ?thesis .  nipkow@28068  1308 qed  nipkow@28068  1309 nipkow@28068  1310 lemma setsum_head_Suc:  nipkow@28068  1311  "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}"  nipkow@28068  1312 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)  nipkow@28068  1313 nipkow@28068  1314 lemma setsum_head_upt_Suc:  nipkow@28068  1315  "m < n \ setsum f {m.. n + 1"  nipkow@31501  1321  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"  nipkow@31501  1322 proof-  nipkow@31501  1323  have "{m .. n+p} = {m..n} \ {n+1..n+p}" using m \ n+1 by auto  nipkow@31501  1324  thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint  nipkow@31501  1325  atLeastSucAtMost_greaterThanAtMost)  nipkow@31501  1326 qed  nipkow@28068  1327 nipkow@15539  1328 lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \  nipkow@15539  1329  setsum f {m.. 'a::ab_group_add"  nipkow@15539  1334 shows "\ m \ n; n \ p \ \  nipkow@15539  1335  setsum f {m.. ('a::ab_group_add)"  nipkow@31505  1342  shows "setsum (\k. f k - f(k + 1)) {(m::nat) .. n} =  nipkow@31505  1343  (if m <= n then f m - f(n + 1) else 0)"  nipkow@31505  1344 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)  nipkow@31505  1345 haftmann@44008  1346 lemma setsum_restrict_set':  haftmann@44008  1347  "finite A \ setsum f {x \ A. x \ B} = (\x\A. if x \ B then f x else 0)"  haftmann@44008  1348  by (simp add: setsum_restrict_set [symmetric] Int_def)  haftmann@44008  1349 haftmann@44008  1350 lemma setsum_restrict_set'':  haftmann@44008  1351  "finite A \ setsum f {x \ A. P x} = (\x\A. if P x then f x else 0)"  haftmann@44008  1352  by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq])  nipkow@31509  1353 nipkow@31509  1354 lemma setsum_setsum_restrict:  haftmann@44008  1355  "finite S \ finite T \  haftmann@44008  1356  setsum (\x. setsum (\y. f x y) {y. y \ T \ R x y}) S = setsum (\y. setsum (\x. f x y) {x. x \ S \ R x y}) T"  haftmann@44008  1357  by (simp add: setsum_restrict_set'') (rule setsum_commute)  nipkow@31509  1358 nipkow@31509  1359 lemma setsum_image_gen: assumes fS: "finite S"  nipkow@31509  1360  shows "setsum g S = setsum (\y. setsum g {x. x \ S \ f x = y}) (f  S)"  nipkow@31509  1361 proof-  nipkow@31509  1362  { fix x assume "x \ S" then have "{y. y\ fS \ f x = y} = {f x}" by auto }  nipkow@31509  1363  hence "setsum g S = setsum (\x. setsum (\y. g x) {y. y\ fS \ f x = y}) S"  nipkow@31509  1364  by simp  nipkow@31509  1365  also have "\ = setsum (\y. setsum g {x. x \ S \ f x = y}) (f  S)"  nipkow@31509  1366  by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]])  nipkow@31509  1367  finally show ?thesis .  nipkow@31509  1368 qed  nipkow@31509  1369 hoelzl@35171  1370 lemma setsum_le_included:  haftmann@36307  1371  fixes f :: "'a \ 'b::ordered_comm_monoid_add"  hoelzl@35171  1372  assumes "finite s" "finite t"  hoelzl@35171  1373  and "\y\t. 0 \ g y" "(\x\s. \y\t. i y = x \ f x \ g y)"  hoelzl@35171  1374  shows "setsum f s \ setsum g t"  hoelzl@35171  1375 proof -  hoelzl@35171  1376  have "setsum f s \ setsum (\y. setsum g {x. x\t \ i x = y}) s"  hoelzl@35171  1377  proof (rule setsum_mono)  hoelzl@35171  1378  fix y assume "y \ s"  hoelzl@35171  1379  with assms obtain z where z: "z \ t" "y = i z" "f y \ g z" by auto  hoelzl@35171  1380  with assms show "f y \ setsum g {x \ t. i x = y}" (is "?A y \ ?B y")  hoelzl@35171  1381  using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]  hoelzl@35171  1382  by (auto intro!: setsum_mono2)  hoelzl@35171  1383  qed  hoelzl@35171  1384  also have "... \ setsum (\y. setsum g {x. x\t \ i x = y}) (i  t)"  hoelzl@35171  1385  using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)  hoelzl@35171  1386  also have "... \ setsum g t"  hoelzl@35171  1387  using assms by (auto simp: setsum_image_gen[symmetric])  hoelzl@35171  1388  finally show ?thesis .  hoelzl@35171  1389 qed  hoelzl@35171  1390 nipkow@31509  1391 lemma setsum_multicount_gen:  nipkow@31509  1392  assumes "finite s" "finite t" "\j\t. (card {i\s. R i j} = k j)"  nipkow@31509  1393  shows "setsum (\i. (card {j\t. R i j})) s = setsum k t" (is "?l = ?r")  nipkow@31509  1394 proof-  nipkow@31509  1395  have "?l = setsum (\i. setsum (\x.1) {j\t. R i j}) s" by auto  nipkow@31509  1396  also have "\ = ?r" unfolding setsum_setsum_restrict[OF assms(1-2)]  nipkow@31509  1397  using assms(3) by auto  nipkow@31509  1398  finally show ?thesis .  nipkow@31509  1399 qed  nipkow@31509  1400 nipkow@31509  1401 lemma setsum_multicount:  nipkow@31509  1402  assumes "finite S" "finite T" "\j\T. (card {i\S. R i j} = k)"  nipkow@31509  1403  shows "setsum (\i. card {j\T. R i j}) S = k * card T" (is "?l = ?r")  nipkow@31509  1404 proof-  nipkow@31509  1405  have "?l = setsum (\i. k) T" by(rule setsum_multicount_gen)(auto simp:assms)  huffman@35216  1406  also have "\ = ?r" by(simp add: mult_commute)  nipkow@31509  1407  finally show ?thesis by auto  nipkow@31509  1408 qed  nipkow@31509  1409 nipkow@28068  1410 nipkow@16733  1411 subsection{* Shifting bounds *}  nipkow@16733  1412 nipkow@15539  1413 lemma setsum_shift_bounds_nat_ivl:  nipkow@15539  1414  "setsum f {m+k.. setsum f {Suc 0..k} = setsum f {0..k}"  nipkow@28068  1433 by(simp add:setsum_head_Suc)  kleing@19106  1434 nipkow@28068  1435 lemma setsum_shift_lb_Suc0_0_upt:  nipkow@28068  1436  "f(0::nat) = 0 \ setsum f {Suc 0.. 1"  haftmann@36307  1445  shows "(\i=0.. 0" by simp_all  haftmann@36307  1448  moreover have "(\i=0.. 0 have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp  haftmann@36350  1454  ultimately show ?case by (simp add: field_simps divide_inverse)  haftmann@36307  1455  qed  haftmann@36307  1456  ultimately show ?thesis by simp  haftmann@36307  1457 qed  haftmann@36307  1458 ballarin@17149  1459 kleing@19469  1460 subsection {* The formula for arithmetic sums *}  kleing@19469  1461 huffman@47222  1462 lemma gauss_sum:  huffman@47222  1463  "(2::'a::comm_semiring_1)*(\i\{1..n}. of_nat i) =  kleing@19469  1464  of_nat n*((of_nat n)+1)"  kleing@19469  1465 proof (induct n)  kleing@19469  1466  case 0  kleing@19469  1467  show ?case by simp  kleing@19469  1468 next  kleing@19469  1469  case (Suc n)  huffman@47222  1470  then show ?case  huffman@47222  1471  by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one)  huffman@47222  1472  (* FIXME: make numeral cancellation simprocs work for semirings *)  kleing@19469  1473 qed  kleing@19469  1474 kleing@19469  1475 theorem arith_series_general:  huffman@47222  1476  "(2::'a::comm_semiring_1) * (\i\{.. 1"  kleing@19469  1480  let ?I = "\i. of_nat i" and ?n = "of_nat n"  kleing@19469  1481  have  kleing@19469  1482  "(\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)"  huffman@30079  1495  by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)  huffman@23431  1496  (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]])  huffman@47222  1497  finally show ?thesis  huffman@47222  1498  unfolding mult_2 by (simp add: algebra_simps)  kleing@19469  1499 next  kleing@19469  1500  assume "\(n > 1)"  kleing@19469  1501  hence "n = 1 \ n = 0" by auto  huffman@47222  1502  thus ?thesis by (auto simp: mult_2)  kleing@19469  1503 qed  kleing@19469  1504 kleing@19469  1505 lemma arith_series_nat:  huffman@47222  1506  "(2::nat) * (\i\{..i\{..i\{..nat"  kleing@19022  1522  shows  kleing@19022  1523  "\x. Q x \ P x \  kleing@19022  1524  (\xxxxx 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1550  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1551  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10)  paulson@29960  1552  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10)  paulson@29960  1553 syntax (xsymbols)  paulson@29960  1554  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1555  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1556  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1557  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1558 syntax (HTML output)  paulson@29960  1559  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1560  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1561  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1562  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1563 syntax (latex_prod output)  paulson@29960  1564  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1565  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1566  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1567  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1568  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1569  ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1570  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1571  ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1572 paulson@29960  1573 translations  paulson@29960  1574  "\x=a..b. t" == "CONST setprod (%x. t) {a..b}"  paulson@29960  1575  "\x=a..i\n. t" == "CONST setprod (\i. t) {..n}"  paulson@29960  1577  "\ii. t) {..= 0 \ nat_set {x..y}"  haftmann@33318  1593  by (simp add: nat_set_def)  haftmann@33318  1594 haftmann@35644  1595 declare transfer_morphism_nat_int[transfer add  haftmann@33318  1596  return: transfer_nat_int_set_functions  haftmann@33318  1597  transfer_nat_int_set_function_closures  haftmann@33318  1598 ]  haftmann@33318  1599 haftmann@33318  1600 lemma transfer_int_nat_set_functions:  haftmann@33318  1601  "is_nat m \ is_nat n \ {m..n} = int  {nat m..nat n}"  haftmann@33318  1602  by (simp only: is_nat_def transfer_nat_int_set_functions  haftmann@33318  1603  transfer_nat_int_set_function_closures  haftmann@33318  1604  transfer_nat_int_set_return_embed nat_0_le  haftmann@33318  1605  cong: transfer_nat_int_set_cong)  haftmann@33318  1606 haftmann@33318  1607 lemma transfer_int_nat_set_function_closures:  haftmann@33318  1608  "is_nat x \ nat_set {x..y}"  haftmann@33318  1609  by (simp only: transfer_nat_int_set_function_closures is_nat_def)  haftmann@33318  1610 haftmann@35644  1611 declare transfer_morphism_int_nat[transfer add  haftmann@33318  1612  return: transfer_int_nat_set_functions  haftmann@33318  1613  transfer_int_nat_set_function_closures  haftmann@33318  1614 ]  haftmann@33318  1615 nipkow@8924  1616 end `