src/HOL/SetInterval.thy
 author hoelzl Tue Jan 18 21:37:23 2011 +0100 (2011-01-18) changeset 41654 32fe42892983 parent 40703 d1fc454d6735 child 42891 e2f473671937 permissions -rw-r--r--
Gauge measure removed
 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  nipkow@24691  17 definition  wenzelm@32960  18  lessThan :: "'a => 'a set" ("(1{..<_})") where  haftmann@25062  19  "{.. 'a set" ("(1{.._})") where  haftmann@25062  23  "{..u} == {x. x \ u}"  nipkow@24691  24 nipkow@24691  25 definition  wenzelm@32960  26  greaterThan :: "'a => 'a set" ("(1{_<..})") where  haftmann@25062  27  "{l<..} == {x. l 'a set" ("(1{_..})") where  haftmann@25062  31  "{l..} == {x. l\x}"  nipkow@24691  32 nipkow@24691  33 definition  haftmann@25062  34  greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where  haftmann@25062  35  "{l<.. 'a => 'a set" ("(1{_..<_})") where  haftmann@25062  39  "{l.. 'a => 'a set" ("(1{_<.._})") where  haftmann@25062  43  "{l<..u} == {l<..} Int {..u}"  nipkow@24691  44 nipkow@24691  45 definition  haftmann@25062  46  atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where  haftmann@25062  47  "{l..u} == {l..} Int {..u}"  nipkow@24691  48 nipkow@24691  49 end  nipkow@8924  50 ballarin@13735  51 nipkow@15048  52 text{* A note of warning when using @{term"{.. 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10)  huffman@36364  58  "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" [0, 0, 10] 10)  huffman@36364  59  "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" [0, 0, 10] 10)  huffman@36364  60  "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10)  kleing@14418  61 nipkow@30372  62 syntax (xsymbols)  huffman@36364  63  "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\ _\_./ _)" [0, 0, 10] 10)  huffman@36364  64  "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" [0, 0, 10] 10)  huffman@36364  65  "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\ _\_./ _)" [0, 0, 10] 10)  huffman@36364  66  "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" [0, 0, 10] 10)  kleing@14418  67 nipkow@30372  68 syntax (latex output)  huffman@36364  69  "_UNION_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" [0, 0, 10] 10)  huffman@36364  70  "_UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" [0, 0, 10] 10)  huffman@36364  71  "_INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" [0, 0, 10] 10)  huffman@36364  72  "_INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" [0, 0, 10] 10)  kleing@14418  73 kleing@14418  74 translations  kleing@14418  75  "UN i<=n. A" == "UN i:{..n}. A"  nipkow@15045  76  "UN i atLeast y) = (y \ (x::'a::order))"  paulson@15418  124 by (blast intro: order_trans)  paulson@13850  125 paulson@13850  126 lemma atLeast_eq_iff [iff]:  paulson@15418  127  "(atLeast x = atLeast y) = (x = (y::'a::linorder))"  paulson@13850  128 by (blast intro: order_antisym order_trans)  paulson@13850  129 paulson@13850  130 lemma greaterThan_subset_iff [iff]:  paulson@15418  131  "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))"  paulson@15418  132 apply (auto simp add: greaterThan_def)  paulson@15418  133  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  134 done  paulson@13850  135 paulson@13850  136 lemma greaterThan_eq_iff [iff]:  paulson@15418  137  "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"  paulson@15418  138 apply (rule iffI)  paulson@15418  139  apply (erule equalityE)  haftmann@29709  140  apply simp_all  paulson@13850  141 done  paulson@13850  142 paulson@15418  143 lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))"  paulson@13850  144 by (blast intro: order_trans)  paulson@13850  145 paulson@15418  146 lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"  paulson@13850  147 by (blast intro: order_antisym order_trans)  paulson@13850  148 paulson@13850  149 lemma lessThan_subset_iff [iff]:  paulson@15418  150  "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))"  paulson@15418  151 apply (auto simp add: lessThan_def)  paulson@15418  152  apply (subst linorder_not_less [symmetric], blast)  paulson@13850  153 done  paulson@13850  154 paulson@13850  155 lemma lessThan_eq_iff [iff]:  paulson@15418  156  "(lessThan x = lessThan y) = (x = (y::'a::linorder))"  paulson@15418  157 apply (rule iffI)  paulson@15418  158  apply (erule equalityE)  haftmann@29709  159  apply simp_all  ballarin@13735  160 done  ballarin@13735  161 hoelzl@40703  162 lemma lessThan_strict_subset_iff:  hoelzl@40703  163  fixes m n :: "'a::linorder"  hoelzl@40703  164  shows "{.. m < n"  hoelzl@40703  165  by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)  ballarin@13735  166 paulson@13850  167 subsection {*Two-sided intervals*}  ballarin@13735  168 nipkow@24691  169 context ord  nipkow@24691  170 begin  nipkow@24691  171 blanchet@35828  172 lemma greaterThanLessThan_iff [simp,no_atp]:  haftmann@25062  173  "(i : {l<.. {a..b} = {}"  nipkow@32400  201 by(auto simp: atLeastAtMost_def atLeast_def atMost_def)  nipkow@32400  202 nipkow@32400  203 lemma atLeastatMost_empty_iff[simp]:  nipkow@32400  204  "{a..b} = {} \ (~ a <= b)"  nipkow@32400  205 by auto (blast intro: order_trans)  nipkow@32400  206 nipkow@32400  207 lemma atLeastatMost_empty_iff2[simp]:  nipkow@32400  208  "{} = {a..b} \ (~ a <= b)"  nipkow@32400  209 by auto (blast intro: order_trans)  nipkow@32400  210 nipkow@32400  211 lemma atLeastLessThan_empty[simp]:  nipkow@32400  212  "b <= a \ {a.. (~ a < b)"  nipkow@32400  217 by auto (blast intro: le_less_trans)  nipkow@32400  218 nipkow@32400  219 lemma atLeastLessThan_empty_iff2[simp]:  nipkow@32400  220  "{} = {a.. (~ a < b)"  nipkow@32400  221 by auto (blast intro: le_less_trans)  nipkow@15554  222 nipkow@32400  223 lemma greaterThanAtMost_empty[simp]: "l \ k ==> {k<..l} = {}"  nipkow@17719  224 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)  nipkow@17719  225 nipkow@32400  226 lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ ~ k < l"  nipkow@32400  227 by auto (blast intro: less_le_trans)  nipkow@32400  228 nipkow@32400  229 lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ ~ k < l"  nipkow@32400  230 by auto (blast intro: less_le_trans)  nipkow@32400  231 haftmann@29709  232 lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. {a .. b} = {a}" by simp  hoelzl@36846  239 nipkow@32400  240 lemma atLeastatMost_subset_iff[simp]:  nipkow@32400  241  "{a..b} <= {c..d} \ (~ a <= b) | c <= a & b <= d"  nipkow@32400  242 unfolding atLeastAtMost_def atLeast_def atMost_def  nipkow@32400  243 by (blast intro: order_trans)  nipkow@32400  244 nipkow@32400  245 lemma atLeastatMost_psubset_iff:  nipkow@32400  246  "{a..b} < {c..d} \  nipkow@32400  247  ((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d"  nipkow@39302  248 by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)  nipkow@32400  249 hoelzl@36846  250 lemma atLeastAtMost_singleton_iff[simp]:  hoelzl@36846  251  "{a .. b} = {c} \ a = b \ b = c"  hoelzl@36846  252 proof  hoelzl@36846  253  assume "{a..b} = {c}"  hoelzl@36846  254  hence "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp  hoelzl@36846  255  moreover with {a..b} = {c} have "c \ a \ b \ c" by auto  hoelzl@36846  256  ultimately show "a = b \ b = c" by auto  hoelzl@36846  257 qed simp  hoelzl@36846  258 nipkow@24691  259 end  paulson@14485  260 nipkow@32408  261 lemma (in linorder) atLeastLessThan_subset_iff:  nipkow@32408  262  "{a.. b <= a | c<=a & b<=d"  nipkow@32408  263 apply (auto simp:subset_eq Ball_def)  nipkow@32408  264 apply(frule_tac x=a in spec)  nipkow@32408  265 apply(erule_tac x=d in allE)  nipkow@32408  266 apply (simp add: less_imp_le)  nipkow@32408  267 done  nipkow@32408  268 hoelzl@40703  269 lemma atLeastLessThan_inj:  hoelzl@40703  270  fixes a b c d :: "'a::linorder"  hoelzl@40703  271  assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"  hoelzl@40703  272  shows "a = c" "b = d"  hoelzl@40703  273 using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+  hoelzl@40703  274 hoelzl@40703  275 lemma atLeastLessThan_eq_iff:  hoelzl@40703  276  fixes a b c d :: "'a::linorder"  hoelzl@40703  277  assumes "a < b" "c < d"  hoelzl@40703  278  shows "{a ..< b} = {c ..< d} \ a = c \ b = d"  hoelzl@40703  279  using atLeastLessThan_inj assms by auto  hoelzl@40703  280 nipkow@32456  281 subsubsection {* Intersection *}  nipkow@32456  282 nipkow@32456  283 context linorder  nipkow@32456  284 begin  nipkow@32456  285 nipkow@32456  286 lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"  nipkow@32456  287 by auto  nipkow@32456  288 nipkow@32456  289 lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"  nipkow@32456  290 by auto  nipkow@32456  291 nipkow@32456  292 lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"  nipkow@32456  293 by auto  nipkow@32456  294 nipkow@32456  295 lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"  nipkow@32456  296 by auto  nipkow@32456  297 nipkow@32456  298 lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"  nipkow@32456  299 by auto  nipkow@32456  300 nipkow@32456  301 lemma Int_atLeastLessThan[simp]: "{a.. Suc  {.. Suc (x - 1)" by auto  hoelzl@39072  331  with x < Suc n show "x = 0" by auto  hoelzl@39072  332 qed  hoelzl@39072  333 paulson@14485  334 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"  paulson@14485  335 by (simp add: lessThan_def atMost_def less_Suc_eq_le)  paulson@14485  336 paulson@14485  337 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"  paulson@14485  338 by blast  paulson@14485  339 paulson@15047  340 subsubsection {* The Constant @{term greaterThan} *}  paulson@15047  341 paulson@14485  342 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"  paulson@14485  343 apply (simp add: greaterThan_def)  paulson@14485  344 apply (blast dest: gr0_conv_Suc [THEN iffD1])  paulson@14485  345 done  paulson@14485  346 paulson@14485  347 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"  paulson@14485  348 apply (simp add: greaterThan_def)  paulson@14485  349 apply (auto elim: linorder_neqE)  paulson@14485  350 done  paulson@14485  351 paulson@14485  352 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"  paulson@14485  353 by blast  paulson@14485  354 paulson@15047  355 subsubsection {* The Constant @{term atLeast} *}  paulson@15047  356 paulson@14485  357 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"  paulson@14485  358 by (unfold atLeast_def UNIV_def, simp)  paulson@14485  359 paulson@14485  360 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"  paulson@14485  361 apply (simp add: atLeast_def)  paulson@14485  362 apply (simp add: Suc_le_eq)  paulson@14485  363 apply (simp add: order_le_less, blast)  paulson@14485  364 done  paulson@14485  365 paulson@14485  366 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"  paulson@14485  367  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)  paulson@14485  368 paulson@14485  369 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"  paulson@14485  370 by blast  paulson@14485  371 paulson@15047  372 subsubsection {* The Constant @{term atMost} *}  paulson@15047  373 paulson@14485  374 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"  paulson@14485  375 by (simp add: atMost_def)  paulson@14485  376 paulson@14485  377 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"  paulson@14485  378 apply (simp add: atMost_def)  paulson@14485  379 apply (simp add: less_Suc_eq order_le_less, blast)  paulson@14485  380 done  paulson@14485  381 paulson@14485  382 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"  paulson@14485  383 by blast  paulson@14485  384 paulson@15047  385 subsubsection {* The Constant @{term atLeastLessThan} *}  paulson@15047  386 nipkow@28068  387 text{*The orientation of the following 2 rules is tricky. The lhs is  nipkow@24449  388 defined in terms of the rhs. Hence the chosen orientation makes sense  nipkow@24449  389 in this theory --- the reverse orientation complicates proofs (eg  nipkow@24449  390 nontermination). But outside, when the definition of the lhs is rarely  nipkow@24449  391 used, the opposite orientation seems preferable because it reduces a  nipkow@24449  392 specific concept to a more general one. *}  nipkow@28068  393 paulson@15047  394 lemma atLeast0LessThan: "{0::nat.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  434 by (auto simp add: atLeastAtMost_def)  nipkow@15554  435 paulson@33044  436 lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j.. ?B" by auto  nipkow@16733  447 next  nipkow@16733  448  show "?B \ ?A"  nipkow@16733  449  proof  nipkow@16733  450  fix n assume a: "n : ?B"  webertj@20217  451  hence "n - k : {i..j}" by auto  nipkow@16733  452  moreover have "n = (n - k) + k" using a by auto  nipkow@16733  453  ultimately show "n : ?A" by blast  nipkow@16733  454  qed  nipkow@16733  455 qed  nipkow@16733  456 nipkow@16733  457 lemma image_add_atLeastLessThan:  nipkow@16733  458  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  461 next  nipkow@16733  462  show "?B \ ?A"  nipkow@16733  463  proof  nipkow@16733  464  fix n assume a: "n : ?B"  webertj@20217  465  hence "n - k : {i..i. i - c)  {x ..< y} =  hoelzl@37664  489  (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"  hoelzl@37664  490  (is "_ = ?right")  hoelzl@37664  491 proof safe  hoelzl@37664  492  fix a assume a: "a \ ?right"  hoelzl@37664  493  show "a \ (\i. i - c)  {x ..< y}"  hoelzl@37664  494  proof cases  hoelzl@37664  495  assume "c < y" with a show ?thesis  hoelzl@37664  496  by (auto intro!: image_eqI[of _ _ "a + c"])  hoelzl@37664  497  next  hoelzl@37664  498  assume "\ c < y" with a show ?thesis  hoelzl@37664  499  by (auto intro!: image_eqI[of _ _ x] split: split_if_asm)  hoelzl@37664  500  qed  hoelzl@37664  501 qed auto  hoelzl@37664  502 hoelzl@35580  503 context ordered_ab_group_add  hoelzl@35580  504 begin  hoelzl@35580  505 hoelzl@35580  506 lemma  hoelzl@35580  507  fixes x :: 'a  hoelzl@35580  508  shows image_uminus_greaterThan[simp]: "uminus  {x<..} = {..<-x}"  hoelzl@35580  509  and image_uminus_atLeast[simp]: "uminus  {x..} = {..-x}"  hoelzl@35580  510 proof safe  hoelzl@35580  511  fix y assume "y < -x"  hoelzl@35580  512  hence *: "x < -y" using neg_less_iff_less[of "-y" x] by simp  hoelzl@35580  513  have "- (-y) \ uminus  {x<..}"  hoelzl@35580  514  by (rule imageI) (simp add: *)  hoelzl@35580  515  thus "y \ uminus  {x<..}" by simp  hoelzl@35580  516 next  hoelzl@35580  517  fix y assume "y \ -x"  hoelzl@35580  518  have "- (-y) \ uminus  {x..}"  hoelzl@35580  519  by (rule imageI) (insert y \ -x[THEN le_imp_neg_le], simp)  hoelzl@35580  520  thus "y \ uminus  {x..}" by simp  hoelzl@35580  521 qed simp_all  hoelzl@35580  522 hoelzl@35580  523 lemma  hoelzl@35580  524  fixes x :: 'a  hoelzl@35580  525  shows image_uminus_lessThan[simp]: "uminus  {.. finite N"  nipkow@28068  572 apply (rule finite_subset)  nipkow@28068  573  apply (rule_tac [2] finite_lessThan, auto)  nipkow@28068  574 done  nipkow@28068  575 nipkow@31044  576 text {* A set of natural numbers is finite iff it is bounded. *}  nipkow@31044  577 lemma finite_nat_set_iff_bounded:  nipkow@31044  578  "finite(N::nat set) = (EX m. ALL n:N. nnat. (!!n. n \ f n) ==> finite {n. f n \ u}"  nipkow@28068  594 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)  paulson@14485  595 nipkow@24853  596 text{* Any subset of an interval of natural numbers the size of the  nipkow@24853  597 subset is exactly that interval. *}  nipkow@24853  598 nipkow@24853  599 lemma subset_card_intvl_is_intvl:  nipkow@24853  600  "A <= {k.. A = {k..i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B")  nipkow@36755  622 proof  nipkow@36755  623  show "?A <= ?B"  nipkow@36755  624  proof  nipkow@36755  625  fix x assume "x : ?A"  nipkow@36755  626  then obtain i where i: "i\n" "x : M i" by auto  nipkow@36755  627  show "x : ?B"  nipkow@36755  628  proof(cases i)  nipkow@36755  629  case 0 with i show ?thesis by simp  nipkow@36755  630  next  nipkow@36755  631  case (Suc j) with i show ?thesis by auto  nipkow@36755  632  qed  nipkow@36755  633  qed  nipkow@36755  634 next  nipkow@36755  635  show "?B <= ?A" by auto  nipkow@36755  636 qed  nipkow@36755  637 nipkow@36755  638 lemma UN_le_add_shift:  nipkow@36755  639  "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B")  nipkow@36755  640 proof  nipkow@36755  641  show "?A <= ?B" by fastsimp  nipkow@36755  642 next  nipkow@36755  643  show "?B <= ?A"  nipkow@36755  644  proof  nipkow@36755  645  fix x assume "x : ?B"  nipkow@36755  646  then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto  nipkow@36755  647  hence "i-k\n & x : M((i-k)+k)" by auto  nipkow@36755  648  thus "x : ?A" by blast  nipkow@36755  649  qed  nipkow@36755  650 qed  nipkow@36755  651 paulson@32596  652 lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)"  paulson@32596  653  by (auto simp add: atLeast0LessThan)  paulson@32596  654 paulson@32596  655 lemma UN_finite_subset: "(!!n::nat. (\i\{0.. C) \ (\n. A n) \ C"  paulson@32596  656  by (subst UN_UN_finite_eq [symmetric]) blast  paulson@32596  657 paulson@33044  658 lemma UN_finite2_subset:  paulson@33044  659  "(!!n::nat. (\i\{0.. (\i\{0.. (\n. A n) \ (\n. B n)"  paulson@33044  660  apply (rule UN_finite_subset)  paulson@33044  661  apply (subst UN_UN_finite_eq [symmetric, of B])  paulson@33044  662  apply blast  paulson@33044  663  done  paulson@32596  664 paulson@32596  665 lemma UN_finite2_eq:  paulson@33044  666  "(!!n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)"  paulson@33044  667  apply (rule subset_antisym)  paulson@33044  668  apply (rule UN_finite2_subset, blast)  paulson@33044  669  apply (rule UN_finite2_subset [where k=k])  huffman@35216  670  apply (force simp add: atLeastLessThan_add_Un [of 0])  paulson@33044  671  done  paulson@32596  672 paulson@32596  673 paulson@14485  674 subsubsection {* Cardinality *}  paulson@14485  675 nipkow@15045  676 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  715 apply(drule ex_bij_betw_finite_nat)  nipkow@31438  716 apply(drule ex_bij_betw_nat_finite)  nipkow@31438  717 apply(auto intro!:bij_betw_trans)  nipkow@31438  718 done  nipkow@31438  719 nipkow@31438  720 lemma ex_bij_betw_nat_finite_1:  nipkow@31438  721  "finite M \ \h. bij_betw h {1 .. card M} M"  nipkow@31438  722 by (rule finite_same_card_bij) auto  nipkow@31438  723 hoelzl@40703  724 lemma bij_betw_iff_card:  hoelzl@40703  725  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  726  shows BIJ: "(\f. bij_betw f A B) \ (card A = card B)"  hoelzl@40703  727 using assms  hoelzl@40703  728 proof(auto simp add: bij_betw_same_card)  hoelzl@40703  729  assume *: "card A = card B"  hoelzl@40703  730  obtain f where "bij_betw f A {0 ..< card A}"  hoelzl@40703  731  using FIN ex_bij_betw_finite_nat by blast  hoelzl@40703  732  moreover obtain g where "bij_betw g {0 ..< card B} B"  hoelzl@40703  733  using FIN' ex_bij_betw_nat_finite by blast  hoelzl@40703  734  ultimately have "bij_betw (g o f) A B"  hoelzl@40703  735  using * by (auto simp add: bij_betw_trans)  hoelzl@40703  736  thus "(\f. bij_betw f A B)" by blast  hoelzl@40703  737 qed  hoelzl@40703  738 hoelzl@40703  739 lemma inj_on_iff_card_le:  hoelzl@40703  740  assumes FIN: "finite A" and FIN': "finite B"  hoelzl@40703  741  shows "(\f. inj_on f A \ f  A \ B) = (card A \ card B)"  hoelzl@40703  742 proof (safe intro!: card_inj_on_le)  hoelzl@40703  743  assume *: "card A \ card B"  hoelzl@40703  744  obtain f where 1: "inj_on f A" and 2: "f  A = {0 ..< card A}"  hoelzl@40703  745  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force  hoelzl@40703  746  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g  {0 ..< card B} = B"  hoelzl@40703  747  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force  hoelzl@40703  748  ultimately have "inj_on g (f  A)" using subset_inj_on[of g _ "f  A"] * by force  hoelzl@40703  749  hence "inj_on (g o f) A" using 1 comp_inj_on by blast  hoelzl@40703  750  moreover  hoelzl@40703  751  {have "{0 ..< card A} \ {0 ..< card B}" using * by force  hoelzl@40703  752  with 2 have "f  A \ {0 ..< card B}" by blast  hoelzl@40703  753  hence "(g o f)  A \ B" unfolding comp_def using 3 by force  hoelzl@40703  754  }  hoelzl@40703  755  ultimately show "(\f. inj_on f A \ f  A \ B)" by blast  hoelzl@40703  756 qed (insert assms, auto)  nipkow@26105  757 paulson@14485  758 subsection {* Intervals of integers *}  paulson@14485  759 nipkow@15045  760 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l.. u ==>  nipkow@15045  773  {(0::int).. u")  paulson@14485  782  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  783  apply (rule finite_imageI)  paulson@14485  784  apply auto  paulson@14485  785  done  paulson@14485  786 nipkow@15045  787 lemma finite_atLeastLessThan_int [iff]: "finite {l.. u")  paulson@14485  809  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  810  apply (subst card_image)  paulson@14485  811  apply (auto simp add: inj_on_def)  paulson@14485  812  done  paulson@14485  813 nipkow@15045  814 lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}"  bulwahn@27656  836 proof -  bulwahn@27656  837  have "{k. P k \ k < i} \ {.. M"  bulwahn@27656  843 shows "card {k \ M. k < Suc i} \ 0"  bulwahn@27656  844 proof -  bulwahn@27656  845  from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto  bulwahn@27656  846  with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)  bulwahn@27656  847 qed  bulwahn@27656  848 bulwahn@27656  849 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"  haftmann@37388  850 apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"])  bulwahn@27656  851 apply simp  bulwahn@27656  852 apply fastsimp  bulwahn@27656  853 apply auto  bulwahn@27656  854 apply (rule inj_on_diff_nat)  bulwahn@27656  855 apply auto  bulwahn@27656  856 apply (case_tac x)  bulwahn@27656  857 apply auto  bulwahn@27656  858 apply (case_tac xa)  bulwahn@27656  859 apply auto  bulwahn@27656  860 apply (case_tac xa)  bulwahn@27656  861 apply auto  bulwahn@27656  862 done  bulwahn@27656  863 bulwahn@27656  864 lemma card_less_Suc:  bulwahn@27656  865  assumes zero_in_M: "0 \ M"  bulwahn@27656  866  shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"  bulwahn@27656  867 proof -  bulwahn@27656  868  from assms have a: "0 \ {k \ M. k < Suc i}" by simp  bulwahn@27656  869  hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})"  bulwahn@27656  870  by (auto simp only: insert_Diff)  bulwahn@27656  871  have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto  bulwahn@27656  872  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  873  apply (subst card_insert)  bulwahn@27656  874  apply simp_all  bulwahn@27656  875  apply (subst b)  bulwahn@27656  876  apply (subst card_less_Suc2[symmetric])  bulwahn@27656  877  apply simp_all  bulwahn@27656  878  done  bulwahn@27656  879  with c show ?thesis by simp  bulwahn@27656  880 qed  bulwahn@27656  881 paulson@14485  882 paulson@13850  883 subsection {*Lemmas useful with the summation operator setsum*}  paulson@13850  884 ballarin@16102  885 text {* For examples, see Algebra/poly/UnivPoly2.thy *}  ballarin@13735  886 wenzelm@14577  887 subsubsection {* Disjoint Unions *}  ballarin@13735  888 wenzelm@14577  889 text {* Singletons and open intervals *}  ballarin@13735  890 ballarin@13735  891 lemma ivl_disj_un_singleton:  nipkow@15045  892  "{l::'a::linorder} Un {l<..} = {l..}"  nipkow@15045  893  "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  897  "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  906  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  908  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  910  "(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  922  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  924 by auto  ballarin@13735  925 ballarin@13735  926 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two  ballarin@13735  927 wenzelm@14577  928 subsubsection {* Disjoint Intersections *}  ballarin@13735  929 wenzelm@14577  930 text {* One- and two-sided intervals *}  ballarin@13735  931 ballarin@13735  932 lemma ivl_disj_int_one:  nipkow@15045  933  "{..l::'a::order} Int {l<.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  969 apply(auto simp:linorder_not_le)  nipkow@15542  970 apply(rule ccontr)  nipkow@15542  971 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  972 apply(clarsimp simp:linorder_not_le)  nipkow@15542  973 apply(fastsimp)  nipkow@15542  974 done  nipkow@15542  975 nipkow@15041  976 nipkow@15042  977 subsection {* Summation indexed over intervals *}  nipkow@15042  978 nipkow@15042  979 syntax  nipkow@15042  980  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  981  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  982  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@16052  983  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  nipkow@15042  984 syntax (xsymbols)  nipkow@15042  985  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  986  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  987  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  988  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15042  989 syntax (HTML output)  nipkow@15042  990  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  991  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  992  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  993  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15056  994 syntax (latex_sum output)  nipkow@15052  995  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  996  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@15052  997  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  998  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@16052  999  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1000  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15052  1001  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  1002  ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15041  1003 nipkow@15048  1004 translations  nipkow@28853  1005  "\x=a..b. t" == "CONST setsum (%x. t) {a..b}"  nipkow@28853  1006  "\x=a..i\n. t" == "CONST setsum (\i. t) {..n}"  nipkow@28853  1008  "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  1016 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  1018 @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \  nipkow@15542  1041  setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)"  nipkow@16052  1048 by (simp add:atMost_Suc add_ac)  nipkow@16052  1049 nipkow@16041  1050 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n"  nipkow@16041  1051 by (simp add:lessThan_Suc add_ac)  nipkow@15041  1052 nipkow@15911  1053 lemma setsum_cl_ivl_Suc[simp]:  nipkow@15561  1054  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  nipkow@15561  1055 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@15561  1056 nipkow@15911  1057 lemma setsum_op_ivl_Suc[simp]:  nipkow@15561  1058  "setsum f {m..  nipkow@15561  1062  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  nipkow@15561  1063 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@16041  1064 *)  nipkow@28068  1065 nipkow@28068  1066 lemma setsum_head:  nipkow@28068  1067  fixes n :: nat  nipkow@28068  1068  assumes mn: "m <= n"  nipkow@28068  1069  shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  nipkow@28068  1070 proof -  nipkow@28068  1071  from mn  nipkow@28068  1072  have "{m..n} = {m} \ {m<..n}"  nipkow@28068  1073  by (auto intro: ivl_disj_un_singleton)  nipkow@28068  1074  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  nipkow@28068  1075  by (simp add: atLeast0LessThan)  nipkow@28068  1076  also have "\ = ?rhs" by simp  nipkow@28068  1077  finally show ?thesis .  nipkow@28068  1078 qed  nipkow@28068  1079 nipkow@28068  1080 lemma setsum_head_Suc:  nipkow@28068  1081  "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}"  nipkow@28068  1082 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)  nipkow@28068  1083 nipkow@28068  1084 lemma setsum_head_upt_Suc:  nipkow@28068  1085  "m < n \ setsum f {m.. n + 1"  nipkow@31501  1091  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"  nipkow@31501  1092 proof-  nipkow@31501  1093  have "{m .. n+p} = {m..n} \ {n+1..n+p}" using m \ n+1 by auto  nipkow@31501  1094  thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint  nipkow@31501  1095  atLeastSucAtMost_greaterThanAtMost)  nipkow@31501  1096 qed  nipkow@28068  1097 nipkow@15539  1098 lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \  nipkow@15539  1099  setsum f {m.. 'a::ab_group_add"  nipkow@15539  1104 shows "\ m \ n; n \ p \ \  nipkow@15539  1105  setsum f {m.. ('a::ab_group_add)"  nipkow@31505  1112  shows "setsum (\k. f k - f(k + 1)) {(m::nat) .. n} =  nipkow@31505  1113  (if m <= n then f m - f(n + 1) else 0)"  nipkow@31505  1114 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)  nipkow@31505  1115 nipkow@31509  1116 lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]  nipkow@31509  1117 nipkow@31509  1118 lemma setsum_setsum_restrict:  nipkow@31509  1119  "finite S \ finite T \ 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"  nipkow@31509  1120  by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)  nipkow@31509  1121  (rule setsum_commute)  nipkow@31509  1122 nipkow@31509  1123 lemma setsum_image_gen: assumes fS: "finite S"  nipkow@31509  1124  shows "setsum g S = setsum (\y. setsum g {x. x \ S \ f x = y}) (f  S)"  nipkow@31509  1125 proof-  nipkow@31509  1126  { fix x assume "x \ S" then have "{y. y\ fS \ f x = y} = {f x}" by auto }  nipkow@31509  1127  hence "setsum g S = setsum (\x. setsum (\y. g x) {y. y\ fS \ f x = y}) S"  nipkow@31509  1128  by simp  nipkow@31509  1129  also have "\ = setsum (\y. setsum g {x. x \ S \ f x = y}) (f  S)"  nipkow@31509  1130  by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]])  nipkow@31509  1131  finally show ?thesis .  nipkow@31509  1132 qed  nipkow@31509  1133 hoelzl@35171  1134 lemma setsum_le_included:  haftmann@36307  1135  fixes f :: "'a \ 'b::ordered_comm_monoid_add"  hoelzl@35171  1136  assumes "finite s" "finite t"  hoelzl@35171  1137  and "\y\t. 0 \ g y" "(\x\s. \y\t. i y = x \ f x \ g y)"  hoelzl@35171  1138  shows "setsum f s \ setsum g t"  hoelzl@35171  1139 proof -  hoelzl@35171  1140  have "setsum f s \ setsum (\y. setsum g {x. x\t \ i x = y}) s"  hoelzl@35171  1141  proof (rule setsum_mono)  hoelzl@35171  1142  fix y assume "y \ s"  hoelzl@35171  1143  with assms obtain z where z: "z \ t" "y = i z" "f y \ g z" by auto  hoelzl@35171  1144  with assms show "f y \ setsum g {x \ t. i x = y}" (is "?A y \ ?B y")  hoelzl@35171  1145  using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]  hoelzl@35171  1146  by (auto intro!: setsum_mono2)  hoelzl@35171  1147  qed  hoelzl@35171  1148  also have "... \ setsum (\y. setsum g {x. x\t \ i x = y}) (i  t)"  hoelzl@35171  1149  using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)  hoelzl@35171  1150  also have "... \ setsum g t"  hoelzl@35171  1151  using assms by (auto simp: setsum_image_gen[symmetric])  hoelzl@35171  1152  finally show ?thesis .  hoelzl@35171  1153 qed  hoelzl@35171  1154 nipkow@31509  1155 lemma setsum_multicount_gen:  nipkow@31509  1156  assumes "finite s" "finite t" "\j\t. (card {i\s. R i j} = k j)"  nipkow@31509  1157  shows "setsum (\i. (card {j\t. R i j})) s = setsum k t" (is "?l = ?r")  nipkow@31509  1158 proof-  nipkow@31509  1159  have "?l = setsum (\i. setsum (\x.1) {j\t. R i j}) s" by auto  nipkow@31509  1160  also have "\ = ?r" unfolding setsum_setsum_restrict[OF assms(1-2)]  nipkow@31509  1161  using assms(3) by auto  nipkow@31509  1162  finally show ?thesis .  nipkow@31509  1163 qed  nipkow@31509  1164 nipkow@31509  1165 lemma setsum_multicount:  nipkow@31509  1166  assumes "finite S" "finite T" "\j\T. (card {i\S. R i j} = k)"  nipkow@31509  1167  shows "setsum (\i. card {j\T. R i j}) S = k * card T" (is "?l = ?r")  nipkow@31509  1168 proof-  nipkow@31509  1169  have "?l = setsum (\i. k) T" by(rule setsum_multicount_gen)(auto simp:assms)  huffman@35216  1170  also have "\ = ?r" by(simp add: mult_commute)  nipkow@31509  1171  finally show ?thesis by auto  nipkow@31509  1172 qed  nipkow@31509  1173 nipkow@28068  1174 nipkow@16733  1175 subsection{* Shifting bounds *}  nipkow@16733  1176 nipkow@15539  1177 lemma setsum_shift_bounds_nat_ivl:  nipkow@15539  1178  "setsum f {m+k.. setsum f {Suc 0..k} = setsum f {0..k}"  nipkow@28068  1197 by(simp add:setsum_head_Suc)  kleing@19106  1198 nipkow@28068  1199 lemma setsum_shift_lb_Suc0_0_upt:  nipkow@28068  1200  "f(0::nat) = 0 \ setsum f {Suc 0.. 1"  haftmann@36307  1209  shows "(\i=0.. 0" by simp_all  haftmann@36307  1212  moreover have "(\i=0.. 0 have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp  haftmann@36350  1218  ultimately show ?case by (simp add: field_simps divide_inverse)  haftmann@36307  1219  qed  haftmann@36307  1220  ultimately show ?thesis by simp  haftmann@36307  1221 qed  haftmann@36307  1222 ballarin@17149  1223 kleing@19469  1224 subsection {* The formula for arithmetic sums *}  kleing@19469  1225 kleing@19469  1226 lemma gauss_sum:  huffman@23277  1227  "((1::'a::comm_semiring_1) + 1)*(\i\{1..n}. of_nat i) =  kleing@19469  1228  of_nat n*((of_nat n)+1)"  kleing@19469  1229 proof (induct n)  kleing@19469  1230  case 0  kleing@19469  1231  show ?case by simp  kleing@19469  1232 next  kleing@19469  1233  case (Suc n)  nipkow@29667  1234  then show ?case by (simp add: algebra_simps)  kleing@19469  1235 qed  kleing@19469  1236 kleing@19469  1237 theorem arith_series_general:  huffman@23277  1238  "((1::'a::comm_semiring_1) + 1) * (\i\{.. 1"  kleing@19469  1242  let ?I = "\i. of_nat i" and ?n = "of_nat n"  kleing@19469  1243  have  kleing@19469  1244  "(\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)"  huffman@30079  1257  by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)  huffman@23431  1258  (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]])  nipkow@29667  1259  finally show ?thesis by (simp add: algebra_simps)  kleing@19469  1260 next  kleing@19469  1261  assume "\(n > 1)"  kleing@19469  1262  hence "n = 1 \ n = 0" by auto  nipkow@29667  1263  thus ?thesis by (auto simp: algebra_simps)  kleing@19469  1264 qed  kleing@19469  1265 kleing@19469  1266 lemma arith_series_nat:  kleing@19469  1267  "Suc (Suc 0) * (\i\{..i\{..i\{..i\{..nat"  kleing@19022  1290  shows  kleing@19022  1291  "\x. Q x \ P x \  kleing@19022  1292  (\xxxxx 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1318  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1319  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10)  paulson@29960  1320  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10)  paulson@29960  1321 syntax (xsymbols)  paulson@29960  1322  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1323  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1324  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1325  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1326 syntax (HTML output)  paulson@29960  1327  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1328  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1329  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1330  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1331 syntax (latex_prod output)  paulson@29960  1332  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1333  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1334  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1335  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1336  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1337  ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1338  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1339  ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1340 paulson@29960  1341 translations  paulson@29960  1342  "\x=a..b. t" == "CONST setprod (%x. t) {a..b}"  paulson@29960  1343  "\x=a..i\n. t" == "CONST setprod (\i. t) {..n}"  paulson@29960  1345  "\ii. t) {..= 0 \ nat_set {x..y}"  haftmann@33318  1361  by (simp add: nat_set_def)  haftmann@33318  1362 haftmann@35644  1363 declare transfer_morphism_nat_int[transfer add  haftmann@33318  1364  return: transfer_nat_int_set_functions  haftmann@33318  1365  transfer_nat_int_set_function_closures  haftmann@33318  1366 ]  haftmann@33318  1367 haftmann@33318  1368 lemma transfer_int_nat_set_functions:  haftmann@33318  1369  "is_nat m \ is_nat n \ {m..n} = int  {nat m..nat n}"  haftmann@33318  1370  by (simp only: is_nat_def transfer_nat_int_set_functions  haftmann@33318  1371  transfer_nat_int_set_function_closures  haftmann@33318  1372  transfer_nat_int_set_return_embed nat_0_le  haftmann@33318  1373  cong: transfer_nat_int_set_cong)  haftmann@33318  1374 haftmann@33318  1375 lemma transfer_int_nat_set_function_closures:  haftmann@33318  1376  "is_nat x \ nat_set {x..y}"  haftmann@33318  1377  by (simp only: transfer_nat_int_set_function_closures is_nat_def)  haftmann@33318  1378 haftmann@35644  1379 declare transfer_morphism_int_nat[transfer add  haftmann@33318  1380  return: transfer_int_nat_set_functions  haftmann@33318  1381  transfer_int_nat_set_function_closures  haftmann@33318  1382 ]  haftmann@33318  1383 nipkow@8924  1384 end