1(* Title: HOL/Set_Interval.thy 2 Author: Tobias Nipkow, Clemens Ballarin, Jeremy Avigad 3 4lessThan, greaterThan, atLeast, atMost and two-sided intervals 5 6Modern convention: Ixy stands for an interval where x and y 7describe the lower and upper bound and x,y : {c,o,i} 8where c = closed, o = open, i = infinite. 9Examples: Ico = {_ ..< _} and Ici = {_ ..} 10*) 11 12section \<open>Set intervals\<close> 13 14theory Set_Interval 15imports Divides 16begin 17 18(* Belongs in Finite_Set but 2 is not available there *) 19lemma card_2_iff: "card S = 2 \<longleftrightarrow> (\<exists>x y. S = {x,y} \<and> x \<noteq> y)" 20 by (auto simp: card_Suc_eq numeral_eq_Suc) 21 22lemma card_2_iff': "card S = 2 \<longleftrightarrow> (\<exists>x\<in>S. \<exists>y\<in>S. x \<noteq> y \<and> (\<forall>z\<in>S. z = x \<or> z = y))" 23 by (auto simp: card_Suc_eq numeral_eq_Suc) 24 25context ord 26begin 27 28definition 29 lessThan :: "'a => 'a set" ("(1{..<_})") where 30 "{..<u} == {x. x < u}" 31 32definition 33 atMost :: "'a => 'a set" ("(1{.._})") where 34 "{..u} == {x. x \<le> u}" 35 36definition 37 greaterThan :: "'a => 'a set" ("(1{_<..})") where 38 "{l<..} == {x. l<x}" 39 40definition 41 atLeast :: "'a => 'a set" ("(1{_..})") where 42 "{l..} == {x. l\<le>x}" 43 44definition 45 greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where 46 "{l<..<u} == {l<..} Int {..<u}" 47 48definition 49 atLeastLessThan :: "'a => 'a => 'a set" ("(1{_..<_})") where 50 "{l..<u} == {l..} Int {..<u}" 51 52definition 53 greaterThanAtMost :: "'a => 'a => 'a set" ("(1{_<.._})") where 54 "{l<..u} == {l<..} Int {..u}" 55 56definition 57 atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where 58 "{l..u} == {l..} Int {..u}" 59 60end 61 62 63text\<open>A note of warning when using \<^term>\<open>{..<n}\<close> on type \<^typ>\<open>nat\<close>: it is equivalent to \<^term>\<open>{0::nat..<n}\<close> but some lemmas involving 64\<^term>\<open>{m..<n}\<close> may not exist in \<^term>\<open>{..<n}\<close>-form as well.\<close> 65 66syntax (ASCII) 67 "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10) 68 "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" [0, 0, 10] 10) 69 "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" [0, 0, 10] 10) 70 "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10) 71 72syntax (latex output) 73 "_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>_ \<le> _)/ _)" [0, 0, 10] 10) 74 "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>_ < _)/ _)" [0, 0, 10] 10) 75 "_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(\<open>unbreakable\<close>_ \<le> _)/ _)" [0, 0, 10] 10) 76 "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(\<open>unbreakable\<close>_ < _)/ _)" [0, 0, 10] 10) 77 78syntax 79 "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10) 80 "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_<_./ _)" [0, 0, 10] 10) 81 "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10) 82 "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_<_./ _)" [0, 0, 10] 10) 83 84translations 85 "\<Union>i\<le>n. A" \<rightleftharpoons> "\<Union>i\<in>{..n}. A" 86 "\<Union>i<n. A" \<rightleftharpoons> "\<Union>i\<in>{..<n}. A" 87 "\<Inter>i\<le>n. A" \<rightleftharpoons> "\<Inter>i\<in>{..n}. A" 88 "\<Inter>i<n. A" \<rightleftharpoons> "\<Inter>i\<in>{..<n}. A" 89 90 91subsection \<open>Various equivalences\<close> 92 93lemma (in ord) lessThan_iff [iff]: "(i \<in> lessThan k) = (i<k)" 94by (simp add: lessThan_def) 95 96lemma Compl_lessThan [simp]: 97 "!!k:: 'a::linorder. -lessThan k = atLeast k" 98 by (auto simp add: lessThan_def atLeast_def) 99 100lemma single_Diff_lessThan [simp]: "!!k:: 'a::preorder. {k} - lessThan k = {k}" 101 by auto 102 103lemma (in ord) greaterThan_iff [iff]: "(i \<in> greaterThan k) = (k<i)" 104 by (simp add: greaterThan_def) 105 106lemma Compl_greaterThan [simp]: 107 "!!k:: 'a::linorder. -greaterThan k = atMost k" 108 by (auto simp add: greaterThan_def atMost_def) 109 110lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k" 111 apply (subst Compl_greaterThan [symmetric]) 112 apply (rule double_complement) 113 done 114 115lemma (in ord) atLeast_iff [iff]: "(i \<in> atLeast k) = (k<=i)" 116by (simp add: atLeast_def) 117 118lemma Compl_atLeast [simp]: "!!k:: 'a::linorder. -atLeast k = lessThan k" 119 by (auto simp add: lessThan_def atLeast_def) 120 121lemma (in ord) atMost_iff [iff]: "(i \<in> atMost k) = (i<=k)" 122by (simp add: atMost_def) 123 124lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" 125by (blast intro: order_antisym) 126 127lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \<inter> { b <..} = { max a b <..}" 128 by auto 129 130lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \<inter> {..< b} = {..< min a b}" 131 by auto 132 133subsection \<open>Logical Equivalences for Set Inclusion and Equality\<close> 134 135lemma atLeast_empty_triv [simp]: "{{}..} = UNIV" 136 by auto 137 138lemma atMost_UNIV_triv [simp]: "{..UNIV} = UNIV" 139 by auto 140 141lemma atLeast_subset_iff [iff]: 142 "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::preorder))" 143by (blast intro: order_trans) 144 145lemma atLeast_eq_iff [iff]: 146 "(atLeast x = atLeast y) = (x = (y::'a::order))" 147by (blast intro: order_antisym order_trans) 148 149lemma greaterThan_subset_iff [iff]: 150 "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" 151 unfolding greaterThan_def by (auto simp: linorder_not_less [symmetric]) 152 153lemma greaterThan_eq_iff [iff]: 154 "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" 155 by (auto simp: elim!: equalityE) 156 157lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::preorder))" 158 by (blast intro: order_trans) 159 160lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::order))" 161 by (blast intro: order_antisym order_trans) 162 163lemma lessThan_subset_iff [iff]: 164 "(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" 165 unfolding lessThan_def by (auto simp: linorder_not_less [symmetric]) 166 167lemma lessThan_eq_iff [iff]: 168 "(lessThan x = lessThan y) = (x = (y::'a::linorder))" 169 by (auto simp: elim!: equalityE) 170 171lemma lessThan_strict_subset_iff: 172 fixes m n :: "'a::linorder" 173 shows "{..<m} < {..<n} \<longleftrightarrow> m < n" 174 by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq) 175 176lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \<subseteq> {b <..} \<longleftrightarrow> b < a" 177 by auto 178 179lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \<subseteq> {..< b} \<longleftrightarrow> a < b" 180 by auto 181 182lemma (in preorder) Ioi_le_Ico: "{a <..} \<subseteq> {a ..}" 183 by (auto intro: less_imp_le) 184 185subsection \<open>Two-sided intervals\<close> 186 187context ord 188begin 189 190lemma greaterThanLessThan_iff [simp]: "(i \<in> {l<..<u}) = (l < i \<and> i < u)" 191 by (simp add: greaterThanLessThan_def) 192 193lemma atLeastLessThan_iff [simp]: "(i \<in> {l..<u}) = (l \<le> i \<and> i < u)" 194 by (simp add: atLeastLessThan_def) 195 196lemma greaterThanAtMost_iff [simp]: "(i \<in> {l<..u}) = (l < i \<and> i \<le> u)" 197 by (simp add: greaterThanAtMost_def) 198 199lemma atLeastAtMost_iff [simp]: "(i \<in> {l..u}) = (l \<le> i \<and> i \<le> u)" 200 by (simp add: atLeastAtMost_def) 201 202text \<open>The above four lemmas could be declared as iffs. Unfortunately this 203breaks many proofs. Since it only helps blast, it is better to leave them 204alone.\<close> 205 206lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }" 207 by auto 208 209lemma (in order) atLeastLessThan_eq_atLeastAtMost_diff: 210 "{a..<b} = {a..b} - {b}" 211 by (auto simp add: atLeastLessThan_def atLeastAtMost_def) 212 213lemma (in order) greaterThanAtMost_eq_atLeastAtMost_diff: 214 "{a<..b} = {a..b} - {a}" 215 by (auto simp add: greaterThanAtMost_def atLeastAtMost_def) 216 217end 218 219subsubsection\<open>Emptyness, singletons, subset\<close> 220 221context preorder 222begin 223 224lemma atLeastatMost_empty_iff[simp]: 225 "{a..b} = {} \<longleftrightarrow> (\<not> a \<le> b)" 226 by auto (blast intro: order_trans) 227 228lemma atLeastatMost_empty_iff2[simp]: 229 "{} = {a..b} \<longleftrightarrow> (\<not> a \<le> b)" 230 by auto (blast intro: order_trans) 231 232lemma atLeastLessThan_empty_iff[simp]: 233 "{a..<b} = {} \<longleftrightarrow> (\<not> a < b)" 234 by auto (blast intro: le_less_trans) 235 236lemma atLeastLessThan_empty_iff2[simp]: 237 "{} = {a..<b} \<longleftrightarrow> (\<not> a < b)" 238 by auto (blast intro: le_less_trans) 239 240lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> \<not> k < l" 241 by auto (blast intro: less_le_trans) 242 243lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> \<not> k < l" 244 by auto (blast intro: less_le_trans) 245 246lemma atLeastatMost_subset_iff[simp]: 247 "{a..b} \<le> {c..d} \<longleftrightarrow> (\<not> a \<le> b) \<or> c \<le> a \<and> b \<le> d" 248 unfolding atLeastAtMost_def atLeast_def atMost_def 249 by (blast intro: order_trans) 250 251lemma atLeastatMost_psubset_iff: 252 "{a..b} < {c..d} \<longleftrightarrow> 253 ((\<not> a \<le> b) \<or> c \<le> a \<and> b \<le> d \<and> (c < a \<or> b < d)) \<and> c \<le> d" 254 by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans) 255 256lemma atLeastAtMost_subseteq_atLeastLessThan_iff: 257 "{a..b} \<subseteq> {c ..< d} \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)" 258 by auto (blast intro: local.order_trans local.le_less_trans elim: )+ 259 260lemma Icc_subset_Ici_iff[simp]: 261 "{l..h} \<subseteq> {l'..} = (\<not> l\<le>h \<or> l\<ge>l')" 262 by(auto simp: subset_eq intro: order_trans) 263 264lemma Icc_subset_Iic_iff[simp]: 265 "{l..h} \<subseteq> {..h'} = (\<not> l\<le>h \<or> h\<le>h')" 266 by(auto simp: subset_eq intro: order_trans) 267 268lemma not_Ici_eq_empty[simp]: "{l..} \<noteq> {}" 269 by(auto simp: set_eq_iff) 270 271lemma not_Iic_eq_empty[simp]: "{..h} \<noteq> {}" 272 by(auto simp: set_eq_iff) 273 274lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric] 275lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric] 276 277end 278 279context order 280begin 281 282lemma atLeastatMost_empty[simp]: 283 "b < a \<Longrightarrow> {a..b} = {}" 284 by(auto simp: atLeastAtMost_def atLeast_def atMost_def) 285 286lemma atLeastLessThan_empty[simp]: 287 "b \<le> a \<Longrightarrow> {a..<b} = {}" 288 by(auto simp: atLeastLessThan_def) 289 290lemma greaterThanAtMost_empty[simp]: "l \<le> k ==> {k<..l} = {}" 291 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) 292 293lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}" 294 by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def) 295 296lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}" 297 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) 298 299lemma atLeastAtMost_singleton': "a = b \<Longrightarrow> {a .. b} = {a}" by simp 300 301lemma Icc_eq_Icc[simp]: 302 "{l..h} = {l'..h'} = (l=l' \<and> h=h' \<or> \<not> l\<le>h \<and> \<not> l'\<le>h')" 303 by(simp add: order_class.eq_iff)(auto intro: order_trans) 304 305lemma atLeastAtMost_singleton_iff[simp]: 306 "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c" 307proof 308 assume "{a..b} = {c}" 309 hence *: "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp 310 with \<open>{a..b} = {c}\<close> have "c \<le> a \<and> b \<le> c" by auto 311 with * show "a = b \<and> b = c" by auto 312qed simp 313 314end 315 316context no_top 317begin 318 319(* also holds for no_bot but no_top should suffice *) 320lemma not_UNIV_le_Icc[simp]: "\<not> UNIV \<subseteq> {l..h}" 321using gt_ex[of h] by(auto simp: subset_eq less_le_not_le) 322 323lemma not_UNIV_le_Iic[simp]: "\<not> UNIV \<subseteq> {..h}" 324using gt_ex[of h] by(auto simp: subset_eq less_le_not_le) 325 326lemma not_Ici_le_Icc[simp]: "\<not> {l..} \<subseteq> {l'..h'}" 327using gt_ex[of h'] 328by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) 329 330lemma not_Ici_le_Iic[simp]: "\<not> {l..} \<subseteq> {..h'}" 331using gt_ex[of h'] 332by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) 333 334end 335 336context no_bot 337begin 338 339lemma not_UNIV_le_Ici[simp]: "\<not> UNIV \<subseteq> {l..}" 340using lt_ex[of l] by(auto simp: subset_eq less_le_not_le) 341 342lemma not_Iic_le_Icc[simp]: "\<not> {..h} \<subseteq> {l'..h'}" 343using lt_ex[of l'] 344by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) 345 346lemma not_Iic_le_Ici[simp]: "\<not> {..h} \<subseteq> {l'..}" 347using lt_ex[of l'] 348by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) 349 350end 351 352 353context no_top 354begin 355 356(* also holds for no_bot but no_top should suffice *) 357lemma not_UNIV_eq_Icc[simp]: "\<not> UNIV = {l'..h'}" 358using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le) 359 360lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric] 361 362lemma not_UNIV_eq_Iic[simp]: "\<not> UNIV = {..h'}" 363using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le) 364 365lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric] 366 367lemma not_Icc_eq_Ici[simp]: "\<not> {l..h} = {l'..}" 368unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast 369 370lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric] 371 372(* also holds for no_bot but no_top should suffice *) 373lemma not_Iic_eq_Ici[simp]: "\<not> {..h} = {l'..}" 374using not_Ici_le_Iic[of l' h] by blast 375 376lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric] 377 378end 379 380context no_bot 381begin 382 383lemma not_UNIV_eq_Ici[simp]: "\<not> UNIV = {l'..}" 384using lt_ex[of l'] by(auto simp: set_eq_iff less_le_not_le) 385 386lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric] 387 388lemma not_Icc_eq_Iic[simp]: "\<not> {l..h} = {..h'}" 389unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast 390 391lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric] 392 393end 394 395 396context dense_linorder 397begin 398 399lemma greaterThanLessThan_empty_iff[simp]: 400 "{ a <..< b } = {} \<longleftrightarrow> b \<le> a" 401 using dense[of a b] by (cases "a < b") auto 402 403lemma greaterThanLessThan_empty_iff2[simp]: 404 "{} = { a <..< b } \<longleftrightarrow> b \<le> a" 405 using dense[of a b] by (cases "a < b") auto 406 407lemma atLeastLessThan_subseteq_atLeastAtMost_iff: 408 "{a ..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 409 using dense[of "max a d" "b"] 410 by (force simp: subset_eq Ball_def not_less[symmetric]) 411 412lemma greaterThanAtMost_subseteq_atLeastAtMost_iff: 413 "{a <.. b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 414 using dense[of "a" "min c b"] 415 by (force simp: subset_eq Ball_def not_less[symmetric]) 416 417lemma greaterThanLessThan_subseteq_atLeastAtMost_iff: 418 "{a <..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 419 using dense[of "a" "min c b"] dense[of "max a d" "b"] 420 by (force simp: subset_eq Ball_def not_less[symmetric]) 421 422lemma greaterThanLessThan_subseteq_greaterThanLessThan: 423 "{a <..< b} \<subseteq> {c <..< d} \<longleftrightarrow> (a < b \<longrightarrow> a \<ge> c \<and> b \<le> d)" 424 using dense[of "a" "min c b"] dense[of "max a d" "b"] 425 by (force simp: subset_eq Ball_def not_less[symmetric]) 426 427lemma greaterThanAtMost_subseteq_atLeastLessThan_iff: 428 "{a <.. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b < d)" 429 using dense[of "a" "min c b"] 430 by (force simp: subset_eq Ball_def not_less[symmetric]) 431 432lemma greaterThanLessThan_subseteq_atLeastLessThan_iff: 433 "{a <..< b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 434 using dense[of "a" "min c b"] dense[of "max a d" "b"] 435 by (force simp: subset_eq Ball_def not_less[symmetric]) 436 437lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff: 438 "{a <..< b} \<subseteq> { c <.. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 439 using dense[of "a" "min c b"] dense[of "max a d" "b"] 440 by (force simp: subset_eq Ball_def not_less[symmetric]) 441 442end 443 444context no_top 445begin 446 447lemma greaterThan_non_empty[simp]: "{x <..} \<noteq> {}" 448 using gt_ex[of x] by auto 449 450end 451 452context no_bot 453begin 454 455lemma lessThan_non_empty[simp]: "{..< x} \<noteq> {}" 456 using lt_ex[of x] by auto 457 458end 459 460lemma (in linorder) atLeastLessThan_subset_iff: 461 "{a..<b} \<subseteq> {c..<d} \<Longrightarrow> b \<le> a \<or> c\<le>a \<and> b\<le>d" 462 apply (auto simp:subset_eq Ball_def not_le) 463 apply(frule_tac x=a in spec) 464 apply(erule_tac x=d in allE) 465 apply (auto simp: ) 466 done 467 468lemma atLeastLessThan_inj: 469 fixes a b c d :: "'a::linorder" 470 assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d" 471 shows "a = c" "b = d" 472using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le antisym_conv2 subset_refl)+ 473 474lemma atLeastLessThan_eq_iff: 475 fixes a b c d :: "'a::linorder" 476 assumes "a < b" "c < d" 477 shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d" 478 using atLeastLessThan_inj assms by auto 479 480lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \<longleftrightarrow> (b \<le> a \<and> d \<le> c) \<or> a = c \<and> b = d" 481 by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le) 482 483lemma (in order) Iio_Int_singleton: "{..<k} \<inter> {x} = (if x < k then {x} else {})" 484 by auto 485 486lemma (in linorder) Ioc_subset_iff: "{a<..b} \<subseteq> {c<..d} \<longleftrightarrow> (b \<le> a \<or> c \<le> a \<and> b \<le> d)" 487 by (auto simp: subset_eq Ball_def) (metis less_le not_less) 488 489lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot" 490by (auto simp: set_eq_iff intro: le_bot) 491 492lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top" 493by (auto simp: set_eq_iff intro: top_le) 494 495lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff: 496 "{x..y} = UNIV \<longleftrightarrow> (x = bot \<and> y = top)" 497by (auto simp: set_eq_iff intro: top_le le_bot) 498 499lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \<longleftrightarrow> n = bot" 500 by (auto simp: set_eq_iff not_less le_bot) 501 502lemma lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0" 503 by (simp add: Iio_eq_empty_iff bot_nat_def) 504 505lemma mono_image_least: 506 assumes f_mono: "mono f" and f_img: "f ` {m ..< n} = {m' ..< n'}" "m < n" 507 shows "f m = m'" 508proof - 509 from f_img have "{m' ..< n'} \<noteq> {}" 510 by (metis atLeastLessThan_empty_iff image_is_empty) 511 with f_img have "m' \<in> f ` {m ..< n}" by auto 512 then obtain k where "f k = m'" "m \<le> k" by auto 513 moreover have "m' \<le> f m" using f_img by auto 514 ultimately show "f m = m'" 515 using f_mono by (auto elim: monoE[where x=m and y=k]) 516qed 517 518 519subsection \<open>Infinite intervals\<close> 520 521context dense_linorder 522begin 523 524lemma infinite_Ioo: 525 assumes "a < b" 526 shows "\<not> finite {a<..<b}" 527proof 528 assume fin: "finite {a<..<b}" 529 moreover have ne: "{a<..<b} \<noteq> {}" 530 using \<open>a < b\<close> by auto 531 ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b" 532 using Max_in[of "{a <..< b}"] by auto 533 then obtain x where "Max {a <..< b} < x" "x < b" 534 using dense[of "Max {a<..<b}" b] by auto 535 then have "x \<in> {a <..< b}" 536 using \<open>a < Max {a <..< b}\<close> by auto 537 then have "x \<le> Max {a <..< b}" 538 using fin by auto 539 with \<open>Max {a <..< b} < x\<close> show False by auto 540qed 541 542lemma infinite_Icc: "a < b \<Longrightarrow> \<not> finite {a .. b}" 543 using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b] 544 by (auto dest: finite_subset) 545 546lemma infinite_Ico: "a < b \<Longrightarrow> \<not> finite {a ..< b}" 547 using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b] 548 by (auto dest: finite_subset) 549 550lemma infinite_Ioc: "a < b \<Longrightarrow> \<not> finite {a <.. b}" 551 using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b] 552 by (auto dest: finite_subset) 553 554lemma infinite_Ioo_iff [simp]: "infinite {a<..<b} \<longleftrightarrow> a < b" 555 using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioo) 556 557lemma infinite_Icc_iff [simp]: "infinite {a .. b} \<longleftrightarrow> a < b" 558 using not_less_iff_gr_or_eq by (fastforce simp: infinite_Icc) 559 560lemma infinite_Ico_iff [simp]: "infinite {a..<b} \<longleftrightarrow> a < b" 561 using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ico) 562 563lemma infinite_Ioc_iff [simp]: "infinite {a<..b} \<longleftrightarrow> a < b" 564 using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioc) 565 566end 567 568lemma infinite_Iio: "\<not> finite {..< a :: 'a :: {no_bot, linorder}}" 569proof 570 assume "finite {..< a}" 571 then have *: "\<And>x. x < a \<Longrightarrow> Min {..< a} \<le> x" 572 by auto 573 obtain x where "x < a" 574 using lt_ex by auto 575 576 obtain y where "y < Min {..< a}" 577 using lt_ex by auto 578 also have "Min {..< a} \<le> x" 579 using \<open>x < a\<close> by fact 580 also note \<open>x < a\<close> 581 finally have "Min {..< a} \<le> y" 582 by fact 583 with \<open>y < Min {..< a}\<close> show False by auto 584qed 585 586lemma infinite_Iic: "\<not> finite {.. a :: 'a :: {no_bot, linorder}}" 587 using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"] 588 by (auto simp: subset_eq less_imp_le) 589 590lemma infinite_Ioi: "\<not> finite {a :: 'a :: {no_top, linorder} <..}" 591proof 592 assume "finite {a <..}" 593 then have *: "\<And>x. a < x \<Longrightarrow> x \<le> Max {a <..}" 594 by auto 595 596 obtain y where "Max {a <..} < y" 597 using gt_ex by auto 598 599 obtain x where x: "a < x" 600 using gt_ex by auto 601 also from x have "x \<le> Max {a <..}" 602 by fact 603 also note \<open>Max {a <..} < y\<close> 604 finally have "y \<le> Max { a <..}" 605 by fact 606 with \<open>Max {a <..} < y\<close> show False by auto 607qed 608 609lemma infinite_Ici: "\<not> finite {a :: 'a :: {no_top, linorder} ..}" 610 using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"] 611 by (auto simp: subset_eq less_imp_le) 612 613subsubsection \<open>Intersection\<close> 614 615context linorder 616begin 617 618lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}" 619by auto 620 621lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}" 622by auto 623 624lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}" 625by auto 626 627lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}" 628by auto 629 630lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}" 631by auto 632 633lemma Int_atLeastLessThan[simp]: "{a..<b} Int {c..<d} = {max a c ..< min b d}" 634by auto 635 636lemma Int_greaterThanAtMost[simp]: "{a<..b} Int {c<..d} = {max a c <.. min b d}" 637by auto 638 639lemma Int_greaterThanLessThan[simp]: "{a<..<b} Int {c<..<d} = {max a c <..< min b d}" 640by auto 641 642lemma Int_atMost[simp]: "{..a} \<inter> {..b} = {.. min a b}" 643 by (auto simp: min_def) 644 645lemma Ioc_disjoint: "{a<..b} \<inter> {c<..d} = {} \<longleftrightarrow> b \<le> a \<or> d \<le> c \<or> b \<le> c \<or> d \<le> a" 646 by auto 647 648end 649 650context complete_lattice 651begin 652 653lemma 654 shows Sup_atLeast[simp]: "Sup {x ..} = top" 655 and Sup_greaterThanAtLeast[simp]: "x < top \<Longrightarrow> Sup {x <..} = top" 656 and Sup_atMost[simp]: "Sup {.. y} = y" 657 and Sup_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Sup { x .. y} = y" 658 and Sup_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Sup { x <.. y} = y" 659 by (auto intro!: Sup_eqI) 660 661lemma 662 shows Inf_atMost[simp]: "Inf {.. x} = bot" 663 and Inf_atMostLessThan[simp]: "top < x \<Longrightarrow> Inf {..< x} = bot" 664 and Inf_atLeast[simp]: "Inf {x ..} = x" 665 and Inf_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Inf { x .. y} = x" 666 and Inf_atLeastLessThan[simp]: "x < y \<Longrightarrow> Inf { x ..< y} = x" 667 by (auto intro!: Inf_eqI) 668 669end 670 671lemma 672 fixes x y :: "'a :: {complete_lattice, dense_linorder}" 673 shows Sup_lessThan[simp]: "Sup {..< y} = y" 674 and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y" 675 and Sup_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Sup { x <..< y} = y" 676 and Inf_greaterThan[simp]: "Inf {x <..} = x" 677 and Inf_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Inf { x <.. y} = x" 678 and Inf_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Inf { x <..< y} = x" 679 by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded) 680 681subsection \<open>Intervals of natural numbers\<close> 682 683subsubsection \<open>The Constant \<^term>\<open>lessThan\<close>\<close> 684 685lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" 686by (simp add: lessThan_def) 687 688lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" 689by (simp add: lessThan_def less_Suc_eq, blast) 690 691text \<open>The following proof is convenient in induction proofs where 692new elements get indices at the beginning. So it is used to transform 693\<^term>\<open>{..<Suc n}\<close> to \<^term>\<open>0::nat\<close> and \<^term>\<open>{..< n}\<close>.\<close> 694 695lemma zero_notin_Suc_image [simp]: "0 \<notin> Suc ` A" 696 by auto 697 698lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})" 699 by (auto simp: image_iff less_Suc_eq_0_disj) 700 701lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k" 702by (simp add: lessThan_def atMost_def less_Suc_eq_le) 703 704lemma atMost_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})" 705 unfolding lessThan_Suc_atMost[symmetric] lessThan_Suc_eq_insert_0[of "Suc n"] .. 706 707lemma UN_lessThan_UNIV: "(\<Union>m::nat. lessThan m) = UNIV" 708by blast 709 710subsubsection \<open>The Constant \<^term>\<open>greaterThan\<close>\<close> 711 712lemma greaterThan_0: "greaterThan 0 = range Suc" 713 unfolding greaterThan_def 714 by (blast dest: gr0_conv_Suc [THEN iffD1]) 715 716lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}" 717 unfolding greaterThan_def 718 by (auto elim: linorder_neqE) 719 720lemma INT_greaterThan_UNIV: "(\<Inter>m::nat. greaterThan m) = {}" 721 by blast 722 723subsubsection \<open>The Constant \<^term>\<open>atLeast\<close>\<close> 724 725lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" 726by (unfold atLeast_def UNIV_def, simp) 727 728lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}" 729 unfolding atLeast_def by (auto simp: order_le_less Suc_le_eq) 730 731lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k" 732 by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 733 734lemma UN_atLeast_UNIV: "(\<Union>m::nat. atLeast m) = UNIV" 735 by blast 736 737subsubsection \<open>The Constant \<^term>\<open>atMost\<close>\<close> 738 739lemma atMost_0 [simp]: "atMost (0::nat) = {0}" 740 by (simp add: atMost_def) 741 742lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)" 743 unfolding atMost_def by (auto simp add: less_Suc_eq order_le_less) 744 745lemma UN_atMost_UNIV: "(\<Union>m::nat. atMost m) = UNIV" 746 by blast 747 748subsubsection \<open>The Constant \<^term>\<open>atLeastLessThan\<close>\<close> 749 750text\<open>The orientation of the following 2 rules is tricky. The lhs is 751defined in terms of the rhs. Hence the chosen orientation makes sense 752in this theory --- the reverse orientation complicates proofs (eg 753nontermination). But outside, when the definition of the lhs is rarely 754used, the opposite orientation seems preferable because it reduces a 755specific concept to a more general one.\<close> 756 757lemma atLeast0LessThan [code_abbrev]: "{0::nat..<n} = {..<n}" 758 by(simp add:lessThan_def atLeastLessThan_def) 759 760lemma atLeast0AtMost [code_abbrev]: "{0..n::nat} = {..n}" 761 by(simp add:atMost_def atLeastAtMost_def) 762 763lemma lessThan_atLeast0: "{..<n} = {0::nat..<n}" 764 by (simp add: atLeast0LessThan) 765 766lemma atMost_atLeast0: "{..n} = {0::nat..n}" 767 by (simp add: atLeast0AtMost) 768 769lemma atLeastLessThan0: "{m..<0::nat} = {}" 770 by (simp add: atLeastLessThan_def) 771 772lemma atLeast0_lessThan_Suc: "{0..<Suc n} = insert n {0..<n}" 773 by (simp add: atLeast0LessThan lessThan_Suc) 774 775lemma atLeast0_lessThan_Suc_eq_insert_0: "{0..<Suc n} = insert 0 (Suc ` {0..<n})" 776 by (simp add: atLeast0LessThan lessThan_Suc_eq_insert_0) 777 778 779subsubsection \<open>The Constant \<^term>\<open>atLeastAtMost\<close>\<close> 780 781lemma Icc_eq_insert_lb_nat: "m \<le> n \<Longrightarrow> {m..n} = insert m {Suc m..n}" 782by auto 783 784lemma atLeast0_atMost_Suc: 785 "{0..Suc n} = insert (Suc n) {0..n}" 786 by (simp add: atLeast0AtMost atMost_Suc) 787 788lemma atLeast0_atMost_Suc_eq_insert_0: 789 "{0..Suc n} = insert 0 (Suc ` {0..n})" 790 by (simp add: atLeast0AtMost atMost_Suc_eq_insert_0) 791 792 793subsubsection \<open>Intervals of nats with \<^term>\<open>Suc\<close>\<close> 794 795text\<open>Not a simprule because the RHS is too messy.\<close> 796lemma atLeastLessThanSuc: 797 "{m..<Suc n} = (if m \<le> n then insert n {m..<n} else {})" 798by (auto simp add: atLeastLessThan_def) 799 800lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 801by (auto simp add: atLeastLessThan_def) 802 803lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 804 by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 805 806lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}" 807 by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 808 greaterThanAtMost_def) 809 810lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}" 811 by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 812 greaterThanLessThan_def) 813 814lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}" 815by (auto simp add: atLeastAtMost_def) 816 817lemma atLeastAtMost_insertL: "m \<le> n \<Longrightarrow> insert m {Suc m..n} = {m ..n}" 818by auto 819 820text \<open>The analogous result is useful on \<^typ>\<open>int\<close>:\<close> 821(* here, because we don't have an own int section *) 822lemma atLeastAtMostPlus1_int_conv: 823 "m \<le> 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}" 824 by (auto intro: set_eqI) 825 826lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}" 827 by (induct k) (simp_all add: atLeastLessThanSuc) 828 829 830subsubsection \<open>Intervals and numerals\<close> 831 832lemma lessThan_nat_numeral: \<comment> \<open>Evaluation for specific numerals\<close> 833 "lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))" 834 by (simp add: numeral_eq_Suc lessThan_Suc) 835 836lemma atMost_nat_numeral: \<comment> \<open>Evaluation for specific numerals\<close> 837 "atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))" 838 by (simp add: numeral_eq_Suc atMost_Suc) 839 840lemma atLeastLessThan_nat_numeral: \<comment> \<open>Evaluation for specific numerals\<close> 841 "atLeastLessThan m (numeral k :: nat) = 842 (if m \<le> (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k)) 843 else {})" 844 by (simp add: numeral_eq_Suc atLeastLessThanSuc) 845 846 847subsubsection \<open>Image\<close> 848 849context linordered_semidom 850begin 851 852lemma image_add_atLeast[simp]: "plus k ` {i..} = {k + i..}" 853proof - 854 have "n = k + (n - k)" if "i + k \<le> n" for n 855 proof - 856 have "n = (n - (k + i)) + (k + i)" using that 857 by (metis add_commute le_add_diff_inverse) 858 then show "n = k + (n - k)" 859 by (metis local.add_diff_cancel_left' add_assoc add_commute) 860 qed 861 then show ?thesis 862 by (fastforce simp: add_le_imp_le_diff add.commute) 863qed 864 865lemma image_add_atLeastAtMost [simp]: 866 "plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B") 867proof 868 show "?A \<subseteq> ?B" 869 by (auto simp add: ac_simps) 870next 871 show "?B \<subseteq> ?A" 872 proof 873 fix n 874 assume "n \<in> ?B" 875 then have "i \<le> n - k" 876 by (simp add: add_le_imp_le_diff) 877 have "n = n - k + k" 878 proof - 879 from \<open>n \<in> ?B\<close> have "n = n - (i + k) + (i + k)" 880 by simp 881 also have "\<dots> = n - k - i + i + k" 882 by (simp add: algebra_simps) 883 also have "\<dots> = n - k + k" 884 using \<open>i \<le> n - k\<close> by simp 885 finally show ?thesis . 886 qed 887 moreover have "n - k \<in> {i..j}" 888 using \<open>n \<in> ?B\<close> 889 by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le) 890 ultimately show "n \<in> ?A" 891 by (simp add: ac_simps) 892 qed 893qed 894 895lemma image_add_atLeastAtMost' [simp]: 896 "(\<lambda>n. n + k) ` {i..j} = {i + k..j + k}" 897 by (simp add: add.commute [of _ k]) 898 899lemma image_add_atLeastLessThan [simp]: 900 "plus k ` {i..<j} = {i + k..<j + k}" 901 by (simp add: image_set_diff atLeastLessThan_eq_atLeastAtMost_diff ac_simps) 902 903lemma image_add_atLeastLessThan' [simp]: 904 "(\<lambda>n. n + k) ` {i..<j} = {i + k..<j + k}" 905 by (simp add: add.commute [of _ k]) 906 907lemma image_add_greaterThanAtMost[simp]: "(+) c ` {a<..b} = {c + a<..c + b}" 908 by (simp add: image_set_diff greaterThanAtMost_eq_atLeastAtMost_diff ac_simps) 909 910end 911 912context ordered_ab_group_add 913begin 914 915lemma 916 fixes x :: 'a 917 shows image_uminus_greaterThan[simp]: "uminus ` {x<..} = {..<-x}" 918 and image_uminus_atLeast[simp]: "uminus ` {x..} = {..-x}" 919proof safe 920 fix y assume "y < -x" 921 hence *: "x < -y" using neg_less_iff_less[of "-y" x] by simp 922 have "- (-y) \<in> uminus ` {x<..}" 923 by (rule imageI) (simp add: *) 924 thus "y \<in> uminus ` {x<..}" by simp 925next 926 fix y assume "y \<le> -x" 927 have "- (-y) \<in> uminus ` {x..}" 928 by (rule imageI) (insert \<open>y \<le> -x\<close>[THEN le_imp_neg_le], simp) 929 thus "y \<in> uminus ` {x..}" by simp 930qed simp_all 931 932lemma 933 fixes x :: 'a 934 shows image_uminus_lessThan[simp]: "uminus ` {..<x} = {-x<..}" 935 and image_uminus_atMost[simp]: "uminus ` {..x} = {-x..}" 936proof - 937 have "uminus ` {..<x} = uminus ` uminus ` {-x<..}" 938 and "uminus ` {..x} = uminus ` uminus ` {-x..}" by simp_all 939 thus "uminus ` {..<x} = {-x<..}" and "uminus ` {..x} = {-x..}" 940 by (simp_all add: image_image 941 del: image_uminus_greaterThan image_uminus_atLeast) 942qed 943 944lemma 945 fixes x :: 'a 946 shows image_uminus_atLeastAtMost[simp]: "uminus ` {x..y} = {-y..-x}" 947 and image_uminus_greaterThanAtMost[simp]: "uminus ` {x<..y} = {-y..<-x}" 948 and image_uminus_atLeastLessThan[simp]: "uminus ` {x..<y} = {-y<..-x}" 949 and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {-y<..<-x}" 950 by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def 951 greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute) 952 953lemma image_add_atMost[simp]: "(+) c ` {..a} = {..c + a}" 954 by (auto intro!: image_eqI[where x="x - c" for x] simp: algebra_simps) 955 956end 957 958lemma image_Suc_atLeastAtMost [simp]: 959 "Suc ` {i..j} = {Suc i..Suc j}" 960 using image_add_atLeastAtMost [of 1 i j] 961 by (simp only: plus_1_eq_Suc) simp 962 963lemma image_Suc_atLeastLessThan [simp]: 964 "Suc ` {i..<j} = {Suc i..<Suc j}" 965 using image_add_atLeastLessThan [of 1 i j] 966 by (simp only: plus_1_eq_Suc) simp 967 968corollary image_Suc_atMost: 969 "Suc ` {..n} = {1..Suc n}" 970 by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost) 971 972corollary image_Suc_lessThan: 973 "Suc ` {..<n} = {1..n}" 974 by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost) 975 976lemma image_diff_atLeastAtMost [simp]: 977 fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}" 978 apply auto 979 apply (rule_tac x="d-x" in rev_image_eqI, auto) 980 done 981 982lemma image_diff_atLeastLessThan [simp]: 983 fixes a b c::"'a::linordered_idom" 984 shows "(-) c ` {a..<b} = {c - b<..c - a}" 985proof - 986 have "(-) c ` {a..<b} = (+) c ` uminus ` {a ..<b}" 987 unfolding image_image by simp 988 also have "\<dots> = {c - b<..c - a}" by simp 989 finally show ?thesis by simp 990qed 991 992lemma image_minus_const_greaterThanAtMost[simp]: 993 fixes a b c::"'a::linordered_idom" 994 shows "(-) c ` {a<..b} = {c - b..<c - a}" 995proof - 996 have "(-) c ` {a<..b} = (+) c ` uminus ` {a<..b}" 997 unfolding image_image by simp 998 also have "\<dots> = {c - b..<c - a}" by simp 999 finally show ?thesis by simp 1000qed 1001 1002lemma image_minus_const_atLeast[simp]: 1003 fixes a c::"'a::linordered_idom" 1004 shows "(-) c ` {a..} = {..c - a}" 1005proof - 1006 have "(-) c ` {a..} = (+) c ` uminus ` {a ..}" 1007 unfolding image_image by simp 1008 also have "\<dots> = {..c - a}" by simp 1009 finally show ?thesis by simp 1010qed 1011 1012lemma image_minus_const_AtMost[simp]: 1013 fixes b c::"'a::linordered_idom" 1014 shows "(-) c ` {..b} = {c - b..}" 1015proof - 1016 have "(-) c ` {..b} = (+) c ` uminus ` {..b}" 1017 unfolding image_image by simp 1018 also have "\<dots> = {c - b..}" by simp 1019 finally show ?thesis by simp 1020qed 1021 1022lemma image_minus_const_atLeastAtMost' [simp]: 1023 "(\<lambda>t. t-d)`{a..b} = {a-d..b-d}" for d::"'a::linordered_idom" 1024 by (metis (no_types, lifting) diff_conv_add_uminus image_add_atLeastAtMost' image_cong) 1025 1026context linordered_field 1027begin 1028 1029lemma image_mult_atLeastAtMost [simp]: 1030 "((*) d ` {a..b}) = {d*a..d*b}" if "d>0" 1031 using that 1032 by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x]) 1033 1034lemma image_divide_atLeastAtMost [simp]: 1035 "((\<lambda>c. c / d) ` {a..b}) = {a/d..b/d}" if "d>0" 1036proof - 1037 from that have "inverse d > 0" 1038 by simp 1039 with image_mult_atLeastAtMost [of "inverse d" a b] 1040 have "(*) (inverse d) ` {a..b} = {inverse d * a..inverse d * b}" 1041 by blast 1042 moreover have "(*) (inverse d) = (\<lambda>c. c / d)" 1043 by (simp add: fun_eq_iff field_simps) 1044 ultimately show ?thesis 1045 by simp 1046qed 1047 1048lemma image_mult_atLeastAtMost_if: 1049 "(*) c ` {x .. y} = 1050 (if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})" 1051proof (cases "c = 0 \<or> x > y") 1052 case True 1053 then show ?thesis 1054 by auto 1055next 1056 case False 1057 then have "x \<le> y" 1058 by auto 1059 from False consider "c < 0"| "c > 0" 1060 by (auto simp add: neq_iff) 1061 then show ?thesis 1062 proof cases 1063 case 1 1064 have "(*) c ` {x..y} = {c * y..c * x}" 1065 proof (rule set_eqI) 1066 fix d 1067 from 1 have "inj (\<lambda>z. z / c)" 1068 by (auto intro: injI) 1069 then have "d \<in> (*) c ` {x..y} \<longleftrightarrow> d / c \<in> (\<lambda>z. z div c) ` (*) c ` {x..y}" 1070 by (subst inj_image_mem_iff) simp_all 1071 also have "\<dots> \<longleftrightarrow> d / c \<in> {x..y}" 1072 using 1 by (simp add: image_image) 1073 also have "\<dots> \<longleftrightarrow> d \<in> {c * y..c * x}" 1074 by (auto simp add: field_simps 1) 1075 finally show "d \<in> (*) c ` {x..y} \<longleftrightarrow> d \<in> {c * y..c * x}" . 1076 qed 1077 with \<open>x \<le> y\<close> show ?thesis 1078 by auto 1079 qed (simp add: mult_left_mono_neg) 1080qed 1081 1082lemma image_mult_atLeastAtMost_if': 1083 "(\<lambda>x. x * c) ` {x..y} = 1084 (if x \<le> y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})" 1085 using image_mult_atLeastAtMost_if [of c x y] by (auto simp add: ac_simps) 1086 1087lemma image_affinity_atLeastAtMost: 1088 "((\<lambda>x. m * x + c) ` {a..b}) = (if {a..b} = {} then {} 1089 else if 0 \<le> m then {m * a + c .. m * b + c} 1090 else {m * b + c .. m * a + c})" 1091proof - 1092 have *: "(\<lambda>x. m * x + c) = ((\<lambda>x. x + c) \<circ> (*) m)" 1093 by (simp add: fun_eq_iff) 1094 show ?thesis by (simp only: * image_comp [symmetric] image_mult_atLeastAtMost_if) 1095 (auto simp add: mult_le_cancel_left) 1096qed 1097 1098lemma image_affinity_atLeastAtMost_diff: 1099 "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {} 1100 else if 0 \<le> m then {m*a - c .. m*b - c} 1101 else {m*b - c .. m*a - c})" 1102 using image_affinity_atLeastAtMost [of m "-c" a b] 1103 by simp 1104 1105lemma image_affinity_atLeastAtMost_div: 1106 "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {} 1107 else if 0 \<le> m then {a/m + c .. b/m + c} 1108 else {b/m + c .. a/m + c})" 1109 using image_affinity_atLeastAtMost [of "inverse m" c a b] 1110 by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide) 1111 1112lemma image_affinity_atLeastAtMost_div_diff: 1113 "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {} 1114 else if 0 \<le> m then {a/m - c .. b/m - c} 1115 else {b/m - c .. a/m - c})" 1116 using image_affinity_atLeastAtMost_diff [of "inverse m" c a b] 1117 by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide) 1118 1119end 1120 1121lemma atLeast1_lessThan_eq_remove0: 1122 "{Suc 0..<n} = {..<n} - {0}" 1123 by auto 1124 1125lemma atLeast1_atMost_eq_remove0: 1126 "{Suc 0..n} = {..n} - {0}" 1127 by auto 1128 1129lemma image_add_int_atLeastLessThan: 1130 "(\<lambda>x. x + (l::int)) ` {0..<u-l} = {l..<u}" 1131 apply (auto simp add: image_def) 1132 apply (rule_tac x = "x - l" in bexI) 1133 apply auto 1134 done 1135 1136lemma image_minus_const_atLeastLessThan_nat: 1137 fixes c :: nat 1138 shows "(\<lambda>i. i - c) ` {x ..< y} = 1139 (if c < y then {x - c ..< y - c} else if x < y then {0} else {})" 1140 (is "_ = ?right") 1141proof safe 1142 fix a assume a: "a \<in> ?right" 1143 show "a \<in> (\<lambda>i. i - c) ` {x ..< y}" 1144 proof cases 1145 assume "c < y" with a show ?thesis 1146 by (auto intro!: image_eqI[of _ _ "a + c"]) 1147 next 1148 assume "\<not> c < y" with a show ?thesis 1149 by (auto intro!: image_eqI[of _ _ x] split: if_split_asm) 1150 qed 1151qed auto 1152 1153lemma image_int_atLeastLessThan: 1154 "int ` {a..<b} = {int a..<int b}" 1155 by (auto intro!: image_eqI [where x = "nat x" for x]) 1156 1157lemma image_int_atLeastAtMost: 1158 "int ` {a..b} = {int a..int b}" 1159 by (auto intro!: image_eqI [where x = "nat x" for x]) 1160 1161 1162subsubsection \<open>Finiteness\<close> 1163 1164lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}" 1165 by (induct k) (simp_all add: lessThan_Suc) 1166 1167lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}" 1168 by (induct k) (simp_all add: atMost_Suc) 1169 1170lemma finite_greaterThanLessThan [iff]: 1171 fixes l :: nat shows "finite {l<..<u}" 1172 by (simp add: greaterThanLessThan_def) 1173 1174lemma finite_atLeastLessThan [iff]: 1175 fixes l :: nat shows "finite {l..<u}" 1176 by (simp add: atLeastLessThan_def) 1177 1178lemma finite_greaterThanAtMost [iff]: 1179 fixes l :: nat shows "finite {l<..u}" 1180 by (simp add: greaterThanAtMost_def) 1181 1182lemma finite_atLeastAtMost [iff]: 1183 fixes l :: nat shows "finite {l..u}" 1184 by (simp add: atLeastAtMost_def) 1185 1186text \<open>A bounded set of natural numbers is finite.\<close> 1187lemma bounded_nat_set_is_finite: "(\<forall>i\<in>N. i < (n::nat)) \<Longrightarrow> finite N" 1188 by (rule finite_subset [OF _ finite_lessThan]) auto 1189 1190text \<open>A set of natural numbers is finite iff it is bounded.\<close> 1191lemma finite_nat_set_iff_bounded: 1192 "finite(N::nat set) = (\<exists>m. \<forall>n\<in>N. n<m)" (is "?F = ?B") 1193proof 1194 assume f:?F show ?B 1195 using Max_ge[OF \<open>?F\<close>, simplified less_Suc_eq_le[symmetric]] by blast 1196next 1197 assume ?B show ?F using \<open>?B\<close> by(blast intro:bounded_nat_set_is_finite) 1198qed 1199 1200lemma finite_nat_set_iff_bounded_le: "finite(N::nat set) = (\<exists>m. \<forall>n\<in>N. n\<le>m)" 1201 unfolding finite_nat_set_iff_bounded 1202 by (blast dest:less_imp_le_nat le_imp_less_Suc) 1203 1204lemma finite_less_ub: 1205 "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}" 1206by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) 1207 1208lemma bounded_Max_nat: 1209 fixes P :: "nat \<Rightarrow> bool" 1210 assumes x: "P x" and M: "\<And>x. P x \<Longrightarrow> x \<le> M" 1211 obtains m where "P m" "\<And>x. P x \<Longrightarrow> x \<le> m" 1212proof - 1213 have "finite {x. P x}" 1214 using M finite_nat_set_iff_bounded_le by auto 1215 then have "Max {x. P x} \<in> {x. P x}" 1216 using Max_in x by auto 1217 then show ?thesis 1218 by (simp add: \<open>finite {x. P x}\<close> that) 1219qed 1220 1221 1222text\<open>Any subset of an interval of natural numbers the size of the 1223subset is exactly that interval.\<close> 1224 1225lemma subset_card_intvl_is_intvl: 1226 assumes "A \<subseteq> {k..<k + card A}" 1227 shows "A = {k..<k + card A}" 1228proof (cases "finite A") 1229 case True 1230 from this and assms show ?thesis 1231 proof (induct A rule: finite_linorder_max_induct) 1232 case empty thus ?case by auto 1233 next 1234 case (insert b A) 1235 hence *: "b \<notin> A" by auto 1236 with insert have "A \<le> {k..<k + card A}" and "b = k + card A" 1237 by fastforce+ 1238 with insert * show ?case by auto 1239 qed 1240next 1241 case False 1242 with assms show ?thesis by simp 1243qed 1244 1245 1246subsubsection \<open>Proving Inclusions and Equalities between Unions\<close> 1247 1248lemma UN_le_eq_Un0: 1249 "(\<Union>i\<le>n::nat. M i) = (\<Union>i\<in>{1..n}. M i) \<union> M 0" (is "?A = ?B") 1250proof 1251 show "?A \<subseteq> ?B" 1252 proof 1253 fix x assume "x \<in> ?A" 1254 then obtain i where i: "i\<le>n" "x \<in> M i" by auto 1255 show "x \<in> ?B" 1256 proof(cases i) 1257 case 0 with i show ?thesis by simp 1258 next 1259 case (Suc j) with i show ?thesis by auto 1260 qed 1261 qed 1262next 1263 show "?B \<subseteq> ?A" by fastforce 1264qed 1265 1266lemma UN_le_add_shift: 1267 "(\<Union>i\<le>n::nat. M(i+k)) = (\<Union>i\<in>{k..n+k}. M i)" (is "?A = ?B") 1268proof 1269 show "?A \<subseteq> ?B" by fastforce 1270next 1271 show "?B \<subseteq> ?A" 1272 proof 1273 fix x assume "x \<in> ?B" 1274 then obtain i where i: "i \<in> {k..n+k}" "x \<in> M(i)" by auto 1275 hence "i-k\<le>n \<and> x \<in> M((i-k)+k)" by auto 1276 thus "x \<in> ?A" by blast 1277 qed 1278qed 1279 1280lemma UN_le_add_shift_strict: 1281 "(\<Union>i<n::nat. M(i+k)) = (\<Union>i\<in>{k..<n+k}. M i)" (is "?A = ?B") 1282proof 1283 show "?B \<subseteq> ?A" 1284 proof 1285 fix x assume "x \<in> ?B" 1286 then obtain i where i: "i \<in> {k..<n+k}" "x \<in> M(i)" by auto 1287 then have "i - k < n \<and> x \<in> M((i-k) + k)" by auto 1288 then show "x \<in> ?A" using UN_le_add_shift by blast 1289 qed 1290qed (fastforce) 1291 1292lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)" 1293 by (auto simp add: atLeast0LessThan) 1294 1295lemma UN_finite_subset: 1296 "(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C" 1297 by (subst UN_UN_finite_eq [symmetric]) blast 1298 1299lemma UN_finite2_subset: 1300 assumes "\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n + k}. B i)" 1301 shows "(\<Union>n. A n) \<subseteq> (\<Union>n. B n)" 1302proof (rule UN_finite_subset, rule) 1303 fix n and a 1304 from assms have "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n + k}. B i)" . 1305 moreover assume "a \<in> (\<Union>i\<in>{0..<n}. A i)" 1306 ultimately have "a \<in> (\<Union>i\<in>{0..<n + k}. B i)" by blast 1307 then show "a \<in> (\<Union>i. B i)" by (auto simp add: UN_UN_finite_eq) 1308qed 1309 1310lemma UN_finite2_eq: 1311 "(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n + k}. B i)) \<Longrightarrow> 1312 (\<Union>n. A n) = (\<Union>n. B n)" 1313 apply (rule subset_antisym [OF UN_finite_subset UN_finite2_subset]) 1314 apply auto 1315 apply (force simp add: atLeastLessThan_add_Un [of 0])+ 1316 done 1317 1318 1319subsubsection \<open>Cardinality\<close> 1320 1321lemma card_lessThan [simp]: "card {..<u} = u" 1322 by (induct u, simp_all add: lessThan_Suc) 1323 1324lemma card_atMost [simp]: "card {..u} = Suc u" 1325 by (simp add: lessThan_Suc_atMost [THEN sym]) 1326 1327lemma card_atLeastLessThan [simp]: "card {l..<u} = u - l" 1328proof - 1329 have "{l..<u} = (\<lambda>x. x + l) ` {..<u-l}" 1330 apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 1331 apply (rule_tac x = "x - l" in exI) 1332 apply arith 1333 done 1334 then have "card {l..<u} = card {..<u-l}" 1335 by (simp add: card_image inj_on_def) 1336 then show ?thesis 1337 by simp 1338qed 1339 1340lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l" 1341 by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp) 1342 1343lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l" 1344 by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp) 1345 1346lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l" 1347 by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp) 1348 1349lemma subset_eq_atLeast0_lessThan_finite: 1350 fixes n :: nat 1351 assumes "N \<subseteq> {0..<n}" 1352 shows "finite N" 1353 using assms finite_atLeastLessThan by (rule finite_subset) 1354 1355lemma subset_eq_atLeast0_atMost_finite: 1356 fixes n :: nat 1357 assumes "N \<subseteq> {0..n}" 1358 shows "finite N" 1359 using assms finite_atLeastAtMost by (rule finite_subset) 1360 1361lemma ex_bij_betw_nat_finite: 1362 "finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M" 1363 apply(drule finite_imp_nat_seg_image_inj_on) 1364 apply(auto simp:atLeast0LessThan[symmetric] lessThan_def[symmetric] card_image bij_betw_def) 1365 done 1366 1367lemma ex_bij_betw_finite_nat: 1368 "finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}" 1369 by (blast dest: ex_bij_betw_nat_finite bij_betw_inv) 1370 1371lemma finite_same_card_bij: 1372 "finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> \<exists>h. bij_betw h A B" 1373 apply(drule ex_bij_betw_finite_nat) 1374 apply(drule ex_bij_betw_nat_finite) 1375 apply(auto intro!:bij_betw_trans) 1376 done 1377 1378lemma ex_bij_betw_nat_finite_1: 1379 "finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M" 1380 by (rule finite_same_card_bij) auto 1381 1382lemma bij_betw_iff_card: 1383 assumes "finite A" "finite B" 1384 shows "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)" 1385proof 1386 assume "card A = card B" 1387 moreover obtain f where "bij_betw f A {0 ..< card A}" 1388 using assms ex_bij_betw_finite_nat by blast 1389 moreover obtain g where "bij_betw g {0 ..< card B} B" 1390 using assms ex_bij_betw_nat_finite by blast 1391 ultimately have "bij_betw (g \<circ> f) A B" 1392 by (auto simp: bij_betw_trans) 1393 thus "(\<exists>f. bij_betw f A B)" by blast 1394qed (auto simp: bij_betw_same_card) 1395 1396lemma subset_eq_atLeast0_lessThan_card: 1397 fixes n :: nat 1398 assumes "N \<subseteq> {0..<n}" 1399 shows "card N \<le> n" 1400proof - 1401 from assms finite_lessThan have "card N \<le> card {0..<n}" 1402 using card_mono by blast 1403 then show ?thesis by simp 1404qed 1405 1406text \<open>Relational version of @{thm [source] card_inj_on_le}:\<close> 1407lemma card_le_if_inj_on_rel: 1408assumes "finite B" 1409 "\<And>a. a \<in> A \<Longrightarrow> \<exists>b. b\<in>B \<and> r a b" 1410 "\<And>a1 a2 b. \<lbrakk> a1 \<in> A; a2 \<in> A; b \<in> B; r a1 b; r a2 b \<rbrakk> \<Longrightarrow> a1 = a2" 1411shows "card A \<le> card B" 1412proof - 1413 let ?P = "\<lambda>a b. b \<in> B \<and> r a b" 1414 let ?f = "\<lambda>a. SOME b. ?P a b" 1415 have 1: "?f ` A \<subseteq> B" by (auto intro: someI2_ex[OF assms(2)]) 1416 have "inj_on ?f A" 1417 proof (auto simp: inj_on_def) 1418 fix a1 a2 assume asms: "a1 \<in> A" "a2 \<in> A" "?f a1 = ?f a2" 1419 have 0: "?f a1 \<in> B" using "1" \<open>a1 \<in> A\<close> by blast 1420 have 1: "r a1 (?f a1)" using someI_ex[OF assms(2)[OF \<open>a1 \<in> A\<close>]] by blast 1421 have 2: "r a2 (?f a1)" using someI_ex[OF assms(2)[OF \<open>a2 \<in> A\<close>]] asms(3) by auto 1422 show "a1 = a2" using assms(3)[OF asms(1,2) 0 1 2] . 1423 qed 1424 with 1 show ?thesis using card_inj_on_le[of ?f A B] assms(1) by simp 1425qed 1426 1427 1428subsection \<open>Intervals of integers\<close> 1429 1430lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}" 1431 by (auto simp add: atLeastAtMost_def atLeastLessThan_def) 1432 1433lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 1434 by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 1435 1436lemma atLeastPlusOneLessThan_greaterThanLessThan_int: 1437 "{l+1..<u} = {l<..<u::int}" 1438 by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 1439 1440subsubsection \<open>Finiteness\<close> 1441 1442lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 1443 {(0::int)..<u} = int ` {..<nat u}" 1444 unfolding image_def lessThan_def 1445 apply auto 1446 apply (rule_tac x = "nat x" in exI) 1447 apply (auto simp add: zless_nat_eq_int_zless [THEN sym]) 1448 done 1449 1450lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}" 1451proof (cases "0 \<le> u") 1452 case True 1453 then show ?thesis 1454 by (auto simp: image_atLeastZeroLessThan_int) 1455qed auto 1456 1457lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}" 1458 by (simp only: image_add_int_atLeastLessThan [symmetric, of l] finite_imageI finite_atLeastZeroLessThan_int) 1459 1460lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" 1461 by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp) 1462 1463lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" 1464 by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 1465 1466lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" 1467 by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) 1468 1469 1470subsubsection \<open>Cardinality\<close> 1471 1472lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u" 1473proof (cases "0 \<le> u") 1474 case True 1475 then show ?thesis 1476 by (auto simp: image_atLeastZeroLessThan_int card_image inj_on_def) 1477qed auto 1478 1479lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u - l)" 1480proof - 1481 have "card {l..<u} = card {0..<u-l}" 1482 apply (subst image_add_int_atLeastLessThan [symmetric]) 1483 apply (rule card_image) 1484 apply (simp add: inj_on_def) 1485 done 1486 then show ?thesis 1487 by (simp add: card_atLeastZeroLessThan_int) 1488qed 1489 1490lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)" 1491 apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 1492 apply (auto simp add: algebra_simps) 1493 done 1494 1495lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)" 1496 by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 1497 1498lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))" 1499 by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) 1500 1501lemma finite_M_bounded_by_nat: "finite {k. P k \<and> k < (i::nat)}" 1502proof - 1503 have "{k. P k \<and> k < i} \<subseteq> {..<i}" by auto 1504 with finite_lessThan[of "i"] show ?thesis by (simp add: finite_subset) 1505qed 1506 1507lemma card_less: 1508 assumes zero_in_M: "0 \<in> M" 1509 shows "card {k \<in> M. k < Suc i} \<noteq> 0" 1510proof - 1511 from zero_in_M have "{k \<in> M. k < Suc i} \<noteq> {}" by auto 1512 with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff) 1513qed 1514 1515lemma card_less_Suc2: 1516 assumes "0 \<notin> M" shows "card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}" 1517proof - 1518 have *: "\<lbrakk>j \<in> M; j < Suc i\<rbrakk> \<Longrightarrow> j - Suc 0 < i \<and> Suc (j - Suc 0) \<in> M \<and> Suc 0 \<le> j" for j 1519 by (cases j) (use assms in auto) 1520 show ?thesis 1521 proof (rule card_bij_eq) 1522 show "inj_on Suc {k. Suc k \<in> M \<and> k < i}" 1523 by force 1524 show "inj_on (\<lambda>x. x - Suc 0) {k \<in> M. k < Suc i}" 1525 by (rule inj_on_diff_nat) (use * in blast) 1526 qed (use * in auto) 1527qed 1528 1529lemma card_less_Suc: 1530 assumes "0 \<in> M" 1531 shows "Suc (card {k. Suc k \<in> M \<and> k < i}) = card {k \<in> M. k < Suc i}" 1532proof - 1533 have "Suc (card {k. Suc k \<in> M \<and> k < i}) = Suc (card {k. Suc k \<in> M - {0} \<and> k < i})" 1534 by simp 1535 also have "\<dots> = Suc (card {k \<in> M - {0}. k < Suc i})" 1536 apply (subst card_less_Suc2) 1537 using assms by auto 1538 also have "\<dots> = Suc (card ({k \<in> M. k < Suc i} - {0}))" 1539 by (force intro: arg_cong [where f=card]) 1540 also have "\<dots> = card (insert 0 ({k \<in> M. k < Suc i} - {0}))" 1541 by (simp add: card_insert) 1542 also have "... = card {k \<in> M. k < Suc i}" 1543 using assms 1544 by (force simp add: intro: arg_cong [where f=card]) 1545 finally show ?thesis. 1546qed 1547 1548 1549subsection \<open>Lemmas useful with the summation operator sum\<close> 1550 1551text \<open>For examples, see Algebra/poly/UnivPoly2.thy\<close> 1552 1553subsubsection \<open>Disjoint Unions\<close> 1554 1555text \<open>Singletons and open intervals\<close> 1556 1557lemma ivl_disj_un_singleton: 1558 "{l::'a::linorder} Un {l<..} = {l..}" 1559 "{..<u} Un {u::'a::linorder} = {..u}" 1560 "(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}" 1561 "(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}" 1562 "(l::'a::linorder) \<le> u ==> {l} Un {l<..u} = {l..u}" 1563 "(l::'a::linorder) \<le> u ==> {l..<u} Un {u} = {l..u}" 1564by auto 1565 1566text \<open>One- and two-sided intervals\<close> 1567 1568lemma ivl_disj_un_one: 1569 "(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}" 1570 "(l::'a::linorder) \<le> u ==> {..<l} Un {l..<u} = {..<u}" 1571 "(l::'a::linorder) \<le> u ==> {..l} Un {l<..u} = {..u}" 1572 "(l::'a::linorder) \<le> u ==> {..<l} Un {l..u} = {..u}" 1573 "(l::'a::linorder) \<le> u ==> {l<..u} Un {u<..} = {l<..}" 1574 "(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}" 1575 "(l::'a::linorder) \<le> u ==> {l..u} Un {u<..} = {l..}" 1576 "(l::'a::linorder) \<le> u ==> {l..<u} Un {u..} = {l..}" 1577by auto 1578 1579text \<open>Two- and two-sided intervals\<close> 1580 1581lemma ivl_disj_un_two: 1582 "[| (l::'a::linorder) < m; m \<le> u |] ==> {l<..<m} Un {m..<u} = {l<..<u}" 1583 "[| (l::'a::linorder) \<le> m; m < u |] ==> {l<..m} Un {m<..<u} = {l<..<u}" 1584 "[| (l::'a::linorder) \<le> m; m \<le> u |] ==> {l..<m} Un {m..<u} = {l..<u}" 1585 "[| (l::'a::linorder) \<le> m; m < u |] ==> {l..m} Un {m<..<u} = {l..<u}" 1586 "[| (l::'a::linorder) < m; m \<le> u |] ==> {l<..<m} Un {m..u} = {l<..u}" 1587 "[| (l::'a::linorder) \<le> m; m \<le> u |] ==> {l<..m} Un {m<..u} = {l<..u}" 1588 "[| (l::'a::linorder) \<le> m; m \<le> u |] ==> {l..<m} Un {m..u} = {l..u}" 1589 "[| (l::'a::linorder) \<le> m; m \<le> u |] ==> {l..m} Un {m<..u} = {l..u}" 1590by auto 1591 1592lemma ivl_disj_un_two_touch: 1593 "[| (l::'a::linorder) < m; m < u |] ==> {l<..m} Un {m..<u} = {l<..<u}" 1594 "[| (l::'a::linorder) \<le> m; m < u |] ==> {l..m} Un {m..<u} = {l..<u}" 1595 "[| (l::'a::linorder) < m; m \<le> u |] ==> {l<..m} Un {m..u} = {l<..u}" 1596 "[| (l::'a::linorder) \<le> m; m \<le> u |] ==> {l..m} Un {m..u} = {l..u}" 1597by auto 1598 1599lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ivl_disj_un_two_touch 1600 1601subsubsection \<open>Disjoint Intersections\<close> 1602 1603text \<open>One- and two-sided intervals\<close> 1604 1605lemma ivl_disj_int_one: 1606 "{..l::'a::order} Int {l<..<u} = {}" 1607 "{..<l} Int {l..<u} = {}" 1608 "{..l} Int {l<..u} = {}" 1609 "{..<l} Int {l..u} = {}" 1610 "{l<..u} Int {u<..} = {}" 1611 "{l<..<u} Int {u..} = {}" 1612 "{l..u} Int {u<..} = {}" 1613 "{l..<u} Int {u..} = {}" 1614 by auto 1615 1616text \<open>Two- and two-sided intervals\<close> 1617 1618lemma ivl_disj_int_two: 1619 "{l::'a::order<..<m} Int {m..<u} = {}" 1620 "{l<..m} Int {m<..<u} = {}" 1621 "{l..<m} Int {m..<u} = {}" 1622 "{l..m} Int {m<..<u} = {}" 1623 "{l<..<m} Int {m..u} = {}" 1624 "{l<..m} Int {m<..u} = {}" 1625 "{l..<m} Int {m..u} = {}" 1626 "{l..m} Int {m<..u} = {}" 1627 by auto 1628 1629lemmas ivl_disj_int = ivl_disj_int_one ivl_disj_int_two 1630 1631subsubsection \<open>Some Differences\<close> 1632 1633lemma ivl_diff[simp]: 1634 "i \<le> n \<Longrightarrow> {i..<m} - {i..<n} = {n..<(m::'a::linorder)}" 1635by(auto) 1636 1637lemma (in linorder) lessThan_minus_lessThan [simp]: 1638 "{..< n} - {..< m} = {m ..< n}" 1639 by auto 1640 1641lemma (in linorder) atLeastAtMost_diff_ends: 1642 "{a..b} - {a, b} = {a<..<b}" 1643 by auto 1644 1645 1646subsubsection \<open>Some Subset Conditions\<close> 1647 1648lemma ivl_subset [simp]: "({i..<j} \<subseteq> {m..<n}) = (j \<le> i \<or> m \<le> i \<and> j \<le> (n::'a::linorder))" 1649 using linorder_class.le_less_linear[of i n] 1650 apply (auto simp: linorder_not_le) 1651 apply (force intro: leI)+ 1652 done 1653 1654lemma obtain_subset_with_card_n: 1655 assumes "n \<le> card S" 1656 obtains T where "T \<subseteq> S" "card T = n" "finite T" 1657proof - 1658 obtain n' where "card S = n + n'" 1659 by (metis assms le_add_diff_inverse) 1660 with that show thesis 1661 proof (induct n' arbitrary: S) 1662 case 0 1663 then show ?case 1664 by (cases "finite S") auto 1665 next 1666 case Suc 1667 then show ?case 1668 by (simp add: card_Suc_eq) (metis subset_insertI2) 1669 qed 1670qed 1671 1672subsection \<open>Generic big monoid operation over intervals\<close> 1673 1674context semiring_char_0 1675begin 1676 1677lemma inj_on_of_nat [simp]: 1678 "inj_on of_nat N" 1679 by rule simp 1680 1681lemma bij_betw_of_nat [simp]: 1682 "bij_betw of_nat N A \<longleftrightarrow> of_nat ` N = A" 1683 by (simp add: bij_betw_def) 1684 1685end 1686 1687context comm_monoid_set 1688begin 1689 1690lemma atLeastLessThan_reindex: 1691 "F g {h m..<h n} = F (g \<circ> h) {m..<n}" 1692 if "bij_betw h {m..<n} {h m..<h n}" for m n ::nat 1693proof - 1694 from that have "inj_on h {m..<n}" and "h ` {m..<n} = {h m..<h n}" 1695 by (simp_all add: bij_betw_def) 1696 then show ?thesis 1697 using reindex [of h "{m..<n}" g] by simp 1698qed 1699 1700lemma atLeastAtMost_reindex: 1701 "F g {h m..h n} = F (g \<circ> h) {m..n}" 1702 if "bij_betw h {m..n} {h m..h n}" for m n ::nat 1703proof - 1704 from that have "inj_on h {m..n}" and "h ` {m..n} = {h m..h n}" 1705 by (simp_all add: bij_betw_def) 1706 then show ?thesis 1707 using reindex [of h "{m..n}" g] by simp 1708qed 1709 1710lemma atLeastLessThan_shift_bounds: 1711 "F g {m + k..<n + k} = F (g \<circ> plus k) {m..<n}" 1712 for m n k :: nat 1713 using atLeastLessThan_reindex [of "plus k" m n g] 1714 by (simp add: ac_simps) 1715 1716lemma atLeastAtMost_shift_bounds: 1717 "F g {m + k..n + k} = F (g \<circ> plus k) {m..n}" 1718 for m n k :: nat 1719 using atLeastAtMost_reindex [of "plus k" m n g] 1720 by (simp add: ac_simps) 1721 1722lemma atLeast_Suc_lessThan_Suc_shift: 1723 "F g {Suc m..<Suc n} = F (g \<circ> Suc) {m..<n}" 1724 using atLeastLessThan_shift_bounds [of _ _ 1] 1725 by (simp add: plus_1_eq_Suc) 1726 1727lemma atLeast_Suc_atMost_Suc_shift: 1728 "F g {Suc m..Suc n} = F (g \<circ> Suc) {m..n}" 1729 using atLeastAtMost_shift_bounds [of _ _ 1] 1730 by (simp add: plus_1_eq_Suc) 1731 1732lemma atLeast_int_lessThan_int_shift: 1733 "F g {int m..<int n} = F (g \<circ> int) {m..<n}" 1734 by (rule atLeastLessThan_reindex) 1735 (simp add: image_int_atLeastLessThan) 1736 1737lemma atLeast_int_atMost_int_shift: 1738 "F g {int m..int n} = F (g \<circ> int) {m..n}" 1739 by (rule atLeastAtMost_reindex) 1740 (simp add: image_int_atLeastAtMost) 1741 1742lemma atLeast0_lessThan_Suc: 1743 "F g {0..<Suc n} = F g {0..<n} \<^bold>* g n" 1744 by (simp add: atLeast0_lessThan_Suc ac_simps) 1745 1746lemma atLeast0_atMost_Suc: 1747 "F g {0..Suc n} = F g {0..n} \<^bold>* g (Suc n)" 1748 by (simp add: atLeast0_atMost_Suc ac_simps) 1749 1750lemma atLeast0_lessThan_Suc_shift: 1751 "F g {0..<Suc n} = g 0 \<^bold>* F (g \<circ> Suc) {0..<n}" 1752 by (simp add: atLeast0_lessThan_Suc_eq_insert_0 atLeast_Suc_lessThan_Suc_shift) 1753 1754lemma atLeast0_atMost_Suc_shift: 1755 "F g {0..Suc n} = g 0 \<^bold>* F (g \<circ> Suc) {0..n}" 1756 by (simp add: atLeast0_atMost_Suc_eq_insert_0 atLeast_Suc_atMost_Suc_shift) 1757 1758lemma atLeast_Suc_lessThan: 1759 "F g {m..<n} = g m \<^bold>* F g {Suc m..<n}" if "m < n" 1760proof - 1761 from that have "{m..<n} = insert m {Suc m..<n}" 1762 by auto 1763 then show ?thesis by simp 1764qed 1765 1766lemma atLeast_Suc_atMost: 1767 "F g {m..n} = g m \<^bold>* F g {Suc m..n}" if "m \<le> n" 1768proof - 1769 from that have "{m..n} = insert m {Suc m..n}" 1770 by auto 1771 then show ?thesis by simp 1772qed 1773 1774lemma ivl_cong: 1775 "a = c \<Longrightarrow> b = d \<Longrightarrow> (\<And>x. c \<le> x \<Longrightarrow> x < d \<Longrightarrow> g x = h x) 1776 \<Longrightarrow> F g {a..<b} = F h {c..<d}" 1777 by (rule cong) simp_all 1778 1779lemma atLeastLessThan_shift_0: 1780 fixes m n p :: nat 1781 shows "F g {m..<n} = F (g \<circ> plus m) {0..<n - m}" 1782 using atLeastLessThan_shift_bounds [of g 0 m "n - m"] 1783 by (cases "m \<le> n") simp_all 1784 1785lemma atLeastAtMost_shift_0: 1786 fixes m n p :: nat 1787 assumes "m \<le> n" 1788 shows "F g {m..n} = F (g \<circ> plus m) {0..n - m}" 1789 using assms atLeastAtMost_shift_bounds [of g 0 m "n - m"] by simp 1790 1791lemma atLeastLessThan_concat: 1792 fixes m n p :: nat 1793 shows "m \<le> n \<Longrightarrow> n \<le> p \<Longrightarrow> F g {m..<n} \<^bold>* F g {n..<p} = F g {m..<p}" 1794 by (simp add: union_disjoint [symmetric] ivl_disj_un) 1795 1796lemma atLeastLessThan_rev: 1797 "F g {n..<m} = F (\<lambda>i. g (m + n - Suc i)) {n..<m}" 1798 by (rule reindex_bij_witness [where i="\<lambda>i. m + n - Suc i" and j="\<lambda>i. m + n - Suc i"], auto) 1799 1800lemma atLeastAtMost_rev: 1801 fixes n m :: nat 1802 shows "F g {n..m} = F (\<lambda>i. g (m + n - i)) {n..m}" 1803 by (rule reindex_bij_witness [where i="\<lambda>i. m + n - i" and j="\<lambda>i. m + n - i"]) auto 1804 1805lemma atLeastLessThan_rev_at_least_Suc_atMost: 1806 "F g {n..<m} = F (\<lambda>i. g (m + n - i)) {Suc n..m}" 1807 unfolding atLeastLessThan_rev [of g n m] 1808 by (cases m) (simp_all add: atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost) 1809 1810end 1811 1812 1813subsection \<open>Summation indexed over intervals\<close> 1814 1815syntax (ASCII) 1816 "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) 1817 "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) 1818 "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10) 1819 "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<=_./ _)" [0,0,10] 10) 1820 1821syntax (latex_sum output) 1822 "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 1823 ("(3\<^latex>\<open>$\\sum_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10) 1824 "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 1825 ("(3\<^latex>\<open>$\\sum_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10) 1826 "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 1827 ("(3\<^latex>\<open>$\\sum_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10) 1828 "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 1829 ("(3\<^latex>\<open>$\\sum_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10) 1830 1831syntax 1832 "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) 1833 "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) 1834 "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) 1835 "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10) 1836 1837translations 1838 "\<Sum>x=a..b. t" == "CONST sum (\<lambda>x. t) {a..b}" 1839 "\<Sum>x=a..<b. t" == "CONST sum (\<lambda>x. t) {a..<b}" 1840 "\<Sum>i\<le>n. t" == "CONST sum (\<lambda>i. t) {..n}" 1841 "\<Sum>i<n. t" == "CONST sum (\<lambda>i. t) {..<n}" 1842 1843text\<open>The above introduces some pretty alternative syntaxes for 1844summation over intervals: 1845\begin{center} 1846\begin{tabular}{lll} 1847Old & New & \LaTeX\\ 1848@{term[source]"\<Sum>x\<in>{a..b}. e"} & \<^term>\<open>\<Sum>x=a..b. e\<close> & @{term[mode=latex_sum]"\<Sum>x=a..b. e"}\\ 1849@{term[source]"\<Sum>x\<in>{a..<b}. e"} & \<^term>\<open>\<Sum>x=a..<b. e\<close> & @{term[mode=latex_sum]"\<Sum>x=a..<b. e"}\\ 1850@{term[source]"\<Sum>x\<in>{..b}. e"} & \<^term>\<open>\<Sum>x\<le>b. e\<close> & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 1851@{term[source]"\<Sum>x\<in>{..<b}. e"} & \<^term>\<open>\<Sum>x<b. e\<close> & @{term[mode=latex_sum]"\<Sum>x<b. e"} 1852\end{tabular} 1853\end{center} 1854The left column shows the term before introduction of the new syntax, 1855the middle column shows the new (default) syntax, and the right column 1856shows a special syntax. The latter is only meaningful for latex output 1857and has to be activated explicitly by setting the print mode to 1858\<open>latex_sum\<close> (e.g.\ via \<open>mode = latex_sum\<close> in 1859antiquotations). It is not the default \LaTeX\ output because it only 1860works well with italic-style formulae, not tt-style. 1861 1862Note that for uniformity on \<^typ>\<open>nat\<close> it is better to use 1863\<^term>\<open>\<Sum>x::nat=0..<n. e\<close> rather than \<open>\<Sum>x<n. e\<close>: \<open>sum\<close> may 1864not provide all lemmas available for \<^term>\<open>{m..<n}\<close> also in the 1865special form for \<^term>\<open>{..<n}\<close>.\<close> 1866 1867text\<open>This congruence rule should be used for sums over intervals as 1868the standard theorem @{text[source]sum.cong} does not work well 1869with the simplifier who adds the unsimplified premise \<^term>\<open>x\<in>B\<close> to 1870the context.\<close> 1871 1872context comm_monoid_set 1873begin 1874 1875lemma zero_middle: 1876 assumes "1 \<le> p" "k \<le> p" 1877 shows "F (\<lambda>j. if j < k then g j else if j = k then \<^bold>1 else h (j - Suc 0)) {..p} 1878 = F (\<lambda>j. if j < k then g j else h j) {..p - Suc 0}" (is "?lhs = ?rhs") 1879proof - 1880 have [simp]: "{..p - Suc 0} \<inter> {j. j < k} = {..<k}" "{..p - Suc 0} \<inter> - {j. j < k} = {k..p - Suc 0}" 1881 using assms by auto 1882 have "?lhs = F g {..<k} \<^bold>* F (\<lambda>j. if j = k then \<^bold>1 else h (j - Suc 0)) {k..p}" 1883 using union_disjoint [of "{..<k}" "{k..p}"] assms 1884 by (simp add: ivl_disj_int_one ivl_disj_un_one) 1885 also have "\<dots> = F g {..<k} \<^bold>* F (\<lambda>j. h (j - Suc 0)) {Suc k..p}" 1886 by (simp add: atLeast_Suc_atMost [of k p] assms) 1887 also have "\<dots> = F g {..<k} \<^bold>* F h {k .. p - Suc 0}" 1888 using reindex [of Suc "{k..p - Suc 0}"] assms by simp 1889 also have "\<dots> = ?rhs" 1890 by (simp add: If_cases) 1891 finally show ?thesis . 1892qed 1893 1894lemma atMost_Suc [simp]: 1895 "F g {..Suc n} = F g {..n} \<^bold>* g (Suc n)" 1896 by (simp add: atMost_Suc ac_simps) 1897 1898lemma lessThan_Suc [simp]: 1899 "F g {..<Suc n} = F g {..<n} \<^bold>* g n" 1900 by (simp add: lessThan_Suc ac_simps) 1901 1902lemma cl_ivl_Suc [simp]: 1903 "F g {m..Suc n} = (if Suc n < m then \<^bold>1 else F g {m..n} \<^bold>* g(Suc n))" 1904 by (auto simp: ac_simps atLeastAtMostSuc_conv) 1905 1906lemma op_ivl_Suc [simp]: 1907 "F g {m..<Suc n} = (if n < m then \<^bold>1 else F g {m..<n} \<^bold>* g(n))" 1908 by (auto simp: ac_simps atLeastLessThanSuc) 1909 1910lemma head: 1911 fixes n :: nat 1912 assumes mn: "m \<le> n" 1913 shows "F g {m..n} = g m \<^bold>* F g {m<..n}" (is "?lhs = ?rhs") 1914proof - 1915 from mn 1916 have "{m..n} = {m} \<union> {m<..n}" 1917 by (auto intro: ivl_disj_un_singleton) 1918 hence "?lhs = F g ({m} \<union> {m<..n})" 1919 by (simp add: atLeast0LessThan) 1920 also have "\<dots> = ?rhs" by simp 1921 finally show ?thesis . 1922qed 1923 1924lemma ub_add_nat: 1925 assumes "(m::nat) \<le> n + 1" 1926 shows "F g {m..n + p} = F g {m..n} \<^bold>* F g {n + 1..n + p}" 1927proof- 1928 have "{m .. n+p} = {m..n} \<union> {n+1..n+p}" using \<open>m \<le> n+1\<close> by auto 1929 thus ?thesis by (auto simp: ivl_disj_int union_disjoint atLeastSucAtMost_greaterThanAtMost) 1930qed 1931 1932lemma nat_group: 1933 fixes k::nat shows "F (\<lambda>m. F g {m * k ..< m*k + k}) {..<n} = F g {..< n * k}" 1934proof (cases k) 1935 case (Suc l) 1936 then have "k > 0" 1937 by auto 1938 then show ?thesis 1939 by (induct n) (simp_all add: atLeastLessThan_concat add.commute atLeast0LessThan[symmetric]) 1940qed auto 1941 1942lemma triangle_reindex: 1943 fixes n :: nat 1944 shows "F (\<lambda>(i,j). g i j) {(i,j). i+j < n} = F (\<lambda>k. F (\<lambda>i. g i (k - i)) {..k}) {..<n}" 1945 apply (simp add: Sigma) 1946 apply (rule reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"]) 1947 apply auto 1948 done 1949 1950lemma triangle_reindex_eq: 1951 fixes n :: nat 1952 shows "F (\<lambda>(i,j). g i j) {(i,j). i+j \<le> n} = F (\<lambda>k. F (\<lambda>i. g i (k - i)) {..k}) {..n}" 1953using triangle_reindex [of g "Suc n"] 1954by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost) 1955 1956lemma nat_diff_reindex: "F (\<lambda>i. g (n - Suc i)) {..<n} = F g {..<n}" 1957 by (rule reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto 1958 1959lemma shift_bounds_nat_ivl: 1960 "F g {m+k..<n+k} = F (\<lambda>i. g(i + k)){m..<n::nat}" 1961by (induct "n", auto simp: atLeastLessThanSuc) 1962 1963lemma shift_bounds_cl_nat_ivl: 1964 "F g {m+k..n+k} = F (\<lambda>i. g(i + k)){m..n::nat}" 1965 by (rule reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto 1966 1967corollary shift_bounds_cl_Suc_ivl: 1968 "F g {Suc m..Suc n} = F (\<lambda>i. g(Suc i)){m..n}" 1969by (simp add: shift_bounds_cl_nat_ivl[where k="Suc 0", simplified]) 1970 1971corollary Suc_reindex_ivl: "m \<le> n \<Longrightarrow> F g {m..n} \<^bold>* g (Suc n) = g m \<^bold>* F (\<lambda>i. g (Suc i)) {m..n}" 1972 by (simp add: assoc atLeast_Suc_atMost flip: shift_bounds_cl_Suc_ivl) 1973 1974corollary shift_bounds_Suc_ivl: 1975 "F g {Suc m..<Suc n} = F (\<lambda>i. g(Suc i)){m..<n}" 1976by (simp add: shift_bounds_nat_ivl[where k="Suc 0", simplified]) 1977 1978lemma atMost_Suc_shift: 1979 shows "F g {..Suc n} = g 0 \<^bold>* F (\<lambda>i. g (Suc i)) {..n}" 1980proof (induct n) 1981 case 0 show ?case by simp 1982next 1983 case (Suc n) note IH = this 1984 have "F g {..Suc (Suc n)} = F g {..Suc n} \<^bold>* g (Suc (Suc n))" 1985 by (rule atMost_Suc) 1986 also have "F g {..Suc n} = g 0 \<^bold>* F (\<lambda>i. g (Suc i)) {..n}" 1987 by (rule IH) 1988 also have "g 0 \<^bold>* F (\<lambda>i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)) = 1989 g 0 \<^bold>* (F (\<lambda>i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)))" 1990 by (rule assoc) 1991 also have "F (\<lambda>i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)) = F (\<lambda>i. g (Suc i)) {..Suc n}" 1992 by (rule atMost_Suc [symmetric]) 1993 finally show ?case . 1994qed 1995 1996lemma lessThan_Suc_shift: 1997 "F g {..<Suc n} = g 0 \<^bold>* F (\<lambda>i. g (Suc i)) {..<n}" 1998 by (induction n) (simp_all add: ac_simps) 1999 2000lemma atMost_shift: 2001 "F g {..n} = g 0 \<^bold>* F (\<lambda>i. g (Suc i)) {..<n}" 2002 by (metis atLeast0AtMost atLeast0LessThan atLeastLessThanSuc_atLeastAtMost 2003 atLeastSucAtMost_greaterThanAtMost le0 head shift_bounds_Suc_ivl) 2004 2005lemma last_plus: 2006 fixes n::nat shows "m \<le> n \<Longrightarrow> F g {m..n} = g n \<^bold>* F g {m..<n}" 2007 by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost commute) 2008 2009lemma nested_swap: 2010 "F (\<lambda>i. F (\<lambda>j. a i j) {0..<i}) {0..n} = F (\<lambda>j. F (\<lambda>i. a i j) {Suc j..n}) {0..<n}" 2011 by (induction n) (auto simp: distrib) 2012 2013lemma nested_swap': 2014 "F (\<lambda>i. F (\<lambda>j. a i j) {..<i}) {..n} = F (\<lambda>j. F (\<lambda>i. a i j) {Suc j..n}) {..<n}" 2015 by (induction n) (auto simp: distrib) 2016 2017lemma atLeast1_atMost_eq: 2018 "F g {Suc 0..n} = F (\<lambda>k. g (Suc k)) {..<n}" 2019proof - 2020 have "F g {Suc 0..n} = F g (Suc ` {..<n})" 2021 by (simp add: image_Suc_lessThan) 2022 also have "\<dots> = F (\<lambda>k. g (Suc k)) {..<n}" 2023 by (simp add: reindex) 2024 finally show ?thesis . 2025qed 2026 2027lemma atLeastLessThan_Suc: "a \<le> b \<Longrightarrow> F g {a..<Suc b} = F g {a..<b} \<^bold>* g b" 2028 by (simp add: atLeastLessThanSuc commute) 2029 2030lemma nat_ivl_Suc': 2031 assumes "m \<le> Suc n" 2032 shows "F g {m..Suc n} = g (Suc n) \<^bold>* F g {m..n}" 2033proof - 2034 from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto 2035 also have "F g \<dots> = g (Suc n) \<^bold>* F g {m..n}" by simp 2036 finally show ?thesis . 2037qed 2038 2039lemma in_pairs: "F g {2*m..Suc(2*n)} = F (\<lambda>i. g(2*i) \<^bold>* g(Suc(2*i))) {m..n}" 2040proof (induction n) 2041 case 0 2042 show ?case 2043 by (cases "m=0") auto 2044next 2045 case (Suc n) 2046 then show ?case 2047 by (auto simp: assoc split: if_split_asm) 2048qed 2049 2050lemma in_pairs_0: "F g {..Suc(2*n)} = F (\<lambda>i. g(2*i) \<^bold>* g(Suc(2*i))) {..n}" 2051 using in_pairs [of _ 0 n] by (simp add: atLeast0AtMost) 2052 2053end 2054 2055lemma sum_natinterval_diff: 2056 fixes f:: "nat \<Rightarrow> ('a::ab_group_add)" 2057 shows "sum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} = 2058 (if m \<le> n then f m - f(n + 1) else 0)" 2059by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) 2060 2061lemma sum_diff_nat_ivl: 2062 fixes f :: "nat \<Rightarrow> 'a::ab_group_add" 2063 shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> sum f {m..<p} - sum f {m..<n} = sum f {n..<p}" 2064 using sum.atLeastLessThan_concat [of m n p f,symmetric] 2065 by (simp add: ac_simps) 2066 2067lemma sum_diff_distrib: "\<forall>x. Q x \<le> P x \<Longrightarrow> (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x :: nat)" 2068 by (subst sum_subtractf_nat) auto 2069 2070 2071context unique_euclidean_semiring_with_bit_shifts 2072begin 2073 2074lemma take_bit_sum: 2075 "take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))" 2076 for n :: nat 2077proof (induction n arbitrary: a) 2078 case 0 2079 then show ?case 2080 by simp 2081next 2082 case (Suc n) 2083 have "(\<Sum>k = 0..<Suc n. push_bit k (of_bool (bit a k))) = 2084 of_bool (odd a) + (\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (bit a k)))" 2085 by (simp add: sum.atLeast_Suc_lessThan ac_simps) 2086 also have "(\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (bit a k))) 2087 = (\<Sum>k = 0..<n. push_bit k (of_bool (bit (a div 2) k))) * 2" 2088 by (simp only: sum.atLeast_Suc_lessThan_Suc_shift) (simp add: sum_distrib_right push_bit_double drop_bit_Suc bit_Suc) 2089 finally show ?case 2090 using Suc [of "a div 2"] by (simp add: ac_simps take_bit_Suc) 2091qed 2092 2093end 2094 2095 2096subsubsection \<open>Shifting bounds\<close> 2097 2098context comm_monoid_add 2099begin 2100 2101context 2102 fixes f :: "nat \<Rightarrow> 'a" 2103 assumes "f 0 = 0" 2104begin 2105 2106lemma sum_shift_lb_Suc0_0_upt: 2107 "sum f {Suc 0..<k} = sum f {0..<k}" 2108proof (cases k) 2109 case 0 2110 then show ?thesis 2111 by simp 2112next 2113 case (Suc k) 2114 moreover have "{0..<Suc k} = insert 0 {Suc 0..<Suc k}" 2115 by auto 2116 ultimately show ?thesis 2117 using \<open>f 0 = 0\<close> by simp 2118qed 2119 2120lemma sum_shift_lb_Suc0_0: "sum f {Suc 0..k} = sum f {0..k}" 2121proof (cases k) 2122 case 0 2123 with \<open>f 0 = 0\<close> show ?thesis 2124 by simp 2125next 2126 case (Suc k) 2127 moreover have "{0..Suc k} = insert 0 {Suc 0..Suc k}" 2128 by auto 2129 ultimately show ?thesis 2130 using \<open>f 0 = 0\<close> by simp 2131qed 2132 2133end 2134 2135end 2136 2137lemma sum_Suc_diff: 2138 fixes f :: "nat \<Rightarrow> 'a::ab_group_add" 2139 assumes "m \<le> Suc n" 2140 shows "(\<Sum>i = m..n. f(Suc i) - f i) = f (Suc n) - f m" 2141using assms by (induct n) (auto simp: le_Suc_eq) 2142 2143lemma sum_Suc_diff': 2144 fixes f :: "nat \<Rightarrow> 'a::ab_group_add" 2145 assumes "m \<le> n" 2146 shows "(\<Sum>i = m..<n. f (Suc i) - f i) = f n - f m" 2147using assms by (induct n) (auto simp: le_Suc_eq) 2148 2149 2150subsubsection \<open>Telescoping\<close> 2151 2152lemma sum_telescope: 2153 fixes f::"nat \<Rightarrow> 'a::ab_group_add" 2154 shows "sum (\<lambda>i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)" 2155 by (induct i) simp_all 2156 2157lemma sum_telescope'': 2158 assumes "m \<le> n" 2159 shows "(\<Sum>k\<in>{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)" 2160 by (rule dec_induct[OF assms]) (simp_all add: algebra_simps) 2161 2162lemma sum_lessThan_telescope: 2163 "(\<Sum>n<m. f (Suc n) - f n :: 'a :: ab_group_add) = f m - f 0" 2164 by (induction m) (simp_all add: algebra_simps) 2165 2166lemma sum_lessThan_telescope': 2167 "(\<Sum>n<m. f n - f (Suc n) :: 'a :: ab_group_add) = f 0 - f m" 2168 by (induction m) (simp_all add: algebra_simps) 2169 2170 2171subsubsection \<open>The formula for geometric sums\<close> 2172 2173lemma sum_power2: "(\<Sum>i=0..<k. (2::nat)^i) = 2^k-1" 2174by (induction k) (auto simp: mult_2) 2175 2176lemma geometric_sum: 2177 assumes "x \<noteq> 1" 2178 shows "(\<Sum>i<n. x ^ i) = (x ^ n - 1) / (x - 1::'a::field)" 2179proof - 2180 from assms obtain y where "y = x - 1" and "y \<noteq> 0" by simp_all 2181 moreover have "(\<Sum>i<n. (y + 1) ^ i) = ((y + 1) ^ n - 1) / y" 2182 by (induct n) (simp_all add: field_simps \<open>y \<noteq> 0\<close>) 2183 ultimately show ?thesis by simp 2184qed 2185 2186lemma diff_power_eq_sum: 2187 fixes y :: "'a::{comm_ring,monoid_mult}" 2188 shows 2189 "x ^ (Suc n) - y ^ (Suc n) = 2190 (x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))" 2191proof (induct n) 2192 case (Suc n) 2193 have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x^n) - y * (y * y ^ n)" 2194 by simp 2195 also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x^n)" 2196 by (simp add: algebra_simps) 2197 also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)" 2198 by (simp only: Suc) 2199 also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)" 2200 by (simp only: mult.left_commute) 2201 also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))" 2202 by (simp add: field_simps Suc_diff_le sum_distrib_right sum_distrib_left) 2203 finally show ?case . 2204qed simp 2205 2206corollary power_diff_sumr2: \<comment> \<open>\<open>COMPLEX_POLYFUN\<close> in HOL Light\<close> 2207 fixes x :: "'a::{comm_ring,monoid_mult}" 2208 shows "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)" 2209using diff_power_eq_sum[of x "n - 1" y] 2210by (cases "n = 0") (simp_all add: field_simps) 2211 2212lemma power_diff_1_eq: 2213 fixes x :: "'a::{comm_ring,monoid_mult}" 2214 shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i<n. (x^i))" 2215using diff_power_eq_sum [of x _ 1] 2216 by (cases n) auto 2217 2218lemma one_diff_power_eq': 2219 fixes x :: "'a::{comm_ring,monoid_mult}" 2220 shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^(n - Suc i))" 2221using diff_power_eq_sum [of 1 _ x] 2222 by (cases n) auto 2223 2224lemma one_diff_power_eq: 2225 fixes x :: "'a::{comm_ring,monoid_mult}" 2226 shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)" 2227by (metis one_diff_power_eq' [of n x] sum.nat_diff_reindex) 2228 2229lemma sum_gp_basic: 2230 fixes x :: "'a::{comm_ring,monoid_mult}" 2231 shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n" 2232 by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost) 2233 2234lemma sum_power_shift: 2235 fixes x :: "'a::{comm_ring,monoid_mult}" 2236 assumes "m \<le> n" 2237 shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)" 2238proof - 2239 have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))" 2240 by (simp add: sum_distrib_left power_add [symmetric]) 2241 also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)" 2242 using \<open>m \<le> n\<close> by (intro sum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto 2243 finally show ?thesis . 2244qed 2245 2246lemma sum_gp_multiplied: 2247 fixes x :: "'a::{comm_ring,monoid_mult}" 2248 assumes "m \<le> n" 2249 shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n" 2250proof - 2251 have "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)" 2252 by (metis mult.assoc mult.commute assms sum_power_shift) 2253 also have "... =x^m * (1 - x^Suc(n-m))" 2254 by (metis mult.assoc sum_gp_basic) 2255 also have "... = x^m - x^Suc n" 2256 using assms 2257 by (simp add: algebra_simps) (metis le_add_diff_inverse power_add) 2258 finally show ?thesis . 2259qed 2260 2261lemma sum_gp: 2262 fixes x :: "'a::{comm_ring,division_ring}" 2263 shows "(\<Sum>i=m..n. x^i) = 2264 (if n < m then 0 2265 else if x = 1 then of_nat((n + 1) - m) 2266 else (x^m - x^Suc n) / (1 - x))" 2267using sum_gp_multiplied [of m n x] apply auto 2268by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq) 2269 2270 2271subsubsection\<open>Geometric progressions\<close> 2272 2273lemma sum_gp0: 2274 fixes x :: "'a::{comm_ring,division_ring}" 2275 shows "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))" 2276 using sum_gp_basic[of x n] 2277 by (simp add: mult.commute field_split_simps) 2278 2279lemma sum_power_add: 2280 fixes x :: "'a::{comm_ring,monoid_mult}" 2281 shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)" 2282 by (simp add: sum_distrib_left power_add) 2283 2284lemma sum_gp_offset: 2285 fixes x :: "'a::{comm_ring,division_ring}" 2286 shows "(\<Sum>i=m..m+n. x^i) = 2287 (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))" 2288 using sum_gp [of x m "m+n"] 2289 by (auto simp: power_add algebra_simps) 2290 2291lemma sum_gp_strict: 2292 fixes x :: "'a::{comm_ring,division_ring}" 2293 shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))" 2294 by (induct n) (auto simp: algebra_simps field_split_simps) 2295 2296 2297subsubsection \<open>The formulae for arithmetic sums\<close> 2298 2299context comm_semiring_1 2300begin 2301 2302lemma double_gauss_sum: 2303 "2 * (\<Sum>i = 0..n. of_nat i) = of_nat n * (of_nat n + 1)" 2304 by (induct n) (simp_all add: sum.atLeast0_atMost_Suc algebra_simps left_add_twice) 2305 2306lemma double_gauss_sum_from_Suc_0: 2307 "2 * (\<Sum>i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1)" 2308proof - 2309 have "sum of_nat {Suc 0..n} = sum of_nat (insert 0 {Suc 0..n})" 2310 by simp 2311 also have "\<dots> = sum of_nat {0..n}" 2312 by (cases n) (simp_all add: atLeast0_atMost_Suc_eq_insert_0) 2313 finally show ?thesis 2314 by (simp add: double_gauss_sum) 2315qed 2316 2317lemma double_arith_series: 2318 "2 * (\<Sum>i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d)" 2319proof - 2320 have "(\<Sum>i = 0..n. a + of_nat i * d) = ((\<Sum>i = 0..n. a) + (\<Sum>i = 0..n. of_nat i * d))" 2321 by (rule sum.distrib) 2322 also have "\<dots> = (of_nat (Suc n) * a + d * (\<Sum>i = 0..n. of_nat i))" 2323 by (simp add: sum_distrib_left algebra_simps) 2324 finally show ?thesis 2325 by (simp add: algebra_simps double_gauss_sum left_add_twice) 2326qed 2327 2328end 2329 2330context unique_euclidean_semiring_with_nat 2331begin 2332 2333lemma gauss_sum: 2334 "(\<Sum>i = 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2" 2335 using double_gauss_sum [of n, symmetric] by simp 2336 2337lemma gauss_sum_from_Suc_0: 2338 "(\<Sum>i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2" 2339 using double_gauss_sum_from_Suc_0 [of n, symmetric] by simp 2340 2341lemma arith_series: 2342 "(\<Sum>i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d) div 2" 2343 using double_arith_series [of a d n, symmetric] by simp 2344 2345end 2346 2347lemma gauss_sum_nat: 2348 "\<Sum>{0..n} = (n * Suc n) div 2" 2349 using gauss_sum [of n, where ?'a = nat] by simp 2350 2351lemma arith_series_nat: 2352 "(\<Sum>i = 0..n. a + i * d) = Suc n * (2 * a + n * d) div 2" 2353 using arith_series [of a d n] by simp 2354 2355lemma Sum_Icc_int: 2356 "\<Sum>{m..n} = (n * (n + 1) - m * (m - 1)) div 2" 2357 if "m \<le> n" for m n :: int 2358using that proof (induct i \<equiv> "nat (n - m)" arbitrary: m n) 2359 case 0 2360 then have "m = n" 2361 by arith 2362 then show ?case 2363 by (simp add: algebra_simps mult_2 [symmetric]) 2364next 2365 case (Suc i) 2366 have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+ 2367 have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp 2368 also have "\<dots> = \<Sum> {m..n-1} + n" using \<open>m \<le> n\<close> 2369 by(subst atLeastAtMostPlus1_int_conv) simp_all 2370 also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n" 2371 by(simp add: Suc(1)[OF 0]) 2372 also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp 2373 also have "\<dots> = (n*(n+1) - m*(m-1)) div 2" 2374 by (simp add: algebra_simps mult_2_right) 2375 finally show ?case . 2376qed 2377 2378lemma Sum_Icc_nat: 2379 "\<Sum>{m..n} = (n * (n + 1) - m * (m - 1)) div 2" for m n :: nat 2380proof (cases "m \<le> n") 2381 case True 2382 then have *: "m * (m - 1) \<le> n * (n + 1)" 2383 by (meson diff_le_self order_trans le_add1 mult_le_mono) 2384 have "int (\<Sum>{m..n}) = (\<Sum>{int m..int n})" 2385 by (simp add: sum.atLeast_int_atMost_int_shift) 2386 also have "\<dots> = (int n * (int n + 1) - int m * (int m - 1)) div 2" 2387 using \<open>m \<le> n\<close> by (simp add: Sum_Icc_int) 2388 also have "\<dots> = int ((n * (n + 1) - m * (m - 1)) div 2)" 2389 using le_square * by (simp add: algebra_simps of_nat_div of_nat_diff) 2390 finally show ?thesis 2391 by (simp only: of_nat_eq_iff) 2392next 2393 case False 2394 then show ?thesis 2395 by (auto dest: less_imp_Suc_add simp add: not_le algebra_simps) 2396qed 2397 2398lemma Sum_Ico_nat: 2399 "\<Sum>{m..<n} = (n * (n - 1) - m * (m - 1)) div 2" for m n :: nat 2400 by (cases n) (simp_all add: atLeastLessThanSuc_atLeastAtMost Sum_Icc_nat) 2401 2402 2403subsubsection \<open>Division remainder\<close> 2404 2405lemma range_mod: 2406 fixes n :: nat 2407 assumes "n > 0" 2408 shows "range (\<lambda>m. m mod n) = {0..<n}" (is "?A = ?B") 2409proof (rule set_eqI) 2410 fix m 2411 show "m \<in> ?A \<longleftrightarrow> m \<in> ?B" 2412 proof 2413 assume "m \<in> ?A" 2414 with assms show "m \<in> ?B" 2415 by auto 2416 next 2417 assume "m \<in> ?B" 2418 moreover have "m mod n \<in> ?A" 2419 by (rule rangeI) 2420 ultimately show "m \<in> ?A" 2421 by simp 2422 qed 2423qed 2424 2425 2426subsection \<open>Products indexed over intervals\<close> 2427 2428syntax (ASCII) 2429 "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10) 2430 "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10) 2431 "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10) 2432 "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10) 2433 2434syntax (latex_prod output) 2435 "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 2436 ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10) 2437 "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 2438 ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10) 2439 "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 2440 ("(3\<^latex>\<open>$\\prod_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10) 2441 "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 2442 ("(3\<^latex>\<open>$\\prod_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10) 2443 2444syntax 2445 "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10) 2446 "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10) 2447 "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10) 2448 "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10) 2449 2450translations 2451 "\<Prod>x=a..b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..b}" 2452 "\<Prod>x=a..<b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..<b}" 2453 "\<Prod>i\<le>n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..n}" 2454 "\<Prod>i<n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..<n}" 2455 2456lemma prod_int_plus_eq: "prod int {i..i+j} = \<Prod>{int i..int (i+j)}" 2457 by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv) 2458 2459lemma prod_int_eq: "prod int {i..j} = \<Prod>{int i..int j}" 2460proof (cases "i \<le> j") 2461 case True 2462 then show ?thesis 2463 by (metis le_iff_add prod_int_plus_eq) 2464next 2465 case False 2466 then show ?thesis 2467 by auto 2468qed 2469 2470subsection \<open>Efficient folding over intervals\<close> 2471 2472function fold_atLeastAtMost_nat where 2473 [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc = 2474 (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a acc))" 2475by pat_completeness auto 2476termination by (relation "measure (\<lambda>(_,a,b,_). Suc b - a)") auto 2477 2478lemma fold_atLeastAtMost_nat: 2479 assumes "comp_fun_commute f" 2480 shows "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}" 2481using assms 2482proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases) 2483 case (1 f a b acc) 2484 interpret comp_fun_commute f by fact 2485 show ?case 2486 proof (cases "a > b") 2487 case True 2488 thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto 2489 next 2490 case False 2491 with 1 show ?thesis 2492 by (subst fold_atLeastAtMost_nat.simps) 2493 (auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm) 2494 qed 2495qed 2496 2497lemma sum_atLeastAtMost_code: 2498 "sum f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a + acc) a b 0" 2499proof - 2500 have "comp_fun_commute (\<lambda>a. (+) (f a))" 2501 by unfold_locales (auto simp: o_def add_ac) 2502 thus ?thesis 2503 by (simp add: sum.eq_fold fold_atLeastAtMost_nat o_def) 2504qed 2505 2506lemma prod_atLeastAtMost_code: 2507 "prod f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a * acc) a b 1" 2508proof - 2509 have "comp_fun_commute (\<lambda>a. (*) (f a))" 2510 by unfold_locales (auto simp: o_def mult_ac) 2511 thus ?thesis 2512 by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def) 2513qed 2514 2515(* TODO: Add support for folding over more kinds of intervals here *) 2516 2517end 2518