src/HOL/Set_Interval.thy
 author wenzelm Fri Mar 07 22:30:58 2014 +0100 (2014-03-07) changeset 55990 41c6b99c5fb7 parent 55719 cdddd073bff8 child 56193 c726ecfb22b6 permissions -rw-r--r--
more antiquotations;
 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 paulson@13850 178 subsection {*Two-sided intervals*} ballarin@13735 179 nipkow@24691 180 context ord nipkow@24691 181 begin nipkow@24691 182 blanchet@54147 183 lemma greaterThanLessThan_iff [simp]: 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}" wenzelm@53374 272 hence *: "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp wenzelm@53374 273 with {a..b} = {c} have "c \ a \ b \ c" by auto wenzelm@53374 274 with * 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@53216 376 context 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 haftmann@52729 455 lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \ x = bot" nipkow@51334 456 by (auto simp: set_eq_iff intro: le_bot) hoelzl@51328 457 haftmann@52729 458 lemma (in order_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@53216 522 fixes x y :: "'a :: {complete_lattice, 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: blanchet@55085 830 assumes "A \ {k.. A" by auto blanchet@55085 840 with insert have "A <= {k..i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B") nipkow@36755 854 proof nipkow@36755 855 show "?A <= ?B" nipkow@36755 856 proof nipkow@36755 857 fix x assume "x : ?A" nipkow@36755 858 then obtain i where i: "i\n" "x : M i" by auto nipkow@36755 859 show "x : ?B" nipkow@36755 860 proof(cases i) nipkow@36755 861 case 0 with i show ?thesis by simp nipkow@36755 862 next nipkow@36755 863 case (Suc j) with i show ?thesis by auto nipkow@36755 864 qed nipkow@36755 865 qed nipkow@36755 866 next nipkow@36755 867 show "?B <= ?A" by auto nipkow@36755 868 qed nipkow@36755 869 nipkow@36755 870 lemma UN_le_add_shift: nipkow@36755 871 "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B") nipkow@36755 872 proof nipkow@44890 873 show "?A <= ?B" by fastforce nipkow@36755 874 next nipkow@36755 875 show "?B <= ?A" nipkow@36755 876 proof nipkow@36755 877 fix x assume "x : ?B" nipkow@36755 878 then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto nipkow@36755 879 hence "i-k\n & x : M((i-k)+k)" by auto nipkow@36755 880 thus "x : ?A" by blast nipkow@36755 881 qed nipkow@36755 882 qed nipkow@36755 883 paulson@32596 884 lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)" paulson@32596 885 by (auto simp add: atLeast0LessThan) paulson@32596 886 paulson@32596 887 lemma UN_finite_subset: "(!!n::nat. (\i\{0.. C) \ (\n. A n) \ C" paulson@32596 888 by (subst UN_UN_finite_eq [symmetric]) blast paulson@32596 889 paulson@33044 890 lemma UN_finite2_subset: paulson@33044 891 "(!!n::nat. (\i\{0.. (\i\{0.. (\n. A n) \ (\n. B n)" paulson@33044 892 apply (rule UN_finite_subset) paulson@33044 893 apply (subst UN_UN_finite_eq [symmetric, of B]) paulson@33044 894 apply blast paulson@33044 895 done paulson@32596 896 paulson@32596 897 lemma UN_finite2_eq: paulson@33044 898 "(!!n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)" paulson@33044 899 apply (rule subset_antisym) paulson@33044 900 apply (rule UN_finite2_subset, blast) paulson@33044 901 apply (rule UN_finite2_subset [where k=k]) huffman@35216 902 apply (force simp add: atLeastLessThan_add_Un [of 0]) paulson@33044 903 done paulson@32596 904 paulson@32596 905 paulson@14485 906 subsubsection {* Cardinality *} paulson@14485 907 nipkow@15045 908 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 947 apply(drule ex_bij_betw_finite_nat) nipkow@31438 948 apply(drule ex_bij_betw_nat_finite) nipkow@31438 949 apply(auto intro!:bij_betw_trans) nipkow@31438 950 done nipkow@31438 951 nipkow@31438 952 lemma ex_bij_betw_nat_finite_1: nipkow@31438 953 "finite M \ \h. bij_betw h {1 .. card M} M" nipkow@31438 954 by (rule finite_same_card_bij) auto nipkow@31438 955 hoelzl@40703 956 lemma bij_betw_iff_card: hoelzl@40703 957 assumes FIN: "finite A" and FIN': "finite B" hoelzl@40703 958 shows BIJ: "(\f. bij_betw f A B) \ (card A = card B)" hoelzl@40703 959 using assms hoelzl@40703 960 proof(auto simp add: bij_betw_same_card) hoelzl@40703 961 assume *: "card A = card B" hoelzl@40703 962 obtain f where "bij_betw f A {0 ..< card A}" hoelzl@40703 963 using FIN ex_bij_betw_finite_nat by blast hoelzl@40703 964 moreover obtain g where "bij_betw g {0 ..< card B} B" hoelzl@40703 965 using FIN' ex_bij_betw_nat_finite by blast hoelzl@40703 966 ultimately have "bij_betw (g o f) A B" hoelzl@40703 967 using * by (auto simp add: bij_betw_trans) hoelzl@40703 968 thus "(\f. bij_betw f A B)" by blast hoelzl@40703 969 qed hoelzl@40703 970 hoelzl@40703 971 lemma inj_on_iff_card_le: hoelzl@40703 972 assumes FIN: "finite A" and FIN': "finite B" hoelzl@40703 973 shows "(\f. inj_on f A \ f  A \ B) = (card A \ card B)" hoelzl@40703 974 proof (safe intro!: card_inj_on_le) hoelzl@40703 975 assume *: "card A \ card B" hoelzl@40703 976 obtain f where 1: "inj_on f A" and 2: "f  A = {0 ..< card A}" hoelzl@40703 977 using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force hoelzl@40703 978 moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g  {0 ..< card B} = B" hoelzl@40703 979 using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force hoelzl@40703 980 ultimately have "inj_on g (f  A)" using subset_inj_on[of g _ "f  A"] * by force hoelzl@40703 981 hence "inj_on (g o f) A" using 1 comp_inj_on by blast hoelzl@40703 982 moreover hoelzl@40703 983 {have "{0 ..< card A} \ {0 ..< card B}" using * by force hoelzl@40703 984 with 2 have "f  A \ {0 ..< card B}" by blast hoelzl@40703 985 hence "(g o f)  A \ B" unfolding comp_def using 3 by force hoelzl@40703 986 } hoelzl@40703 987 ultimately show "(\f. inj_on f A \ f  A \ B)" by blast hoelzl@40703 988 qed (insert assms, auto) nipkow@26105 989 paulson@14485 990 subsection {* Intervals of integers *} paulson@14485 991 nipkow@15045 992 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l.. u ==> nipkow@15045 1005 {(0::int).. u") paulson@14485 1014 apply (subst image_atLeastZeroLessThan_int, assumption) paulson@14485 1015 apply (rule finite_imageI) paulson@14485 1016 apply auto paulson@14485 1017 done paulson@14485 1018 nipkow@15045 1019 lemma finite_atLeastLessThan_int [iff]: "finite {l.. u") paulson@14485 1041 apply (subst image_atLeastZeroLessThan_int, assumption) paulson@14485 1042 apply (subst card_image) paulson@14485 1043 apply (auto simp add: inj_on_def) paulson@14485 1044 done paulson@14485 1045 nipkow@15045 1046 lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}" bulwahn@27656 1068 proof - bulwahn@27656 1069 have "{k. P k \ k < i} \ {.. M" bulwahn@27656 1075 shows "card {k \ M. k < Suc i} \ 0" bulwahn@27656 1076 proof - bulwahn@27656 1077 from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto bulwahn@27656 1078 with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff) bulwahn@27656 1079 qed bulwahn@27656 1080 bulwahn@27656 1081 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}" haftmann@37388 1082 apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"]) bulwahn@27656 1083 apply simp nipkow@44890 1084 apply fastforce bulwahn@27656 1085 apply auto bulwahn@27656 1086 apply (rule inj_on_diff_nat) bulwahn@27656 1087 apply auto bulwahn@27656 1088 apply (case_tac x) bulwahn@27656 1089 apply auto bulwahn@27656 1090 apply (case_tac xa) bulwahn@27656 1091 apply auto bulwahn@27656 1092 apply (case_tac xa) bulwahn@27656 1093 apply auto bulwahn@27656 1094 done bulwahn@27656 1095 bulwahn@27656 1096 lemma card_less_Suc: bulwahn@27656 1097 assumes zero_in_M: "0 \ M" bulwahn@27656 1098 shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}" bulwahn@27656 1099 proof - bulwahn@27656 1100 from assms have a: "0 \ {k \ M. k < Suc i}" by simp bulwahn@27656 1101 hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})" bulwahn@27656 1102 by (auto simp only: insert_Diff) bulwahn@27656 1103 have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto bulwahn@27656 1104 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 1105 apply (subst card_insert) bulwahn@27656 1106 apply simp_all bulwahn@27656 1107 apply (subst b) bulwahn@27656 1108 apply (subst card_less_Suc2[symmetric]) bulwahn@27656 1109 apply simp_all bulwahn@27656 1110 done bulwahn@27656 1111 with c show ?thesis by simp bulwahn@27656 1112 qed bulwahn@27656 1113 paulson@14485 1114 paulson@13850 1115 subsection {*Lemmas useful with the summation operator setsum*} paulson@13850 1116 ballarin@16102 1117 text {* For examples, see Algebra/poly/UnivPoly2.thy *} ballarin@13735 1118 wenzelm@14577 1119 subsubsection {* Disjoint Unions *} ballarin@13735 1120 wenzelm@14577 1121 text {* Singletons and open intervals *} ballarin@13735 1122 ballarin@13735 1123 lemma ivl_disj_un_singleton: nipkow@15045 1124 "{l::'a::linorder} Un {l<..} = {l..}" nipkow@15045 1125 "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}" nipkow@15045 1129 "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}" nipkow@15045 1138 "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}" nipkow@15045 1140 "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}" nipkow@15045 1142 "(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 1154 "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}" ballarin@14398 1156 by auto ballarin@13735 1157 ballarin@13735 1158 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ballarin@13735 1159 wenzelm@14577 1160 subsubsection {* Disjoint Intersections *} ballarin@13735 1161 wenzelm@14577 1162 text {* One- and two-sided intervals *} ballarin@13735 1163 ballarin@13735 1164 lemma ivl_disj_int_one: nipkow@15045 1165 "{..l::'a::order} Int {l<.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))" nipkow@15542 1201 apply(auto simp:linorder_not_le) nipkow@15542 1202 apply(rule ccontr) nipkow@15542 1203 apply(insert linorder_le_less_linear[of i n]) nipkow@15542 1204 apply(clarsimp simp:linorder_not_le) nipkow@44890 1205 apply(fastforce) nipkow@15542 1206 done nipkow@15542 1207 nipkow@15041 1208 nipkow@15042 1209 subsection {* Summation indexed over intervals *} nipkow@15042 1210 nipkow@15042 1211 syntax nipkow@15042 1212 "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) nipkow@15048 1213 "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) nipkow@16052 1214 "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10) nipkow@16052 1215 "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10) nipkow@15042 1216 syntax (xsymbols) nipkow@15042 1217 "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) nipkow@15048 1218 "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) nipkow@16052 1219 "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) nipkow@16052 1220 "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) nipkow@15042 1221 syntax (HTML output) nipkow@15042 1222 "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) nipkow@15048 1223 "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) nipkow@16052 1224 "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) nipkow@16052 1225 "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) nipkow@15056 1226 syntax (latex_sum output) nipkow@15052 1227 "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" nipkow@15052 1228 ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) nipkow@15052 1229 "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" nipkow@15052 1230 ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) nipkow@16052 1231 "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" nipkow@16052 1232 ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10) nipkow@15052 1233 "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" nipkow@16052 1234 ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10) nipkow@15041 1235 nipkow@15048 1236 translations nipkow@28853 1237 "\x=a..b. t" == "CONST setsum (%x. t) {a..b}" nipkow@28853 1238 "\x=a..i\n. t" == "CONST setsum (\i. t) {..n}" nipkow@28853 1240 "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\ nipkow@15056 1248 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\ nipkow@15056 1250 @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \ nipkow@15542 1273 setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)" nipkow@16052 1280 by (simp add:atMost_Suc add_ac) nipkow@16052 1281 nipkow@16041 1282 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n" nipkow@16041 1283 by (simp add:lessThan_Suc add_ac) nipkow@15041 1284 nipkow@15911 1285 lemma setsum_cl_ivl_Suc[simp]: nipkow@15561 1286 "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))" nipkow@15561 1287 by (auto simp:add_ac atLeastAtMostSuc_conv) nipkow@15561 1288 nipkow@15911 1289 lemma setsum_op_ivl_Suc[simp]: nipkow@15561 1290 "setsum f {m.. nipkow@15561 1294 (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)" nipkow@15561 1295 by (auto simp:add_ac atLeastAtMostSuc_conv) nipkow@16041 1296 *) nipkow@28068 1297 nipkow@28068 1298 lemma setsum_head: nipkow@28068 1299 fixes n :: nat nipkow@28068 1300 assumes mn: "m <= n" nipkow@28068 1301 shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs") nipkow@28068 1302 proof - nipkow@28068 1303 from mn nipkow@28068 1304 have "{m..n} = {m} \ {m<..n}" nipkow@28068 1305 by (auto intro: ivl_disj_un_singleton) nipkow@28068 1306 hence "?lhs = (\x\{m} \ {m<..n}. P x)" nipkow@28068 1307 by (simp add: atLeast0LessThan) nipkow@28068 1308 also have "\ = ?rhs" by simp nipkow@28068 1309 finally show ?thesis . nipkow@28068 1310 qed nipkow@28068 1311 nipkow@28068 1312 lemma setsum_head_Suc: nipkow@28068 1313 "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}" nipkow@28068 1314 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) nipkow@28068 1315 nipkow@28068 1316 lemma setsum_head_upt_Suc: nipkow@28068 1317 "m < n \ setsum f {m.. n + 1" nipkow@31501 1323 shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}" nipkow@31501 1324 proof- nipkow@31501 1325 have "{m .. n+p} = {m..n} \ {n+1..n+p}" using m \ n+1 by auto nipkow@31501 1326 thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint nipkow@31501 1327 atLeastSucAtMost_greaterThanAtMost) nipkow@31501 1328 qed nipkow@28068 1329 nipkow@15539 1330 lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \ nipkow@15539 1331 setsum f {m.. 'a::ab_group_add" nipkow@15539 1336 shows "\ m \ n; n \ p \ \ nipkow@15539 1337 setsum f {m.. ('a::ab_group_add)" nipkow@31505 1344 shows "setsum (\k. f k - f(k + 1)) {(m::nat) .. n} = nipkow@31505 1345 (if m <= n then f m - f(n + 1) else 0)" nipkow@31505 1346 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) nipkow@31505 1347 haftmann@44008 1348 lemma setsum_restrict_set': haftmann@44008 1349 "finite A \ setsum f {x \ A. x \ B} = (\x\A. if x \ B then f x else 0)" haftmann@44008 1350 by (simp add: setsum_restrict_set [symmetric] Int_def) haftmann@44008 1351 haftmann@44008 1352 lemma setsum_restrict_set'': haftmann@44008 1353 "finite A \ setsum f {x \ A. P x} = (\x\A. if P x then f x else 0)" haftmann@44008 1354 by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq]) nipkow@31509 1355 nipkow@31509 1356 lemma setsum_setsum_restrict: haftmann@44008 1357 "finite S \ finite T \ haftmann@44008 1358 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 1359 by (simp add: setsum_restrict_set'') (rule setsum_commute) nipkow@31509 1360 nipkow@31509 1361 lemma setsum_image_gen: assumes fS: "finite S" nipkow@31509 1362 shows "setsum g S = setsum (\y. setsum g {x. x \ S \ f x = y}) (f  S)" nipkow@31509 1363 proof- nipkow@31509 1364 { fix x assume "x \ S" then have "{y. y\ fS \ f x = y} = {f x}" by auto } nipkow@31509 1365 hence "setsum g S = setsum (\x. setsum (\y. g x) {y. y\ fS \ f x = y}) S" nipkow@31509 1366 by simp nipkow@31509 1367 also have "\ = setsum (\y. setsum g {x. x \ S \ f x = y}) (f  S)" nipkow@31509 1368 by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]]) nipkow@31509 1369 finally show ?thesis . nipkow@31509 1370 qed nipkow@31509 1371 hoelzl@35171 1372 lemma setsum_le_included: haftmann@36307 1373 fixes f :: "'a \ 'b::ordered_comm_monoid_add" hoelzl@35171 1374 assumes "finite s" "finite t" hoelzl@35171 1375 and "\y\t. 0 \ g y" "(\x\s. \y\t. i y = x \ f x \ g y)" hoelzl@35171 1376 shows "setsum f s \ setsum g t" hoelzl@35171 1377 proof - hoelzl@35171 1378 have "setsum f s \ setsum (\y. setsum g {x. x\t \ i x = y}) s" hoelzl@35171 1379 proof (rule setsum_mono) hoelzl@35171 1380 fix y assume "y \ s" hoelzl@35171 1381 with assms obtain z where z: "z \ t" "y = i z" "f y \ g z" by auto hoelzl@35171 1382 with assms show "f y \ setsum g {x \ t. i x = y}" (is "?A y \ ?B y") hoelzl@35171 1383 using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro] hoelzl@35171 1384 by (auto intro!: setsum_mono2) hoelzl@35171 1385 qed hoelzl@35171 1386 also have "... \ setsum (\y. setsum g {x. x\t \ i x = y}) (i  t)" hoelzl@35171 1387 using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg) hoelzl@35171 1388 also have "... \ setsum g t" hoelzl@35171 1389 using assms by (auto simp: setsum_image_gen[symmetric]) hoelzl@35171 1390 finally show ?thesis . hoelzl@35171 1391 qed hoelzl@35171 1392 nipkow@31509 1393 lemma setsum_multicount_gen: nipkow@31509 1394 assumes "finite s" "finite t" "\j\t. (card {i\s. R i j} = k j)" nipkow@31509 1395 shows "setsum (\i. (card {j\t. R i j})) s = setsum k t" (is "?l = ?r") nipkow@31509 1396 proof- nipkow@31509 1397 have "?l = setsum (\i. setsum (\x.1) {j\t. R i j}) s" by auto nipkow@31509 1398 also have "\ = ?r" unfolding setsum_setsum_restrict[OF assms(1-2)] nipkow@31509 1399 using assms(3) by auto nipkow@31509 1400 finally show ?thesis . nipkow@31509 1401 qed nipkow@31509 1402 nipkow@31509 1403 lemma setsum_multicount: nipkow@31509 1404 assumes "finite S" "finite T" "\j\T. (card {i\S. R i j} = k)" nipkow@31509 1405 shows "setsum (\i. card {j\T. R i j}) S = k * card T" (is "?l = ?r") nipkow@31509 1406 proof- nipkow@31509 1407 have "?l = setsum (\i. k) T" by(rule setsum_multicount_gen)(auto simp:assms) huffman@35216 1408 also have "\ = ?r" by(simp add: mult_commute) nipkow@31509 1409 finally show ?thesis by auto nipkow@31509 1410 qed nipkow@31509 1411 nipkow@28068 1412 nipkow@16733 1413 subsection{* Shifting bounds *} nipkow@16733 1414 nipkow@15539 1415 lemma setsum_shift_bounds_nat_ivl: nipkow@15539 1416 "setsum f {m+k.. setsum f {Suc 0..k} = setsum f {0..k}" nipkow@28068 1435 by(simp add:setsum_head_Suc) kleing@19106 1436 nipkow@28068 1437 lemma setsum_shift_lb_Suc0_0_upt: nipkow@28068 1438 "f(0::nat) = 0 \ setsum f {Suc 0.. 'a::comm_monoid_add" haftmann@52380 1445 shows "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))" haftmann@52380 1446 proof (induct n) haftmann@52380 1447 case 0 show ?case by simp haftmann@52380 1448 next haftmann@52380 1449 case (Suc n) note IH = this haftmann@52380 1450 have "(\i\Suc (Suc n). f i) = (\i\Suc n. f i) + f (Suc (Suc n))" haftmann@52380 1451 by (rule setsum_atMost_Suc) haftmann@52380 1452 also have "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))" haftmann@52380 1453 by (rule IH) haftmann@52380 1454 also have "f 0 + (\i\n. f (Suc i)) + f (Suc (Suc n)) = haftmann@52380 1455 f 0 + ((\i\n. f (Suc i)) + f (Suc (Suc n)))" haftmann@52380 1456 by (rule add_assoc) haftmann@52380 1457 also have "(\i\n. f (Suc i)) + f (Suc (Suc n)) = (\i\Suc n. f (Suc i))" haftmann@52380 1458 by (rule setsum_atMost_Suc [symmetric]) haftmann@52380 1459 finally show ?case . haftmann@52380 1460 qed haftmann@52380 1461 lp15@55718 1462 lemma setsum_last_plus: "n \ 0 \ (\i = 0..n. f i) = f n + (\i = 0..n - Suc 0. f i)" lp15@55718 1463 using atLeastAtMostSuc_conv [of 0 "n - 1"] lp15@55718 1464 by auto lp15@55718 1465 lp15@55718 1466 lemma nested_setsum_swap: lp15@55718 1467 "(\i = 0..n. (\j = 0..j = 0..i = Suc j..n. a i j)" lp15@55718 1468 by (induction n) (auto simp: setsum_addf) lp15@55718 1469 haftmann@52380 1470 ballarin@17149 1471 subsection {* The formula for geometric sums *} ballarin@17149 1472 ballarin@17149 1473 lemma geometric_sum: haftmann@36307 1474 assumes "x \ 1" haftmann@36307 1475 shows "(\i=0.. 0" by simp_all haftmann@36307 1478 moreover have "(\i=0.. 0 have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp haftmann@36350 1484 ultimately show ?case by (simp add: field_simps divide_inverse) haftmann@36307 1485 qed haftmann@36307 1486 ultimately show ?thesis by simp haftmann@36307 1487 qed haftmann@36307 1488 ballarin@17149 1489 kleing@19469 1490 subsection {* The formula for arithmetic sums *} kleing@19469 1491 huffman@47222 1492 lemma gauss_sum: huffman@47222 1493 "(2::'a::comm_semiring_1)*(\i\{1..n}. of_nat i) = kleing@19469 1494 of_nat n*((of_nat n)+1)" kleing@19469 1495 proof (induct n) kleing@19469 1496 case 0 kleing@19469 1497 show ?case by simp kleing@19469 1498 next kleing@19469 1499 case (Suc n) huffman@47222 1500 then show ?case huffman@47222 1501 by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one) huffman@47222 1502 (* FIXME: make numeral cancellation simprocs work for semirings *) kleing@19469 1503 qed kleing@19469 1504 kleing@19469 1505 theorem arith_series_general: huffman@47222 1506 "(2::'a::comm_semiring_1) * (\i\{.. 1" kleing@19469 1510 let ?I = "\i. of_nat i" and ?n = "of_nat n" kleing@19469 1511 have kleing@19469 1512 "(\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 1525 by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def) huffman@23431 1526 (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]]) huffman@47222 1527 finally show ?thesis huffman@47222 1528 unfolding mult_2 by (simp add: algebra_simps) kleing@19469 1529 next kleing@19469 1530 assume "\(n > 1)" kleing@19469 1531 hence "n = 1 \ n = 0" by auto huffman@47222 1532 thus ?thesis by (auto simp: mult_2) kleing@19469 1533 qed kleing@19469 1534 kleing@19469 1535 lemma arith_series_nat: huffman@47222 1536 "(2::nat) * (\i\{..i\{..i\{..nat" kleing@19022 1552 shows kleing@19022 1553 "\x. Q x \ P x \ kleing@19022 1554 (\xxxxxi=0..i=0.. 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10) paulson@29960 1588 "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10) paulson@29960 1589 "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10) paulson@29960 1590 "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10) paulson@29960 1591 syntax (xsymbols) paulson@29960 1592 "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) paulson@29960 1593 "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) paulson@29960 1594 "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) paulson@29960 1595 "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) paulson@29960 1596 syntax (HTML output) paulson@29960 1597 "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) paulson@29960 1598 "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) paulson@29960 1599 "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) paulson@29960 1600 "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) paulson@29960 1601 syntax (latex_prod output) paulson@29960 1602 "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" paulson@29960 1603 ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) paulson@29960 1604 "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" paulson@29960 1605 ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) paulson@29960 1606 "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" paulson@29960 1607 ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10) paulson@29960 1608 "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" paulson@29960 1609 ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10) paulson@29960 1610 paulson@29960 1611 translations paulson@29960 1612 "\x=a..b. t" == "CONST setprod (%x. t) {a..b}" paulson@29960 1613 "\x=a..i\n. t" == "CONST setprod (\i. t) {..n}" paulson@29960 1615 "\ii. t) {..= 0 \ nat_set {x..y}" haftmann@33318 1631 by (simp add: nat_set_def) haftmann@33318 1632 haftmann@35644 1633 declare transfer_morphism_nat_int[transfer add haftmann@33318 1634 return: transfer_nat_int_set_functions haftmann@33318 1635 transfer_nat_int_set_function_closures haftmann@33318 1636 ] haftmann@33318 1637 haftmann@33318 1638 lemma transfer_int_nat_set_functions: haftmann@33318 1639 "is_nat m \ is_nat n \ {m..n} = int ` {nat m..nat n}" haftmann@33318 1640 by (simp only: is_nat_def transfer_nat_int_set_functions haftmann@33318 1641 transfer_nat_int_set_function_closures haftmann@33318 1642 transfer_nat_int_set_return_embed nat_0_le haftmann@33318 1643 cong: transfer_nat_int_set_cong) haftmann@33318 1644 haftmann@33318 1645 lemma transfer_int_nat_set_function_closures: haftmann@33318 1646 "is_nat x \ nat_set {x..y}" haftmann@33318 1647 by (simp only: transfer_nat_int_set_function_closures is_nat_def) haftmann@33318 1648 haftmann@35644 1649 declare transfer_morphism_int_nat[transfer add haftmann@33318 1650 return: transfer_int_nat_set_functions haftmann@33318 1651 transfer_int_nat_set_function_closures haftmann@33318 1652 ] haftmann@33318 1653 lp15@55242 1654 lemma setprod_int_plus_eq: "setprod int {i..i+j} = \{int i..int (i+j)}" lp15@55242 1655 by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv) lp15@55242 1656 lp15@55242 1657 lemma setprod_int_eq: "setprod int {i..j} = \{int i..int j}" lp15@55242 1658 proof (cases "i \ j") lp15@55242 1659 case True lp15@55242 1660 then show ?thesis lp15@55242 1661 by (metis Nat.le_iff_add setprod_int_plus_eq) lp15@55242 1662 next lp15@55242 1663 case False lp15@55242 1664 then show ?thesis lp15@55242 1665 by auto lp15@55242 1666 qed lp15@55242 1667 lp15@55718 1668 lemma setprod_power_distrib: lp15@55718 1669 fixes f :: "'a \ 'b::comm_semiring_1" lp15@55719 1670 shows "setprod f A ^ n = setprod (\x. (f x)^n) A" lp15@55719 1671 proof (cases "finite A") lp15@55719 1672 case True then show ?thesis lp15@55719 1673 by (induct A rule: finite_induct) (auto simp add: power_mult_distrib) lp15@55719 1674 next lp15@55719 1675 case False then show ?thesis lp15@55719 1676 by (metis setprod_infinite power_one) lp15@55719 1677 qed lp15@55718 1678 nipkow@8924 1679 end