src/HOL/SetInterval.thy
 author nipkow Fri Jul 16 11:46:59 2004 +0200 (2004-07-16) changeset 15052 cc562a263609 parent 15048 11b4dce71d73 child 15056 b75073d90bff permissions -rw-r--r--
 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 paulson@14485  12 theory SetInterval = IntArith:  nipkow@8924  13 nipkow@8924  14 constdefs  nipkow@15045  15  lessThan :: "('a::ord) => 'a set" ("(1{..<_})")  nipkow@15045  16  "{.. 'a set" ("(1{.._})")  wenzelm@11609  19  "{..u} == {x. x<=u}"  nipkow@8924  20 nipkow@15045  21  greaterThan :: "('a::ord) => 'a set" ("(1{_<..})")  nipkow@15045  22  "{l<..} == {x. l 'a set" ("(1{_..})")  wenzelm@11609  25  "{l..} == {x. l<=x}"  nipkow@8924  26 nipkow@15045  27  greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{_<..<_})")  nipkow@15045  28  "{l<.. 'a set" ("(1{_..<_})")  nipkow@15045  31  "{l.. 'a set" ("(1{_<.._})")  nipkow@15045  34  "{l<..u} == {l<..} Int {..u}"  ballarin@13735  35 ballarin@13735  36  atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})")  ballarin@13735  37  "{l..u} == {l..} Int {..u}"  ballarin@13735  38 nipkow@15045  39 (* Old syntax, will disappear! *)  nipkow@15045  40 syntax  nipkow@15045  41  "_lessThan" :: "('a::ord) => 'a set" ("(1{.._'(})")  nipkow@15045  42  "_greaterThan" :: "('a::ord) => 'a set" ("(1{')_..})")  nipkow@15045  43  "_greaterThanLessThan" :: "['a::ord, 'a] => 'a set" ("(1{')_.._'(})")  nipkow@15045  44  "_atLeastLessThan" :: "['a::ord, 'a] => 'a set" ("(1{_.._'(})")  nipkow@15045  45  "_greaterThanAtMost" :: "['a::ord, 'a] => 'a set" ("(1{')_.._})")  nipkow@15045  46 translations  nipkow@15045  47  "{..m(}" => "{.. "{m<..}"  nipkow@15045  49  "{)m..n(}" => "{m<.. "{m.. "{m<..n}"  nipkow@15045  52 nipkow@15048  53 nipkow@15048  54 text{* A note of warning when using @{term"{.. nat => 'b set => 'b set" ("(3UN _<=_./ _)" 10)  kleing@14418  60  "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3UN _<_./ _)" 10)  kleing@14418  61  "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10)  kleing@14418  62  "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3INT _<_./ _)" 10)  kleing@14418  63 kleing@14418  64 syntax (input)  kleing@14418  65  "@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10)  kleing@14418  66  "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10)  kleing@14418  67  "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10)  kleing@14418  68  "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10)  kleing@14418  69 kleing@14418  70 syntax (xsymbols)  wenzelm@14846  71  "@UNION_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10)  wenzelm@14846  72  "@UNION_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10)  wenzelm@14846  73  "@INTER_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10)  wenzelm@14846  74  "@INTER_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10)  kleing@14418  75 kleing@14418  76 translations  kleing@14418  77  "UN i<=n. A" == "UN i:{..n}. A"  nipkow@15045  78  "UN i atLeast y) = (y \ (x::'a::order))"  paulson@13850  128 by (blast intro: order_trans)  paulson@13850  129 paulson@13850  130 lemma atLeast_eq_iff [iff]:  paulson@13850  131  "(atLeast x = atLeast y) = (x = (y::'a::linorder))"  paulson@13850  132 by (blast intro: order_antisym order_trans)  paulson@13850  133 paulson@13850  134 lemma greaterThan_subset_iff [iff]:  paulson@13850  135  "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))"  paulson@13850  136 apply (auto simp add: greaterThan_def)  paulson@13850  137  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  138 done  paulson@13850  139 paulson@13850  140 lemma greaterThan_eq_iff [iff]:  paulson@13850  141  "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"  paulson@13850  142 apply (rule iffI)  paulson@13850  143  apply (erule equalityE)  paulson@13850  144  apply (simp add: greaterThan_subset_iff order_antisym, simp)  paulson@13850  145 done  paulson@13850  146 paulson@13850  147 lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))"  paulson@13850  148 by (blast intro: order_trans)  paulson@13850  149 paulson@13850  150 lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"  paulson@13850  151 by (blast intro: order_antisym order_trans)  paulson@13850  152 paulson@13850  153 lemma lessThan_subset_iff [iff]:  paulson@13850  154  "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))"  paulson@13850  155 apply (auto simp add: lessThan_def)  paulson@13850  156  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  157 done  paulson@13850  158 paulson@13850  159 lemma lessThan_eq_iff [iff]:  paulson@13850  160  "(lessThan x = lessThan y) = (x = (y::'a::linorder))"  paulson@13850  161 apply (rule iffI)  paulson@13850  162  apply (erule equalityE)  paulson@13850  163  apply (simp add: lessThan_subset_iff order_antisym, simp)  ballarin@13735  164 done  ballarin@13735  165 ballarin@13735  166 paulson@13850  167 subsection {*Two-sided intervals*}  ballarin@13735  168 wenzelm@14577  169 text {* @{text greaterThanLessThan} *}  ballarin@13735  170 ballarin@13735  171 lemma greaterThanLessThan_iff [simp]:  nipkow@15045  172  "(i : {l<.. m ==> {m.. n then insert n {m.. finite N"  paulson@14485  328  -- {* A bounded set of natural numbers is finite. *}  paulson@14485  329  apply (rule finite_subset)  paulson@14485  330  apply (rule_tac [2] finite_lessThan, auto)  paulson@14485  331  done  paulson@14485  332 paulson@14485  333 subsubsection {* Cardinality *}  paulson@14485  334 nipkow@15045  335 lemma card_lessThan [simp]: "card {.. u ==>  nipkow@15045  379  {(0::int).. u")  paulson@14485  388  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  389  apply (rule finite_imageI)  paulson@14485  390  apply auto  nipkow@15045  391  apply (subgoal_tac "{0.. u")  paulson@14485  423  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  424  apply (subst card_image)  paulson@14485  425  apply (auto simp add: inj_on_def)  paulson@14485  426  done  paulson@14485  427 nipkow@15045  428 lemma card_atLeastLessThan_int [simp]: "card {l.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  465  "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  474  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  476  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  478  "(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  490  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  492 by auto  ballarin@13735  493 ballarin@13735  494 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two  ballarin@13735  495 wenzelm@14577  496 subsubsection {* Disjoint Intersections *}  ballarin@13735  497 wenzelm@14577  498 text {* Singletons and open intervals *}  ballarin@13735  499 ballarin@13735  500 lemma ivl_disj_int_singleton:  nipkow@15045  501  "{l::'a::order} Int {l<..} = {}"  nipkow@15045  502  "{.. 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  542  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@15048  543  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@15042  544 syntax (xsymbols)  nipkow@15042  545  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  546  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@15048  547  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@15042  548 syntax (HTML output)  nipkow@15042  549  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  550  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@15048  551  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@15052  552 syntax (latex output)  nipkow@15052  553  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  554  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@15052  555  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  556  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@15052  557  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@15052  558  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15041  559 nipkow@15048  560 translations  nipkow@15048  561  "\x=a..b. t" == "setsum (%x. t) {a..b}"  nipkow@15048  562  "\x=a..ii. t) {..x\{a..b}. e"} & @{term[source]"\x=a..b. e"} & @{term"\x=a..b. e"}\\  nipkow@15052  571 @{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  583 by (simp add:lessThan_Suc)  nipkow@15041  584 nipkow@8924  585 end