src/HOL/SetInterval.thy
 author nipkow Thu Jul 07 12:39:17 2005 +0200 (2005-07-07) changeset 16733 236dfafbeb63 parent 16102 c5f6726d9bb1 child 17149 e2b19c92ef51 permissions -rw-r--r--
linear arithmetic now takes "&" in assumptions apart.
 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@15418  130 by (blast intro: order_trans)  paulson@13850  131 paulson@13850  132 lemma atLeast_eq_iff [iff]:  paulson@15418  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@15418  137  "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))"  paulson@15418  138 apply (auto simp add: greaterThan_def)  paulson@15418  139  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  140 done  paulson@13850  141 paulson@13850  142 lemma greaterThan_eq_iff [iff]:  paulson@15418  143  "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"  paulson@15418  144 apply (rule iffI)  paulson@15418  145  apply (erule equalityE)  paulson@15418  146  apply (simp_all add: greaterThan_subset_iff)  paulson@13850  147 done  paulson@13850  148 paulson@15418  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@15418  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@15418  156  "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))"  paulson@15418  157 apply (auto simp add: lessThan_def)  paulson@15418  158  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  159 done  paulson@13850  160 paulson@13850  161 lemma lessThan_eq_iff [iff]:  paulson@15418  162  "(lessThan x = lessThan y) = (x = (y::'a::linorder))"  paulson@15418  163 apply (rule iffI)  paulson@15418  164  apply (erule equalityE)  paulson@15418  165  apply (simp_all add: lessThan_subset_iff)  ballarin@13735  166 done  ballarin@13735  167 ballarin@13735  168 paulson@13850  169 subsection {*Two-sided intervals*}  ballarin@13735  170 ballarin@13735  171 lemma greaterThanLessThan_iff [simp]:  nipkow@15045  172  "(i : {l<.. {m::'a::order..n} = {}";  nipkow@15554  194  by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);  nipkow@15554  195 nipkow@15554  196 lemma atLeastLessThan_empty[simp]: "n \ m ==> {m.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  301 by (auto simp add: atLeastAtMost_def)  nipkow@15554  302 nipkow@16733  303 subsubsection {* Image *}  nipkow@16733  304 nipkow@16733  305 lemma image_add_atLeastAtMost:  nipkow@16733  306  "(%n::nat. n+k)  {i..j} = {i+k..j+k}" (is "?A = ?B")  nipkow@16733  307 proof  nipkow@16733  308  show "?A \ ?B" by auto  nipkow@16733  309 next  nipkow@16733  310  show "?B \ ?A"  nipkow@16733  311  proof  nipkow@16733  312  fix n assume a: "n : ?B"  nipkow@16733  313  hence "n - k : {i..j}" by auto arith+  nipkow@16733  314  moreover have "n = (n - k) + k" using a by auto  nipkow@16733  315  ultimately show "n : ?A" by blast  nipkow@16733  316  qed  nipkow@16733  317 qed  nipkow@16733  318 nipkow@16733  319 lemma image_add_atLeastLessThan:  nipkow@16733  320  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  323 next  nipkow@16733  324  show "?B \ ?A"  nipkow@16733  325  proof  nipkow@16733  326  fix n assume a: "n : ?B"  nipkow@16733  327  hence "n - k : {i.. finite N"  paulson@14485  375  -- {* A bounded set of natural numbers is finite. *}  paulson@14485  376  apply (rule finite_subset)  paulson@14485  377  apply (rule_tac [2] finite_lessThan, auto)  paulson@14485  378  done  paulson@14485  379 paulson@14485  380 subsubsection {* Cardinality *}  paulson@14485  381 nipkow@15045  382 lemma card_lessThan [simp]: "card {.. u ==>  nipkow@15045  425  {(0::int).. u")  paulson@14485  434  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  435  apply (rule finite_imageI)  paulson@14485  436  apply auto  paulson@14485  437  done  paulson@14485  438 nipkow@15045  439 lemma finite_atLeastLessThan_int [iff]: "finite {l.. u")  paulson@14485  460  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  461  apply (subst card_image)  paulson@14485  462  apply (auto simp add: inj_on_def)  paulson@14485  463  done  paulson@14485  464 nipkow@15045  465 lemma card_atLeastLessThan_int [simp]: "card {l.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  501  "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  510  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  512  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  514  "(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  526  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  528 by auto  ballarin@13735  529 ballarin@13735  530 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two  ballarin@13735  531 wenzelm@14577  532 subsubsection {* Disjoint Intersections *}  ballarin@13735  533 wenzelm@14577  534 text {* Singletons and open intervals *}  ballarin@13735  535 ballarin@13735  536 lemma ivl_disj_int_singleton:  nipkow@15045  537  "{l::'a::order} Int {l<..} = {}"  nipkow@15045  538  "{.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  584 apply(auto simp:linorder_not_le)  nipkow@15542  585 apply(rule ccontr)  nipkow@15542  586 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  587 apply(clarsimp simp:linorder_not_le)  nipkow@15542  588 apply(fastsimp)  nipkow@15542  589 done  nipkow@15542  590 nipkow@15041  591 nipkow@15042  592 subsection {* Summation indexed over intervals *}  nipkow@15042  593 nipkow@15042  594 syntax  nipkow@15042  595  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  596  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  597  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@16052  598  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  nipkow@15042  599 syntax (xsymbols)  nipkow@15042  600  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  601  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  602  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  603  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15042  604 syntax (HTML output)  nipkow@15042  605  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  606  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  607  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  608  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15056  609 syntax (latex_sum output)  nipkow@15052  610  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  611  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@15052  612  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  613  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@16052  614  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  615  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15052  616  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  617  ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15041  618 nipkow@15048  619 translations  nipkow@15048  620  "\x=a..b. t" == "setsum (%x. t) {a..b}"  nipkow@15048  621  "\x=a..i\n. t" == "setsum (\i. t) {..n}"  nipkow@15048  623  "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  631 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  633 @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \  nipkow@15542  656  setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)"  nipkow@16052  663 by (simp add:atMost_Suc add_ac)  nipkow@16052  664 nipkow@16041  665 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n"  nipkow@16041  666 by (simp add:lessThan_Suc add_ac)  nipkow@15041  667 nipkow@15911  668 lemma setsum_cl_ivl_Suc[simp]:  nipkow@15561  669  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  nipkow@15561  670 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@15561  671 nipkow@15911  672 lemma setsum_op_ivl_Suc[simp]:  nipkow@15561  673  "setsum f {m..  nipkow@15561  677  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  nipkow@15561  678 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@16041  679 *)  nipkow@15539  680 lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \  nipkow@15539  681  setsum f {m.. 'a::ab_group_add"  nipkow@15539  686 shows "\ m \ n; n \ p \ \  nipkow@15539  687 ` setsum f {m..