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