src/HOL/SetInterval.thy
 author hoelzl Thu Sep 02 10:14:32 2010 +0200 (2010-09-02) changeset 39072 1030b1a166ef parent 37664 2946b8f057df child 39198 f967a16dfcdd permissions -rw-r--r--
 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 ballarin@13735  162 paulson@13850  163 subsection {*Two-sided intervals*}  ballarin@13735  164 nipkow@24691  165 context ord  nipkow@24691  166 begin  nipkow@24691  167 blanchet@35828  168 lemma greaterThanLessThan_iff [simp,no_atp]:  haftmann@25062  169  "(i : {l<.. {a..b} = {}"  nipkow@32400  197 by(auto simp: atLeastAtMost_def atLeast_def atMost_def)  nipkow@32400  198 nipkow@32400  199 lemma atLeastatMost_empty_iff[simp]:  nipkow@32400  200  "{a..b} = {} \ (~ a <= b)"  nipkow@32400  201 by auto (blast intro: order_trans)  nipkow@32400  202 nipkow@32400  203 lemma atLeastatMost_empty_iff2[simp]:  nipkow@32400  204  "{} = {a..b} \ (~ a <= b)"  nipkow@32400  205 by auto (blast intro: order_trans)  nipkow@32400  206 nipkow@32400  207 lemma atLeastLessThan_empty[simp]:  nipkow@32400  208  "b <= a \ {a.. (~ a < b)"  nipkow@32400  213 by auto (blast intro: le_less_trans)  nipkow@32400  214 nipkow@32400  215 lemma atLeastLessThan_empty_iff2[simp]:  nipkow@32400  216  "{} = {a.. (~ a < b)"  nipkow@32400  217 by auto (blast intro: le_less_trans)  nipkow@15554  218 nipkow@32400  219 lemma greaterThanAtMost_empty[simp]: "l \ k ==> {k<..l} = {}"  nipkow@17719  220 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)  nipkow@17719  221 nipkow@32400  222 lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ ~ k < l"  nipkow@32400  223 by auto (blast intro: less_le_trans)  nipkow@32400  224 nipkow@32400  225 lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ ~ k < l"  nipkow@32400  226 by auto (blast intro: less_le_trans)  nipkow@32400  227 haftmann@29709  228 lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. {a .. b} = {a}" by simp  hoelzl@36846  235 nipkow@32400  236 lemma atLeastatMost_subset_iff[simp]:  nipkow@32400  237  "{a..b} <= {c..d} \ (~ a <= b) | c <= a & b <= d"  nipkow@32400  238 unfolding atLeastAtMost_def atLeast_def atMost_def  nipkow@32400  239 by (blast intro: order_trans)  nipkow@32400  240 nipkow@32400  241 lemma atLeastatMost_psubset_iff:  nipkow@32400  242  "{a..b} < {c..d} \  nipkow@32400  243  ((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d"  nipkow@32400  244 by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans)  nipkow@32400  245 hoelzl@36846  246 lemma atLeastAtMost_singleton_iff[simp]:  hoelzl@36846  247  "{a .. b} = {c} \ a = b \ b = c"  hoelzl@36846  248 proof  hoelzl@36846  249  assume "{a..b} = {c}"  hoelzl@36846  250  hence "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp  hoelzl@36846  251  moreover with {a..b} = {c} have "c \ a \ b \ c" by auto  hoelzl@36846  252  ultimately show "a = b \ b = c" by auto  hoelzl@36846  253 qed simp  hoelzl@36846  254 nipkow@24691  255 end  paulson@14485  256 nipkow@32408  257 lemma (in linorder) atLeastLessThan_subset_iff:  nipkow@32408  258  "{a.. b <= a | c<=a & b<=d"  nipkow@32408  259 apply (auto simp:subset_eq Ball_def)  nipkow@32408  260 apply(frule_tac x=a in spec)  nipkow@32408  261 apply(erule_tac x=d in allE)  nipkow@32408  262 apply (simp add: less_imp_le)  nipkow@32408  263 done  nipkow@32408  264 nipkow@32456  265 subsubsection {* Intersection *}  nipkow@32456  266 nipkow@32456  267 context linorder  nipkow@32456  268 begin  nipkow@32456  269 nipkow@32456  270 lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"  nipkow@32456  271 by auto  nipkow@32456  272 nipkow@32456  273 lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"  nipkow@32456  274 by auto  nipkow@32456  275 nipkow@32456  276 lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"  nipkow@32456  277 by auto  nipkow@32456  278 nipkow@32456  279 lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"  nipkow@32456  280 by auto  nipkow@32456  281 nipkow@32456  282 lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"  nipkow@32456  283 by auto  nipkow@32456  284 nipkow@32456  285 lemma Int_atLeastLessThan[simp]: "{a.. Suc  {.. Suc (x - 1)" by auto  hoelzl@39072  315  with x < Suc n show "x = 0" by auto  hoelzl@39072  316 qed  hoelzl@39072  317 paulson@14485  318 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"  paulson@14485  319 by (simp add: lessThan_def atMost_def less_Suc_eq_le)  paulson@14485  320 paulson@14485  321 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"  paulson@14485  322 by blast  paulson@14485  323 paulson@15047  324 subsubsection {* The Constant @{term greaterThan} *}  paulson@15047  325 paulson@14485  326 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"  paulson@14485  327 apply (simp add: greaterThan_def)  paulson@14485  328 apply (blast dest: gr0_conv_Suc [THEN iffD1])  paulson@14485  329 done  paulson@14485  330 paulson@14485  331 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"  paulson@14485  332 apply (simp add: greaterThan_def)  paulson@14485  333 apply (auto elim: linorder_neqE)  paulson@14485  334 done  paulson@14485  335 paulson@14485  336 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"  paulson@14485  337 by blast  paulson@14485  338 paulson@15047  339 subsubsection {* The Constant @{term atLeast} *}  paulson@15047  340 paulson@14485  341 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"  paulson@14485  342 by (unfold atLeast_def UNIV_def, simp)  paulson@14485  343 paulson@14485  344 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"  paulson@14485  345 apply (simp add: atLeast_def)  paulson@14485  346 apply (simp add: Suc_le_eq)  paulson@14485  347 apply (simp add: order_le_less, blast)  paulson@14485  348 done  paulson@14485  349 paulson@14485  350 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"  paulson@14485  351  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)  paulson@14485  352 paulson@14485  353 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"  paulson@14485  354 by blast  paulson@14485  355 paulson@15047  356 subsubsection {* The Constant @{term atMost} *}  paulson@15047  357 paulson@14485  358 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"  paulson@14485  359 by (simp add: atMost_def)  paulson@14485  360 paulson@14485  361 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"  paulson@14485  362 apply (simp add: atMost_def)  paulson@14485  363 apply (simp add: less_Suc_eq order_le_less, blast)  paulson@14485  364 done  paulson@14485  365 paulson@14485  366 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"  paulson@14485  367 by blast  paulson@14485  368 paulson@15047  369 subsubsection {* The Constant @{term atLeastLessThan} *}  paulson@15047  370 nipkow@28068  371 text{*The orientation of the following 2 rules is tricky. The lhs is  nipkow@24449  372 defined in terms of the rhs. Hence the chosen orientation makes sense  nipkow@24449  373 in this theory --- the reverse orientation complicates proofs (eg  nipkow@24449  374 nontermination). But outside, when the definition of the lhs is rarely  nipkow@24449  375 used, the opposite orientation seems preferable because it reduces a  nipkow@24449  376 specific concept to a more general one. *}  nipkow@28068  377 paulson@15047  378 lemma atLeast0LessThan: "{0::nat.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  nipkow@15554  418 by (auto simp add: atLeastAtMost_def)  nipkow@15554  419 paulson@33044  420 lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j.. ?B" by auto  nipkow@16733  431 next  nipkow@16733  432  show "?B \ ?A"  nipkow@16733  433  proof  nipkow@16733  434  fix n assume a: "n : ?B"  webertj@20217  435  hence "n - k : {i..j}" by auto  nipkow@16733  436  moreover have "n = (n - k) + k" using a by auto  nipkow@16733  437  ultimately show "n : ?A" by blast  nipkow@16733  438  qed  nipkow@16733  439 qed  nipkow@16733  440 nipkow@16733  441 lemma image_add_atLeastLessThan:  nipkow@16733  442  "(%n::nat. n+k)  {i.. ?B" by auto  nipkow@16733  445 next  nipkow@16733  446  show "?B \ ?A"  nipkow@16733  447  proof  nipkow@16733  448  fix n assume a: "n : ?B"  webertj@20217  449  hence "n - k : {i..i. i - c)  {x ..< y} =  hoelzl@37664  473  (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"  hoelzl@37664  474  (is "_ = ?right")  hoelzl@37664  475 proof safe  hoelzl@37664  476  fix a assume a: "a \ ?right"  hoelzl@37664  477  show "a \ (\i. i - c)  {x ..< y}"  hoelzl@37664  478  proof cases  hoelzl@37664  479  assume "c < y" with a show ?thesis  hoelzl@37664  480  by (auto intro!: image_eqI[of _ _ "a + c"])  hoelzl@37664  481  next  hoelzl@37664  482  assume "\ c < y" with a show ?thesis  hoelzl@37664  483  by (auto intro!: image_eqI[of _ _ x] split: split_if_asm)  hoelzl@37664  484  qed  hoelzl@37664  485 qed auto  hoelzl@37664  486 hoelzl@35580  487 context ordered_ab_group_add  hoelzl@35580  488 begin  hoelzl@35580  489 hoelzl@35580  490 lemma  hoelzl@35580  491  fixes x :: 'a  hoelzl@35580  492  shows image_uminus_greaterThan[simp]: "uminus  {x<..} = {..<-x}"  hoelzl@35580  493  and image_uminus_atLeast[simp]: "uminus  {x..} = {..-x}"  hoelzl@35580  494 proof safe  hoelzl@35580  495  fix y assume "y < -x"  hoelzl@35580  496  hence *: "x < -y" using neg_less_iff_less[of "-y" x] by simp  hoelzl@35580  497  have "- (-y) \ uminus  {x<..}"  hoelzl@35580  498  by (rule imageI) (simp add: *)  hoelzl@35580  499  thus "y \ uminus  {x<..}" by simp  hoelzl@35580  500 next  hoelzl@35580  501  fix y assume "y \ -x"  hoelzl@35580  502  have "- (-y) \ uminus  {x..}"  hoelzl@35580  503  by (rule imageI) (insert y \ -x[THEN le_imp_neg_le], simp)  hoelzl@35580  504  thus "y \ uminus  {x..}" by simp  hoelzl@35580  505 qed simp_all  hoelzl@35580  506 hoelzl@35580  507 lemma  hoelzl@35580  508  fixes x :: 'a  hoelzl@35580  509  shows image_uminus_lessThan[simp]: "uminus  {.. finite N"  nipkow@28068  556 apply (rule finite_subset)  nipkow@28068  557  apply (rule_tac [2] finite_lessThan, auto)  nipkow@28068  558 done  nipkow@28068  559 nipkow@31044  560 text {* A set of natural numbers is finite iff it is bounded. *}  nipkow@31044  561 lemma finite_nat_set_iff_bounded:  nipkow@31044  562  "finite(N::nat set) = (EX m. ALL n:N. nnat. (!!n. n \ f n) ==> finite {n. f n \ u}"  nipkow@28068  578 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)  paulson@14485  579 nipkow@24853  580 text{* Any subset of an interval of natural numbers the size of the  nipkow@24853  581 subset is exactly that interval. *}  nipkow@24853  582 nipkow@24853  583 lemma subset_card_intvl_is_intvl:  nipkow@24853  584  "A <= {k.. A = {k..i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B")  nipkow@36755  606 proof  nipkow@36755  607  show "?A <= ?B"  nipkow@36755  608  proof  nipkow@36755  609  fix x assume "x : ?A"  nipkow@36755  610  then obtain i where i: "i\n" "x : M i" by auto  nipkow@36755  611  show "x : ?B"  nipkow@36755  612  proof(cases i)  nipkow@36755  613  case 0 with i show ?thesis by simp  nipkow@36755  614  next  nipkow@36755  615  case (Suc j) with i show ?thesis by auto  nipkow@36755  616  qed  nipkow@36755  617  qed  nipkow@36755  618 next  nipkow@36755  619  show "?B <= ?A" by auto  nipkow@36755  620 qed  nipkow@36755  621 nipkow@36755  622 lemma UN_le_add_shift:  nipkow@36755  623  "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B")  nipkow@36755  624 proof  nipkow@36755  625  show "?A <= ?B" by fastsimp  nipkow@36755  626 next  nipkow@36755  627  show "?B <= ?A"  nipkow@36755  628  proof  nipkow@36755  629  fix x assume "x : ?B"  nipkow@36755  630  then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto  nipkow@36755  631  hence "i-k\n & x : M((i-k)+k)" by auto  nipkow@36755  632  thus "x : ?A" by blast  nipkow@36755  633  qed  nipkow@36755  634 qed  nipkow@36755  635 paulson@32596  636 lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)"  paulson@32596  637  by (auto simp add: atLeast0LessThan)  paulson@32596  638 paulson@32596  639 lemma UN_finite_subset: "(!!n::nat. (\i\{0.. C) \ (\n. A n) \ C"  paulson@32596  640  by (subst UN_UN_finite_eq [symmetric]) blast  paulson@32596  641 paulson@33044  642 lemma UN_finite2_subset:  paulson@33044  643  "(!!n::nat. (\i\{0.. (\i\{0.. (\n. A n) \ (\n. B n)"  paulson@33044  644  apply (rule UN_finite_subset)  paulson@33044  645  apply (subst UN_UN_finite_eq [symmetric, of B])  paulson@33044  646  apply blast  paulson@33044  647  done  paulson@32596  648 paulson@32596  649 lemma UN_finite2_eq:  paulson@33044  650  "(!!n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)"  paulson@33044  651  apply (rule subset_antisym)  paulson@33044  652  apply (rule UN_finite2_subset, blast)  paulson@33044  653  apply (rule UN_finite2_subset [where k=k])  huffman@35216  654  apply (force simp add: atLeastLessThan_add_Un [of 0])  paulson@33044  655  done  paulson@32596  656 paulson@32596  657 paulson@14485  658 subsubsection {* Cardinality *}  paulson@14485  659 nipkow@15045  660 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  699 apply(drule ex_bij_betw_finite_nat)  nipkow@31438  700 apply(drule ex_bij_betw_nat_finite)  nipkow@31438  701 apply(auto intro!:bij_betw_trans)  nipkow@31438  702 done  nipkow@31438  703 nipkow@31438  704 lemma ex_bij_betw_nat_finite_1:  nipkow@31438  705  "finite M \ \h. bij_betw h {1 .. card M} M"  nipkow@31438  706 by (rule finite_same_card_bij) auto  nipkow@31438  707 nipkow@26105  708 paulson@14485  709 subsection {* Intervals of integers *}  paulson@14485  710 nipkow@15045  711 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l.. u ==>  nipkow@15045  724  {(0::int).. u")  paulson@14485  733  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  734  apply (rule finite_imageI)  paulson@14485  735  apply auto  paulson@14485  736  done  paulson@14485  737 nipkow@15045  738 lemma finite_atLeastLessThan_int [iff]: "finite {l.. u")  paulson@14485  760  apply (subst image_atLeastZeroLessThan_int, assumption)  paulson@14485  761  apply (subst card_image)  paulson@14485  762  apply (auto simp add: inj_on_def)  paulson@14485  763  done  paulson@14485  764 nipkow@15045  765 lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}"  bulwahn@27656  787 proof -  bulwahn@27656  788  have "{k. P k \ k < i} \ {.. M"  bulwahn@27656  794 shows "card {k \ M. k < Suc i} \ 0"  bulwahn@27656  795 proof -  bulwahn@27656  796  from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto  bulwahn@27656  797  with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)  bulwahn@27656  798 qed  bulwahn@27656  799 bulwahn@27656  800 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"  haftmann@37388  801 apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"])  bulwahn@27656  802 apply simp  bulwahn@27656  803 apply fastsimp  bulwahn@27656  804 apply auto  bulwahn@27656  805 apply (rule inj_on_diff_nat)  bulwahn@27656  806 apply auto  bulwahn@27656  807 apply (case_tac x)  bulwahn@27656  808 apply auto  bulwahn@27656  809 apply (case_tac xa)  bulwahn@27656  810 apply auto  bulwahn@27656  811 apply (case_tac xa)  bulwahn@27656  812 apply auto  bulwahn@27656  813 done  bulwahn@27656  814 bulwahn@27656  815 lemma card_less_Suc:  bulwahn@27656  816  assumes zero_in_M: "0 \ M"  bulwahn@27656  817  shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"  bulwahn@27656  818 proof -  bulwahn@27656  819  from assms have a: "0 \ {k \ M. k < Suc i}" by simp  bulwahn@27656  820  hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})"  bulwahn@27656  821  by (auto simp only: insert_Diff)  bulwahn@27656  822  have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto  bulwahn@27656  823  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  824  apply (subst card_insert)  bulwahn@27656  825  apply simp_all  bulwahn@27656  826  apply (subst b)  bulwahn@27656  827  apply (subst card_less_Suc2[symmetric])  bulwahn@27656  828  apply simp_all  bulwahn@27656  829  done  bulwahn@27656  830  with c show ?thesis by simp  bulwahn@27656  831 qed  bulwahn@27656  832 paulson@14485  833 paulson@13850  834 subsection {*Lemmas useful with the summation operator setsum*}  paulson@13850  835 ballarin@16102  836 text {* For examples, see Algebra/poly/UnivPoly2.thy *}  ballarin@13735  837 wenzelm@14577  838 subsubsection {* Disjoint Unions *}  ballarin@13735  839 wenzelm@14577  840 text {* Singletons and open intervals *}  ballarin@13735  841 ballarin@13735  842 lemma ivl_disj_un_singleton:  nipkow@15045  843  "{l::'a::linorder} Un {l<..} = {l..}"  nipkow@15045  844  "{.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  nipkow@15045  848  "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  nipkow@15045  857  "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}"  nipkow@15045  859  "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}"  nipkow@15045  861  "(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  873  "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}"  ballarin@14398  875 by auto  ballarin@13735  876 ballarin@13735  877 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two  ballarin@13735  878 wenzelm@14577  879 subsubsection {* Disjoint Intersections *}  ballarin@13735  880 wenzelm@14577  881 text {* One- and two-sided intervals *}  ballarin@13735  882 ballarin@13735  883 lemma ivl_disj_int_one:  nipkow@15045  884  "{..l::'a::order} Int {l<.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))"  nipkow@15542  920 apply(auto simp:linorder_not_le)  nipkow@15542  921 apply(rule ccontr)  nipkow@15542  922 apply(insert linorder_le_less_linear[of i n])  nipkow@15542  923 apply(clarsimp simp:linorder_not_le)  nipkow@15542  924 apply(fastsimp)  nipkow@15542  925 done  nipkow@15542  926 nipkow@15041  927 nipkow@15042  928 subsection {* Summation indexed over intervals *}  nipkow@15042  929 nipkow@15042  930 syntax  nipkow@15042  931  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  932  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  933  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  nipkow@16052  934  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  nipkow@15042  935 syntax (xsymbols)  nipkow@15042  936  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  937  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  938  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  939  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15042  940 syntax (HTML output)  nipkow@15042  941  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  nipkow@15048  942  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  nipkow@16052  943  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  nipkow@16052  944  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  nipkow@15056  945 syntax (latex_sum output)  nipkow@15052  946  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  947  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@15052  948  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  nipkow@15052  949  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  nipkow@16052  950  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  951  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15052  952  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  nipkow@16052  953  ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  nipkow@15041  954 nipkow@15048  955 translations  nipkow@28853  956  "\x=a..b. t" == "CONST setsum (%x. t) {a..b}"  nipkow@28853  957  "\x=a..i\n. t" == "CONST setsum (\i. t) {..n}"  nipkow@28853  959  "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  nipkow@15056  967 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  nipkow@15056  969 @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \  nipkow@15542  992  setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)"  nipkow@16052  999 by (simp add:atMost_Suc add_ac)  nipkow@16052  1000 nipkow@16041  1001 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n"  nipkow@16041  1002 by (simp add:lessThan_Suc add_ac)  nipkow@15041  1003 nipkow@15911  1004 lemma setsum_cl_ivl_Suc[simp]:  nipkow@15561  1005  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  nipkow@15561  1006 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@15561  1007 nipkow@15911  1008 lemma setsum_op_ivl_Suc[simp]:  nipkow@15561  1009  "setsum f {m..  nipkow@15561  1013  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  nipkow@15561  1014 by (auto simp:add_ac atLeastAtMostSuc_conv)  nipkow@16041  1015 *)  nipkow@28068  1016 nipkow@28068  1017 lemma setsum_head:  nipkow@28068  1018  fixes n :: nat  nipkow@28068  1019  assumes mn: "m <= n"  nipkow@28068  1020  shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")  nipkow@28068  1021 proof -  nipkow@28068  1022  from mn  nipkow@28068  1023  have "{m..n} = {m} \ {m<..n}"  nipkow@28068  1024  by (auto intro: ivl_disj_un_singleton)  nipkow@28068  1025  hence "?lhs = (\x\{m} \ {m<..n}. P x)"  nipkow@28068  1026  by (simp add: atLeast0LessThan)  nipkow@28068  1027  also have "\ = ?rhs" by simp  nipkow@28068  1028  finally show ?thesis .  nipkow@28068  1029 qed  nipkow@28068  1030 nipkow@28068  1031 lemma setsum_head_Suc:  nipkow@28068  1032  "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}"  nipkow@28068  1033 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)  nipkow@28068  1034 nipkow@28068  1035 lemma setsum_head_upt_Suc:  nipkow@28068  1036  "m < n \ setsum f {m.. n + 1"  nipkow@31501  1042  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"  nipkow@31501  1043 proof-  nipkow@31501  1044  have "{m .. n+p} = {m..n} \ {n+1..n+p}" using m \ n+1 by auto  nipkow@31501  1045  thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint  nipkow@31501  1046  atLeastSucAtMost_greaterThanAtMost)  nipkow@31501  1047 qed  nipkow@28068  1048 nipkow@15539  1049 lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \  nipkow@15539  1050  setsum f {m.. 'a::ab_group_add"  nipkow@15539  1055 shows "\ m \ n; n \ p \ \  nipkow@15539  1056  setsum f {m.. ('a::ab_group_add)"  nipkow@31505  1063  shows "setsum (\k. f k - f(k + 1)) {(m::nat) .. n} =  nipkow@31505  1064  (if m <= n then f m - f(n + 1) else 0)"  nipkow@31505  1065 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)  nipkow@31505  1066 nipkow@31509  1067 lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]  nipkow@31509  1068 nipkow@31509  1069 lemma setsum_setsum_restrict:  nipkow@31509  1070  "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  1071  by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)  nipkow@31509  1072  (rule setsum_commute)  nipkow@31509  1073 nipkow@31509  1074 lemma setsum_image_gen: assumes fS: "finite S"  nipkow@31509  1075  shows "setsum g S = setsum (\y. setsum g {x. x \ S \ f x = y}) (f  S)"  nipkow@31509  1076 proof-  nipkow@31509  1077  { fix x assume "x \ S" then have "{y. y\ fS \ f x = y} = {f x}" by auto }  nipkow@31509  1078  hence "setsum g S = setsum (\x. setsum (\y. g x) {y. y\ fS \ f x = y}) S"  nipkow@31509  1079  by simp  nipkow@31509  1080  also have "\ = setsum (\y. setsum g {x. x \ S \ f x = y}) (f  S)"  nipkow@31509  1081  by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]])  nipkow@31509  1082  finally show ?thesis .  nipkow@31509  1083 qed  nipkow@31509  1084 hoelzl@35171  1085 lemma setsum_le_included:  haftmann@36307  1086  fixes f :: "'a \ 'b::ordered_comm_monoid_add"  hoelzl@35171  1087  assumes "finite s" "finite t"  hoelzl@35171  1088  and "\y\t. 0 \ g y" "(\x\s. \y\t. i y = x \ f x \ g y)"  hoelzl@35171  1089  shows "setsum f s \ setsum g t"  hoelzl@35171  1090 proof -  hoelzl@35171  1091  have "setsum f s \ setsum (\y. setsum g {x. x\t \ i x = y}) s"  hoelzl@35171  1092  proof (rule setsum_mono)  hoelzl@35171  1093  fix y assume "y \ s"  hoelzl@35171  1094  with assms obtain z where z: "z \ t" "y = i z" "f y \ g z" by auto  hoelzl@35171  1095  with assms show "f y \ setsum g {x \ t. i x = y}" (is "?A y \ ?B y")  hoelzl@35171  1096  using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]  hoelzl@35171  1097  by (auto intro!: setsum_mono2)  hoelzl@35171  1098  qed  hoelzl@35171  1099  also have "... \ setsum (\y. setsum g {x. x\t \ i x = y}) (i  t)"  hoelzl@35171  1100  using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)  hoelzl@35171  1101  also have "... \ setsum g t"  hoelzl@35171  1102  using assms by (auto simp: setsum_image_gen[symmetric])  hoelzl@35171  1103  finally show ?thesis .  hoelzl@35171  1104 qed  hoelzl@35171  1105 nipkow@31509  1106 lemma setsum_multicount_gen:  nipkow@31509  1107  assumes "finite s" "finite t" "\j\t. (card {i\s. R i j} = k j)"  nipkow@31509  1108  shows "setsum (\i. (card {j\t. R i j})) s = setsum k t" (is "?l = ?r")  nipkow@31509  1109 proof-  nipkow@31509  1110  have "?l = setsum (\i. setsum (\x.1) {j\t. R i j}) s" by auto  nipkow@31509  1111  also have "\ = ?r" unfolding setsum_setsum_restrict[OF assms(1-2)]  nipkow@31509  1112  using assms(3) by auto  nipkow@31509  1113  finally show ?thesis .  nipkow@31509  1114 qed  nipkow@31509  1115 nipkow@31509  1116 lemma setsum_multicount:  nipkow@31509  1117  assumes "finite S" "finite T" "\j\T. (card {i\S. R i j} = k)"  nipkow@31509  1118  shows "setsum (\i. card {j\T. R i j}) S = k * card T" (is "?l = ?r")  nipkow@31509  1119 proof-  nipkow@31509  1120  have "?l = setsum (\i. k) T" by(rule setsum_multicount_gen)(auto simp:assms)  huffman@35216  1121  also have "\ = ?r" by(simp add: mult_commute)  nipkow@31509  1122  finally show ?thesis by auto  nipkow@31509  1123 qed  nipkow@31509  1124 nipkow@28068  1125 nipkow@16733  1126 subsection{* Shifting bounds *}  nipkow@16733  1127 nipkow@15539  1128 lemma setsum_shift_bounds_nat_ivl:  nipkow@15539  1129  "setsum f {m+k.. setsum f {Suc 0..k} = setsum f {0..k}"  nipkow@28068  1148 by(simp add:setsum_head_Suc)  kleing@19106  1149 nipkow@28068  1150 lemma setsum_shift_lb_Suc0_0_upt:  nipkow@28068  1151  "f(0::nat) = 0 \ setsum f {Suc 0.. 1"  haftmann@36307  1160  shows "(\i=0.. 0" by simp_all  haftmann@36307  1163  moreover have "(\i=0.. 0 have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp  haftmann@36350  1169  ultimately show ?case by (simp add: field_simps divide_inverse)  haftmann@36307  1170  qed  haftmann@36307  1171  ultimately show ?thesis by simp  haftmann@36307  1172 qed  haftmann@36307  1173 ballarin@17149  1174 kleing@19469  1175 subsection {* The formula for arithmetic sums *}  kleing@19469  1176 kleing@19469  1177 lemma gauss_sum:  huffman@23277  1178  "((1::'a::comm_semiring_1) + 1)*(\i\{1..n}. of_nat i) =  kleing@19469  1179  of_nat n*((of_nat n)+1)"  kleing@19469  1180 proof (induct n)  kleing@19469  1181  case 0  kleing@19469  1182  show ?case by simp  kleing@19469  1183 next  kleing@19469  1184  case (Suc n)  nipkow@29667  1185  then show ?case by (simp add: algebra_simps)  kleing@19469  1186 qed  kleing@19469  1187 kleing@19469  1188 theorem arith_series_general:  huffman@23277  1189  "((1::'a::comm_semiring_1) + 1) * (\i\{.. 1"  kleing@19469  1193  let ?I = "\i. of_nat i" and ?n = "of_nat n"  kleing@19469  1194  have  kleing@19469  1195  "(\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  1208  by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)  huffman@23431  1209  (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]])  nipkow@29667  1210  finally show ?thesis by (simp add: algebra_simps)  kleing@19469  1211 next  kleing@19469  1212  assume "\(n > 1)"  kleing@19469  1213  hence "n = 1 \ n = 0" by auto  nipkow@29667  1214  thus ?thesis by (auto simp: algebra_simps)  kleing@19469  1215 qed  kleing@19469  1216 kleing@19469  1217 lemma arith_series_nat:  kleing@19469  1218  "Suc (Suc 0) * (\i\{..i\{..i\{..i\{..nat"  kleing@19022  1241  shows  kleing@19022  1242  "\x. Q x \ P x \  kleing@19022  1243  (\xxxxx 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1269  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1270  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10)  paulson@29960  1271  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10)  paulson@29960  1272 syntax (xsymbols)  paulson@29960  1273  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1274  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1275  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1276  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1277 syntax (HTML output)  paulson@29960  1278  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  paulson@29960  1279  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  paulson@29960  1280  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  paulson@29960  1281  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  paulson@29960  1282 syntax (latex_prod output)  paulson@29960  1283  "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1284  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1285  "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b"  paulson@29960  1286  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  paulson@29960  1287  "_upt_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1288  ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1289  "_upto_setprod" :: "idt \ 'a \ 'b \ 'b"  paulson@29960  1290  ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  paulson@29960  1291 paulson@29960  1292 translations  paulson@29960  1293  "\x=a..b. t" == "CONST setprod (%x. t) {a..b}"  paulson@29960  1294  "\x=a..i\n. t" == "CONST setprod (\i. t) {..n}"  paulson@29960  1296  "\ii. t) {..= 0 \ nat_set {x..y}"  haftmann@33318  1312  by (simp add: nat_set_def)  haftmann@33318  1313 haftmann@35644  1314 declare transfer_morphism_nat_int[transfer add  haftmann@33318  1315  return: transfer_nat_int_set_functions  haftmann@33318  1316  transfer_nat_int_set_function_closures  haftmann@33318  1317 ]  haftmann@33318  1318 haftmann@33318  1319 lemma transfer_int_nat_set_functions:  haftmann@33318  1320  "is_nat m \ is_nat n \ {m..n} = int  {nat m..nat n}"  haftmann@33318  1321  by (simp only: is_nat_def transfer_nat_int_set_functions  haftmann@33318  1322  transfer_nat_int_set_function_closures  haftmann@33318  1323  transfer_nat_int_set_return_embed nat_0_le  haftmann@33318  1324  cong: transfer_nat_int_set_cong)  haftmann@33318  1325 haftmann@33318  1326 lemma transfer_int_nat_set_function_closures:  haftmann@33318  1327  "is_nat x \ nat_set {x..y}"  haftmann@33318  1328  by (simp only: transfer_nat_int_set_function_closures is_nat_def)  haftmann@33318  1329 haftmann@35644  1330 declare transfer_morphism_int_nat[transfer add  haftmann@33318  1331  return: transfer_int_nat_set_functions  haftmann@33318  1332  transfer_int_nat_set_function_closures  haftmann@33318  1333 ]  haftmann@33318  1334 nipkow@8924  1335 end