src/HOL/SetInterval.thy
 author huffman Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) changeset 47255 30a1692557b0 parent 47222 1b7c909a6fad permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
 nipkow@8924  1 (* Title: HOL/SetInterval.thy  wenzelm@32960  2  Author: Tobias Nipkow  wenzelm@32960  3  Author: Clemens Ballarin  wenzelm@32960  4  Author: Jeremy Avigad  nipkow@8924  5 ballarin@13735  6 lessThan, greaterThan, atLeast, atMost and two-sided intervals  nipkow@8924  7 *)  nipkow@8924  8 wenzelm@14577  9 header {* Set intervals *}  wenzelm@14577  10 nipkow@15131  11 theory SetInterval  haftmann@33318  12 imports Int Nat_Transfer  nipkow@15131  13 begin  nipkow@8924  14 nipkow@24691  15 context ord  nipkow@24691  16 begin  haftmann@44008  17 nipkow@24691  18 definition  wenzelm@32960  19  lessThan :: "'a => 'a set" ("(1{..<_})") where  haftmann@25062  20  "{.. 'a set" ("(1{.._})") where  haftmann@25062  24  "{..u} == {x. x \ u}"  nipkow@24691  25 nipkow@24691  26 definition  wenzelm@32960  27  greaterThan :: "'a => 'a set" ("(1{_<..})") where  haftmann@25062  28  "{l<..} == {x. l 'a set" ("(1{_..})") where  haftmann@25062  32  "{l..} == {x. l\x}"  nipkow@24691  33 nipkow@24691  34 definition  haftmann@25062  35  greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where  haftmann@25062  36  "{l<.. 'a => 'a set" ("(1{_..<_})") where  haftmann@25062  40  "{l.. 'a => 'a set" ("(1{_<.._})") where  haftmann@25062  44  "{l<..u} == {l<..} Int {..u}"  nipkow@24691  45 nipkow@24691  46 definition  haftmann@25062  47  atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where  haftmann@25062  48  "{l..u} == {l..} Int {..u}"  nipkow@24691  49 nipkow@24691  50 end  nipkow@8924  51 ballarin@13735  52 nipkow@15048  53 text{* A note of warning when using @{term"{.. 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10)  huffman@36364  59  "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" [0, 0, 10] 10)  huffman@36364  60  "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" [0, 0, 10] 10)  huffman@36364  61  "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10)  kleing@14418  62 nipkow@30372  63 syntax (xsymbols)  huffman@36364  64  "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\ _\_./ _)" [0, 0, 10] 10)  huffman@36364  65  "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" [0, 0, 10] 10)  huffman@36364  66  "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\ _\_./ _)" [0, 0, 10] 10)  huffman@36364  67  "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" [0, 0, 10] 10)  kleing@14418  68 nipkow@30372  69 syntax (latex output)  huffman@36364  70  "_UNION_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" [0, 0, 10] 10)  huffman@36364  71  "_UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" [0, 0, 10] 10)  huffman@36364  72  "_INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" [0, 0, 10] 10)  huffman@36364  73  "_INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" [0, 0, 10] 10)  kleing@14418  74 kleing@14418  75 translations  kleing@14418  76  "UN i<=n. A" == "UN i:{..n}. A"  nipkow@15045  77  "UN i atLeast y) = (y \ (x::'a::order))"  paulson@15418  125 by (blast intro: order_trans)  paulson@13850  126 paulson@13850  127 lemma atLeast_eq_iff [iff]:  paulson@15418  128  "(atLeast x = atLeast y) = (x = (y::'a::linorder))"  paulson@13850  129 by (blast intro: order_antisym order_trans)  paulson@13850  130 paulson@13850  131 lemma greaterThan_subset_iff [iff]:  paulson@15418  132  "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))"  paulson@15418  133 apply (auto simp add: greaterThan_def)  paulson@15418  134  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  135 done  paulson@13850  136 paulson@13850  137 lemma greaterThan_eq_iff [iff]:  paulson@15418  138  "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"  paulson@15418  139 apply (rule iffI)  paulson@15418  140  apply (erule equalityE)  haftmann@29709  141  apply simp_all  paulson@13850  142 done  paulson@13850  143 paulson@15418  144 lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))"  paulson@13850  145 by (blast intro: order_trans)  paulson@13850  146 paulson@15418  147 lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"  paulson@13850  148 by (blast intro: order_antisym order_trans)  paulson@13850  149 paulson@13850  150 lemma lessThan_subset_iff [iff]:  paulson@15418  151  "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))"  paulson@15418  152 apply (auto simp add: lessThan_def)  paulson@15418  153  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  154 done  paulson@13850  155 paulson@13850  156 lemma lessThan_eq_iff [iff]:  paulson@15418  157  "(lessThan x = lessThan y) = (x = (y::'a::linorder))"  paulson@15418  158 apply (rule iffI)  paulson@15418  159  apply (erule equalityE)  haftmann@29709  160  apply simp_all  ballarin@13735  161 done  ballarin@13735  162 hoelzl@40703  163 lemma lessThan_strict_subset_iff:  hoelzl@40703  164  fixes m n :: "'a::linorder"  hoelzl@40703  165  shows "{.. m < n"  hoelzl@40703  166  by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)  ballarin@13735  167 paulson@13850  168 subsection {*Two-sided intervals*}  ballarin@13735  169 nipkow@24691  170 context ord  nipkow@24691  171 begin  nipkow@24691  172 blanchet@35828  173 lemma greaterThanLessThan_iff [simp,no_atp]:  haftmann@25062  174  "(i : {l<.. {a..b} = {}"  nipkow@32400  202 by(auto simp: atLeastAtMost_def atLeast_def atMost_def)  nipkow@32400  203 nipkow@32400  204 lemma atLeastatMost_empty_iff[simp]:  nipkow@32400  205  "{a..b} = {} \ (~ a <= b)"  nipkow@32400  206 by auto (blast intro: order_trans)  nipkow@32400  207 nipkow@32400  208 lemma atLeastatMost_empty_iff2[simp]:  nipkow@32400  209  "{} = {a..b} \ (~ a <= b)"  nipkow@32400  210 by auto (blast intro: order_trans)  nipkow@32400  211 nipkow@32400  212 lemma atLeastLessThan_empty[simp]:  nipkow@32400  213  "b <= a \ {a.. (~ a < b)"  nipkow@32400  218 by auto (blast intro: le_less_trans)  nipkow@32400  219 nipkow@32400  220 lemma atLeastLessThan_empty_iff2[simp]:  nipkow@32400  221  "{} = {a.. (~ a < b)"  nipkow@32400  222 by auto (blast intro: le_less_trans)  nipkow@15554  223 nipkow@32400  224 lemma greaterThanAtMost_empty[simp]: "l \ k ==> {k<..l} = {}"  nipkow@17719  225 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)  nipkow@17719  226 nipkow@32400  227 lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ ~ k < l"  nipkow@32400  228 by auto (blast intro: less_le_trans)  nipkow@32400  229 nipkow@32400  230 lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ ~ k < l"  nipkow@32400  231 by auto (blast intro: less_le_trans)  nipkow@32400  232 haftmann@29709  233 lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. {a .. b} = {a}" by simp  hoelzl@36846  240 nipkow@32400  241 lemma atLeastatMost_subset_iff[simp]:  nipkow@32400  242  "{a..b} <= {c..d} \ (~ a <= b) | c <= a & b <= d"  nipkow@32400  243 unfolding atLeastAtMost_def atLeast_def atMost_def  nipkow@32400  244 by (blast intro: order_trans)  nipkow@32400  245 nipkow@32400  246 lemma atLeastatMost_psubset_iff:  nipkow@32400  247  "{a..b} < {c..d} \  nipkow@32400  248  ((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d"  nipkow@39302  249 by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)  nipkow@32400  250 hoelzl@36846  251 lemma atLeastAtMost_singleton_iff[simp]:  hoelzl@36846  252  "{a .. b} = {c} \ a = b \ b = c"  hoelzl@36846  253 proof  hoelzl@36846  254  assume "{a..b} = {c}"  hoelzl@36846  255  hence "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp  hoelzl@36846  256  moreover with {a..b} = {c} have "c \ a \ b \ c" by auto  hoelzl@36846  257  ultimately show "a = b \ b = c" by auto  hoelzl@36846  258 qed simp  hoelzl@36846  259 nipkow@24691  260 end  paulson@14485  261 hoelzl@42891  262 context dense_linorder  hoelzl@42891  263 begin  hoelzl@42891  264 hoelzl@42891  265 lemma greaterThanLessThan_empty_iff[simp]:  hoelzl@42891  266  "{ a <..< b } = {} \ b \ a"  hoelzl@42891  267  using dense[of a b] by (cases "a < b") auto  hoelzl@42891  268 hoelzl@42891  269 lemma greaterThanLessThan_empty_iff2[simp]:  hoelzl@42891  270  "{} = { a <..< b } \ b \ a"  hoelzl@42891  271  using dense[of a b] by (cases "a < b") auto  hoelzl@42891  272 hoelzl@42901  273 lemma atLeastLessThan_subseteq_atLeastAtMost_iff:  hoelzl@42901  274  "{a ..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  275  using dense[of "max a d" "b"]  hoelzl@42901  276  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  277 hoelzl@42901  278 lemma greaterThanAtMost_subseteq_atLeastAtMost_iff:  hoelzl@42901  279  "{a <.. b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  280  using dense[of "a" "min c b"]  hoelzl@42901  281  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  282 hoelzl@42901  283 lemma greaterThanLessThan_subseteq_atLeastAtMost_iff:  hoelzl@42901  284  "{a <..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)"  hoelzl@42901  285  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@42901  286  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@42901  287 hoelzl@43657  288 lemma atLeastAtMost_subseteq_atLeastLessThan_iff:  hoelzl@43657  289  "{a .. b} \ { c ..< d } \ (a \ b \ c \ a \ b < d)"  hoelzl@43657  290  using dense[of "max a d" "b"]  hoelzl@43657  291  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  292 hoelzl@43657  293 lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:  hoelzl@43657  294  "{a <.. b} \ { c ..< d } \ (a < b \ c \ a \ b < d)"  hoelzl@43657  295  using dense[of "a" "min c b"]  hoelzl@43657  296  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  297 hoelzl@43657  298 lemma greaterThanLessThan_subseteq_atLeastLessThan_iff:  hoelzl@43657  299  "{a <..< b} \ { c ..< d } \ (a < b \ c \ a \ b \ d)"  hoelzl@43657  300  using dense[of "a" "min c b"] dense[of "max a d" "b"]  hoelzl@43657  301  by (force simp: subset_eq Ball_def not_less[symmetric])  hoelzl@43657  302 hoelzl@42891  303 end  hoelzl@42891  304 nipkow@32408  305 lemma (in linorder) atLeastLessThan_subset_iff:  nipkow@32408  306  "{a.. b <= a | c<=a & b<=d"  nipkow@32408  307 apply (auto simp:subset_eq Ball_def)  nipkow@32408  308 apply(frule_tac x=a in spec)  nipkow@32408  309 apply(erule_tac x=d in allE)  nipkow@32408  310 apply (simp add: less_imp_le)  nipkow@32408  311 done  nipkow@32408  312 hoelzl@40703  313 lemma atLeastLessThan_inj:  hoelzl@40703  314  fixes a b c d :: "'a::linorder"  hoelzl@40703  315  assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"  hoelzl@40703  316  shows "a = c" "b = d"  hoelzl@40703  317 using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+  hoelzl@40703  318 hoelzl@40703  319 lemma atLeastLessThan_eq_iff:  hoelzl@40703  320  fixes a b c d :: "'a::linorder"  hoelzl@40703  321  assumes "a < b" "c < d"  hoelzl@40703  322  shows "{a ..< b} = {c ..< d} \ a = c \ b = d"  hoelzl@40703  323  using atLeastLessThan_inj assms by auto  hoelzl@40703  324 nipkow@32456  325 subsubsection {* Intersection *}  nipkow@32456  326 nipkow@32456  327 context linorder  nipkow@32456  328 begin  nipkow@32456  329 nipkow@32456  330 lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"  nipkow@32456  331 by auto  nipkow@32456  332 nipkow@32456  333 lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"  nipkow@32456  334 by auto  nipkow@32456  335 nipkow@32456  336 lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"  nipkow@32456  337 by auto  nipkow@32456  338 nipkow@32456  339 lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"  nipkow@32456  340 by auto  nipkow@32456  341 nipkow@32456  342 lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"  nipkow@32456  343 by auto  nipkow@32456  344 nipkow@32456  345 lemma Int_atLeastLessThan[simp]: "{a.. Suc  {.. Suc (x - 1)" by auto  hoelzl@39072  375  with x < Suc n show "x = 0" by auto  hoelzl@39072  376 qed  hoelzl@39072  377 paulson@14485  378 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"  paulson@14485  379 by (simp add: lessThan_def atMost_def less_Suc_eq_le)  paulson@14485  380 paulson@14485  381 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"  paulson@14485  382 by blast  paulson@14485  383 paulson@15047  384 subsubsection {* The Constant @{term greaterThan} *}  paulson@15047  385 paulson@14485  386 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"  paulson@14485  387 apply (simp add: greaterThan_def)  paulson@14485  388 apply (blast dest: gr0_conv_Suc [THEN iffD1])  paulson@14485  389 done  paulson@14485  390 paulson@14485  391 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"  paulson@14485  392 apply (simp add: greaterThan_def)  paulson@14485  393 apply (auto elim: linorder_neqE)  paulson@14485  394 done  paulson@14485  395 paulson@14485  396 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"  paulson@14485  397 by blast  paulson@14485  398 paulson@15047  399 subsubsection {* The Constant @{term atLeast} *}  paulson@15047  400 paulson@14485  401 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"  paulson@14485  402 by (unfold atLeast_def UNIV_def, simp)  paulson@14485  403 paulson@14485  404 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"  paulson@14485  405 apply (simp add: atLeast_def)  paulson@14485  406 apply (simp add: Suc_le_eq)  paulson@14485  407 apply (simp add: order_le_less, blast)  paulson@14485  408 done  paulson@14485  409 paulson@14485  410 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"  paulson@14485  411  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)  paulson@14485  412 paulson@14485  413 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"  paulson@14485  414 by blast  paulson@14485  415 paulson@15047  416 subsubsection {* The Constant @{term atMost} *}  paulson@15047  417 paulson@14485  418 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"  paulson@14485  419 by (simp add: atMost_def)  paulson@14485  420 paulson@14485  421 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"  paulson@14485  422 apply (simp add: atMost_def)  paulson@14485  423 apply (simp add: less_Suc_eq order_le_less, blast)  paulson@14485  424 done  paulson@14485  425 paulson@14485  426 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"  paulson@14485  427 by blast  paulson@14485  428 paulson@15047  429 subsubsection {* The Constant @{term atLeastLessThan} *}  paulson@15047  430 nipkow@28068  431 text{*The orientation of the following 2 rules is tricky. The lhs is  nipkow@24449  432 defined in terms of the rhs. Hence the chosen orientation makes sense  nipkow@24449  433 in this theory --- the reverse orientation complicates proofs (eg  nipkow@24449  434 nontermination). But outside, when the definition of the lhs is rarely  nipkow@24449  435 used, the opposite orientation seems preferable because it reduces a  nipkow@24449  436 specific concept to a more general one. *}  nipkow@28068  437 paulson@15047  438 lemma atLeast0LessThan: "{0::nat.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  478 by (auto simp add: atLeastAtMost_def)  nipkow@15554  479 noschinl@45932  480 lemma atLeastAtMost_insertL: "m \ n \ insert m {Suc m..n} = {m ..n}"  noschinl@45932  481 by auto  noschinl@45932  482 kleing@43157  483 text {* The analogous result is useful on @{typ int}: *}  kleing@43157  484 (* here, because we don't have an own int section *)  kleing@43157  485 lemma atLeastAtMostPlus1_int_conv:  kleing@43157  486  "m <= 1+n \ {m..1+n} = insert (1+n) {m..n::int}"  kleing@43157  487  by (auto intro: set_eqI)  kleing@43157  488 paulson@33044  489 lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j.. ?B" by auto  nipkow@16733  500 next  nipkow@16733  501  show "?B \ ?A"  nipkow@16733  502  proof  nipkow@16733  503  fix n assume a: "n : ?B"  webertj@20217  504  hence "n - k : {i..j}" by auto  nipkow@16733  505  moreover have "n = (n - k) + k" using a by auto  nipkow@16733  506  ultimately show "n : ?A" by blast  nipkow@16733  507  qed  nipkow@16733  508 qed  nipkow@16733  509 nipkow@16733  510 lemma image_add_atLeastLessThan:  nipkow@16733  511  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  514 next  nipkow@16733  515  show "?B \ ?A"  nipkow@16733  516  proof  nipkow@16733  517  fix n assume a: "n : ?B"  webertj@20217  518  hence "n - k : {i..i. i - c)  {x ..< y} =  hoelzl@37664  542  (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"  hoelzl@37664  543  (is "_ = ?right")  hoelzl@37664  544 proof safe  hoelzl@37664  545  fix a assume a: "a \ ?right"  hoelzl@37664  546  show "a \ (\i. i - c)  {x ..< y}"  hoelzl@37664  547  proof cases  hoelzl@37664  548  assume "c < y" with a show ?thesis  hoelzl@37664  549  by (auto intro!: image_eqI[of _ _ "a + c"])  hoelzl@37664  550  next  hoelzl@37664  551  assume "\ c < y" with a show ?thesis  hoelzl@37664  552  by (auto intro!: image_eqI[of _ _ x] split: split_if_asm)  hoelzl@37664  553  qed  hoelzl@37664  554 qed auto  hoelzl@37664  555 hoelzl@35580  556 context ordered_ab_group_add  hoelzl@35580  557 begin  hoelzl@35580  558 hoelzl@35580  559 lemma  hoelzl@35580  560  fixes x :: 'a  hoelzl@35580  561  shows image_uminus_greaterThan[simp]: "uminus  {x<..} = {..<-x}"  hoelzl@35580  562  and image_uminus_atLeast[simp]: "uminus  {x..} = {..-x}"  hoelzl@35580  563 proof safe  hoelzl@35580  564  fix y assume "y < -x"  hoelzl@35580  565  hence *: "x < -y" using neg_less_iff_less[of "-y" x] by simp  hoelzl@35580  566  have "- (-y) \ uminus  {x<..}"  hoelzl@35580  567  by (rule imageI) (simp add: *)  hoelzl@35580  568  thus "y \ uminus  {x<..}" by simp  hoelzl@35580  569 next  hoelzl@35580  570  fix y assume "y \ -x"  hoelzl@35580  571  have "- (-y) \ uminus  {x..}"  hoelzl@35580  572  by (rule imageI) (insert y \ -x[THEN le_imp_neg_le], simp)  hoelzl@35580  573  thus "y \ uminus  {x..}" by simp  hoelzl@35580  574 qed simp_all  hoelzl@35580  575 hoelzl@35580  576 lemma  hoelzl@35580  577  fixes x :: 'a  hoelzl@35580  578  shows image_uminus_lessThan[simp]: "uminus  {.. finite N"  nipkow@28068  625 apply (rule finite_subset)  nipkow@28068  626  apply (rule_tac [2] finite_lessThan, auto)  nipkow@28068  627 done  nipkow@28068  628 nipkow@31044  629 text {* A set of natural numbers is finite iff it is bounded. *}  nipkow@31044  630 lemma finite_nat_set_iff_bounded:  nipkow@31044  631  "finite(N::nat set) = (EX m. ALL n:N. nnat. (!!n. n \ f n) ==> finite {n. f n \ u}"  nipkow@28068  647 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)  paulson@14485  648 nipkow@24853  649 text{* Any subset of an interval of natural numbers the size of the  nipkow@24853  650 subset is exactly that interval. *}  nipkow@24853  651 nipkow@24853  652 lemma subset_card_intvl_is_intvl:  nipkow@24853  653  "A <= {k.. A = {k..i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B")  nipkow@36755  675 proof  nipkow@36755  676  show "?A <= ?B"  nipkow@36755  677  proof  nipkow@36755  678  fix x assume "x : ?A"  nipkow@36755  679  then obtain i where i: "i\n" "x : M i" by auto  nipkow@36755  680  show "x : ?B"  nipkow@36755  681  proof(cases i)  nipkow@36755  682  case 0 with i show ?thesis by simp  nipkow@36755  683  next  nipkow@36755  684  case (Suc j) with i show ?thesis by auto  nipkow@36755  685  qed  nipkow@36755  686  qed  nipkow@36755  687 next  nipkow@36755  688  show "?B <= ?A" by auto  nipkow@36755  689 qed  nipkow@36755  690 nipkow@36755  691 lemma UN_le_add_shift:  nipkow@36755  692  "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B")  nipkow@36755  693 proof  nipkow@44890  694  show "?A <= ?B" by fastforce  nipkow@36755  695 next  nipkow@36755  696  show "?B <= ?A"  nipkow@36755  697  proof  nipkow@36755  698  fix x assume "x : ?B"  nipkow@36755  699  then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto  nipkow@36755  700  hence "i-k\n & x : M((i-k)+k)" by auto  nipkow@36755  701  thus "x : ?A" by blast  nipkow@36755  702  qed  nipkow@36755  703 qed  nipkow@36755  704 paulson@32596  705 lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)"  paulson@32596  706  by (auto simp add: atLeast0LessThan)  paulson@32596  707 paulson@32596  708 lemma UN_finite_subset: "(!!n::nat. (\i\{0.. C) \ (\n. A n) \ C"  paulson@32596  709  by (subst UN_UN_finite_eq [symmetric]) blast  paulson@32596  710 paulson@33044  711 lemma UN_finite2_subset:  paulson@33044  712  "(!!n::nat. (\i\{0.. (\i\{0.. (\n. A n) \ (\n. B n)"  paulson@33044  713  apply (rule UN_finite_subset)  paulson@33044  714  apply (subst UN_UN_finite_eq [symmetric, of B])  paulson@33044  715  apply blast  paulson@33044  716  done  paulson@32596  717 paulson@32596  718 lemma UN_finite2_eq:  paulson@33044  719  "(!!n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)"  paulson@33044  720  apply (rule subset_antisym)  paulson@33044  721  apply (rule UN_finite2_subset, blast)  paulson@33044  722  apply (rule UN_finite2_subset [where k=k])  huffman@35216  723  apply (force simp add: atLeastLessThan_add_Un [of 0])  paulson@33044  724  done  paulson@32596  725 paulson@32596  726 paulson@14485  727 subsubsection {* Cardinality *}  paulson@14485  728 nipkow@15045  729 lemma card_lessThan [simp]: "card {.. \h. bij_betw h {0.. \h. bij_betw h M {0.. finite B \ card A = card B \ EX h. bij_betw h A B"  nipkow@31438  768 apply(drule ex_bij_betw_finite_nat)  nipkow@31438  769 apply(drule ex_bij_betw_nat_finite)  nipkow@31438  770 apply(auto intro!:bij_betw_trans)  nipkow@31438  771 done  nipkow@31438  772 nipkow@31438  773 lemma ex_bij_betw_nat_finite_1:  nipkow@31438  774  "finite M \ \h. bij_betw h {1 .. card M} M"  nipkow@31438  775 by (rule finite_same_card_bij) auto  nipkow@31438  776 hoelzl@40703  777 lemma bij_betw_iff_card:  hoelzl@40703  778  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  779  shows BIJ: "(\f. bij_betw f A B) \ (card A = card B)"  hoelzl@40703  780 using assms  hoelzl@40703  781 proof(auto simp add: bij_betw_same_card)  hoelzl@40703  782  assume *: "card A = card B"  hoelzl@40703  783  obtain f where "bij_betw f A {0 ..< card A}"  hoelzl@40703  784  using FIN ex_bij_betw_finite_nat by blast  hoelzl@40703  785  moreover obtain g where "bij_betw g {0 ..< card B} B"  hoelzl@40703  786  using FIN' ex_bij_betw_nat_finite by blast  hoelzl@40703  787  ultimately have "bij_betw (g o f) A B"  hoelzl@40703  788  using * by (auto simp add: bij_betw_trans)  hoelzl@40703  789  thus "(\f. bij_betw f A B)" by blast  hoelzl@40703  790 qed  hoelzl@40703  791 hoelzl@40703  792 lemma inj_on_iff_card_le:  hoelzl@40703  793  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  794  shows "(\f. inj_on f A \ f  A \ B) = (card A \ card B)"  hoelzl@40703  795 proof (safe intro!: card_inj_on_le)  hoelzl@40703  796  assume *: "card A \ card B"  hoelzl@40703  797  obtain f where 1: "inj_on f A" and 2: "f  A = {0 ..< card A}"  hoelzl@40703  798  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force  hoelzl@40703  799  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g  {0 ..< card B} = B"  hoelzl@40703  800  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force  hoelzl@40703  801  ultimately have "inj_on g (f  A)" using subset_inj_on[of g _ "f  A"] * by force  hoelzl@40703  802  hence "inj_on (g o f) A" using 1 comp_inj_on by blast  hoelzl@40703  803  moreover  hoelzl@40703  804  {have "{0 ..< card A} \ {0 ..< card B}" using * by force  hoelzl@40703  805  with 2 have "f  A \ {0 ..< card B}" by blast  hoelzl@40703  806  hence "(g o f)  A \ B" unfolding comp_def using 3 by force  hoelzl@40703  807  }  hoelzl@40703  808  ultimately show "(\f. inj_on f A \ f  A \ B)" by blast  hoelzl@40703  809 qed (insert assms, auto)  nipkow@26105  810 paulson@14485  811 subsection {* Intervals of integers *}  paulson@14485  812 nipkow@15045  813 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l.. u ==>  nipkow@15045  826  {(0::int).. u")  paulson@14485  835  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  836  apply (rule finite_imageI)  paulson@14485  837  apply auto  paulson@14485  838  done  paulson@14485  839 nipkow@15045  840 lemma finite_atLeastLessThan_int [iff]: "finite {l.. u")  paulson@14485  862  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  863  apply (subst card_image)  paulson@14485  864  apply (auto simp add: inj_on_def)  paulson@14485  865  done  paulson@14485  866 nipkow@15045  867 lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}"  bulwahn@27656  889 proof -  bulwahn@27656  890  have "{k. P k \ k < i} \ {.. M"  bulwahn@27656  896 shows "card {k \ M. k < Suc i} \ 0"  bulwahn@27656  897 proof -  bulwahn@27656  898  from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto  bulwahn@27656  899  with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)  bulwahn@27656  900 qed  bulwahn@27656  901 bulwahn@27656  902 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"  haftmann@37388  903 apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"])  bulwahn@27656  904 apply simp  nipkow@44890  905 apply fastforce  bulwahn@27656  906 apply auto  bulwahn@27656  907 apply (rule inj_on_diff_nat)  bulwahn@27656  908 apply auto  bulwahn@27656  909 apply (case_tac x)  bulwahn@27656  910 apply auto  bulwahn@27656  911 apply (case_tac xa)  bulwahn@27656  912 apply auto  bulwahn@27656  913 apply (case_tac xa)  bulwahn@27656  914 apply auto  bulwahn@27656  915 done  bulwahn@27656  916 bulwahn@27656  917 lemma card_less_Suc:  bulwahn@27656  918  assumes zero_in_M: "0 \ M"  bulwahn@27656  919  shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"  bulwahn@27656  920 proof -  bulwahn@27656  921  from assms have a: "0 \ {k \ M. k < Suc i}" by simp  bulwahn@27656  922  hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})"  bulwahn@27656  923  by (auto simp only: insert_Diff)  bulwahn@27656  924  have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto  bulwahn@27656  925  from finite_M_bounded_by_nat[of "\x. x \ M" "Suc i"] have "Suc (card {k. Suc k \ M \ k < i}) = card (insert 0 ({k \ M. k < Suc i} - {0}))"  bulwahn@27656  926  apply (subst card_insert)  bulwahn@27656  927  apply simp_all  bulwahn@27656  928  apply (subst b)  bulwahn@27656  929  apply (subst card_less_Suc2[symmetric])  bulwahn@27656  930  apply simp_all  bulwahn@27656  931  done  bulwahn@27656  932  with c show ?thesis by simp  bulwahn@27656  933 qed  bulwahn@27656  934 paulson@14485  935 paulson@13850  936 subsection {*Lemmas useful with the summation operator setsum*}  paulson@13850  937 ballarin@16102  938 text {* For examples, see Algebra/poly/UnivPoly2.thy *}  ballarin@13735  939 wenzelm@14577  940 subsubsection {* Disjoint Unions *}  ballarin@13735  941 wenzelm@14577  942 text {* Singletons and open intervals *}  ballarin@13735  943 ballarin@13735  944 lemma ivl_disj_un_singleton:  nipkow@15045  945  "{l::'a::linorder} Un {l<..} = {l..}"  nipkow@15045  946  "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  950  "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  959  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  961  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  963  "(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  975  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  977 by auto  ballarin@13735  978 ballarin@13735  979 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two  ballarin@13735  980 wenzelm@14577  981 subsubsection {* Disjoint Intersections *}  ballarin@13735  982 wenzelm@14577  983 text {* One- and two-sided intervals *}  ballarin@13735  984 ballarin@13735  985 lemma ivl_disj_int_one:  nipkow@15045  986  "{..l::'a::order} Int {l<.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  1022 apply(auto simp:linorder_not_le)  nipkow@15542  1023 apply(rule ccontr)  nipkow@15542  1024 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  1025 apply(clarsimp simp:linorder_not_le)  nipkow@44890  1026 apply(fastforce)  nipkow@15542  1027 done  nipkow@15542  1028 nipkow@15041  1029 nipkow@15042  1030 subsection {* Summation indexed over intervals *}  nipkow@15042  1031 nipkow@15042  1032 syntax  nipkow@15042  1033  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  1034  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  1035  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@16052  1036  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  nipkow@15042  1037 syntax (xsymbols)  nipkow@15042  1038  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  1039  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  1040  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  1041  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15042  1042 syntax (HTML output)  nipkow@15042  1043  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  1044  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  1045  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  1046  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15056  1047 syntax (latex_sum output)  nipkow@15052  1048  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  1049  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@15052  1050  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  1051  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@16052  1052  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1053  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15052  1054  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1055  ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15041  1056 nipkow@15048  1057 translations  nipkow@28853  1058  "\x=a..b. t" == "CONST setsum (%x. t) {a..b}"  nipkow@28853  1059  "\x=a..i\n. t" == "CONST setsum (\i. t) {..n}"  nipkow@28853  1061  "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  1069 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  1071 @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \  nipkow@15542  1094  setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)"  nipkow@16052  1101 by (simp add:atMost_Suc add_ac)  nipkow@16052  1102 nipkow@16041  1103 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n"  nipkow@16041  1104 by (simp add:lessThan_Suc add_ac)  nipkow@15041  1105 nipkow@15911  1106 lemma setsum_cl_ivl_Suc[simp]:  nipkow@15561  1107  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  nipkow@15561  1108 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@15561  1109 nipkow@15911  1110 lemma setsum_op_ivl_Suc[simp]:  nipkow@15561  1111  "setsum f {m..  nipkow@15561  1115  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  nipkow@15561  1116 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@16041  1117 *)  nipkow@28068  1118 nipkow@28068  1119 lemma setsum_head:  nipkow@28068  1120  fixes n :: nat  nipkow@28068  1121  assumes mn: "m <= n"  nipkow@28068  1122  shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  nipkow@28068  1123 proof -  nipkow@28068  1124  from mn  nipkow@28068  1125  have "{m..n} = {m} \ {m<..n}"  nipkow@28068  1126  by (auto intro: ivl_disj_un_singleton)  nipkow@28068  1127  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  nipkow@28068  1128  by (simp add: atLeast0LessThan)  nipkow@28068  1129  also have "\ = ?rhs" by simp  nipkow@28068  1130  finally show ?thesis .  nipkow@28068  1131 qed  nipkow@28068  1132 nipkow@28068  1133 lemma setsum_head_Suc:  nipkow@28068  1134  "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}"  nipkow@28068  1135 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)  nipkow@28068  1136 nipkow@28068  1137 lemma setsum_head_upt_Suc:  nipkow@28068  1138  "m < n \ setsum f {m.. n + 1"  nipkow@31501  1144  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"  nipkow@31501  1145 proof-  nipkow@31501  1146  have "{m .. n+p} = {m..n} \ {n+1..n+p}" using m \ n+1 by auto  nipkow@31501  1147  thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint  nipkow@31501  1148  atLeastSucAtMost_greaterThanAtMost)  nipkow@31501  1149 qed  nipkow@28068  1150 nipkow@15539  1151 lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \  nipkow@15539  1152  setsum f {m.. 'a::ab_group_add"  nipkow@15539  1157 shows "\ m \ n; n \ p \ \  nipkow@15539  1158  setsum f {m.. ('a::ab_group_add)"  nipkow@31505  1165  shows "setsum (\k. f k - f(k + 1)) {(m::nat) .. n} =  nipkow@31505  1166  (if m <= n then f m - f(n + 1) else 0)"  nipkow@31505  1167 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)  nipkow@31505  1168 haftmann@44008  1169 lemma setsum_restrict_set':  haftmann@44008  1170  "finite A \ setsum f {x \ A. x \ B} = (\x\A. if x \ B then f x else 0)"  haftmann@44008  1171  by (simp add: setsum_restrict_set [symmetric] Int_def)  haftmann@44008  1172 haftmann@44008  1173 lemma setsum_restrict_set'':  haftmann@44008  1174  "finite A \ setsum f {x \ A. P x} = (\x\A. if P x then f x else 0)"  haftmann@44008  1175  by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq])  nipkow@31509  1176 nipkow@31509  1177 lemma setsum_setsum_restrict:  haftmann@44008  1178  "finite S \ finite T \  haftmann@44008  1179  setsum (\x. setsum (\y. f x y) {y. y \ T \ R x y}) S = setsum (\y. setsum (\x. f x y) {x. x \ S \ R x y}) T"  haftmann@44008  1180  by (simp add: setsum_restrict_set'') (rule setsum_commute)  nipkow@31509  1181 nipkow@31509  1182 lemma setsum_image_gen: assumes fS: "finite S"  nipkow@31509  1183  shows "setsum g S = setsum (\y. setsum g {x. x \ S \ f x = y}) (f  S)"  nipkow@31509  1184 proof-  nipkow@31509  1185  { fix x assume "x \ S" then have "{y. y\ fS \ f x = y} = {f x}" by auto }  nipkow@31509  1186  hence "setsum g S = setsum (\x. setsum (\y. g x) {y. y\ fS \ f x = y}) S"  nipkow@31509  1187  by simp  nipkow@31509  1188  also have "\ = setsum (\y. setsum g {x. x \ S \ f x = y}) (f  S)"  nipkow@31509  1189  by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]])  nipkow@31509  1190  finally show ?thesis .  nipkow@31509  1191 qed  nipkow@31509  1192 hoelzl@35171  1193 lemma setsum_le_included:  haftmann@36307  1194  fixes f :: "'a \ 'b::ordered_comm_monoid_add"  hoelzl@35171  1195  assumes "finite s" "finite t"  hoelzl@35171  1196  and "\y\t. 0 \ g y" "(\x\s. \y\t. i y = x \ f x \ g y)"  hoelzl@35171  1197  shows "setsum f s \ setsum g t"  hoelzl@35171  1198 proof -  hoelzl@35171  1199  have "setsum f s \ setsum (\y. setsum g {x. x\t \ i x = y}) s"  hoelzl@35171  1200  proof (rule setsum_mono)  hoelzl@35171  1201  fix y assume "y \ s"  hoelzl@35171  1202  with assms obtain z where z: "z \ t" "y = i z" "f y \ g z" by auto  hoelzl@35171  1203  with assms show "f y \ setsum g {x \ t. i x = y}" (is "?A y \ ?B y")  hoelzl@35171  1204  using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]  hoelzl@35171  1205  by (auto intro!: setsum_mono2)  hoelzl@35171  1206  qed  hoelzl@35171  1207  also have "... \ setsum (\y. setsum g {x. x\t \ i x = y}) (i  t)"  hoelzl@35171  1208  using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)  hoelzl@35171  1209  also have "... \ setsum g t"  hoelzl@35171  1210  using assms by (auto simp: setsum_image_gen[symmetric])  hoelzl@35171  1211  finally show ?thesis .  hoelzl@35171  1212 qed  hoelzl@35171  1213 nipkow@31509  1214 lemma setsum_multicount_gen:  nipkow@31509  1215  assumes "finite s" "finite t" "\j\t. (card {i\s. R i j} = k j)"  nipkow@31509  1216  shows "setsum (\i. (card {j\t. R i j})) s = setsum k t" (is "?l = ?r")  nipkow@31509  1217 proof-  nipkow@31509  1218  have "?l = setsum (\i. setsum (\x.1) {j\t. R i j}) s" by auto  nipkow@31509  1219  also have "\ = ?r" unfolding setsum_setsum_restrict[OF assms(1-2)]  nipkow@31509  1220  using assms(3) by auto  nipkow@31509  1221  finally show ?thesis .  nipkow@31509  1222 qed  nipkow@31509  1223 nipkow@31509  1224 lemma setsum_multicount:  nipkow@31509  1225  assumes "finite S" "finite T" "\j\T. (card {i\S. R i j} = k)"  nipkow@31509  1226  shows "setsum (\i. card {j\T. R i j}) S = k * card T" (is "?l = ?r")  nipkow@31509  1227 proof-  nipkow@31509  1228  have "?l = setsum (\i. k) T" by(rule setsum_multicount_gen)(auto simp:assms)  huffman@35216  1229  also have "\ = ?r" by(simp add: mult_commute)  nipkow@31509  1230  finally show ?thesis by auto  nipkow@31509  1231 qed  nipkow@31509  1232 nipkow@28068  1233 nipkow@16733  1234 subsection{* Shifting bounds *}  nipkow@16733  1235 nipkow@15539  1236 lemma setsum_shift_bounds_nat_ivl:  nipkow@15539  1237  "setsum f {m+k.. setsum f {Suc 0..k} = setsum f {0..k}"  nipkow@28068  1256 by(simp add:setsum_head_Suc)  kleing@19106  1257 nipkow@28068  1258 lemma setsum_shift_lb_Suc0_0_upt:  nipkow@28068  1259  "f(0::nat) = 0 \ setsum f {Suc 0.. 1"  haftmann@36307  1268  shows "(\i=0.. 0" by simp_all  haftmann@36307  1271  moreover have "(\i=0.. 0 have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp  haftmann@36350  1277  ultimately show ?case by (simp add: field_simps divide_inverse)  haftmann@36307  1278  qed  haftmann@36307  1279  ultimately show ?thesis by simp  haftmann@36307  1280 qed  haftmann@36307  1281 ballarin@17149  1282 kleing@19469  1283 subsection {* The formula for arithmetic sums *}  kleing@19469  1284 huffman@47222  1285 lemma gauss_sum:  huffman@47222  1286  "(2::'a::comm_semiring_1)*(\i\{1..n}. of_nat i) =  kleing@19469  1287  of_nat n*((of_nat n)+1)"  kleing@19469  1288 proof (induct n)  kleing@19469  1289  case 0  kleing@19469  1290  show ?case by simp  kleing@19469  1291 next  kleing@19469  1292  case (Suc n)  huffman@47222  1293  then show ?case  huffman@47222  1294  by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one)  huffman@47222  1295  (* FIXME: make numeral cancellation simprocs work for semirings *)  kleing@19469  1296 qed  kleing@19469  1297 kleing@19469  1298 theorem arith_series_general:  huffman@47222  1299  "(2::'a::comm_semiring_1) * (\i\{.. 1"  kleing@19469  1303  let ?I = "\i. of_nat i" and ?n = "of_nat n"  kleing@19469  1304  have  kleing@19469  1305  "(\i\{..i\{..i\{.. = ?n*a + (\i\{.. = (?n*a + d*(\i\{1.. = 2*?n*a + d*2*(\i\{1..i\{1..n - 1}. ?I i) = (2*?n*a + d*?I (n - 1)*?I n)"  huffman@30079  1318  by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)  huffman@23431  1319  (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]])  huffman@47222  1320  finally show ?thesis  huffman@47222  1321  unfolding mult_2 by (simp add: algebra_simps)  kleing@19469  1322 next  kleing@19469  1323  assume "\(n > 1)"  kleing@19469  1324  hence "n = 1 \ n = 0" by auto  huffman@47222  1325  thus ?thesis by (auto simp: mult_2)  kleing@19469  1326 qed  kleing@19469  1327 kleing@19469  1328 lemma arith_series_nat:  huffman@47222  1329  "(2::nat) * (\i\{..i\{..i\{..nat"  kleing@19022  1345  shows  kleing@19022  1346  "\x. Q x \ P x \  kleing@19022  1347  (\xxxxx 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1373  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1374  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10)  paulson@29960  1375  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10)  paulson@29960  1376 syntax (xsymbols)  paulson@29960  1377  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1378  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1379  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1380  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1381 syntax (HTML output)  paulson@29960  1382  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1383  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1384  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1385  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1386 syntax (latex_prod output)  paulson@29960  1387  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1388  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1389  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1390  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1391  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1392  ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1393  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1394  ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1395 paulson@29960  1396 translations  paulson@29960  1397  "\x=a..b. t" == "CONST setprod (%x. t) {a..b}"  paulson@29960  1398  "\x=a..i\n. t" == "CONST setprod (\i. t) {..n}"  paulson@29960  1400  "\ii. t) {..= 0 \ nat_set {x..y}"  haftmann@33318  1416  by (simp add: nat_set_def)  haftmann@33318  1417 haftmann@35644  1418 declare transfer_morphism_nat_int[transfer add  haftmann@33318  1419  return: transfer_nat_int_set_functions  haftmann@33318  1420  transfer_nat_int_set_function_closures  haftmann@33318  1421 ]  haftmann@33318  1422 haftmann@33318  1423 lemma transfer_int_nat_set_functions:  haftmann@33318  1424  "is_nat m \ is_nat n \ {m..n} = int  {nat m..nat n}"  haftmann@33318  1425  by (simp only: is_nat_def transfer_nat_int_set_functions  haftmann@33318  1426  transfer_nat_int_set_function_closures  haftmann@33318  1427  transfer_nat_int_set_return_embed nat_0_le  haftmann@33318  1428  cong: transfer_nat_int_set_cong)  haftmann@33318  1429 haftmann@33318  1430 lemma transfer_int_nat_set_function_closures:  haftmann@33318  1431  "is_nat x \ nat_set {x..y}"  haftmann@33318  1432  by (simp only: transfer_nat_int_set_function_closures is_nat_def)  haftmann@33318  1433 haftmann@35644  1434 declare transfer_morphism_int_nat[transfer add  haftmann@33318  1435  return: transfer_int_nat_set_functions  haftmann@33318  1436  transfer_int_nat_set_function_closures  haftmann@33318  1437 ]  haftmann@33318  1438 nipkow@8924  1439 end