src/HOL/SetInterval.thy
 author huffman Wed Jun 20 05:18:39 2007 +0200 (2007-06-20) changeset 23431 25ca91279a9b parent 23413 5caa2710dd5b child 23477 f4b83f03cac9 permissions -rw-r--r--
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
 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@15048  41 text{* A note of warning when using @{term"{.. nat => 'b set => 'b set" ("(3UN _<=_./ _)" 10)  kleing@14418  47  "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3UN _<_./ _)" 10)  kleing@14418  48  "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10)  kleing@14418  49  "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3INT _<_./ _)" 10)  kleing@14418  50 kleing@14418  51 syntax (input)  kleing@14418  52  "@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10)  kleing@14418  53  "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10)  kleing@14418  54  "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10)  kleing@14418  55  "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10)  kleing@14418  56 kleing@14418  57 syntax (xsymbols)  wenzelm@14846  58  "@UNION_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10)  wenzelm@14846  59  "@UNION_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10)  wenzelm@14846  60  "@INTER_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10)  wenzelm@14846  61  "@INTER_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10)  kleing@14418  62 kleing@14418  63 translations  kleing@14418  64  "UN i<=n. A" == "UN i:{..n}. A"  nipkow@15045  65  "UN i atLeast y) = (y \ (x::'a::order))"  paulson@15418  115 by (blast intro: order_trans)  paulson@13850  116 paulson@13850  117 lemma atLeast_eq_iff [iff]:  paulson@15418  118  "(atLeast x = atLeast y) = (x = (y::'a::linorder))"  paulson@13850  119 by (blast intro: order_antisym order_trans)  paulson@13850  120 paulson@13850  121 lemma greaterThan_subset_iff [iff]:  paulson@15418  122  "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))"  paulson@15418  123 apply (auto simp add: greaterThan_def)  paulson@15418  124  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  125 done  paulson@13850  126 paulson@13850  127 lemma greaterThan_eq_iff [iff]:  paulson@15418  128  "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"  paulson@15418  129 apply (rule iffI)  paulson@15418  130  apply (erule equalityE)  paulson@15418  131  apply (simp_all add: greaterThan_subset_iff)  paulson@13850  132 done  paulson@13850  133 paulson@15418  134 lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))"  paulson@13850  135 by (blast intro: order_trans)  paulson@13850  136 paulson@15418  137 lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"  paulson@13850  138 by (blast intro: order_antisym order_trans)  paulson@13850  139 paulson@13850  140 lemma lessThan_subset_iff [iff]:  paulson@15418  141  "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))"  paulson@15418  142 apply (auto simp add: lessThan_def)  paulson@15418  143  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  144 done  paulson@13850  145 paulson@13850  146 lemma lessThan_eq_iff [iff]:  paulson@15418  147  "(lessThan x = lessThan y) = (x = (y::'a::linorder))"  paulson@15418  148 apply (rule iffI)  paulson@15418  149  apply (erule equalityE)  paulson@15418  150  apply (simp_all add: lessThan_subset_iff)  ballarin@13735  151 done  ballarin@13735  152 ballarin@13735  153 paulson@13850  154 subsection {*Two-sided intervals*}  ballarin@13735  155 ballarin@13735  156 lemma greaterThanLessThan_iff [simp]:  nipkow@15045  157  "(i : {l<.. {m::'a::order..n} = {}";  nipkow@15554  179  by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);  nipkow@15554  180 nipkow@15554  181 lemma atLeastLessThan_empty[simp]: "n \ m ==> {m.. k ==> {k<..(l::'a::order)} = {}"  nipkow@17719  185 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)  nipkow@17719  186 nipkow@17719  187 lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<..(l::'a::order)} = {}"  nipkow@17719  188 by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)  nipkow@17719  189 nipkow@15554  190 lemma atLeastAtMost_singleton [simp]: "{a::'a::order..a} = {a}";  nipkow@17719  191 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);  paulson@14485  192 paulson@14485  193 subsection {* Intervals of natural numbers *}  paulson@14485  194 paulson@15047  195 subsubsection {* The Constant @{term lessThan} *}  paulson@15047  196 paulson@14485  197 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"  paulson@14485  198 by (simp add: lessThan_def)  paulson@14485  199 paulson@14485  200 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"  paulson@14485  201 by (simp add: lessThan_def less_Suc_eq, blast)  paulson@14485  202 paulson@14485  203 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"  paulson@14485  204 by (simp add: lessThan_def atMost_def less_Suc_eq_le)  paulson@14485  205 paulson@14485  206 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"  paulson@14485  207 by blast  paulson@14485  208 paulson@15047  209 subsubsection {* The Constant @{term greaterThan} *}  paulson@15047  210 paulson@14485  211 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"  paulson@14485  212 apply (simp add: greaterThan_def)  paulson@14485  213 apply (blast dest: gr0_conv_Suc [THEN iffD1])  paulson@14485  214 done  paulson@14485  215 paulson@14485  216 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"  paulson@14485  217 apply (simp add: greaterThan_def)  paulson@14485  218 apply (auto elim: linorder_neqE)  paulson@14485  219 done  paulson@14485  220 paulson@14485  221 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"  paulson@14485  222 by blast  paulson@14485  223 paulson@15047  224 subsubsection {* The Constant @{term atLeast} *}  paulson@15047  225 paulson@14485  226 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"  paulson@14485  227 by (unfold atLeast_def UNIV_def, simp)  paulson@14485  228 paulson@14485  229 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"  paulson@14485  230 apply (simp add: atLeast_def)  paulson@14485  231 apply (simp add: Suc_le_eq)  paulson@14485  232 apply (simp add: order_le_less, blast)  paulson@14485  233 done  paulson@14485  234 paulson@14485  235 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"  paulson@14485  236  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)  paulson@14485  237 paulson@14485  238 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"  paulson@14485  239 by blast  paulson@14485  240 paulson@15047  241 subsubsection {* The Constant @{term atMost} *}  paulson@15047  242 paulson@14485  243 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"  paulson@14485  244 by (simp add: atMost_def)  paulson@14485  245 paulson@14485  246 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"  paulson@14485  247 apply (simp add: atMost_def)  paulson@14485  248 apply (simp add: less_Suc_eq order_le_less, blast)  paulson@14485  249 done  paulson@14485  250 paulson@14485  251 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"  paulson@14485  252 by blast  paulson@14485  253 paulson@15047  254 subsubsection {* The Constant @{term atLeastLessThan} *}  paulson@15047  255 paulson@15047  256 text{*But not a simprule because some concepts are better left in terms  paulson@15047  257  of @{term atLeastLessThan}*}  paulson@15047  258 lemma atLeast0LessThan: "{0::nat.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  292 by (auto simp add: atLeastAtMost_def)  nipkow@15554  293 nipkow@16733  294 subsubsection {* Image *}  nipkow@16733  295 nipkow@16733  296 lemma image_add_atLeastAtMost:  nipkow@16733  297  "(%n::nat. n+k)  {i..j} = {i+k..j+k}" (is "?A = ?B")  nipkow@16733  298 proof  nipkow@16733  299  show "?A \ ?B" by auto  nipkow@16733  300 next  nipkow@16733  301  show "?B \ ?A"  nipkow@16733  302  proof  nipkow@16733  303  fix n assume a: "n : ?B"  webertj@20217  304  hence "n - k : {i..j}" by auto  nipkow@16733  305  moreover have "n = (n - k) + k" using a by auto  nipkow@16733  306  ultimately show "n : ?A" by blast  nipkow@16733  307  qed  nipkow@16733  308 qed  nipkow@16733  309 nipkow@16733  310 lemma image_add_atLeastLessThan:  nipkow@16733  311  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  314 next  nipkow@16733  315  show "?B \ ?A"  nipkow@16733  316  proof  nipkow@16733  317  fix n assume a: "n : ?B"  webertj@20217  318  hence "n - k : {i.. finite N"  paulson@14485  366  -- {* A bounded set of natural numbers is finite. *}  paulson@14485  367  apply (rule finite_subset)  paulson@14485  368  apply (rule_tac [2] finite_lessThan, auto)  paulson@14485  369  done  paulson@14485  370 paulson@14485  371 subsubsection {* Cardinality *}  paulson@14485  372 nipkow@15045  373 lemma card_lessThan [simp]: "card {.. u ==>  nipkow@15045  415  {(0::int).. u")  paulson@14485  424  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  425  apply (rule finite_imageI)  paulson@14485  426  apply auto  paulson@14485  427  done  paulson@14485  428 nipkow@15045  429 lemma finite_atLeastLessThan_int [iff]: "finite {l.. u")  paulson@14485  450  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  451  apply (subst card_image)  paulson@14485  452  apply (auto simp add: inj_on_def)  paulson@14485  453  done  paulson@14485  454 nipkow@15045  455 lemma card_atLeastLessThan_int [simp]: "card {l.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  491  "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  500  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  502  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  504  "(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  516  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  518 by auto  ballarin@13735  519 ballarin@13735  520 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two  ballarin@13735  521 wenzelm@14577  522 subsubsection {* Disjoint Intersections *}  ballarin@13735  523 wenzelm@14577  524 text {* Singletons and open intervals *}  ballarin@13735  525 ballarin@13735  526 lemma ivl_disj_int_singleton:  nipkow@15045  527  "{l::'a::order} Int {l<..} = {}"  nipkow@15045  528  "{.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  574 apply(auto simp:linorder_not_le)  nipkow@15542  575 apply(rule ccontr)  nipkow@15542  576 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  577 apply(clarsimp simp:linorder_not_le)  nipkow@15542  578 apply(fastsimp)  nipkow@15542  579 done  nipkow@15542  580 nipkow@15041  581 nipkow@15042  582 subsection {* Summation indexed over intervals *}  nipkow@15042  583 nipkow@15042  584 syntax  nipkow@15042  585  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  586  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  587  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@16052  588  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  nipkow@15042  589 syntax (xsymbols)  nipkow@15042  590  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  591  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  592  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  593  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15042  594 syntax (HTML output)  nipkow@15042  595  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  596  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  597  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  598  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15056  599 syntax (latex_sum output)  nipkow@15052  600  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  601  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@15052  602  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  603  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@16052  604  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  605  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15052  606  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  607  ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15041  608 nipkow@15048  609 translations  nipkow@15048  610  "\x=a..b. t" == "setsum (%x. t) {a..b}"  nipkow@15048  611  "\x=a..i\n. t" == "setsum (\i. t) {..n}"  nipkow@15048  613  "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  621 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  623 @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \  nipkow@15542  646  setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)"  nipkow@16052  653 by (simp add:atMost_Suc add_ac)  nipkow@16052  654 nipkow@16041  655 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n"  nipkow@16041  656 by (simp add:lessThan_Suc add_ac)  nipkow@15041  657 nipkow@15911  658 lemma setsum_cl_ivl_Suc[simp]:  nipkow@15561  659  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  nipkow@15561  660 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@15561  661 nipkow@15911  662 lemma setsum_op_ivl_Suc[simp]:  nipkow@15561  663  "setsum f {m..  nipkow@15561  667  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  nipkow@15561  668 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@16041  669 *)  nipkow@15539  670 lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \  nipkow@15539  671  setsum f {m.. 'a::ab_group_add"  nipkow@15539  676 shows "\ m \ n; n \ p \ \  nipkow@15539  677  setsum f {m..x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  kleing@19106  706 proof -  kleing@19106  707  from mn  kleing@19106  708  have "{m..n} = {m} \ {m<..n}"  kleing@19106  709  by (auto intro: ivl_disj_un_singleton)  kleing@19106  710  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  kleing@19106  711  by (simp add: atLeast0LessThan)  kleing@19106  712  also have "\ = ?rhs" by simp  kleing@19106  713  finally show ?thesis .  kleing@19106  714 qed  kleing@19106  715 kleing@19106  716 lemma setsum_head_upt:  kleing@19022  717  fixes m::nat  kleing@19022  718  assumes m: "0 < m"  kleing@19106  719  shows "(\xx\{1..xx\{0.. = (\x\{0..m - 1}. P x)"  kleing@19106  726  by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost)  kleing@19106  727  also  kleing@19106  728  have "\ = P 0 + (\x\{0<..m - 1}. P x)"  kleing@19106  729  by (simp add: setsum_head)  kleing@19106  730  also  kleing@19106  731  from m  kleing@19106  732  have "{0<..m - 1} = {1.. (\i=0..i\{1..n}. of_nat i) =  kleing@19469  753  of_nat n*((of_nat n)+1)"  kleing@19469  754 proof (induct n)  kleing@19469  755  case 0  kleing@19469  756  show ?case by simp  kleing@19469  757 next  kleing@19469  758  case (Suc n)  huffman@23431  759  then show ?case by (simp add: ring_eq_simps)  kleing@19469  760 qed  kleing@19469  761 kleing@19469  762 theorem arith_series_general:  huffman@23277  763  "((1::'a::comm_semiring_1) + 1) * (\i\{.. 1"  kleing@19469  767  let ?I = "\i. of_nat i" and ?n = "of_nat n"  kleing@19469  768  have  kleing@19469  769  "(\i\{..i\{..i\{.. = ?n*a + (\i\{.. = (?n*a + d*(\i\{1.. = (1+1)*?n*a + d*(1+1)*(\i\{1..i\{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"  kleing@19469  781  by (simp only: mult_ac gauss_sum [of "n - 1"])  huffman@23431  782  (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]])  kleing@19469  783  finally show ?thesis by (simp add: mult_ac add_ac right_distrib)  kleing@19469  784 next  kleing@19469  785  assume "\(n > 1)"  kleing@19469  786  hence "n = 1 \ n = 0" by auto  kleing@19469  787  thus ?thesis by (auto simp: mult_ac right_distrib)  kleing@19469  788 qed  kleing@19469  789 kleing@19469  790 lemma arith_series_nat:  kleing@19469  791  "Suc (Suc 0) * (\i\{..i\{..i\{..i\{..nat"  kleing@19022  813  shows  kleing@19022  814  "\x. Q x \ P x \  kleing@19022  815 ` (\xxxxx