src/HOL/SetInterval.thy
 author paulson Tue Oct 19 18:18:45 2004 +0200 (2004-10-19) changeset 15251 bb6f072c8d10 parent 15140 322485b816ac child 15402 97204f3b4705 permissions -rw-r--r--
converted some induct_tac to induct
 nipkow@8924 1 (* Title: HOL/SetInterval.thy nipkow@8924 2 ID: $Id$ ballarin@13735 3 Author: Tobias Nipkow and Clemens Ballarin paulson@14485 4 Additions by Jeremy Avigad in March 2004 paulson@8957 5 Copyright 2000 TU Muenchen nipkow@8924 6 ballarin@13735 7 lessThan, greaterThan, atLeast, atMost and two-sided intervals nipkow@8924 8 *) nipkow@8924 9 wenzelm@14577 10 header {* Set intervals *} wenzelm@14577 11 nipkow@15131 12 theory SetInterval nipkow@15140 13 imports IntArith nipkow@15131 14 begin nipkow@8924 15 nipkow@8924 16 constdefs nipkow@15045 17 lessThan :: "('a::ord) => 'a set" ("(1{..<_})") nipkow@15045 18 "{.. 'a set" ("(1{.._})") wenzelm@11609 21 "{..u} == {x. x<=u}" nipkow@8924 22 nipkow@15045 23 greaterThan :: "('a::ord) => 'a set" ("(1{_<..})") nipkow@15045 24 "{l<..} == {x. l 'a set" ("(1{_..})") wenzelm@11609 27 "{l..} == {x. l<=x}" nipkow@8924 28 nipkow@15045 29 greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{_<..<_})") nipkow@15045 30 "{l<.. 'a set" ("(1{_..<_})") nipkow@15045 33 "{l.. 'a set" ("(1{_<.._})") nipkow@15045 36 "{l<..u} == {l<..} Int {..u}" ballarin@13735 37 ballarin@13735 38 atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") ballarin@13735 39 "{l..u} == {l..} Int {..u}" ballarin@13735 40 nipkow@15045 41 (* Old syntax, will disappear! *) nipkow@15045 42 syntax nipkow@15045 43 "_lessThan" :: "('a::ord) => 'a set" ("(1{.._'(})") nipkow@15045 44 "_greaterThan" :: "('a::ord) => 'a set" ("(1{')_..})") nipkow@15045 45 "_greaterThanLessThan" :: "['a::ord, 'a] => 'a set" ("(1{')_.._'(})") nipkow@15045 46 "_atLeastLessThan" :: "['a::ord, 'a] => 'a set" ("(1{_.._'(})") nipkow@15045 47 "_greaterThanAtMost" :: "['a::ord, 'a] => 'a set" ("(1{')_.._})") nipkow@15045 48 translations nipkow@15045 49 "{..m(}" => "{.. "{m<..}" nipkow@15045 51 "{)m..n(}" => "{m<.. "{m.. "{m<..n}" nipkow@15045 54 nipkow@15048 55 nipkow@15048 56 text{* A note of warning when using @{term"{.. nat => 'b set => 'b set" ("(3UN _<=_./ _)" 10) kleing@14418 62 "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3UN _<_./ _)" 10) kleing@14418 63 "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10) kleing@14418 64 "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3INT _<_./ _)" 10) kleing@14418 65 kleing@14418 66 syntax (input) kleing@14418 67 "@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10) kleing@14418 68 "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10) kleing@14418 69 "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10) kleing@14418 70 "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10) kleing@14418 71 kleing@14418 72 syntax (xsymbols) wenzelm@14846 73 "@UNION_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10) wenzelm@14846 74 "@UNION_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10) wenzelm@14846 75 "@INTER_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10) wenzelm@14846 76 "@INTER_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10) kleing@14418 77 kleing@14418 78 translations kleing@14418 79 "UN i<=n. A" == "UN i:{..n}. A" nipkow@15045 80 "UN i atLeast y) = (y \ (x::'a::order))" paulson@13850 130 by (blast intro: order_trans) paulson@13850 131 paulson@13850 132 lemma atLeast_eq_iff [iff]: paulson@13850 133 "(atLeast x = atLeast y) = (x = (y::'a::linorder))" paulson@13850 134 by (blast intro: order_antisym order_trans) paulson@13850 135 paulson@13850 136 lemma greaterThan_subset_iff [iff]: paulson@13850 137 "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))" paulson@13850 138 apply (auto simp add: greaterThan_def) paulson@13850 139 apply (subst linorder_not_less [symmetric], blast) paulson@13850 140 done paulson@13850 141 paulson@13850 142 lemma greaterThan_eq_iff [iff]: paulson@13850 143 "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" paulson@13850 144 apply (rule iffI) paulson@13850 145 apply (erule equalityE) paulson@13850 146 apply (simp add: greaterThan_subset_iff order_antisym, simp) paulson@13850 147 done paulson@13850 148 paulson@13850 149 lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))" paulson@13850 150 by (blast intro: order_trans) paulson@13850 151 paulson@13850 152 lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" paulson@13850 153 by (blast intro: order_antisym order_trans) paulson@13850 154 paulson@13850 155 lemma lessThan_subset_iff [iff]: paulson@13850 156 "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))" paulson@13850 157 apply (auto simp add: lessThan_def) paulson@13850 158 apply (subst linorder_not_less [symmetric], blast) paulson@13850 159 done paulson@13850 160 paulson@13850 161 lemma lessThan_eq_iff [iff]: paulson@13850 162 "(lessThan x = lessThan y) = (x = (y::'a::linorder))" paulson@13850 163 apply (rule iffI) paulson@13850 164 apply (erule equalityE) paulson@13850 165 apply (simp add: lessThan_subset_iff order_antisym, simp) ballarin@13735 166 done ballarin@13735 167 ballarin@13735 168 paulson@13850 169 subsection {*Two-sided intervals*} ballarin@13735 170 wenzelm@14577 171 text {* @{text greaterThanLessThan} *} ballarin@13735 172 ballarin@13735 173 lemma greaterThanLessThan_iff [simp]: nipkow@15045 174 "(i : {l<.. m ==> {m.. n then insert n {m.. finite N" paulson@14485 330 -- {* A bounded set of natural numbers is finite. *} paulson@14485 331 apply (rule finite_subset) paulson@14485 332 apply (rule_tac [2] finite_lessThan, auto) paulson@14485 333 done paulson@14485 334 paulson@14485 335 subsubsection {* Cardinality *} paulson@14485 336 nipkow@15045 337 lemma card_lessThan [simp]: "card {.. u ==> nipkow@15045 381 {(0::int).. u") paulson@14485 390 apply (subst image_atLeastZeroLessThan_int, assumption) paulson@14485 391 apply (rule finite_imageI) paulson@14485 392 apply auto nipkow@15045 393 apply (subgoal_tac "{0.. u") paulson@14485 425 apply (subst image_atLeastZeroLessThan_int, assumption) paulson@14485 426 apply (subst card_image) paulson@14485 427 apply (auto simp add: inj_on_def) paulson@14485 428 done paulson@14485 429 nipkow@15045 430 lemma card_atLeastLessThan_int [simp]: "card {l.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}" nipkow@15045 467 "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}" nipkow@15045 476 "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}" nipkow@15045 478 "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}" nipkow@15045 480 "(l::'a::linorder) <= u ==> {l.. {l<.. {l<..m} Un {m<.. {l.. {l..m} Un {m<.. {l<.. {l<..m} Un {m<..u} = {l<..u}" nipkow@15045 492 "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}" ballarin@14398 494 by auto ballarin@13735 495 ballarin@13735 496 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ballarin@13735 497 wenzelm@14577 498 subsubsection {* Disjoint Intersections *} ballarin@13735 499 wenzelm@14577 500 text {* Singletons and open intervals *} ballarin@13735 501 ballarin@13735 502 lemma ivl_disj_int_singleton: nipkow@15045 503 "{l::'a::order} Int {l<..} = {}" nipkow@15045 504 "{.. 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) nipkow@15048 544 "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) nipkow@15048 545 "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10) nipkow@15042 546 syntax (xsymbols) nipkow@15042 547 "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) nipkow@15048 548 "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) nipkow@15048 549 "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) nipkow@15042 550 syntax (HTML output) nipkow@15042 551 "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) nipkow@15048 552 "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) nipkow@15048 553 "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) nipkow@15056 554 syntax (latex_sum output) nipkow@15052 555 "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" nipkow@15052 556 ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) nipkow@15052 557 "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" nipkow@15052 558 ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) nipkow@15052 559 "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" nipkow@15052 560 ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10) nipkow@15041 561 nipkow@15048 562 translations nipkow@15048 563 "\x=a..b. t" == "setsum (%x. t) {a..b}" nipkow@15048 564 "\x=a..ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\ nipkow@15056 573 @{term[source]"\x\{a..x=a..x=a..x\{..xxx::nat=0..xi < Suc n. b i) = b n + (\i < n. b i)" nipkow@15041 592 by (simp add:lessThan_Suc) nipkow@15041 593 nipkow@8924 594 end